| products/sources/formale sprachen/Isabelle/HOL/Computational_Algebra/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: gcd_fractions.prf Sprache: Lisp
|
(gcd_fractions
(div_by_gcd_prep_TCC1 0 (div_by_gcd_prep_TCC1-1 nil 3453735869 ("" (subtype-tcc) nil nil) nil nil)) (div_by_gcd_prep 0 (div_by_gcd_prep-1 nil 3453735879 ("" (skosimp) (("" (case "p!1 / gcd(p!1, q!1) > 0") (("1" (assert) (("1" (typepred "gcd(p!1, q!1)") (("1" (hide -1 -3) (("1" (expand "divides") (("1" (skosimp) (("1" (div-by -1 "gcd(p!1, q!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "pos_div_gt") (("2" (typepred "gcd(p!1, q!1)") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd nil) (divides const-decl "bool" divides nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (posint nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_div1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (times_div_cancel1 formula-decl nil extra_real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (pos_div_gt formula-decl nil real_props nil)) nil)) (div_by_gcd_TCC1 0 (div_by_gcd_TCC1-1 nil 3451974213 ("" (lemma "div_by_gcd_prep") (("" (propax) nil nil)) nil) ((div_by_gcd_prep formula-decl nil gcd_fractions nil)) nil)) (gcd_div_by_gcd_TCC1 0 (gcd_div_by_gcd_TCC1-1 nil 3453642317 ("" (subtype-tcc) nil nil) ((divides const-decl "bool" divides nil) (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd nil) (div_by_gcd const-decl "posint" gcd_fractions nil)) nil)) (gcd_div_by_gcd 0 (gcd_div_by_gcd-1 nil 3451974878 ("" (skosimp) (("" (lemma "gcd_times") (("" (inst - "gcd(p!1, q!1)" "div_by_gcd(p!1, q!1)" "div_by_gcd(q!1, p!1)") (("" (case "div_by_gcd(p!1, q!1) * gcd(p!1, q!1) = p!1 AND div_by_gcd(q!1, p!1) * gcd( (("1" (flatten) (("1" (replace*) (("1" (hide -2 -1) (("1" (cancel-by -1 "gcd(p!1, q!1)") nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (prop) (("1" (expand "div_by_gcd") (("1" (assert) nil nil)) nil) ("2" (expand "div_by_gcd") (("2" (rewrite "gcd_sym") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gcd_times formula-decl nil gcd nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (gcd_sym formula-decl nil gcd nil) (div_by_gcd const-decl "posint" gcd_fractions nil) (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd nil) (divides const-decl "bool" divides nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (posint nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (quotient_fully_cancelled 0 (quotient_fully_cancelled-1 nil 3451974081 ("" (skosimp*) (("" (lemma "rational_pred_ax2") (("" (inst - "r!1") (("" (skosimp*) (("" (case "i!1 > 0") (("1" (inst + "div_by_gcd(i!1, p!1)" "div_by_gcd(p!1, i!1)") (("1" (rewrite "gcd_div_by_gcd") (("1" (expand "div_by_gcd") (("1" (rewrite "gcd_sym") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (cross-mult -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rational_pred_ax2 formula-decl nil rational_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (div_cancel4 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (i!1 skolem-const-decl "int" gcd_fractions nil) (posnat nonempty-type-eq-decl nil integers nil) (div_by_gcd const-decl "posint" gcd_fractions nil) (posint nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (gcd_sym formula-decl nil gcd nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (gcd_div_by_gcd formula-decl nil gcd_fractions nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (posrat nonempty-type-eq-decl nil rationals nil) (> const-decl "bool" reals nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (rational nonempty-type-from-decl nil rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil))) [ Seitenstruktur0.26Drucken etwas mehr zur Ethik ] |