src/HOL/Hoare/hoare.ML
changeset 13857 11d7c5a8dbb7
parent 13737 e564c3d2d174
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Hoare/hoare.ML	Tue Mar 11 15:04:24 2003 +0100
     1.2 +++ b/src/HOL/Hoare/hoare.ML	Tue Mar 11 15:04:24 2003 +0100
     1.3 @@ -6,54 +6,11 @@
     1.4  Derivation of the proof rules and, most importantly, the VCG tactic.
     1.5  *)
     1.6  
     1.7 -(*** The proof rules ***)
     1.8 -
     1.9 -Goalw [thm "Valid_def"] "p <= q ==> Valid p (Basic id) q";
    1.10 -by (Auto_tac);
    1.11 -qed "SkipRule";
    1.12 -
    1.13 -Goalw [thm "Valid_def"] "p <= {s. (f s):q} ==> Valid p (Basic f) q";
    1.14 -by (Auto_tac);
    1.15 -qed "BasicRule";
    1.16 -
    1.17 -Goalw [thm "Valid_def"] "Valid P c1 Q ==> Valid Q c2 R ==> Valid P (c1;c2) R";
    1.18 -by (Asm_simp_tac 1);
    1.19 -by (Blast_tac 1);
    1.20 -qed "SeqRule";
    1.21 -
    1.22 -Goalw [thm "Valid_def"]
    1.23 - "p <= {s. (s:b --> s:w) & (s~:b --> s:w')} \
    1.24 -\ ==> Valid w c1 q ==> Valid w' c2 q \
    1.25 -\ ==> Valid p (Cond b c1 c2) q";
    1.26 -by (Asm_simp_tac 1);
    1.27 -by (Blast_tac 1);
    1.28 -qed "CondRule";
    1.29 -
    1.30 -Goal "! s s'. Sem c s s' --> s : I Int b --> s' : I ==> \
    1.31 -\     ! s s'. s : I --> iter n b (Sem c) s s' --> s' : I & s' ~: b";
    1.32 -by (induct_tac "n" 1);
    1.33 - by (Asm_simp_tac 1);
    1.34 -by (Simp_tac 1);
    1.35 -by (Blast_tac 1);
    1.36 -val lemma = result() RS spec RS spec RS mp RS mp;
    1.37 -
    1.38 -Goalw [thm "Valid_def"]
    1.39 - "p <= i ==> Valid (i Int b) c i ==> i Int (-b) <= q \
    1.40 -\ ==> Valid p (While b j c) q";
    1.41 -by (Asm_simp_tac 1);
    1.42 -by (Clarify_tac 1);
    1.43 -by (dtac lemma 1);
    1.44 -by (assume_tac 2);
    1.45 -by (Blast_tac 1);
    1.46 -by (Blast_tac 1);
    1.47 -qed "WhileRule'";
    1.48 -
    1.49 -Goal
    1.50 - "p <= i ==> Valid (i Int b) c i ==> i Int (-b) <= q \
    1.51 -\ ==> Valid p (While b i c) q";
    1.52 -by (rtac WhileRule' 1);
    1.53 -by (ALLGOALS assume_tac);
    1.54 -qed "WhileRule";
    1.55 +val SkipRule = thm"SkipRule";
    1.56 +val BasicRule = thm"BasicRule";
    1.57 +val SeqRule = thm"SeqRule";
    1.58 +val CondRule = thm"CondRule";
    1.59 +val WhileRule = thm"WhileRule";
    1.60  
    1.61  (*** The tactics ***)
    1.62  
    1.63 @@ -191,7 +148,8 @@
    1.64  
    1.65  (** HoareRuleTac **)
    1.66  
    1.67 -fun WlpTac Mlem tac i = rtac SeqRule i THEN  HoareRuleTac Mlem tac false (i+1)
    1.68 +fun WlpTac Mlem tac i =
    1.69 +  rtac SeqRule i THEN  HoareRuleTac Mlem tac false (i+1)
    1.70  and HoareRuleTac Mlem tac pre_cond i st = st |>
    1.71          (*abstraction over st prevents looping*)
    1.72      ( (WlpTac Mlem tac i THEN HoareRuleTac Mlem tac pre_cond i)