src/HOL/IMPP/Hoare.ML
author wenzelm
Sat, 17 Sep 2005 20:14:30 +0200
changeset 17477 ceb42ea2f223
parent 13911 f5c3750292f5
child 17956 369e2af8ee45
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     1
(*  Title:      HOL/IMPP/Hoare.ML
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     2
    ID:         $Id$
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     3
    Author:     David von Oheimb
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     4
    Copyright   1999 TUM
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     5
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     6
Soundness and relative completeness of Hoare rules wrt operational semantics
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     7
*)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     8
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
     9
Goalw [state_not_singleton_def]
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
    10
        "state_not_singleton ==> !t. (!s::state. s = t) --> False";
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    11
by (Clarify_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    12
by (case_tac "ta = t" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    13
by  (ALLGOALS (blast_tac (HOL_cs addDs [not_sym])));
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    14
qed "single_stateE";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    15
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    16
Addsimps[peek_and_def];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    17
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    18
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    19
section "validity";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    20
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
    21
Goalw [triple_valid_def]
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    22
  "|=n:{P}.c.{Q} = (!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s'))";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    23
by Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    24
qed "triple_valid_def2";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    25
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    26
Goal "|=0:{P}. BODY pn .{Q}";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    27
by (simp_tac (simpset() addsimps [triple_valid_def2]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    28
by (Clarsimp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    29
qed "Body_triple_valid_0";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    30
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    31
(* only ==> direction required *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    32
Goal "|=n:{P}. the (body pn) .{Q} = |=Suc n:{P}. BODY pn .{Q}";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    33
by (simp_tac (simpset() addsimps [triple_valid_def2]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    34
by (Force_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    35
qed "Body_triple_valid_Suc";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    36
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    37
Goalw [triple_valid_def] "|=Suc n:t --> |=n:t";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    38
by (induct_tac "t" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    39
by (Simp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    40
by (fast_tac (claset() addIs [evaln_Suc]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    41
qed_spec_mp "triple_valid_Suc";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    42
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    43
Goal "||=Suc n:ts ==> ||=n:ts";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    44
by (fast_tac (claset() addIs [triple_valid_Suc]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    45
qed "triples_valid_Suc";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    46
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    47
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    48
section "derived rules";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    49
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    50
Goal "[| G|-{P'}.c.{Q'}; !Z s. P Z s --> \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    51
\                        (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s') |] \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    52
\      ==> G|-{P}.c.{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
    53
by (rtac hoare_derivs.conseq 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    54
by (Blast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    55
qed "conseq12";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    56
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    57
Goal "[| G|-{P'}.c.{Q}; !Z s. P Z s --> P' Z s |] ==> G|-{P}.c.{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
    58
by (etac conseq12 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    59
by (Fast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    60
qed "conseq1";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    61
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    62
Goal "[| G|-{P}.c.{Q'}; !Z s. Q' Z s --> Q Z s |] ==> G|-{P}.c.{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
    63
by (etac conseq12 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    64
by (Fast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    65
qed "conseq2";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    66
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
    67
Goal "[| G Un (%p. {P p}.      BODY p  .{Q p})`Procs  \
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
    68
\         ||- (%p. {P p}. the (body p) .{Q p})`Procs; \
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    69
\   pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
    70
by (dtac hoare_derivs.Body 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
    71
by (etac hoare_derivs.weaken 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    72
by (Fast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    73
qed "Body1";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    74
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    75
Goal "(insert ({P}. BODY pn .{Q}) G) |-{P}. the (body pn) .{Q} ==> \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    76
\ G|-{P}. BODY pn .{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
    77
by (rtac Body1 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
    78
by (rtac singletonI 2);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    79
by (Clarsimp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    80
qed "BodyN";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    81
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    82
Goal "[| !Z s. P Z s --> G|-{%Z s'. s'=s}.c.{%Z'. Q Z} |] ==> G|-{P}.c.{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
    83
by (rtac hoare_derivs.conseq 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    84
by (Fast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    85
qed "escape";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    86
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    87
Goal "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
    88
by (rtac hoare_derivs.conseq 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    89
by (fast_tac (claset() addDs (premises())) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    90
qed "constant";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    91
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    92
Goal "G|-{%Z s. P Z s & ~b s}.WHILE b DO c.{P}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
    93
by (rtac (hoare_derivs.Loop RS conseq2) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    94
by  (ALLGOALS Simp_tac);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
    95
by (rtac hoare_derivs.conseq 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    96
by (Fast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    97
qed "LoopF";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    98
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    99
(*
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   100
Goal "[| G'||-ts; G' <= G |] ==> G||-ts";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   101
by (etac hoare_derivs.cut 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   102
by (etac hoare_derivs.asm 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   103
qed "thin";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   104
*)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   105
Goal "G'||-ts ==> !G. G' <= G --> G||-ts";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   106
by (etac hoare_derivs.induct 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   107
by                (ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1]));
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   108
by (rtac                  hoare_derivs.empty 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   109
by               (eatac hoare_derivs.insert 1 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   110
by              (fast_tac (claset() addIs [hoare_derivs.asm]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   111
by             (fast_tac (claset() addIs [hoare_derivs.cut]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   112
by            (fast_tac (claset() addIs [hoare_derivs.weaken]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   113
by           (EVERY'[rtac hoare_derivs.conseq, strip_tac, smp_tac 2,Clarify_tac,
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   114
                     smp_tac 1,rtac exI, rtac exI, eatac conjI 1] 1);
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   115
by          (EVERY'[rtac hoare_derivs.Body,dtac spec,etac mp,Fast_tac] 7);
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   116
by         (ALLGOALS (resolve_tac ((funpow 5 tl) hoare_derivs.intros)
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   117
                      THEN_ALL_NEW Fast_tac));
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   118
qed_spec_mp "thin";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   119
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   120
Goal "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   121
by (rtac BodyN 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   122
by (etac thin 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   123
by Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   124
qed "weak_Body";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   125
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   126
Goal "G||-insert t ts ==> G|-t & G||-ts";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   127
by (fast_tac (claset() addIs [hoare_derivs.weaken]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   128
qed "derivs_insertD";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   129
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   130
Goal "[| finite U; \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   131
\ !p. G |-     {P' p}.c0 p.{Q' p}       --> G |-     {P p}.c0 p.{Q p} |] ==> \
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   132
\     G||-(%p. {P' p}.c0 p.{Q' p}) ` U --> G||-(%p. {P p}.c0 p.{Q p}) ` U";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   133
by (etac finite_induct 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   134
by (ALLGOALS Clarsimp_tac);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   135
by (dtac derivs_insertD 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   136
by (rtac hoare_derivs.insert 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   137
by  Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   138
qed_spec_mp "finite_pointwise";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   139
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   140
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   141
section "soundness";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   142
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   143
Goalw [hoare_valids_def]
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   144
 "G|={P &> b}. c .{P} ==> \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   145
\ G|={P}. WHILE b DO c .{P &> (Not o b)}";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   146
by (full_simp_tac (simpset() addsimps [triple_valid_def2]) 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   147
by (rtac allI 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   148
by (subgoal_tac "!d s s'. <d,s> -n-> s' --> \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   149
\ d = WHILE b DO c --> ||=n:G --> (!Z. P Z s --> P Z s' & ~b s')" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   150
by  (EVERY'[etac thin_rl, Fast_tac] 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   151
by (EVERY'[REPEAT o rtac allI, rtac impI] 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   152
by ((etac evaln.induct THEN_ALL_NEW Simp_tac) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   153
by  (ALLGOALS Fast_tac);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   154
qed "Loop_sound_lemma";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   155
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   156
Goalw [hoare_valids_def]
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   157
   "[| G Un (%pn. {P pn}.      BODY pn  .{Q pn})`Procs \
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   158
\        ||=(%pn. {P pn}. the (body pn) .{Q pn})`Procs |] ==> \
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   159
\       G||=(%pn. {P pn}.      BODY pn  .{Q pn})`Procs";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   160
by (rtac allI 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   161
by (induct_tac "n" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   162
by  (fast_tac (claset() addIs [Body_triple_valid_0]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   163
by (Clarsimp_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   164
by (dtac triples_valid_Suc 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   165
by (mp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   166
by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   167
by (EVERY'[dtac spec, etac impE, etac conjI, atac] 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   168
by (fast_tac (claset() addSIs [Body_triple_valid_Suc RS iffD1]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   169
qed "Body_sound_lemma";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   170
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   171
Goal "G||-ts ==> G||=ts";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   172
by (etac hoare_derivs.induct 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   173
by              (TRYALL (eresolve_tac [Loop_sound_lemma, Body_sound_lemma]
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   174
                         THEN_ALL_NEW atac));
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   175
by            (rewtac hoare_valids_def);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   176
by            (Blast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   177
by           (Blast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   178
by          (Blast_tac 1); (* asm *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   179
by         (Blast_tac 1); (* cut *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   180
by        (Blast_tac 1); (* weaken *)
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   181
by       (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs",
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   182
                           Simp_tac, Clarify_tac, REPEAT o smp_tac 1]));
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   183
by       (ALLGOALS (full_simp_tac (simpset() addsimps [triple_valid_def2])));
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   184
by       (EVERY'[strip_tac, smp_tac 2, Blast_tac] 1); (* conseq *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   185
by      (ALLGOALS Clarsimp_tac); (* Skip, Ass, Local *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   186
by   (Force_tac 3); (* Call *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   187
by  (eresolve_tac evaln_elim_cases 2); (* If *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   188
by   (TRYALL Blast_tac);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   189
qed "hoare_sound";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   190
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   191
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   192
section "completeness";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   193
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   194
(* Both versions *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   195
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   196
(*unused*)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   197
Goalw [MGT_def] "G|-MGT c ==> \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   198
\ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   199
by (etac conseq12 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   200
by Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   201
qed "MGT_alternI";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   202
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   203
(* requires com_det *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   204
Goalw [MGT_def] "state_not_singleton ==> \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   205
\ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1} ==> G|-MGT c";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   206
by (etac conseq12 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   207
by Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   208
by (case_tac "? t. <c,?s> -c-> t" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   209
by  (fast_tac (claset() addEs [com_det]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   210
by (Clarsimp_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   211
by (dtac single_stateE 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   212
by (Blast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   213
qed "MGT_alternD";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   214
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   215
Goalw [MGT_def]
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   216
 "{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   217
by (etac conseq12 1);
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   218
by (clarsimp_tac (claset(), simpset() addsimps
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   219
  [hoare_valids_def,eval_eq,triple_valid_def2]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   220
qed "MGF_complete";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   221
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   222
AddSEs WTs_elim_cases;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   223
(* requires com_det, escape (i.e. hoare_derivs.conseq) *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   224
Goal "state_not_singleton ==> \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   225
\ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   226
by (induct_tac "c" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   227
by        (ALLGOALS Clarsimp_tac);
13911
f5c3750292f5 added thm"..." due to new Map.thy
nipkow
parents: 13612
diff changeset
   228
by        (fast_tac (claset() addIs [(thm"domI")]) 7);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   229
by (etac MGT_alternD 6);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   230
by       (rewtac MGT_def);
13911
f5c3750292f5 added thm"..." due to new Map.thy
nipkow
parents: 13612
diff changeset
   231
by       (EVERY'[dtac bspec, etac (thm"domI")] 7);
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   232
by       (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   233
             [("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")]
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   234
             (hoare_derivs.Call RS conseq1), etac conseq12] 7);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   235
by        (ALLGOALS (etac thin_rl));
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   236
by (rtac (hoare_derivs.Skip RS conseq2) 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   237
by (rtac (hoare_derivs.Ass RS conseq1) 2);
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   238
by        (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   239
                  [("P1","%Z' s. s=(Z[Loc loc::=fun Z])")]
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   240
                  (hoare_derivs.Local RS conseq1), etac conseq12] 3);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   241
by         (EVERY'[etac hoare_derivs.Comp, etac conseq12] 5);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   242
by         ((rtac hoare_derivs.If THEN_ALL_NEW etac conseq12) 6);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   243
by          (EVERY'[rtac (hoare_derivs.Loop RS conseq2), etac conseq12] 8);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   244
by           Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   245
qed_spec_mp "MGF_lemma1";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   246
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   247
(* Version: nested single recursion *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   248
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   249
Goal "[| !!G ts. ts <= G ==> P G ts;\
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   250
\ !!G pn. P (insert (mgt_call pn) G) {mgt(the(body pn))} ==> P G {mgt_call pn};\
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   251
\         !!G c. [| wt c; !pn:U. P G {mgt_call pn} |] ==> P G {mgt c}; \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   252
\         !!pn. pn : U ==> wt (the (body pn)); \
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   253
\         finite U; uG = mgt_call`U |] ==> \
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   254
\ !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   255
by (cut_facts_tac (premises()) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   256
by (induct_tac "n" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   257
by  (ALLGOALS Clarsimp_tac);
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   258
by  (subgoal_tac "G = mgt_call ` U" 1);
9078
b8780970d0ed tidied for new card_seteq
paulson
parents: 8177
diff changeset
   259
by   (asm_simp_tac (simpset() addsimps [card_seteq, finite_imageI]) 2);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   260
by  (Asm_full_simp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   261
by  (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   262
by (rtac ballI 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   263
by  (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   264
by  (Fast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   265
by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   266
by (rtac ballI 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   267
by (case_tac "mgt_call pn : G" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   268
by  (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   269
by  (Fast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   270
by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1);
13612
55d32e76ef4e Adapted to new simplifier.
berghofe
parents: 13524
diff changeset
   271
byev[dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3];
55d32e76ef4e Adapted to new simplifier.
berghofe
parents: 13524
diff changeset
   272
by   (eresolve_tac (tl(tl(tl(premises())))) 3);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   273
by   (Fast_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   274
by (dtac finite_subset 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   275
by (etac finite_imageI 1);
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   276
by (Asm_simp_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   277
by (arith_tac 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   278
qed_spec_mp "nesting_lemma";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   279
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   280
Goalw [MGT_def] "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==> \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   281
\ G|-{=}.BODY pn.{->}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   282
by (rtac BodyN 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   283
by (etac conseq2 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   284
by (Force_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   285
qed "MGT_BodyN";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   286
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   287
(* requires BodyN, com_det *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   288
Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   289
by (res_inst_tac [("P","%G ts. G||-ts"),("U","dom body")] nesting_lemma 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   290
by (etac hoare_derivs.asm 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   291
by (etac MGT_BodyN 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   292
by (rtac finite_dom_body 3);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   293
by (etac MGF_lemma1 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   294
by (assume_tac 2);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   295
by       (Blast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   296
by      (Clarsimp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   297
by     (eatac WT_bodiesD 1 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   298
by (rtac le_refl 3);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   299
by    Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   300
qed "MGF";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   301
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   302
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   303
(* Version: simultaneous recursion in call rule *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   304
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   305
(* finiteness not really necessary here *)
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   306
Goalw [MGT_def]     "[| G Un (%pn. {=}.      BODY pn  .{->})`Procs \
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   307
\                         ||-(%pn. {=}. the (body pn) .{->})`Procs; \
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   308
\ finite Procs |] ==>   G ||-(%pn. {=}.      BODY pn  .{->})`Procs";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   309
by (rtac hoare_derivs.Body 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   310
by (etac finite_pointwise 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   311
by (assume_tac 2);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   312
by (Clarify_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   313
by (etac conseq2 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   314
by Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   315
qed "MGT_Body";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   316
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   317
(* requires empty, insert, com_det *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   318
Goal "[| state_not_singleton; WT_bodies; \
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   319
\ F<=(%pn. {=}.the (body pn).{->})`dom body |] ==> \
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   320
\    (%pn. {=}.     BODY pn .{->})`dom body||-F";
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   321
by (ftac finite_subset 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   322
by (rtac (finite_dom_body RS finite_imageI) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   323
by (rotate_tac 2 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   324
by (make_imp_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   325
by (etac finite_induct 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   326
by  (ALLGOALS (clarsimp_tac (
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   327
        claset() addSIs [hoare_derivs.empty,hoare_derivs.insert],
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   328
        simpset() delsimps [range_composition])));
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   329
by (etac MGF_lemma1 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   330
by  (fast_tac (claset() addDs [WT_bodiesD]) 2);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   331
by (Clarsimp_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   332
by (rtac hoare_derivs.asm 1);
13911
f5c3750292f5 added thm"..." due to new Map.thy
nipkow
parents: 13612
diff changeset
   333
by (fast_tac (claset() addIs [(thm"domI")]) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   334
qed_spec_mp "MGF_lemma2_simult";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   335
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   336
(* requires Body, empty, insert, com_det *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   337
Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   338
by (rtac MGF_lemma1 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   339
by (assume_tac 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   340
by (assume_tac 2);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   341
by (Clarsimp_tac 1);
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9078
diff changeset
   342
by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})`dom body" 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   343
by (etac hoare_derivs.weaken 1);
13911
f5c3750292f5 added thm"..." due to new Map.thy
nipkow
parents: 13612
diff changeset
   344
by  (fast_tac (claset() addIs [(thm"domI")]) 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   345
by (rtac (finite_dom_body RSN (2,MGT_Body)) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   346
by (Simp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   347
by (eatac MGF_lemma2_simult 1 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   348
by (rtac subset_refl 1);
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 12486
diff changeset
   349
qed "MGF'";
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   350
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   351
(* requires Body+empty+insert / BodyN, com_det *)
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13911
diff changeset
   352
bind_thm ("hoare_complete", MGF' RS MGF_complete);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   353
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   354
section "unused derived rules";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   355
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   356
Goal "G|-{%Z s. False}.c.{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   357
by (rtac hoare_derivs.conseq 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   358
by (Fast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   359
qed "falseE";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   360
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   361
Goal "G|-{P}.c.{%Z s. True}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   362
by (rtac hoare_derivs.conseq 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   363
by (fast_tac (claset() addSIs [falseE]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   364
qed "trueI";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   365
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   366
Goal "[| G|-{P}.c.{Q}; G|-{P'}.c.{Q'} |] \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   367
\       ==> G|-{%Z s. P Z s | P' Z s}.c.{%Z s. Q Z s | Q' Z s}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   368
by (rtac hoare_derivs.conseq 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   369
by (fast_tac (claset() addEs [conseq12]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   370
qed "disj"; (* analogue conj non-derivable *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   371
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   372
Goal "(!Z s. P Z s --> Q Z s) ==> G|-{P}. SKIP .{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   373
by (rtac conseq12 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   374
by (rtac hoare_derivs.Skip 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   375
by (Fast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   376
qed "hoare_SkipI";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   377
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   378
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   379
section "useful derived rules";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   380
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   381
Goal "{t}|-t";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   382
by (rtac hoare_derivs.asm 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   383
by (rtac subset_refl 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   384
qed "single_asm";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   385
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   386
Goal "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   387
by (rtac hoare_derivs.conseq 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   388
by (Clarsimp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   389
by (cut_facts_tac (premises()) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   390
by (Fast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   391
qed "export_s";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   392
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   393
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   394
Goal "[| G|-{P}. c .{Q}; !k Z s. Q Z s --> Q Z (s[Loc Y::=k]) |] ==> \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   395
\   G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   396
by (rtac export_s 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   397
by (rtac hoare_derivs.Local 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   398
by (etac conseq2 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 10834
diff changeset
   399
by (etac spec 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   400
qed "weak_Local";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   401
11132
09622301ca07 added trial proof
oheimb
parents: 10962
diff changeset
   402
(*
09622301ca07 added trial proof
oheimb
parents: 10962
diff changeset
   403
Goal "!Q. G |-{%Z s. ~(? s'. <c,s> -c-> s')}. c .{Q}";
09622301ca07 added trial proof
oheimb
parents: 10962
diff changeset
   404
by (induct_tac "c" 1);
12486
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11132
diff changeset
   405
by Auto_tac;
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11132
diff changeset
   406
by (rtac conseq1 1);
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11132
diff changeset
   407
by (rtac hoare_derivs.Skip 1);
11132
09622301ca07 added trial proof
oheimb
parents: 10962
diff changeset
   408
force 1;
12486
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11132
diff changeset
   409
by (rtac conseq1 1);
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11132
diff changeset
   410
by (rtac hoare_derivs.Ass 1);
11132
09622301ca07 added trial proof
oheimb
parents: 10962
diff changeset
   411
force 1;
09622301ca07 added trial proof
oheimb
parents: 10962
diff changeset
   412
by (defer_tac 1);
09622301ca07 added trial proof
oheimb
parents: 10962
diff changeset
   413
###
12486
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11132
diff changeset
   414
by (rtac hoare_derivs.Comp 1);
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11132
diff changeset
   415
by (dtac spec 2);
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11132
diff changeset
   416
by (dtac spec 2);
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11132
diff changeset
   417
by (assume_tac 2);
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11132
diff changeset
   418
by (etac conseq1 2);
11132
09622301ca07 added trial proof
oheimb
parents: 10962
diff changeset
   419
by (Clarsimp_tac 2);
09622301ca07 added trial proof
oheimb
parents: 10962
diff changeset
   420
force 1;
09622301ca07 added trial proof
oheimb
parents: 10962
diff changeset
   421
*)