--- a/src/HOL/Analysis/Infinite_Products.thy Tue Jun 12 17:18:40 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy Tue Jun 12 19:37:47 2018 +0200
@@ -6,9 +6,11 @@
*)
section \<open>Infinite Products\<close>
theory Infinite_Products
- imports Complex_Main
+ imports Topology_Euclidean_Space
begin
-
+
+subsection\<open>Preliminaries\<close>
+
lemma sum_le_prod:
fixes f :: "'a \<Rightarrow> 'b :: linordered_semidom"
assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
@@ -50,6 +52,8 @@
by (rule tendsto_eq_intros refl | simp)+
qed auto
+subsection\<open>Definitions and basic properties\<close>
+
definition raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool"
where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
@@ -135,6 +139,9 @@
by blast
qed (auto simp: prod_defs)
+
+subsection\<open>Absolutely convergent products\<close>
+
definition abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where
"abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>i. 1 + norm (f i - 1))"
@@ -383,6 +390,8 @@
shows "abs_convergent_prod f"
using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset)
+subsection\<open>Ignoring initial segments\<close>
+
lemma raw_has_prod_ignore_initial_segment:
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
assumes "raw_has_prod f M p" "N \<ge> M"
@@ -569,6 +578,8 @@
with L show ?thesis by (auto simp: prod_defs)
qed
+subsection\<open>More elementary properties\<close>
+
lemma raw_has_prod_cases:
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
assumes "raw_has_prod f M p"
@@ -1040,7 +1051,7 @@
using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast
-subsection \<open>Infinite products on topological monoids\<close>
+subsection \<open>Infinite products on topological spaces\<close>
context
fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_semigroup_mult,idom}"
@@ -1141,7 +1152,7 @@
end
-subsection \<open>Infinite summability on real normed vector spaces\<close>
+subsection \<open>Infinite summability on real normed fields\<close>
context
fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
@@ -1224,7 +1235,7 @@
end
-context (* Separate contexts are necessary to allow general use of the results above, here. *)
+context
fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
begin
@@ -1298,7 +1309,7 @@
end
-context (* Separate contexts are necessary to allow general use of the results above, here. *)
+context
fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
begin
@@ -1329,4 +1340,128 @@
end
+
+subsection\<open>Exponentials and logarithms\<close>
+
+context
+ fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
+begin
+
+lemma sums_imp_has_prod_exp:
+ assumes "f sums s"
+ shows "raw_has_prod (\<lambda>i. exp (f i)) 0 (exp s)"
+ using assms continuous_on_exp [of UNIV "\<lambda>x::'a. x"]
+ using continuous_on_tendsto_compose [of UNIV exp "(\<lambda>n. sum f {..n})" s]
+ by (simp add: prod_defs sums_def_le exp_sum)
+
+lemma convergent_prod_exp:
+ assumes "summable f"
+ shows "convergent_prod (\<lambda>i. exp (f i))"
+ using sums_imp_has_prod_exp assms unfolding summable_def convergent_prod_def by blast
+
+lemma prodinf_exp:
+ assumes "summable f"
+ shows "prodinf (\<lambda>i. exp (f i)) = exp (suminf f)"
+proof -
+ have "f sums suminf f"
+ using assms by blast
+ then have "(\<lambda>i. exp (f i)) has_prod exp (suminf f)"
+ by (simp add: has_prod_def sums_imp_has_prod_exp)
+ then show ?thesis
+ by (rule has_prod_unique [symmetric])
+qed
+
end
+
+lemma has_prod_imp_sums_ln_real:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes "raw_has_prod f 0 p" and 0: "\<And>x. f x > 0"
+ shows "(\<lambda>i. ln (f i)) sums (ln p)"
+proof -
+ have "p > 0"
+ using assms unfolding prod_defs by (metis LIMSEQ_prod_nonneg less_eq_real_def)
+ then show ?thesis
+ using assms continuous_on_ln [of "{0<..}" "\<lambda>x. x"]
+ using continuous_on_tendsto_compose [of "{0<..}" ln "(\<lambda>n. prod f {..n})" p]
+ by (auto simp: prod_defs sums_def_le ln_prod order_tendstoD)
+qed
+
+lemma summable_ln_real:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0"
+ shows "summable (\<lambda>i. ln (f i))"
+proof -
+ obtain M p where "raw_has_prod f M p"
+ using f convergent_prod_def by blast
+ then consider i where "i<M" "f i = 0" | p where "raw_has_prod f 0 p"
+ using raw_has_prod_cases by blast
+ then show ?thesis
+ proof cases
+ case 1
+ with 0 show ?thesis
+ by (metis less_irrefl)
+ next
+ case 2
+ then show ?thesis
+ using "0" has_prod_imp_sums_ln_real summable_def by blast
+ qed
+qed
+
+lemma suminf_ln_real:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0"
+ shows "suminf (\<lambda>i. ln (f i)) = ln (prodinf f)"
+proof -
+ have "f has_prod prodinf f"
+ by (simp add: f has_prod_iff)
+ then have "raw_has_prod f 0 (prodinf f)"
+ by (metis "0" has_prod_def less_irrefl)
+ then have "(\<lambda>i. ln (f i)) sums ln (prodinf f)"
+ using "0" has_prod_imp_sums_ln_real by blast
+ then show ?thesis
+ by (rule sums_unique [symmetric])
+qed
+
+lemma prodinf_exp_real:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0"
+ shows "prodinf f = exp (suminf (\<lambda>i. ln (f i)))"
+ by (simp add: "0" f less_0_prodinf suminf_ln_real)
+
+
+subsection\<open>Embeddings from the reals into some complete real normed field\<close>
+
+lemma tendsto_eq_of_real_lim:
+ assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"
+ shows "q = of_real (lim f)"
+proof -
+ have "convergent (\<lambda>n. of_real (f n) :: 'a)"
+ using assms convergent_def by blast
+ then have "convergent f"
+ unfolding convergent_def
+ by (simp add: convergent_eq_Cauchy Cauchy_def)
+ then show ?thesis
+ by (metis LIMSEQ_unique assms convergentD sequentially_bot tendsto_Lim tendsto_of_real)
+qed
+
+lemma tendsto_eq_of_real:
+ assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"
+ obtains r where "q = of_real r"
+ using tendsto_eq_of_real_lim assms by blast
+
+lemma has_prod_of_real_iff:
+ "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) has_prod of_real c \<longleftrightarrow> f has_prod c"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ apply (auto simp: prod_defs LIMSEQ_prod_0 tendsto_of_real_iff simp flip: of_real_prod)
+ using tendsto_eq_of_real
+ by (metis of_real_0 tendsto_of_real_iff)
+next
+ assume ?rhs
+ with tendsto_of_real_iff show ?lhs
+ by (fastforce simp: prod_defs simp flip: of_real_prod)
+qed
+
+end
--- a/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy Tue Jun 12 17:18:40 2018 +0200
+++ b/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy Tue Jun 12 19:37:47 2018 +0200
@@ -120,6 +120,9 @@
for the original relativization algorithm.\<close>
thm dictionary_second_step
+text \<open>Alternative construction using \<open>unoverload_type\<close>
+ (This does not require fiddling with \<open>Sign.add_const_constraint\<close>).\<close>
+lemmas dictionary_second_step' = dictionary_first_step[unoverload_type 'a]
text\<open>This is the set-based variant of the theorem compact_imp_closed.\<close>
lemma compact_imp_closed_set_based:
--- a/src/HOL/Types_To_Sets/Types_To_Sets.thy Tue Jun 12 17:18:40 2018 +0200
+++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy Tue Jun 12 19:37:47 2018 +0200
@@ -24,4 +24,8 @@
text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
ML_file "internalize_sort.ML"
+text\<open>The following file provides some automation to unoverload and internalize the parameters o
+ the sort constraints of a type variable.\<close>
+ML_file \<open>unoverload_type.ML\<close>
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML Tue Jun 12 19:37:47 2018 +0200
@@ -0,0 +1,68 @@
+(* Title: HOL/Types_To_Sets/unoverload_type.ML
+ Author: Fabian Immler, TU München
+
+Internalize sorts and unoverload parameters of a type variable.
+*)
+
+signature UNOVERLOAD_TYPE =
+sig
+ val unoverload_type: Context.generic -> string -> thm -> thm
+ val unoverload_type_attr: string -> attribute
+end;
+
+structure Unoverload_Type : UNOVERLOAD_TYPE =
+struct
+
+fun those [] = []
+ | those (NONE::xs) = those xs
+ | those (SOME x::xs) = x::those xs
+
+fun params_of_sort context sort =
+ let
+ val algebra = Sign.classes_of (Context.theory_of context)
+ val params = List.concat (map (Sorts.super_classes algebra) sort) |>
+ map (try (Axclass.get_info (Context.theory_of context))) |>
+ those |>
+ map #params |>
+ List.concat
+ in params end
+
+fun internalize_sort' ctvar thm =
+ let
+ val (_, thm') = Internalize_Sort.internalize_sort ctvar thm
+ val class_premise = case Thm.prems_of thm' of t::_=> t | [] =>
+ raise THM ("internalize_sort': no premise?", 0, [thm'])
+ val class_vars = Term.add_tvars class_premise []
+ val tvar = case class_vars of [x] => TVar x | _ =>
+ raise TERM ("internalize_sort': not one type class variable.", [class_premise])
+ in
+ (tvar, thm')
+ end
+
+fun unoverload_type context s thm =
+ let
+ val tvars = Term.add_tvars (Thm.prop_of thm) []
+ val thy = Context.theory_of context
+ in
+ case find_first (fn ((n,_), _) => n = s) tvars of NONE =>
+ raise THM ("unoverload_type: type variable ("^s^") not in theorem", 0, [thm])
+ | SOME (x as (_, sort)) =>
+ let
+ val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm
+ val consts = params_of_sort context sort |>
+ map (apsnd (map_type_tfree (fn ("'a", _) => tvar | x => TFree x)))
+ in
+ fold (fn c => Unoverloading.unoverload (Thm.global_cterm_of thy (Const c))) consts thm'
+ end
+ end
+
+val tyN = (Args.context -- Args.typ) >>
+ (fn (_, TFree (n, _)) => n
+ | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t))
+
+fun unoverload_type_attr n = Thm.rule_attribute [] (fn context => unoverload_type context n)
+
+val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
+ (tyN >> unoverload_type_attr) "internalize a sort"))
+
+end
\ No newline at end of file