src/HOL/Hoare/Examples.thy
 changeset 13737 e564c3d2d174 parent 13684 48bfc2cc0938 child 13789 d37f66755f47
```     1.1 --- a/src/HOL/Hoare/Examples.thy	Thu Nov 28 15:44:34 2002 +0100
1.2 +++ b/src/HOL/Hoare/Examples.thy	Fri Nov 29 09:48:28 2002 +0100
1.3 @@ -12,7 +12,7 @@
1.4
1.5  (** multiplication by successive addition **)
1.6
1.7 -lemma multiply_by_add: "|- VARS m s a b.
1.8 +lemma multiply_by_add: "VARS m s a b
1.9    {a=A & b=B}
1.10    m := 0; s := 0;
1.11    WHILE m~=a
1.12 @@ -24,7 +24,7 @@
1.13
1.14  (** Euclid's algorithm for GCD **)
1.15
1.16 -lemma Euclid_GCD: "|- VARS a b.
1.17 +lemma Euclid_GCD: "VARS a b
1.18   {0<A & 0<B}
1.19   a := A; b := B;
1.20   WHILE  a~=b
1.21 @@ -49,7 +49,7 @@
1.22  lemmas distribs =
1.24
1.25 -lemma gcd_scm: "|- VARS a b x y.
1.26 +lemma gcd_scm: "VARS a b x y
1.27   {0<A & 0<B & a=A & b=B & x=B & y=A}
1.28   WHILE  a ~= b
1.29   INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
1.30 @@ -64,7 +64,7 @@
1.31
1.32  (** Power by iterated squaring and multiplication **)
1.33
1.34 -lemma power_by_mult: "|- VARS a b c.
1.35 +lemma power_by_mult: "VARS a b c
1.36   {a=A & b=B}
1.37   c := (1::nat);
1.38   WHILE b ~= 0
1.39 @@ -83,7 +83,7 @@
1.40
1.41  (** Factorial **)
1.42
1.43 -lemma factorial: "|- VARS a b.
1.44 +lemma factorial: "VARS a b
1.45   {a=A}
1.46   b := 1;
1.47   WHILE a ~= 0
1.48 @@ -97,7 +97,7 @@
1.49  lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
1.50  by(induct i, simp_all)
1.51
1.52 -lemma "|- VARS i f.
1.53 +lemma "VARS i f
1.54   {True}
1.55   i := (1::nat); f := 1;
1.56   WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
1.57 @@ -113,7 +113,7 @@
1.58
1.59  (* the easy way: *)
1.60
1.61 -lemma sqrt: "|- VARS r x.
1.62 +lemma sqrt: "VARS r x
1.63   {True}
1.64   x := X; r := (0::nat);
1.65   WHILE (r+1)*(r+1) <= x
1.66 @@ -126,7 +126,7 @@
1.67
1.68  (* without multiplication *)
1.69
1.70 -lemma sqrt_without_multiplication: "|- VARS u w r x.
1.71 +lemma sqrt_without_multiplication: "VARS u w r x
1.72   {True}
1.73   x := X; u := 1; w := 1; r := (0::nat);
1.74   WHILE w <= x
1.75 @@ -140,7 +140,7 @@
1.76
1.77  (*** LISTS ***)
1.78
1.79 -lemma imperative_reverse: "|- VARS y x.
1.80 +lemma imperative_reverse: "VARS y x
1.81   {x=X}
1.82   y:=[];
1.83   WHILE x ~= []
1.84 @@ -152,7 +152,7 @@
1.85   apply auto
1.86  done
1.87
1.88 -lemma imperative_append: "|- VARS x y.
1.89 +lemma imperative_append: "VARS x y
1.90   {x=X & y=Y}
1.91   x := rev(x);
1.92   WHILE x~=[]
1.93 @@ -170,7 +170,7 @@
1.94  (*** ARRAYS ***)
1.95
1.96  (* Search for a key *)
1.97 -lemma zero_search: "|- VARS A i.
1.98 +lemma zero_search: "VARS A i
1.99   {True}
1.100   i := 0;
1.101   WHILE i < length A & A!i ~= key
1.102 @@ -198,7 +198,7 @@
1.103  lemma Partition:
1.104  "[| leq == %A i. !k. k<i --> A!k <= pivot;
1.105      geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
1.106 - |- VARS A u l.
1.107 + VARS A u l
1.108   {0 < length(A::('a::order)list)}
1.109   l := 0; u := length A - Suc 0;
1.110   WHILE l <= u
```