I have the following definitions:
inductive star :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
refl: "star r x x"
|step: "r x y ⟹ star r y z ⟹ star r x z"
and
inductive star' :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
refl': "star' r x x"
|step': "star' r x y ⟹ r y z ⟹ star' r x z"
I want to prove the lemma star' r x y ⟹ star r x y. I have transitivity of star.
I follow the guide: concrete-semantics. There (ex. 4.3 as of 2023.12.04) it is hinted that I would need auxiliary lemma and that the induction wouldn't work because the assumption about the inductive predicate (⋀x y z. r x y ⟹ star r y z ⟹ star' r y z ⟹ star' r x z) is not the first assumption (star r x y ⟹ star' r x y), i.e. r x y ≠ star r x y.
My understanding is that I need to make a lemma h of the sort: ∀x y z. r x y ⟶ star r y z ⟶ star' r y z ⟶ star' r x z ⟹ ∀x y z. star r y z ⟶ r x y ⟶ star' r y z ⟶ star' r x z and replace (i.e. simplify) it in the inductive predicate.. But I am having trouble understanding the differences between ∀ and it's meta version.. when I did such lemma and tried to use it for simplification, I got infinite loop:
lemma "star r x y ⟹ star' r x y"
apply(induction rule: star.induct)
apply (simp add: refl')
apply (simp add: h)
I tried many other variants, but to be honest, those attempts were probably even worse than the one I shared just above.