diff -r 20221ec06cba -r 892fcdb96c96 Nominal/LamEx.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/LamEx.thy Tue Mar 23 08:22:48 2010 +0100 @@ -0,0 +1,91 @@ +theory LamEx +imports "Parser" "../Attic/Prove" +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: "\name c. P c (Vr name)" + and a2: "\lm1 lm2 c. \\d. P d lm1; \d. P d lm2\ \ P c (Ap lm1 lm2)" + and a3: "\name lm c. \atom name \ c; \d. P d lm\ \ P c (Lm name lm)" + shows "P c lm" +proof - + have "\p. P c (p \ 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 "\new::name. (atom new) \ (c, Lm (p \ name) (p \ lm))") + defer + apply(simp add: fresh_def) + apply(rule_tac X="supp (c, Lm (p \ name) (p \ lm))" in obtain_at_base) + apply(simp add: supp_Pair finite_supp) + apply(blast) + apply(erule exE) + apply(rule_tac t="p \ Lm name lm" and + s="(((p \ name) \ new) + p) \ 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 \ name) \ new) + p" in meta_spec) + apply(simp) + done + then have "P c (0 \ lm)" by blast + then show "P c lm" by simp +qed + + +lemma + fixes c::"'a::fs" + assumes a1: "\name c. P c (Vr name)" + and a2: "\lm1 lm2 c. \\d. P d lm1; \d. P d lm2\ \ P c (Ap lm1 lm2)" + and a3: "\name lm c. \atom name \ c; \d. P d lm\ \ P c (Lm name lm)" + shows "P c lm" +proof - + have "\p. P c (p \ 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 "\q. (q \ {p \ atom name}) \* c \ supp (p \ Lm name lm) \* q") + apply(erule exE) + apply(rule_tac t="p \ Lm name lm" and + s="q \ p \ 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 \ lm)" by blast + then show "P c lm" by simp +qed + +end + + +