Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Do these tactics exist?


view this post on Zulip Email Gateway (Aug 19 2022 at 15:21):

From: Holden Lee <hl422@cam.ac.uk>
A lot of proofs I have to do are methodical, but to my knowledge can't
be done by auto, because auto doesn't have the right control structure.
Here are some tactics/controls which would be useful to me if they could
work with auto - I'd be interested to know whether they exist, and if not,
could someone point me to how I could code them in?

- "auto subst!: A" where "A is P x ==> f(x)=g(x)" Run auto, but every
time you see f(x), replace it by g(x) and add the subgoal P x.

- "conditional substitution" - Same as above but under conditions. Given
a rule "P x ==> f(x)=g(x)" and a congruence-type rule "!! x. Q x -->
f(x)=g(x) ==> F(f(x),x)=F(g(x),x)" (for example, \sum_{x\in A} f(x) =
\sum_{x\in A} g(x) when for all x\in A, f(x)=g(x)), then replace F(f(x),x)
with F(g(x),x) and add the condition "Q x ==> P x" as a goal to be proved.

- "auto intro a rule only if it succeeds directly (cf. Hint Immediate in
Coq)" Given a rule P x ==> Q x ==> R x, if R x is in the goal, see if P x
and Q x are in the premises. If so, solve it. If not, do not introduce P x,
Q x. (Use case: rules like A\subseteq B ==> B\subseteq C ==> A\subseteq C:
marking this as a intro rule would cause infinite regress.)

- Don't go deeper than depth x - so prevent it from going down an
infinite branch.

Cheers,

Holden

view this post on Zulip Email Gateway (Aug 19 2022 at 15:21):

From: Lawrence Paulson <lp15@cam.ac.uk>
Don’t overlook blast, which is a little more flexible in its use of inference rules and can even cope with reasonable amounts of transitivity. However, it doesn’t do simplification at all, so simplify in a previous step.

Larry


Last updated: Mar 29 2024 at 08:18 UTC