remove lemma stupid_ext
authorhuffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165d26a45f3c835
parent 44155 ae2906662eec
child 44166 d12d89a66742
remove lemma stupid_ext
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 13:24:49 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 09:11:15 2011 -0700
     1.3 @@ -866,7 +866,7 @@
     1.4      obtain g where g: "linear g" "g o op *v A = id" by blast
     1.5      have "matrix g ** A = mat 1"
     1.6        unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
     1.7 -      using g(2) by (simp add: o_def id_def stupid_ext)
     1.8 +      using g(2) by (simp add: fun_eq_iff)
     1.9      then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast}
    1.10    ultimately show ?thesis by blast
    1.11  qed
    1.12 @@ -894,7 +894,7 @@
    1.13      have "A ** (matrix g) = mat 1"
    1.14        unfolding matrix_eq  matrix_vector_mul_lid
    1.15          matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
    1.16 -      using g(2) unfolding o_def stupid_ext[symmetric] id_def
    1.17 +      using g(2) unfolding o_def fun_eq_iff id_def
    1.18        .
    1.19      hence "\<exists>B. A ** (B::real^'m^'n) = mat 1" by blast
    1.20    }
     2.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 11 13:24:49 2011 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 11 09:11:15 2011 -0700
     2.3 @@ -41,9 +41,6 @@
     2.4  end
     2.5  *}
     2.6  
     2.7 -lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
     2.8 -  by auto
     2.9 -
    2.10  lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
    2.11    by (simp add: vec_nth_inject [symmetric] fun_eq_iff)
    2.12