Theory Hoare_Ex

section ‹Using Hoare Logic›

theory Hoare_Ex
  imports Hoare
begin

subsection ‹State spaces›

text ‹
  First of all we provide a store of program variables that occur in any of
  the programs considered later. Slightly unexpected things may happen when
  attempting to work with undeclared variables.
›

record vars =
  I :: nat
  M :: nat
  N :: nat
  S :: nat

text ‹
  While all of our variables happen to have the same type, nothing would
  prevent us from working with many-sorted programs as well, or even
  polymorphic ones. Also note that Isabelle/HOL's extensible record types even
  provides simple means to extend the state space later.
›


subsection ‹Basic examples›

text ‹
  We look at few trivialities involving assignment and sequential composition,
  in order to get an idea of how to work with our formulation of Hoare Logic.

  ┉
  Using the basic ‹assign› rule directly is a bit cumbersome.
›

lemma "⊢ ⦃´(N_update (λ_. (2 * ´N))) ∈ ⦃´N = 10⦄⦄ ´N := 2 * ´N ⦃´N = 10⦄"
  by (rule assign)

text ‹
  Certainly we want the state modification already done, e.g.\ by
  simplification. The ‹hoare› method performs the basic state update for us;
  we may apply the Simplifier afterwards to achieve ``obvious'' consequences
  as well.
›

lemma "⊢ ⦃True⦄ ´N := 10 ⦃´N = 10⦄"
  by hoare

lemma "⊢ ⦃2 * ´N = 10⦄ ´N := 2 * ´N ⦃´N = 10⦄"
  by hoare

lemma "⊢ ⦃´N = 5⦄ ´N := 2 * ´N ⦃´N = 10⦄"
  by hoare simp

lemma "⊢ ⦃´N + 1 = a + 1⦄ ´N := ´N + 1 ⦃´N = a + 1⦄"
  by hoare

lemma "⊢ ⦃´N = a⦄ ´N := ´N + 1 ⦃´N = a + 1⦄"
  by hoare simp

lemma "⊢ ⦃a = a ∧ b = b⦄ ´M := a; ´N := b ⦃´M = a ∧ ´N = b⦄"
  by hoare

lemma "⊢ ⦃True⦄ ´M := a; ´N := b ⦃´M = a ∧ ´N = b⦄"
  by hoare

lemma
  "⊢ ⦃´M = a ∧ ´N = b⦄
      ´I := ´M; ´M := ´N; ´N := ´I
      ⦃´M = b ∧ ´N = a⦄"
  by hoare simp

text ‹
  It is important to note that statements like the following one can only be
  proven for each individual program variable. Due to the extra-logical nature
  of record fields, we cannot formulate a theorem relating record selectors
  and updates schematically.
›

lemma "⊢ ⦃´N = a⦄ ´N := ´N ⦃´N = a⦄"
  by hoare

lemma "⊢ ⦃´x = a⦄ ´x := ´x ⦃´x = a⦄"
  oops

lemma
  "Valid {s. x s = a} (Basic (λs. x_update (x s) s)) {s. x s = n}"
  ― ‹same statement without concrete syntax›
  oops


text ‹
  In the following assignments we make use of the consequence rule in order to
  achieve the intended precondition. Certainly, the ‹hoare› method is able to
  handle this case, too.
›

lemma "⊢ ⦃´M = ´N⦄ ´M := ´M + 1 ⦃´M ≠ ´N⦄"
proof -
  have "⦃´M = ´N⦄ ⊆ ⦃´M + 1 ≠ ´N⦄"
    by auto
  also have "⊢ … ´M := ´M + 1 ⦃´M ≠ ´N⦄"
    by hoare
  finally show ?thesis .
qed

lemma "⊢ ⦃´M = ´N⦄ ´M := ´M + 1 ⦃´M ≠ ´N⦄"
proof -
  have "m = n ⟶ m + 1 ≠ n" for m n :: nat
      ― ‹inclusion of assertions expressed in ``pure'' logic,›
      ― ‹without mentioning the state space›
    by simp
  also have "⊢ ⦃´M + 1 ≠ ´N⦄ ´M := ´M + 1 ⦃´M ≠ ´N⦄"
    by hoare
  finally show ?thesis .
qed

lemma "⊢ ⦃´M = ´N⦄ ´M := ´M + 1 ⦃´M ≠ ´N⦄"
  by hoare simp


subsection ‹Multiplication by addition›

text ‹
  We now do some basic examples of actual ▩‹WHILE› programs. This one is a
  loop for calculating the product of two natural numbers, by iterated
  addition. We first give detailed structured proof based on single-step Hoare
  rules.
›

lemma
  "⊢ ⦃´M = 0 ∧ ´S = 0⦄
      WHILE ´M ≠ a
      DO ´S := ´S + b; ´M := ´M + 1 OD
      ⦃´S = a * b⦄"
proof -
  let "⊢ _ ?while _" = ?thesis
  let "⦃´?inv⦄" = "⦃´S = ´M * b⦄"

  have "⦃´M = 0 ∧ ´S = 0⦄ ⊆ ⦃´?inv⦄" by auto
  also have "⊢ … ?while ⦃´?inv ∧ ¬ (´M ≠ a)⦄"
  proof
    let ?c = "´S := ´S + b; ´M := ´M + 1"
    have "⦃´?inv ∧ ´M ≠ a⦄ ⊆ ⦃´S + b = (´M + 1) * b⦄"
      by auto
    also have "⊢ … ?c ⦃´?inv⦄" by hoare
    finally show "⊢ ⦃´?inv ∧ ´M ≠ a⦄ ?c ⦃´?inv⦄" .
  qed
  also have "… ⊆ ⦃´S = a * b⦄" by auto
  finally show ?thesis .
