src/HOL/Hoare/hoare_tac.ML
changeset 60754 02924903a6fd
parent 55661 ec14796cd140
child 61125 4c68426800de
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Sat Jul 18 20:53:05 2015 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Sat Jul 18 20:54:56 2015 +0200
     1.3 @@ -132,9 +132,9 @@
     1.4  fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
     1.5    before_set2pred_simp_tac ctxt i THEN_MAYBE
     1.6    EVERY [
     1.7 -    rtac subsetI i,
     1.8 -    rtac CollectI i,
     1.9 -    dtac CollectD i,
    1.10 +    resolve_tac ctxt [subsetI] i,
    1.11 +    resolve_tac ctxt [CollectI] i,
    1.12 +    dresolve_tac ctxt [CollectD] i,
    1.13      TRY (split_all_tac ctxt i) THEN_MAYBE
    1.14       (rename_tac var_names i THEN
    1.15        full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
    1.16 @@ -148,7 +148,8 @@
    1.17  (*******************************************************************************)
    1.18  
    1.19  fun max_simp_tac ctxt var_names tac =
    1.20 -  FIRST' [rtac subset_refl, set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
    1.21 +  FIRST' [resolve_tac ctxt [subset_refl],
    1.22 +    set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
    1.23  
    1.24  fun basic_simp_tac ctxt var_names tac =
    1.25    simp_tac
    1.26 @@ -163,26 +164,28 @@
    1.27    let
    1.28      val var_names = map (fst o dest_Free) vars;
    1.29      fun wlp_tac i =
    1.30 -      rtac @{thm SeqRule} i THEN rule_tac false (i + 1)
    1.31 +      resolve_tac ctxt @{thms SeqRule} i THEN rule_tac false (i + 1)
    1.32      and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
    1.33        ((wlp_tac i THEN rule_tac pre_cond i)
    1.34          ORELSE
    1.35          (FIRST [
    1.36 -          rtac @{thm SkipRule} i,
    1.37 -          rtac @{thm AbortRule} i,
    1.38 +          resolve_tac ctxt @{thms SkipRule} i,
    1.39 +          resolve_tac ctxt @{thms AbortRule} i,
    1.40            EVERY [
    1.41 -            rtac @{thm BasicRule} i,
    1.42 -            rtac Mlem i,
    1.43 +            resolve_tac ctxt @{thms BasicRule} i,
    1.44 +            resolve_tac ctxt [Mlem] i,
    1.45              split_simp_tac ctxt i],
    1.46            EVERY [
    1.47 -            rtac @{thm CondRule} i,
    1.48 +            resolve_tac ctxt @{thms CondRule} i,
    1.49              rule_tac false (i + 2),
    1.50              rule_tac false (i + 1)],
    1.51            EVERY [
    1.52 -            rtac @{thm WhileRule} i,
    1.53 +            resolve_tac ctxt @{thms WhileRule} i,
    1.54              basic_simp_tac ctxt var_names tac (i + 2),
    1.55              rule_tac true (i + 1)]]
    1.56 -         THEN (if pre_cond then basic_simp_tac ctxt var_names tac i else rtac subset_refl i)));
    1.57 +         THEN (
    1.58 +           if pre_cond then basic_simp_tac ctxt var_names tac i
    1.59 +           else resolve_tac ctxt [subset_refl] i)));
    1.60    in rule_tac end;
    1.61  
    1.62