Theory Computations
section‹Computations: This section can be skipped›
theory Computations
imports Kauffman_Matrix
begin
lemma unlink_computation:
"rat_poly_plus (rat_poly_times (rat_poly_times A A) (rat_poly_times A A))
(rat_poly_plus
(rat_poly_times 2 (rat_poly_times A (rat_poly_times A (rat_poly_times B B))))
(rat_poly_times (rat_poly_times B B) (rat_poly_times B B))) =
((A^4)+(B^4)+2)"
proof-
have "(rat_poly_times (rat_poly_times A A) (rat_poly_times A A)) = A^4"
by (simp add: numeral_Bit0)
moreover have "(rat_poly_times (rat_poly_times B B) (rat_poly_times B B))
= B^4"
by (simp add: numeral_Bit0)
moreover have "(rat_poly_times 2 (rat_poly_times A (rat_poly_times A (rat_poly_times B B))))
= 2"
using inverse1 by (metis mult_2_right one_add_one rat_poly.assoc rat_poly.comm)
ultimately show ?thesis by auto
qed
lemma computation_swingpos:
" rat_poly_plus (rat_poly_times B (rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) B))
(rat_poly_times (A - rat_poly_times (rat_poly_times B B) B)
(rat_poly_times A (A - rat_poly_times (rat_poly_times B B) B))) =
rat_poly_times A (rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) A)" (is "?l = ?r")
proof-
have 1:"(A - rat_poly_times (rat_poly_times B B) B)
= A - (B^3)"
by (metis power3_eq_cube)
then have 2:"(rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) B)
= A*B - (B^3)*B"
by (metis minus_right_distributivity)
then have "... = 1 - (B^4)"
by (simp add: inverse1 numeral_Bit0 power3_eq_cube)
then have "(rat_poly_times B (rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) B))
= B - (B^4)*B"
using 2
by (metis minus_right_distributivity mult.commute mult.right_neutral)
then have 3:"(rat_poly_times B (rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) B))
= B - (B^5)"
by (metis (no_types, lifting) inverse1 minus_right_distributivity
mult.left_commute mult.right_neutral power2_eq_square power_numeral_odd)
have "(rat_poly_times (A - rat_poly_times (rat_poly_times B B) B)
(rat_poly_times A (A - rat_poly_times (rat_poly_times B B) B)))
= (A - (B^3))*(A*( A - (B^3)))"
using 1 by auto
moreover then have "... = (A - (B^3))*(A*A - (A*(B^3)))"
by (metis minus_left_distributivity)
moreover then have "... = (A - (B^3))*(A*A - (B^2))"
using inverse1
by (simp add: power2_eq_square power3_eq_cube)
moreover then have "... = A*(A*A - (B^2)) - (B^3)*(A*A - (B^2))"
by (metis minus_right_distributivity)
moreover then have "... = ((A^3) - B) - B + (B^5)"
proof-
have "A*(A*A - (B^2)) = (A*A*A - A*(B^2))"
by (simp add: right_diff_distrib)
moreover have "... = (A*A*A - A*(B*B))"
by (metis power2_eq_square)
moreover have "... = ((A^3) - ((A::rat_poly)*B)*B)"
by (simp add: power3_eq_cube)
moreover have "... = ((A^3) - ((1::rat_poly)*B))"
by (metis inverse1)
moreover have "... = (A^3) - B"
by auto
ultimately have s1:"(A::rat_poly)*(A*A - (B^2)) = (A^3) - (B::rat_poly)"
by metis
have s2:"((B::rat_poly)^3)*(A*A - (B^2)) = (B^3)*(A*A) - (B^(3::nat))*(B^2)"
by (metis minus_left_distributivity power3_eq_cube)
moreover then have "... = (((B::rat_poly)^3)*(A*A) - (B^5))"
using power_add
proof-
have "(B^(3::nat))*(B^2) = (B^5)"
by (metis One_nat_def Suc_1 numeral_3_eq_3 power_Suc power_numeral_odd)
then show ?thesis using s2 by auto
qed
moreover then have "... = ((((B::rat_poly)*B*B)*(A*A)) - (B^5))"
by (metis power3_eq_cube)
moreover then have "... = ((((B::rat_poly)*(B*(B*A)*A))) - (B^5))"
by auto
moreover then have "... = ((((B::rat_poly)*(B*(1)*A))) - (B^5))"
using inverse2 by auto
moreover then have "... = ((((B::rat_poly)*(B*A))) - (B^5))"
by auto
moreover then have "... = ((((B::rat_poly))) - (B^5))"
using inverse2
by simp
ultimately have "((B::rat_poly)^3)*(A*A - (B^2)) = ((B::rat_poly) - (B^5))"
by auto
then have "A*(A*A - (B^2)) - (B^3)*(A*A - (B^2))
= (A^3) - (B::rat_poly) - ((B::rat_poly) - (B^5))"
using s1 by auto
then show ?thesis by auto
qed
ultimately have "(rat_poly_times (A - rat_poly_times (rat_poly_times B B) B)
(rat_poly_times A (A - rat_poly_times (rat_poly_times B B) B)))
= ((A^3) - B) - B + (B^5)"
by auto
then have "?l = B - (B^5) + ((A^3) - B) - B + (B^5)"
using 3 by auto
then have 4:"?l = (A^3) - B"
by auto
have "?r = A*((A - rat_poly_times (rat_poly_times B B) B)*A)"
by auto
moreover then have "... = A*(A - (B^3))*A"
using 1 by auto
moreover have "... = A*(A*A - (B^3)*A)"
by (simp add: minus_left_distributivity mult.commute)
moreover have "... = A*(A*A - (B*B*B)*A)"
by (metis power3_eq_cube)
moreover have "... = A*(A*A - (B*B*(B*A)))"
by auto
moreover have "... = A*(A*A - B*B)"
using inverse2 minus_left_distributivity by auto
moreover have "... = A*A*A - A*(B*B)"
by (metis minus_left_distributivity rat_poly.comm)
moreover have "... = A^3 - (A*B)*B"
by (metis ab_semigroup_mult_class.mult_ac(1) power3_eq_cube)
moreover have "... = A^3 - B"
using inverse1 by (metis monoid_mult_class.mult.left_neutral)
ultimately have "?r = A^3 - B"
by auto
then show ?thesis using 4 by auto
qed
lemma computation2:
" rat_poly_plus (rat_poly_times A (rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) A))
(rat_poly_times (B - rat_poly_times (rat_poly_times A A) A)
(rat_poly_times B (B - rat_poly_times (rat_poly_times A A) A))) =
rat_poly_times B (rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) B)" (is "?l = ?r")
proof-
have 1:"(B - rat_poly_times (rat_poly_times A A) A)
= B - (A^3)"
by (metis power3_eq_cube)
then have 2:"(rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) A)
= B*A - (A^3)*A"
by (metis minus_right_distributivity)
then have "... = 1 - (A^4)"
using inverse2
by (metis mult.commute one_plus_numeral power_add power_one_right semiring_norm(2)
semiring_norm(4))
then have "(rat_poly_times A (rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) A))
= A - (A^4)*A"
using 2
by (simp add: minus_left_distributivity)
then have 3:"(rat_poly_times A (rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) A))
= A - (A^5)"
by (simp add: numeral_Bit0 numeral_Bit1)
have "(rat_poly_times (B - rat_poly_times (rat_poly_times A A) A)
(rat_poly_times B (B - rat_poly_times (rat_poly_times A A) A)))
= (B - (A^3))*(B*( B - (A^3)))"
using 1 by auto
moreover then have "... = (B - (A^3))*(B*B - (B*(A^3)))"
by (metis minus_left_distributivity)
moreover then have "... = (B - (A^3))*(B*B - (A^2))"
using inverse2
by (simp add: power2_eq_square power3_eq_cube)
moreover then have "... = B*(B*B - (A^2)) - (A^3)*(B*B - (A^2))"
by (metis minus_right_distributivity)
moreover then have "... = ((B^3) - A) - A + (A^5)"
proof-
have "B*(B*B - (A^2)) = (B*B*B - B*(A^2))"
by (simp add: right_diff_distrib)
moreover have "... = (B*B*B - B*(A*A))"
by (metis power2_eq_square)
moreover have "... = ((B^3) - ((B::rat_poly)*A)*A)"
by (simp add: power3_eq_cube)
moreover have "... = ((B^3) - ((1::rat_poly)*A))"
by (metis inverse2)
moreover have "... = (B^3) - A"
by auto
ultimately have s1:"(B::rat_poly)*(B*B - (A^2)) = (B^3) - (A::rat_poly)"
by metis
have s2:"((A::rat_poly)^3)*(B*B - (A^2)) = (A^3)*(B*B) - (A^(3::nat))*(A^2)"
by (metis minus_left_distributivity power3_eq_cube)
moreover then have "... = (((A::rat_poly)^3)*(B*B) - (A^5))"
using power_add
proof-
have "(A^(3::nat))*(A^2) = A^5"
by (metis One_nat_def Suc_1 numeral_3_eq_3 power_Suc power_numeral_odd)
then show ?thesis using s2 by auto
qed
moreover then have "... = ((((A::rat_poly)*A*A)*(B*B)) - (A^5))"
by (metis power3_eq_cube)
moreover then have "... = ((((A::rat_poly)*(A*(A*B)*B))) - (A^5))"
by auto
moreover then have "... = ((((A::rat_poly)*(A*(1)*B))) - (A^5))"
using inverse1 by auto
moreover then have "... = ((((A::rat_poly)*(A*B))) - (A^5))"
by auto
moreover then have "... = ((((A::rat_poly))) - (A^5))"
using inverse1 by auto
ultimately have "((A::rat_poly)^3)*(B*B - (A^2)) = ((A::rat_poly) - (A^5))"
by auto
then have "B*(B*B - (A^2)) - (A^3)*(B*B - (A^2))
= (B^3) - (A::rat_poly) - ((A::rat_poly) - (A^5))"
using s1 by auto
then show ?thesis by auto
qed
ultimately have "(rat_poly_times (B - rat_poly_times (rat_poly_times A A) A)
(rat_poly_times B (B - rat_poly_times (rat_poly_times A A) A)))
= ((B^3) - A) - A + (A^5)"
by auto
then have "?l = A - (A^5) + ((B^3) - A) - A + (A^5)"
using 3 by auto
then have 4:"?l = (B^3) - A"
by auto
have "?r = B*((B - rat_poly_times (rat_poly_times A A) A)*B)"
by auto
moreover then have "... = B*(B - (A^3))*B"
using 1 by auto
moreover have "... = B*(B*B - (A^3)*B)"
using minus_left_distributivity by (simp add: minus_left_distributivity mult.commute)
moreover have "... = B*(B*B - (A*A*A)*B)"
by (metis power3_eq_cube)
moreover have "... = B*(B*B - (A*A*(A*B)))"
by auto
moreover have "... = B*(B*B - A*A)"
using inverse1 by auto
moreover have "... = B*B*B - B*(A*A)"
by (metis minus_left_distributivity rat_poly.comm)
moreover have "... = B^3 - (B*A)*A"
by (metis ab_semigroup_mult_class.mult_ac(1) power3_eq_cube)
moreover have "... = B^3 - A"
using inverse2 by (metis monoid_mult_class.mult.left_neutral)
ultimately have "?r = B^3 - A"
by auto
then show ?thesis using 4 by auto
qed
lemma computation_swingneg:"rat_poly_times B (rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) B) =
rat_poly_plus
(rat_poly_times (B - rat_poly_times (rat_poly_times A A) A)
(rat_poly_times B (B - rat_poly_times (rat_poly_times A A) A)))
(rat_poly_times A (rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) A))"
using computation2 by auto
lemma computation_toppos:"rat_poly_inv (rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) A) =
rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) B"(is "?l = ?r")
proof-
have "(rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) A)
= ((A - ((B*B)*B))*A)"
by auto
moreover then have "... = (A*A) - ((B*B)*B)*A"
by (metis minus_left_distributivity rat_poly.comm)
moreover then have "... = (A*A) - (B*B)*(B*A)"
by auto
moreover then have "... = (A*A) - (B*B)"
using inverse2 by auto
ultimately have "?l = rat_poly_inv ((A*A) - (B*B))"
by auto
then have 1:"?l = (B*B) - (A*A)"
by auto
have "?r =(B - ((A*A) *A))*B"
by auto
moreover have "... = B*B - ((A*A)*A)*B"
by (metis minus_left_distributivity rat_poly.comm)
moreover have "... = (B*B) - ((A*A)*(A*B))"
by auto
moreover have "... = ((B::rat_poly)*B) - (A*A)"
using inverse1 by auto
ultimately have "?r = (B*B) - (A*A)"
by auto
then show ?thesis using 1 by auto
qed
lemma computation_downpos_prelim:
"rat_poly_inv (rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) B) =
rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) A"(is "?l = ?r")
proof-
have "(rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) B)
= ((B - ((A*A)*A))*B)"
by auto
moreover then have "... = (B*B) - ((A*A)*A)*B"
by (metis minus_left_distributivity rat_poly.comm)
moreover then have "... = (B*B) - (A*A)*(A*B)"
by auto
moreover then have "... = (B*B) - (A*A)"
using inverse1 by auto
ultimately have "?l = rat_poly_inv ((B*B) - (A*A))"
by auto
then have 1:"?l = (A*A) - (B*B)"
by auto
have "?r =(A - ((B*B) *B))*A"
by auto
moreover have "... = A*A - ((B*B)*B)*A"
by (metis minus_left_distributivity rat_poly.comm)
moreover have "... = (A*A) - ((B*B)*(B*A))"
by auto
moreover have "... = ((A::rat_poly)*A) - (B*B)"
using inverse2 by auto
ultimately have "?r = (A*A) - (B*B)"
by auto
then show ?thesis using 1 by auto
qed
lemma computation_downpos:"rat_poly_times A (A - rat_poly_times (rat_poly_times B B) B) =
rat_poly_inv (rat_poly_times B (B - rat_poly_times (rat_poly_times A A) A))"
using computation_downpos_prelim by (metis rat_poly.comm)
lemma computatition_positive_flip:"rat_poly_plus
(rat_poly_inv (rat_poly_times A (rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) A)))
(rat_poly_inv (rat_poly_times B (rat_poly_times A B))) =
rat_poly_inv (rat_poly_times A (rat_poly_times A A))" (is "?l = ?r")
proof-
have "(rat_poly_inv (rat_poly_times B (rat_poly_times A B)))
= (rat_poly_inv (rat_poly_times B 1))"
using inverse1 by auto
moreover have "... = - B"
by auto
ultimately have 1:"(rat_poly_inv (rat_poly_times B (rat_poly_times A B))) = - B"
by auto
have " (rat_poly_times A (rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) A))
= A*((A - ((B*B)*B))*A)"
by auto
moreover then have "... = A*((A*A) - ((B*B)*B*A))"
by (metis minus_left_distributivity rat_poly.comm)
moreover then have "... = A*((A*A) - ((B*B)*1))"
using inverse2 by auto
moreover then have "... = A*((A*A) - (B*B))"
by auto
moreover then have "... = A*(A*A) - (A*(B*B))"
by (metis minus_left_distributivity)
moreover then have "... = (A*(A*A)) - (1*B)"
using inverse1 by auto
moreover then have "... = (A*(A*A)) - B"
by auto
ultimately have "(rat_poly_times A (rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) A))
= (A*(A*A)) - B"
by auto
then have "rat_poly_inv (rat_poly_times A (rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) A))
= B - (A*A*A)"
by auto
then have 3:"?l = - (A*A*A)"
using 1 by auto
moreover have "?r = - (A*A*A)"
by auto
ultimately show ?thesis by auto
qed
lemma computation_negative_flip:"rat_poly_plus
(rat_poly_inv (rat_poly_times B (rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) B)))
(rat_poly_inv (rat_poly_times A (rat_poly_times B A))) =
rat_poly_inv (rat_poly_times B (rat_poly_times B B))" (is "?l = ?r")
proof-
have "(rat_poly_inv (rat_poly_times A (rat_poly_times B A)))
= (rat_poly_inv (rat_poly_times A 1))"
using inverse2 by auto
moreover have "... = - A"
by auto
ultimately have 1:"(rat_poly_inv (rat_poly_times A (rat_poly_times B A))) = - A"
by auto
have " (rat_poly_times B (rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) B))
= B*((B - ((A*A)*A))*B)"
by auto
moreover then have "... = B*((B*B) - ((A*A)*A*B))"
by (metis minus_left_distributivity rat_poly.comm)
moreover then have "... = B*((B*B) - ((A*A)*1))"
using inverse1 by auto
moreover then have "... = B*((B*B) - (A*A))"
by auto
moreover then have "... = B*(B*B) - (B*(A*A))"
by (metis minus_left_distributivity)
moreover then have "... = (B*(B*B)) - (1*A)"
using inverse2 by auto
moreover then have "... = (B*(B*B)) - A"
by auto
ultimately have "(rat_poly_times B (rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) B))
= (B*(B*B)) - A"
by auto
then have "rat_poly_inv (rat_poly_times B (rat_poly_times (B - rat_poly_times (rat_poly_times A A) A) B))
= A - (B*B*B)"
by auto
then have 3:"?l = - (B*B*B)"
using 1 by auto
moreover have "?r = - (B*B*B)"
by auto
ultimately show ?thesis by auto
qed
lemma computation_pull_pos_neg:
"rat_poly_plus (rat_poly_times B (B - rat_poly_times (rat_poly_times A A) A))
(rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) A) = 0"
proof-
have " rat_poly_times (rat_poly_times A A) A
= ((A*A)*A)"
by auto
then have "rat_poly_times B (B - rat_poly_times (rat_poly_times A A) A)
= B*B - B*((A*A)*A)"
using minus_left_distributivity by auto
moreover have "... = B*B - (B*(A*(A*A)))"
by auto
moreover have "... = B*B - ((B*A)*(A*A))"
by auto
moreover have "... = B*B - A*A"
using inverse2 by auto
ultimately have 1:"rat_poly_times B (B - rat_poly_times (rat_poly_times A A) A)
= B*B - A*A"
by auto
have "rat_poly_times (rat_poly_times B B) B = (B*B)*B"
by auto
then have "(rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) A)
= (A*A) - ((B*B)*B)*A"
using minus_right_distributivity by auto
moreover have "... = (A*A) - ((B*B)*(B*A))"
by auto
moreover have "... = (A*A) - (B*B)"
using inverse2 by auto
ultimately have 2:"(rat_poly_times (A - rat_poly_times (rat_poly_times B B) B) A)
= (A*A) - (B*B)"
by auto
have "B*B - A*A + (A*A) - (B*B) = 0"
by auto
with 1 2 show ?thesis by auto
qed
lemma aux1:"(A - rat_poly_times (rat_poly_times B B) B)
= A - (B^3)"
using power3_eq_cube by (metis)
lemma square_subtract:"(((p::rat_poly) - (q::rat_poly))^2)
= (p^2) - (2*p*q) + (q^2)"
proof-
have 1:"(((p::rat_poly) - (q::rat_poly))^2)
= (p- q)*(p - q)"
by (metis power2_eq_square)
then have "(p - q)*(p - q) = (p - q)*p - (p - q)*q"
by (metis minus_right_distributivity rat_poly.comm)
moreover have "(p - q)*p = p*p - q*p"
by (metis minus_left_distributivity rat_poly.comm)
moreover have "(p - q)*q = p*q - q*q"
by (metis minus_left_distributivity rat_poly.comm)
ultimately have "(p - q)*(p - q) = p*p - q*p - (p*q - q*q)"
by auto
moreover have "... = (p*p) - q*p - p*q + q*q"
by auto
moreover have "... = (p^2) -p*q - p*q + (q^2)"
using power2_eq_square by (simp add: power2_eq_square)
ultimately show ?thesis using 1 by auto
qed
lemma cube_minus:"∀p q.((((p::rat_poly) - (q::rat_poly))^3)
= (p^3) - 3*(p^2)*(q) + 3*(p)*(q^2) - (q^3))"
apply(rule allI)
apply(rule allI)
proof-
fix p q
have 1:"(((p::rat_poly) - (q::rat_poly))^3) = (p - q)*(p-q)^2"
by (metis One_nat_def Suc_1 numeral_3_eq_3 power_Suc)
then have "(p-q)^2 = (p^2) - (2*p*q) + (q^2)"
using square_subtract by auto
then have 2:"(p - q)*(p-q)^2 = (p - q)*((p^2) - (2*p*q) + (q^2))"
by auto
moreover have 3:"(p - q)*((p^2) - (2*p*q) + (q^2))
= p*((p^2) - (2*p*q) + (q^2))
- (q*((p^2) - (2*p*q) + (q^2)))"
by (metis minus_right_distributivity)
moreover have "p*((p^2) - (2*p*q) + (q^2))
= p*(p^2) - p*(2*p*q) + (p*(q^2))"
using minus_left_distributivity by (simp add: distrib_left)
moreover have "p*(p^2) = p^3"
by (metis One_nat_def Suc_1 numeral_3_eq_3 power_Suc)
moreover have "p*(2*p*q) = 2*(p^2)*q"
by (metis (no_types, lifting) distrib_left mult_2 power2_eq_square
semigroup_mult_class.mult.assoc)
ultimately have 4:"p*((p^2) - (2*p*q) + (q^2))
= (p^3) - (2*(p^2)*q) + (p*(q^2))"
by auto
have "q*((p^2) - (2*p*q) + (q^2))
= q*(p^2) - q*(2*p*q) + (q*(q^2))"
by (simp add: distrib_left minus_left_distributivity)
moreover have "q*(p^2) = (p^2)*q"
by simp
moreover have "q*(2*p*q) = 2*p*(q^2)"
by (simp add: power2_eq_square)
ultimately have 5:"q*((p^2) - (2*p*q) + (q^2))
= (p^2)*q - 2*p*(q^2) + (q^3)"
by (metis One_nat_def Suc_1 numeral_3_eq_3 power_Suc)
with 1 2 3 4 have "(p - q)^3
= (p^3) - (2*(p^2)*q) + (p*(q^2))
- ((p^2)*q - 2*p*(q^2) + (q^3))"
by auto
moreover have "... = (p^3) - (2*(p^2)*q) + (p*(q^2))
- (p^2)*q + 2*p*(q^2) - (q^3)"
by auto
moreover have "... = (p^3) - 3*(p^2)*(q) + 3*(p)*(q^2) - (q^3)"
by auto
ultimately show
"(p - q) ^ 3
= rat_poly_plus (p ^ 3 -
rat_poly_times
(rat_poly_times 3 (p⇧2)) q)
(rat_poly_times (rat_poly_times 3 p) (q⇧2))
- q ^ 3"
by auto
qed
lemma power_mult: "((p::rat_poly)^m)^n= (p)^(m*(n::nat))"
by (metis power_mult)
lemma cube_minus2:
fixes p q
shows "(((p::rat_poly) - (q::rat_poly))^3)
= (p^3) - 3*(p^2)*(q) + 3*(p)*(q^2) - (q^3)"
using cube_minus by auto
lemma subst_poly:assumes "a = b" shows "(p::rat_poly)*a = p*b"
using assms by auto
lemma sub1:
assumes "p*q = 1"
shows "r*(p*q) = r*1"
using assms by metis
lemma n_distrib:"(A^(n::nat))*(B^n) = (A*B)^n"
by (induct n)(auto)
lemma rat_poly_id_pow:"(1::rat_poly)^n = 1"
by (induct n)(auto)
lemma power_prod:"(A^(n::nat))*(B^n) = (1::rat_poly)"
apply(simp add:n_distrib)
apply(simp add:inverse1)
done
lemma "(pCons 0 1) ≠ 0"
by (metis non_zero var_def)
end