section "A Typed Language" theory Ex06_Types imports "HOL-IMP.Star" Complex_Main begin text \We build on \<^theory>\Complex_Main\ instead of \<^theory>\Main\ to access the real numbers.\ subsection "Arithmetic Expressions" datatype val = Iv int | Rv real type_synonym vname = string type_synonym state = "vname \ val" text_raw\\snip{aexptDef}{0}{2}{%\ datatype aexp = Ic int | Rc real | V vname | Plus aexp aexp text_raw\}%endsnip\ inductive taval :: "aexp \ state \ val \ bool" where "taval (Ic i) s (Iv i)" | "taval (Rc r) s (Rv r)" | "taval (V x) s (s x)" | "taval a1 s (Iv i1) \ taval a2 s (Iv i2) \ taval (Plus a1 a2) s (Iv(i1+i2))" | "taval a1 s (Rv r1) \ taval a2 s (Iv i2) \ taval (Plus a1 a2) s (Rv(r1+i2))" | "taval a1 s (Iv i1) \ taval a2 s (Rv r2) \ taval (Plus a1 a2) s (Rv(i1+r2))" | "taval a1 s (Rv v1) \ taval a2 s (Rv r2) \ taval (Plus a1 a2) s (Rv(v1+r2))" inductive_cases [elim!]: "taval (Ic i) s v" "taval (Rc i) s v" "taval (V x) s v" "taval (Plus a1 a2) s v" subsection "Boolean Expressions" datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp inductive tbval :: "bexp \ state \ bool \ bool" where "tbval (Bc v) s v" | "tbval b s bv \ tbval (Not b) s (\ bv)" | "tbval b1 s bv1 \ tbval b2 s bv2 \ tbval (And b1 b2) s (bv1 & bv2)" | "taval a1 s (Iv i1) \ taval a2 s (Iv i2) \ tbval (Less a1 a2) s (i1 < i2)" | "taval a1 s (Rv r1) \ taval a2 s (Rv r2) \ tbval (Less a1 a2) s (r1 < r2)" | "taval a1 s (Iv i1) \ taval a2 s (Rv r2) \ tbval (Less a1 a2) s (i1 < r2)" | "taval a1 s (Rv r1) \ taval a2 s (Iv i2) \ tbval (Less a1 a2) s (r1 < i2)" subsection "Syntax of Commands" (* a copy of Com.thy - keep in sync! *) datatype com = SKIP | Assign vname aexp ("_ ::= _" [1000, 61] 61) | Seq com com ("_;; _" [60, 61] 60) | If bexp com com ("IF _ THEN _ ELSE _" [0, 0, 61] 61) | While bexp com ("WHILE _ DO _" [0, 61] 61) subsection "Small-Step Semantics of Commands" inductive small_step :: "(com \ state) \ (com \ state) \ bool" (infix "\" 55) where Assign: "taval 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: "tbval b s True \ (IF b THEN c1 ELSE c2,s) \ (c1,s)" | IfFalse: "tbval b s 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 | Rty type_synonym tyenv = "vname \ ty" inductive atyping :: "tyenv \ aexp \ ty \ bool" ("(1_/ \/ (_ :/ _))" [50,0,50] 50) where Ic_ty: "\ \ Ic i : Ity" | Rc_ty: "\ \ Rc r : Rty" | V_ty: "\ \ V x : \ x" | Plus_ty_tt: "\ \ a1 : \ \ \ \ a2 : \ \ \ \ Plus a1 a2 : \" | Plus_ty_ri: "\ \ a1 : Rty \ \ \ a2 : Ity \ \ \ Plus a1 a2 : Rty" | Plus_ty_ir: "\ \ a1 : Ity \ \ \ a2 : Rty \ \ \ Plus a1 a2 : Rty" declare atyping.intros [intro!] inductive_cases [elim!]: "\ \ V x : \" "\ \ Ic i : \" "\ \ Rc r : \" "\ \ Plus a1 a2 : \" "\ \ Plus a1 a2 : Rty" text\Warning: the ``:'' notation leads to syntactic ambiguities, i.e. multiple parse trees, because ``:'' also stands for set membership. In most situations Isabelle's type system will reject all but one parse tree, but will still inform you of the potential ambiguity.\ inductive btyping :: "tyenv \ bexp \ bool" (infix "\" 50) where B_ty: "\ \ Bc v" | Not_ty: "\ \ b \ \ \ Not b" | And_ty: "\ \ b1 \ \ \ b2 \ \ \ And b1 b2" | Less_ty: "\ \ a1 : \ \ \ \ a2 : \' \ \ \ Less a1 a2" declare btyping.intros [intro!] inductive_cases [elim!]: "\ \ Not b" "\ \ And b1 b2" "\ \ Less a1 a2" 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 \ \ \ c1 \ \ \ c2 \ \ \ IF b THEN c1 ELSE c2" | While_ty: "\ \ b \ \ \ c \ \ \ WHILE b DO c" declare ctyping.intros [intro!] 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 (Rv r) = Rty" lemma type_eq_Ity[simp]: "type v = Ity \ (\i. v = Iv i)" by (cases v) simp_all lemma type_eq_Rty[simp]: "type v = Rty \ (\r. v = Rv r)" by (cases v) simp_all definition styping :: "tyenv \ state \ bool" (infix "\" 50) where "\ \ s \ (\x. type (s x) = \ x)" lemma apreservation: "\ \ a : \ \ taval a s v \ \ \ s \ type v = \" apply(induction arbitrary: v rule: atyping.induct) apply (fastforce simp: styping_def)+ done lemma aprogress: "\ \ a : \ \ \ \ s \ \v. taval a s v" proof(induction rule: atyping.induct) case (Plus_ty_tt \ a1 t a2) then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast show ?case proof (cases v1) case Iv with Plus_ty_tt v show ?thesis by(fastforce intro: taval.intros(4) dest!: apreservation) next case Rv with Plus_ty_tt v show ?thesis by(fastforce intro: taval.intros dest!: apreservation) qed next case (Plus_ty_ri \ a1 a2) then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast then show ?case by (metis taval.intros type.cases) next case (Plus_ty_ir \ a1 a2) then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast then show ?case by (metis taval.intros type.cases) qed (auto intro: taval.intros) lemma bprogress: "\ \ b \ \ \ s \ \v. tbval b s v" proof(induction rule: btyping.induct) case (Less_ty \ a1 t a2) then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by (metis aprogress) show ?case proof (cases v1) case Iv with Less_ty v show ?thesis by (cases v2) (fastforce intro!: tbval.intros dest!:apreservation)+ next case Rv with Less_ty v show ?thesis by (cases v2) (fastforce intro!: tbval.intros dest!:apreservation)+ qed qed (auto intro: tbval.intros) theorem progress: "\ \ c \ \ \ s \ c \ SKIP \ \cs'. (c,s) \ cs'" proof(induction rule: ctyping.induct) case Skip_ty thus ?case by simp next case Assign_ty thus ?case by (metis Assign aprogress) next case Seq_ty thus ?case by simp (metis Seq1 Seq2) next case (If_ty \ b c1 c2) then obtain bv where "tbval b s bv" by (metis bprogress) show ?case proof(cases bv) assume "bv" with \tbval b s bv\ show ?case by simp (metis IfTrue) next assume "\bv" with \tbval b s bv\ show ?case by simp (metis IfFalse) qed next case While_ty show ?case by (metis While) qed theorem styping_preservation: "(c,s) \ (c',s') \ \ \ c \ \ \ s \ \ \ s'" proof(induction rule: small_step_induct) case Assign thus ?case by (auto simp: styping_def) (metis Assign(1,3) apreservation) qed auto theorem ctyping_preservation: "(c,s) \ (c',s') \ \ \ c \ \ \ c'" by (induct rule: small_step_induct) (auto simp: ctyping.intros) 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''" apply(induction rule:star_induct) apply (metis progress) by (metis styping_preservation ctyping_preservation) end