# Theory Examples

Up to index of Isabelle/HOL/Hoare

theory Examples
imports Hoare Arith2
begin

    (*  Title:      HOL/Hoare/Examples.thy
        ID:         $Id: Examples.thy,v 1.14 2005/07/13 13:06:22 paulson Exp $
        Author:     Norbert Galm
        Copyright   1998 TUM

    Various examples.
    *)

    theory Examples imports Hoare Arith2 begin

    (*** ARITHMETIC ***)

    (** multiplication by successive addition **)

    lemma multiply_by_add: "VARS m s a b
      {a=A & b=B}
      m := 0; s := 0;
      WHILE m~=a
      INV {s=m*b & a=A & b=B}
      DO s := s+b; m := m+(1::nat) OD
      {s = A*B}"
    by vcg_simp

    lemma "VARS M N P :: int
     {m=M & n=N}
     IF M < 0 THEN M := -M; N := -N ELSE SKIP FI;
     P := 0;
     WHILE 0 < M
     INV {0 <= M & (EX p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N)}
     DO P := P+N; M := M - 1 OD
     {P = m*n}"
    apply vcg_simp
     apply (simp add:int_distrib)
    apply clarsimp
    apply(rule conjI)
     apply clarsimp
    apply clarsimp
    done

    (** Euclid's algorithm for GCD **)

    lemma Euclid_GCD: "VARS a b
     {0<A & 0<B}
     a := A; b := B;
     WHILE  a ≠ b
     INV {0<a & 0<b & gcd A B = gcd a b}
     DO IF a<b THEN b := b-a ELSE a := a-b FI OD
     {a = gcd A B}"
    apply vcg
    (*Now prove the verification conditions*)
      apply auto
      apply(simp add: gcd_diff_r less_imp_le)
     apply(simp add: linorder_not_less gcd_diff_l)
    apply(erule gcd_nnn)
    done

    (** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
    (* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
       where it is given without the invariant. Instead of defining scm
       explicitly we have used the theorem scm x y = x*y/gcd x y and avoided
       division by mupltiplying with gcd x y.
    *)

    lemmas distribs =
      diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2

    lemma gcd_scm: "VARS a b x y
     {0<A & 0<B & a=A & b=B & x=B & y=A}
     WHILE  a ~= b
     INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
     DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD
     {a = gcd A B & 2*A*B = a*(x+y)}"
    apply vcg
      apply simp
     apply(simp add: distribs gcd_diff_r linorder_not_less gcd_diff_l)
    apply(simp add: distribs gcd_nnn)
    done

    (** Power by iterated squaring and multiplication **)

    lemma power_by_mult: "VARS a b c
     {a=A & b=B}
     c := (1::nat);
     WHILE b ~= 0
     INV {A^B = c * a^b}
     DO  WHILE b mod 2 = 0
         INV {A^B = c * a^b}
         DO  a := a*a; b := b div 2 OD;
         c := c*a; b := b - 1
     OD
     {c = A^B}"
    apply vcg_simp
    apply(case_tac "b")
     apply(simp add: mod_less)
    apply simp
    done

    (** Factorial **)

    lemma factorial: "VARS a b
     {a=A}
     b := 1;
     WHILE a ~= 0
     INV {fac A = b * fac a}
     DO b := b*a; a := a - 1 OD
     {b = fac A}"
    apply vcg_simp
    apply(clarsimp split: nat_diff_split)
    done

    lemma [simp]: "1 ≤ i ==> fac (i - Suc 0) * i = fac i"
    by(induct i, simp_all)

    lemma "VARS i f
     {True}
     i := (1::nat); f := 1;
     WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
     DO f := f*i; i := i+1 OD
     {f = fac n}"
    apply vcg_simp
    apply(subgoal_tac "i = Suc n")
    apply simp
    apply arith
    done

    (** Square root **)

    (* the easy way: *)

    lemma sqrt: "VARS r x
     {True}
     x := X; r := (0::nat);
     WHILE (r+1)*(r+1) <= x
     INV {r*r <= x & x=X}
     DO r := r+1 OD
     {r*r <= X & X < (r+1)*(r+1)}"
    apply vcg_simp
    done

    (* without multiplication *)

    lemma sqrt_without_multiplication: "VARS u w r x
     {True}
     x := X; u := 1; w := 1; r := (0::nat);
     WHILE w <= x
     INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X}
     DO r := r + 1; w := w + u + 2; u := u + 2 OD
     {r*r <= X & X < (r+1)*(r+1)}"
    apply vcg_simp
    done

    (*** LISTS ***)

    lemma imperative_reverse: "VARS y x
     {x=X}
     y:=[];
     WHILE x ~= []
     INV {rev(x)@y = rev(X)}
     DO y := (hd x # y); x := tl x OD
     {y=rev(X)}"
    apply vcg_simp
     apply(simp add: neq_Nil_conv)
     apply auto
    done

    lemma imperative_append: "VARS x y
     {x=X & y=Y}
     x := rev(x);
     WHILE x~=[]
     INV {rev(x)@y = X@Y}
     DO y := (hd x # y);
        x := tl x
     OD
     {y = X@Y}"
    apply vcg_simp
    apply(simp add: neq_Nil_conv)
    apply auto
    done

    (*** ARRAYS ***)

    (* Search for a key *)
    lemma zero_search: "VARS A i
     {True}
     i := 0;
     WHILE i < length A & A!i ~= key
     INV {!j. j<i --> A!j ~= key}
     DO i := i+1 OD
     {(i < length A --> A!i = key) &
      (i = length A --> (!j. j < length A --> A!j ~= key))}"
    apply vcg_simp
    apply(blast elim!: less_SucE)
    done

    (*
    The `partition' procedure for quicksort.
    `A' is the array to be sorted (modelled as a list).
    Elements of A must be of class order to infer at the end
    that the elements between u and l are equal to pivot.

    Ambiguity warnings of parser are due to := being used
    both for assignment and list update.
    *)
    lemma lem: "m - Suc 0 < n ==> m < Suc n"
    by arith

    lemma Partition:
    "[| leq == %A i. !k. k<i --> A!k <= pivot;
        geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
     VARS A u l
     {0 < length(A::('a::order)list)}
     l := 0; u := length A - Suc 0;
     WHILE l <= u
      INV {leq A l & geq A u & u<length A & l<=length A}
      DO WHILE l < length A & A!l <= pivot
         INV {leq A l & geq A u & u<length A & l<=length A}
         DO l := l+1 OD;
         WHILE 0 < u & pivot <= A!u
         INV {leq A l & geq A u  & u<length A & l<=length A}
         DO u := u - 1 OD;
         IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
      OD
     {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
    (* expand and delete abbreviations first *)
    apply (simp);
    apply (erule thin_rl)+
    apply vcg_simp
       apply (force simp: neq_Nil_conv)
      apply (blast elim!: less_SucE intro: Suc_leI)
     apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
    apply (force simp: nth_list_update)
    done

    end

lemma multiply_by_add:

      {a = A ∧ b = B}
       m := 0;
       s := 0;
       WHILE m ≠ a INV {s = m * b ∧ a = A ∧ b = B}
        DO s := s + b; m := m + 1 OD
       {s = A * B}

lemma

      {m = M ∧ n = N}
       IF M < 0 THEN M := - M; N := - N  ELSE SKIP FI;
       P := 0;
       WHILE 0 < M
        INV {0 ≤ M ∧
             (∃p. p = (if m < 0 then - m else m) ∧ p * N = m * n ∧ P = (p - M) * N)}
        DO P := P + N; M := M - 1 OD
       {P = m * n}

lemma Euclid_GCD:

      {0 < A ∧ 0 < B}
       a := A;
       b := B;
       WHILE a ≠ b INV {0 < a ∧ 0 < b ∧ Arith2.gcd A B = Arith2.gcd a b}
        DO IF a < b THEN b := b - a  ELSE a := a - b FI OD
       {a = Arith2.gcd A B}

lemmas distribs:

      (m - n) * k = m * k - n * k

      k * (m - n) = k * m - k * n

      (m + n) * k = m * k + n * k

      k * (m + n) = k * m + k * n

lemmas distribs:

      (m - n) * k = m * k - n * k

      k * (m - n) = k * m - k * n

      (m + n) * k = m * k + n * k

      k * (m + n) = k * m + k * n

lemma gcd_scm:

      {0 < A ∧ 0 < B ∧ a = A ∧ b = B ∧ x = B ∧ y = A}
       WHILE a ≠ b
        INV {0 < a ∧
             0 < b ∧ Arith2.gcd A B = Arith2.gcd a b ∧ 2 * A * B = a * x + b * y}
        DO IF a < b THEN b := b - a; x := x + y  ELSE a := a - b; y := y + x FI OD
       {a = Arith2.gcd A B ∧ 2 * A * B = a * (x + y)}

lemma power_by_mult:

      {a = A ∧ b = B}
       c := 1;
       WHILE b ≠ 0 INV {A ^ B = c * a ^ b}
        DO WHILE b mod 2 = 0 INV {A ^ B = c * a ^ b}
            DO a := a * a; b := b div 2 OD;
           c := c * a; b := b - 1
        OD
       {c = A ^ B}

lemma factorial:

      {a = A}
       b := 1; WHILE a ≠ 0 INV {fac A = b * fac a}
                DO b := b * a; a := a - 1 OD
       {b = fac A}

lemma

      1 ≤ i ==> fac (i - Suc 0) * i = fac i

lemma

      {True}
       i := 1;
       f := 1;
       WHILE i ≤ n INV {f = fac (i - 1) ∧ 1 ≤ i ∧ i ≤ n + 1}
        DO f := f * i; i := i + 1 OD
       {f = fac n}

lemma sqrt:

      {True}
       x := X;
       r := 0; WHILE (r + 1) * (r + 1) ≤ x INV {r * r ≤ x ∧ x = X}
                DO r := r + 1 OD
       {r * r ≤ X ∧ X < (r + 1) * (r + 1)}

lemma sqrt_without_multiplication:

      {True}
       x := X;
       u := 1;
       w := 1;
       r := 0;
       WHILE w ≤ x INV {u = r + r + 1 ∧ w = (r + 1) * (r + 1) ∧ r * r ≤ x ∧ x = X}
        DO r := r + 1; w := w + u + 2; u := u + 2 OD
       {r * r ≤ X ∧ X < (r + 1) * (r + 1)}

lemma imperative_reverse:

      {x = X}
       y := []; WHILE x ≠ [] INV {rev x @ y = rev X}
                 DO y := hd x # y; x := tl x OD
       {y = rev X}

lemma imperative_append:

      {x = X ∧ y = Y}
       x := rev x;
       WHILE x ≠ [] INV {rev x @ y = X @ Y}
        DO y := hd x # y; x := tl x OD
       {y = X @ Y}

lemma zero_search:

      {True}
       i := 0;
       WHILE i < length A ∧ A ! i ≠ key INV {∀j<i. A ! j ≠ key}
        DO i := i + 1 OD
       {(i < length A --> A ! i = key) ∧
        (i = length A --> (∀j<length A. A ! j ≠ key))}

lemma lem:

      m - Suc 0 < n ==> m < Suc n

lemma Partition:

      [| leq == %A i. ∀k<i. A ! k ≤ pivot;
         geq == %A i. ∀k. i < k ∧ k < length A --> pivot ≤ A ! k |]
      ==> {0 < length A}
           l := 0;
           u := length A - Suc 0;
           WHILE l ≤ u INV {leq A l ∧ geq A u ∧ u < length A ∧ l ≤ length A}
            DO WHILE l < length A ∧ A ! l ≤ pivot
                INV {leq A l ∧ geq A u ∧ u < length A ∧ l ≤ length A}
                DO l := l + 1 OD;
               WHILE 0 < u ∧ pivot ≤ A ! u
                INV {leq A l ∧ geq A u ∧ u < length A ∧ l ≤ length A}
                DO u := u - 1 OD;
               IF l ≤ u THEN A := A[l := A ! u, u := A ! l]  ELSE SKIP FI
            OD
           {leq A u ∧ (∀k. u < k ∧ k < l --> A ! k = pivot) ∧ geq A l}