theory Orbit
imports Main
begin

section{*Definition of orbits of functions and termination conditions.*}

lemma funpow_1: "(f::'a\<Rightarrow>'a)^(1::nat) = f"
proof -
  have 1: "1 = Suc 0" by simp
  show ?thesis by (simp add: 1)
qed

lemma funpow_2: "f^2 = f o f"
proof -
  have wow: "(2::nat) = (Suc (Suc 0))" by auto
  show ?thesis by (simp add: wow)
qed

lemma funpow_zip: "(f^n) (f x) = (f^(n+1)) x"
  apply (induct n)
  apply auto
  done

lemma funpow_mult: "(f::'a \<Rightarrow> 'a)^(m*n) = (f^m)^n"
  apply (induct n)
  apply simp
  apply (simp add: funpow_add)
  done

lemma funpow_swap: "(f^n)((f^m) x) = (f^m)((f^n) x)"
  apply (induct n arbitrary: m)
  apply (auto simp add: funpow_zip)
  done

lemma nat_remainder_div: "0 < (n::nat) \<Longrightarrow> \<exists> q r. r < n \<and> m = q * n + r" 
  apply (rule exI[where x = "m div n"])
  apply (rule exI[where x = "m mod n"])
  apply simp
  done

lemma cyclic_fun_range: assumes n: "0 < n" and cycle: "(f^n) v = v" shows "\<exists> r. r < n \<and> (f^m) v = (f^r) v"
proof -  
  from nat_remainder_div[where m=m and n=n, OF n]
  obtain q r where qr: "r < n \<and> m = q * n + r" by auto
  have q_pow[rule_format]: "((f^n)^q) v = v"
    apply (induct q)
    apply (auto simp add: cycle)
    done    
  have "(f^m) v = (f^r) v"
    apply (simp add: qr)
    apply (subst add_commute)
    apply (simp add: funpow_add)
    apply (subst mult_commute)
    apply (simp add: funpow_mult q_pow)
    done
  with qr show ?thesis by auto
qed

subsection{*Definition of the orbit of a function over a given point.*}

constdefs
  "Orbit" :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a set"
  "Orbit f d \<equiv> { (f^n) d | n. True}"

lemma Orbit_refl[simp]: "x \<in> Orbit f x"
  apply (simp add: Orbit_def)
  apply (rule_tac x="0" in exI)
  by simp

lemma Orbit_next[dest]: "y \<in> Orbit f (f x) \<Longrightarrow> y \<in> Orbit f x"
  apply (auto simp add: Orbit_def)
  apply (rule_tac x="Suc n" in exI)
  apply (simp add: funpow_zip)
  done

lemma Orbit_reduce:
  shows "Orbit f x = { (f^m)(x) | m. \<forall> i \<le> m. i > 0 \<longrightarrow> (f^i) x \<noteq> x }" (is "?L = ?R")
proof -
  have case1: "?R \<subseteq> ?L"
    by (auto simp add: Orbit_def)
  {
    assume terminates: "\<exists> n. n > 0 \<and> (f^n) x = x"
    let ?M = "LEAST m. m > 0 \<and> (f^m) x = x"
    have M: "?M > 0 \<and> (f^?M) x = x"
      apply (rule LeastI_ex)
      apply (rule terminates)
      done
    {
      fix N::nat
      assume N1: "N > 0"
      assume N2: "(f^N) x = x"
      with N1 N2 have "?M \<le> N" by (simp add: Least_le)
    }
    note M_least = this
    have "?L \<subseteq> ?R"
      apply (auto simp add: Orbit_def)
      proof - 
	fix n
	have "? r. r < ?M \<and> (f^n) x = (f^r) x"
	  apply (rule cyclic_fun_range)
	  apply (simp_all add: M)
	  done
	then obtain r where r: "r < ?M \<and> (f^n) x = (f^r) x" by blast
	show "\<exists>m. (f ^ n) x = (f ^ m) x \<and> (\<forall>i\<le>m. 0 < i \<longrightarrow> (f ^ i) x \<noteq> x)"
	  apply (rule_tac x=r in exI)
	  apply (auto simp add: r)
	  apply (drule M_least)
	  apply auto
	  apply (subgoal_tac "r < ?M")
	  apply simp
	  apply (simp add: r)
	  done
      qed
  }
  note case2a = this
  {
    assume not_terminates: "\<not> (\<exists> n. n > 0 \<and> (f^n) x = x)"
    then have "?L \<subseteq> ?R"
      apply (auto simp add: Orbit_def)
      apply (rule_tac x=n in exI)
      apply auto
      apply (drule_tac x=i in spec)
      apply simp
      done
  }
  note case2b = this
  from case1 case2a case2b show ?thesis by blast
