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