--- a/src/CCL/ex/Flag.thy Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/Flag.thy Tue Mar 22 12:43:51 1994 +0100
@@ -29,9 +29,9 @@
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>>)))) \
+\ ccase(h, <red$lr,<lw,lb>>, \
+\ <lr,<white$lw,lb>>, \
+\ <lr,<lw,blue$lb>>)))) \
\ in flagx(l)"
Flag_def
--- a/src/CCL/ex/List.ML Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/List.ML Tue Mar 22 12:43:51 1994 +0100
@@ -17,15 +17,15 @@
["(f o g) = (%a.f(g(a)))",
"(f o g)(a) = f(g(a))",
"map(f,[]) = []",
- "map(f,x.xs) = f(x).map(f,xs)",
+ "map(f,x$xs) = f(x)$map(f,xs)",
"[] @ m = m",
- "x.xs @ m = x.(xs @ m)",
+ "x$xs @ m = x$(xs @ m)",
"filter(f,[]) = []",
- "filter(f,x.xs) = if f`x then x.filter(f,xs) else filter(f,xs)",
+ "filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)",
"flat([]) = []",
- "flat(x.xs) = x @ flat(xs)",
- "insert(f,a,[]) = a.[]",
- "insert(f,a,x.xs) = if f`a`x then a.x.xs else x.insert(f,a,xs)"];
+ "flat(x$xs) = x @ flat(xs)",
+ "insert(f,a,[]) = a$[]",
+ "insert(f,a,x$xs) = if f`a`x then a$x$xs else x$insert(f,a,xs)"];
val list_ss = nat_ss addsimps listBs;
@@ -36,7 +36,7 @@
by (ALLGOALS (asm_simp_tac list_ss));
val nmapBnil = result();
-val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x.xs) = f^n`x.map(f)^n`xs";
+val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)";
br (prem RS Nat_ind) 1;
by (ALLGOALS (asm_simp_tac list_ss));
val nmapBcons = result();
--- a/src/CCL/ex/List.thy Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/List.thy Tue Mar 22 12:43:51 1994 +0100
@@ -22,23 +22,23 @@
rules
- map_def "map(f,l) == lrec(l,[],%x xs g.f(x).g)"
+ map_def "map(f,l) == lrec(l,[],%x xs g.f(x)$g)"
comp_def "f o g == (%x.f(g(x)))"
- append_def "l @ m == lrec(l,m,%x xs g.x.g)"
+ append_def "l @ m == lrec(l,m,%x xs g.x$g)"
mem_def "a mem l == lrec(l,false,%h t g.if eq(a,h) then true else g)"
- filter_def "filter(f,l) == lrec(l,[],%x xs g.if f`x then x.g else g)"
+ filter_def "filter(f,l) == lrec(l,[],%x xs g.if f`x then x$g else g)"
flat_def "flat(l) == lrec(l,[],%h t g.h @ g)"
- insert_def "insert(f,a,l) == lrec(l,a.[],%h t g.if f`a`h then a.h.t else h.g)"
+ insert_def "insert(f,a,l) == lrec(l,a$[],%h t g.if f`a`h then a$h$t else h$g)"
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)) \
+\ 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 split(p,%x y.qsortx(x) @ h$qsortx(y))) \
\ in qsortx(l)"
end
--- a/src/CCL/ex/Stream.ML Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/Stream.ML Tue Mar 22 12:43:51 1994 +0100
@@ -82,21 +82,21 @@
(*** The equivalance of two versions of an iteration function ***)
(* *)
-(* fun iter1(f,a) = a.iter1(f,f(a)) *)
-(* fun iter2(f,a) = a.map(f,iter2(f,a)) *)
+(* fun iter1(f,a) = a$iter1(f,f(a)) *)
+(* fun iter2(f,a) = a$map(f,iter2(f,a)) *)
-goalw Stream.thy [iter1_def] "iter1(f,a) = a.iter1(f,f(a))";
+goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
br (letrecB RS trans) 1;
by (simp_tac term_ss 1);
val iter1B = result();
-goalw Stream.thy [iter2_def] "iter2(f,a) = a . map(f,iter2(f,a))";
+goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
br (letrecB RS trans) 1;
br refl 1;
val iter2B = result();
val [prem] =goal Stream.thy
- "n:Nat ==> map(f) ^ n ` iter2(f,a) = f ^ n ` a . map(f) ^ n ` map(f,iter2(f,a))";
+ "n:Nat ==> map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))";
br (iter2B RS ssubst) 1;back();back();
by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
val iter2Blemma = result();
--- a/src/CCL/ex/Stream.thy Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/Stream.thy Tue Mar 22 12:43:51 1994 +0100
@@ -14,7 +14,7 @@
rules
- iter1_def "iter1(f,a) == letrec iter x be x.iter(f(x)) in iter(a)"
- iter2_def "iter2(f,a) == letrec iter x be x.map(f,iter(x)) in iter(a)"
+ iter1_def "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
+ iter2_def "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
end
--- a/src/CCL/ex/flag.thy Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/flag.thy Tue Mar 22 12:43:51 1994 +0100
@@ -29,9 +29,9 @@
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>>)))) \
+\ ccase(h, <red$lr,<lw,lb>>, \
+\ <lr,<white$lw,lb>>, \
+\ <lr,<lw,blue$lb>>)))) \
\ in flagx(l)"
Flag_def
--- a/src/CCL/ex/list.ML Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/list.ML Tue Mar 22 12:43:51 1994 +0100
@@ -17,15 +17,15 @@
["(f o g) = (%a.f(g(a)))",
"(f o g)(a) = f(g(a))",
"map(f,[]) = []",
- "map(f,x.xs) = f(x).map(f,xs)",
+ "map(f,x$xs) = f(x)$map(f,xs)",
"[] @ m = m",
- "x.xs @ m = x.(xs @ m)",
+ "x$xs @ m = x$(xs @ m)",
"filter(f,[]) = []",
- "filter(f,x.xs) = if f`x then x.filter(f,xs) else filter(f,xs)",
+ "filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)",
"flat([]) = []",
- "flat(x.xs) = x @ flat(xs)",
- "insert(f,a,[]) = a.[]",
- "insert(f,a,x.xs) = if f`a`x then a.x.xs else x.insert(f,a,xs)"];
+ "flat(x$xs) = x @ flat(xs)",
+ "insert(f,a,[]) = a$[]",
+ "insert(f,a,x$xs) = if f`a`x then a$x$xs else x$insert(f,a,xs)"];
val list_ss = nat_ss addsimps listBs;
@@ -36,7 +36,7 @@
by (ALLGOALS (asm_simp_tac list_ss));
val nmapBnil = result();
-val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x.xs) = f^n`x.map(f)^n`xs";
+val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)";
br (prem RS Nat_ind) 1;
by (ALLGOALS (asm_simp_tac list_ss));
val nmapBcons = result();
--- a/src/CCL/ex/list.thy Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/list.thy Tue Mar 22 12:43:51 1994 +0100
@@ -22,23 +22,23 @@
rules
- map_def "map(f,l) == lrec(l,[],%x xs g.f(x).g)"
+ map_def "map(f,l) == lrec(l,[],%x xs g.f(x)$g)"
comp_def "f o g == (%x.f(g(x)))"
- append_def "l @ m == lrec(l,m,%x xs g.x.g)"
+ append_def "l @ m == lrec(l,m,%x xs g.x$g)"
mem_def "a mem l == lrec(l,false,%h t g.if eq(a,h) then true else g)"
- filter_def "filter(f,l) == lrec(l,[],%x xs g.if f`x then x.g else g)"
+ filter_def "filter(f,l) == lrec(l,[],%x xs g.if f`x then x$g else g)"
flat_def "flat(l) == lrec(l,[],%h t g.h @ g)"
- insert_def "insert(f,a,l) == lrec(l,a.[],%h t g.if f`a`h then a.h.t else h.g)"
+ insert_def "insert(f,a,l) == lrec(l,a$[],%h t g.if f`a`h then a$h$t else h$g)"
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)) \
+\ 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 split(p,%x y.qsortx(x) @ h$qsortx(y))) \
\ in qsortx(l)"
end
--- a/src/CCL/ex/stream.ML Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/stream.ML Tue Mar 22 12:43:51 1994 +0100
@@ -82,21 +82,21 @@
(*** The equivalance of two versions of an iteration function ***)
(* *)
-(* fun iter1(f,a) = a.iter1(f,f(a)) *)
-(* fun iter2(f,a) = a.map(f,iter2(f,a)) *)
+(* fun iter1(f,a) = a$iter1(f,f(a)) *)
+(* fun iter2(f,a) = a$map(f,iter2(f,a)) *)
-goalw Stream.thy [iter1_def] "iter1(f,a) = a.iter1(f,f(a))";
+goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
br (letrecB RS trans) 1;
by (simp_tac term_ss 1);
val iter1B = result();
-goalw Stream.thy [iter2_def] "iter2(f,a) = a . map(f,iter2(f,a))";
+goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
br (letrecB RS trans) 1;
br refl 1;
val iter2B = result();
val [prem] =goal Stream.thy
- "n:Nat ==> map(f) ^ n ` iter2(f,a) = f ^ n ` a . map(f) ^ n ` map(f,iter2(f,a))";
+ "n:Nat ==> map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))";
br (iter2B RS ssubst) 1;back();back();
by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
val iter2Blemma = result();
--- a/src/CCL/ex/stream.thy Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/stream.thy Tue Mar 22 12:43:51 1994 +0100
@@ -14,7 +14,7 @@
rules
- iter1_def "iter1(f,a) == letrec iter x be x.iter(f(x)) in iter(a)"
- iter2_def "iter2(f,a) == letrec iter x be x.map(f,iter(x)) in iter(a)"
+ iter1_def "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
+ iter2_def "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
end