# HG changeset patch
# User immler
# Date 1530186542 -7200
# Node ID f1f989b656bb6d0842d03d73161f88c6df29afd3
# Parent  e980a0441b61d3508d13d6ab08d2300a8ad02b81
transfer more lemmas

diff -r e980a0441b61 -r f1f989b656bb src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Thu Jun 28 13:18:02 2018 +0200
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Thu Jun 28 13:49:02 2018 +0200
@@ -715,6 +715,7 @@
 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_linear_id = vector_space.linear_id
@@ -748,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
@@ -762,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
@@ -808,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