1.1 --- a/src/HOLCF/Adm.thy Thu Apr 13 23:14:18 2006 +0200
1.2 +++ b/src/HOLCF/Adm.thy Thu Apr 13 23:15:44 2006 +0200
1.3 @@ -182,8 +182,8 @@
1.4 lemma compact_UU [simp, intro]: "compact \<bottom>"
1.5 by (rule compactI, simp add: adm_not_free)
1.6
1.7 -lemma adm_not_UU: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x = \<bottom>)"
1.8 -by (simp add: eq_UU_iff adm_not_less)
1.9 +lemma adm_not_UU: "cont t \<Longrightarrow> adm (\<lambda>x. t x \<noteq> \<bottom>)"
1.10 +by (simp add: adm_neq_compact)
1.11
1.12 lemmas adm_lemmas [simp] =
1.13 adm_not_free adm_conj adm_all2 adm_ball2 adm_disj adm_imp adm_iff
2.1 --- a/src/HOLCF/Lift.thy Thu Apr 13 23:14:18 2006 +0200
2.2 +++ b/src/HOLCF/Lift.thy Thu Apr 13 23:15:44 2006 +0200
2.3 @@ -84,7 +84,7 @@
2.4
2.5 lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y = (Def x = y)"
2.6 apply (induct y)
2.7 -apply (simp add: eq_UU_iff)
2.8 +apply simp
2.9 apply (simp add: Def_inject_less_eq)
2.10 done
2.11
3.1 --- a/src/HOLCF/Pcpo.thy Thu Apr 13 23:14:18 2006 +0200
3.2 +++ b/src/HOLCF/Pcpo.thy Thu Apr 13 23:15:44 2006 +0200
3.3 @@ -215,8 +215,11 @@
3.4
3.5 text {* useful lemmas about @{term \<bottom>} *}
3.6
3.7 +lemma less_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
3.8 +by (simp add: po_eq_conv)
3.9 +
3.10 lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
3.11 -by (simp add: po_eq_conv)
3.12 +by simp
3.13
3.14 lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
3.15 by (subst eq_UU_iff)
4.1 --- a/src/HOLCF/Ssum.thy Thu Apr 13 23:14:18 2006 +0200
4.2 +++ b/src/HOLCF/Ssum.thy Thu Apr 13 23:15:44 2006 +0200
4.3 @@ -118,16 +118,16 @@
4.4 by (simp add: less_Ssum_def Rep_Ssum_sinr)
4.5
4.6 lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
4.7 -by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr eq_UU_iff)
4.8 +by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr)
4.9
4.10 lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
4.11 -by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr eq_UU_iff)
4.12 +by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr)
4.13
4.14 lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
4.15 -by (simp add: po_eq_conv)
4.16 +by (subst po_eq_conv, simp)
4.17
4.18 lemma sinr_eq_sinl [simp]: "(sinr\<cdot>x = sinl\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
4.19 -by (simp add: po_eq_conv)
4.20 +by (subst po_eq_conv, simp)
4.21
4.22 subsection {* Chains of strict sums *}
4.23
5.1 --- a/src/HOLCF/ex/Stream.thy Thu Apr 13 23:14:18 2006 +0200
5.2 +++ b/src/HOLCF/ex/Stream.thy Thu Apr 13 23:15:44 2006 +0200
5.3 @@ -81,7 +81,6 @@
5.4 lemma stream_prefix:
5.5 "[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt"
5.6 apply (insert stream.exhaust [of t], auto)
5.7 -apply (drule eq_UU_iff [THEN iffD2], simp)
5.8 by (drule stream.inverts, auto)
5.9
5.10 lemma stream_prefix':
5.11 @@ -100,7 +99,6 @@
5.12 lemma stream_flat_prefix:
5.13 "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
5.14 apply (case_tac "y=UU",auto)
5.15 -apply (drule eq_UU_iff [THEN iffD2],auto)
5.16 apply (drule stream.inverts,auto)
5.17 apply (drule ax_flat [rule_format],simp)
5.18 by (drule stream.inverts,auto)
5.19 @@ -323,8 +321,7 @@
5.20 by (rule stream_finite_lemma2,simp)
5.21
5.22 lemma stream_finite_less: "stream_finite s ==> !t. t<<s --> stream_finite t"
5.23 -apply (erule stream_finite_ind [of s])
5.24 -apply (clarsimp, drule eq_UU_iff [THEN iffD2], auto)
5.25 +apply (erule stream_finite_ind [of s], auto)
5.26 apply (case_tac "t=UU", auto)
5.27 apply (drule stream_exhaust_eq [THEN iffD1],auto)
5.28 apply (drule stream.inverts, auto)
5.29 @@ -457,8 +454,6 @@
5.30 lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t"
5.31 apply (erule stream_finite_ind [of s], auto)
5.32 apply (case_tac "t=UU", auto)
5.33 -apply (drule eq_UU_iff [THEN iffD2])
5.34 -apply (drule scons_eq_UU [THEN iffD2], simp)
5.35 apply (drule stream_exhaust_eq [THEN iffD1], auto)
5.36 apply (erule_tac x="y" in allE, auto)
5.37 by (drule stream.inverts, auto)
5.38 @@ -489,7 +484,6 @@
5.39 apply (simp add: inat_defs)
5.40 apply (simp add: Suc_ile_eq)
5.41 apply (case_tac "y=UU", clarsimp)
5.42 -apply (drule eq_UU_iff [THEN iffD2],simp)
5.43 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
5.44 apply (erule_tac x="ya" in allE, simp)
5.45 apply (drule stream.inverts,auto)
5.46 @@ -498,7 +492,6 @@
5.47 lemma slen_strict_mono_lemma:
5.48 "stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t"
5.49 apply (erule stream_finite_ind, auto)
5.50 -apply (drule eq_UU_iff [THEN iffD2], simp)
5.51 apply (case_tac "sa=UU", auto)
5.52 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
5.53 apply (drule stream.inverts, simp, simp, clarsimp)
5.54 @@ -652,7 +645,6 @@
5.55 apply (simp add: i_th_def i_rt_Suc_back)
5.56 apply (rule stream.casedist [of "i_rt n s1"],simp)
5.57 apply (rule stream.casedist [of "i_rt n s2"],auto)
5.58 -apply (drule eq_UU_iff [THEN iffD2], simp add: scons_eq_UU)
5.59 by (intro monofun_cfun, auto)
5.60
5.61 lemma i_th_stream_take_Suc [rule_format]:
5.62 @@ -821,7 +813,7 @@
5.63 lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)"
5.64 apply (case_tac "#x",auto)
5.65 apply (insert sconc_mono1 [of x y])
5.66 - by (insert eq_UU_iff [THEN iffD2, of x],auto)
5.67 + by auto
5.68
5.69 (* ----------------------------------------------------------------------- *)
5.70
5.71 @@ -1006,6 +998,4 @@
5.72 apply (simp add: stream.finite_def)
5.73 by (drule slen_take_lemma1,auto)
5.74
5.75 -declare eq_UU_iff [THEN sym, simp add]
5.76 -
5.77 end