(*-------------------------------------------*
            |       Uniform Candy Distribution          |
            |               Isabelle 2011               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            |             13 November 2011              |
            *-------------------------------------------*)

(* ................................................................... *

There are N children sitting in a circle, where each child has an even
number of candies. The following step is repeated indefinitely:

  every child passes half of their candies to the child on their left;
  any child who ends up with an odd number of candies is given another
  candy by the teacher.

Then, prove that eventually every child will hold the same number of
candies.

References:

- TPPmark 2011
  http://staff.aist.go.jp/reynald.affeldt/tpp2011/ucd.html
- The Puzzle TOAD
  http://www.cs.cmu.edu/puzzle/puzzle6.html

 * ................................................................... *)

theory UCD_Isabelle2011
imports Complex_Main
begin

declare Min_ge_iff [simp del]
declare Max_le_iff [simp del]
declare Max_less_iff [simp del]

(* =================================================================== *
 |                                                                     |
 |                           Preliminary                               |
 |                                                                     |
 * =================================================================== *)

(* -------------------------------------------------- *
 |                list decomposition                  |
 * -------------------------------------------------- *)

lemma list_nth_decompo:
  "ALL s. i < length s
   --> (EX s0 s1. length s0 = i & s = s0 @ (s!i) # s1)"
apply (induct_tac i, auto)
(* base case *)
 apply (rule_tac x="tl s" in exI)
 apply (simp add: hd_conv_nth[THEN sym])
(* step case *)
 apply (case_tac "s=[]", simp)
 apply (drule_tac x="tl s" in spec)
 apply (drule mp, force)
  apply (elim conjE exE)
  apply (rule_tac x="hd s # s0" in exI)
  apply (auto simp add: neq_Nil_conv)
done

(* -------------------------------------------------- *
 |          max, min, num, stable on list             |
 * -------------------------------------------------- *)

abbreviation
  maxList   :: "nat list => nat"
where
 "maxList s == Max (set s)"

abbreviation
  minList   :: "nat list => nat"
where
 "minList s == Min (set s)"

primrec
  numList        :: "nat => nat list => nat"
where
  "numList m ([])  = 0"
 |"numList m (n#s) = (if (m=n) then (Suc (numList m s)) else numList m s)"

lemma num_test: "numList 2 [4, 2, 10, 2, 5, 2] = 3" by (simp)

definition
  stableList :: "nat list => bool"
where
  stableList_def: "stableList s == ALL n:set s. n = minList s"

(* -------------------------------------- *
 |  basic lemmas on min, num, and stable  |
 * -------------------------------------- *)

lemma min_le_eq:
  "i < length s ==> (s ! i <= minList s) = (s ! i = minList s)"
by (auto, rule antisym, auto)

lemma num_append:
 "numList m(s @ t) = numList m s + numList m t"
by (induct_tac s, auto)

lemma num_zero_not_eq:
  "(numList m s = 0) = (ALL i<length s. s!i ~= m)"
apply (induct_tac s)
apply (auto)
apply (case_tac "i=0", simp)
apply (auto simp add: gr0_conv_Suc)
done

lemma num_not_zero_ex:
  "(0 < numList m s) = (EX i<length s. s!i = m)"
apply (auto)
apply (erule contrapos_pp)
apply (simp add: num_zero_not_eq)
apply (case_tac "0 < numList (s ! i) s")
apply (auto simp add: num_zero_not_eq)
done

lemma num_le[rule_format]:
  "ALL t.
    (length t = length s & (ALL i<length s. t!i = m --> s!i = m))
    --> numList m t <= numList m s"
apply (induct_tac s)
apply (auto simp add: length_Suc_conv)
apply (drule_tac x="ys" in spec, auto)
apply (drule_tac x="ys" in spec, auto)
apply (drule_tac x="ys" in spec, auto)
done

lemma num_less_lm:
  "[| length t0 = length s0; length t1 = length s1; n ~= m ;
      ALL i<length (s0 @ m # s1). (t0 @ n # t1)!i = m --> (s0 @ m # s1)!i = m |]
   ==> numList m (t0 @ n # t1) < numList m (s0 @ m # s1)"
apply (simp add: num_append, simp add: num_append[THEN sym])
apply (simp add: less_Suc_eq_le)
apply (rule num_le)
apply (auto)
apply (case_tac "i<length s0")
 (* i<length s0 *)
 apply (drule_tac x="i" in spec)
 apply (simp add: nth_append)
 (* ~ i<length s0 *)
 apply (drule_tac x="Suc i" in spec)
 apply (simp add: not_less nth_append)
 apply (subgoal_tac "(Suc i - length s0) = Suc (i - length s0)")
 apply (auto)
done

lemma num_less:
  "[| length t = length s; 
      j < length s ; s!j = m ; t!j = n ; n ~= m;
      ALL i<length s. t!i = m --> s!i = m |]
   ==> numList m t < numList m s"
apply (insert list_nth_decompo[of j])
apply (frule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
apply (simp)
apply (elim conjE exE, simp)
apply (rule num_less_lm, auto)
done

lemma num_zero_not_min:
  "[| s ~= [] ; numList m s = 0 |] ==> (m ~= minList s)"
apply (simp add: num_zero_not_eq)
apply (insert in_set_conv_nth[of m s], auto)
done

lemma not_stable_not_nil:
  "~ stableList s ==> s ~= []"
by (auto simp add: stableList_def)

(* --------------------------- *
 |    lemmas on nth and num    |
 * --------------------------- *)

lemma nth_min_lm[rule_format]:
  "(s ! i = minList s & i+j < length s &
    (ALL i. s ! i = minList s --> i < length s - Suc 0 --> s ! Suc i = minList s))
       --> s ! (i+j) = minList s"
by (induct_tac j, auto)

lemma nth_min:
  "[| s ! i = minList s ; i <= j ; j < length s ;
      ALL i. s ! i = minList s --> i < length s - Suc 0 --> s ! Suc i = minList s |]
   ==> s ! j = minList s"
by (insert nth_min_lm[of s i "j - i"], simp)

lemma nth_min_less_lm:
  "[| s ! 0 = minList s | minList s < s ! (length s - Suc 0) ;
      ~ stableList s |] ==>
    EX i. i < length s - Suc 0 & s ! i = minList s & minList s < s ! (Suc i)"
