--- a/src/HOLCF/HOLCF.thy Mon May 24 12:10:24 2010 -0700
+++ b/src/HOLCF/HOLCF.thy Mon May 24 12:42:17 2010 -0700
@@ -9,7 +9,6 @@
Main
Domain
Powerdomains
- Sum_Cpo
begin
default_sort pcpo
--- a/src/HOLCF/IsaMakefile Mon May 24 12:10:24 2010 -0700
+++ b/src/HOLCF/IsaMakefile Mon May 24 12:42:17 2010 -0700
@@ -58,7 +58,6 @@
Representable.thy \
Sprod.thy \
Ssum.thy \
- Sum_Cpo.thy \
Tr.thy \
Universal.thy \
UpperPD.thy \
@@ -100,6 +99,7 @@
$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
Library/Stream.thy \
Library/Strict_Fun.thy \
+ Library/Sum_Cpo.thy \
Library/HOLCF_Library.thy \
Library/ROOT.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
--- a/src/HOLCF/Library/HOLCF_Library.thy Mon May 24 12:10:24 2010 -0700
+++ b/src/HOLCF/Library/HOLCF_Library.thy Mon May 24 12:42:17 2010 -0700
@@ -2,6 +2,7 @@
imports
Stream
Strict_Fun
+ Sum_Cpo
begin
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Library/Sum_Cpo.thy Mon May 24 12:42:17 2010 -0700
@@ -0,0 +1,265 @@
+(* Title: HOLCF/Sum_Cpo.thy
+ Author: Brian Huffman
+*)
+
+header {* The cpo of disjoint sums *}
+
+theory Sum_Cpo
+imports Bifinite
+begin
+
+subsection {* Ordering on sum type *}
+
+instantiation "+" :: (below, below) below
+begin
+
+definition below_sum_def:
+ "x \<sqsubseteq> y \<equiv> case x of
+ Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
+ Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
+
+instance ..
+end
+
+lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
+unfolding below_sum_def by simp
+
+lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
+unfolding below_sum_def by simp
+
+lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
+unfolding below_sum_def by simp
+
+lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
+unfolding below_sum_def by simp
+
+lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
+by simp
+
+lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
+by simp
+
+lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+by (cases x, simp_all)
+
+lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+by (cases x, simp_all)
+
+lemmas sum_below_elims = Inl_belowE Inr_belowE
+
+lemma sum_below_cases:
+ "\<lbrakk>x \<sqsubseteq> y;
+ \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
+ \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
+ \<Longrightarrow> R"
+by (cases x, safe elim!: sum_below_elims, auto)
+
+subsection {* Sum type is a complete partial order *}
+
+instance "+" :: (po, po) po
+proof
+ fix x :: "'a + 'b"
+ show "x \<sqsubseteq> x"
+ by (induct x, simp_all)
+next
+ fix x y :: "'a + 'b"
+ assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
+ by (induct x, auto elim!: sum_below_elims intro: below_antisym)
+next
+ fix x y z :: "'a + 'b"
+ assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
+ by (induct x, auto elim!: sum_below_elims intro: below_trans)
+qed
+
+lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
+by (rule monofunI, erule sum_below_cases, simp_all)
+
+lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
+by (rule monofunI, erule sum_below_cases, simp_all)
+
+lemma sum_chain_cases:
+ assumes Y: "chain Y"
+ assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R"
+ assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R"
+ shows "R"
+ apply (cases "Y 0")
+ apply (rule A)
+ apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
+ apply (rule ext)
+ apply (cut_tac j=i in chain_mono [OF Y le0], simp)
+ apply (erule Inl_belowE, simp)
+ apply (rule B)
+ apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
+ apply (rule ext)
+ apply (cut_tac j=i in chain_mono [OF Y le0], simp)
+ apply (erule Inr_belowE, simp)
+done
+
+lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
+ apply (rule is_lubI)
+ apply (rule ub_rangeI)
+ apply (simp add: is_ub_lub)
+ apply (frule ub_rangeD [where i=arbitrary])
+ apply (erule Inl_belowE, simp)
+ apply (erule is_lub_lub)
+ apply (rule ub_rangeI)
+ apply (drule ub_rangeD, simp)
+done
+
+lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
+ apply (rule is_lubI)
+ apply (rule ub_rangeI)
+ apply (simp add: is_ub_lub)
+ apply (frule ub_rangeD [where i=arbitrary])
+ apply (erule Inr_belowE, simp)
+ apply (erule is_lub_lub)
+ apply (rule ub_rangeI)
+ apply (drule ub_rangeD, simp)
+done
+
+instance "+" :: (cpo, cpo) cpo
+ apply intro_classes
+ apply (erule sum_chain_cases, safe)
+ apply (rule exI)
+ apply (rule is_lub_Inl)
+ apply (erule cpo_lubI)
+ apply (rule exI)
+ apply (rule is_lub_Inr)
+ apply (erule cpo_lubI)
+done
+
+subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *}
+
+lemma cont_Inl: "cont Inl"
+by (intro contI is_lub_Inl cpo_lubI)
+
+lemma cont_Inr: "cont Inr"
+by (intro contI is_lub_Inr cpo_lubI)
+
+lemmas cont2cont_Inl [simp, cont2cont] = cont_compose [OF cont_Inl]
+lemmas cont2cont_Inr [simp, cont2cont] = cont_compose [OF cont_Inr]
+
+lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
+lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
+
+lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
+lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
+
+lemma cont_sum_case1:
+ assumes f: "\<And>a. cont (\<lambda>x. f x a)"
+ assumes g: "\<And>b. cont (\<lambda>x. g x b)"
+ shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
+by (induct y, simp add: f, simp add: g)
+
+lemma cont_sum_case2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (sum_case f g)"
+apply (rule contI)
+apply (erule sum_chain_cases)
+apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
+apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
+done
+
+lemma cont2cont_sum_case:
+ assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
+ assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
+ assumes h: "cont (\<lambda>x. h x)"
+ shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
+apply (rule cont_apply [OF h])
+apply (rule cont_sum_case2 [OF f2 g2])
+apply (rule cont_sum_case1 [OF f1 g1])
+done
+
+lemma cont2cont_sum_case' [simp, cont2cont]:
+ assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
+ assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
+ assumes h: "cont (\<lambda>x. h x)"
+ shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
+proof -
+ note f1 = f [THEN cont_fst_snd_D1]
+ note f2 = f [THEN cont_fst_snd_D2]
+ note g1 = g [THEN cont_fst_snd_D1]
+ note g2 = g [THEN cont_fst_snd_D2]
+ show ?thesis
+ apply (rule cont_apply [OF h])
+ apply (rule cont_sum_case2 [OF f2 g2])
+ apply (rule cont_sum_case1 [OF f1 g1])
+ done
+qed
+
+subsection {* Compactness and chain-finiteness *}
+
+lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
+apply (rule compactI2)
+apply (erule sum_chain_cases, safe)
+apply (simp add: lub_Inl)
+apply (erule (2) compactD2)
+apply (simp add: lub_Inr)
+done
+
+lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)"
+apply (rule compactI2)
+apply (erule sum_chain_cases, safe)
+apply (simp add: lub_Inl)
+apply (simp add: lub_Inr)
+apply (erule (2) compactD2)
+done
+
+lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a"
+unfolding compact_def
+by (drule adm_subst [OF cont_Inl], simp)
+
+lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a"
+unfolding compact_def
+by (drule adm_subst [OF cont_Inr], simp)
+
+lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a"
+by (safe elim!: compact_Inl compact_Inl_rev)
+
+lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
+by (safe elim!: compact_Inr compact_Inr_rev)
+
+instance "+" :: (chfin, chfin) chfin
+apply intro_classes
+apply (erule compact_imp_max_in_chain)
+apply (case_tac "\<Squnion>i. Y i", simp_all)
+done
+
+instance "+" :: (finite_po, finite_po) finite_po ..
+
+instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
+by intro_classes (simp add: below_sum_def split: sum.split)
+
+subsection {* Sum type is a bifinite domain *}
+
+instantiation "+" :: (profinite, profinite) profinite
+begin
+
+definition
+ approx_sum_def: "approx =
+ (\<lambda>n. \<Lambda> x. case x of Inl a \<Rightarrow> Inl (approx n\<cdot>a) | Inr b \<Rightarrow> Inr (approx n\<cdot>b))"
+
+lemma approx_Inl [simp]: "approx n\<cdot>(Inl x) = Inl (approx n\<cdot>x)"
+ unfolding approx_sum_def by simp
+
+lemma approx_Inr [simp]: "approx n\<cdot>(Inr x) = Inr (approx n\<cdot>x)"
+ unfolding approx_sum_def by simp
+
+instance proof
+ fix i :: nat and x :: "'a + 'b"
+ show "chain (approx :: nat \<Rightarrow> 'a + 'b \<rightarrow> 'a + 'b)"
+ unfolding approx_sum_def
+ by (rule ch2ch_LAM, case_tac x, simp_all)
+ show "(\<Squnion>i. approx i\<cdot>x) = x"
+ by (induct x, simp_all add: lub_Inl lub_Inr)
+ show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+ by (induct x, simp_all)
+ have "{x::'a + 'b. approx i\<cdot>x = x} \<subseteq>
+ {x::'a. approx i\<cdot>x = x} <+> {x::'b. approx i\<cdot>x = x}"
+ by (rule subsetI, case_tac x, simp_all add: InlI InrI)
+ thus "finite {x::'a + 'b. approx i\<cdot>x = x}"
+ by (rule finite_subset,
+ intro finite_Plus finite_fixes_approx)
+qed
+
+end
+
+end
--- a/src/HOLCF/Sum_Cpo.thy Mon May 24 12:10:24 2010 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,265 +0,0 @@
-(* Title: HOLCF/Sum_Cpo.thy
- Author: Brian Huffman
-*)
-
-header {* The cpo of disjoint sums *}
-
-theory Sum_Cpo
-imports Bifinite
-begin
-
-subsection {* Ordering on sum type *}
-
-instantiation "+" :: (below, below) below
-begin
-
-definition below_sum_def:
- "x \<sqsubseteq> y \<equiv> case x of
- Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
- Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
-
-instance ..
-end
-
-lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
-unfolding below_sum_def by simp
-
-lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
-unfolding below_sum_def by simp
-
-lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
-unfolding below_sum_def by simp
-
-lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
-unfolding below_sum_def by simp
-
-lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
-by simp
-
-lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
-by simp
-
-lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-by (cases x, simp_all)
-
-lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-by (cases x, simp_all)
-
-lemmas sum_below_elims = Inl_belowE Inr_belowE
-
-lemma sum_below_cases:
- "\<lbrakk>x \<sqsubseteq> y;
- \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
- \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
- \<Longrightarrow> R"
-by (cases x, safe elim!: sum_below_elims, auto)
-
-subsection {* Sum type is a complete partial order *}
-
-instance "+" :: (po, po) po
-proof
- fix x :: "'a + 'b"
- show "x \<sqsubseteq> x"
- by (induct x, simp_all)
-next
- fix x y :: "'a + 'b"
- assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
- by (induct x, auto elim!: sum_below_elims intro: below_antisym)
-next
- fix x y z :: "'a + 'b"
- assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
- by (induct x, auto elim!: sum_below_elims intro: below_trans)
-qed
-
-lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
-by (rule monofunI, erule sum_below_cases, simp_all)
-
-lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
-by (rule monofunI, erule sum_below_cases, simp_all)
-
-lemma sum_chain_cases:
- assumes Y: "chain Y"
- assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R"
- assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R"
- shows "R"
- apply (cases "Y 0")
- apply (rule A)
- apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
- apply (rule ext)
- apply (cut_tac j=i in chain_mono [OF Y le0], simp)
- apply (erule Inl_belowE, simp)
- apply (rule B)
- apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
- apply (rule ext)
- apply (cut_tac j=i in chain_mono [OF Y le0], simp)
- apply (erule Inr_belowE, simp)
-done
-
-lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
- apply (rule is_lubI)
- apply (rule ub_rangeI)
- apply (simp add: is_ub_lub)
- apply (frule ub_rangeD [where i=arbitrary])
- apply (erule Inl_belowE, simp)
- apply (erule is_lub_lub)
- apply (rule ub_rangeI)
- apply (drule ub_rangeD, simp)
-done
-
-lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
- apply (rule is_lubI)
- apply (rule ub_rangeI)
- apply (simp add: is_ub_lub)
- apply (frule ub_rangeD [where i=arbitrary])
- apply (erule Inr_belowE, simp)
- apply (erule is_lub_lub)
- apply (rule ub_rangeI)
- apply (drule ub_rangeD, simp)
-done
-
-instance "+" :: (cpo, cpo) cpo
- apply intro_classes
- apply (erule sum_chain_cases, safe)
- apply (rule exI)
- apply (rule is_lub_Inl)
- apply (erule cpo_lubI)
- apply (rule exI)
- apply (rule is_lub_Inr)
- apply (erule cpo_lubI)
-done
-
-subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *}
-
-lemma cont_Inl: "cont Inl"
-by (intro contI is_lub_Inl cpo_lubI)
-
-lemma cont_Inr: "cont Inr"
-by (intro contI is_lub_Inr cpo_lubI)
-
-lemmas cont2cont_Inl [simp, cont2cont] = cont_compose [OF cont_Inl]
-lemmas cont2cont_Inr [simp, cont2cont] = cont_compose [OF cont_Inr]
-
-lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
-lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
-
-lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
-lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
-
-lemma cont_sum_case1:
- assumes f: "\<And>a. cont (\<lambda>x. f x a)"
- assumes g: "\<And>b. cont (\<lambda>x. g x b)"
- shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
-by (induct y, simp add: f, simp add: g)
-
-lemma cont_sum_case2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (sum_case f g)"
-apply (rule contI)
-apply (erule sum_chain_cases)
-apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
-apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
-done
-
-lemma cont2cont_sum_case:
- assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
- assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
- assumes h: "cont (\<lambda>x. h x)"
- shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
-apply (rule cont_apply [OF h])
-apply (rule cont_sum_case2 [OF f2 g2])
-apply (rule cont_sum_case1 [OF f1 g1])
-done
-
-lemma cont2cont_sum_case' [simp, cont2cont]:
- assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
- assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
- assumes h: "cont (\<lambda>x. h x)"
- shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
-proof -
- note f1 = f [THEN cont_fst_snd_D1]
- note f2 = f [THEN cont_fst_snd_D2]
- note g1 = g [THEN cont_fst_snd_D1]
- note g2 = g [THEN cont_fst_snd_D2]
- show ?thesis
- apply (rule cont_apply [OF h])
- apply (rule cont_sum_case2 [OF f2 g2])
- apply (rule cont_sum_case1 [OF f1 g1])
- done
-qed
-
-subsection {* Compactness and chain-finiteness *}
-
-lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
-apply (rule compactI2)
-apply (erule sum_chain_cases, safe)
-apply (simp add: lub_Inl)
-apply (erule (2) compactD2)
-apply (simp add: lub_Inr)
-done
-
-lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)"
-apply (rule compactI2)
-apply (erule sum_chain_cases, safe)
-apply (simp add: lub_Inl)
-apply (simp add: lub_Inr)
-apply (erule (2) compactD2)
-done
-
-lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a"
-unfolding compact_def
-by (drule adm_subst [OF cont_Inl], simp)
-
-lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a"
-unfolding compact_def
-by (drule adm_subst [OF cont_Inr], simp)
-
-lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a"
-by (safe elim!: compact_Inl compact_Inl_rev)
-
-lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
-by (safe elim!: compact_Inr compact_Inr_rev)
-
-instance "+" :: (chfin, chfin) chfin
-apply intro_classes
-apply (erule compact_imp_max_in_chain)
-apply (case_tac "\<Squnion>i. Y i", simp_all)
-done
-
-instance "+" :: (finite_po, finite_po) finite_po ..
-
-instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: below_sum_def split: sum.split)
-
-subsection {* Sum type is a bifinite domain *}
-
-instantiation "+" :: (profinite, profinite) profinite
-begin
-
-definition
- approx_sum_def: "approx =
- (\<lambda>n. \<Lambda> x. case x of Inl a \<Rightarrow> Inl (approx n\<cdot>a) | Inr b \<Rightarrow> Inr (approx n\<cdot>b))"
-
-lemma approx_Inl [simp]: "approx n\<cdot>(Inl x) = Inl (approx n\<cdot>x)"
- unfolding approx_sum_def by simp
-
-lemma approx_Inr [simp]: "approx n\<cdot>(Inr x) = Inr (approx n\<cdot>x)"
- unfolding approx_sum_def by simp
-
-instance proof
- fix i :: nat and x :: "'a + 'b"
- show "chain (approx :: nat \<Rightarrow> 'a + 'b \<rightarrow> 'a + 'b)"
- unfolding approx_sum_def
- by (rule ch2ch_LAM, case_tac x, simp_all)
- show "(\<Squnion>i. approx i\<cdot>x) = x"
- by (induct x, simp_all add: lub_Inl lub_Inr)
- show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
- by (induct x, simp_all)
- have "{x::'a + 'b. approx i\<cdot>x = x} \<subseteq>
- {x::'a. approx i\<cdot>x = x} <+> {x::'b. approx i\<cdot>x = x}"
- by (rule subsetI, case_tac x, simp_all add: InlI InrI)
- thus "finite {x::'a + 'b. approx i\<cdot>x = x}"
- by (rule finite_subset,
- intro finite_Plus finite_fixes_approx)
-qed
-
-end
-
-end