src/HOL/IMP/Hoare.ML
author berghofe
Fri Jul 24 13:03:20 1998 +0200 (1998-07-24)
changeset 5183 89f162de39cf
parent 5117 7b5efef2ca74
child 5223 4cb05273f764
permissions -rw-r--r--
Adapted to new datatype package.
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
nipkow@5117
    12
Goalw [hoare_valid_def] "|- {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
wenzelm@5069
    26
Goalw [wp_def] "wp SKIP Q = Q";
paulson@2031
    27
by (Simp_tac 1);
nipkow@2810
    28
qed "wp_SKIP";
nipkow@1481
    29
wenzelm@5069
    30
Goalw [wp_def] "wp (x:=a) Q = (%s. Q(s[x:=a s]))";
paulson@2031
    31
by (Simp_tac 1);
nipkow@2810
    32
qed "wp_Ass";
nipkow@1481
    33
wenzelm@5069
    34
Goalw [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
wenzelm@5069
    40
Goalw [wp_def]
nipkow@5117
    41
 "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))";
paulson@2031
    42
by (Simp_tac 1);
paulson@2031
    43
by (rtac ext 1);
paulson@1910
    44
by (Fast_tac 1);
nipkow@2810
    45
qed "wp_If";
nipkow@936
    46
wenzelm@5069
    47
Goalw [wp_def]
nipkow@5117
    48
  "b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";
paulson@2031
    49
by (stac C_While_If 1);
paulson@2031
    50
by (Asm_simp_tac 1);
nipkow@2810
    51
qed "wp_While_True";
nipkow@1481
    52
nipkow@5117
    53
Goalw [wp_def] "~b s ==> wp (WHILE b DO c) Q s = Q s";
paulson@2031
    54
by (stac C_While_If 1);
paulson@2031
    55
by (Asm_simp_tac 1);
nipkow@2810
    56
qed "wp_While_False";
nipkow@1481
    57
nipkow@2810
    58
Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
nipkow@1481
    59
paulson@1910
    60
(*Not suitable for rewriting: LOOPS!*)
nipkow@5117
    61
Goal
nipkow@5117
    62
 "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";
nipkow@4686
    63
by (Simp_tac 1);
nipkow@2810
    64
qed "wp_While_if";
paulson@1910
    65
wenzelm@5069
    66
Goal
nipkow@2810
    67
  "wp (WHILE b DO c) Q s = \
wenzelm@3842
    68
\  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
nipkow@4686
    69
by (Simp_tac 1);
paulson@3023
    70
by (rtac iffI 1);
paulson@3023
    71
 by (rtac weak_coinduct 1);
paulson@3023
    72
  by (etac CollectI 1);
paulson@4153
    73
 by Safe_tac;
paulson@3023
    74
  by (rotate_tac ~1 1);
paulson@3023
    75
  by (Asm_full_simp_tac 1);
paulson@3023
    76
 by (rotate_tac ~1 1);
paulson@3023
    77
 by (Asm_full_simp_tac 1);
wenzelm@4089
    78
by (asm_full_simp_tac (simpset() addsimps [wp_def,Gamma_def]) 1);
paulson@3023
    79
by (strip_tac 1);
paulson@3023
    80
by (rtac mp 1);
paulson@3023
    81
 by (assume_tac 2);
paulson@3023
    82
by (etac induct2 1);
wenzelm@4089
    83
by (fast_tac (claset() addSIs [monoI]) 1);
paulson@3023
    84
by (stac gfp_Tarski 1);
wenzelm@4089
    85
 by (fast_tac (claset() addSIs [monoI]) 1);
paulson@3023
    86
by (Fast_tac 1);
nipkow@2810
    87
qed "wp_While";
paulson@1910
    88
nipkow@1481
    89
Delsimps [C_while];
nipkow@936
    90
paulson@1910
    91
AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
paulson@1910
    92
wenzelm@5069
    93
Goal "!Q. |- {wp c Q} c {Q}";
berghofe@5183
    94
by (induct_tac "c" 1);
paulson@2031
    95
by (ALLGOALS Simp_tac);
paulson@1910
    96
by (REPEAT_FIRST Fast_tac);
paulson@4241
    97
by (blast_tac (claset() addIs [hoare.conseq]) 1);
paulson@3737
    98
by Safe_tac;
paulson@2031
    99
by (rtac hoare.conseq 1);
paulson@2055
   100
  by (etac thin_rl 1);
paulson@1910
   101
  by (Fast_tac 1);
paulson@2055
   102
 by (rtac hoare.While 1);
paulson@2055
   103
 by (rtac hoare.conseq 1);
paulson@2055
   104
   by (etac thin_rl 3);
paulson@2055
   105
   by (rtac allI 3);
paulson@2055
   106
   by (rtac impI 3);
paulson@2055
   107
   by (assume_tac 3);
paulson@1910
   108
  by (Fast_tac 2);
paulson@2055
   109
 by (safe_tac HOL_cs);
paulson@2055
   110
 by (rotate_tac ~1 1);
paulson@2055
   111
 by (Asm_full_simp_tac 1);
paulson@2031
   112
by (rotate_tac ~1 1);
paulson@2031
   113
by (Asm_full_simp_tac 1);
nipkow@2810
   114
qed_spec_mp "wp_is_pre";
nipkow@1481
   115
nipkow@5117
   116
Goal "|= {P}c{Q} ==> |- {P}c{Q}";
nipkow@2810
   117
by (rtac (wp_is_pre RSN (2,hoare.conseq)) 1);
paulson@1910
   118
 by (Fast_tac 2);
nipkow@2810
   119
by (rewrite_goals_tac [hoare_valid_def,wp_def]);
paulson@1910
   120
by (Fast_tac 1);
nipkow@1481
   121
qed "hoare_relative_complete";