Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 61 kB

Quelle Transitive_Closure.thy Sprache: Isabelle

(*  Title:      HOL/Transitive_Closure.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge
*)

section \<open>Reflexive and Transitive closure of a relation\<close>

theory Transitive_Closure
  imports Finite_Set
  abbrevs "^*" = "\<^sup>*" "\<^sup>*\<^sup>*"
    and "^+" = "\<^sup>+" "\<^sup>+\<^sup>+"
    and "^=" = "\<^sup>=" "\<^sup>=\<^sup>="
begin

ML_file \<open>~~/src/Provers/trancl.ML\<close>

text \<open>
  \<open>rtrancl\<close> is reflexive/transitive closure,
  \<open>trancl\<close> is transitive closure,
  \<open>reflcl\<close> is reflexive closure.

  These postfix operators have \<^emph>\<open>maximum priority\<close>, forcing their
  operands to be atomic.
\<close>

context notes [[inductive_internals]]
begin

inductive_set rtrancl :: "('a \ 'a) set \ ('a \ 'a) set" (\(\notation=\postfix *\\_\<^sup>*)\ [1000] 999)
  for r :: "('a \ 'a) set"
  where
    rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \ r\<^sup>*"
  | rtrancl_into_rtrancl [Pure.intro]: "(a, b) \ r\<^sup>* \ (b, c) \ r \ (a, c) \ r\<^sup>*"

inductive_set trancl :: "('a \ 'a) set \ ('a \ 'a) set" (\(\notation=\postfix +\\_\<^sup>+)\ [1000] 999)
  for r :: "('a \ 'a) set"
  where
    r_into_trancl [intro, Pure.intro]: "(a, b) \ r \ (a, b) \ r\<^sup>+"
  | trancl_into_trancl [Pure.intro]: "(a, b) \ r\<^sup>+ \ (b, c) \ r \ (a, c) \ r\<^sup>+"

notation
  rtranclp  (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_\<^sup>*\<^sup>*)\<close> [1000] 1000) and
  tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_\<^sup>+\<^sup>+)\<close> [1000] 1000)

declare
  rtrancl_def [nitpick_unfold del]
  rtranclp_def [nitpick_unfold del]
  trancl_def [nitpick_unfold del]
  tranclp_def [nitpick_unfold del]

end

lemma trancl_incr: "r \ r\<^sup>+"
by auto

abbreviation reflcl :: "('a \ 'a) set \ ('a \ 'a) set" (\(\notation=\postfix =\\_\<^sup>=)\ [1000] 999)
  where "r\<^sup>= \ r \ Id"

abbreviation reflclp :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" (\(\notation=\postfix ==\\_\<^sup>=\<^sup>=)\ [1000] 1000)
  where "r\<^sup>=\<^sup>= \ sup r (=)"

notation (ASCII)
  rtrancl  (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_^*)\<close> [1000] 999) and
  trancl  (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_^+)\<close> [1000] 999) and
  reflcl  (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_^=)\<close> [1000] 999) and
  rtranclp  (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_^**)\<close> [1000] 1000) and
  tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000) and
  reflclp  (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)

bundle rtrancl_syntax
begin
notation
  rtrancl  (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_\<^sup>*)\<close> [1000] 999) and
  rtranclp  (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_\<^sup>*\<^sup>*)\<close> [1000] 1000)
notation (ASCII)
  rtrancl  (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_^*)\<close> [1000] 999) and
  rtranclp  (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_^**)\<close> [1000] 1000)
end

bundle trancl_syntax
begin
notation
  trancl  (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_\<^sup>+)\<close> [1000] 999) and
  tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_\<^sup>+\<^sup>+)\<close> [1000] 1000)
notation (ASCII)
  trancl  (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_^+)\<close> [1000] 999) and
  tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000)
end

bundle reflcl_syntax
begin
notation
  reflcl  (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_\<^sup>=)\<close> [1000] 999) and
  reflclp  (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_\<^sup>=\<^sup>=)\<close> [1000] 1000)
notation (ASCII)
  reflcl  (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_^=)\<close> [1000] 999) and
  reflclp  (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)
end

subsection \<open>Reflexive closure\<close>

lemma reflcl_set_eq [pred_set_conv]: "(sup (\x y. (x, y) \ r) (=)) = (\x y. (x, y) \ r \ Id)"
  by (auto simp: fun_eq_iff)

lemma refl_reflcl[simp]: "refl (r\<^sup>=)"
  by (simp add: refl_on_def)

lemma reflp_on_reflclp[simp]: "reflp_on A R\<^sup>=\<^sup>="
  by (simp add: reflp_on_def)

lemma antisym_on_reflcl[simp]: "antisym_on A (r\<^sup>=) \ antisym_on A r"
  by (simp add: antisym_on_def)

lemma antisymp_on_reflclp[simp]: "antisymp_on A R\<^sup>=\<^sup>= \ antisymp_on A R"
  by (rule antisym_on_reflcl[to_pred])

lemma trans_on_reflcl[simp]: "trans_on A r \ trans_on A (r\<^sup>=)"
  by (auto intro: trans_onI dest: trans_onD)

lemma transp_on_reflclp[simp]: "transp_on A R \ transp_on A R\<^sup>=\<^sup>="
  by (rule trans_on_reflcl[to_pred])

lemma antisymp_on_reflclp_if_asymp_on:
  assumes "asymp_on A R"
  shows "antisymp_on A R\<^sup>=\<^sup>="
  unfolding antisymp_on_reflclp
  using antisymp_on_if_asymp_on[OF \<open>asymp_on A R\<close>] .

lemma antisym_on_reflcl_if_asym_on: "asym_on A R \ antisym_on A (R\<^sup>=)"
  using antisymp_on_reflclp_if_asymp_on[to_set] .

lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>="
  by blast

lemma reflclp_ident_if_reflp[simp]: "reflp R \ R\<^sup>=\<^sup>= = R"
  by (auto dest: reflpD)

text \<open>The following are special cases of @{thm [source] reflclp_ident_if_reflp},
but they appear duplicated in multiple, independent theories, which causes name clashes.\<close>

lemma (in preorder) reflclp_less_eq[simp]: "(\)\<^sup>=\<^sup>= = (\)"
  using reflp_on_le by (simp only: reflclp_ident_if_reflp)

lemma (in preorder) reflclp_greater_eq[simp]: "(\)\<^sup>=\<^sup>= = (\)"
  using reflp_on_ge by (simp only: reflclp_ident_if_reflp)

lemma order_reflclp_if_transp_and_asymp:
  assumes "transp R" and "asymp R"
  shows "class.order R\<^sup>=\<^sup>= R"
proof unfold_locales
  show "\x y. R x y = (R\<^sup>=\<^sup>= x y \ \ R\<^sup>=\<^sup>= y x)"
    using \<open>asymp R\<close> asympD by fastforce
next
  show "\x. R\<^sup>=\<^sup>= x x"
    by simp
next
  show "\x y z. R\<^sup>=\<^sup>= x y \ R\<^sup>=\<^sup>= y z \ R\<^sup>=\<^sup>= x z"
    using transp_on_reflclp[OF \<open>transp R\<close>, THEN transpD] .
next
  show "\x y. R\<^sup>=\<^sup>= x y \ R\<^sup>=\<^sup>= y x \ x = y"
    using antisymp_on_reflclp_if_asymp_on[OF \<open>asymp R\<close>, THEN antisympD] .
qed

subsection \<open>Reflexive-transitive closure\<close>

lemma r_into_rtrancl [intro]: "\p. p \ r \ p \ r\<^sup>*"
  \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close>
  by (simp add: split_tupled_all rtrancl_refl [THEN rtrancl_into_rtrancl])

