theory Samplers imports Main "HOL-Library.Omega_Words_Fun" begin section ‹Utility Lemmas› text ‹ The following lemmas about strictly monotonic functions could go to the standard library of Isabelle/HOL. › text ‹ Strongly monotonic functions over the integers grow without bound. › lemma strict_mono_exceeds: assumes f: "strict_mono (f::nat ⇒ nat)" shows "∃k. n < f k" proof (induct n) from f have "f 0 < f 1" by (rule strict_monoD) simp hence "0 < f 1" by simp thus "∃k. 0 < f k" .. next fix n assume "∃k. n < f k" then obtain k where "n < f k" .. hence "Suc n ≤ f k" by simp also from f have "f k < f (Suc k)" by (rule strict_monoD) simp finally show "∃k. Suc n < f k" .. qed text ‹ More precisely, any natural number ‹n ≥ f 0› lies in the interval between ‹f k› and ‹f (Suc k)›, for some ‹k›. › lemma strict_mono_interval: assumes f: "strict_mono (f::nat ⇒ nat)" and n: "f 0 ≤ n" obtains k where "f k ≤ n" and "n < f (Suc k)" proof - from f[THEN strict_mono_exceeds] obtain m where m: "n < f m" .. have "m ≠ 0" proof assume "m = 0" with m n show "False" by simp qed with m obtain m' where m': "n < f (Suc m')" by (auto simp: gr0_conv_Suc) let ?k = "LEAST k. n < f (Suc k)" from m' have 1: "n < f (Suc ?k)" by (rule LeastI) have "f ?k ≤ n" proof (rule ccontr) assume "¬ ?thesis" hence k: "n < f ?k" by simp show "False" proof (cases "?k") case 0 with k n show "False" by simp next case Suc with k show "False" by (auto dest: Least_le) qed qed with 1 that show ?thesis by simp qed lemma strict_mono_comp: assumes g: "strict_mono (g::'a::order ⇒ 'b::order)" and f: "strict_mono (f::'b::order ⇒ 'c::order)" shows "strict_mono (f ∘ g)" using assms by (auto simp: strict_mono_def) section ‹Stuttering Sampling Functions› text ‹ Given an ‹ω›-sequence ‹σ›, a stuttering sampling function is a strictly monotonic function ‹f::nat ⇒ nat› such that ‹f 0 = 0› and for all ‹i› and all ‹f i ≤ k < f (i+1)›, the elements ‹σ k› are the same. In other words, ‹f› skips some (but not necessarily all) stuttering steps, but never skips a non-stuttering step. Given such ‹σ› and ‹f›, the (stuttering-)sampled reduction of ‹σ› is the sequence of elements of ‹σ› at the indices ‹f i›, which can simply be written as ‹σ ∘ f›. › subsection ‹Definition and elementary properties› definition stutter_sampler where ― ‹f is a stuttering sampling function for @{text "σ"}› "stutter_sampler (f::nat ⇒ nat) σ ≡ f 0 = 0 ∧ strict_mono f ∧ (∀k n. f k < n ∧ n < f (Suc k) ⟶ σ n = σ (f k))" lemma stutter_sampler_0: "stutter_sampler f σ ⟹ f 0 = 0" by (simp add: stutter_sampler_def) lemma stutter_sampler_mono: "stutter_sampler f σ ⟹ strict_mono f" by (simp add: stutter_sampler_def) lemma stutter_sampler_between: assumes f: "stutter_sampler f σ" and lo: "f k ≤ n" and hi: "n < f (Suc k)" shows "σ n = σ (f k)" using assms by (auto simp: stutter_sampler_def less_le) lemma stutter_sampler_interval: assumes f: "stutter_sampler f σ" obtains k where "f k ≤ n" and "n < f (Suc k)" using f[THEN stutter_sampler_mono] proof (rule strict_mono_interval) from f show "f 0 ≤ n" by (simp add: stutter_sampler_0) qed text ‹ The identity function is a stuttering sampling function for any ‹σ›. › lemma id_stutter_sampler [iff]: "stutter_sampler id σ" by (auto simp: stutter_sampler_def strict_mono_def) text ‹ Stuttering sampling functions compose, sort of. › lemma stutter_sampler_comp: assumes f: "stutter_sampler f σ" and g: "stutter_sampler g (σ ∘ f)" shows "stutter_sampler (f ∘ g) σ" proof (auto simp: stutter_sampler_def) from f g show "f (g 0) = 0" by (simp add: stutter_sampler_0) next from g[THEN stutter_sampler_mono] f[THEN stutter_sampler_mono] show "strict_mono (f ∘ g)" by (rule strict_mono_comp) next fix i k assume lo: "f (g i) < k" and hi: "k < f (g (Suc i))" from f obtain m where 1: "f m ≤ k" and 2: "k < f (Suc m)" by (rule stutter_sampler_interval) with f have 3: "σ k = σ (f m)" by (rule stutter_sampler_between) from lo 2 have "f (g i) < f (Suc m)" by simp with f[THEN stutter_sampler_mono] have 4: "g i ≤ m" by (simp add: strict_mono_less) from 1 hi have "f m < f (g (Suc i))" by simp with f[THEN stutter_sampler_mono] have 5: "m < g (Suc i)"by (simp add: strict_mono_less) from g 4 5 have "(σ ∘ f) m = (σ ∘ f) (g i)" by (rule stutter_sampler_between) with 3 show "σ k = σ (f (g i))" by simp qed text ‹ Stuttering sampling functions can be extended to suffixes. › lemma stutter_sampler_suffix: assumes f: "stutter_sampler f σ" shows "stutter_sampler (λk. f (n+k) - f n) (suffix (f n) σ)" proof (auto simp: stutter_sampler_def strict_mono_def) fix i j assume ij: "(i::nat) < j" from f have mono: "strict_mono f" by (rule stutter_sampler_mono) from mono[THEN strict_mono_mono] have "f n ≤ f (n+i)" by (rule monoD) simp moreover from mono[THEN strict_mono_mono] have "f n ≤ f (n+j)" by (rule monoD) simp moreover from mono ij have "f (n+i) < f (n+j)" by (auto intro: strict_monoD) ultimately show "f (n+i) - f n < f (n+j) - f n" by simp next fix i k assume lo: "f (n+i) - f n < k" and hi: "k < f (Suc (n+i)) - f n" from lo have "f (n+i) ≤ f n + k" by simp moreover from hi have "f n + k < f (Suc (n + i))" by simp moreover from f[THEN stutter_sampler_mono, THEN strict_mono_mono] have "f n ≤ f (n+i)" by (rule monoD) simp ultimately show "σ (f n + k) = σ (f n + (f (n+i) - f n))" by (auto dest: stutter_sampler_between[OF f]) qed subsection ‹Preservation of properties through stuttering sampling› text ‹ Stuttering sampling preserves the initial element of the sequence, as well as the presence and relative ordering of different elements. › lemma stutter_sampled_0: assumes "stutter_sampler f σ" shows "σ (f 0) = σ 0" using assms[THEN stutter_sampler_0] by simp lemma stutter_sampled_in_range: assumes f: "stutter_sampler f σ" and s: "s ∈ range σ" shows "s ∈ range (σ ∘ f)" proof - from s obtain n where n: "σ n = s" by auto from f obtain k where "f k ≤ n" "n < f (Suc k)" by (rule stutter_sampler_interval) with f have "σ n = σ (f k)" by (rule stutter_sampler_between) with n show ?thesis by auto qed lemma stutter_sampled_range: "range (σ ∘ f) = range σ" if "stutter_sampler f σ" using that stutter_sampled_in_range [of f σ] by auto lemma stutter_sampled_precedence: assumes f: "stutter_sampler f σ" and ij: "i ≤ j" obtains k l where "k ≤ l" "σ (f k) = σ i" "σ (f l) = σ j" proof - from f obtain k where k: "f k ≤ i" "i < f (Suc k)" by (rule stutter_sampler_interval) with f have 1: "σ i = σ (f k)" by (rule stutter_sampler_between) from f obtain l where l: "f l ≤ j" "j < f (Suc l)" by (rule stutter_sampler_interval) with f have 2: "σ j = σ (f l)" by (rule stutter_sampler_between) from k l ij have "f k < f (Suc l)" by simp with f[THEN stutter_sampler_mono] have "k ≤ l" by (simp add: strict_mono_less) with 1 2 that show ?thesis by simp qed subsection ‹Maximal stuttering sampling› text ‹ We define a particular sampling function that is maximal in the sense that it eliminates all finite stuttering. If a sequence ends with infinite stuttering then it behaves as the identity over the (maximal such) suffix. › fun max_stutter_sampler where "max_stutter_sampler σ 0 = 0" | "max_stutter_sampler σ (Suc n) = (let prev = max_stutter_sampler σ n in if (∀k > prev. σ k = σ prev) then Suc prev else (LEAST k. prev < k ∧ σ k ≠ σ prev))" text ‹ ‹max_stutter_sampler› is indeed a stuttering sampling function. › lemma max_stutter_sampler: "stutter_sampler (max_stutter_sampler σ) σ" (is "stutter_sampler ?ms _") proof - have "?ms 0 = 0" by simp moreover have "∀n. ?ms n < ?ms (Suc n)" proof fix n show "?ms n < ?ms (Suc n)" (is "?prev < ?next") proof (cases "∀k > ?prev. σ k = σ ?prev") case True thus ?thesis by (simp add: Let_def) next case False hence "∃k. ?prev < k ∧ σ k ≠ σ ?prev" by simp from this[THEN LeastI_ex] have "?prev < (LEAST k. ?prev < k ∧ σ k ≠ σ ?prev)" .. with False show ?thesis by (simp add: Let_def) qed qed hence "strict_mono ?ms" unfolding strict_mono_def by (blast intro: lift_Suc_mono_less) moreover have "∀n k. ?ms n < k ∧ k < ?ms (Suc n) ⟶ σ k = σ (?ms n)" proof (clarify) fix n k assume lo: "?ms n < k" (is "?prev < k") and hi: "k < ?ms (Suc n)" (is "k < ?next") show "σ k = σ ?prev" proof (cases "∀k > ?prev. σ k = σ ?prev") case True hence "?next = Suc ?prev" by (simp add: Let_def) with lo hi show ?thesis by simp ― ‹no room for intermediate index› next case False hence "?next = (LEAST k. ?prev < k ∧ σ k ≠ σ ?prev)" by (auto simp add: Let_def) with lo hi show ?thesis by (auto dest: not_less_Least) qed qed ultimately show ?thesis unfolding stutter_sampler_def by blast qed text ‹ We write ‹♮σ› for the sequence ‹σ› sampled by the maximal stuttering sampler. Also, a sequence is \emph{stutter free} if it contains no finite stuttering: whenever two subsequent elements are equal then all subsequent elements are the same. › definition stutter_reduced ("♮_" [100] 100) where "♮σ = σ ∘ (max_stutter_sampler σ)" definition stutter_free where "stutter_free σ ≡ ∀k. σ (Suc k) = σ k ⟶ (∀n>k. σ n = σ k)" lemma stutter_freeI: assumes "⋀k n. ⟦σ (Suc k) = σ k; n>k⟧ ⟹ σ n = σ k" shows "stutter_free σ" using assms unfolding stutter_free_def by blast lemma stutter_freeD: assumes "stutter_free σ" and "σ (Suc k) = σ k" and "n>k" shows "σ n = σ k" using assms unfolding stutter_free_def by blast text ‹ Any suffix of a stutter free sequence is itself stutter free. › lemma stutter_free_suffix: assumes sigma: "stutter_free σ" shows "stutter_free (suffix k σ)" proof (rule stutter_freeI) fix j n assume j: "(suffix k σ) (Suc j) = (suffix k σ) j" and n: "j < n" from j have "σ (Suc (k+j)) = σ (k+j)" by simp moreover from n have "k+n > k+j" by simp ultimately have "σ (k+n) = σ (k+j)" by (rule stutter_freeD[OF sigma]) thus "(suffix k σ) n = (suffix k σ) j" by simp qed lemma stutter_reduced_0: "(♮σ) 0 = σ 0" by (simp add: stutter_reduced_def stutter_sampled_0 max_stutter_sampler) lemma stutter_free_reduced: assumes sigma: "stutter_free σ" shows "♮σ = σ" proof - { fix n have "max_stutter_sampler σ n = n" (is "?ms n = n") proof (induct n) show "?ms 0 = 0" by simp next fix n assume ih: "?ms n = n" show "?ms (Suc n) = Suc n" proof (cases "σ (Suc n) = σ (?ms n)") case True with ih have "σ (Suc n) = σ n" by simp with sigma have "∀k > n. σ k = σ n" unfolding stutter_free_def by blast with ih show ?thesis by (simp add: Let_def) next case False with ih have "(LEAST k. k>n ∧ σ k ≠ σ (?ms n)) = Suc n" by (auto intro: Least_equality) with ih False show ?thesis by (simp add: Let_def) qed qed } thus ?thesis by (auto simp: stutter_reduced_def) qed text ‹ Whenever two sequence elements at two consecutive sampling points of the maximal stuttering sampler are equal then the sequence stutters infinitely from the first sampling point onwards. In particular, ‹♮σ› is stutter free. › lemma max_stutter_sampler_nostuttering: assumes stut: "σ (max_stutter_sampler σ (Suc k)) = σ (max_stutter_sampler σ k)" and n: "n > max_stutter_sampler σ k" (is "_ > ?ms k") shows "σ n = σ (?ms k)" proof (rule ccontr) assume contr: "¬ ?thesis" with n have "?ms k < n ∧ σ n ≠ σ (?ms k)" (is "?diff n") .. hence "?diff (LEAST n. ?diff n)" by (rule LeastI) with contr have "σ (?ms (Suc k)) ≠ σ (?ms k)" by (auto simp add: Let_def) from this stut show "False" .. qed lemma stutter_reduced_stutter_free: "stutter_free (♮σ)" proof (rule stutter_freeI) fix k n assume k: "(♮σ) (Suc k) = (♮σ) k" and n: "k < n" from n have "max_stutter_sampler σ k < max_stutter_sampler σ n" using max_stutter_sampler[THEN stutter_sampler_mono, THEN strict_monoD] by blast with k show "(♮σ) n = (♮σ) k" unfolding stutter_reduced_def by (auto elim: max_stutter_sampler_nostuttering simp del: max_stutter_sampler.simps) qed lemma stutter_reduced_suffix: "♮ (suffix k (♮σ)) = suffix k (♮σ)" proof (rule stutter_free_reduced) have "stutter_free (♮σ)" by (rule stutter_reduced_stutter_free) thus "stutter_free (suffix k (♮σ))" by (rule stutter_free_suffix) qed lemma stutter_reduced_reduced: "♮♮σ = ♮σ" by (insert stutter_reduced_suffix[of 0 "σ", simplified]) text ‹ One can define a partial order on sampling functions for a given sequence ‹σ› by saying that function ‹g› is better than function ‹f› if the reduced sequence induced by ‹f› can be further reduced to obtain the reduced sequence corresponding to ‹g›, i.e. if there exists a stuttering sampling function ‹h› for the reduced sequence ‹σ ∘ f› such that ‹σ ∘ f ∘ h = σ ∘ g›. (Note that ‹f ∘ h› is indeed a stuttering sampling function for ‹σ›, by theorem ‹stutter_sampler_comp›.) We do not formalize this notion but prove that ‹max_stutter_sampler σ› is the best sampling function according to this order. › theorem sample_max_sample: assumes f: "stutter_sampler f σ" shows "♮(σ ∘ f) = ♮σ" proof - let ?mss = "max_stutter_sampler σ" let ?mssf = "max_stutter_sampler (σ ∘ f)" from f have mssf: "stutter_sampler (f ∘ ?mssf) σ" by (blast intro: stutter_sampler_comp max_stutter_sampler) txt ‹ The following is the core invariant of the proof: the sampling functions ‹max_stutter_sampler σ› and ‹f ∘ (max_stutter_sampler (σ ∘ f))› work in lock-step (i.e., sample the same points), except if ‹σ› ends in infinite stuttering, at which point function ‹f› may make larger steps than the maximal sampling functions. › { fix k have " ?mss k = f (?mssf k) ∨ ?mss k ≤ f (?mssf k) ∧ (∀n ≥ ?mss k. σ (?mss k) = σ n)" (is "?P k" is "?A k ∨ ?B k") proof (induct k) from f mssf have "?mss 0 = f (?mssf 0)" by (simp add: max_stutter_sampler stutter_sampler_0) thus "?P 0" .. next fix k assume ih: "?P k" have b: "?B k ⟶ ?B (Suc k)" proof assume 0: "?B k" hence 1: "?mss k ≤ f (?mssf k)" .. (* NB: For some reason "... hence 1: ... and 2: ..." cannot be proved *) from 0 have 2: "∀n ≥ ?mss k. σ (?mss k) = σ n" .. hence "∀n > ?mss k. σ (?mss k) = σ n" by auto hence "∀n > ?mss k. σ n = σ (?mss k)" by auto hence 3: "?mss (Suc k) = Suc (?mss k)" by (simp add: Let_def) with 2 have "σ (?mss k) = σ (?mss (Suc k))" by (auto simp del: max_stutter_sampler.simps) from sym[OF this] 2 3 have "∀n ≥ ?mss (Suc k). σ (?mss (Suc k)) = σ n" by (auto simp del: max_stutter_sampler.simps) moreover from mssf[THEN stutter_sampler_mono, THEN strict_monoD] have "f (?mssf k) < f (?mssf (Suc k))" by (simp del: max_stutter_sampler.simps) with 1 3 have "?mss (Suc k) ≤ f (?mssf (Suc k))" by (simp del: max_stutter_sampler.simps) ultimately show "?B (Suc k)" by blast qed from ih show "?P (Suc k)" proof assume a: "?A k" show ?thesis proof (cases "∀n > ?mss k. σ n = σ (?mss k)") case True hence "∀n ≥ ?mss k. σ (?mss k) = σ n" by (auto simp: le_less) with a have "?B k" by simp with b show ?thesis by (simp del: max_stutter_sampler.simps) next case False hence diff: "σ (?mss (Suc k)) ≠ σ (?mss k)" by (blast dest: max_stutter_sampler_nostuttering) have "?A (Suc k)" proof (rule antisym) show "f (?mssf (Suc k)) ≤ ?mss (Suc k)" proof (rule ccontr) assume "¬ ?thesis" hence contr: "?mss (Suc k) < f (?mssf (Suc k))" by simp from mssf have "σ (?mss (Suc k)) = σ ((f ∘ ?mssf) k)" proof (rule stutter_sampler_between) from max_stutter_sampler[of "σ", THEN stutter_sampler_mono] have "?mss k < ?mss (Suc k)" by (rule strict_monoD) simp with a show "(f ∘ ?mssf) k ≤ ?mss (Suc k)" by (simp add: o_def del: max_stutter_sampler.simps) next from contr show "?mss (Suc k) < (f ∘ ?mssf) (Suc k)" by simp qed with a have "σ (?mss (Suc k)) = σ (?mss k)" by (simp add: o_def del: max_stutter_sampler.simps) with diff show "False" .. qed next have "∃m > ?mssf k. f m = ?mss (Suc k)" proof (rule ccontr) assume "¬ ?thesis" hence contr: "∀i. f ((?mssf k) + Suc i) ≠ ?mss (Suc k)" by simp { fix i have "f (?mssf k + i) < ?mss (Suc k)" (is "?F i") proof (induct i) from a have "f (?mssf k + 0) = ?mss k" by (simp add: o_def) also from max_stutter_sampler[of "σ", THEN stutter_sampler_mono] have "... < ?mss (Suc k)" by (rule strict_monoD) simp finally show "?F 0" . next fix i assume ih: "?F i" show "?F (Suc i)" proof (rule ccontr) assume "¬ ?thesis" then have "?mss (Suc k) ≤ f (?mssf k + Suc i)" by (simp add: o_def) moreover from contr have "f (?mssf k + Suc i) ≠ ?mss (Suc k)" by blast ultimately have i: "?mss (Suc k) < f (?mssf k + Suc i)" by (simp add: less_le) from f have "σ (?mss (Suc k)) = σ (f (?mssf k + i))" proof (rule stutter_sampler_between) from ih show "f (?mssf k + i) ≤ ?mss (Suc k)" by (simp add: o_def) next from i show "?mss (Suc k) < f (Suc (?mssf k + i))" by simp qed also from max_stutter_sampler have "... = σ (?mss k)" proof (rule stutter_sampler_between) from f[THEN stutter_sampler_mono, THEN strict_mono_mono] have "f (?mssf k) ≤ f (?mssf k + i)" by (rule monoD) simp with a show "?mss k ≤ f (?mssf k + i)" by (simp add: o_def) qed (rule ih) also note diff finally show "False" by simp qed qed } note bounded = this from f[THEN stutter_sampler_mono] have "strict_mono (λi. f (?mssf k + i))" by (auto simp: strict_mono_def) then obtain i where i: "?mss (Suc k) < f (?mssf k + i)" by (blast dest: strict_mono_exceeds) from bounded have "f (?mssf k + i) < ?mss (Suc k)" . with i show "False" by (simp del: max_stutter_sampler.simps) qed then obtain m where m: "m > ?mssf k" and m': "f m = ?mss (Suc k)" by blast show "?mss (Suc k) ≤ f (?mssf (Suc k))" proof (rule ccontr) assume "¬ ?thesis" hence contr: "f (?mssf (Suc k)) < ?mss (Suc k)" by simp from mssf[THEN stutter_sampler_mono] have "(f ∘ ?mssf) k < (f ∘ ?mssf) (Suc k)" by (rule strict_monoD) simp with a have "?mss k ≤ f (?mssf (Suc k))" by (simp add: o_def) from this contr have "σ (f (?mssf (Suc k))) = σ (?mss k)" by (rule stutter_sampler_between[OF max_stutter_sampler]) with a have stut: "(σ ∘ f) (?mssf (Suc k)) = (σ ∘ f) (?mssf k)" by (simp add: o_def) from this m have "(σ ∘ f) m = (σ ∘ f) (?mssf k)" by (blast intro: max_stutter_sampler_nostuttering) with diff m' a show "False" by (simp add: o_def) qed qed thus ?thesis .. qed next assume "?B k" with b show ?thesis by (simp del: max_stutter_sampler.simps) qed qed } hence "♮σ = ♮(σ ∘ f)" unfolding stutter_reduced_def by force thus ?thesis by (rule sym) qed end (* theory Samplers *)