Skip to content

Commit 7a0ebe6

Browse files
jvanbrueggejvanbruegge
committed
Fix operations theories
1 parent cba39d7 commit 7a0ebe6

File tree

4 files changed

+15
-144
lines changed

4 files changed

+15
-144
lines changed

‎Tools/mrbnf_sugar.ML‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1257,6 +1257,8 @@ fun create_binder_datatype (spec : spec) lthy =
12571257
("inject", injects, simp)
12581258
] @ the_default [] (Option.map (fn (res, tvsubst_simps) => [
12591259
("subst", tvsubst_simps, simp),
1260+
("IImsupp_permute_commute", #IImsupp_permute_commutes res, []),
1261+
("IImsupp_Diff", #IImsupp_Diffs res, []),
12601262
("tvsubst_permute", [#tvsubst_permute res], [])
12611263
]) tvsubst_opt)) |> (map (fn (thmN, thms, attrs) =>
12621264
((Binding.qualify true (Binding.name_of (#fp_b spec)) (Binding.name thmN), attrs), [(thms, [])])

‎Tools/tvsubst.ML‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -431,8 +431,8 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
431431
dtac ctxt @{thm iffD1[OF disjoint_iff]},
432432
etac ctxt allE,
433433
etac ctxt impE,
434-
rtac ctxt UnI1,
435-
rtac ctxt CollectI,
434+
rtac ctxt @{thm UnI1},
435+
rtac ctxt @{thm CollectI},
436436
assume_tac ctxt,
437437
K (unfold_thms_tac ctxt @{thms Un_iff de_Morgan_disj mem_Collect_eq not_not}),
438438
etac ctxt conjE,
@@ -483,8 +483,8 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
483483
rtac ctxt @{thm imsupp_id_on},
484484
etac ctxt @{thm Int_subset_empty2},
485485
SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms SSupp_def IImsupp_def}),
486-
rtac ctxt subsetI,
487-
TRY o rtac ctxt UnI2,
486+
rtac ctxt @{thm subsetI},
487+
TRY o rtac ctxt @{thm UnI2},
488488
rtac ctxt @{thm UN_I[rotated]},
489489
assume_tac ctxt,
490490
rtac ctxt @{thm CollectI},
@@ -788,7 +788,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
788788
SELECT_GOAL (Local_Defs.unfold0_tac ctxt (@{thms id_o o_id} @ map (fn thm => thm RS sym) (no_reflexive (maps #set_Vrs (MRSBNF_Def.axioms_of_mrsbnf mrsbnf))))),
789789
EqSubst.eqsubst_asm_tac ctxt [0] (MRBNF_Def.set_map_of_mrbnf mrbnf),
790790
REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id}),
791-
etac ctxt imageE,
791+
etac ctxt @{thm imageE},
792792
hyp_subst_tac ctxt,
793793
rtac ctxt @{thm trans[OF comp_apply]},
794794
K (Local_Defs.unfold0_tac ctxt @{thms inv_simp1}),
@@ -1123,15 +1123,15 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
11231123
hyp_subst_tac_thin true ctxt,
11241124
rtac ctxt @{thm set_eqI},
11251125
rtac ctxt iffI,
1126-
REPEAT_DETERM_N (i - 1) o etac ctxt UnE,
1126+
REPEAT_DETERM_N (i - 1) o etac ctxt @{thm UnE},
11271127
EVERY' (map (fn i' => EVERY' [
1128-
REPEAT_DETERM_N (j - 1) o etac ctxt UnE,
1128+
REPEAT_DETERM_N (j - 1) o etac ctxt @{thm UnE},
11291129
EVERY' (map (fn j' => EVERY' [
11301130
rtac ctxt (mk_UnIN j j'),
11311131
etac ctxt (mk_UnIN i i')
11321132
]) (1 upto j))
11331133
]) (1 upto i)),
1134-
REPEAT_DETERM_N (j - 1) o etac ctxt UnE,
1134+
REPEAT_DETERM_N (j - 1) o etac ctxt @{thm UnE},
11351135
EVERY' (map (fn j' => EVERY' [
11361136
REPEAT_DETERM o etac ctxt @{thm Un_forward},
11371137
REPEAT_DETERM o etac ctxt (mk_UnIN j j')
@@ -1209,7 +1209,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
12091209
etac ctxt @{thm Int_subset_empty2},
12101210
rtac ctxt @{thm subsetI},
12111211
SELECT_GOAL (EVERY1 [
1212-
REPEAT_DETERM o etac ctxt UnE,
1212+
REPEAT_DETERM o etac ctxt @{thm UnE},
12131213
REPEAT_DETERM o FIRST' [
12141214
assume_tac ctxt,
12151215
eresolve_tac ctxt @{thms UnI1 UnI2},
@@ -1440,7 +1440,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
14401440
],
14411441
K (Local_Defs.unfold0_tac ctxt @{thms image_id}),
14421442
SELECT_GOAL (EVERY1 [
1443-
REPEAT_DETERM o etac ctxt UnE,
1443+
REPEAT_DETERM o etac ctxt @{thm UnE},
14441444
REPEAT_DETERM o FIRST' [
14451445
assume_tac ctxt,
14461446
eresolve_tac ctxt @{thms UnI1 UnI2},

‎operations/BMV_Fixpoint.thy‎

Lines changed: 3 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -477,8 +477,8 @@ interpretation tvsubst: QREC_fixed_FTerm "avoiding_set1 f1 f2"
477477

478478
apply (rule trans)
479479
apply (rule FTerm.permute_ctor)
480-
apply (assumption | rule ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+
481-
480+
apply (assumption)+
481+
thm trans[OF comp_apply[symmetric] FTerm_pre.map_Sb_strong(1)[THEN fun_cong]]
482482
apply (subst trans[OF comp_apply[symmetric] FTerm_pre.map_Sb_strong(1)[THEN fun_cong]])
483483
apply (assumption | rule supp_id_bound bij_id f_prems)+
484484
apply (unfold0 id_o o_id inv_o_simp2 comp_apply)
@@ -502,9 +502,6 @@ interpretation tvsubst: QREC_fixed_FTerm "avoiding_set1 f1 f2"
502502
apply (erule Int_subset_empty2)
503503
apply (rule subsetI)
504504
apply (rule UnI2)
505-
apply (unfold IImsupp_FType_def comp_def SSupp_FType_def tvVVr_tvsubst_FType_def tv\<eta>_FType_tvsubst_FType_def
506-
IImsupp_def SSupp_def VVr_def TyVar_def
507-
)[1]
508505
apply assumption
509506
done
510507

@@ -947,11 +944,6 @@ lemma FVars_tvsubst2:
947944
apply (subst IImsupp_Diff, assumption+)
948945
apply (subst FType.IImsupp_Diff)
949946
apply (erule Int_subset_empty2)
950-
(* This is only because FType does not use BMVs yet, not part of the tactic *)
951-
apply (unfold IImsupp_FType_def SSupp_FType_def tvVVr_tvsubst_FType_def tv\<eta>_FType_tvsubst_FType_def
952-
TyVar_def[symmetric] SSupp_def[of TyVar, symmetric, THEN meta_eq_to_obj_eq, THEN fun_cong]
953-
comp_def IImsupp_def[of TyVar FVars_FType, symmetric, THEN meta_eq_to_obj_eq, THEN fun_cong]
954-
)[1]
955947
apply (rule Un_upper2)
956948
apply (unfold Un_Diff[symmetric])
957949
apply (rule arg_cong2[OF _ refl, of _ _ "minus"])
@@ -1552,7 +1544,7 @@ val mrbnf = the (MRBNF_Def.mrbnf_of lthy @{type_name FTerm});
15521544
open BNF_Util
15531545
15541546
val x = TVSubst.create_tvsubst_of_mrsbnf
1555-
I fp_res mrsbnf mrbnf @{thm FTerm.vvsubst_cctor} @{binding tvsubst_FTerm'} [SOME {
1547+
I fp_res mrsbnf mrbnf @{thm FTerm.vvsubst_cctor} @{thm FTerm.vvsubst_permute} @{binding tvsubst_FTerm'} [SOME {
15561548
eta = @{term "\<eta> :: 'v::var \<Rightarrow> ('tv::var, 'v::var, 'a::var, 'b::var, 'c, 'd) FTerm_pre"},
15571549
Inj = (@{term "Var :: 'v \<Rightarrow> ('tv::var, 'v::var) FTerm"}, @{thm Var_def}),
15581550
tacs = {

‎operations/BMV_Monad.thy‎

Lines changed: 0 additions & 123 deletions
Original file line numberDiff line numberDiff line change
@@ -21,129 +21,6 @@ abbreviation Inj_FType_1 :: "'tyvar::var \<Rightarrow> 'tyvar FType" where "Inj_
2121
abbreviation Sb_FType :: "('tyvar::var \<Rightarrow> 'tyvar FType) \<Rightarrow> 'tyvar FType \<Rightarrow> 'tyvar FType" where "Sb_FType \<equiv> tvsubst_FType"
2222
abbreviation Vrs_FType_1 :: "'tyvar::var FType \<Rightarrow> 'tyvar set" where "Vrs_FType_1 \<equiv> FVars_FType"
2323

24-
lemma VVr_eq_Var_FType: "tvVVr_tvsubst_FType = TyVar"
25-
unfolding tvVVr_tvsubst_FType_def TyVar_def comp_def tv\<eta>_FType_tvsubst_FType_def by (rule refl)
26-
27-
lemma SSupp_Inj_FType[simp]: "SSupp_FType Inj_FType_1 = {}" unfolding SSupp_FType_def tvVVr_tvsubst_FType_def TyVar_def tv\<eta>_FType_tvsubst_FType_def by simp
28-
lemma IImsupp_Inj_FType[simp]: "IImsupp_FType Inj_FType_1 = {}" unfolding IImsupp_FType_def by simp
29-
lemma SSupp_IImsupp_bound[simp]:
30-
fixes \<rho>::"'tyvar::var \<Rightarrow> 'tyvar FType"
31-
assumes "|SSupp_FType \<rho>| <o |UNIV::'tyvar set|"
32-
shows "|IImsupp_FType \<rho>| <o |UNIV::'tyvar set|"
33-
unfolding IImsupp_FType_def using assms by (auto simp: FType.Un_bound FType.UN_bound FType.set_bd_UNIV)
34-
35-
lemma SSupp_comp_subset_FType:
36-
fixes \<rho> \<rho>'::"'tyvar::var \<Rightarrow> 'tyvar FType"
37-
assumes "|SSupp_FType \<rho>| <o |UNIV::'tyvar set|"
38-
shows "SSupp_FType (tvsubst_FType \<rho> \<circ> \<rho>') \<subseteq> SSupp_FType \<rho> \<union> SSupp_FType \<rho>'"
39-
unfolding SSupp_FType_def tvVVr_tvsubst_FType_def tv\<eta>_FType_tvsubst_FType_def comp_def
40-
apply (unfold TyVar_def[symmetric])
41-
apply (rule subsetI)
42-
apply (unfold mem_Collect_eq)
43-
apply simp
44-
using assms(1) by force
45-
lemma SSupp_comp_bound_FType[simp]:
46-
fixes \<rho> \<rho>'::"'tyvar::var \<Rightarrow> 'tyvar FType"
47-
assumes "|SSupp_FType \<rho>| <o |UNIV::'tyvar set|" "|SSupp_FType \<rho>'| <o |UNIV::'tyvar set|"
48-
shows "|SSupp_FType (tvsubst_FType \<rho> \<circ> \<rho>')| <o |UNIV::'tyvar set|"
49-
using assms SSupp_comp_subset_FType by (metis card_of_subset_bound infinite_class.Un_bound)
50-
51-
lemma Sb_Inj_FType: "Sb_FType Inj_FType_1 = id"
52-
apply (rule ext)
53-
subgoal for x
54-
apply (induction x)
55-
by auto
56-
done
57-
lemma Sb_comp_Inj_FType:
58-
fixes \<rho>::"'tyvar::var \<Rightarrow> 'tyvar FType"
59-
assumes "|SSupp_FType \<rho>| <o |UNIV::'tyvar set|"
60-
shows "Sb_FType \<rho> \<circ> Inj_FType_1 = \<rho>"
61-
using assms by auto
62-
63-
lemma Sb_comp_FType:
64-
fixes \<rho>'' \<rho>'::"'tyvar::var \<Rightarrow> 'tyvar FType"
65-
assumes "|SSupp_FType \<rho>''| <o |UNIV::'tyvar set|" "|SSupp_FType \<rho>'| <o |UNIV::'tyvar set|"
66-
shows "Sb_FType \<rho>'' \<circ> Sb_FType \<rho>' = Sb_FType (Sb_FType \<rho>'' \<circ> \<rho>')"
67-
apply (rule ext)
68-
apply (rule trans[OF comp_apply])
69-
subgoal for x
70-
apply (binder_induction x avoiding: "IImsupp_FType \<rho>''" "IImsupp_FType \<rho>'" "IImsupp_FType (Sb_FType \<rho>'' \<circ> \<rho>')" rule: FType.strong_induct)
71-
using assms by (auto simp: IImsupp_FType_def FType.Un_bound FType.UN_bound FType.set_bd_UNIV)
72-
done
73-
thm Sb_comp_FType[unfolded SSupp_FType_def tvVVr_tvsubst_FType_def[unfolded comp_def] tv\<eta>_FType_tvsubst_FType_def TyVar_def[symmetric]]
74-
lemma Vrs_Inj_FType: "Vrs_FType_1 (Inj_FType_1 a) = {a}"
75-
by simp
76-
77-
lemma Vrs_Sb_FType:
78-
fixes \<rho>'::"'tyvar::var \<Rightarrow> 'tyvar FType"
79-
assumes "|SSupp_FType \<rho>'| <o |UNIV::'tyvar set|"
80-
shows "Vrs_FType_1 (Sb_FType \<rho>' x) = (\<Union>a\<in>Vrs_FType_1 x. Vrs_FType_1 (\<rho>' a))"
81-
proof (binder_induction x avoiding: "IImsupp_FType \<rho>'" rule: FType.strong_induct)
82-
case (TyAll x1 x2)
83-
then show ?case using assms by (auto intro!: FType.IImsupp_Diff[symmetric])
84-
qed (auto simp: assms)
85-
86-
lemma Sb_cong_FType:
87-
fixes \<rho>'' \<rho>'::"'tyvar::var \<Rightarrow> 'tyvar FType"
88-
assumes "|SSupp_FType \<rho>''| <o |UNIV::'tyvar set|" "|SSupp_FType \<rho>'| <o |UNIV::'tyvar set|"
89-
and "\<And>a. a \<in> Vrs_FType_1 t \<Longrightarrow> \<rho>'' a = \<rho>' a"
90-
shows "Sb_FType \<rho>'' t = Sb_FType \<rho>' t"
91-
using assms(3) proof (binder_induction t avoiding: "IImsupp_FType \<rho>''" "IImsupp_FType \<rho>'" rule: FType.strong_induct)
92-
case (TyAll x1 x2)
93-
then show ?case using assms apply (auto simp: FType.permute_id)
94-
by (metis (mono_tags, lifting) CollectI IImsupp_FType_def SSupp_FType_def Un_iff)
95-
qed (auto simp: assms(1-2))
96-
97-
lemma map_is_Sb_FType:
98-
fixes f::"'tyvar::var \<Rightarrow> 'tyvar"
99-
assumes "|supp f| <o |UNIV::'tyvar set|"
100-
shows "vvsubst_FType f = Sb_FType (Inj_FType_1 \<circ> f)"
101-
apply (rule ext)
102-
subgoal for x
103-
proof (binder_induction x avoiding: "imsupp f" rule: FType.strong_induct)
104-
case Bound
105-
then show ?case using imsupp_supp_bound infinite_UNIV assms by blast
106-
next
107-
case (TyAll x1 x2)
108-
then have 1: "x1 \<notin> SSupp_FType (Inj_FType_1 \<circ> f)"
109-
by (simp add: SSupp_FType_def VVr_eq_Var_FType not_in_imsupp_same)
110-
then have "x1 \<notin> IImsupp_FType (Inj_FType_1 \<circ> f)"
111-
unfolding IImsupp_FType_def Un_iff de_Morgan_disj
112-
apply (rule conjI)
113-
apply (insert 1)
114-
apply (erule contrapos_nn)
115-
apply (erule UN_E)
116-
by (metis FType.set(1) TyAll.fresh comp_apply in_imsupp not_in_imsupp_same singletonD)
117-
then show ?case using assms TyAll by (auto simp: FType.SSupp_comp_bound_old)
118-
qed (auto simp: FType.SSupp_comp_bound_old assms)
119-
done
120-
121-
declare [[ML_print_depth=1000]]
122-
123-
local_setup \<open>fold BMV_Monad_Def.register_mrbnf_as_pbmv_monad [@{type_name sum}, @{type_name prod}]\<close>
124-
125-
pbmv_monad "'tv::var FType"
126-
Sbs: tvsubst_FType
127-
Injs: TyVar
128-
Vrs: FVars_FType
129-
bd: natLeq
130-
apply (rule infinite_regular_card_order_natLeq)
131-
apply (rule Sb_Inj_FType)
132-
apply (unfold SSupp_def SSupp_FType_def[unfolded tvVVr_tvsubst_FType_def[unfolded comp_def tv\<eta>_FType_tvsubst_FType_def TyVar_def[symmetric]], symmetric])
133-
apply (rule Sb_comp_Inj_FType; assumption)
134-
apply (rule Sb_comp_FType; assumption)
135-
apply (rule FType.set_bd)
136-
apply (rule Vrs_Inj_FType)
137-
apply (rule Vrs_Sb_FType; assumption)
138-
apply (rule Sb_cong_FType; assumption)
139-
done
140-
print_theorems
141-
142-
mrsbnf "'a::var FType"
143-
apply (rule map_is_Sb_FType; assumption)
144-
done
145-
print_theorems
146-
14724
binder_datatype 'a LM =
14825
Var 'a
14926
| Lst "'a list"

0 commit comments

Comments
 (0)