src/CCL/Trancl.thy
changeset 17456 bcf7544875b2
parent 1474 3f7d67927fe2
child 20140 98acc6d0fab6
     1.1 --- a/src/CCL/Trancl.thy	Sat Sep 17 14:02:31 2005 +0200
     1.2 +++ b/src/CCL/Trancl.thy	Sat Sep 17 17:35:26 2005 +0200
     1.3 @@ -1,28 +1,31 @@
     1.4 -(*  Title:      CCL/trancl.thy
     1.5 +(*  Title:      CCL/Trancl.thy
     1.6      ID:         $Id$
     1.7      Author:     Martin Coen, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9 -
    1.10 -Transitive closure of a relation
    1.11  *)
    1.12  
    1.13 -Trancl = CCL +
    1.14 +header {* Transitive closure of a relation *}
    1.15 +
    1.16 +theory Trancl
    1.17 +imports CCL
    1.18 +begin
    1.19  
    1.20  consts
    1.21 -    trans   :: "i set => o"                   (*transitivity predicate*)
    1.22 -    id      :: "i set"
    1.23 -    rtrancl :: "i set => i set"               ("(_^*)" [100] 100)
    1.24 -    trancl  :: "i set => i set"               ("(_^+)" [100] 100)  
    1.25 -    O       :: "[i set,i set] => i set"       (infixr 60)
    1.26 -
    1.27 -rules   
    1.28 +  trans   :: "i set => o"                   (*transitivity predicate*)
    1.29 +  id      :: "i set"
    1.30 +  rtrancl :: "i set => i set"               ("(_^*)" [100] 100)
    1.31 +  trancl  :: "i set => i set"               ("(_^+)" [100] 100)
    1.32 +  O       :: "[i set,i set] => i set"       (infixr 60)
    1.33  
    1.34 -trans_def       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
    1.35 -comp_def        (*composition of relations*)
    1.36 -                "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
    1.37 -id_def          (*the identity relation*)
    1.38 -                "id == {p. EX x. p = <x,x>}"
    1.39 -rtrancl_def     "r^* == lfp(%s. id Un (r O s))"
    1.40 -trancl_def      "r^+ == r O rtrancl(r)"
    1.41 +axioms
    1.42 +  trans_def:       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
    1.43 +  comp_def:        (*composition of relations*)
    1.44 +                   "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
    1.45 +  id_def:          (*the identity relation*)
    1.46 +                   "id == {p. EX x. p = <x,x>}"
    1.47 +  rtrancl_def:     "r^* == lfp(%s. id Un (r O s))"
    1.48 +  trancl_def:      "r^+ == r O rtrancl(r)"
    1.49 +
    1.50 +ML {* use_legacy_bindings (the_context ()) *}
    1.51  
    1.52  end