56 apply(simp only: supp_Abs) |
56 apply(simp only: supp_Abs) |
57 done |
57 done |
58 |
58 |
59 lemmas supp_fn' = lm_fv[simplified supp_fn[symmetric]] |
59 lemmas supp_fn' = lm_fv[simplified supp_fn[symmetric]] |
60 |
60 |
61 lemma obtain_atom_ex: |
|
62 assumes fin: "finite (supp x)" |
|
63 shows "\<exists>a. a \<sharp> x \<and> sort_of a = s" |
|
64 using obtain_atom[OF fin] |
|
65 unfolding fresh_def |
|
66 by blast |
|
67 |
|
68 lemma |
61 lemma |
69 assumes a0: "finite (supp c)" |
62 fixes c::"'a::fs" |
70 and a1: "\<And>name c. P c (Vr name)" |
63 assumes a1: "\<And>name c. P c (Vr name)" |
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)" |
64 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)" |
72 and a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
65 and a3: "\<And>name lm_raw c. \<lbrakk>\<And>d. P d lm_raw\<rbrakk> \<Longrightarrow> P c (Lm name lm_raw)" |
73 shows "P c lm" |
66 shows "P c lm" |
74 proof - |
67 proof - |
75 have "\<And>p c. P c (p \<bullet> lm)" |
68 have "\<And>p. P c (p \<bullet> lm)" |
76 apply(induct lm rule: lm_induct) |
69 apply(induct lm arbitrary: c rule: lm_induct) |
77 apply(simp only: lm_perm) |
70 apply(simp only: lm_perm) |
78 apply(rule a1) |
71 apply(rule a1) |
79 apply(simp only: lm_perm) |
72 apply(simp only: lm_perm) |
80 apply(rule a2) |
73 apply(rule a2) |
|
74 apply(blast)[1] |
81 apply(assumption) |
75 apply(assumption) |
82 apply(assumption) |
76 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)") |
|
85 apply(erule exE) |
77 apply(erule exE) |
86 apply(rule_tac t="(p \<bullet> Lm name lm)" and |
78 apply(rule_tac t="p \<bullet> Lm name lm_raw" and |
87 s="((((atom (p \<bullet> name)) \<rightleftharpoons> (atom new)) + p) \<bullet> Lm name lm)" in subst) |
79 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm_raw" in subst) |
88 apply(simp) |
80 apply(simp) |
89 apply(subst lm_perm) |
81 apply(subst lm_perm) |
90 apply(subst (2) lm_perm) |
82 apply(subst (2) lm_perm) |
91 apply(rule swap_fresh_fresh) |
83 apply(rule flip_fresh_fresh) |
92 apply(simp add: fresh_def) |
84 apply(simp add: fresh_def) |
93 apply(simp only: supp_fn') |
85 apply(simp only: supp_fn') |
94 apply(simp) |
86 apply(simp) |
95 apply(simp add: fresh_Pair) |
87 apply(simp add: fresh_Pair) |
96 apply(simp add: lm_perm) |
88 apply(simp add: lm_perm) |
97 apply(rule a3) |
89 apply(rule a3) |
98 apply(drule_tac x="(atom (p \<bullet> name) \<rightleftharpoons> atom new) + p" in meta_spec) |
90 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
99 apply(simp) |
91 apply(simp) |
100 sorry (* use at_set_avoiding *) |
92 apply(simp add: fresh_def) |
|
93 apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm_raw))" in obtain_at_base) |
|
94 apply(simp add: supp_Pair finite_supp) |
|
95 apply(blast) |
|
96 done |
101 then have "P c (0 \<bullet> lm)" by blast |
97 then have "P c (0 \<bullet> lm)" by blast |
102 then show "P c lm" by simp |
98 then show "P c lm" by simp |
103 qed |
99 qed |
104 |
100 |
105 |
101 |