--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Star.thy Wed Jun 01 21:35:34 2011 +0200
@@ -0,0 +1,27 @@
+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