--- a/src/CCL/CCL.thy Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/CCL.thy Wed Jun 21 15:01:07 1995 +0200
@@ -64,11 +64,11 @@
(*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***)
- canonical "[| t ---> c; c==true ==> u--->v; \
-\ c==false ==> u--->v; \
-\ !!a b.c==<a,b> ==> u--->v; \
-\ !!f.c==lam x.f(x) ==> u--->v |] ==> \
-\ u--->v"
+ canonical "[| t ---> c; c==true ==> u--->v;
+ c==false ==> u--->v;
+ !!a b.c==<a,b> ==> u--->v;
+ !!f.c==lam x.f(x) ==> u--->v |] ==>
+ u--->v"
(* Should be derivable - but probably a bitch! *)
substitute "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')"
@@ -86,9 +86,9 @@
(* behavioural equivalence (ie the relations PO and EQ defined below). *)
SIM_def
- "SIM(t,t',R) == (t=true & t'=true) | (t=false & t'=false) | \
-\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \
-\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))"
+ "SIM(t,t',R) == (t=true & t'=true) | (t=false & t'=false) |
+ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) |
+ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))"
POgen_def "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
EQgen_def "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
--- a/src/CCL/Hered.thy Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/Hered.thy Wed Jun 21 15:01:07 1995 +0200
@@ -23,8 +23,8 @@
(*** Definitions of Hereditary Termination ***)
HTTgen_def
- "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b> & a : R & b : R) | \
-\ (EX f. t=lam x.f(x) & (ALL x.f(x) : R))}"
+ "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b> & a : R & b : R) |
+ (EX f. t=lam x.f(x) & (ALL x.f(x) : R))}"
HTT_def "HTT == gfp(HTTgen)"
end
--- a/src/CCL/Term.thy Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/Term.thy Wed Jun 21 15:01:07 1995 +0200
@@ -75,13 +75,13 @@
letrec_def
"letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)"
- letrec2_def "letrec g x y be h(x,y,g) in f(g)== \
-\ letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) \
-\ in f(%x y.g'(<x,y>))"
+ letrec2_def "letrec g x y be h(x,y,g) in f(g)==
+ letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>)))
+ in f(%x y.g'(<x,y>))"
- letrec3_def "letrec g x y z be h(x,y,z,g) in f(g) == \
-\ letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) \
-\ in f(%x y z.g'(<x,<y,z>>))"
+ letrec3_def "letrec g x y z be h(x,y,z,g) in f(g) ==
+ letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>))))
+ in f(%x y z.g'(<x,<y,z>>))"
napply_def "f ^n` a == nrec(n,a,%x g.f(g))"
--- a/src/CCL/ex/Flag.thy Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/ex/Flag.thy Wed Jun 21 15:01:07 1995 +0200
@@ -26,21 +26,21 @@
ccase_def "ccase(c,r,w,b) == when(c,%x.r,%wb.when(wb,%x.w,%x.b))"
- flag_def "flag == lam l.letrec \
-\ flagx l be lcase(l,<[],<[],[]>>, \
-\ %h t. split(flagx(t),%lr p.split(p,%lw lb. \
-\ ccase(h, <red$lr,<lw,lb>>, \
-\ <lr,<white$lw,lb>>, \
-\ <lr,<lw,blue$lb>>)))) \
-\ in flagx(l)"
+ flag_def "flag == lam l.letrec
+ flagx l be lcase(l,<[],<[],[]>>,
+ %h t. split(flagx(t),%lr p.split(p,%lw lb.
+ ccase(h, <red$lr,<lw,lb>>,
+ <lr,<white$lw,lb>>,
+ <lr,<lw,blue$lb>>))))
+ in flagx(l)"
Flag_def
- "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). \
-\ x = <lr,<lw,lb>> --> \
-\ (ALL c:Colour.(c mem lr = true --> c=red) & \
-\ (c mem lw = true --> c=white) & \
-\ (c mem lb = true --> c=blue)) & \
-\ Perm(l,lr @ lw @ lb)"
+ "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour).
+ x = <lr,<lw,lb>> -->
+ (ALL c:Colour.(c mem lr = true --> c=red) &
+ (c mem lw = true --> c=white) &
+ (c mem lb = true --> c=blue)) &
+ Perm(l,lr @ lw @ lb)"
end
--- a/src/CCL/ex/List.thy Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/ex/List.thy Wed Jun 21 15:01:07 1995 +0200
@@ -33,12 +33,12 @@
isort_def "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))"
partition_def
- "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.\
-\ if f`x then part(xs,x$a,b) else part(xs,a,x$b)) \
-\ in part(l,[],[])"
- qsort_def "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. \
-\ let p be partition(f`h,t) \
-\ in split(p,%x y.qsortx(x) @ h$qsortx(y))) \
-\ in qsortx(l)"
+ "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
+ if f`x then part(xs,x$a,b) else part(xs,a,x$b))
+ in part(l,[],[])"
+ qsort_def "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
+ let p be partition(f`h,t)
+ in split(p,%x y.qsortx(x) @ h$qsortx(y)))
+ in qsortx(l)"
end
--- a/src/CCL/ex/Nat.thy Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/ex/Nat.thy Wed Jun 21 15:01:07 1995 +0200
@@ -21,18 +21,18 @@
add_def "a #+ b == nrec(a,b,%x g.succ(g))"
mult_def "a #* b == nrec(a,zero,%x g.b #+ g)"
- sub_def "a #- b == letrec sub x y be ncase(y,x,%yy.ncase(x,zero,%xx.sub(xx,yy))) \
-\ in sub(a,b)"
- le_def "a #<= b == letrec le x y be ncase(x,true,%xx.ncase(y,false,%yy.le(xx,yy))) \
-\ in le(a,b)"
+ sub_def "a #- b == letrec sub x y be ncase(y,x,%yy.ncase(x,zero,%xx.sub(xx,yy)))
+ in sub(a,b)"
+ le_def "a #<= b == letrec le x y be ncase(x,true,%xx.ncase(y,false,%yy.le(xx,yy)))
+ in le(a,b)"
lt_def "a #< b == not(b #<= a)"
- div_def "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y)) \
-\ in div(a,b)"
+ div_def "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y))
+ in div(a,b)"
ack_def
- "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x. \
-\ ncase(m,ack(x,succ(zero)),%y.ack(x,ack(succ(x),y))))\
-\ in ack(a,b)"
+ "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x.
+ ncase(m,ack(x,succ(zero)),%y.ack(x,ack(succ(x),y))))
+ in ack(a,b)"
end
--- a/src/CTT/CTT.thy Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CTT/CTT.thy Wed Jun 21 15:01:07 1995 +0200
@@ -112,22 +112,22 @@
NI_succL "a = b : N ==> succ(a) = succ(b) : N"
NE
- "[| p: N; a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] \
-\ ==> rec(p, a, %u v.b(u,v)) : C(p)"
+ "[| p: N; a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |]
+ ==> rec(p, a, %u v.b(u,v)) : C(p)"
NEL
- "[| p = q : N; a = c : C(0); \
-\ !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] \
-\ ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)"
+ "[| p = q : N; a = c : C(0);
+ !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |]
+ ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)"
NC0
- "[| a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] \
-\ ==> rec(0, a, %u v.b(u,v)) = a : C(0)"
+ "[| a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |]
+ ==> rec(0, a, %u v.b(u,v)) = a : C(0)"
NC_succ
- "[| p: N; a: C(0); \
-\ !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==> \
-\ rec(succ(p), a, %u v.b(u,v)) = b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))"
+ "[| p: N; a: C(0);
+ !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==>
+ rec(succ(p), a, %u v.b(u,v)) = b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))"
(*The fourth Peano axiom. See page 91 of Martin-Lof's book*)
zero_ne_succ
@@ -139,22 +139,22 @@
ProdF "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type"
ProdFL
- "[| A = C; !!x. x:A ==> B(x) = D(x) |] ==> \
-\ PROD x:A.B(x) = PROD x:C.D(x)"
+ "[| A = C; !!x. x:A ==> B(x) = D(x) |] ==>
+ PROD x:A.B(x) = PROD x:C.D(x)"
ProdI
"[| A type; !!x. x:A ==> b(x):B(x)|] ==> lam x.b(x) : PROD x:A.B(x)"
ProdIL
- "[| A type; !!x. x:A ==> b(x) = c(x) : B(x)|] ==> \
-\ lam x.b(x) = lam x.c(x) : PROD x:A.B(x)"
+ "[| A type; !!x. x:A ==> b(x) = c(x) : B(x)|] ==>
+ lam x.b(x) = lam x.c(x) : PROD x:A.B(x)"
ProdE "[| p : PROD x:A.B(x); a : A |] ==> p`a : B(a)"
ProdEL "[| p=q: PROD x:A.B(x); a=b : A |] ==> p`a = q`b : B(a)"
ProdC
- "[| a : A; !!x. x:A ==> b(x) : B(x)|] ==> \
-\ (lam x.b(x)) ` a = b(a) : B(a)"
+ "[| a : A; !!x. x:A ==> b(x) : B(x)|] ==>
+ (lam x.b(x)) ` a = b(a) : B(a)"
ProdC2
"p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)"
@@ -170,17 +170,17 @@
SumIL "[| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A.B(x)"
SumE
- "[| p: SUM x:A.B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] \
-\ ==> split(p, %x y.c(x,y)) : C(p)"
+ "[| p: SUM x:A.B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |]
+ ==> split(p, %x y.c(x,y)) : C(p)"
SumEL
- "[| p=q : SUM x:A.B(x); \
-\ !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|] \
-\ ==> split(p, %x y.c(x,y)) = split(q, % x y.d(x,y)) : C(p)"
+ "[| p=q : SUM x:A.B(x);
+ !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|]
+ ==> split(p, %x y.c(x,y)) = split(q, % x y.d(x,y)) : C(p)"
SumC
- "[| a: A; b: B(a); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] \
-\ ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)"
+ "[| a: A; b: B(a); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |]
+ ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)"
fst_def "fst(a) == split(a, %x y.x)"
snd_def "snd(a) == split(a, %x y.y)"
@@ -198,24 +198,24 @@
PlusI_inrL "[| A type; b = d : B |] ==> inr(b) = inr(d) : A+B"
PlusE
- "[| p: A+B; !!x. x:A ==> c(x): C(inl(x)); \
-\ !!y. y:B ==> d(y): C(inr(y)) |] \
-\ ==> when(p, %x.c(x), %y.d(y)) : C(p)"
+ "[| p: A+B; !!x. x:A ==> c(x): C(inl(x));
+ !!y. y:B ==> d(y): C(inr(y)) |]
+ ==> when(p, %x.c(x), %y.d(y)) : C(p)"
PlusEL
- "[| p = q : A+B; !!x. x: A ==> c(x) = e(x) : C(inl(x)); \
-\ !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] \
-\ ==> when(p, %x.c(x), %y.d(y)) = when(q, %x.e(x), %y.f(y)) : C(p)"
+ "[| p = q : A+B; !!x. x: A ==> c(x) = e(x) : C(inl(x));
+ !!y. y: B ==> d(y) = f(y) : C(inr(y)) |]
+ ==> when(p, %x.c(x), %y.d(y)) = when(q, %x.e(x), %y.f(y)) : C(p)"
PlusC_inl
- "[| a: A; !!x. x:A ==> c(x): C(inl(x)); \
-\ !!y. y:B ==> d(y): C(inr(y)) |] \
-\ ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))"
+ "[| a: A; !!x. x:A ==> c(x): C(inl(x));
+ !!y. y:B ==> d(y): C(inr(y)) |]
+ ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))"
PlusC_inr
- "[| b: B; !!x. x:A ==> c(x): C(inl(x)); \
-\ !!y. y:B ==> d(y): C(inr(y)) |] \
-\ ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))"
+ "[| b: B; !!x. x:A ==> c(x): C(inl(x));
+ !!y. y:B ==> d(y): C(inr(y)) |]
+ ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))"
(*The type Eq*)
--- a/src/Cube/Cube.thy Wed Jun 21 11:35:10 1995 +0200
+++ b/src/Cube/Cube.thy Wed Jun 21 15:01:07 1995 +0200
@@ -46,8 +46,8 @@
pi_ss "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
- lam_ss "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
-\ ==> Abs(A, f) : Prod(A, B)"
+ lam_ss "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
+ ==> Abs(A, f) : Prod(A, B)"
beta "Abs(A, f)^a == f(a)"
--- a/src/FOLP/IFOLP.thy Wed Jun 21 11:35:10 1995 +0200
+++ b/src/FOLP/IFOLP.thy Wed Jun 21 15:01:07 1995 +0200
@@ -84,8 +84,8 @@
disjI1 "a:P ==> inl(a):P|Q"
disjI2 "b:Q ==> inr(b):P|Q"
-disjE "[| a:P|Q; !!x.x:P ==> f(x):R; !!x.x:Q ==> g(x):R \
-\ |] ==> when(a,f,g):R"
+disjE "[| a:P|Q; !!x.x:P ==> f(x):R; !!x.x:Q ==> g(x):R
+ |] ==> when(a,f,g):R"
(* Implication *)
--- a/src/FOLP/ex/Nat.thy Wed Jun 21 11:35:10 1995 +0200
+++ b/src/FOLP/ex/Nat.thy Wed Jun 21 15:01:07 1995 +0200
@@ -22,8 +22,8 @@
rec0, recSuc :: "p"
rules
- induct "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x)) \
-\ |] ==> nrec(n,b,c):P(n)"
+ induct "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
+ |] ==> nrec(n,b,c):P(n)"
Suc_inject "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
Suc_neq_0 "p:Suc(m)=0 ==> nneq(p) : R"