qed

lemma Orbit_unfold1: "Orbit f x = {x} \<union> Orbit f (f x)"
  apply (auto simp add: Orbit_def)
  apply (rule_tac x="n - 1" in exI)
  apply (case_tac "n=0")
  apply (auto simp add: funpow_zip)
  apply (rule_tac x=0 in exI)
  apply simp
  apply (rule_tac x="n+1" in exI)
  apply (simp add: funpow_zip)
  done

subsection{*Definition of the section of a function over a given point.*}

constdefs
  "Section continue (f::'a\<Rightarrow>'a) x0 \<equiv> { (f^n) x0 | n. (\<forall> m. m \<le> n \<longrightarrow> continue ((f^m)(x0))) }"

lemma Section_x_x: "\<not> (continue x) \<Longrightarrow> Section continue f x = {}"
  apply (simp add: Section_def)
  apply auto
  done

lemma Section_unfold: "continue i \<Longrightarrow> Section continue f i = insert i (Section continue f (f i))"
  apply (auto simp add: Section_def)
  apply (case_tac n)
  apply simp
  apply (rule_tac x="n - 1" in exI)
  apply (simp add: funpow_zip)
  apply clarsimp
  apply (drule_tac x="m+1" in spec)
  apply simp
  apply (rule_tac x=0 in exI)
  apply simp
  apply (rule_tac x="n+1" in exI)
  apply (auto simp add: funpow_zip)
  apply (case_tac m)
  apply auto
  done

lemma Section_rightopen[dest]: "y \<in>  Section continue f x \<Longrightarrow> continue y"
  by (auto simp add: Section_def)

lemma Section_is_Orbit:
  assumes x0_elem_S: "x0 \<in> Section continue f (f x0)" (is "x0 \<in> ?S")
  shows "?S = Orbit f x0"
proof -
  have x0_noteq_x1: "continue x0"
    apply (insert x0_elem_S)
    apply blast
    done
  have "\<exists> n. n > 0 \<and> (f^n) x0 = x0 \<and> (\<forall> m \<le> n. continue ((f^m) x0))"
    apply (insert x0_elem_S)
    apply (auto simp add: Section_def)
    apply (rule_tac x="n+1" in exI)
    apply (auto simp add: funpow_zip)
    apply (case_tac m)
    apply auto
    done
  then obtain N where N:"N > 0 \<and> (f^N) x0 = x0 \<and> (\<forall> m \<le> N. continue ((f^m) x0))" by auto
  {
    fix n::nat
    assume n: "n > 0"
    have "? r. r < N \<and> (f^n) x0 = (f^r) x0"
      apply (rule cyclic_fun_range)
      apply (simp_all add: N)
      done
    then obtain r where r: "r < N \<and> (f^n) x0 = (f^r) x0" by blast
    then have "continue ((f^n) x0)"
      apply (case_tac "n=0")
      apply (insert n)      
      apply (auto simp add: N)
      done    
  }
  note hammer = this
  {
    fix n :: nat
    note h = hammer[of "n+1", simplified]
  }
  note hammer = this      
  show ?thesis
    apply (auto simp add: Orbit_def Section_def)
    apply (rule_tac x="n+1" in exI)
    apply (simp add: funpow_zip)
    apply (case_tac "n=0")
    apply simp
    apply (rule_tac x="N - 1" in exI)
    apply (auto simp add: N funpow_zip hammer)
    apply (subgoal_tac "? m. n = Suc m")
    apply auto
    apply arith
    done
qed

thm Section_is_Orbit

thm Section_def

term "continue y = (\<forall> m. y = (f^m) x \<longrightarrow> (\<forall> n. n > 0 \<and> n \<le> m \<longrightarrow> (f^m) x \<noteq> x))"


