# Theory Trancl

Up to index of Isabelle/ZF

theory Trancl
imports Fixedpt Perm
begin

    (*  Title:      ZF/Trancl.thy
        ID:         $Id: Trancl.thy,v 1.20 2005/06/17 14:15:09 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1992  University of Cambridge

    *)

    header{*Relations: Their General Properties and Transitive Closure*}

    theory Trancl imports Fixedpt Perm begin

    constdefs
      refl     :: "[i,i]=>o"
        "refl(A,r) == (ALL x: A. <x,x> : r)"

      irrefl   :: "[i,i]=>o"
        "irrefl(A,r) == ALL x: A. <x,x> ~: r"

      sym      :: "i=>o"
        "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"

      asym     :: "i=>o"
        "asym(r) == ALL x y. <x,y>:r --> ~ <y,x>:r"

      antisym  :: "i=>o"
        "antisym(r) == ALL x y.<x,y>:r --> <y,x>:r --> x=y"

      trans    :: "i=>o"
        "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"

      trans_on :: "[i,i]=>o"  ("trans[_]'(_')")
        "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.
                              <x,y>: r --> <y,z>: r --> <x,z>: r"

      rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
        "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"

      trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
        "r^+ == r O r^*"

      equiv    :: "[i,i]=>o"
        "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"

    subsection{*General properties of relations*}

    subsubsection{*irreflexivity*}

    lemma irreflI:
        "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)"
    by (simp add: irrefl_def)

    lemma irreflE: "[| irrefl(A,r);  x:A |] ==>  <x,x> ~: r"
    by (simp add: irrefl_def)

    subsubsection{*symmetry*}

    lemma symI:
         "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"
    by (unfold sym_def, blast)

    lemma symE: "[| sym(r); <x,y>: r |]  ==>  <y,x>: r"
    by (unfold sym_def, blast)

    subsubsection{*antisymmetry*}

    lemma antisymI:
         "[| !!x y.[| <x,y>: r;  <y,x>: r |] ==> x=y |] ==> antisym(r)"
    by (simp add: antisym_def, blast)

    lemma antisymE: "[| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y"
    by (simp add: antisym_def, blast)

    subsubsection{*transitivity*}

    lemma transD: "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r"
    by (unfold trans_def, blast)

    lemma trans_onD:
        "[| trans[A](r);  <a,b>:r;  <b,c>:r;  a:A;  b:A;  c:A |] ==> <a,c>:r"
    by (unfold trans_on_def, blast)

    lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
    by (unfold trans_def trans_on_def, blast)

    lemma trans_on_imp_trans: "[|trans[A](r); r <= A*A|] ==> trans(r)";
    by (simp add: trans_on_def trans_def, blast)

    subsection{*Transitive closure of a relation*}

    lemma rtrancl_bnd_mono:
         "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))"
    by (rule bnd_monoI, blast+)

    lemma rtrancl_mono: "r<=s ==> r^* <= s^*"
    apply (unfold rtrancl_def)
    apply (rule lfp_mono)
    apply (rule rtrancl_bnd_mono)+
    apply blast
    done

    (* r^* = id(field(r)) Un ( r O r^* )    *)
    lemmas rtrancl_unfold =
         rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold], standard]

    (** The relation rtrancl **)

    (*  r^* <= field(r) * field(r)  *)
    lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset, standard]

    lemma relation_rtrancl: "relation(r^*)"
    apply (simp add: relation_def)
    apply (blast dest: rtrancl_type [THEN subsetD])
    done

    (*Reflexivity of rtrancl*)
    lemma rtrancl_refl: "[| a: field(r) |] ==> <a,a> : r^*"
    apply (rule rtrancl_unfold [THEN ssubst])
    apply (erule idI [THEN UnI1])
    done

    (*Closure under composition with r  *)
    lemma rtrancl_into_rtrancl: "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*"
    apply (rule rtrancl_unfold [THEN ssubst])
    apply (rule compI [THEN UnI2], assumption, assumption)
    done

    (*rtrancl of r contains all pairs in r  *)
    lemma r_into_rtrancl: "<a,b> : r ==> <a,b> : r^*"
    by (rule rtrancl_refl [THEN rtrancl_into_rtrancl], blast+)

    (*The premise ensures that r consists entirely of pairs*)
    lemma r_subset_rtrancl: "relation(r) ==> r <= r^*"
    by (simp add: relation_def, blast intro: r_into_rtrancl)

    lemma rtrancl_field: "field(r^*) = field(r)"
    by (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD])

    (** standard induction rule **)

    lemma rtrancl_full_induct [case_names initial step, consumes 1]:
      "[| <a,b> : r^*;
          !!x. x: field(r) ==> P(<x,x>);
          !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |]
       ==>  P(<a,b>)"
    by (erule def_induct [OF rtrancl_def rtrancl_bnd_mono], blast)

    (*nice induction rule.
      Tried adding the typing hypotheses y,z:field(r), but these
      caused expensive case splits!*)
    lemma rtrancl_induct [case_names initial step, induct set: rtrancl]:
      "[| <a,b> : r^*;
          P(a);
          !!y z.[| <a,y> : r^*;  <y,z> : r;  P(y) |] ==> P(z)
       |] ==> P(b)"
    (*by induction on this formula*)
    apply (subgoal_tac "ALL y. <a,b> = <a,y> --> P (y) ")
    (*now solve first subgoal: this formula is sufficient*)
    apply (erule spec [THEN mp], rule refl)
    (*now do the induction*)
    apply (erule rtrancl_full_induct, blast+)
    done

    (*transitivity of transitive closure!! -- by induction.*)
    lemma trans_rtrancl: "trans(r^*)"
    apply (unfold trans_def)
    apply (intro allI impI)
    apply (erule_tac b = z in rtrancl_induct, assumption)
    apply (blast intro: rtrancl_into_rtrancl)
    done

    lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]

    (*elimination of rtrancl -- by induction on a special formula*)
    lemma rtranclE:
        "[| <a,b> : r^*;  (a=b) ==> P;
            !!y.[| <a,y> : r^*;   <y,b> : r |] ==> P |]
         ==> P"
    apply (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r) ")
    (*see HOL/trancl*)
    apply blast
    apply (erule rtrancl_induct, blast+)
    done

    (**** The relation trancl ****)

    (*Transitivity of r^+ is proved by transitivity of r^*  *)
    lemma trans_trancl: "trans(r^+)"
    apply (unfold trans_def trancl_def)
    apply (blast intro: rtrancl_into_rtrancl
                        trans_rtrancl [THEN transD, THEN compI])
    done

    lemmas trans_on_trancl = trans_trancl [THEN trans_imp_trans_on]

    lemmas trancl_trans = trans_trancl [THEN transD, standard]

    (** Conversions between trancl and rtrancl **)

    lemma trancl_into_rtrancl: "<a,b> : r^+ ==> <a,b> : r^*"
    apply (unfold trancl_def)
    apply (blast intro: rtrancl_into_rtrancl)
    done

    (*r^+ contains all pairs in r  *)
    lemma r_into_trancl: "<a,b> : r ==> <a,b> : r^+"
    apply (unfold trancl_def)
    apply (blast intro!: rtrancl_refl)
    done

    (*The premise ensures that r consists entirely of pairs*)
    lemma r_subset_trancl: "relation(r) ==> r <= r^+"
    by (simp add: relation_def, blast intro: r_into_trancl)

    (*intro rule by definition: from r^* and r  *)
    lemma rtrancl_into_trancl1: "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+"
    by (unfold trancl_def, blast)

    (*intro rule from r and r^*  *)
    lemma rtrancl_into_trancl2:
        "[| <a,b> : r;  <b,c> : r^* |]   ==>  <a,c> : r^+"
    apply (erule rtrancl_induct)
     apply (erule r_into_trancl)
    apply (blast intro: r_into_trancl trancl_trans)
    done

    (*Nice induction rule for trancl*)
    lemma trancl_induct [case_names initial step, induct set: trancl]:
      "[| <a,b> : r^+;
          !!y.  [| <a,y> : r |] ==> P(y);
          !!y z.[| <a,y> : r^+;  <y,z> : r;  P(y) |] ==> P(z)
       |] ==> P(b)"
    apply (rule compEpair)
    apply (unfold trancl_def, assumption)
    (*by induction on this formula*)
    apply (subgoal_tac "ALL z. <y,z> : r --> P (z) ")
    (*now solve first subgoal: this formula is sufficient*)
     apply blast
    apply (erule rtrancl_induct)
    apply (blast intro: rtrancl_into_trancl1)+
    done

    (*elimination of r^+ -- NOT an induction rule*)
    lemma tranclE:
        "[| <a,b> : r^+;
            <a,b> : r ==> P;
            !!y.[| <a,y> : r^+; <y,b> : r |] ==> P
         |] ==> P"
    apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r) ")
    apply blast
    apply (rule compEpair)
    apply (unfold trancl_def, assumption)
    apply (erule rtranclE)
    apply (blast intro: rtrancl_into_trancl1)+
    done

    lemma trancl_type: "r^+ <= field(r)*field(r)"
    apply (unfold trancl_def)
    apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2])
    done

    lemma relation_trancl: "relation(r^+)"
    apply (simp add: relation_def)
    apply (blast dest: trancl_type [THEN subsetD])
    done

    lemma trancl_subset_times: "r ⊆ A * A ==> r^+ ⊆ A * A"
    by (insert trancl_type [of r], blast)

    lemma trancl_mono: "r<=s ==> r^+ <= s^+"
    by (unfold trancl_def, intro comp_mono rtrancl_mono)

    lemma trancl_eq_r: "[|relation(r); trans(r)|] ==> r^+ = r"
    apply (rule equalityI)
     prefer 2 apply (erule r_subset_trancl, clarify)
    apply (frule trancl_type [THEN subsetD], clarify)
    apply (erule trancl_induct, assumption)
    apply (blast dest: transD)
    done

    (** Suggested by Sidi Ould Ehmety **)

    lemma rtrancl_idemp [simp]: "(r^*)^* = r^*"
    apply (rule equalityI, auto)
     prefer 2
     apply (frule rtrancl_type [THEN subsetD])
     apply (blast intro: r_into_rtrancl )
    txt{*converse direction*}
    apply (frule rtrancl_type [THEN subsetD], clarify)
    apply (erule rtrancl_induct)
    apply (simp add: rtrancl_refl rtrancl_field)
    apply (blast intro: rtrancl_trans)
    done

    lemma rtrancl_subset: "[| R <= S; S <= R^* |] ==> S^* = R^*"
    apply (drule rtrancl_mono)
    apply (drule rtrancl_mono, simp_all, blast)
    done

    lemma rtrancl_Un_rtrancl:
         "[| relation(r); relation(s) |] ==> (r^* Un s^*)^* = (r Un s)^*"
    apply (rule rtrancl_subset)
    apply (blast dest: r_subset_rtrancl)
    apply (blast intro: rtrancl_mono [THEN subsetD])
    done

    (*** "converse" laws by Sidi Ould Ehmety ***)

    (** rtrancl **)

    lemma rtrancl_converseD: "<x,y>:converse(r)^* ==> <x,y>:converse(r^*)"
    apply (rule converseI)
    apply (frule rtrancl_type [THEN subsetD])
    apply (erule rtrancl_induct)
    apply (blast intro: rtrancl_refl)
    apply (blast intro: r_into_rtrancl rtrancl_trans)
    done

    lemma rtrancl_converseI: "<x,y>:converse(r^*) ==> <x,y>:converse(r)^*"
    apply (drule converseD)
    apply (frule rtrancl_type [THEN subsetD])
    apply (erule rtrancl_induct)
    apply (blast intro: rtrancl_refl)
    apply (blast intro: r_into_rtrancl rtrancl_trans)
    done

    lemma rtrancl_converse: "converse(r)^* = converse(r^*)"
    apply (safe intro!: equalityI)
    apply (frule rtrancl_type [THEN subsetD])
    apply (safe dest!: rtrancl_converseD intro!: rtrancl_converseI)
    done

    (** trancl **)

    lemma trancl_converseD: "<a, b>:converse(r)^+ ==> <a, b>:converse(r^+)"
    apply (erule trancl_induct)
    apply (auto intro: r_into_trancl trancl_trans)
    done

    lemma trancl_converseI: "<x,y>:converse(r^+) ==> <x,y>:converse(r)^+"
    apply (drule converseD)
    apply (erule trancl_induct)
    apply (auto intro: r_into_trancl trancl_trans)
    done

    lemma trancl_converse: "converse(r)^+ = converse(r^+)"
    apply (safe intro!: equalityI)
    apply (frule trancl_type [THEN subsetD])
    apply (safe dest!: trancl_converseD intro!: trancl_converseI)
    done

    lemma converse_trancl_induct [case_names initial step, consumes 1]:
    "[| <a, b>:r^+; !!y. <y, b> :r ==> P(y);
          !!y z. [| <y, z> : r; <z, b> : r^+; P(z) |] ==> P(y) |]
           ==> P(a)"
    apply (drule converseI)
    apply (simp (no_asm_use) add: trancl_converse [symmetric])
    apply (erule trancl_induct)
    apply (auto simp add: trancl_converse)
    done

    ML
    {*
    val refl_def = thm "refl_def";
    val irrefl_def = thm "irrefl_def";
    val equiv_def = thm "equiv_def";
    val sym_def = thm "sym_def";
    val asym_def = thm "asym_def";
    val antisym_def = thm "antisym_def";
    val trans_def = thm "trans_def";
    val trans_on_def = thm "trans_on_def";

    val irreflI = thm "irreflI";
    val symI = thm "symI";
    val symI = thm "symI";
    val antisymI = thm "antisymI";
    val antisymE = thm "antisymE";
    val transD = thm "transD";
    val trans_onD = thm "trans_onD";

    val rtrancl_bnd_mono = thm "rtrancl_bnd_mono";
    val rtrancl_mono = thm "rtrancl_mono";
    val rtrancl_unfold = thm "rtrancl_unfold";
    val rtrancl_type = thm "rtrancl_type";
    val rtrancl_refl = thm "rtrancl_refl";
    val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
    val r_into_rtrancl = thm "r_into_rtrancl";
    val r_subset_rtrancl = thm "r_subset_rtrancl";
    val rtrancl_field = thm "rtrancl_field";
    val rtrancl_full_induct = thm "rtrancl_full_induct";
    val rtrancl_induct = thm "rtrancl_induct";
    val trans_rtrancl = thm "trans_rtrancl";
    val rtrancl_trans = thm "rtrancl_trans";
    val rtranclE = thm "rtranclE";
    val trans_trancl = thm "trans_trancl";
    val trancl_trans = thm "trancl_trans";
    val trancl_into_rtrancl = thm "trancl_into_rtrancl";
    val r_into_trancl = thm "r_into_trancl";
    val r_subset_trancl = thm "r_subset_trancl";
    val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1";
    val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2";
    val trancl_induct = thm "trancl_induct";
    val tranclE = thm "tranclE";
    val trancl_type = thm "trancl_type";
    val trancl_mono = thm "trancl_mono";
    val rtrancl_idemp = thm "rtrancl_idemp";
    val rtrancl_subset = thm "rtrancl_subset";
    val rtrancl_converseD = thm "rtrancl_converseD";
    val rtrancl_converseI = thm "rtrancl_converseI";
    val rtrancl_converse = thm "rtrancl_converse";
    val trancl_converseD = thm "trancl_converseD";
    val trancl_converseI = thm "trancl_converseI";
    val trancl_converse = thm "trancl_converse";
    val converse_trancl_induct = thm "converse_trancl_induct";
    *}

    end

