# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295459788 -3600
# Node ID 42c0d011a177d97a92efe8a43e93c4f18155968f
# Parent  2873b3230c4403f913a4dc1545809f23320329d3
ported some of the old proofs to serve as testcases

diff -r 2873b3230c44 -r 42c0d011a177 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jan 19 18:07:29 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Jan 19 18:56:28 2011 +0100
@@ -7,68 +7,37 @@
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
-| Lam x::"name" l::"lam"  bind x in l
+| Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
-thm lam.distinct
-thm lam.induct
-thm lam.exhaust lam.strong_exhaust
-thm lam.fv_defs
-thm lam.bn_defs
-thm lam.perm_simps
-thm lam.eq_iff
-thm lam.fv_bn_eqvt
-thm lam.size_eqvt
+text {* height function *}
 
 nominal_primrec
   height :: "lam \<Rightarrow> int"
 where
   "height (Var x) = 1"
-| "height (App t1 t2) = (max (height t1) (height t2)) + 1"
-| "height (Lam x t) = (height t) + 1"
+| "height (App t1 t2) = max (height t1) (height t2) + 1"
+| "height (Lam [x].t) = height t + 1"
 apply(rule_tac y="x" in lam.exhaust)
-apply(simp_all)[3]
-apply(simp_all only: lam.distinct)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(subst (asm) Abs_eq_iff)
-apply(erule exE)
-apply(simp add: alphas)
+apply(auto simp add: lam.distinct lam.eq_iff)
+apply(simp add: Abs_eq_iff alphas)
 apply(clarify)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
-apply(simp add: pure_supp)
-apply(simp add: fresh_star_def)
+apply(subst (4) supp_perm_eq[where p="p", symmetric])
+apply(simp add: pure_supp fresh_star_def)
 apply(simp add: eqvt_at_def)
 done
 
 termination
-  apply(relation "measure size")
-  apply(simp_all add: lam.size)
-  done
+  by (relation "measure size") (simp_all add: lam.size)
   
-lemma removeAll_eqvt[eqvt]:
-  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
-by (induct xs) (auto)
-
-lemma supp_removeAll:
-  fixes x::"atom"
-  shows "supp (removeAll x xs) = (supp xs - {x})"
-apply(induct xs)
-apply(simp_all add: supp_Nil supp_Cons)
-apply(rule conjI)
-apply(rule impI)
-apply(simp add: supp_atom)
-apply(rule impI)
-apply(simp add: supp_atom)
-apply(blast)
-done
+  
+text {* free name function - returns atom lists *}
 
 nominal_primrec 
   frees_lst :: "lam \<Rightarrow> atom list"
 where
   "frees_lst (Var x) = [atom x]"
-| "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"
-| "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"
+| "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
+| "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
 apply(rule_tac y="x" in lam.exhaust)
 apply(simp_all)[3]
 apply(simp_all only: lam.distinct)
@@ -95,42 +64,28 @@
   apply(simp_all add: lam.size)
   done
 
-text {* a small lemma *}
+text {* a small test lemma *}
 lemma
-  "supp t = set (frees_lst t)"
-apply(induct t rule: lam.induct)
+  shows "supp t = set (frees_lst t)"
+apply(induct t rule: frees_lst.induct)
 apply(simp_all add: lam.supp supp_at_base)
 done
 
+text {* capture - avoiding substitution *}
+
 nominal_primrec
-  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
 where
-  "(Var x)[y ::= s] = (if x=y then s else (Var x))"
-| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
-| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
-apply(case_tac x)
-apply(simp)
-apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
-apply(simp add: lam.eq_iff lam.distinct)
-apply(auto)[1]
-apply(simp add: lam.eq_iff lam.distinct)
-apply(auto)[1]
-apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
-apply(simp_all add: lam.distinct)[5]
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(erule conjE)+
+  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
+| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
+| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
+apply(auto simp add: lam.distinct lam.eq_iff)
+apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
+apply(blast)+
+apply(simp add: fresh_star_def)
 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")
-prefer 2
-apply(rule conjI)
-apply(simp add: Abs_fresh_iff)
-apply(drule sym)
-apply(simp add: Abs_fresh_iff)
 apply(subst (asm) Abs_eq_iff2)
