--- 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. \<not>(b x)}"
- by blast
-lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close>
-ML_file \<open>hoare_tac.ML\<close>
+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 = \<open>
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close>
"verification condition generator"
method_setup vcg_simp = \<open>
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+ SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
"verification condition generator plus simplification"
method_setup vcg_tc = \<open>
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\<close>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close>
"verification condition generator"
method_setup vcg_tc_simp = \<open>
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+ SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
"verification condition generator plus simplification"
end
--- 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 \<open>Derivation of the proof rules and, most importantly, the VCG tactic\<close>
-lemma Compl_Collect: "-(Collect b) = {x. \<not>(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 \<open>hoare_tac.ML\<close>
+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 = \<open>
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close>
"verification condition generator"
method_setup vcg_simp = \<open>
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+ SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
"verification condition generator plus simplification"
method_setup vcg_tc = \<open>
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\<close>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close>
"verification condition generator"
method_setup vcg_tc_simp = \<open>
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+ SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
"verification condition generator plus simplification"
\<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close>
--- /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. \<not>(b x)}"
+ by blast
+
+ML_file \<open>hoare_tac.ML\<close>
+
+end
+
+end
--- 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>\<open>Orderings.less_eq\<close>, [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>\<open>SeqRule\<close>) 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>\<open>SkipRule\<close>) i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>AbortRule\<close>) i,
EVERY [
- resolve_tac ctxt @{thms BasicRule} i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>BasicRule\<close>) 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>\<open>CondRule\<close>) 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>\<open>WhileRule\<close>) 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>\<open>SeqRuleTC\<close>) 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>\<open>SkipRuleTC\<close>) i,
EVERY [
- resolve_tac ctxt @{thms BasicRuleTC} i,
+ resolve_tac ctxt (get_thms \<^named_theorems>\<open>BasicRuleTC\<close>) 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>\<open>CondRuleTC\<close>) 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>\<open>WhileRuleTC\<close>) 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;
-
--- 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 \<open>Hoare Logic\<close>
theory Hoare
- imports Main
+ imports "HOL-Hoare.Hoare_Tac"
begin
subsection \<open>Abstract syntax and semantics\<close>
@@ -397,22 +397,16 @@
apply blast
done
-lemma Compl_Collect: "- Collect b = {x. \<not> b x}"
- by blast
-
-lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close>
-lemmas SeqRuleTC = SkipRule \<comment> \<open>dummy version\<close>
-lemmas SkipRuleTC = SkipRule \<comment> \<open>dummy version\<close>
-lemmas BasicRuleTC = SkipRule \<comment> \<open>dummy version\<close>
-lemmas CondRuleTC = SkipRule \<comment> \<open>dummy version\<close>
-lemmas WhileRuleTC = SkipRule \<comment> \<open>dummy version\<close>
-
-ML_file \<open>~~/src/HOL/Hoare/hoare_tac.ML\<close>
+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 =
\<open>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"}] )))))\<close>
"verification condition generator for Hoare logic"
--- 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