apply (erule disjE)
(* s ! 0 = minList s *)
 apply (erule contrapos_np)
 apply (simp add: stableList_def)
 apply (auto simp add: in_set_conv_nth)
 apply (simp add: not_less)
 apply (rule nth_min)
  apply (auto simp add: min_le_eq)

(* minList s < s ! (length s - Suc 0) *)
 apply (rotate_tac 1)
 apply (erule contrapos_pp)
 apply (simp add: not_less)
 apply (subgoal_tac "EX i. i<length s & s!i =  minList s")
  apply (elim conjE exE)
  apply (rule eq_refl)
  apply (rule nth_min)
   apply (auto)
  apply (drule_tac x="ia" in spec)
  apply (auto)
  apply (simp add: eq_iff)

 apply (simp add: not_stable_not_nil in_set_conv_nth[THEN sym])
done

lemma nth_min_less:
  "~ stableList s ==>
   (minList s < s ! 0 & s ! (length s - Suc 0) = minList s) |
   (EX i. i < length s - Suc 0 & s ! i = minList s & minList s < s ! (Suc i))"
apply (case_tac "minList s < s ! 0 & s ! (length s - Suc 0) = minList s")
 (* disj 1 *)
 apply (simp
 (* disj 2 *))
 apply (subgoal_tac "0 < length s")
  apply (rule disjI2)
  apply (simp del: disj_not1)
  apply (erule disjE)
   (* ~ minList s < s ! 0 *)
   apply (rule nth_min_less_lm)
   apply (simp_all)
   apply (simp add: not_less)
   apply (simp add: min_le_eq)
   (* s ! (length s - Suc 0) ~= minList s *)
   apply (rule nth_min_less_lm)
    apply (simp_all)
   apply (simp add: less_le, simp)
 apply (auto simp add: stableList_def)
