src/HOL/Library/Inner_Product.thy
changeset 31492 5400beeddb55
parent 31446 2d91b2416de8
child 31590 776d6a4c1327
     1.1 --- a/src/HOL/Library/Inner_Product.thy	Sun Jun 07 15:18:52 2009 -0700
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Sun Jun 07 17:59:54 2009 -0700
     1.3 @@ -10,7 +10,13 @@
     1.4  
     1.5  subsection {* Real inner product spaces *}
     1.6  
     1.7 -text {* Temporarily relax constraints for @{term dist} and @{term norm}. *}
     1.8 +text {*
     1.9 +  Temporarily relax type constraints for @{term "open"},
    1.10 +  @{term dist}, and @{term norm}.
    1.11 +*}
    1.12 +
    1.13 +setup {* Sign.add_const_constraint
    1.14 +  (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"}) *}
    1.15  
    1.16  setup {* Sign.add_const_constraint
    1.17    (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"}) *}
    1.18 @@ -18,7 +24,7 @@
    1.19  setup {* Sign.add_const_constraint
    1.20    (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"}) *}
    1.21  
    1.22 -class real_inner = real_vector + sgn_div_norm + dist_norm + topo_dist +
    1.23 +class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
    1.24    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    1.25    assumes inner_commute: "inner x y = inner y x"
    1.26    and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
    1.27 @@ -124,7 +130,13 @@
    1.28  
    1.29  end
    1.30  
    1.31 -text {* Re-enable constraints for @{term dist} and @{term norm}. *}
    1.32 +text {*
    1.33 +  Re-enable constraints for @{term "open"},
    1.34 +  @{term dist}, and @{term norm}.
    1.35 +*}
    1.36 +
    1.37 +setup {* Sign.add_const_constraint
    1.38 +  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *}
    1.39  
    1.40  setup {* Sign.add_const_constraint
    1.41    (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}