src/HOL/IMP/Star.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 50054 6da283e4497b
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
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@45265
    10
hide_fact (open) refl step  --"names too generic"
nipkow@45265
    11
nipkow@43141
    12
lemma star_trans:
nipkow@43141
    13
  "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
nipkow@45015
    14
proof(induction rule: star.induct)
nipkow@43141
    15
  case refl thus ?case .
nipkow@43141
    16
next
nipkow@43141
    17
  case step thus ?case by (metis star.step)
nipkow@43141
    18
qed
nipkow@43141
    19
nipkow@50054
    20
lemmas star_induct =
nipkow@50054
    21
  star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
nipkow@43141
    22
nipkow@43141
    23
declare star.refl[simp,intro]
nipkow@43141
    24
nipkow@45265
    25
lemma star_step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
nipkow@45265
    26
by(metis star.refl star.step)
nipkow@43141
    27
nipkow@43141
    28
code_pred star .
nipkow@43141
    29
nipkow@43141
    30
end