# HG changeset patch # User wenzelm # Date 1608740165 -3600 # Node ID 9cc431444435c726d6e9b84d848804c73783c458 # Parent 8e99246f89c05aeed4a087764db1e6e819511074 clarified modules: avoid multiple uses of the same ML file; diff -r 8e99246f89c0 -r 9cc431444435 src/HOL/Hoare/Hoare_Logic.thy --- a/src/HOL/Hoare/Hoare_Logic.thy Wed Dec 23 15:20:52 2020 +0100 +++ b/src/HOL/Hoare/Hoare_Logic.thy Wed Dec 23 17:16:05 2020 +0100 @@ -10,7 +10,7 @@ *) theory Hoare_Logic -imports Main +imports Hoare_Tac begin type_synonym 'a bexp = "'a set" @@ -192,28 +192,35 @@ using assms(1) ValidTC_def by force qed -lemma Compl_Collect: "-(Collect b) = {x. \(b x)}" - by blast -lemmas AbortRule = SkipRule \ \dummy version\ -ML_file \hoare_tac.ML\ +declare BasicRule [Hoare_Tac.BasicRule] + and SkipRule [Hoare_Tac.SkipRule] + and SeqRule [Hoare_Tac.SeqRule] + and CondRule [Hoare_Tac.CondRule] + and WhileRule [Hoare_Tac.WhileRule] + +declare BasicRuleTC [Hoare_Tac.BasicRuleTC] + and SkipRuleTC [Hoare_Tac.SkipRuleTC] + and SeqRuleTC [Hoare_Tac.SeqRuleTC] + and CondRuleTC [Hoare_Tac.CondRuleTC] + and WhileRuleTC [Hoare_Tac.WhileRuleTC] method_setup vcg = \ - Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\ "verification condition generator" method_setup vcg_simp = \ Scan.succeed (fn ctxt => - SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\ + SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\ "verification condition generator plus simplification" method_setup vcg_tc = \ - Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\ "verification condition generator" method_setup vcg_tc_simp = \ Scan.succeed (fn ctxt => - SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\ + SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\ "verification condition generator plus simplification" end diff -r 8e99246f89c0 -r 9cc431444435 src/HOL/Hoare/Hoare_Logic_Abort.thy --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 15:20:52 2020 +0100 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 17:16:05 2020 +0100 @@ -7,7 +7,7 @@ *) theory Hoare_Logic_Abort -imports Main +imports Hoare_Tac begin type_synonym 'a bexp = "'a set" @@ -203,27 +203,35 @@ subsection \Derivation of the proof rules and, most importantly, the VCG tactic\ -lemma Compl_Collect: "-(Collect b) = {x. \(b x)}" - by blast +declare BasicRule [Hoare_Tac.BasicRule] + and SkipRule [Hoare_Tac.SkipRule] + and AbortRule [Hoare_Tac.AbortRule] + and SeqRule [Hoare_Tac.SeqRule] + and CondRule [Hoare_Tac.CondRule] + and WhileRule [Hoare_Tac.WhileRule] -ML_file \hoare_tac.ML\ +declare BasicRuleTC [Hoare_Tac.BasicRuleTC] + and SkipRuleTC [Hoare_Tac.SkipRuleTC] + and SeqRuleTC [Hoare_Tac.SeqRuleTC] + and CondRuleTC [Hoare_Tac.CondRuleTC] + and WhileRuleTC [Hoare_Tac.WhileRuleTC] method_setup vcg = \ - Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\ "verification condition generator" method_setup vcg_simp = \ Scan.succeed (fn ctxt => - SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\ + SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\ "verification condition generator plus simplification" method_setup vcg_tc = \ - Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\ "verification condition generator" method_setup vcg_tc_simp = \ Scan.succeed (fn ctxt => - SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\ + SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\ "verification condition generator plus simplification" \ \Special syntax for guarded statements and guarded array updates:\ diff -r 8e99246f89c0 -r 9cc431444435 src/HOL/Hoare/Hoare_Tac.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/Hoare_Tac.thy Wed Dec 23 17:16:05 2020 +0100 @@ -0,0 +1,35 @@ +(* Title: HOL/Hoare/Hoare_Tac.thy + Author: Leonor Prensa Nieto & Tobias Nipkow + Author: Walter Guttmann (extension to total-correctness proofs) + +Derivation of the proof rules and, most importantly, the VCG tactic. +*) + +theory Hoare_Tac + imports Main +begin + +context +begin + +qualified named_theorems BasicRule +qualified named_theorems SkipRule +qualified named_theorems AbortRule +qualified named_theorems SeqRule +qualified named_theorems CondRule +qualified named_theorems WhileRule + +qualified named_theorems BasicRuleTC +qualified named_theorems SkipRuleTC +qualified named_theorems SeqRuleTC +qualified named_theorems CondRuleTC +qualified named_theorems WhileRuleTC + +lemma Compl_Collect: "-(Collect b) = {x. \(b x)}" + by blast + +ML_file \hoare_tac.ML\ + +end + +end diff -r 8e99246f89c0 -r 9cc431444435 src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Wed Dec 23 15:20:52 2020 +0100 +++ b/src/HOL/Hoare/hoare_tac.ML Wed Dec 23 17:16:05 2020 +0100 @@ -5,7 +5,7 @@ Derivation of the proof rules and, most importantly, the VCG tactic. *) -signature HOARE = +signature HOARE_TAC = sig val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool -> int -> tactic @@ -13,7 +13,7 @@ val hoare_tc_tac: Proof.context -> (int -> tactic) -> int -> tactic end; -structure Hoare: HOARE = +structure Hoare_Tac: HOARE_TAC = struct (*** The tactics ***) @@ -77,7 +77,7 @@ in mk_vars pre end; fun mk_CollectC tm = - let val T as Type ("fun",[t,_]) = fastype_of tm; + let val Type ("fun",[t,_]) = fastype_of tm; in HOLogic.Collect_const t $ tm end; fun inclt ty = Const (\<^const_name>\Orderings.less_eq\, [ty,ty] ---> HOLogic.boolT); @@ -164,25 +164,26 @@ fun hoare_rule_tac ctxt (vars, Mlem) tac = let + val get_thms = Proof_Context.get_thms ctxt; val var_names = map (fst o dest_Free) vars; fun wlp_tac i = - resolve_tac ctxt @{thms SeqRule} i THEN rule_tac false (i + 1) + resolve_tac ctxt (get_thms \<^named_theorems>\SeqRule\) i THEN rule_tac false (i + 1) and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*) ((wlp_tac i THEN rule_tac pre_cond i) ORELSE (FIRST [ - resolve_tac ctxt @{thms SkipRule} i, - resolve_tac ctxt @{thms AbortRule} i, + resolve_tac ctxt (get_thms \<^named_theorems>\SkipRule\) i, + resolve_tac ctxt (get_thms \<^named_theorems>\AbortRule\) i, EVERY [ - resolve_tac ctxt @{thms BasicRule} i, + resolve_tac ctxt (get_thms \<^named_theorems>\BasicRule\) i, resolve_tac ctxt [Mlem] i, split_simp_tac ctxt i], EVERY [ - resolve_tac ctxt @{thms CondRule} i, + resolve_tac ctxt (get_thms \<^named_theorems>\CondRule\) i, rule_tac false (i + 2), rule_tac false (i + 1)], EVERY [ - resolve_tac ctxt @{thms WhileRule} i, + resolve_tac ctxt (get_thms \<^named_theorems>\WhileRule\) i, basic_simp_tac ctxt var_names tac (i + 2), rule_tac true (i + 1)]] THEN ( @@ -202,24 +203,25 @@ fun hoare_tc_rule_tac ctxt (vars, Mlem) tac = let + val get_thms = Proof_Context.get_thms ctxt; val var_names = map (fst o dest_Free) vars; fun wlp_tac i = - resolve_tac ctxt @{thms SeqRuleTC} i THEN rule_tac false (i + 1) + resolve_tac ctxt (get_thms \<^named_theorems>\SeqRuleTC\) i THEN rule_tac false (i + 1) and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*) ((wlp_tac i THEN rule_tac pre_cond i) ORELSE (FIRST [ - resolve_tac ctxt @{thms SkipRuleTC} i, + resolve_tac ctxt (get_thms \<^named_theorems>\SkipRuleTC\) i, EVERY [ - resolve_tac ctxt @{thms BasicRuleTC} i, + resolve_tac ctxt (get_thms \<^named_theorems>\BasicRuleTC\) i, resolve_tac ctxt [Mlem] i, split_simp_tac ctxt i], EVERY [ - resolve_tac ctxt @{thms CondRuleTC} i, + resolve_tac ctxt (get_thms \<^named_theorems>\CondRuleTC\) i, rule_tac false (i + 2), rule_tac false (i + 1)], EVERY [ - resolve_tac ctxt @{thms WhileRuleTC} i, + resolve_tac ctxt (get_thms \<^named_theorems>\WhileRuleTC\) i, basic_simp_tac ctxt var_names tac (i + 2), rule_tac true (i + 1)]] THEN ( @@ -232,4 +234,3 @@ SELECT_GOAL (hoare_tc_rule_tac ctxt (Mset ctxt goal) tac true 1) i); end; - diff -r 8e99246f89c0 -r 9cc431444435 src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Wed Dec 23 15:20:52 2020 +0100 +++ b/src/HOL/Isar_Examples/Hoare.thy Wed Dec 23 17:16:05 2020 +0100 @@ -7,7 +7,7 @@ section \Hoare Logic\ theory Hoare - imports Main + imports "HOL-Hoare.Hoare_Tac" begin subsection \Abstract syntax and semantics\ @@ -397,22 +397,16 @@ apply blast done -lemma Compl_Collect: "- Collect b = {x. \ b x}" - by blast - -lemmas AbortRule = SkipRule \ \dummy version\ -lemmas SeqRuleTC = SkipRule \ \dummy version\ -lemmas SkipRuleTC = SkipRule \ \dummy version\ -lemmas BasicRuleTC = SkipRule \ \dummy version\ -lemmas CondRuleTC = SkipRule \ \dummy version\ -lemmas WhileRuleTC = SkipRule \ \dummy version\ - -ML_file \~~/src/HOL/Hoare/hoare_tac.ML\ +declare BasicRule [Hoare_Tac.BasicRule] + and SkipRule [Hoare_Tac.SkipRule] + and SeqRule [Hoare_Tac.SeqRule] + and CondRule [Hoare_Tac.CondRule] + and WhileRule [Hoare_Tac.WhileRule] method_setup hoare = \Scan.succeed (fn ctxt => (SIMPLE_METHOD' - (Hoare.hoare_tac ctxt + (Hoare_Tac.hoare_tac ctxt (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] )))))\ "verification condition generator for Hoare logic" diff -r 8e99246f89c0 -r 9cc431444435 src/HOL/ROOT --- a/src/HOL/ROOT Wed Dec 23 15:20:52 2020 +0100 +++ b/src/HOL/ROOT Wed Dec 23 17:16:05 2020 +0100 @@ -709,6 +709,8 @@ Miscellaneous Isabelle/Isar examples. " options [quick_and_dirty] + sessions + "HOL-Hoare" theories Structured_Statements Basic_Logic