--- a/src/HOL/BNF/BNF.thy Wed Nov 20 20:18:53 2013 +0100
+++ b/src/HOL/BNF/BNF.thy Wed Nov 20 20:45:20 2013 +0100
@@ -10,7 +10,7 @@
header {* Bounded Natural Functors for (Co)datatypes *}
theory BNF
-imports Countable_Set_Type BNF_LFP BNF_GFP Coinduction
+imports Countable_Set_Type BNF_LFP BNF_GFP
begin
hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr
--- a/src/HOL/BNF/Coinduction.thy Wed Nov 20 20:18:53 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: HOL/BNF/Coinduction.thy
- Author: Johannes Hölzl, TU Muenchen
- Author: Dmitriy Traytel, TU Muenchen
- Copyright 2013
-
-Coinduction method that avoids some boilerplate compared to coinduct.
-*)
-
-header {* Coinduction Method *}
-
-theory Coinduction
-imports BNF_Util
-begin
-
-ML_file "Tools/coinduction.ML"
-
-setup Coinduction.setup
-
-end
--- a/src/HOL/BNF/README.html Wed Nov 20 20:18:53 2013 +0100
+++ b/src/HOL/BNF/README.html Wed Nov 20 20:45:20 2013 +0100
@@ -37,9 +37,10 @@
The key notion underlying the package is that of a <i>bounded natural functor</i>
(<i>BNF</i>)—an enriched type constructor satisfying specific properties
preserved by interesting categorical operations (composition, least fixed point,
-and greatest fixed point). The <tt>Basic_BNFs.thy</tt> and <tt>More_BNFs.thy</tt>
-files register various basic types, notably for sums, products, function spaces,
-finite sets, multisets, and countable sets. Custom BNFs can be registered as well.
+and greatest fixed point). The <tt>Basic_BNFs.thy</tt>, <tt>More_BNFs.thy</tt>,
+and <tt>Countable_Set_Type.thy</tt> files register various basic types, notably
+for sums, products, function spaces, finite sets, multisets, and countable sets.
+Custom BNFs can be registered as well.
<p>
<b>Warning:</b> The package is under development. Please contact any nonempty
--- a/src/HOL/BNF/Tools/bnf_util.ML Wed Nov 20 20:18:53 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_util.ML Wed Nov 20 20:45:20 2013 +0100
@@ -132,7 +132,6 @@
val no_refl: thm list -> thm list
val no_reflexive: thm list -> thm list
- val cterm_instantiate_pos: cterm option list -> thm -> thm
val fold_thms: Proof.context -> thm list -> thm -> thm
val parse_binding_colon: binding parser
@@ -140,14 +139,6 @@
val typedef: binding * (string * sort) list * mixfix -> term ->
(binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
-
- val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
- val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
- tactic
- val CONJ_WRAP_GEN: tactic -> ('a -> tactic) -> 'a list -> tactic
- val CONJ_WRAP_GEN': (int -> tactic) -> ('a -> int -> tactic) -> 'a list -> int -> tactic
- val CONJ_WRAP: ('a -> tactic) -> 'a list -> tactic
- val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic
end;
structure BNF_Util : BNF_UTIL =
@@ -276,25 +267,6 @@
((name, Typedef.transform_info phi info), lthy)
end;
-(*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
-fun WRAP gen_before gen_after xs core_tac =
- fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;
-
-fun WRAP' gen_before gen_after xs core_tac =
- fold_rev (fn x => fn tac => gen_before x THEN' tac THEN' gen_after x) xs core_tac;
-
-fun CONJ_WRAP_GEN conj_tac gen_tac xs =
- let val (butlast, last) = split_last xs;
- in WRAP (fn thm => conj_tac THEN gen_tac thm) (K all_tac) butlast (gen_tac last) end;
-
-fun CONJ_WRAP_GEN' conj_tac gen_tac xs =
- let val (butlast, last) = split_last xs;
- in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
-
-(*not eta-converted because of monotype restriction*)
-fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
-fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;
-
(* Term construction *)
@@ -600,17 +572,6 @@
val no_refl = filter_out is_refl;
val no_reflexive = filter_out Thm.is_reflexive;
-fun cterm_instantiate_pos cts thm =
- let
- val cert = Thm.cterm_of (Thm.theory_of_thm thm);
- val vars = Term.add_vars (prop_of thm) [];
- val vars' = rev (drop (length vars - length cts) vars);
- val ps = map_filter (fn (_, NONE) => NONE
- | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
- in
- Drule.cterm_instantiate ps thm
- end;
-
fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
end;
--- a/src/HOL/BNF/Tools/coinduction.ML Wed Nov 20 20:18:53 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,159 +0,0 @@
-(* Title: HOL/BNF/Tools/coinduction.ML
- Author: Johannes Hölzl, TU Muenchen
- Author: Dmitriy Traytel, TU Muenchen
- Copyright 2013
-
-Coinduction method that avoids some boilerplate compared to coinduct.
-*)
-
-signature COINDUCTION =
-sig
- val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
- val setup: theory -> theory
-end;
-
-structure Coinduction : COINDUCTION =
-struct
-
-open BNF_Util
-open BNF_Tactics
-
-fun filter_in_out _ [] = ([], [])
- | filter_in_out P (x :: xs) = (let
- val (ins, outs) = filter_in_out P xs;
- in
- if P x then (x :: ins, outs) else (ins, x :: outs)
- end);
-
-fun ALLGOALS_SKIP skip tac st =
- let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
- in doall (nprems_of st) st end;
-
-fun THEN_ALL_NEW_SKIP skip tac1 tac2 i st =
- st |> (tac1 i THEN (fn st' =>
- Seq.INTERVAL tac2 (i + skip) (i + nprems_of st' - nprems_of st) st'));
-
-fun DELETE_PREMS_AFTER skip tac i st =
- let
- val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
- in
- (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
- end;
-
-fun coinduction_tac ctxt raw_vars opt_raw_thm prems st =
- let
- val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
- fun find_coinduct t =
- Induct.find_coinductP ctxt t @
- (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
- val raw_thm = case opt_raw_thm
- of SOME raw_thm => raw_thm
- | NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd;
- val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
- val cases = Rule_Cases.get raw_thm |> fst
- in
- NO_CASES (HEADGOAL (
- Object_Logic.rulify_tac THEN'
- Method.insert_tac prems THEN'
- Object_Logic.atomize_prems_tac THEN'
- DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
- let
- val vars = raw_vars @ map (term_of o snd) params;
- val names_ctxt = ctxt
- |> fold Variable.declare_names vars
- |> fold Variable.declare_thm (raw_thm :: prems);
- val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
- val (rhoTs, rhots) = Thm.match (thm_concl, concl)
- |>> map (pairself typ_of)
- ||> map (pairself term_of);
- val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
- |> map (subst_atomic_types rhoTs);
- val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
- val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
- |>> (fn names => Variable.variant_fixes names names_ctxt) ;
- val eqs =
- map3 (fn name => fn T => fn (_, rhs) =>
- HOLogic.mk_eq (Free (name, T), rhs))
- names Ts raw_eqs;
- val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
- |> try (Library.foldr1 HOLogic.mk_conj)
- |> the_default @{term True}
- |> list_exists_free vars
- |> Term.map_abs_vars (Variable.revert_fixed ctxt)
- |> fold_rev Term.absfree (names ~~ Ts)
- |> certify ctxt;
- val thm = cterm_instantiate_pos [SOME phi] raw_thm;
- val e = length eqs;
- val p = length prems;
- in
- HEADGOAL (EVERY' [rtac thm,
- EVERY' (map (fn var =>
- rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
- if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
- else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
- K (ALLGOALS_SKIP skip
- (REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
- DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
- (case prems of
- [] => all_tac
- | inv::case_prems =>
- let
- val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
- val inv_thms = init @ [last];
- val eqs = take e inv_thms;
- fun is_local_var t =
- member (fn (t, (_, t')) => t aconv (term_of t')) params t;
- val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
- val assms = assms' @ drop e inv_thms
- in
- HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
- unfold_thms_tac ctxt eqs
- end)) ctxt)))])
- end) ctxt) THEN'
- K (prune_params_tac))) st
- |> Seq.maps (fn (_, st) =>
- CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
- end;
-
-local
-
-val ruleN = "rule"
-val arbitraryN = "arbitrary"
-fun single_rule [rule] = rule
- | single_rule _ = error "Single rule expected";
-
-fun named_rule k arg get =
- Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
- (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
- (case get (Context.proof_of context) name of SOME x => x
- | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
-
-fun rule get_type get_pred =
- named_rule Induct.typeN (Args.type_name false) get_type ||
- named_rule Induct.predN (Args.const false) get_pred ||
- named_rule Induct.setN (Args.const false) get_pred ||
- Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
-
-val coinduct_rule = rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;
-
-fun unless_more_args scan = Scan.unless (Scan.lift
- ((Args.$$$ arbitraryN || Args.$$$ Induct.typeN ||
- Args.$$$ Induct.predN || Args.$$$ Induct.setN || Args.$$$ ruleN) -- Args.colon)) scan;
-
-val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
- Scan.repeat1 (unless_more_args Args.term)) [];
-
-in
-
-val setup =
- Method.setup @{binding coinduction}
- (arbitrary -- Scan.option coinduct_rule >>
- (fn (arbitrary, opt_rule) => fn ctxt =>
- RAW_METHOD_CASES (fn facts =>
- Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts))))
- "coinduction on types or predicates/sets";
-
-end;
-
-end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Coinduction.thy Wed Nov 20 20:45:20 2013 +0100
@@ -0,0 +1,19 @@
+(* Title: HOL/Coinduction.thy
+ Author: Johannes Hölzl, TU Muenchen
+ Author: Dmitriy Traytel, TU Muenchen
+ Copyright 2013
+
+Coinduction method that avoids some boilerplate compared to coinduct.
+*)
+
+header {* Coinduction Method *}
+
+theory Coinduction
+imports Inductive
+begin
+
+ML_file "Tools/coinduction.ML"
+
+setup Coinduction.setup
+
+end
--- a/src/HOL/Main.thy Wed Nov 20 20:18:53 2013 +0100
+++ b/src/HOL/Main.thy Wed Nov 20 20:45:20 2013 +0100
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix
+imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction
begin
text {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/coinduction.ML Wed Nov 20 20:45:20 2013 +0100
@@ -0,0 +1,159 @@
+(* Title: HOL/Tools/coinduction.ML
+ Author: Johannes Hölzl, TU Muenchen
+ Author: Dmitriy Traytel, TU Muenchen
+ Copyright 2013
+
+Coinduction method that avoids some boilerplate compared to coinduct.
+*)
+
+signature COINDUCTION =
+sig
+ val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
+ val setup: theory -> theory
+end;
+
+structure Coinduction : COINDUCTION =
+struct
+
+open Ctr_Sugar_Util
+open Ctr_Sugar_General_Tactics
+
+fun filter_in_out _ [] = ([], [])
+ | filter_in_out P (x :: xs) = (let
+ val (ins, outs) = filter_in_out P xs;
+ in
+ if P x then (x :: ins, outs) else (ins, x :: outs)
+ end);
+
+fun ALLGOALS_SKIP skip tac st =
+ let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
+ in doall (nprems_of st) st end;
+
+fun THEN_ALL_NEW_SKIP skip tac1 tac2 i st =
+ st |> (tac1 i THEN (fn st' =>
+ Seq.INTERVAL tac2 (i + skip) (i + nprems_of st' - nprems_of st) st'));
+
+fun DELETE_PREMS_AFTER skip tac i st =
+ let
+ val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
+ in
+ (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
+ end;
+
+fun coinduction_tac ctxt raw_vars opt_raw_thm prems st =
+ let
+ val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
+ fun find_coinduct t =
+ Induct.find_coinductP ctxt t @
+ (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
+ val raw_thm = case opt_raw_thm
+ of SOME raw_thm => raw_thm
+ | NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd;
+ val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
+ val cases = Rule_Cases.get raw_thm |> fst
+ in
+ NO_CASES (HEADGOAL (
+ Object_Logic.rulify_tac THEN'
+ Method.insert_tac prems THEN'
+ Object_Logic.atomize_prems_tac THEN'
+ DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
+ let
+ val vars = raw_vars @ map (term_of o snd) params;
+ val names_ctxt = ctxt
+ |> fold Variable.declare_names vars
+ |> fold Variable.declare_thm (raw_thm :: prems);
+ val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
+ val (rhoTs, rhots) = Thm.match (thm_concl, concl)
+ |>> map (pairself typ_of)
+ ||> map (pairself term_of);
+ val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
+ |> map (subst_atomic_types rhoTs);
+ val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
+ val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
+ |>> (fn names => Variable.variant_fixes names names_ctxt) ;
+ val eqs =
+ map3 (fn name => fn T => fn (_, rhs) =>
+ HOLogic.mk_eq (Free (name, T), rhs))
+ names Ts raw_eqs;
+ val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
+ |> try (Library.foldr1 HOLogic.mk_conj)
+ |> the_default @{term True}
+ |> list_exists_free vars
+ |> Term.map_abs_vars (Variable.revert_fixed ctxt)
+ |> fold_rev Term.absfree (names ~~ Ts)
+ |> certify ctxt;
+ val thm = cterm_instantiate_pos [SOME phi] raw_thm;
+ val e = length eqs;
+ val p = length prems;
+ in
+ HEADGOAL (EVERY' [rtac thm,
+ EVERY' (map (fn var =>
+ rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
+ if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
+ else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
+ K (ALLGOALS_SKIP skip
+ (REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
+ DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
+ (case prems of
+ [] => all_tac
+ | inv::case_prems =>
+ let
+ val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
+ val inv_thms = init @ [last];
+ val eqs = take e inv_thms;
+ fun is_local_var t =
+ member (fn (t, (_, t')) => t aconv (term_of t')) params t;
+ val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
+ val assms = assms' @ drop e inv_thms
+ in
+ HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
+ unfold_thms_tac ctxt eqs
+ end)) ctxt)))])
+ end) ctxt) THEN'
+ K (prune_params_tac))) st
+ |> Seq.maps (fn (_, st) =>
+ CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
+ end;
+
+local
+
+val ruleN = "rule"
+val arbitraryN = "arbitrary"
+fun single_rule [rule] = rule
+ | single_rule _ = error "Single rule expected";
+
+fun named_rule k arg get =
+ Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
+ (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
+ (case get (Context.proof_of context) name of SOME x => x
+ | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
+
+fun rule get_type get_pred =
+ named_rule Induct.typeN (Args.type_name false) get_type ||
+ named_rule Induct.predN (Args.const false) get_pred ||
+ named_rule Induct.setN (Args.const false) get_pred ||
+ Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
+
+val coinduct_rule = rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;
+
+fun unless_more_args scan = Scan.unless (Scan.lift
+ ((Args.$$$ arbitraryN || Args.$$$ Induct.typeN ||
+ Args.$$$ Induct.predN || Args.$$$ Induct.setN || Args.$$$ ruleN) -- Args.colon)) scan;
+
+val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
+ Scan.repeat1 (unless_more_args Args.term)) [];
+
+in
+
+val setup =
+ Method.setup @{binding coinduction}
+ (arbitrary -- Scan.option coinduct_rule >>
+ (fn (arbitrary, opt_rule) => fn ctxt =>
+ RAW_METHOD_CASES (fn facts =>
+ Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts))))
+ "coinduction on types or predicates/sets";
+
+end;
+
+end;
+
--- a/src/HOL/Tools/ctr_sugar_util.ML Wed Nov 20 20:18:53 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar_util.ML Wed Nov 20 20:45:20 2013 +0100
@@ -56,6 +56,7 @@
val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv
+ val cterm_instantiate_pos: cterm option list -> thm -> thm
val unfold_thms: Proof.context -> thm list -> thm -> thm
val certifyT: Proof.context -> typ -> ctyp
@@ -66,6 +67,14 @@
val parse_binding: binding parser
val ss_only: thm list -> Proof.context -> Proof.context
+
+ val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
+ val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
+ tactic
+ val CONJ_WRAP_GEN: tactic -> ('a -> tactic) -> 'a list -> tactic
+ val CONJ_WRAP_GEN': (int -> tactic) -> ('a -> int -> tactic) -> 'a list -> int -> tactic
+ val CONJ_WRAP: ('a -> tactic) -> 'a list -> tactic
+ val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic
end;
structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
@@ -186,6 +195,17 @@
Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
end;
+fun cterm_instantiate_pos cts thm =
+ let
+ val cert = Thm.cterm_of (Thm.theory_of_thm thm);
+ val vars = Term.add_vars (prop_of thm) [];
+ val vars' = rev (drop (length vars - length cts) vars);
+ val ps = map_filter (fn (_, NONE) => NONE
+ | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
+ in
+ Drule.cterm_instantiate ps thm
+ end;
+
fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
@@ -202,4 +222,23 @@
fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
+(*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
+fun WRAP gen_before gen_after xs core_tac =
+ fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;
+
+fun WRAP' gen_before gen_after xs core_tac =
+ fold_rev (fn x => fn tac => gen_before x THEN' tac THEN' gen_after x) xs core_tac;
+
+fun CONJ_WRAP_GEN conj_tac gen_tac xs =
+ let val (butlast, last) = split_last xs;
+ in WRAP (fn thm => conj_tac THEN gen_tac thm) (K all_tac) butlast (gen_tac last) end;
+
+fun CONJ_WRAP_GEN' conj_tac gen_tac xs =
+ let val (butlast, last) = split_last xs;
+ in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
+
+(*not eta-converted because of monotype restriction*)
+fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
+fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;
+
end;