Loading theory "Compare_Complex" (required by "Real_Factorization" via "Complex_Algebraic_Numbers") Loading theory "Complex_Roots_Real_Poly" (required by "Real_Factorization" via "Complex_Algebraic_Numbers") instantiation complex :: finite_UNIV finite_UNIV_complex == finite_UNIV :: (complex, bool) phantom instantiation complex :: compare compare_complex == compare :: complex \ complex \ order deriving "ceq" instance for type "Complex.complex" via "=" derived is_ceq_complex-lemma deriving "ceq" instance for type "Real.real" via "=" derived is_ceq_real-lemma deriving "ccompare_order" instance for type "Complex.complex" via compare_order derived is_ccompare_complex-lemma deriving "ccompare_order" instance for type "Real.real" via compare_order derived is_ccompare_real-lemma use dlist as set_impl for type complex registered complex in class set_impl use dlist as set_impl for type real registered real in class set_impl ### theory "Compare_Complex" ### 1.498s elapsed time, 3.064s cpu time, 0.000s GC time Loading theory "Algebraic_Numbers_Prelim" (required by "Real_Factorization" via "Complex_Algebraic_Numbers" via "Real_Roots" via "Real_Algebraic_Numbers" via "Algebraic_Numbers") ### theory "Complex_Roots_Real_Poly" ### 1.985s elapsed time, 4.032s cpu time, 0.000s GC time locale factor_preserving = fixes f :: "'a poly \ 'a poly" assumes "factor_preserving f" ### theory "Algebraic_Numbers_Prelim" ### 1.241s elapsed time, 2.460s cpu time, 0.000s GC time Loading theory "Algebraic_Numbers" (required by "Real_Factorization" via "Complex_Algebraic_Numbers" via "Real_Roots" via "Real_Algebraic_Numbers") locale ring_hom_poly_x_minus_y Loading theory "Sturm_Rat" (required by "Real_Factorization" via "Complex_Algebraic_Numbers" via "Real_Roots" via "Real_Algebraic_Numbers") ### theory "Algebraic_Numbers" ### 1.526s elapsed time, 2.996s cpu time, 0.480s GC time ### theory "Sturm_Rat" ### 5.481s elapsed time, 10.912s cpu time, 0.400s GC time Loading theory "Real_Algebraic_Numbers" (required by "Real_Factorization" via "Complex_Algebraic_Numbers" via "Real_Roots") *** Failed to finish proof (line 257 of "~~/afp/thys/Algebraic_Numbers/Complex_Roots_Real_Poly.thy"): *** goal (1 subgoal): *** 1. \x1 x2. *** \Complex x1 x2 \ \; c = Complex x1 x2; *** cnj (Complex x1 x2) = Complex x1 x2\ *** \ False *** At command "by" (line 257 of "~~/afp/thys/Algebraic_Numbers/Complex_Roots_Real_Poly.thy") ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Polynomial.poly" found. ### Missing patterns in function definition: ### \a b. rai_normalize_poly_main a b [] = undefined Found termination order: "(\p. length (snd (snd p))) <*mlex*> {}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" instantiation real_alg :: uminus uminus_real_alg == uminus :: real_alg \ real_alg instantiation real_alg :: plus plus_real_alg == plus :: real_alg \ real_alg \ real_alg instantiation real_alg :: minus minus_real_alg == minus_class.minus :: real_alg \ real_alg \ real_alg instantiation real_alg :: zero zero_real_alg == zero_class.zero :: real_alg instantiation real_alg :: one one_real_alg == one_class.one :: real_alg instantiation real_alg :: times times_real_alg == times :: real_alg \ real_alg \ real_alg instantiation real_alg :: inverse inverse_real_alg == inverse :: real_alg \ real_alg divide_real_alg == divide :: real_alg \ real_alg \ real_alg instantiation real_alg :: sgn sgn_real_alg == sgn :: real_alg \ real_alg instantiation real_alg :: equal equal_real_alg == equal_class.equal :: real_alg \ real_alg \ bool instantiation real_alg :: ord less_eq_real_alg == less_eq :: real_alg \ real_alg \ bool less_real_alg == less :: real_alg \ real_alg \ bool instantiation real_alg :: compare_order compare_real_alg == compare :: real_alg \ real_alg \ order instantiation real_alg :: abs abs_real_alg == abs :: real_alg \ real_alg instantiation real_alg :: floor_ceiling floor_real_alg == floor :: real_alg \ int ### Code generator: dropping subsumed code equation ### Ratreal ?x + Ratreal ?y \ Ratreal (?x + ?y) ### Code generator: dropping subsumed code equation ### - Ratreal ?x \ Ratreal (- ?x) ### Code generator: dropping subsumed code equation ### Ratreal ?x - Ratreal ?y \ Ratreal (?x - ?y) ### Code generator: dropping subsumed code equation ### Ratreal ?x * Ratreal ?y \ Ratreal (?x * ?y) ### Code generator: dropping subsumed code equation ### inverse (Ratreal ?x) \ Ratreal (inverse ?x) ### Code generator: dropping subsumed code equation ### Ratreal ?x / Ratreal ?y \ Ratreal (?x / ?y) ### Code generator: dropping subsumed code equation ### \Ratreal ?x\ \ \?x\ ### Code generator: dropping subsumed code equation ### equal_class.equal ?x ?x \ True ### Code generator: dropping subsumed code equation ### equal_class.equal (Ratreal ?x) (Ratreal ?y) \ equal_class.equal ?x ?y ### Code generator: dropping subsumed code equation ### compare \ comparator_of ### Code generator: dropping subsumed code equation ### Ratreal ?x \ Ratreal ?y \ ?x \ ?y ### Code generator: dropping subsumed code equation ### Ratreal ?x < Ratreal ?y \ ?x < ?y ### Code generator: dropping subsumed code equation ### 0 \ Ratreal 0 ### Code generator: dropping subsumed code equation ### 1 \ Ratreal 1 ### theory "Real_Algebraic_Numbers" ### 19.670s elapsed time, 39.192s cpu time, 1.908s GC time Loading theory "Real_Roots" (required by "Real_Factorization" via "Complex_Algebraic_Numbers") ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Polynomial.poly" found. Loading theory "Show_Real_Alg" (required by "Show_Real_Approx") Found termination order: "{}" ### theory "Real_Roots" ### 1.835s elapsed time, 3.596s cpu time, 0.248s GC time Loading theory "Complex_Algebraic_Numbers" (required by "Real_Factorization") deriving "show" instance for type "Real_Algebraic_Numbers.real_alg" overloading show_real \ show_real :: real \ char list ### theory "Show_Real_Alg" ### 0.847s elapsed time, 1.676s cpu time, 0.000s GC time Loading theory "Show_Real_Approx" overloading show_real_alg \ show_real_alg :: real_alg \ char list ### theory "Show_Real_Approx" ### 0.394s elapsed time, 0.788s cpu time, 0.000s GC time Loading theory "Show_Real_Precise" Found termination order: "{}" Found termination order: "{}" overloading show_real_alg \ show_real_alg :: real_alg \ char list locale inj_field_hom_0' = fixes hom :: "'a \ 'b" assumes "inj_field_hom_0' hom" ### theory "Show_Real_Precise" ### 1.558s elapsed time, 3.120s cpu time, 0.000s GC time ### theory "Complex_Algebraic_Numbers" ### 2.538s elapsed time, 5.080s cpu time, 0.000s GC time Loading theory "Real_Factorization" Found termination order: "(\p. size_list (\p. size (snd p)) (snd (snd p))) <*mlex*> {}" Found termination order: "length <*mlex*> {}" ### theory "Real_Factorization" ### 1.565s elapsed time, 3.132s cpu time, 0.000s GC time *** Failed to finish proof (line 130 of "~~/afp/thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy"): *** goal (1 subgoal): *** 1. \x1 x2. *** x = Complex x1 x2 \ *** Complex x1 x2 + cnj (Complex x1 x2) = complex_of_real x1 * 2 *** At command "by" (line 130 of "~~/afp/thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy") ### Metis: Falling back on "metis (mono_tags)"... *** Failed to finish proof (line 130 of "~~/afp/thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy"): *** goal (1 subgoal): *** 1. \x1 x2. *** x = Complex x1 x2 \ *** Complex x1 x2 + cnj (Complex x1 x2) = complex_of_real x1 * 2 *** At command "by" (line 130 of "~~/afp/thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy") *** Failed to finish proof (line 257 of "~~/afp/thys/Algebraic_Numbers/Complex_Roots_Real_Poly.thy"): *** goal (1 subgoal): *** 1. \x1 x2. *** \Complex x1 x2 \ \; c = Complex x1 x2; *** cnj (Complex x1 x2) = Complex x1 x2\ *** \ False *** At command "by" (line 257 of "~~/afp/thys/Algebraic_Numbers/Complex_Roots_Real_Poly.thy")