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