author nipkow Wed, 16 Jan 2019 11:48:06 +0100 changeset 69666 d51e5e41fafe parent 69665 60110f6d0b4e child 69667 82bb6225588b child 69670 114ae60c4be7
Reorg of material
```--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Jan 16 10:27:57 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Jan 16 11:48:06 2019 +0100
@@ -187,31 +187,6 @@
shows "A ** transpose A = (\<chi> i j. inner (row i A) (row j A))"
by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)

-text\<open>Two sometimes fruitful ways of looking at matrix-vector multiplication.\<close>
-
-lemma%important matrix_mult_dot: "A *v x = (\<chi> i. inner (A\$i) x)"
-  by (simp add: matrix_vector_mult_def inner_vec_def)
-
-lemma%unimportant adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
-  apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
-    sum_distrib_right sum_distrib_left)
-  apply (subst sum.swap)
-  done
-
-lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
-  shows "matrix(adjoint f) = transpose(matrix f)"
-proof%unimportant -
-  also have "\<dots> = transpose(matrix f)"
-    apply rule
-    done
-  finally show ?thesis .
-qed
-
lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
using matrix_vector_mul_linear[of A]
@@ -703,16 +678,6 @@
then show "?A \<subseteq> vec.span ?B" by auto
qed (simp add: card_image inj_on_def axis_eq_axis)

-lemma%unimportant dim_subset_UNIV_cart_gen:
-  fixes S :: "('a::field^'n) set"
-  shows "vec.dim S \<le> CARD('n)"
-  by (metis vec.dim_eq_full vec.dim_subset_UNIV vec.span_UNIV vec_dim_card)
-
-lemma%unimportant dim_subset_UNIV_cart:
-  fixes S :: "(real^'n) set"
-  shows "dim S \<le> CARD('n)"
-  using dim_subset_UNIV_cart_gen[of S] by (simp add: dim_vec_eq)
-
lemma%unimportant affinity_inverses:
assumes m0: "m \<noteq> (0::'a::field)"
shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
@@ -813,13 +778,7 @@
vector_cart[of "\<lambda>j. frechet_derivative f (at x) j \$ k"]
by (simp add: Basis_vec_def axis_eq_axis inner_axis jacobian_def matrix_def)

-subsection%unimportant \<open>Lemmas for working on \<^typ>\<open>real^1\<close>\<close>
-
-lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
-  by (metis (full_types) num1_eq_iff)
-
-lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
-  by auto (metis (full_types) num1_eq_iff)
+subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3\<close>\<close>

lemma exhaust_2:
fixes x :: 2
@@ -865,24 +824,6 @@
lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
unfolding UNIV_3 by (simp add: ac_simps)

-lemma num1_eqI:
-  fixes a::num1 shows "a = b"
-  by (metis (full_types) UNIV_1 UNIV_I empty_iff insert_iff)
-
-lemma num1_eq1 [simp]:
-  fixes a::num1 shows "a = 1"
-  by (rule num1_eqI)
-
-instantiation num1 :: linorder begin
-definition "a < b \<longleftrightarrow> Rep_num1 a < Rep_num1 b"
-definition "a \<le> b \<longleftrightarrow> Rep_num1 a \<le> Rep_num1 b"
-instance
-  by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI)
-end
-
-instance num1 :: wellorder
-  by intro_classes (auto simp: less_eq_num1_def less_num1_def)
-
subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close>

lemma vector_one: "(x::'a ^1) = (\<chi> i. (x\$1))"
@@ -908,171 +849,6 @@
lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x\$1) - (y\$1)\<bar>"
by (auto simp add: norm_real dist_norm)

-subsection%important\<open> Rank of a matrix\<close>
-
-text\<open>Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\<close>
-
-lemma%unimportant matrix_vector_mult_in_columnspace_gen:
-  fixes A :: "'a::field^'n^'m"
-  shows "(A *v x) \<in> vec.span(columns A)"
-  apply (simp add: matrix_vector_column columns_def transpose_def column_def)
-  apply (intro vec.span_sum vec.span_scale)
-  apply (force intro: vec.span_base)
-  done
-
-lemma%unimportant matrix_vector_mult_in_columnspace:
-  fixes A :: "real^'n^'m"
-  shows "(A *v x) \<in> span(columns A)"
-  using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq)
-
-lemma%important orthogonal_nullspace_rowspace:
-  fixes A :: "real^'n^'m"
-  assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)"
-  shows "orthogonal x y"
-  using y
-proof%unimportant (induction rule: span_induct)
-  case base
-  then show ?case
-next
-  case (step v)
-  then obtain i where "v = row i A"
-    by (auto simp: rows_def)
-  with 0 show ?case
-    unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def
-    by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index)
-qed
-
-lemma%unimportant nullspace_inter_rowspace:
-  fixes A :: "real^'n^'m"
-  shows "A *v x = 0 \<and> x \<in> span(rows A) \<longleftrightarrow> x = 0"
-  using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right
-  by blast
-
-lemma%unimportant matrix_vector_mul_injective_on_rowspace:
-  fixes A :: "real^'n^'m"
-  shows "\<lbrakk>A *v x = A *v y; x \<in> span(rows A); y \<in> span(rows A)\<rbrakk> \<Longrightarrow> x = y"
-  using nullspace_inter_rowspace [of A "x-y"]
-  by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff)
-
-definition%important rank :: "'a::field^'n^'m=>nat"
-  where row_rank_def_gen: "rank A \<equiv> vec.dim(rows A)"
-
-lemma%important row_rank_def: "rank A = dim (rows A)" for A::"real^'n^'m"
-  by%unimportant (auto simp: row_rank_def_gen dim_vec_eq)
-
-lemma%important dim_rows_le_dim_columns:
-  fixes A :: "real^'n^'m"
-  shows "dim(rows A) \<le> dim(columns A)"
-proof%unimportant -
-  have "dim (span (rows A)) \<le> dim (span (columns A))"
-  proof -
-    obtain B where "independent B" "span(rows A) \<subseteq> span B"
-              and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))"
-      using basis_exists [of "span(rows A)"] by metis
-    with span_subspace have eq: "span B = span(rows A)"
-      by auto
-    then have inj: "inj_on ((*v) A) (span B)"
-      by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace)
-    then have ind: "independent ((*v) A ` B)"
-      by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>])
-    have "dim (span (rows A)) \<le> card ((*v) A ` B)"
-      unfolding B(2)[symmetric]
-      using inj
-      by (auto simp: card_image inj_on_subset span_superset)
-    also have "\<dots> \<le> dim (span (columns A))"
-      using _ ind
-      by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace)
-    finally show ?thesis .
-  qed
-  then show ?thesis
-qed
-
-lemma%unimportant column_rank_def:
-  fixes A :: "real^'n^'m"
-  shows "rank A = dim(columns A)"
-  unfolding row_rank_def
-  by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose)
-
-lemma%unimportant rank_transpose:
-  fixes A :: "real^'n^'m"
-  shows "rank(transpose A) = rank A"
-  by (metis column_rank_def row_rank_def rows_transpose)
-
-lemma%unimportant matrix_vector_mult_basis:
-  fixes A :: "real^'n^'m"
-  shows "A *v (axis k 1) = column k A"
-  by (simp add: cart_eq_inner_axis column_def matrix_mult_dot)
-
-lemma%unimportant columns_image_basis:
-  fixes A :: "real^'n^'m"
-  shows "columns A = (*v) A ` (range (\<lambda>i. axis i 1))"
-  by (force simp: columns_def matrix_vector_mult_basis [symmetric])
-
-lemma%important rank_dim_range:
-  fixes A :: "real^'n^'m"
-  shows "rank A = dim(range (\<lambda>x. A *v x))"
-  unfolding column_rank_def
-proof%unimportant (rule span_eq_dim)
-  have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r")
-    by (simp add: columns_image_basis image_subsetI span_mono)
-  then show "?l = ?r"
-    by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace
-        span_eq span_span)
-qed
-
-lemma%unimportant rank_bound:
-  fixes A :: "real^'n^'m"
-  shows "rank A \<le> min CARD('m) (CARD('n))"
-  by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff
-      column_rank_def row_rank_def)
-
-lemma%unimportant full_rank_injective:
-  fixes A :: "real^'n^'m"
-  shows "rank A = CARD('n) \<longleftrightarrow> inj ((*v) A)"
-  by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def
-      dim_eq_full [symmetric] card_cart_basis vec.dimension_def)
-
-lemma%unimportant full_rank_surjective:
-  fixes A :: "real^'n^'m"
-  shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)"
-  by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
-                matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
-
-lemma%unimportant rank_I: "rank(mat 1::real^'n^'n) = CARD('n)"
-  by (simp add: full_rank_injective inj_on_def)
-
-lemma%unimportant less_rank_noninjective:
-  fixes A :: "real^'n^'m"
-  shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)"
-using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
-
-lemma%unimportant matrix_nonfull_linear_equations_eq:
-  fixes A :: "real^'n^'m"
-  shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> rank A \<noteq> CARD('n)"
-  by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker)
-
-lemma%unimportant rank_eq_0: "rank A = 0 \<longleftrightarrow> A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0"
-  for A :: "real^'n^'m"
-  by (auto simp: rank_dim_range matrix_eq)
-
-lemma%important rank_mul_le_right:
-  fixes A :: "real^'n^'m" and B :: "real^'p^'n"
-  shows "rank(A ** B) \<le> rank B"
-proof%unimportant -
-  have "rank(A ** B) \<le> dim ((*v) A ` range ((*v) B))"
-    by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc)
-  also have "\<dots> \<le> rank B"
-    by (simp add: rank_dim_range dim_image_le)
-  finally show ?thesis .
-qed
-
-lemma%unimportant rank_mul_le_left:
-  fixes A :: "real^'n^'m" and B :: "real^'p^'n"
-  shows "rank(A ** B) \<le> rank A"
-  by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
-
subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close>

lemma vector_one_nth [simp]:```
```--- a/src/HOL/Analysis/Cartesian_Space.thy	Wed Jan 16 10:27:57 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Wed Jan 16 11:48:06 2019 +0100
@@ -462,4 +462,209 @@
lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1"
unfolding vector_space_over_itself.dimension_def by simp

+
+lemma%unimportant dim_subset_UNIV_cart_gen:
+  fixes S :: "('a::field^'n) set"
+  shows "vec.dim S \<le> CARD('n)"
+  by (metis vec.dim_eq_full vec.dim_subset_UNIV vec.span_UNIV vec_dim_card)
+
+lemma%unimportant dim_subset_UNIV_cart:
+  fixes S :: "(real^'n) set"
+  shows "dim S \<le> CARD('n)"
+  using dim_subset_UNIV_cart_gen[of S] by (simp add: dim_vec_eq)
+
+text\<open>Two sometimes fruitful ways of looking at matrix-vector multiplication.\<close>
+
+lemma%important matrix_mult_dot: "A *v x = (\<chi> i. inner (A\$i) x)"
+  by (simp add: matrix_vector_mult_def inner_vec_def)
+
+lemma%unimportant adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
+  apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
+    sum_distrib_right sum_distrib_left)
+  apply (subst sum.swap)
+  done
+
+lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
+  shows "matrix(adjoint f) = transpose(matrix f)"
+proof%unimportant -
+  also have "\<dots> = transpose(matrix f)"
+    apply rule
+    done
+  finally show ?thesis .
+qed
+
+
+subsection%important\<open> Rank of a matrix\<close>
+
+text\<open>Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\<close>
+
+lemma%unimportant matrix_vector_mult_in_columnspace_gen:
+  fixes A :: "'a::field^'n^'m"
+  shows "(A *v x) \<in> vec.span(columns A)"
+  apply (simp add: matrix_vector_column columns_def transpose_def column_def)
+  apply (intro vec.span_sum vec.span_scale)
+  apply (force intro: vec.span_base)
+  done
+
+lemma%unimportant matrix_vector_mult_in_columnspace:
+  fixes A :: "real^'n^'m"
+  shows "(A *v x) \<in> span(columns A)"
+  using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq)
+
+lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}"
+  by (simp add: subspace_def orthogonal_clauses)
+
+lemma%important orthogonal_nullspace_rowspace:
+  fixes A :: "real^'n^'m"
+  assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)"
+  shows "orthogonal x y"
+  using y
+proof%unimportant (induction rule: span_induct)
+  case base
+  then show ?case
+next
+  case (step v)
+  then obtain i where "v = row i A"
+    by (auto simp: rows_def)
+  with 0 show ?case
+    unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def
+    by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index)
+qed
+
+lemma%unimportant nullspace_inter_rowspace:
+  fixes A :: "real^'n^'m"
+  shows "A *v x = 0 \<and> x \<in> span(rows A) \<longleftrightarrow> x = 0"
+  using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right
+  by blast
+
+lemma%unimportant matrix_vector_mul_injective_on_rowspace:
+  fixes A :: "real^'n^'m"
+  shows "\<lbrakk>A *v x = A *v y; x \<in> span(rows A); y \<in> span(rows A)\<rbrakk> \<Longrightarrow> x = y"
+  using nullspace_inter_rowspace [of A "x-y"]
+  by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff)
+
+definition%important rank :: "'a::field^'n^'m=>nat"
+  where row_rank_def_gen: "rank A \<equiv> vec.dim(rows A)"
+
+lemma%important row_rank_def: "rank A = dim (rows A)" for A::"real^'n^'m"
+  by%unimportant (auto simp: row_rank_def_gen dim_vec_eq)
+
+lemma%important dim_rows_le_dim_columns:
+  fixes A :: "real^'n^'m"
+  shows "dim(rows A) \<le> dim(columns A)"
+proof%unimportant -
+  have "dim (span (rows A)) \<le> dim (span (columns A))"
+  proof -
+    obtain B where "independent B" "span(rows A) \<subseteq> span B"
+              and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))"
+      using basis_exists [of "span(rows A)"] by metis
+    with span_subspace have eq: "span B = span(rows A)"
+      by auto
+    then have inj: "inj_on ((*v) A) (span B)"
+      by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace)
+    then have ind: "independent ((*v) A ` B)"
+      by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>])
+    have "dim (span (rows A)) \<le> card ((*v) A ` B)"
+      unfolding B(2)[symmetric]
+      using inj
+      by (auto simp: card_image inj_on_subset span_superset)
+    also have "\<dots> \<le> dim (span (columns A))"
+      using _ ind
+      by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace)
+    finally show ?thesis .
+  qed
+  then show ?thesis
+qed
+
+lemma%unimportant column_rank_def:
+  fixes A :: "real^'n^'m"
+  shows "rank A = dim(columns A)"
+  unfolding row_rank_def
+  by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose)
+
+lemma%unimportant rank_transpose:
+  fixes A :: "real^'n^'m"
+  shows "rank(transpose A) = rank A"
+  by (metis column_rank_def row_rank_def rows_transpose)
+
+lemma%unimportant matrix_vector_mult_basis:
+  fixes A :: "real^'n^'m"
+  shows "A *v (axis k 1) = column k A"
+  by (simp add: cart_eq_inner_axis column_def matrix_mult_dot)
+
+lemma%unimportant columns_image_basis:
+  fixes A :: "real^'n^'m"
+  shows "columns A = (*v) A ` (range (\<lambda>i. axis i 1))"
+  by (force simp: columns_def matrix_vector_mult_basis [symmetric])
+
+lemma%important rank_dim_range:
+  fixes A :: "real^'n^'m"
+  shows "rank A = dim(range (\<lambda>x. A *v x))"
+  unfolding column_rank_def
+proof%unimportant (rule span_eq_dim)
+  have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r")
+    by (simp add: columns_image_basis image_subsetI span_mono)
+  then show "?l = ?r"
+    by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace
+        span_eq span_span)
+qed
+
+lemma%unimportant rank_bound:
+  fixes A :: "real^'n^'m"
+  shows "rank A \<le> min CARD('m) (CARD('n))"
+  by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff
+      column_rank_def row_rank_def)
+
+lemma%unimportant full_rank_injective:
+  fixes A :: "real^'n^'m"
+  shows "rank A = CARD('n) \<longleftrightarrow> inj ((*v) A)"
+  by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def
+      dim_eq_full [symmetric] card_cart_basis vec.dimension_def)
+
+lemma%unimportant full_rank_surjective:
+  fixes A :: "real^'n^'m"
+  shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)"
+  by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
+                matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
+
+lemma%unimportant rank_I: "rank(mat 1::real^'n^'n) = CARD('n)"
+  by (simp add: full_rank_injective inj_on_def)
+
+lemma%unimportant less_rank_noninjective:
+  fixes A :: "real^'n^'m"
+  shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)"
+using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
+
+lemma%unimportant matrix_nonfull_linear_equations_eq:
+  fixes A :: "real^'n^'m"
+  shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> rank A \<noteq> CARD('n)"
+  by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker)
+
+lemma%unimportant rank_eq_0: "rank A = 0 \<longleftrightarrow> A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0"
+  for A :: "real^'n^'m"
+  by (auto simp: rank_dim_range matrix_eq)
+
+lemma%important rank_mul_le_right:
+  fixes A :: "real^'n^'m" and B :: "real^'p^'n"
+  shows "rank(A ** B) \<le> rank B"
+proof%unimportant -
+  have "rank(A ** B) \<le> dim ((*v) A ` range ((*v) B))"
+    by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc)
+  also have "\<dots> \<le> rank B"
+    by (simp add: rank_dim_range dim_image_le)
+  finally show ?thesis .
+qed
+
+lemma%unimportant rank_mul_le_left:
+  fixes A :: "real^'n^'m" and B :: "real^'p^'n"
+  shows "rank(A ** B) \<le> rank A"
+  by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
+
end
\ No newline at end of file```
```--- a/src/HOL/Library/Numeral_Type.thy	Wed Jan 16 10:27:57 2019 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Jan 16 11:48:06 2019 +0100
@@ -45,6 +45,8 @@
unfolding type_definition.card [OF type_definition_bit1]
by simp

