# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1666801332 -3600
# Node ID 934d4aed8497a69b098fc35105e58e346f0116f7
# Parent  089e546f671f2182e2dc95e8d20a9b5ed6a2841f
A couple of new theorems. Also additional coercions to the complex numbers

diff -r 089e546f671f -r 934d4aed8497 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Oct 26 00:30:50 2022 +0200
+++ b/src/HOL/Complex.thy	Wed Oct 26 17:22:12 2022 +0100
@@ -143,14 +143,23 @@
 
 subsection \<open>Numerals, Arithmetic, and Embedding from R\<close>
 
-abbreviation complex_of_real :: "real \<Rightarrow> complex"
-  where "complex_of_real \<equiv> of_real"
-
 declare [[coercion "of_real :: real \<Rightarrow> complex"]]
 declare [[coercion "of_rat :: rat \<Rightarrow> complex"]]
 declare [[coercion "of_int :: int \<Rightarrow> complex"]]
 declare [[coercion "of_nat :: nat \<Rightarrow> complex"]]
 
+abbreviation complex_of_nat::"nat \<Rightarrow> complex"
+  where "complex_of_nat \<equiv> of_nat"
+
+abbreviation complex_of_int::"int \<Rightarrow> complex"
+  where "complex_of_int \<equiv> of_int"
+
+abbreviation complex_of_rat::"rat \<Rightarrow> complex"
+  where "complex_of_rat \<equiv> of_rat"
+
+abbreviation complex_of_real :: "real \<Rightarrow> complex"
+  where "complex_of_real \<equiv> of_real"
+
 lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n"
   by (induct n) simp_all
 
@@ -1312,4 +1321,28 @@
 lemma Complex_in_Reals: "Complex x 0 \<in> \<real>"
   by (metis Reals_of_real complex_of_real_def)
 
+text \<open>Express a complex number as a linear combination of two others, not collinear with the origin\<close>
+lemma complex_axes:
+  assumes "Im (y/x) \<noteq> 0"
+  obtains a b where "z = of_real a * x + of_real b * y"
+proof -
+  define dd where "dd \<equiv> Re y * Im x -  Im y * Re x"
+  define a where "a = (Im z * Re y - Re z * Im y) / dd"
+  define b where "b = (Re z * Im x - Im z * Re x) / dd"
+  have "dd \<noteq> 0" 
+    using assms by (auto simp: dd_def Im_complex_div_eq_0)
+  have "a * Re x + b * Re y = Re z"
+    using \<open>dd \<noteq> 0\<close>  
+    apply (simp add: a_def b_def field_simps)
+    by (metis dd_def diff_add_cancel distrib_right mult.assoc mult.commute)
+  moreover have "a * Im x + b * Im y = Im z"
+    using \<open>dd \<noteq> 0\<close> 
+    apply (simp add: a_def b_def field_simps)
+    by (metis (no_types) dd_def diff_add_cancel distrib_right mult.assoc mult.commute)
+  ultimately have "z = of_real a * x + of_real b * y"
+    by (simp add: complex_eqI)
+  then show ?thesis using that by simp
+qed
+
+
 end
diff -r 089e546f671f -r 934d4aed8497 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Oct 26 00:30:50 2022 +0200
+++ b/src/HOL/List.thy	Wed Oct 26 17:22:12 2022 +0100
@@ -1743,7 +1743,6 @@
 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
   by(cases xs) simp_all
 
-
 lemma list_eq_iff_nth_eq:
   "(xs = ys) = (length xs = length ys \<and> (\<forall>i<length xs. xs!i = ys!i))"
 proof (induct xs arbitrary: ys)
@@ -1751,11 +1750,14 @@
   show ?case
   proof (cases ys)
     case (Cons y ys)
-    then show ?thesis
-      using Cons.hyps by fastforce
+    with Cons.hyps show ?thesis by fastforce
   qed simp
 qed force
 
+lemma map_equality_iff:
+  "map f xs = map g ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>i<length ys. f (xs!i) = g (ys!i))"
+  by (fastforce simp: list_eq_iff_nth_eq)
+
 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
 proof (induct xs)
   case (Cons x xs)