section ‹Stuttering› theory Stuttering imports Stuttering_Equivalence.StutterEquivalence LList_Prefixes begin function nth_least_ext :: "nat set ⇒ nat ⇒ nat" where "enat k < esize A ⟹ nth_least_ext A k = nth_least A k" | "enat k ≥ esize A ⟹ nth_least_ext A k = Suc (Max A + (k - card A))" by force+ termination by lexicographic_order lemma nth_least_ext_strict_mono: assumes "k < l" shows "nth_least_ext s k < nth_least_ext s l" proof (cases "enat l < esize s") case True have 1: "enat k < esize s" using assms True by (metis enat_ord_simps(2) less_trans) show ?thesis using nth_least_strict_mono assms True 1 by simp next case False have 1: "finite s" using False esize_infinite_enat by auto have 2: "enat l ≥ esize s" using False by simp have 3: "l ≥ card s" using 1 2 by simp show ?thesis proof (cases "enat k < esize s") case True have 4: "s ≠ {}" using True by auto have "nth_least_ext s k = nth_least s k" using True by simp also have "… ≤ Max s" using nth_least_le_Max 1 4 True by this also have "… < Suc (Max s)" by auto also have "… ≤ Suc (Max s + (l - card s))" by auto also have "Suc (Max s + (l - card s)) = nth_least_ext s l" using 2 by simp finally show ?thesis by this next case False have 4: "enat k ≥ esize s" using False by simp have 5: "k ≥ card s" using 1 4 by simp have "nth_least_ext s k = Suc (Max s + (k - card s))" using 4 by simp also have "… < Suc (Max s + (l - card s))" using assms 5 by simp also have "… = nth_least_ext s l" using 2 by simp finally show ?thesis by this qed qed definition stutter_selection :: "nat set ⇒ 'a llist ⇒ bool" where "stutter_selection s w ≡ 0 ∈ s ∧ (∀ k i. enat i < llength w ⟶ enat (Suc k) < esize s ⟶ nth_least s k < i ⟶ i < nth_least s (Suc k) ⟶ w ?! i = w ?! nth_least s k) ∧ (∀ i. enat i < llength w ⟶ finite s ⟶ Max s < i ⟶ w ?! i = w ?! Max s)" lemma stutter_selectionI[intro]: assumes "0 ∈ s" assumes "⋀ k i. enat i < llength w ⟹ enat (Suc k) < esize s ⟹ nth_least s k < i ⟹ i < nth_least s (Suc k) ⟹ w ?! i = w ?! nth_least s k" assumes "⋀ i. enat i < llength w ⟹ finite s ⟹ Max s < i ⟹ w ?! i = w ?! Max s" shows "stutter_selection s w" using assms unfolding stutter_selection_def by auto lemma stutter_selectionD_0[dest]: assumes "stutter_selection s w" shows "0 ∈ s" using assms unfolding stutter_selection_def by auto lemma stutter_selectionD_inside[dest]: assumes "stutter_selection s w" assumes "enat i < llength w" "enat (Suc k) < esize s" assumes "nth_least s k < i" "i < nth_least s (Suc k)" shows "w ?! i = w ?! nth_least s k" using assms unfolding stutter_selection_def by auto lemma stutter_selectionD_infinite[dest]: assumes "stutter_selection s w" assumes "enat i < llength w" "finite s" "Max s < i" shows "w ?! i = w ?! Max s" using assms unfolding stutter_selection_def by auto lemma stutter_selection_stutter_sampler[intro]: assumes "linfinite w" "stutter_selection s w" shows "stutter_sampler (nth_least_ext s) (lnth w)" unfolding stutter_sampler_def proof safe show "nth_least_ext s 0 = 0" using assms(2) by (cases "enat 0 < esize s", auto) show "strict_mono (nth_least_ext s)" using strict_monoI nth_least_ext_strict_mono by blast next fix k i assume 1: "nth_least_ext s k < i" "i < nth_least_ext s (Suc k)" show "w ?! i = w ?! nth_least_ext s k" proof (cases "enat (Suc k)" "esize s" rule: linorder_cases) case less have "w ?! i = w ?! nth_least s k" proof (rule stutter_selectionD_inside) show "stutter_selection s w" using assms(2) by this show "enat i < llength w" using assms(1) by auto show "enat (Suc k) < esize s" using less by this show "nth_least s k < i" using 1(1) less by auto show "i < nth_least s (Suc k)" using 1(2) less by simp qed also have "w ?! nth_least s k = w ?! nth_least_ext s k" using less by auto finally show ?thesis by this next case equal have 2: "enat k < esize s" using equal by (metis enat_ord_simps(2) lessI) have 3: "finite s" using equal by (metis esize_infinite_enat less_irrefl) have 4: "⋀ i. i > Max s ⟹ w ?! i = w ?! Max s" using assms 3 by auto have 5: "k = card s - 1" using equal 3 by (metis diff_Suc_1 enat.inject esize_set.simps(1)) have "Max s = nth_least s (card s - 1)" using nth_least_Max 3 assms(2) by force also have "… = nth_least s k" unfolding 5 by rule also have "… = nth_least_ext s k" using 2 by simp finally have 6: "Max s = nth_least_ext s k" by this have "w ?! i = w ?! Max s" using 1(1) 4 6 by auto also have "… = w ?! nth_least_ext s k" unfolding 6 by rule finally show ?thesis by this next case greater have 2: "enat k ≥ esize s" using greater by (metis Suc_ile_eq not_le) have 3: "finite s" using greater by (metis esize_infinite_enat less_asym) have 4: "⋀ i. i > Max s ⟹ w ?! i = w ?! Max s" using assms 3 by auto have "w ?! i = w ?! Max s" using 1(1) 2 4 by auto also have "… = w ?! Suc (Max s + (k - card s))" using 4 by simp also have "… = w ?! nth_least_ext s k" using 2 by simp finally show ?thesis by this qed qed lemma stutter_equivI_selection[intro]: assumes "linfinite u" "linfinite v" assumes "stutter_selection s u" "stutter_selection t v" assumes "lselect s u = lselect t v" shows "lnth u ≈ lnth v" proof (rule stutter_equivI) have 1: "llength (lselect s u) = llength (lselect t v)" unfolding assms(5) by rule have 2: "esize s = esize t" using 1 assms(1, 2) unfolding lselect_llength by simp show "stutter_sampler (nth_least_ext s) (lnth u)" using assms(1, 3) by rule show "stutter_sampler (nth_least_ext t) (lnth v)" using assms(2, 4) by rule show "lnth u ∘ nth_least_ext s = lnth v ∘ nth_least_ext t" proof (rule ext, unfold comp_apply) fix i show "u ?! nth_least_ext s i = v ?! nth_least_ext t i" proof (cases "enat i < esize s") case True have 3: "enat i < llength (lselect s u)" "enat i < llength (lselect t v)" using assms(1, 2) 2 True unfolding lselect_llength by auto have "u ?! nth_least_ext s i = u ?! nth_least s i" using True by simp also have "… = lselect s u ?! i" using 3(1) by simp also have "… = lselect t v ?! i" unfolding assms(5) by rule also have "… = v ?! nth_least t i" using 3(2) by simp also have "… = v ?! nth_least_ext t i" using True unfolding 2 by simp finally show "u ?! nth_least_ext s i = v ?! nth_least_ext t i" by this next case False have 3: "s ≠ {}" "t ≠ {}" using assms(3, 4) by auto have 4: "finite s" "finite t" using esize_infinite_enat 2 False by metis+ have 5: "⋀ i. i > Max s ⟹ u ?! i = u ?! Max s" using assms(1, 3) 4(1) by auto have 6: "⋀ i. i > Max t ⟹ v ?! i = v ?! Max t" using assms(2, 4) 4(2) by auto have 7: "esize s = enat (card s)" "esize t = enat (card t)" using 4 by auto have 8: "card s ≠ 0" "card t ≠ 0" using 3 4 by auto have 9: "enat (card s - 1) < llength (lselect s u)" using assms(1) 7(1) 8(1) unfolding lselect_llength by simp have 10: "enat (card t - 1) < llength (lselect t v)" using assms(2) 7(2) 8(2) unfolding lselect_llength by simp have "u ?! nth_least_ext s i = u ?! Suc (Max s + (i - card s))" using False by simp also have "… = u ?! Max s" using 5 by simp also have "… = u ?! nth_least s (card s - 1)" using nth_least_Max 4(1) 3(1) by force also have "… = lselect s u ?! (card s - 1)" using lselect_lnth 9 by simp also have "… = lselect s u ?! (card t - 1)" using 2 4 by simp also have "… = lselect t v ?! (card t - 1)" unfolding assms(5) by rule also have "… = v ?! nth_least t (card t - 1)" using lselect_lnth 10 by simp also have "… = v ?! Max t" using nth_least_Max 4(2) 3(2) by force also have "… = v ?! Suc (Max t + (i - card t))" using 6 by simp also have "… = v ?! nth_least_ext t i" using 2 False by simp finally show ?thesis by this qed qed qed definition stuttering_invariant :: "'a word set ⇒ bool" where "stuttering_invariant A ≡ ∀ u v. u ≈ v ⟶ u ∈ A ⟷ v ∈ A" lemma stuttering_invariant_complement[intro!]: assumes "stuttering_invariant A" shows "stuttering_invariant (- A)" using assms unfolding stuttering_invariant_def by simp lemma stutter_equiv_forw_subst[trans]: "w⇩_{1}= w⇩_{2}⟹ w⇩_{2}≈ w⇩_{3}⟹ w⇩_{1}≈ w⇩_{3}" by auto lemma stutter_sampler_build: assumes "stutter_sampler f w" shows "stutter_sampler (0 ## (Suc ∘ f)) (a ## w)" unfolding stutter_sampler_def proof safe have 0: "f 0 = 0" using assms unfolding stutter_sampler_def by auto have 1: "f x < f y" if "x < y" for x y using assms that unfolding stutter_sampler_def strict_mono_def by auto have 2: "(0 ## (Suc ∘ f)) x < (0 ## (Suc ∘ f)) y" if "x < y" for x y using 1 that by (cases x; cases y) (auto) have 3: "w n = w (f k)" if "f k < n" "n < f (Suc k)" for k n using assms that unfolding stutter_sampler_def by auto show "(0 ## (Suc ∘ f)) 0 = 0" by simp show "strict_mono (0 ## (Suc ∘ f))" using 2 by rule show "(a ## w) n = (a ## w) ((0 ## (Suc ∘ f)) k)" if "(0 ## (Suc ∘ f)) k < n" "n < (0 ## (Suc ∘ f)) (Suc k)" for k n using 0 3 that by (cases k; cases n) (force)+ qed lemma stutter_extend_build: assumes "u ≈ v" shows "a ## u ≈ a ## v" proof - obtain f g where 1: "stutter_sampler f u" "stutter_sampler g v" "u ∘ f = v ∘ g" using stutter_equivE assms by this show ?thesis proof (intro stutter_equivI ext) show "stutter_sampler (0 ## (Suc ∘ f)) (a ## u)" using stutter_sampler_build 1(1) by this show "stutter_sampler (0 ## (Suc ∘ g)) (a ## v)" using stutter_sampler_build 1(2) by this show "(a ## u ∘ 0 ## (Suc ∘ f)) i = (a ## v ∘ 0 ## (Suc ∘ g)) i" for i using fun_cong[OF 1(3)] by (cases i) (auto) qed qed lemma stutter_extend_concat: assumes "u ≈ v" shows "w ⌢ u ≈ w ⌢ v" using stutter_extend_build assms by (induct w, force+) lemma build_stutter: "w 0 ## w ≈ w" proof (rule stutter_equivI) show "stutter_sampler (Suc (0 := 0)) (w 0 ## w)" unfolding stutter_sampler_def proof safe show "(Suc (0 := 0)) 0 = 0" by simp show "strict_mono (Suc (0 := 0))" by (rule strict_monoI, simp) next fix k n assume 1: "(Suc (0 := 0)) k < n" "n < (Suc (0 := 0)) (Suc k)" show "(w 0 ## w) n = (w 0 ## w) ((Suc (0 := 0)) k)" using 1 by (cases n, auto) qed show "stutter_sampler id w" by rule show "w 0 ## w ∘ (Suc (0 := 0)) = w ∘ id" by auto qed lemma replicate_stutter: "replicate n (v 0) ⌢ v ≈ v" proof (induct n) case 0 show ?case using stutter_equiv_refl by simp next case (Suc n) have "replicate (Suc n) (v 0) ⌢ v = v 0 ## replicate n (v 0) ⌢ v" by simp also have "… = (replicate n (v 0) ⌢ v) 0 ## replicate n (v 0) ⌢ v" by (cases n, auto) also have "… ≈ replicate n (v 0) ⌢ v" using build_stutter by this also have "… ≈ v" using Suc by this finally show ?case by this qed lemma replicate_stutter': "u ⌢ replicate n (v 0) ⌢ v ≈ u ⌢ v" using stutter_extend_concat replicate_stutter by this end