(* Title: ZF/Tools/cartprod.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
Signatures for inductive definitions.
Syntactic operations for Cartesian Products.
*)
signature FP = (** Description of a fixed point operator **)
sig
val oper : term (*fixed point operator*)
val bnd_mono : term (*monotonicity predicate*)
val bnd_monoI : thm (*intro rule for bnd_mono*)
val subs : thm (*subset theorem for fp*)
val Tarski : thm (*Tarski's fixed point theorem*)
val induct : thm (*induction/coinduction rule*)
end;
signature SU = (** Description of a disjoint sum **)
sig
val sum : term (*disjoint sum operator*)
val inl : term (*left injection*)
val inr : term (*right injection*)
val elim : term (*case operator*)
val case_inl : thm (*inl equality rule for case*)
val case_inr : thm (*inr equality rule for case*)
val inl_iff : thm (*injectivity of inl, using <->*)
val inr_iff : thm (*injectivity of inr, using <->*)
val distinct : thm (*distinctness of inl, inr using <->*)
val distinct' : thm (*distinctness of inr, inl using <->*)
val free_SEs : thm list (*elim rules for SU, and pair_iff!*)
end;
signature PR = (** Description of a Cartesian product **)
sig
val sigma : term (*Cartesian product operator*)
val pair : term (*pairing operator*)
val split_name : string (*name of polymorphic split*)
val pair_iff : thm (*injectivity of pairing, using <->*)
val split_eq : thm (*equality rule for split*)
val fsplitI : thm (*intro rule for fsplit*)
val fsplitD : thm (*destruct rule for fsplit*)
val fsplitE : thm (*elim rule; apparently never used*)
end;
signature CARTPROD = (** Derived syntactic functions for produts **)
sig
val ap_split : typ -> typ -> term -> term
val factors : typ -> typ list
val mk_prod : typ * typ -> typ
val mk_tuple : term -> typ -> term list -> term
val pseudo_type : term -> typ
val remove_split : Proof.context -> thm -> thm
val split_const : typ -> term
val split_rule_var : Proof.context -> term * typ * thm -> thm
end;
functor CartProd_Fun (Pr: PR) : CARTPROD =
struct
(* Some of these functions expect "pseudo-types" containing products,
as in HOL; the true ZF types would just be "i" *)
fun mk_prod (T1,T2) = Type("*", [T1,T2]);
(*Bogus product type underlying a (possibly nested) Sigma.
Lets us share HOL code*)
fun pseudo_type (t $ A $ Abs(_,_,B)) =
if t = Pr.sigma
then mk_prod(pseudo_type A, pseudo_type B)
else \<^typ>\<open>i\<close>
| pseudo_type _ = \<^typ>\<open>i\<close>;
(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
fun factors (Type("*", [T1, T2])) = factors T1 @ factors T2
| factors T = [T];
(*Make a well-typed instance of "split"*)
fun split_const T = Const(Pr.split_name,
[[Ind_Syntax.iT, Ind_Syntax.iT]--->T,
Ind_Syntax.iT] ---> 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 (Type("*", [T1,T2])) T3 u =
split_const T3 $
Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
ap_split T2 T3
((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $
Bound 0))
| ap_split T T3 u = u;
(*Makes a nested tuple from a list, following the product type structure*)
fun mk_tuple pair (Type("*", [T1,T2])) tms =
pair $ mk_tuple pair T1 tms
$ mk_tuple pair T2 (drop (length (factors T1)) tms)
| mk_tuple pair T (t::_) = t;
(*Attempts to remove occurrences of split, and pair-valued parameters*)
fun remove_split ctxt = rewrite_rule ctxt [Pr.split_eq];
(*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
fun split_rule_var ctxt (Var(v,_), Type("fun",[T1,T2]), rl) =
let val T' = factors T1 ---> T2
val newt = ap_split T1 T2 (Var(v,T'))
in
remove_split ctxt
(Drule.instantiate_normalize ([],
[((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl)
end
| split_rule_var _ (t,T,rl) = rl;
end;