src/HOLCF/ex/Hoare.ML

--- a/src/HOLCF/ex/Hoare.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/ex/Hoare.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -40,7 +40,7 @@
 
 val hoare_lemma5 = prove_goal HOLCF.thy 
 "[|(? k. b1`(iterate k g x) ~= TT);\
-\   k=theleast(%n. b1`(iterate n g x) ~= TT)|] ==> \
+\   k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
 \ b1`(iterate k g x)=FF | b1`(iterate k g x)=UU"
  (fn prems =>
         [
@@ -48,7 +48,7 @@
         (hyp_subst_tac 1),
         (rtac hoare_lemma2 1),
         (etac exE 1),
-        (etac theleast1 1)
+        (etac LeastI 1)
         ]);
 
 val hoare_lemma6 = prove_goal HOLCF.thy "b=UU ==> b~=TT"
@@ -69,7 +69,7 @@
 
 val hoare_lemma8 = prove_goal HOLCF.thy 
 "[|(? k. b1`(iterate k g x) ~= TT);\
-\   k=theleast(%n. b1`(iterate n g x) ~= TT)|] ==> \
+\   k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
 \ !m. m < k --> b1`(iterate m g x)=TT"
  (fn prems =>
         [
@@ -81,11 +81,11 @@
         (atac 2),
         (rtac (le_less_trans RS less_irrefl) 1),
         (atac 2),
-        (rtac theleast2 1),
+        (rtac Least_le 1),
         (etac hoare_lemma6 1),
         (rtac (le_less_trans RS less_irrefl) 1),
         (atac 2),
-        (rtac theleast2 1),
+        (rtac Least_le 1),
         (etac hoare_lemma7 1)
         ]);
 
@@ -143,8 +143,8 @@
  (fn prems =>
         [
         (nat_ind_tac "k" 1),
-        (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
-        (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
+        (Simp_tac 1),
+        (Simp_tac 1),
         (strip_tac 1),
         (res_inst_tac [("s","p`(iterate k1 g x)")] trans 1),
         (rtac trans 1),
@@ -152,7 +152,7 @@
         (res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
         (rtac mp 1),
         (etac spec 1),
-        (Simp_tac 1),
+        (simp_tac (!simpset addsimps [less_Suc_eq]) 1),
         (simp_tac HOLCF_ss 1),
         (etac mp 1),
         (strip_tac 1),
@@ -168,24 +168,18 @@
  (fn prems =>
         [
         (nat_ind_tac "k" 1),
-        (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
-        (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
+        (Simp_tac 1),
+(simp_tac (!simpset addsimps [less_Suc_eq]) 1),
         (strip_tac 1),
         (res_inst_tac [("s","q`(iterate k1 g x)")] trans 1),
         (rtac trans 1),
         (rtac (q_def3 RS sym) 2),
         (res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
-        (rtac mp 1),
-        (etac spec 1),
-        (Simp_tac 1),
+        (fast_tac HOL_cs 1),
         (simp_tac HOLCF_ss 1),
         (etac mp 1),
         (strip_tac 1),
-        (rtac mp 1),
-        (etac spec 1),
-        (etac less_trans 1),
-        (Simp_tac 1)
-        ]);
+	(fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1)]);
 
 (* -------- results about p for case (? k. b1`(iterate k g x)~=TT) ------- *)
 
@@ -193,14 +187,14 @@
 val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
 (* 
 val hoare_lemma10 = "[| ? k. b1`(iterate k g ?x1) ~= TT;
-    Suc ?k3 = theleast (%n. b1`(iterate n g ?x1) ~= TT) |] ==>
+    Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
  p`(iterate ?k3 g ?x1) = p`?x1" : thm
 
 *)
 
 val hoare_lemma11 = prove_goal Hoare.thy 
 "(? n.b1`(iterate n g x) ~= TT) ==>\
-\ k=theleast(%n.b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
+\ k=Least(%n.b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
 \ --> p`x = iterate k g x"
  (fn prems =>
         [
@@ -214,7 +208,7 @@
         (rtac p_def3 1),
         (asm_simp_tac HOLCF_ss 1),
         (eres_inst_tac
-           [("s","0"),("t","theleast(%n. b1`(iterate n g x) ~= TT)")] subst 1),
+           [("s","0"),("t","Least(%n. b1`(iterate n g x) ~= TT)")] subst 1),
         (Simp_tac 1),
         (hyp_subst_tac 1),
         (strip_tac 1),
@@ -240,7 +234,7 @@
 
 val hoare_lemma12 = prove_goal Hoare.thy 
 "(? n. b1`(iterate n g x) ~= TT) ==>\
-\ k=theleast(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
+\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
 \ --> p`x = UU"
  (fn prems =>
         [
@@ -398,13 +392,13 @@
 val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
 (* 
 val hoare_lemma25 = "[| ? k. b1`(iterate k g ?x1) ~= TT;
-    Suc ?k3 = theleast (%n. b1`(iterate n g ?x1) ~= TT) |] ==>
+    Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
  q`(iterate ?k3 g ?x1) = q`?x1" : thm
 *)
 
 val hoare_lemma26 = prove_goal Hoare.thy 
 "(? n. b1`(iterate n g x)~=TT) ==>\
-\ k=theleast(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x) =FF \
+\ k=Least(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x) =FF \
 \ --> q`x = q`(iterate k g x)"
  (fn prems =>
         [
@@ -433,7 +427,7 @@
 
 val hoare_lemma27 = prove_goal Hoare.thy 
 "(? n. b1`(iterate n g x) ~= TT) ==>\
-\ k=theleast(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
+\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
 \ --> q`x = UU"
  (fn prems =>
         [