### General properties of relations

#### irreflexivity

lemma irreflI:

      (!!x. x ∈ A ==> ⟨x, x⟩ ∉ r) ==> irrefl(A, r)

lemma irreflE:

      [| irrefl(A, r); x ∈ A |] ==> ⟨x, x⟩ ∉ r

#### symmetry

lemma symI:

      (!!x y. ⟨x, y⟩ ∈ r ==> ⟨y, x⟩ ∈ r) ==> sym(r)

lemma symE:

      [| sym(r); ⟨x, y⟩ ∈ r |] ==> ⟨y, x⟩ ∈ r

#### antisymmetry

lemma antisymI:

      (!!x y. [| ⟨x, y⟩ ∈ r; ⟨y, x⟩ ∈ r |] ==> x = y) ==> antisym(r)

lemma antisymE:

      [| antisym(r); ⟨x, y⟩ ∈ r; ⟨y, x⟩ ∈ r |] ==> x = y

#### transitivity

lemma transD:

      [| trans(r); ⟨a, b⟩ ∈ r; ⟨b, c⟩ ∈ r |] ==> ⟨a, c⟩ ∈ r

lemma trans_onD:

      [| trans[A](r); ⟨a, b⟩ ∈ r; ⟨b, c⟩ ∈ r; a ∈ A; b ∈ A; c ∈ A |] ==> ⟨a, c⟩ ∈ r

