1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Thu Jul 15 14:10:18 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu Jul 15 20:02:16 2021 +0200
1.3 @@ -7,7 +7,7 @@
1.4 "--------------------------------------------------------";
1.5 "table of contents --------------------------------------";
1.6 "--------------------------------------------------------";
1.7 -"----------- fun contains_mult_pot_only --------------------------------------------------------";
1.8 +"----------- fun identifier --------------------------------------------------------------------";
1.9 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
1.10 "----------- fun ist_monom ---------------------------------------------------------------------";
1.11 "----------- fun eval_ist_monom -------------------------";
1.12 @@ -32,40 +32,57 @@
1.13
1.14 val thy = @{theory "PolyMinus"};
1.15
1.16 -"----------- fun contains_mult_pot_only --------------------------------------------------------";
1.17 -"----------- fun contains_mult_pot_only --------------------------------------------------------";
1.18 -"----------- fun contains_mult_pot_only --------------------------------------------------------";
1.19 -val t = @{term 0};
1.20 - if contains_mult_pot_only t then () else error "contains_mult_pot_only 1";
1.21 +"----------- fun identifier --------------------------------------------------------------------";
1.22 +"----------- fun identifier --------------------------------------------------------------------";
1.23 +"----------- fun identifier --------------------------------------------------------------------";
1.24 +if identifier (TermC.str2term "12 ::real") = "12" then () else error "identifier 1";
1.25 +if identifier (TermC.str2term "a ::real") = "a" then () else error "identifier 2";
1.26 +if identifier (TermC.str2term "3 * a ::real") = "a" then () else error "identifier 3";
1.27 +if identifier (TermC.str2term "a \<up> 2 ::real") = "a" then () else error "identifier 4";
1.28 +if identifier (TermC.str2term "3*a \<up> 2 ::real") = "a" then () else error "identifier 5";
1.29 +if identifier (TermC.str2term "a * b ::real") = "b" then () else error "identifier 5b";
1.30
1.31 -val t = @{term "a"};
1.32 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 2";
1.33 -
1.34 -val t = @{term "2 * a"};
1.35 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 3";
1.36 -
1.37 -val t = @{term "2 * a * b"};
1.38 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 4";
1.39 -
1.40 -val t = @{term "a * b"};
1.41 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 5";
1.42 -
1.43 -val t = @{term "2 * a \<up> 2 * b"};
1.44 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 6";
1.45 -
1.46 -val t = @{term "a \<up> 2 * b \<up> 3"};
1.47 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 7";
1.48 -
1.49 -(* but also ..*)
1.50 -val t = @{term "a \<up> 2 * 4 * b \<up> 3 * 5"};
1.51 -if contains_mult_pot_only t then () else error "contains_mult_pot_only 8";
1.52 +(*these are strange (see "specific monomials" in comment to fun.def.)..*)
1.53 +if identifier (TermC.str2term "a*b ::real") = "b" then () else error "identifier 6";
1.54 +if identifier (TermC.str2term "(3*a*b) ::real") = "b" then () else error "identifier 7";
1.55
1.56
1.57 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
1.58 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
1.59 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
1.60 +"a" < "b";
1.61 +"ba" < "ab";
1.62 +"123" < "a"; (*unused due to ---vvv*)
1.63 +"12" < "3"; (*true !!!*)
1.64 +
1.65 +" a kleiner b ==> (b + a) = (a + b)";
1.66 +TermC.str2term "aaa";
1.67 +TermC.str2term "222 * aaa";
1.68 +
1.69 +case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
1.70 + SOME ("123 kleiner 32 = False", _) => ()
1.71 + | _ => error "polyminus.sml: 12 kleiner 9 = False";
1.72 +case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of
1.73 + SOME ("a kleiner b = True", _) => ()
1.74 + | _ => error "polyminus.sml: a kleiner b = True";
1.75 +case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of
1.76 + SOME ("10 * g kleiner f = False", _) => ()
1.77 + | _ => error "polyminus.sml: 10 * g kleiner f = False";
1.78 +case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
1.79 + SOME ("a \<up> 2 kleiner b = True", _) => ()
1.80 + | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
1.81 +case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
1.82 + SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
1.83 + | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
1.84 +case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
1.85 + SOME ("a * b kleiner c = True", _) => ()
1.86 + | _ => error "polyminus.sml: a * b kleiner b = True";
1.87 +case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of
1.88 + SOME ("3 * a * b kleiner c = True", _) => ()
1.89 + | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
1.90 +
1.91 +
1.92 val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
1.93 -
1.94 val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
1.95 eval_kleiner "aaa" "bbb" t "ccc";
1.96 "~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const ("PolyMinus.kleiner",_) $ a $ b)), _) =
1.97 @@ -74,17 +91,45 @@
1.98
1.99 (*if*) identifier a < identifier b (*else*);
1.100 "~~~~~ fun identifier , args:"; val (t) = (a);
1.101 -
1.102 (*+*)case a of
1.103 Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $
1.104 (Const ("Num.num.Bit0", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)))) => ()
1.105 -| _ => error "eval_kleiner CHANGED";
1.106 +| _ => error "eval_kleiner CHANGED"; (*isa*)
1.107 +
1.108 +
1.109 +"----------- fun ist_monom ---------------------------------------------------------------------";
1.110 +"----------- fun ist_monom ---------------------------------------------------------------------";
1.111 +"----------- fun ist_monom ---------------------------------------------------------------------";
1.112 +val t = TermC.str2term "0 ::real";
1.113 + if ist_monom t then () else error "ist_monom 1";
1.114 +
1.115 +val t = TermC.str2term "a";
1.116 +if ist_monom t then () else error "ist_monom 2";
1.117 +
1.118 +val t = TermC.str2term "2 * a";
1.119 +if ist_monom t then () else error "ist_monom 3";
1.120 +
1.121 +val t = TermC.str2term "2 * a * b";
1.122 +if ist_monom t then () else error "ist_monom 4";
1.123 +
1.124 +val t = TermC.str2term "a * b";
1.125 +if ist_monom t then () else error "ist_monom 5";
1.126 +
1.127 +(*not covered before NEW numerals*)
1.128 +val t = TermC.str2term "2 * a \<up> 2 * b";
1.129 +if ist_monom t then () else error "ist_monom 6";
1.130 +
1.131 +(*not covered before NEW numerals*)
1.132 +val t = TermC.str2term "a \<up> 2 * b \<up> 3";
1.133 +if ist_monom t then () else error "ist_monom 7";
1.134 +
1.135 +val t = TermC.str2term "a \<up> 2 * 4 * b \<up> 3 * 5";
1.136 +if ist_monom t then () else error "ist_monom 8";
1.137
1.138
1.139 "----------- fun eval_ist_monom ----------------------------------";
1.140 "----------- fun eval_ist_monom ----------------------------------";
1.141 "----------- fun eval_ist_monom ----------------------------------";
1.142 -ist_monom (TermC.str2term "12");
1.143 case eval_ist_monom 0 0 (TermC.str2term "12 ist_monom") 0 of
1.144 SOME ("12 ist_monom = True", _) => ()
1.145 | _ => error "polyminus.sml: 12 ist_monom = True";
1.146 @@ -239,7 +284,7 @@
1.147 else error "polyminus.sml: ordne_alphabetisch a + b + c";
1.148
1.149 "======= rewrite goes into subterms";
1.150 -val t = TermC.str2term "a + c + b + d";
1.151 +val t = TermC.str2term "a + c + b + d ::real";
1.152 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; UnparseC.term t;
1.153 if UnparseC.term t = "a + b + c + d" then ()
1.154 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
1.155 @@ -268,7 +313,7 @@
1.156 "----------- build fasse_zusammen --------------------------------";
1.157 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
1.158 val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t;
1.159 -if UnparseC.term t = "3 + -2 * e + 2 * f + 2 * g" then ()
1.160 +if UnparseC.term t = "3 + - 2 * e + 2 * f + 2 * g" then ()
1.161 else error "polyminus.sml: fasse_zusammen finished";
1.162
1.163 "----------- build verschoenere ----------------------------------";
1.164 @@ -311,11 +356,17 @@
1.165 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.166
1.167 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.168 + f2str f = "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12"; (*isa == isa2*)
1.169 +val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt;
1.170 + val (*^^^*) Rewrite_Set "ordne_alphabetisch" = nxt;
1.171 + f2str f = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"; (*isa2*)
1.172 +val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
1.173 + f2str f = "3 + - 2 * e + 2 * f + 2 * g"; (*isa2*)
1.174 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.175 + f2str f = "3 - 2 * e + 2 * f + 2 * g"; (*isa2*)
1.176 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.177 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.178 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.179 -if f2str f = "3 - 2 * e + 2 * f + 2 * g"
1.180 + f2str f = "3 - 2 * e + 2 * f + 2 * g"; (*isa2*)
1.181 +if f2str f = "3 - 2 * e + 2 * f + 2 * g" (*isa2*)
1.182 then case nxt of End_Proof' => () | _ => error "me simplification.for_polynomials.with_minus 1"
1.183 else error "polyminus.sml: me simplification.for_polynomials.with_minus 2";
1.184
1.185 @@ -371,7 +422,7 @@
1.186 autoCalculate 1 CompleteCalc;
1.187 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.188 if p = ([], Res) andalso
1.189 - UnparseC.term (get_obj g_res pt (fst p)) = "-3 * u - v"
1.190 + UnparseC.term (get_obj g_res pt (fst p)) = "- 3 * u - v"
1.191 then () else error "polyminus.sml: Vereinfache 139 b)";
1.192
1.193 "======= 138 a ---";
1.194 @@ -384,7 +435,7 @@
1.195 autoCalculate 1 CompleteCalc;
1.196 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.197 if p = ([], Res) andalso
1.198 - UnparseC.term (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"
1.199 + UnparseC.term (get_obj g_res pt (fst p)) = "- 4 * u + 2 * v"
1.200 then () else error "polyminus.sml: Vereinfache 138 a)";
1.201
1.202 "----------- met probe fuer_polynom ------------------------------";
1.203 @@ -582,8 +633,10 @@
1.204 moveActiveRoot 1;
1.205 autoCalculate 1 CompleteCalc;
1.206 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.207 -if p = ([], Res) andalso
1.208 - UnparseC.term (get_obj g_res pt (fst p)) = "-2 + 12 * a \<up> 2 + 5 * a"
1.209 +
1.210 +if p = ([], Res) andalso
1.211 + UnparseC.term (get_obj g_res pt (fst p)) =(*"- 2 + 12 * a \<up> 2 + 5 * a" with OLD numerals*)
1.212 + "- 2 + 5 * a + 12 * a \<up> 2"
1.213 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
1.214
1.215 "----------- pbl binom polynom vereinfachen: cube ----------------";