lemma r_into_rtranclp [intro]: "r x y \ r\<^sup>*\<^sup>* x y"
  \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close>
  by (erule rtranclp.rtrancl_refl [THEN rtranclp.rtrancl_into_rtrancl])

lemma rtranclp_mono: "r \ s \ r\<^sup>*\<^sup>* \ s\<^sup>*\<^sup>*"
  \<comment> \<open>monotonicity of \<open>rtrancl\<close>\<close>
proof (rule predicate2I)
  show "s\<^sup>*\<^sup>* x y" if "r \ s" "r\<^sup>*\<^sup>* x y" for x y
    using \<open>r\<^sup>*\<^sup>* x y\<close> \<open>r \<le> s\<close>
    by (induction rule: rtranclp.induct) (blast intro: rtranclp.rtrancl_into_rtrancl)+
qed

lemma mono_rtranclp[mono]: "(\a b. x a b \ y a b) \ x\<^sup>*\<^sup>* a b \ y\<^sup>*\<^sup>* a b"
   using rtranclp_mono[of x y] by auto

lemmas rtrancl_mono = rtranclp_mono [to_set]

theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]:
  assumes a: "r\<^sup>*\<^sup>* a b"
    and cases: "P a" "\y z. r\<^sup>*\<^sup>* a y \ r y z \ P y \ P z"
  shows "P b"
  using a by (induct x\<equiv>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\<^sup>*)"
  unfolding refl_on_def by fast

text \<open>Transitivity of transitive closure.\<close>
lemma trans_rtrancl: "trans (r\<^sup>*)"
proof (rule transI)
  fix x y z
  assume "(x, y) \ r\<^sup>*"
  assume "(y, z) \ r\<^sup>*"
  then show "(x, z) \ r\<^sup>*"
  proof induct
    case base
    show "(x, y) \ r\<^sup>*" by fact
  next
    case (step u v)
    from \<open>(x, u) \<in> r\<^sup>*\<close> and \<open>(u, v) \<in> r\<close>
    show "(x, v) \ r\<^sup>*" ..
  qed
qed

lemmas rtrancl_trans = trans_rtrancl [THEN transD]

lemma rtranclp_trans:
  assumes "r\<^sup>*\<^sup>* x y"
    and "r\<^sup>*\<^sup>* y z"
  shows "r\<^sup>*\<^sup>* x z"
  using assms(2,1) by induct iprover+

lemma rtranclE [cases set: rtrancl]:
  fixes a b :: 'a
  assumes major: "(a, b) \ r\<^sup>*"
  obtains
    (base) "a = b"
  | (step) y where "(a, y) \ r\<^sup>*" and "(y, b) \ r"
  \<comment> \<open>elimination of \<open>rtrancl\<close> -- by induction on a special formula\<close>
proof -
  have "a = b \ (\y. (a, y) \ r\<^sup>* \ (y, b) \ r)"
    by (rule major [THEN rtrancl_induct]) blast+
  then show ?thesis
    by (auto intro: base step)
qed

lemma rtrancl_Int_subset: "Id \ s \ (r\<^sup>* \ s) O r \ s \ r\<^sup>* \ s"
  by (fastforce elim: rtrancl_induct)

lemma converse_rtranclp_into_rtranclp: "r a b \ r\<^sup>*\<^sup>* b c \ r\<^sup>*\<^sup>* a c"
  by (rule rtranclp_trans) iprover+

lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set]

text \<open>\<^medskip> More \<^term>\<open>r\<^sup>*\<close> equations and inclusions.\<close>

lemma rtranclp_idemp [simp]: "(r\<^sup>*\<^sup>*)\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*"
proof -
  have "r\<^sup>*\<^sup>*\<^sup>*\<^sup>* x y \ r\<^sup>*\<^sup>* x y" for x y
    by (induction rule: rtranclp_induct) (blast intro: rtranclp_trans)+
  then show ?thesis
    by (auto intro!: order_antisym)
qed

lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set]

lemma rtrancl_idemp_self_comp [simp]: "R\<^sup>* O R\<^sup>* = R\<^sup>*"
  by (force intro: rtrancl_trans)

lemma rtrancl_subset_rtrancl: "r \ s\<^sup>* \ r\<^sup>* \ s\<^sup>*"
  by (drule rtrancl_mono, simp)

lemma rtranclp_subset: "R \ S \ S \ R\<^sup>*\<^sup>* \ S\<^sup>*\<^sup>* = R\<^sup>*\<^sup>*"
  by (fastforce dest: rtranclp_mono)

lemmas rtrancl_subset = rtranclp_subset [to_set]

lemma rtranclp_sup_rtranclp: "(sup (R\<^sup>*\<^sup>*) (S\<^sup>*\<^sup>*))\<^sup>*\<^sup>* = (sup R S)\<^sup>*\<^sup>*"
  by (blast intro!: rtranclp_subset intro: rtranclp_mono [THEN predicate2D])

lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set]

lemma rtranclp_reflclp [simp]: "(R\<^sup>=\<^sup>=)\<^sup>*\<^sup>* = R\<^sup>*\<^sup>*"
  by (blast intro!: rtranclp_subset)

lemmas rtrancl_reflcl [simp] = rtranclp_reflclp [to_set]

lemma rtrancl_r_diff_Id: "(r - Id)\<^sup>* = r\<^sup>*"
  by (rule rtrancl_subset [symmetric]) auto

lemma rtranclp_r_diff_Id: "(inf r (\))\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*"
  by (rule rtranclp_subset [symmetric]) auto

theorem rtranclp_converseD:
  assumes "(r\\)\<^sup>*\<^sup>* x y"
  shows "r\<^sup>*\<^sup>* y x"
  using assms by induct (iprover intro: rtranclp_trans dest!: conversepD)+

lemmas rtrancl_converseD = rtranclp_converseD [to_set]

theorem rtranclp_converseI:
  assumes "r\<^sup>*\<^sup>* y x"
  shows "(r\\)\<^sup>*\<^sup>* x y"
  using assms by induct (iprover intro: rtranclp_trans conversepI)+

lemmas rtrancl_converseI = rtranclp_converseI [to_set]

lemma rtrancl_converse: "(r\)\<^sup>* = (r\<^sup>*)\"
  by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)

lemma sym_rtrancl: "sym r \ sym (r\<^sup>*)"
  by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric])

theorem converse_rtranclp_induct [consumes 1, case_names base step]:
  assumes major: "r\<^sup>*\<^sup>* a b"
    and cases: "P b" "\y z. r y z \ r\<^sup>*\<^sup>* 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\<^sup>*\<^sup>* x z"
    and cases: "x = z \ P" "\y. r x y \ r\<^sup>*\<^sup>* y z \ P"
  shows P
proof -
  have "x = z \ (\y. r x y \ r\<^sup>*\<^sup>* y z)"
    by (rule major [THEN converse_rtranclp_induct]) iprover+
  then show ?thesis
    by (auto intro: cases)
qed

lemmas 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\<^sup>* = r\<^sup>* O r"
  by (blast elim: rtranclE converse_rtranclE
      intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)

lemma rtrancl_unfold: "r\<^sup>* = Id \ r\<^sup>* O r"
  by (auto intro: rtrancl_into_rtrancl elim: rtranclE)

lemma rtrancl_Un_separatorE:
  "(a, b) \ (P \ Q)\<^sup>* \ \x y. (a, x) \ P\<^sup>* \ (x, y) \ Q \ x = y \ (a, b) \ P\<^sup>*"
proof (induct rule: rtrancl.induct)
  case rtrancl_refl
  then show ?case by blast
