# HG changeset patch
# User huffman
# Date 1144962944 -7200
# Node ID b2877e230b0732618e5053adedea89b8d93ca975
# Parent  27c2e4cd634bc4588330bf379b3d0145cd06ce12
add lemma less_UU_iff as default simp rule

diff -r 27c2e4cd634b -r b2877e230b07 src/HOLCF/Adm.thy
--- 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
diff -r 27c2e4cd634b -r b2877e230b07 src/HOLCF/Lift.thy
--- 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
 
diff -r 27c2e4cd634b -r b2877e230b07 src/HOLCF/Pcpo.thy
--- 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)
diff -r 27c2e4cd634b -r b2877e230b07 src/HOLCF/Ssum.thy
--- 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 *}
 
diff -r 27c2e4cd634b -r b2877e230b07 src/HOLCF/ex/Stream.thy
--- 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