--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Thu Jun 28 14:13:57 2018 +0100
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Thu Jun 28 14:14:05 2018 +0100
@@ -596,11 +596,11 @@
and lt_module_hom_id = module.module_hom_id
and lt_module_hom_ident = module.module_hom_ident
and lt_module_hom_uminus = module.module_hom_uminus
- and subspace_UNIV = module.subspace_UNIV
- and span_alt = module.span_alt
+ and lt_subspace_UNIV = module.subspace_UNIV
(* should work but don't:
and span_def = module.span_def
and span_UNIV = module.span_UNIV
+ and lt_span_alt = module.span_alt
and dependent_alt = module.dependent_alt
and independent_alt = module.independent_alt
and unique_representation = module.unique_representation
@@ -701,7 +701,7 @@
and module_hom_id = lt_module_hom_id
and module_hom_ident = lt_module_hom_ident
and module_hom_uminus = lt_module_hom_uminus
-
+ and subspace_UNIV = lt_subspace_UNIV
end
subsubsection \<open>Vector Spaces\<close>
@@ -715,10 +715,10 @@
lemmas_with [var_simplified explicit_ab_group_add,
unoverload_type 'd,
OF type.ab_group_add_axioms type_vector_space_on_with,
+ folded dim_S_def,
untransferred,
var_simplified implicit_ab_group_add]:
- lt_vector_space_assms = vector_space.vector_space_assms
-and lt_linear_id = vector_space.linear_id
+ lt_linear_id = vector_space.linear_id
and lt_linear_ident = vector_space.linear_ident
and lt_linear_scale_self = vector_space.linear_scale_self
and lt_linear_scale_left = vector_space.linear_scale_left
@@ -749,13 +749,10 @@
and lt_independent_explicit_finite_subsets = vector_space.independent_explicit_finite_subsets
and lt_independent_if_scalars_zero = vector_space.independent_if_scalars_zero
and lt_subspace_sums = vector_space.subspace_sums
-(* should work but don't:
-and lt_injective_scale = vector_space.lt_injective_scale
-and lt_bij_if_span_eq_span_bases = vector_space.bij_if_span_eq_span_bases
-and lt_dim_def = vector_space.dim_def
+and lt_dim_unique = vector_space.dim_unique
and lt_dim_eq_card = vector_space.dim_eq_card
and lt_basis_card_eq_dim = vector_space.basis_card_eq_dim
-and lt_basis_exists["consumes" - 1, "case_names" "1"] = vector_space.basis_exists
+and lt_basis_exists = vector_space.basis_exists
and lt_dim_eq_card_independent = vector_space.dim_eq_card_independent
and lt_dim_span = vector_space.dim_span
and lt_dim_span_eq_card_independent = vector_space.dim_span_eq_card_independent
@@ -763,10 +760,12 @@
and lt_span_eq_dim = vector_space.span_eq_dim
and lt_dim_le_card' = vector_space.dim_le_card'
and lt_span_card_ge_dim = vector_space.span_card_ge_dim
-and lt_dim_unique = vector_space.dim_unique
-and lt_dim_with = vector_space.dim_with
+and lt_dim_with = vector_space.dim_with
+(* should work but don't:
+and lt_bij_if_span_eq_span_bases = vector_space.bij_if_span_eq_span_bases
*)
(* not expected to work:
+and lt_dim_def = vector_space.dim_def
and lt_extend_basis_superset = vector_space.extend_basis_superset
and lt_independent_extend_basis = vector_space.independent_extend_basis
and lt_span_extend_basis = vector_space.span_extend_basis
@@ -779,8 +778,7 @@
folded subset_iff',
simplified pred_fun_def,
simplified\<comment>\<open>too much?\<close>]:
- vector_space_assms = lt_vector_space_assms
-and linear_id = lt_linear_id
+ linear_id = lt_linear_id
and linear_ident = lt_linear_ident
and linear_scale_self = lt_linear_scale_self
and linear_scale_left = lt_linear_scale_left
@@ -810,6 +808,18 @@
and independent_explicit_finite_subsets = lt_independent_explicit_finite_subsets
and independent_if_scalars_zero = lt_independent_if_scalars_zero
and subspace_sums = lt_subspace_sums
+and dim_unique = lt_dim_unique
+and dim_eq_card = lt_dim_eq_card
+and basis_card_eq_dim = lt_basis_card_eq_dim
+and basis_exists["consumes" - 1, "case_names" "1"] = lt_basis_exists
+and dim_eq_card_independent = lt_dim_eq_card_independent
+and dim_span = lt_dim_span
+and dim_span_eq_card_independent = lt_dim_span_eq_card_independent
+and dim_le_card = lt_dim_le_card
+and span_eq_dim = lt_span_eq_dim
+and dim_le_card' = lt_dim_le_card'
+and span_card_ge_dim = lt_span_card_ge_dim
+and dim_with = lt_dim_with
end
@@ -869,37 +879,34 @@
folded subset_iff',
simplified pred_fun_def,
simplified\<comment>\<open>too much?\<close>]:
- vector_space_assms = lt_vector_space_assms
-and linear_id = lt_linear_id
-and linear_ident = lt_linear_ident
-and linear_scale_self = lt_linear_scale_self
-and linear_scale_left = lt_linear_scale_left
-and linear_uminus = lt_linear_uminus
-and linear_imp_scale["consumes" - 1, "case_names" "1"] = lt_linear_imp_scale
-and scale_eq_0_iff = lt_scale_eq_0_iff
-and scale_left_imp_eq = lt_scale_left_imp_eq
-and scale_right_imp_eq = lt_scale_right_imp_eq
-and scale_cancel_left = lt_scale_cancel_left
-and scale_cancel_right = lt_scale_cancel_right
-and dependent_def = lt_dependent_def
-and dependent_single = lt_dependent_single
-and in_span_insert = lt_in_span_insert
-and dependent_insertD = lt_dependent_insertD
-and independent_insertI = lt_independent_insertI
-and independent_insert = lt_independent_insert
-and maximal_independent_subset_extend["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset_extend
-and maximal_independent_subset["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset
-and in_span_delete = lt_in_span_delete
-and span_redundant = lt_span_redundant
-and span_trans = lt_span_trans
-and span_insert_0 = lt_span_insert_0
-and span_delete_0 = lt_span_delete_0
-and span_image_scale = lt_span_image_scale
-and exchange_lemma = lt_exchange_lemma
-and independent_span_bound = lt_independent_span_bound
-and independent_explicit_finite_subsets = lt_independent_explicit_finite_subsets
-and independent_if_scalars_zero = lt_independent_if_scalars_zero
-and subspace_sums = lt_subspace_sums
+ finiteI_independent = lt_finiteI_independent
+and dim_empty = lt_dim_empty
+and dim_insert = lt_dim_insert
+and dim_singleton = lt_dim_singleton
+and choose_subspace_of_subspace["consumes" - 1, "case_names" "1"] = lt_choose_subspace_of_subspace
+and basis_subspace_exists["consumes" - 1, "case_names" "1"] = lt_basis_subspace_exists
+and dim_mono = lt_dim_mono
+and dim_subset = lt_dim_subset
+and dim_eq_0 = lt_dim_eq_0
+and dim_UNIV = lt_dim_UNIV
+and independent_card_le_dim = lt_independent_card_le_dim
+and card_ge_dim_independent = lt_card_ge_dim_independent
+and card_le_dim_spanning = lt_card_le_dim_spanning
+and card_eq_dim = lt_card_eq_dim
+and subspace_dim_equal = lt_subspace_dim_equal
+and dim_eq_span = lt_dim_eq_span
+and dim_psubset = lt_dim_psubset
+and indep_card_eq_dim_span = lt_indep_card_eq_dim_span
+and independent_bound_general = lt_independent_bound_general
+and independent_explicit = lt_independent_explicit
+and dim_sums_Int = lt_dim_sums_Int
+and dependent_biggerset_general = lt_dependent_biggerset_general
+and subset_le_dim = lt_subset_le_dim
+and linear_inj_imp_surj = lt_linear_inj_imp_surj
+and linear_surj_imp_inj = lt_linear_surj_imp_inj
+and linear_inverse_left = lt_linear_inverse_left
+and left_inverse_linear = lt_left_inverse_linear
+and right_inverse_linear = lt_right_inverse_linear
end