227 val (q, j) = poly (rhs, Rat.one, ([], Rat.zero)) |
227 val (q, j) = poly (rhs, Rat.one, ([], Rat.zero)) |
228 in |
228 in |
229 case rel of |
229 case rel of |
230 @{const_name Orderings.less} => SOME (p, i, "<", q, j) |
230 @{const_name Orderings.less} => SOME (p, i, "<", q, j) |
231 | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j) |
231 | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j) |
232 | "op =" => SOME (p, i, "=", q, j) |
232 | @{const_name HOL.eq} => SOME (p, i, "=", q, j) |
233 | _ => NONE |
233 | _ => NONE |
234 end handle Rat.DIVZERO => NONE; |
234 end handle Rat.DIVZERO => NONE; |
235 |
235 |
236 fun of_lin_arith_sort thy U = |
236 fun of_lin_arith_sort thy U = |
237 Sign.of_sort thy (U, @{sort Rings.linordered_idom}); |
237 Sign.of_sort thy (U, @{sort Rings.linordered_idom}); |
425 (map (incr_boundvars 1) rev_terms) |
425 (map (incr_boundvars 1) rev_terms) |
426 val t1' = incr_boundvars 1 t1 |
426 val t1' = incr_boundvars 1 t1 |
427 val t2' = incr_boundvars 1 t2 |
427 val t2' = incr_boundvars 1 t2 |
428 val t1_lt_t2 = Const (@{const_name Orderings.less}, |
428 val t1_lt_t2 = Const (@{const_name Orderings.less}, |
429 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2 |
429 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2 |
430 val t1_eq_t2_plus_d = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $ |
430 val t1_eq_t2_plus_d = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $ |
431 (Const (@{const_name Groups.plus}, |
431 (Const (@{const_name Groups.plus}, |
432 split_type --> split_type --> split_type) $ t2' $ d) |
432 split_type --> split_type --> split_type) $ t2' $ d) |
433 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
433 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
434 val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false] |
434 val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false] |
435 val subgoal2 = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false] |
435 val subgoal2 = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false] |
445 val n = Bound 0 |
445 val n = Bound 0 |
446 val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)]) |
446 val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)]) |
447 (map (incr_boundvars 1) rev_terms) |
447 (map (incr_boundvars 1) rev_terms) |
448 val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms |
448 val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms |
449 val t1' = incr_boundvars 1 t1 |
449 val t1' = incr_boundvars 1 t1 |
450 val t1_eq_nat_n = Const (@{const_name "op ="}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $ |
450 val t1_eq_nat_n = Const (@{const_name HOL.eq}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $ |
451 (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n) |
451 (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n) |
452 val t1_lt_zero = Const (@{const_name Orderings.less}, |
452 val t1_lt_zero = Const (@{const_name Orderings.less}, |
453 HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int |
453 HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int |
454 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
454 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
455 val subgoal1 = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false] |
455 val subgoal1 = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false] |
469 val terms1 = map (subst_term [(split_term, t1)]) rev_terms |
469 val terms1 = map (subst_term [(split_term, t1)]) rev_terms |
470 val terms2 = map (subst_term [(incr_boundvars 2 split_term, j)]) |
470 val terms2 = map (subst_term [(incr_boundvars 2 split_term, j)]) |
471 (map (incr_boundvars 2) rev_terms) |
471 (map (incr_boundvars 2) rev_terms) |
472 val t1' = incr_boundvars 2 t1 |
472 val t1' = incr_boundvars 2 t1 |
473 val t2' = incr_boundvars 2 t2 |
473 val t2' = incr_boundvars 2 t2 |
474 val t2_eq_zero = Const (@{const_name "op ="}, |
474 val t2_eq_zero = Const (@{const_name HOL.eq}, |
475 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero |
475 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero |
476 val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="}, |
476 val t2_neq_zero = HOLogic.mk_not (Const (@{const_name HOL.eq}, |
477 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero) |
477 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero) |
478 val j_lt_t2 = Const (@{const_name Orderings.less}, |
478 val j_lt_t2 = Const (@{const_name Orderings.less}, |
479 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
479 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
480 val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $ |
480 val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $ |
481 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ |
481 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ |
482 (Const (@{const_name Groups.times}, |
482 (Const (@{const_name Groups.times}, |
483 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
483 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
484 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
484 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
485 val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] |
485 val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] |
501 val terms1 = map (subst_term [(split_term, zero)]) rev_terms |
501 val terms1 = map (subst_term [(split_term, zero)]) rev_terms |
502 val terms2 = map (subst_term [(incr_boundvars 2 split_term, i)]) |
502 val terms2 = map (subst_term [(incr_boundvars 2 split_term, i)]) |
503 (map (incr_boundvars 2) rev_terms) |
503 (map (incr_boundvars 2) rev_terms) |
504 val t1' = incr_boundvars 2 t1 |
504 val t1' = incr_boundvars 2 t1 |
505 val t2' = incr_boundvars 2 t2 |
505 val t2' = incr_boundvars 2 t2 |
506 val t2_eq_zero = Const (@{const_name "op ="}, |
506 val t2_eq_zero = Const (@{const_name HOL.eq}, |
507 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero |
507 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero |
508 val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="}, |
508 val t2_neq_zero = HOLogic.mk_not (Const (@{const_name HOL.eq}, |
509 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero) |
509 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero) |
510 val j_lt_t2 = Const (@{const_name Orderings.less}, |
510 val j_lt_t2 = Const (@{const_name Orderings.less}, |
511 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
511 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
512 val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $ |
512 val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $ |
513 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ |
513 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ |
514 (Const (@{const_name Groups.times}, |
514 (Const (@{const_name Groups.times}, |
515 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
515 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
516 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
516 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
517 val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] |
517 val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] |
539 val terms1 = map (subst_term [(split_term, t1)]) rev_terms |
539 val terms1 = map (subst_term [(split_term, t1)]) rev_terms |
540 val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, j)]) |
540 val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, j)]) |
541 (map (incr_boundvars 2) rev_terms) |
541 (map (incr_boundvars 2) rev_terms) |
542 val t1' = incr_boundvars 2 t1 |
542 val t1' = incr_boundvars 2 t1 |
543 val t2' = incr_boundvars 2 t2 |
543 val t2' = incr_boundvars 2 t2 |
544 val t2_eq_zero = Const (@{const_name "op ="}, |
544 val t2_eq_zero = Const (@{const_name HOL.eq}, |
545 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero |
545 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero |
546 val zero_lt_t2 = Const (@{const_name Orderings.less}, |
546 val zero_lt_t2 = Const (@{const_name Orderings.less}, |
547 split_type --> split_type --> HOLogic.boolT) $ zero $ t2' |
547 split_type --> split_type --> HOLogic.boolT) $ zero $ t2' |
548 val t2_lt_zero = Const (@{const_name Orderings.less}, |
548 val t2_lt_zero = Const (@{const_name Orderings.less}, |
549 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero |
549 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero |
553 split_type --> split_type --> HOLogic.boolT) $ j $ zero |
553 split_type --> split_type --> HOLogic.boolT) $ j $ zero |
554 val j_lt_t2 = Const (@{const_name Orderings.less}, |
554 val j_lt_t2 = Const (@{const_name Orderings.less}, |
555 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
555 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
556 val t2_lt_j = Const (@{const_name Orderings.less}, |
556 val t2_lt_j = Const (@{const_name Orderings.less}, |
557 split_type --> split_type--> HOLogic.boolT) $ t2' $ j |
557 split_type --> split_type--> HOLogic.boolT) $ t2' $ j |
558 val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $ |
558 val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $ |
559 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ |
559 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ |
560 (Const (@{const_name Groups.times}, |
560 (Const (@{const_name Groups.times}, |
561 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
561 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
562 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
562 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
563 val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] |
563 val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] |
593 val terms1 = map (subst_term [(split_term, zero)]) rev_terms |
593 val terms1 = map (subst_term [(split_term, zero)]) rev_terms |
594 val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, i)]) |
594 val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, i)]) |
595 (map (incr_boundvars 2) rev_terms) |
595 (map (incr_boundvars 2) rev_terms) |
596 val t1' = incr_boundvars 2 t1 |
596 val t1' = incr_boundvars 2 t1 |
597 val t2' = incr_boundvars 2 t2 |
597 val t2' = incr_boundvars 2 t2 |
598 val t2_eq_zero = Const (@{const_name "op ="}, |
598 val t2_eq_zero = Const (@{const_name HOL.eq}, |
599 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero |
599 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero |
600 val zero_lt_t2 = Const (@{const_name Orderings.less}, |
600 val zero_lt_t2 = Const (@{const_name Orderings.less}, |
601 split_type --> split_type --> HOLogic.boolT) $ zero $ t2' |
601 split_type --> split_type --> HOLogic.boolT) $ zero $ t2' |
602 val t2_lt_zero = Const (@{const_name Orderings.less}, |
602 val t2_lt_zero = Const (@{const_name Orderings.less}, |
603 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero |
603 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero |
607 split_type --> split_type --> HOLogic.boolT) $ j $ zero |
607 split_type --> split_type --> HOLogic.boolT) $ j $ zero |
608 val j_lt_t2 = Const (@{const_name Orderings.less}, |
608 val j_lt_t2 = Const (@{const_name Orderings.less}, |
609 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
609 split_type --> split_type--> HOLogic.boolT) $ j $ t2' |
610 val t2_lt_j = Const (@{const_name Orderings.less}, |
610 val t2_lt_j = Const (@{const_name Orderings.less}, |
611 split_type --> split_type--> HOLogic.boolT) $ t2' $ j |
611 split_type --> split_type--> HOLogic.boolT) $ t2' $ j |
612 val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $ |
612 val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $ |
613 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ |
613 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ |
614 (Const (@{const_name Groups.times}, |
614 (Const (@{const_name Groups.times}, |
615 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
615 split_type --> split_type --> split_type) $ t2' $ i) $ j) |
616 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
616 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) |
617 val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] |
617 val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] |