src/HOL/IMP/VC.ML
author paulson
Thu Aug 06 15:48:13 1998 +0200 (1998-08-06)
changeset 5278 a903b66822e2
parent 5223 4cb05273f764
permissions -rw-r--r--
even more tidying of Goal commands
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@1973
     9
AddIs hoare.intrs;
nipkow@1973
    10
wenzelm@3842
    11
val lemma = prove_goal HOL.thy "!s. P s --> P s" (K[Fast_tac 1]);
nipkow@1447
    12
wenzelm@5069
    13
Goal "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}";
berghofe@5183
    14
by (induct_tac "c" 1);
paulson@2055
    15
    by (ALLGOALS Simp_tac);
paulson@2055
    16
    by (Fast_tac 1);
paulson@2055
    17
   by (Fast_tac 1);
paulson@2055
    18
  by (Fast_tac 1);
nipkow@1447
    19
 (* if *)
paulson@2055
    20
 by (Deepen_tac 4 1);
nipkow@1447
    21
(* while *)
paulson@2031
    22
by (safe_tac HOL_cs);
clasohm@1465
    23
by (resolve_tac hoare.intrs 1);
paulson@2055
    24
  by (rtac lemma 1);
paulson@2055
    25
 by (resolve_tac hoare.intrs 1);
paulson@2055
    26
 by (resolve_tac hoare.intrs 1);
paulson@2055
    27
   by (ALLGOALS(fast_tac HOL_cs));
nipkow@1447
    28
qed "vc_sound";
nipkow@1447
    29
wenzelm@5069
    30
Goal "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)";
berghofe@5183
    31
by (induct_tac "c" 1);
paulson@2055
    32
    by (ALLGOALS Asm_simp_tac);
paulson@2031
    33
by (EVERY1[rtac allI, rtac allI, rtac impI]);
paulson@2031
    34
by (EVERY1[etac allE, etac allE, etac mp]);
paulson@2031
    35
by (EVERY1[etac allE, etac allE, etac mp, atac]);
nipkow@2810
    36
qed_spec_mp "awp_mono";
nipkow@1447
    37
wenzelm@5069
    38
Goal "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
berghofe@5183
    39
by (induct_tac "c" 1);
paulson@2055
    40
    by (ALLGOALS Asm_simp_tac);
paulson@2031
    41
by (safe_tac HOL_cs);
paulson@2031
    42
by (EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
nipkow@2810
    43
by (fast_tac (HOL_cs addEs [awp_mono]) 1);
nipkow@1486
    44
qed_spec_mp "vc_mono";
nipkow@1447
    45
paulson@5278
    46
Goal "|- {P}c{Q} ==> \
nipkow@5117
    47
\  (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))";
paulson@1743
    48
by (etac hoare.induct 1);
paulson@2055
    49
     by (res_inst_tac [("x","Askip")] exI 1);
paulson@2055
    50
     by (Simp_tac 1);
paulson@2055
    51
    by (res_inst_tac [("x","Aass x a")] exI 1);
paulson@2055
    52
    by (Simp_tac 1);
paulson@2055
    53
   by (SELECT_GOAL(safe_tac HOL_cs)1);
paulson@2055
    54
   by (res_inst_tac [("x","Asemi ac aca")] exI 1);
paulson@2055
    55
   by (Asm_simp_tac 1);
nipkow@2810
    56
   by (fast_tac (HOL_cs addSEs [awp_mono,vc_mono]) 1);
paulson@2055
    57
  by (SELECT_GOAL(safe_tac HOL_cs)1);
paulson@2055
    58
  by (res_inst_tac [("x","Aif b ac aca")] exI 1);
paulson@2055
    59
  by (Asm_simp_tac 1);
paulson@2055
    60
 by (SELECT_GOAL(safe_tac HOL_cs)1);
nipkow@5117
    61
 by (res_inst_tac [("x","Awhile b P ac")] exI 1);
paulson@2055
    62
 by (Asm_simp_tac 1);
paulson@1743
    63
by (safe_tac HOL_cs);
paulson@2031
    64
by (res_inst_tac [("x","ac")] exI 1);
paulson@2031
    65
by (Asm_simp_tac 1);
nipkow@2810
    66
by (fast_tac (HOL_cs addSEs [awp_mono,vc_mono]) 1);
paulson@1743
    67
qed "vc_complete";
nipkow@1451
    68
wenzelm@5069
    69
Goal "!Q. vcawp c Q = (vc c Q, awp c Q)";
berghofe@5183
    70
by (induct_tac "c" 1);
wenzelm@4089
    71
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def])));
nipkow@2810
    72
qed "vcawp_vc_awp";