theory TPP2011Minamide2
imports Main 
begin

locale children =
  fixes S :: "'a set" (* S is the set of children *)
  fixes right::"'a \<Rightarrow> 'a" 
  assumes nonempty[intro,simp]: "S \<noteq> {}"
  assumes finite[intro,simp]: "finite S"
  assumes image: "right ` S \<subseteq> S"


lemma (in children) [simp]: 
  assumes "X \<subseteq> S" shows "finite X"
  by (rule finite_subset[where B = "S"], simp_all add: assms)

primrec (in children) rightn :: "['a, nat] \<Rightarrow> 'a" where
  "rightn x 0 = x" | 
  "rightn x (Suc n) = rightn (right x) n"

lemma (in children) image_rightn[rule_format]:
  "\<forall>x\<in>S. rightn x n \<in> S"
  by (induct n, insert image, auto)

locale circle_children = children +
  assumes circle: "\<forall>x\<in>S. \<forall>y\<in>S. \<exists>n. y = rightn x n" 

definition avg :: "[nat, nat] \<Rightarrow> nat" (infix "\<oplus>" 100)  where
  "m1 \<oplus> m2 = (m1 + m2 + 1) div 2"

lemma avg_sym :"m1 \<oplus> m2 = m2 \<oplus> m1"
  by  (simp add: avg_def)

lemma avg1:
  assumes "m1 \<le> m" "m2 \<le> m" 
  shows "m1 \<oplus> m2 \<le> m"
proof (unfold avg_def)
  have "(m1 + m2 + 1) div 2 \<le> (2*m+1) div 2"
    by (rule div_le_mono, insert assms, auto)
  thus "(m1 + m2 + 1) div 2 \<le> m"
    by simp
qed

lemma avg2:
  assumes "m \<le> m1 " "m \<le> m2"
  shows "m \<le> m1 \<oplus> m2"
proof (unfold avg_def)
  have "(2*m+1) div 2 \<le> (m1 + m2 + 1) div 2" 
    by (rule div_le_mono, insert assms, auto)
  thus " m \<le> (m1 + m2 + 1) div 2"
    by simp
qed

lemma avg3:
  assumes "m < m1 " "m \<le> m2"
  shows "m < m1 \<oplus> m2"
proof (unfold avg_def)
  have "\<exists>m1'. m1 = m1' + 1"
    using assms by arith
  then obtain m1' where "m1 = m1' + 1" by blast
  have "(2*m+2) div 2 \<le> (m1' + m2 + 2) div 2" 
    by (rule div_le_mono, insert prems, auto)
  thus "m < (m1 + m2 + 1) div 2"
    using prems by (simp)
qed

definition (in children) step :: "['a \<Rightarrow> nat] \<Rightarrow> 'a \<Rightarrow> nat" where
  "step f x = f x \<oplus> f (right x)"

definition (in children) wmin :: "['a \<Rightarrow> nat] \<Rightarrow> nat" where
  "wmin f = Min (f ` S)"

definition (in children) wmax :: "['a \<Rightarrow> nat] \<Rightarrow> nat" where
  "wmax f = Max (f ` S)"

lemma (in children) wmin[simp]: 
  assumes "x \<in> S" shows "wmin f \<le> f x"
  by (unfold wmin_def, rule Min_le, insert assms, auto)

lemma (in children) wmax[simp]: 
  assumes "x \<in> S" shows "f x \<le> wmax f"
  by (unfold wmax_def, rule Max_ge, insert assms, auto)

lemma (in children) L1: 
  assumes "x \<in> S" shows "step f x \<le> wmax f"
  by (simp add: step_def, rule avg1, insert assms image, auto)

lemma (in children) L2:
  assumes "x \<in> S" shows "wmin f \<le> step f x"
  by (simp add: step_def, rule avg2, insert assms image, auto)

lemma (in children) L3:
  assumes "x \<in> S" "wmin f < f x"
  shows "wmin f < step f x"
  by (simp add: step_def, rule avg3, fact, insert assms image, auto)

lemma (in children) L4:
  assumes "x \<in> S" "f x < f (right x)"
  shows "f x < step f x"
  by (simp add: step_def, simp add: avg_sym[of "f x"], rule avg3, fact, insert assms image,  simp)

lemma (in children) L5':
  "step f -` {wmin f} \<inter> S \<subseteq> f -` {wmin f} \<inter> S"
