--- a/src/HOLCF/ex/Coind.ML Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/ex/Coind.ML Thu Jun 29 16:28:40 1995 +0200
@@ -11,11 +11,11 @@
(* ------------------------------------------------------------------------- *)
-val nats_def2 = fix_prover Coind.thy nats_def
- "nats = scons[dzero][smap[dsucc][nats]]";
+val nats_def2 = fix_prover2 Coind.thy nats_def
+ "nats = scons`dzero`(smap`dsucc`nats)";
-val from_def2 = fix_prover Coind.thy from_def
- "from = (LAM n.scons[n][from[dsucc[n]]])";
+val from_def2 = fix_prover2 Coind.thy from_def
+ "from = (LAM n.scons`n`(from`(dsucc`n)))";
@@ -24,7 +24,7 @@
(* ------------------------------------------------------------------------- *)
-val from = prove_goal Coind.thy "from[n] = scons[n][from[dsucc[n]]]"
+val from = prove_goal Coind.thy "from`n = scons`n`(from`(dsucc`n))"
(fn prems =>
[
(rtac trans 1),
@@ -34,7 +34,7 @@
]);
-val from1 = prove_goal Coind.thy "from[UU] = UU"
+val from1 = prove_goal Coind.thy "from`UU = UU"
(fn prems =>
[
(rtac trans 1),
@@ -49,12 +49,12 @@
(* ------------------------------------------------------------------------- *)
(* the example *)
-(* prove: nats = from[dzero] *)
+(* prove: nats = from`dzero *)
(* ------------------------------------------------------------------------- *)
-val coind_lemma1 = prove_goal Coind.thy "iterator[n][smap[dsucc]][nats] =\
-\ scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
+val coind_lemma1 = prove_goal Coind.thy "iterator`n`(smap`dsucc)`nats =\
+\ scons`n`(iterator`(dsucc`n)`(smap`dsucc)`nats)"
(fn prems =>
[
(res_inst_tac [("s","n")] dnat_ind 1),
@@ -74,11 +74,11 @@
]);
-val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
+val nats_eq_from = prove_goal Coind.thy "nats = from`dzero"
(fn prems =>
[
(res_inst_tac [("R",
-"% p q.? n. p = iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
+"% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1),
(res_inst_tac [("x","dzero")] exI 2),
(asm_simp_tac (HOLCF_ss addsimps coind_rews) 2),
(rewrite_goals_tac [stream_bisim_def]),
@@ -91,24 +91,24 @@
(etac conjE 1),
(hyp_subst_tac 1),
(res_inst_tac [("x","n")] exI 1),
- (res_inst_tac [("x","iterator[dsucc[n]][smap[dsucc]][nats]")] exI 1),
- (res_inst_tac [("x","from[dsucc[n]]")] exI 1),
+ (res_inst_tac [("x","iterator`(dsucc`n)`(smap`dsucc)`nats")] exI 1),
+ (res_inst_tac [("x","from`(dsucc`n)")] exI 1),
(etac conjI 1),
(rtac conjI 1),
(rtac coind_lemma1 1),
(rtac conjI 1),
(rtac from 1),
- (res_inst_tac [("x","dsucc[n]")] exI 1),
+ (res_inst_tac [("x","dsucc`n")] exI 1),
(fast_tac HOL_cs 1)
]);
(* another proof using stream_coind_lemma2 *)
-val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
+val nats_eq_from = prove_goal Coind.thy "nats = from`dzero"
(fn prems =>
[
(res_inst_tac [("R","% p q.? n. p = \
-\ iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
+\ iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1),
(rtac stream_coind_lemma2 1),
(strip_tac 1),
(etac exE 1),
@@ -122,7 +122,7 @@
(rtac (coind_lemma1 RS ssubst) 1),
(rtac (from RS ssubst) 1),
(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (res_inst_tac [("x","dsucc[n]")] exI 1),
+ (res_inst_tac [("x","dsucc`n")] exI 1),
(rtac conjI 1),
(rtac trans 1),
(rtac (coind_lemma1 RS ssubst) 1),