## Stream: Beginner Questions

### Topic: check whether subgoal changed independent of premise order

#### Leander Behr (Jun 30 2022 at 17:39):

I am using Eisbach to write a method that uses rules to add premises. Using it repeatedly will insert duplicate premises and I also don't want the method to be applicable multiple times without changes in between applications, so that for example `method+` doesn't infinite loop.

I've come up with

``````lemma dupl: "X ⟹ (X ⟹ Y) ⟹ Y" by simp

method thin_duplicate =
match premises in P[thin]: Q for Q ⇒
‹match premises in Q ⇒ ‹rule dupl[OF P]››

method thin_all_duplicates = thin_duplicate+

method my_method = changed ‹my_method'›
``````

The problem is that `thin_all_duplicates` does not preserve the order of premises. Is there a way to remove duplicate premises in a way that does not reorder the existing ones? Or alternatively, a way to check whether premises changed independently of their order?

Note that I know next to no ML or even Isabelle/ML.

edit: I also just noticed that `thin_all_duplicates` sometimes infinite loops, but I haven't figured out why yet. It looks like `[thin]` sometimes removes only one occurrence of the premise, but sometimes also both, which is why I introduced the `dupl` rule in the first place.

#### Leander Behr (Jul 01 2022 at 11:32):

I think one way to solve this would be to use `thin_tac` within `thin_duplicate`, as it appears to consistently remove only one premise. But I couldn't find a way to provide a pattern to it. It appears that it takes neither terms nor facts. That is neither `method X for t = thin_tac t` nor `method X uses t = thin_tac t` work.

Last updated: Sep 22 2023 at 08:19 UTC