# HG changeset patch
# User hoelzl
# Date 1452271264 -3600
# Node ID 877463945ce9e2553bbe327666da8073729a0c47
# Parent  26c0a70f78a3d4e5f2b10c13df1ee2ca49558de8
fix code generation for uniformity: uniformity is a non-computable pure data.

diff -r 26c0a70f78a3 -r 877463945ce9 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Fri Jan 08 17:40:59 2016 +0100
+++ b/src/HOL/Complex.thy	Fri Jan 08 17:41:04 2016 +0100
@@ -284,6 +284,8 @@
 
 end
 
+declare uniformity_Abort[where 'a=complex, code]
+
 lemma norm_ii [simp]: "norm ii = 1"
   by (simp add: norm_complex_def)
 
diff -r 26c0a70f78a3 -r 877463945ce9 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Fri Jan 08 17:40:59 2016 +0100
+++ b/src/HOL/Filter.thy	Fri Jan 08 17:41:04 2016 +0100
@@ -26,6 +26,11 @@
   show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
 qed
 
+text \<open>Kill code generation for filters\<close>
+
+code_datatype Abs_filter
+declare [[code abort: Rep_filter]]
+
 lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
   using Rep_filter [of F] by simp
 
diff -r 26c0a70f78a3 -r 877463945ce9 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 08 17:40:59 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 08 17:41:04 2016 +0100
@@ -383,7 +383,7 @@
 
 lemma fps_numeral_nth: "numeral n $ i = (if i = 0 then numeral n else 0)"
   by (simp add: numeral_fps_const)
-  
+
 lemma fps_numeral_nth_0 [simp]: "numeral n $ 0 = numeral n"
   by (simp add: numeral_fps_const)
 
@@ -467,17 +467,17 @@
 lemma X_neq_numeral [simp]: "(X :: 'a :: {semiring_1,zero_neq_one} fps) \<noteq> numeral c"
   by (simp only: numeral_fps_const X_neq_fps_const) simp
 
-lemma X_pow_eq_X_pow_iff [simp]: 
+lemma X_pow_eq_X_pow_iff [simp]:
   "(X :: ('a :: {comm_ring_1}) fps) ^ m = X ^ n \<longleftrightarrow> m = n"
 proof
   assume "(X :: 'a fps) ^ m = X ^ n"
   hence "(X :: 'a fps) ^ m $ m = X ^ n $ m" by (simp only:)
   thus "m = n" by (simp split: split_if_asm)
 qed simp_all
-  
-
-subsection \<open>Subdegrees\<close>  
-  
+
+
+subsection \<open>Subdegrees\<close>
+
 definition subdegree :: "('a::zero) fps \<Rightarrow> nat" where
   "subdegree f = (if f = 0 then 0 else LEAST n. f$n \<noteq> 0)"
 
@@ -511,7 +511,7 @@
   also from \<open>f \<noteq> 0\<close> have "subdegree f = (LEAST n. f $ n \<noteq> 0)" by (simp add: subdegree_def)
   finally show "f $ n = 0" using not_less_Least by blast
 qed simp_all
-  
+
 lemma subdegree_geI:
   assumes "f \<noteq> 0" "\<And>i. i < n \<Longrightarrow> f$i = 0"
   shows   "subdegree f \<ge> n"
@@ -598,7 +598,7 @@
   finally show "(f * g) $ (subdegree f + subdegree g) \<noteq> 0" .
 next
   fix m assume m: "m < subdegree f + subdegree g"
-  have "(f * g) $ m = (\<Sum>i=0..m. f$i * g$(m-i))" by (simp add: fps_mult_nth) 
+  have "(f * g) $ m = (\<Sum>i=0..m. f$i * g$(m-i))" by (simp add: fps_mult_nth)
   also have "... = (\<Sum>i=0..m. 0)"
   proof (rule setsum.cong)
     fix i assume "i \<in> {0..m}"
@@ -695,9 +695,9 @@
 lemma fps_shift_numeral: "fps_shift n (numeral c) = (if n = 0 then numeral c else 0)"
   by (simp add: numeral_fps_const fps_shift_fps_const)
 
-lemma fps_shift_X_power [simp]: 
+lemma fps_shift_X_power [simp]:
   "n \<le> m \<Longrightarrow> fps_shift n (X ^ m) = (X ^ (m - n) ::'a::comm_ring_1 fps)"
-  by (intro fps_ext) (auto simp: fps_shift_def ) 
+  by (intro fps_ext) (auto simp: fps_shift_def )
 
 lemma fps_shift_times_X_power:
   "n \<le> subdegree f \<Longrightarrow> fps_shift n f * X ^ n = (f :: 'a :: comm_ring_1 fps)"
@@ -711,7 +711,7 @@
   "m \<le> n \<Longrightarrow> fps_shift n (f * X^m) = fps_shift (n - m) (f :: 'a :: comm_ring_1 fps)"
   by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero)
 
