# HG changeset patch
# User huffman
# Date 1199485472 -3600
# Node ID fe56cdb73ae56776f5395d715048707521143482
# Parent  41a014cc44c031e68733af98009b4139a0eb3563
simplified some proofs

diff -r 41a014cc44c0 -r fe56cdb73ae5 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Fri Jan 04 16:35:22 2008 +0100
+++ b/src/HOLCF/ex/Stream.thy	Fri Jan 04 23:24:32 2008 +0100
@@ -335,9 +335,10 @@
 by (rule_tac x="n" in exI,simp)
 
 lemma adm_not_stream_finite: "adm (%x. ~ stream_finite x)"
-apply (rule admI2, auto)
-apply (drule stream_finite_less,drule is_ub_thelub)
-by auto
+apply (rule adm_upward)
+apply (erule contrapos_nn)
+apply (erule (1) stream_finite_less [rule_format])
+done
 
 
 
@@ -799,12 +800,20 @@
 
 (* ----------------------------------------------------------------------- *)
 
+lemma cont_sconc_lemma1: "stream_finite x \<Longrightarrow> cont (\<lambda>y. x ooo y)"
+by (erule stream_finite_ind, simp_all)
+
+lemma cont_sconc_lemma2: "\<not> stream_finite x \<Longrightarrow> cont (\<lambda>y. x ooo y)"
+by (simp add: sconc_def slen_def)
+
+lemma cont_sconc: "cont (\<lambda>y. x ooo y)"
+apply (cases "stream_finite x")
+apply (erule cont_sconc_lemma1)
+apply (erule cont_sconc_lemma2)
+done
+
 lemma sconc_mono: "y << y' ==> x ooo y << x ooo y'"
-apply (case_tac "#x")
- apply (rule stream_finite_ind [of "x"])
-   apply (auto simp add: stream.finite_def)
-  apply (drule slen_take_lemma1,blast)
- by (simp add: stream_prefix',auto simp add: sconc_def)
+by (rule cont_sconc [THEN cont2mono, THEN monofunE])
 
 lemma sconc_mono1 [simp]: "x << x ooo y"
 by (rule sconc_mono [of UU, simplified])
@@ -949,8 +958,7 @@
 by (simp add: contlub_Rep_CFun2)
 
 lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)"
-apply (insert contlub_scons [of a])
-by (simp only: contlub_def)
+by (rule contlubE [OF contlub_Rep_CFun2, symmetric])
 
 lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==>
                         (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
@@ -967,16 +975,11 @@
 done
 
 lemma contlub_sconc: "contlub (%y. x ooo y)"
-by (rule contlubI, insert contlub_sconc_lemma [of _ x], simp)
+by (rule cont_sconc [THEN cont2contlub])
 
 lemma monofun_sconc: "monofun (%y. x ooo y)"
 by (simp add: monofun_def sconc_mono)
 
-lemma cont_sconc: "cont (%y. x ooo y)"
-apply (rule  monocontlub2cont)
- apply (rule monofunI, simp add: sconc_mono)
-by (rule contlub_sconc)
-
 
 (* ----------------------------------------------------------------------- *)
    section "constr_sconc"