1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Thu Jul 15 14:10:18 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Thu Jul 15 20:02:16 2021 +0200
1.3 @@ -110,67 +110,64 @@
1.4 (** eval functions **)
1.5
1.6 (*. get the identifier from specific monomials; see fun ist_monom .*)
1.7 -(*HACK.WN080107*)
1.8 -fun increase str =
1.9 - let
1.10 - val (s, ss) =
1.11 - case Symbol.explode str of
1.12 - s :: ss => (s, ss)
1.13 - | _ => raise ERROR "PolyMinus.increase: uncovered case"
1.14 - in implode ((chr (ord s + 1))::ss) end;
1.15 -fun identifier (Free (id,_)) = id (* 2 , a *)
1.16 - | identifier (Const ("Groups.times_class.times", _) $ Free (_(*num*), _) $ Free (id, _)) =
1.17 - id (* 2*a , a*b *)
1.18 - | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
1.19 - (Const ("Groups.times_class.times", _) $
1.20 - Free (num, _) $ Free _) $ Free (id, _)) =
1.21 - if TermC.is_num' num then id
1.22 +fun identifier (Free (id, _)) = id (* //2, a *)
1.23 +(*TOODOO*)
1.24 + | identifier (* 3*a*b *)
1.25 + (Const ("Groups.times_class.times", _) $ (Const ("Groups.times_class.times", _) $
1.26 + num $ t) $ Free (id, _)) =
1.27 + if TermC.is_num num andalso TermC.is_atom t then id
1.28 else "|||||||||||||"
1.29 - | identifier (Const ("Transcendental.powr", _) $ Free (base, _) $ Free (_(*exp*), _)) =
1.30 - if TermC.is_num' base then "|||||||||||||" (* a^2 *)
1.31 - else (*increase*) base
1.32 - | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
1.33 - (Const ("Transcendental.powr", _) $
1.34 - Free (base, _) $ Free (_(*exp*), _))) =
1.35 - if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base
1.36 +
1.37 + | identifier (* 2*a, a*b *)
1.38 + (Const ("Groups.times_class.times", _) $ num $ Free (id, _)) =
1.39 + if TermC.is_atom num then id
1.40 else "|||||||||||||"
1.41 - | identifier _ = "|||||||||||||"(*the "largest" string*);
1.42 +
1.43 + | identifier (Const ("Transcendental.powr", _) $ base $ exp) = (* a^2 *)
1.44 + if TermC.is_num base andalso TermC.is_atom exp then "|||||||||||||"
1.45 + else TermC.string_of_atom base
1.46 +
1.47 + | identifier (* 3*a^2 *)
1.48 + (Const ("Groups.times_class.times", _) $ num $
1.49 + (Const ("Transcendental.powr", _) $ base $ exp )) =
1.50 + if TermC.is_num num andalso not (TermC.is_num base) andalso TermC.is_atom exp
1.51 + then TermC.string_of_atom base
1.52 + else "|||||||||||||"
1.53 +
1.54 + | identifier t =
1.55 + if TermC.is_num t then TermC.string_of_num t (* 2 , //a *)
1.56 + else "|||||||||||||"; (*the "largest" string*)
1.57
1.58 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
1.59 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
1.60 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
1.61 - if TermC.is_num b then
1.62 - if TermC.is_num a then (*123 kleiner 32 = True !!!*)
1.63 - if TermC.num_of_term a < TermC.num_of_term b then
1.64 - SOME ((UnparseC.term p) ^ " = True",
1.65 - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.66 - else SOME ((UnparseC.term p) ^ " = False",
1.67 - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.68 - else (* -1 * -2 kleiner 0 *)
1.69 - SOME ((UnparseC.term p) ^ " = False",
1.70 - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.71 + if TermC.is_num b then
1.72 + if TermC.is_num a then (*123 kleiner 32 = True !!!*)
1.73 + if TermC.num_of_term a < TermC.num_of_term b then
1.74 + SOME ((UnparseC.term p) ^ " = True",
1.75 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.76 + else SOME ((UnparseC.term p) ^ " = False",
1.77 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.78 + else (* -1 * -2 kleiner 0 *)
1.79 + SOME ((UnparseC.term p) ^ " = False",
1.80 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.81 else
1.82 - if identifier a < identifier b then
1.83 - SOME ((UnparseC.term p) ^ " = True",
1.84 - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.85 - else SOME ((UnparseC.term p) ^ " = False",
1.86 - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.87 + if identifier a < identifier b then
1.88 + SOME ((UnparseC.term p) ^ " = True",
1.89 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.90 + else SOME ((UnparseC.term p) ^ " = False",
1.91 + HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.92 | eval_kleiner _ _ _ _ = NONE;
1.93
1.94 -fun ist_monom (Free _) = true (* 2, a *)
1.95 - | ist_monom (Const ("Groups.times_class.times", _) $
1.96 - (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) = true
1.97 - | ist_monom (Const ("Groups.times_class.times", _) $ (* 2*a, a*b *)
1.98 - Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = false
1.99 - | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
1.100 - (Const ("Groups.times_class.times", _) $
1.101 - (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) $ Free _) = true
1.102 - | ist_monom (Const ("Transcendental.powr", _) $ (* a^2 *)
1.103 - Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = true
1.104 - | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a^2 *)
1.105 - (Const ("Num.numeral_class.numeral", _) $ _) $
1.106 - (Const ("Transcendental.powr", _) $ Free _ $ Free _)) = true
1.107 - | ist_monom _ = false;
1.108 +fun ist_monom t =
1.109 + if TermC.is_atom t then true
1.110 + else
1.111 + case t of
1.112 + Const ("Groups.times_class.times", _) $ t1 $ t2 =>
1.113 + ist_monom t1 andalso ist_monom t2
1.114 + | Const ("Transcendental.powr", _) $ t1 $ t2 =>
1.115 + ist_monom t1 andalso ist_monom t2
1.116 + | _ => false
1.117
1.118 (* is this a univariate monomial ? *)
1.119 (*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*)
1.120 @@ -188,8 +185,8 @@
1.121 (** rulesets **)
1.122
1.123 val erls_ordne_alphabetisch =
1.124 - Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty
1.125 - [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""),
1.126 + Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty
1.127 + [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""),
1.128 Rule.Eval ("PolyMinus.ist_monom", eval_ist_monom "")
1.129 ];
1.130
2.1 --- a/test/Pure/Isar/Test_Parsers.thy Thu Jul 15 14:10:18 2021 +0200
2.2 +++ b/test/Pure/Isar/Test_Parsers.thy Thu Jul 15 20:02:16 2021 +0200
2.3 @@ -145,7 +145,7 @@
2.4 (Args.$$$ "theory" -- Args.name);
2.5 parse (Args.$$$ "theory" -- Args.name);
2.6 (*
2.7 -parse (Args.$$$ "theory") GOON ?!?!?
2.8 +parse (Args.$$$ "theory") ?!?!?
2.9 "theory";
2.10
2.11 parse (Args.$$$ "theory")
2.12 @@ -440,8 +440,8 @@
2.13 parse (body "") "top bullet top";
2.14 \<close>
2.15
2.16 -section \<open>GOON\<close>
2.17 -subsection \<open>GOON\<close>
2.18 +section \<open>xxx\<close>
2.19 +subsection \<open>xxx\<close>
2.20
2.21
2.22 end
2.23 \ No newline at end of file
3.1 --- a/test/Tools/isac/Knowledge/poly.sml Thu Jul 15 14:10:18 2021 +0200
3.2 +++ b/test/Tools/isac/Knowledge/poly.sml Thu Jul 15 20:02:16 2021 +0200
3.3 @@ -1430,10 +1430,10 @@
3.4 (*SO: WHY IS THERE NO REWRITING ...*)
3.5
3.6 val term = TermC.str2term "2*b + (3*a + 3*b)";
3.7 -(*+++*)val SOME (t', []) = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term;
3.8 -(*+++*)if UnparseC.term t' = "a * 3 + (b * 2 + b * 3)" then () else error "no rewriting ?!?";
3.9 -(* before dropping ThmC.numerals_to_Free this was
3.10 -val NONE = rewrite_set_ @ {theory "Isac_Knowledge"} false order_add_mult term;
3.11 -SO: WHY IS THERE NO REWRITING ?!?
3.12 +(*+++*)val NONE = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term;
3.13 +(*
3.14 +WHY IS THERE NO REWRITING ?!?
3.15 +most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML,
3.16 +while order_add_mult uses isac's rewriter -- and this is used rarely!
3.17 *)
3.18
4.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Thu Jul 15 14:10:18 2021 +0200
4.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu Jul 15 20:02:16 2021 +0200
4.3 @@ -7,7 +7,7 @@
4.4 "--------------------------------------------------------";
4.5 "table of contents --------------------------------------";
4.6 "--------------------------------------------------------";
4.7 -"----------- fun contains_mult_pot_only --------------------------------------------------------";
4.8 +"----------- fun identifier --------------------------------------------------------------------";
4.9 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
4.10 "----------- fun ist_monom ---------------------------------------------------------------------";
4.11 "----------- fun eval_ist_monom -------------------------";
4.12 @@ -32,40 +32,57 @@
4.13
4.14 val thy = @{theory "PolyMinus"};
4.15
4.16 -"----------- fun contains_mult_pot_only --------------------------------------------------------";
4.17 -"----------- fun contains_mult_pot_only --------------------------------------------------------";
4.18 -"----------- fun contains_mult_pot_only --------------------------------------------------------";
4.19 -val t = @{term 0};
4.20 - if contains_mult_pot_only t then () else error "contains_mult_pot_only 1";
4.21 +"----------- fun identifier --------------------------------------------------------------------";
4.22 +"----------- fun identifier --------------------------------------------------------------------";
4.23 +"----------- fun identifier --------------------------------------------------------------------";
4.24 +if identifier (TermC.str2term "12 ::real") = "12" then () else error "identifier 1";
4.25 +if identifier (TermC.str2term "a ::real") = "a" then () else error "identifier 2";
4.26 +if identifier (TermC.str2term "3 * a ::real") = "a" then () else error "identifier 3";
4.27 +if identifier (TermC.str2term "a \<up> 2 ::real") = "a" then () else error "identifier 4";
4.28 +if identifier (TermC.str2term "3*a \<up> 2 ::real") = "a" then () else error "identifier 5";
4.29 +if identifier (TermC.str2term "a * b ::real") = "b" then () else error "identifier 5b";
4.30
4.31 -val t = @{term "a"};
4.32 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 2";
4.33 -
4.34 -val t = @{term "2 * a"};
4.35 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 3";
4.36 -
4.37 -val t = @{term "2 * a * b"};
4.38 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 4";
4.39 -
4.40 -val t = @{term "a * b"};
4.41 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 5";
4.42 -
4.43 -val t = @{term "2 * a \<up> 2 * b"};
4.44 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 6";
4.45 -
4.46 -val t = @{term "a \<up> 2 * b \<up> 3"};
4.47 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 7";
4.48 -
4.49 -(* but also ..*)
4.50 -val t = @{term "a \<up> 2 * 4 * b \<up> 3 * 5"};
4.51 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 8";
4.52 +(*these are strange (see "specific monomials" in comment to fun.def.)..*)
4.53 +if identifier (TermC.str2term "a*b ::real") = "b" then () else error "identifier 6";
4.54 +if identifier (TermC.str2term "(3*a*b) ::real") = "b" then () else error "identifier 7";
4.55
4.56
4.57 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
4.58 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
4.59 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
4.60 +"a" < "b";
4.61 +"ba" < "ab";
4.62 +"123" < "a"; (*unused due to ---vvv*)
4.63 +"12" < "3"; (*true !!!*)
4.64 +
4.65 +" a kleiner b ==> (b + a) = (a + b)";
4.66 +TermC.str2term "aaa";
4.67 +TermC.str2term "222 * aaa";
4.68 +
4.69 +case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
4.70 + SOME ("123 kleiner 32 = False", _) => ()
4.71 + | _ => error "polyminus.sml: 12 kleiner 9 = False";
4.72 +case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of
4.73 + SOME ("a kleiner b = True", _) => ()
4.74 + | _ => error "polyminus.sml: a kleiner b = True";
4.75 +case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of
4.76 + SOME ("10 * g kleiner f = False", _) => ()
4.77 + | _ => error "polyminus.sml: 10 * g kleiner f = False";
4.78 +case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
4.79 + SOME ("a \<up> 2 kleiner b = True", _) => ()
4.80 + | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
4.81 +case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
4.82 + SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
4.83 + | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
4.84 +case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
4.85 + SOME ("a * b kleiner c = True", _) => ()
4.86 + | _ => error "polyminus.sml: a * b kleiner b = True";
4.87 +case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of
4.88 + SOME ("3 * a * b kleiner c = True", _) => ()
4.89 + | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
4.90 +
4.91 +
4.92 val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
4.93 -
4.94 val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
4.95 eval_kleiner "aaa" "bbb" t "ccc";
4.96 "~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const ("PolyMinus.kleiner",_) $ a $ b)), _) =
4.97 @@ -74,17 +91,45 @@
4.98
4.99 (*if*) identifier a < identifier b (*else*);
4.100 "~~~~~ fun identifier , args:"; val (t) = (a);
4.101 -
4.102 (*+*)case a of
4.103 Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $
4.104 (Const ("Num.num.Bit0", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)))) => ()
4.105 -| _ => error "eval_kleiner CHANGED";
4.106 +| _ => error "eval_kleiner CHANGED"; (*isa*)
4.107 +
4.108 +
4.109 +"----------- fun ist_monom ---------------------------------------------------------------------";
4.110 +"----------- fun ist_monom ---------------------------------------------------------------------";
4.111 +"----------- fun ist_monom ---------------------------------------------------------------------";
4.112 +val t = TermC.str2term "0 ::real";
4.113 + if ist_monom t then () else error "ist_monom 1";
4.114 +
4.115 +val t = TermC.str2term "a";
4.116 +if ist_monom t then () else error "ist_monom 2";
4.117 +
4.118 +val t = TermC.str2term "2 * a";
4.119 +if ist_monom t then () else error "ist_monom 3";
4.120 +
4.121 +val t = TermC.str2term "2 * a * b";
4.122 +if ist_monom t then () else error "ist_monom 4";
4.123 +
4.124 +val t = TermC.str2term "a * b";
4.125 +if ist_monom t then () else error "ist_monom 5";
4.126 +
4.127 +(*not covered before NEW numerals*)
4.128 +val t = TermC.str2term "2 * a \<up> 2 * b";
4.129 +if ist_monom t then () else error "ist_monom 6";
4.130 +
4.131 +(*not covered before NEW numerals*)
4.132 +val t = TermC.str2term "a \<up> 2 * b \<up> 3";
4.133 +if ist_monom t then () else error "ist_monom 7";
4.134 +
4.135 +val t = TermC.str2term "a \<up> 2 * 4 * b \<up> 3 * 5";
4.136 +if ist_monom t then () else error "ist_monom 8";
4.137
4.138
4.139 "----------- fun eval_ist_monom ----------------------------------";
4.140 "----------- fun eval_ist_monom ----------------------------------";
4.141 "----------- fun eval_ist_monom ----------------------------------";
4.142 -ist_monom (TermC.str2term "12");
4.143 case eval_ist_monom 0 0 (TermC.str2term "12 ist_monom") 0 of
4.144 SOME ("12 ist_monom = True", _) => ()
4.145 | _ => error "polyminus.sml: 12 ist_monom = True";
4.146 @@ -239,7 +284,7 @@
4.147 else error "polyminus.sml: ordne_alphabetisch a + b + c";
4.148
4.149 "======= rewrite goes into subterms";
4.150 -val t = TermC.str2term "a + c + b + d";
4.151 +val t = TermC.str2term "a + c + b + d ::real";
4.152 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; UnparseC.term t;
4.153 if UnparseC.term t = "a + b + c + d" then ()
4.154 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
4.155 @@ -268,7 +313,7 @@
4.156 "----------- build fasse_zusammen --------------------------------";
4.157 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
4.158 val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t;
4.159 -if UnparseC.term t = "3 + -2 * e + 2 * f + 2 * g" then ()
4.160 +if UnparseC.term t = "3 + - 2 * e + 2 * f + 2 * g" then ()
4.161 else error "polyminus.sml: fasse_zusammen finished";
4.162
4.163 "----------- build verschoenere ----------------------------------";
4.164 @@ -311,11 +356,17 @@
4.165 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.166
4.167 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.168 + f2str f = "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12"; (*isa == isa2*)
4.169 +val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt;
4.170 + val (*^^^*) Rewrite_Set "ordne_alphabetisch" = nxt;
4.171 + f2str f = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"; (*isa2*)
4.172 +val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
4.173 + f2str f = "3 + - 2 * e + 2 * f + 2 * g"; (*isa2*)
4.174 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.175 + f2str f = "3 - 2 * e + 2 * f + 2 * g"; (*isa2*)
4.176 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.177 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.178 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.179 -if f2str f = "3 - 2 * e + 2 * f + 2 * g"
4.180 + f2str f = "3 - 2 * e + 2 * f + 2 * g"; (*isa2*)
4.181 +if f2str f = "3 - 2 * e + 2 * f + 2 * g" (*isa2*)
4.182 then case nxt of End_Proof' => () | _ => error "me simplification.for_polynomials.with_minus 1"
4.183 else error "polyminus.sml: me simplification.for_polynomials.with_minus 2";
4.184
4.185 @@ -371,7 +422,7 @@
4.186 autoCalculate 1 CompleteCalc;
4.187 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
4.188 if p = ([], Res) andalso
4.189 - UnparseC.term (get_obj g_res pt (fst p)) = "-3 * u - v"
4.190 + UnparseC.term (get_obj g_res pt (fst p)) = "- 3 * u - v"
4.191 then () else error "polyminus.sml: Vereinfache 139 b)";
4.192
4.193 "======= 138 a ---";
4.194 @@ -384,7 +435,7 @@
4.195 autoCalculate 1 CompleteCalc;
4.196 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
4.197 if p = ([], Res) andalso
4.198 - UnparseC.term (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"
4.199 + UnparseC.term (get_obj g_res pt (fst p)) = "- 4 * u + 2 * v"
4.200 then () else error "polyminus.sml: Vereinfache 138 a)";
4.201
4.202 "----------- met probe fuer_polynom ------------------------------";
4.203 @@ -582,8 +633,10 @@
4.204 moveActiveRoot 1;
4.205 autoCalculate 1 CompleteCalc;
4.206 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
4.207 -if p = ([], Res) andalso
4.208 - UnparseC.term (get_obj g_res pt (fst p)) = "-2 + 12 * a \<up> 2 + 5 * a"
4.209 +
4.210 +if p = ([], Res) andalso
4.211 + UnparseC.term (get_obj g_res pt (fst p)) =(*"- 2 + 12 * a \<up> 2 + 5 * a" with OLD numerals*)
4.212 + "- 2 + 5 * a + 12 * a \<up> 2"
4.213 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
4.214
4.215 "----------- pbl binom polynom vereinfachen: cube ----------------";
5.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Jul 15 14:10:18 2021 +0200
5.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Jul 15 20:02:16 2021 +0200
5.3 @@ -512,13 +512,14 @@
5.4 \<close> ML \<open>
5.5 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
5.6 \<close> ML \<open>
5.7 -val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
5.8 +(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
5.9 \<close> ML \<open>
5.10 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
5.11
5.12 \<close> ML \<open>
5.13 -f
5.14 +(*+*)val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f
5.15 \<close> ML \<open>
5.16 +\<close> ML \<open> (*GOON*)
5.17 map Tactic.input_to_string (specific_from_prog pt p)
5.18 \<close> ML \<open>
5.19 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
5.20 @@ -971,6 +972,18 @@
5.21 ML_file "Knowledge/descript.sml"
5.22 ML_file "Knowledge/simplify.sml"
5.23 ML_file "Knowledge/poly.sml"
5.24 +ML \<open>
5.25 +\<close> ML \<open>
5.26 +\<close> ML \<open>
5.27 +\<close> ML \<open>
5.28 +\<close> ML \<open>
5.29 +\<close> ML \<open>
5.30 +\<close> ML \<open>
5.31 +\<close> ML \<open>
5.32 +\<close> ML \<open>
5.33 +\<close> ML \<open>
5.34 +\<close> ML \<open>
5.35 +\<close>
5.36 ML_file "Knowledge/gcd_poly_ml.sml"
5.37 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
5.38 ML_file "Knowledge/rational.sml" (*Test_Isac_Short*)
6.1 --- a/test/Tools/isac/Test_Some.thy Thu Jul 15 14:10:18 2021 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Thu Jul 15 20:02:16 2021 +0200
6.3 @@ -101,815 +101,23 @@
6.4 \<close> ML \<open>
6.5 \<close>
6.6
6.7 -section \<open>======= NEW src/../PolyMinus.thy ==================================================\<close>
6.8 +section \<open>===================================================================================\<close>
6.9 ML \<open>
6.10 \<close> ML \<open>
6.11 -\<close> ML \<open> (* \<longrightarrow> PolyMinus.thy *)
6.12 -fun identifier (Const ("Groups.times_class.times", _) $ Free (_(*num*), _) $ Free (id, _)) =
6.13 - id (* 2*a , a*b *)
6.14 - | identifier (Const ("Groups.times_class.times", _) $ (Const ("Groups.times_class.times", _) $
6.15 - Free (num, _) $ Free _) $ Free (id, _)) = (* 3*a*b *)
6.16 - if TermC.is_num' num then id
6.17 - else "|||||||||||||"
6.18 - | identifier (Const ("Transcendental.powr", _) $ Free (base, _) $ Free (_(*exp*), _)) =
6.19 - if TermC.is_num' base then "|||||||||||||" (* a^2 *)
6.20 - else (*increase*) base
6.21 - | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
6.22 - (Const ("Transcendental.powr", _) $ Free (base, _) $ Free (_(*exp*), _))) =
6.23 - if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base
6.24 - else "|||||||||||||"
6.25 - | identifier (Free (str, _)) = str (* a *)
6.26 - | identifier t =
6.27 - if TermC.is_atom t then TermC.string_of_atom t
6.28 - else "|||||||||||||"; (*the "largest" string*)
6.29 -
6.30 -\<close> ML \<open> (* \<longrightarrow> PolyMinus.thy *)
6.31 -fun ist_monom t =
6.32 - if TermC.is_atom t then true
6.33 - else
6.34 - case t of
6.35 - Const ("Groups.times_class.times", _) $ t1 $ t2 =>
6.36 - ist_monom t1 andalso ist_monom t2
6.37 - | Const ("Transcendental.powr", _) $ t1 $ t2 =>
6.38 - ist_monom t1 andalso ist_monom t2
6.39 - | _ => false
6.40 -
6.41 -\<close> ML \<open> (* \<longrightarrow> PolyMinus.thy *)
6.42 -fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
6.43 - if TermC.is_num b then
6.44 - if TermC.is_num a then (*123 kleiner 32 = True !!!*)
6.45 - if TermC.num_of_term a < TermC.num_of_term b then
6.46 - SOME ((UnparseC.term p) ^ " = True",
6.47 - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
6.48 - else SOME ((UnparseC.term p) ^ " = False",
6.49 - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
6.50 - else (* -1 * -2 kleiner 0 *)
6.51 - SOME ((UnparseC.term p) ^ " = False",
6.52 - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
6.53 - else
6.54 - if identifier a < identifier b then
6.55 - SOME ((UnparseC.term p) ^ " = True",
6.56 - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
6.57 - else SOME ((UnparseC.term p) ^ " = False",
6.58 - HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
6.59 - | eval_kleiner _ _ _ _ = NONE;
6.60 +\<close> ML \<open>
6.61 \<close> ML \<open>
6.62 \<close>
6.63
6.64 -section \<open>======= test/../polyminus.sml =====================================================\<close>
6.65 +section \<open>===================================================================================\<close>
6.66 ML \<open>
6.67 \<close> ML \<open>
6.68 -(* title: Knowledge/polyminus.sml
6.69 - author: Walther Neuper
6.70 - WN071207,
6.71 - (c) due to copyright terms
6.72 -*)
6.73 -"--------------------------------------------------------";
6.74 -"--------------------------------------------------------";
6.75 -"table of contents --------------------------------------";
6.76 -"--------------------------------------------------------";
6.77 -"----------- fun identifier --------------------------------------------------------------------";
6.78 -"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
6.79 -"----------- fun eval_ist_monom -------------------------";
6.80 -"----------- watch order_add_mult ----------------------";
6.81 -"----------- build predicate for +- ordering ------------";
6.82 -"----------- build fasse_zusammen -----------------------";
6.83 -"----------- build verschoenere -------------------------";
6.84 -"----------- met simplification for_polynomials with_minu";
6.85 -"----------- me simplification.for_polynomials.with_minus";
6.86 -"----------- pbl polynom vereinfachen p.33 --------------";
6.87 -"----------- met probe fuer_polynom ---------------------";
6.88 -"----------- pbl polynom probe --------------------------";
6.89 -"----------- pbl klammer polynom vereinfachen p.34 ------";
6.90 -"----------- try fun applyTactics -----------------------";
6.91 -"----------- pbl binom polynom vereinfachen p.39 --------";
6.92 -"----------- pbl binom polynom vereinfachen: cube -------";
6.93 -"----------- Refine.refine Vereinfache -------------------------";
6.94 -"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
6.95 -"--------------------------------------------------------";
6.96 -"--------------------------------------------------------";
6.97 -"--------------------------------------------------------";
6.98 +\<close> ML \<open>
6.99 +\<close> ML \<open>
6.100 +\<close>
6.101
6.102 -val thy = @{theory "PolyMinus"};
6.103 -
6.104 -"----------- fun identifier --------------------------------------------------------------------";
6.105 -"----------- fun identifier --------------------------------------------------------------------";
6.106 -"----------- fun identifier --------------------------------------------------------------------";
6.107 +section \<open>===================================================================================\<close>
6.108 +ML \<open>
6.109 \<close> ML \<open>
6.110 -if identifier (TermC.str2term "12 ::real") = "12" then () else error "identifier 1";
6.111 -if identifier (TermC.str2term "a ::real") = "a" then () else error "identifier 2";
6.112 -if identifier (TermC.str2term "3 * a ::real") = "a" then () else error "identifier 3";
6.113 -if identifier (TermC.str2term "a \<up> 2 ::real") = "a" then () else error "identifier 4";
6.114 -if identifier (TermC.str2term "3*a \<up> 2 ::real") = "a" then () else error "identifier 5";
6.115 -
6.116 -(*these are strange ..*)
6.117 -if identifier (TermC.str2term "a*b ::real") = "b" then () else error "identifier 6";
6.118 -if identifier (TermC.str2term "(3*a*b) ::real") = "b" then () else error "identifier 7";
6.119 -
6.120 -\<close> ML \<open>
6.121 -"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
6.122 -"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
6.123 -"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
6.124 -"a" < "b";
6.125 -"ba" < "ab";
6.126 -"123" < "a"; (*unused due to ---vvv*)
6.127 -"12" < "3"; (*true !!!*)
6.128 -
6.129 -" a kleiner b ==> (b + a) = (a + b)";
6.130 -TermC.str2term "aaa";
6.131 -TermC.str2term "222 * aaa";
6.132 -
6.133 -\<close> ML \<open>
6.134 -case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
6.135 - SOME ("123 kleiner 32 = False", _) => ()
6.136 - | _ => error "polyminus.sml: 12 kleiner 9 = False";
6.137 -
6.138 -\<close> ML \<open>
6.139 -case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of
6.140 - SOME ("a kleiner b = True", _) => ()
6.141 - | _ => error "polyminus.sml: a kleiner b = True";
6.142 -
6.143 -\<close> ML \<open>
6.144 -case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of
6.145 - SOME ("10 * g kleiner f = False", _) => ()
6.146 - | _ => error "polyminus.sml: 10 * g kleiner f = False";
6.147 -
6.148 -\<close> ML \<open>
6.149 -case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
6.150 - SOME ("a \<up> 2 kleiner b = True", _) => ()
6.151 - | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
6.152 -
6.153 -\<close> ML \<open>
6.154 -"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const ("PolyMinus.kleiner",_) $ a $ b)), _) =
6.155 - ( 0, 0, (TermC.str2term "(a \<up> 2) kleiner b"), 0);
6.156 -\<close> ML \<open>
6.157 - (*if*) TermC.is_num b (*else*);
6.158 -\<close> ML \<open>
6.159 - (*if*) identifier a < identifier b (*else*);
6.160 -\<close> ML \<open>
6.161 -(*+*) identifier a = "|||||||||||||"; (*isa*)
6.162 -(*+*) identifier a = "a"; (*isa2*)
6.163 -\<close> ML \<open>
6.164 -(*+*) identifier b = "b"; (*isa == isa2*)
6.165 -\<close> ML \<open>
6.166 -\<close> ML \<open>
6.167 -\<close> ML \<open>
6.168 -\<close> ML \<open>
6.169 -\<close> ML \<open>
6.170 -\<close> ML \<open>
6.171 -\<close> ML \<open>
6.172 -\<close> ML \<open>
6.173 -\<close> ML \<open>
6.174 -\<close> ML \<open>
6.175 -\<close> ML \<open>
6.176 -case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
6.177 - SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
6.178 - | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
6.179 -
6.180 -\<close> ML \<open>
6.181 -case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
6.182 - SOME ("a * b kleiner c = True", _) => ()
6.183 - | _ => error "polyminus.sml: a * b kleiner b = True";
6.184 -
6.185 -\<close> ML \<open>
6.186 -case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of
6.187 - SOME ("3 * a * b kleiner c = True", _) => ()
6.188 - | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
6.189 -
6.190 -\<close> ML \<open>
6.191 -val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
6.192 -
6.193 -val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
6.194 - eval_kleiner "aaa" "bbb" t "ccc";
6.195 -"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const ("PolyMinus.kleiner",_) $ a $ b)), _) =
6.196 - ("aaa", "bbb", t, "ccc");
6.197 - (*if*) TermC.is_num b (*else*);
6.198 -
6.199 - (*if*) identifier a < identifier b (*else*);
6.200 -"~~~~~ fun identifier , args:"; val (t) = (a);
6.201 -
6.202 -(*+*)case a of
6.203 - Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $
6.204 - (Const ("Num.num.Bit0", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)))) => ()
6.205 -| _ => error "eval_kleiner CHANGED";
6.206 -
6.207 -
6.208 -\<close> ML \<open>
6.209 -"----------- fun ist_monom ---------------------------------------------------------------------";
6.210 -"----------- fun ist_monom ---------------------------------------------------------------------";
6.211 -"----------- fun ist_monom ---------------------------------------------------------------------";
6.212 -val t = @{term 0};
6.213 - if ist_monom t then () else error "ist_monom 1";
6.214 -
6.215 -val t = @{term "a"};
6.216 -if ist_monom t then () else error "ist_monom 2";
6.217 -
6.218 -val t = @{term "2 * a"};
6.219 -if ist_monom t then () else error "ist_monom 3";
6.220 -
6.221 -val t = @{term "2 * a * b"};
6.222 -if ist_monom t then () else error "ist_monom 4";
6.223 -
6.224 -val t = @{term "a * b"};
6.225 -if ist_monom t then () else error "ist_monom 5";
6.226 -
6.227 -val t = @{term "2 * a \<up> 2 * b"};
6.228 -if ist_monom t then () else error "ist_monom 6";
6.229 -
6.230 -val t = @{term "a \<up> 2 * b \<up> 3"};
6.231 -if ist_monom t then () else error "ist_monom 7";
6.232 -
6.233 -(* but also ..*)
6.234 -val t = @{term "a \<up> 2 * 4 * b \<up> 3 * 5"};
6.235 -if ist_monom t then () else error "ist_monom 8";
6.236 -\<close> ML \<open>
6.237 -\<close> ML \<open>
6.238 -\<close> ML \<open>
6.239 -\<close> ML \<open>
6.240 -\<close> ML \<open>
6.241 -\<close> ML \<open>
6.242 -"----------- fun eval_ist_monom ----------------------------------";
6.243 -"----------- fun eval_ist_monom ----------------------------------";
6.244 -"----------- fun eval_ist_monom ----------------------------------";
6.245 -\<close> ML \<open>
6.246 -case eval_ist_monom 0 0 (TermC.str2term "12 ist_monom") 0 of
6.247 - SOME ("12 ist_monom = True", _) => ()
6.248 - | _ => error "polyminus.sml: 12 ist_monom = True";
6.249 -
6.250 -case eval_ist_monom 0 0 (TermC.str2term "a ist_monom") 0 of
6.251 - SOME ("a ist_monom = True", _) => ()
6.252 - | _ => error "polyminus.sml: a ist_monom = True";
6.253 -
6.254 -case eval_ist_monom 0 0 (TermC.str2term "(3*a) ist_monom") 0 of
6.255 - SOME ("3 * a ist_monom = True", _) => ()
6.256 - | _ => error "polyminus.sml: 3 * a ist_monom = True";
6.257 -
6.258 -case eval_ist_monom 0 0 (TermC.str2term "(a \<up> 2) ist_monom") 0 of
6.259 - SOME ("a \<up> 2 ist_monom = True", _) => ()
6.260 - | _ => error "polyminus.sml: a \<up> 2 ist_monom = True";
6.261 -
6.262 -case eval_ist_monom 0 0 (TermC.str2term "(3*a \<up> 2) ist_monom") 0 of
6.263 - SOME ("3 * a \<up> 2 ist_monom = True", _) => ()
6.264 - | _ => error "polyminus.sml: 3*a \<up> 2 ist_monom = True";
6.265 -
6.266 -case eval_ist_monom 0 0 (TermC.str2term "(a*b) ist_monom") 0 of
6.267 - SOME ("a * b ist_monom = True", _) => ()
6.268 - | _ => error "polyminus.sml: a*b ist_monom = True";
6.269 -
6.270 -case eval_ist_monom 0 0 (TermC.str2term "(3*a*b) ist_monom") 0 of
6.271 - SOME ("3 * a * b ist_monom = True", _) => ()
6.272 - | _ => error "polyminus.sml: 3*a*b ist_monom = True";
6.273 -
6.274 -
6.275 -\<close> ML \<open>
6.276 -"----------- watch order_add_mult -------------------------------";
6.277 -"----------- watch order_add_mult -------------------------------";
6.278 -"----------- watch order_add_mult -------------------------------";
6.279 -"----- with these simple variables it works...";
6.280 -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
6.281 -Rewrite.trace_on:=false;
6.282 -val t = TermC.str2term "((a + d) + c) + b";
6.283 -val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
6.284 -if UnparseC.term t = "a + (b + (c + d))" then ()
6.285 -else error "polyminus.sml 1 watch order_add_mult";
6.286 -Rewrite.trace_on:=false;
6.287 -
6.288 -"----- the same stepwise...";
6.289 -val od = ord_make_polynomial true (@{theory "Poly"});
6.290 -val t = TermC.str2term "((a + d) + c) + b";
6.291 -"((a + d) + c) + b";
6.292 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
6.293 -"b + ((a + d) + c)";
6.294 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
6.295 -"b + (c + (a + d))";
6.296 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
6.297 -"b + (a + (c + d))";
6.298 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
6.299 -"a + (b + (c + d))";
6.300 -if UnparseC.term t = "a + (b + (c + d))" then ()
6.301 -else error "polyminus.sml 2 watch order_add_mult";
6.302 -
6.303 -"----- if parentheses are right, left_commute is (almost) sufficient...";
6.304 -val t = TermC.str2term "a + (d + (c + b))";
6.305 -"a + (d + (c + b))";
6.306 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
6.307 -"a + (c + (d + b))";
6.308 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t;UnparseC.term t;
6.309 -"a + (c + (b + d))";
6.310 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
6.311 -"a + (b + (c + d))";
6.312 -
6.313 -"----- but we do not want the parentheses at right; thus: cond.rew.";
6.314 -"WN0712707 complicated monomials do not yet work ...";
6.315 -val t = TermC.str2term "((5*a + 4*d) + 3*c) + 2*b";
6.316 -val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
6.317 -if UnparseC.term t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()
6.318 -else error "polyminus.sml: order_add_mult changed";
6.319 -
6.320 -"----- here we see rew_sub going into subterm with ord.rew....";
6.321 -val od = ord_make_polynomial false (@{theory "Poly"});
6.322 -val t = TermC.str2term "b + a + c + d";
6.323 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
6.324 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
6.325 -(*@@@ rew_sub gosub: t = d + (b + a + c)
6.326 - @@@ rew_sub begin: t = b + a + c*)
6.327 -
6.328 -
6.329 -\<close> ML \<open>
6.330 -"----------- build predicate for +- ordering ---------------------";
6.331 -"----------- build predicate for +- ordering ---------------------";
6.332 -"----------- build predicate for +- ordering ---------------------";
6.333 -\<close> ML \<open>
6.334 -"======= compare tausche_plus with real_num_collect";
6.335 -val od = dummy_ord;
6.336 -
6.337 -val erls = erls_ordne_alphabetisch;
6.338 -val t = TermC.str2term "b + a";
6.339 -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t;
6.340 -if UnparseC.term t = "a + b" then ()
6.341 -else error "polyminus.sml: ordne_alphabetisch1 b + a";
6.342 -
6.343 -val erls = Atools_erls;
6.344 -val t = TermC.str2term "2*a + 3*a";
6.345 -val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term t;
6.346 -
6.347 -"======= test rewrite_, rewrite_set_";
6.348 -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
6.349 -val erls = erls_ordne_alphabetisch;
6.350 -val t = TermC.str2term "b + a";
6.351 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
6.352 -if UnparseC.term t = "a + b" then ()
6.353 -else error "polyminus.sml: ordne_alphabetisch a + b";
6.354 -
6.355 -val t = TermC.str2term "2*b + a";
6.356 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
6.357 -if UnparseC.term t = "a + 2 * b" then ()
6.358 -else error "polyminus.sml: ordne_alphabetisch a + 2 * b";
6.359 -
6.360 -val t = TermC.str2term "a + c + b";
6.361 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
6.362 -if UnparseC.term t = "a + b + c" then ()
6.363 -else error "polyminus.sml: ordne_alphabetisch a + b + c";
6.364 -
6.365 -\<close> ML \<open>
6.366 -"======= rewrite goes into subterms";
6.367 -val t = TermC.str2term "a + c + b + d";
6.368 -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; UnparseC.term t;
6.369 -if UnparseC.term t = "a + b + c + d" then ()
6.370 -else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
6.371 -
6.372 -val t = TermC.str2term "a + c + d + b";
6.373 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
6.374 -if UnparseC.term t = "a + b + c + d" then ()
6.375 -else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
6.376 -
6.377 -"======= here we see rew_sub going into subterm with cond.rew....";
6.378 -val t = TermC.str2term "b + a + c + d";
6.379 -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t;
6.380 -if UnparseC.term t = "a + b + c + d" then ()
6.381 -else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
6.382 -
6.383 -"======= compile rls for the most complicated terms";
6.384 -val t = TermC.str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
6.385 -"5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
6.386 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t;
6.387 -if UnparseC.term t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
6.388 -then () else error "polyminus.sml: ordne_alphabetisch finished";
6.389 -
6.390 -
6.391 -\<close> ML \<open>
6.392 -"----------- build fasse_zusammen --------------------------------";
6.393 -"----------- build fasse_zusammen --------------------------------";
6.394 -"----------- build fasse_zusammen --------------------------------";
6.395 -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
6.396 -val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t;
6.397 -if UnparseC.term t = "3 + -2 * e + 2 * f + 2 * g" then ()
6.398 -else error "polyminus.sml: fasse_zusammen finished";
6.399 -
6.400 -\<close> ML \<open>
6.401 -"----------- build verschoenere ----------------------------------";
6.402 -"----------- build verschoenere ----------------------------------";
6.403 -"----------- build verschoenere ----------------------------------";
6.404 -val t = TermC.str2term "3 + -2 * e + 2 * f + 2 * g";
6.405 -val SOME (t,_) = rewrite_set_ thy false verschoenere t;
6.406 -if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
6.407 -else error "polyminus.sml: verschoenere 3 + -2 * e ...";
6.408 -
6.409 -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
6.410 -Rewrite.trace_on:=false;
6.411 -
6.412 -\<close> ML \<open>
6.413 -"----------- met simplification for_polynomials with_minus -------";
6.414 -"----------- met simplification for_polynomials with_minus -------";
6.415 -"----------- met simplification for_polynomials with_minus -------";
6.416 -val str =
6.417 -"Program SimplifyScript (t_t::real) = \
6.418 -\ (((Try (Rewrite_Set ordne_alphabetisch False)) #> \
6.419 -\ (Try (Rewrite_Set fasse_zusammen False)) #> \
6.420 -\ (Try (Rewrite_Set verschoenere False))) t_t)"
6.421 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
6.422 -TermC.atomty sc;
6.423 -
6.424 -\<close> ML \<open>
6.425 -"----------- me simplification.for_polynomials.with_minus";
6.426 -"----------- me simplification.for_polynomials.with_minus";
6.427 -"----------- me simplification.for_polynomials.with_minus";
6.428 -val c = [];
6.429 -val (p,_,f,nxt,_,pt) =
6.430 - CalcTreeTEST
6.431 - [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
6.432 - "normalform N"],
6.433 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
6.434 - ["simplification", "for_polynomials", "with_minus"]))];
6.435 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.436 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.437 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.438 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.439 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.440 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.441 -
6.442 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.443 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.444 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.445 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.446 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.447 -if f2str f = "3 - 2 * e + 2 * f + 2 * g"
6.448 -then case nxt of End_Proof' => () | _ => error "me simplification.for_polynomials.with_minus 1"
6.449 -else error "polyminus.sml: me simplification.for_polynomials.with_minus 2";
6.450 -
6.451 -\<close> ML \<open>
6.452 -"----------- pbl polynom vereinfachen p.33 -----------------------";
6.453 -"----------- pbl polynom vereinfachen p.33 -----------------------";
6.454 -"----------- pbl polynom vereinfachen p.33 -----------------------";
6.455 -"----------- 140 c ---";
6.456 -reset_states ();
6.457 -CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
6.458 - "normalform N"],
6.459 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
6.460 - ["simplification", "for_polynomials", "with_minus"]))];
6.461 -moveActiveRoot 1;
6.462 -autoCalculate 1 CompleteCalc;
6.463 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.464 -if p = ([], Res) andalso
6.465 - UnparseC.term (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
6.466 -then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
6.467 -
6.468 -\<close> ML \<open>
6.469 -"======= 140 d ---";
6.470 -reset_states ();
6.471 -CalcTree [(["Term (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",
6.472 - "normalform N"],
6.473 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
6.474 - ["simplification", "for_polynomials", "with_minus"]))];
6.475 -moveActiveRoot 1;
6.476 -autoCalculate 1 CompleteCalc;
6.477 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.478 -if p = ([], Res) andalso
6.479 - UnparseC.term (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
6.480 -then () else error "polyminus.sml: Vereinfache 140 d)";
6.481 -
6.482 -\<close> ML \<open>
6.483 -"======= 139 c ---";
6.484 -reset_states ();
6.485 -CalcTree [(["Term (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",
6.486 - "normalform N"],
6.487 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
6.488 - ["simplification", "for_polynomials", "with_minus"]))];
6.489 -moveActiveRoot 1;
6.490 -autoCalculate 1 CompleteCalc;
6.491 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.492 -if p = ([], Res) andalso
6.493 - UnparseC.term (get_obj g_res pt (fst p)) = "- (3 * f)"
6.494 -then () else error "polyminus.sml: Vereinfache 139 c)";
6.495 -
6.496 -\<close> ML \<open>
6.497 -"======= 139 b ---";
6.498 -reset_states ();
6.499 -CalcTree [(["Term (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",
6.500 - "normalform N"],
6.501 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
6.502 - ["simplification", "for_polynomials", "with_minus"]))];
6.503 -moveActiveRoot 1;
6.504 -autoCalculate 1 CompleteCalc;
6.505 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.506 -if p = ([], Res) andalso
6.507 - UnparseC.term (get_obj g_res pt (fst p)) = "-3 * u - v"
6.508 -then () else error "polyminus.sml: Vereinfache 139 b)";
6.509 -
6.510 -\<close> ML \<open>
6.511 -"======= 138 a ---";
6.512 -reset_states ();
6.513 -CalcTree [(["Term (2*u - 3*v - 6*u + 5*v)",
6.514 - "normalform N"],
6.515 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
6.516 - ["simplification", "for_polynomials", "with_minus"]))];
6.517 -moveActiveRoot 1;
6.518 -autoCalculate 1 CompleteCalc;
6.519 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.520 -if p = ([], Res) andalso
6.521 - UnparseC.term (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"
6.522 -then () else error "polyminus.sml: Vereinfache 138 a)";
6.523 -
6.524 -\<close> ML \<open>
6.525 -"----------- met probe fuer_polynom ------------------------------";
6.526 -"----------- met probe fuer_polynom ------------------------------";
6.527 -"----------- met probe fuer_polynom ------------------------------";
6.528 -val str =
6.529 -"Program ProbeScript (e_e::bool) (w_s::bool list) =\
6.530 -\ (let e_e = Take e_e; \
6.531 -\ e_e = Substitute w_s e_e \
6.532 -\ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #> \
6.533 -\ (Try (Repeat (Calculate ''PLUS''))) #> \
6.534 -\ (Try (Repeat (Calculate ''MINUS''))))) e_e)"
6.535 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
6.536 -TermC.atomty sc;
6.537 -
6.538 -\<close> ML \<open>
6.539 -"----------- pbl polynom probe -----------------------------------";
6.540 -"----------- pbl polynom probe -----------------------------------";
6.541 -"----------- pbl polynom probe -----------------------------------";
6.542 -reset_states ();
6.543 -CalcTree [(["Pruefe ((5::int)*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\
6.544 - \3 - 2 * e + 2 * f + 2 * (g::int))",
6.545 - "mitWert [e = (1::int), f = (2::int), g = (3::int)]",
6.546 - "Geprueft b"],
6.547 - ("PolyMinus",["polynom", "probe"],
6.548 - ["probe", "fuer_polynom"]))];
6.549 -moveActiveRoot 1;
6.550 -autoCalculate 1 CompleteCalc;
6.551 -(* autoCalculate 1 CompleteCalcHead;
6.552 - autoCalculate 1 (Steps 1);
6.553 - autoCalculate 1 (Steps 1);
6.554 - val ((pt,p),_) = get_calc 1; UnparseC.term (get_obj g_res pt (fst p));
6.555 -@@@@@WN081114 gives "??.empty", all "Pruefe" are the same,
6.556 -although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)
6.557 -val ((pt,p),_) = get_calc 1;
6.558 -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "11 = 11"
6.559 -then () else error "polyminus.sml: Probe 11 = 11";
6.560 -Test_Tool.show_pt pt;
6.561 -
6.562 -\<close> ML \<open>
6.563 -"----------- pbl klammer polynom vereinfachen p.34 ---------------";
6.564 -"----------- pbl klammer polynom vereinfachen p.34 ---------------";
6.565 -"----------- pbl klammer polynom vereinfachen p.34 ---------------";
6.566 -reset_states ();
6.567 -CalcTree [(["Term (2*u - 5 - (3 - 4*u) + (8*u + 9))",
6.568 - "normalform N"],
6.569 - ("PolyMinus",["klammer", "polynom", "vereinfachen"],
6.570 - ["simplification", "for_polynomials", "with_parentheses"]))];
6.571 -moveActiveRoot 1;
6.572 -autoCalculate 1 CompleteCalc;
6.573 -val ((pt,p),_) = get_calc 1;
6.574 -if p = ([], Res) andalso
6.575 - UnparseC.term (get_obj g_res pt (fst p)) = "1 + 14 * u"
6.576 -then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
6.577 -Test_Tool.show_pt pt;
6.578 -
6.579 -\<close> ML \<open>
6.580 -"======= probe p.34 -----";
6.581 -reset_states ();
6.582 -CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * (u::int))",
6.583 - "mitWert [u = (2::int)]",
6.584 - "Geprueft b"],
6.585 - ("PolyMinus",["polynom", "probe"],
6.586 - ["probe", "fuer_polynom"]))];
6.587 -moveActiveRoot 1;
6.588 -autoCalculate 1 CompleteCalc;
6.589 -val ((pt,p),_) = get_calc 1;
6.590 -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "29 = 29"
6.591 -then () else error "polyminus.sml: Probe 29 = 29";
6.592 -Test_Tool.show_pt pt;
6.593 -
6.594 -\<close> ML \<open>
6.595 -"----------- try fun applyTactics --------------------------------";
6.596 -"----------- try fun applyTactics --------------------------------";
6.597 -"----------- try fun applyTactics --------------------------------";
6.598 -reset_states ();
6.599 -CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
6.600 - "normalform N"],
6.601 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
6.602 - ["simplification", "for_polynomials", "with_minus"]))];
6.603 -moveActiveRoot 1;
6.604 -autoCalculate 1 CompleteCalcHead;
6.605 -autoCalculate 1 (Steps 1);
6.606 -autoCalculate 1 (Steps 1);
6.607 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.608 -"----- 1 \<up> ";
6.609 -fetchApplicableTactics 1 0 p;
6.610 -val appltacs = specific_from_prog pt p;
6.611 -applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
6.612 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.613 -"----- 2 \<up> ";
6.614 -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
6.615 -val erls = erls_ordne_alphabetisch;
6.616 -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
6.617 -\<close> ML \<open>
6.618 -\<close> ML \<open>
6.619 -val SOME (t',_) =
6.620 - rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus} t;
6.621 -UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
6.622 -
6.623 -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
6.624 -val NONE =
6.625 - rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus_plus} t;
6.626 -
6.627 -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
6.628 -val SOME (t',_) =
6.629 - rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
6.630 -UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
6.631 -Rewrite.trace_on := false;
6.632 -
6.633 -
6.634 -applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
6.635 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.636 -"----- 3 \<up> ";
6.637 -applyTactic 1 p (hd (specific_from_prog pt p)) (**);
6.638 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.639 -"----- 4 \<up> ";
6.640 -applyTactic 1 p (hd (specific_from_prog pt p)) (**);
6.641 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.642 -"----- 5 \<up> ";
6.643 -applyTactic 1 p (hd (specific_from_prog pt p)) (**);
6.644 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.645 -"----- 6 \<up> ";
6.646 -
6.647 -(*<CALCMESSAGE> failure </CALCMESSAGE>
6.648 -applyTactic 1 p (hd (specific_from_prog pt p)) (**);
6.649 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.650 -"----- 7 \<up> ";
6.651 -*)
6.652 -autoCalculate 1 CompleteCalc;
6.653 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.654 -(*independent from failure above: met_simp_poly_minus not confluent:
6.655 -(([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)),
6.656 -(([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))]
6.657 -~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
6.658 -
6.659 -
6.660 -\<close> ML \<open>
6.661 -"#############################################################################";
6.662 -reset_states ();
6.663 -CalcTree [(["Term (- (8 * g) + 10 * g + h)",
6.664 - "normalform N"],
6.665 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
6.666 - ["simplification", "for_polynomials", "with_minus"]))];
6.667 -moveActiveRoot 1;
6.668 -autoCalculate 1 CompleteCalc;
6.669 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.670 -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "2 * g + h"
6.671 -then () else error "polyminus.sml: addiere_vor_minus";
6.672 -
6.673 -
6.674 -\<close> ML \<open>
6.675 -"#############################################################################";
6.676 -reset_states ();
6.677 -CalcTree [(["Term (- (8 * g) + 10 * g + f)",
6.678 - "normalform N"],
6.679 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
6.680 - ["simplification", "for_polynomials", "with_minus"]))];
6.681 -moveActiveRoot 1;
6.682 -autoCalculate 1 CompleteCalc;
6.683 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.684 -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "f + 2 * g"
6.685 -then () else error "polyminus.sml: tausche_vor_plus";
6.686 -
6.687 -\<close> ML \<open>
6.688 -"----------- pbl binom polynom vereinfachen p.39 -----------------";
6.689 -"----------- pbl binom polynom vereinfachen p.39 -----------------";
6.690 -"----------- pbl binom polynom vereinfachen p.39 -----------------";
6.691 -val rls = klammern_ausmultiplizieren;
6.692 -val t = TermC.str2term "(3 * a + 2) * (4 * a - 1)";
6.693 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
6.694 -"3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)";
6.695 -val rls = discard_parentheses;
6.696 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
6.697 -"3 * a * 4 * a - 3 * a * 1 + (2 * 4 * a - 2 * 1)";
6.698 -val rls = ordne_monome;
6.699 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
6.700 -"3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)";
6.701 -(*
6.702 -val t = TermC.str2term "3 * a * 4 * a";
6.703 -val rls = ordne_monome;
6.704 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
6.705 -*)
6.706 -val rls = klammern_aufloesen;
6.707 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
6.708 -"3 * 4 * a * a - 1 * 3 * a + 2 * 4 * a - 1 * 2";
6.709 -val rls = ordne_alphabetisch;
6.710 -(*TODO: make is_monom more general, a*a=a^2, ...*)
6.711 -\<close> ML \<open>
6.712 -\<close> ML \<open>
6.713 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
6.714 -"3 * 4 * a * a - 1 * 2 - 1 * 3 * a + 2 * 4 * a";
6.715 -(*STOPPED.WN080104
6.716 -val rls = fasse_zusammen;
6.717 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
6.718 -val rls = verschoenere;
6.719 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
6.720 -*)
6.721 -
6.722 -\<close> ML \<open>
6.723 -(*@@@@@@@*)
6.724 -reset_states ();
6.725 -CalcTree [(["Term ((3*a + 2) * (4*a - 1))",
6.726 - "normalform N"],
6.727 - ("PolyMinus",["binom_klammer", "polynom", "vereinfachen"],
6.728 - ["simplification", "for_polynomials", "with_parentheses_mult"]))];
6.729 -moveActiveRoot 1;
6.730 -autoCalculate 1 CompleteCalc;
6.731 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.732 -\<close> ML \<open>
6.733 -UnparseC.term (get_obj g_res pt (fst p)) = "12 * a \<up> 2 - 2 + 5 * a" (*monoms-order NOTok*)
6.734 -\<close> ML \<open>
6.735 -if p = ([], Res) andalso
6.736 - UnparseC.term (get_obj g_res pt (fst p)) = "-2 + 12 * a \<up> 2 + 5 * a"
6.737 -then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
6.738 -
6.739 -\<close> ML \<open>
6.740 -"----------- pbl binom polynom vereinfachen: cube ----------------";
6.741 -"----------- pbl binom polynom vereinfachen: cube ----------------";
6.742 -"----------- pbl binom polynom vereinfachen: cube ----------------";
6.743 -reset_states ();
6.744 -CalcTree [(["Term (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"],
6.745 - ("PolyMinus",["binom_klammer", "polynom", "vereinfachen"],
6.746 - ["simplification", "for_polynomials", "with_parentheses_mult"]))];
6.747 -moveActiveRoot 1;
6.748 -autoCalculate 1 CompleteCalc;
6.749 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.750 -\<close> ML \<open>
6.751 -UnparseC.term (get_obj g_res pt (fst p)) = "9 * a - 10 * q + 3 * a - 6 * q"
6.752 -\<close> ML \<open>
6.753 -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "12 * a - 16 * q"
6.754 -then () else error "pbl binom polynom vereinfachen: cube";
6.755 -
6.756 -\<close> ML \<open>
6.757 -"----------- Refine.refine Vereinfache ----------------------------------";
6.758 -"----------- Refine.refine Vereinfache ----------------------------------";
6.759 -"----------- Refine.refine Vereinfache ----------------------------------";
6.760 -val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"];
6.761 -(*default_print_depth 11;*)
6.762 -val matches = Refine.refine fmz ["vereinfachen"];
6.763 -(*default_print_depth 3;*)
6.764 -
6.765 -"----- go into details, if it seems not to work -----";
6.766 -"--- does the predicate evaluate correctly ?";
6.767 -val t = TermC.str2term
6.768 - "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))";
6.769 -val ma = eval_matchsub "" "Prog_Expr.matchsub" t thy;
6.770 -case ma of
6.771 - SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \
6.772 - \a - 2 * q + 3 * (a - 2 * q)) = True", _) => ()
6.773 - | _ => error "polyminus.sml matchsub (?a * (?b - ?c)...A";
6.774 -
6.775 -"--- does the respective prls rewrite ?";
6.776 -val prls = Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty
6.777 - [Eval ("Poly.is_polyexp", eval_is_polyexp ""),
6.778 - Eval ("Prog_Expr.matchsub", eval_matchsub ""),
6.779 - Thm ("or_true",@{thm or_true}),
6.780 - (*"(?a | True) = True"*)
6.781 - Thm ("or_false",@{thm or_false}),
6.782 - (*"(?a | False) = ?a"*)
6.783 - Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
6.784 - (*"(~ True) = False"*)
6.785 - Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
6.786 - (*"(~ False) = True"*)];
6.787 -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
6.788 -val SOME (t', _) = rewrite_set_ thy false prls t;
6.789 -Rewrite.trace_on := false;
6.790 -
6.791 -"--- does the respective prls rewrite the whole predicate ?";
6.792 -val t = TermC.str2term
6.793 - "Not (matchsub (?a * (?b + ?c)) (8 * (a - q) + a - 2 * q) | \
6.794 - \ matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
6.795 - \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
6.796 - \ matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
6.797 -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
6.798 -val SOME (t', _) = rewrite_set_ thy false prls t;
6.799 -Rewrite.trace_on := false;
6.800 -if UnparseC.term t' = "False" then ()
6.801 -else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
6.802 -
6.803 -\<close> ML \<open>
6.804 -"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
6.805 -"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
6.806 -"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
6.807 -(*see test/../termC.sml for details*)
6.808 -val t = TermC.parse_patt thy "t_t is_polyexp";
6.809 -val t = TermC.parse_patt thy ("Not (matchsub (?a + (?b + ?c)) t_t | " ^
6.810 - " matchsub (?a + (?b - ?c)) t_t | " ^
6.811 - " matchsub (?a - (?b + ?c)) t_t | " ^
6.812 - " matchsub (?a + (?b - ?c)) t_t )");
6.813 -(*show_types := true;
6.814 -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)"
6.815 -then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
6.816 -show_types := false;*)
6.817 -if UnparseC.term t =
6.818 - "\<not> (matchsub (?a + (?b + ?c)) t_t \<or>\n " ^
6.819 - "matchsub (?a + (?b - ?c)) t_t \<or>\n " ^
6.820 - "matchsub (?a - (?b + ?c)) t_t \<or> " ^
6.821 - "matchsub (?a + (?b - ?c)) t_t)"
6.822 -then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
6.823 -
6.824 \<close> ML \<open>
6.825 \<close> ML \<open>
6.826 \<close>