# HG changeset patch
# User huffman
# Date 1292633025 28800
# Node ID 6d66975b711fe0611f04b5ba4b06ab52988c0f0d
# Parent  ffae1d9bad06e9e4f384afd2cb7bafac892be4a2
renamed CompactBasis.thy to Compact_Basis.thy

diff -r ffae1d9bad06 -r 6d66975b711f src/HOL/HOLCF/CompactBasis.thy
--- a/src/HOL/HOLCF/CompactBasis.thy	Fri Dec 17 23:18:39 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(*  Title:      HOLCF/CompactBasis.thy
-    Author:     Brian Huffman
-*)
-
-header {* A compact basis for powerdomains *}
-
-theory CompactBasis
-imports Bifinite
-begin
-
-default_sort "domain"
-
-subsection {* A compact basis for powerdomains *}
-
-typedef 'a pd_basis =
-  "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
-by (rule_tac x="{arbitrary}" in exI, simp)
-
-lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
-by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
-
-lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
-by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
-
-text {* The powerdomain basis type is countable. *}
-
-lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
-proof -
-  obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
-    using compact_basis.countable ..
-  hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B"
-    by (rule inj_image_eq_iff)
-  have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))"
-    by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
-  thus ?thesis by - (rule exI)
-  (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
-qed
-
-subsection {* Unit and plus constructors *}
-
-definition
-  PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
-  "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
-
-definition
-  PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
-  "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
-
-lemma Rep_PDUnit:
-  "Rep_pd_basis (PDUnit x) = {x}"
-unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
-
-lemma Rep_PDPlus:
-  "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
-unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
-
-lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
-unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
-
-lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
-unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
-
-lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
-unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
-
-lemma PDPlus_absorb: "PDPlus t t = t"
-unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
-
-lemma pd_basis_induct1:
-  assumes PDUnit: "\<And>a. P (PDUnit a)"
-  assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
-  shows "P x"
-apply (induct x, unfold pd_basis_def, clarify)
-apply (erule (1) finite_ne_induct)
-apply (cut_tac a=x in PDUnit)
-apply (simp add: PDUnit_def)
-apply (drule_tac a=x in PDPlus)
-apply (simp add: PDUnit_def PDPlus_def
-  Abs_pd_basis_inverse [unfolded pd_basis_def])
-done
-
-lemma pd_basis_induct:
-  assumes PDUnit: "\<And>a. P (PDUnit a)"
-  assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
-  shows "P x"
-apply (induct x rule: pd_basis_induct1)
-apply (rule PDUnit, erule PDPlus [OF PDUnit])
-done
-
-subsection {* Fold operator *}
-
-definition
-  fold_pd ::
-    "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
-  where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
-
-lemma fold_pd_PDUnit:
-  assumes "class.ab_semigroup_idem_mult f"
-  shows "fold_pd g f (PDUnit x) = g x"
-unfolding fold_pd_def Rep_PDUnit by simp
-
-lemma fold_pd_PDPlus:
-  assumes "class.ab_semigroup_idem_mult f"
-  shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
-proof -
-  interpret ab_semigroup_idem_mult f by fact
-  show ?thesis unfolding fold_pd_def Rep_PDPlus
-    by (simp add: image_Un fold1_Un2)
-qed
-
-end
diff -r ffae1d9bad06 -r 6d66975b711f src/HOL/HOLCF/Compact_Basis.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Fri Dec 17 16:43:45 2010 -0800
@@ -0,0 +1,111 @@
+(*  Title:      HOLCF/Compact_Basis.thy
+    Author:     Brian Huffman
+*)
+
+header {* A compact basis for powerdomains *}
+
+theory Compact_Basis
+imports Bifinite
+begin
+
+default_sort "domain"
+
+subsection {* A compact basis for powerdomains *}
+
+typedef 'a pd_basis =
+  "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
+by (rule_tac x="{arbitrary}" in exI, simp)
+
+lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
+by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
+
+lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
+by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
+
+text {* The powerdomain basis type is countable. *}
+
+lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
+proof -
+  obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
+    using compact_basis.countable ..
+  hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B"
+    by (rule inj_image_eq_iff)
+  have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))"
+    by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
+  thus ?thesis by - (rule exI)
+  (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
+qed
+
+subsection {* Unit and plus constructors *}
+
+definition
+  PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
+  "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
+
+definition
+  PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
+  "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
+
+lemma Rep_PDUnit:
+  "Rep_pd_basis (PDUnit x) = {x}"
+unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
+
+lemma Rep_PDPlus:
+  "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
+unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
+
+lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
+unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
+
+lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
+unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
+
+lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
+unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
+
+lemma PDPlus_absorb: "PDPlus t t = t"
+unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
+
+lemma pd_basis_induct1:
+  assumes PDUnit: "\<And>a. P (PDUnit a)"
+  assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
+  shows "P x"
+apply (induct x, unfold pd_basis_def, clarify)
+apply (erule (1) finite_ne_induct)
+apply (cut_tac a=x in PDUnit)
+apply (simp add: PDUnit_def)
+apply (drule_tac a=x in PDPlus)
+apply (simp add: PDUnit_def PDPlus_def
+  Abs_pd_basis_inverse [unfolded pd_basis_def])
+done
+
+lemma pd_basis_induct:
+  assumes PDUnit: "\<And>a. P (PDUnit a)"
+  assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
+  shows "P x"
+apply (induct x rule: pd_basis_induct1)
+apply (rule PDUnit, erule PDPlus [OF PDUnit])
+done
+
+subsection {* Fold operator *}
+
+definition
+  fold_pd ::
+    "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
+  where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
+
+lemma fold_pd_PDUnit:
+  assumes "class.ab_semigroup_idem_mult f"
+  shows "fold_pd g f (PDUnit x) = g x"
+unfolding fold_pd_def Rep_PDUnit by simp
+
+lemma fold_pd_PDPlus:
+  assumes "class.ab_semigroup_idem_mult f"
+  shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
+proof -
+  interpret ab_semigroup_idem_mult f by fact
+  show ?thesis unfolding fold_pd_def Rep_PDPlus
+    by (simp add: image_Un fold1_Un2)
+qed
+
+end
diff -r ffae1d9bad06 -r 6d66975b711f src/HOL/HOLCF/IsaMakefile
--- a/src/HOL/HOLCF/IsaMakefile	Fri Dec 17 23:18:39 2010 +0100
+++ b/src/HOL/HOLCF/IsaMakefile	Fri Dec 17 16:43:45 2010 -0800
@@ -39,7 +39,7 @@
   Algebraic.thy \
   Bifinite.thy \
   Cfun.thy \
-  CompactBasis.thy \
+  Compact_Basis.thy \
   Completion.thy \
   Cont.thy \
   ConvexPD.thy \
diff -r ffae1d9bad06 -r 6d66975b711f src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Fri Dec 17 23:18:39 2010 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Fri Dec 17 16:43:45 2010 -0800
@@ -5,7 +5,7 @@
 header {* Lower powerdomain *}
 
 theory LowerPD
-imports CompactBasis
+imports Compact_Basis
 begin
 
 subsection {* Basis preorder *}
diff -r ffae1d9bad06 -r 6d66975b711f src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Fri Dec 17 23:18:39 2010 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Fri Dec 17 16:43:45 2010 -0800
@@ -5,7 +5,7 @@
 header {* Upper powerdomain *}
 
 theory UpperPD
-imports CompactBasis
+imports Compact_Basis
 begin
 
 subsection {* Basis preorder *}
diff -r ffae1d9bad06 -r 6d66975b711f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Dec 17 23:18:39 2010 +0100
+++ b/src/HOL/IsaMakefile	Fri Dec 17 16:43:45 2010 -0800
@@ -1406,7 +1406,7 @@
   HOLCF/Algebraic.thy \
   HOLCF/Bifinite.thy \
   HOLCF/Cfun.thy \
-  HOLCF/CompactBasis.thy \
+  HOLCF/Compact_Basis.thy \
   HOLCF/Completion.thy \
   HOLCF/Cont.thy \
   HOLCF/ConvexPD.thy \