1.1 --- a/src/ZF/AC.thy Mon Feb 05 21:33:14 1996 +0100
1.2 +++ b/src/ZF/AC.thy Tue Feb 06 12:27:17 1996 +0100
1.3 @@ -1,6 +1,6 @@
1.4 -(* Title: ZF/AC.thy
1.5 +(* Title: ZF/AC.thy
1.6 ID: $Id$
1.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.9 Copyright 1994 University of Cambridge
1.10
1.11 The Axiom of Choice
1.12 @@ -10,5 +10,5 @@
1.13
1.14 AC = ZF + "func" +
1.15 rules
1.16 - AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
1.17 + AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
1.18 end
2.1 --- a/src/ZF/AC/AC16_WO4.thy Mon Feb 05 21:33:14 1996 +0100
2.2 +++ b/src/ZF/AC/AC16_WO4.thy Tue Feb 06 12:27:17 1996 +0100
2.3 @@ -1,6 +1,6 @@
2.4 -(* Title: ZF/AC/AC16_WO4.thy
2.5 +(* Title: ZF/AC/AC16_WO4.thy
2.6 ID: $Id$
2.7 - Author: Krzysztof Grabczewski
2.8 + Author: Krzysztof Grabczewski
2.9 *)
2.10
2.11 AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux +
2.12 @@ -24,6 +24,6 @@
2.13 LL_def "LL(t_n, k, y) == {v Int y. v:MM(t_n, k, y)}"
2.14
2.15 GG_def "GG(t_n, k, y) == lam v:LL(t_n, k, y).
2.16 - (THE w. w:MM(t_n, k, y) & v <= w) - v"
2.17 + (THE w. w:MM(t_n, k, y) & v <= w) - v"
2.18
2.19 end
3.1 --- a/src/ZF/AC/AC18_AC19.thy Mon Feb 05 21:33:14 1996 +0100
3.2 +++ b/src/ZF/AC/AC18_AC19.thy Tue Feb 06 12:27:17 1996 +0100
3.3 @@ -1,6 +1,6 @@
3.4 -(* Title: ZF/AC/AC18_AC19.thy
3.5 +(* Title: ZF/AC/AC18_AC19.thy
3.6 ID: $Id$
3.7 - Author: Krzysztof Grabczewski
3.8 + Author: Krzysztof Grabczewski
3.9
3.10 Additional definition used in the proof AC19 ==> AC1 which is a part
3.11 of the chain AC1 ==> AC18 ==> AC19 ==> AC1
4.1 --- a/src/ZF/AC/AC_Equiv.thy Mon Feb 05 21:33:14 1996 +0100
4.2 +++ b/src/ZF/AC/AC_Equiv.thy Tue Feb 06 12:27:17 1996 +0100
4.3 @@ -1,6 +1,6 @@
4.4 -(* Title: ZF/AC/AC_Equiv.thy
4.5 +(* Title: ZF/AC/AC_Equiv.thy
4.6 ID: $Id$
4.7 - Author: Krzysztof Grabczewski
4.8 + Author: Krzysztof Grabczewski
4.9
4.10 Axioms AC1 -- AC19 come from "Equivalents of the Axiom of Choice, II"
4.11 by H. Rubin and J.E. Rubin, 1985.
4.12 @@ -42,18 +42,18 @@
4.13 WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
4.14
4.15 WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &
4.16 - (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
4.17 + (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
4.18
4.19 WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
4.20
4.21 WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a
4.22 - & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
4.23 + & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
4.24
4.25 WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->
4.26 - well_ord(A,converse(R)))"
4.27 + well_ord(A,converse(R)))"
4.28
4.29 WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->
4.30 - (EX R. well_ord(A,R))"
4.31 + (EX R. well_ord(A,R))"
4.32
4.33 (* Axioms of Choice *)
4.34
4.35 @@ -62,64 +62,64 @@
4.36 AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
4.37
4.38 AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)
4.39 - --> (EX C. ALL B:A. EX y. B Int C = {y})"
4.40 + --> (EX C. ALL B:A. EX y. B Int C = {y})"
4.41
4.42 AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
4.43
4.44 AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
4.45
4.46 AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.
4.47 - ALL x:domain(g). f`(g`x) = x"
4.48 + ALL x:domain(g). f`(g`x) = x"
4.49
4.50 AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
4.51
4.52 AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)
4.53 - --> (PROD B:A. B)~=0"
4.54 + --> (PROD B:A. B)~=0"
4.55
4.56 AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)
4.57 - --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
4.58 + --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
4.59
4.60 AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->
4.61 - (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
4.62 + (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
4.63
4.64 AC10_def "AC10(n) == ALL A. (ALL B:A. ~Finite(B)) -->
4.65 - (EX f. ALL B:A. (pairwise_disjoint(f`B) &
4.66 - sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
4.67 + (EX f. ALL B:A. (pairwise_disjoint(f`B) &
4.68 + sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
4.69
4.70 AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
4.71
4.72 AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->
4.73 - (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &
4.74 - sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
4.75 + (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &
4.76 + sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
4.77
4.78 AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &
4.79 - f`B <= B & f`B lepoll m)"
4.80 + f`B <= B & f`B lepoll m)"
4.81
4.82 AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
4.83
4.84 AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.
4.85 - f`B~=0 & f`B <= B & f`B lepoll m))"
4.86 + f`B~=0 & f`B <= B & f`B lepoll m))"
4.87
4.88 AC16_def "AC16(n, k) == ALL A. ~Finite(A) -->
4.89 - (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &
4.90 - (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
4.91 + (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &
4.92 + (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
4.93
4.94 AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.
4.95 - EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
4.96 + EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
4.97
4.98 AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->
4.99 ((INT a:A. UN b:B(a). X(a,b)) =
4.100 (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
4.101
4.102 AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =
4.103 - (UN f:(PROD B:A. B). INT a:A. f`a))"
4.104 + (UN f:(PROD B:A. B). INT a:A. f`a))"
4.105
4.106 (* Auxiliary definitions used in the above definitions *)
4.107
4.108 pairwise_disjoint_def "pairwise_disjoint(A)
4.109 - == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
4.110 + == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
4.111
4.112 sets_of_size_between_def "sets_of_size_between(A,m,n)
4.113 - == ALL B:A. m lepoll B & B lepoll n"
4.114 + == ALL B:A. m lepoll B & B lepoll n"
4.115
4.116 end
5.1 --- a/src/ZF/AC/DC.thy Mon Feb 05 21:33:14 1996 +0100
5.2 +++ b/src/ZF/AC/DC.thy Tue Feb 06 12:27:17 1996 +0100
5.3 @@ -1,6 +1,6 @@
5.4 -(* Title: ZF/AC/DC.thy
5.5 +(* Title: ZF/AC/DC.thy
5.6 ID: $Id$
5.7 - Author: Krzysztof Grabczewski
5.8 + Author: Krzysztof Grabczewski
5.9
5.10 Theory file for the proofs concernind the Axiom of Dependent Choice
5.11 *)
5.12 @@ -16,13 +16,13 @@
5.13 rules
5.14
5.15 DC_def "DC(a) == ALL X R. R<=Pow(X)*X &
5.16 - (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R))
5.17 - --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
5.18 + (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R))
5.19 + --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
5.20
5.21 DC0_def "DC0 == ALL A B R. R <= A*B & R~=0 & range(R) <= domain(R)
5.22 - --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
5.23 + --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
5.24
5.25 ff_def "ff(b, X, Q, R) == transrec(b, %c r.
5.26 - THE x. first(x, {x:X. <r``c, x> : R}, Q))"
5.27 + THE x. first(x, {x:X. <r``c, x> : R}, Q))"
5.28
5.29 end
6.1 --- a/src/ZF/AC/HH.thy Mon Feb 05 21:33:14 1996 +0100
6.2 +++ b/src/ZF/AC/HH.thy Tue Feb 06 12:27:17 1996 +0100
6.3 @@ -1,6 +1,6 @@
6.4 -(* Title: ZF/AC/HH.thy
6.5 +(* Title: ZF/AC/HH.thy
6.6 ID: $Id$
6.7 - Author: Krzysztof Grabczewski
6.8 + Author: Krzysztof Grabczewski
6.9
6.10 The theory file for the proofs of
6.11 AC17 ==> AC1
7.1 --- a/src/ZF/AC/Hartog.thy Mon Feb 05 21:33:14 1996 +0100
7.2 +++ b/src/ZF/AC/Hartog.thy Tue Feb 06 12:27:17 1996 +0100
7.3 @@ -1,6 +1,6 @@
7.4 -(* Title: ZF/AC/Hartog.thy
7.5 +(* Title: ZF/AC/Hartog.thy
7.6 ID: $Id$
7.7 - Author: Krzysztof Grabczewski
7.8 + Author: Krzysztof Grabczewski
7.9
7.10 Hartog's function.
7.11 *)
8.1 --- a/src/ZF/AC/OrdQuant.thy Mon Feb 05 21:33:14 1996 +0100
8.2 +++ b/src/ZF/AC/OrdQuant.thy Tue Feb 06 12:27:17 1996 +0100
8.3 @@ -1,6 +1,6 @@
8.4 -(* Title: ZF/AC/OrdQuant.thy
8.5 +(* Title: ZF/AC/OrdQuant.thy
8.6 ID: $Id$
8.7 - Authors: Krzysztof Grabczewski and L C Paulson
8.8 + Authors: Krzysztof Grabczewski and L C Paulson
8.9
8.10 Quantifiers and union operator for ordinals.
8.11 *)
9.1 --- a/src/ZF/AC/Transrec2.thy Mon Feb 05 21:33:14 1996 +0100
9.2 +++ b/src/ZF/AC/Transrec2.thy Tue Feb 06 12:27:17 1996 +0100
9.3 @@ -1,6 +1,6 @@
9.4 -(* Title: ZF/AC/Transrec2.thy
9.5 +(* Title: ZF/AC/Transrec2.thy
9.6 ID: $Id$
9.7 - Author: Krzysztof Grabczewski
9.8 + Author: Krzysztof Grabczewski
9.9
9.10 Transfinite recursion introduced to handle definitions based on the three
9.11 cases of ordinals.
9.12 @@ -14,10 +14,10 @@
9.13
9.14 defs
9.15
9.16 - transrec2_def "transrec2(alpha, a, b) ==
9.17 - transrec(alpha, %i r. if(i=0,
9.18 - a, if(EX j. i=succ(j),
9.19 - b(THE j. i=succ(j), r`(THE j. i=succ(j))),
9.20 - UN j<i. r`j)))"
9.21 + transrec2_def "transrec2(alpha, a, b) ==
9.22 + transrec(alpha, %i r. if(i=0,
9.23 + a, if(EX j. i=succ(j),
9.24 + b(THE j. i=succ(j), r`(THE j. i=succ(j))),
9.25 + UN j<i. r`j)))"
9.26
9.27 end
10.1 --- a/src/ZF/AC/WO6_WO1.thy Mon Feb 05 21:33:14 1996 +0100
10.2 +++ b/src/ZF/AC/WO6_WO1.thy Tue Feb 06 12:27:17 1996 +0100
10.3 @@ -1,6 +1,6 @@
10.4 -(* Title: ZF/AC/WO6_WO1.thy
10.5 +(* Title: ZF/AC/WO6_WO1.thy
10.6 ID: $Id$
10.7 - Author: Krzysztof Grabczewski
10.8 + Author: Krzysztof Grabczewski
10.9
10.10 The proof of "WO6 ==> WO1".
10.11
10.12 @@ -20,18 +20,18 @@
10.13 defs
10.14
10.15 NN_def "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a &
10.16 - (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
10.17 + (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
10.18
10.19 uu_def "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
10.20
10.21 (*Definitions for case 1*)
10.22
10.23 - vv1_def "vv1(f,m,b) ==
10.24 - let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &
10.25 - domain(uu(f,b,g,d)) lepoll m));
10.26 - d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &
10.27 - domain(uu(f,b,g,d)) lepoll m
10.28 - in if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
10.29 + vv1_def "vv1(f,m,b) ==
10.30 + let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &
10.31 + domain(uu(f,b,g,d)) lepoll m));
10.32 + d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &
10.33 + domain(uu(f,b,g,d)) lepoll m
10.34 + in if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
10.35
10.36 ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
10.37
10.38 @@ -40,7 +40,7 @@
10.39 (*Definitions for case 2*)
10.40
10.41 vv2_def "vv2(f,b,g,s) ==
10.42 - if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
10.43 + if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
10.44
10.45 ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
10.46
11.1 --- a/src/ZF/AC/first.thy Mon Feb 05 21:33:14 1996 +0100
11.2 +++ b/src/ZF/AC/first.thy Tue Feb 06 12:27:17 1996 +0100
11.3 @@ -1,6 +1,6 @@
11.4 -(* Title: ZF/AC/first.thy
11.5 +(* Title: ZF/AC/first.thy
11.6 ID: $Id$
11.7 - Author: Krzysztof Grabczewski
11.8 + Author: Krzysztof Grabczewski
11.9
11.10 Theory helpful in proofs using first element of a well ordered set
11.11 *)
11.12 @@ -14,5 +14,5 @@
11.13 defs
11.14
11.15 first_def "first(u, X, R)
11.16 - == u:X & (ALL v:X. v~=u --> <u,v> : R)"
11.17 + == u:X & (ALL v:X. v~=u --> <u,v> : R)"
11.18 end
12.1 --- a/src/ZF/AC/recfunAC16.thy Mon Feb 05 21:33:14 1996 +0100
12.2 +++ b/src/ZF/AC/recfunAC16.thy Tue Feb 06 12:27:17 1996 +0100
12.3 @@ -1,6 +1,6 @@
12.4 -(* Title: ZF/AC/recfunAC16.thy
12.5 +(* Title: ZF/AC/recfunAC16.thy
12.6 ID: $Id$
12.7 - Author: Krzysztof Grabczewski
12.8 + Author: Krzysztof Grabczewski
12.9
12.10 A recursive definition used in the proof of WO2 ==> AC16
12.11 *)
12.12 @@ -15,9 +15,9 @@
12.13
12.14 recfunAC16_def
12.15 "recfunAC16(f,fa,i,a) ==
12.16 - transrec2(i, 0,
12.17 - %g r. if(EX y:r. fa`g <= y, r,
12.18 - r Un {f`(LEAST i. fa`g <= f`i &
12.19 - (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
12.20 + transrec2(i, 0,
12.21 + %g r. if(EX y:r. fa`g <= y, r,
12.22 + r Un {f`(LEAST i. fa`g <= f`i &
12.23 + (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
12.24
12.25 end
13.1 --- a/src/ZF/Arith.thy Mon Feb 05 21:33:14 1996 +0100
13.2 +++ b/src/ZF/Arith.thy Tue Feb 06 12:27:17 1996 +0100
13.3 @@ -1,6 +1,6 @@
13.4 -(* Title: ZF/arith.thy
13.5 +(* Title: ZF/arith.thy
13.6 ID: $Id$
13.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
13.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
13.9 Copyright 1992 University of Cambridge
13.10
13.11 Arithmetic operators and their definitions
13.12 @@ -9,11 +9,11 @@
13.13 Arith = Epsilon + "simpdata" +
13.14 consts
13.15 rec :: [i, i, [i,i]=>i]=>i
13.16 - "#*" :: [i,i]=>i (infixl 70)
13.17 - div :: [i,i]=>i (infixl 70)
13.18 - mod :: [i,i]=>i (infixl 70)
13.19 - "#+" :: [i,i]=>i (infixl 65)
13.20 - "#-" :: [i,i]=>i (infixl 65)
13.21 + "#*" :: [i,i]=>i (infixl 70)
13.22 + div :: [i,i]=>i (infixl 70)
13.23 + mod :: [i,i]=>i (infixl 70)
13.24 + "#+" :: [i,i]=>i (infixl 65)
13.25 + "#-" :: [i,i]=>i (infixl 65)
13.26
13.27 defs
13.28 rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
14.1 --- a/src/ZF/Bool.thy Mon Feb 05 21:33:14 1996 +0100
14.2 +++ b/src/ZF/Bool.thy Tue Feb 06 12:27:17 1996 +0100
14.3 @@ -1,6 +1,6 @@
14.4 -(* Title: ZF/bool.thy
14.5 +(* Title: ZF/bool.thy
14.6 ID: $Id$
14.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
14.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
14.9 Copyright 1992 University of Cambridge
14.10
14.11 Booleans in Zermelo-Fraenkel Set Theory
14.12 @@ -10,24 +10,24 @@
14.13
14.14 Bool = ZF + "simpdata" +
14.15 consts
14.16 - "1" :: i ("1")
14.17 + "1" :: i ("1")
14.18 "2" :: i ("2")
14.19 bool :: i
14.20 cond :: [i,i,i]=>i
14.21 - not :: i=>i
14.22 + not :: i=>i
14.23 "and" :: [i,i]=>i (infixl 70)
14.24 - or :: [i,i]=>i (infixl 65)
14.25 - xor :: [i,i]=>i (infixl 65)
14.26 + or :: [i,i]=>i (infixl 65)
14.27 + xor :: [i,i]=>i (infixl 65)
14.28
14.29 translations
14.30 "1" == "succ(0)"
14.31 "2" == "succ(1)"
14.32
14.33 defs
14.34 - bool_def "bool == {0,1}"
14.35 - cond_def "cond(b,c,d) == if(b=1,c,d)"
14.36 - not_def "not(b) == cond(b,0,1)"
14.37 - and_def "a and b == cond(a,b,0)"
14.38 - or_def "a or b == cond(a,1,b)"
14.39 - xor_def "a xor b == cond(a,not(b),b)"
14.40 + bool_def "bool == {0,1}"
14.41 + cond_def "cond(b,c,d) == if(b=1,c,d)"
14.42 + not_def "not(b) == cond(b,0,1)"
14.43 + and_def "a and b == cond(a,b,0)"
14.44 + or_def "a or b == cond(a,1,b)"
14.45 + xor_def "a xor b == cond(a,not(b),b)"
14.46 end
15.1 --- a/src/ZF/Cardinal.thy Mon Feb 05 21:33:14 1996 +0100
15.2 +++ b/src/ZF/Cardinal.thy Tue Feb 06 12:27:17 1996 +0100
15.3 @@ -1,6 +1,6 @@
15.4 -(* Title: ZF/Cardinal.thy
15.5 +(* Title: ZF/Cardinal.thy
15.6 ID: $Id$
15.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
15.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
15.9 Copyright 1994 University of Cambridge
15.10
15.11 Cardinals in Zermelo-Fraenkel Set Theory
16.1 --- a/src/ZF/CardinalArith.thy Mon Feb 05 21:33:14 1996 +0100
16.2 +++ b/src/ZF/CardinalArith.thy Tue Feb 06 12:27:17 1996 +0100
16.3 @@ -1,6 +1,6 @@
16.4 -(* Title: ZF/CardinalArith.thy
16.5 +(* Title: ZF/CardinalArith.thy
16.6 ID: $Id$
16.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
16.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
16.9 Copyright 1994 University of Cambridge
16.10
16.11 Cardinal Arithmetic
17.1 --- a/src/ZF/Cardinal_AC.thy Mon Feb 05 21:33:14 1996 +0100
17.2 +++ b/src/ZF/Cardinal_AC.thy Tue Feb 06 12:27:17 1996 +0100
17.3 @@ -1,6 +1,6 @@
17.4 -(* Title: ZF/Cardinal_AC.thy
17.5 +(* Title: ZF/Cardinal_AC.thy
17.6 ID: $Id$
17.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
17.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
17.9 Copyright 1994 University of Cambridge
17.10
17.11 Cardinal Arithmetic WITH the Axiom of Choice
18.1 --- a/src/ZF/Coind/BCR.thy Mon Feb 05 21:33:14 1996 +0100
18.2 +++ b/src/ZF/Coind/BCR.thy Tue Feb 06 12:27:17 1996 +0100
18.3 @@ -1,6 +1,6 @@
18.4 -(* Title: ZF/Coind/BCR.thy
18.5 +(* Title: ZF/Coind/BCR.thy
18.6 ID: $Id$
18.7 - Author: Jacob Frost, Cambridge University Computer Laboratory
18.8 + Author: Jacob Frost, Cambridge University Computer Laboratory
18.9 Copyright 1995 University of Cambridge
18.10 *)
18.11
18.12 @@ -19,9 +19,9 @@
18.13 consts
18.14 isofenv :: [i,i] => o
18.15 defs
18.16 - isofenv_def "isofenv(ve,te) ==
18.17 - ve_dom(ve) = te_dom(te) &
18.18 - ( ALL x:ve_dom(ve).
18.19 + isofenv_def "isofenv(ve,te) ==
18.20 + ve_dom(ve) = te_dom(te) &
18.21 + ( ALL x:ve_dom(ve).
18.22 EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
18.23
18.24 end
19.1 --- a/src/ZF/Coind/Dynamic.thy Mon Feb 05 21:33:14 1996 +0100
19.2 +++ b/src/ZF/Coind/Dynamic.thy Tue Feb 06 12:27:17 1996 +0100
19.3 @@ -1,6 +1,6 @@
19.4 -(* Title: ZF/Coind/Dynamic.thy
19.5 +(* Title: ZF/Coind/Dynamic.thy
19.6 ID: $Id$
19.7 - Author: Jacob Frost, Cambridge University Computer Laboratory
19.8 + Author: Jacob Frost, Cambridge University Computer Laboratory
19.9 Copyright 1995 University of Cambridge
19.10 *)
19.11
20.1 --- a/src/ZF/Coind/ECR.thy Mon Feb 05 21:33:14 1996 +0100
20.2 +++ b/src/ZF/Coind/ECR.thy Tue Feb 06 12:27:17 1996 +0100
20.3 @@ -1,6 +1,6 @@
20.4 -(* Title: ZF/Coind/ECR.thy
20.5 +(* Title: ZF/Coind/ECR.thy
20.6 ID: $Id$
20.7 - Author: Jacob Frost, Cambridge University Computer Laboratory
20.8 + Author: Jacob Frost, Cambridge University Computer Laboratory
20.9 Copyright 1995 University of Cambridge
20.10 *)
20.11
20.12 @@ -17,9 +17,9 @@
20.13 "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
20.14 htr_closI
20.15 "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv;
20.16 - <te,e_fn(x,e),t>:ElabRel;
20.17 - ve_dom(ve) = te_dom(te);
20.18 - {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)
20.19 + <te,e_fn(x,e),t>:ElabRel;
20.20 + ve_dom(ve) = te_dom(te);
20.21 + {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)
20.22 |] ==>
20.23 <v_clos(x,e,ve),t>:HasTyRel"
20.24 monos "[Pow_mono]"
20.25 @@ -31,8 +31,8 @@
20.26 hastyenv :: [i,i] => o
20.27 defs
20.28 hastyenv_def
20.29 - " hastyenv(ve,te) ==
20.30 - ve_dom(ve) = te_dom(te) &
20.31 + " hastyenv(ve,te) ==
20.32 + ve_dom(ve) = te_dom(te) &
20.33 (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
20.34
20.35 end
21.1 --- a/src/ZF/Coind/Language.thy Mon Feb 05 21:33:14 1996 +0100
21.2 +++ b/src/ZF/Coind/Language.thy Tue Feb 06 12:27:17 1996 +0100
21.3 @@ -1,14 +1,14 @@
21.4 -(* Title: ZF/Coind/Language.thy
21.5 +(* Title: ZF/Coind/Language.thy
21.6 ID: $Id$
21.7 - Author: Jacob Frost, Cambridge University Computer Laboratory
21.8 + Author: Jacob Frost, Cambridge University Computer Laboratory
21.9 Copyright 1995 University of Cambridge
21.10 *)
21.11
21.12 Language ="Datatype" + QUniv +
21.13
21.14 consts
21.15 - Const :: i (* Abstract type of constants *)
21.16 - c_app :: [i,i] => i (*Abstract constructor for fun application*)
21.17 + Const :: i (* Abstract type of constants *)
21.18 + c_app :: [i,i] => i (*Abstract constructor for fun application*)
21.19
21.20 rules
21.21 constNEE "c:Const ==> c ~= 0"
21.22 @@ -16,8 +16,8 @@
21.23
21.24
21.25 consts
21.26 - Exp :: i (* Datatype of expressions *)
21.27 - ExVar :: i (* Abstract type of variables *)
21.28 + Exp :: i (* Datatype of expressions *)
21.29 + ExVar :: i (* Abstract type of variables *)
21.30 datatype <= "univ(Const Un ExVar)"
21.31 "Exp" = e_const("c:Const")
21.32 | e_var("x:ExVar")
22.1 --- a/src/ZF/Coind/Map.thy Mon Feb 05 21:33:14 1996 +0100
22.2 +++ b/src/ZF/Coind/Map.thy Tue Feb 06 12:27:17 1996 +0100
22.3 @@ -1,6 +1,6 @@
22.4 -(* Title: ZF/Coind/Map.thy
22.5 +(* Title: ZF/Coind/Map.thy
22.6 ID: $Id$
22.7 - Author: Jacob Frost, Cambridge University Computer Laboratory
22.8 + Author: Jacob Frost, Cambridge University Computer Laboratory
22.9 Copyright 1995 University of Cambridge
22.10 *)
22.11
23.1 --- a/src/ZF/Coind/Static.thy Mon Feb 05 21:33:14 1996 +0100
23.2 +++ b/src/ZF/Coind/Static.thy Tue Feb 06 12:27:17 1996 +0100
23.3 @@ -1,6 +1,6 @@
23.4 -(* Title: ZF/Coind/Static.thy
23.5 +(* Title: ZF/Coind/Static.thy
23.6 ID: $Id$
23.7 - Author: Jacob Frost, Cambridge University Computer Laboratory
23.8 + Author: Jacob Frost, Cambridge University Computer Laboratory
23.9 Copyright 1995 University of Cambridge
23.10 *)
23.11
24.1 --- a/src/ZF/Coind/Types.thy Mon Feb 05 21:33:14 1996 +0100
24.2 +++ b/src/ZF/Coind/Types.thy Tue Feb 06 12:27:17 1996 +0100
24.3 @@ -1,14 +1,14 @@
24.4 -(* Title: ZF/Coind/Types.thy
24.5 +(* Title: ZF/Coind/Types.thy
24.6 ID: $Id$
24.7 - Author: Jacob Frost, Cambridge University Computer Laboratory
24.8 + Author: Jacob Frost, Cambridge University Computer Laboratory
24.9 Copyright 1995 University of Cambridge
24.10 *)
24.11
24.12 Types = Language +
24.13
24.14 consts
24.15 - Ty :: i (* Datatype of types *)
24.16 - TyConst :: i (* Abstract type of type constants *)
24.17 + Ty :: i (* Datatype of types *)
24.18 + TyConst :: i (* Abstract type of type constants *)
24.19 datatype <= "univ(TyConst)"
24.20 "Ty" = t_const("tc:TyConst")
24.21 | t_fun("t1:Ty","t2:Ty")
25.1 --- a/src/ZF/Coind/Values.thy Mon Feb 05 21:33:14 1996 +0100
25.2 +++ b/src/ZF/Coind/Values.thy Tue Feb 06 12:27:17 1996 +0100
25.3 @@ -1,6 +1,6 @@
25.4 -(* Title: ZF/Coind/Values.thy
25.5 +(* Title: ZF/Coind/Values.thy
25.6 ID: $Id$
25.7 - Author: Jacob Frost, Cambridge University Computer Laboratory
25.8 + Author: Jacob Frost, Cambridge University Computer Laboratory
25.9 Copyright 1995 University of Cambridge
25.10 *)
25.11
26.1 --- a/src/ZF/Epsilon.thy Mon Feb 05 21:33:14 1996 +0100
26.2 +++ b/src/ZF/Epsilon.thy Tue Feb 06 12:27:17 1996 +0100
26.3 @@ -1,6 +1,6 @@
26.4 -(* Title: ZF/epsilon.thy
26.5 +(* Title: ZF/epsilon.thy
26.6 ID: $Id$
26.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
26.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
26.9 Copyright 1993 University of Cambridge
26.10
26.11 Epsilon induction and recursion
26.12 @@ -12,7 +12,7 @@
26.13 transrec :: [i, [i,i]=>i] =>i
26.14
26.15 defs
26.16 - eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
26.17 - transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
26.18 - rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
26.19 + eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
26.20 + transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
26.21 + rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
26.22 end
27.1 --- a/src/ZF/EquivClass.thy Mon Feb 05 21:33:14 1996 +0100
27.2 +++ b/src/ZF/EquivClass.thy Tue Feb 06 12:27:17 1996 +0100
27.3 @@ -1,6 +1,6 @@
27.4 -(* Title: ZF/EquivClass.thy
27.5 +(* Title: ZF/EquivClass.thy
27.6 ID: $Id$
27.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
27.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
27.9 Copyright 1994 University of Cambridge
27.10
27.11 Equivalence relations in Zermelo-Fraenkel Set Theory
27.12 @@ -9,7 +9,7 @@
27.13 EquivClass = Rel + Perm +
27.14 consts
27.15 "'/" :: [i,i]=>i (infixl 90) (*set of equiv classes*)
27.16 - congruent :: [i,i=>i]=>o
27.17 + congruent :: [i,i=>i]=>o
27.18 congruent2 :: [i,[i,i]=>i]=>o
27.19
27.20 defs
28.1 --- a/src/ZF/Finite.thy Mon Feb 05 21:33:14 1996 +0100
28.2 +++ b/src/ZF/Finite.thy Tue Feb 06 12:27:17 1996 +0100
28.3 @@ -1,6 +1,6 @@
28.4 -(* Title: ZF/Finite.thy
28.5 +(* Title: ZF/Finite.thy
28.6 ID: $Id$
28.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
28.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
28.9 Copyright 1994 University of Cambridge
28.10
28.11 Finite powerset operator
28.12 @@ -8,8 +8,8 @@
28.13
28.14 Finite = Arith + Inductive +
28.15 consts
28.16 - Fin :: i=>i
28.17 - FiniteFun :: [i,i]=>i ("(_ -||>/ _)" [61, 60] 60)
28.18 + Fin :: i=>i
28.19 + FiniteFun :: [i,i]=>i ("(_ -||>/ _)" [61, 60] 60)
28.20
28.21 inductive
28.22 domains "Fin(A)" <= "Pow(A)"
28.23 @@ -24,6 +24,6 @@
28.24 intrs
28.25 emptyI "0 : A -||> B"
28.26 consI "[| a: A; b: B; h: A -||> B; a ~: domain(h)
28.27 - |] ==> cons(<a,b>,h) : A -||> B"
28.28 + |] ==> cons(<a,b>,h) : A -||> B"
28.29 type_intrs "Fin.intrs"
28.30 end
29.1 --- a/src/ZF/Fixedpt.thy Mon Feb 05 21:33:14 1996 +0100
29.2 +++ b/src/ZF/Fixedpt.thy Tue Feb 06 12:27:17 1996 +0100
29.3 @@ -1,6 +1,6 @@
29.4 -(* Title: ZF/fixedpt.thy
29.5 +(* Title: ZF/fixedpt.thy
29.6 ID: $Id$
29.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
29.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
29.9 Copyright 1992 University of Cambridge
29.10
29.11 Least and greatest fixed points
30.1 --- a/src/ZF/IMP/Com.thy Mon Feb 05 21:33:14 1996 +0100
30.2 +++ b/src/ZF/IMP/Com.thy Tue Feb 06 12:27:17 1996 +0100
30.3 @@ -1,6 +1,6 @@
30.4 -(* Title: ZF/IMP/Com.thy
30.5 +(* Title: ZF/IMP/Com.thy
30.6 ID: $Id$
30.7 - Author: Heiko Loetzbeyer & Robert Sandner, TUM
30.8 + Author: Heiko Loetzbeyer & Robert Sandner, TUM
30.9 Copyright 1994 TUM
30.10
30.11 Arithmetic expressions, Boolean expressions, Commands
30.12 @@ -23,14 +23,14 @@
30.13
30.14 (** Evaluation of arithmetic expressions **)
30.15 consts evala :: i
30.16 - "@evala" :: [i,i,i] => o ("<_,_>/ -a-> _" [0,0,50] 50)
30.17 + "@evala" :: [i,i,i] => o ("<_,_>/ -a-> _" [0,0,50] 50)
30.18 translations
30.19 "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
30.20 inductive
30.21 domains "evala" <= "aexp * (loc -> nat) * nat"
30.22 intrs
30.23 N "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
30.24 - X "[| x:loc; sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
30.25 + X "[| x:loc; sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
30.26 Op1 "[| <e,sigma> -a-> n; f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
30.27 Op2 "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f: (nat*nat) -> nat |]
30.28 ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
30.29 @@ -46,13 +46,13 @@
30.30 | false
30.31 | ROp ("f: (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
30.32 | noti ("b : bexp")
30.33 - | andi ("b0 : bexp", "b1 : bexp") (infixl 60)
30.34 - | ori ("b0 : bexp", "b1 : bexp") (infixl 60)
30.35 + | andi ("b0 : bexp", "b1 : bexp") (infixl 60)
30.36 + | ori ("b0 : bexp", "b1 : bexp") (infixl 60)
30.37
30.38
30.39 (** Evaluation of boolean expressions **)
30.40 -consts evalb :: i
30.41 - "@evalb" :: [i,i,i] => o ("<_,_>/ -b-> _" [0,0,50] 50)
30.42 +consts evalb :: i
30.43 + "@evalb" :: [i,i,i] => o ("<_,_>/ -b-> _" [0,0,50] 50)
30.44
30.45 translations
30.46 "<be,sig> -b-> b" == "<be,sig,b> : evalb"
30.47 @@ -63,15 +63,15 @@
30.48 tru "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
30.49 fls "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
30.50 ROp "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |]
30.51 - ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
30.52 + ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
30.53 noti "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
30.54 andi "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
30.55 ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
30.56 ori "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
30.57 - ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
30.58 + ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
30.59
30.60 type_intrs "bexp.intrs @
30.61 - [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
30.62 + [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
30.63 type_elims "[make_elim(evala.dom_subset RS subsetD)]"
30.64
30.65
30.66 @@ -80,24 +80,24 @@
30.67
30.68 datatype <= "univ(loc Un aexp Un bexp)"
30.69 "com" = skip
30.70 - | ":=" ("x:loc", "a:aexp") (infixl 60)
30.71 - | semic ("c0:com", "c1:com") ("_; _" [60, 60] 10)
30.72 - | while ("b:bexp", "c:com") ("while _ do _" 60)
30.73 - | ifc ("b:bexp", "c0:com", "c1:com") ("ifc _ then _ else _" 60)
30.74 + | ":=" ("x:loc", "a:aexp") (infixl 60)
30.75 + | semic ("c0:com", "c1:com") ("_; _" [60, 60] 10)
30.76 + | while ("b:bexp", "c:com") ("while _ do _" 60)
30.77 + | ifc ("b:bexp", "c0:com", "c1:com") ("ifc _ then _ else _" 60)
30.78
30.79 (*Constructor ";" has low precedence to avoid syntactic ambiguities
30.80 with [| m: nat; x: loc; ... |] ==> ... It usually will need parentheses.*)
30.81
30.82 (** Execution of commands **)
30.83 consts evalc :: i
30.84 - "@evalc" :: [i,i,i] => o ("<_,_>/ -c-> _" [0,0,50] 50)
30.85 - "assign" :: [i,i,i] => i ("_[_'/_]" [95,0,0] 95)
30.86 + "@evalc" :: [i,i,i] => o ("<_,_>/ -c-> _" [0,0,50] 50)
30.87 + "assign" :: [i,i,i] => i ("_[_'/_]" [95,0,0] 95)
30.88
30.89 translations
30.90 "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
30.91
30.92 defs
30.93 - assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
30.94 + assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
30.95
30.96 inductive
30.97 domains "evalc" <= "com * (loc -> nat) * (loc -> nat)"
30.98 @@ -111,11 +111,11 @@
30.99 <c0 ; c1, sigma> -c-> sigma1"
30.100
30.101 ifc1 "[| b:bexp; c1:com; sigma:loc->nat;
30.102 - <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==>
30.103 + <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==>
30.104 <ifc b then c0 else c1, sigma> -c-> sigma1"
30.105
30.106 ifc0 "[| b:bexp; c0:com; sigma:loc->nat;
30.107 - <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==>
30.108 + <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==>
30.109 <ifc b then c0 else c1, sigma> -c-> sigma1"
30.110
30.111 while0 "[| c: com; <b, sigma> -b-> 0 |] ==>
30.112 @@ -128,6 +128,6 @@
30.113 con_defs "[assign_def]"
30.114 type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
30.115 type_elims "[make_elim(evala.dom_subset RS subsetD),
30.116 - make_elim(evalb.dom_subset RS subsetD) ]"
30.117 + make_elim(evalb.dom_subset RS subsetD) ]"
30.118
30.119 end
31.1 --- a/src/ZF/IMP/Denotation.thy Mon Feb 05 21:33:14 1996 +0100
31.2 +++ b/src/ZF/IMP/Denotation.thy Tue Feb 06 12:27:17 1996 +0100
31.3 @@ -1,6 +1,6 @@
31.4 -(* Title: ZF/IMP/Denotation.thy
31.5 +(* Title: ZF/IMP/Denotation.thy
31.6 ID: $Id$
31.7 - Author: Heiko Loetzbeyer & Robert Sandner, TUM
31.8 + Author: Heiko Loetzbeyer & Robert Sandner, TUM
31.9 Copyright 1994 TUM
31.10
31.11 Denotational semantics of expressions & commands
31.12 @@ -14,33 +14,33 @@
31.13 C :: i => i
31.14 Gamma :: [i,i,i] => i
31.15
31.16 -rules (*NOT definitional*)
31.17 - A_nat_def "A(N(n)) == (%sigma. n)"
31.18 - A_loc_def "A(X(x)) == (%sigma. sigma`x)"
31.19 - A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
31.20 - A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
31.21 +rules (*NOT definitional*)
31.22 + A_nat_def "A(N(n)) == (%sigma. n)"
31.23 + A_loc_def "A(X(x)) == (%sigma. sigma`x)"
31.24 + A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
31.25 + A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
31.26
31.27
31.28 - B_true_def "B(true) == (%sigma. 1)"
31.29 - B_false_def "B(false) == (%sigma. 0)"
31.30 - B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
31.31 + B_true_def "B(true) == (%sigma. 1)"
31.32 + B_false_def "B(false) == (%sigma. 0)"
31.33 + B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
31.34
31.35
31.36 - B_not_def "B(noti(b)) == (%sigma. not(B(b,sigma)))"
31.37 - B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
31.38 - B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
31.39 + B_not_def "B(noti(b)) == (%sigma. not(B(b,sigma)))"
31.40 + B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
31.41 + B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
31.42
31.43 - C_skip_def "C(skip) == id(loc->nat)"
31.44 - C_assign_def "C(x := a) == {io:(loc->nat)*(loc->nat).
31.45 - snd(io) = fst(io)[A(a,fst(io))/x]}"
31.46 + C_skip_def "C(skip) == id(loc->nat)"
31.47 + C_assign_def "C(x := a) == {io:(loc->nat)*(loc->nat).
31.48 + snd(io) = fst(io)[A(a,fst(io))/x]}"
31.49
31.50 - C_comp_def "C(c0 ; c1) == C(c1) O C(c0)"
31.51 - C_if_def "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un
31.52 - {io:C(c1). B(b,fst(io))=0}"
31.53 + C_comp_def "C(c0 ; c1) == C(c1) O C(c0)"
31.54 + C_if_def "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un
31.55 + {io:C(c1). B(b,fst(io))=0}"
31.56
31.57 - Gamma_def "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un
31.58 - {io : id(loc->nat). B(b,fst(io))=0})"
31.59 + Gamma_def "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un
31.60 + {io : id(loc->nat). B(b,fst(io))=0})"
31.61
31.62 - C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
31.63 + C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
31.64
31.65 end
32.1 --- a/src/ZF/IMP/Equiv.thy Mon Feb 05 21:33:14 1996 +0100
32.2 +++ b/src/ZF/IMP/Equiv.thy Tue Feb 06 12:27:17 1996 +0100
32.3 @@ -1,6 +1,6 @@
32.4 -(* Title: ZF/IMP/Equiv.thy
32.5 +(* Title: ZF/IMP/Equiv.thy
32.6 ID: $Id$
32.7 - Author: Heiko Loetzbeyer & Robert Sandner, TUM
32.8 + Author: Heiko Loetzbeyer & Robert Sandner, TUM
32.9 Copyright 1994 TUM
32.10 *)
32.11
33.1 --- a/src/ZF/Let.thy Mon Feb 05 21:33:14 1996 +0100
33.2 +++ b/src/ZF/Let.thy Tue Feb 06 12:27:17 1996 +0100
33.3 @@ -1,6 +1,6 @@
33.4 -(* Title: ZF/Let
33.5 +(* Title: ZF/Let
33.6 ID: $Id$
33.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
33.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
33.9 Copyright 1995 University of Cambridge
33.10
33.11 Let expressions, and tuple pattern-matching (borrowed from HOL)
34.1 --- a/src/ZF/List.thy Mon Feb 05 21:33:14 1996 +0100
34.2 +++ b/src/ZF/List.thy Tue Feb 06 12:27:17 1996 +0100
34.3 @@ -1,6 +1,6 @@
34.4 -(* Title: ZF/List
34.5 +(* Title: ZF/List
34.6 ID: $Id$
34.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
34.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
34.9 Copyright 1994 University of Cambridge
34.10
34.11 Lists in Zermelo-Fraenkel Set Theory
34.12 @@ -13,20 +13,20 @@
34.13 List = Datatype +
34.14
34.15 consts
34.16 - "@" :: [i,i]=>i (infixr 60)
34.17 + "@" :: [i,i]=>i (infixr 60)
34.18 list_rec :: [i, i, [i,i,i]=>i] => i
34.19 - map :: [i=>i, i] => i
34.20 + map :: [i=>i, i] => i
34.21 length,rev :: i=>i
34.22 flat :: i=>i
34.23 list_add :: i=>i
34.24 hd,tl :: i=>i
34.25 - drop :: [i,i]=>i
34.26 + drop :: [i,i]=>i
34.27
34.28 (* List Enumeration *)
34.29 - "[]" :: i ("[]")
34.30 - "@List" :: is => i ("[(_)]")
34.31 + "[]" :: i ("[]")
34.32 + "@List" :: is => i ("[(_)]")
34.33
34.34 - list :: i=>i
34.35 + list :: i=>i
34.36
34.37
34.38 datatype
34.39 @@ -41,9 +41,9 @@
34.40
34.41 defs
34.42
34.43 - hd_def "hd(l) == list_case(0, %x xs.x, l)"
34.44 - tl_def "tl(l) == list_case(Nil, %x xs.xs, l)"
34.45 - drop_def "drop(i,l) == rec(i, l, %j r. tl(r))"
34.46 + hd_def "hd(l) == list_case(0, %x xs.x, l)"
34.47 + tl_def "tl(l) == list_case(Nil, %x xs.xs, l)"
34.48 + drop_def "drop(i,l) == rec(i, l, %j r. tl(r))"
34.49
34.50 list_rec_def
34.51 "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
35.1 --- a/src/ZF/Nat.thy Mon Feb 05 21:33:14 1996 +0100
35.2 +++ b/src/ZF/Nat.thy Tue Feb 06 12:27:17 1996 +0100
35.3 @@ -1,6 +1,6 @@
35.4 -(* Title: ZF/Nat.thy
35.5 +(* Title: ZF/Nat.thy
35.6 ID: $Id$
35.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
35.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
35.9 Copyright 1994 University of Cambridge
35.10
35.11 Natural numbers in Zermelo-Fraenkel Set Theory
35.12 @@ -8,7 +8,7 @@
35.13
35.14 Nat = Ordinal + Bool + "mono" +
35.15 consts
35.16 - nat :: i
35.17 + nat :: i
35.18 nat_case :: [i, i=>i, i]=>i
35.19 nat_rec :: [i, i, [i,i]=>i]=>i
35.20
35.21 @@ -17,10 +17,10 @@
35.22 nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
35.23
35.24 nat_case_def
35.25 - "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
35.26 + "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
35.27
35.28 nat_rec_def
35.29 - "nat_rec(k,a,b) ==
35.30 - wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
35.31 + "nat_rec(k,a,b) ==
35.32 + wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
35.33
35.34 end
36.1 --- a/src/ZF/Order.thy Mon Feb 05 21:33:14 1996 +0100
36.2 +++ b/src/ZF/Order.thy Tue Feb 06 12:27:17 1996 +0100
36.3 @@ -1,6 +1,6 @@
36.4 -(* Title: ZF/Order.thy
36.5 +(* Title: ZF/Order.thy
36.6 ID: $Id$
36.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
36.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
36.9 Copyright 1994 University of Cambridge
36.10
36.11 Orders in Zermelo-Fraenkel Set Theory
36.12 @@ -8,13 +8,13 @@
36.13
36.14 Order = WF + Perm +
36.15 consts
36.16 - part_ord :: [i,i]=>o (*Strict partial ordering*)
36.17 - linear, tot_ord :: [i,i]=>o (*Strict total ordering*)
36.18 - well_ord :: [i,i]=>o (*Well-ordering*)
36.19 - mono_map :: [i,i,i,i]=>i (*Order-preserving maps*)
36.20 - ord_iso :: [i,i,i,i]=>i (*Order isomorphisms*)
36.21 - pred :: [i,i,i]=>i (*Set of predecessors*)
36.22 - ord_iso_map :: [i,i,i,i]=>i (*Construction for linearity theorem*)
36.23 + part_ord :: [i,i]=>o (*Strict partial ordering*)
36.24 + linear, tot_ord :: [i,i]=>o (*Strict total ordering*)
36.25 + well_ord :: [i,i]=>o (*Well-ordering*)
36.26 + mono_map :: [i,i,i,i]=>i (*Order-preserving maps*)
36.27 + ord_iso :: [i,i,i,i]=>i (*Order isomorphisms*)
36.28 + pred :: [i,i,i]=>i (*Set of predecessors*)
36.29 + ord_iso_map :: [i,i,i,i]=>i (*Construction for linearity theorem*)
36.30
36.31 defs
36.32 part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
37.1 --- a/src/ZF/OrderArith.thy Mon Feb 05 21:33:14 1996 +0100
37.2 +++ b/src/ZF/OrderArith.thy Tue Feb 06 12:27:17 1996 +0100
37.3 @@ -1,6 +1,6 @@
37.4 -(* Title: ZF/OrderArith.thy
37.5 +(* Title: ZF/OrderArith.thy
37.6 ID: $Id$
37.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
37.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
37.9 Copyright 1994 University of Cambridge
37.10
37.11 Towards ordinal arithmetic
37.12 @@ -15,14 +15,14 @@
37.13 (*disjoint sum of two relations; underlies ordinal addition*)
37.14 radd_def "radd(A,r,B,s) ==
37.15 {z: (A+B) * (A+B).
37.16 - (EX x y. z = <Inl(x), Inr(y)>) |
37.17 - (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) |
37.18 + (EX x y. z = <Inl(x), Inr(y)>) |
37.19 + (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) |
37.20 (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
37.21
37.22 (*lexicographic product of two relations; underlies ordinal multiplication*)
37.23 rmult_def "rmult(A,r,B,s) ==
37.24 {z: (A*B) * (A*B).
37.25 - EX x' y' x y. z = <<x',y'>, <x,y>> &
37.26 + EX x' y' x y. z = <<x',y'>, <x,y>> &
37.27 (<x',x>: r | (x'=x & <y',y>: s))}"
37.28
37.29 (*inverse image of a relation*)
38.1 --- a/src/ZF/OrderType.thy Mon Feb 05 21:33:14 1996 +0100
38.2 +++ b/src/ZF/OrderType.thy Tue Feb 06 12:27:17 1996 +0100
38.3 @@ -1,6 +1,6 @@
38.4 -(* Title: ZF/OrderType.thy
38.5 +(* Title: ZF/OrderType.thy
38.6 ID: $Id$
38.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
38.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
38.9 Copyright 1994 University of Cambridge
38.10
38.11 Order types and ordinal arithmetic.
39.1 --- a/src/ZF/Ordinal.thy Mon Feb 05 21:33:14 1996 +0100
39.2 +++ b/src/ZF/Ordinal.thy Tue Feb 06 12:27:17 1996 +0100
39.3 @@ -1,6 +1,6 @@
39.4 -(* Title: ZF/Ordinal.thy
39.5 +(* Title: ZF/Ordinal.thy
39.6 ID: $Id$
39.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
39.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
39.9 Copyright 1994 University of Cambridge
39.10
39.11 Ordinals in Zermelo-Fraenkel Set Theory
39.12 @@ -8,7 +8,7 @@
39.13
39.14 Ordinal = WF + Bool + "simpdata" + "equalities" +
39.15 consts
39.16 - Memrel :: i=>i
39.17 + Memrel :: i=>i
39.18 Transset,Ord :: i=>o
39.19 "<" :: [i,i] => o (infixl 50) (*less than on ordinals*)
39.20 "le" :: [i,i] => o (infixl 50) (*less than or equals*)
39.21 @@ -18,9 +18,9 @@
39.22 "x le y" == "x < succ(y)"
39.23
39.24 defs
39.25 - Memrel_def "Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }"
39.26 - Transset_def "Transset(i) == ALL x:i. x<=i"
39.27 - Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))"
39.28 + Memrel_def "Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }"
39.29 + Transset_def "Transset(i) == ALL x:i. x<=i"
39.30 + Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))"
39.31 lt_def "i<j == i:j & Ord(j)"
39.32 Limit_def "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
39.33
40.1 --- a/src/ZF/Perm.thy Mon Feb 05 21:33:14 1996 +0100
40.2 +++ b/src/ZF/Perm.thy Tue Feb 06 12:27:17 1996 +0100
40.3 @@ -1,6 +1,6 @@
40.4 -(* Title: ZF/perm
40.5 +(* Title: ZF/perm
40.6 ID: $Id$
40.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
40.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
40.9 Copyright 1991 University of Cambridge
40.10
40.11 The theory underlying permutation groups
40.12 @@ -11,26 +11,26 @@
40.13
40.14 Perm = ZF + "mono" +
40.15 consts
40.16 - O :: [i,i]=>i (infixr 60)
40.17 - id :: i=>i
40.18 + O :: [i,i]=>i (infixr 60)
40.19 + id :: i=>i
40.20 inj,surj,bij:: [i,i]=>i
40.21
40.22 defs
40.23
40.24 (*composition of relations and functions; NOT Suppes's relative product*)
40.25 - comp_def "r O s == {xz : domain(s)*range(r) .
40.26 - EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
40.27 + comp_def "r O s == {xz : domain(s)*range(r) .
40.28 + EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
40.29
40.30 (*the identity function for A*)
40.31 - id_def "id(A) == (lam x:A. x)"
40.32 + id_def "id(A) == (lam x:A. x)"
40.33
40.34 (*one-to-one functions from A to B*)
40.35 inj_def "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
40.36
40.37 (*onto functions from A to B*)
40.38 - surj_def "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
40.39 + surj_def "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
40.40
40.41 (*one-to-one and onto functions*)
40.42 - bij_def "bij(A,B) == inj(A,B) Int surj(A,B)"
40.43 + bij_def "bij(A,B) == inj(A,B) Int surj(A,B)"
40.44
40.45 end
41.1 --- a/src/ZF/QPair.thy Mon Feb 05 21:33:14 1996 +0100
41.2 +++ b/src/ZF/QPair.thy Tue Feb 06 12:27:17 1996 +0100
41.3 @@ -1,6 +1,6 @@
41.4 -(* Title: ZF/qpair.thy
41.5 +(* Title: ZF/qpair.thy
41.6 ID: $Id$
41.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
41.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
41.9 Copyright 1993 University of Cambridge
41.10
41.11 Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
41.12 @@ -13,19 +13,19 @@
41.13
41.14 QPair = Sum + "simpdata" +
41.15 consts
41.16 - QPair :: [i, i] => i ("<(_;/ _)>")
41.17 + QPair :: [i, i] => i ("<(_;/ _)>")
41.18 qfst,qsnd :: i => i
41.19 qsplit :: [[i, i] => 'a, i] => 'a::logic (*for pattern-matching*)
41.20 qconverse :: i => i
41.21 QSigma :: [i, i => i] => i
41.22
41.23 - "<+>" :: [i,i]=>i (infixr 65)
41.24 + "<+>" :: [i,i]=>i (infixr 65)
41.25 QInl,QInr :: i=>i
41.26 qcase :: [i=>i, i=>i, i]=>i
41.27
41.28 syntax
41.29 "@QSUM" :: [idt, i, i] => i ("(3QSUM _:_./ _)" 10)
41.30 - "<*>" :: [i, i] => i (infixr 80)
41.31 + "<*>" :: [i, i] => i (infixr 80)
41.32
41.33 translations
41.34 "QSUM x:A. B" => "QSigma(A, %x. B)"
42.1 --- a/src/ZF/QUniv.thy Mon Feb 05 21:33:14 1996 +0100
42.2 +++ b/src/ZF/QUniv.thy Tue Feb 06 12:27:17 1996 +0100
42.3 @@ -1,6 +1,6 @@
42.4 -(* Title: ZF/univ.thy
42.5 +(* Title: ZF/univ.thy
42.6 ID: $Id$
42.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
42.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
42.9 Copyright 1993 University of Cambridge
42.10
42.11 A small universe for lazy recursive types
43.1 --- a/src/ZF/Rel.thy Mon Feb 05 21:33:14 1996 +0100
43.2 +++ b/src/ZF/Rel.thy Tue Feb 06 12:27:17 1996 +0100
43.3 @@ -1,6 +1,6 @@
43.4 -(* Title: ZF/Rel.thy
43.5 +(* Title: ZF/Rel.thy
43.6 ID: $Id$
43.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
43.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
43.9 Copyright 1994 University of Cambridge
43.10
43.11 Relations in Zermelo-Fraenkel Set Theory
43.12 @@ -10,7 +10,7 @@
43.13 consts
43.14 refl,irrefl,equiv :: [i,i]=>o
43.15 sym,asym,antisym,trans :: i=>o
43.16 - trans_on :: [i,i]=>o ("trans[_]'(_')")
43.17 + trans_on :: [i,i]=>o ("trans[_]'(_')")
43.18
43.19 defs
43.20 refl_def "refl(A,r) == (ALL x: A. <x,x> : r)"
43.21 @@ -25,7 +25,7 @@
43.22
43.23 trans_def "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
43.24
43.25 - trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.
43.26 + trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.
43.27 <x,y>: r --> <y,z>: r --> <x,z>: r"
43.28
43.29 equiv_def "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
44.1 --- a/src/ZF/Resid/Confluence.thy Mon Feb 05 21:33:14 1996 +0100
44.2 +++ b/src/ZF/Resid/Confluence.thy Tue Feb 06 12:27:17 1996 +0100
44.3 @@ -1,6 +1,6 @@
44.4 -(* Title: Confluence.thy
44.5 +(* Title: Confluence.thy
44.6 ID: $Id$
44.7 - Author: Ole Rasmussen
44.8 + Author: Ole Rasmussen
44.9 Copyright 1995 University of Cambridge
44.10 Logic Image: ZF
44.11 *)
44.12 @@ -8,14 +8,14 @@
44.13 Confluence = Reduction+
44.14
44.15 consts
44.16 - confluence :: i=>o
44.17 - strip :: o
44.18 + confluence :: i=>o
44.19 + strip :: o
44.20
44.21 defs
44.22 confluence_def "confluence(R) ==
44.23 - ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->
44.24 - (EX u.<y,u>:R & <z,u>:R))"
44.25 + ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->
44.26 + (EX u.<y,u>:R & <z,u>:R))"
44.27 strip_def "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) -->
44.28 - (EX u.(y =1=> u) & (z===>u)))"
44.29 + (EX u.(y =1=> u) & (z===>u)))"
44.30 end
44.31
45.1 --- a/src/ZF/Resid/Conversion.thy Mon Feb 05 21:33:14 1996 +0100
45.2 +++ b/src/ZF/Resid/Conversion.thy Tue Feb 06 12:27:17 1996 +0100
45.3 @@ -1,6 +1,6 @@
45.4 -(* Title: Conversion.thy
45.5 +(* Title: Conversion.thy
45.6 ID: $Id$
45.7 - Author: Ole Rasmussen
45.8 + Author: Ole Rasmussen
45.9 Copyright 1995 University of Cambridge
45.10 Logic Image: ZF
45.11
45.12 @@ -9,10 +9,10 @@
45.13 Conversion = Confluence+
45.14
45.15 consts
45.16 - Sconv1 :: i
45.17 - "<-1->" :: [i,i]=>o (infixl 50)
45.18 - Sconv :: i
45.19 - "<--->" :: [i,i]=>o (infixl 50)
45.20 + Sconv1 :: i
45.21 + "<-1->" :: [i,i]=>o (infixl 50)
45.22 + Sconv :: i
45.23 + "<--->" :: [i,i]=>o (infixl 50)
45.24
45.25 translations
45.26 "a<-1->b" == "<a,b>:Sconv1"
45.27 @@ -21,16 +21,16 @@
45.28 inductive
45.29 domains "Sconv1" <= "lambda*lambda"
45.30 intrs
45.31 - red1 "m -1-> n ==> m<-1->n"
45.32 - expl "n -1-> m ==> m<-1->n"
45.33 - type_intrs "[red1D1,red1D2]@lambda.intrs@bool_typechecks"
45.34 + red1 "m -1-> n ==> m<-1->n"
45.35 + expl "n -1-> m ==> m<-1->n"
45.36 + type_intrs "[red1D1,red1D2]@lambda.intrs@bool_typechecks"
45.37
45.38 inductive
45.39 domains "Sconv" <= "lambda*lambda"
45.40 intrs
45.41 - one_step "m<-1->n ==> m<--->n"
45.42 - refl "m:lambda ==> m<--->m"
45.43 - trans "[|m<--->n; n<--->p|] ==> m<--->p"
45.44 - type_intrs "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
45.45 + one_step "m<-1->n ==> m<--->n"
45.46 + refl "m:lambda ==> m<--->m"
45.47 + trans "[|m<--->n; n<--->p|] ==> m<--->p"
45.48 + type_intrs "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
45.49 end
45.50
46.1 --- a/src/ZF/Resid/Cube.thy Mon Feb 05 21:33:14 1996 +0100
46.2 +++ b/src/ZF/Resid/Cube.thy Tue Feb 06 12:27:17 1996 +0100
46.3 @@ -1,6 +1,6 @@
46.4 -(* Title: Cube.thy
46.5 +(* Title: Cube.thy
46.6 ID: $Id$
46.7 - Author: Ole Rasmussen
46.8 + Author: Ole Rasmussen
46.9 Copyright 1995 University of Cambridge
46.10 Logic Image: ZF
46.11 *)
47.1 --- a/src/ZF/Resid/Redex.thy Mon Feb 05 21:33:14 1996 +0100
47.2 +++ b/src/ZF/Resid/Redex.thy Tue Feb 06 12:27:17 1996 +0100
47.3 @@ -1,6 +1,6 @@
47.4 -(* Title: Redex.thy
47.5 +(* Title: Redex.thy
47.6 ID: $Id$
47.7 - Author: Ole Rasmussen
47.8 + Author: Ole Rasmussen
47.9 Copyright 1995 University of Cambridge
47.10 Logic Image: ZF
47.11 *)
47.12 @@ -10,14 +10,14 @@
47.13 redexes :: i
47.14
47.15 datatype
47.16 - "redexes" = Var ("n: nat")
47.17 + "redexes" = Var ("n: nat")
47.18 | Fun ("t: redexes")
47.19 | App ("b:bool" ,"f:redexes" , "a:redexes")
47.20 type_intrs "[bool_into_univ]"
47.21
47.22
47.23 consts
47.24 - redex_rec :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
47.25 + redex_rec :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
47.26
47.27 defs
47.28 redex_rec_def
48.1 --- a/src/ZF/Resid/Reduction.thy Mon Feb 05 21:33:14 1996 +0100
48.2 +++ b/src/ZF/Resid/Reduction.thy Tue Feb 06 12:27:17 1996 +0100
48.3 @@ -1,6 +1,6 @@
48.4 -(* Title: Reduction.thy
48.5 +(* Title: Reduction.thy
48.6 ID: $Id$
48.7 - Author: Ole Rasmussen
48.8 + Author: Ole Rasmussen
48.9 Copyright 1995 University of Cambridge
48.10 Logic Image: ZF
48.11 *)
48.12 @@ -21,39 +21,39 @@
48.13 inductive
48.14 domains "Sred1" <= "lambda*lambda"
48.15 intrs
48.16 - beta "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
48.17 - rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
48.18 - apl_l "[|m2:lambda; m1 -1-> n1|] ==>
48.19 - Apl(m1,m2) -1-> Apl(n1,m2)"
48.20 - apl_r "[|m1:lambda; m2 -1-> n2|] ==>
48.21 - Apl(m1,m2) -1-> Apl(m1,n2)"
48.22 - type_intrs "red_typechecks"
48.23 + beta "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
48.24 + rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
48.25 + apl_l "[|m2:lambda; m1 -1-> n1|] ==>
48.26 + Apl(m1,m2) -1-> Apl(n1,m2)"
48.27 + apl_r "[|m1:lambda; m2 -1-> n2|] ==>
48.28 + Apl(m1,m2) -1-> Apl(m1,n2)"
48.29 + type_intrs "red_typechecks"
48.30
48.31 inductive
48.32 domains "Sred" <= "lambda*lambda"
48.33 intrs
48.34 - one_step "[|m-1->n|] ==> m--->n"
48.35 - refl "m:lambda==>m --->m"
48.36 - trans "[|m--->n; n--->p|]==>m--->p"
48.37 - type_intrs "[Sred1.dom_subset RS subsetD]@red_typechecks"
48.38 + one_step "[|m-1->n|] ==> m--->n"
48.39 + refl "m:lambda==>m --->m"
48.40 + trans "[|m--->n; n--->p|]==>m--->p"
48.41 + type_intrs "[Sred1.dom_subset RS subsetD]@red_typechecks"
48.42
48.43 inductive
48.44 domains "Spar_red1" <= "lambda*lambda"
48.45 intrs
48.46 - beta "[|m =1=> m';
48.47 - n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
48.48 - rvar "n:nat==> Var(n) =1=> Var(n)"
48.49 - rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
48.50 - rapl "[|m =1=> m';
48.51 - n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
48.52 - type_intrs "red_typechecks"
48.53 + beta "[|m =1=> m';
48.54 + n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
48.55 + rvar "n:nat==> Var(n) =1=> Var(n)"
48.56 + rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
48.57 + rapl "[|m =1=> m';
48.58 + n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
48.59 + type_intrs "red_typechecks"
48.60
48.61 inductive
48.62 domains "Spar_red" <= "lambda*lambda"
48.63 intrs
48.64 - one_step "[|m =1=> n|] ==> m ===> n"
48.65 - trans "[|m===>n; n===>p|]==>m===>p"
48.66 - type_intrs "[Spar_red1.dom_subset RS subsetD]@red_typechecks"
48.67 + one_step "[|m =1=> n|] ==> m ===> n"
48.68 + trans "[|m===>n; n===>p|]==>m===>p"
48.69 + type_intrs "[Spar_red1.dom_subset RS subsetD]@red_typechecks"
48.70
48.71
48.72 end
49.1 --- a/src/ZF/Resid/Residuals.thy Mon Feb 05 21:33:14 1996 +0100
49.2 +++ b/src/ZF/Resid/Residuals.thy Tue Feb 06 12:27:17 1996 +0100
49.3 @@ -1,6 +1,6 @@
49.4 -(* Title: Residuals.thy
49.5 +(* Title: Residuals.thy
49.6 ID: $Id$
49.7 - Author: Ole Rasmussen
49.8 + Author: Ole Rasmussen
49.9 Copyright 1995 University of Cambridge
49.10 Logic Image: ZF
49.11
49.12 @@ -9,9 +9,9 @@
49.13 Residuals = Substitution+
49.14
49.15 consts
49.16 - Sres :: i
49.17 - residuals :: [i,i,i]=>i
49.18 - "|>" :: [i,i]=>i (infixl 70)
49.19 + Sres :: i
49.20 + residuals :: [i,i,i]=>i
49.21 + "|>" :: [i,i]=>i (infixl 70)
49.22
49.23 translations
49.24 "residuals(u,v,w)" == "<u,v,w>:Sres"
49.25 @@ -19,16 +19,16 @@
49.26 inductive
49.27 domains "Sres" <= "redexes*redexes*redexes"
49.28 intrs
49.29 - Res_Var "n:nat ==> residuals(Var(n),Var(n),Var(n))"
49.30 - Res_Fun "[|residuals(u,v,w)|]==>
49.31 - residuals(Fun(u),Fun(v),Fun(w))"
49.32 - Res_App "[|residuals(u1,v1,w1);
49.33 - residuals(u2,v2,w2); b:bool|]==>
49.34 - residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
49.35 - Res_redex "[|residuals(u1,v1,w1);
49.36 - residuals(u2,v2,w2); b:bool|]==>
49.37 - residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
49.38 - type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
49.39 + Res_Var "n:nat ==> residuals(Var(n),Var(n),Var(n))"
49.40 + Res_Fun "[|residuals(u,v,w)|]==>
49.41 + residuals(Fun(u),Fun(v),Fun(w))"
49.42 + Res_App "[|residuals(u1,v1,w1);
49.43 + residuals(u2,v2,w2); b:bool|]==>
49.44 + residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
49.45 + Res_redex "[|residuals(u1,v1,w1);
49.46 + residuals(u2,v2,w2); b:bool|]==>
49.47 + residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
49.48 + type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
49.49
49.50 rules
49.51 res_func_def "u |> v == THE w.residuals(u,v,w)"
50.1 --- a/src/ZF/Resid/SubUnion.thy Mon Feb 05 21:33:14 1996 +0100
50.2 +++ b/src/ZF/Resid/SubUnion.thy Tue Feb 06 12:27:17 1996 +0100
50.3 @@ -1,6 +1,6 @@
50.4 -(* Title: SubUnion.thy
50.5 +(* Title: SubUnion.thy
50.6 ID: $Id$
50.7 - Author: Ole Rasmussen
50.8 + Author: Ole Rasmussen
50.9 Copyright 1995 University of Cambridge
50.10 Logic Image: ZF
50.11 *)
50.12 @@ -11,7 +11,7 @@
50.13 Ssub,Scomp,Sreg :: i
50.14 "<==","~" :: [i,i]=>o (infixl 70)
50.15 un :: [i,i]=>i (infixl 70)
50.16 - regular :: i=>o
50.17 + regular :: i=>o
50.18
50.19 translations
50.20 "a<==b" == "<a,b>:Ssub"
50.21 @@ -21,39 +21,39 @@
50.22 inductive
50.23 domains "Ssub" <= "redexes*redexes"
50.24 intrs
50.25 - Sub_Var "n:nat ==> Var(n)<== Var(n)"
50.26 - Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
50.27 - Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==>
50.28 - App(0,u1,u2)<== App(b,v1,v2)"
50.29 - Sub_App2 "[|u1<== v1; u2<== v2|]==>
50.30 - App(1,u1,u2)<== App(1,v1,v2)"
50.31 - type_intrs "redexes.intrs@bool_typechecks"
50.32 + Sub_Var "n:nat ==> Var(n)<== Var(n)"
50.33 + Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
50.34 + Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==>
50.35 + App(0,u1,u2)<== App(b,v1,v2)"
50.36 + Sub_App2 "[|u1<== v1; u2<== v2|]==>
50.37 + App(1,u1,u2)<== App(1,v1,v2)"
50.38 + type_intrs "redexes.intrs@bool_typechecks"
50.39
50.40 inductive
50.41 domains "Scomp" <= "redexes*redexes"
50.42 intrs
50.43 - Comp_Var "n:nat ==> Var(n) ~ Var(n)"
50.44 - Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
50.45 - Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>
50.46 - App(b1,u1,u2) ~ App(b2,v1,v2)"
50.47 - type_intrs "redexes.intrs@bool_typechecks"
50.48 + Comp_Var "n:nat ==> Var(n) ~ Var(n)"
50.49 + Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
50.50 + Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>
50.51 + App(b1,u1,u2) ~ App(b2,v1,v2)"
50.52 + type_intrs "redexes.intrs@bool_typechecks"
50.53
50.54 inductive
50.55 domains "Sreg" <= "redexes"
50.56 intrs
50.57 - Reg_Var "n:nat ==> regular(Var(n))"
50.58 - Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
50.59 - Reg_App1 "[|regular(Fun(u)); regular(v)
50.60 - |]==>regular(App(1,Fun(u),v))"
50.61 - Reg_App2 "[|regular(u); regular(v)
50.62 - |]==>regular(App(0,u,v))"
50.63 - type_intrs "redexes.intrs@bool_typechecks"
50.64 + Reg_Var "n:nat ==> regular(Var(n))"
50.65 + Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
50.66 + Reg_App1 "[|regular(Fun(u)); regular(v)
50.67 + |]==>regular(App(1,Fun(u),v))"
50.68 + Reg_App2 "[|regular(u); regular(v)
50.69 + |]==>regular(App(0,u,v))"
50.70 + type_intrs "redexes.intrs@bool_typechecks"
50.71
50.72 defs
50.73 union_def "u un v == redex_rec(u,
50.74 - %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),
50.75 + %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),
50.76 %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),
50.77 %b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,
50.78 - %c z u. App(b or c, m`z, p`u), t))`v"
50.79 + %c z u. App(b or c, m`z, p`u), t))`v"
50.80 end
50.81
51.1 --- a/src/ZF/Resid/Substitution.thy Mon Feb 05 21:33:14 1996 +0100
51.2 +++ b/src/ZF/Resid/Substitution.thy Tue Feb 06 12:27:17 1996 +0100
51.3 @@ -1,6 +1,6 @@
51.4 -(* Title: Substitution.thy
51.5 +(* Title: Substitution.thy
51.6 ID: $Id$
51.7 - Author: Ole Rasmussen
51.8 + Author: Ole Rasmussen
51.9 Copyright 1995 University of Cambridge
51.10 Logic Image: ZF
51.11 *)
51.12 @@ -8,19 +8,19 @@
51.13 Substitution = SubUnion +
51.14
51.15 consts
51.16 - lift_rec :: [i,i]=> i
51.17 - lift :: i=>i
51.18 - subst_rec :: [i,i,i]=> i
51.19 + lift_rec :: [i,i]=> i
51.20 + lift :: i=>i
51.21 + subst_rec :: [i,i,i]=> i
51.22 "'/" :: [i,i]=>i (infixl 70) (*subst*)
51.23 translations
51.24 "lift(r)" == "lift_rec(r,0)"
51.25 "u/v" == "subst_rec(u,v,0)"
51.26
51.27 defs
51.28 - lift_rec_def "lift_rec(r,kg) ==
51.29 - redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))),
51.30 - %x m.(lam k:nat.Fun(m`(succ(k)))),
51.31 - %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
51.32 + lift_rec_def "lift_rec(r,kg) ==
51.33 + redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))),
51.34 + %x m.(lam k:nat.Fun(m`(succ(k)))),
51.35 + %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
51.36
51.37
51.38 (* subst_rec(u,Var(i),k) = if k<i then Var(i-1)
51.39 @@ -30,15 +30,15 @@
51.40 subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))
51.41
51.42 *)
51.43 - subst_rec_def "subst_rec(u,t,kg) ==
51.44 - redex_rec(t,
51.45 - %i.(lam r:redexes.lam k:nat.
51.46 - if(k<i,Var(i#-1),
51.47 - if(k=i,r,Var(i)))),
51.48 - %x m.(lam r:redexes.lam k:nat.
51.49 + subst_rec_def "subst_rec(u,t,kg) ==
51.50 + redex_rec(t,
51.51 + %i.(lam r:redexes.lam k:nat.
51.52 + if(k<i,Var(i#-1),
51.53 + if(k=i,r,Var(i)))),
51.54 + %x m.(lam r:redexes.lam k:nat.
51.55 Fun(m`(lift(r))`(succ(k)))),
51.56 - %b x y m p.lam r:redexes.lam k:nat.
51.57 - App(b,m`r`k,p`r`k))`u`kg"
51.58 + %b x y m p.lam r:redexes.lam k:nat.
51.59 + App(b,m`r`k,p`r`k))`u`kg"
51.60
51.61
51.62 end
52.1 --- a/src/ZF/Resid/Terms.thy Mon Feb 05 21:33:14 1996 +0100
52.2 +++ b/src/ZF/Resid/Terms.thy Tue Feb 06 12:27:17 1996 +0100
52.3 @@ -1,6 +1,6 @@
52.4 -(* Title: Terms.thy
52.5 +(* Title: Terms.thy
52.6 ID: $Id$
52.7 - Author: Ole Rasmussen
52.8 + Author: Ole Rasmussen
52.9 Copyright 1995 University of Cambridge
52.10 Logic Image: ZF
52.11 *)
52.12 @@ -8,9 +8,9 @@
52.13 Terms = Cube+
52.14
52.15 consts
52.16 - lambda :: i
52.17 - unmark :: i=>i
52.18 - Apl :: [i,i]=>i
52.19 + lambda :: i
52.20 + unmark :: i=>i
52.21 + Apl :: [i,i]=>i
52.22
52.23 translations
52.24 "Apl(n,m)" == "App(0,n,m)"
52.25 @@ -18,15 +18,15 @@
52.26 inductive
52.27 domains "lambda" <= "redexes"
52.28 intrs
52.29 - Lambda_Var " n:nat ==> Var(n):lambda"
52.30 - Lambda_Fun " u:lambda ==> Fun(u):lambda"
52.31 - Lambda_App "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
52.32 - type_intrs "redexes.intrs@bool_typechecks"
52.33 + Lambda_Var " n:nat ==> Var(n):lambda"
52.34 + Lambda_Fun " u:lambda ==> Fun(u):lambda"
52.35 + Lambda_App "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
52.36 + type_intrs "redexes.intrs@bool_typechecks"
52.37
52.38 defs
52.39 - unmark_def "unmark(u) == redex_rec(u,%i.Var(i),
52.40 - %x m.Fun(m),
52.41 - %b x y m p.Apl(m,p))"
52.42 + unmark_def "unmark(u) == redex_rec(u,%i.Var(i),
52.43 + %x m.Fun(m),
52.44 + %b x y m p.Apl(m,p))"
52.45 end
52.46
52.47
53.1 --- a/src/ZF/Sum.thy Mon Feb 05 21:33:14 1996 +0100
53.2 +++ b/src/ZF/Sum.thy Tue Feb 06 12:27:17 1996 +0100
53.3 @@ -1,6 +1,6 @@
53.4 -(* Title: ZF/sum.thy
53.5 +(* Title: ZF/sum.thy
53.6 ID: $Id$
53.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
53.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
53.9 Copyright 1993 University of Cambridge
53.10
53.11 Disjoint sums in Zermelo-Fraenkel Set Theory
53.12 @@ -9,7 +9,7 @@
53.13
53.14 Sum = Bool + "simpdata" +
53.15 consts
53.16 - "+" :: [i,i]=>i (infixr 65)
53.17 + "+" :: [i,i]=>i (infixr 65)
53.18 Inl,Inr :: i=>i
53.19 case :: [i=>i, i=>i, i]=>i
53.20 Part :: [i,i=>i] => i
53.21 @@ -21,5 +21,5 @@
53.22 case_def "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))"
53.23
53.24 (*operator for selecting out the various summands*)
53.25 - Part_def "Part(A,h) == {x: A. EX z. x = h(z)}"
53.26 + Part_def "Part(A,h) == {x: A. EX z. x = h(z)}"
53.27 end
54.1 --- a/src/ZF/Trancl.thy Mon Feb 05 21:33:14 1996 +0100
54.2 +++ b/src/ZF/Trancl.thy Tue Feb 06 12:27:17 1996 +0100
54.3 @@ -1,6 +1,6 @@
54.4 -(* Title: ZF/trancl.thy
54.5 +(* Title: ZF/trancl.thy
54.6 ID: $Id$
54.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
54.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
54.9 Copyright 1992 University of Cambridge
54.10
54.11 Transitive closure of a relation
54.12 @@ -12,6 +12,6 @@
54.13 trancl :: i=>i ("(_^+)" [100] 100) (*transitive closure*)
54.14
54.15 defs
54.16 - rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
54.17 + rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
54.18 trancl_def "r^+ == r O r^*"
54.19 end
55.1 --- a/src/ZF/Univ.thy Mon Feb 05 21:33:14 1996 +0100
55.2 +++ b/src/ZF/Univ.thy Tue Feb 06 12:27:17 1996 +0100
55.3 @@ -1,6 +1,6 @@
55.4 -(* Title: ZF/univ.thy
55.5 +(* Title: ZF/univ.thy
55.6 ID: $Id$
55.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
55.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
55.9 Copyright 1992 University of Cambridge
55.10
55.11 The cumulative hierarchy and a small universe for recursive types
55.12 @@ -19,13 +19,13 @@
55.13 univ :: i=>i
55.14
55.15 translations
55.16 - "Vset(x)" == "Vfrom(0,x)"
55.17 + "Vset(x)" == "Vfrom(0,x)"
55.18
55.19 defs
55.20 Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
55.21
55.22 Vrec_def
55.23 - "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
55.24 + "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
55.25 H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
55.26
55.27 univ_def "univ(A) == Vfrom(A,nat)"
56.1 --- a/src/ZF/WF.thy Mon Feb 05 21:33:14 1996 +0100
56.2 +++ b/src/ZF/WF.thy Tue Feb 06 12:27:17 1996 +0100
56.3 @@ -1,6 +1,6 @@
56.4 -(* Title: ZF/wf.thy
56.5 +(* Title: ZF/wf.thy
56.6 ID: $Id$
56.7 - Author: Tobias Nipkow and Lawrence C Paulson
56.8 + Author: Tobias Nipkow and Lawrence C Paulson
56.9 Copyright 1994 University of Cambridge
56.10
56.11 Well-founded Recursion
56.12 @@ -9,26 +9,26 @@
56.13 WF = Trancl + "mono" + "equalities" +
56.14 consts
56.15 wf :: i=>o
56.16 - wf_on :: [i,i]=>o ("wf[_]'(_')")
56.17 + wf_on :: [i,i]=>o ("wf[_]'(_')")
56.18
56.19 wftrec,wfrec :: [i, i, [i,i]=>i] =>i
56.20 - wfrec_on :: [i, i, i, [i,i]=>i] =>i ("wfrec[_]'(_,_,_')")
56.21 + wfrec_on :: [i, i, i, [i,i]=>i] =>i ("wfrec[_]'(_,_,_')")
56.22 is_recfun :: [i, i, [i,i]=>i, i] =>o
56.23 the_recfun :: [i, i, [i,i]=>i] =>i
56.24
56.25 defs
56.26 (*r is a well-founded relation*)
56.27 - wf_def "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
56.28 + wf_def "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
56.29
56.30 (*r is well-founded relation over A*)
56.31 wf_on_def "wf_on(A,r) == wf(r Int A*A)"
56.32
56.33 is_recfun_def "is_recfun(r,a,H,f) ==
56.34 - (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
56.35 + (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
56.36
56.37 the_recfun_def "the_recfun(r,a,H) == (THE f.is_recfun(r,a,H,f))"
56.38
56.39 - wftrec_def "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
56.40 + wftrec_def "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
56.41
56.42 (*public version. Does not require r to be transitive*)
56.43 wfrec_def "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
57.1 --- a/src/ZF/ZF.thy Mon Feb 05 21:33:14 1996 +0100
57.2 +++ b/src/ZF/ZF.thy Tue Feb 06 12:27:17 1996 +0100
57.3 @@ -61,7 +61,7 @@
57.4 range :: i => i
57.5 field :: i => i
57.6 converse :: i => i
57.7 - function :: i => o (*is a relation a function?*)
57.8 + function :: i => o (*is a relation a function?*)
57.9 Lambda :: [i, i => i] => i
57.10 restrict :: [i, i] => i
57.11
57.12 @@ -214,8 +214,8 @@
57.13 domain_def "domain(r) == {x. w:r, EX y. w=<x,y>}"
57.14 range_def "range(r) == domain(converse(r))"
57.15 field_def "field(r) == domain(r) Un range(r)"
57.16 - function_def "function(r) == ALL x y. <x,y>:r -->
57.17 - (ALL y'. <x,y'>:r --> y=y')"
57.18 + function_def "function(r) == ALL x y. <x,y>:r -->
57.19 + (ALL y'. <x,y'>:r --> y=y')"
57.20 image_def "r `` A == {y : range(r) . EX x:A. <x,y> : r}"
57.21 vimage_def "r -`` A == converse(r)``A"
57.22
58.1 --- a/src/ZF/Zorn.thy Mon Feb 05 21:33:14 1996 +0100
58.2 +++ b/src/ZF/Zorn.thy Tue Feb 06 12:27:17 1996 +0100
58.3 @@ -1,6 +1,6 @@
58.4 -(* Title: ZF/Zorn.thy
58.5 +(* Title: ZF/Zorn.thy
58.6 ID: $Id$
58.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
58.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
58.9 Copyright 1994 University of Cambridge
58.10
58.11 Based upon the article
58.12 @@ -39,10 +39,10 @@
58.13 inductive
58.14 domains "TFin(S,next)" <= "Pow(S)"
58.15 intrs
58.16 - nextI "[| x : TFin(S,next); next: increasing(S)
58.17 + nextI "[| x : TFin(S,next); next: increasing(S)
58.18 |] ==> next`x : TFin(S,next)"
58.19
58.20 - Pow_UnionI "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
58.21 + Pow_UnionI "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
58.22
58.23 monos "[Pow_mono]"
58.24 con_defs "[increasing_def]"
59.1 --- a/src/ZF/ex/Acc.thy Mon Feb 05 21:33:14 1996 +0100
59.2 +++ b/src/ZF/ex/Acc.thy Tue Feb 06 12:27:17 1996 +0100
59.3 @@ -1,6 +1,6 @@
59.4 -(* Title: ZF/ex/Acc.thy
59.5 +(* Title: ZF/ex/Acc.thy
59.6 ID: $Id$
59.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
59.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
59.9 Copyright 1994 University of Cambridge
59.10
59.11 Inductive definition of acc(r)
60.1 --- a/src/ZF/ex/BT.thy Mon Feb 05 21:33:14 1996 +0100
60.2 +++ b/src/ZF/ex/BT.thy Tue Feb 06 12:27:17 1996 +0100
60.3 @@ -1,6 +1,6 @@
60.4 -(* Title: ZF/ex/BT.thy
60.5 +(* Title: ZF/ex/BT.thy
60.6 ID: $Id$
60.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
60.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
60.9 Copyright 1992 University of Cambridge
60.10
60.11 Binary trees
60.12 @@ -8,12 +8,12 @@
60.13
60.14 BT = Datatype +
60.15 consts
60.16 - bt_rec :: [i, i, [i,i,i,i,i]=>i] => i
60.17 - n_nodes :: i=>i
60.18 - n_leaves :: i=>i
60.19 - bt_reflect :: i=>i
60.20 + bt_rec :: [i, i, [i,i,i,i,i]=>i] => i
60.21 + n_nodes :: i=>i
60.22 + n_leaves :: i=>i
60.23 + bt_reflect :: i=>i
60.24
60.25 - bt :: i=>i
60.26 + bt :: i=>i
60.27
60.28 datatype
60.29 "bt(A)" = Lf | Br ("a: A", "t1: bt(A)", "t2: bt(A)")
60.30 @@ -22,8 +22,8 @@
60.31 bt_rec_def
60.32 "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
60.33
60.34 - n_nodes_def "n_nodes(t) == bt_rec(t, 0, %x y z r s. succ(r#+s))"
60.35 - n_leaves_def "n_leaves(t) == bt_rec(t, succ(0), %x y z r s. r#+s)"
60.36 + n_nodes_def "n_nodes(t) == bt_rec(t, 0, %x y z r s. succ(r#+s))"
60.37 + n_leaves_def "n_leaves(t) == bt_rec(t, succ(0), %x y z r s. r#+s)"
60.38 bt_reflect_def "bt_reflect(t) == bt_rec(t, Lf, %x y z r s. Br(x,s,r))"
60.39
60.40 end
61.1 --- a/src/ZF/ex/Brouwer.thy Mon Feb 05 21:33:14 1996 +0100
61.2 +++ b/src/ZF/ex/Brouwer.thy Tue Feb 06 12:27:17 1996 +0100
61.3 @@ -1,6 +1,6 @@
61.4 -(* Title: ZF/ex/Brouwer.thy
61.5 +(* Title: ZF/ex/Brouwer.thy
61.6 ID: $ $
61.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
61.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
61.9 Copyright 1994 University of Cambridge
61.10
61.11 Infinite branching datatype definitions
61.12 @@ -15,15 +15,15 @@
61.13
61.14 datatype <= "Vfrom(0, csucc(nat))"
61.15 "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
61.16 - monos "[Pi_mono]"
61.17 + monos "[Pi_mono]"
61.18 type_intrs "inf_datatype_intrs"
61.19
61.20 (*The union with nat ensures that the cardinal is infinite*)
61.21 datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
61.22 "Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
61.23 - monos "[Pi_mono]"
61.24 + monos "[Pi_mono]"
61.25 type_intrs "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]
61.26 - @ inf_datatype_intrs"
61.27 + @ inf_datatype_intrs"
61.28
61.29
61.30 end
62.1 --- a/src/ZF/ex/CoUnit.thy Mon Feb 05 21:33:14 1996 +0100
62.2 +++ b/src/ZF/ex/CoUnit.thy Tue Feb 06 12:27:17 1996 +0100
62.3 @@ -1,6 +1,6 @@
62.4 -(* Title: ZF/ex/CoUnit.ML
62.5 +(* Title: ZF/ex/CoUnit.ML
62.6 ID: $Id$
62.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
62.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
62.9 Copyright 1994 University of Cambridge
62.10
62.11 Trivial codatatype definitions, one of which goes wrong!
63.1 --- a/src/ZF/ex/Comb.thy Mon Feb 05 21:33:14 1996 +0100
63.2 +++ b/src/ZF/ex/Comb.thy Tue Feb 06 12:27:17 1996 +0100
63.3 @@ -1,6 +1,6 @@
63.4 -(* Title: ZF/ex/Comb.thy
63.5 +(* Title: ZF/ex/Comb.thy
63.6 ID: $Id$
63.7 - Author: Lawrence C Paulson
63.8 + Author: Lawrence C Paulson
63.9 Copyright 1994 University of Cambridge
63.10
63.11 Combinatory Logic example: the Church-Rosser Theorem
63.12 @@ -27,8 +27,8 @@
63.13 **)
63.14 consts
63.15 contract :: i
63.16 - "-1->" :: [i,i] => o (infixl 50)
63.17 - "--->" :: [i,i] => o (infixl 50)
63.18 + "-1->" :: [i,i] => o (infixl 50)
63.19 + "--->" :: [i,i] => o (infixl 50)
63.20
63.21 translations
63.22 "p -1-> q" == "<p,q> : contract"
63.23 @@ -49,8 +49,8 @@
63.24 **)
63.25 consts
63.26 parcontract :: i
63.27 - "=1=>" :: [i,i] => o (infixl 50)
63.28 - "===>" :: [i,i] => o (infixl 50)
63.29 + "=1=>" :: [i,i] => o (infixl 50)
63.30 + "===>" :: [i,i] => o (infixl 50)
63.31
63.32 translations
63.33 "p =1=> q" == "<p,q> : parcontract"
64.1 --- a/src/ZF/ex/Data.thy Mon Feb 05 21:33:14 1996 +0100
64.2 +++ b/src/ZF/ex/Data.thy Tue Feb 06 12:27:17 1996 +0100
64.3 @@ -1,6 +1,6 @@
64.4 -(* Title: ZF/ex/Data.thy
64.5 +(* Title: ZF/ex/Data.thy
64.6 ID: $Id$
64.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
64.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
64.9 Copyright 1994 University of Cambridge
64.10
64.11 Sample datatype definition.
65.1 --- a/src/ZF/ex/Enum.thy Mon Feb 05 21:33:14 1996 +0100
65.2 +++ b/src/ZF/ex/Enum.thy Tue Feb 06 12:27:17 1996 +0100
65.3 @@ -1,6 +1,6 @@
65.4 -(* Title: ZF/ex/Enum
65.5 +(* Title: ZF/ex/Enum
65.6 ID: $Id$
65.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
65.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
65.9 Copyright 1993 University of Cambridge
65.10
65.11 Example of a BIG enumeration type
66.1 --- a/src/ZF/ex/Integ.thy Mon Feb 05 21:33:14 1996 +0100
66.2 +++ b/src/ZF/ex/Integ.thy Tue Feb 06 12:27:17 1996 +0100
66.3 @@ -1,6 +1,6 @@
66.4 -(* Title: ZF/ex/integ.thy
66.5 +(* Title: ZF/ex/integ.thy
66.6 ID: $Id$
66.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
66.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
66.9 Copyright 1993 University of Cambridge
66.10
66.11 The integers as equivalence classes over nat*nat.
66.12 @@ -9,34 +9,34 @@
66.13 Integ = EquivClass + Arith +
66.14 consts
66.15 intrel,integ:: i
66.16 - znat :: i=>i ("$# _" [80] 80)
66.17 - zminus :: i=>i ("$~ _" [80] 80)
66.18 - znegative :: i=>o
66.19 - zmagnitude :: i=>i
66.20 + znat :: i=>i ("$# _" [80] 80)
66.21 + zminus :: i=>i ("$~ _" [80] 80)
66.22 + znegative :: i=>o
66.23 + zmagnitude :: i=>i
66.24 "$*" :: [i,i]=>i (infixl 70)
66.25 "$'/" :: [i,i]=>i (infixl 70)
66.26 "$'/'/" :: [i,i]=>i (infixl 70)
66.27 - "$+" :: [i,i]=>i (infixl 65)
66.28 + "$+" :: [i,i]=>i (infixl 65)
66.29 "$-" :: [i,i]=>i (infixl 65)
66.30 - "$<" :: [i,i]=>o (infixl 50)
66.31 + "$<" :: [i,i]=>o (infixl 50)
66.32
66.33 defs
66.34
66.35 intrel_def
66.36 - "intrel == {p:(nat*nat)*(nat*nat).
66.37 + "intrel == {p:(nat*nat)*(nat*nat).
66.38 EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
66.39
66.40 integ_def "integ == (nat*nat)/intrel"
66.41
66.42 - znat_def "$# m == intrel `` {<m,0>}"
66.43 + znat_def "$# m == intrel `` {<m,0>}"
66.44
66.45 - zminus_def "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
66.46 + zminus_def "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
66.47
66.48 znegative_def
66.49 - "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
66.50 + "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
66.51
66.52 zmagnitude_def
66.53 - "zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
66.54 + "zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
66.55
66.56 (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
66.57 Perhaps a "curried" or even polymorphic congruent predicate would be
66.58 @@ -47,7 +47,7 @@
66.59 in intrel``{<x1#+x2, y1#+y2>}"
66.60
66.61 zdiff_def "Z1 $- Z2 == Z1 $+ zminus(Z2)"
66.62 - zless_def "Z1 $< Z2 == znegative(Z1 $- Z2)"
66.63 + zless_def "Z1 $< Z2 == znegative(Z1 $- Z2)"
66.64
66.65 (*This illustrates the primitive form of definitions (no patterns)*)
66.66 zmult_def
67.1 --- a/src/ZF/ex/LList.thy Mon Feb 05 21:33:14 1996 +0100
67.2 +++ b/src/ZF/ex/LList.thy Tue Feb 06 12:27:17 1996 +0100
67.3 @@ -1,6 +1,6 @@
67.4 -(* Title: ZF/ex/LList.thy
67.5 +(* Title: ZF/ex/LList.thy
67.6 ID: $Id$
67.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
67.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
67.9 Copyright 1994 University of Cambridge
67.10
67.11 Codatatype definition of Lazy Lists
68.1 --- a/src/ZF/ex/Limit.thy Mon Feb 05 21:33:14 1996 +0100
68.2 +++ b/src/ZF/ex/Limit.thy Tue Feb 06 12:27:17 1996 +0100
68.3 @@ -1,6 +1,6 @@
68.4 -(* Title: ZF/ex/Limit
68.5 +(* Title: ZF/ex/Limit
68.6 ID: $Id$
68.7 - Author: Sten Agerholm
68.8 + Author: Sten Agerholm
68.9
68.10 A formalization of the inverse limit construction of domain theory.
68.11
69.1 --- a/src/ZF/ex/ListN.thy Mon Feb 05 21:33:14 1996 +0100
69.2 +++ b/src/ZF/ex/ListN.thy Tue Feb 06 12:27:17 1996 +0100
69.3 @@ -1,6 +1,6 @@
69.4 -(* Title: ZF/ex/ListN
69.5 +(* Title: ZF/ex/ListN
69.6 ID: $Id$
69.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
69.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
69.9 Copyright 1994 University of Cambridge
69.10
69.11 Inductive definition of lists of n elements
69.12 @@ -10,7 +10,7 @@
69.13 *)
69.14
69.15 ListN = List +
69.16 -consts listn ::i=>i
69.17 +consts listn ::i=>i
69.18 inductive
69.19 domains "listn(A)" <= "nat*list(A)"
69.20 intrs
70.1 --- a/src/ZF/ex/Ntree.thy Mon Feb 05 21:33:14 1996 +0100
70.2 +++ b/src/ZF/ex/Ntree.thy Tue Feb 06 12:27:17 1996 +0100
70.3 @@ -1,6 +1,6 @@
70.4 -(* Title: ZF/ex/Ntree.ML
70.5 +(* Title: ZF/ex/Ntree.ML
70.6 ID: $Id$
70.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
70.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
70.9 Copyright 1994 University of Cambridge
70.10
70.11 Datatype definition n-ary branching trees
70.12 @@ -17,18 +17,18 @@
70.13
70.14 datatype
70.15 "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
70.16 - monos "[[subset_refl, Pi_mono] MRS UN_mono]" (*MUST have this form*)
70.17 + monos "[[subset_refl, Pi_mono] MRS UN_mono]" (*MUST have this form*)
70.18 type_intrs "[nat_fun_univ RS subsetD]"
70.19 type_elims "[UN_E]"
70.20
70.21 datatype
70.22 "maptree(A)" = Sons ("a: A", "h: maptree(A) -||> maptree(A)")
70.23 - monos "[FiniteFun_mono1]" (*Use monotonicity in BOTH args*)
70.24 + monos "[FiniteFun_mono1]" (*Use monotonicity in BOTH args*)
70.25 type_intrs "[FiniteFun_univ1 RS subsetD]"
70.26
70.27 datatype
70.28 "maptree2(A,B)" = Sons2 ("a: A", "h: B -||> maptree2(A,B)")
70.29 - monos "[subset_refl RS FiniteFun_mono]"
70.30 + monos "[subset_refl RS FiniteFun_mono]"
70.31 type_intrs "[FiniteFun_in_univ']"
70.32
70.33 end
71.1 --- a/src/ZF/ex/Primrec.thy Mon Feb 05 21:33:14 1996 +0100
71.2 +++ b/src/ZF/ex/Primrec.thy Tue Feb 06 12:27:17 1996 +0100
71.3 @@ -1,6 +1,6 @@
71.4 -(* Title: ZF/ex/Primrec.thy
71.5 +(* Title: ZF/ex/Primrec.thy
71.6 ID: $Id$
71.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
71.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
71.9 Copyright 1994 University of Cambridge
71.10
71.11 Primitive Recursive Functions
71.12 @@ -22,8 +22,8 @@
71.13 PROJ :: i=>i
71.14 COMP :: [i,i]=>i
71.15 PREC :: [i,i]=>i
71.16 - ACK :: i=>i
71.17 - ack :: [i,i]=>i
71.18 + ACK :: i=>i
71.19 + ack :: [i,i]=>i
71.20
71.21 translations
71.22 "ack(x,y)" == "ACK(x) ` [y]"
71.23 @@ -57,8 +57,8 @@
71.24 PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
71.25 monos "[list_mono]"
71.26 con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
71.27 - type_intrs "nat_typechecks @ list.intrs @
71.28 - [lam_type, list_case_type, drop_type, map_type,
71.29 - apply_type, rec_type]"
71.30 + type_intrs "nat_typechecks @ list.intrs @
71.31 + [lam_type, list_case_type, drop_type, map_type,
71.32 + apply_type, rec_type]"
71.33
71.34 end
72.1 --- a/src/ZF/ex/PropLog.thy Mon Feb 05 21:33:14 1996 +0100
72.2 +++ b/src/ZF/ex/PropLog.thy Tue Feb 06 12:27:17 1996 +0100
72.3 @@ -1,6 +1,6 @@
72.4 -(* Title: ZF/ex/PropLog.thy
72.5 +(* Title: ZF/ex/PropLog.thy
72.6 ID: $Id$
72.7 - Author: Tobias Nipkow & Lawrence C Paulson
72.8 + Author: Tobias Nipkow & Lawrence C Paulson
72.9 Copyright 1993 University of Cambridge
72.10
72.11 Datatype definition of propositional logic formulae and inductive definition
72.12 @@ -15,13 +15,13 @@
72.13
72.14 datatype
72.15 "prop" = Fls
72.16 - | Var ("n: nat") ("#_" [100] 100)
72.17 - | "=>" ("p: prop", "q: prop") (infixr 90)
72.18 + | Var ("n: nat") ("#_" [100] 100)
72.19 + | "=>" ("p: prop", "q: prop") (infixr 90)
72.20
72.21 (** The proof system **)
72.22 consts
72.23 thms :: i => i
72.24 - "|-" :: [i,i] => o (infixl 50)
72.25 + "|-" :: [i,i] => o (infixl 50)
72.26
72.27 translations
72.28 "H |- p" == "p : thms(H)"
72.29 @@ -41,7 +41,7 @@
72.30 consts
72.31 prop_rec :: [i, i, i=>i, [i,i,i,i]=>i] => i
72.32 is_true :: [i,i] => o
72.33 - "|=" :: [i,i] => o (infixl 50)
72.34 + "|=" :: [i,i] => o (infixl 50)
72.35 hyps :: [i,i] => i
72.36
72.37 defs
73.1 --- a/src/ZF/ex/Ramsey.thy Mon Feb 05 21:33:14 1996 +0100
73.2 +++ b/src/ZF/ex/Ramsey.thy Tue Feb 06 12:27:17 1996 +0100
73.3 @@ -1,6 +1,6 @@
73.4 -(* Title: ZF/ex/ramsey.thy
73.5 +(* Title: ZF/ex/ramsey.thy
73.6 ID: $Id$
73.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
73.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
73.9 Copyright 1992 University of Cambridge
73.10
73.11 Ramsey's Theorem (finite exponent 2 version)
73.12 @@ -20,9 +20,9 @@
73.13
73.14 Ramsey = Arith +
73.15 consts
73.16 - Symmetric :: i=>o
73.17 - Atleast :: [i,i]=>o
73.18 - Clique,Indept,Ramsey :: [i,i,i]=>o
73.19 + Symmetric :: i=>o
73.20 + Atleast :: [i,i]=>o
73.21 + Clique,Indept,Ramsey :: [i,i,i]=>o
73.22
73.23 defs
73.24
74.1 --- a/src/ZF/ex/Rmap.thy Mon Feb 05 21:33:14 1996 +0100
74.2 +++ b/src/ZF/ex/Rmap.thy Tue Feb 06 12:27:17 1996 +0100
74.3 @@ -1,6 +1,6 @@
74.4 -(* Title: ZF/ex/Rmap
74.5 +(* Title: ZF/ex/Rmap
74.6 ID: $Id$
74.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
74.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
74.9 Copyright 1994 University of Cambridge
74.10
74.11 Inductive definition of an operator to "map" a relation over a list
75.1 --- a/src/ZF/ex/TF.thy Mon Feb 05 21:33:14 1996 +0100
75.2 +++ b/src/ZF/ex/TF.thy Tue Feb 06 12:27:17 1996 +0100
75.3 @@ -1,6 +1,6 @@
75.4 -(* Title: ZF/ex/TF.thy
75.5 +(* Title: ZF/ex/TF.thy
75.6 ID: $Id$
75.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
75.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
75.9 Copyright 1994 University of Cambridge
75.10
75.11 Trees & forests, a mutually recursive type definition.
75.12 @@ -24,14 +24,14 @@
75.13
75.14 defs
75.15 TF_rec_def
75.16 - "TF_rec(z,b,c,d) == Vrec(z,
75.17 - %z r. tree_forest_case(%x f. b(x, f, r`f),
75.18 - c,
75.19 - %t f. d(t, f, r`t, r`f), z))"
75.20 + "TF_rec(z,b,c,d) == Vrec(z,
75.21 + %z r. tree_forest_case(%x f. b(x, f, r`f),
75.22 + c,
75.23 + %t f. d(t, f, r`t, r`f), z))"
75.24
75.25 list_of_TF_def
75.26 "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [],
75.27 - %t f r1 r2. Cons(t, r2))"
75.28 + %t f r1 r2. Cons(t, r2))"
75.29
75.30 TF_of_list_def
75.31 "TF_of_list(f) == list_rec(f, Fnil, %t f r. Fcons(t,r))"
76.1 --- a/src/ZF/ex/Term.thy Mon Feb 05 21:33:14 1996 +0100
76.2 +++ b/src/ZF/ex/Term.thy Tue Feb 06 12:27:17 1996 +0100
76.3 @@ -1,6 +1,6 @@
76.4 -(* Title: ZF/ex/Term.thy
76.5 +(* Title: ZF/ex/Term.thy
76.6 ID: $Id$
76.7 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
76.8 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
76.9 Copyright 1994 University of Cambridge
76.10
76.11 Terms over an alphabet.
76.12 @@ -19,7 +19,7 @@
76.13
76.14 datatype
76.15 "term(A)" = Apply ("a: A", "l: list(term(A))")
76.16 - monos "[list_mono]"
76.17 + monos "[list_mono]"
76.18
76.19 type_elims "[make_elim (list_univ RS subsetD)]"
76.20 (*Or could have
76.21 @@ -31,12 +31,12 @@
76.22 "term_rec(t,d) ==
76.23 Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
76.24
76.25 - term_map_def "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
76.26 + term_map_def "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
76.27
76.28 - term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
76.29 + term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
76.30
76.31 - reflect_def "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
76.32 + reflect_def "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
76.33
76.34 - preorder_def "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
76.35 + preorder_def "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
76.36
76.37 end
77.1 --- a/src/ZF/ex/twos_compl.thy Mon Feb 05 21:33:14 1996 +0100
77.2 +++ b/src/ZF/ex/twos_compl.thy Tue Feb 06 12:27:17 1996 +0100
77.3 @@ -1,5 +1,5 @@
77.4 (* ID: $Id$
77.5 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
77.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
77.7 Copyright 1994 University of Cambridge
77.8 *)
77.9