--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Sep 27 18:39:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Sep 27 18:58:15 2012 +0200
@@ -923,8 +923,7 @@
(*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
in
- Skip_Proof.prove lthy [] [] goal
- (fn {context = ctxt, ...} => mk_collect_set_natural_tac ctxt (#set_natural axioms))
+ Skip_Proof.prove lthy [] [] goal (K (mk_collect_set_natural_tac (#set_natural axioms)))
|> Thm.close_derivation
end;
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Sep 27 18:39:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Sep 27 18:58:15 2012 +0200
@@ -8,7 +8,7 @@
signature BNF_DEF_TACTICS =
sig
- val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic
+ val mk_collect_set_natural_tac: thm list -> tactic
val mk_id': thm -> thm
val mk_comp': thm -> thm
val mk_in_mono_tac: int -> tactic
@@ -44,8 +44,12 @@
((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
(etac subset_trans THEN' atac) 1;
-fun mk_collect_set_natural_tac ctxt set_naturals =
- substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1;
+fun mk_collect_set_natural_tac set_naturals =
+ (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
+ EVERY' (map (fn set_natural =>
+ rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
+ rtac set_natural) set_naturals) THEN'
+ rtac @{thm image_empty}) 1;
fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals =
if null set_naturals then
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Sep 27 18:39:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Sep 27 18:58:15 2012 +0200
@@ -14,7 +14,6 @@
val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
val fo_rtac: thm -> Proof.context -> int -> tactic
val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic
- val substs_tac: Proof.context -> thm list -> int -> tactic
val unfold_thms_tac: Proof.context -> thm list -> tactic
val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
@@ -62,7 +61,6 @@
(*unlike "unfold_thms_tac", these succeed when the RHS contains schematic variables not in the LHS*)
fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
-fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt NONE;
(* Theorems for open typedefs with UNIV as representing set *)