Hanno Becker (Apr 30 2024 at 11:15): Hanno Becker (Apr 30 2024 at 11:15):Hi. I'd like to modify the claset so that safe and clarsimp do _not_ do the following
lemma
‹¬(A ⊆ B) ⟹ C›
apply safe_step
(* proof (prove)
goal (1 subgoal):
1. ⋀x. ¬ C ⟹ x ∈ A ⟹ x ∈ B *)
However, I'm struggling with identifying the lemma/code that triggers this transformation. Can someone help?
Lukas Stevens (Apr 30 2024 at 12:37):It applies something like subsetI.
Lukas Stevens (Apr 30 2024 at 12:58):It seems to apply contraposition and then subsetI. It is not clear why it applies contraposition though...
Hanno Becker (Apr 30 2024 at 20:27):It would be enough to know how to disable it :-)
Simon Roßkopf (Apr 30 2024 at 21:20):To remove a rule (intro/dest/elim...) from the claset you can use the rule del attribute, for example with declare subsetI[rule del]. See also section 9.4.2 of the isar-ref.
After that the safe_step does nothing on your example goal.
Hanno Becker (May 01 2024 at 03:05):Thank you. I should have clarified that removing subsetI goes too far in my case -- I only want to avoid it in conjunction with contraposition.
Lukas Stevens (May 02 2024 at 09:25):I tried disabling all contraposition theorems that I found using find_theorems but to no avail. Maybe contraposition is baked into safe_step?
Last updated: May 19 2024 at 01:13 UTC