section ‹Finite Prefixes of Infinite Sequences› theory Word_Prefixes imports List_Prefixes "../Extensions/List_Extensions" Transition_Systems_and_Automata.Sequence begin definition prefix_fininf :: "'a list ⇒ 'a stream ⇒ bool" (infix "≤⇩_{F}⇩_{I}" 50) where "u ≤⇩_{F}⇩_{I}v ≡ ∃ w. u @- w = v" lemma prefix_fininfI[intro]: assumes "u @- w = v" shows "u ≤⇩_{F}⇩_{I}v" using assms unfolding prefix_fininf_def by auto lemma prefix_fininfE[elim]: assumes "u ≤⇩_{F}⇩_{I}v" obtains w where "v = u @- w" using assms unfolding prefix_fininf_def by auto lemma prefix_fininfI_empty[intro!]: "[] ≤⇩_{F}⇩_{I}w" by force lemma prefix_fininfI_item[intro!]: assumes "a = b" "u ≤⇩_{F}⇩_{I}v" shows "a # u ≤⇩_{F}⇩_{I}b ## v" using assms by force lemma prefix_fininfE_item[elim!]: assumes "a # u ≤⇩_{F}⇩_{I}b ## v" obtains "a = b" "u ≤⇩_{F}⇩_{I}v" using assms by force lemma prefix_fininf_item[simp]: "a # u ≤⇩_{F}⇩_{I}a ## v ⟷ u ≤⇩_{F}⇩_{I}v" by force lemma prefix_fininf_list[simp]: "w @ u ≤⇩_{F}⇩_{I}w @- v ⟷ u ≤⇩_{F}⇩_{I}v" by (induct w, auto) lemma prefix_fininf_conc[intro]: "u ≤⇩_{F}⇩_{I}u @- v" by auto lemma prefix_fininf_prefix[intro]: "stake k w ≤⇩_{F}⇩_{I}w" using stake_sdrop by blast lemma prefix_fininf_set_range[dest]: "u ≤⇩_{F}⇩_{I}v ⟹ set u ⊆ sset v" by auto lemma prefix_fininf_absorb: assumes "u ≤⇩_{F}⇩_{I}v @- w" "length u ≤ length v" shows "u ≤ v" proof - obtain x where 1: "u @- x = v @- w" using assms(1) by auto have "u ≤ u @ stake (length v - length u) x" by rule also have "… = stake (length v) (u @- x)" using assms(2) by (simp add: stake_shift) also have "… = stake (length v) (v @- w)" unfolding 1 by rule also have "… = v" using eq_shift by blast finally show ?thesis by this qed lemma prefix_fininf_extend: assumes "u ≤⇩_{F}⇩_{I}v @- w" "length v ≤ length u" shows "v ≤ u" proof - obtain x where 1: "u @- x = v @- w" using assms(1) by auto have "v ≤ v @ stake (length u - length v) w" by rule also have "… = stake (length u) (v @- w)" using assms(2) by (simp add: stake_shift) also have "… = stake (length u) (u @- x)" unfolding 1 by rule also have "… = u" using eq_shift by blast finally show ?thesis by this qed lemma prefix_fininf_length: assumes "u ≤⇩_{F}⇩_{I}w" "v ≤⇩_{F}⇩_{I}w" "length u ≤ length v" shows "u ≤ v" proof - obtain u' v' where 1: "w = u @- u'" "w = v @- v'" using assms(1, 2) by blast+ have "u = stake (length u) (u @- u')" using shift_eq by blast also have "… = stake (length u) w" unfolding 1(1) by rule also have "… = stake (length u) (v @- v')" unfolding 1(2) by rule also have "… = take (length u) v" using assms by (simp add: min.absorb2 stake_append) also have "… ≤ v" by rule finally show ?thesis by this qed lemma prefix_fininf_append: assumes "u ≤⇩_{F}⇩_{I}v @- w" obtains (absorb) "u ≤ v" | (extend) z where "u = v @ z" "z ≤⇩_{F}⇩_{I}w" proof (cases "length u" "length v" rule: le_cases) case le obtain x where 1: "u @- x = v @- w" using assms(1) by auto show ?thesis proof (rule absorb) have "u ≤ u @ stake (length v - length u) x" by rule also have "… = stake (length v) (u @- x)" using le by (simp add: stake_shift) also have "… = stake (length v) (v @- w)" unfolding 1 by rule also have "… = v" using eq_shift by blast finally show "u ≤ v" by this qed next case ge obtain x where 1: "u @- x = v @- w" using assms(1) by auto show ?thesis proof (rule extend) have "u = stake (length u) (u @- x)" using shift_eq by auto also have "… = stake (length u) (v @- w)" unfolding 1 by rule also have "… = v @ stake (length u - length v) w" using ge by (simp add: stake_shift) finally show "u = v @ stake (length u - length v) w" by this show "stake (length u - length v) w ≤⇩_{F}⇩_{I}w" by rule qed qed lemma prefix_fin_prefix_fininf_trans[trans, intro]: "u ≤ v ⟹ v ≤⇩_{F}⇩_{I}w ⟹ u ≤⇩_{F}⇩_{I}w" by (metis Prefix_Order.prefixE prefix_fininf_def shift_append) lemma prefix_finE_nth: assumes "u ≤ v" "i < length u" shows "u ! i = v ! i" proof - obtain w where 1: "v = u @ w" using assms(1) by auto show ?thesis unfolding 1 using assms(2) by (simp add: nth_append) qed lemma prefix_fininfI_nth: assumes "⋀ i. i < length u ⟹ u ! i = w !! i" shows "u ≤⇩_{F}⇩_{I}w" proof (rule prefix_fininfI) show "u @- sdrop (length u) w = w" by (simp add: assms list_eq_iff_nth_eq shift_eq) qed definition chain :: "(nat ⇒ 'a list) ⇒ bool" where "chain w ≡ mono w ∧ (∀ k. ∃ l. k < length (w l))" definition limit :: "(nat ⇒ 'a list) ⇒ 'a stream" where "limit w ≡ smap (λ k. w (SOME l. k < length (w l)) ! k) nats" lemma chainI[intro?]: assumes "mono w" assumes "⋀ k. ∃ l. k < length (w l)" shows "chain w" using assms unfolding chain_def by auto lemma chainD_mono[dest?]: assumes "chain w" shows "mono w" using assms unfolding chain_def by auto lemma chainE_length[elim?]: assumes "chain w" obtains l where "k < length (w l)" using assms unfolding chain_def by auto lemma chain_prefix_limit: assumes "chain w" shows "w k ≤⇩_{F}⇩_{I}limit w" proof (rule prefix_fininfI_nth) fix i assume 1: "i < length (w k)" have 2: "mono w" "⋀ k. ∃ l. k < length (w l)" using chainD_mono chainE_length assms by blast+ have 3: "i < length (w (SOME l. i < length (w l)))" using someI_ex 2(2) by this show "w k ! i = limit w !! i" proof (cases "k" "SOME l. i < length (w l)" rule: le_cases) case (le) have 4: "w k ≤ w (SOME l. i < length (w l))" using monoD 2(1) le by this show ?thesis unfolding limit_def using prefix_finE_nth 4 1 by auto next case (ge) have 4: "w (SOME l. i < length (w l)) ≤ w k" using monoD 2(1) ge by this show ?thesis unfolding limit_def using prefix_finE_nth 4 3 by auto qed qed lemma chain_construct_1: assumes "P 0 x⇩_{0}" "⋀ k x. P k x ⟹ ∃ x'. P (Suc k) x' ∧ f x ≤ f x'" assumes "⋀ k x. P k x ⟹ k ≤ length (f x)" obtains Q where "⋀ k. P k (Q k)" "chain (f ∘ Q)" proof - obtain x' where 1: "P 0 x⇩_{0}" "⋀ k x. P k x ⟹ P (Suc k) (x' k x) ∧ f x ≤ f (x' k x)" using assms(1, 2) by metis define Q where "Q ≡ rec_nat x⇩_{0}x'" have [simp]: "Q 0 = x⇩_{0}" "⋀ k. Q (Suc k) = x' k (Q k)" unfolding Q_def by simp+ have 2: "⋀ k. P k (Q k)" proof - fix k show "P k (Q k)" using 1 by (induct k, auto) qed show ?thesis proof (intro that chainI monoI, unfold comp_apply) fix k show "P k (Q k)" using 2 by this next fix x y :: nat assume "x ≤ y" thus "f (Q x) ≤ f (Q y)" proof (induct "y - x" arbitrary: x y) case 0 show ?case using 0 by simp next case (Suc k) have "f (Q x) ≤ f (Q (Suc x))" using 1(2) 2 by auto also have "… ≤ f (Q y)" using Suc(2) by (intro Suc(1), auto) finally show ?case by this qed next fix k have 3: "P (Suc k) (Q (Suc k))" using 2 by this have 4: "Suc k ≤ length (f (Q (Suc k)))" using assms(3) 3 by this have 5: "k < length (f (Q (Suc k)))" using 4 by auto show "∃ l. k < length (f (Q l))" using 5 by blast qed qed lemma chain_construct_2: assumes "P 0 x⇩_{0}" "⋀ k x. P k x ⟹ ∃ x'. P (Suc k) x' ∧ f x ≤ f x' ∧ g x ≤ g x'" assumes "⋀ k x. P k x ⟹ k ≤ length (f x)" "⋀ k x. P k x ⟹ k ≤ length (g x)" obtains Q where "⋀ k. P k (Q k)" "chain (f ∘ Q)" "chain (g ∘ Q)" proof - obtain x' where 1: "P 0 x⇩_{0}" "⋀ k x. P k x ⟹ P (Suc k) (x' k x) ∧ f x ≤ f (x' k x) ∧ g x ≤ g (x' k x)" using assms(1, 2) by metis define Q where "Q ≡ rec_nat x⇩_{0}x'" have [simp]: "Q 0 = x⇩_{0}" "⋀ k. Q (Suc k) = x' k (Q k)" unfolding Q_def by simp+ have 2: "⋀ k. P k (Q k)" proof - fix k show "P k (Q k)" using 1 by (induct k, auto) qed show ?thesis proof (intro that chainI monoI, unfold comp_apply) fix k show "P k (Q k)" using 2 by this next fix x y :: nat assume "x ≤ y" thus "f (Q x) ≤ f (Q y)" proof (induct "y - x" arbitrary: x y) case 0 show ?case using 0 by simp next case (Suc k) have "f (Q x) ≤ f (Q (Suc x))" using 1(2) 2 by auto also have "… ≤ f (Q y)" using Suc(2) by (intro Suc(1), auto) finally show ?case by this qed next fix k have 3: "P (Suc k) (Q (Suc k))" using 2 by this have 4: "Suc k ≤ length (f (Q (Suc k)))" using assms(3) 3 by this have 5: "k < length (f (Q (Suc k)))" using 4 by auto show "∃ l. k < length (f (Q l))" using 5 by blast next fix x y :: nat assume "x ≤ y" thus "g (Q x) ≤ g (Q y)" proof (induct "y - x" arbitrary: x y) case 0 show ?case using 0 by simp next case (Suc k) have "g (Q x) ≤ g (Q (Suc x))" using 1(2) 2 by auto also have "… ≤ g (Q y)" using Suc(2) by (intro Suc(1), auto) finally show ?case by this qed next fix k have 3: "P (Suc k) (Q (Suc k))" using 2 by this have 4: "Suc k ≤ length (g (Q (Suc k)))" using assms(4) 3 by this have 5: "k < length (g (Q (Suc k)))" using 4 by auto show "∃ l. k < length (g (Q l))" using 5 by blast qed qed lemma chain_construct_2': assumes "P 0 u⇩_{0}v⇩_{0}" "⋀ k u v. P k u v ⟹ ∃ u' v'. P (Suc k) u' v' ∧ u ≤ u' ∧ v ≤ v'" assumes "⋀ k u v. P k u v ⟹ k ≤ length u" "⋀ k u v. P k u v ⟹ k ≤ length v" obtains u v where "⋀ k. P k (u k) (v k)" "chain u" "chain v" proof - obtain Q where 1: "⋀ k. (case_prod ∘ P) k (Q k)" "chain (fst ∘ Q)" "chain (snd ∘ Q)" proof (rule chain_construct_2) show "∃ x'. (case_prod ∘ P) (Suc k) x' ∧ fst x ≤ fst x' ∧ snd x ≤ snd x'" if "(case_prod ∘ P) k x" for k x using assms that by auto show "(case_prod ∘ P) 0 (u⇩_{0}, v⇩_{0})" using assms by auto show "k ≤ length (fst x)" if "(case_prod ∘ P) k x" for k x using assms that by auto show "k ≤ length (snd x)" if "(case_prod ∘ P) k x" for k x using assms that by auto qed rule show ?thesis proof show "P k ((fst ∘ Q) k) ((snd ∘ Q) k)" for k using 1(1) by (auto simp: prod.case_eq_if) show "chain (fst ∘ Q)" "chain (snd ∘ Q)" using 1(2, 3) by this qed qed end