equal
deleted
inserted
replaced
69 | _ => fold (add_binders thy i) ts bs) |
69 | _ => fold (add_binders thy i) ts bs) |
70 | (u, ts) => add_binders thy i u (fold (add_binders thy i) ts bs)) |
70 | (u, ts) => add_binders thy i u (fold (add_binders thy i) ts bs)) |
71 | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs |
71 | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs |
72 | add_binders thy i _ bs = bs; |
72 | add_binders thy i _ bs = bs; |
73 |
73 |
74 fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of |
74 fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of |
75 Const (name, _) => |
75 Const (name, _) => |
76 if member (op =) names name then SOME (f p q) else NONE |
76 if member (op =) names name then SOME (f p q) else NONE |
77 | _ => NONE) |
77 | _ => NONE) |
78 | split_conj _ _ _ _ = NONE; |
78 | split_conj _ _ _ _ = NONE; |
79 |
79 |
87 (* or id (ALL z. P z (pi_1 o ... o pi_n o t)) *) |
87 (* or id (ALL z. P z (pi_1 o ... o pi_n o t)) *) |
88 (* *) |
88 (* *) |
89 (* where "id" protects the subformula from simplification *) |
89 (* where "id" protects the subformula from simplification *) |
90 (*********************************************************************) |
90 (*********************************************************************) |
91 |
91 |
92 fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ = |
92 fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ = |
93 (case head_of p of |
93 (case head_of p of |
94 Const (name, _) => |
94 Const (name, _) => |
95 if member (op =) names name then SOME (HOLogic.mk_conj (p, |
95 if member (op =) names name then SOME (HOLogic.mk_conj (p, |
96 Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $ |
96 Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $ |
97 (subst_bounds (pis, strip_all pis q)))) |
97 (subst_bounds (pis, strip_all pis q)))) |