# HG changeset patch # User urbanc # Date 1213669190 -7200 # Node ID e5787c5be196d5af1e545f54446d5cdae142f797 # Parent df85326af57c244ab35be057042d20e641b173b1 added a progress lemma and tuned some comments diff -r df85326af57c -r e5787c5be196 src/HOL/Nominal/Examples/CK_Machine.thy --- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Jun 16 22:20:59 2008 +0200 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy Tue Jun 17 04:19:50 2008 +0200 @@ -9,15 +9,17 @@ 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 to get the induction - through. Type preservation is proved for the machine and also for - the small- and big-step semantics. + 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 theory is inspired by notes of Roshan James from Indiana University - and the lecture notes by Andy Pitts for his semantics course. See + 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/ + http://www.cs.indiana.edu/~rpjames/lm.pdf + http://www.cl.cam.ac.uk/teaching/2001/Semantics/ *} @@ -28,12 +30,12 @@ | APP "lam" "lam" | LAM "\name\lam" ("LAM [_]._") | NUM "nat" -| DIFF "lam" "lam" ("_ -- _") -| PLUS "lam" "lam" ("_ ++ _") +| DIFF "lam" "lam" ("_ -- _") (* subtraction *) +| PLUS "lam" "lam" ("_ ++ _") (* addition *) | TRUE | FALSE | IF "lam" "lam" "lam" -| FIX "\name\lam" ("FIX [_]._") +| FIX "\name\lam" ("FIX [_]._") (* recursion *) | ZET "lam" (* zero test *) | EQI "lam" "lam" (* equality test on numbers *) @@ -94,6 +96,8 @@ | CEQIL "ctx" "lam" | CEQIR "lam" "ctx" +text {* The operation of filling a term into a context: *} + fun filling :: "ctx \ lam \ lam" ("_\_\") where @@ -109,6 +113,8 @@ | "(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 @@ -128,13 +134,15 @@ 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 {* CK Machine *} +section {* The CK-Machine *} inductive val :: "lam\bool" @@ -186,7 +194,7 @@ shows " \* " using a by (rule ms2) (rule ms1) -section {* Evaluation Relation *} +section {* The Evaluation Relation (Big-Step Semantics) *} inductive eval :: "lam\lam\bool" ("_ \ _") @@ -229,6 +237,8 @@ shows "t \ t" using a by (induct) (auto) +text {* The Completeness Property: *} + theorem eval_implies_machine_star_ctx: assumes a: "t \ t'" shows " \* " @@ -236,14 +246,12 @@ by (induct arbitrary: Es) (metis eval_to machine.intros ms1 ms2 ms3 ms4 v_LAM)+ -text {* Completeness Property *} - corollary eval_implies_machine_star: assumes a: "t \ t'" shows " \* " using a by (auto dest: eval_implies_machine_star_ctx) -section {* CBV Reduction Relation *} +section {* The CBV Reduction Relation (Small-Step Semantics) *} lemma less_eqvt[eqvt]: fixes pi::"name prm" @@ -254,7 +262,7 @@ inductive cbv :: "lam\lam\bool" ("_ \cbv _") where - cbv1': "\val v; x\v\ \ APP (LAM [x].t) v \cbv t[x::=v]" + 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" @@ -279,14 +287,14 @@ nominal_inductive cbv by (simp_all add: abs_fresh fresh_fact) -lemma cbv1[intro]: +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 "\ \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 @@ -342,7 +350,7 @@ by (induct) (auto simp add: eval_val cbv_star_eval dest: cbvs2) -text {* Soundness Property *} +text {* The Soundness Property *} theorem machine_star_implies_eval: assumes a: " \* " @@ -355,6 +363,8 @@ section {* Typing *} +text {* Types *} + nominal_datatype ty = tVAR "string" | tBOOL @@ -370,13 +380,19 @@ 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 @@ -409,7 +425,7 @@ using a1 a2 a3 by (induct) (auto simp add: fresh_set fresh_prod fresh_atm) -section {* Typing Relation *} +section {* The Typing Relation *} inductive typing :: "tctx \ lam \ ty \ bool" ("_ \ _ : _") @@ -435,6 +451,9 @@ "\ \ 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 @@ -457,7 +476,7 @@ by (cases rule: typing.strong_cases) (auto simp add: alpha lam.inject abs_fresh ty_fresh) -section {* Type Preservation for the CBV Reduction Relation *} +section {* The Type-Preservation Property for the CBV Reduction Relation *} lemma weakening: fixes \1 \2::"tctx" @@ -517,7 +536,7 @@ using a b by (induct) (auto intro: cbv_type_preservation) -section {* Type Preservation for the Machine and Evaluation Relation *} +section {* The Type-Preservation Property for the Machine and Evaluation Relation *} theorem machine_type_preservation: assumes a: " \* " @@ -537,6 +556,35 @@ 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