lemma trans_imp_trans_on:

      trans(r) ==> trans[A](r)

lemma trans_on_imp_trans:

      [| trans[A](r); r ⊆ A × A |] ==> trans(r)

### Transitive closure of a relation

lemma rtrancl_bnd_mono:

      bnd_mono(field(r) × field(r), %s. id(field(r)) ∪ (r O s))

lemma rtrancl_mono:

      r ⊆ s ==> r^* ⊆ s^*

lemmas rtrancl_unfold:

      r^* = id(field(r)) ∪ (r O r^*)

lemmas rtrancl_unfold:

      r^* = id(field(r)) ∪ (r O r^*)

lemmas rtrancl_type:

      r^* ⊆ field(r) × field(r)

lemmas rtrancl_type:

      r^* ⊆ field(r) × field(r)

lemma relation_rtrancl:

      relation(r^*)

lemma rtrancl_refl:

      a ∈ field(r) ==> ⟨a, a⟩ ∈ r^*

lemma rtrancl_into_rtrancl:

      [| ⟨a, b⟩ ∈ r^*; ⟨b, c⟩ ∈ r |] ==> ⟨a, c⟩ ∈ r^*

lemma r_into_rtrancl:

      ⟨a, b⟩ ∈ r ==> ⟨a, b⟩ ∈ r^*

