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
```