theory Cycle imports Main
begin

constdefs 
  closed :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
  "closed A f \<equiv> \<forall> x \<in> A. f x \<in> A"

constdefs
  cyclic :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
  "cyclic A f \<equiv> \<forall> d \<in> A. \<exists> n. n > 0 \<and> (f^n) d = d"

constdefs
  cyclic_equiv :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<times> 'a) set"
  "cyclic_equiv A f \<equiv> { (a,b) . a \<in> A \<and> b \<in> A \<and> (? 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 \<Longrightarrow> ? 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 \<in> A"
      shows "? n'. (f^n') ((f^n) x) = x"
proof -
  from c x have "? m. m > 0 \<and> (f^m)(x) = x" by (auto simp add: Ball_def cyclic_def) 
  then obtain m where m: "m > 0 \<and> (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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<equiv> closed A f \<and> cyclic A f"

constdefs 
  "representing A f R \<equiv> closed A f \<and> cyclic A f \<and> R \<subseteq> A \<and> (\<forall> x y. (x \<in> R \<and> y \<in> R \<and> (\<exists> n. (f^n) (x) = y)) \<longrightarrow> x = y) \<and> A = { (f^n) (x) | n x. x \<in> R }" 
  
end