1 (* Title: ZF/cartprod.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 Syntactic operations for Cartesian Products |
|
7 *) |
|
8 |
|
9 signature PR = (** Description of a Cartesian product **) |
|
10 sig |
|
11 val sigma : term (*Cartesian product operator*) |
|
12 val pair : term (*pairing operator*) |
|
13 val split_name : string (*name of polymorphic split*) |
|
14 val pair_iff : thm (*injectivity of pairing, using <->*) |
|
15 val split_eq : thm (*equality rule for split*) |
|
16 val fsplitI : thm (*intro rule for fsplit*) |
|
17 val fsplitD : thm (*destruct rule for fsplit*) |
|
18 val fsplitE : thm (*elim rule; apparently never used*) |
|
19 end; |
|
20 |
|
21 signature CARTPROD = (** Derived syntactic functions for produts **) |
|
22 sig |
|
23 val ap_split : typ -> typ -> term -> term |
|
24 val factors : typ -> typ list |
|
25 val mk_prod : typ * typ -> typ |
|
26 val mk_tuple : term -> typ -> term list -> term |
|
27 val pseudo_type : term -> typ |
|
28 val remove_split : thm -> thm |
|
29 val split_const : typ -> term |
|
30 val split_rule_var : term * typ * thm -> thm |
|
31 end; |
|
32 |
|
33 |
|
34 functor CartProd_Fun (Pr: PR) : CARTPROD = |
|
35 struct |
|
36 |
|
37 (* Some of these functions expect "pseudo-types" containing products, |
|
38 as in HOL; the true ZF types would just be "i" *) |
|
39 |
|
40 fun mk_prod (T1,T2) = Type("*", [T1,T2]); |
|
41 |
|
42 (*Bogus product type underlying a (possibly nested) Sigma. |
|
43 Lets us share HOL code*) |
|
44 fun pseudo_type (t $ A $ Abs(_,_,B)) = |
|
45 if t = Pr.sigma then mk_prod(pseudo_type A, pseudo_type B) |
|
46 else Ind_Syntax.iT |
|
47 | pseudo_type _ = Ind_Syntax.iT; |
|
48 |
|
49 (*Maps the type T1*...*Tn to [T1,...,Tn], however nested*) |
|
50 fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2 |
|
51 | factors T = [T]; |
|
52 |
|
53 (*Make a well-typed instance of "split"*) |
|
54 fun split_const T = Const(Pr.split_name, |
|
55 [[Ind_Syntax.iT, Ind_Syntax.iT]--->T, |
|
56 Ind_Syntax.iT] ---> T); |
|
57 |
|
58 (*In ap_split S T u, term u expects separate arguments for the factors of S, |
|
59 with result type T. The call creates a new term expecting one argument |
|
60 of type S.*) |
|
61 fun ap_split (Type("*", [T1,T2])) T3 u = |
|
62 split_const T3 $ |
|
63 Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*) |
|
64 ap_split T2 T3 |
|
65 ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ |
|
66 Bound 0)) |
|
67 | ap_split T T3 u = u; |
|
68 |
|
69 (*Makes a nested tuple from a list, following the product type structure*) |
|
70 fun mk_tuple pair (Type("*", [T1,T2])) tms = |
|
71 pair $ (mk_tuple pair T1 tms) |
|
72 $ (mk_tuple pair T2 (drop (length (factors T1), tms))) |
|
73 | mk_tuple pair T (t::_) = t; |
|
74 |
|
75 (*Attempts to remove occurrences of split, and pair-valued parameters*) |
|
76 val remove_split = rewrite_rule [Pr.split_eq]; |
|
77 |
|
78 (*Uncurries any Var according to its "pseudo-product type" T1 in the rule*) |
|
79 fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) = |
|
80 let val T' = factors T1 ---> T2 |
|
81 val newt = ap_split T1 T2 (Var(v,T')) |
|
82 val cterm = Thm.cterm_of (#sign(rep_thm rl)) |
|
83 in |
|
84 remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), |
|
85 cterm newt)]) rl) |
|
86 end |
|
87 | split_rule_var (t,T,rl) = rl; |
|
88 |
|
89 end; |
|
90 |
|