1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sat Jun 12 14:29:10 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sat Jun 12 18:06:27 2021 +0200
1.3 @@ -155,9 +155,9 @@
1.4 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.5 ],
1.6 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.7 - rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.8 + rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
1.9 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.10 - Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.11 + \<^rule_thm>\<open>NTH_NIL\<close>,
1.12 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs"eval_lhs_"),
1.13 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
1.14 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in")
1.15 @@ -175,18 +175,18 @@
1.16 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.17 ],
1.18 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.19 - rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.20 + rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
1.21 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.22 - Rule.Thm ("NTH_NIL", ThmC.numerals_to_Free @{thm NTH_NIL}),
1.23 + \<^rule_thm>\<open>NTH_NIL\<close>,
1.24 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
1.25 \<^rule_eval>\<open>Prog_Expr.filter_sameFunId\<close> (Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter_sameFunId"),
1.26 (*WN070514 just for smltest/../biegelinie.sml ...*)
1.27 \<^rule_eval>\<open>Prog_Expr.sameFunId\<close> (Prog_Expr.eval_sameFunId "Prog_Expr.sameFunId"),
1.28 - Rule.Thm ("filter_Cons", ThmC.numerals_to_Free @{thm filter_Cons}),
1.29 - Rule.Thm ("filter_Nil", ThmC.numerals_to_Free @{thm filter_Nil}),
1.30 - Rule.Thm ("if_True", ThmC.numerals_to_Free @{thm if_True}),
1.31 - Rule.Thm ("if_False", ThmC.numerals_to_Free @{thm if_False}),
1.32 - Rule.Thm ("hd_thm", ThmC.numerals_to_Free @{thm hd_thm})
1.33 + \<^rule_thm>\<open>filter_Cons\<close>,
1.34 + \<^rule_thm>\<open>filter_Nil\<close>,
1.35 + \<^rule_thm>\<open>if_True\<close>,
1.36 + \<^rule_thm>\<open>if_False\<close>,
1.37 + \<^rule_thm>\<open>hd_thm\<close>
1.38 ],
1.39 scr = Rule.Empty_Prog};
1.40 \<close>
1.41 @@ -260,15 +260,15 @@
1.42 {rew_ord'="tless_true",
1.43 rls' = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty
1.44 [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.45 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1.46 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})],
1.47 + \<^rule_thm>\<open>not_true\<close>,
1.48 + \<^rule_thm>\<open>not_false\<close>],
1.49 calc = [],
1.50 srls = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty
1.51 [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
1.52 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.53 - Rule.Thm ("last_thmI",ThmC.numerals_to_Free @{thm last_thmI}),
1.54 - Rule.Thm ("if_True",ThmC.numerals_to_Free @{thm if_True}),
1.55 - Rule.Thm ("if_False",ThmC.numerals_to_Free @{thm if_False})],
1.56 + \<^rule_thm>\<open>last_thmI\<close>,
1.57 + \<^rule_thm>\<open>if_True\<close>,
1.58 + \<^rule_thm>\<open>if_False\<close>],
1.59 prls = Rule_Set.Empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.Empty},
1.60 @{thm biegelinie.simps})]
1.61 \<close>
1.62 @@ -329,8 +329,8 @@
1.63 {rew_ord'="tless_true",
1.64 rls' = Rule_Set.append_rules "erls_ausBelastung" Rule_Set.empty
1.65 [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.66 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.67 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
1.68 + \<^rule_thm>\<open>not_true\<close>,
1.69 + \<^rule_thm>\<open>not_false\<close>],
1.70 calc = [],
1.71 srls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty
1.72 [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "eval_rhs_")],
2.1 --- a/src/Tools/isac/Knowledge/Diff.thy Sat Jun 12 14:29:10 2021 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Sat Jun 12 18:06:27 2021 +0200
2.3 @@ -111,32 +111,32 @@
2.4 rew_ord = ("termlessI",termlessI),
2.5 erls = Rule_Set.append_rules "erls_diff_conv" Rule_Set.empty
2.6 [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
2.7 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
2.8 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
2.9 + \<^rule_thm>\<open>not_true\<close>,
2.10 + \<^rule_thm>\<open>not_false\<close>,
2.11 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
2.12 - Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
2.13 - Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false})
2.14 + \<^rule_thm>\<open>and_true\<close>,
2.15 + \<^rule_thm>\<open>and_false\<close>
2.16 ],
2.17 srls = Rule_Set.Empty, calc = [], errpatts = [],
2.18 rules =
2.19 - [Rule.Thm ("frac_conv", ThmC.numerals_to_Free @{thm frac_conv}),
2.20 + [\<^rule_thm>\<open>frac_conv\<close>,
2.21 (*"?bdv occurs_in ?b \<Longrightarrow> 0 < ?n \<Longrightarrow> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n"*)
2.22 - Rule.Thm ("sqrt_conv_bdv", ThmC.numerals_to_Free @{thm sqrt_conv_bdv}),
2.23 + \<^rule_thm>\<open>sqrt_conv_bdv\<close>,
2.24 (*"sqrt ?bdv = ?bdv \<up> (1 / 2)"*)
2.25 - Rule.Thm ("sqrt_conv_bdv_n", ThmC.numerals_to_Free @{thm sqrt_conv_bdv_n}),
2.26 + \<^rule_thm>\<open>sqrt_conv_bdv_n\<close>,
2.27 (*"sqrt (?bdv \<up> ?n) = ?bdv \<up> (?n / 2)"*)
2.28 - Rule.Thm ("sqrt_conv", ThmC.numerals_to_Free @{thm sqrt_conv}),
2.29 + \<^rule_thm>\<open>sqrt_conv\<close>,
2.30 (*"?bdv occurs_in ?u \<Longrightarrow> sqrt ?u = ?u \<up> (1 / 2)"*)
2.31 - Rule.Thm ("root_conv", ThmC.numerals_to_Free @{thm root_conv}),
2.32 + \<^rule_thm>\<open>root_conv\<close>,
2.33 (*"?bdv occurs_in ?u \<Longrightarrow> nroot ?n ?u = ?u \<up> (1 / ?n)"*)
2.34 - Rule.Thm ("realpow_pow_bdv", ThmC.numerals_to_Free @{thm realpow_pow_bdv}),
2.35 + \<^rule_thm>\<open>realpow_pow_bdv\<close>,
2.36 (* "(?bdv \<up> ?b) \<up> ?c = ?bdv \<up> (?b * ?c)"*)
2.37 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
2.38 - Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
2.39 + \<^rule_thm>\<open>rat_mult\<close>,
2.40 (*a / b * (c / d) = a * c / (b * d)*)
2.41 - Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
2.42 + \<^rule_thm>\<open>times_divide_eq_right\<close>,
2.43 (*?x * (?y / ?z) = ?x * ?y / ?z*)
2.44 - Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left})
2.45 + \<^rule_thm>\<open>times_divide_eq_left\<close>
2.46 (*?y / ?z * ?x = ?y * ?x / ?z*)
2.47 ],
2.48 scr = Rule.Empty_Prog};
2.49 @@ -150,16 +150,16 @@
2.50 erls = Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty
2.51 [\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_")],
2.52 srls = Rule_Set.Empty, calc = [], errpatts = [],
2.53 - rules = [Rule.Thm ("frac_sym_conv", ThmC.numerals_to_Free @{thm frac_sym_conv}),
2.54 - Rule.Thm ("sqrt_sym_conv", ThmC.numerals_to_Free @{thm sqrt_sym_conv}),
2.55 - Rule.Thm ("root_sym_conv", ThmC.numerals_to_Free @{thm root_sym_conv}),
2.56 + rules = [\<^rule_thm>\<open>frac_sym_conv\<close>,
2.57 + \<^rule_thm>\<open>sqrt_sym_conv\<close>,
2.58 + \<^rule_thm>\<open>root_sym_conv\<close>,
2.59 \<^rule_thm_sym>\<open>real_mult_minus1\<close>,
2.60 (*- ?z = "-1 * ?z"*)
2.61 - Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
2.62 + \<^rule_thm>\<open>rat_mult\<close>,
2.63 (*a / b * (c / d) = a * c / (b * d)*)
2.64 - Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
2.65 + \<^rule_thm>\<open>times_divide_eq_right\<close>,
2.66 (*?x * (?y / ?z) = ?x * ?y / ?z*)
2.67 - Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
2.68 + \<^rule_thm>\<open>times_divide_eq_left\<close>,
2.69 (*?y / ?z * ?x = ?y * ?x / ?z*)
2.70 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_")
2.71 ],
2.72 @@ -182,8 +182,8 @@
2.73 (*..*)
2.74 val erls_diff =
2.75 Rule_Set.append_rules "erls_differentiate.." Rule_Set.empty
2.76 - [Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
2.77 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
2.78 + [\<^rule_thm>\<open>not_true\<close>,
2.79 + \<^rule_thm>\<open>not_false\<close>,
2.80
2.81 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
2.82 \<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
2.83 @@ -195,27 +195,27 @@
2.84 val diff_rules =
2.85 Rule_Def.Repeat {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
2.86 erls = erls_diff, srls = Rule_Set.Empty, calc = [], errpatts = [],
2.87 - rules = [Rule.Thm ("diff_sum",ThmC.numerals_to_Free @{thm diff_sum}),
2.88 - Rule.Thm ("diff_dif",ThmC.numerals_to_Free @{thm diff_dif}),
2.89 - Rule.Thm ("diff_prod_const",ThmC.numerals_to_Free @{thm diff_prod_const}),
2.90 - Rule.Thm ("diff_prod",ThmC.numerals_to_Free @{thm diff_prod}),
2.91 - Rule.Thm ("diff_quot",ThmC.numerals_to_Free @{thm diff_quot}),
2.92 - Rule.Thm ("diff_sin",ThmC.numerals_to_Free @{thm diff_sin}),
2.93 - Rule.Thm ("diff_sin_chain",ThmC.numerals_to_Free @{thm diff_sin_chain}),
2.94 - Rule.Thm ("diff_cos",ThmC.numerals_to_Free @{thm diff_cos}),
2.95 - Rule.Thm ("diff_cos_chain",ThmC.numerals_to_Free @{thm diff_cos_chain}),
2.96 - Rule.Thm ("diff_pow",ThmC.numerals_to_Free @{thm diff_pow}),
2.97 - Rule.Thm ("diff_pow_chain",ThmC.numerals_to_Free @{thm diff_pow_chain}),
2.98 - Rule.Thm ("diff_ln",ThmC.numerals_to_Free @{thm diff_ln}),
2.99 - Rule.Thm ("diff_ln_chain",ThmC.numerals_to_Free @{thm diff_ln_chain}),
2.100 - Rule.Thm ("diff_exp",ThmC.numerals_to_Free @{thm diff_exp}),
2.101 - Rule.Thm ("diff_exp_chain",ThmC.numerals_to_Free @{thm diff_exp_chain}),
2.102 + rules = [\<^rule_thm>\<open>diff_sum\<close>,
2.103 + \<^rule_thm>\<open>diff_dif\<close>,
2.104 + \<^rule_thm>\<open>diff_prod_const\<close>,
2.105 + \<^rule_thm>\<open>diff_prod\<close>,
2.106 + \<^rule_thm>\<open>diff_quot\<close>,
2.107 + \<^rule_thm>\<open>diff_sin\<close>,
2.108 + \<^rule_thm>\<open>diff_sin_chain\<close>,
2.109 + \<^rule_thm>\<open>diff_cos\<close>,
2.110 + \<^rule_thm>\<open>diff_cos_chain\<close>,
2.111 + \<^rule_thm>\<open>diff_pow\<close>,
2.112 + \<^rule_thm>\<open>diff_pow_chain\<close>,
2.113 + \<^rule_thm>\<open>diff_ln\<close>,
2.114 + \<^rule_thm>\<open>diff_ln_chain\<close>,
2.115 + \<^rule_thm>\<open>diff_exp\<close>,
2.116 + \<^rule_thm>\<open>diff_exp_chain\<close>,
2.117 (*
2.118 - Rule.Thm ("diff_sqrt",ThmC.numerals_to_Free @{thm diff_sqrt}),
2.119 - Rule.Thm ("diff_sqrt_chain",ThmC.numerals_to_Free @{thm diff_sqrt_chain}),
2.120 + \<^rule_thm>\<open>diff_sqrt\<close>,
2.121 + \<^rule_thm>\<open>diff_sqrt_chain\<close>,
2.122 *)
2.123 - Rule.Thm ("diff_const",ThmC.numerals_to_Free @{thm diff_const}),
2.124 - Rule.Thm ("diff_var",ThmC.numerals_to_Free @{thm diff_var})
2.125 + \<^rule_thm>\<open>diff_const\<close>,
2.126 + \<^rule_thm>\<open>diff_var\<close>
2.127 ],
2.128 scr = Rule.Empty_Prog};
2.129 \<close>
3.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Sat Jun 12 14:29:10 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Sat Jun 12 18:06:27 2021 +0200
3.3 @@ -35,17 +35,17 @@
3.4 val eval_rls = prep_rls' (
3.5 Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),
3.6 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
3.7 - rules = [Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),
3.8 - Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
3.9 - Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
3.10 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
3.11 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
3.12 - Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
3.13 - Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
3.14 - Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
3.15 - Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
3.16 - Rule.Thm ("and_commute", ThmC.numerals_to_Free @{thm and_commute}),
3.17 - Rule.Thm ("or_commute", ThmC.numerals_to_Free @{thm or_commute}),
3.18 + rules = [\<^rule_thm>\<open>refl\<close>,
3.19 + \<^rule_thm>\<open>order_refl\<close>,
3.20 + \<^rule_thm>\<open>radd_left_cancel_le\<close>,
3.21 + \<^rule_thm>\<open>not_true\<close>,
3.22 + \<^rule_thm>\<open>not_false\<close>,
3.23 + \<^rule_thm>\<open>and_true\<close>,
3.24 + \<^rule_thm>\<open>and_false\<close>,
3.25 + \<^rule_thm>\<open>or_true\<close>,
3.26 + \<^rule_thm>\<open>or_false\<close>,
3.27 + \<^rule_thm>\<open>and_commute\<close>,
3.28 + \<^rule_thm>\<open>or_commute\<close>,
3.29
3.30 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
3.31 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
3.32 @@ -194,8 +194,8 @@
3.33 \<close>
3.34 ML \<open>
3.35 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr
3.36 - [Rule.Thm ("filterVar_Const", ThmC.numerals_to_Free @{thm filterVar_Const}),
3.37 - Rule.Thm ("filterVar_Nil", ThmC.numerals_to_Free @{thm filterVar_Nil})];
3.38 + [\<^rule_thm>\<open>filterVar_Const\<close>,
3.39 + \<^rule_thm>\<open>filterVar_Nil\<close>];
3.40 \<close>
3.41 rule_set_knowledge prog_expr = \<open>prog_expr\<close>
3.42 ML \<open>
4.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 12 14:29:10 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 12 18:06:27 2021 +0200
4.3 @@ -173,17 +173,17 @@
4.4 rew_ord = ("ord_simplify_System",
4.5 ord_simplify_System false @{theory "Integrate"}),
4.6 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
4.7 - rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
4.8 + rules = [\<^rule_thm>\<open>mult.commute\<close>,
4.9 (* z * w = w * z *)
4.10 - Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
4.11 + \<^rule_thm>\<open>real_mult_left_commute\<close>,
4.12 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
4.13 - Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
4.14 + \<^rule_thm>\<open>mult.assoc\<close>,
4.15 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
4.16 - Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
4.17 + \<^rule_thm>\<open>add.commute\<close>,
4.18 (*z + w = w + z*)
4.19 - Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
4.20 + \<^rule_thm>\<open>add.left_commute\<close>,
4.21 (*x + (y + z) = y + (x + z)*)
4.22 - Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc})
4.23 + \<^rule_thm>\<open>add.assoc\<close>
4.24 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
4.25 ],
4.26 scr = Rule.Empty_Prog};
4.27 @@ -245,9 +245,9 @@
4.28 Rule_Set.Sequence {id = "simplify_System_parenthesized", preconds = []:term list,
4.29 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
4.30 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
4.31 - rules = [Rule.Thm ("distrib_right",ThmC.numerals_to_Free @{thm distrib_right}),
4.32 + rules = [\<^rule_thm>\<open>distrib_right\<close>,
4.33 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
4.34 - Rule.Thm ("add_divide_distrib",ThmC.numerals_to_Free @{thm add_divide_distrib}),
4.35 + \<^rule_thm>\<open>add_divide_distrib\<close>,
4.36 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
4.37 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
4.38 Rule.Rls_ norm_Rational_noadd_fractions(**2**),
4.39 @@ -291,9 +291,9 @@
4.40 [(\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))],
4.41 srls = Rule_Set.Empty, calc = [], errpatts = [],
4.42 rules =
4.43 - [Rule.Thm ("commute_0_equality", ThmC.numerals_to_Free @{thm commute_0_equality}),
4.44 - Rule.Thm ("separate_bdvs_add", ThmC.numerals_to_Free @{thm separate_bdvs_add}),
4.45 - Rule.Thm ("separate_bdvs_mult", ThmC.numerals_to_Free @{thm separate_bdvs_mult})],
4.46 + [\<^rule_thm>\<open>commute_0_equality\<close>,
4.47 + \<^rule_thm>\<open>separate_bdvs_add\<close>,
4.48 + \<^rule_thm>\<open>separate_bdvs_mult\<close>],
4.49 scr = Rule.Empty_Prog};
4.50 \<close>
4.51 ML \<open>
4.52 @@ -305,15 +305,15 @@
4.53 [\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"),
4.54 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
4.55 \<^rule_eval>\<open>Prog_Expr.some_occur_in\<close> (Prog_Expr.eval_some_occur_in "#some_occur_in_"),
4.56 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
4.57 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
4.58 + \<^rule_thm>\<open>not_true\<close>,
4.59 + \<^rule_thm>\<open>not_false\<close>
4.60 ],
4.61 srls = Rule_Set.Empty, calc = [], errpatts = [],
4.62 - rules = [Rule.Thm ("commute_0_equality", ThmC.numerals_to_Free @{thm commute_0_equality}),
4.63 - Rule.Thm ("separate_bdvs0", ThmC.numerals_to_Free @{thm separate_bdvs0}),
4.64 - Rule.Thm ("separate_bdvs_add1", ThmC.numerals_to_Free @{thm separate_bdvs_add1}),
4.65 - Rule.Thm ("separate_bdvs_add1", ThmC.numerals_to_Free @{thm separate_bdvs_add2}),
4.66 - Rule.Thm ("separate_bdvs_mult", ThmC.numerals_to_Free @{thm separate_bdvs_mult})
4.67 + rules = [\<^rule_thm>\<open>commute_0_equality\<close>,
4.68 + \<^rule_thm>\<open>separate_bdvs0\<close>,
4.69 + \<^rule_thm>\<open>separate_bdvs_add1\<close>,
4.70 + \<^rule_thm>\<open>separate_bdvs_add2\<close>,
4.71 + \<^rule_thm>\<open>separate_bdvs_mult\<close>
4.72 ], scr = Rule.Empty_Prog};
4.73
4.74 \<close>
4.75 @@ -326,7 +326,7 @@
4.76 rew_ord = ("ord_simplify_System",
4.77 ord_simplify_System false \<^theory>),
4.78 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
4.79 - rules = [Rule.Thm ("order_system_NxN", ThmC.numerals_to_Free @{thm order_system_NxN})
4.80 + rules = [\<^rule_thm>\<open>order_system_NxN\<close>
4.81 ],
4.82 scr = Rule.Empty_Prog};
4.83
4.84 @@ -344,11 +344,11 @@
4.85 ],
4.86 scr = Rule.Empty_Prog},
4.87 srls = Rule_Set.Empty, calc = [], errpatts = [],
4.88 - rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
4.89 + rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
4.90 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
4.91 - Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
4.92 - Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
4.93 - Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
4.94 + \<^rule_thm>\<open>NTH_NIL\<close>,
4.95 + \<^rule_thm>\<open>tl_Cons\<close>,
4.96 + \<^rule_thm>\<open>tl_Nil\<close>,
4.97 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")
4.98 ],
4.99 scr = Rule.Empty_Prog};
4.100 @@ -371,11 +371,11 @@
4.101 ],
4.102 scr = Rule.Empty_Prog},
4.103 srls = Rule_Set.Empty, calc = [], errpatts = [],
4.104 - rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
4.105 + rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
4.106 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
4.107 - Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
4.108 - Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
4.109 - Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
4.110 + \<^rule_thm>\<open>NTH_NIL\<close>,
4.111 + \<^rule_thm>\<open>tl_Cons\<close>,
4.112 + \<^rule_thm>\<open>tl_Nil\<close>,
4.113 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")
4.114 ],
4.115 scr = Rule.Empty_Prog};
4.116 @@ -413,8 +413,8 @@
4.117 ("#Where" ,["Length (e_s:: bool list) = 2", "Length v_s = 2"]),
4.118 ("#Find" ,["solution ss'''"])],
4.119 Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
4.120 - [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
4.121 - Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
4.122 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
4.123 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
4.124 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
4.125 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
4.126 SOME "solveSystem e_s v_s", [])),
4.127 @@ -440,8 +440,8 @@
4.128 ("#Where" ,["Length (e_s:: bool list) = 3", "Length v_s = 3"]),
4.129 ("#Find" ,["solution ss'''"])],
4.130 Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
4.131 - [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
4.132 - Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
4.133 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
4.134 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
4.135 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
4.136 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
4.137 SOME "solveSystem e_s v_s", [])),
4.138 @@ -452,8 +452,8 @@
4.139 ("#Where" ,["Length (e_s:: bool list) = 4", "Length v_s = 4"]),
4.140 ("#Find" ,["solution ss'''"])],
4.141 Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
4.142 - [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
4.143 - Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
4.144 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
4.145 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
4.146 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
4.147 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
4.148 SOME "solveSystem e_s v_s", [])),
4.149 @@ -491,9 +491,9 @@
4.150 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
4.151 ],
4.152 srls = Rule_Set.Empty, calc = [], errpatts = [],
4.153 - rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
4.154 + rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
4.155 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
4.156 - Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL})],
4.157 + \<^rule_thm>\<open>NTH_NIL\<close>],
4.158 scr = Rule.Empty_Prog};
4.159 \<close>
4.160
4.161 @@ -541,9 +541,9 @@
4.162 ("#Find" ,["solution ss'''"])],
4.163 {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
4.164 srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
4.165 - [Rule.Thm ("hd_thm",ThmC.numerals_to_Free @{thm hd_thm}),
4.166 - Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
4.167 - Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil})],
4.168 + [\<^rule_thm>\<open>hd_thm\<close>,
4.169 + \<^rule_thm>\<open>tl_Cons\<close>,
4.170 + \<^rule_thm>\<open>tl_Nil\<close>],
4.171 prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
4.172 @{thm solve_system.simps})]
4.173 \<close>
4.174 @@ -576,9 +576,9 @@
4.175 ("#Find" ,["solution ss'''"])],
4.176 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
4.177 srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
4.178 - [Rule.Thm ("hd_thm",ThmC.numerals_to_Free @{thm hd_thm}),
4.179 - Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
4.180 - Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil})],
4.181 + [\<^rule_thm>\<open>hd_thm\<close>,
4.182 + \<^rule_thm>\<open>tl_Cons\<close>,
4.183 + \<^rule_thm>\<open>tl_Nil\<close>],
4.184 prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
4.185 @{thm solve_system2.simps})]
4.186 \<close>
4.187 @@ -608,9 +608,9 @@
4.188 ("#Find" ,["solution ss'''"])],
4.189 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
4.190 srls = Rule_Set.append_rules "srls_normalise_4x4" srls
4.191 - [Rule.Thm ("hd_thm",ThmC.numerals_to_Free @{thm hd_thm}),
4.192 - Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
4.193 - Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil})],
4.194 + [\<^rule_thm>\<open>hd_thm\<close>,
4.195 + \<^rule_thm>\<open>tl_Cons\<close>,
4.196 + \<^rule_thm>\<open>tl_Nil\<close>],
4.197 prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
4.198 (*STOPPED.WN06? met ["EqSystem", "normalise", "4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
4.199 @{thm solve_system3.simps})]
5.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sat Jun 12 14:29:10 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sat Jun 12 18:06:27 2021 +0200
5.3 @@ -119,17 +119,17 @@
5.4 srls = Rule_Set.Empty, calc = [], errpatts = [],
5.5 rules = [(*for rewriting conditions in Thm's*)
5.6 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
5.7 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
5.8 + \<^rule_thm>\<open>not_true\<close>,
5.9 Rule.Thm ("not_false",@{thm not_false})
5.10 ],
5.11 scr = Rule.Empty_Prog},
5.12 srls = Rule_Set.Empty, calc = [], errpatts = [],
5.13 rules = [
5.14 - Rule.Thm ("integral_const", ThmC.numerals_to_Free @{thm integral_const}),
5.15 - Rule.Thm ("integral_var", ThmC.numerals_to_Free @{thm integral_var}),
5.16 - Rule.Thm ("integral_add", ThmC.numerals_to_Free @{thm integral_add}),
5.17 - Rule.Thm ("integral_mult", ThmC.numerals_to_Free @{thm integral_mult}),
5.18 - Rule.Thm ("integral_pow", ThmC.numerals_to_Free @{thm integral_pow}),
5.19 + \<^rule_thm>\<open>integral_const\<close>,
5.20 + \<^rule_thm>\<open>integral_var\<close>,
5.21 + \<^rule_thm>\<open>integral_add\<close>,
5.22 + \<^rule_thm>\<open>integral_mult\<close>,
5.23 + \<^rule_thm>\<open>integral_pow\<close>,
5.24 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")(*for n+1*)
5.25 ],
5.26 scr = Rule.Empty_Prog};
5.27 @@ -145,12 +145,12 @@
5.28 srls = Rule_Set.Empty, calc = [], errpatts = [],
5.29 rules = [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches""),
5.30 \<^rule_eval>\<open>Integrate.is_f_x\<close> (eval_is_f_x "is_f_x_"),
5.31 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
5.32 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})
5.33 + \<^rule_thm>\<open>not_true\<close>,
5.34 + \<^rule_thm>\<open>not_false\<close>
5.35 ],
5.36 scr = Rule.Empty_Prog},
5.37 srls = Rule_Set.Empty, calc = [], errpatts = [],
5.38 - rules = [ (*Rule.Thm ("call_for_new_c", ThmC.numerals_to_Free @{thm call_for_new_c}),*)
5.39 + rules = [ (*\<^rule_thm>\<open>call_for_new_c\<close>,*)
5.40 Rule.Cal1 ("Integrate.add_new_c", eval_add_new_c "new_c_")
5.41 ],
5.42 scr = Rule.Empty_Prog};
5.43 @@ -172,11 +172,11 @@
5.44 Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
5.45 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
5.46 srls = Rule_Set.Empty, calc = [], errpatts = [],
5.47 - rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
5.48 + rules = [\<^rule_thm>\<open>rat_mult\<close>,
5.49 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
5.50 - Rule.Thm ("rat_mult_poly_l", ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
5.51 + \<^rule_thm>\<open>rat_mult_poly_l\<close>,
5.52 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
5.53 - Rule.Thm ("rat_mult_poly_r", ThmC.numerals_to_Free @{thm rat_mult_poly_r}),
5.54 + \<^rule_thm>\<open>rat_mult_poly_r\<close>,
5.55 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
5.56
5.57 Rule.Thm ("real_divide_divide1_mg",
5.58 @@ -190,7 +190,7 @@
5.59 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
5.60 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
5.61
5.62 - Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
5.63 + \<^rule_thm>\<open>rat_power\<close>
5.64 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
5.65 ],
5.66 scr = Rule.Empty_Prog
5.67 @@ -226,12 +226,12 @@
5.68 val separate_bdv2 =
5.69 Rule_Set.append_rules "separate_bdv2"
5.70 collect_bdv
5.71 - [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
5.72 + [\<^rule_thm>\<open>separate_bdv\<close>,
5.73 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
5.74 - Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
5.75 - Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
5.76 + \<^rule_thm>\<open>separate_bdv_n\<close>,
5.77 + \<^rule_thm>\<open>separate_1_bdv\<close>,
5.78 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
5.79 - Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
5.80 + \<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
5.81 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
5.82 *****Rule.Thm ("add_divide_distrib",
5.83 ***** ThmC.numerals_to_Free @{thm add_divide_distrib})
5.84 @@ -242,9 +242,9 @@
5.85 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
5.86 erls = Atools_erls, srls = Rule_Set.Empty,
5.87 calc = [], errpatts = [],
5.88 - rules = [Rule.Thm ("distrib_right", ThmC.numerals_to_Free @{thm distrib_right}),
5.89 + rules = [\<^rule_thm>\<open>distrib_right\<close>,
5.90 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
5.91 - Rule.Thm ("add_divide_distrib", ThmC.numerals_to_Free @{thm add_divide_distrib}),
5.92 + \<^rule_thm>\<open>add_divide_distrib\<close>,
5.93 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
5.94 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
5.95 Rule.Rls_ norm_Rational_noadd_fractions,
5.96 @@ -273,18 +273,18 @@
5.97 * Rule.Rls_ simplify_power,
5.98 * Rule.Rls_ collect_numerals,
5.99 * Rule.Rls_ reduce_012,
5.100 -* Rule.Thm ("realpow_oneI", ThmC.numerals_to_Free @{thm realpow_oneI}),
5.101 +* \<^rule_thm>\<open>realpow_oneI\<close>,
5.102 * Rule.Rls_ discard_parentheses,
5.103 * Rule.Rls_ collect_bdv,
5.104 * (*below inserted from 'make_ratpoly_in'*)
5.105 * Rule.Rls_ (Rule_Set.append_rules "separate_bdv"
5.106 * collect_bdv
5.107 -* [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
5.108 +* [\<^rule_thm>\<open>separate_bdv\<close>,
5.109 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
5.110 -* Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
5.111 -* Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
5.112 +* \<^rule_thm>\<open>separate_bdv_n\<close>,
5.113 +* \<^rule_thm>\<open>separate_1_bdv\<close>,
5.114 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
5.115 -* Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
5.116 +* \<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
5.117 * (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
5.118 * Rule.Thm ("add_divide_distrib",
5.119 * ThmC.numerals_to_Free @{thm add_divide_distrib})
6.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sat Jun 12 14:29:10 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Sat Jun 12 18:06:27 2021 +0200
6.3 @@ -33,17 +33,17 @@
6.4 \<^rule_eval>\<open>is_polyrat_in\<close> (eval_is_polyrat_in ""),
6.5 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
6.6 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
6.7 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
6.8 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
6.9 - Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
6.10 - Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
6.11 - Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
6.12 - Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false})
6.13 + \<^rule_thm>\<open>not_true\<close>,
6.14 + \<^rule_thm>\<open>not_false\<close>,
6.15 + \<^rule_thm>\<open>and_true\<close>,
6.16 + \<^rule_thm>\<open>and_false\<close>,
6.17 + \<^rule_thm>\<open>or_true\<close>,
6.18 + \<^rule_thm>\<open>or_false\<close>
6.19 ];
6.20 (* ----- erls ----- *)
6.21 val LinEq_crls =
6.22 Rule_Set.append_rules "LinEq_crls" poly_crls
6.23 - [Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1})
6.24 + [\<^rule_thm>\<open>real_assoc_1\<close>
6.25 (*
6.26 Don't use
6.27 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
6.28 @@ -54,7 +54,7 @@
6.29 (* ----- crls ----- *)
6.30 val LinEq_erls =
6.31 Rule_Set.append_rules "LinEq_erls" Poly_erls
6.32 - [Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1})
6.33 + [\<^rule_thm>\<open>real_assoc_1\<close>
6.34 (*
6.35 Don't use
6.36 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
6.37 @@ -72,7 +72,7 @@
6.38 srls = Rule_Set.Empty,
6.39 calc = [], errpatts = [],
6.40 rules = [
6.41 - Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1}),
6.42 + \<^rule_thm>\<open>real_assoc_1\<close>,
6.43 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
6.44 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
6.45 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
6.46 @@ -95,11 +95,11 @@
6.47 srls = Rule_Set.Empty,
6.48 calc = [], errpatts = [],
6.49 rules = [
6.50 - Rule.Thm("lin_isolate_add1",ThmC.numerals_to_Free @{thm lin_isolate_add1}),
6.51 + \<^rule_thm>\<open>lin_isolate_add1\<close>,
6.52 (* a+bx=0 -> bx=-a *)
6.53 - Rule.Thm("lin_isolate_add2",ThmC.numerals_to_Free @{thm lin_isolate_add2}),
6.54 + \<^rule_thm>\<open>lin_isolate_add2\<close>,
6.55 (* a+ x=0 -> x=-a *)
6.56 - Rule.Thm("lin_isolate_div",ThmC.numerals_to_Free @{thm lin_isolate_div})
6.57 + \<^rule_thm>\<open>lin_isolate_div\<close>
6.58 (* bx=c -> x=c/b *)
6.59 ],
6.60 scr = Rule.Empty_Prog});
7.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat Jun 12 14:29:10 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat Jun 12 18:06:27 2021 +0200
7.3 @@ -109,8 +109,8 @@
7.4 Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
7.5 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
7.6 rules =
7.7 - [Rule.Thm ("ansatz_2nd_order",ThmC.numerals_to_Free @{thm ansatz_2nd_order}),
7.8 - Rule.Thm ("ansatz_3rd_order",ThmC.numerals_to_Free @{thm ansatz_3rd_order})
7.9 + [\<^rule_thm>\<open>ansatz_2nd_order\<close>,
7.10 + \<^rule_thm>\<open>ansatz_3rd_order\<close>
7.11 ],
7.12 scr = Rule.Empty_Prog});
7.13
7.14 @@ -118,8 +118,8 @@
7.15 Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
7.16 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
7.17 rules =
7.18 - [Rule.Thm ("equival_trans_2nd_order",ThmC.numerals_to_Free @{thm equival_trans_2nd_order}),
7.19 - Rule.Thm ("equival_trans_3rd_order",ThmC.numerals_to_Free @{thm equival_trans_3rd_order})
7.20 + [\<^rule_thm>\<open>equival_trans_2nd_order\<close>,
7.21 + \<^rule_thm>\<open>equival_trans_3rd_order\<close>
7.22 ],
7.23 scr = Rule.Empty_Prog});
7.24
7.25 @@ -128,7 +128,7 @@
7.26 erls = Rule_Set.Empty,
7.27 srls = Rule_Set.Empty, calc = [], errpatts = [],
7.28 rules =
7.29 - [Rule.Thm ("multiply_2nd_order",ThmC.numerals_to_Free @{thm multiply_2nd_order})
7.30 + [\<^rule_thm>\<open>multiply_2nd_order\<close>
7.31 ],
7.32 scr = Rule.Empty_Prog});
7.33 \<close>
7.34 @@ -173,9 +173,9 @@
7.35 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
7.36 srls = Rule_Set.Empty, calc = [], errpatts = [],
7.37 rules = [
7.38 - Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
7.39 + \<^rule_thm>\<open>NTH_CONS\<close>,
7.40 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
7.41 - Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
7.42 + \<^rule_thm>\<open>NTH_NIL\<close>,
7.43 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
7.44 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
7.45 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
8.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sat Jun 12 14:29:10 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sat Jun 12 18:06:27 2021 +0200
8.3 @@ -653,7 +653,7 @@
8.4 (*.for evaluation of conditions in rewrite rules.*)
8.5 val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls
8.6 [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
8.7 - Rule.Thm ("real_unari_minus", ThmC.numerals_to_Free @{thm real_unari_minus}),
8.8 + \<^rule_thm>\<open>real_unari_minus\<close>,
8.9 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
8.10 \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
8.11 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
8.12 @@ -661,7 +661,7 @@
8.13
8.14 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls
8.15 [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
8.16 - Rule.Thm ("real_unari_minus", ThmC.numerals_to_Free @{thm real_unari_minus}),
8.17 + \<^rule_thm>\<open>real_unari_minus\<close>,
8.18 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
8.19 \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
8.20 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
8.21 @@ -671,9 +671,9 @@
8.22 val expand =
8.23 Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
8.24 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
8.25 - rules = [Rule.Thm ("distrib_right" , ThmC.numerals_to_Free @{thm distrib_right}),
8.26 + rules = [\<^rule_thm>\<open>distrib_right\<close>,
8.27 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
8.28 - Rule.Thm ("distrib_left", ThmC.numerals_to_Free @{thm distrib_left})
8.29 + \<^rule_thm>\<open>distrib_left\<close>
8.30 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
8.31 ], scr = Rule.Empty_Prog};
8.32
8.33 @@ -681,7 +681,7 @@
8.34 Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
8.35 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
8.36 rules =
8.37 - [Rule.Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}),
8.38 + [\<^rule_thm>\<open>real_diff_minus\<close>,
8.39 (*"a - b = a + -1 * b"*)
8.40 \<^rule_thm_sym>\<open>real_mult_minus1\<close>
8.41 (*- ?z = "-1 * ?z"*)],
8.42 @@ -693,31 +693,31 @@
8.43 erls = Rule_Set.empty,srls = Rule_Set.Empty,
8.44 calc = [], errpatts = [],
8.45 rules =
8.46 - [Rule.Thm ("real_plus_binom_pow4", ThmC.numerals_to_Free @{thm real_plus_binom_pow4}),
8.47 + [\<^rule_thm>\<open>real_plus_binom_pow4\<close>,
8.48 (*"(a + b) \<up> 4 = ... "*)
8.49 - Rule.Thm ("real_plus_binom_pow5",ThmC.numerals_to_Free @{thm real_plus_binom_pow5}),
8.50 + \<^rule_thm>\<open>real_plus_binom_pow5\<close>,
8.51 (*"(a + b) \<up> 5 = ... "*)
8.52 - Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),
8.53 + \<^rule_thm>\<open>real_plus_binom_pow3\<close>,
8.54 (*"(a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" *)
8.55 (*WN071229 changed/removed for Schaerding -----vvv*)
8.56 - (*Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),*)
8.57 + (*\<^rule_thm>\<open>real_plus_binom_pow2\<close>,*)
8.58 (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
8.59 - Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
8.60 + \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
8.61 (*"(a + b) \<up> 2 = (a + b) * (a + b)"*)
8.62 - (*Rule.Thm ("real_plus_minus_binom1_p_p", ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p_p}),*)
8.63 + (*\<^rule_thm>\<open>real_plus_minus_binom1_p_p\<close>,*)
8.64 (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*)
8.65 - (*Rule.Thm ("real_plus_minus_binom2_p_p", ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p_p}),*)
8.66 + (*\<^rule_thm>\<open>real_plus_minus_binom2_p_p\<close>,*)
8.67 (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
8.68 (*WN071229 changed/removed for Schaerding -----\<up>*)
8.69
8.70 - Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
8.71 + \<^rule_thm>\<open>distrib_right\<close>,
8.72 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
8.73 - Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
8.74 + \<^rule_thm>\<open>distrib_left\<close>,
8.75 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
8.76
8.77 - Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
8.78 + \<^rule_thm>\<open>realpow_multI\<close>,
8.79 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
8.80 - Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow})
8.81 + \<^rule_thm>\<open>realpow_pow\<close>
8.82 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
8.83 ], scr = Rule.Empty_Prog};
8.84
8.85 @@ -730,19 +730,19 @@
8.86 srls = Rule_Set.Empty,
8.87 calc = [], errpatts = [],
8.88 rules =
8.89 - [Rule.Thm ("real_plus_binom_pow4_poly", ThmC.numerals_to_Free @{thm real_plus_binom_pow4_poly}),
8.90 + [\<^rule_thm>\<open>real_plus_binom_pow4_poly\<close>,
8.91 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 4 = ... "*)
8.92 - Rule.Thm ("real_plus_binom_pow5_poly", ThmC.numerals_to_Free @{thm real_plus_binom_pow5_poly}),
8.93 + \<^rule_thm>\<open>real_plus_binom_pow5_poly\<close>,
8.94 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 5 = ... "*)
8.95 - Rule.Thm ("real_plus_binom_pow2_poly",ThmC.numerals_to_Free @{thm real_plus_binom_pow2_poly}),
8.96 + \<^rule_thm>\<open>real_plus_binom_pow2_poly\<close>,
8.97 (*"[| a is_polyexp; b is_polyexp |] ==>
8.98 (a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
8.99 - Rule.Thm ("real_plus_binom_pow3_poly",ThmC.numerals_to_Free @{thm real_plus_binom_pow3_poly}),
8.100 + \<^rule_thm>\<open>real_plus_binom_pow3_poly\<close>,
8.101 (*"[| a is_polyexp; b is_polyexp |] ==>
8.102 (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" *)
8.103 - Rule.Thm ("real_plus_minus_binom1_p_p",ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p_p}),
8.104 + \<^rule_thm>\<open>real_plus_minus_binom1_p_p\<close>,
8.105 (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*)
8.106 - Rule.Thm ("real_plus_minus_binom2_p_p",ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p_p}),
8.107 + \<^rule_thm>\<open>real_plus_minus_binom2_p_p\<close>,
8.108 (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
8.109
8.110 Rule.Thm ("real_add_mult_distrib_poly",
8.111 @@ -752,10 +752,10 @@
8.112 ThmC.numerals_to_Free @{thm real_add_mult_distrib2_poly}),
8.113 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
8.114
8.115 - Rule.Thm ("realpow_multI_poly", ThmC.numerals_to_Free @{thm realpow_multI_poly}),
8.116 + \<^rule_thm>\<open>realpow_multI_poly\<close>,
8.117 (*"[| r is_polyexp; s is_polyexp |] ==>
8.118 (r * s) \<up> n = r \<up> n * s \<up> n"*)
8.119 - Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow})
8.120 + \<^rule_thm>\<open>realpow_pow\<close>
8.121 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
8.122 ], scr = Rule.Empty_Prog};
8.123
8.124 @@ -768,10 +768,10 @@
8.125 a*(a*a) --> a*a \<up> 2 und nicht a*(a*a) --> a \<up> 2*a *)
8.126 \<^rule_thm_sym>\<open>realpow_twoI\<close>,
8.127 (*"r * r = r \<up> 2"*)
8.128 - Rule.Thm ("realpow_twoI_assoc_l",ThmC.numerals_to_Free @{thm realpow_twoI_assoc_l}),
8.129 + \<^rule_thm>\<open>realpow_twoI_assoc_l\<close>,
8.130 (*"r * (r * s) = r \<up> 2 * s"*)
8.131
8.132 - Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
8.133 + \<^rule_thm>\<open>realpow_plus_1\<close>,
8.134 (*"r * r \<up> n = r \<up> (n + 1)"*)
8.135 Rule.Thm ("realpow_plus_1_assoc_l",
8.136 ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l}),
8.137 @@ -783,12 +783,12 @@
8.138
8.139 \<^rule_thm_sym>\<open>realpow_addI\<close>,
8.140 (*"r \<up> n * r \<up> m = r \<up> (n + m)"*)
8.141 - Rule.Thm ("realpow_addI_assoc_l",ThmC.numerals_to_Free @{thm realpow_addI_assoc_l}),
8.142 + \<^rule_thm>\<open>realpow_addI_assoc_l\<close>,
8.143 (*"r \<up> n * (r \<up> m * s) = r \<up> (n + m) * s"*)
8.144
8.145 (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
8.146 "r * r = r \<up> 2" wenn r=a \<up> b*)
8.147 - Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow})
8.148 + \<^rule_thm>\<open>realpow_pow\<close>
8.149 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
8.150 ], scr = Rule.Empty_Prog};
8.151
8.152 @@ -812,13 +812,13 @@
8.153 erls = Rule_Set.empty,srls = Rule_Set.Empty,
8.154 calc = [], errpatts = [],
8.155 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
8.156 - Rule.Thm ("mult_1_right",ThmC.numerals_to_Free @{thm mult_1_right}),
8.157 + \<^rule_thm>\<open>mult_1_right\<close>,
8.158 (*"z * 1 = z"*) (*wegen "a * b * b \<up> (-1) + a"*)
8.159 - Rule.Thm ("realpow_zeroI",ThmC.numerals_to_Free @{thm realpow_zeroI}),
8.160 + \<^rule_thm>\<open>realpow_zeroI\<close>,
8.161 (*"r \<up> 0 = 1"*) (*wegen "a*a \<up> (-1)*c + b + c"*)
8.162 - Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
8.163 + \<^rule_thm>\<open>realpow_oneI\<close>,
8.164 (*"r \<up> 1 = r"*)
8.165 - Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI})
8.166 + \<^rule_thm>\<open>realpow_eq_oneI\<close>
8.167 (*"1 \<up> n = 1"*)
8.168 ], scr = Rule.Empty_Prog};
8.169
8.170 @@ -829,21 +829,21 @@
8.171 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"))
8.172 ], errpatts = [],
8.173 rules =
8.174 - [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
8.175 + [\<^rule_thm>\<open>real_num_collect\<close>,
8.176 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
8.177 - Rule.Thm ("real_num_collect_assoc_r",ThmC.numerals_to_Free @{thm real_num_collect_assoc_r}),
8.178 + \<^rule_thm>\<open>real_num_collect_assoc_r\<close>,
8.179 (*"[| l is_const; m is_const |] ==> \
8.180 \(k + m * n) + l * n = k + (l + m)*n"*)
8.181 - Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
8.182 + \<^rule_thm>\<open>real_one_collect\<close>,
8.183 (*"m is_const ==> n + m * n = (1 + m) * n"*)
8.184 - Rule.Thm ("real_one_collect_assoc_r",ThmC.numerals_to_Free @{thm real_one_collect_assoc_r}),
8.185 + \<^rule_thm>\<open>real_one_collect_assoc_r\<close>,
8.186 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
8.187
8.188 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
8.189
8.190 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
8.191 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
8.192 - Rule.Thm ("real_mult_2_assoc_r",ThmC.numerals_to_Free @{thm real_mult_2_assoc_r}),
8.193 + \<^rule_thm>\<open>real_mult_2_assoc_r\<close>,
8.194 (*"(k + z1) + z1 = k + 2 * z1"*)
8.195 \<^rule_thm_sym>\<open>real_mult_2\<close>
8.196 (*"z1 + z1 = 2 * z1"*)
8.197 @@ -853,20 +853,20 @@
8.198 Rule_Def.Repeat{id = "reduce_012_", preconds = [],
8.199 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
8.200 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
8.201 - rules = [Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
8.202 + rules = [\<^rule_thm>\<open>mult_1_left\<close>,
8.203 (*"1 * z = z"*)
8.204 - Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
8.205 + \<^rule_thm>\<open>mult_zero_left\<close>,
8.206 (*"0 * z = 0"*)
8.207 - Rule.Thm ("mult_zero_right",ThmC.numerals_to_Free @{thm mult_zero_right}),
8.208 + \<^rule_thm>\<open>mult_zero_right\<close>,
8.209 (*"z * 0 = 0"*)
8.210 - Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
8.211 + \<^rule_thm>\<open>add_0_left\<close>,
8.212 (*"0 + z = z"*)
8.213 - Rule.Thm ("add_0_right",ThmC.numerals_to_Free @{thm add_0_right}),
8.214 + \<^rule_thm>\<open>add_0_right\<close>,
8.215 (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
8.216
8.217 - (*Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI})*)
8.218 + (*\<^rule_thm>\<open>realpow_oneI\<close>*)
8.219 (*"?r \<up> 1 = ?r"*)
8.220 - Rule.Thm ("division_ring_divide_zero",ThmC.numerals_to_Free @{thm division_ring_divide_zero})
8.221 + \<^rule_thm>\<open>division_ring_divide_zero\<close>
8.222 (*"0 / ?x = 0"*)
8.223 ], scr = Rule.Empty_Prog};
8.224
8.225 @@ -884,16 +884,16 @@
8.226 erls = Rule_Set.empty,srls = Rule_Set.Empty,
8.227 calc = [], errpatts = [],
8.228 (*asm_thm = [],*)
8.229 - rules = [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
8.230 + rules = [\<^rule_thm>\<open>distrib_right\<close>,
8.231 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
8.232 - Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
8.233 + \<^rule_thm>\<open>distrib_left\<close>,
8.234 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
8.235 (*Rule.Thm ("distrib_right1",ThmC.numerals_to_Free @{thm distrib_right}1),
8.236 ....... 18.3.03 undefined???*)
8.237
8.238 - Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
8.239 + \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
8.240 (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
8.241 - Rule.Thm ("real_minus_binom_pow2_p",ThmC.numerals_to_Free @{thm real_minus_binom_pow2_p}),
8.242 + \<^rule_thm>\<open>real_minus_binom_pow2_p\<close>,
8.243 (*"(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2"*)
8.244 Rule.Thm ("real_plus_minus_binom1_p",
8.245 ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p}),
8.246 @@ -902,9 +902,9 @@
8.247 ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p}),
8.248 (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
8.249
8.250 - Rule.Thm ("minus_minus",ThmC.numerals_to_Free @{thm minus_minus}),
8.251 + \<^rule_thm>\<open>minus_minus\<close>,
8.252 (*"- (- ?z) = ?z"*)
8.253 - Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
8.254 + \<^rule_thm>\<open>real_diff_minus\<close>,
8.255 (*"a - b = a + -1 * b"*)
8.256 \<^rule_thm_sym>\<open>real_mult_minus1\<close>
8.257 (*- ?z = "-1 * ?z"*)
8.258 @@ -912,7 +912,7 @@
8.259 (*Rule.Thm ("real_minus_add_distrib",
8.260 ThmC.numerals_to_Free @{thm real_minus_add_distrib}),*)
8.261 (*"- (?x + ?y) = - ?x + - ?y"*)
8.262 - (*Rule.Thm ("real_diff_plus",ThmC.numerals_to_Free @{thm real_diff_plus})*)
8.263 + (*\<^rule_thm>\<open>real_diff_plus\<close>*)
8.264 (*"a - b = a + -b"*)
8.265 ], scr = Rule.Empty_Prog};
8.266
8.267 @@ -921,20 +921,20 @@
8.268 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
8.269 erls = Rule_Set.empty, srls = Rule_Set.Empty,
8.270 calc = [], errpatts = [],
8.271 - rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
8.272 + rules = [\<^rule_thm>\<open>realpow_multI\<close>,
8.273 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
8.274
8.275 \<^rule_thm_sym>\<open>realpow_twoI\<close>,
8.276 (*"r1 * r1 = r1 \<up> 2"*)
8.277 - Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
8.278 + \<^rule_thm>\<open>realpow_plus_1\<close>,
8.279 (*"r * r \<up> n = r \<up> (n + 1)"*)
8.280 - Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
8.281 + \<^rule_thm>\<open>realpow_pow\<close>,
8.282 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
8.283 \<^rule_thm_sym>\<open>realpow_addI\<close>,
8.284 (*"r \<up> n * r \<up> m = r \<up> (n + m)"*)
8.285 - Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
8.286 + \<^rule_thm>\<open>realpow_oneI\<close>,
8.287 (*"r \<up> 1 = r"*)
8.288 - Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI})
8.289 + \<^rule_thm>\<open>realpow_eq_oneI\<close>
8.290 (*"1 \<up> n = 1"*)
8.291 ], scr = Rule.Empty_Prog};
8.292
8.293 @@ -946,14 +946,14 @@
8.294 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
8.295 ("POWER", ("Transcendental.powr", eval_binop "#power_"))
8.296 ], errpatts = [],
8.297 - rules = [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
8.298 + rules = [\<^rule_thm>\<open>real_num_collect\<close>,
8.299 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
8.300 - Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
8.301 + \<^rule_thm>\<open>real_num_collect_assoc\<close>,
8.302 (*"[| l is_const; m is_const |] ==>
8.303 l * n + (m * n + k) = (l + m) * n + k"*)
8.304 - Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
8.305 + \<^rule_thm>\<open>real_one_collect\<close>,
8.306 (*"m is_const ==> n + m * n = (1 + m) * n"*)
8.307 - Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
8.308 + \<^rule_thm>\<open>real_one_collect_assoc\<close>,
8.309 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
8.310 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
8.311 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
8.312 @@ -964,9 +964,9 @@
8.313 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
8.314 erls = Rule_Set.empty,srls = Rule_Set.Empty,
8.315 calc = [], errpatts = [],
8.316 - rules = [Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
8.317 + rules = [\<^rule_thm>\<open>mult_1_left\<close>,
8.318 (*"1 * z = z"*)
8.319 - (*Rule.Thm ("real_mult_minus1",ThmC.numerals_to_Free @{thm real_mult_minus1}),14.3.03*)
8.320 + (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*)
8.321 (*"-1 * z = - z"*)
8.322 Rule.Thm ("minus_mult_left",
8.323 ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),
8.324 @@ -974,15 +974,15 @@
8.325 (*Rule.Thm ("real_minus_mult_cancel",
8.326 ThmC.numerals_to_Free @{thm real_minus_mult_cancel}),
8.327 (*"- ?x * - ?y = ?x * ?y"*)---*)
8.328 - Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
8.329 + \<^rule_thm>\<open>mult_zero_left\<close>,
8.330 (*"0 * z = 0"*)
8.331 - Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
8.332 + \<^rule_thm>\<open>add_0_left\<close>,
8.333 (*"0 + z = z"*)
8.334 - Rule.Thm ("right_minus",ThmC.numerals_to_Free @{thm right_minus}),
8.335 + \<^rule_thm>\<open>right_minus\<close>,
8.336 (*"?z + - ?z = 0"*)
8.337 \<^rule_thm_sym>\<open>real_mult_2\<close>,
8.338 (*"z1 + z1 = 2 * z1"*)
8.339 - Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc})
8.340 + \<^rule_thm>\<open>real_mult_2_assoc\<close>
8.341 (*"z1 + (z1 + k) = 2 * z1 + k"*)
8.342 ], scr = Rule.Empty_Prog};
8.343
8.344 @@ -1000,17 +1000,17 @@
8.345 rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>),
8.346 erls = Rule_Set.empty,srls = Rule_Set.Empty,
8.347 calc = [], errpatts = [],
8.348 - rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
8.349 + rules = [\<^rule_thm>\<open>mult.commute\<close>,
8.350 (* z * w = w * z *)
8.351 - Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
8.352 + \<^rule_thm>\<open>real_mult_left_commute\<close>,
8.353 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
8.354 - Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
8.355 + \<^rule_thm>\<open>mult.assoc\<close>,
8.356 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
8.357 - Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
8.358 + \<^rule_thm>\<open>add.commute\<close>,
8.359 (*z + w = w + z*)
8.360 - Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
8.361 + \<^rule_thm>\<open>add.left_commute\<close>,
8.362 (*x + (y + z) = y + (x + z)*)
8.363 - Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc})
8.364 + \<^rule_thm>\<open>add.assoc\<close>
8.365 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
8.366 ], scr = Rule.Empty_Prog};
8.367 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
8.368 @@ -1020,11 +1020,11 @@
8.369 rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>),
8.370 erls = Rule_Set.empty,srls = Rule_Set.Empty,
8.371 calc = [], errpatts = [],
8.372 - rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
8.373 + rules = [\<^rule_thm>\<open>mult.commute\<close>,
8.374 (* z * w = w * z *)
8.375 - Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
8.376 + \<^rule_thm>\<open>real_mult_left_commute\<close>,
8.377 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
8.378 - Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc})
8.379 + \<^rule_thm>\<open>mult.assoc\<close>
8.380 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
8.381 ], scr = Rule.Empty_Prog};
8.382 \<close>
8.383 @@ -1189,21 +1189,21 @@
8.384 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
8.385 ("POWER", ("Transcendental.powr", eval_binop "#power_"))*)
8.386 ], errpatts = [],
8.387 - rules = [Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
8.388 + rules = [\<^rule_thm>\<open>real_plus_binom_times\<close>,
8.389 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
8.390 - Rule.Thm ("real_plus_binom_times1" ,ThmC.numerals_to_Free @{thm real_plus_binom_times1}),
8.391 + \<^rule_thm>\<open>real_plus_binom_times1\<close>,
8.392 (*"(a + 1*b)*(a + -1*b) = a \<up> 2 + -1*b \<up> 2"*)
8.393 - Rule.Thm ("real_plus_binom_times2" ,ThmC.numerals_to_Free @{thm real_plus_binom_times2}),
8.394 + \<^rule_thm>\<open>real_plus_binom_times2\<close>,
8.395 (*"(a + -1*b)*(a + 1*b) = a \<up> 2 + -1*b \<up> 2"*)
8.396
8.397 - Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),(*"1 * z = z"*)
8.398 + \<^rule_thm>\<open>mult_1_left\<close>,(*"1 * z = z"*)
8.399
8.400 - Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
8.401 + \<^rule_thm>\<open>distrib_right\<close>,
8.402 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
8.403 - Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
8.404 + \<^rule_thm>\<open>distrib_left\<close>,
8.405 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
8.406
8.407 - Rule.Thm ("mult.assoc", ThmC.numerals_to_Free @{thm mult.assoc}),
8.408 + \<^rule_thm>\<open>mult.assoc\<close>,
8.409 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
8.410 Rule.Rls_ order_mult_rls_,
8.411 (*Rule.Rls_ order_add_rls_,*)
8.412 @@ -1216,29 +1216,29 @@
8.413 (*"r1 * r1 = r1 \<up> 2"*)
8.414 \<^rule_thm_sym>\<open>real_mult_2\<close>,
8.415 (*"z1 + z1 = 2 * z1"*)
8.416 - Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
8.417 + \<^rule_thm>\<open>real_mult_2_assoc\<close>,
8.418 (*"z1 + (z1 + k) = 2 * z1 + k"*)
8.419
8.420 - Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
8.421 + \<^rule_thm>\<open>real_num_collect\<close>,
8.422 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
8.423 - Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
8.424 + \<^rule_thm>\<open>real_num_collect_assoc\<close>,
8.425 (*"[| l is_const; m is_const |] ==>
8.426 l * n + (m * n + k) = (l + m) * n + k"*)
8.427 - Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
8.428 + \<^rule_thm>\<open>real_one_collect\<close>,
8.429 (*"m is_const ==> n + m * n = (1 + m) * n"*)
8.430 - Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
8.431 + \<^rule_thm>\<open>real_one_collect_assoc\<close>,
8.432 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
8.433
8.434 - Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
8.435 + \<^rule_thm>\<open>realpow_multI\<close>,
8.436 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
8.437
8.438 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
8.439 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
8.440 \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
8.441
8.442 - Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),(*"1 * z = z"*)
8.443 - Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),(*"0 * z = 0"*)
8.444 - Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left})(*0 + z = z*)
8.445 + \<^rule_thm>\<open>mult_1_left\<close>,(*"1 * z = z"*)
8.446 + \<^rule_thm>\<open>mult_zero_left\<close>,(*"0 * z = 0"*)
8.447 + \<^rule_thm>\<open>add_0_left\<close>(*0 + z = z*)
8.448
8.449 (*Rule.Rls_ order_add_rls_*)
8.450 ],
8.451 @@ -1308,66 +1308,66 @@
8.452 ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),
8.453 (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
8.454 (*RL 020915*)
8.455 - Rule.Thm ("real_pp_binom_times",ThmC.numerals_to_Free @{thm real_pp_binom_times}),
8.456 + \<^rule_thm>\<open>real_pp_binom_times\<close>,
8.457 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
8.458 - Rule.Thm ("real_pm_binom_times",ThmC.numerals_to_Free @{thm real_pm_binom_times}),
8.459 + \<^rule_thm>\<open>real_pm_binom_times\<close>,
8.460 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
8.461 - Rule.Thm ("real_mp_binom_times",ThmC.numerals_to_Free @{thm real_mp_binom_times}),
8.462 + \<^rule_thm>\<open>real_mp_binom_times\<close>,
8.463 (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
8.464 - Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}),
8.465 + \<^rule_thm>\<open>real_mm_binom_times\<close>,
8.466 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
8.467 - Rule.Thm ("realpow_multI",ThmC.numerals_to_Free @{thm realpow_multI}),
8.468 + \<^rule_thm>\<open>realpow_multI\<close>,
8.469 (*(a*b) \<up> n = a \<up> n * b \<up> n*)
8.470 - Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),
8.471 + \<^rule_thm>\<open>real_plus_binom_pow3\<close>,
8.472 (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
8.473 Rule.Thm ("real_minus_binom_pow3",
8.474 ThmC.numerals_to_Free @{thm real_minus_binom_pow3}),
8.475 (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
8.476
8.477
8.478 - (*Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
8.479 + (*\<^rule_thm>\<open>distrib_right\<close>,
8.480 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
8.481 - Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
8.482 + \<^rule_thm>\<open>distrib_left\<close>,
8.483 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
8.484 - Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),
8.485 + \<^rule_thm>\<open>left_diff_distrib\<close>,
8.486 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
8.487 - Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),
8.488 + \<^rule_thm>\<open>right_diff_distrib\<close>,
8.489 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
8.490 *)
8.491 - Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
8.492 + \<^rule_thm>\<open>mult_1_left\<close>,
8.493 (*"1 * z = z"*)
8.494 - Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
8.495 + \<^rule_thm>\<open>mult_zero_left\<close>,
8.496 (*"0 * z = 0"*)
8.497 - Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),(*"0 + z = z"*)
8.498 + \<^rule_thm>\<open>add_0_left\<close>,(*"0 + z = z"*)
8.499
8.500 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
8.501 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
8.502 \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
8.503 - (*Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
8.504 + (*\<^rule_thm>\<open>mult.commute\<close>,
8.505 (*AC-rewriting*)
8.506 Rule.Thm ("real_mult_left_commute",
8.507 ThmC.numerals_to_Free @{thm real_mult_left_commute}),
8.508 - Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
8.509 - Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
8.510 - Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
8.511 - Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
8.512 + \<^rule_thm>\<open>mult.assoc\<close>,
8.513 + \<^rule_thm>\<open>add.commute\<close>,
8.514 + \<^rule_thm>\<open>add.left_commute\<close>,
8.515 + \<^rule_thm>\<open>add.assoc\<close>,
8.516 *)
8.517 \<^rule_thm_sym>\<open>realpow_twoI\<close>,
8.518 (*"r1 * r1 = r1 \<up> 2"*)
8.519 - Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
8.520 + \<^rule_thm>\<open>realpow_plus_1\<close>,
8.521 (*"r * r \<up> n = r \<up> (n + 1)"*)
8.522 (*\<^rule_thm_sym>\<open>real_mult_2\<close>,
8.523 (*"z1 + z1 = 2 * z1"*)*)
8.524 - Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
8.525 + \<^rule_thm>\<open>real_mult_2_assoc\<close>,
8.526 (*"z1 + (z1 + k) = 2 * z1 + k"*)
8.527
8.528 - Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
8.529 + \<^rule_thm>\<open>real_num_collect\<close>,
8.530 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
8.531 Rule.Thm ("real_num_collect_assoc",
8.532 ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
8.533 (*"[| l is_const; m is_const |] ==>
8.534 l * n + (m * n + k) = (l + m) * n + k"*)
8.535 - Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
8.536 + \<^rule_thm>\<open>real_one_collect\<close>,
8.537 (*"m is_const ==> n + m * n = (1 + m) * n"*)
8.538 Rule.Thm ("real_one_collect_assoc",
8.539 ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
9.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sat Jun 12 14:29:10 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sat Jun 12 18:06:27 2021 +0200
9.3 @@ -335,34 +335,34 @@
9.4 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
9.5 \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
9.6 \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in ""),
9.7 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
9.8 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
9.9 - Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
9.10 - Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
9.11 - Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
9.12 - Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false})
9.13 + \<^rule_thm>\<open>not_true\<close>,
9.14 + \<^rule_thm>\<open>not_false\<close>,
9.15 + \<^rule_thm>\<open>and_true\<close>,
9.16 + \<^rule_thm>\<open>and_false\<close>,
9.17 + \<^rule_thm>\<open>or_true\<close>,
9.18 + \<^rule_thm>\<open>or_false\<close>
9.19 ];
9.20
9.21 val PolyEq_erls =
9.22 Rule_Set.merge "PolyEq_erls" LinEq_erls
9.23 (Rule_Set.append_rules "ops_preds" calculate_Rational
9.24 [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
9.25 - Rule.Thm ("plus_leq", ThmC.numerals_to_Free @{thm plus_leq}),
9.26 - Rule.Thm ("minus_leq", ThmC.numerals_to_Free @{thm minus_leq}),
9.27 - Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
9.28 - Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),
9.29 - Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3})
9.30 + \<^rule_thm>\<open>plus_leq\<close>,
9.31 + \<^rule_thm>\<open>minus_leq\<close>,
9.32 + \<^rule_thm>\<open>rat_leq1\<close>,
9.33 + \<^rule_thm>\<open>rat_leq2\<close>,
9.34 + \<^rule_thm>\<open>rat_leq3\<close>
9.35 ]);
9.36
9.37 val PolyEq_crls =
9.38 Rule_Set.merge "PolyEq_crls" LinEq_crls
9.39 (Rule_Set.append_rules "ops_preds" calculate_Rational
9.40 [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
9.41 - Rule.Thm ("plus_leq", ThmC.numerals_to_Free @{thm plus_leq}),
9.42 - Rule.Thm ("minus_leq", ThmC.numerals_to_Free @{thm minus_leq}),
9.43 - Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
9.44 - Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),
9.45 - Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3})
9.46 + \<^rule_thm>\<open>plus_leq\<close>,
9.47 + \<^rule_thm>\<open>minus_leq\<close>,
9.48 + \<^rule_thm>\<open>rat_leq1\<close>,
9.49 + \<^rule_thm>\<open>rat_leq2\<close>,
9.50 + \<^rule_thm>\<open>rat_leq3\<close>
9.51 ]);
9.52
9.53 val cancel_leading_coeff = prep_rls'(
9.54 @@ -370,19 +370,19 @@
9.55 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
9.56 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
9.57 rules =
9.58 - [Rule.Thm ("cancel_leading_coeff1",ThmC.numerals_to_Free @{thm cancel_leading_coeff1}),
9.59 - Rule.Thm ("cancel_leading_coeff2",ThmC.numerals_to_Free @{thm cancel_leading_coeff2}),
9.60 - Rule.Thm ("cancel_leading_coeff3",ThmC.numerals_to_Free @{thm cancel_leading_coeff3}),
9.61 - Rule.Thm ("cancel_leading_coeff4",ThmC.numerals_to_Free @{thm cancel_leading_coeff4}),
9.62 - Rule.Thm ("cancel_leading_coeff5",ThmC.numerals_to_Free @{thm cancel_leading_coeff5}),
9.63 - Rule.Thm ("cancel_leading_coeff6",ThmC.numerals_to_Free @{thm cancel_leading_coeff6}),
9.64 - Rule.Thm ("cancel_leading_coeff7",ThmC.numerals_to_Free @{thm cancel_leading_coeff7}),
9.65 - Rule.Thm ("cancel_leading_coeff8",ThmC.numerals_to_Free @{thm cancel_leading_coeff8}),
9.66 - Rule.Thm ("cancel_leading_coeff9",ThmC.numerals_to_Free @{thm cancel_leading_coeff9}),
9.67 - Rule.Thm ("cancel_leading_coeff10",ThmC.numerals_to_Free @{thm cancel_leading_coeff10}),
9.68 - Rule.Thm ("cancel_leading_coeff11",ThmC.numerals_to_Free @{thm cancel_leading_coeff11}),
9.69 - Rule.Thm ("cancel_leading_coeff12",ThmC.numerals_to_Free @{thm cancel_leading_coeff12}),
9.70 - Rule.Thm ("cancel_leading_coeff13",ThmC.numerals_to_Free @{thm cancel_leading_coeff13})
9.71 + [\<^rule_thm>\<open>cancel_leading_coeff1\<close>,
9.72 + \<^rule_thm>\<open>cancel_leading_coeff2\<close>,
9.73 + \<^rule_thm>\<open>cancel_leading_coeff3\<close>,
9.74 + \<^rule_thm>\<open>cancel_leading_coeff4\<close>,
9.75 + \<^rule_thm>\<open>cancel_leading_coeff5\<close>,
9.76 + \<^rule_thm>\<open>cancel_leading_coeff6\<close>,
9.77 + \<^rule_thm>\<open>cancel_leading_coeff7\<close>,
9.78 + \<^rule_thm>\<open>cancel_leading_coeff8\<close>,
9.79 + \<^rule_thm>\<open>cancel_leading_coeff9\<close>,
9.80 + \<^rule_thm>\<open>cancel_leading_coeff10\<close>,
9.81 + \<^rule_thm>\<open>cancel_leading_coeff11\<close>,
9.82 + \<^rule_thm>\<open>cancel_leading_coeff12\<close>,
9.83 + \<^rule_thm>\<open>cancel_leading_coeff13\<close>
9.84 ],scr = Rule.Empty_Prog});
9.85
9.86 val prep_rls' = Auto_Prog.prep_rls @{theory};
9.87 @@ -392,11 +392,11 @@
9.88 Rule_Def.Repeat {id = "complete_square", preconds = [],
9.89 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
9.90 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
9.91 - rules = [Rule.Thm ("complete_square1",ThmC.numerals_to_Free @{thm complete_square1}),
9.92 - Rule.Thm ("complete_square2",ThmC.numerals_to_Free @{thm complete_square2}),
9.93 - Rule.Thm ("complete_square3",ThmC.numerals_to_Free @{thm complete_square3}),
9.94 - Rule.Thm ("complete_square4",ThmC.numerals_to_Free @{thm complete_square4}),
9.95 - Rule.Thm ("complete_square5",ThmC.numerals_to_Free @{thm complete_square5})
9.96 + rules = [\<^rule_thm>\<open>complete_square1\<close>,
9.97 + \<^rule_thm>\<open>complete_square2\<close>,
9.98 + \<^rule_thm>\<open>complete_square3\<close>,
9.99 + \<^rule_thm>\<open>complete_square4\<close>,
9.100 + \<^rule_thm>\<open>complete_square5\<close>
9.101 ],
9.102 scr = Rule.Empty_Prog
9.103 });
9.104 @@ -407,11 +407,11 @@
9.105 erls = PolyEq_erls,
9.106 srls = Rule_Set.Empty,
9.107 calc = [], errpatts = [],
9.108 - rules = [Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1}),
9.109 - Rule.Thm ("real_assoc_2",ThmC.numerals_to_Free @{thm real_assoc_2}),
9.110 - Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
9.111 - Rule.Thm ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
9.112 - Rule.Thm ("realpow_multI",ThmC.numerals_to_Free @{thm realpow_multI}),
9.113 + rules = [\<^rule_thm>\<open>real_assoc_1\<close>,
9.114 + \<^rule_thm>\<open>real_assoc_2\<close>,
9.115 + \<^rule_thm>\<open>real_diff_minus\<close>,
9.116 + \<^rule_thm>\<open>real_unari_minus\<close>,
9.117 + \<^rule_thm>\<open>realpow_multI\<close>,
9.118 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
9.119 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
9.120 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
9.121 @@ -439,7 +439,7 @@
9.122 erls = PolyEq_erls,
9.123 srls = Rule_Set.Empty,
9.124 calc = [], errpatts = [],
9.125 - rules = [Rule.Thm("d0_true",ThmC.numerals_to_Free @{thm d0_true}),
9.126 + rules = [\<^rule_thm>\<open>d0_true\<close>,
9.127 Rule.Thm("d0_false",ThmC.numerals_to_Free @{thm d0_false})
9.128 ],
9.129 scr = Rule.Empty_Prog
9.130 @@ -454,11 +454,11 @@
9.131 srls = Rule_Set.Empty,
9.132 calc = [], errpatts = [],
9.133 rules = [
9.134 - Rule.Thm("d1_isolate_add1",ThmC.numerals_to_Free @{thm d1_isolate_add1}),
9.135 + \<^rule_thm>\<open>d1_isolate_add1\<close>,
9.136 (* a+bx=0 -> bx=-a *)
9.137 - Rule.Thm("d1_isolate_add2",ThmC.numerals_to_Free @{thm d1_isolate_add2}),
9.138 + \<^rule_thm>\<open>d1_isolate_add2\<close>,
9.139 (* a+ x=0 -> x=-a *)
9.140 - Rule.Thm("d1_isolate_div",ThmC.numerals_to_Free @{thm d1_isolate_div})
9.141 + \<^rule_thm>\<open>d1_isolate_div\<close>
9.142 (* bx=c -> x=c/b *)
9.143 ],
9.144 scr = Rule.Empty_Prog
9.145 @@ -473,16 +473,16 @@
9.146 Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
9.147 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
9.148 rules =
9.149 - [Rule.Thm ("d2_prescind1", ThmC.numerals_to_Free @{thm d2_prescind1}), (* ax+bx^2=0 -> x(a+bx)=0 *)
9.150 - Rule.Thm ("d2_prescind2", ThmC.numerals_to_Free @{thm d2_prescind2}), (* ax+ x^2=0 -> x(a+ x)=0 *)
9.151 - Rule.Thm ("d2_prescind3", ThmC.numerals_to_Free @{thm d2_prescind3}), (* x+bx^2=0 -> x(1+bx)=0 *)
9.152 - Rule.Thm ("d2_prescind4", ThmC.numerals_to_Free @{thm d2_prescind4}), (* x+ x^2=0 -> x(1+ x)=0 *)
9.153 - Rule.Thm ("d2_sqrt_equation1", ThmC.numerals_to_Free @{thm d2_sqrt_equation1}), (* x^2=c -> x=+-sqrt(c) *)
9.154 - Rule.Thm ("d2_sqrt_equation1_neg", ThmC.numerals_to_Free @{thm d2_sqrt_equation1_neg}), (* [0<c] x^2=c -> []*)
9.155 - Rule.Thm ("d2_sqrt_equation2", ThmC.numerals_to_Free @{thm d2_sqrt_equation2}), (* x^2=0 -> x=0 *)
9.156 - Rule.Thm ("d2_reduce_equation1", ThmC.numerals_to_Free @{thm d2_reduce_equation1}),(* x(a+bx)=0 -> x=0 |a+bx=0*)
9.157 - Rule.Thm ("d2_reduce_equation2", ThmC.numerals_to_Free @{thm d2_reduce_equation2}),(* x(a+ x)=0 -> x=0 |a+ x=0*)
9.158 - Rule.Thm ("d2_isolate_div", ThmC.numerals_to_Free @{thm d2_isolate_div}) (* bx^2=c -> x^2=c/b *)
9.159 + [\<^rule_thm>\<open>d2_prescind1\<close>, (* ax+bx^2=0 -> x(a+bx)=0 *)
9.160 + \<^rule_thm>\<open>d2_prescind2\<close>, (* ax+ x^2=0 -> x(a+ x)=0 *)
9.161 + \<^rule_thm>\<open>d2_prescind3\<close>, (* x+bx^2=0 -> x(1+bx)=0 *)
9.162 + \<^rule_thm>\<open>d2_prescind4\<close>, (* x+ x^2=0 -> x(1+ x)=0 *)
9.163 + \<^rule_thm>\<open>d2_sqrt_equation1\<close>, (* x^2=c -> x=+-sqrt(c) *)
9.164 + \<^rule_thm>\<open>d2_sqrt_equation1_neg\<close>, (* [0<c] x^2=c -> []*)
9.165 + \<^rule_thm>\<open>d2_sqrt_equation2\<close>, (* x^2=0 -> x=0 *)
9.166 + \<^rule_thm>\<open>d2_reduce_equation1\<close>,(* x(a+bx)=0 -> x=0 |a+bx=0*)
9.167 + \<^rule_thm>\<open>d2_reduce_equation2\<close>,(* x(a+ x)=0 -> x=0 |a+ x=0*)
9.168 + \<^rule_thm>\<open>d2_isolate_div\<close> (* bx^2=c -> x^2=c/b *)
9.169 ],
9.170 scr = Rule.Empty_Prog
9.171 });
9.172 @@ -498,17 +498,17 @@
9.173 calc = [], errpatts = [],
9.174 (*asm_thm = [("d2_sqrt_equation1", ""),("d2_sqrt_equation1_neg", ""),
9.175 ("d2_isolate_div", "")],*)
9.176 - rules = [Rule.Thm("d2_isolate_add1",ThmC.numerals_to_Free @{thm d2_isolate_add1}),
9.177 + rules = [\<^rule_thm>\<open>d2_isolate_add1\<close>,
9.178 (* a+ bx^2=0 -> bx^2=(-1)a*)
9.179 - Rule.Thm("d2_isolate_add2",ThmC.numerals_to_Free @{thm d2_isolate_add2}),
9.180 + \<^rule_thm>\<open>d2_isolate_add2\<close>,
9.181 (* a+ x^2=0 -> x^2=(-1)a*)
9.182 - Rule.Thm("d2_sqrt_equation2",ThmC.numerals_to_Free @{thm d2_sqrt_equation2}),
9.183 + \<^rule_thm>\<open>d2_sqrt_equation2\<close>,
9.184 (* x^2=0 -> x=0 *)
9.185 - Rule.Thm("d2_sqrt_equation1",ThmC.numerals_to_Free @{thm d2_sqrt_equation1}),
9.186 + \<^rule_thm>\<open>d2_sqrt_equation1\<close>,
9.187 (* x^2=c -> x=+-sqrt(c)*)
9.188 - Rule.Thm("d2_sqrt_equation1_neg",ThmC.numerals_to_Free @{thm d2_sqrt_equation1_neg}),
9.189 + \<^rule_thm>\<open>d2_sqrt_equation1_neg\<close>,
9.190 (* [c<0] x^2=c -> x=[] *)
9.191 - Rule.Thm("d2_isolate_div",ThmC.numerals_to_Free @{thm d2_isolate_div})
9.192 + \<^rule_thm>\<open>d2_isolate_div\<close>
9.193 (* bx^2=c -> x^2=c/b*)
9.194 ],
9.195 scr = Rule.Empty_Prog
9.196 @@ -521,41 +521,41 @@
9.197 Rule_Def.Repeat {id = "d2_polyeq_pqFormula_simplify", preconds = [],
9.198 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
9.199 srls = Rule_Set.Empty, calc = [], errpatts = [],
9.200 - rules = [Rule.Thm("d2_pqformula1",ThmC.numerals_to_Free @{thm d2_pqformula1}),
9.201 + rules = [\<^rule_thm>\<open>d2_pqformula1\<close>,
9.202 (* q+px+ x^2=0 *)
9.203 - Rule.Thm("d2_pqformula1_neg",ThmC.numerals_to_Free @{thm d2_pqformula1_neg}),
9.204 + \<^rule_thm>\<open>d2_pqformula1_neg\<close>,
9.205 (* q+px+ x^2=0 *)
9.206 - Rule.Thm("d2_pqformula2",ThmC.numerals_to_Free @{thm d2_pqformula2}),
9.207 + \<^rule_thm>\<open>d2_pqformula2\<close>,
9.208 (* q+px+1x^2=0 *)
9.209 - Rule.Thm("d2_pqformula2_neg",ThmC.numerals_to_Free @{thm d2_pqformula2_neg}),
9.210 + \<^rule_thm>\<open>d2_pqformula2_neg\<close>,
9.211 (* q+px+1x^2=0 *)
9.212 - Rule.Thm("d2_pqformula3",ThmC.numerals_to_Free @{thm d2_pqformula3}),
9.213 + \<^rule_thm>\<open>d2_pqformula3\<close>,
9.214 (* q+ x+ x^2=0 *)
9.215 - Rule.Thm("d2_pqformula3_neg",ThmC.numerals_to_Free @{thm d2_pqformula3_neg}),
9.216 + \<^rule_thm>\<open>d2_pqformula3_neg\<close>,
9.217 (* q+ x+ x^2=0 *)
9.218 - Rule.Thm("d2_pqformula4",ThmC.numerals_to_Free @{thm d2_pqformula4}),
9.219 + \<^rule_thm>\<open>d2_pqformula4\<close>,
9.220 (* q+ x+1x^2=0 *)
9.221 - Rule.Thm("d2_pqformula4_neg",ThmC.numerals_to_Free @{thm d2_pqformula4_neg}),
9.222 + \<^rule_thm>\<open>d2_pqformula4_neg\<close>,
9.223 (* q+ x+1x^2=0 *)
9.224 - Rule.Thm("d2_pqformula5",ThmC.numerals_to_Free @{thm d2_pqformula5}),
9.225 + \<^rule_thm>\<open>d2_pqformula5\<close>,
9.226 (* qx+ x^2=0 *)
9.227 - Rule.Thm("d2_pqformula6",ThmC.numerals_to_Free @{thm d2_pqformula6}),
9.228 + \<^rule_thm>\<open>d2_pqformula6\<close>,
9.229 (* qx+1x^2=0 *)
9.230 - Rule.Thm("d2_pqformula7",ThmC.numerals_to_Free @{thm d2_pqformula7}),
9.231 + \<^rule_thm>\<open>d2_pqformula7\<close>,
9.232 (* x+ x^2=0 *)
9.233 - Rule.Thm("d2_pqformula8",ThmC.numerals_to_Free @{thm d2_pqformula8}),
9.234 + \<^rule_thm>\<open>d2_pqformula8\<close>,
9.235 (* x+1x^2=0 *)
9.236 - Rule.Thm("d2_pqformula9",ThmC.numerals_to_Free @{thm d2_pqformula9}),
9.237 + \<^rule_thm>\<open>d2_pqformula9\<close>,
9.238 (* q +1x^2=0 *)
9.239 - Rule.Thm("d2_pqformula9_neg",ThmC.numerals_to_Free @{thm d2_pqformula9_neg}),
9.240 + \<^rule_thm>\<open>d2_pqformula9_neg\<close>,
9.241 (* q +1x^2=0 *)
9.242 - Rule.Thm("d2_pqformula10",ThmC.numerals_to_Free @{thm d2_pqformula10}),
9.243 + \<^rule_thm>\<open>d2_pqformula10\<close>,
9.244 (* q + x^2=0 *)
9.245 - Rule.Thm("d2_pqformula10_neg",ThmC.numerals_to_Free @{thm d2_pqformula10_neg}),
9.246 + \<^rule_thm>\<open>d2_pqformula10_neg\<close>,
9.247 (* q + x^2=0 *)
9.248 - Rule.Thm("d2_sqrt_equation2",ThmC.numerals_to_Free @{thm d2_sqrt_equation2}),
9.249 + \<^rule_thm>\<open>d2_sqrt_equation2\<close>,
9.250 (* x^2=0 *)
9.251 - Rule.Thm("d2_sqrt_equation3",ThmC.numerals_to_Free @{thm d2_sqrt_equation3})
9.252 + \<^rule_thm>\<open>d2_sqrt_equation3\<close>
9.253 (* 1x^2=0 *)
9.254 ],scr = Rule.Empty_Prog
9.255 });
9.256 @@ -567,41 +567,41 @@
9.257 Rule_Def.Repeat {id = "d2_polyeq_abcFormula_simplify", preconds = [],
9.258 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
9.259 srls = Rule_Set.Empty, calc = [], errpatts = [],
9.260 - rules = [Rule.Thm("d2_abcformula1",ThmC.numerals_to_Free @{thm d2_abcformula1}),
9.261 + rules = [\<^rule_thm>\<open>d2_abcformula1\<close>,
9.262 (*c+bx+cx^2=0 *)
9.263 - Rule.Thm("d2_abcformula1_neg",ThmC.numerals_to_Free @{thm d2_abcformula1_neg}),
9.264 + \<^rule_thm>\<open>d2_abcformula1_neg\<close>,
9.265 (*c+bx+cx^2=0 *)
9.266 - Rule.Thm("d2_abcformula2",ThmC.numerals_to_Free @{thm d2_abcformula2}),
9.267 + \<^rule_thm>\<open>d2_abcformula2\<close>,
9.268 (*c+ x+cx^2=0 *)
9.269 - Rule.Thm("d2_abcformula2_neg",ThmC.numerals_to_Free @{thm d2_abcformula2_neg}),
9.270 + \<^rule_thm>\<open>d2_abcformula2_neg\<close>,
9.271 (*c+ x+cx^2=0 *)
9.272 - Rule.Thm("d2_abcformula3",ThmC.numerals_to_Free @{thm d2_abcformula3}),
9.273 + \<^rule_thm>\<open>d2_abcformula3\<close>,
9.274 (*c+bx+ x^2=0 *)
9.275 - Rule.Thm("d2_abcformula3_neg",ThmC.numerals_to_Free @{thm d2_abcformula3_neg}),
9.276 + \<^rule_thm>\<open>d2_abcformula3_neg\<close>,
9.277 (*c+bx+ x^2=0 *)
9.278 - Rule.Thm("d2_abcformula4",ThmC.numerals_to_Free @{thm d2_abcformula4}),
9.279 + \<^rule_thm>\<open>d2_abcformula4\<close>,
9.280 (*c+ x+ x^2=0 *)
9.281 - Rule.Thm("d2_abcformula4_neg",ThmC.numerals_to_Free @{thm d2_abcformula4_neg}),
9.282 + \<^rule_thm>\<open>d2_abcformula4_neg\<close>,
9.283 (*c+ x+ x^2=0 *)
9.284 - Rule.Thm("d2_abcformula5",ThmC.numerals_to_Free @{thm d2_abcformula5}),
9.285 + \<^rule_thm>\<open>d2_abcformula5\<close>,
9.286 (*c+ cx^2=0 *)
9.287 - Rule.Thm("d2_abcformula5_neg",ThmC.numerals_to_Free @{thm d2_abcformula5_neg}),
9.288 + \<^rule_thm>\<open>d2_abcformula5_neg\<close>,
9.289 (*c+ cx^2=0 *)
9.290 - Rule.Thm("d2_abcformula6",ThmC.numerals_to_Free @{thm d2_abcformula6}),
9.291 + \<^rule_thm>\<open>d2_abcformula6\<close>,
9.292 (*c+ x^2=0 *)
9.293 - Rule.Thm("d2_abcformula6_neg",ThmC.numerals_to_Free @{thm d2_abcformula6_neg}),
9.294 + \<^rule_thm>\<open>d2_abcformula6_neg\<close>,
9.295 (*c+ x^2=0 *)
9.296 - Rule.Thm("d2_abcformula7",ThmC.numerals_to_Free @{thm d2_abcformula7}),
9.297 + \<^rule_thm>\<open>d2_abcformula7\<close>,
9.298 (* bx+ax^2=0 *)
9.299 - Rule.Thm("d2_abcformula8",ThmC.numerals_to_Free @{thm d2_abcformula8}),
9.300 + \<^rule_thm>\<open>d2_abcformula8\<close>,
9.301 (* bx+ x^2=0 *)
9.302 - Rule.Thm("d2_abcformula9",ThmC.numerals_to_Free @{thm d2_abcformula9}),
9.303 + \<^rule_thm>\<open>d2_abcformula9\<close>,
9.304 (* x+ax^2=0 *)
9.305 - Rule.Thm("d2_abcformula10",ThmC.numerals_to_Free @{thm d2_abcformula10}),
9.306 + \<^rule_thm>\<open>d2_abcformula10\<close>,
9.307 (* x+ x^2=0 *)
9.308 - Rule.Thm("d2_sqrt_equation2",ThmC.numerals_to_Free @{thm d2_sqrt_equation2}),
9.309 + \<^rule_thm>\<open>d2_sqrt_equation2\<close>,
9.310 (* x^2=0 *)
9.311 - Rule.Thm("d2_sqrt_equation3",ThmC.numerals_to_Free @{thm d2_sqrt_equation3})
9.312 + \<^rule_thm>\<open>d2_sqrt_equation3\<close>
9.313 (* bx^2=0 *)
9.314 ],
9.315 scr = Rule.Empty_Prog
9.316 @@ -615,53 +615,53 @@
9.317 Rule_Def.Repeat {id = "d2_polyeq_simplify", preconds = [],
9.318 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
9.319 srls = Rule_Set.Empty, calc = [], errpatts = [],
9.320 - rules = [Rule.Thm("d2_pqformula1",ThmC.numerals_to_Free @{thm d2_pqformula1}),
9.321 + rules = [\<^rule_thm>\<open>d2_pqformula1\<close>,
9.322 (* p+qx+ x^2=0 *)
9.323 - Rule.Thm("d2_pqformula1_neg",ThmC.numerals_to_Free @{thm d2_pqformula1_neg}),
9.324 + \<^rule_thm>\<open>d2_pqformula1_neg\<close>,
9.325 (* p+qx+ x^2=0 *)
9.326 - Rule.Thm("d2_pqformula2",ThmC.numerals_to_Free @{thm d2_pqformula2}),
9.327 + \<^rule_thm>\<open>d2_pqformula2\<close>,
9.328 (* p+qx+1x^2=0 *)
9.329 - Rule.Thm("d2_pqformula2_neg",ThmC.numerals_to_Free @{thm d2_pqformula2_neg}),
9.330 + \<^rule_thm>\<open>d2_pqformula2_neg\<close>,
9.331 (* p+qx+1x^2=0 *)
9.332 - Rule.Thm("d2_pqformula3",ThmC.numerals_to_Free @{thm d2_pqformula3}),
9.333 + \<^rule_thm>\<open>d2_pqformula3\<close>,
9.334 (* p+ x+ x^2=0 *)
9.335 - Rule.Thm("d2_pqformula3_neg",ThmC.numerals_to_Free @{thm d2_pqformula3_neg}),
9.336 + \<^rule_thm>\<open>d2_pqformula3_neg\<close>,
9.337 (* p+ x+ x^2=0 *)
9.338 - Rule.Thm("d2_pqformula4",ThmC.numerals_to_Free @{thm d2_pqformula4}),
9.339 + \<^rule_thm>\<open>d2_pqformula4\<close>,
9.340 (* p+ x+1x^2=0 *)
9.341 - Rule.Thm("d2_pqformula4_neg",ThmC.numerals_to_Free @{thm d2_pqformula4_neg}),
9.342 + \<^rule_thm>\<open>d2_pqformula4_neg\<close>,
9.343 (* p+ x+1x^2=0 *)
9.344 - Rule.Thm("d2_abcformula1",ThmC.numerals_to_Free @{thm d2_abcformula1}),
9.345 + \<^rule_thm>\<open>d2_abcformula1\<close>,
9.346 (* c+bx+cx^2=0 *)
9.347 - Rule.Thm("d2_abcformula1_neg",ThmC.numerals_to_Free @{thm d2_abcformula1_neg}),
9.348 + \<^rule_thm>\<open>d2_abcformula1_neg\<close>,
9.349 (* c+bx+cx^2=0 *)
9.350 - Rule.Thm("d2_abcformula2",ThmC.numerals_to_Free @{thm d2_abcformula2}),
9.351 + \<^rule_thm>\<open>d2_abcformula2\<close>,
9.352 (* c+ x+cx^2=0 *)
9.353 - Rule.Thm("d2_abcformula2_neg",ThmC.numerals_to_Free @{thm d2_abcformula2_neg}),
9.354 + \<^rule_thm>\<open>d2_abcformula2_neg\<close>,
9.355 (* c+ x+cx^2=0 *)
9.356 - Rule.Thm("d2_prescind1",ThmC.numerals_to_Free @{thm d2_prescind1}),
9.357 + \<^rule_thm>\<open>d2_prescind1\<close>,
9.358 (* ax+bx^2=0 -> x(a+bx)=0 *)
9.359 - Rule.Thm("d2_prescind2",ThmC.numerals_to_Free @{thm d2_prescind2}),
9.360 + \<^rule_thm>\<open>d2_prescind2\<close>,
9.361 (* ax+ x^2=0 -> x(a+ x)=0 *)
9.362 - Rule.Thm("d2_prescind3",ThmC.numerals_to_Free @{thm d2_prescind3}),
9.363 + \<^rule_thm>\<open>d2_prescind3\<close>,
9.364 (* x+bx^2=0 -> x(1+bx)=0 *)
9.365 - Rule.Thm("d2_prescind4",ThmC.numerals_to_Free @{thm d2_prescind4}),
9.366 + \<^rule_thm>\<open>d2_prescind4\<close>,
9.367 (* x+ x^2=0 -> x(1+ x)=0 *)
9.368 - Rule.Thm("d2_isolate_add1",ThmC.numerals_to_Free @{thm d2_isolate_add1}),
9.369 + \<^rule_thm>\<open>d2_isolate_add1\<close>,
9.370 (* a+ bx^2=0 -> bx^2=(-1)a*)
9.371 - Rule.Thm("d2_isolate_add2",ThmC.numerals_to_Free @{thm d2_isolate_add2}),
9.372 + \<^rule_thm>\<open>d2_isolate_add2\<close>,
9.373 (* a+ x^2=0 -> x^2=(-1)a*)
9.374 - Rule.Thm("d2_sqrt_equation1",ThmC.numerals_to_Free @{thm d2_sqrt_equation1}),
9.375 + \<^rule_thm>\<open>d2_sqrt_equation1\<close>,
9.376 (* x^2=c -> x=+-sqrt(c)*)
9.377 - Rule.Thm("d2_sqrt_equation1_neg",ThmC.numerals_to_Free @{thm d2_sqrt_equation1_neg}),
9.378 + \<^rule_thm>\<open>d2_sqrt_equation1_neg\<close>,
9.379 (* [c<0] x^2=c -> x=[]*)
9.380 - Rule.Thm("d2_sqrt_equation2",ThmC.numerals_to_Free @{thm d2_sqrt_equation2}),
9.381 + \<^rule_thm>\<open>d2_sqrt_equation2\<close>,
9.382 (* x^2=0 -> x=0 *)
9.383 - Rule.Thm("d2_reduce_equation1",ThmC.numerals_to_Free @{thm d2_reduce_equation1}),
9.384 + \<^rule_thm>\<open>d2_reduce_equation1\<close>,
9.385 (* x(a+bx)=0 -> x=0 | a+bx=0*)
9.386 - Rule.Thm("d2_reduce_equation2",ThmC.numerals_to_Free @{thm d2_reduce_equation2}),
9.387 + \<^rule_thm>\<open>d2_reduce_equation2\<close>,
9.388 (* x(a+ x)=0 -> x=0 | a+ x=0*)
9.389 - Rule.Thm("d2_isolate_div",ThmC.numerals_to_Free @{thm d2_isolate_div})
9.390 + \<^rule_thm>\<open>d2_isolate_div\<close>
9.391 (* bx^2=c -> x^2=c/b*)
9.392 ],
9.393 scr = Rule.Empty_Prog
9.394 @@ -676,65 +676,65 @@
9.395 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
9.396 srls = Rule_Set.Empty, calc = [], errpatts = [],
9.397 rules =
9.398 - [Rule.Thm("d3_reduce_equation1",ThmC.numerals_to_Free @{thm d3_reduce_equation1}),
9.399 + [\<^rule_thm>\<open>d3_reduce_equation1\<close>,
9.400 (*a*bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) =
9.401 (bdv=0 | (a + b*bdv + c*bdv \<up> 2=0)*)
9.402 - Rule.Thm("d3_reduce_equation2",ThmC.numerals_to_Free @{thm d3_reduce_equation2}),
9.403 + \<^rule_thm>\<open>d3_reduce_equation2\<close>,
9.404 (* bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) =
9.405 (bdv=0 | (1 + b*bdv + c*bdv \<up> 2=0)*)
9.406 - Rule.Thm("d3_reduce_equation3",ThmC.numerals_to_Free @{thm d3_reduce_equation3}),
9.407 + \<^rule_thm>\<open>d3_reduce_equation3\<close>,
9.408 (*a*bdv + bdv \<up> 2 + c*bdv \<up> 3=0) =
9.409 (bdv=0 | (a + bdv + c*bdv \<up> 2=0)*)
9.410 - Rule.Thm("d3_reduce_equation4",ThmC.numerals_to_Free @{thm d3_reduce_equation4}),
9.411 + \<^rule_thm>\<open>d3_reduce_equation4\<close>,
9.412 (* bdv + bdv \<up> 2 + c*bdv \<up> 3=0) =
9.413 (bdv=0 | (1 + bdv + c*bdv \<up> 2=0)*)
9.414 - Rule.Thm("d3_reduce_equation5",ThmC.numerals_to_Free @{thm d3_reduce_equation5}),
9.415 + \<^rule_thm>\<open>d3_reduce_equation5\<close>,
9.416 (*a*bdv + b*bdv \<up> 2 + bdv \<up> 3=0) =
9.417 (bdv=0 | (a + b*bdv + bdv \<up> 2=0)*)
9.418 - Rule.Thm("d3_reduce_equation6",ThmC.numerals_to_Free @{thm d3_reduce_equation6}),
9.419 + \<^rule_thm>\<open>d3_reduce_equation6\<close>,
9.420 (* bdv + b*bdv \<up> 2 + bdv \<up> 3=0) =
9.421 (bdv=0 | (1 + b*bdv + bdv \<up> 2=0)*)
9.422 - Rule.Thm("d3_reduce_equation7",ThmC.numerals_to_Free @{thm d3_reduce_equation7}),
9.423 + \<^rule_thm>\<open>d3_reduce_equation7\<close>,
9.424 (*a*bdv + bdv \<up> 2 + bdv \<up> 3=0) =
9.425 (bdv=0 | (1 + bdv + bdv \<up> 2=0)*)
9.426 - Rule.Thm("d3_reduce_equation8",ThmC.numerals_to_Free @{thm d3_reduce_equation8}),
9.427 + \<^rule_thm>\<open>d3_reduce_equation8\<close>,
9.428 (* bdv + bdv \<up> 2 + bdv \<up> 3=0) =
9.429 (bdv=0 | (1 + bdv + bdv \<up> 2=0)*)
9.430 - Rule.Thm("d3_reduce_equation9",ThmC.numerals_to_Free @{thm d3_reduce_equation9}),
9.431 + \<^rule_thm>\<open>d3_reduce_equation9\<close>,
9.432 (*a*bdv + c*bdv \<up> 3=0) =
9.433 (bdv=0 | (a + c*bdv \<up> 2=0)*)
9.434 - Rule.Thm("d3_reduce_equation10",ThmC.numerals_to_Free @{thm d3_reduce_equation10}),
9.435 + \<^rule_thm>\<open>d3_reduce_equation10\<close>,
9.436 (* bdv + c*bdv \<up> 3=0) =
9.437 (bdv=0 | (1 + c*bdv \<up> 2=0)*)
9.438 - Rule.Thm("d3_reduce_equation11",ThmC.numerals_to_Free @{thm d3_reduce_equation11}),
9.439 + \<^rule_thm>\<open>d3_reduce_equation11\<close>,
9.440 (*a*bdv + bdv \<up> 3=0) =
9.441 (bdv=0 | (a + bdv \<up> 2=0)*)
9.442 - Rule.Thm("d3_reduce_equation12",ThmC.numerals_to_Free @{thm d3_reduce_equation12}),
9.443 + \<^rule_thm>\<open>d3_reduce_equation12\<close>,
9.444 (* bdv + bdv \<up> 3=0) =
9.445 (bdv=0 | (1 + bdv \<up> 2=0)*)
9.446 - Rule.Thm("d3_reduce_equation13",ThmC.numerals_to_Free @{thm d3_reduce_equation13}),
9.447 + \<^rule_thm>\<open>d3_reduce_equation13\<close>,
9.448 (* b*bdv \<up> 2 + c*bdv \<up> 3=0) =
9.449 (bdv=0 | ( b*bdv + c*bdv \<up> 2=0)*)
9.450 - Rule.Thm("d3_reduce_equation14",ThmC.numerals_to_Free @{thm d3_reduce_equation14}),
9.451 + \<^rule_thm>\<open>d3_reduce_equation14\<close>,
9.452 (* bdv \<up> 2 + c*bdv \<up> 3=0) =
9.453 (bdv=0 | ( bdv + c*bdv \<up> 2=0)*)
9.454 - Rule.Thm("d3_reduce_equation15",ThmC.numerals_to_Free @{thm d3_reduce_equation15}),
9.455 + \<^rule_thm>\<open>d3_reduce_equation15\<close>,
9.456 (* b*bdv \<up> 2 + bdv \<up> 3=0) =
9.457 (bdv=0 | ( b*bdv + bdv \<up> 2=0)*)
9.458 - Rule.Thm("d3_reduce_equation16",ThmC.numerals_to_Free @{thm d3_reduce_equation16}),
9.459 + \<^rule_thm>\<open>d3_reduce_equation16\<close>,
9.460 (* bdv \<up> 2 + bdv \<up> 3=0) =
9.461 (bdv=0 | ( bdv + bdv \<up> 2=0)*)
9.462 - Rule.Thm("d3_isolate_add1",ThmC.numerals_to_Free @{thm d3_isolate_add1}),
9.463 + \<^rule_thm>\<open>d3_isolate_add1\<close>,
9.464 (*[|Not(bdv occurs_in a)|] ==> (a + b*bdv \<up> 3=0) =
9.465 (bdv=0 | (b*bdv \<up> 3=a)*)
9.466 - Rule.Thm("d3_isolate_add2",ThmC.numerals_to_Free @{thm d3_isolate_add2}),
9.467 + \<^rule_thm>\<open>d3_isolate_add2\<close>,
9.468 (*[|Not(bdv occurs_in a)|] ==> (a + bdv \<up> 3=0) =
9.469 (bdv=0 | ( bdv \<up> 3=a)*)
9.470 - Rule.Thm("d3_isolate_div",ThmC.numerals_to_Free @{thm d3_isolate_div}),
9.471 + \<^rule_thm>\<open>d3_isolate_div\<close>,
9.472 (*[|Not(b=0)|] ==> (b*bdv \<up> 3=c) = (bdv \<up> 3=c/b*)
9.473 - Rule.Thm("d3_root_equation2",ThmC.numerals_to_Free @{thm d3_root_equation2}),
9.474 + \<^rule_thm>\<open>d3_root_equation2\<close>,
9.475 (*(bdv \<up> 3=0) = (bdv=0) *)
9.476 - Rule.Thm("d3_root_equation1",ThmC.numerals_to_Free @{thm d3_root_equation1})
9.477 + \<^rule_thm>\<open>d3_root_equation1\<close>
9.478 (*bdv \<up> 3=c) = (bdv = nroot 3 c*)
9.479 ],
9.480 scr = Rule.Empty_Prog
9.481 @@ -749,7 +749,7 @@
9.482 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
9.483 srls = Rule_Set.Empty, calc = [], errpatts = [],
9.484 rules =
9.485 - [Rule.Thm("d4_sub_u1",ThmC.numerals_to_Free @{thm d4_sub_u1})
9.486 + [\<^rule_thm>\<open>d4_sub_u1\<close>
9.487 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
9.488 ],
9.489 scr = Rule.Empty_Prog
9.490 @@ -1225,17 +1225,17 @@
9.491 ord_make_polynomial_in false @{theory "Poly"}),
9.492 erls = Rule_Set.empty,srls = Rule_Set.Empty,
9.493 calc = [], errpatts = [],
9.494 - rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
9.495 + rules = [\<^rule_thm>\<open>mult.commute\<close>,
9.496 (* z * w = w * z *)
9.497 - Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
9.498 + \<^rule_thm>\<open>real_mult_left_commute\<close>,
9.499 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
9.500 - Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
9.501 + \<^rule_thm>\<open>mult.assoc\<close>,
9.502 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
9.503 - Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
9.504 + \<^rule_thm>\<open>add.commute\<close>,
9.505 (*z + w = w + z*)
9.506 - Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
9.507 + \<^rule_thm>\<open>add.left_commute\<close>,
9.508 (*x + (y + z) = y + (x + z)*)
9.509 - Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc})
9.510 + \<^rule_thm>\<open>add.assoc\<close>
9.511 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
9.512 ], scr = Rule.Empty_Prog});
9.513
9.514 @@ -1246,30 +1246,30 @@
9.515 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
9.516 erls = Rule_Set.empty,srls = Rule_Set.Empty,
9.517 calc = [], errpatts = [],
9.518 - rules = [Rule.Thm ("bdv_collect_1",ThmC.numerals_to_Free @{thm bdv_collect_1}),
9.519 - Rule.Thm ("bdv_collect_2",ThmC.numerals_to_Free @{thm bdv_collect_2}),
9.520 - Rule.Thm ("bdv_collect_3",ThmC.numerals_to_Free @{thm bdv_collect_3}),
9.521 + rules = [\<^rule_thm>\<open>bdv_collect_1\<close>,
9.522 + \<^rule_thm>\<open>bdv_collect_2\<close>,
9.523 + \<^rule_thm>\<open>bdv_collect_3\<close>,
9.524
9.525 - Rule.Thm ("bdv_collect_assoc1_1",ThmC.numerals_to_Free @{thm bdv_collect_assoc1_1}),
9.526 - Rule.Thm ("bdv_collect_assoc1_2",ThmC.numerals_to_Free @{thm bdv_collect_assoc1_2}),
9.527 - Rule.Thm ("bdv_collect_assoc1_3",ThmC.numerals_to_Free @{thm bdv_collect_assoc1_3}),
9.528 + \<^rule_thm>\<open>bdv_collect_assoc1_1\<close>,
9.529 + \<^rule_thm>\<open>bdv_collect_assoc1_2\<close>,
9.530 + \<^rule_thm>\<open>bdv_collect_assoc1_3\<close>,
9.531
9.532 - Rule.Thm ("bdv_collect_assoc2_1",ThmC.numerals_to_Free @{thm bdv_collect_assoc2_1}),
9.533 - Rule.Thm ("bdv_collect_assoc2_2",ThmC.numerals_to_Free @{thm bdv_collect_assoc2_2}),
9.534 - Rule.Thm ("bdv_collect_assoc2_3",ThmC.numerals_to_Free @{thm bdv_collect_assoc2_3}),
9.535 + \<^rule_thm>\<open>bdv_collect_assoc2_1\<close>,
9.536 + \<^rule_thm>\<open>bdv_collect_assoc2_2\<close>,
9.537 + \<^rule_thm>\<open>bdv_collect_assoc2_3\<close>,
9.538
9.539
9.540 - Rule.Thm ("bdv_n_collect_1",ThmC.numerals_to_Free @{thm bdv_n_collect_1}),
9.541 - Rule.Thm ("bdv_n_collect_2",ThmC.numerals_to_Free @{thm bdv_n_collect_2}),
9.542 - Rule.Thm ("bdv_n_collect_3",ThmC.numerals_to_Free @{thm bdv_n_collect_3}),
9.543 + \<^rule_thm>\<open>bdv_n_collect_1\<close>,
9.544 + \<^rule_thm>\<open>bdv_n_collect_2\<close>,
9.545 + \<^rule_thm>\<open>bdv_n_collect_3\<close>,
9.546
9.547 - Rule.Thm ("bdv_n_collect_assoc1_1",ThmC.numerals_to_Free @{thm bdv_n_collect_assoc1_1}),
9.548 - Rule.Thm ("bdv_n_collect_assoc1_2",ThmC.numerals_to_Free @{thm bdv_n_collect_assoc1_2}),
9.549 - Rule.Thm ("bdv_n_collect_assoc1_3",ThmC.numerals_to_Free @{thm bdv_n_collect_assoc1_3}),
9.550 + \<^rule_thm>\<open>bdv_n_collect_assoc1_1\<close>,
9.551 + \<^rule_thm>\<open>bdv_n_collect_assoc1_2\<close>,
9.552 + \<^rule_thm>\<open>bdv_n_collect_assoc1_3\<close>,
9.553
9.554 - Rule.Thm ("bdv_n_collect_assoc2_1",ThmC.numerals_to_Free @{thm bdv_n_collect_assoc2_1}),
9.555 - Rule.Thm ("bdv_n_collect_assoc2_2",ThmC.numerals_to_Free @{thm bdv_n_collect_assoc2_2}),
9.556 - Rule.Thm ("bdv_n_collect_assoc2_3",ThmC.numerals_to_Free @{thm bdv_n_collect_assoc2_3})
9.557 + \<^rule_thm>\<open>bdv_n_collect_assoc2_1\<close>,
9.558 + \<^rule_thm>\<open>bdv_n_collect_assoc2_2\<close>,
9.559 + \<^rule_thm>\<open>bdv_n_collect_assoc2_3\<close>
9.560 ], scr = Rule.Empty_Prog});
9.561
9.562 \<close>
9.563 @@ -1286,7 +1286,7 @@
9.564 Rule.Rls_ simplify_power,
9.565 Rule.Rls_ collect_numerals,
9.566 Rule.Rls_ reduce_012,
9.567 - Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
9.568 + \<^rule_thm>\<open>realpow_oneI\<close>,
9.569 Rule.Rls_ discard_parentheses,
9.570 Rule.Rls_ collect_bdv
9.571 ],
9.572 @@ -1298,12 +1298,12 @@
9.573 val separate_bdvs =
9.574 Rule_Set.append_rules "separate_bdvs"
9.575 collect_bdv
9.576 - [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
9.577 + [\<^rule_thm>\<open>separate_bdv\<close>,
9.578 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
9.579 - Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
9.580 - Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
9.581 + \<^rule_thm>\<open>separate_bdv_n\<close>,
9.582 + \<^rule_thm>\<open>separate_1_bdv\<close>,
9.583 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
9.584 - Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n}),
9.585 + \<^rule_thm>\<open>separate_1_bdv_n\<close>,
9.586 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
9.587 Rule.Thm ("add_divide_distrib",
9.588 ThmC.numerals_to_Free @{thm add_divide_distrib})
10.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Sat Jun 12 14:29:10 2021 +0200
10.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Sat Jun 12 18:06:27 2021 +0200
10.3 @@ -200,21 +200,21 @@
10.4 Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [],
10.5 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
10.6 erls = erls_ordne_alphabetisch,
10.7 - rules = [Rule.Thm ("tausche_plus",ThmC.numerals_to_Free @{thm tausche_plus}),
10.8 + rules = [\<^rule_thm>\<open>tausche_plus\<close>,
10.9 (*"b kleiner a ==> (b + a) = (a + b)"*)
10.10 - Rule.Thm ("tausche_minus",ThmC.numerals_to_Free @{thm tausche_minus}),
10.11 + \<^rule_thm>\<open>tausche_minus\<close>,
10.12 (*"b kleiner a ==> (b - a) = (-a + b)"*)
10.13 - Rule.Thm ("tausche_vor_plus",ThmC.numerals_to_Free @{thm tausche_vor_plus}),
10.14 + \<^rule_thm>\<open>tausche_vor_plus\<close>,
10.15 (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
10.16 - Rule.Thm ("tausche_vor_minus",ThmC.numerals_to_Free @{thm tausche_vor_minus}),
10.17 + \<^rule_thm>\<open>tausche_vor_minus\<close>,
10.18 (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
10.19 - Rule.Thm ("tausche_plus_plus",ThmC.numerals_to_Free @{thm tausche_plus_plus}),
10.20 + \<^rule_thm>\<open>tausche_plus_plus\<close>,
10.21 (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
10.22 - Rule.Thm ("tausche_plus_minus",ThmC.numerals_to_Free @{thm tausche_plus_minus}),
10.23 + \<^rule_thm>\<open>tausche_plus_minus\<close>,
10.24 (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
10.25 - Rule.Thm ("tausche_minus_plus",ThmC.numerals_to_Free @{thm tausche_minus_plus}),
10.26 + \<^rule_thm>\<open>tausche_minus_plus\<close>,
10.27 (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
10.28 - Rule.Thm ("tausche_minus_minus",ThmC.numerals_to_Free @{thm tausche_minus_minus})
10.29 + \<^rule_thm>\<open>tausche_minus_minus\<close>
10.30 (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
10.31 ], scr = Rule.Empty_Prog};
10.32
10.33 @@ -225,42 +225,42 @@
10.34 [\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")],
10.35 srls = Rule_Set.Empty, calc = [], errpatts = [],
10.36 rules =
10.37 - [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
10.38 + [\<^rule_thm>\<open>real_num_collect\<close>,
10.39 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
10.40 - Rule.Thm ("real_num_collect_assoc_r",ThmC.numerals_to_Free @{thm real_num_collect_assoc_r}),
10.41 + \<^rule_thm>\<open>real_num_collect_assoc_r\<close>,
10.42 (*"[| l is_const; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
10.43 - Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
10.44 + \<^rule_thm>\<open>real_one_collect\<close>,
10.45 (*"m is_const ==> n + m * n = (1 + m) * n"*)
10.46 - Rule.Thm ("real_one_collect_assoc_r",ThmC.numerals_to_Free @{thm real_one_collect_assoc_r}),
10.47 + \<^rule_thm>\<open>real_one_collect_assoc_r\<close>,
10.48 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
10.49
10.50
10.51 - Rule.Thm ("subtrahiere",ThmC.numerals_to_Free @{thm subtrahiere}),
10.52 + \<^rule_thm>\<open>subtrahiere\<close>,
10.53 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
10.54 - Rule.Thm ("subtrahiere_von_1",ThmC.numerals_to_Free @{thm subtrahiere_von_1}),
10.55 + \<^rule_thm>\<open>subtrahiere_von_1\<close>,
10.56 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
10.57 - Rule.Thm ("subtrahiere_1",ThmC.numerals_to_Free @{thm subtrahiere_1}),
10.58 + \<^rule_thm>\<open>subtrahiere_1\<close>,
10.59 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
10.60
10.61 - Rule.Thm ("subtrahiere_x_plus_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_plus_minus}),
10.62 + \<^rule_thm>\<open>subtrahiere_x_plus_minus\<close>,
10.63 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
10.64 - Rule.Thm ("subtrahiere_x_plus1_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_plus1_minus}),
10.65 + \<^rule_thm>\<open>subtrahiere_x_plus1_minus\<close>,
10.66 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
10.67 - Rule.Thm ("subtrahiere_x_plus_minus1",ThmC.numerals_to_Free @{thm subtrahiere_x_plus_minus1}),
10.68 + \<^rule_thm>\<open>subtrahiere_x_plus_minus1\<close>,
10.69 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
10.70
10.71 - Rule.Thm ("subtrahiere_x_minus_plus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_plus}),
10.72 + \<^rule_thm>\<open>subtrahiere_x_minus_plus\<close>,
10.73 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
10.74 - Rule.Thm ("subtrahiere_x_minus1_plus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus1_plus}),
10.75 + \<^rule_thm>\<open>subtrahiere_x_minus1_plus\<close>,
10.76 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
10.77 - Rule.Thm ("subtrahiere_x_minus_plus1",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_plus1}),
10.78 + \<^rule_thm>\<open>subtrahiere_x_minus_plus1\<close>,
10.79 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
10.80
10.81 - Rule.Thm ("subtrahiere_x_minus_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_minus}),
10.82 + \<^rule_thm>\<open>subtrahiere_x_minus_minus\<close>,
10.83 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
10.84 - Rule.Thm ("subtrahiere_x_minus1_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus1_minus}),
10.85 + \<^rule_thm>\<open>subtrahiere_x_minus1_minus\<close>,
10.86 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
10.87 - Rule.Thm ("subtrahiere_x_minus_minus1",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_minus1}),
10.88 + \<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>,
10.89 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
10.90
10.91 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
10.92 @@ -268,18 +268,18 @@
10.93
10.94 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
10.95 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
10.96 - Rule.Thm ("real_mult_2_assoc_r",ThmC.numerals_to_Free @{thm real_mult_2_assoc_r}),
10.97 + \<^rule_thm>\<open>real_mult_2_assoc_r\<close>,
10.98 (*"(k + z1) + z1 = k + 2 * z1"*)
10.99 \<^rule_thm_sym>\<open>real_mult_2\<close>,
10.100 (*"z1 + z1 = 2 * z1"*)
10.101
10.102 - Rule.Thm ("addiere_vor_minus",ThmC.numerals_to_Free @{thm addiere_vor_minus}),
10.103 + \<^rule_thm>\<open>addiere_vor_minus\<close>,
10.104 (*"[| l is_const; m is_const |] ==> -(l * v) + m * v = (-l + m) *v"*)
10.105 - Rule.Thm ("addiere_eins_vor_minus",ThmC.numerals_to_Free @{thm addiere_eins_vor_minus}),
10.106 + \<^rule_thm>\<open>addiere_eins_vor_minus\<close>,
10.107 (*"[| m is_const |] ==> - v + m * v = (-1 + m) * v"*)
10.108 - Rule.Thm ("subtrahiere_vor_minus",ThmC.numerals_to_Free @{thm subtrahiere_vor_minus}),
10.109 + \<^rule_thm>\<open>subtrahiere_vor_minus\<close>,
10.110 (*"[| l is_const; m is_const |] ==> -(l * v) - m * v = (-l - m) *v"*)
10.111 - Rule.Thm ("subtrahiere_eins_vor_minus",ThmC.numerals_to_Free @{thm subtrahiere_eins_vor_minus})
10.112 + \<^rule_thm>\<open>subtrahiere_eins_vor_minus\<close>
10.113 (*"[| m is_const |] ==> - v - m * v = (-1 - m) * v"*)
10.114
10.115 ], scr = Rule.Empty_Prog};
10.116 @@ -289,26 +289,26 @@
10.117 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
10.118 erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty
10.119 [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner "")],
10.120 - rules = [Rule.Thm ("vorzeichen_minus_weg1",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg1}),
10.121 + rules = [\<^rule_thm>\<open>vorzeichen_minus_weg1\<close>,
10.122 (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
10.123 - Rule.Thm ("vorzeichen_minus_weg2",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg2}),
10.124 + \<^rule_thm>\<open>vorzeichen_minus_weg2\<close>,
10.125 (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
10.126 - Rule.Thm ("vorzeichen_minus_weg3",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg3}),
10.127 + \<^rule_thm>\<open>vorzeichen_minus_weg3\<close>,
10.128 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
10.129 - Rule.Thm ("vorzeichen_minus_weg4",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg4}),
10.130 + \<^rule_thm>\<open>vorzeichen_minus_weg4\<close>,
10.131 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
10.132
10.133 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
10.134
10.135 - Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
10.136 + \<^rule_thm>\<open>mult_zero_left\<close>,
10.137 (*"0 * z = 0"*)
10.138 - Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
10.139 + \<^rule_thm>\<open>mult_1_left\<close>,
10.140 (*"1 * z = z"*)
10.141 - Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
10.142 + \<^rule_thm>\<open>add_0_left\<close>,
10.143 (*"0 + z = z"*)
10.144 - Rule.Thm ("null_minus",ThmC.numerals_to_Free @{thm null_minus}),
10.145 + \<^rule_thm>\<open>null_minus\<close>,
10.146 (*"0 - a = -a"*)
10.147 - Rule.Thm ("vor_minus_mal",ThmC.numerals_to_Free @{thm vor_minus_mal})
10.148 + \<^rule_thm>\<open>vor_minus_mal\<close>
10.149 (*"- a * b = (-a) * b"*)
10.150
10.151 (*Rule.Thm ("",ThmC.numerals_to_Free @{}),*)
10.152 @@ -320,25 +320,25 @@
10.153 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
10.154 rules = [\<^rule_thm_sym>\<open>add.assoc\<close>,
10.155 (*"a + (b + c) = (a + b) + c"*)
10.156 - Rule.Thm ("klammer_plus_minus",ThmC.numerals_to_Free @{thm klammer_plus_minus}),
10.157 + \<^rule_thm>\<open>klammer_plus_minus\<close>,
10.158 (*"a + (b - c) = (a + b) - c"*)
10.159 - Rule.Thm ("klammer_minus_plus",ThmC.numerals_to_Free @{thm klammer_minus_plus}),
10.160 + \<^rule_thm>\<open>klammer_minus_plus\<close>,
10.161 (*"a - (b + c) = (a - b) - c"*)
10.162 - Rule.Thm ("klammer_minus_minus",ThmC.numerals_to_Free @{thm klammer_minus_minus})
10.163 + \<^rule_thm>\<open>klammer_minus_minus\<close>
10.164 (*"a - (b - c) = (a - b) + c"*)
10.165 ], scr = Rule.Empty_Prog};
10.166
10.167 val klammern_ausmultiplizieren =
10.168 Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [],
10.169 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
10.170 - rules = [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
10.171 + rules = [\<^rule_thm>\<open>distrib_right\<close>,
10.172 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
10.173 - Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
10.174 + \<^rule_thm>\<open>distrib_left\<close>,
10.175 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
10.176
10.177 - Rule.Thm ("klammer_mult_minus",ThmC.numerals_to_Free @{thm klammer_mult_minus}),
10.178 + \<^rule_thm>\<open>klammer_mult_minus\<close>,
10.179 (*"a * (b - c) = a * b - a * c"*)
10.180 - Rule.Thm ("klammer_minus_mult",ThmC.numerals_to_Free @{thm klammer_minus_mult})
10.181 + \<^rule_thm>\<open>klammer_minus_mult\<close>
10.182 (*"(b - c) * a = b * a - c * a"*)
10.183
10.184 (*Rule.Thm ("",ThmC.numerals_to_Free @{}),
10.185 @@ -352,13 +352,13 @@
10.186 [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""),
10.187 \<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "")
10.188 ],
10.189 - rules = [Rule.Thm ("tausche_mal",ThmC.numerals_to_Free @{thm tausche_mal}),
10.190 + rules = [\<^rule_thm>\<open>tausche_mal\<close>,
10.191 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
10.192 - Rule.Thm ("tausche_vor_mal",ThmC.numerals_to_Free @{thm tausche_vor_mal}),
10.193 + \<^rule_thm>\<open>tausche_vor_mal\<close>,
10.194 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
10.195 - Rule.Thm ("tausche_mal_mal",ThmC.numerals_to_Free @{thm tausche_mal_mal}),
10.196 + \<^rule_thm>\<open>tausche_mal_mal\<close>,
10.197 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
10.198 - Rule.Thm ("x_quadrat",ThmC.numerals_to_Free @{thm x_quadrat})
10.199 + \<^rule_thm>\<open>x_quadrat\<close>
10.200 (*"(x * a) * a = x * a \<up> 2"*)
10.201
10.202 (*Rule.Thm ("",ThmC.numerals_to_Free @{}),
10.203 @@ -414,13 +414,13 @@
10.204 Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty
10.205 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
10.206 \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
10.207 - Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
10.208 + \<^rule_thm>\<open>or_true\<close>,
10.209 (*"(?a | True) = True"*)
10.210 - Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
10.211 + \<^rule_thm>\<open>or_false\<close>,
10.212 (*"(?a | False) = ?a"*)
10.213 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
10.214 + \<^rule_thm>\<open>not_true\<close>,
10.215 (*"(~ True) = False"*)
10.216 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
10.217 + \<^rule_thm>\<open>not_false\<close>
10.218 (*"(~ False) = True"*)],
10.219 SOME "Vereinfache t_t", [["simplification", "for_polynomials", "with_minus"]])),
10.220 (Problem.prep_input @{theory} "pbl_vereinf_poly_klammer" [] Problem.id_empty
10.221 @@ -435,13 +435,13 @@
10.222 Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty
10.223 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
10.224 \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
10.225 - Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
10.226 + \<^rule_thm>\<open>or_true\<close>,
10.227 (*"(?a | True) = True"*)
10.228 - Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
10.229 + \<^rule_thm>\<open>or_false\<close>,
10.230 (*"(?a | False) = ?a"*)
10.231 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
10.232 + \<^rule_thm>\<open>not_true\<close>,
10.233 (*"(~ True) = False"*)
10.234 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
10.235 + \<^rule_thm>\<open>not_false\<close>
10.236 (*"(~ False) = True"*)],
10.237 SOME "Vereinfache t_t",
10.238 [["simplification", "for_polynomials", "with_parentheses"]])),
10.239 @@ -497,13 +497,13 @@
10.240 prls = Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty
10.241 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
10.242 \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
10.243 - Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
10.244 + \<^rule_thm>\<open>and_true\<close>,
10.245 (*"(?a & True) = ?a"*)
10.246 - Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
10.247 + \<^rule_thm>\<open>and_false\<close>,
10.248 (*"(?a & False) = False"*)
10.249 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
10.250 + \<^rule_thm>\<open>not_true\<close>,
10.251 (*"(~ True) = False"*)
10.252 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
10.253 + \<^rule_thm>\<open>not_false\<close>
10.254 (*"(~ False) = True"*)],
10.255 crls = Rule_Set.empty, errpats = [], nrls = rls_p_33},
10.256 @{thm simplify.simps})]
11.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sat Jun 12 14:29:10 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Sat Jun 12 18:06:27 2021 +0200
11.3 @@ -86,12 +86,12 @@
11.4 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
11.5 \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in ""),
11.6 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
11.7 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
11.8 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
11.9 - Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
11.10 - Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
11.11 - Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
11.12 - Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false})
11.13 + \<^rule_thm>\<open>not_true\<close>,
11.14 + \<^rule_thm>\<open>not_false\<close>,
11.15 + \<^rule_thm>\<open>and_true\<close>,
11.16 + \<^rule_thm>\<open>and_false\<close>,
11.17 + \<^rule_thm>\<open>or_true\<close>,
11.18 + \<^rule_thm>\<open>or_false\<close>
11.19 ];
11.20
11.21 \<close> ML \<open>
11.22 @@ -102,8 +102,8 @@
11.23 (Rule_Set.append_rules "is_ratequation_in"
11.24 Poly_erls [(*\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),*)
11.25 \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in "")]))
11.26 - [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)
11.27 - Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})]; (*WN: ein Hack*)
11.28 + [\<^rule_thm>\<open>and_commute\<close>, (*WN: ein Hack*)
11.29 + \<^rule_thm>\<open>or_commute\<close>]; (*WN: ein Hack*)
11.30
11.31 \<close> ML \<open>
11.32 val RatEq_crls =
11.33 @@ -112,19 +112,19 @@
11.34 (Rule_Set.append_rules "is_ratequation_in"
11.35 Poly_erls [(*\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),*)
11.36 \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in "")]))
11.37 - [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)
11.38 - Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})]; (*WN: ein Hack*)
11.39 + [\<^rule_thm>\<open>and_commute\<close>, (*WN: ein Hack*)
11.40 + \<^rule_thm>\<open>or_commute\<close>]; (*WN: ein Hack*)
11.41
11.42 val RatEq_eliminate = prep_rls'(
11.43 Rule_Def.Repeat
11.44 {id = "RatEq_eliminate", preconds = [], rew_ord = ("termlessI", termlessI), erls = rateq_erls,
11.45 srls = Rule_Set.Empty, calc = [], errpatts = [],
11.46 rules = [
11.47 - Rule.Thm("rat_mult_denominator_both",ThmC.numerals_to_Free @{thm rat_mult_denominator_both}),
11.48 + \<^rule_thm>\<open>rat_mult_denominator_both\<close>,
11.49 (* a/b=c/d -> ad=cb *)
11.50 - Rule.Thm("rat_mult_denominator_left",ThmC.numerals_to_Free @{thm rat_mult_denominator_left}),
11.51 + \<^rule_thm>\<open>rat_mult_denominator_left\<close>,
11.52 (* a =c/d -> ad=c *)
11.53 - Rule.Thm("rat_mult_denominator_right",ThmC.numerals_to_Free @{thm rat_mult_denominator_right})
11.54 + \<^rule_thm>\<open>rat_mult_denominator_right\<close>
11.55 (* a/b=c -> a=cb *)
11.56 ],
11.57 scr = Rule.Empty_Prog});
11.58 @@ -135,21 +135,21 @@
11.59 {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI), erls = rateq_erls,
11.60 srls = Rule_Set.Empty, calc = [], errpatts = [],
11.61 rules = [
11.62 - Rule.Thm("real_rat_mult_1",ThmC.numerals_to_Free @{thm real_rat_mult_1}),
11.63 + \<^rule_thm>\<open>real_rat_mult_1\<close>,
11.64 (*a*(b/c) = (a*b)/c*)
11.65 - Rule.Thm("real_rat_mult_2",ThmC.numerals_to_Free @{thm real_rat_mult_2}),
11.66 + \<^rule_thm>\<open>real_rat_mult_2\<close>,
11.67 (*(a/b)*(c/d) = (a*c)/(b*d)*)
11.68 - Rule.Thm("real_rat_mult_3",ThmC.numerals_to_Free @{thm real_rat_mult_3}),
11.69 + \<^rule_thm>\<open>real_rat_mult_3\<close>,
11.70 (* (a/b)*c = (a*c)/b*)
11.71 - Rule.Thm("real_rat_pow",ThmC.numerals_to_Free @{thm real_rat_pow}),
11.72 + \<^rule_thm>\<open>real_rat_pow\<close>,
11.73 (*(a/b) \<up> 2 = a \<up> 2/b \<up> 2*)
11.74 - Rule.Thm("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
11.75 + \<^rule_thm>\<open>real_diff_minus\<close>,
11.76 (* a - b = a + (-1) * b *)
11.77 - Rule.Thm("rat_double_rat_1",ThmC.numerals_to_Free @{thm rat_double_rat_1}),
11.78 + \<^rule_thm>\<open>rat_double_rat_1\<close>,
11.79 (* (a / (c/d) = (a*d) / c) *)
11.80 - Rule.Thm("rat_double_rat_2",ThmC.numerals_to_Free @{thm rat_double_rat_2}),
11.81 + \<^rule_thm>\<open>rat_double_rat_2\<close>,
11.82 (* ((a/b) / (c/d) = (a*d) / (b*c)) *)
11.83 - Rule.Thm("rat_double_rat_3",ThmC.numerals_to_Free @{thm rat_double_rat_3})
11.84 + \<^rule_thm>\<open>rat_double_rat_3\<close>
11.85 (* ((a/b) / c = a / (b*c) ) *)],
11.86 scr = Rule.Empty_Prog});
11.87 \<close>
12.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sat Jun 12 14:29:10 2021 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sat Jun 12 18:06:27 2021 +0200
12.3 @@ -396,8 +396,8 @@
12.4 rules =
12.5 [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
12.6 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
12.7 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
12.8 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
12.9 + \<^rule_thm>\<open>not_true\<close>,
12.10 + \<^rule_thm>\<open>not_false\<close>],
12.11 scr = Rule.Empty_Prog});
12.12
12.13 (* simplifies expressions with numerals;
12.14 @@ -413,37 +413,37 @@
12.15
12.16 Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
12.17 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
12.18 - Rule.Thm ("rat_add", ThmC.numerals_to_Free @{thm rat_add}),
12.19 + \<^rule_thm>\<open>rat_add\<close>,
12.20 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
12.21 \a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
12.22 - Rule.Thm ("rat_add1", ThmC.numerals_to_Free @{thm rat_add1}),
12.23 + \<^rule_thm>\<open>rat_add1\<close>,
12.24 (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
12.25 - Rule.Thm ("rat_add2", ThmC.numerals_to_Free @{thm rat_add2}),
12.26 + \<^rule_thm>\<open>rat_add2\<close>,
12.27 (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
12.28 - Rule.Thm ("rat_add3", ThmC.numerals_to_Free @{thm rat_add3}),
12.29 + \<^rule_thm>\<open>rat_add3\<close>,
12.30 (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c"\
12.31 .... is_const to be omitted here FIXME*)
12.32
12.33 - Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
12.34 + \<^rule_thm>\<open>rat_mult\<close>,
12.35 (*a / b * (c / d) = a * c / (b * d)*)
12.36 - Rule.Thm ("times_divide_eq_right", ThmC.numerals_to_Free @{thm times_divide_eq_right}),
12.37 + \<^rule_thm>\<open>times_divide_eq_right\<close>,
12.38 (*?x * (?y / ?z) = ?x * ?y / ?z*)
12.39 - Rule.Thm ("times_divide_eq_left", ThmC.numerals_to_Free @{thm times_divide_eq_left}),
12.40 + \<^rule_thm>\<open>times_divide_eq_left\<close>,
12.41 (*?y / ?z * ?x = ?y * ?x / ?z*)
12.42
12.43 - Rule.Thm ("real_divide_divide1", ThmC.numerals_to_Free @{thm real_divide_divide1}),
12.44 + \<^rule_thm>\<open>real_divide_divide1\<close>,
12.45 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
12.46 - Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
12.47 + \<^rule_thm>\<open>divide_divide_eq_left\<close>,
12.48 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
12.49
12.50 - Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}),
12.51 + \<^rule_thm>\<open>rat_power\<close>,
12.52 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
12.53
12.54 - Rule.Thm ("mult_cross", ThmC.numerals_to_Free @{thm mult_cross}),
12.55 + \<^rule_thm>\<open>mult_cross\<close>,
12.56 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
12.57 - Rule.Thm ("mult_cross1", ThmC.numerals_to_Free @{thm mult_cross1}),
12.58 + \<^rule_thm>\<open>mult_cross1\<close>,
12.59 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
12.60 - Rule.Thm ("mult_cross2", ThmC.numerals_to_Free @{thm mult_cross2})
12.61 + \<^rule_thm>\<open>mult_cross2\<close>
12.62 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
12.63 scr = Rule.Empty_Prog})
12.64 calculate_Poly);
12.65 @@ -479,7 +479,7 @@
12.66 val SOME (t'', asm) = cancel_p_ thy t;
12.67 val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
12.68 val der = der @
12.69 - [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))]
12.70 + [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'', asm))]
12.71 val rs = (Rule.distinct' o (map #1)) der
12.72 val rs = filter_out (ThmC.member'
12.73 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
12.74 @@ -540,7 +540,7 @@
12.75 val SOME (t'', asm) = add_fraction_p_ thy t;
12.76 val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
12.77 val der = der @
12.78 - [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))]
12.79 + [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'',asm))]
12.80 val rs = (Rule.distinct' o (map #1)) der;
12.81 val rs = filter_out (ThmC.member'
12.82 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
12.83 @@ -607,8 +607,8 @@
12.84 rules = [\<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
12.85 \<^rule_eval>\<open>Prog_Expr.is_even\<close> (Prog_Expr.eval_is_even "#is_even_"),
12.86 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
12.87 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
12.88 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
12.89 + \<^rule_thm>\<open>not_false\<close>,
12.90 + \<^rule_thm>\<open>not_true\<close>,
12.91 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
12.92 ],
12.93 scr = Rule.Empty_Prog
12.94 @@ -618,29 +618,29 @@
12.95 val powers = prep_rls'(
12.96 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
12.97 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
12.98 - rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
12.99 + rules = [\<^rule_thm>\<open>realpow_multI\<close>,
12.100 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
12.101 - Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
12.102 + \<^rule_thm>\<open>realpow_pow\<close>,
12.103 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
12.104 - Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
12.105 + \<^rule_thm>\<open>realpow_oneI\<close>,
12.106 (*"r \<up> 1 = r"*)
12.107 - Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}),
12.108 + \<^rule_thm>\<open>realpow_minus_even\<close>,
12.109 (*"n is_even ==> (- r) \<up> n = r \<up> n" ?-->discard_minus?*)
12.110 - Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}),
12.111 + \<^rule_thm>\<open>realpow_minus_odd\<close>,
12.112 (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
12.113
12.114 (*----- collect atoms over * -----*)
12.115 - Rule.Thm ("realpow_two_atom",ThmC.numerals_to_Free @{thm realpow_two_atom}),
12.116 + \<^rule_thm>\<open>realpow_two_atom\<close>,
12.117 (*"r is_atom ==> r * r = r \<up> 2"*)
12.118 - Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
12.119 + \<^rule_thm>\<open>realpow_plus_1\<close>,
12.120 (*"r is_atom ==> r * r \<up> n = r \<up> (n + 1)"*)
12.121 - Rule.Thm ("realpow_addI_atom",ThmC.numerals_to_Free @{thm realpow_addI_atom}),
12.122 + \<^rule_thm>\<open>realpow_addI_atom\<close>,
12.123 (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*)
12.124
12.125 (*----- distribute none-atoms -----*)
12.126 - Rule.Thm ("realpow_def_atom",ThmC.numerals_to_Free @{thm realpow_def_atom}),
12.127 + \<^rule_thm>\<open>realpow_def_atom\<close>,
12.128 (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
12.129 - Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
12.130 + \<^rule_thm>\<open>realpow_eq_oneI\<close>,
12.131 (*"1 \<up> n = 1"*)
12.132 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
12.133 ],
12.134 @@ -651,12 +651,12 @@
12.135 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
12.136 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
12.137 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
12.138 - rules = [Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
12.139 + rules = [\<^rule_thm>\<open>rat_mult\<close>,
12.140 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
12.141 - Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
12.142 + \<^rule_thm>\<open>times_divide_eq_right\<close>,
12.143 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
12.144 otherwise inv.to a / b / c = ...*)
12.145 - Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
12.146 + \<^rule_thm>\<open>times_divide_eq_left\<close>,
12.147 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
12.148 and does not commute a / b * c \<up> 2 !*)
12.149
12.150 @@ -675,28 +675,28 @@
12.151 val reduce_0_1_2 = prep_rls'(
12.152 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
12.153 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
12.154 - rules = [(*Rule.Thm ("divide_1",ThmC.numerals_to_Free @{thm divide_1}),
12.155 + rules = [(*\<^rule_thm>\<open>divide_1\<close>,
12.156 "?x / 1 = ?x" unnecess.for normalform*)
12.157 - Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
12.158 + \<^rule_thm>\<open>mult_1_left\<close>,
12.159 (*"1 * z = z"*)
12.160 - (*Rule.Thm ("real_mult_minus1",ThmC.numerals_to_Free @{thm real_mult_minus1}),
12.161 + (*\<^rule_thm>\<open>real_mult_minus1\<close>,
12.162 "-1 * z = - z"*)
12.163 - (*Rule.Thm ("real_minus_mult_cancel",ThmC.numerals_to_Free @{thm real_minus_mult_cancel}),
12.164 + (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>,
12.165 "- ?x * - ?y = ?x * ?y"*)
12.166
12.167 - Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
12.168 + \<^rule_thm>\<open>mult_zero_left\<close>,
12.169 (*"0 * z = 0"*)
12.170 - Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
12.171 + \<^rule_thm>\<open>add_0_left\<close>,
12.172 (*"0 + z = z"*)
12.173 - (*Rule.Thm ("right_minus",ThmC.numerals_to_Free @{thm right_minus}),
12.174 + (*\<^rule_thm>\<open>right_minus\<close>,
12.175 "?z + - ?z = 0"*)
12.176
12.177 \<^rule_thm_sym>\<open>real_mult_2\<close>,
12.178 (*"z1 + z1 = 2 * z1"*)
12.179 - Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
12.180 + \<^rule_thm>\<open>real_mult_2_assoc\<close>,
12.181 (*"z1 + (z1 + k) = 2 * z1 + k"*)
12.182
12.183 - Rule.Thm ("division_ring_divide_zero",ThmC.numerals_to_Free @{thm division_ring_divide_zero})
12.184 + \<^rule_thm>\<open>division_ring_divide_zero\<close>
12.185 (*"0 / ?x = 0"*)
12.186 ], scr = Rule.Empty_Prog});
12.187
12.188 @@ -741,20 +741,20 @@
12.189 val simplify_rational =
12.190 Rule_Set.merge "simplify_rational" expand_binoms
12.191 (Rule_Set.append_rules "divide" calculate_Rational
12.192 - [Rule.Thm ("div_by_1",ThmC.numerals_to_Free @{thm div_by_1}),
12.193 + [\<^rule_thm>\<open>div_by_1\<close>,
12.194 (*"?x / 1 = ?x"*)
12.195 - Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
12.196 + \<^rule_thm>\<open>rat_mult\<close>,
12.197 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
12.198 - Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
12.199 + \<^rule_thm>\<open>times_divide_eq_right\<close>,
12.200 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
12.201 otherwise inv.to a / b / c = ...*)
12.202 - Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
12.203 + \<^rule_thm>\<open>times_divide_eq_left\<close>,
12.204 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
12.205 - Rule.Thm ("add_minus",ThmC.numerals_to_Free @{thm add_minus}),
12.206 + \<^rule_thm>\<open>add_minus\<close>,
12.207 (*"?a + ?b - ?b = ?a"*)
12.208 - Rule.Thm ("add_minus1",ThmC.numerals_to_Free @{thm add_minus1}),
12.209 + \<^rule_thm>\<open>add_minus1\<close>,
12.210 (*"?a - ?b + ?b = ?a"*)
12.211 - Rule.Thm ("divide_minus1",ThmC.numerals_to_Free @{thm divide_minus1})
12.212 + \<^rule_thm>\<open>divide_minus1\<close>
12.213 (*"?x / -1 = - ?x"*)
12.214 ]);
12.215 \<close>
12.216 @@ -781,9 +781,9 @@
12.217 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
12.218 srls = Rule_Set.Empty, calc = [], errpatts = [],
12.219 rules =
12.220 - [Rule.Thm ("rat_mult_poly_l",ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
12.221 + [\<^rule_thm>\<open>rat_mult_poly_l\<close>,
12.222 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
12.223 - Rule.Thm ("rat_mult_poly_r",ThmC.numerals_to_Free @{thm rat_mult_poly_r})
12.224 + \<^rule_thm>\<open>rat_mult_poly_r\<close>
12.225 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) ],
12.226 scr = Rule.Empty_Prog});
12.227
12.228 @@ -795,22 +795,22 @@
12.229 val rat_mult_div_pow = prep_rls'(
12.230 Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
12.231 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
12.232 - rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
12.233 + rules = [\<^rule_thm>\<open>rat_mult\<close>,
12.234 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
12.235 - Rule.Thm ("rat_mult_poly_l", ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
12.236 + \<^rule_thm>\<open>rat_mult_poly_l\<close>,
12.237 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
12.238 - Rule.Thm ("rat_mult_poly_r", ThmC.numerals_to_Free @{thm rat_mult_poly_r}),
12.239 + \<^rule_thm>\<open>rat_mult_poly_r\<close>,
12.240 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
12.241
12.242 - Rule.Thm ("real_divide_divide1_mg", ThmC.numerals_to_Free @{thm real_divide_divide1_mg}),
12.243 + \<^rule_thm>\<open>real_divide_divide1_mg\<close>,
12.244 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
12.245 - Rule.Thm ("divide_divide_eq_right", ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
12.246 + \<^rule_thm>\<open>divide_divide_eq_right\<close>,
12.247 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
12.248 - Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
12.249 + \<^rule_thm>\<open>divide_divide_eq_left\<close>,
12.250 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
12.251 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
12.252
12.253 - Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
12.254 + \<^rule_thm>\<open>rat_power\<close>
12.255 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
12.256 ],
12.257 scr = Rule.Empty_Prog});
12.258 @@ -819,9 +819,9 @@
12.259 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
12.260 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
12.261 rules =
12.262 - [Rule.Thm ("div_by_1", ThmC.numerals_to_Free @{thm div_by_1}),
12.263 + [\<^rule_thm>\<open>div_by_1\<close>,
12.264 (*"?x / 1 = ?x"*)
12.265 - Rule.Thm ("mult_1_left", ThmC.numerals_to_Free @{thm mult_1_left})
12.266 + \<^rule_thm>\<open>mult_1_left\<close>
12.267 (*"1 * z = z"*)
12.268 ],
12.269 scr = Rule.Empty_Prog});
13.1 --- a/src/Tools/isac/Knowledge/Root.thy Sat Jun 12 14:29:10 2021 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Root.thy Sat Jun 12 18:06:27 2021 +0200
13.3 @@ -162,7 +162,7 @@
13.4 (*-------------------------rulse-------------------------*)
13.5 val Root_crls =
13.6 Rule_Set.append_rules "Root_crls" Atools_erls
13.7 - [Rule.Thm ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
13.8 + [\<^rule_thm>\<open>real_unari_minus\<close>,
13.9 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
13.10 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
13.11 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
13.12 @@ -174,7 +174,7 @@
13.13
13.14 val Root_erls =
13.15 Rule_Set.append_rules "Root_erls" Atools_erls
13.16 - [Rule.Thm ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
13.17 + [\<^rule_thm>\<open>real_unari_minus\<close>,
13.18 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
13.19 \<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
13.20 \<^rule_eval>\<open>Transcendental.powr\<close> (**)(eval_binop "#power_"),
13.21 @@ -192,55 +192,55 @@
13.22 rew_ord = ("sqrt_right", sqrt_right false \<^theory>),
13.23 erls = Atools_erls, srls = Rule_Set.Empty,
13.24 calc = [], errpatts = [],
13.25 - rules = [Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
13.26 + rules = [\<^rule_thm>\<open>real_diff_minus\<close>,
13.27 (*"a - b = a + (-1) * b"*)
13.28
13.29 - Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
13.30 + \<^rule_thm>\<open>distrib_right\<close>,
13.31 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
13.32 - Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
13.33 + \<^rule_thm>\<open>distrib_left\<close>,
13.34 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
13.35 - Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),
13.36 + \<^rule_thm>\<open>left_diff_distrib\<close>,
13.37 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
13.38 - Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),
13.39 + \<^rule_thm>\<open>right_diff_distrib\<close>,
13.40 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
13.41
13.42 - Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
13.43 + \<^rule_thm>\<open>mult_1_left\<close>,
13.44 (*"1 * z = z"*)
13.45 - Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
13.46 + \<^rule_thm>\<open>mult_zero_left\<close>,
13.47 (*"0 * z = 0"*)
13.48 - Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
13.49 + \<^rule_thm>\<open>add_0_left\<close>,
13.50 (*"0 + z = z"*)
13.51
13.52 - Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
13.53 + \<^rule_thm>\<open>mult.commute\<close>,
13.54 (*AC-rewriting*)
13.55 - Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
13.56 + \<^rule_thm>\<open>real_mult_left_commute\<close>,
13.57 (**)
13.58 - Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
13.59 + \<^rule_thm>\<open>mult.assoc\<close>,
13.60 (**)
13.61 - Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
13.62 + \<^rule_thm>\<open>add.commute\<close>,
13.63 (**)
13.64 - Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
13.65 + \<^rule_thm>\<open>add.left_commute\<close>,
13.66 (**)
13.67 - Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
13.68 + \<^rule_thm>\<open>add.assoc\<close>,
13.69 (**)
13.70
13.71 \<^rule_thm_sym>\<open>realpow_twoI\<close>,
13.72 (*"r1 * r1 = r1 \<up> 2"*)
13.73 - Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
13.74 + \<^rule_thm>\<open>realpow_plus_1\<close>,
13.75 (*"r * r \<up> n = r \<up> (n + 1)"*)
13.76 \<^rule_thm_sym>\<open>real_mult_2\<close>,
13.77 (*"z1 + z1 = 2 * z1"*)
13.78 - Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
13.79 + \<^rule_thm>\<open>real_mult_2_assoc\<close>,
13.80 (*"z1 + (z1 + k) = 2 * z1 + k"*)
13.81
13.82 - Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
13.83 + \<^rule_thm>\<open>real_num_collect\<close>,
13.84 (*"[| l is_const; m is_const |]==> l * n + m * n = (l + m) * n"*)
13.85 - Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
13.86 + \<^rule_thm>\<open>real_num_collect_assoc\<close>,
13.87 (*"[| l is_const; m is_const |] ==>
13.88 l * n + (m * n + k) = (l + m) * n + k"*)
13.89 - Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
13.90 + \<^rule_thm>\<open>real_one_collect\<close>,
13.91 (*"m is_const ==> n + m * n = (1 + m) * n"*)
13.92 - Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
13.93 + \<^rule_thm>\<open>real_one_collect_assoc\<close>,
13.94 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
13.95
13.96 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
13.97 @@ -260,33 +260,33 @@
13.98 rew_ord = ("termlessI",termlessI),
13.99 erls = Atools_erls, srls = Rule_Set.Empty,
13.100 calc = [], errpatts = [],
13.101 - rules = [Rule.Thm ("real_plus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
13.102 + rules = [\<^rule_thm>\<open>real_plus_binom_pow2\<close>,
13.103 (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
13.104 - Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
13.105 + \<^rule_thm>\<open>real_plus_binom_times\<close>,
13.106 (*"(a + b)*(a + b) = ...*)
13.107 - Rule.Thm ("real_minus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
13.108 + \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
13.109 (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
13.110 - Rule.Thm ("real_minus_binom_times",ThmC.numerals_to_Free @{thm real_minus_binom_times}),
13.111 + \<^rule_thm>\<open>real_minus_binom_times\<close>,
13.112 (*"(a - b)*(a - b) = ...*)
13.113 - Rule.Thm ("real_plus_minus_binom1",ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),
13.114 + \<^rule_thm>\<open>real_plus_minus_binom1\<close>,
13.115 (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
13.116 - Rule.Thm ("real_plus_minus_binom2",ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),
13.117 + \<^rule_thm>\<open>real_plus_minus_binom2\<close>,
13.118 (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
13.119 (*RL 020915*)
13.120 - Rule.Thm ("real_pp_binom_times",ThmC.numerals_to_Free @{thm real_pp_binom_times}),
13.121 + \<^rule_thm>\<open>real_pp_binom_times\<close>,
13.122 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
13.123 - Rule.Thm ("real_pm_binom_times",ThmC.numerals_to_Free @{thm real_pm_binom_times}),
13.124 + \<^rule_thm>\<open>real_pm_binom_times\<close>,
13.125 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
13.126 - Rule.Thm ("real_mp_binom_times",ThmC.numerals_to_Free @{thm real_mp_binom_times}),
13.127 + \<^rule_thm>\<open>real_mp_binom_times\<close>,
13.128 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
13.129 - Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}),
13.130 + \<^rule_thm>\<open>real_mm_binom_times\<close>,
13.131 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
13.132 - Rule.Thm ("realpow_mul",ThmC.numerals_to_Free @{thm realpow_mul}),
13.133 + \<^rule_thm>\<open>realpow_mul\<close>,
13.134 (*(a*b) \<up> n = a \<up> n * b \<up> n*)
13.135
13.136 - Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}), (*"1 * z = z"*)
13.137 - Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}), (*"0 * z = 0"*)
13.138 - Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
13.139 + \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
13.140 + \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
13.141 + \<^rule_thm>\<open>add_0_left\<close>,
13.142 (*"0 + z = z"*)
13.143
13.144 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
13.145 @@ -298,19 +298,19 @@
13.146
13.147 \<^rule_thm_sym>\<open>realpow_twoI\<close>,
13.148 (*"r1 * r1 = r1 \<up> 2"*)
13.149 - Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
13.150 + \<^rule_thm>\<open>realpow_plus_1\<close>,
13.151 (*"r * r \<up> n = r \<up> (n + 1)"*)
13.152 - Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
13.153 + \<^rule_thm>\<open>real_mult_2_assoc\<close>,
13.154 (*"z1 + (z1 + k) = 2 * z1 + k"*)
13.155
13.156 - Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
13.157 + \<^rule_thm>\<open>real_num_collect\<close>,
13.158 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
13.159 - Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
13.160 + \<^rule_thm>\<open>real_num_collect_assoc\<close>,
13.161 (*"[| l is_const; m is_const |] ==>
13.162 l * n + (m * n + k) = (l + m) * n + k"*)
13.163 - Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
13.164 + \<^rule_thm>\<open>real_one_collect\<close>,
13.165 (*"m is_const ==> n + m * n = (1 + m) * n"*)
13.166 - Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
13.167 + \<^rule_thm>\<open>real_one_collect_assoc\<close>,
13.168 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
13.169
13.170 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
14.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sat Jun 12 14:29:10 2021 +0200
14.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sat Jun 12 18:06:27 2021 +0200
14.3 @@ -186,21 +186,21 @@
14.4 \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
14.5 \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in ""),
14.6 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
14.7 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
14.8 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
14.9 - Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
14.10 - Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
14.11 - Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
14.12 - Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false})
14.13 + \<^rule_thm>\<open>not_true\<close>,
14.14 + \<^rule_thm>\<open>not_false\<close>,
14.15 + \<^rule_thm>\<open>and_true\<close>,
14.16 + \<^rule_thm>\<open>and_false\<close>,
14.17 + \<^rule_thm>\<open>or_true\<close>,
14.18 + \<^rule_thm>\<open>or_false\<close>
14.19 ];
14.20
14.21 val RootEq_erls =
14.22 Rule_Set.append_rules "RootEq_erls" Root_erls
14.23 - [Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left})];
14.24 + [\<^rule_thm>\<open>divide_divide_eq_left\<close>];
14.25
14.26 val RootEq_crls =
14.27 Rule_Set.append_rules "RootEq_crls" Root_crls
14.28 - [Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left})];
14.29 + [\<^rule_thm>\<open>divide_divide_eq_left\<close>];
14.30
14.31 val rooteq_srls =
14.32 Rule_Set.append_rules "rooteq_srls" Rule_Set.empty
14.33 @@ -215,13 +215,13 @@
14.34 Rule_Def.Repeat {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
14.35 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.36 rules = [
14.37 - Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1}),
14.38 + \<^rule_thm>\<open>sqrt_square_1\<close>,
14.39 (* (sqrt a) \<up> 2 -> a *)
14.40 - Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
14.41 + \<^rule_thm>\<open>sqrt_square_2\<close>,
14.42 (* sqrt (a \<up> 2) -> a *)
14.43 - Rule.Thm("sqrt_times_root_1",ThmC.numerals_to_Free @{thm sqrt_times_root_1}),
14.44 + \<^rule_thm>\<open>sqrt_times_root_1\<close>,
14.45 (* sqrt a sqrt b -> sqrt(ab) *)
14.46 - Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
14.47 + \<^rule_thm>\<open>sqrt_times_root_2\<close>,
14.48 (* a sqrt b sqrt c -> a sqrt(bc) *)
14.49 Rule.Thm("sqrt_square_equation_both_1",
14.50 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_1}),
14.51 @@ -257,7 +257,7 @@
14.52 Rule.Thm("sqrt_isolate_l_add6",
14.53 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add6}),
14.54 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
14.55 - (*Rule.Thm("sqrt_isolate_l_div",ThmC.numerals_to_Free @{thm sqrt_isolate_l_div}),*)
14.56 + (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
14.57 (* b*sqrt(x) = d sqrt(x) d/b *)
14.58 Rule.Thm("sqrt_isolate_r_add1",
14.59 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add1}),
14.60 @@ -277,7 +277,7 @@
14.61 Rule.Thm("sqrt_isolate_r_add6",
14.62 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add6}),
14.63 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
14.64 - (*Rule.Thm("sqrt_isolate_r_div",ThmC.numerals_to_Free @{thm sqrt_isolate_r_div}),*)
14.65 + (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
14.66 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
14.67 Rule.Thm("sqrt_square_equation_left_1",
14.68 ThmC.numerals_to_Free @{thm sqrt_square_equation_left_1}),
14.69 @@ -285,25 +285,25 @@
14.70 Rule.Thm("sqrt_square_equation_left_2",
14.71 ThmC.numerals_to_Free @{thm sqrt_square_equation_left_2}),
14.72 (* c*sqrt(x)=b -> c^2*x=b^2 *)
14.73 - Rule.Thm("sqrt_square_equation_left_3",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_3}),
14.74 + \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,
14.75 (* c/sqrt(x)=b -> c^2/x=b^2 *)
14.76 - Rule.Thm("sqrt_square_equation_left_4",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_4}),
14.77 + \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>,
14.78 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
14.79 - Rule.Thm("sqrt_square_equation_left_5",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_5}),
14.80 + \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>,
14.81 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
14.82 - Rule.Thm("sqrt_square_equation_left_6",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_6}),
14.83 + \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>,
14.84 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
14.85 - Rule.Thm("sqrt_square_equation_right_1",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_1}),
14.86 + \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>,
14.87 (* a=sqrt(x) ->a^2=x *)
14.88 - Rule.Thm("sqrt_square_equation_right_2",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_2}),
14.89 + \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>,
14.90 (* a=c*sqrt(x) ->a^2=c^2*x *)
14.91 - Rule.Thm("sqrt_square_equation_right_3",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_3}),
14.92 + \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>,
14.93 (* a=c/sqrt(x) ->a^2=c^2/x *)
14.94 - Rule.Thm("sqrt_square_equation_right_4",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_4}),
14.95 + \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>,
14.96 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
14.97 - Rule.Thm("sqrt_square_equation_right_5",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_5}),
14.98 + \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>,
14.99 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
14.100 - Rule.Thm("sqrt_square_equation_right_6",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_6})
14.101 + \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>
14.102 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
14.103 ],scr = Rule.Empty_Prog
14.104 });
14.105 @@ -315,39 +315,39 @@
14.106 rew_ord = ("termlessI",termlessI),
14.107 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.108 rules = [
14.109 - Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1}),
14.110 + \<^rule_thm>\<open>sqrt_square_1\<close>,
14.111 (* (sqrt a) \<up> 2 -> a *)
14.112 - Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
14.113 + \<^rule_thm>\<open>sqrt_square_2\<close>,
14.114 (* sqrt (a \<up> 2) -> a *)
14.115 - Rule.Thm("sqrt_times_root_1",ThmC.numerals_to_Free @{thm sqrt_times_root_1}),
14.116 + \<^rule_thm>\<open>sqrt_times_root_1\<close>,
14.117 (* sqrt a sqrt b -> sqrt(ab) *)
14.118 - Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
14.119 + \<^rule_thm>\<open>sqrt_times_root_2\<close>,
14.120 (* a sqrt b sqrt c -> a sqrt(bc) *)
14.121 - Rule.Thm("sqrt_isolate_l_add1",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add1}),
14.122 + \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>,
14.123 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
14.124 - Rule.Thm("sqrt_isolate_l_add2",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add2}),
14.125 + \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>,
14.126 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
14.127 - Rule.Thm("sqrt_isolate_l_add3",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add3}),
14.128 + \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>,
14.129 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
14.130 - Rule.Thm("sqrt_isolate_l_add4",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add4}),
14.131 + \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>,
14.132 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
14.133 - Rule.Thm("sqrt_isolate_l_add5",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add5}),
14.134 + \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>,
14.135 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
14.136 - Rule.Thm("sqrt_isolate_l_add6",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add6}),
14.137 + \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>,
14.138 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
14.139 - (*Rule.Thm("sqrt_isolate_l_div",ThmC.numerals_to_Free @{thm sqrt_isolate_l_div}),*)
14.140 + (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
14.141 (* b*sqrt(x) = d sqrt(x) d/b *)
14.142 - Rule.Thm("sqrt_square_equation_left_1",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_1}),
14.143 + \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>,
14.144 (* sqrt(x)=b -> x=b^2 *)
14.145 - Rule.Thm("sqrt_square_equation_left_2",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_2}),
14.146 + \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>,
14.147 (* a*sqrt(x)=b -> a^2*x=b^2*)
14.148 - Rule.Thm("sqrt_square_equation_left_3",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_3}),
14.149 + \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,
14.150 (* c/sqrt(x)=b -> c^2/x=b^2 *)
14.151 - Rule.Thm("sqrt_square_equation_left_4",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_4}),
14.152 + \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>,
14.153 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
14.154 - Rule.Thm("sqrt_square_equation_left_5",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_5}),
14.155 + \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>,
14.156 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
14.157 - Rule.Thm("sqrt_square_equation_left_6",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_6})
14.158 + \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>
14.159 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
14.160 ],
14.161 scr = Rule.Empty_Prog
14.162 @@ -361,39 +361,39 @@
14.163 rew_ord = ("termlessI",termlessI),
14.164 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.165 rules = [
14.166 - Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1}),
14.167 + \<^rule_thm>\<open>sqrt_square_1\<close>,
14.168 (* (sqrt a) \<up> 2 -> a *)
14.169 - Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
14.170 + \<^rule_thm>\<open>sqrt_square_2\<close>,
14.171 (* sqrt (a \<up> 2) -> a *)
14.172 - Rule.Thm("sqrt_times_root_1",ThmC.numerals_to_Free @{thm sqrt_times_root_1}),
14.173 + \<^rule_thm>\<open>sqrt_times_root_1\<close>,
14.174 (* sqrt a sqrt b -> sqrt(ab) *)
14.175 - Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
14.176 + \<^rule_thm>\<open>sqrt_times_root_2\<close>,
14.177 (* a sqrt b sqrt c -> a sqrt(bc) *)
14.178 - Rule.Thm("sqrt_isolate_r_add1",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add1}),
14.179 + \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>,
14.180 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
14.181 - Rule.Thm("sqrt_isolate_r_add2",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add2}),
14.182 + \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>,
14.183 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
14.184 - Rule.Thm("sqrt_isolate_r_add3",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add3}),
14.185 + \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>,
14.186 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
14.187 - Rule.Thm("sqrt_isolate_r_add4",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add4}),
14.188 + \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>,
14.189 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
14.190 - Rule.Thm("sqrt_isolate_r_add5",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add5}),
14.191 + \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>,
14.192 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
14.193 - Rule.Thm("sqrt_isolate_r_add6",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add6}),
14.194 + \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>,
14.195 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
14.196 - (*Rule.Thm("sqrt_isolate_r_div",ThmC.numerals_to_Free @{thm sqrt_isolate_r_div}),*)
14.197 + (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
14.198 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
14.199 - Rule.Thm("sqrt_square_equation_right_1",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_1}),
14.200 + \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>,
14.201 (* a=sqrt(x) ->a^2=x *)
14.202 - Rule.Thm("sqrt_square_equation_right_2",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_2}),
14.203 + \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>,
14.204 (* a=c*sqrt(x) ->a^2=c^2*x *)
14.205 - Rule.Thm("sqrt_square_equation_right_3",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_3}),
14.206 + \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>,
14.207 (* a=c/sqrt(x) ->a^2=c^2/x *)
14.208 - Rule.Thm("sqrt_square_equation_right_4",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_4}),
14.209 + \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>,
14.210 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
14.211 - Rule.Thm("sqrt_square_equation_right_5",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_5}),
14.212 + \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>,
14.213 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
14.214 - Rule.Thm("sqrt_square_equation_right_6",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_6})
14.215 + \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>
14.216 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
14.217 ],
14.218 scr = Rule.Empty_Prog
14.219 @@ -405,9 +405,9 @@
14.220 preconds = [], rew_ord = ("termlessI",termlessI),
14.221 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.222 (*asm_thm = [("sqrt_square_1", "")],*)
14.223 - rules = [Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1}),
14.224 + rules = [\<^rule_thm>\<open>real_assoc_1\<close>,
14.225 (* a+(b+c) = a+b+c *)
14.226 - Rule.Thm ("real_assoc_2",ThmC.numerals_to_Free @{thm real_assoc_2}),
14.227 + \<^rule_thm>\<open>real_assoc_2\<close>,
14.228 (* a*(b*c) = a*b*c *)
14.229 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
14.230 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
14.231 @@ -415,17 +415,17 @@
14.232 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
14.233 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
14.234 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
14.235 - Rule.Thm("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
14.236 - Rule.Thm("real_minus_binom_pow2",ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
14.237 - Rule.Thm("realpow_mul",ThmC.numerals_to_Free @{thm realpow_mul}),
14.238 + \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
14.239 + \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
14.240 + \<^rule_thm>\<open>realpow_mul\<close>,
14.241 (* (a * b)^n = a^n * b^n*)
14.242 - Rule.Thm("sqrt_times_root_1",ThmC.numerals_to_Free @{thm sqrt_times_root_1}),
14.243 + \<^rule_thm>\<open>sqrt_times_root_1\<close>,
14.244 (* sqrt b * sqrt c = sqrt(b*c) *)
14.245 - Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
14.246 + \<^rule_thm>\<open>sqrt_times_root_2\<close>,
14.247 (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
14.248 - Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
14.249 + \<^rule_thm>\<open>sqrt_square_2\<close>,
14.250 (* sqrt (a \<up> 2) = a *)
14.251 - Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1})
14.252 + \<^rule_thm>\<open>sqrt_square_1\<close>
14.253 (* sqrt a \<up> 2 = a *)
14.254 ],
14.255 scr = Rule.Empty_Prog
15.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Sat Jun 12 14:29:10 2021 +0200
15.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Sat Jun 12 18:06:27 2021 +0200
15.3 @@ -14,9 +14,9 @@
15.4 (*.calculate numeral groundterms.*)
15.5 val calculate_RootRat =
15.6 Rule_Set.append_rules "calculate_RootRat" calculate_Rational
15.7 - [Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
15.8 + [\<^rule_thm>\<open>distrib_left\<close>,
15.9 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
15.10 - Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
15.11 + \<^rule_thm>\<open>mult_1_left\<close>,
15.12 (* 1 * z = z *)
15.13 \<^rule_thm_sym>\<open>real_mult_minus1\<close>,
15.14 (* "- z1 = -1 * z1" *)
16.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sat Jun 12 14:29:10 2021 +0200
16.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Sat Jun 12 18:06:27 2021 +0200
16.3 @@ -75,12 +75,12 @@
16.4 \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
16.5 \<^rule_eval>\<open>is_rootRatAddTerm_in\<close> (eval_is_rootRatAddTerm_in ""),
16.6 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
16.7 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
16.8 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
16.9 - Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
16.10 - Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
16.11 - Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
16.12 - Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false})];
16.13 + \<^rule_thm>\<open>not_true\<close>,
16.14 + \<^rule_thm>\<open>not_false\<close>,
16.15 + \<^rule_thm>\<open>and_true\<close>,
16.16 + \<^rule_thm>\<open>and_false\<close>,
16.17 + \<^rule_thm>\<open>or_true\<close>,
16.18 + \<^rule_thm>\<open>or_false\<close>];
16.19
16.20 val RooRatEq_erls =
16.21 Rule_Set.merge "RooRatEq_erls" rootrat_erls
16.22 @@ -102,15 +102,15 @@
16.23 rew_ord = ("termlessI",termlessI),
16.24 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.25 rules =
16.26 - [Rule.Thm("rootrat_equation_left_1", ThmC.numerals_to_Free @{thm rootrat_equation_left_1}),
16.27 + [\<^rule_thm>\<open>rootrat_equation_left_1\<close>,
16.28 (* [|c is_rootTerm_in bdv|] ==>
16.29 ( (a + b/c = d) = ( b = (d - a) * c )) *)
16.30 - Rule.Thm("rootrat_equation_left_2",ThmC.numerals_to_Free @{thm rootrat_equation_left_2}),
16.31 + \<^rule_thm>\<open>rootrat_equation_left_2\<close>,
16.32 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
16.33 - Rule.Thm("rootrat_equation_right_1",ThmC.numerals_to_Free @{thm rootrat_equation_right_1}),
16.34 + \<^rule_thm>\<open>rootrat_equation_right_1\<close>,
16.35 (* [|f is_rootTerm_in bdv|] ==>
16.36 ( (a = d + e/f) = ( (a - d) * f = e )) *)
16.37 - Rule.Thm("rootrat_equation_right_2",ThmC.numerals_to_Free @{thm rootrat_equation_right_2})
16.38 + \<^rule_thm>\<open>rootrat_equation_right_2\<close>
16.39 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
16.40 ], scr = Rule.Empty_Prog});
16.41 \<close>
17.1 --- a/src/Tools/isac/Knowledge/Test.thy Sat Jun 12 14:29:10 2021 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sat Jun 12 18:06:27 2021 +0200
17.3 @@ -363,17 +363,17 @@
17.4 Rule_Def.Repeat {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
17.5 erls = Rule_Set.empty, srls = Rule_Set.Empty,
17.6 calc = [], errpatts = [],
17.7 - rules = [Rule.Thm ("refl",ThmC.numerals_to_Free @{thm refl}),
17.8 - Rule.Thm ("order_refl",ThmC.numerals_to_Free @{thm order_refl}),
17.9 - Rule.Thm ("radd_left_cancel_le",ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
17.10 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
17.11 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
17.12 - Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
17.13 - Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
17.14 - Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
17.15 - Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false}),
17.16 - Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}),
17.17 - Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute}),
17.18 + rules = [\<^rule_thm>\<open>refl\<close>,
17.19 + \<^rule_thm>\<open>order_refl\<close>,
17.20 + \<^rule_thm>\<open>radd_left_cancel_le\<close>,
17.21 + \<^rule_thm>\<open>not_true\<close>,
17.22 + \<^rule_thm>\<open>not_false\<close>,
17.23 + \<^rule_thm>\<open>and_true\<close>,
17.24 + \<^rule_thm>\<open>and_false\<close>,
17.25 + \<^rule_thm>\<open>or_true\<close>,
17.26 + \<^rule_thm>\<open>or_false\<close>,
17.27 + \<^rule_thm>\<open>and_commute\<close>,
17.28 + \<^rule_thm>\<open>or_commute\<close>,
17.29
17.30 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
17.31 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
17.32 @@ -397,24 +397,24 @@
17.33 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
17.34 erls=testerls,srls = Rule_Set.empty,
17.35 calc=[], errpatts = [],
17.36 - rules = [Rule.Thm ("refl",ThmC.numerals_to_Free @{thm refl}),
17.37 - Rule.Thm ("order_refl",ThmC.numerals_to_Free @{thm order_refl}),
17.38 - Rule.Thm ("radd_left_cancel_le",ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
17.39 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
17.40 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
17.41 - Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
17.42 - Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
17.43 - Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
17.44 - Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false}),
17.45 - Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}),
17.46 - Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute}),
17.47 + rules = [\<^rule_thm>\<open>refl\<close>,
17.48 + \<^rule_thm>\<open>order_refl\<close>,
17.49 + \<^rule_thm>\<open>radd_left_cancel_le\<close>,
17.50 + \<^rule_thm>\<open>not_true\<close>,
17.51 + \<^rule_thm>\<open>not_false\<close>,
17.52 + \<^rule_thm>\<open>and_true\<close>,
17.53 + \<^rule_thm>\<open>and_false\<close>,
17.54 + \<^rule_thm>\<open>or_true\<close>,
17.55 + \<^rule_thm>\<open>or_false\<close>,
17.56 + \<^rule_thm>\<open>and_commute\<close>,
17.57 + \<^rule_thm>\<open>or_commute\<close>,
17.58
17.59 - Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
17.60 + \<^rule_thm>\<open>real_diff_minus\<close>,
17.61
17.62 - Rule.Thm ("root_ge0",ThmC.numerals_to_Free @{thm root_ge0}),
17.63 - Rule.Thm ("root_add_ge0",ThmC.numerals_to_Free @{thm root_add_ge0}),
17.64 - Rule.Thm ("root_ge0_1",ThmC.numerals_to_Free @{thm root_ge0_1}),
17.65 - Rule.Thm ("root_ge0_2",ThmC.numerals_to_Free @{thm root_ge0_2}),
17.66 + \<^rule_thm>\<open>root_ge0\<close>,
17.67 + \<^rule_thm>\<open>root_add_ge0\<close>,
17.68 + \<^rule_thm>\<open>root_ge0_1\<close>,
17.69 + \<^rule_thm>\<open>root_ge0_2\<close>,
17.70
17.71 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
17.72 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root "#eval_contains_root"),
17.73 @@ -449,12 +449,12 @@
17.74 Rule_Def.Repeat{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
17.75 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
17.76 rules =
17.77 - [Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}),
17.78 - Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),
17.79 - Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
17.80 - Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),
17.81 - Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),
17.82 - Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc})],
17.83 + [\<^rule_thm>\<open>radd_commute\<close>,
17.84 + \<^rule_thm>\<open>radd_left_commute\<close>,
17.85 + \<^rule_thm>\<open>add.assoc\<close>,
17.86 + \<^rule_thm>\<open>rmult_commute\<close>,
17.87 + \<^rule_thm>\<open>rmult_left_commute\<close>,
17.88 + \<^rule_thm>\<open>rmult_assoc\<close>],
17.89 scr = Rule.Empty_Prog
17.90 };
17.91
17.92 @@ -462,7 +462,7 @@
17.93 val norm_equation =
17.94 Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
17.95 erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
17.96 - rules = [Rule.Thm ("rnorm_equation_add",ThmC.numerals_to_Free @{thm rnorm_equation_add})
17.97 + rules = [\<^rule_thm>\<open>rnorm_equation_add\<close>
17.98 ],
17.99 scr = Rule.Empty_Prog
17.100 };
17.101 @@ -475,22 +475,22 @@
17.102 erls = tval_rls, srls = Rule_Set.empty,
17.103 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
17.104 rules = [
17.105 - Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
17.106 - Rule.Thm ("radd_mult_distrib2",ThmC.numerals_to_Free @{thm radd_mult_distrib2}),
17.107 - Rule.Thm ("rdistr_right_assoc",ThmC.numerals_to_Free @{thm rdistr_right_assoc}),
17.108 - Rule.Thm ("rdistr_right_assoc_p",ThmC.numerals_to_Free @{thm rdistr_right_assoc_p}),
17.109 - Rule.Thm ("rdistr_div_right",ThmC.numerals_to_Free @{thm rdistr_div_right}),
17.110 - Rule.Thm ("rbinom_power_2",ThmC.numerals_to_Free @{thm rbinom_power_2}),
17.111 + \<^rule_thm>\<open>real_diff_minus\<close>,
17.112 + \<^rule_thm>\<open>radd_mult_distrib2\<close>,
17.113 + \<^rule_thm>\<open>rdistr_right_assoc\<close>,
17.114 + \<^rule_thm>\<open>rdistr_right_assoc_p\<close>,
17.115 + \<^rule_thm>\<open>rdistr_div_right\<close>,
17.116 + \<^rule_thm>\<open>rbinom_power_2\<close>,
17.117
17.118 - Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}),
17.119 - Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),
17.120 - Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
17.121 - Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),
17.122 - Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),
17.123 - Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc}),
17.124 + \<^rule_thm>\<open>radd_commute\<close>,
17.125 + \<^rule_thm>\<open>radd_left_commute\<close>,
17.126 + \<^rule_thm>\<open>add.assoc\<close>,
17.127 + \<^rule_thm>\<open>rmult_commute\<close>,
17.128 + \<^rule_thm>\<open>rmult_left_commute\<close>,
17.129 + \<^rule_thm>\<open>rmult_assoc\<close>,
17.130
17.131 - Rule.Thm ("radd_real_const_eq",ThmC.numerals_to_Free @{thm radd_real_const_eq}),
17.132 - Rule.Thm ("radd_real_const",ThmC.numerals_to_Free @{thm radd_real_const}),
17.133 + \<^rule_thm>\<open>radd_real_const_eq\<close>,
17.134 + \<^rule_thm>\<open>radd_real_const\<close>,
17.135 (* these 2 rules are invers to distr_div_right wrt. termination.
17.136 thus they MUST be done IMMEDIATELY before calc *)
17.137 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
17.138 @@ -498,27 +498,27 @@
17.139 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
17.140 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
17.141
17.142 - Rule.Thm ("rcollect_right",ThmC.numerals_to_Free @{thm rcollect_right}),
17.143 - Rule.Thm ("rcollect_one_left",ThmC.numerals_to_Free @{thm rcollect_one_left}),
17.144 - Rule.Thm ("rcollect_one_left_assoc",ThmC.numerals_to_Free @{thm rcollect_one_left_assoc}),
17.145 - Rule.Thm ("rcollect_one_left_assoc_p",ThmC.numerals_to_Free @{thm rcollect_one_left_assoc_p}),
17.146 + \<^rule_thm>\<open>rcollect_right\<close>,
17.147 + \<^rule_thm>\<open>rcollect_one_left\<close>,
17.148 + \<^rule_thm>\<open>rcollect_one_left_assoc\<close>,
17.149 + \<^rule_thm>\<open>rcollect_one_left_assoc_p\<close>,
17.150
17.151 - Rule.Thm ("rshift_nominator",ThmC.numerals_to_Free @{thm rshift_nominator}),
17.152 - Rule.Thm ("rcancel_den",ThmC.numerals_to_Free @{thm rcancel_den}),
17.153 - Rule.Thm ("rroot_square_inv",ThmC.numerals_to_Free @{thm rroot_square_inv}),
17.154 - Rule.Thm ("rroot_times_root",ThmC.numerals_to_Free @{thm rroot_times_root}),
17.155 - Rule.Thm ("rroot_times_root_assoc_p",ThmC.numerals_to_Free @{thm rroot_times_root_assoc_p}),
17.156 - Rule.Thm ("rsqare",ThmC.numerals_to_Free @{thm rsqare}),
17.157 - Rule.Thm ("power_1",ThmC.numerals_to_Free @{thm power_1}),
17.158 - Rule.Thm ("rtwo_of_the_same",ThmC.numerals_to_Free @{thm rtwo_of_the_same}),
17.159 - Rule.Thm ("rtwo_of_the_same_assoc_p",ThmC.numerals_to_Free @{thm rtwo_of_the_same_assoc_p}),
17.160 + \<^rule_thm>\<open>rshift_nominator\<close>,
17.161 + \<^rule_thm>\<open>rcancel_den\<close>,
17.162 + \<^rule_thm>\<open>rroot_square_inv\<close>,
17.163 + \<^rule_thm>\<open>rroot_times_root\<close>,
17.164 + \<^rule_thm>\<open>rroot_times_root_assoc_p\<close>,
17.165 + \<^rule_thm>\<open>rsqare\<close>,
17.166 + \<^rule_thm>\<open>power_1\<close>,
17.167 + \<^rule_thm>\<open>rtwo_of_the_same\<close>,
17.168 + \<^rule_thm>\<open>rtwo_of_the_same_assoc_p\<close>,
17.169
17.170 - Rule.Thm ("rmult_1",ThmC.numerals_to_Free @{thm rmult_1}),
17.171 - Rule.Thm ("rmult_1_right",ThmC.numerals_to_Free @{thm rmult_1_right}),
17.172 - Rule.Thm ("rmult_0",ThmC.numerals_to_Free @{thm rmult_0}),
17.173 - Rule.Thm ("rmult_0_right",ThmC.numerals_to_Free @{thm rmult_0_right}),
17.174 - Rule.Thm ("radd_0",ThmC.numerals_to_Free @{thm radd_0}),
17.175 - Rule.Thm ("radd_0_right",ThmC.numerals_to_Free @{thm radd_0_right})
17.176 + \<^rule_thm>\<open>rmult_1\<close>,
17.177 + \<^rule_thm>\<open>rmult_1_right\<close>,
17.178 + \<^rule_thm>\<open>rmult_0\<close>,
17.179 + \<^rule_thm>\<open>rmult_0_right\<close>,
17.180 + \<^rule_thm>\<open>radd_0\<close>,
17.181 + \<^rule_thm>\<open>radd_0_right\<close>
17.182 ],
17.183 scr = Rule.Empty_Prog
17.184 (*since 040209 filled by prep_rls': STest_simplify*)
17.185 @@ -529,12 +529,12 @@
17.186 val isolate_root =
17.187 Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
17.188 erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [],
17.189 - rules = [Rule.Thm ("rroot_to_lhs",ThmC.numerals_to_Free @{thm rroot_to_lhs}),
17.190 - Rule.Thm ("rroot_to_lhs_mult",ThmC.numerals_to_Free @{thm rroot_to_lhs_mult}),
17.191 - Rule.Thm ("rroot_to_lhs_add_mult",ThmC.numerals_to_Free @{thm rroot_to_lhs_add_mult}),
17.192 - Rule.Thm ("risolate_root_add",ThmC.numerals_to_Free @{thm risolate_root_add}),
17.193 - Rule.Thm ("risolate_root_mult",ThmC.numerals_to_Free @{thm risolate_root_mult}),
17.194 - Rule.Thm ("risolate_root_div",ThmC.numerals_to_Free @{thm risolate_root_div}) ],
17.195 + rules = [\<^rule_thm>\<open>rroot_to_lhs\<close>,
17.196 + \<^rule_thm>\<open>rroot_to_lhs_mult\<close>,
17.197 + \<^rule_thm>\<open>rroot_to_lhs_add_mult\<close>,
17.198 + \<^rule_thm>\<open>risolate_root_add\<close>,
17.199 + \<^rule_thm>\<open>risolate_root_mult\<close>,
17.200 + \<^rule_thm>\<open>risolate_root_div\<close> ],
17.201 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>))
17.202 "empty_script")
17.203 };
17.204 @@ -544,12 +544,12 @@
17.205 Rule_Def.Repeat{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
17.206 erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [],
17.207 rules =
17.208 - [Rule.Thm ("risolate_bdv_add",ThmC.numerals_to_Free @{thm risolate_bdv_add}),
17.209 - Rule.Thm ("risolate_bdv_mult_add",ThmC.numerals_to_Free @{thm risolate_bdv_mult_add}),
17.210 - Rule.Thm ("risolate_bdv_mult",ThmC.numerals_to_Free @{thm risolate_bdv_mult}),
17.211 - Rule.Thm ("mult_square",ThmC.numerals_to_Free @{thm mult_square}),
17.212 - Rule.Thm ("constant_square",ThmC.numerals_to_Free @{thm constant_square}),
17.213 - Rule.Thm ("constant_mult_square",ThmC.numerals_to_Free @{thm constant_mult_square})
17.214 + [\<^rule_thm>\<open>risolate_bdv_add\<close>,
17.215 + \<^rule_thm>\<open>risolate_bdv_mult_add\<close>,
17.216 + \<^rule_thm>\<open>risolate_bdv_mult\<close>,
17.217 + \<^rule_thm>\<open>mult_square\<close>,
17.218 + \<^rule_thm>\<open>constant_square\<close>,
17.219 + \<^rule_thm>\<open>constant_mult_square\<close>
17.220 ],
17.221 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>))
17.222 "empty_script")
17.223 @@ -605,54 +605,54 @@
17.224 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
17.225 ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))
17.226 ], errpatts = [],
17.227 - rules = [Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
17.228 + rules = [\<^rule_thm>\<open>real_diff_minus\<close>,
17.229 (*"a - b = a + (-1) * b"*)
17.230 - Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
17.231 + \<^rule_thm>\<open>distrib_right\<close>,
17.232 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
17.233 - Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
17.234 + \<^rule_thm>\<open>distrib_left\<close>,
17.235 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
17.236 - Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),
17.237 + \<^rule_thm>\<open>left_diff_distrib\<close>,
17.238 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
17.239 - Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),
17.240 + \<^rule_thm>\<open>right_diff_distrib\<close>,
17.241 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
17.242 - Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
17.243 + \<^rule_thm>\<open>mult_1_left\<close>,
17.244 (*"1 * z = z"*)
17.245 - Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
17.246 + \<^rule_thm>\<open>mult_zero_left\<close>,
17.247 (*"0 * z = 0"*)
17.248 - Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
17.249 + \<^rule_thm>\<open>add_0_left\<close>,
17.250 (*"0 + z = z"*)
17.251
17.252 (*AC-rewriting*)
17.253 - Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
17.254 + \<^rule_thm>\<open>mult.commute\<close>,
17.255 (* z * w = w * z *)
17.256 - Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
17.257 + \<^rule_thm>\<open>real_mult_left_commute\<close>,
17.258 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
17.259 - Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
17.260 + \<^rule_thm>\<open>mult.assoc\<close>,
17.261 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
17.262 - Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
17.263 + \<^rule_thm>\<open>add.commute\<close>,
17.264 (*z + w = w + z*)
17.265 - Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
17.266 + \<^rule_thm>\<open>add.left_commute\<close>,
17.267 (*x + (y + z) = y + (x + z)*)
17.268 - Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
17.269 + \<^rule_thm>\<open>add.assoc\<close>,
17.270 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
17.271
17.272 \<^rule_thm_sym>\<open>realpow_twoI\<close>,
17.273 (*"r1 * r1 = r1 \<up> 2"*)
17.274 - Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
17.275 + \<^rule_thm>\<open>realpow_plus_1\<close>,
17.276 (*"r * r \<up> n = r \<up> (n + 1)"*)
17.277 \<^rule_thm_sym>\<open>real_mult_2\<close>,
17.278 (*"z1 + z1 = 2 * z1"*)
17.279 - Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
17.280 + \<^rule_thm>\<open>real_mult_2_assoc\<close>,
17.281 (*"z1 + (z1 + k) = 2 * z1 + k"*)
17.282
17.283 - Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
17.284 + \<^rule_thm>\<open>real_num_collect\<close>,
17.285 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
17.286 - Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
17.287 + \<^rule_thm>\<open>real_num_collect_assoc\<close>,
17.288 (*"[| l is_const; m is_const |] ==>
17.289 l * n + (m * n + k) = (l + m) * n + k"*)
17.290 - Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
17.291 + \<^rule_thm>\<open>real_one_collect\<close>,
17.292 (*"m is_const ==> n + m * n = (1 + m) * n"*)
17.293 - Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
17.294 + \<^rule_thm>\<open>real_one_collect_assoc\<close>,
17.295 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
17.296
17.297 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
17.298 @@ -672,81 +672,81 @@
17.299 ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))
17.300 ], errpatts = [],
17.301 rules =
17.302 - [Rule.Thm ("real_plus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
17.303 + [\<^rule_thm>\<open>real_plus_binom_pow2\<close>,
17.304 (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
17.305 - Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
17.306 + \<^rule_thm>\<open>real_plus_binom_times\<close>,
17.307 (*"(a + b)*(a + b) = ...*)
17.308 - Rule.Thm ("real_minus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
17.309 + \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
17.310 (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
17.311 - Rule.Thm ("real_minus_binom_times",ThmC.numerals_to_Free @{thm real_minus_binom_times}),
17.312 + \<^rule_thm>\<open>real_minus_binom_times\<close>,
17.313 (*"(a - b)*(a - b) = ...*)
17.314 - Rule.Thm ("real_plus_minus_binom1",ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),
17.315 + \<^rule_thm>\<open>real_plus_minus_binom1\<close>,
17.316 (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
17.317 - Rule.Thm ("real_plus_minus_binom2",ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),
17.318 + \<^rule_thm>\<open>real_plus_minus_binom2\<close>,
17.319 (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
17.320 (*RL 020915*)
17.321 - Rule.Thm ("real_pp_binom_times",ThmC.numerals_to_Free @{thm real_pp_binom_times}),
17.322 + \<^rule_thm>\<open>real_pp_binom_times\<close>,
17.323 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
17.324 - Rule.Thm ("real_pm_binom_times",ThmC.numerals_to_Free @{thm real_pm_binom_times}),
17.325 + \<^rule_thm>\<open>real_pm_binom_times\<close>,
17.326 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
17.327 - Rule.Thm ("real_mp_binom_times",ThmC.numerals_to_Free @{thm real_mp_binom_times}),
17.328 + \<^rule_thm>\<open>real_mp_binom_times\<close>,
17.329 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
17.330 - Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}),
17.331 + \<^rule_thm>\<open>real_mm_binom_times\<close>,
17.332 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
17.333 - Rule.Thm ("realpow_multI",ThmC.numerals_to_Free @{thm realpow_multI}),
17.334 + \<^rule_thm>\<open>realpow_multI\<close>,
17.335 (*(a*b) \<up> n = a \<up> n * b \<up> n*)
17.336 - Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),
17.337 + \<^rule_thm>\<open>real_plus_binom_pow3\<close>,
17.338 (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
17.339 - Rule.Thm ("real_minus_binom_pow3",ThmC.numerals_to_Free @{thm real_minus_binom_pow3}),
17.340 + \<^rule_thm>\<open>real_minus_binom_pow3\<close>,
17.341 (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
17.342
17.343
17.344 - (* Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
17.345 + (* \<^rule_thm>\<open>distrib_right\<close>,
17.346 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
17.347 - Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
17.348 + \<^rule_thm>\<open>distrib_left\<close>,
17.349 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
17.350 - Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),
17.351 + \<^rule_thm>\<open>left_diff_distrib\<close>,
17.352 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
17.353 - Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),
17.354 + \<^rule_thm>\<open>right_diff_distrib\<close>,
17.355 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
17.356 *)
17.357
17.358 - Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
17.359 + \<^rule_thm>\<open>mult_1_left\<close>,
17.360 (*"1 * z = z"*)
17.361 - Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
17.362 + \<^rule_thm>\<open>mult_zero_left\<close>,
17.363 (*"0 * z = 0"*)
17.364 - Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
17.365 + \<^rule_thm>\<open>add_0_left\<close>,
17.366 (*"0 + z = z"*)
17.367
17.368 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
17.369 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
17.370 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
17.371 (*
17.372 - Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
17.373 + \<^rule_thm>\<open>mult.commute\<close>,
17.374 (*AC-rewriting*)
17.375 - Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
17.376 - Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
17.377 - Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
17.378 - Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
17.379 - Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
17.380 + \<^rule_thm>\<open>real_mult_left_commute\<close>,
17.381 + \<^rule_thm>\<open>mult.assoc\<close>,
17.382 + \<^rule_thm>\<open>add.commute\<close>,
17.383 + \<^rule_thm>\<open>add.left_commute\<close>,
17.384 + \<^rule_thm>\<open>add.assoc\<close>,
17.385 *)
17.386
17.387 \<^rule_thm_sym>\<open>realpow_twoI\<close>,
17.388 (*"r1 * r1 = r1 \<up> 2"*)
17.389 - Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
17.390 + \<^rule_thm>\<open>realpow_plus_1\<close>,
17.391 (*"r * r \<up> n = r \<up> (n + 1)"*)
17.392 (*\<^rule_thm_sym>\<open>real_mult_2\<close>,
17.393 (*"z1 + z1 = 2 * z1"*)*)
17.394 - Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
17.395 + \<^rule_thm>\<open>real_mult_2_assoc\<close>,
17.396 (*"z1 + (z1 + k) = 2 * z1 + k"*)
17.397
17.398 - Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
17.399 + \<^rule_thm>\<open>real_num_collect\<close>,
17.400 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
17.401 - Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
17.402 + \<^rule_thm>\<open>real_num_collect_assoc\<close>,
17.403 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
17.404 - Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
17.405 + \<^rule_thm>\<open>real_one_collect\<close>,
17.406 (*"m is_const ==> n + m * n = (1 + m) * n"*)
17.407 - Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
17.408 + \<^rule_thm>\<open>real_one_collect_assoc\<close>,
17.409 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
17.410
17.411 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
18.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Jun 12 14:29:10 2021 +0200
18.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Jun 12 18:06:27 2021 +0200
18.3 @@ -74,9 +74,9 @@
18.4
18.5 ML \<open>
18.6 val inverse_Z = Rule_Set.append_rules "inverse_Z" Atools_erls
18.7 - [ Rule.Thm ("rule3",ThmC.numerals_to_Free @{thm rule3}),
18.8 - Rule.Thm ("rule4",ThmC.numerals_to_Free @{thm rule4}),
18.9 - Rule.Thm ("rule1",ThmC.numerals_to_Free @{thm rule1})
18.10 + [ \<^rule_thm>\<open>rule3\<close>,
18.11 + \<^rule_thm>\<open>rule4\<close>,
18.12 + \<^rule_thm>\<open>rule1\<close>
18.13 ];
18.14
18.15 \<close> ML \<open>