merged
authorpaulson
Tue, 19 Jun 2018 12:14:31 +0100
changeset 68468 ae42b0f6885d
parent 68466 3ead36cbe6b7 (current diff)
parent 68467 44ffc5b9cd76 (diff)
child 68469 7ddcce75c3ee
child 68470 aad109fde9ec
merged
--- a/CONTRIBUTORS	Mon Jun 18 22:20:55 2018 +0100
+++ b/CONTRIBUTORS	Tue Jun 19 12:14:31 2018 +0100
@@ -6,6 +6,9 @@
 Contributions to Isabelle2018
 -----------------------------
 
+* June 2018: Martin Baillon and Paulo Emílio de Vilhena
+  A variety of contributions to HOL-Algebra.
+
 * May 2018: Manuel Eberl
   Landau symbols and asymptotic equivalence (moved from the AFP).
 
--- a/NEWS	Mon Jun 18 22:20:55 2018 +0100
+++ b/NEWS	Tue Jun 19 12:14:31 2018 +0100
@@ -375,6 +375,10 @@
 * Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
 infix/prefix notation.
 
+* Session HOL-Algebra: Revamped with much new material.
+The set of isomorphisms between two groups is now denoted iso rather than iso_set.
+INCOMPATIBILITY.
+
 * Session HOL-Analysis: infinite products, Moebius functions, the
 Riemann mapping theorem, the Vitali covering theorem,
 change-of-variables results for integration and measures.
--- a/src/HOL/Algebra/Zassenhaus.thy	Mon Jun 18 22:20:55 2018 +0100
+++ b/src/HOL/Algebra/Zassenhaus.thy	Tue Jun 19 12:14:31 2018 +0100
@@ -1,12 +1,18 @@
+(*  Title:      HOL/Algebra/Zassenhaus.thy
+    Author:     Martin Baillon
+*)
+
+section \<open>The Zassenhaus Lemma\<close>
+
 theory Zassenhaus
   imports Coset Group_Action
 begin
 
-
-subsubsection \<open>Lemmas about normalizer\<close>
+text \<open>Proves the second isomorphism theorem and the Zassenhaus lemma.\<close>
 
+subsection \<open>Lemmas about normalizer\<close>
 
-lemma (in group) subgroup_in_normalizer: 
+lemma (in group) subgroup_in_normalizer:
   assumes "subgroup H G"
   shows "normal H (G\<lparr>carrier:= (normalizer G H)\<rparr>)"
 proof(intro group.normal_invI)
@@ -19,7 +25,7 @@
     have "x <# H = H"
       by (metis \<open>x \<in> H\<close> assms group.lcos_mult_one is_group
          l_repr_independence one_closed subgroup.subset)
-    moreover have "H #> inv x = H" 
+    moreover have "H #> inv x = H"
       by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed)
     ultimately have "x <# H #> (inv x) = H" by simp
     thus " x \<in> stabilizer G (\<lambda>g. \<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H"
@@ -58,7 +64,7 @@
 lemma (in group) normal_imp_subgroup_normalizer:
   assumes "subgroup H G"
     and "N \<lhd> (G\<lparr>carrier := H\<rparr>)"
-  shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" 
+  shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
 proof-
   have N_carrierG : "N \<subseteq> carrier(G)"
     using assms normal_imp_subgroup subgroup.subset
@@ -72,7 +78,7 @@
       hence "x <# N #> inv x =(N #> x) #> inv x"
         by simp
       also have "... = N #> \<one>"
-        using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp  
+        using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp
       finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
       thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) N = N}"
         using xcarrierG by (simp add : N_carrierG)
@@ -103,10 +109,10 @@
       using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD)
     have "N #> h1 = h1 <# N"
       using normalI B2 assms normal.coset_eq subgroup.subset by blast
-    hence "h1\<otimes>n2 \<in> N #> h1" 
+    hence "h1\<otimes>n2 \<in> N #> h1"
       using B2 B3 assms l_coset_def by fastforce
