# HG changeset patch
# User urbanc
# Date 1213669190 -7200
# Node ID e5787c5be196d5af1e545f54446d5cdae142f797
# Parent  df85326af57c244ab35be057042d20e641b173b1
added a progress lemma and tuned some comments

diff -r df85326af57c -r e5787c5be196 src/HOL/Nominal/Examples/CK_Machine.thy
--- a/src/HOL/Nominal/Examples/CK_Machine.thy	Mon Jun 16 22:20:59 2008 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Tue Jun 17 04:19:50 2008 +0200
@@ -9,15 +9,17 @@
   This theory establishes soundness and completeness for a CK-machine
   with respect to a cbv-big-step semantics. The language includes 
   functions, recursion, booleans and numbers. In the soundness proof 
-  the small-step cbv-reduction relation is used to get the induction
-  through. Type preservation is proved for the machine and also for
-  the small- and big-step semantics.
+  the small-step cbv-reduction relation is used in order to get the 
+  induction through. The type-preservation property is proved for the 
+  machine and  also for the small- and big-step semantics. Finally, 
+  the progress property is proved for the small-step semantics.
 
-  The theory is inspired by notes of Roshan James from Indiana University
-  and the lecture notes by Andy Pitts for his semantics course. See
+  The development is inspired by notes about context machines written
+  by Roshan James (Indiana University) and also by the lecture notes 
+  written by Andy Pitts for his semantics course. See
   
-  http://www.cs.indiana.edu/~rpjames/lm.pdf
-  http://www.cl.cam.ac.uk/teaching/2001/Semantics/
+     http://www.cs.indiana.edu/~rpjames/lm.pdf
+     http://www.cl.cam.ac.uk/teaching/2001/Semantics/
 
 *}
 
@@ -28,12 +30,12 @@
 | APP "lam" "lam" 
 | LAM "\<guillemotleft>name\<guillemotright>lam" ("LAM [_]._")
 | NUM "nat"
-| DIFF "lam" "lam" ("_ -- _")
-| PLUS "lam" "lam" ("_ ++ _")
+| DIFF "lam" "lam" ("_ -- _")    (* subtraction *) 
+| PLUS "lam" "lam" ("_ ++ _")    (* addition *)
 | TRUE
 | FALSE
 | IF "lam" "lam" "lam"
-| FIX "\<guillemotleft>name\<guillemotright>lam" ("FIX [_]._")  
+| FIX "\<guillemotleft>name\<guillemotright>lam" ("FIX [_]._")  (* recursion *)
 | ZET "lam"                      (* zero test *)
 | EQI "lam" "lam"                (* equality test on numbers *)
 
@@ -94,6 +96,8 @@
   | CEQIL "ctx" "lam"
   | CEQIR "lam" "ctx"
 
+text {* The operation of filling a term into a context: *} 
+
 fun
   filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>")
 where
@@ -109,6 +113,8 @@
 | "(CEQIL E t')\<lbrakk>t\<rbrakk> = EQI (E\<lbrakk>t\<rbrakk>) t'"
 | "(CEQIR t' E)\<lbrakk>t\<rbrakk> = EQI t' (E\<lbrakk>t\<rbrakk>)"
 
+text {* The operation of composing two contexts: *}
+
 fun 
  ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _")
 where
@@ -128,13 +134,15 @@
   shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
 by (induct E1 rule: ctx.induct) (auto)
 
+text {* Composing a list (stack) of contexts. *}
+
 fun
   ctx_composes :: "ctx list \<Rightarrow> ctx" ("_\<down>")
 where
     "[]\<down> = \<box>"
   | "(E#Es)\<down> = (Es\<down>) \<circ> E"
 
-section {* CK Machine *}
+section {* The CK-Machine *}
 
 inductive
   val :: "lam\<Rightarrow>bool" 
@@ -186,7 +194,7 @@
   shows "<e1,Es1> \<mapsto>* <e2,Es2>"
 using a by (rule ms2) (rule ms1)
 
-section {* Evaluation Relation *}
+section {* The Evaluation Relation (Big-Step Semantics) *}
 
 inductive
   eval :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<Down> _") 
@@ -229,6 +237,8 @@
   shows "t \<Down> t"
 using a by (induct) (auto)
 
+text {* The Completeness Property: *}
+
 theorem eval_implies_machine_star_ctx:
   assumes a: "t \<Down> t'"
   shows "<t,Es> \<mapsto>* <t',Es>"
@@ -236,14 +246,12 @@
 by (induct arbitrary: Es)
    (metis eval_to machine.intros ms1 ms2 ms3 ms4 v_LAM)+
 
-text {* Completeness Property *}
-
 corollary eval_implies_machine_star:
   assumes a: "t \<Down> t'"
   shows "<t,[]> \<mapsto>* <t',[]>"
 using a by (auto dest: eval_implies_machine_star_ctx)
 
-section {* CBV Reduction Relation *}
+section {* The CBV Reduction Relation (Small-Step Semantics) *}
 
 lemma less_eqvt[eqvt]:
   fixes pi::"name prm"
@@ -254,7 +262,7 @@
 inductive
   cbv :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>cbv _") 
 where
