Quelle  Compile.thy

(* The definitions for a challenge suggested by Adam Chlipala *)

theory Compile
imports "HOL-Nominal.Nominal"
begin

atom_decl name 

nominal_datatype data = 
    DNat
  | DProd "data" "data"
  | DSum "data" "data"

nominal_datatype ty = 
    Data "data"
  | Arrow "ty" "ty" (‹_→_› [100,100] 100)

nominal_datatype trm = 
  Var "name"
  | Lam "«name¬trm" (‹Lam [_]._› [100,100] 100)
  | App "trm" "trm"
  | Const "nat"
  | Pr "trm" "trm"
  | Fst "trm"
  | Snd "trm"
  | InL "trm"
  | InR "trm"
  | Case "trm" "«name¬trm" "«name¬trm" 
          (‹Case _ of inl _ → _ | inr _ → _› [100,100,100,100,100] 100)

nominal_datatype dataI = OneI | NatI

nominal_datatype tyI = 
    DataI "dataI"
  | ArrowI "tyI" "tyI" (‹_→_› [100,100] 100)

nominal_datatype trmI = 
    IVar "name"
  | ILam "«name¬trmI" (‹ILam [_]._› [100,100] 100)
  | IApp "trmI" "trmI"
  | IUnit
  | INat "nat"
  | ISucc "trmI"
  | IAss "trmI" "trmI" (‹_↝_› [100,100] 100)
  | IRef "trmI" 
  | ISeq "trmI" "trmI" (‹_;;_› [100,100] 100)
  | Iif "trmI" "trmI" "trmI"

text ‹valid contexts›

inductive 
  valid :: "(name×'a::pt_name) list ==> bool"
where
  v1[intro]: "valid []"
| v2[intro]: "[valid Γ;a♯Γ]==> valid ((a,σ)#Γ)" (* maybe dom of \<Gamma> *)

text ‹typing judgements for trms›

inductive 
  typing :: "(name×ty) list==>trm==>ty==>bool" (‹ _ ⊨ _ : _ › [80,80,80] 80)
where
  t0[intro]: "[valid Γ; (x,τ)∈set Γ]==> Γ ⊨ Var x : τ"
