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