# HG changeset patch # User huffman # Date 1286484883 25200 # Node ID 310f9858510780f754b6ca381d717b157338d7a4 # Parent 0300d5170622dad6d92175aed352c3fc088766f2 move stuff from Algebraic.thy to Bifinite.thy and elsewhere diff -r 0300d5170622 -r 310f98585107 src/HOLCF/Algebraic.thy --- a/src/HOLCF/Algebraic.thy Thu Oct 07 13:33:06 2010 -0700 +++ b/src/HOLCF/Algebraic.thy Thu Oct 07 13:54:43 2010 -0700 @@ -2,10 +2,10 @@ Author: Brian Huffman *) -header {* Algebraic deflations and SFP domains *} +header {* Algebraic deflations *} theory Algebraic -imports Universal Bifinite +imports Universal begin subsection {* Type constructor for finite deflations *} @@ -257,232 +257,4 @@ apply (simp add: in_sfp_def) done -subsection {* Class of SFP domains *} - -text {* - We define a SFP domain as a pcpo that is isomorphic to some - algebraic deflation over the universal domain. -*} - -class sfp = pcpo + - fixes emb :: "'a::pcpo \ udom" - fixes prj :: "udom \ 'a::pcpo" - fixes sfp :: "'a itself \ sfp" - assumes ep_pair_emb_prj: "ep_pair emb prj" - assumes cast_SFP: "cast\(sfp TYPE('a)) = emb oo prj" - -syntax "_SFP" :: "type \ sfp" ("(1SFP/(1'(_')))") -translations "SFP('t)" \ "CONST sfp TYPE('t)" - -interpretation sfp: - pcpo_ep_pair "emb :: 'a::sfp \ udom" "prj :: udom \ 'a::sfp" - unfolding pcpo_ep_pair_def - by (rule ep_pair_emb_prj) - -lemmas emb_inverse = sfp.e_inverse -lemmas emb_prj_below = sfp.e_p_below -lemmas emb_eq_iff = sfp.e_eq_iff -lemmas emb_strict = sfp.e_strict -lemmas prj_strict = sfp.p_strict - -subsection {* SFP domains have a countable compact basis *} - -text {* - Eventually it should be possible to generalize this to an unpointed - variant of the sfp class. -*} - -interpretation compact_basis: - ideal_completion below Rep_compact_basis "approximants::'a::sfp \ _" -proof - - obtain Y where Y: "\i. Y i \ Y (Suc i)" - and SFP: "SFP('a) = (\i. sfp_principal (Y i))" - by (rule sfp.obtain_principal_chain) - def approx \ "\i. (prj oo cast\(sfp_principal (Y i)) oo emb) :: 'a \ 'a" - interpret sfp_approx: approx_chain approx - proof (rule approx_chain.intro) - show "chain (\i. approx i)" - unfolding approx_def by (simp add: Y) - show "(\i. approx i) = ID" - unfolding approx_def - by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq) - show "\i. finite_deflation (approx i)" - unfolding approx_def - apply (rule sfp.finite_deflation_p_d_e) - apply (rule finite_deflation_cast) - apply (rule sfp.compact_principal) - apply (rule below_trans [OF monofun_cfun_fun]) - apply (rule is_ub_thelub, simp add: Y) - apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP) - done - qed - (* FIXME: why does show ?thesis fail here? *) - show "ideal_completion below Rep_compact_basis (approximants::'a \ _)" .. -qed - -subsection {* Type combinators *} - -definition - sfp_fun1 :: - "(nat \ 'a \ 'a) \ ((udom \ udom) \ ('a \ 'a)) \ (sfp \ sfp)" -where - "sfp_fun1 approx f = - sfp.basis_fun (\a. - sfp_principal (Abs_fin_defl - (udom_emb approx oo f\(Rep_fin_defl a) oo udom_prj approx)))" - -definition - sfp_fun2 :: - "(nat \ 'a \ 'a) \ ((udom \ udom) \ (udom \ udom) \ ('a \ 'a)) - \ (sfp \ sfp \ sfp)" -where - "sfp_fun2 approx f = - sfp.basis_fun (\a. - sfp.basis_fun (\b. - sfp_principal (Abs_fin_defl - (udom_emb approx oo - f\(Rep_fin_defl a)\(Rep_fin_defl b) oo udom_prj approx))))" - -lemma cast_sfp_fun1: - assumes approx: "approx_chain approx" - assumes f: "\a. finite_deflation a \ finite_deflation (f\a)" - shows "cast\(sfp_fun1 approx f\A) = udom_emb approx oo f\(cast\A) oo udom_prj approx" -proof - - have 1: "\a. finite_deflation - (udom_emb approx oo f\(Rep_fin_defl a) oo udom_prj approx)" - apply (rule ep_pair.finite_deflation_e_d_p) - apply (rule approx_chain.ep_pair_udom [OF approx]) - apply (rule f, rule finite_deflation_Rep_fin_defl) - done - show ?thesis - by (induct A rule: sfp.principal_induct, simp) - (simp only: sfp_fun1_def - sfp.basis_fun_principal - sfp.basis_fun_mono - sfp.principal_mono - Abs_fin_defl_mono [OF 1 1] - monofun_cfun below_refl - Rep_fin_defl_mono - cast_sfp_principal - Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) -qed - -lemma cast_sfp_fun2: - assumes approx: "approx_chain approx" - assumes f: "\a b. finite_deflation a \ finite_deflation b \ - finite_deflation (f\a\b)" - shows "cast\(sfp_fun2 approx f\A\B) = - udom_emb approx oo f\(cast\A)\(cast\B) oo udom_prj approx" -proof - - have 1: "\a b. finite_deflation (udom_emb approx oo - f\(Rep_fin_defl a)\(Rep_fin_defl b) oo udom_prj approx)" - apply (rule ep_pair.finite_deflation_e_d_p) - apply (rule ep_pair_udom [OF approx]) - apply (rule f, (rule finite_deflation_Rep_fin_defl)+) - done - show ?thesis - by (induct A B rule: sfp.principal_induct2, simp, simp) - (simp only: sfp_fun2_def - sfp.basis_fun_principal - sfp.basis_fun_mono - sfp.principal_mono - Abs_fin_defl_mono [OF 1 1] - monofun_cfun below_refl - Rep_fin_defl_mono - cast_sfp_principal - Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) -qed - -subsection {* Instance for universal domain type *} - -instantiation udom :: sfp -begin - -definition [simp]: - "emb = (ID :: udom \ udom)" - -definition [simp]: - "prj = (ID :: udom \ udom)" - -definition - "sfp (t::udom itself) = (\i. sfp_principal (Abs_fin_defl (udom_approx i)))" - -instance proof - show "ep_pair emb (prj :: udom \ udom)" - by (simp add: ep_pair.intro) -next - show "cast\SFP(udom) = emb oo (prj :: udom \ udom)" - unfolding sfp_udom_def - apply (subst contlub_cfun_arg) - apply (rule chainI) - apply (rule sfp.principal_mono) - apply (simp add: below_fin_defl_def) - apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) - apply (rule chainE) - apply (rule chain_udom_approx) - apply (subst cast_sfp_principal) - apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) - done -qed - end - -subsection {* Instance for continuous function space *} - -definition - cfun_approx :: "nat \ (udom \ udom) \ (udom \ udom)" -where - "cfun_approx = (\i. cfun_map\(udom_approx i)\(udom_approx i))" - -lemma cfun_approx: "approx_chain cfun_approx" -proof (rule approx_chain.intro) - show "chain (\i. cfun_approx i)" - unfolding cfun_approx_def by simp - show "(\i. cfun_approx i) = ID" - unfolding cfun_approx_def - by (simp add: lub_distribs cfun_map_ID) - show "\i. finite_deflation (cfun_approx i)" - unfolding cfun_approx_def - by (intro finite_deflation_cfun_map finite_deflation_udom_approx) -qed - -definition cfun_sfp :: "sfp \ sfp \ sfp" -where "cfun_sfp = sfp_fun2 cfun_approx cfun_map" - -lemma cast_cfun_sfp: - "cast\(cfun_sfp\A\B) = - udom_emb cfun_approx oo cfun_map\(cast\A)\(cast\B) oo udom_prj cfun_approx" -unfolding cfun_sfp_def -apply (rule cast_sfp_fun2 [OF cfun_approx]) -apply (erule (1) finite_deflation_cfun_map) -done - -instantiation cfun :: (sfp, sfp) sfp -begin - -definition - "emb = udom_emb cfun_approx oo cfun_map\prj\emb" - -definition - "prj = cfun_map\emb\prj oo udom_prj cfun_approx" - -definition - "sfp (t::('a \ 'b) itself) = cfun_sfp\SFP('a)\SFP('b)" - -instance proof - show "ep_pair emb (prj :: udom \ 'a \ 'b)" - unfolding emb_cfun_def prj_cfun_def - using ep_pair_udom [OF cfun_approx] - by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj) -next - show "cast\SFP('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" - unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp - by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map) -qed - -end - -lemma SFP_cfun: "SFP('a::sfp \ 'b::sfp) = cfun_sfp\SFP('a)\SFP('b)" -by (rule sfp_cfun_def) - -end diff -r 0300d5170622 -r 310f98585107 src/HOLCF/Bifinite.thy --- a/src/HOLCF/Bifinite.thy Thu Oct 07 13:33:06 2010 -0700 +++ b/src/HOLCF/Bifinite.thy Thu Oct 07 13:54:43 2010 -0700 @@ -2,172 +2,238 @@ Author: Brian Huffman *) -header {* Bifinite domains and approximation *} +header {* Bifinite domains *} theory Bifinite -imports Deflation +imports Algebraic begin -subsection {* Map operator for product type *} +subsection {* Class of SFP domains *} + +text {* + We define a SFP domain as a pcpo that is isomorphic to some + algebraic deflation over the universal domain. +*} + +class sfp = pcpo + + fixes emb :: "'a::pcpo \ udom" + fixes prj :: "udom \ 'a::pcpo" + fixes sfp :: "'a itself \ sfp" + assumes ep_pair_emb_prj: "ep_pair emb prj" + assumes cast_SFP: "cast\(sfp TYPE('a)) = emb oo prj" -definition - cprod_map :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" -where - "cprod_map = (\ f g p. (f\(fst p), g\(snd p)))" +syntax "_SFP" :: "type \ sfp" ("(1SFP/(1'(_')))") +translations "SFP('t)" \ "CONST sfp TYPE('t)" + +interpretation sfp: + pcpo_ep_pair "emb :: 'a::sfp \ udom" "prj :: udom \ 'a::sfp" + unfolding pcpo_ep_pair_def + by (rule ep_pair_emb_prj) -lemma cprod_map_Pair [simp]: "cprod_map\f\g\(x, y) = (f\x, g\y)" -unfolding cprod_map_def by simp +lemmas emb_inverse = sfp.e_inverse +lemmas emb_prj_below = sfp.e_p_below +lemmas emb_eq_iff = sfp.e_eq_iff +lemmas emb_strict = sfp.e_strict +lemmas prj_strict = sfp.p_strict -lemma cprod_map_ID: "cprod_map\ID\ID = ID" -unfolding expand_cfun_eq by auto +subsection {* SFP domains have a countable compact basis *} -lemma cprod_map_map: - "cprod_map\f1\g1\(cprod_map\f2\g2\p) = - cprod_map\(\ x. f1\(f2\x))\(\ x. g1\(g2\x))\p" -by (induct p) simp +text {* + Eventually it should be possible to generalize this to an unpointed + variant of the sfp class. +*} -lemma ep_pair_cprod_map: - assumes "ep_pair e1 p1" and "ep_pair e2 p2" - shows "ep_pair (cprod_map\e1\e2) (cprod_map\p1\p2)" -proof - interpret e1p1: ep_pair e1 p1 by fact - interpret e2p2: ep_pair e2 p2 by fact - fix x show "cprod_map\p1\p2\(cprod_map\e1\e2\x) = x" - by (induct x) simp - fix y show "cprod_map\e1\e2\(cprod_map\p1\p2\y) \ y" - by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below) +interpretation compact_basis: + ideal_completion below Rep_compact_basis "approximants::'a::sfp \ _" +proof - + obtain Y where Y: "\i. Y i \ Y (Suc i)" + and SFP: "SFP('a) = (\i. sfp_principal (Y i))" + by (rule sfp.obtain_principal_chain) + def approx \ "\i. (prj oo cast\(sfp_principal (Y i)) oo emb) :: 'a \ 'a" + interpret sfp_approx: approx_chain approx + proof (rule approx_chain.intro) + show "chain (\i. approx i)" + unfolding approx_def by (simp add: Y) + show "(\i. approx i) = ID" + unfolding approx_def + by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq) + show "\i. finite_deflation (approx i)" + unfolding approx_def + apply (rule sfp.finite_deflation_p_d_e) + apply (rule finite_deflation_cast) + apply (rule sfp.compact_principal) + apply (rule below_trans [OF monofun_cfun_fun]) + apply (rule is_ub_thelub, simp add: Y) + apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP) + done + qed + (* FIXME: why does show ?thesis fail here? *) + show "ideal_completion below Rep_compact_basis (approximants::'a \ _)" .. qed -lemma deflation_cprod_map: - assumes "deflation d1" and "deflation d2" - shows "deflation (cprod_map\d1\d2)" -proof - interpret d1: deflation d1 by fact - interpret d2: deflation d2 by fact - fix x - show "cprod_map\d1\d2\(cprod_map\d1\d2\x) = cprod_map\d1\d2\x" - by (induct x) (simp add: d1.idem d2.idem) - show "cprod_map\d1\d2\x \ x" - by (induct x) (simp add: d1.below d2.below) -qed +subsection {* Type combinators *} + +definition + sfp_fun1 :: + "(nat \ 'a \ 'a) \ ((udom \ udom) \ ('a \ 'a)) \ (sfp \ sfp)" +where + "sfp_fun1 approx f = + sfp.basis_fun (\a. + sfp_principal (Abs_fin_defl + (udom_emb approx oo f\(Rep_fin_defl a) oo udom_prj approx)))" + +definition + sfp_fun2 :: + "(nat \ 'a \ 'a) \ ((udom \ udom) \ (udom \ udom) \ ('a \ 'a)) + \ (sfp \ sfp \ sfp)" +where + "sfp_fun2 approx f = + sfp.basis_fun (\a. + sfp.basis_fun (\b. + sfp_principal (Abs_fin_defl + (udom_emb approx oo + f\(Rep_fin_defl a)\(Rep_fin_defl b) oo udom_prj approx))))" -lemma finite_deflation_cprod_map: - assumes "finite_deflation d1" and "finite_deflation d2" - shows "finite_deflation (cprod_map\d1\d2)" -proof (rule finite_deflation_intro) - interpret d1: finite_deflation d1 by fact - interpret d2: finite_deflation d2 by fact - have "deflation d1" and "deflation d2" by fact+ - thus "deflation (cprod_map\d1\d2)" by (rule deflation_cprod_map) - have "{p. cprod_map\d1\d2\p = p} \ {x. d1\x = x} \ {y. d2\y = y}" - by clarsimp - thus "finite {p. cprod_map\d1\d2\p = p}" - by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) +lemma cast_sfp_fun1: + assumes approx: "approx_chain approx" + assumes f: "\a. finite_deflation a \ finite_deflation (f\a)" + shows "cast\(sfp_fun1 approx f\A) = udom_emb approx oo f\(cast\A) oo udom_prj approx" +proof - + have 1: "\a. finite_deflation + (udom_emb approx oo f\(Rep_fin_defl a) oo udom_prj approx)" + apply (rule ep_pair.finite_deflation_e_d_p) + apply (rule approx_chain.ep_pair_udom [OF approx]) + apply (rule f, rule finite_deflation_Rep_fin_defl) + done + show ?thesis + by (induct A rule: sfp.principal_induct, simp) + (simp only: sfp_fun1_def + sfp.basis_fun_principal + sfp.basis_fun_mono + sfp.principal_mono + Abs_fin_defl_mono [OF 1 1] + monofun_cfun below_refl + Rep_fin_defl_mono + cast_sfp_principal + Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) qed -subsection {* Map operator for continuous function space *} +lemma cast_sfp_fun2: + assumes approx: "approx_chain approx" + assumes f: "\a b. finite_deflation a \ finite_deflation b \ + finite_deflation (f\a\b)" + shows "cast\(sfp_fun2 approx f\A\B) = + udom_emb approx oo f\(cast\A)\(cast\B) oo udom_prj approx" +proof - + have 1: "\a b. finite_deflation (udom_emb approx oo + f\(Rep_fin_defl a)\(Rep_fin_defl b) oo udom_prj approx)" + apply (rule ep_pair.finite_deflation_e_d_p) + apply (rule ep_pair_udom [OF approx]) + apply (rule f, (rule finite_deflation_Rep_fin_defl)+) + done + show ?thesis + by (induct A B rule: sfp.principal_induct2, simp, simp) + (simp only: sfp_fun2_def + sfp.basis_fun_principal + sfp.basis_fun_mono + sfp.principal_mono + Abs_fin_defl_mono [OF 1 1] + monofun_cfun below_refl + Rep_fin_defl_mono + cast_sfp_principal + Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) +qed + +subsection {* Instance for universal domain type *} + +instantiation udom :: sfp +begin + +definition [simp]: + "emb = (ID :: udom \ udom)" + +definition [simp]: + "prj = (ID :: udom \ udom)" definition - cfun_map :: "('b \ 'a) \ ('c \ 'd) \ ('a \ 'c) \ ('b \ 'd)" -where - "cfun_map = (\ a b f x. b\(f\(a\x)))" - -lemma cfun_map_beta [simp]: "cfun_map\a\b\f\x = b\(f\(a\x))" -unfolding cfun_map_def by simp - -lemma cfun_map_ID: "cfun_map\ID\ID = ID" -unfolding expand_cfun_eq by simp + "sfp (t::udom itself) = (\i. sfp_principal (Abs_fin_defl (udom_approx i)))" -lemma cfun_map_map: - "cfun_map\f1\g1\(cfun_map\f2\g2\p) = - cfun_map\(\ x. f2\(f1\x))\(\ x. g1\(g2\x))\p" -by (rule ext_cfun) simp - -lemma ep_pair_cfun_map: - assumes "ep_pair e1 p1" and "ep_pair e2 p2" - shows "ep_pair (cfun_map\p1\e2) (cfun_map\e1\p2)" -proof - interpret e1p1: ep_pair e1 p1 by fact - interpret e2p2: ep_pair e2 p2 by fact - fix f show "cfun_map\e1\p2\(cfun_map\p1\e2\f) = f" - by (simp add: expand_cfun_eq) - fix g show "cfun_map\p1\e2\(cfun_map\e1\p2\g) \ g" - apply (rule below_cfun_ext, simp) - apply (rule below_trans [OF e2p2.e_p_below]) - apply (rule monofun_cfun_arg) - apply (rule e1p1.e_p_below) +instance proof + show "ep_pair emb (prj :: udom \ udom)" + by (simp add: ep_pair.intro) +next + show "cast\SFP(udom) = emb oo (prj :: udom \ udom)" + unfolding sfp_udom_def + apply (subst contlub_cfun_arg) + apply (rule chainI) + apply (rule sfp.principal_mono) + apply (simp add: below_fin_defl_def) + apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) + apply (rule chainE) + apply (rule chain_udom_approx) + apply (subst cast_sfp_principal) + apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) done qed -lemma deflation_cfun_map: - assumes "deflation d1" and "deflation d2" - shows "deflation (cfun_map\d1\d2)" -proof - interpret d1: deflation d1 by fact - interpret d2: deflation d2 by fact - fix f - show "cfun_map\d1\d2\(cfun_map\d1\d2\f) = cfun_map\d1\d2\f" - by (simp add: expand_cfun_eq d1.idem d2.idem) - show "cfun_map\d1\d2\f \ f" - apply (rule below_cfun_ext, simp) - apply (rule below_trans [OF d2.below]) - apply (rule monofun_cfun_arg) - apply (rule d1.below) - done +end + +subsection {* Instance for continuous function space *} + +definition + cfun_approx :: "nat \ (udom \ udom) \ (udom \ udom)" +where + "cfun_approx = (\i. cfun_map\(udom_approx i)\(udom_approx i))" + +lemma cfun_approx: "approx_chain cfun_approx" +proof (rule approx_chain.intro) + show "chain (\i. cfun_approx i)" + unfolding cfun_approx_def by simp + show "(\i. cfun_approx i) = ID" + unfolding cfun_approx_def + by (simp add: lub_distribs cfun_map_ID) + show "\i. finite_deflation (cfun_approx i)" + unfolding cfun_approx_def + by (intro finite_deflation_cfun_map finite_deflation_udom_approx) qed -lemma finite_range_cfun_map: - assumes a: "finite (range (\x. a\x))" - assumes b: "finite (range (\y. b\y))" - shows "finite (range (\f. cfun_map\a\b\f))" (is "finite (range ?h)") -proof (rule finite_imageD) - let ?f = "\g. range (\x. (a\x, g\x))" - show "finite (?f ` range ?h)" - proof (rule finite_subset) - let ?B = "Pow (range (\x. a\x) \ range (\y. b\y))" - show "?f ` range ?h \ ?B" - by clarsimp - show "finite ?B" - by (simp add: a b) - qed - show "inj_on ?f (range ?h)" - proof (rule inj_onI, rule ext_cfun, clarsimp) - fix x f g - assume "range (\x. (a\x, b\(f\(a\x)))) = range (\x. (a\x, b\(g\(a\x))))" - hence "range (\x. (a\x, b\(f\(a\x)))) \ range (\x. (a\x, b\(g\(a\x))))" - by (rule equalityD1) - hence "(a\x, b\(f\(a\x))) \ range (\x. (a\x, b\(g\(a\x))))" - by (simp add: subset_eq) - then obtain y where "(a\x, b\(f\(a\x))) = (a\y, b\(g\(a\y)))" - by (rule rangeE) - thus "b\(f\(a\x)) = b\