next
  case rtrancl_into_rtrancl
  then show ?case by (blast intro: rtrancl_trans)
qed

lemma rtrancl_Un_separator_converseE:
  "(a, b) \ (P \ Q)\<^sup>* \ \x y. (x, b) \ P\<^sup>* \ (y, x) \ Q \ y = x \ (a, b) \ P\<^sup>*"
proof (induct rule: converse_rtrancl_induct)
  case base
  then show ?case by blast
next
  case step
  then show ?case by (blast intro: rtrancl_trans)
qed

lemma Image_closed_trancl:
  assumes "r `` X \ X"
  shows "r\<^sup>* `` X = X"
proof -
  from assms have **: "{y. \x\X. (x, y) \ r} \ X"
    by auto
  have "x \ X" if 1: "(y, x) \ r\<^sup>*" and 2: "y \ X" for x y
  proof -
    from 1 show "x \ X"
    proof induct
      case base
      show ?case by (fact 2)
    next
      case step
      with ** show ?case by auto
    qed
  qed
  then show ?thesis by auto
qed

lemma rtranclp_ident_if_reflp_and_transp:
  assumes "reflp R" and "transp R"
  shows "R\<^sup>*\<^sup>* = R"
proof (intro ext iffI)
  fix x y
  show "R\<^sup>*\<^sup>* x y \ R x y"
  proof (induction y rule: rtranclp_induct)
    case base
    show ?case
      using \<open>reflp R\<close>[THEN reflpD] .
  next
    case (step y z)
    thus ?case
      using \<open>transp R\<close>[THEN transpD, of x y  z] by simp
  qed
next
  fix x y
  show "R x y \ R\<^sup>*\<^sup>* x y"
    using r_into_rtranclp .
qed

text \<open>The following are special cases of @{thm [source] rtranclp_ident_if_reflp_and_transp},
but they appear duplicated in multiple, independent theories, which causes name clashes.\<close>

lemma (in preorder) rtranclp_less_eq[simp]: "(\)\<^sup>*\<^sup>* = (\)"
  using reflp_on_le transp_on_le by (simp only: rtranclp_ident_if_reflp_and_transp)

lemma (in preorder) rtranclp_greater_eq[simp]: "(\)\<^sup>*\<^sup>* = (\)"
  using reflp_on_ge transp_on_ge by (simp only: rtranclp_ident_if_reflp_and_transp)

subsection \<open>Transitive closure\<close>

lemma totalp_on_tranclp: "totalp_on A R \ totalp_on A (tranclp R)"
  by (auto intro: totalp_onI dest: totalp_onD)

lemma total_on_trancl: "total_on A r \ total_on A (trancl r)"
  by (rule totalp_on_tranclp[to_set])

lemma trancl_mono:
  assumes "p \ r\<^sup>+" "r \ s"
  shows "p \ s\<^sup>+"
proof -
  have "\(a, b) \ r\<^sup>+; r \ s\ \ (a, b) \ s\<^sup>+" for a b
    by (induction rule: trancl.induct) (iprover dest: subsetD)+
  with assms show ?thesis
    by (cases p) force
qed

lemma trancl_mono_subset: "A \ B \ A^+ \ B^+"
by (blast intro: trancl_mono)

lemma r_into_trancl': "\p. p \ r \ p \ r\<^sup>+"
  by (simp only: split_tupled_all) (erule r_into_trancl)

text \<open>\<^medskip> Conversions between \<open>trancl\<close> and \<open>rtrancl\<close>.\<close>

lemma tranclp_into_rtranclp: "r\<^sup>+\<^sup>+ a b \ r\<^sup>*\<^sup>* a b"
  by (erule tranclp.induct) iprover+

lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set]

lemma rtranclp_into_tranclp1:
  assumes "r\<^sup>*\<^sup>* a b"
  shows "r b c \ r\<^sup>+\<^sup>+ a c"
  using assms by (induct arbitrary: c) iprover+

lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set]

lemma rtranclp_into_tranclp2:
  assumes "r a b" "r\<^sup>*\<^sup>* b c" shows "r\<^sup>+\<^sup>+ a c"
  \<comment> \<open>intro rule from \<open>r\<close> and \<open>rtrancl\<close>\<close>
  using \<open>r\<^sup>*\<^sup>* b c\<close>
proof (cases rule: rtranclp.cases)
  case rtrancl_refl
  with assms show ?thesis
    by iprover
next
  case rtrancl_into_rtrancl
  with assms show ?thesis
    by (auto intro: rtranclp_trans [THEN rtranclp_into_tranclp1])
qed

lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set]

text \<open>Nice induction rule for \<open>trancl\<close>\<close>
lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]:
  assumes a: "r\<^sup>+\<^sup>+ a b"
    and cases: "\y. r a y \ P y" "\y z. r\<^sup>+\<^sup>+ a y \ r y z \ P y \ P z"
  shows "P b"
  using a by (induct x\<equiv>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\<^sup>+\<^sup>+ x y"
    and cases: "\x y. r x y \ P x y" "\x y z. r\<^sup>+\<^sup>+ x y \ P x y \ r\<^sup>+\<^sup>+ y z \ P y z \ P x z"
  shows "P x y"
  \<comment> \<open>Another induction rule for trancl, incorporating transitivity\<close>
  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\<^sup>+"
  obtains
    (base) "(a, b) \ r"
  | (step) c where "(a, c) \ r\<^sup>+" and "(c, b) \ r"
  using assms by cases simp_all

lemma trancl_Int_subset: "r \ s \ (r\<^sup>+ \ s) O r \ s \ r\<^sup>+ \ s"
  by (fastforce simp add: elim: trancl_induct)

lemma trancl_unfold: "r\<^sup>+ = r \ r\<^sup>+ O r"
  by (auto intro: trancl_into_trancl elim: tranclE)

text \<open>Transitivity of \<^term>\<open>r\<^sup>+\<close>\<close>
lemma trans_trancl [simp]: "trans (r\<^sup>+)"
proof (rule transI)
  fix x y z
  assume "(x, y) \ r\<^sup>+"
  assume "(y, z) \ r\<^sup>+"
  then show "(x, z) \ r\<^sup>+"
  proof induct
    case (base u)
    from \<open>(x, y) \<in> r\<^sup>+\<close> and \<open>(y, u) \<in> r\<close>
    show "(x, u) \ r\<^sup>+" ..
  next
    case (step u v)
    from \<open>(x, u) \<in> r\<^sup>+\<close> and \<open>(u, v) \<in> r\<close>
    show "(x, v) \ r\<^sup>+" ..
  qed
qed

lemmas trancl_trans = trans_trancl [THEN transD]

lemma tranclp_trans:
  assumes "r\<^sup>+\<^sup>+ x y"
    and "r\<^sup>+\<^sup>+ y z"
  shows "r\<^sup>+\<^sup>+ x z"
  using assms(2,1) by induct iprover+

lemma trancl_id [simp]: "trans r \ r\<^sup>+ = r"
  unfolding trans_def by (fastforce simp add: elim: trancl_induct)

lemma rtranclp_tranclp_tranclp:
  assumes "r\<^sup>*\<^sup>* x y"
  shows "\z. r\<^sup>+\<^sup>+ y z \ r\<^sup>+\<^sup>+ 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\<^sup>+\<^sup>+ b c \ r\<^sup>+\<^sup>+ a c"
  by (erule tranclp_trans [OF tranclp.r_into_trancl])

lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set]