-  cbv1': "\<lbrakk>val v; x\<sharp>v\<rbrakk> \<Longrightarrow> APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]"
+  cbv1: "\<lbrakk>val v; x\<sharp>v\<rbrakk> \<Longrightarrow> APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]"
 | cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> APP t t2 \<longrightarrow>cbv APP t' t2"
 | cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> APP t2 t \<longrightarrow>cbv APP t2 t'"
 | cbv4[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t -- t2 \<longrightarrow>cbv t' -- t2"
@@ -279,14 +287,14 @@
 nominal_inductive cbv
  by (simp_all add: abs_fresh fresh_fact)
 
-lemma cbv1[intro]: 
+lemma better_cbv1[intro]: 
   assumes a: "val v" 
   shows "APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]"
 proof -
   obtain y::"name" where fs: "y\<sharp>(x,t,v)" by (rule exists_fresh, rule fin_supp, blast)
   have "APP (LAM [x].t) v = APP (LAM [y].([(y,x)]\<bullet>t)) v" using fs
     by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
-  also have "\<dots> \<longrightarrow>cbv  ([(y,x)]\<bullet>t)[y::=v]" using fs a by (auto simp add: cbv.eqvt cbv1')
+  also have "\<dots> \<longrightarrow>cbv  ([(y,x)]\<bullet>t)[y::=v]" using fs a by (auto simp add: cbv.eqvt cbv1)
   also have "\<dots> = t[x::=v]" using fs by (simp add: subst_rename[symmetric])
   finally show "APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]" by simp
 qed
@@ -342,7 +350,7 @@
 by (induct)
    (auto simp add: eval_val cbv_star_eval dest: cbvs2)
 
-text {* Soundness Property *}
+text {* The Soundness Property *}
 
 theorem machine_star_implies_eval:
   assumes a: "<t1,[]> \<mapsto>* <t2,[]>" 
@@ -355,6 +363,8 @@
 
 section {* Typing *}
 
+text {* Types *}
+
 nominal_datatype ty =
   tVAR "string"
 | tBOOL 
@@ -370,13 +380,19 @@
 by (induct T rule: ty.induct)
    (auto simp add: fresh_string)
 
+text {* Typing Contexts *}
+
 types tctx = "(name\<times>ty) list"
 
+text {* Sub-Typing Contexts *}
+
 abbreviation
   "sub_tctx" :: "tctx \<Rightarrow> tctx \<Rightarrow> bool" ("_ \<subseteq> _") 
 where
   "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^isub>1 \<longrightarrow> x \<in> set \<Gamma>\<^isub>2"
 
+text {* Valid Typing Contexts *}
+
 inductive
   valid :: "tctx \<Rightarrow> bool"
 where
@@ -409,7 +425,7 @@
 using a1 a2 a3
 by (induct) (auto simp add: fresh_set fresh_prod fresh_atm)
 
-section {* Typing Relation *}
+section {* The Typing Relation *}
 
 inductive
   typing :: "tctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _") 
@@ -435,6 +451,9 @@
   "\<Gamma> \<turnstile> ZET t : T"
   "\<Gamma> \<turnstile> EQI t1 t2 : T"
   "\<Gamma> \<turnstile> APP t1 t2 : T"
+  "\<Gamma> \<turnstile> TRUE : T"
+  "\<Gamma> \<turnstile> FALSE : T"
+  "\<Gamma> \<turnstile> NUM n : T"
 declare lam.inject[simp del]
 
 equivariance typing
@@ -457,7 +476,7 @@
 by (cases rule: typing.strong_cases) 
    (auto simp add: alpha lam.inject abs_fresh ty_fresh)
 
-section {* Type Preservation for the CBV Reduction Relation *}
+section {* The Type-Preservation Property for the CBV Reduction Relation *}
 
 lemma weakening: 
   fixes \<Gamma>1 \<Gamma>2::"tctx"
@@ -517,7 +536,7 @@
 using a b
 by (induct) (auto intro: cbv_type_preservation)
 
-section {* Type Preservation for the Machine and Evaluation Relation *}
+section {* The Type-Preservation Property for the Machine and Evaluation Relation *}
 
 theorem machine_type_preservation:
   assumes a: "<t,[]> \<mapsto>* <t',[]>"
@@ -537,6 +556,35 @@
   then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation)
 qed
 
+text {* The Progress Property *}
+
+lemma canonical_tARR[dest]:
+  assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"
+  and     b: "val t"
+  shows "\<exists>x t'. t = LAM [x].t'"
+using b a by (induct) (auto) 
+
+lemma canonical_tINT[dest]:
+  assumes a: "[] \<turnstile> t : tINT"
+  and     b: "val t"
+  shows "\<exists>n. t = NUM n"
+using b a 
+by (induct) (auto simp add: fresh_list_nil)
+
+lemma canonical_tBOOL[dest]:
+  assumes a: "[] \<turnstile> t : tBOOL"
+  and     b: "val t"
+  shows "t = TRUE \<or> t = FALSE"
+using b a 
+by (induct) (auto simp add: fresh_list_nil)
+
+theorem progress:
+  assumes a: "[] \<turnstile> t : T"
+  shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"
+using a
+by (induct \<Gamma>\<equiv>"[]::tctx" t T)
+   (auto dest!: canonical_tINT intro!: cbv.intros gr0I)
+
 end