# HG changeset patch # User huffman # Date 1267397742 28800 # Node ID c4d3d65856ddf17c2e6c82744d0fa7372bd3b96a # Parent c23b42730b9b1853d052716f1a8e50933e3efecb move some powerdomain stuff into a new file diff -r c23b42730b9b -r c4d3d65856dd src/HOLCF/HOLCF.thy --- a/src/HOLCF/HOLCF.thy Sun Feb 28 14:05:21 2010 -0800 +++ b/src/HOLCF/HOLCF.thy Sun Feb 28 14:55:42 2010 -0800 @@ -6,8 +6,10 @@ theory HOLCF imports - Domain ConvexPD Algebraic Universal Sum_Cpo Main - Representable + Main + Domain + Powerdomains + Sum_Cpo uses "holcf_logic.ML" "Tools/adm_tac.ML" diff -r c23b42730b9b -r c4d3d65856dd src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Sun Feb 28 14:05:21 2010 -0800 +++ b/src/HOLCF/IsaMakefile Sun Feb 28 14:55:42 2010 -0800 @@ -51,6 +51,7 @@ Pcpodef.thy \ Pcpo.thy \ Porder.thy \ + Powerdomains.thy \ Product_Cpo.thy \ Representable.thy \ Sprod.thy \ @@ -65,6 +66,7 @@ Tools/cont_proc.ML \ Tools/Domain/domain_extender.ML \ Tools/Domain/domain_axioms.ML \ + Tools/Domain/domain_constructors.ML \ Tools/Domain/domain_isomorphism.ML \ Tools/Domain/domain_library.ML \ Tools/Domain/domain_syntax.ML \ diff -r c23b42730b9b -r c4d3d65856dd src/HOLCF/Powerdomains.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Powerdomains.thy Sun Feb 28 14:55:42 2010 -0800 @@ -0,0 +1,310 @@ +(* Title: HOLCF/Powerdomains.thy + Author: Brian Huffman +*) + +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 +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 (intro finite_deflation.intro finite_deflation_axioms.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 (intro finite_deflation.intro finite_deflation_axioms.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 (intro finite_deflation.intro finite_deflation_axioms.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)" +apply (rule isodeflI) +apply (simp add: cast_upper_defl 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)" +apply (rule isodeflI) +apply (simp add: cast_lower_defl 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)" +apply (rule isodeflI) +apply (simp add: cast_convex_defl cast_isodefl) +apply (simp add: emb_convex_pd_def prj_convex_pd_def) +apply (simp add: convex_map_map) +done + +subsection {* Domain package setup for powerdomains *} + +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 "lower_pd"}, @{term lower_defl}, @{const_name lower_map}, + @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}), + + (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map}, + @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID})] +*} + +end diff -r c23b42730b9b -r c4d3d65856dd src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Sun Feb 28 14:05:21 2010 -0800 +++ b/src/HOLCF/Representable.thy Sun Feb 28 14:55:42 2010 -0800 @@ -5,7 +5,7 @@ header {* Representable Types *} theory Representable -imports Algebraic Universal Ssum Sprod One ConvexPD Fixrec +imports Algebraic Universal Ssum Sprod One Fixrec uses ("Tools/repdef.ML") ("Tools/Domain/domain_isomorphism.ML") @@ -460,214 +460,6 @@ end -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 -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 (intro finite_deflation.intro finite_deflation_axioms.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 (intro finite_deflation.intro finite_deflation_axioms.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 (intro finite_deflation.intro finite_deflation_axioms.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 {* Type combinators *} definition @@ -697,9 +489,6 @@ definition "sprod_defl = TypeRep_fun2 sprod_map" definition "cprod_defl = TypeRep_fun2 cprod_map" definition "u_defl = TypeRep_fun1 u_map" -definition "upper_defl = TypeRep_fun1 upper_map" -definition "lower_defl = TypeRep_fun1 lower_map" -definition "convex_defl = TypeRep_fun1 convex_map" lemma Rep_fin_defl_mono: "a \ b \ Rep_fin_defl a \ Rep_fin_defl b" unfolding below_fin_defl_def . @@ -783,27 +572,6 @@ apply (erule finite_deflation_u_map) done -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 - text {* REP of type constructor = type combinator *} lemma REP_cfun: "REP('a \ 'b) = cfun_defl\REP('a)\REP('b)" @@ -814,7 +582,6 @@ 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) @@ -847,39 +614,12 @@ apply (simp add: u_map_map cfcomp1) 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 - lemmas REP_simps = REP_cfun REP_ssum REP_sprod REP_cprod REP_up - REP_upper - REP_lower - REP_convex subsection {* Isomorphic deflations *} @@ -1007,30 +747,6 @@ apply (simp add: u_map_map) done -lemma isodefl_upper: - "isodefl d t \ isodefl (upper_map\d) (upper_defl\t)" -apply (rule isodeflI) -apply (simp add: cast_upper_defl 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)" -apply (rule isodeflI) -apply (simp add: cast_lower_defl 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)" -apply (rule isodeflI) -apply (simp add: cast_convex_defl cast_isodefl) -apply (simp add: emb_convex_pd_def prj_convex_pd_def) -apply (simp add: convex_map_map) -done - subsection {* Constructing Domain Isomorphisms *} use "Tools/Domain/domain_isomorphism.ML" @@ -1050,16 +766,7 @@ @{thm REP_cprod}, @{thm isodefl_cprod}, @{thm cprod_map_ID}), (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, - @{thm REP_up}, @{thm isodefl_u}, @{thm u_map_ID}), - - (@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}, - @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}), - - (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}, - @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}), - - (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map}, - @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID})] + @{thm REP_up}, @{thm isodefl_u}, @{thm u_map_ID})] *} end