1 theory Tutorial4s

     2 imports Tutorial1s

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

   119     using ctx_compose ctx_composes.simps filling.simps by simp

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

   121 next

   122   case (m2 v t2 Es)

   123   have "val v" by fact

   124   have "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> = (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>"  

   125     using ctx_compose ctx_composes.simps filling.simps by simp

   126   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

   127 next

   128   case (m3 v x t Es)

   129   have aa: "val v" by fact

   130   have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> = Es\<down>\<lbrakk>App (Lam [x]. t) v\<rbrakk>" 

   131     using ctx_compose ctx_composes.simps filling.simps by simp

   132   then have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" 

   133     using better_cbv1[OF aa] cbv_in_ctx by simp

   134   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

   135 qed

   136 

   137 text {* 

   138   It is not difficult to extend the lemma above to

   139   arbitrary reductions sequences of the CK machine. *}

   140 

   141 lemma machines_implies_cbvs_ctx:

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

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

   144 using a machine_implies_cbvs_ctx 

   145 by (induct) (blast)+

   146 

   147 text {* 

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

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

   150   a corresponding cbv-reduction sequence. 

   151 *}

   152 

   153 corollary machines_implies_cbvs:

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

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

   156 proof - 

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

   158      using a machines_implies_cbvs_ctx by blast

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

   160 qed

   161 

   162 text {*

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

   164   relation. For this we need two auxiliary lemmas. 

   165 *}

   166 

   167 lemma eval_val:

   168   assumes a: "val t"

   169   shows "t \<Down> t"

   170 using a by (induct) (auto)

   171 

   172 

   173 lemma e_App_elim:

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

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

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

   177 

   178 

   179 subsection {* EXERCISE *}

   180 

   181 text {*

   182   Complete the first and second case in the 

   183   proof below. 

   184 *}

   185 

   186 lemma cbv_eval:

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

   188   shows "t1 \<Down> t3"

   189 using a

   190 proof(induct arbitrary: t3)

   191   case (cbv1 v x t t3)

   192   have a1: "val v" by fact

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

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

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

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

   197 next

   198   case (cbv2 t t' t2 t3)

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

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

   201   then obtain x t'' v' 

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

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

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

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

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

   207 qed (auto elim!: e_App_elim)

   208 

   209 

   210 text {* 

   211   Next we extend the lemma above to arbitray initial

   212   sequences of cbv-reductions. *}

   213 

   214 lemma cbvs_eval:

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

   216   shows "t1 \<Down> t3"

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

   218 

   219 text {* 

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

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

   222 *}

   223 

   224 lemma cbvs_implies_eval:

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

   226   shows "t \<Down> v"

   227 using a

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

   229 

   230 text {* 

   231   All facts tied together give us the desired property about

   232   machines. 

   233 *}

   234 

   235 theorem machines_implies_eval:

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

   237   and     b: "val t2" 

   238   shows "t1 \<Down> t2"

   239 proof -

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

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

   242 qed

   243 

   244 

   245 

   246 

   247 end

   248