src/HOL/Probability/Fin_Map.thy
changeset 62101 26c0a70f78a3
parent 61988 34b51f436e92
child 62102 877463945ce9
     1.1 --- a/src/HOL/Probability/Fin_Map.thy	Fri Jan 08 16:37:56 2016 +0100
     1.2 +++ b/src/HOL/Probability/Fin_Map.thy	Fri Jan 08 17:40:59 2016 +0100
     1.3 @@ -150,7 +150,7 @@
     1.4  begin
     1.5  
     1.6  definition open_finmap :: "('a \<Rightarrow>\<^sub>F 'b) set \<Rightarrow> bool" where
     1.7 -  "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
     1.8 +   [code del]: "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
     1.9  
    1.10  lemma open_Pi'I: "(\<And>i. i \<in> I \<Longrightarrow> open (A i)) \<Longrightarrow> open (Pi' I A)"
    1.11    by (auto intro: generate_topology.Basis simp: open_finmap_def)
    1.12 @@ -254,12 +254,31 @@
    1.13  
    1.14  subsection \<open>Metric Space of Finite Maps\<close>
    1.15  
    1.16 -instantiation finmap :: (type, metric_space) metric_space
    1.17 +(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
    1.18 +
    1.19 +instantiation finmap :: (type, metric_space) dist
    1.20  begin
    1.21  
    1.22  definition dist_finmap where
    1.23    "dist P Q = Max (range (\<lambda>i. dist ((P)\<^sub>F i) ((Q)\<^sub>F i))) + (if domain P = domain Q then 0 else 1)"
    1.24  
    1.25 +instance ..
    1.26 +end
    1.27 +
    1.28 +instantiation finmap :: (type, metric_space) uniformity_dist
    1.29 +begin
    1.30 +
    1.31 +definition [code del]:
    1.32 +  "(uniformity :: (('a, 'b) finmap \<times> ('a, 'b) finmap) filter) = 
    1.33 +    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    1.34 +
    1.35 +instance 
    1.36 +  by standard (rule uniformity_finmap_def)
    1.37 +end
    1.38 +
    1.39 +instantiation finmap :: (type, metric_space) metric_space
    1.40 +begin
    1.41 +
    1.42  lemma finite_proj_image': "x \<notin> domain P \<Longrightarrow> finite ((P)\<^sub>F ` S)"
    1.43    by (rule finite_subset[of _ "proj P ` (domain P \<inter> S \<union> {x})"]) auto
    1.44  
    1.45 @@ -308,7 +327,7 @@
    1.46  instance
    1.47  proof
    1.48    fix S::"('a \<Rightarrow>\<^sub>F 'b) set"
    1.49 -  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" (is "_ = ?od")
    1.50 +  have *: "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" (is "_ = ?od")
    1.51    proof
    1.52      assume "open S"
    1.53      thus ?od
    1.54 @@ -387,6 +406,9 @@
    1.55        by (intro generate_topology.UN) (auto intro: generate_topology.Basis)
    1.56      finally show "open S" .
    1.57    qed
    1.58 +  show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
    1.59 +    unfolding * eventually_uniformity_metric
    1.60 +    by (simp del: split_paired_All add: dist_finmap_def dist_commute eq_commute)
    1.61  next
    1.62    fix P Q::"'a \<Rightarrow>\<^sub>F 'b"
    1.63    have Max_eq_iff: "\<And>A m. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (Max A = m) = (m \<in> A \<and> (\<forall>a\<in>A. a \<le> m))"