# HG changeset patch
# User nipkow
# Date 1035811791 -3600
# Node ID 91674c8a008b5ee1ed949cb80fae1280c00a9dca
# Parent  06cce9be31a43b78b8287de8bc0cacd9210cd033
conversion ML -> thy

diff -r 06cce9be31a4 -r 91674c8a008b src/HOL/Hoare/Examples.thy
--- a/src/HOL/Hoare/Examples.thy	Sun Oct 27 23:34:02 2002 +0100
+++ b/src/HOL/Hoare/Examples.thy	Mon Oct 28 14:29:51 2002 +0100
@@ -6,4 +6,207 @@
 Various examples.
 *)
 
-Examples = Hoare + Arith2
+theory Examples = Hoare + Arith2:
+
+(*** ARITHMETIC ***)
+
+(** multiplication by successive addition **)
+
+lemma multiply_by_add: "|- VARS m s a b.
+  {a=A & b=B}
+  m := 0; s := 0;
+  WHILE m~=a
+  INV {s=m*b & a=A & b=B}
+  DO s := s+b; m := m+(1::nat) OD
+  {s = A*B}"
+by vcg_simp
+
+
+(** Euclid's algorithm for GCD **)
+
+lemma Euclid_GCD: "|- VARS a b.
+ {0<A & 0<B}
+ a := A; b := B;
+ WHILE  a~=b
+ INV {0<a & 0<b & gcd A B = gcd a b}
+ DO IF a<b THEN b := b-a ELSE a := a-b FI OD
+ {a = gcd A B}"
+apply vcg
+(*Now prove the verification conditions*)
+  apply auto
+  apply(simp add: gcd_diff_r less_imp_le)
+ apply(simp add: not_less_iff_le gcd_diff_l)
+apply(erule gcd_nnn)
+done
+
+(** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
+(* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
+   where it is given without the invariant. Instead of defining scm
+   explicitly we have used the theorem scm x y = x*y/gcd x y and avoided
+   division by mupltiplying with gcd x y.
+*)
+
+lemmas distribs =
+  diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2
+
+lemma gcd_scm: "|- VARS a b x y.
+ {0<A & 0<B & a=A & b=B & x=B & y=A}
+ WHILE  a ~= b
+ INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
+ DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD
+ {a = gcd A B & 2*A*B = a*(x+y)}"
+apply vcg
+  apply simp
+ apply(simp add: distribs gcd_diff_r not_less_iff_le gcd_diff_l)
+ apply arith
+apply(simp add: distribs gcd_nnn)
+done
+
+(** Power by iterated squaring and multiplication **)
+
+lemma power_by_mult: "|- VARS a b c.
+ {a=A & b=B}
+ c := (1::nat);
+ WHILE b ~= 0
+ INV {A^B = c * a^b}
+ DO  WHILE b mod 2 = 0
+     INV {A^B = c * a^b}
+     DO  a := a*a; b := b div 2 OD;
+     c := c*a; b := b - 1
+ OD
+ {c = A^B}"
+apply vcg_simp
+apply(case_tac "b")
+ apply(simp add: mod_less)
+apply simp
+done
+
+(** Factorial **)
+
+lemma factorial: "|- VARS a b.
+ {a=A}
+ b := 1;
+ WHILE a ~= 0
+ INV {fac A = b * fac a}
+ DO b := b*a; a := a - 1 OD
+ {b = fac A}"
+apply vcg_simp
+apply(clarsimp split: nat_diff_split)
+done
+
+
+(** Square root **)
+
+(* the easy way: *)
+
+lemma sqrt: "|- VARS r x.
+ {True}
+ x := X; r := (0::nat);
+ WHILE (r+1)*(r+1) <= x
+ INV {r*r <= x & x=X}
+ DO r := r+1 OD
+ {r*r <= X & X < (r+1)*(r+1)}"
+apply vcg_simp
+apply auto
+done
+
+(* without multiplication *)
+
+lemma sqrt_without_multiplication: "|- VARS u w r x.
+ {True}
+ x := X; u := 1; w := 1; r := (0::nat);
+ WHILE w <= x
+ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X}
+ DO r := r + 1; w := w + u + 2; u := u + 2 OD
+ {r*r <= X & X < (r+1)*(r+1)}"
+apply vcg_simp
+apply auto
+done
+
+
+(*** LISTS ***)
+
+lemma imperative_reverse: "|- VARS y x.
+ {x=X}
+ y:=[];
+ WHILE x ~= []
+ INV {rev(x)@y = rev(X)}
+ DO y := (hd x # y); x := tl x OD
+ {y=rev(X)}"
+apply vcg_simp
+ apply(simp add: neq_Nil_conv)
+ apply auto
+done
+
+lemma imperative_append: "|- VARS x y.
+ {x=X & y=Y}
+ x := rev(x);
+ WHILE x~=[]
+ INV {rev(x)@y = X@Y}
+ DO y := (hd x # y);
+    x := tl x
+ OD
+ {y = X@Y}"
+apply vcg_simp
+apply(simp add: neq_Nil_conv)
+apply auto
+done
+
+
+(*** ARRAYS ***)
+
+(* Search for a key *)
+lemma zero_search: "|- VARS A i.
+ {True}
+ i := 0;
+ WHILE i < length A & A!i ~= key
+ INV {!j. j<i --> A!j ~= key}
+ DO i := i+1 OD
+ {(i < length A --> A!i = key) &
+  (i = length A --> (!j. j < length A --> A!j ~= key))}"
+apply vcg_simp
+apply(blast elim!: less_SucE)
+done
+
+(* 
+The `partition' procedure for quicksort.
+`A' is the array to be sorted (modelled as a list).
+Elements of A must be of class order to infer at the end
+that the elements between u and l are equal to pivot.
+
+Ambiguity warnings of parser are due to := being used
+both for assignment and list update.
+*)
+lemma lem: "m - Suc 0 < n ==> m < Suc n"
+by arith
+
+
+lemma Partition:
+"[| leq == %A i. !k. k<i --> A!k <= pivot;
+    geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
+ |- VARS A u l.
+ {0 < length(A::('a::order)list)}
+ l := 0; u := length A - Suc 0;
+ WHILE l <= u
+  INV {leq A l & geq A u & u<length A & l<=length A}
+  DO WHILE l < length A & A!l <= pivot
+     INV {leq A l & geq A u & u<length A & l<=length A}
+     DO l := l+1 OD;
+     WHILE 0 < u & pivot <= A!u
+     INV {leq A l & geq A u  & u<length A & l<=length A}
+     DO u := u - 1 OD;
+     IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
+  OD
+ {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
+(* expand and delete abbreviations first *)
+apply (simp);
+apply (erule thin_rl)+
+apply vcg_simp
+    apply (force simp: neq_Nil_conv)
+   apply (blast elim!: less_SucE intro: Suc_leI)
+  apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
+ apply (force simp: nth_list_update)
+apply (auto intro: order_antisym)
+done
+
+end
\ No newline at end of file
diff -r 06cce9be31a4 -r 91674c8a008b src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Sun Oct 27 23:34:02 2002 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Mon Oct 28 14:29:51 2002 +0100
@@ -9,34 +9,34 @@
 later.
 *)
 
-Hoare  = Main +
+theory Hoare  = Main
+files ("Hoare.ML"):
 
 types
-    'a bexp = 'a set
-    'a assn = 'a set
-    'a fexp = 'a =>'a
+    'a bexp = "'a set"
+    'a assn = "'a set"
 
 datatype
- 'a com = Basic ('a fexp)         
-   | Seq ('a com) ('a com)               ("(_;/ _)"      [61,60] 60)
-   | Cond ('a bexp) ('a com) ('a com)    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
-   | While ('a bexp) ('a assn) ('a com)  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
+ 'a com = Basic "'a \<Rightarrow> 'a"         
+   | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
+   | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
+   | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
   
 syntax
-  "@assign"  :: id => 'b => 'a com        ("(2_ :=/ _)" [70,65] 61)
-  "@annskip" :: 'a com                    ("SKIP")
+  "@assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
+  "@annskip" :: "'a com"                    ("SKIP")
 
 translations
             "SKIP" == "Basic id"
 
-types 'a sem = 'a => 'a => bool
+types 'a sem = "'a => 'a => bool"
 
-consts iter :: nat => 'a bexp => 'a sem => 'a sem
+consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
 primrec
 "iter 0 b S = (%s s'. s ~: b & (s=s'))"
 "iter (Suc n) b S = (%s s'. s : b & (? s''. S s s'' & iter n b S s'' s'))"
 
-consts Sem :: 'a com => 'a sem
+consts Sem :: "'a com => 'a sem"
 primrec
 "Sem(Basic f) s s' = (s' = f s)"
 "Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')"
@@ -44,7 +44,7 @@
                                       (s ~: b --> Sem c2 s s'))"
 "Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')"
 
-constdefs Valid :: ['a bexp, 'a com, 'a bexp] => bool
+constdefs Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
   "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
 
 
@@ -56,18 +56,15 @@
   "_vars" 	     :: "[id, vars] => vars"	       ("_ _")
 
 syntax
- "@hoare_vars" :: [vars, 'a assn,'a com,'a assn] => bool
+ "@hoare_vars" :: "[vars, 'a assn,'a com,'a assn] => bool"
                  ("|- VARS _.// {_} // _ // {_}" [0,0,55,0] 50)
 syntax ("" output)
- "@hoare"      :: ['a assn,'a com,'a assn] => bool
+ "@hoare"      :: "['a assn,'a com,'a assn] => bool"
                  ("|- {_} // _ // {_}" [0,55,0] 50)
 
-end
-
-ML
-
 (** parse translations **)
 
+ML{*
 fun mk_abstuple []     body = absfree ("x", dummyT, body)
   | mk_abstuple [v]    body = absfree ((fst o dest_Free) v, dummyT, body)
   | mk_abstuple (v::w) body = Syntax.const "split" $
@@ -80,19 +77,20 @@
                            mk_fbody v e xs;
 
 fun mk_fexp v e xs = mk_abstuple xs (mk_fbody v e xs);
-
+*}
 
 (* bexp_tr & assn_tr *)
 (*all meta-variables for bexp except for TRUE are translated as if they
   were boolean expressions*)
-  
+ML{*
 fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"
   | bexp_tr b xs = Syntax.const "Collect" $ mk_abstuple xs b;
   
 fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
+*}
 
 (* com_tr *)
-  
+ML{*
 fun assign_tr [Free (V,_),E] xs = Syntax.const "Basic" $
                                       mk_fexp (Free(V,dummyT)) E xs
   | assign_tr ts _ = raise TERM ("assign_tr", ts);
@@ -107,9 +105,10 @@
   | com_tr (Const ("While",_) $ b $ I $ c) xs = Syntax.const "While" $
                                          bexp_tr b xs $ assn_tr I xs $ com_tr c xs
   | com_tr trm _ = trm;
+*}
 
 (* triple_tr *)
-
+ML{*
 fun vars_tr (x as Free _) = [x]
   | vars_tr (Const ("_vars", _) $ (x as Free _) $ vars) = x :: vars_tr vars
   | vars_tr t = raise TERM ("vars_tr", [t]);
@@ -120,16 +119,15 @@
            assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
       end
   | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
-  
+*}
 
-
-val parse_translation = [("@hoare_vars", hoare_vars_tr)];
+parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
 
 
 (*****************************************************************************)
 
 (*** print translations ***)
-
+ML{*
 fun dest_abstuple (Const ("split",_) $ (Abs(v,_, body))) =
                             subst_bound (Syntax.free v, dest_abstuple body)
   | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
@@ -156,9 +154,10 @@
 fun is_f (Const ("split",_) $ (Abs(x,_,t))) = true
   | is_f (Abs(x,_,t)) = true
   | is_f t = false;
-  
+*}
+
 (* assn_tr' & bexp_tr'*)
-  
+ML{*  
 fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
   | assn_tr' (Const ("op Int",_) $ (Const ("Collect",_) $ T1) $ 
                                    (Const ("Collect",_) $ T2)) =  
@@ -167,9 +166,10 @@
 
 fun bexp_tr' (Const ("Collect",_) $ T) = dest_abstuple T 
   | bexp_tr' t = t;
+*}
 
 (*com_tr' *)
-
+ML{*
 fun mk_assign f =
   let val (vs, ts) = mk_vts f;
       val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
@@ -189,5 +189,21 @@
 
 fun spec_tr' [p, c, q] =
   Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
- 
-val print_translation = [("Valid", spec_tr')];
+*}
+
+print_translation {* [("Valid", spec_tr')] *}
+
+use "Hoare.ML"
+
+method_setup vcg = {*
+  Method.no_args
+    (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
+  "verification condition generator"
+
+method_setup vcg_simp = {*
+  Method.ctxt_args (fn ctxt =>
+    Method.METHOD (fn facts => 
+      hoare_tac (asm_full_simp_tac (Simplifier.get_local_simpset ctxt))1)) *}
+  "verification condition generator plus simplification"
+
+end
diff -r 06cce9be31a4 -r 91674c8a008b src/HOL/Hoare/Pointers.thy
--- a/src/HOL/Hoare/Pointers.thy	Sun Oct 27 23:34:02 2002 +0100
+++ b/src/HOL/Hoare/Pointers.thy	Mon Oct 28 14:29:51 2002 +0100
@@ -94,13 +94,27 @@
 
 section"Hoare logic"
 
-(* This should already be done in Hoare.thy, which should be converted to
-Isar *)
+consts fac :: "nat \<Rightarrow> nat"
+primrec
+"fac 0 = 1"
+"fac (Suc n) = Suc n * fac n"
+
+lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
+by(induct i, simp_all)
 
-method_setup vcg_simp_tac = {*
-  Method.no_args
-    (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac Asm_full_simp_tac)) *}
-  "verification condition generator plus simplification"
+lemma "|- VARS i f.
+ {True}
+ i := (1::nat); f := 1;
+ WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
+ DO f := f*i; i := i+1 OD
+ {f = fac n}"
+apply vcg_simp
+apply(subgoal_tac "i = Suc n")
+apply simp
+apply arith
+done
+
+
 
 subsection"List reversal"
 
@@ -111,7 +125,7 @@
                  rev As' @ Bs' = rev As @ Bs}
   DO r := p; p := tl(the p); tl := tl(the r := q); q := r OD
   {list tl q (rev As @ Bs)}"
-apply vcg_simp_tac
+apply vcg_simp
 
 apply(rule_tac x = As in exI)
 apply simp
@@ -144,7 +158,7 @@
   INV {p ~= None & (\<exists>As'. list tl p As' \<and> X \<in> set As')}
   DO p := tl(the p) OD
   {p = Some X}"
-apply vcg_simp_tac
+apply vcg_simp
   apply(case_tac p)
    apply clarsimp
   apply fastsimp
@@ -162,7 +176,7 @@
   INV {p ~= None & (\<exists>As'. path tl p As' (Some X))}
   DO p := tl(the p) OD
   {p = Some X}"
-apply vcg_simp_tac
+apply vcg_simp
   apply(case_tac p)
    apply clarsimp
   apply(rule conjI)
@@ -195,7 +209,7 @@
   INV {p ~= None & Some X \<in> ({(Some x,tl x) |x. True}^* `` {p})}
   DO p := tl(the p) OD
   {p = Some X}"
-apply vcg_simp_tac
+apply vcg_simp
   apply(case_tac p)
    apply(simp add:lem1 eq_sym_conv)
   apply simp
@@ -214,7 +228,7 @@
   INV {p ~= None & X \<in> ({(x,y). tl x = Some y}^* `` {the p})}
   DO p := tl(the p) OD
   {p = Some X}"
-apply vcg_simp_tac
+apply vcg_simp
  apply clarsimp
  apply(erule converse_rtranclE)
   apply simp
diff -r 06cce9be31a4 -r 91674c8a008b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Oct 27 23:34:02 2002 +0100
+++ b/src/HOL/IsaMakefile	Mon Oct 28 14:29:51 2002 +0100
@@ -293,7 +293,7 @@
 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
 
 $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \
-  Hoare/Examples.ML Hoare/Examples.thy Hoare/Hoare.ML Hoare/Hoare.thy \
+  Hoare/Examples.thy Hoare/Hoare.ML Hoare/Hoare.thy \
   Hoare/Pointers.thy Hoare/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Hoare