Theory Pi_to_M3_rat
theory Pi_to_M3_rat
imports Pi_Relations J3_Relations M3_Polynomial
begin
subsection ‹Relation between $M_3$ and $\Pi$›
ML‹
Theory.setup (
Method.setup \<^binding>‹unfold_auto› (Attrib.thms >>
(fn thms => fn ctxt =>
SIMPLE_METHOD (
REPEAT1 (
CHANGED_PROP (
(TRY (Clasimp.auto_tac ctxt)) THEN
Local_Defs.unfold_tac ctxt thms THEN
(TRY (Clasimp.auto_tac ctxt))
)
)
)
)
) "repeated unfold and auto"
)
›
locale matiyasevich_polynomial = section5
begin
type_synonym τ=real
definition x' :: "τ mpoly" where "x' ≡ of_int_mpoly x"
definition 𝒜⇩1' :: "τ mpoly" where "𝒜⇩1' ≡ of_int_mpoly 𝒜⇩1"
definition 𝒜⇩2' :: "τ mpoly" where "𝒜⇩2' ≡ of_int_mpoly 𝒜⇩2"
definition 𝒜⇩3' :: "τ mpoly" where "𝒜⇩3' ≡ of_int_mpoly 𝒜⇩3"
definition 𝒳⇩3' :: "τ mpoly" where "𝒳⇩3' ≡ of_int_mpoly 𝒳⇩3"
definition 𝒮' :: "τ mpoly" where "𝒮' ≡ of_int_mpoly 𝒮"
definition 𝒯' :: "τ mpoly" where "𝒯' ≡ of_int_mpoly 𝒯"
definition ℛ' :: "τ mpoly" where "ℛ' ≡ of_int_mpoly ℛ"
definition ℐ' :: "τ mpoly" where "ℐ' ≡ of_int_mpoly ℐ"
definition 𝒴' :: "τ mpoly" where "𝒴' ≡ of_int_mpoly 𝒴"
definition 𝒵' :: "τ mpoly" where "𝒵' ≡ of_int_mpoly ℨ"
definition 𝒥' :: "τ mpoly" where "𝒥' ≡ of_int_mpoly 𝒥"
definition 𝗇' :: "τ mpoly" where "𝗇' ≡ of_int_mpoly 𝗇"
definition 𝒰' ::"τ mpoly" where "𝒰' = of_int_mpoly 𝒰"
definition 𝒱' ::"τ mpoly" where "𝒱' = of_int_mpoly 𝒱"
definition J3' :: "τ mpoly" where "J3' = of_int_mpoly J3"
definition ψ' :: "nat ⇒ τ mpoly" where "ψ' = of_int_mpoly ∘ ((λ_. 0)(0 := 𝒯^2+𝒮^2*𝗇 -𝒯^2*𝒰- 𝒳⇩3^3*𝒰, 1 := 𝒰^2*𝒜⇩1, 2 := 𝒰^2*𝒜⇩2, 3 := 𝒰^2*𝒜⇩3))"
definition M3_poly' :: "τ mpoly" where "M3_poly' ≡ of_int_mpoly M3_poly"
lemma Pi_equals_M3_rationals:
fixes A⇩1 A⇩2 A⇩3 R S T n :: int
defines "X ≡ X⇩0 π"
defines "I ≡ I⇩0 π"
defines "U ≡ U⇩0 π"
defines "V ≡ V⇩0 π"
defines "φ ≡ (λ_. 0)(0 := Var 0, 1 := Const A⇩1, 2 := Const A⇩2, 3 := Const A⇩3)"
defines "φ' ≡ of_int_mpoly ∘ φ"
defines "ℱ ≡ poly_subst φ J3"
defines "ℱ' ≡ of_int_mpoly ℱ :: τ mpoly"
defines "q ≡ MPoly_Type.degree ℱ 0"
defines "Π ≡ pi_relations.Π ℱ 0"
defines "G_sub ≡ pi_relations.G_sub ℱ 0"
defines "G_sub' ≡ of_int_mpoly ∘ (pi_relations.G_sub ℱ 0)"
defines "ξ ≡ ((λ_. 0)(4 := S, 5 := T, 6:=R, 7:=X^3, 11:=n))"
defines "ξ' ≡ of_int ∘ ξ"
assumes "U ≠ 0"
assumes "q = 8"
assumes F_monom_over_0: "vars ℱ ⊆ {0}"
and F_one_0: "MPoly_Type.coeff ℱ (Abs_poly_mapping (λk. (MPoly_Type.degree ℱ 0 when k = 0))) = 1"
shows "insertion ξ Π = M3 π"
proof -
have U_ev: "insertion ξ 𝒰 = U" unfolding defs U_def U⇩0_def ξ_def power2_eq_square
by auto
have V_ev: "insertion ξ 𝒱 = V" unfolding defs V_def V⇩0_def ξ_def power2_eq_square
by auto
have j_in_sum: "⋀j. j≤q ⟶ of_int (insertion ξ ((G_sub j) * 𝒱^j * 𝒰^(q-j)))
= insertion ξ (G_sub j) * (V/U)^j * U^q"
proof
fix j
assume "j ≤ q"
have "insertion ξ ((G_sub j) * 𝒱^j * 𝒰^(q-j) )
= (insertion ξ ((G_sub j) * 𝒱^j) * (insertion ξ 𝒰^(q-j)))" by auto
also have "... = insertion ξ (G_sub j) * V^j * U^(q-j)"
by (auto simp: U_ev V_ev)
also have "... = insertion ξ (G_sub j) * V^j * U^q / U^j"
using power_diff[of "U" "j" "q"] `U ≠ 0` `j≤ q` apply simp
by (metis (no_types, lifting) of_int_0_eq_iff of_int_power power_diff times_divide_eq_right)
also have "... = insertion ξ (G_sub j) * (V/U)^j * U^q"
using power_divide[of "V" "U" "j"] by auto
finally show "insertion ξ ((G_sub j) * 𝒱^j * 𝒰^(q-j)) = insertion ξ (G_sub j) * (V/U)^j * U^q"
by auto
qed
have XI3: "I = X^3"
unfolding I_def I⇩0_def X_def by simp
interpret pi_relations: pi_relations ℱ 0
using F_monom_over_0 F_one_0
by (unfold_locales; auto)
have X1_unfold:"(of_int_mpoly (Const 1 + 𝒜⇩1⇧2 + 𝒜⇩2⇧2 + 𝒜⇩3⇧2))
= (of_int_mpoly (Const 1) + (of_int_mpoly 𝒜⇩1)⇧2 + (of_int_mpoly 𝒜⇩2)⇧2 + (of_int_mpoly 𝒜⇩3)⇧2)"
unfolding of_int_mpoly_simps ..
have aux0: "(λx. insertion ((λ_. 0)(0 := real_of_int V / real_of_int U - real_of_int I - (real_of_int T)⇧2))
(of_int_mpoly (((λ_. 0)(0 := Var 0, Suc 0 := Const A⇩1, 2 := Const A⇩2, 3 := Const A⇩3)) x))) i
= ((λ_. 0)(0 := real_of_int V / real_of_int U - real_of_int I - (real_of_int T)⇧2,
Suc 0 := real_of_int A⇩1, 2 := real_of_int A⇩2, 3 := real_of_int A⇩3)) i" for i
apply (cases "i = 0")
by (auto simp: of_int_mpoly_simps)
have G_sub_vars: "vars (G_sub j) ⊆ {5, 7}" for j
unfolding G_sub_def pi_relations.G_sub_def ℐ_def 𝒯_def
defs diff_conv_add_uminus
apply (rule subset_trans[OF vars_setsum]; simp)
apply (rule UN_least)
unfolding power2_eq_square of_int_Const of_nat_Const diff_conv_add_uminus
by mpoly_vars
have G_sub_aux0: "insertion ξ (G_sub j)
= insertion ((λ_. 0)(5 := T, 7 := X ^ 3)) (G_sub j)" for j
unfolding ξ_def
apply (rule insertion_irrelevant_vars)
using G_sub_vars[of j] by auto
{
fix j
have "real_of_int (insertion ((λ_. 0)(5 := T, 7 := X ^ 3)) (local.pi_relations.G_sub j))
= insertion (of_int ∘ ((λ_. 0)(5 := T, 7 := X ^ 3))) (of_int_mpoly (G_sub j))"
unfolding G_sub_def[symmetric] insertion_of_int_mpoly ..
also have "... = insertion
((λx. real_of_int (((λ_. 0)(5 := T, 7 := X ^ 3)) x))(8 := real_of_int V / real_of_int U))
(of_int_mpoly (G_sub j))"
apply (intro insertion_irrelevant_vars)
using vars_of_int_mpoly[of "G_sub j"] G_sub_vars[of j] by auto
also have "...
= insertion ((λx. real_of_int
(((λ_. 0)(5 := T, 7 := X ^ 3)) x))(8 := real_of_int V / real_of_int U))
(of_int_mpoly (local.pi_relations.G_sub j))"
unfolding G_sub_def[symmetric] ..
finally have G_sub_aux1: "real_of_int (insertion ((λ_. 0)(5 := T, 7 := X ^ 3)) (local.pi_relations.G_sub j))
= insertion ((λx. real_of_int (((λ_. 0)(5 := T, 7 := X ^ 3)) x))(8 := real_of_int V / real_of_int U))
(of_int_mpoly (local.pi_relations.G_sub j))" .
}
note G_sub_aux1 = this
have degree_aux_lt: "MPoly_Type.degree ℱ' 0 ≤ q"
unfolding q_def ℱ'_def
by (simp add: le_funD)
have vars_ℱ': "vars ℱ' ⊆ {0}"
unfolding ℱ'_def
apply (rule subset_trans[OF vars_of_int_mpoly])
by (auto simp add: F_monom_over_0)
have coeff_ℱ': "MPoly_Type.coeff ℱ' = MPoly_Type.coeff ℱ"
unfolding ℱ'_def of_int_mpoly_coeff ..
have degree_aux_gt: "MPoly_Type.degree ℱ' 0 ≥ q"
proof -
have "MPoly_Type.coeff ℱ' (Abs_poly_mapping (λk. (q when k = 0))) = 1"
using F_one_0 coeff_ℱ' q_def by simp
thus ?thesis
unfolding MPoly_Type.degree.rep_eq apply (intro Max_ge)
subgoal by simp
apply (rule insertI2)
unfolding keys.rep_eq image_iff bex_simps(6) coeff_def
apply (rule exI[of _ "Poly_Mapping.single 0 q"])
by (auto simp: Poly_Mapping.single.abs_eq when_def)
qed
have degree_aux: "MPoly_Type.degree ℱ' 0 = q"
using degree_aux_lt degree_aux_gt by simp
have univariate_expansion:
"ℱ' = (∑d = 0..MPoly_Type.degree ℱ' 0. of_int (pi_relations.coeff_F d) * (Var 0) ^ d)"
apply (subst mpoly_univariate_expansion_sum[of ℱ' 0, OF vars_ℱ'])
apply (rule sum.cong, simp)
unfolding pi_relations.coeff_F_def Poly_Mapping.single.abs_eq coeff_ℱ' of_int_general_Const
by (simp add: of_int_mpoly_simps)
have X_unfold:"X = insertion
((λ_. 0)
(0 := real_of_int V / real_of_int U - real_of_int I - (real_of_int T)⇧2,
Suc 0 := real_of_int A⇩1, 2 := real_of_int A⇩2, 3 := real_of_int A⇩3)) 𝒳⇩3'"
unfolding x'_def 𝒜⇩1'_def 𝒜⇩2'_def 𝒜⇩3'_def 𝒳⇩3'_def x_def 𝒜⇩1_def 𝒜⇩2_def 𝒜⇩3_def 𝒳⇩3_def X_def X⇩0_def X1_unfold of_int_mpoly_simps
by simp
have U_V_cancel: "of_int U * (of_int V/of_int U) = (of_int V :: real)"
by (simp add: ‹U ≠ 0›)
have "insertion ξ Π = insertion ξ (∑j=0..q. G_sub j * 𝒱^j * 𝒰^(q-j))"
unfolding Π_def pi_relations.Π_def
unfolding q_def pi_relations.q_def
unfolding G_sub_def pi_relations.G_sub_def
unfolding defs
by (auto simp: algebra_simps)
also have "... = (∑j=0..q. insertion ξ ((G_sub j) * 𝒱^j * 𝒰^(q-j)))"
by auto
also have "of_int (...) = (∑j=0..q. insertion ξ (G_sub j) * (V/U)^j * U^q)"
apply (subst of_int_sum)
apply (rule sum.cong)
using j_in_sum by auto
also have "... = U^q * (∑j=0..q. insertion ξ (G_sub j) * (V/U)^j)"
apply (subst sum_distrib_left)
by (simp add: algebra_simps)
also have "... = U^q * insertion ((λ_. 0)(5:=T, 7:=I, 8:=V/U)) (of_int_mpoly (pi_relations.G))"
unfolding pi_relations.G_in_Y G_sub_aux0
apply (simp only: of_int_mpoly_simps 𝒴_def G_sub_def)
using insertion_of_int_mpoly[where ?P = "local.pi_relations.G_sub _"
and ?α = "((λ_. 0)(4 := S, 5 := T, 6 := R, 7 := X ^ 3, 11 := n))"]
apply (subst insertion_simps)
subgoal by simp
unfolding q_def pi_relations.q_def comp_def of_int_mpoly_simps ‹I = X^3›
apply (subst insertion_simps)+
unfolding G_sub_aux1
by (simp add: mult.commute)
also have "... = U^q * insertion ((λ_. 0)(0:=of_int V/of_int U - of_int I - of_int T^2)) ℱ'"
unfolding pi_relations.G_def
apply (subst univariate_expansion)
apply (simp add: defs of_int_mpoly_simps pi_relations.q_def pi_relations.coeff_F_def)
apply (rule disjI2)
apply (rule sum.cong)
subgoal by (simp add: degree_aux q_def)
unfolding of_int_Const of_int_mpoly_Const
apply (simp only: insertion_simps)
unfolding of_int_general_Const of_int_mpoly_Const
by simp
also have "... = U^q * insertion ((λ_. 0)(0:=of_int V/of_int U - of_int I - of_int T^2,
1:=of_int A⇩1, 2:=of_int A⇩2, 3:=of_int A⇩3)) J3'"
unfolding ℱ'_def ℱ_def J3'_def φ_def
apply simp
unfolding of_int_mpoly_poly_subst
unfolding insertion_poly_subst comp_def
apply (subst aux0)
by simp
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U) * (
4
* (of_int V - (of_int U) * of_int I - (of_int U) * of_int T^2)
* (
((of_int V - (of_int U) * of_int I - (of_int U) * of_int T^2))^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
- 8
* (of_int U)^2
* (of_int V - (of_int U) * of_int I - (of_int U) * of_int T^2)
* A⇩2
* X^2
))^2
)
"
proof -
have "
... =
(of_int U)^8 * (
(
(
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2 - A⇩3 * X^4
)^2
+ 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩1
- 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩2 * X^2
- 4 * A⇩1 * A⇩2 * X^2
)^2
- A⇩1 * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
)^2
)
"
by (unfold_auto ‹q = 8› J3'_def x'_def 𝒜⇩1'_def 𝒜⇩2'_def 𝒜⇩3'_def 𝒳⇩3'_def J3_def x_def 𝒜⇩1_def
𝒜⇩2_def 𝒜⇩3_def 𝒳⇩3_def X_unfold insertion_simps of_int_mpoly_simps)
also have "
... =
(((of_int U)^4)^2) * (
(
(
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)^2
+ 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩1
- 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩2 * X^2
- 4 * A⇩1 * A⇩2 * X^2
)^2
- A⇩1 * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
)^2
)
"
by simp
also have "
... =
(
((((of_int U)^4)^2) * (
(
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)^2
+ 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩1
- 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩2 * X^2
- 4 * A⇩1 * A⇩2 * X^2
)^2)
- (of_int U)^8 * (A⇩1 * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
)^2)
)
"
unfolding right_diff_distrib by simp
also have "
... =
(
((((of_int U)^4)^2) * (
(
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)^2
+ 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩1
- 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩2 * X^2
- 4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * (((of_int U)^4) * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
))^2
)
"
unfolding power_mult_distrib by simp
also have "
... =
(
((((of_int U)^4) * (
(
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)^2
+ 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩1
- 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩2 * X^2
- 4 * A⇩1 * A⇩2 * X^2
))^2)
- A⇩1 * (((of_int U)^4) * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
))^2
)
"
unfolding power_mult_distrib by simp
also have "
... =
(
((
((of_int U)^2^2) * (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)^2
+ ((of_int U)^4) * 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩1
- ((of_int U)^4) * 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩2 * X^2
- ((of_int U)^4) * 4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * (((of_int U)^4) * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
))^2
)
"
unfolding distrib_left right_diff_distrib mult.assoc by simp
also have "
... =
(
((
(
(of_int U)^2 * (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
)^2
+ ((of_int U)^4) * 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩1
- ((of_int U)^4) * 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩2 * X^2
- ((of_int U)^4) * 4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * (((of_int U)^4) * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
))^2
)
"
unfolding power_mult_distrib by simp
also have "
... =
(
((
(
(
(of_int U)^2 * (of_int V/of_int U - of_int I - of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ ((of_int U)^4) * 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩1
- ((of_int U)^4) * 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩2 * X^2
- ((of_int U)^4) * 4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * (((of_int U)^4) * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
))^2
)
"
unfolding distrib_left right_diff_distrib mult.assoc by simp
also have "
... =
(
((
(
(
((of_int U) * (of_int V/of_int U - of_int I - of_int T^2))^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ ((of_int U)^4) * 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩1
- ((of_int U)^4) * 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩2 * X^2
- ((of_int U)^4) * 4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * (((of_int U)^4) * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
))^2
)
"
unfolding power_mult_distrib by simp
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ ((of_int U)^4) * 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩1
- ((of_int U)^4) * 4 * (of_int V/of_int U - of_int I - of_int T^2)^2 * A⇩2 * X^2
- ((of_int U)^4) * 4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * (((of_int U)^4) * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
))^2
)
"
unfolding distrib_left right_diff_distrib U_V_cancel by simp
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int U)^2 * (of_int V/of_int U - of_int I - of_int T^2)^2) * A⇩1
- 4 * (of_int U)^2 * ((of_int U)^2 * (of_int V/of_int U - of_int I - of_int T^2)^2) * A⇩2 * X^2
- 4 * ((of_int U)^4) * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * (((of_int U)^4) * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
))^2
)
"
unfolding ab_semigroup_mult_class.mult.commute[of 4] mult.assoc by simp
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int U) * (of_int V/of_int U - of_int I - of_int T^2))^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int U) * (of_int V/of_int U - of_int I - of_int T^2))^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U)^4 * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
))^2
)
"
unfolding power_mult_distrib ..
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U)^4 * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
))^2
)
"
unfolding distrib_left right_diff_distrib U_V_cancel by simp
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U) * ((of_int U)^3 * (
4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
)))^2
)
"
unfolding power_def mult.assoc by simp
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U) * (
(of_int U)^3
* (4
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
))
- (of_int U)^3 * (8 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2)
))^2
)
"
unfolding right_diff_distrib ..
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U) * (
4
* (of_int U)^3
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8 * (of_int U)^3 * (of_int V/of_int U - of_int I - of_int T^2) * A⇩2 * X^2
))^2
)
"
unfolding ab_semigroup_mult_class.mult.commute[of 4] ab_semigroup_mult_class.mult.commute[of 8] mult.assoc by simp
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U) * (
4
* (of_int U)
* (of_int U)^2
* (of_int V/of_int U - of_int I - of_int T^2)
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
)
- 8
* (of_int U)^2
* (of_int U) * (of_int V/of_int U - of_int I - of_int T^2)
* A⇩2
* X^2
))^2
)
"
unfolding power2_eq_square power3_eq_cube mult.assoc ..
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U) * (
4
* ((of_int U)
* (of_int V/of_int U - of_int I - of_int T^2))
* ((of_int U)^2
* (
(of_int V/of_int U - of_int I - of_int T^2)^2
+ A⇩1
+ A⇩2 * X^2
- A⇩3 * X^4
))
- 8
* (of_int U)^2 * (of_int U)
* (of_int V/of_int U - of_int I - of_int T^2)
* A⇩2
* X^2
))^2
)
"
unfolding ab_semigroup_mult_class.mult.commute[of "(of_int U)^2"] mult.assoc by simp
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U) * (
4
* ((of_int U) * (of_int V/of_int U) - (of_int U) * of_int I - (of_int U) * of_int T^2)
* (
(of_int U)^2 * (of_int V/of_int U - of_int I - of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
- 8
* (of_int U)^2
* ((of_int U) * (of_int V/of_int U - of_int I - of_int T^2))
* A⇩2
* X^2
))^2
)
"
unfolding distrib_left right_diff_distrib mult.assoc by simp
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U) * (
4
* ((of_int U) * (of_int V/of_int U) - (of_int U) * of_int I - (of_int U) * of_int T^2)
* (
((of_int U) * (of_int V/of_int U - of_int I - of_int T^2))^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
- 8
* (of_int U)^2
* ((of_int U) * (of_int V/of_int U - of_int I - of_int T^2))
* A⇩2
* X^2
))^2
)
"
unfolding power_mult_distrib ..
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U) * (
4
* ((of_int U) * (of_int V/of_int U) - (of_int U) * of_int I - (of_int U) * of_int T^2)
* (
(((of_int U) * (of_int V/of_int U) - (of_int U) * of_int I - (of_int U) * of_int T^2))^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
- 8
* (of_int U)^2
* ((of_int U) * (of_int V/of_int U) - (of_int U) * of_int I - (of_int U) * of_int T^2)
* A⇩2
* X^2
))^2
)
"
unfolding distrib_left right_diff_distrib ..
also have "
... =
(
((
(
(
(of_int V - of_int U * of_int I - of_int U * of_int T^2)^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
)^2
+ 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩1
- 4 * (of_int U)^2 * ((of_int V) - (of_int U) * of_int I - (of_int U) * of_int T^2)^2 * A⇩2 * X^2
- 4 * (of_int U)^4 * A⇩1 * A⇩2 * X^2
)^2)
- A⇩1 * ((of_int U) * (
4
* (of_int V - (of_int U) * of_int I - (of_int U) * of_int T^2)
* (
((of_int V - (of_int U) * of_int I - (of_int U) * of_int T^2))^2
+ (of_int U)^2 * A⇩1
+ (of_int U)^2 * A⇩2 * X^2
- (of_int U)^2 * A⇩3 * X^4
)
- 8
* (of_int U)^2
* (of_int V - (of_int U) * of_int I - (of_int U) * of_int T^2)
* A⇩2
* X^2
))^2
)
"
unfolding U_V_cancel by simp
finally show ?thesis .
qed
also have "... = M3 π" unfolding M3_def X_def I_def U_def V_def by auto
finally show "insertion ξ Π = M3 π" by auto
qed
end
end