src/HOL/IMP/VC.ML
author paulson
Thu Sep 26 12:47:47 1996 +0200 (1996-09-26)
changeset 2031 03a843f0f447
parent 1973 8c94c9a5be10
child 2055 cc274e47f607
permissions -rw-r--r--
Ran expandshort
clasohm@1465
     1
(*  Title:      HOL/IMP/VC.ML
nipkow@1447
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Tobias Nipkow
nipkow@1447
     4
    Copyright   1996 TUM
nipkow@1447
     5
nipkow@1447
     6
Soundness and completeness of vc
nipkow@1447
     7
*)
nipkow@1447
     8
nipkow@1447
     9
open VC;
nipkow@1447
    10
nipkow@1973
    11
AddIs hoare.intrs;
nipkow@1973
    12
nipkow@1973
    13
val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[Fast_tac 1]);
nipkow@1447
    14
nipkow@1486
    15
goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}";
paulson@2031
    16
by (acom.induct_tac "c" 1);
nipkow@1447
    17
    by(ALLGOALS Simp_tac);
nipkow@1973
    18
    by(Fast_tac 1);
nipkow@1973
    19
   by(Fast_tac 1);
nipkow@1973
    20
  by(Fast_tac 1);
nipkow@1447
    21
 (* if *)
nipkow@1973
    22
 by(Deepen_tac 4 1);
nipkow@1447
    23
(* while *)
paulson@2031
    24
by (safe_tac HOL_cs);
clasohm@1465
    25
by (resolve_tac hoare.intrs 1);
nipkow@1447
    26
  br lemma 1;
nipkow@1447
    27
 brs hoare.intrs 1;
nipkow@1447
    28
 brs hoare.intrs 1;
nipkow@1973
    29
   by(ALLGOALS(fast_tac HOL_cs));
nipkow@1447
    30
qed "vc_sound";
nipkow@1447
    31
nipkow@1447
    32
goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)";
paulson@2031
    33
by (acom.induct_tac "c" 1);
nipkow@1447
    34
    by(ALLGOALS Asm_simp_tac);
paulson@2031
    35
by (EVERY1[rtac allI, rtac allI, rtac impI]);
paulson@2031
    36
by (EVERY1[etac allE, etac allE, etac mp]);
paulson@2031
    37
by (EVERY1[etac allE, etac allE, etac mp, atac]);
nipkow@1486
    38
qed_spec_mp "wp_mono";
nipkow@1447
    39
nipkow@1447
    40
goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
paulson@2031
    41
by (acom.induct_tac "c" 1);
nipkow@1447
    42
    by(ALLGOALS Asm_simp_tac);
paulson@2031
    43
by (safe_tac HOL_cs);
paulson@2031
    44
by (EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
paulson@2031
    45
by (fast_tac (HOL_cs addEs [wp_mono]) 1);
nipkow@1486
    46
qed_spec_mp "vc_mono";
nipkow@1447
    47
nipkow@1447
    48
goal VC.thy
paulson@1743
    49
  "!!P c Q. |- {P}c{Q} ==> \
nipkow@1940
    50
\          (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> wp ac Q s))";
paulson@1743
    51
by (etac hoare.induct 1);
nipkow@1447
    52
     by(res_inst_tac [("x","Askip")] exI 1);
nipkow@1447
    53
     by(Simp_tac 1);
nipkow@1447
    54
    by(res_inst_tac [("x","Aass x a")] exI 1);
nipkow@1447
    55
    by(Simp_tac 1);
nipkow@1447
    56
   by(SELECT_GOAL(safe_tac HOL_cs)1);
nipkow@1447
    57
   by(res_inst_tac [("x","Asemi ac aca")] exI 1);
nipkow@1447
    58
   by(Asm_simp_tac 1);
nipkow@1447
    59
   by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
nipkow@1447
    60
  by(SELECT_GOAL(safe_tac HOL_cs)1);
nipkow@1447
    61
  by(res_inst_tac [("x","Aif b ac aca")] exI 1);
nipkow@1447
    62
  by(Asm_simp_tac 1);
nipkow@1447
    63
 by(SELECT_GOAL(safe_tac HOL_cs)1);
paulson@1743
    64
 by(res_inst_tac [("x","Awhile b Pa ac")] exI 1);
nipkow@1447
    65
 by(Asm_simp_tac 1);
paulson@1743
    66
by (safe_tac HOL_cs);
paulson@2031
    67
by (res_inst_tac [("x","ac")] exI 1);
paulson@2031
    68
by (Asm_simp_tac 1);
paulson@2031
    69
by (fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
paulson@1743
    70
qed "vc_complete";
nipkow@1451
    71
nipkow@1451
    72
goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)";
paulson@2031
    73
by (acom.induct_tac "c" 1);
paulson@2031
    74
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def])));
nipkow@1451
    75
qed "vcwp_vc_wp";