--- 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"
--- 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 \
--- /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\<cdot>emb"
+definition prj_upper_pd_def: "prj = upper_map\<cdot>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\<cdot>emb"
+definition prj_lower_pd_def: "prj = lower_map\<cdot>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\<cdot>emb"
+definition prj_convex_pd_def: "prj = convex_map\<cdot>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 \<rightarrow> 'b::cpo"
+ assumes "finite ((\<lambda>x. d\<cdot>x) ` {x. compact x})"
+ shows "finite (range (\<lambda>x. d\<cdot>x))"
+proof (rule finite_subset [OF _ prems])
+ {
+ fix x :: 'a
+ have "range (\<lambda>i. d\<cdot>(approx i\<cdot>x)) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
+ by auto
+ hence "finite (range (\<lambda>i. d\<cdot>(approx i\<cdot>x)))"
+ using prems by (rule finite_subset)
+ hence "finite_chain (\<lambda>i. d\<cdot>(approx i\<cdot>x))"
+ by (simp add: finite_range_imp_finch)
+ hence "\<exists>i. (\<Squnion>i. d\<cdot>(approx i\<cdot>x)) = d\<cdot>(approx i\<cdot>x)"
+ by (simp add: finite_chain_def maxinch_is_thelub)
+ hence "\<exists>i. d\<cdot>x = d\<cdot>(approx i\<cdot>x)"
+ by (simp add: lub_distribs)
+ hence "d\<cdot>x \<in> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
+ by auto
+ }
+ thus "range (\<lambda>x. d\<cdot>x) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
+ by clarsimp
+qed
+
+lemma finite_deflation_upper_map:
+ assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>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\<cdot>d)" by (rule deflation_upper_map)
+ have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
+ hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
+ by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
+ hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
+ hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>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 (\<lambda>x. d\<cdot>x))))" by simp
+ hence "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>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 "\<exists>b. d\<cdot>(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 ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` {xs::'a upper_pd. compact xs})"
+ by simp
+ hence "finite (range (\<lambda>xs. upper_map\<cdot>d\<cdot>xs))"
+ by (rule finite_compact_range_imp_finite_range)
+ thus "finite {xs. upper_map\<cdot>d\<cdot>xs = xs}"
+ by (rule finite_range_imp_finite_fixes)
+qed
+
+lemma finite_deflation_lower_map:
+ assumes "finite_deflation d" shows "finite_deflation (lower_map\<cdot>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\<cdot>d)" by (rule deflation_lower_map)
+ have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
+ hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
+ by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
+ hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
+ hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>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 (\<lambda>x. d\<cdot>x))))" by simp
+ hence "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>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 "\<exists>b. d\<cdot>(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 ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` {xs::'a lower_pd. compact xs})"
+ by simp
+ hence "finite (range (\<lambda>xs. lower_map\<cdot>d\<cdot>xs))"
+ by (rule finite_compact_range_imp_finite_range)
+ thus "finite {xs. lower_map\<cdot>d\<cdot>xs = xs}"
+ by (rule finite_range_imp_finite_fixes)
+qed
+
+lemma finite_deflation_convex_map:
+ assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>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\<cdot>d)" by (rule deflation_convex_map)
+ have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
+ hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
+ by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
+ hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
+ hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>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 (\<lambda>x. d\<cdot>x))))" by simp
+ hence "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>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 "\<exists>b. d\<cdot>(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 ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` {xs::'a convex_pd. compact xs})"
+ by simp
+ hence "finite (range (\<lambda>xs. convex_map\<cdot>d\<cdot>xs))"
+ by (rule finite_compact_range_imp_finite_range)
+ thus "finite {xs. convex_map\<cdot>d\<cdot>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\<cdot>(upper_defl\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>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\<cdot>(lower_defl\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>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\<cdot>(convex_defl\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>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\<cdot>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\<cdot>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\<cdot>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 \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>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 \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>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 \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>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
--- 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\<cdot>emb"
-definition prj_upper_pd_def: "prj = upper_map\<cdot>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\<cdot>emb"
-definition prj_lower_pd_def: "prj = lower_map\<cdot>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\<cdot>emb"
-definition prj_convex_pd_def: "prj = convex_map\<cdot>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 \<rightarrow> 'b::cpo"
- assumes "finite ((\<lambda>x. d\<cdot>x) ` {x. compact x})"
- shows "finite (range (\<lambda>x. d\<cdot>x))"
-proof (rule finite_subset [OF _ prems])
- {
- fix x :: 'a
- have "range (\<lambda>i. d\<cdot>(approx i\<cdot>x)) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
- by auto
- hence "finite (range (\<lambda>i. d\<cdot>(approx i\<cdot>x)))"
- using prems by (rule finite_subset)
- hence "finite_chain (\<lambda>i. d\<cdot>(approx i\<cdot>x))"
- by (simp add: finite_range_imp_finch)
- hence "\<exists>i. (\<Squnion>i. d\<cdot>(approx i\<cdot>x)) = d\<cdot>(approx i\<cdot>x)"
- by (simp add: finite_chain_def maxinch_is_thelub)
- hence "\<exists>i. d\<cdot>x = d\<cdot>(approx i\<cdot>x)"
- by (simp add: lub_distribs)
- hence "d\<cdot>x \<in> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
- by auto
- }
- thus "range (\<lambda>x. d\<cdot>x) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
- by clarsimp
-qed
-
-lemma finite_deflation_upper_map:
- assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>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\<cdot>d)" by (rule deflation_upper_map)
- have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
- hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
- by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
- hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
- hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>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 (\<lambda>x. d\<cdot>x))))" by simp
- hence "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>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 "\<exists>b. d\<cdot>(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 ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` {xs::'a upper_pd. compact xs})"
- by simp
- hence "finite (range (\<lambda>xs. upper_map\<cdot>d\<cdot>xs))"
- by (rule finite_compact_range_imp_finite_range)
- thus "finite {xs. upper_map\<cdot>d\<cdot>xs = xs}"
- by (rule finite_range_imp_finite_fixes)
-qed
-
-lemma finite_deflation_lower_map:
- assumes "finite_deflation d" shows "finite_deflation (lower_map\<cdot>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\<cdot>d)" by (rule deflation_lower_map)
- have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
- hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
- by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
- hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
- hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>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 (\<lambda>x. d\<cdot>x))))" by simp
- hence "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>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 "\<exists>b. d\<cdot>(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 ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` {xs::'a lower_pd. compact xs})"
- by simp
- hence "finite (range (\<lambda>xs. lower_map\<cdot>d\<cdot>xs))"
- by (rule finite_compact_range_imp_finite_range)
- thus "finite {xs. lower_map\<cdot>d\<cdot>xs = xs}"
- by (rule finite_range_imp_finite_fixes)
-qed
-
-lemma finite_deflation_convex_map:
- assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>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\<cdot>d)" by (rule deflation_convex_map)
- have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
- hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
- by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
- hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
- hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>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 (\<lambda>x. d\<cdot>x))))" by simp
- hence "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>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 "\<exists>b. d\<cdot>(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 ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` {xs::'a convex_pd. compact xs})"
- by simp
- hence "finite (range (\<lambda>xs. convex_map\<cdot>d\<cdot>xs))"
- by (rule finite_compact_range_imp_finite_range)
- thus "finite {xs. convex_map\<cdot>d\<cdot>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 \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> 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\<cdot>(upper_defl\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>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\<cdot>(lower_defl\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>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\<cdot>(convex_defl\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>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 \<rightarrow> 'b) = cfun_defl\<cdot>REP('a)\<cdot>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 \<oplus> 'b) = ssum_defl\<cdot>REP('a)\<cdot>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\<cdot>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\<cdot>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\<cdot>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 \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>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 \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>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 \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>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