--- a/src/HOL/Tools/TFL/usyntax.ML Wed Jul 29 16:43:02 2009 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Wed Jul 29 16:48:34 2009 +0200
@@ -118,7 +118,7 @@
val alpha = mk_vartype "'a"
val beta = mk_vartype "'b"
-val strip_prod_type = HOLogic.prodT_factors;
+val strip_prod_type = HOLogic.flatten_tupleT;
--- a/src/HOL/Tools/hologic.ML Wed Jul 29 16:43:02 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Wed Jul 29 16:48:34 2009 +0200
@@ -66,17 +66,15 @@
val mk_snd: term -> term
val split_const: typ * typ * typ -> term
val mk_split: term -> term
- val prodT_factors: typ -> typ list
- val mk_tuple: typ -> term list -> term
- val dest_tuple: term -> term list
- val ap_split: typ -> typ -> term -> term
- val prod_factors: term -> int list list
- val dest_tuple': int list list -> term -> term list
- val prodT_factors': int list list -> typ -> typ list
- val ap_split': int list list -> typ -> typ -> term -> term
- val mk_tuple': int list list -> typ -> term list -> term
+ val flatten_tupleT: typ -> typ list
val mk_tupleT: int list list -> typ list -> typ
- val strip_split: term -> term * typ list * int list list
+ val strip_tupleT: int list list -> typ -> typ list
+ val flat_tupleT_paths: typ -> int list list
+ val mk_tuple: int list list -> typ -> term list -> term
+ val dest_tuple: int list list -> term -> term list
+ val flat_tuple_paths: term -> int list list
+ val mk_splits: int list list -> typ -> typ -> term -> term
+ val strip_splits: term -> term * typ list * int list list
val natT: typ
val zero: term
val is_zero: term -> bool
@@ -320,95 +318,17 @@
| _ => raise TERM ("mk_split: bad body type", [t]));
(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
-fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2
- | prodT_factors T = [T];
-
-(*Makes a nested tuple from a list, following the product type structure*)
-fun mk_tuple (Type ("*", [T1, T2])) tms =
- mk_prod (mk_tuple T1 tms,
- mk_tuple T2 (Library.drop (length (prodT_factors T1), tms)))
- | mk_tuple T (t::_) = t;
-
-fun dest_tuple (Const ("Pair", _) $ t $ u) = dest_tuple t @ dest_tuple u
- | dest_tuple t = [t];
+fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
+ | flatten_tupleT T = [T];
-(*In ap_split S T u, term u expects separate arguments for the factors of S,
- with result type T. The call creates a new term expecting one argument
- of type S.*)
-fun ap_split T T3 u =
- let
- fun ap (T :: Ts) =
- (case T of
- Type ("*", [T1, T2]) =>
- split_const (T1, T2, Ts ---> T3) $ ap (T1 :: T2 :: Ts)
- | _ => Abs ("x", T, ap Ts))
- | ap [] =
- let val k = length (prodT_factors T)
- in list_comb (incr_boundvars k u, map Bound (k - 1 downto 0)) end
- in ap [T] end;
+(* tuples with specific arities
-
-(* operations on tuples with specific arities *)
-(*
an "arity" of a tuple is a list of lists of integers
("factors"), denoting paths to subterms that are pairs
*)
fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
-fun prod_factors t =
- let
- fun factors p (Const ("Pair", _) $ t $ u) =
- p :: factors (1::p) t @ factors (2::p) u
- | factors p _ = []
- in factors [] t end;
-
-fun dest_tuple' ps =
- let
- fun dest p t = if p mem ps then (case t of
- Const ("Pair", _) $ t $ u =>
- dest (1::p) t @ dest (2::p) u
- | _ => prod_err "dest_tuple'") else [t]
- in dest [] end;
-
-fun prodT_factors' ps =
- let
- fun factors p T = if p mem ps then (case T of
- Type ("*", [T1, T2]) =>
- factors (1::p) T1 @ factors (2::p) T2
- | _ => prod_err "prodT_factors'") else [T]
- in factors [] end;
-
-(*In ap_split' ps S T u, term u expects separate arguments for the factors of S,
- with result type T. The call creates a new term expecting one argument
- of type S.*)
-fun ap_split' ps T T3 u =
- let
- fun ap ((p, T) :: pTs) =
- if p mem ps then (case T of
- Type ("*", [T1, T2]) =>
- split_const (T1, T2, map snd pTs ---> T3) $
- ap ((1::p, T1) :: (2::p, T2) :: pTs)
- | _ => prod_err "ap_split'")
- else Abs ("x", T, ap pTs)
- | ap [] =
- let val k = length ps
- in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
- in ap [([], T)] end;
-
-fun mk_tuple' ps =
- let
- fun mk p T ts =
- if p mem ps then (case T of
- Type ("*", [T1, T2]) =>
- let
- val (t, ts') = mk (1::p) T1 ts;
- val (u, ts'') = mk (2::p) T2 ts'
- in (pair_const T1 T2 $ t $ u, ts'') end
- | _ => prod_err "mk_tuple'")
- else (hd ts, tl ts)
- in fst oo mk [] end;
-
fun mk_tupleT ps =
let
fun mk p Ts =
@@ -420,7 +340,67 @@
else (hd Ts, tl Ts)
in fst o mk [] end;
-fun strip_split t =
+fun strip_tupleT ps =
+ let
+ fun factors p T = if p mem ps then (case T of
+ Type ("*", [T1, T2]) =>
+ factors (1::p) T1 @ factors (2::p) T2
+ | _ => prod_err "strip_tupleT") else [T]
+ in factors [] end;
+
+val flat_tupleT_paths =
+ let
+ fun factors p (Type ("*", [T1, T2])) =
+ p :: factors (1::p) T1 @ factors (2::p) T2
+ | factors p _ = []
+ in factors [] end;
+
+fun mk_tuple ps =
+ let
+ fun mk p T ts =
+ if p mem ps then (case T of
+ Type ("*", [T1, T2]) =>
+ let
+ val (t, ts') = mk (1::p) T1 ts;
+ val (u, ts'') = mk (2::p) T2 ts'
+ in (pair_const T1 T2 $ t $ u, ts'') end
+ | _ => prod_err "mk_tuple")
+ else (hd ts, tl ts)
+ in fst oo mk [] end;
+
+fun dest_tuple ps =
+ let
+ fun dest p t = if p mem ps then (case t of
+ Const ("Pair", _) $ t $ u =>
+ dest (1::p) t @ dest (2::p) u
+ | _ => prod_err "dest_tuple") else [t]
+ in dest [] end;
+
+val flat_tuple_paths =
+ let
+ fun factors p (Const ("Pair", _) $ t $ u) =
+ p :: factors (1::p) t @ factors (2::p) u
+ | factors p _ = []
+ in factors [] end;
+
+(*In mk_splits ps S T u, term u expects separate arguments for the factors of S,
+ with result type T. The call creates a new term expecting one argument
+ of type S.*)
+fun mk_splits ps T T3 u =
+ let
+ fun ap ((p, T) :: pTs) =
+ if p mem ps then (case T of
+ Type ("*", [T1, T2]) =>
+ split_const (T1, T2, map snd pTs ---> T3) $
+ ap ((1::p, T1) :: (2::p, T2) :: pTs)
+ | _ => prod_err "mk_splits")
+ else Abs ("x", T, ap pTs)
+ | ap [] =
+ let val k = length ps
+ in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
+ in ap [([], T)] end;
+
+val strip_splits =
let
fun strip [] qs Ts t = (t, Ts, qs)
| strip (p :: ps) qs Ts (Const ("split", _) $ t) =
@@ -429,7 +409,7 @@
| strip (p :: ps) qs Ts t = strip ps qs
(hd (binder_types (fastype_of1 (Ts, t))) :: Ts)
(incr_boundvars 1 t $ Bound 0)
- in strip [[]] [] [] t end;
+ in strip [[]] [] [] end;
(* nat *)
--- a/src/HOL/Tools/inductive_codegen.ML Wed Jul 29 16:43:02 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Wed Jul 29 16:48:34 2009 +0200
@@ -645,7 +645,7 @@
fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of
(Const ("Collect", _), [u]) =>
- let val (r, Ts, fs) = HOLogic.strip_split u
+ let val (r, Ts, fs) = HOLogic.strip_splits u
in case strip_comb r of
(Const (s, T), ts) =>
(case (get_clauses thy s, get_assoc_code thy (s, T)) of
--- a/src/HOL/Tools/inductive_set.ML Wed Jul 29 16:43:02 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Wed Jul 29 16:48:34 2009 +0200
@@ -33,10 +33,10 @@
val collect_mem_simproc =
Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
- let val (u, Ts, ps) = HOLogic.strip_split t
+ let val (u, Ts, ps) = HOLogic.strip_splits t
in case u of
(c as Const ("op :", _)) $ q $ S' =>
- (case try (HOLogic.dest_tuple' ps) q of
+ (case try (HOLogic.dest_tuple ps) q of
NONE => NONE
| SOME ts =>
if not (loose_bvar (S', 0)) andalso
@@ -79,7 +79,7 @@
fun mk_collect p T t =
let val U = HOLogic.dest_setT T
in HOLogic.Collect_const U $
- HOLogic.ap_split' (HOLogic.prod_factors p) U HOLogic.boolT t
+ HOLogic.mk_splits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
end;
fun decomp (Const (s, _) $ ((m as Const ("op :",
Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
@@ -223,11 +223,11 @@
map (fn (x, ps) =>
let
val U = HOLogic.dest_setT (fastype_of x);
- val x' = map_type (K (HOLogic.prodT_factors' ps U ---> HOLogic.boolT)) x
+ val x' = map_type (K (HOLogic.strip_tupleT ps U ---> HOLogic.boolT)) x
in
(cterm_of thy x,
cterm_of thy (HOLogic.Collect_const U $
- HOLogic.ap_split' ps U HOLogic.boolT x'))
+ HOLogic.mk_splits ps U HOLogic.boolT x'))
end) fs;
fun mk_to_pred_eq p fs optfs' T thm =
@@ -240,7 +240,7 @@
| SOME fs' =>
let
val (_, U) = split_last (binder_types T);
- val Ts = HOLogic.prodT_factors' fs' U;
+ val Ts = HOLogic.strip_tupleT fs' U;
(* FIXME: should cterm_instantiate increment indexes? *)
val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
val (arg_cong_f, _) = arg_cong' |> cprop_of |> Drule.strip_imp_concl |>
@@ -248,7 +248,7 @@
in
thm' RS (Drule.cterm_instantiate [(arg_cong_f,
cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
- HOLogic.Collect_const U $ HOLogic.ap_split' fs' U
+ HOLogic.Collect_const U $ HOLogic.mk_splits fs' U
HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
end)
in
@@ -270,7 +270,7 @@
fun factors_of t fs = case strip_abs_body t of
Const ("op :", _) $ u $ S =>
if is_Free S orelse is_Var S then
- let val ps = HOLogic.prod_factors u
+ let val ps = HOLogic.flat_tuple_paths u
in (SOME ps, (S, ps) :: fs) end
else (NONE, fs)
| _ => (NONE, fs);
@@ -279,7 +279,7 @@
val ((h', ts'), fs') = (case rhs of
Abs _ => (case strip_abs_body rhs of
Const ("op :", _) $ u $ S =>
- (strip_comb S, SOME (HOLogic.prod_factors u))
+ (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
| _ => error "member symbol on right-hand side expected")
| _ => (strip_comb rhs, NONE))
in
@@ -366,7 +366,7 @@
in
(cterm_of thy x,
cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_tuple' ps T (map Bound (length ps downto 0)), x'))))
+ (HOLogic.mk_tuple ps T (map Bound (length ps downto 0)), x'))))
end) fs
in
thm |>
@@ -412,7 +412,7 @@
PredSetConvData.get (Context.Proof ctxt);
fun infer (Abs (_, _, t)) = infer t
| infer (Const ("op :", _) $ t $ u) =
- infer_arities thy set_arities (SOME (HOLogic.prod_factors t), u)
+ infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
| infer (t $ u) = infer t #> infer u
| infer _ = I;
val new_arities = filter_out
@@ -422,14 +422,14 @@
SOME fs =>
let
val T = HOLogic.dest_setT (fastype_of x);
- val Ts = HOLogic.prodT_factors' fs T;
+ val Ts = HOLogic.strip_tupleT fs T;
val x' = map_type (K (Ts ---> HOLogic.boolT)) x
in
(x, (x',
(HOLogic.Collect_const T $
- HOLogic.ap_split' fs T HOLogic.boolT x',
+ HOLogic.mk_splits fs T HOLogic.boolT x',
list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_tuple' fs T (map Bound (length fs downto 0)),
+ (HOLogic.mk_tuple fs T (map Bound (length fs downto 0)),
x)))))
end
| NONE => (x, (x, (x, x))))) params;
@@ -448,13 +448,13 @@
Pretty.str ("of " ^ s ^ " do not agree with types"),
Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
Pretty.str "of declared parameters"]));
- val Ts = HOLogic.prodT_factors' fs U;
+ val Ts = HOLogic.strip_tupleT fs U;
val c' = Free (s ^ "p",
map fastype_of params1 @ Ts ---> HOLogic.boolT)
in
((c', (fs, U, Ts)),
(list_comb (c, params2),
- HOLogic.Collect_const U $ HOLogic.ap_split' fs U HOLogic.boolT
+ HOLogic.Collect_const U $ HOLogic.mk_splits fs U HOLogic.boolT
(list_comb (c', params1))))
end) |> split_list |>> split_list;
val eqns' = eqns @
@@ -484,7 +484,7 @@
val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
(map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
fold_rev lambda params (HOLogic.Collect_const U $
- HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
+ HOLogic.mk_splits fs U HOLogic.boolT (list_comb (p, params3))))))
(cnames_syn ~~ cs_info ~~ preds)) ctxt1;
(* prove theorems for converting predicate to set notation *)
@@ -495,7 +495,7 @@
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(list_comb (p, params3),
list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_tuple' fs U (map Bound (length fs downto 0)),
+ (HOLogic.mk_tuple fs U (map Bound (length fs downto 0)),
list_comb (c, params))))))
(K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
[def, mem_Collect_eq, split_conv]) 1))
--- a/src/HOL/Tools/split_rule.ML Wed Jul 29 16:43:02 2009 +0200
+++ b/src/HOL/Tools/split_rule.ML Wed Jul 29 16:48:34 2009 +0200
@@ -50,13 +50,13 @@
internal_split_const (T1, T2, T3) $
Abs ("v", T1,
ap_split T2 T3
- ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
+ ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $
Bound 0))
| ap_split T T3 u = u;
(*Curries any Var of function type in the rule*)
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
- let val T' = HOLogic.prodT_factors T1 ---> T2;
+ let val T' = HOLogic.flatten_tupleT T1 ---> T2;
val newt = ap_split T1 T2 (Var (v, T'));
val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
@@ -66,7 +66,7 @@
(* complete splitting of partially splitted rules *)
fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
- (ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U)
+ (ap_split T (List.concat (map HOLogic.flatten_tupleT Ts) ---> U)
(incr_boundvars 1 u) $ Bound 0))
| ap_split' _ _ u = u;
@@ -76,10 +76,10 @@
val (Us', U') = strip_type T;
val Us = Library.take (length ts, Us');
val U = Library.drop (length ts, Us') ---> U';
- val T' = List.concat (map HOLogic.prodT_factors Us) ---> U;
+ val T' = List.concat (map HOLogic.flatten_tupleT Us) ---> U;
fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
let
- val Ts = HOLogic.prodT_factors T;
+ val Ts = HOLogic.flatten_tupleT T;
val ys = Name.variant_list xs (replicate (length Ts) a);
in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
(map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
--- a/src/HOL/ex/predicate_compile.ML Wed Jul 29 16:43:02 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Wed Jul 29 16:48:34 2009 +0200
@@ -1531,7 +1531,7 @@
let
val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
| _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
- val (body, Ts, fp) = HOLogic.strip_split split;
+ val (body, Ts, fp) = HOLogic.strip_splits split;
(*FIXME former order of tuple positions must be restored*)
val (pred as Const (name, T), all_args) = strip_comb body
val (params, args) = chop (nparams_of thy name) all_args