# HG changeset patch
# User huffman
# Date 1214855276 -7200
# Node ID 42ee5e7c3b50a6f3a9fcf825a1a307a1b16724b3
# Parent  1fb3d1219c12fc43d38664327a313b8784acce21
remove unused Cset.thy

diff -r 1fb3d1219c12 -r 42ee5e7c3b50 src/HOLCF/Cset.thy
--- a/src/HOLCF/Cset.thy	Mon Jun 30 14:06:44 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-(*  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 1fb3d1219c12 -r 42ee5e7c3b50 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Mon Jun 30 14:06:44 2008 +0200
+++ b/src/HOLCF/IsaMakefile	Mon Jun 30 21:47:56 2008 +0200
@@ -30,7 +30,7 @@
 $(OUT)/HOLCF: $(OUT)/HOL Adm.thy Bifinite.thy Cfun.thy			\
   CompactBasis.thy Cont.thy ConvexPD.thy Cprod.thy Discrete.thy		\
   Domain.thy Ffun.thy Fixrec.thy Fix.thy HOLCF.thy Lift.thy		\
-  LowerPD.thy One.thy Pcpodef.thy Pcpo.thy Porder.thy Cset.thy		\
+  LowerPD.thy One.thy Pcpodef.thy Pcpo.thy Porder.thy			\
   Sprod.thy Ssum.thy Tr.thy UpperPD.thy Up.thy ROOT.ML			\
   Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML		\
   Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML		\