# HG changeset patch
# User nipkow
# Date 860155512 -7200
# Node ID 4e92704cf32029955735151b4deda32e7d7a88cc
# Parent  d5e1a2b869a216a9f35dd2259597d7b368a418fe
renamed variable 'inv'

diff -r d5e1a2b869a2 -r 4e92704cf320 src/HOL/Hoare/Hoare.ML
--- a/src/HOL/Hoare/Hoare.ML	Fri Apr 04 14:01:18 1997 +0200
+++ b/src/HOL/Hoare/Hoare.ML	Fri Apr 04 14:05:12 1997 +0200
@@ -38,18 +38,16 @@
   (fn [prem1,prem2] =>[cut_facts_tac [prem2] 1,
                        fast_tac (!claset addIs [prem1]) 1]);
 
-val [iter_0,iter_Suc] = nat_recs Iter_def;
-
 val lemma = prove_goalw thy [Spec_def,While_def]
-  "[| Spec (%s.inv s & b s) c inv; !!s. [| inv s; ~b s |] ==> q s |] \
-\  ==> Spec inv (While b inv c) q"
+  "[| Spec (%s.I s & b s) c I; !!s. [| I s; ~b s |] ==> q s |] \
+\  ==> Spec I (While b I c) q"
   (fn [prem1,prem2] =>
      [REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2,
       etac thin_rl 1, res_inst_tac[("x","s")]spec 1,
       res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
-      simp_tac (!simpset addsimps [iter_0]) 1,
+      Simp_tac 1,
       fast_tac (!claset addIs [prem2]) 1,
-      simp_tac (!simpset addsimps [iter_Suc,Seq_def]) 1,
+      simp_tac (!simpset addsimps [Seq_def]) 1,
       cut_facts_tac [prem1] 1, fast_tac (!claset addIs [prem2]) 1]);
 
 val WhileRule = lemma RSN (2,strenthen_pre);
diff -r d5e1a2b869a2 -r 4e92704cf320 src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Fri Apr 04 14:01:18 1997 +0200
+++ b/src/HOL/Hoare/Hoare.thy	Fri Apr 04 14:05:12 1997 +0200
@@ -42,12 +42,15 @@
   Cond          :: ['a bexp, 'a com, 'a com] => 'a com
   "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
 
-  While         :: ['a bexp, 'a bexp, 'a com] => 'a com
-  "While b inv c s s' == ? n. Iter n b c s s'"
+consts
+  Iter          :: [nat, 'a bexp, 'a com] => 'a com
+primrec Iter nat
+  "Iter 0 b c = (%s s'.~b(s) & (s=s'))"
+  "Iter (Suc n) b c = (%s s'. b(s) & Seq c (Iter n b c) s s')"
 
-  Iter          :: [nat, 'a bexp, 'a com] => 'a com
-  "Iter n b c == nat_rec (%s s'.~b(s) & (s=s'))
-             (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s') n"
+constdefs
+  While         :: ['a bexp, 'a bexp, 'a com] => 'a com
+  "While b I c s s' == ? n. Iter n b c s s'"
 
   Spec          :: ['a bexp, 'a com, 'a bexp] => bool
   "Spec p c q == !s s'. c s s' --> p s --> q s'"