# HG changeset patch
# User huffman
# Date 1213984993 -7200
# Node ID 2c42b1505f2577fa25969e5ab113eb2dd66dfced
# Parent  eec7a1889ca5d154ec7cb0c9bb8ef91c3857e51a
removed SetPcpo.thy and cpo instance for type bool;
added Cset.thy with pcpo type 'a cset isomorphic to 'a set;
updated ideal completion theory to use cset

diff -r eec7a1889ca5 -r 2c42b1505f25 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Fri Jun 20 19:59:00 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy	Fri Jun 20 20:03:13 2008 +0200
@@ -6,7 +6,7 @@
 header {* Compact bases of domains *}
 
 theory CompactBasis
-imports Bifinite SetPcpo
+imports Bifinite Cset
 begin
 
 subsection {* Ideals over a preorder *}
@@ -78,9 +78,16 @@
 apply (simp add: f)
 done
 
-lemma adm_ideal: "adm (\<lambda>A. ideal A)"
+lemma adm_ideal: "adm (\<lambda>A. ideal (Rep_cset A))"
 unfolding ideal_def by (intro adm_lemmas adm_set_lemmas)
 
+lemma cpodef_ideal_lemma:
+  "(\<exists>x. x \<in> {S. ideal (Rep_cset S)}) \<and> adm (\<lambda>x. x \<in> {S. ideal (Rep_cset S)})"
+apply (simp add: adm_ideal)
+apply (rule exI [where x="Abs_cset {x. x \<preceq> arbitrary}"])
+apply (simp add: ideal_principal)
+done
+
 lemma lub_image_principal:
   assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
@@ -150,7 +157,7 @@
   fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
   fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
   assumes ideal_rep: "\<And>x. preorder.ideal r (rep x)"
-  assumes cont_rep: "cont rep"
+  assumes rep_contlub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
   assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}"
   assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
 begin
@@ -216,14 +223,12 @@
 by (rule exI, rule basis_fun_lemma2, erule f_mono)
 
 lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
-apply (drule cont_rep [THEN cont2mono, THEN monofunE])
-apply (simp add: set_cpo_simps)
+apply (frule bin_chain)
+apply (drule rep_contlub)
+apply (simp only: thelubI [OF lub_bin_chain])
+apply (rule subsetI, rule UN_I [where a=0], simp_all)
 done
 
-lemma rep_contlub:
-  "chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
-by (simp add: cont2contlubE [OF cont_rep] set_cpo_simps)
-
 lemma less_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
 by (rule iffI [OF rep_mono subset_repD])
 
@@ -537,16 +542,13 @@
       done
   qed
 next
-  show "cont compacts"
+  fix Y :: "nat \<Rightarrow> 'a"
+  assume Y: "chain Y"
+  show "compacts (\<Squnion>i. Y i) = (\<Union>i. compacts (Y i))"
     unfolding compacts_def
-    apply (rule contI2)
-    apply (rule monofunI)
-    apply (simp add: set_cpo_simps)
-    apply (fast intro: trans_less)
-    apply (simp add: set_cpo_simps)
-    apply clarify
-    apply simp
-    apply (erule (1) compactD2 [OF compact_Rep_compact_basis])
+    apply safe
+    apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
+    apply (erule trans_less, rule is_ub_thelub [OF Y])
     done
 next
   fix a :: "'a compact_basis"
diff -r eec7a1889ca5 -r 2c42b1505f25 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Fri Jun 20 19:59:00 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy	Fri Jun 20 20:03:13 2008 +0200
@@ -142,30 +142,24 @@
 subsection {* Type definition *}
 
 cpodef (open) 'a convex_pd =
-  "{S::'a::profinite pd_basis set. convex_le.ideal S}"
-apply (simp add: convex_le.adm_ideal)
-apply (fast intro: convex_le.ideal_principal)
-done
+  "{S::'a pd_basis cset. convex_le.ideal (Rep_cset S)}"
+by (rule convex_le.cpodef_ideal_lemma)
 
-lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
+lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_cset (Rep_convex_pd xs))"
 by (rule Rep_convex_pd [unfolded mem_Collect_eq])
 
-lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys"
-unfolding less_convex_pd_def less_set_eq .
-
 definition
   convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
-  "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
+  "convex_principal t = Abs_convex_pd (Abs_cset {u. u \<le>\<natural> t})"
 
 lemma Rep_convex_principal:
-  "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}"
+  "Rep_cset (Rep_convex_pd (convex_principal t)) = {u. u \<le>\<natural> t}"
 unfolding convex_principal_def
-apply (rule Abs_convex_pd_inverse [simplified])
-apply (rule convex_le.ideal_principal)
-done
+by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
 
 interpretation convex_pd:
-  ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
+  ideal_completion
+    [convex_le approx_pd convex_principal "\<lambda>x. Rep_cset (Rep_convex_pd x)"]
 apply unfold_locales
 apply (rule approx_pd_convex_le)
 apply (rule approx_pd_idem)
@@ -174,9 +168,9 @@
 apply (rule finite_range_approx_pd)
 apply (rule approx_pd_covers)
 apply (rule ideal_Rep_convex_pd)
-apply (rule cont_Rep_convex_pd)
+apply (simp add: cont2contlubE [OF cont_Rep_convex_pd] Rep_cset_lub)
 apply (rule Rep_convex_principal)
-apply (simp only: less_convex_pd_def less_set_eq)
+apply (simp only: less_convex_pd_def sq_le_cset_def)
 done
 
 text {* Convex powerdomain is pointed *}
@@ -216,7 +210,8 @@
 by (rule convex_pd.completion_approx_principal)
 
 lemma approx_eq_convex_principal:
-  "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
+  "\<exists>t\<in>Rep_cset (Rep_convex_pd xs).
+    approx n\<cdot>xs = convex_principal (approx_pd n t)"
 unfolding approx_convex_pd_def
 by (rule convex_pd.completion_approx_eq_principal)
 
