--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Mon Oct 21 23:45:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Tue Oct 22 14:17:12 2013 +0200
@@ -31,7 +31,10 @@
{prems: thm list, context: Proof.context} -> tactic
val mk_in_bd_tac: int -> thm -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm ->
- thm -> {prems: 'a, context: Proof.context} -> tactic
+ thm -> {prems: thm list, context: Proof.context} -> tactic
+
+ val mk_trivial_wit_tac: thm list -> thm list -> {prems: thm list, context: Proof.context} ->
+ tactic
end;
structure BNF_Def_Tactics : BNF_DEF_TACTICS =
@@ -302,4 +305,8 @@
map_comp RS sym, map_id])] 1
end;
+fun mk_trivial_wit_tac wit_defs set_maps {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt wit_defs THEN HEADGOAL (EVERY' (map (fn thm =>
+ dtac (thm RS equalityD1 RS set_mp) THEN' etac imageE THEN' atac) set_maps)) THEN ALLGOALS atac;
+
end;