-lemma fps_shift_subdegree [simp]: 
+lemma fps_shift_subdegree [simp]:
   "n \<le> subdegree f \<Longrightarrow> subdegree (fps_shift n f) = subdegree (f :: 'a :: comm_ring_1 fps) - n"
   by (cases "f = 0") (force intro: nth_less_subdegree_zero subdegreeI)+
 
@@ -726,11 +726,11 @@
 lemma fps_shift_fps_shift:
   "fps_shift (m + n) f = fps_shift m (fps_shift n f)"
   by (rule fps_ext) (simp add: add_ac)
-  
+
 lemma fps_shift_add:
   "fps_shift n (f + g) = fps_shift n f + fps_shift n g"
   by (simp add: fps_eq_iff)
-  
+
 lemma fps_shift_mult:
   assumes "n \<le> subdegree (g :: 'b :: {comm_ring_1} fps)"
   shows   "fps_shift n (h*g) = h * fps_shift n g"
@@ -774,7 +774,7 @@
 
 lemma fps_cutoff_0 [simp]: "fps_cutoff 0 f = 0"
   by (simp add: fps_eq_iff)
-  
+
 lemma fps_cutoff_zero [simp]: "fps_cutoff n 0 = 0"
   by (simp add: fps_eq_iff)
 
@@ -782,12 +782,12 @@
   by (simp add: fps_eq_iff)
 
 lemma fps_cutoff_fps_const: "fps_cutoff n (fps_const c) = (if n = 0 then 0 else fps_const c)"
-  by (simp add: fps_eq_iff)  
+  by (simp add: fps_eq_iff)
 
 lemma fps_cutoff_numeral: "fps_cutoff n (numeral c) = (if n = 0 then 0 else numeral c)"
   by (simp add: numeral_fps_const fps_cutoff_fps_const)
 
-lemma fps_shift_cutoff: 
+lemma fps_shift_cutoff:
   "fps_shift n (f :: ('a :: comm_ring_1) fps) * X^n + fps_cutoff n f = f"
   by (simp add: fps_eq_iff X_power_mult_right_nth)
 
@@ -844,9 +844,9 @@
       let ?n = "subdegree (a - b)"
       from neq have "dist a b > 0" "dist b c > 0" and "dist a c > 0" by (simp_all add: dist_fps_def)
       with that have "dist a b > dist a c" and "dist a b > dist b c" by simp_all
-      with neq have "?n < subdegree (a - c)" and "?n < subdegree (b - c)"  
+      with neq have "?n < subdegree (a - c)" and "?n < subdegree (b - c)"
         by (simp_all add: dist_fps_def field_simps)
-      hence "(a - c) $ ?n = 0" and "(b - c) $ ?n = 0" 
+      hence "(a - c) $ ?n = 0" and "(b - c) $ ?n = 0"
         by (simp_all only: nth_less_subdegree_zero)
       hence "(a - b) $ ?n = 0" by simp
       moreover from neq have "(a - b) $ ?n \<noteq> 0" by (intro nth_subdegree_nonzero) simp_all
@@ -858,6 +858,8 @@
 
 end
 
+declare uniformity_Abort[where 'a="'a :: comm_ring_1 fps", code]
+
 lemma open_fps_def: "open (S :: 'a::comm_ring_1 fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
   unfolding open_dist ball_def subset_eq by simp
 
@@ -925,8 +927,8 @@
           from False have dth: "dist (?s n) a = (1/2)^subdegree (?s n - a)"
             by (simp add: dist_fps_def field_simps)
           from False have kn: "subdegree (?s n - a) > n"
-            by (intro subdegree_greaterI) (simp_all add: fps_sum_rep_nth)              
-          then have "dist (?s n) a < (1/2)^n" 
+            by (intro subdegree_greaterI) (simp_all add: fps_sum_rep_nth)
+          then have "dist (?s n) a < (1/2)^n"
             by (simp add: field_simps dist_fps_def)
           also have "\<dots> \<le> (1/2)^n0"
             using nn0 by (simp add: divide_simps)
@@ -958,7 +960,7 @@
 definition fps_inverse_def: "inverse f = (if f $ 0 = 0 then 0 else Abs_fps (natfun_inverse f))"
 
 definition fps_divide_def:
-  "f div g = (if g = 0 then 0 else 
+  "f div g = (if g = 0 then 0 else
      let n = subdegree g; h = fps_shift n g
      in  fps_shift n (f * inverse h))"
 
