# HG changeset patch # User huffman # Date 1286387367 25200 # Node ID b525988432e93b9aea9f539206756f91026e3f05 # Parent c62b4ff97bfca5242701f7d1cdef4bdc29080a4d major reorganization/simplification of HOLCF type classes: removed profinite/bifinite classes and approx function; universal domain uses approx_chain locale instead of bifinite class; ideal_completion locale does not use 'take' functions, requires countable basis instead; replaced type 'udom alg_defl' with type 'sfp'; replaced class 'rep' with class 'sfp'; renamed REP('a) to SFP('a); diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Algebraic.thy --- a/src/HOLCF/Algebraic.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Algebraic.thy Wed Oct 06 10:49:27 2010 -0700 @@ -2,303 +2,18 @@ Author: Brian Huffman *) -header {* Algebraic deflations *} +header {* Algebraic deflations and SFP domains *} theory Algebraic -imports Completion Fix Eventual Bifinite -begin - -subsection {* Constructing finite deflations by iteration *} - -lemma le_Suc_induct: - assumes le: "i \ j" - assumes step: "\i. P i (Suc i)" - assumes refl: "\i. P i i" - assumes trans: "\i j k. \P i j; P j k\ \ P i k" - shows "P i j" -proof (cases "i = j") - assume "i = j" - thus "P i j" by (simp add: refl) -next - assume "i \ j" - with le have "i < j" by simp - thus "P i j" using step trans by (rule less_Suc_induct) -qed - -definition - eventual_iterate :: "('a \ 'a::cpo) \ ('a \ 'a)" -where - "eventual_iterate f = eventual (\n. iterate n\f)" - -text {* A pre-deflation is like a deflation, but not idempotent. *} - -locale pre_deflation = - fixes f :: "'a \ 'a::cpo" - assumes below: "\x. f\x \ x" - assumes finite_range: "finite (range (\x. f\x))" +imports Universal Bifinite begin -lemma iterate_below: "iterate i\f\x \ x" -by (induct i, simp_all add: below_trans [OF below]) - -lemma iterate_fixed: "f\x = x \ iterate i\f\x = x" -by (induct i, simp_all) - -lemma antichain_iterate_app: "i \ j \ iterate j\f\x \ iterate i\f\x" -apply (erule le_Suc_induct) -apply (simp add: below) -apply (rule below_refl) -apply (erule (1) below_trans) -done - -lemma finite_range_iterate_app: "finite (range (\i. iterate i\f\x))" -proof (rule finite_subset) - show "range (\i. iterate i\f\x) \ insert x (range (\x. f\x))" - by (clarify, case_tac i, simp_all) - show "finite (insert x (range (\x. f\x)))" - by (simp add: finite_range) -qed - -lemma eventually_constant_iterate_app: - "eventually_constant (\i. iterate i\f\x)" -unfolding eventually_constant_def MOST_nat_le -proof - - let ?Y = "\i. iterate i\f\x" - have "\j. \k. ?Y j \ ?Y k" - apply (rule finite_range_has_max) - apply (erule antichain_iterate_app) - apply (rule finite_range_iterate_app) - done - then obtain j where j: "\k. ?Y j \ ?Y k" by fast - show "\z m. \n\m. ?Y n = z" - proof (intro exI allI impI) - fix k - assume "j \ k" - hence "?Y k \ ?Y j" by (rule antichain_iterate_app) - also have "?Y j \ ?Y k" by (rule j) - finally show "?Y k = ?Y j" . - qed -qed - -lemma eventually_constant_iterate: - "eventually_constant (\n. iterate n\f)" -proof - - have "\y\range (\x. f\x). eventually_constant (\i. iterate i\f\y)" - by (simp add: eventually_constant_iterate_app) - hence "\y\range (\x. f\x). MOST i. MOST j. iterate j\f\y = iterate i\f\y" - unfolding eventually_constant_MOST_MOST . - hence "MOST i. MOST j. \y\range (\x. f\x). iterate j\f\y = iterate i\f\y" - by (simp only: MOST_finite_Ball_distrib [OF finite_range]) - hence "MOST i. MOST j. \x. iterate j\f\(f\x) = iterate i\f\(f\x)" - by simp - hence "MOST i. MOST j. \x. iterate (Suc j)\f\x = iterate (Suc i)\f\x" - by (simp only: iterate_Suc2) - hence "MOST i. MOST j. iterate (Suc j)\f = iterate (Suc i)\f" - by (simp only: expand_cfun_eq) - hence "eventually_constant (\i. iterate (Suc i)\f)" - unfolding eventually_constant_MOST_MOST . - thus "eventually_constant (\i. iterate i\f)" - by (rule eventually_constant_SucD) -qed - -abbreviation - d :: "'a \ 'a" -where - "d \ eventual_iterate f" - -lemma MOST_d: "MOST n. P (iterate n\f) \ P d" -unfolding eventual_iterate_def -using eventually_constant_iterate by (rule MOST_eventual) - -lemma f_d: "f\(d\x) = d\x" -apply (rule MOST_d) -apply (subst iterate_Suc [symmetric]) -apply (rule eventually_constant_MOST_Suc_eq) -apply (rule eventually_constant_iterate_app) -done - -lemma d_fixed_iff: "d\x = x \ f\x = x" -proof - assume "d\x = x" - with f_d [where x=x] - show "f\x = x" by simp -next - assume f: "f\x = x" - have "\n. iterate n\f\x = x" - by (rule allI, rule nat.induct, simp, simp add: f) - hence "MOST n. iterate n\f\x = x" - by (rule ALL_MOST) - thus "d\x = x" - by (rule MOST_d) -qed - -lemma finite_deflation_d: "finite_deflation d" -proof - fix x :: 'a - have "d \ range (\n. iterate n\f)" - unfolding eventual_iterate_def - using eventually_constant_iterate - by (rule eventual_mem_range) - then obtain n where n: "d = iterate n\f" .. - have "iterate n\f\(d\x) = d\x" - using f_d by (rule iterate_fixed) - thus "d\(d\x) = d\x" - by (simp add: n) -next - fix x :: 'a - show "d\x \ x" - by (rule MOST_d, simp add: iterate_below) -next - from finite_range - have "finite {x. f\x = x}" - by (rule finite_range_imp_finite_fixes) - thus "finite {x. d\x = x}" - by (simp add: d_fixed_iff) -qed - -lemma deflation_d: "deflation d" -using finite_deflation_d -by (rule finite_deflation_imp_deflation) - -end - -lemma finite_deflation_eventual_iterate: - "pre_deflation d \ finite_deflation (eventual_iterate d)" -by (rule pre_deflation.finite_deflation_d) - -lemma pre_deflation_oo: - assumes "finite_deflation d" - assumes f: "\x. f\x \ x" - shows "pre_deflation (d oo f)" -proof - interpret d: finite_deflation d by fact - fix x - show "\x. (d oo f)\x \ x" - by (simp, rule below_trans [OF d.below f]) - show "finite (range (\x. (d oo f)\x))" - by (rule finite_subset [OF _ d.finite_range], auto) -qed - -lemma eventual_iterate_oo_fixed_iff: - assumes "finite_deflation d" - assumes f: "\x. f\x \ x" - shows "eventual_iterate (d oo f)\x = x \ d\x = x \ f\x = x" -proof - - interpret d: finite_deflation d by fact - let ?e = "d oo f" - interpret e: pre_deflation "d oo f" - using `finite_deflation d` f - by (rule pre_deflation_oo) - let ?g = "eventual (\n. iterate n\?e)" - show ?thesis - apply (subst e.d_fixed_iff) - apply simp - apply safe - apply (erule subst) - apply (rule d.idem) - apply (rule below_antisym) - apply (rule f) - apply (erule subst, rule d.below) - apply simp - done -qed - -lemma eventual_mono: - assumes A: "eventually_constant A" - assumes B: "eventually_constant B" - assumes below: "\n. A n \ B n" - shows "eventual A \ eventual B" -proof - - from A have "MOST n. A n = eventual A" - by (rule MOST_eq_eventual) - then have "MOST n. eventual A \ B n" - by (rule MOST_mono) (erule subst, rule below) - with B show "eventual A \ eventual B" - by (rule MOST_eventual) -qed - -lemma eventual_iterate_mono: - assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \ g" - shows "eventual_iterate f \ eventual_iterate g" -unfolding eventual_iterate_def -apply (rule eventual_mono) -apply (rule pre_deflation.eventually_constant_iterate [OF f]) -apply (rule pre_deflation.eventually_constant_iterate [OF g]) -apply (rule monofun_cfun_arg [OF `f \ g`]) -done - -lemma cont2cont_eventual_iterate_oo: - assumes d: "finite_deflation d" - assumes cont: "cont f" and below: "\x y. f x\y \ y" - shows "cont (\x. eventual_iterate (d oo f x))" - (is "cont ?e") -proof (rule contI2) - show "monofun ?e" - apply (rule monofunI) - apply (rule eventual_iterate_mono) - apply (rule pre_deflation_oo [OF d below]) - apply (rule pre_deflation_oo [OF d below]) - apply (rule monofun_cfun_arg) - apply (erule cont2monofunE [OF cont]) - done -next - fix Y :: "nat \ 'b" - assume Y: "chain Y" - with cont have fY: "chain (\i. f (Y i))" - by (rule ch2ch_cont) - assume eY: "chain (\i. ?e (Y i))" - have lub_below: "\x. f (\i. Y i)\x \ x" - by (rule admD [OF _ Y], simp add: cont, rule below) - have "deflation (?e (\i. Y i))" - apply (rule pre_deflation.deflation_d) - apply (rule pre_deflation_oo [OF d lub_below]) - done - then show "?e (\i. Y i) \ (\i. ?e (Y i))" - proof (rule deflation.belowI) - fix x :: 'a - assume "?e (\i. Y i)\x = x" - hence "d\x = x" and "f (\i. Y i)\x = x" - by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below]) - hence "(\i. f (Y i)\x) = x" - apply (simp only: cont2contlubE [OF cont Y]) - apply (simp only: contlub_cfun_fun [OF fY]) - done - have "compact (d\x)" - using d by (rule finite_deflation.compact) - then have "compact x" - using `d\x = x` by simp - then have "compact (\i. f (Y i)\x)" - using `(\i. f (Y i)\x) = x` by simp - then have "\n. max_in_chain n (\i. f (Y i)\x)" - by - (rule compact_imp_max_in_chain, simp add: fY, assumption) - then obtain n where n: "max_in_chain n (\i. f (Y i)\x)" .. - then have "f (Y n)\x = x" - using `(\i. f (Y i)\x) = x` fY by (simp add: maxinch_is_thelub) - with `d\x = x` have "?e (Y n)\x = x" - by (simp add: eventual_iterate_oo_fixed_iff [OF d below]) - moreover have "?e (Y n)\x \ (\i. ?e (Y i)\x)" - by (rule is_ub_thelub, simp add: eY) - ultimately have "x \ (\i. ?e (Y i))\x" - by (simp add: contlub_cfun_fun eY) - also have "(\i. ?e (Y i))\x \ x" - apply (rule deflation.below) - apply (rule admD [OF adm_deflation eY]) - apply (rule pre_deflation.deflation_d) - apply (rule pre_deflation_oo [OF d below]) - done - finally show "(\i. ?e (Y i))\x = x" .. - qed -qed - - subsection {* Type constructor for finite deflations *} -default_sort profinite +typedef (open) fin_defl = "{d::udom \ udom. finite_deflation d}" +by (fast intro: finite_deflation_UU) -typedef (open) 'a fin_defl = "{d::'a \ 'a. finite_deflation d}" -by (fast intro: finite_deflation_approx) - -instantiation fin_defl :: (profinite) below +instantiation fin_defl :: below begin definition below_fin_defl_def: @@ -307,8 +22,9 @@ instance .. end -instance fin_defl :: (profinite) po -by (rule typedef_po [OF type_definition_fin_defl below_fin_defl_def]) +instance fin_defl :: po +using type_definition_fin_defl below_fin_defl_def +by (rule typedef_po) lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)" using Rep_fin_defl by simp @@ -337,269 +53,146 @@ apply (rule fin_defl_belowI, simp) done +lemma Rep_fin_defl_mono: "a \ b \ Rep_fin_defl a \ Rep_fin_defl b" +unfolding below_fin_defl_def . + lemma Abs_fin_defl_mono: "\finite_deflation a; finite_deflation b; a \ b\ \ Abs_fin_defl a \ Abs_fin_defl b" unfolding below_fin_defl_def by (simp add: Abs_fin_defl_inverse) - -subsection {* Take function for finite deflations *} - -definition - defl_approx :: "nat \ ('a \ 'a) \ ('a \ 'a)" -where - "defl_approx i d = eventual_iterate (approx i oo d)" - -lemma finite_deflation_defl_approx: - "deflation d \ finite_deflation (defl_approx i d)" -unfolding defl_approx_def -apply (rule pre_deflation.finite_deflation_d) -apply (rule pre_deflation_oo) -apply (rule finite_deflation_approx) -apply (erule deflation.below) -done - -lemma deflation_defl_approx: - "deflation d \ deflation (defl_approx i d)" -apply (rule finite_deflation_imp_deflation) -apply (erule finite_deflation_defl_approx) -done - -lemma defl_approx_fixed_iff: - "deflation d \ defl_approx i d\x = x \ approx i\x = x \ d\x = x" -unfolding defl_approx_def -apply (rule eventual_iterate_oo_fixed_iff) -apply (rule finite_deflation_approx) -apply (erule deflation.below) -done - -lemma defl_approx_below: - "\a \ b; deflation a; deflation b\ \ defl_approx i a \ defl_approx i b" -apply (rule deflation.belowI) -apply (erule deflation_defl_approx) -apply (simp add: defl_approx_fixed_iff) -apply (erule (1) deflation.belowD) -apply (erule conjunct2) -done - -lemma cont2cont_defl_approx: - assumes cont: "cont f" and below: "\x y. f x\y \ y" - shows "cont (\x. defl_approx i (f x))" -unfolding defl_approx_def -using finite_deflation_approx assms -by (rule cont2cont_eventual_iterate_oo) - -definition - fd_take :: "nat \ 'a fin_defl \ 'a fin_defl" -where - "fd_take i d = Abs_fin_defl (defl_approx i (Rep_fin_defl d))" - -lemma Rep_fin_defl_fd_take: - "Rep_fin_defl (fd_take i d) = defl_approx i (Rep_fin_defl d)" -unfolding fd_take_def -apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq]) -apply (rule finite_deflation_defl_approx) -apply (rule deflation_Rep_fin_defl) -done +lemma (in finite_deflation) compact_belowI: + assumes "\x. compact x \ d\x = x \ f\x = x" shows "d \ f" +by (rule belowI, rule assms, erule subst, rule compact) -lemma fd_take_fixed_iff: - "Rep_fin_defl (fd_take i d)\x = x \ - approx i\x = x \ Rep_fin_defl d\x = x" -unfolding Rep_fin_defl_fd_take -apply (rule defl_approx_fixed_iff) -apply (rule deflation_Rep_fin_defl) -done - -lemma fd_take_below: "fd_take n d \ d" -apply (rule fin_defl_belowI) -apply (simp add: fd_take_fixed_iff) -done - -lemma fd_take_idem: "fd_take n (fd_take n d) = fd_take n d" -apply (rule fin_defl_eqI) -apply (simp add: fd_take_fixed_iff) -done - -lemma fd_take_mono: "a \ b \ fd_take n a \ fd_take n b" -apply (rule fin_defl_belowI) -apply (simp add: fd_take_fixed_iff) -apply (simp add: fin_defl_belowD) -done - -lemma approx_fixed_le_lemma: "\i \ j; approx i\x = x\ \ approx j\x = x" -by (erule subst, simp add: min_def) - -lemma fd_take_chain: "m \ n \ fd_take m a \ fd_take n a" -apply (rule fin_defl_belowI) -apply (simp add: fd_take_fixed_iff) -apply (simp add: approx_fixed_le_lemma) -done - -lemma finite_range_fd_take: "finite (range (fd_take n))" -apply (rule finite_imageD [where f="\a. {x. Rep_fin_defl a\x = x}"]) -apply (rule finite_subset [where B="Pow {x. approx n\x = x}"]) -apply (clarify, simp add: fd_take_fixed_iff) -apply (simp add: finite_fixes_approx) -apply (rule inj_onI, clarify) -apply (simp add: set_eq_iff fin_defl_eqI) -done - -lemma fd_take_covers: "\n. fd_take n a = a" -apply (rule_tac x= - "Max ((\x. LEAST n. approx n\x = x) ` {x. Rep_fin_defl a\x = x})" in exI) -apply (rule below_antisym) -apply (rule fd_take_below) -apply (rule fin_defl_belowI) -apply (simp add: fd_take_fixed_iff) -apply (rule approx_fixed_le_lemma) -apply (rule Max_ge) -apply (rule finite_imageI) -apply (rule Rep_fin_defl.finite_fixes) -apply (rule imageI) -apply (erule CollectI) -apply (rule LeastI_ex) -apply (rule profinite_compact_eq_approx) -apply (erule subst) -apply (rule Rep_fin_defl.compact) -done - -interpretation fin_defl: basis_take below fd_take -apply default -apply (rule fd_take_below) -apply (rule fd_take_idem) -apply (erule fd_take_mono) -apply (rule fd_take_chain, simp) -apply (rule finite_range_fd_take) -apply (rule fd_take_covers) -done - +lemma compact_Rep_fin_defl [simp]: "compact (Rep_fin_defl a)" +using finite_deflation_Rep_fin_defl +by (rule finite_deflation_imp_compact) subsection {* Defining algebraic deflations by ideal completion *} -typedef (open) 'a alg_defl = - "{S::'a fin_defl set. below.ideal S}" +text {* + An SFP domain is one that can be represented as the limit of a + sequence of finite posets. Here we use omega-algebraic deflations + (i.e. countable ideals of finite deflations) to model sequences of + finite posets. +*} + +typedef (open) sfp = "{S::fin_defl set. below.ideal S}" by (fast intro: below.ideal_principal) -instantiation alg_defl :: (profinite) below +instantiation sfp :: below begin definition - "x \ y \ Rep_alg_defl x \ Rep_alg_defl y" + "x \ y \ Rep_sfp x \ Rep_sfp y" instance .. end -instance alg_defl :: (profinite) po -by (rule below.typedef_ideal_po - [OF type_definition_alg_defl below_alg_defl_def]) +instance sfp :: po +using type_definition_sfp below_sfp_def +by (rule below.typedef_ideal_po) -instance alg_defl :: (profinite) cpo -by (rule below.typedef_ideal_cpo - [OF type_definition_alg_defl below_alg_defl_def]) +instance sfp :: cpo +using type_definition_sfp below_sfp_def +by (rule below.typedef_ideal_cpo) -lemma Rep_alg_defl_lub: - "chain Y \ Rep_alg_defl (\i. Y i) = (\i. Rep_alg_defl (Y i))" -by (rule below.typedef_ideal_rep_contlub - [OF type_definition_alg_defl below_alg_defl_def]) +lemma Rep_sfp_lub: + "chain Y \ Rep_sfp (\i. Y i) = (\i. Rep_sfp (Y i))" +using type_definition_sfp below_sfp_def +by (rule below.typedef_ideal_rep_contlub) -lemma ideal_Rep_alg_defl: "below.ideal (Rep_alg_defl xs)" -by (rule Rep_alg_defl [unfolded mem_Collect_eq]) +lemma ideal_Rep_sfp: "below.ideal (Rep_sfp xs)" +by (rule Rep_sfp [unfolded mem_Collect_eq]) definition - alg_defl_principal :: "'a fin_defl \ 'a alg_defl" where - "alg_defl_principal t = Abs_alg_defl {u. u \ t}" + sfp_principal :: "fin_defl \ sfp" where + "sfp_principal t = Abs_sfp {u. u \ t}" -lemma Rep_alg_defl_principal: - "Rep_alg_defl (alg_defl_principal t) = {u. u \ t}" -unfolding alg_defl_principal_def -by (simp add: Abs_alg_defl_inverse below.ideal_principal) +lemma Rep_sfp_principal: + "Rep_sfp (sfp_principal t) = {u. u \ t}" +unfolding sfp_principal_def +by (simp add: Abs_sfp_inverse below.ideal_principal) -interpretation alg_defl: - ideal_completion below fd_take alg_defl_principal Rep_alg_defl +lemma fin_defl_countable: "\f::fin_defl \ nat. inj f" +proof + have *: "\d. finite (approx_chain.place udom_approx ` + Rep_compact_basis -` {x. Rep_fin_defl d\x = x})" + apply (rule finite_imageI) + apply (rule finite_vimageI) + apply (rule Rep_fin_defl.finite_fixes) + apply (simp add: inj_on_def Rep_compact_basis_inject) + done + have range_eq: "range Rep_compact_basis = {x. compact x}" + using type_definition_compact_basis by (rule type_definition.Rep_range) + show "inj (\d. set_encode + (approx_chain.place udom_approx ` Rep_compact_basis -` {x. Rep_fin_defl d\x = x}))" + apply (rule inj_onI) + apply (simp only: set_encode_eq *) + apply (simp only: inj_image_eq_iff approx_chain.inj_place [OF udom_approx]) + apply (drule_tac f="image Rep_compact_basis" in arg_cong) + apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff) + apply (rule Rep_fin_defl_inject [THEN iffD1]) + apply (rule below_antisym) + apply (rule Rep_fin_defl.compact_belowI, rename_tac z) + apply (drule_tac x=z in spec, simp) + apply (rule Rep_fin_defl.compact_belowI, rename_tac z) + apply (drule_tac x=z in spec, simp) + done +qed + +interpretation sfp: ideal_completion below sfp_principal Rep_sfp apply default -apply (rule ideal_Rep_alg_defl) -apply (erule Rep_alg_defl_lub) -apply (rule Rep_alg_defl_principal) -apply (simp only: below_alg_defl_def) +apply (rule ideal_Rep_sfp) +apply (erule Rep_sfp_lub) +apply (rule Rep_sfp_principal) +apply (simp only: below_sfp_def) +apply (rule fin_defl_countable) done text {* Algebraic deflations are pointed *} -lemma alg_defl_minimal: - "alg_defl_principal (Abs_fin_defl \) \ x" -apply (induct x rule: alg_defl.principal_induct, simp) -apply (rule alg_defl.principal_mono) -apply (induct_tac a) -apply (rule Abs_fin_defl_mono) -apply (rule finite_deflation_UU) -apply simp -apply (rule minimal) +lemma sfp_minimal: "sfp_principal (Abs_fin_defl \) \ x" +apply (induct x rule: sfp.principal_induct, simp) +apply (rule sfp.principal_mono) +apply (simp add: below_fin_defl_def) +apply (simp add: Abs_fin_defl_inverse finite_deflation_UU) done -instance alg_defl :: (bifinite) pcpo -by intro_classes (fast intro: alg_defl_minimal) - -lemma inst_alg_defl_pcpo: "\ = alg_defl_principal (Abs_fin_defl \)" -by (rule alg_defl_minimal [THEN UU_I, symmetric]) - -text {* Algebraic deflations are profinite *} - -instantiation alg_defl :: (profinite) profinite -begin - -definition - approx_alg_defl_def: "approx = alg_defl.completion_approx" +instance sfp :: pcpo +by intro_classes (fast intro: sfp_minimal) -instance -apply (intro_classes, unfold approx_alg_defl_def) -apply (rule alg_defl.chain_completion_approx) -apply (rule alg_defl.lub_completion_approx) -apply (rule alg_defl.completion_approx_idem) -apply (rule alg_defl.finite_fixes_completion_approx) -done - -end - -instance alg_defl :: (bifinite) bifinite .. - -lemma approx_alg_defl_principal [simp]: - "approx n\(alg_defl_principal t) = alg_defl_principal (fd_take n t)" -unfolding approx_alg_defl_def -by (rule alg_defl.completion_approx_principal) - -lemma approx_eq_alg_defl_principal: - "\t\Rep_alg_defl xs. approx n\xs = alg_defl_principal (fd_take n t)" -unfolding approx_alg_defl_def -by (rule alg_defl.completion_approx_eq_principal) - +lemma inst_sfp_pcpo: "\ = sfp_principal (Abs_fin_defl \)" +by (rule sfp_minimal [THEN UU_I, symmetric]) subsection {* Applying algebraic deflations *} definition - cast :: "'a alg_defl \ 'a \ 'a" + cast :: "sfp \ udom \ udom" where - "cast = alg_defl.basis_fun Rep_fin_defl" + "cast = sfp.basis_fun Rep_fin_defl" -lemma cast_alg_defl_principal: - "cast\(alg_defl_principal a) = Rep_fin_defl a" +lemma cast_sfp_principal: + "cast\(sfp_principal a) = Rep_fin_defl a" unfolding cast_def -apply (rule alg_defl.basis_fun_principal) +apply (rule sfp.basis_fun_principal) apply (simp only: below_fin_defl_def) done lemma deflation_cast: "deflation (cast\d)" -apply (induct d rule: alg_defl.principal_induct) +apply (induct d rule: sfp.principal_induct) apply (rule adm_subst [OF _ adm_deflation], simp) -apply (simp add: cast_alg_defl_principal) +apply (simp add: cast_sfp_principal) apply (rule finite_deflation_imp_deflation) apply (rule finite_deflation_Rep_fin_defl) done lemma finite_deflation_cast: "compact d \ finite_deflation (cast\d)" -apply (drule alg_defl.compact_imp_principal, clarify) -apply (simp add: cast_alg_defl_principal) +apply (drule sfp.compact_imp_principal, clarify) +apply (simp add: cast_sfp_principal) apply (rule finite_deflation_Rep_fin_defl) done @@ -608,43 +201,33 @@ declare cast.idem [simp] -lemma cast_approx: "cast\(approx n\A) = defl_approx n (cast\A)" -apply (rule alg_defl.principal_induct) -apply (rule adm_eq) -apply simp -apply (simp add: cont2cont_defl_approx cast.below) -apply (simp only: approx_alg_defl_principal) -apply (simp only: cast_alg_defl_principal) -apply (simp only: Rep_fin_defl_fd_take) +lemma compact_cast [simp]: "compact d \ compact (cast\d)" +apply (rule finite_deflation_imp_compact) +apply (erule finite_deflation_cast) done -lemma cast_approx_fixed_iff: - "cast\(approx i\A)\x = x \ approx i\x = x \ cast\A\x = x" -apply (simp only: cast_approx) -apply (rule defl_approx_fixed_iff) -apply (rule deflation_cast) +lemma cast_below_cast: "cast\A \ cast\B \ A \ B" +apply (induct A rule: sfp.principal_induct, simp) +apply (induct B rule: sfp.principal_induct, simp) +apply (simp add: cast_sfp_principal below_fin_defl_def) done -lemma defl_approx_cast: "defl_approx i (cast\A) = cast\(approx i\A)" -by (rule cast_approx [symmetric]) - -lemma cast_below_cast_iff: "cast\A \ cast\B \ A \ B" -apply (induct A rule: alg_defl.principal_induct, simp) -apply (induct B rule: alg_defl.principal_induct) -apply (simp add: cast_alg_defl_principal) -apply (simp add: finite_deflation_imp_compact finite_deflation_Rep_fin_defl) -apply (simp add: cast_alg_defl_principal below_fin_defl_def) +lemma compact_cast_iff: "compact (cast\d) \ compact d" +apply (rule iffI) +apply (simp only: compact_def cast_below_cast [symmetric]) +apply (erule adm_subst [OF cont_Rep_CFun2]) +apply (erule compact_cast) done lemma cast_below_imp_below: "cast\A \ cast\B \ A \ B" -by (simp only: cast_below_cast_iff) +by (simp only: cast_below_cast) lemma cast_eq_imp_eq: "cast\A = cast\B \ A = B" by (simp add: below_antisym cast_below_imp_below) lemma cast_strict1 [simp]: "cast\\ = \" -apply (subst inst_alg_defl_pcpo) -apply (subst cast_alg_defl_principal) +apply (subst inst_sfp_pcpo) +apply (subst cast_sfp_principal) apply (rule Abs_fin_defl_inverse) apply (simp add: finite_deflation_UU) done @@ -652,119 +235,271 @@ lemma cast_strict2 [simp]: "cast\A\\ = \" by (rule cast.below [THEN UU_I]) - subsection {* Deflation membership relation *} definition - in_deflation :: "'a::profinite \ 'a alg_defl \ bool" (infixl ":::" 50) + in_sfp :: "udom \ sfp \ bool" (infixl ":::" 50) where "x ::: A \ cast\A\x = x" -lemma adm_in_deflation: "adm (\x. x ::: A)" -unfolding in_deflation_def by simp +lemma adm_in_sfp: "adm (\x. x ::: A)" +unfolding in_sfp_def by simp -lemma in_deflationI: "cast\A\x = x \ x ::: A" -unfolding in_deflation_def . +lemma in_sfpI: "cast\A\x = x \ x ::: A" +unfolding in_sfp_def . lemma cast_fixed: "x ::: A \ cast\A\x = x" -unfolding in_deflation_def . +unfolding in_sfp_def . -lemma cast_in_deflation [simp]: "cast\A\x ::: A" -unfolding in_deflation_def by (rule cast.idem) +lemma cast_in_sfp [simp]: "cast\A\x ::: A" +unfolding in_sfp_def by (rule cast.idem) -lemma bottom_in_deflation [simp]: "\ ::: A" -unfolding in_deflation_def by (rule cast_strict2) +lemma bottom_in_sfp [simp]: "\ ::: A" +unfolding in_sfp_def by (rule cast_strict2) -lemma subdeflationD: "A \ B \ x ::: A \ x ::: B" -unfolding in_deflation_def +lemma sfp_belowD: "A \ B \ x ::: A \ x ::: B" +unfolding in_sfp_def apply (rule deflation.belowD) apply (rule deflation_cast) apply (erule monofun_cfun_arg) apply assumption done -lemma rev_subdeflationD: "x ::: A \ A \ B \ x ::: B" -by (rule subdeflationD) +lemma rev_sfp_belowD: "x ::: A \ A \ B \ x ::: B" +by (rule sfp_belowD) -lemma subdeflationI: "(\x. x ::: A \ x ::: B) \ A \ B" +lemma sfp_belowI: "(\x. x ::: A \ x ::: B) \ A \ B" apply (rule cast_below_imp_below) apply (rule cast.belowI) -apply (simp add: in_deflation_def) -done - -text "Identity deflation:" - -lemma "cast\(\i. alg_defl_principal (Abs_fin_defl (approx i)))\x = x" -apply (subst contlub_cfun_arg) -apply (rule chainI) -apply (rule alg_defl.principal_mono) -apply (rule Abs_fin_defl_mono) -apply (rule finite_deflation_approx) -apply (rule finite_deflation_approx) -apply (rule chainE) -apply (rule chain_approx) -apply (simp add: cast_alg_defl_principal - Abs_fin_defl_inverse finite_deflation_approx) +apply (simp add: in_sfp_def) done -subsection {* Bifinite domains and algebraic deflations *} +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. +*} -text {* This lemma says that if we have an ep-pair from -a bifinite domain into a universal domain, then e oo p -is an algebraic deflation. *} +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)))" -lemma - assumes "ep_pair e p" - constrains e :: "'a::profinite \ 'b::profinite" - shows "\d. cast\d = e oo p" -proof - interpret ep_pair e p by fact - let ?a = "\i. e oo approx i oo p" - have a: "\i. finite_deflation (?a i)" - apply (rule finite_deflation_e_d_p) - apply (rule finite_deflation_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 - let ?d = "\i. alg_defl_principal (Abs_fin_defl (?a i))" - show "cast\?d = e oo p" + 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 alg_defl.principal_mono) - apply (rule Abs_fin_defl_mono [OF a a]) - apply (rule chainE, simp) - apply (subst cast_alg_defl_principal) - apply (simp add: Abs_fin_defl_inverse a) - apply (simp add: expand_cfun_eq lub_distribs) - done -qed - -text {* This lemma says that if we have an ep-pair -from a cpo into a bifinite domain, and e oo p is -an algebraic deflation, then the cpo is bifinite. *} - -lemma - assumes "ep_pair e p" - constrains e :: "'a::cpo \ 'b::profinite" - assumes d: "\x. cast\d\x = e\(p\x)" - obtains a :: "nat \ 'a \ 'a" where - "\i. finite_deflation (a i)" - "(\i. a i) = ID" -proof - interpret ep_pair e p by fact - let ?a = "\i. p oo cast\(approx i\d) oo e" - show "\i. finite_deflation (?a i)" - apply (rule finite_deflation_p_d_e) - apply (rule finite_deflation_cast) - apply (rule compact_approx) - apply (rule below_eq_trans [OF _ d]) - apply (rule monofun_cfun_fun) - apply (rule monofun_cfun_arg) - apply (rule approx_below) - done - show "(\i. ?a i) = ID" - apply (rule ext_cfun, simp) - apply (simp add: lub_distribs) - apply (simp add: d) + 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 c62b4ff97bfc -r b525988432e9 src/HOLCF/Bifinite.thy --- a/src/HOLCF/Bifinite.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Bifinite.thy Wed Oct 06 10:49:27 2010 -0700 @@ -8,103 +8,7 @@ imports Deflation begin -subsection {* Omega-profinite and bifinite domains *} - -class profinite = - fixes approx :: "nat \ 'a \ 'a" - assumes chain_approx [simp]: "chain approx" - assumes lub_approx_app [simp]: "(\i. approx i\x) = x" - assumes approx_idem: "approx i\(approx i\x) = approx i\x" - assumes finite_fixes_approx: "finite {x. approx i\x = x}" - -class bifinite = profinite + pcpo - -lemma approx_below: "approx i\x \ x" -proof - - have "chain (\i. approx i\x)" by simp - hence "approx i\x \ (\i. approx i\x)" by (rule is_ub_thelub) - thus "approx i\x \ x" by simp -qed - -lemma finite_deflation_approx: "finite_deflation (approx i)" -proof - fix x :: 'a - show "approx i\(approx i\x) = approx i\x" - by (rule approx_idem) - show "approx i\x \ x" - by (rule approx_below) - show "finite {x. approx i\x = x}" - by (rule finite_fixes_approx) -qed - -interpretation approx: finite_deflation "approx i" -by (rule finite_deflation_approx) - -lemma (in deflation) deflation: "deflation d" .. - -lemma deflation_approx: "deflation (approx i)" -by (rule approx.deflation) - -lemma lub_approx [simp]: "(\i. approx i) = (\ x. x)" -by (rule ext_cfun, simp add: contlub_cfun_fun) - -lemma approx_strict [simp]: "approx i\\ = \" -by (rule UU_I, rule approx_below) - -lemma approx_approx1: - "i \ j \ approx i\(approx j\x) = approx i\x" -apply (rule deflation_below_comp1 [OF deflation_approx deflation_approx]) -apply (erule chain_mono [OF chain_approx]) -done - -lemma approx_approx2: - "j \ i \ approx i\(approx j\x) = approx j\x" -apply (rule deflation_below_comp2 [OF deflation_approx deflation_approx]) -apply (erule chain_mono [OF chain_approx]) -done - -lemma approx_approx [simp]: - "approx i\(approx j\x) = approx (min i j)\x" -apply (rule_tac x=i and y=j in linorder_le_cases) -apply (simp add: approx_approx1 min_def) -apply (simp add: approx_approx2 min_def) -done - -lemma finite_image_approx: "finite ((\x. approx n\x) ` A)" -by (rule approx.finite_image) - -lemma finite_range_approx: "finite (range (\x. approx i\x))" -by (rule approx.finite_range) - -lemma compact_approx [simp]: "compact (approx n\x)" -by (rule approx.compact) - -lemma profinite_compact_eq_approx: "compact x \ \i. approx i\x = x" -by (rule admD2, simp_all) - -lemma profinite_compact_iff: "compact x \ (\n. approx n\x = x)" - apply (rule iffI) - apply (erule profinite_compact_eq_approx) - apply (erule exE) - apply (erule subst) - apply (rule compact_approx) -done - -lemma approx_induct: - assumes adm: "adm P" and P: "\n x. P (approx n\x)" - shows "P x" -proof - - have "P (\n. approx n\x)" - by (rule admD [OF adm], simp, simp add: P) - thus "P x" by simp -qed - -lemma profinite_below_ext: "(\i. approx i\x \ approx i\y) \ x \ y" -apply (subgoal_tac "(\i. approx i\x) \ (\i. approx i\y)", simp) -apply (rule lub_mono, simp, simp, simp) -done - -subsection {* Instance for product type *} +subsection {* Map operator for product type *} definition cprod_map :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" @@ -161,46 +65,7 @@ by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) qed -instantiation prod :: (profinite, profinite) profinite -begin - -definition - approx_prod_def: - "approx = (\n. cprod_map\(approx n)\(approx n))" - -instance proof - fix i :: nat and x :: "'a \ 'b" - show "chain (approx :: nat \ 'a \ 'b \ 'a \ 'b)" - unfolding approx_prod_def by simp - show "(\i. approx i\x) = x" - unfolding approx_prod_def cprod_map_def - by (simp add: lub_distribs thelub_Pair) - show "approx i\(approx i\x) = approx i\x" - unfolding approx_prod_def cprod_map_def by simp - have "{x::'a \ 'b. approx i\x = x} \ - {x::'a. approx i\x = x} \ {x::'b. approx i\x = x}" - unfolding approx_prod_def by clarsimp - thus "finite {x::'a \ 'b. approx i\x = x}" - by (rule finite_subset, - intro finite_cartesian_product finite_fixes_approx) -qed - -end - -instance prod :: (bifinite, bifinite) bifinite .. - -lemma approx_Pair [simp]: - "approx i\(x, y) = (approx i\x, approx i\y)" -unfolding approx_prod_def by simp - -lemma fst_approx: "fst (approx i\p) = approx i\(fst p)" -by (induct p, simp) - -lemma snd_approx: "snd (approx i\p) = approx i\(snd p)" -by (induct p, simp) - - -subsection {* Instance for continuous function space *} +subsection {* Map operator for continuous function space *} definition cfun_map :: "('b \ 'a) \ ('c \ 'd) \ ('a \ 'c) \ ('b \ 'd)" @@ -305,39 +170,4 @@ apply (simp only: finite_deflation_cfun_map) done -instantiation cfun :: (profinite, profinite) profinite -begin - -definition - approx_cfun_def: - "approx = (\n. cfun_map\(approx n)\(approx n))" - -instance proof - show "chain (approx :: nat \ ('a \ 'b) \ ('a \ 'b))" - unfolding approx_cfun_def by simp -next - fix x :: "'a \ 'b" - show "(\i. approx i\x) = x" - unfolding approx_cfun_def cfun_map_def - by (simp add: lub_distribs eta_cfun) -next - fix i :: nat and x :: "'a \ 'b" - show "approx i\(approx i\x) = approx i\x" - unfolding approx_cfun_def cfun_map_def by simp -next - fix i :: nat - show "finite {x::'a \ 'b. approx i\x = x}" - unfolding approx_cfun_def - by (intro finite_deflation.finite_fixes - finite_deflation_cfun_map - finite_deflation_approx) -qed - end - -instance cfun :: (profinite, bifinite) bifinite .. - -lemma approx_cfun: "approx n\f\x = approx n\(f\(approx n\x))" -by (simp add: approx_cfun_def) - -end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/CompactBasis.thy --- a/src/HOLCF/CompactBasis.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/CompactBasis.thy Wed Oct 06 10:49:27 2010 -0700 @@ -2,174 +2,18 @@ Author: Brian Huffman *) -header {* Compact bases of domains *} +header {* A compact basis for powerdomains *} theory CompactBasis -imports Completion Bifinite -begin - -subsection {* Compact bases of bifinite domains *} - -default_sort profinite - -typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}" -by (fast intro: compact_approx) - -lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)" -by (rule Rep_compact_basis [unfolded mem_Collect_eq]) - -instantiation compact_basis :: (profinite) below +imports Algebraic begin -definition - compact_le_def: - "(op \) \ (\x y. Rep_compact_basis x \ Rep_compact_basis y)" - -instance .. - -end - -instance compact_basis :: (profinite) po -by (rule typedef_po - [OF type_definition_compact_basis compact_le_def]) - -text {* Take function for compact basis *} - -definition - compact_take :: "nat \ 'a compact_basis \ 'a compact_basis" where - "compact_take = (\n a. Abs_compact_basis (approx n\(Rep_compact_basis a)))" - -lemma Rep_compact_take: - "Rep_compact_basis (compact_take n a) = approx n\(Rep_compact_basis a)" -unfolding compact_take_def -by (simp add: Abs_compact_basis_inverse) - -lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric] - -interpretation compact_basis: - basis_take below compact_take -proof - fix n :: nat and a :: "'a compact_basis" - show "compact_take n a \ a" - unfolding compact_le_def - by (simp add: Rep_compact_take approx_below) -next - fix n :: nat and a :: "'a compact_basis" - show "compact_take n (compact_take n a) = compact_take n a" - by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_take) -next - fix n :: nat and a b :: "'a compact_basis" - assume "a \ b" thus "compact_take n a \ compact_take n b" - unfolding compact_le_def Rep_compact_take - by (rule monofun_cfun_arg) -next - fix n :: nat and a :: "'a compact_basis" - show "\n a. compact_take n a \ compact_take (Suc n) a" - unfolding compact_le_def Rep_compact_take - by (rule chainE, simp) -next - fix n :: nat - show "finite (range (compact_take n))" - apply (rule finite_imageD [where f="Rep_compact_basis"]) - apply (rule finite_subset [where B="range (\x. approx n\x)"]) - apply (clarsimp simp add: Rep_compact_take) - apply (rule finite_range_approx) - apply (rule inj_onI, simp add: Rep_compact_basis_inject) - done -next - fix a :: "'a compact_basis" - show "\n. compact_take n a = a" - apply (simp add: Rep_compact_basis_inject [symmetric]) - apply (simp add: Rep_compact_take) - apply (rule profinite_compact_eq_approx) - apply (rule compact_Rep_compact_basis) - done -qed - -text {* Ideal completion *} - -definition - approximants :: "'a \ 'a compact_basis set" where - "approximants = (\x. {a. Rep_compact_basis a \ x})" - -interpretation compact_basis: - ideal_completion below compact_take Rep_compact_basis approximants -proof - fix w :: 'a - show "preorder.ideal below (approximants w)" - proof (rule below.idealI) - show "\x. x \ approximants w" - unfolding approximants_def - apply (rule_tac x="Abs_compact_basis (approx 0\w)" in exI) - apply (simp add: Abs_compact_basis_inverse approx_below) - done - next - fix x y :: "'a compact_basis" - assume "x \ approximants w" "y \ approximants w" - thus "\z \ approximants w. x \ z \ y \ z" - unfolding approximants_def - apply simp - apply (cut_tac a=x in compact_Rep_compact_basis) - apply (cut_tac a=y in compact_Rep_compact_basis) - apply (drule profinite_compact_eq_approx) - apply (drule profinite_compact_eq_approx) - apply (clarify, rename_tac i j) - apply (rule_tac x="Abs_compact_basis (approx (max i j)\w)" in exI) - apply (simp add: compact_le_def) - apply (simp add: Abs_compact_basis_inverse approx_below) - apply (erule subst, erule subst) - apply (simp add: monofun_cfun chain_mono [OF chain_approx]) - done - next - fix x y :: "'a compact_basis" - assume "x \ y" "y \ approximants w" thus "x \ approximants w" - unfolding approximants_def - apply simp - apply (simp add: compact_le_def) - apply (erule (1) below_trans) - done - qed -next - fix Y :: "nat \ 'a" - assume Y: "chain Y" - show "approximants (\i. Y i) = (\i. approximants (Y i))" - unfolding approximants_def - apply safe - apply (simp add: compactD2 [OF compact_Rep_compact_basis Y]) - apply (erule below_trans, rule is_ub_thelub [OF Y]) - done -next - fix a :: "'a compact_basis" - show "approximants (Rep_compact_basis a) = {b. b \ a}" - unfolding approximants_def compact_le_def .. -next - fix x y :: "'a" - assume "approximants x \ approximants y" thus "x \ y" - apply (subgoal_tac "(\i. approx i\x) \ y", simp) - apply (rule admD, simp, simp) - apply (drule_tac c="Abs_compact_basis (approx i\x)" in subsetD) - apply (simp add: approximants_def Abs_compact_basis_inverse approx_below) - apply (simp add: approximants_def Abs_compact_basis_inverse) - done -qed - -text {* minimal compact element *} - -definition - compact_bot :: "'a::bifinite compact_basis" where - "compact_bot = Abs_compact_basis \" - -lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \" -unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse) - -lemma compact_bot_minimal [simp]: "compact_bot \ a" -unfolding compact_le_def Rep_compact_bot by simp - +default_sort sfp subsection {* A compact basis for powerdomains *} typedef 'a pd_basis = - "{S::'a::profinite compact_basis set. finite S \ S \ {}}" + "{S::'a compact_basis set. finite S \ S \ {}}" by (rule_tac x="{arbitrary}" in exI, simp) lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)" @@ -178,7 +22,21 @@ lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \ {}" by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp -text {* unit and plus *} +text {* The powerdomain basis type is countable. *} + +lemma pd_basis_countable: "\f::'a::sfp pd_basis \ nat. inj f" +proof - + obtain g :: "'a compact_basis \ nat" where "inj g" + using compact_basis.countable .. + hence image_g_eq: "\A B. g ` A = g ` B \ A = B" + by (rule inj_image_eq_iff) + have "inj (\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 \ 'a pd_basis" where @@ -229,7 +87,7 @@ apply (rule PDUnit, erule PDPlus [OF PDUnit]) done -text {* fold-pd *} +subsection {* Fold operator *} definition fold_pd :: @@ -250,52 +108,26 @@ by (simp add: image_Un fold1_Un2) qed -text {* Take function for powerdomain basis *} - -definition - pd_take :: "nat \ 'a pd_basis \ 'a pd_basis" where - "pd_take n = (\t. Abs_pd_basis (compact_take n ` Rep_pd_basis t))" +subsection {* Lemmas for proving if-and-only-if inequalities *} -lemma Rep_pd_take: - "Rep_pd_basis (pd_take n t) = compact_take n ` Rep_pd_basis t" -unfolding pd_take_def -apply (rule Abs_pd_basis_inverse) -apply (simp add: pd_basis_def) -done - -lemma pd_take_simps [simp]: - "pd_take n (PDUnit a) = PDUnit (compact_take n a)" - "pd_take n (PDPlus t u) = PDPlus (pd_take n t) (pd_take n u)" -apply (simp_all add: Rep_pd_basis_inject [symmetric]) -apply (simp_all add: Rep_pd_take Rep_PDUnit Rep_PDPlus image_Un) +lemma chain_max_below_iff: + assumes Y: "chain Y" shows "Y (max i j) \ x \ Y i \ x \ Y j \ x" +apply auto +apply (erule below_trans [OF chain_mono [OF Y le_maxI1]]) +apply (erule below_trans [OF chain_mono [OF Y le_maxI2]]) +apply (simp add: max_def) done -lemma pd_take_idem: "pd_take n (pd_take n t) = pd_take n t" -apply (induct t rule: pd_basis_induct) -apply (simp add: compact_basis.take_take) -apply simp -done - -lemma finite_range_pd_take: "finite (range (pd_take n))" -apply (rule finite_imageD [where f="Rep_pd_basis"]) -apply (rule finite_subset [where B="Pow (range (compact_take n))"]) -apply (clarsimp simp add: Rep_pd_take) -apply (simp add: compact_basis.finite_range_take) -apply (rule inj_onI, simp add: Rep_pd_basis_inject) -done +lemma all_ex_below_disj_iff: + assumes "chain X" and "chain Y" + shows "(\i. \j. X i \ Z j \ Y i \ Z j) \ + (\i. \j. X i \ Z j) \ (\i. \j. Y i \ Z j)" +by (metis chain_max_below_iff assms) -lemma pd_take_covers: "\n. pd_take n t = t" -apply (subgoal_tac "\n. \m\n. pd_take m t = t", fast) -apply (induct t rule: pd_basis_induct) -apply (cut_tac a=a in compact_basis.take_covers) -apply (clarify, rule_tac x=n in exI) -apply (clarify, simp) -apply (rule below_antisym) -apply (rule compact_basis.take_less) -apply (drule_tac a=a in compact_basis.take_chain_le) -apply simp -apply (clarify, rename_tac i j) -apply (rule_tac x="max i j" in exI, simp) -done +lemma all_ex_below_conj_iff: + assumes "chain X" and "chain Y" and "chain Z" + shows "(\i. \j. X i \ Z j \ Y i \ Z j) \ + (\i. \j. X i \ Z j) \ (\i. \j. Y i \ Z j)" +oops end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Completion.thy --- a/src/HOLCF/Completion.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Completion.thy Wed Oct 06 10:49:27 2010 -0700 @@ -2,7 +2,7 @@ Author: Brian Huffman *) -header {* Defining bifinite domains by ideal completion *} +header {* Defining algebraic domains by ideal completion *} theory Completion imports Cfun @@ -164,64 +164,27 @@ subsection {* Lemmas about least upper bounds *} -lemma finite_directed_contains_lub: - "\finite S; directed S\ \ \u\S. S <<| u" -apply (drule (1) directed_finiteD, rule subset_refl) -apply (erule bexE) -apply (rule rev_bexI, assumption) -apply (erule (1) is_lub_maximal) -done - -lemma lub_finite_directed_in_self: - "\finite S; directed S\ \ lub S \ S" -apply (drule (1) finite_directed_contains_lub, clarify) -apply (drule thelubI, simp) -done - -lemma finite_directed_has_lub: "\finite S; directed S\ \ \u. S <<| u" -by (drule (1) finite_directed_contains_lub, fast) - -lemma is_ub_thelub0: "\\u. S <<| u; x \ S\ \ x \ lub S" +lemma is_ub_thelub_ex: "\\u. S <<| u; x \ S\ \ x \ lub S" apply (erule exE, drule lubI) apply (drule is_lubD1) apply (erule (1) is_ubD) done -lemma is_lub_thelub0: "\\u. S <<| u; S <| x\ \ lub S \ x" +lemma is_lub_thelub_ex: "\\u. S <<| u; S <| x\ \ lub S \ x" by (erule exE, drule lubI, erule is_lub_lub) subsection {* Locale for ideal completion *} -locale basis_take = preorder + - fixes take :: "nat \ 'a::type \ 'a" - assumes take_less: "take n a \ a" - assumes take_take: "take n (take n a) = take n a" - assumes take_mono: "a \ b \ take n a \ take n b" - assumes take_chain: "take n a \ take (Suc n) a" - assumes finite_range_take: "finite (range (take n))" - assumes take_covers: "\n. take n a = a" -begin - -lemma take_chain_less: "m < n \ take m a \ take n a" -by (erule less_Suc_induct, rule take_chain, erule (1) r_trans) - -lemma take_chain_le: "m \ n \ take m a \ take n a" -by (cases "m = n", simp add: r_refl, simp add: take_chain_less) - -end - -locale ideal_completion = basis_take + +locale ideal_completion = preorder + fixes principal :: "'a::type \ 'b::cpo" fixes rep :: "'b::cpo \ 'a::type set" - assumes ideal_rep: "\x. preorder.ideal r (rep x)" + assumes ideal_rep: "\x. ideal (rep x)" assumes rep_contlub: "\Y. chain Y \ rep (\i. Y i) = (\i. rep (Y i))" assumes rep_principal: "\a. rep (principal a) = {b. b \ a}" assumes subset_repD: "\x y. rep x \ rep y \ x \ y" + assumes countable: "\f::'a \ nat. inj f" begin -lemma finite_take_rep: "finite (take n ` rep x)" -by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range_take]) - lemma rep_mono: "x \ y \ rep x \ rep y" apply (frule bin_chain) apply (drule rep_contlub) @@ -251,12 +214,19 @@ lemma principal_eq_iff: "principal a = principal b \ a \ b \ b \ a" unfolding po_eq_conv [where 'a='b] principal_below_iff .. +lemma eq_iff: "x = y \ rep x = rep y" +unfolding po_eq_conv below_def by auto + lemma repD: "a \ rep x \ principal a \ x" by (simp add: rep_eq) lemma principal_mono: "a \ b \ principal a \ principal b" by (simp only: principal_below_iff) +lemma ch2ch_principal [simp]: + "\i. Y i \ Y (Suc i) \ chain (\i. principal (Y i))" +by (simp add: chainI principal_mono) + lemma belowI: "(\a. principal a \ x \ principal a \ u) \ x \ u" unfolding principal_below_iff_mem_rep by (simp add: below_def subset_eq) @@ -271,68 +241,155 @@ apply (simp add: rep_eq) done +subsubsection {* Principal ideals approximate all elements *} + +lemma compact_principal [simp]: "compact (principal a)" +by (rule compactI2, simp add: principal_below_iff_mem_rep rep_contlub) + +text {* Construct a chain whose lub is the same as a given ideal *} + +lemma obtain_principal_chain: + obtains Y where "\i. Y i \ Y (Suc i)" and "x = (\i. principal (Y i))" +proof - + obtain count :: "'a \ nat" where inj: "inj count" + using countable .. + def enum \ "\i. THE a. count a = i" + have enum_count [simp]: "\x. enum (count x) = x" + unfolding enum_def by (simp add: inj_eq [OF inj]) + def a \ "LEAST i. enum i \ rep x" + def b \ "\i. LEAST j. enum j \ rep x \ \ enum j \ enum i" + def c \ "\i j. LEAST k. enum k \ rep x \ enum i \ enum k \ enum j \ enum k" + def P \ "\i. \j. enum j \ rep x \ \ enum j \ enum i" + def X \ "nat_rec a (\n i. if P i then c i (b i) else i)" + have X_0: "X 0 = a" unfolding X_def by simp + have X_Suc: "\n. X (Suc n) = (if P (X n) then c (X n) (b (X n)) else X n)" + unfolding X_def by simp + have a_mem: "enum a \ rep x" + unfolding a_def + apply (rule LeastI_ex) + apply (cut_tac ideal_rep [of x]) + apply (drule idealD1) + apply (clarify, rename_tac a) + apply (rule_tac x="count a" in exI, simp) + done + have b: "\i. P i \ enum i \ rep x + \ enum (b i) \ rep x \ \ enum (b i) \ enum i" + unfolding P_def b_def by (erule LeastI2_ex, simp) + have c: "\i j. enum i \ rep x \ enum j \ rep x + \ enum (c i j) \ rep x \ enum i \ enum (c i j) \ enum j \ enum (c i j)" + unfolding c_def + apply (drule (1) idealD2 [OF ideal_rep], clarify) + apply (rule_tac a="count z" in LeastI2, simp, simp) + done + have X_mem: "\n. enum (X n) \ rep x" + apply (induct_tac n) + apply (simp add: X_0 a_mem) + apply (clarsimp simp add: X_Suc, rename_tac n) + apply (simp add: b c) + done + have X_chain: "\n. enum (X n) \ enum (X (Suc n))" + apply (clarsimp simp add: X_Suc r_refl) + apply (simp add: b c X_mem) + done + have less_b: "\n i. n < b i \ enum n \ rep x \ enum n \ enum i" + unfolding b_def by (drule not_less_Least, simp) + have X_covers: "\n. \k\n. enum k \ rep x \ enum k \ enum (X n)" + apply (induct_tac n) + apply (clarsimp simp add: X_0 a_def) + apply (drule_tac k=0 in Least_le, simp add: r_refl) + apply (clarsimp, rename_tac n k) + apply (erule le_SucE) + apply (rule r_trans [OF _ X_chain], simp) + apply (case_tac "P (X n)", simp add: X_Suc) + apply (rule_tac x="b (X n)" and y="Suc n" in linorder_cases) + apply (simp only: less_Suc_eq_le) + apply (drule spec, drule (1) mp, simp add: b X_mem) + apply (simp add: c X_mem) + apply (drule (1) less_b) + apply (erule r_trans) + apply (simp add: b c X_mem) + apply (simp add: X_Suc) + apply (simp add: P_def) + done + have 1: "\i. enum (X i) \ enum (X (Suc i))" + by (simp add: X_chain) + have 2: "x = (\n. principal (enum (X n)))" + apply (simp add: eq_iff rep_contlub 1 rep_principal) + apply (auto, rename_tac a) + apply (subgoal_tac "\i. a = enum i", erule exE) + apply (rule_tac x=i in exI, simp add: X_covers) + apply (rule_tac x="count a" in exI, simp) + apply (erule idealD3 [OF ideal_rep]) + apply (rule X_mem) + done + from 1 2 show ?thesis .. +qed + +lemma principal_induct: + assumes adm: "adm P" + assumes P: "\a. P (principal a)" + shows "P x" +apply (rule obtain_principal_chain [of x]) +apply (simp add: admD [OF adm] P) +done + +lemma principal_induct2: + "\\y. adm (\x. P x y); \x. adm (\y. P x y); + \a b. P (principal a) (principal b)\ \ P x y" +apply (rule_tac x=y in spec) +apply (rule_tac x=x in principal_induct, simp) +apply (rule allI, rename_tac y) +apply (rule_tac x=y in principal_induct, simp) +apply simp +done + +lemma compact_imp_principal: "compact x \ \a. x = principal a" +apply (rule obtain_principal_chain [of x]) +apply (drule adm_compact_neq [OF _ cont_id]) +apply (subgoal_tac "chain (\i. principal (Y i))") +apply (drule (2) admD2, fast, simp) +done + +lemma obtain_compact_chain: + obtains Y :: "nat \ 'b" + where "chain Y" and "\i. compact (Y i)" and "x = (\i. Y i)" +apply (rule obtain_principal_chain [of x]) +apply (rule_tac Y="\i. principal (Y i)" in that, simp_all) +done + subsection {* Defining functions in terms of basis elements *} definition basis_fun :: "('a::type \ 'c::cpo) \ 'b \ 'c" where "basis_fun = (\f. (\ x. lub (f ` rep x)))" -lemma basis_fun_lemma0: - fixes f :: "'a::type \ 'c::cpo" - assumes f_mono: "\a b. a \ b \ f a \ f b" - shows "\u. f ` take i ` rep x <<| u" -apply (rule finite_directed_has_lub) -apply (rule finite_imageI) -apply (rule finite_take_rep) -apply (subst image_image) -apply (rule directed_image_ideal) -apply (rule ideal_rep) -apply (rule f_mono) -apply (erule take_mono) -done - -lemma basis_fun_lemma1: - fixes f :: "'a::type \ 'c::cpo" - assumes f_mono: "\a b. a \ b \ f a \ f b" - shows "chain (\i. lub (f ` take i ` rep x))" - apply (rule chainI) - apply (rule is_lub_thelub0) - apply (rule basis_fun_lemma0, erule f_mono) - apply (rule is_ubI, clarsimp, rename_tac a) - apply (rule below_trans [OF f_mono [OF take_chain]]) - apply (rule is_ub_thelub0) - apply (rule basis_fun_lemma0, erule f_mono) - apply simp -done - -lemma basis_fun_lemma2: - fixes f :: "'a::type \ 'c::cpo" - assumes f_mono: "\a b. a \ b \ f a \ f b" - shows "f ` rep x <<| (\i. lub (f ` take i ` rep x))" - apply (rule is_lubI) - apply (rule ub_imageI, rename_tac a) - apply (cut_tac a=a in take_covers, erule exE, rename_tac i) - apply (erule subst) - apply (rule rev_below_trans) - apply (rule_tac x=i in is_ub_thelub) - apply (rule basis_fun_lemma1, erule f_mono) - apply (rule is_ub_thelub0) - apply (rule basis_fun_lemma0, erule f_mono) - apply simp - apply (rule is_lub_thelub [OF _ ub_rangeI]) - apply (rule basis_fun_lemma1, erule f_mono) - apply (rule is_lub_thelub0) - apply (rule basis_fun_lemma0, erule f_mono) - apply (rule is_ubI, clarsimp, rename_tac a) - apply (rule below_trans [OF f_mono [OF take_less]]) - apply (erule (1) ub_imageD) -done - lemma basis_fun_lemma: fixes f :: "'a::type \ 'c::cpo" assumes f_mono: "\a b. a \ b \ f a \ f b" shows "\u. f ` rep x <<| u" -by (rule exI, rule basis_fun_lemma2, erule f_mono) +proof - + obtain Y where Y: "\i. Y i \ Y (Suc i)" + and x: "x = (\i. principal (Y i))" + by (rule obtain_principal_chain [of x]) + have chain: "chain (\i. f (Y i))" + by (rule chainI, simp add: f_mono Y) + have rep_x: "rep x = (\n. {a. a \ Y n})" + by (simp add: x rep_contlub Y rep_principal) + have "f ` rep x <<| (\n. f (Y n))" + apply (rule is_lubI) + apply (rule ub_imageI, rename_tac a) + apply (clarsimp simp add: rep_x) + apply (drule f_mono) + apply (erule below_trans) + apply (rule is_ub_thelub [OF chain]) + apply (rule is_lub_thelub [OF chain]) + apply (rule ub_rangeI) + apply (drule_tac x="Y i" in ub_imageD) + apply (simp add: rep_x, fast intro: r_refl) + apply assumption + done + thus ?thesis .. +qed lemma basis_fun_beta: fixes f :: "'a::type \ 'c::cpo" @@ -345,13 +402,13 @@ show cont: "cont (\x. lub (f ` rep x))" apply (rule contI2) apply (rule monofunI) - apply (rule is_lub_thelub0 [OF lub ub_imageI]) - apply (rule is_ub_thelub0 [OF lub imageI]) + apply (rule is_lub_thelub_ex [OF lub ub_imageI]) + apply (rule is_ub_thelub_ex [OF lub imageI]) apply (erule (1) subsetD [OF rep_mono]) - apply (rule is_lub_thelub0 [OF lub ub_imageI]) + apply (rule is_lub_thelub_ex [OF lub ub_imageI]) apply (simp add: rep_contlub, clarify) apply (erule rev_below_trans [OF is_ub_thelub]) - apply (erule is_ub_thelub0 [OF lub imageI]) + apply (erule is_ub_thelub_ex [OF lub imageI]) done qed @@ -371,113 +428,15 @@ shows "basis_fun f \ basis_fun g" apply (rule below_cfun_ext) apply (simp only: basis_fun_beta f_mono g_mono) - apply (rule is_lub_thelub0) + apply (rule is_lub_thelub_ex) apply (rule basis_fun_lemma, erule f_mono) apply (rule ub_imageI, rename_tac a) apply (rule below_trans [OF below]) - apply (rule is_ub_thelub0) + apply (rule is_ub_thelub_ex) apply (rule basis_fun_lemma, erule g_mono) apply (erule imageI) done -lemma compact_principal [simp]: "compact (principal a)" -by (rule compactI2, simp add: principal_below_iff_mem_rep rep_contlub) - -subsection {* Bifiniteness of ideal completions *} - -definition - completion_approx :: "nat \ 'b \ 'b" where - "completion_approx = (\i. basis_fun (\a. principal (take i a)))" - -lemma completion_approx_beta: - "completion_approx i\x = (\a\rep x. principal (take i a))" -unfolding completion_approx_def -by (simp add: basis_fun_beta principal_mono take_mono) - -lemma completion_approx_principal: - "completion_approx i\(principal a) = principal (take i a)" -unfolding completion_approx_def -by (simp add: basis_fun_principal principal_mono take_mono) - -lemma chain_completion_approx: "chain completion_approx" -unfolding completion_approx_def -apply (rule chainI) -apply (rule basis_fun_mono) -apply (erule principal_mono [OF take_mono]) -apply (erule principal_mono [OF take_mono]) -apply (rule principal_mono [OF take_chain]) -done - -lemma lub_completion_approx: "(\i. completion_approx i\x) = x" -unfolding completion_approx_beta - apply (subst image_image [where f=principal, symmetric]) - apply (rule unique_lub [OF _ lub_principal_rep]) - apply (rule basis_fun_lemma2, erule principal_mono) -done - -lemma completion_approx_eq_principal: - "\a\rep x. completion_approx i\x = principal (take i a)" -unfolding completion_approx_beta - apply (subst image_image [where f=principal, symmetric]) - apply (subgoal_tac "finite (principal ` take i ` rep x)") - apply (subgoal_tac "directed (principal ` take i ` rep x)") - apply (drule (1) lub_finite_directed_in_self, fast) - apply (subst image_image) - apply (rule directed_image_ideal) - apply (rule ideal_rep) - apply (erule principal_mono [OF take_mono]) - apply (rule finite_imageI) - apply (rule finite_take_rep) -done - -lemma completion_approx_idem: - "completion_approx i\(completion_approx i\x) = completion_approx i\x" -using completion_approx_eq_principal [where i=i and x=x] -by (auto simp add: completion_approx_principal take_take) - -lemma finite_fixes_completion_approx: - "finite {x. completion_approx i\x = x}" (is "finite ?S") -apply (subgoal_tac "?S \ principal ` range (take i)") -apply (erule finite_subset) -apply (rule finite_imageI) -apply (rule finite_range_take) -apply (clarify, erule subst) -apply (cut_tac x=x and i=i in completion_approx_eq_principal) -apply fast -done - -lemma principal_induct: - assumes adm: "adm P" - assumes P: "\a. P (principal a)" - shows "P x" - apply (subgoal_tac "P (\i. completion_approx i\x)") - apply (simp add: lub_completion_approx) - apply (rule admD [OF adm]) - apply (simp add: chain_completion_approx) - apply (cut_tac x=x and i=i in completion_approx_eq_principal) - apply (clarify, simp add: P) -done - -lemma principal_induct2: - "\\y. adm (\x. P x y); \x. adm (\y. P x y); - \a b. P (principal a) (principal b)\ \ P x y" -apply (rule_tac x=y in spec) -apply (rule_tac x=x in principal_induct, simp) -apply (rule allI, rename_tac y) -apply (rule_tac x=y in principal_induct, simp) -apply simp -done - -lemma compact_imp_principal: "compact x \ \a. x = principal a" -apply (drule adm_compact_neq [OF _ cont_id]) -apply (drule admD2 [where Y="\n. completion_approx n\x"]) -apply (simp add: chain_completion_approx) -apply (simp add: lub_completion_approx) -apply (erule exE, erule ssubst) -apply (cut_tac i=i and x=x in completion_approx_eq_principal) -apply (clarify, erule exI) -done - end end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/ConvexPD.thy --- a/src/HOLCF/ConvexPD.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/ConvexPD.thy Wed Oct 06 10:49:27 2010 -0700 @@ -116,27 +116,6 @@ apply (simp add: 4) done -lemma pd_take_convex_chain: - "pd_take n t \\ pd_take (Suc n) t" -apply (induct t rule: pd_basis_induct) -apply (simp add: compact_basis.take_chain) -apply (simp add: PDPlus_convex_mono) -done - -lemma pd_take_convex_le: "pd_take i t \\ t" -apply (induct t rule: pd_basis_induct) -apply (simp add: compact_basis.take_less) -apply (simp add: PDPlus_convex_mono) -done - -lemma pd_take_convex_mono: - "t \\ u \ pd_take n t \\ pd_take n u" -apply (erule convex_le_induct) -apply (erule (1) convex_le_trans) -apply (simp add: compact_basis.take_mono) -apply (simp add: PDPlus_convex_mono) -done - subsection {* Type definition *} @@ -144,7 +123,7 @@ "{S::'a pd_basis set. convex_le.ideal S}" by (fast intro: convex_le.ideal_principal) -instantiation convex_pd :: (profinite) below +instantiation convex_pd :: (sfp) below begin definition @@ -153,18 +132,18 @@ instance .. end -instance convex_pd :: (profinite) po -by (rule convex_le.typedef_ideal_po - [OF type_definition_convex_pd below_convex_pd_def]) +instance convex_pd :: (sfp) po +using type_definition_convex_pd below_convex_pd_def +by (rule convex_le.typedef_ideal_po) -instance convex_pd :: (profinite) cpo -by (rule convex_le.typedef_ideal_cpo - [OF type_definition_convex_pd below_convex_pd_def]) +instance convex_pd :: (sfp) cpo +using type_definition_convex_pd below_convex_pd_def +by (rule convex_le.typedef_ideal_cpo) lemma Rep_convex_pd_lub: "chain Y \ Rep_convex_pd (\i. Y i) = (\i. Rep_convex_pd (Y i))" -by (rule convex_le.typedef_ideal_rep_contlub - [OF type_definition_convex_pd below_convex_pd_def]) +using type_definition_convex_pd below_convex_pd_def +by (rule convex_le.typedef_ideal_rep_contlub) lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)" by (rule Rep_convex_pd [unfolded mem_Collect_eq]) @@ -179,18 +158,13 @@ by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal) interpretation convex_pd: - ideal_completion convex_le pd_take convex_principal Rep_convex_pd + ideal_completion convex_le convex_principal Rep_convex_pd apply unfold_locales -apply (rule pd_take_convex_le) -apply (rule pd_take_idem) -apply (erule pd_take_convex_mono) -apply (rule pd_take_convex_chain) -apply (rule finite_range_pd_take) -apply (rule pd_take_covers) apply (rule ideal_Rep_convex_pd) apply (erule Rep_convex_pd_lub) apply (rule Rep_convex_principal) apply (simp only: below_convex_pd_def) +apply (rule pd_basis_countable) done text {* Convex powerdomain is pointed *} @@ -198,42 +172,12 @@ lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \ ys" by (induct ys rule: convex_pd.principal_induct, simp, simp) -instance convex_pd :: (bifinite) pcpo +instance convex_pd :: (sfp) pcpo by intro_classes (fast intro: convex_pd_minimal) lemma inst_convex_pd_pcpo: "\ = convex_principal (PDUnit compact_bot)" by (rule convex_pd_minimal [THEN UU_I, symmetric]) -text {* Convex powerdomain is profinite *} - -instantiation convex_pd :: (profinite) profinite -begin - -definition - approx_convex_pd_def: "approx = convex_pd.completion_approx" - -instance -apply (intro_classes, unfold approx_convex_pd_def) -apply (rule convex_pd.chain_completion_approx) -apply (rule convex_pd.lub_completion_approx) -apply (rule convex_pd.completion_approx_idem) -apply (rule convex_pd.finite_fixes_completion_approx) -done - -end - -instance convex_pd :: (bifinite) bifinite .. - -lemma approx_convex_principal [simp]: - "approx n\(convex_principal t) = convex_principal (pd_take n t)" -unfolding approx_convex_pd_def -by (rule convex_pd.completion_approx_principal) - -lemma approx_eq_convex_principal: - "\t\Rep_convex_pd xs. approx n\xs = convex_principal (pd_take n t)" -unfolding approx_convex_pd_def -by (rule convex_pd.completion_approx_eq_principal) - subsection {* Monadic unit and plus *} @@ -269,16 +213,6 @@ by (simp add: convex_pd.basis_fun_principal convex_pd.basis_fun_mono PDPlus_convex_mono) -lemma approx_convex_unit [simp]: - "approx n\{x}\ = {approx n\x}\" -apply (induct x rule: compact_basis.principal_induct, simp) -apply (simp add: approx_Rep_compact_basis) -done - -lemma approx_convex_plus [simp]: - "approx n\(xs +\ ys) = approx n\xs +\ approx n\ys" -by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp) - interpretation convex_add: semilattice convex_add proof fix xs ys zs :: "'a convex_pd" show "(xs +\ ys) +\ zs = xs +\ (ys +\ zs)" @@ -336,14 +270,20 @@ unfolding po_eq_conv by simp lemma convex_unit_strict [simp]: "{\}\ = \" -unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp +using convex_unit_Rep_compact_basis [of compact_bot] +by (simp add: inst_convex_pd_pcpo) lemma convex_unit_strict_iff [simp]: "{x}\ = \ \ x = \" unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff) -lemma compact_convex_unit_iff [simp]: - "compact {x}\ \ compact x" -unfolding profinite_compact_iff by simp +lemma compact_convex_unit: "compact x \ compact {x}\" +by (auto dest!: compact_basis.compact_imp_principal) + +lemma compact_convex_unit_iff [simp]: "compact {x}\ \ compact x" +apply (safe elim!: compact_convex_unit) +apply (simp only: compact_def convex_unit_below_iff [symmetric]) +apply (erule adm_subst [OF cont_Rep_CFun2]) +done lemma compact_convex_plus [simp]: "\compact xs; compact ys\ \ compact (xs +\ ys)" @@ -441,32 +381,20 @@ unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit) -subsection {* Map and join *} +subsection {* Map *} definition convex_map :: "('a \ 'b) \ 'a convex_pd \ 'b convex_pd" where "convex_map = (\ f xs. convex_bind\xs\(\ x. {f\x}\))" -definition - convex_join :: "'a convex_pd convex_pd \ 'a convex_pd" where - "convex_join = (\ xss. convex_bind\xss\(\ xs. xs))" - lemma convex_map_unit [simp]: - "convex_map\f\(convex_unit\x) = convex_unit\(f\x)" + "convex_map\f\{x}\ = {f\x}\" unfolding convex_map_def by simp lemma convex_map_plus [simp]: "convex_map\f\(xs +\ ys) = convex_map\f\xs +\ convex_map\f\ys" unfolding convex_map_def by simp -lemma convex_join_unit [simp]: - "convex_join\{xs}\ = xs" -unfolding convex_join_def by simp - -lemma convex_join_plus [simp]: - "convex_join\(xss +\ yss) = convex_join\xss +\ convex_join\yss" -unfolding convex_join_def by simp - lemma convex_map_ident: "convex_map\(\ x. x)\xs = xs" by (induct xs rule: convex_pd_induct, simp_all) @@ -477,6 +405,137 @@ "convex_map\f\(convex_map\g\xs) = convex_map\(\ x. f\(g\x))\xs" by (induct xs rule: convex_pd_induct, simp_all) +lemma ep_pair_convex_map: "ep_pair e p \ ep_pair (convex_map\e) (convex_map\p)" +apply default +apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse) +apply (induct_tac y rule: convex_pd_induct) +apply (simp_all add: ep_pair.e_p_below monofun_cfun) +done + +lemma deflation_convex_map: "deflation d \ deflation (convex_map\d)" +apply default +apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem) +apply (induct_tac x rule: convex_pd_induct) +apply (simp_all add: deflation.below monofun_cfun) +done + +(* FIXME: long proof! *) +lemma finite_deflation_convex_map: + assumes "finite_deflation d" shows "finite_deflation (convex_map\d)" +proof (rule finite_deflation_intro) + interpret d: finite_deflation d by fact + have "deflation d" by fact + thus "deflation (convex_map\d)" by (rule deflation_convex_map) + have "finite (range (\x. d\x))" by (rule d.finite_range) + hence "finite (Rep_compact_basis -` range (\x. d\x))" + by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) + hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp + hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" + by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) + hence *: "finite (convex_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp + hence "finite (range (\xs. convex_map\d\xs))" + apply (rule rev_finite_subset) + apply clarsimp + apply (induct_tac xs rule: convex_pd.principal_induct) + apply (simp add: adm_mem_finite *) + apply (rename_tac t, induct_tac t rule: pd_basis_induct) + apply (simp only: convex_unit_Rep_compact_basis [symmetric] convex_map_unit) + apply simp + apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDUnit) + apply (rule range_eqI) + apply (erule sym) + apply (rule exI) + apply (rule Abs_compact_basis_inverse [symmetric]) + apply (simp add: d.compact) + apply (simp only: convex_plus_principal [symmetric] convex_map_plus) + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDPlus) + done + thus "finite {xs. convex_map\d\xs = xs}" + by (rule finite_range_imp_finite_fixes) +qed + +subsection {* Convex powerdomain is an SFP domain *} + +definition + convex_approx :: "nat \ udom convex_pd \ udom convex_pd" +where + "convex_approx = (\i. convex_map\(udom_approx i))" + +lemma convex_approx: "approx_chain convex_approx" +proof (rule approx_chain.intro) + show "chain (\i. convex_approx i)" + unfolding convex_approx_def by simp + show "(\i. convex_approx i) = ID" + unfolding convex_approx_def + by (simp add: lub_distribs convex_map_ID) + show "\i. finite_deflation (convex_approx i)" + unfolding convex_approx_def + by (intro finite_deflation_convex_map finite_deflation_udom_approx) +qed + +definition convex_sfp :: "sfp \ sfp" +where "convex_sfp = sfp_fun1 convex_approx convex_map" + +lemma cast_convex_sfp: + "cast\(convex_sfp\A) = + udom_emb convex_approx oo convex_map\(cast\A) oo udom_prj convex_approx" +unfolding convex_sfp_def +apply (rule cast_sfp_fun1 [OF convex_approx]) +apply (erule finite_deflation_convex_map) +done + +instantiation convex_pd :: (sfp) sfp +begin + +definition + "emb = udom_emb convex_approx oo convex_map\emb" + +definition + "prj = convex_map\prj oo udom_prj convex_approx" + +definition + "sfp (t::'a convex_pd itself) = convex_sfp\SFP('a)" + +instance proof + show "ep_pair emb (prj :: udom \ 'a convex_pd)" + unfolding emb_convex_pd_def prj_convex_pd_def + using ep_pair_udom [OF convex_approx] + by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj) +next + show "cast\SFP('a convex_pd) = emb oo (prj :: udom \ 'a convex_pd)" + unfolding emb_convex_pd_def prj_convex_pd_def sfp_convex_pd_def cast_convex_sfp + by (simp add: cast_SFP oo_def expand_cfun_eq convex_map_map) +qed + +end + +text {* SFP of type constructor = type combinator *} + +lemma SFP_convex: "SFP('a convex_pd) = convex_sfp\SFP('a)" +by (rule sfp_convex_pd_def) + + +subsection {* Join *} + +definition + convex_join :: "'a convex_pd convex_pd \ 'a convex_pd" where + "convex_join = (\ xss. convex_bind\xss\(\ xs. xs))" + +lemma convex_join_unit [simp]: + "convex_join\{xs}\ = xs" +unfolding convex_join_def by simp + +lemma convex_join_plus [simp]: + "convex_join\(xss +\ yss) = convex_join\xss +\ convex_join\yss" +unfolding convex_join_def by simp + lemma convex_join_map_unit: "convex_join\(convex_map\convex_unit\xs) = xs" by (induct xs rule: convex_pd_induct, simp_all) @@ -490,24 +549,6 @@ convex_map\f\(convex_join\xss)" by (induct xss rule: convex_pd_induct, simp_all) -lemma convex_map_approx: "convex_map\(approx n)\xs = approx n\xs" -by (induct xs rule: convex_pd_induct, simp_all) - -lemma ep_pair_convex_map: - "ep_pair e p \ ep_pair (convex_map\e) (convex_map\p)" -apply default -apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse) -apply (induct_tac y rule: convex_pd_induct) -apply (simp_all add: ep_pair.e_p_below monofun_cfun) -done - -lemma deflation_convex_map: "deflation d \ deflation (convex_map\d)" -apply default -apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem) -apply (induct_tac x rule: convex_pd_induct) -apply (simp_all add: deflation.below monofun_cfun) -done - subsection {* Conversions to other powerdomains *} @@ -536,10 +577,6 @@ "convex_to_upper\(xs +\ ys) = convex_to_upper\xs +\ convex_to_upper\ys" by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp) -lemma approx_convex_to_upper: - "approx i\(convex_to_upper\xs) = convex_to_upper\(approx i\xs)" -by (induct xs rule: convex_pd_induct, simp, simp, simp) - lemma convex_to_upper_bind [simp]: "convex_to_upper\(convex_bind\xs\f) = upper_bind\(convex_to_upper\xs)\(convex_to_upper oo f)" @@ -579,10 +616,6 @@ "convex_to_lower\(xs +\ ys) = convex_to_lower\xs +\ convex_to_lower\ys" by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp) -lemma approx_convex_to_lower: - "approx i\(convex_to_lower\xs) = convex_to_lower\(approx i\xs)" -by (induct xs rule: convex_pd_induct, simp, simp, simp) - lemma convex_to_lower_bind [simp]: "convex_to_lower\(convex_bind\xs\f) = lower_bind\(convex_to_lower\xs)\(convex_to_lower oo f)" diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Cprod.thy --- a/src/HOLCF/Cprod.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Cprod.thy Wed Oct 06 10:49:27 2010 -0700 @@ -5,7 +5,7 @@ header {* The cpo of cartesian products *} theory Cprod -imports Bifinite +imports Algebraic begin default_sort cpo @@ -40,4 +40,62 @@ lemma csplit_Pair [simp]: "csplit\f\(x, y) = f\x\y" by (simp add: csplit_def) +subsection {* Cartesian product is an SFP domain *} + +definition + prod_approx :: "nat \ udom \ udom \ udom \ udom" +where + "prod_approx = (\i. cprod_map\(udom_approx i)\(udom_approx i))" + +lemma prod_approx: "approx_chain prod_approx" +proof (rule approx_chain.intro) + show "chain (\i. prod_approx i)" + unfolding prod_approx_def by simp + show "(\i. prod_approx i) = ID" + unfolding prod_approx_def + by (simp add: lub_distribs cprod_map_ID) + show "\i. finite_deflation (prod_approx i)" + unfolding prod_approx_def + by (intro finite_deflation_cprod_map finite_deflation_udom_approx) +qed + +definition prod_sfp :: "sfp \ sfp \ sfp" +where "prod_sfp = sfp_fun2 prod_approx cprod_map" + +lemma cast_prod_sfp: + "cast\(prod_sfp\A\B) = udom_emb prod_approx oo + cprod_map\(cast\A)\(cast\B) oo udom_prj prod_approx" +unfolding prod_sfp_def +apply (rule cast_sfp_fun2 [OF prod_approx]) +apply (erule (1) finite_deflation_cprod_map) +done + +instantiation prod :: (sfp, sfp) sfp +begin + +definition + "emb = udom_emb prod_approx oo cprod_map\emb\emb" + +definition + "prj = cprod_map\prj\prj oo udom_prj prod_approx" + +definition + "sfp (t::('a \ 'b) itself) = prod_sfp\SFP('a)\SFP('b)" + +instance proof + show "ep_pair emb (prj :: udom \ 'a \ 'b)" + unfolding emb_prod_def prj_prod_def + using ep_pair_udom [OF prod_approx] + by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj) +next + show "cast\SFP('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" + unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp + by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map) +qed + end + +lemma SFP_prod: "SFP('a::sfp \ 'b::sfp) = prod_sfp\SFP('a)\SFP('b)" +by (rule sfp_prod_def) + +end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Eventual.thy --- a/src/HOLCF/Eventual.thy Tue Oct 05 17:53:00 2010 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,153 +0,0 @@ -(* Title: HOLCF/Eventual.thy - Author: Brian Huffman -*) - -header {* Eventually-constant sequences *} - -theory Eventual -imports Infinite_Set -begin - -subsection {* Lemmas about MOST *} - -lemma MOST_INFM: - assumes inf: "infinite (UNIV::'a set)" - shows "MOST x::'a. P x \ INFM x::'a. P x" - unfolding Alm_all_def Inf_many_def - apply (auto simp add: Collect_neg_eq) - apply (drule (1) finite_UnI) - apply (simp add: Compl_partition2 inf) - done - -lemma MOST_SucI: "MOST n. P n \ MOST n. P (Suc n)" -by (rule MOST_inj [OF _ inj_Suc]) - -lemma MOST_SucD: "MOST n. P (Suc n) \ MOST n. P n" -unfolding MOST_nat -apply (clarify, rule_tac x="Suc m" in exI, clarify) -apply (erule Suc_lessE, simp) -done - -lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \ (MOST n. P n)" -by (rule iffI [OF MOST_SucD MOST_SucI]) - -lemma INFM_finite_Bex_distrib: - "finite A \ (INFM y. \x\A. P x y) \ (\x\A. INFM y. P x y)" -by (induct set: finite, simp, simp add: INFM_disj_distrib) - -lemma MOST_finite_Ball_distrib: - "finite A \ (MOST y. \x\A. P x y) \ (\x\A. MOST y. P x y)" -by (induct set: finite, simp, simp add: MOST_conj_distrib) - -lemma MOST_ge_nat: "MOST n::nat. m \ n" -unfolding MOST_nat_le by fast - -subsection {* Eventually constant sequences *} - -definition - eventually_constant :: "(nat \ 'a) \ bool" -where - "eventually_constant S = (\x. MOST i. S i = x)" - -lemma eventually_constant_MOST_MOST: - "eventually_constant S \ (MOST m. MOST n. S n = S m)" -unfolding eventually_constant_def MOST_nat -apply safe -apply (rule_tac x=m in exI, clarify) -apply (rule_tac x=m in exI, clarify) -apply simp -apply fast -done - -lemma eventually_constantI: "MOST i. S i = x \ eventually_constant S" -unfolding eventually_constant_def by fast - -lemma eventually_constant_comp: - "eventually_constant (\i. S i) \ eventually_constant (\i. f (S i))" -unfolding eventually_constant_def -apply (erule exE, rule_tac x="f x" in exI) -apply (erule MOST_mono, simp) -done - -lemma eventually_constant_Suc_iff: - "eventually_constant (\i. S (Suc i)) \ eventually_constant (\i. S i)" -unfolding eventually_constant_def -by (subst MOST_Suc_iff, rule refl) - -lemma eventually_constant_SucD: - "eventually_constant (\i. S (Suc i)) \ eventually_constant (\i. S i)" -by (rule eventually_constant_Suc_iff [THEN iffD1]) - -subsection {* Limits of eventually constant sequences *} - -definition - eventual :: "(nat \ 'a) \ 'a" where - "eventual S = (THE x. MOST i. S i = x)" - -lemma eventual_eqI: "MOST i. S i = x \ eventual S = x" -unfolding eventual_def -apply (rule the_equality, assumption) -apply (rename_tac y) -apply (subgoal_tac "MOST i::nat. y = x", simp) -apply (erule MOST_rev_mp) -apply (erule MOST_rev_mp) -apply simp -done - -lemma MOST_eq_eventual: - "eventually_constant S \ MOST i. S i = eventual S" -unfolding eventually_constant_def -by (erule exE, simp add: eventual_eqI) - -lemma eventual_mem_range: - "eventually_constant S \ eventual S \ range S" -apply (drule MOST_eq_eventual) -apply (simp only: MOST_nat_le, clarify) -apply (drule spec, drule mp, rule order_refl) -apply (erule range_eqI [OF sym]) -done - -lemma eventually_constant_MOST_iff: - assumes S: "eventually_constant S" - shows "(MOST n. P (S n)) \ P (eventual S)" -apply (subgoal_tac "(MOST n. P (S n)) \ (MOST n::nat. P (eventual S))") -apply simp -apply (rule iffI) -apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]]) -apply (erule MOST_mono, force) -apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]]) -apply (erule MOST_mono, simp) -done - -lemma MOST_eventual: - "\eventually_constant S; MOST n. P (S n)\ \ P (eventual S)" -proof - - assume "eventually_constant S" - hence "MOST n. S n = eventual S" - by (rule MOST_eq_eventual) - moreover assume "MOST n. P (S n)" - ultimately have "MOST n. S n = eventual S \ P (S n)" - by (rule MOST_conj_distrib [THEN iffD2, OF conjI]) - hence "MOST n::nat. P (eventual S)" - by (rule MOST_mono) auto - thus ?thesis by simp -qed - -lemma eventually_constant_MOST_Suc_eq: - "eventually_constant S \ MOST n. S (Suc n) = S n" -apply (drule MOST_eq_eventual) -apply (frule MOST_Suc_iff [THEN iffD2]) -apply (erule MOST_rev_mp) -apply (erule MOST_rev_mp) -apply simp -done - -lemma eventual_comp: - "eventually_constant S \ eventual (\i. f (S i)) = f (eventual (\i. S i))" -apply (rule eventual_eqI) -apply (rule MOST_mono) -apply (erule MOST_eq_eventual) -apply simp -done - -end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/HOLCF.thy --- a/src/HOLCF/HOLCF.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/HOLCF.thy Wed Oct 06 10:49:27 2010 -0700 @@ -45,8 +45,6 @@ lemmas expand_cfun_less = expand_cfun_below lemmas less_cfun_ext = below_cfun_ext lemmas injection_less = injection_below -lemmas approx_less = approx_below -lemmas profinite_less_ext = profinite_below_ext lemmas less_up_def = below_up_def lemmas not_Iup_less = not_Iup_below lemmas Iup_less = Iup_below diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/IsaMakefile Wed Oct 06 10:49:27 2010 -0700 @@ -48,7 +48,6 @@ Deflation.thy \ Domain.thy \ Domain_Aux.thy \ - Eventual.thy \ Ffun.thy \ Fixrec.thy \ Fix.thy \ diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Library/Strict_Fun.thy --- a/src/HOLCF/Library/Strict_Fun.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Library/Strict_Fun.thy Wed Oct 06 10:49:27 2010 -0700 @@ -1,4 +1,4 @@ -(* Title: HOLCF/ex/Strict_Fun.thy +(* Title: HOLCF/Library/Strict_Fun.thy Author: Brian Huffman *) @@ -143,96 +143,78 @@ deflation_strict `deflation d1` `deflation d2`) qed -subsection {* Strict function space is bifinite *} +subsection {* Strict function space is an SFP domain *} + +definition + sfun_approx :: "nat \ (udom \! udom) \ (udom \! udom)" +where + "sfun_approx = (\i. sfun_map\(udom_approx i)\(udom_approx i))" -instantiation sfun :: (bifinite, bifinite) bifinite +lemma sfun_approx: "approx_chain sfun_approx" +proof (rule approx_chain.intro) + show "chain (\i. sfun_approx i)" + unfolding sfun_approx_def by simp + show "(\i. sfun_approx i) = ID" + unfolding sfun_approx_def + by (simp add: lub_distribs sfun_map_ID) + show "\i. finite_deflation (sfun_approx i)" + unfolding sfun_approx_def + by (intro finite_deflation_sfun_map finite_deflation_udom_approx) +qed + +definition sfun_sfp :: "sfp \ sfp \ sfp" +where "sfun_sfp = sfp_fun2 sfun_approx sfun_map" + +lemma cast_sfun_sfp: + "cast\(sfun_sfp\A\B) = + udom_emb sfun_approx oo sfun_map\(cast\A)\(cast\B) oo udom_prj sfun_approx" +unfolding sfun_sfp_def +apply (rule cast_sfp_fun2 [OF sfun_approx]) +apply (erule (1) finite_deflation_sfun_map) +done + +instantiation sfun :: (sfp, sfp) sfp begin definition - "approx = (\i. sfun_map\(approx i)\(approx i))" + "emb = udom_emb sfun_approx oo sfun_map\prj\emb" + +definition + "prj = sfun_map\emb\prj oo udom_prj sfun_approx" + +definition + "sfp (t::('a \! 'b) itself) = sfun_sfp\SFP('a)\SFP('b)" instance proof - show "chain (approx :: nat \ ('a \! 'b) \ ('a \! 'b))" - unfolding approx_sfun_def by simp -next - fix x :: "'a \! 'b" - show "(\i. approx i\x) = x" - unfolding approx_sfun_def - by (simp add: lub_distribs sfun_map_ID [unfolded ID_def]) + show "ep_pair emb (prj :: udom \ 'a \! 'b)" + unfolding emb_sfun_def prj_sfun_def + using ep_pair_udom [OF sfun_approx] + by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj) next - fix i :: nat and x :: "'a \! 'b" - show "approx i\(approx i\x) = approx i\x" - unfolding approx_sfun_def - by (intro deflation.idem deflation_sfun_map deflation_approx) -next - fix i :: nat - show "finite {x::'a \! 'b. approx i\x = x}" - unfolding approx_sfun_def - by (intro finite_deflation.finite_fixes - finite_deflation_sfun_map - finite_deflation_approx) + show "cast\SFP('a \! 'b) = emb oo (prj :: udom \ 'a \! 'b)" + unfolding emb_sfun_def prj_sfun_def sfp_sfun_def cast_sfun_sfp + by (simp add: cast_SFP oo_def expand_cfun_eq sfun_map_map) qed end -subsection {* Strict function space is representable *} - -instantiation sfun :: (rep, rep) rep -begin - -definition - "emb = udom_emb oo sfun_map\prj\emb" - -definition - "prj = sfun_map\emb\prj oo udom_prj" - -instance -apply (default, unfold emb_sfun_def prj_sfun_def) -apply (rule ep_pair_comp) -apply (rule ep_pair_sfun_map) -apply (rule ep_pair_emb_prj) -apply (rule ep_pair_emb_prj) -apply (rule ep_pair_udom) -done - -end +text {* SFP of type constructor = type combinator *} -text {* - A deflation constructor lets us configure the domain package to work - with the strict function space type constructor. -*} - -definition - sfun_defl :: "TypeRep \ TypeRep \ TypeRep" -where - "sfun_defl = TypeRep_fun2 sfun_map" - -lemma cast_sfun_defl: - "cast\(sfun_defl\A\B) = udom_emb oo sfun_map\(cast\A)\(cast\B) oo udom_prj" -unfolding sfun_defl_def -apply (rule cast_TypeRep_fun2) -apply (erule (1) finite_deflation_sfun_map) -done - -lemma REP_sfun: "REP('a::rep \! 'b::rep) = sfun_defl\REP('a)\REP('b)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_sfun_defl) -apply (simp only: prj_sfun_def emb_sfun_def) -apply (simp add: sfun_map_def cfun_map_def strictify_cancel) -done +lemma SFP_sfun: "SFP('a::sfp \! 'b::sfp) = sfun_sfp\SFP('a)\SFP('b)" +by (rule sfp_sfun_def) lemma isodefl_sfun: "isodefl d1 t1 \ isodefl d2 t2 \ - isodefl (sfun_map\d1\d2) (sfun_defl\t1\t2)" + isodefl (sfun_map\d1\d2) (sfun_sfp\t1\t2)" apply (rule isodeflI) -apply (simp add: cast_sfun_defl cast_isodefl) +apply (simp add: cast_sfun_sfp cast_isodefl) apply (simp add: emb_sfun_def prj_sfun_def) apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation]) done setup {* Domain_Isomorphism.add_type_constructor - (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm REP_sfun}, + (@{type_name "sfun"}, @{term sfun_sfp}, @{const_name sfun_map}, @{thm SFP_sfun}, @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map}) *} diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Library/Sum_Cpo.thy --- a/src/HOLCF/Library/Sum_Cpo.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Library/Sum_Cpo.thy Wed Oct 06 10:49:27 2010 -0700 @@ -5,7 +5,7 @@ header {* The cpo of disjoint sums *} theory Sum_Cpo -imports Bifinite +imports HOLCF begin subsection {* Ordering on sum type *} @@ -218,38 +218,4 @@ instance sum :: (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 sum :: (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 c62b4ff97bfc -r b525988432e9 src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Lift.thy Wed Oct 06 10:49:27 2010 -0700 @@ -171,51 +171,89 @@ by (cases x, simp_all) -subsection {* Lifted countable types are bifinite *} - -instantiation lift :: (countable) bifinite -begin +subsection {* Lifted countable types are SFP domains *} definition - approx_lift_def: - "approx = (\n. FLIFT x. if to_nat x < n then Def x else \)" + lift_approx :: "nat \ 'a::countable lift \ 'a lift" +where + "lift_approx = (\i. FLIFT x. if to_nat x < i then Def x else \)" + +lemma chain_lift_approx [simp]: "chain lift_approx" + unfolding lift_approx_def + by (rule chainI, simp add: FLIFT_mono) -instance proof - fix x :: "'a lift" - show "chain (approx :: nat \ 'a lift \ 'a lift)" - unfolding approx_lift_def - by (rule chainI, simp add: FLIFT_mono) -next - fix x :: "'a lift" - show "(\i. approx i\x) = x" - unfolding approx_lift_def - apply (cases x, simp) - apply (rule thelubI) - apply (rule is_lubI) - apply (rule ub_rangeI, simp) - apply (drule ub_rangeD) - apply (erule rev_below_trans) - apply simp - apply (rule lessI) - done -next - fix i :: nat and x :: "'a lift" - show "approx i\(approx i\x) = approx i\x" - unfolding approx_lift_def +lemma lub_lift_approx [simp]: "(\i. lift_approx i) = ID" +apply (rule ext_cfun) +apply (simp add: contlub_cfun_fun) +apply (simp add: lift_approx_def) +apply (case_tac x, simp) +apply (rule thelubI) +apply (rule is_lubI) +apply (rule ub_rangeI, simp) +apply (drule ub_rangeD) +apply (erule rev_below_trans) +apply simp +apply (rule lessI) +done + +lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)" +proof + fix x + show "lift_approx i\x \ x" + unfolding lift_approx_def by (cases x, simp, simp) -next - fix i :: nat - show "finite {x::'a lift. approx i\x = x}" + show "lift_approx i\(lift_approx i\x) = lift_approx i\x" + unfolding lift_approx_def + by (cases x, simp, simp) + show "finite {x::'a lift. lift_approx i\x = x}" proof (rule finite_subset) let ?S = "insert (\::'a lift) (Def ` to_nat -` {..x = x} \ ?S" - unfolding approx_lift_def + show "{x::'a lift. lift_approx i\x = x} \ ?S" + unfolding lift_approx_def by (rule subsetI, case_tac x, simp, simp split: split_if_asm) show "finite ?S" by (simp add: finite_vimageI) qed qed +lemma lift_approx: "approx_chain lift_approx" +using chain_lift_approx lub_lift_approx finite_deflation_lift_approx +by (rule approx_chain.intro) + +instantiation lift :: (countable) sfp +begin + +definition + "emb = udom_emb lift_approx" + +definition + "prj = udom_prj lift_approx" + +definition + "sfp (t::'a lift itself) = + (\i. sfp_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))" + +instance proof + show ep: "ep_pair emb (prj :: udom \ 'a lift)" + unfolding emb_lift_def prj_lift_def + by (rule ep_pair_udom [OF lift_approx]) + show "cast\SFP('a lift) = emb oo (prj :: udom \ 'a lift)" + unfolding sfp_lift_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_lift_approx + ep_pair.finite_deflation_e_d_p [OF ep]) + apply (intro monofun_cfun below_refl) + apply (rule chainE) + apply (rule chain_lift_approx) + apply (subst cast_sfp_principal) + apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx + ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs) + done +qed + end end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/LowerPD.thy --- a/src/HOLCF/LowerPD.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/LowerPD.thy Wed Oct 06 10:49:27 2010 -0700 @@ -71,27 +71,6 @@ apply (simp add: lower_le_PDPlus_iff 3) done -lemma pd_take_lower_chain: - "pd_take n t \\ pd_take (Suc n) t" -apply (induct t rule: pd_basis_induct) -apply (simp add: compact_basis.take_chain) -apply (simp add: PDPlus_lower_mono) -done - -lemma pd_take_lower_le: "pd_take i t \\ t" -apply (induct t rule: pd_basis_induct) -apply (simp add: compact_basis.take_less) -apply (simp add: PDPlus_lower_mono) -done - -lemma pd_take_lower_mono: - "t \\ u \ pd_take n t \\ pd_take n u" -apply (erule lower_le_induct) -apply (simp add: compact_basis.take_mono) -apply (simp add: lower_le_PDUnit_PDPlus_iff) -apply (simp add: lower_le_PDPlus_iff) -done - subsection {* Type definition *} @@ -99,7 +78,7 @@ "{S::'a pd_basis set. lower_le.ideal S}" by (fast intro: lower_le.ideal_principal) -instantiation lower_pd :: (profinite) below +instantiation lower_pd :: (sfp) below begin definition @@ -108,11 +87,11 @@ instance .. end -instance lower_pd :: (profinite) po +instance lower_pd :: (sfp) po by (rule lower_le.typedef_ideal_po [OF type_definition_lower_pd below_lower_pd_def]) -instance lower_pd :: (profinite) cpo +instance lower_pd :: (sfp) cpo by (rule lower_le.typedef_ideal_cpo [OF type_definition_lower_pd below_lower_pd_def]) @@ -134,18 +113,13 @@ by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal) interpretation lower_pd: - ideal_completion lower_le pd_take lower_principal Rep_lower_pd + ideal_completion lower_le lower_principal Rep_lower_pd apply unfold_locales -apply (rule pd_take_lower_le) -apply (rule pd_take_idem) -apply (erule pd_take_lower_mono) -apply (rule pd_take_lower_chain) -apply (rule finite_range_pd_take) -apply (rule pd_take_covers) apply (rule ideal_Rep_lower_pd) apply (erule Rep_lower_pd_lub) apply (rule Rep_lower_principal) apply (simp only: below_lower_pd_def) +apply (rule pd_basis_countable) done text {* Lower powerdomain is pointed *} @@ -153,42 +127,12 @@ lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \ ys" by (induct ys rule: lower_pd.principal_induct, simp, simp) -instance lower_pd :: (bifinite) pcpo +instance lower_pd :: (sfp) pcpo by intro_classes (fast intro: lower_pd_minimal) lemma inst_lower_pd_pcpo: "\ = lower_principal (PDUnit compact_bot)" by (rule lower_pd_minimal [THEN UU_I, symmetric]) -text {* Lower powerdomain is profinite *} - -instantiation lower_pd :: (profinite) profinite -begin - -definition - approx_lower_pd_def: "approx = lower_pd.completion_approx" - -instance -apply (intro_classes, unfold approx_lower_pd_def) -apply (rule lower_pd.chain_completion_approx) -apply (rule lower_pd.lub_completion_approx) -apply (rule lower_pd.completion_approx_idem) -apply (rule lower_pd.finite_fixes_completion_approx) -done - -end - -instance lower_pd :: (bifinite) bifinite .. - -lemma approx_lower_principal [simp]: - "approx n\(lower_principal t) = lower_principal (pd_take n t)" -unfolding approx_lower_pd_def -by (rule lower_pd.completion_approx_principal) - -lemma approx_eq_lower_principal: - "\t\Rep_lower_pd xs. approx n\xs = lower_principal (pd_take n t)" -unfolding approx_lower_pd_def -by (rule lower_pd.completion_approx_eq_principal) - subsection {* Monadic unit and plus *} @@ -224,16 +168,6 @@ by (simp add: lower_pd.basis_fun_principal lower_pd.basis_fun_mono PDPlus_lower_mono) -lemma approx_lower_unit [simp]: - "approx n\{x}\ = {approx n\x}\" -apply (induct x rule: compact_basis.principal_induct, simp) -apply (simp add: approx_Rep_compact_basis) -done - -lemma approx_lower_plus [simp]: - "approx n\(xs +\ ys) = (approx n\xs) +\ (approx n\ys)" -by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp) - interpretation lower_add: semilattice lower_add proof fix xs ys zs :: "'a lower_pd" show "(xs +\ ys) +\ zs = xs +\ (ys +\ zs)" @@ -309,7 +243,8 @@ by (simp add: po_eq_conv) lemma lower_unit_strict [simp]: "{\}\ = \" -unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp +using lower_unit_Rep_compact_basis [of compact_bot] +by (simp add: inst_lower_pd_pcpo) lemma lower_unit_strict_iff [simp]: "{x}\ = \ \ x = \" unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff) @@ -332,8 +267,14 @@ apply (simp add: lower_plus_least) done +lemma compact_lower_unit: "compact x \ compact {x}\" +by (auto dest!: compact_basis.compact_imp_principal) + lemma compact_lower_unit_iff [simp]: "compact {x}\ \ compact x" -unfolding profinite_compact_iff by simp +apply (safe elim!: compact_lower_unit) +apply (simp only: compact_def lower_unit_below_iff [symmetric]) +apply (erule adm_subst [OF cont_Rep_CFun2]) +done lemma compact_lower_plus [simp]: "\compact xs; compact ys\ \ compact (xs +\ ys)" @@ -429,16 +370,12 @@ unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit) -subsection {* Map and join *} +subsection {* Map *} definition lower_map :: "('a \ 'b) \ 'a lower_pd \ 'b lower_pd" where "lower_map = (\ f xs. lower_bind\xs\(\ x. {f\x}\))" -definition - lower_join :: "'a lower_pd lower_pd \ 'a lower_pd" where - "lower_join = (\ xss. lower_bind\xss\(\ xs. xs))" - lemma lower_map_unit [simp]: "lower_map\f\{x}\ = {f\x}\" unfolding lower_map_def by simp @@ -447,14 +384,6 @@ "lower_map\f\(xs +\ ys) = lower_map\f\xs +\ lower_map\f\ys" unfolding lower_map_def by simp -lemma lower_join_unit [simp]: - "lower_join\{xs}\ = xs" -unfolding lower_join_def by simp - -lemma lower_join_plus [simp]: - "lower_join\(xss +\ yss) = lower_join\xss +\ lower_join\yss" -unfolding lower_join_def by simp - lemma lower_map_ident: "lower_map\(\ x. x)\xs = xs" by (induct xs rule: lower_pd_induct, simp_all) @@ -465,22 +394,6 @@ "lower_map\f\(lower_map\g\xs) = lower_map\(\ x. f\(g\x))\xs" by (induct xs rule: lower_pd_induct, simp_all) -lemma lower_join_map_unit: - "lower_join\(lower_map\lower_unit\xs) = xs" -by (induct xs rule: lower_pd_induct, simp_all) - -lemma lower_join_map_join: - "lower_join\(lower_map\lower_join\xsss) = lower_join\(lower_join\xsss)" -by (induct xsss rule: lower_pd_induct, simp_all) - -lemma lower_join_map_map: - "lower_join\(lower_map\(lower_map\f)\xss) = - lower_map\f\(lower_join\xss)" -by (induct xss rule: lower_pd_induct, simp_all) - -lemma lower_map_approx: "lower_map\(approx n)\xs = approx n\xs" -by (induct xs rule: lower_pd_induct, simp_all) - lemma ep_pair_lower_map: "ep_pair e p \ ep_pair (lower_map\e) (lower_map\p)" apply default apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse) @@ -495,4 +408,134 @@ apply (simp_all add: deflation.below monofun_cfun) done +(* FIXME: long proof! *) +lemma finite_deflation_lower_map: + assumes "finite_deflation d" shows "finite_deflation (lower_map\d)" +proof (rule finite_deflation_intro) + interpret d: finite_deflation d by fact + have "deflation d" by fact + thus "deflation (lower_map\d)" by (rule deflation_lower_map) + have "finite (range (\x. d\x))" by (rule d.finite_range) + hence "finite (Rep_compact_basis -` range (\x. d\x))" + by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) + hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp + hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" + by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) + hence *: "finite (lower_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp + hence "finite (range (\xs. lower_map\d\xs))" + apply (rule rev_finite_subset) + apply clarsimp + apply (induct_tac xs rule: lower_pd.principal_induct) + apply (simp add: adm_mem_finite *) + apply (rename_tac t, induct_tac t rule: pd_basis_induct) + apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_map_unit) + apply simp + apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDUnit) + apply (rule range_eqI) + apply (erule sym) + apply (rule exI) + apply (rule Abs_compact_basis_inverse [symmetric]) + apply (simp add: d.compact) + apply (simp only: lower_plus_principal [symmetric] lower_map_plus) + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDPlus) + done + thus "finite {xs. lower_map\d\xs = xs}" + by (rule finite_range_imp_finite_fixes) +qed + +subsection {* Lower powerdomain is an SFP domain *} + +definition + lower_approx :: "nat \ udom lower_pd \ udom lower_pd" +where + "lower_approx = (\i. lower_map\(udom_approx i))" + +lemma lower_approx: "approx_chain lower_approx" +proof (rule approx_chain.intro) + show "chain (\i. lower_approx i)" + unfolding lower_approx_def by simp + show "(\i. lower_approx i) = ID" + unfolding lower_approx_def + by (simp add: lub_distribs lower_map_ID) + show "\i. finite_deflation (lower_approx i)" + unfolding lower_approx_def + by (intro finite_deflation_lower_map finite_deflation_udom_approx) +qed + +definition lower_sfp :: "sfp \ sfp" +where "lower_sfp = sfp_fun1 lower_approx lower_map" + +lemma cast_lower_sfp: + "cast\(lower_sfp\A) = + udom_emb lower_approx oo lower_map\(cast\A) oo udom_prj lower_approx" +unfolding lower_sfp_def +apply (rule cast_sfp_fun1 [OF lower_approx]) +apply (erule finite_deflation_lower_map) +done + +instantiation lower_pd :: (sfp) sfp +begin + +definition + "emb = udom_emb lower_approx oo lower_map\emb" + +definition + "prj = lower_map\prj oo udom_prj lower_approx" + +definition + "sfp (t::'a lower_pd itself) = lower_sfp\SFP('a)" + +instance proof + show "ep_pair emb (prj :: udom \ 'a lower_pd)" + unfolding emb_lower_pd_def prj_lower_pd_def + using ep_pair_udom [OF lower_approx] + by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj) +next + show "cast\SFP('a lower_pd) = emb oo (prj :: udom \ 'a lower_pd)" + unfolding emb_lower_pd_def prj_lower_pd_def sfp_lower_pd_def cast_lower_sfp + by (simp add: cast_SFP oo_def expand_cfun_eq lower_map_map) +qed + end + +text {* SFP of type constructor = type combinator *} + +lemma SFP_lower: "SFP('a lower_pd) = lower_sfp\SFP('a)" +by (rule sfp_lower_pd_def) + + +subsection {* Join *} + +definition + lower_join :: "'a lower_pd lower_pd \ 'a lower_pd" where + "lower_join = (\ xss. lower_bind\xss\(\ xs. xs))" + +lemma lower_join_unit [simp]: + "lower_join\{xs}\ = xs" +unfolding lower_join_def by simp + +lemma lower_join_plus [simp]: + "lower_join\(xss +\ yss) = lower_join\xss +\ lower_join\yss" +unfolding lower_join_def by simp + +lemma lower_join_map_unit: + "lower_join\(lower_map\lower_unit\xs) = xs" +by (induct xs rule: lower_pd_induct, simp_all) + +lemma lower_join_map_join: + "lower_join\(lower_map\lower_join\xsss) = lower_join\(lower_join\xsss)" +by (induct xsss rule: lower_pd_induct, simp_all) + +lemma lower_join_map_map: + "lower_join\(lower_map\(lower_map\f)\xss) = + lower_map\f\(lower_join\xss)" +by (induct xss rule: lower_pd_induct, simp_all) + +end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Powerdomains.thy --- a/src/HOLCF/Powerdomains.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Powerdomains.thy Wed Oct 06 10:49:27 2010 -0700 @@ -5,290 +5,29 @@ header {* Powerdomains *} theory Powerdomains -imports Representable ConvexPD -begin - -subsection {* Powerdomains are representable *} - -text "Upper powerdomain of a representable type is representable." - -instantiation upper_pd :: (rep) rep -begin - -definition emb_upper_pd_def: "emb = udom_emb oo upper_map\emb" -definition prj_upper_pd_def: "prj = upper_map\prj oo udom_prj" - -instance - apply (intro_classes, unfold emb_upper_pd_def prj_upper_pd_def) - apply (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj ep_pair_udom) -done - -end - -text "Lower powerdomain of a representable type is representable." - -instantiation lower_pd :: (rep) rep -begin - -definition emb_lower_pd_def: "emb = udom_emb oo lower_map\emb" -definition prj_lower_pd_def: "prj = lower_map\prj oo udom_prj" - -instance - apply (intro_classes, unfold emb_lower_pd_def prj_lower_pd_def) - apply (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj ep_pair_udom) -done - -end - -text "Convex powerdomain of a representable type is representable." - -instantiation convex_pd :: (rep) rep +imports ConvexPD Domain begin -definition emb_convex_pd_def: "emb = udom_emb oo convex_map\emb" -definition prj_convex_pd_def: "prj = convex_map\prj oo udom_prj" - -instance - apply (intro_classes, unfold emb_convex_pd_def prj_convex_pd_def) - apply (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj ep_pair_udom) -done - -end - -subsection {* Finite deflation lemmas *} - -text "TODO: move these lemmas somewhere else" - -lemma finite_compact_range_imp_finite_range: - fixes d :: "'a::profinite \ 'b::cpo" - assumes "finite ((\x. d\x) ` {x. compact x})" - shows "finite (range (\x. d\x))" -proof (rule finite_subset [OF _ prems]) - { - fix x :: 'a - have "range (\i. d\(approx i\x)) \ (\x. d\x) ` {x. compact x}" - by auto - hence "finite (range (\i. d\(approx i\x)))" - using prems by (rule finite_subset) - hence "finite_chain (\i. d\(approx i\x))" - by (simp add: finite_range_imp_finch) - hence "\i. (\i. d\(approx i\x)) = d\(approx i\x)" - by (simp add: finite_chain_def maxinch_is_thelub) - hence "\i. d\x = d\(approx i\x)" - by (simp add: lub_distribs) - hence "d\x \ (\x. d\x) ` {x. compact x}" - by auto - } - thus "range (\x. d\x) \ (\x. d\x) ` {x. compact x}" - by clarsimp -qed - -lemma finite_deflation_upper_map: - assumes "finite_deflation d" shows "finite_deflation (upper_map\d)" -proof (rule finite_deflation_intro) - interpret d: finite_deflation d by fact - have "deflation d" by fact - thus "deflation (upper_map\d)" by (rule deflation_upper_map) - have "finite (range (\x. d\x))" by (rule d.finite_range) - hence "finite (Rep_compact_basis -` range (\x. d\x))" - by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) - hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp - hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" - by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) - hence "finite (upper_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp - hence "finite ((\xs. upper_map\d\xs) ` range upper_principal)" - apply (rule finite_subset [COMP swap_prems_rl]) - apply (clarsimp, rename_tac t) - apply (induct_tac t rule: pd_basis_induct) - apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit) - apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDUnit) - apply (rule image_eqI) - apply (erule sym) - apply simp - apply (rule exI) - apply (rule Abs_compact_basis_inverse [symmetric]) - apply (simp add: d.compact) - apply (simp only: upper_plus_principal [symmetric] upper_map_plus) - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDPlus) - done - moreover have "{xs::'a upper_pd. compact xs} = range upper_principal" - by (auto dest: upper_pd.compact_imp_principal) - ultimately have "finite ((\xs. upper_map\d\xs) ` {xs::'a upper_pd. compact xs})" - by simp - hence "finite (range (\xs. upper_map\d\xs))" - by (rule finite_compact_range_imp_finite_range) - thus "finite {xs. upper_map\d\xs = xs}" - by (rule finite_range_imp_finite_fixes) -qed - -lemma finite_deflation_lower_map: - assumes "finite_deflation d" shows "finite_deflation (lower_map\d)" -proof (rule finite_deflation_intro) - interpret d: finite_deflation d by fact - have "deflation d" by fact - thus "deflation (lower_map\d)" by (rule deflation_lower_map) - have "finite (range (\x. d\x))" by (rule d.finite_range) - hence "finite (Rep_compact_basis -` range (\x. d\x))" - by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) - hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp - hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" - by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) - hence "finite (lower_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp - hence "finite ((\xs. lower_map\d\xs) ` range lower_principal)" - apply (rule finite_subset [COMP swap_prems_rl]) - apply (clarsimp, rename_tac t) - apply (induct_tac t rule: pd_basis_induct) - apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_map_unit) - apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDUnit) - apply (rule image_eqI) - apply (erule sym) - apply simp - apply (rule exI) - apply (rule Abs_compact_basis_inverse [symmetric]) - apply (simp add: d.compact) - apply (simp only: lower_plus_principal [symmetric] lower_map_plus) - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDPlus) - done - moreover have "{xs::'a lower_pd. compact xs} = range lower_principal" - by (auto dest: lower_pd.compact_imp_principal) - ultimately have "finite ((\xs. lower_map\d\xs) ` {xs::'a lower_pd. compact xs})" - by simp - hence "finite (range (\xs. lower_map\d\xs))" - by (rule finite_compact_range_imp_finite_range) - thus "finite {xs. lower_map\d\xs = xs}" - by (rule finite_range_imp_finite_fixes) -qed - -lemma finite_deflation_convex_map: - assumes "finite_deflation d" shows "finite_deflation (convex_map\d)" -proof (rule finite_deflation_intro) - interpret d: finite_deflation d by fact - have "deflation d" by fact - thus "deflation (convex_map\d)" by (rule deflation_convex_map) - have "finite (range (\x. d\x))" by (rule d.finite_range) - hence "finite (Rep_compact_basis -` range (\x. d\x))" - by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) - hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp - hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" - by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) - hence "finite (convex_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp - hence "finite ((\xs. convex_map\d\xs) ` range convex_principal)" - apply (rule finite_subset [COMP swap_prems_rl]) - apply (clarsimp, rename_tac t) - apply (induct_tac t rule: pd_basis_induct) - apply (simp only: convex_unit_Rep_compact_basis [symmetric] convex_map_unit) - apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDUnit) - apply (rule image_eqI) - apply (erule sym) - apply simp - apply (rule exI) - apply (rule Abs_compact_basis_inverse [symmetric]) - apply (simp add: d.compact) - apply (simp only: convex_plus_principal [symmetric] convex_map_plus) - apply clarsimp - apply (rule imageI) - apply (rule vimageI2) - apply (simp add: Rep_PDPlus) - done - moreover have "{xs::'a convex_pd. compact xs} = range convex_principal" - by (auto dest: convex_pd.compact_imp_principal) - ultimately have "finite ((\xs. convex_map\d\xs) ` {xs::'a convex_pd. compact xs})" - by simp - hence "finite (range (\xs. convex_map\d\xs))" - by (rule finite_compact_range_imp_finite_range) - thus "finite {xs. convex_map\d\xs = xs}" - by (rule finite_range_imp_finite_fixes) -qed - -subsection {* Deflation combinators *} - -definition "upper_defl = TypeRep_fun1 upper_map" -definition "lower_defl = TypeRep_fun1 lower_map" -definition "convex_defl = TypeRep_fun1 convex_map" - -lemma cast_upper_defl: - "cast\(upper_defl\A) = udom_emb oo upper_map\(cast\A) oo udom_prj" -unfolding upper_defl_def -apply (rule cast_TypeRep_fun1) -apply (erule finite_deflation_upper_map) -done - -lemma cast_lower_defl: - "cast\(lower_defl\A) = udom_emb oo lower_map\(cast\A) oo udom_prj" -unfolding lower_defl_def -apply (rule cast_TypeRep_fun1) -apply (erule finite_deflation_lower_map) -done - -lemma cast_convex_defl: - "cast\(convex_defl\A) = udom_emb oo convex_map\(cast\A) oo udom_prj" -unfolding convex_defl_def -apply (rule cast_TypeRep_fun1) -apply (erule finite_deflation_convex_map) -done - -lemma REP_upper: "REP('a upper_pd) = upper_defl\REP('a)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_upper_defl) -apply (simp add: prj_upper_pd_def) -apply (simp add: emb_upper_pd_def) -apply (simp add: upper_map_map cfcomp1) -done - -lemma REP_lower: "REP('a lower_pd) = lower_defl\REP('a)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_lower_defl) -apply (simp add: prj_lower_pd_def) -apply (simp add: emb_lower_pd_def) -apply (simp add: lower_map_map cfcomp1) -done - -lemma REP_convex: "REP('a convex_pd) = convex_defl\REP('a)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_convex_defl) -apply (simp add: prj_convex_pd_def) -apply (simp add: emb_convex_pd_def) -apply (simp add: convex_map_map cfcomp1) -done - lemma isodefl_upper: - "isodefl d t \ isodefl (upper_map\d) (upper_defl\t)" + "isodefl d t \ isodefl (upper_map\d) (upper_sfp\t)" apply (rule isodeflI) -apply (simp add: cast_upper_defl cast_isodefl) +apply (simp add: cast_upper_sfp cast_isodefl) apply (simp add: emb_upper_pd_def prj_upper_pd_def) apply (simp add: upper_map_map) done lemma isodefl_lower: - "isodefl d t \ isodefl (lower_map\d) (lower_defl\t)" + "isodefl d t \ isodefl (lower_map\d) (lower_sfp\t)" apply (rule isodeflI) -apply (simp add: cast_lower_defl cast_isodefl) +apply (simp add: cast_lower_sfp cast_isodefl) apply (simp add: emb_lower_pd_def prj_lower_pd_def) apply (simp add: lower_map_map) done lemma isodefl_convex: - "isodefl d t \ isodefl (convex_map\d) (convex_defl\t)" + "isodefl d t \ isodefl (convex_map\d) (convex_sfp\t)" apply (rule isodeflI) -apply (simp add: cast_convex_defl cast_isodefl) +apply (simp add: cast_convex_sfp cast_isodefl) apply (simp add: emb_convex_pd_def prj_convex_pd_def) apply (simp add: convex_map_map) done @@ -297,16 +36,16 @@ setup {* fold Domain_Isomorphism.add_type_constructor - [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}, - @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}, + [(@{type_name "upper_pd"}, @{term upper_sfp}, @{const_name upper_map}, + @{thm SFP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}, @{thm deflation_upper_map}), - (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}, - @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}, + (@{type_name "lower_pd"}, @{term lower_sfp}, @{const_name lower_map}, + @{thm SFP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}, @{thm deflation_lower_map}), - (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map}, - @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID}, + (@{type_name "convex_pd"}, @{term convex_sfp}, @{const_name convex_map}, + @{thm SFP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID}, @{thm deflation_convex_map})] *} diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Representable.thy Wed Oct 06 10:49:27 2010 -0700 @@ -5,97 +5,30 @@ header {* Representable Types *} theory Representable -imports Algebraic Universal Ssum Sprod One Fixrec Domain_Aux +imports Algebraic Universal Ssum One Fixrec Domain_Aux uses ("Tools/repdef.ML") ("Tools/Domain/domain_isomorphism.ML") begin -subsection {* Class of representable types *} - -text "Overloaded embedding and projection functions between - a representable type and the universal domain." - -class rep = bifinite + - fixes emb :: "'a::pcpo \ udom" - fixes prj :: "udom \ 'a::pcpo" - assumes ep_pair_emb_prj: "ep_pair emb prj" - -interpretation rep: - pcpo_ep_pair - "emb :: 'a::rep \ udom" - "prj :: udom \ 'a::rep" - unfolding pcpo_ep_pair_def - by (rule ep_pair_emb_prj) - -lemmas emb_inverse = rep.e_inverse -lemmas emb_prj_below = rep.e_p_below -lemmas emb_eq_iff = rep.e_eq_iff -lemmas emb_strict = rep.e_strict -lemmas prj_strict = rep.p_strict - - -subsection {* Making \emph{rep} the default class *} - -text {* - From now on, free type variables are assumed to be in class - @{term rep}, unless specified otherwise. -*} - -default_sort rep +default_sort sfp subsection {* Representations of types *} -text "A TypeRep is an algebraic deflation over the universe of values." - -types TypeRep = "udom alg_defl" -translations (type) "TypeRep" \ (type) "udom alg_defl" - -definition - Rep_of :: "'a::rep itself \ TypeRep" -where - "Rep_of TYPE('a::rep) = - (\i. alg_defl_principal (Abs_fin_defl - (emb oo (approx i :: 'a \ 'a) oo prj)))" - -syntax "_REP" :: "type \ TypeRep" ("(1REP/(1'(_')))") -translations "REP('t)" \ "CONST Rep_of TYPE('t)" +lemma emb_prj: "emb\((prj\x)::'a::sfp) = cast\SFP('a)\x" +by (simp add: cast_SFP) -lemma cast_REP: - "cast\REP('a::rep) = (emb::'a \ udom) oo (prj::udom \ 'a)" -proof - - let ?a = "\i. emb oo approx i oo (prj::udom \ 'a)" - have a: "\i. finite_deflation (?a i)" - apply (rule rep.finite_deflation_e_d_p) - apply (rule finite_deflation_approx) - done - show ?thesis - unfolding Rep_of_def - apply (subst contlub_cfun_arg) - apply (rule chainI) - apply (rule alg_defl.principal_mono) - apply (rule Abs_fin_defl_mono [OF a a]) - apply (rule chainE, simp) - apply (subst cast_alg_defl_principal) - apply (simp add: Abs_fin_defl_inverse a) - apply (simp add: expand_cfun_eq lub_distribs) - done -qed - -lemma emb_prj: "emb\((prj\x)::'a::rep) = cast\REP('a)\x" -by (simp add: cast_REP) - -lemma in_REP_iff: - "x ::: REP('a::rep) \ emb\((prj\x)::'a) = x" -by (simp add: in_deflation_def cast_REP) +lemma in_SFP_iff: + "x ::: SFP('a::sfp) \ emb\((prj\x)::'a) = x" +by (simp add: in_sfp_def cast_SFP) lemma prj_inverse: - "x ::: REP('a::rep) \ emb\((prj\x)::'a) = x" -by (simp only: in_REP_iff) + "x ::: SFP('a::sfp) \ emb\((prj\x)::'a) = x" +by (simp only: in_SFP_iff) -lemma emb_in_REP [simp]: - "emb\(x::'a::rep) ::: REP('a)" -by (simp add: in_REP_iff) +lemma emb_in_SFP [simp]: + "emb\(x::'a::sfp) ::: SFP('a)" +by (simp add: in_SFP_iff) subsection {* Coerce operator *} @@ -115,16 +48,16 @@ by (rule ext_cfun, simp add: beta_coerce) lemma emb_coerce: - "REP('a) \ REP('b) + "SFP('a) \ SFP('b) \ emb\((coerce::'a \ 'b)\x) = emb\x" apply (simp add: beta_coerce) apply (rule prj_inverse) - apply (erule subdeflationD) - apply (rule emb_in_REP) + apply (erule sfp_belowD) + apply (rule emb_in_SFP) done lemma coerce_prj: - "REP('a) \ REP('b) + "SFP('a) \ SFP('b) \ (coerce::'b \ 'a)\(prj\x) = prj\x" apply (simp add: coerce_def) apply (rule emb_eq_iff [THEN iffD1]) @@ -136,21 +69,21 @@ done lemma coerce_coerce [simp]: - "REP('a) \ REP('b) + "SFP('a) \ SFP('b) \ coerce\((coerce::'a \ 'b)\x) = coerce\x" -by (simp add: beta_coerce prj_inverse subdeflationD) +by (simp add: beta_coerce prj_inverse sfp_belowD) lemma coerce_inverse: - "emb\(x::'a) ::: REP('b) \ coerce\(coerce\x :: 'b) = x" + "emb\(x::'a) ::: SFP('b) \ coerce\(coerce\x :: 'b) = x" by (simp only: beta_coerce prj_inverse emb_inverse) lemma coerce_type: - "REP('a) \ REP('b) - \ emb\((coerce::'a \ 'b)\x) ::: REP('a)" -by (simp add: beta_coerce prj_inverse subdeflationD) + "SFP('a) \ SFP('b) + \ emb\((coerce::'a \ 'b)\x) ::: SFP('a)" +by (simp add: beta_coerce prj_inverse sfp_belowD) lemma ep_pair_coerce: - "REP('a) \ REP('b) + "SFP('a) \ SFP('b) \ ep_pair (coerce::'a \ 'b) (coerce::'b \ 'a)" apply (rule ep_pair.intro) apply simp @@ -165,30 +98,29 @@ lemma domain_abs_iso: fixes abs and rep - assumes REP: "REP('b) = REP('a)" + assumes SFP: "SFP('b) = SFP('a)" assumes abs_def: "abs \ (coerce :: 'a \ 'b)" assumes rep_def: "rep \ (coerce :: 'b \ 'a)" shows "rep\(abs\x) = x" -unfolding abs_def rep_def by (simp add: REP) +unfolding abs_def rep_def by (simp add: SFP) lemma domain_rep_iso: fixes abs and rep - assumes REP: "REP('b) = REP('a)" + assumes SFP: "SFP('b) = SFP('a)" assumes abs_def: "abs \ (coerce :: 'a \ 'b)" assumes rep_def: "rep \ (coerce :: 'b \ 'a)" shows "abs\(rep\x) = x" -unfolding abs_def rep_def by (simp add: REP [symmetric]) +unfolding abs_def rep_def by (simp add: SFP [symmetric]) subsection {* Proving a subtype is representable *} text {* - Temporarily relax type constraints for @{term "approx"}, - @{term emb}, and @{term prj}. + Temporarily relax type constraints for @{term emb}, and @{term prj}. *} setup {* Sign.add_const_constraint - (@{const_name "approx"}, SOME @{typ "nat \ 'a::cpo \ 'a"}) *} + (@{const_name sfp}, SOME @{typ "'a::pcpo itself \ sfp"}) *} setup {* Sign.add_const_constraint (@{const_name emb}, SOME @{typ "'a::pcpo \ udom"}) *} @@ -196,118 +128,19 @@ setup {* Sign.add_const_constraint (@{const_name prj}, SOME @{typ "udom \ 'a::pcpo"}) *} -definition - repdef_approx :: - "('a::pcpo \ udom) \ (udom \ 'a) \ udom alg_defl \ nat \ 'a \ 'a" -where - "repdef_approx Rep Abs t = (\i. \ x. Abs (cast\(approx i\t)\(Rep x)))" - lemma typedef_rep_class: fixes Rep :: "'a::pcpo \ udom" fixes Abs :: "udom \ 'a::pcpo" - fixes t :: TypeRep + fixes t :: sfp assumes type: "type_definition Rep Abs {x. x ::: t}" assumes below: "op \ \ \x y. Rep x \ Rep y" assumes emb: "emb \ (\ x. Rep x)" assumes prj: "prj \ (\ x. Abs (cast\t\x))" - assumes approx: "(approx :: nat \ 'a \ 'a) \ repdef_approx Rep Abs t" - shows "OFCLASS('a, rep_class)" + assumes sfp: "sfp \ (\ a::'a itself. t)" + shows "OFCLASS('a, sfp_class)" proof have adm: "adm (\x. x \ {x. x ::: t})" - by (simp add: adm_in_deflation) - have emb_beta: "\x. emb\x = Rep x" - unfolding emb - apply (rule beta_cfun) - apply (rule typedef_cont_Rep [OF type below adm]) - done - have prj_beta: "\y. prj\y = Abs (cast\t\y)" - unfolding prj - apply (rule beta_cfun) - apply (rule typedef_cont_Abs [OF type below adm]) - apply simp_all - done - have cast_cast_approx: - "\i x. cast\t\(cast\(approx i\t)\x) = cast\(approx i\t)\x" - apply (rule cast_fixed) - apply (rule subdeflationD) - apply (rule approx.below) - apply (rule cast_in_deflation) - done - have approx': - "approx = (\i. \(x::'a). prj\(cast\(approx i\t)\(emb\x)))" - unfolding approx repdef_approx_def - apply (subst cast_cast_approx [symmetric]) - apply (simp add: prj_beta [symmetric] emb_beta [symmetric]) - done - have emb_in_deflation: "\x::'a. emb\x ::: t" - using type_definition.Rep [OF type] - by (simp add: emb_beta) - have prj_emb: "\x::'a. prj\(emb\x) = x" - unfolding prj_beta - apply (simp add: cast_fixed [OF emb_in_deflation]) - apply (simp add: emb_beta type_definition.Rep_inverse [OF type]) - done - have emb_prj: "\y. emb\(prj\y :: 'a) = cast\t\y" - unfolding prj_beta emb_beta - by (simp add: type_definition.Abs_inverse [OF type]) - show "ep_pair (emb :: 'a \ udom) prj" - apply default - apply (simp add: prj_emb) - apply (simp add: emb_prj cast.below) - done - show "chain (approx :: nat \ 'a \ 'a)" - unfolding approx' by simp - show "\x::'a. (\i. approx i\x) = x" - unfolding approx' - apply (simp add: lub_distribs) - apply (subst cast_fixed [OF emb_in_deflation]) - apply (rule prj_emb) - done - show "\(i::nat) (x::'a). approx i\(approx i\x) = approx i\x" - unfolding approx' - apply simp - apply (simp add: emb_prj) - apply (simp add: cast_cast_approx) - done - show "\i::nat. finite {x::'a. approx i\x = x}" - apply (rule_tac B="(\x. prj\x) ` {x. cast\(approx i\t)\x = x}" - in finite_subset) - apply (clarsimp simp add: approx') - apply (drule_tac f="\x. emb\x" in arg_cong) - apply (rule image_eqI) - apply (rule prj_emb [symmetric]) - apply (simp add: emb_prj) - apply (simp add: cast_cast_approx) - apply (rule finite_imageI) - apply (simp add: cast_approx_fixed_iff) - apply (simp add: Collect_conj_eq) - apply (simp add: finite_fixes_approx) - done -qed - -text {* Restore original typing constraints *} - -setup {* Sign.add_const_constraint - (@{const_name "approx"}, SOME @{typ "nat \ 'a::profinite \ 'a"}) *} - -setup {* Sign.add_const_constraint - (@{const_name emb}, SOME @{typ "'a::rep \ udom"}) *} - -setup {* Sign.add_const_constraint - (@{const_name prj}, SOME @{typ "udom \ 'a::rep"}) *} - -lemma typedef_REP: - fixes Rep :: "'a::rep \ udom" - fixes Abs :: "udom \ 'a::rep" - fixes t :: TypeRep - assumes type: "type_definition Rep Abs {x. x ::: t}" - assumes below: "op \ \ \x y. Rep x \ Rep y" - assumes emb: "emb \ (\ x. Rep x)" - assumes prj: "prj \ (\ x. Abs (cast\t\x))" - shows "REP('a) = t" -proof - - have adm: "adm (\x. x \ {x. x ::: t})" - by (simp add: adm_in_deflation) + by (simp add: adm_in_sfp) have emb_beta: "\x. emb\x = Rep x" unfolding emb apply (rule beta_cfun) @@ -319,313 +152,51 @@ apply (rule typedef_cont_Abs [OF type below adm]) apply simp_all done - have emb_in_deflation: "\x::'a. emb\x ::: t" + have emb_in_sfp: "\x::'a. emb\x ::: t" using type_definition.Rep [OF type] by (simp add: emb_beta) have prj_emb: "\x::'a. prj\(emb\x) = x" unfolding prj_beta - apply (simp add: cast_fixed [OF emb_in_deflation]) + apply (simp add: cast_fixed [OF emb_in_sfp]) apply (simp add: emb_beta type_definition.Rep_inverse [OF type]) done have emb_prj: "\y. emb\(prj\y :: 'a) = cast\t\y" unfolding prj_beta emb_beta by (simp add: type_definition.Abs_inverse [OF type]) - show "REP('a) = t" - apply (rule cast_eq_imp_eq, rule ext_cfun) - apply (simp add: cast_REP emb_prj) + show "ep_pair (emb :: 'a \ udom) prj" + apply default + apply (simp add: prj_emb) + apply (simp add: emb_prj cast.below) done + show "cast\SFP('a) = emb oo (prj :: udom \ 'a)" + by (rule ext_cfun, simp add: sfp emb_prj) qed -lemma adm_mem_Collect_in_deflation: "adm (\x. x \ {x. x ::: A})" -unfolding mem_Collect_eq by (rule adm_in_deflation) +lemma typedef_SFP: + assumes "sfp \ (\a::'a::pcpo itself. t)" + shows "SFP('a::pcpo) = t" +unfolding assms .. + +text {* Restore original typing constraints *} + +setup {* Sign.add_const_constraint + (@{const_name sfp}, SOME @{typ "'a::sfp itself \ sfp"}) *} + +setup {* Sign.add_const_constraint + (@{const_name emb}, SOME @{typ "'a::sfp \ udom"}) *} + +setup {* Sign.add_const_constraint + (@{const_name prj}, SOME @{typ "udom \ 'a::sfp"}) *} + +lemma adm_mem_Collect_in_sfp: "adm (\x. x \ {x. x ::: A})" +unfolding mem_Collect_eq by (rule adm_in_sfp) use "Tools/repdef.ML" - -subsection {* Instances of class \emph{rep} *} - -subsubsection {* Universal Domain *} - -text "The Universal Domain itself is trivially representable." - -instantiation udom :: rep -begin - -definition emb_udom_def [simp]: "emb = (ID :: udom \ udom)" -definition prj_udom_def [simp]: "prj = (ID :: udom \ udom)" - -instance - apply (intro_classes) - apply (simp_all add: ep_pair.intro) -done - -end - -subsubsection {* Lifted types *} - -instantiation lift :: (countable) rep -begin - -definition emb_lift_def: - "emb = udom_emb oo (FLIFT x. Def (to_nat x))" - -definition prj_lift_def: - "prj = (FLIFT n. if (\x::'a::countable. n = to_nat x) - then Def (THE x::'a. n = to_nat x) else \) oo udom_prj" - -instance - apply (intro_classes, unfold emb_lift_def prj_lift_def) - apply (rule ep_pair_comp [OF _ ep_pair_udom]) - apply (rule ep_pair.intro) - apply (case_tac x, simp, simp) - apply (case_tac y, simp, clarsimp) -done - -end - -subsubsection {* Representable type constructors *} - -text "Functions between representable types are representable." - -instantiation cfun :: (rep, rep) rep -begin - -definition emb_cfun_def: "emb = udom_emb oo cfun_map\prj\emb" -definition prj_cfun_def: "prj = cfun_map\emb\prj oo udom_prj" - -instance - apply (intro_classes, unfold emb_cfun_def prj_cfun_def) - apply (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj ep_pair_udom) -done - -end - -text "Strict products of representable types are representable." - -instantiation sprod :: (rep, rep) rep -begin - -definition emb_sprod_def: "emb = udom_emb oo sprod_map\emb\emb" -definition prj_sprod_def: "prj = sprod_map\prj\prj oo udom_prj" - -instance - apply (intro_classes, unfold emb_sprod_def prj_sprod_def) - apply (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj ep_pair_udom) -done - -end - -text "Strict sums of representable types are representable." - -instantiation ssum :: (rep, rep) rep -begin - -definition emb_ssum_def: "emb = udom_emb oo ssum_map\emb\emb" -definition prj_ssum_def: "prj = ssum_map\prj\prj oo udom_prj" - -instance - apply (intro_classes, unfold emb_ssum_def prj_ssum_def) - apply (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj ep_pair_udom) -done - -end - -text "Up of a representable type is representable." - -instantiation "u" :: (rep) rep -begin - -definition emb_u_def: "emb = udom_emb oo u_map\emb" -definition prj_u_def: "prj = u_map\prj oo udom_prj" - -instance - apply (intro_classes, unfold emb_u_def prj_u_def) - apply (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj ep_pair_udom) -done - -end - -text "Cartesian products of representable types are representable." - -instantiation prod :: (rep, rep) rep -begin - -definition emb_cprod_def: "emb = udom_emb oo cprod_map\emb\emb" -definition prj_cprod_def: "prj = cprod_map\prj\prj oo udom_prj" - -instance - apply (intro_classes, unfold emb_cprod_def prj_cprod_def) - apply (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj ep_pair_udom) -done - -end - -subsection {* Type combinators *} - -definition - TypeRep_fun1 :: - "((udom \ udom) \ ('a \ 'a)) - \ (TypeRep \ TypeRep)" -where - "TypeRep_fun1 f = - alg_defl.basis_fun (\a. - alg_defl_principal ( - Abs_fin_defl (udom_emb oo f\(Rep_fin_defl a) oo udom_prj)))" - -definition - TypeRep_fun2 :: - "((udom \ udom) \ (udom \ udom) \ ('a \ 'a)) - \ (TypeRep \ TypeRep \ TypeRep)" -where - "TypeRep_fun2 f = - alg_defl.basis_fun (\a. - alg_defl.basis_fun (\b. - alg_defl_principal ( - Abs_fin_defl (udom_emb oo - f\(Rep_fin_defl a)\(Rep_fin_defl b) oo udom_prj))))" - -definition "cfun_defl = TypeRep_fun2 cfun_map" -definition "ssum_defl = TypeRep_fun2 ssum_map" -definition "sprod_defl = TypeRep_fun2 sprod_map" -definition "cprod_defl = TypeRep_fun2 cprod_map" -definition "u_defl = TypeRep_fun1 u_map" - -lemma Rep_fin_defl_mono: "a \ b \ Rep_fin_defl a \ Rep_fin_defl b" -unfolding below_fin_defl_def . - -lemma cast_TypeRep_fun1: - assumes f: "\a. finite_deflation a \ finite_deflation (f\a)" - shows "cast\(TypeRep_fun1 f\A) = udom_emb oo f\(cast\A) oo udom_prj" -proof - - have 1: "\a. finite_deflation (udom_emb oo f\(Rep_fin_defl a) oo udom_prj)" - apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom]) - apply (rule f, rule finite_deflation_Rep_fin_defl) - done - show ?thesis - by (induct A rule: alg_defl.principal_induct, simp) - (simp only: TypeRep_fun1_def - alg_defl.basis_fun_principal - alg_defl.basis_fun_mono - alg_defl.principal_mono - Abs_fin_defl_mono [OF 1 1] - monofun_cfun below_refl - Rep_fin_defl_mono - cast_alg_defl_principal - Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) -qed - -lemma cast_TypeRep_fun2: - assumes f: "\a b. finite_deflation a \ finite_deflation b \ - finite_deflation (f\a\b)" - shows "cast\(TypeRep_fun2 f\A\B) = - udom_emb oo f\(cast\A)\(cast\B) oo udom_prj" -proof - - have 1: "\a b. finite_deflation - (udom_emb oo f\(Rep_fin_defl a)\(Rep_fin_defl b) oo udom_prj)" - apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom]) - apply (rule f, (rule finite_deflation_Rep_fin_defl)+) - done - show ?thesis - by (induct A B rule: alg_defl.principal_induct2, simp, simp) - (simp only: TypeRep_fun2_def - alg_defl.basis_fun_principal - alg_defl.basis_fun_mono - alg_defl.principal_mono - Abs_fin_defl_mono [OF 1 1] - monofun_cfun below_refl - Rep_fin_defl_mono - cast_alg_defl_principal - Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) -qed - -lemma cast_cfun_defl: - "cast\(cfun_defl\A\B) = udom_emb oo cfun_map\(cast\A)\(cast\B) oo udom_prj" -unfolding cfun_defl_def -apply (rule cast_TypeRep_fun2) -apply (erule (1) finite_deflation_cfun_map) -done - -lemma cast_ssum_defl: - "cast\(ssum_defl\A\B) = udom_emb oo ssum_map\(cast\A)\(cast\B) oo udom_prj" -unfolding ssum_defl_def -apply (rule cast_TypeRep_fun2) -apply (erule (1) finite_deflation_ssum_map) -done - -lemma cast_sprod_defl: - "cast\(sprod_defl\A\B) = udom_emb oo sprod_map\(cast\A)\(cast\B) oo udom_prj" -unfolding sprod_defl_def -apply (rule cast_TypeRep_fun2) -apply (erule (1) finite_deflation_sprod_map) -done - -lemma cast_cprod_defl: - "cast\(cprod_defl\A\B) = udom_emb oo cprod_map\(cast\A)\(cast\B) oo udom_prj" -unfolding cprod_defl_def -apply (rule cast_TypeRep_fun2) -apply (erule (1) finite_deflation_cprod_map) -done - -lemma cast_u_defl: - "cast\(u_defl\A) = udom_emb oo u_map\(cast\A) oo udom_prj" -unfolding u_defl_def -apply (rule cast_TypeRep_fun1) -apply (erule finite_deflation_u_map) -done - -text {* REP of type constructor = type combinator *} - -lemma REP_cfun: "REP('a \ 'b) = cfun_defl\REP('a)\REP('b)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_cfun_defl) -apply (simp add: cfun_map_def) -apply (simp only: prj_cfun_def emb_cfun_def) -apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom]) -done - -lemma REP_ssum: "REP('a \ 'b) = ssum_defl\REP('a)\REP('b)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_ssum_defl) -apply (simp add: prj_ssum_def) -apply (simp add: emb_ssum_def) -apply (simp add: ssum_map_map cfcomp1) -done - -lemma REP_sprod: "REP('a \ 'b) = sprod_defl\REP('a)\REP('b)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_sprod_defl) -apply (simp add: prj_sprod_def) -apply (simp add: emb_sprod_def) -apply (simp add: sprod_map_map cfcomp1) -done - -lemma REP_cprod: "REP('a \ 'b) = cprod_defl\REP('a)\REP('b)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_cprod_defl) -apply (simp add: prj_cprod_def) -apply (simp add: emb_cprod_def) -apply (simp add: cprod_map_map cfcomp1) -done - -lemma REP_up: "REP('a u) = u_defl\REP('a)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_u_defl) -apply (simp add: prj_u_def) -apply (simp add: emb_u_def) -apply (simp add: u_map_map cfcomp1) -done - -lemmas REP_simps = - REP_cfun - REP_ssum - REP_sprod - REP_cprod - REP_up - subsection {* Isomorphic deflations *} definition - isodefl :: "('a::rep \ 'a) \ udom alg_defl \ bool" + isodefl :: "('a::sfp \ 'a) \ sfp \ bool" where "isodefl d t \ cast\t = emb oo d oo prj" @@ -640,10 +211,10 @@ by (drule cfun_fun_cong [where x="\"], simp) lemma isodefl_imp_deflation: - fixes d :: "'a::rep \ 'a" + fixes d :: "'a::sfp \ 'a" assumes "isodefl d t" shows "deflation d" proof - note prems [unfolded isodefl_def, simp] + note assms [unfolded isodefl_def, simp] fix x :: 'a show "d\(d\x) = d\x" using cast.idem [of t "emb\x"] by simp @@ -651,12 +222,12 @@ using cast.below [of t "emb\x"] by simp qed -lemma isodefl_ID_REP: "isodefl (ID :: 'a \ 'a) REP('a)" -unfolding isodefl_def by (simp add: cast_REP) +lemma isodefl_ID_SFP: "isodefl (ID :: 'a \ 'a) SFP('a)" +unfolding isodefl_def by (simp add: cast_SFP) -lemma isodefl_REP_imp_ID: "isodefl (d :: 'a \ 'a) REP('a) \ d = ID" +lemma isodefl_SFP_imp_ID: "isodefl (d :: 'a \ 'a) SFP('a) \ d = ID" unfolding isodefl_def -apply (simp add: cast_REP) +apply (simp add: cast_SFP) apply (simp add: expand_cfun_eq) apply (rule allI) apply (drule_tac x="emb\x" in spec) @@ -684,66 +255,66 @@ apply (rule isodefl_lub, simp, simp) apply (induct_tac i) apply (simp add: isodefl_bottom) -apply (simp add: prems) +apply (simp add: assms) done lemma isodefl_coerce: fixes d :: "'a \ 'a" - assumes REP: "REP('b) = REP('a)" + assumes SFP: "SFP('b) = SFP('a)" shows "isodefl d t \ isodefl (coerce oo d oo coerce :: 'b \ 'b) t" unfolding isodefl_def apply (simp add: expand_cfun_eq) -apply (simp add: emb_coerce coerce_prj REP) +apply (simp add: emb_coerce coerce_prj SFP) done lemma isodefl_abs_rep: fixes abs and rep and d - assumes REP: "REP('b) = REP('a)" + assumes SFP: "SFP('b) = SFP('a)" assumes abs_def: "abs \ (coerce :: 'a \ 'b)" assumes rep_def: "rep \ (coerce :: 'b \ 'a)" shows "isodefl d t \ isodefl (abs oo d oo rep) t" -unfolding abs_def rep_def using REP by (rule isodefl_coerce) +unfolding abs_def rep_def using SFP by (rule isodefl_coerce) lemma isodefl_cfun: "isodefl d1 t1 \ isodefl d2 t2 \ - isodefl (cfun_map\d1\d2) (cfun_defl\t1\t2)" + isodefl (cfun_map\d1\d2) (cfun_sfp\t1\t2)" apply (rule isodeflI) -apply (simp add: cast_cfun_defl cast_isodefl) +apply (simp add: cast_cfun_sfp cast_isodefl) apply (simp add: emb_cfun_def prj_cfun_def) apply (simp add: cfun_map_map cfcomp1) done lemma isodefl_ssum: "isodefl d1 t1 \ isodefl d2 t2 \ - isodefl (ssum_map\d1\d2) (ssum_defl\t1\t2)" + isodefl (ssum_map\d1\d2) (ssum_sfp\t1\t2)" apply (rule isodeflI) -apply (simp add: cast_ssum_defl cast_isodefl) +apply (simp add: cast_ssum_sfp cast_isodefl) apply (simp add: emb_ssum_def prj_ssum_def) apply (simp add: ssum_map_map isodefl_strict) done lemma isodefl_sprod: "isodefl d1 t1 \ isodefl d2 t2 \ - isodefl (sprod_map\d1\d2) (sprod_defl\t1\t2)" + isodefl (sprod_map\d1\d2) (sprod_sfp\t1\t2)" apply (rule isodeflI) -apply (simp add: cast_sprod_defl cast_isodefl) +apply (simp add: cast_sprod_sfp cast_isodefl) apply (simp add: emb_sprod_def prj_sprod_def) apply (simp add: sprod_map_map isodefl_strict) done lemma isodefl_cprod: "isodefl d1 t1 \ isodefl d2 t2 \ - isodefl (cprod_map\d1\d2) (cprod_defl\t1\t2)" + isodefl (cprod_map\d1\d2) (prod_sfp\t1\t2)" apply (rule isodeflI) -apply (simp add: cast_cprod_defl cast_isodefl) -apply (simp add: emb_cprod_def prj_cprod_def) +apply (simp add: cast_prod_sfp cast_isodefl) +apply (simp add: emb_prod_def prj_prod_def) apply (simp add: cprod_map_map cfcomp1) done lemma isodefl_u: - "isodefl d t \ isodefl (u_map\d) (u_defl\t)" + "isodefl d t \ isodefl (u_map\d) (u_sfp\t)" apply (rule isodeflI) -apply (simp add: cast_u_defl cast_isodefl) +apply (simp add: cast_u_sfp cast_isodefl) apply (simp add: emb_u_def prj_u_def) apply (simp add: u_map_map) done @@ -754,19 +325,19 @@ setup {* fold Domain_Isomorphism.add_type_constructor - [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun}, + [(@{type_name cfun}, @{term cfun_sfp}, @{const_name cfun_map}, @{thm SFP_cfun}, @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}), - (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum}, + (@{type_name ssum}, @{term ssum_sfp}, @{const_name ssum_map}, @{thm SFP_ssum}, @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}), - (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod}, + (@{type_name sprod}, @{term sprod_sfp}, @{const_name sprod_map}, @{thm SFP_sprod}, @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}), - (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod}, + (@{type_name prod}, @{term cprod_sfp}, @{const_name cprod_map}, @{thm SFP_prod}, @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}), - (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm REP_up}, + (@{type_name "u"}, @{term u_sfp}, @{const_name u_map}, @{thm SFP_u}, @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})] *} diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Sprod.thy --- a/src/HOLCF/Sprod.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Sprod.thy Wed Oct 06 10:49:27 2010 -0700 @@ -5,7 +5,7 @@ header {* The type of strict products *} theory Sprod -imports Bifinite +imports Algebraic begin default_sort pcpo @@ -310,37 +310,66 @@ by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) qed -subsection {* Strict product is a bifinite domain *} +subsection {* Strict product is an SFP domain *} + +definition + sprod_approx :: "nat \ udom \ udom \ udom \ udom" +where + "sprod_approx = (\i. sprod_map\(udom_approx i)\(udom_approx i))" -instantiation sprod :: (bifinite, bifinite) bifinite +lemma sprod_approx: "approx_chain sprod_approx" +proof (rule approx_chain.intro) + show "chain (\i. sprod_approx i)" + unfolding sprod_approx_def by simp + show "(\i. sprod_approx i) = ID" + unfolding sprod_approx_def + by (simp add: lub_distribs sprod_map_ID) + show "\i. finite_deflation (sprod_approx i)" + unfolding sprod_approx_def + by (intro finite_deflation_sprod_map finite_deflation_udom_approx) +qed + +definition sprod_sfp :: "sfp \ sfp \ sfp" +where "sprod_sfp = sfp_fun2 sprod_approx sprod_map" + +lemma cast_sprod_sfp: + "cast\(sprod_sfp\A\B) = + udom_emb sprod_approx oo + sprod_map\(cast\A)\(cast\B) oo + udom_prj sprod_approx" +unfolding sprod_sfp_def +apply (rule cast_sfp_fun2 [OF sprod_approx]) +apply (erule (1) finite_deflation_sprod_map) +done + +instantiation sprod :: (sfp, sfp) sfp begin definition - approx_sprod_def: - "approx = (\n. sprod_map\(approx n)\(approx n))" + "emb = udom_emb sprod_approx oo sprod_map\emb\emb" + +definition + "prj = sprod_map\prj\prj oo udom_prj sprod_approx" + +definition + "sfp (t::('a \ 'b) itself) = sprod_sfp\SFP('a)\SFP('b)" instance proof - fix i :: nat and x :: "'a \ 'b" - show "chain (approx :: nat \ 'a \ 'b \ 'a \ 'b)" - unfolding approx_sprod_def by simp - show "(\i. approx i\x) = x" - unfolding approx_sprod_def sprod_map_def - by (simp add: lub_distribs eta_cfun) - show "approx i\(approx i\x) = approx i\x" - unfolding approx_sprod_def sprod_map_def - by (simp add: ssplit_def strictify_conv_if) - show "finite {x::'a \ 'b. approx i\x = x}" - unfolding approx_sprod_def - by (intro finite_deflation.finite_fixes - finite_deflation_sprod_map - finite_deflation_approx) + show "ep_pair emb (prj :: udom \ 'a \ 'b)" + unfolding emb_sprod_def prj_sprod_def + using ep_pair_udom [OF sprod_approx] + by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj) +next + show "cast\SFP('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" + unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp + by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map) qed end -lemma approx_spair [simp]: - "approx i\(:x, y:) = (:approx i\x, approx i\y:)" -unfolding approx_sprod_def sprod_map_def -by (simp add: ssplit_def strictify_conv_if) +text {* SFP of type constructor = type combinator *} + +lemma SFP_sprod: "SFP('a::sfp \ 'b::sfp) = sprod_sfp\SFP('a)\SFP('b)" +by (rule sfp_sprod_def) end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Ssum.thy --- a/src/HOLCF/Ssum.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Ssum.thy Wed Oct 06 10:49:27 2010 -0700 @@ -295,37 +295,64 @@ by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) qed -subsection {* Strict sum is a bifinite domain *} +subsection {* Strict sum is an SFP domain *} + +definition + ssum_approx :: "nat \ udom \ udom \ udom \ udom" +where + "ssum_approx = (\i. ssum_map\(udom_approx i)\(udom_approx i))" -instantiation ssum :: (bifinite, bifinite) bifinite +lemma ssum_approx: "approx_chain ssum_approx" +proof (rule approx_chain.intro) + show "chain (\i. ssum_approx i)" + unfolding ssum_approx_def by simp + show "(\i. ssum_approx i) = ID" + unfolding ssum_approx_def + by (simp add: lub_distribs ssum_map_ID) + show "\i. finite_deflation (ssum_approx i)" + unfolding ssum_approx_def + by (intro finite_deflation_ssum_map finite_deflation_udom_approx) +qed + +definition ssum_sfp :: "sfp \ sfp \ sfp" +where "ssum_sfp = sfp_fun2 ssum_approx ssum_map" + +lemma cast_ssum_sfp: + "cast\(ssum_sfp\A\B) = + udom_emb ssum_approx oo ssum_map\(cast\A)\(cast\B) oo udom_prj ssum_approx" +unfolding ssum_sfp_def +apply (rule cast_sfp_fun2 [OF ssum_approx]) +apply (erule (1) finite_deflation_ssum_map) +done + +instantiation ssum :: (sfp, sfp) sfp begin definition - approx_ssum_def: - "approx = (\n. ssum_map\(approx n)\(approx n))" + "emb = udom_emb ssum_approx oo ssum_map\emb\emb" -lemma approx_sinl [simp]: "approx i\(sinl\x) = sinl\(approx i\x)" -unfolding approx_ssum_def by (cases "x = \") simp_all +definition + "prj = ssum_map\prj\prj oo udom_prj ssum_approx" -lemma approx_sinr [simp]: "approx i\(sinr\x) = sinr\(approx i\x)" -unfolding approx_ssum_def by (cases "x = \") simp_all +definition + "sfp (t::('a \ 'b) itself) = ssum_sfp\SFP('a)\SFP('b)" instance proof - fix i :: nat and x :: "'a \ 'b" - show "chain (approx :: nat \ 'a \ 'b \ 'a \ 'b)" - unfolding approx_ssum_def by simp - show "(\i. approx i\x) = x" - unfolding approx_ssum_def - by (cases x, simp_all add: lub_distribs) - show "approx i\(approx i\x) = approx i\x" - by (cases x, simp add: approx_ssum_def, simp, simp) - show "finite {x::'a \ 'b. approx i\x = x}" - unfolding approx_ssum_def - by (intro finite_deflation.finite_fixes - finite_deflation_ssum_map - finite_deflation_approx) + show "ep_pair emb (prj :: udom \ 'a \ 'b)" + unfolding emb_ssum_def prj_ssum_def + using ep_pair_udom [OF ssum_approx] + by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj) +next + show "cast\SFP('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" + unfolding emb_ssum_def prj_ssum_def sfp_ssum_def cast_ssum_sfp + by (simp add: cast_SFP oo_def expand_cfun_eq ssum_map_map) qed end +text {* SFP of type constructor = type combinator *} + +lemma SFP_ssum: "SFP('a::sfp \ 'b::sfp) = ssum_sfp\SFP('a)\SFP('b)" +by (rule sfp_ssum_def) + end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Wed Oct 06 10:49:27 2010 -0700 @@ -144,7 +144,7 @@ fun thy_type (dname,tvars,mx) = (dname, length tvars, mx); fun thy_arity (dname,tvars,mx) = - (Sign.full_name thy dname, map (snd o dest_TFree) tvars, @{sort rep}); + (Sign.full_name thy dname, map (snd o dest_TFree) tvars, arg_sort false); (* this theory is used just for parsing and error checking *) val tmp_thy = thy @@ -213,7 +213,7 @@ end; fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo}; -fun rep_arg lazy = @{sort rep}; +fun rep_arg lazy = @{sort sfp}; val add_domain = gen_add_domain Sign.certify_typ Domain_Axioms.add_axioms pcpo_arg; diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Oct 06 10:49:27 2010 -0700 @@ -48,7 +48,7 @@ structure DeflData = Theory_Data ( - (* terms like "foo_defl" *) + (* terms like "foo_sfp" *) type T = term Symtab.table; val empty = Symtab.empty; val extend = I; @@ -57,7 +57,7 @@ structure RepData = Theory_Data ( - (* theorems like "REP('a foo) = foo_defl$REP('a)" *) + (* theorems like "SFP('a foo) = foo_sfp$SFP('a)" *) type T = thm list; val empty = []; val extend = I; @@ -83,11 +83,11 @@ ); fun add_type_constructor - (tname, defl_const, map_name, REP_thm, + (tname, defl_const, map_name, SFP_thm, isodefl_thm, map_ID_thm, defl_map_thm) = DeflData.map (Symtab.insert (K true) (tname, defl_const)) #> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm) - #> RepData.map (Thm.add_thm REP_thm) + #> RepData.map (Thm.add_thm SFP_thm) #> IsodeflData.map (Thm.add_thm isodefl_thm) #> MapIdData.map (Thm.add_thm map_ID_thm); @@ -104,19 +104,19 @@ infixr 6 ->>; infix -->>; -val deflT = @{typ "udom alg_defl"}; +val sfpT = @{typ "sfp"}; fun mapT (T as Type (_, Ts)) = (map (fn T => T ->> T) Ts) -->> (T ->> T) | mapT T = T ->> T; -fun mk_Rep_of T = - Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T; +fun mk_SFP T = + Const (@{const_name sfp}, Term.itselfT T --> sfpT) $ Logic.mk_type T; fun coerce_const T = Const (@{const_name coerce}, T); fun isodefl_const T = - Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT); + Const (@{const_name isodefl}, (T ->> T) --> sfpT --> HOLogic.boolT); fun mk_deflation t = Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t; @@ -218,13 +218,13 @@ let fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts | is_closed_typ _ = false; - fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT) + fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, sfpT) | defl_of (TVar _) = error ("defl_of_typ: TVar") | defl_of (T as Type (c, Ts)) = case Symtab.lookup tab c of SOME t => list_ccomb (t, map defl_of Ts) | NONE => if is_closed_typ T - then mk_Rep_of T + then mk_SFP T else error ("defl_of_typ: type variable under unsupported type constructor " ^ c); in defl_of T end; @@ -443,7 +443,7 @@ (* declare deflation combinator constants *) fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy = let - val defl_type = map (K deflT) vs -->> deflT; + val defl_type = map (K sfpT) vs -->> sfpT; val defl_bind = Binding.suffix_name "_defl" tbind; in Sign.declare_const ((defl_bind, defl_type), NoSyn) thy @@ -470,34 +470,34 @@ fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy = let fun tfree a = TFree (a, the (AList.lookup (op =) sorts a)) - val reps = map (mk_Rep_of o tfree) vs; + val reps = map (mk_SFP o tfree) vs; val defl = list_ccomb (defl_const, reps); - val ((_, _, _, {REP, ...}), thy) = + val ((_, _, _, {SFP, ...}), thy) = Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy; in - (REP, thy) + (SFP, thy) end; - val (REP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy; - val thy = RepData.map (fold Thm.add_thm REP_thms) thy; + val (SFP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy; + val thy = RepData.map (fold Thm.add_thm SFP_thms) thy; - (* prove REP equations *) - fun mk_REP_eq_thm (lhsT, rhsT) = + (* prove SFP equations *) + fun mk_SFP_eq_thm (lhsT, rhsT) = let - val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT); - val REP_simps = RepData.get thy; + val goal = mk_eqs (mk_SFP lhsT, mk_SFP rhsT); + val SFP_simps = RepData.get thy; val tac = - rewrite_goals_tac (map mk_meta_eq REP_simps) + rewrite_goals_tac (map mk_meta_eq SFP_simps) THEN resolve_tac defl_unfold_thms 1; in Goal.prove_global thy [] [] goal (K tac) end; - val REP_eq_thms = map mk_REP_eq_thm dom_eqns; + val SFP_eq_thms = map mk_SFP_eq_thm dom_eqns; - (* register REP equations *) - val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dbinds; + (* register SFP equations *) + val SFP_eq_binds = map (Binding.prefix_name "SFP_eq_") dbinds; val (_, thy) = thy |> (Global_Theory.add_thms o map Thm.no_attributes) - (REP_eq_binds ~~ REP_eq_thms); + (SFP_eq_binds ~~ SFP_eq_thms); (* define rep/abs functions *) fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy = @@ -516,10 +516,10 @@ |>> ListPair.unzip; (* prove isomorphism and isodefl rules *) - fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy = + fun mk_iso_thms ((tbind, SFP_eq), (rep_def, abs_def)) thy = let fun make thm = - Drule.zero_var_indexes (thm OF [REP_eq, abs_def, rep_def]); + Drule.zero_var_indexes (thm OF [SFP_eq, abs_def, rep_def]); val rep_iso_thm = make @{thm domain_rep_iso}; val abs_iso_thm = make @{thm domain_abs_iso}; val isodefl_thm = make @{thm isodefl_abs_rep}; @@ -532,7 +532,7 @@ end; val ((iso_thms, isodefl_abs_rep_thms), thy) = thy - |> fold_map mk_iso_thms (dbinds ~~ REP_eq_thms ~~ rep_abs_defs) + |> fold_map mk_iso_thms (dbinds ~~ SFP_eq_thms ~~ rep_abs_defs) |>> ListPair.unzip; (* collect info about rep/abs *) @@ -561,7 +561,7 @@ val isodefl_thm = let fun unprime a = Library.unprefix "'" a; - fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT); + fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), sfpT); fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T); fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T); fun mk_goal ((map_const, defl_const), (T, rhsT)) = @@ -579,9 +579,9 @@ @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id}; val bottom_rules = @{thms fst_strict snd_strict isodefl_bottom simp_thms}; - val REP_simps = map (fn th => th RS sym) (RepData.get thy); + val SFP_simps = map (fn th => th RS sym) (RepData.get thy); val isodefl_rules = - @{thms conjI isodefl_ID_REP} + @{thms conjI isodefl_ID_SFP} @ isodefl_abs_rep_thms @ IsodeflData.get thy; in @@ -595,7 +595,7 @@ simp_tac (HOL_basic_ss addsimps bottom_rules) 1, simp_tac beta_ss 1, simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1, - simp_tac (HOL_basic_ss addsimps REP_simps) 1, + simp_tac (HOL_basic_ss addsimps SFP_simps) 1, REPEAT (etac @{thm conjE} 1), REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)]) end; @@ -613,23 +613,23 @@ (* prove map_ID theorems *) fun prove_map_ID_thm - (((map_const, (lhsT, _)), REP_thm), isodefl_thm) = + (((map_const, (lhsT, _)), SFP_thm), isodefl_thm) = let val Ts = snd (dest_Type lhsT); val lhs = list_ccomb (map_const, map mk_ID Ts); val goal = mk_eqs (lhs, mk_ID lhsT); val tac = EVERY - [rtac @{thm isodefl_REP_imp_ID} 1, - stac REP_thm 1, + [rtac @{thm isodefl_SFP_imp_ID} 1, + stac SFP_thm 1, rtac isodefl_thm 1, - REPEAT (rtac @{thm isodefl_ID_REP} 1)]; + REPEAT (rtac @{thm isodefl_ID_SFP} 1)]; in Goal.prove_global thy [] [] goal (K tac) end; val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds; val map_ID_thms = map prove_map_ID_thm - (map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms); + (map_consts ~~ dom_eqns ~~ SFP_thms ~~ isodefl_thms); val (_, thy) = thy |> (Global_Theory.add_thms o map Thm.no_attributes) (map_ID_binds ~~ map_ID_thms); diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Tools/repdef.ML Wed Oct 06 10:49:27 2010 -0700 @@ -7,7 +7,7 @@ signature REPDEF = sig type rep_info = - { emb_def: thm, prj_def: thm, approx_def: thm, REP: thm } + { emb_def: thm, prj_def: thm, sfp_def: thm, SFP: thm } val add_repdef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> theory -> @@ -28,20 +28,19 @@ (** type definitions **) type rep_info = - { emb_def: thm, prj_def: thm, approx_def: thm, REP: thm }; + { emb_def: thm, prj_def: thm, sfp_def: thm, SFP: thm }; (* building types and terms *) val udomT = @{typ udom}; -fun alg_deflT T = Type (@{type_name alg_defl}, [T]); +val sfpT = @{typ sfp}; fun emb_const T = Const (@{const_name emb}, T ->> udomT); fun prj_const T = Const (@{const_name prj}, udomT ->> T); -fun approx_const T = Const (@{const_name approx}, natT --> (T ->> T)); +fun sfp_const T = Const (@{const_name sfp}, Term.itselfT T --> sfpT); -fun cast_const T = Const (@{const_name cast}, alg_deflT T ->> T ->> T); fun mk_cast (t, x) = capply_const (udomT, udomT) - $ (capply_const (alg_deflT udomT, udomT ->> udomT) $ cast_const udomT $ t) + $ (capply_const (sfpT, udomT ->> udomT) $ @{const cast} $ t) $ x; (* manipulating theorems *) @@ -71,8 +70,8 @@ val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl; val deflT = Term.fastype_of defl; - val _ = if deflT = @{typ "udom alg_defl"} then () - else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT)); + val _ = if deflT = @{typ "sfp"} then () + else error ("Not type sfp: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT)); (*lhs*) val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args; @@ -85,12 +84,12 @@ |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); (*set*) - val in_defl = @{term "in_deflation :: udom => udom alg_defl => bool"}; + val in_defl = @{term "in_sfp :: udom => sfp => bool"}; val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl); (*pcpodef*) - val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_deflation} 1; - val tac2 = rtac @{thm adm_mem_Collect_in_deflation} 1; + val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_sfp} 1; + val tac2 = rtac @{thm adm_mem_Collect_in_sfp} 1; val ((info, cpo_info, pcpo_info), thy) = thy |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2); @@ -100,52 +99,48 @@ val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const); val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $ Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0))); - val repdef_approx_const = - Const (@{const_name repdef_approx}, (newT --> udomT) --> (udomT --> newT) - --> alg_deflT udomT --> natT --> (newT ->> newT)); - val approx_eqn = Logic.mk_equals (approx_const newT, - repdef_approx_const $ Rep_const $ Abs_const $ defl); + val sfp_eqn = Logic.mk_equals (sfp_const newT, + Abs ("x", Term.itselfT newT, defl)); val name_def = Binding.suffix_name "_def" name; val emb_bind = (Binding.prefix_name "emb_" name_def, []); val prj_bind = (Binding.prefix_name "prj_" name_def, []); - val approx_bind = (Binding.prefix_name "approx_" name_def, []); + val sfp_bind = (Binding.prefix_name "sfp_" name_def, []); (*instantiate class rep*) val lthy = thy - |> Class.instantiation ([full_tname], lhs_tfrees, @{sort rep}); + |> Class.instantiation ([full_tname], lhs_tfrees, @{sort sfp}); val ((_, (_, emb_ldef)), lthy) = Specification.definition (NONE, (emb_bind, emb_eqn)) lthy; val ((_, (_, prj_ldef)), lthy) = Specification.definition (NONE, (prj_bind, prj_eqn)) lthy; - val ((_, (_, approx_ldef)), lthy) = - Specification.definition (NONE, (approx_bind, approx_eqn)) lthy; + val ((_, (_, sfp_ldef)), lthy) = + Specification.definition (NONE, (sfp_bind, sfp_eqn)) lthy; val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef; val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef; - val approx_def = singleton (ProofContext.export lthy ctxt_thy) approx_ldef; + val sfp_def = singleton (ProofContext.export lthy ctxt_thy) sfp_ldef; val type_definition_thm = MetaSimplifier.rewrite_rule (the_list (#set_def (#2 info))) (#type_definition (#2 info)); val typedef_thms = - [type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def]; + [type_definition_thm, #below_def cpo_info, emb_def, prj_def, sfp_def]; val thy = lthy |> Class.prove_instantiation_instance (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1)) |> Local_Theory.exit_global; (*other theorems*) - val typedef_thms' = map (Thm.transfer thy) - [type_definition_thm, #below_def cpo_info, emb_def, prj_def]; - val (REP_thm, thy) = thy + val sfp_thm' = Thm.transfer thy sfp_def; + val (SFP_thm, thy) = thy |> Sign.add_path (Binding.name_of name) |> Global_Theory.add_thm - ((Binding.prefix_name "REP_" name, - Drule.zero_var_indexes (@{thm typedef_REP} OF typedef_thms')), []) + ((Binding.prefix_name "SFP_" name, + Drule.zero_var_indexes (@{thm typedef_SFP} OF [sfp_thm'])), []) ||> Sign.restore_naming thy; val rep_info = - { emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm }; + { emb_def = emb_def, prj_def = prj_def, sfp_def = sfp_def, SFP = SFP_thm }; in ((info, cpo_info, pcpo_info, rep_info), thy) end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Tutorial/New_Domain.thy --- a/src/HOLCF/Tutorial/New_Domain.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Tutorial/New_Domain.thy Wed Oct 06 10:49:27 2010 -0700 @@ -9,14 +9,14 @@ begin text {* - The definitional domain package only works with representable domains, - i.e. types in class @{text rep}. + The definitional domain package only works with SFP domains, + i.e. types in class @{text sfp}. *} -default_sort rep +default_sort sfp text {* - Provided that @{text rep} is the default sort, the @{text new_domain} + Provided that @{text sfp} is the default sort, the @{text new_domain} package should work with any type definition supported by the old domain package. *} diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Universal.thy --- a/src/HOLCF/Universal.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Universal.thy Wed Oct 06 10:49:27 2010 -0700 @@ -5,10 +5,12 @@ header {* A universal bifinite domain *} theory Universal -imports CompactBasis Nat_Bijection +imports Completion Deflation Nat_Bijection begin -subsection {* Basis datatype *} +subsection {* Basis for universal domain *} + +subsubsection {* Basis datatype *} types ubasis = nat @@ -75,7 +77,7 @@ apply (simp add: 2 node_gt1 node_gt2) done -subsection {* Basis ordering *} +subsubsection {* Basis ordering *} inductive ubasis_le :: "nat \ nat \ bool" @@ -95,6 +97,12 @@ apply (erule ubasis_le_lower) done +interpretation udom: preorder ubasis_le +apply default +apply (rule ubasis_le_refl) +apply (erule (1) ubasis_le_trans) +done + subsubsection {* Generic take function *} function @@ -187,66 +195,6 @@ apply simp done -subsubsection {* Take function for \emph{ubasis} *} - -definition - ubasis_take :: "nat \ ubasis \ ubasis" -where - "ubasis_take n = ubasis_until (\x. x \ n)" - -lemma ubasis_take_le: "ubasis_take n x \ n" -unfolding ubasis_take_def by (rule ubasis_until, rule le0) - -lemma ubasis_take_same: "x \ n \ ubasis_take n x = x" -unfolding ubasis_take_def by (rule ubasis_until_same) - -lemma ubasis_take_idem: "ubasis_take n (ubasis_take n x) = ubasis_take n x" -by (rule ubasis_take_same [OF ubasis_take_le]) - -lemma ubasis_take_0 [simp]: "ubasis_take 0 x = 0" -unfolding ubasis_take_def by (simp add: ubasis_until_0) - -lemma ubasis_take_less: "ubasis_le (ubasis_take n x) x" -unfolding ubasis_take_def by (rule ubasis_until_less) - -lemma ubasis_take_chain: "ubasis_le (ubasis_take n x) (ubasis_take (Suc n) x)" -unfolding ubasis_take_def by (rule ubasis_until_chain) simp - -lemma ubasis_take_mono: - assumes "ubasis_le x y" - shows "ubasis_le (ubasis_take n x) (ubasis_take n y)" -unfolding ubasis_take_def - apply (rule ubasis_until_mono [OF _ prems]) - apply (frule (2) order_less_le_trans [OF node_gt2]) - apply (erule order_less_imp_le) -done - -lemma finite_range_ubasis_take: "finite (range (ubasis_take n))" -apply (rule finite_subset [where B="{..n}"]) -apply (simp add: subset_eq ubasis_take_le) -apply simp -done - -lemma ubasis_take_covers: "\n. ubasis_take n x = x" -apply (rule exI [where x=x]) -apply (simp add: ubasis_take_same) -done - -interpretation udom: preorder ubasis_le -apply default -apply (rule ubasis_le_refl) -apply (erule (1) ubasis_le_trans) -done - -interpretation udom: basis_take ubasis_le ubasis_take -apply default -apply (rule ubasis_take_less) -apply (rule ubasis_take_idem) -apply (erule ubasis_take_mono) -apply (rule ubasis_take_chain) -apply (rule finite_range_ubasis_take) -apply (rule ubasis_take_covers) -done subsection {* Defining the universal domain by ideal completion *} @@ -263,17 +211,17 @@ end instance udom :: po -by (rule udom.typedef_ideal_po - [OF type_definition_udom below_udom_def]) +using type_definition_udom below_udom_def +by (rule udom.typedef_ideal_po) instance udom :: cpo -by (rule udom.typedef_ideal_cpo - [OF type_definition_udom below_udom_def]) +using type_definition_udom below_udom_def +by (rule udom.typedef_ideal_cpo) lemma Rep_udom_lub: "chain Y \ Rep_udom (\i. Y i) = (\i. Rep_udom (Y i))" -by (rule udom.typedef_ideal_rep_contlub - [OF type_definition_udom below_udom_def]) +using type_definition_udom below_udom_def +by (rule udom.typedef_ideal_rep_contlub) lemma ideal_Rep_udom: "udom.ideal (Rep_udom xs)" by (rule Rep_udom [unfolded mem_Collect_eq]) @@ -288,12 +236,13 @@ by (simp add: Abs_udom_inverse udom.ideal_principal) interpretation udom: - ideal_completion ubasis_le ubasis_take udom_principal Rep_udom + ideal_completion ubasis_le udom_principal Rep_udom apply unfold_locales apply (rule ideal_Rep_udom) apply (erule Rep_udom_lub) apply (rule Rep_udom_principal) apply (simp only: below_udom_def) +apply (rule exI, rule inj_on_id) done text {* Universal domain is pointed *} @@ -309,43 +258,60 @@ lemma inst_udom_pcpo: "\ = udom_principal 0" by (rule udom_minimal [THEN UU_I, symmetric]) -text {* Universal domain is bifinite *} + +subsection {* Compact bases of domains *} -instantiation udom :: bifinite +typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}" +by auto + +lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)" +by (rule Rep_compact_basis [unfolded mem_Collect_eq]) + +instantiation compact_basis :: (pcpo) below begin definition - approx_udom_def: "approx = udom.completion_approx" + compact_le_def: + "(op \) \ (\x y. Rep_compact_basis x \ Rep_compact_basis y)" -instance -apply (intro_classes, unfold approx_udom_def) -apply (rule udom.chain_completion_approx) -apply (rule udom.lub_completion_approx) -apply (rule udom.completion_approx_idem) -apply (rule udom.finite_fixes_completion_approx) -done - +instance .. end -lemma approx_udom_principal [simp]: - "approx n\(udom_principal x) = udom_principal (ubasis_take n x)" -unfolding approx_udom_def -by (rule udom.completion_approx_principal) +instance compact_basis :: (pcpo) po +using type_definition_compact_basis compact_le_def +by (rule typedef_po) + +definition + approximants :: "'a \ 'a compact_basis set" where + "approximants = (\x. {a. Rep_compact_basis a \ x})" -lemma approx_eq_udom_principal: - "\a\Rep_udom x. approx n\x = udom_principal (ubasis_take n a)" -unfolding approx_udom_def -by (rule udom.completion_approx_eq_principal) +definition + compact_bot :: "'a::pcpo compact_basis" where + "compact_bot = Abs_compact_basis \" + +lemma Rep_compact_bot [simp]: "Rep_compact_basis compact_bot = \" +unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse) + +lemma compact_bot_minimal [simp]: "compact_bot \ a" +unfolding compact_le_def Rep_compact_bot by simp subsection {* Universality of \emph{udom} *} -default_sort bifinite +text {* We use a locale to parameterize the construction over a chain +of approx functions on the type to be embedded. *} + +locale approx_chain = + fixes approx :: "nat \ 'a::pcpo \ 'a" + assumes chain_approx [simp]: "chain (\i. approx i)" + assumes lub_approx [simp]: "(\i. approx i) = ID" + assumes finite_deflation_approx: "\i. finite_deflation (approx i)" +begin subsubsection {* Choosing a maximal element from a finite set *} lemma finite_has_maximal: - fixes A :: "'a::po set" + fixes A :: "'a compact_basis set" shows "\finite A; A \ {}\ \ \x\A. \y\A. x \ y \ x = y" proof (induct rule: finite_ne_induct) case (singleton x) @@ -456,43 +422,86 @@ apply (simp add: choose_pos.simps) done -subsubsection {* Rank of basis elements *} +subsubsection {* Properties of approx function *} + +lemma deflation_approx: "deflation (approx i)" +using finite_deflation_approx by (rule finite_deflation_imp_deflation) + +lemma approx_idem: "approx i\(approx i\x) = approx i\x" +using deflation_approx by (rule deflation.idem) + +lemma approx_below: "approx i\x \ x" +using deflation_approx by (rule deflation.below) + +lemma finite_range_approx: "finite (range (\x. approx i\x))" +apply (rule finite_deflation.finite_range) +apply (rule finite_deflation_approx) +done + +lemma compact_approx: "compact (approx n\x)" +apply (rule finite_deflation.compact) +apply (rule finite_deflation_approx) +done + +lemma compact_eq_approx: "compact x \ \i. approx i\x = x" +by (rule admD2, simp_all) + +subsubsection {* Compact basis take function *} primrec - cb_take :: "nat \ 'a compact_basis \ 'a compact_basis" -where + cb_take :: "nat \ 'a compact_basis \ 'a compact_basis" where "cb_take 0 = (\x. compact_bot)" -| "cb_take (Suc n) = compact_take n" +| "cb_take (Suc n) = (\a. Abs_compact_basis (approx n\(Rep_compact_basis a)))" + +declare cb_take.simps [simp del] + +lemma cb_take_zero [simp]: "cb_take 0 a = compact_bot" +by (simp only: cb_take.simps) + +lemma Rep_cb_take: + "Rep_compact_basis (cb_take (Suc n) a) = approx n\(Rep_compact_basis a)" +by (simp add: Abs_compact_basis_inverse cb_take.simps(2) compact_approx) + +lemmas approx_Rep_compact_basis = Rep_cb_take [symmetric] lemma cb_take_covers: "\n. cb_take n x = x" -apply (rule exE [OF compact_basis.take_covers [where a=x]]) -apply (rename_tac n, rule_tac x="Suc n" in exI, simp) +apply (subgoal_tac "\n. cb_take (Suc n) x = x", fast) +apply (simp add: Rep_compact_basis_inject [symmetric]) +apply (simp add: Rep_cb_take) +apply (rule compact_eq_approx) +apply (rule compact_Rep_compact_basis) done lemma cb_take_less: "cb_take n x \ x" -by (cases n, simp, simp add: compact_basis.take_less) +unfolding compact_le_def +by (cases n, simp, simp add: Rep_cb_take approx_below) lemma cb_take_idem: "cb_take n (cb_take n x) = cb_take n x" -by (cases n, simp, simp add: compact_basis.take_take) +unfolding Rep_compact_basis_inject [symmetric] +by (cases n, simp, simp add: Rep_cb_take approx_idem) lemma cb_take_mono: "x \ y \ cb_take n x \ cb_take n y" -by (cases n, simp, simp add: compact_basis.take_mono) +unfolding compact_le_def +by (cases n, simp, simp add: Rep_cb_take monofun_cfun_arg) lemma cb_take_chain_le: "m \ n \ cb_take m x \ cb_take n x" -apply (cases m, simp) -apply (cases n, simp) -apply (simp add: compact_basis.take_chain_le) +unfolding compact_le_def +apply (cases m, simp, cases n, simp) +apply (simp add: Rep_cb_take, rule chain_mono, simp, simp) done -lemma range_const: "range (\x. c) = {c}" -by auto - lemma finite_range_cb_take: "finite (range (cb_take n))" apply (cases n) -apply (simp add: range_const) -apply (simp add: compact_basis.finite_range_take) +apply (subgoal_tac "range (cb_take 0) = {compact_bot}", simp, force) +apply (rule finite_imageD [where f="Rep_compact_basis"]) +apply (rule finite_subset [where B="range (\x. approx (n - 1)\x)"]) +apply (clarsimp simp add: Rep_cb_take) +apply (rule finite_range_approx) +apply (rule inj_onI, simp add: Rep_compact_basis_inject) done +subsubsection {* Rank of basis elements *} + definition rank :: "'a compact_basis \ nat" where @@ -809,22 +818,86 @@ apply (rule ubasis_until_less) done -hide_const (open) - node - choose - choose_pos - place - sub +end + +sublocale approx_chain \ compact_basis!: + ideal_completion below Rep_compact_basis + "approximants :: 'a \ 'a compact_basis set" +proof + fix w :: "'a" + show "below.ideal (approximants w)" + proof (rule below.idealI) + show "\x. x \ approximants w" + unfolding approximants_def + apply (rule_tac x="Abs_compact_basis (approx 0\w)" in exI) + apply (simp add: Abs_compact_basis_inverse approx_below compact_approx) + done + next + fix x y :: "'a compact_basis" + assume "x \ approximants w" "y \ approximants w" + thus "\z \ approximants w. x \ z \ y \ z" + unfolding approximants_def + apply simp + apply (cut_tac a=x in compact_Rep_compact_basis) + apply (cut_tac a=y in compact_Rep_compact_basis) + apply (drule compact_eq_approx) + apply (drule compact_eq_approx) + apply (clarify, rename_tac i j) + apply (rule_tac x="Abs_compact_basis (approx (max i j)\w)" in exI) + apply (simp add: compact_le_def) + apply (simp add: Abs_compact_basis_inverse approx_below compact_approx) + apply (erule subst, erule subst) + apply (simp add: monofun_cfun chain_mono [OF chain_approx]) + done + next + fix x y :: "'a compact_basis" + assume "x \ y" "y \ approximants w" thus "x \ approximants w" + unfolding approximants_def + apply simp + apply (simp add: compact_le_def) + apply (erule (1) below_trans) + done + qed +next + fix Y :: "nat \ 'a" + assume Y: "chain Y" + show "approximants (\i. Y i) = (\i. approximants (Y i))" + unfolding approximants_def + apply safe + apply (simp add: compactD2 [OF compact_Rep_compact_basis Y]) + apply (erule below_trans, rule is_ub_thelub [OF Y]) + done +next + fix a :: "'a compact_basis" + show "approximants (Rep_compact_basis a) = {b. b \ a}" + unfolding approximants_def compact_le_def .. +next + fix x y :: "'a" + assume "approximants x \ approximants y" thus "x \ y" + apply (subgoal_tac "(\i. approx i\x) \ y") + apply (simp add: lub_distribs) + apply (rule admD, simp, simp) + apply (drule_tac c="Abs_compact_basis (approx i\x)" in subsetD) + apply (simp add: approximants_def Abs_compact_basis_inverse + approx_below compact_approx) + apply (simp add: approximants_def Abs_compact_basis_inverse compact_approx) + done +next + show "\f::'a compact_basis \ nat. inj f" + by (rule exI, rule inj_place) +qed subsubsection {* EP-pair from any bifinite domain into \emph{udom} *} +context approx_chain begin + definition - udom_emb :: "'a::bifinite \ udom" + udom_emb :: "'a \ udom" where "udom_emb = compact_basis.basis_fun (\x. udom_principal (basis_emb x))" definition - udom_prj :: "udom \ 'a::bifinite" + udom_prj :: "udom \ 'a" where "udom_prj = udom.basis_fun (\x. Rep_compact_basis (basis_prj x))" @@ -855,3 +928,103 @@ done end + +abbreviation "udom_emb \ approx_chain.udom_emb" +abbreviation "udom_prj \ approx_chain.udom_prj" + +lemmas ep_pair_udom = approx_chain.ep_pair_udom + +subsection {* Chain of approx functions for type \emph{udom} *} + +definition + udom_approx :: "nat \ udom \ udom" +where + "udom_approx i = + udom.basis_fun (\x. udom_principal (ubasis_until (\y. y \ i) x))" + +lemma udom_approx_mono: + "ubasis_le a b \ + udom_principal (ubasis_until (\y. y \ i) a) \ + udom_principal (ubasis_until (\y. y \ i) b)" +apply (rule udom.principal_mono) +apply (rule ubasis_until_mono) +apply (frule (2) order_less_le_trans [OF node_gt2]) +apply (erule order_less_imp_le) +apply assumption +done + +lemma adm_mem_finite: "\cont f; finite S\ \ adm (\x. f x \ S)" +by (erule adm_subst, induct set: finite, simp_all) + +lemma udom_approx_principal: + "udom_approx i\(udom_principal x) = + udom_principal (ubasis_until (\y. y \ i) x)" +unfolding udom_approx_def +apply (rule udom.basis_fun_principal) +apply (erule udom_approx_mono) +done + +lemma finite_deflation_udom_approx: "finite_deflation (udom_approx i)" +proof + fix x show "udom_approx i\(udom_approx i\x) = udom_approx i\x" + by (induct x rule: udom.principal_induct, simp) + (simp add: udom_approx_principal ubasis_until_idem) +next + fix x show "udom_approx i\x \ x" + by (induct x rule: udom.principal_induct, simp) + (simp add: udom_approx_principal ubasis_until_less) +next + have *: "finite (range (\x. udom_principal (ubasis_until (\y. y \ i) x)))" + apply (subst range_composition [where f=udom_principal]) + apply (simp add: finite_range_ubasis_until) + done + show "finite {x. udom_approx i\x = x}" + apply (rule finite_range_imp_finite_fixes) + apply (rule rev_finite_subset [OF *]) + apply (clarsimp, rename_tac x) + apply (induct_tac x rule: udom.principal_induct) + apply (simp add: adm_mem_finite *) + apply (simp add: udom_approx_principal) + done +qed + +interpretation udom_approx: finite_deflation "udom_approx i" +by (rule finite_deflation_udom_approx) + +lemma chain_udom_approx [simp]: "chain (\i. udom_approx i)" +unfolding udom_approx_def +apply (rule chainI) +apply (rule udom.basis_fun_mono) +apply (erule udom_approx_mono) +apply (erule udom_approx_mono) +apply (rule udom.principal_mono) +apply (rule ubasis_until_chain, simp) +done + +lemma lub_udom_approx [simp]: "(\i. udom_approx i) = ID" +apply (rule ext_cfun, simp add: contlub_cfun_fun) +apply (rule below_antisym) +apply (rule is_lub_thelub) +apply (simp) +apply (rule ub_rangeI) +apply (rule udom_approx.below) +apply (rule_tac x=x in udom.principal_induct) +apply (simp add: lub_distribs) +apply (rule rev_below_trans) +apply (rule_tac x=a in is_ub_thelub) +apply simp +apply (simp add: udom_approx_principal) +apply (simp add: ubasis_until_same ubasis_le_refl) +done + +lemma udom_approx: "approx_chain udom_approx" +proof + show "chain (\i. udom_approx i)" + by (rule chain_udom_approx) + show "(\i. udom_approx i) = ID" + by (rule lub_udom_approx) +qed + +hide_const (open) node + +end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/Up.thy --- a/src/HOLCF/Up.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/Up.thy Wed Oct 06 10:49:27 2010 -0700 @@ -5,7 +5,7 @@ header {* The type of lifted values *} theory Up -imports Bifinite +imports Algebraic begin default_sort cpo @@ -332,35 +332,62 @@ by (rule finite_subset, simp add: d.finite_fixes) qed -subsection {* Lifted cpo is a bifinite domain *} +subsection {* Lifted cpo is an SFP domain *} + +definition u_approx :: "nat \ udom\<^sub>\ \ udom\<^sub>\" +where "u_approx = (\i. u_map\(udom_approx i))" -instantiation u :: (profinite) bifinite +lemma u_approx: "approx_chain u_approx" +proof (rule approx_chain.intro) + show "chain (\i. u_approx i)" + unfolding u_approx_def by simp + show "(\i. u_approx i) = ID" + unfolding u_approx_def + by (simp add: lub_distribs u_map_ID) + show "\i. finite_deflation (u_approx i)" + unfolding u_approx_def + by (intro finite_deflation_u_map finite_deflation_udom_approx) +qed + +definition u_sfp :: "sfp \ sfp" +where "u_sfp = sfp_fun1 u_approx u_map" + +lemma cast_u_sfp: + "cast\(u_sfp\A) = + udom_emb u_approx oo u_map\(cast\A) oo udom_prj u_approx" +unfolding u_sfp_def +apply (rule cast_sfp_fun1 [OF u_approx]) +apply (erule finite_deflation_u_map) +done + +instantiation u :: (sfp) sfp begin definition - approx_up_def: - "approx = (\n. u_map\(approx n))" + "emb = udom_emb u_approx oo u_map\emb" + +definition + "prj = u_map\prj oo udom_prj u_approx" + +definition + "sfp (t::'a u itself) = u_sfp\SFP('a)" instance proof - fix i :: nat and x :: "'a u" - show "chain (approx :: nat \ 'a u \ 'a u)" - unfolding approx_up_def by simp - show "(\i. approx i\x) = x" - unfolding approx_up_def - by (induct x, simp, simp add: lub_distribs) - show "approx i\(approx i\x) = approx i\x" - unfolding approx_up_def - by (induct x) simp_all - show "finite {x::'a u. approx i\x = x}" - unfolding approx_up_def - by (intro finite_deflation.finite_fixes - finite_deflation_u_map - finite_deflation_approx) + show "ep_pair emb (prj :: udom \ 'a u)" + unfolding emb_u_def prj_u_def + using ep_pair_udom [OF u_approx] + by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj) +next + show "cast\SFP('a u) = emb oo (prj :: udom \ 'a u)" + unfolding emb_u_def prj_u_def sfp_u_def cast_u_sfp + by (simp add: cast_SFP oo_def expand_cfun_eq u_map_map) qed end -lemma approx_up [simp]: "approx i\(up\x) = up\(approx i\x)" -unfolding approx_up_def by simp +text {* SFP of type constructor = type combinator *} + +lemma SFP_u: "SFP('a::sfp u) = u_sfp\SFP('a)" +by (rule sfp_u_def) end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/UpperPD.thy --- a/src/HOLCF/UpperPD.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/UpperPD.thy Wed Oct 06 10:49:27 2010 -0700 @@ -69,27 +69,6 @@ apply (simp add: upper_le_PDPlus_iff 3) done -lemma pd_take_upper_chain: - "pd_take n t \\ pd_take (Suc n) t" -apply (induct t rule: pd_basis_induct) -apply (simp add: compact_basis.take_chain) -apply (simp add: PDPlus_upper_mono) -done - -lemma pd_take_upper_le: "pd_take i t \\ t" -apply (induct t rule: pd_basis_induct) -apply (simp add: compact_basis.take_less) -apply (simp add: PDPlus_upper_mono) -done - -lemma pd_take_upper_mono: - "t \\ u \ pd_take n t \\ pd_take n u" -apply (erule upper_le_induct) -apply (simp add: compact_basis.take_mono) -apply (simp add: upper_le_PDPlus_PDUnit_iff) -apply (simp add: upper_le_PDPlus_iff) -done - subsection {* Type definition *} @@ -97,7 +76,7 @@ "{S::'a pd_basis set. upper_le.ideal S}" by (fast intro: upper_le.ideal_principal) -instantiation upper_pd :: (profinite) below +instantiation upper_pd :: (sfp) below begin definition @@ -106,18 +85,18 @@ instance .. end -instance upper_pd :: (profinite) po -by (rule upper_le.typedef_ideal_po - [OF type_definition_upper_pd below_upper_pd_def]) +instance upper_pd :: (sfp) po +using type_definition_upper_pd below_upper_pd_def +by (rule upper_le.typedef_ideal_po) -instance upper_pd :: (profinite) cpo -by (rule upper_le.typedef_ideal_cpo - [OF type_definition_upper_pd below_upper_pd_def]) +instance upper_pd :: (sfp) cpo +using type_definition_upper_pd below_upper_pd_def +by (rule upper_le.typedef_ideal_cpo) lemma Rep_upper_pd_lub: "chain Y \ Rep_upper_pd (\i. Y i) = (\i. Rep_upper_pd (Y i))" -by (rule upper_le.typedef_ideal_rep_contlub - [OF type_definition_upper_pd below_upper_pd_def]) +using type_definition_upper_pd below_upper_pd_def +by (rule upper_le.typedef_ideal_rep_contlub) lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd xs)" by (rule Rep_upper_pd [unfolded mem_Collect_eq]) @@ -132,18 +111,13 @@ by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal) interpretation upper_pd: - ideal_completion upper_le pd_take upper_principal Rep_upper_pd + ideal_completion upper_le upper_principal Rep_upper_pd apply unfold_locales -apply (rule pd_take_upper_le) -apply (rule pd_take_idem) -apply (erule pd_take_upper_mono) -apply (rule pd_take_upper_chain) -apply (rule finite_range_pd_take) -apply (rule pd_take_covers) apply (rule ideal_Rep_upper_pd) apply (erule Rep_upper_pd_lub) apply (rule Rep_upper_principal) apply (simp only: below_upper_pd_def) +apply (rule pd_basis_countable) done text {* Upper powerdomain is pointed *} @@ -151,42 +125,12 @@ lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \ ys" by (induct ys rule: upper_pd.principal_induct, simp, simp) -instance upper_pd :: (bifinite) pcpo +instance upper_pd :: (sfp) pcpo by intro_classes (fast intro: upper_pd_minimal) lemma inst_upper_pd_pcpo: "\ = upper_principal (PDUnit compact_bot)" by (rule upper_pd_minimal [THEN UU_I, symmetric]) -text {* Upper powerdomain is profinite *} - -instantiation upper_pd :: (profinite) profinite -begin - -definition - approx_upper_pd_def: "approx = upper_pd.completion_approx" - -instance -apply (intro_classes, unfold approx_upper_pd_def) -apply (rule upper_pd.chain_completion_approx) -apply (rule upper_pd.lub_completion_approx) -apply (rule upper_pd.completion_approx_idem) -apply (rule upper_pd.finite_fixes_completion_approx) -done - -end - -instance upper_pd :: (bifinite) bifinite .. - -lemma approx_upper_principal [simp]: - "approx n\(upper_principal t) = upper_principal (pd_take n t)" -unfolding approx_upper_pd_def -by (rule upper_pd.completion_approx_principal) - -lemma approx_eq_upper_principal: - "\t\Rep_upper_pd xs. approx n\xs = upper_principal (pd_take n t)" -unfolding approx_upper_pd_def -by (rule upper_pd.completion_approx_eq_principal) - subsection {* Monadic unit and plus *} @@ -222,16 +166,6 @@ by (simp add: upper_pd.basis_fun_principal upper_pd.basis_fun_mono PDPlus_upper_mono) -lemma approx_upper_unit [simp]: - "approx n\{x}\ = {approx n\x}\" -apply (induct x rule: compact_basis.principal_induct, simp) -apply (simp add: approx_Rep_compact_basis) -done - -lemma approx_upper_plus [simp]: - "approx n\(xs +\ ys) = (approx n\xs) +\ (approx n\ys)" -by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp) - interpretation upper_add: semilattice upper_add proof fix xs ys zs :: "'a upper_pd" show "(xs +\ ys) +\ zs = xs +\ (ys +\ zs)" @@ -307,7 +241,8 @@ unfolding po_eq_conv by simp lemma upper_unit_strict [simp]: "{\}\ = \" -unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp +using upper_unit_Rep_compact_basis [of compact_bot] +by (simp add: inst_upper_pd_pcpo) lemma upper_plus_strict1 [simp]: "\ +\ ys = \" by (rule UU_I, rule upper_plus_below1) @@ -328,8 +263,14 @@ apply auto done +lemma compact_upper_unit: "compact x \ compact {x}\" +by (auto dest!: compact_basis.compact_imp_principal) + lemma compact_upper_unit_iff [simp]: "compact {x}\ \ compact x" -unfolding profinite_compact_iff by simp +apply (safe elim!: compact_upper_unit) +apply (simp only: compact_def upper_unit_below_iff [symmetric]) +apply (erule adm_subst [OF cont_Rep_CFun2]) +done lemma compact_upper_plus [simp]: "\compact xs; compact ys\ \ compact (xs +\ ys)" @@ -424,16 +365,12 @@ unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit) -subsection {* Map and join *} +subsection {* Map *} definition upper_map :: "('a \ 'b) \ 'a upper_pd \ 'b upper_pd" where "upper_map = (\ f xs. upper_bind\xs\(\ x. {f\x}\))" -definition - upper_join :: "'a upper_pd upper_pd \ 'a upper_pd" where - "upper_join = (\ xss. upper_bind\xss\(\ xs. xs))" - lemma upper_map_unit [simp]: "upper_map\f\{x}\ = {f\x}\" unfolding upper_map_def by simp @@ -442,14 +379,6 @@ "upper_map\f\(xs +\ ys) = upper_map\f\xs +\ upper_map\f\ys" unfolding upper_map_def by simp -lemma upper_join_unit [simp]: - "upper_join\{xs}\ = xs" -unfolding upper_join_def by simp - -lemma upper_join_plus [simp]: - "upper_join\(xss +\ yss) = upper_join\xss +\ upper_join\yss" -unfolding upper_join_def by simp - lemma upper_map_ident: "upper_map\(\ x. x)\xs = xs" by (induct xs rule: upper_pd_induct, simp_all) @@ -460,22 +389,6 @@ "upper_map\f\(upper_map\g\xs) = upper_map\(\ x. f\(g\x))\xs" by (induct xs rule: upper_pd_induct, simp_all) -lemma upper_join_map_unit: - "upper_join\(upper_map\upper_unit\xs) = xs" -by (induct xs rule: upper_pd_induct, simp_all) - -lemma upper_join_map_join: - "upper_join\(upper_map\upper_join\xsss) = upper_join\(upper_join\xsss)" -by (induct xsss rule: upper_pd_induct, simp_all) - -lemma upper_join_map_map: - "upper_join\(upper_map\(upper_map\f)\xss) = - upper_map\f\(upper_join\xss)" -by (induct xss rule: upper_pd_induct, simp_all) - -lemma upper_map_approx: "upper_map\(approx n)\xs = approx n\xs" -by (induct xs rule: upper_pd_induct, simp_all) - lemma ep_pair_upper_map: "ep_pair e p \ ep_pair (upper_map\e) (upper_map\p)" apply default apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse) @@ -490,4 +403,134 @@ apply (simp_all add: deflation.below monofun_cfun) done +(* FIXME: long proof! *) +lemma finite_deflation_upper_map: + assumes "finite_deflation d" shows "finite_deflation (upper_map\d)" +proof (rule finite_deflation_intro) + interpret d: finite_deflation d by fact + have "deflation d" by fact + thus "deflation (upper_map\d)" by (rule deflation_upper_map) + have "finite (range (\x. d\x))" by (rule d.finite_range) + hence "finite (Rep_compact_basis -` range (\x. d\x))" + by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) + hence "finite (Pow (Rep_compact_basis -` range (\x. d\x)))" by simp + hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" + by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) + hence *: "finite (upper_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\x. d\x))))" by simp + hence "finite (range (\xs. upper_map\d\xs))" + apply (rule rev_finite_subset) + apply clarsimp + apply (induct_tac xs rule: upper_pd.principal_induct) + apply (simp add: adm_mem_finite *) + apply (rename_tac t, induct_tac t rule: pd_basis_induct) + apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit) + apply simp + apply (subgoal_tac "\b. d\(Rep_compact_basis a) = Rep_compact_basis b") + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDUnit) + apply (rule range_eqI) + apply (erule sym) + apply (rule exI) + apply (rule Abs_compact_basis_inverse [symmetric]) + apply (simp add: d.compact) + apply (simp only: upper_plus_principal [symmetric] upper_map_plus) + apply clarsimp + apply (rule imageI) + apply (rule vimageI2) + apply (simp add: Rep_PDPlus) + done + thus "finite {xs. upper_map\d\xs = xs}" + by (rule finite_range_imp_finite_fixes) +qed + +subsection {* Upper powerdomain is an SFP domain *} + +definition + upper_approx :: "nat \ udom upper_pd \ udom upper_pd" +where + "upper_approx = (\i. upper_map\(udom_approx i))" + +lemma upper_approx: "approx_chain upper_approx" +proof (rule approx_chain.intro) + show "chain (\i. upper_approx i)" + unfolding upper_approx_def by simp + show "(\i. upper_approx i) = ID" + unfolding upper_approx_def + by (simp add: lub_distribs upper_map_ID) + show "\i. finite_deflation (upper_approx i)" + unfolding upper_approx_def + by (intro finite_deflation_upper_map finite_deflation_udom_approx) +qed + +definition upper_sfp :: "sfp \ sfp" +where "upper_sfp = sfp_fun1 upper_approx upper_map" + +lemma cast_upper_sfp: + "cast\(upper_sfp\A) = + udom_emb upper_approx oo upper_map\(cast\A) oo udom_prj upper_approx" +unfolding upper_sfp_def +apply (rule cast_sfp_fun1 [OF upper_approx]) +apply (erule finite_deflation_upper_map) +done + +instantiation upper_pd :: (sfp) sfp +begin + +definition + "emb = udom_emb upper_approx oo upper_map\emb" + +definition + "prj = upper_map\prj oo udom_prj upper_approx" + +definition + "sfp (t::'a upper_pd itself) = upper_sfp\SFP('a)" + +instance proof + show "ep_pair emb (prj :: udom \ 'a upper_pd)" + unfolding emb_upper_pd_def prj_upper_pd_def + using ep_pair_udom [OF upper_approx] + by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj) +next + show "cast\SFP('a upper_pd) = emb oo (prj :: udom \ 'a upper_pd)" + unfolding emb_upper_pd_def prj_upper_pd_def sfp_upper_pd_def cast_upper_sfp + by (simp add: cast_SFP oo_def expand_cfun_eq upper_map_map) +qed + end + +text {* SFP of type constructor = type combinator *} + +lemma SFP_upper: "SFP('a upper_pd) = upper_sfp\SFP('a)" +by (rule sfp_upper_pd_def) + + +subsection {* Join *} + +definition + upper_join :: "'a upper_pd upper_pd \ 'a upper_pd" where + "upper_join = (\ xss. upper_bind\xss\(\ xs. xs))" + +lemma upper_join_unit [simp]: + "upper_join\{xs}\ = xs" +unfolding upper_join_def by simp + +lemma upper_join_plus [simp]: + "upper_join\(xss +\ yss) = upper_join\xss +\ upper_join\yss" +unfolding upper_join_def by simp + +lemma upper_join_map_unit: + "upper_join\(upper_map\upper_unit\xs) = xs" +by (induct xs rule: upper_pd_induct, simp_all) + +lemma upper_join_map_join: + "upper_join\(upper_map\upper_join\xsss) = upper_join\(upper_join\xsss)" +by (induct xsss rule: upper_pd_induct, simp_all) + +lemma upper_join_map_map: + "upper_join\(upper_map\(upper_map\f)\xss) = + upper_map\f\(upper_join\xss)" +by (induct xss rule: upper_pd_induct, simp_all) + +end diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/ex/Domain_Proofs.thy --- a/src/HOLCF/ex/Domain_Proofs.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/ex/Domain_Proofs.thy Wed Oct 06 10:49:27 2010 -0700 @@ -8,7 +8,7 @@ imports HOLCF begin -default_sort rep +default_sort sfp (* @@ -28,50 +28,50 @@ text {* Start with the one-step non-recursive version *} definition - foo_bar_baz_deflF :: - "TypeRep \ TypeRep \ TypeRep \ TypeRep \ TypeRep \ TypeRep \ TypeRep" + foo_bar_baz_sfpF :: + "sfp \ sfp \ sfp \ sfp \ sfp \ sfp \ sfp" where - "foo_bar_baz_deflF = (\ a. Abs_CFun (\(t1, t2, t3). - ( ssum_defl\REP(one)\(sprod_defl\(u_defl\a)\(u_defl\t2)) - , u_defl\(cfun_defl\t3\REP(tr)) - , u_defl\(cfun_defl\(convex_defl\t1)\REP(tr)))))" + "foo_bar_baz_sfpF = (\ a. Abs_CFun (\(t1, t2, t3). + ( ssum_sfp\SFP(one)\(sprod_sfp\(u_sfp\a)\(u_sfp\t2)) + , u_sfp\(cfun_sfp\t3\SFP(tr)) + , u_sfp\(cfun_sfp\(convex_sfp\t1)\SFP(tr)))))" -lemma foo_bar_baz_deflF_beta: - "foo_bar_baz_deflF\a\t = - ( ssum_defl\REP(one)\(sprod_defl\(u_defl\a)\(u_defl\(fst (snd t)))) - , u_defl\(cfun_defl\(snd (snd t))\REP(tr)) - , u_defl\(cfun_defl\(convex_defl\(fst t))\REP(tr)))" -unfolding foo_bar_baz_deflF_def +lemma foo_bar_baz_sfpF_beta: + "foo_bar_baz_sfpF\a\t = + ( ssum_sfp\SFP(one)\(sprod_sfp\(u_sfp\a)\(u_sfp\(fst (snd t)))) + , u_sfp\(cfun_sfp\(snd (snd t))\SFP(tr)) + , u_sfp\(cfun_sfp\(convex_sfp\(fst t))\SFP(tr)))" +unfolding foo_bar_baz_sfpF_def by (simp add: split_def) text {* Individual type combinators are projected from the fixed point. *} -definition foo_defl :: "TypeRep \ TypeRep" -where "foo_defl = (\ a. fst (fix\(foo_bar_baz_deflF\a)))" +definition foo_sfp :: "sfp \ sfp" +where "foo_sfp = (\ a. fst (fix\(foo_bar_baz_sfpF\a)))" -definition bar_defl :: "TypeRep \ TypeRep" -where "bar_defl = (\ a. fst (snd (fix\(foo_bar_baz_deflF\a))))" +definition bar_sfp :: "sfp \ sfp" +where "bar_sfp = (\ a. fst (snd (fix\(foo_bar_baz_sfpF\a))))" -definition baz_defl :: "TypeRep \ TypeRep" -where "baz_defl = (\ a. snd (snd (fix\(foo_bar_baz_deflF\a))))" +definition baz_sfp :: "sfp \ sfp" +where "baz_sfp = (\ a. snd (snd (fix\(foo_bar_baz_sfpF\a))))" lemma defl_apply_thms: - "foo_defl\a = fst (fix\(foo_bar_baz_deflF\a))" - "bar_defl\a = fst (snd (fix\(foo_bar_baz_deflF\a)))" - "baz_defl\a = snd (snd (fix\(foo_bar_baz_deflF\a)))" -unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all + "foo_sfp\a = fst (fix\(foo_bar_baz_sfpF\a))" + "bar_sfp\a = fst (snd (fix\(foo_bar_baz_sfpF\a)))" + "baz_sfp\a = snd (snd (fix\(foo_bar_baz_sfpF\a)))" +unfolding foo_sfp_def bar_sfp_def baz_sfp_def by simp_all text {* Unfold rules for each combinator. *} -lemma foo_defl_unfold: - "foo_defl\a = ssum_defl\REP(one)\(sprod_defl\(u_defl\a)\(u_defl\(bar_defl\a)))" -unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) +lemma foo_sfp_unfold: + "foo_sfp\a = ssum_sfp\SFP(one)\(sprod_sfp\(u_sfp\a)\(u_sfp\(bar_sfp\a)))" +unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta) -lemma bar_defl_unfold: "bar_defl\a = u_defl\(cfun_defl\(baz_defl\a)\REP(tr))" -unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) +lemma bar_sfp_unfold: "bar_sfp\a = u_sfp\(cfun_sfp\(baz_sfp\a)\SFP(tr))" +unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta) -lemma baz_defl_unfold: "baz_defl\a = u_defl\(cfun_defl\(convex_defl\(foo_defl\a))\REP(tr))" -unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) +lemma baz_sfp_unfold: "baz_sfp\a = u_sfp\(cfun_sfp\(convex_sfp\(foo_sfp\a))\SFP(tr))" +unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta) text "The automation for the previous steps will be quite similar to how the fixrec package works." @@ -82,28 +82,28 @@ text {* Use @{text pcpodef} with the appropriate type combinator. *} -pcpodef (open) 'a foo = "{x. x ::: foo_defl\REP('a)}" -by (simp_all add: adm_in_deflation) +pcpodef (open) 'a foo = "{x. x ::: foo_sfp\SFP('a)}" +by (simp_all add: adm_in_sfp) -pcpodef (open) 'a bar = "{x. x ::: bar_defl\REP('a)}" -by (simp_all add: adm_in_deflation) +pcpodef (open) 'a bar = "{x. x ::: bar_sfp\SFP('a)}" +by (simp_all add: adm_in_sfp) -pcpodef (open) 'a baz = "{x. x ::: baz_defl\REP('a)}" -by (simp_all add: adm_in_deflation) +pcpodef (open) 'a baz = "{x. x ::: baz_sfp\SFP('a)}" +by (simp_all add: adm_in_sfp) text {* Prove rep instance using lemma @{text typedef_rep_class}. *} -instantiation foo :: (rep) rep +instantiation foo :: (sfp) sfp begin definition emb_foo :: "'a foo \ udom" where "emb_foo \ (\ x. Rep_foo x)" definition prj_foo :: "udom \ 'a foo" -where "prj_foo \ (\ y. Abs_foo (cast\(foo_defl\REP('a))\y))" +where "prj_foo \ (\ y. Abs_foo (cast\(foo_sfp\SFP('a))\y))" -definition approx_foo :: "nat \ 'a foo \ 'a foo" -where "approx_foo \ repdef_approx Rep_foo Abs_foo (foo_defl\REP('a))" +definition sfp_foo :: "'a foo itself \ sfp" +where "sfp_foo \ \a. foo_sfp\SFP('a)" instance apply (rule typedef_rep_class) @@ -111,22 +111,22 @@ apply (rule below_foo_def) apply (rule emb_foo_def) apply (rule prj_foo_def) -apply (rule approx_foo_def) +apply (rule sfp_foo_def) done end -instantiation bar :: (rep) rep +instantiation bar :: (sfp) sfp begin definition emb_bar :: "'a bar \ udom" where "emb_bar \ (\ x. Rep_bar x)" definition prj_bar :: "udom \ 'a bar" -where "prj_bar \ (\ y. Abs_bar (cast\(bar_defl\REP('a))\y))" +where "prj_bar \ (\ y. Abs_bar (cast\(bar_sfp\SFP('a))\y))" -definition approx_bar :: "nat \ 'a bar \ 'a bar" -where "approx_bar \ repdef_approx Rep_bar Abs_bar (bar_defl\REP('a))" +definition sfp_bar :: "'a bar itself \ sfp" +where "sfp_bar \ \a. bar_sfp\SFP('a)" instance apply (rule typedef_rep_class) @@ -134,22 +134,22 @@ apply (rule below_bar_def) apply (rule emb_bar_def) apply (rule prj_bar_def) -apply (rule approx_bar_def) +apply (rule sfp_bar_def) done end -instantiation baz :: (rep) rep +instantiation baz :: (sfp) sfp begin definition emb_baz :: "'a baz \ udom" where "emb_baz \ (\ x. Rep_baz x)" definition prj_baz :: "udom \ 'a baz" -where "prj_baz \ (\ y. Abs_baz (cast\(baz_defl\REP('a))\y))" +where "prj_baz \ (\ y. Abs_baz (cast\(baz_sfp\SFP('a))\y))" -definition approx_baz :: "nat \ 'a baz \ 'a baz" -where "approx_baz \ repdef_approx Rep_baz Abs_baz (baz_defl\REP('a))" +definition sfp_baz :: "'a baz itself \ sfp" +where "sfp_baz \ \a. baz_sfp\SFP('a)" instance apply (rule typedef_rep_class) @@ -157,50 +157,44 @@ apply (rule below_baz_def) apply (rule emb_baz_def) apply (rule prj_baz_def) -apply (rule approx_baz_def) +apply (rule sfp_baz_def) done end -text {* Prove REP rules using lemma @{text typedef_REP}. *} +text {* Prove SFP rules using lemma @{text typedef_SFP}. *} -lemma REP_foo: "REP('a foo) = foo_defl\REP('a)" -apply (rule typedef_REP) -apply (rule type_definition_foo) -apply (rule below_foo_def) -apply (rule emb_foo_def) -apply (rule prj_foo_def) +lemma SFP_foo: "SFP('a foo) = foo_sfp\SFP('a)" +apply (rule typedef_SFP) +apply (rule sfp_foo_def) done -lemma REP_bar: "REP('a bar) = bar_defl\REP('a)" -apply (rule typedef_REP) -apply (rule type_definition_bar) -apply (rule below_bar_def) -apply (rule emb_bar_def) -apply (rule prj_bar_def) +lemma SFP_bar: "SFP('a bar) = bar_sfp\SFP('a)" +apply (rule typedef_SFP) +apply (rule sfp_bar_def) +done + +lemma SFP_baz: "SFP('a baz) = baz_sfp\SFP('a)" +apply (rule typedef_SFP) +apply (rule sfp_baz_def) done -lemma REP_baz: "REP('a baz) = baz_defl\REP('a)" -apply (rule typedef_REP) -apply (rule type_definition_baz) -apply (rule below_baz_def) -apply (rule emb_baz_def) -apply (rule prj_baz_def) -done +text {* Prove SFP equations using type combinator unfold lemmas. *} -text {* Prove REP equations using type combinator unfold lemmas. *} +lemmas SFP_simps = + SFP_ssum SFP_sprod SFP_u SFP_cfun -lemma REP_foo': "REP('a foo) = REP(one \ 'a\<^sub>\ \ ('a bar)\<^sub>\)" -unfolding REP_foo REP_bar REP_baz REP_simps -by (rule foo_defl_unfold) +lemma SFP_foo': "SFP('a foo) = SFP(one \ 'a\<^sub>\ \ ('a bar)\<^sub>\)" +unfolding SFP_foo SFP_bar SFP_baz SFP_simps +by (rule foo_sfp_unfold) -lemma REP_bar': "REP('a bar) = REP(('a baz \ tr)\<^sub>\)" -unfolding REP_foo REP_bar REP_baz REP_simps -by (rule bar_defl_unfold) +lemma SFP_bar': "SFP('a bar) = SFP(('a baz \ tr)\<^sub>\)" +unfolding SFP_foo SFP_bar SFP_baz SFP_simps +by (rule bar_sfp_unfold) -lemma REP_baz': "REP('a baz) = REP(('a foo convex_pd \ tr)\<^sub>\)" -unfolding REP_foo REP_bar REP_baz REP_simps REP_convex -by (rule baz_defl_unfold) +lemma SFP_baz': "SFP('a baz) = SFP(('a foo convex_pd \ tr)\<^sub>\)" +unfolding SFP_foo SFP_bar SFP_baz SFP_simps SFP_convex +by (rule baz_sfp_unfold) (********************************************************************) @@ -229,36 +223,36 @@ text {* Prove isomorphism rules. *} lemma foo_abs_iso: "foo_rep\(foo_abs\x) = x" -by (rule domain_abs_iso [OF REP_foo' foo_abs_def foo_rep_def]) +by (rule domain_abs_iso [OF SFP_foo' foo_abs_def foo_rep_def]) lemma foo_rep_iso: "foo_abs\(foo_rep\x) = x" -by (rule domain_rep_iso [OF REP_foo' foo_abs_def foo_rep_def]) +by (rule domain_rep_iso [OF SFP_foo' foo_abs_def foo_rep_def]) lemma bar_abs_iso: "bar_rep\(bar_abs\x) = x" -by (rule domain_abs_iso [OF REP_bar' bar_abs_def bar_rep_def]) +by (rule domain_abs_iso [OF SFP_bar' bar_abs_def bar_rep_def]) lemma bar_rep_iso: "bar_abs\(bar_rep\x) = x" -by (rule domain_rep_iso [OF REP_bar' bar_abs_def bar_rep_def]) +by (rule domain_rep_iso [OF SFP_bar' bar_abs_def bar_rep_def]) lemma baz_abs_iso: "baz_rep\(baz_abs\x) = x" -by (rule domain_abs_iso [OF REP_baz' baz_abs_def baz_rep_def]) +by (rule domain_abs_iso [OF SFP_baz' baz_abs_def baz_rep_def]) lemma baz_rep_iso: "baz_abs\(baz_rep\x) = x" -by (rule domain_rep_iso [OF REP_baz' baz_abs_def baz_rep_def]) +by (rule domain_rep_iso [OF SFP_baz' baz_abs_def baz_rep_def]) text {* Prove isodefl rules using @{text isodefl_coerce}. *} lemma isodefl_foo_abs: "isodefl d t \ isodefl (foo_abs oo d oo foo_rep) t" -by (rule isodefl_abs_rep [OF REP_foo' foo_abs_def foo_rep_def]) +by (rule isodefl_abs_rep [OF SFP_foo' foo_abs_def foo_rep_def]) lemma isodefl_bar_abs: "isodefl d t \ isodefl (bar_abs oo d oo bar_rep) t" -by (rule isodefl_abs_rep [OF REP_bar' bar_abs_def bar_rep_def]) +by (rule isodefl_abs_rep [OF SFP_bar' bar_abs_def bar_rep_def]) lemma isodefl_baz_abs: "isodefl d t \ isodefl (baz_abs oo d oo baz_rep) t" -by (rule isodefl_abs_rep [OF REP_baz' baz_abs_def baz_rep_def]) +by (rule isodefl_abs_rep [OF SFP_baz' baz_abs_def baz_rep_def]) (********************************************************************) @@ -322,15 +316,15 @@ lemma isodefl_foo_bar_baz: assumes isodefl_d: "isodefl d t" shows - "isodefl (foo_map\d) (foo_defl\t) \ - isodefl (bar_map\d) (bar_defl\t) \ - isodefl (baz_map\d) (baz_defl\t)" + "isodefl (foo_map\d) (foo_sfp\t) \ + isodefl (bar_map\d) (bar_sfp\t) \ + isodefl (baz_map\d) (baz_sfp\t)" unfolding map_apply_thms defl_apply_thms apply (rule parallel_fix_ind) apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id) apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms) apply (simp only: foo_bar_baz_mapF_beta - foo_bar_baz_deflF_beta + foo_bar_baz_sfpF_beta fst_conv snd_conv) apply (elim conjE) apply (intro @@ -338,7 +332,7 @@ isodefl_foo_abs isodefl_bar_abs isodefl_baz_abs - isodefl_ssum isodefl_sprod isodefl_ID_REP + isodefl_ssum isodefl_sprod isodefl_ID_SFP isodefl_u isodefl_convex isodefl_cfun isodefl_d ) @@ -349,27 +343,27 @@ lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1] lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2] -text {* Prove map ID lemmas, using isodefl_REP_imp_ID *} +text {* Prove map ID lemmas, using isodefl_SFP_imp_ID *} lemma foo_map_ID: "foo_map\ID = ID" -apply (rule isodefl_REP_imp_ID) -apply (subst REP_foo) +apply (rule isodefl_SFP_imp_ID) +apply (subst SFP_foo) apply (rule isodefl_foo) -apply (rule isodefl_ID_REP) +apply (rule isodefl_ID_SFP) done lemma bar_map_ID: "bar_map\ID = ID" -apply (rule isodefl_REP_imp_ID) -apply (subst REP_bar) +apply (rule isodefl_SFP_imp_ID) +apply (subst SFP_bar) apply (rule isodefl_bar) -apply (rule isodefl_ID_REP) +apply (rule isodefl_ID_SFP) done lemma baz_map_ID: "baz_map\ID = ID" -apply (rule isodefl_REP_imp_ID) -apply (subst REP_baz) +apply (rule isodefl_SFP_imp_ID) +apply (subst SFP_baz) apply (rule isodefl_baz) -apply (rule isodefl_ID_REP) +apply (rule isodefl_ID_SFP) done (********************************************************************) diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/ex/Powerdomain_ex.thy --- a/src/HOLCF/ex/Powerdomain_ex.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/ex/Powerdomain_ex.thy Wed Oct 06 10:49:27 2010 -0700 @@ -8,7 +8,7 @@ imports HOLCF begin -default_sort bifinite +default_sort sfp subsection {* Monadic sorting example *}