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))"
```