lemma trancl_trancl_Un: "(A^+ \ B)^+ = (A \ B)^+"
proof
  show "(A\<^sup>+ \ B)\<^sup>+ \ (A \ B)\<^sup>+"
    using trancl_id[OF trans_trancl] trancl_incr[of "A \ B"]
      trancl_mono_subset[of A "(A \ B)\<^sup>+"] trancl_mono_subset[of "A\<^sup>+ \ B" "(A \ B)\<^sup>+"]
    by blast
  show "(A \ B)\<^sup>+ \ (A\<^sup>+ \ B)\<^sup>+"
    using trancl_incr[of A] trancl_mono_subset[OF sup_mono] by blast
qed

lemma trancl_absorb_subset_trancl: "B \ A^+ \ (A \ B)^+ = A^+"
using trancl_trancl_Un[of A B] sup.order_iff[of B "A\<^sup>+"] by auto

lemma tranclp_converseI:
  assumes "(r\<^sup>+\<^sup>+)\\ x y" shows "(r\\)\<^sup>+\<^sup>+ x y"
  using conversepD [OF assms]
proof (induction rule: tranclp_induct)
  case (base y)
  then show ?case
    by (iprover intro: conversepI)
next
  case (step y z)
  then show ?case
    by (iprover intro: conversepI tranclp_trans)
qed

lemmas trancl_converseI = tranclp_converseI [to_set]

lemma tranclp_converseD:
  assumes "(r\\)\<^sup>+\<^sup>+ x y" shows "(r\<^sup>+\<^sup>+)\\ x y"
proof -
  have "r\<^sup>+\<^sup>+ y x"
    using assms
    by (induction rule: tranclp_induct) (iprover dest: conversepD intro: tranclp_trans)+
  then show ?thesis
    by (rule conversepI)
qed

lemmas trancl_converseD = tranclp_converseD [to_set]

lemma tranclp_converse: "(r\\)\<^sup>+\<^sup>+ = (r\<^sup>+\<^sup>+)\\"
  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\<^sup>+)"
  by (simp only: sym_conv_converse_eq trancl_converse [symmetric])

lemma converse_tranclp_induct [consumes 1, case_names base step]:
  assumes major: "r\<^sup>+\<^sup>+ a b"
    and cases: "\y. r y b \ P y" "\y z. r y z \ r\<^sup>+\<^sup>+ z b \ P z \ P y"
  shows "P a"
proof -
  have "r\\\<^sup>+\<^sup>+ b a"
    by (intro tranclp_converseI conversepI major)
  then show ?thesis
    by (induction rule: tranclp_induct) (blast intro: cases dest: tranclp_converseD)+
qed

lemmas converse_trancl_induct = converse_tranclp_induct [to_set]

lemma tranclpD: "R\<^sup>+\<^sup>+ x y \ \z. R x z \ R\<^sup>*\<^sup>* z y"
proof (induction rule: converse_tranclp_induct)
  case (step u v)
  then show ?case
    by (blast intro: rtranclp_trans)
qed auto

lemmas tranclD = tranclpD [to_set]

lemma converse_tranclpE:
  assumes major: "tranclp r x z"
    and base: "r x z \ P"
    and step: "\y. r x y \ tranclp r y z \ P"
  shows P
proof -
  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 \<open>r x y\<close> base show P
      by iprover
  next
    case rtrancl_into_rtrancl
    then have "tranclp r y z"
      by (iprover intro: rtranclp_into_tranclp1)
    with \<open>r x y\<close> step show P
      by iprover
  qed
qed

lemmas converse_tranclE = converse_tranclpE [to_set]

lemma tranclD2: "(x, y) \ R\<^sup>+ \ \z. (x, z) \ R\<^sup>* \ (z, y) \ R"
  by (blast elim: tranclE intro: trancl_into_rtrancl)

lemma irrefl_tranclI: "r\ \ r\<^sup>* = {} \ (x, x) \ r\<^sup>+"
  by (blast elim: tranclE dest: trancl_into_rtrancl)

lemma irrefl_trancl_rD: "\x. (x, x) \ r\<^sup>+ \ (x, y) \ r \ x \ y"
  by (blast dest: r_into_trancl)

lemma trancl_subset_Sigma_aux: "(a, b) \ r\<^sup>* \ r \ A \ A \ a = b \ a \ A"
  by (induct rule: rtrancl_induct) auto

lemma trancl_subset_Sigma:
  assumes "r \ A \ A" shows "r\<^sup>+ \ A \ A"
proof (rule trancl_Int_subset [OF assms])
  show "(r\<^sup>+ \ A \ A) O r \ A \ A"
    using assms by auto
qed

lemma reflclp_tranclp [simp]: "(r\<^sup>+\<^sup>+)\<^sup>=\<^sup>= = r\<^sup>*\<^sup>*"
  by (fast elim: rtranclp.cases tranclp_into_rtranclp dest: rtranclp_into_tranclp1)

lemmas reflcl_trancl [simp] = reflclp_tranclp [to_set]

lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*"
proof -
  have "(a, b) \ (r\<^sup>=)\<^sup>+ \ (a, b) \ r\<^sup>*" for a b
    by (force dest: trancl_into_rtrancl)
  moreover have "(a, b) \ (r\<^sup>=)\<^sup>+" if "(a, b) \ r\<^sup>*" for a b
    using that
  proof (cases a b rule: rtranclE)
    case step
    show ?thesis
      by (rule rtrancl_into_trancl1) (use step in auto)
  qed auto
  ultimately show ?thesis
    by auto
qed

lemma rtrancl_trancl_reflcl [code]: "r\<^sup>* = (r\<^sup>+)\<^sup>="
  by simp

lemma trancl_empty [simp]: "{}\<^sup>+ = {}"
  by (auto elim: trancl_induct)

lemma rtrancl_empty [simp]: "{}\<^sup>* = Id"
  by (rule subst [OF reflcl_trancl]) simp

lemma rtrancl__Id[simp]: "Id\<^sup>* = Id"
using rtrancl_empty rtrancl_idemp[of "{}"] by (simp)

lemma rtranclpD: "R\<^sup>*\<^sup>* a b \ a = b \ a \ b \ R\<^sup>+\<^sup>+ a b"
  by (force simp: reflclp_tranclp [symmetric] simp del: reflclp_tranclp)

lemmas rtranclD = rtranclpD [to_set]

lemma rtrancl_eq_or_trancl: "(x,y) \ R\<^sup>* \ x = y \ x \ y \ (x, y) \ R\<^sup>+"
  by (fast elim: trancl_into_rtrancl dest: rtranclD)

lemma trancl_unfold_right: "r\<^sup>+ = r\<^sup>* O r"
  by (auto dest: tranclD2 intro: rtrancl_into_trancl1)

lemma trancl_unfold_left: "r\<^sup>+ = r O r\<^sup>*"
  by (auto dest: tranclD intro: rtrancl_into_trancl2)

lemma tranclp_unfold_left: "r^++ = r OO r^**"
by (auto intro!: ext dest: tranclpD intro: rtranclp_into_tranclp2)

lemma trancl_insert: "(insert (y, x) r)\<^sup>+ = r\<^sup>+ \ {(a, b). (a, y) \ r\<^sup>* \ (x, b) \ r\<^sup>*}"
  \<comment> \<open>primitive recursion for \<open>trancl\<close> over finite relations\<close>
proof -
  have "\a b. (a, b) \ (insert (y, x) r)\<^sup>+ \
           (a, b) \<in> r\<^sup>+ \<union> {(a, b). (a, y) \<in> r\<^sup>* \<and> (x, b) \<in> r\<^sup>*}"
    by (erule trancl_induct) (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)+
  moreover have "r\<^sup>+ \ {(a, b). (a, y) \ r\<^sup>* \ (x, b) \ r\<^sup>*} \ (insert (y, x) r)\<^sup>+"
    by (blast intro: trancl_mono rtrancl_mono [THEN [2] rev_subsetD]
                     rtrancl_trancl_trancl rtrancl_into_trancl2)
  ultimately show ?thesis
    by auto
