1.1 --- a/src/Tools/isac/IsacKnowledge/PolyMinus.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,521 +0,0 @@
1.4 -(* questionable attempts to perserve binary minus as wanted by teachers
1.5 - WN071207
1.6 - (c) due to copyright terms
1.7 -remove_thy"PolyMinus";
1.8 -use_thy"IsacKnowledge/PolyMinus";
1.9 -
1.10 -use_thy"IsacKnowledge/Isac";
1.11 -use"IsacKnowledge/PolyMinus.ML";
1.12 -*)
1.13 -
1.14 -(** interface isabelle -- isac **)
1.15 -theory' := overwritel (!theory', [("PolyMinus.thy",PolyMinus.thy)]);
1.16 -
1.17 -(** eval functions **)
1.18 -
1.19 -(*. get the identifier from specific monomials; see fun ist_monom .*)
1.20 -(*HACK.WN080107*)
1.21 -fun increase str =
1.22 - let val s::ss = explode str
1.23 - in implode ((chr (ord s + 1))::ss) end;
1.24 -fun identifier (Free (id,_)) = id (* 2, a *)
1.25 - | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
1.26 - id (* 2*a, a*b *)
1.27 - | identifier (Const ("op *", _) $ (* 3*a*b *)
1.28 - (Const ("op *", _) $
1.29 - Free (num, _) $ Free _) $ Free (id, _)) =
1.30 - if is_numeral num then id
1.31 - else "|||||||||||||"
1.32 - | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
1.33 - if is_numeral base then "|||||||||||||" (* a^2 *)
1.34 - else (*increase*) base
1.35 - | identifier (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
1.36 - (Const ("Atools.pow", _) $
1.37 - Free (base, _) $ Free (exp, _))) =
1.38 - if is_numeral num andalso not (is_numeral base) then (*increase*) base
1.39 - else "|||||||||||||"
1.40 - | identifier _ = "|||||||||||||"(*the "largest" string*);
1.41 -
1.42 -(*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
1.43 -(* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
1.44 -fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
1.45 - if is_num b then
1.46 - if is_num a then (*123 kleiner 32 = True !!!*)
1.47 - if int_of_Free a < int_of_Free b then
1.48 - SOME ((term2str p) ^ " = True",
1.49 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.50 - else SOME ((term2str p) ^ " = False",
1.51 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.52 - else (* -1 * -2 kleiner 0 *)
1.53 - SOME ((term2str p) ^ " = False",
1.54 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.55 - else
1.56 - if identifier a < identifier b then
1.57 - SOME ((term2str p) ^ " = True",
1.58 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.59 - else SOME ((term2str p) ^ " = False",
1.60 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.61 - | eval_kleiner _ _ _ _ = NONE;
1.62 -
1.63 -fun ist_monom (Free (id,_)) = true
1.64 - | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
1.65 - if is_numeral num then true else false
1.66 - | ist_monom _ = false;
1.67 -(*. this function only accepts the most simple monoms vvvvvvvvvv .*)
1.68 -fun ist_monom (Free (id,_)) = true (* 2, a *)
1.69 - | ist_monom (Const ("op *", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
1.70 - if is_numeral id then false else true
1.71 - | ist_monom (Const ("op *", _) $ (* 3*a*b *)
1.72 - (Const ("op *", _) $
1.73 - Free (num, _) $ Free _) $ Free (id, _)) =
1.74 - if is_numeral num andalso not (is_numeral id) then true else false
1.75 - | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
1.76 - true (* a^2 *)
1.77 - | ist_monom (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
1.78 - (Const ("Atools.pow", _) $
1.79 - Free (base, _) $ Free (exp, _))) =
1.80 - if is_numeral num then true else false
1.81 - | ist_monom _ = false;
1.82 -
1.83 -(* is this a univariate monomial ? *)
1.84 -(*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*)
1.85 -fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _ =
1.86 - if ist_monom a then
1.87 - SOME ((term2str p) ^ " = True",
1.88 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.89 - else SOME ((term2str p) ^ " = False",
1.90 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.91 - | eval_ist_monom _ _ _ _ = NONE;
1.92 -
1.93 -
1.94 -(** rewrite order **)
1.95 -
1.96 -(** rulesets **)
1.97 -
1.98 -val erls_ordne_alphabetisch =
1.99 - append_rls "erls_ordne_alphabetisch" e_rls
1.100 - [Calc ("PolyMinus.kleiner", eval_kleiner ""),
1.101 - Calc ("PolyMinus.ist'_monom", eval_ist_monom "")
1.102 - ];
1.103 -
1.104 -val ordne_alphabetisch =
1.105 - Rls{id = "ordne_alphabetisch", preconds = [],
1.106 - rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
1.107 - erls = erls_ordne_alphabetisch,
1.108 - rules = [Thm ("tausche_plus",num_str tausche_plus),
1.109 - (*"b kleiner a ==> (b + a) = (a + b)"*)
1.110 - Thm ("tausche_minus",num_str tausche_minus),
1.111 - (*"b kleiner a ==> (b - a) = (-a + b)"*)
1.112 - Thm ("tausche_vor_plus",num_str tausche_vor_plus),
1.113 - (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
1.114 - Thm ("tausche_vor_minus",num_str tausche_vor_minus),
1.115 - (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
1.116 - Thm ("tausche_plus_plus",num_str tausche_plus_plus),
1.117 - (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
1.118 - Thm ("tausche_plus_minus",num_str tausche_plus_minus),
1.119 - (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
1.120 - Thm ("tausche_minus_plus",num_str tausche_minus_plus),
1.121 - (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
1.122 - Thm ("tausche_minus_minus",num_str tausche_minus_minus)
1.123 - (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
1.124 - ], scr = EmptyScr}:rls;
1.125 -
1.126 -val fasse_zusammen =
1.127 - Rls{id = "fasse_zusammen", preconds = [],
1.128 - rew_ord = ("dummy_ord", dummy_ord),
1.129 - erls = append_rls "erls_fasse_zusammen" e_rls
1.130 - [Calc ("Atools.is'_const",eval_const "#is_const_")],
1.131 - srls = Erls, calc = [],
1.132 - rules =
1.133 - [Thm ("real_num_collect",num_str real_num_collect),
1.134 - (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.135 - Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r),
1.136 - (*"[| l is_const; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
1.137 - Thm ("real_one_collect",num_str real_one_collect),
1.138 - (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.139 - Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
1.140 - (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
1.141 -
1.142 -
1.143 - Thm ("subtrahiere",num_str subtrahiere),
1.144 - (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
1.145 - Thm ("subtrahiere_von_1",num_str subtrahiere_von_1),
1.146 - (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
1.147 - Thm ("subtrahiere_1",num_str subtrahiere_1),
1.148 - (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
1.149 -
1.150 - Thm ("subtrahiere_x_plus_minus",num_str subtrahiere_x_plus_minus),
1.151 - (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
1.152 - Thm ("subtrahiere_x_plus1_minus",num_str subtrahiere_x_plus1_minus),
1.153 - (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
1.154 - Thm ("subtrahiere_x_plus_minus1",num_str subtrahiere_x_plus_minus1),
1.155 - (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
1.156 -
1.157 - Thm ("subtrahiere_x_minus_plus",num_str subtrahiere_x_minus_plus),
1.158 - (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
1.159 - Thm ("subtrahiere_x_minus1_plus",num_str subtrahiere_x_minus1_plus),
1.160 - (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
1.161 - Thm ("subtrahiere_x_minus_plus1",num_str subtrahiere_x_minus_plus1),
1.162 - (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
1.163 -
1.164 - Thm ("subtrahiere_x_minus_minus",num_str subtrahiere_x_minus_minus),
1.165 - (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
1.166 - Thm ("subtrahiere_x_minus1_minus",num_str subtrahiere_x_minus1_minus),
1.167 - (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
1.168 - Thm ("subtrahiere_x_minus_minus1",num_str subtrahiere_x_minus_minus1),
1.169 - (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
1.170 -
1.171 - Calc ("op +", eval_binop "#add_"),
1.172 - Calc ("op -", eval_binop "#subtr_"),
1.173 -
1.174 - (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
1.175 - (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
1.176 - Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
1.177 - (*"(k + z1) + z1 = k + 2 * z1"*)
1.178 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.179 - (*"z1 + z1 = 2 * z1"*)
1.180 -
1.181 - Thm ("addiere_vor_minus",num_str addiere_vor_minus),
1.182 - (*"[| l is_const; m is_const |] ==> -(l * v) + m * v = (-l + m) *v"*)
1.183 - Thm ("addiere_eins_vor_minus",num_str addiere_eins_vor_minus),
1.184 - (*"[| m is_const |] ==> - v + m * v = (-1 + m) * v"*)
1.185 - Thm ("subtrahiere_vor_minus",num_str subtrahiere_vor_minus),
1.186 - (*"[| l is_const; m is_const |] ==> -(l * v) - m * v = (-l - m) *v"*)
1.187 - Thm ("subtrahiere_eins_vor_minus",num_str subtrahiere_eins_vor_minus)
1.188 - (*"[| m is_const |] ==> - v - m * v = (-1 - m) * v"*)
1.189 -
1.190 - ], scr = EmptyScr}:rls;
1.191 -
1.192 -val verschoenere =
1.193 - Rls{id = "verschoenere", preconds = [],
1.194 - rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
1.195 - erls = append_rls "erls_verschoenere" e_rls
1.196 - [Calc ("PolyMinus.kleiner", eval_kleiner "")],
1.197 - rules = [Thm ("vorzeichen_minus_weg1",num_str vorzeichen_minus_weg1),
1.198 - (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
1.199 - Thm ("vorzeichen_minus_weg2",num_str vorzeichen_minus_weg2),
1.200 - (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
1.201 - Thm ("vorzeichen_minus_weg3",num_str vorzeichen_minus_weg3),
1.202 - (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
1.203 - Thm ("vorzeichen_minus_weg4",num_str vorzeichen_minus_weg4),
1.204 - (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
1.205 -
1.206 - Calc ("op *", eval_binop "#mult_"),
1.207 -
1.208 - Thm ("real_mult_0",num_str real_mult_0),
1.209 - (*"0 * z = 0"*)
1.210 - Thm ("real_mult_1",num_str real_mult_1),
1.211 - (*"1 * z = z"*)
1.212 - Thm ("real_add_zero_left",num_str real_add_zero_left),
1.213 - (*"0 + z = z"*)
1.214 - Thm ("null_minus",num_str null_minus),
1.215 - (*"0 - a = -a"*)
1.216 - Thm ("vor_minus_mal",num_str vor_minus_mal)
1.217 - (*"- a * b = (-a) * b"*)
1.218 -
1.219 - (*Thm ("",num_str ),*)
1.220 - (**)
1.221 - ], scr = EmptyScr}:rls (*end verschoenere*);
1.222 -
1.223 -val klammern_aufloesen =
1.224 - Rls{id = "klammern_aufloesen", preconds = [],
1.225 - rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
1.226 - rules = [Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym)),
1.227 - (*"a + (b + c) = (a + b) + c"*)
1.228 - Thm ("klammer_plus_minus",num_str klammer_plus_minus),
1.229 - (*"a + (b - c) = (a + b) - c"*)
1.230 - Thm ("klammer_minus_plus",num_str klammer_minus_plus),
1.231 - (*"a - (b + c) = (a - b) - c"*)
1.232 - Thm ("klammer_minus_minus",num_str klammer_minus_minus)
1.233 - (*"a - (b - c) = (a - b) + c"*)
1.234 - ], scr = EmptyScr}:rls;
1.235 -
1.236 -val klammern_ausmultiplizieren =
1.237 - Rls{id = "klammern_ausmultiplizieren", preconds = [],
1.238 - rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
1.239 - rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.240 - (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.241 - Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.242 - (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.243 -
1.244 - Thm ("klammer_mult_minus",num_str klammer_mult_minus),
1.245 - (*"a * (b - c) = a * b - a * c"*)
1.246 - Thm ("klammer_minus_mult",num_str klammer_minus_mult)
1.247 - (*"(b - c) * a = b * a - c * a"*)
1.248 -
1.249 - (*Thm ("",num_str ),
1.250 - (*""*)*)
1.251 - ], scr = EmptyScr}:rls;
1.252 -
1.253 -val ordne_monome =
1.254 - Rls{id = "ordne_monome", preconds = [],
1.255 - rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
1.256 - erls = append_rls "erls_ordne_monome" e_rls
1.257 - [Calc ("PolyMinus.kleiner", eval_kleiner ""),
1.258 - Calc ("Atools.is'_atom", eval_is_atom "")
1.259 - ],
1.260 - rules = [Thm ("tausche_mal",num_str tausche_mal),
1.261 - (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
1.262 - Thm ("tausche_vor_mal",num_str tausche_vor_mal),
1.263 - (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
1.264 - Thm ("tausche_mal_mal",num_str tausche_mal_mal),
1.265 - (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
1.266 - Thm ("x_quadrat",num_str x_quadrat)
1.267 - (*"(x * a) * a = x * a ^^^ 2"*)
1.268 -
1.269 - (*Thm ("",num_str ),
1.270 - (*""*)*)
1.271 - ], scr = EmptyScr}:rls;
1.272 -
1.273 -
1.274 -val rls_p_33 =
1.275 - append_rls "rls_p_33" e_rls
1.276 - [Rls_ ordne_alphabetisch,
1.277 - Rls_ fasse_zusammen,
1.278 - Rls_ verschoenere
1.279 - ];
1.280 -val rls_p_34 =
1.281 - append_rls "rls_p_34" e_rls
1.282 - [Rls_ klammern_aufloesen,
1.283 - Rls_ ordne_alphabetisch,
1.284 - Rls_ fasse_zusammen,
1.285 - Rls_ verschoenere
1.286 - ];
1.287 -val rechnen =
1.288 - append_rls "rechnen" e_rls
1.289 - [Calc ("op *", eval_binop "#mult_"),
1.290 - Calc ("op +", eval_binop "#add_"),
1.291 - Calc ("op -", eval_binop "#subtr_")
1.292 - ];
1.293 -
1.294 -ruleset' :=
1.295 -overwritelthy thy (!ruleset',
1.296 - [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
1.297 - ("fasse_zusammen", prep_rls fasse_zusammen),
1.298 - ("verschoenere", prep_rls verschoenere),
1.299 - ("ordne_monome", prep_rls ordne_monome),
1.300 - ("klammern_aufloesen", prep_rls klammern_aufloesen),
1.301 - ("klammern_ausmultiplizieren",
1.302 - prep_rls klammern_ausmultiplizieren)
1.303 - ]);
1.304 -
1.305 -(** problems **)
1.306 -
1.307 -store_pbt
1.308 - (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID
1.309 - (["polynom","vereinfachen"],
1.310 - [], Erls, NONE, []));
1.311 -
1.312 -store_pbt
1.313 - (prep_pbt PolyMinus.thy "pbl_vereinf_poly_minus" [] e_pblID
1.314 - (["plus_minus","polynom","vereinfachen"],
1.315 - [("#Given" ,["term t_"]),
1.316 - ("#Where" ,["t_ is_polyexp",
1.317 - "Not (matchsub (?a + (?b + ?c)) t_ | \
1.318 - \ matchsub (?a + (?b - ?c)) t_ | \
1.319 - \ matchsub (?a - (?b + ?c)) t_ | \
1.320 - \ matchsub (?a + (?b - ?c)) t_ )",
1.321 - "Not (matchsub (?a * (?b + ?c)) t_ | \
1.322 - \ matchsub (?a * (?b - ?c)) t_ | \
1.323 - \ matchsub ((?b + ?c) * ?a) t_ | \
1.324 - \ matchsub ((?b - ?c) * ?a) t_ )"]),
1.325 - ("#Find" ,["normalform n_"])
1.326 - ],
1.327 - append_rls "prls_pbl_vereinf_poly" e_rls
1.328 - [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
1.329 - Calc ("Tools.matchsub", eval_matchsub ""),
1.330 - Thm ("or_true",or_true),
1.331 - (*"(?a | True) = True"*)
1.332 - Thm ("or_false",or_false),
1.333 - (*"(?a | False) = ?a"*)
1.334 - Thm ("not_true",num_str not_true),
1.335 - (*"(~ True) = False"*)
1.336 - Thm ("not_false",num_str not_false)
1.337 - (*"(~ False) = True"*)],
1.338 - SOME "Vereinfache t_",
1.339 - [["simplification","for_polynomials","with_minus"]]));
1.340 -
1.341 -store_pbt
1.342 - (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer" [] e_pblID
1.343 - (["klammer","polynom","vereinfachen"],
1.344 - [("#Given" ,["term t_"]),
1.345 - ("#Where" ,["t_ is_polyexp",
1.346 - "Not (matchsub (?a * (?b + ?c)) t_ | \
1.347 - \ matchsub (?a * (?b - ?c)) t_ | \
1.348 - \ matchsub ((?b + ?c) * ?a) t_ | \
1.349 - \ matchsub ((?b - ?c) * ?a) t_ )"]),
1.350 - ("#Find" ,["normalform n_"])
1.351 - ],
1.352 - append_rls "prls_pbl_vereinf_poly_klammer" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
1.353 - Calc ("Tools.matchsub", eval_matchsub ""),
1.354 - Thm ("or_true",or_true),
1.355 - (*"(?a | True) = True"*)
1.356 - Thm ("or_false",or_false),
1.357 - (*"(?a | False) = ?a"*)
1.358 - Thm ("not_true",num_str not_true),
1.359 - (*"(~ True) = False"*)
1.360 - Thm ("not_false",num_str not_false)
1.361 - (*"(~ False) = True"*)],
1.362 - SOME "Vereinfache t_",
1.363 - [["simplification","for_polynomials","with_parentheses"]]));
1.364 -
1.365 -store_pbt
1.366 - (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
1.367 - (["binom_klammer","polynom","vereinfachen"],
1.368 - [("#Given" ,["term t_"]),
1.369 - ("#Where" ,["t_ is_polyexp"]),
1.370 - ("#Find" ,["normalform n_"])
1.371 - ],
1.372 - append_rls "e_rls" e_rls [(*for preds in where_*)
1.373 - Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.374 - SOME "Vereinfache t_",
1.375 - [["simplification","for_polynomials","with_parentheses_mult"]]));
1.376 -
1.377 -store_pbt
1.378 - (prep_pbt PolyMinus.thy "pbl_probe" [] e_pblID
1.379 - (["probe"],
1.380 - [], Erls, NONE, []));
1.381 -
1.382 -store_pbt
1.383 - (prep_pbt PolyMinus.thy "pbl_probe_poly" [] e_pblID
1.384 - (["polynom","probe"],
1.385 - [("#Given" ,["Pruefe e_", "mitWert ws_"]),
1.386 - ("#Where" ,["e_ is_polyexp"]),
1.387 - ("#Find" ,["Geprueft p_"])
1.388 - ],
1.389 - append_rls "prls_pbl_probe_poly"
1.390 - e_rls [(*for preds in where_*)
1.391 - Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.392 - SOME "Probe e_ ws_",
1.393 - [["probe","fuer_polynom"]]));
1.394 -
1.395 -store_pbt
1.396 - (prep_pbt PolyMinus.thy "pbl_probe_bruch" [] e_pblID
1.397 - (["bruch","probe"],
1.398 - [("#Given" ,["Pruefe e_", "mitWert ws_"]),
1.399 - ("#Where" ,["e_ is_ratpolyexp"]),
1.400 - ("#Find" ,["Geprueft p_"])
1.401 - ],
1.402 - append_rls "prls_pbl_probe_bruch"
1.403 - e_rls [(*for preds in where_*)
1.404 - Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
1.405 - SOME "Probe e_ ws_",
1.406 - [["probe","fuer_bruch"]]));
1.407 -
1.408 -
1.409 -(** methods **)
1.410 -
1.411 -store_met
1.412 - (prep_met PolyMinus.thy "met_simp_poly_minus" [] e_metID
1.413 - (["simplification","for_polynomials","with_minus"],
1.414 - [("#Given" ,["term t_"]),
1.415 - ("#Where" ,["t_ is_polyexp",
1.416 - "Not (matchsub (?a + (?b + ?c)) t_ | \
1.417 - \ matchsub (?a + (?b - ?c)) t_ | \
1.418 - \ matchsub (?a - (?b + ?c)) t_ | \
1.419 - \ matchsub (?a + (?b - ?c)) t_ )"]),
1.420 - ("#Find" ,["normalform n_"])
1.421 - ],
1.422 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
1.423 - prls = append_rls "prls_met_simp_poly_minus" e_rls
1.424 - [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
1.425 - Calc ("Tools.matchsub", eval_matchsub ""),
1.426 - Thm ("and_true",and_true),
1.427 - (*"(?a & True) = ?a"*)
1.428 - Thm ("and_false",and_false),
1.429 - (*"(?a & False) = False"*)
1.430 - Thm ("not_true",num_str not_true),
1.431 - (*"(~ True) = False"*)
1.432 - Thm ("not_false",num_str not_false)
1.433 - (*"(~ False) = True"*)],
1.434 - crls = e_rls, nrls = rls_p_33},
1.435 -"Script SimplifyScript (t_::real) = \
1.436 -\ ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.437 -\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.438 -\ (Try (Rewrite_Set verschoenere False)))) t_)"
1.439 - ));
1.440 -
1.441 -store_met
1.442 - (prep_met PolyMinus.thy "met_simp_poly_parenth" [] e_metID
1.443 - (["simplification","for_polynomials","with_parentheses"],
1.444 - [("#Given" ,["term t_"]),
1.445 - ("#Where" ,["t_ is_polyexp"]),
1.446 - ("#Find" ,["normalform n_"])
1.447 - ],
1.448 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
1.449 - prls = append_rls "simplification_for_polynomials_prls" e_rls
1.450 - [(*for preds in where_*)
1.451 - Calc("Poly.is'_polyexp",eval_is_polyexp"")],
1.452 - crls = e_rls, nrls = rls_p_34},
1.453 -"Script SimplifyScript (t_::real) = \
1.454 -\ ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@ \
1.455 -\ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.456 -\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.457 -\ (Try (Rewrite_Set verschoenere False)))) t_)"
1.458 - ));
1.459 -
1.460 -store_met
1.461 - (prep_met PolyMinus.thy "met_simp_poly_parenth_mult" [] e_metID
1.462 - (["simplification","for_polynomials","with_parentheses_mult"],
1.463 - [("#Given" ,["term t_"]),
1.464 - ("#Where" ,["t_ is_polyexp"]),
1.465 - ("#Find" ,["normalform n_"])
1.466 - ],
1.467 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
1.468 - prls = append_rls "simplification_for_polynomials_prls" e_rls
1.469 - [(*for preds in where_*)
1.470 - Calc("Poly.is'_polyexp",eval_is_polyexp"")],
1.471 - crls = e_rls, nrls = rls_p_34},
1.472 -"Script SimplifyScript (t_::real) = \
1.473 -\ ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ \
1.474 -\ (Try (Rewrite_Set discard_parentheses False)) @@ \
1.475 -\ (Try (Rewrite_Set ordne_monome False)) @@ \
1.476 -\ (Try (Rewrite_Set klammern_aufloesen False)) @@ \
1.477 -\ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.478 -\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.479 -\ (Try (Rewrite_Set verschoenere False)))) t_)"
1.480 - ));
1.481 -
1.482 -store_met
1.483 - (prep_met PolyMinus.thy "met_probe" [] e_metID
1.484 - (["probe"],
1.485 - [],
1.486 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
1.487 - prls = Erls, crls = e_rls, nrls = Erls},
1.488 - "empty_script"));
1.489 -
1.490 -store_met
1.491 - (prep_met PolyMinus.thy "met_probe_poly" [] e_metID
1.492 - (["probe","fuer_polynom"],
1.493 - [("#Given" ,["Pruefe e_", "mitWert ws_"]),
1.494 - ("#Where" ,["e_ is_polyexp"]),
1.495 - ("#Find" ,["Geprueft p_"])
1.496 - ],
1.497 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
1.498 - prls = append_rls "prls_met_probe_bruch"
1.499 - e_rls [(*for preds in where_*)
1.500 - Calc ("Rational.is'_ratpolyexp",
1.501 - eval_is_ratpolyexp "")],
1.502 - crls = e_rls, nrls = rechnen},
1.503 -"Script ProbeScript (e_::bool) (ws_::bool list) = \
1.504 -\ (let e_ = Take e_; \
1.505 -\ e_ = Substitute ws_ e_ \
1.506 -\ in (Repeat((Try (Repeat (Calculate times))) @@ \
1.507 -\ (Try (Repeat (Calculate plus ))) @@ \
1.508 -\ (Try (Repeat (Calculate minus))))) e_)"
1.509 -));
1.510 -
1.511 -store_met
1.512 - (prep_met PolyMinus.thy "met_probe_bruch" [] e_metID
1.513 - (["probe","fuer_bruch"],
1.514 - [("#Given" ,["Pruefe e_", "mitWert ws_"]),
1.515 - ("#Where" ,["e_ is_ratpolyexp"]),
1.516 - ("#Find" ,["Geprueft p_"])
1.517 - ],
1.518 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
1.519 - prls = append_rls "prls_met_probe_bruch"
1.520 - e_rls [(*for preds in where_*)
1.521 - Calc ("Rational.is'_ratpolyexp",
1.522 - eval_is_ratpolyexp "")],
1.523 - crls = e_rls, nrls = Erls},
1.524 - "empty_script"));