# 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'"