72 | _ => false; |
72 | _ => false; |
73 |
73 |
74 (*Function is_arith_rel returns true if and only if the term is an operation of the |
74 (*Function is_arith_rel returns true if and only if the term is an operation of the |
75 form [int,int]---> int*) |
75 form [int,int]---> int*) |
76 |
76 |
77 (*Transform a natural number to a term*) |
77 (*Transform a natural (FIXME?) number to a term*) |
78 |
78 val mk_number = HOLogic.mk_number HOLogic.intT |
79 fun mk_number 0 = Const("HOL.zero",HOLogic.intT) |
79 |
80 |mk_number 1 = Const("HOL.one",HOLogic.intT) |
80 (*Transform an Term to an natural (FIXME?) number*) |
81 |mk_number n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_numeral n); |
81 fun dest_number t = let |
82 |
82 val (T, n) = HOLogic.dest_number t |
83 (*Transform an Term to an natural number*) |
83 in if T = HOLogic.intT then n else error ("bad typ: " ^ Display.raw_string_of_typ T) end; |
84 |
84 |
85 fun dest_number (Const("HOL.zero",Type ("IntDef.int", []))) = 0 |
|
86 |dest_number (Const("HOL.one",Type ("IntDef.int", []))) = 1 |
|
87 |dest_number (Const ("Numeral.number_of",_) $ n) = |
|
88 HOLogic.dest_numeral n; |
|
89 (*Some terms often used for pattern matching*) |
85 (*Some terms often used for pattern matching*) |
90 |
|
91 val zero = mk_number 0; |
86 val zero = mk_number 0; |
92 val one = mk_number 1; |
87 val one = mk_number 1; |
93 |
88 |
94 (*Tests if a Term is representing a number*) |
89 (*Tests if a Term is representing a number*) |
95 |
90 val is_numeral = can dest_number; |
96 fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_number t); |
91 |
97 |
|
98 (*maps a unary natural function on a term containing an natural number*) |
92 (*maps a unary natural function on a term containing an natural number*) |
99 |
93 fun numeral1 f n = mk_number (f (dest_number n)); |
100 fun numeral1 f n = mk_number (f(dest_number n)); |
|
101 |
94 |
102 (*maps a binary natural function on 2 term containing natural numbers*) |
95 (*maps a binary natural function on 2 term containing natural numbers*) |
103 |
96 fun numeral2 f m n = mk_number (f (dest_number m) (dest_number n)); |
104 fun numeral2 f m n = mk_number(f(dest_number m) (dest_number n)); |
|
105 |
97 |
106 (* ------------------------------------------------------------------------- *) |
98 (* ------------------------------------------------------------------------- *) |
107 (* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k *) |
99 (* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k *) |
108 (* *) |
100 (* *) |
109 (* Note that we're quite strict: the ci must be present even if 1 *) |
101 (* Note that we're quite strict: the ci must be present even if 1 *) |