*To*: Holden Lee <hl422 at cam.ac.uk>*Subject*: Re: [isabelle] Do these tactics exist?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 11 Aug 2014 14:29:30 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAKSvo_Yu0rgAytOYhjGonzCzZEe+Xcuh37V9nDJ1eNU0vmuqOg@mail.gmail.com>*References*: <CAKSvo_Yu0rgAytOYhjGonzCzZEe+Xcuh37V9nDJ1eNU0vmuqOg@mail.gmail.com>

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 On 11 Aug 2014, at 13:00, Holden Lee <hl422 at cam.ac.uk> wrote: > 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

**References**:**[isabelle] Do these tactics exist?***From:*Holden Lee

- Previous by Date: Re: [isabelle] op =simp=> in congruence rules
- Next by Date: [isabelle] monadic function definition
- Previous by Thread: [isabelle] Do these tactics exist?
- Next by Thread: [isabelle] monadic function definition
- Cl-isabelle-users August 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list