# HG changeset patch # User wneuper # Date 1629721446 -7200 # Node ID 070aa3b448d63ebe815a1926c751bfffd6aa655b # Parent e9a69b881f22658fe5e41c21cf1d595b5a52533d repair rule-set reduce_0_1_2 diff -r e9a69b881f22 -r 070aa3b448d6 src/Tools/isac/Knowledge/Rational.thy --- a/src/Tools/isac/Knowledge/Rational.thy Mon Aug 23 12:33:10 2021 +0200 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Aug 23 14:24:06 2021 +0200 @@ -650,7 +650,7 @@ Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], rules = [ - (*\<^rule_thm>\divide_1\, "?x / 1 = ?x" unnecessary.for normalform*) + \<^rule_thm>\div_by_1\, (*"?x / 1 = ?x"*) \<^rule_thm>\mult_1_left\, (*"1 * z = z"*) \<^rule_thm>\minus_zero\, (*"- 0 = 0"*) (*\<^rule_thm>\real_mult_minus1\, "-1 * z = - z"*) @@ -711,7 +711,7 @@ erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], rules = [ - Rule.Rls_ norm_Rational_min, + Rule.Rls_ norm_Rational_min, Rule.Rls_ discard_parentheses], scr = Rule.Empty_Prog}); diff -r e9a69b881f22 -r 070aa3b448d6 test/Tools/isac/Knowledge/polyeq-1.sml --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Aug 23 12:33:10 2021 +0200 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Mon Aug 23 14:24:06 2021 +0200 @@ -2,14 +2,14 @@ testexamples for PolyEq, poynomial equations and equational systems Author: Richard Lang 2003 (c) due to copyright terms -WN030609: some expls dont work due to unfinished handling of 'expanded terms'; - others marked with TODO have to be checked, too. + +Separation into polyeq-1.sml and polyeq-1a.sml due to *) "-----------------------------------------------------------------"; "table of contents -----------------------------------------------"; "-----------------------------------------------------------------"; -"------ polyeq- 1.sml ---------------------------------------------"; +"------ polyeq-1.sml ---------------------------------------------"; "----------- tests on predicates in problems ---------------------"; "----------- test matching problems ------------------------------"; "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; @@ -22,6 +22,7 @@ "----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; "----------- equality (2 + x + x \ 2 = 0) ----------------------------------------------------"; "----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; +"------ polyeq- 2.sml ---------------------------------------------"; "----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; "----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; "----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; @@ -50,6 +51,7 @@ "----------- tests on predicates in problems ---------------------"; "----------- tests on predicates in problems ---------------------"; "----------- tests on predicates in problems ---------------------"; +val thy = @{theory}; Rewrite.trace_on:=false; (*true false*) val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \ 2 = 0)"; @@ -323,16 +325,16 @@ (** )end;( *local*) val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; -if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?"; +if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then () else error "still GREATER?"; val x = TermC.str2term "x ::real"; val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \ 2 / 4 ::real"); -if 2006 = size_of_term' 1 true x t1 +if 2006 = size_of_term' 1 false(*true*) x t1 then () else error "size_of_term' (L * q_0 * x \ 2) CHANGED)"; val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \ 3) :: real"); -if 3004 = size_of_term' 1 true x t2 +if 3004 = size_of_term' 1 false(*true*) x t2 then () else error "size_of_term' (- 1 * (q_0 * x \ 3)) CHANGED"; @@ -348,23 +350,23 @@ val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b"; val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b"; -if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then () +if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then () else error "termorder.sml diff.behav ord_make_polynomial_in #1"; -if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then () +if ord_make_polynomial_in false(*true*) thy substa (x1,x2) = true(*LESS *) then () else error "termorder.sml diff.behav ord_make_polynomial_in #2"; -if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then () +if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then () else error "termorder.sml diff.behav ord_make_polynomial_in #3"; val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; val bb = (Thm.term_of o the o (TermC.parse thy)) "x \ 3"; - ord_make_polynomial_in true thy substx (aa, bb); + ord_make_polynomial_in false(*true*) thy substx (aa, bb); true; (* => LESS *) val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; val bb = (Thm.term_of o the o (TermC.parse thy)) "x \ 3"; - ord_make_polynomial_in true thy substa (aa, bb); + ord_make_polynomial_in false(*true*) thy substa (aa, bb); false; (* => GREATER *) (* und nach dem Re-engineering der Termorders in den 'rulesets' @@ -909,7 +911,7 @@ | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; (*EP- 16*) -val fmz = ["equality (x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; +val fmz = ["equality (x + 2 * x \ 2 = (0::real))", "solveFor (x::real)", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -917,7 +919,12 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +(*+*)val Test_Out.FormKF "x + 2 * x \ 2 = 0" = f; +(*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt + +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \ 2 = 0", d2_polyeq_abcFormula_simplify*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => () @@ -991,7 +998,7 @@ | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]"; *) if f2str f = -"[x = - 1 * - 1 + - 1 * sqrt (2 \ 2 / 2 \ 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - -8))]" + "[x = - 1 * - 1 + - 1 * sqrt (2 \ 2 / 2 \ 2 - - 8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - - 8))]" (*"[x = - 1 * - 1 + - 1 * sqrt (1 \ 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \ 2 - -8))]"*) then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]"; @@ -999,7 +1006,7 @@ "----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; "----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; "----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat +(*stopped due to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat see --- val rls = calculate_RootRat > calculate_Rational ---*) val thy = @{theory PolyEq}; val ctxt = Proof_Context.init_global thy; @@ -1008,37 +1015,43 @@ val rls = complete_square; val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t; -UnparseC.term t = "-8 + (2 / 2 - x) \ 2 = (2 / 2) \ 2"; +if UnparseC.term t = "- 8 + (2 / 2 - x) \ 2 = (2 / 2) \ 2" +then () else error "rls complete_square CHANGED"; -val thm = ThmC.numerals_to_Free @{thm square_explicit1}; +val thm = @{thm square_explicit1}; val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t; -UnparseC.term t = "(2 / 2 - x) \ 2 = (2 / 2) \ 2 - -8"; +if UnparseC.term t = "(2 / 2 - x) \ 2 = (2 / 2) \ 2 - - 8" +then () else error "thm square_explicit1 CHANGED"; -val thm = ThmC.numerals_to_Free @{thm root_plus_minus}; +val thm = @{thm root_plus_minus}; val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t; -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \ 2 - -8) |"^ - "\n2 / 2 - x = - 1 * sqrt ((2 / 2) \ 2 - -8)"; +if UnparseC.term t = +"2 / 2 - x = sqrt ((2 / 2) \ 2 - - 8) \\n2 / 2 - x = - 1 * sqrt ((2 / 2) \ 2 - - 8)" +then () else error "thm root_plus_minus CHANGED"; (*the thm bdv_explicit2* here required to be constrained to ::real*) -val thm = ThmC.numerals_to_Free @{thm bdv_explicit2}; +val thm = @{thm bdv_explicit2}; val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \ 2 - -8) |"^ - "\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - -8)"; +if UnparseC.term t = +"2 / 2 - x = sqrt ((2 / 2) \ 2 - - 8) \\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - - 8)" +then () else error "thm bdv_explicit2 CHANGED"; -val thm = ThmC.numerals_to_Free @{thm bdv_explicit3}; +val thm = @{thm bdv_explicit3}; val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \ 2 - -8) |"^ - "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - -8))"; +if UnparseC.term t = +"2 / 2 - x = sqrt ((2 / 2) \ 2 - - 8) \\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - - 8))" +then () else error "thm bdv_explicit3 CHANGED"; -val thm = ThmC.numerals_to_Free @{thm bdv_explicit2}; +val thm = @{thm bdv_explicit2}; val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; -UnparseC.term t = "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - -8) |"^ - "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - -8))"; +if UnparseC.term t = +"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - - 8) \\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - - 8))" +then () else error "thm bdv_explicit2 CHANGED"; val rls = calculate_RootRat; val SOME (t,asm) = rewrite_set_ thy true rls t; if UnparseC.term t = - "- 1 * x = - 1 + sqrt (2 \ 2 / 2 \ 2 - -8) \\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - -8))" + "- 1 * x = - 1 + sqrt (2 \ 2 / 2 \ 2 - - 8) \\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - - 8))" (*"- 1 * x = - 1 + sqrt (2 \ 2 / 2 \ 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - -8))"..isabisac15*) then () else error "(-8 - 2*x + x \ 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT"; (*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*) diff -r e9a69b881f22 -r 070aa3b448d6 test/Tools/isac/Knowledge/polyeq-2.sml --- a/test/Tools/isac/Knowledge/polyeq-2.sml Mon Aug 23 12:33:10 2021 +0200 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Mon Aug 23 14:24:06 2021 +0200 @@ -107,7 +107,7 @@ case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => () | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]"; *) -if f2str f = "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]" then () +if f2str f = "[x = sqrt (0 - - 49), x = - 1 * sqrt (0 - - 49)]" then () else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]"; @@ -212,6 +212,7 @@ "----------- rls make_polynomial_in ------------------------------"; "----------- rls make_polynomial_in ------------------------------"; "----------- rls make_polynomial_in ------------------------------"; +val thy = @{theory}; (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*) (*WN.19.3.03 ---v-*) (*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1"); @@ -283,18 +284,18 @@ (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*) t |> UnparseC.term; t |> TermC.atomty; -val thm = ThmC.numerals_to_Free @{thm d2_prescind1}; +val thm = @{thm d2_prescind1}; thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty; val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t'; (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) --> x = 0 | -6 + 5 * x = 0*) t' |> UnparseC.term; t' |> TermC.atomty; -val thm = ThmC.numerals_to_Free @{thm d2_reduce_equation1}; +val thm = @{thm d2_reduce_equation1}; thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty; val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t''; (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))" *) -if UnparseC.term t'' = "x = 0 \ -6 + 5 * x = 0" then () +if UnparseC.term t'' = "x = 0 \ - 6 + 5 * x = 0" then () else error "rls d2_polyeq_bdv_only_simplify broken"; diff -r e9a69b881f22 -r 070aa3b448d6 test/Tools/isac/ProgLang/evaluate.sml --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Aug 23 12:33:10 2021 +0200 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon Aug 23 14:24:06 2021 +0200 @@ -484,18 +484,11 @@ (*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2" *) +val NONE = adhoc_thm @{theory} eval_ t; +"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t); val NONE = - adhoc_thm @{theory} eval_ t; -"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t); -val SOME ("#divide_e~1_2", t') = (*case*) get_pair thy op_ eval_fn t (*of*); -(*+*)UnparseC.term t = "- 1 / 2"; -(*+*)UnparseC.term t' = "- 1 / 2 = - 1 / 2"; "HOL.Trueprop"; - -if t = (TermC.rhs o HOLogic.dest_Trueprop) t' -then () else error "fun adhoc_thm + fun eval_cancel CHANGED"; - "----------- fun adhoc_thm \ exception TYPE --------------------------------------------------"; "----------- fun adhoc_thm \ exception TYPE --------------------------------------------------"; diff -r e9a69b881f22 -r 070aa3b448d6 test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Mon Aug 23 12:33:10 2021 +0200 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Aug 23 14:24:06 2021 +0200 @@ -293,8 +293,8 @@ ML_file "Knowledge/rootrat.sml" ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*) -(*ML_file "Knowledge/polyeq-1.sml" TOODOO.1 error inherited from root.sml*) -(*ML_file "Knowledge/polyeq-2.sml" TOODOO.1 Test_Isac_Short*) + ML_file "Knowledge/polyeq-1.sml" +(*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*) (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *) ML_file "Knowledge/calculus.sml" ML_file "Knowledge/trig.sml" diff -r e9a69b881f22 -r 070aa3b448d6 test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Mon Aug 23 12:33:10 2021 +0200 +++ b/test/Tools/isac/Test_Some.thy Mon Aug 23 14:24:06 2021 +0200 @@ -107,19 +107,7 @@ section \===================================================================================\ ML \ \ ML \ -\ ML \ -\ ML \ -\ - -ML \ -val thy = @{theory}; Rewrite.trace_on := false; (**) -\ -(* ML_file "Knowledge/polyeq-1.sml" TOODOO.1 error inherited from root.sml*) -section \======== check test/../polyeq-1.sml ===============================================\ -ML \ -val thy = @{theory}; -\ ML \ -(* Title: Knowledge/polyeq-1.sml +(* Title: Knowledge/polyeq- 1.sml testexamples for PolyEq, poynomial equations and equational systems Author: Richard Lang 2003 (c) due to copyright terms @@ -130,33 +118,6 @@ "-----------------------------------------------------------------"; "table of contents -----------------------------------------------"; "-----------------------------------------------------------------"; -"------ polyeq- 1.sml ---------------------------------------------"; -"----------- tests on predicates in problems ---------------------"; -"----------- test matching problems ------------------------------"; -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; -"----------- open local of fun ord_make_polynomial_in ------------------------------------------"; -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; -"----------- lin.eq degree_0 -------------------------------------"; -"----------- test thm's d2_pq_formulsxx[_neg]---------------------"; -"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; -"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; -"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; -"----------- equality (2 + x + x \ 2 = 0) ----------------------------------------------------"; -"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; -"----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; -"----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; -"----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; -"----------- equality (x + 1*x \ 2 = 0) ------------------------------------------------------"; -"----------- equality (-4 + x \ 2 = 0) -------------------------------------------------------"; -"----------- equality (4 + 1*x \ 2 = 0) -------------------------------------------------------"; -"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; -"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; -"----------- equality (1 + x + 2*x \ 2 = 0) --------------------------------------------------"; -"----------- (-8 - 2*x + x \ 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; -"----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; -"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; -"-----------------------------------------------------------------"; -"------ polyeq- 2.sml ---------------------------------------------"; "----------- (a*b - (a+b)*x + x \ 2 = 0), (*Schalk 2,S.68Nr.44.a*)"; "----------- (-64 + x \ 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; "----------- (- 147 + 3*x \ 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; @@ -168,1529 +129,292 @@ "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; -"----------- tests on predicates in problems ---------------------"; -"----------- tests on predicates in problems ---------------------"; -"----------- tests on predicates in problems ---------------------"; -val thy = @{theory}; -Rewrite.trace_on:=false; (*true false*) - val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \ 2 = 0)"; - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1; - if ((UnparseC.term t) = "- 8 - 2 * x + x \ 2") then () - else error "polyeq.sml: diff.behav. in lhs"; - - val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \ 2) is_expanded_in x"; - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2; - if (UnparseC.term t) = "True" then () - else error "polyeq.sml: diff.behav. 1 in is_expended_in"; - - val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x"; - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0; - if (UnparseC.term t) = "False" then () - else error "polyeq.sml: diff.behav. 2 in is_poly_in"; - - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \ 2) is_poly_in x"; - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; - if (UnparseC.term t) = "True" then () - else error "polyeq.sml: diff.behav. 3 in is_poly_in"; - - val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \ 2 = 0)) is_expanded_in x"; - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; - if (UnparseC.term t) = "True" then () - else error "polyeq.sml: diff.behav. 4 in is_expended_in"; - - val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \ 2 = 0)) is_expanded_in x"; - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6; - if (UnparseC.term t) = "True" then () - else error "polyeq.sml: diff.behav. 5 in is_expended_in"; - - val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \ 2) has_degree_in x) = 2"; - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; - if (UnparseC.term t) = "True" then () - else error "polyeq.sml: diff.behav. in has_degree_in_in"; - - val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2"; - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; - if (UnparseC.term t) = "False" then () - else error "polyeq.sml: diff.behav. 6 in has_degree_in_in"; - - val t4 = (Thm.term_of o the o (TermC.parse thy)) - "((-8 - 2*x + x \ 2) has_degree_in x) = 1"; - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; - if (UnparseC.term t) = "False" then () - else error "polyeq.sml: diff.behav. 7 in has_degree_in_in"; - -val t5 = (Thm.term_of o the o (TermC.parse thy)) - "((-8 - 2*x + x \ 2) has_degree_in x) = 2"; - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5; - if (UnparseC.term t) = "True" then () - else error "polyeq.sml: diff.behav. 8 in has_degree_in_in"; - -\ ML \ -"----------- test matching problems --------------------------0---"; -"----------- test matching problems --------------------------0---"; -"----------- test matching problems --------------------------0---"; -val fmz = ["equality (-8 - 2*x + x \ 2 = 0)", "solveFor x", "solutions L"]; -if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) = - M_Match.Matches' {Find = [Correct "solutions L"], - With = [], - Given = [Correct "equality (- 8 - 2 * x + x \ 2 = 0)", Correct "solveFor x"], - Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \ 2 = 0)", - Correct "lhs (- 8 - 2 * x + x \ 2 = 0) is_expanded_in x"], - Relate = []} -then () else error "M_Match.match_pbl [expanded,univariate,equation]"; - -if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) = - M_Match.Matches' {Find = [Correct "solutions L"], - With = [], - Given = [Correct "equality (- 8 - 2 * x + x \ 2 = 0)", Correct "solveFor x"], - Where = [Correct "lhs (- 8 - 2 * x + x \ 2 = 0) has_degree_in x = 2"], - Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*) -then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]"; - - -\ ML \ -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; -"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; -(*################################################################################## ------------ 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy - - (*Aufgabe zum Einstieg in die Arbeit...*) - val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \ 2 = 0"; - (*ein 'ruleset' aus Poly.ML wird angewandt...*) - val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t; - UnparseC.term t; - "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \ 2)) = 0"; - val SOME (t,_) = - rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t; - UnparseC.term t; - "x \ 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0"; -(* bei Verwendung von "size_of-term" nach MG :*) -(*"x \ 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *) - - (*wir holen 'a' wieder aus der Klammerung heraus...*) - val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t; - UnparseC.term t; - "x \ 2 + - 1 * b * x + - 1 * x * a + b * a = 0"; -(* "x \ 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *) - - val SOME (t,_) = - rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t; - UnparseC.term t; - "x \ 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0"; - (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben - "x \ 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*) - - (*das rewriting l"asst sich beobachten mit -Rewrite.trace_on := false; (*true false*) - *) - -"------ 15.11.02 --------------------------"; - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x"; - val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv"; - val a = (Thm.term_of o the o (TermC.parse thy)) "a"; - -Rewrite.trace_on := false; (*true false*) - (* Anwenden einer Regelmenge aus Termorder.ML: *) - val SOME (t,_) = - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; - UnparseC.term t; - val SOME (t,_) = - rewrite_set_ thy false discard_parentheses t; - UnparseC.term t; -"1 + b * x + x * a"; - - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \ 2"; - val SOME (t,_) = - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; - UnparseC.term t; - val SOME (t,_) = - rewrite_set_ thy false discard_parentheses t; - UnparseC.term t; -"1 + (x + b * x) * a + a \ 2"; - - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \ 2 * x + b * a + 7*a \ 2"; - val SOME (t,_) = - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; - UnparseC.term t; - val SOME (t,_) = - rewrite_set_ thy false discard_parentheses t; - UnparseC.term t; -"1 + b * a + (7 + x) * a \ 2"; - -(* MG2003 - Prog_Expr.thy grundlegende Algebra - Poly.thy Polynome - Rational.thy Br"uche - Root.thy Wurzeln - RootRat.thy Wurzen + Br"uche - Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03) - - get_thm Termorder.thy "bdv_n_collect"; - get_thm (theory "Isac_Knowledge") "bdv_n_collect"; -*) - val t = (Thm.term_of o the o (TermC.parse thy)) "a \ 2 * x + 7 * a \ 2"; - val SOME (t,_) = - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; - UnparseC.term t; - val SOME (t,_) = - rewrite_set_ thy false discard_parentheses t; - UnparseC.term t; -"(7 + x) * a \ 2"; - - val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi"; - - val t = (Thm.term_of o the o (parseold thy)) "7"; -##################################################################################*) - - -\ ML \ -"----------- open local of fun ord_make_polynomial_in ------------------------------------------"; -"----------- open local of fun ord_make_polynomial_in ------------------------------------------"; -"----------- open local of fun ord_make_polynomial_in ------------------------------------------"; -(* termorder hacked by MG, adapted later by WN *) -(** )local ( *. for make_polynomial_in .*) - -open Term; (* for type order = EQUAL | LESS | GREATER *) - -fun pr_ord EQUAL = "EQUAL" - | pr_ord LESS = "LESS" - | pr_ord GREATER = "GREATER"; - -fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0) - | dest_hd' x (t as Free (a, T)) = - if x = t then ((("|||||||||||||", 0), T), 0) (*WN*) - else (((a, 0), T), 1) - | dest_hd' _ (Var v) = (v, 2) - | dest_hd' _ (Bound i) = ((("", i), dummyT), 3) - | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4) - | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def."; - -fun size_of_term' i pr x (t as Const (\<^const_name>\powr\, _) $ - Free (var, _) $ Free (pot, _)) = - (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else (); - case x of (*WN*) - (Free (xstr, _)) => - if xstr = var - then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else (); - 1000 * (the (TermC.int_opt_of_string pot))) - else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3) - | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x)) - | size_of_term' i pr x (t as Abs (_, _, body)) = - (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else (); - 1 + size_of_term' (i + 1) pr x body) - | size_of_term' i pr x (f $ t) = - let - val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else (); - val s1 = size_of_term' (i + 1) pr x f - val s2 = size_of_term' (i + 1) pr x t - val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else (); - in (s1 + s2) end - | size_of_term' i pr x t = - (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else (); - case t of - Free (subst, _) => - (case x of - Free (xstr, _) => - if xstr = subst - then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000) - else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1) - | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x)) - | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1)); - -fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) - let - val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else (); - val ord = - case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord - val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else () - in ord end - | term_ord' i pr x _ (t, u) = - let - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else (); - val ord = - case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of - EQUAL => - let val (f, ts) = strip_comb t and (g, us) = strip_comb u - in - (case hd_ord (i + 1) pr x (f, g) of - EQUAL => (terms_ord x (i + 1) pr) (ts, us) - | ord => ord) - end - | ord => ord - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else () - in ord end -and hd_ord i pr x (f, g) = (* ~ term.ML *) - let - val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else (); - val ord = prod_ord - (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord - (dest_hd' x f, dest_hd' x g) - val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else (); - in ord end -and terms_ord x i pr (ts, us) = - let - val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else (); - val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us); - val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else (); - in ord end - -(** )in( *local*) - -fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) = - ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **) - case subst of - (_, x) :: _ => - term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS - | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst)) - -(** )end;( *local*) - -val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; -if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?"; - -val x = TermC.str2term "x ::real"; - -val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \ 2 / 4 ::real"); -if 2006 = size_of_term' 1 true x t1 -then () else error "size_of_term' (L * q_0 * x \ 2) CHANGED)"; - -val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \ 3) :: real"); -if 3004 = size_of_term' 1 true x t2 -then () else error "size_of_term' (- 1 * (q_0 * x \ 3)) CHANGED"; - - -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; -"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; - val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")]; - val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")]; - val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")]; - - val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x"; - val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b"; - val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b"; - val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b"; - -if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then () -else error "termorder.sml diff.behav ord_make_polynomial_in #1"; - -if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then () -else error "termorder.sml diff.behav ord_make_polynomial_in #2"; - -if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then () -else error "termorder.sml diff.behav ord_make_polynomial_in #3"; - - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \ 3"; - ord_make_polynomial_in true thy substx (aa, bb); - true; (* => LESS *) - - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \ 3"; - ord_make_polynomial_in true thy substa (aa, bb); - false; (* => GREATER *) - -(* und nach dem Re-engineering der Termorders in den 'rulesets' - kannst Du die 'gr"osste' Variable frei w"ahlen: *) - val bdv= TermC.str2term "bdv ::real"; - val x = TermC.str2term "x ::real"; - val a = TermC.str2term "a ::real"; - val b = TermC.str2term "b ::real"; -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2; -if UnparseC.term t' = "b + x + a" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #11"; - -val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2; - -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2; -if UnparseC.term t' = "a + b + x" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #13"; - - val ppp' = "-6 + -5*x + x \ 3 + - 1*x \ 2 + - 1*x \ 3 + - 14*x \ 2"; - val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp'; -val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; -if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \ 2" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #15"; - - val ttt' = "(3*x + 5)/18 ::real"; - val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt'; -val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; -if UnparseC.term uuu = "(5 + 3 * x) / 18" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #16a"; - -val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt; -if UnparseC.term uuu = "(5 + 3 * x) / 18" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #16b"; - -"----------- lin.eq degree_0 -------------------------------------"; -"----------- lin.eq degree_0 -------------------------------------"; -"----------- lin.eq degree_0 -------------------------------------"; -"----- d0_false ------"; -val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d0_polyeq_equation"]); -(*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ======== -TODO: change to "equality (x + - 1*x = (0::real))" - and search for an appropriate problem and method. - -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => () - | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []"; - -"----- d0_true ------"; -val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d0_polyeq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => () - | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList"; -============ inhibit exn WN110914 ============================================*) - -\ text \ (*rewrite_set_, rewrite_ ..= NONE*) -"----------- test thm's d2_pq_formulsxx[_neg]---------------------"; -"----------- test thm's d2_pq_formulsxx[_neg]---------------------"; -"----------- test thm's d2_pq_formulsxx[_neg]---------------------"; -"----- d2_pqformula1 ------!!!!"; -val fmz = ["equality (- 1/8 + (- 1/4)*z + z \ 2 = (0::real))", "solveFor z", "solutions L"]; -val (dI',pI',mI') = - ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*) -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; - -(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*) -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*) -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; - -if p = ([], Res) andalso - f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then - case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \ 2 = (0::real)) CHANGED 1" -else error "(- 1/8 + (- 1/4)*z + z \ 2 = (0::real)) CHANGED 2"; - -\ ML \ -"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; -"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; -"----------- equality (2 +(- 1)*x + x \ 2 = (0::real)) ----------------------------------------"; -"----- d2_pqformula1_neg ------"; -val fmz = ["equality (2 +(- 1)*x + x \ 2 = (0::real))", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*### or2list False - ([1],Res) False Or_to_List)*) -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*### or2list False - ([2],Res) [] Check_elementwise "Assumptions"*) -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val asm = Ctree.get_assumptions pt p; -if f2str f = "[]" andalso - UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \ 2 = 0) is_poly_in x\", " ^ - "\"lhs (2 + - 1 * x + x \ 2 = 0) has_degree_in x = 2\"]" then () -else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \ 2 = 0"; - -\ text \ (*rewrite_set_, rewrite_ ..= NONE*) -"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; -"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; -"----------- equality (- 2 +(- 1)*x + 1*x \ 2 = 0) ---------------------------------------------"; -"----- d2_pqformula2 ------"; -val fmz = ["equality (- 2 +(- 1)*x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_pq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; - -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 2, x = - 1]" => () - | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]"; - - -\ text \ (*rewrite_set_, rewrite_ ..= NONE*) -"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; -"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; -"----------- equality (- 2 + x + x \ 2 = 0) ---------------------------------------------------"; -"----- d2_pqformula3 ------"; -(*EP-9*) -val fmz = ["equality (- 2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_pq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; - -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1, x = - 2]" => () - | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]"; - - -\ ML \ -"----------- equality (2 + x + x \ 2 = 0) ----------------------------------------------------"; -"----------- equality (2 + x + x \ 2 = 0) ----------------------------------------------------"; -"----------- equality (2 + x + x \ 2 = 0) ----------------------------------------------------"; -"----- d2_pqformula3_neg ------"; -val fmz = ["equality (2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_pq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; - -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -"TODO 2 + x + x \ 2 = 0"; -"TODO 2 + x + x \ 2 = 0"; -"TODO 2 + x + x \ 2 = 0"; - -\ text \ (*rewrite_set_, rewrite_ ..= NONE*) -"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; -"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; -"----------- equality (- 2 + x + 1*x \ 2 = 0)) ------------------------------------------------"; -"----- d2_pqformula4 ------"; -val fmz = ["equality (- 2 + x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_pq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1, x = - 2]" => () - | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \ 2 = 0 -> [x = 1, x = - 2]"; - -\ ML \ -"----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; -"----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; -"----------- equality (1*x + x \ 2 = 0) ----------------------------------------------------"; -"----- d2_pqformula5 ------"; -val fmz = ["equality (1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_pq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = - 1]" => () - | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]"; - -\ ML \ -"----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; -"----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; -"----------- equality (1*x + 1*x \ 2 = 0) ----------------------------------------------------"; -"----- d2_pqformula6 ------"; -val fmz = ["equality (1*x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_pq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = - 1]" => () - | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]"; - -\ ML \ -"----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; -"----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; -"----------- equality (x + x \ 2 = 0) ------------------------------------------------------"; -"----- d2_pqformula7 ------"; -(*EP- 10*) -val fmz = ["equality ( x + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_pq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = - 1]" => () - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; - -\ ML \ -"----------- equality (x + 1*x \ 2 = 0) ------------------------------------------------------"; -"----------- equality (x + 1*x \ 2 = 0) ------------------------------------------------------"; -"----------- equality (x + 1*x \ 2 = 0) ------------------------------------------------------"; -"----- d2_pqformula8 ------"; -val fmz = ["equality (x + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_pq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = - 1]" => () - | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]"; - -\ ML \ -"----------- equality (-4 + x \ 2 = 0) -------------------------------------------------------"; -"----------- equality (-4 + x \ 2 = 0) -------------------------------------------------------"; -"----------- equality (-4 + x \ 2 = 0) -------------------------------------------------------"; -"----- d2_pqformula9 ------"; -val fmz = ["equality (-4 + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_pq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 2, x = - 2]" => () - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]"; - - -\ ML \ -"----------- equality (4 + 1*x \ 2 = 0) -------------------------------------------------------"; -"----------- equality (4 + 1*x \ 2 = 0) -------------------------------------------------------"; -"----------- equality (4 + 1*x \ 2 = 0) -------------------------------------------------------"; -"----- d2_pqformula9_neg ------"; -val fmz = ["equality (4 + 1*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_pq_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -"TODO 4 + 1*x \ 2 = 0"; -"TODO 4 + 1*x \ 2 = 0"; -"TODO 4 + 1*x \ 2 = 0"; - -\ text \ (*rewrite_set_, rewrite_ ..= NONE*) -"-------------------- test thm's d2_abc_formulsxx[_neg]-----"; -"-------------------- test thm's d2_abc_formulsxx[_neg]-----"; -"-------------------- test thm's d2_abc_formulsxx[_neg]-----"; -val fmz = ["equality (- 1 +(- 1)*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => () - | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]"; - -\ ML \ -"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; -"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; -"----------- equality (1 +(- 1)*x + 2*x \ 2 = 0) ----------------------------------------------"; -val fmz = ["equality (1 +(- 1)*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; - -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -"TODO 1 +(- 1)*x + 2*x \ 2 = 0"; -"TODO 1 +(- 1)*x + 2*x \ 2 = 0"; -"TODO 1 +(- 1)*x + 2*x \ 2 = 0"; - - -\ ML \ -"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; -"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; -"----------- equality (- 1 + x + 2*x \ 2 = 0) -------------------------------------------------"; -(*EP- 11*) -val fmz = ["equality (- 1 + x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; - -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; - -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => () - | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]"; - - -\ ML \ -"----------- equality (1 + x + 2*x \ 2 = 0) --------------------------------------------------"; -"----------- equality (1 + x + 2*x \ 2 = 0) --------------------------------------------------"; -"----------- equality (1 + x + 2*x \ 2 = 0) --------------------------------------------------"; -val fmz = ["equality (1 + x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; - -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -"TODO 1 + x + 2*x \ 2 = 0"; -"TODO 1 + x + 2*x \ 2 = 0"; -"TODO 1 + x + 2*x \ 2 = 0"; - - -val fmz = ["equality (- 2 + 1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1, x = - 2]" => () - | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]"; - -val fmz = ["equality ( 2 + 1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -"TODO 2 + 1*x + x \ 2 = 0"; -"TODO 2 + 1*x + x \ 2 = 0"; -"TODO 2 + 1*x + x \ 2 = 0"; - -\ ML \ -(*EP- 12*) -val fmz = ["equality (- 2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 1, x = - 2]" => () - | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]"; - -val fmz = ["equality ( 2 + x + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -"TODO 2 + x + x \ 2 = 0"; -"TODO 2 + x + x \ 2 = 0"; -"TODO 2 + x + x \ 2 = 0"; - -\ ML \ -(*EP- 13*) -val fmz = ["equality (-8 + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 2, x = - 2]" => () - | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]"; - -val fmz = ["equality ( 8+ 2*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -"TODO 8+ 2*x \ 2 = 0"; -"TODO 8+ 2*x \ 2 = 0"; -"TODO 8+ 2*x \ 2 = 0"; - -\ ML \ -(*EP- 14*) -val fmz = ["equality (-4 + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 2, x = - 2]" => () - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]"; - - -\ ML \ -val fmz = ["equality ( 4+ x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -"TODO 4+ x \ 2 = 0"; -"TODO 4+ x \ 2 = 0"; -"TODO 4+ x \ 2 = 0"; - -\ ML \ -(*EP- 15*) -val fmz = ["equality (2*x + 2*x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = - 1]" => () - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; - -\ ML \ -val fmz = ["equality (1*x + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = - 1]" => () - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; - -\ text \ (*rewrite_set_, rewrite_ ..= NONE*) -\ ML \ -(*EP- 16*) -val fmz = ["equality (x + 2 * x \ 2 = (0::real))", "solveFor (x::real)", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -\ ML \ -(*+*)val Test_Out.FormKF "x + 2 * x \ 2 = 0" = f; -(*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt -\ ML \ -Rewrite.trace_on := false; (*false true*) -\ text \ (* *) -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \ 2 = 0", d2_polyeq_abcFormula_simplify*) -\ ML \ (*//---------------- adhoc inserted ------------------------------------------------\\*) -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt); -\ ML \ - val (pt, p) = - (*Step.by_tactic is here for testing by me; do_next would suffice in me*) - case Step.by_tactic tac (pt, p) of - ("ok", (_, _, ptp)) => ptp - | ("unsafe-ok", (_, _, ptp)) => ptp - | ("not-applicable",_) => (pt, p) - | ("end-of-calculation", (_, _, ptp)) => ptp - | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic" - | _ => raise ERROR "me: uncovered case Step.by_tactic" -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - (*case*) - Step.do_next p ((pt, Pos.e_pos'), []) (*of*); -\ ML \ -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), [])); -\ ML \ - (*if*) Pos.on_calc_end ip (*else*); -\ ML \ - val (_, probl_id, _) = Calc.references (pt, p); -\ ML \ -val _ = - (*case*) tacis (*of*); -\ ML \ - (*if*) probl_id = Problem.id_empty (*else*); -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - switch_specify_solve p_ (pt, ip); -\ ML \ -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); -\ ML \ - (*if*) Pos.on_specification ([], state_pos) (*else*); -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - LI.do_next (pt, input_pos) -\ ML \ -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos); -\ ML \ - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); -\ ML \ - val thy' = get_obj g_domID pt (par_pblobj pt p); - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - (*case*) - LI.find_next_step sc (pt, pos) ist ctxt (*of*); -\ ML \ -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) = - (sc, (pt, pos), ist, ctxt); -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - (*case*) - LI.scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) -\ ML \ -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) = - ((prog, (ptp, ctxt)), (Pstate ist)); -\ ML \ - (*if*) path = [] (*else*); -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - go_scan_up (prog, cc) (trans_scan_up ist) -\ ML \ -"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) = - ((prog, cc), (trans_scan_up ist)); -\ ML \ - (*if*) path = [R] (*else*); -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - scan_up pcc (ist |> path_up) (go_up path sc) -\ ML \ -"~~~~~ and scan_up , args:"; val (pcc, ist,(Const (\<^const_name>\Tactical.Try\(*1*), _) $ _ )) = - (pcc, (ist |> path_up), (go_up path sc)); -\ text \ (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \ x = - 1 / 2 = NONE*) - go_scan_up pcc ist -\ ML \ -"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) = - (pcc, ist); -\ ML \ - (*if*) path = [R] (*else*); -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - scan_up pcc (ist |> path_up) (go_up path sc) -\ ML \ -"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\Tactical.Chain\(*3*), _) $ _)) = - (pcc, (ist |> path_up), (go_up path sc)); -\ ML \ - val e2 = check_Seq_up ist sc; -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - (*case*) - scan_dn cc (ist |> path_up_down [R]) e2 (*of*); -\ ML \ -"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\Tactical.Chain\(*2*), _) $ e1 $ e2)) = - (cc, (ist |> path_up_down [R]), e2); -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - (*case*) - scan_dn cc (ist |> path_down [L, R]) e1 (*of*); -\ ML \ -"~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const (\<^const_name>\Tactical.Try\(*2*), _) $ e)) = - (cc, (ist |> path_down [L, R]), e1); -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - (*case*) - scan_dn cc (ist |> path_down [R]) e (*of*); -\ ML \ -"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) = - (cc, (ist |> path_down [R]), e); -\ ML \ - (*if*) Tactical.contained_in t (*else*); -\ ML \ -val (Program.Tac prog_tac, form_arg) = (*case*) - LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*); -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - check_tac cc ist (prog_tac, form_arg) -\ ML \ -"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) = - (cc, ist, (prog_tac, form_arg)); -\ ML \ - val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac -\ ML \ -val _ = (*case*) m (*of*); -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - (*case*) -Solve_Step.check m (pt, p) (*of*); -\ ML \ -"~~~~~ fun check , args:"; val ((Tactic.Rewrite_Set rls), (cs as (pt, (p, _)))) = - (m, (pt, p)); -\ ML \ - val pp = Ctree.par_pblobj pt p; - val thy' = Ctree.get_obj Ctree.g_domID pt pp; - val f = Calc.current_formula cs; -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - (*case*) - Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f (*of*); -\ ML \ -"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = - ((ThyC.get_theory thy'), false, (assoc_rls rls), f); -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - rewrite__set_ thy 1 bool [] rls term; -\ ML \ -"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) = - (thy, 1, bool, [], rls, term); -\ ML \ -\ ML \ (* \ src/../rewrite.sml *) -(*//-------------------------------- cp fromewrite.sml-----------------------------------------\\*) -\ ML \ -fun msg call thy op_ thmC t = - call ^ ": \n" ^ - "Eval.get_pair for " ^ quote op_ ^ " \ SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^ - "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \ NONE"; -\ ML \ - (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*) - datatype switch = Appl | Noap; - fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *) - | rew_once ruls asm ct Appl [] = - (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls - | Rule_Set.Sequence _ => (ct, asm) - | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\"")) - | rew_once ruls asm ct apno (rul :: thms) = - case rul of - Rule.Thm (thmid, thm) => - (trace_in1 i "try thm" thmid; - case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm ct of - NONE => rew_once ruls asm ct apno thms - | SOME (ct', asm') => - (trace_in2 i "rewrites to" thy ct'; - rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms))) - (* once again try the same rule, e.g. associativity against "()"*) - | Rule.Eval (cc as (op_, _)) => - let val _ = trace_in1 i "try calc" op_; - in case Eval.adhoc_thm thy cc ct of - NONE => rew_once ruls asm ct apno thms - | SOME (_, thm') => - let - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm' ct; - val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" thy op_ thm' ct) - val _ = trace_in3 i "calc. to" thy pairopt; - in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end - end - | Rule.Cal1 (cc as (op_, _)) => - let val _ = trace_in1 i "try cal1" op_; - in case Eval.adhoc_thm1_ thy cc ct of - NONE => (ct, asm) - | SOME (_, thm') => - let - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm' ct; - val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^ - ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE") - val _ = trace_in3 i "cal1. to" thy pairopt; - in the pairopt end - end - | Rule.Rls_ rls' => - (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of - SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms - | NONE => rew_once ruls asm ct apno thms) - | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\""); -(*\\------------------------------- cp from rewrite.sml---------------------------------------//*) -\ ML \ - val ruls = (#rules o Rule_Set.rep) rls; -\ text \ (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) -Rewrite.trace_on := false; (*false rew_once-3-isa.txt true*) - val (ct', asm') = - rew_once ruls [] ct Noap ruls; -\ ML \ -(*+*)UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \ x = (- 1 - sqrt (1 - 0)) / (2 * 2)"; -\ ML \ -(*+*)rls;(*val it = - Repeat - {calc = - [("PLUS", ("Groups.plus_class.plus", fn)), ("MINUS", ("Groups.minus_class.minus", fn)), ("TIMES", ("Groups.times_class.times", fn)), - ("DIVIDE", ("Rings.divide_class.divide", fn)), ("SQRT", ("NthRoot.sqrt", fn)), ("POWER", ("Transcendental.powr", fn))], - ======^^^^^^====== - erls = ------------------------------ id = "calc_rat_erls" ------------------------------------------------------vvvvvvvvvvvvvvvvvvvv - Repeat - {calc = [("DIVIDE", ("Rings.divide_class.divide", fn))], erls = - ======^^^^^^====== - Repeat - {calc = [("matches", ("Prog_Expr.matches", fn)), ("equal", ("HOL.eq", fn)), ("is_num", ("Prog_Expr.is_num", fn))], erls = Empty, errpatts = [], id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", fn), - rules = [Eval ("Prog_Expr.matches", fn), Eval ("HOL.eq", fn), Eval ("Prog_Expr.is_num", fn), Thm ("not_true", "(\ True) = False"), Thm ("not_false", "(\ False) = True")], scr = Empty_Prog, srls = Empty}, - errpatts = [], id = "PolyEq_erls", <<<------------------------------------- "PolyEq_erls" - preconds = [], rew_ord = ("dummy_ord", fn), rules = - [Thm ("real_assoc_1", "?a + (?b + ?c) = ?a + ?b + ?c"), Eval ("Transcendental.powr", fn), Eval ("Groups.times_class.times", fn), Eval ("Groups.minus_class.minus", fn), Eval ("Groups.plus_class.plus", fn), - Thm ("real_unari_minus", "\ (?a is_num) \ - ?a = - 1 * ?a"), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.occurs_in", fn), Eval ("Prog_Expr.is_num", fn), Eval ("Prog_Expr.ident", fn), - Eval ("Orderings.ord_class.less_eq", fn), Eval ("Orderings.ord_class.less", fn), Thm ("radd_left_cancel_le", "(?k + ?m \ ?k + ?n) = (?m \ ?n)"), Thm ("order_refl", "?x \ ?x"), Thm ("refl", "?t = ?t"), - Thm ("or_false", "(?a \ False) = ?a"), Thm ("or_true", "(?a \ True) = True"), Thm ("and_false", "(?a \ False) = False"), Thm ("and_true", "(?a \ True) = ?a"), Thm ("not_false", "(\ False) = True"), - Thm ("not_true", "(\ True) = False"), Thm ("mult_cross2", "?d \ 0 \ (?a = ?c / ?d) = (?a * ?d = ?c)"), Thm ("mult_cross1", "?b \ 0 \ (?a / ?b = ?c) = (?a = ?b * ?c)"), - Thm ("mult_cross", "?b \ 0 \ ?d \ 0 \ (?a / ?b = ?c / ?d) = (?a * ?d = ?b * ?c)"), Thm ("rat_power", "(?a / ?b) \ ?n = ?a \ ?n / ?b \ ?n"), Thm ("divide_divide_eq_left", "?a / ?b / ?c = ?a / (?b * ?c)"), - Thm ("real_divide_divide1", "?y \ 0 \ ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"), Thm ("times_divide_eq_left", "?b / ?c * ?a = ?b * ?a / ?c"), - Thm ("times_divide_eq_right", "?a * (?b / ?c) = ?a * ?b / ?c"), Thm ("rat_mult", "?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"), - Thm ("rat_add3", "?a is_num \ ?b is_num \ ?c is_num \ ?a + ?b / ?c = (?a * ?c + ?b) / ?c"), Thm ("rat_add2", "?a is_num \ ?b is_num \ ?c is_num \ ?a / ?c + ?b = (?a + ?b * ?c) / ?c"), - Thm ("rat_add1", "?a is_num \ ?b is_num \ ?c is_num \ ?a / ?c + ?b / ?c = (?a + ?b) / ?c"), - Thm ("rat_add", "?a is_num \ ?b is_num \ ?c is_num \ ?d is_num \ ?a / ?c + ?b / ?d = (?a * ?d + ?b * ?c) / (?c * ?d)"), Thm ("sym_minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"), - Eval ("Rings.divide_class.divide", fn), Eval ("HOL.eq", fn), Thm ("plus_leq", "(0 \ ?a + ?b) = (- 1 * ?b \ ?a)"), Thm ("minus_leq", "(0 \ ?a - ?b) = (?b \ ?a)"), - ======^^^^^^====== - Thm ("rat_leq1", "0 \ ?b \ 0 \ ?d \ (?a / ?b \ ?c / ?d) = (?a * ?d \ ?b * ?c)"), Thm ("rat_leq2", "0 \ ?d \ (?a \ ?c / ?d) = (?a * ?d \ ?c)"), - Thm ("rat_leq3", "0 \ ?b \ (?a / ?b \ ?c) = (?a \ ?b * ?c)")], - scr = Empty_Prog, srls = Empty}, - errpatts = [], id = "polyeq_simplify", <<<------------------------------- "polyeq_simplify" - preconds = [], rew_ord = ("termlessI", fn), rules = - [Thm ("real_assoc_1", "?a + (?b + ?c) = ?a + ?b + ?c"), Thm ("real_assoc_2", "?a * (?b * ?c) = ?a * ?b * ?c"), Thm ("real_diff_minus", "?a - ?b = ?a + - 1 * ?b"), - Thm ("real_unari_minus", "\ (?a is_num) \ - ?a = - 1 * ?a"), Thm ("realpow_multI", "(?r * ?s) \ ?n = ?r \ ?n * ?s \ ?n"), Eval ("Groups.plus_class.plus", fn), Eval ("Groups.minus_class.minus", fn), - Eval ("Groups.times_class.times", fn), Eval ("Rings.divide_class.divide", fn), Eval ("NthRoot.sqrt", fn), Eval ("Transcendental.powr", fn), - ======^^^^^^====== - Rls_ - ( - Repeat - {calc = [], erls = - Repeat ---------vvvvvvvvvvvvvvvvvvvvvvvvv------------------ - {calc = [], erls = Empty, errpatts = [], id = "erls_in_reduce_012", preconds = [], rew_ord = ("dummy_ord", fn), rules = - [Eval ("Prog_Expr.is_num", fn), Thm ("not_false", "(\ False) = True"), Thm ("not_true", "(\ True) = False")], scr = Empty_Prog, srls = Empty}, - errpatts = [], id = "reduce_012", <<<---------------------------------- "reduce_012" - preconds = [], rew_ord = ("dummy_ord", fn), rules = - [Thm ("mult_1_left", "1 * ?a = ?a"), Thm ("real_minus_mult_left", "\ (?a is_num) \ - ?a * ?b = - (?a * ?b)"), Thm ("mult_zero_left", "0 * ?a = 0"), Thm ("add_0_left", "0 + ?a = ?a"), - Thm ("add_0_right", "?a + 0 = ?a"), Thm ("right_minus", "?a + - ?a = 0"), Thm ("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1"), Thm ("real_mult_2_assoc", "?z1.0 + (?z1.0 + ?k) = 2 * ?z1.0 + ?k")], - scr = Empty_Prog, srls = Empty} - )], - scr = Empty_Prog, srls = Empty}: id = - Rule_Def.rule_set*) -\ ML \ -"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms)) = - (ruls, [], ct, Noap, ruls); -\ ML \ -val Rule.Thm (thmid, thm) = - (*case*) rul (*of*); -\ ML \ -val NONE = (*case*) rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*); -\ ML \ -(* GOON: find a way to find out, why test -- fun adhoc_thm + fun eval_cancel -- gives - Eval.adhoc_thm \ NONE and above we have ERROR -(*rew_once: Eval.get_pair for "Rings.divide_class.divide" \ SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE*) - - *) -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -(*/------------------------------- fun rew_once ITERATED BY HAND -----------------------------\*) -\ ML \ -UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \ x = (- 1 - sqrt (1 - 0)) / (2 * 2)"; -\ ML \ -val thm = Rule.thm (nth 1 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*) -\ ML \ -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*); -\ ML \ -val thm = Rule.thm (nth 2 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c" - ATTENTION "real_assoc_1" == "real_assoc_2"*) -\ ML \ -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm ct -\ ML \ -val thm = Rule.thm (nth 3 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*) -\ ML \ -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm ct -\ ML \ -UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \\nx = (- 1 + - 1 * sqrt (1 - 0)) / (2 * 2)" -\ ML \ -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm ct -\ ML \ -UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)" -\ ML \ -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm ct -\ ML \ -UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)" -\ ML \ -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm ct -\ ML \ -val thm = Rule.thm (nth 4 ruls); (* = "\ (?a is_num) \ - ?a = - 1 * ?a"*) -\ ML \ -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm ct -\ ML \ -val thm = Rule.thm (nth 5 ruls); (* = "(?r * ?s) \ ?n = ?r \ ?n * ?s \ ?n"*) -\ ML \ -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm ct -\ ML \ (* \ Rule.*) -\ ML \ -val (cc as (op_, _)) = Rule.eval (nth 6 ruls); (* = "Groups.plus_class.plus"*) -\ ML \ -val NONE = Eval.adhoc_thm thy cc ct -\ ML \ -val (cc as (op_, _)) = Rule.eval (nth 7 ruls); (* = "Groups.minus_class.minus"*) -\ ML \ -val NONE = Eval.adhoc_thm thy cc ct -\ ML \ -val (cc as (op_, _)) = Rule.eval (nth 8 ruls); (* = "Groups.times_class.times"*) -\ ML \ -val SOME (_, thm') = Eval.adhoc_thm thy cc ct -\ ML \ -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm' ct; -\ ML \ - "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)"; -UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)" -\ ML \ -val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm' ct; -\ ML \ -UnparseC.term ct = "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)" -\ ML \ -val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) - ((#erls o Rule_Set.rep) rls) put_asm thm' ct; -\ ML \ -val (cc as (op_, _)) = Rule.eval (nth 9 ruls); (* = "Rings.divide_class.divide"*) -\ ML \ -val NONE = Eval.adhoc_thm thy cc ct -\ ML \ -val (cc as (op_, _)) = Rule.eval (nth 10 ruls); (* = "NthRoot.sqrt"*) -\ ML \ -val NONE = Eval.adhoc_thm thy cc ct -\ ML \ -val (cc as (op_, _)) = Rule.eval (nth 11 ruls); (* = "Transcendental.powr"*) -\ ML \ -val NONE = Eval.adhoc_thm thy cc ct -\ ML \ -val rls' = Rule.rls (nth 12 ruls); (* = "reduce_012"*) -\ ML \ -val SOME (ct, []) = rewrite__set_ thy (i + 1) put_asm bdv rls' ct -\ ML \ - "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)"; -UnparseC.term ct = "x = (- 1 + sqrt 1) / (2 * 2) \ x = (- 1 + - 1 * sqrt 1) / (2 * 2)" -\ ML \ -length ruls = 12; -(*========== now are further iterations to come, and there is the strange error ===============*) -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ (*\\---------------- adhoc inserted ------------------------------------------------//*) -\ text \ -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => () - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]"; - -\ ML \ -(*EP-//*) -val fmz = ["equality (x + x \ 2 = 0)", "solveFor x", "solutions L"]; -val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], - ["PolyEq", "solve_d2_polyeq_abc_equation"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -case f of Test_Out.FormKF "[x = 0, x = - 1]" => () - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; - - -\ ML \ -"----------- (-8 - 2*x + x \ 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; -"----------- (-8 - 2*x + x \ 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; -"----------- (-8 - 2*x + x \ 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat -see --- val rls = calculate_RootRat > calculate_Rational --- -calculate_RootRat was a TODO with 2002, requires re-design. -see also --- (-8 - 2*x + x \ 2 = 0), by rewriting --- below -*) - val fmz = ["equality (-8 - 2*x + x \ 2 = 0)", (*Schalk 2, S.67 Nr.31.b*) +"----------- (a*b - (a+b)*x + x \ 2 = 0), (*Schalk 2,S.68Nr.44.a*)"; +"----------- (a*b - (a+b)*x + x \ 2 = 0), (*Schalk 2,S.68Nr.44.a*)"; +"----------- (a*b - (a+b)*x + x \ 2 = 0), (*Schalk 2,S.68Nr.44.a*)"; + val fmz = ["equality (a*b - (a+b)*x + x \ 2 = 0)", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["degree_2", "expanded", "univariate", "equation"], ["PolyEq", "complete_square"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; - -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*Apply_Method ("PolyEq", "complete_square")*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"-8 - 2 * x + x \ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"-8 + (2 / 2 - x) \ 2 = (2 / 2) \ 2", nxt = Rewrite("square_explicit1"*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"(2 / 2 - x) \ 2 = (2 / 2) \ 2 - -8" nxt = Rewrite("root_plus_minus*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"2 / 2 - x = sqrt ((2 / 2) \ 2 - -8) | - 2 / 2 - x = - sqrt ((2 / 2) \ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"2 / 2 - x = sqrt ((2 / 2) \ 2 - -8) | - - 1*x = - (2 / 2) + - sqrt ((2 / 2) \ 2 - -8)"nxt = R_Inst("bdv_explt2"*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - -8) | - - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))"nxt = bdv_explicit3*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - -8) | - x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))" nxt = bdv_explicit3*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \ 2 - -8)) | - x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \ 2 - -8))"nxt = calculate_Rational - NOT IMPLEMENTED SINCE 2002 ------------------------------ \ \ \ \ \ \ *) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"x = - 2 | x = 4" nxt = Or_to_List*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*"[x = - 2, x = 4]" nxt = Check_Postcond*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; -(* FIXXXME - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO - | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]"; -*) -if f2str f = - "[x = - 1 * - 1 + - 1 * sqrt (2 \ 2 / 2 \ 2 - - 8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - - 8))]" -(*"[x = - 1 * - 1 + - 1 * sqrt (1 \ 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \ 2 - -8))]"*) -then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]"; +(*WN.2.5.03 TODO FIXME Matthias ? + case f of + Form' + (Test_Out.FormKF + (~1,EdUndef,0,Nundef, + "[x = (a + b) / 2 + - 1 * sqrt ((a + b) \ 2 / 2 \ 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) \ 2 / 2 \ 2 - a * b)]")) + => () + | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x \ 2 = 0"; + this will be simplified [x = a, x = b] to by Factor.ML*) \ ML \ -"----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; -"----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; -"----------- (-8 - 2*x + x \ 2 = 0), by rewriting ---------------"; -(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat -see --- val rls = calculate_RootRat > calculate_Rational ---*) -val thy = @{theory PolyEq}; -val ctxt = Proof_Context.init_global thy; -val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")]; -val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \ 2 = (0::real)"; - -\ ML \ -val rls = complete_square; -val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t; -\ ML \ -if UnparseC.term t = "- 8 + (2 / 2 - x) \ 2 = (2 / 2) \ 2" -then () else error "rls complete_square CHANGED"; - -\ ML \ -val thm = @{thm square_explicit1}; -val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t; -\ ML \ -if UnparseC.term t = "(2 / 2 - x) \ 2 = (2 / 2) \ 2 - - 8" -then () else error "thm square_explicit1 CHANGED"; - -\ ML \ -val thm = @{thm root_plus_minus}; -val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t; -\ ML \ -if UnparseC.term t = -"2 / 2 - x = sqrt ((2 / 2) \ 2 - - 8) \\n2 / 2 - x = - 1 * sqrt ((2 / 2) \ 2 - - 8)" -then () else error "thm root_plus_minus CHANGED"; - -\ ML \ -(*the thm bdv_explicit2* here required to be constrained to ::real*) -val thm = @{thm bdv_explicit2}; -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; -\ ML \ -if UnparseC.term t = -"2 / 2 - x = sqrt ((2 / 2) \ 2 - - 8) \\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - - 8)" -then () else error "thm bdv_explicit2 CHANGED"; - -\ ML \ -val thm = @{thm bdv_explicit3}; -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; -\ ML \ -if UnparseC.term t = -"2 / 2 - x = sqrt ((2 / 2) \ 2 - - 8) \\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - - 8))" -then () else error "thm bdv_explicit3 CHANGED"; - -\ ML \ -val thm = @{thm bdv_explicit2}; -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; -\ ML \ -if UnparseC.term t = -"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \ 2 - - 8) \\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \ 2 - - 8))" -then () else error "thm bdv_explicit2 CHANGED"; - -\ ML \ -val rls = calculate_RootRat; -val SOME (t,asm) = rewrite_set_ thy true rls t; -\ ML \ -if UnparseC.term t = - "- 1 * x = - 1 + sqrt (2 \ 2 / 2 \ 2 - - 8) \\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - - 8))" -(*"- 1 * x = - 1 + sqrt (2 \ 2 / 2 \ 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \ 2 / 2 \ 2 - -8))"..isabisac15*) -then () else error "(-8 - 2*x + x \ 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT"; -(*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*) - - -\ ML \ -"-------------------- (3 - 10*x + 3*x \ 2 = 0), ----------------------"; -"-------------------- (3 - 10*x + 3*x \ 2 = 0), ----------------------"; -"-------------------- (3 - 10*x + 3*x \ 2 = 0), ----------------------"; -"---- test the erls ----"; - val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \ 2 - 1"; - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1; - val t' = UnparseC.term t; - (*if t'= \<^const_name>\True\ then () - else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*) -(* *) - val fmz = ["equality (3 - 10*x + 3*x \ 2 = 0)", +"----------- (-64 + x \ 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; +"----------- (-64 + x \ 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; +"----------- (-64 + x \ 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; + val fmz = ["equality (-64 + x \ 2 = 0)",(*Schalk 2, S.66 Nr.1.a~*) "solveFor x", "solutions L"]; val (dI',pI',mI') = ("PolyEq",["degree_2", "expanded", "univariate", "equation"], ["PolyEq", "complete_square"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - (*Apply_Method ("PolyEq", "complete_square")*) - val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; +(*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = - 1 * sqrt (0 - -64)]" + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => () + | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]"; +*) -"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; -"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; -"----------- (- 16 + 4*x + 2*x \ 2 = 0), --------------------------"; - val fmz = ["equality (- 16 + 4*x + 2*x \ 2 = 0)", +\ ML \ +"----------- (- 147 + 3*x \ 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; +"----------- (- 147 + 3*x \ 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; +"----------- (- 147 + 3*x \ 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; +val fmz = ["equality (- 147 + 3*x \ 2 = 0)",(*Schalk 2, S.66 Nr.1.b*) "solveFor x", "solutions L"]; - val (dI',pI',mI') = +val (dI',pI',mI') = ("PolyEq",["degree_2", "expanded", "univariate", "equation"], ["PolyEq", "complete_square"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - (*Apply_Method ("PolyEq", "complete_square")*) - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; - val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(* FIXXXXME n1., - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO - | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]"; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]" + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => () + | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]"; *) +if f2str f = "[x = sqrt (0 - - 49), x = - 1 * sqrt (0 - - 49)]" then () +else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]"; + \ ML \ -\ +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5"; +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5"; +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5"; +(*EP- 17 Schalk_I_p86_n5*) +val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"]; +(* Refine.refine fmz ["univariate", "equation"]; +*) +val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(* val nxt = + ("Model_Problem", + Model_Problem ["normalise", "polynomial", "univariate", "equation"]) + : string * tac*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(* val nxt = + ("Subproblem", + Subproblem ("PolyEq",["polynomial", "univariate", "equation"])) + : string * tac *) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = + ("Model_Problem", + Model_Problem ["degree_1", "polynomial", "univariate", "equation"]) + : string * tac *) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +case f of Test_Out.FormKF "[x = 2]" => () + | _ => error "polyeq.sml: diff.behav. in [x = 2]"; -section \===================================================================================\ -ML \ + \ ML \ +"----------- ((x+1)*(x+2) - (3*x - 2) \ 2=.. Schalk II s.68 Bsp 37"; +"----------- ((x+1)*(x+2) - (3*x - 2) \ 2=.. Schalk II s.68 Bsp 37"; +"----------- ((x+1)*(x+2) - (3*x - 2) \ 2=.. Schalk II s.68 Bsp 37"; +(*is in rlang.sml, too*) +val fmz = ["equality ((x+1)*(x+2) - (3*x - 2) \ 2=(2*x - 1) \ 2+(3*x - 1)*(x+1))", + "solveFor x", "solutions L"]; +val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate", "equation"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(* val nxt = + ("Model_Problem", + Model_Problem ["normalise", "polynomial", "univariate", "equation"]) + : string * tac *) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(* val nxt = + ("Subproblem", + Subproblem ("PolyEq",["polynomial", "univariate", "equation"])) + : string * tac*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = + ("Model_Problem", + Model_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]) + : string * tac*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +case f of Test_Out.FormKF "[x = 2 / 15, x = 1]" => () + | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]"; + + +" -4 + x \ 2 =0 "; +" -4 + x \ 2 =0 "; +" -4 + x \ 2 =0 "; +val fmz = ["equality ( -4 + x \ 2 =0)", "solveFor x", "solutions L"]; +(* val fmz = ["equality (1 + x \ 2 =0)", "solveFor x", "solutions L"];*) +(*val fmz = ["equality (0 =0)", "solveFor x", "solutions L"];*) +val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; + +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +case f of Test_Out.FormKF "[x = 2, x = - 2]" => () + | _ => error "polyeq.sml: diff.behav. in [x = 2, x = - 2]"; + +\ ML \ +"----------- rls make_polynomial_in ------------------------------"; +"----------- rls make_polynomial_in ------------------------------"; +"----------- rls make_polynomial_in ------------------------------"; +val thy = @{theory}; +(*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*) +(*WN.19.3.03 ---v-*) +(*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1"); +val t = TermC.str2term "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0"; +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; +if UnparseC.term t' = "- 1 * R * R2 + R2 * R1 + - 1 * R * R1 = 0" then () +else error "make_polynomial_in (- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0)"; +"- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0"; +(*WN.19.3.03 ---^-*) + +(*3(c)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "p"); +val t = TermC.str2term "y \ 2 + - 2 * (x * p) = 0"; +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; +if UnparseC.term t' = "y \ 2 + - 2 * x * p = 0" then () +else error "make_polynomial_in (y \ 2 + - 2 * (x * p) = 0)"; + +(*3(d)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "x2"); +val t = TermC.str2term +"A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1 * (x1 * (y2 * (1 / 2))) + - 1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + - 1 * (y3 * (1 / 2 * x2)) = 0"; +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; +if UnparseC.term t' = +"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - 1 * x1 * y2 * (1 / 2) +\n- 1 * x3 * y1 * (1 / 2) +\ny1 * (1 / 2) * x2 +\n- 1 * y3 * (1 / 2) * x2 =\n0" +then () +else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1..."; +"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0"; + +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t; +if UnparseC.term t' = +"A / 1 + x1 * y3 / 2 + x3 * y2 / 2 + - 1 * x1 * y2 / 2 + - 1 * x3 * y1 / 2 +\ny1 * x2 / 2 +\n- 1 * y3 * x2 / 2 =\n0" +then () +else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1..."; +"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - 1 * x1 * y2 * (1 / 2) + - 1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - 1 * y3 * (1 / 2)) * x2 = 0"; + +(*3(e)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "a"); +val t = TermC.str2term +"A \ 2 + c \ 2 * (c / d) \ 2 + (-4 * (c / d) \ 2) * a \ 2 = 0"; +val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; +(* the invisible parentheses are as expected *) + +val t = TermC.str2term "(x + 1) * (x + 2) - (3 * x - 2) \ 2 - ((2 * x - 1) \ 2 + (3 * x - 1) * (x + 1)) = 0"; +Rewrite.trace_on:= false; (*true false*) +rewrite_set_ thy false expand_binoms t; +Rewrite.trace_on:=false; (*true false*) + + +\ ML \ +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; +reset_states (); +CalcTree +[(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"], + ("PolyEq",["univariate", "equation"],["no_met"]))]; +Iterator 1; +moveActiveRoot 1; + +autoCalculate 1 CompleteCalc; +val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; +interSteps 1 ([1],Res) +(*BEFORE Isabelle2002 --> 2011: no Rewrite_Set... ?see fun prep_rls?*); + + +\ ML \ +"----------- rls d2_polyeq_bdv_only_simplify ---------------------"; +"----------- rls d2_polyeq_bdv_only_simplify ---------------------"; +"----------- rls d2_polyeq_bdv_only_simplify ---------------------"; +val t = TermC.str2term "-6 * x + 5 * x \ 2 = (0::real)"; +val subst = [(TermC.str2term "(bdv::real)", TermC.str2term "(x::real)")]; +val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t; +(* steps in rls d2_polyeq_bdv_only_simplify:*) + +(*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*) +t |> UnparseC.term; t |> TermC.atomty; +val thm = @{thm d2_prescind1}; +thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty; +val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t'; + +(*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) + --> x = 0 | -6 + 5 * x = 0*) +t' |> UnparseC.term; t' |> TermC.atomty; +val thm = @{thm d2_reduce_equation1}; +thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty; +val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t''; +(* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" + instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))" +*) +if UnparseC.term t'' = "x = 0 \ - 6 + 5 * x = 0" then () +else error "rls d2_polyeq_bdv_only_simplify broken"; \ ML \ \ ML \ \