1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Mon Aug 02 11:38:40 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Aug 02 15:25:49 2021 +0200
1.3 @@ -171,6 +171,7 @@
1.4 real_mult_minus1: "-1 * z = - (z::real)" and
1.5 (*sym_real_mult_minus1 expands indefinitely without assumptions ...*)
1.6 real_mult_minus1_sym: "[| \<not>(matches (- 1 * x) z); \<not>(z is_num) |] ==> - (z::real) = -1 * z" and
1.7 + real_minus_mult_left: "\<not> ((a::real) is_num) ==> (- a) * b = - (a * b)" and
1.8 real_mult_2: "2 * z = z + (z::real)" and
1.9
1.10 real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
1.11 @@ -1031,20 +1032,22 @@
1.12 val reduce_012 =
1.13 Rule_Def.Repeat{id = "reduce_012", preconds = [],
1.14 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.15 - erls = Rule_Set.empty,srls = Rule_Set.Empty,
1.16 - calc = [], errpatts = [],
1.17 + erls = Rule_Set.append_rules "erls_in_reduce_012" Rule_Set.empty [
1.18 + \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
1.19 + \<^rule_thm>\<open>not_false\<close>,
1.20 + \<^rule_thm>\<open>not_true\<close>],
1.21 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.22 rules = [\<^rule_thm>\<open>mult_1_left\<close>,
1.23 (*"1 * z = z"*)
1.24 (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*)
1.25 (*"-1 * z = - z"*)
1.26 - Rule.Thm ("minus_mult_left", (@{thm minus_mult_left} RS @{thm sym})),
1.27 - (*- (?x * ?y) = "- ?x * ?y"*)
1.28 + \<^rule_thm>\<open>real_minus_mult_left\<close>, (*"\<not> ((a::real) is_num) ==> (- a) * b = - (a * b)"*)
1.29 (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>,
1.30 (*"- ?x * - ?y = ?x * ?y"*)---*)
1.31 \<^rule_thm>\<open>mult_zero_left\<close>,
1.32 (*"0 * z = 0"*)
1.33 - \<^rule_thm>\<open>add_0_left\<close>,
1.34 - (*"0 + z = z"*)
1.35 + \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
1.36 + \<^rule_thm>\<open>add_0_right\<close>, (*"a + - a = 0"*)
1.37 \<^rule_thm>\<open>right_minus\<close>,
1.38 (*"?z + - ?z = 0"*)
1.39 \<^rule_thm_sym>\<open>real_mult_2\<close>,
2.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Mon Aug 02 11:38:40 2021 +0200
2.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Mon Aug 02 15:25:49 2021 +0200
2.3 @@ -177,25 +177,13 @@
2.4
2.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. solve-phase *)
2.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.7 -
2.8 -
2.9 -(* TOODOO make_ratpoly: "- 6 * x + 5 * x \<up> 2 = 0" \<longrightarrow> "- (6 * x) + 5 * x \<up> 2 = 0" ------------\\
2.10 -NO NO -----------------^^^^^^^^^^^^^^^^^, rather:
2.11 -## rls: reduce_012 on: - 6 * x + 5 * x \<up> 2 = 0
2.12 -### try thm: "mult_1_left"
2.13 -### try thm: "minus_mult_left"
2.14 -#### eval asms: "- 6 * x = - (6 * x)"
2.15 - ^^^^^^^^ HERE APPLIES minus_mult_left SINCE NEW numerals
2.16 -### rewrites to: "- (6 * x) + 5 * x \<up> 2 = 0"
2.17 -
2.18 -(* IN THE STEP BELOW ---vvv--- THE SYSTEM HANGS *)
2.19 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x \<up> 2 = 0";
2.20
2.21 -if p = ([4, 3], Res) andalso f2str f = "-6 * x + 5 * x \<up> 2 = 0"
2.22 +if p = ([4, 3], Res) andalso f2str f = "- 6 * x + 5 * x \<up> 2 = 0"
2.23 then
2.24 ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()
2.25 | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
2.26 -else error "xxx";
2.27 +else error "Subproblem ([4, 3], Res) CHANGED";
2.28
2.29 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 2. specify-phase *)
2.30 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.31 @@ -215,12 +203,12 @@
2.32
2.33 (* *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [
2.34 (*0.pre*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
2.35 -(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) \<or>\n"
2.36 -(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
2.37 -(*2.pre*) "lhs (-6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
2.38 -(*2.pre*) "lhs (-6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
2.39 +(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n"
2.40 +(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
2.41 +(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
2.42 +(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
2.43 (*0.asm*) "x \<noteq> 0",
2.44 -(*0.asm*) "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
2.45 +(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
2.46 (* *)])
2.47 (* *)then () else error "assumptions at end 2. Subproblem CHANGED";
2.48 (*[4, 4], Res*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt;(*\<rightarrow>1. Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
2.49 @@ -260,11 +248,11 @@
2.50 (*NEW*) | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc";
2.51
2.52 (* *)if eq_set op = (map UnparseC.term (get_assumptions ctxt_parent), [
2.53 -(*0.pre*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
2.54 -(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) \<or>\n"
2.55 -(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
2.56 +(*0.pre*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
2.57 +(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n"
2.58 +(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
2.59 (*0.asm*) "x \<noteq> 0",
2.60 -(*0.asm*) "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
2.61 +(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
2.62 (* *)])
2.63 (* *)then () else error "assumptions at xxx CHANGED";
2.64
2.65 @@ -272,12 +260,12 @@
2.66 ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent;
2.67 (* *)if eq_set op = (map UnparseC.term (get_assumptions ctxt'), [
2.68 (*0.pre*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
2.69 -(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) \<or>\n"
2.70 -(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
2.71 -(*0.asm*) "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
2.72 +(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n"
2.73 +(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
2.74 +(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
2.75 (*0.asm*) "x \<noteq> 0", (* <----------------------- "x \<noteq> 0" contradiction resoved ---\*)
2.76 -(*2.pre*) "lhs (-6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
2.77 -(*2.pre*) "lhs (-6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
2.78 +(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
2.79 +(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
2.80 (*2.res*) (*"x \<noteq> 0",*) "x = 6 / 5" (* <---------------- "x \<noteq> 0" would contradict "x = 0" ---/*)
2.81 (* *)])
2.82 (* *)then () else error "assumptions at xxx CHANGED";
2.83 @@ -317,12 +305,11 @@
2.84 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)
2.85
2.86 (*/-------- final test -----------------------------------------------------------------------\*)
2.87 -if f2str f = "[x = 6 / 5]" andalso map UnparseC.term (Ctree.get_assumptions pt p) =
2.88 - ["x = 6 / 5", "lhs (-6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
2.89 - "lhs (-6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
2.90 - "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) \<or>\n\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
2.91 - "x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
2.92 +if f2str f = "[x = 6 / 5]" andalso map UnparseC.term (Ctree.get_assumptions pt p) = [
2.93 + "x = 6 / 5",
2.94 + "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x", "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
2.95 + "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
2.96 + "x \<noteq> 0",
2.97 + "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
2.98 "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"]
2.99 then () else error "test CHANGED";
2.100 -(**) TOODOO make_ratpoly: "- 6 * x + 5 * x \<up> 2 = 0" \<longrightarrow> "- (6 * x) + 5 * x \<up> 2 = 0" --------//*)
2.101 -
3.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Aug 02 11:38:40 2021 +0200
3.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Mon Aug 02 15:25:49 2021 +0200
3.3 @@ -77,7 +77,6 @@
3.4 if (UnparseC.term t) = "True" then ()
3.5 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
3.6
3.7 -
3.8 val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
3.9 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
3.10 if (UnparseC.term t) = "True" then ()
3.11 @@ -112,17 +111,17 @@
3.12 if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
3.13 M_Match.Matches' {Find = [Correct "solutions L"],
3.14 With = [],
3.15 - Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
3.16 - Where = [Correct "matches (?a = 0) (-8 - 2 * x + x \<up> 2 = 0)",
3.17 - Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
3.18 + Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
3.19 + Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
3.20 + Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
3.21 Relate = []}
3.22 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
3.23
3.24 if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
3.25 M_Match.Matches' {Find = [Correct "solutions L"],
3.26 With = [],
3.27 - Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
3.28 - Where = [Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
3.29 + Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
3.30 + Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
3.31 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
3.32 then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
3.33
3.34 @@ -371,10 +370,10 @@
3.35
3.36 (* und nach dem Re-engineering der Termorders in den 'rulesets'
3.37 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
3.38 - val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
3.39 - val x = (Thm.term_of o the o (TermC.parse thy)) "x";
3.40 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
3.41 - val b = (Thm.term_of o the o (TermC.parse thy)) "b";
3.42 + val bdv= TermC.str2term "bdv ::real";
3.43 + val x = TermC.str2term "x ::real";
3.44 + val a = TermC.str2term "a ::real";
3.45 + val b = TermC.str2term "b ::real";
3.46 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
3.47 if UnparseC.term t' = "b + x + a" then ()
3.48 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
3.49 @@ -387,12 +386,8 @@
3.50
3.51 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
3.52 val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
3.53 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
3.54 -if UnparseC.term t' = "- 6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
3.55 -else error "termorder.sml diff.behav ord_make_polynomial_in #14";
3.56 -
3.57 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
3.58 -if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2 + 0" then ()
3.59 +if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
3.60 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
3.61
3.62 val ttt' = "(3*x + 5)/18 ::real";
3.63 @@ -401,12 +396,10 @@
3.64 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
3.65 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
3.66
3.67 -(*============ inhibit exn WN120316 ==============================================
3.68 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
3.69 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
3.70 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
3.71
3.72 -
3.73 "----------- lin.eq degree_0 -------------------------------------";
3.74 "----------- lin.eq degree_0 -------------------------------------";
3.75 "----------- lin.eq degree_0 -------------------------------------";
4.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Mon Aug 02 11:38:40 2021 +0200
4.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Mon Aug 02 15:25:49 2021 +0200
4.3 @@ -888,11 +888,11 @@
4.4 "-------------- ME_Misc.pt_extract form, tac, asm<>[] --------------------";
4.5 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3], Res));
4.6 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
4.7 - ("(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)",
4.8 + ("(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)",
4.9 Subproblem
4.10 ("PolyEq",
4.11 ["normalise", "polynomial", "univariate", "equation"]),
4.12 - ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]) => ()
4.13 + ["x \<noteq> 0", "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]) => ()
4.14 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract asm<>[]";
4.15 (*WN060717 unintentionally changed some rls/ord while
4.16 completing knowl. for thes2file...
5.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Aug 02 11:38:40 2021 +0200
5.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Aug 02 15:25:49 2021 +0200
5.3 @@ -190,7 +190,7 @@
5.4 ML_file "BaseDefinitions/calcelems.sml"
5.5 ML_file "BaseDefinitions/termC.sml"
5.6 ML_file "BaseDefinitions/substitution.sml"
5.7 - ML_file "BaseDefinitions/contextC.sml" (*TOODOO make_ratpoly: "- 6 * x" \<longrightarrow> "- (6 * x)"*)
5.8 + ML_file "BaseDefinitions/contextC.sml"
5.9 ML_file "BaseDefinitions/environment.sml"
5.10 (** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
5.11 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
5.12 @@ -234,7 +234,7 @@
5.13 ML_file "MathEngBasic/thmC.sml"
5.14 ML_file "MathEngBasic/rewrite.sml"
5.15 ML_file "MathEngBasic/tactic.sml"
5.16 -(** )ML_file "MathEngBasic/ctree.sml" ( ** )loops with eliminate ThmC.numerals_to_Free*)
5.17 + ML_file "MathEngBasic/ctree.sml"
5.18 ML_file "MathEngBasic/calculation.sml"
5.19
5.20 ML_file "Specify/formalise.sml"
5.21 @@ -272,8 +272,7 @@
5.22 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
5.23 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
5.24 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009- 2*)
5.25 -(** )ML_file "BridgeLibisabelle/interface.sml"( *loops with eliminate ThmC.numerals_to_Free
5.26 - but is deprecated after ^^^^^^^^^^^^^^^( **)
5.27 + ML_file "BridgeLibisabelle/interface.sml"
5.28 ML_file "BridgeJEdit/parseC.sml"
5.29 ML_file "BridgeJEdit/preliminary.sml"
5.30
5.31 @@ -287,15 +286,15 @@
5.32 ML_file "Knowledge/rational-1.sml"
5.33 (*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*)
5.34 ML_file "Knowledge/equation.sml"
5.35 -(*ML_file "Knowledge/root.sml" see TOODOO.1*)
5.36 +(*ML_file "Knowledge/root.sml" see TOODOO.1*)
5.37 ML_file "Knowledge/lineq.sml"
5.38
5.39 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
5.40 (*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*)
5.41 -(*ML_file "Knowledge/rootrat.sml" error inherited from root.sml*)
5.42 +(*ML_file "Knowledge/rootrat.sml" TOODOO.1 error inherited from root.sml*)
5.43 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
5.44 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
5.45 -(*ML_file "Knowledge/polyeq-1.sml" error inherited from root.sml | in Test_Some.thy*)
5.46 +(*ML_file "Knowledge/polyeq-1.sml" TOODOO.1 error inherited from root.sml*)
5.47 (*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*)
5.48 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
5.49 ML_file "Knowledge/calculus.sml"
6.1 --- a/test/Tools/isac/Test_Some.thy Mon Aug 02 11:38:40 2021 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Mon Aug 02 15:25:49 2021 +0200
6.3 @@ -203,9 +203,9 @@
6.4 if (UnparseC.term t) = "True" then ()
6.5 else error "polyeq.sml: diff.behav. in has_degree_in_in";
6.6
6.7 -\<close> text \<open> (*TOODOO broken with repair ord_make_polynomial_in*)
6.8 +\<close> ML \<open> (*TOODOO broken with repair ord_make_polynomial_in*)
6.9 val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
6.10 - val SOME (t,_) = rewrite_set_ @ {theory PolyEq} false PolyEq_prls t3;
6.11 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
6.12 if (UnparseC.term t) = "False" then ()
6.13 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
6.14
6.15 @@ -222,7 +222,7 @@
6.16 if (UnparseC.term t) = "True" then ()
6.17 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
6.18
6.19 -\<close> text \<open> (* M_Match.match_pbl [expanded,univariate,equation] *)
6.20 +\<close> ML \<open> (* M_Match.match_pbl [expanded,univariate,equation] *)
6.21 "----------- test matching problems --------------------------0---";
6.22 "----------- test matching problems --------------------------0---";
6.23 "----------- test matching problems --------------------------0---";
6.24 @@ -230,21 +230,22 @@
6.25 if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
6.26 M_Match.Matches' {Find = [Correct "solutions L"],
6.27 With = [],
6.28 - Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
6.29 - Where = [Correct "matches (?a = 0) (-8 - 2 * x + x \<up> 2 = 0)",
6.30 - Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
6.31 + Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
6.32 + Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
6.33 + Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
6.34 Relate = []}
6.35 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
6.36
6.37 +\<close> ML \<open>
6.38 if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
6.39 M_Match.Matches' {Find = [Correct "solutions L"],
6.40 With = [],
6.41 - Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
6.42 - Where = [Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
6.43 + Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
6.44 + Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
6.45 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
6.46 then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
6.47
6.48 -
6.49 +\<close> ML \<open>
6.50 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
6.51 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
6.52 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
6.53 @@ -513,55 +514,7 @@
6.54 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
6.55 val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
6.56 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
6.57 -\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
6.58 -\<close> ML \<open>
6.59 -[(bdv,x)]
6.60 -\<close> ML \<open>
6.61 - val ppp = TermC.str2term "-6 + -5*x ::real";
6.62 - val ppp = TermC.str2term "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
6.63 -\<close> ML \<open>
6.64 -Rewrite.trace_on := true; (*false true*)
6.65 -\<close> ML \<open>
6.66 -Rewrite.trace_on;
6.67 -\<close> ML \<open>
6.68 -val SOME (t', _) = rewrite_set_inst_ thy false [(bdv, x)] make_polynomial_in ppp;
6.69 -\<close> ML \<open>
6.70 -Rewrite.trace_on := true; (*false true*)
6.71 -\<close> ML \<open>
6.72 -UnparseC.term t' = "- 6 + - (5 * x)"
6.73 -\<close> ML \<open>
6.74 -@{thm minus_mult_left}
6.75 -\<close> ML \<open>
6.76 -\<close> ML \<open>
6.77 -\<close> ML \<open>
6.78 -\<close> ML \<open>
6.79 -\<close> ML \<open>
6.80 -\<close> ML \<open>
6.81 -(*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*)
6.82 -fun eval_is_num (thmid:string) "Prog_Expr.is_num" (t as (Const _ $ arg)) _ =
6.83 - if TermC.is_num arg
6.84 - then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
6.85 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
6.86 - else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
6.87 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
6.88 - | eval_is_num _ _ _ _ = NONE;
6.89 -\<close> ML \<open>
6.90 -\<close> ML \<open>
6.91 -val t = TermC.str2term "(5::real) is_num";
6.92 -\<close> ML \<open>
6.93 -eval_is_num "aaa" "Prog_Expr.is_num" t "" (*GOON> must be SOME \<And>\<And>\<And>\<And>\<And>*)
6.94 -\<close> ML \<open>
6.95 -\<close> ML \<open>
6.96 -\<close> ML \<open>
6.97 -\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
6.98 -\<close> ML \<open>
6.99 -UnparseC.term t'
6.100 -\<close> text \<open> (*TOODOO broken with repair ord_make_polynomial_in*)
6.101 -if UnparseC.term t' = "- 6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
6.102 -else error "termorder.sml diff.behav ord_make_polynomial_in #14";
6.103 -
6.104 -val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
6.105 -if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2 + 0" then ()
6.106 +if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
6.107 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
6.108
6.109 \<close> ML \<open>
6.110 @@ -676,7 +629,7 @@
6.111 "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
6.112 else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
6.113
6.114 -\<close> text \<open> (*TOODOO rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 1 * (- 1 / 2) + sqrt ((- 1) \<up> 2 + 8) / 2 \<or>
6.115 +\<close> text \<open> (*see TOODOO.1 broken with merge after "eliminate ThmC.numerals_to_Free"
6.116 x = - 1 * (- 1 / 2) + - 1 * (sqrt ((- 1) \<up> 2 + 8) / 2) = NONE*)
6.117 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
6.118 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
6.119 @@ -699,7 +652,7 @@
6.120 | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
6.121
6.122
6.123 -\<close> text \<open> (*see TOODOO.1
6.124 +\<close> text \<open> (*see TOODOO.1 broken with merge after "eliminate ThmC.numerals_to_Free"
6.125 exception TYPE raised (line 169 of "consts.ML"): Illegal type for constant "HOL.eq" :: real
6.126 \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool*)
6.127 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
6.128 @@ -761,10 +714,11 @@
6.129 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.130 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.131 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.132 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.133 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
6.134 | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
6.135
6.136 -\<close> text \<open> (* loops*)
6.137 +\<close> text \<open> (* FormKF "[]" instead of "[x = 0, x = - 1]"*)
6.138 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
6.139 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
6.140 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
6.141 @@ -784,7 +738,7 @@
6.142 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.143 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
6.144
6.145 -\<close> text \<open> (* loops*)
6.146 +\<close> text \<open> (* TOODOO.1 *)
6.147 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
6.148 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
6.149 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
6.150 @@ -804,7 +758,7 @@
6.151 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.152 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
6.153
6.154 -\<close> text \<open> (* loops*)
6.155 +\<close> text \<open> (* TOODOO.1*)
6.156 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
6.157 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
6.158 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
6.159 @@ -825,7 +779,7 @@
6.160 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.161 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
6.162
6.163 -\<close> text \<open> (* loops*)
6.164 +\<close> text \<open> (* TOODOO.1*)
6.165 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
6.166 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
6.167 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
6.168 @@ -845,7 +799,7 @@
6.169 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.170 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
6.171
6.172 -\<close> text \<open> (*see TOODOO.1*)
6.173 +\<close> text \<open> (* TOODOO.1*)
6.174 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
6.175 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
6.176 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
6.177 @@ -1105,7 +1059,7 @@
6.178 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.179 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
6.180
6.181 -\<close> text \<open> (* loops*)
6.182 +\<close> text \<open> (* TOODOO.1*)
6.183 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.184 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.185 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
6.186 @@ -1120,7 +1074,7 @@
6.187 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
6.188 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
6.189
6.190 -\<close> text \<open> (* loops*)
6.191 +\<close> text \<open> (* TOODOO.1 *)
6.192 (*EP- 16*)
6.193 val fmz = ["equality (x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.194 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.195 @@ -1136,7 +1090,7 @@
6.196 case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
6.197 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
6.198
6.199 -\<close> text \<open> (* loops*)
6.200 +\<close> ML \<open> (* loops*)
6.201 (*EP-//*)
6.202 val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
6.203 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
6.204 @@ -1153,7 +1107,7 @@
6.205 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
6.206
6.207
6.208 -\<close> text \<open> (* loops*)
6.209 +\<close> text \<open> (* TOODOO.1 *)
6.210 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
6.211 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
6.212 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
6.213 @@ -1211,7 +1165,7 @@
6.214 then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
6.215
6.216
6.217 -\<close> text \<open> (* loops*)
6.218 +\<close> text \<open> (* TOODOO.1 *)
6.219 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
6.220 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
6.221 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
6.222 @@ -1268,7 +1222,7 @@
6.223 val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
6.224 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
6.225 val t' = UnparseC.term t;
6.226 - (*if t'= "HOL.True" then ()
6.227 + (*if t'= \<^const_name>\<open>True\<close> then ()
6.228 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
6.229 (* *)
6.230 val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
6.231 @@ -1287,11 +1241,7 @@
6.232 (*Apply_Method ("PolyEq", "complete_square")*)
6.233 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
6.234
6.235 -\<close> text \<open> (* loops*)
6.236 -\<close> text \<open> (*f = Test_Out.FormKF "[]" *)
6.237 -\<close> text \<open> (*see TOODOO.1*)
6.238 -\<close> ML \<open>
6.239 -\<close> text \<open> (* loops*)
6.240 +\<close> text \<open> (* TOODOO.1 broken with merge after "eliminate ThmC.numerals_to_Free" *)
6.241 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
6.242 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
6.243 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
6.244 @@ -1514,7 +1464,7 @@
6.245 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
6.246 ( * inhertited errors -----------------------------------------------------------------------//*)
6.247
6.248 -\<close> text \<open> (*TOODOO broken with merge after "eliminate ThmC.numerals_to_Free" *)
6.249 +\<close> text \<open> (*TOODOO.1 broken with merge after "eliminate ThmC.numerals_to_Free" *)
6.250 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
6.251 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
6.252 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";