-apply(auto)
-apply(simp add: alphas)
-apply(simp add: atom_eqvt)
+apply(simp add: alphas atom_eqvt)
 apply(clarify)
 apply(rule trans)
 apply(rule_tac p="p" in supp_perm_eq[symmetric])
@@ -151,18 +106,126 @@
 apply(simp add: Abs_fresh_iff)
 apply(subgoal_tac "p \<bullet> ya = ya")
 apply(subgoal_tac "p \<bullet> sa = sa")
-unfolding eqvt_at_def
-apply(simp add: atom_eqvt fresh_Pair)
+apply(simp add: atom_eqvt eqvt_at_def)
 apply(rule perm_supp_eq)
 apply(auto simp add: fresh_star_def fresh_Pair)[1]
 apply(rule perm_supp_eq)
 apply(auto simp add: fresh_star_def fresh_Pair)[1]
+apply(rule conjI)
+apply(simp add: Abs_fresh_iff)
+apply(drule sym)
+apply(simp add: Abs_fresh_iff)
 done
 
 termination
-  apply(relation "measure (\<lambda>(t,_,_). size t)")
-  apply(simp_all add: lam.size)
-  done
+  by (relation "measure (\<lambda>(t,_,_). size t)")
+     (simp_all add: lam.size)
+
+lemma subst_eqvt[eqvt]:
+  shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
+by (induct t x s rule: subst.induct) (simp_all)
+
+lemma forget:
+  shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
+apply(nominal_induct t avoiding: x s rule: lam.strong_induct)
+apply(auto simp add: lam.fresh fresh_at_base)
+done
+
+text {* same lemma but with subst.induction *}
+lemma forget2:
+  shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
+apply(induct t x s rule: subst.induct)
+apply(auto simp add: lam.fresh fresh_at_base fresh_Pair)
+done
+
+lemma fresh_fact:
+  fixes z::"name"
+  assumes a: "atom z \<sharp> s"
+  and b: "z = y \<or> atom z \<sharp> t"
+  shows "atom z \<sharp> t[y ::= s]"
+using a b
+apply (nominal_induct t avoiding: z y s rule: lam.strong_induct)
+apply (auto simp add: lam.fresh fresh_at_base)
+done
+
+lemma substitution_lemma:  
+  assumes a: "x \<noteq> y" "atom x \<sharp> u"
+  shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]"
+using a 
+by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)
+   (auto simp add: fresh_fact forget)
+
+lemma subst_rename: 
+  assumes a: "atom y \<sharp> t"
+  shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet>t)[y ::= s]"
+using a 
+apply (nominal_induct t avoiding: x y s rule: lam.strong_induct)
+apply (auto simp add: lam.fresh fresh_at_base)
+done
+
+
+subsection {* single-step beta-reduction *}
+
+inductive 
+  beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80)
+where
+  b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s"
+| b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2"
+| b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2"
+| b4[intro]: "atom x \<sharp> s \<Longrightarrow> App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]"
+
+equivariance beta
+
+nominal_inductive beta
+  avoids b4: "x"
+  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
+
+text {* One-Reduction *}
+
+inductive 
+  One :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>1 _" [80,80] 80)
+where
+  o1[intro]: "Var x \<longrightarrow>1 Var x"
+| o2[intro]: "\<lbrakk>t1 \<longrightarrow>1 t2; s1 \<longrightarrow>1 s2\<rbrakk> \<Longrightarrow> App t1 s1 \<longrightarrow>1 App t2 s2"
+| o3[intro]: "t1 \<longrightarrow>1 t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>1 Lam [x].t2"
+| o4[intro]: "\<lbrakk>atom x \<sharp> (s1, s2); t1 \<longrightarrow>1 t2; s1 \<longrightarrow>1 s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]"
+
+equivariance One
+
+nominal_inductive One 
+  avoids o3: "x"
+      |  o4: "x"
+  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
+
+lemma One_refl:
+  shows "t \<longrightarrow>1 t"
+by (nominal_induct t rule: lam.strong_induct) (auto)
+
+lemma One_subst: 
+  assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"
+  shows "t1[x ::= s1] \<longrightarrow>1 t2[x ::= s2]" 
+using a 
+apply(nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
+apply(auto simp add: substitution_lemma fresh_at_base fresh_fact fresh_Pair)
+done
+
+lemma better_o4_intro:
+  assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"
+  shows "App (Lam [x]. t1) s1 \<longrightarrow>1 t2[ x ::= s2]"
+proof -
+  obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" sorry
+  have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs
+    by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
+  also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt)
+  also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric])
+  finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp
+qed
+
+
+
+
+
+section {* Locally Nameless Terms *}
 
 nominal_datatype ln = 
   LNBnd nat
