# HG changeset patch # User paulson # Date 914860622 -3600 # Node ID 7fef0169ab5ebcb9cd49d81b3b2c6dc1f2fe486a # Parent 88e6e55dd1682422381d179983fae140788f067c moved from ZF to new subdirectory Tools diff -r 88e6e55dd168 -r 7fef0169ab5e src/ZF/Tools/cartprod.ML --- /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; + diff -r 88e6e55dd168 -r 7fef0169ab5e src/ZF/Tools/typechk.ML --- /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)); +