src/CTT/CTT.thy
changeset 3837 d7f033c74b38
parent 1149 5750eba8820d
child 10467 e6e7205e9e91
     1.1 --- a/src/CTT/CTT.thy	Fri Oct 10 16:29:41 1997 +0200
     1.2 +++ b/src/CTT/CTT.thy	Fri Oct 10 17:10:12 1997 +0200
     1.3 @@ -113,21 +113,21 @@
     1.4  
     1.5    NE
     1.6     "[| p: N;  a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] 
     1.7 -   ==> rec(p, a, %u v.b(u,v)) : C(p)"
     1.8 +   ==> rec(p, a, %u v. b(u,v)) : C(p)"
     1.9  
    1.10    NEL
    1.11     "[| p = q : N;  a = c : C(0);  
    1.12        !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] 
    1.13 -   ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)"
    1.14 +   ==> rec(p, a, %u v. b(u,v)) = rec(q,c,d) : C(p)"
    1.15  
    1.16    NC0
    1.17     "[| a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] 
    1.18 -   ==> rec(0, a, %u v.b(u,v)) = a : C(0)"
    1.19 +   ==> rec(0, a, %u v. b(u,v)) = a : C(0)"
    1.20  
    1.21    NC_succ
    1.22     "[| p: N;  a: C(0);  
    1.23         !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==>  
    1.24 -   rec(succ(p), a, %u v.b(u,v)) = b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))"
    1.25 +   rec(succ(p), a, %u v. b(u,v)) = b(p, rec(p, a, %u v. b(u,v))) : C(succ(p))"
    1.26  
    1.27    (*The fourth Peano axiom.  See page 91 of Martin-Lof's book*)
    1.28    zero_ne_succ
    1.29 @@ -136,54 +136,54 @@
    1.30  
    1.31    (*The Product of a family of types*)
    1.32  
    1.33 -  ProdF  "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type"
    1.34 +  ProdF  "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type"
    1.35  
    1.36    ProdFL
    1.37     "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> 
    1.38 -   PROD x:A.B(x) = PROD x:C.D(x)"
    1.39 +   PROD x:A. B(x) = PROD x:C. D(x)"
    1.40  
    1.41    ProdI
    1.42 -   "[| A type;  !!x. x:A ==> b(x):B(x)|] ==> lam x.b(x) : PROD x:A.B(x)"
    1.43 +   "[| A type;  !!x. x:A ==> b(x):B(x)|] ==> lam x. b(x) : PROD x:A. B(x)"
    1.44  
    1.45    ProdIL
    1.46     "[| A type;  !!x. x:A ==> b(x) = c(x) : B(x)|] ==> 
    1.47 -   lam x.b(x) = lam x.c(x) : PROD x:A.B(x)"
    1.48 +   lam x. b(x) = lam x. c(x) : PROD x:A. B(x)"
    1.49  
    1.50 -  ProdE  "[| p : PROD x:A.B(x);  a : A |] ==> p`a : B(a)"
    1.51 -  ProdEL "[| p=q: PROD x:A.B(x);  a=b : A |] ==> p`a = q`b : B(a)"
    1.52 +  ProdE  "[| p : PROD x:A. B(x);  a : A |] ==> p`a : B(a)"
    1.53 +  ProdEL "[| p=q: PROD x:A. B(x);  a=b : A |] ==> p`a = q`b : B(a)"
    1.54  
    1.55    ProdC
    1.56     "[| a : A;  !!x. x:A ==> b(x) : B(x)|] ==> 
    1.57 -   (lam x.b(x)) ` a = b(a) : B(a)"
    1.58 +   (lam x. b(x)) ` a = b(a) : B(a)"
    1.59  
    1.60    ProdC2
    1.61 -   "p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)"
    1.62 +   "p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)"
    1.63  
    1.64  
    1.65    (*The Sum of a family of types*)
    1.66  
    1.67 -  SumF  "[| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A.B(x) type"
    1.68 +  SumF  "[| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type"
    1.69    SumFL
    1.70 -    "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A.B(x) = SUM x:C.D(x)"
    1.71 +    "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A. B(x) = SUM x:C. D(x)"
    1.72  
    1.73 -  SumI  "[| a : A;  b : B(a) |] ==> <a,b> : SUM x:A.B(x)"
    1.74 -  SumIL "[| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A.B(x)"
    1.75 +  SumI  "[| a : A;  b : B(a) |] ==> <a,b> : SUM x:A. B(x)"
    1.76 +  SumIL "[| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)"
    1.77  
    1.78    SumE
    1.79 -    "[| p: SUM x:A.B(x);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
    1.80 -    ==> split(p, %x y.c(x,y)) : C(p)"
    1.81 +    "[| p: SUM x:A. B(x);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
    1.82 +    ==> split(p, %x y. c(x,y)) : C(p)"
    1.83  
    1.84    SumEL
    1.85 -    "[| p=q : SUM x:A.B(x); 
    1.86 +    "[| p=q : SUM x:A. B(x); 
    1.87         !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|] 
    1.88 -    ==> split(p, %x y.c(x,y)) = split(q, % x y.d(x,y)) : C(p)"
    1.89 +    ==> split(p, %x y. c(x,y)) = split(q, % x y. d(x,y)) : C(p)"
    1.90  
    1.91    SumC
    1.92      "[| a: A;  b: B(a);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
    1.93 -    ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)"
    1.94 +    ==> split(<a,b>, %x y. c(x,y)) = c(a,b) : C(<a,b>)"
    1.95  
    1.96 -  fst_def   "fst(a) == split(a, %x y.x)"
    1.97 -  snd_def   "snd(a) == split(a, %x y.y)"
    1.98 +  fst_def   "fst(a) == split(a, %x y. x)"
    1.99 +  snd_def   "snd(a) == split(a, %x y. y)"
   1.100  
   1.101  
   1.102    (*The sum of two types*)
   1.103 @@ -200,22 +200,22 @@
   1.104    PlusE
   1.105      "[| p: A+B;  !!x. x:A ==> c(x): C(inl(x));  
   1.106                  !!y. y:B ==> d(y): C(inr(y)) |] 
   1.107 -    ==> when(p, %x.c(x), %y.d(y)) : C(p)"
   1.108 +    ==> when(p, %x. c(x), %y. d(y)) : C(p)"
   1.109  
   1.110    PlusEL
   1.111      "[| p = q : A+B;  !!x. x: A ==> c(x) = e(x) : C(inl(x));   
   1.112                       !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] 
   1.113 -    ==> when(p, %x.c(x), %y.d(y)) = when(q, %x.e(x), %y.f(y)) : C(p)"
   1.114 +    ==> when(p, %x. c(x), %y. d(y)) = when(q, %x. e(x), %y. f(y)) : C(p)"
   1.115  
   1.116    PlusC_inl
   1.117      "[| a: A;  !!x. x:A ==> c(x): C(inl(x));  
   1.118                !!y. y:B ==> d(y): C(inr(y)) |] 
   1.119 -    ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))"
   1.120 +    ==> when(inl(a), %x. c(x), %y. d(y)) = c(a) : C(inl(a))"
   1.121  
   1.122    PlusC_inr
   1.123      "[| b: B;  !!x. x:A ==> c(x): C(inl(x));  
   1.124                !!y. y:B ==> d(y): C(inr(y)) |] 
   1.125 -    ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))"
   1.126 +    ==> when(inr(b), %x. c(x), %y. d(y)) = d(b) : C(inr(b))"
   1.127  
   1.128  
   1.129    (*The type Eq*)