lemma Section_is_Orbit': "insert x (Section (\<lambda>y. y \<noteq> x) f (f x)) = Orbit f x"
  apply auto
  apply (simp add: Section_def Orbit_def)
  apply clarsimp
  apply (rule_tac x="n+1" in exI)
  apply (simp add: funpow_zip)
  apply (auto simp add: Section_def Orbit_reduce)
  apply (case_tac m)  
  apply (simp_all add: funpow_zip)
  apply (drule_tac x="nat" in spec)
  apply clarsimp
  apply (case_tac "ma = nat")
  apply auto
  done

subsection{*Definition of a termination condition in terms of orbits.*}

fun terminates :: "('a \<Rightarrow> bool) \<times> ('a \<Rightarrow> 'a) \<times> 'a \<Rightarrow> bool"
where
  "terminates (continue, f, x) = (\<exists> y. (y \<in> Orbit f x) \<and> \<not> (continue y))"

declare terminates.simps[simp del]

lemmas terminates_simp = terminates.simps

lemma finite_Section: 
  assumes terminates: "terminates (continue, f, x)"
  shows "finite (Section continue f x)"
proof -
  have "? N. \<not> continue ((f^N) x)"
    apply (insert terminates)
    apply (auto simp add: terminates_simp Orbit_def)
    done
  then obtain N where N: "\<not> continue ((f^N) x)" by auto
  have "Section continue f x \<subseteq> image (\<lambda> n. (f^n) x) {..N}"
    apply (auto simp add: Section_def image_def Bex_def) 
    apply (rule_tac x=n in exI)
    apply simp
    apply (drule_tac x=N in spec)
    apply (auto simp add: N)
    done
  note finite_sub = finite_subset[OF this, simplified]
  then show ?thesis by blast
qed

lemma terminates_imp_notin_Section: 
  assumes terminates: "terminates (continue, f, x)"
  shows "x \<notin> Section continue f (f x)"
proof -
  {
    assume "x \<in> Section continue f (f x)"
    then have SO: "Section continue f (f x) = Orbit f x"
      by (rule Section_is_Orbit)
    from terminates[simplified terminates_simp] 
    obtain y where y: "y \<in> Orbit f x \<and> \<not> continue y" by blast
    have "y \<notin> Orbit f x"
      by (auto simp add: SO[symmetric] y)
    with y have "False"
      by auto
  }
  then show ?thesis by auto 
qed

lemma orbit_stepback: "i \<noteq> x \<Longrightarrow> (x \<in> Orbit f (f i)) = (x \<in> Orbit f i)"
  apply (auto simp add: Orbit_def)
  apply (rule_tac x = "n+1" in exI)
  apply (simp add: funpow_zip)
  apply (case_tac n)
  apply (auto simp add: funpow_zip)
  done

lemma terminates_rec: "terminates (continue, f, x) = (if continue x then terminates (continue, f, f x) else True)"
  apply (auto simp add: terminates_simp)
  apply (rule_tac x=y in exI)
  apply (simp add: Orbit_unfold1[of f x])
  apply clarsimp
  apply (rule_tac x=x in exI)
  apply simp
  done

lemma Suc_card_Section_eq:  
  assumes x0_neq_x1: "continue x0"
  and terminates: "terminates (continue, f, f x0)"
  and finite_A: "finite A"
  and x0_elem_A: "x0 \<in> A"
  shows "Suc (card (Section continue f (f x0) \<inter> A)) = card (Section continue f x0 \<inter> A)"
proof -
  have insert: "insert x0 (Section continue f (f x0) \<inter> A) = Section continue f x0 \<inter> A" (is "?L=?R")
    by (auto simp add: Section_unfold[of continue, OF x0_neq_x1] x0_elem_A)
  have x0_notin_Section: "x0 \<notin> Section continue f (f x0)" 
    apply (rule terminates_imp_notin_Section)
    apply (simp add: terminates_rec[where x=x0 and continue=continue] x0_neq_x1 terminates)
    done
  from x0_notin_Section finite_A  have card_L: "card ?L = Suc (card (Section continue f (f x0) \<inter> A))"
    by simp
  then show ?thesis
    by (simp add: card_L[symmetric] insert)
qed

end