(*<*) theory Big_StepT imports "~~/src/HOL/IMP/Big_Step" begin (*>*) text \\NumHomework{A Hoare Calculus with Execution Times}{31~January~2017}\ text \ In this homework, we will consider a hoare calculus with execution times. We first give a modified big-step semantics to account for execution times. A judgement of the form \(c, s) \ n \ t\ has the intended meaning that we can get from state \s\ to state \t\ by an terminating execution of program \c\ that takes exactly \n\ time steps. \ (*<*) subsection "Big-Step with Time Semantics of Commands" (*>*) inductive big_step_t :: "com \ state \ nat \ state \ bool" ("_ \ _ \ _" 55) where Skip: "(SKIP,s) \ Suc 0 \ s" | Assign: "(x ::= a,s) \ Suc 0 \ s(x := aval a s)" | Seq: "\ (c1,s1) \ x \ s2; (c2,s2) \ y \ s3 ; z=x+y \ \ (c1;;c2, s1) \ z \ s3" | IfTrue: "\ bval b s; (c1,s) \ x \ t; y=x+1 \ \ (IF b THEN c1 ELSE c2, s) \ y \ t" | IfFalse: "\ \bval b s; (c2,s) \ x \ t; y=x+1 \ \ (IF b THEN c1 ELSE c2, s) \ y \ t" | WhileFalse: "\ \bval b s \ \ (WHILE b DO c,s) \ Suc 0 \ s" | WhileTrue: "\ bval b s1; (c,s1) \ x \ s2; (WHILE b DO c, s2) \ y \ s3; 1+x+y=z \ \ (WHILE b DO c, s1) \ z \ s3" (*<*) schematic_goal ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \ ?g \ ?t" apply(rule Seq) apply(rule Assign) apply(simp) apply(rule Assign) apply simp done thm ex[simplified] text{* We want to execute the big-step rules: *} code_pred big_step_t . text{* For inductive definitions we need command \texttt{values} instead of \texttt{value}. *} values "{(t, x). (SKIP, \_. 0) \ x \ t}" text{* We need to translate the result state into a list to display it. *} values "{map t [''x''] |t x. (SKIP, <''x'' := 42>) \ x \ t}" values "{map t [''x''] |t x. (''x'' ::= N 2, <''x'' := 42>) \ x \ t}" values "{map t [''x'',''y''] |t x. (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)), <''x'' := 0, ''y'' := 13>) \ x \ t}" text{* Proof automation: *} declare big_step_t.intros [intro] thm big_step_t.induct lemmas big_step_t_induct = big_step_t.induct[split_format(complete)] thm big_step_t_induct subsection "Rule inversion" text{* What can we deduce from @{prop "(SKIP,s) \ x \ t"} ? That @{prop "s = t"}. This is how we can automatically prove it: *} inductive_cases Skip_tE[elim!]: "(SKIP,s) \ x \ t" thm Skip_tE text{* This is an \emph{elimination rule}. The [elim] attribute tells auto, blast and friends (but not simp!) to use it automatically; [elim!] means that it is applied eagerly. Similarly for the other commands: *} inductive_cases Assign_tE[elim!]: "(x ::= a,s) \ p \ t" thm Assign_tE inductive_cases Seq_tE[elim!]: "(c1;;c2,s1) \ p \ s3" thm Seq_tE inductive_cases If_tE[elim!]: "(IF b THEN c1 ELSE c2,s) \ x \ t" thm If_tE inductive_cases While_tE[elim]: "(WHILE b DO c,s) \ x \ t" thm While_tE text{* Only [elim]: [elim!] would not terminate. *} text{* An automatic example: *} lemma "(IF b THEN SKIP ELSE SKIP, s) \ x \ t \ t = s" by blast text{* Rule inversion by hand via the ``cases'' method: *} lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \ x \ t" shows "t = s" proof- from assms show ?thesis proof cases --"inverting assms" case IfTrue thm IfTrue thus ?thesis by blast next case IfFalse thus ?thesis by blast qed qed (* Using rule inversion to prove simplification rules: *) lemma assign_t_simp: "(x ::= a,s) \ Suc 0 \ s' \ (s' = s(x := aval a s))" by (auto) text {* An example combining rule inversion and derivations *} lemma Seq_t_assoc: "((c1;; c2;; c3, s) \ p \ s') \ ((c1;; (c2;; c3), s) \ p \ s')" proof assume "(c1;; c2;; c3, s) \ p \ s'" then obtain s1 s2 p1 p2 p3 where c1: "(c1, s) \ p1 \ s1" and c2: "(c2, s1) \ p2 \ s2" and c3: "(c3, s2) \ p3 \ s'" and p: "p = p1 + (p2 + p3)" by auto from c2 c3 have "(c2;; c3, s1) \ p2 + p3 \ s'" apply (rule Seq) by simp with c1 show "(c1;; (c2;; c3), s) \ p \ s'" unfolding p apply (rule Seq) by simp next -- "The other direction is analogous" assume "(c1;; (c2;; c3), s) \ p \ s'" then obtain s1 s2 p1 p2 p3 where c1: "(c1, s) \ p1 \ s1" and c2: "(c2, s1) \ p2 \ s2" and c3: "(c3, s2) \ p3 \ s'" and p: "p = (p1 + p2) + p3" by auto from c1 c2 have "(c1;; c2, s) \ p1 + p2 \ s2" apply (rule Seq) by simp from this c3 show "(c1;; c2;; c3, s) \ p \ s'" unfolding p apply (rule Seq) by simp qed subsection "Relation to Big_Step Semantics" thm SkipE AssignE assign_simp thm Big_Step.Assign lemma "(\p. ((c, s) \ p \ s')) = ((c, s) \ s')" proof assume "\p. (c, s) \ p \ s'" then obtain p where "(c, s) \ p \ s'" try0 by blast then show "((c, s) \ s')" apply(induct c s p s' rule: big_step_t_induct) prefer 2 apply(rule Big_Step.Assign) apply(auto) done next assume "((c, s) \ s')" then show "(\p. ((c, s) \ p \ s'))" apply(induct c s s' rule: big_step_induct) by blast+ qed (* thus some properties carry over: *) (* subsection "Command Equivalence" text {* We call two statements @{text c} and @{text c'} equivalent wrt.\ the big-step semantics when \emph{@{text c} started in @{text s} terminates in @{text s'} iff @{text c'} started in the same @{text s} also terminates in the same @{text s'}}. Formally: *} text_raw{*\snip{BigStepEquiv}{0}{1}{% *} abbreviation equiv_c :: "com \ com \ bool" (infix "\" 50) where "c \ c' \ (\s t. \x1 x2. ((c,s) \ x1 \ t) = ((c',s) \ x2 \ t))" text_raw{*}%endsnip*} text {* Warning: @{text"\"} is the symbol written \verb!\ < s i m >! (without spaces). As an example, we show that loop unfolding is an equivalence transformation on programs: *} lemma unfold_while: "(WHILE b DO c) \ (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \ ?iw") proof - -- "to show the equivalence, we look at the derivation tree for" -- "each side and from that construct a derivation tree for the other side" { fix s t p assume "(?w, s) \ p \ t" -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s}," -- "then both statements do nothing:" { assume "\bval b s" hence "t = s" using `(?w,s) \p \ t` by blast hence "(?iw, s) \ p \ t" using `\bval b s` by blast } moreover -- "on the other hand, if @{text b} is @{text True} in state @{text s}," -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \ t"} *} { assume "bval b s" with `(?w, s) \ p \ t` obtain s' where "(c, s) \ p \ s'" and "(?w, s') \ p \ t" by auto -- "now we can build a derivation tree for the @{text IF}" -- "first, the body of the True-branch:" hence "(c;; ?w, s) \p \ t" by (rule Seq) -- "then the whole @{text IF}" with `bval b s` have "(?iw, s) \ p \ t" by (rule IfTrue) } ultimately -- "both cases together give us what we want:" have "(?iw, s) \p \ t" by blast } moreover -- "now the other direction:" { fix s t assume "(?iw, s) \p \ t" -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch" -- "of the @{text IF} is executed, and both statements do nothing:" { assume "\bval b s" hence "s = t" using `(?iw, s) \p \ t` by blast hence "(?w, s) \p \ t" using `\bval b s` by blast } moreover -- "on the other hand, if @{text b} is @{text True} in state @{text s}," -- {* then this time only the @{text IfTrue} rule can have be used *} { assume "bval b s" with `(?iw, s) \p \ t` have "(c;; ?w, s) \p \ t" by auto -- "and for this, only the Seq-rule is applicable:" then obtain s' where "(c, s) \p \ s'" and "(?w, s') \p \ t" by auto -- "with this information, we can build a derivation tree for the @{text WHILE}" with `bval b s` have "(?w, s) \p \ t" by (rule WhileTrue) } ultimately -- "both cases together again give us what we want:" have "(?w, s) \p \ t" by blast } ultimately show ?thesis by blast qed text {* Luckily, such lengthy proofs are seldom necessary. Isabelle can prove many such facts automatically. *} lemma while_unfold: "(WHILE b DO c) \ (IF b THEN c;; WHILE b DO c ELSE SKIP)" by blast lemma triv_if: "(IF b THEN c ELSE c) \ c" by blast lemma commute_if: "(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2) \ (IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))" by blast lemma sim_while_cong_aux: "(WHILE b DO c,s) \ p \ t \ c \ c' \ \q. (WHILE b DO c',s) \ q \ t" apply(induction "WHILE b DO c" s p t arbitrary: b c rule: big_step_t_induct) apply blast sorry lemma sim_while_cong: "c \ c' \ WHILE b DO c \ WHILE b DO c'" by (metis sim_whi le_cong_aux) text {* Command equivalence is an equivalence relation, i.e.\ it is reflexive, symmetric, and transitive. Because we used an abbreviation above, Isabelle derives this automatically. *} lemma sim_refl: "c \ c" by blast lemma sim_sym: "(c \ c') = (c' \ c)" by fast lemma sim_trans: "c \ c' \ c' \ c'' \ c \ c''" sorry *) subsection "Execution is deterministic" text {* This proof is automatic. *} theorem big_step_t_determ: "\ (c,s) \ p \ t; (c,s) \ q \ u \ \ u = t" apply (induction arbitrary: u q rule: big_step_t.induct) apply blast+ done thm Skip_tE While_tE[of _ _ s1] theorem big_step_t_determ2: "\ (c,s) \ p \ t; (c,s) \ q \ u \ \ (u = t \ p=q)" apply (induction arbitrary: u q rule: big_step_t_induct) apply(elim Skip_tE) apply(simp) apply(elim Assign_tE) apply(simp) apply blast apply(elim If_tE) apply(simp) apply blast apply(elim If_tE) apply blast apply(simp) apply(erule While_tE) apply(simp) apply blast proof (goal_cases) case 1 thm While_tE from 1(7) show ?case apply(safe) apply(erule While_tE) using 1(1-6) apply fast using 1(1-6) apply (simp) apply(erule While_tE) using 1(1-6) apply fast using 1(1-6) by (simp) qed text {* This is the proof as you might present it in a lecture. The remaining cases are simple enough to be proved automatically: *} theorem "(c,s) \ p \ t \ (c,s) \ p' \ t' \ t' = t" proof (induction arbitrary: t' p' rule: big_step_t.induct) -- "the only interesting case, @{text WhileTrue}:" fix b c s s1 t t' p p' p1 p2 -- "The assumptions of the rule:" assume "bval b s" and "(c,s) \ p1 \ s1" and "(WHILE b DO c,s1) \ p2 \ t" -- {* Ind.Hyp; note the @{text"\"} because of arbitrary: *} assume IHc: "\t' p'. (c,s) \ p' \ t' \ t' = s1" assume IHw: "\t' p'. (WHILE b DO c,s1) \ p' \ t' \ t' = t" -- "Premise of implication:" assume "(WHILE b DO c,s) \ p' \ t'" with `bval b s` obtain s1' p1' p2' where c: "(c,s) \ p1' \ s1'" and w: "(WHILE b DO c,s1') \ p2' \ t'" by auto from c IHc have "s1' = s1" by blast with w IHw show "t' = t" by blast qed blast+ -- "prove the rest automatically" end (*>*)