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.23    diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2
    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