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
     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 hide_fact (open) refl step  --"names too generic"
    11 
    12 lemma star_trans:
    13   "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
    14 proof(induction rule: star.induct)
    15   case refl thus ?case .
    16 next
    17   case step thus ?case by (metis star.step)
    18 qed
    19 
    20 lemmas star_induct =
    21   star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
    22 
    23 declare star.refl[simp,intro]
    24 
    25 lemma star_step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
    26 by(metis star.refl star.step)
    27 
    28 code_pred star .
    29 
    30 end