1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Sat Jun 12 14:27:03 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Sat Jun 12 14:29:10 2021 +0200
1.3 @@ -64,25 +64,25 @@
1.4 \<close> ML \<open>
1.5 val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty
1.6 [ \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.7 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.8 + \<^rule_thm>\<open>not_true\<close>,
1.9 (*"(~ True) = False"*)
1.10 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
1.11 + \<^rule_thm>\<open>not_false\<close>,
1.12 (*"(~ False) = True"*)
1.13 - Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
1.14 + \<^rule_thm>\<open>and_true\<close>,
1.15 (*"(?a & True) = ?a"*)
1.16 - Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
1.17 + \<^rule_thm>\<open>and_false\<close>,
1.18 (*"(?a & False) = False"*)
1.19 - Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
1.20 + \<^rule_thm>\<open>or_true\<close>,
1.21 (*"(?a | True) = True"*)
1.22 - Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
1.23 + \<^rule_thm>\<open>or_false\<close>,
1.24 (*"(?a | False) = ?a"*)
1.25
1.26 - Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
1.27 - Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),
1.28 - Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3}),
1.29 - Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),
1.30 - Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
1.31 - Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
1.32 + \<^rule_thm>\<open>rat_leq1\<close>,
1.33 + \<^rule_thm>\<open>rat_leq2\<close>,
1.34 + \<^rule_thm>\<open>rat_leq3\<close>,
1.35 + \<^rule_thm>\<open>refl\<close>,
1.36 + \<^rule_thm>\<open>order_refl\<close>,
1.37 + \<^rule_thm>\<open>radd_left_cancel_le\<close>,
1.38
1.39 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.40 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.41 @@ -96,19 +96,19 @@
1.42 ML \<open>
1.43 val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty
1.44 [ \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
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 ("and_true", ThmC.numerals_to_Free @{thm and_true}),
1.48 - Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
1.49 - Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
1.50 - Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
1.51 -
1.52 - Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
1.53 - Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),
1.54 - Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3}),
1.55 - Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),
1.56 - Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
1.57 - Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
1.58 + \<^rule_thm>\<open>not_true\<close>,
1.59 + \<^rule_thm>\<open>not_false\<close>,
1.60 + \<^rule_thm>\<open>and_true\<close>,
1.61 + \<^rule_thm>\<open>and_false\<close>,
1.62 + \<^rule_thm>\<open>or_true\<close>,
1.63 + \<^rule_thm>\<open>or_false\<close>,
1.64 +
1.65 + \<^rule_thm>\<open>rat_leq1\<close>,
1.66 + \<^rule_thm>\<open>rat_leq2\<close>,
1.67 + \<^rule_thm>\<open>rat_leq3\<close>,
1.68 + \<^rule_thm>\<open>refl\<close>,
1.69 + \<^rule_thm>\<open>order_refl\<close>,
1.70 + \<^rule_thm>\<open>radd_left_cancel_le\<close>,
1.71
1.72 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.73 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.74 @@ -132,8 +132,8 @@
1.75
1.76 \<^rule_eval>\<open>Prog_Expr.Vars\<close> (Prog_Expr.eval_var "#Vars_"),
1.77
1.78 - Rule.Thm ("if_True",ThmC.numerals_to_Free @{thm if_True}),
1.79 - Rule.Thm ("if_False",ThmC.numerals_to_Free @{thm if_False})];
1.80 + \<^rule_thm>\<open>if_True\<close>,
1.81 + \<^rule_thm>\<open>if_False\<close>];
1.82
1.83 val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge "list_erls"
1.84 (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
2.1 --- a/src/Tools/isac/Knowledge/Diff.thy Sat Jun 12 14:27:03 2021 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Sat Jun 12 14:29:10 2021 +0200
2.3 @@ -153,9 +153,8 @@
2.4 rules = [Rule.Thm ("frac_sym_conv", ThmC.numerals_to_Free @{thm frac_sym_conv}),
2.5 Rule.Thm ("sqrt_sym_conv", ThmC.numerals_to_Free @{thm sqrt_sym_conv}),
2.6 Rule.Thm ("root_sym_conv", ThmC.numerals_to_Free @{thm root_sym_conv}),
2.7 - Rule.Thm ("sym_real_mult_minus1",
2.8 - ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})),
2.9 - (*- ?z = "-1 * ?z"*)
2.10 + \<^rule_thm_sym>\<open>real_mult_minus1\<close>,
2.11 + (*- ?z = "-1 * ?z"*)
2.12 Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
2.13 (*a / b * (c / d) = a * c / (b * d)*)
2.14 Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
3.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 12 14:27:03 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 12 14:29:10 2021 +0200
3.3 @@ -252,8 +252,7 @@
3.4 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
3.5 Rule.Rls_ norm_Rational_noadd_fractions(**2**),
3.6 Rule.Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
3.7 - Rule.Thm ("sym_mult.assoc",
3.8 - ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym}))
3.9 + \<^rule_thm_sym>\<open>mult.assoc\<close>
3.10 (*Rule.Rls_ discard_parentheses *3**),
3.11 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
3.12 Rule.Rls_ separate_bdv2,
3.13 @@ -281,8 +280,7 @@
3.14 (*
3.15 val simplify_System =
3.16 Rule_Set.append_rules "simplify_System" simplify_System_parenthesized
3.17 - [Rule.Thm ("sym_add.assoc",
3.18 - ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))];
3.19 + [\<^rule_thm_sym>\<open>add.assoc\<close>];
3.20 *)
3.21 \<close>
3.22 ML \<open>
4.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sat Jun 12 14:27:03 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sat Jun 12 14:29:10 2021 +0200
4.3 @@ -683,7 +683,7 @@
4.4 rules =
4.5 [Rule.Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}),
4.6 (*"a - b = a + -1 * b"*)
4.7 - Rule.Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym}))
4.8 + \<^rule_thm_sym>\<open>real_mult_minus1\<close>
4.9 (*- ?z = "-1 * ?z"*)],
4.10 scr = Rule.Empty_Prog};
4.11
4.12 @@ -766,8 +766,7 @@
4.13 calc = [], errpatts = [],
4.14 rules = [(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
4.15 a*(a*a) --> a*a \<up> 2 und nicht a*(a*a) --> a \<up> 2*a *)
4.16 - Rule.Thm ("sym_realpow_twoI",
4.17 - ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
4.18 + \<^rule_thm_sym>\<open>realpow_twoI\<close>,
4.19 (*"r * r = r \<up> 2"*)
4.20 Rule.Thm ("realpow_twoI_assoc_l",ThmC.numerals_to_Free @{thm realpow_twoI_assoc_l}),
4.21 (*"r * (r * s) = r \<up> 2 * s"*)
4.22 @@ -782,8 +781,7 @@
4.23 ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l2}),
4.24 (*"r \<up> m * (r * s) = r \<up> (1 + m) * s"*)
4.25
4.26 - Rule.Thm ("sym_realpow_addI",
4.27 - ThmC.numerals_to_Free (@{thm realpow_addI} RS @{thm sym})),
4.28 + \<^rule_thm_sym>\<open>realpow_addI\<close>,
4.29 (*"r \<up> n * r \<up> m = r \<up> (n + m)"*)
4.30 Rule.Thm ("realpow_addI_assoc_l",ThmC.numerals_to_Free @{thm realpow_addI_assoc_l}),
4.31 (*"r \<up> n * (r \<up> m * s) = r \<up> (n + m) * s"*)
4.32 @@ -847,7 +845,7 @@
4.33 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
4.34 Rule.Thm ("real_mult_2_assoc_r",ThmC.numerals_to_Free @{thm real_mult_2_assoc_r}),
4.35 (*"(k + z1) + z1 = k + 2 * z1"*)
4.36 - Rule.Thm ("sym_real_mult_2",ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym}))
4.37 + \<^rule_thm_sym>\<open>real_mult_2\<close>
4.38 (*"z1 + z1 = 2 * z1"*)
4.39 ], scr = Rule.Empty_Prog};
4.40
4.41 @@ -874,11 +872,9 @@
4.42
4.43 val discard_parentheses1 =
4.44 Rule_Set.append_rules "discard_parentheses1" Rule_Set.empty
4.45 - [Rule.Thm ("sym_mult.assoc",
4.46 - ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym}))
4.47 + [\<^rule_thm_sym>\<open>mult.assoc\<close>
4.48 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
4.49 - (*Rule.Thm ("sym_add.assoc",
4.50 - ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))*)
4.51 + (*\<^rule_thm_sym>\<open>add.assoc\<close>*)
4.52 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
4.53 ];
4.54
4.55 @@ -910,8 +906,7 @@
4.56 (*"- (- ?z) = ?z"*)
4.57 Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
4.58 (*"a - b = a + -1 * b"*)
4.59 - Rule.Thm ("sym_real_mult_minus1",
4.60 - ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym}))
4.61 + \<^rule_thm_sym>\<open>real_mult_minus1\<close>
4.62 (*- ?z = "-1 * ?z"*)
4.63
4.64 (*Rule.Thm ("real_minus_add_distrib",
4.65 @@ -929,15 +924,13 @@
4.66 rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
4.67 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
4.68
4.69 - Rule.Thm ("sym_realpow_twoI",
4.70 - ThmC.numerals_to_Free( @{thm realpow_twoI} RS @{thm sym})),
4.71 + \<^rule_thm_sym>\<open>realpow_twoI\<close>,
4.72 (*"r1 * r1 = r1 \<up> 2"*)
4.73 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
4.74 (*"r * r \<up> n = r \<up> (n + 1)"*)
4.75 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
4.76 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
4.77 - Rule.Thm ("sym_realpow_addI",
4.78 - ThmC.numerals_to_Free (@{thm realpow_addI} RS @{thm sym})),
4.79 + \<^rule_thm_sym>\<open>realpow_addI\<close>,
4.80 (*"r \<up> n * r \<up> m = r \<up> (n + m)"*)
4.81 Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
4.82 (*"r \<up> 1 = r"*)
4.83 @@ -987,8 +980,7 @@
4.84 (*"0 + z = z"*)
4.85 Rule.Thm ("right_minus",ThmC.numerals_to_Free @{thm right_minus}),
4.86 (*"?z + - ?z = 0"*)
4.87 - Rule.Thm ("sym_real_mult_2",
4.88 - ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
4.89 + \<^rule_thm_sym>\<open>real_mult_2\<close>,
4.90 (*"z1 + z1 = 2 * z1"*)
4.91 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc})
4.92 (*"z1 + (z1 + k) = 2 * z1 + k"*)
4.93 @@ -996,10 +988,7 @@
4.94
4.95 val discard_parentheses =
4.96 Rule_Set.append_rules "discard_parentheses" Rule_Set.empty
4.97 - [Rule.Thm ("sym_mult.assoc",
4.98 - ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym})),
4.99 - Rule.Thm ("sym_add.assoc",
4.100 - ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))];
4.101 + [\<^rule_thm_sym>\<open>mult.assoc\<close>, \<^rule_thm_sym>\<open>add.assoc\<close>];
4.102 \<close>
4.103
4.104 subsubsection \<open>hard-coded AC rewriting\<close>
4.105 @@ -1223,11 +1212,9 @@
4.106 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
4.107 \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
4.108
4.109 - Rule.Thm ("sym_realpow_twoI",
4.110 - ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
4.111 + \<^rule_thm_sym>\<open>realpow_twoI\<close>,
4.112 (*"r1 * r1 = r1 \<up> 2"*)
4.113 - Rule.Thm ("sym_real_mult_2",
4.114 - ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
4.115 + \<^rule_thm_sym>\<open>real_mult_2\<close>,
4.116 (*"z1 + z1 = 2 * z1"*)
4.117 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
4.118 (*"z1 + (z1 + k) = 2 * z1 + k"*)
4.119 @@ -1365,13 +1352,11 @@
4.120 Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
4.121 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
4.122 *)
4.123 - Rule.Thm ("sym_realpow_twoI",
4.124 - ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
4.125 + \<^rule_thm_sym>\<open>realpow_twoI\<close>,
4.126 (*"r1 * r1 = r1 \<up> 2"*)
4.127 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
4.128 (*"r * r \<up> n = r \<up> (n + 1)"*)
4.129 - (*Rule.Thm ("sym_real_mult_2",
4.130 - ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
4.131 + (*\<^rule_thm_sym>\<open>real_mult_2\<close>,
4.132 (*"z1 + z1 = 2 * z1"*)*)
4.133 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
4.134 (*"z1 + (z1 + k) = 2 * z1 + k"*)
5.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Sat Jun 12 14:27:03 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Sat Jun 12 14:29:10 2021 +0200
5.3 @@ -270,7 +270,7 @@
5.4 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
5.5 Rule.Thm ("real_mult_2_assoc_r",ThmC.numerals_to_Free @{thm real_mult_2_assoc_r}),
5.6 (*"(k + z1) + z1 = k + 2 * z1"*)
5.7 - Rule.Thm ("sym_real_mult_2",ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
5.8 + \<^rule_thm_sym>\<open>real_mult_2\<close>,
5.9 (*"z1 + z1 = 2 * z1"*)
5.10
5.11 Rule.Thm ("addiere_vor_minus",ThmC.numerals_to_Free @{thm addiere_vor_minus}),
5.12 @@ -318,8 +318,7 @@
5.13 val klammern_aufloesen =
5.14 Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [],
5.15 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
5.16 - rules = [Rule.Thm ("sym_add.assoc",
5.17 - ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
5.18 + rules = [\<^rule_thm_sym>\<open>add.assoc\<close>,
5.19 (*"a + (b + c) = (a + b) + c"*)
5.20 Rule.Thm ("klammer_plus_minus",ThmC.numerals_to_Free @{thm klammer_plus_minus}),
5.21 (*"a + (b - c) = (a + b) - c"*)
6.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sat Jun 12 14:27:03 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sat Jun 12 14:29:10 2021 +0200
6.3 @@ -691,8 +691,7 @@
6.4 (*Rule.Thm ("right_minus",ThmC.numerals_to_Free @{thm right_minus}),
6.5 "?z + - ?z = 0"*)
6.6
6.7 - Rule.Thm ("sym_real_mult_2",
6.8 - ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
6.9 + \<^rule_thm_sym>\<open>real_mult_2\<close>,
6.10 (*"z1 + z1 = 2 * z1"*)
6.11 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
6.12 (*"z1 + (z1 + k) = 2 * z1 + k"*)
7.1 --- a/src/Tools/isac/Knowledge/Root.thy Sat Jun 12 14:27:03 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Root.thy Sat Jun 12 14:29:10 2021 +0200
7.3 @@ -224,13 +224,11 @@
7.4 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
7.5 (**)
7.6
7.7 - Rule.Thm ("sym_realpow_twoI",
7.8 - ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
7.9 + \<^rule_thm_sym>\<open>realpow_twoI\<close>,
7.10 (*"r1 * r1 = r1 \<up> 2"*)
7.11 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
7.12 (*"r * r \<up> n = r \<up> (n + 1)"*)
7.13 - Rule.Thm ("sym_real_mult_2",
7.14 - ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
7.15 + \<^rule_thm_sym>\<open>real_mult_2\<close>,
7.16 (*"z1 + z1 = 2 * z1"*)
7.17 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
7.18 (*"z1 + (z1 + k) = 2 * z1 + k"*)
7.19 @@ -298,8 +296,7 @@
7.20 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
7.21 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
7.22
7.23 - Rule.Thm ("sym_realpow_twoI",
7.24 - ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
7.25 + \<^rule_thm_sym>\<open>realpow_twoI\<close>,
7.26 (*"r1 * r1 = r1 \<up> 2"*)
7.27 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
7.28 (*"r * r \<up> n = r \<up> (n + 1)"*)
8.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Sat Jun 12 14:27:03 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Sat Jun 12 14:29:10 2021 +0200
8.3 @@ -18,7 +18,7 @@
8.4 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
8.5 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
8.6 (* 1 * z = z *)
8.7 - Rule.Thm ("sym_real_mult_minus1",ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})),
8.8 + \<^rule_thm_sym>\<open>real_mult_minus1\<close>,
8.9 (* "- z1 = -1 * z1" *)
8.10 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_")
8.11 ];
9.1 --- a/src/Tools/isac/Knowledge/Test.thy Sat Jun 12 14:27:03 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sat Jun 12 14:29:10 2021 +0200
9.3 @@ -441,9 +441,7 @@
9.4 Rule_Def.Repeat{id = "rearrange_assoc", preconds = [],
9.5 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
9.6 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
9.7 - rules =
9.8 - [Rule.Thm ("sym_add.assoc",ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
9.9 - Rule.Thm ("sym_rmult_assoc",ThmC.numerals_to_Free (@{thm rmult_assoc} RS @{thm sym}))],
9.10 + rules = [\<^rule_thm_sym>\<open>add.assoc\<close>, \<^rule_thm_sym>\<open>rmult_assoc\<close>],
9.11 scr = Rule.Empty_Prog
9.12 };
9.13
9.14 @@ -638,13 +636,11 @@
9.15 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
9.16 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
9.17
9.18 - Rule.Thm ("sym_realpow_twoI",
9.19 - ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
9.20 + \<^rule_thm_sym>\<open>realpow_twoI\<close>,
9.21 (*"r1 * r1 = r1 \<up> 2"*)
9.22 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
9.23 (*"r * r \<up> n = r \<up> (n + 1)"*)
9.24 - Rule.Thm ("sym_real_mult_2",
9.25 - ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
9.26 + \<^rule_thm_sym>\<open>real_mult_2\<close>,
9.27 (*"z1 + z1 = 2 * z1"*)
9.28 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
9.29 (*"z1 + (z1 + k) = 2 * z1 + k"*)
9.30 @@ -735,13 +731,11 @@
9.31 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
9.32 *)
9.33
9.34 - Rule.Thm ("sym_realpow_twoI",
9.35 - ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
9.36 + \<^rule_thm_sym>\<open>realpow_twoI\<close>,
9.37 (*"r1 * r1 = r1 \<up> 2"*)
9.38 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
9.39 (*"r * r \<up> n = r \<up> (n + 1)"*)
9.40 - (*Rule.Thm ("sym_real_mult_2",
9.41 - ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
9.42 + (*\<^rule_thm_sym>\<open>real_mult_2\<close>,
9.43 (*"z1 + z1 = 2 * z1"*)*)
9.44 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
9.45 (*"z1 + (z1 + k) = 2 * z1 + k"*)
10.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Sat Jun 12 14:27:03 2021 +0200
10.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Sat Jun 12 14:29:10 2021 +0200
10.3 @@ -27,6 +27,8 @@
10.4
10.5 val revert_sym_rule: theory -> Rule.rule -> Rule.rule
10.6
10.7 + val make_rule: Proof.context -> bool -> string * Position.T -> Rule_Def.rule
10.8 +
10.9 \<^isac_test>\<open>
10.10 val dest_eq_concl: thm -> term * term
10.11 val string_of_thm_in_thy: theory -> thm -> string
10.12 @@ -160,4 +162,34 @@
10.13 | revert_sym_rule _ rule = raise ERROR ("revert_sym_rule: NOT for " ^ Rule.to_string rule)
10.14
10.15
10.16 +(* ML antiquotations *)
10.17 +
10.18 +val sym_prefix = "sym_";
10.19 +
10.20 +fun make_rule ctxt symmetric (xname, pos) =
10.21 + let
10.22 + val _ =
10.23 + if String.isPrefix sym_prefix xname
10.24 + then error ("Bad theorem name with sym-prefix " ^ quote xname ^ Position.here pos) else ();
10.25 +
10.26 + val context = Context.Proof ctxt;
10.27 + val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
10.28 + val {name, dynamic, thms, ...} = Facts.retrieve context facts (xname, pos);
10.29 + val thm =
10.30 + if dynamic then error ("Bad dynamic fact " ^ quote name ^ Position.here pos)
10.31 + else Facts.the_single (name, pos) thms;
10.32 + val (xname', thm') = if symmetric then (sym_prefix ^ xname, thm RS sym) else (xname, thm);
10.33 + in Rule.Thm (xname', numerals_to_Free thm') end;
10.34 +
10.35 +fun antiquotation binding sym =
10.36 + ML_Antiquotation.value_embedded binding
10.37 + (Scan.lift Args.embedded_position >> (fn name =>
10.38 + "ThmC.make_rule ML_context " ^ Bool.toString sym ^
10.39 + ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position name));
10.40 +
10.41 +val _ =
10.42 + Theory.setup
10.43 + (antiquotation \<^binding>\<open>rule_thm\<close> false #>
10.44 + antiquotation \<^binding>\<open>rule_thm_sym\<close> true);
10.45 +
10.46 (**)end(**)
11.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sat Jun 12 14:27:03 2021 +0200
11.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sat Jun 12 14:29:10 2021 +0200
11.3 @@ -40,10 +40,10 @@
11.4 val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
11.5 |> map (Thy_Hierarchy.thms_of_rls o #2 o #2)
11.6 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
11.7 - Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
11.8 + \<^rule_thm_sym>\<open>real_mult_minus1\<close>, "- ?z1 = -1 * ?z1")]]*)
11.9 |> flat
11.10 (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
11.11 - Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)
11.12 + \<^rule_thm_sym>\<open>real_mult_minus1\<close>, "- ?z1 = -1 * ?z1")]*)
11.13 |> map (ThmC.revert_sym_rule thy)
11.14 (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
11.15 Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)
12.1 --- a/test/Tools/isac/MathEngBasic/thmC.sml Sat Jun 12 14:27:03 2021 +0200
12.2 +++ b/test/Tools/isac/MathEngBasic/thmC.sml Sat Jun 12 14:29:10 2021 +0200
12.3 @@ -46,8 +46,7 @@
12.4 "----------- fun revert_sym_rule ---------------------------------------------------------------";
12.5 "----------- fun revert_sym_rule ---------------------------------------------------------------";
12.6 "~~~~~ fun revert_sym_rule , args:"; val (thy, (Rule.Thm (id, thm))) =
12.7 - (@{theory Isac_Knowledge},
12.8 - Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})));
12.9 + (@{theory Isac_Knowledge}, \<^rule_thm_sym>\<open>real_mult_minus1\<close>);
12.10
12.11 if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = -1 * ?z1" then ()
12.12 else error "input to revert_sym_rule CHANGED";
12.13 @@ -58,8 +57,7 @@
12.14 val id'' = Thm.get_name_hint thm'
12.15
12.16 val thy = @{theory Isac_Knowledge}
12.17 -val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
12.18 - (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
12.19 +val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy (\<^rule_thm_sym>\<open>real_mult_minus1\<close>)
12.20 ;
12.21 if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
12.22 then () else error "fun revert_sym_rule changed 1";