-    from this obtain y2 where y2_def:"y2 \<in> N" and y2_prop:"y2\<otimes>h1 = h1\<otimes>n2" 
-      using singletonD by (metis (no_types, lifting) UN_E r_coset_def) 
+    from this obtain y2 where y2_def:"y2 \<in> N" and y2_prop:"y2\<otimes>h1 = h1\<otimes>n2"
+      using singletonD by (metis (no_types, lifting) UN_E r_coset_def)
     have " x\<otimes>y =  n1 \<otimes> y2 \<otimes> h1 \<otimes> h2" using y2_def B2 B3
       by (smt assms y2_prop m_assoc m_closed normal_imp_subgroup subgroup.mem_carrier)
     moreover have B4 :"n1 \<otimes> y2 \<in>N"
@@ -129,10 +135,10 @@
     hence "... \<otimes>h \<in> N"
       using assms C2
       by (meson normal.inv_op_closed1 normal_def subgroup.m_inv_closed subgroup.mem_carrier)
-    hence  C4:"(inv h \<otimes> inv n \<otimes> h) \<otimes> inv h \<in> (N<#>H)" 
+    hence  C4:"(inv h \<otimes> inv n \<otimes> h) \<otimes> inv h \<in> (N<#>H)"
       using   C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto
     have "inv h \<otimes> inv n \<otimes> h \<otimes> inv h = inv h \<otimes> inv n"
-      using  subgroup.subset[OF assms(2)] 
+      using  subgroup.subset[OF assms(2)]
       by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE)
     thus "inv(x)\<in>N<#>H" using C4 C2 C3 by simp
   qed
@@ -149,7 +155,7 @@
   thus "(N <#> H \<subseteq> carrier G \<and> (\<forall>x y. x \<in> N <#> H \<longrightarrow> y \<in> N <#> H \<longrightarrow> x \<otimes> y \<in> N <#> H)) \<and>
     \<one> \<in> N <#> H \<and> (\<forall>x. x \<in> N <#> H \<longrightarrow> inv x \<in> N <#> H)" using A B C D assms by blast
 qed
-    
+
 
 lemma (in group) mult_norm_sub_in_sub:
   assumes "normal N (G\<lparr>carrier:=K\<rparr>)"
@@ -201,7 +207,7 @@
 
 
 proposition (in group) weak_snd_iso_thme:
-  assumes "subgroup  H G" 
+  assumes "subgroup  H G"
     and "N\<lhd>G"
   shows "(G\<lparr>carrier := N<#>H\<rparr> Mod N \<cong> G\<lparr>carrier:=H\<rparr> Mod (N\<inter>H))"
 proof-
@@ -325,8 +331,8 @@
           carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
          G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
           (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>
-         G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H" 
-    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H] 
+         G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
+    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H]
           subgroup.subset[OF assms(3)]
           subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
     by simp
@@ -343,7 +349,7 @@
   moreover have "H\<inter>N = N\<inter>H" using assms  by auto
   ultimately show "(G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>  G\<lparr>carrier := H\<rparr> Mod H \<inter> N" by auto
 qed
- 
+
 
 corollary (in group) snd_iso_thme_recip :
   assumes "subgroup H G"
@@ -358,9 +364,9 @@
 
 
 lemma (in group) distinc:
-  assumes "subgroup  H G" 
-    and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
-    and  "subgroup K G" 
+  assumes "subgroup  H G"
+    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
+    and  "subgroup K G"
     and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
   shows "subgroup (H\<inter>K) (G\<lparr>carrier:=(normalizer G (H1<#>(H\<inter>K1))) \<rparr>)"
 proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]])
@@ -401,7 +407,7 @@
       by auto
     also have "... = {x} <#> (H1 <#> H \<inter> K1) <#> {inv x}"
       using allG xG set_mult_assoc setmult_subset_G by (metis inf.coboundedI2)
