src/HOL/IMP/VC.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2810 c4e16b36bc57
child 3842 b55686a7b22c
permissions -rw-r--r--
Dep. on Provers/nat_transitive
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@2810
    15
goal VC.thy "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}";
paulson@2031
    16
by (acom.induct_tac "c" 1);
paulson@2055
    17
    by (ALLGOALS Simp_tac);
paulson@2055
    18
    by (Fast_tac 1);
paulson@2055
    19
   by (Fast_tac 1);
paulson@2055
    20
  by (Fast_tac 1);
nipkow@1447
    21
 (* if *)
paulson@2055
    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);
paulson@2055
    26
  by (rtac lemma 1);
paulson@2055
    27
 by (resolve_tac hoare.intrs 1);
paulson@2055
    28
 by (resolve_tac hoare.intrs 1);
paulson@2055
    29
   by (ALLGOALS(fast_tac HOL_cs));
nipkow@1447
    30
qed "vc_sound";
nipkow@1447
    31
nipkow@2810
    32
goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)";
paulson@2031
    33
by (acom.induct_tac "c" 1);
paulson@2055
    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@2810
    38
qed_spec_mp "awp_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);
paulson@2055
    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]);
nipkow@2810
    45
by (fast_tac (HOL_cs addEs [awp_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@2810
    50
\          (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))";
paulson@1743
    51
by (etac hoare.induct 1);
paulson@2055
    52
     by (res_inst_tac [("x","Askip")] exI 1);
paulson@2055
    53
     by (Simp_tac 1);
paulson@2055
    54
    by (res_inst_tac [("x","Aass x a")] exI 1);
paulson@2055
    55
    by (Simp_tac 1);
paulson@2055
    56
   by (SELECT_GOAL(safe_tac HOL_cs)1);
paulson@2055
    57
   by (res_inst_tac [("x","Asemi ac aca")] exI 1);
paulson@2055
    58
   by (Asm_simp_tac 1);
nipkow@2810
    59
   by (fast_tac (HOL_cs addSEs [awp_mono,vc_mono]) 1);
paulson@2055
    60
  by (SELECT_GOAL(safe_tac HOL_cs)1);
paulson@2055
    61
  by (res_inst_tac [("x","Aif b ac aca")] exI 1);
paulson@2055
    62
  by (Asm_simp_tac 1);
paulson@2055
    63
 by (SELECT_GOAL(safe_tac HOL_cs)1);
paulson@2055
    64
 by (res_inst_tac [("x","Awhile b Pa ac")] exI 1);
paulson@2055
    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);
nipkow@2810
    69
by (fast_tac (HOL_cs addSEs [awp_mono,vc_mono]) 1);
paulson@1743
    70
qed "vc_complete";
nipkow@1451
    71
nipkow@2810
    72
goal VC.thy "!Q. vcawp c Q = (vc c Q, awp c Q)";
paulson@2031
    73
by (acom.induct_tac "c" 1);
paulson@2031
    74
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def])));
nipkow@2810
    75
qed "vcawp_vc_awp";