1 

     2 theory Tutorial4

     3 imports Tutorial1

     4 begin

     5 

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

     7 

     8 text {*

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

    10   calculates a nomrmalform that corresponds to the evaluation 

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

    12 *}

    13 

    14 inductive

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

    16 where

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

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

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

    20 

    21 equivariance val

    22 equivariance cbv

    23 nominal_inductive cbv

    24   avoids cbv1: "x"

    25   unfolding fresh_star_def

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

    27 

    28 text {*

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

    30   this relation with the additional freshness constraint

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

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

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

    34   usual rule. 

    35 *}

    36 

    37 lemma subst_rename: 

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

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

    40 using a 

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

    42    (auto simp add: lam.fresh fresh_at_base)

    43 

    44 

    45 lemma better_cbv1 [intro]: 

    46   assumes a: "val v" 

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

    48 proof -

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

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

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

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

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

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

    55 qed

    56 

    57 text {*

    58   The transitive closure of the cbv-reduction relation: 

    59 *}

    60 

    61 inductive 

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

    63 where

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

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

    66 

    67 lemma cbvs3 [intro]:

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

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

    70 using a by (induct) (auto) 

    71 

    72 

    73 subsection {* EXERCISE 8 *}

    74 

    75 text {*  

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

    77 *}

    78 

    79 lemma cbv_in_ctx:

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

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

    82 using a

    83 proof (induct E)

    84   case Hole

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

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

    87 next

    88   case (CAppL E s)

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

    90   moreover

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

    92   ultimately 

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

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

    95 next

    96   case (CAppR s E)

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

    98   moreover

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

   100   ultimately 

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

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

   103 qed

   104 

   105 section {* EXERCISE 9 *} 

   106  

   107 text {*

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

   109   establish the follwoing property:

   110 *}

   111 

   112 lemma machine_implies_cbvs_ctx:

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

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

   115 using a 

   116 proof (induct)

   117   case (m1 t1 t2 Es)

   118 

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

   120 next

   121   case (m2 v t2 Es)

   122   have "val v" by fact

   123 

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

   125 next

   126   case (m3 v x t Es)

   127   have "val v" by fact

   128  

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

   130 qed

   131 

   132 text {* 

   133   It is not difficult to extend the lemma above to

   134   arbitrary reductions sequences of the CK machine. *}

   135 

   136 lemma machines_implies_cbvs_ctx:

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

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

   139 using a 

   140 by (induct) (auto dest: machine_implies_cbvs_ctx)

   141 

   142 text {* 

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

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

   145   a corresponding cbv-reduction sequence. *}

   146 

   147 corollary machines_implies_cbvs:

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

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

   150 using a by (auto dest: machines_implies_cbvs_ctx)

   151 

   152 text {*

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

   154   relation. For this we need two auxiliary lemmas. *}

   155 

   156 lemma eval_val:

   157   assumes a: "val t"

   158   shows "t \<Down> t"

   159 using a by (induct) (auto)

   160 

   161 lemma e_App_elim:

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

   163   shows "\<exists>x t v'. t1 \<Down> Lam [x].t \<and> t2 \<Down> v' \<and> t[x::=v'] \<Down> v"

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

   165 

   166 text {******************************************************************

   167   

   168   10.) Exercise

   169   -------------

   170 

   171   Complete the first case in the proof below. 

   172 

   173 *}

   174 

   175 lemma cbv_eval:

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

   177   shows "t1 \<Down> t3"

   178 using a

   179 proof(induct arbitrary: t3)

   180   case (cbv1 v x t t3)

   181   have a1: "val v" by fact

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

   183 

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

   185 next

   186   case (cbv2 t t' t2 t3)

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

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

   189   then obtain x t'' v' 

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

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

   192       and a3: "t''[x ::= v'] \<Down> t3" using e_App_elim by blast

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

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

   195 qed (auto dest!: e_App_elim)

   196 

   197 

   198 text {* 

   199   Next we extend the lemma above to arbitray initial

   200   sequences of cbv-reductions. *}

   201 

   202 lemma cbvs_eval:

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

   204   shows "t1 \<Down> t3"

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

   206 

   207 text {* 

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

   209   by a cbv-reduction sequence, then t evaluates to this value. *}

   210 

   211 lemma cbvs_implies_eval:

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

   213   shows "t \<Down> v"

   214 using a

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

   216 

   217 text {* 

   218   All facts tied together give us the desired property about

   219   K machines. *}

   220 

   221 theorem machines_implies_eval:

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

   223   and     b: "val t2" 

   224   shows "t1 \<Down> t2"

   225 proof -

   226   have "t1 \<longrightarrow>cbv* t2" using a by (simp add: machines_implies_cbvs)

   227   then show "t1 \<Down> t2" using b by (simp add: cbvs_implies_eval)

   228 qed

   229 

   230 lemma valid_elim:

   231   assumes a: "valid ((x, T) # \<Gamma>)"

   232   shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>"

   233 using a by (cases) (auto)

   234 

   235 lemma valid_insert:

   236   assumes a: "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"

   237   shows "valid (\<Delta> @ \<Gamma>)" 

   238 using a

   239 by (induct \<Delta>)

   240    (auto simp add: fresh_append fresh_Cons dest!: valid_elim)

   241 

   242 lemma fresh_list: 

   243   shows "atom y \<sharp> xs = (\<forall>x \<in> set xs. atom y \<sharp> x)"

   244 by (induct xs) (simp_all add: fresh_Nil fresh_Cons)

   245 

   246 lemma context_unique:

   247   assumes a1: "valid \<Gamma>"

   248   and     a2: "(x, T) \<in> set \<Gamma>"

   249   and     a3: "(x, U) \<in> set \<Gamma>"

   250   shows "T = U" 

   251 using a1 a2 a3

   252 by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)

   253 

   254 lemma type_substitution_aux:

   255   assumes a: "(\<Delta> @ [(x, T')] @ \<Gamma>) \<turnstile> e : T"

   256   and     b: "\<Gamma> \<turnstile> e' : T'"

   257   shows "(\<Delta> @ \<Gamma>) \<turnstile> e[x ::= e'] : T" 

   258 using a b 

   259 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)

   260   case (t_Var y T x e' \<Delta>)

   261   have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact

   262   have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact 

   263   have a3: "\<Gamma> \<turnstile> e' : T'" by fact

   264   from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)

   265   { assume eq: "x = y"

   266     from a1 a2 have "T = T'" using eq by (auto intro: context_unique)

   267     with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" using eq a4 by (auto intro: weakening)

   268   }

   269   moreover

   270   { assume ineq: "x \<noteq> y"

   271     from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp

   272     then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" using ineq a4 by auto

   273   }

   274   ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast

   275 qed (force simp add: fresh_append fresh_Cons)+

   276 

   277 corollary type_substitution:

   278   assumes a: "(x,T') # \<Gamma> \<turnstile> e : T"

   279   and     b: "\<Gamma> \<turnstile> e' : T'"

   280   shows "\<Gamma> \<turnstile> e[x::=e'] : T"

   281 using a b type_substitution_aux[where \<Delta>="[]"]

   282 by (auto)

   283 

   284 lemma t_App_elim:

   285   assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"

   286   shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> t2 : T'"

   287 using a

   288 by (cases) (auto simp add: lam.eq_iff lam.distinct)

   289 

   290 lemma t_Lam_elim:

   291   assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" 

   292   and     fc: "atom x \<sharp> \<Gamma>" 

   293   shows "\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> (x, T1) # \<Gamma> \<turnstile> t : T2"

   294 using ty fc

   295 apply(cases)

   296 apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)

   297 apply(auto simp add: Abs1_eq_iff)

   298 apply(rule_tac p="(x \<leftrightarrow> xa)" in permute_boolE)

   299 apply(perm_simp)

   300 apply(simp add: flip_def swap_fresh_fresh ty_fresh)

   301 done

   302 

   303 theorem cbv_type_preservation:

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

   305   and     b: "\<Gamma> \<turnstile> t : T" 

   306   shows "\<Gamma> \<turnstile> t' : T"

   307 using a b

   308 by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)

   309    (auto dest!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)

   310 

   311 corollary cbvs_type_preservation:

   312   assumes a: "t \<longrightarrow>cbv* t'"

   313   and     b: "\<Gamma> \<turnstile> t : T" 

   314   shows "\<Gamma> \<turnstile> t' : T"

   315 using a b

   316 by (induct) (auto intro: cbv_type_preservation)

   317 

   318 text {* 

   319   The Type-Preservation Property for the Machine and Evaluation Relation. *}

   320 

   321 theorem machine_type_preservation:

   322   assumes a: "<t, []> \<mapsto>* <t', []>"

   323   and     b: "\<Gamma> \<turnstile> t : T" 

   324   shows "\<Gamma> \<turnstile> t' : T"

   325 proof -

   326   from a have "t \<longrightarrow>cbv* t'" by (simp add: machines_implies_cbvs)

   327   then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: cbvs_type_preservation)

   328 qed

   329 

   330 theorem eval_type_preservation:

   331   assumes a: "t \<Down> t'"

   332   and     b: "\<Gamma> \<turnstile> t : T" 

   333   shows "\<Gamma> \<turnstile> t' : T"

   334 proof -

   335   from a have "<t, []> \<mapsto>* <t', []>" by (simp add: eval_implies_machines)

   336   then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation)

   337 qed

   338 

   339 text {* The Progress Property *}

   340 

   341 lemma canonical_tArr:

   342   assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"

   343   and     b: "val t"

   344   shows "\<exists>x t'. t = Lam [x].t'"

   345 using b a by (induct) (auto) 

   346 

   347 theorem progress:

   348   assumes a: "[] \<turnstile> t : T"

   349   shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"

   350 using a

   351 by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)

   352    (auto intro: cbv.intros dest!: canonical_tArr)

   353 

   354