author huffman Fri, 08 Jul 2005 02:38:05 +0200 changeset 16751 7af6723ad741 parent 16750 282d092b1dbd child 16752 270ec60cc9e8
 src/HOLCF/Sprod.thy file | annotate | diff | comparison | revisions
```--- a/src/HOLCF/Sprod.thy	Fri Jul 08 02:37:42 2005 +0200
+++ b/src/HOLCF/Sprod.thy	Fri Jul 08 02:38:05 2005 +0200
@@ -144,11 +144,14 @@
lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
by (rule_tac p=p in sprodE, simp_all)

-lemma less_sprod: "p1 \<sqsubseteq> p2 = (sfst\<cdot>p1 \<sqsubseteq> sfst\<cdot>p2 \<and> ssnd\<cdot>p1 \<sqsubseteq> ssnd\<cdot>p2)"
+lemma less_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
apply (simp add: less_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
apply (rule less_cprod)
done

+lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)"
+by (auto simp add: po_eq_conv less_sprod)
+
lemma spair_less:
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
apply (case_tac "a = \<bottom>")```