--- a/src/HOL/Hoare/hoare_tac.ML Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Sat Jul 18 20:54:56 2015 +0200
@@ -132,9 +132,9 @@
fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
before_set2pred_simp_tac ctxt i THEN_MAYBE
EVERY [
- rtac subsetI i,
- rtac CollectI i,
- dtac CollectD i,
+ resolve_tac ctxt [subsetI] i,
+ resolve_tac ctxt [CollectI] i,
+ dresolve_tac ctxt [CollectD] i,
TRY (split_all_tac ctxt i) THEN_MAYBE
(rename_tac var_names i THEN
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
@@ -148,7 +148,8 @@
(*******************************************************************************)
fun max_simp_tac ctxt var_names tac =
- FIRST' [rtac subset_refl, set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
+ FIRST' [resolve_tac ctxt [subset_refl],
+ set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
fun basic_simp_tac ctxt var_names tac =
simp_tac
@@ -163,26 +164,28 @@
let
val var_names = map (fst o dest_Free) vars;
fun wlp_tac i =
- rtac @{thm SeqRule} i THEN rule_tac false (i + 1)
+ resolve_tac ctxt @{thms 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 [
- rtac @{thm SkipRule} i,
- rtac @{thm AbortRule} i,
+ resolve_tac ctxt @{thms SkipRule} i,
+ resolve_tac ctxt @{thms AbortRule} i,
EVERY [
- rtac @{thm BasicRule} i,
- rtac Mlem i,
+ resolve_tac ctxt @{thms BasicRule} i,
+ resolve_tac ctxt [Mlem] i,
split_simp_tac ctxt i],
EVERY [
- rtac @{thm CondRule} i,
+ resolve_tac ctxt @{thms CondRule} i,
rule_tac false (i + 2),
rule_tac false (i + 1)],
EVERY [
- rtac @{thm WhileRule} i,
+ resolve_tac ctxt @{thms WhileRule} i,
basic_simp_tac ctxt var_names tac (i + 2),
rule_tac true (i + 1)]]
- THEN (if pre_cond then basic_simp_tac ctxt var_names tac i else rtac subset_refl i)));
+ THEN (
+ if pre_cond then basic_simp_tac ctxt var_names tac i
+ else resolve_tac ctxt [subset_refl] i)));
in rule_tac end;