Suppose the goal is P l, then I can use apply(subst X) where X is of the form l=r
and as a result I obtain P r. Now my question is whether there exists some other tactic like subst but which could use X to change P r into P l.
Here is an example
theorem mul_1_I : "(x::nat) = 1 * x" by (rule sym, rule Nat.nat_mult_1)
theorem "(λ x::nat . x) ≤ (λ x::nat . 2*x)"
using [[simp_trace]]
apply(rule le_funI)
apply(subst mul_1_I)
apply(rule mult_le_mono1)
apply(simp)
done
where
lemma nat_mult_1: "1 * n = n"
Right now I have to first prove this auxiliary lemma mul_1_I which applies sym to nat_mult_1 and only then I can use subst. Would be ideal if I didn't have to create new lemma specifically for this.
You can use the symmetric attribute to derive the swapped fact. For example, if x is of the form l = r, then x [symmetric] is the fact r = l (which is also valid due to the symmetry of =). Therefore, in your particular case you can use subst nat_mult_1 [symmetric] directly and avoid creating your auxiliary lemma.