--- 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);
--- 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'"