# Theory Transitive_Closure

Up to index of Isabelle/HOL-Proofs

theory Transitive_Closure
imports Relation
(*  Title:      HOL/Transitive_Closure.thy    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1992  University of Cambridge*)header {* Reflexive and Transitive closure of a relation *}theory Transitive_Closureimports RelationbeginML_file "~~/src/Provers/trancl.ML"text {*  @{text rtrancl} is reflexive/transitive closure,  @{text trancl} is transitive closure,  @{text reflcl} is reflexive closure.  These postfix operators have \emph{maximum priority}, forcing their  operands to be atomic.*}inductive_set  rtrancl :: "('a × 'a) set => ('a × 'a) set"   ("(_^*)" [1000] 999)  for r :: "('a × 'a) set"where    rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) : r^*"  | rtrancl_into_rtrancl [Pure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"inductive_set  trancl :: "('a × 'a) set => ('a × 'a) set"  ("(_^+)" [1000] 999)  for r :: "('a × 'a) set"where    r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"  | trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+"declare rtrancl_def [nitpick_unfold del]        rtranclp_def [nitpick_unfold del]        trancl_def [nitpick_unfold del]        tranclp_def [nitpick_unfold del]notation  rtranclp  ("(_^**)" [1000] 1000) and  tranclp  ("(_^++)" [1000] 1000)abbreviation  reflclp :: "('a => 'a => bool) => 'a => 'a => bool"  ("(_^==)" [1000] 1000) where  "r^== ≡ sup r op ="abbreviation  reflcl :: "('a × 'a) set => ('a × 'a) set"  ("(_^=)" [1000] 999) where  "r^= ≡ r ∪ Id"notation (xsymbols)  rtranclp  ("(_⇧*⇧*)" [1000] 1000) and  tranclp  ("(_⇧+⇧+)" [1000] 1000) and  reflclp  ("(_⇧=⇧=)" [1000] 1000) and  rtrancl  ("(_⇧*)" [1000] 999) and  trancl  ("(_⇧+)" [1000] 999) and  reflcl  ("(_⇧=)" [1000] 999)notation (HTML output)  rtranclp  ("(_⇧*⇧*)" [1000] 1000) and  tranclp  ("(_⇧+⇧+)" [1000] 1000) and  reflclp  ("(_⇧=⇧=)" [1000] 1000) and  rtrancl  ("(_⇧*)" [1000] 999) and  trancl  ("(_⇧+)" [1000] 999) and  reflcl  ("(_⇧=)" [1000] 999)subsection {* Reflexive closure *}lemma refl_reflcl[simp]: "refl(r^=)"by(simp add:refl_on_def)lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"by(simp add:antisym_def)lemma trans_reflclI[simp]: "trans r ==> trans(r^=)"unfolding trans_def by blastlemma reflclp_idemp [simp]: "(P^==)^==  =  P^=="by blastsubsection {* Reflexive-transitive closure *}lemma reflcl_set_eq [pred_set_conv]: "(sup (λx y. (x, y) ∈ r) op =) = (λx y. (x, y) ∈ r ∪ Id)"  by (auto simp add: fun_eq_iff)lemma r_into_rtrancl [intro]: "!!p. p ∈ r ==> p ∈ r^*"  -- {* @{text rtrancl} of @{text r} contains @{text r} *}  apply (simp only: split_tupled_all)  apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])  donelemma r_into_rtranclp [intro]: "r x y ==> r^** x y"  -- {* @{text rtrancl} of @{text r} contains @{text r} *}  by (erule rtranclp.rtrancl_refl [THEN rtranclp.rtrancl_into_rtrancl])lemma rtranclp_mono: "r ≤ s ==> r^** ≤ s^**"  -- {* monotonicity of @{text rtrancl} *}  apply (rule predicate2I)  apply (erule rtranclp.induct)   apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+)  donelemmas rtrancl_mono = rtranclp_mono [to_set]theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]:  assumes a: "r^** a b"    and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z"  shows "P b" using a  by (induct x≡a b) (rule cases)+lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set]lemmas rtranclp_induct2 =  rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule,                 consumes 1, case_names refl step]lemmas rtrancl_induct2 =  rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),                 consumes 1, case_names refl step]lemma refl_rtrancl: "refl (r^*)"by (unfold refl_on_def) fasttext {* Transitivity of transitive closure. *}lemma trans_rtrancl: "trans (r^*)"proof (rule transI)  fix x y z  assume "(x, y) ∈ r⇧*"  assume "(y, z) ∈ r⇧*"  then show "(x, z) ∈ r⇧*"  proof induct    case base    show "(x, y) ∈ r⇧*" by fact  next    case (step u v)    from (x, u) ∈ r⇧* and (u, v) ∈ r    show "(x, v) ∈ r⇧*" ..  qedqedlemmas rtrancl_trans = trans_rtrancl [THEN transD]lemma rtranclp_trans:  assumes xy: "r^** x y"  and yz: "r^** y z"  shows "r^** x z" using yz xy  by induct iprover+lemma rtranclE [cases set: rtrancl]:  assumes major: "(a::'a, b) : r^*"  obtains    (base) "a = b"  | (step) y where "(a, y) : r^*" and "(y, b) : r"  -- {* elimination of @{text rtrancl} -- by induction on a special formula *}  apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")   apply (rule_tac [2] major [THEN rtrancl_induct])    prefer 2 apply blast   prefer 2 apply blast  apply (erule asm_rl exE disjE conjE base step)+  donelemma rtrancl_Int_subset: "[| Id ⊆ s; (r^* ∩ s) O r ⊆ s|] ==> r^* ⊆ s"  apply (rule subsetI)  apply (rule_tac p="x" in PairE, clarify)  apply (erule rtrancl_induct, auto)   donelemma converse_rtranclp_into_rtranclp:  "r a b ==> r⇧*⇧* b c ==> r⇧*⇧* a c"  by (rule rtranclp_trans) iprover+lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set]text {*  \medskip More @{term "r^*"} equations and inclusions.*}lemma rtranclp_idemp [simp]: "(r^**)^** = r^**"  apply (auto intro!: order_antisym)  apply (erule rtranclp_induct)   apply (rule rtranclp.rtrancl_refl)  apply (blast intro: rtranclp_trans)  donelemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set]lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*"  apply (rule set_eqI)  apply (simp only: split_tupled_all)  apply (blast intro: rtrancl_trans)  donelemma rtrancl_subset_rtrancl: "r ⊆ s^* ==> r^* ⊆ s^*"  apply (drule rtrancl_mono)  apply simp  donelemma rtranclp_subset: "R ≤ S ==> S ≤ R^** ==> S^** = R^**"  apply (drule rtranclp_mono)  apply (drule rtranclp_mono)  apply simp  donelemmas rtrancl_subset = rtranclp_subset [to_set]lemma rtranclp_sup_rtranclp: "(sup (R^**) (S^**))^** = (sup R S)^**"by (blast intro!: rtranclp_subset intro: rtranclp_mono [THEN predicate2D])lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set]lemma rtranclp_reflclp [simp]: "(R^==)^** = R^**"by (blast intro!: rtranclp_subset)lemmas rtrancl_reflcl [simp] = rtranclp_reflclp [to_set]lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*"  apply (rule sym)  apply (rule rtrancl_subset, blast, clarify)  apply (rename_tac a b)  apply (case_tac "a = b")   apply blast  apply blast  donelemma rtranclp_r_diff_Id: "(inf r op ~=)^** = r^**"  apply (rule sym)  apply (rule rtranclp_subset)   apply blast+  donetheorem rtranclp_converseD:  assumes r: "(r^--1)^** x y"  shows "r^** y x"proof -  from r show ?thesis    by induct (iprover intro: rtranclp_trans dest!: conversepD)+qedlemmas rtrancl_converseD = rtranclp_converseD [to_set]theorem rtranclp_converseI:  assumes "r^** y x"  shows "(r^--1)^** x y"  using assms  by induct (iprover intro: rtranclp_trans conversepI)+lemmas rtrancl_converseI = rtranclp_converseI [to_set]lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"  by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)lemma sym_rtrancl: "sym r ==> sym (r^*)"  by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric])theorem converse_rtranclp_induct [consumes 1, case_names base step]:  assumes major: "r^** a b"    and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y"  shows "P a"  using rtranclp_converseI [OF major]  by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set]lemmas converse_rtranclp_induct2 =  converse_rtranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule,                 consumes 1, case_names refl step]lemmas converse_rtrancl_induct2 =  converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),                 consumes 1, case_names refl step]lemma converse_rtranclpE [consumes 1, case_names base step]:  assumes major: "r^** x z"    and cases: "x=z ==> P"      "!!y. [| r x y; r^** y z |] ==> P"  shows P  apply (subgoal_tac "x = z | (EX y. r x y & r^** y z)")   apply (rule_tac [2] major [THEN converse_rtranclp_induct])    prefer 2 apply iprover   prefer 2 apply iprover  apply (erule asm_rl exE disjE conjE cases)+  donelemmas converse_rtranclE = converse_rtranclpE [to_set]lemmas converse_rtranclpE2 = converse_rtranclpE [of _ "(xa,xb)" "(za,zb)", split_rule]lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule]lemma r_comp_rtrancl_eq: "r O r^* = r^* O r"  by (blast elim: rtranclE converse_rtranclE    intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)lemma rtrancl_unfold: "r^* = Id Un r^* O r"  by (auto intro: rtrancl_into_rtrancl elim: rtranclE)lemma rtrancl_Un_separatorE:  "(a,b) : (P ∪ Q)^* ==> ∀x y. (a,x) : P^* --> (x,y) : Q --> x=y ==> (a,b) : P^*"apply (induct rule:rtrancl.induct) apply blastapply (blast intro:rtrancl_trans)donelemma rtrancl_Un_separator_converseE:  "(a,b) : (P ∪ Q)^* ==> ∀x y. (x,b) : P^* --> (y,x) : Q --> y=x ==> (a,b) : P^*"apply (induct rule:converse_rtrancl_induct) apply blastapply (blast intro:rtrancl_trans)donelemma Image_closed_trancl:  assumes "r  X ⊆ X" shows "r⇧*  X = X"proof -  from assms have **: "{y. ∃x∈X. (x, y) ∈ r} ⊆ X" by auto  have "!!x y. (y, x) ∈ r⇧* ==> y ∈ X ==> x ∈ X"  proof -    fix x y    assume *: "y ∈ X"    assume "(y, x) ∈ r⇧*"    then show "x ∈ X"    proof induct      case base show ?case by (fact *)    next      case step with ** show ?case by auto    qed  qed  then show ?thesis by autoqedsubsection {* Transitive closure *}lemma trancl_mono: "!!p. p ∈ r^+ ==> r ⊆ s ==> p ∈ s^+"  apply (simp add: split_tupled_all)  apply (erule trancl.induct)   apply (iprover dest: subsetD)+  donelemma r_into_trancl': "!!p. p : r ==> p : r^+"  by (simp only: split_tupled_all) (erule r_into_trancl)text {*  \medskip Conversions between @{text trancl} and @{text rtrancl}.*}lemma tranclp_into_rtranclp: "r^++ a b ==> r^** a b"  by (erule tranclp.induct) iprover+lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set]lemma rtranclp_into_tranclp1: assumes r: "r^** a b"  shows "!!c. r b c ==> r^++ a c" using r  by induct iprover+lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set]lemma rtranclp_into_tranclp2: "[| r a b; r^** b c |] ==> r^++ a c"  -- {* intro rule from @{text r} and @{text rtrancl} *}  apply (erule rtranclp.cases)   apply iprover  apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1])    apply (simp | rule r_into_rtranclp)+  donelemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set]text {* Nice induction rule for @{text trancl} *}lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]:  assumes a: "r^++ a b"  and cases: "!!y. r a y ==> P y"    "!!y z. r^++ a y ==> r y z ==> P y ==> P z"  shows "P b" using a  by (induct x≡a b) (iprover intro: cases)+lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set]lemmas tranclp_induct2 =  tranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule,    consumes 1, case_names base step]lemmas trancl_induct2 =  trancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),    consumes 1, case_names base step]lemma tranclp_trans_induct:  assumes major: "r^++ x y"    and cases: "!!x y. r x y ==> P x y"      "!!x y z. [| r^++ x y; P x y; r^++ y z; P y z |] ==> P x z"  shows "P x y"  -- {* Another induction rule for trancl, incorporating transitivity *}  by (iprover intro: major [THEN tranclp_induct] cases)lemmas trancl_trans_induct = tranclp_trans_induct [to_set]lemma tranclE [cases set: trancl]:  assumes "(a, b) : r^+"  obtains    (base) "(a, b) : r"  | (step) c where "(a, c) : r^+" and "(c, b) : r"  using assms by cases simp_alllemma trancl_Int_subset: "[| r ⊆ s; (r^+ ∩ s) O r ⊆ s|] ==> r^+ ⊆ s"  apply (rule subsetI)  apply (rule_tac p = x in PairE)  apply clarify  apply (erule trancl_induct)   apply auto  donelemma trancl_unfold: "r^+ = r Un r^+ O r"  by (auto intro: trancl_into_trancl elim: tranclE)text {* Transitivity of @{term "r^+"} *}lemma trans_trancl [simp]: "trans (r^+)"proof (rule transI)  fix x y z  assume "(x, y) ∈ r^+"  assume "(y, z) ∈ r^+"  then show "(x, z) ∈ r^+"  proof induct    case (base u)    from (x, y) ∈ r^+ and (y, u) ∈ r    show "(x, u) ∈ r^+" ..  next    case (step u v)    from (x, u) ∈ r^+ and (u, v) ∈ r    show "(x, v) ∈ r^+" ..  qedqedlemmas trancl_trans = trans_trancl [THEN transD]lemma tranclp_trans:  assumes xy: "r^++ x y"  and yz: "r^++ y z"  shows "r^++ x z" using yz xy  by induct iprover+lemma trancl_id [simp]: "trans r ==> r^+ = r"  apply auto  apply (erule trancl_induct)   apply assumption  apply (unfold trans_def)  apply blast  donelemma rtranclp_tranclp_tranclp:  assumes "r^** x y"  shows "!!z. r^++ y z ==> r^++ x z" using assms  by induct (iprover intro: tranclp_trans)+lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set]lemma tranclp_into_tranclp2: "r a b ==> r^++ b c ==> r^++ a c"  by (erule tranclp_trans [OF tranclp.r_into_trancl])lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set]lemma trancl_insert:  "(insert (y, x) r)^+ = r^+ ∪ {(a, b). (a, y) ∈ r^* ∧ (x, b) ∈ r^*}"  -- {* primitive recursion for @{text trancl} over finite relations *}  apply (rule equalityI)   apply (rule subsetI)   apply (simp only: split_tupled_all)   apply (erule trancl_induct, blast)   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)  apply (rule subsetI)  apply (blast intro: trancl_mono rtrancl_mono    [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)  donelemma tranclp_converseI: "(r^++)^--1 x y ==> (r^--1)^++ x y"  apply (drule conversepD)  apply (erule tranclp_induct)  apply (iprover intro: conversepI tranclp_trans)+  donelemmas trancl_converseI = tranclp_converseI [to_set]lemma tranclp_converseD: "(r^--1)^++ x y ==> (r^++)^--1 x y"  apply (rule conversepI)  apply (erule tranclp_induct)  apply (iprover dest: conversepD intro: tranclp_trans)+  donelemmas trancl_converseD = tranclp_converseD [to_set]lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1"  by (fastforce simp add: fun_eq_iff    intro!: tranclp_converseI dest!: tranclp_converseD)lemmas trancl_converse = tranclp_converse [to_set]lemma sym_trancl: "sym r ==> sym (r^+)"  by (simp only: sym_conv_converse_eq trancl_converse [symmetric])lemma converse_tranclp_induct [consumes 1, case_names base step]:  assumes major: "r^++ a b"    and cases: "!!y. r y b ==> P(y)"      "!!y z.[| r y z;  r^++ z b;  P(z) |] ==> P(y)"  shows "P a"  apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major])   apply (rule cases)   apply (erule conversepD)  apply (blast intro: assms dest!: tranclp_converseD)  donelemmas converse_trancl_induct = converse_tranclp_induct [to_set]lemma tranclpD: "R^++ x y ==> EX z. R x z ∧ R^** z y"  apply (erule converse_tranclp_induct)   apply auto  apply (blast intro: rtranclp_trans)  donelemmas tranclD = tranclpD [to_set]lemma converse_tranclpE:  assumes major: "tranclp r x z"  assumes base: "r x z ==> P"  assumes step: "!! y. [| r x y; tranclp r y z |] ==> P"  shows Pproof -  from tranclpD[OF major]  obtain y where "r x y" and "rtranclp r y z" by iprover  from this(2) show P  proof (cases rule: rtranclp.cases)    case rtrancl_refl    with r x y base show P by iprover  next    case rtrancl_into_rtrancl    from this have "tranclp r y z"      by (iprover intro: rtranclp_into_tranclp1)    with r x y step show P by iprover  qedqedlemmas converse_tranclE = converse_tranclpE [to_set]lemma tranclD2:  "(x, y) ∈ R⇧+ ==> ∃z. (x, z) ∈ R⇧* ∧ (z, y) ∈ R"  by (blast elim: tranclE intro: trancl_into_rtrancl)lemma irrefl_tranclI: "r^-1 ∩ r^* = {} ==> (x, x) ∉ r^+"  by (blast elim: tranclE dest: trancl_into_rtrancl)lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) ∉ r^+ ==> (x, y) ∈ r ==> x ≠ y"  by (blast dest: r_into_trancl)lemma trancl_subset_Sigma_aux:    "(a, b) ∈ r^* ==> r ⊆ A × A ==> a = b ∨ a ∈ A"  by (induct rule: rtrancl_induct) autolemma trancl_subset_Sigma: "r ⊆ A × A ==> r^+ ⊆ A × A"  apply (rule subsetI)  apply (simp only: split_tupled_all)  apply (erule tranclE)   apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+  donelemma reflclp_tranclp [simp]: "(r^++)^== = r^**"  apply (safe intro!: order_antisym)   apply (erule tranclp_into_rtranclp)  apply (blast elim: rtranclp.cases dest: rtranclp_into_tranclp1)  donelemmas reflcl_trancl [simp] = reflclp_tranclp [to_set]lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"  apply safe   apply (drule trancl_into_rtrancl, simp)  apply (erule rtranclE, safe)   apply (rule r_into_trancl, simp)  apply (rule rtrancl_into_trancl1)   apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast)  donelemma rtrancl_trancl_reflcl [code]: "r^* = (r^+)^="  by simplemma trancl_empty [simp]: "{}^+ = {}"  by (auto elim: trancl_induct)lemma rtrancl_empty [simp]: "{}^* = Id"  by (rule subst [OF reflcl_trancl]) simplemma rtranclpD: "R^** a b ==> a = b ∨ a ≠ b ∧ R^++ a b"by (force simp add: reflclp_tranclp [symmetric] simp del: reflclp_tranclp)lemmas rtranclD = rtranclpD [to_set]lemma rtrancl_eq_or_trancl:  "(x,y) ∈ R⇧* = (x=y ∨ x≠y ∧ (x,y) ∈ R⇧+)"  by (fast elim: trancl_into_rtrancl dest: rtranclD)lemma trancl_unfold_right: "r^+ = r^* O r"by (auto dest: tranclD2 intro: rtrancl_into_trancl1)lemma trancl_unfold_left: "r^+ = r O r^*"by (auto dest: tranclD intro: rtrancl_into_trancl2)text {* Simplifying nested closures *}lemma rtrancl_trancl_absorb[simp]: "(R^*)^+ = R^*"by (simp add: trans_rtrancl)lemma trancl_rtrancl_absorb[simp]: "(R^+)^* = R^*"by (subst reflcl_trancl[symmetric]) simplemma rtrancl_reflcl_absorb[simp]: "(R^*)^= = R^*"by autotext {* @{text Domain} and @{text Range} *}lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"  by blastlemma Range_rtrancl [simp]: "Range (R^*) = UNIV"  by blastlemma rtrancl_Un_subset: "(R^* ∪ S^*) ⊆ (R Un S)^*"  by (rule rtrancl_Un_rtrancl [THEN subst]) fastlemma in_rtrancl_UnI: "x ∈ R^* ∨ x ∈ S^* ==> x ∈ (R ∪ S)^*"  by (blast intro: subsetD [OF rtrancl_Un_subset])lemma trancl_domain [simp]: "Domain (r^+) = Domain r"  by (unfold Domain_unfold) (blast dest: tranclD)lemma trancl_range [simp]: "Range (r^+) = Range r"  unfolding Domain_converse [symmetric] by (simp add: trancl_converse [symmetric])lemma Not_Domain_rtrancl:    "x ~: Domain R ==> ((x, y) : R^*) = (x = y)"  apply auto  apply (erule rev_mp)  apply (erule rtrancl_induct)   apply auto  donelemma trancl_subset_Field2: "r^+ <= Field r × Field r"  apply clarify  apply (erule trancl_induct)   apply (auto simp add: Field_def)  donelemma finite_trancl[simp]: "finite (r^+) = finite r"  apply auto   prefer 2   apply (rule trancl_subset_Field2 [THEN finite_subset])   apply (rule finite_SigmaI)    prefer 3    apply (blast intro: r_into_trancl' finite_subset)   apply (auto simp add: finite_Field)  donetext {* More about converse @{text rtrancl} and @{text trancl}, should  be merged with main body. *}lemma single_valued_confluent:  "[| single_valued r; (x,y) ∈ r^*; (x,z) ∈ r^* |]  ==> (y,z) ∈ r^* ∨ (z,y) ∈ r^*"  apply (erule rtrancl_induct)  apply simp  apply (erule disjE)   apply (blast elim:converse_rtranclE dest:single_valuedD)  apply(blast intro:rtrancl_trans)  donelemma r_r_into_trancl: "(a, b) ∈ R ==> (b, c) ∈ R ==> (a, c) ∈ R^+"  by (fast intro: trancl_trans)lemma trancl_into_trancl [rule_format]:    "(a, b) ∈ r⇧+ ==> (b, c) ∈ r --> (a,c) ∈ r⇧+"  apply (erule trancl_induct)   apply (fast intro: r_r_into_trancl)  apply (fast intro: r_r_into_trancl trancl_trans)  donelemma tranclp_rtranclp_tranclp:    "r⇧+⇧+ a b ==> r⇧*⇧* b c ==> r⇧+⇧+ a c"  apply (drule tranclpD)  apply (elim exE conjE)  apply (drule rtranclp_trans, assumption)  apply (drule rtranclp_into_tranclp2, assumption, assumption)  donelemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set]lemmas transitive_closure_trans [trans] =  r_r_into_trancl trancl_trans rtrancl_trans  trancl.trancl_into_trancl trancl_into_trancl2  rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl  rtrancl_trancl_trancl trancl_rtrancl_trancllemmas transitive_closurep_trans' [trans] =  tranclp_trans rtranclp_trans  tranclp.trancl_into_trancl tranclp_into_tranclp2  rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp  rtranclp_tranclp_tranclp tranclp_rtranclp_tranclpdeclare trancl_into_rtrancl [elim]subsection {* The power operation on relations *}text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *}overloading  relpow == "compow :: nat => ('a × 'a) set => ('a × 'a) set"  relpowp == "compow :: nat => ('a => 'a => bool) => ('a => 'a => bool)"beginprimrec relpow :: "nat => ('a × 'a) set => ('a × 'a) set" where    "relpow 0 R = Id"  | "relpow (Suc n) R = (R ^^ n) O R"primrec relpowp :: "nat => ('a => 'a => bool) => ('a => 'a => bool)" where    "relpowp 0 R = HOL.eq"  | "relpowp (Suc n) R = (R ^^ n) OO R"endlemma relpowp_relpow_eq [pred_set_conv]:  fixes R :: "'a rel"  shows "(λx y. (x, y) ∈ R) ^^ n = (λx y. (x, y) ∈ R ^^ n)"  by (induct n) (simp_all add: relcompp_relcomp_eq)text {* for code generation *}definition relpow :: "nat => ('a × 'a) set => ('a × 'a) set" where  relpow_code_def [code_abbrev]: "relpow = compow"definition relpowp :: "nat => ('a => 'a => bool) => ('a => 'a => bool)" where  relpowp_code_def [code_abbrev]: "relpowp = compow"lemma [code]:  "relpow (Suc n) R = (relpow n R) O R"  "relpow 0 R = Id"  by (simp_all add: relpow_code_def)lemma [code]:  "relpowp (Suc n) R = (R ^^ n) OO R"  "relpowp 0 R = HOL.eq"  by (simp_all add: relpowp_code_def)hide_const (open) relpowhide_const (open) relpowplemma relpow_1 [simp]:  fixes R :: "('a × 'a) set"  shows "R ^^ 1 = R"  by simplemma relpowp_1 [simp]:  fixes P :: "'a => 'a => bool"  shows "P ^^ 1 = P"  by (fact relpow_1 [to_pred])lemma relpow_0_I:   "(x, x) ∈ R ^^ 0"  by simplemma relpowp_0_I:  "(P ^^ 0) x x"  by (fact relpow_0_I [to_pred])lemma relpow_Suc_I:  "(x, y) ∈  R ^^ n ==> (y, z) ∈ R ==> (x, z) ∈ R ^^ Suc n"  by autolemma relpowp_Suc_I:  "(P ^^ n) x y ==> P y z ==> (P ^^ Suc n) x z"  by (fact relpow_Suc_I [to_pred])lemma relpow_Suc_I2:  "(x, y) ∈ R ==> (y, z) ∈ R ^^ n ==> (x, z) ∈ R ^^ Suc n"  by (induct n arbitrary: z) (simp, fastforce)lemma relpowp_Suc_I2:  "P x y ==> (P ^^ n) y z ==> (P ^^ Suc n) x z"  by (fact relpow_Suc_I2 [to_pred])lemma relpow_0_E:  "(x, y) ∈ R ^^ 0 ==> (x = y ==> P) ==> P"  by simplemma relpowp_0_E:  "(P ^^ 0) x y ==> (x = y ==> Q) ==> Q"  by (fact relpow_0_E [to_pred])lemma relpow_Suc_E:  "(x, z) ∈ R ^^ Suc n ==> (!!y. (x, y) ∈ R ^^ n ==> (y, z) ∈ R ==> P) ==> P"  by autolemma relpowp_Suc_E:  "(P ^^ Suc n) x z ==> (!!y. (P ^^ n) x y ==> P y z ==> Q) ==> Q"  by (fact relpow_Suc_E [to_pred])lemma relpow_E:  "(x, z) ∈  R ^^ n ==>  (n = 0 ==> x = z ==> P)   ==> (!!y m. n = Suc m ==> (x, y) ∈  R ^^ m ==> (y, z) ∈ R ==> P)   ==> P"  by (cases n) autolemma relpowp_E:  "(P ^^ n) x z ==> (n = 0 ==> x = z ==> Q)  ==> (!!y m. n = Suc m ==> (P ^^ m) x y ==> P y z ==> Q)  ==> Q"  by (fact relpow_E [to_pred])lemma relpow_Suc_D2:  "(x, z) ∈ R ^^ Suc n ==> (∃y. (x, y) ∈ R ∧ (y, z) ∈ R ^^ n)"  apply (induct n arbitrary: x z)   apply (blast intro: relpow_0_I elim: relpow_0_E relpow_Suc_E)  apply (blast intro: relpow_Suc_I elim: relpow_0_E relpow_Suc_E)  donelemma relpowp_Suc_D2:  "(P ^^ Suc n) x z ==> ∃y. P x y ∧ (P ^^ n) y z"  by (fact relpow_Suc_D2 [to_pred])lemma relpow_Suc_E2:  "(x, z) ∈ R ^^ Suc n ==> (!!y. (x, y) ∈ R ==> (y, z) ∈ R ^^ n ==> P) ==> P"  by (blast dest: relpow_Suc_D2)lemma relpowp_Suc_E2:  "(P ^^ Suc n) x z ==> (!!y. P x y ==> (P ^^ n) y z ==> Q) ==> Q"  by (fact relpow_Suc_E2 [to_pred])lemma relpow_Suc_D2':  "∀x y z. (x, y) ∈ R ^^ n ∧ (y, z) ∈ R --> (∃w. (x, w) ∈ R ∧ (w, z) ∈ R ^^ n)"  by (induct n) (simp_all, blast)lemma relpowp_Suc_D2':  "∀x y z. (P ^^ n) x y ∧ P y z --> (∃w. P x w ∧ (P ^^ n) w z)"  by (fact relpow_Suc_D2' [to_pred])lemma relpow_E2:  "(x, z) ∈ R ^^ n ==>  (n = 0 ==> x = z ==> P)     ==> (!!y m. n = Suc m ==> (x, y) ∈ R ==> (y, z) ∈ R ^^ m ==> P)   ==> P"  apply (cases n, simp)  apply (cut_tac n=nat and R=R in relpow_Suc_D2', simp, blast)  donelemma relpowp_E2:  "(P ^^ n) x z ==> (n = 0 ==> x = z ==> Q)    ==> (!!y m. n = Suc m ==> P x y ==> (P ^^ m) y z ==> Q)  ==> Q"  by (fact relpow_E2 [to_pred])lemma relpow_add: "R ^^ (m+n) = R^^m O R^^n"  by (induct n) autolemma relpowp_add: "P ^^ (m + n) = P ^^ m OO P ^^ n"  by (fact relpow_add [to_pred])lemma relpow_commute: "R O R ^^ n = R ^^ n O R"  by (induct n) (simp, simp add: O_assoc [symmetric])lemma relpowp_commute: "P OO P ^^ n = P ^^ n OO P"  by (fact relpow_commute [to_pred])lemma relpow_empty:  "0 < n ==> ({} :: ('a × 'a) set) ^^ n = {}"  by (cases n) autolemma relpowp_bot:  "0 < n ==> (⊥ :: 'a => 'a => bool) ^^ n = ⊥"  by (fact relpow_empty [to_pred])lemma rtrancl_imp_UN_relpow:  assumes "p ∈ R^*"  shows "p ∈ (\<Union>n. R ^^ n)"proof (cases p)  case (Pair x y)  with assms have "(x, y) ∈ R^*" by simp  then have "(x, y) ∈ (\<Union>n. R ^^ n)" proof induct    case base show ?case by (blast intro: relpow_0_I)  next    case step then show ?case by (blast intro: relpow_Suc_I)  qed  with Pair show ?thesis by simpqedlemma rtranclp_imp_Sup_relpowp:  assumes "(P^**) x y"  shows "(\<Squnion>n. P ^^ n) x y"  using assms and rtrancl_imp_UN_relpow [to_pred] by blastlemma relpow_imp_rtrancl:  assumes "p ∈ R ^^ n"  shows "p ∈ R^*"proof (cases p)  case (Pair x y)  with assms have "(x, y) ∈ R ^^ n" by simp  then have "(x, y) ∈ R^*" proof (induct n arbitrary: x y)    case 0 then show ?case by simp  next    case Suc then show ?case      by (blast elim: relpow_Suc_E intro: rtrancl_into_rtrancl)  qed  with Pair show ?thesis by simpqedlemma relpowp_imp_rtranclp:  assumes "(P ^^ n) x y"  shows "(P^**) x y"  using assms and relpow_imp_rtrancl [to_pred] by blastlemma rtrancl_is_UN_relpow:  "R^* = (\<Union>n. R ^^ n)"  by (blast intro: rtrancl_imp_UN_relpow relpow_imp_rtrancl)lemma rtranclp_is_Sup_relpowp:  "P^** = (\<Squnion>n. P ^^ n)"  using rtrancl_is_UN_relpow [to_pred, of P] by autolemma rtrancl_power:  "p ∈ R^* <-> (∃n. p ∈ R ^^ n)"  by (simp add: rtrancl_is_UN_relpow)lemma rtranclp_power:  "(P^**) x y <-> (∃n. (P ^^ n) x y)"  by (simp add: rtranclp_is_Sup_relpowp)lemma trancl_power:  "p ∈ R^+ <-> (∃n > 0. p ∈ R ^^ n)"  apply (cases p)  apply simp  apply (rule iffI)   apply (drule tranclD2)   apply (clarsimp simp: rtrancl_is_UN_relpow)   apply (rule_tac x="Suc n" in exI)   apply (clarsimp simp: relcomp_unfold)   apply fastforce  apply clarsimp  apply (case_tac n, simp)  apply clarsimp  apply (drule relpow_imp_rtrancl)  apply (drule rtrancl_into_trancl1) apply auto  donelemma tranclp_power:  "(P^++) x y <-> (∃n > 0. (P ^^ n) x y)"  using trancl_power [to_pred, of P "(x, y)"] by simplemma rtrancl_imp_relpow:  "p ∈ R^* ==> ∃n. p ∈ R ^^ n"  by (auto dest: rtrancl_imp_UN_relpow)lemma rtranclp_imp_relpowp:  "(P^**) x y ==> ∃n. (P ^^ n) x y"  by (auto dest: rtranclp_imp_Sup_relpowp)text{* By Sternagel/Thiemann: *}lemma relpow_fun_conv:  "((a,b) ∈ R ^^ n) = (∃f. f 0 = a ∧ f n = b ∧ (∀i<n. (f i, f(Suc i)) ∈ R))"proof (induct n arbitrary: b)  case 0 show ?case by autonext  case (Suc n)  show ?case  proof (simp add: relcomp_unfold Suc)    show "(∃y. (∃f. f 0 = a ∧ f n = y ∧ (∀i<n. (f i,f(Suc i)) ∈ R)) ∧ (y,b) ∈ R)     = (∃f. f 0 = a ∧ f(Suc n) = b ∧ (∀i<Suc n. (f i, f (Suc i)) ∈ R))"    (is "?l = ?r")    proof      assume ?l      then obtain c f where 1: "f 0 = a"  "f n = c"  "!!i. i < n ==> (f i, f (Suc i)) ∈ R"  "(c,b) ∈ R" by auto      let ?g = "λ m. if m = Suc n then b else f m"      show ?r by (rule exI[of _ ?g], simp add: 1)    next      assume ?r      then obtain f where 1: "f 0 = a"  "b = f (Suc n)"  "!!i. i < Suc n ==> (f i, f (Suc i)) ∈ R" by auto      show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], insert 1, auto)    qed  qedqedlemma relpowp_fun_conv:  "(P ^^ n) x y <-> (∃f. f 0 = x ∧ f n = y ∧ (∀i<n. P (f i) (f (Suc i))))"  by (fact relpow_fun_conv [to_pred])lemma relpow_finite_bounded1:assumes "finite(R :: ('a*'a)set)" and "k>0"shows "R^^k ⊆ (UN n:{n. 0<n & n <= card R}. R^^n)" (is "_ ⊆ ?r")proof-  { fix a b k    have "(a,b) : R^^(Suc k) ==> EX n. 0<n & n <= card R & (a,b) : R^^n"    proof(induct k arbitrary: b)      case 0      hence "R ≠ {}" by auto      with card_0_eq[OF finite R] have "card R >= Suc 0" by auto      thus ?case using 0 by force    next      case (Suc k)      then obtain a' where "(a,a') : R^^(Suc k)" and "(a',b) : R" by auto      from Suc(1)[OF (a,a') : R^^(Suc k)]      obtain n where "n ≤ card R" and "(a,a') ∈ R ^^ n" by auto      have "(a,b) : R^^(Suc n)" using (a,a') ∈ R^^n and (a',b)∈ R by auto      { assume "n < card R"        hence ?case using (a,b): R^^(Suc n) Suc_leI[OF n < card R] by blast      } moreover      { assume "n = card R"        from (a,b) ∈ R ^^ (Suc n)[unfolded relpow_fun_conv]        obtain f where "f 0 = a" and "f(Suc n) = b"          and steps: "!!i. i <= n ==> (f i, f (Suc i)) ∈ R" by auto        let ?p = "%i. (f i, f(Suc i))"        let ?N = "{i. i ≤ n}"        have "?p  ?N <= R" using steps by auto        from card_mono[OF assms(1) this]        have "card(?p  ?N) <= card R" .        also have "… < card ?N" using n = card R by simp        finally have "~ inj_on ?p ?N" by(rule pigeonhole)        then obtain i j where i: "i <= n" and j: "j <= n" and ij: "i ≠ j" and          pij: "?p i = ?p j" by(auto simp: inj_on_def)        let ?i = "min i j" let ?j = "max i j"        have i: "?i <= n" and j: "?j <= n" and pij: "?p ?i = ?p ?j"           and ij: "?i < ?j"          using i j ij pij unfolding min_def max_def by auto        from i j pij ij obtain i j where i: "i<=n" and j: "j<=n" and ij: "i<j"          and pij: "?p i = ?p j" by blast        let ?g = "λ l. if l ≤ i then f l else f (l + (j - i))"        let ?n = "Suc(n - (j - i))"        have abl: "(a,b) ∈ R ^^ ?n" unfolding relpow_fun_conv        proof (rule exI[of _ ?g], intro conjI impI allI)          show "?g ?n = b" using f(Suc n) = b j ij by auto        next          fix k assume "k < ?n"          show "(?g k, ?g (Suc k)) ∈ R"          proof (cases "k < i")            case True            with i have "k <= n" by auto            from steps[OF this] show ?thesis using True by simp          next            case False            hence "i ≤ k" by auto            show ?thesis            proof (cases "k = i")              case True              thus ?thesis using ij pij steps[OF i] by simp            next              case False              with i ≤ k have "i < k" by auto              hence small: "k + (j - i) <= n" using k<?n by arith              show ?thesis using steps[OF small] i<k by auto            qed          qed        qed (simp add: f 0 = a)        moreover have "?n <= n" using i j ij by arith        ultimately have ?case using n = card R by blast      }      ultimately show ?case using n ≤ card R by force    qed  }  thus ?thesis using gr0_implies_Suc[OF k>0] by autoqedlemma relpow_finite_bounded:assumes "finite(R :: ('a*'a)set)"shows "R^^k ⊆ (UN n:{n. n <= card R}. R^^n)"apply(cases k) apply forceusing relpow_finite_bounded1[OF assms, of k] by autolemma rtrancl_finite_eq_relpow:  "finite R ==> R^* = (UN n : {n. n <= card R}. R^^n)"by(fastforce simp: rtrancl_power dest: relpow_finite_bounded)lemma trancl_finite_eq_relpow:  "finite R ==> R^+ = (UN n : {n. 0 < n & n <= card R}. R^^n)"apply(auto simp add: trancl_power)apply(auto dest: relpow_finite_bounded1)donelemma finite_relcomp[simp,intro]:assumes "finite R" and "finite S"shows "finite(R O S)"proof-  have "R O S = (UN (x,y) : R. \<Union>((%(u,v). if u=y then {(x,v)} else {})  S))"    by(force simp add: split_def)  thus ?thesis using assms by(clarsimp)qedlemma finite_relpow[simp,intro]:  assumes "finite(R :: ('a*'a)set)" shows "n>0 ==> finite(R^^n)"apply(induct n) apply simpapply(case_tac n) apply(simp_all add: assms)donelemma single_valued_relpow:  fixes R :: "('a * 'a) set"  shows "single_valued R ==> single_valued (R ^^ n)"apply (induct n arbitrary: R)apply simp_allapply (rule single_valuedI)apply (fast dest: single_valuedD elim: relpow_Suc_E)donesubsection {* Bounded transitive closure *}definition ntrancl :: "nat => ('a × 'a) set => ('a × 'a) set"where  "ntrancl n R = (\<Union>i∈{i. 0 < i ∧ i ≤ Suc n}. R ^^ i)"lemma ntrancl_Zero [simp, code]:  "ntrancl 0 R = R"proof  show "R ⊆ ntrancl 0 R"    unfolding ntrancl_def by fastforcenext  {     fix i have "0 < i ∧ i ≤ Suc 0 <-> i = 1" by auto  }  from this show "ntrancl 0 R ≤ R"    unfolding ntrancl_def by autoqedlemma ntrancl_Suc [simp]:  "ntrancl (Suc n) R = ntrancl n R O (Id ∪ R)"proof  {    fix a b    assume "(a, b) ∈ ntrancl (Suc n) R"    from this obtain i where "0 < i" "i ≤ Suc (Suc n)" "(a, b) ∈ R ^^ i"      unfolding ntrancl_def by auto    have "(a, b) ∈ ntrancl n R O (Id ∪ R)"    proof (cases "i = 1")      case True      from this (a, b) ∈ R ^^ i show ?thesis        unfolding ntrancl_def by auto    next      case False      from this 0 < i obtain j where j: "i = Suc j" "0 < j"        by (cases i) auto      from this (a, b) ∈ R ^^ i obtain c where c1: "(a, c) ∈ R ^^ j" and c2:"(c, b) ∈ R"        by auto      from c1 j i ≤ Suc (Suc n) have "(a, c) ∈ ntrancl n R"        unfolding ntrancl_def by fastforce      from this c2 show ?thesis by fastforce    qed  }  from this show "ntrancl (Suc n) R ⊆ ntrancl n R O (Id ∪ R)"    by autonext  show "ntrancl n R O (Id ∪ R) ⊆ ntrancl (Suc n) R"    unfolding ntrancl_def by fastforceqedlemma [code]:  "ntrancl (Suc n) r = (let r' = ntrancl n r in r' Un r' O r)"unfolding Let_def by autolemma finite_trancl_ntranl:  "finite R ==> trancl R = ntrancl (card R - 1) R"  by (cases "card R") (auto simp add: trancl_finite_eq_relpow relpow_empty ntrancl_def)subsection {* Acyclic relations *}definition acyclic :: "('a * 'a) set => bool" where  "acyclic r <-> (!x. (x,x) ~: r^+)"abbreviation acyclicP :: "('a => 'a => bool) => bool" where  "acyclicP r ≡ acyclic {(x, y). r x y}"lemma acyclic_irrefl [code]:  "acyclic r <-> irrefl (r^+)"  by (simp add: acyclic_def irrefl_def)lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"  by (simp add: acyclic_def)lemma acyclic_insert [iff]:     "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"apply (simp add: acyclic_def trancl_insert)apply (blast intro: rtrancl_trans)donelemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"by (simp add: acyclic_def trancl_converse)lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"apply (simp add: acyclic_def antisym_def)apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)done(* Other direction:acyclic = no loopsantisym = only self loopsGoalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)==> antisym( r^* ) = acyclic(r - Id)";*)lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"apply (simp add: acyclic_def)apply (blast intro: trancl_mono)donesubsection {* Setup of transitivity reasoner *}ML {*structure Trancl_Tac = Trancl_Tac(  val r_into_trancl = @{thm trancl.r_into_trancl};  val trancl_trans  = @{thm trancl_trans};  val rtrancl_refl = @{thm rtrancl.rtrancl_refl};  val r_into_rtrancl = @{thm r_into_rtrancl};  val trancl_into_rtrancl = @{thm trancl_into_rtrancl};  val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};  val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};  val rtrancl_trans = @{thm rtrancl_trans};  fun decomp (@{const Trueprop} $t) = let fun dec (Const (@{const_name Set.member}, _)$ (Const (@{const_name Pair}, _) $a$ b) $rel ) = let fun decr (Const ("Transitive_Closure.rtrancl", _ )$ r) = (r,"r*")              | decr (Const ("Transitive_Closure.trancl", _ ) $r) = (r,"r+") | decr r = (r,"r"); val (rel,r) = decr (Envir.beta_eta_contract rel); in SOME (a,b,rel,r) end | dec _ = NONE in dec t end | decomp _ = NONE;);structure Tranclp_Tac = Trancl_Tac( val r_into_trancl = @{thm tranclp.r_into_trancl}; val trancl_trans = @{thm tranclp_trans}; val rtrancl_refl = @{thm rtranclp.rtrancl_refl}; val r_into_rtrancl = @{thm r_into_rtranclp}; val trancl_into_rtrancl = @{thm tranclp_into_rtranclp}; val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp}; val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp}; val rtrancl_trans = @{thm rtranclp_trans}; fun decomp (@{const Trueprop}$ t) =    let fun dec (rel $a$ b) =        let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $r) = (r,"r*") | decr (Const ("Transitive_Closure.tranclp", _ )$ r)  = (r,"r+")              | decr r = (r,"r");            val (rel,r) = decr rel;        in SOME (a, b, rel, r) end      | dec _ =  NONE    in dec t end    | decomp _ = NONE;);*}setup {*  Simplifier.map_simpset_global (fn ss => ss    addSolver (mk_solver "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))    addSolver (mk_solver "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))    addSolver (mk_solver "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))    addSolver (mk_solver "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))*}text {* Optional methods. *}method_setup trancl =  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac) *}  {* simple transitivity reasoner *}method_setup rtrancl =  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac) *}  {* simple transitivity reasoner *}method_setup tranclp =  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac) *}  {* simple transitivity reasoner (predicate version) *}method_setup rtranclp =  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac) *}  {* simple transitivity reasoner (predicate version) *}end`