src/HOL/IMP/Hoare.ML
author nipkow
Wed Nov 24 12:12:36 1999 +0100 (1999-11-24)
changeset 8029 05446a898852
parent 5515 903c956beac3
child 9241 f961c1fdff50
permissions -rw-r--r--
Basis now Main.
     1 (*  Title:      HOL/IMP/Hoare.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995 TUM
     5 
     6 Soundness (and part of) relative completeness of Hoare rules
     7 wrt denotational semantics
     8 *)
     9 
    10 Goal "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}";
    11 by (etac hoare.conseq 1);
    12 by  (atac 1);
    13 by (Fast_tac 1);
    14 qed "hoare_conseq1";
    15 
    16 Goal "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}";
    17 by (rtac hoare.conseq 1);
    18 by    (atac 2);
    19 by   (ALLGOALS Fast_tac);
    20 qed "hoare_conseq2";
    21 
    22 Goalw [hoare_valid_def] "|- {P}c{Q} ==> |= {P}c{Q}";
    23 by (etac hoare.induct 1);
    24      by (ALLGOALS Asm_simp_tac);
    25   by (Fast_tac 1);
    26  by (Fast_tac 1);
    27 by (EVERY' [rtac allI, rtac allI, rtac impI] 1);
    28 by (etac induct2 1);
    29  by (rtac Gamma_mono 1);
    30 by (rewtac Gamma_def);  
    31 by (Fast_tac 1);
    32 qed "hoare_sound";
    33 
    34 Goalw [wp_def] "wp SKIP Q = Q";
    35 by (Simp_tac 1);
    36 qed "wp_SKIP";
    37 
    38 Goalw [wp_def] "wp (x:=a) Q = (%s. Q(s[x:=a s]))";
    39 by (Simp_tac 1);
    40 qed "wp_Ass";
    41 
    42 Goalw [wp_def] "wp (c;d) Q = wp c (wp d Q)";
    43 by (Simp_tac 1);
    44 by (rtac ext 1);
    45 by (Fast_tac 1);
    46 qed "wp_Semi";
    47 
    48 Goalw [wp_def]
    49  "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))";
    50 by (Simp_tac 1);
    51 by (rtac ext 1);
    52 by (Fast_tac 1);
    53 qed "wp_If";
    54 
    55 Goalw [wp_def]
    56   "b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";
    57 by (stac C_While_If 1);
    58 by (Asm_simp_tac 1);
    59 qed "wp_While_True";
    60 
    61 Goalw [wp_def] "~b s ==> wp (WHILE b DO c) Q s = Q s";
    62 by (stac C_While_If 1);
    63 by (Asm_simp_tac 1);
    64 qed "wp_While_False";
    65 
    66 Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
    67 
    68 (*Not suitable for rewriting: LOOPS!*)
    69 Goal "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";
    70 by (Simp_tac 1);
    71 qed "wp_While_if";
    72 
    73 Goal "wp (WHILE b DO c) Q s = \
    74 \  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
    75 by (Simp_tac 1);
    76 by (rtac iffI 1);
    77  by (rtac weak_coinduct 1);
    78   by (etac CollectI 1);
    79  by Safe_tac;
    80   by (rotate_tac ~1 1);
    81   by (Asm_full_simp_tac 1);
    82  by (rotate_tac ~1 1);
    83  by (Asm_full_simp_tac 1);
    84 by (asm_full_simp_tac (simpset() addsimps [wp_def,Gamma_def]) 1);
    85 by (strip_tac 1);
    86 by (rtac mp 1);
    87  by (assume_tac 2);
    88 by (etac induct2 1);
    89 by (fast_tac (claset() addSIs [monoI]) 1);
    90 by (stac gfp_Tarski 1);
    91  by (fast_tac (claset() addSIs [monoI]) 1);
    92 by (Fast_tac 1);
    93 qed "wp_While";
    94 
    95 Delsimps [C_while];
    96 
    97 AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
    98 
    99 Goal "!Q. |- {wp c Q} c {Q}";
   100 by (induct_tac "c" 1);
   101     by (ALLGOALS Simp_tac);
   102     by (REPEAT_FIRST Fast_tac);
   103  by (blast_tac (claset() addIs [hoare_conseq1]) 1);
   104 by Safe_tac;
   105 by (rtac hoare_conseq2 1);
   106  by (rtac hoare.While 1);
   107  by (rtac hoare_conseq1 1);
   108   by (Fast_tac 2);
   109  by (safe_tac HOL_cs);
   110  by (ALLGOALS (EVERY'[rotate_tac ~1, Asm_full_simp_tac]));
   111 qed_spec_mp "wp_is_pre";
   112 
   113 Goal "|= {P}c{Q} ==> |- {P}c{Q}";
   114 by (rtac (wp_is_pre RSN (2,hoare_conseq1)) 1);
   115 by (rewrite_goals_tac [hoare_valid_def,wp_def]);
   116 by (Fast_tac 1);
   117 qed "hoare_relative_complete";