done

(* nth_min_less_hd is used for lemma 4 *)

lemma nth_min_less_hd:
  "~ stableList s ==>
    EX i. i<length s & minList s = s ! i & minList s < (s @ [hd s]) ! (Suc i)"
apply (insert nth_min_less[of s], simp)
apply (subgoal_tac "0 < length s")
 apply (erule disjE)
  (* disj 1 *)
  apply (rule_tac x="(length s - Suc 0)" in exI)
  apply (simp add: hd_conv_nth)
  (* disj 2 *)
  apply (elim conjE exE)
  apply (rule_tac x="i" in exI, simp)
  apply (subgoal_tac "Suc i < length s")
   apply (simp add: nth_append)
  apply (auto)
done

(* -------------------------------------------------- *
 |            iterateive composition                  |
 * -------------------------------------------------- *)

primrec
  repeat :: "nat => ('a => 'a) => ('a => 'a)"
where
  "repeat      0  = (%f. id)"
 |"repeat (Suc k) = (%f. (repeat k f) o f)"

(* -------------------------- *
 |  basic lemmas on repeat    |
 * -------------------------- *)

lemma length_repeat:
  "ALL t. length (f t) = length t
   ==> ALL s. length(repeat k f s) = length s"
by (induct_tac k, auto)

lemma repeat_nil:
  "ALL t. length (f t) = length t
   ==> (repeat k f s = []) = (s = [])"
apply (subgoal_tac "(length(repeat k f s) = 0) = (length s = 0)")
apply (simp)
apply (simp add: length_repeat)
done

lemma repeat_assoc:
  "ALL s. (repeat k f (f s)) = f (repeat k f s)"
by (induct_tac k, auto)

lemma min_repeat_le:
  "(ALL k. minList ((repeat k f) s) <= minList ((repeat (Suc k) f) s))
   --> minList s <= minList ((repeat k f) s)"
apply (induct_tac k)
apply (auto)
apply (drule_tac x="n" in spec)
apply (simp add: repeat_assoc)
done

lemma repeat_repeat_append:
  "ALL s. repeat k0 f (repeat k1 f s) = repeat (k0+k1) f s"
apply (induct_tac k0)
apply (auto)
apply (drule_tac x="f s" in spec)
apply (simp add: repeat_assoc)
done

(* --------------------------- *
 |  lemmas on num and repeat   |
 * --------------------------- *)

lemma num_repeat_zero_lm[rule_format]:
  "ALL s. (numList m s <= n & 
          (ALL k. 0 < numList m ((repeat k f) s)
                 --> (numList m ((repeat (Suc k) f) s) < numList m ((repeat k f) s))))
   --> (EX k. numList m ((repeat k f) s) = 0)"
apply (induct_tac n)
 (* base *)
 apply (intro allI impI, rule_tac x="0" in exI, simp)
 (* step *)
 apply (intro allI impI)
 apply (simp)
 apply (case_tac "(EX k. numList m ((repeat k f) s) = 0)", simp)
 apply (drule_tac x="(f s)" in spec)
 apply (elim conjE exE)
 apply (drule mp)
  apply (rule conjI)
   (* conj 1 *)
   apply (drule_tac x="0" in spec)
   apply (simp)
   apply (drule_tac x="0" in spec)
   apply (simp)
   (* conj 2 *)
   apply (intro allI)
   apply (drule_tac x="Suc k" in spec)
   apply (simp)

 apply (erule exE)
 apply (rule_tac x="Suc k" in exI)
 apply (simp)
done

lemma num_repeat_zero:
  "ALL k. 0 < numList m ((repeat k f) s)
         --> (numList m ((repeat (Suc k) f) s) < numList m ((repeat k f) s))
   ==> EX k. numList m ((repeat k f) s) = 0"
