# HG changeset patch # User huffman # Date 1313445024 25200 # Node ID 786876687ef88dea9eb8e5ff1613c7f04021681b # Parent 1e0414bda9af3cb4b6f4a55de4016b8a7245df4d remove duplicate lemma disjoint_iff diff -r 1e0414bda9af -r 786876687ef8 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Aug 15 14:29:17 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Aug 15 14:50:24 2011 -0700 @@ -272,9 +272,6 @@ subsubsection {* Type @{typ "'a \ 'b"} *} -lemma disjoint_iff: "A \ B = {} \ (\x\A. \y\B. x \ y)" - by auto (* TODO: move elsewhere *) - instantiation prod :: (euclidean_space, euclidean_space) euclidean_space begin @@ -307,7 +304,7 @@ next show "DIM('a \ 'b) = card (Basis :: ('a \ 'b) set)" unfolding dimension_prod_def Basis_prod_def - by (simp add: card_Un_disjoint disjoint_iff + by (simp add: card_Un_disjoint disjoint_iff_not_equal card_image inj_on_def dimension_def) next show "basis ` {.. 'b)} = (Basis :: ('a \ 'b) set)" diff -r 1e0414bda9af -r 786876687ef8 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Aug 15 14:29:17 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Aug 15 14:50:24 2011 -0700 @@ -590,7 +590,7 @@ next show "DIM('a ^ 'b) = card (Basis :: ('a ^ 'b) set)" unfolding Basis_vec_def dimension_vec_def dimension_def - by (simp add: card_UN_disjoint [unfolded disjoint_iff] + by (simp add: card_UN_disjoint [unfolded disjoint_iff_not_equal] axis_eq_axis nonzero_Basis) next show "basis ` {..