6049
|
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 |
Signatures for inductive definitions
|
|
7 |
|
|
8 |
Syntactic operations for Cartesian Products
|
|
9 |
*)
|
|
10 |
|
|
11 |
signature FP = (** Description of a fixed point operator **)
|
|
12 |
sig
|
|
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*)
|
|
19 |
end;
|
|
20 |
|
|
21 |
signature SU = (** Description of a disjoint sum **)
|
|
22 |
sig
|
|
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!*)
|
|
34 |
end;
|
|
35 |
|
|
36 |
signature PR = (** Description of a Cartesian product **)
|
|
37 |
sig
|
|
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*)
|
|
46 |
end;
|
|
47 |
|
|
48 |
signature CARTPROD = (** Derived syntactic functions for produts **)
|
|
49 |
sig
|
|
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
|
|
58 |
end;
|
|
59 |
|
|
60 |
|
|
61 |
functor CartProd_Fun (Pr: PR) : CARTPROD =
|
|
62 |
struct
|
|
63 |
|
|
64 |
(* Some of these functions expect "pseudo-types" containing products,
|
|
65 |
as in HOL; the true ZF types would just be "i" *)
|
|
66 |
|
|
67 |
fun mk_prod (T1,T2) = Type("*", [T1,T2]);
|
|
68 |
|
|
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)
|
|
73 |
else Ind_Syntax.iT
|
|
74 |
| pseudo_type _ = Ind_Syntax.iT;
|
|
75 |
|
|
76 |
(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
|
|
77 |
fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
|
|
78 |
| factors T = [T];
|
|
79 |
|
|
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);
|
|
84 |
|
|
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
|
|
87 |
of type S.*)
|
|
88 |
fun ap_split (Type("*", [T1,T2])) T3 u =
|
|
89 |
split_const T3 $
|
|
90 |
Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
|
|
91 |
ap_split T2 T3
|
|
92 |
((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $
|
|
93 |
Bound 0))
|
|
94 |
| ap_split T T3 u = u;
|
|
95 |
|
|
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 (drop (length (factors T1), tms)))
|
|
100 |
| mk_tuple pair T (t::_) = t;
|
|
101 |
|
|
102 |
(*Attempts to remove occurrences of split, and pair-valued parameters*)
|
|
103 |
val remove_split = rewrite_rule [Pr.split_eq];
|
|
104 |
|
|
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))
|
|
110 |
in
|
|
111 |
remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
|
|
112 |
cterm newt)]) rl)
|
|
113 |
end
|
|
114 |
| split_rule_var (t,T,rl) = rl;
|
|
115 |
|
|
116 |
end;
|
|
117 |
|