src/HOL/Hoare/Examples.thy
 author nipkow Thu Jul 07 12:39:17 2005 +0200 (2005-07-07) changeset 16733 236dfafbeb63 parent 16417 9bc16273c2d4 child 16796 140f1e0ea846 permissions -rw-r--r--
linear arithmetic now takes "&" in assumptions apart.
 clasohm@1476 ` 1` ```(* Title: HOL/Hoare/Examples.thy ``` nipkow@1335 ` 2` ``` ID: \$Id\$ ``` clasohm@1476 ` 3` ``` Author: Norbert Galm ``` nipkow@5646 ` 4` ``` Copyright 1998 TUM ``` nipkow@1335 ` 5` nipkow@5646 ` 6` ```Various examples. ``` nipkow@1335 ` 7` ```*) ``` nipkow@1335 ` 8` haftmann@16417 ` 9` ```theory Examples imports Hoare Arith2 begin ``` nipkow@13682 ` 10` nipkow@13682 ` 11` ```(*** ARITHMETIC ***) ``` nipkow@13682 ` 12` nipkow@13682 ` 13` ```(** multiplication by successive addition **) ``` nipkow@13682 ` 14` nipkow@13737 ` 15` ```lemma multiply_by_add: "VARS m s a b ``` nipkow@13682 ` 16` ``` {a=A & b=B} ``` nipkow@13682 ` 17` ``` m := 0; s := 0; ``` nipkow@13682 ` 18` ``` WHILE m~=a ``` nipkow@13682 ` 19` ``` INV {s=m*b & a=A & b=B} ``` nipkow@13682 ` 20` ``` DO s := s+b; m := m+(1::nat) OD ``` nipkow@13682 ` 21` ``` {s = A*B}" ``` nipkow@13682 ` 22` ```by vcg_simp ``` nipkow@13682 ` 23` nipkow@13789 ` 24` ```lemma "VARS M N P :: int ``` nipkow@13789 ` 25` ``` {m=M & n=N} ``` nipkow@13789 ` 26` ``` IF M < 0 THEN M := -M; N := -N ELSE SKIP FI; ``` nipkow@13789 ` 27` ``` P := 0; ``` nipkow@13789 ` 28` ``` WHILE 0 < M ``` nipkow@13789 ` 29` ``` INV {0 <= M & (EX p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N)} ``` nipkow@13789 ` 30` ``` DO P := P+N; M := M - 1 OD ``` nipkow@13789 ` 31` ``` {P = m*n}" ``` nipkow@13789 ` 32` ```apply vcg_simp ``` nipkow@13789 ` 33` ``` apply (simp add:int_distrib) ``` nipkow@13789 ` 34` ```apply clarsimp ``` nipkow@13789 ` 35` ```apply(rule conjI) ``` nipkow@13789 ` 36` ``` apply clarsimp ``` nipkow@13789 ` 37` ```apply clarsimp ``` nipkow@13789 ` 38` ```done ``` nipkow@13682 ` 39` nipkow@13682 ` 40` ```(** Euclid's algorithm for GCD **) ``` nipkow@13682 ` 41` nipkow@13737 ` 42` ```lemma Euclid_GCD: "VARS a b ``` nipkow@13682 ` 43` ``` {0 b ``` nipkow@13682 ` 46` ``` INV {0 i \ fac (i - Suc 0) * i = fac i" ``` nipkow@13684 ` 112` ```by(induct i, simp_all) ``` nipkow@13684 ` 113` nipkow@13737 ` 114` ```lemma "VARS i f ``` nipkow@13684 ` 115` ``` {True} ``` nipkow@13684 ` 116` ``` i := (1::nat); f := 1; ``` nipkow@13684 ` 117` ``` WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1} ``` nipkow@13684 ` 118` ``` DO f := f*i; i := i+1 OD ``` nipkow@13684 ` 119` ``` {f = fac n}" ``` nipkow@13684 ` 120` ```apply vcg_simp ``` nipkow@13684 ` 121` ```apply(subgoal_tac "i = Suc n") ``` nipkow@13684 ` 122` ```apply simp ``` nipkow@13684 ` 123` ```apply arith ``` nipkow@13684 ` 124` ```done ``` nipkow@13682 ` 125` nipkow@13682 ` 126` ```(** Square root **) ``` nipkow@13682 ` 127` nipkow@13682 ` 128` ```(* the easy way: *) ``` nipkow@13682 ` 129` nipkow@13737 ` 130` ```lemma sqrt: "VARS r x ``` nipkow@13682 ` 131` ``` {True} ``` nipkow@13682 ` 132` ``` x := X; r := (0::nat); ``` nipkow@13682 ` 133` ``` WHILE (r+1)*(r+1) <= x ``` nipkow@13682 ` 134` ``` INV {r*r <= x & x=X} ``` nipkow@13682 ` 135` ``` DO r := r+1 OD ``` nipkow@13682 ` 136` ``` {r*r <= X & X < (r+1)*(r+1)}" ``` nipkow@13682 ` 137` ```apply vcg_simp ``` nipkow@13682 ` 138` ```done ``` nipkow@13682 ` 139` nipkow@13682 ` 140` ```(* without multiplication *) ``` nipkow@13682 ` 141` nipkow@13737 ` 142` ```lemma sqrt_without_multiplication: "VARS u w r x ``` nipkow@13682 ` 143` ``` {True} ``` nipkow@13682 ` 144` ``` x := X; u := 1; w := 1; r := (0::nat); ``` nipkow@13682 ` 145` ``` WHILE w <= x ``` nipkow@13682 ` 146` ``` INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X} ``` nipkow@13682 ` 147` ``` DO r := r + 1; w := w + u + 2; u := u + 2 OD ``` nipkow@13682 ` 148` ``` {r*r <= X & X < (r+1)*(r+1)}" ``` nipkow@13682 ` 149` ```apply vcg_simp ``` nipkow@13682 ` 150` ```done ``` nipkow@13682 ` 151` nipkow@13682 ` 152` nipkow@13682 ` 153` ```(*** LISTS ***) ``` nipkow@13682 ` 154` nipkow@13737 ` 155` ```lemma imperative_reverse: "VARS y x ``` nipkow@13682 ` 156` ``` {x=X} ``` nipkow@13682 ` 157` ``` y:=[]; ``` nipkow@13682 ` 158` ``` WHILE x ~= [] ``` nipkow@13682 ` 159` ``` INV {rev(x)@y = rev(X)} ``` nipkow@13682 ` 160` ``` DO y := (hd x # y); x := tl x OD ``` nipkow@13682 ` 161` ``` {y=rev(X)}" ``` nipkow@13682 ` 162` ```apply vcg_simp ``` nipkow@13682 ` 163` ``` apply(simp add: neq_Nil_conv) ``` nipkow@13682 ` 164` ``` apply auto ``` nipkow@13682 ` 165` ```done ``` nipkow@13682 ` 166` nipkow@13737 ` 167` ```lemma imperative_append: "VARS x y ``` nipkow@13682 ` 168` ``` {x=X & y=Y} ``` nipkow@13682 ` 169` ``` x := rev(x); ``` nipkow@13682 ` 170` ``` WHILE x~=[] ``` nipkow@13682 ` 171` ``` INV {rev(x)@y = X@Y} ``` nipkow@13682 ` 172` ``` DO y := (hd x # y); ``` nipkow@13682 ` 173` ``` x := tl x ``` nipkow@13682 ` 174` ``` OD ``` nipkow@13682 ` 175` ``` {y = X@Y}" ``` nipkow@13682 ` 176` ```apply vcg_simp ``` nipkow@13682 ` 177` ```apply(simp add: neq_Nil_conv) ``` nipkow@13682 ` 178` ```apply auto ``` nipkow@13682 ` 179` ```done ``` nipkow@13682 ` 180` nipkow@13682 ` 181` nipkow@13682 ` 182` ```(*** ARRAYS ***) ``` nipkow@13682 ` 183` nipkow@13682 ` 184` ```(* Search for a key *) ``` nipkow@13737 ` 185` ```lemma zero_search: "VARS A i ``` nipkow@13682 ` 186` ``` {True} ``` nipkow@13682 ` 187` ``` i := 0; ``` nipkow@13682 ` 188` ``` WHILE i < length A & A!i ~= key ``` nipkow@13682 ` 189` ``` INV {!j. j A!j ~= key} ``` nipkow@13682 ` 190` ``` DO i := i+1 OD ``` nipkow@13682 ` 191` ``` {(i < length A --> A!i = key) & ``` nipkow@13682 ` 192` ``` (i = length A --> (!j. j < length A --> A!j ~= key))}" ``` nipkow@13682 ` 193` ```apply vcg_simp ``` nipkow@13682 ` 194` ```apply(blast elim!: less_SucE) ``` nipkow@13682 ` 195` ```done ``` nipkow@13682 ` 196` nipkow@13682 ` 197` ```(* ``` nipkow@13682 ` 198` ```The `partition' procedure for quicksort. ``` nipkow@13682 ` 199` ````A' is the array to be sorted (modelled as a list). ``` nipkow@13682 ` 200` ```Elements of A must be of class order to infer at the end ``` nipkow@13682 ` 201` ```that the elements between u and l are equal to pivot. ``` nipkow@13682 ` 202` nipkow@13682 ` 203` ```Ambiguity warnings of parser are due to := being used ``` nipkow@13682 ` 204` ```both for assignment and list update. ``` nipkow@13682 ` 205` ```*) ``` nipkow@13682 ` 206` ```lemma lem: "m - Suc 0 < n ==> m < Suc n" ``` nipkow@13682 ` 207` ```by arith ``` nipkow@13682 ` 208` nipkow@13682 ` 209` nipkow@13682 ` 210` ```lemma Partition: ``` nipkow@13682 ` 211` ```"[| leq == %A i. !k. k A!k <= pivot; ``` nipkow@13682 ` 212` ``` geq == %A i. !k. i pivot <= A!k |] ==> ``` nipkow@13737 ` 213` ``` VARS A u l ``` nipkow@13682 ` 214` ``` {0 < length(A::('a::order)list)} ``` nipkow@13682 ` 215` ``` l := 0; u := length A - Suc 0; ``` nipkow@13682 ` 216` ``` WHILE l <= u ``` nipkow@13682 ` 217` ``` INV {leq A l & geq A u & u A!k = pivot) & geq A l}" ``` nipkow@13682 ` 227` ```(* expand and delete abbreviations first *) ``` nipkow@13682 ` 228` ```apply (simp); ``` nipkow@13682 ` 229` ```apply (erule thin_rl)+ ``` nipkow@13682 ` 230` ```apply vcg_simp ``` nipkow@16733 ` 231` ``` apply (force simp: neq_Nil_conv) ``` nipkow@16733 ` 232` ``` apply (blast elim!: less_SucE intro: Suc_leI) ``` nipkow@16733 ` 233` ``` apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem) ``` nipkow@16733 ` 234` ```apply (force simp: nth_list_update) ``` nipkow@13682 ` 235` ```done ``` nipkow@13682 ` 236` nipkow@13682 ` 237` `end`