theory Solution11_2 imports "HOL-IMP.BExp" begin 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) | Or com com ("_ OR/ _" [60, 61] 60) 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" | OrLeft: "\ (c\<^sub>1,s\<^sub>1) \ s\<^sub>2\ \ (c\<^sub>1 OR c\<^sub>2, s\<^sub>1) \ s\<^sub>2" | OrRight: "\ (c\<^sub>2,s\<^sub>1) \ s\<^sub>2\ \ (c\<^sub>1 OR c\<^sub>2, s\<^sub>1) \ s\<^sub>2" code_pred big_step . declare big_step.intros [intro] lemmas big_step_induct = big_step.induct[split_format(complete)] 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" inductive_cases OrE[elim]: "(c1 OR c2, s) \ t" abbreviation equiv_c :: "com \ com \ bool" (infix "\" 50) where "c \ c' \ (\s t. (c,s) \ t = (c',s) \ t)" 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 assume "(?w, s) \ 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) \ t` by blast hence "(?iw, s) \ 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) \ t` obtain s' where "(c, s) \ s'" and "(?w, s') \ 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) \ t" by (rule Seq) -- "then the whole @{text IF}" with `bval b s` have "(?iw, s) \ t" by (rule IfTrue) } ultimately -- "both cases together give us what we want:" have "(?iw, s) \ t" by blast } moreover -- "now the other direction:" { fix s t assume "(?iw, s) \ 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) \ t` by blast hence "(?w, s) \ 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) \ t` have "(c;; ?w, s) \ t" by auto -- "and for this, only the Seq-rule is applicable:" then obtain s' where "(c, s) \ s'" and "(?w, s') \ t" by auto -- "with this information, we can build a derivation tree for the @{text WHILE}" with `bval b s` have "(?w, s) \ t" by (rule WhileTrue) } ultimately -- "both cases together again give us what we want:" have "(?w, s) \ t" by blast } ultimately show ?thesis by blast qed type_synonym assn = "state \ bool" definition hoare_valid :: "assn \ com \ assn \ bool" ("\ {(1_)}/ (_)/ {(1_)}" 50) where "\ {P}c{Q} = (\s t. P s \ (c,s) \ t \ Q t)" abbreviation state_subst :: "state \ aexp \ vname \ state" ("_[_'/_]" [1000,0,0] 999) where "s[a/x] == s(x := aval a s)" inductive hoare :: "assn \ com \ assn \ bool" ("\ ({(1_)}/ (_)/ {(1_)})" 50) where Skip: "\ {P} SKIP {P}" | Assign: "\ {\s. P(s[a/x])} x::=a {P}" | Seq: "\ \ {P} c\<^sub>1 {Q}; \ {Q} c\<^sub>2 {R} \ \ \ {P} c\<^sub>1;;c\<^sub>2 {R}" | If: "\ \ {\s. P s \ bval b s} c\<^sub>1 {Q}; \ {\s. P s \ \ bval b s} c\<^sub>2 {Q} \ \ \ {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" | While: "\ {\s. P s \ bval b s} c {P} \ \ {P} WHILE b DO c {\s. P s \ \ bval b s}" | conseq: "\ \s. P' s \ P s; \ {P} c {Q}; \s. Q s \ Q' s \ \ \ {P'} c {Q'}" | Or: "\ \ {P} c\<^sub>1 {R}; \ {Q} c\<^sub>2 {R} \ \ \ {\ s. P s \ Q s} c\<^sub>1 OR c\<^sub>2 {R}" lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If lemma strengthen_pre: "\ \s. P' s \ P s; \ {P} c {Q} \ \ \ {P'} c {Q}" by (blast intro: conseq) lemma weaken_post: "\ \ {P} c {Q}; \s. Q s \ Q' s \ \ \ {P} c {Q'}" by (blast intro: conseq) lemma Assign': "\s. P s \ Q(s[a/x]) \ \ {P} x ::= a {Q}" by (simp add: strengthen_pre[OF _ Assign]) lemma While': assumes "\ {\s. P s \ bval b s} c {P}" and "\s. P s \ \ bval b s \ Q s" shows "\ {P} WHILE b DO c {Q}" by(rule weaken_post[OF While[OF assms(1)] assms(2)]) lemma hoare_sound: "\ {P}c{Q} \ \ {P}c{Q}" proof(induction rule: hoare.induct) case (While P b c) { fix s t have "(WHILE b DO c,s) \ t \ P s \ P t \ \ bval b t" proof(induction "WHILE b DO c" s t rule: big_step_induct) case WhileFalse thus ?case by blast next case WhileTrue thus ?case using While.IH unfolding hoare_valid_def by blast qed } thus ?case unfolding hoare_valid_def by blast qed (auto simp: hoare_valid_def) definition wp :: "com \ assn \ assn" where "wp c Q = (\s. \t. (c,s) \ t \ Q t)" lemma wp_SKIP[simp]: "wp SKIP Q = Q" by (rule ext) (auto simp: wp_def) lemma wp_Ass[simp]: "wp (x::=a) Q = (\s. Q(s[a/x]))" by (rule ext) (auto simp: wp_def) lemma wp_Seq[simp]: "wp (c\<^sub>1;;c\<^sub>2) Q = wp c\<^sub>1 (wp c\<^sub>2 Q)" by (rule ext) (auto simp: wp_def) lemma wp_If[simp]: "wp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\s. if bval b s then wp c\<^sub>1 Q s else wp c\<^sub>2 Q s)" by (rule ext) (auto simp: wp_def) lemma wp_While_If: "wp (WHILE b DO c) Q s = wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s" unfolding wp_def by (metis unfold_while) lemma wp_While_True[simp]: "bval b s \ wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s" by(simp add: wp_While_If) lemma wp_While_False[simp]: "\ bval b s \ wp (WHILE b DO c) Q s = Q s" by(simp add: wp_While_If) lemma wp_Or[simp]: "wp (c\<^sub>1 OR c\<^sub>2) Q = (\ s. wp c\<^sub>1 Q s \ wp c\<^sub>2 Q s)" by (rule ext) (auto simp: wp_def) lemma wp_is_pre: "\ {wp c Q} c {Q}" proof(induction c arbitrary: Q) case If thus ?case by(auto intro: conseq) next case (While b c) let ?w = "WHILE b DO c" show "\ {wp ?w Q} ?w {Q}" proof(rule While') show "\ {\s. wp ?w Q s \ bval b s} c {wp ?w Q}" proof(rule strengthen_pre[OF _ While.IH]) show "\s. wp ?w Q s \ bval b s \ wp c (wp ?w Q) s" by auto qed show "\s. wp ?w Q s \ \ bval b s \ Q s" by auto qed qed (auto intro: hoare.Or) lemma hoare_complete: assumes "\ {P}c{Q}" shows "\ {P}c{Q}" proof(rule strengthen_pre) show "\s. P s \ wp c Q s" using assms by (auto simp: hoare_valid_def wp_def) show "\ {wp c Q} c {Q}" by(rule wp_is_pre) qed corollary hoare_sound_complete: "\ {P}c{Q} \ \ {P}c{Q}" by (metis hoare_complete hoare_sound) end