# HG changeset patch
# User urbanc
# Date 1133410813 -3600
# Node ID c68296902ddb922d83f174d587054d3718b2ea93
# Parent  b83b00cbaecf366f6be9cc542a0577130c10afed
cleaned up further the proofs (diamond still needs work);
changed "fresh:" to "avoiding:"

diff -r b83b00cbaecf -r c68296902ddb src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Thu Dec 01 04:46:17 2005 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Thu Dec 01 05:20:13 2005 +0100
@@ -6,69 +6,73 @@
 
 text {* The Church-Rosser proof from Barendregt's book *}
 
-lemma forget[rule_format]: 
-  shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"
-proof (nominal_induct t1 fresh: a t2 rule: lam_induct)
-  case (Var a t2 b) 
-  show ?case by (simp, simp add: fresh_atm)
+lemma forget: 
+  assumes a: "a\<sharp>t1"
+  shows "t1[a::=t2] = t1"
+using a
+proof (nominal_induct t1 avoiding: a t2 rule: lam_induct)
+  case (Var b) 
+  thus ?case by (simp add: fresh_atm)
 next 
   case App
-  thus ?case by (simp add: fresh_prod)
+  thus ?case by simp
 next
-  case (Lam c t a t2)
-  have i: "\<And>c t2. c\<sharp>t \<longrightarrow>  t[c::=t2] = t" by fact
+  case (Lam c t)
+  have ih: "\<And>c t2. c\<sharp>t \<Longrightarrow>  t[c::=t2] = t" by fact
   have a: "c\<sharp>t2" by fact
   have "c\<sharp>a" by fact
   hence b: "a\<noteq>c" by (simp add: fresh_atm)
-  show ?case
-  proof 
-    assume "a\<sharp>Lam [c].t" 
-    hence "a\<sharp>t" using b by (simp add: abs_fresh)
-    hence "t[a::=t2] = t" using i by simp
-    thus "(Lam [c].t)[a::=t2] = Lam [c].t" using a b by (simp add: alpha)
-  qed
+  have "a\<sharp>Lam [c].t" by fact 
+  hence "a\<sharp>t" using b by (simp add: abs_fresh)
+  hence "t[a::=t2] = t" using ih by simp
+  thus "(Lam [c].t)[a::=t2] = Lam [c].t" using a b by simp
 qed
 
-lemma forget[rule_format]: 
-  shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"
-apply (nominal_induct t1 fresh: a t2 rule: lam_induct)
+lemma forget: 
+  assumes a: "a\<sharp>t1"
+  shows "t1[a::=t2] = t1"
+  using a
+apply (nominal_induct t1 avoiding: a t2 rule: lam_induct)
 apply(auto simp add: abs_fresh fresh_atm)
 done
 
-lemma fresh_fact[rule_format]: 
+lemma fresh_fact: 
+  fixes   b :: "name"
+  and    a  :: "name"
+  and    t1 :: "lam"
+  and    t2 :: "lam"
+  assumes a: "a\<sharp>t1"
+  and     b: "a\<sharp>t2"
+  shows "a\<sharp>(t1[b::=t2])"
+using a b
+proof (nominal_induct t1 avoiding: a b t2 rule: lam_induct)
+  case (Var c) 
+  thus ?case by simp
+next
+  case App thus ?case by simp 
+next
+  case (Lam c t)
+  have ih: "\<And>(a::name) b t2. a\<sharp>t \<Longrightarrow> a\<sharp>t2 \<Longrightarrow> a\<sharp>(t[b::=t2])" by fact
+  have fr: "c\<sharp>a" "c\<sharp>b" "c\<sharp>t2" by fact+
+  hence fr': "c\<noteq>a" by (simp add: fresh_atm) 
+  have a1: "a\<sharp>t2" by fact
+  have a2: "a\<sharp>Lam [c].t" by fact
+  hence "a\<sharp>t" using fr' by (simp add: abs_fresh)
+  hence "a\<sharp>t[b::=t2]" using a1 ih by simp
+  thus "a\<sharp>(Lam [c].t)[b::=t2]" using fr  by (simp add: abs_fresh)
+qed
+
+lemma fresh_fact: 
   fixes   b :: "name"
   and    a  :: "name"
   and    t1 :: "lam"
   and    t2 :: "lam" 
-  shows "a\<sharp>t1\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t1[b::=t2])"
-proof (nominal_induct t1 fresh: a b t2 rule: lam_induct)
-  case (Var c a b t2) 
-  show ?case by simp
-next
-  case App thus ?case by simp 
-next
-  case (Lam c t a b t2)
-  have  i: "\<And>(a::name) b t2. a\<sharp>t\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t[b::=t2])" by fact
-  have fr: "c\<sharp>a" "c\<sharp>b" "c\<sharp>t2" by fact+
-  hence fr': "c\<noteq>a" by (simp add: fresh_atm) 
-  show ?case 
-  proof (intro strip)
-    assume a1: "a\<sharp>t2"
-    assume a2: "a\<sharp>Lam [c].t"
-    hence "a\<sharp>t" using fr' by (simp add: abs_fresh)
-    hence "a\<sharp>t[b::=t2]" using a1 i by simp
-    thus "a\<sharp>(Lam [c].t)[b::=t2]" using fr  by (simp add: abs_fresh)
-  qed
-qed
-
-lemma fresh_fact[rule_format]: 
-  fixes   b :: "name"
-  and    a  :: "name"
-  and    t1 :: "lam"
-  and    t2 :: "lam" 
-  shows "a\<sharp>t1\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t1[b::=t2])"
-apply(nominal_induct t1 fresh: a b t2 rule: lam_induct)
-apply(auto simp add: abs_fresh fresh_prod fresh_atm)
+  assumes a: "a\<sharp>t1"
+  and     b: "a\<sharp>t2"
+  shows "a\<sharp>(t1[b::=t2])"
+using a b
+apply(nominal_induct t1 avoiding: a b t2 rule: lam_induct)
+apply(auto simp add: abs_fresh fresh_atm)
 done
 
 lemma subs_lemma:  
@@ -81,7 +85,7 @@
   and     b: "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
 using a b
-proof (nominal_induct M fresh: x y N L rule: lam_induct)
+proof (nominal_induct M avoiding: x y N L rule: lam_induct)
   case (Var z) (* case 1: Variables*)
   have "x\<noteq>y" by fact
   have "x\<sharp>L" by fact
@@ -136,11 +140,11 @@
   and   L::"lam"
   and   M::"lam"
   and   N::"lam"
-  assumes "x\<noteq>y"
-  and     "x\<sharp>L"
+  assumes a: "x\<noteq>y"
+  and     b: "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
-using prems
-by (nominal_induct M fresh: x y N L rule: lam_induct)
+using a b
+by (nominal_induct M avoiding: x y N L rule: lam_induct)
    (auto simp add: fresh_fact forget)
 
 lemma subst_rename[rule_format]: 
@@ -149,7 +153,7 @@
   and    t1 :: "lam"
   and    t2 :: "lam"
   shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
-proof (nominal_induct t1 fresh: a c t2 rule: lam_induct)
+proof (nominal_induct t1 avoiding: a c t2 rule: lam_induct)
   case (Var b)
   show "c\<sharp>(Var b) \<longrightarrow> (Var b)[a::=t2] = ([(c,a)]\<bullet>(Var b))[c::=t2]" by (simp add: calc_atm fresh_atm)
 next
@@ -178,7 +182,7 @@
   and    t1 :: "lam"
   and    t2 :: "lam"
   shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
-apply(nominal_induct t1 fresh: a c t2 rule: lam_induct)
+apply(nominal_induct t1 avoiding: a c t2 rule: lam_induct)
 apply(auto simp add: calc_atm fresh_atm abs_fresh)
 done
 
@@ -364,7 +368,7 @@
   assumes a: "a\<sharp>t2" 
   shows "a\<sharp>(t1[a::=t2])"
 using a 
-proof (nominal_induct t1 fresh: a t2 rule: lam_induct)
+proof (nominal_induct t1 avoiding: a t2 rule: lam_induct)
   case (Var b) 
   thus ?case by (simp add: fresh_atm)
 next
@@ -377,49 +381,47 @@
   ultimately show ?case by (simp add: abs_fresh)
 qed
 
-lemma one_fresh_preserv[rule_format]:
+lemma one_fresh_preserv:
   fixes    t :: "lam"
   and      s :: "lam"
   and      a :: "name"
   assumes a: "t\<longrightarrow>\<^isub>1s"
-  shows "a\<sharp>t \<longrightarrow> a\<sharp>s"
-using a
+  and     b: "a\<sharp>t"
+  shows "a\<sharp>s"
+using a b
 proof (induct)
-  case o1 show ?case by simp
+  case o1 thus ?case by simp
 next
-  case o2 thus ?case by (simp add: fresh_prod)
+  case o2 thus ?case by simp
 next
   case (o3 c s1 s2)
-  assume i: "a\<sharp>s1 \<longrightarrow>  a\<sharp>s2"
+  have ih: "a\<sharp>s1 \<Longrightarrow>  a\<sharp>s2" by fact
+  have c: "a\<sharp>Lam [c].s1" by fact
   show ?case
-  proof (intro strip, cases "a=c")
-    assume "a=c" 
-    thus "a\<sharp>Lam [c].s2" by (simp add: abs_fresh)
+  proof (cases "a=c")
+    assume "a=c" thus "a\<sharp>Lam [c].s2" by (simp add: abs_fresh)
   next
-    assume b: "a\<noteq>c" and "a\<sharp>Lam [c].s1"
-    hence "a\<sharp>s1" by (simp add: abs_fresh)
-    hence "a\<sharp>s2" using i by simp
-    thus "a\<sharp>Lam [c].s2" using b by (simp add: abs_fresh) 
+    assume d: "a\<noteq>c" 
+    with c have "a\<sharp>s1" by (simp add: abs_fresh)
+    hence "a\<sharp>s2" using ih by simp
+    thus "a\<sharp>Lam [c].s2" using d by (simp add: abs_fresh) 
   qed
 next 
   case (o4 c t1 t2 s1 s2)
-  assume i1: "a\<sharp>t1 \<longrightarrow> a\<sharp>t2"
-     and i2: "a\<sharp>s1 \<longrightarrow> a\<sharp>s2"
-  show "a\<sharp>App (Lam [c].s1) t1 \<longrightarrow> a\<sharp>s2[c::=t2]"
-  proof
-    assume "a\<sharp>App (Lam [c].s1) t1"
-    hence c1: "a\<sharp>Lam [c].s1" and c2: "a\<sharp>t1" by (simp add: fresh_prod)+
-    from c2 i1 have c3: "a\<sharp>t2" by simp
-    show "a\<sharp>s2[c::=t2]"
-    proof (cases "a=c")
-      assume "a=c"
-      thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact')
-    next
-      assume d1: "a\<noteq>c"
-      from c1 d1 have "a\<sharp>s1" by (simp add: abs_fresh)
-      hence "a\<sharp>s2" using i2 by simp
-      thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact)
-    qed
+  have i1: "a\<sharp>t1 \<Longrightarrow> a\<sharp>t2" by fact
+  have i2: "a\<sharp>s1 \<Longrightarrow> a\<sharp>s2" by fact
+  have as: "a\<sharp>App (Lam [c].s1) t1" by fact
+  hence c1: "a\<sharp>Lam [c].s1" and c2: "a\<sharp>t1" by (simp add: fresh_prod)+
+  from c2 i1 have c3: "a\<sharp>t2" by simp
+  show "a\<sharp>s2[c::=t2]"
+  proof (cases "a=c")
+    assume "a=c"
+    thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact')
+  next
+    assume d1: "a\<noteq>c"
+    from c1 d1 have "a\<sharp>s1" by (simp add: abs_fresh)
+    hence "a\<sharp>s2" using i2 by simp
+    thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact)
   qed
 qed
 
