src/HOLCF/Dnat.ML

 
 (* ------------------------------------------------------------------------*)
 (* Exhaustion and elimination for dnat                                     *)
 (* ------------------------------------------------------------------------*)
 
-val Exh_dnat = prove_goalw Dnat.thy [dsucc_def,dzero_def]
+qed_goalw "Exh_dnat" Dnat.thy [dsucc_def,dzero_def]
 	"n = UU | n = dzero | (? x . x~=UU & n = dsucc[x])"
  (fn prems =>
 	[
 	(simp_tac HOLCF_ss  1),
 	(rtac (dnat_rep_iso RS subst) 1),

 	(rtac (disjI2 RS disjI2) 1),
 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
 	(fast_tac HOL_cs 1)
 	]);
 
-val dnatE = prove_goal Dnat.thy 
+qed_goal "dnatE" Dnat.thy 
  "[| n=UU ==> Q; n=dzero ==> Q; !!x.[|n=dsucc[x];x~=UU|]==>Q|]==>Q"
  (fn prems =>
 	[
 	(rtac (Exh_dnat RS disjE) 1),
 	(eresolve_tac prems 1),

 
 (* ------------------------------------------------------------------------*)
 (* Co -induction for dnats                                                 *)
 (* ------------------------------------------------------------------------*)
 
-val dnat_coind_lemma = prove_goalw Dnat.thy [dnat_bisim_def] 
+qed_goalw "dnat_coind_lemma" Dnat.thy [dnat_bisim_def] 
 "dnat_bisim(R) ==> ! p q.R(p,q) --> dnat_take(n)[p]=dnat_take(n)[q]"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(nat_ind_tac "n" 1),

 	(REPEAT (etac conjE 1)),
 	(rtac cfun_arg_cong 1),
 	(fast_tac HOL_cs 1)
 	]);
 
-val dnat_coind = prove_goal Dnat.thy "[|dnat_bisim(R);R(p,q)|] ==> p = q"
+qed_goal "dnat_coind" Dnat.thy "[|dnat_bisim(R);R(p,q)|] ==> p = q"
  (fn prems =>
 	[
 	(rtac dnat_take_lemma 1),
 	(rtac (dnat_coind_lemma RS spec RS spec RS mp) 1),
 	(resolve_tac prems 1),

 (* ------------------------------------------------------------------------*)
 (* structural induction for admissible predicates                          *)
 (* ------------------------------------------------------------------------*)
 
 (* not needed any longer
-val dnat_ind = prove_goal Dnat.thy
+qed_goal "dnat_ind" Dnat.thy
 "[| adm(P);\
 \   P(UU);\
 \   P(dzero);\
 \   !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc[s1])|] ==> P(s)"
  (fn prems =>

 	(eresolve_tac prems 1),
 	(etac spec 1)
 	]);
 *)
 
-val dnat_finite_ind = prove_goal Dnat.thy
+qed_goal "dnat_finite_ind" Dnat.thy
 "[|P(UU);P(dzero);\
 \  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
 \  |] ==> !s.P(dnat_take(n)[s])"
  (fn prems =>
 	[

 	(resolve_tac prems 1),
 	(atac 1),
 	(etac spec 1)
 	]);
 
-val dnat_all_finite_lemma1 = prove_goal Dnat.thy
+qed_goal "dnat_all_finite_lemma1" Dnat.thy
 "!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s"
  (fn prems =>
 	[
 	(nat_ind_tac "n" 1),
 	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),

 	(etac disjE 1),
 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
 	]);
 
-val dnat_all_finite_lemma2 = prove_goal Dnat.thy "? n.dnat_take(n)[s]=s"
+qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take(n)[s]=s"
  (fn prems =>
 	[
 	(res_inst_tac [("Q","s=UU")] classical2 1),
 	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
 	(subgoal_tac "(!n.dnat_take(n)[s]=UU) |(? n.dnat_take(n)[s]=s)" 1),

 	(rtac allI 1),
 	(rtac dnat_all_finite_lemma1 1)
 	]);
 
 
-val dnat_ind = prove_goal Dnat.thy
+qed_goal "dnat_ind" Dnat.thy
 "[|P(UU);P(dzero);\
 \  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
 \  |] ==> P(s)"
  (fn prems =>
 	[

 	(REPEAT (resolve_tac prems 1)),
 	(REPEAT (atac 1))
 	]);
 
 
-val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(dzero)"
+qed_goalw "dnat_flat" Dnat.thy [flat_def] "flat(dzero)"
  (fn prems =>
 	[
 	(rtac allI 1),
 	(res_inst_tac [("s","x")] dnat_ind 1),
 	(fast_tac HOL_cs 1),