lemma r_subset_rtrancl:

      relation(r) ==> r ⊆ r^*

lemma rtrancl_field:

      field(r^*) = field(r)

lemma rtrancl_full_induct:

      [| ⟨a, b⟩ ∈ r^*; !!x. x ∈ field(r) ==> P(⟨x, x⟩);
         !!x y z. [| P(⟨x, y⟩); ⟨x, y⟩ ∈ r^*; ⟨y, z⟩ ∈ r |] ==> P(⟨x, z⟩) |]
      ==> P(⟨a, b⟩)

lemma rtrancl_induct:

      [| ⟨a, b⟩ ∈ r^*; P(a); !!y z. [| ⟨a, y⟩ ∈ r^*; ⟨y, z⟩ ∈ r; P(y) |] ==> P(z) |]
      ==> P(b)

lemma trans_rtrancl:

      trans(r^*)

lemmas rtrancl_trans:

      [| ⟨a, b⟩ ∈ r^*; ⟨b, c⟩ ∈ r^* |] ==> ⟨a, c⟩ ∈ r^*

lemmas rtrancl_trans:

      [| ⟨a, b⟩ ∈ r^*; ⟨b, c⟩ ∈ r^* |] ==> ⟨a, c⟩ ∈ r^*

lemma rtranclE:

      [| ⟨a, b⟩ ∈ r^*; a = b ==> P; !!y. [| ⟨a, y⟩ ∈ r^*; ⟨y, b⟩ ∈ r |] ==> P |] ==> P