@@ -493,7 +495,7 @@
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
-proof (nominal_induct M fresh: x N N' rule: lam_induct)
+proof (nominal_induct M avoiding: x N N' rule: lam_induct)
   case (Var y) 
   show "Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y", auto)
 next
@@ -512,11 +514,11 @@
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
-apply(nominal_induct M fresh: x N N' rule: lam_induct)
+apply(nominal_induct M avoiding: x N N' rule: lam_induct)
 apply(auto simp add: fresh_prod fresh_atm)
 done
 
-lemma one_subst[rule_format]: 
+lemma one_subst: 
   fixes    M :: "lam"
   and      M':: "lam"
   and      N :: "lam"
@@ -526,7 +528,7 @@
   and     b: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
 using prems
-proof (nominal_induct M M' fresh: N N' x rule: one_induct)
+proof (nominal_induct M M' avoiding: N N' x rule: one_induct)
   case (o1 M)
   thus ?case by (simp add: one_subst_aux)
 next
@@ -554,10 +556,11 @@
   and     b: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
 using a b
-apply(nominal_induct M M' fresh: N N' x rule: one_induct)
+apply(nominal_induct M M' avoiding: N N' x rule: one_induct)
 apply(auto simp add: one_subst_aux subs_lemma fresh_atm)
 done
 
+(* FIXME: change to make use of the new induction facilities *)
 lemma diamond[rule_format]:
   fixes    M :: "lam"
   and      M1:: "lam"