# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270804085 -7200
# Node ID fddb470720f11c69c70ec8db5528edaebc9a48a4
# Parent  5165c350ee1af409baea447f99b300d34ad112f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper

diff -r 5165c350ee1a -r fddb470720f1 Nominal/Ex/ExLam.thy
--- a/Nominal/Ex/ExLam.thy	Thu Apr 08 14:18:38 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-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
-
-
-
diff -r 5165c350ee1a -r fddb470720f1 Nominal/Ex/Lambda.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 09 11:08:05 2010 +0200
@@ -0,0 +1,105 @@
+theory Lambda
+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]
+
+(* 
+  Old way of establishing strong induction
+  principles by chosing a fresh name.
+*)
+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(assumption)
+    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
+
+(* 
+  New way of establishing strong induction
+  principles by using a appropriate permutation.
+*)
+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(assumption)
+    apply(assumption)
+    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)
+    apply(rule at_set_avoiding2)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp only: lm.perm atom_eqvt)
+    apply(simp add: fresh_star_def fresh_def supp_fn')
+    apply(rule supp_perm_eq)
+    apply(simp)
+    done
+  then have "P c (0 \<bullet> lm)" by blast
+  then show "P c lm" by simp
+qed
+
+end
+
+
+
diff -r 5165c350ee1a -r fddb470720f1 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Thu Apr 08 14:18:38 2010 +0200
+++ b/Nominal/ROOT.ML	Fri Apr 09 11:08:05 2010 +0200
@@ -1,7 +1,7 @@
 quick_and_dirty := true;
 
 no_document use_thys
-   ["Ex/ExLam",
+   ["Ex/Lambda",
     "Ex/ExLF",
     "Ex/Ex1",
     "Ex/Ex1rec",
diff -r 5165c350ee1a -r fddb470720f1 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Apr 08 14:18:38 2010 +0200
+++ b/Paper/Paper.thy	Fri Apr 09 11:08:05 2010 +0200
@@ -424,7 +424,7 @@
   permutations.  The sorts of atoms can be used to represent different kinds of
   variables, such as the term-, coercion- and type-variables in Core-Haskell.
   It is assumed that there is an infinite supply of atoms for each
-  sort. However, in order to simplify the description, we shall restrict ourselves 
+  sort. However, in the intrest of brevity, we shall restrict ourselves 
   in what follows to only one sort of atoms.
 
   Permutations are bijective functions from atoms to atoms that are