@@ -1012,7 +1014,7 @@
 
 lemma fps_inverse_0_iff[simp]: "(inverse f) $ 0 = (0::'a::division_ring) \<longleftrightarrow> f $ 0 = 0"
   by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero)
-  
+
 lemma fps_inverse_nth_0 [simp]: "inverse f $ 0 = inverse (f $ 0 :: 'a :: division_ring)"
   by (simp add: fps_inverse_def)
 
@@ -1100,7 +1102,7 @@
   also from A have "... = inverse f * inverse g" by auto
   finally show "inverse (f * g) = inverse f * inverse g" .
 qed
-  
+
 
 lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field))) =
     Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then - 1 else 0)"
@@ -1142,15 +1144,15 @@
 
 definition fps_mod_def:
   "f mod g = (if g = 0 then f else
-     let n = subdegree g; h = fps_shift n g 
+     let n = subdegree g; h = fps_shift n g
      in  fps_cutoff n (f * inverse h) * h)"
 
-lemma fps_mod_eq_zero: 
+lemma fps_mod_eq_zero:
   assumes "g \<noteq> 0" and "subdegree f \<ge> subdegree g"
   shows   "f mod g = 0"
   using assms by (cases "f = 0") (auto simp: fps_cutoff_zero_iff fps_mod_def Let_def)
 
-lemma fps_times_divide_eq: 
+lemma fps_times_divide_eq:
   assumes "g \<noteq> 0" and "subdegree f \<ge> subdegree (g :: 'a fps)"
   shows   "f div g * g = f"
 proof (cases "f = 0")
@@ -1158,7 +1160,7 @@
   def n \<equiv> "subdegree g"
   def h \<equiv> "fps_shift n g"
   from assms have [simp]: "h $ 0 \<noteq> 0" unfolding h_def by (simp add: n_def)
-  
+
   from assms nz have "f div g * g = fps_shift n (f * inverse h) * g"
     by (simp add: fps_divide_def Let_def h_def n_def)
   also have "... = fps_shift n (f * inverse h) * X^n * h" unfolding h_def n_def
@@ -1170,12 +1172,12 @@
   finally show ?thesis by simp
 qed (simp_all add: fps_divide_def Let_def)
 
-lemma 
+lemma
   assumes "g$0 \<noteq> 0"
   shows   fps_divide_unit: "f div g = f * inverse g" and fps_mod_unit [simp]: "f mod g = 0"
 proof -
   from assms have [simp]: "subdegree g = 0" by (simp add: subdegree_eq_0_iff)
-  from assms show "f div g = f * inverse g" 
+  from assms show "f div g = f * inverse g"
     by (auto simp: fps_divide_def Let_def subdegree_eq_0_iff)
   from assms show "f mod g = 0" by (intro fps_mod_eq_zero) auto
 qed
@@ -1190,11 +1192,11 @@
   from assms have "h \<noteq> 0" by auto
   note nz [simp] = \<open>g \<noteq> 0\<close> \<open>h \<noteq> 0\<close>
   from assms have [simp]: "subdegree h = 0" by (simp add: subdegree_eq_0_iff)
-  
-  have "(h * f) div (h * g) = 
+
+  have "(h * f) div (h * g) =
           fps_shift (subdegree g) (h * f * inverse (fps_shift (subdegree g) (h*g)))"
     by (simp add: fps_divide_def Let_def)
-  also have "h * f * inverse (fps_shift (subdegree g) (h*g)) = 
+  also have "h * f * inverse (fps_shift (subdegree g) (h*g)) =
                (inverse h * h) * f * inverse (fps_shift (subdegree g) g)"
     by (subst fps_shift_mult) (simp_all add: algebra_simps fps_inverse_mult)
   also from assms have "inverse h * h = 1" by (rule inverse_mult_eq_1)
@@ -1205,7 +1207,7 @@
   "(f * X^m) div (g * X^m) = f div (g :: 'a :: field fps)"
 proof (cases "g = 0")
   assume [simp]: "g \<noteq> 0"
-  have "(f * X^m) div (g * X^m) = 
+  have "(f * X^m) div (g * X^m) =
           fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*X^m))*X^m)"
     by (simp add: fps_divide_def Let_def algebra_simps)
   also have "... = f div g"
