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