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