src/HOL/IMP/Hoare.ML
author clasohm
Tue Jan 30 15:24:36 1996 +0100 (1996-01-30)
changeset 1465 5d7a7e439cec
parent 1447 bc2c0acbbf29
child 1481 03f096efa26d
permissions -rw-r--r--
expanded tabs
clasohm@1465
     1
(*  Title:      HOL/IMP/Hoare.ML
nipkow@938
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Tobias Nipkow
nipkow@936
     4
    Copyright   1995 TUM
nipkow@936
     5
nipkow@1447
     6
Soundness of Hoare rules wrt denotational semantics
nipkow@936
     7
*)
nipkow@936
     8
nipkow@936
     9
open Hoare;
nipkow@936
    10
nipkow@1447
    11
goalw Hoare.thy [spec_def] "!P c Q. ({{P}}c{{Q}}) --> spec P c Q";
clasohm@1465
    12
by (rtac hoare.mutual_induct 1);
nipkow@1447
    13
    by(ALLGOALS Asm_simp_tac);
nipkow@1447
    14
  by(fast_tac rel_cs 1);
nipkow@1447
    15
 by(fast_tac HOL_cs 1);
clasohm@1465
    16
by (rtac allI 1);
clasohm@1465
    17
by (rtac allI 1);
clasohm@1465
    18
by (rtac impI 1);
clasohm@1465
    19
by (etac induct2 1);
nipkow@1447
    20
 br Gamma_mono 1;
clasohm@1465
    21
by (rewtac Gamma_def);  
nipkow@936
    22
by(eres_inst_tac [("x","a")] allE 1);
nipkow@936
    23
by (safe_tac comp_cs);
nipkow@1447
    24
  by(ALLGOALS Asm_full_simp_tac);
nipkow@1447
    25
qed "hoare_sound";
nipkow@936
    26
nipkow@1447
    27
(*
nipkow@936
    28
fun while_tac inv ss i =
nipkow@936
    29
  EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i,
nipkow@936
    30
        asm_full_simp_tac ss (i+1)];
nipkow@936
    31
nipkow@936
    32
fun assign_tac ss = EVERY'[rtac hoare_assign, simp_tac ss,
nipkow@936
    33
                           TRY o (strip_tac THEN' atac)];
nipkow@936
    34
nipkow@936
    35
fun hoare_tac ss =
nipkow@936
    36
  REPEAT(STATE(fn th => FIRST'[rtac hoare_seq, assign_tac ss] (nprems_of th)));
nipkow@936
    37
nipkow@936
    38
(* example *)
nipkow@936
    39
val prems = goal Hoare.thy
nipkow@936
    40
  "[| u ~= y; u ~= z; y ~= z |] ==> \
nipkow@936
    41
\  {{%s.s(x)=i & s(y)=j}} \
nipkow@936
    42
\  z := X x; (u := N 0; \
nipkow@936
    43
\  while noti(ROp op = (X u) (X y)) \
nipkow@936
    44
\             do (u := Op1 Suc (X u); z := Op1 Suc (X z))) \
nipkow@936
    45
\  {{%s. s(z)=i+j}}";
clasohm@1266
    46
val ss = !simpset addsimps (eq_sym_conv::assign_def::prems);
nipkow@936
    47
by(hoare_tac ss);
nipkow@936
    48
by(while_tac "%s.s z = i + s u & s y = j" ss 3);
nipkow@936
    49
by(hoare_tac ss);
nipkow@936
    50
result();
nipkow@1447
    51
*)