Theory Repeat_Stabilize

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

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)

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)