by (rule num_repeat_zero_lm, auto)

(* =================================================================== *
 |                                                                     |
 |                    Uniform Candy Distribution                       |
 |                                                                     |
 * =================================================================== *)

(* -------------------------------------------------- *
 |                    definition                      |
 * -------------------------------------------------- *)

definition
  allEven :: "nat list => bool"
where
  allEven_def : "allEven s == (ALL s:set s. even s)"

definition
  fill :: "nat => nat"
where
  fill_def : "fill c == if even c then c else c+1"

definition
  nextOne :: "nat => nat => nat"
where
  nextOne_def : "nextOne c0 c1 == fill(c0 div 2 + c1 div 2)"

primrec
  nextList :: "nat => (nat list) => (nat list)"
where
   "nextList 0       s = []"
 | "nextList (Suc i) s = (nextList i s) @ [nextOne (s ! i) (s ! (Suc i))]"

definition
  nextCirc :: "(nat list) => (nat list)"
where
  nextCirc_def:
   "nextCirc s == nextList (length s) (s @ [hd s])"

(* ------ test ------ *)

lemma "nextList (Suc (Suc (Suc 0))) [4, 2, 10, 4] = [4, 6, 8]"
by (simp add: nextOne_def fill_def)

lemma "nextCirc [4, 2, 10] = [4, 6, 8]"
by (simp add: nextCirc_def nextOne_def fill_def)

(* -------------------------------------------------- *
 |                lemmas on nextOne                   |
 * -------------------------------------------------- *)

lemma min_nextOne_eq:
  "even c ==> nextOne c c = c"
apply (auto simp add: fill_def nextOne_def even_mult_two_ex)
apply (drule_tac x="m" in spec, simp)
done

lemma min_nextOne_le1:
  "[| even c0;  even c1; c0 <= c1 |] ==> c0 <= nextOne c0 c1"
by (auto simp add: fill_def nextOne_def even_mult_two_ex)

lemma min_nextOne_le2:
  "[| even c0;  even c1; c0 <= c1 |] ==> c0 <= nextOne c1 c0"
by (auto simp add: fill_def nextOne_def even_mult_two_ex)

lemma min_nextOne_le:
  "[| even c0;  even c1 |] ==> min c0 c1 <= nextOne c0 c1"
by (auto simp add: fill_def nextOne_def even_mult_two_ex)

lemma max_nextOne_le1:
  "[| even c0;  even c1; c0 <= c1 |] ==> nextOne c0 c1 <= c1"
apply (simp add: fill_def nextOne_def)
apply (auto simp add: even_mult_two_ex)
apply (case_tac "2 * mb < ma", auto)
apply (case_tac "m < 2 * mb", auto)
done

lemma max_nextOne_le2:
  "[| even c0; even c1; c0 <= c1 |] ==> nextOne c1 c0 <= c1"
apply (simp add: fill_def nextOne_def)
apply (auto simp add: even_mult_two_ex)
apply (case_tac "m < 2 * mb", auto)
apply (case_tac "2 * mb < ma", auto)
done

lemma max_nextOne_le:
  "[| even c0;  even c1 |] ==> nextOne c0 c1 <= max c0 c1"
by (simp add: max_def max_nextOne_le1 max_nextOne_le2)

lemma min_nextOne_less1:
  "[| even c0;  even c1; c0 < c1 |] ==> c0 < nextOne c0 c1"
by (auto simp add: fill_def nextOne_def even_mult_two_ex)

lemma min_nextOne_less2:
  "[| even c0;  even c1; c0 < c1 |] ==> c0 < nextOne c1 c0"
by (auto simp add: fill_def nextOne_def even_mult_two_ex)

lemma min_nextOne_less:
  "[| even c0;  even c1; c0 ~= c1 |] ==> min c0 c1 < nextOne c0 c1"
by (auto simp add: min_def min_nextOne_less1 min_nextOne_less2)

lemma even_nextOne: "even (nextOne c0 c1)"
by (auto simp add: fill_def nextOne_def)

