Shweta Rajiv (Oct 18 2025 at 19:31): Shweta Rajiv (Oct 18 2025 at 19:31):Hi. I’m trying to write a proof method that recursively rewrites both sides of a logical equivalence.
For example:
lemma add_zero: "x = x + 0" by simp
method lhs_rewrite for x :: nat = (subst add_zero)
method recursive_rewrite for x :: nat =
(rule iffI; recursive_rewrite x)
| (match premises in H: "_ ⟹ _" ⇒ ‹insert H, recursive_rewrite x›)
| (lhs_rewrite x)
lemma
fixes x :: nat
shows "(x = x) ⟷ (x = x)"
apply (recursive_rewrite x)
This produces subgoals:
1. (x = x) ⟹ x + 0 = x + 0
2. (x = x) ⟹ x + 0 = x + 0
which is good, but I’d like the method to also rewrite inside the premise,
i.e. get both sides as x + 0 = x + 0 ⟹ x + 0 = x + 0.
Is there a way to make a custom method rewrite inside the antecedent of implications as well? This is what I tried to do with the match premises but I don't think I'm using it correctly.
Mathias Fleury (Oct 18 2025 at 19:36):You can also let the subst do the work:
method lhs_rewrite for x :: nat = ((subst (asm) add_zero)?; (subst add_zero)?)
I see. But suppose the rule was an implication.
For example:
lemma less_imp_le_rule:
fixes x y :: nat
shows "x < y ⟹ x ≤ y"
by simp
method rel_rewrite for x y :: nat =
(rule less_imp_le_rule)
method recursive_rewrite1 for x y :: nat =
(rule iffI; recursive_rewrite1 x y)
| (rule impI; recursive_rewrite1 x y)
| (match premises in H: _ ⇒ ‹rel_rewrite x y›)
| (rel_rewrite x y)
lemma
fixes x y :: nat
shows "(x ≤ y) ⟷ (y ≤ x)"
apply (recursive_rewrite1 x y)
After running this, the goal becomes:
1. x ≤ y ⟹ y < x
2. y ≤ x ⟹ x < y
So, the rule has been applied in the conclusions.
However, I’d also like the premises (x ≤ y and y ≤ x) to be converted to x < y and y < x, respectively. So, I want the method to be applied to the premises as well.
Mathias Fleury (Oct 19 2025 at 19:32):Wrong direction for the rule for implicatio
Mathias Fleury (Oct 19 2025 at 19:32):you need the dest rule
Mathias Fleury (Oct 19 2025 at 19:34):You want this, but it does not hold:
lemma less_imp_le_ruleD:
fixes x y :: nat
shows "x ≤ y ⟹ x < y "
by simp
Ah, sorry I didn’t mean that I wanted to use x ≤ y ⟹ x < y. I was trying to come up with a simple toy example to illustrate a method definition issue.
I’m using the Eisbach manual to try to implement a recursive method. I can apply my rules in the conclusion of each subgoal, but I’d also like to apply them inside the premises of implications. It seemed like that’s what match premises is intended for, but I couldn’t get it to work.
After some more reading, my understanding is that match premises lets you lift the premise as a hypothetical theorem to use in other rules, but it doesn’t actually let you change or rewrite the premise itself. The match method allows selection of specific premises or conclusion patterns to apply other methods to. It does not alter the structure of the goal itself. So I suppose I’d need to use subst or some other mechanism if I really want to rewrite inside the premise?
Edoardo Putti (Oct 31 2025 at 09:58):This can be taken care of with a conversion. Rewrite your lemma to use meta-equality and then you use it to create a conversion (Conv.rewr_thm). Once you have a conversion there is a way to turn it into a tactic using CONVERSION.
Shweta Rajiv (Nov 03 2025 at 18:53):Thank you! This certainly seems like it could work. I now have a minimal version that does what I want using conversion and I think I can extend it to my original problem.
Last updated: Nov 07 2025 at 16:23 UTC