src/HOLCF/Cprod.thy
changeset 16750 282d092b1dbd
parent 16553 aa36d41e4263
child 16916 da331e0a4a81
equal deleted inserted replaced
16749:c96aaaf25f48 16750:282d092b1dbd
   283 lemma surjective_pairing_Cprod2: "<cfst\<cdot>p, csnd\<cdot>p> = p"
   283 lemma surjective_pairing_Cprod2: "<cfst\<cdot>p, csnd\<cdot>p> = p"
   284 apply (unfold cfst_def csnd_def)
   284 apply (unfold cfst_def csnd_def)
   285 apply (simp add: cont_fst cont_snd cpair_eq_pair)
   285 apply (simp add: cont_fst cont_snd cpair_eq_pair)
   286 done
   286 done
   287 
   287 
   288 lemma less_cprod: "p1 \<sqsubseteq> p2 = (cfst\<cdot>p1 \<sqsubseteq> cfst\<cdot>p2 \<and> csnd\<cdot>p1 \<sqsubseteq> csnd\<cdot>p2)"
   288 lemma less_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
   289 by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
   289 by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
       
   290 
       
   291 lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
       
   292 by (auto simp add: po_eq_conv less_cprod)
   290 
   293 
   291 lemma lub_cprod2: 
   294 lemma lub_cprod2: 
   292   "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   295   "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   293 apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
   296 apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
   294 apply (erule lub_cprod)
   297 apply (erule lub_cprod)