diff -r eec7a1889ca5 -r 2c42b1505f25 src/HOLCF/Cset.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Cset.thy	Fri Jun 20 20:03:13 2008 +0200
@@ -0,0 +1,117 @@
+(*  Title:      HOLCF/Cset.thy
+    ID:         $Id$
+    Author:     Brian Huffman
+*)
+
+header {* Set as a pointed cpo *}
+
+theory Cset
+imports Adm
+begin
+
+subsection {* Type definition *}
+
+defaultsort type
+
+typedef (open) 'a cset = "UNIV :: 'a set set" ..
+
+declare Rep_cset_inverse [simp]
+declare Abs_cset_inverse [simplified, simp]
+
+instantiation cset :: (type) po
+begin
+
+definition
+  sq_le_cset_def:
+    "x \<sqsubseteq> y \<longleftrightarrow> Rep_cset x \<subseteq> Rep_cset y"
+
+instance proof
+  fix x :: "'a cset"
+  show "x \<sqsubseteq> x"
+    unfolding sq_le_cset_def
+    by (rule subset_refl)
+next
+  fix x y z :: "'a cset"
+  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
+    unfolding sq_le_cset_def
+    by (rule subset_trans)
+next
+  fix x y :: "'a cset"
+  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
+    unfolding sq_le_cset_def Rep_cset_inject [symmetric]
+    by (rule subset_antisym)
+qed
+
+end
+
+lemma is_lub_UNION: "A <<| Abs_cset (UNION A Rep_cset)"
+unfolding is_lub_def is_ub_def sq_le_cset_def by auto
+
+instance cset :: (type) cpo
+proof
+  fix S :: "nat \<Rightarrow> 'a cset"
+  show "\<exists>x. range S <<| x"
+    by (fast intro: is_lub_UNION)
+qed
+
+lemma lub_cset: "lub A = Abs_cset (UNION A Rep_cset)"
+by (rule thelubI [OF is_lub_UNION])
+
+lemma Rep_cset_lub: "Rep_cset (lub A) = UNION A Rep_cset"
+by (simp add: lub_cset)
+
+text {* cset is pointed *}
+
+lemma cset_minimal: "Abs_cset {} \<sqsubseteq> x"
+unfolding sq_le_cset_def by simp
+
+instance cset :: (type) pcpo
+by intro_classes (fast intro: cset_minimal)
+
+lemma inst_cset_pcpo: "\<bottom> = Abs_cset {}"
+by (rule cset_minimal [THEN UU_I, symmetric])
+
+lemma Rep_cset_UU: "Rep_cset \<bottom> = {}"
+unfolding inst_cset_pcpo by simp
+
+lemmas Rep_cset_simps = Rep_cset_lub Rep_cset_UU
+
+subsection {* Admissibility of set predicates *}
+
+lemma adm_nonempty: "adm (\<lambda>A. \<exists>x. x \<in> Rep_cset A)"
+by (rule admI, simp add: Rep_cset_lub, fast)
+
+lemma adm_in: "adm (\<lambda>A. x \<in> Rep_cset A)"
+by (rule admI, simp add: Rep_cset_lub)
+
+lemma adm_not_in: "adm (\<lambda>A. x \<notin> Rep_cset A)"
+by (rule admI, simp add: Rep_cset_lub)
+
+lemma adm_Ball: "(\<And>x. adm (\<lambda>A. P A x)) \<Longrightarrow> adm (\<lambda>A. \<forall>x\<in>Rep_cset A. P A x)"
+unfolding Ball_def by (simp add: adm_not_in)
+
+lemma adm_Bex: "adm (\<lambda>A. \<exists>x\<in>Rep_cset A. P x)"
+by (rule admI, simp add: Rep_cset_lub)
+
+lemma adm_subset: "adm (\<lambda>A. Rep_cset A \<subseteq> B)"
+by (rule admI, auto simp add: Rep_cset_lub)
+
+lemma adm_superset: "adm (\<lambda>A. B \<subseteq> Rep_cset A)"
+by (rule admI, auto simp add: Rep_cset_lub)
+
+lemmas adm_set_lemmas =
+  adm_nonempty adm_in adm_not_in adm_Bex adm_Ball adm_subset adm_superset
+
+subsection {* Compactness *}
+
+lemma compact_empty: "compact (Abs_cset {})"
+by (fold inst_cset_pcpo, simp)
+
+lemma compact_insert: "compact (Abs_cset A) \<Longrightarrow> compact (Abs_cset (insert x A))"
+unfolding compact_def sq_le_cset_def
+by (simp add: adm_set_lemmas)
+
+lemma finite_imp_compact: "finite A \<Longrightarrow> compact (Abs_cset A)"
+by (induct A set: finite, rule compact_empty, erule compact_insert)
+
+end
diff -r eec7a1889ca5 -r 2c42b1505f25 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Fri Jun 20 19:59:00 2008 +0200
+++ b/src/HOLCF/LowerPD.thy	Fri Jun 20 20:03:13 2008 +0200
@@ -97,27 +97,24 @@
 subsection {* Type definition *}
 
 cpodef (open) 'a lower_pd =
-  "{S::'a::profinite pd_basis set. lower_le.ideal S}"
-apply (simp add: lower_le.adm_ideal)
-apply (fast intro: lower_le.ideal_principal)
-done
+  "{S::'a pd_basis cset. lower_le.ideal (Rep_cset S)}"
+by (rule lower_le.cpodef_ideal_lemma)
 
-lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd x)"
+lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_cset (Rep_lower_pd xs))"
 by (rule Rep_lower_pd [unfolded mem_Collect_eq])
 
 definition
   lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
-  "lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}"
+  "lower_principal t = Abs_lower_pd (Abs_cset {u. u \<le>\<flat> t})"
 
 lemma Rep_lower_principal:
