Theory Repeat_Stabilize

section‹Repeat finitely Until it Stabilizes›
theory Repeat_Stabilize
imports Main
begin

text‹Repeating something a number of times›


text‹Iterating a function at most @{term n} times (first parameter) until it stabilizes.›
fun repeat_stabilize :: "nat ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'a" where
  "repeat_stabilize 0 _ v = v" |
  "repeat_stabilize (Suc n) f v = (let v_new = f v in if v = v_new then v else repeat_stabilize n f v_new)"

lemma repeat_stabilize_funpow: "repeat_stabilize n f v = (f^^n) v"
  proof(induction n arbitrary: v)
  case (Suc n)
    have "f v = v ⟹ (f^^n) v = v" by(induction n) simp_all
    with Suc show ?case by(simp add: Let_def funpow_swap1)
  qed(simp)

lemma repeat_stabilize_induct: "(P m) ⟹ (⋀m. P m ⟹ P (f m)) ⟹ P (repeat_stabilize n f m)"
  apply(simp add: repeat_stabilize_funpow)
  apply(induction n)
   by(simp)+


end