lemma trans_trancl:

      trans(r^+)

lemmas trans_on_trancl:

      trans[A](r1^+)

lemmas trans_on_trancl:

      trans[A](r1^+)

lemmas trancl_trans:

      [| ⟨a, b⟩ ∈ r^+; ⟨b, c⟩ ∈ r^+ |] ==> ⟨a, c⟩ ∈ r^+

lemmas trancl_trans:

      [| ⟨a, b⟩ ∈ r^+; ⟨b, c⟩ ∈ r^+ |] ==> ⟨a, c⟩ ∈ r^+

lemma trancl_into_rtrancl:

      ⟨a, b⟩ ∈ r^+ ==> ⟨a, b⟩ ∈ r^*

lemma r_into_trancl:

      ⟨a, b⟩ ∈ r ==> ⟨a, b⟩ ∈ r^+

lemma r_subset_trancl:

      relation(r) ==> r ⊆ r^+

lemma rtrancl_into_trancl1:

      [| ⟨a, b⟩ ∈ r^*; ⟨b, c⟩ ∈ r |] ==> ⟨a, c⟩ ∈ r^+

lemma rtrancl_into_trancl2:

      [| ⟨a, b⟩ ∈ r; ⟨b, c⟩ ∈ r^* |] ==> ⟨a, c⟩ ∈ r^+

