|
1 theory Term1 |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 section {*** lets with binding patterns ***} |
|
8 |
|
9 datatype rtrm1 = |
|
10 rVr1 "name" |
|
11 | rAp1 "rtrm1" "rtrm1" |
|
12 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
|
13 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
|
14 and bp = |
|
15 BUnit |
|
16 | BVr "name" |
|
17 | BPr "bp" "bp" |
|
18 |
|
19 print_theorems |
|
20 |
|
21 (* to be given by the user *) |
|
22 |
|
23 primrec |
|
24 bv1 |
|
25 where |
|
26 "bv1 (BUnit) = {}" |
|
27 | "bv1 (BVr x) = {atom x}" |
|
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
|
29 |
|
30 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *} |
|
31 thm permute_rtrm1_permute_bp.simps |
|
32 |
|
33 local_setup {* |
|
34 snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") |
|
35 [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]], |
|
36 [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *} |
|
37 |
|
38 notation |
|
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
|
40 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
|
41 thm alpha_rtrm1_alpha_bp_alpha_bv1.intros |
|
42 (*thm fv_rtrm1_fv_bp.simps[no_vars]*) |
|
43 |
|
44 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp_alpha_bv1.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases alpha_bv1.cases} ctxt)) ctxt)) *} |
|
45 thm alpha1_inj |
|
46 |
|
47 local_setup {* |
|
48 snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] (build_eqvts_tac @{thm rtrm1_bp.inducts(2)} @{thms bv1.simps permute_rtrm1_permute_bp.simps} @{context})) |
|
49 *} |
|
50 |
|
51 local_setup {* |
|
52 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps} @{context}) |
|
53 *} |
|
54 |
|
55 (*local_setup {* |
|
56 snd o build_eqvts @{binding fv_rtrm1_fv_bv1_eqvt} [@{term fv_rtrm1}, @{term fv_bv1}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bv1.simps permute_rtrm1_permute_bp.simps} @{context}) |
|
57 *} |
|
58 print_theorems |
|
59 |
|
60 local_setup {* |
|
61 snd o build_eqvts @{binding fv_bp_eqvt} [@{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.inducts(2)} @{thms fv_rtrm1_fv_bv1.simps fv_bp.simps permute_rtrm1_permute_bp.simps} @{context}) |
|
62 *} |
|
63 print_theorems |
|
64 *) |
|
65 |
|
66 local_setup {* |
|
67 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), |
|
68 build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms permute_rtrm1_permute_bp.simps alpha1_inj} ctxt 1) ctxt) ctxt)) *} |
|
69 |
|
70 lemma alpha1_eqvt_proper[eqvt]: |
|
71 "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))" |
|
72 "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))" |
|
73 apply (simp_all only: eqvts) |
|
74 apply rule |
|
75 apply (simp_all add: alpha1_eqvt) |
|
76 apply (subst permute_minus_cancel(2)[symmetric,of "t" "pi"]) |
|
77 apply (subst permute_minus_cancel(2)[symmetric,of "s" "pi"]) |
|
78 apply (simp_all only: alpha1_eqvt) |
|
79 apply rule |
|
80 apply (simp_all add: alpha1_eqvt) |
|
81 apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"]) |
|
82 apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"]) |
|
83 apply (simp_all only: alpha1_eqvt) |
|
84 done |
|
85 thm eqvts_raw(1) |
|
86 |
|
87 lemma "(b \<approx>1 a \<longrightarrow> a \<approx>1 b) \<and> (x \<approx>1b y \<longrightarrow> y \<approx>1b x) \<and> (alpha_bv1 x y \<longrightarrow> alpha_bv1 y x)" |
|
88 apply (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} @{context} 1 *}) |
|
89 done |
|
90 |
|
91 lemma alpha1_equivp: |
|
92 "equivp alpha_rtrm1" |
|
93 "equivp alpha_bp" |
|
94 sorry |
|
95 |
|
96 (* |
|
97 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
|
98 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} |
|
99 thm alpha1_equivp*) |
|
100 |
|
101 local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] |
|
102 (rtac @{thm alpha1_equivp(1)} 1) *} |
|
103 |
|
104 local_setup {* |
|
105 (fn ctxt => ctxt |
|
106 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) |
|
107 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) |
|
108 |> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1})) |
|
109 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
|
110 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
|
111 *} |
|
112 print_theorems |
|
113 |
|
114 local_setup {* snd o prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}] |
|
115 (fn _ => Skip_Proof.cheat_tac @{theory}) *} |
|
116 local_setup {* snd o prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}] |
|
117 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
|
118 local_setup {* snd o prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}] |
|
119 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
|
120 local_setup {* snd o prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}] |
|
121 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
|
122 local_setup {* snd o prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}] |
|
123 (fn _ => Skip_Proof.cheat_tac @{theory}) *} |
|
124 local_setup {* snd o prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}] |
|
125 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
|
126 |
|
127 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
|
128 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
|
129 |
|
130 setup {* define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})] |
|
131 @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *} |
|
132 |
|
133 lemmas |
|
134 permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] |
|
135 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
|
136 and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt[quot_lifted] |
|
137 and alpha1_INJ = alpha1_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] |
|
138 |
|
139 lemma supports: |
|
140 "(supp (atom x)) supports (Vr1 x)" |
|
141 "(supp t \<union> supp s) supports (Ap1 t s)" |
|
142 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
|
143 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
|
144 "{} supports BUnit" |
|
145 "(supp (atom x)) supports (BVr x)" |
|
146 "(supp a \<union> supp b) supports (BPr a b)" |
|
147 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *}) |
|
148 done |
|
149 |
|
150 prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *} |
|
151 apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *}) |
|
152 done |
|
153 |
|
154 instance trm1 and bp :: fs |
|
155 apply default |
|
156 apply (simp_all add: rtrm1_bp_fs) |
|
157 done |
|
158 |
|
159 lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp" |
|
160 apply(induct bp rule: trm1_bp_inducts(2)) |
|
161 apply(simp_all) |
|
162 done |
|
163 |
|
164 lemma fv_eq_bv: "fv_bp = bv1" |
|
165 apply(rule ext) |
|
166 apply(rule fv_eq_bv_pre) |
|
167 done |
|
168 |
|
169 lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}" |
|
170 apply auto |
|
171 apply (rule_tac x="(x \<rightleftharpoons> a)" in exI) |
|
172 apply auto |
|
173 done |
|
174 |
|
175 lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)" |
|
176 apply rule |
|
177 apply (induct a b rule: alpha_rtrm1_alpha_bp_alpha_bv1.inducts(2)) |
|
178 apply (simp_all add: equivp_reflp[OF alpha1_equivp(2)]) |
|
179 done |
|
180 |
|
181 lemma alpha_bp_eq: "alpha_bp = (op =)" |
|
182 apply (rule ext)+ |
|
183 apply (rule alpha_bp_eq_eq) |
|
184 done |
|
185 |
|
186 lemma ex_out: |
|
187 "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))" |
|
188 "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))" |
|
189 "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))" |
|
190 "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))" |
|
191 "(\<exists>x. Q \<and> P x \<and> Z x \<and> W x) = (Q \<and> (\<exists>x. P x \<and> Z x \<and> W x))" |
|
192 apply (blast)+ |
|
193 done |
|
194 |
|
195 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}" |
|
196 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
|
197 |
|
198 lemma supp_fv_let: |
|
199 assumes sa : "fv_bp bp = supp bp" |
|
200 shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\<rbrakk> |
|
201 \<Longrightarrow> supp (Lt1 bp ta tb) = supp ta \<union> (supp (bp, tb) - supp bp)" |
|
202 apply(fold supp_Abs) |
|
203 apply(simp (no_asm) only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
|
204 apply(simp (no_asm) only: supp_def) |
|
205 apply(simp only: permute_set_eq permute_trm1) |
|
206 apply(simp only: alpha1_INJ alpha_bp_eq) |
|
207 apply(simp only: ex_out) |
|
208 apply(simp only: Collect_neg_conj) |
|
209 apply(simp only: permute_ABS) |
|
210 apply(simp only: Abs_eq_iff) |
|
211 apply(simp only: alpha_gen supp_Pair split_conv eqvts) |
|
212 apply(simp only: infinite_Un) |
|
213 apply(simp only: Collect_disj_eq) |
|
214 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
|
215 apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric]) |
|
216 apply (simp only: eqvts Pair_eq) |
|
217 done |
|
218 |
|
219 lemma supp_fv: |
|
220 "supp t = fv_trm1 t" |
|
221 "supp b = fv_bp b" |
|
222 apply(induct t and b rule: trm1_bp_inducts) |
|
223 apply(simp_all) |
|
224 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
225 apply(simp only: supp_at_base[simplified supp_def]) |
|
226 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
227 apply(simp add: Collect_imp_eq Collect_neg_eq Un_commute) |
|
228 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") |
|
229 apply(simp add: supp_Abs fv_trm1) |
|
230 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) |
|
231 apply(simp add: alpha1_INJ) |
|
232 apply(simp add: Abs_eq_iff) |
|
233 apply(simp add: alpha_gen.simps) |
|
234 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
|
235 apply(simp add: supp_fv_let fv_trm1 fv_eq_bv supp_Pair) |
|
236 apply blast |
|
237 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
238 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
239 apply(simp only: supp_at_base[simplified supp_def]) |
|
240 apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1 alpha1_INJ[simplified alpha_bp_eq]) |
|
241 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
|
242 apply(fold supp_def) |
|
243 apply simp |
|
244 done |
|
245 |
|
246 lemma trm1_supp: |
|
247 "supp (Vr1 x) = {atom x}" |
|
248 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
|
249 "supp (Lm1 x t) = (supp t) - {atom x}" |
|
250 "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)" |
|
251 by (simp_all add: supp_fv fv_trm1 fv_eq_bv) |
|
252 |
|
253 lemma trm1_induct_strong: |
|
254 assumes "\<And>name b. P b (Vr1 name)" |
|
255 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
|
256 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
|
257 and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)" |
|
258 shows "P a rtrma" |
|
259 sorry |
|
260 |
|
261 end |