161 | LessD of injust |
161 | LessD of injust |
162 | NotLessD of injust |
162 | NotLessD of injust |
163 | NotLeD of injust |
163 | NotLeD of injust |
164 | NotLeDD of injust |
164 | NotLeDD of injust |
165 | Multiplied of int * injust |
165 | Multiplied of int * injust |
166 | Multiplied2 of int * injust |
|
167 | Added of injust * injust; |
166 | Added of injust * injust; |
168 |
167 |
169 datatype lineq = Lineq of int * lineq_type * int list * injust; |
168 datatype lineq = Lineq of int * lineq_type * int list * injust; |
170 |
169 |
171 (* ------------------------------------------------------------------------- *) |
170 (* ------------------------------------------------------------------------- *) |
521 | mk (NotLeD j) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) |
520 | mk (NotLeD j) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) |
522 | mk (NotLeDD j) = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD)) |
521 | mk (NotLeDD j) = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD)) |
523 | mk (NotLessD j) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) |
522 | mk (NotLessD j) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) |
524 | mk (Added (j1, j2)) = simp (trace_thm "+" (add_thms (mk j1) (mk j2))) |
523 | mk (Added (j1, j2)) = simp (trace_thm "+" (add_thms (mk j1) (mk j2))) |
525 | mk (Multiplied (n, j)) = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (mult_thm (n, mk j))) |
524 | mk (Multiplied (n, j)) = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (mult_thm (n, mk j))) |
526 | mk (Multiplied2 (n, j)) = (trace_msg ("**" ^ string_of_int n); trace_thm "**" (mult_thm (n, mk j))) |
|
527 |
525 |
528 in |
526 in |
529 let |
527 let |
530 val _ = trace_msg "mkthm"; |
528 val _ = trace_msg "mkthm"; |
531 val thm = trace_thm "Final thm:" (mk just); |
529 val thm = trace_thm "Final thm:" (mk just); |
568 val lhsa = map (coeff lhs) atoms |
566 val lhsa = map (coeff lhs) atoms |
569 and rhsa = map (coeff rhs) atoms |
567 and rhsa = map (coeff rhs) atoms |
570 val diff = map2 (curry (op -)) rhsa lhsa |
568 val diff = map2 (curry (op -)) rhsa lhsa |
571 val c = i-j |
569 val c = i-j |
572 val just = Asm k |
570 val just = Asm k |
573 fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j)) |
571 fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied(m,j)) |
574 in case rel of |
572 in case rel of |
575 "<=" => lineq(c,Le,diff,just) |
573 "<=" => lineq(c,Le,diff,just) |
576 | "~<=" => if discrete |
574 | "~<=" => if discrete |
577 then lineq(1-c,Le,map (op ~) diff,NotLeDD(just)) |
575 then lineq(1-c,Le,map (op ~) diff,NotLeDD(just)) |
578 else lineq(~c,Lt,map (op ~) diff,NotLeD(just)) |
576 else lineq(~c,Lt,map (op ~) diff,NotLeD(just)) |