|
(* 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.15 Sekunden
(vorverarbeitet)
¤
|
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.
|
