# HG changeset patch # User huffman # Date 1231986163 28800 # Node ID 247e4c816004b32e637943a9d8790eba7978e1f9 # Parent 7f4a32134447daa6706f8e819b569b9beab07f37 rename Dsum.thy to Sum_Cpo.thy diff -r 7f4a32134447 -r 247e4c816004 src/HOLCF/Dsum.thy --- a/src/HOLCF/Dsum.thy Wed Jan 14 18:18:48 2009 -0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,251 +0,0 @@ -(* Title: HOLCF/Dsum.thy - Author: Brian Huffman -*) - -header {* The cpo of disjoint sums *} - -theory Dsum -imports Bifinite -begin - -subsection {* Ordering on type @{typ "'a + 'b"} *} - -instantiation "+" :: (sq_ord, sq_ord) sq_ord -begin - -definition - less_sum_def: "x \ y \ case x of - Inl a \ (case y of Inl b \ a \ b | Inr b \ False) | - Inr a \ (case y of Inl b \ False | Inr b \ a \ b)" - -instance .. -end - -lemma Inl_less_iff [simp]: "Inl x \ Inl y = x \ y" -unfolding less_sum_def by simp - -lemma Inr_less_iff [simp]: "Inr x \ Inr y = x \ y" -unfolding less_sum_def by simp - -lemma Inl_less_Inr [simp]: "\ Inl x \ Inr y" -unfolding less_sum_def by simp - -lemma Inr_less_Inl [simp]: "\ Inr x \ Inl y" -unfolding less_sum_def by simp - -lemma Inl_mono: "x \ y \ Inl x \ Inl y" -by simp - -lemma Inr_mono: "x \ y \ Inr x \ Inr y" -by simp - -lemma Inl_lessE: "\Inl a \ x; \b. \x = Inl b; a \ b\ \ R\ \ R" -by (cases x, simp_all) - -lemma Inr_lessE: "\Inr a \ x; \b. \x = Inr b; a \ b\ \ R\ \ R" -by (cases x, simp_all) - -lemmas sum_less_elims = Inl_lessE Inr_lessE - -lemma sum_less_cases: - "\x \ y; - \a b. \x = Inl a; y = Inl b; a \ b\ \ R; - \a b. \x = Inr a; y = Inr b; a \ b\ \ R\ - \ R" -by (cases x, safe elim!: sum_less_elims, auto) - -subsection {* Sum type is a complete partial order *} - -instance "+" :: (po, po) po -proof - fix x :: "'a + 'b" - show "x \ x" - by (induct x, simp_all) -next - fix x y :: "'a + 'b" - assume "x \ y" and "y \ x" thus "x = y" - by (induct x, auto elim!: sum_less_elims intro: antisym_less) -next - fix x y z :: "'a + 'b" - assume "x \ y" and "y \ z" thus "x \ z" - by (induct x, auto elim!: sum_less_elims intro: trans_less) -qed - -lemma monofun_inv_Inl: "monofun (\p. THE a. p = Inl a)" -by (rule monofunI, erule sum_less_cases, simp_all) - -lemma monofun_inv_Inr: "monofun (\p. THE b. p = Inr b)" -by (rule monofunI, erule sum_less_cases, simp_all) - -lemma sum_chain_cases: - assumes Y: "chain Y" - assumes A: "\A. \chain A; Y = (\i. Inl (A i))\ \ R" - assumes B: "\B. \chain B; Y = (\i. Inr (B i))\ \ 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_lessE, 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_lessE, simp) -done - -lemma is_lub_Inl: "range S <<| x \ range (\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_lessE, simp) - apply (erule is_lub_lub) - apply (rule ub_rangeI) - apply (drule ub_rangeD, simp) -done - -lemma is_lub_Inr: "range S <<| x \ range (\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_lessE, 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 @{term Inl}, @{term Inr}, @{term sum_case} *} - -lemma cont2cont_Inl [simp]: "cont f \ cont (\x. Inl (f x))" -by (fast intro: contI is_lub_Inl elim: contE) - -lemma cont2cont_Inr [simp]: "cont f \ cont (\x. Inr (f x))" -by (fast intro: contI is_lub_Inr elim: contE) - -lemma cont_Inl: "cont Inl" -by (rule cont2cont_Inl [OF cont_id]) - -lemma cont_Inr: "cont Inr" -by (rule cont2cont_Inr [OF cont_id]) - -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: "\a. cont (\x. f x a)" - assumes g: "\b. cont (\x. g x b)" - shows "cont (\x. case y of Inl a \ f x a | Inr b \ g x b)" -by (induct y, simp add: f, simp add: g) - -lemma cont_sum_case2: "\cont f; cont g\ \ 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 [simp]: - assumes f1: "\a. cont (\x. f x a)" and f2: "\x. cont (\a. f x a)" - assumes g1: "\b. cont (\x. g x b)" and g2: "\x. cont (\b. g x b)" - assumes h: "cont (\x. h x)" - shows "cont (\x. case h x of Inl a \ f x a | Inr b \ g x b)" -apply (rule cont2cont_app2 [OF cont2cont_lambda _ h]) -apply (rule cont_sum_case1 [OF f1 g1]) -apply (rule cont_sum_case2 [OF f2 g2]) -done - -subsection {* Compactness and chain-finiteness *} - -lemma compact_Inl: "compact a \ 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 \ 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) \ compact a" -unfolding compact_def -by (drule adm_subst [OF cont_Inl], simp) - -lemma compact_Inr_rev: "compact (Inr a) \ 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 "\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: less_sum_def split: sum.split) - -subsection {* Sum type is a bifinite domain *} - -instantiation "+" :: (profinite, profinite) profinite -begin - -definition - approx_sum_def: "approx = - (\n. \ x. case x of Inl a \ Inl (approx n\a) | Inr b \ Inr (approx n\b))" - -lemma approx_Inl [simp]: "approx n\(Inl x) = Inl (approx n\x)" - unfolding approx_sum_def by simp - -lemma approx_Inr [simp]: "approx n\(Inr x) = Inr (approx n\x)" - unfolding approx_sum_def by simp - -instance proof - fix i :: nat and x :: "'a + 'b" - show "chain (approx :: nat \ 'a + 'b \ 'a + 'b)" - unfolding approx_sum_def - by (rule ch2ch_LAM, case_tac x, simp_all) - show "(\i. approx i\x) = x" - by (induct x, simp_all add: lub_Inl lub_Inr) - show "approx i\(approx i\x) = approx i\x" - by (induct x, simp_all) - have "{x::'a + 'b. approx i\x = x} \ - {x::'a. approx i\x = x} <+> {x::'b. approx i\x = x}" - by (rule subsetI, case_tac x, simp_all add: InlI InrI) - thus "finite {x::'a + 'b. approx i\x = x}" - by (rule finite_subset, - intro finite_Plus finite_fixes_approx) -qed - -end - -end diff -r 7f4a32134447 -r 247e4c816004 src/HOLCF/HOLCF.thy --- a/src/HOLCF/HOLCF.thy Wed Jan 14 18:18:48 2009 -0800 +++ b/src/HOLCF/HOLCF.thy Wed Jan 14 18:22:43 2009 -0800 @@ -6,7 +6,7 @@ theory HOLCF imports - Domain ConvexPD Algebraic Universal Dsum Main + Domain ConvexPD Algebraic Universal Sum_Cpo Main uses "holcf_logic.ML" "Tools/cont_consts.ML" diff -r 7f4a32134447 -r 247e4c816004 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Wed Jan 14 18:18:48 2009 -0800 +++ b/src/HOLCF/IsaMakefile Wed Jan 14 18:22:43 2009 -0800 @@ -39,7 +39,6 @@ Discrete.thy \ Deflation.thy \ Domain.thy \ - Dsum.thy \ Eventual.thy \ Ffun.thy \ Fixrec.thy \ @@ -55,6 +54,7 @@ Product_Cpo.thy \ Sprod.thy \ Ssum.thy \ + Sum_Cpo.thy \ Tr.thy \ Universal.thy \ UpperPD.thy \ diff -r 7f4a32134447 -r 247e4c816004 src/HOLCF/Sum_Cpo.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Sum_Cpo.thy Wed Jan 14 18:22:43 2009 -0800 @@ -0,0 +1,251 @@ +(* Title: HOLCF/Sum_Cpo.thy + Author: Brian Huffman +*) + +header {* The cpo of disjoint sums *} + +theory Sum_Cpo +imports Bifinite +begin + +subsection {* Ordering on type @{typ "'a + 'b"} *} + +instantiation "+" :: (sq_ord, sq_ord) sq_ord +begin + +definition + less_sum_def: "x \ y \ case x of + Inl a \ (case y of Inl b \ a \ b | Inr b \ False) | + Inr a \ (case y of Inl b \ False | Inr b \ a \ b)" + +instance .. +end + +lemma Inl_less_iff [simp]: "Inl x \ Inl y = x \ y" +unfolding less_sum_def by simp + +lemma Inr_less_iff [simp]: "Inr x \ Inr y = x \ y" +unfolding less_sum_def by simp + +lemma Inl_less_Inr [simp]: "\ Inl x \ Inr y" +unfolding less_sum_def by simp + +lemma Inr_less_Inl [simp]: "\ Inr x \ Inl y" +unfolding less_sum_def by simp + +lemma Inl_mono: "x \ y \ Inl x \ Inl y" +by simp + +lemma Inr_mono: "x \ y \ Inr x \ Inr y" +by simp + +lemma Inl_lessE: "\Inl a \ x; \b. \x = Inl b; a \ b\ \ R\ \ R" +by (cases x, simp_all) + +lemma Inr_lessE: "\Inr a \ x; \b. \x = Inr b; a \ b\ \ R\ \ R" +by (cases x, simp_all) + +lemmas sum_less_elims = Inl_lessE Inr_lessE + +lemma sum_less_cases: + "\x \ y; + \a b. \x = Inl a; y = Inl b; a \ b\ \ R; + \a b. \x = Inr a; y = Inr b; a \ b\ \ R\ + \ R" +by (cases x, safe elim!: sum_less_elims, auto) + +subsection {* Sum type is a complete partial order *} + +instance "+" :: (po, po) po +proof + fix x :: "'a + 'b" + show "x \ x" + by (induct x, simp_all) +next + fix x y :: "'a + 'b" + assume "x \ y" and "y \ x" thus "x = y" + by (induct x, auto elim!: sum_less_elims intro: antisym_less) +next + fix x y z :: "'a + 'b" + assume "x \ y" and "y \ z" thus "x \ z" + by (induct x, auto elim!: sum_less_elims intro: trans_less) +qed + +lemma monofun_inv_Inl: "monofun (\p. THE a. p = Inl a)" +by (rule monofunI, erule sum_less_cases, simp_all) + +lemma monofun_inv_Inr: "monofun (\p. THE b. p = Inr b)" +by (rule monofunI, erule sum_less_cases, simp_all) + +lemma sum_chain_cases: + assumes Y: "chain Y" + assumes A: "\A. \chain A; Y = (\i. Inl (A i))\ \ R" + assumes B: "\B. \chain B; Y = (\i. Inr (B i))\ \ 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_lessE, 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_lessE, simp) +done + +lemma is_lub_Inl: "range S <<| x \ range (\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_lessE, simp) + apply (erule is_lub_lub) + apply (rule ub_rangeI) + apply (drule ub_rangeD, simp) +done + +lemma is_lub_Inr: "range S <<| x \ range (\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_lessE, 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 @{term Inl}, @{term Inr}, @{term sum_case} *} + +lemma cont2cont_Inl [simp]: "cont f \ cont (\x. Inl (f x))" +by (fast intro: contI is_lub_Inl elim: contE) + +lemma cont2cont_Inr [simp]: "cont f \ cont (\x. Inr (f x))" +by (fast intro: contI is_lub_Inr elim: contE) + +lemma cont_Inl: "cont Inl" +by (rule cont2cont_Inl [OF cont_id]) + +lemma cont_Inr: "cont Inr" +by (rule cont2cont_Inr [OF cont_id]) + +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: "\a. cont (\x. f x a)" + assumes g: "\b. cont (\x. g x b)" + shows "cont (\x. case y of Inl a \ f x a | Inr b \ g x b)" +by (induct y, simp add: f, simp add: g) + +lemma cont_sum_case2: "\cont f; cont g\ \ 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 [simp]: + assumes f1: "\a. cont (\x. f x a)" and f2: "\x. cont (\a. f x a)" + assumes g1: "\b. cont (\x. g x b)" and g2: "\x. cont (\b. g x b)" + assumes h: "cont (\x. h x)" + shows "cont (\x. case h x of Inl a \ f x a | Inr b \ g x b)" +apply (rule cont2cont_app2 [OF cont2cont_lambda _ h]) +apply (rule cont_sum_case1 [OF f1 g1]) +apply (rule cont_sum_case2 [OF f2 g2]) +done + +subsection {* Compactness and chain-finiteness *} + +lemma compact_Inl: "compact a \ 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 \ 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) \ compact a" +unfolding compact_def +by (drule adm_subst [OF cont_Inl], simp) + +lemma compact_Inr_rev: "compact (Inr a) \ 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 "\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: less_sum_def split: sum.split) + +subsection {* Sum type is a bifinite domain *} + +instantiation "+" :: (profinite, profinite) profinite +begin + +definition + approx_sum_def: "approx = + (\n. \ x. case x of Inl a \ Inl (approx n\a) | Inr b \ Inr (approx n\b))" + +lemma approx_Inl [simp]: "approx n\(Inl x) = Inl (approx n\x)" + unfolding approx_sum_def by simp + +lemma approx_Inr [simp]: "approx n\(Inr x) = Inr (approx n\x)" + unfolding approx_sum_def by simp + +instance proof + fix i :: nat and x :: "'a + 'b" + show "chain (approx :: nat \ 'a + 'b \ 'a + 'b)" + unfolding approx_sum_def + by (rule ch2ch_LAM, case_tac x, simp_all) + show "(\i. approx i\x) = x" + by (induct x, simp_all add: lub_Inl lub_Inr) + show "approx i\(approx i\x) = approx i\x" + by (induct x, simp_all) + have "{x::'a + 'b. approx i\x = x} \ + {x::'a. approx i\x = x} <+> {x::'b. approx i\x = x}" + by (rule subsetI, case_tac x, simp_all add: InlI InrI) + thus "finite {x::'a + 'b. approx i\x = x}" + by (rule finite_subset, + intro finite_Plus finite_fixes_approx) +qed + +end + +end