--- a/src/HOLCF/Adm.thy Thu Apr 13 23:14:18 2006 +0200
+++ b/src/HOLCF/Adm.thy Thu Apr 13 23:15:44 2006 +0200
@@ -182,8 +182,8 @@
lemma compact_UU [simp, intro]: "compact \<bottom>"
by (rule compactI, simp add: adm_not_free)
-lemma adm_not_UU: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x = \<bottom>)"
-by (simp add: eq_UU_iff adm_not_less)
+lemma adm_not_UU: "cont t \<Longrightarrow> adm (\<lambda>x. t x \<noteq> \<bottom>)"
+by (simp add: adm_neq_compact)
lemmas adm_lemmas [simp] =
adm_not_free adm_conj adm_all2 adm_ball2 adm_disj adm_imp adm_iff
--- a/src/HOLCF/Lift.thy Thu Apr 13 23:14:18 2006 +0200
+++ b/src/HOLCF/Lift.thy Thu Apr 13 23:15:44 2006 +0200
@@ -84,7 +84,7 @@
lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y = (Def x = y)"
apply (induct y)
-apply (simp add: eq_UU_iff)
+apply simp
apply (simp add: Def_inject_less_eq)
done
--- a/src/HOLCF/Pcpo.thy Thu Apr 13 23:14:18 2006 +0200
+++ b/src/HOLCF/Pcpo.thy Thu Apr 13 23:15:44 2006 +0200
@@ -215,8 +215,11 @@
text {* useful lemmas about @{term \<bottom>} *}
+lemma less_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
+by (simp add: po_eq_conv)
+
lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
-by (simp add: po_eq_conv)
+by simp
lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
by (subst eq_UU_iff)
--- a/src/HOLCF/Ssum.thy Thu Apr 13 23:14:18 2006 +0200
+++ b/src/HOLCF/Ssum.thy Thu Apr 13 23:15:44 2006 +0200
@@ -118,16 +118,16 @@
by (simp add: less_Ssum_def Rep_Ssum_sinr)
lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr eq_UU_iff)
+by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr)
lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr eq_UU_iff)
+by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr)
lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
-by (simp add: po_eq_conv)
+by (subst po_eq_conv, simp)
lemma sinr_eq_sinl [simp]: "(sinr\<cdot>x = sinl\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
-by (simp add: po_eq_conv)
+by (subst po_eq_conv, simp)
subsection {* Chains of strict sums *}
--- a/src/HOLCF/ex/Stream.thy Thu Apr 13 23:14:18 2006 +0200
+++ b/src/HOLCF/ex/Stream.thy Thu Apr 13 23:15:44 2006 +0200
@@ -81,7 +81,6 @@
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)
-apply (drule eq_UU_iff [THEN iffD2], simp)
by (drule stream.inverts, auto)
lemma stream_prefix':
@@ -100,7 +99,6 @@
lemma stream_flat_prefix:
"[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
apply (case_tac "y=UU",auto)
-apply (drule eq_UU_iff [THEN iffD2],auto)
apply (drule stream.inverts,auto)
apply (drule ax_flat [rule_format],simp)
by (drule stream.inverts,auto)
@@ -323,8 +321,7 @@
by (rule stream_finite_lemma2,simp)
lemma stream_finite_less: "stream_finite s ==> !t. t<<s --> stream_finite t"
-apply (erule stream_finite_ind [of s])
-apply (clarsimp, drule eq_UU_iff [THEN iffD2], auto)
+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)
@@ -457,8 +454,6 @@
lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t"
apply (erule stream_finite_ind [of s], auto)
apply (case_tac "t=UU", auto)
-apply (drule eq_UU_iff [THEN iffD2])
-apply (drule scons_eq_UU [THEN iffD2], simp)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (erule_tac x="y" in allE, auto)
by (drule stream.inverts, auto)
@@ -489,7 +484,6 @@
apply (simp add: inat_defs)
apply (simp add: Suc_ile_eq)
apply (case_tac "y=UU", clarsimp)
-apply (drule eq_UU_iff [THEN iffD2],simp)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
apply (erule_tac x="ya" in allE, simp)
apply (drule stream.inverts,auto)
@@ -498,7 +492,6 @@
lemma slen_strict_mono_lemma:
"stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t"
apply (erule stream_finite_ind, auto)
-apply (drule eq_UU_iff [THEN iffD2], simp)
apply (case_tac "sa=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
apply (drule stream.inverts, simp, simp, clarsimp)
@@ -652,7 +645,6 @@
apply (simp add: i_th_def i_rt_Suc_back)
apply (rule stream.casedist [of "i_rt n s1"],simp)
apply (rule stream.casedist [of "i_rt n s2"],auto)
-apply (drule eq_UU_iff [THEN iffD2], simp add: scons_eq_UU)
by (intro monofun_cfun, auto)
lemma i_th_stream_take_Suc [rule_format]:
@@ -821,7 +813,7 @@
lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)"
apply (case_tac "#x",auto)
apply (insert sconc_mono1 [of x y])
- by (insert eq_UU_iff [THEN iffD2, of x],auto)
+ by auto
(* ----------------------------------------------------------------------- *)
@@ -1006,6 +998,4 @@
apply (simp add: stream.finite_def)
by (drule slen_take_lemma1,auto)
-declare eq_UU_iff [THEN sym, simp add]
-
end