header "A Typed Language" theory hw08_tmpl imports "~~/src/HOL/IMP/Star" begin subsection "Expressions" datatype val = Iv int | Bv bool type_synonym vname = string type_synonym state = "vname \ val" datatype exp = N int | V vname | Plus exp exp | Bc bool | Not exp | And exp exp | Less exp exp inductive eval :: "exp \ state \ val \ bool" where "eval (N i) s (Iv i)" | "eval (V x) s (s x)" | "eval a1 s (Iv i1) \ eval a2 s (Iv i2) \ eval (Plus a1 a2) s (Iv(i1+i2))" | "eval (Bc v) s (Bv v)" | "eval b s (Bv bv) \ eval (Not b) s (Bv(\ bv))" | "eval b1 s (Bv bv1) \ eval b2 s (Bv bv2) \ eval (And b1 b2) s (Bv(bv1 & bv2))" | "eval a1 s (Iv i1) \ eval a2 s (Iv i2) \ eval (Less a1 a2) s (Bv(i1 < i2))" inductive_cases [elim!]: "eval (N i) s v" "eval (V x) s v" "eval (Plus a1 a2) s v" "eval (Bc b) s v" "eval (Not b) s v" "eval (And b1 b2) s v" "eval (Less a1 a2) s v" subsection "Syntax of Commands" (* a copy of Com.thy - keep in sync! *) datatype com = SKIP | Assign vname exp ("_ ::= _" [1000, 61] 61) | Seq com com ("_;; _" [60, 61] 60) | If exp com com ("IF _ THEN _ ELSE _" [0, 0, 61] 61) | While exp com ("WHILE _ DO _" [0, 61] 61) subsection "Small-Step Semantics of Commands" inductive small_step :: "(com \ state) \ (com \ state) \ bool" (infix "\" 55) where Assign: "eval a s v \ (x ::= a, s) \ (SKIP, s(x := v))" | Seq1: "(SKIP;;c,s) \ (c,s)" | Seq2: "(c1,s) \ (c1',s') \ (c1;;c2,s) \ (c1';;c2,s')" | IfTrue: "eval b s (Bv True) \ (IF b THEN c1 ELSE c2,s) \ (c1,s)" | IfFalse: "eval b s (Bv False) \ (IF b THEN c1 ELSE c2,s) \ (c2,s)" | While: "(WHILE b DO c,s) \ (IF b THEN c;; WHILE b DO c ELSE SKIP,s)" lemmas small_step_induct = small_step.induct[split_format(complete)] subsection "The Type System" datatype ty = Ity | Bty type_synonym tyenv = "vname \ ty" inductive etyping :: "tyenv \ exp \ ty \ bool" ("(1_/ \/ (_ :/ _))" [50,0,50] 50) where Ic_ty: "\ \ N i : Ity" | V_ty: "\ \ V x : \ x" | Plus_ty: "\ \ a1 : Ity \ \ \ a2 : Ity \ \ \ Plus a1 a2 : Ity" | B_ty: "\ \ Bc v : Bty" | Not_ty: "\ \ b : Bty \ \ \ Not b : Bty" | And_ty: "\ \ b1 : Bty \ \ \ b2 : Bty \ \ \ And b1 b2 : Bty" | Less_ty: "\ \ a1 : Ity \ \ \ a2 : Ity \ \ \ Less a1 a2 : Bty" inductive ctyping :: "tyenv \ com \ bool" (infix "\" 50) where Skip_ty: "\ \ SKIP" | Assign_ty: "\ \ a : \(x) \ \ \ x ::= a" | Seq_ty: "\ \ c1 \ \ \ c2 \ \ \ c1;;c2" | If_ty: "\ \ b : Bty \ \ \ c1 \ \ \ c2 \ \ \ IF b THEN c1 ELSE c2" | While_ty: "\ \ b : Bty \ \ \ c \ \ \ WHILE b DO c" inductive_cases [elim!]: "\ \ x ::= a" "\ \ c1;;c2" "\ \ IF b THEN c1 ELSE c2" "\ \ WHILE b DO c" subsection "Well-typed Programs Do Not Get Stuck" fun type :: "val \ ty" where "type (Iv i) = Ity" | "type (Bv r) = Bty" lemma type_eq_Ity[simp]: "type v = Ity \ (\i. v = Iv i)" by (cases v) simp_all lemma type_eq_Bty[simp]: "type v = Bty \ (\r. v = Bv r)" by (cases v) simp_all definition styping :: "tyenv \ state \ bool" (infix "\" 50) where "\ \ s \ (\x. type (s x) = \ x)" lemma epreservation: "\ \ a : \ \ eval a s v \ \ \ s \ type v = \" oops lemma eprogress: "\ \ a : \ \ \ \ s \ \v. eval a s v" oops theorem progress: "\ \ c \ \ \ s \ c \ SKIP \ \cs'. (c,s) \ cs'" oops theorem styping_preservation: "(c,s) \ (c',s') \ \ \ c \ \ \ s \ \ \ s'" oops theorem ctyping_preservation: "(c,s) \ (c',s') \ \ \ c \ \ \ c'" oops abbreviation small_steps :: "com * state \ com * state \ bool" (infix "\*" 55) where "x \* y == star small_step x y" theorem type_sound: "(c,s) \* (c',s') \ \ \ c \ \ \ s \ c' \ SKIP \ \cs''. (c',s') \ cs''" oops end