129 ("op |", bT --> bT --> bT), |
129 ("op |", bT --> bT --> bT), |
130 ("op -->", bT --> bT --> bT), |
130 ("op -->", bT --> bT --> bT), |
131 ("op =", bT --> bT --> bT), |
131 ("op =", bT --> bT --> bT), |
132 ("Not", bT --> bT), |
132 ("Not", bT --> bT), |
133 |
133 |
134 ("Orderings.less_eq", iT --> iT --> bT), |
134 (@{const_name Orderings.less_eq}, iT --> iT --> bT), |
135 ("op =", iT --> iT --> bT), |
135 ("op =", iT --> iT --> bT), |
136 ("Orderings.less", iT --> iT --> bT), |
136 (@{const_name Orderings.less}, iT --> iT --> bT), |
137 ("Divides.dvd", iT --> iT --> bT), |
137 (@{const_name Divides.dvd}, iT --> iT --> bT), |
138 ("Divides.div", iT --> iT --> iT), |
138 (@{const_name Divides.div}, iT --> iT --> iT), |
139 ("Divides.mod", iT --> iT --> iT), |
139 (@{const_name Divides.mod}, iT --> iT --> iT), |
140 ("HOL.plus", iT --> iT --> iT), |
140 (@{const_name HOL.plus}, iT --> iT --> iT), |
141 ("HOL.minus", iT --> iT --> iT), |
141 (@{const_name HOL.minus}, iT --> iT --> iT), |
142 ("HOL.times", iT --> iT --> iT), |
142 (@{const_name HOL.times}, iT --> iT --> iT), |
143 ("HOL.abs", iT --> iT), |
143 (@{const_name HOL.abs}, iT --> iT), |
144 ("HOL.uminus", iT --> iT), |
144 (@{const_name HOL.uminus}, iT --> iT), |
145 ("HOL.max", iT --> iT --> iT), |
145 (@{const_name Orderings.max}, iT --> iT --> iT), |
146 ("HOL.min", iT --> iT --> iT), |
146 (@{const_name Orderings.min}, iT --> iT --> iT), |
147 |
147 |
148 ("Orderings.less_eq", nT --> nT --> bT), |
148 (@{const_name Orderings.less_eq}, nT --> nT --> bT), |
149 ("op =", nT --> nT --> bT), |
149 ("op =", nT --> nT --> bT), |
150 ("Orderings.less", nT --> nT --> bT), |
150 (@{const_name Orderings.less}, nT --> nT --> bT), |
151 ("Divides.dvd", nT --> nT --> bT), |
151 (@{const_name Divides.dvd}, nT --> nT --> bT), |
152 ("Divides.div", nT --> nT --> nT), |
152 (@{const_name Divides.div}, nT --> nT --> nT), |
153 ("Divides.mod", nT --> nT --> nT), |
153 (@{const_name Divides.mod}, nT --> nT --> nT), |
154 ("HOL.plus", nT --> nT --> nT), |
154 (@{const_name HOL.plus}, nT --> nT --> nT), |
155 ("HOL.minus", nT --> nT --> nT), |
155 (@{const_name HOL.minus}, nT --> nT --> nT), |
156 ("HOL.times", nT --> nT --> nT), |
156 (@{const_name HOL.times}, nT --> nT --> nT), |
157 ("Suc", nT --> nT), |
157 (@{const_name Suc}, nT --> nT), |
158 ("HOL.max", nT --> nT --> nT), |
158 (@{const_name Orderings.max}, nT --> nT --> nT), |
159 ("HOL.min", nT --> nT --> nT), |
159 (@{const_name Orderings.min}, nT --> nT --> nT), |
160 |
160 |
161 ("Numeral.bit.B0", bitT), |
161 (@{const_name Numeral.bit.B0}, bitT), |
162 ("Numeral.bit.B1", bitT), |
162 (@{const_name Numeral.bit.B1}, bitT), |
163 ("Numeral.Bit", iT --> bitT --> iT), |
163 (@{const_name Numeral.Bit}, iT --> bitT --> iT), |
164 ("Numeral.Pls", iT), |
164 (@{const_name Numeral.Pls}, iT), |
165 ("Numeral.Min", iT), |
165 (@{const_name Numeral.Min}, iT), |
166 ("Numeral.number_of", iT --> iT), |
166 (@{const_name Numeral.number_of}, iT --> iT), |
167 ("Numeral.number_of", iT --> nT), |
167 (@{const_name Numeral.number_of}, iT --> nT), |
168 ("HOL.zero", nT), |
168 (@{const_name HOL.zero}, nT), |
169 ("HOL.zero", iT), |
169 (@{const_name HOL.zero}, iT), |
170 ("HOL.one", nT), |
170 (@{const_name HOL.one}, nT), |
171 ("HOL.one", iT), |
171 (@{const_name HOL.one}, iT), |
172 ("False", bT), |
172 (@{const_name False}, bT), |
173 ("True", bT)]; |
173 (@{const_name True}, bT)]; |
174 |
174 |
175 (* Preparation of the formula to be sent to the Integer quantifier *) |
175 (* Preparation of the formula to be sent to the Integer quantifier *) |
176 (* elimination procedure *) |
176 (* elimination procedure *) |
177 (* Transforms meta implications and meta quantifiers to object *) |
177 (* Transforms meta implications and meta quantifiers to object *) |
178 (* implications and object quantifiers *) |
178 (* implications and object quantifiers *) |