src/HOL/IMP/Star.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45015 fdac1e9880eb
child 45265 521508e85c0d
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
nipkow@43141
     1
theory Star imports Main
nipkow@43141
     2
begin
nipkow@43141
     3
nipkow@43141
     4
inductive
nipkow@43141
     5
  star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
nipkow@43141
     6
for r where
nipkow@43141
     7
refl:  "star r x x" |
nipkow@43141
     8
step:  "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
nipkow@43141
     9
nipkow@43141
    10
lemma star_trans:
nipkow@43141
    11
  "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
nipkow@45015
    12
proof(induction rule: star.induct)
nipkow@43141
    13
  case refl thus ?case .
nipkow@43141
    14
next
nipkow@43141
    15
  case step thus ?case by (metis star.step)
nipkow@43141
    16
qed
nipkow@43141
    17
nipkow@43141
    18
lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
nipkow@43141
    19
nipkow@43141
    20
declare star.refl[simp,intro]
nipkow@43141
    21
nipkow@43141
    22
lemma step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
nipkow@43141
    23
by(metis refl step)
nipkow@43141
    24
nipkow@43141
    25
code_pred star .
nipkow@43141
    26
nipkow@43141
    27
end