src/HOLCF/Stream.ML

 
 (* ------------------------------------------------------------------------*)
 (* Exhaustion and elimination for streams                                  *)
 (* ------------------------------------------------------------------------*)
 
-val Exh_stream = prove_goalw Stream.thy [scons_def]
+qed_goalw "Exh_stream" Stream.thy [scons_def]
 	"s = UU | (? x xs. x~=UU & s = scons[x][xs])"
  (fn prems =>
 	[
 	(simp_tac HOLCF_ss  1),
 	(rtac (stream_rep_iso RS subst) 1),

 	(rtac exI 1),
 	(etac conjI 1),
 	(asm_simp_tac HOLCF_ss  1)
 	]);
 
-val streamE = prove_goal Stream.thy 
+qed_goal "streamE" Stream.thy 
 	"[| s=UU ==> Q; !!x xs.[|s=scons[x][xs];x~=UU|]==>Q|]==>Q"
  (fn prems =>
 	[
 	(rtac (Exh_stream RS disjE) 1),
 	(eresolve_tac prems 1),

 
 (* ------------------------------------------------------------------------*)
 (* enhance the simplifier                                                  *)
 (* ------------------------------------------------------------------------*)
 
-val stream_copy2 = prove_goal Stream.thy 
+qed_goal "stream_copy2" Stream.thy 
      "stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
  (fn prems =>
 	[
 	(res_inst_tac [("Q","x=UU")] classical2 1),
 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
 	]);
 
-val shd2 = prove_goal Stream.thy "shd[scons[x][xs]]=x"
+qed_goal "shd2" Stream.thy "shd[scons[x][xs]]=x"
  (fn prems =>
 	[
 	(res_inst_tac [("Q","x=UU")] classical2 1),
 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
 	]);
 
-val stream_take2 = prove_goal Stream.thy 
+qed_goal "stream_take2" Stream.thy 
  "stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
  (fn prems =>
 	[
 	(res_inst_tac [("Q","x=UU")] classical2 1),
 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),

 
 val stream_take_lemma = prover stream_reach  [stream_take_def]
 	"(!!n.stream_take(n)[s1]=stream_take(n)[s2]) ==> s1=s2";
 
 
-val stream_reach2 = prove_goal Stream.thy  "lub(range(%i.stream_take(i)[s]))=s"
+qed_goal "stream_reach2" Stream.thy  "lub(range(%i.stream_take(i)[s]))=s"
  (fn prems =>
 	[
 	(res_inst_tac [("t","s")] (stream_reach RS subst) 1),
 	(rtac (fix_def2 RS ssubst) 1),
 	(rewrite_goals_tac [stream_take_def]),

 
 (* ------------------------------------------------------------------------*)
 (* Co -induction for streams                                               *)
 (* ------------------------------------------------------------------------*)
 
-val stream_coind_lemma = prove_goalw Stream.thy [stream_bisim_def] 
+qed_goalw "stream_coind_lemma" Stream.thy [stream_bisim_def] 
 "stream_bisim(R) ==> ! p q.R(p,q) --> stream_take(n)[p]=stream_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 stream_coind = prove_goal Stream.thy "[|stream_bisim(R);R(p,q)|] ==> p = q"
+qed_goal "stream_coind" Stream.thy "[|stream_bisim(R);R(p,q)|] ==> p = q"
  (fn prems =>
 	[
 	(rtac stream_take_lemma 1),
 	(rtac (stream_coind_lemma RS spec RS spec RS mp) 1),
 	(resolve_tac prems 1),

 
 (* ------------------------------------------------------------------------*)
 (* structural induction for admissible predicates                          *)
 (* ------------------------------------------------------------------------*)
 
-val stream_finite_ind = prove_goal Stream.thy
+qed_goal "stream_finite_ind" Stream.thy
 "[|P(UU);\
 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
 \  |] ==> !s.P(stream_take(n)[s])"
  (fn prems =>
 	[

 	(resolve_tac prems 1),
 	(atac 1),
 	(etac spec 1)
 	]);
 
-val stream_finite_ind2 = prove_goalw Stream.thy  [stream_finite_def]
+qed_goalw "stream_finite_ind2" Stream.thy  [stream_finite_def]
 "(!!n.P(stream_take(n)[s])) ==>  stream_finite(s) -->P(s)"
  (fn prems =>
 	[
 	(strip_tac 1),
 	(etac exE 1),
 	(etac subst 1),
 	(resolve_tac prems 1)
 	]);
 
-val stream_finite_ind3 = prove_goal Stream.thy 
+qed_goal "stream_finite_ind3" Stream.thy 
 "[|P(UU);\
 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
 \  |] ==> stream_finite(s) --> P(s)"
  (fn prems =>
 	[

 
 (* prove induction using definition of admissibility 
    stream_reach rsp. stream_reach2 
    and finite induction stream_finite_ind *)
 
-val stream_ind = prove_goal Stream.thy
+qed_goal "stream_ind" Stream.thy
 "[|adm(P);\
 \  P(UU);\
 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
 \  |] ==> P(s)"
  (fn prems =>

 	(REPEAT (resolve_tac prems 1)),
 	(REPEAT (atac 1))
 	]);
 
 (* prove induction with usual LCF-Method using fixed point induction *)
-val stream_ind = prove_goal Stream.thy
+qed_goal "stream_ind" Stream.thy
 "[|adm(P);\
 \  P(UU);\
 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
 \  |] ==> P(s)"
  (fn prems =>

 
 (* ------------------------------------------------------------------------*)
 (* simplify use of Co-induction                                            *)
 (* ------------------------------------------------------------------------*)
 
-val surjectiv_scons = prove_goal Stream.thy "scons[shd[s]][stl[s]]=s"
+qed_goal "surjectiv_scons" Stream.thy "scons[shd[s]][stl[s]]=s"
  (fn prems =>
 	[
 	(res_inst_tac [("s","s")] streamE 1),
 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
 	]);
 
 
-val stream_coind_lemma2 = prove_goalw Stream.thy [stream_bisim_def]
+qed_goalw "stream_coind_lemma2" Stream.thy [stream_bisim_def]
 "!s1 s2. R(s1, s2)-->shd[s1]=shd[s2] & R(stl[s1],stl[s2]) ==>stream_bisim(R)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(strip_tac 1),

 
 (* ----------------------------------------------------------------------- *)
 (* 2 lemmas about stream_finite                                            *)
 (* ----------------------------------------------------------------------- *)
 
-val stream_finite_UU = prove_goalw Stream.thy [stream_finite_def]
+qed_goalw "stream_finite_UU" Stream.thy [stream_finite_def]
 	 "stream_finite(UU)"
  (fn prems =>
 	[
 	(rtac exI 1),
 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
 	]);
 
-val inf_stream_not_UU = prove_goal Stream.thy  "~stream_finite(s)  ==> s ~= UU"
+qed_goal "inf_stream_not_UU" Stream.thy  "~stream_finite(s)  ==> s ~= UU"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(etac swap 1),
 	(dtac notnotD 1),

 
 (* ----------------------------------------------------------------------- *)
 (* a lemma about shd                                                       *)
 (* ----------------------------------------------------------------------- *)
 
-val stream_shd_lemma1 = prove_goal Stream.thy "shd[s]=UU --> s=UU"
+qed_goal "stream_shd_lemma1" Stream.thy "shd[s]=UU --> s=UU"
  (fn prems =>
 	[
 	(res_inst_tac [("s","s")] streamE 1),
 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
 	(hyp_subst_tac 1),

 
 (* ----------------------------------------------------------------------- *)
 (* lemmas about stream_take                                                *)
 (* ----------------------------------------------------------------------- *)
 
-val stream_take_lemma1 = prove_goal Stream.thy 
+qed_goal "stream_take_lemma1" Stream.thy 
  "!x xs.x~=UU --> \
 \  stream_take(Suc(n))[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
  (fn prems =>
 	[
 	(rtac allI 1),

 	(atac 1),
 	(atac 1)
 	]);
 
 
-val stream_take_lemma2 = prove_goal Stream.thy 
+qed_goal "stream_take_lemma2" Stream.thy 
  "! s2. stream_take(n)[s2] = s2 --> stream_take(Suc(n))[s2]=s2"
  (fn prems =>
 	[
 	(nat_ind_tac "n" 1),
 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),

 	(atac 2),
 	(rtac cfun_arg_cong 1),
 	(fast_tac HOL_cs 1)
 	]);
 
-val stream_take_lemma3 = prove_goal Stream.thy 
+qed_goal "stream_take_lemma3" Stream.thy 
  "!x xs.x~=UU --> \
 \  stream_take(n)[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
  (fn prems =>
 	[
 	(nat_ind_tac "n" 1),

 	(atac 1),
 	(atac 1),
 	(etac (stream_take2 RS subst) 1)
 	]);
 
-val stream_take_lemma4 = prove_goal Stream.thy 
+qed_goal "stream_take_lemma4" Stream.thy 
  "!x xs.\
 \stream_take(n)[xs]=xs --> stream_take(Suc(n))[scons[x][xs]] = scons[x][xs]"
  (fn prems =>
 	[
 	(nat_ind_tac "n" 1),

 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
 	]);
 
 (* ---- *)
 
-val stream_take_lemma5 = prove_goal Stream.thy 
+qed_goal "stream_take_lemma5" Stream.thy 
 "!s. stream_take(n)[s]=s --> iterate(n,stl,s)=UU"
  (fn prems =>
 	[
 	(nat_ind_tac "n" 1),
 	(simp_tac iterate_ss 1),

 	(hyp_subst_tac 1),
 	(etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
 	(atac 1)
 	]);
 
-val stream_take_lemma6 = prove_goal Stream.thy 
+qed_goal "stream_take_lemma6" Stream.thy 
 "!s.iterate(n,stl,s)=UU --> stream_take(n)[s]=s"
  (fn prems =>
 	[
 	(nat_ind_tac "n" 1),
 	(simp_tac iterate_ss 1),

 	(hyp_subst_tac 1),
 	(rtac (iterate_Suc2 RS ssubst) 1),
 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
 	]);
 
-val stream_take_lemma7 = prove_goal Stream.thy 
+qed_goal "stream_take_lemma7" Stream.thy 
 "(iterate(n,stl,s)=UU) = (stream_take(n)[s]=s)"
  (fn prems =>
 	[
 	(rtac iffI 1),
 	(etac (stream_take_lemma6 RS spec RS mp) 1),
 	(etac (stream_take_lemma5 RS spec RS mp) 1)
 	]);
 
 
-val stream_take_lemma8 = prove_goal Stream.thy
+qed_goal "stream_take_lemma8" Stream.thy
 "[|adm(P); !n. ? m. n < m & P(stream_take(m)[s])|] ==> P(s)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac (stream_reach2 RS subst) 1),

 
 (* ----------------------------------------------------------------------- *)
 (* lemmas stream_finite                                                    *)
 (* ----------------------------------------------------------------------- *)
 
-val stream_finite_lemma1 = prove_goalw Stream.thy [stream_finite_def]
+qed_goalw "stream_finite_lemma1" Stream.thy [stream_finite_def]
  "stream_finite(xs) ==> stream_finite(scons[x][xs])"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(etac exE 1),
 	(rtac exI 1),
 	(etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
 	]);
 
-val stream_finite_lemma2 = prove_goalw Stream.thy [stream_finite_def]
+qed_goalw "stream_finite_lemma2" Stream.thy [stream_finite_def]
  "[|x~=UU; stream_finite(scons[x][xs])|] ==> stream_finite(xs)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(etac exE 1),
 	(rtac exI 1),
 	(etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
 	(atac 1)
 	]);
 
-val stream_finite_lemma3 = prove_goal Stream.thy 
+qed_goal "stream_finite_lemma3" Stream.thy 
  "x~=UU ==> stream_finite(scons[x][xs]) = stream_finite(xs)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac iffI 1),

 	(atac 1),
 	(etac stream_finite_lemma1 1)
 	]);
 
 
-val stream_finite_lemma5 = prove_goalw Stream.thy [stream_finite_def]
+qed_goalw "stream_finite_lemma5" Stream.thy [stream_finite_def]
  "(!n. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1))\
 \=(s1 << s2  --> stream_finite(s2) --> stream_finite(s1))"
  (fn prems =>
 	[
 	(rtac iffI 1),
 	(fast_tac HOL_cs 1),
 	(fast_tac HOL_cs 1)
 	]);
 
-val stream_finite_lemma6 = prove_goal Stream.thy
+qed_goal "stream_finite_lemma6" Stream.thy
  "!s1 s2. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1)"
  (fn prems =>
 	[
 	(nat_ind_tac "n" 1),
 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),

 	(atac 1),
 	(atac 1),
 	(atac 1)
 	]);
 
-val stream_finite_lemma7 = prove_goal Stream.thy 
+qed_goal "stream_finite_lemma7" Stream.thy 
 "s1 << s2  --> stream_finite(s2) --> stream_finite(s1)"
  (fn prems =>
 	[
 	(rtac (stream_finite_lemma5 RS iffD1) 1),
 	(rtac allI 1),
 	(rtac (stream_finite_lemma6 RS spec RS spec) 1)
 	]);
 
-val stream_finite_lemma8 = prove_goalw Stream.thy [stream_finite_def]
+qed_goalw "stream_finite_lemma8" Stream.thy [stream_finite_def]
 "stream_finite(s) = (? n. iterate(n,stl,s)=UU)"
  (fn prems =>
 	[
 	(simp_tac (HOL_ss addsimps [stream_take_lemma7]) 1)
 	]);

 
 (* ----------------------------------------------------------------------- *)
 (* admissibility of ~stream_finite                                         *)
 (* ----------------------------------------------------------------------- *)
 
-val adm_not_stream_finite = prove_goalw Stream.thy [adm_def]
+qed_goalw "adm_not_stream_finite" Stream.thy [adm_def]
  "adm(%s. ~ stream_finite(s))"
  (fn prems =>
 	[
 	(strip_tac 1 ),
 	(res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical3 1),

 (* and prove adm. of ~(? n. iterate(n, stl, s) = UU)                       *)
 (* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8          *)
 (* ----------------------------------------------------------------------- *)
 
 
-val adm_not_stream_finite2=prove_goal Stream.thy "adm(%s. ~ stream_finite(s))"
+qed_goal "adm_not_stream_finite" Stream.thy "adm(%s. ~ stream_finite(s))"
  (fn prems =>
 	[
 	(subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate(n,stl,s)~=UU))" 1),
 	(etac (adm_cong RS iffD2)1),
 	(REPEAT(resolve_tac adm_thms 1)),