1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/mlehnfeld/master/ruleset.Unsynchronized-1 Wed Sep 25 13:33:46 2013 +0100
1.3 @@ -0,0 +1,39 @@
1.4 +ruleset.Unsynchronized-1 and ruleset.Unsynchronized-2 are copies from ~/.isabelle/../log/Isac,
1.5 +where log/Isac was created by two different session Isac. and the output stems from ...
1.6 +--------------------------------------------------------------------------------------
1.7 +Build_Thydata.thy:
1.8 + writeln "======= begin ! ruleset' =======";
1.9 + ! ruleset' |> rev (*!!!!!*)
1.10 + |> map check_kestore_rls |> map writeln;
1.11 + writeln "======= ! ruleset' ordered =======";
1.12 +--------------------------------------------------------------------------------------
1.13 +
1.14 +======= begin ! ruleset' =======
1.15 +(expand_binomtest, (Test, Rls {#calc = 3, #rules = 29, ...))
1.16 +(make_polytest, (Test, Rls {#calc = 3, #rules = 25, ...))
1.17 +(rearrange_assoc, (Test, Rls {#calc = 0, #rules = 2, ...))
1.18 +(ac_plus_times, (Test, Rls {#calc = 0, #rules = 6, ...))
1.19 +(norm_equation, (Test, Rls {#calc = 0, #rules = 1, ...))
1.20 +----- ruleset.Unsynchronized-2: (inverse_z, (Inverse_Z_Transform, Rls {#calc = 0, #rules = 1, ...))
1.21 +(matches, (Test, Rls {#calc = 8, #rules = 20, ...))
1.22 +(isolate_bdv, (Test, Rls {#calc = 0, #rules = 6, ...))
1.23 +(isolate_root, (Test, Rls {#calc = 0, #rules = 6, ...))
1.24 +(tval_rls, (Test, Rls {#calc = 11, #rules = 27, ...))
1.25 +(Test_simplify, (Test, Rls {#calc = 4, #rules = 37, ...))
1.26 +----- ruleset.Unsynchronized-2: (testerls, (Test, Rls {#calc = 8, #rules = 19, ...))
1.27 +(norm_System, (EqSystem, Rls {#calc = 0, #rules = 9, ...))
1.28 +(norm_System_noadd_fractions, (EqSystem, Rls {#calc = 0, #rules = 8, ...))
1.29 +(order_add_mult_System, (EqSystem, Rls {#calc = 0, #rules = 6, ...))
1.30 +(order_system, (EqSystem, Rls {#calc = 0, #rules = 1, ...))
1.31 +(isolate_bdvs_4x4, (EqSystem, Rls {#calc = 0, #rules = 5, ...))
1.32 +(isolate_bdvs, (EqSystem, Rls {#calc = 0, #rules = 3, ...))
1.33 +(simplify_System, (EqSystem, Seq {#calc = 1, #rules = 6, ...))
1.34 +(simplify_System_parenthesized, (EqSystem, Seq {#calc = 1, #rules = 8, ...))
1.35 +(testerls, (Test, Rls {#calc = 8, #rules = 19, ...))
1.36 +(norm_Rational_rls_noadd_fractions, (Integrate, Rls {#calc = 0, #rules = 4, ...))
1.37 +(norm_Rational_noadd_fractions, (Integrate, Seq {#calc = 0, #rules = 6, ...))
1.38 +(separate_bdv2, (Integrate, Rls {#calc = 0, #rules = 22, ...))
1.39 +:
1.40 +:
1.41 +:
1.42 +======= ! ruleset' ordered =======
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-isac/mlehnfeld/master/ruleset.Unsynchronized-2 Wed Sep 25 13:33:46 2013 +0100
2.3 @@ -0,0 +1,135 @@
2.4 +WN130922 Build_Thydata.thy:
2.5 + writeln "======= begin ! ruleset' =======";
2.6 + ! ruleset' |> rev (*!!!!!*)
2.7 + |> map check_kestore_rls |> map writeln;
2.8 + writeln "======= ! ruleset' ordered =======";
2.9 +--------------------------------------------------------------------------------------
2.10 +======= length (! ruleset') = 124
2.11 +--------------------------------------------------------------------------------------
2.12 +======= begin ! ruleset' =======
2.13 +(expand_binomtest, (Test, Rls {#calc = 3, #rules = 29, ...))
2.14 +(make_polytest, (Test, Rls {#calc = 3, #rules = 25, ...))
2.15 +(rearrange_assoc, (Test, Rls {#calc = 0, #rules = 2, ...))
2.16 +(ac_plus_times, (Test, Rls {#calc = 0, #rules = 6, ...))
2.17 +(norm_equation, (Test, Rls {#calc = 0, #rules = 1, ...))
2.18 +(inverse_z, (Inverse_Z_Transform, Rls {#calc = 0, #rules = 1, ...))
2.19 +(matches, (Test, Rls {#calc = 8, #rules = 20, ...))
2.20 +(isolate_bdv, (Test, Rls {#calc = 0, #rules = 6, ...))
2.21 +(isolate_root, (Test, Rls {#calc = 0, #rules = 6, ...))
2.22 +(tval_rls, (Test, Rls {#calc = 11, #rules = 27, ...))
2.23 +(Test_simplify, (Test, Rls {#calc = 4, #rules = 37, ...))
2.24 +(testerls, (Test, Rls {#calc = 8, #rules = 19, ...))
2.25 +(norm_System, (EqSystem, Rls {#calc = 0, #rules = 9, ...))
2.26 +(norm_System_noadd_fractions, (EqSystem, Rls {#calc = 0, #rules = 8, ...))
2.27 +(order_add_mult_System, (EqSystem, Rls {#calc = 0, #rules = 6, ...))
2.28 +(order_system, (EqSystem, Rls {#calc = 0, #rules = 1, ...))
2.29 +(isolate_bdvs_4x4, (EqSystem, Rls {#calc = 0, #rules = 5, ...))
2.30 +(isolate_bdvs, (EqSystem, Rls {#calc = 0, #rules = 3, ...))
2.31 +(simplify_System, (EqSystem, Seq {#calc = 1, #rules = 6, ...))
2.32 +(simplify_System_parenthesized, (EqSystem, Seq {#calc = 1, #rules = 8, ...))
2.33 +----- ruleset.Unsynchronized-1: (testerls, (Test, Rls {#calc = 8, #rules = 19, ...))
2.34 +(norm_Rational_rls_noadd_fractions, (Integrate, Rls {#calc = 0, #rules = 4, ...))
2.35 +(norm_Rational_noadd_fractions, (Integrate, Seq {#calc = 0, #rules = 6, ...))
2.36 +(separate_bdv2, (Integrate, Rls {#calc = 0, #rules = 22, ...))
2.37 +(integration, (Integrate, Seq {#calc = 0, #rules = 3, ...))
2.38 +(simplify_Integral, (Integrate, Seq {#calc = 1, #rules = 7, ...))
2.39 +(add_new_c, (Integrate, Seq {#calc = 0, #rules = 1, ...))
2.40 +(integration_rules, (Integrate, Rls {#calc = 1, #rules = 6, ...))
2.41 +(eval_rls, (DiffApp, Rls {#calc = 0, #rules = 19, ...))
2.42 +(diff_sym_conv, (Diff, Rls {#calc = 1, #rules = 8, ...))
2.43 +(diff_conv, (Diff, Rls {#calc = 1, #rules = 10, ...))
2.44 +(norm_diff, (Diff, Rls {#calc = 0, #rules = 2, ...))
2.45 +(diff_rules, (Diff, Rls {#calc = 0, #rules = 2, ...))
2.46 +(separate_bdvs, (PolyEq, Rls {#calc = 0, #rules = 23, ...))
2.47 +(make_ratpoly_in, (PolyEq, Seq {#calc = 0, #rules = 5, ...))
2.48 +(make_polynomial_in, (PolyEq, Seq {#calc = 0, #rules = 8, ...))
2.49 +(collect_bdv, (PolyEq, Rls {#calc = 0, #rules = 18, ...))
2.50 +(order_add_mult_in, (PolyEq, Rls {#calc = 0, #rules = 6, ...))
2.51 +(d4_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 1, ...))
2.52 +(d3_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 21, ...))
2.53 +(d2_polyeq_abcFormula_simplify, (PolyEq, Rls {#calc = 0, #rules = 18, ...))
2.54 +(d2_polyeq_pqFormula_simplify, (PolyEq, Rls {#calc = 0, #rules = 18, ...))
2.55 +(d2_polyeq_sq_only_simplify, (PolyEq, Rls {#calc = 0, #rules = 6, ...))
2.56 +(d2_polyeq_bdv_only_simplify, (PolyEq, Rls {#calc = 0, #rules = 10, ...))
2.57 +(d2_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 24, ...))
2.58 +(d1_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 3, ...))
2.59 +(d0_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 2, ...))
2.60 +(polyeq_simplify, (PolyEq, Rls {#calc = 6, #rules = 12, ...))
2.61 +(PolyEq_erls, (PolyEq, Rls {#calc = 1, #rules = 42, ...))
2.62 +(complete_square, (PolyEq, Rls {#calc = 0, #rules = 5, ...))
2.63 +(cancel_leading_coeff, (PolyEq, Rls {#calc = 0, #rules = 13, ...))
2.64 +(equival_trans, (Partial_Fractions, Rls {#calc = 0, #rules = 2, ...))
2.65 +(multiply_ansatz, (Partial_Fractions, Rls {#calc = 0, #rules = 1, ...))
2.66 +(ansatz_rls, (Partial_Fractions, Rls {#calc = 0, #rules = 2, ...))
2.67 +(rootrat_solve, (RootRatEq, Rls {#calc = 0, #rules = 4, ...))
2.68 +(RooRatEq_erls, (RootRatEq, Rls {#calc = 2, #rules = 43, ...))
2.69 +(klammern_ausmultiplizieren, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))
2.70 +(klammern_aufloesen, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))
2.71 +(ordne_monome, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))
2.72 +(verschoenere, (PolyMinus, Rls {#calc = 1, #rules = 10, ...))
2.73 +(fasse_zusammen, (PolyMinus, Rls {#calc = 2, #rules = 24, ...))
2.74 +(ordne_alphabetisch, (PolyMinus, Rls {#calc = 0, #rules = 8, ...))
2.75 +(calculate_RootRat, (RootRat, Rls {#calc = 2, #rules = 19, ...))
2.76 +(rootrat_erls, (RootRat, Rls {#calc = 14, #rules = 41, ...))
2.77 +(RatEq_simplify, (RatEq, Rls {#calc = 0, #rules = 8, ...))
2.78 +(RatEq_eliminate, (RatEq, Rls {#calc = 0, #rules = 3, ...))
2.79 +(rateq_erls, (RatEq, Rls {#calc = 1, #rules = 41, ...))
2.80 +(rooteq_simplify, (RootEq, Rls {#calc = 6, #rules = 15, ...))
2.81 +(r_sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 16, ...))
2.82 +(l_sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 16, ...))
2.83 +(sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 32, ...))
2.84 +(rooteq_srls, (RootEq, Rls {#calc = 0, #rules = 3, ...))
2.85 +(RootEq_erls, (RootEq, Rls {#calc = 0, #rules = 28, ...))
2.86 +(cancel_p_rls, (Rational, Rls {#calc = 0, #rules = 1, ...))
2.87 +(rat_mult_div_pow, (Rational, Rls {#calc = 1, #rules = 8, ...))
2.88 +(rat_mult_poly, (Rational, Rls {#calc = 0, #rules = 2, ...))
2.89 +(norm_Rational_parenthesized, (Rational, Seq {#calc = 0, #rules = 2, ...))
2.90 +(norm_Rational_rls, (Rational, Rls {#calc = 0, #rules = 5, ...))
2.91 +(norm_Rational, (Rational, Seq {#calc = 0, #rules = 6, ...))
2.92 +(norm_rat_erls, (Rational, Rls {#calc = 1, #rules = 1, ...))
2.93 +(rat_reduce_1, (Rational, Rls {#calc = 0, #rules = 2, ...))
2.94 +(reduce_0_1_2, (Rational, Rls {#calc = 0, #rules = 6, ...))
2.95 +(rat_mult_divide, (Rational, Rls {#calc = 1, #rules = 6, ...))
2.96 +(powers, (Rational, Rls {#calc = 1, #rules = 11, ...))
2.97 +(powers_erls, (Rational, Rls {#calc = 4, #rules = 6, ...))
2.98 +(add_fractions_p_rls, (Rational, Rls {#calc = 0, #rules = 1, ...))
2.99 +(add_fractions_p, (Rational, Rrls {...}))
2.100 +(cancel_p, (Rational, Rrls {...}))
2.101 +(rational_erls, (Rational, Rls {#calc = 1, #rules = 35, ...))
2.102 +(calc_rat_erls, (Rational, Rls {#calc = 2, #rules = 4, ...))
2.103 +(calculate_Rational, (Rational, Rls {#calc = 1, #rules = 15, ...))
2.104 +(LinEq_simplify, (LinEq, Rls {#calc = 0, #rules = 3, ...))
2.105 +(LinPoly_simplify, (LinEq, Rls {#calc = 4, #rules = 5, ...))
2.106 +(LinEq_erls, (LinEq, Rls {#calc = 0, #rules = 26, ...))
2.107 +(expand_rootbinoms, (Root, Rls {#calc = 6, #rules = 33, ...))
2.108 +(make_rooteq, (Root, Rls {#calc = 3, #rules = 25, ...))
2.109 +(Root_erls, (Root, Rls {#calc = 0, #rules = 27, ...))
2.110 +(make_rat_poly_with_parentheses, (Poly, Seq {#calc = 1, #rules = 10, ...))
2.111 +(order_add_rls_, (Poly, Rls {#calc = 0, #rules = 1, ...))
2.112 +(order_mult_rls_, (Poly, Rls {#calc = 0, #rules = 1, ...))
2.113 +(discard_parentheses1, (Poly, Rls {#calc = 0, #rules = 1, ...))
2.114 +(reduce_012_, (Poly, Rls {#calc = 0, #rules = 6, ...))
2.115 +(reduce_012_mult_, (Poly, Rls {#calc = 0, #rules = 4, ...))
2.116 +(calc_add_mult_pow_, (Poly, Rls {#calc = 3, #rules = 3, ...))
2.117 +(simplify_power_, (Poly, Rls {#calc = 0, #rules = 8, ...))
2.118 +(expand_poly_rat_, (Poly, Rls {#calc = 0, #rules = 10, ...))
2.119 +(expand_poly_, (Poly, Rls {#calc = 0, #rules = 8, ...))
2.120 +(discard_minus, (Poly, Rls {#calc = 0, #rules = 2, ...))
2.121 +(rev_rew_p, (Poly, Seq {#calc = 3, #rules = 25, ...))
2.122 +(expand_binoms, (Poly, Rls {#calc = 3, #rules = 29, ...))
2.123 +(make_polynomial, (Poly, Seq {#calc = 1, #rules = 11, ...))
2.124 +(discard_parentheses, (Poly, Rls {#calc = 0, #rules = 2, ...))
2.125 +(reduce_012, (Poly, Rls {#calc = 0, #rules = 7, ...))
2.126 +(collect_numerals_, (Poly, Rls {#calc = 1, #rules = 7, ...))
2.127 +(collect_numerals, (Poly, Rls {#calc = 3, #rules = 7, ...))
2.128 +(order_add_mult, (Poly, Rls {#calc = 0, #rules = 6, ...))
2.129 +(simplify_power, (Poly, Rls {#calc = 0, #rules = 7, ...))
2.130 +(expand_poly, (Poly, Rls {#calc = 0, #rules = 9, ...))
2.131 +(expand, (Poly, Rls {#calc = 0, #rules = 2, ...))
2.132 +(Poly_erls, (Poly, Rls {#calc = 0, #rules = 25, ...))
2.133 +(norm_Poly, (Poly, Seq {#calc = 1, #rules = 11, ...))
2.134 +(univariate_equation_prls, (Equation, Rls {#calc = 1, #rules = 1, ...))
2.135 +(list_rls, (DiffApp, Rls {#calc = 8, #rules = 53, ...))
2.136 +(e_rrls, (Tools, Rrls {...}))
2.137 +(e_rls, (Tools, Rls {#calc = 0, #rules = 0, ...))
2.138 +======= ! ruleset' ordered =======
3.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Sep 23 22:36:46 2013 +0100
3.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 25 13:33:46 2013 +0100
3.3 @@ -1511,6 +1511,12 @@
3.4 ("separate_bdvs", separate_bdvs)
3.5 ]);
3.6 *}
3.7 +setup {* KEStore_Elems.add_rlss
3.8 + [("order_add_mult_in", (Context.theory_name @{theory}, order_add_mult_in)),
3.9 + ("collect_bdv", (Context.theory_name @{theory}, collect_bdv)),
3.10 + ("make_polynomial_in", (Context.theory_name @{theory}, make_polynomial_in)),
3.11 + ("make_ratpoly_in", (Context.theory_name @{theory}, make_ratpoly_in)),
3.12 + ("separate_bdvs", (Context.theory_name @{theory}, separate_bdvs))] *}
3.13
3.14 end
3.15