Commit f11922aa authored by Lawrence Paulson's avatar Lawrence Paulson

follow_on changes from Complex_Geometry

parent de4ae134bdf9
......@@ -456,7 +456,7 @@ next
using unit_disc_fix_moebius_preserve_poincare_between[of ?M "0\<^sub>h" u v]
using \<open>v \<in> unit_disc\<close> \<open>u \<in> unit_disc\<close> \<open>v \<noteq> 0\<^sub>h\<close> \<open>u \<noteq> 0\<^sub>h\<close>
using arg_mult_eq[of "cis \<phi>" u' v']
by simp (auto simp add: arg_mult)
by simp (auto simp add: arg_mult norm_mult)
qed
qed
thus ?thesis
......@@ -474,13 +474,8 @@ lemma poincare_between_y_axis_0uv:
using poincare_between_0uv[of "of_complex (\<i> * x)" "of_complex (\<i> * y)"]
using arg_pi2_iff[of "\<i> * cor x"] arg_pi2_iff[of "\<i> * cor y"]
using arg_minus_pi2_iff[of "\<i> * cor x"] arg_minus_pi2_iff[of "\<i> * 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
apply (simp add: norm_mult)
apply (smt (verit, best))
done
lemma poincare_between_x_axis_uvw:
......
......@@ -378,12 +378,10 @@ next
by auto
hence "cmod (cnj k * u') = 1"
by auto
hence "cmod k * cmod u' = 1"
by auto
thus False
using \<open>cmod k < 1\<close> \<open>cmod u' < 1\<close>
using mult_strict_mono[of "cmod k" 1 "cmod u'" 1]
by simp
by (simp add: norm_mult)
qed
have "dv \<noteq> 0"
......@@ -394,12 +392,10 @@ next
by auto
hence "cmod (cnj k * v') = 1"
by auto
hence "cmod k * cmod v' = 1"
by auto
thus False
using \<open>cmod k < 1\<close> \<open>cmod v' < 1\<close>
using mult_strict_mono[of "cmod k" 1 "cmod v'" 1]
by simp
by (simp add: norm_mult)
qed
have "kk \<noteq> 0"
......@@ -410,12 +406,10 @@ next
by auto
hence "cmod (k * cnj k) = 1"
by auto
hence "cmod k * cmod k = 1"
by auto
thus False
using \<open>cmod k < 1\<close>
using mult_strict_mono[of "cmod k" 1 "cmod k" 1]
by simp
using complex_mod_sqrt_Re_mult_cnj by auto
qed
note nz = \<open>du \<noteq> 0\<close> \<open>dv \<noteq> 0\<close> \<open>kk \<noteq> 0\<close>
......@@ -428,18 +422,17 @@ next
unfolding complex_mod_mult_cnj[symmetric]
by (subst (asm) d) simp
also have "... = cmod ((d*cnj d*kk*kk) / (du*cnj du*dv*cnj dv))"
by (simp add: field_simps)
finally have 1: "?lhs = cmod ((d*cnj d*kk*kk) / (du*cnj du*dv*cnj dv))"
.
by (simp add: field_simps norm_mult norm_divide)
finally have 1: "?lhs = cmod ((d*cnj d*kk*kk) / (du*cnj du*dv*cnj dv))" .
have "(1 - ((cmod nu) / (cmod du))\<^sup>2)*(1 - ((cmod nv) / (cmod dv))\<^sup>2) =
(1 - cmod((nu * cnj nu) / (du * cnj du)))*(1 - cmod((nv * cnj nv) / (dv * cnj dv)))" (is "?rhs = _")
by (metis cmod_divide complex_mod_mult_cnj power_divide)
by (metis norm_divide complex_mod_mult_cnj power_divide)
also have "... = cmod(((du*cnj du - nu*cnj nu) / (du * cnj du)) * ((dv*cnj dv - nv*cnj nv) / (dv * cnj dv)))"
proof-
have "u' \<noteq> 1 / cnj k" "v' \<noteq> 1 / cnj k"
using \<open>cmod u' < 1\<close> \<open>cmod v' < 1\<close> \<open>cmod k < 1\<close>
by (auto simp add: False)
by (auto simp add: False norm_divide)
moreover
have "cmod k \<noteq> 1"
using \<open>cmod k < 1\<close>
......@@ -472,10 +465,7 @@ next
by (simp_all add: cmod_def)
thus ?thesis
using nz
apply simp
apply (subst diff_divide_eq_iff, simp, simp)
apply (subst diff_divide_eq_iff, simp, simp)
done
by (simp add: diff_divide_distrib norm_mult)
qed
also have "... = cmod(((ddu * kk) / (du * cnj du)) * ((ddv * kk) / (dv * cnj dv)))"
by (subst ddu, subst ddv, simp)
......@@ -488,8 +478,7 @@ next
cmod ((d*cnj d*kk*kk) / (du*cnj du*dv*cnj dv)) / cmod((ddu*ddv*kk*kk) / (du*cnj du*dv*cnj dv))"
by (subst 1, subst 2, simp)
also have "... = cmod ((d*cnj d)/(ddu*ddv))"
using nz
by simp
using nz by (simp add: norm_mult norm_divide)
also have "... = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2)*(1 - (cmod v')\<^sup>2))"
proof-
have "(cmod u')\<^sup>2 < 1" "(cmod v')\<^sup>2 < 1"
......@@ -499,13 +488,10 @@ next
by (auto simp add: cmod_eq_Re cmod_power2 power2_eq_square[symmetric])
thus ?thesis
using nz
apply (subst **)+
unfolding complex_mod_mult_cnj[symmetric]
by simp
by (simp add: "**"(6) "**"(7) norm_divide norm_mult power2_eq_square)
qed
finally
have 3: "?lhs / ?rhs = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2)*(1 - (cmod v')\<^sup>2))"
.
have 3: "?lhs / ?rhs = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2)*(1 - (cmod v')\<^sup>2))" .
have "cmod k \<noteq> 1" "u' \<noteq> 1 / cnj k" "v' \<noteq> 1 / cnj k" "u \<noteq> \<infinity>\<^sub>h" "v \<noteq> \<infinity>\<^sub>h"
using \<open>cmod k < 1\<close> \<open>u \<in> unit_disc\<close> \<open>v \<in> unit_disc\<close> * \<open>k \<noteq> 0\<close> ** \<open>kk \<noteq> 0\<close> nz
......@@ -514,7 +500,7 @@ next
using * ** 3
using moebius_pt_blaschke[of k u']
using moebius_pt_blaschke[of k v']
by simp
by (simp add: norm_divide)
qed
text \<open>To prove the equivalence between the h-distance definition and the distance formula, we shall
......@@ -528,7 +514,7 @@ lemma rotation_preserve_distance_formula [simp]:
poincare_distance_formula (to_complex u) (to_complex v)"
using assms
using inf_or_of_complex[of u] inf_or_of_complex[of v]
by auto
by (auto simp: norm_mult)
text\<open>Unit disc fixing Möbius preserve @{term poincare_distance_formula}.\<close>
lemma unit_disc_fix_preserve_distance_formula [simp]:
......
......@@ -43,7 +43,7 @@ proof (transfer, transfer)
assume "circline_eq_cmat H1 H2"
thus "is_poincare_line_cmat H1 \<longleftrightarrow> is_poincare_line_cmat H2"
using hh
by (cases H1, cases H2) (auto simp add: power_mult_distrib)
by (cases H1, cases H2) (auto simp: norm_mult power_mult_distrib)
qed
lemma is_poincare_line_mk_circline:
......@@ -497,14 +497,14 @@ next
have u: "cor ((Re (u1/u2))\<^sup>2) + cor ((Im (u1/u2))\<^sup>2) = 1"
using \<open>on_circline_cmat_cvec unit_circle_cmat ?u\<close> uv
apply (subst cor_add[symmetric])
apply (subst of_real_add[symmetric])
apply (subst complex_mult_cnj[symmetric])
apply (simp add: vec_cnj_def mult.commute)
done
have v: "cor ((Re (v1/v2))\<^sup>2) + cor ((Im (v1/v2))\<^sup>2) = 1"
using \<open>on_circline_cmat_cvec unit_circle_cmat ?v\<close> uv
apply (subst cor_add[symmetric])
apply (subst of_real_add[symmetric])
apply (subst complex_mult_cnj[symmetric])
apply (simp add: vec_cnj_def mult.commute)
done
......@@ -1261,7 +1261,7 @@ proof (transfer, transfer, safe)
using complex_mult_cnj_cmod[symmetric, of v1]
using complex_mult_cnj_cmod[symmetric, of u2]
using complex_mult_cnj_cmod[symmetric, of v2]
apply (auto simp add: power_divide)
apply (simp add: power_divide norm_mult norm_divide)
apply (rule_tac x="Re ?k" in exI)
apply simp
apply (simp add: field_simps)
......@@ -1377,7 +1377,7 @@ proof (transfer, transfer, safe)
using complex_mult_cnj_cmod[symmetric, of v1]
using complex_mult_cnj_cmod[symmetric, of u2]
using complex_mult_cnj_cmod[symmetric, of v2]
apply (auto simp add: power_divide)
apply (simp add: power_divide norm_mult norm_divide)
apply (rule_tac x="Re ?k" in exI)
apply simp
apply (simp add: field_simps)
......
......@@ -408,7 +408,6 @@ proof transfer
apply (simp add: sgn_mult power_mult_distrib)
apply (subst right_diff_distrib[symmetric])
apply (subst real_sqrt_mult)
apply (subst cor_mult)
by (simp add: real_sgn_eq right_diff_distrib)
thus "calc_x_axis_intersection_cmat_cvec H1 \<approx>\<^sub>v
......
......@@ -54,7 +54,7 @@ proof transfer
case True
hence "is_poincare_line_cmat H2"
using k * hermitean_mult_real[of H1 k] hh
by (auto simp add: power2_eq_square)
by (auto simp add: power2_eq_square norm_mult)
have **: "sqrt (\<bar>k\<bar> * cmod B1 * (\<bar>k\<bar> * cmod B1) - k * Re D1 * (k * Re D1)) =
\<bar>k\<bar> * sqrt(cmod B1 * cmod B1 - Re D1 * Re D1)"
proof-
......@@ -69,7 +69,7 @@ proof transfer
using * k
apply (simp add: Let_def)
apply safe
apply (simp add: power2_eq_square rel_set_def)
apply (simp add: power2_eq_square rel_set_def norm_mult)
apply safe
apply (cases "k > 0")
apply (rule_tac x="(cor k)\<^sup>2" in exI)
......@@ -92,11 +92,11 @@ proof transfer
apply (erule notE, rule_tac x="(cor k)\<^sup>2" in exI)
apply (subst **)
apply (simp add: power2_eq_square field_simps)
apply (rule_tac x="(cor k)\<^sup>2" in exI)
apply (cases "k > 0")
apply (erule notE, rule_tac x="(cor k)\<^sup>2" in exI)
apply (subst **)
apply (simp add: power2_eq_square field_simps)
apply (rule_tac x="(cor k)\<^sup>2" in exI)
apply (subst **)
apply (simp add: power2_eq_square field_simps)
done
......@@ -104,15 +104,13 @@ proof transfer
case False
hence "\<not> is_poincare_line_cmat H2"
using k * hermitean_mult_real[of H1 k] hh
by (auto simp add: power2_eq_square)
by (auto simp add: power2_eq_square norm_mult)
have "rel_set (\<approx>\<^sub>v) {(- 1, 1), (1, 1)} {(- 1, 1), (1, 1)}"
by (simp add: rel_set_def)
thus ?thesis
using \<open>\<not> is_poincare_line_cmat H1\<close> \<open>\<not> is_poincare_line_cmat H2\<close>
using *
apply (simp add: Let_def)
apply safe
done
by (auto simp add: Let_def)
qed
qed
......@@ -531,8 +529,8 @@ proof-
by (metis (mono_tags, lifting) circline_set_unit_circle imageE mem_Collect_eq mult.right_neutral norm_mult to_complex_of_complex unit_circle_set_def)
hence "k = -1"
using \<open>to_complex i1 = cor k * to_complex i2\<close> \<open>i1 \<noteq> i2\<close>
using \<open>i1 \<in> circline_set unit_circle\<close> \<open>i2 \<in> circline_set unit_circle\<close>
by (metis (no_types, lifting) circline_set_unit_circle complex_cnj_complex_of_real complex_mult_cnj_cmod cor_neg_one imageE mult_cancel_right2 norm_one of_real_eq_iff square_eq_1_iff to_complex_of_complex)
using \<open>i1 \<in> circline_set unit_circle\<close> \<open>i2 \<in> circline_set unit_circle\<close>
by (smt (verit, best) mult_cancel_right1 norm_of_real not_inf_on_unit_circle'' of_complex_to_complex of_real_1)
have "\<forall> i1 \<in> calc_ideal_points H. \<forall> i2 \<in> calc_ideal_points H. is_poincare_line H \<and> i1 \<noteq> i2 \<and> to_complex i1 = - to_complex i2 \<longrightarrow>
0\<^sub>h \<in> circline_set H"
......
......@@ -95,7 +95,7 @@ proof-
from in_disc * \<open>u' = cor ru * cis \<phi>\<close> \<open>z' = cor rz * cis \<phi>\<close> \<open>y' = cor ry * cis \<theta>\<close>
have "ru < 1" "rz < 1" "ry < 1"
by simp_all
by (auto simp: norm_mult)
note polar = this y_polar uz_polar
......@@ -1091,7 +1091,7 @@ proof (transfer, transfer)
assume "on_circline_cmat_cvec H (of_complex_cvec (1 / 2 + \<i> / 2))"
hence "6*A + 4*Re B + 4*Im B = 0"
using *
unfolding cor_mult
unfolding of_real_mult
apply (subst Re_express_cnj[of B])
apply (subst Im_express_cnj[of B])
apply (simp add: vec_cnj_def)
......@@ -1428,7 +1428,7 @@ proof-
hence "?a \<noteq> ?c"
by (metis to_complex_of_complex)
have "(-\<i>/2) \<noteq> (1/5)"
by (metis add.inverse_inverse cmod_divide div_by_1 divide_divide_eq_right inverse_eq_divide minus_divide_left mult.commute norm_ii norm_minus_cancel norm_numeral norm_one numeral_One numeral_eq_iff semiring_norm(88))
by (simp add: minus_equation_iff)
hence "?b \<noteq> ?c"
by (metis to_complex_of_complex)
......@@ -1436,7 +1436,6 @@ proof-
by auto
moreover
have "\<not>(poincare_collinear {?a, ?b, ?c})"
unfolding poincare_collinear_def
proof(rule ccontr)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment