theory tut06 imports "HOL-IMP.Compiler" Complex_Main begin fun ccomp :: "com \ instr list" where "ccomp SKIP = []" | "ccomp (x ::= a) = acomp a @ [STORE x]" | "ccomp (c\<^sub>1;;c\<^sub>2) = ccomp c\<^sub>1 @ ccomp c\<^sub>2" | "ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = ( if c\<^sub>2 = SKIP then (let cc\<^sub>1 = ccomp c\<^sub>1; cb = bcomp b False (size cc\<^sub>1) in cb @ cc\<^sub>1) else (let cc\<^sub>1 = ccomp c\<^sub>1; cc\<^sub>2 = ccomp c\<^sub>2; cb = bcomp b False (size cc\<^sub>1 + 1) in cb @ cc\<^sub>1 @ JMP (size cc\<^sub>2) # cc\<^sub>2))" | "ccomp (WHILE b DO c) = (let cc = ccomp c; cb = bcomp b False (size cc + 1) in cb @ cc @ [JMP (-(size cb + size cc + 1))])" value "ccomp (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1) ELSE ''v'' ::= V ''u'')" value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))" subsection "Preservation of semantics" thm ccomp.simps lemma ccomp_bigstep: "(c,s) \ t \ ccomp c \ (0,s,stk) \* (size(ccomp c),t,stk)" proof(induction arbitrary: stk rule: big_step_induct) case (Assign x a s) show ?case by (fastforce simp:fun_upd_def cong: if_cong) next case (Seq c1 s1 s2 c2 s3) let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2" have "?cc1 @ ?cc2 \ (0,s1,stk) \* (size ?cc1,s2,stk)" using Seq.IH(1) by fastforce moreover have "?cc1 @ ?cc2 \ (size ?cc1,s2,stk) \* (size(?cc1 @ ?cc2),s3,stk)" using Seq.IH(2) by fastforce ultimately show ?case by simp (blast intro: star_trans) next case (WhileTrue b s1 c s2 s3) let ?cc = "ccomp c" let ?cb = "bcomp b False (size ?cc + 1)" let ?cw = "ccomp(WHILE b DO c)" have "?cw \ (0,s1,stk) \* (size ?cb,s1,stk)" using \bval b s1\ by fastforce moreover have "?cw \ (size ?cb,s1,stk) \* (size ?cb + size ?cc,s2,stk)" using WhileTrue.IH(1) by fastforce moreover have "?cw \ (size ?cb + size ?cc,s2,stk) \* (0,s2,stk)" by fastforce moreover have "?cw \ (0,s2,stk) \* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2)) ultimately show ?case by(blast intro: star_trans) next case (IfTrue b s c\<^sub>1 t c\<^sub>2) let ?cb = "bcomp b False (size (ccomp c\<^sub>1))" let ?cc1 = "ccomp c\<^sub>1" let ?cc2 = "ccomp c\<^sub>2" let ?cb2 = "bcomp b False (size (ccomp c\<^sub>1) + 1)" from \bval b s\ have 1: "?cb @ ?cc1 \ (0, s, stk) \* (size ?cb, s, stk)" by fastforce show ?case proof (cases "c\<^sub>2 = SKIP") case True with IfTrue.IH have "?cc1 \ (0, s, stk) \* (size ?cc1, t, stk)" by auto then have "?cb @ ?cc1 \ (size ?cb, s, stk) \* (size ?cb + size ?cc1, t, stk)" by auto with 1 True show ?thesis by (fastforce intro: star_trans) next case False let ?c = "?cb2 @ ?cc1 @ JMP (size ?cc2) # ?cc2" from False have [simp]: "ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = ?cb2 @ ?cc1 @ JMP (size ?cc2) # ?cc2" by (cases c\<^sub>2) auto from \bval b s\ have 1: "?c \ (0, s, stk) \* (size ?cb2, s, stk)" by fastforce moreover from IfTrue.IH have "?c \ (size ?cb2, s, stk) \* (size ?cb2 + size ?cc1, t, stk)" by fastforce moreover from \bval b s\ have 1: "?c \ (size ?cb2 + size ?cc1, t, stk) \* (size ?cb2 + size ?cc1 + size ?cc2 + 1, t, stk)" by fastforce ultimately show ?thesis using 1 False by (fastforce intro: star_trans) qed next case (IfFalse b s c\<^sub>2 t c\<^sub>1) then show ?case by fastforce qed fastforce+ 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 (Iv i1) \ taval a2 s (Rv i2) \ taval (Plus a1 a2) s (Rv(real_of_int i1+i2))" | "taval a1 s (Rv i1) \ taval a2 s (Iv i2) \ taval (Plus a1 a2) s (Rv(i1+real_of_int i2))" | "taval a1 s (Rv r1) \ taval a2 s (Rv r2) \ taval (Plus a1 a2) s (Rv(r1+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 (Iv i1) \ taval a2 s (Rv i2) \ tbval (Less a1 a2) s (i1 < i2)" | "taval a1 s (Rv 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)" 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: "\ \ a1 : \ \ \ \ a2 : \ \ \ \ Plus a1 a2 : \" declare atyping.intros [intro!] inductive_cases [elim!]: "\ \ V x : \" "\ \ Ic i : \" "\ \ Rc r : \" "\ \ Plus a1 a2 : \" 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 \ 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 v show ?thesis by(fastforce intro: taval.intros(4) dest!: apreservation) next case Rv with Plus_ty v show ?thesis by (cases v2) (fastforce intro: taval.intros(5,7) dest!: apreservation)+ qed 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 (fastforce intro!: tbval.intros(4) dest!:apreservation) next case Rv with Less_ty v show ?thesis by (cases v2) (fastforce intro!: tbval.intros(5,7) 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