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