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 |
50 |
50 |
51 local_setup {* |
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}) |
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 *} |
53 *} |
54 |
54 |
55 (* |
55 (*local_setup {* |
56 local_setup {* |
|
57 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}) |
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}) |
58 *} |
57 *} |
59 print_theorems |
58 print_theorems |
60 |
59 |
61 local_setup {* |
60 local_setup {* |
62 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}) |
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}) |
63 *} |
62 *} |
64 print_theorems |
63 print_theorems |
65 *) |
64 *) |
66 |
65 |
67 lemma alpha1_eqvt: |
|
68 "(rtrm1 \<approx>1 rtrm1a \<longrightarrow> (p \<bullet> rtrm1) \<approx>1 (p \<bullet> rtrm1a)) \<and> |
|
69 (bp \<approx>1b bpa \<longrightarrow> (p \<bullet> bp) \<approx>1b (p \<bullet> bpa)) \<and> |
|
70 (alpha_bv1 a b c \<longrightarrow> alpha_bv1 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))" |
|
71 by (tactic {* alpha_eqvt_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms alpha1_inj permute_rtrm1_permute_bp.simps} @{context} 1 *}) |
|
72 |
|
73 (* |
|
74 local_setup {* |
66 local_setup {* |
75 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), |
67 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), |
76 build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} ctxt) ctxt)) *}*) |
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)) *} |
77 |
69 |
78 lemma alpha1_eqvt_proper[eqvt]: |
70 lemma alpha1_eqvt_proper[eqvt]: |
79 "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))" |
71 "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))" |
80 "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))" |
72 "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))" |
81 apply (simp_all only: eqvts) |
73 apply (simp_all only: eqvts) |
90 apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"]) |
82 apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"]) |
91 apply (simp_all only: alpha1_eqvt) |
83 apply (simp_all only: alpha1_eqvt) |
92 done |
84 done |
93 thm eqvts_raw(1) |
85 thm eqvts_raw(1) |
94 |
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 |
95 lemma alpha1_equivp: |
91 lemma alpha1_equivp: |
96 "equivp alpha_rtrm1" |
92 "equivp alpha_rtrm1" |
97 "equivp alpha_bp" |
93 "equivp alpha_bp" |
98 sorry |
94 sorry |
99 |
95 |
100 (* |
96 (* |
101 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
97 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
102 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{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)) *} |
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)) *} |
103 thm alpha1_equivp |
99 thm alpha1_equivp*) |
104 *) |
|
105 |
100 |
106 local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] |
101 local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] |
107 (rtac @{thm alpha1_equivp(1)} 1) *} |
102 (rtac @{thm alpha1_equivp(1)} 1) *} |
108 |
103 |
109 local_setup {* |
104 local_setup {* |
136 @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *} |
131 @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *} |
137 |
132 |
138 lemmas |
133 lemmas |
139 permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] |
134 permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] |
140 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
135 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
141 and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt(1)[quot_lifted] |
136 and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt[quot_lifted] |
142 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
137 and alpha1_INJ = alpha1_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] |
143 |
138 |
144 lemma supports: |
139 lemma supports: |
145 "(supp (atom x)) supports (Vr1 x)" |
140 "(supp (atom x)) supports (Vr1 x)" |
146 "(supp t \<union> supp s) supports (Ap1 t s)" |
141 "(supp t \<union> supp s) supports (Ap1 t s)" |
147 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
142 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
148 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
143 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
149 (* "{} supports BUnit"*) |
144 "{} supports BUnit" |
150 "(supp (atom x)) supports (BVr x)" |
145 "(supp (atom x)) supports (BVr x)" |
151 (* "(supp a \<union> supp b) supports (BPr a b)"*) |
146 "(supp a \<union> supp b) supports (BPr a b)" |
152 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *}) |
147 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *}) |
153 done |
148 done |
154 |
149 |
155 prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *} |
150 prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *} |
156 apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *}) |
151 apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *}) |
195 "(\<exists>x. Q \<and> P x \<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))" |
196 "(\<exists>x. Q \<and> P x \<and> Z x \<and> W x) = (Q \<and> (\<exists>x. P x \<and> Z x \<and> W 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))" |
197 apply (blast)+ |
192 apply (blast)+ |
198 done |
193 done |
199 |
194 |
200 lemma "(Abs bs (x, x') = Abs cs (y, y')) = (\<exists>p. (bs, x) \<approx>gen op = supp p (cs, y) \<and> (bs, x') \<approx>gen op = supp p (cs, y'))" |
|
201 thm Abs_eq_iff |
|
202 apply (simp add: Abs_eq_iff) |
|
203 apply (rule arg_cong[of _ _ "Ex"]) |
|
204 apply (rule ext) |
|
205 apply (simp only: alpha_gen) |
|
206 apply (simp only: supp_Pair eqvts) |
|
207 apply rule |
|
208 apply (erule conjE)+ |
|
209 oops |
|
210 |
|
211 lemma "(f (p \<bullet> bp), p \<bullet> bp) \<approx>gen op = f pi (f bp, bp) = False" |
|
212 apply (simp add: alpha_gen fresh_star_def) |
|
213 oops |
|
214 |
|
215 (* TODO: permute_ABS should be in eqvt? *) |
|
216 |
|
217 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}" |
195 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}" |
218 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
196 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
219 |
197 |
220 lemma " |
|
221 {a\<Colon>atom. infinite ({b\<Colon>atom. \<not> (\<exists>pi\<Colon>perm. P pi a b \<and> Q pi a b)})} = |
|
222 {a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. P p a b)}} \<union> |
|
223 {a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. Q p a b)}}" |
|
224 oops |
|
225 |
|
226 lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)" |
198 lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)" |
227 by (simp add: finite_Un) |
199 by (simp add: finite_Un) |
228 |
200 |
229 |
|
230 |
|
231 lemma supp_fv_let: |
201 lemma supp_fv_let: |
232 assumes sa : "fv_bp bp = supp bp" |
202 assumes sa : "fv_bp bp = supp bp" |
233 shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb\<rbrakk> |
203 shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\<rbrakk> |
234 \<Longrightarrow> supp (Lt1 bp ta tb) = fv_trm1 (Lt1 bp ta tb)" |
204 \<Longrightarrow> supp (Lt1 bp ta tb) = supp ta \<union> (supp (bp, tb) - supp bp)" |
235 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv]) |
|
236 apply simp |
|
237 apply(fold supp_Abs) |
205 apply(fold supp_Abs) |
238 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
206 apply(simp (no_asm) only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
239 apply(simp (no_asm) only: supp_def) |
207 apply(simp (no_asm) only: supp_def) |
240 apply(simp only: permute_set_eq permute_trm1) |
208 apply(simp only: permute_set_eq permute_trm1) |
241 apply(simp only: alpha1_INJ) |
209 apply(simp only: alpha1_INJ alpha_bp_eq) |
242 apply(simp only: ex_out) |
210 apply(simp only: ex_out) |
243 apply(simp only: Collect_neg_conj) |
211 apply(simp only: Collect_neg_conj) |
244 apply(simp only: permute_ABS) |
212 apply(simp only: permute_ABS) |
245 apply(simp only: Abs_eq_iff) |
213 apply(simp only: Abs_eq_iff) |
246 apply(simp only: alpha_gen fv_eq_bv supp_Pair) |
214 apply(simp only: alpha_gen supp_Pair split_conv eqvts) |
247 apply(simp only: inf_or[symmetric]) |
215 apply(simp only: inf_or[symmetric]) |
248 apply(simp only: Collect_disj_eq) |
216 apply(simp only: Collect_disj_eq) |
249 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
217 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) |
250 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric]) |
218 apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric]) |
251 apply(induct bp) |
219 apply (simp only: eqvts Pair_eq) |
252 apply(simp_all only: TrueI) |
220 done |
253 apply(simp_all only: permute_trm1) |
|
254 apply(simp_all only: bv1.simps) |
|
255 apply(simp_all only: alpha1_INJ) (* Doesn't look true... *) |
|
256 apply(simp) |
|
257 sorry |
|
258 |
|
259 lemma |
|
260 "(\<not> (\<exists>p. (a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)} = supp tb - {atom name} \<and> |
|
261 ({atom (p \<bullet> (a \<rightleftharpoons> b) \<bullet> name)} = {atom name}) \<and> |
|
262 ((a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)}) \<sharp>* p \<and> |
|
263 p \<bullet> (a \<rightleftharpoons> b) \<bullet> tb = tb)) = |
|
264 (\<not> (\<exists>p. (a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)} = supp tb - {atom name} \<and> |
|
265 ((a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)}) \<sharp>* p \<and> |
|
266 p \<bullet> (a \<rightleftharpoons> b) \<bullet> tb = tb))" |
|
267 apply simp |
|
268 apply rule |
|
269 prefer 2 |
|
270 apply (meson)[2] |
|
271 apply clarify |
|
272 apply (erule_tac x="p" in allE) |
|
273 apply simp |
|
274 apply (simp add: atom_eqvt[symmetric]) |
|
275 sorry |
|
276 |
|
277 thm trm1_bp_inducts |
|
278 |
221 |
279 lemma supp_fv: |
222 lemma supp_fv: |
280 "supp t = fv_trm1 t" |
223 "supp t = fv_trm1 t" |
281 "supp b = fv_bp b" |
224 "supp b = fv_bp b" |
282 apply(induct t and b rule: trm1_bp_inducts) |
225 apply(induct t and b rule: trm1_bp_inducts) |
290 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) |
233 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) |
291 apply(simp add: alpha1_INJ) |
234 apply(simp add: alpha1_INJ) |
292 apply(simp add: Abs_eq_iff) |
235 apply(simp add: Abs_eq_iff) |
293 apply(simp add: alpha_gen.simps) |
236 apply(simp add: alpha_gen.simps) |
294 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
237 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
295 defer |
238 apply(simp add: supp_fv_let fv_trm1 fv_eq_bv supp_Pair) |
296 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
239 apply blast |
|
240 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
241 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
297 apply(simp only: supp_at_base[simplified supp_def]) |
242 apply(simp only: supp_at_base[simplified supp_def]) |
298 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |
243 apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1 alpha1_INJ[simplified alpha_bp_eq]) |
299 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) |
244 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
300 (*apply(rule supp_fv_let) apply(simp_all)*) |
|
301 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \<union> supp(rtrm11)") |
|
302 (*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> supp(rtrm11)")*) |
|
303 apply(simp add: supp_Abs fv_trm1 supp_Pair Un_Diff Un_assoc fv_eq_bv) |
|
304 apply(blast) (* Un_commute in a good place *) |
|
305 apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1) |
|
306 apply(simp only: alpha1_INJ permute_ABS permute_prod.simps Abs_eq_iff) |
|
307 apply(simp only: ex_out) |
|
308 apply(simp only: Un_commute) |
|
309 apply(simp only: alpha_bp_eq fv_eq_bv) |
|
310 apply(simp only: alpha_gen fv_eq_bv supp_Pair) |
|
311 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
|
312 apply(simp only: ex_out) |
|
313 apply(simp only: Collect_neg_conj finite_Un Diff_cancel) |
|
314 apply(simp) |
|
315 apply(fold supp_def) |
245 apply(fold supp_def) |
316 sorry |
246 apply simp |
|
247 done |
317 |
248 |
318 lemma trm1_supp: |
249 lemma trm1_supp: |
319 "supp (Vr1 x) = {atom x}" |
250 "supp (Vr1 x) = {atom x}" |
320 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
251 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
321 "supp (Lm1 x t) = (supp t) - {atom x}" |
252 "supp (Lm1 x t) = (supp t) - {atom x}" |