qed

lemma trancl_insert2:
  "(insert (a, b) r)\<^sup>+ = r\<^sup>+ \ {(x, y). ((x, a) \ r\<^sup>+ \ x = a) \ ((b, y) \ r\<^sup>+ \ y = b)}"
  by (auto simp: trancl_insert rtrancl_eq_or_trancl)

lemma rtrancl_insert: "(insert (a,b) r)\<^sup>* = r\<^sup>* \ {(x, y). (x, a) \ r\<^sup>* \ (b, y) \ r\<^sup>*}"
  using trancl_insert[of a b r]
  by (simp add: rtrancl_trancl_reflcl del: reflcl_trancl) blast

text \<open>Simplifying nested closures\<close>

lemma rtrancl_trancl_absorb[simp]: "(R\<^sup>*)\<^sup>+ = R\<^sup>*"
  by (simp add: trans_rtrancl)

lemma trancl_rtrancl_absorb[simp]: "(R\<^sup>+)\<^sup>* = R\<^sup>*"
  by (subst reflcl_trancl[symmetric]) simp

lemma rtrancl_reflcl_absorb[simp]: "(R\<^sup>*)\<^sup>= = R\<^sup>*"
  by auto

text \<open>\<open>Domain\<close> and \<open>Range\<close>\<close>

lemma Domain_rtrancl [simp]: "Domain (R\<^sup>*) = UNIV"
  by blast

lemma Range_rtrancl [simp]: "Range (R\<^sup>*) = UNIV"
  by blast

lemma rtrancl_Un_subset: "(R\<^sup>* \ S\<^sup>*) \ (R \ S)\<^sup>*"
  by (rule rtrancl_Un_rtrancl [THEN subst]) fast

lemma in_rtrancl_UnI: "x \ R\<^sup>* \ x \ S\<^sup>* \ x \ (R \ S)\<^sup>*"
  by (blast intro: subsetD [OF rtrancl_Un_subset])

lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r"
  by (unfold Domain_unfold) (blast dest: tranclD)

lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r"
  unfolding Domain_converse [symmetric] by (simp add: trancl_converse [symmetric])

lemma Not_Domain_rtrancl:
  assumes "x \ Domain R" shows "(x, y) \ R\<^sup>* \ x = y"
proof -
have "(x, y) \ R\<^sup>* \ x = y"
  by (erule rtrancl_induct) (use assms in auto)
  then show ?thesis
    by auto
qed

lemma trancl_subset_Field2: "r\<^sup>+ \ Field r \ Field r"
  by (rule trancl_Int_subset) (auto simp: Field_def)

