author  nipkow 
Wed, 10 May 1995 08:38:52 +0200  
changeset 1116  7fca5aabcbb0 
parent 1106  62bdb9e5722b 
child 1155  928a16e02f9f 
permissions  rwrr 
615  1 
(* Title: ZF/ZF.thy 
0  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
ZermeloFraenkel Set Theory 

7 
*) 

8 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

9 
ZF = FOL + Let + 
0  10 

11 
types 

615  12 
i 
0  13 

14 
arities 

15 
i :: term 

16 

17 
consts 

18 

675
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

19 
"0" :: "i" ("0") (*the empty set*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

20 
Pow :: "i => i" (*power sets*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

21 
Inf :: "i" (*infinite set*) 
0  22 

23 
(* Bounded Quantifiers *) 

24 

675
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

25 
Ball, Bex :: "[i, i => o] => o" 
0  26 

27 
(* General Union and Intersection *) 

28 

675
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

29 
Union,Inter :: "i => i" 
0  30 

31 
(* Variations on Replacement *) 

32 

675
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

33 
PrimReplace :: "[i, [i, i] => o] => i" 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

34 
Replace :: "[i, [i, i] => o] => i" 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

35 
RepFun :: "[i, i => i] => i" 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

36 
Collect :: "[i, i => o] => i" 
0  37 

38 
(* Descriptions *) 

39 

675
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

40 
The :: "(i => o) => i" (binder "THE " 10) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

41 
if :: "[o, i, i] => i" 
0  42 

43 
(* Finite Sets *) 

44 

675
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

45 
Upair, cons :: "[i, i] => i" 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

46 
succ :: "i => i" 
0  47 

615  48 
(* Ordered Pairing *) 
0  49 

675
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

50 
Pair :: "[i, i] => i" 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

51 
fst, snd :: "i => i" 
1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

52 
split :: "[[i, i] => 'a, i] => 'a::logic" (*for patternmatching*) 
0  53 

54 
(* Sigma and Pi Operators *) 

55 

675
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

56 
Sigma, Pi :: "[i, i => i] => i" 
0  57 

58 
(* Relations and Functions *) 

59 

675
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

60 
domain :: "i => i" 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

61 
range :: "i => i" 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

62 
field :: "i => i" 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

63 
converse :: "i => i" 
690  64 
function :: "i => o" (*is a relation a function?*) 
675
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

65 
Lambda :: "[i, i => i] => i" 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

66 
restrict :: "[i, i] => i" 
0  67 

68 
(* Infixes in order of decreasing precedence *) 

69 

675
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

70 
"``" :: "[i, i] => i" (infixl 90) (*image*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

71 
"``" :: "[i, i] => i" (infixl 90) (*inverse image*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

72 
"`" :: "[i, i] => i" (infixl 90) (*function application*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

73 
(*"*" :: "[i, i] => i" (infixr 80) (*Cartesian product*)*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

74 
"Int" :: "[i, i] => i" (infixl 70) (*binary intersection*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

75 
"Un" :: "[i, i] => i" (infixl 65) (*binary union*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

76 
"" :: "[i, i] => i" (infixl 65) (*set difference*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

77 
(*">" :: "[i, i] => i" (infixr 60) (*function space*)*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

78 
"<=" :: "[i, i] => o" (infixl 50) (*subset relation*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

79 
":" :: "[i, i] => o" (infixl 50) (*membership relation*) 
59a4fa76b590
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp
parents:
632
diff
changeset

80 
(*"~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*)*) 
0  81 

82 

615  83 
types 
84 
is 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

85 
pttrns 
615  86 

87 
syntax 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

88 
"" :: "i => is" ("_") 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

89 
"@Enum" :: "[i, is] => is" ("_,/ _") 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

90 
"~:" :: "[i, i] => o" (infixl 50) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

91 
"@Finset" :: "is => i" ("{(_)}") 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

92 
"@Tuple" :: "[i, is] => i" ("<(_,/ _)>") 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

93 
"@Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})") 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

94 
"@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})") 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

95 
"@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51]) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

96 
"@INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

97 
"@UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

98 
"@PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

99 
"@SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

100 
">" :: "[i, i] => i" (infixr 60) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

101 
"*" :: "[i, i] => i" (infixr 80) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

102 
"@lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

103 
"@Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

104 
"@Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

105 

62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

106 
(** Patterns  extends predefined type "pttrn" used in abstractions **) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

107 

62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

108 
"@pttrn" :: "pttrns => pttrn" ("<_>") 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

109 
"" :: " pttrn => pttrns" ("_") 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

110 
"@pttrns" :: "[pttrn,pttrns] => pttrns" ("_,/_") 
615  111 

0  112 
translations 
615  113 
"x ~: y" == "~ (x : y)" 
0  114 
"{x, xs}" == "cons(x, {xs})" 
115 
"{x}" == "cons(x, 0)" 

116 
"{x:A. P}" == "Collect(A, %x. P)" 

117 
"{y. x:A, Q}" == "Replace(A, %x y. Q)" 

615  118 
"{b. x:A}" == "RepFun(A, %x. b)" 
0  119 
"INT x:A. B" == "Inter({B. x:A})" 
120 
"UN x:A. B" == "Union({B. x:A})" 

121 
"PROD x:A. B" => "Pi(A, %x. B)" 

122 
"SUM x:A. B" => "Sigma(A, %x. B)" 

49  123 
"A > B" => "Pi(A, _K(B))" 
124 
"A * B" => "Sigma(A, _K(B))" 

0  125 
"lam x:A. f" == "Lambda(A, %x. f)" 
126 
"ALL x:A. P" == "Ball(A, %x. P)" 

127 
"EX x:A. P" == "Bex(A, %x. P)" 

37  128 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

129 
"<x, y, z>" == "<x, <y, z>>" 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

130 
"<x, y>" == "Pair(x, y)" 
1116  131 
"%<x,y,zs>.b" == "split(%x <y,zs>.b)" 
132 
"%<x,y>.b" == "split(%x y.b)" 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

133 
(* The <= direction fails if split has more than one argument because 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

134 
astmatching fails. Otherwise it would work fine *) 
0  135 

690  136 
defs 
0  137 

615  138 
(* Bounded Quantifiers *) 
139 
Ball_def "Ball(A, P) == ALL x. x:A > P(x)" 

140 
Bex_def "Bex(A, P) == EX x. x:A & P(x)" 

690  141 

615  142 
subset_def "A <= B == ALL x:A. x:B" 
690  143 
succ_def "succ(i) == cons(i, i)" 
144 

145 
rules 

0  146 

615  147 
(* ZF axioms  see Suppes p.238 
148 
Axioms for Union, Pow and Replace state existence only, 

149 
uniqueness is derivable using extensionality. *) 

0  150 

615  151 
extension "A = B <> A <= B & B <= A" 
152 
Union_iff "A : Union(C) <> (EX B:C. A:B)" 

153 
Pow_iff "A : Pow(B) <> A <= B" 

0  154 

615  155 
(*We may name this set, though it is not uniquely defined.*) 
156 
infinity "0:Inf & (ALL y:Inf. succ(y): Inf)" 

0  157 

615  158 
(*This formulation facilitates case analysis on A.*) 
159 
foundation "A=0  (EX x:A. ALL y:x. y~:A)" 

0  160 

615  161 
(*Schema axiom since predicate P is a higherorder variable*) 
162 
replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) > y=z) ==> \ 

163 
\ b : PrimReplace(A,P) <> (EX x:A. P(x,b))" 

164 

690  165 
defs 
166 

615  167 
(* Derived form of replacement, restricting P to its functional part. 
168 
The resulting set (for functional P) is the same as with 

169 
PrimReplace, but the rules are simpler. *) 

0  170 

615  171 
Replace_def "Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))" 
172 

173 
(* Functional form of replacement  analgous to ML's map functional *) 

0  174 

615  175 
RepFun_def "RepFun(A,f) == {y . x:A, y=f(x)}" 
0  176 

615  177 
(* Separation and Pairing can be derived from the Replacement 
178 
and Powerset Axioms using the following definitions. *) 

0  179 

615  180 
Collect_def "Collect(A,P) == {y . x:A, x=y & P(x)}" 
0  181 

615  182 
(*Unordered pairs (Upair) express binary union/intersection and cons; 
183 
set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*) 

0  184 

615  185 
Upair_def "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a)  (x=Pow(0) & y=b)}" 
186 
cons_def "cons(a,A) == Upair(a,a) Un A" 

187 

188 
(* Difference, general intersection, binary union and small intersection *) 

0  189 

615  190 
Diff_def "A  B == { x:A . ~(x:B) }" 
191 
Inter_def "Inter(A) == { x:Union(A) . ALL y:A. x:y}" 

192 
Un_def "A Un B == Union(Upair(A,B))" 

193 
Int_def "A Int B == Inter(Upair(A,B))" 

0  194 

615  195 
(* Definite descriptions  via Replace over the set "1" *) 
0  196 

615  197 
the_def "The(P) == Union({y . x:{0}, P(y)})" 
198 
if_def "if(P,a,b) == THE z. P & z=a  ~P & z=b" 

0  199 

615  200 
(* Ordered pairs and disjoint union of a family of sets *) 
0  201 

615  202 
(* this "symmetric" definition works better than {{a}, {a,b}} *) 
203 
Pair_def "<a,b> == {{a,a}, {a,b}}" 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

204 
fst_def "fst(p) == THE a. EX b. p=<a,b>" 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

205 
snd_def "snd(p) == THE b. EX a. p=<a,b>" 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

206 
split_def "split(c,p) == c(fst(p), snd(p))" 
615  207 
Sigma_def "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}" 
0  208 

615  209 
(* Operations on relations *) 
0  210 

615  211 
(*converse of relation r, inverse of function*) 
212 
converse_def "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}" 

0  213 

615  214 
domain_def "domain(r) == {x. w:r, EX y. w=<x,y>}" 
215 
range_def "range(r) == domain(converse(r))" 

216 
field_def "field(r) == domain(r) Un range(r)" 

690  217 
function_def "function(r) == ALL x y. <x,y>:r > \ 
218 
\ (ALL y'. <x,y'>:r > y=y')" 

615  219 
image_def "r `` A == {y : range(r) . EX x:A. <x,y> : r}" 
220 
vimage_def "r `` A == converse(r)``A" 

0  221 

615  222 
(* Abstraction, application and Cartesian product of a family of sets *) 
0  223 

615  224 
lam_def "Lambda(A,b) == {<x,b(x)> . x:A}" 
225 
apply_def "f`a == THE y. <a,y> : f" 

690  226 
Pi_def "Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}" 
0  227 

228 
(* Restrict the function f to the domain A *) 

615  229 
restrict_def "restrict(f,A) == lam x:A.f`x" 
0  230 

231 
end 

232 

233 

234 
ML 

235 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

236 
(* Patternmatching and 'Dependent' type operators *) 
1116  237 
(* 
1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

238 
local open Syntax 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

239 

62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

240 
fun pttrn s = const"@pttrn" $ s; 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

241 
fun pttrns s t = const"@pttrns" $ s $ t; 
0  242 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

243 
fun split2(Abs(x,T,t)) = 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

244 
let val (pats,u) = split1 t 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

245 
in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

246 
 split2(Const("split",_) $ r) = 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

247 
let val (pats,s) = split2(r) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

248 
val (pats2,t) = split1(s) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

249 
in (pttrns (pttrn pats) pats2, t) end 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

250 
and split1(Abs(x,T,t)) = (Free(x,T), subst_bounds([free x],t)) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

251 
 split1(Const("split",_)$t) = split2(t); 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

252 

62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

253 
fun split_tr'(t::args) = 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

254 
let val (pats,ft) = split2(t) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

255 
in list_comb(const"_lambda" $ pttrn pats $ ft, args) end; 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

256 

62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

257 
in 
1116  258 
*) 
1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

259 
val print_translation = 
1116  260 
[(*("split", split_tr'),*) 
1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

261 
("Pi", dependent_tr' ("@PROD", "op >")), 
632  262 
("Sigma", dependent_tr' ("@SUM", "op *"))]; 
1116  263 
(* 
1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

264 
end; 
1116  265 
*) 