Theory Hoare_Sound_Complete

Up to index of Isabelle/HOL/HOL-IMP

theory Hoare_Sound_Complete
imports Hoare
`(* Author: Tobias Nipkow *)theory Hoare_Sound_Complete imports Hoare beginsubsection "Soundness"definitionhoare_valid :: "assn => com => assn => bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where"\<Turnstile> {P}c{Q} = (∀s t. (c,s) => t  -->  P s -->  Q t)"lemma hoare_sound: "\<turnstile> {P}c{Q}  ==>  \<Turnstile> {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(2) unfolding hoare_valid_def by blast    qed  }  thus ?case unfolding hoare_valid_def by blastqed (auto simp: hoare_valid_def)subsection "Weakest Precondition"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⇣1;c⇣2) Q = wp c⇣1 (wp c⇣2 Q)"by (rule ext) (auto simp: wp_def)lemma wp_If[simp]: "wp (IF b THEN c⇣1 ELSE c⇣2) Q = (λs. (bval b s --> wp c⇣1 Q s) ∧  (¬ bval b s --> wp c⇣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)subsection "Completeness"lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"proof(induction c arbitrary: Q)  case Seq thus ?case by(auto intro: Seq)next  case (If b c1 c2)  let ?If = "IF b THEN c1 ELSE c2"  show ?case  proof(rule hoare.If)    show "\<turnstile> {λs. wp ?If Q s ∧ bval b s} c1 {Q}"    proof(rule strengthen_pre[OF _ If(1)])      show "∀s. wp ?If Q s ∧ bval b s --> wp c1 Q s" by auto    qed    show "\<turnstile> {λs. wp ?If Q s ∧ ¬ bval b s} c2 {Q}"    proof(rule strengthen_pre[OF _ If(2)])      show "∀s. wp ?If Q s ∧ ¬ bval b s --> wp c2 Q s" by auto    qed  qednext  case (While b c)  let ?w = "WHILE b DO c"  have "\<turnstile> {wp ?w Q} ?w {λs. wp ?w Q s ∧ ¬ bval b s}"  proof(rule hoare.While)    show "\<turnstile> {λs. wp ?w Q s ∧ bval b s} c {wp ?w Q}"    proof(rule strengthen_pre[OF _ While(1)])      show "∀s. wp ?w Q s ∧ bval b s --> wp c (wp ?w Q) s" by auto    qed  qed  thus ?case  proof(rule weaken_post)    show "∀s. wp ?w Q s ∧ ¬ bval b s --> Q s" by auto  qedqed autolemma hoare_relative_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {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 "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)qedend`