remove duplicate lemma disjoint_iff
authorhuffman
Mon Aug 15 14:50:24 2011 -0700 (2011-08-15)
changeset 44215786876687ef8
parent 44214 1e0414bda9af
child 44216 903bfe95fece
remove duplicate lemma disjoint_iff
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Aug 15 14:29:17 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Aug 15 14:50:24 2011 -0700
     1.3 @@ -272,9 +272,6 @@
     1.4  
     1.5  subsubsection {* Type @{typ "'a \<times> 'b"} *}
     1.6  
     1.7 -lemma disjoint_iff: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
     1.8 -  by auto (* TODO: move elsewhere *)
     1.9 -
    1.10  instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
    1.11  begin
    1.12  
    1.13 @@ -307,7 +304,7 @@
    1.14  next
    1.15    show "DIM('a \<times> 'b) = card (Basis :: ('a \<times> 'b) set)"
    1.16      unfolding dimension_prod_def Basis_prod_def
    1.17 -    by (simp add: card_Un_disjoint disjoint_iff
    1.18 +    by (simp add: card_Un_disjoint disjoint_iff_not_equal
    1.19        card_image inj_on_def dimension_def)
    1.20  next
    1.21    show "basis ` {..<DIM('a \<times> 'b)} = (Basis :: ('a \<times> 'b) set)"
     2.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Aug 15 14:29:17 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Aug 15 14:50:24 2011 -0700
     2.3 @@ -590,7 +590,7 @@
     2.4  next
     2.5    show "DIM('a ^ 'b) = card (Basis :: ('a ^ 'b) set)"
     2.6      unfolding Basis_vec_def dimension_vec_def dimension_def
     2.7 -    by (simp add: card_UN_disjoint [unfolded disjoint_iff]
     2.8 +    by (simp add: card_UN_disjoint [unfolded disjoint_iff_not_equal]
     2.9        axis_eq_axis nonzero_Basis)
    2.10  next
    2.11    show "basis ` {..<DIM('a ^ 'b)} = (Basis :: ('a ^ 'b) set)"