1.1 --- a/src/Tools/isac/Build_Isac.thy Fri Sep 03 17:19:20 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Mon Sep 06 14:48:38 2010 +0200
1.3 @@ -65,6 +65,8 @@
1.4 use_thy "Knowledge/Poly"
1.5 *)
1.6 use_thy "Knowledge/Rational"
1.7 +use_thy "Knowledge/PolyMinus"
1.8 +use_thy "Knowledge/Equation"
1.9
1.10 ML {*
1.11 111;
1.12 @@ -73,8 +75,6 @@
1.13
1.14 text {*------------------------------------------*}
1.15 (*
1.16 -use_thy "Knowledge/PolyMinus"
1.17 -use_thy "Knowledge/Equation"
1.18 use_thy "Knowledge/LinEq"
1.19 use_thy "Knowledge/Root"
1.20 use_thy "Knowledge/RootEq"
2.1 --- a/src/Tools/isac/Interpret/solve.sml Fri Sep 03 17:19:20 2010 +0200
2.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Sep 06 14:48:38 2010 +0200
2.3 @@ -91,10 +91,24 @@
2.4
2.5 (*13.9.02--------------
2.6 type ctr = (loc * pos) list;
2.7 -val ops = [("PLUS","op +"),("minus","op -"),("TIMES","op *"),
2.8 +val ops = [("PLUS","op +"),("MINUS","op -"),("TIMES","op *"),
2.9 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")];
2.10 +ML {*
2.11 +@{term "PLUS"}; (*Free ("PLUS", "'a") : term*)
2.12 +@{term "plus"}; (*Const ("Groups.plus_class.plus", "'a => 'a => 'a")*)
2.13 +@{term "MINUS"}; (*Free ("MINUS", "'a")*)
2.14 +@{term "minus"}; (*Const ("Groups.minus_class.minus", "'a => 'a => 'a")*)
2.15 +@{term "TIMES"}; (*Free ("TIMES", "'a")*)
2.16 +@{term "times"}; (*Const ("Groups.times_class.times", "'a => 'a => 'a")*)
2.17 +@{term "CANCEL"}; (*Free ("CANCEL", "'a")*)
2.18 +@{term "cancel"}; (*Free ("cancel", "'a")*)
2.19 +@{term "POWER"}; (*Free ("POWER", "'a")*)
2.20 +@{term "pow"}; (*Free ("pow", "'a")*)
2.21 +@{term "SQRT"}; (*Free ("SQRT", "'a")*)
2.22 +@{term "sqrt"}; (*Const ("NthRoot.sqrt", "RealDef.real => RealDef.real")*)
2.23 +*}
2.24 fun op_intern op_ =
2.25 - case assoc (ops,op_) of
2.26 + case assoc (ops, op_) of
2.27 SOME op' => op' | NONE => raise error ("op_intern: no op= "^op_);
2.28 -----------------------*)
2.29
3.1 --- a/src/Tools/isac/Knowledge/Atools.thy Fri Sep 03 17:19:20 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Mon Sep 06 14:48:38 2010 +0200
3.3 @@ -694,8 +694,7 @@
3.4 ("ident" ,("Atools.ident",eval_ident "#ident_")),
3.5 ("equal" ,("op =",eval_equal "#equal_")),
3.6 ("PLUS" ,("op +" ,eval_binop "#add_")),
3.7 - ("minus" ,("op -",eval_binop "#sub_")), (*040207 only for prep_rls
3.8 - no script with "minus"*)
3.9 + ("MINUS" ,("op -",eval_binop "#sub_")),
3.10 ("TIMES" ,("op *" ,eval_binop "#mult_")),
3.11 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")),
3.12 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
4.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Fri Sep 03 17:19:20 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Sep 06 14:48:38 2010 +0200
4.3 @@ -215,7 +215,7 @@
4.4 Seq {id = "norm_Rational_noadd_fractions", preconds = [],
4.5 rew_ord = ("dummy_ord",dummy_ord),
4.6 erls = norm_rat_erls, srls = Erls, calc = [],
4.7 - rules = [Rls_ discard_minus1,
4.8 + rules = [Rls_ discard_minus,
4.9 Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
4.10 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
4.11 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
5.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri Sep 03 17:19:20 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Sep 06 14:48:38 2010 +0200
5.3 @@ -324,7 +324,7 @@
5.4 case poly_deg_in t v of SOME _ => true | NONE => false;
5.5 fun has_degree_in t v =
5.6 case expand_deg_in t v of SOME d => d | NONE => ~1;
5.7 -end;
5.8 +end;(*local*)
5.9 (* FIXME.WN100826 shift this into test-----------------------------
5.10 val v = (term_of o the o (parse thy)) "x";
5.11 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";
5.12 @@ -503,11 +503,9 @@
5.13 'rlsIDs' redefined by MG as 'rlsIDs_'
5.14 ^^^*)
5.15
5.16 -val discard_minus1 =
5.17 - Rls{id = "discard_minus1", preconds = [],
5.18 - rew_ord = ("dummy_ord", dummy_ord),
5.19 - erls = e_rls,srls = Erls,
5.20 - calc = [],
5.21 +val discard_minus =
5.22 + Rls{id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
5.23 + erls = e_rls, srls = Erls, calc = [],
5.24 (*asm_thm = [],*)
5.25 rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
5.26 (*"a - b = a + -1 * b"*)
5.27 @@ -515,6 +513,7 @@
5.28 num_str (@{thm real_mult_minus1} RS @{thm sym}))
5.29 (*- ?z = "-1 * ?z"*)
5.30 ], scr = EmptyScr}:rls;
5.31 +
5.32 val expand_poly_ =
5.33 Rls{id = "expand_poly_", preconds = [],
5.34 rew_ord = ("dummy_ord", dummy_ord),
5.35 @@ -1213,7 +1212,7 @@
5.36 | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
5.37 in
5.38 fun monom_degree l = counter (0, l)
5.39 -end;
5.40 +end;(*local*)
5.41
5.42 (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
5.43 der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
5.44 @@ -1432,7 +1431,7 @@
5.45 Seq {id = "make_polynomial", preconds = []:term list,
5.46 rew_ord = ("dummy_ord", dummy_ord),
5.47 erls = Atools_erls, srls = Erls,calc = [],
5.48 - rules = [Rls_ discard_minus1,
5.49 + rules = [Rls_ discard_minus,
5.50 Rls_ expand_poly_,
5.51 Calc ("op *", eval_binop "#mult_"),
5.52 Rls_ order_mult_rls_,
5.53 @@ -1450,7 +1449,7 @@
5.54 Seq {id = "norm_Poly", preconds = []:term list,
5.55 rew_ord = ("dummy_ord", dummy_ord),
5.56 erls = Atools_erls, srls = Erls, calc = [],
5.57 - rules = [Rls_ discard_minus1,
5.58 + rules = [Rls_ discard_minus,
5.59 Rls_ expand_poly_,
5.60 Calc ("op *", eval_binop "#mult_"),
5.61 Rls_ order_mult_rls_,
5.62 @@ -1472,7 +1471,7 @@
5.63 Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list,
5.64 rew_ord = ("dummy_ord", dummy_ord),
5.65 erls = Atools_erls, srls = Erls, calc = [],
5.66 - rules = [Rls_ discard_minus1,
5.67 + rules = [Rls_ discard_minus,
5.68 Rls_ expand_poly_rat_,(*ignors rationals*)
5.69 Calc ("op *", eval_binop "#mult_"),
5.70 Rls_ order_mult_rls_,
5.71 @@ -1569,7 +1568,7 @@
5.72 ("make_polynomial", prep_rls make_polynomial),
5.73 ("expand_binoms", prep_rls expand_binoms),
5.74 ("rev_rew_p", prep_rls rev_rew_p),
5.75 - ("discard_minus1", prep_rls discard_minus1),
5.76 + ("discard_minus", prep_rls discard_minus),
5.77 ("expand_poly_", prep_rls expand_poly_),
5.78 ("expand_poly_rat_", prep_rls expand_poly_rat_),
5.79 ("simplify_power_", prep_rls simplify_power_),
6.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Fri Sep 03 17:19:20 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Mon Sep 06 14:48:38 2010 +0200
6.3 @@ -25,85 +25,85 @@
6.4 => bool"
6.5 ("((Script ProbeScript (_ _ =))// (_))" 9)
6.6
6.7 -rules
6.8 +axioms
6.9
6.10 - null_minus "0 - a = -a"
6.11 - vor_minus_mal "- a * b = (-a) * b"
6.12 + null_minus: "0 - a = -a"
6.13 + vor_minus_mal: "- a * b = (-a) * b"
6.14
6.15 (*commute with invariant (a.b).c -association*)
6.16 - tausche_plus "[| b ist_monom; a kleiner b |] ==>
6.17 + tausche_plus: "[| b ist_monom; a kleiner b |] ==>
6.18 (b + a) = (a + b)"
6.19 - tausche_minus "[| b ist_monom; a kleiner b |] ==>
6.20 + tausche_minus: "[| b ist_monom; a kleiner b |] ==>
6.21 (b - a) = (-a + b)"
6.22 - tausche_vor_plus "[| b ist_monom; a kleiner b |] ==>
6.23 + tausche_vor_plus: "[| b ist_monom; a kleiner b |] ==>
6.24 (- b + a) = (a - b)"
6.25 - tausche_vor_minus "[| b ist_monom; a kleiner b |] ==>
6.26 + tausche_vor_minus: "[| b ist_monom; a kleiner b |] ==>
6.27 (- b - a) = (-a - b)"
6.28 - tausche_plus_plus "b kleiner c ==> (a + c + b) = (a + b + c)"
6.29 - tausche_plus_minus "b kleiner c ==> (a + c - b) = (a - b + c)"
6.30 - tausche_minus_plus "b kleiner c ==> (a - c + b) = (a + b - c)"
6.31 - tausche_minus_minus "b kleiner c ==> (a - c - b) = (a - b - c)"
6.32 + tausche_plus_plus: "b kleiner c ==> (a + c + b) = (a + b + c)"
6.33 + tausche_plus_minus: "b kleiner c ==> (a + c - b) = (a - b + c)"
6.34 + tausche_minus_plus: "b kleiner c ==> (a - c + b) = (a + b - c)"
6.35 + tausche_minus_minus: "b kleiner c ==> (a - c - b) = (a - b - c)"
6.36
6.37 (*commute with invariant (a.b).c -association*)
6.38 - tausche_mal "[| b is_atom; a kleiner b |] ==>
6.39 + tausche_mal: "[| b is_atom; a kleiner b |] ==>
6.40 (b * a) = (a * b)"
6.41 - tausche_vor_mal "[| b is_atom; a kleiner b |] ==>
6.42 + tausche_vor_mal: "[| b is_atom; a kleiner b |] ==>
6.43 (-b * a) = (-a * b)"
6.44 - tausche_mal_mal "[| c is_atom; b kleiner c |] ==>
6.45 + tausche_mal_mal: "[| c is_atom; b kleiner c |] ==>
6.46 (x * c * b) = (x * b * c)"
6.47 - x_quadrat "(x * a) * a = x * a ^^^ 2"
6.48 + x_quadrat: "(x * a) * a = x * a ^^^ 2"
6.49
6.50
6.51 - subtrahiere "[| l is_const; m is_const |] ==>
6.52 + subtrahiere: "[| l is_const; m is_const |] ==>
6.53 m * v - l * v = (m - l) * v"
6.54 - subtrahiere_von_1 "[| l is_const |] ==>
6.55 + subtrahiere_von_1: "[| l is_const |] ==>
6.56 v - l * v = (1 - l) * v"
6.57 - subtrahiere_1 "[| l is_const; m is_const |] ==>
6.58 + subtrahiere_1: "[| l is_const; m is_const |] ==>
6.59 m * v - v = (m - 1) * v"
6.60
6.61 - subtrahiere_x_plus_minus "[| l is_const; m is_const |] ==>
6.62 + subtrahiere_x_plus_minus: "[| l is_const; m is_const |] ==>
6.63 (x + m * v) - l * v = x + (m - l) * v"
6.64 - subtrahiere_x_plus1_minus "[| l is_const |] ==>
6.65 + subtrahiere_x_plus1_minus: "[| l is_const |] ==>
6.66 (x + v) - l * v = x + (1 - l) * v"
6.67 - subtrahiere_x_plus_minus1 "[| m is_const |] ==>
6.68 + subtrahiere_x_plus_minus1: "[| m is_const |] ==>
6.69 (x + m * v) - v = x + (m - 1) * v"
6.70
6.71 - subtrahiere_x_minus_plus "[| l is_const; m is_const |] ==>
6.72 + subtrahiere_x_minus_plus: "[| l is_const; m is_const |] ==>
6.73 (x - m * v) + l * v = x + (-m + l) * v"
6.74 - subtrahiere_x_minus1_plus "[| l is_const |] ==>
6.75 + subtrahiere_x_minus1_plus: "[| l is_const |] ==>
6.76 (x - v) + l * v = x + (-1 + l) * v"
6.77 - subtrahiere_x_minus_plus1 "[| m is_const |] ==>
6.78 + subtrahiere_x_minus_plus1: "[| m is_const |] ==>
6.79 (x - m * v) + v = x + (-m + 1) * v"
6.80
6.81 - subtrahiere_x_minus_minus "[| l is_const; m is_const |] ==>
6.82 + subtrahiere_x_minus_minus: "[| l is_const; m is_const |] ==>
6.83 (x - m * v) - l * v = x + (-m - l) * v"
6.84 - subtrahiere_x_minus1_minus"[| l is_const |] ==>
6.85 + subtrahiere_x_minus1_minus:"[| l is_const |] ==>
6.86 (x - v) - l * v = x + (-1 - l) * v"
6.87 - subtrahiere_x_minus_minus1"[| m is_const |] ==>
6.88 + subtrahiere_x_minus_minus1:"[| m is_const |] ==>
6.89 (x - m * v) - v = x + (-m - 1) * v"
6.90
6.91
6.92 - addiere_vor_minus "[| l is_const; m is_const |] ==>
6.93 + addiere_vor_minus: "[| l is_const; m is_const |] ==>
6.94 - (l * v) + m * v = (-l + m) * v"
6.95 - addiere_eins_vor_minus "[| m is_const |] ==>
6.96 + addiere_eins_vor_minus: "[| m is_const |] ==>
6.97 - v + m * v = (-1 + m) * v"
6.98 - subtrahiere_vor_minus "[| l is_const; m is_const |] ==>
6.99 + subtrahiere_vor_minus: "[| l is_const; m is_const |] ==>
6.100 - (l * v) - m * v = (-l - m) * v"
6.101 - subtrahiere_eins_vor_minus"[| m is_const |] ==>
6.102 + subtrahiere_eins_vor_minus:"[| m is_const |] ==>
6.103 - v - m * v = (-1 - m) * v"
6.104
6.105 - vorzeichen_minus_weg1 "l kleiner 0 ==> a + l * b = a - -1*l * b"
6.106 - vorzeichen_minus_weg2 "l kleiner 0 ==> a - l * b = a + -1*l * b"
6.107 - vorzeichen_minus_weg3 "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"
6.108 - vorzeichen_minus_weg4 "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"
6.109 + vorzeichen_minus_weg1: "l kleiner 0 ==> a + l * b = a - -1*l * b"
6.110 + vorzeichen_minus_weg2: "l kleiner 0 ==> a - l * b = a + -1*l * b"
6.111 + vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"
6.112 + vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"
6.113
6.114 (*klammer_plus_plus = (add_assoc RS sym)*)
6.115 - klammer_plus_minus "a + (b - c) = (a + b) - c"
6.116 - klammer_minus_plus "a - (b + c) = (a - b) - c"
6.117 - klammer_minus_minus "a - (b - c) = (a - b) + c"
6.118 + klammer_plus_minus: "a + (b - c) = (a + b) - c"
6.119 + klammer_minus_plus: "a - (b + c) = (a - b) - c"
6.120 + klammer_minus_minus: "a - (b - c) = (a - b) + c"
6.121
6.122 - klammer_mult_minus "a * (b - c) = a * b - a * c"
6.123 - klammer_minus_mult "(b - c) * a = b * a - c * a"
6.124 + klammer_mult_minus: "a * (b - c) = a * b - a * c"
6.125 + klammer_minus_mult: "(b - c) * a = b * a - c * a"
6.126
6.127 ML {*
6.128 val thy = @{theory};
6.129 @@ -213,7 +213,7 @@
6.130 (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
6.131 Thm ("tausche_minus_plus",num_str @{thm tausche_minus_plus}),
6.132 (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
6.133 - Thm ("tausche_minus_minus",num_str @{thm tausche_minus_minus)
6.134 + Thm ("tausche_minus_minus",num_str @{thm tausche_minus_minus})
6.135 (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
6.136 ], scr = EmptyScr}:rls;
6.137
6.138 @@ -407,66 +407,66 @@
6.139 store_pbt
6.140 (prep_pbt thy "pbl_vereinf_poly_minus" [] e_pblID
6.141 (["plus_minus","polynom","vereinfachen"],
6.142 - [("#Given" ,["TERM t_"]),
6.143 - ("#Where" ,["t_ is_polyexp",
6.144 - "Not (matchsub (?a + (?b + ?c)) t_ | " ^
6.145 - " matchsub (?a + (?b - ?c)) t_ | " ^
6.146 - " matchsub (?a - (?b + ?c)) t_ | " ^
6.147 - " matchsub (?a + (?b - ?c)) t_ )",
6.148 - "Not (matchsub (?a * (?b + ?c)) t_ | " ^
6.149 - " matchsub (?a * (?b - ?c)) t_ | " ^
6.150 - " matchsub ((?b + ?c) * ?a) t_ | " ^
6.151 - " matchsub ((?b - ?c) * ?a) t_ )"]),
6.152 - ("#Find" ,["normalform n_"])
6.153 + [("#Given" ,["TERM t_t"]),
6.154 + ("#Where" ,["t_t is_polyexp",
6.155 + "Not (matchsub (?a + (?b + ?c)) t_t | " ^
6.156 + " matchsub (?a + (?b - ?c)) t_t | " ^
6.157 + " matchsub (?a - (?b + ?c)) t_t | " ^
6.158 + " matchsub (?a + (?b - ?c)) t_t )",
6.159 + "Not (matchsub (?a * (?b + ?c)) t_t | " ^
6.160 + " matchsub (?a * (?b - ?c)) t_t | " ^
6.161 + " matchsub ((?b + ?c) * ?a) t_t | " ^
6.162 + " matchsub ((?b - ?c) * ?a) t_t )"]),
6.163 + ("#Find" ,["normalform n_n"])
6.164 ],
6.165 append_rls "prls_pbl_vereinf_poly" e_rls
6.166 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
6.167 Calc ("Tools.matchsub", eval_matchsub ""),
6.168 - Thm ("or_true",or_true),
6.169 + Thm ("or_true", num_str @{thm or_true}),
6.170 (*"(?a | True) = True"*)
6.171 - Thm ("or_false",or_false),
6.172 + Thm ("or_false", num_str @{thm or_false}),
6.173 (*"(?a | False) = ?a"*)
6.174 Thm ("not_true",num_str @{thm not_true}),
6.175 (*"(~ True) = False"*)
6.176 Thm ("not_false",num_str @{thm not_false})
6.177 (*"(~ False) = True"*)],
6.178 - SOME "Vereinfache t_",
6.179 + SOME "Vereinfache t_t",
6.180 [["simplification","for_polynomials","with_minus"]]));
6.181
6.182 store_pbt
6.183 (prep_pbt thy "pbl_vereinf_poly_klammer" [] e_pblID
6.184 (["klammer","polynom","vereinfachen"],
6.185 - [("#Given" ,["TERM t_"]),
6.186 - ("#Where" ,["t_ is_polyexp",
6.187 - "Not (matchsub (?a * (?b + ?c)) t_ | " ^
6.188 - " matchsub (?a * (?b - ?c)) t_ | " ^
6.189 - " matchsub ((?b + ?c) * ?a) t_ | " ^
6.190 - " matchsub ((?b - ?c) * ?a) t_ )"]),
6.191 - ("#Find" ,["normalform n_"])
6.192 + [("#Given" ,["TERM t_t"]),
6.193 + ("#Where" ,["t_t is_polyexp",
6.194 + "Not (matchsub (?a * (?b + ?c)) t_t | " ^
6.195 + " matchsub (?a * (?b - ?c)) t_t | " ^
6.196 + " matchsub ((?b + ?c) * ?a) t_t | " ^
6.197 + " matchsub ((?b - ?c) * ?a) t_t )"]),
6.198 + ("#Find" ,["normalform n_n"])
6.199 ],
6.200 append_rls "prls_pbl_vereinf_poly_klammer" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
6.201 Calc ("Tools.matchsub", eval_matchsub ""),
6.202 - Thm ("or_true",or_true),
6.203 + Thm ("or_true", num_str @{thm or_true}),
6.204 (*"(?a | True) = True"*)
6.205 - Thm ("or_false",or_false),
6.206 + Thm ("or_false", num_str @{thm or_false}),
6.207 (*"(?a | False) = ?a"*)
6.208 Thm ("not_true",num_str @{thm not_true}),
6.209 (*"(~ True) = False"*)
6.210 Thm ("not_false",num_str @{thm not_false})
6.211 (*"(~ False) = True"*)],
6.212 - SOME "Vereinfache t_",
6.213 + SOME "Vereinfache t_t",
6.214 [["simplification","for_polynomials","with_parentheses"]]));
6.215
6.216 store_pbt
6.217 (prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
6.218 (["binom_klammer","polynom","vereinfachen"],
6.219 - [("#Given" ,["TERM t_"]),
6.220 - ("#Where" ,["t_ is_polyexp"]),
6.221 - ("#Find" ,["normalform n_"])
6.222 + [("#Given" ,["TERM t_t"]),
6.223 + ("#Where" ,["t_t is_polyexp"]),
6.224 + ("#Find" ,["normalform n_n"])
6.225 ],
6.226 append_rls "e_rls" e_rls [(*for preds in where_*)
6.227 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
6.228 - SOME "Vereinfache t_",
6.229 + SOME "Vereinfache t_t",
6.230 [["simplification","for_polynomials","with_parentheses_mult"]]));
6.231
6.232 store_pbt
6.233 @@ -477,27 +477,27 @@
6.234 store_pbt
6.235 (prep_pbt thy "pbl_probe_poly" [] e_pblID
6.236 (["polynom","probe"],
6.237 - [("#Given" ,["Pruefe e_", "mitWert ws_"]),
6.238 - ("#Where" ,["e_ is_polyexp"]),
6.239 - ("#Find" ,["Geprueft p_"])
6.240 + [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
6.241 + ("#Where" ,["e_e is_polyexp"]),
6.242 + ("#Find" ,["Geprueft p_p"])
6.243 ],
6.244 append_rls "prls_pbl_probe_poly"
6.245 e_rls [(*for preds in where_*)
6.246 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
6.247 - SOME "Probe e_ ws_",
6.248 + SOME "Probe e_e w_w",
6.249 [["probe","fuer_polynom"]]));
6.250
6.251 store_pbt
6.252 (prep_pbt thy "pbl_probe_bruch" [] e_pblID
6.253 (["bruch","probe"],
6.254 - [("#Given" ,["Pruefe e_", "mitWert ws_"]),
6.255 - ("#Where" ,["e_ is_ratpolyexp"]),
6.256 - ("#Find" ,["Geprueft p_"])
6.257 + [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
6.258 + ("#Where" ,["e_e is_ratpolyexp"]),
6.259 + ("#Find" ,["Geprueft p_p"])
6.260 ],
6.261 append_rls "prls_pbl_probe_bruch"
6.262 e_rls [(*for preds in where_*)
6.263 Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
6.264 - SOME "Probe e_ ws_",
6.265 + SOME "Probe e_e w_w",
6.266 [["probe","fuer_bruch"]]));
6.267
6.268
6.269 @@ -506,72 +506,72 @@
6.270 store_met
6.271 (prep_met thy "met_simp_poly_minus" [] e_metID
6.272 (["simplification","for_polynomials","with_minus"],
6.273 - [("#Given" ,["TERM t_"]),
6.274 - ("#Where" ,["t_ is_polyexp",
6.275 - "Not (matchsub (?a + (?b + ?c)) t_ | " ^
6.276 - " matchsub (?a + (?b - ?c)) t_ | " ^
6.277 - " matchsub (?a - (?b + ?c)) t_ | " ^
6.278 - " matchsub (?a + (?b - ?c)) t_ )"]),
6.279 - ("#Find" ,["normalform n_"])
6.280 + [("#Given" ,["TERM t_t"]),
6.281 + ("#Where" ,["t_t is_polyexp",
6.282 + "Not (matchsub (?a + (?b + ?c)) t_t | " ^
6.283 + " matchsub (?a + (?b - ?c)) t_t | " ^
6.284 + " matchsub (?a - (?b + ?c)) t_t | " ^
6.285 + " matchsub (?a + (?b - ?c)) t_t )"]),
6.286 + ("#Find" ,["normalform n_n"])
6.287 ],
6.288 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
6.289 prls = append_rls "prls_met_simp_poly_minus" e_rls
6.290 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
6.291 Calc ("Tools.matchsub", eval_matchsub ""),
6.292 - Thm ("and_true",and_true),
6.293 + Thm ("and_true",num_str @{thm and_true}),
6.294 (*"(?a & True) = ?a"*)
6.295 - Thm ("and_false",and_false),
6.296 + Thm ("and_false",num_str @{thm and_false}),
6.297 (*"(?a & False) = False"*)
6.298 Thm ("not_true",num_str @{thm not_true}),
6.299 (*"(~ True) = False"*)
6.300 Thm ("not_false",num_str @{thm not_false})
6.301 (*"(~ False) = True"*)],
6.302 crls = e_rls, nrls = rls_p_33},
6.303 -"Script SimplifyScript (t_::real) = " ^
6.304 +"Script SimplifyScript (t_t::real) = " ^
6.305 " ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
6.306 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
6.307 -" (Try (Rewrite_Set verschoenere False)))) t_)"
6.308 +" (Try (Rewrite_Set verschoenere False)))) t_t)"
6.309 ));
6.310
6.311 store_met
6.312 (prep_met thy "met_simp_poly_parenth" [] e_metID
6.313 (["simplification","for_polynomials","with_parentheses"],
6.314 - [("#Given" ,["TERM t_"]),
6.315 - ("#Where" ,["t_ is_polyexp"]),
6.316 - ("#Find" ,["normalform n_"])
6.317 + [("#Given" ,["TERM t_t"]),
6.318 + ("#Where" ,["t_t is_polyexp"]),
6.319 + ("#Find" ,["normalform n_n"])
6.320 ],
6.321 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
6.322 prls = append_rls "simplification_for_polynomials_prls" e_rls
6.323 [(*for preds in where_*)
6.324 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
6.325 crls = e_rls, nrls = rls_p_34},
6.326 -"Script SimplifyScript (t_::real) = " ^
6.327 +"Script SimplifyScript (t_t::real) = " ^
6.328 " ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@ " ^
6.329 " (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
6.330 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
6.331 -" (Try (Rewrite_Set verschoenere False)))) t_)"
6.332 +" (Try (Rewrite_Set verschoenere False)))) t_t)"
6.333 ));
6.334
6.335 store_met
6.336 (prep_met thy "met_simp_poly_parenth_mult" [] e_metID
6.337 (["simplification","for_polynomials","with_parentheses_mult"],
6.338 - [("#Given" ,["TERM t_"]),
6.339 - ("#Where" ,["t_ is_polyexp"]),
6.340 - ("#Find" ,["normalform n_"])
6.341 + [("#Given" ,["TERM t_t"]),
6.342 + ("#Where" ,["t_t is_polyexp"]),
6.343 + ("#Find" ,["normalform n_n"])
6.344 ],
6.345 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
6.346 prls = append_rls "simplification_for_polynomials_prls" e_rls
6.347 [(*for preds in where_*)
6.348 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
6.349 crls = e_rls, nrls = rls_p_34},
6.350 -"Script SimplifyScript (t_::real) = " ^
6.351 +"Script SimplifyScript (t_t::real) = " ^
6.352 " ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ " ^
6.353 " (Try (Rewrite_Set discard_parentheses False)) @@ " ^
6.354 " (Try (Rewrite_Set ordne_monome False)) @@ " ^
6.355 " (Try (Rewrite_Set klammern_aufloesen False)) @@ " ^
6.356 " (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
6.357 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
6.358 -" (Try (Rewrite_Set verschoenere False)))) t_)"
6.359 +" (Try (Rewrite_Set verschoenere False)))) t_t)"
6.360 ));
6.361
6.362 store_met
6.363 @@ -585,9 +585,9 @@
6.364 store_met
6.365 (prep_met thy "met_probe_poly" [] e_metID
6.366 (["probe","fuer_polynom"],
6.367 - [("#Given" ,["Pruefe e_", "mitWert ws_"]),
6.368 - ("#Where" ,["e_ is_polyexp"]),
6.369 - ("#Find" ,["Geprueft p_"])
6.370 + [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
6.371 + ("#Where" ,["e_e is_polyexp"]),
6.372 + ("#Find" ,["Geprueft p_p"])
6.373 ],
6.374 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
6.375 prls = append_rls "prls_met_probe_bruch"
6.376 @@ -595,20 +595,20 @@
6.377 Calc ("Rational.is'_ratpolyexp",
6.378 eval_is_ratpolyexp "")],
6.379 crls = e_rls, nrls = rechnen},
6.380 -"Script ProbeScript (e_::bool) (ws_::bool list) = " ^
6.381 -" (let e_ = Take e_; " ^
6.382 -" e_ = Substitute ws_ e_ " ^
6.383 +"Script ProbeScript (e_e::bool) (w_w::bool list) = " ^
6.384 +" (let e_e = Take e_e; " ^
6.385 +" e_e = Substitute w_w e_e " ^
6.386 " in (Repeat((Try (Repeat (Calculate TIMES))) @@ " ^
6.387 " (Try (Repeat (Calculate PLUS ))) @@ " ^
6.388 -" (Try (Repeat (Calculate minus))))) e_)"
6.389 +" (Try (Repeat (Calculate MINUS))))) e_e)"
6.390 ));
6.391
6.392 store_met
6.393 (prep_met thy "met_probe_bruch" [] e_metID
6.394 (["probe","fuer_bruch"],
6.395 - [("#Given" ,["Pruefe e_", "mitWert ws_"]),
6.396 - ("#Where" ,["e_ is_ratpolyexp"]),
6.397 - ("#Find" ,["Geprueft p_"])
6.398 + [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
6.399 + ("#Where" ,["e_e is_ratpolyexp"]),
6.400 + ("#Find" ,["Geprueft p_p"])
6.401 ],
6.402 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
6.403 prls = append_rls "prls_met_probe_bruch"
7.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri Sep 03 17:19:20 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Sep 06 14:48:38 2010 +0200
7.3 @@ -3436,12 +3436,13 @@
7.4 (*-------------------18.3.03 --> struct <-----------vvv--*)
7.5 val add_fractions_p = common_nominator_p; (*FIXXXME:eilig f"ur norm_Rational*)
7.6
7.7 -(*.discard binary minus, shift unary minus into -1*;
7.8 +(*WN100906 removed in favour of discard_minus = discard_minus_ formerly
7.9 + discard binary minus, shift unary minus into -1*;
7.10 unary minus before numerals are put into the numeral by parsing;
7.11 - contains absolute minimum of thms for context in norm_Rational .*)
7.12 + contains absolute minimum of thms for context in norm_Rational
7.13 val discard_minus = prep_rls(
7.14 Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
7.15 - erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
7.16 + erls = e_rls, srls = Erls, calc = [],
7.17 rules = [Thm ("real_diff_minus", num_str @{thm real_diff_minus}),
7.18 (*"a - b = a + -1 * b"*)
7.19 Thm ("sym_real_mult_minus1",
7.20 @@ -3450,6 +3451,8 @@
7.21 ],
7.22 scr = EmptyScr
7.23 }):rls;
7.24 + *)
7.25 +
7.26 (*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
7.27 val powers_erls = prep_rls(
7.28 Rls {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
7.29 @@ -3729,7 +3732,7 @@
7.30 Seq {id = "norm_Rational"(*_mg*), preconds = [],
7.31 rew_ord = ("dummy_ord",dummy_ord),
7.32 erls = norm_rat_erls, srls = Erls, calc = [],
7.33 - rules = [Rls_ discard_minus1,
7.34 + rules = [Rls_ discard_minus,
7.35 Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
7.36 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
7.37 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
7.38 @@ -3801,7 +3804,7 @@
7.39 eval_is_ratpolyexp "")],
7.40 crls = e_rls, nrls = norm_Rational_rls},
7.41 "Script SimplifyScript (t_t::real) = " ^
7.42 -" ((Try (Rewrite_Set discard_minus1 False) @@ " ^
7.43 +" ((Try (Rewrite_Set discard_minus False) @@ " ^
7.44 " Try (Rewrite_Set rat_mult_poly False) @@ " ^
7.45 " Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ " ^
7.46 " Try (Rewrite_Set cancel_p_rls False) @@ " ^
8.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Fri Sep 03 17:19:20 2010 +0200
8.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Sep 06 14:48:38 2010 +0200
8.3 @@ -324,7 +324,7 @@
8.4 \ e_ = Substitute ws_ e_ \
8.5 \ in (Repeat((Try (Repeat (Calculate TIMES))) @@ \
8.6 \ (Try (Repeat (Calculate PLUS ))) @@ \
8.7 -\ (Try (Repeat (Calculate minus))))) e_)"
8.8 +\ (Try (Repeat (Calculate MINUS))))) e_)"
8.9 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
8.10 atomty sc;
8.11
9.1 --- a/test/Tools/isac/Knowledge/rational.sml Fri Sep 03 17:19:20 2010 +0200
9.2 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Sep 06 14:48:38 2010 +0200
9.3 @@ -2090,7 +2090,7 @@
9.4 (*no trailing _*)
9.5 val p1 = parse thy (
9.6 "Script SimplifyScript (t_t::real) = " ^
9.7 -" (Rewrite_Set discard_minus1 False " ^
9.8 +" (Rewrite_Set discard_minus False " ^
9.9 " t_t)");
9.10
9.11 (*required (): (Rewrite_Set discard_minus False)*)
10.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Fri Sep 03 17:19:20 2010 +0200
10.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Mon Sep 06 14:48:38 2010 +0200
10.3 @@ -29,7 +29,7 @@
10.4 (prep_met Test.thy "met_testinter" [] e_metID
10.5 (["Test","test_interSteps_1"]:metID,
10.6 [("#Given" ,["TERM t_"]),
10.7 - ("#Find" ,["normalform n_"])
10.8 + ("#Find" ,["normalform n_n"])
10.9 ],
10.10 {rew_ord'="dummy_ord",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,
10.11 crls=tval_rls, nrls=e_rls},