# HG changeset patch
# User immler
# Date 1387210102 -3600
# Node ID d9edb711ef31474661aa958f6bca1aaf3cc259e1
# Parent  13f08c876899cf699a00f87a4d4267d80d7c9bdb
pragmatic executability of instance prod::{open,dist,norm}

diff -r 13f08c876899 -r d9edb711ef31 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -44,7 +44,7 @@
 instantiation prod :: (topological_space, topological_space) topological_space
 begin
 
-definition open_prod_def:
+definition open_prod_def[code del]:
   "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
     (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)"
 
@@ -87,6 +87,8 @@
 
 end
 
+code_abort "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"
+
 lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)"
 unfolding open_prod_def by auto
 
@@ -257,7 +259,7 @@
 instantiation prod :: (metric_space, metric_space) metric_space
 begin
 
-definition dist_prod_def:
+definition dist_prod_def[code del]:
   "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
 
 lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
@@ -344,6 +346,8 @@
 
 end
 
+code_abort "dist::('a::metric_space*'b::metric_space)\<Rightarrow>('a*'b) \<Rightarrow> real"
+
 lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
   unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
 
@@ -388,7 +392,7 @@
 instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
 begin
 
-definition norm_prod_def:
+definition norm_prod_def[code del]:
   "norm x = sqrt ((norm (fst x))\<^sup>2 + (norm (snd x))\<^sup>2)"
 
 definition sgn_prod_def:
@@ -422,6 +426,8 @@
 
 end
 
+code_abort "norm::('a::real_normed_vector*'b::real_normed_vector) \<Rightarrow> real"
+
 instance prod :: (banach, banach) banach ..
 
 subsubsection {* Pair operations are linear *}