src/HOL/Hoare/Examples.thy
author nipkow
Mon Oct 28 17:56:00 2002 +0100 (2002-10-28)
changeset 13684 48bfc2cc0938
parent 13682 91674c8a008b
child 13737 e564c3d2d174
permissions -rw-r--r--
moved fac example
     1 (*  Title:      HOL/Hoare/Examples.thy
     2     ID:         $Id$
     3     Author:     Norbert Galm
     4     Copyright   1998 TUM
     5 
     6 Various examples.
     7 *)
     8 
     9 theory Examples = Hoare + Arith2:
    10 
    11 (*** ARITHMETIC ***)
    12 
    13 (** multiplication by successive addition **)
    14 
    15 lemma multiply_by_add: "|- VARS m s a b.
    16   {a=A & b=B}
    17   m := 0; s := 0;
    18   WHILE m~=a
    19   INV {s=m*b & a=A & b=B}
    20   DO s := s+b; m := m+(1::nat) OD
    21   {s = A*B}"
    22 by vcg_simp
    23 
    24 
    25 (** Euclid's algorithm for GCD **)
    26 
    27 lemma Euclid_GCD: "|- VARS a b.
    28  {0<A & 0<B}
    29  a := A; b := B;
    30  WHILE  a~=b
    31  INV {0<a & 0<b & gcd A B = gcd a b}
    32  DO IF a<b THEN b := b-a ELSE a := a-b FI OD
    33  {a = gcd A B}"
    34 apply vcg
    35 (*Now prove the verification conditions*)
    36   apply auto
    37   apply(simp add: gcd_diff_r less_imp_le)
    38  apply(simp add: not_less_iff_le gcd_diff_l)
    39 apply(erule gcd_nnn)
    40 done
    41 
    42 (** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
    43 (* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
    44    where it is given without the invariant. Instead of defining scm
    45    explicitly we have used the theorem scm x y = x*y/gcd x y and avoided
    46    division by mupltiplying with gcd x y.
    47 *)
    48 
    49 lemmas distribs =
    50   diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2
    51 
    52 lemma gcd_scm: "|- VARS a b x y.
    53  {0<A & 0<B & a=A & b=B & x=B & y=A}
    54  WHILE  a ~= b
    55  INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
    56  DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD
    57  {a = gcd A B & 2*A*B = a*(x+y)}"
    58 apply vcg
    59   apply simp
    60  apply(simp add: distribs gcd_diff_r not_less_iff_le gcd_diff_l)
    61  apply arith
    62 apply(simp add: distribs gcd_nnn)
    63 done
    64 
    65 (** Power by iterated squaring and multiplication **)
    66 
    67 lemma power_by_mult: "|- VARS a b c.
    68  {a=A & b=B}
    69  c := (1::nat);
    70  WHILE b ~= 0
    71  INV {A^B = c * a^b}
    72  DO  WHILE b mod 2 = 0
    73      INV {A^B = c * a^b}
    74      DO  a := a*a; b := b div 2 OD;
    75      c := c*a; b := b - 1
    76  OD
    77  {c = A^B}"
    78 apply vcg_simp
    79 apply(case_tac "b")
    80  apply(simp add: mod_less)
    81 apply simp
    82 done
    83 
    84 (** Factorial **)
    85 
    86 lemma factorial: "|- VARS a b.
    87  {a=A}
    88  b := 1;
    89  WHILE a ~= 0
    90  INV {fac A = b * fac a}
    91  DO b := b*a; a := a - 1 OD
    92  {b = fac A}"
    93 apply vcg_simp
    94 apply(clarsimp split: nat_diff_split)
    95 done
    96 
    97 lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
    98 by(induct i, simp_all)
    99 
   100 lemma "|- VARS i f.
   101  {True}
   102  i := (1::nat); f := 1;
   103  WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
   104  DO f := f*i; i := i+1 OD
   105  {f = fac n}"
   106 apply vcg_simp
   107 apply(subgoal_tac "i = Suc n")
   108 apply simp
   109 apply arith
   110 done
   111 
   112 (** Square root **)
   113 
   114 (* the easy way: *)
   115 
   116 lemma sqrt: "|- VARS r x.
   117  {True}
   118  x := X; r := (0::nat);
   119  WHILE (r+1)*(r+1) <= x
   120  INV {r*r <= x & x=X}
   121  DO r := r+1 OD
   122  {r*r <= X & X < (r+1)*(r+1)}"
   123 apply vcg_simp
   124 apply auto
   125 done
   126 
   127 (* without multiplication *)
   128 
   129 lemma sqrt_without_multiplication: "|- VARS u w r x.
   130  {True}
   131  x := X; u := 1; w := 1; r := (0::nat);
   132  WHILE w <= x
   133  INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X}
   134  DO r := r + 1; w := w + u + 2; u := u + 2 OD
   135  {r*r <= X & X < (r+1)*(r+1)}"
   136 apply vcg_simp
   137 apply auto
   138 done
   139 
   140 
   141 (*** LISTS ***)
   142 
   143 lemma imperative_reverse: "|- VARS y x.
   144  {x=X}
   145  y:=[];
   146  WHILE x ~= []
   147  INV {rev(x)@y = rev(X)}
   148  DO y := (hd x # y); x := tl x OD
   149  {y=rev(X)}"
   150 apply vcg_simp
   151  apply(simp add: neq_Nil_conv)
   152  apply auto
   153 done
   154 
   155 lemma imperative_append: "|- VARS x y.
   156  {x=X & y=Y}
   157  x := rev(x);
   158  WHILE x~=[]
   159  INV {rev(x)@y = X@Y}
   160  DO y := (hd x # y);
   161     x := tl x
   162  OD
   163  {y = X@Y}"
   164 apply vcg_simp
   165 apply(simp add: neq_Nil_conv)
   166 apply auto
   167 done
   168 
   169 
   170 (*** ARRAYS ***)
   171 
   172 (* Search for a key *)
   173 lemma zero_search: "|- VARS A i.
   174  {True}
   175  i := 0;
   176  WHILE i < length A & A!i ~= key
   177  INV {!j. j<i --> A!j ~= key}
   178  DO i := i+1 OD
   179  {(i < length A --> A!i = key) &
   180   (i = length A --> (!j. j < length A --> A!j ~= key))}"
   181 apply vcg_simp
   182 apply(blast elim!: less_SucE)
   183 done
   184 
   185 (* 
   186 The `partition' procedure for quicksort.
   187 `A' is the array to be sorted (modelled as a list).
   188 Elements of A must be of class order to infer at the end
   189 that the elements between u and l are equal to pivot.
   190 
   191 Ambiguity warnings of parser are due to := being used
   192 both for assignment and list update.
   193 *)
   194 lemma lem: "m - Suc 0 < n ==> m < Suc n"
   195 by arith
   196 
   197 
   198 lemma Partition:
   199 "[| leq == %A i. !k. k<i --> A!k <= pivot;
   200     geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
   201  |- VARS A u l.
   202  {0 < length(A::('a::order)list)}
   203  l := 0; u := length A - Suc 0;
   204  WHILE l <= u
   205   INV {leq A l & geq A u & u<length A & l<=length A}
   206   DO WHILE l < length A & A!l <= pivot
   207      INV {leq A l & geq A u & u<length A & l<=length A}
   208      DO l := l+1 OD;
   209      WHILE 0 < u & pivot <= A!u
   210      INV {leq A l & geq A u  & u<length A & l<=length A}
   211      DO u := u - 1 OD;
   212      IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
   213   OD
   214  {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
   215 (* expand and delete abbreviations first *)
   216 apply (simp);
   217 apply (erule thin_rl)+
   218 apply vcg_simp
   219     apply (force simp: neq_Nil_conv)
   220    apply (blast elim!: less_SucE intro: Suc_leI)
   221   apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
   222  apply (force simp: nth_list_update)
   223 apply (auto intro: order_antisym)
   224 done
   225 
   226 end