lemma trancl_induct:

      [| ⟨a, b⟩ ∈ r^+; !!y. ⟨a, y⟩ ∈ r ==> P(y);
         !!y z. [| ⟨a, y⟩ ∈ r^+; ⟨y, z⟩ ∈ r; P(y) |] ==> P(z) |]
      ==> P(b)

lemma tranclE:

      [| ⟨a, b⟩ ∈ r^+; ⟨a, b⟩ ∈ r ==> P; !!y. [| ⟨a, y⟩ ∈ r^+; ⟨y, b⟩ ∈ r |] ==> P |]
      ==> P

lemma trancl_type:

      r^+ ⊆ field(r) × field(r)

lemma relation_trancl:

      relation(r^+)

lemma trancl_subset_times:

      r ⊆ A × A ==> r^+ ⊆ A × A

lemma trancl_mono:

      r ⊆ s ==> r^+ ⊆ s^+

lemma trancl_eq_r:

      [| relation(r); trans(r) |] ==> r^+ = r

lemma rtrancl_idemp:

      r^*^* = r^*

lemma rtrancl_subset:

      [| R ⊆ S; S ⊆ R^* |] ==> S^* = R^*

lemma rtrancl_Un_rtrancl:

      [| relation(r); relation(s) |] ==> (r^* ∪ s^*)^* = (r ∪ s)^*

lemma rtrancl_converseD:

      ⟨x, y⟩ ∈ converse(r)^* ==> ⟨x, y⟩ ∈ converse(r^*)

lemma rtrancl_converseI:

      ⟨x, y⟩ ∈ converse(r^*) ==> ⟨x, y⟩ ∈ converse(r)^*

lemma rtrancl_converse:

      converse(r)^* = converse(r^*)

lemma trancl_converseD:

      ⟨a, b⟩ ∈ converse(r)^+ ==> ⟨a, b⟩ ∈ converse(r^+)

lemma trancl_converseI:

      ⟨x, y⟩ ∈ converse(r^+) ==> ⟨x, y⟩ ∈ converse(r)^+

lemma trancl_converse:

      converse(r)^+ = converse(r^+)

lemma converse_trancl_induct:

      [| ⟨a, b⟩ ∈ r^+; !!y. ⟨y, b⟩ ∈ r ==> P(y);
         !!y z. [| ⟨y, z⟩ ∈ r; ⟨z, b⟩ ∈ r^+; P(z) |] ==> P(y) |]
      ==> P(a)