equal
deleted
inserted
replaced
219 | opp_quant _ _ = false |
219 | opp_quant _ _ = false |
220 |
220 |
221 fun with_quant pred i (Const q1 $ Abs (_, T1, t1), Const q2 $ Abs (_, T2, t2)) = |
221 fun with_quant pred i (Const q1 $ Abs (_, T1, t1), Const q2 $ Abs (_, T2, t2)) = |
222 if pred q1 q2 andalso T1 = T2 then |
222 if pred q1 q2 andalso T1 = T2 then |
223 let val t = Var (("", i), T1) |
223 let val t = Var (("", i), T1) |
224 in SOME (pairself Term.subst_bound ((t, t1), (t, t2))) end |
224 in SOME (apply2 Term.subst_bound ((t, t1), (t, t2))) end |
225 else NONE |
225 else NONE |
226 | with_quant _ _ _ = NONE |
226 | with_quant _ _ _ = NONE |
227 |
227 |
228 fun dest_quant_pair i (@{term HOL.Not} $ t1, t2) = |
228 fun dest_quant_pair i (@{term HOL.Not} $ t1, t2) = |
229 Option.map (apfst HOLogic.mk_not) (with_quant opp_quant i (t1, t2)) |
229 Option.map (apfst HOLogic.mk_not) (with_quant opp_quant i (t1, t2)) |