1345 |
1345 |
1346 val order_mult_ = |
1346 val order_mult_ = |
1347 Rrls {id = "order_mult_", |
1347 Rrls {id = "order_mult_", |
1348 prepat = |
1348 prepat = |
1349 (* ?p matched with the current term gives an environment, |
1349 (* ?p matched with the current term gives an environment, |
1350 which evaluates (the instantiated) "p is_multUnordered" to true*) |
1350 which evaluates (the instantiated) "?p is_multUnordered" to true *) |
1351 [([(term_of o the o (parse thy)) "p is_multUnordered"], |
1351 [([parse_patt thy "?p is_multUnordered"], |
1352 parse_patt thy "?p :: real" )], |
1352 parse_patt thy "?p :: real")], |
1353 rew_ord = ("dummy_ord", dummy_ord), |
1353 rew_ord = ("dummy_ord", dummy_ord), |
1354 erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*) |
1354 erls = append_rls "e_rls-is_multUnordered" e_rls |
1355 [Calc ("Poly.is'_multUnordered", |
1355 [Calc ("Poly.is'_multUnordered", |
1356 eval_is_multUnordered "")], |
1356 eval_is_multUnordered "")], |
1357 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1357 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1358 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
1358 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
1359 ("DIVIDE", ("Rings.inverse_class.divide", |
1359 ("DIVIDE", ("Rings.inverse_class.divide", |
1397 |
1397 |
1398 val order_add_ = |
1398 val order_add_ = |
1399 Rrls {id = "order_add_", |
1399 Rrls {id = "order_add_", |
1400 prepat = (*WN.18.6.03 Preconditions und Pattern, |
1400 prepat = (*WN.18.6.03 Preconditions und Pattern, |
1401 die beide passen muessen, damit das Rrls angewandt wird*) |
1401 die beide passen muessen, damit das Rrls angewandt wird*) |
1402 [([(term_of o the o (parse thy)) "p is_addUnordered"], |
1402 [([parse_patt @{theory} "?p is_addUnordered"], |
1403 parse_patt thy "?p" |
1403 parse_patt @{theory} "?p :: real" |
1404 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment |
1404 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment |
1405 fuer die Evaluation der Precondition "p is_addUnordered"*))], |
1405 fuer die Evaluation der Precondition "p is_addUnordered"*))], |
1406 rew_ord = ("dummy_ord", dummy_ord), |
1406 rew_ord = ("dummy_ord", dummy_ord), |
1407 erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*) |
1407 erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*) |
1408 [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "") |
1408 [Calc ("Poly.is'_addUnordered", |
1409 (*WN.18.6.03 definiert in thy, |
1409 eval_is_addUnordered "")], |
1410 evaluiert prepat*)], |
1410 calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")), |
1411 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), |
1411 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")), |
1412 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), |
1412 ("DIVIDE",("Rings.inverse_class.divide", |
1413 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), |
1413 eval_cancel "#divide_e")), |
1414 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], |
1414 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], |
1415 (*asm_thm=[],*) |
1415 (*asm_thm=[],*) |
1416 scr=Rfuns {init_state = init_state, |
1416 scr=Rfuns {init_state = init_state, |
1417 normal_form = normal_form, |
1417 normal_form = normal_form, |
1418 locate_rule = locate_rule, |
1418 locate_rule = locate_rule, |
1419 next_rule = next_rule, |
1419 next_rule = next_rule, |