src/HOLCF/ex/Coind.ML

 (* ------------------------------------------------------------------------- *)
 (* recursive  properties                                                     *)
 (* ------------------------------------------------------------------------- *)
 
 
-qed_goal "from" 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),
 	(rtac (from_def2 RS ssubst) 1),
 	(simp_tac HOLCF_ss  1),
 	(rtac refl 1)
 	]);
 
 
-qed_goal "from1" Coind.thy "from[UU] = UU"
+val from1 = prove_goal Coind.thy "from[UU] = UU"
  (fn prems =>
 	[
 	(rtac trans 1),
 	(rtac (from RS ssubst) 1),
 	(resolve_tac  stream_constrdef 1),

 (* the example                                                               *)
 (* prove:        nats = from[dzero]                                          *)
 (* ------------------------------------------------------------------------- *)
 
 
-qed_goal "coind_lemma1" Coind.thy "iterator[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),
 	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),

 	(rtac cfun_arg_cong 1),
 	(asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat_rews)) 1)
 	]);
 
 
-qed_goal "nats_eq_from" 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),
 	(res_inst_tac [("x","dzero")] exI 2),

 	(rtac disjI1 1),
 	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
 	(rtac disjI2 1),
 	(etac conjE 1),
 	(hyp_subst_tac 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),
 	(etac conjI 1),
 	(rtac conjI 1),

 	(fast_tac HOL_cs 1)
 	]);
 
 (* another proof using stream_coind_lemma2 *)
 
-qed_goal "nats_eq_from" 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),
 	(rtac stream_coind_lemma2 1),

 	(res_inst_tac [("Q","n=UU")] classical2 1),
 	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
 	(res_inst_tac [("x","UU::dnat")] exI 1),
 	(simp_tac (HOLCF_ss addsimps coind_rews addsimps stream_rews) 1),
 	(etac conjE 1),
-	(hyp_subst_tac 1),
 	(hyp_subst_tac 1),
 	(rtac conjI 1),
 	(rtac (coind_lemma1 RS ssubst) 1),
 	(rtac (from RS ssubst) 1),
 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),