Test_Some.thy + rewrite.sml + poly.sml ok: real_mult_minus1_sym works with is_atom
1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Mon Jul 12 17:21:37 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Tue Jul 13 08:52:35 2021 +0200
1.3 @@ -13,7 +13,16 @@
1.4
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 -\<close> ML \<open>
1.8 +\<close> text \<open>
1.9 +fun string_of_atom (t as Const ("Num.numeral_class.numeral", _) $ _) = dest_numeral' t
1.10 +(*
1.11 + | string_of_atom (t as Const ("Groups.one_class.one", _)) = HOLogic.dest_numeral t
1.12 + | string_of_atom (t as Const ("Groups.zero_class.zero", _)) = HOLogic.dest_numeral t
1.13 + | string_of_atom (Const (str, _)) = str
1.14 + | string_of_atom (Free _) = true
1.15 + | string_of_atom (Var _) = true
1.16 + | string_of_atom _ = false;
1.17 +*)
1.18 \<close> ML \<open>
1.19 \<close> ML \<open>
1.20 \<close> ML \<open>
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Jul 12 17:21:37 2021 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Tue Jul 13 08:52:35 2021 +0200
2.3 @@ -551,7 +551,9 @@
2.4 |> typ_a2real; (*TODO drop*)
2.5 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
2.6
2.7 -fun is_atom (Const ("Float.Float",_) $ _) = true
2.8 +fun is_atom (Const ("Num.numeral_class.numeral", _) $ _) = true
2.9 + | is_atom (Const ("Groups.one_class.one", _)) = true
2.10 + | is_atom (Const ("Groups.zero_class.zero", _)) = true
2.11 | is_atom (Const _) = true
2.12 | is_atom (Free _) = true
2.13 | is_atom (Var _) = true
3.1 --- a/src/Tools/isac/Knowledge/Poly.thy Mon Jul 12 17:21:37 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Jul 13 08:52:35 2021 +0200
3.3 @@ -169,6 +169,8 @@
3.4
3.5 real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)" and
3.6 real_mult_minus1: "-1 * z = - (z::real)" and
3.7 + (*sym_real_mult_minus1 expands indefinitely without assumptions ...*)
3.8 + real_mult_minus1_sym: "[| \<not>(matches (- 1 * x) z); \<not>(z is_atom) |] ==> - (z::real) = -1 * z" and
3.9 real_mult_2: "2 * z = z + (z::real)" and
3.10
3.11 real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
3.12 @@ -702,22 +704,13 @@
3.13 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
3.14 ], scr = Rule.Empty_Prog};
3.15
3.16 -val discard_minus =
3.17 - Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
3.18 - erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
3.19 - rules =
3.20 - [Rule.Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}) (*,*)
3.21 - (*"a - b = a + -1 * b"*)
3.22 - (* superfluous since proper "uminus", but shifted realpow_minus_even, realpow_minus_odd here.
3.23 - Rule.Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym}))
3.24 - "- ?z = -1 * ?z"*)],
3.25 - scr = Rule.Empty_Prog};
3.26 -
3.27 -(*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
3.28 +(* erls for calculate_Rational + etc *)
3.29 val powers_erls =
3.30 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
3.31 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
3.32 - rules = [Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
3.33 + rules =
3.34 + [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),
3.35 + Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
3.36 Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"),
3.37 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
3.38 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
3.39 @@ -726,6 +719,17 @@
3.40 ],
3.41 scr = Rule.Empty_Prog
3.42 };
3.43 +
3.44 +val discard_minus =
3.45 + Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
3.46 + erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
3.47 + rules =
3.48 + [Rule.Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}),
3.49 + (*"a - b = a + -1 * b"*)
3.50 + Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym}))
3.51 + (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)],
3.52 + scr = Rule.Empty_Prog};
3.53 +
3.54 val expand_poly_ =
3.55 Rule_Def.Repeat{id = "expand_poly_", preconds = [],
3.56 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
3.57 @@ -932,10 +936,9 @@
3.58 val expand_poly =
3.59 Rule_Def.Repeat{id = "expand_poly", preconds = [],
3.60 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
3.61 - erls = Rule_Set.empty,srls = Rule_Set.Empty,
3.62 - calc = [], errpatts = [],
3.63 - (*asm_thm = [],*)
3.64 - rules = [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
3.65 + erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
3.66 + rules =
3.67 + [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
3.68 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
3.69 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
3.70 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
3.71 @@ -957,9 +960,8 @@
3.72 (*"- (- ?z) = ?z"*)
3.73 Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
3.74 (*"a - b = a + -1 * b"*)
3.75 - Rule.Thm ("sym_real_mult_minus1",
3.76 - ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym}))
3.77 - (*- ?z = "-1 * ?z"*)
3.78 + Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym}))
3.79 + (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
3.80
3.81 (*Rule.Thm ("real_minus_add_distrib",
3.82 ThmC.numerals_to_Free @{thm real_minus_add_distrib}),*)
4.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Jul 12 17:21:37 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Jul 13 08:52:35 2021 +0200
4.3 @@ -325,7 +325,7 @@
4.4 val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
4.5 Rule_Set.append_rules "PolyEq_prls" Rule_Set.empty
4.6 [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
4.7 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
4.8 + Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),
4.9 Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs ""),
4.10 Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""),
4.11 Rule.Eval ("Poly.is_expanded_in", eval_is_expanded_in ""),
5.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Jul 12 17:21:37 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Jul 13 08:52:35 2021 +0200
5.3 @@ -406,7 +406,8 @@
5.4 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
5.5 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
5.6 rules =
5.7 - [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
5.8 + [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),
5.9 + Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
5.10 Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
5.11 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
5.12 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
6.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Mon Jul 12 17:21:37 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Tue Jul 13 08:52:35 2021 +0200
6.3 @@ -20,8 +20,8 @@
6.4 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
6.5 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
6.6 (* 1 * z = z *)
6.7 - Rule.Thm ("sym_real_mult_minus1",ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})),
6.8 - (* "- z1 = -1 * z1" *)
6.9 + Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym})),
6.10 + (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
6.11 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_")
6.12 ];
6.13
7.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Mon Jul 12 17:21:37 2021 +0200
7.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Tue Jul 13 08:52:35 2021 +0200
7.3 @@ -279,13 +279,12 @@
7.4 | eval_some_occur_in _ _ _ _ = NONE;
7.5
7.6 (*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
7.7 -fun eval_is_atom (thmid:string) "Prog_Expr.is_atom"
7.8 - (t as (Const _ $ arg)) _ =
7.9 - (case arg of
7.10 - Free (n,_) => SOME (TermC.mk_thmid thmid n "",
7.11 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
7.12 - | _ => SOME (TermC.mk_thmid thmid "" "",
7.13 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
7.14 +fun eval_is_atom (thmid:string) "Prog_Expr.is_atom" (t as (Const _ $ arg)) _ =
7.15 + if TermC.is_atom arg
7.16 + then SOME (TermC.mk_thmid thmid "" "",
7.17 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
7.18 + else SOME (TermC.mk_thmid thmid "" "",
7.19 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
7.20 | eval_is_atom _ _ _ _ = NONE;
7.21
7.22 fun even i = (i div 2) * 2 = i;
8.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Mon Jul 12 17:21:37 2021 +0200
8.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Tue Jul 13 08:52:35 2021 +0200
8.3 @@ -6,6 +6,7 @@
8.4 "-----------------------------------------------------------------------------------------------";
8.5 "table of contents -----------------------------------------------------------------------------";
8.6 "-----------------------------------------------------------------------------------------------";
8.7 +"----------- fun is_atom -----------------------------------------------------------------------";
8.8 "----------- numerals in Isabelle2011/12/13 -------------";
8.9 "----------- inst_bdv -----------------------------------";
8.10 "----------- subst_atomic_all ---------------------------";
8.11 @@ -35,6 +36,10 @@
8.12 "--------------------------------------------------------";
8.13 "--------------------------------------------------------";
8.14
8.15 +"----------- fun is_atom -----------------------------------------------------------------------";
8.16 +"----------- fun is_atom -----------------------------------------------------------------------";
8.17 +"----------- fun is_atom -----------------------------------------------------------------------";
8.18 +
8.19 "----------- numerals in Isabelle2011/12/13 -------------";
8.20 "----------- numerals in Isabelle2011/12/13 -------------";
8.21 "----------- numerals in Isabelle2011/12/13 -------------";
9.1 --- a/test/Tools/isac/Test_Some.thy Mon Jul 12 17:21:37 2021 +0200
9.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 13 08:52:35 2021 +0200
9.3 @@ -1195,11 +1195,49 @@
9.4 BUT: this raises no exn ! ! !*)
9.5 \<close> ML \<open>
9.6 Rewrite.trace_on := false;
9.7 +\<close> text \<open>
9.8 Rewrite.trace_on := true;
9.9 -\<close> text \<open> (*exception TERM raised dest_number - 2 + 3 * x*)
9.10 +\<close> ML \<open> (*norm_Rational: exception TERM raised dest_number - 2 + 3 * x*)
9.11 val SOME (t', _) = rewrite_set_ thy false norm_Rational t;
9.12 \<close> ML \<open>
9.13 @{thm real_mult_minus1}
9.14 +\<close> ML \<open>
9.15 +
9.16 +@{term 0};
9.17 +\<close> ML \<open>
9.18 +"----------- fun is_atom -----------------------------------------------------------------------";
9.19 +"----------- fun is_atom -----------------------------------------------------------------------";
9.20 +"----------- fun is_atom -----------------------------------------------------------------------";
9.21 +\<close> ML \<open>
9.22 +\<close> ML \<open>
9.23 +if is_atom @{term 0} then () else error "is_atom 1 CHANGED";
9.24 +val eval_t = @{term "1 is_atom"};
9.25 +case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
9.26 + SOME ("#is_atom__", _) => ()
9.27 +| _ => error "eval_is_atom 1 CHANGED";
9.28 +\<close> ML \<open>
9.29 +Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t ()
9.30 +\<close> ML \<open>
9.31 +\<close> ML \<open>
9.32 +\<close> ML \<open>
9.33 +if is_atom @{term 1} then () else error "is_atom 1 CHANGED";
9.34 +val eval_t = @{term "1 is_atom"};
9.35 +case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
9.36 + SOME ("#is_atom__", _) => ()
9.37 +| _ => error "eval_is_atom 1 CHANGED";
9.38 +\<close> ML \<open>
9.39 +Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t ()
9.40 +\<close> ML \<open>
9.41 +\<close> ML \<open>
9.42 +\<close> ML \<open>
9.43 +val eval_t = @{term "0 is_atom"};
9.44 +\<close> text \<open>
9.45 +string_of_atom
9.46 +\<close> ML \<open>
9.47 +\<close> ML \<open>
9.48 +\<close> ML \<open>
9.49 +\<close> ML \<open>
9.50 +\<close> ML \<open>
9.51 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
9.52
9.53 if poly_of_term vs (TermC.str2term "12::real") = SOME [(12, [0, 0, 0])]
9.54 @@ -1813,6 +1851,7 @@
9.55 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]")
9.56 then () else error "rational.sml cancel Schalk 188a";
9.57
9.58 +\<close> ML \<open>
9.59 val t = TermC.str2term "(8*((-1) + x))/(9*((-1) + x))";
9.60 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
9.61 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]")
9.62 @@ -1853,6 +1892,7 @@
9.63 ("(1 + 3 * a + 9 * a \<up> 2 + 27 * a \<up> 3) /\n(3 * a + 18 * a \<up> 2 + 27 * a \<up> 3)", "[]")
9.64 then () else error "rational.sml make_polynomial Schalk 190c";
9.65
9.66 +\<close> ML \<open>
9.67 "-------- example 191a";
9.68 val t = TermC.str2term "( x \<up> 2 + -1 * y \<up> 2 ) / ( x + y )";
9.69 is_expanded (TermC.str2term "x \<up> 2 + - 1 * y \<up> 2") = false; (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
9.70 @@ -1861,6 +1901,7 @@
9.71 if (UnparseC.term t', UnparseC.terms asm) = ("(x + - 1 * y) / 1", "[]")
9.72 then () else error "rational.sml make_polynomial Schalk 191a";
9.73
9.74 +\<close> ML \<open>
9.75 "-------- example 191b";
9.76 val t = TermC.str2term "((x + (- 1) * y)*(x + y))/((1)*(x + y))";
9.77 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
9.78 @@ -1874,40 +1915,47 @@
9.79 is_expanded (TermC.str2term "25 + -30*x + 9*x \<up> 2") = true;
9.80 is_expanded (TermC.str2term "-25 + 9*x \<up> 2") = true;
9.81
9.82 +\<close> ML \<open>
9.83 val t = TermC.str2term "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
9.84 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
9.85 if (UnparseC.term t', UnparseC.terms asm) = ("(25 + - 30 * x + 9 * x \<up> 2) / (- 25 + 9 * x \<up> 2)", "[]")
9.86 then () else error "rational.sml make_polynomial Schalk 191c";
9.87
9.88 +\<close> ML \<open>
9.89 "-------- example 192b";
9.90 val t = TermC.str2term "( 7 * x \<up> 3 + - 1 * x \<up> 2 * y ) / ( 7 * x * y \<up> 2 + - 1 * y \<up> 3 )";
9.91 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
9.92 if (UnparseC.term t', UnparseC.terms asm) = ("x \<up> 2 / y \<up> 2", "[\"y \<up> 2 \<noteq> 0\"]")
9.93 then () else error "rational.sml cancel_p Schalk 192b";
9.94
9.95 +\<close> ML \<open>
9.96 val t = TermC.str2term "((x \<up> 2)*(7 * x + (-1) * y))/((y \<up> 2)*(7 * x + (-1) * y))";
9.97 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
9.98 if (UnparseC.term t', UnparseC.terms asm) =
9.99 ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]")
9.100 then () else error "rational.sml make_polynomial Schalk 192b";
9.101
9.102 +\<close> ML \<open>
9.103 val t = TermC.str2term "((x \<up> 2)*(7 * x + (-1) * y))/((y \<up> 2)*(7 * x + (-1) * y))";
9.104 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
9.105 if (UnparseC.term t', UnparseC.terms asm) =
9.106 ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]")
9.107 then () else error "rational.sml make_polynomial Schalk WN050929 not working";
9.108
9.109 +\<close> ML \<open>
9.110 val t = TermC.str2term "( x \<up> 2 + -6 * x + 9 ) / ( x \<up> 2 + -9 )";
9.111 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
9.112 if (UnparseC.term t', UnparseC.terms asm) = ("(- 3 + x) / (3 + x)", "[\"3 + x \<noteq> 0\"]")
9.113 then () else error "rational.sml cancel_p Schalk 193a";
9.114
9.115 +\<close> ML \<open>
9.116 "-------- example 193b";
9.117 val t = TermC.str2term "( x \<up> 2 + -8 * x + 16 ) / ( 2 * x \<up> 2 + -32 )";
9.118 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
9.119 if (UnparseC.term t', UnparseC.terms asm) = ("(- 4 + x) / (8 + 2 * x)", "[\"8 + 2 * x \<noteq> 0\"]")
9.120 then () else error "rational.sml cancel_p Schalk 193b";
9.121
9.122 +\<close> ML \<open>
9.123 "-------- example 193c";
9.124 val t = TermC.str2term "( 2 * x + -50 * x \<up> 3 ) / ( 25 * x \<up> 2 + -10 * x + 1 )";
9.125 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
9.126 @@ -1915,6 +1963,7 @@
9.127 ("(2 * x + 10 * x \<up> 2) / (1 + - 5 * x)", "[\"1 + - 5 * x \<noteq> 0\"]")
9.128 then () else error "rational.sml cancel_p Schalk 193c";
9.129
9.130 +\<close> ML \<open>
9.131 (*WN: improved with new numerals*)
9.132 val t = TermC.str2term "(-25 + 9*x \<up> 2)/(5 + 3*x)";
9.133 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
9.134 @@ -2147,20 +2196,16 @@
9.135 *)
9.136
9.137 \<close> ML \<open>
9.138 -\<close> ML \<open>
9.139 -@{thm real_mult_minus1}
9.140 -\<close> ML \<open>
9.141 "-------- examples: rls norm_Rational ----------------------------------------";
9.142 "-------- examples: rls norm_Rational ----------------------------------------";
9.143 "-------- examples: rls norm_Rational ----------------------------------------";
9.144 val t = TermC.str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
9.145 -\<close> text \<open> (*norm_Rational: exception TERM dest_number - 2 + 3 * x*)
9.146 +\<close> ML \<open>
9.147 val SOME (t', _) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
9.148 if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1";
9.149
9.150 \<close> ML \<open>
9.151 val t = TermC.str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
9.152 -\<close> text \<open> (*norm_Rational: exception TERM dest_number - 3 + 13 * x*)
9.153 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
9.154 if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then ()
9.155 else error "rational.sml 2";
9.156 @@ -2485,6 +2530,7 @@
9.157 then () else error "rational.sml: diff.behav. in norm_Rational_mg 21";
9.158
9.159
9.160 +\<close> text \<open> (*cancel_p loops since "sym_real_mult_minus1"*)
9.161 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
9.162 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
9.163 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
9.164 @@ -2494,7 +2540,7 @@
9.165 if UnparseC.term t = "(- 5 * x + 5 * y) / (- 18 * x + - 18 * y)"
9.166 then () else error "rational.sml: diff.behav. in norm_Rational_mg 22";
9.167
9.168 -\<close> ML \<open>
9.169 +\<close> text \<open> (*cancel_p loops since "sym_real_mult_minus1"*)
9.170 (*------- SRM.test Schalk I, p.68 Nr. 436b *)
9.171 val t = TermC.str2term "5*a*(a - b) \<up> 2*(a + b) \<up> 3/(7*b*(a - b) \<up> 3) * 7*b/(a + b) \<up> 3";
9.172 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
9.173 @@ -2524,7 +2570,7 @@
9.174 else error "rational.sml: diff.behav. in norm_Rational_mg 24";
9.175 *)
9.176
9.177 -\<close> ML \<open>
9.178 +\<close> text \<open> (*cancel_p loops since "sym_real_mult_minus1"*)
9.179 "----- S.K. corrected non-termination 060904";
9.180 val t = TermC.str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a \<up> 2 - 16*b \<up> 2))";
9.181 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
9.182 @@ -2676,7 +2722,7 @@
9.183 then () else error "rational.sml: diff.behav. in norm_Rational_mg 53";
9.184
9.185
9.186 -\<close> ML \<open> (*double fractions MANY EXAMPLES*)
9.187 +\<close> ML \<open>
9.188 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";
9.189 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";
9.190 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";
9.191 @@ -2991,11 +3037,11 @@
9.192 | _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";
9.193
9.194
9.195 -\<close> ML \<open>
9.196 +\<close> text \<open> (*rulesets for cancel_p loops since "sym_real_mult_minus1"*)
9.197 "-------- investigate rulesets for cancel_p ----------------------------------";
9.198 "-------- investigate rulesets for cancel_p ----------------------------------";
9.199 "-------- investigate rulesets for cancel_p ----------------------------------";
9.200 -val thy = @{theory "Rational"};
9.201 +val thy = @ {theory "Rational"};
9.202 val t = TermC.str2term "(a \<up> 2 + -1*b \<up> 2) / (a \<up> 2 + -2*a*b + b \<up> 2)";
9.203 val tt = TermC.str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*);
9.204
9.205 @@ -3006,27 +3052,27 @@
9.206 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
9.207 if UnparseC.term tt' = "a \<up> 2 + - 2 * a * b + b \<up> 2" then () else error "rls chancel_p 2";
9.208
9.209 -\<close> ML \<open> (*factout_p_ \<longrightarrow> NONE*)
9.210 +\<close> text \<open> (*factout_p_ ff*)
9.211 "----- with .make_deriv; WN1130912 not investigated further, will be discontinued";
9.212 val SOME (tt, _) = factout_p_ thy t;
9.213 if UnparseC.term tt = "(a + b) * (a + - 1 * b) / ((a + - 1 * b) * (a + - 1 * b))"
9.214 then () else error "rls chancel_p 3";
9.215
9.216 -\<close> ML \<open>
9.217 +\<close> text \<open> (*factout_p_ ff*)
9.218 "--- with simpler ruleset";
9.219 val {rules, rew_ord= (_, ro), ...} = Rule_Set.rep (assoc_rls "rev_rew_p");
9.220 val der = Derive.do_one thy Atools_erls rules ro NONE tt;
9.221
9.222 if length der = 12 then () else error "WN1130912 rls chancel_p 4";
9.223 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
9.224 -\<close> ML \<open>
9.225 +\<close> text \<open> (*factout_p_ ff*)
9.226
9.227 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*)
9.228 "...,(-1 * b \<up> 2 + a \<up> 2) / (-2 * (a * b) + a \<up> 2 + (-1 * b) \<up> 2) ]";
9.229 (*default_print_depth 99;*) map (Rule.to_string o #2) der; (*default_print_depth 3;*)
9.230 (*default_print_depth 99;*) map (UnparseC.term o #1 o #3) der; (*default_print_depth 3;*)
9.231
9.232 -\<close> ML \<open>
9.233 +\<close> text \<open> (*factout_p_ ff*)
9.234 val der = Derive.do_one thy Atools_erls rules ro NONE
9.235 (TermC.str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
9.236 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
9.237 @@ -3050,7 +3096,7 @@
9.238 then () else error "get_denominator ((a + x) / b) = b"
9.239
9.240
9.241 -\<close> ML \<open>
9.242 +\<close> text \<open> (*several errpats loops since "sym_real_mult_minus1"*)
9.243 "-------- several errpats in complicated term --------------------------------";
9.244 "-------- several errpats in complicated term --------------------------------";
9.245 "-------- several errpats in complicated term --------------------------------";