theory Tutorial4

begin

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

text {*

  In order to help establishing the property that the CK Machine

  calculates a nomrmalform that corresponds to the evaluation 

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

*}

inductive

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

where

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

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

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

equivariance val

equivariance cbv

nominal_inductive cbv

  avoids cbv1: "x"

  unfolding fresh_star_def

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

text {*

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

  this relation with the additional freshness constraint

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

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

  pain show that the more restricted rule is equivalent to the

  usual rule. 

*}

lemma subst_rename: 

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

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

using a 

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

   (auto simp add: lam.fresh fresh_at_base)

lemma better_cbv1 [intro]: 

  assumes a: "val v" 

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

proof -

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

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

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

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

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

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

qed

text {*

  The transitive closure of the cbv-reduction relation: 

*}

inductive 

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

where

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

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

lemma cbvs3 [intro]:

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

  shows "e1 \<longrightarrow>cbv* e3"

using a by (induct) (auto) 

subsection {* EXERCISE 8 *}

text {*  

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

*}

lemma cbv_in_ctx:

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

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

using a

proof (induct E)

  case Hole

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

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

next

  case (CAppL E s)

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

  moreover

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

  ultimately 

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

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

next

  case (CAppR s E)

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

  moreover

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

  ultimately 

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

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

qed

section {* EXERCISE 9 *} 

text {*

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

  establish the follwoing property:

*}

lemma machine_implies_cbvs_ctx:

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

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

using a 

proof (induct)

  case (m1 t1 t2 Es)

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

next

  case (m2 v t2 Es)

  have "val v" by fact

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

next

  case (m3 v x t Es)

  have "val v" by fact

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

qed

text {* 

  It is not difficult to extend the lemma above to

  arbitrary reductions sequences of the CK machine. *}

lemma machines_implies_cbvs_ctx:

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

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

text {* 

  So whenever we let the CL machine start in an initial

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

corollary machines_implies_cbvs:

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

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

text {*

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

lemma eval_val:

  assumes a: "val t"

  shows "t \<Down> t"

using a by (induct) (auto)

lemma e_App_elim:

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

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

*}

lemma cbv_eval:

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

  shows "t1 \<Down> t3"

using a

proof(induct arbitrary: t3)

  case (cbv1 v x t t3)

  have a1: "val v" by fact

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

next

  case (cbv2 t t' t2 t3)

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

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

  then obtain x t'' v' 

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

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

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

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

text {* 

  Next we extend the lemma above to arbitray initial

  sequences of cbv-reductions. *}

lemma cbvs_eval:

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

  shows "t1 \<Down> t3"

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

text {* 

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

lemma cbvs_implies_eval:

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

  shows "t \<Down> v"

using a

by (induct) (auto intro: eval_val cbvs_eval)

text {* 

  All facts tied together give us the desired property about

theorem machines_implies_eval:

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

  and     b: "val t2" 

  shows "t1 \<Down> t2"

proof -

qed

lemma valid_elim:

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

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

using a by (cases) (auto)

lemma valid_insert:

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

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

using a

by (induct \<Delta>)

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

lemma fresh_list: 

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

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

lemma context_unique:

  assumes a1: "valid \<Gamma>"

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

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

  shows "T = U" 

using a1 a2 a3

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

lemma type_substitution_aux:

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

using a b 

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

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

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

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

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

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

  { assume eq: "x = y"

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

  }

  moreover

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

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

  }

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

qed (force simp add: fresh_append fresh_Cons)+

corollary type_substitution:

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

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

lemma t_App_elim:

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

using a

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

lemma t_Lam_elim:

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

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

using ty fc

apply(cases)

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

apply(auto simp add: Abs1_eq_iff)

apply(perm_simp)

done

theorem cbv_type_preservation:

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

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

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

using a b

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

corollary cbvs_type_preservation:

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

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

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

using a b

by (induct) (auto intro: cbv_type_preservation)

text {* 

theorem machine_type_preservation:

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

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

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

proof -

qed

theorem eval_type_preservation:

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

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

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

proof -

qed

text {* The Progress Property *}

lemma canonical_tArr:

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

  and     b: "val t"

using b a by (induct) (auto) 

theorem progress:

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

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

using a

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