src/HOLCF/Cprod.thy
changeset 16916 da331e0a4a81
parent 16750 282d092b1dbd
child 17816 9942c5ed866a
equal deleted inserted replaced
16915:bca4c3b1afca 16916:da331e0a4a81
   130 by (rule minimal_cprod [THEN UU_I, symmetric])
   130 by (rule minimal_cprod [THEN UU_I, symmetric])
   131 
   131 
   132 
   132 
   133 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
   133 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
   134 
   134 
   135 lemma contlub_pair1: "contlub (\<lambda>x. (x,y))"
   135 lemma contlub_pair1: "contlub (\<lambda>x. (x, y))"
   136 apply (rule contlubI)
   136 apply (rule contlubI)
   137 apply (subst thelub_cprod)
   137 apply (subst thelub_cprod)
   138 apply (erule monofun_pair1 [THEN ch2ch_monofun])
   138 apply (erule monofun_pair1 [THEN ch2ch_monofun])
   139 apply (simp add: thelub_const)
   139 apply (simp add: thelub_const)
   140 done
   140 done
   250 by (simp add: cpair_eq_pair)
   250 by (simp add: cpair_eq_pair)
   251 
   251 
   252 lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
   252 lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
   253 by (simp add: cpair_eq_pair less_cprod_def)
   253 by (simp add: cpair_eq_pair less_cprod_def)
   254 
   254 
       
   255 lemma cpair_defined_iff: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
       
   256 by (simp add: inst_cprod_pcpo cpair_eq_pair)
       
   257 
   255 lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>"
   258 lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>"
   256 by (simp add: cpair_eq_pair inst_cprod_pcpo)
   259 by (simp add: cpair_defined_iff)
   257 
   260 
   258 lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
   261 lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
   259 by (simp add: cpair_eq_pair inst_cprod_pcpo)
   262 by (rule cpair_strict [symmetric])
   260 
   263 
   261 lemma defined_cpair_rev: 
   264 lemma defined_cpair_rev: 
   262  "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
   265  "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
   263 by (simp add: inst_cprod_pcpo cpair_eq_pair)
   266 by (simp add: inst_cprod_pcpo cpair_eq_pair)
   264 
   267