# HG changeset patch
# User nipkow
# Date 1528825067 -7200
# Node ID 6f3bd27ba389e28809e68ed988e0ac93a3c26a6b
# Parent  b0eb6a91924df43f686b131074bd00e2d84bf9bc# Parent  b294e095f64cf2e61fa76b56130d8f4a26dc4ebd
merged

diff -r b294e095f64c -r 6f3bd27ba389 src/HOL/Analysis/Infinite_Products.thy
--- 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
diff -r b294e095f64c -r 6f3bd27ba389 src/HOL/Types_To_Sets/Examples/T2_Spaces.thy
--- 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:
diff -r b294e095f64c -r 6f3bd27ba389 src/HOL/Types_To_Sets/Types_To_Sets.thy
--- 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
diff -r b294e095f64c -r 6f3bd27ba389 src/HOL/Types_To_Sets/unoverload_type.ML
--- /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