1.1 --- a/doc-isac/mlehnfeld/master/ruleset.Unsynchronized-2 Thu Jun 26 17:19:30 2014 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,135 +0,0 @@
1.4 -WN130922 Build_Thydata.thy:
1.5 - writeln "======= begin ! ruleset' =======";
1.6 - ! ruleset' |> rev (*!!!!!*)
1.7 - |> map check_kestore_rls |> map writeln;
1.8 - writeln "======= ! ruleset' ordered =======";
1.9 ---------------------------------------------------------------------------------------
1.10 -======= length (! ruleset') = 124
1.11 ---------------------------------------------------------------------------------------
1.12 -======= begin ! ruleset' =======
1.13 -(expand_binomtest, (Test, Rls {#calc = 3, #rules = 29, ...))
1.14 -(make_polytest, (Test, Rls {#calc = 3, #rules = 25, ...))
1.15 -(rearrange_assoc, (Test, Rls {#calc = 0, #rules = 2, ...))
1.16 -(ac_plus_times, (Test, Rls {#calc = 0, #rules = 6, ...))
1.17 -(norm_equation, (Test, Rls {#calc = 0, #rules = 1, ...))
1.18 -(inverse_z, (Inverse_Z_Transform, Rls {#calc = 0, #rules = 1, ...))
1.19 -(matches, (Test, Rls {#calc = 8, #rules = 20, ...))
1.20 -(isolate_bdv, (Test, Rls {#calc = 0, #rules = 6, ...))
1.21 -(isolate_root, (Test, Rls {#calc = 0, #rules = 6, ...))
1.22 -(tval_rls, (Test, Rls {#calc = 11, #rules = 27, ...))
1.23 -(Test_simplify, (Test, Rls {#calc = 4, #rules = 37, ...))
1.24 -(testerls, (Test, Rls {#calc = 8, #rules = 19, ...))
1.25 -(norm_System, (EqSystem, Rls {#calc = 0, #rules = 9, ...))
1.26 -(norm_System_noadd_fractions, (EqSystem, Rls {#calc = 0, #rules = 8, ...))
1.27 -(order_add_mult_System, (EqSystem, Rls {#calc = 0, #rules = 6, ...))
1.28 -(order_system, (EqSystem, Rls {#calc = 0, #rules = 1, ...))
1.29 -(isolate_bdvs_4x4, (EqSystem, Rls {#calc = 0, #rules = 5, ...))
1.30 -(isolate_bdvs, (EqSystem, Rls {#calc = 0, #rules = 3, ...))
1.31 -(simplify_System, (EqSystem, Seq {#calc = 1, #rules = 6, ...))
1.32 -(simplify_System_parenthesized, (EqSystem, Seq {#calc = 1, #rules = 8, ...))
1.33 ------ ruleset.Unsynchronized-1: (testerls, (Test, Rls {#calc = 8, #rules = 19, ...))
1.34 -(norm_Rational_rls_noadd_fractions, (Integrate, Rls {#calc = 0, #rules = 4, ...))
1.35 -(norm_Rational_noadd_fractions, (Integrate, Seq {#calc = 0, #rules = 6, ...))
1.36 -(separate_bdv2, (Integrate, Rls {#calc = 0, #rules = 22, ...))
1.37 -(integration, (Integrate, Seq {#calc = 0, #rules = 3, ...))
1.38 -(simplify_Integral, (Integrate, Seq {#calc = 1, #rules = 7, ...))
1.39 -(add_new_c, (Integrate, Seq {#calc = 0, #rules = 1, ...))
1.40 -(integration_rules, (Integrate, Rls {#calc = 1, #rules = 6, ...))
1.41 -(eval_rls, (DiffApp, Rls {#calc = 0, #rules = 19, ...))
1.42 -(diff_sym_conv, (Diff, Rls {#calc = 1, #rules = 8, ...))
1.43 -(diff_conv, (Diff, Rls {#calc = 1, #rules = 10, ...))
1.44 -(norm_diff, (Diff, Rls {#calc = 0, #rules = 2, ...))
1.45 -(diff_rules, (Diff, Rls {#calc = 0, #rules = 2, ...))
1.46 -(separate_bdvs, (PolyEq, Rls {#calc = 0, #rules = 23, ...))
1.47 -(make_ratpoly_in, (PolyEq, Seq {#calc = 0, #rules = 5, ...))
1.48 -(make_polynomial_in, (PolyEq, Seq {#calc = 0, #rules = 8, ...))
1.49 -(collect_bdv, (PolyEq, Rls {#calc = 0, #rules = 18, ...))
1.50 -(order_add_mult_in, (PolyEq, Rls {#calc = 0, #rules = 6, ...))
1.51 -(d4_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 1, ...))
1.52 -(d3_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 21, ...))
1.53 -(d2_polyeq_abcFormula_simplify, (PolyEq, Rls {#calc = 0, #rules = 18, ...))
1.54 -(d2_polyeq_pqFormula_simplify, (PolyEq, Rls {#calc = 0, #rules = 18, ...))
1.55 -(d2_polyeq_sq_only_simplify, (PolyEq, Rls {#calc = 0, #rules = 6, ...))
1.56 -(d2_polyeq_bdv_only_simplify, (PolyEq, Rls {#calc = 0, #rules = 10, ...))
1.57 -(d2_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 24, ...))
1.58 -(d1_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 3, ...))
1.59 -(d0_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 2, ...))
1.60 -(polyeq_simplify, (PolyEq, Rls {#calc = 6, #rules = 12, ...))
1.61 -(PolyEq_erls, (PolyEq, Rls {#calc = 1, #rules = 42, ...))
1.62 -(complete_square, (PolyEq, Rls {#calc = 0, #rules = 5, ...))
1.63 -(cancel_leading_coeff, (PolyEq, Rls {#calc = 0, #rules = 13, ...))
1.64 -(equival_trans, (Partial_Fractions, Rls {#calc = 0, #rules = 2, ...))
1.65 -(multiply_ansatz, (Partial_Fractions, Rls {#calc = 0, #rules = 1, ...))
1.66 -(ansatz_rls, (Partial_Fractions, Rls {#calc = 0, #rules = 2, ...))
1.67 -(rootrat_solve, (RootRatEq, Rls {#calc = 0, #rules = 4, ...))
1.68 -(RooRatEq_erls, (RootRatEq, Rls {#calc = 2, #rules = 43, ...))
1.69 -(klammern_ausmultiplizieren, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))
1.70 -(klammern_aufloesen, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))
1.71 -(ordne_monome, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))
1.72 -(verschoenere, (PolyMinus, Rls {#calc = 1, #rules = 10, ...))
1.73 -(fasse_zusammen, (PolyMinus, Rls {#calc = 2, #rules = 24, ...))
1.74 -(ordne_alphabetisch, (PolyMinus, Rls {#calc = 0, #rules = 8, ...))
1.75 -(calculate_RootRat, (RootRat, Rls {#calc = 2, #rules = 19, ...))
1.76 -(rootrat_erls, (RootRat, Rls {#calc = 14, #rules = 41, ...))
1.77 -(RatEq_simplify, (RatEq, Rls {#calc = 0, #rules = 8, ...))
1.78 -(RatEq_eliminate, (RatEq, Rls {#calc = 0, #rules = 3, ...))
1.79 -(rateq_erls, (RatEq, Rls {#calc = 1, #rules = 41, ...))
1.80 -(rooteq_simplify, (RootEq, Rls {#calc = 6, #rules = 15, ...))
1.81 -(r_sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 16, ...))
1.82 -(l_sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 16, ...))
1.83 -(sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 32, ...))
1.84 -(rooteq_srls, (RootEq, Rls {#calc = 0, #rules = 3, ...))
1.85 -(RootEq_erls, (RootEq, Rls {#calc = 0, #rules = 28, ...))
1.86 -(cancel_p_rls, (Rational, Rls {#calc = 0, #rules = 1, ...))
1.87 -(rat_mult_div_pow, (Rational, Rls {#calc = 1, #rules = 8, ...))
1.88 -(rat_mult_poly, (Rational, Rls {#calc = 0, #rules = 2, ...))
1.89 -(norm_Rational_parenthesized, (Rational, Seq {#calc = 0, #rules = 2, ...))
1.90 -(norm_Rational_rls, (Rational, Rls {#calc = 0, #rules = 5, ...))
1.91 -(norm_Rational, (Rational, Seq {#calc = 0, #rules = 6, ...))
1.92 -(norm_rat_erls, (Rational, Rls {#calc = 1, #rules = 1, ...))
1.93 -(rat_reduce_1, (Rational, Rls {#calc = 0, #rules = 2, ...))
1.94 -(reduce_0_1_2, (Rational, Rls {#calc = 0, #rules = 6, ...))
1.95 -(rat_mult_divide, (Rational, Rls {#calc = 1, #rules = 6, ...))
1.96 -(powers, (Rational, Rls {#calc = 1, #rules = 11, ...))
1.97 -(powers_erls, (Rational, Rls {#calc = 4, #rules = 6, ...))
1.98 -(add_fractions_p_rls, (Rational, Rls {#calc = 0, #rules = 1, ...))
1.99 -(add_fractions_p, (Rational, Rrls {...}))
1.100 -(cancel_p, (Rational, Rrls {...}))
1.101 -(rational_erls, (Rational, Rls {#calc = 1, #rules = 35, ...))
1.102 -(calc_rat_erls, (Rational, Rls {#calc = 2, #rules = 4, ...))
1.103 -(calculate_Rational, (Rational, Rls {#calc = 1, #rules = 15, ...))
1.104 -(LinEq_simplify, (LinEq, Rls {#calc = 0, #rules = 3, ...))
1.105 -(LinPoly_simplify, (LinEq, Rls {#calc = 4, #rules = 5, ...))
1.106 -(LinEq_erls, (LinEq, Rls {#calc = 0, #rules = 26, ...))
1.107 -(expand_rootbinoms, (Root, Rls {#calc = 6, #rules = 33, ...))
1.108 -(make_rooteq, (Root, Rls {#calc = 3, #rules = 25, ...))
1.109 -(Root_erls, (Root, Rls {#calc = 0, #rules = 27, ...))
1.110 -(make_rat_poly_with_parentheses, (Poly, Seq {#calc = 1, #rules = 10, ...))
1.111 -(order_add_rls_, (Poly, Rls {#calc = 0, #rules = 1, ...))
1.112 -(order_mult_rls_, (Poly, Rls {#calc = 0, #rules = 1, ...))
1.113 -(discard_parentheses1, (Poly, Rls {#calc = 0, #rules = 1, ...))
1.114 -(reduce_012_, (Poly, Rls {#calc = 0, #rules = 6, ...))
1.115 -(reduce_012_mult_, (Poly, Rls {#calc = 0, #rules = 4, ...))
1.116 -(calc_add_mult_pow_, (Poly, Rls {#calc = 3, #rules = 3, ...))
1.117 -(simplify_power_, (Poly, Rls {#calc = 0, #rules = 8, ...))
1.118 -(expand_poly_rat_, (Poly, Rls {#calc = 0, #rules = 10, ...))
1.119 -(expand_poly_, (Poly, Rls {#calc = 0, #rules = 8, ...))
1.120 -(discard_minus, (Poly, Rls {#calc = 0, #rules = 2, ...))
1.121 -(rev_rew_p, (Poly, Seq {#calc = 3, #rules = 25, ...))
1.122 -(expand_binoms, (Poly, Rls {#calc = 3, #rules = 29, ...))
1.123 -(make_polynomial, (Poly, Seq {#calc = 1, #rules = 11, ...))
1.124 -(discard_parentheses, (Poly, Rls {#calc = 0, #rules = 2, ...))
1.125 -(reduce_012, (Poly, Rls {#calc = 0, #rules = 7, ...))
1.126 -(collect_numerals_, (Poly, Rls {#calc = 1, #rules = 7, ...))
1.127 -(collect_numerals, (Poly, Rls {#calc = 3, #rules = 7, ...))
1.128 -(order_add_mult, (Poly, Rls {#calc = 0, #rules = 6, ...))
1.129 -(simplify_power, (Poly, Rls {#calc = 0, #rules = 7, ...))
1.130 -(expand_poly, (Poly, Rls {#calc = 0, #rules = 9, ...))
1.131 -(expand, (Poly, Rls {#calc = 0, #rules = 2, ...))
1.132 -(Poly_erls, (Poly, Rls {#calc = 0, #rules = 25, ...))
1.133 -(norm_Poly, (Poly, Seq {#calc = 1, #rules = 11, ...))
1.134 -(univariate_equation_prls, (Equation, Rls {#calc = 1, #rules = 1, ...))
1.135 -(list_rls, (DiffApp, Rls {#calc = 8, #rules = 53, ...))
1.136 -(e_rrls, (Tools, Rrls {...}))
1.137 -(e_rls, (Tools, Rls {#calc = 0, #rules = 0, ...))
1.138 -======= ! ruleset' ordered =======