164 remark: polynomial2expanded o expanded2polynomial = I, |
164 remark: polynomial2expanded o expanded2polynomial = I, |
165 where 'o' is function chaining, and 'I' is identity WN0210???SK |
165 where 'o' is function chaining, and 'I' is identity WN0210???SK |
166 |
166 |
167 functions for greatest common divisor and canceling |
167 functions for greatest common divisor and canceling |
168 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
168 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
169 ################################################################################ |
|
170 ## search Isabelle2009-2/src/HOL/Multivariate_Analysis |
|
171 ## Amine Chaieb, Robert Himmelmann, John Harrison. |
|
172 ################################################################################ |
169 mv_gcd |
173 mv_gcd |
170 factout_ |
174 factout_ |
171 factout_p_ |
175 factout_p_ |
172 cancel_ |
176 cancel_ |
173 cancel_p_ |
177 cancel_p_ |
3068 error ("next_rule: doesnt match rev-sets in istate"); |
3072 error ("next_rule: doesnt match rev-sets in istate"); |
3069 |
3073 |
3070 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
3074 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
3071 []:(rule * (term * term list)) list; |
3075 []:(rule * (term * term list)) list; |
3072 |
3076 |
|
3077 (* pat matched with the current term gives an environment |
|
3078 (or not: hen the Rrls not applied); |
|
3079 if pre1 and pre2 evaluate to HOLogic.true_const in this environment, |
|
3080 then the Rrls is applied. *) |
3073 val pat = parse_patt thy "?r/?s"; |
3081 val pat = parse_patt thy "?r/?s"; |
3074 val pre1 = parse_patt thy "?r is_expanded"; |
3082 val pre1 = parse_patt thy "?r is_expanded"; |
3075 val pre2 = parse_patt thy "?s is_expanded"; |
3083 val pre2 = parse_patt thy "?s is_expanded"; |
3076 val prepat = [([pre1, pre2], pat)]; |
3084 val prepat = [([pre1, pre2], pat)]; |
3077 |
3085 |
3216 the list is empty, if the users term does not belong |
3224 the list is empty, if the users term does not belong |
3217 to a cancellation of the term last agreed upon.*) |
3225 to a cancellation of the term last agreed upon.*) |
3218 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
3226 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
3219 []:(rule * (term * term list)) list; |
3227 []:(rule * (term * term list)) list; |
3220 |
3228 |
|
3229 (* if each pat* matches with the current term, the Rrls is applied |
|
3230 (there are no preconditions to be checked, they are HOLogic.true_const) *) |
3221 val pat0 = parse_patt thy "?r/?s+?u/?v"; |
3231 val pat0 = parse_patt thy "?r/?s+?u/?v"; |
3222 val pat1 = parse_patt thy "?r/?s+?u "; |
3232 val pat1 = parse_patt thy "?r/?s+?u "; |
3223 val pat2 = parse_patt thy "?r +?u/?v"; |
3233 val pat2 = parse_patt thy "?r +?u/?v"; |
3224 val prepat = [([HOLogic.true_const], pat0), |
3234 val prepat = [([HOLogic.true_const], pat0), |
3225 ([HOLogic.true_const], pat1), |
3235 ([HOLogic.true_const], pat1), |
3226 ([HOLogic.true_const], pat2)]; |
3236 ([HOLogic.true_const], pat2)]; |
3227 |
|
3228 in |
3237 in |
3229 |
3238 |
3230 (*11.02 schnelle L"osung f"ur RL: Bruch auch gek"urzt; |
3239 (*11.02 schnelle L"osung f"ur RL: Bruch auch gek"urzt; |
3231 besser w"are: auf 1 gemeinsamen Bruchstrich, Nenner und Z"ahler unvereinfacht |
3240 besser w"are: auf 1 gemeinsamen Bruchstrich, Nenner und Z"ahler unvereinfacht |
3232 dh. wie common_nominator_p_, aber auf 1 Bruchstrich*) |
3241 dh. wie common_nominator_p_, aber auf 1 Bruchstrich*) |
3360 the list is empty, if the users term does not belong |
3369 the list is empty, if the users term does not belong |
3361 to a cancellation of the term last agreed upon.*) |
3370 to a cancellation of the term last agreed upon.*) |
3362 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
3371 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
3363 []:(rule * (term * term list)) list; |
3372 []:(rule * (term * term list)) list; |
3364 |
3373 |
|
3374 (* if each pat* matches with the current term, the Rrls is applied |
|
3375 (there are no preconditions to be checked, they are HOLogic.true_const) *) |
3365 val pat0 = parse_patt thy "?r/?s+?u/?v"; |
3376 val pat0 = parse_patt thy "?r/?s+?u/?v"; |
3366 val pat01 = parse_patt thy "?r/?s-?u/?v"; |
3377 val pat01 = parse_patt thy "?r/?s-?u/?v"; |
3367 val pat1 = parse_patt thy "?r/?s+?u "; |
3378 val pat1 = parse_patt thy "?r/?s+?u "; |
3368 val pat11 = parse_patt thy "?r/?s-?u "; |
3379 val pat11 = parse_patt thy "?r/?s-?u "; |
3369 val pat2 = parse_patt thy "?r +?u/?v"; |
3380 val pat2 = parse_patt thy "?r +?u/?v"; |