1.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Sun Aug 08 15:21:33 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Mon Aug 09 11:19:25 2021 +0200
1.3 @@ -1,4 +1,4 @@
1.4 -(* Title: tests for rationals
1.5 +(* Title: "Knowledge/rational-2.sml"
1.6 Author: Walther Neuper
1.7 Use is subject to license terms.
1.8 *)
1.9 @@ -434,7 +434,7 @@
1.10 (* Rewrite.trace_on:
1.11 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.12 (* |||||||||||||||||||||||||||| *)
1.13 -val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
1.14 +val t = TermC.str2term (* ||||||||||||||||||||||||| *)
1.15 "AA / 4 + (BB / 2 + - 1 * BB / 2)";
1.16 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
1.17 val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
1.18 @@ -444,11 +444,9 @@
1.19
1.20 val vs = TermC.vars_of t;
1.21 val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =
1.22 - (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
1.23 -
1.24 + (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
1.25 "~~~~~ fun poly_of_term , args:"; val (vs, t) = (vs, n1);
1.26 -val SOME [(1, [xxx, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];
1.27 -(*+*)if xxx = 1 then () else error "monom_of_term changed"
1.28 +val SOME [(1, [1, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];
1.29
1.30 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (id, _))) =
1.31 (vs, (1, replicate (length vs) 0), t);
1.32 @@ -721,23 +719,21 @@
1.33 val (t, _, revsets, _) = ini t;
1.34
1.35 if length (hd revsets) = 11 then () else error "length of revset changed";
1.36 -(*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
1.37 -if (revsets |> nth 1 |> nth 1 |> id_of_thm) =
1.38 +if (revsets |> nth 1 |> nth 1 |> Rule.id) =
1.39 (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id)
1.40 then () else error "first element of revset changed";
1.41 if
1.42 -(revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\",?r1 \<up> 2 = ?r1 * ?r1)" andalso
1.43 -(revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 \<up> 2\",9 = 3 \<up> 2)" andalso
1.44 -(revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\",6 * x = 2 * (3 * x))"
1.45 +(revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\", ?r1 \<up> 2 = ?r1 * ?r1)" andalso
1.46 +(revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 \<up> 2\", 9 = 3 \<up> 2)" andalso
1.47 +(revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\", 6 * x = 2 * (3 * x))"
1.48 andalso
1.49 -(revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: -3 * x = - 1 * (3 * x)\",-3 * x = - 1 * (3 * x))"
1.50 +(revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: - 3 * x = - 1 * (3 * x)\", - 3 * x = - 1 * (3 * x))"
1.51 andalso
1.52 -(revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\",9 = 3 * 3)" andalso
1.53 +(revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\", 9 = 3 * 3)" andalso
1.54 (revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso
1.55 (revsets |> nth 1 |> nth 7 |> Rule.to_string) =
1.56 - "Thm (\"sym_mult.assoc\",?a * (?b * ?c) = ?a * ?b * ?c)"
1.57 + "Thm (\"sym_mult.assoc\", ?a * (?b * ?c) = ?a * ?b * ?c)"
1.58 then () else error "first 7 elements in revset changed"
1.59 - \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
1.60
1.61 (** find the rule 'r' to apply to term 't' **)
1.62 (*/------- WN1309: since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_
1.63 @@ -865,8 +861,7 @@
1.64 "HOL.True";
1.65
1.66 val t = TermC.str2term "(6*x) \<up> 2";
1.67 -val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false
1.68 - (ThmC.numerals_to_Free @{thm realpow_def_atom}) t;
1.69 +val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false @{thm realpow_def_atom} t;
1.70 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then ()
1.71 else error "rational.sml powers_erls (6*x) \<up> 2";
1.72
1.73 @@ -1419,7 +1414,7 @@
1.74 if UnparseC.term t = "- 3 * b \<up> 3 / (- 2 * a + 2 * b)"
1.75 then () else error "rational.sml: diff.behav. in norm_Rational_mg 48";
1.76
1.77 -(*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
1.78 +
1.79 "-------- me Schalk I No.186 -------------------------------------------------";
1.80 "-------- me Schalk I No.186 -------------------------------------------------";
1.81 "-------- me Schalk I No.186 -------------------------------------------------";
1.82 @@ -1441,11 +1436,10 @@
1.83 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
1.84 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
1.85 case (f2str f, nxt) of
1.86 - ("14", ("End_Proof'", _)) => ()
1.87 + ("14", End_Proof') => ()
1.88 | _ => error "rational.sml diff.behav. in me Schalk I No.186";
1.89 - \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
1.90
1.91 -(*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
1.92 +
1.93 "-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
1.94 "-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
1.95 "-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
1.96 @@ -1488,15 +1482,14 @@
1.97 val (t, asm) = get_obj g_result pt [1, 2];
1.98 if UnparseC.term t = "(2 + - 1 * x) / (2 * a) / (2 * a / (x + - 1 * 2))" andalso UnparseC.terms asm = "[]"
1.99 then () else error "3rd interSteps ..Simp_Rat_Double_No- 1 changed on [1, 2]";
1.100 - \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
1.101
1.102
1.103 -(*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
1.104 +
1.105 "-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
1.106 "-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
1.107 "-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
1.108 reset_states ();
1.109 -CalcTree [(["Term ((a^2 + - 1*b^2) / (a^2 + - 2*a*b + b^2))", "normalform N"],
1.110 +CalcTree [(["Term ((a \<up> 2 + - 1*b \<up> 2) / (a \<up> 2 + - 2*a*b + b \<up> 2))", "normalform N"],
1.111 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
1.112 Iterator 1;
1.113 moveActiveRoot 1;
1.114 @@ -1566,7 +1559,6 @@
1.115 val (_, tac, _) = ME_Misc.pt_extract (pt, p);
1.116 case tac of SOME (Rewrite ("sym_distrib_left", _)) => ()
1.117 | _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";
1.118 - \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
1.119
1.120
1.121 "-------- investigate rulesets for cancel_p ----------------------------------";