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