proof (auto)
  fix x
  assume x_in_S: "x \<in> S"
  assume "step f x = wmin f"
  show "f x = wmin f"
  proof (rule contrapos_pp)
    assume H: "f x \<noteq> wmin f"
    have "wmin f < step f x"
    proof (rule L3)
      show "wmin f < f x"
        by (rule neq_le_trans, insert H x_in_S, auto)
    qed (fact)
    thus "step f x \<noteq> wmin f"
      by simp
  qed (fact)
qed

lemma (in children) L5'':
  assumes H1: "f x = wmin f" and "x \<in> S" "wmin f < f (right x)" 
  shows "step f -` {wmin f} \<inter> S \<subset> f -` {wmin f} \<inter> S"
proof (rule, rule L5')
  have "wmin f < step f x" 
    by (simp add: H1[THEN sym], rule L4, fact, simp add: H1, fact)
  hence "step f x \<noteq> wmin f" by simp
  with H1 `x \<in> S`
  show "step f -` {wmin f} \<inter> S \<noteq> f -` {wmin f} \<inter> S"
    by (auto simp add: vimage_def)
qed

lemma (in children) right:
  shows "\<forall>x\<in>S. (f x \<noteq> f (rightn x n))  \<longrightarrow> (\<exists>y\<in>S. f y = f x \<and> f y \<noteq> f (right y))"
proof (induct n)
  case 0
  show ?case
    using assms by auto
next
  case (Suc n)
  show ?case
  proof 
    fix x
    assume "x \<in> S"
    let ?x' = "right x"
    show "f x \<noteq> f (rightn x (Suc n)) \<longrightarrow> (\<exists>y\<in>S. f y = f x \<and> f y \<noteq> f (right y))"
    proof (cases "f x = f ?x'")
      case True
      have "(f ?x' \<noteq> f (rightn ?x' n))  \<longrightarrow> (\<exists>y\<in>S. f y = f ?x' \<and> f y \<noteq> f (right y))"
        by (rule Suc[THEN bspec], insert `x \<in> S` image, auto)
      with True
      show ?thesis by auto
    next
      case False
      show ?thesis
        by (rule impI, rule bexI[of _ x], insert False, auto, rule `x\<in>S`)
    qed
  qed
qed

lemma (in circle_children) L5:
  assumes "wmin f < wmax f"
  shows "step f -` {wmin f} \<inter> S \<subset> f -` {wmin f} \<inter> S"
proof -
  have "wmin f \<in> f ` S"
    by (auto simp add: wmin_def)
  hence "\<exists>x\<in>S. f x = wmin f" 
    by (auto)
  then obtain x where "x \<in> S""f x = wmin f" by blast
  have "wmax f \<in> f ` S"
    by (auto simp add: wmax_def)
  hence "\<exists>y\<in>S. f y = wmax f" 
    by (auto)
  then obtain y where "y\<in>S" "f y = wmax f" by blast
  have "\<exists>n. y = rightn x n"
    by (rule circle[rule_format], fact+)
  then obtain n where "y = rightn x n" by blast
  have "\<exists>y\<in>S. f y = f x \<and> f y \<noteq> f (right y)"
  proof (rule right[rule_format], fact)
    show "f x \<noteq> f (rightn x n)"
      using prems by auto
  qed
  then obtain y where "y\<in>S" "f y = f x" "f y \<noteq> f (right y)" by blast
  show ?thesis
  proof (rule L5''[of _ y])
    show "f y = wmin f" using prems by auto 
  next
    have "wmin f \<noteq> f (right y)" using prems by simp
    also have "wmin f \<le> f (right y)" using `y\<in>S` image by auto
    finally show "wmin f < f (right y)" by simp
  qed (fact)
qed

lemma (in children) step_wmin: "wmin f \<le> wmin (step f)"
  by (subst (2) wmin_def, auto simp add: L2)

lemma (in children) step_wmax: "wmax (step f) \<le>  wmax f"
  by (subst (1) wmax_def, auto simp add: L1)

lemma (in children) step_wmax_wmin: 
  "wmax (step f) - wmin (step f) \<le> wmax f - wmin f"
  using step_wmin[of f] step_wmax[of f]
  by auto

lemma (in children) wmin_wmax:
  "wmin f \<le> wmax f"
  by (auto simp add: wmin_def wmax_def)

primrec (in circle_children) nstep :: "['a \<Rightarrow> nat, nat] \<Rightarrow> ('a \<Rightarrow> nat)" where
  "nstep f 0 = f" |
  "nstep f (Suc n) = nstep (step f) n"

theorem (in circle_children) terminating: (* abstract version *)
  "\<exists>n. wmin (nstep f n) = wmax (nstep f n)" (is "?P f")
proof -
  let ?R = 
    "inv_image (less_than <*lex*> finite_psubset) 
               (%f. (wmax f - wmin f, f -` {wmin f} \<inter> S))"
  show ?thesis
  proof (induct rule: wf_induct[where r = ?R])
    show "wf ?R" by auto
  next
    fix f
    assume IH: "\<forall>y. (y, f)
            \<in> inv_image (less_than <*lex*> finite_psubset)
               (\<lambda>f. (wmax f - wmin f, f -` {wmin f} \<inter> S)) \<longrightarrow> ?P y"
    show "\<exists>n. wmin (nstep f n) = wmax (nstep f n)"
    proof (cases "wmax f = wmin f")
      case True
      show ?thesis by (rule exI[of _ 0], simp add: True)
    next 
      case False
      have "?P (step f)"
      proof (rule IH[rule_format])
        show "(step f, f) \<in> inv_image (less_than <*lex*> finite_psubset)
          (\<lambda>f. (wmax f - wmin f, f -` {wmin f} \<inter> S))"
        proof (simp, cases "wmax (step f) - wmin (step f) < wmax f - wmin f")
          case True
          thus "wmax (step f) - wmin (step f) < wmax f - wmin f \<or>
            wmax (step f) - wmin (step f) = wmax f - wmin f \<and>
            step f -` {wmin (step f)} \<inter> S \<subset> f -` {wmin f} \<inter> S"
            by auto
        next
          case False
          thus "wmax (step f) - wmin (step f) < wmax f - wmin f \<or>
            wmax (step f) - wmin (step f) = wmax f - wmin f \<and>
            step f -` {wmin (step f)} \<inter> S \<subset> f -` {wmin f} \<inter> S"
            using step_wmax_wmin[of f]
          proof simp
            assume "wmax (step f) - wmin (step f) = wmax f - wmin f"
            hence "wmin (step f) = wmin f"
              using step_wmin[of f] step_wmax[of f] wmin_wmax[of f] 
                wmin_wmax[of "step f"]
              by auto
            thus "step f -` {wmin (step f)} \<inter> S \<subset> f -` {wmin f} \<inter> S"
            proof (simp)
              show "step f -` {wmin f} \<inter> S \<subset> f -` {wmin f} \<inter> S"
              proof (rule L5)
                from `wmax f \<noteq> wmin f` wmin_wmax[of f] 
                show "wmin f < wmax f" by auto
              qed
            qed
          qed
        qed
      qed
      then obtain n where n: "wmin (nstep (step f) n) = wmax (nstep (step f) n)" by blast
      show ?thesis 
        by (rule exI[of _ "Suc n"], insert n, auto)
    qed
  qed
qed

locale N =
  fixes N::nat
  assumes [simp]:"0 < N" 

context N begin

lemma circle:
  assumes H: "x < N" "y < N" shows "\<exists>n. y = (x + n) mod N"
proof (cases "x \<le> y") 
  case True
  show ?thesis
    by (rule exI[of _ "y - x"], insert True H, auto)
next
  case False
  show ?thesis
    by (rule exI[of _ "y + (N - x)"], insert False H, auto)
qed


lemma children: "children {0..<N} (%x. Suc x mod N)"
  by (unfold children_def, auto)

lemma rightn[rule_format]: 
  "\<forall>x. x < N \<longrightarrow> children.rightn (\<lambda>x. Suc x mod N) x n = (x + n) mod N"
proof (induct n)
  case 0
  show ?case
    by (simp add: children.rightn.simps[OF children])
next
  case (Suc n)
  thus ?case
    by (auto simp add: children.rightn.simps[OF children], arith)
qed

lemma circle_children: "circle_children {0..<N} (%x. Suc x mod N)"
proof (unfold circle_children_def, rule conjI, rule children, unfold circle_children_axioms_def)
  show "\<forall>x\<in>{0..<N}. \<forall>y\<in>{0..<N}. \<exists>n. y = children.rightn (\<lambda>x. Suc x mod N) x n"
    by (auto simp add: rightn, rule circle, auto)
qed

end

theorem (* concrete version *)
  fixes N::nat
  assumes "0 < N" "S = {0..< N}" "right = (\<lambda>x. Suc x mod N)"
  shows "\<exists>n. children.wmin S (circle_children.nstep right f n) =
             children.wmax S (circle_children.nstep right f n)"
proof (simp add: assms, rule circle_children.terminating)
  show "circle_children {0..<N} (\<lambda>x. Suc x mod N)"
    by (rule N.circle_children, simp add: N_def, fact)
qed


end