made tactics more robust
authortraytel
Sun Dec 17 08:42:59 2017 +0100 (17 months ago)
changeset 6722219809bc9d7ff
parent 67221 62a5fbdded50
child 67223 711eec20aecd
made tactics more robust
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Sat Dec 16 22:32:04 2017 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Sun Dec 17 08:42:59 2017 +0100
     1.3 @@ -1904,7 +1904,8 @@
     1.4              Goal.prove_sorry lthy vars [] goal
     1.5                (fn {context = ctxt, prems = _} =>
     1.6                  HEADGOAL (rtac ctxt (pred_set RSN (2, pred_set RSN (2, box_equals)))) THEN
     1.7 -                unfold_thms_tac ctxt (@{thm Ball_image_comp} :: map Lazy.force set_map) THEN
     1.8 +                unfold_thms_tac ctxt
     1.9 +                  (@{thms Ball_image_comp ball_empty} @ map Lazy.force set_map) THEN
    1.10                  HEADGOAL (rtac ctxt refl))
    1.11              |> Thm.close_derivation
    1.12            end;
     2.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sat Dec 16 22:32:04 2017 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sun Dec 17 08:42:59 2017 +0100
     2.3 @@ -259,8 +259,11 @@
     2.4      (HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl) ORELSE
     2.5       REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) ::
     2.6         @{thms exE conjE CollectE}))) THEN
     2.7 -     HEADGOAL (hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt rel_map THEN HEADGOAL (rtac ctxt iffI) THEN
     2.8 -     last_tac iffD1 THEN last_tac iffD2)
     2.9 +     HEADGOAL (hyp_subst_tac ctxt) THEN
    2.10 +     REPEAT_DETERM (HEADGOAL (resolve_tac ctxt (maps (fn thm =>
    2.11 +       [thm RS trans, thm RS @{thm trans[rotated, OF sym]}]) rel_map))) THEN
    2.12 +     HEADGOAL (rtac ctxt iffI) THEN
    2.13 +     last_tac iffD1 THEN  print_tac ctxt "baz" THEN last_tac iffD2)
    2.14    end;
    2.15  
    2.16  fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =