--- a/src/ZF/AC.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC.thy
+(* Title: ZF/AC.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
The Axiom of Choice
@@ -10,5 +10,5 @@
AC = ZF + "func" +
rules
- AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
+ AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
end
--- a/src/ZF/AC/AC16_WO4.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/AC16_WO4.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/AC16_WO4.thy
+(* Title: ZF/AC/AC16_WO4.thy
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
*)
AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux +
@@ -24,6 +24,6 @@
LL_def "LL(t_n, k, y) == {v Int y. v:MM(t_n, k, y)}"
GG_def "GG(t_n, k, y) == lam v:LL(t_n, k, y).
- (THE w. w:MM(t_n, k, y) & v <= w) - v"
+ (THE w. w:MM(t_n, k, y) & v <= w) - v"
end
--- a/src/ZF/AC/AC18_AC19.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/AC18_AC19.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/AC18_AC19.thy
+(* Title: ZF/AC/AC18_AC19.thy
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
Additional definition used in the proof AC19 ==> AC1 which is a part
of the chain AC1 ==> AC18 ==> AC19 ==> AC1
--- a/src/ZF/AC/AC_Equiv.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/AC_Equiv.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/AC_Equiv.thy
+(* Title: ZF/AC/AC_Equiv.thy
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
Axioms AC1 -- AC19 come from "Equivalents of the Axiom of Choice, II"
by H. Rubin and J.E. Rubin, 1985.
@@ -42,18 +42,18 @@
WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &
- (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
+ (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a
- & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
+ & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->
- well_ord(A,converse(R)))"
+ well_ord(A,converse(R)))"
WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->
- (EX R. well_ord(A,R))"
+ (EX R. well_ord(A,R))"
(* Axioms of Choice *)
@@ -62,64 +62,64 @@
AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)
- --> (EX C. ALL B:A. EX y. B Int C = {y})"
+ --> (EX C. ALL B:A. EX y. B Int C = {y})"
AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.
- ALL x:domain(g). f`(g`x) = x"
+ ALL x:domain(g). f`(g`x) = x"
AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)
- --> (PROD B:A. B)~=0"
+ --> (PROD B:A. B)~=0"
AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)
- --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
+ --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->
- (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
+ (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
AC10_def "AC10(n) == ALL A. (ALL B:A. ~Finite(B)) -->
- (EX f. ALL B:A. (pairwise_disjoint(f`B) &
- sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
+ (EX f. ALL B:A. (pairwise_disjoint(f`B) &
+ sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->
- (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &
- sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
+ (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &
+ sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &
- f`B <= B & f`B lepoll m)"
+ f`B <= B & f`B lepoll m)"
AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.
- f`B~=0 & f`B <= B & f`B lepoll m))"
+ f`B~=0 & f`B <= B & f`B lepoll m))"
AC16_def "AC16(n, k) == ALL A. ~Finite(A) -->
- (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &
- (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
+ (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &
+ (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.
- EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
+ EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->
((INT a:A. UN b:B(a). X(a,b)) =
(UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =
- (UN f:(PROD B:A. B). INT a:A. f`a))"
+ (UN f:(PROD B:A. B). INT a:A. f`a))"
(* Auxiliary definitions used in the above definitions *)
pairwise_disjoint_def "pairwise_disjoint(A)
- == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
+ == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
sets_of_size_between_def "sets_of_size_between(A,m,n)
- == ALL B:A. m lepoll B & B lepoll n"
+ == ALL B:A. m lepoll B & B lepoll n"
end
--- a/src/ZF/AC/DC.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/DC.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/DC.thy
+(* Title: ZF/AC/DC.thy
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
Theory file for the proofs concernind the Axiom of Dependent Choice
*)
@@ -16,13 +16,13 @@
rules
DC_def "DC(a) == ALL X R. R<=Pow(X)*X &
- (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R))
- --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
+ (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R))
+ --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
DC0_def "DC0 == ALL A B R. R <= A*B & R~=0 & range(R) <= domain(R)
- --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
+ --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
ff_def "ff(b, X, Q, R) == transrec(b, %c r.
- THE x. first(x, {x:X. <r``c, x> : R}, Q))"
+ THE x. first(x, {x:X. <r``c, x> : R}, Q))"
end
--- a/src/ZF/AC/HH.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/HH.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/HH.thy
+(* Title: ZF/AC/HH.thy
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
The theory file for the proofs of
AC17 ==> AC1
--- a/src/ZF/AC/Hartog.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/Hartog.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/Hartog.thy
+(* Title: ZF/AC/Hartog.thy
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
Hartog's function.
*)
--- a/src/ZF/AC/OrdQuant.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/OrdQuant.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/OrdQuant.thy
+(* Title: ZF/AC/OrdQuant.thy
ID: $Id$
- Authors: Krzysztof Grabczewski and L C Paulson
+ Authors: Krzysztof Grabczewski and L C Paulson
Quantifiers and union operator for ordinals.
*)
--- a/src/ZF/AC/Transrec2.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/Transrec2.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/Transrec2.thy
+(* Title: ZF/AC/Transrec2.thy
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
Transfinite recursion introduced to handle definitions based on the three
cases of ordinals.
@@ -14,10 +14,10 @@
defs
- transrec2_def "transrec2(alpha, a, b) ==
- transrec(alpha, %i r. if(i=0,
- a, if(EX j. i=succ(j),
- b(THE j. i=succ(j), r`(THE j. i=succ(j))),
- UN j<i. r`j)))"
+ transrec2_def "transrec2(alpha, a, b) ==
+ transrec(alpha, %i r. if(i=0,
+ a, if(EX j. i=succ(j),
+ b(THE j. i=succ(j), r`(THE j. i=succ(j))),
+ UN j<i. r`j)))"
end
--- a/src/ZF/AC/WO6_WO1.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/WO6_WO1.thy
+(* Title: ZF/AC/WO6_WO1.thy
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
The proof of "WO6 ==> WO1".
@@ -20,18 +20,18 @@
defs
NN_def "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a &
- (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
+ (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
uu_def "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
(*Definitions for case 1*)
- vv1_def "vv1(f,m,b) ==
- let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &
- domain(uu(f,b,g,d)) lepoll m));
- d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &
- domain(uu(f,b,g,d)) lepoll m
- in if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
+ vv1_def "vv1(f,m,b) ==
+ let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &
+ domain(uu(f,b,g,d)) lepoll m));
+ d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &
+ domain(uu(f,b,g,d)) lepoll m
+ in if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
@@ -40,7 +40,7 @@
(*Definitions for case 2*)
vv2_def "vv2(f,b,g,s) ==
- if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
+ if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
--- a/src/ZF/AC/first.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/first.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/first.thy
+(* Title: ZF/AC/first.thy
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
Theory helpful in proofs using first element of a well ordered set
*)
@@ -14,5 +14,5 @@
defs
first_def "first(u, X, R)
- == u:X & (ALL v:X. v~=u --> <u,v> : R)"
+ == u:X & (ALL v:X. v~=u --> <u,v> : R)"
end
--- a/src/ZF/AC/recfunAC16.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/recfunAC16.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/recfunAC16.thy
+(* Title: ZF/AC/recfunAC16.thy
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
A recursive definition used in the proof of WO2 ==> AC16
*)
@@ -15,9 +15,9 @@
recfunAC16_def
"recfunAC16(f,fa,i,a) ==
- transrec2(i, 0,
- %g r. if(EX y:r. fa`g <= y, r,
- r Un {f`(LEAST i. fa`g <= f`i &
- (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
+ transrec2(i, 0,
+ %g r. if(EX y:r. fa`g <= y, r,
+ r Un {f`(LEAST i. fa`g <= f`i &
+ (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
end
--- a/src/ZF/Arith.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Arith.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/arith.thy
+(* Title: ZF/arith.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Arithmetic operators and their definitions
@@ -9,11 +9,11 @@
Arith = Epsilon + "simpdata" +
consts
rec :: [i, i, [i,i]=>i]=>i
- "#*" :: [i,i]=>i (infixl 70)
- div :: [i,i]=>i (infixl 70)
- mod :: [i,i]=>i (infixl 70)
- "#+" :: [i,i]=>i (infixl 65)
- "#-" :: [i,i]=>i (infixl 65)
+ "#*" :: [i,i]=>i (infixl 70)
+ div :: [i,i]=>i (infixl 70)
+ mod :: [i,i]=>i (infixl 70)
+ "#+" :: [i,i]=>i (infixl 65)
+ "#-" :: [i,i]=>i (infixl 65)
defs
rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
--- a/src/ZF/Bool.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Bool.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/bool.thy
+(* Title: ZF/bool.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Booleans in Zermelo-Fraenkel Set Theory
@@ -10,24 +10,24 @@
Bool = ZF + "simpdata" +
consts
- "1" :: i ("1")
+ "1" :: i ("1")
"2" :: i ("2")
bool :: i
cond :: [i,i,i]=>i
- not :: i=>i
+ not :: i=>i
"and" :: [i,i]=>i (infixl 70)
- or :: [i,i]=>i (infixl 65)
- xor :: [i,i]=>i (infixl 65)
+ or :: [i,i]=>i (infixl 65)
+ xor :: [i,i]=>i (infixl 65)
translations
"1" == "succ(0)"
"2" == "succ(1)"
defs
- bool_def "bool == {0,1}"
- cond_def "cond(b,c,d) == if(b=1,c,d)"
- not_def "not(b) == cond(b,0,1)"
- and_def "a and b == cond(a,b,0)"
- or_def "a or b == cond(a,1,b)"
- xor_def "a xor b == cond(a,not(b),b)"
+ bool_def "bool == {0,1}"
+ cond_def "cond(b,c,d) == if(b=1,c,d)"
+ not_def "not(b) == cond(b,0,1)"
+ and_def "a and b == cond(a,b,0)"
+ or_def "a or b == cond(a,1,b)"
+ xor_def "a xor b == cond(a,not(b),b)"
end
--- a/src/ZF/Cardinal.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Cardinal.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Cardinal.thy
+(* Title: ZF/Cardinal.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Cardinals in Zermelo-Fraenkel Set Theory
--- a/src/ZF/CardinalArith.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/CardinalArith.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/CardinalArith.thy
+(* Title: ZF/CardinalArith.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Cardinal Arithmetic
--- a/src/ZF/Cardinal_AC.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Cardinal_AC.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Cardinal_AC.thy
+(* Title: ZF/Cardinal_AC.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Cardinal Arithmetic WITH the Axiom of Choice
--- a/src/ZF/Coind/BCR.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Coind/BCR.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Coind/BCR.thy
+(* Title: ZF/Coind/BCR.thy
ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
+ Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
*)
@@ -19,9 +19,9 @@
consts
isofenv :: [i,i] => o
defs
- isofenv_def "isofenv(ve,te) ==
- ve_dom(ve) = te_dom(te) &
- ( ALL x:ve_dom(ve).
+ isofenv_def "isofenv(ve,te) ==
+ ve_dom(ve) = te_dom(te) &
+ ( ALL x:ve_dom(ve).
EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
end
--- a/src/ZF/Coind/Dynamic.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Coind/Dynamic.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Coind/Dynamic.thy
+(* Title: ZF/Coind/Dynamic.thy
ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
+ Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
*)
--- a/src/ZF/Coind/ECR.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Coind/ECR.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Coind/ECR.thy
+(* Title: ZF/Coind/ECR.thy
ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
+ Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
*)
@@ -17,9 +17,9 @@
"[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
htr_closI
"[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv;
- <te,e_fn(x,e),t>:ElabRel;
- ve_dom(ve) = te_dom(te);
- {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)
+ <te,e_fn(x,e),t>:ElabRel;
+ ve_dom(ve) = te_dom(te);
+ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)
|] ==>
<v_clos(x,e,ve),t>:HasTyRel"
monos "[Pow_mono]"
@@ -31,8 +31,8 @@
hastyenv :: [i,i] => o
defs
hastyenv_def
- " hastyenv(ve,te) ==
- ve_dom(ve) = te_dom(te) &
+ " hastyenv(ve,te) ==
+ ve_dom(ve) = te_dom(te) &
(ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
end
--- a/src/ZF/Coind/Language.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Coind/Language.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,14 +1,14 @@
-(* Title: ZF/Coind/Language.thy
+(* Title: ZF/Coind/Language.thy
ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
+ Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
*)
Language ="Datatype" + QUniv +
consts
- Const :: i (* Abstract type of constants *)
- c_app :: [i,i] => i (*Abstract constructor for fun application*)
+ Const :: i (* Abstract type of constants *)
+ c_app :: [i,i] => i (*Abstract constructor for fun application*)
rules
constNEE "c:Const ==> c ~= 0"
@@ -16,8 +16,8 @@
consts
- Exp :: i (* Datatype of expressions *)
- ExVar :: i (* Abstract type of variables *)
+ Exp :: i (* Datatype of expressions *)
+ ExVar :: i (* Abstract type of variables *)
datatype <= "univ(Const Un ExVar)"
"Exp" = e_const("c:Const")
| e_var("x:ExVar")
--- a/src/ZF/Coind/Map.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Coind/Map.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Coind/Map.thy
+(* Title: ZF/Coind/Map.thy
ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
+ Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
*)
--- a/src/ZF/Coind/Static.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Coind/Static.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Coind/Static.thy
+(* Title: ZF/Coind/Static.thy
ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
+ Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
*)
--- a/src/ZF/Coind/Types.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Coind/Types.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,14 +1,14 @@
-(* Title: ZF/Coind/Types.thy
+(* Title: ZF/Coind/Types.thy
ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
+ Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
*)
Types = Language +
consts
- Ty :: i (* Datatype of types *)
- TyConst :: i (* Abstract type of type constants *)
+ Ty :: i (* Datatype of types *)
+ TyConst :: i (* Abstract type of type constants *)
datatype <= "univ(TyConst)"
"Ty" = t_const("tc:TyConst")
| t_fun("t1:Ty","t2:Ty")
--- a/src/ZF/Coind/Values.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Coind/Values.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Coind/Values.thy
+(* Title: ZF/Coind/Values.thy
ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
+ Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
*)
--- a/src/ZF/Epsilon.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Epsilon.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/epsilon.thy
+(* Title: ZF/epsilon.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Epsilon induction and recursion
@@ -12,7 +12,7 @@
transrec :: [i, [i,i]=>i] =>i
defs
- eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
- transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
- rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
+ eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
+ transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
+ rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
end
--- a/src/ZF/EquivClass.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/EquivClass.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/EquivClass.thy
+(* Title: ZF/EquivClass.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Equivalence relations in Zermelo-Fraenkel Set Theory
@@ -9,7 +9,7 @@
EquivClass = Rel + Perm +
consts
"'/" :: [i,i]=>i (infixl 90) (*set of equiv classes*)
- congruent :: [i,i=>i]=>o
+ congruent :: [i,i=>i]=>o
congruent2 :: [i,[i,i]=>i]=>o
defs
--- a/src/ZF/Finite.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Finite.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Finite.thy
+(* Title: ZF/Finite.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Finite powerset operator
@@ -8,8 +8,8 @@
Finite = Arith + Inductive +
consts
- Fin :: i=>i
- FiniteFun :: [i,i]=>i ("(_ -||>/ _)" [61, 60] 60)
+ Fin :: i=>i
+ FiniteFun :: [i,i]=>i ("(_ -||>/ _)" [61, 60] 60)
inductive
domains "Fin(A)" <= "Pow(A)"
@@ -24,6 +24,6 @@
intrs
emptyI "0 : A -||> B"
consI "[| a: A; b: B; h: A -||> B; a ~: domain(h)
- |] ==> cons(<a,b>,h) : A -||> B"
+ |] ==> cons(<a,b>,h) : A -||> B"
type_intrs "Fin.intrs"
end
--- a/src/ZF/Fixedpt.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Fixedpt.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/fixedpt.thy
+(* Title: ZF/fixedpt.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Least and greatest fixed points
--- a/src/ZF/IMP/Com.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/IMP/Com.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/IMP/Com.thy
+(* Title: ZF/IMP/Com.thy
ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
Arithmetic expressions, Boolean expressions, Commands
@@ -23,14 +23,14 @@
(** Evaluation of arithmetic expressions **)
consts evala :: i
- "@evala" :: [i,i,i] => o ("<_,_>/ -a-> _" [0,0,50] 50)
+ "@evala" :: [i,i,i] => o ("<_,_>/ -a-> _" [0,0,50] 50)
translations
"<ae,sig> -a-> n" == "<ae,sig,n> : evala"
inductive
domains "evala" <= "aexp * (loc -> nat) * nat"
intrs
N "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
- X "[| x:loc; sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
+ X "[| x:loc; sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
Op1 "[| <e,sigma> -a-> n; f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
Op2 "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f: (nat*nat) -> nat |]
==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
@@ -46,13 +46,13 @@
| false
| ROp ("f: (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
| noti ("b : bexp")
- | andi ("b0 : bexp", "b1 : bexp") (infixl 60)
- | ori ("b0 : bexp", "b1 : bexp") (infixl 60)
+ | andi ("b0 : bexp", "b1 : bexp") (infixl 60)
+ | ori ("b0 : bexp", "b1 : bexp") (infixl 60)
(** Evaluation of boolean expressions **)
-consts evalb :: i
- "@evalb" :: [i,i,i] => o ("<_,_>/ -b-> _" [0,0,50] 50)
+consts evalb :: i
+ "@evalb" :: [i,i,i] => o ("<_,_>/ -b-> _" [0,0,50] 50)
translations
"<be,sig> -b-> b" == "<be,sig,b> : evalb"
@@ -63,15 +63,15 @@
tru "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
fls "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
ROp "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |]
- ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
+ ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
noti "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
andi "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
==> <b0 andi b1,sigma> -b-> (w0 and w1)"
ori "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
- ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
+ ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
type_intrs "bexp.intrs @
- [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
+ [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
type_elims "[make_elim(evala.dom_subset RS subsetD)]"
@@ -80,24 +80,24 @@
datatype <= "univ(loc Un aexp Un bexp)"
"com" = skip
- | ":=" ("x:loc", "a:aexp") (infixl 60)
- | semic ("c0:com", "c1:com") ("_; _" [60, 60] 10)
- | while ("b:bexp", "c:com") ("while _ do _" 60)
- | ifc ("b:bexp", "c0:com", "c1:com") ("ifc _ then _ else _" 60)
+ | ":=" ("x:loc", "a:aexp") (infixl 60)
+ | semic ("c0:com", "c1:com") ("_; _" [60, 60] 10)
+ | while ("b:bexp", "c:com") ("while _ do _" 60)
+ | ifc ("b:bexp", "c0:com", "c1:com") ("ifc _ then _ else _" 60)
(*Constructor ";" has low precedence to avoid syntactic ambiguities
with [| m: nat; x: loc; ... |] ==> ... It usually will need parentheses.*)
(** Execution of commands **)
consts evalc :: i
- "@evalc" :: [i,i,i] => o ("<_,_>/ -c-> _" [0,0,50] 50)
- "assign" :: [i,i,i] => i ("_[_'/_]" [95,0,0] 95)
+ "@evalc" :: [i,i,i] => o ("<_,_>/ -c-> _" [0,0,50] 50)
+ "assign" :: [i,i,i] => i ("_[_'/_]" [95,0,0] 95)
translations
"<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
defs
- assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
+ assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
inductive
domains "evalc" <= "com * (loc -> nat) * (loc -> nat)"
@@ -111,11 +111,11 @@
<c0 ; c1, sigma> -c-> sigma1"
ifc1 "[| b:bexp; c1:com; sigma:loc->nat;
- <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==>
+ <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==>
<ifc b then c0 else c1, sigma> -c-> sigma1"
ifc0 "[| b:bexp; c0:com; sigma:loc->nat;
- <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==>
+ <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==>
<ifc b then c0 else c1, sigma> -c-> sigma1"
while0 "[| c: com; <b, sigma> -b-> 0 |] ==>
@@ -128,6 +128,6 @@
con_defs "[assign_def]"
type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
type_elims "[make_elim(evala.dom_subset RS subsetD),
- make_elim(evalb.dom_subset RS subsetD) ]"
+ make_elim(evalb.dom_subset RS subsetD) ]"
end
--- a/src/ZF/IMP/Denotation.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/IMP/Denotation.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/IMP/Denotation.thy
+(* Title: ZF/IMP/Denotation.thy
ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
Denotational semantics of expressions & commands
@@ -14,33 +14,33 @@
C :: i => i
Gamma :: [i,i,i] => i
-rules (*NOT definitional*)
- A_nat_def "A(N(n)) == (%sigma. n)"
- A_loc_def "A(X(x)) == (%sigma. sigma`x)"
- A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
- A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
+rules (*NOT definitional*)
+ A_nat_def "A(N(n)) == (%sigma. n)"
+ A_loc_def "A(X(x)) == (%sigma. sigma`x)"
+ A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
+ A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
- B_true_def "B(true) == (%sigma. 1)"
- B_false_def "B(false) == (%sigma. 0)"
- B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
+ B_true_def "B(true) == (%sigma. 1)"
+ B_false_def "B(false) == (%sigma. 0)"
+ B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
- B_not_def "B(noti(b)) == (%sigma. not(B(b,sigma)))"
- B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
- B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
+ B_not_def "B(noti(b)) == (%sigma. not(B(b,sigma)))"
+ B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
+ B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
- C_skip_def "C(skip) == id(loc->nat)"
- C_assign_def "C(x := a) == {io:(loc->nat)*(loc->nat).
- snd(io) = fst(io)[A(a,fst(io))/x]}"
+ C_skip_def "C(skip) == id(loc->nat)"
+ C_assign_def "C(x := a) == {io:(loc->nat)*(loc->nat).
+ snd(io) = fst(io)[A(a,fst(io))/x]}"
- C_comp_def "C(c0 ; c1) == C(c1) O C(c0)"
- C_if_def "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un
- {io:C(c1). B(b,fst(io))=0}"
+ C_comp_def "C(c0 ; c1) == C(c1) O C(c0)"
+ C_if_def "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un
+ {io:C(c1). B(b,fst(io))=0}"
- Gamma_def "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un
- {io : id(loc->nat). B(b,fst(io))=0})"
+ Gamma_def "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un
+ {io : id(loc->nat). B(b,fst(io))=0})"
- C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
+ C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
end
--- a/src/ZF/IMP/Equiv.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/IMP/Equiv.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/IMP/Equiv.thy
+(* Title: ZF/IMP/Equiv.thy
ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
*)
--- a/src/ZF/Let.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Let.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Let
+(* Title: ZF/Let
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Let expressions, and tuple pattern-matching (borrowed from HOL)
--- a/src/ZF/List.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/List.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/List
+(* Title: ZF/List
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Lists in Zermelo-Fraenkel Set Theory
@@ -13,20 +13,20 @@
List = Datatype +
consts
- "@" :: [i,i]=>i (infixr 60)
+ "@" :: [i,i]=>i (infixr 60)
list_rec :: [i, i, [i,i,i]=>i] => i
- map :: [i=>i, i] => i
+ map :: [i=>i, i] => i
length,rev :: i=>i
flat :: i=>i
list_add :: i=>i
hd,tl :: i=>i
- drop :: [i,i]=>i
+ drop :: [i,i]=>i
(* List Enumeration *)
- "[]" :: i ("[]")
- "@List" :: is => i ("[(_)]")
+ "[]" :: i ("[]")
+ "@List" :: is => i ("[(_)]")
- list :: i=>i
+ list :: i=>i
datatype
@@ -41,9 +41,9 @@
defs
- hd_def "hd(l) == list_case(0, %x xs.x, l)"
- tl_def "tl(l) == list_case(Nil, %x xs.xs, l)"
- drop_def "drop(i,l) == rec(i, l, %j r. tl(r))"
+ hd_def "hd(l) == list_case(0, %x xs.x, l)"
+ tl_def "tl(l) == list_case(Nil, %x xs.xs, l)"
+ drop_def "drop(i,l) == rec(i, l, %j r. tl(r))"
list_rec_def
"list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
--- a/src/ZF/Nat.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Nat.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Nat.thy
+(* Title: ZF/Nat.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Natural numbers in Zermelo-Fraenkel Set Theory
@@ -8,7 +8,7 @@
Nat = Ordinal + Bool + "mono" +
consts
- nat :: i
+ nat :: i
nat_case :: [i, i=>i, i]=>i
nat_rec :: [i, i, [i,i]=>i]=>i
@@ -17,10 +17,10 @@
nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
nat_case_def
- "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
+ "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
nat_rec_def
- "nat_rec(k,a,b) ==
- wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
+ "nat_rec(k,a,b) ==
+ wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
end
--- a/src/ZF/Order.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Order.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Order.thy
+(* Title: ZF/Order.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Orders in Zermelo-Fraenkel Set Theory
@@ -8,13 +8,13 @@
Order = WF + Perm +
consts
- part_ord :: [i,i]=>o (*Strict partial ordering*)
- linear, tot_ord :: [i,i]=>o (*Strict total ordering*)
- well_ord :: [i,i]=>o (*Well-ordering*)
- mono_map :: [i,i,i,i]=>i (*Order-preserving maps*)
- ord_iso :: [i,i,i,i]=>i (*Order isomorphisms*)
- pred :: [i,i,i]=>i (*Set of predecessors*)
- ord_iso_map :: [i,i,i,i]=>i (*Construction for linearity theorem*)
+ part_ord :: [i,i]=>o (*Strict partial ordering*)
+ linear, tot_ord :: [i,i]=>o (*Strict total ordering*)
+ well_ord :: [i,i]=>o (*Well-ordering*)
+ mono_map :: [i,i,i,i]=>i (*Order-preserving maps*)
+ ord_iso :: [i,i,i,i]=>i (*Order isomorphisms*)
+ pred :: [i,i,i]=>i (*Set of predecessors*)
+ ord_iso_map :: [i,i,i,i]=>i (*Construction for linearity theorem*)
defs
part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
--- a/src/ZF/OrderArith.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/OrderArith.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/OrderArith.thy
+(* Title: ZF/OrderArith.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Towards ordinal arithmetic
@@ -15,14 +15,14 @@
(*disjoint sum of two relations; underlies ordinal addition*)
radd_def "radd(A,r,B,s) ==
{z: (A+B) * (A+B).
- (EX x y. z = <Inl(x), Inr(y)>) |
- (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) |
+ (EX x y. z = <Inl(x), Inr(y)>) |
+ (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) |
(EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
(*lexicographic product of two relations; underlies ordinal multiplication*)
rmult_def "rmult(A,r,B,s) ==
{z: (A*B) * (A*B).
- EX x' y' x y. z = <<x',y'>, <x,y>> &
+ EX x' y' x y. z = <<x',y'>, <x,y>> &
(<x',x>: r | (x'=x & <y',y>: s))}"
(*inverse image of a relation*)
--- a/src/ZF/OrderType.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/OrderType.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/OrderType.thy
+(* Title: ZF/OrderType.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Order types and ordinal arithmetic.
--- a/src/ZF/Ordinal.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Ordinal.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Ordinal.thy
+(* Title: ZF/Ordinal.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Ordinals in Zermelo-Fraenkel Set Theory
@@ -8,7 +8,7 @@
Ordinal = WF + Bool + "simpdata" + "equalities" +
consts
- Memrel :: i=>i
+ Memrel :: i=>i
Transset,Ord :: i=>o
"<" :: [i,i] => o (infixl 50) (*less than on ordinals*)
"le" :: [i,i] => o (infixl 50) (*less than or equals*)
@@ -18,9 +18,9 @@
"x le y" == "x < succ(y)"
defs
- Memrel_def "Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }"
- Transset_def "Transset(i) == ALL x:i. x<=i"
- Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))"
+ Memrel_def "Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }"
+ Transset_def "Transset(i) == ALL x:i. x<=i"
+ Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))"
lt_def "i<j == i:j & Ord(j)"
Limit_def "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
--- a/src/ZF/Perm.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Perm.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/perm
+(* Title: ZF/perm
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
The theory underlying permutation groups
@@ -11,26 +11,26 @@
Perm = ZF + "mono" +
consts
- O :: [i,i]=>i (infixr 60)
- id :: i=>i
+ O :: [i,i]=>i (infixr 60)
+ id :: i=>i
inj,surj,bij:: [i,i]=>i
defs
(*composition of relations and functions; NOT Suppes's relative product*)
- comp_def "r O s == {xz : domain(s)*range(r) .
- EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
+ comp_def "r O s == {xz : domain(s)*range(r) .
+ EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
(*the identity function for A*)
- id_def "id(A) == (lam x:A. x)"
+ id_def "id(A) == (lam x:A. x)"
(*one-to-one functions from A to B*)
inj_def "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
(*onto functions from A to B*)
- surj_def "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
+ surj_def "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
(*one-to-one and onto functions*)
- bij_def "bij(A,B) == inj(A,B) Int surj(A,B)"
+ bij_def "bij(A,B) == inj(A,B) Int surj(A,B)"
end
--- a/src/ZF/QPair.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/QPair.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/qpair.thy
+(* Title: ZF/qpair.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
@@ -13,19 +13,19 @@
QPair = Sum + "simpdata" +
consts
- QPair :: [i, i] => i ("<(_;/ _)>")
+ QPair :: [i, i] => i ("<(_;/ _)>")
qfst,qsnd :: i => i
qsplit :: [[i, i] => 'a, i] => 'a::logic (*for pattern-matching*)
qconverse :: i => i
QSigma :: [i, i => i] => i
- "<+>" :: [i,i]=>i (infixr 65)
+ "<+>" :: [i,i]=>i (infixr 65)
QInl,QInr :: i=>i
qcase :: [i=>i, i=>i, i]=>i
syntax
"@QSUM" :: [idt, i, i] => i ("(3QSUM _:_./ _)" 10)
- "<*>" :: [i, i] => i (infixr 80)
+ "<*>" :: [i, i] => i (infixr 80)
translations
"QSUM x:A. B" => "QSigma(A, %x. B)"
--- a/src/ZF/QUniv.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/QUniv.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/univ.thy
+(* Title: ZF/univ.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
A small universe for lazy recursive types
--- a/src/ZF/Rel.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Rel.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Rel.thy
+(* Title: ZF/Rel.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Relations in Zermelo-Fraenkel Set Theory
@@ -10,7 +10,7 @@
consts
refl,irrefl,equiv :: [i,i]=>o
sym,asym,antisym,trans :: i=>o
- trans_on :: [i,i]=>o ("trans[_]'(_')")
+ trans_on :: [i,i]=>o ("trans[_]'(_')")
defs
refl_def "refl(A,r) == (ALL x: A. <x,x> : r)"
@@ -25,7 +25,7 @@
trans_def "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
- trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.
+ trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.
<x,y>: r --> <y,z>: r --> <x,z>: r"
equiv_def "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
--- a/src/ZF/Resid/Confluence.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/Confluence.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Confluence.thy
+(* Title: Confluence.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
*)
@@ -8,14 +8,14 @@
Confluence = Reduction+
consts
- confluence :: i=>o
- strip :: o
+ confluence :: i=>o
+ strip :: o
defs
confluence_def "confluence(R) ==
- ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->
- (EX u.<y,u>:R & <z,u>:R))"
+ ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->
+ (EX u.<y,u>:R & <z,u>:R))"
strip_def "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) -->
- (EX u.(y =1=> u) & (z===>u)))"
+ (EX u.(y =1=> u) & (z===>u)))"
end
--- a/src/ZF/Resid/Conversion.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/Conversion.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Conversion.thy
+(* Title: Conversion.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
@@ -9,10 +9,10 @@
Conversion = Confluence+
consts
- Sconv1 :: i
- "<-1->" :: [i,i]=>o (infixl 50)
- Sconv :: i
- "<--->" :: [i,i]=>o (infixl 50)
+ Sconv1 :: i
+ "<-1->" :: [i,i]=>o (infixl 50)
+ Sconv :: i
+ "<--->" :: [i,i]=>o (infixl 50)
translations
"a<-1->b" == "<a,b>:Sconv1"
@@ -21,16 +21,16 @@
inductive
domains "Sconv1" <= "lambda*lambda"
intrs
- red1 "m -1-> n ==> m<-1->n"
- expl "n -1-> m ==> m<-1->n"
- type_intrs "[red1D1,red1D2]@lambda.intrs@bool_typechecks"
+ red1 "m -1-> n ==> m<-1->n"
+ expl "n -1-> m ==> m<-1->n"
+ type_intrs "[red1D1,red1D2]@lambda.intrs@bool_typechecks"
inductive
domains "Sconv" <= "lambda*lambda"
intrs
- one_step "m<-1->n ==> m<--->n"
- refl "m:lambda ==> m<--->m"
- trans "[|m<--->n; n<--->p|] ==> m<--->p"
- type_intrs "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
+ one_step "m<-1->n ==> m<--->n"
+ refl "m:lambda ==> m<--->m"
+ trans "[|m<--->n; n<--->p|] ==> m<--->p"
+ type_intrs "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
end
--- a/src/ZF/Resid/Cube.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/Cube.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Cube.thy
+(* Title: Cube.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
*)
--- a/src/ZF/Resid/Redex.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/Redex.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Redex.thy
+(* Title: Redex.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
*)
@@ -10,14 +10,14 @@
redexes :: i
datatype
- "redexes" = Var ("n: nat")
+ "redexes" = Var ("n: nat")
| Fun ("t: redexes")
| App ("b:bool" ,"f:redexes" , "a:redexes")
type_intrs "[bool_into_univ]"
consts
- redex_rec :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
+ redex_rec :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
defs
redex_rec_def
--- a/src/ZF/Resid/Reduction.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/Reduction.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Reduction.thy
+(* Title: Reduction.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
*)
@@ -21,39 +21,39 @@
inductive
domains "Sred1" <= "lambda*lambda"
intrs
- beta "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
- rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
- apl_l "[|m2:lambda; m1 -1-> n1|] ==>
- Apl(m1,m2) -1-> Apl(n1,m2)"
- apl_r "[|m1:lambda; m2 -1-> n2|] ==>
- Apl(m1,m2) -1-> Apl(m1,n2)"
- type_intrs "red_typechecks"
+ beta "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
+ rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
+ apl_l "[|m2:lambda; m1 -1-> n1|] ==>
+ Apl(m1,m2) -1-> Apl(n1,m2)"
+ apl_r "[|m1:lambda; m2 -1-> n2|] ==>
+ Apl(m1,m2) -1-> Apl(m1,n2)"
+ type_intrs "red_typechecks"
inductive
domains "Sred" <= "lambda*lambda"
intrs
- one_step "[|m-1->n|] ==> m--->n"
- refl "m:lambda==>m --->m"
- trans "[|m--->n; n--->p|]==>m--->p"
- type_intrs "[Sred1.dom_subset RS subsetD]@red_typechecks"
+ one_step "[|m-1->n|] ==> m--->n"
+ refl "m:lambda==>m --->m"
+ trans "[|m--->n; n--->p|]==>m--->p"
+ type_intrs "[Sred1.dom_subset RS subsetD]@red_typechecks"
inductive
domains "Spar_red1" <= "lambda*lambda"
intrs
- beta "[|m =1=> m';
- n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
- rvar "n:nat==> Var(n) =1=> Var(n)"
- rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
- rapl "[|m =1=> m';
- n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
- type_intrs "red_typechecks"
+ beta "[|m =1=> m';
+ n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
+ rvar "n:nat==> Var(n) =1=> Var(n)"
+ rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
+ rapl "[|m =1=> m';
+ n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
+ type_intrs "red_typechecks"
inductive
domains "Spar_red" <= "lambda*lambda"
intrs
- one_step "[|m =1=> n|] ==> m ===> n"
- trans "[|m===>n; n===>p|]==>m===>p"
- type_intrs "[Spar_red1.dom_subset RS subsetD]@red_typechecks"
+ one_step "[|m =1=> n|] ==> m ===> n"
+ trans "[|m===>n; n===>p|]==>m===>p"
+ type_intrs "[Spar_red1.dom_subset RS subsetD]@red_typechecks"
end
--- a/src/ZF/Resid/Residuals.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/Residuals.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Residuals.thy
+(* Title: Residuals.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
@@ -9,9 +9,9 @@
Residuals = Substitution+
consts
- Sres :: i
- residuals :: [i,i,i]=>i
- "|>" :: [i,i]=>i (infixl 70)
+ Sres :: i
+ residuals :: [i,i,i]=>i
+ "|>" :: [i,i]=>i (infixl 70)
translations
"residuals(u,v,w)" == "<u,v,w>:Sres"
@@ -19,16 +19,16 @@
inductive
domains "Sres" <= "redexes*redexes*redexes"
intrs
- Res_Var "n:nat ==> residuals(Var(n),Var(n),Var(n))"
- Res_Fun "[|residuals(u,v,w)|]==>
- residuals(Fun(u),Fun(v),Fun(w))"
- Res_App "[|residuals(u1,v1,w1);
- residuals(u2,v2,w2); b:bool|]==>
- residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
- Res_redex "[|residuals(u1,v1,w1);
- residuals(u2,v2,w2); b:bool|]==>
- residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
- type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
+ Res_Var "n:nat ==> residuals(Var(n),Var(n),Var(n))"
+ Res_Fun "[|residuals(u,v,w)|]==>
+ residuals(Fun(u),Fun(v),Fun(w))"
+ Res_App "[|residuals(u1,v1,w1);
+ residuals(u2,v2,w2); b:bool|]==>
+ residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
+ Res_redex "[|residuals(u1,v1,w1);
+ residuals(u2,v2,w2); b:bool|]==>
+ residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
+ type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
rules
res_func_def "u |> v == THE w.residuals(u,v,w)"
--- a/src/ZF/Resid/SubUnion.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/SubUnion.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: SubUnion.thy
+(* Title: SubUnion.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
*)
@@ -11,7 +11,7 @@
Ssub,Scomp,Sreg :: i
"<==","~" :: [i,i]=>o (infixl 70)
un :: [i,i]=>i (infixl 70)
- regular :: i=>o
+ regular :: i=>o
translations
"a<==b" == "<a,b>:Ssub"
@@ -21,39 +21,39 @@
inductive
domains "Ssub" <= "redexes*redexes"
intrs
- Sub_Var "n:nat ==> Var(n)<== Var(n)"
- Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
- Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==>
- App(0,u1,u2)<== App(b,v1,v2)"
- Sub_App2 "[|u1<== v1; u2<== v2|]==>
- App(1,u1,u2)<== App(1,v1,v2)"
- type_intrs "redexes.intrs@bool_typechecks"
+ Sub_Var "n:nat ==> Var(n)<== Var(n)"
+ Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
+ Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==>
+ App(0,u1,u2)<== App(b,v1,v2)"
+ Sub_App2 "[|u1<== v1; u2<== v2|]==>
+ App(1,u1,u2)<== App(1,v1,v2)"
+ type_intrs "redexes.intrs@bool_typechecks"
inductive
domains "Scomp" <= "redexes*redexes"
intrs
- Comp_Var "n:nat ==> Var(n) ~ Var(n)"
- Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
- Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>
- App(b1,u1,u2) ~ App(b2,v1,v2)"
- type_intrs "redexes.intrs@bool_typechecks"
+ Comp_Var "n:nat ==> Var(n) ~ Var(n)"
+ Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
+ Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>
+ App(b1,u1,u2) ~ App(b2,v1,v2)"
+ type_intrs "redexes.intrs@bool_typechecks"
inductive
domains "Sreg" <= "redexes"
intrs
- Reg_Var "n:nat ==> regular(Var(n))"
- Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
- Reg_App1 "[|regular(Fun(u)); regular(v)
- |]==>regular(App(1,Fun(u),v))"
- Reg_App2 "[|regular(u); regular(v)
- |]==>regular(App(0,u,v))"
- type_intrs "redexes.intrs@bool_typechecks"
+ Reg_Var "n:nat ==> regular(Var(n))"
+ Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
+ Reg_App1 "[|regular(Fun(u)); regular(v)
+ |]==>regular(App(1,Fun(u),v))"
+ Reg_App2 "[|regular(u); regular(v)
+ |]==>regular(App(0,u,v))"
+ type_intrs "redexes.intrs@bool_typechecks"
defs
union_def "u un v == redex_rec(u,
- %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),
+ %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),
%x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),
%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,
- %c z u. App(b or c, m`z, p`u), t))`v"
+ %c z u. App(b or c, m`z, p`u), t))`v"
end
--- a/src/ZF/Resid/Substitution.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/Substitution.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Substitution.thy
+(* Title: Substitution.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
*)
@@ -8,19 +8,19 @@
Substitution = SubUnion +
consts
- lift_rec :: [i,i]=> i
- lift :: i=>i
- subst_rec :: [i,i,i]=> i
+ lift_rec :: [i,i]=> i
+ lift :: i=>i
+ subst_rec :: [i,i,i]=> i
"'/" :: [i,i]=>i (infixl 70) (*subst*)
translations
"lift(r)" == "lift_rec(r,0)"
"u/v" == "subst_rec(u,v,0)"
defs
- lift_rec_def "lift_rec(r,kg) ==
- redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))),
- %x m.(lam k:nat.Fun(m`(succ(k)))),
- %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
+ lift_rec_def "lift_rec(r,kg) ==
+ redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))),
+ %x m.(lam k:nat.Fun(m`(succ(k)))),
+ %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
(* subst_rec(u,Var(i),k) = if k<i then Var(i-1)
@@ -30,15 +30,15 @@
subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))
*)
- subst_rec_def "subst_rec(u,t,kg) ==
- redex_rec(t,
- %i.(lam r:redexes.lam k:nat.
- if(k<i,Var(i#-1),
- if(k=i,r,Var(i)))),
- %x m.(lam r:redexes.lam k:nat.
+ subst_rec_def "subst_rec(u,t,kg) ==
+ redex_rec(t,
+ %i.(lam r:redexes.lam k:nat.
+ if(k<i,Var(i#-1),
+ if(k=i,r,Var(i)))),
+ %x m.(lam r:redexes.lam k:nat.
Fun(m`(lift(r))`(succ(k)))),
- %b x y m p.lam r:redexes.lam k:nat.
- App(b,m`r`k,p`r`k))`u`kg"
+ %b x y m p.lam r:redexes.lam k:nat.
+ App(b,m`r`k,p`r`k))`u`kg"
end
--- a/src/ZF/Resid/Terms.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/Terms.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Terms.thy
+(* Title: Terms.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
*)
@@ -8,9 +8,9 @@
Terms = Cube+
consts
- lambda :: i
- unmark :: i=>i
- Apl :: [i,i]=>i
+ lambda :: i
+ unmark :: i=>i
+ Apl :: [i,i]=>i
translations
"Apl(n,m)" == "App(0,n,m)"
@@ -18,15 +18,15 @@
inductive
domains "lambda" <= "redexes"
intrs
- Lambda_Var " n:nat ==> Var(n):lambda"
- Lambda_Fun " u:lambda ==> Fun(u):lambda"
- Lambda_App "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
- type_intrs "redexes.intrs@bool_typechecks"
+ Lambda_Var " n:nat ==> Var(n):lambda"
+ Lambda_Fun " u:lambda ==> Fun(u):lambda"
+ Lambda_App "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
+ type_intrs "redexes.intrs@bool_typechecks"
defs
- unmark_def "unmark(u) == redex_rec(u,%i.Var(i),
- %x m.Fun(m),
- %b x y m p.Apl(m,p))"
+ unmark_def "unmark(u) == redex_rec(u,%i.Var(i),
+ %x m.Fun(m),
+ %b x y m p.Apl(m,p))"
end
--- a/src/ZF/Sum.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Sum.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/sum.thy
+(* Title: ZF/sum.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Disjoint sums in Zermelo-Fraenkel Set Theory
@@ -9,7 +9,7 @@
Sum = Bool + "simpdata" +
consts
- "+" :: [i,i]=>i (infixr 65)
+ "+" :: [i,i]=>i (infixr 65)
Inl,Inr :: i=>i
case :: [i=>i, i=>i, i]=>i
Part :: [i,i=>i] => i
@@ -21,5 +21,5 @@
case_def "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))"
(*operator for selecting out the various summands*)
- Part_def "Part(A,h) == {x: A. EX z. x = h(z)}"
+ Part_def "Part(A,h) == {x: A. EX z. x = h(z)}"
end
--- a/src/ZF/Trancl.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Trancl.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/trancl.thy
+(* Title: ZF/trancl.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Transitive closure of a relation
@@ -12,6 +12,6 @@
trancl :: i=>i ("(_^+)" [100] 100) (*transitive closure*)
defs
- rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
+ rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
trancl_def "r^+ == r O r^*"
end
--- a/src/ZF/Univ.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Univ.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/univ.thy
+(* Title: ZF/univ.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
The cumulative hierarchy and a small universe for recursive types
@@ -19,13 +19,13 @@
univ :: i=>i
translations
- "Vset(x)" == "Vfrom(0,x)"
+ "Vset(x)" == "Vfrom(0,x)"
defs
Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
Vrec_def
- "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
+ "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
univ_def "univ(A) == Vfrom(A,nat)"
--- a/src/ZF/WF.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/WF.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/wf.thy
+(* Title: ZF/wf.thy
ID: $Id$
- Author: Tobias Nipkow and Lawrence C Paulson
+ Author: Tobias Nipkow and Lawrence C Paulson
Copyright 1994 University of Cambridge
Well-founded Recursion
@@ -9,26 +9,26 @@
WF = Trancl + "mono" + "equalities" +
consts
wf :: i=>o
- wf_on :: [i,i]=>o ("wf[_]'(_')")
+ wf_on :: [i,i]=>o ("wf[_]'(_')")
wftrec,wfrec :: [i, i, [i,i]=>i] =>i
- wfrec_on :: [i, i, i, [i,i]=>i] =>i ("wfrec[_]'(_,_,_')")
+ wfrec_on :: [i, i, i, [i,i]=>i] =>i ("wfrec[_]'(_,_,_')")
is_recfun :: [i, i, [i,i]=>i, i] =>o
the_recfun :: [i, i, [i,i]=>i] =>i
defs
(*r is a well-founded relation*)
- wf_def "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
+ wf_def "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
(*r is well-founded relation over A*)
wf_on_def "wf_on(A,r) == wf(r Int A*A)"
is_recfun_def "is_recfun(r,a,H,f) ==
- (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
+ (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
the_recfun_def "the_recfun(r,a,H) == (THE f.is_recfun(r,a,H,f))"
- wftrec_def "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
+ wftrec_def "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
(*public version. Does not require r to be transitive*)
wfrec_def "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
--- a/src/ZF/ZF.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ZF.thy Tue Feb 06 12:27:17 1996 +0100
@@ -61,7 +61,7 @@
range :: i => i
field :: i => i
converse :: i => i
- function :: i => o (*is a relation a function?*)
+ function :: i => o (*is a relation a function?*)
Lambda :: [i, i => i] => i
restrict :: [i, i] => i
@@ -214,8 +214,8 @@
domain_def "domain(r) == {x. w:r, EX y. w=<x,y>}"
range_def "range(r) == domain(converse(r))"
field_def "field(r) == domain(r) Un range(r)"
- function_def "function(r) == ALL x y. <x,y>:r -->
- (ALL y'. <x,y'>:r --> y=y')"
+ function_def "function(r) == ALL x y. <x,y>:r -->
+ (ALL y'. <x,y'>:r --> y=y')"
image_def "r `` A == {y : range(r) . EX x:A. <x,y> : r}"
vimage_def "r -`` A == converse(r)``A"
--- a/src/ZF/Zorn.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Zorn.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Zorn.thy
+(* Title: ZF/Zorn.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Based upon the article
@@ -39,10 +39,10 @@
inductive
domains "TFin(S,next)" <= "Pow(S)"
intrs
- nextI "[| x : TFin(S,next); next: increasing(S)
+ nextI "[| x : TFin(S,next); next: increasing(S)
|] ==> next`x : TFin(S,next)"
- Pow_UnionI "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
+ Pow_UnionI "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
monos "[Pow_mono]"
con_defs "[increasing_def]"
--- a/src/ZF/ex/Acc.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Acc.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/Acc.thy
+(* Title: ZF/ex/Acc.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Inductive definition of acc(r)
--- a/src/ZF/ex/BT.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/BT.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/BT.thy
+(* Title: ZF/ex/BT.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Binary trees
@@ -8,12 +8,12 @@
BT = Datatype +
consts
- bt_rec :: [i, i, [i,i,i,i,i]=>i] => i
- n_nodes :: i=>i
- n_leaves :: i=>i
- bt_reflect :: i=>i
+ bt_rec :: [i, i, [i,i,i,i,i]=>i] => i
+ n_nodes :: i=>i
+ n_leaves :: i=>i
+ bt_reflect :: i=>i
- bt :: i=>i
+ bt :: i=>i
datatype
"bt(A)" = Lf | Br ("a: A", "t1: bt(A)", "t2: bt(A)")
@@ -22,8 +22,8 @@
bt_rec_def
"bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
- n_nodes_def "n_nodes(t) == bt_rec(t, 0, %x y z r s. succ(r#+s))"
- n_leaves_def "n_leaves(t) == bt_rec(t, succ(0), %x y z r s. r#+s)"
+ n_nodes_def "n_nodes(t) == bt_rec(t, 0, %x y z r s. succ(r#+s))"
+ n_leaves_def "n_leaves(t) == bt_rec(t, succ(0), %x y z r s. r#+s)"
bt_reflect_def "bt_reflect(t) == bt_rec(t, Lf, %x y z r s. Br(x,s,r))"
end
--- a/src/ZF/ex/Brouwer.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Brouwer.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/Brouwer.thy
+(* Title: ZF/ex/Brouwer.thy
ID: $ $
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Infinite branching datatype definitions
@@ -15,15 +15,15 @@
datatype <= "Vfrom(0, csucc(nat))"
"brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
- monos "[Pi_mono]"
+ monos "[Pi_mono]"
type_intrs "inf_datatype_intrs"
(*The union with nat ensures that the cardinal is infinite*)
datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
"Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
- monos "[Pi_mono]"
+ monos "[Pi_mono]"
type_intrs "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]
- @ inf_datatype_intrs"
+ @ inf_datatype_intrs"
end
--- a/src/ZF/ex/CoUnit.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/CoUnit.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/CoUnit.ML
+(* Title: ZF/ex/CoUnit.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Trivial codatatype definitions, one of which goes wrong!
--- a/src/ZF/ex/Comb.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Comb.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/Comb.thy
+(* Title: ZF/ex/Comb.thy
ID: $Id$
- Author: Lawrence C Paulson
+ Author: Lawrence C Paulson
Copyright 1994 University of Cambridge
Combinatory Logic example: the Church-Rosser Theorem
@@ -27,8 +27,8 @@
**)
consts
contract :: i
- "-1->" :: [i,i] => o (infixl 50)
- "--->" :: [i,i] => o (infixl 50)
+ "-1->" :: [i,i] => o (infixl 50)
+ "--->" :: [i,i] => o (infixl 50)
translations
"p -1-> q" == "<p,q> : contract"
@@ -49,8 +49,8 @@
**)
consts
parcontract :: i
- "=1=>" :: [i,i] => o (infixl 50)
- "===>" :: [i,i] => o (infixl 50)
+ "=1=>" :: [i,i] => o (infixl 50)
+ "===>" :: [i,i] => o (infixl 50)
translations
"p =1=> q" == "<p,q> : parcontract"
--- a/src/ZF/ex/Data.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Data.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/Data.thy
+(* Title: ZF/ex/Data.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Sample datatype definition.
--- a/src/ZF/ex/Enum.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Enum.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/Enum
+(* Title: ZF/ex/Enum
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Example of a BIG enumeration type
--- a/src/ZF/ex/Integ.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Integ.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/integ.thy
+(* Title: ZF/ex/integ.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
The integers as equivalence classes over nat*nat.
@@ -9,34 +9,34 @@
Integ = EquivClass + Arith +
consts
intrel,integ:: i
- znat :: i=>i ("$# _" [80] 80)
- zminus :: i=>i ("$~ _" [80] 80)
- znegative :: i=>o
- zmagnitude :: i=>i
+ znat :: i=>i ("$# _" [80] 80)
+ zminus :: i=>i ("$~ _" [80] 80)
+ znegative :: i=>o
+ zmagnitude :: i=>i
"$*" :: [i,i]=>i (infixl 70)
"$'/" :: [i,i]=>i (infixl 70)
"$'/'/" :: [i,i]=>i (infixl 70)
- "$+" :: [i,i]=>i (infixl 65)
+ "$+" :: [i,i]=>i (infixl 65)
"$-" :: [i,i]=>i (infixl 65)
- "$<" :: [i,i]=>o (infixl 50)
+ "$<" :: [i,i]=>o (infixl 50)
defs
intrel_def
- "intrel == {p:(nat*nat)*(nat*nat).
+ "intrel == {p:(nat*nat)*(nat*nat).
EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
integ_def "integ == (nat*nat)/intrel"
- znat_def "$# m == intrel `` {<m,0>}"
+ znat_def "$# m == intrel `` {<m,0>}"
- zminus_def "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
+ zminus_def "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
znegative_def
- "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
+ "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
zmagnitude_def
- "zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
+ "zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
(*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
Perhaps a "curried" or even polymorphic congruent predicate would be
@@ -47,7 +47,7 @@
in intrel``{<x1#+x2, y1#+y2>}"
zdiff_def "Z1 $- Z2 == Z1 $+ zminus(Z2)"
- zless_def "Z1 $< Z2 == znegative(Z1 $- Z2)"
+ zless_def "Z1 $< Z2 == znegative(Z1 $- Z2)"
(*This illustrates the primitive form of definitions (no patterns)*)
zmult_def
--- a/src/ZF/ex/LList.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/LList.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/LList.thy
+(* Title: ZF/ex/LList.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Codatatype definition of Lazy Lists
--- a/src/ZF/ex/Limit.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Limit.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/Limit
+(* Title: ZF/ex/Limit
ID: $Id$
- Author: Sten Agerholm
+ Author: Sten Agerholm
A formalization of the inverse limit construction of domain theory.
--- a/src/ZF/ex/ListN.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/ListN.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/ListN
+(* Title: ZF/ex/ListN
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Inductive definition of lists of n elements
@@ -10,7 +10,7 @@
*)
ListN = List +
-consts listn ::i=>i
+consts listn ::i=>i
inductive
domains "listn(A)" <= "nat*list(A)"
intrs
--- a/src/ZF/ex/Ntree.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Ntree.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/Ntree.ML
+(* Title: ZF/ex/Ntree.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Datatype definition n-ary branching trees
@@ -17,18 +17,18 @@
datatype
"ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
- monos "[[subset_refl, Pi_mono] MRS UN_mono]" (*MUST have this form*)
+ monos "[[subset_refl, Pi_mono] MRS UN_mono]" (*MUST have this form*)
type_intrs "[nat_fun_univ RS subsetD]"
type_elims "[UN_E]"
datatype
"maptree(A)" = Sons ("a: A", "h: maptree(A) -||> maptree(A)")
- monos "[FiniteFun_mono1]" (*Use monotonicity in BOTH args*)
+ monos "[FiniteFun_mono1]" (*Use monotonicity in BOTH args*)
type_intrs "[FiniteFun_univ1 RS subsetD]"
datatype
"maptree2(A,B)" = Sons2 ("a: A", "h: B -||> maptree2(A,B)")
- monos "[subset_refl RS FiniteFun_mono]"
+ monos "[subset_refl RS FiniteFun_mono]"
type_intrs "[FiniteFun_in_univ']"
end
--- a/src/ZF/ex/Primrec.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Primrec.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/Primrec.thy
+(* Title: ZF/ex/Primrec.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Primitive Recursive Functions
@@ -22,8 +22,8 @@
PROJ :: i=>i
COMP :: [i,i]=>i
PREC :: [i,i]=>i
- ACK :: i=>i
- ack :: [i,i]=>i
+ ACK :: i=>i
+ ack :: [i,i]=>i
translations
"ack(x,y)" == "ACK(x) ` [y]"
@@ -57,8 +57,8 @@
PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
monos "[list_mono]"
con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
- type_intrs "nat_typechecks @ list.intrs @
- [lam_type, list_case_type, drop_type, map_type,
- apply_type, rec_type]"
+ type_intrs "nat_typechecks @ list.intrs @
+ [lam_type, list_case_type, drop_type, map_type,
+ apply_type, rec_type]"
end
--- a/src/ZF/ex/PropLog.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/PropLog.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/PropLog.thy
+(* Title: ZF/ex/PropLog.thy
ID: $Id$
- Author: Tobias Nipkow & Lawrence C Paulson
+ Author: Tobias Nipkow & Lawrence C Paulson
Copyright 1993 University of Cambridge
Datatype definition of propositional logic formulae and inductive definition
@@ -15,13 +15,13 @@
datatype
"prop" = Fls
- | Var ("n: nat") ("#_" [100] 100)
- | "=>" ("p: prop", "q: prop") (infixr 90)
+ | Var ("n: nat") ("#_" [100] 100)
+ | "=>" ("p: prop", "q: prop") (infixr 90)
(** The proof system **)
consts
thms :: i => i
- "|-" :: [i,i] => o (infixl 50)
+ "|-" :: [i,i] => o (infixl 50)
translations
"H |- p" == "p : thms(H)"
@@ -41,7 +41,7 @@
consts
prop_rec :: [i, i, i=>i, [i,i,i,i]=>i] => i
is_true :: [i,i] => o
- "|=" :: [i,i] => o (infixl 50)
+ "|=" :: [i,i] => o (infixl 50)
hyps :: [i,i] => i
defs
--- a/src/ZF/ex/Ramsey.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Ramsey.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/ramsey.thy
+(* Title: ZF/ex/ramsey.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Ramsey's Theorem (finite exponent 2 version)
@@ -20,9 +20,9 @@
Ramsey = Arith +
consts
- Symmetric :: i=>o
- Atleast :: [i,i]=>o
- Clique,Indept,Ramsey :: [i,i,i]=>o
+ Symmetric :: i=>o
+ Atleast :: [i,i]=>o
+ Clique,Indept,Ramsey :: [i,i,i]=>o
defs
--- a/src/ZF/ex/Rmap.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Rmap.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/Rmap
+(* Title: ZF/ex/Rmap
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Inductive definition of an operator to "map" a relation over a list
--- a/src/ZF/ex/TF.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/TF.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/TF.thy
+(* Title: ZF/ex/TF.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Trees & forests, a mutually recursive type definition.
@@ -24,14 +24,14 @@
defs
TF_rec_def
- "TF_rec(z,b,c,d) == Vrec(z,
- %z r. tree_forest_case(%x f. b(x, f, r`f),
- c,
- %t f. d(t, f, r`t, r`f), z))"
+ "TF_rec(z,b,c,d) == Vrec(z,
+ %z r. tree_forest_case(%x f. b(x, f, r`f),
+ c,
+ %t f. d(t, f, r`t, r`f), z))"
list_of_TF_def
"list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [],
- %t f r1 r2. Cons(t, r2))"
+ %t f r1 r2. Cons(t, r2))"
TF_of_list_def
"TF_of_list(f) == list_rec(f, Fnil, %t f r. Fcons(t,r))"
--- a/src/ZF/ex/Term.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/Term.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/Term.thy
+(* Title: ZF/ex/Term.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Terms over an alphabet.
@@ -19,7 +19,7 @@
datatype
"term(A)" = Apply ("a: A", "l: list(term(A))")
- monos "[list_mono]"
+ monos "[list_mono]"
type_elims "[make_elim (list_univ RS subsetD)]"
(*Or could have
@@ -31,12 +31,12 @@
"term_rec(t,d) ==
Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
- term_map_def "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
+ term_map_def "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
- term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
+ term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
- reflect_def "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
+ reflect_def "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
- preorder_def "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
+ preorder_def "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
end
--- a/src/ZF/ex/twos_compl.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ex/twos_compl.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,5 +1,5 @@
(* ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)