1.1 --- a/doc-isac/mlehnfeld/master/ordered-ruleset.Unsynchronized Thu Jun 26 17:19:30 2014 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,150 +0,0 @@
1.4 -WN130922 Build_Thydata.thy:
1.5 - writeln "======= ! ruleset' ordered =======";
1.6 - ! ruleset' |> rev (*!!!!!*)
1.7 - |> map check_kestore_rls |> enumerate_strings |> sort string_ord |> map writeln;
1.8 - writeln "======= end ! ruleset' =======";
1.9 ---------------------------------------------------------------------------------------
1.10 -======= length (! ruleset') = 123
1.11 ---------------------------------------------------------------------------------------
1.12 -Legend:
1.13 -# (*a small difference to KEStore_Elems.get_rlss*)
1.14 -# -----RULESET: an entry missing here in comparison to KEStore_Elems.get_rlss
1.15 ---------------------------------------------------------------------------------------
1.16 -======= ! ruleset' ordered =======
1.17 -(LinEq_erls, (LinEq, Rls {#calc = 0, #rules = 26, ...))--92
1.18 -(LinEq_simplify, (LinEq, Rls {#calc = 0, #rules = 3, ...))--90
1.19 -(LinPoly_simplify, (LinEq, Rls {#calc = 4, #rules = 5, ...))--91
1.20 -(PolyEq_erls, (PolyEq, Rls {#calc = 1, #rules = 42, ...))--47
1.21 -(Poly_erls, (Poly, Rls {#calc = 0 (*11*), #rules = 25, ...))--118
1.22 -(RatEq_eliminate, (RatEq, Rls {#calc = 0, #rules = 3, ...))--64
1.23 -(RatEq_simplify, (RatEq, Rls {#calc = 0, #rules = 8, ...))--63
1.24 -(RooRatEq_erls, (RootRatEq, Rls {#calc = 2, #rules = 43, ...))--54
1.25 -(RootEq_erls, (RootEq, Rls {#calc = 0, #rules = 28, ...))--71
1.26 -
1.27 -(Root_erls, (Root, Rls {#calc = 0, #rules = 27, ...))--95
1.28 -(Test_simplify, (Test, Rls {#calc = 4, #rules = 37, ...))--10
1.29 -(ac_plus_times, (Test, Rls {#calc = 0, #rules = 6, ...))--4
1.30 -(add_fractions_p, (Rational, Rrls {...}))--85
1.31 -(add_fractions_p_rls, (Rational, Rls {#calc = 0, #rules = 1, ...))--84
1.32 -(add_new_c, (Integrate, Seq {#calc = 0, #rules = 1, ...))--25
1.33 -(ansatz_rls, (Partial_Fractions, Rls {#calc = 0, #rules = 2, ...))--52
1.34 -(calc_add_mult_pow_, (Poly, Rls {#calc = 3, #rules = 3, ...))--102
1.35 -(calc_rat_erls, (Rational, Rls {#calc = 2, #rules = 4, ...))--88
1.36 -(calculate_Rational, (Rational, Rls {#calc = 1, #rules = 15, ...))--89
1.37 -
1.38 -(calculate_RootRat, (RootRat, Rls {#calc = 2, #rules = 19, ...))--61
1.39 -(cancel_leading_coeff, (PolyEq, Rls {#calc = 0, #rules = 13, ...))--49
1.40 -(cancel_p, (Rational, Rrls {...}))--86
1.41 -(cancel_p_rls, (Rational, Rls {#calc = 0, #rules = 1, ...))--72
1.42 -(collect_bdv, (PolyEq, Rls {#calc = 0, #rules = 18, ...))--35
1.43 -(collect_numerals, (Poly, Rls {#calc = 3, #rules = 7, ...))--113
1.44 -(collect_numerals_, (Poly, Rls {#calc = 1, #rules = 7, ...))--112
1.45 -(complete_square, (PolyEq, Rls {#calc = 0, #rules = 5, ...))--48
1.46 -(d0_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 2, ...))--45
1.47 -(d1_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 3, ...))--44
1.48 -
1.49 -(d2_polyeq_abcFormula_simplify, (PolyEq, Rls {#calc = 0, #rules = 18, ...))--39
1.50 -(d2_polyeq_bdv_only_simplify, (PolyEq, Rls {#calc = 0, #rules = 10, ...))--42
1.51 -(d2_polyeq_pqFormula_simplify, (PolyEq, Rls {#calc = 0, #rules = 18, ...))--40
1.52 -(d2_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 24, ...))--43
1.53 -(d2_polyeq_sq_only_simplify, (PolyEq, Rls {#calc = 0, #rules = 6, ...))--41
1.54 -(d3_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 21, ...))--38
1.55 -(d4_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 1, ...))--37
1.56 -(diff_conv, (Diff, Rls {#calc = 1, #rules = 10, ...))--29
1.57 -(diff_rules, (Diff, Rls {#calc = 0, #rules = 2, ...))--31
1.58 -(diff_sym_conv, (Diff, Rls {#calc = 1, #rules = 8, ...))--28
1.59 -
1.60 -(discard_minus, (Poly, Rls {#calc = 0, #rules = 2, ...))--106
1.61 -(discard_parentheses, (Poly, Rls {#calc = 0, #rules = 2, ...))--110
1.62 -(discard_parentheses1, (Poly, Rls {#calc = 0, #rules = 1, ...))--99
1.63 -(e_rls, (Tools (*KEStore*), Rls {#calc = 0, #rules = 0, ...))--123
1.64 -(e_rrls, (Tools (*KEStore*), Rrls {...}))--122
1.65 -(equival_trans, (Partial_Fractions, Rls {#calc = 0, #rules = 2, ...))--50
1.66 -(eval_rls, (DiffApp, Rls {#calc = 0, #rules = 19, ...))--27
1.67 -(expand, (Poly, Rls {#calc = 0, #rules = 2, ...))--117
1.68 -(expand_binoms, (Poly, Rls {#calc = 3, #rules = 29, ...))--108
1.69 -(expand_binomtest, (Test, Rls {#calc = 3, #rules = 29, ...))--1
1.70 -
1.71 -(expand_poly, (Poly, Rls {#calc = 0, #rules = 9, ...))--116
1.72 -(expand_poly_, (Poly, Rls {#calc = 0, #rules = 8, ...))--105
1.73 -(expand_poly_rat_, (Poly, Rls {#calc = 0, #rules = 10, ...))--104
1.74 -(expand_rootbinoms, (Root, Rls {#calc = 6, #rules = 33, ...))--93
1.75 -(fasse_zusammen, (PolyMinus, Rls {#calc = 2, #rules = 24, ...))--59
1.76 -(integration, (Integrate, Seq {#calc = 0, #rules = 3, ...))--23
1.77 -(integration_rules, (Integrate, Rls {#calc = 1, #rules = 6, ...))--26
1.78 ------KESTORE: (inverse_z, (Inverse_Z_Transform, Rls {#calc = 0, #rules = 1, ...))--1
1.79 -(isolate_bdv, (Test, Rls {#calc = 0, #rules = 6, ...))--7
1.80 -(isolate_bdvs, (EqSystem, Rls {#calc = 0, #rules = 3, ...))--16
1.81 -
1.82 -(isolate_bdvs_4x4, (EqSystem, Rls {#calc = 0, #rules = 5, ...))--15
1.83 -(isolate_root, (Test, Rls {#calc = 0, #rules = 6, ...))--8
1.84 -(klammern_aufloesen, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))--56
1.85 -(klammern_ausmultiplizieren, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))--55
1.86 -(l_sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 16, ...))--68
1.87 -(list_rls, (DiffApp (*ListC*), Rls {#calc = 8, #rules = 53, ...))--121
1.88 -(make_polynomial, (Poly, Seq {#calc = 1, #rules = 11, ...))--109
1.89 -(make_polynomial_in, (PolyEq, Seq {#calc = 0, #rules = 8, ...))--34
1.90 -(make_polytest, (Test, Rls {#calc = 3, #rules = 25, ...))--2
1.91 -(make_rat_poly_with_parentheses, (Poly, Seq {#calc = 1, #rules = 10, ...))--96
1.92 -
1.93 -(make_ratpoly_in, (PolyEq, Seq {#calc = 0, #rules = 5, ...))--33
1.94 -(make_rooteq, (Root, Rls {#calc = 3, #rules = 25, ...))--94
1.95 -(matches, (Test, Rls {#calc = 8, #rules = 20, ...))--6
1.96 -(multiply_ansatz, (Partial_Fractions, Rls {#calc = 0, #rules = 1, ...))--51
1.97 -(norm_Poly, (Poly, Seq {#calc = 1, #rules = 11, ...))--119
1.98 -(norm_Rational, (Rational, Seq {#calc = 0, #rules = 6, ...))--77
1.99 -(norm_Rational_noadd_fractions, (Integrate, Seq {#calc = 0, #rules = 6, ...))--21
1.100 -(norm_Rational_parenthesized, (Rational, Seq {#calc = 0, #rules = 2, ...))--75
1.101 -(norm_Rational_rls, (Rational, Rls {#calc = 0, #rules = 5, ...))--76
1.102 -(norm_Rational_rls_noadd_fractions, (Integrate, Rls {#calc = 0, #rules = 4, ...))--20
1.103 -
1.104 -(norm_System, (EqSystem, Rls {#calc = 0, #rules = 9, ...))--11
1.105 -(norm_System_noadd_fractions, (EqSystem, Rls {#calc = 0, #rules = 8, ...))--12
1.106 -(norm_diff, (Diff, Rls {#calc = 0, #rules = 2, ...))--30
1.107 -(norm_equation, (Test, Rls {#calc = 0, #rules = 1, ...))--5
1.108 -(norm_rat_erls, (Rational, Rls {#calc = 1, #rules = 1, ...))--78
1.109 -(order_add_mult, (Poly, Rls {#calc = 0, #rules = 6, ...))--114
1.110 -(order_add_mult_System, (EqSystem, Rls {#calc = 0, #rules = 6, ...))--13
1.111 -(order_add_mult_in, (PolyEq, Rls {#calc = 0, #rules = 6, ...))--36
1.112 -(order_add_rls_, (Poly, Rls {#calc = 0, #rules = 1, ...))--97
1.113 -(order_mult_rls_, (Poly, Rls {#calc = 0, #rules = 1, ...))--98
1.114 -
1.115 -(order_system, (EqSystem, Rls {#calc = 0, #rules = 1, ...))--14
1.116 -(ordne_alphabetisch, (PolyMinus, Rls {#calc = 0, #rules = 8, ...))--60
1.117 -(ordne_monome, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))--57
1.118 -(polyeq_simplify, (PolyEq, Rls {#calc = 6, #rules = 12, ...))--46
1.119 -(powers, (Rational, Rls {#calc = 1, #rules = 11, ...))--82
1.120 -(powers_erls, (Rational, Rls {#calc = 4, #rules = 6, ...))--83
1.121 -(r_sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 16, ...))--67
1.122 -(rat_mult_div_pow, (Rational, Rls {#calc = 1, #rules = 8, ...))--73
1.123 -(rat_mult_divide, (Rational, Rls {#calc = 1, #rules = 6, ...))--81
1.124 -(rat_mult_poly, (Rational, Rls {#calc = 0, #rules = 2, ...))--74
1.125 -
1.126 -(rat_reduce_1, (Rational, Rls {#calc = 0, #rules = 2, ...))--79
1.127 -(rateq_erls, (RatEq, Rls {#calc = 1, #rules = 41, ...))--65
1.128 -(rational_erls, (Rational, Rls {#calc = 1, #rules = 35, ...))--87
1.129 -(rearrange_assoc, (Test, Rls {#calc = 0, #rules = 2, ...))--3
1.130 -(reduce_012, (Poly, Rls {#calc = 0, #rules = 7, ...))--111
1.131 -(reduce_012_, (Poly, Rls {#calc = 0, #rules = 6, ...))--100
1.132 -(reduce_012_mult_, (Poly, Rls {#calc = 0, #rules = 4, ...))--101
1.133 -(reduce_0_1_2, (Rational, Rls {#calc = 0, #rules = 6, ...))--80
1.134 -(rev_rew_p, (Poly, Seq {#calc = 3, #rules = 25, ...))--107
1.135 -(rooteq_simplify, (RootEq, Rls {#calc = 6, #rules = 15, ...))--66
1.136 -
1.137 -(rooteq_srls, (RootEq, Rls {#calc = 0, #rules = 3, ...))--70
1.138 -(rootrat_erls, (RootRat, Rls {#calc = 14, #rules = 41, ...))--62
1.139 -(rootrat_solve, (RootRatEq, Rls {#calc = 0, #rules = 4, ...))--53
1.140 -(separate_bdv2, (Integrate, Rls {#calc = 0, #rules = 22, ...))--22
1.141 -(separate_bdvs, (PolyEq, Rls {#calc = 0, #rules = 23, ...))--32
1.142 -(simplify_Integral, (Integrate, Seq {#calc = 1, #rules = 7, ...))--24
1.143 -(simplify_System, (EqSystem, Seq {#calc = 1, #rules = 6, ...))--17
1.144 -(simplify_System_parenthesized, (EqSystem, Seq {#calc = 1, #rules = 8, ...))--18
1.145 -(simplify_power, (Poly, Rls {#calc = 0, #rules = 7, ...))--115
1.146 -(simplify_power_, (Poly, Rls {#calc = 0, #rules = 8, ...))--103
1.147 -
1.148 -(sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 32, ...))--69
1.149 -(testerls, (Test, Rls {#calc = 8, #rules = 19, ...))--19
1.150 -(tval_rls, (Test, Rls {#calc = 11, #rules = 27, ...))--9
1.151 -(univariate_equation_prls, (Equation, Rls {#calc = 1, #rules = 1, ...))--120
1.152 -(verschoenere, (PolyMinus, Rls {#calc = 1, #rules = 10, ...))--58
1.153 -======= end ! ruleset' =======