-    finally have "H1 <#> H \<inter> K1 = x <# (H1 <#> H \<inter> K1) #> inv x" 
+    finally have "H1 <#> H \<inter> K1 = x <# (H1 <#> H \<inter> K1) #> inv x"
       using xG setmult_subset_G allG by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult)
     thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) (H1 <#> H \<inter> K1)
                                                                        = H1 <#> H \<inter> K1}"
@@ -411,9 +417,9 @@
 qed
 
 lemma (in group) preliminary1:
-  assumes "subgroup  H G" 
-    and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
-    and  "subgroup K G" 
+  assumes "subgroup  H G"
+    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
+    and  "subgroup K G"
     and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
   shows " (H\<inter>K) \<inter> (H1<#>(H\<inter>K1)) = (H1\<inter>K)<#>(H\<inter>K1)"
 proof
@@ -452,15 +458,15 @@
 qed
 
 lemma (in group) preliminary2:
-  assumes "subgroup  H G" 
+  assumes "subgroup  H G"
     and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
-    and  "subgroup K G" 
+    and  "subgroup K G"
     and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
   shows "(H1<#>(H\<inter>K1)) \<lhd> G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>"
 proof-
   have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G"
     using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
-  have subH1:"subgroup (H1 <#> H \<inter> K) (G\<lparr>carrier := H\<rparr>)" 
+  have subH1:"subgroup (H1 <#> H \<inter> K) (G\<lparr>carrier := H\<rparr>)"
     using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)]
           assms(1)]] assms by auto
   have "Group.group (G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>)"
@@ -541,7 +547,7 @@
     finally  have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x =H1 <#> H \<inter> K1  #> hk"
       using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF
            assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp
-    thus " H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = 
+    thus " H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x =
              x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1)" using eq1 by simp
   qed
   ultimately show "H1 <#> H \<inter> K1 \<lhd> G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>"
@@ -550,9 +556,9 @@
 
 
 proposition (in group)  Zassenhaus_1:
-  assumes "subgroup  H G" 
-    and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
-    and  "subgroup K G" 
+  assumes "subgroup  H G"
+    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
+    and  "subgroup K G"
     and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
   shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>H\<inter>K1)) \<cong> (G\<lparr>carrier:= (H\<inter>K)\<rparr> Mod  ((H1\<inter>K)<#>(H\<inter>K1)))"
 proof-
@@ -572,7 +578,7 @@
     also have "... = ((H\<inter>K)<#>H1) <#>(H\<inter>K1)"
       using set_mult_assoc[where ?M = "H\<inter>K"] K1_incl_G H1_incl_G assms
       by (simp add: inf.coboundedI2 subgroup.subset)
-    also have "... = (H1<#>(H\<inter>K))<#>(H\<inter>K1)" 
+    also have "... = (H1<#>(H\<inter>K))<#>(H\<inter>K1)"
       using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto
     also have "... =  H1 <#> ((H\<inter>K)<#>(H\<inter>K1))"
       using set_mult_assoc K1_incl_G H1_incl_G assms
@@ -585,25 +591,25 @@
               incl_subgroup[OF assms(3) normal_imp_subgroup]] subgroups_Inter_pair] assms
               normal_imp_subgroup by (metis inf_commute normal_inter)
     qed
-    hence " H1 <#> ((H\<inter>K)<#>(H\<inter>K1)) =  H1 <#> ((H\<inter>K))" 
+    hence " H1 <#> ((H\<inter>K)<#>(H\<inter>K1)) =  H1 <#> ((H\<inter>K))"
       by simp
     thus "N <#> N1 = H1 <#> H \<inter> K"
       by (simp add: calculation)
   qed
 
-  have "N\<inter>N1 = (H1\<inter>K)<#>(H\<inter>K1)" 
-    using preliminary1 assms N_def N1_def by simp 
+  have "N\<inter>N1 = (H1\<inter>K)<#>(H\<inter>K1)"
+    using preliminary1 assms N_def N1_def by simp
   thus  "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod N1)  \<cong> (G\<lparr>carrier:= N\<rparr> Mod  ((H1\<inter>K)<#>(H\<inter>K1)))"
     using H_simp Hp by auto
 qed
 
 
 theorem (in group) Zassenhaus:
