src/HOL/IMP/Hoare.ML
author nipkow
Tue Mar 07 14:57:37 1995 +0100 (1995-03-07)
changeset 936 a6d7b4084761
child 938 621be7ec81d7
permissions -rw-r--r--
Hoare logic
nipkow@936
     1
(*  Title: 	HOL/IMP/Hoare.ML
nipkow@936
     2
    ID:
nipkow@936
     3
    Author: 	Tobias Nipkow
nipkow@936
     4
    Copyright   1995 TUM
nipkow@936
     5
nipkow@936
     6
Derivation of Hoare rules
nipkow@936
     7
*)
nipkow@936
     8
nipkow@936
     9
open Hoare;
nipkow@936
    10
nipkow@936
    11
Unify.trace_bound := 30;
nipkow@936
    12
Unify.search_bound := 30;
nipkow@936
    13
nipkow@936
    14
goalw Hoare.thy [spec_def]
nipkow@936
    15
  "!!P.[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] \
nipkow@936
    16
\  ==> {{P'}}c{{Q'}}";
nipkow@936
    17
by(fast_tac HOL_cs 1);
nipkow@936
    18
bind_thm("hoare_conseq", impI RSN (3,allI RSN (3,impI RS allI RS result())));
nipkow@936
    19
nipkow@936
    20
goalw Hoare.thy (spec_def::C_simps)  "{{P}} skip {{P}}";
nipkow@936
    21
by(fast_tac comp_cs 1);
nipkow@936
    22
qed"hoare_skip";
nipkow@936
    23
nipkow@936
    24
goalw Hoare.thy (spec_def::C_simps)
nipkow@936
    25
  "!!P. [| !s. P s --> Q(s[A a s/x]) |] ==> {{P}} x := a {{Q}}";
nipkow@936
    26
by(asm_full_simp_tac prod_ss 1);
nipkow@936
    27
qed"hoare_assign";
nipkow@936
    28
nipkow@936
    29
goalw Hoare.thy (spec_def::C_simps)
nipkow@936
    30
  "!!P. [| {{P}} c {{Q}}; {{Q}} d {{R}} |] ==> {{P}} c;d {{R}}";
nipkow@936
    31
by(fast_tac comp_cs 1);
nipkow@936
    32
qed"hoare_seq";
nipkow@936
    33
nipkow@936
    34
goalw Hoare.thy (spec_def::C_simps)
nipkow@936
    35
  "!!P. [| {{%s. P s & B b s}} c {{Q}}; {{%s. P s & ~B b s}} d {{Q}} |] ==> \
nipkow@936
    36
\  {{P}} ifc b then c else d {{Q}}";
nipkow@936
    37
by(simp_tac prod_ss 1);
nipkow@936
    38
by(fast_tac comp_cs 1);
nipkow@936
    39
qed"hoare_if";
nipkow@936
    40
nipkow@936
    41
val major::prems = goal Hoare.thy
nipkow@936
    42
  "[| <a,b> :lfp f; mono f; \
nipkow@936
    43
\     !!a b. <a,b> : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
nipkow@936
    44
by(res_inst_tac [("c1","P")] (split RS subst) 1);
nipkow@936
    45
br (major RS induct) 1;
nipkow@936
    46
brs prems 1;
nipkow@936
    47
by(res_inst_tac[("p","x")]PairE 1);
nipkow@936
    48
by(hyp_subst_tac 1);
nipkow@936
    49
by(asm_simp_tac (prod_ss addsimps prems) 1);
nipkow@936
    50
qed"induct2";
nipkow@936
    51
nipkow@936
    52
goalw Hoare.thy (spec_def::C_simps)
nipkow@936
    53
  "!!P. [| {{%s. P s & B b s}} c {{P}} |] ==> \
nipkow@936
    54
\  {{P}} while b do c {{%s. P s & ~B b s}}";
nipkow@936
    55
br allI 1;
nipkow@936
    56
br allI 1;
nipkow@936
    57
br impI 1;
nipkow@936
    58
be induct2 1;
nipkow@936
    59
br Gamma_mono 1;
nipkow@936
    60
by (rewrite_goals_tac [Gamma_def]);  
nipkow@936
    61
by(eres_inst_tac [("x","a")] allE 1);
nipkow@936
    62
by (safe_tac comp_cs);
nipkow@936
    63
by(ALLGOALS(asm_full_simp_tac prod_ss));
nipkow@936
    64
qed"hoare_while";
nipkow@936
    65
nipkow@936
    66
fun while_tac inv ss i =
nipkow@936
    67
  EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i,
nipkow@936
    68
        asm_full_simp_tac ss (i+1)];
nipkow@936
    69
nipkow@936
    70
fun assign_tac ss = EVERY'[rtac hoare_assign, simp_tac ss,
nipkow@936
    71
                           TRY o (strip_tac THEN' atac)];
nipkow@936
    72
nipkow@936
    73
fun hoare_tac ss =
nipkow@936
    74
  REPEAT(STATE(fn th => FIRST'[rtac hoare_seq, assign_tac ss] (nprems_of th)));
nipkow@936
    75
nipkow@936
    76
(* example *)
nipkow@936
    77
val prems = goal Hoare.thy
nipkow@936
    78
  "[| u ~= y; u ~= z; y ~= z |] ==> \
nipkow@936
    79
\  {{%s.s(x)=i & s(y)=j}} \
nipkow@936
    80
\  z := X x; (u := N 0; \
nipkow@936
    81
\  while noti(ROp op = (X u) (X y)) \
nipkow@936
    82
\             do (u := Op1 Suc (X u); z := Op1 Suc (X z))) \
nipkow@936
    83
\  {{%s. s(z)=i+j}}";
nipkow@936
    84
val ss = arith_ss addsimps (eq_sym_conv::assign_def::prems@A_simps@B_simps);
nipkow@936
    85
by(hoare_tac ss);
nipkow@936
    86
by(while_tac "%s.s z = i + s u & s y = j" ss 3);
nipkow@936
    87
by(hoare_tac ss);
nipkow@936
    88
result();