1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 15 10:07:43 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 15 11:11:54 2020 +0200
1.3 @@ -174,17 +174,17 @@
1.4 rew_ord = ("ord_simplify_System",
1.5 ord_simplify_System false @{theory "Integrate"}),
1.6 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
1.7 - rules = [Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult.commute}),
1.8 + rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
1.9 (* z * w = w * z *)
1.10 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
1.11 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.12 - Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
1.13 + Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
1.14 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.15 - Rule.Thm ("add_commute",ThmC.numerals_to_Free @{thm add.commute}),
1.16 + Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
1.17 (*z + w = w + z*)
1.18 - Rule.Thm ("add_left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
1.19 + Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
1.20 (*x + (y + z) = y + (x + z)*)
1.21 - Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc})
1.22 + Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc})
1.23 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.24 ],
1.25 scr = Rule.EmptyScr};
1.26 @@ -253,7 +253,7 @@
1.27 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.28 Rule.Rls_ norm_Rational_noadd_fractions(**2**),
1.29 Rule.Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
1.30 - Rule.Thm ("sym_mult_assoc",
1.31 + Rule.Thm ("sym_mult.assoc",
1.32 ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym}))
1.33 (*Rule.Rls_ discard_parentheses *3**),
1.34 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.35 @@ -282,7 +282,7 @@
1.36 (*
1.37 val simplify_System =
1.38 Rule_Set.append_rules "simplify_System" simplify_System_parenthesized
1.39 - [Rule.Thm ("sym_add_assoc",
1.40 + [Rule.Thm ("sym_add.assoc",
1.41 ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))];
1.42 *)
1.43 \<close>
2.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Apr 15 10:07:43 2020 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Apr 15 11:11:54 2020 +0200
2.3 @@ -874,11 +874,11 @@
2.4
2.5 val discard_parentheses1 =
2.6 Rule_Set.append_rules "discard_parentheses1" Rule_Set.empty
2.7 - [Rule.Thm ("sym_mult_assoc",
2.8 + [Rule.Thm ("sym_mult.assoc",
2.9 ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym}))
2.10 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
2.11 - (*Rule.Thm ("sym_add_assoc",
2.12 - ThmC.numerals_to_Free (@{thm add_assoc} RS @{thm sym}))*)
2.13 + (*Rule.Thm ("sym_add.assoc",
2.14 + ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))*)
2.15 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
2.16 ];
2.17
2.18 @@ -996,9 +996,9 @@
2.19
2.20 val discard_parentheses =
2.21 Rule_Set.append_rules "discard_parentheses" Rule_Set.empty
2.22 - [Rule.Thm ("sym_mult_assoc",
2.23 + [Rule.Thm ("sym_mult.assoc",
2.24 ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym})),
2.25 - Rule.Thm ("sym_add_assoc",
2.26 + Rule.Thm ("sym_add.assoc",
2.27 ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))];
2.28 \<close>
2.29
2.30 @@ -1011,17 +1011,17 @@
2.31 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
2.32 erls = Rule_Set.empty,srls = Rule_Set.Empty,
2.33 calc = [], errpatts = [],
2.34 - rules = [Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult.commute}),
2.35 + rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
2.36 (* z * w = w * z *)
2.37 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
2.38 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
2.39 - Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
2.40 + Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
2.41 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
2.42 - Rule.Thm ("add_commute",ThmC.numerals_to_Free @{thm add.commute}),
2.43 + Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
2.44 (*z + w = w + z*)
2.45 - Rule.Thm ("add_left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
2.46 + Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
2.47 (*x + (y + z) = y + (x + z)*)
2.48 - Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc})
2.49 + Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc})
2.50 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
2.51 ], scr = Rule.EmptyScr};
2.52 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
2.53 @@ -1031,11 +1031,11 @@
2.54 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
2.55 erls = Rule_Set.empty,srls = Rule_Set.Empty,
2.56 calc = [], errpatts = [],
2.57 - rules = [Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult.commute}),
2.58 + rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
2.59 (* z * w = w * z *)
2.60 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
2.61 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
2.62 - Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc})
2.63 + Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc})
2.64 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
2.65 ], scr = Rule.EmptyScr};
2.66 \<close>
2.67 @@ -1215,7 +1215,7 @@
2.68 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
2.69 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
2.70
2.71 - Rule.Thm ("mult_assoc", ThmC.numerals_to_Free @{thm mult.assoc}),
2.72 + Rule.Thm ("mult.assoc", ThmC.numerals_to_Free @{thm mult.assoc}),
2.73 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
2.74 Rule.Rls_ order_mult_rls_,
2.75 (*Rule.Rls_ order_add_rls_,*)
2.76 @@ -1357,14 +1357,14 @@
2.77 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
2.78 Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
2.79 Rule.Num_Calc ("Prog_Expr.pow", (**)eval_binop "#power_"),
2.80 - (*Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult_commute}),
2.81 + (*Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
2.82 (*AC-rewriting*)
2.83 Rule.Thm ("real_mult_left_commute",
2.84 ThmC.numerals_to_Free @{thm real_mult_left_commute}),
2.85 - Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
2.86 - Rule.Thm ("add_commute",ThmC.numerals_to_Free @{thm add.commute}),
2.87 - Rule.Thm ("add_left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
2.88 - Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc}),
2.89 + Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
2.90 + Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
2.91 + Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
2.92 + Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
2.93 *)
2.94 Rule.Thm ("sym_realpow_twoI",
2.95 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
3.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Apr 15 10:07:43 2020 +0200
3.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Apr 15 11:11:54 2020 +0200
3.3 @@ -1237,17 +1237,17 @@
3.4 ord_make_polynomial_in false @{theory "Poly"}),
3.5 erls = Rule_Set.empty,srls = Rule_Set.Empty,
3.6 calc = [], errpatts = [],
3.7 - rules = [Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult.commute}),
3.8 + rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
3.9 (* z * w = w * z *)
3.10 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
3.11 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
3.12 - Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
3.13 + Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
3.14 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
3.15 - Rule.Thm ("add_commute",ThmC.numerals_to_Free @{thm add.commute}),
3.16 + Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
3.17 (*z + w = w + z*)
3.18 - Rule.Thm ("add_left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
3.19 + Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
3.20 (*x + (y + z) = y + (x + z)*)
3.21 - Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc})
3.22 + Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc})
3.23 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
3.24 ], scr = Rule.EmptyScr});
3.25
4.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed Apr 15 10:07:43 2020 +0200
4.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed Apr 15 11:11:54 2020 +0200
4.3 @@ -92,7 +92,7 @@
4.4 vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" and
4.5 vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" and
4.6
4.7 - (*klammer_plus_plus = (add_assoc RS sym)*)
4.8 + (*klammer_plus_plus = (add.assoc RS sym)*)
4.9 klammer_plus_minus: "a + (b - c) = (a + b) - c" and
4.10 klammer_minus_plus: "a - (b + c) = (a - b) - c" and
4.11 klammer_minus_minus: "a - (b - c) = (a - b) + c" and
4.12 @@ -312,7 +312,7 @@
4.13 val klammern_aufloesen =
4.14 Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [],
4.15 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
4.16 - rules = [Rule.Thm ("sym_add_assoc",
4.17 + rules = [Rule.Thm ("sym_add.assoc",
4.18 ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
4.19 (*"a + (b + c) = (a + b) + c"*)
4.20 Rule.Thm ("klammer_plus_minus",ThmC.numerals_to_Free @{thm klammer_plus_minus}),
5.1 --- a/src/Tools/isac/Knowledge/Root.thy Wed Apr 15 10:07:43 2020 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Apr 15 11:11:54 2020 +0200
5.3 @@ -212,17 +212,17 @@
5.4 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
5.5 (*"0 + z = z"*)
5.6
5.7 - Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult.commute}),
5.8 + Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
5.9 (*AC-rewriting*)
5.10 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
5.11 (**)
5.12 - Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
5.13 + Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
5.14 (**)
5.15 - Rule.Thm ("add_commute",ThmC.numerals_to_Free @{thm add.commute}),
5.16 + Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
5.17 (**)
5.18 - Rule.Thm ("add_left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
5.19 + Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
5.20 (**)
5.21 - Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc}),
5.22 + Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
5.23 (**)
5.24
5.25 Rule.Thm ("sym_realpow_twoI",
6.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Apr 15 10:07:43 2020 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Apr 15 11:11:54 2020 +0200
6.3 @@ -442,7 +442,7 @@
6.4 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
6.5 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
6.6 rules =
6.7 - [Rule.Thm ("sym_add_assoc",ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
6.8 + [Rule.Thm ("sym_add.assoc",ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
6.9 Rule.Thm ("sym_rmult_assoc",ThmC.numerals_to_Free (@{thm rmult_assoc} RS @{thm sym}))],
6.10 scr = Rule.EmptyScr
6.11 };
6.12 @@ -453,7 +453,7 @@
6.13 rules =
6.14 [Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}),
6.15 Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),
6.16 - Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc}),
6.17 + Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
6.18 Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),
6.19 Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),
6.20 Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc})],
6.21 @@ -486,7 +486,7 @@
6.22
6.23 Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}),
6.24 Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),
6.25 - Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc}),
6.26 + Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
6.27 Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),
6.28 Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),
6.29 Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc}),
6.30 @@ -624,17 +624,17 @@
6.31 (*"0 + z = z"*)
6.32
6.33 (*AC-rewriting*)
6.34 - Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult.commute}),
6.35 + Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
6.36 (* z * w = w * z *)
6.37 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
6.38 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
6.39 - Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
6.40 + Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
6.41 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
6.42 - Rule.Thm ("add_commute",ThmC.numerals_to_Free @{thm add.commute}),
6.43 + Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
6.44 (*z + w = w + z*)
6.45 - Rule.Thm ("add_left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
6.46 + Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
6.47 (*x + (y + z) = y + (x + z)*)
6.48 - Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc}),
6.49 + Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
6.50 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
6.51
6.52 Rule.Thm ("sym_realpow_twoI",
6.53 @@ -725,13 +725,13 @@
6.54 Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
6.55 Rule.Num_Calc ("Prog_Expr.pow", (**)eval_binop "#power_"),
6.56 (*
6.57 - Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult_commute}),
6.58 + Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
6.59 (*AC-rewriting*)
6.60 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
6.61 - Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
6.62 - Rule.Thm ("add_commute",ThmC.numerals_to_Free @{thm add_commute}),
6.63 - Rule.Thm ("add_left_commute",ThmC.numerals_to_Free @{thm add_left_commute}),
6.64 - Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add_assoc}),
6.65 + Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
6.66 + Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
6.67 + Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
6.68 + Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
6.69 *)
6.70
6.71 Rule.Thm ("sym_realpow_twoI",
7.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Wed Apr 15 10:07:43 2020 +0200
7.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Wed Apr 15 11:11:54 2020 +0200
7.3 @@ -55,22 +55,6 @@
7.4
7.5 val numerals_to_Free = ThmC_Def.numerals_to_Free; (* numeral \<rightarrow> Free ("int", T) *)
7.6
7.7 -(*
7.8 - "metaview" as seen from programs and from user input;
7.9 - both are parsed as terms by the function package.
7.10 -*)
7.11 -fun id_Isac_to_Isabelle thy thmid = (* Isac uses thmid *)
7.12 - let val thmid' = case thmid of
7.13 - "add_commute" => "add.commute"
7.14 - | "mult_commute" => "mult.commute"
7.15 - | "add_left_commute" => "add.left_commute"
7.16 - | "mult_left_commute" => "mult.left_commute"
7.17 - | "add_assoc" => "add.assoc"
7.18 - | "mult_assoc" => "mult.assoc"
7.19 - | _ => thmid
7.20 - in (Global_Theory.get_thm thy) thmid' end;
7.21 -(**)
7.22 -
7.23
7.24 (** handle symmetric equalities, generated by deriving input terms **)
7.25
7.26 @@ -95,8 +79,7 @@
7.27 | "#" :: _ =>
7.28 raise ERROR ("thm_from_thy not impl.for " ^ thmid)
7.29 | _ =>
7.30 - (**)thmid |> id_Isac_to_Isabelle thy |> numerals_to_Free(**)
7.31 - (** )thmid |> Global_Theory.get_thm thy |> numerals_to_Free( **)
7.32 + thmid |> Global_Theory.get_thm thy |> numerals_to_Free
7.33
7.34 (* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
7.35 fun sym_thm thm =
8.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Apr 15 10:07:43 2020 +0200
8.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Apr 15 11:11:54 2020 +0200
8.3 @@ -127,7 +127,7 @@
8.4 "Rewrite_Set_Inst [(''bdv'',v)] ''real_diff_minus''";
8.5 val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
8.6 " ((Try (Repeat (Rewrite ''real_diff_minus''))) #> \
8.7 - \ (Try (Repeat (Rewrite ''add_commute''))) #> \
8.8 + \ (Try (Repeat (Rewrite ''add.commute''))) #> \
8.9 \ (Try (Repeat (Rewrite ''mult_commute'')))) t";
8.10
8.11 fun rule2stac _ (Rule.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ HOLogic.mk_string thmID))
9.1 --- a/test/Tools/isac/Interpret/li-tool.sml Wed Apr 15 10:07:43 2020 +0200
9.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Apr 15 11:11:54 2020 +0200
9.3 @@ -38,7 +38,7 @@
9.4 val appltacs = specific_from_prog pt p;
9.5 case appltacs of
9.6 [Rewrite ("radd_commute", radd_commute),
9.7 - Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]
9.8 + Rewrite ("add.assoc", add_assoc), Calculate "TIMES"]
9.9 => if (UnparseC.term o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso
9.10 (UnparseC.term o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
9.11 else error "script.sml fun specific_from_prog diff.behav. 2"
10.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed Apr 15 10:07:43 2020 +0200
10.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Apr 15 11:11:54 2020 +0200
10.3 @@ -118,7 +118,7 @@
10.4 "----------- rewrite-order ord_simplify_System -------------------";
10.5 "----------- rewrite-order ord_simplify_System -------------------";
10.6 "M_b x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
10.7 -"--- add.commute ---"; (* ... add_commute cf. b42e334c97ee *)
10.8 +"--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
10.9 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
10.10 str2term"c * x") then ()
10.11 else error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";
10.12 @@ -131,7 +131,7 @@
10.13 str2term"c_2") then ()
10.14 else error "integrate.sml, (c * x) < (c_2) not#3";
10.15
10.16 -"--- mult_commute ---";
10.17 +"--- mult.commute ---";
10.18 if ord_simplify_System false thy [] (str2term"x * c",
10.19 str2term"c * x") then ()
10.20 else error "integrate.sml, (x * c) < (c * x) not#4";
11.1 --- a/test/Tools/isac/Knowledge/rational-old.sml Wed Apr 15 10:07:43 2020 +0200
11.2 +++ b/test/Tools/isac/Knowledge/rational-old.sml Wed Apr 15 11:11:54 2020 +0200
11.3 @@ -720,7 +720,7 @@
11.4 OK Thm ("sym_real_add_assoc",
11.5 "?z1.0 + (?z2.0 + ?z3.0) = ?z1.0 + ?z2.0 + ?z3.0"),
11.6 OK Thm
11.7 - ("sym_mult_assoc","?z1.0 * (?z2.0 * ?z3.0) = ?z1.0 * ?z2.0 * ?z3.0"),
11.8 + ("sym_mult.assoc","?z1.0 * (?z2.0 * ?z3.0) = ?z1.0 * ?z2.0 * ?z3.0"),
11.9 OK Thm ("sym_real_mult_left_commute",
11.10 "?z2.0 * (?z1.0 * ?z3.0) = ?z1.0 * (?z2.0 * ?z3.0)"),
11.11 OK Thm ("sym_mult_commute","?w * ?z = ?z * ?w"),
12.1 --- a/test/Tools/isac/Knowledge/rational.sml Wed Apr 15 10:07:43 2020 +0200
12.2 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Apr 15 11:11:54 2020 +0200
12.3 @@ -818,7 +818,7 @@
12.4 (revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\",9 = 3 * 3)" andalso
12.5 (revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso
12.6 (revsets |> nth 1 |> nth 7 |> Rule.to_string) =
12.7 - "Thm (\"sym_mult_assoc\",?a * (?b * ?c) = ?a * ?b * ?c)"
12.8 + "Thm (\"sym_mult.assoc\",?a * (?b * ?c) = ?a * ?b * ?c)"
12.9 then () else error "first 7 elements in revset changed"
12.10
12.11 (** find the rule 'r' to apply to term 't' **)
12.12 @@ -830,9 +830,9 @@
12.13 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x),
12.14 Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))","
12.15 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x),
12.16 - Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))","
12.17 + Thm ("sym_mult.assoc",""), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))","
12.18 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x),
12.19 - Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))","
12.20 + Thm ("sym_mult.assoc",""), ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))","
12.21 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))","
12.22 :
12.23 ### Isabelle2002:
12.24 @@ -916,7 +916,7 @@
12.25 (make_polynomial enth"alt zu viele rules)
12.26 WN060823 'init_state' requires rewriting on specified location in the term
12.27 default_print_depth 99; Rfuns; default_print_depth 3;
12.28 -WN060831 cycling "sym_order_mult_rls_" "sym_mult_assoc"
12.29 +WN060831 cycling "sym_order_mult_rls_" "sym_mult.assoc"
12.30 as was with make_polynomial before ?!?*)
12.31
12.32 val SOME r = nex revsets t;
13.1 --- a/test/Tools/isac/Knowledge/rlang.sml Wed Apr 15 10:07:43 2020 +0200
13.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Wed Apr 15 11:11:54 2020 +0200
13.3 @@ -1432,13 +1432,13 @@
13.4 ## rls: expand on:
13.5 ## rls: reduce_0_1_2 on:
13.6 ## rls: order_add_mult on:
13.7 -### try thm: mult_commute
13.8 +### try thm: mult.commute
13.9 === rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = b * (4 * a) / (a ^^^ 2 + -1 * b ^^^ 2)
13.10
13.11 ### try thm: real_mult_left_commute
13.12 === rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = 4 * (b * a) / (a ^^^ 2 + -1 * b ^^^ 2)
13.13
13.14 -### try thm: mult_commute
13.15 +### try thm: mult.commute
13.16 === rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)
13.17
13.18 ### try calc: op *'
14.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Apr 15 10:07:43 2020 +0200
14.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Apr 15 11:11:54 2020 +0200
14.3 @@ -128,7 +128,7 @@
14.4 (*if*) p = ([], Res) (*else*);
14.5 (*if*) member op = [Pbl,Met] p_ (*else*);
14.6
14.7 - val (_, ([(Rewrite ("add_assoc", _), _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);
14.8 + val (_, ([(Rewrite ("add.assoc", _), _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);
14.9 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
14.10 = (auto, (c @ c'), ptp');
14.11 (*if*) p = ([], Res) (*else*);