Theory HOL-IMP.Star

theory Star imports Main
begin

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"

hide_fact (open) refl step  ― ‹names too generic›

lemma star_trans:
  "star r x y ⟹ star r y z ⟹ star r x z"
proof(induction rule: star.induct)
  case refl thus ?case .
next
  case step thus ?case by (metis star.step)
qed

lemmas star_induct =
  star.induct[of "r:: 'a*'b ⇒ 'a*'b ⇒ bool", split_format(complete)]

declare star.refl[simp,intro]

lemma star_step1[simp, intro]: "r x y ⟹ star r x y"
by(metis star.refl star.step)

code_pred star .

end