# HG changeset patch
# User urbanc
# Date 1169058595 -3600
# Node ID b1be13d32efd0575f67a11251042ebef1b5eaee9
# Parent  fd2b69c2f15d47f2372b0bc271959df9fddb3dd7
tuned a bit the proofs

diff -r fd2b69c2f15d -r b1be13d32efd src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Wed Jan 17 11:39:32 2007 +0100
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed Jan 17 19:29:55 2007 +0100
@@ -1,10 +1,12 @@
 (* "$Id$" *)
 (*                                                    *)
-(* Formalisation of the chapter                       *)
-(* Logical Relations and a Case Study in Equivalence  *)
-(* Checking                                           *)
-(* by Crary.                                          *)
-(* Formalisation by Julien Narboux and Christian Urban*)
+(* Formalisation of the chapter on Logical Relations  *)
+(* and a Case Study in Equivalence Checking           *)
+(* by Karl Crary from the book on Advanced Topics in  *)
+(* Types and Programming Languages, MIT Press 2005    *)
+
+(* The formalisation was done by Julien Narboux and   *)
+(* Christian Urban                                    *)
 
 theory Crary
   imports "Nominal"
@@ -22,7 +24,7 @@
                      | App "trm" "trm"
                      | Const "nat"
 
-(* FIXME: the next lemma needs to be in Nominal.thy *)
+(* The next 3 lemmas should be in the nominal library *)
 lemma eq_eqvt:
   fixes pi::"name prm"
   and   x::"'a::pt_name"
@@ -42,8 +44,7 @@
   and   xs::"('a::pt_name) list"
   shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
   by (perm_simp add: pt_list_set_pi[OF pt_name_inst])
-
-(* End of library *)
+(* end of library *)
 
 lemma perm_ty[simp]: 
   fixes T::"ty"
@@ -60,9 +61,7 @@
 lemma ty_cases:
   fixes T::ty
   shows "(\<exists> T1 T2. T=T1\<rightarrow>T2) \<or> T=TUnit \<or> T=TBase"
-apply (induct T rule:ty.induct_weak)
-apply (auto)
-done
+by (induct T rule:ty.induct_weak) (auto)
 
 text {* Size Functions *} 
 
@@ -100,7 +99,7 @@
 inductive2
   valid :: "(name \<times> 'a::pt_name) list \<Rightarrow> bool"
 where
-    v_nil[intro]: "valid []"
+    v_nil[intro]:  "valid []"
   | v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
 
 lemma valid_eqvt:
@@ -113,7 +112,7 @@
 inductive_cases2  
   valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)"
 
-text {* typing judgements for trms *}
+text {* typing judgements for terms *}
 
 inductive2
   typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 
@@ -423,13 +422,10 @@
 	by (simp, blast intro: equiv_def_eqvt)
     next
       case (Q_Ext x \<Gamma> s t T1 T2 pi c)
-      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (T1\<rightarrow>T2)" using a7 
-	apply -
+      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (T1\<rightarrow>T2)"  
+	apply(auto intro!: a7 simp add: fresh_bij)
+	apply(drule equiv_def_eqvt)
 	apply(simp)
-	apply(rule_tac x="pi\<bullet>x" in a7)
-	apply(simp add: fresh_bij)
-	apply(drule equiv_def_eqvt)
-	apply(simp)+
 	done
     next
       case (Q_Abs x \<Gamma> T1 s2 t2 T2 pi c)
@@ -539,25 +535,23 @@
   fixes pi::"name prm"
   assumes a: "t \<leadsto> t'"
   shows "(pi\<bullet>t) \<leadsto> (pi\<bullet>t')"
-  using a
-  apply(induct)
-  apply(auto simp add: subst_eqvt fresh_bij)
-  done
+using a
+by (induct) (auto simp add: subst_eqvt fresh_bij)
 
 lemma whn_eqvt:
   fixes pi::"name prm"
   assumes a: "t \<Down> t'"
   shows "(pi\<bullet>t) \<Down> (pi\<bullet>t')"
