# Theory HoareT

Up to index of Isabelle/HOL/HOL-IMP

theory HoareT
imports Hoare_Sound_Complete
(* Author: Tobias Nipkow *)theory HoareT imports Hoare_Sound_Complete beginsubsection "Hoare Logic for Total Correctness"text{* Note that this definition of total validity @{text"\<Turnstile>⇩t"} onlyworks if execution is deterministic (which it is in our case). *}definition hoare_tvalid :: "assn => com => assn => bool"  ("\<Turnstile>⇩t {(1_)}/ (_)/ {(1_)}" 50) where"\<Turnstile>⇩t {P}c{Q}  ≡  ∀s. P s --> (∃t. (c,s) => t ∧ Q t)"text{* Provability of Hoare triples in the proof system for totalcorrectness is written @{text"\<turnstile>⇩t {P}c{Q}"} and definedinductively. The rules for @{text"\<turnstile>⇩t"} differ from those for@{text"\<turnstile>"} only in the one place where nontermination can arise: the@{term While}-rule. *}inductive  hoaret :: "assn => com => assn => bool" ("\<turnstile>⇩t ({(1_)}/ (_)/ {(1_)})" 50)whereSkip:  "\<turnstile>⇩t {P} SKIP {P}" |Assign:  "\<turnstile>⇩t {λs. P(s[a/x])} x::=a {P}" |Seq: "[| \<turnstile>⇩t {P⇣1} c⇣1 {P⇣2}; \<turnstile>⇩t {P⇣2} c⇣2 {P⇣3} |] ==> \<turnstile>⇩t {P⇣1} c⇣1;c⇣2 {P⇣3}" |If: "[| \<turnstile>⇩t {λs. P s ∧ bval b s} c⇣1 {Q}; \<turnstile>⇩t {λs. P s ∧ ¬ bval b s} c⇣2 {Q} |]  ==> \<turnstile>⇩t {P} IF b THEN c⇣1 ELSE c⇣2 {Q}" |While:  "[| !!n::nat. \<turnstile>⇩t {λs. P s ∧ bval b s ∧ f s = n} c {λs. P s ∧ f s < n}|]   ==> \<turnstile>⇩t {P} WHILE b DO c {λs. P s ∧ ¬bval b s}" |conseq: "[| ∀s. P' s --> P s; \<turnstile>⇩t {P}c{Q}; ∀s. Q s --> Q' s  |] ==>           \<turnstile>⇩t {P'}c{Q'}"text{* The @{term While}-rule is like the one for partial correctness but itrequires additionally that with every execution of the loop body some measurefunction @{term[source]"f :: state => nat"} decreases. *}lemma strengthen_pre:  "[| ∀s. P' s --> P s;  \<turnstile>⇩t {P} c {Q} |] ==> \<turnstile>⇩t {P'} c {Q}"by (metis conseq)lemma weaken_post:  "[| \<turnstile>⇩t {P} c {Q};  ∀s. Q s --> Q' s |] ==>  \<turnstile>⇩t {P} c {Q'}"by (metis conseq)lemma Assign': "∀s. P s --> Q(s[a/x]) ==> \<turnstile>⇩t {P} x ::= a {Q}"by (simp add: strengthen_pre[OF _ Assign])lemma While':assumes "!!n::nat. \<turnstile>⇩t {λs. P s ∧ bval b s ∧ f s = n} c {λs. P s ∧ f s < n}"    and "∀s. P s ∧ ¬ bval b s --> Q s"shows "\<turnstile>⇩t {P} WHILE b DO c {Q}"by(blast intro: assms(1) weaken_post[OF While assms(2)])text{* Our standard example: *}abbreviation "w n ==  WHILE Less (V ''y'') (N n)  DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"lemma "\<turnstile>⇩t {λs. 0 ≤ n} ''x'' ::= N 0; ''y'' ::= N 0; w n {λs. s ''x'' = ∑{1..n}}"apply(rule Seq)prefer 2apply(rule While'  [where P = "λs. s ''x'' = ∑ {1..s ''y''} ∧ 0 ≤ s ''y'' ∧ s ''y'' ≤ n"   and f = "λs. nat (n - s ''y'')"])apply(rule Seq)prefer 2apply(rule Assign)apply(rule Assign')apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)apply clarsimpapply fastforceapply(rule Seq)prefer 2apply(rule Assign)apply(rule Assign')apply simpdonetext{* The soundness theorem: *}theorem hoaret_sound: "\<turnstile>⇩t {P}c{Q}  ==>  \<Turnstile>⇩t {P}c{Q}"proof(unfold hoare_tvalid_def, induct rule: hoaret.induct)  case (While P b f c)  show ?case  proof    fix s    show "P s --> (∃t. (WHILE b DO c, s) => t ∧ P t ∧ ¬ bval b t)"    proof(induction "f s" arbitrary: s rule: less_induct)      case (less n)      thus ?case by (metis While(2) WhileFalse WhileTrue)    qed  qednext  case If thus ?case by auto blastqed fastforce+text{*The completeness proof proceeds along the same lines as the one for partialcorrectness. First we have to strengthen our notion of weakest preconditionto take termination into account: *}definition wpt :: "com => assn => assn" ("wp⇩t") where"wp⇩t c Q  ≡  λs. ∃t. (c,s) => t ∧ Q t"lemma [simp]: "wp⇩t SKIP Q = Q"by(auto intro!: ext simp: wpt_def)lemma [simp]: "wp⇩t (x ::= e) Q = (λs. Q(s(x := aval e s)))"by(auto intro!: ext simp: wpt_def)lemma [simp]: "wp⇩t (c⇣1;c⇣2) Q = wp⇩t c⇣1 (wp⇩t c⇣2 Q)"unfolding wpt_defapply(rule ext)apply autodonelemma [simp]: "wp⇩t (IF b THEN c⇣1 ELSE c⇣2) Q = (λs. wp⇩t (if bval b s then c⇣1 else c⇣2) Q s)"apply(unfold wpt_def)apply(rule ext)apply autodonetext{* Now we define the number of iterations @{term "WHILE b DO c"} needs toterminate when started in state @{text s}. Because this is a truly partialfunction, we define it as an (inductive) relation first: *}inductive Its :: "bexp => com => state => nat => bool" whereIts_0: "¬ bval b s ==> Its b c s 0" |Its_Suc: "[| bval b s;  (c,s) => s';  Its b c s' n |] ==> Its b c s (Suc n)"text{* The relation is in fact a function: *}lemma Its_fun: "Its b c s n ==> Its b c s n' ==> n=n'"proof(induction arbitrary: n' rule:Its.induct)(* new release:  case Its_0 thus ?case by(metis Its.cases)next  case Its_Suc thus ?case by(metis Its.cases big_step_determ)qed*)  case Its_0  from this(1) Its.cases[OF this(2)] show ?case by metisnext  case (Its_Suc b s c s' n n')  note C = this  from this(5) show ?case  proof cases    case Its_0 with Its_Suc(1) show ?thesis by blast  next    case Its_Suc with C show ?thesis by(metis big_step_determ)  qedqedtext{* For all terminating loops, @{const Its} yields a result: *}lemma WHILE_Its: "(WHILE b DO c,s) => t ==> ∃n. Its b c s n"proof(induction "WHILE b DO c" s t rule: big_step_induct)  case WhileFalse thus ?case by (metis Its_0)next  case WhileTrue thus ?case by (metis Its_Suc)qedtext{* Now the relation is turned into a function with the help ofthe description operator @{text THE}: *}definition its :: "bexp => com => state => nat" where"its b c s = (THE n. Its b c s n)"text{* The key property: every loop iteration increases @{const its} by 1. *}lemma its_Suc: "[| bval b s; (c, s) => s'; (WHILE b DO c, s') => t|]       ==> its b c s = Suc(its b c s')"by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality)lemma wpt_is_pre: "\<turnstile>⇩t {wp⇩t c Q} c {Q}"proof (induction c arbitrary: Q)  case SKIP show ?case by simp (blast intro:hoaret.Skip)next  case Assign show ?case by simp (blast intro:hoaret.Assign)next  case Seq thus ?case by simp (blast intro:hoaret.Seq)next  case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq)next  case (While b c)  let ?w = "WHILE b DO c"  { fix n    have "∀s. wp⇩t ?w Q s ∧ bval b s ∧ its b c s = n -->              wp⇩t c (λs'. wp⇩t ?w Q s' ∧ its b c s' < n) s"      unfolding wpt_def by (metis WhileE its_Suc lessI)    note strengthen_pre[OF this While]  } note hoaret.While[OF this]  moreover have "∀s. wp⇩t ?w Q s ∧ ¬ bval b s --> Q s" by (auto simp add:wpt_def)  ultimately show ?case by(rule weaken_post)qedtext{*\noindent In the @{term While}-case, @{const its} provides the obvioustermination argument.The actual completeness theorem follows directly, in the same manneras for partial correctness: *}theorem hoaret_complete: "\<Turnstile>⇩t {P}c{Q} ==> \<turnstile>⇩t {P}c{Q}"apply(rule strengthen_pre[OF _ wpt_is_pre])apply(auto simp: hoare_tvalid_def hoare_valid_def wpt_def)doneend