IMP/Util distinguishes between sets and functions again; imported only where used.
theory Star imports Main
begin
inductive
star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
for r where
refl: "star r x x" |
step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
lemma star_trans:
"star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
proof(induct 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 \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
declare star.refl[simp,intro]
lemma step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
by(metis refl step)
code_pred star .
end