--- a/src/HOLCF/ex/Stream.thy Wed May 03 03:46:25 2006 +0200
+++ b/src/HOLCF/ex/Stream.thy Wed May 03 03:47:15 2006 +0200
@@ -81,15 +81,15 @@
lemma stream_prefix:
"[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt"
apply (insert stream.exhaust [of t], auto)
-by (drule stream.inverts, auto)
+by (auto simp add: stream.inverts)
lemma stream_prefix':
"b ~= UU ==> x << b && z =
(x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))"
apply (case_tac "x=UU",auto)
apply (drule stream_exhaust_eq [THEN iffD1],auto)
-apply (drule stream.inverts,auto)
-by (intro monofun_cfun,auto)
+by (auto simp add: stream.inverts)
+
(*
lemma stream_prefix1: "[| x<<y; xs<<ys |] ==> x&&xs << y&&ys"
@@ -99,9 +99,9 @@
lemma stream_flat_prefix:
"[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
apply (case_tac "y=UU",auto)
-apply (drule stream.inverts,auto)
-apply (drule ax_flat [rule_format],simp)
-by (drule stream.inverts,auto)
+apply (auto simp add: stream.inverts)
+by (drule ax_flat [rule_format],simp)
+
@@ -324,7 +324,7 @@
apply (erule stream_finite_ind [of s], auto)
apply (case_tac "t=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1],auto)
-apply (drule stream.inverts, auto)
+apply (auto simp add: stream.inverts)
apply (erule_tac x="y" in allE, simp)
by (rule stream_finite_lemma1, simp)
@@ -456,7 +456,7 @@
apply (case_tac "t=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (erule_tac x="y" in allE, auto)
-by (drule stream.inverts, auto)
+by (auto simp add: stream.inverts)
lemma slen_mono: "s << t ==> #s <= #t"
apply (case_tac "stream_finite t")
@@ -486,7 +486,7 @@
apply (case_tac "y=UU", clarsimp)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
apply (erule_tac x="ya" in allE, simp)
-apply (drule stream.inverts,auto)
+apply (auto simp add: stream.inverts)
by (drule ax_flat [rule_format], simp)
lemma slen_strict_mono_lemma:
@@ -494,7 +494,7 @@
apply (erule stream_finite_ind, auto)
apply (case_tac "sa=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
-apply (drule stream.inverts, simp, simp, clarsimp)
+apply (simp add: stream.inverts, clarsimp)
by (drule ax_flat [rule_format], simp)
lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"