468 is_polyexp t andalso not (t = sort_variables t); |
468 is_polyexp t andalso not (t = sort_variables t); |
469 if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1"; |
469 if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1"; |
470 |
470 |
471 "----- eval_is_multUnordered ---"; |
471 "----- eval_is_multUnordered ---"; |
472 val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) + (-48 * x \<up> 4 + 8))) is_multUnordered"; |
472 val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) + (-48 * x \<up> 4 + 8))) is_multUnordered"; |
473 case eval_is_multUnordered "testid" "" tm thy of |
473 case eval_is_multUnordered "testid" "" tm @{context} of |
474 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ |
474 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ |
475 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ |
475 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ |
476 (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ |
476 (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ |
477 Const (\<^const_name>\<open>True\<close>, _))) => () |
477 Const (\<^const_name>\<open>True\<close>, _))) => () |
478 | _ => error "poly.sml diff. eval_is_multUnordered"; |
478 | _ => error "poly.sml diff. eval_is_multUnordered"; |
490 |
490 |
491 (*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true |
491 (*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true |
492 (*+*) andalso not (is_multUnordered arg) |
492 (*+*) andalso not (is_multUnordered arg) |
493 (*+*)then () else error "sort_variables 3 * a + - 2 * a CHANGED"; |
493 (*+*)then () else error "sort_variables 3 * a + - 2 * a CHANGED"; |
494 |
494 |
495 case eval_is_multUnordered "xxx " "yyy " t thy of |
495 case eval_is_multUnordered "xxx " "yyy " t @{context} of |
496 SOME |
496 SOME |
497 ("xxx 3 * a + - 2 * a_", |
497 ("xxx 3 * a + - 2 * a_", |
498 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ |
498 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ |
499 Const (\<^const_name>\<open>False\<close>, _))) => () |
499 Const (\<^const_name>\<open>False\<close>, _))) => () |
500 (* Const (\<^const_name>\<open>True\<close>, _))) => () <<<<<--------------------------- this is false*) |
500 (* Const (\<^const_name>\<open>True\<close>, _))) => () <<<<<--------------------------- this is false*) |
505 |
505 |
506 (*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true |
506 (*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true |
507 (*+*) andalso not (is_multUnordered arg) |
507 (*+*) andalso not (is_multUnordered arg) |
508 (*+*)then () else error "sort_variables - 2 * a CHANGED"; |
508 (*+*)then () else error "sort_variables - 2 * a CHANGED"; |
509 |
509 |
510 case eval_is_multUnordered "xxx " "yyy " t thy of |
510 case eval_is_multUnordered "xxx " "yyy " t @{context} of |
511 SOME |
511 SOME |
512 ("xxx - 2 * a_", |
512 ("xxx - 2 * a_", |
513 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ |
513 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ |
514 Const (\<^const_name>\<open>False\<close>, _))) => () |
514 Const (\<^const_name>\<open>False\<close>, _))) => () |
515 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED"; |
515 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED"; |
519 |
519 |
520 (*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true |
520 (*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true |
521 (*+*) andalso not (is_multUnordered arg) |
521 (*+*) andalso not (is_multUnordered arg) |
522 (*+*)then () else error "sort_variables a CHANGED"; |
522 (*+*)then () else error "sort_variables a CHANGED"; |
523 |
523 |
524 case eval_is_multUnordered "xxx " "yyy " t thy of |
524 case eval_is_multUnordered "xxx " "yyy " t @{context} of |
525 SOME |
525 SOME |
526 ("xxx a_", |
526 ("xxx a_", |
527 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ |
527 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ |
528 Const (\<^const_name>\<open>False\<close>, _))) => () |
528 Const (\<^const_name>\<open>False\<close>, _))) => () |
529 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED"; |
529 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED"; |
533 |
533 |
534 (*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true |
534 (*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true |
535 (*+*) andalso not (is_multUnordered arg) |
535 (*+*) andalso not (is_multUnordered arg) |
536 (*+*)then () else error "sort_variables - 2 CHANGED"; |
536 (*+*)then () else error "sort_variables - 2 CHANGED"; |
537 |
537 |
538 case eval_is_multUnordered "xxx " "yyy " t thy of |
538 case eval_is_multUnordered "xxx " "yyy " t @{context} of |
539 SOME |
539 SOME |
540 ("xxx - 2_", |
540 ("xxx - 2_", |
541 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ |
541 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ |
542 Const (\<^const_name>\<open>False\<close>, _))) => () |
542 Const (\<^const_name>\<open>False\<close>, _))) => () |
543 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED"; |
543 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED"; |
674 False (*isa2*) |
674 False (*isa2*) |
675 *) |
675 *) |
676 val t = TermC.str2term "(6 * a) is_multUnordered"; |
676 val t = TermC.str2term "(6 * a) is_multUnordered"; |
677 val SOME |
677 val SOME |
678 (_, t') = |
678 (_, t') = |
679 eval_is_multUnordered "xxx" () t @{theory}; |
679 eval_is_multUnordered "xxx" () t @{context}; |
680 (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then () |
680 (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then () |
681 (*+*)else error "6 * a is_multUnordered = False CHANGED"; |
681 (*+*)else error "6 * a is_multUnordered = False CHANGED"; |
682 |
682 |
683 "~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _, |
683 "~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _, |
684 (t as (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ arg)), thy) = ("xxx", (), t, @{theory}); |
684 (t as (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ arg)), thy) = ("xxx", (), t, @{theory}); |