-  "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}"
+  "Rep_cset (Rep_lower_pd (lower_principal t)) = {u. u \<le>\<flat> t}"
 unfolding lower_principal_def
-apply (rule Abs_lower_pd_inverse [simplified])
-apply (rule lower_le.ideal_principal)
-done
+by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
 
 interpretation lower_pd:
-  ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd]
+  ideal_completion
+    [lower_le approx_pd lower_principal "\<lambda>x. Rep_cset (Rep_lower_pd x)"]
 apply unfold_locales
 apply (rule approx_pd_lower_le)
 apply (rule approx_pd_idem)
@@ -126,9 +123,9 @@
 apply (rule finite_range_approx_pd)
 apply (rule approx_pd_covers)
 apply (rule ideal_Rep_lower_pd)
-apply (rule cont_Rep_lower_pd)
+apply (simp add: cont2contlubE [OF cont_Rep_lower_pd] Rep_cset_lub)
 apply (rule Rep_lower_principal)
-apply (simp only: less_lower_pd_def less_set_eq)
+apply (simp only: less_lower_pd_def sq_le_cset_def)
 done
 
 text {* Lower powerdomain is pointed *}
@@ -168,7 +165,8 @@
 by (rule lower_pd.completion_approx_principal)
 
 lemma approx_eq_lower_principal:
-  "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
+  "\<exists>t\<in>Rep_cset (Rep_lower_pd xs).
+    approx n\<cdot>xs = lower_principal (approx_pd n t)"
 unfolding approx_lower_pd_def
 by (rule lower_pd.completion_approx_eq_principal)
 
diff -r eec7a1889ca5 -r 2c42b1505f25 src/HOLCF/SetPcpo.thy
--- a/src/HOLCF/SetPcpo.thy	Fri Jun 20 19:59:00 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(*  Title:      HOLCF/SetPcpo.thy
-    ID:         $Id$
-    Author:     Brian Huffman
-*)
-
-header {* Set as a pointed cpo *}
-
-theory SetPcpo
-imports Adm Ffun
-begin
-
-instantiation bool :: po
-begin
-
-definition
-  less_bool_def: "(op \<sqsubseteq>) = (op \<longrightarrow>)"
-
-instance
-by (intro_classes, unfold less_bool_def, safe)
-
-end
-
-lemma less_set_eq: "(op \<sqsubseteq>) = (op \<subseteq>)"
-  by (simp add: less_fun_def less_bool_def le_fun_def le_bool_def expand_fun_eq)
-
-instance bool :: finite_po ..
-
-lemma Union_is_lub: "A <<| Union A"
-unfolding is_lub_def is_ub_def less_set_eq by fast
-
-instance bool :: cpo ..
-
-lemma lub_eq_Union: "lub = Union"
-by (rule ext, rule thelubI [OF Union_is_lub])
-
-instance bool :: pcpo
-proof
-  have "\<forall>y::bool. False \<sqsubseteq> y" unfolding less_bool_def by simp
-  thus "\<exists>x::bool. \<forall>y. x \<sqsubseteq> y" ..
-qed
-
-lemma UU_eq_empty: "\<bottom> = {}"
-by (rule UU_I [symmetric], simp add: less_set_eq)
-
-lemmas set_cpo_simps = less_set_eq lub_eq_Union UU_eq_empty
-
-subsection {* Admissibility of set predicates *}
-
-lemma adm_nonempty: "adm (\<lambda>A. \<exists>x. x \<in> A)"
-by (rule admI, force simp add: lub_eq_Union)
-
-lemma adm_in: "adm (\<lambda>A. x \<in> A)"
-by (rule admI, simp add: lub_eq_Union)
-
-lemma adm_not_in: "adm (\<lambda>A. x \<notin> A)"
-by (rule admI, simp add: lub_eq_Union)
-
-lemma adm_Ball: "(\<And>x. adm (\<lambda>A. P A x)) \<Longrightarrow> adm (\<lambda>A. \<forall>x\<in>A. P A x)"
-unfolding Ball_def by (simp add: adm_not_in)
-
-lemma adm_Bex: "adm (\<lambda>A. Bex A P)"
-by (rule admI, simp add: lub_eq_Union)
-
-lemma adm_subset: "adm (\<lambda>A. A \<subseteq> B)"
-by (rule admI, auto simp add: lub_eq_Union)
-
-lemma adm_superset: "adm (\<lambda>A. B \<subseteq> A)"
-by (rule admI, auto simp add: lub_eq_Union)
-
-lemmas adm_set_lemmas =
-  adm_nonempty adm_in adm_not_in adm_Bex adm_Ball adm_subset adm_superset
-
-subsection {* Compactness *}
-
-lemma compact_empty: "compact {}"
-by (fold UU_eq_empty, simp)
-
-lemma compact_insert: "compact A \<Longrightarrow> compact (insert x A)"
-unfolding compact_def set_cpo_simps
-by (simp add: adm_set_lemmas)
-
-lemma finite_imp_compact: "finite A \<Longrightarrow> compact A"
-by (induct A set: finite, rule compact_empty, erule compact_insert)
-
-end
diff -r eec7a1889ca5 -r 2c42b1505f25 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Fri Jun 20 19:59:00 2008 +0200
+++ b/src/HOLCF/UpperPD.thy	Fri Jun 20 20:03:13 2008 +0200
@@ -95,27 +95,24 @@
 subsection {* Type definition *}
 
 cpodef (open) 'a upper_pd =
