--- a/src/CCL/Hered.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Hered.ML Tue Mar 22 12:42:56 1994 +0100
@@ -70,7 +70,7 @@
"zero : HTT",
"succ(n) : HTT <-> n : HTT",
"[] : HTT",
- "x.xs : HTT <-> x : HTT & xs : HTT"];
+ "x$xs : HTT <-> x : HTT & xs : HTT"];
end;
val HTT_Is = HTT_rews @ (HTT_rews RL [iffD2]);
@@ -108,7 +108,7 @@
\ succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>\
-\ h.t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
+\ h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
(*** Formation Rules for Types ***)
--- a/src/CCL/Term.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Term.ML Tue Mar 22 12:42:56 1994 +0100
@@ -90,10 +90,10 @@
val nrecBbot = mk_beta_rl "nrec(bot,t,u) = bot";
val lcaseBnil = mk_beta_rl "lcase([],t,u) = t";
-val lcaseBcons = mk_beta_rl "lcase(x.xs,t,u) = u(x,xs)";
+val lcaseBcons = mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)";
val lcaseBbot = mk_beta_rl "lcase(bot,t,u) = bot";
val lrecBnil = mk_beta_rl "lrec([],t,u) = t";
-val lrecBcons = mk_beta_rl "lrec(x.xs,t,u) = u(x,xs,lrec(xs,t,u))";
+val lrecBcons = mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))";
val lrecBbot = mk_beta_rl "lrec(bot,t,u) = bot";
val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def])
@@ -120,12 +120,12 @@
["(inl(a) = inl(a')) <-> (a=a')",
"(inr(a) = inr(a')) <-> (a=a')",
"(succ(a) = succ(a')) <-> (a=a')",
- "(a.b = a'.b') <-> (a=a' & b=b')"];
+ "(a$b = a'$b') <-> (a=a' & b=b')"];
(*** Constructors are distinct ***)
val term_dstncts = mkall_dstnct_thms Term.thy data_defs (ccl_injs @ term_injs)
- [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op ."]];
+ [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op $"]];
(*** Rules for pre-order [= ***)
@@ -136,7 +136,7 @@
val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
"inr(b) [= inr(b') <-> b [= b'",
"succ(n) [= succ(n') <-> n [= n'",
- "x.xs [= x'.xs' <-> x [= x' & xs [= xs'"];
+ "x$xs [= x'$xs' <-> x [= x' & xs [= xs'"];
end;
(*** Rewriting and Proving ***)
--- a/src/CCL/Term.thy Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Term.thy Tue Mar 22 12:42:56 1994 +0100
@@ -28,7 +28,7 @@
nrec :: "[i,i,[i,i]=>i]=>i"
nil :: "i" ("([])")
- "." :: "[i,i]=>i" (infixr 80)
+ "$" :: "[i,i]=>i" (infixr 80)
lcase :: "[i,i,[i,i]=>i]=>i"
lrec :: "[i,i,[i,i,i]=>i]=>i"
@@ -60,7 +60,7 @@
ncase_def "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
nil_def "[] == inl(one)"
- cons_def "h.t == inr(<h,t>)"
+ cons_def "h$t == inr(<h,t>)"
lcase_def "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
--- a/src/CCL/Type.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Type.ML Tue Mar 22 12:42:56 1994 +0100
@@ -183,9 +183,9 @@
val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
val NatXH = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
-val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x.xs))";
-val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x.xs))";
-val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x.xs)";
+val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x$xs))";
+val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x$xs))";
+val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x$xs)";
val iXHs = [NatXH,ListXH];
val icase_rls = XH_to_Es iXHs;
@@ -198,7 +198,7 @@
val zeroT = icanT_tac "zero : Nat";
val succT = icanT_tac "n:Nat ==> succ(n) : Nat";
val nilT = icanT_tac "[] : List(A)";
-val consT = icanT_tac "[| h:A; t:List(A) |] ==> h.t : List(A)";
+val consT = icanT_tac "[| h:A; t:List(A) |] ==> h$t : List(A)";
val icanTs = [zeroT,succT,nilT,consT];
@@ -209,7 +209,7 @@
val lcaseT = incanT_tac
"[| l:List(A); l=[] ==> b:C([]); \
-\ !!h t.[| h:A; t:List(A); l=h.t |] ==> c(h,t):C(h.t) |] ==> \
+\ !!h t.[| h:A; t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> \
\ lcase(l,b,c) : C(l)";
val incanTs = [ncaseT,lcaseT];
@@ -230,7 +230,7 @@
val List_ind = ind_tac
"[| l:List(A); P([]); \
-\ !!x xs.[| x:A; xs:List(A); P(xs) |] ==> P(x.xs) |] ==> \
+\ !!x xs.[| x:A; xs:List(A); P(xs) |] ==> P(x$xs) |] ==> \
\ P(l)";
val inds = [Nat_ind,List_ind];
@@ -250,7 +250,7 @@
val lrecT = prec_tac
"[| l:List(A); b:C([]); \
-\ !!x xs g.[| x:A; xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x.xs) |] ==> \
+\ !!x xs g.[| x:A; xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==> \
\ lrec(l,b,c) : C(l)";
val precTs = [nrecT,lrecT];
@@ -300,7 +300,7 @@
(* EG *)
val prems = goal Type.thy
- "letrec g x be zero.g(x) in g(bot) : Lists(Nat)";
+ "letrec g x be zero$g(x) in g(bot) : Lists(Nat)";
by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
br (letrecB RS ssubst) 1;
bw cons_def;
--- a/src/CCL/Wfd.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Wfd.ML Tue Mar 22 12:42:56 1994 +0100
@@ -179,7 +179,7 @@
by (fast_tac set_cs 1);
val NatPRXH = result();
-goalw Wfd.thy [ListPR_def] "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)";
+goalw Wfd.thy [ListPR_def] "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
by (fast_tac set_cs 1);
val ListPRXH = result();
--- a/src/CCL/Wfd.thy Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Wfd.thy Tue Mar 22 12:42:56 1994 +0100
@@ -30,5 +30,5 @@
"ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
NatPR_def "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
- ListPR_def "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h.t>}"
+ ListPR_def "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h$t>}"
end
--- a/src/CCL/coinduction.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/coinduction.ML Tue Mar 22 12:42:56 1994 +0100
@@ -60,7 +60,7 @@
"<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))",
"[| <h,h'> : lfp(%x. POgen(x) Un R Un PO); \
\ <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> \
-\ <h.t,h'.t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
+\ <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
fun POgen_tac (rla,rlb) i =
SELECT_GOAL (safe_tac ccl_cs) i THEN
@@ -90,7 +90,7 @@
"<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
"[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); \
\ <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |] ==> \
-\ <h.t,h'.t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"];
+\ <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"];
fun EQgen_raw_tac i =
(REPEAT (resolve_tac (EQgenIs @ [EQ_refl RS (EQgen_mono RS ci3_AI)] @
--- a/src/CCL/eval.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/eval.ML Tue Mar 22 12:42:56 1994 +0100
@@ -58,11 +58,11 @@
"[| n ---> zero; t ---> c |] ==> nrec(n,t,u) ---> c",
"[| n--->succ(x); u(x,nrec(x,t,u))--->c |] ==> nrec(n,t,u)--->c",
"[] ---> []",
- "h.t ---> h.t",
+ "h$t ---> h$t",
"[| l ---> []; t ---> c |] ==> lcase(l,t,u) ---> c",
- "[| l ---> x.xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c",
+ "[| l ---> x$xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c",
"[| l ---> []; t ---> c |] ==> lrec(l,t,u) ---> c",
- "[| l--->x.xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c"];
+ "[| l--->x$xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c"];
EVal_rls := !EVal_rls @ V_rls;
@@ -93,12 +93,12 @@
(* Reverse *)
val prems = goal thy
- "letrec id l be lcase(l,[],%x xs.x.id(xs)) \
-\ in id(zero.succ(zero).[]) ---> ?a";
+ "letrec id l be lcase(l,[],%x xs.x$id(xs)) \
+\ in id(zero$succ(zero)$[]) ---> ?a";
by (ceval_tac []);
val prems = goal thy
- "letrec rev l be lcase(l,[],%x xs.lrec(rev(xs),x.[],%y ys g.y.g)) \
-\ in rev(zero.succ(zero).(succ((lam x.x)`succ(zero))).([])) ---> ?a";
+ "letrec rev l be lcase(l,[],%x xs.lrec(rev(xs),x$[],%y ys g.y$g)) \
+\ in rev(zero$succ(zero)$(succ((lam x.x)`succ(zero)))$([])) ---> ?a";
by (ceval_tac []);
--- a/src/CCL/hered.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/hered.ML Tue Mar 22 12:42:56 1994 +0100
@@ -70,7 +70,7 @@
"zero : HTT",
"succ(n) : HTT <-> n : HTT",
"[] : HTT",
- "x.xs : HTT <-> x : HTT & xs : HTT"];
+ "x$xs : HTT <-> x : HTT & xs : HTT"];
end;
val HTT_Is = HTT_rews @ (HTT_rews RL [iffD2]);
@@ -108,7 +108,7 @@
\ succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>\
-\ h.t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
+\ h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
(*** Formation Rules for Types ***)
--- a/src/CCL/term.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/term.ML Tue Mar 22 12:42:56 1994 +0100
@@ -90,10 +90,10 @@
val nrecBbot = mk_beta_rl "nrec(bot,t,u) = bot";
val lcaseBnil = mk_beta_rl "lcase([],t,u) = t";
-val lcaseBcons = mk_beta_rl "lcase(x.xs,t,u) = u(x,xs)";
+val lcaseBcons = mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)";
val lcaseBbot = mk_beta_rl "lcase(bot,t,u) = bot";
val lrecBnil = mk_beta_rl "lrec([],t,u) = t";
-val lrecBcons = mk_beta_rl "lrec(x.xs,t,u) = u(x,xs,lrec(xs,t,u))";
+val lrecBcons = mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))";
val lrecBbot = mk_beta_rl "lrec(bot,t,u) = bot";
val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def])
@@ -120,12 +120,12 @@
["(inl(a) = inl(a')) <-> (a=a')",
"(inr(a) = inr(a')) <-> (a=a')",
"(succ(a) = succ(a')) <-> (a=a')",
- "(a.b = a'.b') <-> (a=a' & b=b')"];
+ "(a$b = a'$b') <-> (a=a' & b=b')"];
(*** Constructors are distinct ***)
val term_dstncts = mkall_dstnct_thms Term.thy data_defs (ccl_injs @ term_injs)
- [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op ."]];
+ [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op $"]];
(*** Rules for pre-order [= ***)
@@ -136,7 +136,7 @@
val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
"inr(b) [= inr(b') <-> b [= b'",
"succ(n) [= succ(n') <-> n [= n'",
- "x.xs [= x'.xs' <-> x [= x' & xs [= xs'"];
+ "x$xs [= x'$xs' <-> x [= x' & xs [= xs'"];
end;
(*** Rewriting and Proving ***)
--- a/src/CCL/term.thy Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/term.thy Tue Mar 22 12:42:56 1994 +0100
@@ -28,7 +28,7 @@
nrec :: "[i,i,[i,i]=>i]=>i"
nil :: "i" ("([])")
- "." :: "[i,i]=>i" (infixr 80)
+ "$" :: "[i,i]=>i" (infixr 80)
lcase :: "[i,i,[i,i]=>i]=>i"
lrec :: "[i,i,[i,i,i]=>i]=>i"
@@ -60,7 +60,7 @@
ncase_def "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
nil_def "[] == inl(one)"
- cons_def "h.t == inr(<h,t>)"
+ cons_def "h$t == inr(<h,t>)"
lcase_def "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
--- a/src/CCL/type.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/type.ML Tue Mar 22 12:42:56 1994 +0100
@@ -183,9 +183,9 @@
val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
val NatXH = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
-val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x.xs))";
-val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x.xs))";
-val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x.xs)";
+val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x$xs))";
+val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x$xs))";
+val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x$xs)";
val iXHs = [NatXH,ListXH];
val icase_rls = XH_to_Es iXHs;
@@ -198,7 +198,7 @@
val zeroT = icanT_tac "zero : Nat";
val succT = icanT_tac "n:Nat ==> succ(n) : Nat";
val nilT = icanT_tac "[] : List(A)";
-val consT = icanT_tac "[| h:A; t:List(A) |] ==> h.t : List(A)";
+val consT = icanT_tac "[| h:A; t:List(A) |] ==> h$t : List(A)";
val icanTs = [zeroT,succT,nilT,consT];
@@ -209,7 +209,7 @@
val lcaseT = incanT_tac
"[| l:List(A); l=[] ==> b:C([]); \
-\ !!h t.[| h:A; t:List(A); l=h.t |] ==> c(h,t):C(h.t) |] ==> \
+\ !!h t.[| h:A; t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> \
\ lcase(l,b,c) : C(l)";
val incanTs = [ncaseT,lcaseT];
@@ -230,7 +230,7 @@
val List_ind = ind_tac
"[| l:List(A); P([]); \
-\ !!x xs.[| x:A; xs:List(A); P(xs) |] ==> P(x.xs) |] ==> \
+\ !!x xs.[| x:A; xs:List(A); P(xs) |] ==> P(x$xs) |] ==> \
\ P(l)";
val inds = [Nat_ind,List_ind];
@@ -250,7 +250,7 @@
val lrecT = prec_tac
"[| l:List(A); b:C([]); \
-\ !!x xs g.[| x:A; xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x.xs) |] ==> \
+\ !!x xs g.[| x:A; xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==> \
\ lrec(l,b,c) : C(l)";
val precTs = [nrecT,lrecT];
@@ -300,7 +300,7 @@
(* EG *)
val prems = goal Type.thy
- "letrec g x be zero.g(x) in g(bot) : Lists(Nat)";
+ "letrec g x be zero$g(x) in g(bot) : Lists(Nat)";
by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
br (letrecB RS ssubst) 1;
bw cons_def;
--- a/src/CCL/typecheck.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/typecheck.ML Tue Mar 22 12:42:56 1994 +0100
@@ -25,7 +25,7 @@
"P(zero) ==> zero : {x:Nat.P(x)}",
"a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
"P([]) ==> [] : {x:List(A).P(x)}",
- "h : {x:A. t : {y:List(A).P(x.y)}} ==> h.t : {x:List(A).P(x)}"
+ "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
] end;
*)
val Subtype_canTs =
@@ -38,7 +38,7 @@
"a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}",
"b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}",
"a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
- "h : {x:A. t : {y:List(A).P(x.y)}} ==> h.t : {x:List(A).P(x)}"
+ "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
] end;
val prems = goal Type.thy
--- a/src/CCL/wfd.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/wfd.ML Tue Mar 22 12:42:56 1994 +0100
@@ -179,7 +179,7 @@
by (fast_tac set_cs 1);
val NatPRXH = result();
-goalw Wfd.thy [ListPR_def] "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)";
+goalw Wfd.thy [ListPR_def] "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
by (fast_tac set_cs 1);
val ListPRXH = result();
--- a/src/CCL/wfd.thy Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/wfd.thy Tue Mar 22 12:42:56 1994 +0100
@@ -30,5 +30,5 @@
"ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
NatPR_def "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
- ListPR_def "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h.t>}"
+ ListPR_def "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h$t>}"
end