# Theory Partial_Order_Reduction.Word_Prefixes

```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```