Quelle Compile.thy Sprache: Isabelle

(* 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" (\<open>_\<rightarrow>_\<close> [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"
          (\<open>Case _ of inl _ \<rightarrow> _ | inr _ \<rightarrow> _\<close> [100,100,100,100,100] 100)

nominal_datatype dataI = OneI | NatI

nominal_datatype tyI =
    DataI "dataI"
  | ArrowI "tyI" "tyI" (\<open>_\<rightarrow>_\<close> [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" (\<open>_\<leadsto>_\<close> [100,100] 100)
  | IRef "trmI"
  | ISeq "trmI" "trmI" (\<open>_;;_\<close> [100,100] 100)
  | Iif "trmI" "trmI" "trmI"

text \<open>valid contexts\<close>

inductive
  valid :: "(name\'a::pt_name) list \ bool"
where
  v1[intro]: "valid []"
| v2[intro]: "\valid \;a\\\\ valid ((a,\)#\)" (* maybe dom of \ *)

text \<open>typing judgements for trms\<close>

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(\<sigma>1))#\<Gamma>) \<turnstile> e1 : \<tau>; ((x2,Data(\<sigma>2))#\<Gamma>) \<turnstile> e2 : \<tau>\<rbrakk>
             \<Longrightarrow> \<Gamma> \<turnstile> (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) : \<tau>"

text \<open>typing judgements for Itrms\<close>

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 \<open>capture-avoiding substitution\<close>

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 \<rightarrow> e1 | inr z \<rightarrow> 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 \<open>big-step evaluation for trms\<close>

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)\
            \<Longrightarrow> (m,IApp e1 e2) I\<Down> (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 \<open>Translation functions\<close>

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)\<leadsto>v1);;(ISucc(ISucc limit)\<leadsto>v2));;(INat 0 \<leadsto> 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)\<leadsto>INat(0));;(ISucc(ISucc limit)\<leadsto>v));;(INat 0 \<leadsto> ISucc(ISucc(limit))))"
| "trans (InR e) =
        (let limit = IRef(INat 0) in
         let v = (trans e) in
         (((ISucc limit)\<leadsto>INat(1));;(ISucc(ISucc limit)\<leadsto>v));;(INat 0 \<leadsto> ISucc(ISucc(limit))))"
| "\x2\x1; x1\e; x1\e2; x2\e; x2\e1\ \
   trans (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> 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

quality93%

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.