src/HOL/IMP/Star.thy
author nipkow
Tue, 20 Sep 2011 05:48:23 +0200
changeset 45015 fdac1e9880eb
parent 43141 11fce8564415
child 45265 521508e85c0d
permissions -rw-r--r--
Updated IMP to use new induction method

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(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 \<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