59 lemmas supp_fn' = lm_fv[simplified supp_fn[symmetric]] |
59 lemmas supp_fn' = lm_fv[simplified supp_fn[symmetric]] |
60 |
60 |
61 lemma |
61 lemma |
62 fixes c::"'a::fs" |
62 fixes c::"'a::fs" |
63 assumes a1: "\<And>name c. P c (Vr name)" |
63 assumes a1: "\<And>name c. P c (Vr name)" |
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)" |
64 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
65 and a3: "\<And>name lm_raw c. \<lbrakk>\<And>d. P d lm_raw\<rbrakk> \<Longrightarrow> P c (Lm name lm_raw)" |
65 and a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
66 shows "P c lm" |
66 shows "P c lm" |
67 proof - |
67 proof - |
68 have "\<And>p. P c (p \<bullet> lm)" |
68 have "\<And>p. P c (p \<bullet> lm)" |
69 apply(induct lm arbitrary: c rule: lm_induct) |
69 apply(induct lm arbitrary: c rule: lm_induct) |
70 apply(simp only: lm_perm) |
70 apply(simp only: lm_perm) |
71 apply(rule a1) |
71 apply(rule a1) |
72 apply(simp only: lm_perm) |
72 apply(simp only: lm_perm) |
73 apply(rule a2) |
73 apply(rule a2) |
74 apply(blast)[1] |
74 apply(blast)[1] |
75 apply(assumption) |
75 apply(assumption) |
76 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm_raw))") |
76 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))") |
77 apply(erule exE) |
77 apply(erule exE) |
78 apply(rule_tac t="p \<bullet> Lm name lm_raw" and |
78 apply(rule_tac t="p \<bullet> Lm name lm" and |
79 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm_raw" in subst) |
79 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst) |
80 apply(simp) |
80 apply(simp) |
81 apply(subst lm_perm) |
81 apply(subst lm_perm) |
82 apply(subst (2) lm_perm) |
82 apply(subst (2) lm_perm) |
83 apply(rule flip_fresh_fresh) |
83 apply(rule flip_fresh_fresh) |
84 apply(simp add: fresh_def) |
84 apply(simp add: fresh_def) |
88 apply(simp add: lm_perm) |
88 apply(simp add: lm_perm) |
89 apply(rule a3) |
89 apply(rule a3) |
90 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
90 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
91 apply(simp) |
91 apply(simp) |
92 apply(simp add: fresh_def) |
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) |
93 apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base) |
94 apply(simp add: supp_Pair finite_supp) |
94 apply(simp add: supp_Pair finite_supp) |
95 apply(blast) |
95 apply(blast) |
96 done |
96 done |
97 then have "P c (0 \<bullet> lm)" by blast |
97 then have "P c (0 \<bullet> lm)" by blast |
98 then show "P c lm" by simp |
98 then show "P c lm" by simp |