src/HOL/Library/Inner_Product.thy
changeset 62101 26c0a70f78a3
parent 61915 e9812a95d108
child 63589 58aab4745e85
     1.1 --- a/src/HOL/Library/Inner_Product.thy	Fri Jan 08 16:37:56 2016 +0100
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Fri Jan 08 17:40:59 2016 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  subsection \<open>Real inner product spaces\<close>
     1.5  
     1.6  text \<open>
     1.7 -  Temporarily relax type constraints for @{term "open"},
     1.8 +  Temporarily relax type constraints for @{term "open"}, @{term "uniformity"},
     1.9    @{term dist}, and @{term norm}.
    1.10  \<close>
    1.11  
    1.12 @@ -22,9 +22,12 @@
    1.13    (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close>
    1.14  
    1.15  setup \<open>Sign.add_const_constraint
    1.16 +  (@{const_name uniformity}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
    1.17 +
    1.18 +setup \<open>Sign.add_const_constraint
    1.19    (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
    1.20  
    1.21 -class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
    1.22 +class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
    1.23    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    1.24    assumes inner_commute: "inner x y = inner y x"
    1.25    and inner_add_left: "inner (x + y) z = inner x z + inner y z"
    1.26 @@ -166,7 +169,7 @@
    1.27    by (metis inner_commute inner_divide_left)
    1.28  
    1.29  text \<open>
    1.30 -  Re-enable constraints for @{term "open"},
    1.31 +  Re-enable constraints for @{term "open"}, @{term "uniformity"},
    1.32    @{term dist}, and @{term norm}.
    1.33  \<close>
    1.34  
    1.35 @@ -174,6 +177,9 @@
    1.36    (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
    1.37  
    1.38  setup \<open>Sign.add_const_constraint
    1.39 +  (@{const_name uniformity}, SOME @{typ "('a::uniform_space \<times> 'a) filter"})\<close>
    1.40 +
    1.41 +setup \<open>Sign.add_const_constraint
    1.42    (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
    1.43  
    1.44  setup \<open>Sign.add_const_constraint