--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Jan 17 16:08:41 2019 +0000
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Jan 17 16:22:21 2019 -0500
@@ -259,32 +259,20 @@
text\<open>The ordering on one-dimensional vectors is linear.\<close>
-class cart_one =
- assumes UNIV_one: "card (UNIV :: 'a set) = Suc 0"
-begin
-
-subclass finite
-proof
- from UNIV_one show "finite (UNIV :: 'a set)"
- by (auto intro!: card_ge_0_finite)
-qed
-
-end
-
instance vec:: (order, finite) order
by standard (auto simp: less_eq_vec_def less_vec_def vec_eq_iff
intro: order.trans order.antisym order.strict_implies_order)
-instance vec :: (linorder, cart_one) linorder
+instance vec :: (linorder, CARD_1) linorder
proof
obtain a :: 'b where all: "\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a"
proof -
- have "card (UNIV :: 'b set) = Suc 0" by (rule UNIV_one)
+ have "CARD ('b) = 1" by (rule CARD_1)
then obtain b :: 'b where "UNIV = {b}" by (auto iff: card_Suc_eq)
then have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P b" by auto
then show thesis by (auto intro: that)
qed
- fix x y :: "'a^'b::cart_one"
+ fix x y :: "'a^'b::CARD_1"
note [simp] = less_eq_vec_def less_vec_def all vec_eq_iff field_simps
show "x \<le> y \<or> y \<le> x" by auto
qed
@@ -638,7 +626,7 @@
lemma%unimportant norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
by (simp add: norm_vec_def L2_set_le_sum)
-lemma%unimportant bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
+lemma%unimportant bounded_linear_vec_nth[intro]: "bounded_linear (\<lambda>x. x $ i)"
apply standard
apply (rule vector_add_component)
apply (rule vector_scaleR_component)