10 rVr1 "name" |
10 rVr1 "name" |
11 | rAp1 "rtrm1" "rtrm1" |
11 | rAp1 "rtrm1" "rtrm1" |
12 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
12 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
13 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
13 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
14 and bp = |
14 and bp = |
15 BUnit |
15 (* BUnit*) |
16 | BVr "name" |
16 BVr "name" |
17 | BPr "bp" "bp" |
17 (*| BPr "bp" "bp"*) |
18 |
18 |
19 print_theorems |
19 print_theorems |
20 |
20 |
21 (* to be given by the user *) |
21 (* to be given by the user *) |
22 |
22 |
23 primrec |
23 primrec |
24 bv1 |
24 bv1 |
25 where |
25 where |
26 "bv1 (BUnit) = {}" |
26 (* "bv1 (BUnit) = {}"*) |
27 | "bv1 (BVr x) = {atom x}" |
27 "bv1 (BVr x) = {atom x}" |
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
28 (*| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"*) |
29 |
29 |
30 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *} |
30 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *} |
31 thm permute_rtrm1_permute_bp.simps |
31 thm permute_rtrm1_permute_bp.simps |
32 |
32 |
33 local_setup {* |
33 local_setup {* |
34 snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") |
34 snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") |
35 [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]], |
35 [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]], |
36 [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *} |
36 [[](*, [], []*)]] [(@{term bv1}, 1, [(*[],*) [0](*, [0, 1]*)])] *} |
37 |
37 |
38 notation |
38 notation |
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
40 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
40 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
41 thm alpha_rtrm1_alpha_bp_alpha_bv1.intros |
41 thm alpha_rtrm1_alpha_bp_alpha_bv1.intros |
42 thm fv_rtrm1_fv_bp.simps[no_vars] |
42 (*thm fv_rtrm1_fv_bp.simps[no_vars]*) |
43 |
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)) *} |
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 |
45 thm alpha1_inj |
46 |
46 |
47 local_setup {* |
47 local_setup {* |
132 lemma supports: |
132 lemma supports: |
133 "(supp (atom x)) supports (Vr1 x)" |
133 "(supp (atom x)) supports (Vr1 x)" |
134 "(supp t \<union> supp s) supports (Ap1 t s)" |
134 "(supp t \<union> supp s) supports (Ap1 t s)" |
135 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
135 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
136 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
136 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
137 "{} supports BUnit" |
137 (* "{} supports BUnit"*) |
138 "(supp (atom x)) supports (BVr x)" |
138 "(supp (atom x)) supports (BVr x)" |
139 "(supp a \<union> supp b) supports (BPr a b)" |
139 (* "(supp a \<union> supp b) supports (BPr a b)"*) |
140 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *}) |
140 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *}) |
141 done |
141 done |
142 |
142 |
143 prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *} |
143 prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *} |
144 apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *}) |
144 apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *}) |
213 |
213 |
214 lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)" |
214 lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)" |
215 by (simp add: finite_Un) |
215 by (simp add: finite_Un) |
216 |
216 |
217 |
217 |
|
218 |
218 lemma supp_fv_let: |
219 lemma supp_fv_let: |
219 assumes sa : "fv_bp bp = supp bp" |
220 assumes sa : "fv_bp bp = supp bp" |
220 shows "\<lbrakk>fv_trm1 trm11 = supp trm11; fv_trm1 trm12 = supp trm12\<rbrakk> |
221 shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb\<rbrakk> |
221 \<Longrightarrow> supp (Lt1 bp trm11 trm12) = fv_trm1 (Lt1 bp trm11 trm12)" |
222 \<Longrightarrow> supp (Lt1 bp ta tb) = fv_trm1 (Lt1 bp ta tb)" |
222 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv]) |
223 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv]) |
223 apply simp |
224 apply simp |
224 apply(fold supp_Abs) |
225 apply(fold supp_Abs) |
225 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
226 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
226 apply(simp (no_asm) only: supp_def) |
227 apply(simp (no_asm) only: supp_def) |
233 apply(simp only: alpha_gen fv_eq_bv supp_Pair) |
234 apply(simp only: alpha_gen fv_eq_bv supp_Pair) |
234 apply(simp only: inf_or[symmetric]) |
235 apply(simp only: inf_or[symmetric]) |
235 apply(simp only: Collect_disj_eq) |
236 apply(simp only: Collect_disj_eq) |
236 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
237 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
237 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
238 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
238 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
239 apply(induct bp) |
239 apply(simp only: HOL.imp_disj2[symmetric] HOL.not_ex[symmetric] HOL.disj_not1[symmetric] HOL.de_Morgan_conj[symmetric]) |
240 apply(simp_all only: TrueI) |
|
241 apply(simp_all only: permute_trm1) |
|
242 apply(simp_all only: bv1.simps) |
|
243 apply(simp_all only: alpha1_INJ) (* Doesn't look true... *) |
|
244 apply(simp) |
|
245 sorry |
|
246 |
|
247 lemma |
|
248 "(\<not> (\<exists>p. (a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)} = supp tb - {atom name} \<and> |
|
249 ({atom (p \<bullet> (a \<rightleftharpoons> b) \<bullet> name)} = {atom name}) \<and> |
|
250 ((a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)}) \<sharp>* p \<and> |
|
251 p \<bullet> (a \<rightleftharpoons> b) \<bullet> tb = tb)) = |
|
252 (\<not> (\<exists>p. (a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)} = supp tb - {atom name} \<and> |
|
253 ((a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)}) \<sharp>* p \<and> |
|
254 p \<bullet> (a \<rightleftharpoons> b) \<bullet> tb = tb))" |
|
255 apply simp |
|
256 apply rule |
|
257 prefer 2 |
|
258 apply (meson)[2] |
|
259 apply clarify |
|
260 apply (erule_tac x="p" in allE) |
|
261 apply simp |
|
262 apply (simp add: atom_eqvt[symmetric]) |
240 sorry |
263 sorry |
241 |
264 |
242 lemma supp_fv: |
265 lemma supp_fv: |
243 "supp t = fv_trm1 t" |
266 "supp t = fv_trm1 t" |
244 "supp b = fv_bp b" |
267 "supp b = fv_bp b" |