@@ -1217,7 +1219,7 @@
   fix f g :: "'a fps"
   def n \<equiv> "subdegree g"
   def h \<equiv> "fps_shift n g"
-  
+
   show "f div g * g + f mod g = f"
   proof (cases "g = 0 \<or> f = 0")
     assume "\<not>(g = 0 \<or> f = 0)"
@@ -1229,8 +1231,8 @@
     next
       assume "subdegree f < subdegree g"
       have g_decomp: "g = h * X^n" unfolding h_def n_def by (rule subdegree_decompose)
-      have "f div g * g + f mod g = 
-              fps_shift n (f * inverse h) * g + fps_cutoff n (f * inverse h) * h" 
+      have "f div g * g + f mod g =
+              fps_shift n (f * inverse h) * g + fps_cutoff n (f * inverse h) * h"
         by (simp add: fps_mod_def fps_divide_def Let_def n_def h_def)
       also have "... = h * (fps_shift n (f * inverse h) * X^n + fps_cutoff n (f * inverse h))"
         by (subst g_decomp) (simp add: algebra_simps)
@@ -1268,7 +1270,7 @@
     by (subst subdegree_decompose) (simp_all add: dfs)
   also have "... = X^n" by (subst inverse_mult_eq_1) (simp_all add: dfs)
   also have "fps_shift n (g * X^n) = g" by simp
-  also have "fps_shift n (f * inverse h') = f div h" 
+  also have "fps_shift n (f * inverse h') = f div h"
     by (simp add: fps_divide_def Let_def dfs)
   finally show "(f + g * h) div h = g + f div h" by simp
 qed (auto simp: fps_divide_def fps_mod_def Let_def)
@@ -1297,16 +1299,16 @@
   by (simp add: fps_divide_unit divide_inverse)
 
 
-lemma dvd_imp_subdegree_le: 
+lemma dvd_imp_subdegree_le:
   "(f :: 'a :: idom fps) dvd g \<Longrightarrow> g \<noteq> 0 \<Longrightarrow> subdegree f \<le> subdegree g"
   by (auto elim: dvdE)
 
-lemma fps_dvd_iff: 
+lemma fps_dvd_iff:
   assumes "(f :: 'a :: field fps) \<noteq> 0" "g \<noteq> 0"
   shows   "f dvd g \<longleftrightarrow> subdegree f \<le> subdegree g"
 proof
   assume "subdegree f \<le> subdegree g"
-  with assms have "g mod f = 0" 
+  with assms have "g mod f = 0"
     by (simp add: fps_mod_def Let_def fps_cutoff_zero_iff)
   thus "f dvd g" by (simp add: dvd_eq_mod_eq_0)
 qed (simp add: assms dvd_imp_subdegree_le)
@@ -1317,7 +1319,7 @@
 lemma fps_const_divide: "fps_const (x :: _ :: field) / fps_const y = fps_const (x / y)"
   by (cases "y = 0") (simp_all add: fps_divide_unit fps_const_inverse divide_inverse)
 
-lemma inverse_fps_numeral: 
+lemma inverse_fps_numeral:
   "inverse (numeral n :: ('a :: field_char_0) fps) = fps_const (inverse (numeral n))"
   by (intro fps_inverse_unique fps_ext) (simp_all add: fps_numeral_nth)
 
@@ -1327,7 +1329,7 @@
 instantiation fps :: (field) normalization_semidom
 begin
 
-definition fps_unit_factor_def [simp]: 
+definition fps_unit_factor_def [simp]:
   "unit_factor f = fps_shift (subdegree f) f"
 
 definition fps_normalize_def [simp]:
@@ -1358,7 +1360,7 @@
 instantiation fps :: (field) euclidean_ring
 begin
 
-definition fps_euclidean_size_def: 
+definition fps_euclidean_size_def:
   "euclidean_size f = (if f = 0 then 0 else Suc (subdegree f))"
 
 instance proof
@@ -1395,10 +1397,10 @@
   qed (simp_all add: fps_dvd_iff)
 qed
 
-lemma fps_gcd_altdef: "gcd (f :: 'a :: field fps) g = 
+lemma fps_gcd_altdef: "gcd (f :: 'a :: field fps) g =
   (if f = 0 \<and> g = 0 then 0 else
-   if f = 0 then X ^ subdegree g else 
-   if g = 0 then X ^ subdegree f else 
+   if f = 0 then X ^ subdegree g else
+   if g = 0 then X ^ subdegree f else
      X ^ min (subdegree f) (subdegree g))"
   by (simp add: fps_gcd)
 
