src/HOLCF/Cprod.thy
changeset 25906 2179c6661218
parent 25905 098469c6c351
child 25907 695a9d88d697
     1.1 --- a/src/HOLCF/Cprod.thy	Mon Jan 14 20:04:40 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Mon Jan 14 20:28:59 2008 +0100
     1.3 @@ -118,26 +118,6 @@
     1.4  apply (erule monofun_snd [THEN ub2ub_monofun])
     1.5  done
     1.6  
     1.7 -lemma directed_lub_cprod:
     1.8 -  fixes S :: "('a::dcpo \<times> 'b::dcpo) set"
     1.9 -  assumes S: "directed S"
    1.10 -  shows "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)"
    1.11 -apply (rule is_lubI)
    1.12 -apply (rule is_ubI)
    1.13 -apply (rule_tac t=x in surjective_pairing [THEN ssubst])
    1.14 -apply (rule monofun_pair)
    1.15 -apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_fst S] imageI])
    1.16 -apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_snd S] imageI])
    1.17 -apply (rule_tac t=u in surjective_pairing [THEN ssubst])
    1.18 -apply (rule monofun_pair)
    1.19 -apply (rule is_lub_thelub')
    1.20 -apply (rule dir2dir_monofun [OF monofun_fst S])
    1.21 -apply (erule ub2ub_monofun' [OF monofun_fst])
    1.22 -apply (rule is_lub_thelub')
    1.23 -apply (rule dir2dir_monofun [OF monofun_snd S])
    1.24 -apply (erule ub2ub_monofun' [OF monofun_snd])
    1.25 -done
    1.26 -
    1.27  lemma thelub_cprod:
    1.28    "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
    1.29      \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
    1.30 @@ -152,15 +132,6 @@
    1.31    thus "\<exists>x. range S <<| x" ..
    1.32  qed
    1.33  
    1.34 -instance "*" :: (dcpo, dcpo) dcpo
    1.35 -proof
    1.36 -  fix S :: "('a \<times> 'b) set"
    1.37 -  assume "directed S"
    1.38 -  hence "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)"
    1.39 -    by (rule directed_lub_cprod)
    1.40 -  thus "\<exists>x. S <<| x" ..
    1.41 -qed
    1.42 -
    1.43  instance "*" :: (finite_po, finite_po) finite_po ..
    1.44  
    1.45  subsection {* Product type is pointed *}