# HG changeset patch
# User nipkow
# Date 1241958124 -7200
# Node ID e270f45ac0ec0875519f6c7fab67d60994a6719c
# Parent  31b4cbe16debfddcdaa75193321434a71d61a997# Parent  f4db921165cecf9721ef467c269f920a2ef285bf
merged

diff -r 31b4cbe16deb -r e270f45ac0ec src/HOL/Library/Nat_Infinity.thy
--- 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
 
 
diff -r 31b4cbe16deb -r e270f45ac0ec src/HOLCF/FOCUS/Stream_adm.thy
--- 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? *)
diff -r 31b4cbe16deb -r e270f45ac0ec src/HOLCF/ex/Stream.thy
--- 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
 
 (* ----------------------------------------------------------------------- *)