1.1 --- a/src/Tools/isac/Build_Isac.thy Fri Sep 03 14:28:38 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Fri Sep 03 17:19:20 2010 +0200
1.3 @@ -58,25 +58,19 @@
1.4
1.5 ML {* writeln "**** build the Knowledge *********************************" *}
1.6 (*use_thy "Knowledge/Typefix"*)
1.7 -use_thy "Knowledge/Delete"
1.8 -use_thy "Knowledge/Descript"
1.9 -use_thy "Knowledge/Atools"
1.10 -use_thy "Knowledge/Simplify"
1.11 -use_thy "Knowledge/Poly"
1.12 -
1.13 -ML {*
1.14 -val r = @{thm divide_minus1};
1.15 -*}
1.16 -lemma "(x::real) / -1 = - x"
1.17 -by (rule divide_minus1)
1.18 -
1.19 -
1.20 +(*use_thy "Knowledge/Delete"
1.21 + use_thy "Knowledge/Descript"
1.22 + use_thy "Knowledge/Atools"
1.23 + use_thy "Knowledge/Simplify"
1.24 + use_thy "Knowledge/Poly"
1.25 +*)
1.26 use_thy "Knowledge/Rational"
1.27
1.28 ML {*
1.29 -val ------+ = "123";
1.30 +111;
1.31 *}
1.32
1.33 +
1.34 text {*------------------------------------------*}
1.35 (*
1.36 use_thy "Knowledge/PolyMinus"
2.1 --- a/src/Tools/isac/Interpret/rewtools.sml Fri Sep 03 14:28:38 2010 +0200
2.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Fri Sep 03 17:19:20 2010 +0200
2.3 @@ -173,7 +173,7 @@
2.4 THERE IS SOMETHING DIFFERENT beetween rewriting with the code above
2.5 and between rewriting with rewrite_set: with rules from make_polynomial and
2.6 t = "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)" the actual code
2.7 -leads to cycling Rls_ order_mult_rls_..Rls_ discard_parentheses_..Rls_ order..
2.8 +leads to cycling Rls_ order_mult_rls_..Rls_ discard_parentheses1..Rls_ order..
2.9 *)
2.10 in rew_once (!lim_deriv) [] tt Noap rs end;
2.11
3.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Fri Sep 03 14:28:38 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Fri Sep 03 17:19:20 2010 +0200
3.3 @@ -187,11 +187,14 @@
3.4 Thm ("rat_mult_poly_r",num_str @{thm rat_mult_poly_r}),
3.5 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
3.6
3.7 - Thm ("real_divide_divide1_mg", @{thm real_divide_divide1_mg}),
3.8 + Thm ("real_divide_divide1_mg",
3.9 + num_str @{thm real_divide_divide1_mg}),
3.10 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
3.11 - Thm ("real_divide_divide_eq_right", @{thm real_divide_divide1_eq}),
3.12 + Thm ("divide_divide_eq_right",
3.13 + num_str @{thm divide_divide_eq_right}),
3.14 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
3.15 - Thm ("real_divide_divide_eq_left", @{thm real_divide_divide2_eq}),
3.16 + Thm ("divide_divide_eq_left",
3.17 + num_str @{thm divide_divide_eq_left}),
3.18 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
3.19 Calc ("HOL.divide" ,eval_cancel "#divide_"),
3.20
3.21 @@ -212,12 +215,12 @@
3.22 Seq {id = "norm_Rational_noadd_fractions", preconds = [],
3.23 rew_ord = ("dummy_ord",dummy_ord),
3.24 erls = norm_rat_erls, srls = Erls, calc = [],
3.25 - rules = [Rls_ discard_minus_,
3.26 + rules = [Rls_ discard_minus1,
3.27 Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
3.28 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
3.29 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
3.30 Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
3.31 - Rls_ discard_parentheses_ (* mult only *)
3.32 + Rls_ discard_parentheses1 (* mult only *)
3.33 ],
3.34 scr = Script ((term_of o the o (parse thy)) "empty_script")
3.35 }:rls;
4.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri Sep 03 14:28:38 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri Sep 03 17:19:20 2010 +0200
4.3 @@ -503,8 +503,8 @@
4.4 'rlsIDs' redefined by MG as 'rlsIDs_'
4.5 ^^^*)
4.6
4.7 -val discard_minus_ =
4.8 - Rls{id = "discard_minus_", preconds = [],
4.9 +val discard_minus1 =
4.10 + Rls{id = "discard_minus1", preconds = [],
4.11 rew_ord = ("dummy_ord", dummy_ord),
4.12 erls = e_rls,srls = Erls,
4.13 calc = [],
4.14 @@ -735,8 +735,8 @@
4.15 ], scr = EmptyScr}:rls;
4.16
4.17 (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
4.18 -val discard_parentheses_ =
4.19 - append_rls "discard_parentheses_" e_rls
4.20 +val discard_parentheses1 =
4.21 + append_rls "discard_parentheses1" e_rls
4.22 [Thm ("sym_real_mult_assoc",
4.23 num_str (@{thm real_mult_assoc} RS @{thm sym}))
4.24 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
4.25 @@ -1432,7 +1432,7 @@
4.26 Seq {id = "make_polynomial", preconds = []:term list,
4.27 rew_ord = ("dummy_ord", dummy_ord),
4.28 erls = Atools_erls, srls = Erls,calc = [],
4.29 - rules = [Rls_ discard_minus_,
4.30 + rules = [Rls_ discard_minus1,
4.31 Rls_ expand_poly_,
4.32 Calc ("op *", eval_binop "#mult_"),
4.33 Rls_ order_mult_rls_,
4.34 @@ -1442,7 +1442,7 @@
4.35 Rls_ order_add_rls_,
4.36 Rls_ collect_numerals_,
4.37 Rls_ reduce_012_,
4.38 - Rls_ discard_parentheses_
4.39 + Rls_ discard_parentheses1
4.40 ],
4.41 scr = EmptyScr
4.42 }:rls;
4.43 @@ -1450,7 +1450,7 @@
4.44 Seq {id = "norm_Poly", preconds = []:term list,
4.45 rew_ord = ("dummy_ord", dummy_ord),
4.46 erls = Atools_erls, srls = Erls, calc = [],
4.47 - rules = [Rls_ discard_minus_,
4.48 + rules = [Rls_ discard_minus1,
4.49 Rls_ expand_poly_,
4.50 Calc ("op *", eval_binop "#mult_"),
4.51 Rls_ order_mult_rls_,
4.52 @@ -1460,19 +1460,19 @@
4.53 Rls_ order_add_rls_,
4.54 Rls_ collect_numerals_,
4.55 Rls_ reduce_012_,
4.56 - Rls_ discard_parentheses_
4.57 + Rls_ discard_parentheses1
4.58 ],
4.59 scr = EmptyScr
4.60 }:rls;
4.61
4.62 -(* MG:03 Like make_polynomial_ but without Rls_ discard_parentheses_
4.63 +(* MG:03 Like make_polynomial_ but without Rls_ discard_parentheses1
4.64 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
4.65 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
4.66 val make_rat_poly_with_parentheses =
4.67 Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list,
4.68 rew_ord = ("dummy_ord", dummy_ord),
4.69 erls = Atools_erls, srls = Erls, calc = [],
4.70 - rules = [Rls_ discard_minus_,
4.71 + rules = [Rls_ discard_minus1,
4.72 Rls_ expand_poly_rat_,(*ignors rationals*)
4.73 Calc ("op *", eval_binop "#mult_"),
4.74 Rls_ order_mult_rls_,
4.75 @@ -1482,7 +1482,7 @@
4.76 Rls_ order_add_rls_,
4.77 Rls_ collect_numerals_,
4.78 Rls_ reduce_012_
4.79 - (*Rls_ discard_parentheses_ *)
4.80 + (*Rls_ discard_parentheses1 *)
4.81 ],
4.82 scr = EmptyScr
4.83 }:rls;
4.84 @@ -1569,14 +1569,14 @@
4.85 ("make_polynomial", prep_rls make_polynomial),
4.86 ("expand_binoms", prep_rls expand_binoms),
4.87 ("rev_rew_p", prep_rls rev_rew_p),
4.88 - ("discard_minus_", prep_rls discard_minus_),
4.89 + ("discard_minus1", prep_rls discard_minus1),
4.90 ("expand_poly_", prep_rls expand_poly_),
4.91 ("expand_poly_rat_", prep_rls expand_poly_rat_),
4.92 ("simplify_power_", prep_rls simplify_power_),
4.93 ("calc_add_mult_pow_", prep_rls calc_add_mult_pow_),
4.94 ("reduce_012_mult_", prep_rls reduce_012_mult_),
4.95 ("reduce_012_", prep_rls reduce_012_),
4.96 - ("discard_parentheses_",prep_rls discard_parentheses_),
4.97 + ("discard_parentheses1",prep_rls discard_parentheses1),
4.98 ("order_mult_rls_", prep_rls order_mult_rls_),
4.99 ("order_add_rls_", prep_rls order_add_rls_),
4.100 ("make_rat_poly_with_parentheses",
5.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri Sep 03 14:28:38 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Sep 03 17:19:20 2010 +0200
5.3 @@ -85,9 +85,8 @@
5.4 numerator and nominator in normalform [2] or [3].
5.5 *}
5.6
5.7 -ML {*
5.8 +ML {*
5.9 val thy = @{theory};
5.10 -val ------------------------------------------------------+ = "11111";
5.11
5.12 signature RATIONALI =
5.13 sig
5.14 @@ -135,8 +134,6 @@
5.15 (*WN0210???SK: fehlen Funktionen, die exportiert werden sollen ? *)
5.16 end
5.17
5.18 -val ------------------------------------------------------++ = "22222";
5.19 -
5.20 (*.**************************************************************************
5.21 survey on the functions
5.22 ~~~~~~~~~~~~~~~~~~~~~~~
5.23 @@ -2826,8 +2823,6 @@
5.24 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)
5.25 ], scr = EmptyScr})
5.26 calculate_Poly);
5.27 -val ------------------------------------------------------+++ = "33333";
5.28 -
5.29
5.30 (*("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))*)
5.31 fun eval_is_expanded (thmid:string) _
5.32 @@ -2866,8 +2861,6 @@
5.33
5.34 (* ************************************************************************* *)
5.35
5.36 -val ------------------------------------------------------++++ = "44444";
5.37 -
5.38 local(*. cancel_p
5.39 ------------------------
5.40 cancels a single fraction consisting of two (uni- or multivariate)
5.41 @@ -3020,8 +3013,6 @@
5.42 attach_form = attach_form}}
5.43 end;(*local*)
5.44
5.45 -val ------------------------------------------------------+++++ = "55555";
5.46 -
5.47 local(*.ad (1) 'cancel'
5.48 ------------------------------
5.49 cancels a single fraction consisting of two (uni- or multivariate)
5.50 @@ -3079,9 +3070,9 @@
5.51 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
5.52 []:(rule * (term * term list)) list;
5.53
5.54 -val pat = (term_of o the o (parse thy)) "?r/?s";
5.55 -val pre1 = (term_of o the o (parse thy)) "?r is_expanded";
5.56 -val pre2 = (term_of o the o (parse thy)) "?s is_expanded";
5.57 +val pat = parse_patt thy "?r/?s";
5.58 +val pre1 = parse_patt thy "?r is_expanded";
5.59 +val pre2 = parse_patt thy "?s is_expanded";
5.60 val prepat = [([pre1, pre2], pat)];
5.61
5.62 in
5.63 @@ -3103,9 +3094,6 @@
5.64 attach_form = attach_form}}
5.65 end;(*local*)
5.66
5.67 -val ------------------------------------------------------+++++-+ = "66666";
5.68 -
5.69 -
5.70 local(*.ad [2] 'common_nominator_p'
5.71 ---------------------------------
5.72 FIXME Beschreibung .*)
5.73 @@ -3230,9 +3218,9 @@
5.74 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
5.75 []:(rule * (term * term list)) list;
5.76
5.77 -val pat0 = (term_of o the o (parse thy)) "?r/?s+?u/?v";
5.78 -val pat1 = (term_of o the o (parse thy)) "?r/?s+?u ";
5.79 -val pat2 = (term_of o the o (parse thy)) "?r +?u/?v";
5.80 +val pat0 = parse_patt thy "?r/?s+?u/?v";
5.81 +val pat1 = parse_patt thy "?r/?s+?u ";
5.82 +val pat2 = parse_patt thy "?r +?u/?v";
5.83 val prepat = [([HOLogic.true_const], pat0),
5.84 ([HOLogic.true_const], pat1),
5.85 ([HOLogic.true_const], pat2)];
5.86 @@ -3258,8 +3246,6 @@
5.87 attach_form = attach_form}}
5.88 end;(*local*)
5.89
5.90 -val ------------------------------------------------------+++++-++ = "77777";
5.91 -
5.92 local(*.ad [2] 'common_nominator'
5.93 ---------------------------------
5.94 FIXME Beschreibung .*)
5.95 @@ -3275,10 +3261,6 @@
5.96
5.97 (*.init_state = fn : term -> istate
5.98 initialzies the state of the interactive interpreter. The state is:
5.99 -
5.100 -val ------------------------------------------------------+++++-++++ = "99999";
5.101 -val ------------------------------------------------------+++++-+++++ = "00000";
5.102 -
5.103 type rrlsstate = (*state for reverse rewriting*)
5.104 (term * (*the current formula*)
5.105 term * (*the final term*)
5.106 @@ -3380,12 +3362,12 @@
5.107 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
5.108 []:(rule * (term * term list)) list;
5.109
5.110 -val pat0 = (term_of o the o (parse thy)) "?r/?s+?u/?v";
5.111 -val pat01 = (term_of o the o (parse thy)) "?r/?s-?u/?v";
5.112 -val pat1 = (term_of o the o (parse thy)) "?r/?s+?u ";
5.113 -val pat11 = (term_of o the o (parse thy)) "?r/?s-?u ";
5.114 -val pat2 = (term_of o the o (parse thy)) "?r +?u/?v";
5.115 -val pat21 = (term_of o the o (parse thy)) "?r -?u/?v";
5.116 +val pat0 = parse_patt thy "?r/?s+?u/?v";
5.117 +val pat01 = parse_patt thy "?r/?s-?u/?v";
5.118 +val pat1 = parse_patt thy "?r/?s+?u ";
5.119 +val pat11 = parse_patt thy "?r/?s-?u ";
5.120 +val pat2 = parse_patt thy "?r +?u/?v";
5.121 +val pat21 = parse_patt thy "?r -?u/?v";
5.122 val prepat = [([HOLogic.true_const], pat0),
5.123 ([HOLogic.true_const], pat01),
5.124 ([HOLogic.true_const], pat1),
5.125 @@ -3415,8 +3397,6 @@
5.126 end;(*local*)
5.127 end;(*struct*)
5.128
5.129 -val ------------------------------------------------------+++++-+++ = "88888";
5.130 -
5.131 open RationalI;
5.132 (*##*)
5.133
5.134 @@ -3468,8 +3448,7 @@
5.135 num_str (@{thm real_mult_minus1} RS @{thm sym}))
5.136 (*- ?z = "-1 * ?z"*)
5.137 ],
5.138 - scr = Script ((term_of o the o (parse thy))
5.139 - "empty_script")
5.140 + scr = EmptyScr
5.141 }):rls;
5.142 (*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
5.143 val powers_erls = prep_rls(
5.144 @@ -3478,12 +3457,11 @@
5.145 rules = [Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
5.146 Calc ("Atools.is'_even",eval_is_even "#is_even_"),
5.147 Calc ("op <",eval_equ "#less_"),
5.148 - Thm ("not_false", not_false),
5.149 - Thm ("not_true", not_true),
5.150 + Thm ("not_false", num_str @{thm not_false}),
5.151 + Thm ("not_true", num_str @{thm not_true}),
5.152 Calc ("op +",eval_binop "#add_")
5.153 ],
5.154 - scr = Script ((term_of o the o (parse thy))
5.155 - "empty_script")
5.156 + scr = EmptyScr
5.157 }:rls);
5.158 (*.all powers over + distributed; atoms over * collected, other distributed
5.159 contains absolute minimum of thms for context in norm_Rational .*)
5.160 @@ -3516,8 +3494,7 @@
5.161 (*"1 ^^^ n = 1"*)
5.162 Calc ("op +",eval_binop "#add_")
5.163 ],
5.164 - scr = Script ((term_of o the o (parse thy))
5.165 - "empty_script")
5.166 + scr = EmptyScr
5.167 }:rls);
5.168 (*.contains absolute minimum of thms for context in norm_Rational.*)
5.169 val rat_mult_divide = prep_rls(
5.170 @@ -3533,14 +3510,17 @@
5.171 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x^^^n too much
5.172 and does not commute a / b * c ^^^ 2 !*)
5.173
5.174 - Thm ("divide_divide_eq_right", real_divide_divide1_eq),
5.175 + Thm ("divide_divide_eq_right",
5.176 + num_str @{thm divide_divide_eq_right}),
5.177 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
5.178 - Thm ("divide_divide_eq_left", real_divide_divide2_eq),
5.179 + Thm ("divide_divide_eq_left",
5.180 + num_str @{thm divide_divide_eq_left}),
5.181 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
5.182 Calc ("HOL.divide" ,eval_cancel "#divide_")
5.183 ],
5.184 - scr = Script ((term_of o the o (parse thy)) "empty_script")
5.185 + scr = EmptyScr
5.186 }:rls);
5.187 +
5.188 (*.contains absolute minimum of thms for context in norm_Rational.*)
5.189 val reduce_0_1_2 = prep_rls(
5.190 Rls{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
5.191 @@ -3577,17 +3557,15 @@
5.192 Rls {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
5.193 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
5.194 rules = [Calc ("Atools.is'_const",eval_const "#is_const_")
5.195 - ],
5.196 - scr = Script ((term_of o the o (parse thy))
5.197 - "empty_script")
5.198 - }:rls);
5.199 + ], scr = EmptyScr}:rls);
5.200 +
5.201 (*.consists of rls containing the absolute minimum of thms.*)
5.202 (*040209: this version has been used by RL for his equations,
5.203 which is now replaced by MGs version below
5.204 vvv OLD VERSION !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
5.205 val norm_Rational = prep_rls(
5.206 Rls {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
5.207 - erls = norm_rat_erls, srls = Erls, calc = [], (*asm_thm = [],*)
5.208 + erls = norm_rat_erls, srls = Erls, calc = [],
5.209 rules = [(*sequence given by operator precedence*)
5.210 Rls_ discard_minus,
5.211 Rls_ powers,
5.212 @@ -3600,23 +3578,17 @@
5.213 Rls_ add_fractions_p,
5.214 Rls_ cancel_p
5.215 ],
5.216 - scr = Script ((term_of o the o (parse thy))
5.217 - "empty_script")
5.218 - }:rls);
5.219 + scr = EmptyScr}:rls);
5.220 +
5.221 val norm_Rational_parenthesized = prep_rls(
5.222 Seq {id = "norm_Rational_parenthesized", preconds = []:term list,
5.223 rew_ord = ("dummy_ord", dummy_ord),
5.224 erls = Atools_erls, srls = Erls,
5.225 - calc = [], (*asm_thm = [],*)
5.226 + calc = [],
5.227 rules = [Rls_ norm_Rational, (*from RL -- not the latest one*)
5.228 Rls_ discard_parentheses
5.229 ],
5.230 - scr = EmptyScr
5.231 - }:rls);
5.232 -
5.233 -
5.234 -(*-------------------18.3.03 --> struct <-----------^^^--*)
5.235 -
5.236 + scr = EmptyScr}:rls);
5.237
5.238 (*WN030318???SK: simplifies all but cancel and common_nominator*)
5.239 val simplify_rational =
5.240 @@ -3687,6 +3659,7 @@
5.241 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
5.242 ],
5.243 scr = EmptyScr});
5.244 +
5.245 (* ------------------------------------------------------------------ *)
5.246 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
5.247 used in looping part norm_Rational_rls, see example DA-M02-main.p.60
5.248 @@ -3710,19 +3683,21 @@
5.249 Thm ("rat_mult_poly_r",num_str @{thm rat_mult_poly_r}),
5.250 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
5.251
5.252 - Thm ("real_divide_divide1_mg", real_divide_divide1_mg),
5.253 + Thm ("real_divide_divide1_mg",
5.254 + num_str @{thm real_divide_divide1_mg}),
5.255 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
5.256 - Thm ("divide_divide_eq_right", real_divide_divide1_eq),
5.257 + Thm ("divide_divide_eq_right",
5.258 + num_str @{thm divide_divide_eq_right}),
5.259 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
5.260 - Thm ("divide_divide_eq_left", real_divide_divide2_eq),
5.261 + Thm ("divide_divide_eq_left",
5.262 + num_str @{thm divide_divide_eq_left}),
5.263 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
5.264 Calc ("HOL.divide" ,eval_cancel "#divide_"),
5.265
5.266 Thm ("rat_power", num_str @{thm rat_power})
5.267 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
5.268 ],
5.269 - scr = Script ((term_of o the o (parse thy)) "empty_script")
5.270 - }:rls);
5.271 + scr = EmptyScr}:rls);
5.272 (* ------------------------------------------------------------------ *)
5.273 val rat_reduce_1 = prep_rls(
5.274 Rls {id = "rat_reduce_1", preconds = [],
5.275 @@ -3733,8 +3708,7 @@
5.276 Thm ("mult_1_left",num_str @{thm mult_1_left})
5.277 (*"1 * z = z"*)
5.278 ],
5.279 - scr = Script ((term_of o the o (parse thy)) "empty_script")
5.280 - }:rls);
5.281 + scr = EmptyScr}:rls);
5.282 (* ------------------------------------------------------------------ *)
5.283 (*. looping part of norm_Rational(*_mg*) .*)
5.284 val norm_Rational_rls = prep_rls(
5.285 @@ -3747,8 +3721,7 @@
5.286 Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
5.287 Rls_ rat_reduce_1
5.288 ],
5.289 - scr = Script ((term_of o the o (parse thy)) "empty_script")
5.290 - }:rls);
5.291 + scr = EmptyScr}:rls);
5.292 (* ------------------------------------------------------------------ *)
5.293 (*040109 'norm_Rational'(by RL) replaced by 'norm_Rational_mg'(MG)
5.294 just be renaming:*)
5.295 @@ -3756,18 +3729,16 @@
5.296 Seq {id = "norm_Rational"(*_mg*), preconds = [],
5.297 rew_ord = ("dummy_ord",dummy_ord),
5.298 erls = norm_rat_erls, srls = Erls, calc = [],
5.299 - rules = [Rls_ discard_minus_,
5.300 + rules = [Rls_ discard_minus1,
5.301 Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
5.302 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
5.303 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
5.304 Rls_ norm_Rational_rls, (* the main rls, looping (#) *)
5.305 - Rls_ discard_parentheses_ (* mult only *)
5.306 + Rls_ discard_parentheses1 (* mult only *)
5.307 ],
5.308 - scr = Script ((term_of o the o (parse thy)) "empty_script")
5.309 - }:rls);
5.310 + scr = EmptyScr}:rls);
5.311 (* ------------------------------------------------------------------ *)
5.312
5.313 -
5.314 ruleset' := overwritelthy @{theory} (!ruleset',
5.315 [("calculate_Rational", calculate_Rational),
5.316 ("calc_rat_erls",calc_rat_erls),
5.317 @@ -3801,24 +3772,25 @@
5.318 store_pbt
5.319 (prep_pbt thy "pbl_simp_rat" [] e_pblID
5.320 (["rational","simplification"],
5.321 - [("#Given" ,["TERM t_"]),
5.322 - ("#Where" ,["t_ is_ratpolyexp"]),
5.323 - ("#Find" ,["normalform n_"])
5.324 + [("#Given" ,["TERM t_t"]),
5.325 + ("#Where" ,["t_t is_ratpolyexp"]),
5.326 + ("#Find" ,["normalform n_n"])
5.327 ],
5.328 append_rls "e_rls" e_rls [(*for preds in where_*)],
5.329 - SOME "Simplify t_",
5.330 + SOME "Simplifyt_t",
5.331 [["simplification","of_rationals"]]));
5.332
5.333 (** methods **)
5.334 +val --------------------------------------------------+++++-+++++ = "00000";
5.335
5.336 (*WN061025 this methods script is copied from (auto-generated) script
5.337 of norm_Rational in order to ease repair on inform*)
5.338 store_met
5.339 (prep_met thy "met_simp_rat" [] e_metID
5.340 (["simplification","of_rationals"],
5.341 - [("#Given" ,["TERM t_"]),
5.342 - ("#Where" ,["t_ is_ratpolyexp"]),
5.343 - ("#Find" ,["normalform n_"])
5.344 + [("#Given" ,["TERM t_t"]),
5.345 + ("#Where" ,["t_t is_ratpolyexp"]),
5.346 + ("#Find" ,["normalform n_n"])
5.347 ],
5.348 {rew_ord'="tless_true",
5.349 rls' = e_rls,
5.350 @@ -3828,8 +3800,8 @@
5.351 Calc ("Rational.is'_ratpolyexp",
5.352 eval_is_ratpolyexp "")],
5.353 crls = e_rls, nrls = norm_Rational_rls},
5.354 -"Script SimplifyScript (t_::real) = " ^
5.355 -" ((Try (Rewrite_Set discard_minus_ False) @@ " ^
5.356 +"Script SimplifyScript (t_t::real) = " ^
5.357 +" ((Try (Rewrite_Set discard_minus1 False) @@ " ^
5.358 " Try (Rewrite_Set rat_mult_poly False) @@ " ^
5.359 " Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ " ^
5.360 " Try (Rewrite_Set cancel_p_rls False) @@ " ^
5.361 @@ -3839,9 +3811,10 @@
5.362 " Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^
5.363 " Try (Rewrite_Set cancel_p_rls False) @@ " ^
5.364 " Try (Rewrite_Set rat_reduce_1 False)))) @@ " ^
5.365 -" Try (Rewrite_Set discard_parentheses_ False)) " ^
5.366 -" t_)"
5.367 +" Try (Rewrite_Set discard_parentheses1 False)) " ^
5.368 +" t_t)"
5.369 ));
5.370 +
5.371 *}
5.372
5.373 end
6.1 --- a/test/Tools/isac/Knowledge/rational.sml Fri Sep 03 14:28:38 2010 +0200
6.2 +++ b/test/Tools/isac/Knowledge/rational.sml Fri Sep 03 17:19:20 2010 +0200
6.3 @@ -43,6 +43,7 @@
6.4 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
6.5 "-------- investigate rulesets for cancel_p ----------------------";
6.6 "-------- investigate format of factout_ and factout_p_ ----------";
6.7 +"-------- how to stepwise construct Scripts ----------------------";
6.8 "-----------------------------------------------------------------";
6.9 "-----------------------------------------------------------------";
6.10 "-----------------------------------------------------------------";
6.11 @@ -2020,4 +2021,114 @@
6.12 add_fraction_p_ thy t;
6.13 " ((a + b * x)*(a + b * x) + (-1 * a + b * x)*(a + -1 * (b * x))) /\
6.14 \ ((a + b * x)*(-1 * a + b * x)) ";
6.15 -*)
6.16 \ No newline at end of file
6.17 +*)
6.18 +
6.19 +
6.20 +"-------- how to stepwise construct Scripts ----------------------";
6.21 +"-------- how to stepwise construct Scripts ----------------------";
6.22 +"-------- how to stepwise construct Scripts ----------------------";
6.23 +lse raise error "rational.sml SK060904-1a worked since 0707xx";
6.24 +
6.25 +"----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
6.26 +val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
6.27 +\(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
6.28 +val SOME (t',_) = cancel_p_ thy t;
6.29 +if term2str t' = "1 / (4 * c + 3 * e)" then ()
6.30 +else raise error "rational.sml SK060904-1b";
6.31 +
6.32 +
6.33 +"----- SK060904-2a non-termination of add_fraction_p_";
6.34 +val t = str2term " (a + b * x) / (a + -1 * (b * x)) + \
6.35 + \ (-1 * a + b * x) / (a + b * x) ";
6.36 +(* nonterm.SK
6.37 +val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
6.38 +
6.39 +common_nominator_p_ thy t;
6.40 +" (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + \
6.41 +\ (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
6.42 +
6.43 +add_fraction_p_ thy t;
6.44 +" ((a + b * x)*(a + b * x) + (-1 * a + b * x)*(a + -1 * (b * x))) /\
6.45 +\ ((a + b * x)*(-1 * a + b * x)) ";
6.46 +*)
6.47 +
6.48 +
6.49 +"-------- how to stepwise construct Scripts ----------------------";
6.50 +"-------- how to stepwise construct Scripts ----------------------";
6.51 +"-------- how to stepwise construct Scripts ----------------------";
6.52 +lse raise error "rational.sml SK060904-1a worked since 0707xx";
6.53 +
6.54 +"----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
6.55 +val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
6.56 +\(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
6.57 +val SOME (t',_) = cancel_p_ thy t;
6.58 +if term2str t' = "1 / (4 * c + 3 * e)" then ()
6.59 +else raise error "rational.sml SK060904-1b";
6.60 +
6.61 +
6.62 +"----- SK060904-2a non-termination of add_fraction_p_";
6.63 +val t = str2term " (a + b * x) / (a + -1 * (b * x)) + \
6.64 + \ (-1 * a + b * x) / (a + b * x) ";
6.65 +(* nonterm.SK
6.66 +val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
6.67 +
6.68 +common_nominator_p_ thy t;
6.69 +" (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + \
6.70 +\ (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
6.71 +
6.72 +add_fraction_p_ thy t;
6.73 +" ((a + b * x)*(a + b * x) + (-1 * a + b * x)*(a + -1 * (b * x))) /\
6.74 +\ ((a + b * x)*(-1 * a + b * x)) ";
6.75 +*)
6.76 +
6.77 +
6.78 +"-------- how to stepwise construct Scripts ----------------------";
6.79 +"-------- how to stepwise construct Scripts ----------------------";
6.80 +"-------- how to stepwise construct Scripts ----------------------";
6.81 +val thy = (theory "Rational");
6.82 +val -------------------------------------------------- = "00000";
6.83 +(*no trailing _*)
6.84 +val p1 = parse thy (
6.85 +"Script SimplifyScript (t_t::real) = " ^
6.86 +" (Rewrite_Set discard_minus1 False " ^
6.87 +" t_t)");
6.88 +
6.89 +(*required (): (Rewrite_Set discard_minus False)*)
6.90 +val p2 = parse thy (
6.91 +"Script SimplifyScript (t_t::real) = " ^
6.92 +" (Rewrite_Set discard_minus False " ^
6.93 +" t_t)");
6.94 +
6.95 +val p3 = parse thy (
6.96 +"Script SimplifyScript (t_t::real) = " ^
6.97 +" ((Rewrite_Set discard_minus False) " ^
6.98 +" t_t)");
6.99 +
6.100 +val p4 = parse thy (
6.101 +"Script SimplifyScript (t_t::real) = " ^
6.102 +" ((Rewrite_Set discard_minus False) " ^
6.103 +" t_t)");
6.104 +
6.105 +val p5 = parse thy (
6.106 +"Script SimplifyScript (t_t::real) = " ^
6.107 +" ((Try (Rewrite_Set discard_minus False) " ^
6.108 +" Try (Rewrite_Set discard_parentheses False)) " ^
6.109 +" t_t)");
6.110 +
6.111 +val --------------------------------------------------+ = "11111";
6.112 +val p6 = parse thy (
6.113 +"Script SimplifyScript (t_t::real) = " ^
6.114 +" ((Try (Rewrite_Set discard_minus False) @@ " ^
6.115 +" Try (Rewrite_Set rat_mult_poly False) @@ " ^
6.116 +" Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ " ^
6.117 +" Try (Rewrite_Set cancel_p_rls False) @@ " ^
6.118 +" (Repeat " ^
6.119 +" ((Try (Rewrite_Set common_nominator_p_rls False) @@ " ^
6.120 +" Try (Rewrite_Set rat_mult_div_pow False) @@ " ^
6.121 +" Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^
6.122 +" Try (Rewrite_Set cancel_p_rls False) @@ " ^
6.123 +" Try (Rewrite_Set rat_reduce_1 False)))) @@ " ^
6.124 +" Try (Rewrite_Set discard_parentheses False)) " ^
6.125 +" t_t)"
6.126 +);
6.127 +val --------------------------------------------------++ = "22222";