# HG changeset patch
# User urbanc
# Date 1206698898 -3600
# Node ID 5c21ec1ff293702b0d47de127191de21f72f7a38
# Parent  9385d441cec67fbf6abd2658845292b375155240
tuned proofs

diff -r 9385d441cec6 -r 5c21ec1ff293 src/HOL/Nominal/Examples/CR_Takahashi.thy
--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Mar 28 00:02:58 2008 +0100
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Mar 28 11:08:18 2008 +0100
@@ -45,23 +45,17 @@
 by (nominal_induct t avoiding: x s rule: lam.induct)
    (auto simp add: abs_fresh fresh_atm)
 
-lemma fresh_fact1:
+lemma fresh_fact:
   fixes z::"name"
-  shows "z\<sharp>(t,s) \<Longrightarrow> z\<sharp>t[y::=s]"
+  shows "z\<sharp>s \<and> (z=y \<or> z\<sharp>t) \<Longrightarrow> z\<sharp>t[y::=s]"
 by (nominal_induct t avoiding: z y s rule: lam.induct)
    (auto simp add: abs_fresh fresh_prod fresh_atm)
 
-lemma fresh_fact2: 
-  fixes x::"name"
-  shows "x\<sharp>s \<Longrightarrow> x\<sharp>t[x::=s]"
-by (nominal_induct t avoiding: x s rule: lam.induct)
-   (auto simp add: abs_fresh fresh_atm)
-
 lemma substitution_lemma:  
   assumes a: "x\<noteq>y" "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.induct)
-           (auto simp add: fresh_fact1 forget)
+           (auto simp add: fresh_fact forget)
 
 lemma subst_rename: 
   assumes a: "y\<sharp>t"
@@ -100,7 +94,7 @@
 
 equivariance One
 nominal_inductive One 
-  by (simp_all add: abs_fresh fresh_fact2)
+  by (simp_all add: abs_fresh fresh_fact)
 
 lemma One_refl:
   shows "t \<longrightarrow>\<^isub>1 t"
@@ -110,7 +104,7 @@
   assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
   shows "t1[x::=s1] \<longrightarrow>\<^isub>1 t2[x::=s2]" 
 using a by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
-           (auto simp add: substitution_lemma fresh_atm fresh_fact1)
+           (auto simp add: substitution_lemma fresh_atm fresh_fact)
 
 lemma better_o4_intro:
   assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
@@ -142,6 +136,12 @@
          (\<exists>x p p' s'. r = p'[x::=s'] \<and> t = Lam [x].p \<and> p \<longrightarrow>\<^isub>1 p' \<and> s \<longrightarrow>\<^isub>1 s' \<and> x\<sharp>(s,s'))" 
 using a by (cases rule: One.cases) (auto simp add: lam.inject)
 
+lemma One_App_: 
+  assumes a: "App t s \<longrightarrow>\<^isub>1 r"
+  obtains t' s' where "r = App t' s'" "t \<longrightarrow>\<^isub>1 t'" "s \<longrightarrow>\<^isub>1 s'" 
+        | x p p' s' where "r = p'[x::=s']" "t = Lam [x].p" "p \<longrightarrow>\<^isub>1 p'" "s \<longrightarrow>\<^isub>1 s'" "x\<sharp>(s,s')"
+using a by (cases rule: One.cases) (auto simp add: lam.inject)
+
 lemma One_Redex: 
   assumes a: "App (Lam [x].t) s \<longrightarrow>\<^isub>1 r" "x\<sharp>(s,r)"
   shows "(\<exists>t' s'. r = App (Lam [x].t') s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or> 
@@ -171,7 +171,7 @@
 
 equivariance Dev
 nominal_inductive Dev 
-  by (simp_all add: abs_fresh fresh_fact2)
+  by (simp_all add: abs_fresh fresh_fact)
 
 lemma better_d4_intro:
   assumes a: "t1 \<longrightarrow>\<^isub>d t2" "s1 \<longrightarrow>\<^isub>d s2"
@@ -190,7 +190,7 @@
   assumes a: "M\<longrightarrow>\<^isub>d N"  
   shows "x\<sharp>M \<Longrightarrow> x\<sharp>N"
 using a
-by (induct) (auto simp add: abs_fresh fresh_fact1 fresh_fact2)
+by (induct) (auto simp add: abs_fresh fresh_fact)
 
 lemma Dev_Lam:
   assumes a: "Lam [x].M \<longrightarrow>\<^isub>d N" 
@@ -212,10 +212,31 @@
   assumes a: "t \<longrightarrow>\<^isub>d t1" "t \<longrightarrow>\<^isub>1 t2"
   shows "t2 \<longrightarrow>\<^isub>1 t1"
 using a 
-apply(nominal_induct avoiding: t2 rule: Dev.strong_induct)
-apply(auto dest!: One_Var One_Lam One_App)[3]
-apply(auto dest!: One_Redex intro: One_subst)
-done
+proof(nominal_induct avoiding: t2 rule: Dev.strong_induct)
+  case (d4 x s1 s2 t1 t1' t2) 
+  have ih1: "\<And>t. t1 \<longrightarrow>\<^isub>1 t \<Longrightarrow>  t \<longrightarrow>\<^isub>1 t1'"
+  and  ih2: "\<And>s. s1 \<longrightarrow>\<^isub>1 s \<Longrightarrow>  s \<longrightarrow>\<^isub>1 s2"
+  and  fc: "x\<sharp>t2" "x\<sharp>s1" "x\<sharp>s2" by fact+ 
+  have "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>1 t2" by fact
+  then obtain t' s' where "(t2 = App (Lam [x].t') s' \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s') \<or> 
+                           (t2 = t'[x::=s'] \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s')"
+    (* MARKUS: How does I do this better *) using fc by (auto dest!: One_Redex)
+  then show "t2 \<longrightarrow>\<^isub>1 t1'[x::=s2]"
+    apply -
+    apply(erule disjE)
+    apply(erule conjE)+
+    apply(simp)
+    apply(rule o4)
+    using fc apply(simp)
+    using ih1 apply(simp)
+    using ih2 apply(simp)
+    apply(erule conjE)+
+    apply(simp)
+    apply(rule One_subst)
+    using ih1 apply(simp)
+    using ih2 apply(simp)    
+    done
+qed (auto dest!: One_Lam One_Var One_App)
 
 lemma Diamond_for_One:
   assumes a: "t \<longrightarrow>\<^isub>1 t1" "t \<longrightarrow>\<^isub>1 t2"