Move towards standard functions.
1 (* Title: ZF/cartprod.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1996 University of Cambridge
6 Signatures for inductive definitions
8 Syntactic operations for Cartesian Products
11 signature FP = (** Description of a fixed point operator **)
13 val oper : term (*fixed point operator*)
14 val bnd_mono : term (*monotonicity predicate*)
15 val bnd_monoI : thm (*intro rule for bnd_mono*)
16 val subs : thm (*subset theorem for fp*)
17 val Tarski : thm (*Tarski's fixed point theorem*)
18 val induct : thm (*induction/coinduction rule*)
21 signature SU = (** Description of a disjoint sum **)
23 val sum : term (*disjoint sum operator*)
24 val inl : term (*left injection*)
25 val inr : term (*right injection*)
26 val elim : term (*case operator*)
27 val case_inl : thm (*inl equality rule for case*)
28 val case_inr : thm (*inr equality rule for case*)
29 val inl_iff : thm (*injectivity of inl, using <->*)
30 val inr_iff : thm (*injectivity of inr, using <->*)
31 val distinct : thm (*distinctness of inl, inr using <->*)
32 val distinct' : thm (*distinctness of inr, inl using <->*)
33 val free_SEs : thm list (*elim rules for SU, and pair_iff!*)
36 signature PR = (** Description of a Cartesian product **)
38 val sigma : term (*Cartesian product operator*)
39 val pair : term (*pairing operator*)
40 val split_name : string (*name of polymorphic split*)
41 val pair_iff : thm (*injectivity of pairing, using <->*)
42 val split_eq : thm (*equality rule for split*)
43 val fsplitI : thm (*intro rule for fsplit*)
44 val fsplitD : thm (*destruct rule for fsplit*)
45 val fsplitE : thm (*elim rule; apparently never used*)
48 signature CARTPROD = (** Derived syntactic functions for produts **)
50 val ap_split : typ -> typ -> term -> term
51 val factors : typ -> typ list
52 val mk_prod : typ * typ -> typ
53 val mk_tuple : term -> typ -> term list -> term
54 val pseudo_type : term -> typ
55 val remove_split : thm -> thm
56 val split_const : typ -> term
57 val split_rule_var : term * typ * thm -> thm
61 functor CartProd_Fun (Pr: PR) : CARTPROD =
64 (* SOME of these functions expect "pseudo-types" containing products,
65 as in HOL; the true ZF types would just be "i" *)
67 fun mk_prod (T1,T2) = Type("*", [T1,T2]);
69 (*Bogus product type underlying a (possibly nested) Sigma.
70 Lets us share HOL code*)
71 fun pseudo_type (t $ A $ Abs(_,_,B)) =
72 if t = Pr.sigma then mk_prod(pseudo_type A, pseudo_type B)
74 | pseudo_type _ = Ind_Syntax.iT;
76 (*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
77 fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
80 (*Make a well-typed instance of "split"*)
81 fun split_const T = Const(Pr.split_name,
82 [[Ind_Syntax.iT, Ind_Syntax.iT]--->T,
83 Ind_Syntax.iT] ---> T);
85 (*In ap_split S T u, term u expects separate arguments for the factors of S,
86 with result type T. The call creates a new term expecting one argument
88 fun ap_split (Type("*", [T1,T2])) T3 u =
90 Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
92 ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $
94 | ap_split T T3 u = u;
96 (*Makes a nested tuple from a list, following the product type structure*)
97 fun mk_tuple pair (Type("*", [T1,T2])) tms =
98 pair $ (mk_tuple pair T1 tms)
99 $ (mk_tuple pair T2 (Library.drop (length (factors T1), tms)))
100 | mk_tuple pair T (t::_) = t;
102 (*Attempts to remove occurrences of split, and pair-valued parameters*)
103 val remove_split = rewrite_rule [Pr.split_eq];
105 (*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
106 fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
107 let val T' = factors T1 ---> T2
108 val newt = ap_split T1 T2 (Var(v,T'))
109 val cterm = Thm.cterm_of (#sign(rep_thm rl))
111 remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
114 | split_rule_var (t,T,rl) = rl;