1 

     2 theory Tutorial4

     3 imports Tutorial1 Tutorial2

     4 begin

     5 

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

     7 

     8 

     9 inductive

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

    11 where

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

    13 | cbv2: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2"

    14 | cbv3: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'"

    15 

    16 inductive 

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

    18 where

    19   cbvs1: "e \<longrightarrow>cbv* e"

    20 | cbvs2: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"

    21 

    22 declare cbv.intros[intro] cbv_star.intros[intro]

    23 

    24 subsection {* EXERCISE 11 *}

    25 

    26 text {*

    27   Show that cbv* is transitive, by filling the gaps in the 

    28   proof below.

    29 *}

    30 

    31 lemma cbvs3 [intro]:

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

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

    34 using a 

    35 proof (induct) 

    36   case (cbvs1 e1)

    37   have asm: "e1 \<longrightarrow>cbv* e3" by fact

    38   show "e1 \<longrightarrow>cbv* e3" sorry

    39 next

    40   case (cbvs2 e1 e2 e3')

    41   have "e1 \<longrightarrow>cbv e2" by fact

    42   have "e2 \<longrightarrow>cbv* e3'" by fact

    43   have "e3' \<longrightarrow>cbv* e3 \<Longrightarrow> e2 \<longrightarrow>cbv* e3" by fact

    44   have "e3' \<longrightarrow>cbv* e3" by fact

    45 

    46   show "e1 \<longrightarrow>cbv* e3" sorry

    47 qed 

    48 

    49 

    50 text {*

    51   In order to help establishing the property that the machine

    52   calculates a nomrmalform that corresponds to the evaluation 

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

    54 *}

    55 

    56 

    57 equivariance val

    58 equivariance cbv

    59 nominal_inductive cbv

    60   avoids cbv1: "x"

    61   unfolding fresh_star_def

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

    63 

    64 text {*

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

    66   this relation with the additional freshness constraint

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

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

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

    70   usual rule. 

    71 *}

    72 

    73 lemma subst_rename: 

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

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

    76 using a 

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

    78    (auto simp add: lam.fresh fresh_at_base)

    79 

    80 

    81 lemma better_cbv1 [intro]: 

    82   assumes a: "val v" 

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

    84 proof -

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

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

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

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

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

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

    91 qed

    92 

    93 

    94 

    95 subsection {* EXERCISE 12 *}

    96 

    97 text {*  

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

    99 *}

   100 

   101 lemma cbv_in_ctx:

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

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

   104 using a

   105 proof (induct E)

   106   case Hole

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

   108   show "\<box>\<lbrakk>t\<rbrakk> \<longrightarrow>cbv \<box>\<lbrakk>t'\<rbrakk>" sorry

   109 next

   110   case (CAppL E s)

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

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

   113 

   114   show "(CAppL E s)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppL E s)\<lbrakk>t'\<rbrakk>" sorry

   115 next

   116   case (CAppR s E)

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

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

   119   

   120   show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" sorry

   121 qed

   122 

   123 section {* EXERCISE 13 *} 

   124  

   125 text {*

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

   127   establish the follwoing property:

   128 *}

   129 

   130 lemma machine_implies_cbvs_ctx:

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

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

   133 using a 

   134 proof (induct)

   135   case (m1 t1 t2 Es)

   136 

   137   show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>" sorry

   138 next

   139   case (m2 v t2 Es)

   140   have "val v" by fact

   141 

   142   show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" sorry

   143 next

   144   case (m3 v x t Es)

   145   have "val v" by fact

   146  

   147   show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" sorry

   148 qed

   149 

   150 text {* 

   151   It is not difficult to extend the lemma above to

   152   arbitrary reductions sequences of the machine. 

   153 *}

   154 

   155 lemma machines_implies_cbvs_ctx:

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

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

   158 using a machine_implies_cbvs_ctx 

   159 by (induct) (blast)+

   160 

   161 text {* 

   162   So whenever we let the machine start in an initial

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

   164   a corresponding cbv-reduction sequence. 

   165 *}

   166 

   167 corollary machines_implies_cbvs:

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

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

   170 proof - 

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

   172      using a machines_implies_cbvs_ctx by blast

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

   174 qed

   175 

   176 text {*

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

   178   relation. For this we need one auxiliary lemma about

   179   inverting the e_App rule. 

   180 *}

   181 

   182 

   183 lemma e_App_elim:

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

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

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

   187 

   188 

   189 subsection {* EXERCISE 13 *}

   190 

   191 text {*

   192   Complete the first and second case in the 

   193   proof below. 

   194 *}

   195 

   196 lemma cbv_eval:

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

   198   shows "t1 \<Down> t3"

   199 using a

   200 proof(induct arbitrary: t3)

   201   case (cbv1 v x t t3)

   202   have a1: "val v" by fact

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

   204 

   205   show "App (Lam [x].t) v \<Down> t3" sorry

   206 next

   207   case (cbv2 t t' t2 t3)

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

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

   210   then obtain x t'' v' 

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

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

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

   214   

   215   show "App t t2 \<Down> t3" sorry

   216 qed (auto elim!: e_App_elim)

   217 

   218 

   219 text {* 

   220   Next we extend the lemma above to arbitray initial

   221   sequences of cbv-reductions. 

   222 *}

   223 

   224 lemma cbvs_eval:

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

   226   shows "t1 \<Down> t3"

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

   228 

   229 text {* 

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

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

   232 

   233   This proof is not by induction. So we have to set up the proof

   234   with

   235 

   236     proof -

   237     

   238   in order to prevent Isabelle from applying a default introduction   

   239   rule.

   240 *}

   241 

   242 lemma cbvs_implies_eval:

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

   244   and     b: "val v"

   245   shows "t \<Down> v"

   246 proof - 

   247   have "v \<Down> v" using b eval_val by simp

   248   then show "t \<Down> v" using a cbvs_eval by auto

   249 qed

   250 

   251 section {* EXERCISE 15 *}

   252 

   253 text {* 

   254   All facts tied together give us the desired property 

   255   about machines: we know that a machines transitions

   256   correspond to cbvs transitions, and with the lemma

   257   above they correspond to an eval judgement.

   258 *}

   259 

   260 theorem machines_implies_eval:

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

   262   and     b: "val t2" 

   263   shows "t1 \<Down> t2"

   264 proof - 

   265   

   266   show "t1 \<Down> t2" sorry

   267 qed

   268 

   269 end

   270