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.
I think one way to solve this would be to use
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