+subsection \<open>@{typ num1}\<close>
+
instance num1 :: finite
proof
show "finite (UNIV::num1 set)"
@@ -62,6 +64,42 @@

end

+lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
+  by (induct x, induct y) simp
+
+instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}"
+begin
+
+instance
+  by standard (simp_all add: num1_eq_iff)
+
+end
+
+lemma num1_eqI:
+  fixes a::num1 shows "a = b"
+
+lemma num1_eq1 [simp]:
+  fixes a::num1 shows "a = 1"
+  by (rule num1_eqI)
+
+lemma forall_1[simp]: "(\<forall>i::num1. P i) \<longleftrightarrow> P 1"
+  by (metis (full_types) num1_eq_iff)
+
+lemma ex_1[simp]: "(\<exists>x::num1. P x) \<longleftrightarrow> P 1"
+  by auto (metis (full_types) num1_eq_iff)
+
+instantiation num1 :: linorder begin
+definition "a < b \<longleftrightarrow> Rep_num1 a < Rep_num1 b"
+definition "a \<le> b \<longleftrightarrow> Rep_num1 a \<le> Rep_num1 b"
+instance
+  by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI)
+end
+
+instance num1 :: wellorder
+  by intro_classes (auto simp: less_eq_num1_def less_num1_def)
+
+
instance bit0 :: (finite) card2
proof
show "finite (UNIV::'a bit0 set)"
@@ -195,17 +233,6 @@
\<^typ>\<open>num1\<close>, since 0 and 1 are not distinct.
\<close>

-instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}"
-begin
-
-lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
-  by (induct x, induct y) simp
-
-instance
-  by standard (simp_all add: num1_eq_iff)
-
-end
-
instantiation
bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}"
begin
@@ -360,8 +387,7 @@
definition "enum_class.enum_ex P = P (1 :: num1)"
instance
by intro_classes
-     (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def,
-      (metis (full_types) num1_eq_iff)+)
+     (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def)
end

instantiation num0 and num1 :: card_UNIV begin```