src/HOL/IMP/Star.thy
author huffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165 d26a45f3c835
parent 43141 11fce8564415
child 45015 fdac1e9880eb
permissions -rw-r--r--
remove lemma stupid_ext
     1 theory Star imports Main
     2 begin
     3 
     4 inductive
     5   star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
     6 for r where
     7 refl:  "star r x x" |
     8 step:  "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
     9 
    10 lemma star_trans:
    11   "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
    12 proof(induct rule: star.induct)
    13   case refl thus ?case .
    14 next
    15   case step thus ?case by (metis star.step)
    16 qed
    17 
    18 lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
    19 
    20 declare star.refl[simp,intro]
    21 
    22 lemma step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
    23 by(metis refl step)
    24 
    25 code_pred star .
    26 
    27 end