header {*

  Hand-in on 17 June at noon. Please rename the file 
  and send your solution to me as

        Hw16_\<guillemotleft>your name\<guillemotright>

*}

theory Hw16
imports Nominal
begin

atom_decl name

text {* 

  Task 1 (moderate)

  Add to the language a equality test on numbers. Change the definitions and 
  proofs so that they go through. The big-step semantics of this equality test 
  is given by:

   t1 \<Down> (NUM n)   t2 \<Down> (NUM n)
  ------------------------------
      EQI t1 t2 \<Down> TRUE 

   t1 \<Down> (NUM n1)  t2 \<Down> (NUM n2)   n1 \<noteq> n2
   ---------------------------------------
        EQI t1 t2 \<Down> FALSE 

*}


nominal_datatype lam =
  VAR "name"
| APP "lam" "lam" 
| LAM "\<guillemotleft>name\<guillemotright>lam" ("LAM [_]._")
| NUM "nat"
| DIFF "lam" "lam" ("_ -- _")
| PLUS "lam" "lam" ("_ ++ _")
| TRUE
| FALSE
| IF "lam" "lam" "lam"
| FIX "\<guillemotleft>name\<guillemotright>lam" ("FIX [_]._")
| ZET "lam" 

consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)

nominal_primrec
  "(VAR x)[y::=s] = (if x=y then s else (VAR x))"
  "(APP t\<^isub>1 t\<^isub>2)[y::=s] = APP (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
  "x\<sharp>(y,s) \<Longrightarrow> (LAM [x].t)[y::=s] = LAM [x].(t[y::=s])"
  "(NUM n)[y::=s] = NUM n"
  "(t\<^isub>1 -- t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) -- (t\<^isub>2[y::=s])"
  "(t\<^isub>1 ++ t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) ++ (t\<^isub>2[y::=s])"
  "x\<sharp>(y,s) \<Longrightarrow> (FIX [x].t)[y::=s] = FIX [x].(t[y::=s])"
  "TRUE[y::=s] = TRUE"
  "FALSE[y::=s] = FALSE"
  "(IF t1 t2 t3)[y::=s] = IF (t1[y::=s]) (t2[y::=s]) (t3[y::=s])"
  "(ZET t)[y::=s] = ZET (t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)+
apply(fresh_guess)+
done

datatype ctx = 
    Hole ("\<box>")  
  | CAPPL "ctx" "lam"
  | CAPPR "lam" "ctx"
  | CDIFFL "ctx" "lam"
  | CDIFFR "lam" "ctx"
  | CPLUSL "ctx" "lam"
  | CPLUSR "lam" "ctx"
  | CIF "ctx" "lam" "lam"
  | CZE "ctx"

fun
  filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>")
where
  "\<box>\<lbrakk>t\<rbrakk> = t"
| "(CAPPL E t')\<lbrakk>t\<rbrakk> = APP (E\<lbrakk>t\<rbrakk>) t'"
| "(CAPPR t' E)\<lbrakk>t\<rbrakk> = APP t' (E\<lbrakk>t\<rbrakk>)"
| "(CDIFFL E t')\<lbrakk>t\<rbrakk> = (E\<lbrakk>t\<rbrakk>) -- t'"
| "(CDIFFR t' E)\<lbrakk>t\<rbrakk> = t' -- (E\<lbrakk>t\<rbrakk>)"
| "(CPLUSL E t')\<lbrakk>t\<rbrakk> = (E\<lbrakk>t\<rbrakk>) ++ t'"
| "(CPLUSR t' E)\<lbrakk>t\<rbrakk> = t' ++ (E\<lbrakk>t\<rbrakk>)"
| "(CIF E t1 t2)\<lbrakk>t\<rbrakk> = IF (E\<lbrakk>t\<rbrakk>) t1 t2"
| "(CZE E)\<lbrakk>t\<rbrakk> = ZET (E\<lbrakk>t\<rbrakk>)"

inductive
  val :: "lam\<Rightarrow>bool" 
where
  v_LAM[intro]:   "val (LAM [x].e)"
| v_NUM[intro]:   "val (NUM n)"  
| v_FALSE[intro]: "val FALSE"
| v_TRUE[intro]:  "val TRUE"

inductive
  machine :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto> <_,_>")
where
  m1[intro]: "<APP e1 e2, Es> \<mapsto> <e1,(CAPPL \<box> e2)#Es>"
