--- 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"}
--- 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]: