# HG changeset patch
# User huffman
# Date 1244157096 25200
# Node ID 2d91b2416de842a462fa356ca090209d01a852a8
# Parent  c8a474a919a70608984cb6e940a4fe345e565e96
add extra type constraints for dist, norm

diff -r c8a474a919a7 -r 2d91b2416de8 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Thu Jun 04 14:32:00 2009 -0700
+++ b/src/HOL/Library/Inner_Product.thy	Thu Jun 04 16:11:36 2009 -0700
@@ -10,6 +10,14 @@
 
 subsection {* Real inner product spaces *}
 
+text {* Temporarily relax constraints for @{term dist} and @{term norm}. *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"}) *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"}) *}
+
 class real_inner = real_vector + sgn_div_norm + dist_norm + topo_dist +
   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
   assumes inner_commute: "inner x y = inner y x"
@@ -116,6 +124,14 @@
 
 end
 
+text {* Re-enable constraints for @{term dist} and @{term norm}. *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
+
 interpretation inner:
   bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
 proof
diff -r c8a474a919a7 -r 2d91b2416de8 src/HOL/Library/normarith.ML
--- a/src/HOL/Library/normarith.ML	Thu Jun 04 14:32:00 2009 -0700
+++ b/src/HOL/Library/normarith.ML	Thu Jun 04 16:11:36 2009 -0700
@@ -353,7 +353,7 @@
   val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) []
   val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
   val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
-  fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: norm) => real"}) t
+  fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   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
   val replace_conv = try_conv (rewrs_conv asl)
diff -r c8a474a919a7 -r 2d91b2416de8 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Thu Jun 04 14:32:00 2009 -0700
+++ b/src/HOL/RealVector.thy	Thu Jun 04 16:11:36 2009 -0700
@@ -733,6 +733,18 @@
     using norm_triangle_ineq4 [of "x - z" "y - z"] by simp
 qed
 
+subsection {* Extra type constraints *}
+
+text {* Only allow @{term dist} in class @{text metric_space}. *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
+
+text {* Only allow @{term norm} in class @{text real_normed_vector}. *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
+
 
 subsection {* Sign function *}