| m2[intro]: "val v \<Longrightarrow> <v,(CAPPL \<box> e2)#Es> \<mapsto> <e2,(CAPPR v \<box>)#Es>"
| m3[intro]: "val v \<Longrightarrow> <v,(CAPPR (LAM [y].e) \<box>)#Es> \<mapsto> <e[y::=v],Es>"
| m4[intro]: "<e1 -- e2, Es> \<mapsto> <e1,(CDIFFL \<box> e2)#Es>"
| m5[intro]: "<NUM n1,(CDIFFL \<box> e2)#Es> \<mapsto> <e2,(CDIFFR (NUM n1) \<box>)#Es>"
| m6[intro]: "<NUM n2,(CDIFFR (NUM n1) \<box>)#Es> \<mapsto> <NUM (n1 - n2),Es>"
| m4'[intro]:"<e1 ++ e2, Es> \<mapsto> <e1,(CPLUSL \<box> e2)#Es>"
| m5'[intro]:"<NUM n1,(CPLUSL \<box> e2)#Es> \<mapsto> <e2,(CPLUSR (NUM n1) \<box>)#Es>"
| m6'[intro]:"<NUM n2,(CPLUSR (NUM n1) \<box>)#Es> \<mapsto> <NUM (n1+n2),Es>"
| m7[intro]: "<IF e1 e2 e3,Es> \<mapsto> <e1,(CIF \<box> e2 e3)#Es>"
| m8[intro]: "<TRUE,(CIF \<box> e1 e2)#Es> \<mapsto> <e1,Es>"
| m9[intro]: "<FALSE,(CIF \<box> e1 e2)#Es> \<mapsto> <e2,Es>"
| mA[intro]: "<FIX [x].t,Es> \<mapsto> <t[x::=FIX [x].t],Es>"
| mB[intro]: "<ZET e,Es> \<mapsto> <e,(CZE \<box>)#Es>"
| mC[intro]: "<NUM 0,(CZE \<box>)#Es> \<mapsto> <TRUE,Es>"
| mD[intro]: "0 < n \<Longrightarrow> <NUM n,(CZE \<box>)#Es> \<mapsto> <FALSE,Es>"

inductive 
  "machine_star" :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto>* <_,_>")
where
  ms1[intro]: "<e,Es> \<mapsto>* <e,Es>"
| ms2[intro]: "\<lbrakk><e1,Es1> \<mapsto> <e2,Es2>; <e2,Es2> \<mapsto>* <e3,Es3>\<rbrakk> \<Longrightarrow> <e1,Es1> \<mapsto>* <e3,Es3>"

lemma ms3[intro,trans]:
  assumes a: "<e1,Es1> \<mapsto>* <e2,Es2>" "<e2,Es2> \<mapsto>* <e3,Es3>"
  shows "<e1,Es1> \<mapsto>* <e3,Es3>"
using a by (induct) (auto) 

lemma ms4[intro]:
  assumes a: "<e1,Es1> \<mapsto> <e2,Es2>" 
  shows "<e1,Es1> \<mapsto>* <e2,Es2>"
using a by (rule ms2) (rule ms1)

inductive
  eval :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<Down> _") 
where
  eval_NUM[intro]:  "NUM n \<Down> NUM n" 
| eval_DIFF[intro]: "\<lbrakk>t1 \<Down> (NUM n1); t2 \<Down> (NUM n2)\<rbrakk> \<Longrightarrow> t1 -- t2 \<Down> NUM (n1 - n2)"
| eval_PLUS[intro]: "\<lbrakk>t1 \<Down> (NUM n1); t2 \<Down> (NUM n2)\<rbrakk> \<Longrightarrow> t1 ++ t2 \<Down> NUM (n1 + n2)"
| eval_LAM[intro]:  "LAM [x].t \<Down> LAM [x].t"
| eval_APP[intro]:  "\<lbrakk>t1\<Down> LAM [x].t; t2\<Down> t2'; t[x::=t2']\<Down> t'\<rbrakk> \<Longrightarrow> APP t1 t2 \<Down> t'"
| eval_FIX[intro]:  "t[x::= FIX [x].t] \<Down> t' \<Longrightarrow> FIX [x].t \<Down> t'"
| eval_IF1[intro]:  "\<lbrakk>t1 \<Down> TRUE; t2 \<Down> t'\<rbrakk> \<Longrightarrow> IF t1 t2 t3 \<Down> t'"
| eval_IF2[intro]:  "\<lbrakk>t1 \<Down> FALSE; t3 \<Down> t'\<rbrakk> \<Longrightarrow> IF t1 t2 t3 \<Down> t'"
| eval_TRUE[intro]: "TRUE \<Down> TRUE"
| eval_FALSE[intro]:"FALSE \<Down> FALSE"
| eval_ZE1[intro]:  "t \<Down> NUM 0 \<Longrightarrow> ZET t \<Down> TRUE"
| eval_ZE2[intro]:  "\<lbrakk>t \<Down> NUM n; 0 < n\<rbrakk> \<Longrightarrow> ZET t \<Down> FALSE"

