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