@@ -1414,7 +1416,7 @@
   qed (simp_all add: fps_dvd_iff)
 qed
 
-lemma fps_lcm_altdef: "lcm (f :: 'a :: field fps) g = 
+lemma fps_lcm_altdef: "lcm (f :: 'a :: field fps) g =
   (if f = 0 \<or> g = 0 then 0 else X ^ max (subdegree f) (subdegree g))"
   by (simp add: fps_lcm)
 
@@ -1434,7 +1436,7 @@
   with d assms show "d dvd X ^ (INF f:A-{0}. subdegree f)" by (simp add: fps_dvd_iff)
 qed simp_all
 
-lemma fps_Gcd_altdef: "Gcd (A :: 'a :: field fps set) = 
+lemma fps_Gcd_altdef: "Gcd (A :: 'a :: field fps set) =
   (if A \<subseteq> {0} then 0 else X ^ (INF f:A-{0}. subdegree f))"
   using fps_Gcd by auto
 
@@ -1460,7 +1462,7 @@
 qed simp_all
 
 lemma fps_Lcm_altdef:
-  "Lcm (A :: 'a :: field fps set) = 
+  "Lcm (A :: 'a :: field fps set) =
      (if 0 \<in> A \<or> \<not>bdd_above (subdegree`A) then 0 else
       if A = {} then 1 else X ^ (SUP f:A. subdegree f))"
 proof (cases "bdd_above (subdegree`A)")
@@ -2876,7 +2878,7 @@
     note thb[simp] = iffD1[OF power_radical[where r=r and k=h], OF b0 rb0[unfolded k], unfolded k[symmetric]]
     from b0 rb0' have th2: "(?r a / ?r b)^k = a/b"
       by (simp add: fps_divide_unit power_mult_distrib fps_inverse_power[symmetric])
-      
+
     from iffD1[OF radical_unique[where r=r and a="?r a / ?r b" and b="a/b" and k=h], symmetric, unfolded k[symmetric], OF th0 th1 ab0' th2]
     show ?thesis .
   qed
@@ -4178,9 +4180,9 @@
 proof -
   have th0: "fps_cos c $ 0 \<noteq> 0" by (simp add: fps_cos_def)
   from this have "fps_cos c \<noteq> 0" by (intro notI) simp
-  hence "fps_deriv (fps_tan c) = 
+  hence "fps_deriv (fps_tan c) =
            fps_const c * (fps_cos c^2 + fps_sin c^2) / (fps_cos c^2)"
-    by (simp add: fps_tan_def fps_divide_deriv power2_eq_square algebra_simps 
+    by (simp add: fps_tan_def fps_divide_deriv power2_eq_square algebra_simps
                   fps_sin_deriv fps_cos_deriv fps_const_neg[symmetric] div_mult_swap
              del: fps_const_neg)
   also note fps_sin_cos_sum_of_squares
diff -r 26c0a70f78a3 -r 877463945ce9 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Fri Jan 08 17:40:59 2016 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Fri Jan 08 17:41:04 2016 +0100
@@ -276,13 +276,15 @@
 begin
 
 definition [code del]:
-  "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) = 
+  "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) =
     (INF e:{0 <..}. principal {(x, y). dist x y < e})"
 
-instance 
+instance
   by standard (rule uniformity_prod_def)
 end
 
+declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
+
 instantiation prod :: (metric_space, metric_space) metric_space
 begin
 
@@ -566,9 +568,9 @@
 lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
     by (cases x, simp)+
 
-lemma 
+lemma
   fixes x :: "'a::real_normed_vector"
-  shows norm_Pair1 [simp]: "norm (0,x) = norm x" 
+  shows norm_Pair1 [simp]: "norm (0,x) = norm x"
     and norm_Pair2 [simp]: "norm (x,0) = norm x"
 by (auto simp: norm_Pair)
 
diff -r 26c0a70f78a3 -r 877463945ce9 src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Fri Jan 08 17:40:59 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Fri Jan 08 17:41:04 2016 +0100
@@ -152,6 +152,8 @@
 
 end
 
+declare uniformity_Abort[where 'a="('a :: real_normed_vector) \<Rightarrow>\<^sub>L ('b :: real_normed_vector)", code]
+
 lemma norm_blinfun_eqI:
   assumes "n \<le> norm (blinfun_apply f x) / norm x"
   assumes "\<And>x. norm (blinfun_apply f x) \<le> n * norm x"
diff -r 26c0a70f78a3 -r 877463945ce9 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Jan 08 17:40:59 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Jan 08 17:41:04 2016 +0100
@@ -252,7 +252,7 @@
   fix x :: "'a ^ 'b" show "\<not> open {x}"
   proof
     assume "open {x}"
-    hence "\<forall>i. open ((\<lambda>x. x $ i) ` {x})" by (fast intro: open_image_vec_nth)   
+    hence "\<forall>i. open ((\<lambda>x. x $ i) ` {x})" by (fast intro: open_image_vec_nth)
     hence "\<forall>i. open {x $ i}" by simp
     thus "False" by (simp add: not_open_singleton)
   qed
@@ -275,13 +275,15 @@
 begin
 
 definition [code del]:
-  "(uniformity :: (('a, 'b) vec \<times> ('a, 'b) vec) filter) = 
+  "(uniformity :: (('a, 'b) vec \<times> ('a, 'b) vec) filter) =
     (INF e:{0 <..}. principal {(x, y). dist x y < e})"
 
-instance 
+instance
   by standard (rule uniformity_vec_def)
 end
 
+declare uniformity_Abort[where 'a="'a :: metric_space ^ 'b :: finite", code]
+
 instantiation vec :: (metric_space, finite) metric_space
 begin
 
diff -r 26c0a70f78a3 -r 877463945ce9 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Fri Jan 08 17:40:59 2016 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Fri Jan 08 17:41:04 2016 +0100
@@ -269,13 +269,15 @@
 begin
 
 definition [code del]:
-  "(uniformity :: (('a, 'b) finmap \<times> ('a, 'b) finmap) filter) = 
+  "(uniformity :: (('a, 'b) finmap \<times> ('a, 'b) finmap) filter) =
     (INF e:{0 <..}. principal {(x, y). dist x y < e})"
 
-instance 
+instance
   by standard (rule uniformity_finmap_def)
 end
 
+declare uniformity_Abort[where 'a="('a, 'b::metric_space) finmap", code]
+
 instantiation finmap :: (type, metric_space) metric_space
 begin
 
diff -r 26c0a70f78a3 -r 877463945ce9 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 17:40:59 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 17:41:04 2016 +0100
@@ -9,7 +9,6 @@
 imports Real Topological_Spaces
 begin
 
-
 lemma (in ordered_ab_group_add) diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
   by (simp add: le_diff_eq)
 
@@ -1185,6 +1184,8 @@
 
 end
 
+declare uniformity_Abort[where 'a=real, code]
+
 lemma dist_of_real [simp]:
   fixes a :: "'a::real_normed_div_algebra"
   shows "dist (of_real x :: 'a) (of_real y) = dist x y"
diff -r 26c0a70f78a3 -r 877463945ce9 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Fri Jan 08 17:40:59 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy	Fri Jan 08 17:41:04 2016 +0100
@@ -102,7 +102,7 @@
   using open_Un[OF assms] by (simp add: Un_def)
 
 lemma open_Collect_ex: "(\<And>i. open {x. P i x}) \<Longrightarrow> open {x. \<exists>i. P i x}"
-  using open_UN[of UNIV "\<lambda>i. {x. P i x}"] unfolding Collect_ex_eq by simp 
+  using open_UN[of UNIV "\<lambda>i. {x. P i x}"] unfolding Collect_ex_eq by simp
 
 lemma open_Collect_imp: "closed {x. P x} \<Longrightarrow> open {x. Q x} \<Longrightarrow> open {x. P x \<longrightarrow> Q x}"
   unfolding imp_conv_disj by (intro open_Collect_disj open_Collect_neg)
@@ -120,7 +120,7 @@
   using closed_Un[OF assms] by (simp add: Un_def)
 
 lemma closed_Collect_all: "(\<And>i. closed {x. P i x}) \<Longrightarrow> closed {x. \<forall>i. P i x}"
-  using closed_INT[of UNIV "\<lambda>i. {x. P i x}"] unfolding Collect_all_eq by simp 
+  using closed_INT[of UNIV "\<lambda>i. {x. P i x}"] unfolding Collect_all_eq by simp
 
 lemma closed_Collect_imp: "open {x. P x} \<Longrightarrow> closed {x. Q x} \<Longrightarrow> closed {x. P x \<longrightarrow> Q x}"
   unfolding imp_conv_disj by (intro closed_Collect_disj closed_Collect_neg)
@@ -203,9 +203,9 @@
 | UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k) \<Longrightarrow> generate_topology S (\<Union>K)"
 | Basis: "s \<in> S \<Longrightarrow> generate_topology S s"
 
-hide_fact (open) UNIV Int UN Basis 
-
-lemma generate_topology_Union: 
+hide_fact (open) UNIV Int UN Basis
+
+lemma generate_topology_Union:
   "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
   using generate_topology.UN [of "K ` I"] by auto
 
@@ -344,7 +344,7 @@
 proof (safe intro!: antisym INF_greatest)
   fix S assume "generate_topology T S" "x \<in> S"
   then show "(INF S:{S \<in> T. x \<in> S}. principal S) \<le> principal S"
-    by induction 
+    by induction
        (auto intro: INF_lower order_trans simp add: inf_principal[symmetric] simp del: inf_principal)
 qed (auto intro!: INF_lower intro: generate_topology.intros)
 
@@ -352,7 +352,7 @@
   "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
   unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)
 
-lemma (in topological_space) eventually_nhds_in_open: 
+lemma (in topological_space) eventually_nhds_in_open:
   "open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
   by (subst eventually_nhds) blast
 
@@ -391,7 +391,7 @@
 proof (intro allI eventually_subst)
   have "eventually (\<lambda>x. x \<in> S) (nhds x)"
     using \<open>x \<in> S\<close> \<open>open S\<close> by (auto simp: eventually_nhds)
-  then show "\<forall>\<^sub>F n in nhds x. (n \<noteq> x \<longrightarrow> n \<in> T \<longrightarrow> P n) = (n \<noteq> x \<longrightarrow> n \<in> U \<longrightarrow> P n)" for P  
+  then show "\<forall>\<^sub>F n in nhds x. (n \<noteq> x \<longrightarrow> n \<in> T \<longrightarrow> P n) = (n \<noteq> x \<longrightarrow> n \<in> U \<longrightarrow> P n)" for P
     by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, blast)
 qed
 
@@ -412,14 +412,14 @@
 lemma (in order_topology) nhds_order: "nhds x =
   inf (INF a:{x <..}. principal {..< a}) (INF a:{..< x}. principal {a <..})"
 proof -
-  have 1: "{S \<in> range lessThan \<union> range greaterThan. x \<in> S} = 
+  have 1: "{S \<in> range lessThan \<union> range greaterThan. x \<in> S} =
       (\<lambda>a. {..< a}) ` {x <..} \<union> (\<lambda>a. {a <..}) ` {..< x}"
     by auto
   show ?thesis
     unfolding nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def ..
 qed
 
-lemma (in linorder_topology) at_within_order: "UNIV \<noteq> {x} \<Longrightarrow> 
+lemma (in linorder_topology) at_within_order: "UNIV \<noteq> {x} \<Longrightarrow>
   at x within s = inf (INF a:{x <..}. principal ({..< a} \<inter> s - {x}))
                       (INF a:{..< x}. principal ({a <..} \<inter> s - {x}))"
 proof (cases "{x <..} = {}" "{..< x} = {}" rule: case_split[case_product case_split])
@@ -472,7 +472,7 @@
   by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense)
 
 lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
-  by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 
+  by (auto simp: eventually_at_filter filter_eq_iff eventually_sup
            elim: eventually_elim2 eventually_mono)
 
 lemma eventually_at_split:
@@ -904,7 +904,7 @@
     by (intro dependent_nat_choice) (auto simp: conj_commute)
   then obtain f where "subseq f" and mono: "\<And>n m. f n \<le> m \<Longrightarrow> s m \<le> s (f n)"
     by (auto simp: subseq_Suc_iff)
-  moreover 
+  moreover
   then have "incseq f"
     unfolding subseq_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le)
   then have "monoseq (\<lambda>n. s (f n))"
@@ -963,7 +963,7 @@
 proof (rule inj_onI)
   assume g: "subseq g"
   fix x y assume "g x = g y"
-  with subseq_mono[OF g, of x y] subseq_mono[OF g, of y x] show "x = y" 
+  with subseq_mono[OF g, of x y] subseq_mono[OF g, of y x] show "x = y"
     by (cases x y rule: linorder_cases) simp_all
 qed
 
@@ -977,7 +977,7 @@
   by (simp add: decseq_def monoseq_def)
 
 lemma decseq_eq_incseq:
-  fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)" 
+  fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)"
   by (simp add: decseq_def incseq_def)
 
 lemma INT_decseq_offset:
