src/HOL/IMP/Star.thy

+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