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