Theory Cycle

theory Cycle imports Main
begin

constdefs 
  closed :: "'a set => ('a => 'a) => bool"
  "closed A f ≡ ∀ x ∈ A. f x ∈ A"

constdefs
  cyclic :: "'a set => ('a => 'a) => bool"
  "cyclic A f ≡ ∀ d ∈ A. ∃ n. n > 0 ∧ (f^n) d = d"

constdefs
  cyclic_equiv :: "'a set => ('a => 'a) => ('a × 'a) set"
  "cyclic_equiv A f ≡ { (a,b) . a ∈ A ∧ b ∈ A ∧ (? n. (f^n) a = b) }"

lemma refl_cyclic_equiv: "refl A (cyclic_equiv A f)"
  apply (auto simp add: cyclic_equiv_def refl_def)
  apply (rule exI[where x="0"])
  apply simp
  done

lemma archimedian_law: "(m::nat) > 0 ==> ? q. n < q*m"
  apply (induct n)
  apply auto
  apply (rule_tac x="q+1" in exI) 
  apply simp
  done

lemma cyclic_wrap: 
      assumes c: "cyclic A f"
      assumes x: "x ∈ A"
      shows "? n'. (f^n') ((f^n) x) = x"
proof -
  from c x have "? m. m > 0 ∧ (f^m)(x) = x" by (auto simp add: Ball_def cyclic_def) 
  then obtain m where m: "m > 0 ∧ (f^m)(x) = x"  ..
  with archimedian_law have "? q. n < q*m" by auto
  then obtain q where "n < q*m" ..
  then have q: "q*m - n + n = q * m" by simp
  show "? n'. (f^n')((f^n) x) = x"
    apply (rule exI[where x="q*m-n"])
    apply (simp only: o_apply[where f="f ^ (q * m - n)" and g="(f ^ n)", symmetric] funpow_add[symmetric] q)
    apply (induct q)
    apply (simp_all add: funpow_add m)
    done
qed

lemma sym_cyclic_equiv: "cyclic A f ==> sym (cyclic_equiv A f)"
  by (auto simp add: sym_def cyclic_equiv_def cyclic_wrap)

lemma trans_cyclic_equiv: "trans (cyclic_equiv A f)"
  apply (auto simp add: cyclic_equiv_def trans_def)
  apply (rule_tac x="na+n" in exI)
  apply (simp add: funpow_add)
  done

lemma "cyclic A f ==> equiv A (cyclic_equiv A f)"
  by (simp add: equiv_def refl_cyclic_equiv sym_cyclic_equiv trans_cyclic_equiv)

constdefs 
  "cyclic_on A f ≡ closed A f ∧ cyclic A f"

constdefs 
  "representing A f R ≡ closed A f ∧ cyclic A f ∧ R ⊆ A ∧ (∀ x y. (x ∈ R ∧ y ∈ R ∧ (∃ n. (f^n) (x) = y)) --> x = y) ∧ A = { (f^n) (x) | n x. x ∈ R }" 
  
end