diff -r 2873b3230c44 -r 42c0d011a177 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Wed Jan 19 18:07:29 2011 +0100
+++ b/Nominal/Nominal2_Abs.thy	Wed Jan 19 18:56:28 2011 +0100
@@ -744,8 +744,7 @@
   and   "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"
 proof -
   { assume "a = b"
-    then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)"
-      by (simp add: Abs1_eq)
+    then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
   }
   moreover
   { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"
@@ -769,8 +768,7 @@
     by blast
 next
   { assume "a = b"
-    then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)"
-      by (simp add: Abs1_eq)
+    then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
   }
   moreover
   { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"
@@ -794,8 +792,7 @@
     by blast
 next
   { assume "c = d"
-    then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)"
-      by (simp add: Abs1_eq)
+    then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)" by (simp add: Abs1_eq)
   }
   moreover
   { assume *: "c \<noteq> d" and **: "Abs_lst [c] x = Abs_lst [d] y"
@@ -819,6 +816,15 @@
     by blast
 qed
 
+lemma Abs1_eq_iff':
+  fixes x::"'a::fs"
+  assumes "sort_of a = sort_of b"
+  and     "sort_of c = sort_of d"
+  shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)"
+  and   "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)"
+  and   "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> (d \<rightleftharpoons> c) \<bullet> x = y \<and> d \<sharp> x)"
+using assms by (auto simp add: Abs1_eq_iff fresh_permute_left)
+
 
 subsection {* Renaming of bodies of abstractions *}
 
diff -r 2873b3230c44 -r 42c0d011a177 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Wed Jan 19 18:07:29 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Jan 19 18:56:28 2011 +0100
@@ -844,14 +844,25 @@
   by (simp add: fresh_permute_iff)
 
 lemma supp_eqvt:
-  fixes  p  :: "perm"
-  and    x   :: "'a::pt"
   shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
   unfolding supp_conv_fresh
   unfolding Collect_def
   unfolding permute_fun_def
   by (simp add: Not_eqvt fresh_eqvt)
 
+lemma fresh_permute_left:
+  shows "a \<sharp> p \<bullet> x \<longleftrightarrow> - p \<bullet> a \<sharp> x"
+proof
+  assume "a \<sharp> p \<bullet> x"
+  then have "- p \<bullet> a \<sharp> - p \<bullet> p \<bullet> x" by (simp only: fresh_permute_iff)
+  then show "- p \<bullet> a \<sharp> x" by simp
+next
+  assume "- p \<bullet> a \<sharp> x"
+  then have "p \<bullet> - p \<bullet> a \<sharp> p \<bullet> x" by (simp only: fresh_permute_iff)
+  then show "a \<sharp> p \<bullet> x" by simp
+qed
+
+
 subsection {* supports *}
 
 definition
@@ -2236,11 +2247,15 @@
   apply(simp)
   done
 
+lemma fresh_at_base_permute_iff[simp]:
+  fixes a::"'a::at_base"
+  shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x"
+  unfolding atom_eqvt[symmetric]
+  by (simp add: fresh_permute_iff)
+
 
 section {* Infrastructure for concrete atom types *}
 
-section {* A swapping operation for concrete atoms *}
-  
 definition
   flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')")
 where
@@ -2305,6 +2320,8 @@
 using assms
 by (simp add: flip_def swap_fresh_fresh)
 
+
+
 subsection {* Syntax for coercing at-elements to the atom-type *}
 
 syntax
@@ -2502,7 +2519,7 @@
   apply (subst fresh_fun_apply', assumption+)
   apply (drule fresh_permute_iff [where p=p, THEN iffD2])
   apply (drule fresh_permute_iff [where p=p, THEN iffD2])
-  apply (simp add: atom_eqvt permute_fun_app_eq [where f=h])
+  apply (simp only: atom_eqvt permute_fun_app_eq [where f=h])
   apply (erule (1) fresh_fun_apply' [symmetric])
   done