41 apply(simp only: de_Morgan_conj) |
41 apply(simp only: de_Morgan_conj) |
42 apply(simp only: Collect_disj_eq) |
42 apply(simp only: Collect_disj_eq) |
43 apply(simp only: infinite_Un) |
43 apply(simp only: infinite_Un) |
44 apply(simp only: Collect_disj_eq) |
44 apply(simp only: Collect_disj_eq) |
45 apply(simp only: supp_def[symmetric]) |
45 apply(simp only: supp_def[symmetric]) |
46 apply(rule_tac t="supp (Lm name lm_raw)" and s="supp (Abs {atom name} lm_raw)" in subst) |
46 apply(rule_tac t="supp (Lm name lm)" and s="supp (Abs {atom name} lm)" in subst) |
47 apply(simp (no_asm) only: supp_def) |
47 apply(simp (no_asm) only: supp_def) |
48 apply(simp only: lm_perm) |
48 apply(simp only: lm_perm) |
49 apply(simp only: permute_ABS) |
49 apply(simp only: permute_ABS) |
50 apply(simp only: lm_eq_iff) |
50 apply(simp only: lm_eq_iff) |
51 apply(simp only: Abs_eq_iff) |
51 apply(simp only: Abs_eq_iff) |
66 by blast |
66 by blast |
67 |
67 |
68 lemma |
68 lemma |
69 assumes a0: "finite (supp c)" |
69 assumes a0: "finite (supp c)" |
70 and a1: "\<And>name c. P c (Vr name)" |
70 and a1: "\<And>name c. P c (Vr name)" |
71 and a2: "\<And>lm_raw1 lm_raw2 c. \<lbrakk>\<And>d. P d lm_raw1; \<And>d. P d lm_raw2\<rbrakk> \<Longrightarrow> P c (Ap lm_raw1 lm_raw2)" |
71 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
72 and a3: "\<And>name lm_raw c. \<lbrakk>\<And>d. P d lm_raw\<rbrakk> \<Longrightarrow> P c (Lm name lm_raw)" |
72 and a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
73 shows "P c lm" |
73 shows "P c lm" |
74 proof - |
74 proof - |
75 have "\<And>p c. P c (p \<bullet> lm)" |
75 have "\<And>p c. P c (p \<bullet> lm)" |
76 apply(induct lm rule: lm_induct) |
76 apply(induct lm rule: lm_induct) |
77 apply(simp only: lm_perm) |
77 apply(simp only: lm_perm) |
78 apply(rule a1) |
78 apply(rule a1) |
79 apply(simp only: lm_perm) |
79 apply(simp only: lm_perm) |
80 apply(rule a2) |
80 apply(rule a2) |
81 apply(assumption) |
81 apply(assumption) |
82 apply(assumption) |
82 apply(assumption) |
83 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm_raw)) |
83 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm)) |
84 \<and> sort_of (atom new) = sort_of (atom name)") |
84 \<and> sort_of (atom new) = sort_of (atom name)") |
85 apply(erule exE) |
85 apply(erule exE) |
86 apply(rule_tac t="(p \<bullet> Lm name lm_raw)" and |
86 apply(rule_tac t="(p \<bullet> Lm name lm)" and |
87 s="((((atom (p \<bullet> name)) \<rightleftharpoons> (atom new)) + p) \<bullet> Lm name lm_raw)" in subst) |
87 s="((((atom (p \<bullet> name)) \<rightleftharpoons> (atom new)) + p) \<bullet> Lm name lm)" in subst) |
88 apply(simp) |
88 apply(simp) |
89 apply(subst lm_perm) |
89 apply(subst lm_perm) |
90 apply(subst (2) lm_perm) |
90 apply(subst (2) lm_perm) |
91 apply(rule swap_fresh_fresh) |
91 apply(rule swap_fresh_fresh) |
92 apply(simp add: fresh_def) |
92 apply(simp add: fresh_def) |
148 apply(simp only: de_Morgan_conj) |
148 apply(simp only: de_Morgan_conj) |
149 apply(simp only: Collect_disj_eq) |
149 apply(simp only: Collect_disj_eq) |
150 apply(simp only: infinite_Un) |
150 apply(simp only: infinite_Un) |
151 apply(simp only: Collect_disj_eq) |
151 apply(simp only: Collect_disj_eq) |
152 (* LAM case *) |
152 (* LAM case *) |
153 apply(rule_tac t="supp (LAM name lam_raw)" and s="supp (Abs {atom name} lam_raw)" in subst) |
153 apply(rule_tac t="supp (LAM name lam)" and s="supp (Abs {atom name} lam)" in subst) |
154 apply(simp (no_asm) only: supp_def) |
154 apply(simp (no_asm) only: supp_def) |
155 apply(simp only: lam_bp_perm) |
155 apply(simp only: lam_bp_perm) |
156 apply(simp only: permute_ABS) |
156 apply(simp only: permute_ABS) |
157 apply(simp only: lam_bp_eq_iff) |
157 apply(simp only: lam_bp_eq_iff) |
158 apply(simp only: Abs_eq_iff) |
158 apply(simp only: Abs_eq_iff) |
160 apply(simp only: alpha_gen) |
160 apply(simp only: alpha_gen) |
161 apply(simp only: supp_eqvt[symmetric]) |
161 apply(simp only: supp_eqvt[symmetric]) |
162 apply(simp only: eqvts) |
162 apply(simp only: eqvts) |
163 apply(simp only: supp_Abs) |
163 apply(simp only: supp_Abs) |
164 (* LET case *) |
164 (* LET case *) |
165 apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \<union> fv_bi bp_raw" in subst) |
165 apply(rule_tac t="supp (LET bp lam)" and s="supp (Abs (bi bp) lam) \<union> fv_bi bp" in subst) |
166 apply(simp (no_asm) only: supp_def) |
166 apply(simp (no_asm) only: supp_def) |
167 apply(simp only: lam_bp_perm) |
167 apply(simp only: lam_bp_perm) |
168 apply(simp only: permute_ABS) |
168 apply(simp only: permute_ABS) |
169 apply(simp only: lam_bp_eq_iff) |
169 apply(simp only: lam_bp_eq_iff) |
170 apply(simp only: eqvts) |
170 apply(simp only: eqvts) |
237 apply(simp only: de_Morgan_conj) |
237 apply(simp only: de_Morgan_conj) |
238 apply(simp only: Collect_disj_eq) |
238 apply(simp only: Collect_disj_eq) |
239 apply(simp only: infinite_Un) |
239 apply(simp only: infinite_Un) |
240 apply(simp only: Collect_disj_eq) |
240 apply(simp only: Collect_disj_eq) |
241 (* LAM case *) |
241 (* LAM case *) |
242 apply(rule_tac t="supp (LAM' name lam'_raw)" and s="supp (Abs {atom name} lam'_raw)" in subst) |
242 apply(rule_tac t="supp (LAM' name lam')" and s="supp (Abs {atom name} lam')" in subst) |
243 apply(simp (no_asm) only: supp_def) |
243 apply(simp (no_asm) only: supp_def) |
244 apply(simp only: lam'_bp'_perm) |
244 apply(simp only: lam'_bp'_perm) |
245 apply(simp only: permute_ABS) |
245 apply(simp only: permute_ABS) |
246 apply(simp only: lam'_bp'_eq_iff) |
246 apply(simp only: lam'_bp'_eq_iff) |
247 apply(simp only: Abs_eq_iff) |
247 apply(simp only: Abs_eq_iff) |
249 apply(simp only: alpha_gen) |
249 apply(simp only: alpha_gen) |
250 apply(simp only: supp_eqvt[symmetric]) |
250 apply(simp only: supp_eqvt[symmetric]) |
251 apply(simp only: eqvts) |
251 apply(simp only: eqvts) |
252 apply(simp only: supp_Abs) |
252 apply(simp only: supp_Abs) |
253 (* LET case *) |
253 (* LET case *) |
254 apply(rule_tac t="supp (LET' bp'_raw lam'_raw)" and |
254 apply(rule_tac t="supp (LET' bp' lam')" and |
255 s="supp (Abs (bi' bp'_raw) (bp'_raw, lam'_raw))" in subst) |
255 s="supp (Abs (bi' bp') (bp', lam'))" in subst) |
256 apply(simp (no_asm) only: supp_def) |
256 apply(simp (no_asm) only: supp_def) |
257 apply(simp only: lam'_bp'_perm) |
257 apply(simp only: lam'_bp'_perm) |
258 apply(simp only: permute_ABS) |
258 apply(simp only: permute_ABS) |
259 apply(simp only: lam'_bp'_eq_iff) |
259 apply(simp only: lam'_bp'_eq_iff) |
260 apply(simp only: Abs_eq_iff) |
260 apply(simp only: Abs_eq_iff) |
323 apply(simp only: de_Morgan_conj) |
323 apply(simp only: de_Morgan_conj) |
324 apply(simp only: Collect_disj_eq) |
324 apply(simp only: Collect_disj_eq) |
325 apply(simp only: infinite_Un) |
325 apply(simp only: infinite_Un) |
326 apply(simp only: Collect_disj_eq) |
326 apply(simp only: Collect_disj_eq) |
327 (* LAM case *) |
327 (* LAM case *) |
328 apply(rule_tac t="supp (Lam name trm'_raw)" and s="supp (Abs {atom name} trm'_raw)" in subst) |
328 apply(rule_tac t="supp (Lam name trm')" and s="supp (Abs {atom name} trm')" in subst) |
329 apply(simp (no_asm) only: supp_def) |
329 apply(simp (no_asm) only: supp_def) |
330 apply(simp only: trm'_pat'_perm) |
330 apply(simp only: trm'_pat'_perm) |
331 apply(simp only: permute_ABS) |
331 apply(simp only: permute_ABS) |
332 apply(simp only: trm'_pat'_eq_iff) |
332 apply(simp only: trm'_pat'_eq_iff) |
333 apply(simp only: Abs_eq_iff) |
333 apply(simp only: Abs_eq_iff) |
335 apply(simp only: alpha_gen) |
335 apply(simp only: alpha_gen) |
336 apply(simp only: supp_eqvt[symmetric]) |
336 apply(simp only: supp_eqvt[symmetric]) |
337 apply(simp only: eqvts) |
337 apply(simp only: eqvts) |
338 apply(simp only: supp_Abs) |
338 apply(simp only: supp_Abs) |
339 (* LET case *) |
339 (* LET case *) |
340 apply(rule_tac t="supp (Let pat'_raw trm'_raw1 trm'_raw2)" |
340 apply(rule_tac t="supp (Let pat' trm'1 trm'2)" |
341 and s="supp (Abs (f pat'_raw) trm'_raw2) \<union> supp trm'_raw1 \<union> fv_f pat'_raw" in subst) |
341 and s="supp (Abs (f pat') trm'2) \<union> supp trm'1 \<union> fv_f pat'" in subst) |
342 apply(simp (no_asm) only: supp_def) |
342 apply(simp (no_asm) only: supp_def) |
343 apply(simp only: trm'_pat'_perm) |
343 apply(simp only: trm'_pat'_perm) |
344 apply(simp only: permute_ABS) |
344 apply(simp only: permute_ABS) |
345 apply(simp only: trm'_pat'_eq_iff) |
345 apply(simp only: trm'_pat'_eq_iff) |
346 apply(simp only: eqvts) |
346 apply(simp only: eqvts) |
458 apply(simp only: de_Morgan_conj) |
458 apply(simp only: de_Morgan_conj) |
459 apply(simp only: Collect_disj_eq) |
459 apply(simp only: Collect_disj_eq) |
460 apply(simp only: infinite_Un) |
460 apply(simp only: infinite_Un) |
461 apply(simp only: Collect_disj_eq) |
461 apply(simp only: Collect_disj_eq) |
462 (* All case *) |
462 (* All case *) |
463 apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst) |
463 apply(rule_tac t="supp (All fun t)" and s="supp (Abs (atom ` fun) t)" in subst) |
464 apply(simp (no_asm) only: supp_def) |
464 apply(simp (no_asm) only: supp_def) |
465 apply(simp only: t_tyS_perm) |
465 apply(simp only: t_tyS_perm) |
466 apply(simp only: permute_ABS) |
466 apply(simp only: permute_ABS) |
467 apply(simp only: t_tyS_eq_iff) |
467 apply(simp only: t_tyS_eq_iff) |
468 apply(simp only: Abs_eq_iff) |
468 apply(simp only: Abs_eq_iff) |