theory Solution08_1 imports Complex_Main "HOL-IMP.BExp" "HOL-IMP.Star" begin datatype val = Iv int | Rv real type_synonym vname = string type_synonym state = "vname \ val" datatype aexp = Ic int | Rc real | V vname | Plus aexp aexp 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 (Rv r2) \ taval (Plus a1 a2) s (Rv(r1+r2))" (*** BEGIN MODIFICATION **) | "taval a1 s (Iv (r1)) \ taval a2 s (Rv r2) \ taval (Plus a1 a2) s (Rv(r1+r2))" | "taval a1 s (Rv r1) \ taval a2 s (Iv r2) \ taval (Plus a1 a2) s (Rv(r1+r2))" (*** END MODIFICATION **) inductive_cases [elim!]: "taval (Ic i) s v" "taval (Rc i) s v" "taval (V x) s v" "taval (Plus a1 a2) s v" 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)" (*** BEGIN MODIFICATION **) |"taval a1 s (Iv i1) \ taval a2 s (Rv i2) \ tbval (Less a1 a2) s (i1 < i2)" |"taval a1 s (Rv r1) \ taval a2 s (Iv r2) \ tbval (Less a1 a2) s (r1 < r2)" (*** END MODIFICATION **) 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) 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)] 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" | (*** BEGIN MODIFICATION **) Plus_ty_ii: "\ \ a1 : Ity \ \ \ a2 : Ity \ \ \ Plus a1 a2 : Ity" |Plus_ty_tr: "\ \ a1 : _ \ \ \ a2 : Rty \ \ \ Plus a1 a2 : Rty" |Plus_ty_rt: "\ \ a1 : Rty \ \ \ a2 : _ \ \ \ Plus a1 a2 : Rty" (*** END MODIFICATION **) inductive btyping :: "tyenv \ bexp \ bool" (infix "\" 50) where B_ty: "\ \ Bc v" | Not_ty: "\ \ b \ \ \ Not b" | And_ty: "\ \ b1 \ \ \ b2 \ \ \ And b1 b2" | (*** BEGIN MODIFICATION **) Less_ty: "\ \ a1 : \ \ \ \ a2 : \' \ \ \ Less a1 a2" (*** END MODIFICATION **) inductive ctyping :: "tyenv \ com \ bool" (infix "\" 50) where Skip_ty: "\ \ SKIP" | (* No implicit coercion here *) 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" inductive_cases [elim!]: "\ \ x ::= a" "\ \ c1;;c2" "\ \ IF b THEN c1 ELSE c2" "\ \ WHILE b DO c" fun type :: "val \ ty" where "type (Iv i) = Ity" | "type (Rv r) = Rty" lemma [simp]: "type v = Ity \ (\i. v = Iv i)" by (cases v) simp_all lemma [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 = \" by (induction arbitrary: v rule: atyping.induct) (fastforce simp: styping_def)+ lemma aprogress: "\ \ a : \ \ \ \ s \ \v. taval a s v" proof(induction rule: atyping.induct) (*** BEGIN MODIFICATION **) case (Plus_ty_ii \ a1 a2) then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast with Plus_ty_ii show ?case by (fastforce intro: taval.intros dest!: apreservation) next case (Plus_ty_tr \ a1 t a2) then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast with Plus_ty_tr show ?case by (cases v1) (fastforce intro: taval.intros dest!: apreservation)+ next case (Plus_ty_rt \ a1 a2 t) then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast with Plus_ty_rt show ?case by (cases v2) (fastforce intro: taval.intros dest!: apreservation)+ (*** END MODIFICATION **) 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) (*** BEGIN MODIFICATION **) 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 (*** END MODIFICATION **) 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''" proof (induction rule:star_induct) case refl then show ?case by (metis progress) next case step then show ?case by (metis styping_preservation ctyping_preservation) qed end