# HG changeset patch
# User paulson
# Date 1531499225 -3600
# Node ID e371784becd90beb607aa34011e046db1b95383d
# Parent  b942da0962c25b78202fa13ff5a255dc9393cd02# Parent  330c0ec897a463c0cea878bcc877d4a60d241dc5
merged

diff -r b942da0962c2 -r e371784becd9 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Jul 13 15:42:18 2018 +0200
+++ b/src/HOL/Divides.thy	Fri Jul 13 17:27:05 2018 +0100
@@ -26,16 +26,17 @@
     simp add: ac_simps sgn_1_pos sgn_1_neg)
 
 lemma unique_quotient_lemma:
-  "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
-apply (subgoal_tac "r' + b * (q'-q) \<le> r")
- prefer 2 apply (simp add: right_diff_distrib)
-apply (subgoal_tac "0 < b * (1 + q - q') ")
-apply (erule_tac [2] order_le_less_trans)
- prefer 2 apply (simp add: right_diff_distrib distrib_left)
-apply (subgoal_tac "b * q' < b * (1 + q) ")
- prefer 2 apply (simp add: right_diff_distrib distrib_left)
-apply (simp add: mult_less_cancel_left)
-done
+  assumes "b * q' + r' \<le> b * q + r" "0 \<le> r'" "r' < b" "r < b" shows "q' \<le> (q::int)"
+proof -
+  have "r' + b * (q'-q) \<le> r"
+    using assms by (simp add: right_diff_distrib)
+  moreover have "0 < b * (1 + q - q') "
+    using assms by (simp add: right_diff_distrib distrib_left)
+  moreover have "b * q' < b * (1 + q)"
+    using assms by (simp add: right_diff_distrib distrib_left)
+  ultimately show ?thesis
+    using assms by (simp add: mult_less_cancel_left)
+qed
 
 lemma unique_quotient_lemma_neg:
   "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
@@ -43,10 +44,9 @@
 
 lemma unique_quotient:
   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
