# HG changeset patch # User clasohm # Date 823606037 -3600 # Node ID 2b8c2a7547ab977ded189ba455b90c70463d19b8 # Parent 4c51ab632cda581e4c3163748c98159281779e80 expanded tabs diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/AC.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/AC/AC16_WO4.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/AC/AC18_AC19.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/AC/AC_Equiv.thy --- 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 (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 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` : bij(B1,B2))" + (EX f. ALL B1:A. ALL B2:A. f` : 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/AC/DC.thy --- 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. : R)) - --> (EX f:a->X. ALL b : R)" + (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. : R)) + --> (EX f:a->X. ALL 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. :R)" + --> (EX f:nat->domain(R). ALL n:nat. :R)" ff_def "ff(b, X, Q, R) == transrec(b, %c r. - THE x. first(x, {x:X. : R}, Q))" + THE x. first(x, {x:X. : R}, Q))" end diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/AC/HH.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/AC/Hartog.thy --- 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. *) diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/AC/OrdQuant.thy --- 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. *) diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/AC/Transrec2.thy --- 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 WO1". @@ -20,18 +20,18 @@ defs NN_def "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a & - (UN b : R)" + == u:X & (ALL v:X. v~=u --> : R)" end diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/AC/recfunAC16.thy --- 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 (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 (ALL t:r. ~ fa`b <= t))))}))" end diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Arith.thy --- 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))" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Bool.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Cardinal.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/CardinalArith.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Cardinal_AC.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Coind/BCR.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Coind/Dynamic.thy --- 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 *) diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Coind/ECR.thy --- 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) |] ==> :HasTyRel" htr_closI "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; - :ElabRel; - ve_dom(ve) = te_dom(te); - {.y:ve_dom(ve)}:Pow(HasTyRel) + :ElabRel; + ve_dom(ve) = te_dom(te); + {.y:ve_dom(ve)}:Pow(HasTyRel) |] ==> :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). :HasTyRel)" end diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Coind/Language.thy --- 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") diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Coind/Map.thy --- 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 *) diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Coind/Static.thy --- 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 *) diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Coind/Types.thy --- 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") diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Coind/Values.thy --- 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 *) diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Epsilon.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/EquivClass.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Finite.thy --- 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(,h) : A -||> B" + |] ==> cons(,h) : A -||> B" type_intrs "Fin.intrs" end diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Fixedpt.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/IMP/Com.thy --- 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 " -a-> n" == " : evala" inductive domains "evala" <= "aexp * (loc -> nat) * nat" intrs N "[| n:nat ; sigma:loc->nat |] ==> -a-> n" - X "[| x:loc; sigma:loc->nat |] ==> -a-> sigma`x" + X "[| x:loc; sigma:loc->nat |] ==> -a-> sigma`x" Op1 "[| -a-> n; f: nat -> nat |] ==> -a-> f`n" Op2 "[| -a-> n0; -a-> n1; f: (nat*nat) -> nat |] ==> -a-> f`" @@ -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 " -b-> b" == " : evalb" @@ -63,15 +63,15 @@ tru "[| sigma:loc -> nat |] ==> -b-> 1" fls "[| sigma:loc -> nat |] ==> -b-> 0" ROp "[| -a-> n0; -a-> n1; f: (nat*nat)->bool |] - ==> -b-> f` " + ==> -b-> f` " noti "[| -b-> w |] ==> -b-> not(w)" andi "[| -b-> w0; -b-> w1 |] ==> -b-> (w0 and w1)" ori "[| -b-> w0; -b-> w1 |] - ==> -b-> (w0 or w1)" + ==> -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 " -c-> 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 @@ -c-> sigma1" ifc1 "[| b:bexp; c1:com; sigma:loc->nat; - -b-> 1; -c-> sigma1 |] ==> + -b-> 1; -c-> sigma1 |] ==> -c-> sigma1" ifc0 "[| b:bexp; c0:com; sigma:loc->nat; - -b-> 0; -c-> sigma1 |] ==> + -b-> 0; -c-> sigma1 |] ==> -c-> sigma1" while0 "[| c: com; -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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/IMP/Denotation.thy --- 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`)" +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`)" - B_true_def "B(true) == (%sigma. 1)" - B_false_def "B(false) == (%sigma. 0)" - B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`)" + B_true_def "B(true) == (%sigma. 1)" + B_false_def "B(false) == (%sigma. 0)" + B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`)" - 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/IMP/Equiv.thy --- 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 *) diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Let.thy --- 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) diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/List.thy --- 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))" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Nat.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Order.thy --- 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)" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/OrderArith.thy --- 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 = ) | - (EX x' x. z = & :r) | + (EX x y. z = ) | + (EX x' x. z = & :r) | (EX y' y. z = & :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 = <, > & + EX x' y' x y. z = <, > & (: r | (x'=x & : s))}" (*inverse image of a relation*) diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/OrderType.thy --- 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. diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Ordinal.thy --- 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 }" - 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 }" + Transset_def "Transset(i) == ALL x:i. x<=i" + Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))" lt_def "i succ(y)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= & :s & :r}" + comp_def "r O s == {xz : domain(s)*range(r) . + EX x y z. xz= & :s & :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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/QPair.thy --- 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)" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/QUniv.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Rel.thy --- 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. : r)" @@ -25,7 +25,7 @@ trans_def "trans(r) == ALL x y z. : r --> : r --> : 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. : r --> : r --> : r" equiv_def "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Resid/Confluence.thy --- 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. :R --> (ALL z.:R --> - (EX u.:R & :R))" + ALL x y. :R --> (ALL z.:R --> + (EX u.:R & :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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Resid/Conversion.thy --- 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" == ":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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Resid/Cube.thy --- 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 *) diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Resid/Redex.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Resid/Reduction.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Resid/Residuals.thy --- 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)" == ":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)" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Resid/SubUnion.thy --- 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" == ":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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Resid/Substitution.thy --- 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(ii - 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Sum.thy --- 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) == (%. 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Trancl.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Univ.thy --- 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)" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/WF.thy --- 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. :r --> ~ y:Z)" + wf_def "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. :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})))" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ZF.thy --- 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=}" range_def "range(r) == domain(converse(r))" field_def "field(r) == domain(r) Un range(r)" - function_def "function(r) == ALL x y. :r --> - (ALL y'. :r --> y=y')" + function_def "function(r) == ALL x y. :r --> + (ALL y'. :r --> y=y')" image_def "r `` A == {y : range(r) . EX x:A. : r}" vimage_def "r -`` A == converse(r)``A" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/Zorn.thy --- 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]" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Acc.thy --- 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) diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/BT.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Brouwer.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/CoUnit.thy --- 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! diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Comb.thy --- 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" == " : 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" == " : parcontract" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Data.thy --- 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. diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Enum.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Integ.thy --- 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#+y2 = x2#+y1}" integ_def "integ == (nat*nat)/intrel" - znat_def "$# m == intrel `` {}" + znat_def "$# m == intrel `` {}" - zminus_def "$~ Z == UN :Z. intrel``{}" + zminus_def "$~ Z == UN :Z. intrel``{}" znegative_def - "znegative(Z) == EX x y. x:Z" + "znegative(Z) == EX x y. x:Z" zmagnitude_def - "zmagnitude(Z) == UN :Z. (y#-x) #+ (x#-y)" + "zmagnitude(Z) == UN :Z. (y#-x) #+ (x#-y)" (*Cannot use UN 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``{}" 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/LList.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Limit.thy --- 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. diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/ListN.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Ntree.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Primrec.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/PropLog.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Ramsey.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Rmap.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/TF.thy --- 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))" diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/Term.thy --- 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 diff -r 4c51ab632cda -r 2b8c2a7547ab src/ZF/ex/twos_compl.thy --- 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 *)