| t1[intro]: "[Γ ⊨ e1 : τ1→τ2; Γ ⊨ e2 : τ1]==> Γ ⊨ App e1 e2 : τ2"
| t2[intro]: "[x♯Γ;((x,τ1)#Γ) ⊨ t : τ2] ==> Γ ⊨ Lam [x].t : τ1→τ2"
| t3[intro]: "valid Γ ==> Γ ⊨ Const n : Data(DNat)"
| t4[intro]: "[Γ ⊨ e1 : Data(σ1); Γ ⊨ e2 : Data(σ2)] ==> Γ ⊨ Pr e1 e2 : Data (DProd σ1 σ2)"
| t5[intro]: "[Γ ⊨ e : Data(DProd σ1 σ2)] ==> Γ ⊨ Fst e : Data(σ1)"
| t6[intro]: "[Γ ⊨ e : Data(DProd σ1 σ2)] ==> Γ ⊨ Snd e : Data(σ2)"
| t7[intro]: "[Γ ⊨ e : Data(σ1)] ==> Γ ⊨ InL e : Data(DSum σ1 σ2)"
| t8[intro]: "[Γ ⊨ e : Data(σ2)] ==> Γ ⊨ InR e : Data(DSum σ1 σ2)"
| t9[intro]: "[x1♯Γ; x2♯Γ; Γ ⊨ e: Data(DSum σ1 σ2);
             ((x1,Data(σ1))#Γ) ⊨ e1 : τ; ((x2,Data(σ2))#Γ) ⊨ e2 : τ]
             ==> Γ ⊨ (Case e of inl x1 → e1 | inr x2 → e2) : τ"

text ‹typing judgements for Itrms›

inductive 
  Ityping :: "(name×tyI) list==>trmI==>tyI==>bool" (‹ _ I⊨ _ : _ › [80,80,80] 80)
where
  t0[intro]: "[valid Γ; (x,τ)∈set Γ]==> Γ I⊨ IVar x : τ"
| t1[intro]: "[Γ I⊨ e1 : τ1→τ2; Γ I⊨ e2 : τ1]==> Γ I⊨ IApp e1 e2 : τ2"
| t2[intro]: "[x♯Γ;((x,τ1)#Γ) I⊨ t : τ2] ==> Γ I⊨ ILam [x].t : τ1→τ2"
| t3[intro]: "valid Γ ==> Γ I⊨ IUnit : DataI(OneI)"
| t4[intro]: "valid Γ ==> Γ I⊨ INat(n) : DataI(NatI)"
| t5[intro]: "Γ I⊨ e : DataI(NatI) ==> Γ I⊨ ISucc(e) : DataI(NatI)"
| t6[intro]: "[Γ I⊨ e : DataI(NatI)] ==> Γ I⊨ IRef e : DataI (NatI)"
| t7[intro]: "[Γ I⊨ e1 : DataI(NatI); Γ I⊨ e2 : DataI(NatI)] ==> Γ I⊨ e1↝e2 : DataI(OneI)"
| t8[intro]: "[Γ I⊨ e1 : DataI(NatI); Γ I⊨ e2 : τ] ==> Γ I⊨ e1;;e2 : τ"
| t9[intro]: "[Γ I⊨ e: DataI(NatI); Γ I⊨ e1 : τ; Γ I⊨ e2 : τ] ==> Γ I⊨ Iif e e1 e2 : τ"

text ‹capture-avoiding substitution›

class subst =
  fixes subst :: "'a ==> name ==> 'a ==> 'a"  (‹_[_::=_]› [100,100,100] 100)

instantiation trm :: subst
begin

nominal_primrec subst_trm
where
  "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
| "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
| "[x♯y; x♯t'] ==> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
| "(Const n)[y::=t'] = Const n"
| "(Pr e1 e2)[y::=t'] = Pr (e1[y::=t']) (e2[y::=t'])"
| "(Fst e)[y::=t'] = Fst (e[y::=t'])"
| "(Snd e)[y::=t'] = Snd (e[y::=t'])"
| "(InL e)[y::=t'] = InL (e[y::=t'])"
| "(InR e)[y::=t'] = InR (e[y::=t'])"
| "[z≠x; x♯y; x♯e; x♯e2; z♯y; z♯e; z♯e1; x♯t'; z♯t'] ==>
     (Case e of inl x → e1 | inr z → e2)[y::=t'] =
       (Case (e[y::=t']) of inl x → (e1[y::=t']) | inr z → (e2[y::=t']))"
  by(finite_guess | simp add: abs_fresh | fresh_guess)+

instance ..

end

instantiation trmI :: subst
begin

nominal_primrec subst_trmI
where
  "(IVar x)[y::=t'] = (if x=y then t' else (IVar x))"
| "(IApp t1 t2)[y::=t'] = IApp (t1[y::=t']) (t2[y::=t'])"
| "[x♯y; x♯t'] ==> (ILam [x].t)[y::=t'] = ILam [x].(t[y::=t'])"
| "(INat n)[y::=t'] = INat n"
| "(IUnit)[y::=t'] = IUnit"
| "(ISucc e)[y::=t'] = ISucc (e[y::=t'])"
| "(IAss e1 e2)[y::=t'] = IAss (e1[y::=t']) (e2[y::=t'])"
| "(IRef e)[y::=t'] = IRef (e[y::=t'])"
| "(ISeq e1 e2)[y::=t'] = ISeq (e1[y::=t']) (e2[y::=t'])"
| "(Iif e e1 e2)[y::=t'] = Iif (e[y::=t']) (e1[y::=t']) (e2[y::=t'])"
  by(finite_guess | simp add: abs_fresh | fresh_guess)+

instance ..

end

lemma Isubst_eqvt[eqvt]:
  fixes pi::"name prm"
  and   t1::"trmI"
  and   t2::"trmI"
  and   x::"name"
  shows "pi∙(t1[x::=t2]) = ((pi∙t1)[(pi∙x)::=(pi∙t2)])"
  by (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct)
     (simp_all add: subst_trmI.simps eqvts fresh_bij)

lemma Isubst_supp:
  fixes t1::"trmI"
  and   t2::"trmI"
  and   x::"name"
  shows "((supp (t1[x::=t2]))::name set) ⊆ (supp t2)∪((supp t1)-{x})"
proof (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct)
  case (IVar name)
  then show ?case
    by (simp add: supp_atm trmI.supp(1))
qed (fastforce simp add: subst_trmI.simps trmI.supp supp_atm abs_supp supp_nat)+

lemma Isubst_fresh:
  fixes x::"name"
  and   y::"name"
  and   t1::"trmI"
  and   t2::"trmI"
  assumes "x♯[y].t1" "x♯t2"
  shows "x♯(t1[y::=t2])"
  using assms Isubst_supp abs_supp(2)  unfolding fresh_def Isubst_supp by fastforce

text ‹big-step evaluation for trms›

inductive 
  big :: "trm==>trm==>bool" (‹_ ⇓ _› [80,80] 80)
where
  b0[intro]: "Lam [x].e ⇓ Lam [x].e"
| b1[intro]: "[e1⇓Lam [x].e; e2⇓e2'; e[x::=e2']⇓e'] ==> App e1 e2 ⇓ e'"
| b2[intro]: "Const n ⇓ Const n"
| b3[intro]: "[e1⇓e1'; e2⇓e2'] ==> Pr e1 e2 ⇓ Pr e1' e2'"
| b4[intro]: "e⇓Pr e1 e2 ==> Fst e⇓e1"
| b5[intro]: "e⇓Pr e1 e2 ==> Snd e⇓e2"
| b6[intro]: "e⇓e' ==> InL e ⇓ InL e'"
| b7[intro]: "e⇓e' ==> InR e ⇓ InR e'"
| b8[intro]: "[e⇓InL e'; e1[x::=e']⇓e''] ==> Case e of inl x1 → e1 | inr x2 → e2 ⇓ e''"
| b9[intro]: "[e⇓InR e'; e2[x::=e']⇓e''] ==> Case e of inl x1 → e1 | inr x2 → e2 ⇓ e''"

inductive 
  Ibig :: "((nat==>nat)×trmI)==>((nat==>nat)×trmI)==>bool" (‹_ I⇓ _› [80,80] 80)
where
  m0[intro]: "(m,ILam [x].e) I⇓ (m,ILam [x].e)"
| m1[intro]: "[(m,e1)I⇓(m',ILam [x].e); (m',e2)I⇓(m'',e3); (m'',e[x::=e3])I⇓(m''',e4)]
            ==> (m,IApp e1 e2) I⇓ (m''',e4)"
| m2[intro]: "(m,IUnit) I⇓ (m,IUnit)"
| m3[intro]: "(m,INat(n))I⇓(m,INat(n))"
| m4[intro]: "(m,e)I⇓(m',INat(n)) ==> (m,ISucc(e))I⇓(m',INat(n+1))"
| m5[intro]: "(m,e)I⇓(m',INat(n)) ==> (m,IRef(e))I⇓(m',INat(m' n))"
| m6[intro]: "[(m,e1)I⇓(m',INat(n1)); (m',e2)I⇓(m'',INat(n2))] ==> (m,e1↝e2)I⇓(m''(n1:=n2),IUnit)"
| m7[intro]: "[(m,e1)I⇓(m',IUnit); (m',e2)I⇓(m'',e)] ==> (m,e1;;e2)I⇓(m'',e)"
| m8[intro]: "[(m,e)I⇓(m',INat(n)); n≠0; (m',e1)I⇓(m'',e)] ==> (m,Iif e e1 e2)I⇓(m'',e)"
| m9[intro]: "[(m,e)I⇓(m',INat(0)); (m',e2)I⇓(m'',e)] ==> (m,Iif e e1 e2)I⇓(m'',e)"

text ‹Translation functions›

nominal_primrec
  trans :: "trm ==> trmI"
where
  "trans (Var x) = (IVar x)"
| "trans (App e1 e2) = IApp (trans e1) (trans e2)"
| "trans (Lam [x].e) = ILam [x].(trans e)"
| "trans (Const n) = INat n"
| "trans (Pr e1 e2) =
       (let limit = IRef(INat 0) in
        let v1 = (trans e1) in
        let v2 = (trans e2) in
        (((ISucc limit)↝v1);;(ISucc(ISucc limit)↝v2));;(INat 0 ↝ ISucc(ISucc(limit))))"
| "trans (Fst e) = IRef (ISucc (trans e))"
| "trans (Snd e) = IRef (ISucc (ISucc (trans e)))"
| "trans (InL e) =
        (let limit = IRef(INat 0) in
         let v = (trans e) in
         (((ISucc limit)↝INat(0));;(ISucc(ISucc limit)↝v));;(INat 0 ↝ ISucc(ISucc(limit))))"
| "trans (InR e) =
        (let limit = IRef(INat 0) in
         let v = (trans e) in
         (((ISucc limit)↝INat(1));;(ISucc(ISucc limit)↝v));;(INat 0 ↝ ISucc(ISucc(limit))))"
| "[x2≠x1; x1♯e; x1♯e2; x2♯e; x2♯e1] ==>
   trans (Case e of inl x1 → e1 | inr x2 → e2) =
       (let v = (trans e) in
        let v1 = (trans e1) in
        let v2 = (trans e2) in
        Iif (IRef (ISucc v)) (v2[x2::=IRef (ISucc (ISucc v))]) (v1[x1::=IRef (ISucc (ISucc v))]))"
  unfolding Let_def
  by(finite_guess | simp add: abs_fresh Isubst_fresh | fresh_guess)+

nominal_primrec
  trans_type :: "ty ==> tyI"
where
  "trans_type (Data σ) = DataI(NatI)"
| "trans_type (τ1→τ2) = (trans_type τ1)→(trans_type τ2)"
  by (rule TrueI)+

end