equal
deleted
inserted
replaced
56 by (simp add: sinl_Abs_Ssum Abs_Ssum_inverse sinl_Ssum) |
56 by (simp add: sinl_Abs_Ssum Abs_Ssum_inverse sinl_Ssum) |
57 |
57 |
58 lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)" |
58 lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)" |
59 by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum) |
59 by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum) |
60 |
60 |
61 subsection {* Properties of @{term sinl} and @{term sinr} *} |
61 subsection {* Properties of \emph{sinl} and \emph{sinr} *} |
62 |
62 |
63 text {* Ordering *} |
63 text {* Ordering *} |
64 |
64 |
65 lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)" |
65 lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)" |
66 by (simp add: below_Ssum_def Rep_Ssum_sinl strictify_conv_if) |
66 by (simp add: below_Ssum_def Rep_Ssum_sinl strictify_conv_if) |