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