-  "{S::'a::profinite pd_basis set. upper_le.ideal S}"
-apply (simp add: upper_le.adm_ideal)
-apply (fast intro: upper_le.ideal_principal)
-done
+  "{S::'a pd_basis cset. upper_le.ideal (Rep_cset S)}"
+by (rule upper_le.cpodef_ideal_lemma)
 
-lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd x)"
+lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_cset (Rep_upper_pd xs))"
 by (rule Rep_upper_pd [unfolded mem_Collect_eq])
 
 definition
   upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
-  "upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}"
+  "upper_principal t = Abs_upper_pd (Abs_cset {u. u \<le>\<sharp> t})"
 
 lemma Rep_upper_principal:
-  "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}"
+  "Rep_cset (Rep_upper_pd (upper_principal t)) = {u. u \<le>\<sharp> t}"
 unfolding upper_principal_def
-apply (rule Abs_upper_pd_inverse [unfolded mem_Collect_eq])
-apply (rule upper_le.ideal_principal)
-done
+by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
 
 interpretation upper_pd:
-  ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd]
+  ideal_completion
+    [upper_le approx_pd upper_principal "\<lambda>x. Rep_cset (Rep_upper_pd x)"]
 apply unfold_locales
 apply (rule approx_pd_upper_le)
 apply (rule approx_pd_idem)
@@ -124,9 +121,9 @@
 apply (rule finite_range_approx_pd)
 apply (rule approx_pd_covers)
 apply (rule ideal_Rep_upper_pd)
-apply (rule cont_Rep_upper_pd)
+apply (simp add: cont2contlubE [OF cont_Rep_upper_pd] Rep_cset_lub)
 apply (rule Rep_upper_principal)
-apply (simp only: less_upper_pd_def less_set_eq)
+apply (simp only: less_upper_pd_def sq_le_cset_def)
 done
 
 text {* Upper powerdomain is pointed *}
@@ -166,7 +163,8 @@
 by (rule upper_pd.completion_approx_principal)
 
 lemma approx_eq_upper_principal:
-  "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
+  "\<exists>t\<in>Rep_cset (Rep_upper_pd xs).
+    approx n\<cdot>xs = upper_principal (approx_pd n t)"
 unfolding approx_upper_pd_def
 by (rule upper_pd.completion_approx_eq_principal)