refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
--- a/src/HOL/BNF/BNF_Util.thy Tue Oct 01 14:05:25 2013 +0200
+++ b/src/HOL/BNF/BNF_Util.thy Tue Oct 01 14:05:25 2013 +0200
@@ -9,7 +9,7 @@
header {* Library for Bounded Natural Functors *}
theory BNF_Util
-imports "../Cardinals/Cardinal_Arithmetic"
+imports Ctr_Sugar "../Cardinals/Cardinal_Arithmetic"
begin
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
--- a/src/HOL/BNF/Ctr_Sugar.thy Tue Oct 01 14:05:25 2013 +0200
+++ b/src/HOL/BNF/Ctr_Sugar.thy Tue Oct 01 14:05:25 2013 +0200
@@ -8,7 +8,7 @@
header {* Wrapping Existing Freely Generated Type's Constructors *}
theory Ctr_Sugar
-imports BNF_Util
+imports Main
keywords
"wrap_free_constructors" :: thy_goal and
"no_discs_sels" and
@@ -23,6 +23,7 @@
"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
by blast+
+ML_file "Tools/ctr_sugar_util.ML"
ML_file "Tools/ctr_sugar_tactics.ML"
ML_file "Tools/ctr_sugar.ML"
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Tue Oct 01 14:05:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Tue Oct 01 14:05:25 2013 +0200
@@ -8,11 +8,9 @@
signature BNF_TACTICS =
sig
- val ss_only : thm list -> Proof.context -> Proof.context
+ include CTR_SUGAR_GENERAL_TACTICS
- val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
val fo_rtac: thm -> Proof.context -> 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
val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic
@@ -35,13 +33,9 @@
structure BNF_Tactics : BNF_TACTICS =
struct
+open Ctr_Sugar_General_Tactics
open BNF_Util
-fun ss_only ths ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths
-
-fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
- tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
-
(*stolen from Christian Urban's Cookbook*)
fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} =>
let
@@ -51,9 +45,6 @@
rtac (Drule.instantiate_normalize insts thm) 1
end);
-fun unfold_thms_tac _ [] = all_tac
- | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
-
fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
--- a/src/HOL/BNF/Tools/bnf_util.ML Tue Oct 01 14:05:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Tue Oct 01 14:05:25 2013 +0200
@@ -7,10 +7,8 @@
signature BNF_UTIL =
sig
- val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
- val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
- val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
- 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list
+ include CTR_SUGAR_UTIL
+
val map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list
val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) ->
@@ -32,9 +30,6 @@
val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list
- val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c
- val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) ->
- 'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd
val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
@@ -50,35 +45,16 @@
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j -> 'k list * 'j
val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
- val splice: 'a list -> 'a list -> 'a list
- val transpose: 'a list list -> 'a list list
- val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
- val pad_list: 'a -> int -> 'a list -> 'a list
+ val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list
- val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list
- val permute_like: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c list -> 'c list
-
- val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
- val mk_TFrees: int -> Proof.context -> typ list * Proof.context
val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
- val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context
- val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context
- val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context
val mk_Freesss: string -> typ list list list -> Proof.context ->
term list list list * Proof.context
val mk_Freessss: string -> typ list list list list -> Proof.context ->
term list list list list * Proof.context
- val mk_Frees': string -> typ list -> Proof.context ->
- (term list * (string * typ) list) * Proof.context
- val mk_Freess': string -> typ list list -> Proof.context ->
- (term list list * (string * typ) list list) * Proof.context
val nonzero_string_of_int: int -> string
- val resort_tfree: sort -> typ -> typ
val retype_free: typ -> term -> term
val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
- val variant_types: string list -> sort list -> Proof.context ->
- (string * sort) list * Proof.context
- val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
val binder_fun_types: typ -> typ list
val body_fun_type: typ -> typ
@@ -86,8 +62,6 @@
val strip_fun_type: typ -> typ list * typ
val strip_typeN: int -> typ -> typ list * typ
- val mk_predT: typ list -> typ
- val mk_pred1T: typ -> typ
val mk_pred2T: typ -> typ -> typ
val mk_relT: typ * typ -> typ
val dest_relT: typ -> typ * typ
@@ -105,8 +79,6 @@
val mk_Field: term -> term
val mk_Gr: term -> term -> term
val mk_Grp: term -> term -> term
- val mk_IfN: typ -> term list -> term list -> term
- val mk_Trueprop_eq: term * term -> term
val mk_UNION: term -> term -> term
val mk_Union: typ -> term
val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term
@@ -129,13 +101,6 @@
val mk_rel_compp: term * term -> term
val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term
- val rapp: term -> term -> term
-
- val list_all_free: term list -> term -> term
- val list_exists_free: term list -> term -> term
-
- val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv
-
(*parameterized terms*)
val mk_nthN: int -> term -> int -> term
@@ -144,7 +109,6 @@
val mk_conjIN: int -> thm
val mk_conjunctN: int -> int -> thm
val conj_dests: int -> thm -> thm list
- val mk_disjIN: int -> int -> thm
val mk_nthI: int -> int -> thm
val mk_nth_conv: int -> int -> thm
val mk_ordLeq_csum: int -> int -> thm -> thm
@@ -162,7 +126,6 @@
val subset_UNIV: thm
val mk_sym: thm -> thm
val mk_trans: thm -> thm -> thm
- val mk_unabs_def: int -> thm -> thm
val is_triv_implies: thm -> bool
val is_refl: thm -> bool
@@ -172,14 +135,7 @@
val cterm_instantiate_pos: cterm option list -> thm -> thm
val fold_thms: Proof.context -> thm list -> thm -> thm
- val unfold_thms: Proof.context -> thm list -> thm -> thm
- val certifyT: Proof.context -> typ -> ctyp
- val certify: Proof.context -> term -> cterm
-
- val standard_binding: binding
- val equal_binding: binding
- val parse_binding: binding parser
val parse_binding_colon: binding parser
val parse_opt_binding_colon: binding parser
@@ -198,20 +154,9 @@
structure BNF_Util : BNF_UTIL =
struct
-(* Library proper *)
-
-fun map3 _ [] [] [] = []
- | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
- | map3 _ _ _ _ = raise ListPair.UnequalLengths;
+open Ctr_Sugar_Util
-fun map4 _ [] [] [] [] = []
- | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s
- | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map5 _ [] [] [] [] [] = []
- | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) =
- f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s
- | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+(* Library proper *)
fun map6 _ [] [] [] [] [] [] = []
| map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) =
@@ -260,22 +205,6 @@
map13 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s
| map13 _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-fun fold_map2 _ [] [] acc = ([], acc)
- | fold_map2 f (x1::x1s) (x2::x2s) acc =
- let
- val (x, acc') = f x1 x2 acc;
- val (xs, acc'') = fold_map2 f x1s x2s acc';
- in (x :: xs, acc'') end
- | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun fold_map3 _ [] [] [] acc = ([], acc)
- | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc =
- let
- val (x, acc') = f x1 x2 x3 acc;
- val (xs, acc'') = fold_map3 f x1s x2s x3s acc';
- in (x :: xs, acc'') end
- | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths;
-
fun fold_map4 _ [] [] [] [] acc = ([], acc)
| fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
let
@@ -331,17 +260,6 @@
let val (xs1, xs2, xs3, xs4) = split_list4 xs;
in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
-(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
-fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
-fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
-
-(* The standard binding stands for a name generated following the canonical convention (e.g.,
- "is_Nil" from "Nil"). The smart binding is either the standard binding or no binding at all,
- depending on the context. *)
-val standard_binding = @{binding _};
-val equal_binding = @{binding "="};
-
-val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
val parse_binding_colon = parse_binding --| @{keyword ":"};
val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
@@ -387,13 +305,8 @@
fun nonzero_string_of_int 0 = ""
| nonzero_string_of_int n = string_of_int n;
-val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
-
-fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
val mk_TFreess = fold_map mk_TFrees;
-fun resort_tfree S (TFree (s, _)) = TFree (s, S);
-
(*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
fun typ_subst_nonatomic [] = I
| typ_subst_nonatomic inst =
@@ -402,32 +315,12 @@
| subst T = perhaps (AList.lookup (op =) inst) T;
in subst end;
-fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n);
-
-fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names;
-fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
-fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss;
-fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
-fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
fun retype_free T (Free (s, _)) = Free (s, T)
| retype_free _ t = raise TERM ("retype_free", [t]);
-fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre;
-
-fun variant_types ss Ss ctxt =
- let
- val (tfrees, _) =
- fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
- val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
- in (tfrees, ctxt') end;
-
-fun variant_tfrees ss =
- apfst (map TFree) o
- variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
-
(** Types **)
@@ -447,8 +340,6 @@
val binder_fun_types = fst o strip_fun_type;
val body_fun_type = snd o strip_fun_type;
-fun mk_predT Ts = Ts ---> HOLogic.boolT;
-fun mk_pred1T T = mk_predT [T];
fun mk_pred2T T U = mk_predT [T, U];
val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT;
val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT;
@@ -465,12 +356,6 @@
(** Operators **)
-val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
-
-fun mk_IfN _ _ [t] = t
- | mk_IfN T (c :: cs) (t :: ts) =
- Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts;
-
fun mk_converse R =
let
val RT = dest_relT (fastype_of R);
@@ -637,21 +522,6 @@
let val T = (case xs of [] => defT | (x::_) => fastype_of x);
in Const (@{const_name collect}, HOLogic.mk_setT T --> T) $ (HOLogic.mk_set T xs) end;
-fun rapp u t = betapply (t, u);
-
-fun list_quant_free quant_const =
- fold_rev (fn free => fn P =>
- let val (x, T) = Term.dest_Free free;
- in quant_const T $ Term.absfree (x, T) P end);
-
-val list_all_free = list_quant_free HOLogic.all_const;
-val list_exists_free = list_quant_free HOLogic.exists_const;
-
-fun fo_match ctxt t pat =
- let val thy = Proof_Context.theory_of ctxt in
- Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
- end;
-
fun find_indices eq xs ys = map_filter I
(map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys);
@@ -699,11 +569,6 @@
fun mk_conjIN 1 = @{thm TrueE[OF TrueI]}
| mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI);
-fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
- | mk_disjIN _ 1 = disjI1
- | mk_disjIN 2 2 = disjI2
- | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
-
fun mk_ordLeq_csum 1 1 thm = thm
| mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}]
| mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}]
@@ -730,26 +595,6 @@
| mk_UnIN n m = mk_UnIN' (n - m)
end;
-fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
-
-fun transpose [] = []
- | transpose ([] :: xss) = transpose xss
- | transpose xss = map hd xss :: transpose (map tl xss);
-
-fun permute_like eq xs xs' ys = map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs';
-
-fun seq_conds f n k xs =
- if k = n then
- map (f false) (take (k - 1) xs)
- else
- let val (negs, pos) = split_last (take k xs) in
- map (f false) negs @ [f true pos]
- end;
-
-fun pad_list x n xs = xs @ replicate (n - length xs) x;
-
-fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
-
fun is_triv_implies thm =
op aconv (Logic.dest_implies (Thm.prop_of thm))
handle TERM _ => false;
@@ -776,6 +621,5 @@
end;
fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
-fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
end;
--- a/src/HOL/BNF/Tools/ctr_sugar.ML Tue Oct 01 14:05:25 2013 +0200
+++ b/src/HOL/BNF/Tools/ctr_sugar.ML Tue Oct 01 14:05:25 2013 +0200
@@ -60,7 +60,7 @@
structure Ctr_Sugar : CTR_SUGAR =
struct
-open BNF_Util
+open Ctr_Sugar_Util
open Ctr_Sugar_Tactics
type ctr_sugar =
@@ -779,14 +779,14 @@
val (safe_collapse_thms, all_collapse_thms) =
let
- fun mk_goal m ctr udisc usel_ctr =
+ fun mk_goal m udisc usel_ctr =
let
val prem = HOLogic.mk_Trueprop udisc;
val concl = mk_Trueprop_eq ((usel_ctr, u) |> m = 0 ? swap);
in
(prem aconv concl, Logic.all u (Logic.mk_implies (prem, concl)))
end;
- val (trivs, goals) = map4 mk_goal ms ctrs udiscs usel_ctrs |> split_list;
+ val (trivs, goals) = map3 mk_goal ms udiscs usel_ctrs |> split_list;
val thms =
map5 (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
--- a/src/HOL/BNF/Tools/ctr_sugar_tactics.ML Tue Oct 01 14:05:25 2013 +0200
+++ b/src/HOL/BNF/Tools/ctr_sugar_tactics.ML Tue Oct 01 14:05:25 2013 +0200
@@ -5,8 +5,16 @@
Tactics for wrapping existing freely generated type's constructors.
*)
+signature CTR_SUGAR_GENERAL_TACTICS =
+sig
+ val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
+ val unfold_thms_tac: Proof.context -> thm list -> tactic
+end;
+
signature CTR_SUGAR_TACTICS =
sig
+ include CTR_SUGAR_GENERAL_TACTICS
+
val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
@@ -29,11 +37,16 @@
structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS =
struct
-open BNF_Util
-open BNF_Tactics
+open Ctr_Sugar_Util
val meta_mp = @{thm meta_mp};
+fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
+ tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
+
+fun unfold_thms_tac _ [] = all_tac
+ | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
+
fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
fun mk_nchotomy_tac n exhaust =
@@ -155,3 +168,5 @@
HEADGOAL (rtac refl);
end;
+
+structure Ctr_Sugar_General_Tactics: CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Tools/ctr_sugar_util.ML Tue Oct 01 14:05:25 2013 +0200
@@ -0,0 +1,192 @@
+(* Title: HOL/BNF/Tools/ctr_sugar_util.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2012
+
+Library for wrapping existing freely generated type's constructors.
+*)
+
+signature CTR_SUGAR_UTIL =
+sig
+ val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
+ val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
+ val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
+ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list
+ val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c
+ val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) ->
+ 'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd
+ val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
+ val transpose: 'a list list -> 'a list list
+ val pad_list: 'a -> int -> 'a list -> 'a list
+ val splice: 'a list -> 'a list -> 'a list
+ val permute_like: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c list -> 'c list
+
+ val mk_names: int -> string -> string list
+ val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
+ val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context
+ val mk_TFrees: int -> Proof.context -> typ list * Proof.context
+ val mk_Frees': string -> typ list -> Proof.context ->
+ (term list * (string * typ) list) * Proof.context
+ val mk_Freess': string -> typ list list -> Proof.context ->
+ (term list list * (string * typ) list list) * Proof.context
+ val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context
+ val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context
+ val resort_tfree: sort -> typ -> typ
+ val variant_types: string list -> sort list -> Proof.context ->
+ (string * sort) list * Proof.context
+ val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
+
+ val mk_predT: typ list -> typ
+ val mk_pred1T: typ -> typ
+
+ val mk_disjIN: int -> int -> thm
+
+ val mk_unabs_def: int -> thm -> thm
+
+ val mk_IfN: typ -> term list -> term list -> term
+ val mk_Trueprop_eq: term * term -> term
+
+ val rapp: term -> term -> term
+
+ val list_all_free: term list -> term -> term
+ val list_exists_free: term list -> term -> term
+
+ val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv
+
+ val unfold_thms: Proof.context -> thm list -> thm -> thm
+
+ val certifyT: Proof.context -> typ -> ctyp
+ val certify: Proof.context -> term -> cterm
+
+ val standard_binding: binding
+ val equal_binding: binding
+ val parse_binding: binding parser
+
+ val ss_only: thm list -> Proof.context -> Proof.context
+end;
+
+structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
+struct
+
+fun map3 _ [] [] [] = []
+ | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
+ | map3 _ _ _ _ = raise ListPair.UnequalLengths;
+
+fun map4 _ [] [] [] [] = []
+ | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s
+ | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
+
+fun map5 _ [] [] [] [] [] = []
+ | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) =
+ f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s
+ | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
+fun fold_map2 _ [] [] acc = ([], acc)
+ | fold_map2 f (x1::x1s) (x2::x2s) acc =
+ let
+ val (x, acc') = f x1 x2 acc;
+ val (xs, acc'') = fold_map2 f x1s x2s acc';
+ in (x :: xs, acc'') end
+ | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths;
+
+fun fold_map3 _ [] [] [] acc = ([], acc)
+ | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc =
+ let
+ val (x, acc') = f x1 x2 x3 acc;
+ val (xs, acc'') = fold_map3 f x1s x2s x3s acc';
+ in (x :: xs, acc'') end
+ | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths;
+
+fun seq_conds f n k xs =
+ if k = n then
+ map (f false) (take (k - 1) xs)
+ else
+ let val (negs, pos) = split_last (take k xs) in
+ map (f false) negs @ [f true pos]
+ end;
+
+fun transpose [] = []
+ | transpose ([] :: xss) = transpose xss
+ | transpose xss = map hd xss :: transpose (map tl xss);
+
+fun pad_list x n xs = xs @ replicate (n - length xs) x;
+
+fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
+
+fun permute_like eq xs xs' ys = map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs';
+
+fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n);
+fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names;
+
+val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
+
+fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
+
+fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
+fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
+
+fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
+fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
+
+fun resort_tfree S (TFree (s, _)) = TFree (s, S);
+
+fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre;
+
+fun variant_types ss Ss ctxt =
+ let
+ val (tfrees, _) =
+ fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
+ val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
+ in (tfrees, ctxt') end;
+
+fun variant_tfrees ss =
+ apfst (map TFree) o
+ variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
+
+fun mk_predT Ts = Ts ---> HOLogic.boolT;
+fun mk_pred1T T = mk_predT [T];
+
+fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
+ | mk_disjIN _ 1 = disjI1
+ | mk_disjIN 2 2 = disjI2
+ | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
+
+fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
+
+fun mk_IfN _ _ [t] = t
+ | mk_IfN T (c :: cs) (t :: ts) =
+ Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts;
+
+val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
+
+fun rapp u t = betapply (t, u);
+
+fun list_quant_free quant_const =
+ fold_rev (fn free => fn P =>
+ let val (x, T) = Term.dest_Free free;
+ in quant_const T $ Term.absfree (x, T) P end);
+
+val list_all_free = list_quant_free HOLogic.all_const;
+val list_exists_free = list_quant_free HOLogic.exists_const;
+
+fun fo_match ctxt t pat =
+ let val thy = Proof_Context.theory_of ctxt in
+ Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
+ 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*)
+fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
+fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
+
+(* The standard binding stands for a name generated following the canonical convention (e.g.,
+ "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no
+ binding at all, depending on the context. *)
+val standard_binding = @{binding _};
+val equal_binding = @{binding "="};
+
+val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
+
+fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
+
+end;