diff -r 2406350c358f -r 8b5a1ad60487 Nominal/ExLam.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/ExLam.thy Tue Mar 23 08:51:43 2010 +0100 @@ -0,0 +1,91 @@ +theory ExLam +imports "Parser" +begin + +atom_decl name + +nominal_datatype lm = + Vr "name" +| Ap "lm" "lm" +| Lm x::"name" l::"lm" bind x in l + +lemmas supp_fn' = lm.fv[simplified lm.supp] + +lemma + fixes c::"'a::fs" + assumes a1: "\<And>name c. P c (Vr name)" + and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" + and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" + shows "P c lm" +proof - + have "\<And>p. P c (p \<bullet> lm)" + apply(induct lm arbitrary: c rule: lm.induct) + apply(simp only: lm.perm) + apply(rule a1) + apply(simp only: lm.perm) + apply(rule a2) + apply(blast)[1] + apply(assumption) + apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))") + defer + apply(simp add: fresh_def) + apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base) + apply(simp add: supp_Pair finite_supp) + apply(blast) + apply(erule exE) + apply(rule_tac t="p \<bullet> Lm name lm" and + s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst) + apply(simp del: lm.perm) + apply(subst lm.perm) + apply(subst (2) lm.perm) + apply(rule flip_fresh_fresh) + apply(simp add: fresh_def) + apply(simp only: supp_fn') + apply(simp) + apply(simp add: fresh_Pair) + apply(simp) + apply(rule a3) + apply(simp add: fresh_Pair) + apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) + apply(simp) + done + then have "P c (0 \<bullet> lm)" by blast + then show "P c lm" by simp +qed + + +lemma + fixes c::"'a::fs" + assumes a1: "\<And>name c. P c (Vr name)" + and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" + and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" + shows "P c lm" +proof - + have "\<And>p. P c (p \<bullet> lm)" + apply(induct lm arbitrary: c rule: lm.induct) + apply(simp only: lm.perm) + apply(rule a1) + apply(simp only: lm.perm) + apply(rule a2) + apply(blast)[1] + apply(assumption) + thm at_set_avoiding + apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q") + apply(erule exE) + apply(rule_tac t="p \<bullet> Lm name lm" and + s="q \<bullet> p \<bullet> Lm name lm" in subst) + defer + apply(simp add: lm.perm) + apply(rule a3) + apply(simp add: eqvts fresh_star_def) + apply(drule_tac x="q + p" in meta_spec) + apply(simp) + sorry + then have "P c (0 \<bullet> lm)" by blast + then show "P c lm" by simp +qed + +end + + +