src/HOLCF/Cprod.thy
changeset 16315 bfb2f513916a
parent 16210 5d1b752cacc1
child 16553 aa36d41e4263
equal deleted inserted replaced
16314:7102a1aaecfd 16315:bfb2f513916a
   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)"
       
   289 by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
       
   290 
   288 lemma lub_cprod2: 
   291 lemma lub_cprod2: 
   289   "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   292   "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
   290 apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
   293 apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
   291 apply (erule lub_cprod)
   294 apply (erule lub_cprod)
   292 done
   295 done