# HG changeset patch
# User narboux
# Date 1175709385 -7200
# Node ID 33a690455f88a9e0158635a6cffd8c1de066b08c
# Parent  de39593f2948f8d30effb34241f02a8756430207
add a few details in the Fst and Snd cases of unicity proof

diff -r de39593f2948 -r 33a690455f88 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Wed Apr 04 18:05:05 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed Apr 04 19:56:25 2007 +0200
@@ -6,7 +6,7 @@
 (* Types and Programming Languages, MIT Press 2005    *)
 
 (* The formalisation was done by Julien Narboux and   *)
-(* Christian Urban                                    *)
+(* Christian Urban.                                   *)
 
 theory Crary
   imports "../Nominal"
@@ -479,8 +479,7 @@
 declare trm.inject [simp del]
 declare ty.inject [simp del]
 
-
-(* FIXME this lemma should not be here I am reinventing the wheel I guess *)
+(* FIXME this lemma should not be here *)
 lemma perm_basic[simp]:
  fixes x y::"name"
 shows "[(x,y)]\<bullet>y = x"
@@ -499,13 +498,14 @@
 qed
 
 (*
+Warning this lemma is false:
+
 lemma algorithmic_type_unicity:
   shows "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
   and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
 
 Here is the counter example : 
 \<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : Tbase and \<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : TUnit
-
 *)
 
 lemma algorithmic_path_type_unicity:
@@ -948,7 +948,6 @@
   then show  "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" using main_lemma(1) val by simp
 qed
 
-
 text {* We leave soundness as an exercise - like in the book :-) \\ 
  @{prop[mode=IfThen] "\<lbrakk>\<Gamma> \<turnstile> s \<Leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} \\
  @{prop "\<lbrakk>\<Gamma> \<turnstile> s \<leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} 
diff -r de39593f2948 -r 33a690455f88 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Wed Apr 04 18:05:05 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Wed Apr 04 19:56:25 2007 +0200
@@ -7,6 +7,9 @@
 (*                                                   *) 
 (* We thank Nick Benton for helping us with the      *) 
 (* termination-proof for evaluation.                 *)
+(*                                                   *)
+(* The formalisation was done by Julien Narboux and  *)
+(* Christian Urban.                                  *)
 
 theory SOS
   imports "../Nominal"
@@ -723,11 +726,17 @@
   then have "e\<^isub>2[x\<^isub>2::=e'] \<Down> t\<^isub>2" using h by (simp add: trm.inject)
   thus "e'' = t\<^isub>2" using ih2 by simp
 next
-  case b_Fst
-  then show ?case by (force simp add: trm.inject)
+  case (b_Fst e e\<^isub>1 e\<^isub>2 e\<^isub>2')
+  have "e \<Down> Pr e\<^isub>1 e\<^isub>2" by fact
+  have "\<And> b. e \<Down> b \<Longrightarrow> Pr e\<^isub>1 e\<^isub>2 = b" by fact
+  have "Fst e \<Down> e\<^isub>2'" by fact
+  show "e\<^isub>1 = e\<^isub>2'" using prems by (force simp add: trm.inject)
 next
-  case b_Snd
-  then show ?case by (force simp add: trm.inject)
+  case (b_Snd e e\<^isub>1 e\<^isub>2 e\<^isub>2')
+  have "e \<Down> Pr e\<^isub>1 e\<^isub>2" by fact
+  have "\<And> b. e \<Down> b \<Longrightarrow> Pr e\<^isub>1 e\<^isub>2 = b" by fact
+  have "Snd e \<Down> e\<^isub>2'" by fact
+  show "e\<^isub>2 = e\<^isub>2'" using prems by (force simp add: trm.inject)
 qed (blast)+
 
 lemma not_val_App[simp]: