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
```