Theory Orbit

theory Orbit
imports Main
begin

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

lemma funpow_1: "(f::'a=>'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 => '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) ==> ∃ q r. r < n ∧ 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 "∃ r. r < n ∧ (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 ∧ 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 => 'a) => 'a => 'a set"
  "Orbit f d ≡ { (f^n) d | n. True}"

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

lemma Orbit_next[dest]: "y ∈ Orbit f (f x) ==> y ∈ 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. ∀ i ≤ m. i > 0 --> (f^i) x ≠ x }" (is "?L = ?R")
proof -
  have case1: "?R ⊆ ?L"
    by (auto simp add: Orbit_def)
  {
    assume terminates: "∃ n. n > 0 ∧ (f^n) x = x"
    let ?M = "LEAST m. m > 0 ∧ (f^m) x = x"
    have M: "?M > 0 ∧ (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 ≤ N" by (simp add: Least_le)
    }
    note M_least = this
    have "?L ⊆ ?R"
      apply (auto simp add: Orbit_def)
      proof - 
        fix n
        have "? r. r < ?M ∧ (f^n) x = (f^r) x"
          apply (rule cyclic_fun_range)
          apply (simp_all add: M)
          done
        then obtain r where r: "r < ?M ∧ (f^n) x = (f^r) x" by blast
        show "∃m. (f ^ n) x = (f ^ m) x ∧ (∀i≤m. 0 < i --> (f ^ i) x ≠ 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: "¬ (∃ n. n > 0 ∧ (f^n) x = x)"
    then have "?L ⊆ ?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} ∪ 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=>'a) x0 ≡ { (f^n) x0 | n. (∀ m. m ≤ n --> continue ((f^m)(x0))) }"

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

lemma Section_unfold: "continue i ==> 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 ∈  Section continue f x ==> continue y"
  by (auto simp add: Section_def)

lemma Section_is_Orbit:
  assumes x0_elem_S: "x0 ∈ Section continue f (f x0)" (is "x0 ∈ ?S")
  shows "?S = Orbit f x0"
proof -
  have x0_noteq_x1: "continue x0"
    apply (insert x0_elem_S)
    apply blast
    done
  have "∃ n. n > 0 ∧ (f^n) x0 = x0 ∧ (∀ m ≤ 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 ∧ (f^N) x0 = x0 ∧ (∀ m ≤ N. continue ((f^m) x0))" by auto
  {
    fix n::nat
    assume n: "n > 0"
    have "? r. r < N ∧ (f^n) x0 = (f^r) x0"
      apply (rule cyclic_fun_range)
      apply (simp_all add: N)
      done
    then obtain r where r: "r < N ∧ (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 = (∀ m. y = (f^m) x --> (∀ n. n > 0 ∧ n ≤ m --> (f^m) x ≠ x))"


lemma Section_is_Orbit': "insert x (Section (λy. y ≠ 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 => bool) × ('a => 'a) × 'a => bool"
where
  "terminates (continue, f, x) = (∃ y. (y ∈ Orbit f x) ∧ ¬ (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. ¬ continue ((f^N) x)"
    apply (insert terminates)
    apply (auto simp add: terminates_simp Orbit_def)
    done
  then obtain N where N: "¬ continue ((f^N) x)" by auto
  have "Section continue f x ⊆ image (λ 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 ∉ Section continue f (f x)"
proof -
  {
    assume "x ∈ 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 ∈ Orbit f x ∧ ¬ continue y" by blast
    have "y ∉ 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 ≠ x ==> (x ∈ Orbit f (f i)) = (x ∈ 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 ∈ A"
  shows "Suc (card (Section continue f (f x0) ∩ A)) = card (Section continue f x0 ∩ A)"
proof -
  have insert: "insert x0 (Section continue f (f x0) ∩ A) = Section continue f x0 ∩ A" (is "?L=?R")
    by (auto simp add: Section_unfold[of continue, OF x0_neq_x1] x0_elem_A)
  have x0_notin_Section: "x0 ∉ 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) ∩ A))"
    by simp
  then show ?thesis
    by (simp add: card_L[symmetric] insert)
qed

end