--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Tools/cartprod.ML Mon Dec 28 16:57:02 1998 +0100
@@ -0,0 +1,117 @@
+(* Title: ZF/cartprod.ML
+ ID: $Id$
+ 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 : thm -> thm
+ val split_const : typ -> term
+ val split_rule_var : 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 Ind_Syntax.iT
+ | pseudo_type _ = Ind_Syntax.iT;
+
+(*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*)
+val remove_split = rewrite_rule [Pr.split_eq];
+
+(*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
+fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
+ let val T' = factors T1 ---> T2
+ val newt = ap_split T1 T2 (Var(v,T'))
+ val cterm = Thm.cterm_of (#sign(rep_thm rl))
+ in
+ remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
+ cterm newt)]) rl)
+ end
+ | split_rule_var (t,T,rl) = rl;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Tools/typechk.ML Mon Dec 28 16:57:02 1998 +0100
@@ -0,0 +1,33 @@
+(* Title: ZF/typechk
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+
+Tactics for type checking -- from CTT
+*)
+
+fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) =
+ not (is_Var (head_of a))
+ | is_rigid_elem _ = false;
+
+(*Try solving a:A by assumption provided a is rigid!*)
+val test_assume_tac = SUBGOAL(fn (prem,i) =>
+ if is_rigid_elem (Logic.strip_assums_concl prem)
+ then assume_tac i else eq_assume_tac i);
+
+(*Type checking solves a:?A (a rigid, ?A maybe flexible).
+ match_tac is too strict; would refuse to instantiate ?A*)
+fun typechk_step_tac tyrls =
+ FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
+
+fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
+
+val ZF_typechecks =
+ [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
+
+(*Instantiates variables in typing conditions.
+ drawback: does not simplify conjunctions*)
+fun type_auto_tac tyrls hyps = SELECT_GOAL
+ (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
+ ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
+