# HG changeset patch # User nipkow # Date 794584657 -3600 # Node ID a6d7b40847610cb68c2c6d13ad6775fd9541faa1 # Parent a94ef3eed456d3a0611fc2ddca1d799ba42a2b09 Hoare logic diff -r a94ef3eed456 -r a6d7b4084761 src/HOL/IMP/Hoare.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IMP/Hoare.ML Tue Mar 07 14:57:37 1995 +0100 @@ -0,0 +1,88 @@ +(* Title: HOL/IMP/Hoare.ML + ID: + Author: Tobias Nipkow + Copyright 1995 TUM + +Derivation of Hoare rules +*) + +open Hoare; + +Unify.trace_bound := 30; +Unify.search_bound := 30; + +goalw Hoare.thy [spec_def] + "!!P.[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] \ +\ ==> {{P'}}c{{Q'}}"; +by(fast_tac HOL_cs 1); +bind_thm("hoare_conseq", impI RSN (3,allI RSN (3,impI RS allI RS result()))); + +goalw Hoare.thy (spec_def::C_simps) "{{P}} skip {{P}}"; +by(fast_tac comp_cs 1); +qed"hoare_skip"; + +goalw Hoare.thy (spec_def::C_simps) + "!!P. [| !s. P s --> Q(s[A a s/x]) |] ==> {{P}} x := a {{Q}}"; +by(asm_full_simp_tac prod_ss 1); +qed"hoare_assign"; + +goalw Hoare.thy (spec_def::C_simps) + "!!P. [| {{P}} c {{Q}}; {{Q}} d {{R}} |] ==> {{P}} c;d {{R}}"; +by(fast_tac comp_cs 1); +qed"hoare_seq"; + +goalw Hoare.thy (spec_def::C_simps) + "!!P. [| {{%s. P s & B b s}} c {{Q}}; {{%s. P s & ~B b s}} d {{Q}} |] ==> \ +\ {{P}} ifc b then c else d {{Q}}"; +by(simp_tac prod_ss 1); +by(fast_tac comp_cs 1); +qed"hoare_if"; + +val major::prems = goal Hoare.thy + "[| :lfp f; mono f; \ +\ !!a b. : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b"; +by(res_inst_tac [("c1","P")] (split RS subst) 1); +br (major RS induct) 1; +brs prems 1; +by(res_inst_tac[("p","x")]PairE 1); +by(hyp_subst_tac 1); +by(asm_simp_tac (prod_ss addsimps prems) 1); +qed"induct2"; + +goalw Hoare.thy (spec_def::C_simps) + "!!P. [| {{%s. P s & B b s}} c {{P}} |] ==> \ +\ {{P}} while b do c {{%s. P s & ~B b s}}"; +br allI 1; +br allI 1; +br impI 1; +be induct2 1; +br Gamma_mono 1; +by (rewrite_goals_tac [Gamma_def]); +by(eres_inst_tac [("x","a")] allE 1); +by (safe_tac comp_cs); +by(ALLGOALS(asm_full_simp_tac prod_ss)); +qed"hoare_while"; + +fun while_tac inv ss i = + EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i, + asm_full_simp_tac ss (i+1)]; + +fun assign_tac ss = EVERY'[rtac hoare_assign, simp_tac ss, + TRY o (strip_tac THEN' atac)]; + +fun hoare_tac ss = + REPEAT(STATE(fn th => FIRST'[rtac hoare_seq, assign_tac ss] (nprems_of th))); + +(* example *) +val prems = goal Hoare.thy + "[| u ~= y; u ~= z; y ~= z |] ==> \ +\ {{%s.s(x)=i & s(y)=j}} \ +\ z := X x; (u := N 0; \ +\ while noti(ROp op = (X u) (X y)) \ +\ do (u := Op1 Suc (X u); z := Op1 Suc (X z))) \ +\ {{%s. s(z)=i+j}}"; +val ss = arith_ss addsimps (eq_sym_conv::assign_def::prems@A_simps@B_simps); +by(hoare_tac ss); +by(while_tac "%s.s z = i + s u & s y = j" ss 3); +by(hoare_tac ss); +result(); diff -r a94ef3eed456 -r a6d7b4084761 src/HOL/IMP/Hoare.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IMP/Hoare.thy Tue Mar 07 14:57:37 1995 +0100 @@ -0,0 +1,14 @@ +(* Title: HOL/IMP/Hoare.thy + ID: + Author: Tobias Nipkow + Copyright 1995 TUM + +Semantic embedding of Hoare logic +*) + +Hoare = Denotation + +consts + spec:: "[state=>bool,com,state=>bool] => bool" ("{{(1_)}}/ (_)/ {{(1_)}}" 10) +defs + spec_def "spec P c Q == !s t. : C(c) --> P s --> Q t" +end diff -r a94ef3eed456 -r a6d7b4084761 src/HOL/IMP/ROOT.ML --- a/src/HOL/IMP/ROOT.ML Tue Mar 07 13:37:48 1995 +0100 +++ b/src/HOL/IMP/ROOT.ML Tue Mar 07 14:57:37 1995 +0100 @@ -1,11 +1,13 @@ (* Title: CHOL/IMP/ROOT.ML ID: $Id$ - Author: Heiko Loetzbeyer & Robert Sandner, TUM - Copyright 1994 TUM + Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow + Copyright 1995 TUM -Executes the formalization of the denotational and operational semantics of a -simple while-language, including an equivalence proof. The whole development -essentially formalizes/transcribes chapters 2 and 5 of +The formalization of the denotational, operational and axiomatic semantics of +a simple while-language, including +(1) an equivalence proof between denotational and operational semantics and +(2) the derivation of the Hoare rules from the denotational semantics. +The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993. @@ -19,3 +21,4 @@ loadpath := [".","IMP"]; time_use_thy "Properties"; time_use_thy "Equiv"; +time_use_thy "Hoare";