(* -------------------------------------------------- *
 |                 lemmas on nextLine                 |
 * -------------------------------------------------- *)

lemma length_nextList[rule_format]:
  "i < length s --> length (nextList i s) = i"
by (induct_tac i, simp+)

lemma nth_nextList_nextOne_diff[rule_format]:
  "Suc (i+j) < length s -->
     nextList (Suc (i+j)) s ! i = nextOne (s ! i) (s ! (Suc i))"
by (induct_tac j, auto simp add: nth_append length_nextList)

lemma nth_nextList_nextOne:
  "[| Suc n < length s ; i <= n |] ==>
      nextList (Suc n) s ! i = nextOne (s ! i) (s ! (Suc i))"
by (insert nth_nextList_nextOne_diff[of i "n - i"], simp)

(* -------------------------------------------------- *
 |                 lemmas on nextCirc                 |
 * -------------------------------------------------- *)

lemma nth_nextCirc_nextOne:
  "i < length s ==> (nextCirc s) ! i = nextOne (s ! i) ((s @ [hd s]) ! (Suc i))"
apply (simp add: nextCirc_def)
apply (insert nth_nextList_nextOne[of "length s - 1" "s @ [hd s]" i])
apply (subgoal_tac "(EX m. length s = Suc m)", erule exE)
 apply (simp add: nth_append del: nextList.simps)
apply (auto simp add: gr0_conv_Suc[THEN sym])
done

lemma length_nextCirc:
  "length (nextCirc s) = length s"
by (simp add: nextCirc_def length_nextList)

lemma length_nextCirc_not_nil:
  "(nextCirc s = []) = (s = [])"
apply (subgoal_tac "(length(nextCirc s) = 0) = (length s = 0)")
 apply (simp only: length_0_conv)
apply (simp add: length_nextCirc)
done

lemma even_nextCirc:
  "allEven (nextCirc s)"
apply (auto simp add: allEven_def in_set_conv_nth length_nextCirc)
apply (simp add: nth_nextCirc_nextOne)
apply (simp add: even_nextOne)
done

(* -------------------------------------------------- *
 |           lemma 1 (max : not increase)             |
 * -------------------------------------------------- *)

lemma nextCirc_max_le:
  "[| allEven s ; s ~= [] |] ==> maxList (nextCirc s) <= maxList s"
apply (subgoal_tac
  "EX i. i<length (nextCirc s) & (nextCirc s) ! i = maxList (nextCirc s)")

 apply (elim conjE exE)
 apply (rotate_tac -1, drule sym)
 apply (simp add: length_nextCirc nth_nextCirc_nextOne)
 apply (rule order_trans)
  apply (rule max_nextOne_le)
   apply (auto simp add: allEven_def nth_append)

apply (simp add: length_nextCirc_not_nil in_set_conv_nth[THEN sym])
done

(* -------------------------------------------------- *
 |           lemma 2 (min : not decrease)             |
 * -------------------------------------------------- *)

lemma nextCirc_min_le:
  "[| allEven s ; s ~= [] |] ==> minList s <=  minList (nextCirc s)"
apply (subgoal_tac
  "EX i. i<length (nextCirc s) & (nextCirc s) ! i = minList (nextCirc s)")

 apply (elim conjE exE)
 apply (rotate_tac -1, drule sym)
 apply (simp add: length_nextCirc nth_nextCirc_nextOne)
 apply (rule order_trans)
  defer
  apply (rule min_nextOne_le)
   apply (auto simp add: allEven_def nth_append)

apply (simp add: length_nextCirc_not_nil in_set_conv_nth[THEN sym])
done

(* -------------------------------------------------- *
 |               lemma 3 (greater than min)           |
 * -------------------------------------------------- *)

lemma nextCirc_gt_min:
  "allEven s
   ==> ALL i < length s. minList s < s!i --> minList s < (nextCirc s)!i"
