# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269328968 -3600
# Node ID 892fcdb96c960ef475499b5d45c438a31fe8a689
# Parent  20221ec06cba955117d7d86d3b1345842b9caf56
Move LamEx out of Test.

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: "\<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
+
+
+
diff -r 20221ec06cba -r 892fcdb96c96 Nominal/NotRsp.thy
--- a/Nominal/NotRsp.thy	Tue Mar 23 08:20:13 2010 +0100
+++ b/Nominal/NotRsp.thy	Tue Mar 23 08:22:48 2010 +0100
@@ -1,4 +1,4 @@
-theory Test
+theory NotRsp
 imports "Parser" "../Attic/Prove"
 begin
 
diff -r 20221ec06cba -r 892fcdb96c96 Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 23 08:20:13 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 08:22:48 2010 +0100
@@ -6,87 +6,6 @@
 
 ML {* val _ = recursive := false *}
 
-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
-
 text {* example 1, equivalent to example 2 from Terms *}
 
 nominal_datatype lam =