Stream: Beginner Questions

Topic: check whether subgoal changed independent of premise order

view this post on Zulip 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.

view this post on Zulip 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