-  using a
-  apply(induct)
-  apply(rule QAN_Reduce)
-  apply(rule whr_eqvt)
-  apply(assumption)+
-  apply(rule QAN_Normal)
-  apply(auto)
-  apply(drule_tac pi="rev pi" in whr_eqvt)
-  apply(perm_simp)
-  done
+using a
+apply(induct)
+apply(rule QAN_Reduce)
+apply(rule whr_eqvt)
+apply(assumption)+
+apply(rule QAN_Normal)
+apply(auto)
+apply(drule_tac pi="rev pi" in whr_eqvt)
+apply(perm_simp)
+done
 
 text {* Algorithmic term equivalence and algorithmic path equivalence *}
 
@@ -677,9 +671,8 @@
   then show ?thesis by simp
 qed
 
-(* post-processing of the strong induction principle     *) 
-(* extracts the strong_inducts-version from strong_induct *)
-
+(* post-processing of the strong induction principle proved above; *) 
+(* the code extracts the strong_inducts-version from strong_induct *)
 setup {*
   PureThy.add_thmss
     [(("alg_equiv_alg_path_equiv_strong_inducts",
@@ -747,9 +740,10 @@
 where    
    "\<Gamma> \<turnstile> s is t : TUnit = valid \<Gamma>"
  | "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s <=> t : TBase"
- | "\<Gamma> \<turnstile> s is t : (T1 \<rightarrow> T2) =  (valid \<Gamma> \<and> (\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T2)))"
+ | "\<Gamma> \<turnstile> s is t : (T1 \<rightarrow> T2) =  
+           (valid \<Gamma> \<and> (\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T2)))"
 apply (auto simp add: ty.inject)
-apply (subgoal_tac "(\<exists> T1 T2. b=T1 \<rightarrow> T2) \<or> b=TUnit \<or> b=TBase" )
+apply (subgoal_tac "(\<exists>T1 T2. b=T1 \<rightarrow> T2) \<or> b=TUnit \<or> b=TBase" )
 apply (force)
 apply (rule ty_cases)
 done
@@ -791,8 +785,8 @@
   assumes a: "x\<sharp>L" 
   shows "L[x::=P] = L"
   using a
-  by (nominal_induct L avoiding: x P rule: trm.induct)
-     (auto simp add: fresh_atm abs_fresh)
+by (nominal_induct L avoiding: x P rule: trm.induct)
+   (auto simp add: fresh_atm abs_fresh)
 
 lemma subst_fun_eq:
   fixes u::trm
@@ -820,15 +814,14 @@
   assumes h:"c \<sharp> \<theta>"
   shows "\<theta><t>[c::=s] = (c,s)#\<theta><t>"
   using h
-  apply(nominal_induct t avoiding: \<theta> c s rule: trm.induct)
-  apply(auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)
-  done
+by (nominal_induct t avoiding: \<theta> c s rule: trm.induct)
+   (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)
 
 lemma subst_fresh_simpl:
-  assumes "x\<sharp>\<theta>"
+  assumes a: "x\<sharp>\<theta>"
   shows "\<theta><Var x> = Var x"
-  using assms
-  by (induct \<theta> arbitrary: x, auto simp add:fresh_list_cons fresh_prod fresh_atm)
+using a
+by (induct \<theta> arbitrary: x, auto simp add:fresh_list_cons fresh_prod fresh_atm)
 
 lemma psubst_subst_propagate: 
   assumes "x\<sharp>\<theta>" 
@@ -873,15 +866,13 @@
   assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
   shows "s \<leadsto>|" and "t \<leadsto>|"
 using assms
-by (induct rule: alg_equiv_alg_path_equiv.inducts (2)) (simp, auto)
+by (induct rule: alg_equiv_alg_path_equiv.inducts(2)) (simp, auto)
 
 lemma path_equiv_implies_nf:
   shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> True"
     and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> s \<leadsto>|"
         "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> t \<leadsto>|"
-  apply (induct rule: alg_equiv_alg_path_equiv.inducts)
-  apply auto
-  done
+by (induct rule: alg_equiv_alg_path_equiv.inducts) (auto)
 
 lemma main_lemma:
   shows "\<Gamma> \<turnstile> s is t : T \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T" and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> \<Gamma> \<turnstile> p is q : T"
@@ -928,33 +919,35 @@
 qed (auto elim:alg_equiv_valid)
 
 corollary corollary_main:
-  assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
+  assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
   shows "\<Gamma> \<turnstile> s <=> t : T"
-using assms main_lemma by blast
+using a main_lemma by blast
 
 lemma algorithmic_symmetry_aux:
-  shows "(\<Gamma> \<turnstile> s <=> t : T \<longrightarrow> \<Gamma> \<turnstile> t <=> s : T) \<and> (\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> s : T)"
-by (rule alg_equiv_alg_path_equiv.induct,auto)
+  shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> \<Gamma> \<turnstile> t <=> s : T" 
+  and   "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> s : T"
+by (induct rule: alg_equiv_alg_path_equiv.inducts) (auto)
 
 lemma algorithmic_symmetry:
-  assumes "\<Gamma> \<turnstile> s <=> t : T"
+  assumes a: "\<Gamma> \<turnstile> s <=> t : T"
   shows "\<Gamma> \<turnstile> t <=> s : T"
-using assms by (simp add: algorithmic_symmetry_aux)
+using a by (simp add: algorithmic_symmetry_aux)
 
 lemma algorithmic_path_symmetry:
-  assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
+  assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
   shows "\<Gamma> \<turnstile> t \<leftrightarrow> s : T"
-using assms by (simp add: algorithmic_symmetry_aux)
+using a by (simp add: algorithmic_symmetry_aux)
 
 lemma red_unicity : 
-  assumes "x \<leadsto> a" "x \<leadsto> b"
+  assumes a: "x \<leadsto> a" 
+  and     b: "x \<leadsto> b"
   shows "a=b"
-  using assms
+  using a b
 apply (induct arbitrary: b)
 apply (erule whr_App_Lam)
 apply (clarify)
 apply (rule subst_fun_eq)
-apply (force)
+apply (simp)
 apply (force)
 apply (erule whr_App)
 apply (blast)+
@@ -975,7 +968,7 @@
 qed (auto)
 
 lemma Q_eqvt :
-  fixes pi:: "(name \<times> name) list"
+  fixes pi:: "name prm"
   shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) <=> (pi\<bullet>t) : T"
   and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) \<leftrightarrow> (pi\<bullet>t) : T"
 using assms
@@ -998,7 +991,7 @@
 (* FIXME this lemma should not be here I am reinventing the wheel I guess *)
 
 lemma perm_basic[simp]:
- fixes x y ::name
+ fixes x y::"name"
 shows "[(x,y)]\<bullet>y = x"
 using assms using calc_atm by perm_simp
 
@@ -1006,13 +999,15 @@
   assumes fs:"x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u" and h:"\<Gamma> \<turnstile> t <=> u : T1\<rightarrow>T2"
   shows "(x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> App u (Var x) : T2"
 proof -
-obtain y where  fs2:"y\<sharp>\<Gamma>" "y\<sharp>u" "y\<sharp>t" and "(y,T1)#\<Gamma> \<turnstile> App t (Var y) <=> App u (Var y) : T2" using h by auto
-then have "([(x,y)]\<bullet>((y,T1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) <=> [(x,y)]\<bullet> App u (Var y) : T2" using Q_eqvt by blast
-then show ?thesis using fs fs2 by (perm_simp)
+  obtain y where  fs2:"y\<sharp>\<Gamma>" "y\<sharp>u" "y\<sharp>t" and "(y,T1)#\<Gamma> \<turnstile> App t (Var y) <=> App u (Var y) : T2" 
+    using h by auto
+  then have "([(x,y)]\<bullet>((y,T1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) <=> [(x,y)]\<bullet> App u (Var y) : T2" 
+    using Q_eqvt by blast
+  then show ?thesis using fs fs2 by (perm_simp)
 qed
 
-lemma fresh_context[rule_format]: 
-  fixes  \<Gamma> :: "(name\<times>ty)list"
+lemma fresh_context: 
+  fixes  \<Gamma> :: "(name\<times>ty) list"
   and    a :: "name"
   assumes "a\<sharp>\<Gamma>"
   shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
@@ -1042,7 +1037,8 @@
 
 lemma algorithmic_path_type_unicity:
   shows "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
-proof (induct arbitrary:  u T' rule:alg_equiv_alg_path_equiv.inducts(2) [of _ _ _ _ _  "%a b c d . True"    ])
+proof (induct arbitrary:  u T' 
+       rule: alg_equiv_alg_path_equiv.inducts(2) [of _ _ _ _ _  "%a b c d . True"    ])
   case (QAP_Var \<Gamma> x T u T')
   have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact
   then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto
@@ -1073,10 +1069,12 @@
   case (QAT_Arrow  x \<Gamma> s t T1 T2 u)
   have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
   moreover have h:"\<Gamma> \<turnstile> t <=> u : T1\<rightarrow>T2" by fact
-  moreover then obtain y where "y\<sharp>\<Gamma>" "y\<sharp>t" "y\<sharp>u" and "(y,T1)#\<Gamma> \<turnstile> App t (Var y) <=> App u (Var y) : T2" by auto
+  moreover then obtain y where "y\<sharp>\<Gamma>" "y\<sharp>t" "y\<sharp>u" and "(y,T1)#\<Gamma> \<turnstile> App t (Var y) <=> App u (Var y) : T2" 
+    by auto
   moreover have fs2:"x\<sharp>u" by fact
   ultimately have "(x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> App u (Var x) : T2" using Q_Arrow_strong_inversion by blast
-  moreover have ih:"\<And> v. (x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> v : T2 \<Longrightarrow> (x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> v : T2" by fact
+  moreover have ih:"\<And> v. (x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> v : T2 \<Longrightarrow> (x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> v : T2" 
+    by fact
   ultimately have "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App u (Var x) : T2" by auto
   then show "\<Gamma> \<turnstile> s <=> u : T1\<rightarrow>T2" using fs fs2 by auto
 next
@@ -1086,7 +1084,8 @@
   have "\<Gamma> \<turnstile> s <=> t : T1" by fact
   have ih2:"\<And>u. \<Gamma> \<turnstile> t <=> u : T1 \<Longrightarrow> \<Gamma> \<turnstile> s <=> u : T1" by fact
   have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T2" by fact
-  then obtain r T1' v where ha:"\<Gamma> \<turnstile> q \<leftrightarrow> r : T1'\<rightarrow>T2" and hb:"\<Gamma> \<turnstile> t <=> v : T1'" and eq:"u = App r v" by auto
+  then obtain r T1' v where ha:"\<Gamma> \<turnstile> q \<leftrightarrow> r : T1'\<rightarrow>T2" and hb:"\<Gamma> \<turnstile> t <=> v : T1'" and eq:"u = App r v" 
+    by auto
   moreover have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T1\<rightarrow>T2" using h1 algorithmic_path_symmetry by auto
   ultimately have "T1'\<rightarrow>T2 = T1\<rightarrow>T2" using algorithmic_path_type_unicity by auto
   then have "T1' = T1" using ty.inject by auto
@@ -1101,9 +1100,10 @@
    (auto)
 
 lemma logical_symmetry:
-  assumes "\<Gamma> \<turnstile> s is t : T"
+  assumes a: "\<Gamma> \<turnstile> s is t : T"
   shows "\<Gamma> \<turnstile> t is s : T"
-using assms by (nominal_induct arbitrary: \<Gamma> s t rule:ty.induct, auto simp add: algorithmic_symmetry)
+using a 
+by (nominal_induct arbitrary: \<Gamma> s t rule:ty.induct) (auto simp add: algorithmic_symmetry)
 
 lemma logical_transitivity:
   assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma> \<turnstile> t is u : T" 
@@ -1132,19 +1132,19 @@
 qed (auto)
 
 lemma logical_weak_head_closure:
-  assumes "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" "t' \<leadsto> t"
+  assumes a: "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" "t' \<leadsto> t"
   shows "\<Gamma> \<turnstile> s' is t' : T"
-using assms 
-apply (nominal_induct arbitrary: \<Gamma> s t s' t' rule:ty.induct)
-apply (auto simp add: algorithmic_weak_head_closure)
-apply (blast)
+using a
+apply(nominal_induct arbitrary: \<Gamma> s t s' t' rule:ty.induct)
+apply(auto simp add: algorithmic_weak_head_closure)
+apply(blast)
 done
 
 lemma logical_weak_head_closure':
   assumes "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" 
   shows "\<Gamma> \<turnstile> s' is t : T"
 using assms
-proof (nominal_induct arbitrary: \<Gamma> s t s' rule:ty.induct)
+proof (nominal_induct arbitrary: \<Gamma> s t s' rule: ty.induct)
   case (TBase  \<Gamma> s t s')
   then show ?case by force
 next
@@ -1243,7 +1243,6 @@
 ultimately show "\<Gamma>' \<turnstile> \<gamma><Lam [x].t2> is \<theta><Lam [x].t2> : T1\<rightarrow>T2" using fs by auto 
 qed (auto)
 
- 
 theorem fundamental_theorem_2:
   assumes h1: "\<Gamma> \<turnstile> s == t : T" 
   and     h2: "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>"
@@ -1321,7 +1320,8 @@
     then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using h2 logical_subst_monotonicity by blast
     then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext hl fs by blast
     then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><App s (Var x)>  is (x,t')#\<theta><App t (Var x)> : T2" using ih by blast
-    then have "\<Gamma>'' \<turnstile> App (((x,s')#\<gamma>)<s>)  (((x,s')#\<gamma>)<(Var x)>) is App ((x,t')#\<theta><t>) ((x,t')#\<theta><(Var x)>) : T2" by auto
+    then have "\<Gamma>'' \<turnstile> App (((x,s')#\<gamma>)<s>) (((x,s')#\<gamma>)<(Var x)>) is App ((x,t')#\<theta><t>) ((x,t')#\<theta><(Var x)>) : T2"
+      by auto
     then have "\<Gamma>'' \<turnstile> App ((x,s')#\<gamma><s>) s'  is App ((x,t')#\<theta><t>) t' : T2" by auto
     then have "\<Gamma>'' \<turnstile> App (\<gamma><s>) s' is App (\<theta><t>) t' : T2" using fs fresh_psubst_simpl by auto
   }
@@ -1346,12 +1346,12 @@
   then show  "\<Gamma> \<turnstile> s <=> t : T" using main_lemma by simp
 qed
 
-(* Soundness is left as an exercise - like in the book*)
+(* Soundness is left as an exercise - like in the book - for the avid formalist 
 
-(*
 theorem soundness:
-  shows "\<lbrakk> \<Gamma> \<turnstile> s <=> t : T ; \<Gamma> \<turnstile> t : T ; \<Gamma> \<turnstile> s : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == t : T"
-  and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> t : T ; \<Gamma> \<turnstile> s : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == t : T"
+  shows "\<lbrakk>\<Gamma> \<turnstile> s <=> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == t : T"
+  and   "\<lbrakk>\<Gamma> \<turnstile> s \<leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == t : T"
+
 *)
 
 end