added theorem less_cprod
authorhuffman
Wed Jun 08 00:07:46 2005 +0200 (2005-06-08)
changeset 16315bfb2f513916a
parent 16314 7102a1aaecfd
child 16316 17db5df51a35
added theorem less_cprod
src/HOLCF/Cprod.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Wed Jun 08 00:04:38 2005 +0200
     1.2 +++ b/src/HOLCF/Cprod.thy	Wed Jun 08 00:07:46 2005 +0200
     1.3 @@ -285,6 +285,9 @@
     1.4  apply (simp add: cont_fst cont_snd cpair_eq_pair)
     1.5  done
     1.6  
     1.7 +lemma less_cprod: "p1 \<sqsubseteq> p2 = (cfst\<cdot>p1 \<sqsubseteq> cfst\<cdot>p2 \<and> csnd\<cdot>p1 \<sqsubseteq> csnd\<cdot>p2)"
     1.8 +by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
     1.9 +
    1.10  lemma lub_cprod2: 
    1.11    "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    1.12  apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)