Hoare logic
authornipkow
Tue Mar 07 14:57:37 1995 +0100 (1995-03-07)
changeset 936a6d7b4084761
parent 935 a94ef3eed456
child 937 c7e599f524de
Hoare logic
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Hoare.thy
src/HOL/IMP/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/Hoare.ML	Tue Mar 07 14:57:37 1995 +0100
     1.3 @@ -0,0 +1,88 @@
     1.4 +(*  Title: 	HOL/IMP/Hoare.ML
     1.5 +    ID:
     1.6 +    Author: 	Tobias Nipkow
     1.7 +    Copyright   1995 TUM
     1.8 +
     1.9 +Derivation of Hoare rules
    1.10 +*)
    1.11 +
    1.12 +open Hoare;
    1.13 +
    1.14 +Unify.trace_bound := 30;
    1.15 +Unify.search_bound := 30;
    1.16 +
    1.17 +goalw Hoare.thy [spec_def]
    1.18 +  "!!P.[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] \
    1.19 +\  ==> {{P'}}c{{Q'}}";
    1.20 +by(fast_tac HOL_cs 1);
    1.21 +bind_thm("hoare_conseq", impI RSN (3,allI RSN (3,impI RS allI RS result())));
    1.22 +
    1.23 +goalw Hoare.thy (spec_def::C_simps)  "{{P}} skip {{P}}";
    1.24 +by(fast_tac comp_cs 1);
    1.25 +qed"hoare_skip";
    1.26 +
    1.27 +goalw Hoare.thy (spec_def::C_simps)
    1.28 +  "!!P. [| !s. P s --> Q(s[A a s/x]) |] ==> {{P}} x := a {{Q}}";
    1.29 +by(asm_full_simp_tac prod_ss 1);
    1.30 +qed"hoare_assign";
    1.31 +
    1.32 +goalw Hoare.thy (spec_def::C_simps)
    1.33 +  "!!P. [| {{P}} c {{Q}}; {{Q}} d {{R}} |] ==> {{P}} c;d {{R}}";
    1.34 +by(fast_tac comp_cs 1);
    1.35 +qed"hoare_seq";
    1.36 +
    1.37 +goalw Hoare.thy (spec_def::C_simps)
    1.38 +  "!!P. [| {{%s. P s & B b s}} c {{Q}}; {{%s. P s & ~B b s}} d {{Q}} |] ==> \
    1.39 +\  {{P}} ifc b then c else d {{Q}}";
    1.40 +by(simp_tac prod_ss 1);
    1.41 +by(fast_tac comp_cs 1);
    1.42 +qed"hoare_if";
    1.43 +
    1.44 +val major::prems = goal Hoare.thy
    1.45 +  "[| <a,b> :lfp f; mono f; \
    1.46 +\     !!a b. <a,b> : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
    1.47 +by(res_inst_tac [("c1","P")] (split RS subst) 1);
    1.48 +br (major RS induct) 1;
    1.49 +brs prems 1;
    1.50 +by(res_inst_tac[("p","x")]PairE 1);
    1.51 +by(hyp_subst_tac 1);
    1.52 +by(asm_simp_tac (prod_ss addsimps prems) 1);
    1.53 +qed"induct2";
    1.54 +
    1.55 +goalw Hoare.thy (spec_def::C_simps)
    1.56 +  "!!P. [| {{%s. P s & B b s}} c {{P}} |] ==> \
    1.57 +\  {{P}} while b do c {{%s. P s & ~B b s}}";
    1.58 +br allI 1;
    1.59 +br allI 1;
    1.60 +br impI 1;
    1.61 +be induct2 1;
    1.62 +br Gamma_mono 1;
    1.63 +by (rewrite_goals_tac [Gamma_def]);  
    1.64 +by(eres_inst_tac [("x","a")] allE 1);
    1.65 +by (safe_tac comp_cs);
    1.66 +by(ALLGOALS(asm_full_simp_tac prod_ss));
    1.67 +qed"hoare_while";
    1.68 +
    1.69 +fun while_tac inv ss i =
    1.70 +  EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i,
    1.71 +        asm_full_simp_tac ss (i+1)];
    1.72 +
    1.73 +fun assign_tac ss = EVERY'[rtac hoare_assign, simp_tac ss,
    1.74 +                           TRY o (strip_tac THEN' atac)];
    1.75 +
    1.76 +fun hoare_tac ss =
    1.77 +  REPEAT(STATE(fn th => FIRST'[rtac hoare_seq, assign_tac ss] (nprems_of th)));
    1.78 +
    1.79 +(* example *)
    1.80 +val prems = goal Hoare.thy
    1.81 +  "[| u ~= y; u ~= z; y ~= z |] ==> \
    1.82 +\  {{%s.s(x)=i & s(y)=j}} \
    1.83 +\  z := X x; (u := N 0; \
    1.84 +\  while noti(ROp op = (X u) (X y)) \
    1.85 +\             do (u := Op1 Suc (X u); z := Op1 Suc (X z))) \
    1.86 +\  {{%s. s(z)=i+j}}";
    1.87 +val ss = arith_ss addsimps (eq_sym_conv::assign_def::prems@A_simps@B_simps);
    1.88 +by(hoare_tac ss);
    1.89 +by(while_tac "%s.s z = i + s u & s y = j" ss 3);
    1.90 +by(hoare_tac ss);
    1.91 +result();
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IMP/Hoare.thy	Tue Mar 07 14:57:37 1995 +0100
     2.3 @@ -0,0 +1,14 @@
     2.4 +(*  Title: 	HOL/IMP/Hoare.thy
     2.5 +    ID:
     2.6 +    Author: 	Tobias Nipkow
     2.7 +    Copyright   1995 TUM
     2.8 +
     2.9 +Semantic embedding of Hoare logic
    2.10 +*)
    2.11 +
    2.12 +Hoare = Denotation +
    2.13 +consts
    2.14 +  spec:: "[state=>bool,com,state=>bool] => bool" ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
    2.15 +defs
    2.16 +  spec_def "spec P c Q == !s t. <s,t> : C(c) --> P s --> Q t"
    2.17 +end
     3.1 --- a/src/HOL/IMP/ROOT.ML	Tue Mar 07 13:37:48 1995 +0100
     3.2 +++ b/src/HOL/IMP/ROOT.ML	Tue Mar 07 14:57:37 1995 +0100
     3.3 @@ -1,11 +1,13 @@
     3.4  (*  Title: 	CHOL/IMP/ROOT.ML
     3.5      ID:         $Id$
     3.6 -    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     3.7 -    Copyright   1994 TUM
     3.8 +    Author: 	Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
     3.9 +    Copyright   1995 TUM
    3.10  
    3.11 -Executes the formalization of the denotational and operational semantics of a
    3.12 -simple while-language, including an equivalence proof. The whole development
    3.13 -essentially formalizes/transcribes chapters 2 and 5 of
    3.14 +The formalization of the denotational, operational and axiomatic semantics of
    3.15 +a simple while-language, including
    3.16 +(1) an equivalence proof between denotational and operational semantics and
    3.17 +(2) the derivation of the Hoare rules from the denotational semantics.
    3.18 +The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
    3.19  
    3.20  Glynn Winskel. The Formal Semantics of Programming Languages.
    3.21  MIT Press, 1993.
    3.22 @@ -19,3 +21,4 @@
    3.23  loadpath := [".","IMP"];
    3.24  time_use_thy "Properties";
    3.25  time_use_thy "Equiv";
    3.26 +time_use_thy "Hoare";