Quelle  Hoare_Ex.thy

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