lemma eval_APP_elim:
  assumes a: "APP t1 t2 \<Down> t'"
  shows "\<exists>x t t2'. t1\<Down> LAM [x].t \<and> t2\<Down> t2' \<and> t[x::=t2']\<Down> t'"
using a by (cases) (auto simp add: lam.inject)

lemma eval_IF_elim:
  assumes a: "IF t1 t2 t3 \<Down> t'"
  shows "(t1 \<Down> TRUE \<and> t2 \<Down> t') \<or> (t1 \<Down> FALSE \<and> t3 \<Down> t')"
using a by (cases) (auto simp add: lam.inject)

lemma eval_ZET_elim:
  assumes a: "ZET t \<Down> t'"
  shows "(t \<Down> NUM 0 \<and> t' = TRUE) \<or> (\<exists>n. t \<Down> NUM n \<and> 0 < n \<and> t' = FALSE)"
using a by (cases) (auto simp add: lam.inject)

lemma eval_PLUS_elim:
  assumes a: "t1 ++ t2 \<Down> t'"
  shows "\<exists>n1 n2. t1\<Down> (NUM n1) \<and> t2\<Down> (NUM n2) \<and> t' = NUM (n1 + n2)"
using a by (cases) (auto simp add: lam.inject)

lemma eval_DIFF_elim:
  assumes a: "t1 -- t2 \<Down> t'"
  shows "\<exists>n1 n2. t1\<Down> (NUM n1) \<and> t2\<Down> (NUM n2) \<and> t' = NUM (n1 - n2)"
using a by (cases) (auto simp add: lam.inject)

lemma eval_NUM_elim:
  assumes a: "(NUM n) \<Down> t"
  shows "t = NUM n"
using a by (cases) (auto simp add: lam.inject)

lemma eval_TRUE_elim:
  assumes a: "TRUE \<Down> t"
  shows "t = TRUE"
using a by (cases) (auto)

lemma eval_FALSE_elim:
  assumes a: "FALSE \<Down> t"
  shows "t = FALSE"
using a by (cases) (auto)

lemma eval_to:
  assumes a: "t \<Down> t'"
  shows "val t'"
using a by (induct) (auto)

lemma eval_val:
  assumes a: "val t"
  shows "t \<Down> t"
using a by (induct) (auto)

theorem eval_implies_machine:
  assumes a: "t \<Down> t'"
  shows "<t,Es> \<mapsto>* <t',Es>"
