add extra type constraints for dist, norm
authorhuffman
Thu Jun 04 16:11:36 2009 -0700 (2009-06-04)
changeset 314462d91b2416de8
parent 31445 c8a474a919a7
child 31447 97bab1ac463e
add extra type constraints for dist, norm
src/HOL/Library/Inner_Product.thy
src/HOL/Library/normarith.ML
src/HOL/RealVector.thy
     1.1 --- a/src/HOL/Library/Inner_Product.thy	Thu Jun 04 14:32:00 2009 -0700
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Thu Jun 04 16:11:36 2009 -0700
     1.3 @@ -10,6 +10,14 @@
     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 +
     1.9 +setup {* Sign.add_const_constraint
    1.10 +  (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"}) *}
    1.11 +
    1.12 +setup {* Sign.add_const_constraint
    1.13 +  (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"}) *}
    1.14 +
    1.15  class real_inner = real_vector + sgn_div_norm + dist_norm + topo_dist +
    1.16    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    1.17    assumes inner_commute: "inner x y = inner y x"
    1.18 @@ -116,6 +124,14 @@
    1.19  
    1.20  end
    1.21  
    1.22 +text {* Re-enable constraints for @{term dist} and @{term norm}. *}
    1.23 +
    1.24 +setup {* Sign.add_const_constraint
    1.25 +  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
    1.26 +
    1.27 +setup {* Sign.add_const_constraint
    1.28 +  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
    1.29 +
    1.30  interpretation inner:
    1.31    bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
    1.32  proof
     2.1 --- a/src/HOL/Library/normarith.ML	Thu Jun 04 14:32:00 2009 -0700
     2.2 +++ b/src/HOL/Library/normarith.ML	Thu Jun 04 16:11:36 2009 -0700
     2.3 @@ -353,7 +353,7 @@
     2.4    val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) []
     2.5    val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
     2.6    val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
     2.7 -  fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: norm) => real"}) t
     2.8 +  fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
     2.9    fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
    2.10    val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns
    2.11    val replace_conv = try_conv (rewrs_conv asl)
     3.1 --- a/src/HOL/RealVector.thy	Thu Jun 04 14:32:00 2009 -0700
     3.2 +++ b/src/HOL/RealVector.thy	Thu Jun 04 16:11:36 2009 -0700
     3.3 @@ -733,6 +733,18 @@
     3.4      using norm_triangle_ineq4 [of "x - z" "y - z"] by simp
     3.5  qed
     3.6  
     3.7 +subsection {* Extra type constraints *}
     3.8 +
     3.9 +text {* Only allow @{term dist} in class @{text metric_space}. *}
    3.10 +
    3.11 +setup {* Sign.add_const_constraint
    3.12 +  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
    3.13 +
    3.14 +text {* Only allow @{term norm} in class @{text real_normed_vector}. *}
    3.15 +
    3.16 +setup {* Sign.add_const_constraint
    3.17 +  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
    3.18 +
    3.19  
    3.20  subsection {* Sign function *}
    3.21