Stream: Beginner Questions

Topic: Automatic reordering of current facts to apply rule

Mark Wassell (Aug 18 2020 at 08:03):

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?

Lukas Stevens (Aug 18 2020 at 08:06):

By using from instead of then you can reorder the facts, e.g. from this(2,3,1) have ...

Mark Wassell (Aug 18 2020 at 08:14):

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.

Lukas Stevens (Aug 18 2020 at 08:17):

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

Manuel Eberl (Aug 18 2020 at 08:17):

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

Manuel Eberl (Aug 18 2020 at 08:18):

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

Manuel Eberl (Aug 18 2020 at 08:18):

if there is no ambiguity, it should work without problems

Manuel Eberl (Aug 18 2020 at 08:19):

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

Peter Zeller (Aug 18 2020 at 18:40):

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

Mark Wassell (Aug 19 2020 at 07:03):

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

Last updated: Dec 21 2024 at 16:20 UTC