-
Andrei Paskevich authored
Prevent introduce_premises from splitting too aggressively on the left-hand side: - under quantifiers: "forall x. P /\ Q" =/=> "(forall x. P) /\ (forall x. Q)" - match-with: "match t with A -> P | B -> Q" =/=> "(t = A -> P) /\ (t = B -> Q)" - if-then-else: "if f then P else Q" =/=> "(f -> P) /\ (not f -> Q)" - equivalence: "P <-> Q" =/=> "(P -> Q) /\ (Q -> P)" Those splits duplicate formulas, hinder readability and do not really simplify anything. Moreover, in case of a split under a quantifier, they create several universal premises for provers to instantiate, instead of just one. TODO: introduce_premises should be able to split under a single-branch match. However, this requires special treatment in Introduce.dequant, since the pattern should be rather skolemized than used as a condition.
8b809621