Theory Serial_Rel

(*  Title:      Serial_Rel.thy
    Author:     Sebastian Ullrich
*)

subsection "Serial Relations"

text ‹A serial relation on a finite carrier induces a cycle.›

theory Serial_Rel
imports Main
begin

definition "serial_on A r ⟷ (∀x ∈ A. ∃y ∈ A. (x,y) ∈ r)"
lemmas serial_onI = serial_on_def[THEN iffD2, rule_format]
lemmas serial_onE = serial_on_def[THEN iffD1, rule_format, THEN bexE]

fun iterated_serial_on :: "'a set ⇒ 'a rel ⇒ 'a ⇒ nat ⇒ 'a" where
  "iterated_serial_on A r x 0 = x"
| "iterated_serial_on A r x (Suc n) = (SOME y. y ∈ A ∧ (iterated_serial_on A r x n,y) ∈ r)"

lemma iterated_serial_on_linear: "iterated_serial_on A r x (n+m) = iterated_serial_on A r (iterated_serial_on A r x n) m"
by (induction m) auto

lemma iterated_serial_on_in_A:
  assumes "serial_on A r" "a ∈ A"
  shows "iterated_serial_on A r a n ∈ A"
proof (induct n)
  case (Suc n)
  thus ?case
    using assms(1, 2) by (subst iterated_serial_on.simps(2)) (rule someI2_ex, auto elim: serial_onE)
qed (simp add:assms(2))

lemma iterated_serial_on_in_power:
  assumes "serial_on A r" "a ∈ A"
  shows "(a,iterated_serial_on A r a n) ∈ r ^^ n"
proof (induct n)
  case (Suc n)
  moreover obtain b where "(iterated_serial_on A r a n,b) ∈ r" "b ∈ A"
    using iterated_serial_on_in_A[OF assms, of n] assms(1) by - (rule serial_onE)
  ultimately show ?case by (subst iterated_serial_on.simps(2)) (rule someI2_ex, auto)
qed simp

lemma trancl_powerI: "a ∈ R ^^ n ⟹ n > 0 ⟹ a ∈ R⇧+"
by (auto simp:trancl_power)

theorem serial_on_finite_cycle:
  assumes "serial_on A r" "A ≠ {}" "finite A"
  obtains a where "a ∈ A" "(a,a) ∈ r⇧+"
proof-
  from assms(2) obtain a where a: "a ∈ A" by auto
  let ?f = "iterated_serial_on A r a"
  from a have "range ?f ⊆ A" using assms(1) by (auto intro: iterated_serial_on_in_A)
  with assms(3) have "∃m∈UNIV.¬ finite {n ∈ UNIV. ?f n = ?f m}"
    by - (rule pigeonhole_infinite, auto simp: finite_subset)
  then obtain n m where "?f m = ?f n" and[simp]: "n < m"
    by (metis (mono_tags, lifting) finite_nat_set_iff_bounded mem_Collect_eq not_less_eq)
  hence "?f n = iterated_serial_on A r (?f n) (m-n)"
    using iterated_serial_on_linear[of A r a n "m-n"] by (auto simp:less_imp_le_nat)
  also have "(?f n,iterated_serial_on A r (?f n) (m-n)) ∈ r ^^ (m - n)"
    by (rule iterated_serial_on_in_power[OF assms(1)], rule iterated_serial_on_in_A[OF assms(1) a])
  finally show ?thesis
    by - (rule that[of "?f n"], rule iterated_serial_on_in_A[OF assms(1) a], rule trancl_powerI, auto)
qed

end