122 |
122 |
123 ("False", bT), |
123 ("False", bT), |
124 ("True", bT)]; |
124 ("True", bT)]; |
125 |
125 |
126 (*returns true if the formula is relevant for presburger arithmetic tactic*) |
126 (*returns true if the formula is relevant for presburger arithmetic tactic*) |
127 fun relevant t = (term_typed_consts t) subset allowed_consts; |
127 fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso |
|
128 map (fn i => snd (nth_elem (i, ps))) (loose_bnos t) @ |
|
129 map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t) |
|
130 subset [iT, nT]; |
128 |
131 |
129 (* Preparation of the formula to be sent to the Integer quantifier *) |
132 (* Preparation of the formula to be sent to the Integer quantifier *) |
130 (* elimination procedure *) |
133 (* elimination procedure *) |
131 (* Transforms meta implications and meta quantifiers to object *) |
134 (* Transforms meta implications and meta quantifiers to object *) |
132 (* implications and object quantifiers *) |
135 (* implications and object quantifiers *) |
134 fun prepare_for_presburger q fm = |
137 fun prepare_for_presburger q fm = |
135 let |
138 let |
136 val ps = Logic.strip_params fm |
139 val ps = Logic.strip_params fm |
137 val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) |
140 val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) |
138 val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) |
141 val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) |
139 val _ = if relevant c then () else raise CooperDec.COOPER |
142 val _ = if relevant (rev ps) c then () else raise CooperDec.COOPER |
140 fun mk_all ((s, T), (P,n)) = |
143 fun mk_all ((s, T), (P,n)) = |
141 if 0 mem loose_bnos P then |
144 if 0 mem loose_bnos P then |
142 (HOLogic.all_const T $ Abs (s, T, P), n) |
145 (HOLogic.all_const T $ Abs (s, T, P), n) |
143 else (incr_boundvars ~1 P, n-1) |
146 else (incr_boundvars ~1 P, n-1) |
144 fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; |
147 fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; |
145 val (rhs,irhs) = partition relevant hs |
148 val (rhs,irhs) = partition (relevant (rev ps)) hs |
146 val np = length ps |
149 val np = length ps |
147 val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) |
150 val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) |
148 (ps,(foldr HOLogic.mk_imp (rhs, c), np)) |
151 (ps,(foldr HOLogic.mk_imp (rhs, c), np)) |
149 val (vs, _) = partition (fn t => q orelse (type_of t) = nT) |
152 val (vs, _) = partition (fn t => q orelse (type_of t) = nT) |
150 (term_frees fm' @ term_vars fm'); |
153 (term_frees fm' @ term_vars fm'); |
156 |
159 |
157 (* object implication to meta---*) |
160 (* object implication to meta---*) |
158 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; |
161 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; |
159 |
162 |
160 (* the presburger tactic*) |
163 (* the presburger tactic*) |
161 fun presburger_tac q i st = |
164 fun presburger_tac q i = ObjectLogic.atomize_tac i THEN (fn st => |
162 let |
165 let |
163 val g = BasisLibrary.List.nth (prems_of st, i - 1); |
166 val g = BasisLibrary.List.nth (prems_of st, i - 1); |
164 val sg = sign_of_thm st; |
167 val sg = sign_of_thm st; |
165 (* Transform the term*) |
168 (* Transform the term*) |
166 val (t,np,nh) = prepare_for_presburger q g |
169 val (t,np,nh) = prepare_for_presburger q g |
201 Sign.string_of_term sg t1); |
204 Sign.string_of_term sg t1); |
202 ((mproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm, |
205 ((mproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm, |
203 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |
206 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |
204 | _ => (pre_thm, assm_tac i) |
207 | _ => (pre_thm, assm_tac i) |
205 in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st |
208 in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st |
206 end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st; |
209 end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st); |
207 |
210 |
208 fun presburger_args meth = |
211 fun presburger_args meth = |
209 Method.simple_args (Scan.optional (Args.$$$ "no_quantify" >> K false) true) |
212 Method.simple_args (Scan.optional (Args.$$$ "no_quantify" >> K false) true) |
210 (fn q => fn _ => meth q 1); |
213 (fn q => fn _ => meth q 1); |
211 |
214 |