using a
apply(induct arbitrary: Es)
apply(metis eval_to m1 ms1 m2 ms2 m3 ms3 ms4 m4 m5 m6 m4' m5' m6' m7 m8 m9 mA mB mC mD v_LAM)+
done

fun 
 ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _")
where
  "\<box> \<circ> E' = E'"
| "(CAPPL E t') \<circ> E' = CAPPL (E \<circ> E') t'"
| "(CAPPR t' E) \<circ> E' = CAPPR t' (E \<circ> E')"
| "(CDIFFL E t') \<circ> E' = CDIFFL (E \<circ> E') t'"
| "(CDIFFR t' E) \<circ> E' = CDIFFR t' (E \<circ> E')"
| "(CPLUSL E t') \<circ> E' = CPLUSL (E \<circ> E') t'"
| "(CPLUSR t' E) \<circ> E' = CPLUSR t' (E \<circ> E')"
| "(CIF E t1 t2) \<circ> E' = CIF (E \<circ> E') t1 t2"
| "(CZE E) \<circ> E' = CZE (E \<circ> E')"

lemma ctx_compose:
  shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
by (induct E1 rule: ctx.induct) (auto)

fun
  ctx_composes :: "ctx list \<Rightarrow> ctx" ("_\<down>")
where
    "[]\<down> = \<box>"
  | "(E#Es)\<down> = (Es\<down>) \<circ> E"

inductive
  cbv :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>cbv _") 
where
  cbv1[intro]: "val v \<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'"
| cbv4[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t -- t2 \<longrightarrow>cbv t' -- t2"
| cbv5[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t2 -- t \<longrightarrow>cbv t2 -- t'"
| cbv6[intro]: "(NUM n1) -- (NUM n2) \<longrightarrow>cbv NUM (n1 - n2)"
| cbv4'[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t ++ t2 \<longrightarrow>cbv t' ++ t2"
| cbv5'[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t2 ++ t \<longrightarrow>cbv t2 ++ t'"
| cbv6'[intro]:"(NUM n1) ++ (NUM n2) \<longrightarrow>cbv NUM (n1 + n2)"
| cbv7[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> IF t t1 t2 \<longrightarrow>cbv IF t' t1 t2"
| cbv8[intro]: "IF TRUE t1 t2 \<longrightarrow>cbv t1"
| cbv9[intro]: "IF FALSE t1 t2 \<longrightarrow>cbv t2"
| cbvA[intro]: "FIX [x].t \<longrightarrow>cbv t[x::=FIX [x].t]"
| cbvB[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> ZET t \<longrightarrow>cbv ZET t'"
| cbvC[intro]: "ZET (NUM 0) \<longrightarrow>cbv TRUE"
| cbvD[intro]: "0 < n \<Longrightarrow> ZET (NUM n) \<longrightarrow>cbv FALSE"

inductive 
  "cbv_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>cbv* _")
where
  cbvs1[intro]: "e \<longrightarrow>cbv* e"
| cbvs2[intro]: "e \<longrightarrow>cbv e' \<Longrightarrow> e \<longrightarrow>cbv* e'"
| cbvs3[intro,trans]: "\<lbrakk>e1\<longrightarrow>cbv* e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"

lemma cbv_in_ctx:
  assumes a: "t \<longrightarrow>cbv t'"
  shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>"
using a by (induct E) (auto)

lemma machine_implies_cbv_star:
  assumes a: "<e,Es> \<mapsto> <e',Es'>"
  shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
using a
by (induct) (auto simp add: ctx_compose intro: cbv_in_ctx)

lemma cbv_eval:
  assumes a: "t1 \<longrightarrow>cbv t2" "t2 \<Down> t3"
  shows "t1 \<Down> t3"
using a
apply(induct arbitrary: t3)
apply(auto dest!: eval_APP_elim eval_ZET_elim eval_DIFF_elim 
                  eval_NUM_elim eval_IF_elim eval_PLUS_elim 
                  eval_FALSE_elim eval_TRUE_elim
                  intro: eval_val)
done

lemma cbv_star_eval:
  assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3"
  shows "t1 \<Down> t3"
using a by (induct) (auto simp add: cbv_eval)

lemma machine_implies_eval:
  assumes a: "<t1,Es> \<mapsto> <t2,Es'>" 
  and     b: "(Es'\<down>)\<lbrakk>t2\<rbrakk> \<Down> t3"
  shows "(Es\<down>)\<lbrakk>t1\<rbrakk> \<Down> t3"
proof -
  from a have "(Es\<down>)\<lbrakk>t1\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>t2\<rbrakk>" by (rule machine_implies_cbv_star)
  moreover 
  have "(Es'\<down>)\<lbrakk>t2\<rbrakk> \<Down> t3" by fact
  ultimately show "(Es\<down>)\<lbrakk>t1\<rbrakk> \<Down> t3" by (rule cbv_star_eval)
qed

lemma machine_star_implies_eval:
  assumes a: "<t1,Es> \<mapsto>* <t2,[]>" "val t2" 
  shows "(Es\<down>)\<lbrakk>t1\<rbrakk> \<Down> t2"
using a
by (induct t1 Es t2 Es'\<equiv>"[]::ctx list")
   (auto simp add: eval_val machine_implies_eval)

theorem
  assumes a: "<t1,[]> \<mapsto>* <t2,[]>" "val t2" 
  shows "t1 \<Down> t2"
using a by (auto dest: machine_star_implies_eval)

lemma forget: 
  assumes asm: "y\<sharp>t"
  shows "t[y::=s] = t"
  using asm 
by (nominal_induct t avoiding: y s rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_atm)

lemma forget2: 
  shows "(LAM [y].t)[y::=s] = (LAM [y].t)"
by (rule forget) (simp add: abs_fresh)


text {*

  Task 2: (moderate)

  Have a look at the program below calculating the sum of the first
  n numbers. 

  Write a program that calculates the nth Fibonacci number.

*}


consts 
  x::"name"
  f::"name"

abbreviation
  Sum :: "lam"
where
  "Sum \<equiv> FIX [f].LAM [x].(IF (ZET (VAR x)) (NUM 0) ((VAR x) ++ (APP (VAR f) ((VAR x) -- NUM 1))))"

text {*

  Task 3: (easy)

  For theorem eval_implies_machine (stated above) give on 
  *paper* the cases for applications, lambda-abstractions
  and if's. State clearly which property you are proving
  and what the induction hypotheses are.

*}


end