Re: [isabelle] resolve current subgoal with matching premise





On 12/05/2014 09:41 AM, Peter Lammich wrote:
In "$AFP/Automatic_Refinement/Lib/Refine_Util", there is a method
rprems.

apply (rprems)  -- resolve with the first matching premise
apply (rprems n) -- resolve with the nth premise

I frequently use this to apply induction hypothesis in
apply-style/automatic proofs.
Yes, that's also my use case. Thanks for the pointer!

cheers

chris


Cheers,
   Peter


On Do, 2014-12-04 at 22:37 +0100, Jasmin Christian Blanchette wrote:
Hi Chris,

is there an easy way in Isabelle/ML to replace the current subgoal by the assumptions of the first premise whose conclusion matches it?

Example:
I have a subgoal of the shape

!! a1 ... aN.
  (!! b1 ... bK. ...) ==>
  ...
  (!! i1 ... iM. ... ==> P iI) (*[*]*) ==>
  ...
  (!! z1 ... zL. ...) ==> P aJ

and would like to replace it by the premises of [*]. I think this should be easy but could figure it out immediately.

You could try

     apply ((drule meta_spec)+, erule meta_mp)

E.g.:

     lemma "!! a1 aJ aN.
      (!! b1 bK. q b1 bK) ==>
      (!! i1 iI iM. r i1 iI iM ==> P iI) ==>
      (!! z1 zL. s z1 zL) ==> P aJ"
     apply ((drule meta_spec)+, erule meta_mp)

If you do this at the tactic level (or use the "back" command), the built-in nondeterminism will make it work more generally for any premise whose conclusion matches the subgoal's conclusion.

I hope this helps.

Cheers,

Jasmin









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.