src/HOL/IMP/Hoare.ML
author nipkow
Tue Mar 18 18:02:19 1997 +0100 (1997-03-18)
changeset 2810 c4e16b36bc57
parent 2055 cc274e47f607
child 2861 7bbd3751523f
permissions -rw-r--r--
Added wp_while.
clasohm@1465
     1
(*  Title:      HOL/IMP/Hoare.ML
nipkow@938
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Tobias Nipkow
nipkow@936
     4
    Copyright   1995 TUM
nipkow@936
     5
nipkow@1481
     6
Soundness (and part of) relative completeness of Hoare rules
nipkow@1481
     7
wrt denotational semantics
nipkow@936
     8
*)
nipkow@936
     9
nipkow@936
    10
open Hoare;
nipkow@936
    11
paulson@1730
    12
goalw Hoare.thy [hoare_valid_def] "!!P c Q. |- {P}c{Q} ==> |= {P}c{Q}";
paulson@1730
    13
by (etac hoare.induct 1);
paulson@2055
    14
    by (ALLGOALS Asm_simp_tac);
nipkow@1973
    15
  by (Fast_tac 1);
paulson@1910
    16
 by (Fast_tac 1);
clasohm@1465
    17
by (rtac allI 1);
clasohm@1465
    18
by (rtac allI 1);
clasohm@1465
    19
by (rtac impI 1);
clasohm@1465
    20
by (etac induct2 1);
paulson@2055
    21
 by (rtac Gamma_mono 1);
clasohm@1465
    22
by (rewtac Gamma_def);  
nipkow@1973
    23
by (Fast_tac 1);
paulson@1730
    24
qed "hoare_sound";
nipkow@936
    25
nipkow@2810
    26
goalw Hoare.thy [wp_def] "wp SKIP Q = Q";
paulson@2031
    27
by (Simp_tac 1);
nipkow@2810
    28
qed "wp_SKIP";
nipkow@1481
    29
nipkow@2810
    30
goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s.Q(s[a s/x]))";
paulson@2031
    31
by (Simp_tac 1);
nipkow@2810
    32
qed "wp_Ass";
nipkow@1481
    33
nipkow@2810
    34
goalw Hoare.thy [wp_def] "wp (c;d) Q = wp c (wp d Q)";
paulson@2031
    35
by (Simp_tac 1);
paulson@2031
    36
by (rtac ext 1);
paulson@1910
    37
by (Fast_tac 1);
nipkow@2810
    38
qed "wp_Semi";
nipkow@936
    39
nipkow@2810
    40
goalw Hoare.thy [wp_def]
nipkow@2810
    41
  "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) & \
nipkow@2810
    42
\                                    (~b s --> wp d Q s))";
paulson@2031
    43
by (Simp_tac 1);
paulson@2031
    44
by (rtac ext 1);
paulson@1910
    45
by (Fast_tac 1);
nipkow@2810
    46
qed "wp_If";
nipkow@936
    47
nipkow@2810
    48
goalw Hoare.thy [wp_def]
nipkow@2810
    49
  "!!s. b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";
paulson@2031
    50
by (stac C_While_If 1);
paulson@2031
    51
by (Asm_simp_tac 1);
nipkow@2810
    52
qed "wp_While_True";
nipkow@1481
    53
nipkow@2810
    54
goalw Hoare.thy [wp_def] "!!s. ~b s ==> wp (WHILE b DO c) Q s = Q s";
paulson@2031
    55
by (stac C_While_If 1);
paulson@2031
    56
by (Asm_simp_tac 1);
nipkow@2810
    57
qed "wp_While_False";
nipkow@1481
    58
nipkow@2810
    59
Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
nipkow@1481
    60
paulson@1910
    61
(*Not suitable for rewriting: LOOPS!*)
nipkow@2810
    62
goal Hoare.thy "wp (WHILE b DO c) Q s = \
nipkow@2810
    63
\                 (if b s then wp (c;WHILE b DO c) Q s else Q s)";
paulson@1910
    64
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
nipkow@2810
    65
qed "wp_While_if";
paulson@1910
    66
nipkow@2810
    67
goal thy
nipkow@2810
    68
  "wp (WHILE b DO c) Q s = \
nipkow@2810
    69
\  (s : gfp(%S.{s.if b s then wp c (%s.s:S) s else Q s}))";
nipkow@2810
    70
by(simp_tac (!simpset setloop(split_tac[expand_if])) 1);
nipkow@2810
    71
br iffI 1;
nipkow@2810
    72
 br weak_coinduct 1;
nipkow@2810
    73
  by(Best_tac 1);
nipkow@2810
    74
 by(safe_tac (!claset));
nipkow@2810
    75
  by(rotate_tac ~1 1);
nipkow@2810
    76
  by(Asm_full_simp_tac 1);
nipkow@2810
    77
 by(rotate_tac ~1 1);
nipkow@2810
    78
 by(Asm_full_simp_tac 1);
nipkow@2810
    79
by(asm_full_simp_tac (!simpset addsimps [wp_def,Gamma_def]) 1);
nipkow@2810
    80
by(strip_tac 1);
nipkow@2810
    81
br mp 1;
nipkow@2810
    82
 ba 2;
nipkow@2810
    83
be induct2 1;
nipkow@2810
    84
by(fast_tac (!claset addSIs [monoI]) 1);
nipkow@2810
    85
by(stac gfp_Tarski 1);
nipkow@2810
    86
 by(fast_tac (!claset addSIs [monoI]) 1);
nipkow@2810
    87
by(Fast_tac 1);
nipkow@2810
    88
qed "wp_While";
paulson@1910
    89
nipkow@1481
    90
Delsimps [C_while];
nipkow@936
    91
paulson@1910
    92
AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
paulson@1910
    93
nipkow@2810
    94
goal Hoare.thy "!Q. |- {wp c Q} c {Q}";
paulson@2031
    95
by (com.induct_tac "c" 1);
paulson@2031
    96
by (ALLGOALS Simp_tac);
paulson@1910
    97
by (REPEAT_FIRST Fast_tac);
paulson@1910
    98
by (deepen_tac (!claset addIs [hoare.conseq]) 0 1);
paulson@1910
    99
by (Step_tac 1);
paulson@2031
   100
by (rtac hoare.conseq 1);
paulson@2055
   101
  by (etac thin_rl 1);
paulson@1910
   102
  by (Fast_tac 1);
paulson@2055
   103
 by (rtac hoare.While 1);
paulson@2055
   104
 by (rtac hoare.conseq 1);
paulson@2055
   105
   by (etac thin_rl 3);
paulson@2055
   106
   by (rtac allI 3);
paulson@2055
   107
   by (rtac impI 3);
paulson@2055
   108
   by (assume_tac 3);
paulson@1910
   109
  by (Fast_tac 2);
paulson@2055
   110
 by (safe_tac HOL_cs);
paulson@2055
   111
 by (rotate_tac ~1 1);
paulson@2055
   112
 by (Asm_full_simp_tac 1);
paulson@2031
   113
by (rotate_tac ~1 1);
paulson@2031
   114
by (Asm_full_simp_tac 1);
nipkow@2810
   115
qed_spec_mp "wp_is_pre";
nipkow@1481
   116
nipkow@1486
   117
goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
nipkow@2810
   118
by (rtac (wp_is_pre RSN (2,hoare.conseq)) 1);
paulson@1910
   119
 by (Fast_tac 2);
nipkow@2810
   120
by (rewrite_goals_tac [hoare_valid_def,wp_def]);
paulson@1910
   121
by (Fast_tac 1);
nipkow@1481
   122
qed "hoare_relative_complete";