(* $Id: oregon3a.thy 419 2008-08-03 23:44:55Z urbanc $ *) theory CK_Machine imports "../Nominal" begin text {* This theory establishes soundness and completeness for a CK-machine with respect to a cbv-big-step semantics. The language includes functions, recursion, booleans and numbers. In the soundness proof the small-step cbv-reduction relation is used in order to get the induction through. The type-preservation property is proved for the machine and also for the small- and big-step semantics. Finally, the progress property is proved for the small-step semantics. The development is inspired by notes about context machines written by Roshan James (Indiana University) and also by the lecture notes written by Andy Pitts for his semantics course. See http://www.cs.indiana.edu/~rpjames/lm.pdf http://www.cl.cam.ac.uk/teaching/2001/Semantics/ *} atom_decl name nominal_datatype lam = VAR "name" | APP "lam" "lam" | LAM "\name\lam" ("LAM [_]._") | NUM "nat" | DIFF "lam" "lam" ("_ -- _") (* subtraction *) | PLUS "lam" "lam" ("_ ++ _") (* addition *) | TRUE | FALSE | IF "lam" "lam" "lam" | FIX "\name\lam" ("FIX [_]._") (* recursion *) | ZET "lam" (* zero test *) | EQI "lam" "lam" (* equality test on numbers *) section {* Capture-Avoiding Substitution *} consts subst :: "lam \ name \ lam \ 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\(y,s) \ (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\(y,s) \ (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])" "(EQI t1 t2)[y::=s] = EQI (t1[y::=s]) (t2[y::=s])" apply(finite_guess)+ apply(rule TrueI)+ apply(simp add: abs_fresh)+ apply(fresh_guess)+ done lemma subst_eqvt[eqvt]: fixes pi::"name prm" shows "pi\(t1[x::=t2]) = (pi\t1)[(pi\x)::=(pi\t2)]" by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct) (auto simp add: perm_bij fresh_atm fresh_bij) lemma fresh_fact: fixes z::"name" shows "\z\s; (z=y \ z\t)\ \ z\t[y::=s]" by (nominal_induct t avoiding: z y s rule: lam.strong_induct) (auto simp add: abs_fresh fresh_prod fresh_atm fresh_nat) lemma subst_rename: assumes a: "y\t" shows "t[x::=s] = ([(y,x)]\t)[y::=s]" using a by (nominal_induct t avoiding: x y s rule: lam.strong_induct) (auto simp add: calc_atm fresh_atm abs_fresh perm_nat_def) section {* Evaluation Contexts *} datatype ctx = Hole ("\") | CAPPL "ctx" "lam" | CAPPR "lam" "ctx" | CDIFFL "ctx" "lam" | CDIFFR "lam" "ctx" | CPLUSL "ctx" "lam" | CPLUSR "lam" "ctx" | CIF "ctx" "lam" "lam" | CZET "ctx" | CEQIL "ctx" "lam" | CEQIR "lam" "ctx" text {* The operation of filling a term into a context: *} fun filling :: "ctx \ lam \ lam" ("_\_\") where "\\t\ = t" | "(CAPPL E t')\t\ = APP (E\t\) t'" | "(CAPPR t' E)\t\ = APP t' (E\t\)" | "(CDIFFL E t')\t\ = (E\t\) -- t'" | "(CDIFFR t' E)\t\ = t' -- (E\t\)" | "(CPLUSL E t')\t\ = (E\t\) ++ t'" | "(CPLUSR t' E)\t\ = t' ++ (E\t\)" | "(CIF E t1 t2)\t\ = IF (E\t\) t1 t2" | "(CZET E)\t\ = ZET (E\t\)" | "(CEQIL E t')\t\ = EQI (E\t\) t'" | "(CEQIR t' E)\t\ = EQI t' (E\t\)" text {* The operation of composing two contexts: *} fun ctx_compose :: "ctx \ ctx \ ctx" ("_ \ _") where "\ \ E' = E'" | "(CAPPL E t') \ E' = CAPPL (E \ E') t'" | "(CAPPR t' E) \ E' = CAPPR t' (E \ E')" | "(CDIFFL E t') \ E' = CDIFFL (E \ E') t'" | "(CDIFFR t' E) \ E' = CDIFFR t' (E \ E')" | "(CPLUSL E t') \ E' = CPLUSL (E \ E') t'" | "(CPLUSR t' E) \ E' = CPLUSR t' (E \ E')" | "(CIF E t1 t2) \ E' = CIF (E \ E') t1 t2" | "(CZET E) \ E' = CZET (E \ E')" | "(CEQIL E t') \ E' = CEQIL (E \ E') t'" | "(CEQIR t' E) \ E' = CEQIR t' (E \ E')" lemma ctx_compose: shows "(E1 \ E2)\t\ = E1\E2\t\\" by (induct E1 rule: ctx.induct) (auto) text {* Composing a list (stack) of contexts. *} fun ctx_composes :: "ctx list \ ctx" ("_\") where "[]\ = \" | "(E#Es)\ = (Es\) \ E" section {* The CK-Machine *} inductive val :: "lam\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" equivariance val inductive machine :: "lam\ctx list\lam\ctx list\bool" ("<_,_> \ <_,_>") where m1[intro]: " \ e2)#Es>" | m2[intro]: "val v \ e2)#Es> \ )#Es>" | m3[intro]: "val v \ )#Es> \ " | m4[intro]: " \ e2)#Es>" | m5[intro]: " e2)#Es> \ )#Es>" | m6[intro]: ")#Es> \ " | m4'[intro]:" \ e2)#Es>" | m5'[intro]:" e2)#Es> \ )#Es>" | m6'[intro]:")#Es> \ " | m7[intro]: " \ e2 e3)#Es>" | m8[intro]: " e1 e2)#Es> \ " | m9[intro]: " e1 e2)#Es> \ " | mA[intro]: " \ " | mB[intro]: " \ )#Es>" | mC[intro]: ")#Es> \ " | mD[intro]: "0 < n \ )#Es> \ " | mE[intro]: " \ e2)#Es>" | mF[intro]: " e2)#Es> \ )#Es>" | mG[intro]: ")#Es> \ " | mH[intro]: "n1\n2 \ )#Es> \ " inductive "machine_star" :: "lam\ctx list\lam\ctx list\bool" ("<_,_> \* <_,_>") where ms1[intro]: " \* " | ms2[intro]: "\ \ ; \* \ \ \* " lemma ms3[intro,trans]: assumes a: " \* " " \* " shows " \* " using a by (induct) (auto) lemma ms4[intro]: assumes a: " \ " shows " \* " using a by (rule ms2) (rule ms1) section {* The Evaluation Relation (Big-Step Semantics) *} inductive eval :: "lam\lam\bool" ("_ \ _") where eval_NUM[intro]: "NUM n \ NUM n" | eval_DIFF[intro]: "\t1 \ (NUM n1); t2 \ (NUM n2)\ \ t1 -- t2 \ NUM (n1 - n2)" | eval_PLUS[intro]: "\t1 \ (NUM n1); t2 \ (NUM n2)\ \ t1 ++ t2 \ NUM (n1 + n2)" | eval_LAM[intro]: "LAM [x].t \ LAM [x].t" | eval_APP[intro]: "\t1\ LAM [x].t; t2\ t2'; t[x::=t2']\ t'\ \ APP t1 t2 \ t'" | eval_FIX[intro]: "t[x::= FIX [x].t] \ t' \ FIX [x].t \ t'" | eval_IF1[intro]: "\t1 \ TRUE; t2 \ t'\ \ IF t1 t2 t3 \ t'" | eval_IF2[intro]: "\t1 \ FALSE; t3 \ t'\ \ IF t1 t2 t3 \ t'" | eval_TRUE[intro]: "TRUE \ TRUE" | eval_FALSE[intro]:"FALSE \ FALSE" | eval_ZET1[intro]: "t \ NUM 0 \ ZET t \ TRUE" | eval_ZET2[intro]: "\t \ NUM n; 0 < n\ \ ZET t \ FALSE" | eval_EQ1[intro]: "\t1 \ NUM n; t2 \ NUM n\ \ EQI t1 t2 \ TRUE" | eval_EQ2[intro]: "\t1 \ NUM n1; t2 \ NUM n2; n1\n2\ \ EQI t1 t2 \ FALSE" declare lam.inject[simp] inductive_cases eval_elim: "APP t1 t2 \ t'" "IF t1 t2 t3 \ t'" "ZET t \ t'" "EQI t1 t2 \ t'" "t1 ++ t2 \ t'" "t1 -- t2 \ t'" "(NUM n) \ t" "TRUE \ t" "FALSE \ t" declare lam.inject[simp del] lemma eval_to: assumes a: "t \ t'" shows "val t'" using a by (induct) (auto) lemma eval_val: assumes a: "val t" shows "t \ t" using a by (induct) (auto) text {* The Completeness Property: *} theorem eval_implies_machine_star_ctx: assumes a: "t \ t'" shows " \* " using a by (induct arbitrary: Es) (metis eval_to machine.intros ms1 ms2 ms3 ms4 v_LAM)+ corollary eval_implies_machine_star: assumes a: "t \ t'" shows " \* " using a by (auto dest: eval_implies_machine_star_ctx) section {* The CBV Reduction Relation (Small-Step Semantics) *} lemma less_eqvt[eqvt]: fixes pi::"name prm" and n1 n2::"nat" shows "(pi\(n1 < n2)) = ((pi\n1) < (pi\n2))" by (simp add: perm_nat_def perm_bool) inductive cbv :: "lam\lam\bool" ("_ \cbv _") where cbv1: "\val v; x\v\ \ APP (LAM [x].t) v \cbv t[x::=v]" | cbv2[intro]: "t \cbv t' \ APP t t2 \cbv APP t' t2" | cbv3[intro]: "t \cbv t' \ APP t2 t \cbv APP t2 t'" | cbv4[intro]: "t \cbv t' \ t -- t2 \cbv t' -- t2" | cbv5[intro]: "t \cbv t' \ t2 -- t \cbv t2 -- t'" | cbv6[intro]: "(NUM n1) -- (NUM n2) \cbv NUM (n1 - n2)" | cbv4'[intro]: "t \cbv t' \ t ++ t2 \cbv t' ++ t2" | cbv5'[intro]: "t \cbv t' \ t2 ++ t \cbv t2 ++ t'" | cbv6'[intro]:"(NUM n1) ++ (NUM n2) \cbv NUM (n1 + n2)" | cbv7[intro]: "t \cbv t' \ IF t t1 t2 \cbv IF t' t1 t2" | cbv8[intro]: "IF TRUE t1 t2 \cbv t1" | cbv9[intro]: "IF FALSE t1 t2 \cbv t2" | cbvA[intro]: "FIX [x].t \cbv t[x::=FIX [x].t]" | cbvB[intro]: "t \cbv t' \ ZET t \cbv ZET t'" | cbvC[intro]: "ZET (NUM 0) \cbv TRUE" | cbvD[intro]: "0 < n \ ZET (NUM n) \cbv FALSE" | cbvE[intro]: "t \cbv t' \ EQI t t2 \cbv EQI t' t2" | cbvF[intro]: "t \cbv t' \ EQI t2 t \cbv EQI t2 t'" | cbvG[intro]: "EQI (NUM n) (NUM n) \cbv TRUE" | cbvH[intro]: "n1\n2 \ EQI (NUM n1) (NUM n2) \cbv FALSE" equivariance cbv nominal_inductive cbv by (simp_all add: abs_fresh fresh_fact) lemma better_cbv1[intro]: assumes a: "val v" shows "APP (LAM [x].t) v \cbv t[x::=v]" proof - obtain y::"name" where fs: "y\(x,t,v)" by (rule exists_fresh, rule fin_supp, blast) have "APP (LAM [x].t) v = APP (LAM [y].([(y,x)]\t)) v" using fs by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) also have "\ \cbv ([(y,x)]\t)[y::=v]" using fs a by (auto simp add: cbv.eqvt cbv1) also have "\ = t[x::=v]" using fs by (simp add: subst_rename[symmetric]) finally show "APP (LAM [x].t) v \cbv t[x::=v]" by simp qed inductive "cbv_star" :: "lam\lam\bool" (" _ \cbv* _") where cbvs1[intro]: "e \cbv* e" | cbvs2[intro]: "\e1\cbv e2; e2 \cbv* e3\ \ e1 \cbv* e3" lemma cbvs3[intro,trans]: assumes a: "e1 \cbv* e2" "e2 \cbv* e3" shows "e1 \cbv* e3" using a by (induct) (auto) lemma cbv_in_ctx: assumes a: "t \cbv t'" shows "E\t\ \cbv E\t'\" using a by (induct E) (auto) lemma machine_implies_cbv_star_ctx: assumes a: " \ " shows "(Es\)\e\ \cbv* (Es'\)\e'\" using a by (induct) (auto simp add: ctx_compose intro: cbv_in_ctx) lemma machine_star_implies_cbv_star_ctx: assumes a: " \* " shows "(Es\)\e\ \cbv* (Es'\)\e'\" using a by (induct) (auto dest: machine_implies_cbv_star_ctx) lemma machine_star_implies_cbv_star: assumes a: " \* " shows "e \cbv* e'" using a by (auto dest: machine_star_implies_cbv_star_ctx) lemma cbv_eval: assumes a: "t1 \cbv t2" "t2 \ t3" shows "t1 \ t3" using a by (induct arbitrary: t3) (auto elim!: eval_elim intro: eval_val) lemma cbv_star_eval: assumes a: "t1 \cbv* t2" "t2 \ t3" shows "t1 \ t3" using a by (induct) (auto simp add: cbv_eval) lemma cbv_star_implies_eval: assumes a: "t \cbv* v" "val v" shows "t \ v" using a by (induct) (auto simp add: eval_val cbv_star_eval dest: cbvs2) text {* The Soundness Property *} theorem machine_star_implies_eval: assumes a: " \* " and b: "val t2" shows "t1 \ t2" proof - from a have "t1 \cbv* t2" by (simp add: machine_star_implies_cbv_star) then show "t1 \ t2" using b by (simp add: cbv_star_implies_eval) qed section {* Typing *} text {* Types *} nominal_datatype ty = tVAR "string" | tBOOL | tINT | tARR "ty" "ty" ("_ \ _") declare ty.inject[simp] lemma ty_fresh: fixes x::"name" and T::"ty" shows "x\T" by (induct T rule: ty.induct) (auto simp add: fresh_string) text {* Typing Contexts *} types tctx = "(name\ty) list" text {* Sub-Typing Contexts *} abbreviation "sub_tctx" :: "tctx \ tctx \ bool" ("_ \ _") where "\\<^isub>1 \ \\<^isub>2 \ \x. x \ set \\<^isub>1 \ x \ set \\<^isub>2" text {* Valid Typing Contexts *} inductive valid :: "tctx \ bool" where v1[intro]: "valid []" | v2[intro]: "\valid \; x\\\\ valid ((x,T)#\)" equivariance valid lemma valid_elim[dest]: assumes a: "valid ((x,T)#\)" shows "x\\ \ valid \" using a by (cases) (auto) lemma valid_insert: assumes a: "valid (\@[(x,T)]@\)" shows "valid (\ @ \)" using a by (induct \) (auto simp add: fresh_list_append fresh_list_cons dest!: valid_elim) lemma fresh_set: shows "y\xs = (\x\set xs. y\x)" by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons) lemma context_unique: assumes a1: "valid \" and a2: "(x,T) \ set \" and a3: "(x,U) \ set \" shows "T = U" using a1 a2 a3 by (induct) (auto simp add: fresh_set fresh_prod fresh_atm) section {* The Typing Relation *} inductive typing :: "tctx \ lam \ ty \ bool" ("_ \ _ : _") where t_VAR[intro]: "\valid \; (x,T)\set \\ \ \ \ VAR x : T" | t_APP[intro]: "\\ \ t\<^isub>1 : T\<^isub>1\T\<^isub>2; \ \ t\<^isub>2 : T\<^isub>1\ \ \ \ APP t\<^isub>1 t\<^isub>2 : T\<^isub>2" | t_LAM[intro]: "\x\\; (x,T\<^isub>1)#\ \ t : T\<^isub>2\ \ \ \ LAM [x].t : T\<^isub>1 \ T\<^isub>2" | t_NUM[intro]: "\ \ (NUM n) : tINT" | t_DIFF[intro]: "\\ \ t\<^isub>1 : tINT; \ \ t\<^isub>2 : tINT\ \ \ \ t\<^isub>1 -- t\<^isub>2 : tINT" | t_PLUS[intro]: "\\ \ t\<^isub>1 : tINT; \ \ t\<^isub>2 : tINT\ \ \ \ t\<^isub>1 ++ t\<^isub>2 : tINT" | t_TRUE[intro]: "\ \ TRUE : tBOOL" | t_FALSE[intro]: "\ \ FALSE : tBOOL" | t_IF[intro]: "\\ \ t1 : tBOOL; \ \ t2 : T; \ \ t3 : T\ \ \ \ IF t1 t2 t3 : T" | t_ZET[intro]: "\ \ t : tINT \ \ \ ZET t : tBOOL" | t_EQI[intro]: "\\ \ t1 : tINT; \ \ t2 : tINT\ \ \ \ EQI t1 t2 : tBOOL" | t_FIX[intro]: "\x\\; (x,T)#\ \ t : T\ \ \ \ FIX [x].t : T" declare lam.inject[simp] inductive_cases typing_inversion[elim]: "\ \ t\<^isub>1 -- t\<^isub>2 : T" "\ \ t\<^isub>1 ++ t\<^isub>2 : T" "\ \ IF t1 t2 t3 : T" "\ \ ZET t : T" "\ \ EQI t1 t2 : T" "\ \ APP t1 t2 : T" "\ \ TRUE : T" "\ \ FALSE : T" "\ \ NUM n : T" declare lam.inject[simp del] equivariance typing nominal_inductive typing by (simp_all add: abs_fresh ty_fresh) lemma t_LAM_inversion[dest]: assumes ty: "\ \ LAM [x].t : T" and fc: "x\\" shows "\T\<^isub>1 T\<^isub>2. T = T\<^isub>1 \ T\<^isub>2 \ (x,T\<^isub>1)#\ \ t : T\<^isub>2" using ty fc by (cases rule: typing.strong_cases) (auto simp add: alpha lam.inject abs_fresh ty_fresh) lemma t_FIX_inversion[dest]: assumes ty: "\ \ FIX [x].t : T" and fc: "x\\" shows "(x,T)#\ \ t : T" using ty fc by (cases rule: typing.strong_cases) (auto simp add: alpha lam.inject abs_fresh ty_fresh) section {* The Type-Preservation Property for the CBV Reduction Relation *} lemma weakening: fixes \1 \2::"tctx" assumes a: "\1 \ t : T" and b: "valid \2" and c: "\1 \ \2" shows "\2 \ t : T" using a b c by (nominal_induct \1 t T avoiding: \2 rule: typing.strong_induct) (auto | atomize)+ lemma type_substitution_aux: assumes a: "(\@[(x,T')]@\) \ e : T" and b: "\ \ e' : T'" shows "(\@\) \ e[x::=e'] : T" using a b proof (nominal_induct \'\"\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) case (t_VAR \' y T x e' \) then have a1: "valid (\@[(x,T')]@\)" and a2: "(y,T) \ set (\@[(x,T')]@\)" and a3: "\ \ e' : T'" by simp_all from a1 have a4: "valid (\@\)" by (rule valid_insert) { assume eq: "x=y" from a1 a2 have "T=T'" using eq by (auto intro: context_unique) with a3 have "\@\ \ VAR y[x::=e'] : T" using eq a4 by (auto intro: weakening) } moreover { assume ineq: "x\y" from a2 have "(y,T) \ set (\@\)" using ineq by simp then have "\@\ \ VAR y[x::=e'] : T" using ineq a4 by auto } ultimately show "\@\ \ VAR y[x::=e'] : T" by blast qed (auto | force simp add: fresh_list_append fresh_list_cons)+ corollary type_substitution: assumes a: "(x,T')#\ \ e : T" and b: "\ \ e' : T'" shows "\ \ e[x::=e'] : T" using a b by (auto intro: type_substitution_aux[where \="[]",simplified]) theorem cbv_type_preservation: assumes a: "t \cbv t'" and b: "\ \ t : T" shows "\ \ t' : T" using a b apply(nominal_induct avoiding: \ T rule: cbv.strong_induct) apply(auto elim!: typing_inversion dest: t_LAM_inversion simp add: type_substitution) apply(frule t_FIX_inversion) apply(auto simp add: type_substitution) done corollary cbv_star_type_preservation: assumes a: "t \cbv* t'" and b: "\ \ t : T" shows "\ \ t' : T" using a b by (induct) (auto intro: cbv_type_preservation) section {* The Type-Preservation Property for the Machine and Evaluation Relation *} theorem machine_type_preservation: assumes a: " \* " and b: "\ \ t : T" shows "\ \ t' : T" proof - from a have "t \cbv* t'" by (simp add: machine_star_implies_cbv_star) then show "\ \ t' : T" using b by (simp add: cbv_star_type_preservation) qed theorem eval_type_preservation: assumes a: "t \ t'" and b: "\ \ t : T" shows "\ \ t' : T" proof - from a have " \* " by (simp add: eval_implies_machine_star) then show "\ \ t' : T" using b by (simp add: machine_type_preservation) qed text {* The Progress Property *} lemma canonical_tARR[dest]: assumes a: "[] \ t : T1 \ T2" and b: "val t" shows "\x t'. t = LAM [x].t'" using b a by (induct) (auto) lemma canonical_tINT[dest]: assumes a: "[] \ t : tINT" and b: "val t" shows "\n. t = NUM n" using b a by (induct) (auto simp add: fresh_list_nil) lemma canonical_tBOOL[dest]: assumes a: "[] \ t : tBOOL" and b: "val t" shows "t = TRUE \ t = FALSE" using b a by (induct) (auto simp add: fresh_list_nil) theorem progress: assumes a: "[] \ t : T" shows "(\t'. t \cbv t') \ (val t)" using a by (induct \\"[]::tctx" t T) (auto dest!: canonical_tINT intro!: cbv.intros gr0I) end