@@ -1179,10 +1179,10 @@
 qed
 
 lemma (in first_countable_topology) eventually_nhds_within_iff_sequentially:
-  "eventually P (inf (nhds a) (principal s)) \<longleftrightarrow> 
+  "eventually P (inf (nhds a) (principal s)) \<longleftrightarrow>
     (\<forall>f. (\<forall>n. f n \<in> s) \<and> f \<longlonglongrightarrow> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
 proof (safe intro!: sequentially_imp_eventually_nhds_within)
-  assume "eventually P (inf (nhds a) (principal s))" 
+  assume "eventually P (inf (nhds a) (principal s))"
   then obtain S where "open S" "a \<in> S" "\<forall>x\<in>S. x \<in> s \<longrightarrow> P x"
     by (auto simp: eventually_inf_principal eventually_nhds)
   moreover fix f assume "\<forall>n. f n \<in> s" "f \<longlonglongrightarrow> a"
@@ -1624,7 +1624,7 @@
 
 lemma isCont_tendsto_compose: "isCont g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
   unfolding isCont_def by (rule tendsto_compose)
-  
+
 lemma continuous_on_tendsto_compose:
   assumes f_cont: "continuous_on s f"
   assumes g: "(g \<longlongrightarrow> l) F"
@@ -1657,7 +1657,7 @@
     unfolding eventually_nhds by (intro exI[of _ "f`S"]) (auto intro!: open_map)
 qed (metis filterlim_iff tendsto_at_iff_tendsto_nhds isCont_def eventually_filtermap cont)
 
-lemma continuous_at_split: 
+lemma continuous_at_split:
   "continuous (at (x::'a::linorder_topology)) f = (continuous (at_left x) f \<and> continuous (at_right x) f)"
   by (simp add: continuous_within filterlim_at_split)
 
@@ -1909,7 +1909,7 @@
   by (auto intro!: connectedI)
 
 lemma connectedD:
-  "connected A \<Longrightarrow> open U \<Longrightarrow> open V \<Longrightarrow> U \<inter> V \<inter> A = {} \<Longrightarrow> A \<subseteq> U \<union> V \<Longrightarrow> U \<inter> A = {} \<or> V \<inter> A = {}" 
+  "connected A \<Longrightarrow> open U \<Longrightarrow> open V \<Longrightarrow> U \<inter> V \<inter> A = {} \<Longrightarrow> A \<subseteq> U \<union> V \<Longrightarrow> U \<inter> A = {} \<or> V \<inter> A = {}"
   by (auto simp: connected_def)
 
 end
@@ -2209,7 +2209,7 @@
 lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
   unfolding connected_iff_interval by auto
 
-lemma connected_contains_Ioo: 
+lemma connected_contains_Ioo:
   fixes A :: "'a :: linorder_topology set"
   assumes A: "connected A" "a \<in> A" "b \<in> A" shows "{a <..< b} \<subseteq> A"
   using connectedD_interval[OF A] by (simp add: subset_eq Ball_def less_imp_le)
@@ -2434,7 +2434,7 @@
 
 subsection \<open>Uniform spaces\<close>
 
-class uniformity = 
+class uniformity =
   fixes uniformity :: "('a \<times> 'a) filter"
 begin
 
@@ -2443,6 +2443,10 @@
 
 end
 
+lemma uniformity_Abort:
+  "uniformity = Abs_filter (\<lambda>P. Code.abort (STR ''uniformity is not executable'') (\<lambda>x. Rep_filter uniformity P))"
+  unfolding Code.abort_def Rep_filter_inverse ..
+
 class open_uniformity = "open" + uniformity +
   assumes open_uniformity: "\<And>U. open U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
 
@@ -2494,7 +2498,7 @@
 lemma totally_bounded_subset: "totally_bounded S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> totally_bounded T"
   by (force simp add: totally_bounded_def)
 
-lemma totally_bounded_Union[intro]: 
+lemma totally_bounded_Union[intro]:
   assumes M: "finite M" "\<And>S. S \<in> M \<Longrightarrow> totally_bounded S" shows "totally_bounded (\<Union>M)"
   unfolding totally_bounded_def
 proof safe
@@ -2578,7 +2582,7 @@
 subsubsection \<open>Uniformly continuous functions\<close>
 
 definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::uniform_space \<Rightarrow> 'b::uniform_space) \<Rightarrow> bool" where
-  uniformly_continuous_on_uniformity: "uniformly_continuous_on s f \<longleftrightarrow> 
+  uniformly_continuous_on_uniformity: "uniformly_continuous_on s f \<longleftrightarrow>
     (LIM (x, y) (uniformity_on s). (f x, f y) :> uniformity)"
 
 lemma uniformly_continuous_onD: