# Theory Trancl

Up to index of Isabelle/CCL

theory Trancl
imports CCL
uses [Trancl.ML]
begin

    (*  Title:      CCL/Trancl.thy
        ID:         $Id: Trancl.thy,v 1.3 2005/09/17 15:35:29 wenzelm Exp $
        Author:     Martin Coen, Cambridge University Computer Laboratory
        Copyright   1993  University of Cambridge
    *)

    header {* Transitive closure of a relation *}

    theory Trancl
    imports CCL
    begin

    consts
      trans   :: "i set => o"                   (*transitivity predicate*)
      id      :: "i set"
      rtrancl :: "i set => i set"               ("(_^*)" [100] 100)
      trancl  :: "i set => i set"               ("(_^+)" [100] 100)
      O       :: "[i set,i set] => i set"       (infixr 60)

    axioms
      trans_def:       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
      comp_def:        (*composition of relations*)
                       "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
      id_def:          (*the identity relation*)
                       "id == {p. EX x. p = <x,x>}"
      rtrancl_def:     "r^* == lfp(%s. id Un (r O s))"
      trancl_def:      "r^+ == r O rtrancl(r)"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem transI:

      (!!x y z. [| <x,y> : r; <y,z> : r |] ==> <x,z> : r) ==> trans(r)

theorem transD:

      [| trans(r); <a,b> : r; <b,c> : r |] ==> <a,c> : r

theorem idI:

      <a,a> : id

theorem idE:

      [| p : id; !!x. p = <x,x> ==> P |] ==> P

theorem compI:

      [| <a,b> : s; <b,c> : r |] ==> <a,c> : r O s

theorem compE:

      [| xz : r O s; !!x y z. [| xz = <x,z>; <x,y> : s; <y,z> : r |] ==> P |] ==> P

theorem compEpair:

      [| <a,c> : r O s; !!y. [| <a,y> : s; <y,c> : r |] ==> P |] ==> P

theorem comp_mono:

      [| r' <= r; s' <= s |] ==> r' O s' <= r O s

theorem rtrancl_fun_mono:

      mono(%s. id Un (r O s))

theorem rtrancl_refl:

      <a,a> : r^*

theorem rtrancl_into_rtrancl:

      [| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*

theorem r_into_rtrancl:

      <a,b> : r ==> <a,b> : r^*

theorem rtrancl_full_induct:

      [| <a,b> : r^*; !!x. P(<x,x>);
         !!x y z. [| P(<x,y>); <x,y> : r^*; <y,z> : r |] ==> P(<x,z>) |]
      ==> P(<a,b>)

theorem rtrancl_induct:

      [| <a,b> : r^*; P(a); !!y z. [| <a,y> : r^*; <y,z> : r; P(y) |] ==> P(z) |]
      ==> P(b)

theorem trans_rtrancl:

      trans(r^*)

theorem rtranclE:

      [| <a,b> : r^*; a = b ==> P; !!y. [| <a,y> : r^*; <y,b> : r |] ==> P |] ==> P

theorem trancl_into_rtrancl:

      <a,b> : r^+ ==> <a,b> : r^*

theorem r_into_trancl:

      <a,b> : r ==> <a,b> : r^+

theorem rtrancl_into_trancl1:

      [| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+

theorem rtrancl_into_trancl2:

      [| <a,b> : r; <b,c> : r^* |] ==> <a,c> : r^+

theorem tranclE:

      [| <a,b> : r^+; <a,b> : r ==> P; !!y. [| <a,y> : r^+; <y,b> : r |] ==> P |]
      ==> P

theorem trans_trancl:

      trans(r^+)

theorem trancl_into_trancl2:

      [| <a,b> : r; <b,c> : r^+ |] ==> <a,c> : r^+