theory tut10_1 imports "~~/src/HOL/IMP/BExp" begin (** We extend commands by a REPEAT-UNTIL loop **) 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) (* begin mod *) | Repeat com bexp ("(REPEAT _/ UNTIL _)" [0, 61] 61) (* end mod *) (** Extension of the big-step semantics is straightforward **) inductive big_step :: "com \ state \ state \ bool" (infix "\" 55) where Skip: "(SKIP,s) \ s" | Assign: "(x ::= a,s) \ s(x := aval a s)" | Seq: "\ (c\<^sub>1,s\<^sub>1) \ s\<^sub>2; (c\<^sub>2,s\<^sub>2) \ s\<^sub>3 \ \ (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \ s\<^sub>3" | IfTrue: "\ bval b s; (c\<^sub>1,s) \ t \ \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ t" | IfFalse: "\ \bval b s; (c\<^sub>2,s) \ t \ \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ t" | WhileFalse: "\bval b s \ (WHILE b DO c,s) \ s" | WhileTrue: "\ bval b s\<^sub>1; (c,s\<^sub>1) \ s\<^sub>2; (WHILE b DO c, s\<^sub>2) \ s\<^sub>3 \ \ (WHILE b DO c, s\<^sub>1) \ s\<^sub>3" (* begin mod *) | RepeatTrue: "\ (c,s1) \ s2; bval b s2 \ \ (REPEAT c UNTIL b,s1) \ s2" | RepeatFalse: "\ (c,s\<^sub>1) \ s\<^sub>2; \ bval b s\<^sub>2; (REPEAT c UNTIL b, s\<^sub>2) \ s\<^sub>3 \ \ (REPEAT c UNTIL b, s\<^sub>1) \ s\<^sub>3" (* end mod *) text{* Proof automation: *} declare big_step.intros [intro] lemmas big_step_induct = big_step.induct[split_format(complete)] subsection "Rule inversion" inductive_cases SkipE[elim!]: "(SKIP,s) \ t" inductive_cases AssignE[elim!]: "(x ::= a,s) \ t" inductive_cases SeqE[elim!]: "(c1;;c2,s1) \ s3" inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \ t" inductive_cases WhileE[elim]: "(WHILE b DO c,s) \ t" (* begin mod *) inductive_cases RepeatE[elim]: "(REPEAT c UNTIL b,s) \ t" thm RepeatE (* end mod *) subsection "Execution is deterministic" theorem big_step_determ: "\ (c,s) \ t; (c,s) \ u \ \ u = t" by (induction arbitrary: u rule: big_step.induct) blast+ (**! Now, modify the denotation semantics accordingly **) type_synonym com_den = "(state \ state) set" definition W :: "(state \ bool) \ com_den \ (com_den \ com_den)" where "W db dc = (\dw. {(s,t). if db s then (s,t) \ dc O dw else s=t})" find_theorems relcomp (* begin mod *) definition R :: "(state \ bool) \ com_den \ (com_den \ com_den)" (* won't work probably: where "R rb rc == (\dr. {(s,t). if rb t then (s,t)\rc else (s,t)\rc O dr })"*) where "R rb rc == (\dr. rc O {(s,t). if rb s then s=t else (s,t)\dr} )" (* end mod *) fun D :: "com \ com_den" where "D SKIP = Id" | "D (x ::= a) = {(s,t). t = s(x := aval a s)}" | "D (c1;;c2) = D(c1) O D(c2)" | "D (IF b THEN c1 ELSE c2) = {(s,t). if bval b s then (s,t) \ D c1 else (s,t) \ D c2}" | "D (WHILE b DO c) = lfp (W (bval b) (D c))" | (* begin mod *) "D (REPEAT c UNTIL b) = lfp (R (bval b) (D c))" (**! What is the denotation of REPEAT ?**) (* end mod *) lemma W_mono: "mono (W b r)" by (unfold W_def mono_def) auto lemma R_mono: "mono (R b r)" by (unfold R_def mono_def) auto lemma D_While_If: "D(WHILE b DO c) = D(IF b THEN c;;WHILE b DO c ELSE SKIP)" proof- let ?w = "WHILE b DO c" let ?f = "W (bval b) (D c)" have "D ?w = lfp ?f" by simp also have "\ = ?f (lfp ?f)" by(rule lfp_unfold [OF W_mono]) also have "\ = D(IF b THEN c;;?w ELSE SKIP)" by (simp add: W_def) finally show ?thesis . qed thm lfp_unfold (* begin mod *) lemma D_Repeat_If: "D(REPEAT c UNTIL b) = D(c;; IF b THEN SKIP ELSE REPEAT c UNTIL b)" apply simp apply (subst lfp_unfold[OF R_mono]) apply (auto simp: R_def) done lemmas [simp del] = D.simps(5,6) (** \ This may help you to prevent simp from unfolding D WHILE and D REPEAT to their fixed point definitions, and thus preventing application of D_While_If, D_Repeat_If after simp or auto are called **) (* end mod *) text{* Equivalence of denotational and big-step semantics: *} lemma D_if_big_step: "(c,s) \ t \ (s,t) \ D(c)" proof (induction rule: big_step_induct) case WhileFalse with D_While_If show ?case by auto next case WhileTrue show ?case unfolding D_While_If using WhileTrue by auto (* begin mod *) next case RepeatFalse show ?case unfolding D_Repeat_If using RepeatFalse by auto next case RepeatTrue show ?case unfolding D_Repeat_If using RepeatTrue by auto qed auto abbreviation Big_step :: "com \ com_den" where "Big_step c \ {(s,t). (c,s) \ t}" lemma Big_step_if_D: "(s,t) \ D(c) \ (s,t) : Big_step c" proof (induction c arbitrary: s t) case Seq thus ?case by fastforce next case (While b c) let ?B = "Big_step (WHILE b DO c)" let ?f = "W (bval b) (D c)" have "?f ?B \ ?B" using While.IH by (auto simp: W_def) from lfp_lowerbound[where ?f = "?f", OF this] While.prems show ?case by (auto simp: D.simps) next case (Repeat c b) let ?B = "Big_step (REPEAT c UNTIL b)" let ?f = "R (bval b) (D c)" have "?f ?B \ ?B" using Repeat.IH by (auto simp: R_def) from lfp_lowerbound[where ?f = "?f", OF this] Repeat.prems show ?case by (auto simp: D.simps) qed (auto split: if_splits) theorem denotational_is_big_step: "(s,t) \ D(c) = ((c,s) \ t)" by (metis D_if_big_step Big_step_if_D[simplified]) end