Skip to content

Commit 368628f

Browse files
jvanbrueggejvanbruegge
committed
WIP
1 parent 7dca25e commit 368628f

File tree

3 files changed

+51
-18
lines changed

3 files changed

+51
-18
lines changed

‎Tools/mrsbnf_def.ML‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -175,7 +175,7 @@ fun note_mrsbnf_thms fact_policy qualify name_opt mrsbnf lthy =
175175
]
176176
|> filter_out (null o #2)
177177
|> map (fn (thmN, thms, attrs) => ((qualify (Binding.qualify true (short_type_name (name ())) (Binding.name thmN)), attrs), [
178-
(map (Local_Defs.unfold0 lthy unfolds) thms, [])
178+
(thms, [])
179179
]));
180180
in Local_Theory.notes notes lthy |>> append noted end
181181
val fact_policy = fact_policy (Proof_Context.theory_of lthy);

‎Tools/tvsubst.ML‎

Lines changed: 42 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -603,7 +603,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
603603
val ((((fs, rhos), hs), x), _) = lthy
604604
|> mk_Frees "f" (map ((fn a => a --> a) o HOLogic.dest_setT o body_type o fastype_of) (BMV_Monad_Def.leader BMV_Monad_Def.RVrs_of_bmv_monad bmv))
605605
||>> mk_Frees "\<rho>" (map fastype_of (BMV_Monad_Def.leader BMV_Monad_Def.Injs_of_bmv_monad bmv))
606-
||>> mk_Frees "h" (replicate 2 (#T quot --> #T quot))
606+
||>> mk_Frees "h" (replicate nrecs (#T quot --> #T quot))
607607
||>> apfst hd o mk_Frees "x" [domain_type (fastype_of (#ctor quot))];
608608

609609
val prems = flat (BMV_Monad_Def.mk_small_prems_of_bmv_monad bmv
@@ -671,8 +671,11 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
671671

672672
val rho_prems = Proof_Context.get_thms lthy "f_prems";
673673

674-
val avoiding_sets = map (foldl1 mk_Un o map_filter I) (transpose IImsuppss);
674+
val avoiding_sets = map2 (fn free =>
675+
the_default (mk_bot free) o try (foldl1 mk_Un) o map_filter I
676+
) frees (transpose (filter_out null IImsuppss));
675677

678+
val _ = @{print} "3"
676679
val Uctor =
677680
let
678681
val ctor = #ctor quot;
@@ -855,9 +858,9 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
855858
],
856859
REPEAT_DETERM o rtac ctxt @{thm Un_mono'},
857860
SELECT_GOAL (Local_Defs.unfold0_tac ctxt (no_reflexive (#set_Vrs mrsbnf_axioms))),
858-
EqSubst.eqsubst_tac ctxt [0] (#Vrs_Sbs bmv_axioms),
861+
EqSubst.eqsubst_tac ctxt [0] (#Sb_Inj bmv_axioms :: #Vrs_Sbs bmv_axioms),
859862
REPEAT_DETERM o resolve_tac ctxt (@{thms supp_id_bound} @ rho_prems),
860-
K (Local_Defs.unfold0_tac ctxt @{thms image_id}),
863+
K (Local_Defs.unfold0_tac ctxt @{thms image_id id_apply}),
861864
rtac ctxt @{thm Un_upper1} ORELSE' EVERY' [
862865
rtac ctxt @{thm subsetI},
863866
etac ctxt @{thm UN_E},
@@ -893,14 +896,15 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
893896
rtac ctxt @{thm UN_mono[OF subset_refl]},
894897
resolve_tac ctxt prems,
895898
SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms prod.collapse}),
896-
eresolve_tac ctxt @{thms UnI1 UnI2}
899+
eresolve_tac ctxt @{thms UnI1 UnI2} ORELSE' assume_tac ctxt
897900
]
898901
]) ctxt
899902
])), Position.no_range), NONE) state;
900903

901904
val (tvsubst, lthy) = mk_def_t true Binding.empty I (Binding.name_of tvsubst_b) 0
902905
(hd (MRBNF_Recursor.get_RECs true "tvsubst" lthy)) lthy;
903906

907+
val _ = @{print} "4"
904908
val tvsubst_not_isInj =
905909
let
906910
val x = Free ("x", domain_type (fastype_of (#ctor quot)));
@@ -1143,6 +1147,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
11431147
| _ => error "only works for datatypes"
11441148
val fresh_induct = #fresh_induct fp_thms;
11451149

1150+
(* needs to account for vars that are not injections on RHS *)
11461151
val FVars_tvsubsts = map (fn FVars =>
11471152
let
11481153
val t = Free ("t", domain_type (fastype_of FVars));
@@ -1159,6 +1164,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
11591164
FVars $ (Term.list_comb (fst tvsubst, map_filter I rhos) $ t),
11601165
foldl1 mk_Un rhss
11611166
);
1167+
val _ = @{print} (Thm.cterm_of lthy goal)
11621168
in Goal.prove_sorry lthy (names (map_filter I rhos @ [t])) rho_prems' goal (fn {context=ctxt, prems} => EVERY1 [
11631169
DETERM o rtac ctxt (infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) avoiding_sets) fresh_induct),
11641170
REPEAT_DETERM_N nvars o SELECT_GOAL (REPEAT_DETERM (FIRST1 [
@@ -1184,25 +1190,42 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
11841190
EqSubst.eqsubst_tac ctxt [0] (#Vrs_Sbs bmv_axioms),
11851191
REPEAT_DETERM o resolve_tac ctxt (@{thms supp_id_bound} @ prems)
11861192
],
1187-
K (Local_Defs.unfold0_tac ctxt (@{thms image_id UN_Un} @ #Vrs_Map (the (BMV_Monad_Def.leader BMV_Monad_Def.params_of_bmv_monad bmv)))),
1193+
K (Local_Defs.unfold0_tac ctxt (@{thms image_id UN_Un id_apply}
1194+
@ #Vrs_Map (the (BMV_Monad_Def.leader BMV_Monad_Def.params_of_bmv_monad bmv))
1195+
@ [#Sb_Inj bmv_axioms]
1196+
)),
1197+
K (print_tac ctxt "1"),
11881198
rtac ctxt (mk_Un_cong (nrecs + 1) (length rhss)),
1189-
REPEAT_DETERM o EVERY' [
1190-
EqSubst.eqsubst_tac ctxt [0] (map_filter (Option.map (#eta_compl_free o #axioms)) defs),
1199+
REPEAT_DETERM_N 10 o EVERY' [ (* TODO: fix *)
1200+
EqSubst.eqsubst_tac ctxt [0] (@{print}(map_filter (Option.map (#eta_compl_free o #axioms)) defs)),
1201+
K (print_tac ctxt "1.1"),
11911202
SELECT_GOAL (Local_Defs.unfold0_tac ctxt (map_filter (Option.map (snd o #isInj)) defs)),
11921203
rotate_tac ~1,
11931204
etac ctxt @{thm contrapos_np},
1205+
K (print_tac ctxt "1.2"),
11941206
SELECT_GOAL (Local_Defs.unfold0_tac ctxt (@{thms not_all not_not comp_def} @ map_filter (Option.map (snd o #Inj)) defs)),
11951207
etac ctxt exE,
11961208
hyp_subst_tac ctxt,
1209+
K (print_tac ctxt "1.3"),
11971210
rtac ctxt exI,
1198-
rtac ctxt refl
1211+
rtac ctxt refl,
1212+
K (print_tac ctxt "1.35")
11991213
],
1200-
K (Local_Defs.unfold0_tac ctxt @{thms UN_empty Un_empty_left Un_empty_right}),
1214+
K (Local_Defs.unfold0_tac ctxt (@{thms UN_empty Un_empty_left Un_empty_right image_id}
1215+
@ the_default [] (Option.map single (#Map_map mrsbnf_facts))
1216+
)),
1217+
TRY o EVERY' [
1218+
EqSubst.eqsubst_tac ctxt [0] (MRBNF_Def.set_map_of_mrbnf mrbnf),
1219+
REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id}
1220+
],
1221+
K (Local_Defs.unfold0_tac ctxt (@{thms image_id})),
1222+
K (print_tac ctxt "1.4"),
12011223
rtac ctxt refl,
12021224
rtac ctxt trans,
12031225
rtac ctxt @{thm arg_cong2[OF _ refl, of _ _ "minus"]},
12041226
rtac ctxt @{thm UN_cong},
12051227
Goal.assume_rule_tac ctxt,
1228+
K (print_tac ctxt "2"),
12061229
REPEAT_DETERM o EVERY' [
12071230
EqSubst.eqsubst_tac ctxt [0] (maps (the_default []) IImsupp_Diffs @ maps (the_default [] o #IImsupp_Diffs) sugars),
12081231
REPEAT_DETERM o (assume_tac ctxt ORELSE' EVERY' [
@@ -1218,12 +1241,16 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
12181241
])
12191242
])
12201243
],
1244+
K (print_tac ctxt "3"),
12211245
K (Local_Defs.unfold0_tac ctxt @{thms Un_Diff[symmetric]}),
12221246
rtac ctxt @{thm arg_cong2[OF _ refl, of _ _ "minus"]},
12231247
K (Local_Defs.unfold0_tac ctxt @{thms UN_UN_flatten UN_Un_distrib[symmetric]}),
12241248
rtac ctxt refl,
1225-
rtac ctxt @{thm UN_cong},
1226-
Goal.assume_rule_tac ctxt,
1249+
TRY o EVERY' [
1250+
rtac ctxt @{thm UN_cong},
1251+
Goal.assume_rule_tac ctxt
1252+
],
1253+
K (print_tac ctxt "4"),
12271254
EVERY' (map_filter (Option.map (fn def => EVERY' [
12281255
K (Local_Defs.unfold0_tac ctxt [snd (#isInj def)]),
12291256
etac ctxt exE,
@@ -1234,8 +1261,10 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
12341261
K (Local_Defs.unfold0_tac ctxt (@{thms UN_single UN_empty Un_empty_left Un_empty_right}
12351262
@ maps (the_default []) FVars_Injs
12361263
)),
1264+
K (print_tac ctxt "5"),
12371265
rtac ctxt refl
1238-
])) (rev defs))
1266+
])) (rev defs)),
1267+
K (print_tac ctxt "end")
12391268
]) end
12401269
) (#FVarss quot);
12411270

‎tests/Regression_Tests.thy‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
theory Regression_Tests
22
imports "Binders.MRBNF_Recursor" "../thys/LetRec/DAList_MRBNF" "HOL-Library.FSet"
33
begin
4-
4+
(*
55
(* #68 *)
66
binder_datatype 'a trm =
77
Var 'a
@@ -14,7 +14,6 @@ binder_datatype 'a LLC =
1414
| Abs x::'a t::"'a LLC" binds x in t
1515
| Let "(x::'a, t::'a LLC) alist" u::"'a LLC" binds x in t u
1616

17-
declare [[ML_print_depth=1000]]
1817
(* #70 *)
1918
datatype ('tv, 'ev, 'rv) type = Type 'tv 'ev 'rv
2019
binder_datatype ('tv, 'ev, 'rv) type_scheme =
@@ -25,14 +24,19 @@ binder_datatype ('tv, 'ev, 'rv) type_scheme =
2524
binder_datatype ('tv, 'ev, 'rv) type_scheme2 =
2625
TAll "(X::'tv) list" \<sigma>::"('tv, 'ev, 'rv) type_scheme2" binds X in \<sigma>
2726
| ERAll "(\<epsilon>::'ev) list" "(\<rho>::'rv) list" T::"('tv, 'ev, 'rv) type" binds \<epsilon> \<rho> in T
27+
*)
28+
ML \<open>
29+
Multithreading.parallel_proofs := 0
30+
\<close>
2831

2932
(* #75 *)
3033
binder_datatype ('a, 'b, 'c, 'd) trm3 =
3134
Var 'a
35+
(* | Test "'b list" *)
3236
| App "('a, 'b, 'c, 'd) trm3" "('a, 'b, 'c, 'd) trm3"
3337
| Lam a::'a b::'b c::'c d::'d e::"('a, 'b, 'c, 'd) trm3" binds a b c d in e
3438

35-
(* #74 *)
39+
(*(* #74 *)
3640
binder_datatype 'a trm4 = V 'a | Lm x::'a t::"'a trm4" binds x in t
3741
binder_datatype 'a foo = Foo 'a | Bind "(x::'a) trm4" t::"'a foo" binds x in t
3842

@@ -92,5 +96,5 @@ lemma
9296
fixes x y::"'a::var" and e::"'a term"
9397
shows "e = e"
9498
by (binder_induction e avoiding: "{x} \<union> {y}" rule: term.strong_induct) auto
95-
99+
*)
96100
end

0 commit comments

Comments
 (0)