--- a/src/HOL/Library/Nat_Infinity.thy Sat May 09 09:17:45 2009 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Sun May 10 14:22:04 2009 +0200
@@ -24,7 +24,10 @@
Infty ("\<infinity>")
-lemma not_Infty_eq[simp]: "(x ~= Infty) = (EX i. x = Fin i)"
+lemma not_Infty_eq[iff]: "(x ~= Infty) = (EX i. x = Fin i)"
+by (cases x) auto
+
+lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = Infty)"
by (cases x) auto
--- a/src/HOLCF/FOCUS/Stream_adm.thy Sat May 09 09:17:45 2009 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Sun May 10 14:22:04 2009 +0200
@@ -50,11 +50,7 @@
apply ( erule spec)
apply ( assumption)
apply ( assumption)
-apply (drule not_ex [THEN iffD1])
-apply (subst slen_infinite)
-apply (erule thin_rl)
-apply (erule_tac x = j in allE)
-apply auto
+apply (metis inat_ord_code(4) slen_infinite)
done
(* should be without reference to stream length? *)
--- a/src/HOLCF/ex/Stream.thy Sat May 09 09:17:45 2009 +0200
+++ b/src/HOLCF/ex/Stream.thy Sun May 10 14:22:04 2009 +0200
@@ -873,7 +873,6 @@
lemma slen_sconc_finite1:
"[| #(x ooo y) = Infty; Fin n = #x |] ==> #y = Infty"
apply (case_tac "#y ~= Infty",auto)
-apply (simp only: slen_infinite [symmetric])
apply (drule_tac y=y in rt_sconc1)
apply (insert stream_finite_i_rt [of n "x ooo y"])
by (simp add: slen_infinite)
@@ -888,16 +887,15 @@
apply (drule ex_sconc,auto)
apply (erule contrapos_pp)
apply (insert stream_finite_i_rt)
- apply (simp add: slen_infinite,auto)
+ apply (fastsimp simp add: slen_infinite,auto)
by (simp add: sconc_def)
lemma sconc_finite: "(#x~=Infty & #y~=Infty) = (#(x ooo y)~=Infty)"
apply auto
- apply (case_tac "#x",auto)
- apply (erule contrapos_pp,simp)
- apply (erule slen_sconc_finite1,simp)
- apply (drule slen_sconc_infinite1 [of _ y],simp)
-by (drule slen_sconc_infinite2 [of _ x],simp)
+ apply (metis not_Infty_eq slen_sconc_finite1)
+ apply (metis not_Infty_eq slen_sconc_infinite1)
+apply (metis not_Infty_eq slen_sconc_infinite2)
+done
(* ----------------------------------------------------------------------- *)