1.1 --- a/src/HOL/Nominal/Examples/Contexts.thy	Thu Jun 12 09:37:13 2008 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Contexts.thy	Thu Jun 12 09:41:13 2008 +0200
     1.3 @@ -9,8 +9,7 @@
     1.4    We show here that the Plotkin-style of defining
     1.5    beta-reduction (based on congruence rules) is
     1.6    equivalent to the Felleisen-Hieb-style representation 
     1.7 -  (based on contexts). We also define cbv-evaluation 
     1.8 -  via a CK-machine described by Roshan James.
     1.9 +  (based on contexts). 
    1.10    
    1.11    The interesting point in this theory is that contexts 
    1.12    do not contain any binders. On the other hand the operation 
    1.13 @@ -24,6 +23,7 @@
    1.14  text {* 
    1.15    Lambda-Terms - the Lam-term constructor binds a name
    1.16  *}
    1.17 +
    1.18  nominal_datatype lam = 
    1.19      Var "name"
    1.20    | App "lam" "lam"
    1.21 @@ -40,7 +40,7 @@
    1.22    | CAppR "lam" "ctx" 
    1.23    | CLam "name" "ctx"  ("CLam [_]._" [100,100] 100) 
    1.24  
    1.25 -text {* Capture-avoiding substitution *}
    1.26 +text {* Capture-Avoiding Substitution *}
    1.27  
    1.28  consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
    1.29  
    1.30 @@ -141,68 +141,11 @@
    1.31    then show  "App (Lam [x].t) t' \<longrightarrow>x t[x::=t']" by simp
    1.32  qed (metis ctx_red_in_ctx filling.simps)+ (* found by SledgeHammer *)
    1.33  
    1.34 +
    1.35  lemma ctx_existence:
    1.36    assumes a: "t \<longrightarrow>o t'"
    1.37    shows "\<exists>C s s'. t = C\<lbrakk>s\<rbrakk> \<and> t' = C\<lbrakk>s'\<rbrakk> \<and> s \<longrightarrow>o s'"
    1.38  using a
    1.39  by (induct) (metis cong_red.intros filling.simps)+
    1.40  
    1.41 -section {* We now use context in a CBV list machine *}
    1.42 -
    1.43 -text {* First, a function that composes a list of contexts. *}
    1.44 -
    1.45 -primrec
    1.46 -  ctx_composes :: "ctx list \<Rightarrow> ctx" ("_\<down>" [80] 80)
    1.47 -where
    1.48 -    "[]\<down> = \<box>"
    1.49 -  | "(E#Es)\<down> = (Es\<down>) \<circ> E"    
    1.50 -
    1.51 -text {* Values *}
    1.52 -
    1.53 -inductive
    1.54 -  val :: "lam\<Rightarrow>bool" 
    1.55 -where
    1.56 -   v_Lam[intro]: "val (Lam [x].e)"
    1.57 - | v_Var[intro]: "val (Var x)"
    1.58 -
    1.59 -text {* CBV-reduction using contexts *}
    1.60 -
    1.61 -inductive
    1.62 -  cbv :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>cbv _" [80,80] 80) 
    1.63 -where
    1.64 -  cbv_beta[intro]: "val v \<Longrightarrow> E\<lbrakk>App (Lam [x].e) v\<rbrakk> \<longrightarrow>cbv E\<lbrakk>e[x::=v]\<rbrakk>"
    1.65 -
    1.66 -text {* reflexive, transitive closure of CBV reduction *}
    1.67 -inductive 
    1.68 -  "cbv_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>cbv* _" [80,80] 80)
    1.69 -where
    1.70 -  cbvs1[intro]: "e \<longrightarrow>cbv* e"
    1.71 -| cbvs2[intro]: "e \<longrightarrow>cbv e' \<Longrightarrow> e \<longrightarrow>cbv* e'"
    1.72 -| cbvs3[intro,trans]: "\<lbrakk>e1\<longrightarrow>cbv* e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
    1.73 -
    1.74 -text {* A little CK-machine, which builds up a list of evaluation contexts. *}
    1.75 -
    1.76 -inductive
    1.77 -  machine :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto> <_,_>" [60,60,60,60] 60)
    1.78 -where
    1.79 -  m1[intro]: "<App e1 e2, Es> \<mapsto> <e1,(CAppL \<box> e2)#Es>"
    1.80 -| m2[intro]: "val v \<Longrightarrow> <v,(CAppL \<box> e2)#Es> \<mapsto> <e2,(CAppR v \<box>)#Es>"
    1.81 -| m3[intro]: "val v \<Longrightarrow> <v,(CAppR (Lam [x].e) \<box>)#Es> \<mapsto> <e[x::=v],Es>"
    1.82 -
    1.83 -lemma machine_red_implies_cbv_reds_aux:
    1.84 -  assumes a: "<e,Es> \<mapsto> <e',Es'>"
    1.85 -  shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
    1.86 -using a by (induct) (auto simp add: ctx_compose)
    1.87 -
    1.88 -lemma machine_execution_implies_cbv_reds:
    1.89 -  assumes a: "<e,[]> \<mapsto> <e',[]>"
    1.90 -  shows "e \<longrightarrow>cbv* e'"
    1.91 -using a by (auto dest: machine_red_implies_cbv_reds_aux)
    1.92 -
    1.93 -text {*
    1.94 -  One would now like to show something about the opposite
    1.95 -  direction, by according to Amr Sabry this amounts to
    1.96 -  showing a standardisation lemma, which is hard.
    1.97 -  *}
    1.98 -
    1.99  end