apply (intro allI impI)
apply (subgoal_tac "s ~= []")

 apply (simp add: nth_nextCirc_nextOne)
 apply (case_tac "(s @ [hd s]) ! Suc i = s ! i")
  apply (simp add: allEven_def min_nextOne_eq)
 apply (rule le_less_trans)
  defer
   apply (rule min_nextOne_less)
   apply (auto simp add: allEven_def nth_append)
done

(* -------------------------------------------------- *
 |             lemma 4 (min : increase)               |
 * -------------------------------------------------- *)

lemma nextCirc_min_less:
  "[| allEven s ; ~ stableList s |]
   ==> EX i. i < length s & s!i = minList s & s!i < (nextCirc s)!i"
apply (insert nth_min_less_hd[of s], simp)
apply (elim conjE exE)
apply (rule_tac x="i" in exI)
apply (simp add: length_nextCirc nth_nextCirc_nextOne)
apply (rule min_nextOne_less1)
 apply (auto simp add: allEven_def nth_append not_stable_not_nil)
done

(* -------------------------------------------------- *
 |             lemma 5 (num: decrease)                |
 * -------------------------------------------------- *)

lemma nextCirc_num_less:
  "[| allEven s ; ~ stableList s |]
   ==> numList (minList s) (nextCirc s) < numList (minList s) s"
apply (insert nextCirc_min_less[of s], simp)
apply (insert nextCirc_gt_min[of s], simp)
apply (elim conjE exE)
apply (rule num_less)
 apply (simp add: length_nextCirc)
 apply (simp)+
apply (intro allI impI)
apply (rotate_tac -1)
apply (erule contrapos_pp)
apply (drule_tac x="ia" in spec)
apply (simp add: less_le)
done

(* -------------------------------------------------- *
 |         basic lemmas on (repeat nextCirc)          |
 * -------------------------------------------------- *)

lemma even_repeat_nextCirc:
  "allEven s ==> allEven (repeat k nextCirc s)"
apply (induct_tac k)
 apply (simp add: even_nextCirc)
 apply (simp add: repeat_assoc even_nextCirc)
done

lemma length_repeat_nextCirc:
  "ALL s. length (repeat k nextCirc s) = length s"
by (induct_tac k, auto simp add: length_nextCirc)

lemma repeat_nextCirc_not_nil:
  "((repeat k nextCirc s) = []) = (s = [])"
apply (subgoal_tac "(length(repeat k nextCirc s) = 0) = (length s = 0)")
 apply (simp only: length_0_conv)
apply (simp add: length_repeat_nextCirc)
done

lemma not_stable_repeat_nextCirc_not_nil:
  "ALL k. ~stableList (repeat k nextCirc s) ==> s ~= []"
apply (drule_tac x="0" in spec)
apply (simp add: not_stable_not_nil)
done

(* --- min le --- *)

lemma min_repeat_nextCirc_le:
  "ALL s. (allEven s & s ~= [])
   --> minList s <= minList (repeat k nextCirc s)"
apply (induct_tac k)
 (* base *)
 apply (simp add: nextCirc_min_le)
 (* step *)
 apply (intro allI impI)
 apply (drule_tac x="nextCirc s" in spec)
 apply (simp_all add: even_nextCirc length_nextCirc_not_nil)
 apply (rule order_trans)
  apply (rule nextCirc_min_le)
  apply (simp_all)
done

(* --- max le --- *)

lemma max_repeat_nextCirc_le:
  "ALL s. (allEven s & s ~= [])
   --> maxList (repeat k nextCirc s) <= maxList s"
apply (induct_tac k)
 (* base *)
 apply (simp add: nextCirc_max_le)
 (* step *)
 apply (intro allI impI)
 apply (drule_tac x="nextCirc s" in spec)
 apply (simp_all add: even_nextCirc length_nextCirc_not_nil)
 apply (rule order_trans)
  apply (simp)
  apply (simp add: nextCirc_max_le)
done

(* -------------------------------------------------- *
 |               lemmas (min: less)                   |
 * -------------------------------------------------- *)

