227 | incr_tvar k T = incrT k T handle SAME => T; |
227 | incr_tvar k T = incrT k T handle SAME => T; |
228 |
228 |
229 end; |
229 end; |
230 |
230 |
231 |
231 |
232 (*Make lifting functions from subgoal and increment. |
232 (* Lifting functions from subgoal and increment: |
233 lift_abs operates on terms |
233 lift_abs operates on terms |
234 lift_all operates on propositions *) |
234 lift_all operates on propositions *) |
235 |
235 |
236 fun lift_abs inc = |
236 fun lift_abs inc = |
237 let |
237 let |
238 fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t |
238 fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t |
239 | lift Ts (Const ("all", _) $ Abs (a, T, b)) t = Abs (a, T, lift (T :: Ts) b t) |
239 | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t) |
240 | lift Ts _ t = incr_indexes (rev Ts, inc) t; |
240 | lift Ts _ t = incr_indexes (rev Ts, inc) t; |
241 in lift [] end; |
241 in lift [] end; |
242 |
242 |
243 fun lift_all inc = |
243 fun lift_all inc = |
244 let |
244 let |
245 fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t |
245 fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t |
246 | lift Ts ((c as Const ("all", _)) $ Abs (a, T, b)) t = c $ Abs (a, T, lift (T :: Ts) b t) |
246 | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t) |
247 | lift Ts _ t = incr_indexes (rev Ts, inc) t; |
247 | lift Ts _ t = incr_indexes (rev Ts, inc) t; |
248 in lift [] end; |
248 in lift [] end; |
249 |
249 |
250 (*Strips assumptions in goal, yielding list of hypotheses. *) |
250 (*Strips assumptions in goal, yielding list of hypotheses. *) |
251 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B |
251 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B |