src/HOLCF/Ssum.thy
 changeset 16316 17db5df51a35 parent 16211 faa9691da2bc child 16699 24b494ff8f0f
```--- a/src/HOLCF/Ssum.thy	Wed Jun 08 00:07:46 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Wed Jun 08 00:16:28 2005 +0200
@@ -145,16 +145,16 @@

subsection {* Ordering properties of @{term sinl} and @{term sinr} *}

-lemma less_ssum4a: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
+lemma sinl_less: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
by (simp add: less_ssum_def Rep_Ssum_sinl cpair_less)

-lemma less_ssum4b: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
+lemma sinr_less: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
by (simp add: less_ssum_def Rep_Ssum_sinr cpair_less)

-lemma less_ssum4c: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
+lemma sinl_less_sinr: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)

-lemma less_ssum4d: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
+lemma sinr_less_sinl: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)

subsection {* Chains of strict sums *}
@@ -162,15 +162,15 @@
lemma less_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
apply (rule_tac p=p in ssumE)
apply (rule_tac x="\<bottom>" in exI, simp)