# HG changeset patch # User huffman # Date 1120758000 -7200 # Node ID 5608017ee28b5a9984d441da6665a77918b82ad1 # Parent d0b61beefa495c6a382e4ee655adb078b43e37cb fixes to work with UU_reorient_simproc diff -r d0b61beefa49 -r 5608017ee28b src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Thu Jul 07 19:18:26 2005 +0200 +++ b/src/HOLCF/ex/Stream.thy Thu Jul 07 19:40:00 2005 +0200 @@ -174,7 +174,7 @@ lemma stream_take_lemma3 [rule_format]: "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs" apply (induct_tac n,clarsimp) -apply (drule sym, erule scons_not_empty, simp) +(*apply (drule sym, erule scons_not_empty, simp)*) apply (clarify, rule stream_take_more) apply (erule_tac x="x" in allE) by (erule_tac x="xs" in allE,simp) @@ -356,8 +356,8 @@ apply (simp add: slen_def, auto) apply (simp add: stream.finite_def, auto) apply (rule Least_Suc2,auto) -apply (drule sym) -apply (drule sym scons_eq_UU [THEN iffD1],simp) +(*apply (drule sym)*) +(*apply (drule sym scons_eq_UU [THEN iffD1],simp)*) apply (erule stream_finite_lemma2, simp) apply (simp add: slen_def, auto) by (drule stream_finite_lemma1,auto) @@ -384,7 +384,7 @@ lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \ | #y < Fin (Suc n))" apply (rule stream.casedist [of x], auto) -apply (drule sym, drule scons_eq_UU [THEN iffD1],auto) +apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto) apply (simp add: inat_defs split:inat_splits) apply (subgoal_tac "s=y & aa=a",simp); apply (simp add: inat_defs split:inat_splits) @@ -784,8 +784,8 @@ apply (simp add: i_rt_Suc_forw) apply (rule_tac x="a && x" in exI,auto) apply (case_tac "xa=UU",auto) - apply (drule_tac s="stream_take nat$x" in scons_neq_UU) - apply (simp add: i_rt_Suc_forw) +(*apply (drule_tac s="stream_take nat$x" in scons_neq_UU) + apply (simp add: i_rt_Suc_forw)*) apply (drule stream_exhaust_eq [THEN iffD1],auto) apply (drule streams_prefix_lemma1,simp+) by (simp add: sconc_def)