Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Compile.thy Sprache: Isabelle

Original von: 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" ("_\_" [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 \<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']))"
  apply(finite_guess)+
  apply(rule TrueI)+
  apply(simp add: abs_fresh)+
  apply(fresh_guess)+
  done

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'])"
  apply(finite_guess)+
  apply(rule TrueI)+
  apply(simp add: abs_fresh)+
  apply(fresh_guess)+
  done

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)])"
  apply (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct)
  apply (simp_all add: subst_trmI.simps eqvts fresh_bij)
  done

lemma Isubst_supp:
  fixes t1::"trmI"
  and   t2::"trmI"
  and   x::"name"
  shows "((supp (t1[x::=t2]))::name set) \ (supp t2)\((supp t1)-{x})"
  apply (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct)
  apply (auto simp add: subst_trmI.simps trmI.supp supp_atm abs_supp supp_nat)
  apply blast+
  done

lemma Isubst_fresh:
  fixes x::"name"
  and   y::"name"
  and   t1::"trmI"
  and   t2::"trmI"
  assumes a: "x\[y].t1" "x\t2"
  shows "x\(t1[y::=t2])"
using a
apply(auto simp add: fresh_def Isubst_supp)
apply(drule rev_subsetD)
apply(rule Isubst_supp)
apply(simp add: abs_supp)
done

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)\<mapsto>v1);;(ISucc(ISucc limit)\<mapsto>v2));;(INat 0 \<mapsto> 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)\<mapsto>INat(0));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
| "trans (InR e) =
        (let limit = IRef(INat 0) in
         let v = (trans e) in
         (((ISucc limit)\<mapsto>INat(1));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> 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))]))"
  apply(finite_guess add: Let_def)+
  apply(rule TrueI)+
  apply(simp add: abs_fresh Isubst_fresh)+
  apply(fresh_guess add: Let_def)+
  done

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

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.