1.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Sat Aug 21 18:58:33 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Sun Aug 22 09:43:43 2021 +0200
1.3 @@ -21,6 +21,8 @@
1.4 val distinct' : rule list -> rule list
1.5
1.6 val thm_id: rule -> string
1.7 + val eval: rule -> string * Rule_Def.eval_fn
1.8 + val rls: rule -> Rule_Def.rule_set
1.9
1.10 val make_eval: string -> Rule_Def.eval_fn -> rule
1.11 end
1.12 @@ -70,6 +72,11 @@
1.13 fun thm (Rule_Def.Thm (_, thm)) = thm
1.14 | thm r = raise ERROR ("Rule.thm: uncovered case " ^ to_string r)
1.15
1.16 +fun eval (Eval e) = e
1.17 + | eval r = raise ERROR ("Rule.eval NOT FOR " ^ to_string r)
1.18 +fun rls (Rls_ rls) = rls
1.19 + | rls r = raise ERROR ("Rule.rls NOT FOR " ^ to_string r)
1.20 +
1.21
1.22 (* ML antiquotations *)
1.23
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Aug 21 18:58:33 2021 +0200
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sun Aug 22 09:43:43 2021 +0200
2.3 @@ -109,7 +109,7 @@
2.4 Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'), ctxt)
2.5 end
2.6 | _ =>
2.7 - (case Solve_Step.check m (pt, p) of
2.8 + (case Solve_Step.check m (pt, p) of
2.9 Applicable.Yes m' =>
2.10 Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'),
2.11 Tactic.insert_assumptions m' ctxt)
3.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sat Aug 21 18:58:33 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sun Aug 22 09:43:43 2021 +0200
3.3 @@ -410,13 +410,11 @@
3.4 val calc_rat_erls =
3.5 prep_rls'
3.6 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
3.7 - erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
3.8 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
3.9 rules = [
3.10 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
3.11 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
3.12 -(*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* )
3.13 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
3.14 -( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
3.15 \<^rule_thm>\<open>not_true\<close>,
3.16 \<^rule_thm>\<open>not_false\<close>],
3.17 scr = Rule.Empty_Prog});
3.18 @@ -654,6 +652,7 @@
3.19 rules = [
3.20 (*\<^rule_thm>\<open>divide_1\<close>, "?x / 1 = ?x" unnecessary.for normalform*)
3.21 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
3.22 + \<^rule_thm>\<open>minus_zero\<close>, (*"- 0 = 0"*)
3.23 (*\<^rule_thm>\<open>real_mult_minus1\<close>, "-1 * z = - z"*)
3.24 (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>, "- ?x * - ?y = ?x * ?y"*)
3.25
4.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Sat Aug 21 18:58:33 2021 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Sun Aug 22 09:43:43 2021 +0200
4.3 @@ -79,6 +79,9 @@
4.4 if ! trace_on andalso i < ! depth
4.5 then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_thy thy p')
4.6 else();
4.7 +fun msg thy op_ thmC t =
4.8 + "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^
4.9 + "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
4.10
4.11 fun rewrite__ thy i bdv tless rls put_asm thm ct =
4.12 let
4.13 @@ -139,23 +142,23 @@
4.14 (*asm false .. thm not applied ^^^; continue until False vvv*)
4.15 else chk (indets @ [t] @ a') asms);
4.16 in chk [] asms end
4.17 -and rewrite__set_ thy _ _ _ Rule_Set.Empty t = (* rewrite with a rule set*)
4.18 +and rewrite__set_ thy (*1*)_ _ _ Rule_Set.Empty t = (* rewrite with a rule set*)
4.19 raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
4.20 - | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*)
4.21 + | rewrite__set_ (*2*)thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*)
4.22 let
4.23 val _= trace_eq1 i "rls" rrls thy t;
4.24 val (t', asm, rew) = app_rev thy (i + 1) rrls t
4.25 in if rew then SOME (t', distinct op = asm) else NONE end
4.26 - | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Eval, Cal1 *)
4.27 + | rewrite__set_ (*3*)thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Eval, Cal1 *)
4.28 let
4.29 (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
4.30 datatype switch = Appl | Noap;
4.31 - fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
4.32 - | rew_once ruls asm ct Appl [] =
4.33 + fun rew_once (*1*)_ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
4.34 + | rew_once (*2*)ruls asm ct Appl [] =
4.35 (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
4.36 | Rule_Set.Sequence _ => (ct, asm)
4.37 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
4.38 - | rew_once ruls asm ct apno (rul :: thms) =
4.39 + | rew_once (*3*)ruls asm ct apno (rul :: thms) =
4.40 case rul of
4.41 Rule.Thm (thmid, thm) =>
4.42 (trace_in1 i "try thm" thmid;
4.43 @@ -174,8 +177,7 @@
4.44 let
4.45 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.46 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
4.47 - val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
4.48 - ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
4.49 + val _ = if pairopt <> NONE then () else raise ERROR (msg thy op_ thm' ct)
4.50 val _ = trace_in3 i "calc. to" thy pairopt;
4.51 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
4.52 end
5.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sat Aug 21 18:58:33 2021 +0200
5.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Aug 22 09:43:43 2021 +0200
5.3 @@ -732,7 +732,7 @@
5.4 setNextTactic 1 (Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]);
5.5 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
5.6 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "d1_polyeq_simplify"));
5.7 -(*SINCE eliminate ThmC.numerals_to_Free:
5.8 +(*SINCE eliminate ThmC.numerals_to_Free: TOODOO
5.9 rewrite_set_, rewrite_ "- 4 / 3 = - 4 / 3" x = - 4 / 3 = NONE---------------------------\\* )
5.10 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
5.11 setNextTactic 1 (Rewrite_Set "polyeq_simplify");
6.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Sat Aug 21 18:58:33 2021 +0200
6.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Sun Aug 22 09:43:43 2021 +0200
6.3 @@ -1,4 +1,4 @@
6.4 -(* Title: Knowledge/polyeq- 1.sml
6.5 +(* Title: Knowledge/polyeq-1.sml
6.6 testexamples for PolyEq, poynomial equations and equational systems
6.7 Author: Richard Lang 2003
6.8 (c) due to copyright terms
7.1 --- a/test/Tools/isac/Knowledge/rootrat.sml Sat Aug 21 18:58:33 2021 +0200
7.2 +++ b/test/Tools/isac/Knowledge/rootrat.sml Sun Aug 22 09:43:43 2021 +0200
7.3 @@ -14,50 +14,27 @@
7.4 "----------- val rls = calculate_RootRat > calculate_Rational ----";
7.5 "----------- val rls = calculate_RootRat > calculate_Rational ----";
7.6 "----------- val rls = calculate_RootRat > calculate_Rational ----";
7.7 -(*val calculate_RootRat =
7.8 - Rule_Set.append_rules "calculate_RootRat" calculate_Rational [...]
7.9 - val calculate_Rational = prep_rls (merge_rls "calculate_Rational" [...]
7.10 - calculate_Poly
7.11 - val calculate_Poly =
7.12 - Rule_Set.append_rules "calculate_PolyFIXXXME.not.impl." Rule_Set.empty [];
7.13 - WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
7.14 +(*
7.15 + Note after CS "eliminate ThmC.numerals_to_Free" and "replace is_const with is_num" Aug.2021:
7.16 + Output of this test is questionable, (*1*) is from long ago.
7.17 + Input is questionable, too.
7.18 + So this test is left for reactivating biegelinie-*.sml.
7.19 *)
7.20 -
7.21 val thy = @{theory RootRat};
7.22 val ctxt = Proof_Context.init_global thy;
7.23 -val ttt = (the o (parseNEW ctxt)) ("- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
7.24 - "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))");
7.25 -TermC.atomty t; (*!real ?by sqrt and \<up> ?*)
7.26 +val t = (the o (parseNEW ctxt))
7.27 +("- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) | \nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))");
7.28
7.29 -"--- val rls = calculate_Poly ---";
7.30 -(*val rls = assoc_rls "calculate_Poly"; WAS ME_Isa: 'calculate_Poly' not in system
7.31 -goon with what just started ...*)
7.32 -val calculate_Poly = Rule_Set.append_rules "calculate_Poly" Rule_Set.empty
7.33 - [ Eval (\<^const_name>\<open>plus\<close>,eval_binop "#add_"),
7.34 - Eval (\<^const_name>\<open>minus\<close>,eval_binop "#sub_"),
7.35 - Eval (\<^const_name>\<open>times\<close>,eval_binop "#mult_"),
7.36 - Eval (\<^const_name>\<open>powr\<close> ,eval_binop "#power_")
7.37 - ];
7.38 -val rls = calculate_Poly;
7.39 +val rls = calculate_Rational;
7.40 +val SOME (t', asm) = rewrite_set_ thy true rls t;
7.41 +if UnparseC.term t' =
7.42 + "- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - - 8) \<or>\nx = - 1 * (- 1 + - 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))"
7.43 +(*"- 1 * x = - 1 + sqrt (1 \<up> 2 - -8) | x = - 1 * (- 1 + - 1 * sqrt (1 \<up> 2 - -8))" (*1*)*)
7.44 +then () else error "rls calculate_Rational CHANGED";
7.45
7.46 -(*val SOME (t,asm) = rewrite_set_ thy true rls ttt; WAS: NONE .. ok*)
7.47 +val rls = calculate_RootRat;
7.48 +val SOME (t, asm) = rewrite_set_ thy true rls t;
7.49 +if UnparseC.term t =
7.50 +"- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - - 8) \<or>\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))"
7.51 +then () else error "rls calculate_RootRat CHANGED";
7.52
7.53 -"--- val rls = calculate_Rational ---";
7.54 -val rls = assoc_rls "calculate_Rational";
7.55 -val rls = calculate_Rational;
7.56 -
7.57 -val SOME (t,asm) = rewrite_set_ thy true rls ttt;
7.58 -if UnparseC.term t =
7.59 -"- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) \<or>\nx = - 1 * (- 1 + - 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"
7.60 -(*"- 1 * x = - 1 + sqrt (1 \<up> 2 - -8) | x = - 1 * (- 1 + - 1 * sqrt (1 \<up> 2 - -8))"*)
7.61 -then () else error "val rls = calculate_Rational goon";
7.62 -
7.63 -"--- val rls = calculate_RootRat ---";
7.64 -val rls = assoc_rls "calculate_RootRat";
7.65 -val rls = calculate_RootRat;
7.66 -
7.67 -val SOME (t,asm) = rewrite_set_ thy true rls ttt;
7.68 -
7.69 -(*~~~~~ val rls = calculate_RootRat: rewrite stepwise*)
7.70 -val thm = ThmC.numerals_to_Free @{thm complete_square2};
7.71 -
8.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sat Aug 21 18:58:33 2021 +0200
8.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sun Aug 22 09:43:43 2021 +0200
8.3 @@ -190,7 +190,7 @@
8.4 ML_file "BaseDefinitions/calcelems.sml"
8.5 ML_file "BaseDefinitions/termC.sml"
8.6 ML_file "BaseDefinitions/substitution.sml"
8.7 -(*ML_file "BaseDefinitions/contextC.sml" TOODOO.1 broken with real_unary_minus *)
8.8 + ML_file "BaseDefinitions/contextC.sml"
8.9 ML_file "BaseDefinitions/environment.sml"
8.10 (** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
8.11 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
8.12 @@ -232,9 +232,9 @@
8.13
8.14 subsection \<open>further functionality alongside batch build sequence\<close>
8.15 ML_file "MathEngBasic/thmC.sml"
8.16 -(*ML_file "MathEngBasic/rewrite.sml" TOODOO.1 loops with real_unary_minus *)
8.17 + ML_file "MathEngBasic/rewrite.sml"
8.18 ML_file "MathEngBasic/tactic.sml"
8.19 -(*ML_file "MathEngBasic/ctree.sml" TOODOO.1 loops with real_unary_minus *)
8.20 + ML_file "MathEngBasic/ctree.sml"
8.21 ML_file "MathEngBasic/calculation.sml"
8.22
8.23 ML_file "Specify/formalise.sml"
8.24 @@ -254,7 +254,7 @@
8.25
8.26 ML_file "Interpret/istate.sml"
8.27 ML_file "Interpret/sub-problem.sml"
8.28 -(*ML_file "Interpret/error-pattern.sml" TOODOO.1 loops with real_unary_minus *)
8.29 + ML_file "Interpret/error-pattern.sml"
8.30 ML_file "Interpret/li-tool.sml"
8.31 ML_file "Interpret/lucas-interpreter.sml"
8.32 ML_file "Interpret/step-solve.sml"
8.33 @@ -272,7 +272,7 @@
8.34 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
8.35 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
8.36 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009- 2*)
8.37 -(*ML_file "BridgeLibisabelle/interface.sml" TOODOO.1 loops with real_unary_minus *)
8.38 + ML_file "BridgeLibisabelle/interface.sml"
8.39 ML_file "BridgeJEdit/parseC.sml"
8.40 ML_file "BridgeJEdit/preliminary.sml"
8.41
8.42 @@ -290,7 +290,7 @@
8.43
8.44 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
8.45 (*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*)
8.46 -(*ML_file "Knowledge/rootrat.sml" TOODOO.1 error inherited from root.sml*)
8.47 + ML_file "Knowledge/rootrat.sml"
8.48 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
8.49 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
8.50 (*ML_file "Knowledge/polyeq-1.sml" TOODOO.1 error inherited from root.sml*)
8.51 @@ -302,7 +302,7 @@
8.52 ML_file "Knowledge/diff.sml"
8.53 ML_file "Knowledge/integrate.sml"
8.54 ML_file "Knowledge/eqsystem-1.sml"
8.55 - ML_file "Knowledge/eqsystem-2.sml"
8.56 +(*ML_file "Knowledge/eqsystem-2.sml" broken by 8e46f61fdb15 *)
8.57 ML_file "Knowledge/test.sml"
8.58 ML_file "Knowledge/polyminus.sml"
8.59 ML_file "Knowledge/vect.sml"
9.1 --- a/test/Tools/isac/Test_Some.thy Sat Aug 21 18:58:33 2021 +0200
9.2 +++ b/test/Tools/isac/Test_Some.thy Sun Aug 22 09:43:43 2021 +0200
9.3 @@ -111,718 +111,1653 @@
9.4 \<close> ML \<open>
9.5 \<close>
9.6
9.7 -(*ML_file "MathEngBasic/rewrite.sml" TOODOO.1 loops with real_unary_minus *)
9.8 -section \<open>======== check test/../rewrite.sml ===============================================\<close>
9.9 ML \<open>
9.10 +val thy = @{theory}; Rewrite.trace_on := false; (**)
9.11 +\<close>
9.12 +(* ML_file "Knowledge/polyeq-1.sml" TOODOO.1 error inherited from root.sml*)
9.13 +section \<open>======== check test/../polyeq-1.sml ===============================================\<close>
9.14 +ML \<open>
9.15 +val thy = @{theory};
9.16 \<close> ML \<open>
9.17 -(* Title: "MathEngBasic/rewrite.sml"
9.18 - Author: Walther Neuper 050908
9.19 - (c) copyright due to lincense terms.
9.20 +(* Title: Knowledge/polyeq-1.sml
9.21 + testexamples for PolyEq, poynomial equations and equational systems
9.22 + Author: Richard Lang 2003
9.23 + (c) due to copyright terms
9.24 +WN030609: some expls dont work due to unfinished handling of 'expanded terms';
9.25 + others marked with TODO have to be checked, too.
9.26 *)
9.27
9.28 -"-----------------------------------------------------------------------------------------------";
9.29 -"table of contents -----------------------------------------------------------------------------";
9.30 -"-----------------------------------------------------------------------------------------------";
9.31 -"----------- assemble rewrite ------------------------------------------------------------------";
9.32 -"----------- test rewriting without Isac's thys ------------------------------------------------";
9.33 -"----------- test rewriting without Isac's thys, ~~~~~ fun rewrite_ ----------------------------";
9.34 -"----------- conditional rewriting without Isac's thys -----------------------------------------";
9.35 -"----------- conditional rewriting without Isac's thys, ~~~~~ fun ------------------------------";
9.36 -"----------- conditional rewriting creating an assumption---------------------------------------";
9.37 -"----------- step through 'and rew_sub': -------------------------------------------------------";
9.38 -"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
9.39 -"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
9.40 -"----------- check diff 2002--2009-3 -----------------------------------------------------------";
9.41 -"----------- compare all prepat's existing 2010 ------------------------------------------------";
9.42 -"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
9.43 -"----------- 2011 thms with axclasses ----------------------------------------------------------";
9.44 -"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
9.45 -"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
9.46 -"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
9.47 -"-----------------------------------------------------------------------------------------------";
9.48 -"-----------------------------------------------------------------------------------------------";
9.49 -"-----------------------------------------------------------------------------------------------";
9.50 +"-----------------------------------------------------------------";
9.51 +"table of contents -----------------------------------------------";
9.52 +"-----------------------------------------------------------------";
9.53 +"------ polyeq- 1.sml ---------------------------------------------";
9.54 +"----------- tests on predicates in problems ---------------------";
9.55 +"----------- test matching problems ------------------------------";
9.56 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
9.57 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
9.58 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
9.59 +"----------- lin.eq degree_0 -------------------------------------";
9.60 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
9.61 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
9.62 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
9.63 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
9.64 +"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
9.65 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
9.66 +"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
9.67 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
9.68 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
9.69 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
9.70 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
9.71 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
9.72 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
9.73 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
9.74 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
9.75 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
9.76 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
9.77 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
9.78 +"-----------------------------------------------------------------";
9.79 +"------ polyeq- 2.sml ---------------------------------------------";
9.80 +"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
9.81 +"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
9.82 +"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
9.83 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
9.84 +"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
9.85 +"----------- rls make_polynomial_in ------------------------------";
9.86 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
9.87 +"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
9.88 +"-----------------------------------------------------------------";
9.89 +"-----------------------------------------------------------------";
9.90
9.91 +"----------- tests on predicates in problems ---------------------";
9.92 +"----------- tests on predicates in problems ---------------------";
9.93 +"----------- tests on predicates in problems ---------------------";
9.94 +val thy = @{theory};
9.95 +Rewrite.trace_on:=false; (*true false*)
9.96
9.97 -"----------- assemble rewrite ------------------------------------------------------------------";
9.98 -"----------- assemble rewrite ------------------------------------------------------------------";
9.99 -"----------- assemble rewrite ------------------------------------------------------------------";
9.100 -"===== rewriting by thm with 'a";
9.101 -(*show_types := true;*)
9.102 + val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
9.103 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
9.104 + if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
9.105 + else error "polyeq.sml: diff.behav. in lhs";
9.106
9.107 -val thy = @{theory Complex_Main};
9.108 -val ctxt = @{context};
9.109 -val thm = @{thm add.commute};
9.110 -val t = (Thm.term_of o the) (TermC.parse thy "((r + u) + t) + s");
9.111 -"----- from old: fun rewrite__";
9.112 -val bdv = [];
9.113 -val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm));
9.114 -"----- from old: and rew_sub";
9.115 -val (LHS,RHS) = (dest_equals o strip_trueprop
9.116 - o Logic.strip_imp_concl) r;
9.117 -(* old
9.118 -val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
9.119 -"----- fun match_rew in Pure/pattern.ML";
9.120 -val rtm = the_default RHS (Term.rename_abs LHS t RHS);
9.121 + val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
9.122 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
9.123 + if (UnparseC.term t) = "True" then ()
9.124 + else error "polyeq.sml: diff.behav. 1 in is_expended_in";
9.125
9.126 -writeln(Syntax.string_of_term ctxt rtm);
9.127 -writeln(Syntax.string_of_term ctxt LHS);
9.128 -writeln(Syntax.string_of_term ctxt t);
9.129 + val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
9.130 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
9.131 + if (UnparseC.term t) = "False" then ()
9.132 + else error "polyeq.sml: diff.behav. 2 in is_poly_in";
9.133
9.134 -(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
9.135 -val (rew, RHS) = (Envir.subst_term
9.136 - (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
9.137 -(*lookup in isabelle?trace?response...*)
9.138 -writeln(Syntax.string_of_term ctxt rew);
9.139 -writeln(Syntax.string_of_term ctxt RHS);
9.140 -"===== rewriting: prep insertion into rew_sub";
9.141 -val thy = @{theory Complex_Main};
9.142 -val ctxt = @{context};
9.143 -val thm = @{thm nonzero_divide_mult_cancel_right};
9.144 -val r = Thm.prop_of thm;
9.145 -val tm = @{term "x / (2 * x)::real"};
9.146 -"----- and rew_sub";
9.147 -val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
9.148 - o Logic.strip_imp_concl) r;
9.149 -val r' = Envir.subst_term (Pattern.match thy (LHS, tm)
9.150 - (Vartab.empty, Vartab.empty)) r;
9.151 -val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
9.152 -val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
9.153 - o Logic.strip_imp_concl) r';
9.154 + val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
9.155 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
9.156 + if (UnparseC.term t) = "True" then ()
9.157 + else error "polyeq.sml: diff.behav. 3 in is_poly_in";
9.158
9.159 -(*is displayed on top of <response> buffer...*)
9.160 -Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
9.161 -Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
9.162 -(**)
9.163 + val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
9.164 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
9.165 + if (UnparseC.term t) = "True" then ()
9.166 + else error "polyeq.sml: diff.behav. 4 in is_expended_in";
9.167
9.168 -"----------- test rewriting without Isac's thys ------------------------------------------------";
9.169 -"----------- test rewriting without Isac's thys ------------------------------------------------";
9.170 -"----------- test rewriting without Isac's thys ------------------------------------------------";
9.171 + val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
9.172 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
9.173 + if (UnparseC.term t) = "True" then ()
9.174 + else error "polyeq.sml: diff.behav. 5 in is_expended_in";
9.175 +
9.176 + val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
9.177 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
9.178 + if (UnparseC.term t) = "True" then ()
9.179 + else error "polyeq.sml: diff.behav. in has_degree_in_in";
9.180
9.181 -"===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
9.182 -val thy = @{theory Complex_Main};
9.183 -val ctxt = @{context};
9.184 -val thm = @{thm add.commute};
9.185 -val tm = @{term "x + y*z::real"};
9.186 + val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
9.187 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
9.188 + if (UnparseC.term t) = "False" then ()
9.189 + else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
9.190
9.191 -val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
9.192 -(*is displayed on _TOP_ of <response> buffer...*)
9.193 -Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
9.194 -if r = @{term "y*z + x::real"}
9.195 -then () else error "rewrite.sml diff.result in rewriting";
9.196 + val t4 = (Thm.term_of o the o (TermC.parse thy))
9.197 + "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
9.198 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
9.199 + if (UnparseC.term t) = "False" then ()
9.200 + else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
9.201
9.202 -"----- rewriting a subterm";
9.203 -val tm = @{term "w*(x + y*z)::real"};
9.204 -
9.205 -val SOME (r, _) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
9.206 -
9.207 -"----- ordered rewriting";
9.208 -fun tord (_:subst) pp = LibraryC.termless pp;
9.209 -if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
9.210 -else error "rewrite.sml diff.behav. in ord.rewr.";
9.211 -
9.212 -val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm);
9.213 -(*is displayed on _TOP_ of <response> buffer...*)
9.214 -Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
9.215 -
9.216 -val tm = @{term "x*y + z::real"};
9.217 -val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm);
9.218 -
9.219 -
9.220 -"----------- conditional rewriting without Isac's thys -----------------------------------------";
9.221 -"----------- conditional rewriting without Isac's thys -----------------------------------------";
9.222 -"----------- conditional rewriting without Isac's thys -----------------------------------------";
9.223 -"===== prepr cond.rew. with Pattern.match";
9.224 -val thy = @{theory Complex_Main};
9.225 -val ctxt = @{context};
9.226 -val thm = @{thm nonzero_divide_mult_cancel_right}; (* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a":*)
9.227 -val rule = Thm.prop_of thm;
9.228 -val tm = @{term "x / (2 * x)::real"};
9.229 -val prem = Logic.strip_imp_prems rule;
9.230 -val nps = Logic.count_prems rule;
9.231 -val prems = Logic.strip_prems (nps, [], rule);
9.232 -
9.233 -val eq = Logic.strip_imp_concl rule;
9.234 -val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
9.235 -
9.236 -val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
9.237 -val rule' = Envir.subst_term mtcs rule;
9.238 -
9.239 -val prems' = (fst o Logic.strip_prems) (Logic.count_prems rule', [], rule');
9.240 -val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) rule';
9.241 -
9.242 -(rule' |> UnparseC.term) = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
9.243 - rule';
9.244 -
9.245 -(rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
9.246 - rule' |> Logic.strip_imp_concl;
9.247 -
9.248 -(rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
9.249 - rule' |> Logic.strip_imp_concl;
9.250 -
9.251 -
9.252 -"----------- conditional rewriting creating an assumption---------------------------------------";
9.253 -"----------- conditional rewriting creating an assumption---------------------------------------";
9.254 -"----------- conditional rewriting creating an assumption---------------------------------------";
9.255 -val thm = @{thm nonzero_divide_mult_cancel_right};
9.256 -val tm = @{term "x / (2 * x)::real"};
9.257 -
9.258 -val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
9.259 -
9.260 -if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
9.261 -else error "rewrite.sml diff.result in cond.rew.";
9.262 -
9.263 -if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
9.264 -then () else error "rewrite.sml diff.asm in cond.rew.";
9.265 -"----- conditional rewriting immediately: can only be done with ";
9.266 -"------Isabelle numerals, because erls cannot handle them yet.";
9.267 -
9.268 -
9.269 -"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
9.270 -"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
9.271 -"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
9.272 -val thm = @{thm nonzero_divide_mult_cancel_right};(* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a"*)
9.273 -val tm = @{term "x / (2 * x)::real"};
9.274 -val erls = eval_rls;
9.275 -
9.276 -(**)val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
9.277 -(** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
9.278 - dest_Trueprop
9.279 - ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
9.280 -"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
9.281 - (thy, dummy_ord, erls, false, thm, tm);
9.282 -"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
9.283 - (thy, 1, []: (term * term) list, rew_ord, erls, bool, thm, term);
9.284 -
9.285 -(**) val (t', asms, _(*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
9.286 - (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;
9.287 -(** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
9.288 - dest_Trueprop
9.289 - ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
9.290 -"~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
9.291 - (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
9.292 - (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);
9.293 -(*+*)UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
9.294 -
9.295 - val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r;
9.296 -(*+*)(UnparseC.term lhs, UnparseC.term rhs) = ("?b / (?a * ?b)", "(1::?'a) / ?a");
9.297 - val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
9.298 - handle Pattern.MATCH => raise NO_REWRITE;
9.299 - val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'));
9.300 -(*+*)UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
9.301 -(*+*)r';
9.302 - val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
9.303 - val _ = trace_in2 i "eval asms" thy r';
9.304 - val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls;
9.305 - (*if*) nofalse (*then*);
9.306 - val (t'', p'') = (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'));
9.307 -(*## asms accepted: [x \<noteq> 0] stored: [x \<noteq> 0] *)
9.308 -
9.309 -(*+*)if (UnparseC.term t'', map UnparseC.term p'') = ("1 / 2", ["x \<noteq> 0"]) then ()
9.310 -(*+*)else error "conditional rewriting x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2 CHANGED";
9.311 -
9.312 -
9.313 -"----------- step through 'and rew_sub': ----------------";
9.314 -"----------- step through 'and rew_sub': ----------------";
9.315 -"----------- step through 'and rew_sub': ----------------";
9.316 -(*and make asms without Trueprop, beginning with the result:*)
9.317 -val tm = @{term "x / (2 * x)::real"};
9.318 -val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
9.319 -(*show_types := false;*)
9.320 -"----- evaluate arguments";
9.321 -val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
9.322 - (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
9.323 -"----- step 1: LHS, RHS of rule";
9.324 - val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
9.325 - o Logic.strip_imp_concl) r;
9.326 -UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
9.327 -UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term RHS = "(1::?'a) / ?a";
9.328 -"----- step 2: the rule instantiated";
9.329 - val r' = Envir.subst_term
9.330 - (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
9.331 -UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
9.332 -"----- step 3: get the (instantiated) assumption(s)";
9.333 - val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
9.334 -UnparseC.term (hd p') = "x \<noteq> 0";
9.335 -"=====vvv make asms without Trueprop ---vvv";
9.336 - val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
9.337 - (Logic.count_prems r', [], r'));
9.338 -case p' of
9.339 - [Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _)
9.340 - $ Free ("x", _) $ Const (\<^const_name>\<open>zero_class.zero\<close>, _))] => ()
9.341 - | _ => error "rewrite.sml assumption changed";
9.342 -"===== \<up> make asms without Trueprop --- \<up> ";
9.343 -"----- step 4: get the (instantiated) RHS";
9.344 - val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
9.345 - o Logic.strip_imp_concl) r';
9.346 -UnparseC.term t' = "1 / 2";
9.347 -
9.348 -"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
9.349 -"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
9.350 -"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
9.351 -"----- step 0: args for rewrite_terms_, local fun";
9.352 -val (thy, ord, erls, equs, t) =
9.353 - (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [TermC.str2term "x = 0"],
9.354 - TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
9.355 -"----- step 1: args for rew_";
9.356 -val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
9.357 -"----- step 2: rew_sub";
9.358 -rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
9.359 -"----- step 3: step through rew_sub -- inefficient: goes into subterms";
9.360 -
9.361 -
9.362 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
9.363 -writeln "---------- rewrite_terms_ 1---------------------------";
9.364 -if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
9.365 -else error "rewrite.sml rewrite_terms_ [x = 0]";
9.366 -
9.367 -val equs = [TermC.str2term "M_b 0 = 0"];
9.368 -val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
9.369 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
9.370 -writeln "---------- rewrite_terms_ 2---------------------------";
9.371 -if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
9.372 -else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
9.373 -
9.374 -val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
9.375 -val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
9.376 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
9.377 -writeln "---------- rewrite_terms_ 3---------------------------";
9.378 -if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
9.379 -else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
9.380 -
9.381 -
9.382 -"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
9.383 -"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
9.384 -"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
9.385 -(*see smltest/Scripts/term_G.sml: inst_bdv 2*)
9.386 -val t = TermC.str2term"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";
9.387 -val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
9.388 - (TermC.str2term"bdv_2",TermC.str2term"c_2"),
9.389 - (TermC.str2term"bdv_3",TermC.str2term"c_3"),
9.390 - (TermC.str2term"bdv_4",TermC.str2term"c_4")];
9.391 -(*------------ outcommented WN071210, after inclusion into ROOT.ML
9.392 -val SOME (t,_) =
9.393 - rewrite_inst_ thy e_rew_ord
9.394 - (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
9.395 - [(Eval ("EqSystem.occur_exactly_in",
9.396 - eval_occur_exactly_in
9.397 - "#eval_occur_exactly_in_"))
9.398 - ])
9.399 - false bdvs (ThmC.numerals_to_Free @{separate_bdvs_add) t;
9.400 -(writeln o UnparseC.term) t;
9.401 -if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L \<up> 2) / 2)"
9.402 -then () else error "rewrite.sml rewrite_inst_ bdvs";
9.403 -> Rewrite.trace_on:=true;false
9.404 -Rewrite.trace_on:=false;--------------------------------------------*)
9.405 -
9.406 -
9.407 -"----------- compare all prepat's existing 2010 ------------------------------------------------";
9.408 -"----------- compare all prepat's existing 2010 ------------------------------------------------";
9.409 -"----------- compare all prepat's existing 2010 ------------------------------------------------";
9.410 -val thy = @{theory "Isac_Knowledge"};
9.411 -val t = @{term "a + b * x = (0 ::real)"};
9.412 -val pat = TermC.parse_patt thy "?l = (?r ::real)";
9.413 -val precond = TermC.parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
9.414 -val precond = TermC.parse_patt thy "(?l::real) is_expanded";
9.415 -
9.416 -val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
9.417 -val preinst = Envir.subst_term inst precond;
9.418 -UnparseC.term preinst;
9.419 -
9.420 -"===== Rational.thy: cancel ===";
9.421 -(* pat matched with the current term gives an environment
9.422 - (or not: hen the Rrls not applied);
9.423 - if pre1 and pre2 evaluate to @{term True} in this environment,
9.424 - then the Rrls is applied. *)
9.425 -val t = TermC.str2term "(a + b) / c ::real";
9.426 -val pat = TermC.parse_patt thy "?r / ?s ::real";
9.427 -val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"];
9.428 -val prepat = [(pres, pat)];
9.429 -val erls = rational_erls;
9.430 -(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
9.431 -
9.432 -val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
9.433 -val asms = map (Envir.subst_term subst) pres;
9.434 -if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
9.435 -then () else error "rewrite.sml: prepat cancel subst";
9.436 -
9.437 -if ([], true) = eval__true thy 0 asms [] erls
9.438 -then () else error "rewrite.sml: prepat cancel eval__true";
9.439 -
9.440 -"===== Rational.thy: add_fractions_p ===";
9.441 -(* if each pat* TermC.matches with the current term, the Rrls is applied
9.442 - (there are no preconditions to be checked, they are @{term True}) *)
9.443 -val t = TermC.str2term "a / b + 1 / 2";
9.444 -val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";
9.445 -val pres = [@{term True}];
9.446 -val prepat = [(pres, pat)];
9.447 -val erls = rational_erls;
9.448 -(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
9.449 -
9.450 -val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
9.451 -if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
9.452 -then () else error "rewrite.sml: prepat add_fractions_p";
9.453 -
9.454 -"===== Poly.thy: order_mult_ ===";
9.455 - (* ?p matched with the current term gives an environment,
9.456 - which evaluates (the instantiated) "p is_multUnordered" to true*)
9.457 -val t = TermC.str2term "x \<up> 2 * x";
9.458 -val pat = TermC.parse_patt thy "?p :: real"
9.459 -val pres = [TermC.parse_patt thy "?p is_multUnordered"];
9.460 -val prepat = [(pres, pat)];
9.461 -val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
9.462 - [Eval ("Poly.is_multUnordered",
9.463 - eval_is_multUnordered "")];
9.464 -
9.465 -val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
9.466 -val asms = map (Envir.subst_term subst) pres;
9.467 -if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
9.468 -then () else error "rewrite.sml: prepat order_mult_ subst";
9.469 -
9.470 -if ([], true) = eval__true thy 0 asms [] erls
9.471 -then () else error "rewrite.sml: prepat order_mult_ eval__true";
9.472 -
9.473 +val t5 = (Thm.term_of o the o (TermC.parse thy))
9.474 + "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
9.475 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
9.476 + if (UnparseC.term t) = "True" then ()
9.477 + else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
9.478
9.479 \<close> ML \<open>
9.480 -"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
9.481 -"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
9.482 -"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
9.483 -val t = TermC.str2term "x \<up> 2 * x";
9.484 +"----------- test matching problems --------------------------0---";
9.485 +"----------- test matching problems --------------------------0---";
9.486 +"----------- test matching problems --------------------------0---";
9.487 +val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.488 +if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
9.489 + M_Match.Matches' {Find = [Correct "solutions L"],
9.490 + With = [],
9.491 + Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
9.492 + Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
9.493 + Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
9.494 + Relate = []}
9.495 +then () else error "M_Match.match_pbl [expanded,univariate,equation]";
9.496
9.497 -if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
9.498 -val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
9.499 +if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
9.500 + M_Match.Matches' {Find = [Correct "solutions L"],
9.501 + With = [],
9.502 + Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
9.503 + Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
9.504 + Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
9.505 +then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
9.506
9.507 -(*+*)case eval_is_multUnordered "testid" "" tm thy of
9.508 -(*+*) SOME
9.509 -(*+*) ("testidx \<up> 2 * x_",
9.510 -(*+*) Const (\<^const_name>\<open>Trueprop\<close>, _) $
9.511 -(*+*) (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
9.512 -(*+*) (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $
9.513 -(*+*) (Const (\<^const_name>\<open>times\<close>, _) $
9.514 -(*+*) (Const (\<^const_name>\<open>powr\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
9.515 -(*+*) Const (\<^const_name>\<open>True\<close>, _))) => ()
9.516 -(*+*)(* ^^^^^^ compare ---vvv *)
9.517 -(*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
9.518 -
9.519 -
9.520 - eval_is_multUnordered "testid" "" tm thy;
9.521 -
9.522 -case eval_is_multUnordered "testid" "" tm thy of
9.523 - SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
9.524 - (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
9.525 - (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
9.526 - Const (\<^const_name>\<open>True\<close>, _))) => ()
9.527 - | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
9.528 -
9.529 -tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
9.530 -val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
9.531 -tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
9.532 -if UnparseC.term t' = "x * x \<up> 2" then ()
9.533 -else error "rewrite.sml Poly.is_multUnordered doesn't work";
9.534 -
9.535 -(* for achieving the previous result, the following code was taken apart *)
9.536 -"----- rewrite__set_ ---";
9.537 -val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
9.538 - val (t', asm, rew) = app_rev thy (i+1) rrls t;
9.539 -"----- app_rev ---";
9.540 -val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
9.541 - fun chk_prepat thy erls [] t = true
9.542 - | chk_prepat thy erls prepat t =
9.543 - let fun chk (pres, pat) =
9.544 - (let val subst: Type.tyenv * Envir.tenv =
9.545 - Pattern.match thy (pat, t)
9.546 - (Vartab.empty, Vartab.empty)
9.547 - in snd (eval__true thy (i+1)
9.548 - (map (Envir.subst_term subst) pres)
9.549 - [] erls)
9.550 - end)
9.551 - handle Pattern.MATCH => false
9.552 - fun scan_ f [] = false (*scan_ NEVER called by []*)
9.553 - | scan_ f (pp::pps) = if f pp then true
9.554 - else scan_ f pps;
9.555 - in scan_ chk prepat end;
9.556 -
9.557 - (*.apply the normal_form of a rev-set.*)
9.558 - fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
9.559 - if chk_prepat thy erls prepat t
9.560 - then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)
9.561 - normal_form t)
9.562 - else NONE;
9.563 -(*fixme val NONE = app_rev' thy rrls t;*)
9.564 -"----- app_rev' ---";
9.565 -val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
9.566 -(*fixme false*) chk_prepat thy erls prepat t;
9.567 -"----- chk_prepat ---";
9.568 -val (thy, erls, prepat, t) = (thy, erls, prepat, t);
9.569 - fun chk (pres, pat) =
9.570 - (let val subst: Type.tyenv * Envir.tenv =
9.571 - Pattern.match thy (pat, t)
9.572 - (Vartab.empty, Vartab.empty)
9.573 - in snd (eval__true thy (i+1)
9.574 - (map (Envir.subst_term subst) pres)
9.575 - [] erls)
9.576 - end)
9.577 - handle Pattern.MATCH => false;
9.578 - fun scan_ _ [] = false (*scan_ NEVER called by []*)
9.579 - | scan_ f (pp::pps) = if f pp then true
9.580 - else scan_ f pps;
9.581 -tracing "=== poly.sml: scan_ chk prepat begin";
9.582 -scan_ chk prepat;
9.583 -tracing "=== poly.sml: scan_ chk prepat end";
9.584 -
9.585 -"----- chk ---";
9.586 -(*reestablish...*) val t = TermC.str2term "x \<up> 2 * x";
9.587 -val [(pres, pat)] = prepat;
9.588 - val subst: Type.tyenv * Envir.tenv =
9.589 - Pattern.match thy (pat, t)
9.590 - (Vartab.empty, Vartab.empty);
9.591 -
9.592 -(*fixme: asms = ["p is_multUnordered"]...instantiate*)
9.593 -"----- eval__true ---";
9.594 -val asms = (map (Envir.subst_term subst) pres);
9.595 -if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then ()
9.596 -else error "rewrite.sml: diff. is_multUnordered, asms";
9.597 -val (thy, i, asms, bdv, rls) =
9.598 - (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"],
9.599 - [] : (term * term) list, erls);
9.600 -case eval__true thy i asms bdv rls of
9.601 - ([], true) => ()
9.602 - | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
9.603
9.604 \<close> ML \<open>
9.605 -"----------- 2011 thms with axclasses ----------------------------------------------------------";
9.606 -"----------- 2011 thms with axclasses ----------------------------------------------------------";
9.607 -"----------- 2011 thms with axclasses ----------------------------------------------------------";
9.608 -val thm = @{thm div_by_1};
9.609 -val prop = Thm.prop_of thm;
9.610 -TermC.atomty prop; (*Type 'a*)
9.611 -val t = TermC.str2term "(2*x)/1"; (*Type real*)
9.612 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
9.613 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
9.614 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
9.615 +(*##################################################################################
9.616 +----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
9.617 +
9.618 + (*Aufgabe zum Einstieg in die Arbeit...*)
9.619 + val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
9.620 + (*ein 'ruleset' aus Poly.ML wird angewandt...*)
9.621 + val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
9.622 + UnparseC.term t;
9.623 + "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";
9.624 + val SOME (t,_) =
9.625 + rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
9.626 + UnparseC.term t;
9.627 + "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
9.628 +(* bei Verwendung von "size_of-term" nach MG :*)
9.629 +(*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *)
9.630 +
9.631 + (*wir holen 'a' wieder aus der Klammerung heraus...*)
9.632 + val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
9.633 + UnparseC.term t;
9.634 + "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
9.635 +(* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)
9.636 +
9.637 + val SOME (t,_) =
9.638 + rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
9.639 + UnparseC.term t;
9.640 + "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
9.641 + (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
9.642 + "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
9.643 +
9.644 + (*das rewriting l"asst sich beobachten mit
9.645 +Rewrite.trace_on := false; (*true false*)
9.646 + *)
9.647 +
9.648 +"------ 15.11.02 --------------------------";
9.649 + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
9.650 + val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
9.651 + val a = (Thm.term_of o the o (TermC.parse thy)) "a";
9.652 +
9.653 +Rewrite.trace_on := false; (*true false*)
9.654 + (* Anwenden einer Regelmenge aus Termorder.ML: *)
9.655 + val SOME (t,_) =
9.656 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
9.657 + UnparseC.term t;
9.658 + val SOME (t,_) =
9.659 + rewrite_set_ thy false discard_parentheses t;
9.660 + UnparseC.term t;
9.661 +"1 + b * x + x * a";
9.662 +
9.663 + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
9.664 + val SOME (t,_) =
9.665 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
9.666 + UnparseC.term t;
9.667 + val SOME (t,_) =
9.668 + rewrite_set_ thy false discard_parentheses t;
9.669 + UnparseC.term t;
9.670 +"1 + (x + b * x) * a + a \<up> 2";
9.671 +
9.672 + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
9.673 + val SOME (t,_) =
9.674 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
9.675 + UnparseC.term t;
9.676 + val SOME (t,_) =
9.677 + rewrite_set_ thy false discard_parentheses t;
9.678 + UnparseC.term t;
9.679 +"1 + b * a + (7 + x) * a \<up> 2";
9.680 +
9.681 +(* MG2003
9.682 + Prog_Expr.thy grundlegende Algebra
9.683 + Poly.thy Polynome
9.684 + Rational.thy Br"uche
9.685 + Root.thy Wurzeln
9.686 + RootRat.thy Wurzen + Br"uche
9.687 + Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
9.688 +
9.689 + get_thm Termorder.thy "bdv_n_collect";
9.690 + get_thm (theory "Isac_Knowledge") "bdv_n_collect";
9.691 +*)
9.692 + val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
9.693 + val SOME (t,_) =
9.694 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
9.695 + UnparseC.term t;
9.696 + val SOME (t,_) =
9.697 + rewrite_set_ thy false discard_parentheses t;
9.698 + UnparseC.term t;
9.699 +"(7 + x) * a \<up> 2";
9.700 +
9.701 + val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
9.702 +
9.703 + val t = (Thm.term_of o the o (parseold thy)) "7";
9.704 +##################################################################################*)
9.705 +
9.706
9.707 \<close> ML \<open>
9.708 -val (thy, ro, er, inst) =
9.709 - (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
9.710 -val SOME (t, _) = rewrite_ thy ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)
9.711 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
9.712 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
9.713 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
9.714 +(* termorder hacked by MG, adapted later by WN *)
9.715 +(** )local ( *. for make_polynomial_in .*)
9.716
9.717 -"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
9.718 -"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
9.719 -"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
9.720 -val thy = @{theory RatEq};
9.721 -val ctxt = Proof_Context.init_global thy;
9.722 -val SOME t = parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
9.723 -val rls = assoc_rls "RatEq_eliminate"
9.724 +open Term; (* for type order = EQUAL | LESS | GREATER *)
9.725 +
9.726 +fun pr_ord EQUAL = "EQUAL"
9.727 + | pr_ord LESS = "LESS"
9.728 + | pr_ord GREATER = "GREATER";
9.729 +
9.730 +fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
9.731 + | dest_hd' x (t as Free (a, T)) =
9.732 + if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
9.733 + else (((a, 0), T), 1)
9.734 + | dest_hd' _ (Var v) = (v, 2)
9.735 + | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
9.736 + | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
9.737 + | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
9.738 +
9.739 +fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
9.740 + Free (var, _) $ Free (pot, _)) =
9.741 + (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
9.742 + case x of (*WN*)
9.743 + (Free (xstr, _)) =>
9.744 + if xstr = var
9.745 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
9.746 + 1000 * (the (TermC.int_opt_of_string pot)))
9.747 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
9.748 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
9.749 + | size_of_term' i pr x (t as Abs (_, _, body)) =
9.750 + (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
9.751 + 1 + size_of_term' (i + 1) pr x body)
9.752 + | size_of_term' i pr x (f $ t) =
9.753 + let
9.754 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
9.755 + val s1 = size_of_term' (i + 1) pr x f
9.756 + val s2 = size_of_term' (i + 1) pr x t
9.757 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
9.758 + in (s1 + s2) end
9.759 + | size_of_term' i pr x t =
9.760 + (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
9.761 + case t of
9.762 + Free (subst, _) =>
9.763 + (case x of
9.764 + Free (xstr, _) =>
9.765 + if xstr = subst
9.766 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
9.767 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
9.768 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
9.769 + | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
9.770 +
9.771 +fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
9.772 + let
9.773 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
9.774 + val ord =
9.775 + case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
9.776 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
9.777 + in ord end
9.778 + | term_ord' i pr x _ (t, u) =
9.779 + let
9.780 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
9.781 + val ord =
9.782 + case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
9.783 + EQUAL =>
9.784 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u
9.785 + in
9.786 + (case hd_ord (i + 1) pr x (f, g) of
9.787 + EQUAL => (terms_ord x (i + 1) pr) (ts, us)
9.788 + | ord => ord)
9.789 + end
9.790 + | ord => ord
9.791 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
9.792 + in ord end
9.793 +and hd_ord i pr x (f, g) = (* ~ term.ML *)
9.794 + let
9.795 + val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
9.796 + val ord = prod_ord
9.797 + (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
9.798 + (dest_hd' x f, dest_hd' x g)
9.799 + val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
9.800 + in ord end
9.801 +and terms_ord x i pr (ts, us) =
9.802 + let
9.803 + val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
9.804 + val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
9.805 + val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
9.806 + in ord end
9.807 +
9.808 +(** )in( *local*)
9.809 +
9.810 +fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
9.811 + ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
9.812 + case subst of
9.813 + (_, x) :: _ =>
9.814 + term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
9.815 + | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
9.816 +
9.817 +(** )end;( *local*)
9.818 +
9.819 +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
9.820 +if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?";
9.821 +
9.822 +val x = TermC.str2term "x ::real";
9.823 +
9.824 +val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
9.825 +if 2006 = size_of_term' 1 true x t1
9.826 +then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
9.827 +
9.828 +val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
9.829 +if 3004 = size_of_term' 1 true x t2
9.830 +then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
9.831 +
9.832 +
9.833 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
9.834 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
9.835 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
9.836 + val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
9.837 + val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
9.838 + val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
9.839 +
9.840 + val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
9.841 + val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
9.842 + val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
9.843 + val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
9.844 +
9.845 +if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
9.846 +else error "termorder.sml diff.behav ord_make_polynomial_in #1";
9.847 +
9.848 +if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
9.849 +else error "termorder.sml diff.behav ord_make_polynomial_in #2";
9.850 +
9.851 +if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
9.852 +else error "termorder.sml diff.behav ord_make_polynomial_in #3";
9.853 +
9.854 + val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
9.855 + val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
9.856 + ord_make_polynomial_in true thy substx (aa, bb);
9.857 + true; (* => LESS *)
9.858 +
9.859 + val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
9.860 + val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
9.861 + ord_make_polynomial_in true thy substa (aa, bb);
9.862 + false; (* => GREATER *)
9.863 +
9.864 +(* und nach dem Re-engineering der Termorders in den 'rulesets'
9.865 + kannst Du die 'gr"osste' Variable frei w"ahlen: *)
9.866 + val bdv= TermC.str2term "bdv ::real";
9.867 + val x = TermC.str2term "x ::real";
9.868 + val a = TermC.str2term "a ::real";
9.869 + val b = TermC.str2term "b ::real";
9.870 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
9.871 +if UnparseC.term t' = "b + x + a" then ()
9.872 +else error "termorder.sml diff.behav ord_make_polynomial_in #11";
9.873 +
9.874 +val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
9.875 +
9.876 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
9.877 +if UnparseC.term t' = "a + b + x" then ()
9.878 +else error "termorder.sml diff.behav ord_make_polynomial_in #13";
9.879 +
9.880 + val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
9.881 + val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
9.882 +val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
9.883 +if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
9.884 +else error "termorder.sml diff.behav ord_make_polynomial_in #15";
9.885 +
9.886 + val ttt' = "(3*x + 5)/18 ::real";
9.887 + val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
9.888 +val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
9.889 +if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
9.890 +else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
9.891 +
9.892 +val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
9.893 +if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
9.894 +else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
9.895 +
9.896 +"----------- lin.eq degree_0 -------------------------------------";
9.897 +"----------- lin.eq degree_0 -------------------------------------";
9.898 +"----------- lin.eq degree_0 -------------------------------------";
9.899 +"----- d0_false ------";
9.900 +val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
9.901 +val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
9.902 + ["PolyEq", "solve_d0_polyeq_equation"]);
9.903 +(*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
9.904 +TODO: change to "equality (x + - 1*x = (0::real))"
9.905 + and search for an appropriate problem and method.
9.906 +
9.907 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.908 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.909 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.910 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.911 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.912 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.913 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.914 +case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
9.915 + | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
9.916 +
9.917 +"----- d0_true ------";
9.918 +val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
9.919 +val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
9.920 + ["PolyEq", "solve_d0_polyeq_equation"]);
9.921 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.922 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.923 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.924 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.925 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.926 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.927 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.928 +case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
9.929 + | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
9.930 +============ inhibit exn WN110914 ============================================*)
9.931 +
9.932 +\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
9.933 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
9.934 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
9.935 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
9.936 +"----- d2_pqformula1 ------!!!!";
9.937 +val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
9.938 +val (dI',pI',mI') =
9.939 + ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
9.940 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.941 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.942 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.943 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.944 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.945 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.946 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.947 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
9.948 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.949 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.950 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.951 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.952 +
9.953 +(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
9.954 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
9.955 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.956 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.957 +
9.958 +if p = ([], Res) andalso
9.959 + f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
9.960 + case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
9.961 +else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
9.962
9.963 \<close> ML \<open>
9.964 -Rewrite.trace_on := true; (*false true*)
9.965 -\<close> text \<open> (* GOON: TOODOO.1 loops with real_unary_minus *)
9.966 -val SOME (t''''', asm''''') =
9.967 - rewrite_set_ thy true rls t;
9.968 -\<close> text \<open>
9.969 -"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
9.970 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
9.971 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
9.972 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
9.973 +"----- d2_pqformula1_neg ------";
9.974 +val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
9.975 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
9.976 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.977 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.978 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.979 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.980 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.981 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.982 +(*### or2list False
9.983 + ([1],Res) False Or_to_List)*)
9.984 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.985 +(*### or2list False
9.986 + ([2],Res) [] Check_elementwise "Assumptions"*)
9.987 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.988 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.989 +val asm = Ctree.get_assumptions pt p;
9.990 +if f2str f = "[]" andalso
9.991 + UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
9.992 + "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
9.993 +else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
9.994 +
9.995 +\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
9.996 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
9.997 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
9.998 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
9.999 +"----- d2_pqformula2 ------";
9.1000 +val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1001 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1002 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
9.1003 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1004 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1005 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1006 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1007 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1008 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1009 +
9.1010 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1011 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1012 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1013 +case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
9.1014 + | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
9.1015 +
9.1016 +
9.1017 +\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
9.1018 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
9.1019 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
9.1020 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
9.1021 +"----- d2_pqformula3 ------";
9.1022 +(*EP-9*)
9.1023 +val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1024 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1025 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
9.1026 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1027 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1028 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1029 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1030 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1031 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1032 +
9.1033 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1034 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1035 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1036 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
9.1037 + | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
9.1038 +
9.1039 +
9.1040 +\<close> ML \<open>
9.1041 +"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
9.1042 +"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
9.1043 +"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
9.1044 +"----- d2_pqformula3_neg ------";
9.1045 +val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1046 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1047 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
9.1048 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1049 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1050 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1051 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1052 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1053 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1054 +
9.1055 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1056 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1057 +"TODO 2 + x + x \<up> 2 = 0";
9.1058 +"TODO 2 + x + x \<up> 2 = 0";
9.1059 +"TODO 2 + x + x \<up> 2 = 0";
9.1060 +
9.1061 +\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
9.1062 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
9.1063 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
9.1064 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
9.1065 +"----- d2_pqformula4 ------";
9.1066 +val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1067 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1068 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
9.1069 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1070 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1071 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1072 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1073 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1074 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1075 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1076 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1077 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1078 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
9.1079 + | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
9.1080 +
9.1081 +\<close> ML \<open>
9.1082 +"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
9.1083 +"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
9.1084 +"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
9.1085 +"----- d2_pqformula5 ------";
9.1086 +val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1087 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1088 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
9.1089 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1090 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1091 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1092 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1093 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1094 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1095 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1096 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1097 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1098 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
9.1099 + | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
9.1100 +
9.1101 +\<close> ML \<open>
9.1102 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
9.1103 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
9.1104 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
9.1105 +"----- d2_pqformula6 ------";
9.1106 +val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1107 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1108 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
9.1109 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1110 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1111 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1112 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1113 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1114 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1115 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1116 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1117 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1118 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
9.1119 + | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
9.1120 +
9.1121 +\<close> ML \<open>
9.1122 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
9.1123 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
9.1124 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
9.1125 +"----- d2_pqformula7 ------";
9.1126 +(*EP- 10*)
9.1127 +val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1128 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1129 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
9.1130 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1131 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1132 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1133 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1134 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1135 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1136 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1137 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1138 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1139 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
9.1140 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
9.1141 +
9.1142 +\<close> ML \<open>
9.1143 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
9.1144 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
9.1145 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
9.1146 +"----- d2_pqformula8 ------";
9.1147 +val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1148 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1149 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
9.1150 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1151 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1152 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1153 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1154 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1155 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1156 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1157 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1158 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1159 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
9.1160 + | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
9.1161 +
9.1162 +\<close> ML \<open>
9.1163 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
9.1164 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
9.1165 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
9.1166 +"----- d2_pqformula9 ------";
9.1167 +val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1168 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1169 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
9.1170 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1171 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1172 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1173 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1174 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1175 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1176 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1177 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1178 +case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
9.1179 + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
9.1180 +
9.1181 +
9.1182 +\<close> ML \<open>
9.1183 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
9.1184 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
9.1185 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
9.1186 +"----- d2_pqformula9_neg ------";
9.1187 +val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1188 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1189 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
9.1190 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1191 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1192 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1193 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1194 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1195 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1196 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1197 +"TODO 4 + 1*x \<up> 2 = 0";
9.1198 +"TODO 4 + 1*x \<up> 2 = 0";
9.1199 +"TODO 4 + 1*x \<up> 2 = 0";
9.1200 +
9.1201 +\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
9.1202 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
9.1203 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
9.1204 +"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
9.1205 +val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1206 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1207 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1208 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1209 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1210 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1211 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1212 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1213 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1214 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1215 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1216 +case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
9.1217 + | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
9.1218 +
9.1219 +\<close> ML \<open>
9.1220 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
9.1221 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
9.1222 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
9.1223 +val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1224 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1225 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1226 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1227 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1228 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1229 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1230 +
9.1231 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1232 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1233 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1234 +"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
9.1235 +"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
9.1236 +"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
9.1237 +
9.1238 +
9.1239 +\<close> ML \<open>
9.1240 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
9.1241 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
9.1242 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
9.1243 +(*EP- 11*)
9.1244 +val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1245 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1246 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1247 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1248 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1249 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1250 +
9.1251 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1252 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1253 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1254 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1255 +
9.1256 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1257 +case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
9.1258 + | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
9.1259 +
9.1260 +
9.1261 +\<close> ML \<open>
9.1262 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
9.1263 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
9.1264 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
9.1265 +val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1266 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1267 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1268 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1269 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1270 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1271 +
9.1272 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1273 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1274 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1275 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1276 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1277 +"TODO 1 + x + 2*x \<up> 2 = 0";
9.1278 +"TODO 1 + x + 2*x \<up> 2 = 0";
9.1279 +"TODO 1 + x + 2*x \<up> 2 = 0";
9.1280 +
9.1281 +
9.1282 +val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1283 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1284 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1285 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1286 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1287 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1288 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1289 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1290 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1291 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1292 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1293 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
9.1294 + | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
9.1295 +
9.1296 +val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1297 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1298 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1299 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1300 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1301 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1302 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1303 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1304 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1305 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1306 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1307 +"TODO 2 + 1*x + x \<up> 2 = 0";
9.1308 +"TODO 2 + 1*x + x \<up> 2 = 0";
9.1309 +"TODO 2 + 1*x + x \<up> 2 = 0";
9.1310 +
9.1311 +\<close> ML \<open>
9.1312 +(*EP- 12*)
9.1313 +val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1314 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1315 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1316 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1317 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1318 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1319 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1320 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1321 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1322 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1323 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1324 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
9.1325 + | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
9.1326 +
9.1327 +val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1328 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1329 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1330 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1331 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1332 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1333 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1334 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1335 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1336 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1337 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1338 +"TODO 2 + x + x \<up> 2 = 0";
9.1339 +"TODO 2 + x + x \<up> 2 = 0";
9.1340 +"TODO 2 + x + x \<up> 2 = 0";
9.1341 +
9.1342 +\<close> ML \<open>
9.1343 +(*EP- 13*)
9.1344 +val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1345 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1346 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1347 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1348 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1349 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1350 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1351 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1352 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1353 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1354 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1355 +case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
9.1356 + | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
9.1357 +
9.1358 +val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1359 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1360 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1361 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1362 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1363 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1364 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1365 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1366 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1367 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1368 +"TODO 8+ 2*x \<up> 2 = 0";
9.1369 +"TODO 8+ 2*x \<up> 2 = 0";
9.1370 +"TODO 8+ 2*x \<up> 2 = 0";
9.1371 +
9.1372 +\<close> ML \<open>
9.1373 +(*EP- 14*)
9.1374 +val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1375 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1376 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1377 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1378 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1379 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1380 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1381 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1382 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1383 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1384 +case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
9.1385 + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
9.1386 +
9.1387 +
9.1388 +\<close> ML \<open>
9.1389 +val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1390 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1391 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1392 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1393 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1394 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1395 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1396 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1397 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1398 +"TODO 4+ x \<up> 2 = 0";
9.1399 +"TODO 4+ x \<up> 2 = 0";
9.1400 +"TODO 4+ x \<up> 2 = 0";
9.1401 +
9.1402 +\<close> ML \<open>
9.1403 +(*EP- 15*)
9.1404 +val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1405 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1406 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1407 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1408 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1409 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1410 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1411 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1412 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1413 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1414 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1415 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
9.1416 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
9.1417 +
9.1418 +\<close> ML \<open>
9.1419 +val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.1420 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1421 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1422 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1423 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1424 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1425 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1426 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1427 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1428 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1429 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1430 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
9.1431 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
9.1432 +
9.1433 +\<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*)
9.1434 +\<close> ML \<open>
9.1435 +(*EP- 16*)
9.1436 +val fmz = ["equality (x + 2*x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"];
9.1437 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.1438 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.1439 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1440 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1441 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1442 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1443 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1444 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.1445 +\<close> ML \<open>
9.1446 +(*+*)val Test_Out.FormKF "x + 2 * x \<up> 2 = 0" = f;
9.1447 +(*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt
9.1448 +\<close> ML \<open>
9.1449 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1450 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*)
9.1451 +\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
9.1452 +\<close> ML \<open>
9.1453 + @{theory}; (*Isac_Test.Test_Some:153857*)
9.1454 +\<close> ML \<open>
9.1455 +d2_polyeq_abcFormula_simplify
9.1456 +\<close> ML \<open>
9.1457 +val t = TermC.str2term "x + 2 * x \<up> 2 = 0";
9.1458 +val subst = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
9.1459 +\<close> ML \<open>
9.1460 +val SOME (t', []) = rewrite_set_ @{theory} true d2_polyeq_abcFormula_simplify t;
9.1461 +\<close> ML \<open>
9.1462 +UnparseC.term t' = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)";
9.1463 +(* same as isabisac15 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
9.1464 +\<close> ML \<open>
9.1465 +rewrite_set_inst_ @{theory} true subst d2_polyeq_abcFormula_simplify t
9.1466 +\<close> ML \<open>
9.1467 +UnparseC.term t' = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)"
9.1468 +(* same as isabisac15 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
9.1469 +\<close> ML \<open> (*------- BUT THE ERROR COMES FROM Step.do_next WITH ANOTHER REWRITE -----------------*)
9.1470 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
9.1471 +\<close> ML \<open>
9.1472 + val (pt, p) =
9.1473 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
9.1474 + case Step.by_tactic tac (pt, p) of
9.1475 + ("ok", (_, _, ptp)) => ptp
9.1476 + | ("unsafe-ok", (_, _, ptp)) => ptp
9.1477 + | ("not-applicable",_) => (pt, p)
9.1478 + | ("end-of-calculation", (_, _, ptp)) => ptp
9.1479 + | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
9.1480 + | _ => raise ERROR "me: uncovered case Step.by_tactic"
9.1481 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1482 + (*case*)
9.1483 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
9.1484 +\<close> ML \<open>
9.1485 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
9.1486 +\<close> ML \<open>
9.1487 + (*if*) Pos.on_calc_end ip (*else*);
9.1488 +\<close> ML \<open>
9.1489 + val (_, probl_id, _) = Calc.references (pt, p);
9.1490 +\<close> ML \<open>
9.1491 +val _ =
9.1492 + (*case*) tacis (*of*);
9.1493 +\<close> ML \<open>
9.1494 + (*if*) probl_id = Problem.id_empty (*else*);
9.1495 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1496 + switch_specify_solve p_ (pt, ip);
9.1497 +\<close> ML \<open>
9.1498 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
9.1499 +\<close> ML \<open>
9.1500 + (*if*) Pos.on_specification ([], state_pos) (*else*);
9.1501 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1502 + LI.do_next (pt, input_pos)
9.1503 +\<close> ML \<open>
9.1504 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
9.1505 +\<close> ML \<open>
9.1506 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
9.1507 +\<close> ML \<open>
9.1508 + val thy' = get_obj g_domID pt (par_pblobj pt p);
9.1509 + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
9.1510 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1511 + (*case*)
9.1512 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
9.1513 +\<close> ML \<open>
9.1514 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) =
9.1515 + (sc, (pt, pos), ist, ctxt);
9.1516 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1517 + (*case*)
9.1518 + LI.scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist)
9.1519 +\<close> ML \<open>
9.1520 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) =
9.1521 + ((prog, (ptp, ctxt)), (Pstate ist));
9.1522 +\<close> ML \<open>
9.1523 + (*if*) path = [] (*else*);
9.1524 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1525 + go_scan_up (prog, cc) (trans_scan_up ist)
9.1526 +\<close> ML \<open>
9.1527 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
9.1528 + ((prog, cc), (trans_scan_up ist));
9.1529 +\<close> ML \<open>
9.1530 + (*if*) path = [R] (*else*);
9.1531 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1532 + scan_up pcc (ist |> path_up) (go_up path sc)
9.1533 +\<close> ML \<open>
9.1534 +"~~~~~ and scan_up , args:"; val (pcc, ist,(Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ _ )) =
9.1535 + (pcc, (ist |> path_up), (go_up path sc));
9.1536 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1537 + go_scan_up pcc ist
9.1538 +\<close> ML \<open>
9.1539 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
9.1540 + (pcc, ist);
9.1541 +\<close> ML \<open>
9.1542 + (*if*) path = [R] (*else*);
9.1543 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1544 + scan_up pcc (ist |> path_up) (go_up path sc)
9.1545 +\<close> ML \<open>
9.1546 +"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _)) =
9.1547 + (pcc, (ist |> path_up), (go_up path sc));
9.1548 +\<close> ML \<open>
9.1549 + val e2 = check_Seq_up ist sc;
9.1550 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1551 + (*case*)
9.1552 + scan_dn cc (ist |> path_up_down [R]) e2 (*of*);
9.1553 +\<close> ML \<open>
9.1554 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ e1 $ e2)) =
9.1555 + (cc, (ist |> path_up_down [R]), e2);
9.1556 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1557 + (*case*)
9.1558 + scan_dn cc (ist |> path_down [L, R]) e1 (*of*);
9.1559 +\<close> ML \<open>
9.1560 +"~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e)) =
9.1561 + (cc, (ist |> path_down [L, R]), e1);
9.1562 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1563 + (*case*)
9.1564 + scan_dn cc (ist |> path_down [R]) e (*of*);
9.1565 +\<close> ML \<open>
9.1566 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) =
9.1567 + (cc, (ist |> path_down [R]), e);
9.1568 +\<close> ML \<open>
9.1569 + (*if*) Tactical.contained_in t (*else*);
9.1570 +\<close> ML \<open>
9.1571 +val (Program.Tac prog_tac, form_arg) = (*case*)
9.1572 + LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
9.1573 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1574 + check_tac cc ist (prog_tac, form_arg)
9.1575 +\<close> ML \<open>
9.1576 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) =
9.1577 + (cc, ist, (prog_tac, form_arg));
9.1578 +\<close> ML \<open>
9.1579 + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
9.1580 +\<close> ML \<open>
9.1581 +val _ = (*case*) m (*of*);
9.1582 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1583 + (*case*)
9.1584 +Solve_Step.check m (pt, p) (*of*);
9.1585 +\<close> ML \<open>
9.1586 +"~~~~~ fun check , args:"; val ((Tactic.Rewrite_Set rls), (cs as (pt, (p, _)))) =
9.1587 + (m, (pt, p));
9.1588 +\<close> ML \<open>
9.1589 + val pp = Ctree.par_pblobj pt p;
9.1590 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
9.1591 + val f = Calc.current_formula cs;
9.1592 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1593 + (*case*)
9.1594 + Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f (*of*);
9.1595 +\<close> ML \<open>
9.1596 +ThyC.get_theory thy'
9.1597 +\<close> ML \<open>
9.1598 +\<close> ML \<open>
9.1599 +\<close> ML \<open>
9.1600 +\<close> ML \<open> (* \<longrightarrow> src/../rewrite.sml*)
9.1601 +fun trace_calc0 str =
9.1602 + if ! trace_on then writeln ("### " ^ str) else ()
9.1603 +fun trace_calc1 str1 str2 =
9.1604 + if ! trace_on then writeln (str1 ^ str2) else ()
9.1605 +fun trace_calc2 str term popt =
9.1606 + if ! trace_on then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
9.1607 +fun trace_calc3 str term =
9.1608 + if ! trace_on then writeln ("### " ^ str ^ UnparseC.term term) else ()
9.1609 +fun trace_calc4 str t1 t2 =
9.1610 + if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
9.1611 +\<close> ML \<open>
9.1612 +fun get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2)) = (* binary funs *)
9.1613 + (trace_calc1 "1.. get_pair: binop = " op_;
9.1614 + if op_ = op0 then
9.1615 + let
9.1616 + val popt = ef op_ t thy
9.1617 + val _ = trace_calc2 "2.. get_pair: " t popt
9.1618 + in case popt of SOME _ => popt | NONE =>
9.1619 + let
9.1620 + val popt = get_pair thy op_ ef t1
9.1621 + val _ = trace_calc2 "3.. get_pair: " t1 popt
9.1622 + in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end
9.1623 + end
9.1624 + else (* search subterms *)
9.1625 + let
9.1626 + val popt = get_pair thy op_ ef t1
9.1627 + val _ = trace_calc2 "4.. get_pair: " t popt
9.1628 + in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end)
9.1629 + | get_pair _ _ _ _ = NONE
9.1630 +\<close> ML \<open>
9.1631 +fun adhoc_thm thy (op_, eval_fn) ct =
9.1632 + case get_pair thy op_ eval_fn ct of
9.1633 + NONE => NONE
9.1634 + | SOME (thmid, t) => SOME (thmid, Skip_Proof.make_thm thy t);
9.1635 +\<close> ML \<open>
9.1636 +\<close> ML \<open>
9.1637 +\<close> ML \<open>
9.1638 +\<close> ML \<open>
9.1639 +\<close> ML \<open>
9.1640 +UnparseC.term f = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)"
9.1641 +\<close> ML \<open>
9.1642 +"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) =
9.1643 + ((ThyC.get_theory thy'), false, (assoc_rls rls), f);
9.1644 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1645 rewrite__set_ thy 1 bool [] rls term;
9.1646 \<close> ML \<open>
9.1647 -"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
9.1648 - = (thy, 1, bool, []:(term * term) list, rls, term);
9.1649 -
9.1650 +"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
9.1651 + (thy, 1, bool, [], rls, term);
9.1652 +\<close> ML \<open> (* \<longrightarrow> src/../rewrite.sml *)
9.1653 +fun msg thmC t =
9.1654 + "rewrite with thm " ^ quote (ThmC.string_of_thm thmC) ^
9.1655 + " on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
9.1656 \<close> ML \<open>
9.1657 -(*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
9.1658 - datatype switch = Applicable.Yes | Noap;
9.1659 +\<close> ML \<open>
9.1660 +\<close> ML \<open>
9.1661 +(*//-------------------------------- cp fromewrite.sml-----------------------------------------\\*)
9.1662 + (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
9.1663 + datatype switch = Appl | Noap;
9.1664 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
9.1665 - | rew_once ruls asm ct Applicable.Yes [] =
9.1666 - (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
9.1667 + | rew_once ruls asm ct Appl [] =
9.1668 + (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
9.1669 | Rule_Set.Sequence _ => (ct, asm)
9.1670 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
9.1671 | rew_once ruls asm ct apno (rul :: thms) =
9.1672 case rul of
9.1673 Rule.Thm (thmid, thm) =>
9.1674 - (trace1 i (" try thm: " ^ thmid);
9.1675 - case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
9.1676 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
9.1677 + (trace_in1 i "try thm" thmid;
9.1678 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1679 + ((#erls o Rule_Set.rep) rls) put_asm thm ct of
9.1680 NONE => rew_once ruls asm ct apno thms
9.1681 | SOME (ct', asm') =>
9.1682 - (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
9.1683 - rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms)))
9.1684 + (trace_in2 i "rewrites to" thy ct';
9.1685 + rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
9.1686 (* once again try the same rule, e.g. associativity against "()"*)
9.1687 | Rule.Eval (cc as (op_, _)) =>
9.1688 - let val _= trace1 i (" try calc: " ^ op_ ^ "'")
9.1689 - val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
9.1690 + let val _ = trace_in1 i "try calc" op_;
9.1691 in case Eval.adhoc_thm thy cc ct of
9.1692 NONE => rew_once ruls asm ct apno thms
9.1693 | SOME (_, thm') =>
9.1694 let
9.1695 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
9.1696 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
9.1697 - val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
9.1698 - ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
9.1699 - val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
9.1700 - in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end
9.1701 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1702 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
9.1703 + val _ = if pairopt <> NONE then () else raise ERROR (msg thm' ct)
9.1704 + val _ = trace_in3 i "calc. to" thy pairopt;
9.1705 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
9.1706 end
9.1707 | Rule.Cal1 (cc as (op_, _)) =>
9.1708 - let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
9.1709 - val ct = TermC.uminus_to_string ct
9.1710 + let val _ = trace_in1 i "try cal1" op_;
9.1711 in case Eval.adhoc_thm1_ thy cc ct of
9.1712 NONE => (ct, asm)
9.1713 | SOME (_, thm') =>
9.1714 let
9.1715 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
9.1716 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
9.1717 - val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
9.1718 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1719 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
9.1720 + val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
9.1721 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
9.1722 - val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
9.1723 + val _ = trace_in3 i "cal1. to" thy pairopt;
9.1724 in the pairopt end
9.1725 end
9.1726 | Rule.Rls_ rls' =>
9.1727 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
9.1728 - SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms
9.1729 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
9.1730 | NONE => rew_once ruls asm ct apno thms)
9.1731 - | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
9.1732 - val ruls = (#rules o Rule.Rule_Set.rep) rls;
9.1733 -(* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)*)
9.1734 - val (ct', asm') = rew_once ruls [] ct Noap ruls;
9.1735 -"~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
9.1736 - = (ruls, []:term list, ct, Noap, ruls);
9.1737 - val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
9.1738 -
9.1739 - val SOME (ct', asm') = (*case*)
9.1740 - rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
9.1741 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
9.1742 -"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
9.1743 - = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
9.1744 - ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
9.1745 -
9.1746 - val (t', asms, _ (*lrd*), rew) =
9.1747 - rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
9.1748 - (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm) ct;
9.1749 -"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
9.1750 - = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
9.1751 - (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct);
9.1752 - val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
9.1753 - val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
9.1754 -;
9.1755 -(*+*)if UnparseC.term r' =
9.1756 -(*+*) "\<lbrakk>9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
9.1757 -(*+*) "\<Longrightarrow> ((3 + -1 * x + x \<up> 2) /\n" ^
9.1758 -(*+*) " (9 * x + -6 * x \<up> 2 + x \<up> 3) =\n" ^
9.1759 -(*+*) " 1 / x) =\n" ^
9.1760 -(*+*) " ((3 + -1 * x + x \<up> 2) * x =\n" ^
9.1761 -(*+*) " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3))"
9.1762 -(*+*)then () else error "instantiated rule CHANGED";
9.1763 -
9.1764 - val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
9.1765 -;
9.1766 -(*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
9.1767 -(*+*)then () else error "stored assumptions CHANGED";
9.1768 -
9.1769 - val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
9.1770 -;
9.1771 -(*+*)if UnparseC.term t' = "(3 + -1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)"
9.1772 -(*+*)then () else error "rewritten term (an equality) CHANGED";
9.1773 -
9.1774 - val (simpl_p', nofalse) =
9.1775 - eval__true thy (i + 1) p' bdv rls;
9.1776 -"~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
9.1777 - (*if*) asms = [@{term True}] orelse asms = [] (*else*);
9.1778 -
9.1779 -(*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
9.1780 -(*+*)then () else error "asms before chk CHANGED";
9.1781 -
9.1782 - fun chk indets [] = (indets, true) (*return asms<>True until false*)
9.1783 - | chk indets (a :: asms) =
9.1784 - (case rewrite__set_ thy (i + 1) false bdv rls a of
9.1785 - NONE => (chk (indets @ [a]) asms)
9.1786 - | SOME (t, a') =>
9.1787 - if t = @{term True} then (chk (indets @ a') asms)
9.1788 - else if t = @{term False} then ([], false)
9.1789 - (*asm false .. thm not applied \<up> ; continue until False vvv*)
9.1790 - else chk (indets @ [t] @ a') asms);
9.1791 -
9.1792 - val (xxx, true) =
9.1793 - chk [] asms; (*return from eval__true*);
9.1794 -"~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
9.1795 -
9.1796 -(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
9.1797 -(*+*)(*val rules =
9.1798 -(*+*) [Eval (\<^const_name>\<open>divide\<close>, fn),
9.1799 -(*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
9.1800 -(*+*) :
9.1801 -(*+*) Eval (\<^const_name>\<open>HOL.eq\<close>, fn),
9.1802 -(*+*) Thm ("not_true", "(\<not> True) = False"),
9.1803 -(*+*) Thm ("not_false", "(\<not> False) = True"),
9.1804 -(*+*) :
9.1805 -(*+*) Eval (\<^const_name>\<open>powr\<close>, fn),
9.1806 -(*+*) Eval ("RatEq.is_ratequation_in", fn)]:
9.1807 -(*+*) rule list*)
9.1808 -(*+*)chk: term list -> term list -> term list * bool
9.1809 -
9.1810 - rewrite__set_ thy (i + 1) false bdv rls a (*of*);
9.1811 -
9.1812 -(*+*)Rewrite.trace_on := false; (*true false*)
9.1813 -
9.1814 - (*this was False; vvvv--- means: indeterminate*)
9.1815 - val (* SOME (t, a') *)NONE = (*case*)
9.1816 - rewrite__set_ thy (i + 1) false bdv rls a (*of*);
9.1817 -
9.1818 -(*+*)UnparseC.term a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
9.1819 -(*
9.1820 - :
9.1821 - #### rls: rateq_erls on: x \<noteq> 0
9.1822 - :
9.1823 - ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
9.1824 - ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
9.1825 - ##### try calc: HOL.eq'
9.1826 - ##### try thm: not_true
9.1827 - ##### try thm: not_false
9.1828 - ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
9.1829 - and True, False are NOT stored ...
9.1830 - :
9.1831 - ### asms accepted: [x \<noteq> 0] stored: []
9.1832 - : *)
9.1833 -Rewrite.trace_on := false; (*true false*)
9.1834 -( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
9.1835 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
9.1836 +(*\\------------------------------- cp from rewrite.sml---------------------------------------//*)
9.1837 \<close> ML \<open>
9.1838 -
9.1839 +\<close> ML \<open>
9.1840 +"--------------------------------- NEW TEST --> ??? -------------------------------------------";
9.1841 +"--------------------------------- NEW TEST --> ??? -------------------------------------------";
9.1842 +"--------------------------------- NEW TEST --> ??? -------------------------------------------";
9.1843 +\<close> ML \<open>
9.1844 +"~~~~~ and rewrite__set_ thy , args:"; val ((*3*)thy, i, put_asm, bdv, rls, ct) =
9.1845 + (@{theory}, 0, true, []: (term * term) list, assoc_rls "reduce_012", @{term "- 1 / 2 :: real"});
9.1846 +\<close> ML \<open>
9.1847 + val ruls = (#rules o Rule_Set.rep) rls;
9.1848 +\<close> ML \<open>
9.1849 +takerest (8, ruls)
9.1850 +\<close> ML \<open>
9.1851 +\<close> ML \<open>
9.1852 +\<close> ML \<open>
9.1853 + rew_once ruls [] ct Noap ruls;
9.1854 +\<close> ML \<open>
9.1855 +"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms)) =
9.1856 + (ruls, [], ct, Noap, ruls);
9.1857 +\<close> ML \<open>
9.1858 +rul
9.1859 +\<close> ML \<open>
9.1860 +\<close> ML \<open>
9.1861 +val SOME (_, thm') =
9.1862 + Eval.adhoc_thm @{theory} cc t
9.1863 +\<close> ML \<open>
9.1864 +\<close> ML \<open>
9.1865 +\<close> ML \<open>
9.1866 +\<close> ML \<open>
9.1867 +\<close> ML \<open>
9.1868 +\<close> ML \<open>
9.1869 +\<close> ML \<open>
9.1870 +\<close> ML \<open>
9.1871 +\<close> ML \<open>
9.1872 +\<close> ML \<open>
9.1873 +\<close> ML \<open>
9.1874 +\<close> ML \<open>
9.1875 +\<close> ML \<open>
9.1876 +\<close> ML \<open>
9.1877 +\<close> ML \<open>
9.1878 +\<close> ML \<open>
9.1879 +\<close> ML \<open>
9.1880 +\<close> ML \<open>
9.1881 +\<close> ML \<open>
9.1882 +\<close> ML \<open>
9.1883 +\<close> ML \<open>
9.1884 +\<close> ML \<open>
9.1885 +\<close> ML \<open>
9.1886 +\<close> ML \<open>
9.1887 +\<close> ML \<open>
9.1888 +\<close> ML \<open>
9.1889 +\<close> ML \<open>
9.1890 +\<close> ML \<open>
9.1891 + val ruls = (#rules o Rule_Set.rep) rls;
9.1892 +\<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*)
9.1893 +Rewrite.trace_on := true; (*false true*)
9.1894 + val (ct', asm') =
9.1895 + rew_once ruls [] ct Noap ruls;
9.1896 +\<close> ML \<open>
9.1897 +(*+*)UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)";
9.1898 +\<close> ML \<open>
9.1899 +(*+*)rls
9.1900 +\<close> ML \<open>
9.1901 +(*+*)ruls(* =
9.1902 + [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"),
9.1903 + Thm ("real_unari_minus", "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"), Thm ("realpow_multI", "(?r * ?s) \<up> ?n = ?r \<up> ?n * ?s \<up> ?n"), Eval ("Groups.plus_class.plus", fn), Eval ("Groups.minus_class.minus", fn),
9.1904 + Eval ("Groups.times_class.times", fn), Eval ("Rings.divide_class.divide", fn), Eval ("NthRoot.sqrt", fn), Eval ("Transcendental.powr", fn),
9.1905 + Rls ( Repeat
9.1906 + {calc = [], erls =
9.1907 + Repeat
9.1908 + {calc = [], erls = Empty, errpatts = [], id = "erls_in_reduce_012", preconds = [], rew_ord = ("dummy_ord", fn), rules =
9.1909 + [Eval ("Prog_Expr.is_num", fn), Thm ("not_false", "(\<not> False) = True"), Thm ("not_true", "(\<not> True) = False")], scr = Empty_Prog, srls = Empty},
9.1910 + errpatts = [], id = "reduce_012", preconds = [], rew_ord = ("dummy_ord", fn), rules =
9.1911 +------------------------------^^^^^^^^^^^^
9.1912 + [Thm ("mult_1_left", "1 * ?a = ?a"), Thm ("real_minus_mult_left", "\<not> (?a is_num) \<Longrightarrow> - ?a * ?b = - (?a * ?b)"), Thm ("mult_zero_left", "0 * ?a = 0"), Thm ("add_0_left", "0 + ?a = ?a"),
9.1913 + 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")],
9.1914 + scr = Empty_Prog, srls = Empty}
9.1915 + )]*)
9.1916 +\<close> ML \<open>
9.1917 +"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms)) =
9.1918 + (ruls, [], ct, Noap, ruls);
9.1919 +\<close> ML \<open>
9.1920 +val Rule.Thm (thmid, thm) =
9.1921 + (*case*) rul (*of*);
9.1922 +\<close> ML \<open>
9.1923 +val NONE = (*case*) rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1924 + ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*);
9.1925 +\<close> ML \<open>
9.1926 +\<close> ML \<open>
9.1927 +\<close> ML \<open>
9.1928 +\<close> ML \<open>
9.1929 +\<close> ML \<open>
9.1930 +\<close> ML \<open>
9.1931 +\<close> ML \<open>
9.1932 +\<close> ML \<open>
9.1933 +\<close> ML \<open>
9.1934 +\<close> ML \<open>
9.1935 +\<close> ML \<open>
9.1936 +\<close> ML \<open>
9.1937 +\<close> ML \<open>
9.1938 +\<close> ML \<open>
9.1939 +\<close> ML \<open>
9.1940 +\<close> ML \<open>
9.1941 +\<close> ML \<open>
9.1942 +\<close> ML \<open>
9.1943 +\<close> ML \<open>
9.1944 +\<close> ML \<open>
9.1945 +\<close> ML \<open>
9.1946 +\<close> ML \<open>
9.1947 +\<close> ML \<open>
9.1948 +\<close> ML \<open>
9.1949 +\<close> ML \<open>
9.1950 +\<close> ML \<open>
9.1951 +\<close> ML \<open>
9.1952 +\<close> ML \<open>
9.1953 +(*/------------------------------- fun rew_once ITERATED BY HAND -----------------------------\*)
9.1954 +\<close> ML \<open>
9.1955 +UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)";
9.1956 +\<close> ML \<open>
9.1957 +val thm = Rule.thm (nth 1 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*)
9.1958 +\<close> ML \<open>
9.1959 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1960 + ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*);
9.1961 +\<close> ML \<open>
9.1962 +val thm = Rule.thm (nth 2 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"
9.1963 + ATTENTION "real_assoc_1" == "real_assoc_2"*)
9.1964 +\<close> ML \<open>
9.1965 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1966 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
9.1967 +\<close> ML \<open>
9.1968 +val thm = Rule.thm (nth 3 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*)
9.1969 +\<close> ML \<open>
9.1970 +val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1971 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
9.1972 +\<close> ML \<open>
9.1973 +UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 - 0)) / (2 * 2)"
9.1974 +\<close> ML \<open>
9.1975 +val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1976 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
9.1977 +\<close> ML \<open>
9.1978 +UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)"
9.1979 +\<close> ML \<open>
9.1980 +val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1981 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
9.1982 +\<close> ML \<open>
9.1983 +UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)"
9.1984 +\<close> ML \<open>
9.1985 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1986 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
9.1987 +\<close> ML \<open>
9.1988 +val thm = Rule.thm (nth 4 ruls); (* = "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"*)
9.1989 +\<close> ML \<open>
9.1990 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1991 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
9.1992 +\<close> ML \<open>
9.1993 +val thm = Rule.thm (nth 5 ruls); (* = "(?r * ?s) \<up> ?n = ?r \<up> ?n * ?s \<up> ?n"*)
9.1994 +\<close> ML \<open>
9.1995 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.1996 + ((#erls o Rule_Set.rep) rls) put_asm thm ct
9.1997 +\<close> ML \<open> (* \<longrightarrow> Rule.*)
9.1998 +\<close> ML \<open>
9.1999 +val (cc as (op_, _)) = Rule.eval (nth 6 ruls); (* = "Groups.plus_class.plus"*)
9.2000 +\<close> ML \<open>
9.2001 +val NONE = Eval.adhoc_thm thy cc ct
9.2002 +\<close> ML \<open>
9.2003 +val (cc as (op_, _)) = Rule.eval (nth 7 ruls); (* = "Groups.minus_class.minus"*)
9.2004 +\<close> ML \<open>
9.2005 +val NONE = Eval.adhoc_thm thy cc ct
9.2006 +\<close> ML \<open>
9.2007 +val (cc as (op_, _)) = Rule.eval (nth 8 ruls); (* = "Groups.times_class.times"*)
9.2008 +\<close> ML \<open>
9.2009 +val SOME (_, thm') = Eval.adhoc_thm thy cc ct
9.2010 +\<close> ML \<open>
9.2011 +val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.2012 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
9.2013 +\<close> ML \<open>
9.2014 + "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)";
9.2015 +UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)"
9.2016 +\<close> ML \<open>
9.2017 +val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.2018 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
9.2019 +\<close> ML \<open>
9.2020 +UnparseC.term ct = "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)"
9.2021 +\<close> ML \<open>
9.2022 +val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
9.2023 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
9.2024 +\<close> ML \<open>
9.2025 +val (cc as (op_, _)) = Rule.eval (nth 9 ruls); (* = "Rings.divide_class.divide"*)
9.2026 +\<close> ML \<open>
9.2027 +val NONE = Eval.adhoc_thm thy cc ct
9.2028 +\<close> ML \<open>
9.2029 +val (cc as (op_, _)) = Rule.eval (nth 10 ruls); (* = "NthRoot.sqrt"*)
9.2030 +\<close> ML \<open>
9.2031 +val NONE = Eval.adhoc_thm thy cc ct
9.2032 +\<close> ML \<open>
9.2033 +val (cc as (op_, _)) = Rule.eval (nth 11 ruls); (* = "Transcendental.powr"*)
9.2034 +\<close> ML \<open>
9.2035 +val NONE = Eval.adhoc_thm thy cc ct
9.2036 +\<close> ML \<open>
9.2037 +val rls' = Rule.rls (nth 12 ruls); (* = "reduce_012"*)
9.2038 +\<close> ML \<open>
9.2039 +val SOME (ct, []) = rewrite__set_ thy (i + 1) put_asm bdv rls' ct
9.2040 +\<close> ML \<open>
9.2041 + "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)";
9.2042 +UnparseC.term ct = "x = (- 1 + sqrt 1) / (2 * 2) \<or> x = (- 1 + - 1 * sqrt 1) / (2 * 2)"
9.2043 +\<close> ML \<open>
9.2044 +length ruls = 12
9.2045 +\<close> ML \<open>
9.2046 +\<close> ML \<open>
9.2047 +\<close> ML \<open>
9.2048 +\<close> ML \<open>
9.2049 +\<close> ML \<open>
9.2050 +\<close> ML \<open>
9.2051 +\<close> ML \<open>
9.2052 +\<close> ML \<open>
9.2053 +\<close> ML \<open>
9.2054 +\<close> ML \<open>
9.2055 +\<close> ML \<open>
9.2056 +\<close> ML \<open>
9.2057 +\<close> ML \<open>
9.2058 +\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
9.2059 +\<close> text \<open>
9.2060 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2061 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2062 +case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
9.2063 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
9.2064
9.2065 \<close> ML \<open>
9.2066 -"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
9.2067 -"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
9.2068 -"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
9.2069 -"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
9.2070 - (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
9.2071 -"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
9.2072 - (thy, 1, [], rew_ord, erls, bool, thm, term);
9.2073 -"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
9.2074 - (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)
9.2075 - val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r
9.2076 - val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
9.2077 - val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
9.2078 - val t' = (snd o HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r'
9.2079 -;
9.2080 -if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()
9.2081 -else error "ARGS FOR Pattern.match CHANGED";
9.2082 -val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
9.2083 -if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
9.2084 - else error "Pattern.match CHANGED";
9.2085 +(*EP-//*)
9.2086 +val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
9.2087 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
9.2088 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
9.2089 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.2090 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2091 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2092 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2093 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2094 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2095 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2096 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2097 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
9.2098 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
9.2099
9.2100 -"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
9.2101 -"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
9.2102 -"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
9.2103 -(* norm_equation is defined in Test.thy, other rls see Knowledg/**)
9.2104 -val thy = @{theory};
9.2105 -val rls = norm_equation;
9.2106 -val term = TermC.str2term "x + 1 = 2";
9.2107 -
9.2108 -(**)val SOME (t, asm) = rewrite_set_ thy false rls term;
9.2109 -(** )##### try thm: "root_ge0"
9.2110 -exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):
9.2111 - dest_eq
9.2112 - 0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True( **)
9.2113 -if UnparseC.term t = "x + 1 + - 1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
9.2114 -
9.2115 -"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
9.2116 -"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
9.2117 - (thy, 1, bool, []: (term * term) list, rls, term);
9.2118 -(*deleted after error detection*)
9.2119
9.2120 \<close> ML \<open>
9.2121 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
9.2122 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
9.2123 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
9.2124 +(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
9.2125 +see --- val rls = calculate_RootRat > calculate_Rational ---
9.2126 +calculate_RootRat was a TODO with 2002, requires re-design.
9.2127 +see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
9.2128 +*)
9.2129 + val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
9.2130 + "solveFor x", "solutions L"];
9.2131 + val (dI',pI',mI') =
9.2132 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
9.2133 + ["PolyEq", "complete_square"]);
9.2134 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.2135 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2136 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2137 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2138 +
9.2139 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2140 +(*Apply_Method ("PolyEq", "complete_square")*)
9.2141 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2142 +(*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
9.2143 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2144 +(*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
9.2145 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2146 +(*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
9.2147 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2148 +(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
9.2149 + 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
9.2150 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2151 +(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
9.2152 + - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
9.2153 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2154 +(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
9.2155 + - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
9.2156 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2157 +(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
9.2158 + x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
9.2159 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2160 +(*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
9.2161 + x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
9.2162 + NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
9.2163 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2164 +(*"x = - 2 | x = 4" nxt = Or_to_List*)
9.2165 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2166 +(*"[x = - 2, x = 4]" nxt = Check_Postcond*)
9.2167 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
9.2168 +(* FIXXXME
9.2169 + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
9.2170 + | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
9.2171 +*)
9.2172 +if f2str f =
9.2173 + "[x = - 1 * - 1 + - 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))]"
9.2174 +(*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
9.2175 +then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
9.2176 +
9.2177 +
9.2178 +\<close> ML \<open>
9.2179 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
9.2180 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
9.2181 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
9.2182 +(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
9.2183 +see --- val rls = calculate_RootRat > calculate_Rational ---*)
9.2184 +val thy = @{theory PolyEq};
9.2185 +val ctxt = Proof_Context.init_global thy;
9.2186 +val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
9.2187 +val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
9.2188 +
9.2189 +\<close> ML \<open>
9.2190 +val rls = complete_square;
9.2191 +val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
9.2192 +\<close> ML \<open>
9.2193 +if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2"
9.2194 +then () else error "rls complete_square CHANGED";
9.2195 +
9.2196 +\<close> ML \<open>
9.2197 +val thm = @{thm square_explicit1};
9.2198 +val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
9.2199 +\<close> ML \<open>
9.2200 +if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
9.2201 +then () else error "thm square_explicit1 CHANGED";
9.2202 +
9.2203 +\<close> ML \<open>
9.2204 +val thm = @{thm root_plus_minus};
9.2205 +val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
9.2206 +\<close> ML \<open>
9.2207 +if UnparseC.term t =
9.2208 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
9.2209 +then () else error "thm root_plus_minus CHANGED";
9.2210 +
9.2211 +\<close> ML \<open>
9.2212 +(*the thm bdv_explicit2* here required to be constrained to ::real*)
9.2213 +val thm = @{thm bdv_explicit2};
9.2214 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
9.2215 +\<close> ML \<open>
9.2216 +if UnparseC.term t =
9.2217 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
9.2218 +then () else error "thm bdv_explicit2 CHANGED";
9.2219 +
9.2220 +\<close> ML \<open>
9.2221 +val thm = @{thm bdv_explicit3};
9.2222 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
9.2223 +\<close> ML \<open>
9.2224 +if UnparseC.term t =
9.2225 +"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
9.2226 +then () else error "thm bdv_explicit3 CHANGED";
9.2227 +
9.2228 +\<close> ML \<open>
9.2229 +val thm = @{thm bdv_explicit2};
9.2230 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
9.2231 +\<close> ML \<open>
9.2232 +if UnparseC.term t =
9.2233 +"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
9.2234 +then () else error "thm bdv_explicit2 CHANGED";
9.2235 +
9.2236 +\<close> ML \<open>
9.2237 +val rls = calculate_RootRat;
9.2238 +val SOME (t,asm) = rewrite_set_ thy true rls t;
9.2239 +\<close> ML \<open>
9.2240 +if UnparseC.term t =
9.2241 + "- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - - 8) \<or>\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))"
9.2242 +(*"- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"..isabisac15*)
9.2243 +then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
9.2244 +(*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
9.2245 +
9.2246 +
9.2247 +\<close> ML \<open>
9.2248 +"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
9.2249 +"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
9.2250 +"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
9.2251 +"---- test the erls ----";
9.2252 + val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
9.2253 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
9.2254 + val t' = UnparseC.term t;
9.2255 + (*if t'= \<^const_name>\<open>True\<close> then ()
9.2256 + else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
9.2257 +(* *)
9.2258 + val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
9.2259 + "solveFor x", "solutions L"];
9.2260 + val (dI',pI',mI') =
9.2261 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
9.2262 + ["PolyEq", "complete_square"]);
9.2263 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.2264 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2265 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2266 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2267 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2268 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2269 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2270 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2271 + (*Apply_Method ("PolyEq", "complete_square")*)
9.2272 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
9.2273 +
9.2274 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
9.2275 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
9.2276 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
9.2277 + val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
9.2278 + "solveFor x", "solutions L"];
9.2279 + val (dI',pI',mI') =
9.2280 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
9.2281 + ["PolyEq", "complete_square"]);
9.2282 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.2283 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2284 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2285 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2286 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2287 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2288 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2289 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2290 + (*Apply_Method ("PolyEq", "complete_square")*)
9.2291 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2292 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2293 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2294 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2295 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2296 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2297 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2298 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2299 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2300 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.2301 +(* FIXXXXME n1.,
9.2302 + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
9.2303 + | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
9.2304 +*)
9.2305 +
9.2306 \<close> ML \<open>
9.2307 \<close>
9.2308