lemma min_repeat_nextCirc_eq_min:
  "[| allEven s ; s ~= [] ; 0 < numList (minList s) (repeat k nextCirc s) |]
   ==> minList (repeat k nextCirc s) = minList s"
apply (auto simp add: num_not_zero_ex)
apply (rule antisym)
 apply (rotate_tac -1, drule sym)
 apply (simp)
apply (simp add: min_repeat_nextCirc_le)
done

lemma num_repeat_nextCirc_zero:
  "ALL s. (allEven s & (ALL k. ~stableList (repeat k nextCirc s)))
   --> (EX k. numList (minList s) (repeat k nextCirc s) = 0)"
apply (intro allI impI)
apply (rule num_repeat_zero)
apply (auto)
apply (simp add: repeat_assoc)
apply (subgoal_tac 
  " numList (minList (repeat k nextCirc s)) (nextCirc (repeat k nextCirc s))
  < numList (minList (repeat k nextCirc s)) (repeat k nextCirc s)")
 apply (simp add: not_stable_repeat_nextCirc_not_nil min_repeat_nextCirc_eq_min)
apply (simp add: nextCirc_num_less even_repeat_nextCirc)
done

lemma min_repeat_nextCirc_less:
  "ALL s. (allEven s & (ALL k. ~stableList (repeat k nextCirc s)))
   --> (EX k. minList s < minList ((repeat k nextCirc) s))"
apply (intro allI impI)
apply (insert num_repeat_nextCirc_zero)
apply (drule_tac x="s" in spec)
apply (simp)
apply (erule exE)
apply (rule_tac x="k" in exI)
apply (simp add: num_zero_not_eq)
apply (simp (no_asm_simp) add: less_le)

apply (simp add: not_stable_repeat_nextCirc_not_nil min_repeat_nextCirc_le)
apply (rotate_tac 1)
apply (erule contrapos_pn)
apply (simp add: in_set_conv_nth[THEN sym])
apply (simp add: not_stable_repeat_nextCirc_not_nil repeat_nextCirc_not_nil)
done

(* -------------------------------------------------- *
 |          lemmas (min: repeat increase)             |
 * -------------------------------------------------- *)

lemma min_repeat_nextCirc_inc:
  "[| allEven s ; ALL k. ~stableList (repeat k nextCirc s) |]
   ==> EX k. minList s + any < minList ((repeat k nextCirc) s)"
apply (induct_tac any)
 (* base *)
 apply (simp add: min_repeat_nextCirc_less)
 (* step *)
 apply (erule exE)
 apply (insert min_repeat_nextCirc_less)
 apply (drule_tac x="(repeat k nextCirc s)" in spec)
 apply (simp add: repeat_repeat_append)
 apply (drule mp)
  apply (simp add: even_repeat_nextCirc)
 apply (elim conjE exE)
 apply (rule_tac x="ka + k" in exI)
 apply (auto)
done

(* -------------------------------------------------- *
 |            Theorem: eventually stable              |
 * -------------------------------------------------- *)

theorem eventually_stable:
  "[| allEven s ; s ~= [] |] ==> EX k. stableList (repeat k nextCirc s)"
apply (case_tac "EX k. stableList (repeat k nextCirc s)", simp)

(* if it never reaches a stable state *)
apply (insert min_repeat_nextCirc_inc[of s "maxList s - minList s"])
apply (simp)
apply (elim conjE exE)
apply (rotate_tac -1)
apply (erule contrapos_pp)
apply (simp add: not_less)
apply (subgoal_tac "minList (repeat k nextCirc s) <= maxList (repeat k nextCirc s)")
 apply (rule order_trans)
  apply (assumption)
 apply (simp add: repeat_nextCirc_not_nil)
 apply (simp add: max_repeat_nextCirc_le)

apply (simp add: repeat_nextCirc_not_nil)
done

(* ----------------------------------------------- *)

declare Min_ge_iff [simp]
declare Max_le_iff [simp]
declare Max_less_iff [simp]

end