src/CCL/Trancl.thy
changeset 24825 c4f13ab78f9d
parent 20140 98acc6d0fab6
child 32153 a0e57fb1b930
     1.1 --- a/src/CCL/Trancl.thy	Wed Oct 03 19:49:33 2007 +0200
     1.2 +++ b/src/CCL/Trancl.thy	Wed Oct 03 21:29:05 2007 +0200
     1.3 @@ -15,11 +15,11 @@
     1.4    id      :: "i set"
     1.5    rtrancl :: "i set => i set"               ("(_^*)" [100] 100)
     1.6    trancl  :: "i set => i set"               ("(_^+)" [100] 100)
     1.7 -  O       :: "[i set,i set] => i set"       (infixr 60)
     1.8 +  relcomp :: "[i set,i set] => i set"       (infixr "O" 60)
     1.9  
    1.10  axioms
    1.11    trans_def:       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
    1.12 -  comp_def:        (*composition of relations*)
    1.13 +  relcomp_def:     (*composition of relations*)
    1.14                     "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
    1.15    id_def:          (*the identity relation*)
    1.16                     "id == {p. EX x. p = <x,x>}"
    1.17 @@ -57,14 +57,14 @@
    1.18  subsection {* Composition of two relations *}
    1.19  
    1.20  lemma compI: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"
    1.21 -  unfolding comp_def by blast
    1.22 +  unfolding relcomp_def by blast
    1.23  
    1.24  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    1.25  lemma compE:
    1.26      "[| xz : r O s;
    1.27          !!x y z. [| xz = <x,z>;  <x,y>:s;  <y,z>:r |] ==> P
    1.28       |] ==> P"
    1.29 -  unfolding comp_def by blast
    1.30 +  unfolding relcomp_def by blast
    1.31  
    1.32  lemma compEpair:
    1.33    "[| <a,c> : r O s;