-  apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
-  apply (blast intro: order_antisym
-    dest: order_eq_refl [THEN unique_quotient_lemma]
-    order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
+  apply (rule order_antisym)
+   apply (simp_all add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
+     apply (blast intro: order_eq_refl [THEN unique_quotient_lemma] order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   done
 
 lemma unique_remainder:
diff -r b942da0962c2 -r e371784becd9 src/HOL/Vector_Spaces.thy
--- a/src/HOL/Vector_Spaces.thy	Fri Jul 13 15:42:18 2018 +0200
+++ b/src/HOL/Vector_Spaces.thy	Fri Jul 13 17:27:05 2018 +0100
@@ -281,16 +281,9 @@
 qed
 
 lemma in_span_delete:
-  assumes a: "a \<in> span S"
-    and na: "a \<notin> span (S - {b})"
+  assumes a: "a \<in> span S" and na: "a \<notin> span (S - {b})"
   shows "b \<in> span (insert a (S - {b}))"
-  apply (rule in_span_insert)
-  apply (rule set_rev_mp)
-  apply (rule a)
-  apply (rule span_mono)
-  apply blast
-  apply (rule na)
-  done
+  by (metis Diff_empty Diff_insert0 a in_span_insert insert_Diff na)
 
 lemma span_redundant: "x \<in> span S \<Longrightarrow> span (insert x S) = span S"
   unfolding span_def by (rule hull_redundant)
@@ -484,7 +477,7 @@
       have \<open>b \<in> span C\<close>
         using \<open>b \<in> B\<close> unfolding eq[symmetric] by (rule span_base)
       have \<open>(\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. (?R' b v * ?R v w) *s w) =
-          (\<Sum>v | ?R' b v \<noteq> 0. ?R' b v *s (\<Sum>w | ?R v w \<noteq> 0. ?R v w *s w))\<close>
+           (\<Sum>v | ?R' b v \<noteq> 0. ?R' b v *s (\<Sum>w | ?R v w \<noteq> 0. ?R v w *s w))\<close>
         by (simp add: scale_sum_right)
       also have \<open>\<dots> = (\<Sum>v | ?R' b v \<noteq> 0. ?R' b v *s v)\<close>
         by (auto simp: sum_nonzero_representation_eq B eq span_base representation_ne_zero)
@@ -492,15 +485,13 @@
         by (rule sum_nonzero_representation_eq[OF C \<open>b \<in> span C\<close>])
       finally have "?R b b = ?R (\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. (?R' b v * ?R v w) *s w) b"
         by simp
+      also have "... = (\<Sum>i\<in>{v. ?R' b v \<noteq> 0}. ?R (\<Sum>w | ?R i w \<noteq> 0. (?R' b i * ?R i w) *s w) b)"
+        by (subst representation_sum[OF B])  (auto intro: span_sum span_scale span_base representation_ne_zero)
+      also have "... = (\<Sum>i\<in>{v. ?R' b v \<noteq> 0}.
+           \<Sum>j \<in> {w. ?R i w \<noteq> 0}. ?R ((?R' b i * ?R i j ) *s  j ) b)"
+        by (subst representation_sum[OF B]) (auto simp add: span_sum span_scale span_base representation_ne_zero)
       also have \<open>\<dots> = (\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. ?R' b v * ?R v w * ?R w b)\<close>
-        using B \<open>b \<in> B\<close>
-        apply (subst representation_sum[OF B])
-         apply (fastforce intro: span_sum span_scale span_base representation_ne_zero)
-        apply (rule sum.cong[OF refl])
-        apply (subst representation_sum[OF B])
-         apply (simp add: span_sum span_scale span_base representation_ne_zero)
-        apply (simp add: representation_scale[OF B] span_base representation_ne_zero)
-        done
+        using B \<open>b \<in> B\<close> by (simp add: representation_scale[OF B] span_base representation_ne_zero)
       finally have "(\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. ?R' b v * ?R v w * ?R w b) \<noteq> 0"
         using representation_basis[OF B \<open>b \<in> B\<close>] by auto
       then obtain v w where bv: "?R' b v \<noteq> 0" and vw: "?R v w \<noteq> 0" and "?R' b v * ?R v w * ?R w b \<noteq> 0"
@@ -516,7 +507,7 @@
     proof (subst B_eq, rule card_of_UNION_ordLeq_infinite[OF \<open>infinite C\<close>])
       show "ordLeq3 (card_of C) (card_of C)"
         by (intro ordLeq_refl card_of_Card_order)
-      show "\<forall>c\<in>C. ordLeq3 (card_of {v. representation B c v \<noteq> 0}) (card_of C)"
+      show "\<forall>c\<in>C. ordLeq3 (card_of {v. ?R c v \<noteq> 0}) (card_of C)"
         by (intro ballI ordLeq3_finite_infinite \<open>infinite C\<close> finite_representation)
     qed }
   from this[of B C] this[of C B] B C eq \<open>infinite C\<close> \<open>infinite B\<close>
@@ -584,10 +575,9 @@
 
 lemma subspace_sums: "\<lbrakk>subspace S; subspace T\<rbrakk> \<Longrightarrow> subspace {x + y|x y. x \<in> S \<and> y \<in> T}"
   apply (simp add: subspace_def)
-  apply (intro conjI impI allI)
-  using add.right_neutral apply blast
-   apply clarify
-   apply (metis add.assoc add.left_commute)
+  apply (intro conjI impI allI; clarsimp simp: algebra_simps)
+  using add.left_neutral apply blast
+   apply (metis add.assoc)
   using scale_right_distrib by blast
 
 end
@@ -876,10 +866,10 @@
     proof (rule vector_space_pair.linear_eq_on[where x=v])
       show "vector_space_pair ( *a) ( *a)" by unfold_locales
       show "linear ( *a) ( *a) (?g \<circ> f)"
-        apply (rule Vector_Spaces.linear_compose[of _ "( *b)"])
-        subgoal by unfold_locales
-        apply fact
-        done
+      proof (rule Vector_Spaces.linear_compose[of _ "( *b)"])
+        show "linear ( *a) ( *b) f"
+          by unfold_locales
+      qed fact
       show "linear ( *a) ( *a) id" by (rule vs1.linear_id)
       show "v \<in> vs1.span B" by fact
       show "b \<in> B \<Longrightarrow> (p.construct (f ` B) (the_inv_into B f) \<circ> f) b = id b" for b
@@ -915,10 +905,7 @@
     proof (rule vector_space_pair.linear_eq_on[where x=v])
       show "vector_space_pair ( *b) ( *b)" by unfold_locales
       show "linear ( *b) ( *b) (f \<circ> ?g)"
-        apply (rule Vector_Spaces.linear_compose[of _ "( *a)"])
-        apply fact
-        subgoal by fact
-        done
+        by (rule Vector_Spaces.linear_compose[of _ "( *a)"]) fact+
       show "linear ( *b) ( *b) id" by (rule vs2.linear_id)
       have "vs2.span (f ` B) = vs2.span C"
         using fB_C vs2.span_mono[of C "f ` B"] vs2.span_minimal[of "f`B" "vs2.span C"]
@@ -1035,8 +1022,7 @@
           by (metis member_remove remove_def)
       qed
       also have " \<dots> \<le> card (S - {y})"
-        apply (rule card_image_le)
-        using fS by simp
+        by (simp add: card_image_le fS)
       also have "\<dots> \<le> card S - 1" using y fS by simp
       finally show False using S0 by arith
     qed
@@ -1076,22 +1062,23 @@
     case False
     obtain B where B: "B \<subseteq> span S" "independent B" "span S \<subseteq> span B" "card B = dim (span S)"
       using basis_exists [of "span S"] by blast
-    have 1: "insert x B \<subseteq> span (insert x S)"
-      by (meson B(1) insertI1 insert_subset order_trans span_base span_mono subset_insertI)
-    have 2: "span (insert x S) \<subseteq> span (insert x B)"
-      by (metis \<open>B \<subseteq> span S\<close> \<open>span S \<subseteq> span B\<close> span_breakdown_eq span_subspace subsetI subspace_span)
-    have 3: "independent (insert x B)"
-      by (metis B(1-3) independent_insert span_subspace subspace_span False)
     have "dim (span (insert x S)) = Suc (dim S)"
-      apply (rule dim_unique [OF 1 2 3])
-      by (metis B False card_insert_disjoint dim_span finiteI_independent span_base span_eq span_span)
+    proof (rule dim_unique)
+      show "insert x B \<subseteq> span (insert x S)"
+        by (meson B(1) insertI1 insert_subset order_trans span_base span_mono subset_insertI)
+      show "span (insert x S) \<subseteq> span (insert x B)"
+        by (metis \<open>B \<subseteq> span S\<close> \<open>span S \<subseteq> span B\<close> span_breakdown_eq span_subspace subsetI subspace_span)
+      show "independent (insert x B)"
+        by (metis B(1-3) independent_insert span_subspace subspace_span False)
+      show "card (insert x B) = Suc (dim S)"
+        using B False finiteI_independent by force
+    qed
     then show ?thesis
       by (metis False Suc_eq_plus1 dim_span)
   qed
 qed
 
-lemma dim_singleton [simp]:
-  "dim{x} = (if x = 0 then 0 else 1)"
+lemma dim_singleton [simp]: "dim{x} = (if x = 0 then 0 else 1)"
   by (simp add: dim_insert)
 
 proposition choose_subspace_of_subspace:
@@ -1109,9 +1096,10 @@
     then show ?case
     proof (cases "span S \<subseteq> span T")
       case True
-      have "dim S = dim T"
-        apply (rule span_eq_dim [OF subset_antisym [OF True]])
+      have "span T \<subseteq> span S"
         by (simp add: \<open>T \<subseteq> span S\<close> span_minimal)
+      then have "dim S = dim T"
+        by (rule span_eq_dim [OF subset_antisym [OF True]])
       then show ?thesis
         using Suc.prems \<open>dim T = n\<close> by linarith
     next
@@ -1122,8 +1110,7 @@
         by (metis (no_types) \<open>T \<subseteq> span S\<close> subsetD insert_subset span_superset span_mono span_span)
       with \<open>dim T = n\<close>  \<open>subspace T\<close> y show ?thesis
         apply (rule_tac x="span(insert y T)" in exI)
-        apply (auto simp: dim_insert)
-        using span_eq_iff by blast
+        using span_eq_iff by (fastforce simp: dim_insert)
     qed
   qed
   with that show ?thesis by blast
@@ -1268,15 +1255,12 @@
 
 lemma independent_explicit:
   shows "independent B \<longleftrightarrow> finite B \<and> (\<forall>c. (\<Sum>v\<in>B. c v *s v) = 0 \<longrightarrow> (\<forall>v \<in> B. c v = 0))"
-  apply (cases "finite B")
-   apply (force simp: dependent_finite)
   using independent_bound_general
-  apply auto
-  done
+  by (fastforce simp: dependent_finite)
 
 proposition dim_sums_Int:
   assumes "subspace S" "subspace T"
-  shows "dim {x + y |x y. x \<in> S \<and> y \<in> T} + dim(S \<inter> T) = dim S + dim T"
+  shows "dim {x + y |x y. x \<in> S \<and> y \<in> T} + dim(S \<inter> T) = dim S + dim T" (is "dim ?ST + _ = _")
 proof -
   obtain B where B: "B \<subseteq> S \<inter> T" "S \<inter> T \<subseteq> span B"
              and indB: "independent B"
@@ -1289,29 +1273,28 @@
   then have "finite B" "finite C" "finite D"
     by (simp_all add: finiteI_independent indB independent_bound_general)
   have Beq: "B = C \<inter> D"
-    apply (rule sym)
-    apply (rule spanning_subset_independent)
-    using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> apply blast
-    apply (meson \<open>independent C\<close> independent_mono inf.cobounded1)
-    using B \<open>C \<subseteq> S\<close> \<open>D \<subseteq> T\<close> apply auto
-    done
+  proof (rule spanning_subset_independent [symmetric])
+    show "independent (C \<inter> D)"
+      by (meson \<open>independent C\<close> independent_mono inf.cobounded1)
+  qed (use B \<open>C \<subseteq> S\<close> \<open>D \<subseteq> T\<close> \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> in auto)
   then have Deq: "D = B \<union> (D - C)"
     by blast
-  have CUD: "C \<union> D \<subseteq> {x + y |x y. x \<in> S \<and> y \<in> T}"
-    apply safe
-    apply (metis add.right_neutral subsetCE \<open>C \<subseteq> S\<close> \<open>subspace T\<close> set_eq_subset span_zero span_minimal)
-    apply (metis add.left_neutral subsetCE \<open>D \<subseteq> T\<close> \<open>subspace S\<close> set_eq_subset span_zero span_minimal)
-    done
+  have CUD: "C \<union> D \<subseteq> ?ST"
+  proof (simp, intro conjI)
+    show "C \<subseteq> ?ST"
+      using span_zero span_minimal [OF _ \<open>subspace T\<close>] \<open>C \<subseteq> S\<close> by force
+    show "D \<subseteq> ?ST"
+      using span_zero span_minimal [OF _ \<open>subspace S\<close>] \<open>D \<subseteq> T\<close> by force
+  qed
   have "a v = 0" if 0: "(\<Sum>v\<in>C. a v *s v) + (\<Sum>v\<in>D - C. a v *s v) = 0"
                  and v: "v \<in> C \<union> (D-C)" for a v
   proof -
+    have CsS: "\<And>x. x \<in> C \<Longrightarrow> a x *s x \<in> S"
+      using \<open>C \<subseteq> S\<close> \<open>subspace S\<close> subspace_scale by auto
     have eq: "(\<Sum>v\<in>D - C. a v *s v) = - (\<Sum>v\<in>C. a v *s v)"
       using that add_eq_0_iff by blast
     have "(\<Sum>v\<in>D - C. a v *s v) \<in> S"
-      apply (subst eq)
-      apply (rule subspace_neg [OF \<open>subspace S\<close>])
-      apply (rule subspace_sum [OF \<open>subspace S\<close>])
-      by (meson subsetCE subspace_scale \<open>C \<subseteq> S\<close> \<open>subspace S\<close>)
+      by (simp add: eq CsS \<open>subspace S\<close> subspace_neg subspace_sum)
     moreover have "(\<Sum>v\<in>D - C. a v *s v) \<in> T"
       apply (rule subspace_sum [OF \<open>subspace T\<close>])
       by (meson DiffD1 \<open>D \<subseteq> T\<close> \<open>subspace T\<close> subset_eq subspace_def)
@@ -1350,8 +1333,7 @@
         using Beq \<open>(\<Sum>x\<in>C - B. a x *s x) = 0\<close> f3 f4 by auto
     qed
     with 0 have Dcc0: "(\<Sum>v\<in>D. a v *s v) = 0"
-      apply (subst Deq)
-      by (simp add: \<open>finite B\<close> \<open>finite D\<close> sum_Un)
+      by (subst Deq) (simp add: \<open>finite B\<close> \<open>finite D\<close> sum_Un)
     then have D0: "\<And>v. v \<in> D \<Longrightarrow> a v = 0"
       using independent_explicit \<open>independent D\<close> \<open>finite D\<close> by blast
     show ?thesis
@@ -1368,10 +1350,13 @@
     by (metis \<open>C \<subseteq> S\<close> \<open>independent C\<close> \<open>S \<subseteq> span C\<close> basis_card_eq_dim)
   moreover have "dim T = card D"
     by (metis \<open>D \<subseteq> T\<close> \<open>independent D\<close> \<open>T \<subseteq> span D\<close> basis_card_eq_dim)
-  moreover have "dim {x + y |x y. x \<in> S \<and> y \<in> T} = card(C \<union> D)"
-    apply (rule dim_unique [OF CUD _ indCUD refl], clarify)
-    apply (meson \<open>S \<subseteq> span C\<close> \<open>T \<subseteq> span D\<close> span_add span_superset span_minimal subsetCE subspace_span sup.bounded_iff)
-    done
+  moreover have "dim ?ST = card(C \<union> D)"
+  proof -
+    have *: "\<And>x y. \<lbrakk>x \<in> S; y \<in> T\<rbrakk> \<Longrightarrow> x + y \<in> span (C \<union> D)"
+      by (meson \<open>S \<subseteq> span C\<close> \<open>T \<subseteq> span D\<close> span_add span_mono subsetCE sup.cobounded1 sup.cobounded2)
+    show ?thesis
+      by (auto intro: * dim_unique [OF CUD _ indCUD refl])
+  qed
   ultimately show ?thesis
     using \<open>B = C \<inter> D\<close> [symmetric]
     by (simp add:  \<open>independent C\<close> \<open>independent D\<close> card_Un_Int finiteI_independent)
@@ -1396,20 +1381,16 @@
     by blast
   from B(4) have d: "dim UNIV = card B"
     by simp
-  have th: "UNIV \<subseteq> span (f ` B)"
-    apply (rule card_ge_dim_independent)
-      apply blast
-    using B(2) inj_on_subset[OF fi]
-     apply (rule lf.independent_inj_on_image)
-     apply blast
-    apply (rule order_eq_refl)
-    apply (rule sym)
-    unfolding d
-    apply (rule card_image)
-    apply (rule subset_inj_on[OF fi])
-    apply blast
-    done
-  from th show ?thesis
+  have "UNIV \<subseteq> span (f ` B)"
+  proof (rule card_ge_dim_independent)
+    show "independent (f ` B)"
+      by (simp add: B(2) fi lf.independent_inj_image)
+    have "card (f ` B) = dim UNIV"
+      by (metis B(1) card_image d fi inj_on_subset)
+    then show "dim UNIV \<le> card (f ` B)"
+      by simp
+  qed blast
+  then show ?thesis
     unfolding lf.span_image surj_def
     using B(3) by blast
 qed
@@ -1535,38 +1516,19 @@
     and fi: "inj f"
     and dims: "vs2.dim UNIV = vs1.dim UNIV"
   shows "\<exists>f'. linear s2 s1 f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
-proof -
-  show ?thesis
-    unfolding isomorphism_expand[symmetric]
-    using linear_exists_right_inverse_on[OF lf vs1.subspace_UNIV]
-      linear_exists_left_inverse_on[OF lf vs1.subspace_UNIV fi]
-    apply (auto simp: module_hom_iff_linear)
-    subgoal for f' f''
-      apply (rule exI[where x=f''])
-      using linear_injective_imp_surjective[OF lf fi dims]
-      apply auto
-      by (metis comp_apply eq_id_iff surj_def)
-    done
-qed
+  unfolding isomorphism_expand[symmetric]
+  using linear_injective_imp_surjective[OF lf fi dims]
+  using fi left_right_inverse_eq lf linear_injective_left_inverse linear_surjective_right_inverse by blast
 
 lemma linear_surjective_isomorphism:
   assumes lf: "linear s1 s2 f"
     and sf: "surj f"
     and dims: "vs2.dim UNIV = vs1.dim UNIV"
   shows "\<exists>f'. linear s2 s1 f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
-proof -
-  show ?thesis
-    unfolding isomorphism_expand[symmetric]
-    using linear_exists_right_inverse_on[OF lf vs1.subspace_UNIV]
-      linear_exists_left_inverse_on[OF lf vs1.subspace_UNIV]
-    using linear_surjective_imp_injective[OF lf sf dims] sf
-    apply (auto simp: module_hom_iff_linear)
-    subgoal for f' f''
-      apply (rule exI[where x=f''])
-      apply auto
-      by (metis isomorphism_expand)
-    done
-qed
+  using linear_surjective_imp_injective[OF lf sf dims] sf
+    linear_exists_right_inverse_on[OF lf vs1.subspace_UNIV]
+    linear_exists_left_inverse_on[OF lf vs1.subspace_UNIV]
+    dims lf linear_injective_isomorphism by auto
 
 lemma basis_to_basis_subspace_isomorphism:
   assumes s: "vs1.subspace S"
@@ -1674,12 +1636,8 @@
   from linear_surjective_isomorphism[OF lf fi]
   obtain h:: "'b \<Rightarrow> 'b" where h: "linear scale scale h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
     by blast
-  have "h = g"
-    apply (rule ext)
-    using gf h(2,3)
-    apply (simp add: o_def id_def fun_eq_iff)
-    apply metis
-    done
+  then have "h = g"
+    by (metis gf isomorphism_expand left_right_inverse_eq)
   with h(1) show ?thesis by blast
 qed