src/HOL/Transitive_Closure.thy
changeset 11327 cd2c27a23df1
parent 11115 285b31e9e026
child 12428 f3033eed309a
     1.1 --- a/src/HOL/Transitive_Closure.thy	Tue May 22 15:11:43 2001 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Tue May 22 15:12:11 2001 +0200
     1.3 @@ -13,13 +13,18 @@
     1.4  to be atomic.
     1.5  *)
     1.6  
     1.7 -theory Transitive_Closure = Lfp + Relation
     1.8 +theory Transitive_Closure = Inductive
     1.9  files ("Transitive_Closure_lemmas.ML"):
    1.10  
    1.11 +consts
    1.12 +  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    1.13 +
    1.14 +inductive "r^*"
    1.15 +intros
    1.16 +  rtrancl_refl [intro!, simp]: "(a, a) : r^*"
    1.17 +  rtrancl_into_rtrancl:        "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*"
    1.18 +
    1.19  constdefs
    1.20 -  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    1.21 -  "r^* == lfp (%s. Id Un (r O s))"
    1.22 -
    1.23    trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
    1.24    "r^+ ==  r O rtrancl r"
    1.25  
    1.26 @@ -89,5 +94,11 @@
    1.27  	"x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
    1.28   apply (auto)
    1.29   by (erule rev_mp, erule rtrancl_induct, auto)
    1.30 - 
    1.31 +
    1.32 +
    1.33 +declare rtrancl_induct [induct set: rtrancl]
    1.34 +declare rtranclE [cases set: rtrancl]
    1.35 +declare trancl_induct [induct set: trancl]
    1.36 +declare tranclE [cases set: trancl]
    1.37 +
    1.38  end