1.1 --- a/src/HOL/Tools/TFL/usyntax.ML Thu Jul 30 23:06:06 2009 +0200
1.2 +++ b/src/HOL/Tools/TFL/usyntax.ML Thu Jul 30 23:09:29 2009 +0200
1.3 @@ -118,7 +118,7 @@
1.4 val alpha = mk_vartype "'a"
1.5 val beta = mk_vartype "'b"
1.6
1.7 -val strip_prod_type = HOLogic.prodT_factors;
1.8 +val strip_prod_type = HOLogic.flatten_tupleT;
1.9
1.10
1.11
2.1 --- a/src/HOL/Tools/hologic.ML Thu Jul 30 23:06:06 2009 +0200
2.2 +++ b/src/HOL/Tools/hologic.ML Thu Jul 30 23:09:29 2009 +0200
2.3 @@ -66,17 +66,15 @@
2.4 val mk_snd: term -> term
2.5 val split_const: typ * typ * typ -> term
2.6 val mk_split: term -> term
2.7 - val prodT_factors: typ -> typ list
2.8 - val mk_tuple: typ -> term list -> term
2.9 - val dest_tuple: term -> term list
2.10 - val ap_split: typ -> typ -> term -> term
2.11 - val prod_factors: term -> int list list
2.12 - val dest_tuple': int list list -> term -> term list
2.13 - val prodT_factors': int list list -> typ -> typ list
2.14 - val ap_split': int list list -> typ -> typ -> term -> term
2.15 - val mk_tuple': int list list -> typ -> term list -> term
2.16 + val flatten_tupleT: typ -> typ list
2.17 val mk_tupleT: int list list -> typ list -> typ
2.18 - val strip_split: term -> term * typ list * int list list
2.19 + val strip_tupleT: int list list -> typ -> typ list
2.20 + val flat_tupleT_paths: typ -> int list list
2.21 + val mk_tuple: int list list -> typ -> term list -> term
2.22 + val dest_tuple: int list list -> term -> term list
2.23 + val flat_tuple_paths: term -> int list list
2.24 + val mk_splits: int list list -> typ -> typ -> term -> term
2.25 + val strip_splits: term -> term * typ list * int list list
2.26 val natT: typ
2.27 val zero: term
2.28 val is_zero: term -> bool
2.29 @@ -320,95 +318,17 @@
2.30 | _ => raise TERM ("mk_split: bad body type", [t]));
2.31
2.32 (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
2.33 -fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2
2.34 - | prodT_factors T = [T];
2.35 +fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
2.36 + | flatten_tupleT T = [T];
2.37
2.38 -(*Makes a nested tuple from a list, following the product type structure*)
2.39 -fun mk_tuple (Type ("*", [T1, T2])) tms =
2.40 - mk_prod (mk_tuple T1 tms,
2.41 - mk_tuple T2 (Library.drop (length (prodT_factors T1), tms)))
2.42 - | mk_tuple T (t::_) = t;
2.43 +(* tuples with specific arities
2.44
2.45 -fun dest_tuple (Const ("Pair", _) $ t $ u) = dest_tuple t @ dest_tuple u
2.46 - | dest_tuple t = [t];
2.47 -
2.48 -(*In ap_split S T u, term u expects separate arguments for the factors of S,
2.49 - with result type T. The call creates a new term expecting one argument
2.50 - of type S.*)
2.51 -fun ap_split T T3 u =
2.52 - let
2.53 - fun ap (T :: Ts) =
2.54 - (case T of
2.55 - Type ("*", [T1, T2]) =>
2.56 - split_const (T1, T2, Ts ---> T3) $ ap (T1 :: T2 :: Ts)
2.57 - | _ => Abs ("x", T, ap Ts))
2.58 - | ap [] =
2.59 - let val k = length (prodT_factors T)
2.60 - in list_comb (incr_boundvars k u, map Bound (k - 1 downto 0)) end
2.61 - in ap [T] end;
2.62 -
2.63 -
2.64 -(* operations on tuples with specific arities *)
2.65 -(*
2.66 an "arity" of a tuple is a list of lists of integers
2.67 ("factors"), denoting paths to subterms that are pairs
2.68 *)
2.69
2.70 fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
2.71
2.72 -fun prod_factors t =
2.73 - let
2.74 - fun factors p (Const ("Pair", _) $ t $ u) =
2.75 - p :: factors (1::p) t @ factors (2::p) u
2.76 - | factors p _ = []
2.77 - in factors [] t end;
2.78 -
2.79 -fun dest_tuple' ps =
2.80 - let
2.81 - fun dest p t = if p mem ps then (case t of
2.82 - Const ("Pair", _) $ t $ u =>
2.83 - dest (1::p) t @ dest (2::p) u
2.84 - | _ => prod_err "dest_tuple'") else [t]
2.85 - in dest [] end;
2.86 -
2.87 -fun prodT_factors' ps =
2.88 - let
2.89 - fun factors p T = if p mem ps then (case T of
2.90 - Type ("*", [T1, T2]) =>
2.91 - factors (1::p) T1 @ factors (2::p) T2
2.92 - | _ => prod_err "prodT_factors'") else [T]
2.93 - in factors [] end;
2.94 -
2.95 -(*In ap_split' ps S T u, term u expects separate arguments for the factors of S,
2.96 - with result type T. The call creates a new term expecting one argument
2.97 - of type S.*)
2.98 -fun ap_split' ps T T3 u =
2.99 - let
2.100 - fun ap ((p, T) :: pTs) =
2.101 - if p mem ps then (case T of
2.102 - Type ("*", [T1, T2]) =>
2.103 - split_const (T1, T2, map snd pTs ---> T3) $
2.104 - ap ((1::p, T1) :: (2::p, T2) :: pTs)
2.105 - | _ => prod_err "ap_split'")
2.106 - else Abs ("x", T, ap pTs)
2.107 - | ap [] =
2.108 - let val k = length ps
2.109 - in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
2.110 - in ap [([], T)] end;
2.111 -
2.112 -fun mk_tuple' ps =
2.113 - let
2.114 - fun mk p T ts =
2.115 - if p mem ps then (case T of
2.116 - Type ("*", [T1, T2]) =>
2.117 - let
2.118 - val (t, ts') = mk (1::p) T1 ts;
2.119 - val (u, ts'') = mk (2::p) T2 ts'
2.120 - in (pair_const T1 T2 $ t $ u, ts'') end
2.121 - | _ => prod_err "mk_tuple'")
2.122 - else (hd ts, tl ts)
2.123 - in fst oo mk [] end;
2.124 -
2.125 fun mk_tupleT ps =
2.126 let
2.127 fun mk p Ts =
2.128 @@ -420,7 +340,67 @@
2.129 else (hd Ts, tl Ts)
2.130 in fst o mk [] end;
2.131
2.132 -fun strip_split t =
2.133 +fun strip_tupleT ps =
2.134 + let
2.135 + fun factors p T = if p mem ps then (case T of
2.136 + Type ("*", [T1, T2]) =>
2.137 + factors (1::p) T1 @ factors (2::p) T2
2.138 + | _ => prod_err "strip_tupleT") else [T]
2.139 + in factors [] end;
2.140 +
2.141 +val flat_tupleT_paths =
2.142 + let
2.143 + fun factors p (Type ("*", [T1, T2])) =
2.144 + p :: factors (1::p) T1 @ factors (2::p) T2
2.145 + | factors p _ = []
2.146 + in factors [] end;
2.147 +
2.148 +fun mk_tuple ps =
2.149 + let
2.150 + fun mk p T ts =
2.151 + if p mem ps then (case T of
2.152 + Type ("*", [T1, T2]) =>
2.153 + let
2.154 + val (t, ts') = mk (1::p) T1 ts;
2.155 + val (u, ts'') = mk (2::p) T2 ts'
2.156 + in (pair_const T1 T2 $ t $ u, ts'') end
2.157 + | _ => prod_err "mk_tuple")
2.158 + else (hd ts, tl ts)
2.159 + in fst oo mk [] end;
2.160 +
2.161 +fun dest_tuple ps =
2.162 + let
2.163 + fun dest p t = if p mem ps then (case t of
2.164 + Const ("Pair", _) $ t $ u =>
2.165 + dest (1::p) t @ dest (2::p) u
2.166 + | _ => prod_err "dest_tuple") else [t]
2.167 + in dest [] end;
2.168 +
2.169 +val flat_tuple_paths =
2.170 + let
2.171 + fun factors p (Const ("Pair", _) $ t $ u) =
2.172 + p :: factors (1::p) t @ factors (2::p) u
2.173 + | factors p _ = []
2.174 + in factors [] end;
2.175 +
2.176 +(*In mk_splits ps S T u, term u expects separate arguments for the factors of S,
2.177 + with result type T. The call creates a new term expecting one argument
2.178 + of type S.*)
2.179 +fun mk_splits ps T T3 u =
2.180 + let
2.181 + fun ap ((p, T) :: pTs) =
2.182 + if p mem ps then (case T of
2.183 + Type ("*", [T1, T2]) =>
2.184 + split_const (T1, T2, map snd pTs ---> T3) $
2.185 + ap ((1::p, T1) :: (2::p, T2) :: pTs)
2.186 + | _ => prod_err "mk_splits")
2.187 + else Abs ("x", T, ap pTs)
2.188 + | ap [] =
2.189 + let val k = length ps
2.190 + in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
2.191 + in ap [([], T)] end;
2.192 +
2.193 +val strip_splits =
2.194 let
2.195 fun strip [] qs Ts t = (t, Ts, qs)
2.196 | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
2.197 @@ -429,7 +409,7 @@
2.198 | strip (p :: ps) qs Ts t = strip ps qs
2.199 (hd (binder_types (fastype_of1 (Ts, t))) :: Ts)
2.200 (incr_boundvars 1 t $ Bound 0)
2.201 - in strip [[]] [] [] t end;
2.202 + in strip [[]] [] [] end;
2.203
2.204
2.205 (* nat *)
3.1 --- a/src/HOL/Tools/inductive_codegen.ML Thu Jul 30 23:06:06 2009 +0200
3.2 +++ b/src/HOL/Tools/inductive_codegen.ML Thu Jul 30 23:09:29 2009 +0200
3.3 @@ -645,7 +645,7 @@
3.4
3.5 fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of
3.6 (Const ("Collect", _), [u]) =>
3.7 - let val (r, Ts, fs) = HOLogic.strip_split u
3.8 + let val (r, Ts, fs) = HOLogic.strip_splits u
3.9 in case strip_comb r of
3.10 (Const (s, T), ts) =>
3.11 (case (get_clauses thy s, get_assoc_code thy (s, T)) of
4.1 --- a/src/HOL/Tools/inductive_set.ML Thu Jul 30 23:06:06 2009 +0200
4.2 +++ b/src/HOL/Tools/inductive_set.ML Thu Jul 30 23:09:29 2009 +0200
4.3 @@ -33,10 +33,10 @@
4.4 val collect_mem_simproc =
4.5 Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
4.6 fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
4.7 - let val (u, Ts, ps) = HOLogic.strip_split t
4.8 + let val (u, Ts, ps) = HOLogic.strip_splits t
4.9 in case u of
4.10 (c as Const ("op :", _)) $ q $ S' =>
4.11 - (case try (HOLogic.dest_tuple' ps) q of
4.12 + (case try (HOLogic.dest_tuple ps) q of
4.13 NONE => NONE
4.14 | SOME ts =>
4.15 if not (loose_bvar (S', 0)) andalso
4.16 @@ -79,7 +79,7 @@
4.17 fun mk_collect p T t =
4.18 let val U = HOLogic.dest_setT T
4.19 in HOLogic.Collect_const U $
4.20 - HOLogic.ap_split' (HOLogic.prod_factors p) U HOLogic.boolT t
4.21 + HOLogic.mk_splits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
4.22 end;
4.23 fun decomp (Const (s, _) $ ((m as Const ("op :",
4.24 Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
4.25 @@ -223,11 +223,11 @@
4.26 map (fn (x, ps) =>
4.27 let
4.28 val U = HOLogic.dest_setT (fastype_of x);
4.29 - val x' = map_type (K (HOLogic.prodT_factors' ps U ---> HOLogic.boolT)) x
4.30 + val x' = map_type (K (HOLogic.strip_tupleT ps U ---> HOLogic.boolT)) x
4.31 in
4.32 (cterm_of thy x,
4.33 cterm_of thy (HOLogic.Collect_const U $
4.34 - HOLogic.ap_split' ps U HOLogic.boolT x'))
4.35 + HOLogic.mk_splits ps U HOLogic.boolT x'))
4.36 end) fs;
4.37
4.38 fun mk_to_pred_eq p fs optfs' T thm =
4.39 @@ -240,7 +240,7 @@
4.40 | SOME fs' =>
4.41 let
4.42 val (_, U) = split_last (binder_types T);
4.43 - val Ts = HOLogic.prodT_factors' fs' U;
4.44 + val Ts = HOLogic.strip_tupleT fs' U;
4.45 (* FIXME: should cterm_instantiate increment indexes? *)
4.46 val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
4.47 val (arg_cong_f, _) = arg_cong' |> cprop_of |> Drule.strip_imp_concl |>
4.48 @@ -248,7 +248,7 @@
4.49 in
4.50 thm' RS (Drule.cterm_instantiate [(arg_cong_f,
4.51 cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
4.52 - HOLogic.Collect_const U $ HOLogic.ap_split' fs' U
4.53 + HOLogic.Collect_const U $ HOLogic.mk_splits fs' U
4.54 HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
4.55 end)
4.56 in
4.57 @@ -270,7 +270,7 @@
4.58 fun factors_of t fs = case strip_abs_body t of
4.59 Const ("op :", _) $ u $ S =>
4.60 if is_Free S orelse is_Var S then
4.61 - let val ps = HOLogic.prod_factors u
4.62 + let val ps = HOLogic.flat_tuple_paths u
4.63 in (SOME ps, (S, ps) :: fs) end
4.64 else (NONE, fs)
4.65 | _ => (NONE, fs);
4.66 @@ -279,7 +279,7 @@
4.67 val ((h', ts'), fs') = (case rhs of
4.68 Abs _ => (case strip_abs_body rhs of
4.69 Const ("op :", _) $ u $ S =>
4.70 - (strip_comb S, SOME (HOLogic.prod_factors u))
4.71 + (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
4.72 | _ => error "member symbol on right-hand side expected")
4.73 | _ => (strip_comb rhs, NONE))
4.74 in
4.75 @@ -366,7 +366,7 @@
4.76 in
4.77 (cterm_of thy x,
4.78 cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
4.79 - (HOLogic.mk_tuple' ps T (map Bound (length ps downto 0)), x'))))
4.80 + (HOLogic.mk_tuple ps T (map Bound (length ps downto 0)), x'))))
4.81 end) fs
4.82 in
4.83 thm |>
4.84 @@ -412,7 +412,7 @@
4.85 PredSetConvData.get (Context.Proof ctxt);
4.86 fun infer (Abs (_, _, t)) = infer t
4.87 | infer (Const ("op :", _) $ t $ u) =
4.88 - infer_arities thy set_arities (SOME (HOLogic.prod_factors t), u)
4.89 + infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
4.90 | infer (t $ u) = infer t #> infer u
4.91 | infer _ = I;
4.92 val new_arities = filter_out
4.93 @@ -422,14 +422,14 @@
4.94 SOME fs =>
4.95 let
4.96 val T = HOLogic.dest_setT (fastype_of x);
4.97 - val Ts = HOLogic.prodT_factors' fs T;
4.98 + val Ts = HOLogic.strip_tupleT fs T;
4.99 val x' = map_type (K (Ts ---> HOLogic.boolT)) x
4.100 in
4.101 (x, (x',
4.102 (HOLogic.Collect_const T $
4.103 - HOLogic.ap_split' fs T HOLogic.boolT x',
4.104 + HOLogic.mk_splits fs T HOLogic.boolT x',
4.105 list_abs (map (pair "x") Ts, HOLogic.mk_mem
4.106 - (HOLogic.mk_tuple' fs T (map Bound (length fs downto 0)),
4.107 + (HOLogic.mk_tuple fs T (map Bound (length fs downto 0)),
4.108 x)))))
4.109 end
4.110 | NONE => (x, (x, (x, x))))) params;
4.111 @@ -448,13 +448,13 @@
4.112 Pretty.str ("of " ^ s ^ " do not agree with types"),
4.113 Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
4.114 Pretty.str "of declared parameters"]));
4.115 - val Ts = HOLogic.prodT_factors' fs U;
4.116 + val Ts = HOLogic.strip_tupleT fs U;
4.117 val c' = Free (s ^ "p",
4.118 map fastype_of params1 @ Ts ---> HOLogic.boolT)
4.119 in
4.120 ((c', (fs, U, Ts)),
4.121 (list_comb (c, params2),
4.122 - HOLogic.Collect_const U $ HOLogic.ap_split' fs U HOLogic.boolT
4.123 + HOLogic.Collect_const U $ HOLogic.mk_splits fs U HOLogic.boolT
4.124 (list_comb (c', params1))))
4.125 end) |> split_list |>> split_list;
4.126 val eqns' = eqns @
4.127 @@ -484,7 +484,7 @@
4.128 val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
4.129 (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
4.130 fold_rev lambda params (HOLogic.Collect_const U $
4.131 - HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
4.132 + HOLogic.mk_splits fs U HOLogic.boolT (list_comb (p, params3))))))
4.133 (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
4.134
4.135 (* prove theorems for converting predicate to set notation *)
4.136 @@ -495,7 +495,7 @@
4.137 (HOLogic.mk_Trueprop (HOLogic.mk_eq
4.138 (list_comb (p, params3),
4.139 list_abs (map (pair "x") Ts, HOLogic.mk_mem
4.140 - (HOLogic.mk_tuple' fs U (map Bound (length fs downto 0)),
4.141 + (HOLogic.mk_tuple fs U (map Bound (length fs downto 0)),
4.142 list_comb (c, params))))))
4.143 (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
4.144 [def, mem_Collect_eq, split_conv]) 1))
5.1 --- a/src/HOL/Tools/split_rule.ML Thu Jul 30 23:06:06 2009 +0200
5.2 +++ b/src/HOL/Tools/split_rule.ML Thu Jul 30 23:09:29 2009 +0200
5.3 @@ -50,13 +50,13 @@
5.4 internal_split_const (T1, T2, T3) $
5.5 Abs ("v", T1,
5.6 ap_split T2 T3
5.7 - ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
5.8 + ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $
5.9 Bound 0))
5.10 | ap_split T T3 u = u;
5.11
5.12 (*Curries any Var of function type in the rule*)
5.13 fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
5.14 - let val T' = HOLogic.prodT_factors T1 ---> T2;
5.15 + let val T' = HOLogic.flatten_tupleT T1 ---> T2;
5.16 val newt = ap_split T1 T2 (Var (v, T'));
5.17 val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
5.18 in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
5.19 @@ -66,7 +66,7 @@
5.20 (* complete splitting of partially splitted rules *)
5.21
5.22 fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
5.23 - (ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U)
5.24 + (ap_split T (maps HOLogic.flatten_tupleT Ts ---> U)
5.25 (incr_boundvars 1 u) $ Bound 0))
5.26 | ap_split' _ _ u = u;
5.27
5.28 @@ -76,12 +76,12 @@
5.29 val (Us', U') = strip_type T;
5.30 val Us = Library.take (length ts, Us');
5.31 val U = Library.drop (length ts, Us') ---> U';
5.32 - val T' = List.concat (map HOLogic.prodT_factors Us) ---> U;
5.33 + val T' = maps HOLogic.flatten_tupleT Us ---> U;
5.34 fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
5.35 let
5.36 - val Ts = HOLogic.prodT_factors T;
5.37 + val Ts = HOLogic.flatten_tupleT T;
5.38 val ys = Name.variant_list xs (replicate (length Ts) a);
5.39 - in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
5.40 + in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple (HOLogic.flat_tupleT_paths T) T
5.41 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
5.42 end
5.43 | mk_tuple _ x = x;
6.1 --- a/src/HOL/ex/predicate_compile.ML Thu Jul 30 23:06:06 2009 +0200
6.2 +++ b/src/HOL/ex/predicate_compile.ML Thu Jul 30 23:09:29 2009 +0200
6.3 @@ -1531,7 +1531,7 @@
6.4 let
6.5 val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
6.6 | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
6.7 - val (body, Ts, fp) = HOLogic.strip_split split;
6.8 + val (body, Ts, fp) = HOLogic.strip_splits split;
6.9 (*FIXME former order of tuple positions must be restored*)
6.10 val (pred as Const (name, T), all_args) = strip_comb body
6.11 val (params, args) = chop (nparams_of thy name) all_args