src/CCL/Trancl.thy
 changeset 24825 c4f13ab78f9d parent 20140 98acc6d0fab6 child 32153 a0e57fb1b930
equal inserted replaced
24824:b7866aea0815 24825:c4f13ab78f9d
`    13 consts`
`    13 consts`
`    14   trans   :: "i set => o"                   (*transitivity predicate*)`
`    14   trans   :: "i set => o"                   (*transitivity predicate*)`
`    15   id      :: "i set"`
`    15   id      :: "i set"`
`    16   rtrancl :: "i set => i set"               ("(_^*)" [100] 100)`
`    16   rtrancl :: "i set => i set"               ("(_^*)" [100] 100)`
`    17   trancl  :: "i set => i set"               ("(_^+)" [100] 100)`
`    17   trancl  :: "i set => i set"               ("(_^+)" [100] 100)`
`    18   O       :: "[i set,i set] => i set"       (infixr 60)`
`    18   relcomp :: "[i set,i set] => i set"       (infixr "O" 60)`
`    19 `
`    19 `
`    20 axioms`
`    20 axioms`
`    21   trans_def:       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"`
`    21   trans_def:       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"`
`    22   comp_def:        (*composition of relations*)`
`    22   relcomp_def:     (*composition of relations*)`
`    23                    "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"`
`    23                    "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"`
`    24   id_def:          (*the identity relation*)`
`    24   id_def:          (*the identity relation*)`
`    25                    "id == {p. EX x. p = <x,x>}"`
`    25                    "id == {p. EX x. p = <x,x>}"`
`    26   rtrancl_def:     "r^* == lfp(%s. id Un (r O s))"`
`    26   rtrancl_def:     "r^* == lfp(%s. id Un (r O s))"`
`    27   trancl_def:      "r^+ == r O rtrancl(r)"`
`    27   trancl_def:      "r^+ == r O rtrancl(r)"`
`    55 `
`    55 `
`    56 `
`    56 `
`    57 subsection {* Composition of two relations *}`
`    57 subsection {* Composition of two relations *}`
`    58 `
`    58 `
`    59 lemma compI: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"`
`    59 lemma compI: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"`
`    60   unfolding comp_def by blast`
`    60   unfolding relcomp_def by blast`
`    61 `
`    61 `
`    62 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)`
`    62 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)`
`    63 lemma compE:`
`    63 lemma compE:`
`    64     "[| xz : r O s;`
`    64     "[| xz : r O s;`
`    65         !!x y z. [| xz = <x,z>;  <x,y>:s;  <y,z>:r |] ==> P`
`    65         !!x y z. [| xz = <x,z>;  <x,y>:s;  <y,z>:r |] ==> P`
`    66      |] ==> P"`
`    66      |] ==> P"`
`    67   unfolding comp_def by blast`
`    67   unfolding relcomp_def by blast`
`    68 `
`    68 `
`    69 lemma compEpair:`
`    69 lemma compEpair:`
`    70   "[| <a,c> : r O s;`
`    70   "[| <a,c> : r O s;`
`    71       !!y. [| <a,y>:s;  <y,c>:r |] ==> P`
`    71       !!y. [| <a,y>:s;  <y,c>:r |] ==> P`
`    72    |] ==> P"`
`    72    |] ==> P"`