-  assumes "subgroup  H G" 
-    and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
-    and  "subgroup K G" 
+  assumes "subgroup  H G"
+    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
+    and  "subgroup K G"
     and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
-  shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>(H\<inter>K1)))  \<cong> 
+  shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>(H\<inter>K1)))  \<cong>
          (G\<lparr>carrier:= K1 <#> (H\<inter>K)\<rparr> Mod (K1<#>(K\<inter>H1)))"
 proof-
   define Gmod1 Gmod2 Gmod3 Gmod4
@@ -620,8 +626,8 @@
     show "K1 \<inter> H \<lhd> G\<lparr>carrier := H \<inter> K\<rparr>"
       using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add: inf_commute)
    next
-    show "subgroup (K \<inter> H1) (G\<lparr>carrier := H \<inter> K\<rparr>)" 
-      using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter) 
+    show "subgroup (K \<inter> H1) (G\<lparr>carrier := H \<inter> K\<rparr>)"
+      using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter)
   qed
   hence  "Gmod3  = Gmod4" using Hp Gmod4_def by simp
   hence "Gmod1 \<cong> Gmod2"
--- a/src/HOL/Analysis/Analysis.thy	Mon Jun 18 22:20:55 2018 +0100
+++ b/src/HOL/Analysis/Analysis.thy	Tue Jun 19 12:14:31 2018 +0100
@@ -7,6 +7,7 @@
   Radon_Nikodym
   Fashoda_Theorem
   Determinants
