I have situations where my current facts contain facts that match some of the premises of a rule I wish to apply and may also include additional ones. Doing "then have mygoal proof(rule myrule)" doesn't work as the list of premises in myrule does not match the list of current facts.

For example, my current facts are A B C, I need to prove P and I have a rule B ⇒ A ⇒ D ⇒ P.

Is there a way of applying the rule so that the appropriate ordering of current facts is done automatically so that the rule can be applied. If not can Eisbach help?

By using `from`

instead of `then`

you can reorder the facts, e.g. `from this(2,3,1) have ...`

Thanks, I handn't throught to use this( <list of numbers> ).

I am still interested in any automatic method of finding the ordering as the proof is not robust if the ordering of the current facts changes. The use case I have in mind is inductive predicate proofs where the 'case' introduces a number of facts and the order can change if I make a change to the rule that introduces new premises or deletes them.

I am not sure if something like this exists. In some cases it would quite hard to discern the right ordering, for example if you have the rule `x < y ==> y < z ==> x < z`

I guess you could try something like `by (rule myrule; rule this; fail)`

but depending on how much ambiguity there is, that might cause a lot of backtracking

if there is no ambiguity, it should work without problems

as Lukas said, it is not always the case that there is a clear "correct" ordering, so I don't think there is a builtin Isar method that tries to do something like that

You might want to try my `fuzzy_rule`

method: https://github.com/peterzeller/isabelle_fuzzy_rule

It's an attempt to get rid of the strict ordering and strict matching requirements of `rule`

Thanks, I will take a look. The matching requirement was another thing I was looking for some flexibility on.

Last updated: Sep 25 2022 at 23:25 UTC