1 theory Tutorial4

     2 imports Tutorial1

     3 begin

     4 

     5 section {* The CBV Reduction Relation (Small-Step Semantics) *}

     6 

     7 text {*

     8   In order to help establishing the property that the CK Machine

     9   calculates a nomrmalform that corresponds to the evaluation 

    10   relation, we introduce the call-by-value small-step semantics.

    11 *}

    12 

    13 inductive

    14   cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60) 

    15 where

    16   cbv1: "\<lbrakk>val v; atom x \<sharp> v\<rbrakk> \<Longrightarrow> App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]"

    17 | cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2"

    18 | cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'"

    19 

    20 equivariance val

    21 equivariance cbv

    22 nominal_inductive cbv

    23   avoids cbv1: "x"

    24   unfolding fresh_star_def

    25   by (simp_all add: lam.fresh Abs_fresh_iff fresh_Pair fresh_fact)

    26 

    27 text {*

    28   In order to satisfy the vc-condition we have to formulate

    29   this relation with the additional freshness constraint

    30   atom x \<sharp> v. Although this makes the definition vc-ompatible, it

    31   makes the definition less useful. We can with a little bit of 

    32   pain show that the more restricted rule is equivalent to the

    33   usual rule. 

    34 *}

    35 

    36 lemma subst_rename: 

    37   assumes a: "atom y \<sharp> t"

    38   shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet> t)[y ::= s]"

    39 using a 

    40 by (nominal_induct t avoiding: x y s rule: lam.strong_induct)

    41    (auto simp add: lam.fresh fresh_at_base)

    42 

    43 

    44 lemma better_cbv1 [intro]: 

    45   assumes a: "val v" 

    46   shows "App (Lam [x].t) v \<longrightarrow>cbv t[x::=v]"

    47 proof -

    48   obtain y::"name" where fs: "atom y \<sharp> (x, t, v)" by (rule obtain_fresh)

    49   have "App (Lam [x].t) v = App (Lam [y].((y \<leftrightarrow> x) \<bullet> t)) v" using fs

    50     by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)

    51   also have "\<dots> \<longrightarrow>cbv ((y \<leftrightarrow> x) \<bullet> t)[y ::= v]" using fs a cbv1 by auto

    52   also have "\<dots> = t[x ::= v]" using fs subst_rename[symmetric] by simp

    53   finally show "App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]" by simp

    54 qed

    55 

    56 text {*

    57   The transitive closure of the cbv-reduction relation: 

    58 *}

    59 

    60 inductive 

    61   "cbvs" :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>cbv* _" [60, 60] 60)

    62 where

    63   cbvs1[intro]: "e \<longrightarrow>cbv* e"

    64 | cbvs2[intro]: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"

    65 

    66 lemma cbvs3 [intro]:

    67   assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"

    68   shows "e1 \<longrightarrow>cbv* e3"

    69 using a by (induct) (auto) 

    70 

    71 

    72 subsection {* EXERCISE 8 *}

    73 

    74 text {*  

    75   If more simple exercises are needed, then complete the following proof. 

    76 *}

    77 

    78 lemma cbv_in_ctx:

    79   assumes a: "t \<longrightarrow>cbv t'"

    80   shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>"

    81 using a

    82 proof (induct E)

    83   case Hole

    84   have "t \<longrightarrow>cbv t'" by fact

    85   then show "\<box>\<lbrakk>t\<rbrakk> \<longrightarrow>cbv \<box>\<lbrakk>t'\<rbrakk>" by simp

    86 next

    87   case (CAppL E s)

    88   have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact

    89   moreover

    90   have "t \<longrightarrow>cbv t'" by fact

    91   ultimately 

    92   have "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by simp

    93   then show "(CAppL E s)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppL E s)\<lbrakk>t'\<rbrakk>" by auto

    94 next

    95   case (CAppR s E)

    96   have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact

    97   moreover

    98   have a: "t \<longrightarrow>cbv t'" by fact

    99   ultimately 

   100   have "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by simp

   101   then show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" by auto

   102 qed

   103 

   104 section {* EXERCISE 9 *} 

   105  

   106 text {*

   107   The point of the cbv-reduction was that we can easily relatively 

   108   establish the follwoing property:

   109 *}

   110 

   111 lemma machine_implies_cbvs_ctx:

   112   assumes a: "<e, Es> \<mapsto> <e', Es'>"

   113   shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"

   114 using a 

   115 proof (induct)

   116   case (m1 t1 t2 Es)

   117 thm machine.intros thm cbv2

   118   have "Es\<down>\<lbrakk>App t1 t2\<rbrakk> = (Es\<down> \<odot> CAppL \<box> t2)\<lbrakk>t1\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp

   119   then show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>" using cbvs.intros by simp

   120 next

   121   case (m2 v t2 Es)

   122   have "val v" by fact

   123   have "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> = (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>"  using ctx_compose ctx_composes.simps filling.simps by simp

   124   then show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" using cbvs.intros by simp

   125 next

   126   case (m3 v x t Es)

   127   have aa: "val v" by fact

   128   have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> = Es\<down>\<lbrakk>App (Lam [x]. t) v\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp

   129   then have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" using better_cbv1[OF aa] cbv_in_ctx by simp

   130   then show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" using cbvs.intros by blast

   131 qed

   132 

   133 text {* 

   134   It is not difficult to extend the lemma above to

   135   arbitrary reductions sequences of the CK machine. *}

   136 

   137 lemma machines_implies_cbvs_ctx:

   138   assumes a: "<e, Es> \<mapsto>* <e', Es'>"

   139   shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"

   140 using a machine_implies_cbvs_ctx 

   141 by (induct) (blast)+

   142 

   143 text {* 

   144   So whenever we let the CL machine start in an initial

   145   state and it arrives at a final state, then there exists

   146   a corresponding cbv-reduction sequence. 

   147 *}

   148 

   149 corollary machines_implies_cbvs:

   150   assumes a: "<e, []> \<mapsto>* <e', []>"

   151   shows "e \<longrightarrow>cbv* e'"

   152 proof - 

   153   have "[]\<down>\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* []\<down>\<lbrakk>e'\<rbrakk>" 

   154      using a machines_implies_cbvs_ctx by blast

   155   then show "e \<longrightarrow>cbv* e'" by simp  

   156 qed

   157 

   158 text {*

   159   We now want to relate the cbv-reduction to the evaluation

   160   relation. For this we need two auxiliary lemmas. 

   161 *}

   162 

   163 lemma eval_val:

   164   assumes a: "val t"

   165   shows "t \<Down> t"

   166 using a by (induct) (auto)

   167 

   168 

   169 lemma e_App_elim:

   170   assumes a: "App t1 t2 \<Down> v"

   171   obtains x t v' where "t1 \<Down> Lam [x].t" "t2 \<Down> v'" "t[x::=v'] \<Down> v"

   172 using a by (cases) (auto simp add: lam.eq_iff lam.distinct) 

   173 

   174 

   175 subsection {* EXERCISE *}

   176 

   177 text {*

   178   Complete the first and second case in the 

   179   proof below. 

   180 *}

   181 

   182 lemma cbv_eval:

   183   assumes a: "t1 \<longrightarrow>cbv t2" "t2 \<Down> t3"

   184   shows "t1 \<Down> t3"

   185 using a

   186 proof(induct arbitrary: t3)

   187   case (cbv1 v x t t3)

   188   have a1: "val v" by fact

   189   have a2: "t[x ::= v] \<Down> t3" by fact

   190   have a3: "Lam [x].t \<Down> Lam [x].t" by auto

   191   have a4: "v \<Down> v" using a1 eval_val by auto

   192   show "App (Lam [x].t) v \<Down> t3" using a3 a4 a2 by auto 

   193 next

   194   case (cbv2 t t' t2 t3)

   195   have ih: "\<And>t3. t' \<Down> t3 \<Longrightarrow> t \<Down> t3" by fact

   196   have "App t' t2 \<Down> t3" by fact

   197   then obtain x t'' v' 

   198     where a1: "t' \<Down> Lam [x].t''" 

   199       and a2: "t2 \<Down> v'" 

   200       and a3: "t''[x ::= v'] \<Down> t3" by (rule e_App_elim) 

   201   have "t \<Down>  Lam [x].t''" using ih a1 by auto 

   202   then show "App t t2 \<Down> t3" using a2 a3 by auto

   203 qed (auto elim!: e_App_elim)

   204 

   205 

   206 text {* 

   207   Next we extend the lemma above to arbitray initial

   208   sequences of cbv-reductions. *}

   209 

   210 lemma cbvs_eval:

   211   assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3"

   212   shows "t1 \<Down> t3"

   213 using a by (induct) (auto intro: cbv_eval)

   214 

   215 text {* 

   216   Finally, we can show that if from a term t we reach a value 

   217   by a cbv-reduction sequence, then t evaluates to this value. 

   218 *}

   219 

   220 lemma cbvs_implies_eval:

   221   assumes a: "t \<longrightarrow>cbv* v" "val v"

   222   shows "t \<Down> v"

   223 using a

   224 by (induct) (auto intro: eval_val cbvs_eval)

   225 

   226 text {* 

   227   All facts tied together give us the desired property about

   228   machines. 

   229 *}

   230 

   231 theorem machines_implies_eval:

   232   assumes a: "<t1, []> \<mapsto>* <t2, []>" 

   233   and     b: "val t2" 

   234   shows "t1 \<Down> t2"

   235 proof -

   236   have "t1 \<longrightarrow>cbv* t2" using a machines_implies_cbvs by simp

   237   then show "t1 \<Down> t2" using b cbvs_implies_eval by simp

   238 qed

   239 

   240 

   241 

   242 

   243 end

   244