diff --git a/thys/Closest_Pair_Points/Common.thy b/thys/Closest_Pair_Points/Common.thy --- a/thys/Closest_Pair_Points/Common.thy +++ b/thys/Closest_Pair_Points/Common.thy @@ -1,1121 +1,1110 @@ section "Common" theory Common imports "HOL-Library.Going_To_Filter" "Akra_Bazzi.Akra_Bazzi_Method" "Akra_Bazzi.Akra_Bazzi_Approximation" "HOL-Library.Code_Target_Numeral" begin type_synonym point = "int * int" subsection "Auxiliary Functions and Lemmas" subsubsection "Landau Auxiliary" text \ The following lemma expresses a procedure for deriving complexity properties of the form @{prop"t \ O[m going_to at_top within A](f o m)"} where \<^item> \t\ is a (timing) function on same data domain (e.g. lists), \<^item> \m\ is a measure function on that data domain (e.g. length), \<^item> \t'\ is a function on @{typ nat}, \<^item> \A\ is the set of valid inputs for the data domain. One needs to show that \<^item> \t\ is bounded by @{term "t' o m"} for valid inputs \<^item> @{prop"t' \ O(f)"} to conclude the overall property @{prop"t \ O[m going_to at_top within A](f o m)"}. \ lemma bigo_measure_trans: fixes t :: "'a \ real" and t' :: "nat \ real" and m :: "'a \ nat" and f ::"nat \ real" assumes "\x. x \ A \ t x \ (t' o m) x" and "t' \ O(f)" and "\x. x \ A \ 0 \ t x" shows "t \ O[m going_to at_top within A](f o m)" proof - have 0: "\x. x \ A \ 0 \ (t' o m) x" by (meson assms(1,3) order_trans) have 1: "t \ O[m going_to at_top within A](t' o m)" apply(rule bigoI[where c=1]) using assms 0 by (simp add: eventually_inf_principal going_to_within_def) have 2: "t' o m \ O[m going_to at_top](f o m)" unfolding o_def going_to_def by(rule landau_o.big.filtercomap[OF assms(2)]) have 3: "t' o m \ O[m going_to at_top within A](f o m)" using landau_o.big.filter_mono[OF _2] going_to_mono[OF _subset_UNIV] by blast show ?thesis by(rule landau_o.big_trans[OF 1 3]) qed subsubsection "Miscellaneous Lemmas" lemma set_take_drop_i_le_j: "i \ j \ set xs = set (take j xs) \ set (drop i xs)" proof (induction xs arbitrary: i j) case (Cons x xs) show ?case proof (cases "i = 0") case True thus ?thesis using set_take_subset by force next case False hence "set xs = set (take (j - 1) xs) \ set (drop (i - 1) xs)" by (simp add: Cons diff_le_mono) moreover have "set (take j (x # xs)) = insert x (set (take (j - 1) xs))" using False Cons.prems by (auto simp: take_Cons') moreover have "set (drop i (x # xs)) = set (drop (i - 1) xs)" using False Cons.prems by (auto simp: drop_Cons') ultimately show ?thesis by auto qed qed simp lemma set_take_drop: "set xs = set (take n xs) \ set (drop n xs)" using set_take_drop_i_le_j by fast lemma assumes "sorted_wrt f xs" shows sorted_wrt_take: "sorted_wrt f (take n xs)" and sorted_wrt_drop: "sorted_wrt f (drop n xs)" proof - from assms have "sorted_wrt f (take n xs @ drop n xs)" by simp then show "sorted_wrt f (take n xs)" and "sorted_wrt f (drop n xs)" unfolding sorted_wrt_append by simp_all qed lemma sorted_wrt_filter: "sorted_wrt f xs \ sorted_wrt f (filter P xs)" by (induction xs) auto lemma sorted_wrt_take_drop: "sorted_wrt f xs \ \x \ set (take n xs). \y \ set (drop n xs). f x y" using sorted_wrt_append[of f "take n xs" "drop n xs"] by simp lemma sorted_wrt_hd_less: assumes "sorted_wrt f xs" "\x. f x x" shows "\x \ set xs. f (hd xs) x" using assms by (cases xs) auto lemma sorted_wrt_hd_less_take: assumes "sorted_wrt f (x # xs)" "\x. f x x" shows "\y \ set (take n (x # xs)). f x y" using assms sorted_wrt_hd_less in_set_takeD by fastforce lemma sorted_wrt_take_less_hd_drop: assumes "sorted_wrt f xs" "n < length xs" shows "\x \ set (take n xs). f x (hd (drop n xs))" using sorted_wrt_take_drop assms by fastforce lemma sorted_wrt_hd_drop_less_drop: assumes "sorted_wrt f xs" "\x. f x x" shows "\x \ set (drop n xs). f (hd (drop n xs)) x" using assms sorted_wrt_drop sorted_wrt_hd_less by blast lemma length_filter_P_impl_Q: "(\x. P x \ Q x) \ length (filter P xs) \ length (filter Q xs)" by (induction xs) auto lemma filter_Un: "set xs = A \ B \ set (filter P xs) = { x \ A. P x } \ { x \ B. P x }" apply (induction xs) apply (auto) by (metis UnI1 UnI2 insert_iff)+ subsubsection \@{const length}\ fun t_length :: "'a list \ nat" where "t_length [] = 0" | "t_length (x#xs) = 1 + t_length xs" lemma t_length: "t_length xs = length xs" by (induction xs) auto fun length_it' :: "nat \ 'a list \ nat" where "length_it' acc [] = acc" | "length_it' acc (x#xs) = length_it' (acc+1) xs" definition length_it :: "'a list \ nat" where "length_it xs = length_it' 0 xs" lemma length_conv_length_it': "length xs + acc = length_it' acc xs" by (induction acc xs rule: length_it'.induct) auto lemma length_conv_length_it[code_unfold]: "length xs = length_it xs" unfolding length_it_def using length_conv_length_it' add_0_right by metis subsubsection \@{const rev}\ fun rev_it' :: "'a list \ 'a list \ 'a list" where "rev_it' acc [] = acc" | "rev_it' acc (x#xs) = rev_it' (x#acc) xs" definition rev_it :: "'a list \ 'a list" where "rev_it xs = rev_it' [] xs" lemma rev_conv_rev_it': "rev xs @ acc = rev_it' acc xs" by (induction acc xs rule: rev_it'.induct) auto lemma rev_conv_rev_it[code_unfold]: "rev xs = rev_it xs" unfolding rev_it_def using rev_conv_rev_it' append_Nil2 by metis subsubsection \@{const take}\ fun t_take :: "nat \ 'a list \ nat" where "t_take n [] = 0" | "t_take n (x#xs) = 1 + ( case n of 0 \ 0 | Suc m \ t_take m xs )" lemma t_take: "t_take n xs \ min (n + 1) (length xs)" by (induction xs arbitrary: n) (auto split: nat.split) subsubsection \@{const filter}\ fun t_filter :: "('a \ bool) \ 'a list \ nat" where "t_filter P [] = 0" | "t_filter P (x#xs) = 1 + (if P x then t_filter P xs else t_filter P xs)" lemma t_filter: "t_filter P xs = length xs" by (induction xs) auto fun filter_it' :: "'a list \ ('a \ bool) \ 'a list \ 'a list" where "filter_it' acc P [] = rev acc" | "filter_it' acc P (x#xs) = ( if P x then filter_it' (x#acc) P xs else filter_it' acc P xs )" definition filter_it :: "('a \ bool) \ 'a list \ 'a list" where "filter_it P xs = filter_it' [] P xs" lemma filter_conv_filter_it': "rev acc @ filter P xs = filter_it' acc P xs" by (induction acc P xs rule: filter_it'.induct) auto lemma filter_conv_filter_it[code_unfold]: "filter P xs = filter_it P xs" unfolding filter_it_def using filter_conv_filter_it' append_Nil rev.simps(1) by metis subsubsection \\split_at\\ fun split_at :: "nat \ 'a list \ ('a list * 'a list)" where "split_at n [] = ([], [])" | "split_at n (x # xs) = ( case n of 0 \ ([], x # xs) | Suc m \ let (xs', ys') = split_at m xs in (x # xs', ys') )" lemma split_at_take_drop_conv: "split_at n xs = (take n xs, drop n xs)" by (induction xs arbitrary: n) (auto split: nat.split) fun t_split_at :: "nat \ 'a list \ nat" where "t_split_at n [] = 0" | "t_split_at n (x#xs) = 1 + ( case n of 0 \ 0 | Suc m \ t_split_at m xs )" lemma t_split_at: "t_split_at n xs \ length xs" by (induction xs arbitrary: n) (auto split: nat.split) fun split_at_it' :: "'a list \ nat \ 'a list \ ('a list * 'a list)" where "split_at_it' acc n [] = (rev acc, [])" | "split_at_it' acc n (x#xs) = ( case n of 0 \ (rev acc, x#xs) | Suc m \ split_at_it' (x#acc) m xs )" definition split_at_it :: "nat \ 'a list \ ('a list * 'a list)" where "split_at_it n xs = split_at_it' [] n xs" lemma split_at_conv_split_at_it': assumes "(ts, ds) = split_at n xs" "(tsi, dsi) = split_at_it' acc n xs" shows "rev acc @ ts = tsi" and "ds = dsi" using assms apply (induction acc n xs arbitrary: ts rule: split_at_it'.induct) apply (auto simp: split_at.simps split: prod.splits nat.splits) done lemma split_at_conv_split_at_it_prod: assumes "(ts, ds) = split_at n xs" "(ts', ds') = split_at_it n xs" shows "(ts, ds) = (ts', ds')" using assms unfolding split_at_it_def using split_at_conv_split_at_it' rev.simps(1) append_Nil by fast+ lemma split_at_conv_split_at_it[code_unfold]: "split_at n xs = split_at_it n xs" using split_at_conv_split_at_it_prod surj_pair by metis subsection "Mergesort" subsubsection "Functional Correctness Proof" definition sorted_fst :: "point list \ bool" where "sorted_fst ps = sorted_wrt (\p\<^sub>0 p\<^sub>1. fst p\<^sub>0 \ fst p\<^sub>1) ps" definition sorted_snd :: "point list \ bool" where "sorted_snd ps = sorted_wrt (\p\<^sub>0 p\<^sub>1. snd p\<^sub>0 \ snd p\<^sub>1) ps" fun merge :: "('b \ 'a::linorder) \ 'b list \ 'b list \ 'b list" where "merge f (x # xs) (y # ys) = ( if f x \ f y then x # merge f xs (y # ys) else y # merge f (x # xs) ys )" | "merge f [] ys = ys" | "merge f xs [] = xs" lemma length_merge: "length (merge f xs ys) = length xs + length ys" by (induction f xs ys rule: merge.induct) auto lemma set_merge: "set (merge f xs ys) = set xs \ set ys" by (induction f xs ys rule: merge.induct) auto lemma distinct_merge: assumes "set xs \ set ys = {}" "distinct xs" "distinct ys" shows "distinct (merge f xs ys)" using assms by (induction f xs ys rule: merge.induct) (auto simp: set_merge) lemma sorted_merge: assumes "P = (\x y. f x \ f y)" shows "sorted_wrt P (merge f xs ys) \ sorted_wrt P xs \ sorted_wrt P ys" using assms by (induction f xs ys rule: merge.induct) (auto simp: set_merge) function mergesort :: "('b \ 'a::linorder) \ 'b list \ 'b list" where "mergesort f [] = []" | "mergesort f [x] = [x]" | "mergesort f (x # y # xs') = ( let xs = x # y # xs' in let n = length xs div 2 in let (l, r) = split_at n xs in merge f (mergesort f l) (mergesort f r) )" by pat_completeness auto termination mergesort apply (relation "Wellfounded.measure (\(_, xs). length xs)") apply (auto simp: split_at_take_drop_conv Let_def) done lemma sorted_wrt_mergesort: "sorted_wrt (\x y. f x \ f y) (mergesort f xs)" by (induction f xs rule: mergesort.induct) (auto simp: split_at_take_drop_conv sorted_merge) lemma set_mergesort: "set (mergesort f xs) = set xs" apply (induction f xs rule: mergesort.induct) apply (simp_all add: set_merge split_at_take_drop_conv) using set_take_drop by (metis list.simps(15)) lemma length_mergesort: "length (mergesort f xs) = length xs" by (induction f xs rule: mergesort.induct) (auto simp: length_merge split_at_take_drop_conv) lemma distinct_mergesort: "distinct xs \ distinct (mergesort f xs)" proof (induction f xs rule: mergesort.induct) case (3 f x y xs) let ?xs' = "x # y # xs" obtain l r where lr_def: "(l, r) = split_at (length ?xs' div 2) ?xs'" by (metis surj_pair) have "distinct l" "distinct r" using "3.prems" split_at_take_drop_conv distinct_take distinct_drop lr_def by (metis prod.sel)+ hence "distinct (mergesort f l)" "distinct (mergesort f r)" using "3.IH" lr_def by auto moreover have "set l \ set r = {}" using "3.prems" split_at_take_drop_conv lr_def by (metis append_take_drop_id distinct_append prod.sel) ultimately show ?case using lr_def by (auto simp: distinct_merge set_mergesort split: prod.splits) qed auto lemmas mergesort = sorted_wrt_mergesort set_mergesort length_mergesort distinct_mergesort lemma sorted_fst_take_less_hd_drop: assumes "sorted_fst ps" "n < length ps" shows "\p \ set (take n ps). fst p \ fst (hd (drop n ps))" using assms sorted_wrt_take_less_hd_drop[of "\p\<^sub>0 p\<^sub>1. fst p\<^sub>0 \ fst p\<^sub>1"] sorted_fst_def by fastforce lemma sorted_fst_hd_drop_less_drop: assumes "sorted_fst ps" shows "\p \ set (drop n ps). fst (hd (drop n ps)) \ fst p" using assms sorted_wrt_hd_drop_less_drop[of "\p\<^sub>0 p\<^sub>1. fst p\<^sub>0 \ fst p\<^sub>1"] sorted_fst_def by fastforce subsubsection "Time Complexity Proof" fun t_merge' :: "('b \ 'a::linorder) \ 'b list \ 'b list \ nat" where "t_merge' f (x#xs) (y#ys) = 1 + ( if f x \ f y then t_merge' f xs (y#ys) else t_merge' f (x#xs) ys )" | "t_merge' f xs [] = 0" | "t_merge' f [] ys = 0" definition t_merge :: "('b \ 'a::linorder) \ ('b list * 'b list) \ nat" where "t_merge f xys = t_merge' f (fst xys) (snd xys)" lemma t_merge: "t_merge f (xs, ys) \ length xs + length ys" unfolding t_merge_def by (induction f xs ys rule: t_merge'.induct) auto function t_mergesort :: "('b \ 'a::linorder) \ 'b list \ nat" where "t_mergesort f [] = 0" | "t_mergesort f [_] = 1" | "t_mergesort f (x # y # xs') = ( let xs = x # y # xs' in let (l, r) = split_at (length xs div 2) xs in t_length xs + t_split_at (length xs div 2) xs + t_mergesort f l + t_mergesort f r + t_merge f (l, r) )" by pat_completeness auto termination t_mergesort apply (relation "Wellfounded.measure (\(_, xs). length xs)") apply (auto simp: split_at_take_drop_conv Let_def) done function mergesort_recurrence :: "nat \ real" where "mergesort_recurrence 0 = 0" | "mergesort_recurrence 1 = 1" | "2 \ n \ mergesort_recurrence n = mergesort_recurrence (nat \real n / 2\) + mergesort_recurrence (nat \real n / 2\) + 3 * n" by force simp_all termination by akra_bazzi_termination simp_all lemma mergesort_recurrence_nonneg[simp]: "0 \ mergesort_recurrence n" by (induction n rule: mergesort_recurrence.induct) (auto simp del: One_nat_def) lemma t_mergesort_conv_mergesort_recurrence: "t_mergesort f xs \ mergesort_recurrence (length xs)" proof (induction f xs rule: t_mergesort.induct) case (2 f x) thus ?case using mergesort_recurrence.simps(2) by auto next case (3 f x y xs') define XS where "XS = x # y # xs'" define N where "N = length XS" obtain L R where LR_def: "(L, R) = split_at (N div 2) XS" using prod.collapse by blast note defs = XS_def N_def LR_def let ?LHS = "t_length XS + t_split_at (N div 2) XS + t_mergesort f L + t_mergesort f R + t_merge f (L, R)" let ?RHS = "mergesort_recurrence (nat \real N / 2\) + mergesort_recurrence (nat \real N / 2\) + 3 * N" have IHL: "t_mergesort f L \ mergesort_recurrence (length L)" using defs "3.IH"(1) prod.collapse by blast have IHR: "t_mergesort f R \ mergesort_recurrence (length R)" using defs "3.IH"(2) prod.collapse by blast have *: "length L = N div 2" "length R = N - N div 2" using defs by (auto simp: split_at_take_drop_conv) hence "(nat \real N / 2\) = length L" "(nat \real N / 2\) = length R" by linarith+ hence IH: "t_mergesort f L \ mergesort_recurrence (nat \real N / 2\)" "t_mergesort f R \ mergesort_recurrence (nat \real N / 2\)" using IHL IHR by simp_all have "N = length L + length R" using * by linarith hence "t_merge f (L, R) \ N" using t_merge by simp moreover have "t_length XS = N" using t_length N_def by blast moreover have "t_split_at (N div 2) XS \ N" using t_split_at N_def by blast ultimately have *: "?LHS \ ?RHS" using IH by simp moreover have "t_mergesort f XS = ?LHS" using defs by (auto simp: Let_def split: prod.split) moreover have "mergesort_recurrence N = ?RHS" by (simp add: defs) ultimately have "t_mergesort f XS \ mergesort_recurrence N" by presburger thus ?case using XS_def N_def by blast qed auto theorem mergesort_recurrence: "mergesort_recurrence \ \(\n. n * ln n)" by (master_theorem) auto theorem t_mergesort_bigo: "t_mergesort f \ O[length going_to at_top]((\n. n * ln n) o length)" proof - have 0: "\xs. t_mergesort f xs \ (mergesort_recurrence o length) xs" unfolding comp_def using t_mergesort_conv_mergesort_recurrence by blast show ?thesis using bigo_measure_trans[OF 0] by (simp add: bigthetaD1 mergesort_recurrence) qed subsubsection "Code Export" lemma merge_xs_Nil[simp]: "merge f xs [] = xs" by (cases xs) auto fun merge_it' :: "('b \ 'a::linorder) \ 'b list \ 'b list \ 'b list \ 'b list" where "merge_it' f acc [] [] = rev acc" | "merge_it' f acc (x#xs) [] = merge_it' f (x#acc) xs []" | "merge_it' f acc [] (y#ys) = merge_it' f (y#acc) ys []" | "merge_it' f acc (x#xs) (y#ys) = ( if f x \ f y then merge_it' f (x#acc) xs (y#ys) else merge_it' f (y#acc) (x#xs) ys )" definition merge_it :: "('b \ 'a::linorder) \ 'b list \ 'b list \ 'b list" where "merge_it f xs ys = merge_it' f [] xs ys" lemma merge_conv_merge_it': "rev acc @ merge f xs ys = merge_it' f acc xs ys" by (induction f acc xs ys rule: merge_it'.induct) auto lemma merge_conv_merge_it[code_unfold]: "merge f xs ys = merge_it f xs ys" unfolding merge_it_def using merge_conv_merge_it' rev.simps(1) append_Nil by metis subsection "Minimal Distance" definition sparse :: "real \ point set \ bool" where "sparse \ ps \ (\p\<^sub>0 \ ps. \p\<^sub>1 \ ps. p\<^sub>0 \ p\<^sub>1 \ \ \ dist p\<^sub>0 p\<^sub>1)" lemma sparse_identity: assumes "sparse \ (set ps)" "\p \ set ps. \ \ dist p\<^sub>0 p" shows "sparse \ (set (p\<^sub>0 # ps))" using assms by (simp add: dist_commute sparse_def) lemma sparse_update: assumes "sparse \ (set ps)" assumes "dist p\<^sub>0 p\<^sub>1 \ \" "\p \ set ps. dist p\<^sub>0 p\<^sub>1 \ dist p\<^sub>0 p" shows "sparse (dist p\<^sub>0 p\<^sub>1) (set (p\<^sub>0 # ps))" using assms apply (auto simp: dist_commute sparse_def) by force+ lemma sparse_mono: "sparse \ P \ \ \ \ \ sparse \ P" unfolding sparse_def by fastforce subsection "Distance" lemma dist_transform: fixes p :: point and \ :: real and l :: int shows "dist p (l, snd p) < \ \ l - \ < fst p \ fst p < l + \" proof - have "dist p (l, snd p) = sqrt ((real_of_int (fst p) - l)\<^sup>2)" by (auto simp add: dist_prod_def dist_real_def prod.case_eq_if) thus ?thesis by auto qed fun dist_code :: "point \ point \ int" where "dist_code p\<^sub>0 p\<^sub>1 = (fst p\<^sub>0 - fst p\<^sub>1)\<^sup>2 + (snd p\<^sub>0 - snd p\<^sub>1)\<^sup>2" lemma dist_eq_sqrt_dist_code: fixes p\<^sub>0 :: point shows "dist p\<^sub>0 p\<^sub>1 = sqrt (dist_code p\<^sub>0 p\<^sub>1)" by (auto simp: dist_prod_def dist_real_def split: prod.splits) lemma dist_eq_dist_code_lt: fixes p\<^sub>0 :: point shows "dist p\<^sub>0 p\<^sub>1 < dist p\<^sub>2 p\<^sub>3 \ dist_code p\<^sub>0 p\<^sub>1 < dist_code p\<^sub>2 p\<^sub>3" using dist_eq_sqrt_dist_code real_sqrt_less_iff by presburger lemma dist_eq_dist_code_le: fixes p\<^sub>0 :: point shows "dist p\<^sub>0 p\<^sub>1 \ dist p\<^sub>2 p\<^sub>3 \ dist_code p\<^sub>0 p\<^sub>1 \ dist_code p\<^sub>2 p\<^sub>3" using dist_eq_sqrt_dist_code real_sqrt_le_iff by presburger lemma dist_eq_dist_code_abs_lt: fixes p\<^sub>0 :: point shows "\c\ < dist p\<^sub>0 p\<^sub>1 \ c\<^sup>2 < dist_code p\<^sub>0 p\<^sub>1" using dist_eq_sqrt_dist_code by (metis of_int_less_of_int_power_cancel_iff real_sqrt_abs real_sqrt_less_iff) lemma dist_eq_dist_code_abs_le: fixes p\<^sub>0 :: point shows "dist p\<^sub>0 p\<^sub>1 \ \c\ \ dist_code p\<^sub>0 p\<^sub>1 \ c\<^sup>2" using dist_eq_sqrt_dist_code by (metis of_int_power_le_of_int_cancel_iff real_sqrt_abs real_sqrt_le_iff) lemma dist_fst_abs: fixes p :: point and l :: int shows "dist p (l, snd p) = \fst p - l\" proof - have "dist p (l, snd p) = sqrt ((real_of_int (fst p) - l)\<^sup>2)" by (simp add: dist_prod_def dist_real_def prod.case_eq_if) thus ?thesis by simp qed declare dist_code.simps [simp del] subsection "Brute Force Closest Pair Algorithm" subsubsection "Functional Correctness Proof" fun find_closest_bf :: "point \ point list \ point" where "find_closest_bf _ [] = undefined" | "find_closest_bf _ [p] = p" | "find_closest_bf p (p\<^sub>0 # ps) = ( let p\<^sub>1 = find_closest_bf p ps in if dist p p\<^sub>0 < dist p p\<^sub>1 then p\<^sub>0 else p\<^sub>1 )" lemma find_closest_bf_set: "0 < length ps \ find_closest_bf p ps \ set ps" by (induction p ps rule: find_closest_bf.induct) (auto simp: Let_def split: prod.splits if_splits) lemma find_closest_bf_dist: "\q \ set ps. dist p (find_closest_bf p ps) \ dist p q" by (induction p ps rule: find_closest_bf.induct) (auto split: prod.splits) fun closest_pair_bf :: "point list \ (point * point)" where "closest_pair_bf [] = undefined" | "closest_pair_bf [_] = undefined" | "closest_pair_bf [p\<^sub>0, p\<^sub>1] = (p\<^sub>0, p\<^sub>1)" | "closest_pair_bf (p\<^sub>0 # ps) = ( let (c\<^sub>0, c\<^sub>1) = closest_pair_bf ps in let p\<^sub>1 = find_closest_bf p\<^sub>0 ps in if dist c\<^sub>0 c\<^sub>1 \ dist p\<^sub>0 p\<^sub>1 then (c\<^sub>0, c\<^sub>1) else (p\<^sub>0, p\<^sub>1) )" lemma closest_pair_bf_c0: "1 < length ps \ (c\<^sub>0, c\<^sub>1) = closest_pair_bf ps \ c\<^sub>0 \ set ps" by (induction ps arbitrary: c\<^sub>0 c\<^sub>1 rule: closest_pair_bf.induct) (auto simp: Let_def find_closest_bf_set split: if_splits prod.splits) lemma closest_pair_bf_c1: "1 < length ps \ (c\<^sub>0, c\<^sub>1) = closest_pair_bf ps \ c\<^sub>1 \ set ps" proof (induction ps arbitrary: c\<^sub>0 c\<^sub>1 rule: closest_pair_bf.induct) case (4 p\<^sub>0 p\<^sub>2 p\<^sub>3 ps) let ?ps = "p\<^sub>2 # p\<^sub>3 # ps" obtain c\<^sub>0 c\<^sub>1 where c\<^sub>0_def: "(c\<^sub>0, c\<^sub>1) = closest_pair_bf ?ps" using prod.collapse by blast define p\<^sub>1 where p\<^sub>1_def: "p\<^sub>1 = find_closest_bf p\<^sub>0 ?ps" note defs = c\<^sub>0_def p\<^sub>1_def have "c\<^sub>1 \ set ?ps" using "4.IH" defs by simp moreover have "p\<^sub>1 \ set ?ps" using find_closest_bf_set defs by blast ultimately show ?case using "4.prems"(2) defs by (auto simp: Let_def split: prod.splits if_splits) qed auto lemma closest_pair_bf_c0_ne_c1: "1 < length ps \ distinct ps \ (c\<^sub>0, c\<^sub>1) = closest_pair_bf ps \ c\<^sub>0 \ c\<^sub>1" proof (induction ps arbitrary: c\<^sub>0 c\<^sub>1 rule: closest_pair_bf.induct) case (4 p\<^sub>0 p\<^sub>2 p\<^sub>3 ps) let ?ps = "p\<^sub>2 # p\<^sub>3 # ps" obtain c\<^sub>0 c\<^sub>1 where c\<^sub>0_def: "(c\<^sub>0, c\<^sub>1) = closest_pair_bf ?ps" using prod.collapse by blast define p\<^sub>1 where p\<^sub>1_def: "p\<^sub>1 = find_closest_bf p\<^sub>0 ?ps" note defs = c\<^sub>0_def p\<^sub>1_def have "c\<^sub>0 \ c\<^sub>1" using "4.IH" "4.prems"(2) defs by simp moreover have "p\<^sub>0 \ p\<^sub>1" using find_closest_bf_set "4.prems"(2) defs by (metis distinct.simps(2) length_pos_if_in_set list.set_intros(1)) ultimately show ?case using "4.prems"(3) defs by (auto simp: Let_def split: prod.splits if_splits) qed auto lemmas closest_pair_bf_c0_c1 = closest_pair_bf_c0 closest_pair_bf_c1 closest_pair_bf_c0_ne_c1 lemma closest_pair_bf_dist: assumes "1 < length ps" "(c\<^sub>0, c\<^sub>1) = closest_pair_bf ps" shows "sparse (dist c\<^sub>0 c\<^sub>1) (set ps)" using assms proof (induction ps arbitrary: c\<^sub>0 c\<^sub>1 rule: closest_pair_bf.induct) case (4 p\<^sub>0 p\<^sub>2 p\<^sub>3 ps) let ?ps = "p\<^sub>2 # p\<^sub>3 # ps" obtain c\<^sub>0 c\<^sub>1 where c\<^sub>0_def: "(c\<^sub>0, c\<^sub>1) = closest_pair_bf ?ps" using prod.collapse by blast define p\<^sub>1 where p\<^sub>1_def: "p\<^sub>1 = find_closest_bf p\<^sub>0 ?ps" note defs = c\<^sub>0_def p\<^sub>1_def hence IH: "sparse (dist c\<^sub>0 c\<^sub>1) (set ?ps)" using 4 c\<^sub>0_def by simp have *: "\p \ set ?ps. (dist p\<^sub>0 p\<^sub>1) \ dist p\<^sub>0 p" using find_closest_bf_dist defs by blast show ?case proof (cases "dist c\<^sub>0 c\<^sub>1 \ dist p\<^sub>0 p\<^sub>1") case True hence "\p \ set ?ps. dist c\<^sub>0 c\<^sub>1 \ dist p\<^sub>0 p" using * by auto hence "sparse (dist c\<^sub>0 c\<^sub>1) (set (p\<^sub>0 # ?ps))" using sparse_identity IH by blast thus ?thesis using True "4.prems" defs by (auto split: prod.splits) next case False hence "sparse (dist p\<^sub>0 p\<^sub>1) (set (p\<^sub>0 # ?ps))" using sparse_update[of "dist c\<^sub>0 c\<^sub>1" ?ps p\<^sub>0 p\<^sub>1] IH * defs by argo thus ?thesis using False "4.prems" defs by (auto split: prod.splits) qed qed (auto simp: dist_commute sparse_def) subsubsection "Time Complexity Proof" fun t_find_closest_bf :: "point \ point list \ nat" where "t_find_closest_bf _ [] = 0" | "t_find_closest_bf _ [_] = 1" | "t_find_closest_bf p (p\<^sub>0 # ps) = 1 + ( let p\<^sub>1 = find_closest_bf p ps in t_find_closest_bf p ps + ( if dist p p\<^sub>0 < dist p p\<^sub>1 then 0 else 0 ) )" lemma t_find_closest_bf: "t_find_closest_bf p ps = length ps" by (induction p ps rule: t_find_closest_bf.induct) auto fun t_closest_pair_bf :: "point list \ nat" where "t_closest_pair_bf [] = 0" | "t_closest_pair_bf [_] = 1" | "t_closest_pair_bf [_, _] = 2" | "t_closest_pair_bf (p\<^sub>0 # ps) = 1 + ( let (c\<^sub>0, c\<^sub>1) = closest_pair_bf ps in t_closest_pair_bf ps + ( let p\<^sub>1 = find_closest_bf p\<^sub>0 ps in t_find_closest_bf p\<^sub>0 ps + ( if dist c\<^sub>0 c\<^sub>1 \ dist p\<^sub>0 p\<^sub>1 then 0 else 0 )) )" lemma t_closest_pair_bf: "t_closest_pair_bf ps \ length ps * length ps" proof (induction rule: t_closest_pair_bf.induct) case (4 p\<^sub>0 p\<^sub>2 p\<^sub>3 ps) let ?ps = "p\<^sub>2 # p\<^sub>3 # ps" have "t_closest_pair_bf ?ps \ length ?ps * length ?ps" using 4 prod_cases3 by metis thus ?case using "4.prems" t_find_closest_bf by simp qed auto subsubsection "Code Export" fun find_closest_bf_code :: "point \ point list \ (int * point)" where "find_closest_bf_code p [] = undefined" | "find_closest_bf_code p [p\<^sub>0] = (dist_code p p\<^sub>0, p\<^sub>0)" | "find_closest_bf_code p (p\<^sub>0 # ps) = ( let (\\<^sub>1, p\<^sub>1) = find_closest_bf_code p ps in let \\<^sub>0 = dist_code p p\<^sub>0 in if \\<^sub>0 < \\<^sub>1 then (\\<^sub>0, p\<^sub>0) else (\\<^sub>1, p\<^sub>1) )" lemma find_closest_bf_code_dist_eq: "0 < length ps \ (\, c) = find_closest_bf_code p ps \ \ = dist_code p c" by (induction p ps rule: find_closest_bf_code.induct) (auto simp: Let_def split: prod.splits if_splits) lemma find_closest_bf_code_eq: "0 < length ps \ c = find_closest_bf p ps \ (\', c') = find_closest_bf_code p ps \ c = c'" proof (induction p ps arbitrary: c \' c' rule: find_closest_bf.induct) case (3 p p\<^sub>0 p\<^sub>2 ps) define \\<^sub>0 \\<^sub>0' where \\<^sub>0_def: "\\<^sub>0 = dist p p\<^sub>0" "\\<^sub>0' = dist_code p p\<^sub>0" obtain \\<^sub>1 p\<^sub>1 \\<^sub>1' p\<^sub>1' where \\<^sub>1_def: "\\<^sub>1 = dist p p\<^sub>1" "p\<^sub>1 = find_closest_bf p (p\<^sub>2 # ps)" "(\\<^sub>1', p\<^sub>1') = find_closest_bf_code p (p\<^sub>2 # ps)" using prod.collapse by blast+ note defs = \\<^sub>0_def \\<^sub>1_def have *: "p\<^sub>1 = p\<^sub>1'" using "3.IH" defs by simp hence "\\<^sub>0 < \\<^sub>1 \ \\<^sub>0' < \\<^sub>1'" using find_closest_bf_code_dist_eq[of "p\<^sub>2 # ps" \\<^sub>1' p\<^sub>1' p] dist_eq_dist_code_lt defs by simp thus ?case using "3.prems"(2,3) * defs by (auto split: prod.splits) qed auto declare find_closest_bf_code.simps [simp del] fun closest_pair_bf_code :: "point list \ (int * point * point)" where "closest_pair_bf_code [] = undefined" | "closest_pair_bf_code [p\<^sub>0] = undefined" | "closest_pair_bf_code [p\<^sub>0, p\<^sub>1] = (dist_code p\<^sub>0 p\<^sub>1, p\<^sub>0, p\<^sub>1)" | "closest_pair_bf_code (p\<^sub>0 # ps) = ( let (\\<^sub>c, c\<^sub>0, c\<^sub>1) = closest_pair_bf_code ps in let (\\<^sub>p, p\<^sub>1) = find_closest_bf_code p\<^sub>0 ps in if \\<^sub>c \ \\<^sub>p then (\\<^sub>c, c\<^sub>0, c\<^sub>1) else (\\<^sub>p, p\<^sub>0, p\<^sub>1) )" lemma closest_pair_bf_code_dist_eq: "1 < length ps \ (\, c\<^sub>0, c\<^sub>1) = closest_pair_bf_code ps \ \ = dist_code c\<^sub>0 c\<^sub>1" proof (induction ps arbitrary: \ c\<^sub>0 c\<^sub>1 rule: closest_pair_bf_code.induct) case (4 p\<^sub>0 p\<^sub>2 p\<^sub>3 ps) let ?ps = "p\<^sub>2 # p\<^sub>3 # ps" obtain \\<^sub>c c\<^sub>0 c\<^sub>1 where \\<^sub>c_def: "(\\<^sub>c, c\<^sub>0, c\<^sub>1) = closest_pair_bf_code ?ps" by (metis prod_cases3) obtain \\<^sub>p p\<^sub>1 where \\<^sub>p_def: "(\\<^sub>p, p\<^sub>1) = find_closest_bf_code p\<^sub>0 ?ps" using prod.collapse by blast note defs = \\<^sub>c_def \\<^sub>p_def have "\\<^sub>c = dist_code c\<^sub>0 c\<^sub>1" using "4.IH" defs by simp moreover have "\\<^sub>p = dist_code p\<^sub>0 p\<^sub>1" using find_closest_bf_code_dist_eq defs by blast ultimately show ?case using "4.prems"(2) defs by (auto split: prod.splits if_splits) qed auto lemma closest_pair_bf_code_eq: assumes "1 < length ps" assumes "(c\<^sub>0, c\<^sub>1) = closest_pair_bf ps" "(\', c\<^sub>0', c\<^sub>1') = closest_pair_bf_code ps" shows "c\<^sub>0 = c\<^sub>0' \ c\<^sub>1 = c\<^sub>1'" using assms proof (induction ps arbitrary: c\<^sub>0 c\<^sub>1 \' c\<^sub>0' c\<^sub>1' rule: closest_pair_bf_code.induct) case (4 p\<^sub>0 p\<^sub>2 p\<^sub>3 ps) let ?ps = "p\<^sub>2 # p\<^sub>3 # ps" obtain c\<^sub>0 c\<^sub>1 \\<^sub>c' c\<^sub>0' c\<^sub>1' where \\<^sub>c_def: "(c\<^sub>0, c\<^sub>1) = closest_pair_bf ?ps" "(\\<^sub>c', c\<^sub>0', c\<^sub>1') = closest_pair_bf_code ?ps" by (metis prod_cases3) obtain p\<^sub>1 \\<^sub>p' p\<^sub>1' where \\<^sub>p_def: "p\<^sub>1 = find_closest_bf p\<^sub>0 ?ps" "(\\<^sub>p', p\<^sub>1') = find_closest_bf_code p\<^sub>0 ?ps" using prod.collapse by blast note defs = \\<^sub>c_def \\<^sub>p_def have A: "c\<^sub>0 = c\<^sub>0' \ c\<^sub>1 = c\<^sub>1'" using "4.IH" defs by simp moreover have B: "p\<^sub>1 = p\<^sub>1'" using find_closest_bf_code_eq defs by blast moreover have "\\<^sub>c' = dist_code c\<^sub>0' c\<^sub>1'" using defs closest_pair_bf_code_dist_eq[of ?ps] by simp moreover have "\\<^sub>p' = dist_code p\<^sub>0 p\<^sub>1'" using defs find_closest_bf_code_dist_eq by blast ultimately have "dist c\<^sub>0 c\<^sub>1 \ dist p\<^sub>0 p\<^sub>1 \ \\<^sub>c' \ \\<^sub>p'" by (simp add: dist_eq_dist_code_le) thus ?case using "4.prems"(2,3) defs A B by (auto simp: Let_def split: prod.splits) qed auto subsection "Geometry" subsubsection "Band Filter" lemma set_band_filter_aux: fixes \ :: real and ps :: "point list" assumes "p\<^sub>0 \ ps\<^sub>L" "p\<^sub>1 \ ps\<^sub>R" "p\<^sub>0 \ p\<^sub>1" "dist p\<^sub>0 p\<^sub>1 < \" "set ps = ps\<^sub>L \ ps\<^sub>R" assumes "\p \ ps\<^sub>L. fst p \ l" "\p \ ps\<^sub>R. l \ fst p" assumes "ps' = filter (\p. l - \ < fst p \ fst p < l + \) ps" shows "p\<^sub>0 \ set ps' \ p\<^sub>1 \ set ps'" proof (rule ccontr) assume "\ (p\<^sub>0 \ set ps' \ p\<^sub>1 \ set ps')" then consider (A) "p\<^sub>0 \ set ps' \ p\<^sub>1 \ set ps'" | (B) "p\<^sub>0 \ set ps' \ p\<^sub>1 \ set ps'" | (C) "p\<^sub>0 \ set ps' \ p\<^sub>1 \ set ps'" by blast thus False proof cases case A hence "fst p\<^sub>0 \ l - \ \ l + \ \ fst p\<^sub>0" "fst p\<^sub>1 \ l - \ \ l + \ \ fst p\<^sub>1" using assms(1,2,5,8) by auto hence "fst p\<^sub>0 \ l - \" "l + \ \ fst p\<^sub>1" using assms(1,2,6,7) by force+ hence "\ \ dist (fst p\<^sub>0) (fst p\<^sub>1)" using dist_real_def by simp hence "\ \ dist p\<^sub>0 p\<^sub>1" using dist_fst_le[of p\<^sub>0 p\<^sub>1] by (auto split: prod.splits) then show ?thesis using assms(4) by fastforce next case B hence "fst p\<^sub>1 \ l - \ \ l + \ \ fst p\<^sub>1" using assms(2,5,8) by auto hence "l + \ \ fst p\<^sub>1" using assms(2,7) by auto moreover have "fst p\<^sub>0 \ l" using assms(1,6) by simp ultimately have "\ \ dist (fst p\<^sub>0) (fst p\<^sub>1)" using dist_real_def by simp hence "\ \ dist p\<^sub>0 p\<^sub>1" using dist_fst_le[of p\<^sub>0 p\<^sub>1] less_le_trans by (auto split: prod.splits) thus ?thesis using assms(4) by simp next case C hence "fst p\<^sub>0 \ l - \ \ l + \ \ fst p\<^sub>0" using assms(1,2,5,8) by auto hence "fst p\<^sub>0 \ l - \" using assms(1,6) by auto moreover have "l \ fst p\<^sub>1" using assms(2,7) by simp ultimately have "\ \ dist (fst p\<^sub>0) (fst p\<^sub>1)" using dist_real_def by simp hence "\ \ dist p\<^sub>0 p\<^sub>1" using dist_fst_le[of p\<^sub>0 p\<^sub>1] less_le_trans by (auto split: prod.splits) thus ?thesis using assms(4) by simp qed qed lemma set_band_filter: fixes \ :: real and ps :: "point list" assumes "p\<^sub>0 \ set ps" "p\<^sub>1 \ set ps" "p\<^sub>0 \ p\<^sub>1" "dist p\<^sub>0 p\<^sub>1 < \" "set ps = ps\<^sub>L \ ps\<^sub>R" assumes "sparse \ ps\<^sub>L" "sparse \ ps\<^sub>R" assumes "\p \ ps\<^sub>L. fst p \ l" "\p \ ps\<^sub>R. l \ fst p" assumes "ps' = filter (\p. l - \ < fst p \ fst p < l + \) ps" shows "p\<^sub>0 \ set ps' \ p\<^sub>1 \ set ps'" proof - have "p\<^sub>0 \ ps\<^sub>L \ p\<^sub>1 \ ps\<^sub>L" "p\<^sub>0 \ ps\<^sub>R \ p\<^sub>1 \ ps\<^sub>R" using assms(3,4,6,7) sparse_def by force+ then consider (A) "p\<^sub>0 \ ps\<^sub>L \ p\<^sub>1 \ ps\<^sub>R" | (B) "p\<^sub>0 \ ps\<^sub>R \ p\<^sub>1 \ ps\<^sub>L" using assms(1,2,5) by auto thus ?thesis proof cases case A thus ?thesis using set_band_filter_aux assms(3,4,5,8,9,10) by (auto split: prod.splits) next case B moreover have "dist p\<^sub>1 p\<^sub>0 < \" using assms(4) dist_commute by metis ultimately show ?thesis using set_band_filter_aux assms(3)[symmetric] assms(5,8,9,10) by (auto split: prod.splits) qed qed subsubsection "2D-Boxes and Points" lemma cbox_2D: fixes x\<^sub>0 :: real and y\<^sub>0 :: real shows "cbox (x\<^sub>0, y\<^sub>0) (x\<^sub>1, y\<^sub>1) = { (x, y). x\<^sub>0 \ x \ x \ x\<^sub>1 \ y\<^sub>0 \ y \ y \ y\<^sub>1 }" by fastforce lemma mem_cbox_2D: fixes x :: real and y :: real shows "x\<^sub>0 \ x \ x \ x\<^sub>1 \ y\<^sub>0 \ y \ y \ y\<^sub>1 \ (x, y) \ cbox (x\<^sub>0, y\<^sub>0) (x\<^sub>1, y\<^sub>1)" by fastforce lemma cbox_top_un: fixes x\<^sub>0 :: real and y\<^sub>0 :: real assumes "y\<^sub>0 \ y\<^sub>1" "y\<^sub>1 \ y\<^sub>2" shows "cbox (x\<^sub>0, y\<^sub>0) (x\<^sub>1, y\<^sub>1) \ cbox (x\<^sub>0, y\<^sub>1) (x\<^sub>1, y\<^sub>2) = cbox (x\<^sub>0, y\<^sub>0) (x\<^sub>1, y\<^sub>2)" using assms by auto lemma cbox_right_un: fixes x\<^sub>0 :: real and y\<^sub>0 :: real assumes "x\<^sub>0 \ x\<^sub>1" "x\<^sub>1 \ x\<^sub>2" shows "cbox (x\<^sub>0, y\<^sub>0) (x\<^sub>1, y\<^sub>1) \ cbox (x\<^sub>1, y\<^sub>0) (x\<^sub>2, y\<^sub>1) = cbox (x\<^sub>0, y\<^sub>0) (x\<^sub>2, y\<^sub>1)" using assms by auto lemma cbox_max_dist: assumes "p\<^sub>0 = (x, y)" "p\<^sub>1 = (x + \, y + \)" assumes "(x\<^sub>0, y\<^sub>0) \ cbox p\<^sub>0 p\<^sub>1" "(x\<^sub>1, y\<^sub>1) \ cbox p\<^sub>0 p\<^sub>1" "0 \ \" shows "dist (x\<^sub>0, y\<^sub>0) (x\<^sub>1, y\<^sub>1) \ sqrt 2 * \" proof - have X: "dist x\<^sub>0 x\<^sub>1 \ \" using assms dist_real_def by auto have Y: "dist y\<^sub>0 y\<^sub>1 \ \" using assms dist_real_def by auto have "dist (x\<^sub>0, y\<^sub>0) (x\<^sub>1, y\<^sub>1) = sqrt ((dist x\<^sub>0 x\<^sub>1)\<^sup>2 + (dist y\<^sub>0 y\<^sub>1)\<^sup>2)" using dist_Pair_Pair by auto also have "... \ sqrt (\\<^sup>2 + (dist y\<^sub>0 y\<^sub>1)\<^sup>2)" using X power_mono by fastforce also have "... \ sqrt (\\<^sup>2 + \\<^sup>2)" using Y power_mono by fastforce also have "... = sqrt 2 * sqrt (\\<^sup>2)" using real_sqrt_mult by simp also have "... = sqrt 2 * \" using assms(5) by simp finally show ?thesis . qed subsubsection "Pigeonhole Argument" lemma card_le_1_if_pairwise_eq: - assumes "\x \ S. \y \ S. x = y" - shows "card S \ 1" -proof (rule ccontr) - assume "\ card S \ 1" - hence "2 \ card S" - by simp - then obtain T where *: "T \ S \ card T = 2" - using ex_card by metis - then obtain x y where "x \ T \ y \ T \ x \ y" - using card_2_exists by metis - then show False - using * assms by blast -qed + "\x \ S. \y \ S. x = y \ card S \ 1" +by (metis One_nat_def card_infinite card_le_Suc0_iff_eq le_0_eq le_SucI) lemma card_Int_if_either_in: assumes "\x \ S. \y \ S. x = y \ x \ T \ y \ T" shows "card (S \ T) \ 1" proof (rule ccontr) assume "\ (card (S \ T) \ 1)" then obtain x y where *: "x \ S \ T \ y \ S \ T \ x \ y" by (meson card_le_1_if_pairwise_eq) hence "x \ T" "y \ T" by simp_all moreover have "x \ T \ y \ T" using assms * by auto ultimately show False by blast qed lemma card_Int_Un_le_Sum_card_Int: assumes "finite S" shows "card (A \ \S) \ (\B \ S. card (A \ B))" using assms proof (induction "card S" arbitrary: S) case (Suc n) then obtain B T where *: "S = { B } \ T" "card T = n" "B \ T" by (metis card_Suc_eq Suc_eq_plus1 insert_is_Un) hence "card (A \ \S) = card (A \ \({ B } \ T))" by blast also have "... \ card (A \ B) + card (A \ \T)" by (simp add: card_Un_le inf_sup_distrib1) also have "... \ card (A \ B) + (\B \ T. card (A \ B))" using Suc * by simp also have "... \ (\B \ S. card (A \ B))" using Suc.prems * by simp finally show ?case . qed simp lemma pigeonhole: assumes "finite T" "S \ \T" "card T < card S" shows "\x \ S. \y \ S. \X \ T. x \ y \ x \ X \ y \ X" proof (rule ccontr) assume "\ (\x \ S. \y \ S. \X \ T. x \ y \ x \ X \ y \ X)" hence *: "\X \ T. card (S \ X) \ 1" using card_Int_if_either_in by metis have "card T < card (S \ \T)" using Int_absorb2 assms by fastforce also have "... \ (\X \ T. card (S \ X))" using assms(1) card_Int_Un_le_Sum_card_Int by blast also have "... \ card T" using * sum_mono by fastforce finally show False by simp qed subsubsection "Delta Sparse Points within a Square" lemma max_points_square: assumes "\p \ ps. p \ cbox (x, y) (x + \, y + \)" "sparse \ ps" "0 \ \" shows "card ps \ 4" proof (cases "\ = 0") case True hence "{ (x, y) } = cbox (x, y) (x + \, y + \)" using cbox_def by simp hence "\p \ ps. p = (x, y)" using assms(1) by blast hence "\p \ ps. \q \ ps. p = q" apply (auto split: prod.splits) by (metis of_int_eq_iff)+ thus ?thesis using card_le_1_if_pairwise_eq by force next case False hence \: "0 < \" using assms(3) by simp show ?thesis proof (rule ccontr) assume A: "\ (card ps \ 4)" define PS where PS_def: "PS = (\(x, y). (real_of_int x, real_of_int y)) ` ps" have "inj_on (\(x, y). (real_of_int x, real_of_int y)) ps" using inj_on_def by fastforce hence *: "\ (card PS \ 4)" using A PS_def by (simp add: card_image) let ?x' = "x + \ / 2" let ?y' = "y + \ / 2" let ?ll = "cbox ( x , y ) (?x' , ?y' )" let ?lu = "cbox ( x , ?y') (?x' , y + \)" let ?rl = "cbox (?x', y ) ( x + \, ?y' )" let ?ru = "cbox (?x', ?y') ( x + \, y + \)" let ?sq = "{ ?ll, ?lu, ?rl, ?ru }" have card_le_4: "card ?sq \ 4" by (simp add: card_insert_le_m1) have "cbox (x, y) (?x', y + \) = ?ll \ ?lu" using cbox_top_un assms(3) by auto moreover have "cbox (?x', y) (x + \, y + \) = ?rl \ ?ru" using cbox_top_un assms(3) by auto moreover have "cbox (x, y) (?x', y + \) \ cbox (?x', y) (x + \, y + \) = cbox (x, y) (x + \, y + \)" using cbox_right_un assms(3) by simp ultimately have "?ll \ ?lu \ ?rl \ ?ru = cbox (x, y) (x + \, y + \)" by blast hence "PS \ \(?sq)" using assms(1) PS_def by (auto split: prod.splits) moreover have "card ?sq < card PS" using * card_insert_le_m1 card_le_4 by linarith moreover have "finite ?sq" by simp ultimately have "\p\<^sub>0 \ PS. \p\<^sub>1 \ PS. \S \ ?sq. (p\<^sub>0 \ p\<^sub>1 \ p\<^sub>0 \ S \ p\<^sub>1 \ S)" using pigeonhole[of ?sq PS] by blast then obtain S p\<^sub>0 p\<^sub>1 where #: "p\<^sub>0 \ PS" "p\<^sub>1 \ PS" "S \ ?sq" "p\<^sub>0 \ p\<^sub>1" "p\<^sub>0 \ S" "p\<^sub>1 \ S" by blast have D: "0 \ \ / 2" using assms(3) by simp have LL: "\p\<^sub>0 \ ?ll. \p\<^sub>1 \ ?ll. dist p\<^sub>0 p\<^sub>1 \ sqrt 2 * (\ / 2)" using cbox_max_dist[of "(x, y)" x y "(?x', ?y')" "\ / 2"] D by auto have LU: "\p\<^sub>0 \ ?lu. \p\<^sub>1 \ ?lu. dist p\<^sub>0 p\<^sub>1 \ sqrt 2 * (\ / 2)" using cbox_max_dist[of "(x, ?y')" x ?y' "(?x', y + \)" "\ / 2"] D by auto have RL: "\p\<^sub>0 \ ?rl. \p\<^sub>1 \ ?rl. dist p\<^sub>0 p\<^sub>1 \ sqrt 2 * (\ / 2)" using cbox_max_dist[of "(?x', y)" ?x' y "(x + \, ?y')" "\ / 2"] D by auto have RU: "\p\<^sub>0 \ ?ru. \p\<^sub>1 \ ?ru. dist p\<^sub>0 p\<^sub>1 \ sqrt 2 * (\ / 2)" using cbox_max_dist[of "(?x', ?y')" ?x' ?y' "(x + \, y + \)" "\ / 2"] D by auto have "\p\<^sub>0 \ S. \p\<^sub>1 \ S. dist p\<^sub>0 p\<^sub>1 \ sqrt 2 * (\ / 2)" using # LL LU RL RU by blast hence "dist p\<^sub>0 p\<^sub>1 \ (sqrt 2 / 2) * \" using # by simp moreover have "(sqrt 2 / 2) * \ < \" using sqrt2_less_2 \ by simp ultimately have "dist p\<^sub>0 p\<^sub>1 < \" by simp moreover have "\ \ dist p\<^sub>0 p\<^sub>1" using assms(2) # sparse_def PS_def by auto ultimately show False by simp qed qed end \ No newline at end of file diff --git a/thys/Complex_Geometry/Chordal_Metric.thy b/thys/Complex_Geometry/Chordal_Metric.thy --- a/thys/Complex_Geometry/Chordal_Metric.thy +++ b/thys/Complex_Geometry/Chordal_Metric.thy @@ -1,1725 +1,1725 @@ (* -------------------------------------------------------------------------- *) subsection \Chordal Metric\ (* -------------------------------------------------------------------------- *) text \Riemann sphere can be made a metric space. We are going to introduce distance on Riemann sphere and to prove that it is a metric space. The distance between two points on the sphere is defined as the length of the chord that connects them. This metric can be used in formalization of elliptic geometry.\ theory Chordal_Metric imports Homogeneous_Coordinates Riemann_Sphere Oriented_Circlines "HOL-Analysis.Inner_Product" "HOL-Analysis.Euclidean_Space" begin (* -------------------------------------------------------------------------- *) subsubsection \Inner product and norm\ (* -------------------------------------------------------------------------- *) definition inprod_cvec :: "complex_vec \ complex_vec \ complex" where [simp]: "inprod_cvec z w = (let (z1, z2) = z; (w1, w2) = w in vec_cnj (z1, z2) *\<^sub>v\<^sub>v (w1, w2))" syntax "_inprod_cvec" :: "complex_vec \ complex_vec \ complex" ("\_,_\") translations "\z,w\" == "CONST inprod_cvec z w" lemma real_inprod_cvec [simp]: shows "is_real \z,z\" by (cases z, simp add: vec_cnj_def) lemma inprod_cvec_ge_zero [simp]: shows "Re \z,z\ \ 0" by (cases z, simp add: vec_cnj_def) lemma inprod_cvec_bilinear1 [simp]: assumes "z' = k *\<^sub>s\<^sub>v z" shows "\z',w\ = cnj k * \z,w\" using assms by (cases z, cases z', cases w) (simp add: vec_cnj_def field_simps) lemma inprod_cvec_bilinear2 [simp]: assumes "z' = k *\<^sub>s\<^sub>v z" shows "\w, z'\ = k * \w, z\" using assms by (cases z, cases z', cases w) (simp add: vec_cnj_def field_simps) lemma inprod_cvec_g_zero [simp]: assumes "z \ vec_zero" shows "Re \z, z\ > 0" proof- have "\ a b. a \ 0 \ b \ 0 \ 0 < (Re a * Re a + Im a * Im a) + (Re b * Re b + Im b * Im b)" by (smt complex_eq_0 not_sum_squares_lt_zero power2_eq_square) thus ?thesis using assms by (cases z, simp add: vec_cnj_def) qed definition norm_cvec :: "complex_vec \ real" where [simp]: "norm_cvec z = sqrt (Re \z,z\)" syntax "_norm_cvec" :: "complex_vec \ complex" ("\_\") translations "\z\" == "CONST norm_cvec z" lemma norm_cvec_square: shows "\z\\<^sup>2 = Re (\z,z\)" by (simp del: inprod_cvec_def) lemma norm_cvec_gt_0: assumes "z \ vec_zero" shows "\z\ > 0" using assms by (simp del: inprod_cvec_def) lemma norm_cvec_scale: assumes "z' = k *\<^sub>s\<^sub>v z" shows "\z'\\<^sup>2 = Re (cnj k * k) * \z\\<^sup>2" unfolding norm_cvec_square using inprod_cvec_bilinear1[OF assms, of z'] using inprod_cvec_bilinear2[OF assms, of z] by (simp del: inprod_cvec_def add: field_simps) lift_definition inprod_hcoords :: "complex_homo_coords \ complex_homo_coords \ complex" is inprod_cvec done lift_definition norm_hcoords :: "complex_homo_coords \ real" is norm_cvec done (* -------------------------------------------------------------------------- *) subsubsection \Distance in $\mathbb{C}P^1$ - defined by Fubini-Study metric.\ (* -------------------------------------------------------------------------- *) text \Formula for the chordal distance between the two points can be given directly based on the homogenous coordinates of their stereographic projections in the plane. This is called the Fubini-Study metric.\ definition dist_fs_cvec :: "complex_vec \ complex_vec \ real" where [simp]: "dist_fs_cvec z1 z2 = (let (z1x, z1y) = z1; (z2x, z2y) = z2; num = (z1x*z2y - z2x*z1y) * (cnj z1x*cnj z2y - cnj z2x*cnj z1y); den = (z1x*cnj z1x + z1y*cnj z1y) * (z2x*cnj z2x + z2y*cnj z2y) in 2*sqrt(Re num / Re den))" lemma dist_fs_cvec_iff: assumes "z \ vec_zero" and "w \ vec_zero" shows "dist_fs_cvec z w = 2*sqrt(1 - (cmod \z,w\)\<^sup>2 / (\z\\<^sup>2 * \w\\<^sup>2))" proof- obtain z1 z2 w1 w2 where *: "z = (z1, z2)" "w = (w1, w2)" by (cases "z", cases "w") auto have 1: "2*sqrt(1 - (cmod \z,w\)\<^sup>2 / (\z\\<^sup>2 * \w\\<^sup>2)) = 2*sqrt((\z\\<^sup>2 * \w\\<^sup>2 - (cmod \z,w\)\<^sup>2) / (\z\\<^sup>2 * \w\\<^sup>2))" using norm_cvec_gt_0[of z] norm_cvec_gt_0[of w] assms by (simp add: field_simps) have 2: "\z\\<^sup>2 * \w\\<^sup>2 = Re ((z1*cnj z1 + z2*cnj z2) * (w1*cnj w1 + w2*cnj w2))" using assms * by (simp add: vec_cnj_def) have 3: "\z\\<^sup>2 * \w\\<^sup>2 - (cmod \z,w\)\<^sup>2 = Re ((z1*w2 - w1*z2) * (cnj z1*cnj w2 - cnj w1*cnj z2))" apply (subst cmod_square, (subst norm_cvec_square)+) using * by (simp add: vec_cnj_def field_simps) thus ?thesis using 1 2 3 using * unfolding dist_fs_cvec_def Let_def by simp qed lift_definition dist_fs_hcoords :: "complex_homo_coords \ complex_homo_coords \ real" is dist_fs_cvec done lift_definition dist_fs :: "complex_homo \ complex_homo \ real" is dist_fs_hcoords proof transfer fix z1 z2 z1' z2' :: complex_vec obtain z1x z1y z2x z2y z1'x z1'y z2'x z2'y where zz: "z1 = (z1x, z1y)" "z2 = (z2x, z2y)" "z1' = (z1'x, z1'y)" "z2' = (z2'x, z2'y)" by (cases "z1", cases "z2", cases "z1'", cases "z2'") blast assume 1: "z1 \ vec_zero" "z2 \ vec_zero" "z1' \ vec_zero" "z2' \ vec_zero" "z1 \\<^sub>v z1'" "z2 \\<^sub>v z2'" then obtain k1 k2 where *: "k1 \ 0" "z1' = k1 *\<^sub>s\<^sub>v z1" and **: "k2 \ 0" "z2' = k2 *\<^sub>s\<^sub>v z2" by auto have "(cmod \z1,z2\)\<^sup>2 / (\z1\\<^sup>2 * \z2\\<^sup>2) = (cmod \z1',z2'\)\<^sup>2 / (\z1'\\<^sup>2 * \z2'\\<^sup>2)" using \k1 \ 0\ \k2 \ 0\ using cmod_square[symmetric, of k1] cmod_square[symmetric, of k2] apply (subst norm_cvec_scale[OF *(2)]) apply (subst norm_cvec_scale[OF **(2)]) apply (subst inprod_cvec_bilinear1[OF *(2)]) apply (subst inprod_cvec_bilinear2[OF **(2)]) by (simp add: power2_eq_square) thus "dist_fs_cvec z1 z2 = dist_fs_cvec z1' z2'" using 1 dist_fs_cvec_iff by simp qed lemma dist_fs_finite: shows "dist_fs (of_complex z1) (of_complex z2) = 2 * cmod(z1 - z2) / (sqrt (1+(cmod z1)\<^sup>2) * sqrt (1+(cmod z2)\<^sup>2))" apply transfer apply transfer apply (subst cmod_square)+ apply (simp add: real_sqrt_divide cmod_def power2_eq_square) apply (subst real_sqrt_mult[symmetric]) apply (simp add: field_simps) done lemma dist_fs_infinite1: shows "dist_fs (of_complex z1) \\<^sub>h = 2 / sqrt (1+(cmod z1)\<^sup>2)" by (transfer, transfer) (subst cmod_square, simp add: real_sqrt_divide) lemma dist_fs_infinite2: shows "dist_fs \\<^sub>h (of_complex z1) = 2 / sqrt (1+(cmod z1)\<^sup>2)" by (transfer, transfer) (subst cmod_square, simp add: real_sqrt_divide) lemma dist_fs_cvec_zero: assumes "z \ vec_zero" and "w \ vec_zero" shows "dist_fs_cvec z w = 0 \ (cmod \z,w\)\<^sup>2 = (\z\\<^sup>2 * \w\\<^sup>2)" using assms norm_cvec_gt_0[of z] norm_cvec_gt_0[of w] by (subst dist_fs_cvec_iff) auto lemma dist_fs_zero1 [simp]: shows "dist_fs z z = 0" by (transfer, transfer) (subst dist_fs_cvec_zero, simp, (subst norm_cvec_square)+, subst cmod_square, simp del: inprod_cvec_def) lemma dist_fs_zero2 [simp]: assumes "dist_fs z1 z2 = 0" shows "z1 = z2" using assms proof (transfer, transfer) fix z w :: complex_vec obtain z1 z2 w1 w2 where *: "z = (z1, z2)" "w = (w1, w2)" by (cases "z", cases "w", auto) let ?x = "(z1*w2 - w1*z2) * (cnj z1*cnj w2 - cnj w1*cnj z2)" assume "z \ vec_zero" "w \ vec_zero" "dist_fs_cvec z w = 0" hence "(cmod \z,w\)\<^sup>2 = \z\\<^sup>2 * \w\\<^sup>2" by (subst (asm) dist_fs_cvec_zero, simp_all) hence "Re ?x = 0" using * by (subst (asm) cmod_square) ((subst (asm) norm_cvec_square)+, simp add: vec_cnj_def field_simps) hence "?x = 0" using complex_mult_cnj_cmod[of "z1*w2 - w1*z2"] zero_complex.simps by (subst complex_eq_if_Re_eq[of ?x 0]) (simp add: power2_eq_square, simp, linarith) moreover have "z1 * w2 - w1 * z2 = 0 \ cnj z1 * cnj w2 - cnj w1 * cnj z2 = 0" by (metis complex_cnj_diff complex_cnj_mult complex_cnj_zero_iff) ultimately show "z \\<^sub>v w" using * \z \ vec_zero\ \w \ vec_zero\ using complex_cvec_eq_mix[of z1 z2 w1 w2] by auto qed lemma dist_fs_sym: shows "dist_fs z1 z2 = dist_fs z2 z1" by (transfer, transfer) (simp add: split_def field_simps) (* -------------------------------------------------------------------------- *) subsubsection \Triangle inequality for Fubini-Study metric\ (* -------------------------------------------------------------------------- *) lemma dist_fs_triangle_finite: shows "cmod(a - b) / (sqrt (1+(cmod a)\<^sup>2) * sqrt (1+(cmod b)\<^sup>2)) \ cmod (a - c) / (sqrt (1+(cmod a)\<^sup>2) * sqrt (1+(cmod c)\<^sup>2)) + cmod (c - b) / (sqrt (1+(cmod b)\<^sup>2) * sqrt (1+(cmod c)\<^sup>2))" proof- let ?cc = "1+(cmod c)\<^sup>2" and ?bb = "1+(cmod b)\<^sup>2" and ?aa = "1+(cmod a)\<^sup>2" have "sqrt ?cc > 0" "sqrt ?aa > 0" "sqrt ?bb > 0" by (smt real_sqrt_gt_zero zero_compare_simps(12))+ have "(a - b)*(1+cnj c*c) = (a-c)*(1+cnj c*b) + (c-b)*(1 + cnj c*a)" by (simp add: field_simps) moreover have "1 + cnj c * c = 1 + (cmod c)\<^sup>2" using complex_norm_square by auto hence "cmod ((a - b)*(1+cnj c*c)) = cmod(a - b) * (1+(cmod c)\<^sup>2)" by (smt norm_mult norm_of_real zero_compare_simps(12)) ultimately have "cmod(a - b) * (1+(cmod c)\<^sup>2) \ cmod (a-c) * cmod (1+cnj c*b) + cmod (c-b) * cmod(1 + cnj c*a)" using complex_mod_triangle_ineq2[of "(a-c)*(1+cnj c*b)" "(c-b)*(1 + cnj c*a)"] by simp moreover have *: "\ a b c d b' d'. \b \ b'; d \ d'; a \ (0::real); c \ 0\ \ a*b + c*d \ a*b' + c*d'" by (smt mult_left_mono) have "cmod (a-c) * cmod (1+cnj c*b) + cmod (c-b) * cmod(1 + cnj c*a) \ cmod (a - c) * (sqrt (1+(cmod c)\<^sup>2) * sqrt (1+(cmod b)\<^sup>2)) + cmod (c - b) * (sqrt (1+(cmod c)\<^sup>2) * sqrt (1+(cmod a)\<^sup>2))" using *[OF cmod_1_plus_mult_le[of "cnj c" b] cmod_1_plus_mult_le[of "cnj c" a], of "cmod (a-c)" "cmod (c-b)"] by (simp add: field_simps real_sqrt_mult[symmetric]) ultimately have "cmod(a - b) * ?cc \ cmod (a - c) * sqrt ?cc * sqrt ?bb + cmod (c - b) * sqrt ?cc * sqrt ?aa" by simp moreover hence "0 \ ?cc * sqrt ?aa * sqrt ?bb" using mult_right_mono[of 0 "sqrt ?aa" "sqrt ?bb"] using mult_right_mono[of 0 "?cc" "sqrt ?aa * sqrt ?bb"] by simp moreover have "sqrt ?cc / ?cc = 1 / sqrt ?cc" using \sqrt ?cc > 0\ by (simp add: field_simps) hence "sqrt ?cc / (?cc * sqrt ?aa) = 1 / (sqrt ?aa * sqrt ?cc)" using times_divide_eq_right[of "1/sqrt ?aa" "sqrt ?cc" "?cc"] using \sqrt ?aa > 0\ by simp hence "cmod (a - c) * sqrt ?cc / (?cc * sqrt ?aa) = cmod (a - c) / (sqrt ?aa * sqrt ?cc)" using times_divide_eq_right[of "cmod (a - c)" "sqrt ?cc" "(?cc * sqrt ?aa)"] by simp moreover have "sqrt ?cc / ?cc = 1 / sqrt ?cc" using \sqrt ?cc > 0\ by (simp add: field_simps) hence "sqrt ?cc / (?cc * sqrt ?bb) = 1 / (sqrt ?bb * sqrt ?cc)" using times_divide_eq_right[of "1/sqrt ?bb" "sqrt ?cc" "?cc"] using \sqrt ?bb > 0\ by simp hence "cmod (c - b) * sqrt ?cc / (?cc * sqrt ?bb) = cmod (c - b) / (sqrt ?bb * sqrt ?cc)" using times_divide_eq_right[of "cmod (c - b)" "sqrt ?cc" "?cc * sqrt ?bb"] by simp ultimately show ?thesis using divide_right_mono[of "cmod (a - b) * ?cc" "cmod (a - c) * sqrt ?cc * sqrt ?bb + cmod (c - b) * sqrt ?cc * sqrt ?aa" "?cc * sqrt ?aa * sqrt ?bb"] \sqrt ?aa > 0\ \sqrt ?bb > 0\ \sqrt ?cc > 0\ by (simp add: add_divide_distrib) qed lemma dist_fs_triangle_infinite1: shows "1 / sqrt(1 + (cmod b)\<^sup>2) \ 1 / sqrt(1 + (cmod c)\<^sup>2) + cmod (b - c) / (sqrt(1 + (cmod b)\<^sup>2) * sqrt(1 + (cmod c)\<^sup>2))" proof- let ?bb = "sqrt (1 + (cmod b)\<^sup>2)" and ?cc = "sqrt (1 + (cmod c)\<^sup>2)" have "?bb > 0" "?cc > 0" by (metis add_strict_increasing real_sqrt_gt_0_iff zero_le_power2 zero_less_one)+ hence *: "?bb * ?cc \ 0" by simp have **: "(?cc - ?bb) / (?bb * ?cc) = 1 / ?bb - 1 / ?cc" using \sqrt (1 + (cmod b)\<^sup>2) > 0\ \sqrt (1 + (cmod c)\<^sup>2) > 0\ by (simp add: field_simps) show "1 / ?bb \ 1 / ?cc + cmod (b - c) / (?bb * ?cc)" using divide_right_mono[OF cmod_diff_ge[of c b] *] by (subst (asm) **) (simp add: field_simps norm_minus_commute) qed lemma dist_fs_triangle_infinite2: shows "1 / sqrt(1 + (cmod a)\<^sup>2) \ cmod (a - c) / (sqrt (1+(cmod a)\<^sup>2) * sqrt (1+(cmod c)\<^sup>2)) + 1 / sqrt(1 + (cmod c)\<^sup>2)" using dist_fs_triangle_infinite1[of a c] by simp lemma dist_fs_triangle_infinite3: shows "cmod(a - b) / (sqrt (1+(cmod a)\<^sup>2) * sqrt (1+(cmod b)\<^sup>2)) \ 1 / sqrt(1 + (cmod a)\<^sup>2) + 1 / sqrt(1 + (cmod b)\<^sup>2)" proof- let ?aa = "sqrt (1 + (cmod a)\<^sup>2)" and ?bb = "sqrt (1 + (cmod b)\<^sup>2)" have "?aa > 0" "?bb > 0" by (metis add_strict_increasing real_sqrt_gt_0_iff zero_le_power2 zero_less_one)+ hence *: "?aa * ?bb \ 0" by simp have **: "(?aa + ?bb) / (?aa * ?bb) = 1 / ?aa + 1 / ?bb" using \?aa > 0\ \?bb > 0\ by (simp add: field_simps) show "cmod (a - b) / (?aa * ?bb) \ 1 / ?aa + 1 / ?bb" using divide_right_mono[OF cmod_diff_le[of a b] *] by (subst (asm) **) (simp add: field_simps norm_minus_commute) qed lemma dist_fs_triangle: shows "dist_fs A B \ dist_fs A C + dist_fs C B" proof (cases "A = \\<^sub>h") case True show ?thesis proof (cases "B = \\<^sub>h") case True show ?thesis proof (cases "C = \\<^sub>h") case True show ?thesis using \A = \\<^sub>h\ \B = \\<^sub>h\ \C = \\<^sub>h\ by simp next case False then obtain c where "C = of_complex c" using inf_or_of_complex[of C] by auto show ?thesis using \A = \\<^sub>h\ \B = \\<^sub>h\ \C = of_complex c\ by (simp add: dist_fs_infinite2 dist_fs_sym) qed next case False then obtain b where "B = of_complex b" using inf_or_of_complex[of B] by auto show ?thesis proof (cases "C = \\<^sub>h") case True show ?thesis using \A = \\<^sub>h\ \C = \\<^sub>h\ \B = of_complex b\ by simp next case False then obtain c where "C = of_complex c" using inf_or_of_complex[of C] by auto show ?thesis using \A = \\<^sub>h\ \B = of_complex b\ \C = of_complex c\ using mult_left_mono[OF dist_fs_triangle_infinite1[of b c], of 2] by (simp add: dist_fs_finite dist_fs_infinite1 dist_fs_infinite2 dist_fs_sym) qed qed next case False then obtain a where "A = of_complex a" using inf_or_of_complex[of A] by auto show ?thesis proof (cases "B = \\<^sub>h") case True show ?thesis proof (cases "C = \\<^sub>h") case True show ?thesis using \B = \\<^sub>h\ \C = \\<^sub>h\ \A = of_complex a\ by (simp add: dist_fs_infinite2) next case False then obtain c where "C = of_complex c" using inf_or_of_complex[of C] by auto show ?thesis using \B = \\<^sub>h\ \C = of_complex c\ \A = of_complex a\ using mult_left_mono[OF dist_fs_triangle_infinite2[of a c], of 2] by (simp add: dist_fs_finite dist_fs_infinite1 dist_fs_infinite2) qed next case False then obtain b where "B = of_complex b" using inf_or_of_complex[of B] by auto show ?thesis proof (cases "C = \\<^sub>h") case True thus ?thesis using \C = \\<^sub>h\ \B = of_complex b\ \A = of_complex a\ using mult_left_mono[OF dist_fs_triangle_infinite3[of a b], of 2] by (simp add: dist_fs_finite dist_fs_infinite1 dist_fs_infinite2) next case False then obtain c where "C = of_complex c" using inf_or_of_complex[of C] by auto show ?thesis using \A = of_complex a\ \B = of_complex b\ \C = of_complex c\ using mult_left_mono[OF dist_fs_triangle_finite[of a b c], of 2] by (simp add: dist_fs_finite norm_minus_commute dist_fs_sym) qed qed qed (* -------------------------------------------------------------------------- *) subsubsection \$\mathbb{C}P^1$ with Fubini-Study metric is a metric space\ (* -------------------------------------------------------------------------- *) text \Using the (already available) fact that $\mathbb{R}^3$ is a metric space (under the distance function $\lambda\ x\ y.\ @{term norm}(x - y)$), it was not difficult to show that the type @{term complex_homo} equipped with @{term dist_fs} is a metric space, i.e., an instantiation of the @{term metric_space} locale.\ instantiation complex_homo :: metric_space begin definition "dist_complex_homo = dist_fs" -definition "(uniformity_complex_homo :: (complex_homo \ complex_homo) filter) = (INF e:{0<..}. principal {(x, y). dist_class.dist x y < e})" +definition "(uniformity_complex_homo :: (complex_homo \ complex_homo) filter) = (INF e\{0<..}. principal {(x, y). dist_class.dist x y < e})" definition "open_complex_homo (U :: complex_homo set) = (\ x \ U. eventually (\(x', y). x' = x \ y \ U) uniformity)" instance proof fix x y :: complex_homo show "(dist_class.dist x y = 0) = (x = y)" unfolding dist_complex_homo_def using dist_fs_zero1[of x] dist_fs_zero2[of x y] by auto next fix x y z :: complex_homo show "dist_class.dist x y \ dist_class.dist x z + dist_class.dist y z" unfolding dist_complex_homo_def using dist_fs_triangle[of x y z] by (simp add: dist_fs_sym) qed (simp_all add: open_complex_homo_def uniformity_complex_homo_def) end (* -------------------------------------------------------------------------- *) subsubsection \Chordal distance on the Riemann sphere\ (* -------------------------------------------------------------------------- *) text \Distance of the two points is given by the length of the chord. We show that it corresponds to the Fubini-Study metric in the plane.\ definition dist_riemann_sphere_r3 :: "R3 \ R3 \ real" where [simp]: "dist_riemann_sphere_r3 M1 M2 = (let (x1, y1, z1) = M1; (x2, y2, z2) = M2 in norm (x1 - x2, y1 - y2, z1 - z2))" lemma dist_riemann_sphere_r3_inner: assumes "M1 \ unit_sphere" and "M2 \ unit_sphere" shows "(dist_riemann_sphere_r3 M1 M2)\<^sup>2 = 2 - 2 * inner M1 M2" using assms apply (cases M1, cases M2) apply (auto simp add: norm_prod_def) apply (simp add: power2_eq_square field_simps) done lift_definition dist_riemann_sphere' :: "riemann_sphere \ riemann_sphere \ real" is dist_riemann_sphere_r3 done lemma dist_riemann_sphere_ge_0 [simp]: shows "dist_riemann_sphere' M1 M2 \ 0" apply transfer using norm_ge_zero by (simp add: split_def Let_def) text \Using stereographic projection we prove the connection between chordal metric on the spehere and Fubini-Study metric in the plane.\ lemma dist_stereographic_finite: assumes "stereographic M1 = of_complex m1" and "stereographic M2 = of_complex m2" shows "dist_riemann_sphere' M1 M2 = 2 * cmod (m1 - m2) / (sqrt (1 + (cmod m1)\<^sup>2) * sqrt (1 + (cmod m2)\<^sup>2))" using assms proof- have *: "M1 = inv_stereographic (of_complex m1)" "M2 = inv_stereographic (of_complex m2)" using inv_stereographic_is_inv assms by (metis inv_stereographic_stereographic)+ have "(1 + (cmod m1)\<^sup>2) \ 0" "(1 + (cmod m2)\<^sup>2) \ 0" by (smt power2_less_0)+ have "(1 + (cmod m1)\<^sup>2) > 0" "(1 + (cmod m2)\<^sup>2) > 0" by (smt realpow_square_minus_le)+ hence "(1 + (cmod m1)\<^sup>2) * (1 + (cmod m2)\<^sup>2) > 0" by (metis norm_mult_less norm_zero power2_eq_square zero_power2) hence ++: "sqrt ((1 + cmod m1 * cmod m1) * (1 + cmod m2 * cmod m2)) > 0" using real_sqrt_gt_0_iff by (simp add: power2_eq_square) hence **: "(2 * cmod (m1 - m2) / sqrt ((1 + cmod m1 * cmod m1) * (1 + cmod m2 * cmod m2))) \ 0 \ cmod (m1 - m2) \ 0" by (metis diff_self divide_nonneg_pos mult_2 norm_ge_zero norm_triangle_ineq4 norm_zero) have "(dist_riemann_sphere' M1 M2)\<^sup>2 * (1 + (cmod m1)\<^sup>2) * (1 + (cmod m2)\<^sup>2) = 4 * (cmod (m1 - m2))\<^sup>2" using * proof (transfer, transfer) fix m1 m2 M1 M2 assume us: "M1 \ unit_sphere" "M2 \ unit_sphere" and *: "M1 = inv_stereographic_cvec_r3 (of_complex_cvec m1)" "M2 = inv_stereographic_cvec_r3 (of_complex_cvec m2)" have "(1 + (cmod m1)\<^sup>2) \ 0" "(1 + (cmod m2)\<^sup>2) \ 0" by (smt power2_less_0)+ thus "(dist_riemann_sphere_r3 M1 M2)\<^sup>2 * (1 + (cmod m1)\<^sup>2) * (1 + (cmod m2)\<^sup>2) = 4 * (cmod (m1 - m2))\<^sup>2" apply (subst dist_riemann_sphere_r3_inner[OF us]) apply (subst *)+ apply (simp add: dist_riemann_sphere_r3_inner[OF us] complex_mult_cnj_cmod) apply (subst left_diff_distrib[of 2]) apply (subst left_diff_distrib[of "2*(1+(cmod m1)\<^sup>2)"]) apply (subst distrib_right[of _ _ "(1 + (cmod m1)\<^sup>2)"]) apply (subst distrib_right[of _ _ "(1 + (cmod m1)\<^sup>2)"]) apply simp apply (subst distrib_right[of _ _ "(1 + (cmod m2)\<^sup>2)"]) apply (subst distrib_right[of _ _ "(1 + (cmod m2)\<^sup>2)"]) apply (subst distrib_right[of _ _ "(1 + (cmod m2)\<^sup>2)"]) apply simp apply (subst (asm) cmod_square)+ apply (subst cmod_square)+ apply (simp add: field_simps) done qed hence "(dist_riemann_sphere' M1 M2)\<^sup>2 = 4 * (cmod (m1 - m2))\<^sup>2 / ((1 + (cmod m1)\<^sup>2) * (1 + (cmod m2)\<^sup>2))" using \(1 + (cmod m1)\<^sup>2) \ 0\ \(1 + (cmod m2)\<^sup>2) \ 0\ using eq_divide_imp[of "(1 + (cmod m1)\<^sup>2) * (1 + (cmod m2)\<^sup>2)" "(dist_riemann_sphere' M1 M2)\<^sup>2" "4 * (cmod (m1 - m2))\<^sup>2"] by simp thus "dist_riemann_sphere' M1 M2 = 2 * cmod (m1 - m2) / (sqrt (1 + (cmod m1)\<^sup>2) * sqrt (1 + (cmod m2)\<^sup>2))" using power2_eq_iff[of "dist_riemann_sphere' M1 M2" "2 * (cmod (m1 - m2)) / sqrt ((1 + (cmod m1)\<^sup>2) * (1 + (cmod m2)\<^sup>2))"] using \(1 + (cmod m1)\<^sup>2) * (1 + (cmod m2)\<^sup>2) > 0\ \(1 + (cmod m1)\<^sup>2) > 0\ \(1 + (cmod m2)\<^sup>2) > 0\ apply (auto simp add: power2_eq_square real_sqrt_mult[symmetric]) using dist_riemann_sphere_ge_0[of M1 M2] ** using ++ divide_le_0_iff by force qed lemma dist_stereographic_infinite: assumes "stereographic M1 = \\<^sub>h" and "stereographic M2 = of_complex m2" shows "dist_riemann_sphere' M1 M2 = 2 / sqrt (1 + (cmod m2)\<^sup>2)" proof- have *: "M1 = inv_stereographic \\<^sub>h" "M2 = inv_stereographic (of_complex m2)" using inv_stereographic_is_inv assms by (metis inv_stereographic_stereographic)+ have "(1 + (cmod m2)\<^sup>2) \ 0" by (smt power2_less_0) have "(1 + (cmod m2)\<^sup>2) > 0" by (smt realpow_square_minus_le)+ hence "sqrt (1 + cmod m2 * cmod m2) > 0" using real_sqrt_gt_0_iff by (simp add: power2_eq_square) hence **: "2 / sqrt (1 + cmod m2 * cmod m2) > 0" by simp have "(dist_riemann_sphere' M1 M2)\<^sup>2 * (1 + (cmod m2)\<^sup>2) = 4" using * apply transfer apply transfer proof- fix M1 M2 m2 assume us: "M1 \ unit_sphere" "M2 \ unit_sphere" and *: "M1 = inv_stereographic_cvec_r3 \\<^sub>v" "M2 = inv_stereographic_cvec_r3 (of_complex_cvec m2)" have "(1 + (cmod m2)\<^sup>2) \ 0" by (smt power2_less_0) thus "(dist_riemann_sphere_r3 M1 M2)\<^sup>2 * (1 + (cmod m2)\<^sup>2) = 4" apply (subst dist_riemann_sphere_r3_inner[OF us]) apply (subst *)+ apply (simp add: complex_mult_cnj_cmod) apply (subst left_diff_distrib[of 2], simp) done qed hence "(dist_riemann_sphere' M1 M2)\<^sup>2 = 4 / (1 + (cmod m2)\<^sup>2)" using \(1 + (cmod m2)\<^sup>2) \ 0\ by (simp add: field_simps) thus "dist_riemann_sphere' M1 M2 = 2 / sqrt (1 + (cmod m2)\<^sup>2)" using power2_eq_iff[of "dist_riemann_sphere' M1 M2" "2 / sqrt (1 + (cmod m2)\<^sup>2)"] using \(1 + (cmod m2)\<^sup>2) > 0\ apply (auto simp add: power2_eq_square real_sqrt_mult[symmetric]) using dist_riemann_sphere_ge_0[of M1 M2] ** by simp qed lemma dist_rieman_sphere_zero [simp]: shows "dist_riemann_sphere' M M = 0" by transfer auto lemma dist_riemann_sphere_sym: shows "dist_riemann_sphere' M1 M2 = dist_riemann_sphere' M2 M1" proof transfer fix M1 M2 :: R3 obtain x1 y1 z1 x2 y2 z2 where MM: "(x1, y1, z1) = M1" "(x2, y2, z2) = M2" by (cases "M1", cases "M2", auto) show "dist_riemann_sphere_r3 M1 M2 = dist_riemann_sphere_r3 M2 M1" using norm_minus_cancel[of "(x1 - x2, y1 - y2, z1 - z2)"] MM[symmetric] by simp qed text \Central theorem that connects the two metrics.\ lemma dist_stereographic: shows "dist_riemann_sphere' M1 M2 = dist_fs (stereographic M1) (stereographic M2)" proof (cases "M1 = North") case True hence "stereographic M1 = \\<^sub>h" by (simp add: stereographic_North) show ?thesis proof (cases "M2 = North") case True show ?thesis using \M1 = North\ \M2 = North\ by auto next case False hence "stereographic M2 \ \\<^sub>h" using stereographic_North[of M2] by simp then obtain m2 where "stereographic M2 = of_complex m2" using inf_or_of_complex[of "stereographic M2"] by auto show ?thesis using \stereographic M2 = of_complex m2\ \stereographic M1 = \\<^sub>h\ using dist_fs_infinite1 dist_stereographic_infinite by (simp add: dist_fs_sym) qed next case False hence "stereographic M1 \ \\<^sub>h" by (simp add: stereographic_North) then obtain m1 where "stereographic M1 = of_complex m1" using inf_or_of_complex[of "stereographic M1"] by auto show ?thesis proof (cases "M2 = North") case True hence "stereographic M2 = \\<^sub>h" by (simp add: stereographic_North) show ?thesis using \stereographic M1 = of_complex m1\ \stereographic M2 = \\<^sub>h\ using dist_fs_infinite2 dist_stereographic_infinite by (subst dist_riemann_sphere_sym, simp add: dist_fs_sym) next case False hence "stereographic M2 \ \\<^sub>h" by (simp add: stereographic_North) then obtain m2 where "stereographic M2 = of_complex m2" using inf_or_of_complex[of "stereographic M2"] by auto show ?thesis using \stereographic M1 = of_complex m1\ \stereographic M2 = of_complex m2\ using dist_fs_finite dist_stereographic_finite by simp qed qed text \Other direction\ lemma dist_stereographic': shows "dist_fs A B = dist_riemann_sphere' (inv_stereographic A) (inv_stereographic B)" by (subst dist_stereographic) (metis stereographic_inv_stereographic) text \The @{term riemann_sphere} equipped with @{term dist_riemann_sphere'} is a metric space, i.e., an instantiation of the @{term metric_space} locale.\ instantiation riemann_sphere :: metric_space begin definition "dist_riemann_sphere = dist_riemann_sphere'" -definition "(uniformity_riemann_sphere :: (riemann_sphere \ riemann_sphere) filter) = (INF e:{0<..}. principal {(x, y). dist_class.dist x y < e})" +definition "(uniformity_riemann_sphere :: (riemann_sphere \ riemann_sphere) filter) = (INF e\{0<..}. principal {(x, y). dist_class.dist x y < e})" definition "open_riemann_sphere (U :: riemann_sphere set) = (\ x \ U. eventually (\(x', y). x' = x \ y \ U) uniformity)" instance proof fix x y :: riemann_sphere show "(dist_class.dist x y = 0) = (x = y)" unfolding dist_riemann_sphere_def proof transfer fix x y :: R3 obtain x1 y1 z1 x2 y2 z2 where *: "(x1, y1, z1) = x" "(x2, y2, z2) = y" by (cases x, cases y, auto) assume "x \ unit_sphere" "y \ unit_sphere" thus "(dist_riemann_sphere_r3 x y = 0) = (x = y)" using norm_eq_zero[of "(x1 - y2, y1 - y2, z1 - z2)"] using *[symmetric] by (simp add: zero_prod_def) qed next fix x y z :: riemann_sphere show "dist_class.dist x y \ dist_class.dist x z + dist_class.dist y z" unfolding dist_riemann_sphere_def proof transfer fix x y z :: R3 obtain x1 y1 z1 x2 y2 z2 x3 y3 z3 where MM: "(x1, y1, z1) = x" "(x2, y2, z2) = y" "(x3, y3, z3) = z" by (cases "x", cases "y", cases "z", auto) assume "x \ unit_sphere" "y \ unit_sphere" "z \ unit_sphere" thus "dist_riemann_sphere_r3 x y \ dist_riemann_sphere_r3 x z + dist_riemann_sphere_r3 y z" using MM[symmetric] norm_minus_cancel[of "(x3 - x2, y3 - y2, z3 - z2)"] norm_triangle_ineq[of "(x1 - x3, y1 - y3, z1 - z3)" "(x3 - x2, y3 - y2, z3 - z2)"] by simp qed qed (simp_all add: uniformity_riemann_sphere_def open_riemann_sphere_def) end text \The @{term riemann_sphere} metric space is perfect, i.e., it does not have isolated points.\ instantiation riemann_sphere :: perfect_space begin instance proof fix M :: riemann_sphere show "\ open {M}" unfolding open_dist dist_riemann_sphere_def apply (subst dist_riemann_sphere_sym) proof transfer fix M assume "M \ unit_sphere" obtain x y z where MM: "M = (x, y, z)" by (cases "M") auto then obtain \ \ where *: "x = cos \ * cos \" "y = cos \ * sin \" "z = sin \" "-pi / 2 \ \ \ \ \ pi / 2" using \M \ unit_sphere\ using ex_sphere_params[of x y z] by auto have "\ e. e > 0 \ (\y. y \ unit_sphere \ dist_riemann_sphere_r3 M y < e \ y \ M)" proof- fix e :: real assume "e > 0" then obtain \' where "1 - (e*e/2) < cos (\ - \')" "\ \ \'" "-pi/2 \ \'" "\' \ pi/2" using ex_cos_gt[of \ "1 - (e*e/2)"] \- pi / 2 \ \ \ \ \ pi / 2\ by auto hence "sin \ \ sin \'" using \-pi / 2 \ \ \ \ \ pi / 2\ sin_inj[of \ \'] by auto have "2 - 2 * cos (\ - \') < e*e" using mult_strict_right_mono[OF \1 - (e*e/2) < cos (\ - \')\, of 2] by (simp add: field_simps) have "2 - 2 * cos (\ - \') \ 0" using cos_le_one[of "\ - \'"] - by (simp add: sign_simps) + by (simp add: algebra_split_simps) let ?M' = "(cos \' * cos \, cos \' * sin \, sin \')" have "dist_riemann_sphere_r3 M ?M' = sqrt ((cos \ - cos \')\<^sup>2 + (sin \ - sin \')\<^sup>2)" using MM * sphere_params_on_sphere[of _ \' \] using sin_cos_squared_add[of \] apply (simp add: dist_riemann_sphere'_def Abs_riemann_sphere_inverse norm_prod_def) apply (subst left_diff_distrib[symmetric])+ apply (subst power_mult_distrib)+ apply (subst distrib_left[symmetric]) apply simp done also have "... = sqrt (2 - 2*cos (\ - \'))" by (simp add: power2_eq_square field_simps cos_diff) finally have "(dist_riemann_sphere_r3 M ?M')\<^sup>2 = 2 - 2*cos (\ - \')" using \2 - 2 * cos (\ - \') \ 0\ by simp hence "(dist_riemann_sphere_r3 M ?M')\<^sup>2 < e\<^sup>2" using \2 - 2 * cos (\ - \') < e*e\ by (simp add: power2_eq_square) hence "dist_riemann_sphere_r3 M ?M' < e" apply (rule power2_less_imp_less) using \e > 0\ by simp moreover have "M \ ?M'" using MM \sin \ \ sin \'\ * by simp moreover have "?M' \ unit_sphere" using sphere_params_on_sphere by auto ultimately show "\y. y \ unit_sphere \ dist_riemann_sphere_r3 M y < e \ y \ M" unfolding dist_riemann_sphere_def by (rule_tac x="?M'" in exI, simp) qed thus "\ (\x\{M}. \e>0. \y\{x. x \ unit_sphere}. dist_riemann_sphere_r3 x y < e \ y \ {M})" by auto qed qed end text \The @{term complex_homo} metric space is perfect, i.e., it does not have isolated points.\ instantiation complex_homo :: perfect_space begin instance proof fix x::complex_homo show "\ open {x}" unfolding open_dist proof (auto) fix e::real assume "e > 0" thus "\ y. dist_class.dist y x < e \ y \ x" using not_open_singleton[of "inv_stereographic x"] unfolding open_dist unfolding dist_complex_homo_def dist_riemann_sphere_def apply (subst dist_stereographic', auto) apply (erule_tac x=e in allE, auto) apply (rule_tac x="stereographic y" in exI, auto) done qed qed end lemma Lim_within: shows "(f \ l) (at a within S) \ (\e >0. \d>0. \x \ S. 0 < dist_class.dist x a \ dist_class.dist x a < d \ dist_class.dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at) lemma continuous_on_iff: shows "continuous_on s f \ (\x\s. \e>0. \d>0. \x'\s. dist_class.dist x' x < d \ dist_class.dist (f x') (f x) < e)" unfolding continuous_on_def Lim_within by (metis dist_pos_lt dist_self) text \Using the chordal metric in the extended plane, and the Euclidean metric on the sphere in $\mathbb{R}^3$, the stereographic and inverse stereographic projections are proved to be continuous.\ lemma "continuous_on UNIV stereographic" unfolding continuous_on_iff unfolding dist_complex_homo_def dist_riemann_sphere_def by (subst dist_stereographic', auto) lemma "continuous_on UNIV inv_stereographic" unfolding continuous_on_iff unfolding dist_complex_homo_def dist_riemann_sphere_def by (subst dist_stereographic, auto) (* -------------------------------------------------------------------------- *) subsubsection \Chordal circles\ (* -------------------------------------------------------------------------- *) text \Real circlines are sets of points that are equidistant from some given point in the chordal metric. There are exactly two such points (two chordal centers). On the Riemann sphere, these two points are obtained as intersections of the sphere and a line that goes trough center of the circle, and its orthogonal to its plane.\ text \The circline for the given chordal center and radius.\ definition chordal_circle_cvec_cmat :: "complex_vec \ real \ complex_mat" where [simp]: "chordal_circle_cvec_cmat a r = (let (a1, a2) = a in ((4*a2*cnj a2 - (cor r)\<^sup>2*(a1*cnj a1 + a2*cnj a2)), (-4*a1*cnj a2), (-4*cnj a1*a2), (4*a1*cnj a1 - (cor r)\<^sup>2*(a1*cnj a1 + a2*cnj a2))))" lemma chordal_circle_cmat_hermitean_nonzero [simp]: assumes "a \ vec_zero" shows "chordal_circle_cvec_cmat a r \ hermitean_nonzero" using assms by (cases a) (auto simp add: hermitean_def mat_adj_def mat_cnj_def Let_def) lift_definition chordal_circle_hcoords_clmat :: "complex_homo_coords \ real \ circline_mat" is chordal_circle_cvec_cmat using chordal_circle_cmat_hermitean_nonzero by (simp del: chordal_circle_cvec_cmat_def) lift_definition chordal_circle :: "complex_homo \ real \ circline" is chordal_circle_hcoords_clmat proof transfer fix a b :: complex_vec and r :: real assume *: "a \ vec_zero" "b \ vec_zero" obtain a1 a2 where aa: "a = (a1, a2)" by (cases a, auto) obtain b1 b2 where bb: "b = (b1, b2)" by (cases b, auto) assume "a \\<^sub>v b" then obtain k where "b = (k * a1, k * a2)" "k \ 0" using aa bb by auto moreover have "cor (Re (k * cnj k)) = k * cnj k" by (metis complex_In_mult_cnj_zero complex_of_real_Re) ultimately show "circline_eq_cmat (chordal_circle_cvec_cmat a r) (chordal_circle_cvec_cmat b r)" using * aa bb by simp (rule_tac x="Re (k*cnj k)" in exI, auto simp add: Let_def field_simps) qed lemma sqrt_1_plus_square: shows "sqrt (1 + a\<^sup>2) \ 0" by (smt real_sqrt_less_mono real_sqrt_zero realpow_square_minus_le) lemma assumes "dist_fs z a = r" shows "z \ circline_set (chordal_circle a r)" proof (cases "a \ \\<^sub>h") case True then obtain a' where "a = of_complex a'" using inf_or_of_complex by auto let ?A = "4 - (cor r)\<^sup>2 * (1 + (a'*cnj a'))" and ?B = "-4*a'" and ?C="-4*cnj a'" and ?D = "4*a'*cnj a' - (cor r)\<^sup>2 * (1 + (a'*cnj a'))" have hh: "(?A, ?B, ?C, ?D) \ {H. hermitean H \ H \ mat_zero}" by (auto simp add: hermitean_def mat_adj_def mat_cnj_def power2_eq_square) hence *: "chordal_circle (of_complex a') r = mk_circline ?A ?B ?C ?D" by (transfer, transfer, simp, rule_tac x=1 in exI, simp) show ?thesis proof (cases "z \ \\<^sub>h") case True then obtain z' where "z = of_complex z'" using inf_or_of_complex[of z] inf_or_of_complex[of a] by auto have "2 * cmod (z' - a') / (sqrt (1 + (cmod z')\<^sup>2) * sqrt (1 + (cmod a')\<^sup>2)) = r" using dist_fs_finite[of z' a'] assms \z = of_complex z'\ \a = of_complex a'\ by auto hence "4 * (cmod (z' - a'))\<^sup>2 / ((1 + (cmod z')\<^sup>2) * (1 + (cmod a')\<^sup>2)) = r\<^sup>2 " by (auto simp add: field_simps) moreover have "sqrt (1 + (cmod z')\<^sup>2) \ 0" "sqrt (1 + (cmod a')\<^sup>2) \ 0" using sqrt_1_plus_square by simp+ hence "(1 + (cmod z')\<^sup>2) * (1 + (cmod a')\<^sup>2) \ 0" by simp ultimately have "4 * (cmod (z' - a'))\<^sup>2 = r\<^sup>2 * ((1 + (cmod z')\<^sup>2) * (1 + (cmod a')\<^sup>2))" by (simp add: field_simps) hence "4 * Re ((z' - a')*cnj (z' - a')) = r\<^sup>2 * (1 + Re (z'*cnj z')) * (1 + Re (a'*cnj a'))" by ((subst cmod_square[symmetric])+, simp) hence "4 * (Re(z'*cnj z') - Re(a'*cnj z') - Re(cnj a'*z') + Re(a'*cnj a')) = r\<^sup>2 * (1 + Re (z'*cnj z')) * (1 + Re (a'*cnj a'))" by (simp add: field_simps) hence "Re (?A * z' * cnj z' + ?B * cnj z' + ?C * z' + ?D) = 0" by (simp add: power2_eq_square field_simps) hence "?A * z' * cnj z' + ?B * cnj z' + ?C * z' + ?D = 0" by (subst complex_eq_if_Re_eq) (auto simp add: power2_eq_square) hence "(cnj z' * ?A + ?C) * z' + (cnj z' * ?B + ?D) = 0" by algebra hence "z \ circline_set (mk_circline ?A ?B ?C ?D)" using \z = of_complex z'\ hh unfolding circline_set_def by simp (transfer, transfer, simp add: vec_cnj_def) thus ?thesis using * by (subst \a = of_complex a'\) simp next case False hence "2 / sqrt (1 + (cmod a')\<^sup>2) = r" using assms \a = of_complex a'\ using dist_fs_infinite2[of a'] by simp moreover have "sqrt (1 + (cmod a')\<^sup>2) \ 0" using sqrt_1_plus_square by simp ultimately have "2 = r * sqrt (1 + (cmod a')\<^sup>2)" by (simp add: field_simps) hence "4 = (r * sqrt (1 + (cmod a')\<^sup>2))\<^sup>2" by simp hence "4 = r\<^sup>2 * (1 + (cmod a')\<^sup>2)" by (simp add: power_mult_distrib) hence "Re (4 - (cor r)\<^sup>2 * (1 + (a' * cnj a'))) = 0" by (subst (asm) cmod_square) (simp add: field_simps power2_eq_square) hence "4 - (cor r)\<^sup>2 * (1 + (a'*cnj a')) = 0" by (subst complex_eq_if_Re_eq) (auto simp add: power2_eq_square) hence "circline_A0 (mk_circline ?A ?B ?C ?D)" using hh by (simp, transfer, transfer, simp) hence "z \ circline_set (mk_circline ?A ?B ?C ?D)" using inf_in_circline_set[of "mk_circline ?A ?B ?C ?D"] using \\ z \ \\<^sub>h\ by simp thus ?thesis using * by (subst \a = of_complex a'\) simp qed next case False let ?A = "-(cor r)\<^sup>2" and ?B = "0" and ?C = "0" and ?D = "4 -(cor r)\<^sup>2" have hh: "(?A, ?B, ?C, ?D) \ {H. hermitean H \ H \ mat_zero}" by (auto simp add: hermitean_def mat_adj_def mat_cnj_def power2_eq_square) hence *: "chordal_circle a r = mk_circline ?A ?B ?C ?D" using \\ a \ \\<^sub>h\ by simp (transfer, transfer, simp, rule_tac x=1 in exI, simp) show ?thesis proof (cases "z = \\<^sub>h") case True show ?thesis using assms \z = \\<^sub>h\ \\ a \ \\<^sub>h\ using * hh by (simp, subst inf_in_circline_set, transfer, transfer, simp) next case False then obtain z' where "z = of_complex z'" using inf_or_of_complex[of z] by auto have "2 / sqrt (1 + (cmod z')\<^sup>2) = r" using assms \z = of_complex z'\\\ a \ \\<^sub>h\ using dist_fs_infinite2[of z'] by (simp add: dist_fs_sym) moreover have "sqrt (1 + (cmod z')\<^sup>2) \ 0" using sqrt_1_plus_square by simp ultimately have "2 = r * sqrt (1 + (cmod z')\<^sup>2)" by (simp add: field_simps) hence "4 = (r * sqrt (1 + (cmod z')\<^sup>2))\<^sup>2" by simp hence "4 = r\<^sup>2 * (1 + (cmod z')\<^sup>2)" by (simp add: power_mult_distrib) hence "Re (4 - (cor r)\<^sup>2 * (1 + (z' * cnj z'))) = 0" by (subst (asm) cmod_square) (simp add: field_simps power2_eq_square) hence "- (cor r)\<^sup>2 * z'*cnj z' + 4 - (cor r)\<^sup>2 = 0" by (subst complex_eq_if_Re_eq) (auto simp add: power2_eq_square field_simps) hence "z \ circline_set (mk_circline ?A ?B ?C ?D)" using hh unfolding circline_set_def by (subst \z = of_complex z'\, simp) (transfer, transfer, auto simp add: vec_cnj_def field_simps) thus ?thesis using * by simp qed qed lemma assumes "z \ circline_set (chordal_circle a r)" and "r \ 0" shows "dist_fs z a = r" proof (cases "a = \\<^sub>h") case False then obtain a' where "a = of_complex a'" using inf_or_of_complex by auto let ?A = "4 - (cor r)\<^sup>2 * (1 + (a'*cnj a'))" and ?B = "-4*a'" and ?C="-4*cnj a'" and ?D = "4*a'*cnj a' - (cor r)\<^sup>2 * (1 + (a'*cnj a'))" have hh: "(?A, ?B, ?C, ?D) \ {H. hermitean H \ H \ mat_zero}" by (auto simp add: hermitean_def mat_adj_def mat_cnj_def power2_eq_square) hence *: "chordal_circle (of_complex a') r = mk_circline ?A ?B ?C ?D" by (transfer, transfer, simp, rule_tac x=1 in exI, simp) show ?thesis proof (cases "z = \\<^sub>h") case False then obtain z' where "z = of_complex z'" using inf_or_of_complex[of z] inf_or_of_complex[of a] by auto hence "z \ circline_set (mk_circline ?A ?B ?C ?D)" using assms \a = of_complex a'\ * by simp hence "(cnj z' * ?A + ?C) * z' + (cnj z' * ?B + ?D) = 0" using hh unfolding circline_set_def by (subst (asm) \z = of_complex z'\, simp) (transfer, transfer, simp add: vec_cnj_def) hence "?A * z' * cnj z' + ?B * cnj z' + ?C * z' + ?D = 0" by algebra hence "Re (?A * z' * cnj z' + ?B * cnj z' +?C * z' +?D) = 0" by (simp add: power2_eq_square field_simps) hence "4 * Re ((z' - a')*cnj (z' - a')) = r\<^sup>2 * (1 + Re (z'*cnj z')) * (1 + Re (a'*cnj a'))" by (simp add: field_simps power2_eq_square) hence "4 * (cmod (z' - a'))\<^sup>2 = r\<^sup>2 * ((1 + (cmod z')\<^sup>2) * (1 + (cmod a')\<^sup>2))" by (subst cmod_square)+ simp moreover have "sqrt (1 + (cmod z')\<^sup>2) \ 0" "sqrt (1 + (cmod a')\<^sup>2) \ 0" using sqrt_1_plus_square by simp+ hence "(1 + (cmod z')\<^sup>2) * (1 + (cmod a')\<^sup>2) \ 0" by simp ultimately have "4 * (cmod (z' - a'))\<^sup>2 / ((1 + (cmod z')\<^sup>2) * (1 + (cmod a')\<^sup>2)) = r\<^sup>2 " by (simp add: field_simps) hence "2 * cmod (z' - a') / (sqrt (1 + (cmod z')\<^sup>2) * sqrt (1 + (cmod a')\<^sup>2)) = r" using \r \ 0\ by (subst (asm) real_sqrt_eq_iff[symmetric]) (simp add: real_sqrt_mult real_sqrt_divide) thus ?thesis using \z = of_complex z'\ \a = of_complex a'\ using dist_fs_finite[of z' a'] by simp next case True have "z \ circline_set (mk_circline ?A ?B ?C ?D)" using assms \a = of_complex a'\ * by simp hence "circline_A0 (mk_circline ?A ?B ?C ?D)" using inf_in_circline_set[of "mk_circline ?A ?B ?C ?D"] using \z = \\<^sub>h\ by simp hence "4 - (cor r)\<^sup>2 * (1 + (a'*cnj a')) = 0" using hh by (transfer, transfer, simp) hence "Re (4 - (cor r)\<^sup>2 * (1 + (a' * cnj a'))) = 0" by simp hence "4 = r\<^sup>2 * (1 + (cmod a')\<^sup>2)" by (subst cmod_square) (simp add: power2_eq_square) hence "2 = r * sqrt (1 + (cmod a')\<^sup>2)" using \r \ 0\ by (subst (asm) real_sqrt_eq_iff[symmetric]) (simp add: real_sqrt_mult) moreover have "sqrt (1 + (cmod a')\<^sup>2) \ 0" using sqrt_1_plus_square by simp ultimately have "2 / sqrt (1 + (cmod a')\<^sup>2) = r" by (simp add: field_simps) thus ?thesis using \a = of_complex a'\ \z = \\<^sub>h\ using dist_fs_infinite2[of a'] by simp qed next case True let ?A = "-(cor r)\<^sup>2" and ?B = "0" and ?C = "0" and ?D = "4 -(cor r)\<^sup>2" have hh: "(?A, ?B, ?C, ?D) \ {H. hermitean H \ H \ mat_zero}" by (auto simp add: hermitean_def mat_adj_def mat_cnj_def power2_eq_square) hence *: "chordal_circle a r = mk_circline ?A ?B ?C ?D" using \a = \\<^sub>h\ by simp (transfer, transfer, simp, rule_tac x=1 in exI, simp) show ?thesis proof (cases "z = \\<^sub>h") case True thus ?thesis using \a = \\<^sub>h\ assms * hh by simp (subst (asm) inf_in_circline_set, transfer, transfer, simp) next case False then obtain z' where "z = of_complex z'" using inf_or_of_complex by auto hence "z \ circline_set (mk_circline ?A ?B ?C ?D)" using assms * by simp hence "- (cor r)\<^sup>2 * z'*cnj z' + 4 - (cor r)\<^sup>2 = 0" using hh unfolding circline_set_def apply (subst (asm) \z = of_complex z'\) by (simp, transfer, transfer, simp add: vec_cnj_def, algebra) hence "4 - (cor r)\<^sup>2 * (1 + (z'*cnj z')) = 0" by (simp add: field_simps) hence "Re (4 - (cor r)\<^sup>2 * (1 + (z' * cnj z'))) = 0" by simp hence "4 = r\<^sup>2 * (1 + (cmod z')\<^sup>2)" by (subst cmod_square) (simp add: power2_eq_square) hence "2 = r * sqrt (1 + (cmod z')\<^sup>2)" using \r \ 0\ by (subst (asm) real_sqrt_eq_iff[symmetric]) (simp add: real_sqrt_mult) moreover have "sqrt (1 + (cmod z')\<^sup>2) \ 0" using sqrt_1_plus_square by simp ultimately have "2 / sqrt (1 + (cmod z')\<^sup>2) = r" by (simp add: field_simps) thus ?thesis using \z = of_complex z'\ \a = \\<^sub>h\ using dist_fs_infinite2[of z'] by (simp add: dist_fs_sym) qed qed text \Two chordal centers and radii for the given circline\ definition chordal_circles_cmat :: "complex_mat \ (complex \ real) \ (complex \ real)" where [simp]: "chordal_circles_cmat H = (let (A, B, C, D) = H; dsc = sqrt(Re ((D-A)\<^sup>2 + 4 * (B*cnj B))); a1 = (A - D + cor dsc) / (2 * C); r1 = sqrt((4 - Re((-4 * a1/B) * A)) / (1 + Re (a1*cnj a1))); a2 = (A - D - cor dsc) / (2 * C); r2 = sqrt((4 - Re((-4 * a2/B) * A)) / (1 + Re (a2*cnj a2))) in ((a1, r1), (a2, r2)))" lift_definition chordal_circles_clmat :: "circline_mat \ (complex \ real) \ (complex \ real)" is chordal_circles_cmat done lift_definition chordal_circles :: "ocircline \ (complex \ real) \ (complex \ real)" is chordal_circles_clmat proof transfer fix H1 H2 :: complex_mat obtain A1 B1 C1 D1 where hh1: "(A1, B1, C1, D1) = H1" by (cases H1) auto obtain A2 B2 C2 D2 where hh2: "(A2, B2, C2, D2) = H2" by (cases H2) auto assume "ocircline_eq_cmat H1 H2" then obtain k where *: "k > 0" "A2 = cor k * A1" "B2 = cor k * B1" "C2 = cor k * C1" "D2 = cor k * D1" using hh1[symmetric] hh2[symmetric] by auto let ?dsc1 = "sqrt (Re ((D1 - A1)\<^sup>2 + 4 * (B1 * cnj B1)))" and ?dsc2 = "sqrt (Re ((D2 - A2)\<^sup>2 + 4 * (B2 * cnj B2)))" let ?a11 = "(A1 - D1 + cor ?dsc1) / (2 * C1)" and ?a12 = "(A2 - D2 + cor ?dsc2) / (2 * C2)" let ?a21 = "(A1 - D1 - cor ?dsc1) / (2 * C1)" and ?a22 = "(A2 - D2 - cor ?dsc2) / (2 * C2)" let ?r11 = "sqrt((4 - Re((-4 * ?a11/B1) * A1)) / (1 + Re (?a11*cnj ?a11)))" let ?r12 = "sqrt((4 - Re((-4 * ?a12/B2) * A2)) / (1 + Re (?a12*cnj ?a12)))" let ?r21 = "sqrt((4 - Re((-4 * ?a21/B1) * A1)) / (1 + Re (?a21*cnj ?a21)))" let ?r22 = "sqrt((4 - Re((-4 * ?a22/B2) * A2)) / (1 + Re (?a22*cnj ?a22)))" have "Re ((D2 - A2)\<^sup>2 + 4 * (B2 * cnj B2)) = k\<^sup>2 * Re ((D1 - A1)\<^sup>2 + 4 * (B1 * cnj B1))" using * by (simp add: power2_eq_square field_simps) hence "?dsc2 = k * ?dsc1" using \k > 0\ by (simp add: real_sqrt_mult) hence "A2 - D2 + cor ?dsc2 = cor k * (A1 - D1 + cor ?dsc1)" "A2 - D2 - cor ?dsc2 = cor k * (A1 - D1 - cor ?dsc1)" "2*C2 = cor k * (2*C1)" using * by (auto simp add: field_simps) hence "?a12 = ?a11" "?a22 = ?a21" using \k > 0\ by simp_all moreover have "Re((-4 * ?a12/B2) * A2) = Re((-4 * ?a11/B1) * A1)" using * by (subst \?a12 = ?a11\) (simp, simp add: field_simps) have "?r12 = ?r11" by (subst \Re((-4 * ?a12/B2) * A2) = Re((-4 * ?a11/B1) * A1)\, (subst \?a12 = ?a11\)+) simp moreover have "Re((-4 * ?a22/B2) * A2) = Re((-4 * ?a21/B1) * A1)" using * by (subst \?a22 = ?a21\) (simp, simp add: field_simps) have "?r22 = ?r21" by (subst \Re((-4 * ?a22/B2) * A2) = Re((-4 * ?a21/B1) * A1)\, (subst \?a22 = ?a21\)+) simp moreover have "chordal_circles_cmat H1 = ((?a11, ?r11), (?a21, ?r21))" using hh1[symmetric] unfolding chordal_circles_cmat_def Let_def by (simp del: times_complex.sel) moreover have "chordal_circles_cmat H2 = ((?a12, ?r12), (?a22, ?r22))" using hh2[symmetric] unfolding chordal_circles_cmat_def Let_def by (simp del: times_complex.sel) ultimately show "chordal_circles_cmat H1 = chordal_circles_cmat H2" by metis qed lemma chordal_circle_radius_positive: assumes "hermitean (A, B, C, D)" and "Re (mat_det (A, B, C, D)) \ 0" and "B \ 0" and "dsc = sqrt(Re ((D-A)\<^sup>2 + 4 * (B*cnj B)))" and "a1 = (A - D + cor dsc) / (2 * C)" and "a2 = (A - D - cor dsc) / (2 * C)" shows "Re (A*a1/B) \ -1 \ Re (A*a2/B) \ -1" proof- from assms have "is_real A" "is_real D" "C = cnj B" using hermitean_elems by auto have *: "A*a1/B = ((A - D + cor dsc) / (2 * (B * cnj B))) * A" using \B \ 0\ \C = cnj B\ \a1 = (A - D + cor dsc) / (2 * C)\ by (simp add: field_simps) algebra have **: "A*a2/B = ((A - D - cor dsc) / (2 * (B * cnj B))) * A" using \B \ 0\ \C = cnj B\ \a2 = (A - D - cor dsc) / (2 * C)\ by (simp add: field_simps) algebra have "dsc \ 0" proof- have "0 \ Re ((D - A)\<^sup>2) + 4 * Re ((cor (cmod B))\<^sup>2)" using \is_real A\ \is_real D\ by (subst cor_squared, subst Re_complex_of_real) (simp add: power2_eq_square) thus ?thesis using \dsc = sqrt(Re ((D-A)\<^sup>2 + 4*(B*cnj B)))\ by (subst (asm) complex_mult_cnj_cmod) simp qed hence "Re (A - D - cor dsc) \ Re (A - D + cor dsc)" by simp moreover have "Re (2 * (B * cnj B)) > 0" using \B \ 0\ by (subst complex_mult_cnj_cmod, simp add: power2_eq_square) ultimately have xxx: "Re (A - D + cor dsc) / Re (2 * (B * cnj B)) \ Re (A - D - cor dsc) / Re (2 * (B * cnj B))" (is "?lhs \ ?rhs") by (metis divide_right_mono less_eq_real_def) have "Re A * Re D \ Re (B*cnj B)" using \Re (mat_det (A, B, C, D)) \ 0\ \C = cnj B\ \is_real A\ \is_real D\ by simp have "(Re (2 * (B * cnj B)) / Re A) / Re (2 * B * cnj B) = 1 / Re A" using \Re (2 * (B * cnj B)) > 0\ apply (subst divide_divide_eq_left) apply (subst mult.assoc) apply (subst nonzero_divide_mult_cancel_right) by simp_all show ?thesis proof (cases "Re A > 0") case True hence "Re (A*a1/B) \ Re (A*a2/B)" using * ** \Re (2 * (B * cnj B)) > 0\ \B \ 0\ \is_real A\ \is_real D\ xxx using mult_right_mono[of ?rhs ?lhs "Re A"] apply simp apply (subst Re_divide_real, simp, simp) apply (subst Re_divide_real, simp, simp) apply (subst Re_mult_real, simp)+ apply simp done moreover have "Re (A*a2/B) \ -1" proof- from \Re A * Re D \ Re (B*cnj B)\ have "Re (A\<^sup>2) \ Re (B*cnj B) + Re ((A - D)*A)" using \Re A > 0\ \is_real A\ \is_real D\ by (simp add: power2_eq_square field_simps) have "1 \ Re (B*cnj B) / Re (A\<^sup>2) + Re (A - D) / Re A" using \Re A > 0\ \is_real A\ \is_real D\ using divide_right_mono[OF \Re (A\<^sup>2) \ Re (B*cnj B) + Re ((A - D)*A)\, of "Re (A\<^sup>2)"] by (simp add: power2_eq_square add_divide_distrib) have "4 * Re(B*cnj B) \ 4 * (Re (B*cnj B))\<^sup>2 / Re (A\<^sup>2) + 2*Re (A - D) / Re A * 2 * Re(B*cnj B)" using mult_right_mono[OF \1 \ Re (B*cnj B) / Re (A\<^sup>2) + Re (A - D) / Re A\, of "4 * Re (B*cnj B)"] by (simp add: distrib_right) (simp add: power2_eq_square field_simps) moreover have "A \ 0" using \Re A > 0\ by auto hence "4 * (Re (B*cnj B))\<^sup>2 / Re (A\<^sup>2) = Re (4 * (B*cnj B)\<^sup>2 / A\<^sup>2)" using Re_divide_real[of "A\<^sup>2" "4 * (B*cnj B)\<^sup>2"] \Re A > 0\ \is_real A\ by (auto simp add: power2_eq_square) moreover have "2*Re (A - D) / Re A * 2 * Re(B*cnj B) = Re (2 * (A - D) / A * 2 * B * cnj B)" using \is_real A\ \is_real D\ \A \ 0\ using Re_divide_real[of "A" "(4 * A - 4 * D) * B * cnj B"] by (simp add: field_simps) ultimately have "Re ((D - A)\<^sup>2 + 4 * B*cnj B) \ Re((A - D)\<^sup>2 + 4 * (B*cnj B)\<^sup>2 / A\<^sup>2 + 2*(A - D) / A * 2 * B*cnj B)" by (simp add: field_simps power2_eq_square) hence "Re ((D - A)\<^sup>2 + 4 * B*cnj B) \ Re(((A - D) + 2 * B*cnj B / A)\<^sup>2)" using \A \ 0\ by (subst power2_sum) (simp add: power2_eq_square field_simps) hence "dsc \ sqrt (Re(((A - D) + 2 * B*cnj B / A)\<^sup>2))" using \dsc = sqrt(Re ((D-A)\<^sup>2 + 4*(B*cnj B)))\ by simp moreover have "Re(((A - D) + 2 * B*cnj B / A)\<^sup>2) = (Re((A - D) + 2 * B*cnj B / A))\<^sup>2" using \is_real A\ \is_real D\ div_reals by (simp add: power2_eq_square) ultimately have "dsc \ \Re (A - D + 2 * B * cnj B / A)\" by simp moreover have "Re (A - D + 2 * B * cnj B / A) \ 0" proof- have *: "Re (A\<^sup>2 + B*cnj B) \ 0" using \is_real A\ by (simp add: power2_eq_square) also have "Re (A\<^sup>2 + 2*B*cnj B - A*D) \ Re (A\<^sup>2 + B*cnj B)" using \Re A * Re D \ Re (B*cnj B)\ using \is_real A\ \is_real D\ by simp finally have "Re (A\<^sup>2 + 2*B*cnj B - A*D) \ 0" by simp show ?thesis using divide_right_mono[OF \Re (A\<^sup>2 + 2*B*cnj B - A*D) \ 0\, of "Re A"] \Re A > 0\ \is_real A\ \A \ 0\ by (simp add: add_divide_distrib diff_divide_distrib) (subst Re_divide_real, auto simp add: power2_eq_square field_simps) qed ultimately have "dsc \ Re (A - D + 2 * B * cnj B / A)" by simp hence "- Re (2 * (B * cnj B) / A) \ Re ((A - D - cor dsc))" by (simp add: field_simps) hence *: "- (Re (2 * (B * cnj B)) / Re A) \ Re (A - D - cor dsc)" using \is_real A\ \A \ 0\ by (subst (asm) Re_divide_real, auto) from divide_right_mono[OF this, of "Re (2 * B * cnj B)"] have "- 1 / Re A \ Re (A - D - cor dsc) / Re (2 * B * cnj B)" using \Re A > 0\ \B \ 0\ \A \ 0\ \0 < Re (2 * (B * cnj B))\ using \(Re (2 * (B * cnj B)) / Re A) / Re (2 * B * cnj B) = 1 / Re A\ by simp from mult_right_mono[OF this, of "Re A"] show ?thesis using \is_real A\ \is_real D\ \B \ 0\ \Re A > 0\ \A \ 0\ apply (subst **) apply (subst Re_mult_real, simp) apply (subst Re_divide_real, simp, simp) apply (simp add: field_simps) done qed ultimately show ?thesis by simp next case False show ?thesis proof (cases "Re A < 0") case True hence "Re (A*a1/B) \ Re (A*a2/B)" using * ** \Re (2 * (B * cnj B)) > 0\ \B \ 0\ \is_real A\ \is_real D\ xxx using mult_right_mono_neg[of ?rhs ?lhs "Re A"] apply simp apply (subst Re_divide_real, simp, simp) apply (subst Re_divide_real, simp, simp) apply (subst Re_mult_real, simp)+ apply simp done moreover have "Re (A*a1/B) \ -1" proof- from \Re A * Re D \ Re (B*cnj B)\ have "Re (A\<^sup>2) \ Re (B*cnj B) - Re ((D - A)*A)" using \Re A < 0\ \is_real A\ \is_real D\ by (simp add: power2_eq_square field_simps) hence "1 \ Re (B*cnj B) / Re (A\<^sup>2) - Re (D - A) / Re A" using \Re A < 0\ \is_real A\ \is_real D\ using divide_right_mono[OF \Re (A\<^sup>2) \ Re (B*cnj B) - Re ((D - A)*A)\, of "Re (A\<^sup>2)"] by (simp add: power2_eq_square diff_divide_distrib) have "4 * Re(B*cnj B) \ 4 * (Re (B*cnj B))\<^sup>2 / Re (A\<^sup>2) - 2*Re (D - A) / Re A * 2 * Re(B*cnj B)" using mult_right_mono[OF \1 \ Re (B*cnj B) / Re (A\<^sup>2) - Re (D - A) / Re A\, of "4 * Re (B*cnj B)"] by (simp add: left_diff_distrib) (simp add: power2_eq_square field_simps) moreover have "A \ 0" using \Re A < 0\ by auto hence "4 * (Re (B*cnj B))\<^sup>2 / Re (A\<^sup>2) = Re (4 * (B*cnj B)\<^sup>2 / A\<^sup>2)" using Re_divide_real[of "A\<^sup>2" "4 * (B*cnj B)\<^sup>2"] \Re A < 0\ \is_real A\ by (auto simp add: power2_eq_square) moreover have "2*Re (D - A) / Re A * 2 * Re(B*cnj B) = Re (2 * (D - A) / A * 2 * B * cnj B)" using \is_real A\ \is_real D\ \A \ 0\ using Re_divide_real[of "A" "(4 * D - 4 * A) * B * cnj B"] by (simp add: field_simps) ultimately have "Re ((D - A)\<^sup>2 + 4 * B*cnj B) \ Re((D - A)\<^sup>2 + 4 * (B*cnj B)\<^sup>2 / A\<^sup>2 - 2*(D - A) / A * 2 * B*cnj B)" by (simp add: field_simps power2_eq_square) hence "Re ((D - A)\<^sup>2 + 4 * B*cnj B) \ Re(((D - A) - 2 * B*cnj B / A)\<^sup>2)" using \A \ 0\ by (subst power2_diff) (simp add: power2_eq_square field_simps) hence "dsc \ sqrt (Re(((D - A) - 2 * B*cnj B / A)\<^sup>2))" using \dsc = sqrt(Re ((D-A)\<^sup>2 + 4*(B*cnj B)))\ by simp moreover have "Re(((D - A) - 2 * B*cnj B / A)\<^sup>2) = (Re((D - A) - 2 * B*cnj B / A))\<^sup>2" using \is_real A\ \is_real D\ div_reals by (simp add: power2_eq_square) ultimately have "dsc \ \Re (D - A - 2 * B * cnj B / A)\" by simp moreover have "Re (D - A - 2 * B * cnj B / A) \ 0" proof- have "Re (A\<^sup>2 + B*cnj B) \ 0" using \is_real A\ by (simp add: power2_eq_square) also have "Re (A\<^sup>2 + 2*B*cnj B - A*D) \ Re (A\<^sup>2 + B*cnj B)" using \Re A * Re D \ Re (B*cnj B)\ using \is_real A\ \is_real D\ by simp finally have "Re (A\<^sup>2 + 2*B*cnj B - A*D) \ 0" by simp show ?thesis using divide_right_mono_neg[OF \Re (A\<^sup>2 + 2*B*cnj B - A*D) \ 0\, of "Re A"] \Re A < 0\ \is_real A\ \A \ 0\ by (simp add: add_divide_distrib diff_divide_distrib) (subst Re_divide_real, auto simp add: power2_eq_square field_simps) qed ultimately have "dsc \ Re (D - A - 2 * B * cnj B / A)" by simp hence "- Re (2 * (B * cnj B) / A) \ Re ((A - D + cor dsc))" by (simp add: field_simps) hence "- (Re (2 * (B * cnj B)) / Re A) \ Re (A - D + cor dsc)" using \is_real A\ \A \ 0\ by (subst (asm) Re_divide_real, auto) from divide_right_mono[OF this, of "Re (2 * B * cnj B)"] have "- 1 / Re A \ Re (A - D + cor dsc) / Re (2 * B * cnj B)" using \Re A < 0\ \B \ 0\ \A \ 0\ \0 < Re (2 * (B * cnj B))\ using \(Re (2 * (B * cnj B)) / Re A) / Re (2 * B * cnj B) = 1 / Re A\ by simp from mult_right_mono_neg[OF this, of "Re A"] show ?thesis using \is_real A\ \is_real D\ \B \ 0\ \Re A < 0\ \A \ 0\ apply (subst *) apply (subst Re_mult_real, simp) apply (subst Re_divide_real, simp, simp) apply (simp add: field_simps) done qed ultimately show ?thesis by simp next case False hence "A = 0" using \\ Re A > 0\ \is_real A\ using complex_eq_if_Re_eq by auto thus ?thesis by simp qed qed qed lemma chordal_circle_det_positive: fixes x y :: real assumes "x * y < 0" shows "x / (x - y) > 0" proof (cases "x > 0") case True hence "y < 0" using \x * y < 0\ by (smt mult_nonneg_nonneg) have "x - y > 0" using \x > 0\ \y < 0\ by auto thus ?thesis using \x > 0\ by (metis zero_less_divide_iff) next case False hence *: "y > 0 \ x < 0" using \x * y < 0\ using mult_nonpos_nonpos[of x y] by (cases "x=0") force+ have "x - y < 0" using * by auto thus ?thesis using * by (metis zero_less_divide_iff) qed lemma chordal_circle1: assumes "is_real A" and "is_real D" and "Re (A * D) < 0" and "r = sqrt(Re ((4*A)/(A-D)))" shows "mk_circline A 0 0 D = chordal_circle \\<^sub>h r" using assms proof (transfer, transfer) fix A D r assume *: "is_real A" "is_real D" "Re (A * D) < 0" "r = sqrt (Re ((4*A)/(A-D)))" hence "A \ 0 \ D \ 0" by auto hence "(A, 0, 0, D) \ hermitean_nonzero" using eq_cnj_iff_real[of A] eq_cnj_iff_real[of D] * unfolding hermitean_def by (simp add: mat_adj_def mat_cnj_def) moreover have "(- (cor r)\<^sup>2, 0, 0, 4 - (cor r)\<^sup>2) \ hermitean_nonzero" by (simp add: hermitean_def mat_adj_def mat_cnj_def power2_eq_square) moreover have "A \ D" using \Re (A * D) < 0\ \is_real A\ \is_real D\ by auto have "Re ((4*A)/(A-D)) \ 0" proof- have "Re A / Re (A - D) \ 0" using \Re (A * D) < 0\ \is_real A\ \is_real D\ using chordal_circle_det_positive[of "Re A" "Re D"] by simp thus ?thesis using \is_real A\ \is_real D\ \A \ D\ by (subst Re_divide_real, auto) qed moreover have "- (cor (sqrt (Re (4 * A / (A - D)))))\<^sup>2 = cor (Re (4 / (D - A))) * A" using \Re ((4*A)/(A-D)) \ 0\ \is_real A\ \is_real D\ \A \ D\ by (subst cor_squared, subst real_sqrt_power[symmetric], simp) (simp add: Re_divide_real Re_mult_real minus_divide_right) moreover have "4 * (A - D) - 4 * A = 4 * -D" by (simp add: field_simps) hence "4 - 4 * A / (A - D) = -4 * D / (A - D)" using \A \ D\ by (smt ab_semigroup_mult_class.mult_ac(1) diff_divide_eq_iff eq_iff_diff_eq_0 mult_minus1 mult_minus1_right mult_numeral_1_right right_diff_distrib_numeral times_divide_eq_right) hence "4 - 4 * A / (A - D) = 4 * D / (D - A)" by (metis (hide_lams, no_types) minus_diff_eq minus_divide_left minus_divide_right minus_mult_left) hence **: "4 - (cor (sqrt (Re (4 * A / (A - D)))))\<^sup>2 = cor (Re (4 / (D - A))) * D" using \Re ((4*A)/(A-D)) \ 0\ \is_real A\ \is_real D\ \A \ D\ by (subst cor_squared, subst real_sqrt_power[symmetric], simp) ultimately show "circline_eq_cmat (mk_circline_cmat A 0 0 D) (chordal_circle_cvec_cmat \\<^sub>v r)" using * \is_real A\ \is_real D\ \A \ D\ \r = sqrt(Re ((4*A)/(A-D)))\ by (simp, rule_tac x="Re(4/(D-A))" in exI, auto, simp_all add: **) qed lemma chordal_circle2: assumes "is_real A" and "is_real D" and "Re (A * D) < 0" and "r = sqrt(Re ((4*D)/(D-A)))" shows "mk_circline A 0 0 D = chordal_circle 0\<^sub>h r" using assms proof (transfer, transfer) fix A D r assume *: "is_real A" "is_real D" "Re (A * D) < 0" "r = sqrt (Re ((4*D)/(D-A)))" hence "A \ 0 \ D \ 0" by auto hence "(A, 0, 0, D) \ {H. hermitean H \ H \ mat_zero}" using eq_cnj_iff_real[of A] eq_cnj_iff_real[of D] * unfolding hermitean_def by (simp add: mat_adj_def mat_cnj_def) moreover have "(4 - (cor r)\<^sup>2, 0, 0, - (cor r)\<^sup>2) \ {H. hermitean H \ H \ mat_zero}" by (auto simp add: hermitean_def mat_adj_def mat_cnj_def power2_eq_square) moreover have "A \ D" using \Re (A * D) < 0\ \is_real A\ \is_real D\ by auto have "Re((4*D)/(D-A)) \ 0" proof- have "Re D / Re (D - A) \ 0" using \Re (A * D) < 0\ \is_real A\ \is_real D\ using chordal_circle_det_positive[of "Re D" "Re A"] by (simp add: field_simps) thus ?thesis using \is_real A\ \is_real D\ \A \ D\ by (subst Re_divide_real, auto) qed have "4 * (D - A) - 4 * D = 4 * -A" by (simp add: field_simps) hence "4 - 4 * D / (D - A) = -4 * A / (D - A)" using \A \ D\ by (smt ab_semigroup_mult_class.mult_ac(1) diff_divide_eq_iff eq_iff_diff_eq_0 mult_minus1 mult_minus1_right mult_numeral_1_right right_diff_distrib_numeral times_divide_eq_right) hence "4 - 4 * D / (D - A) = 4 * A / (A - D)" by (metis (hide_lams, no_types) minus_diff_eq minus_divide_left minus_divide_right minus_mult_left) hence **: "4 - (cor (sqrt (Re ((4*D)/(D-A)))))\<^sup>2 = cor (Re (4 / (A - D))) * A" using \is_real A\ \is_real D\ \A \ D\ \Re (4 * D / (D - A)) \ 0\ by (subst cor_squared, subst real_sqrt_power[symmetric], simp) moreover have "- (cor (sqrt (Re ((4*D)/(D-A)))))\<^sup>2 = cor (Re (4 / (A - D))) * D" using \is_real A\ \is_real D\ \A \ D\ \Re ((4*D)/(D-A)) \ 0\ by (subst cor_squared, subst real_sqrt_power[symmetric], simp) (simp add: Re_divide_real minus_divide_right) ultimately show "circline_eq_cmat (mk_circline_cmat A 0 0 D) (chordal_circle_cvec_cmat 0\<^sub>v r)" using \is_real A\ \is_real D\ \A \ 0 \ D \ 0\ \r = sqrt (Re ((4*D)/(D-A)))\ using * by (simp, rule_tac x="Re (4/(A-D))" in exI, auto, simp_all add: **) qed lemma chordal_circle': assumes "B \ 0" and "(A, B, C, D) \ hermitean_nonzero" and "Re (mat_det (A, B, C, D)) \ 0" and "C * a\<^sup>2 + (D - A) * a - B = 0" and "r = sqrt((4 - Re((-4 * a/B) * A)) / (1 + Re (a*cnj a)))" shows "mk_circline A B C D = chordal_circle (of_complex a) r" using assms proof (transfer, transfer) fix A B C D a :: complex and r :: real let ?k = "(-4) * a / B" assume *: "(A, B, C, D) \ {H. hermitean H \ H \ mat_zero}" and **: "B \ 0" "C * a\<^sup>2 + (D - A) * a - B = 0" and rr: "r = sqrt ((4 - Re (?k * A)) / (1 + Re (a * cnj a)))" and det: "Re (mat_det (A, B, C, D)) \ 0" have "is_real A" "is_real D" "C = cnj B" using * hermitean_elems by auto from ** have a12: "let dsc = sqrt(Re ((D-A)\<^sup>2 + 4 * (B*cnj B))) in a = (A - D + cor dsc) / (2 * C) \ a = (A - D - cor dsc) / (2 * C)" proof- have "Re ((D-A)\<^sup>2 + 4 * (B*cnj B)) \ 0" using \is_real A\ \is_real D\ by (subst complex_mult_cnj_cmod) (simp add: power2_eq_square) hence "ccsqrt ((D - A)\<^sup>2 - 4 * C * - B) = cor (sqrt (Re ((D - A)\<^sup>2 + 4 * (B * cnj B))))" using csqrt_real[of "((D - A)\<^sup>2 + 4 * (B * cnj B))"] \is_real A\ \is_real D\ \C = cnj B\ by (auto simp add: power2_eq_square field_simps) thus ?thesis using complex_quadratic_equation_two_roots[of C a "D - A" "-B"] using \C * a\<^sup>2 + (D - A) * a - B = 0\ \B \ 0\ \C = cnj B\ by (simp add: Let_def) qed have "is_real ?k" using a12 \C = cnj B\ \is_real A\ \is_real D\ by (auto simp add: Let_def) have "a \ 0" using ** by auto hence "Re ?k \ 0" using \is_real (-4*a / B)\ \B \ 0\ by (metis complex.expand divide_eq_0_iff divisors_zero zero_complex.simps(1) zero_complex.simps(2) zero_neq_neg_numeral) moreover have "(-4) * a = cor (Re ?k) * B" using complex_of_real_Re[OF \is_real (-4*a/B)\] \B \ 0\ by simp moreover have "is_real (a/B)" using \is_real ?k\ is_real_mult_real[of "-4" "a / B"] by simp hence "is_real (B * cnj a)" using * \C = cnj B\ by (metis (no_types, lifting) Im_complex_div_eq_0 complex_cnj_divide eq_cnj_iff_real hermitean_elems(3) mem_Collect_eq mult.commute) hence "B * cnj a = cnj B * a" using eq_cnj_iff_real[of "B * cnj a"] by simp hence "-4 * cnj a = cor (Re ?k) * C" using \C = cnj B\ using complex_of_real_Re[OF \is_real ?k\] \B \ 0\ by (simp, simp add: field_simps) moreover have "1 + a * cnj a \ 0" by (subst complex_mult_cnj_cmod) (smt cor_add of_real_0 of_real_1 of_real_eq_iff realpow_square_minus_le) have "r\<^sup>2 = (4 - Re (?k * A)) / (1 + Re (a * cnj a))" proof- have "Re (a / B * A) \ -1" using a12 chordal_circle_radius_positive[of A B C D] * \B \ 0\ det by (auto simp add: Let_def field_simps) from mult_right_mono_neg[OF this, of "-4"] have "4 - Re (?k * A) \ 0" using Re_mult_real[of "-4" "a / B * A"] by (simp add: field_simps) moreover have "1 + Re (a * cnj a) > 0" using \a \ 0\ complex_mult_cnj complex_neq_0 by auto ultimately have "(4 - Re (?k * A)) / (1 + Re (a * cnj a)) \ 0" by (metis divide_nonneg_pos) thus ?thesis using rr by simp qed hence "r\<^sup>2 = Re ((4 - ?k * A) / (1 + a * cnj a))" using \is_real ?k\ \is_real A\ \1 + a * cnj a \ 0\ by (subst Re_divide_real, auto) hence "(cor r)\<^sup>2 = (4 - ?k * A) / (1 + a * cnj a)" using \is_real ?k\ \is_real A\ using mult_reals[of ?k A] by (simp add: cor_squared) hence "4 - (cor r)\<^sup>2 * (a * cnj a + 1) = cor (Re ?k) * A" using complex_of_real_Re[OF \is_real (-4*a/B)\] using \1 + a * cnj a \ 0\ by (simp add: field_simps) moreover have "?k = cnj ?k" using \is_real ?k\ using eq_cnj_iff_real[of "-4*a/B"] by simp have "?k\<^sup>2 = cor ((cmod ?k)\<^sup>2)" using cor_cmod_real[OF \is_real ?k\] unfolding power2_eq_square by (subst cor_mult) (metis minus_mult_minus) hence "?k\<^sup>2 = ?k * cnj ?k" using complex_mult_cnj_cmod[of ?k] by simp hence ***: "a * cnj a = (cor ((Re ?k)\<^sup>2) * B * C) / 16" using complex_of_real_Re[OF \is_real (-4*a/B)\] \C = cnj B\ \is_real (-4*a/B)\ \B \ 0\ by simp from ** have "cor ((Re ?k)\<^sup>2) * B * C - 4 * cor (Re ?k) * (D-A) - 16 = 0" using complex_of_real_Re[OF \is_real ?k\] by (simp add: power2_eq_square, simp add: field_simps, algebra) hence "?k * (D-A) = 4 * (cor ((Re ?k)\<^sup>2) * B * C / 16 - 1)" by (subst (asm) complex_of_real_Re[OF \is_real ?k\]) algebra hence "?k * (D-A) = 4 * (a*cnj a - 1)" by (subst (asm) ***[symmetric]) simp hence "4 * a * cnj a - (cor r)\<^sup>2 * (a * cnj a + 1) = cor (Re ?k) * D" using \4 - (cor r)\<^sup>2 * (a * cnj a + 1) = cor (Re ?k) * A\ using complex_of_real_Re[OF \is_real (-4*a/B)\] by simp algebra ultimately show "circline_eq_cmat (mk_circline_cmat A B C D) (chordal_circle_cvec_cmat (of_complex_cvec a) r)" using * \a \ 0\ by (simp, rule_tac x="Re (-4*a / B)" in exI, simp) qed end diff --git a/thys/Gauss_Sums/Complex_Roots_Of_Unity.thy b/thys/Gauss_Sums/Complex_Roots_Of_Unity.thy --- a/thys/Gauss_Sums/Complex_Roots_Of_Unity.thy +++ b/thys/Gauss_Sums/Complex_Roots_Of_Unity.thy @@ -1,286 +1,286 @@ (* File: Complex_Roots_Of_Unity.thy Authors: Rodrigo Raya, EPFL; Manuel Eberl, TUM Complex roots of unity (exp(2i\/n)) and sums over them. *) theory Complex_Roots_Of_Unity imports "HOL-Analysis.Analysis" Periodic_Arithmetic begin section \Complex roots of unity\ definition "unity_root k n = cis (2 * pi * of_int n / of_nat k)" lemma unity_root_k_0 [simp]: "unity_root k 0 = 1" and unity_root_0_n [simp]: "unity_root 0 n = 1" unfolding unity_root_def by simp+ lemma unity_root_conv_exp: "unity_root k n = exp (of_real (2*pi*n/k) * \)" unfolding unity_root_def by (subst cis_conv_exp,subst mult.commute,blast) lemma unity_root_mod: "unity_root k (n mod int k) = unity_root k n" proof (cases "k = 0") case True then show ?thesis by simp next case False obtain q :: int where q_def: "n = q*k + (n mod k)" using div_mult_mod_eq[symmetric] by blast have "n / k = q + (n mod k) / k" proof (auto simp add: divide_simps False) have "real_of_int n = real_of_int (q*k + (n mod k))" using q_def by simp also have "\ = real_of_int q * real k + real_of_int (n mod k)" using of_int_add of_int_mult by simp finally show "real_of_int n = real_of_int q * real k + real_of_int (n mod k)" by blast qed then have "(2*pi*n/k) = 2*pi*q + (2*pi*(n mod k)/k)" using False by (auto simp add: field_simps) then have "(2*pi*n/k)*\ = 2*pi*q*\ + (2*pi*(n mod k)/k)*\" (is "?l = ?r1 + ?r2") by (auto simp add: algebra_simps) then have "exp ?l = exp ?r2" using exp_plus_2pin by (simp add: exp_add mult.commute) then show ?thesis using unity_root_def unity_root_conv_exp by simp qed lemma unity_root_cong: assumes "[m = n] (mod int k)" shows "unity_root k m = unity_root k n" proof - from assms have "m mod int k = n mod int k" by (auto simp: cong_def) hence "unity_root k (m mod int k) = unity_root k (n mod int k)" by simp thus ?thesis by (simp add: unity_root_mod) qed lemma unity_root_mod_nat: "unity_root k (nat (n mod int k)) = unity_root k n" proof (cases k) case (Suc l) then have "n mod int k \ 0" by auto show ?thesis unfolding int_nat_eq by (simp add: \n mod int k \ 0\ unity_root_mod) qed auto lemma unity_root_eqD: assumes gr: "k > 0" assumes eq: "unity_root k i = unity_root k j" shows "i mod k = j mod k" proof - let ?arg1 = "(2*pi*i/k)* \" let ?arg2 = "(2*pi*j/k)* \" from eq unity_root_conv_exp have "exp ?arg1 = exp ?arg2" by simp from this exp_eq obtain n :: int where "?arg1 = ?arg2 +(2*n*pi)*\" by blast then have e1: "?arg1 - ?arg2 = 2*n*pi*\" by simp have e2: "?arg1 - ?arg2 = 2*(i-j)*(1/k)*pi*\" by (auto simp add: algebra_simps) from e1 e2 have "2*n*pi*\ = 2*(i-j)*(1/k)*pi*\" by simp then have "2*n*k*pi*\ = 2*(i-j)*pi*\" by (simp add: divide_simps \k > 0\)(simp add: field_simps) then have "2*n*k = 2*(i-j)" by (meson complex_i_not_zero mult_cancel_right of_int_eq_iff of_real_eq_iff pi_neq_zero) then have "n*k = i-j" by auto then show ?thesis by Groebner_Basis.algebra qed lemma unity_root_eq_1_iff: fixes k n :: nat assumes "k > 0" shows "unity_root k n = 1 \ k dvd n" proof - have "unity_root k n = exp ((2*pi*n/k) * \)" by (simp add: unity_root_conv_exp) also have "exp ((2*pi*n/k)* \) = 1 \ k dvd n" using complex_root_unity_eq_1[of k n] assms by (auto simp add: algebra_simps) finally show ?thesis by simp qed lemma unity_root_pow: "unity_root k n ^ m = unity_root k (n * m)" using unity_root_def - by (simp add: Complex.DeMoivre linordered_field_class.sign_simps(6) mult.commute) + by (simp add: Complex.DeMoivre mult.commute algebra_split_simps(6)) lemma unity_root_add: "unity_root k (m + n) = unity_root k m * unity_root k n" by (simp add: unity_root_conv_exp add_divide_distrib algebra_simps exp_add) lemma unity_root_uminus: "unity_root k (-m) = cnj (unity_root k m)" unfolding unity_root_conv_exp exp_cnj by simp lemma inverse_unity_root: "inverse (unity_root k m) = cnj (unity_root k m)" unfolding unity_root_conv_exp exp_cnj by (simp add: field_simps exp_minus) lemma unity_root_diff: "unity_root k (m - n) = unity_root k m * cnj (unity_root k n)" using unity_root_add[of k m "-n"] by (simp add: unity_root_uminus) lemma unity_root_eq_1_iff_int: fixes k :: nat and n :: int assumes "k > 0" shows "unity_root k n = 1 \ k dvd n" proof (cases "n \ 0") case True obtain n' where "n = int n'" using zero_le_imp_eq_int[OF True] by blast then show ?thesis using unity_root_eq_1_iff[OF \k > 0\, of n'] of_nat_dvd_iff by blast next case False then have "-n \ 0" by auto have "unity_root k n = inverse (unity_root k (-n))" unfolding inverse_unity_root by (simp add: unity_root_uminus) then have "(unity_root k n = 1) = (unity_root k (-n) = 1)" by simp also have "(unity_root k (-n) = 1) = (k dvd (-n))" using unity_root_eq_1_iff[of k "nat (-n)",OF \k > 0\] False int_dvd_int_iff[of k "nat (-n)"] nat_0_le[OF \-n \ 0\] by auto finally show ?thesis by simp qed lemma unity_root_eq_1 [simp]: "int k dvd n \ unity_root k n = 1" by (cases "k = 0") (auto simp: unity_root_eq_1_iff_int) lemma unity_periodic_arithmetic: "periodic_arithmetic (unity_root k) k" unfolding periodic_arithmetic_def proof fix n have "unity_root k (n + k) = unity_root k ((n+k) mod k)" using unity_root_mod[of k] zmod_int by presburger also have "unity_root k ((n+k) mod k) = unity_root k n" using unity_root_mod zmod_int by auto finally show "unity_root k (n + k) = unity_root k n" by simp qed lemma unity_periodic_arithmetic_mult: "periodic_arithmetic (\n. unity_root k (m * int n)) k" unfolding periodic_arithmetic_def proof fix n have "unity_root k (m * int (n + k)) = unity_root k (m*n + m*k)" by (simp add: algebra_simps) also have "\ = unity_root k (m*n)" using unity_root_mod[of k "m * int n"] unity_root_mod[of k "m * int n + m * int k"] mod_mult_self3 by presburger finally show "unity_root k (m * int (n + k)) = unity_root k (m * int n)" by simp qed lemma unity_root_periodic_arithmetic_mult_minus: shows "periodic_arithmetic (\i. unity_root k (-int i*int m)) k" unfolding periodic_arithmetic_def proof fix n have "unity_root k (-(n + k) * m) = cnj (unity_root k (n*m+k*m))" by (simp add: ring_distribs unity_root_diff unity_root_add unity_root_uminus) also have "\ = cnj (unity_root k (n*m))" using mult_period[of "unity_root k" k m] unity_periodic_arithmetic[of k] unfolding periodic_arithmetic_def by presburger also have "\ = unity_root k (-n*m)" by (simp add: unity_root_uminus) finally show "unity_root k (-(n + k) * m) = unity_root k (-n*m)" by simp qed lemma unity_div: fixes a :: int and d :: nat assumes "d dvd k" shows "unity_root k (a*d) = unity_root (k div d) a" proof - have 1: "(2*pi*(a*d)/k) = (2*pi*a)/(k div d)" using Suc_pred assms by (simp add: divide_simps, fastforce) have "unity_root k (a*d) = exp ((2*pi*(a*d)/k)* \)" using unity_root_conv_exp by simp also have "\ = exp (((2*pi*a)/(k div d))* \)" using 1 by simp also have "\ = unity_root (k div d) a" using unity_root_conv_exp by simp finally show ?thesis by simp qed lemma unity_div_num: assumes "k > 0" "d > 0" "d dvd k" shows "unity_root k (x * (k div d)) = unity_root d x" using assms dvd_div_mult_self unity_div by auto section \Geometric sums of roots of unity\ text\ Apostol calls these `geometric sums', which is a bit too generic. We therefore decided to refer to them as `sums of roots of unity'. \ definition "unity_root_sum k n = (\m 0 \ unity_root_sum k 0 = k" unfolding unity_root_sum_def by simp_all text \Theorem 8.1\ theorem unity_root_sum: fixes k :: nat and n :: int assumes gr: "k \ 1" shows "k dvd n \ unity_root_sum k n = k" and "\k dvd n \ unity_root_sum k n = 0" proof - assume dvd: "k dvd n" let ?x = "unity_root k n" have unit: "?x = 1" using dvd gr unity_root_eq_1_iff_int by auto have exp: "?x^m = unity_root k (n*m)" for m using unity_root_pow by simp have "unity_root_sum k n = (\m = (\m = (\m = k" using gr by (induction k, auto) finally show "unity_root_sum k n = k" by simp next assume dvd: "\k dvd n" let ?x = "unity_root k n" have "?x \ 1" using dvd gr unity_root_eq_1_iff_int by auto have "(?x^k - 1)/(?x - 1) = (\m?x \ 1\] by auto then have sum: "unity_root_sum k n = (?x^k - 1)/(?x - 1)" using unity_root_sum_def unity_root_pow by simp have "?x^k = 1" using gr unity_root_eq_1_iff_int unity_root_pow by simp then show "unity_root_sum k n = 0" using sum by auto qed corollary unity_root_sum_periodic_arithmetic: "periodic_arithmetic (unity_root_sum k) k" unfolding periodic_arithmetic_def proof fix n show "unity_root_sum k (n + k) = unity_root_sum k n" by (cases "k = 0"; cases "k dvd n") (auto simp add: unity_root_sum) qed lemma unity_root_sum_nonzero_iff: fixes r :: int assumes "k \ 1" and "r \ {-k<.. 0 \ r = 0" proof assume "unity_root_sum k r \ 0" then have "k dvd r" using unity_root_sum assms by blast then show "r = 0" using assms(2) using dvd_imp_le_int by force next assume "r = 0" then have "k dvd r" by auto then have "unity_root_sum k r = k" using assms(1) unity_root_sum by blast then show "unity_root_sum k r \ 0" using assms(1) by simp qed end \ No newline at end of file diff --git a/thys/Poincare_Disc/Poincare.thy b/thys/Poincare_Disc/Poincare.thy --- a/thys/Poincare_Disc/Poincare.thy +++ b/thys/Poincare_Disc/Poincare.thy @@ -1,210 +1,210 @@ section\Poincar\'e disc model types\ text \In this section we introduce datatypes that represent objects in the Poincar\'e disc model. The types are defined as subtypes (e.g., the h-points are defined as elements of $\mathbb{C}P^1$ that lie within the unit disc). The functions on those types are defined by lifting the functions defined on the carrier type (e.g., h-distance is defined by lifting the distance function defined for elements of $\mathbb{C}P^1$).\ theory Poincare imports Poincare_Lines Poincare_Between Poincare_Distance Poincare_Circles begin (* ------------------------------------------------------------------ *) subsection \H-points\ (* ------------------------------------------------------------------ *) typedef p_point = "{z. z \ unit_disc}" using zero_in_unit_disc by (rule_tac x="0\<^sub>h" in exI, simp) setup_lifting type_definition_p_point text \Point zero\ lift_definition p_zero :: "p_point" is "0\<^sub>h" by (rule zero_in_unit_disc) text \Constructing h-points from complex numbers\ lift_definition p_of_complex :: "complex \ p_point" is "\ z. if cmod z < 1 then of_complex z else 0\<^sub>h" by auto (* ------------------------------------------------------------------ *) subsection \H-lines\ (* ------------------------------------------------------------------ *) typedef p_line = "{H. is_poincare_line H}" by (rule_tac x="x_axis" in exI, simp) setup_lifting type_definition_p_line lift_definition p_incident :: "p_line \ p_point \ bool" is on_circline done text \Set of h-points on an h-line\ definition p_points :: "p_line \ p_point set" where "p_points l = {p. p_incident l p}" text \x-axis is an example of an h-line\ lift_definition p_x_axis :: "p_line" is x_axis by simp text \Constructing the unique h-line from two h-points\ lift_definition p_line :: "p_point \ p_point \ p_line" is poincare_line proof- fix u v show "is_poincare_line (poincare_line u v)" proof (cases "u \ v") case True thus ?thesis by simp next text\This branch must work only for formal reasons.\ case False thus ?thesis by (transfer, transfer, auto simp add: hermitean_def mat_adj_def mat_cnj_def split: if_split_asm) qed qed text \Next we show how to lift some lemmas. This could be done for all the lemmas that we have proved earlier, but we do not do that.\ text \If points are different then the constructed line contains the starting points\ lemma p_on_line: assumes "z \ w" shows "p_incident (p_line z w) z" "p_incident (p_line z w) w" using assms by (transfer, simp)+ text \There is a unique h-line passing trough the two different given h-points\ lemma assumes "u \ v" shows "\! l. {u, v} \ p_points l" using assms apply (rule_tac a="p_line u v" in ex1I, auto simp add: p_points_def p_on_line) apply (transfer, simp add: unique_poincare_line) done text \The unique h-line trough zero and a non-zero h-point on the x-axis is the x-axis\ lemma assumes "p_zero \ p_points l" "u \ p_points l" "u \ p_zero" "u \ p_points p_x_axis" shows "l = p_x_axis" using assms unfolding p_points_def apply simp apply transfer using is_poincare_line_0_real_is_x_axis inf_notin_unit_disc unfolding circline_set_def by blast (* ------------------------------------------------------------------ *) subsection \H-collinearity\ (* ------------------------------------------------------------------ *) lift_definition p_collinear :: "p_point set \ bool" is poincare_collinear done (* ------------------------------------------------------------------ *) subsection \H-isometries\ (* ------------------------------------------------------------------ *) text \H-isometries are functions that map the unit disc onto itself\ typedef p_isometry = "{f. unit_disc_fix_f f}" by (rule_tac x="id" in exI, simp add: unit_disc_fix_f_def, rule_tac x="id_moebius" in exI, simp) setup_lifting type_definition_p_isometry text \Action of an h-isometry on an h-point\ lift_definition p_isometry_pt :: "p_isometry \ p_point \ p_point" is "\ f p. f p" using unit_disc_fix_f_unit_disc by auto text \Action of an h-isometry on an h-line\ lift_definition p_isometry_line :: "p_isometry \ p_line \ p_line" is "\ f l. unit_disc_fix_f_circline f l" proof- fix f H assume "unit_disc_fix_f f" "is_poincare_line H" then obtain M where "unit_disc_fix M" and *: "f = moebius_pt M \ f = moebius_pt M \ conjugate" unfolding unit_disc_fix_f_def by auto show "is_poincare_line (unit_disc_fix_f_circline f H)" using * proof assume "f = moebius_pt M" thus ?thesis using \unit_disc_fix M\ \is_poincare_line H\ using unit_disc_fix_f_circline_direct[of M f H] by auto next assume "f = moebius_pt M \ conjugate" thus ?thesis using \unit_disc_fix M\ \is_poincare_line H\ using unit_disc_fix_f_circline_indirect[of M f H] by auto qed qed text \An example lemma about h-isometries.\ text \H-isometries preserve h-collinearity\ lemma p_collinear_p_isometry_pt [simp]: shows "p_collinear (p_isometry_pt M ` A) \ p_collinear A" proof- have *: "\ M A. ((\x. moebius_pt M (conjugate x)) ` A = moebius_pt M ` (conjugate ` A))" by auto show ?thesis by transfer (auto simp add: unit_disc_fix_f_def *) qed (* ------------------------------------------------------------------ *) subsection \H-distance and h-congruence\ (* ------------------------------------------------------------------ *) lift_definition p_dist :: "p_point \ p_point \ real" is poincare_distance done definition p_congruent :: "p_point \ p_point \ p_point \ p_point \ bool" where [simp]: "p_congruent u v u' v' \ p_dist u v = p_dist u' v'" lemma assumes "p_dist u v = p_dist u' v'" assumes "p_dist v w = p_dist v' w'" assumes "p_dist u w = p_dist u' w'" shows "\ f. p_isometry_pt f u = u' \ p_isometry_pt f v = v' \ p_isometry_pt f w = w'" using assms apply transfer using unit_disc_fix_f_congruent_triangles by auto text\We prove that unit disc equipped with Poincar\'e distance is a metric space, i.e. an instantiation of @{term metric_space} locale.\ instantiation p_point :: metric_space begin definition "dist_p_point = p_dist" -definition "(uniformity_p_point :: (p_point \ p_point) filter) = (INF e:{0<..}. principal {(x, y). dist_class.dist x y < e})" +definition "(uniformity_p_point :: (p_point \ p_point) filter) = (INF e\{0<..}. principal {(x, y). dist_class.dist x y < e})" definition "open_p_point (U :: p_point set) = (\ x \ U. eventually (\(x', y). x' = x \ y \ U) uniformity)" instance proof fix x y :: p_point show "(dist_class.dist x y = 0) = (x = y)" unfolding dist_p_point_def by (transfer, simp add: poincare_distance_eq_0_iff) next fix x y z :: p_point show "dist_class.dist x y \ dist_class.dist x z + dist_class.dist y z" unfolding dist_p_point_def apply transfer using poincare_distance_triangle_inequality poincare_distance_sym by metis qed (simp_all add: open_p_point_def uniformity_p_point_def) end (* ------------------------------------------------------------------ *) subsection \H-betweennes\ (* ------------------------------------------------------------------ *) lift_definition p_between :: "p_point \ p_point \ p_point \ bool" is poincare_between done end diff --git a/thys/Poincare_Disc/Poincare_Between.thy b/thys/Poincare_Disc/Poincare_Between.thy --- a/thys/Poincare_Disc/Poincare_Between.thy +++ b/thys/Poincare_Disc/Poincare_Between.thy @@ -1,1263 +1,1262 @@ theory Poincare_Between imports Poincare_Distance begin (* ------------------------------------------------------------------ *) section\H-betweenness in the Poincar\'e model\ (* ------------------------------------------------------------------ *) subsection \H-betwenness expressed by a cross-ratio\ text\The point $v$ is h-between $u$ and $w$ if the cross-ratio between the pairs $u$ and $w$ and $v$ and inverse of $v$ is real and negative.\ definition poincare_between :: "complex_homo \ complex_homo \ complex_homo \ bool" where "poincare_between u v w \ u = v \ v = w \ (let cr = cross_ratio u v w (inversion v) in is_real (to_complex cr) \ Re (to_complex cr) < 0)" subsubsection \H-betwenness is preserved by h-isometries\ text \Since they preserve cross-ratio and inversion, h-isometries (unit disc preserving Möbius transformations and conjugation) preserve h-betweeness.\ lemma unit_disc_fix_moebius_preserve_poincare_between [simp]: assumes "unit_disc_fix M" and "u \ unit_disc" and "v \ unit_disc" and "w \ unit_disc" shows "poincare_between (moebius_pt M u) (moebius_pt M v) (moebius_pt M w) \ poincare_between u v w" proof (cases "u = v \ v = w") case True thus ?thesis using assms unfolding poincare_between_def by auto next case False moreover hence "moebius_pt M u \ moebius_pt M v \ moebius_pt M v \ moebius_pt M w" by auto moreover have "v \ inversion v" "w \ inversion v" using inversion_noteq_unit_disc[of v w] using inversion_noteq_unit_disc[of v v] using \v \ unit_disc\ \w \ unit_disc\ by auto ultimately show ?thesis using assms using unit_circle_fix_moebius_pt_inversion[of M v, symmetric] unfolding poincare_between_def by (simp del: unit_circle_fix_moebius_pt_inversion) qed lemma conjugate_preserve_poincare_between [simp]: assumes "u \ unit_disc" and "v \ unit_disc" and "w \ unit_disc" shows "poincare_between (conjugate u) (conjugate v) (conjugate w) \ poincare_between u v w" proof (cases "u = v \ v = w") case True thus ?thesis using assms unfolding poincare_between_def by auto next case False moreover hence "conjugate u \ conjugate v \ conjugate v \ conjugate w" using conjugate_inj by blast moreover have "v \ inversion v" "w \ inversion v" using inversion_noteq_unit_disc[of v w] using inversion_noteq_unit_disc[of v v] using \v \ unit_disc\ \w \ unit_disc\ by auto ultimately show ?thesis using assms using conjugate_cross_ratio[of v w "inversion v" u] unfolding poincare_between_def by (metis conjugate_id_iff conjugate_involution inversion_def inversion_sym o_apply) qed subsubsection \Some elementary properties of h-betwenness\ lemma poincare_between_nonstrict [simp]: shows "poincare_between u u v" and "poincare_between u v v" by (simp_all add: poincare_between_def) lemma poincare_between_sandwich: assumes "u \ unit_disc" and "v \ unit_disc" assumes "poincare_between u v u" shows "u = v" proof (rule ccontr) assume "\ ?thesis" thus False using assms using inversion_noteq_unit_disc[of v u] using cross_ratio_1[of v u "inversion v"] unfolding poincare_between_def Let_def by auto qed lemma poincare_between_rev: assumes "u \ unit_disc" and "v \ unit_disc" and "w \ unit_disc" shows "poincare_between u v w \ poincare_between w v u" using assms using inversion_noteq_unit_disc[of v w] using inversion_noteq_unit_disc[of v u] using cross_ratio_commute_13[of u v w "inversion v"] using cross_ratio_not_inf[of w "inversion v" v u] using cross_ratio_not_zero[of w v u "inversion v"] using inf_or_of_complex[of "cross_ratio w v u (inversion v)"] unfolding poincare_between_def by (auto simp add: Let_def Im_complex_div_eq_0 Re_divide divide_less_0_iff) subsubsection \H-betwenness and h-collinearity\ text\Three points can be in an h-between relation only when they are h-collinear.\ lemma poincare_between_poincare_collinear [simp]: assumes in_disc: "u \ unit_disc" "v \ unit_disc" "w \ unit_disc" assumes betw: "poincare_between u v w" shows "poincare_collinear {u, v, w}" proof (cases "u = v \ v = w") case True thus ?thesis using assms by auto next case False hence distinct: "distinct [u, v, w, inversion v]" using in_disc inversion_noteq_unit_disc[of v v] inversion_noteq_unit_disc[of v u] inversion_noteq_unit_disc[of v w] using betw poincare_between_sandwich[of w v] by (auto simp add: poincare_between_def Let_def) then obtain H where *: "{u, v, w, inversion v} \ circline_set H" using assms unfolding poincare_between_def using four_points_on_circline_iff_cross_ratio_real[of u v w "inversion v"] by auto hence "H = poincare_line u v" using assms distinct using unique_circline_set[of u v "inversion v"] using poincare_line[of u v] poincare_line_inversion[of u v] unfolding circline_set_def by auto thus ?thesis using * assms False unfolding poincare_collinear_def by (rule_tac x="poincare_line u v" in exI) simp qed lemma poincare_between_poincare_line_uvz: assumes "u \ v" and "u \ unit_disc" and "v \ unit_disc" and "z \ unit_disc" and "poincare_between u v z" shows "z \ circline_set (poincare_line u v)" using assms using poincare_between_poincare_collinear[of u v z] using unique_poincare_line[OF assms(1-3)] unfolding poincare_collinear_def by auto lemma poincare_between_poincare_line_uzv: assumes "u \ v" and "u \ unit_disc" and "v \ unit_disc" and "z \ unit_disc" "poincare_between u z v" shows "z \ circline_set (poincare_line u v)" using assms using poincare_between_poincare_collinear[of u z v] using unique_poincare_line[OF assms(1-3)] unfolding poincare_collinear_def by auto subsubsection \H-betweeness on Euclidean segments\ text\If the three points lie on an h-line that is a Euclidean line (e.g., if it contains zero), h-betweenness can be characterized much simpler than in the definition.\ lemma poincare_between_x_axis_u0v: assumes "is_real u'" and "u' \ 0" and "v' \ 0" shows "poincare_between (of_complex u') 0\<^sub>h (of_complex v') \ is_real v' \ Re u' * Re v' < 0" proof- have "Re u' \ 0" using \is_real u'\ \u' \ 0\ using complex_eq_if_Re_eq by auto have nz: "of_complex u' \ 0\<^sub>h" "of_complex v' \ 0\<^sub>h" by (simp_all add: \u' \ 0\ \v' \ 0\) hence "0\<^sub>h \ of_complex v'" by metis let ?cr = "cross_ratio (of_complex u') 0\<^sub>h (of_complex v') \\<^sub>h" have "is_real (to_complex ?cr) \ Re (to_complex ?cr) < 0 \ is_real v' \ Re u' * Re v' < 0" using cross_ratio_0inf[of v' u'] \v' \ 0\ \u' \ 0\ \is_real u'\ by (metis Re_complex_div_lt_0 Re_mult_real complex_cnj_divide divide_cancel_left eq_cnj_iff_real to_complex_of_complex) thus ?thesis unfolding poincare_between_def inversion_zero using \of_complex u' \ 0\<^sub>h\ \0\<^sub>h \ of_complex v'\ by simp qed lemma poincare_between_u0v: assumes "u \ unit_disc" and "v \ unit_disc" and "u \ 0\<^sub>h" and "v \ 0\<^sub>h" shows "poincare_between u 0\<^sub>h v \ (\ k < 0. to_complex u = cor k * to_complex v)" (is "?P u v") proof (cases "u = v") case True thus ?thesis using assms using inf_or_of_complex[of v] using poincare_between_sandwich[of u "0\<^sub>h"] by auto next case False have "\ u. u \ unit_disc \ u \ 0\<^sub>h \ ?P u v" (is "?P' v") proof (rule wlog_rotation_to_positive_x_axis) fix \ v let ?M = "moebius_pt (moebius_rotation \)" assume 1: "v \ unit_disc" "v \ 0\<^sub>h" assume 2: "?P' (?M v)" show "?P' v" proof (rule allI, rule impI, (erule conjE)+) fix u assume 3: "u \ unit_disc" "u \ 0\<^sub>h" have "poincare_between (?M u) 0\<^sub>h (?M v) \ poincare_between u 0\<^sub>h v" using \u \ unit_disc\ \v \ unit_disc\ using unit_disc_fix_moebius_preserve_poincare_between unit_disc_fix_rotation zero_in_unit_disc by fastforce thus "?P u v" using 1 2[rule_format, of "?M u"] 3 using inf_or_of_complex[of u] inf_or_of_complex[of v] by auto qed next fix x assume 1: "is_real x" "0 < Re x" "Re x < 1" hence "x \ 0" by auto show "?P' (of_complex x)" proof (rule allI, rule impI, (erule conjE)+) fix u assume 2: "u \ unit_disc" "u \ 0\<^sub>h" then obtain u' where "u = of_complex u'" using inf_or_of_complex[of u] by auto show "?P u (of_complex x)" using 1 2 \x \ 0\ \u = of_complex u'\ using poincare_between_rev[of u "0\<^sub>h" "of_complex x"] using poincare_between_x_axis_u0v[of x u'] \is_real x\ apply (auto simp add: cmod_eq_Re) - apply (rule_tac x="Re u' / Re x" in exI, simp add: divide_neg_pos sign_simps) + apply (rule_tac x="Re u' / Re x" in exI, simp add: divide_neg_pos algebra_split_simps) using mult_neg_pos mult_pos_neg by blast qed qed fact+ thus ?thesis using assms by auto qed lemma poincare_between_u0v_polar_form: assumes "x \ unit_disc" and "y \ unit_disc" and "x \ 0\<^sub>h" and "y \ 0\<^sub>h" and "to_complex x = cor rx * cis \" "to_complex y = cor ry * cis \" shows "poincare_between x 0\<^sub>h y \ rx * ry < 0" (is "?P x y rx ry") proof- from assms have "rx \ 0" "ry \ 0" using inf_or_of_complex[of x] inf_or_of_complex[of y] by auto have "(\k<0. cor rx = cor k * cor ry ) = (rx * ry < 0)" proof assume "\k<0. cor rx = cor k * cor ry" then obtain k where "k < 0" "cor rx = cor k * cor ry" by auto hence "rx = k * ry" using of_real_eq_iff by fastforce thus "rx * ry < 0" using \k < 0\ \rx \ 0\ \ry \ 0\ by (smt divisors_zero mult_nonneg_nonpos mult_nonpos_nonpos zero_less_mult_pos2) next assume "rx * ry < 0" hence "rx = (rx/ry)*ry" "rx / ry < 0" using \rx \ 0\ \ry \ 0\ - by (auto simp add: divide_less_0_iff sign_simps) + by (auto simp add: divide_less_0_iff algebra_split_simps) thus "\k<0. cor rx = cor k * cor ry" using \rx \ 0\ \ry \ 0\ by (rule_tac x="rx / ry" in exI, simp) qed thus ?thesis using assms using poincare_between_u0v[OF assms(1-4)] by auto qed lemma poincare_between_x_axis_0uv: fixes x y :: real assumes "-1 < x" and "x < 1" and "x \ 0" assumes "-1 < y" and "y < 1" and "y \ 0" shows "poincare_between 0\<^sub>h (of_complex x) (of_complex y) \ (x < 0 \ y < 0 \ y \ x) \ (x > 0 \ y > 0 \ x \ y)" (is "?lhs \ ?rhs") proof (cases "x = y") case True thus ?thesis using assms unfolding poincare_between_def by auto next case False let ?x = "of_complex x" and ?y = "of_complex y" have "?x \ unit_disc" "?y \ unit_disc" using assms by auto have distinct: "distinct [0\<^sub>h, ?x, ?y, inversion ?x]" using \x \ 0\ \y \ 0\ \x \ y\ \?x \ unit_disc\ \?y \ unit_disc\ using inversion_noteq_unit_disc[of ?x ?y] using inversion_noteq_unit_disc[of ?x ?x] using inversion_noteq_unit_disc[of ?x "0\<^sub>h"] using of_complex_inj[of x y] by (metis distinct_length_2_or_more distinct_singleton of_complex_zero_iff of_real_eq_0_iff of_real_eq_iff zero_in_unit_disc) let ?cr = "cross_ratio 0\<^sub>h ?x ?y (inversion ?x)" have "Re (to_complex ?cr) = x\<^sup>2 * (x*y - 1) / (x * (y - x))" using \x \ 0\ \x \ y\ unfolding inversion_def by simp (transfer, transfer, auto simp add: vec_cnj_def power2_eq_square field_simps split: if_split_asm) moreover { fix a b :: real assume "b \ 0" hence "a < 0 \ b\<^sup>2 * a < (0::real)" by (metis mult.commute mult_eq_0_iff mult_neg_pos mult_pos_pos not_less_iff_gr_or_eq not_real_square_gt_zero power2_eq_square) } hence "x\<^sup>2 * (x*y - 1) < 0" using assms by (smt minus_mult_minus mult_le_cancel_left1) moreover have "x * (y - x) > 0 \ ?rhs" using \x \ 0\ \y \ 0\ \x \ y\ by (smt mult_le_0_iff) ultimately have *: "Re (to_complex ?cr) < 0 \ ?rhs" by (simp add: divide_less_0_iff) show ?thesis proof assume ?lhs have "is_real (to_complex ?cr)" "Re (to_complex ?cr) < 0" using \?lhs\ distinct unfolding poincare_between_def Let_def by auto thus ?rhs using * by simp next assume ?rhs hence "Re (to_complex ?cr) < 0" using * by simp moreover have "{0\<^sub>h, of_complex (cor x), of_complex (cor y), inversion (of_complex (cor x))} \ circline_set x_axis" using \x \ 0\ is_real_inversion[of "cor x"] using inf_or_of_complex[of "inversion ?x"] by (auto simp del: inversion_of_complex) hence "is_real (to_complex ?cr)" using four_points_on_circline_iff_cross_ratio_real[OF distinct] by auto ultimately show ?lhs using distinct unfolding poincare_between_def Let_def by auto qed qed lemma poincare_between_0uv: assumes "u \ unit_disc" and "v \ unit_disc" and "u \ 0\<^sub>h" and "v \ 0\<^sub>h" shows "poincare_between 0\<^sub>h u v \ (let u' = to_complex u; v' = to_complex v in arg u' = arg v' \ cmod u' \ cmod v')" (is "?P u v") proof (cases "u = v") case True thus ?thesis by simp next case False have "\ v. v \ unit_disc \ v \ 0\<^sub>h \ v \ u \ (poincare_between 0\<^sub>h u v \ (let u' = to_complex u; v' = to_complex v in arg u' = arg v' \ cmod u' \ cmod v'))" (is "?P' u") proof (rule wlog_rotation_to_positive_x_axis) show "u \ unit_disc" "u \ 0\<^sub>h" by fact+ next fix x assume *: "is_real x" "0 < Re x" "Re x < 1" hence "of_complex x \ unit_disc" "of_complex x \ 0\<^sub>h" "of_complex x \ circline_set x_axis" unfolding circline_set_x_axis by (auto simp add: cmod_eq_Re) show "?P' (of_complex x)" proof safe fix v assume "v \ unit_disc" "v \ 0\<^sub>h" "v \ of_complex x" "poincare_between 0\<^sub>h (of_complex x) v" hence "v \ circline_set x_axis" using poincare_between_poincare_line_uvz[of "0\<^sub>h" "of_complex x" v] using poincare_line_0_real_is_x_axis[of "of_complex x"] using \of_complex x \ 0\<^sub>h\ \v \ 0\<^sub>h\ \v \ of_complex x\ \of_complex x \ unit_disc\ \of_complex x \ circline_set x_axis\ by auto obtain v' where "v = of_complex v'" using \v \ unit_disc\ using inf_or_of_complex[of v] by auto hence **: "v = of_complex v'" "-1 < Re v'" "Re v' < 1" "Re v' \ 0" "is_real v'" using \v \ unit_disc\ \v \ 0\<^sub>h\ \v \ circline_set x_axis\ of_complex_inj[of v'] unfolding circline_set_x_axis by (auto simp add: cmod_eq_Re real_imag_0) show "let u' = to_complex (of_complex x); v' = to_complex v in arg u' = arg v' \ cmod u' \ cmod v'" using poincare_between_x_axis_0uv[of "Re x" "Re v'"] * ** using \poincare_between 0\<^sub>h (of_complex x) v\ using arg_complex_of_real_positive[of "Re x"] arg_complex_of_real_negative[of "Re x"] using arg_complex_of_real_positive[of "Re v'"] arg_complex_of_real_negative[of "Re v'"] by (auto simp add: cmod_eq_Re) next fix v assume "v \ unit_disc" "v \ 0\<^sub>h" "v \ of_complex x" then obtain v' where **: "v = of_complex v'" "v' \ 0" "v' \ x" using inf_or_of_complex[of v] by auto blast assume "let u' = to_complex (of_complex x); v' = to_complex v in arg u' = arg v' \ cmod u' \ cmod v'" hence ***: "Re x < 0 \ Re v' < 0 \ Re v' \ Re x \ 0 < Re x \ 0 < Re v' \ Re x \ Re v'" "is_real v'" using arg_pi_iff[of x] arg_pi_iff[of v'] using arg_0_iff[of x] arg_0_iff[of v'] using * ** by (smt cmod_Re_le_iff to_complex_of_complex)+ have "-1 < Re v'" "Re v' < 1" "Re v' \ 0" "is_real v'" using \v \ unit_disc\ ** \is_real v'\ by (auto simp add: cmod_eq_Re complex_eq_if_Re_eq) thus "poincare_between 0\<^sub>h (of_complex x) v" using poincare_between_x_axis_0uv[of "Re x" "Re v'"] * ** *** by simp qed next fix \ u assume "u \ unit_disc" "u \ 0\<^sub>h" let ?M = "moebius_rotation \" assume *: "?P' (moebius_pt ?M u)" show "?P' u" proof (rule allI, rule impI, (erule conjE)+) fix v assume "v \ unit_disc" "v \ 0\<^sub>h" "v \ u" have "moebius_pt ?M v \ moebius_pt ?M u" using \v \ u\ by auto obtain u' v' where "v = of_complex v'" "u = of_complex u'" "v' \ 0" "u' \ 0" using inf_or_of_complex[of u] inf_or_of_complex[of v] using \v \ unit_disc\ \u \ unit_disc\ \v \ 0\<^sub>h\ \u \ 0\<^sub>h\ by auto thus "?P u v" using *[rule_format, of "moebius_pt ?M v"] using \moebius_pt ?M v \ moebius_pt ?M u\ using unit_disc_fix_moebius_preserve_poincare_between[of ?M "0\<^sub>h" u v] using \v \ unit_disc\ \u \ unit_disc\ \v \ 0\<^sub>h\ \u \ 0\<^sub>h\ using arg_mult_eq[of "cis \" u' v'] by simp (auto simp add: arg_mult) qed qed thus ?thesis using assms False by auto qed lemma poincare_between_y_axis_0uv: fixes x y :: real assumes "-1 < x" and "x < 1" and "x \ 0" assumes "-1 < y" and "y < 1" and "y \ 0" shows "poincare_between 0\<^sub>h (of_complex (\ * x)) (of_complex (\ * y)) \ (x < 0 \ y < 0 \ y \ x) \ (x > 0 \ y > 0 \ x \ y)" (is "?lhs \ ?rhs") using assms using poincare_between_0uv[of "of_complex (\ * x)" "of_complex (\ * y)"] using arg_pi2_iff[of "\ * cor x"] arg_pi2_iff[of "\ * cor y"] using arg_minus_pi2_iff[of "\ * cor x"] arg_minus_pi2_iff[of "\ * cor y"] apply simp apply (cases "x > 0") apply (cases "y > 0", simp, simp) apply (cases "y > 0") apply simp using pi_gt_zero apply linarith apply simp done lemma poincare_between_x_axis_uvw: fixes x y z :: real assumes "-1 < x" and "x < 1" assumes "-1 < y" and "y < 1" and "y \ x" assumes "-1 < z" and "z < 1" and "z \ x" shows "poincare_between (of_complex x) (of_complex y) (of_complex z) \ (y < x \ z < x \ z \ y) \ (y > x \ z > x \ y \ z)" (is "?lhs \ ?rhs") proof (cases "x = 0 \ y = 0 \ z = 0") case True thus ?thesis proof (cases "x = 0") case True thus ?thesis using poincare_between_x_axis_0uv assms by simp next case False show ?thesis proof (cases "z = 0") case True thus ?thesis using poincare_between_x_axis_0uv assms poincare_between_rev by (smt norm_of_real of_complex_zero of_real_0 poincare_between_nonstrict(2) unit_disc_iff_cmod_lt_1) next case False have "y = 0" using `x \ 0` `z \ 0` `x = 0 \ y = 0 \ z = 0` by simp have "poincare_between (of_complex x) 0\<^sub>h (of_complex z) = (is_real z \ x * z < 0)" using `x \ 0` `z \ 0` poincare_between_x_axis_u0v by auto moreover have "x * z < 0 \ ?rhs" using True \x \ 0\ \z \ 0\ by (smt zero_le_mult_iff) ultimately show ?thesis using `y = 0` by auto qed qed next case False thus ?thesis proof (cases "z = y") case True thus ?thesis using assms unfolding poincare_between_def by auto next case False let ?x = "of_complex x" and ?y = "of_complex y" and ?z = "of_complex z" have "?x \ unit_disc" "?y \ unit_disc" "?z \ unit_disc" using assms by auto have distinct: "distinct [?x, ?y, ?z, inversion ?y]" using \y \ x\ \z \ x\ False \?x \ unit_disc\ \?y \ unit_disc\ \?z \ unit_disc\ using inversion_noteq_unit_disc[of ?y ?y] using inversion_noteq_unit_disc[of ?y ?x] using inversion_noteq_unit_disc[of ?y ?z] using of_complex_inj[of x y] of_complex_inj[of y z] of_complex_inj[of x z] by auto have "cor y * cor x \ 1" using assms by (smt minus_mult_minus mult_less_cancel_left2 mult_less_cancel_right2 of_real_1 of_real_eq_iff of_real_mult) let ?cr = "cross_ratio ?x ?y ?z (inversion ?y)" have "Re (to_complex ?cr) = (x - y) * (z*y - 1)/ ((x*y - 1)*(z - y))" proof- have " \y x z. \y \ x; z \ x; z \ y; cor y * cor x \ 1; x \ 0; y \ 0; z \ 0\ \ (y * y + y * (y * (x * z)) - (y * x + y * (y * (y * z)))) / (y * y + y * (y * (x * z)) - (y * z + y * (y * (y * x)))) = (y + y * (x * z) - (x + y * (y * z))) / (y + y * (x * z) - (z + y * (y * x)))" by (metis (no_types, hide_lams) ab_group_add_class.ab_diff_conv_add_uminus distrib_left mult_divide_mult_cancel_left_if mult_minus_right) thus ?thesis using \y \ x\ \z \ x\ False \\ (x = 0 \ y = 0 \ z = 0)\ using \cor y * cor x \ 1\ unfolding inversion_def by (transfer, transfer, auto simp add: vec_cnj_def power2_eq_square field_simps split: if_split_asm) qed moreover have "(x*y - 1) < 0" using assms by (smt minus_mult_minus mult_less_cancel_right2 zero_less_mult_iff) moreover have "(z*y - 1) < 0" using assms by (smt minus_mult_minus mult_less_cancel_right2 zero_less_mult_iff) moreover have "(x - y) / (z - y) < 0 \ ?rhs" using \y \ x\ \z \ x\ False \\ (x = 0 \ y = 0 \ z = 0)\ by (smt divide_less_cancel divide_nonneg_nonpos divide_nonneg_pos divide_nonpos_nonneg divide_nonpos_nonpos) ultimately have *: "Re (to_complex ?cr) < 0 \ ?rhs" - by (smt linordered_field_class.sign_simps(45) minus_divide_left zero_less_divide_iff zero_less_mult_iff) - + by (smt algebra_split_simps(24) minus_divide_left zero_less_divide_iff zero_less_mult_iff) show ?thesis proof assume ?lhs have "is_real (to_complex ?cr)" "Re (to_complex ?cr) < 0" using \?lhs\ distinct unfolding poincare_between_def Let_def by auto thus ?rhs using * by simp next assume ?rhs hence "Re (to_complex ?cr) < 0" using * by simp moreover have "{of_complex (cor x), of_complex (cor y), of_complex (cor z), inversion (of_complex (cor y))} \ circline_set x_axis" using \\ (x = 0 \ y = 0 \ z = 0)\ is_real_inversion[of "cor y"] using inf_or_of_complex[of "inversion ?y"] by (auto simp del: inversion_of_complex) hence "is_real (to_complex ?cr)" using four_points_on_circline_iff_cross_ratio_real[OF distinct] by auto ultimately show ?lhs using distinct unfolding poincare_between_def Let_def by auto qed qed qed subsubsection \H-betweenness and h-collinearity\ text\For three h-collinear points at least one of the three possible h-betweeness relations must hold.\ lemma poincare_collinear3_between: assumes "u \ unit_disc" and "v \ unit_disc" and "w \ unit_disc" assumes "poincare_collinear {u, v, w}" shows "poincare_between u v w \ poincare_between u w v \ poincare_between v u w" (is "?P' u v w") proof (cases "u=v") case True thus ?thesis using assms by auto next case False have "\ w. w \ unit_disc \ poincare_collinear {u, v, w} \ ?P' u v w" (is "?P u v") proof (rule wlog_positive_x_axis[where P="?P"]) fix x assume x: "is_real x" "0 < Re x" "Re x < 1" hence "x \ 0" using complex.expand[of x 0] by auto hence *: "poincare_line 0\<^sub>h (of_complex x) = x_axis" using x poincare_line_0_real_is_x_axis[of "of_complex x"] unfolding circline_set_x_axis by auto have "of_complex x \ unit_disc" using x by (auto simp add: cmod_eq_Re) have "of_complex x \ 0\<^sub>h" using \x \ 0\ by auto show "?P 0\<^sub>h (of_complex x)" proof safe fix w assume "w \ unit_disc" assume "poincare_collinear {0\<^sub>h, of_complex x, w}" hence "w \ circline_set x_axis" using * unique_poincare_line[of "0\<^sub>h" "of_complex x"] \of_complex x \ unit_disc\ \x \ 0\ \of_complex x \ 0\<^sub>h\ unfolding poincare_collinear_def by auto then obtain w' where w': "w = of_complex w'" "is_real w'" using \w \ unit_disc\ using inf_or_of_complex[of w] unfolding circline_set_x_axis by auto hence "-1 < Re w'" "Re w' < 1" using \w \ unit_disc\ by (auto simp add: cmod_eq_Re) assume 1: "\ poincare_between (of_complex x) 0\<^sub>h w" hence "w \ 0\<^sub>h" "w' \ 0" using w' unfolding poincare_between_def by auto hence "Re w' \ 0" using w' complex.expand[of w' 0] by auto have "Re w' \ 0" using 1 poincare_between_x_axis_u0v[of x w'] \Re x > 0\ \is_real x\ \x \ 0\ \w' \ 0\ w' using mult_pos_neg by force moreover assume "\ poincare_between 0\<^sub>h (of_complex x) w" hence "Re w' < Re x" using poincare_between_x_axis_0uv[of "Re x" "Re w'"] using w' x \-1 < Re w'\ \Re w' < 1\ \Re w' \ 0\ by auto ultimately show "poincare_between 0\<^sub>h w (of_complex x)" using poincare_between_x_axis_0uv[of "Re w'" "Re x"] using w' x \-1 < Re w'\ \Re w' < 1\ \Re w' \ 0\ by auto qed next show "u \ unit_disc" "v \ unit_disc" "u \ v" by fact+ next fix M u v assume 1: "unit_disc_fix M" "u \ unit_disc" "v \ unit_disc" "u \ v" let ?Mu = "moebius_pt M u" and ?Mv = "moebius_pt M v" assume 2: "?P ?Mu ?Mv" show "?P u v" proof safe fix w assume "w \ unit_disc" "poincare_collinear {u, v, w}" "\ poincare_between u v w" "\ poincare_between v u w" thus "poincare_between u w v" using 1 2[rule_format, of "moebius_pt M w"] by simp qed qed thus ?thesis using assms by simp qed lemma poincare_collinear3_iff: assumes "u \ unit_disc" "v \ unit_disc" "w \ unit_disc" shows "poincare_collinear {u, v, w} \ poincare_between u v w \ poincare_between v u w \ poincare_between v w u" using assms by (metis poincare_collinear3_between insert_commute poincare_between_poincare_collinear poincare_between_rev) subsection \Some properties of betweenness\ lemma poincare_between_transitivity: assumes "a \ unit_disc" and "x \ unit_disc" and "b \ unit_disc" and "y \ unit_disc" and "poincare_between a x b" and "poincare_between a b y" shows "poincare_between x b y" proof(cases "a = b") case True thus ?thesis using assms using poincare_between_sandwich by blast next case False have "\ x. \ y. poincare_between a x b \ poincare_between a b y \ x \ unit_disc \ y \ unit_disc \ poincare_between x b y" (is "?P a b") proof (rule wlog_positive_x_axis[where P="?P"]) show "a \ unit_disc" using assms by simp next show "b \ unit_disc" using assms by simp next show "a \ b" using False by simp next fix M u v assume *: "unit_disc_fix M" "u \ unit_disc" "v \ unit_disc" "u \ v" "\x y. poincare_between (moebius_pt M u) x (moebius_pt M v) \ poincare_between (moebius_pt M u) (moebius_pt M v) y \ x \ unit_disc \ y \ unit_disc \ poincare_between x (moebius_pt M v) y" show "\x y. poincare_between u x v \ poincare_between u v y \ x \ unit_disc \ y \ unit_disc \ poincare_between x v y" proof safe fix x y assume "poincare_between u x v" "poincare_between u v y" " x \ unit_disc" "y \ unit_disc" have "poincare_between (moebius_pt M u) (moebius_pt M x) (moebius_pt M v)" using \poincare_between u x v\ \unit_disc_fix M\ \x \ unit_disc\ \u \ unit_disc\ \v \ unit_disc\ by simp moreover have "poincare_between (moebius_pt M u) (moebius_pt M v) (moebius_pt M y)" using \poincare_between u v y\ \unit_disc_fix M\ \y \ unit_disc\ \u \ unit_disc\ \v \ unit_disc\ by simp moreover have "(moebius_pt M x) \ unit_disc" using \unit_disc_fix M\ \x \ unit_disc\ by simp moreover have "(moebius_pt M y) \ unit_disc" using \unit_disc_fix M\ \y \ unit_disc\ by simp ultimately have "poincare_between (moebius_pt M x) (moebius_pt M v) (moebius_pt M y)" using * by blast thus "poincare_between x v y" using \y \ unit_disc\ * \x \ unit_disc\ by simp qed next fix x assume xx: "is_real x" "0 < Re x" "Re x < 1" hence "of_complex x \ unit_disc" using cmod_eq_Re by auto hence "of_complex x \ \\<^sub>h" by simp have " of_complex x \ 0\<^sub>h" using xx by auto have "of_complex x \ circline_set x_axis" using xx by simp show "\m n. poincare_between 0\<^sub>h m (of_complex x) \ poincare_between 0\<^sub>h (of_complex x) n \ m \ unit_disc \ n \ unit_disc \ poincare_between m (of_complex x) n" proof safe fix m n assume **: "poincare_between 0\<^sub>h m (of_complex x)" "poincare_between 0\<^sub>h (of_complex x) n" "m \ unit_disc" " n \ unit_disc" show "poincare_between m (of_complex x) n" proof(cases "m = 0\<^sub>h") case True thus ?thesis using ** by auto next case False hence "m \ circline_set x_axis" using poincare_between_poincare_line_uzv[of "0\<^sub>h" "of_complex x" m] using poincare_line_0_real_is_x_axis[of "of_complex x"] using \of_complex x \ unit_disc\ \of_complex x \ \\<^sub>h\ \of_complex x \ 0\<^sub>h\ using \of_complex x \ circline_set x_axis\ \m \ unit_disc\ **(1) by simp then obtain m' where "m = of_complex m'" "is_real m'" using inf_or_of_complex[of m] \m \ unit_disc\ unfolding circline_set_x_axis by auto hence "Re m' \ Re x" using \poincare_between 0\<^sub>h m (of_complex x)\ xx \of_complex x \ 0\<^sub>h\ using False ** \of_complex x \ unit_disc\ using cmod_Re_le_iff poincare_between_0uv by auto have "n \ 0\<^sub>h" using **(2, 4) \of_complex x \ 0\<^sub>h\ \of_complex x \ unit_disc\ using poincare_between_sandwich by fastforce have "n \ circline_set x_axis" using poincare_between_poincare_line_uvz[of "0\<^sub>h" "of_complex x" n] using poincare_line_0_real_is_x_axis[of "of_complex x"] using \of_complex x \ unit_disc\ \of_complex x \ \\<^sub>h\ \of_complex x \ 0\<^sub>h\ using \of_complex x \ circline_set x_axis\ \n \ unit_disc\ **(2) by simp then obtain n' where "n = of_complex n'" "is_real n'" using inf_or_of_complex[of n] \n \ unit_disc\ unfolding circline_set_x_axis by auto hence "Re x \ Re n'" using \poincare_between 0\<^sub>h (of_complex x) n\ xx \of_complex x \ 0\<^sub>h\ using False ** \of_complex x \ unit_disc\ \n \ 0\<^sub>h\ using cmod_Re_le_iff poincare_between_0uv by (metis Re_complex_of_real arg_0_iff rcis_cmod_arg rcis_zero_arg to_complex_of_complex) have "poincare_between (of_complex m') (of_complex x) (of_complex n')" using \Re x \ Re n'\ \Re m' \ Re x\ using poincare_between_x_axis_uvw[of "Re m'" "Re x" "Re n'"] using \is_real n'\ \is_real m'\ \n \ unit_disc\ \n = of_complex n'\ using xx \m = of_complex m'\ \m \ unit_disc\ by (smt complex_of_real_Re norm_of_real poincare_between_def unit_disc_iff_cmod_lt_1) thus ?thesis using \n = of_complex n'\ \m = of_complex m'\ by auto qed qed qed thus ?thesis using assms by blast qed (* ------------------------------------------------------------------ *) subsection\Poincare between - sum distances\ (* ------------------------------------------------------------------ *) text\Another possible definition of the h-betweenness relation is given in terms of h-distances between pairs of points. We prove it as a characterization equivalent to our cross-ratio based definition.\ lemma poincare_between_sum_distances_x_axis_u0v: assumes "of_complex u' \ unit_disc" "of_complex v' \ unit_disc" assumes "is_real u'" "u' \ 0" "v' \ 0" shows "poincare_distance (of_complex u') 0\<^sub>h + poincare_distance 0\<^sub>h (of_complex v') = poincare_distance (of_complex u') (of_complex v') \ is_real v' \ Re u' * Re v' < 0" (is "?P u' v' \ ?Q u' v'") proof- have "Re u' \ 0" using \is_real u'\ \u' \ 0\ using complex_eq_if_Re_eq by simp let ?u = "cmod u'" and ?v = "cmod v'" and ?uv = "cmod (u' - v')" have disc: "?u\<^sup>2 < 1" "?v\<^sup>2 < 1" using unit_disc_cmod_square_lt_1[OF assms(1)] using unit_disc_cmod_square_lt_1[OF assms(2)] by auto have "poincare_distance (of_complex u') 0\<^sub>h + poincare_distance 0\<^sub>h (of_complex v') = arcosh (((1 + ?u\<^sup>2) * (1 + ?v\<^sup>2) + 4 * ?u * ?v) / ((1 - ?u\<^sup>2) * (1 - ?v\<^sup>2)))" (is "_ = arcosh ?r1") using poincare_distance_formula_zero_sum[OF assms(1-2)] by (simp add: Let_def) moreover have "poincare_distance (of_complex u') (of_complex v') = arcosh (((1 - ?u\<^sup>2) * (1 - ?v\<^sup>2) + 2 * ?uv\<^sup>2) / ((1 - ?u\<^sup>2) * (1 - ?v\<^sup>2)))" (is "_ = arcosh ?r2") using disc using poincare_distance_formula[OF assms(1-2)] by (subst add_divide_distrib) simp moreover have "arcosh ?r1 = arcosh ?r2 \ ?Q u' v'" proof assume "arcosh ?r1 = arcosh ?r2" hence "?r1 = ?r2" proof (subst (asm) arcosh_eq_iff) show "?r1 \ 1" proof- have "(1 - ?u\<^sup>2) * (1 - ?v\<^sup>2) \ (1 + ?u\<^sup>2) * (1 + ?v\<^sup>2) + 4 * ?u * ?v" by (simp add: field_simps) thus ?thesis using disc by simp qed next show "?r2 \ 1" using disc by simp qed hence "(1 + ?u\<^sup>2) * (1 + ?v\<^sup>2) + 4 * ?u * ?v = (1 - ?u\<^sup>2) * (1 - ?v\<^sup>2) + 2 * ?uv\<^sup>2" using disc by auto hence "(cmod (u' - v'))\<^sup>2 = (cmod u' + cmod v')\<^sup>2" by (simp add: field_simps power2_eq_square) hence *: "Re u' * Re v' + \Re u'\ * sqrt ((Im v')\<^sup>2 + (Re v')\<^sup>2) = 0" using \is_real u'\ unfolding cmod_power2 cmod_def by (simp add: field_simps) (simp add: power2_eq_square field_simps) hence "sqrt ((Im v')\<^sup>2 + (Re v')\<^sup>2) = \Re v'\" using \Re u' \ 0\ \v' \ 0\ by (smt complex_neq_0 mult.commute mult_cancel_right mult_minus_left real_sqrt_gt_0_iff) hence "Im v' = 0" by (smt Im_eq_0 norm_complex_def) moreover hence "Re u' * Re v' = - \Re u'\ * \Re v'\" using * by simp hence "Re u' * Re v' < 0" using \Re u' \ 0\ \v' \ 0\ by (simp add: \is_real v'\ complex_eq_if_Re_eq) ultimately show "?Q u' v'" by simp next assume "?Q u' v'" hence "is_real v'" "Re u' * Re v' < 0" by auto have "?r1 = ?r2" proof (cases "Re u' > 0") case True hence "Re v' < 0" using \Re u' * Re v' < 0\ by (smt zero_le_mult_iff) show ?thesis using disc \is_real u'\ \is_real v'\ using \Re u' > 0\ \Re v' < 0\ unfolding cmod_power2 cmod_def by simp (simp add: power2_eq_square field_simps) next case False hence "Re u' < 0" using \Re u' \ 0\ by simp hence "Re v' > 0" using \Re u' * Re v' < 0\ by (smt zero_le_mult_iff) show ?thesis using disc \is_real u'\ \is_real v'\ using \Re u' < 0\ \Re v' > 0\ unfolding cmod_power2 cmod_def by simp (simp add: power2_eq_square field_simps) qed thus "arcosh ?r1 = arcosh ?r2" by metis qed ultimately show ?thesis by simp qed text\ Different proof of the previous theorem relying on the cross-ratio definition, and not the distance formula. We suppose that this could be also used to prove the triangle inequality. \ lemma poincare_between_sum_distances_x_axis_u0v_different_proof: assumes "of_complex u' \ unit_disc" "of_complex v' \ unit_disc" assumes "is_real u'" "u' \ 0" "v' \ 0" (* additional condition *) "is_real v'" shows "poincare_distance (of_complex u') 0\<^sub>h + poincare_distance 0\<^sub>h (of_complex v') = poincare_distance (of_complex u') (of_complex v') \ Re u' * Re v' < 0" (is "?P u' v' \ ?Q u' v'") proof- have "-1 < Re u'" "Re u' < 1" "Re u' \ 0" using assms by (auto simp add: cmod_eq_Re complex_eq_if_Re_eq) have "-1 < Re v'" "Re v' < 1" "Re v' \ 0" using assms by (auto simp add: cmod_eq_Re complex_eq_if_Re_eq) have "\ln (Re ((1 - u') / (1 + u')))\ + \ln (Re ((1 - v') / (1 + v')))\ = \ln (Re ((1 + u') * (1 - v') / ((1 - u') * (1 + v'))))\ \ Re u' * Re v' < 0" (is "\ln ?a1\ + \ln ?a2\ = \ln ?a3\ \ _") proof- have 1: "0 < ?a1" "ln ?a1 > 0 \ Re u' < 0" using \Re u' < 1\ \Re u' > -1\ \is_real u'\ using complex_is_Real_iff by auto have 2: "0 < ?a2" "ln ?a2 > 0 \ Re v' < 0" using \Re v' < 1\ \Re v' > -1\ \is_real v'\ using complex_is_Real_iff by auto have 3: "0 < ?a3" "ln ?a3 > 0 \ Re v' < Re u'" using \Re u' < 1\ \Re u' > -1\ \is_real u'\ using \Re v' < 1\ \Re v' > -1\ \is_real v'\ using complex_is_Real_iff by auto (simp add: field_simps)+ show ?thesis proof assume *: "Re u' * Re v' < 0" show "\ln ?a1\ + \ln ?a2\ = \ln ?a3\" proof (cases "Re u' > 0") case True hence "Re v' < 0" using * by (smt mult_nonneg_nonneg) show ?thesis using 1 2 3 \Re u' > 0\ \Re v' < 0\ using \Re u' < 1\ \Re u' > -1\ \is_real u'\ using \Re v' < 1\ \Re v' > -1\ \is_real v'\ using complex_is_Real_iff using ln_div ln_mult by simp next case False hence "Re v' > 0" "Re u' < 0" using * by (smt zero_le_mult_iff)+ show ?thesis using 1 2 3 \Re u' < 0\ \Re v' > 0\ using \Re u' < 1\ \Re u' > -1\ \is_real u'\ using \Re v' < 1\ \Re v' > -1\ \is_real v'\ using complex_is_Real_iff using ln_div ln_mult by simp qed next assume *: "\ln ?a1\ + \ln ?a2\ = \ln ?a3\" { assume "Re u' > 0" "Re v' > 0" hence False using * 1 2 3 using \Re u' < 1\ \Re u' > -1\ \is_real u'\ using \Re v' < 1\ \Re v' > -1\ \is_real v'\ using complex_is_Real_iff using ln_mult ln_div by (cases "Re v' < Re u'") auto } moreover { assume "Re u' < 0" "Re v' < 0" hence False using * 1 2 3 using \Re u' < 1\ \Re u' > -1\ \is_real u'\ using \Re v' < 1\ \Re v' > -1\ \is_real v'\ using complex_is_Real_iff using ln_mult ln_div by (cases "Re v' < Re u'") auto } ultimately show "Re u' * Re v' < 0" using \Re u' \ 0\ \Re v' \ 0\ by (smt divisors_zero mult_le_0_iff) qed qed thus ?thesis using assms apply (subst poincare_distance_sym, simp, simp) apply (subst poincare_distance_zero_x_axis, simp, simp add: circline_set_x_axis) apply (subst poincare_distance_zero_x_axis, simp, simp add: circline_set_x_axis) apply (subst poincare_distance_x_axis_x_axis, simp, simp, simp add: circline_set_x_axis, simp add: circline_set_x_axis) apply simp done qed lemma poincare_between_sum_distances: assumes "u \ unit_disc" and "v \ unit_disc" and "w \ unit_disc" shows "poincare_between u v w \ poincare_distance u v + poincare_distance v w = poincare_distance u w" (is "?P' u v w") proof (cases "u = v") case True thus ?thesis using assms by simp next case False have "\ w. w \ unit_disc \ (poincare_between u v w \ poincare_distance u v + poincare_distance v w = poincare_distance u w)" (is "?P u v") proof (rule wlog_positive_x_axis) fix x assume "is_real x" "0 < Re x" "Re x < 1" have "of_complex x \ circline_set x_axis" using \is_real x\ by (auto simp add: circline_set_x_axis) have "of_complex x \ unit_disc" using \is_real x\ \0 < Re x\ \Re x < 1\ by (simp add: cmod_eq_Re) have "x \ 0" using \is_real x\ \Re x > 0\ by auto show "?P (of_complex x) 0\<^sub>h" proof (rule allI, rule impI) fix w assume "w \ unit_disc" then obtain w' where "w = of_complex w'" using inf_or_of_complex[of w] by auto show "?P' (of_complex x) 0\<^sub>h w" proof (cases "w = 0\<^sub>h") case True thus ?thesis by simp next case False hence "w' \ 0" using \w = of_complex w'\ by auto show ?thesis using \is_real x\ \x \ 0\ \w = of_complex w'\ \w' \ 0\ using \of_complex x \ unit_disc\ \w \ unit_disc\ apply simp apply (subst poincare_between_x_axis_u0v, simp_all) apply (subst poincare_between_sum_distances_x_axis_u0v, simp_all) done qed qed next show "v \ unit_disc" "u \ unit_disc" using assms by auto next show "v \ u" using \u \ v\ by simp next fix M u v assume *: "unit_disc_fix M" "u \ unit_disc" "v \ unit_disc" "u \ v" and **: "?P (moebius_pt M v) (moebius_pt M u)" show "?P v u" proof (rule allI, rule impI) fix w assume "w \ unit_disc" hence "moebius_pt M w \ unit_disc" using \unit_disc_fix M\ by auto thus "?P' v u w" using \u \ unit_disc\ \v \ unit_disc\ \w \ unit_disc\ \unit_disc_fix M\ using **[rule_format, of "moebius_pt M w"] by auto qed qed thus ?thesis using assms by simp qed subsection \Some more properties of h-betweenness.\ text \Some lemmas proved earlier are proved almost directly using the sum of distances characterization.\ lemma unit_disc_fix_moebius_preserve_poincare_between': assumes "unit_disc_fix M" and "u \ unit_disc" and "v \ unit_disc" and "w \ unit_disc" shows "poincare_between (moebius_pt M u) (moebius_pt M v) (moebius_pt M w) \ poincare_between u v w" using assms using poincare_between_sum_distances by simp lemma conjugate_preserve_poincare_between': assumes "u \ unit_disc" "v \ unit_disc" "w \ unit_disc" shows "poincare_between (conjugate u) (conjugate v) (conjugate w) \ poincare_between u v w" using assms using poincare_between_sum_distances by simp text \There is a unique point on a ray on the given distance from the given starting point\ lemma unique_poincare_distance_on_ray: assumes "d \ 0" "u \ v" "u \ unit_disc" "v \ unit_disc" assumes "y \ unit_disc" "poincare_distance u y = d" "poincare_between u v y" assumes "z \ unit_disc" "poincare_distance u z = d" "poincare_between u v z" shows "y = z" proof- have "\ d y z. d \ 0 \ y \ unit_disc \ poincare_distance u y = d \ poincare_between u v y \ z \ unit_disc \ poincare_distance u z = d \ poincare_between u v z \ y = z" (is "?P u v") proof (rule wlog_positive_x_axis[where P="?P"]) fix x assume x: "is_real x" "0 < Re x" "Re x < 1" hence "x \ 0" using complex.expand[of x 0] by auto hence *: "poincare_line 0\<^sub>h (of_complex x) = x_axis" using x poincare_line_0_real_is_x_axis[of "of_complex x"] unfolding circline_set_x_axis by auto have "of_complex x \ unit_disc" using x by (auto simp add: cmod_eq_Re) have "arg x = 0" using x using arg_0_iff by blast show "?P 0\<^sub>h (of_complex x)" proof safe fix y z assume "y \ unit_disc" "z \ unit_disc" then obtain y' z' where yz: "y = of_complex y'" "z = of_complex z'" using inf_or_of_complex[of y] inf_or_of_complex[of z] by auto assume betw: "poincare_between 0\<^sub>h (of_complex x) y" "poincare_between 0\<^sub>h (of_complex x) z" hence "y \ 0\<^sub>h" "z \ 0\<^sub>h" using \x \ 0\ \of_complex x \ unit_disc\ \y \ unit_disc\ using poincare_between_sandwich[of "0\<^sub>h" "of_complex x"] using of_complex_zero_iff[of x] by force+ hence "arg y' = 0" "cmod y' \ cmod x" "arg z' = 0" "cmod z' \ cmod x" using poincare_between_0uv[of "of_complex x" y] poincare_between_0uv[of "of_complex x" z] using \of_complex x \ unit_disc\ \x \ 0\ \arg x = 0\ \y \ unit_disc\ \z \ unit_disc\ betw yz by (simp_all add: Let_def) hence *: "is_real y'" "is_real z'" "Re y' > 0" "Re z' > 0" using arg_0_iff[of y'] arg_0_iff[of z'] x \y \ 0\<^sub>h\ \z \ 0\<^sub>h\ yz by auto assume "poincare_distance 0\<^sub>h z = poincare_distance 0\<^sub>h y" "0 \ poincare_distance 0\<^sub>h y" thus "y = z" using * yz \y \ unit_disc\ \z \ unit_disc\ using unique_x_axis_poincare_distance_positive[of "poincare_distance 0\<^sub>h y"] by (auto simp add: cmod_eq_Re unit_disc_to_complex_inj) qed next show "u \ unit_disc" "v \ unit_disc" "u \ v" by fact+ next fix M u v assume *: "unit_disc_fix M" "u \ unit_disc" "v \ unit_disc" "u \ v" assume **: "?P (moebius_pt M u) (moebius_pt M v)" show "?P u v" proof safe fix d y z assume ***: "0 \ poincare_distance u y" "y \ unit_disc" "poincare_between u v y" "z \ unit_disc" "poincare_between u v z" "poincare_distance u z = poincare_distance u y" let ?Mu = "moebius_pt M u" and ?Mv = "moebius_pt M v" and ?My = "moebius_pt M y" and ?Mz = "moebius_pt M z" have "?Mu \ unit_disc" "?Mv \ unit_disc" "?My \ unit_disc" "?Mz \ unit_disc" using \u \ unit_disc\ \v \ unit_disc\ \y \ unit_disc\ \z \ unit_disc\ using \unit_disc_fix M\ by auto hence "?My = ?Mz" using * *** using **[rule_format, of "poincare_distance ?Mu ?My" ?My ?Mz] by simp thus "y = z" using bij_moebius_pt[of M] unfolding bij_def inj_on_def by blast qed qed thus ?thesis using assms by auto qed end \ No newline at end of file diff --git a/thys/Poincare_Disc/Poincare_Circles.thy b/thys/Poincare_Disc/Poincare_Circles.thy --- a/thys/Poincare_Disc/Poincare_Circles.thy +++ b/thys/Poincare_Disc/Poincare_Circles.thy @@ -1,618 +1,618 @@ theory Poincare_Circles imports Poincare_Distance begin (* -------------------------------------------------------------------------- *) section\H-circles in the Poincar\'e model\ (* -------------------------------------------------------------------------- *) text\Circles consist of points that are at the same distance from the center.\ definition poincare_circle :: "complex_homo \ real \ complex_homo set" where "poincare_circle z r = {z'. z' \ unit_disc \ poincare_distance z z' = r}" text\Each h-circle in the Poincar\'e model is represented by an Euclidean circle in the model --- the center and radius of that euclidean circle are determined by the following formulas.\ definition poincare_circle_euclidean :: "complex_homo \ real \ euclidean_circle" where "poincare_circle_euclidean z r = (let R = (cosh r - 1) / 2; z' = to_complex z; cz = 1 - (cmod z')\<^sup>2; k = cz * R + 1 in (z' / k, cz * sqrt(R * (R + 1)) / k))" text\That Euclidean circle has a positive radius and is always fully within the disc.\ lemma poincare_circle_in_disc: assumes "r > 0" and "z \ unit_disc" and "(ze, re) = poincare_circle_euclidean z r" shows "cmod ze < 1" "re > 0" "\ x \ circle ze re. cmod x < 1" proof- let ?R = "(cosh r - 1) / 2" let ?z' = "to_complex z" let ?cz = "1 - (cmod ?z')\<^sup>2" let ?k = "?cz * ?R + 1" let ?ze = "?z' / ?k" let ?re = "?cz * sqrt(?R * (?R + 1)) / ?k" from \z \ unit_disc\ obtain z' where z': "z = of_complex z'" using inf_or_of_complex[of z] by auto hence "z' = ?z'" by simp obtain cz where cz: "cz = (1 - (cmod z')\<^sup>2)" by auto have "cz > 0" "cz \ 1" using \z \ unit_disc\ z' cz using unit_disc_cmod_square_lt_1 by fastforce+ obtain R where R: "R = ?R" by blast have "R > 0" using cosh_gt_1[of r] \r > 0\ by (subst R) simp obtain k where k: "k = cz * R + 1" by auto have "k > 1" using k \R > 0\ \cz > 0\ by simp hence "cmod k = k" by simp let ?RR = "cz * sqrt(R * (R + 1)) / k" have "cmod z' + cz * sqrt(R * (R + 1)) < k" proof- have "((R+1)-R)\<^sup>2 > 0" by simp hence "(R+1)\<^sup>2 - 2*R*(R+1) + R\<^sup>2 > 0" unfolding power2_diff by (simp add: field_simps) hence "(R+1)\<^sup>2 + 2*R*(R+1) + R\<^sup>2 - 4*R*(R+1) > 0" by simp hence "(2*R+1)\<^sup>2 / 4 > R*(R+1)" using power2_sum[of "R+1" R] by (simp add: field_simps) hence "sqrt(R*(R+1)) < (2*R+1) / 2" using \R > 0\ - by (smt arith_geo_mean_sqrt linordered_field_class.sign_simps(45) power_divide real_sqrt_four real_sqrt_pow2) + by (smt arith_geo_mean_sqrt power_divide real_sqrt_four real_sqrt_pow2 zero_le_mult_iff) hence "sqrt(R*(R+1)) - R < 1/2" by (simp add: field_simps) hence "(1 + (cmod z')) * (sqrt(R*(R+1)) - R) < (1 + (cmod z')) * (1 / 2)" by (subst mult_strict_left_mono, simp, smt norm_not_less_zero, simp) also have "... < 1" using \z \ unit_disc\ z' by auto finally have "(1 - cmod z') * ((1 + cmod z') * (sqrt(R*(R+1)) - R)) < (1 - cmod z') * 1" using \z \ unit_disc\ z' by (subst mult_strict_left_mono, simp_all) hence "cz * (sqrt (R*(R+1)) - R) < 1 - cmod z'" using square_diff_square_factored[of 1 "cmod z'"] by (subst cz, subst (asm) mult.assoc[symmetric], simp add: power2_eq_square field_simps) hence "cmod z' + cz * sqrt(R*(R+1)) < 1 + R * cz" by (simp add: field_simps) thus ?thesis using k by (simp add: field_simps) qed hence "cmod z' / k + cz * sqrt(R * (R + 1)) / k < 1" using \k > 1\ unfolding add_divide_distrib[symmetric] by simp hence "cmod (z' / k) + cz * sqrt(R * (R + 1)) / k < 1" using \k > 1\ by simp hence "cmod ?ze + ?re < 1" using k cz \R = ?R\ z' by simp moreover have "cz * sqrt(R * (R + 1)) / k > 0" using \cz > 0\ \R > 0\ \k > 1\ by auto hence "?re > 0" using k cz \R = ?R\ z' by simp moreover have "cmod ?ze < 1" using \cmod ?ze + ?re < 1\ \?re > 0\ by simp moreover have "ze = ?ze" "re = ?re" using \(ze, re) = poincare_circle_euclidean z r\ unfolding poincare_circle_euclidean_def Let_def by simp_all moreover have "\ x \ circle ze re. cmod x \ cmod ze + re" using norm_triangle_ineq2[of _ ze] unfolding circle_def by (smt mem_Collect_eq) ultimately show "cmod ze < 1" "re > 0" "\ x \ circle ze re. cmod x < 1" by auto qed text\The connection between the points on the h-circle and its corresponding Euclidean circle.\ lemma poincare_circle_is_euclidean_circle: assumes "z \ unit_disc" and "r > 0" shows "let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` (circle Ze Re) = poincare_circle z r" proof- { fix x let ?z = "to_complex z" from assms obtain z' where z': "z = of_complex z'" "cmod z' < 1" using inf_or_of_complex[of z] by auto have *: "\ x. cmod x < 1 \ 1 - (cmod x)\<^sup>2 > 0" by (metis less_iff_diff_less_0 minus_diff_eq mult.left_neutral neg_less_0_iff_less norm_mult_less norm_power power2_eq_square) let ?R = "(cosh r - 1) / 2" obtain R where R: "R = ?R" by blast let ?cx = "1 - (cmod x)\<^sup>2" and ?cz = "1 - (cmod z')\<^sup>2" and ?czx = "(cmod (z' - x))\<^sup>2" let ?k = "1 + R * ?cz" obtain k where k: "k = ?k" by blast have "R > 0" using R cosh_gt_1[OF \r > 0\] by simp hence "k > 1" using assms z' k *[of z'] by auto hence **: "cor k \ 0" by (smt of_real_eq_0_iff) have "of_complex x \ poincare_circle z r \ cmod x < 1 \ poincare_distance z (of_complex x) = r" unfolding poincare_circle_def by auto also have "... \ cmod x < 1 \ poincare_distance_formula' ?z x = cosh r" using poincare_distance_formula[of z "of_complex x"] cosh_dist[of z "of_complex x"] unfolding poincare_distance_formula_def using assms using arcosh_cosh_real by auto also have "... \ cmod x < 1 \ ?czx / (?cz * ?cx) = ?R" using z' by (simp add: field_simps) also have "... \ cmod x < 1 \ ?czx = ?R * ?cx * ?cz" using assms z' *[of z'] *[of x] using nonzero_divide_eq_eq[of "(1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)" "(cmod (z' - x))\<^sup>2" ?R] by (auto, simp add: field_simps) also have "... \ cmod x < 1 \ (z' - x) * (cnj z' - cnj x) = R * ?cz * (1 - x * cnj x)" (is "_ \ _ \ ?l = ?r") proof- let ?l = "(z' - x) * (cnj z' - cnj x)" and ?r = "R * (1 - Re (z' * cnj z')) * (1 - x * cnj x)" have "is_real ?l" using eq_cnj_iff_real[of "?l"] by simp moreover have "is_real ?r" using eq_cnj_iff_real[of "1 - x * cnj x"] using Im_complex_of_real[of "R * (1 - Re (z' * cnj z'))"] by simp ultimately show ?thesis apply (subst R[symmetric]) apply (subst cmod_square)+ apply (subst complex_eq_if_Re_eq, simp_all add: field_simps) done qed also have "... \ cmod x < 1 \ z' * cnj z' - x * cnj z' - cnj x * z' + x * cnj x = R * ?cz - R * ?cz * x * cnj x" unfolding right_diff_distrib left_diff_distrib by (simp add: field_simps) also have "... \ cmod x < 1 \ k * (x * cnj x) - x * cnj z' - cnj x * z' + z' * cnj z' = R * ?cz" (is "_ \ _ \ ?lhs = ?rhs") by (subst k) (auto simp add: field_simps) also have "... \ cmod x < 1 \ (k * x * cnj x - x * cnj z' - cnj x * z' + z' * cnj z') / k = (R * ?cz) / k" using ** by (auto simp add: Groups.mult_ac(1)) also have "... \ cmod x < 1 \ x * cnj x - x * cnj z' / k - cnj x * z' / k + z' * cnj z' / k = (R * ?cz) / k" using ** unfolding add_divide_distrib diff_divide_distrib by auto also have "... \ cmod x < 1 \ (x - z'/k) * cnj(x - z'/k) = (R * ?cz) / k + (z' / k) * cnj(z' / k) - z' * cnj z' / k" by (auto simp add: field_simps diff_divide_distrib) also have "... \ cmod x < 1 \ (cmod (x - z'/k))\<^sup>2 = (R * ?cz) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k" apply (subst complex_mult_cnj_cmod)+ apply (subst complex_eq_if_Re_eq) apply (simp_all add: power_divide) done also have "... \ cmod x < 1 \ (cmod (x - z'/k))\<^sup>2 = (R * ?cz * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2" using ** unfolding add_divide_distrib diff_divide_distrib by (simp add: power2_eq_square) also have "... \ cmod x < 1 \ (cmod (x - z'/k))\<^sup>2 = ?cz\<^sup>2 * R * (R + 1) / k\<^sup>2" (is "_ \ _ \ ?a\<^sup>2 = ?b") proof- have *: "R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1)" by (subst k)+ (simp add: field_simps power2_diff) thus ?thesis by (subst *, simp) qed also have "... \ cmod x < 1 \ cmod (x - z'/k) = ?cz * sqrt (R * (R + 1)) / k" using \R > 0\ *[of z'] ** \k > 1\ \z \ unit_disc\ z' using real_sqrt_unique[of ?a ?b, symmetric] by (auto simp add: real_sqrt_divide real_sqrt_mult power_divide power_mult_distrib) finally have "of_complex x \ poincare_circle z r \ cmod x < 1 \ x \ circle (z'/k) (?cz * sqrt(R * (R+1)) / k)" unfolding circle_def z' k R by simp hence "of_complex x \ poincare_circle z r \ (let (Ze, Re) = poincare_circle_euclidean z r in cmod x < 1 \ x \ circle Ze Re)" unfolding poincare_circle_euclidean_def Let_def circle_def using z' R k by (simp add: field_simps) hence "of_complex x \ poincare_circle z r \ (let (Ze, Re) = poincare_circle_euclidean z r in x \ circle Ze Re)" using poincare_circle_in_disc[OF \r > 0\ \z \ unit_disc\] by auto } note * = this show ?thesis unfolding Let_def proof safe fix Ze Re x assume "poincare_circle_euclidean z r = (Ze, Re)" "x \ circle Ze Re" thus "of_complex x \ poincare_circle z r" using *[of x] by simp next fix Ze Re x assume **: "poincare_circle_euclidean z r = (Ze, Re)" "x \ poincare_circle z r" then obtain x' where x': "x = of_complex x'" unfolding poincare_circle_def using inf_or_of_complex[of x] by auto hence "x' \ circle Ze Re" using *[of x'] ** by simp thus "x \ of_complex ` circle Ze Re" using x' by auto qed qed subsection \Intersection of circles in special positions\ text \Two h-circles centered at the x-axis intersect at mutually conjugate points\ lemma intersect_poincare_circles_x_axis: assumes z: "is_real z1" and "is_real z2" and "r1 > 0" and "r2 > 0" and "-1 < Re z1" and "Re z1 < 1" and "-1 < Re z2" and "Re z2 < 1" and "z1 \ z2" assumes x1: "x1 \ poincare_circle (of_complex z1) r1 \ poincare_circle (of_complex z2) r2" and x2: "x2 \ poincare_circle (of_complex z1) r1 \ poincare_circle (of_complex z2) r2" and "x1 \ x2" shows "x1 = conjugate x2" proof- have in_disc: "of_complex z1 \ unit_disc" "of_complex z2 \ unit_disc" using assms by (auto simp add: cmod_eq_Re) obtain x1' x2' where x': "x1 = of_complex x1'" "x2 = of_complex x2'" using x1 x2 using inf_or_of_complex[of x1] inf_or_of_complex[of x2] unfolding poincare_circle_def by auto obtain Ze1 Re1 where 1: "(Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1" by (metis poincare_circle_euclidean_def) obtain Ze2 Re2 where 2: "(Ze2, Re2) = poincare_circle_euclidean (of_complex z2) r2" by (metis poincare_circle_euclidean_def) have circle: "x1' \ circle Ze1 Re1 \ circle Ze2 Re2" "x2' \ circle Ze1 Re1 \ circle Ze2 Re2" using poincare_circle_is_euclidean_circle[of "of_complex z1" r1] using poincare_circle_is_euclidean_circle[of "of_complex z2" r2] using assms 1 2 \of_complex z1 \ unit_disc\ \of_complex z2 \ unit_disc\ x' by auto (metis image_iff of_complex_inj)+ have "is_real Ze1" "is_real Ze2" using 1 2 \is_real z1\ \is_real z2\ by (simp_all add: poincare_circle_euclidean_def Let_def) have "Re1 > 0" "Re2 > 0" using 1 2 in_disc \r1 > 0\ \r2 > 0\ using poincare_circle_in_disc(2)[of r1 "of_complex z1" Ze1 Re1] using poincare_circle_in_disc(2)[of r2 "of_complex z2" Ze2 Re2] by auto have "Ze1 \ Ze2" proof (rule ccontr) assume "\ ?thesis" hence eq: "Ze1 = Ze2" "Re1 = Re2" using circle(1) unfolding circle_def by auto let ?A = "Ze1 - Re1" and ?B = "Ze1 + Re1" have "?A \ circle Ze1 Re1" "?B \ circle Ze1 Re1" using \Re1 > 0\ unfolding circle_def by simp_all hence "of_complex ?A \ poincare_circle (of_complex z1) r1" "of_complex ?B \ poincare_circle (of_complex z1) r1" "of_complex ?A \ poincare_circle (of_complex z2) r2" "of_complex ?B \ poincare_circle (of_complex z2) r2" using eq using poincare_circle_is_euclidean_circle[OF \of_complex z1 \ unit_disc\ \r1 > 0\] using poincare_circle_is_euclidean_circle[OF \of_complex z2 \ unit_disc\ \r2 > 0\] using 1 2 by auto blast+ hence "poincare_distance (of_complex z1) (of_complex ?A) = poincare_distance (of_complex z1) (of_complex ?B)" "poincare_distance (of_complex z2) (of_complex ?A) = poincare_distance (of_complex z2) (of_complex ?B)" "-1 < Re (Ze1 - Re1)" "Re (Ze1 - Re1) < 1" "-1 < Re (Ze1 + Re1)" "Re (Ze1 + Re1) < 1" using \is_real Ze1\ \is_real Ze2\ unfolding poincare_circle_def by (auto simp add: cmod_eq_Re) hence "z1 = z2" using unique_midpoint_x_axis[of "Ze1 - Re1" "Ze1 + Re1"] using \is_real Ze1\ \is_real z1\ \is_real z2\ \Re1 > 0\ \-1 < Re z1\ \Re z1 < 1\ \-1 < Re z2\ \Re z2 < 1\ by auto thus False using \z1 \ z2\ by simp qed hence *: "(Re x1')\<^sup>2 + (Im x1')\<^sup>2 - 2 * Re x1' * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0" "(Re x1')\<^sup>2 + (Im x1')\<^sup>2 - 2 * Re x1' * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0" "(Re x2')\<^sup>2 + (Im x2')\<^sup>2 - 2 * Re x2' * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0" "(Re x2')\<^sup>2 + (Im x2')\<^sup>2 - 2 * Re x2' * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0" using circle_equation[of Re1 Ze1] circle_equation[of Re2 Ze2] circle using eq_cnj_iff_real[of Ze1] \is_real Ze1\ \Re1 > 0\ using eq_cnj_iff_real[of Ze2] \is_real Ze2\ \Re2 > 0\ using complex_add_cnj[of x1'] complex_add_cnj[of x2'] using distrib_left[of Ze1 x1' "cnj x1'"] distrib_left[of Ze2 x1' "cnj x1'"] using distrib_left[of Ze1 x2' "cnj x2'"] distrib_left[of Ze2 x2' "cnj x2'"] by (auto simp add: complex_mult_cnj power2_eq_square field_simps) hence "- 2 * Re x1' * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = - 2 * Re x1' * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2)" "- 2 * Re x2' * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = - 2 * Re x2' * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2)" by (smt add_diff_cancel_right' add_diff_eq eq_iff_diff_eq_0 minus_diff_eq mult_minus_left of_real_minus)+ hence "2 * Re x1' * (Ze2 - Ze1) = (Ze2 * Ze2 - cor (Re2 * Re2)) - (Ze1 * Ze1 - cor (Re1 * Re1))" "2 * Re x2' * (Ze2 - Ze1) = (Ze2 * Ze2 - cor (Re2 * Re2)) - (Ze1 * Ze1 - cor (Re1 * Re1))" by simp_all (simp add: field_simps)+ hence "2 * Re x1' * (Ze2 - Ze1) = 2 * Re x2' * (Ze2 - Ze1)" by simp hence "Re x1' = Re x2'" using \Ze1 \ Ze2\ by simp moreover hence "(Im x1')\<^sup>2 = (Im x2')\<^sup>2" using *(1) *(3) by (simp add: \is_real Ze1\ complex_eq_if_Re_eq) hence "Im x1' = Im x2' \ Im x1' = -Im x2'" using power2_eq_iff by blast ultimately show ?thesis using x' `x1 \ x2` using complex.expand by (metis cnj.code complex_surj conjugate_of_complex) qed text \Two h-circles of the same radius centered at mutually conjugate points intersect at the x-axis\ lemma intersect_poincare_circles_conjugate_centers: assumes in_disc: "z1 \ unit_disc" "z2 \ unit_disc" and "z1 \ z2" and "z1 = conjugate z2" and "r > 0" and u: "u \ poincare_circle z1 r \ poincare_circle z2 r" shows "is_real (to_complex u)" proof- obtain z1e r1e z2e r2e where euclidean: "(z1e, r1e) = poincare_circle_euclidean z1 r" "(z2e, r2e) = poincare_circle_euclidean z2 r" by (metis poincare_circle_euclidean_def) obtain z1' z2' where z': "z1 = of_complex z1'" "z2 = of_complex z2'" using inf_or_of_complex[of z1] inf_or_of_complex[of z2] in_disc by auto obtain u' where u': "u = of_complex u'" using u inf_or_of_complex[of u] by (auto simp add: poincare_circle_def) have "z1' = cnj z2'" using \z1 = conjugate z2\ z' by (auto simp add: of_complex_inj) moreover let ?cz = "1 - (cmod z2')\<^sup>2" let ?den = "?cz * (cosh r - 1) / 2 + 1" have "?cz > 0" using in_disc z' by (simp add: cmod_def) hence "?den \ 1" using cosh_gt_1[OF \r > 0\] by auto hence "?den \ 0" by simp hence "cor ?den \ 0" using of_real_eq_0_iff by blast ultimately have "r1e = r2e" "z1e = cnj z2e" "z1e \ z2e" using z' euclidean \z1 \ z2\ unfolding poincare_circle_euclidean_def Let_def by simp_all metis hence "u' \ circle (cnj z2e) r2e \ circle z2e r2e" "z2e \ cnj z2e" using euclidean u u' using poincare_circle_is_euclidean_circle[of z1 r] using poincare_circle_is_euclidean_circle[of z2 r] using in_disc \r > 0\ by auto (metis image_iff of_complex_inj)+ hence "(cmod (u' - z2e))\<^sup>2 = (cmod(u' - cnj z2e))\<^sup>2" by (simp add: circle_def) hence "(u' - z2e) * (cnj u' - cnj z2e) = (u' - cnj z2e) * (cnj u' - z2e)" by (metis complex_cnj_cnj complex_cnj_diff complex_norm_square) hence "(z2e - cnj z2e) * (u' - cnj u') = 0" by (simp add: field_simps) thus ?thesis using u' \z2e \ cnj z2e\ eq_cnj_iff_real[of u'] by simp qed subsection \Congruent triangles\ text\For every pair of triangles such that its three pairs of sides are pairwise equal there is an h-isometry (a unit disc preserving Möbius transform, eventually composed with a conjugation) that maps one triangle onto the other.\ lemma unit_disc_fix_f_congruent_triangles: assumes in_disc: "u \ unit_disc" "v \ unit_disc" "w \ unit_disc" and in_disc': "u' \ unit_disc" "v' \ unit_disc" "w' \ unit_disc" and d: "poincare_distance u v = poincare_distance u' v'" "poincare_distance v w = poincare_distance v' w'" "poincare_distance u w = poincare_distance u' w'" shows "\ M. unit_disc_fix_f M \ M u = u' \ M v = v' \ M w = w'" proof (cases "u = v \ u = w \ v = w") case True thus ?thesis using assms using poincare_distance_eq_0_iff[of u' v'] using poincare_distance_eq_0_iff[of v' w'] using poincare_distance_eq_0_iff[of u' w'] using poincare_distance_eq_ex_moebius[of v w v' w'] using poincare_distance_eq_ex_moebius[of u w u' w'] using poincare_distance_eq_ex_moebius[of u v u' v'] by (metis unit_disc_fix_f_def) next case False have "\ w u' v' w'. w \ unit_disc \ u' \ unit_disc \ v' \ unit_disc \ w' \ unit_disc \ w \ u \ w \ v \ poincare_distance u v = poincare_distance u' v' \ poincare_distance v w = poincare_distance v' w' \ poincare_distance u w = poincare_distance u' w' \ (\ M. unit_disc_fix_f M \ M u = u' \ M v = v' \ M w = w')" (is "?P u v") proof (rule wlog_positive_x_axis[where P="?P"]) show "v \ unit_disc" "u \ unit_disc" by fact+ next show "u \ v" using False by simp next fix x assume x: "is_real x" "0 < Re x" "Re x < 1" hence "of_complex x \ 0\<^sub>h" using of_complex_zero_iff[of x] by (auto simp add: complex.expand) show "?P 0\<^sub>h (of_complex x)" proof safe fix w u' v' w' assume in_disc: "w \ unit_disc" "u' \ unit_disc" "v' \ unit_disc" "w' \ unit_disc" assume "poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'" then obtain M' where M': "unit_disc_fix M'" "moebius_pt M' u' = 0\<^sub>h" "moebius_pt M' v' = (of_complex x)" using poincare_distance_eq_ex_moebius[of u' v' "0\<^sub>h" "of_complex x"] in_disc x by (auto simp add: cmod_eq_Re) let ?w = "moebius_pt M' w'" have "?w \ unit_disc" using \unit_disc_fix M'\ \w' \ unit_disc\ by simp assume "w \ 0\<^sub>h" "w \ of_complex x" hence dist_gt_0: "poincare_distance 0\<^sub>h w > 0" "poincare_distance (of_complex x) w > 0" using poincare_distance_eq_0_iff[of "0\<^sub>h" w] in_disc poincare_distance_ge0[of "0\<^sub>h" w] using poincare_distance_eq_0_iff[of "of_complex x" w] in_disc poincare_distance_ge0[of "of_complex x" w] using x by (simp_all add: cmod_eq_Re) assume "poincare_distance (of_complex x) w = poincare_distance v' w'" "poincare_distance 0\<^sub>h w = poincare_distance u' w'" hence "poincare_distance 0\<^sub>h ?w = poincare_distance 0\<^sub>h w" "poincare_distance (of_complex x) ?w = poincare_distance (of_complex x) w" using M'(1) M'(2)[symmetric] M'(3)[symmetric] in_disc using unit_disc_fix_preserve_poincare_distance[of M' u' w'] using unit_disc_fix_preserve_poincare_distance[of M' v' w'] by simp_all hence "?w \ poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \ poincare_circle (of_complex x) (poincare_distance (of_complex x) w)" "w \ poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \ poincare_circle (of_complex x) (poincare_distance (of_complex x) w)" using \?w \ unit_disc\ \w \ unit_disc\ unfolding poincare_circle_def by simp_all hence "?w = w \ ?w = conjugate w" using intersect_poincare_circles_x_axis[of 0 x "poincare_distance 0\<^sub>h w" "poincare_distance (of_complex x) w" ?w w] x using \of_complex x \ 0\<^sub>h\ dist_gt_0 using poincare_distance_eq_0_iff by auto thus "\M. unit_disc_fix_f M \ M 0\<^sub>h = u' \ M (of_complex x) = v' \ M w = w'" proof assume "moebius_pt M' w' = w" thus ?thesis using M' using moebius_pt_invert[of M' u' "0\<^sub>h"] using moebius_pt_invert[of M' v' "of_complex x"] using moebius_pt_invert[of M' w' "w"] apply (rule_tac x="moebius_pt (-M')" in exI) apply (simp add: unit_disc_fix_f_def) apply (rule_tac x="-M'" in exI, simp) done next let ?M = "moebius_pt (-M') \ conjugate" assume "moebius_pt M' w' = conjugate w" hence "?M w = w'" using moebius_pt_invert[of M' w' "conjugate w"] by simp moreover have "?M 0\<^sub>h = u'" "?M (of_complex x) = v'" using moebius_pt_invert[of M' u' "0\<^sub>h"] using moebius_pt_invert[of M' v' "of_complex x"] using M' \is_real x\ eq_cnj_iff_real[of x] by simp_all moreover have "unit_disc_fix_f ?M" using \unit_disc_fix M'\ unfolding unit_disc_fix_f_def by (rule_tac x="-M'" in exI, simp) ultimately show ?thesis by blast qed qed next fix M u v assume 1: "unit_disc_fix M" "u \ unit_disc" "v \ unit_disc" let ?Mu = "moebius_pt M u" and ?Mv = "moebius_pt M v" assume 2: "?P ?Mu ?Mv" show "?P u v" proof safe fix w u' v' w' let ?Mw = "moebius_pt M w" and ?Mu' = "moebius_pt M u'" and ?Mv' = "moebius_pt M v'" and ?Mw' = "moebius_pt M w'" assume "w \ unit_disc" "u' \ unit_disc" "v' \ unit_disc" "w' \ unit_disc" "w \ u" "w \ v" "poincare_distance u v = poincare_distance u' v'" "poincare_distance v w = poincare_distance v' w'" "poincare_distance u w = poincare_distance u' w'" then obtain M' where M': "unit_disc_fix_f M'" "M' ?Mu = ?Mu'" "M' ?Mv = ?Mv'" "M' ?Mw = ?Mw'" using 1 2[rule_format, of ?Mw ?Mu' ?Mv' ?Mw'] by auto let ?M = "moebius_pt (-M) \ M' \ moebius_pt M" show "\M. unit_disc_fix_f M \ M u = u' \ M v = v' \ M w = w'" proof (rule_tac x="?M" in exI, safe) show "unit_disc_fix_f ?M" using M'(1) \unit_disc_fix M\ by (subst unit_disc_fix_f_comp, subst unit_disc_fix_f_comp, simp_all) next show "?M u = u'" "?M v = v'" "?M w = w'" using M' by auto qed qed qed thus ?thesis using assms False by auto qed end \ No newline at end of file