src/HOL/IMP/VC.ML
author nipkow
Tue Jan 23 10:59:35 1996 +0100 (1996-01-23)
changeset 1447 bc2c0acbbf29
child 1451 6803ecb9b198
permissions -rw-r--r--
Added a verified verification-condition generator.
nipkow@1447
     1
(*  Title: 	HOL/IMP/VC.ML
nipkow@1447
     2
    ID:         $Id$
nipkow@1447
     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@1447
    11
val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[fast_tac HOL_cs 1]);
nipkow@1447
    12
nipkow@1447
    13
goal VC.thy "!Q. (!s. vc c Q s) --> ({{wp c Q}} (astrip c) {{Q}})";
nipkow@1447
    14
by(acom.induct_tac "c" 1);
nipkow@1447
    15
    by(ALLGOALS Simp_tac);
nipkow@1447
    16
    by(fast_tac (HOL_cs addIs hoare.intrs) 1);
nipkow@1447
    17
   by(fast_tac (HOL_cs addIs hoare.intrs) 1);
nipkow@1447
    18
  by(fast_tac (HOL_cs addIs hoare.intrs) 1);
nipkow@1447
    19
 (* if *)
nipkow@1447
    20
 br allI 1;
nipkow@1447
    21
 br impI 1;
nipkow@1447
    22
 brs hoare.intrs 1;
nipkow@1447
    23
  brs hoare.intrs 1;
nipkow@1447
    24
    by(fast_tac HOL_cs 2);
nipkow@1447
    25
   by(fast_tac HOL_cs 1);
nipkow@1447
    26
  by(fast_tac HOL_cs 1);
nipkow@1447
    27
 brs hoare.intrs 1;
nipkow@1447
    28
   by(fast_tac HOL_cs 2);
nipkow@1447
    29
  by(fast_tac HOL_cs 1);
nipkow@1447
    30
 by(fast_tac HOL_cs 1);
nipkow@1447
    31
(* while *)
nipkow@1447
    32
by(safe_tac HOL_cs);
nipkow@1447
    33
brs hoare.intrs 1;
nipkow@1447
    34
  br lemma 1;
nipkow@1447
    35
 brs hoare.intrs 1;
nipkow@1447
    36
 brs hoare.intrs 1;
nipkow@1447
    37
   by(fast_tac HOL_cs 2);
nipkow@1447
    38
  by(ALLGOALS(fast_tac HOL_cs));
nipkow@1447
    39
qed "vc_sound";
nipkow@1447
    40
nipkow@1447
    41
goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)";
nipkow@1447
    42
by(acom.induct_tac "c" 1);
nipkow@1447
    43
    by(ALLGOALS Asm_simp_tac);
nipkow@1447
    44
by(EVERY1[rtac allI, rtac allI, rtac impI]);
nipkow@1447
    45
by(EVERY1[etac allE, etac allE, etac mp]);
nipkow@1447
    46
by(EVERY1[etac allE, etac allE, etac mp, atac]);
nipkow@1447
    47
bind_thm("wp_mono", result() RS spec RS spec RS mp RS spec RS mp);
nipkow@1447
    48
nipkow@1447
    49
goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
nipkow@1447
    50
by(acom.induct_tac "c" 1);
nipkow@1447
    51
    by(ALLGOALS Asm_simp_tac);
nipkow@1447
    52
by(safe_tac HOL_cs);
nipkow@1447
    53
by(EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
nipkow@1447
    54
by(fast_tac (HOL_cs addEs [wp_mono]) 1);
nipkow@1447
    55
bind_thm("vc_mono", result() RS spec RS spec RS mp RS spec RS mp);
nipkow@1447
    56
nipkow@1447
    57
goal VC.thy
nipkow@1447
    58
  "!P c Q. ({{P}}c{{Q}}) --> \
nipkow@1447
    59
\          (? ac. astrip ac = c & (!s. P s --> wp ac Q s) & (!s. vc ac Q s))";
nipkow@1447
    60
br hoare.mutual_induct 1;
nipkow@1447
    61
     by(res_inst_tac [("x","Askip")] exI 1);
nipkow@1447
    62
     by(Simp_tac 1);
nipkow@1447
    63
    by(res_inst_tac [("x","Aass x a")] exI 1);
nipkow@1447
    64
    by(Simp_tac 1);
nipkow@1447
    65
   by(SELECT_GOAL(safe_tac HOL_cs)1);
nipkow@1447
    66
   by(res_inst_tac [("x","Asemi ac aca")] exI 1);
nipkow@1447
    67
   by(Asm_simp_tac 1);
nipkow@1447
    68
   by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
nipkow@1447
    69
  by(SELECT_GOAL(safe_tac HOL_cs)1);
nipkow@1447
    70
  by(res_inst_tac [("x","Aif b ac aca")] exI 1);
nipkow@1447
    71
  by(Asm_simp_tac 1);
nipkow@1447
    72
 by(SELECT_GOAL(safe_tac HOL_cs)1);
nipkow@1447
    73
 by(res_inst_tac [("x","Awhile b P ac")] exI 1);
nipkow@1447
    74
 by(Asm_simp_tac 1);
nipkow@1447
    75
by(SELECT_GOAL(safe_tac HOL_cs)1);
nipkow@1447
    76
by(res_inst_tac [("x","ac")] exI 1);
nipkow@1447
    77
by(Asm_simp_tac 1);
nipkow@1447
    78
by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
nipkow@1447
    79
qed "vc_complete";