Leander Behr (Jun 30 2022 at 17:39): 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: Apr 25 2024 at 16:19 UTC