qed

text ‹
  The subsequent version of the proof applies the ‹hoare› method to reduce the
  Hoare statement to a purely logical problem that can be solved fully
  automatically. Note that we have to specify the ▩‹WHILE› loop invariant in
  the original statement.
›

lemma
  "⊢ ⦃´M = 0 ∧ ´S = 0⦄
      WHILE ´M ≠ a
      INV ⦃´S = ´M * b⦄
      DO ´S := ´S + b; ´M := ´M + 1 OD
      ⦃´S = a * b⦄"
  by hoare auto


subsection ‹Summing natural numbers›

text ‹
  We verify an imperative program to sum natural numbers up to a given limit.
  First some functional definition for proper specification of the problem.

  ┉
  The following proof is quite explicit in the individual steps taken, with
  the ‹hoare› method only applied locally to take care of assignment and
  sequential composition. Note that we express intermediate proof obligation
  in pure logic, without referring to the state space.
›

theorem
  "⊢ ⦃True⦄
      ´S := 0; ´I := 1;
      WHILE ´I ≠ n
      DO
        ´S := ´S + ´I;
        ´I := ´I + 1
      OD
      ⦃´S = (∑j<n. j)⦄"
  (is "⊢ _ (_; ?while) _")
proof -
  let ?sum = "λk::nat. ∑j<k. j"
  let ?inv = "λs i::nat. s = ?sum i"

  have "⊢ ⦃True⦄ ´S := 0; ´I := 1 ⦃?inv ´S ´I⦄"
  proof -
    have "True ⟶ 0 = ?sum 1"
      by simp
    also have "⊢ ⦃…⦄ ´S := 0; ´I := 1 ⦃?inv ´S ´I⦄"
      by hoare
    finally show ?thesis .
  qed
  also have "⊢ … ?while ⦃?inv ´S ´I ∧ ¬ ´I ≠ n⦄"
  proof
    let ?body = "´S := ´S + ´I; ´I := ´I + 1"
    have "?inv s i ∧ i ≠ n ⟶ ?inv (s + i) (i + 1)" for s i
      by simp
    also have "⊢ ⦃´S + ´I = ?sum (´I + 1)⦄ ?body ⦃?inv ´S ´I⦄"
      by hoare
    finally show "⊢ ⦃?inv ´S ´I ∧ ´I ≠ n⦄ ?body ⦃?inv ´S ´I⦄" .
  qed
  also have "s = ?sum i ∧ ¬ i ≠ n ⟶ s = ?sum n" for s i
    by simp
  finally show ?thesis .
qed

text ‹
  The next version uses the ‹hoare› method, while still explaining the
  resulting proof obligations in an abstract, structured manner.
›

theorem
  "⊢ ⦃True⦄
      ´S := 0; ´I := 1;
      WHILE ´I ≠ n
      INV ⦃´S = (∑j<´I. j)⦄
      DO
        ´S := ´S + ´I;
        ´I := ´I + 1
      OD
      ⦃´S = (∑j<n. j)⦄"
proof -
  let ?sum = "λk::nat. ∑j<k. j"
  let ?inv = "λs i::nat. s = ?sum i"
  show ?thesis
  proof hoare
    show "?inv 0 1" by simp
    show "?inv (s + i) (i + 1)" if "?inv s i ∧ i ≠ n" for s i
      using that by simp
    show "s = ?sum n" if "?inv s i ∧ ¬ i ≠ n" for s i
      using that by simp
  qed
qed

text ‹
  Certainly, this proof may be done fully automatic as well, provided that the
  invariant is given beforehand.
›

theorem
  "⊢ ⦃True⦄
      ´S := 0; ´I := 1;
      WHILE ´I ≠ n
      INV ⦃´S = (∑j<´I. j)⦄
      DO
        ´S := ´S + ´I;
        ´I := ´I + 1
      OD
      ⦃´S = (∑j<n. j)⦄"
  by hoare auto


subsection ‹Time›

text ‹
  A simple embedding of time in Hoare logic: function ‹timeit› inserts an
  extra variable to keep track of the elapsed time.
›

record tstate = time :: nat

type_synonym 'a time = "⦇time :: nat, … :: 'a⦈"

primrec timeit :: "'a time com ⇒ 'a time com"
  where
    "timeit (Basic f) = (Basic f; Basic(λs. s⦇time := Suc (time s)⦈))"
  | "timeit (c1; c2) = (timeit c1; timeit c2)"
  | "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
  | "timeit (While b iv v c) = While b iv v (timeit c)"

record tvars = tstate +
  I :: nat
  J :: nat

lemma lem: "(0::nat) < n ⟹ n + n ≤ Suc (n * n)"
  by (induct n) simp_all

lemma
  "⊢ ⦃i = ´I ∧ ´time = 0⦄
    (timeit
      (WHILE ´I ≠ 0
        INV ⦃2 *´ time + ´I * ´I + 5 * ´I = i * i + 5 * i⦄
        DO
          ´J := ´I;
          WHILE ´J ≠ 0
          INV ⦃0 < ´I ∧ 2 * ´time + ´I * ´I + 3 * ´I + 2 * ´J - 2 = i * i + 5 * i⦄
          DO ´J := ´J - 1 OD;
          ´I := ´I - 1
        OD))
    ⦃2 * ´time = i * i + 5 * i⦄"
  apply simp
  apply hoare
      apply simp
     apply clarsimp
    apply clarsimp
   apply arith
   prefer 2
   apply clarsimp
  apply (clarsimp simp: nat_distrib)
  apply (frule lem)
  apply arith
  done

end