author urbanc Wed, 17 Jan 2007 19:29:55 +0100 changeset 22082 b1be13d32efd parent 22081 fd2b69c2f15d child 22083 4bfd987b005c
tuned a bit the proofs
```--- 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)"
-
-(* 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(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"
-  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 {*
[(("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 (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"
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 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)

-  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 (blast)
+using a
+apply(nominal_induct arbitrary: \<Gamma> s t s' t' rule:ty.induct)
+apply(blast)
done

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```