src/HOLCF/Completion.thy
changeset 39984 0300d5170622
parent 39983 910d3ea1efa8
child 40002 c5b5f7a3a3b1
     1.1 --- a/src/HOLCF/Completion.thy	Thu Oct 07 13:22:13 2010 -0700
     1.2 +++ b/src/HOLCF/Completion.thy	Thu Oct 07 13:33:06 2010 -0700
     1.3 @@ -410,4 +410,26 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma (in preorder) typedef_ideal_completion:
     1.8 +  fixes Abs :: "'a set \<Rightarrow> 'b::cpo"
     1.9 +  assumes type: "type_definition Rep Abs {S. ideal S}"
    1.10 +  assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
    1.11 +  assumes principal: "\<And>a. principal a = Abs {b. b \<preceq> a}"
    1.12 +  assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f"
    1.13 +  shows "ideal_completion r principal Rep"
    1.14 +proof
    1.15 +  interpret type_definition Rep Abs "{S. ideal S}" by fact
    1.16 +  fix a b :: 'a and x y :: 'b and Y :: "nat \<Rightarrow> 'b"
    1.17 +  show "ideal (Rep x)"
    1.18 +    using Rep [of x] by simp
    1.19 +  show "chain Y \<Longrightarrow> Rep (\<Squnion>i. Y i) = (\<Union>i. Rep (Y i))"
    1.20 +    using type below by (rule typedef_ideal_rep_contlub)
    1.21 +  show "Rep (principal a) = {b. b \<preceq> a}"
    1.22 +    by (simp add: principal Abs_inverse ideal_principal)
    1.23 +  show "Rep x \<subseteq> Rep y \<Longrightarrow> x \<sqsubseteq> y"
    1.24 +    by (simp only: below)
    1.25 +  show "\<exists>f::'a \<Rightarrow> nat. inj f"
    1.26 +    by (rule countable)
    1.27 +qed
    1.28 +
    1.29  end