Theory Impossible_Geometry
section ‹Proving the impossibility of trisecting an angle and doubling the cube›
theory Impossible_Geometry
imports Complex_Main
begin
section ‹Formal Proof›
subsection ‹Definition of the set of Points›
datatype point = Point real real
definition points_def:
"points = {M. ∃ x ∈ ℝ. ∃ y ∈ ℝ. (M = Point x y)}"
primrec abscissa :: "point => real"
where abscissa: "abscissa (Point x y) = x"
primrec ordinate :: "point => real"
where ordinate: "ordinate (Point x y) = y"
lemma point_surj [simp]:
"Point (abscissa M) (ordinate M) = M"
by (induct M) simp
lemma point_eqI [intro?]:
"⟦abscissa M = abscissa N; ordinate M = ordinate N⟧ ⟹ M = N"
by (induct M, induct N) simp
lemma point_eq_iff:
"M = N ⟷ abscissa M = abscissa N ∧ ordinate M = ordinate N"
by (induct M, induct N) simp
subsection ‹Subtraction›
text ‹Datatype point has a structure of abelian group›
instantiation point :: ab_group_add
begin
definition point_zero_def:
"0 = Point 0 0"
definition point_one_def:
"point_one = Point 1 0"
definition point_add_def:
"A + B = Point (abscissa A + abscissa B) (ordinate A + ordinate B)"
definition point_minus_def:
"- A = Point (- abscissa A) (- ordinate A)"
definition point_diff_def:
"A - (B::point) = A + - B"
lemma Point_eq_0 [simp]:
"Point xA yA = 0 ⟷ (xA = 0 ∧ yA = 0)"
by (simp add: point_zero_def)
lemma point_abscissa_zero [simp]:
"abscissa 0 = 0"
by (simp add: point_zero_def)
lemma point_ordinate_zero [simp]:
"ordinate 0 = 0"
by (simp add: point_zero_def)
lemma point_add [simp]:
"Point xA yA + Point xB yB = Point (xA + xB) (yA + yB)"
by (simp add: point_add_def)
lemma point_abscissa_add [simp]:
"abscissa (A + B) = abscissa A + abscissa B"
by (simp add: point_add_def)
lemma point_ordinate_add [simp]:
"ordinate (A + B) = ordinate A + ordinate B"
by (simp add: point_add_def)
lemma point_minus [simp]:
"- (Point xA yA) = Point (- xA) (- yA)"
by (simp add: point_minus_def)
lemma point_abscissa_minus [simp]:
"abscissa (- A) = - abscissa (A)"
by (simp add: point_minus_def)
lemma point_ordinate_minus [simp]:
"ordinate (- A) = - ordinate (A)"
by (simp add: point_minus_def)
lemma point_diff [simp]:
"Point xA yA - Point xB yB = Point (xA - xB) (yA - yB)"
by (simp add: point_diff_def)
lemma point_abscissa_diff [simp]:
"abscissa (A - B) = abscissa (A) - abscissa (B)"
by (simp add: point_diff_def)
lemma point_ordinate_diff [simp]:
"ordinate (A - B) = ordinate (A) - ordinate (B)"
by (simp add: point_diff_def)
instance
by intro_classes (simp_all add: point_add_def point_diff_def)
end
subsection ‹Metric Space›
text ‹We can also define a distance, hence point is also a metric space›
instantiation point :: metric_space
begin
definition point_dist_def:
"dist A B = sqrt ((abscissa (A - B))^2 + (ordinate (A - B))^2)"
definition
"(uniformity :: (point × point) filter) = (INF e∈{0 <..}. principal {(x, y). dist x y < e})"
definition
"open (S :: point set) = (∀x∈S. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ S)"
lemma point_dist [simp]:
"dist (Point xA yA) (Point xB yB) = sqrt ((xA - xB)^2 + (yA - yB)^2)"
unfolding point_dist_def
by simp
lemma real_sqrt_diff_squares_triangle_ineq:
fixes a b c d :: real
shows "sqrt ((a - c)^2 + (b - d)^2) ≤ sqrt (a^2 + b^2) + sqrt (c^2 + d^2)"
proof -
have "sqrt ((a - c)^2 + (b - d)^2) ≤ sqrt (a^2 + b^2) + sqrt ((-c)^2 + (-d)^2)"
by (metis diff_conv_add_uminus real_sqrt_sum_squares_triangle_ineq)
also have "... = sqrt (a^2 + b^2) + sqrt (c^2 + d^2)"
by simp
finally show ?thesis .
qed
instance
proof
fix A B C :: point and S :: "point set"
show "(dist A B = 0) = (A = B)"
by (induct A, induct B) (simp add: point_dist_def)
show "(dist A B) ≤ (dist A C) + (dist B C)"
proof -
have "sqrt ((abscissa (A - B))^2 + (ordinate (A - B))^2) ≤
sqrt ((abscissa (A - C))^2 + (ordinate (A - C))^2) +
sqrt ((abscissa (B - C))^2 + (ordinate (B - C))^2)"
using real_sqrt_diff_squares_triangle_ineq
[of "abscissa (A) - abscissa (C)" "abscissa (B) - abscissa (C)"
"ordinate (A) - ordinate (C)" "ordinate (B) - ordinate (C)"]
by (simp only: point_diff_def) (simp add: algebra_simps)
thus ?thesis
by (simp add: point_dist_def)
qed
qed (rule uniformity_point_def open_point_def)+
end
subsection ‹Geometric Definitions›
text ‹These geometric definitions will later be used to define
constructible points›
text ‹The distance between two points is defined with the distance
of the metric space point›
definition distance_def:
"distance A B = dist A B"
text ‹@{term "parallel A B C D"} is true if the lines @{term "(AB)"}
and @{term "(CD)"} are parallel. If not it is false.›
definition parallel_def:
"parallel A B C D = ((abscissa A - abscissa B) * (ordinate C - ordinate D) = (ordinate A - ordinate B) * (abscissa C - abscissa D))"
text ‹Three points @{term "A B C"} are collinear if and only if the
lines @{term "(AB)"} and @{term "(AC)"} are parallel›
definition collinear_def:
"collinear A B C = parallel A B A C"
text ‹The point @{term M} is the intersection of two lines @{term
"(AB)"} and @{term "(CD)"} if and only if the points @{term A}, @{term
M} and @{term B} are collinear and the points @{term C}, @{term M} and
@{term D} are also collinear›
definition is_intersection_def:
"is_intersection M A B C D = (collinear A M B ∧ collinear C M D)"
subsection ‹Reals definable with square roots›
text ‹The inductive set @{term "radical_sqrt"} defines the reals
that can be defined with square roots. If @{term x} is in the
following set, then it depends only upon rational expressions and
square roots. For example, suppose @{term x} is of the form : $x =
(\sqrt{a + \sqrt{b}} + \sqrt{c + \sqrt{d*e +f}}) / (\sqrt{a} +
\sqrt{b}) + (a + \sqrt{b}) / \sqrt{g}$, where @{term a}, @{term b},
@{term c}, @{term d}, @{term e}, @{term f} and @{term g} are
rationals. Then @{term x} is in @{term "radical_sqrt"} because it is
only defined with rationals and square roots of radicals.›
inductive_set radical_sqrt :: "real set"
where
"x ∈ ℚ ⟹ x ∈ radical_sqrt"|
"x ∈ radical_sqrt ⟹ -x ∈ radical_sqrt"|
"x ∈ radical_sqrt ⟹ x ≠ 0 ⟹ 1/x ∈ radical_sqrt"|
"x ∈ radical_sqrt ⟹ y ∈ radical_sqrt ⟹ x+y ∈ radical_sqrt"|
"x ∈ radical_sqrt ⟹ y ∈ radical_sqrt ⟹ x*y ∈ radical_sqrt"|
"x ∈ radical_sqrt ⟹ x ≥ 0 ⟹ sqrt x ∈ radical_sqrt"
text ‹Here, we list some rules that will be used to prove that a
given real is in @{term "radical_sqrt"}.›
text ‹Given two reals in @{term "radical_sqrt"} @{term x} and @{term
y}, the subtraction $x - y$ is also in @{term "radical_sqrt"}.›
lemma radical_sqrt_rule_subtraction:
"x ∈ radical_sqrt ⟹ y ∈ radical_sqrt ⟹ x-y ∈ radical_sqrt"
by (metis diff_conv_add_uminus radical_sqrt.intros(2) radical_sqrt.intros(4))
text ‹Given two reals in @{term "radical_sqrt"} @{term x} and @{term
y}, and $y \neq 0$, the division $x / y$ is also in @{term
"radical_sqrt"}.›
lemma radical_sqrt_rule_division:
"x ∈ radical_sqrt ⟹ y ∈ radical_sqrt ⟹ y ≠ 0 ⟹ x/y ∈ radical_sqrt"
by (metis divide_real_def radical_sqrt.intros(3) radical_sqrt.intros(5) real_scaleR_def real_vector.scale_one)
text ‹Given a positive real @{term x} in @{term "radical_sqrt"}, its
square $x^2$ is also in @{term "radical_sqrt"}.›
lemma radical_sqrt_rule_power2:
"x ∈ radical_sqrt ⟹ x ≥ 0 ⟹ x^2 ∈ radical_sqrt"
by (metis power2_eq_square radical_sqrt.intros(5))
text ‹Given a positive real @{term x} in @{term "radical_sqrt"}, its
cube $x^3$ is also in @{term "radical_sqrt"}.›
lemma radical_sqrt_rule_power3:
"x ∈ radical_sqrt ⟹ x ≥ 0 ⟹ x^3 ∈ radical_sqrt"
by (metis power3_eq_cube radical_sqrt.intros(5))
subsection ‹Introduction of the datatype expr which represents radical expressions›
text ‹An expression expr is either a rational constant: Const or the
negation of an expression or the inverse of an expression or the
addition of two expressions or the multiplication of two expressions
or the square root of an expression.›