+  Cross3
   Homeomorphism
   Bounded_Continuous_Function
   Function_Topology
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Cross3.thy	Tue Jun 19 12:14:31 2018 +0100
@@ -0,0 +1,227 @@
+(* Title:      HOL/Analysis/Cross3.thy
+   Author:     L C Paulson, University of Cambridge
+
+Ported from HOL Light
+*)
+
+section\<open>Vector Cross Products in 3 Dimensions.\<close>
+
+theory "Cross3"
+  imports Determinants
+begin
+
+context includes no_Set_Product_syntax 
+begin \<comment>\<open>locally disable syntax for set product, to avoid warnings\<close>
+
+definition cross3 :: "[real^3, real^3] \<Rightarrow> real^3"  (infixr "\<times>" 80)
+  where "a \<times> b \<equiv>
+    vector [a$2 * b$3 - a$3 * b$2,
+            a$3 * b$1 - a$1 * b$3,
+            a$1 * b$2 - a$2 * b$1]"
+
+end
+
+bundle cross3_syntax begin
+notation cross3 (infixr "\<times>" 80)
+no_notation Product_Type.Times (infixr "\<times>" 80)
+end
+
+bundle no_cross3_syntax begin
+no_notation cross3 (infixr "\<times>" 80)
+notation Product_Type.Times (infixr "\<times>" 80)
+end
+
+unbundle cross3_syntax
+
+subsection\<open> Basic lemmas.\<close>
+
+lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps
+
+lemma dot_cross_self: "x \<bullet> (x \<times> y) = 0" "x \<bullet> (y \<times> x) = 0" "(x \<times> y) \<bullet> y = 0" "(y \<times> x) \<bullet> y = 0"
+  by (simp_all add: orthogonal_def cross3_simps)
+
+lemma orthogonal_cross: "orthogonal (x \<times> y) x" "orthogonal (x \<times> y) y"  
+                        "orthogonal y (x \<times> y)" "orthogonal (x \<times> y) x"
+  by (simp_all add: orthogonal_def dot_cross_self)
+
+lemma cross_zero_left [simp]: "0 \<times> x = 0" and cross_zero_right [simp]: "x \<times> 0 = 0" for x::"real^3"
+  by (simp_all add: cross3_simps)
+
+lemma cross_skew: "(x \<times> y) = -(y \<times> x)" for x::"real^3"
+  by (simp add: cross3_simps)
+
+lemma cross_refl [simp]: "x \<times> x = 0" for x::"real^3"
+  by (simp add: cross3_simps)
+
+lemma cross_add_left: "(x + y) \<times> z = (x \<times> z) + (y \<times> z)" for x::"real^3"
+  by (simp add: cross3_simps)
+
+lemma cross_add_right: "x \<times> (y + z) = (x \<times> y) + (x \<times> z)" for x::"real^3"
+  by (simp add: cross3_simps)
+
+lemma cross_mult_left: "(c *\<^sub>R x) \<times> y = c *\<^sub>R (x \<times> y)" for x::"real^3"
+  by (simp add: cross3_simps)
+
+lemma cross_mult_right: "x \<times> (c *\<^sub>R y) = c *\<^sub>R (x \<times> y)" for x::"real^3"
+  by (simp add: cross3_simps)
+
+lemma cross_minus_left [simp]: "(-x) \<times> y = - (x \<times> y)" for x::"real^3"
+  by (simp add: cross3_simps)
+
+lemma cross_minus_right [simp]: "x \<times> -y = - (x \<times> y)" for x::"real^3"
+  by (simp add: cross3_simps)
+
+lemma left_diff_distrib: "(x - y) \<times> z = x \<times> z - y \<times> z" for x::"real^3"
+  by (simp add: cross3_simps)
+
+lemma right_diff_distrib: "x \<times> (y - z) = x \<times> y - x \<times> z" for x::"real^3"
+  by (simp add: cross3_simps)
+
+hide_fact (open) left_diff_distrib right_diff_distrib
+
+lemma Jacobi: "x \<times> (y \<times> z) + y \<times> (z \<times> x) + z \<times> (x \<times> y) = 0" for x::"real^3"
+  by (simp add: cross3_simps)
+
+lemma Lagrange: "x \<times> (y \<times> z) = (x \<bullet> z) *\<^sub>R y - (x \<bullet> y) *\<^sub>R z"
+  by (simp add: cross3_simps) (metis (full_types) exhaust_3)
+
+lemma cross_triple: "(x \<times> y) \<bullet> z = (y \<times> z) \<bullet> x"
+  by (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)
+
+lemma cross_components:
+   "(x \<times> y)$1 = x$2 * y$3 - y$2 * x$3" "(x \<times> y)$2 = x$3 * y$1 - y$3 * x$1" "(x \<times> y)$3 = x$1 * y$2 - y$1 * x$2"
+  by (simp_all add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)
+
+lemma cross_basis: "(axis 1 1) \<times> (axis 2 1) = axis 3 1" "(axis 2 1) \<times> (axis 1 1) = -(axis 3 1)" 
+                   "(axis 2 1) \<times> (axis 3 1) = axis 1 1" "(axis 3 1) \<times> (axis 2 1) = -(axis 1 1)" 
+                   "(axis 3 1) \<times> (axis 1 1) = axis 2 1" "(axis 1 1) \<times> (axis 3 1) = -(axis 2 1)"
+  using exhaust_3
+  by (force simp add: axis_def cross3_simps)+
+
+lemma cross_basis_nonzero:
+  "u \<noteq> 0 \<Longrightarrow> ~(u \<times> axis 1 1 = 0) \<or> ~(u \<times> axis 2 1 = 0) \<or> ~(u \<times> axis 3 1 = 0)"
+  by (clarsimp simp add: axis_def cross3_simps) (metis vector_3 exhaust_3)
+
+lemma cross_dot_cancel:
+  fixes x::"real^3"
+  assumes deq: "x \<bullet> y = x \<bullet> z" and veq: "x \<times> y = x \<times> z" and x: "x \<noteq> 0"
+  shows "y = z" 
+proof -
+  have "x \<bullet> x \<noteq> 0"
+    by (simp add: x)
+  then have "y - z = 0"
+    using veq
+    by (metis (no_types, lifting) Cross3.right_diff_distrib Lagrange deq eq_iff_diff_eq_0 inner_diff_right scale_eq_0_iff)
+  then show ?thesis
+    using eq_iff_diff_eq_0 by blast
+qed
+
+lemma norm_cross_dot: "(norm (x \<times> y))\<^sup>2 + (x \<bullet> y)\<^sup>2 = (norm x * norm y)\<^sup>2"
+  unfolding power2_norm_eq_inner power_mult_distrib
+  by (simp add: cross3_simps power2_eq_square)
+
+lemma dot_cross_det: "x \<bullet> (y \<times> z) = det(vector[x,y,z])"
+  by (simp add: cross3_simps) 
+
+lemma cross_cross_det: "(w \<times> x) \<times> (y \<times> z) = det(vector[w,x,z]) *\<^sub>R y - det(vector[w,x,y]) *\<^sub>R z"
+  using exhaust_3 by (force simp add: cross3_simps) 
+
+lemma dot_cross: "(w \<times> x) \<bullet> (y \<times> z) = (w \<bullet> y) * (x \<bullet> z) - (w \<bullet> z) * (x \<bullet> y)"
+  by (force simp add: cross3_simps) 
+
+lemma norm_cross: "(norm (x \<times> y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \<bullet> y)\<^sup>2"
+  unfolding power2_norm_eq_inner power_mult_distrib
+  by (simp add: cross3_simps power2_eq_square)
+
+lemma cross_eq_0: "x \<times> y = 0 \<longleftrightarrow> collinear{0,x,y}"
+proof -
+  have "x \<times> y = 0 \<longleftrightarrow> norm (x \<times> y) = 0"
+    by simp
+  also have "... \<longleftrightarrow> (norm x * norm y)\<^sup>2 = (x \<bullet> y)\<^sup>2"
+    using norm_cross [of x y] by (auto simp: power_mult_distrib)
+  also have "... \<longleftrightarrow> \<bar>x \<bullet> y\<bar> = norm x * norm y"
+    using power2_eq_iff
+    by (metis (mono_tags, hide_lams) abs_minus abs_norm_cancel abs_power2 norm_mult power_abs real_norm_def) 
+  also have "... \<longleftrightarrow> collinear {0, x, y}"
+    by (rule norm_cauchy_schwarz_equal)
+  finally show ?thesis .
+qed
+
+lemma cross_eq_self: "x \<times> y = x \<longleftrightarrow> x = 0" "x \<times> y = y \<longleftrightarrow> y = 0"
+  apply (metis cross_zero_left dot_cross_self(1) inner_eq_zero_iff)
+  by (metis cross_zero_right dot_cross_self(2) inner_eq_zero_iff)
+
+lemma norm_and_cross_eq_0:
+   "x \<bullet> y = 0 \<and> x \<times> y = 0 \<longleftrightarrow> x = 0 \<or> y = 0" (is "?lhs = ?rhs")
+proof 
+  assume ?lhs
+  then show ?rhs
+    by (metis cross_dot_cancel cross_zero_right inner_zero_right)
+qed auto
+
+lemma bilinear_cross: "bilinear(\<times>)"
+  apply (auto simp add: bilinear_def linear_def)
+  apply unfold_locales
+  apply (simp add: cross_add_right)
+  apply (simp add: cross_mult_right)
+  apply (simp add: cross_add_left)
+  apply (simp add: cross_mult_left)
+  done
+
+subsection\<open>Preservation by rotation, or other orthogonal transformation up to sign.\<close>
+
+lemma cross_matrix_mult: "transpose A *v ((A *v x) \<times> (A *v y)) = det A *\<^sub>R (x \<times> y)"
+  apply (simp add: vec_eq_iff   )
+  apply (simp add: vector_matrix_mult_def matrix_vector_mult_def forall_3 cross3_simps)
+  done
+
+lemma cross_orthogonal_matrix:
+  assumes "orthogonal_matrix A"
+  shows "(A *v x) \<times> (A *v y) = det A *\<^sub>R (A *v (x \<times> y))"
+proof -
+  have "mat 1 = transpose (A ** transpose A)"
+    by (metis (no_types) assms orthogonal_matrix_def transpose_mat)
+  then show ?thesis
+    by (metis (no_types) vector_matrix_mul_rid vector_transpose_matrix cross_matrix_mult matrix_vector_mul_assoc matrix_vector_mult_scaleR)
+qed
+
+lemma cross_rotation_matrix: "rotation_matrix A \<Longrightarrow> (A *v x) \<times> (A *v y) =  A *v (x \<times> y)"
+  by (simp add: rotation_matrix_def cross_orthogonal_matrix)
+
+lemma cross_rotoinversion_matrix: "rotoinversion_matrix A \<Longrightarrow> (A *v x) \<times> (A *v y) = - A *v (x \<times> y)"
+  by (simp add: rotoinversion_matrix_def cross_orthogonal_matrix scaleR_matrix_vector_assoc)
+
+lemma cross_orthogonal_transformation:
+  assumes "orthogonal_transformation f"
+  shows   "(f x) \<times> (f y) = det(matrix f) *\<^sub>R f(x \<times> y)"
+proof -
+  have orth: "orthogonal_matrix (matrix f)"
+    using assms orthogonal_transformation_matrix by blast
+  have "matrix f *v z = f z" for z
+    using assms orthogonal_transformation_matrix by force
+  with cross_orthogonal_matrix [OF orth] show ?thesis
+    by simp
+qed
+
+lemma cross_linear_image:
+   "\<lbrakk>linear f; \<And>x. norm(f x) = norm x; det(matrix f) = 1\<rbrakk>
+           \<Longrightarrow> (f x) \<times> (f y) = f(x \<times> y)"
+  by (simp add: cross_orthogonal_transformation orthogonal_transformation)
+
+subsection\<open>Continuity\<close>
+
+lemma continuous_cross: "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (f x) \<times> (g x))"
+  apply (subst continuous_componentwise)
+  apply (clarsimp simp add: cross3_simps)
+  apply (intro continuous_intros; simp)
+  done
+
+lemma continuous_on_cross:
+  fixes f :: "'a::t2_space \<Rightarrow> real^3"
+  shows "\<lbrakk>continuous_on S f; continuous_on S g\<rbrakk> \<Longrightarrow> continuous_on S (\<lambda>x. (f x) \<times> (g x))"
+  by (simp add: continuous_on_eq_continuous_within continuous_cross)
+
+unbundle no_cross3_syntax
+
+end
+
--- a/src/HOL/Analysis/L2_Norm.thy	Mon Jun 18 22:20:55 2018 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy	Tue Jun 19 12:14:31 2018 +0100
@@ -110,12 +110,6 @@
   apply simp
   done
 
-lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<^sup>2 + y\<^sup>2) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
-  apply (rule power2_le_imp_le)
-  apply (simp add: power2_sum)
-  apply simp
-  done
-
 lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
   apply (cases "finite A")
   apply (induct set: finite)
@@ -126,19 +120,6 @@
   apply simp
   done
 
-lemma L2_set_mult_ineq_lemma:
-  fixes a b c d :: real
-  shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
-proof -
-  have "0 \<le> (a * d - b * c)\<^sup>2" by simp
-  also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * d) * (b * c)"
-    by (simp only: power2_diff power_mult_distrib)
-  also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * c) * (b * d)"
-    by simp
-  finally show "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
-    by simp
-qed
-
 lemma L2_set_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> L2_set f A * L2_set g A"
   apply (cases "finite A")
   apply (induct set: finite)
--- a/src/HOL/Analysis/Starlike.thy	Mon Jun 18 22:20:55 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Tue Jun 19 12:14:31 2018 +0100
@@ -188,6 +188,14 @@
   "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
   unfolding convex_alt closed_segment_def by auto
 
+lemma closed_segment_in_Reals:
+   "\<lbrakk>x \<in> closed_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
+  by (meson subsetD convex_Reals convex_contains_segment)
+
+lemma open_segment_in_Reals:
+   "\<lbrakk>x \<in> open_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
+  by (metis Diff_iff closed_segment_in_Reals open_segment_def)
+
 lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S"
   by (simp add: convex_contains_segment)
 
--- a/src/HOL/NthRoot.thy	Mon Jun 18 22:20:55 2018 +0100
+++ b/src/HOL/NthRoot.thy	Tue Jun 19 12:14:31 2018 +0100
@@ -665,30 +665,34 @@
 
 lemma sqrt_sum_squares_le_sum:
   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
-  apply (rule power2_le_imp_le)
-  apply (simp add: power2_sum)
-  apply simp
-  done
+  by (rule power2_le_imp_le) (simp_all add: power2_sum)
+
+lemma L2_set_mult_ineq_lemma:
+  fixes a b c d :: real
+  shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
+proof -
+  have "0 \<le> (a * d - b * c)\<^sup>2" by simp
+  also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * d) * (b * c)"
+    by (simp only: power2_diff power_mult_distrib)
+  also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * c) * (b * d)"
+    by simp
+  finally show "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
+    by simp
+qed
+
+lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<^sup>2 + y\<^sup>2) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
+  by (rule power2_le_imp_le) (simp_all add: power2_sum)
 
 lemma real_sqrt_sum_squares_triangle_ineq:
   "sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)"
-  apply (rule power2_le_imp_le)
-   apply simp
-   apply (simp add: power2_sum)
-   apply (simp only: mult.assoc distrib_left [symmetric])
-   apply (rule mult_left_mono)
-    apply (rule power2_le_imp_le)
-     apply (simp add: power2_sum power_mult_distrib)
-     apply (simp add: ring_distribs)
-     apply (subgoal_tac "0 \<le> b\<^sup>2 * c\<^sup>2 + a\<^sup>2 * d\<^sup>2 - 2 * (a * c) * (b * d)")
-      apply simp
-     apply (rule_tac b="(a * d - b * c)\<^sup>2" in ord_le_eq_trans)
-      apply (rule zero_le_power2)
-     apply (simp add: power2_diff power_mult_distrib)
-    apply simp
-   apply simp
-  apply (simp add: add_increasing)
-  done
+proof -
+  have "(a * c + b * d) \<le> (sqrt (a\<^sup>2 + b\<^sup>2) * sqrt (c\<^sup>2 + d\<^sup>2))"
+    by (rule power2_le_imp_le) (simp_all add: power2_sum power_mult_distrib ring_distribs L2_set_mult_ineq_lemma add.commute)
+  then have "(a + c)\<^sup>2 + (b + d)\<^sup>2 \<le> (sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2))\<^sup>2"
+    by (simp add: power2_sum)
+  then show ?thesis
+    by (auto intro: power2_le_imp_le)
+qed
 
 lemma real_sqrt_sum_squares_less: "\<bar>x\<bar> < u / sqrt 2 \<Longrightarrow> \<bar>y\<bar> < u / sqrt 2 \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u"
   apply (rule power2_less_imp_less)
--- a/src/HOL/Product_Type.thy	Mon Jun 18 22:20:55 2018 +0100
+++ b/src/HOL/Product_Type.thy	Tue Jun 19 12:14:31 2018 +0100
@@ -963,6 +963,13 @@
 
 hide_const (open) Times
 
+bundle no_Set_Product_syntax begin
+no_notation Product_Type.Times (infixr "\<times>" 80)
+end
+bundle Set_Product_syntax begin
+notation Product_Type.Times (infixr "\<times>" 80)
+end
+
 syntax
   "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
 translations
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Jun 18 22:20:55 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Jun 19 12:14:31 2018 +0100
@@ -905,6 +905,11 @@
     using assms by (force intro: power_eq_imp_eq_base)
 qed
 
+lemma power_eq_1_iff:
+  fixes w :: "'a::real_normed_div_algebra"
+  shows "w ^ n = 1 \<Longrightarrow> norm w = 1 \<or> n = 0"
+  by (metis norm_one power_0_left power_eq_0_iff power_eq_imp_eq_norm power_one)
+
 lemma norm_mult_numeral1 [simp]: "norm (numeral w * a) = numeral w * norm a"
   for a b :: "'a::{real_normed_field,field}"
   by (simp add: norm_mult)