src/HOL/IMP/Hoare.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4241 3f3f87c6fe3b
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     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 open Hoare;
    11 
    12 goalw Hoare.thy [hoare_valid_def] "!!P c Q. |- {P}c{Q} ==> |= {P}c{Q}";
    13 by (etac hoare.induct 1);
    14     by (ALLGOALS Asm_simp_tac);
    15   by (Fast_tac 1);
    16  by (Fast_tac 1);
    17 by (rtac allI 1);
    18 by (rtac allI 1);
    19 by (rtac impI 1);
    20 by (etac induct2 1);
    21  by (rtac Gamma_mono 1);
    22 by (rewtac Gamma_def);  
    23 by (Fast_tac 1);
    24 qed "hoare_sound";
    25 
    26 goalw Hoare.thy [wp_def] "wp SKIP Q = Q";
    27 by (Simp_tac 1);
    28 qed "wp_SKIP";
    29 
    30 goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s. Q(s[a s/x]))";
    31 by (Simp_tac 1);
    32 qed "wp_Ass";
    33 
    34 goalw Hoare.thy [wp_def] "wp (c;d) Q = wp c (wp d Q)";
    35 by (Simp_tac 1);
    36 by (rtac ext 1);
    37 by (Fast_tac 1);
    38 qed "wp_Semi";
    39 
    40 goalw Hoare.thy [wp_def]
    41   "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) & \
    42 \                                    (~b s --> wp d Q s))";
    43 by (Simp_tac 1);
    44 by (rtac ext 1);
    45 by (Fast_tac 1);
    46 qed "wp_If";
    47 
    48 goalw Hoare.thy [wp_def]
    49   "!!s. b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";
    50 by (stac C_While_If 1);
    51 by (Asm_simp_tac 1);
    52 qed "wp_While_True";
    53 
    54 goalw Hoare.thy [wp_def] "!!s. ~b s ==> wp (WHILE b DO c) Q s = Q s";
    55 by (stac C_While_If 1);
    56 by (Asm_simp_tac 1);
    57 qed "wp_While_False";
    58 
    59 Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
    60 
    61 (*Not suitable for rewriting: LOOPS!*)
    62 goal Hoare.thy "wp (WHILE b DO c) Q s = \
    63 \                 (if b s then wp (c;WHILE b DO c) Q s else Q s)";
    64 by (simp_tac (simpset() addsplits [expand_if]) 1);
    65 qed "wp_While_if";
    66 
    67 goal thy
    68   "wp (WHILE b DO c) Q s = \
    69 \  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
    70 by (simp_tac (simpset() addsplits [expand_if]) 1);
    71 by (rtac iffI 1);
    72  by (rtac weak_coinduct 1);
    73   by (etac CollectI 1);
    74  by Safe_tac;
    75   by (rotate_tac ~1 1);
    76   by (Asm_full_simp_tac 1);
    77  by (rotate_tac ~1 1);
    78  by (Asm_full_simp_tac 1);
    79 by (asm_full_simp_tac (simpset() addsimps [wp_def,Gamma_def]) 1);
    80 by (strip_tac 1);
    81 by (rtac mp 1);
    82  by (assume_tac 2);
    83 by (etac induct2 1);
    84 by (fast_tac (claset() addSIs [monoI]) 1);
    85 by (stac gfp_Tarski 1);
    86  by (fast_tac (claset() addSIs [monoI]) 1);
    87 by (Fast_tac 1);
    88 qed "wp_While";
    89 
    90 Delsimps [C_while];
    91 
    92 AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
    93 
    94 goal Hoare.thy "!Q. |- {wp c Q} c {Q}";
    95 by (com.induct_tac "c" 1);
    96 by (ALLGOALS Simp_tac);
    97 by (REPEAT_FIRST Fast_tac);
    98 by (deepen_tac (claset() addIs [hoare.conseq]) 0 1);
    99 by Safe_tac;
   100 by (rtac hoare.conseq 1);
   101   by (etac thin_rl 1);
   102   by (Fast_tac 1);
   103  by (rtac hoare.While 1);
   104  by (rtac hoare.conseq 1);
   105    by (etac thin_rl 3);
   106    by (rtac allI 3);
   107    by (rtac impI 3);
   108    by (assume_tac 3);
   109   by (Fast_tac 2);
   110  by (safe_tac HOL_cs);
   111  by (rotate_tac ~1 1);
   112  by (Asm_full_simp_tac 1);
   113 by (rotate_tac ~1 1);
   114 by (Asm_full_simp_tac 1);
   115 qed_spec_mp "wp_is_pre";
   116 
   117 goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
   118 by (rtac (wp_is_pre RSN (2,hoare.conseq)) 1);
   119  by (Fast_tac 2);
   120 by (rewrite_goals_tac [hoare_valid_def,wp_def]);
   121 by (Fast_tac 1);
   122 qed "hoare_relative_complete";