# HG changeset patch # User wneuper # Date 1626372136 -7200 # Node ID a7c0e6ab4883470259d172f0ebab893841f25212 # Parent 5c7128feb370c4a12b45af39cc2d0ba497e492d6 rewrite.sml + poly.sml + rational.sml + polyminus.sml: ok diff -r 5c7128feb370 -r a7c0e6ab4883 src/Tools/isac/Knowledge/PolyMinus.thy --- a/src/Tools/isac/Knowledge/PolyMinus.thy Thu Jul 15 14:10:18 2021 +0200 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Thu Jul 15 20:02:16 2021 +0200 @@ -110,67 +110,64 @@ (** eval functions **) (*. get the identifier from specific monomials; see fun ist_monom .*) -(*HACK.WN080107*) -fun increase str = - let - val (s, ss) = - case Symbol.explode str of - s :: ss => (s, ss) - | _ => raise ERROR "PolyMinus.increase: uncovered case" - in implode ((chr (ord s + 1))::ss) end; -fun identifier (Free (id,_)) = id (* 2 , a *) - | identifier (Const ("Groups.times_class.times", _) $ Free (_(*num*), _) $ Free (id, _)) = - id (* 2*a , a*b *) - | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *) - (Const ("Groups.times_class.times", _) $ - Free (num, _) $ Free _) $ Free (id, _)) = - if TermC.is_num' num then id +fun identifier (Free (id, _)) = id (* //2, a *) +(*TOODOO*) + | identifier (* 3*a*b *) + (Const ("Groups.times_class.times", _) $ (Const ("Groups.times_class.times", _) $ + num $ t) $ Free (id, _)) = + if TermC.is_num num andalso TermC.is_atom t then id else "|||||||||||||" - | identifier (Const ("Transcendental.powr", _) $ Free (base, _) $ Free (_(*exp*), _)) = - if TermC.is_num' base then "|||||||||||||" (* a^2 *) - else (*increase*) base - | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *) - (Const ("Transcendental.powr", _) $ - Free (base, _) $ Free (_(*exp*), _))) = - if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base + + | identifier (* 2*a, a*b *) + (Const ("Groups.times_class.times", _) $ num $ Free (id, _)) = + if TermC.is_atom num then id else "|||||||||||||" - | identifier _ = "|||||||||||||"(*the "largest" string*); + + | identifier (Const ("Transcendental.powr", _) $ base $ exp) = (* a^2 *) + if TermC.is_num base andalso TermC.is_atom exp then "|||||||||||||" + else TermC.string_of_atom base + + | identifier (* 3*a^2 *) + (Const ("Groups.times_class.times", _) $ num $ + (Const ("Transcendental.powr", _) $ base $ exp )) = + if TermC.is_num num andalso not (TermC.is_num base) andalso TermC.is_atom exp + then TermC.string_of_atom base + else "|||||||||||||" + + | identifier t = + if TermC.is_num t then TermC.string_of_num t (* 2 , //a *) + else "|||||||||||||"; (*the "largest" string*) (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*) (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *) fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ = - if TermC.is_num b then - if TermC.is_num a then (*123 kleiner 32 = True !!!*) - if TermC.num_of_term a < TermC.num_of_term b then - SOME ((UnparseC.term p) ^ " = True", - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) - else SOME ((UnparseC.term p) ^ " = False", - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) - else (* -1 * -2 kleiner 0 *) - SOME ((UnparseC.term p) ^ " = False", - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) + if TermC.is_num b then + if TermC.is_num a then (*123 kleiner 32 = True !!!*) + if TermC.num_of_term a < TermC.num_of_term b then + SOME ((UnparseC.term p) ^ " = True", + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) + else SOME ((UnparseC.term p) ^ " = False", + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) + else (* -1 * -2 kleiner 0 *) + SOME ((UnparseC.term p) ^ " = False", + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) else - if identifier a < identifier b then - SOME ((UnparseC.term p) ^ " = True", - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) - else SOME ((UnparseC.term p) ^ " = False", - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) + if identifier a < identifier b then + SOME ((UnparseC.term p) ^ " = True", + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) + else SOME ((UnparseC.term p) ^ " = False", + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) | eval_kleiner _ _ _ _ = NONE; -fun ist_monom (Free _) = true (* 2, a *) - | ist_monom (Const ("Groups.times_class.times", _) $ - (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) = true - | ist_monom (Const ("Groups.times_class.times", _) $ (* 2*a, a*b *) - Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = false - | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *) - (Const ("Groups.times_class.times", _) $ - (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) $ Free _) = true - | ist_monom (Const ("Transcendental.powr", _) $ (* a^2 *) - Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = true - | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a^2 *) - (Const ("Num.numeral_class.numeral", _) $ _) $ - (Const ("Transcendental.powr", _) $ Free _ $ Free _)) = true - | ist_monom _ = false; +fun ist_monom t = + if TermC.is_atom t then true + else + case t of + Const ("Groups.times_class.times", _) $ t1 $ t2 => + ist_monom t1 andalso ist_monom t2 + | Const ("Transcendental.powr", _) $ t1 $ t2 => + ist_monom t1 andalso ist_monom t2 + | _ => false (* is this a univariate monomial ? *) (*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*) @@ -188,8 +185,8 @@ (** rulesets **) val erls_ordne_alphabetisch = - Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty - [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""), + Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty + [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""), Rule.Eval ("PolyMinus.ist_monom", eval_ist_monom "") ]; diff -r 5c7128feb370 -r a7c0e6ab4883 test/Pure/Isar/Test_Parsers.thy --- a/test/Pure/Isar/Test_Parsers.thy Thu Jul 15 14:10:18 2021 +0200 +++ b/test/Pure/Isar/Test_Parsers.thy Thu Jul 15 20:02:16 2021 +0200 @@ -145,7 +145,7 @@ (Args.$$$ "theory" -- Args.name); parse (Args.$$$ "theory" -- Args.name); (* -parse (Args.$$$ "theory") GOON ?!?!? +parse (Args.$$$ "theory") ?!?!? "theory"; parse (Args.$$$ "theory") @@ -440,8 +440,8 @@ parse (body "") "top bullet top"; \ -section \GOON\ -subsection \GOON\ +section \xxx\ +subsection \xxx\ end \ No newline at end of file diff -r 5c7128feb370 -r a7c0e6ab4883 test/Tools/isac/Knowledge/poly.sml --- a/test/Tools/isac/Knowledge/poly.sml Thu Jul 15 14:10:18 2021 +0200 +++ b/test/Tools/isac/Knowledge/poly.sml Thu Jul 15 20:02:16 2021 +0200 @@ -1430,10 +1430,10 @@ (*SO: WHY IS THERE NO REWRITING ...*) val term = TermC.str2term "2*b + (3*a + 3*b)"; -(*+++*)val SOME (t', []) = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term; -(*+++*)if UnparseC.term t' = "a * 3 + (b * 2 + b * 3)" then () else error "no rewriting ?!?"; -(* before dropping ThmC.numerals_to_Free this was -val NONE = rewrite_set_ @ {theory "Isac_Knowledge"} false order_add_mult term; -SO: WHY IS THERE NO REWRITING ?!? +(*+++*)val NONE = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term; +(* +WHY IS THERE NO REWRITING ?!? +most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML, +while order_add_mult uses isac's rewriter -- and this is used rarely! *) diff -r 5c7128feb370 -r a7c0e6ab4883 test/Tools/isac/Knowledge/polyminus.sml --- a/test/Tools/isac/Knowledge/polyminus.sml Thu Jul 15 14:10:18 2021 +0200 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu Jul 15 20:02:16 2021 +0200 @@ -7,7 +7,7 @@ "--------------------------------------------------------"; "table of contents --------------------------------------"; "--------------------------------------------------------"; -"----------- fun contains_mult_pot_only --------------------------------------------------------"; +"----------- fun identifier --------------------------------------------------------------------"; "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------"; "----------- fun ist_monom ---------------------------------------------------------------------"; "----------- fun eval_ist_monom -------------------------"; @@ -32,40 +32,57 @@ val thy = @{theory "PolyMinus"}; -"----------- fun contains_mult_pot_only --------------------------------------------------------"; -"----------- fun contains_mult_pot_only --------------------------------------------------------"; -"----------- fun contains_mult_pot_only --------------------------------------------------------"; -val t = @{term 0}; - if contains_mult_pot_only t then () else error "contains_mult_pot_only 1"; +"----------- fun identifier --------------------------------------------------------------------"; +"----------- fun identifier --------------------------------------------------------------------"; +"----------- fun identifier --------------------------------------------------------------------"; +if identifier (TermC.str2term "12 ::real") = "12" then () else error "identifier 1"; +if identifier (TermC.str2term "a ::real") = "a" then () else error "identifier 2"; +if identifier (TermC.str2term "3 * a ::real") = "a" then () else error "identifier 3"; +if identifier (TermC.str2term "a \ 2 ::real") = "a" then () else error "identifier 4"; +if identifier (TermC.str2term "3*a \ 2 ::real") = "a" then () else error "identifier 5"; +if identifier (TermC.str2term "a * b ::real") = "b" then () else error "identifier 5b"; -val t = @{term "a"}; -if contains_mult_pot_only t then () else error "contains_mult_pot_only 2"; - -val t = @{term "2 * a"}; -if contains_mult_pot_only t then () else error "contains_mult_pot_only 3"; - -val t = @{term "2 * a * b"}; -if contains_mult_pot_only t then () else error "contains_mult_pot_only 4"; - -val t = @{term "a * b"}; -if contains_mult_pot_only t then () else error "contains_mult_pot_only 5"; - -val t = @{term "2 * a \ 2 * b"}; -if contains_mult_pot_only t then () else error "contains_mult_pot_only 6"; - -val t = @{term "a \ 2 * b \ 3"}; -if contains_mult_pot_only t then () else error "contains_mult_pot_only 7"; - -(* but also ..*) -val t = @{term "a \ 2 * 4 * b \ 3 * 5"}; -if contains_mult_pot_only t then () else error "contains_mult_pot_only 8"; +(*these are strange (see "specific monomials" in comment to fun.def.)..*) +if identifier (TermC.str2term "a*b ::real") = "b" then () else error "identifier 6"; +if identifier (TermC.str2term "(3*a*b) ::real") = "b" then () else error "identifier 7"; "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------"; "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------"; "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------"; +"a" < "b"; +"ba" < "ab"; +"123" < "a"; (*unused due to ---vvv*) +"12" < "3"; (*true !!!*) + +" a kleiner b ==> (b + a) = (a + b)"; +TermC.str2term "aaa"; +TermC.str2term "222 * aaa"; + +case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of + SOME ("123 kleiner 32 = False", _) => () + | _ => error "polyminus.sml: 12 kleiner 9 = False"; +case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of + SOME ("a kleiner b = True", _) => () + | _ => error "polyminus.sml: a kleiner b = True"; +case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of + SOME ("10 * g kleiner f = False", _) => () + | _ => error "polyminus.sml: 10 * g kleiner f = False"; +case eval_kleiner 0 0 (TermC.str2term "(a \ 2) kleiner b") 0 of + SOME ("a \ 2 kleiner b = True", _) => () + | _ => error "polyminus.sml: a \ 2 kleiner b = True"; +case eval_kleiner 0 0 (TermC.str2term "(3*a \ 2) kleiner b") 0 of + SOME ("3 * a \ 2 kleiner b = True", _) => () + | _ => error "polyminus.sml: 3 * a \ 2 kleiner b = True"; +case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of + SOME ("a * b kleiner c = True", _) => () + | _ => error "polyminus.sml: a * b kleiner b = True"; +case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of + SOME ("3 * a * b kleiner c = True", _) => () + | _ => error "polyminus.sml: 3 * a * b kleiner b = True"; + + val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)"; - val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) = eval_kleiner "aaa" "bbb" t "ccc"; "~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const ("PolyMinus.kleiner",_) $ a $ b)), _) = @@ -74,17 +91,45 @@ (*if*) identifier a < identifier b (*else*); "~~~~~ fun identifier , args:"; val (t) = (a); - (*+*)case a of Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ (Const ("Num.num.Bit0", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)))) => () -| _ => error "eval_kleiner CHANGED"; +| _ => error "eval_kleiner CHANGED"; (*isa*) + + +"----------- fun ist_monom ---------------------------------------------------------------------"; +"----------- fun ist_monom ---------------------------------------------------------------------"; +"----------- fun ist_monom ---------------------------------------------------------------------"; +val t = TermC.str2term "0 ::real"; + if ist_monom t then () else error "ist_monom 1"; + +val t = TermC.str2term "a"; +if ist_monom t then () else error "ist_monom 2"; + +val t = TermC.str2term "2 * a"; +if ist_monom t then () else error "ist_monom 3"; + +val t = TermC.str2term "2 * a * b"; +if ist_monom t then () else error "ist_monom 4"; + +val t = TermC.str2term "a * b"; +if ist_monom t then () else error "ist_monom 5"; + +(*not covered before NEW numerals*) +val t = TermC.str2term "2 * a \ 2 * b"; +if ist_monom t then () else error "ist_monom 6"; + +(*not covered before NEW numerals*) +val t = TermC.str2term "a \ 2 * b \ 3"; +if ist_monom t then () else error "ist_monom 7"; + +val t = TermC.str2term "a \ 2 * 4 * b \ 3 * 5"; +if ist_monom t then () else error "ist_monom 8"; "----------- fun eval_ist_monom ----------------------------------"; "----------- fun eval_ist_monom ----------------------------------"; "----------- fun eval_ist_monom ----------------------------------"; -ist_monom (TermC.str2term "12"); case eval_ist_monom 0 0 (TermC.str2term "12 ist_monom") 0 of SOME ("12 ist_monom = True", _) => () | _ => error "polyminus.sml: 12 ist_monom = True"; @@ -239,7 +284,7 @@ else error "polyminus.sml: ordne_alphabetisch a + b + c"; "======= rewrite goes into subterms"; -val t = TermC.str2term "a + c + b + d"; +val t = TermC.str2term "a + c + b + d ::real"; val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; UnparseC.term t; if UnparseC.term t = "a + b + c + d" then () else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d"; @@ -268,7 +313,7 @@ "----------- build fasse_zusammen --------------------------------"; val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"; val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t; -if UnparseC.term t = "3 + -2 * e + 2 * f + 2 * g" then () +if UnparseC.term t = "3 + - 2 * e + 2 * f + 2 * g" then () else error "polyminus.sml: fasse_zusammen finished"; "----------- build verschoenere ----------------------------------"; @@ -311,11 +356,17 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; + f2str f = "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12"; (*isa == isa2*) +val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; + val (*^^^*) Rewrite_Set "ordne_alphabetisch" = nxt; + f2str f = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"; (*isa2*) +val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; + f2str f = "3 + - 2 * e + 2 * f + 2 * g"; (*isa2*) val (p,_,f,nxt,_,pt) = me nxt p c pt; + f2str f = "3 - 2 * e + 2 * f + 2 * g"; (*isa2*) val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -if f2str f = "3 - 2 * e + 2 * f + 2 * g" + f2str f = "3 - 2 * e + 2 * f + 2 * g"; (*isa2*) +if f2str f = "3 - 2 * e + 2 * f + 2 * g" (*isa2*) then case nxt of End_Proof' => () | _ => error "me simplification.for_polynomials.with_minus 1" else error "polyminus.sml: me simplification.for_polynomials.with_minus 2"; @@ -371,7 +422,7 @@ autoCalculate 1 CompleteCalc; val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; if p = ([], Res) andalso - UnparseC.term (get_obj g_res pt (fst p)) = "-3 * u - v" + UnparseC.term (get_obj g_res pt (fst p)) = "- 3 * u - v" then () else error "polyminus.sml: Vereinfache 139 b)"; "======= 138 a ---"; @@ -384,7 +435,7 @@ autoCalculate 1 CompleteCalc; val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; if p = ([], Res) andalso - UnparseC.term (get_obj g_res pt (fst p)) = "-4 * u + 2 * v" + UnparseC.term (get_obj g_res pt (fst p)) = "- 4 * u + 2 * v" then () else error "polyminus.sml: Vereinfache 138 a)"; "----------- met probe fuer_polynom ------------------------------"; @@ -582,8 +633,10 @@ moveActiveRoot 1; autoCalculate 1 CompleteCalc; val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if p = ([], Res) andalso - UnparseC.term (get_obj g_res pt (fst p)) = "-2 + 12 * a \ 2 + 5 * a" + +if p = ([], Res) andalso + UnparseC.term (get_obj g_res pt (fst p)) =(*"- 2 + 12 * a \ 2 + 5 * a" with OLD numerals*) + "- 2 + 5 * a + 12 * a \ 2" then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ..."; "----------- pbl binom polynom vereinfachen: cube ----------------"; diff -r 5c7128feb370 -r a7c0e6ab4883 test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Thu Jul 15 14:10:18 2021 +0200 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Jul 15 20:02:16 2021 +0200 @@ -512,13 +512,14 @@ \ ML \ (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*) \ ML \ -val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f +(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f \ ML \ (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*) \ ML \ -f +(*+*)val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f \ ML \ +\ ML \ (*GOON*) map Tactic.input_to_string (specific_from_prog pt p) \ ML \ (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = @@ -971,6 +972,18 @@ ML_file "Knowledge/descript.sml" ML_file "Knowledge/simplify.sml" ML_file "Knowledge/poly.sml" +ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML_file "Knowledge/gcd_poly_ml.sml" ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*) ML_file "Knowledge/rational.sml" (*Test_Isac_Short*) diff -r 5c7128feb370 -r a7c0e6ab4883 test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Thu Jul 15 14:10:18 2021 +0200 +++ b/test/Tools/isac/Test_Some.thy Thu Jul 15 20:02:16 2021 +0200 @@ -101,815 +101,23 @@ \ ML \ \ -section \======= NEW src/../PolyMinus.thy ==================================================\ +section \===================================================================================\ ML \ \ ML \ -\ ML \ (* \ PolyMinus.thy *) -fun identifier (Const ("Groups.times_class.times", _) $ Free (_(*num*), _) $ Free (id, _)) = - id (* 2*a , a*b *) - | identifier (Const ("Groups.times_class.times", _) $ (Const ("Groups.times_class.times", _) $ - Free (num, _) $ Free _) $ Free (id, _)) = (* 3*a*b *) - if TermC.is_num' num then id - else "|||||||||||||" - | identifier (Const ("Transcendental.powr", _) $ Free (base, _) $ Free (_(*exp*), _)) = - if TermC.is_num' base then "|||||||||||||" (* a^2 *) - else (*increase*) base - | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *) - (Const ("Transcendental.powr", _) $ Free (base, _) $ Free (_(*exp*), _))) = - if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base - else "|||||||||||||" - | identifier (Free (str, _)) = str (* a *) - | identifier t = - if TermC.is_atom t then TermC.string_of_atom t - else "|||||||||||||"; (*the "largest" string*) - -\ ML \ (* \ PolyMinus.thy *) -fun ist_monom t = - if TermC.is_atom t then true - else - case t of - Const ("Groups.times_class.times", _) $ t1 $ t2 => - ist_monom t1 andalso ist_monom t2 - | Const ("Transcendental.powr", _) $ t1 $ t2 => - ist_monom t1 andalso ist_monom t2 - | _ => false - -\ ML \ (* \ PolyMinus.thy *) -fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ = - if TermC.is_num b then - if TermC.is_num a then (*123 kleiner 32 = True !!!*) - if TermC.num_of_term a < TermC.num_of_term b then - SOME ((UnparseC.term p) ^ " = True", - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) - else SOME ((UnparseC.term p) ^ " = False", - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) - else (* -1 * -2 kleiner 0 *) - SOME ((UnparseC.term p) ^ " = False", - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) - else - if identifier a < identifier b then - SOME ((UnparseC.term p) ^ " = True", - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) - else SOME ((UnparseC.term p) ^ " = False", - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) - | eval_kleiner _ _ _ _ = NONE; +\ ML \ \ ML \ \ -section \======= test/../polyminus.sml =====================================================\ +section \===================================================================================\ ML \ \ ML \ -(* title: Knowledge/polyminus.sml - author: Walther Neuper - WN071207, - (c) due to copyright terms -*) -"--------------------------------------------------------"; -"--------------------------------------------------------"; -"table of contents --------------------------------------"; -"--------------------------------------------------------"; -"----------- fun identifier --------------------------------------------------------------------"; -"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------"; -"----------- fun eval_ist_monom -------------------------"; -"----------- watch order_add_mult ----------------------"; -"----------- build predicate for +- ordering ------------"; -"----------- build fasse_zusammen -----------------------"; -"----------- build verschoenere -------------------------"; -"----------- met simplification for_polynomials with_minu"; -"----------- me simplification.for_polynomials.with_minus"; -"----------- pbl polynom vereinfachen p.33 --------------"; -"----------- met probe fuer_polynom ---------------------"; -"----------- pbl polynom probe --------------------------"; -"----------- pbl klammer polynom vereinfachen p.34 ------"; -"----------- try fun applyTactics -----------------------"; -"----------- pbl binom polynom vereinfachen p.39 --------"; -"----------- pbl binom polynom vereinfachen: cube -------"; -"----------- Refine.refine Vereinfache -------------------------"; -"----------- *** Problem.prep_input: syntax error in '#Where' of [v"; -"--------------------------------------------------------"; -"--------------------------------------------------------"; -"--------------------------------------------------------"; +\ ML \ +\ ML \ +\ -val thy = @{theory "PolyMinus"}; - -"----------- fun identifier --------------------------------------------------------------------"; -"----------- fun identifier --------------------------------------------------------------------"; -"----------- fun identifier --------------------------------------------------------------------"; +section \===================================================================================\ +ML \ \ ML \ -if identifier (TermC.str2term "12 ::real") = "12" then () else error "identifier 1"; -if identifier (TermC.str2term "a ::real") = "a" then () else error "identifier 2"; -if identifier (TermC.str2term "3 * a ::real") = "a" then () else error "identifier 3"; -if identifier (TermC.str2term "a \ 2 ::real") = "a" then () else error "identifier 4"; -if identifier (TermC.str2term "3*a \ 2 ::real") = "a" then () else error "identifier 5"; - -(*these are strange ..*) -if identifier (TermC.str2term "a*b ::real") = "b" then () else error "identifier 6"; -if identifier (TermC.str2term "(3*a*b) ::real") = "b" then () else error "identifier 7"; - -\ ML \ -"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------"; -"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------"; -"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------"; -"a" < "b"; -"ba" < "ab"; -"123" < "a"; (*unused due to ---vvv*) -"12" < "3"; (*true !!!*) - -" a kleiner b ==> (b + a) = (a + b)"; -TermC.str2term "aaa"; -TermC.str2term "222 * aaa"; - -\ ML \ -case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of - SOME ("123 kleiner 32 = False", _) => () - | _ => error "polyminus.sml: 12 kleiner 9 = False"; - -\ ML \ -case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of - SOME ("a kleiner b = True", _) => () - | _ => error "polyminus.sml: a kleiner b = True"; - -\ ML \ -case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of - SOME ("10 * g kleiner f = False", _) => () - | _ => error "polyminus.sml: 10 * g kleiner f = False"; - -\ ML \ -case eval_kleiner 0 0 (TermC.str2term "(a \ 2) kleiner b") 0 of - SOME ("a \ 2 kleiner b = True", _) => () - | _ => error "polyminus.sml: a \ 2 kleiner b = True"; - -\ ML \ -"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const ("PolyMinus.kleiner",_) $ a $ b)), _) = - ( 0, 0, (TermC.str2term "(a \ 2) kleiner b"), 0); -\ ML \ - (*if*) TermC.is_num b (*else*); -\ ML \ - (*if*) identifier a < identifier b (*else*); -\ ML \ -(*+*) identifier a = "|||||||||||||"; (*isa*) -(*+*) identifier a = "a"; (*isa2*) -\ ML \ -(*+*) identifier b = "b"; (*isa == isa2*) -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -case eval_kleiner 0 0 (TermC.str2term "(3*a \ 2) kleiner b") 0 of - SOME ("3 * a \ 2 kleiner b = True", _) => () - | _ => error "polyminus.sml: 3 * a \ 2 kleiner b = True"; - -\ ML \ -case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of - SOME ("a * b kleiner c = True", _) => () - | _ => error "polyminus.sml: a * b kleiner b = True"; - -\ ML \ -case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of - SOME ("3 * a * b kleiner c = True", _) => () - | _ => error "polyminus.sml: 3 * a * b kleiner b = True"; - -\ ML \ -val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)"; - -val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) = - eval_kleiner "aaa" "bbb" t "ccc"; -"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const ("PolyMinus.kleiner",_) $ a $ b)), _) = - ("aaa", "bbb", t, "ccc"); - (*if*) TermC.is_num b (*else*); - - (*if*) identifier a < identifier b (*else*); -"~~~~~ fun identifier , args:"; val (t) = (a); - -(*+*)case a of - Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ - (Const ("Num.num.Bit0", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)))) => () -| _ => error "eval_kleiner CHANGED"; - - -\ ML \ -"----------- fun ist_monom ---------------------------------------------------------------------"; -"----------- fun ist_monom ---------------------------------------------------------------------"; -"----------- fun ist_monom ---------------------------------------------------------------------"; -val t = @{term 0}; - if ist_monom t then () else error "ist_monom 1"; - -val t = @{term "a"}; -if ist_monom t then () else error "ist_monom 2"; - -val t = @{term "2 * a"}; -if ist_monom t then () else error "ist_monom 3"; - -val t = @{term "2 * a * b"}; -if ist_monom t then () else error "ist_monom 4"; - -val t = @{term "a * b"}; -if ist_monom t then () else error "ist_monom 5"; - -val t = @{term "2 * a \ 2 * b"}; -if ist_monom t then () else error "ist_monom 6"; - -val t = @{term "a \ 2 * b \ 3"}; -if ist_monom t then () else error "ist_monom 7"; - -(* but also ..*) -val t = @{term "a \ 2 * 4 * b \ 3 * 5"}; -if ist_monom t then () else error "ist_monom 8"; -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -"----------- fun eval_ist_monom ----------------------------------"; -"----------- fun eval_ist_monom ----------------------------------"; -"----------- fun eval_ist_monom ----------------------------------"; -\ ML \ -case eval_ist_monom 0 0 (TermC.str2term "12 ist_monom") 0 of - SOME ("12 ist_monom = True", _) => () - | _ => error "polyminus.sml: 12 ist_monom = True"; - -case eval_ist_monom 0 0 (TermC.str2term "a ist_monom") 0 of - SOME ("a ist_monom = True", _) => () - | _ => error "polyminus.sml: a ist_monom = True"; - -case eval_ist_monom 0 0 (TermC.str2term "(3*a) ist_monom") 0 of - SOME ("3 * a ist_monom = True", _) => () - | _ => error "polyminus.sml: 3 * a ist_monom = True"; - -case eval_ist_monom 0 0 (TermC.str2term "(a \ 2) ist_monom") 0 of - SOME ("a \ 2 ist_monom = True", _) => () - | _ => error "polyminus.sml: a \ 2 ist_monom = True"; - -case eval_ist_monom 0 0 (TermC.str2term "(3*a \ 2) ist_monom") 0 of - SOME ("3 * a \ 2 ist_monom = True", _) => () - | _ => error "polyminus.sml: 3*a \ 2 ist_monom = True"; - -case eval_ist_monom 0 0 (TermC.str2term "(a*b) ist_monom") 0 of - SOME ("a * b ist_monom = True", _) => () - | _ => error "polyminus.sml: a*b ist_monom = True"; - -case eval_ist_monom 0 0 (TermC.str2term "(3*a*b) ist_monom") 0 of - SOME ("3 * a * b ist_monom = True", _) => () - | _ => error "polyminus.sml: 3*a*b ist_monom = True"; - - -\ ML \ -"----------- watch order_add_mult -------------------------------"; -"----------- watch order_add_mult -------------------------------"; -"----------- watch order_add_mult -------------------------------"; -"----- with these simple variables it works..."; -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) -Rewrite.trace_on:=false; -val t = TermC.str2term "((a + d) + c) + b"; -val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t; -if UnparseC.term t = "a + (b + (c + d))" then () -else error "polyminus.sml 1 watch order_add_mult"; -Rewrite.trace_on:=false; - -"----- the same stepwise..."; -val od = ord_make_polynomial true (@{theory "Poly"}); -val t = TermC.str2term "((a + d) + c) + b"; -"((a + d) + c) + b"; -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t; -"b + ((a + d) + c)"; -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t; -"b + (c + (a + d))"; -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t; -"b + (a + (c + d))"; -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t; -"a + (b + (c + d))"; -if UnparseC.term t = "a + (b + (c + d))" then () -else error "polyminus.sml 2 watch order_add_mult"; - -"----- if parentheses are right, left_commute is (almost) sufficient..."; -val t = TermC.str2term "a + (d + (c + b))"; -"a + (d + (c + b))"; -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t; -"a + (c + (d + b))"; -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t;UnparseC.term t; -"a + (c + (b + d))"; -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t; -"a + (b + (c + d))"; - -"----- but we do not want the parentheses at right; thus: cond.rew."; -"WN0712707 complicated monomials do not yet work ..."; -val t = TermC.str2term "((5*a + 4*d) + 3*c) + 2*b"; -val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t; -if UnparseC.term t = "2 * b + (3 * c + (4 * d + 5 * a))" then () -else error "polyminus.sml: order_add_mult changed"; - -"----- here we see rew_sub going into subterm with ord.rew...."; -val od = ord_make_polynomial false (@{theory "Poly"}); -val t = TermC.str2term "b + a + c + d"; -val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t; -val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t; -(*@@@ rew_sub gosub: t = d + (b + a + c) - @@@ rew_sub begin: t = b + a + c*) - - -\ ML \ -"----------- build predicate for +- ordering ---------------------"; -"----------- build predicate for +- ordering ---------------------"; -"----------- build predicate for +- ordering ---------------------"; -\ ML \ -"======= compare tausche_plus with real_num_collect"; -val od = dummy_ord; - -val erls = erls_ordne_alphabetisch; -val t = TermC.str2term "b + a"; -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t; -if UnparseC.term t = "a + b" then () -else error "polyminus.sml: ordne_alphabetisch1 b + a"; - -val erls = Atools_erls; -val t = TermC.str2term "2*a + 3*a"; -val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term t; - -"======= test rewrite_, rewrite_set_"; -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) -val erls = erls_ordne_alphabetisch; -val t = TermC.str2term "b + a"; -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t; -if UnparseC.term t = "a + b" then () -else error "polyminus.sml: ordne_alphabetisch a + b"; - -val t = TermC.str2term "2*b + a"; -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t; -if UnparseC.term t = "a + 2 * b" then () -else error "polyminus.sml: ordne_alphabetisch a + 2 * b"; - -val t = TermC.str2term "a + c + b"; -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t; -if UnparseC.term t = "a + b + c" then () -else error "polyminus.sml: ordne_alphabetisch a + b + c"; - -\ ML \ -"======= rewrite goes into subterms"; -val t = TermC.str2term "a + c + b + d"; -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; UnparseC.term t; -if UnparseC.term t = "a + b + c + d" then () -else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d"; - -val t = TermC.str2term "a + c + d + b"; -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t; -if UnparseC.term t = "a + b + c + d" then () -else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d"; - -"======= here we see rew_sub going into subterm with cond.rew...."; -val t = TermC.str2term "b + a + c + d"; -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t; -if UnparseC.term t = "a + b + c + d" then () -else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d"; - -"======= compile rls for the most complicated terms"; -val t = TermC.str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; -"5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12"; -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; -if UnparseC.term t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" -then () else error "polyminus.sml: ordne_alphabetisch finished"; - - -\ ML \ -"----------- build fasse_zusammen --------------------------------"; -"----------- build fasse_zusammen --------------------------------"; -"----------- build fasse_zusammen --------------------------------"; -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"; -val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t; -if UnparseC.term t = "3 + -2 * e + 2 * f + 2 * g" then () -else error "polyminus.sml: fasse_zusammen finished"; - -\ ML \ -"----------- build verschoenere ----------------------------------"; -"----------- build verschoenere ----------------------------------"; -"----------- build verschoenere ----------------------------------"; -val t = TermC.str2term "3 + -2 * e + 2 * f + 2 * g"; -val SOME (t,_) = rewrite_set_ thy false verschoenere t; -if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then () -else error "polyminus.sml: verschoenere 3 + -2 * e ..."; - -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) -Rewrite.trace_on:=false; - -\ ML \ -"----------- met simplification for_polynomials with_minus -------"; -"----------- met simplification for_polynomials with_minus -------"; -"----------- met simplification for_polynomials with_minus -------"; -val str = -"Program SimplifyScript (t_t::real) = \ -\ (((Try (Rewrite_Set ordne_alphabetisch False)) #> \ -\ (Try (Rewrite_Set fasse_zusammen False)) #> \ -\ (Try (Rewrite_Set verschoenere False))) t_t)" -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str; -TermC.atomty sc; - -\ ML \ -"----------- me simplification.for_polynomials.with_minus"; -"----------- me simplification.for_polynomials.with_minus"; -"----------- me simplification.for_polynomials.with_minus"; -val c = []; -val (p,_,f,nxt,_,pt) = - CalcTreeTEST - [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", - "normalform N"], - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_minus"]))]; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; - -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -if f2str f = "3 - 2 * e + 2 * f + 2 * g" -then case nxt of End_Proof' => () | _ => error "me simplification.for_polynomials.with_minus 1" -else error "polyminus.sml: me simplification.for_polynomials.with_minus 2"; - -\ ML \ -"----------- pbl polynom vereinfachen p.33 -----------------------"; -"----------- pbl polynom vereinfachen p.33 -----------------------"; -"----------- pbl polynom vereinfachen p.33 -----------------------"; -"----------- 140 c ---"; -reset_states (); -CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", - "normalform N"], - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_minus"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if p = ([], Res) andalso - UnparseC.term (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g" -then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f..."; - -\ ML \ -"======= 140 d ---"; -reset_states (); -CalcTree [(["Term (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)", - "normalform N"], - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_minus"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if p = ([], Res) andalso - UnparseC.term (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t" -then () else error "polyminus.sml: Vereinfache 140 d)"; - -\ ML \ -"======= 139 c ---"; -reset_states (); -CalcTree [(["Term (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)", - "normalform N"], - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_minus"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if p = ([], Res) andalso - UnparseC.term (get_obj g_res pt (fst p)) = "- (3 * f)" -then () else error "polyminus.sml: Vereinfache 139 c)"; - -\ ML \ -"======= 139 b ---"; -reset_states (); -CalcTree [(["Term (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)", - "normalform N"], - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_minus"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if p = ([], Res) andalso - UnparseC.term (get_obj g_res pt (fst p)) = "-3 * u - v" -then () else error "polyminus.sml: Vereinfache 139 b)"; - -\ ML \ -"======= 138 a ---"; -reset_states (); -CalcTree [(["Term (2*u - 3*v - 6*u + 5*v)", - "normalform N"], - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_minus"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if p = ([], Res) andalso - UnparseC.term (get_obj g_res pt (fst p)) = "-4 * u + 2 * v" -then () else error "polyminus.sml: Vereinfache 138 a)"; - -\ ML \ -"----------- met probe fuer_polynom ------------------------------"; -"----------- met probe fuer_polynom ------------------------------"; -"----------- met probe fuer_polynom ------------------------------"; -val str = -"Program ProbeScript (e_e::bool) (w_s::bool list) =\ -\ (let e_e = Take e_e; \ -\ e_e = Substitute w_s e_e \ -\ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #> \ -\ (Try (Repeat (Calculate ''PLUS''))) #> \ -\ (Try (Repeat (Calculate ''MINUS''))))) e_e)" -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str; -TermC.atomty sc; - -\ ML \ -"----------- pbl polynom probe -----------------------------------"; -"----------- pbl polynom probe -----------------------------------"; -"----------- pbl polynom probe -----------------------------------"; -reset_states (); -CalcTree [(["Pruefe ((5::int)*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\ - \3 - 2 * e + 2 * f + 2 * (g::int))", - "mitWert [e = (1::int), f = (2::int), g = (3::int)]", - "Geprueft b"], - ("PolyMinus",["polynom", "probe"], - ["probe", "fuer_polynom"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -(* autoCalculate 1 CompleteCalcHead; - autoCalculate 1 (Steps 1); - autoCalculate 1 (Steps 1); - val ((pt,p),_) = get_calc 1; UnparseC.term (get_obj g_res pt (fst p)); -@@@@@WN081114 gives "??.empty", all "Pruefe" are the same, -although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*) -val ((pt,p),_) = get_calc 1; -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "11 = 11" -then () else error "polyminus.sml: Probe 11 = 11"; -Test_Tool.show_pt pt; - -\ ML \ -"----------- pbl klammer polynom vereinfachen p.34 ---------------"; -"----------- pbl klammer polynom vereinfachen p.34 ---------------"; -"----------- pbl klammer polynom vereinfachen p.34 ---------------"; -reset_states (); -CalcTree [(["Term (2*u - 5 - (3 - 4*u) + (8*u + 9))", - "normalform N"], - ("PolyMinus",["klammer", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_parentheses"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; -if p = ([], Res) andalso - UnparseC.term (get_obj g_res pt (fst p)) = "1 + 14 * u" -then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ..."; -Test_Tool.show_pt pt; - -\ ML \ -"======= probe p.34 -----"; -reset_states (); -CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * (u::int))", - "mitWert [u = (2::int)]", - "Geprueft b"], - ("PolyMinus",["polynom", "probe"], - ["probe", "fuer_polynom"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "29 = 29" -then () else error "polyminus.sml: Probe 29 = 29"; -Test_Tool.show_pt pt; - -\ ML \ -"----------- try fun applyTactics --------------------------------"; -"----------- try fun applyTactics --------------------------------"; -"----------- try fun applyTactics --------------------------------"; -reset_states (); -CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", - "normalform N"], - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_minus"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalcHead; -autoCalculate 1 (Steps 1); -autoCalculate 1 (Steps 1); -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -"----- 1 \ "; -fetchApplicableTactics 1 0 p; -val appltacs = specific_from_prog pt p; -applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*); -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -"----- 2 \ "; -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) -val erls = erls_ordne_alphabetisch; -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g"; -\ ML \ -\ ML \ -val SOME (t',_) = - rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus} t; -UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g"; - -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g"; -val NONE = - rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus_plus} t; - -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g"; -val SOME (t',_) = - rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t; -UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f"; -Rewrite.trace_on := false; - - -applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*); -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -"----- 3 \ "; -applyTactic 1 p (hd (specific_from_prog pt p)) (**); -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -"----- 4 \ "; -applyTactic 1 p (hd (specific_from_prog pt p)) (**); -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -"----- 5 \ "; -applyTactic 1 p (hd (specific_from_prog pt p)) (**); -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -"----- 6 \ "; - -(* failure -applyTactic 1 p (hd (specific_from_prog pt p)) (**); -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -"----- 7 \ "; -*) -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -(*independent from failure above: met_simp_poly_minus not confluent: -(([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)), -(([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))] -~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*) - - -\ ML \ -"#############################################################################"; -reset_states (); -CalcTree [(["Term (- (8 * g) + 10 * g + h)", - "normalform N"], - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_minus"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "2 * g + h" -then () else error "polyminus.sml: addiere_vor_minus"; - - -\ ML \ -"#############################################################################"; -reset_states (); -CalcTree [(["Term (- (8 * g) + 10 * g + f)", - "normalform N"], - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_minus"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "f + 2 * g" -then () else error "polyminus.sml: tausche_vor_plus"; - -\ ML \ -"----------- pbl binom polynom vereinfachen p.39 -----------------"; -"----------- pbl binom polynom vereinfachen p.39 -----------------"; -"----------- pbl binom polynom vereinfachen p.39 -----------------"; -val rls = klammern_ausmultiplizieren; -val t = TermC.str2term "(3 * a + 2) * (4 * a - 1)"; -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t; -"3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)"; -val rls = discard_parentheses; -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t; -"3 * a * 4 * a - 3 * a * 1 + (2 * 4 * a - 2 * 1)"; -val rls = ordne_monome; -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t; -"3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)"; -(* -val t = TermC.str2term "3 * a * 4 * a"; -val rls = ordne_monome; -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t; -*) -val rls = klammern_aufloesen; -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t; -"3 * 4 * a * a - 1 * 3 * a + 2 * 4 * a - 1 * 2"; -val rls = ordne_alphabetisch; -(*TODO: make is_monom more general, a*a=a^2, ...*) -\ ML \ -\ ML \ -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t; -"3 * 4 * a * a - 1 * 2 - 1 * 3 * a + 2 * 4 * a"; -(*STOPPED.WN080104 -val rls = fasse_zusammen; -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t; -val rls = verschoenere; -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t; -*) - -\ ML \ -(*@@@@@@@*) -reset_states (); -CalcTree [(["Term ((3*a + 2) * (4*a - 1))", - "normalform N"], - ("PolyMinus",["binom_klammer", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_parentheses_mult"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -\ ML \ -UnparseC.term (get_obj g_res pt (fst p)) = "12 * a \ 2 - 2 + 5 * a" (*monoms-order NOTok*) -\ ML \ -if p = ([], Res) andalso - UnparseC.term (get_obj g_res pt (fst p)) = "-2 + 12 * a \ 2 + 5 * a" -then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ..."; - -\ ML \ -"----------- pbl binom polynom vereinfachen: cube ----------------"; -"----------- pbl binom polynom vereinfachen: cube ----------------"; -"----------- pbl binom polynom vereinfachen: cube ----------------"; -reset_states (); -CalcTree [(["Term (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"], - ("PolyMinus",["binom_klammer", "polynom", "vereinfachen"], - ["simplification", "for_polynomials", "with_parentheses_mult"]))]; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -\ ML \ -UnparseC.term (get_obj g_res pt (fst p)) = "9 * a - 10 * q + 3 * a - 6 * q" -\ ML \ -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "12 * a - 16 * q" -then () else error "pbl binom polynom vereinfachen: cube"; - -\ ML \ -"----------- Refine.refine Vereinfache ----------------------------------"; -"----------- Refine.refine Vereinfache ----------------------------------"; -"----------- Refine.refine Vereinfache ----------------------------------"; -val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"]; -(*default_print_depth 11;*) -val matches = Refine.refine fmz ["vereinfachen"]; -(*default_print_depth 3;*) - -"----- go into details, if it seems not to work -----"; -"--- does the predicate evaluate correctly ?"; -val t = TermC.str2term - "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))"; -val ma = eval_matchsub "" "Prog_Expr.matchsub" t thy; -case ma of - SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \ - \a - 2 * q + 3 * (a - 2 * q)) = True", _) => () - | _ => error "polyminus.sml matchsub (?a * (?b - ?c)...A"; - -"--- does the respective prls rewrite ?"; -val prls = Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty - [Eval ("Poly.is_polyexp", eval_is_polyexp ""), - Eval ("Prog_Expr.matchsub", eval_matchsub ""), - Thm ("or_true",@{thm or_true}), - (*"(?a | True) = True"*) - Thm ("or_false",@{thm or_false}), - (*"(?a | False) = ?a"*) - Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}), - (*"(~ True) = False"*) - Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}) - (*"(~ False) = True"*)]; -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) -val SOME (t', _) = rewrite_set_ thy false prls t; -Rewrite.trace_on := false; - -"--- does the respective prls rewrite the whole predicate ?"; -val t = TermC.str2term - "Not (matchsub (?a * (?b + ?c)) (8 * (a - q) + a - 2 * q) | \ - \ matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \ - \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \ - \ matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )"; -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) -val SOME (t', _) = rewrite_set_ thy false prls t; -Rewrite.trace_on := false; -if UnparseC.term t' = "False" then () -else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ..."; - -\ ML \ -"----------- *** Problem.prep_input: syntax error in '#Where' of [v"; -"----------- *** Problem.prep_input: syntax error in '#Where' of [v"; -"----------- *** Problem.prep_input: syntax error in '#Where' of [v"; -(*see test/../termC.sml for details*) -val t = TermC.parse_patt thy "t_t is_polyexp"; -val t = TermC.parse_patt thy ("Not (matchsub (?a + (?b + ?c)) t_t | " ^ - " matchsub (?a + (?b - ?c)) t_t | " ^ - " matchsub (?a - (?b + ?c)) t_t | " ^ - " matchsub (?a + (?b - ?c)) t_t )"); -(*show_types := true; -if UnparseC.term t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)" -then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1"; -show_types := false;*) -if UnparseC.term t = - "\ (matchsub (?a + (?b + ?c)) t_t \\n " ^ - "matchsub (?a + (?b - ?c)) t_t \\n " ^ - "matchsub (?a - (?b + ?c)) t_t \ " ^ - "matchsub (?a + (?b - ?c)) t_t)" -then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1"; - \ ML \ \ ML \ \