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