src/HOL/IMP/Hoare.ML
author paulson
Mon Aug 19 11:17:20 1996 +0200 (1996-08-19)
changeset 1910 6d572f96fb76
parent 1747 f20c9abe4b50
child 1973 8c94c9a5be10
permissions -rw-r--r--
Tidied some proofs, maybe using less_SucE
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);
nipkow@1447
    14
    by(ALLGOALS Asm_simp_tac);
nipkow@1447
    15
  by(fast_tac rel_cs 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);
nipkow@1447
    21
 br Gamma_mono 1;
nipkow@1747
    22
by(prune_params_tac);
nipkow@1747
    23
by(rename_tac "s t" 1);
clasohm@1465
    24
by (rewtac Gamma_def);  
nipkow@1747
    25
by(eres_inst_tac [("x","s")] allE 1);
paulson@1910
    26
by (Step_tac 1);
nipkow@1447
    27
  by(ALLGOALS Asm_full_simp_tac);
paulson@1730
    28
qed "hoare_sound";
nipkow@936
    29
nipkow@1696
    30
goalw Hoare.thy [swp_def] "swp SKIP Q = Q";
nipkow@1481
    31
by(Simp_tac 1);
nipkow@1481
    32
br ext 1;
paulson@1910
    33
by (Fast_tac 1);
nipkow@1696
    34
qed "swp_SKIP";
nipkow@1481
    35
nipkow@1696
    36
goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[a s/x]))";
nipkow@1481
    37
by(Simp_tac 1);
nipkow@1481
    38
qed "swp_Ass";
nipkow@1481
    39
nipkow@1481
    40
goalw Hoare.thy [swp_def] "swp (c;d) Q = swp c (swp d Q)";
nipkow@1481
    41
by(Simp_tac 1);
nipkow@1481
    42
br ext 1;
paulson@1910
    43
by (Fast_tac 1);
nipkow@1481
    44
qed "swp_Semi";
nipkow@936
    45
nipkow@1481
    46
goalw Hoare.thy [swp_def]
nipkow@1696
    47
  "swp (IF b THEN c ELSE d) Q = (%s. (b s --> swp c Q s) & \
nipkow@1696
    48
\                                    (~b s --> swp d Q s))";
nipkow@1481
    49
by(Simp_tac 1);
nipkow@1481
    50
br ext 1;
paulson@1910
    51
by (Fast_tac 1);
nipkow@1481
    52
qed "swp_If";
nipkow@936
    53
nipkow@1481
    54
goalw Hoare.thy [swp_def]
nipkow@1696
    55
  "!!s. b s ==> swp (WHILE b DO c) Q s = swp (c;WHILE b DO c) Q s";
nipkow@1481
    56
by(stac C_While_If 1);
nipkow@1481
    57
by(Asm_simp_tac 1);
nipkow@1481
    58
qed "swp_While_True";
nipkow@1481
    59
nipkow@1696
    60
goalw Hoare.thy [swp_def] "!!s. ~b s ==> swp (WHILE b DO c) Q s = Q s";
nipkow@1481
    61
by(stac C_While_If 1);
nipkow@1481
    62
by(Asm_simp_tac 1);
paulson@1910
    63
by (Fast_tac 1);
nipkow@1481
    64
qed "swp_While_False";
nipkow@1481
    65
nipkow@1696
    66
Addsimps [swp_SKIP,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False];
nipkow@1481
    67
paulson@1910
    68
(*Not suitable for rewriting: LOOPS!*)
paulson@1910
    69
goal Hoare.thy "swp (WHILE b DO c) Q s = \
paulson@1910
    70
\                 (if b s then swp (c;WHILE b DO c) Q s else Q s)";
paulson@1910
    71
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@1910
    72
qed "swp_While_if";
paulson@1910
    73
paulson@1910
    74
nipkow@1481
    75
Delsimps [C_while];
nipkow@936
    76
paulson@1910
    77
AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
paulson@1910
    78
nipkow@1486
    79
goal Hoare.thy "!Q. |- {swp c Q} c {Q}";
nipkow@1481
    80
by(com.induct_tac "c" 1);
nipkow@1481
    81
by(ALLGOALS Simp_tac);
paulson@1910
    82
by (REPEAT_FIRST Fast_tac);
paulson@1910
    83
by (deepen_tac (!claset addIs [hoare.conseq]) 0 1);
paulson@1910
    84
by (Step_tac 1);
nipkow@1481
    85
br hoare.conseq 1;
nipkow@1481
    86
  be thin_rl 1;
paulson@1910
    87
  by (Fast_tac 1);
nipkow@1696
    88
 br hoare.While 1;
nipkow@1481
    89
 br hoare.conseq 1;
nipkow@1481
    90
   be thin_rl 3;
nipkow@1481
    91
   br allI 3;
nipkow@1481
    92
   br impI 3;
nipkow@1481
    93
   ba 3;
paulson@1910
    94
  by (Fast_tac 2);
nipkow@1481
    95
 by(safe_tac HOL_cs);
nipkow@1481
    96
 by(rotate_tac ~1 1);
nipkow@1481
    97
 by(Asm_full_simp_tac 1);
nipkow@1481
    98
by(rotate_tac ~1 1);
nipkow@1481
    99
by(Asm_full_simp_tac 1);
nipkow@1486
   100
qed_spec_mp "swp_is_pre";
nipkow@1481
   101
nipkow@1486
   102
goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
nipkow@1481
   103
br (swp_is_pre RSN (2,hoare.conseq)) 1;
paulson@1910
   104
 by (Fast_tac 2);
nipkow@1696
   105
by(rewrite_goals_tac [hoare_valid_def,swp_def]);
paulson@1910
   106
by (Fast_tac 1);
nipkow@1481
   107
qed "hoare_relative_complete";