lemma finite_trancl[simp]: "finite (r\<^sup>+) = finite r"
proof
  show "finite (r\<^sup>+) \ finite r"
    by (blast intro: r_into_trancl' finite_subset)
  show "finite r \ finite (r\<^sup>+)"
    by (auto simp: finite_Field trancl_subset_Field2 [THEN finite_subset])
qed

lemma finite_rtrancl_Image[simp]: assumes "finite R" "finite A" shows "finite (R\<^sup>* `` A)"
proof (rule ccontr)
  assume "infinite (R\<^sup>* `` A)"
  with assms show False
    by(simp add: rtrancl_trancl_reflcl Un_Image del: reflcl_trancl)
qed

text \<open>More about converse \<open>rtrancl\<close> and \<open>trancl\<close>, should
  be merged with main body.\<close>

lemma single_valued_confluent:
  assumes "single_valued r" and xy: "(x, y) \ r\<^sup>*" and xz: "(x, z) \ r\<^sup>*"
  shows "(y, z) \ r\<^sup>* \ (z, y) \ r\<^sup>*"
  using xy
proof (induction rule: rtrancl_induct)
  case base
  show ?case
    by (simp add: assms)
next
  case (step y z)
  with xz \<open>single_valued r\<close> show ?case
    by (auto elim: converse_rtranclE dest: single_valuedD intro: rtrancl_trans)
qed

lemma r_r_into_trancl: "(a, b) \ R \ (b, c) \ R \ (a, c) \ R\<^sup>+"
  by (fast intro: trancl_trans)

lemma trancl_into_trancl: "(a, b) \ r\<^sup>+ \ (b, c) \ r \ (a, c) \ r\<^sup>+"
  by (induct rule: trancl_induct) (fast intro: r_r_into_trancl trancl_trans)+

lemma tranclp_rtranclp_tranclp:
  assumes "r\<^sup>+\<^sup>+ a b" "r\<^sup>*\<^sup>* b c" shows "r\<^sup>+\<^sup>+ a c"
proof -
  obtain z where "r a z" "r\<^sup>*\<^sup>* z c"
    using assms by (iprover dest: tranclpD rtranclp_trans)
  then show ?thesis
    by (blast dest: rtranclp_into_tranclp2)
qed

lemma rtranclp_conversep: "r\\\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*\\"
  by(auto simp add: fun_eq_iff intro: rtranclp_converseI rtranclp_converseD)

lemmas symp_rtranclp = sym_rtrancl[to_pred]

lemmas symp_conv_conversep_eq = sym_conv_converse_eq[to_pred]

lemmas rtranclp_tranclp_absorb [simp] = rtrancl_trancl_absorb[to_pred]
lemmas tranclp_rtranclp_absorb [simp] = trancl_rtrancl_absorb[to_pred]
lemmas rtranclp_reflclp_absorb [simp] = rtrancl_reflcl_absorb[to_pred]

lemmas 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_trancl

lemmas 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_tranclp

declare trancl_into_rtrancl [elim]

lemma tranclp_ident_if_transp:
  assumes "transp R"
  shows "R\<^sup>+\<^sup>+ = R"
proof (intro ext iffI)
  fix x y
  show "R\<^sup>+\<^sup>+ x y \ R x y"
  proof (induction y rule: tranclp_induct)
    case (base y)
    thus ?case
      by simp
  next
    case (step y z)
    thus ?case
      using \<open>transp R\<close>[THEN transpD, of x y  z] by simp
  qed
next
  fix x y
  show "R x y \ R\<^sup>+\<^sup>+ x y"
    using tranclp.r_into_trancl .
qed

text \<open>The following are special cases of @{thm [source] tranclp_ident_if_transp},
but they appear duplicated in multiple, independent theories, which causes name clashes.\<close>

lemma (in preorder) tranclp_less[simp]: "(<)\<^sup>+\<^sup>+ = (<)"
  using transp_on_less by (simp only: tranclp_ident_if_transp)

lemma (in preorder) tranclp_less_eq[simp]: "(\)\<^sup>+\<^sup>+ = (\)"
  using transp_on_le by (simp only: tranclp_ident_if_transp)

lemma (in preorder) tranclp_greater[simp]: "(>)\<^sup>+\<^sup>+ = (>)"
  using transp_on_greater by (simp only: tranclp_ident_if_transp)

lemma (in preorder) tranclp_greater_eq[simp]: "(\)\<^sup>+\<^sup>+ = (\)"
  using transp_on_ge by (simp only: tranclp_ident_if_transp)

subsection \<open>Symmetric closure\<close>

definition symclp :: "('a \ 'a \ bool) \ 'a \ 'a \ bool"
where "symclp r x y \ r x y \ r y x"

lemma symclpI [simp, intro?]:
  shows symclpI1: "r x y \ symclp r x y"
    and symclpI2: "r y x \ symclp r x y"
  by(simp_all add: symclp_def)

lemma symclpE [consumes 1, cases pred]:
  assumes "symclp r x y"
  obtains (base) "r x y" | (sym) "r y x"
  using assms by(auto simp add: symclp_def)

lemma symclp_pointfree: "symclp r = sup r r\\"
  by(auto simp add: symclp_def fun_eq_iff)

lemma symclp_greater: "r \ symclp r"
  by(simp add: symclp_pointfree)

lemma symclp_conversep [simp]: "symclp r\\ = symclp r"
  by(simp add: symclp_pointfree sup.commute)

lemma symp_on_symclp [simp]: "symp_on A (symclp R)"
  by(auto simp add: symp_on_def elim: symclpE intro: symclpI)

lemma symp_symclp_eq: "symp r \ symclp r = r"
  by(simp add: symclp_pointfree symp_conv_conversep_eq)

lemma symp_rtranclp_symclp [simp]: "symp (symclp r)\<^sup>*\<^sup>*"
  by(simp add: symp_rtranclp)

lemma rtranclp_symclp_sym [sym]: "(symclp r)\<^sup>*\<^sup>* x y \ (symclp r)\<^sup>*\<^sup>* y x"
  by(rule sympD[OF symp_rtranclp_symclp])

lemma symclp_idem [simp]: "symclp (symclp r) = symclp r"
  by(simp add: symclp_pointfree sup_commute converse_join)

lemma reflp_on_rtranclp [simp]: "reflp_on A R\<^sup>*\<^sup>*"
  by (simp add: reflp_on_def)

subsection \<open>The power operation on relations\<close>

text \<open>\<open>R ^^ n = R O \<dots> O R\<close>, the n-fold composition of \<open>R\<close>\<close>

overloading
  relpow \<equiv> "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
  relpowp \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
begin

primrec 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"

end

lemmas relpowp_Suc_right = relpowp.simps(2)

lemma relpowp_relpow_eq [pred_set_conv]:
  "(\x y. (x, y) \ R) ^^ n = (\x y. (x, y) \ R ^^ n)" for R :: "'a rel"
  by (induct n) (simp_all add: relcompp_relcomp_eq)

text \<open>For code generation:\<close>

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 0 R = Id"
  "relpow (Suc n) R = relpow n R O R"
  by (simp_all add: relpow_code_def)

lemma [code]:
  "relpowp 0 R = HOL.eq"
  "relpowp (Suc n) R = relpowp n R OO R"
  by (simp_all add: relpowp_code_def)

hide_const (open) relpow
hide_const (open) relpowp

lemma relpow_1 [simp]: "R ^^ 1 = R"
  for R :: "('a \ 'a) set"
  by simp

lemma relpowp_1 [simp]: "P ^^ 1 = P"
  for P :: "'a \ 'a \ bool"
  by (fact relpow_1 [to_pred])

lemma relpowp_Suc_0 [simp]: "P ^^ (Suc 0) = P"
  for P :: "'a \ 'a \ bool"
  by (auto)

lemma relpow_0_I: "(x, x) \ R ^^ 0"
  by simp

lemma 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 auto

lemma relpowp_Suc_I[trans]: "(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[trans]: "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 simp

lemma 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 auto

lemma 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 \<Longrightarrow> x = z \<Longrightarrow> P) \<Longrightarrow>
    (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in>  R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P"
  by (cases n) auto

lemma relpowp_E:
  "(P ^^ n) x z \
    (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) \<Longrightarrow>
    (\<And>y m. n = Suc m \<Longrightarrow> (P ^^ m) x y \<Longrightarrow> P y z \<Longrightarrow> Q) \<Longrightarrow> Q"
  by (fact relpow_E [to_pred])

lemma relpow_Suc_D2: "(x, z) \ R ^^ Suc n \ (\y. (x, y) \ R \ (y, z) \ R ^^ n)"
  by (induct n arbitrary: x z)
    (blast intro: relpow_0_I relpow_Suc_I elim: relpow_0_E relpow_Suc_E)+

lemma 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:
  assumes "(x, z) \ R ^^ n" "n = 0 \ x = z \ P"
          "\y m. n = Suc m \ (x, y) \ R \ (y, z) \ R ^^ m \ P"
      shows "P"
proof (cases n)
  case 0
  with assms show ?thesis
    by simp
next
  case (Suc m)
  with assms relpow_Suc_D2' [of m R] show ?thesis
    by force
qed

lemma relpowp_E2:
  "(P ^^ n) x z \
    (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) \<Longrightarrow>
    (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q) \<Longrightarrow> Q"
  by (fact relpow_E2 [to_pred])

lemma relpowp_trans[trans]: "(R ^^ i) x y \ (R ^^ j) y z \ (R ^^ (i + j)) x z"
proof (induction i arbitrary: x)
  case 0
  thus ?case by simp
next
  case (Suc i)
  obtain x' where "R x x'" and "(R ^^ i) x' y"
    using \<open>(R ^^ Suc i) x y\<close>[THEN relpowp_Suc_D2] by auto

  show "(R ^^ (Suc i + j)) x z"
    unfolding add_Suc
  proof (rule relpowp_Suc_I2)
    show "R x x'"
      using \<open>R x x'\<close> .
  next
    show "(R ^^ (i + j)) x' z"
      using Suc.IH[OF \<open>(R ^^ i) x' y\<close> \<open>(R ^^ j) y z\<close>] .
  qed
qed

lemma relpowp_mono:
  fixes x y :: 'a
  shows "(\x y. R x y \ S x y) \ (R ^^ n) x y \ (S ^^ n) x y"
by (induction n arbitrary: y) auto

lemma relpow_trans[trans]: "(x, y) \ R ^^ i \ (y, z) \ R ^^ j \ (x, z) \ R ^^ (i + j)"
  using relpowp_trans[to_set] .

lemma relpowp_left_unique:
  fixes R :: "'a \ 'a \ bool" and n :: nat and x y z :: 'a
  assumes lunique: "\x y z. R x z \ R y z \ x = y"
  shows "(R ^^ n) x z \ (R ^^ n) y z \ x = y"
proof (induction n arbitrary: x y z)
  case 0
  thus ?case
    by simp
next
  case (Suc n')
  then obtain x' y' :: 'a where
    "(R ^^ n') x x'" and "R x' z" and
    "(R ^^ n') y y'" and "R y' z"
    by auto

  have "x' = y'"
    using lunique[OF \<open>R x' z\<close> \<open>R y' z\<close>] .

  show "x = y"
  proof (rule Suc.IH)
    show "(R ^^ n') x x'"
      using \<open>(R ^^ n') x x'\<close> .
  next
    show "(R ^^ n') y x'"
      using \<open>(R ^^ n') y y'\<close>
      unfolding \<open>x' = y'\<close> .
  qed
qed

lemma relpow_left_unique:
  fixes R :: "('a \ 'a) set" and n :: nat and x y z :: 'a
  shows "(\x y z. (x, z) \ R \ (y, z) \ R \ x = y) \
    (x, z) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> x = y"
  using relpowp_left_unique[to_set] .

lemma relpowp_right_unique:
  fixes R :: "'a \ 'a \ bool" and n :: nat and x y z :: 'a
  assumes runique: "\x y z. R x y \ R x z \ y = z"
  shows "(R ^^ n) x y \ (R ^^ n) x z \ y = z"
proof (induction n arbitrary: x y z)
  case 0
  thus ?case
    by simp
next
  case (Suc n')
  then obtain x' :: 'a where
    "(R ^^ n') x x'" and "R x' y" and "R x' z"
    by auto
  thus "y = z"
    using runique by simp
qed

lemma relpow_right_unique:
  fixes R :: "('a \ 'a) set" and n :: nat and x y z :: 'a
  shows "(\x y z. (x, y) \ R \ (x, z) \ R \ y = z) \
    (x, y) \<in> (R ^^ n) \<Longrightarrow> (x, z) \<in> (R ^^ n) \<Longrightarrow> y = z"
  using relpowp_right_unique[to_set] .

lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n"
  by (induct n) auto

lemma 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_all add: O_assoc [symmetric])

lemma relpowp_commute: "P OO P ^^ n = P ^^ n OO P"
  by (fact relpow_commute [to_pred])

lemma relpowp_Suc_left: "R ^^ Suc n = R OO (R ^^ n)"
by (simp add: relpowp_commute)

lemma relpow_empty: "0 < n \ ({} :: ('a \ 'a) set) ^^ n = {}"
  by (cases n) auto

lemma relpowp_bot: "0 < n \ (\ :: 'a \ 'a \ bool) ^^ n = \"
  by (fact relpow_empty [to_pred])

lemma rtrancl_imp_UN_relpow:
  assumes "p \ R\<^sup>*"
  shows "p \ (\n. R ^^ n)"
proof (cases p)
  case (Pair x y)
  with assms have "(x, y) \ R\<^sup>*" by simp
  then have "(x, y) \ (\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 simp
qed

lemma rtranclp_imp_Sup_relpowp:
  assumes "(P\<^sup>*\<^sup>*) x y"
  shows "(\n. P ^^ n) x y"
  using assms and rtrancl_imp_UN_relpow [of "(x, y)", to_pred] by simp

lemma relpow_imp_rtrancl:
  assumes "p \ R ^^ n"
  shows "p \ R\<^sup>*"
proof (cases p)
  case (Pair x y)
  with assms have "(x, y) \ R ^^ n" by simp
  then have "(x, y) \ R\<^sup>*"
  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 simp
qed

lemma relpowp_imp_rtranclp: "(P ^^ n) x y \ (P\<^sup>*\<^sup>*) x y"
  using relpow_imp_rtrancl [of "(x, y)", to_pred] by simp

lemma rtrancl_is_UN_relpow: "R\<^sup>* = (\n. R ^^ n)"
  by (blast intro: rtrancl_imp_UN_relpow relpow_imp_rtrancl)

lemma rtranclp_is_Sup_relpowp: "P\<^sup>*\<^sup>* = (\n. P ^^ n)"
  using rtrancl_is_UN_relpow [to_pred, of P] by auto

lemma rtrancl_power: "p \ R\<^sup>* \ (\n. p \ R ^^ n)"
  by (simp add: rtrancl_is_UN_relpow)

lemma rtranclp_power: "(P\<^sup>*\<^sup>*) x y \ (\n. (P ^^ n) x y)"
  by (simp add: rtranclp_is_Sup_relpowp)

lemma trancl_power: "p \ R\<^sup>+ \ (\n > 0. p \ R ^^ n)"
proof -
  have "(a, b) \ R\<^sup>+ \ (\n>0. (a, b) \ R ^^ n)" for a b
  proof safe
    show "(a, b) \ R\<^sup>+ \ \n>0. (a, b) \ R ^^ n"
      by (fastforce simp: rtrancl_is_UN_relpow relcomp_unfold dest: tranclD2)
    show "(a, b) \ R\<^sup>+" if "n > 0" "(a, b) \ R ^^ n" for n
    proof (cases n)
      case (Suc m)
      with that show ?thesis
        by (auto simp: dest: relpow_imp_rtrancl rtrancl_into_trancl1)
    qed (use that in auto)
  qed
  then show ?thesis
    by (cases p) auto
qed

lemma tranclp_power: "(P\<^sup>+\<^sup>+) x y \ (\n > 0. (P ^^ n) x y)"
  using trancl_power [to_pred, of P "(x, y)"] by simp

lemma rtrancl_imp_relpow: "p \ R\<^sup>* \ \n. p \ R ^^ n"
  by (auto dest: rtrancl_imp_UN_relpow)

lemma rtranclp_imp_relpowp: "(P\<^sup>*\<^sup>*) x y \ \n. (P ^^ n) x y"
  by (auto dest: rtranclp_imp_Sup_relpowp)

text \<open>By Sternagel/Thiemann:\<close>
lemma relpow_fun_conv: "(a, b) \ R ^^ n \ (\f. f 0 = a \ f n = b \ (\i R))"
proof (induct n arbitrary: b)
  case 0
  show ?case by auto
next
  case (Suc n)
  show ?case
  proof -
    have "(\y. (\f. f 0 = a \ f n = y \ (\i R)) \ (y,b) \ R) \
      (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> 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], auto simp add: 1)
    qed
    then show ?thesis by (simp add: relcomp_unfold Suc)
  qed
qed

lemma relpowp_fun_conv: "(P ^^ n) x y \ (\f. f 0 = x \ f n = y \ (\i
  by (fact relpow_fun_conv [to_pred])

lemma relpow_finite_bounded1:
  fixes R :: "('a \ 'a) set"
  assumes "finite R" and "k > 0"
  shows "R^^k \ (\n\{n. 0 < n \ n \ card R}. R^^n)"
    (is "_ \ ?r")
proof -
  have "(a, b) \ R^^(Suc k) \ \n. 0 < n \ n \ card R \ (a, b) \ R^^n" for a b k
  proof (induct k arbitrary: b)
    case 0
    then have "R \ {}" by auto
    with card_0_eq[OF \<open>finite R\<close>] have "card R \<ge> Suc 0" by auto
    then show ?case using 0 by force
  next
    case (Suc k)
    then obtain a' where "(a, a') \<in> R^^(Suc k)" and "(a', b) \<in> R"
      by auto
    from Suc(1)[OF \<open>(a, a') \<in> R^^(Suc k)\<close>] obtain n where "n \<le> card R" and "(a, a') \<in> R ^^ n"
      by auto
    have "(a, b) \ R^^(Suc n)"
      using \<open>(a, a') \<in> R^^n\<close> and \<open>(a', b)\<in> R\<close> by auto
    from \<open>n \<le> card R\<close> consider "n < card R" | "n = card R" by force
    then show ?case
    proof cases
      case 1
      then show ?thesis
        using \<open>(a, b) \<in> R^^(Suc n)\<close> Suc_leI[OF \<open>n < card R\<close>] by blast
    next
      case 2
      from \<open>(a, b) \<in> R ^^ (Suc n)\<close> [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 \<open>n = card R\<close> 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 \<open>f(Suc n) = b\<close> 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
          then have "i \ k" by auto
          show ?thesis
          proof (cases "k = i")
            case True
            then show ?thesis
              using ij pij steps[OF i] by simp
          next
            case False
            with \<open>i \<le> k\<close> have "i < k" by auto
            then have small: "k + (j - i) \ n"
              using \<open>k<?n\<close> by arith
            show ?thesis
              using steps[OF small] \<open>i<k\<close> by auto
          qed
        qed
      qed (simp add: \<open>f 0 = a\<close>)
      moreover have "?n \ n"
        using i j ij by arith
      ultimately show ?thesis
        using \<open>n = card R\<close> by blast
    qed
  qed
  then show ?thesis
    using gr0_implies_Suc[OF \<open>k > 0\<close>] by auto
qed

lemma relpow_finite_bounded:
  fixes R :: "('a \ 'a) set"
  assumes "finite R"
  shows "R^^k \ (\n\{n. n \ card R}. R^^n)"
proof (cases k)
  case (Suc k')
  then show ?thesis
    using relpow_finite_bounded1[OF assms, of k] by auto
qed force

lemma rtrancl_finite_eq_relpow: "finite R \ R\<^sup>* = (\n\{n. n \ card R}. R^^n)"
  by (fastforce simp: rtrancl_power dest: relpow_finite_bounded)

lemma trancl_finite_eq_relpow:
  assumes "finite R" shows "R\<^sup>+ = (\n\{n. 0 < n \ n \ card R}. R^^n)"
proof -
  have "\a b n. \0 < n; (a, b) \ R ^^ n\ \ \x>0. x \ card R \ (a, b) \ R ^^ x"
    using assms by (auto dest: relpow_finite_bounded1)
  then show ?thesis
    by (auto simp: trancl_power)
qed

lemma finite_relcomp[simp,intro]:
  assumes "finite R" and "finite S"
  shows "finite (R O S)"
proof-
  have "R O S = (\(x, y)\R. \(u, v)\S. if u = y then {(x, v)} else {})"
    by (force simp: split_def image_constant_conv split: if_splits)
  then show ?thesis
    using assms by clarsimp
qed

lemma finite_relpow [simp, intro]:
  fixes R :: "('a \ 'a) set"
  assumes "finite R"
  shows "n > 0 \ finite (R^^n)"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by (cases n) (use assms in simp_all)
qed

lemma single_valued_relpow:
  fixes R :: "('a \ 'a) set"
  shows "single_valued R \ single_valued (R ^^ n)"
proof (induct n arbitrary: R)
  case 0
  then show ?case by simp
next
  case (Suc n)
  show ?case
    by (rule single_valuedI)
      (use Suc in \<open>fast dest: single_valuedD elim: relpow_Suc_E\<close>)
qed

subsection \<open>Bounded transitive closure\<close>

definition ntrancl :: "nat \ ('a \ 'a) set \ ('a \ 'a) set"
  where "ntrancl n R = (\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 fastforce
  have "0 < i \ i \ Suc 0 \ i = 1" for i
    by auto
  then show "ntrancl 0 R \ R"
    unfolding ntrancl_def by auto
qed

lemma ntrancl_Suc [simp]: "ntrancl (Suc n) R = ntrancl n R O (Id \ R)"
proof
  have "(a, b) \ ntrancl n R O (Id \ R)" if "(a, b) \ ntrancl (Suc n) R" for a b
  proof -
    from that obtain i where "0 < i" "i \ Suc (Suc n)" "(a, b) \ R ^^ i"
      unfolding ntrancl_def by auto
    show ?thesis
    proof (cases "i = 1")
      case True
      with \<open>(a, b) \<in> R ^^ i\<close> show ?thesis
        by (auto simp: ntrancl_def)
    next
      case False
      with \<open>0 < i\<close> obtain j where j: "i = Suc j" "0 < j"
        by (cases i) auto
      with \<open>(a, b) \<in> R ^^ i\<close> obtain c where c1: "(a, c) \<in> R ^^ j" and c2: "(c, b) \<in> R"
        by auto
      from c1 j \<open>i \<le> Suc (Suc n)\<close> have "(a, c) \<in> ntrancl n R"
        by (fastforce simp: ntrancl_def)
      with c2 show ?thesis by fastforce
    qed
  qed
  then show "ntrancl (Suc n) R \ ntrancl n R O (Id \ R)"
    by auto
  show "ntrancl n R O (Id \ R) \ ntrancl (Suc n) R"
    by (fastforce simp: ntrancl_def)
qed

lemma [code]: "ntrancl (Suc n) r = (let r' = ntrancl n r in r' \ r' O r)"
  by (auto simp: Let_def)

lemma finite_trancl_ntranl: "finite R \ trancl R = ntrancl (card R - 1) R"
  by (cases "card R") (auto simp: trancl_finite_eq_relpow relpow_empty ntrancl_def)

subsection \<open>Acyclic relations\<close>

definition acyclic :: "('a \ 'a) set \ bool"
  where "acyclic r \ (\x. (x,x) \ r\<^sup>+)"

abbreviation acyclicP :: "('a \ 'a \ bool) \ bool"
  where "acyclicP r \ acyclic {(x, y). r x y}"

lemma acyclic_irrefl [code]: "acyclic r \ irrefl (r\<^sup>+)"
  by (simp add: acyclic_def irrefl_def)

lemma acyclicI: "\x. (x, x) \ r\<^sup>+ \ acyclic r"
  by (simp add: acyclic_def)

lemma (in preorder) acyclicI_order:
  assumes *: "\a b. (a, b) \ r \ f b < f a"
  shows "acyclic r"
proof -
  have "f b < f a" if "(a, b) \ r\<^sup>+" for a b
    using that by induct (auto intro: * less_trans)
  then show ?thesis
    by (auto intro!: acyclicI)
qed

lemma acyclic_insert [iff]: "acyclic (insert (y, x) r) \ acyclic r \ (x, y) \ r\<^sup>*"
  by (simp add: acyclic_def trancl_insert) (blast intro: rtrancl_trans)

lemma acyclic_converse [iff]: "acyclic (r\) \ 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\<^sup>*)"
  by (simp add: acyclic_def antisym_def)
    (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)

(* Other direction:
acyclic = no loops
antisym = only self loops
Goalw [acyclic_def,antisym_def] "antisym( r\<^sup>* ) \<Longrightarrow> acyclic(r - Id)
\<Longrightarrow> antisym( r\<^sup>* ) = acyclic(r - Id)";
*)

lemma acyclic_subset: "acyclic s \ r \ s \ acyclic r"
  unfolding acyclic_def by (blast intro: trancl_mono)

subsection \<open>Setup of transitivity reasoner\<close>

ML \<open>
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_>\<open>Trueprop for t\<close> =
        let
          fun dec \<^Const_>\<open>Set.member _ for \<^Const_>\<open>Pair _ _ for a b\<close> rel\<close> =
              let
                fun decr \<^Const_>\<open>rtrancl _ for r\<close> = (r,"r*")
                  | decr \<^Const_>\<open>trancl _ for r\<close> = (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_>\<open>Trueprop for t\<close> =
        let
          fun dec (rel $ a $ b) =
            let
              fun decr \<^Const_>\<open>rtranclp _ for r\<close> = (r,"r*")
                | decr \<^Const_>\<open>tranclp _ for r\<close> = (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;
);
\<close>

setup \<open>
  map_theory_simpset (fn ctxt => ctxt
    |> Simplifier.add_unsafe_solver (mk_solver "Trancl" Trancl_Tac.trancl_tac)
    |> Simplifier.add_unsafe_solver (mk_solver "Rtrancl" Trancl_Tac.rtrancl_tac)
    |> Simplifier.add_unsafe_solver (mk_solver "Tranclp" Tranclp_Tac.trancl_tac)
    |> Simplifier.add_unsafe_solver (mk_solver "Rtranclp" Tranclp_Tac.rtrancl_tac))
\<close>

lemma transp_rtranclp [simp]: "transp R\<^sup>*\<^sup>*"
  by(auto simp add: transp_def)

text \<open>Optional methods.\<close>

method_setup trancl =
  \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac)\<close>
  \<open>simple transitivity reasoner\<close>
method_setup rtrancl =
  \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac)\<close>
  \<open>simple transitivity reasoner\<close>
method_setup tranclp =
  \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac)\<close>
  \<open>simple transitivity reasoner (predicate version)\<close>
method_setup rtranclp =
  \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac)\<close>
  \<open>simple transitivity reasoner (predicate version)\<close>

end

quality99%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.8Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.