# Theory List_Prefixes

section ‹List Prefixes›

theory List_Prefixes
imports "HOL-Library.Prefix_Order"
begin

lemmas [intro] = prefixI strict_prefixI[folded less_eq_list_def]
lemmas [elim] = prefixE strict_prefixE[folded less_eq_list_def]

lemmas [intro?] = take_is_prefix[folded less_eq_list_def]

hide_const (open) Sublist.prefix Sublist.suffix

lemma prefix_finI_item[intro!]:
assumes "a = b" "u ≤ v"
shows "a # u ≤ b # v"
using assms by force
lemma prefix_finE_item[elim!]:
assumes "a # u ≤ b # v"
obtains "a = b" "u ≤ v"
using assms by force

lemma prefix_fin_append[intro]: "u ≤ u @ v" by auto
lemma pprefix_fin_length[dest]:
assumes "u < v"
shows "length u < length v"
proof -
obtain a w where 1: "v = u @ a # w" using assms by rule
show ?thesis unfolding 1 by simp
qed

end

# Theory List_Extensions

section ‹Lists›

theory List_Extensions
imports "HOL-Library.Sublist"
begin

declare remove1_idem[simp]

lemma nth_append_simps[simp]:
"i < length xs ⟹ (xs @ ys) ! i = xs ! i"
"i ≥ length xs ⟹ (xs @ ys) ! i = ys ! (i - length xs)"
unfolding nth_append by simp+

notation zip (infixr "||" 51)

abbreviation "project A ≡ filter (λ a. a ∈ A)"
abbreviation "select s w ≡ nths w s"

lemma map_plus[simp]: "map (plus n) [i ..< j] = [i + n ..< j + n]"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
have "map (plus (Suc n)) [i ..< j] = map (Suc ∘ plus n) [i ..< j]" by simp
also have "… = (map Suc ∘ map (plus n)) [i ..< j]" by simp
also have "… = map Suc (map (plus n) [i ..< j])" by simp
also have "… = map Suc [i + n ..< j + n]" unfolding Suc by simp
also have "… = [Suc (i + n) ..< Suc (j + n)]" unfolding map_Suc_upt by simp
also have "… = [i + Suc n ..< j + Suc n]" by simp
finally show ?case by this
qed

lemma singleton_list_lengthE[elim]:
assumes "length xs = 1"
obtains x
where "xs = [x]"
proof -
have 0: "length xs = Suc 0" using assms by simp
obtain y ys where 1: "xs = y # ys" "length ys = 0" using 0 Suc_length_conv by metis
show ?thesis using that 1 by blast
qed

lemma singleton_hd_last: "length xs = 1 ⟹ hd xs = last xs" by fastforce

lemma set_subsetI[intro]:
assumes "⋀ i. i < length xs ⟹ xs ! i ∈ S"
shows "set xs ⊆ S"
proof
fix x
assume 0: "x ∈ set xs"
obtain i where 1: "i < length xs" "x = xs ! i" using 0 unfolding in_set_conv_nth by blast
show "x ∈ S" using assms(1) 1 by auto
qed

lemma hd_take[simp]:
assumes "n ≠ 0" "xs ≠ []"
shows "hd (take n xs) = hd xs"
proof -
have 1: "take n xs ≠ []" using assms by simp
have 2: "0 < n" using assms by simp
have "hd (take n xs) = take n xs ! 0" using hd_conv_nth[OF 1] by this
also have "… = xs ! 0" using nth_take[OF 2] by this
also have "… = hd xs" using hd_conv_nth[OF assms(2)] by simp
finally show ?thesis by this
qed
lemma hd_drop[simp]:
assumes "n < length xs"
shows "hd (drop n xs) = xs ! n"
using hd_drop_conv_nth assms by this
lemma last_take[simp]:
assumes "n < length xs"
shows "last (take (Suc n) xs) = xs ! n"
using assms
proof (induct xs arbitrary: n)
case (Nil)
show ?case using Nil by simp
next
case (Cons x xs)
show ?case using Cons by (auto) (metis Suc_less_eq Suc_pred)
qed

lemma split_list_first_unique:
assumes "u⇩1 @ [a] @ u⇩2 = v⇩1 @ [a] @ v⇩2" "a ∉ set u⇩1" "a ∉ set v⇩1"
shows "u⇩1 = v⇩1"
proof -
obtain w where "u⇩1 = v⇩1 @ w ∧ w @ [a] @ u⇩2 = [a] @ v⇩2 ∨
u⇩1 @ w = v⇩1 ∧ [a] @ u⇩2 = w @ [a] @ v⇩2" using assms(1) append_eq_append_conv2 by blast
thus ?thesis using assms(2, 3) by (auto) (metis hd_append2 list.sel(1) list.set_sel(1))+
qed

end

# Theory 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

# Theory Set_Extensions

section ‹Sets›

theory Set_Extensions
imports
"HOL-Library.Infinite_Set"
begin

declare finite_subset[intro]

lemma set_not_emptyI[intro 0]: "x ∈ S ⟹ S ≠ {}" by auto
lemma sets_empty_iffI[intro 0]:
assumes "⋀ a. a ∈ A ⟹ ∃ b. b ∈ B"
assumes "⋀ b. b ∈ B ⟹ ∃ a. a ∈ A"
shows "A = {} ⟷ B = {}"
using assms by auto
lemma disjointI[intro 0]:
assumes "⋀ x. x ∈ A ⟹ x ∈ B ⟹ False"
shows "A ∩ B = {}"
using assms by auto
lemma range_subsetI[intro 0]:
assumes "⋀ x. f x ∈ S"
shows "range f ⊆ S"
using assms by blast

lemma finite_imageI_range:
assumes "finite (range f)"
shows "finite (f  A)"
using finite_subset image_mono subset_UNIV assms by metis

lemma inf_img_fin_domE':
assumes "infinite A"
assumes "finite (f  A)"
obtains y
where "y ∈ f  A" "infinite (A ∩ f - {y})"
proof (rule ccontr)
assume 1: "¬ thesis"
have 2: "finite (⋃ y ∈ f  A. A ∩ f - {y})"
proof (rule finite_UN_I)
show "finite (f  A)" using assms(2) by this
show "⋀ y. y ∈ f  A ⟹ finite (A ∩ f - {y})" using that 1 by blast
qed
have 3: "A ⊆ (⋃ y ∈ f  A. A ∩ f - {y})" by blast
show False using assms(1) 2 3 by blast
qed

lemma vimage_singleton[simp]: "f - {y} = {x. f x = y}" unfolding vimage_def by simp

lemma these_alt_def: "Option.these S = Some - S" unfolding Option.these_def by force
lemma the_vimage_subset: "the - {a} ⊆ {None, Some a}" by auto

lemma finite_induct_reverse[consumes 1, case_names remove]:
assumes "finite S"
assumes "⋀ S. finite S ⟹ (⋀ x. x ∈ S ⟹ P (S - {x})) ⟹ P S"
shows "P S"
using assms(1)
proof (induct rule: finite_psubset_induct)
case (psubset S)
show ?case
proof (rule assms(2))
show "finite S" using psubset(1) by this
next
fix x
assume 0: "x ∈ S"
show "P (S - {x})"
proof (rule psubset(2))
show "S - {x} ⊂ S" using 0 by auto
qed
qed
qed

lemma zero_not_in_Suc_image[simp]: "0 ∉ Suc  A" by auto

lemma Collect_split_Suc:
"¬ P 0 ⟹ {i. P i} = Suc  {i. P (Suc i)}"
"P 0 ⟹ {i. P i} = {0} ∪ Suc  {i. P (Suc i)}"
proof -
assume "¬ P 0"
thus "{i. P i} = Suc  {i. P (Suc i)}"
by (auto, metis image_eqI mem_Collect_eq nat.exhaust)
next
assume "P 0"
thus "{i. P i} = {0} ∪ Suc  {i. P (Suc i)}"
by (auto, metis imageI mem_Collect_eq not0_implies_Suc)
qed

lemma Collect_subsume[simp]:
assumes "⋀ x. x ∈ A ⟹ P x"
shows "{x ∈ A. P x} = A"
using assms unfolding simp_implies_def by auto

lemma Max_ge':
assumes "finite A" "A ≠ {}"
assumes "b ∈ A" "a ≤ b"
shows "a ≤ Max A"
using assms Max_ge_iff by auto

abbreviation "least A ≡ LEAST k. k ∈ A"

lemma least_contains[intro?, simp]:
fixes A :: "'a :: wellorder set"
assumes "k ∈ A"
shows "least A ∈ A"
using assms by (metis LeastI)
lemma least_contains'[intro?, simp]:
fixes A :: "'a :: wellorder set"
assumes "A ≠ {}"
shows "least A ∈ A"
using assms by (metis LeastI equals0I)
lemma least_least[intro?, simp]:
fixes A :: "'a :: wellorder set"
assumes "k ∈ A"
shows "least A ≤ k"
using assms by (metis Least_le)
lemma least_unique:
fixes A :: "'a :: wellorder set"
assumes "k ∈ A" "k ≤ least A"
shows "k = least A"
using assms by (metis Least_le antisym)
lemma least_not_less:
fixes A :: "'a :: wellorder set"
assumes "k < least A"
shows "k ∉ A"
using assms by (metis not_less_Least)
lemma leastI2_order[simp]:
fixes A :: "'a :: wellorder set"
assumes "A ≠ {}" "⋀ k. k ∈ A ⟹ (⋀ l. l ∈ A ⟹ k ≤ l) ⟹ P k"
shows "P (least A)"
proof (rule LeastI2_order)
show "least A ∈ A" using assms(1) by rule
next
fix k
assume 1: "k ∈ A"
show "least A ≤ k" using 1 by rule
next
fix k
assume 1: "k ∈ A" "∀ l. l ∈ A ⟶ k ≤ l"
show "P k" using assms(2) 1 by auto
qed

lemma least_singleton[simp]:
fixes a :: "'a :: wellorder"
shows "least {a} = a"
by (metis insert_not_empty least_contains' singletonD)

lemma least_image[simp]:
fixes f :: "'a :: wellorder ⇒ 'b :: wellorder"
assumes "A ≠ {}" "⋀ k l. k ∈ A ⟹ l ∈ A ⟹ k ≤ l ⟹ f k ≤ f l"
shows "least (f  A) = f (least A)"
proof (rule leastI2_order)
show "A ≠ {}" using assms(1) by this
next
fix k
assume 1: "k ∈ A" "⋀ i. i ∈ A ⟹ k ≤ i"
show "least (f  A) = f k"
proof (rule leastI2_order)
show "f  A ≠ {}" using assms(1) by simp
next
fix l
assume 2: "l ∈ f  A" "⋀ i. i ∈ f  A ⟹ l ≤ i"
show "l = f k" using assms(2) 1 2 by force
qed
qed

lemma least_le:
fixes A B :: "'a :: wellorder set"
assumes "B ≠ {}"
assumes "⋀ i. i ≤ least A ⟹ i ≤ least B ⟹ i ∈ B ⟹ i ∈ A"
shows "least A ≤ least B"
proof (rule ccontr)
assume 1: "¬ least A ≤ least B"
have 2: "least B ∈ A" using assms(1, 2) 1 by simp
have 3: "least A ≤ least B" using 2 by rule
show False using 1 3 by rule
qed
lemma least_eq:
fixes A B :: "'a :: wellorder set"
assumes "A ≠ {}" "B ≠ {}"
assumes "⋀ i. i ≤ least A ⟹ i ≤ least B ⟹ i ∈ A ⟷ i ∈ B"
shows "least A = least B"
using assms by (auto intro: antisym least_le)

lemma least_Suc[simp]:
assumes "A ≠ {}"
shows "least (Suc  A) = Suc (least A)"
proof (rule antisym)
obtain k where 10: "k ∈ A" using assms by blast
have 11: "Suc k ∈ Suc  A" using 10 by auto
have 20: "least A ∈ A" using 10 LeastI by metis
have 21: "least (Suc  A) ∈ Suc  A" using 11 LeastI by metis
have 30: "⋀ l. l ∈ A ⟹ least A ≤ l" using 10 Least_le by metis
have 31: "⋀ l. l ∈ Suc  A ⟹ least (Suc  A) ≤ l" using 11 Least_le by metis
show "least (Suc  A) ≤ Suc (least A)" using 20 31 by auto
show "Suc (least A) ≤ least (Suc  A)" using 21 30 by auto
qed

lemma least_Suc_diff[simp]: "Suc  A - {least (Suc  A)} = Suc  (A - {least A})"
proof (cases "A = {}")
case True
show ?thesis unfolding True by simp
next
case False
have "Suc  A - {least (Suc  A)} = Suc  A - {Suc (least A)}" using False by simp
also have "… = Suc  A - Suc  {least A}" by simp
also have "… = Suc  (A - {least A})" by blast
finally show ?thesis by this
qed

lemma Max_diff_least[simp]:
fixes A :: "'a :: wellorder set"
assumes "finite A" "A - {least A} ≠ {}"
shows "Max (A - {least A}) = Max A"
proof -
have 1: "least A ∈ A" using assms(2) by auto
obtain a where 2: "a ∈ A - {least A}" using assms(2) by blast
have "Max A = Max (insert (least A) (A - {least A}))" using insert_absorb 1 by force
also have "… = max (least A) (Max (A - {least A}))"
proof (rule Max_insert)
show "finite (A - {least A})" using assms(1) by auto
show "A - {least A} ≠ {}" using assms(2) by this
qed
also have "… = Max (A - {least A})"
proof (rule max_absorb2, rule Max_ge')
show "finite (A - {least A})" using assms(1) by auto
show "A - {least A} ≠ {}" using assms(2) by this
show "a ∈ A - {least A}" using 2 by this
show "least A ≤ a" using 2 by simp
qed
finally show ?thesis by rule
qed

lemma nat_set_card_equality_less:
fixes A :: "nat set"
assumes "x ∈ A" "y ∈ A" "card {z ∈ A. z < x} = card {z ∈ A. z < y}"
shows "x = y"
proof (cases x y rule: linorder_cases)
case less
have 0: "finite {z ∈ A. z < y}" by simp
have 1: "{z ∈ A. z < x} ⊂ {z ∈ A. z < y}" using assms(1, 2) less by force
have 2: "card {z ∈ A. z < x} < card {z ∈ A. z < y}" using psubset_card_mono 0 1 by this
show ?thesis using assms(3) 2 by simp
next
case equal
show ?thesis using equal by this
next
case greater
have 0: "finite {z ∈ A. z < x}" by simp
have 1: "{z ∈ A. z < y} ⊂ {z ∈ A. z < x}" using assms(1, 2) greater by force
have 2: "card {z ∈ A. z < y} < card {z ∈ A. z < x}" using psubset_card_mono 0 1 by this
show ?thesis using assms(3) 2 by simp
qed

lemma nat_set_card_equality_le:
fixes A :: "nat set"
assumes "x ∈ A" "y ∈ A" "card {z ∈ A. z ≤ x} = card {z ∈ A. z ≤ y}"
shows "x = y"
proof (cases x y rule: linorder_cases)
case less
have 0: "finite {z ∈ A. z ≤ y}" by simp
have 1: "{z ∈ A. z ≤ x} ⊂ {z ∈ A. z ≤ y}" using assms(1, 2) less by force
have 2: "card {z ∈ A. z ≤ x} < card {z ∈ A. z ≤ y}" using psubset_card_mono 0 1 by this
show ?thesis using assms(3) 2 by simp
next
case equal
show ?thesis using equal by this
next
case greater
have 0: "finite {z ∈ A. z ≤ x}" by simp
have 1: "{z ∈ A. z ≤ y} ⊂ {z ∈ A. z ≤ x}" using assms(1, 2) greater by force
have 2: "card {z ∈ A. z ≤ y} < card {z ∈ A. z ≤ x}" using psubset_card_mono 0 1 by this
show ?thesis using assms(3) 2 by simp
qed

lemma nat_set_card_mono[simp]:
fixes A :: "nat set"
assumes "x ∈ A"
shows "card {z ∈ A. z < x} < card {z ∈ A. z < y} ⟷ x < y"
proof
assume 1: "card {z ∈ A. z < x} < card {z ∈ A. z < y}"
show "x < y"
proof (rule ccontr)
assume 2: "¬ x < y"
have 3: "card {z ∈ A. z < y} ≤ card {z ∈ A. z < x}" using 2 by (auto intro: card_mono)
show "False" using 1 3 by simp
qed
next
assume 1: "x < y"
show "card {z ∈ A. z < x} < card {z ∈ A. z < y}"
proof (intro psubset_card_mono psubsetI)
show "finite {z ∈ A. z < y}" by simp
show "{z ∈ A. z < x} ⊆ {z ∈ A. z < y}" using 1 by auto
show "{z ∈ A. z < x} ≠ {z ∈ A. z < y}" using assms 1 by blast
qed
qed

lemma card_one[elim]:
assumes "card A = 1"
obtains a
where "A = {a}"
using assms by (metis One_nat_def card_Suc_eq)

lemma image_alt_def: "f  A = {f x |x. x ∈ A}" by auto

lemma supset_mono_inductive[mono]:
assumes "⋀ x. x ∈ B ⟶ x ∈ C"
shows "A ⊆ B ⟶ A ⊆ C"
using assms by auto
lemma Collect_mono_inductive[mono]:
assumes "⋀ x. P x ⟶ Q x"
shows "x ∈ {x. P x} ⟶ x ∈ {x. Q x}"
using assms by auto

lemma image_union_split:
assumes "f  (A ∪ B) = g  C"
obtains D E
where "f  A = g  D" "f  B = g  E" "D ⊆ C" "E ⊆ C"
using assms unfolding image_Un
by (metis (erased, lifting) inf_sup_ord(3) inf_sup_ord(4) subset_imageE)
lemma image_insert_split:
assumes "inj g" "f  insert a B = g  C"
obtains d E
where "f a = g d" "f  B = g  E" "d ∈ C" "E ⊆ C"
proof -
have 1: "f  ({a} ∪ B) = g  C" using assms(2) by simp
obtain D E where 2: "f  {a} = g  D" "f  B = g  E" "D ⊆ C" "E ⊆ C"
using image_union_split 1 by this
obtain d where 3: "D = {d}" using assms(1) 2(1) by (auto, metis (erased, hide_lams) imageE
image_empty image_insert inj_image_eq_iff singletonI)
show ?thesis using that 2 unfolding 3 by simp
qed

end

# Theory Basic_Extensions

section ‹Basics›

theory Basic_Extensions
imports "HOL-Library.Infinite_Set"
begin

subsection ‹Types›

type_synonym 'a step = "'a ⇒ 'a"

subsection ‹Rules›

declare less_imp_le[dest, simp]

declare le_funI[intro]
declare le_funE[elim]
declare le_funD[dest]

lemma IdI'[intro]:
assumes "x = y"
shows "(x, y) ∈ Id"
using assms by auto

lemma (in order) order_le_cases:
assumes "x ≤ y"
obtains (eq) "x = y" | (lt) "x < y"
using assms le_less by auto

lemma (in linorder) linorder_cases':
obtains (le) "x ≤ y" | (gt) "x > y"
by force

lemma monoI_comp[intro]:
assumes "mono f" "mono g"
shows "mono (f ∘ g)"
using assms by (intro monoI, auto dest: monoD)
lemma strict_monoI_comp[intro]:
assumes "strict_mono f" "strict_mono g"
shows "strict_mono (f ∘ g)"
using assms by (intro strict_monoI, auto dest: strict_monoD)

lemma eq_le_absorb[simp]:
fixes x y :: "'a :: order"
shows "x = y ∧ x ≤ y ⟷ x = y" "x ≤ y ∧ x = y ⟷ x = y"
by auto

lemma INFM_Suc[simp]: "(∃⇩∞ i. P (Suc i)) ⟷ (∃⇩∞ i. P i)"
unfolding INFM_nat using Suc_lessE less_Suc_eq by metis
lemma INFM_plus[simp]: "(∃⇩∞ i. P (i + n :: nat)) ⟷ (∃⇩∞ i. P i)"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
have "(∃⇩∞ i. P (i + Suc n)) ⟷ (∃⇩∞ i. P (Suc i + n))" by simp
also have "… ⟷ (∃⇩∞ i. P (i + n))" using INFM_Suc by this
also have "… ⟷ (∃⇩∞ i. P i)" using Suc by this
finally show ?case by this
qed
lemma INFM_minus[simp]: "(∃⇩∞ i. P (i - n :: nat)) ⟷ (∃⇩∞ i. P i)"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
have "(∃⇩∞ i. P (i - Suc n)) ⟷ (∃⇩∞ i. P (Suc i - Suc n))" using INFM_Suc by meson
also have "… ⟷ (∃⇩∞ i. P (i - n))" by simp
also have "… ⟷ (∃⇩∞ i. P i)" using Suc by this
finally show ?case by this
qed

subsection ‹Constants›

definition const :: "'a ⇒ 'b ⇒ 'a"
where "const x ≡ λ _. x"
definition const2 :: "'a ⇒ 'b ⇒ 'c ⇒ 'a"
where "const2 x ≡ λ _ _. x"
definition const3 :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'a"
where "const3 x ≡ λ _ _ _. x"
definition const4 :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'a"
where "const4 x ≡ λ _ _ _ _. x"
definition const5 :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'f ⇒ 'a"
where "const5 x ≡ λ _ _ _ _ _. x"

lemma const_apply[simp]: "const x y = x" unfolding const_def by rule
lemma const2_apply[simp]: "const2 x y z = x" unfolding const2_def by rule
lemma const3_apply[simp]: "const3 x y z u = x" unfolding const3_def by rule
lemma const4_apply[simp]: "const4 x y z u v = x" unfolding const4_def by rule
lemma const5_apply[simp]: "const5 x y z u v w = x" unfolding const5_def by rule

definition zip_fun :: "('a ⇒ 'b) ⇒ ('a ⇒ 'c) ⇒ 'a ⇒ 'b × 'c" (infixr "∥" 51)
where "f ∥ g ≡ λ x. (f x, g x)"

lemma zip_fun_simps[simp]:
"(f ∥ g) x = (f x, g x)"
"fst ∘ (f ∥ g) = f"
"snd ∘ (f ∥ g) = g"
"fst ∘ h ∥ snd ∘ h = h"
"fst  range (f ∥ g) = range f"
"snd  range (f ∥ g) = range g"
unfolding zip_fun_def by force+

lemma zip_fun_eq[dest]:
assumes "f ∥ g = h ∥ i"
shows "f = h" "g = i"
using assms unfolding zip_fun_def by (auto dest: fun_cong)

lemma zip_fun_range_subset[intro, simp]: "range (f ∥ g) ⊆ range f × range g"
unfolding zip_fun_def by blast
lemma zip_fun_range_finite[elim]:
assumes "finite (range (f ∥ g))"
obtains "finite (range f)" "finite (range g)"
proof
show "finite (range f)" using finite_imageI [OF assms(1), of fst]
show "finite (range g)" using finite_imageI [OF assms(1), of snd]
qed

lemma zip_fun_split:
obtains f g
where "h = f ∥ g"
proof
show "h = fst ∘ h ∥ snd ∘ h" by simp
qed

abbreviation "None_None ≡ (None, None)"
abbreviation "None_Some ≡ λ (y). (None, Some y)"
abbreviation "Some_None ≡ λ (x). (Some x, None)"
abbreviation "Some_Some ≡ λ (x, y). (Some x, Some y)"

abbreviation "None_None_None ≡ (None, None, None)"
abbreviation "None_None_Some ≡ λ (z). (None, None, Some z)"
abbreviation "None_Some_None ≡ λ (y). (None, Some y, None)"
abbreviation "None_Some_Some ≡ λ (y, z). (None, Some y, Some z)"
abbreviation "Some_None_None ≡ λ (x). (Some x, None, None)"
abbreviation "Some_None_Some ≡ λ (x, z). (Some x, None, Some z)"
abbreviation "Some_Some_None ≡ λ (x, y). (Some x, Some y, None)"
abbreviation "Some_Some_Some ≡ λ (x, y, z). (Some x, Some y, Some z)"

lemma inj_Some2[simp, intro]:
"inj None_Some"
"inj Some_None"
"inj Some_Some"
by (rule injI, force)+

lemma inj_Some3[simp, intro]:
"inj None_None_Some"
"inj None_Some_None"
"inj None_Some_Some"
"inj Some_None_None"
"inj Some_None_Some"
"inj Some_Some_None"
"inj Some_Some_Some"
by (rule injI, force)+

definition swap :: "'a × 'b ⇒ 'b × 'a"
where "swap x ≡ (snd x, fst x)"

lemma swap_simps[simp]: "swap (a, b) = (b, a)" unfolding swap_def by simp
lemma swap_inj[intro, simp]: "inj swap" by (rule injI, auto)
lemma swap_surj[intro, simp]: "surj swap" by (rule surjI[where ?f = swap], auto)
lemma swap_bij[intro, simp]: "bij swap" by (rule bijI, auto)

definition push :: "('a × 'b) × 'c ⇒ 'a × 'b × 'c"
where "push x ≡ (fst (fst x), snd (fst x), snd x)"
definition pull :: "'a × 'b × 'c ⇒ ('a × 'b) × 'c"
where "pull x ≡ ((fst x, fst (snd x)), snd (snd x))"

lemma push_simps[simp]: "push ((x, y), z) = (x, y, z)" unfolding push_def by simp
lemma pull_simps[simp]: "pull (x, y, z) = ((x, y), z)" unfolding pull_def by simp

definition label :: "'vertex × 'label × 'vertex ⇒ 'label"
where "label ≡ fst ∘ snd"

lemma label_select[simp]: "label (p, a, q) = a" unfolding label_def by simp

subsection ‹Theorems for @term{curry} and @term{split}›

lemma curry_split[simp]: "curry ∘ case_prod = id" by auto
lemma split_curry[simp]: "case_prod ∘ curry = id" by auto

lemma curry_le[simp]: "curry f ≤ curry g ⟷ f ≤ g" unfolding le_fun_def by force
lemma split_le[simp]: "case_prod f ≤ case_prod g ⟷ f ≤ g" unfolding le_fun_def by force

lemma mono_curry_left[simp]: "mono (curry ∘ h) ⟷ mono h"
unfolding mono_def by fastforce
lemma mono_split_left[simp]: "mono (case_prod ∘ h) ⟷ mono h"
unfolding mono_def by fastforce
lemma mono_curry_right[simp]: "mono (h ∘ curry) ⟷ mono h"
unfolding mono_def split_le[symmetric] by bestsimp
lemma mono_split_right[simp]: "mono (h ∘ case_prod) ⟷ mono h"
unfolding mono_def curry_le[symmetric] by bestsimp

lemma Collect_curry[simp]: "{x. P (curry x)} = case_prod  {x. P x}" using image_Collect by fastforce
lemma Collect_split[simp]: "{x. P (case_prod x)} = curry  {x. P x}" using image_Collect by force

lemma gfp_split_curry[simp]: "gfp (case_prod ∘ f ∘ curry) = case_prod (gfp f)"
proof -
have "gfp (case_prod ∘ f ∘ curry) = Sup {u. u ≤ case_prod (f (curry u))}" unfolding gfp_def by simp
also have "… = Sup {u. curry u ≤ curry (case_prod (f (curry u)))}" unfolding curry_le by simp
also have "… = Sup {u. curry u ≤ f (curry u)}" by simp
also have "… = Sup (case_prod  {u. u ≤ f u})" unfolding Collect_curry[of "λ u. u ≤ f u"] by simp
also have "… = case_prod (Sup {u. u ≤ f u})" by (force simp add: image_comp)
also have "… = case_prod (gfp f)" unfolding gfp_def by simp
finally show ?thesis by this
qed
lemma gfp_curry_split[simp]: "gfp (curry ∘ f ∘ case_prod) = curry (gfp f)"
proof -
have "gfp (curry ∘ f ∘ case_prod) = Sup {u. u ≤ curry (f (case_prod u))}" unfolding gfp_def by simp
also have "… = Sup {u. case_prod u ≤ case_prod (curry (f (case_prod u)))}" unfolding split_le by simp
also have "… = Sup {u. case_prod u ≤ f (case_prod u)}" by simp
also have "… = Sup (curry  {u. u ≤ f u})" unfolding Collect_split[of "λ u. u ≤ f u"] by simp
also have "… = curry (Sup {u. u ≤ f u})" by (force simp add: image_comp)
also have "… = curry (gfp f)" unfolding gfp_def by simp
finally show ?thesis by this
qed

lemma not_someI:
assumes "⋀ x. P x ⟹ False"
shows "¬ P (SOME x. P x)"
using assms by blast
lemma some_ccontr:
assumes "(⋀ x. ¬ P x) ⟹ False"
shows "P (SOME x. P x)"
using assms someI_ex ccontr by metis

end

# Theory Relation_Extensions

section ‹Relations›

theory Relation_Extensions
imports
Basic_Extensions
begin

abbreviation rev_lex_prod (infixr "<*rlex*>" 80)
where "r⇩1 <*rlex*> r⇩2 ≡ inv_image (r⇩2 <*lex*> r⇩1) swap"

lemmas sym_rtranclp[intro] = sym_rtrancl[to_pred]

definition liftablep :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool"
where "liftablep r f ≡ ∀ x y. r x y ⟶ r (f x) (f y)"

lemma liftablepI[intro]:
assumes "⋀ x y. r x y ⟹ r (f x) (f y)"
shows "liftablep r f"
using assms
unfolding liftablep_def
by simp
lemma liftablepE[elim]:
assumes "liftablep r f"
assumes "r x y"
obtains "r (f x) (f y)"
using assms
unfolding liftablep_def
by simp

lemma liftablep_rtranclp:
assumes "liftablep r f"
shows "liftablep r⇧*⇧* f"
proof
fix x y
assume "r⇧*⇧* x y"
thus "r⇧*⇧* (f x) (f y)"
using assms
by (induct rule: rtranclp_induct, force+)
qed

definition confluentp :: "('a ⇒ 'a ⇒ bool) ⇒ bool"
where "confluentp r ≡ ∀ x y1 y2. r⇧*⇧* x y1 ⟶ r⇧*⇧* x y2 ⟶ (∃ z. r⇧*⇧* y1 z ∧ r⇧*⇧* y2 z)"

lemma confluentpI[intro]:
assumes "⋀ x y1 y2. r⇧*⇧* x y1 ⟹ r⇧*⇧* x y2 ⟹ ∃ z. r⇧*⇧* y1 z ∧ r⇧*⇧* y2 z"
shows "confluentp r"
using assms
unfolding confluentp_def
by simp

lemma confluentpE[elim]:
assumes "confluentp r"
assumes "r⇧*⇧* x y1" "r⇧*⇧* x y2"
obtains z
where "r⇧*⇧* y1 z" "r⇧*⇧* y2 z"
using assms
unfolding confluentp_def
by blast

lemma confluentpI'[intro]:
assumes "⋀ x y1 y2. r⇧*⇧* x y1 ⟹ r x y2 ⟹ ∃ z. r⇧*⇧* y1 z ∧ r⇧*⇧* y2 z"
shows "confluentp r"
proof
fix x y1 y2
assume "r⇧*⇧* x y1" "r⇧*⇧* x y2"
thus "∃ z. r⇧*⇧* y1 z ∧ r⇧*⇧* y2 z" using assms by (induct rule: rtranclp_induct, force+)
qed

lemma transclp_eq_implies_confluent_imp:
assumes "r1⇧*⇧* = r2⇧*⇧*"
assumes "confluentp r1"
shows "confluentp r2"
using assms
by force

lemma transclp_eq_implies_confluent_eq:
assumes "r1⇧*⇧* = r2⇧*⇧*"
shows "confluentp r1 ⟷ confluentp r2"
using assms transclp_eq_implies_confluent_imp
by metis

definition diamondp :: "('a ⇒ 'a ⇒ bool) ⇒ bool"
where "diamondp r ≡ ∀ x y1 y2. r x y1 ⟶ r x y2 ⟶ (∃ z. r y1 z ∧ r y2 z)"

lemma diamondpI[intro]:
assumes "⋀ x y1 y2. r x y1 ⟹ r x y2 ⟹ ∃ z. r y1 z ∧ r y2 z"
shows "diamondp r"
using assms
unfolding diamondp_def
by simp

lemma diamondpE[elim]:
assumes "diamondp r"
assumes "r x y1" "r x y2"
obtains z
where "r y1 z" "r y2 z"
using assms
unfolding diamondp_def
by blast

lemma diamondp_implies_confluentp:
assumes "diamondp r"
shows "confluentp r"
proof (rule confluentpI')
fix x y1 y2
assume "r⇧*⇧* x y1" "r x y2"
hence "∃ z. r y1 z ∧ r⇧*⇧* y2 z" using assms by (induct rule: rtranclp_induct, force+)
thus "∃ z. r⇧*⇧* y1 z ∧ r⇧*⇧* y2 z" by blast
qed

locale wellfounded_relation =
fixes R :: "'a ⇒ 'a ⇒ bool"
assumes wellfounded: "wfP R"

end



# Theory Transition_System_Extensions

section ‹Transition Systems›

theory Transition_System_Extensions
imports
"Basics/Word_Prefixes"
"Extensions/Set_Extensions"
"Extensions/Relation_Extensions"
Transition_Systems_and_Automata.Transition_System
Transition_Systems_and_Automata.Transition_System_Extra
Transition_Systems_and_Automata.Transition_System_Construction
begin

context transition_system_initial
begin

definition cycles :: "'state ⇒ 'transition list set"
where "cycles p ≡ {w. path w p ∧ target w p = p}"

lemma cyclesI[intro!]:
assumes "path w p" "target w p = p"
shows "w ∈ cycles p"
using assms unfolding cycles_def by auto
lemma cyclesE[elim!]:
assumes "w ∈ cycles p"
obtains "path w p" "target w p = p"
using assms unfolding cycles_def by auto

inductive_set executable :: "'transition set"
where executable: "p ∈ nodes ⟹ enabled a p ⟹ a ∈ executable"

lemma executableI_step[intro!]:
assumes "p ∈ nodes" "enabled a p"
shows "a ∈ executable"
using executable assms by this
lemma executableI_words_fin[intro!]:
assumes "p ∈ nodes" "path w p"
shows "set w ⊆ executable"
using assms by (induct w arbitrary: p, auto del: subsetI)
lemma executableE[elim?]:
assumes "a ∈ executable"
obtains p
where "p ∈ nodes" "enabled a p"
using assms by induct auto

end

locale transition_system_interpreted =
transition_system ex en
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and int :: "'state ⇒ 'interpretation"
begin

definition visible :: "'action set"
where "visible ≡ {a. ∃ q. en a q ∧ int q ≠ int (ex a q)}"

lemma visibleI[intro]:
assumes "en a q" "int q ≠ int (ex a q)"
shows "a ∈ visible"
using assms unfolding visible_def by auto
lemma visibleE[elim]:
assumes "a ∈ visible"
obtains q
where "en a q" "int q ≠ int (ex a q)"
using assms unfolding visible_def by auto

abbreviation "invisible ≡ - visible"

lemma execute_fin_word_invisible:
assumes "path w p" "set w ⊆ invisible"
shows "int (target w p) = int p"
using assms by (induct w arbitrary: p rule: list.induct, auto)
lemma execute_inf_word_invisible:
assumes "run w p" "k ≤ l" "⋀ i. k ≤ i ⟹ i < l ⟹ w !! i ∉ visible"
shows "int ((p ## trace w p) !! k) = int ((p ## trace w p) !! l)"
proof -
have "(p ## trace w p) !! l = target (stake l w) p" by simp
also have "stake l w = stake k w @ stake (l - k) (sdrop k w)" using assms(2) by simp
also have "target … p = target (stake (l - k) (sdrop k w)) (target (stake k w) p)"
unfolding fold_append comp_apply by rule
also have "int … = int (target (stake k w) p)"
proof (rule execute_fin_word_invisible)
have "w = stake l w @- sdrop l w" by simp
also have "stake l w = stake k w @ stake (l - k) (sdrop k w)" using assms(2) by simp
finally have 1: "run (stake k w @- stake (l - k) (sdrop k w) @- sdrop l w) p"
unfolding shift_append using assms(1) by simp
show "path (stake (l - k) (sdrop k w)) (target (stake k w) p)" using 1 by auto
show "set (stake (l - k) (sdrop k w)) ⊆ invisible" using assms(3) by (auto simp: set_stake_snth)
qed
also have "… = int ((p ## trace w p) !! k)" by simp
finally show ?thesis by rule
qed

end

locale transition_system_complete =
transition_system_initial ex en init +
transition_system_interpreted ex en int
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and init :: "'state ⇒ bool"
and int :: "'state ⇒ 'interpretation"
begin

definition language :: "'interpretation stream set"
where "language ≡ {smap int (p ## trace w p) |p w. init p ∧ run w p}"

lemma languageI[intro!]:
assumes "w = smap int (p ## trace v p)" "init p" "run v p"
shows "w ∈ language"
using assms unfolding language_def by auto
lemma languageE[elim!]:
assumes "w ∈ language"
obtains p v
where "w = smap int (p ## trace v p)" "init p" "run v p"
using assms unfolding language_def by auto

end

locale transition_system_finite_nodes =
transition_system_initial ex en init
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and init :: "'state ⇒ bool"
+
assumes reachable_finite: "finite nodes"

locale transition_system_cut =
transition_system_finite_nodes ex en init
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and init :: "'state ⇒ bool"
+
fixes cuts :: "'action set"
assumes cycles_cut: "p ∈ nodes ⟹ w ∈ cycles p ⟹ w ≠ [] ⟹ set w ∩ cuts ≠ {}"
begin

inductive scut :: "'state ⇒ 'state ⇒ bool"
where scut: "p ∈ nodes ⟹ en a p ⟹ a ∉ cuts ⟹ scut p (ex a p)"

declare scut.intros[intro!]
declare scut.cases[elim!]

lemma scut_reachable:
assumes "scut p q"
shows "p ∈ nodes" "q ∈ nodes"
using assms by auto
lemma scut_trancl:
assumes "scut⇧+⇧+ p q"
obtains w
where "path w p" "target w p = q" "set w ∩ cuts = {}" "w ≠ []"
using assms
proof (induct arbitrary: thesis)
case (base q)
show ?case using base by force
next
case (step q r)
obtain w where 1: "path w p" "target w p = q" "set w ∩ cuts = {}" "w ≠ []"
using step(3) by this
obtain a where 2: "en a q" "a ∉ cuts" "ex a q = r" using step(2) by auto
show ?case
proof (rule step(4))
show "path (w @ [a]) p" using 1 2 by auto
show "target (w @ [a]) p = r" using 1 2 by auto
show "set (w @ [a]) ∩ cuts = {}" using 1 2 by auto
show "w @ [a] ≠ []" by auto
qed
qed

sublocale wellfounded_relation "scut¯¯"
proof (unfold_locales, intro finite_acyclic_wf_converse[to_pred] acyclicI[to_pred], safe)
have 1: "{(p, q). scut p q} ⊆ nodes × nodes" using scut_reachable by blast
have 2: "finite (nodes × nodes)"
using finite_cartesian_product reachable_finite by blast
show "finite {(p, q). scut p q}" using 1 2 by blast
next
fix p
assume 1: "scut⇧+⇧+ p p"
have 2: "p ∈ nodes" using 1 tranclE[to_pred] scut_reachable by metis
obtain w where 3: "path w p" "target w p = p" "set w ∩ cuts = {}" "w ≠ []"
using scut_trancl 1 by this
have 4: "w ∈ cycles p" using 3(1, 2) by auto
have 5: "set w ∩ cuts ≠ {}" using cycles_cut 2 4 3(4) by this
show "False" using 3(3) 5 by simp
qed

lemma no_cut_scut:
assumes "p ∈ nodes" "en a p" "a ∉ cuts"
shows "scut¯¯ (ex a p) p"
using assms by auto

end

locale transition_system_sticky =
transition_system_complete ex en init int +
transition_system_cut ex en init sticky
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and init :: "'state ⇒ bool"
and int :: "'state ⇒ 'interpretation"
and sticky :: "'action set"
+
assumes executable_visible_sticky: "executable ∩ visible ⊆ sticky"

end


# Theory Traces

section ‹Trace Theory›

theory Traces
imports "Basics/Word_Prefixes"
begin

locale traces =
fixes ind :: "'item ⇒ 'item ⇒ bool"
assumes independence_symmetric[sym]: "ind a b ⟹ ind b a"
begin

abbreviation Ind :: "'item set ⇒ 'item set ⇒ bool"
where "Ind A B ≡ ∀ a ∈ A. ∀ b ∈ B. ind a b"

inductive eq_swap :: "'item list ⇒ 'item list ⇒ bool" (infix "=⇩S" 50)
where swap: "ind a b ⟹ u @ [a] @ [b] @ v =⇩S u @ [b] @ [a] @ v"

declare eq_swap.intros[intro]
declare eq_swap.cases[elim]

lemma eq_swap_sym[sym]: "v =⇩S w ⟹ w =⇩S v" using independence_symmetric by auto

lemma eq_swap_length[dest]: "w⇩1 =⇩S w⇩2 ⟹ length w⇩1 = length w⇩2" by force
lemma eq_swap_range[dest]: "w⇩1 =⇩S w⇩2 ⟹ set w⇩1 = set w⇩2" by force

lemma eq_swap_extend:
assumes "w⇩1 =⇩S w⇩2"
shows "u @ w⇩1 @ v =⇩S u @ w⇩2 @ v"
using assms
proof induct
case (swap a b u' v')
have "u @ (u' @ [a] @ [b] @ v') @ v = (u @ u') @ [a] @ [b] @ (v' @ v)" by simp
also have "… =⇩S (u @ u') @ [b] @ [a] @ (v' @ v)" using swap by blast
also have "… = u @ (u' @ [b] @ [a] @ v') @ v" by simp
finally show ?case by this
qed

lemma eq_swap_remove1:
assumes "w⇩1 =⇩S w⇩2"
obtains (equal) "remove1 c w⇩1 = remove1 c w⇩2" | (swap) "remove1 c w⇩1 =⇩S remove1 c w⇩2"
using assms
proof induct
case (swap a b u v)
have "c ∉ set (u @ [a] @ [b] @ v) ∨
c ∈ set u ∨
c ∉ set u ∧ c = a ∨
c ∉ set u ∧ c ≠ a ∧ c = b ∨
c ∉ set u ∧ c ≠ a ∧ c ≠ b ∧ c ∈ set v"
by auto
thus ?case
proof (elim disjE)
assume 0: "c ∉ set (u @ [a] @ [b] @ v)"
have 1: "c ∉ set (u @ [b] @ [a] @ v)" using 0 by auto
have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [a] @ [b] @ v" using remove1_idem 0 by this
have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [b] @ [a] @ v" using remove1_idem 1 by this
have 4: "remove1 c (u @ [a] @ [b] @ v) =⇩S remove1 c (u @ [b] @ [a] @ v)"
unfolding 2 3 using eq_swap.intros swap(1) by this
show thesis using swap(3) 4 by this
next
assume 0: "c ∈ set u"
have 2: "remove1 c (u @ [a] @ [b] @ v) = remove1 c u @ [a] @ [b] @ v"
unfolding remove1_append using 0 by simp
have 3: "remove1 c (u @ [b] @ [a] @ v) = remove1 c u @ [b] @ [a] @ v"
unfolding remove1_append using 0 by simp
have 4: "remove1 c (u @ [a] @ [b] @ v) =⇩S remove1 c (u @ [b] @ [a] @ v)"
unfolding 2 3 using eq_swap.intros swap(1) by this
show thesis using swap(3) 4 by this
next
assume 0: "c ∉ set u ∧ c = a"
have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [b] @ v"
unfolding remove1_append using remove1_idem 0 by auto
have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [b] @ v"
unfolding remove1_append using remove1_idem 0 by auto
have 4: "remove1 c (u @ [a] @ [b] @ v) = remove1 c (u @ [b] @ [a] @ v)"
unfolding 2 3 by rule
show thesis using swap(2) 4 by this
next
assume 0: "c ∉ set u ∧ c ≠ a ∧ c = b"
have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [a] @ v"
unfolding remove1_append using remove1_idem 0 by auto
have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [a] @ v"
unfolding remove1_append using remove1_idem 0 by auto
have 4: "remove1 c (u @ [a] @ [b] @ v) = remove1 c (u @ [b] @ [a] @ v)"
unfolding 2 3 by rule
show thesis using swap(2) 4 by this
next
assume 0: "c ∉ set u ∧ c ≠ a ∧ c ≠ b ∧ c ∈ set v"
have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [a] @ [b] @ remove1 c v"
unfolding remove1_append using 0 by simp
have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [b] @ [a] @ remove1 c v"
unfolding remove1_append using 0 by simp
have 4: "remove1 c (u @ [a] @ [b] @ v) =⇩S remove1 c (u @ [b] @ [a] @ v)"
unfolding 2 3 using eq_swap.intros swap(1) by this
show ?thesis using swap(3) 4 by this
qed
qed

lemma eq_swap_rev:
assumes "w⇩1 =⇩S w⇩2"
shows "rev w⇩1 =⇩S rev w⇩2"
using assms
proof induct
case (swap a b u v)
have 1: "rev v @ [a] @ [b] @ rev u =⇩S rev v @ [b] @ [a] @ rev u" using swap by blast
have 2: "rev v @ [b] @ [a] @ rev u =⇩S rev v @ [a] @ [b] @ rev u" using 1 eq_swap_sym by blast
show ?case using 2 by simp
qed

abbreviation eq_fin :: "'item list ⇒ 'item list ⇒ bool" (infix "=⇩F" 50)
where "eq_fin ≡ eq_swap⇧*⇧*"

lemma eq_fin_symp[intro, sym]: "u =⇩F v ⟹ v =⇩F u"
using eq_swap_sym sym_rtrancl[to_pred] unfolding symp_def by metis

lemma eq_fin_length[dest]: "w⇩1 =⇩F w⇩2 ⟹ length w⇩1 = length w⇩2"
by (induct rule: rtranclp.induct, auto)
lemma eq_fin_range[dest]: "w⇩1 =⇩F w⇩2 ⟹ set w⇩1 = set w⇩2"
by (induct rule: rtranclp.induct, auto)

lemma eq_fin_remove1:
assumes "w⇩1 =⇩F w⇩2"
shows "remove1 c w⇩1 =⇩F remove1 c w⇩2"
using assms
proof induct
case (base)
show ?case by simp
next
case (step w⇩2 w⇩3)
show ?case
using step(2)
proof (cases rule: eq_swap_remove1[where ?c = c])
case equal
show ?thesis using step equal by simp
next
case swap
show ?thesis using step swap by auto
qed
qed

lemma eq_fin_rev:
assumes "w⇩1 =⇩F w⇩2"
shows "rev w⇩1 =⇩F rev w⇩2"
using assms by (induct, auto dest: eq_swap_rev)

lemma eq_fin_concat_eq_fin_start:
assumes "u @ v⇩1 =⇩F u @ v⇩2"
shows "v⇩1 =⇩F v⇩2"
using assms
proof (induct u arbitrary: v⇩1 v⇩2 rule: rev_induct)
case (Nil)
show ?case using Nil by simp
next
case (snoc a u)
have 1: "u @ [a] @ v⇩1 =⇩F u @ [a] @ v⇩2" using snoc(2) by simp
have 2: "[a] @ v⇩1 =⇩F [a] @ v⇩2" using snoc(1) 1 by this
show ?case using eq_fin_remove1[OF 2, of a] by simp
qed

lemma eq_fin_concat: "u @ w⇩1 @ v =⇩F u @ w⇩2 @ v ⟷ w⇩1 =⇩F w⇩2"
proof
assume 0: "u @ w⇩1 @ v =⇩F u @ w⇩2 @ v"
have 1: "w⇩1 @ v =⇩F w⇩2 @ v" using eq_fin_concat_eq_fin_start 0 by this
have 2: "rev (w⇩1 @ v) =⇩F rev (w⇩2 @ v)" using 1 by (blast dest: eq_fin_rev)
have 3: "rev v @ rev w⇩1 =⇩F rev v @ rev w⇩2" using 2 by simp
have 4: "rev w⇩1 =⇩F rev w⇩2" using eq_fin_concat_eq_fin_start 3 by this
have 5: "rev (rev w⇩1) =⇩F rev (rev w⇩2)" using 4 by (blast dest: eq_fin_rev)
show "w⇩1 =⇩F w⇩2" using 5 by simp
next
show "u @ w⇩1 @ v =⇩F u @ w⇩2 @ v" if "w⇩1 =⇩F w⇩2"
using that by (induct, auto dest: eq_swap_extend[of _ _ u v])
qed
lemma eq_fin_concat_start[iff]: "w @ w⇩1 =⇩F w @ w⇩2 ⟷ w⇩1 =⇩F w⇩2"
using eq_fin_concat[of "w" _ "[]"] by simp
lemma eq_fin_concat_end[iff]: "w⇩1 @ w =⇩F w⇩2 @ w ⟷ w⇩1 =⇩F w⇩2"
using eq_fin_concat[of "[]" _ "w"] by simp

lemma ind_eq_fin':
assumes "Ind {a} (set v)"
shows "[a] @ v =⇩F v @ [a]"
using assms
proof (induct v)
case (Nil)
show ?case by simp
next
case (Cons b v)
have 1: "Ind {a} (set v)" using Cons(2) by auto
have 2: "ind a b" using Cons(2) by auto
have "[a] @ b # v = [a] @ [b] @ v" by simp
also have "… =⇩S [b] @ [a] @ v" using eq_swap.intros[OF 2, of "[]"] by auto
also have "… =⇩F [b] @ v @ [a]" using Cons(1) 1 by blast
also have "… = (b # v) @ [a]" by simp
finally show ?case by this
qed

lemma ind_eq_fin[intro]:
assumes "Ind (set u) (set v)"
shows "u @ v =⇩F v @ u"
using assms
proof (induct u)
case (Nil)
show ?case by simp
next
case (Cons a u)
have 1: "Ind (set u) (set v)" using Cons(2) by auto
have 2: "Ind {a} (set v)" using Cons(2) by auto
have "(a # u) @ v = [a] @ u @ v" by simp
also have "… =⇩F [a] @ v @ u" using Cons(1) 1 by blast
also have "… = ([a] @ v) @ u" by simp
also have "… =⇩F (v @ [a]) @ u" using ind_eq_fin' 2 by blast
also have "… = v @ (a # u)" by simp
finally show ?case by this
qed

definition le_fin :: "'item list ⇒ 'item list ⇒ bool" (infix "≼⇩F" 50)
where "w⇩1 ≼⇩F w⇩2 ≡ ∃ v⇩1. w⇩1 @ v⇩1 =⇩F w⇩2"

lemma le_finI[intro 0]:
assumes "w⇩1 @ v⇩1 =⇩F w⇩2"
shows "w⇩1 ≼⇩F w⇩2"
using assms unfolding le_fin_def by auto
lemma le_finE[elim 0]:
assumes "w⇩1 ≼⇩F w⇩2"
obtains v⇩1
where "w⇩1 @ v⇩1 =⇩F w⇩2"
using assms unfolding le_fin_def by auto

lemma le_fin_empty[simp]: "[] ≼⇩F w" by force
lemma le_fin_trivial[intro]: "w⇩1 =⇩F w⇩2 ⟹ w⇩1 ≼⇩F w⇩2"
proof
assume 1: "w⇩1 =⇩F w⇩2"
show "w⇩1 @ [] =⇩F w⇩2" using 1 by simp
qed

lemma le_fin_length[dest]: "w⇩1 ≼⇩F w⇩2 ⟹ length w⇩1 ≤ length w⇩2" by force
lemma le_fin_range[dest]: "w⇩1 ≼⇩F w⇩2 ⟹ set w⇩1 ⊆ set w⇩2" by force

lemma eq_fin_alt_def: "w⇩1 =⇩F w⇩2 ⟷ w⇩1 ≼⇩F w⇩2 ∧ w⇩2 ≼⇩F w⇩1"
proof
show "w⇩1 ≼⇩F w⇩2 ∧ w⇩2 ≼⇩F w⇩1" if "w⇩1 =⇩F w⇩2" using that by blast
next
assume 0: "w⇩1 ≼⇩F w⇩2 ∧ w⇩2 ≼⇩F w⇩1"
have 1: "w⇩1 ≼⇩F w⇩2" "w⇩2 ≼⇩F w⇩1" using 0 by auto
have 10: "length w⇩1 = length w⇩2" using 1 by force
obtain v⇩1 v⇩2 where 2: "w⇩1 @ v⇩1 =⇩F w⇩2" "w⇩2 @ v⇩2 =⇩F w⇩1" using 1 by (elim le_finE)
have 3: "length w⇩1 = length (w⇩1 @ v⇩1)" using 2 10 by force
have 4: "w⇩1 = w⇩1 @ v⇩1" using 3 by auto
have 5: "length w⇩2 = length (w⇩2 @ v⇩2)" using 2 10 by force
have 6: "w⇩2 = w⇩2 @ v⇩2" using 5 by auto
show "w⇩1 =⇩F w⇩2" using 4 6 2 by simp
qed

lemma le_fin_reflp[simp, intro]: "w ≼⇩F w" by auto
lemma le_fin_transp[intro, trans]:
assumes "w⇩1 ≼⇩F w⇩2" "w⇩2 ≼⇩F w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
proof -
obtain v⇩1 where 1: "w⇩1 @ v⇩1 =⇩F w⇩2" using assms(1) by rule
obtain v⇩2 where 2: "w⇩2 @ v⇩2 =⇩F w⇩3" using assms(2) by rule
show ?thesis
proof
have "w⇩1 @ v⇩1 @ v⇩2 = (w⇩1 @ v⇩1) @ v⇩2" by simp
also have "… =⇩F w⇩2 @ v⇩2" using 1 by blast
also have "… =⇩F w⇩3" using 2 by blast
finally show "w⇩1 @ v⇩1 @ v⇩2 =⇩F w⇩3" by this
qed
qed
lemma eq_fin_le_fin_transp[intro, trans]:
assumes "w⇩1 =⇩F w⇩2" "w⇩2 ≼⇩F w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
using assms by auto
lemma le_fin_eq_fin_transp[intro, trans]:
assumes "w⇩1 ≼⇩F w⇩2" "w⇩2 =⇩F w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
using assms by auto
lemma prefix_le_fin_transp[intro, trans]:
assumes "w⇩1 ≤ w⇩2" "w⇩2 ≼⇩F w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
proof -
obtain v⇩1 where 1: "w⇩2 = w⇩1 @ v⇩1" using assms(1) by rule
obtain v⇩2 where 2: "w⇩2 @ v⇩2 =⇩F w⇩3" using assms(2) by rule
show ?thesis
proof
show "w⇩1 @ v⇩1 @ v⇩2 =⇩F w⇩3" using 1 2 by simp
qed
qed
lemma le_fin_prefix_transp[intro, trans]:
assumes "w⇩1 ≼⇩F w⇩2" "w⇩2 ≤ w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
proof -
obtain v⇩1 where 1: "w⇩1 @ v⇩1 =⇩F w⇩2" using assms(1) by rule
obtain v⇩2 where 2: "w⇩3 = w⇩2 @ v⇩2" using assms(2) by rule
show ?thesis
proof
have "w⇩1 @ v⇩1 @ v⇩2 = (w⇩1 @ v⇩1) @ v⇩2" by simp
also have "… =⇩F w⇩2 @ v⇩2" using 1 by blast
also have "… = w⇩3" using 2 by simp
finally show "w⇩1 @ v⇩1 @ v⇩2 =⇩F w⇩3" by this
qed
qed
lemma prefix_eq_fin_transp[intro, trans]:
assumes "w⇩1 ≤ w⇩2" "w⇩2 =⇩F w⇩3"
shows "w⇩1 ≼⇩F w⇩3"
using assms by auto

lemma le_fin_concat_start[iff]: "w @ w⇩1 ≼⇩F w @ w⇩2 ⟷ w⇩1 ≼⇩F w⇩2"
proof
assume 0: "w @ w⇩1 ≼⇩F w @ w⇩2"
obtain v⇩1 where 1: "w @ w⇩1 @ v⇩1 =⇩F w @ w⇩2" using 0 by auto
show "w⇩1 ≼⇩F w⇩2" using 1 by auto
next
assume 0: "w⇩1 ≼⇩F w⇩2"
obtain v⇩1 where 1: "w⇩1 @ v⇩1 =⇩F w⇩2" using 0 by auto
have 2: "(w @ w⇩1) @ v⇩1 =⇩F w @ w⇩2" using 1 by auto
show "w @ w⇩1 ≼⇩F w @ w⇩2" using 2 by blast
qed
lemma le_fin_concat_end[dest]:
assumes "w⇩1 ≼⇩F w⇩2"
shows "w⇩1 ≼⇩F w⇩2 @ w"
proof -
obtain v⇩1 where 1: "w⇩1 @ v⇩1 =⇩F w⇩2" using assms by rule
show ?thesis
proof
have "w⇩1 @ v⇩1 @ w = (w⇩1 @ v⇩1) @ w" by simp
also have "… =⇩F w⇩2 @ w" using 1 by blast
finally show "w⇩1 @ v⇩1 @ w =⇩F w⇩2 @ w" by this
qed
qed

definition le_fininf :: "'item list ⇒ 'item stream ⇒ bool" (infix "≼⇩F⇩I" 50)
where "w⇩1 ≼⇩F⇩I w⇩2 ≡ ∃ v⇩2. v⇩2 ≤⇩F⇩I w⇩2 ∧ w⇩1 ≼⇩F v⇩2"

lemma le_fininfI[intro 0]:
assumes "v⇩2 ≤⇩F⇩I w⇩2" "w⇩1 ≼⇩F v⇩2"
shows "w⇩1 ≼⇩F⇩I w⇩2"
using assms unfolding le_fininf_def by auto
lemma le_fininfE[elim 0]:
assumes "w⇩1 ≼⇩F⇩I w⇩2"
obtains v⇩2
where "v⇩2 ≤⇩F⇩I w⇩2" "w⇩1 ≼⇩F v⇩2"
using assms unfolding le_fininf_def by auto

lemma le_fininf_empty[simp]: "[] ≼⇩F⇩I w" by force

lemma le_fininf_range[dest]: "w⇩1 ≼⇩F⇩I w⇩2 ⟹ set w⇩1 ⊆ sset w⇩2" by force

lemma eq_fin_le_fininf_transp[intro, trans]:
assumes "w⇩1 =⇩F w⇩2" "w⇩2 ≼⇩F⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast
lemma le_fin_le_fininf_transp[intro, trans]:
assumes "w⇩1 ≼⇩F w⇩2" "w⇩2 ≼⇩F⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast
lemma prefix_le_fininf_transp[intro, trans]:
assumes "w⇩1 ≤ w⇩2" "w⇩2 ≼⇩F⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by auto
lemma le_fin_prefix_fininf_transp[intro, trans]:
assumes "w⇩1 ≼⇩F w⇩2" "w⇩2 ≤⇩F⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by auto
lemma eq_fin_prefix_fininf_transp[intro, trans]:
assumes "w⇩1 =⇩F w⇩2" "w⇩2 ≤⇩F⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by auto

lemma le_fininf_concat_start[iff]: "w @ w⇩1 ≼⇩F⇩I w @- w⇩2 ⟷ w⇩1 ≼⇩F⇩I w⇩2"
proof
assume 0: "w @ w⇩1 ≼⇩F⇩I w @- w⇩2"
obtain v⇩2 where 1: "v⇩2 ≤⇩F⇩I w @- w⇩2" "w @ w⇩1 ≼⇩F v⇩2" using 0 by rule
have 2: "length w ≤ length v⇩2" using 1(2) by force
have 4: "w ≤ v⇩2" using prefix_fininf_extend[OF 1(1) 2] by this
obtain v⇩1 where 5: "v⇩2 = w @ v⇩1" using 4 by rule
show "w⇩1 ≼⇩F⇩I w⇩2"
proof
show "v⇩1 ≤⇩F⇩I w⇩2" using 1(1) unfolding 5 by auto
show "w⇩1 ≼⇩F v⇩1" using 1(2) unfolding 5 by simp
qed
next
assume 0: "w⇩1 ≼⇩F⇩I w⇩2"
obtain v⇩2 where 1: "v⇩2 ≤⇩F⇩I w⇩2" "w⇩1 ≼⇩F v⇩2" using 0 by rule
show "w @ w⇩1 ≼⇩F⇩I w @- w⇩2"
proof
show "w @ v⇩2 ≤⇩F⇩I (w @- w⇩2)" using 1(1) by auto
show "w @ w⇩1 ≼⇩F w @ v⇩2" using 1(2) by auto
qed
qed

lemma le_fininf_singleton[intro, simp]: "[shd v] ≼⇩F⇩I v"
proof -
have "[shd v] ≼⇩F⇩I shd v ## sdrop 1 v" by blast
also have "… = v" by simp
finally show ?thesis by this
qed

definition le_inf :: "'item stream ⇒ 'item stream ⇒ bool" (infix "≼⇩I" 50)
where "w⇩1 ≼⇩I w⇩2 ≡ ∀ v⇩1. v⇩1 ≤⇩F⇩I w⇩1 ⟶ v⇩1 ≼⇩F⇩I w⇩2"

lemma le_infI[intro 0]:
assumes "⋀ v⇩1. v⇩1 ≤⇩F⇩I w⇩1 ⟹ v⇩1 ≼⇩F⇩I w⇩2"
shows "w⇩1 ≼⇩I w⇩2"
using assms unfolding le_inf_def by auto
lemma le_infE[elim 0]:
assumes "w⇩1 ≼⇩I w⇩2" "v⇩1 ≤⇩F⇩I w⇩1"
obtains "v⇩1 ≼⇩F⇩I w⇩2"
using assms unfolding le_inf_def by auto

lemma le_inf_range[dest]:
assumes "w⇩1 ≼⇩I w⇩2"
shows "sset w⇩1 ⊆ sset w⇩2"
proof
fix a
assume 1: "a ∈ sset w⇩1"
obtain i where 2: "a = w⇩1 !! i" using 1 by (metis imageE sset_range)
have 3: "stake (Suc i) w⇩1 ≤⇩F⇩I w⇩1" by rule
have 4: "stake (Suc i) w⇩1 ≼⇩F⇩I w⇩2" using assms 3 by rule
have 5: "w⇩1 !! i ∈ set (stake (Suc i) w⇩1)" by (meson lessI set_stake_snth)
show "a ∈ sset w⇩2" unfolding 2 using 5 4 by fastforce
qed

lemma le_inf_reflp[simp, intro]: "w ≼⇩I w" by auto
lemma prefix_fininf_le_inf_transp[intro, trans]:
assumes "w⇩1 ≤⇩F⇩I w⇩2" "w⇩2 ≼⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast
lemma le_fininf_le_inf_transp[intro, trans]:
assumes "w⇩1 ≼⇩F⇩I w⇩2" "w⇩2 ≼⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast
lemma le_inf_transp[intro, trans]:
assumes "w⇩1 ≼⇩I w⇩2" "w⇩2 ≼⇩I w⇩3"
shows "w⇩1 ≼⇩I w⇩3"
using assms by blast

lemma le_infI':
assumes "⋀ k. ∃ v. v ≤⇩F⇩I w⇩1 ∧ k < length v ∧ v ≼⇩F⇩I w⇩2"
shows "w⇩1 ≼⇩I w⇩2"
proof
fix u
assume 1: "u ≤⇩F⇩I w⇩1"
obtain v where 2: "v ≤⇩F⇩I w⇩1" "length u < length v" "v ≼⇩F⇩I w⇩2" using assms by auto
have 3: "length u ≤ length v" using 2(2) by auto
have 4: "u ≤ v" using prefix_fininf_length 1 2(1) 3 by this
show "u ≼⇩F⇩I w⇩2" using 4 2(3) by rule
qed

lemma le_infI_chain_left:
assumes "chain w" "⋀ k. w k ≼⇩F⇩I v"
shows "limit w ≼⇩I v"
proof (rule le_infI')
fix k
obtain l where 1: "k < length (w l)" using assms(1) by rule
show "∃ va. va ≤⇩F⇩I limit w ∧ k < length va ∧ va ≼⇩F⇩I v"
proof (intro exI conjI)
show "w l ≤⇩F⇩I limit w" using chain_prefix_limit assms(1) by this
show "k < length (w l)" using 1 by this
show "w l ≼⇩F⇩I v" using assms(2) by this
qed
qed
lemma le_infI_chain_right:
assumes "chain w" "⋀ u. u ≤⇩F⇩I v ⟹ u ≼⇩F w (l u)"
shows "v ≼⇩I limit w"
proof
fix u
assume 1: "u ≤⇩F⇩I v"
show "u ≼⇩F⇩I limit w"
proof
show "w (l u) ≤⇩F⇩I limit w" using chain_prefix_limit assms(1) by this
show "u ≼⇩F w (l u)" using assms(2) 1 by this
qed
qed
lemma le_infI_chain_right':
assumes "chain w" "⋀ k. stake k v ≼⇩F w (l k)"
shows "v ≼⇩I limit w"
proof (rule le_infI_chain_right)
show "chain w" using assms(1) by this
next
fix u
assume 1: "u ≤⇩F⇩I v"
have 2: "stake (length u) v = u" using 1 by (simp add: prefix_fininf_def shift_eq)
have 3: "stake (length u) v ≼⇩F w (l (length u))" using assms(2) by this
show "u ≼⇩F w (l (length u))" using 3 unfolding 2 by this
qed

definition eq_inf :: "'item stream ⇒ 'item stream ⇒ bool" (infix "=⇩I" 50)
where "w⇩1 =⇩I w⇩2 ≡ w⇩1 ≼⇩I w⇩2 ∧ w⇩2 ≼⇩I w⇩1"

lemma eq_infI[intro 0]:
assumes "w⇩1 ≼⇩I w⇩2" "w⇩2 ≼⇩I w⇩1"
shows "w⇩1 =⇩I w⇩2"
using assms unfolding eq_inf_def by auto
lemma eq_infE[elim 0]:
assumes "w⇩1 =⇩I w⇩2"
obtains "w⇩1 ≼⇩I w⇩2" "w⇩2 ≼⇩I w⇩1"
using assms unfolding eq_inf_def by auto

lemma eq_inf_range[dest]: "w⇩1 =⇩I w⇩2 ⟹ sset w⇩1 = sset w⇩2" by force

lemma eq_inf_reflp[simp, intro]: "w =⇩I w" by auto
lemma eq_inf_symp[intro]: "w⇩1 =⇩I w⇩2 ⟹ w⇩2 =⇩I w⇩1" by auto
lemma eq_inf_transp[intro, trans]:
assumes "w⇩1 =⇩I w⇩2" "w⇩2 =⇩I w⇩3"
shows "w⇩1 =⇩I w⇩3"
using assms by blast
lemma le_fininf_eq_inf_transp[intro, trans]:
assumes "w⇩1 ≼⇩F⇩I w⇩2" "w⇩2 =⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast
lemma le_inf_eq_inf_transp[intro, trans]:
assumes "w⇩1 ≼⇩I w⇩2" "w⇩2 =⇩I w⇩3"
shows "w⇩1 ≼⇩I w⇩3"
using assms by blast
lemma eq_inf_le_inf_transp[intro, trans]:
assumes "w⇩1 =⇩I w⇩2" "w⇩2 ≼⇩I w⇩3"
shows "w⇩1 ≼⇩I w⇩3"
using assms by blast
lemma prefix_fininf_eq_inf_transp[intro, trans]:
assumes "w⇩1 ≤⇩F⇩I w⇩2" "w⇩2 =⇩I w⇩3"
shows "w⇩1 ≼⇩F⇩I w⇩3"
using assms by blast

lemma le_inf_concat_start[iff]: "w @- w⇩1 ≼⇩I w @- w⇩2 ⟷ w⇩1 ≼⇩I w⇩2"
proof
assume 1: "w @- w⇩1 ≼⇩I w @- w⇩2"
show "w⇩1 ≼⇩I w⇩2"
proof
fix v⇩1
assume 2: "v⇩1 ≤⇩F⇩I w⇩1"
have "w @ v⇩1 ≤⇩F⇩I w @- w⇩1" using 2 by auto
also have "… ≼⇩I w @- w⇩2" using 1 by this
finally show "v⇩1 ≼⇩F⇩I w⇩2" by rule
qed
next
assume 1: "w⇩1 ≼⇩I w⇩2"
show "w @- w⇩1 ≼⇩I w @- w⇩2"
proof
fix v⇩1
assume 2: "v⇩1 ≤⇩F⇩I w @- w⇩1"
then show "v⇩1 ≼⇩F⇩I w @- w⇩2"
proof (cases rule: prefix_fininf_append)
case (absorb)
show ?thesis using absorb by auto
next
case (extend z)
show ?thesis using 1 extend by auto
qed
qed
qed
lemma eq_fin_le_inf_concat_end[dest]: "w⇩1 =⇩F w⇩2 ⟹ w⇩1 @- w ≼⇩I w⇩2 @- w"
proof
fix v⇩1
assume 1: "w⇩1 =⇩F w⇩2" "v⇩1 ≤⇩F⇩I w⇩1 @- w"
show "v⇩1 ≼⇩F⇩I w⇩2 @- w"
using 1(2)
proof (cases rule: prefix_fininf_append)
case (absorb)
show ?thesis
proof
show "w⇩2 ≤⇩F⇩I (w⇩2 @- w)" by auto
show "v⇩1 ≼⇩F w⇩2" using absorb 1(1) by auto
qed
next
case (extend w')
show ?thesis
proof
show "w⇩2 @ w' ≤⇩F⇩I (w⇩2 @- w)" using extend(2) by auto
show "v⇩1 ≼⇩F w⇩2 @ w'" unfolding extend(1) using 1(1) by auto
qed
qed
qed

lemma eq_inf_concat_start[iff]: "w @- w⇩1 =⇩I w @- w⇩2 ⟷ w⇩1 =⇩I w⇩2" by blast
lemma eq_inf_concat_end[dest]: "w⇩1 =⇩F w⇩2 ⟹ w⇩1 @- w =⇩I w⇩2 @- w"
proof -
assume 0: "w⇩1 =⇩F w⇩2"
have 1: "w⇩2 =⇩F w⇩1" using 0 by auto
show "w⇩1 @- w =⇩I w⇩2 @- w"
using eq_fin_le_inf_concat_end[OF 0] eq_fin_le_inf_concat_end[OF 1] by auto
qed

lemma le_fininf_suffixI[intro]:
assumes "w =⇩I w⇩1 @- w⇩2"
shows "w⇩1 ≼⇩F⇩I w"
using assms by blast
lemma le_fininf_suffixE[elim]:
assumes "w⇩1 ≼⇩F⇩I w"
obtains w⇩2
where "w =⇩I w⇩1 @- w⇩2"
proof -
obtain v⇩2 where 1: "v⇩2 ≤⇩F⇩I w" "w⇩1 ≼⇩F v⇩2" using assms(1) by rule
obtain u⇩1 where 2: "w⇩1 @ u⇩1 =⇩F v⇩2" using 1(2) by rule
obtain v⇩2' where 3: "w = v⇩2 @- v⇩2'" using 1(1) by rule
show ?thesis
proof
show "w =⇩I w⇩1 @- u⇩1 @- v⇩2'" unfolding 3 using 2 by fastforce
qed
qed

lemma subsume_fin:
assumes "u⇩1 ≼⇩F⇩I w" "v⇩1 ≼⇩F⇩I w"
obtains w⇩1
where "u⇩1 ≼⇩F w⇩1" "v⇩1 ≼⇩F w⇩1"
proof -
obtain u⇩2 where 2: "u⇩2 ≤⇩F⇩I w" "u⇩1 ≼⇩F u⇩2" using assms(1) by rule
obtain v⇩2 where 3: "v⇩2 ≤⇩F⇩I w" "v⇩1 ≼⇩F v⇩2" using assms(2) by rule
show ?thesis
proof (cases "length u⇩2" "length v⇩2" rule: le_cases)
case le
show ?thesis
proof
show "u⇩1 ≼⇩F v⇩2" using 2(2) prefix_fininf_length[OF 2(1) 3(1) le] by auto
show "v⇩1 ≼⇩F v⇩2" using 3(2) by this
qed
next
case ge
show ?thesis
proof
show "u⇩1 ≼⇩F u⇩2" using 2(2) by this
show "v⇩1 ≼⇩F u⇩2" using 3(2) prefix_fininf_length[OF 3(1) 2(1) ge] by auto
qed
qed
qed

lemma eq_fin_end:
assumes "u⇩1 =⇩F u⇩2" "u⇩1 @ v⇩1 =⇩F u⇩2 @ v⇩2"
shows "v⇩1 =⇩F v⇩2"
proof -
have "u⇩1 @ v⇩2 =⇩F u⇩2 @ v⇩2" using assms(1) by blast
also have "… =⇩F u⇩1 @ v⇩1" using assms(2) by blast
finally show ?thesis by blast
qed

definition indoc :: "'item ⇒ 'item list ⇒ bool"
where "indoc a u ≡ ∃ u⇩1 u⇩2. u = u⇩1 @ [a] @ u⇩2 ∧ a ∉ set u⇩1 ∧ Ind {a} (set u⇩1)"

lemma indoc_set: "indoc a u ⟹ a ∈ set u" unfolding indoc_def by auto

lemma indoc_appendI1[intro]:
assumes "indoc a u"
shows "indoc a (u @ v)"
using assms unfolding indoc_def by force
lemma indoc_appendI2[intro]:
assumes "a ∉ set u" "Ind {a} (set u)" "indoc a v"
shows "indoc a (u @ v)"
proof -
obtain v⇩1 v⇩2 where 1: "v = v⇩1 @ [a] @ v⇩2" "a ∉ set v⇩1" "Ind {a} (set v⇩1)"
using assms(3) unfolding indoc_def by blast
show ?thesis
proof (unfold indoc_def, intro exI conjI)
show "u @ v = (u @ v⇩1) @ [a] @ v⇩2" unfolding 1(1) by simp
show "a ∉ set (u @ v⇩1)" using assms(1) 1(2) by auto
show "Ind {a} (set (u @ v⇩1))" using assms(2) 1(3) by auto
qed
qed
lemma indoc_appendE[elim!]:
assumes "indoc a (u @ v)"
obtains (first) "a ∈ set u" "indoc a u" | (second)  "a ∉ set u" "Ind {a} (set u)" "indoc a v"
proof -
obtain w⇩1 w⇩2 where 1: "u @ v = w⇩1 @ [a] @ w⇩2" "a ∉ set w⇩1" "Ind {a} (set w⇩1)"
using assms unfolding indoc_def by blast
show ?thesis
proof (cases "a ∈ set u")
case True
obtain u⇩1 u⇩2 where 2: "u = u⇩1 @ [a] @ u⇩2" "a ∉ set u⇩1"
using split_list_first[OF True] by auto
have 3: "w⇩1 = u⇩1"
proof (rule split_list_first_unique)
show "w⇩1 @ [a] @ w⇩2 = u⇩1 @ [a] @ u⇩2 @ v" using 1(1) unfolding 2(1) by simp
show "a ∉ set w⇩1" using 1(2) by auto
show "a ∉ set u⇩1" using 2(2) by this
qed
show ?thesis
proof (rule first)
show "a ∈ set u" using True by this
show "indoc a u"
proof (unfold indoc_def, intro exI conjI)
show "u = u⇩1 @ [a] @ u⇩2" using 2(1) by this
show "a ∉ set u⇩1" using 1(2) unfolding 3 by this
show "Ind {a} (set u⇩1)" using 1(3) unfolding 3 by this
qed
qed
next
case False
have 2: "a ∈ set v" using indoc_set assms False by fastforce
obtain v⇩1 v⇩2 where 3: "v = v⇩1 @ [a] @ v⇩2" "a ∉ set v⇩1"
using split_list_first[OF 2] by auto
have 4: "w⇩1 = u @ v⇩1"
proof (rule split_list_first_unique)
show "w⇩1 @ [a] @ w⇩2 = (u @ v⇩1) @ [a] @ v⇩2" using 1(1) unfolding 3(1) by simp
show "a ∉ set w⇩1" using 1(2) by auto
show "a ∉ set (u @ v⇩1)" using False 3(2) by auto
qed
show ?thesis
proof (rule second)
show "a ∉ set u" using False by this
show "Ind {a} (set u)" using 1(3) 4 by auto
show "indoc a v"
proof (unfold indoc_def, intro exI conjI)
show "v = v⇩1 @ [a] @ v⇩2" using 3(1) by this
show "a ∉ set v⇩1" using 1(2) unfolding 4 by auto
show "Ind {a} (set v⇩1)" using 1(3) unfolding 4 by auto
qed
qed
qed
qed

lemma indoc_single: "indoc a [b] ⟷ a = b"
proof
assume 1: "indoc a [b]"
obtain u⇩1 u⇩2 where 2: "[b] = u⇩1 @ [a] @ u⇩2" "Ind {a} (set u⇩1)"
using 1 unfolding indoc_def by auto
show "a = b" using 2(1)
by (metis append_eq_Cons_conv append_is_Nil_conv list.distinct(2) list.inject)
next
assume 1: "a = b"
show "indoc a [b]"
unfolding indoc_def 1
proof (intro exI conjI)
show "[b] = [] @ [b] @ []" by simp
show "b ∉ set []" by simp
show "Ind {b} (set [])" by simp
qed
qed

lemma indoc_append[simp]: "indoc a (u @ v) ⟷
indoc a u ∨ a ∉ set u ∧ Ind {a} (set u) ∧ indoc a v" by blast
lemma indoc_Nil[simp]: "indoc a [] ⟷ False" unfolding indoc_def by auto
lemma indoc_Cons[simp]: "indoc a (b # v) ⟷ a = b ∨ a ≠ b ∧ ind a b ∧ indoc a v"
proof -
have "indoc a (b # v) ⟷ indoc a ([b] @ v)" by simp
also have "… ⟷ indoc a [b] ∨ a ∉ set [b] ∧ Ind {a} (set [b]) ∧ indoc a v"
unfolding indoc_append by rule
also have "… ⟷ a = b ∨ a ≠ b ∧ ind a b ∧ indoc a v" unfolding indoc_single by simp
finally show ?thesis by this
qed

lemma eq_swap_indoc: "u =⇩S v ⟹ indoc c u ⟹ indoc c v" by auto
lemma eq_fin_indoc: "u =⇩F v ⟹ indoc c u ⟹ indoc c v" by (induct rule: rtranclp.induct, auto)

lemma eq_fin_ind':
assumes "[a] @ u =⇩F u⇩1 @ [a] @ u⇩2" "a ∉ set u⇩1"
shows "Ind {a} (set u⇩1)"
proof -
have 1: "indoc a ([a] @ u)" by simp
have 2: "indoc a (u⇩1 @ [a] @ u⇩2)" using eq_fin_indoc assms(1) 1 by this
show ?thesis using assms(2) 2 by blast
qed
lemma eq_fin_ind:
assumes "u @ v =⇩F v @ u" "set u ∩ set v = {}"
shows "Ind (set u) (set v)"
using assms
proof (induct u)
case Nil
show ?case by simp
next
case (Cons a u)
have 1: "Ind {a} (set v)"
proof (rule eq_fin_ind')
show "[a] @ u @ v =⇩F v @ [a] @ u" using Cons(2) by simp
show "a ∉ set v" using Cons(3) by simp
qed
have 2: "Ind (set [a]) (set v)" using 1 by simp
have 4: "Ind (set u) (set v)"
proof (rule Cons(1))
have "[a] @ u @ v = (a # u) @ v" by simp
also have "… =⇩F v @ a # u" using Cons(2) by this
also have "… = (v @ [a]) @ u" by simp
also have "… =⇩F ([a] @ v) @ u" using 2 by blast
also have "… = [a] @ v @ u" by simp
finally show "u @ v =⇩F v @ u" by blast
show "set u ∩ set v = {}" using Cons(3) by auto
qed
show ?case using 1 4 by auto
qed

lemma le_fin_member':
assumes "[a] ≼⇩F u @ v" "a ∈ set u"
shows "[a] ≼⇩F u"
proof -
obtain w where 1: "[a] @ w =⇩F u @ v" using assms(1) by rule
obtain u⇩1 u⇩2 where 2: "u = u⇩1 @ [a] @ u⇩2" "a ∉ set u⇩1"
using split_list_first[OF assms(2)] by auto
have 3: "Ind {a} (set u⇩1)"
proof (rule eq_fin_ind')
show "[a] @ w =⇩F u⇩1 @ [a] @ u⇩2 @ v" using 1 unfolding 2(1) by simp
show "a ∉ set u⇩1" using 2(2) by this
qed
have 4: "Ind (set [a]) (set u⇩1)" using 3 by simp
have "[a] ≤ [a] @ u⇩1 @ u⇩2" by auto
also have "… = ([a] @ u⇩1) @ u⇩2" by simp
also have "… =⇩F (u⇩1 @ [a]) @ u⇩2" using 4 by blast
also have "… = u" unfolding 2(1) by simp
finally show ?thesis by this
qed
lemma le_fin_not_member':
assumes "[a] ≼⇩F u @ v" "a ∉ set u"
shows "[a] ≼⇩F v"
proof -
obtain w where 1: "[a] @ w =⇩F u @ v" using assms(1) by rule
have 3: "a ∈ set v" using assms by auto
obtain v⇩1 v⇩2 where 4: "v = v⇩1 @ [a] @ v⇩2" "a ∉ set v⇩1" using split_list_first[OF 3] by auto
have 5: "[a] @ w =⇩F u @ v⇩1 @ [a] @ v⇩2" using 1 unfolding 4(1) by this
have 6: "Ind {a} (set (u @ v⇩1))"
proof (rule eq_fin_ind')
show "[a] @ w =⇩F (u @ v⇩1) @ [a] @ v⇩2" using 5 by simp
show "a ∉ set (u @ v⇩1)" using assms(2) 4(2) by auto
qed
have 9: "Ind (set [a]) (set v⇩1)" using 6 by auto
have "[a] ≤ [a] @ v⇩1 @ v⇩2" by auto
also have "… = ([a] @ v⇩1) @ v⇩2" by simp
also have "… =⇩F (v⇩1 @ [a]) @ v⇩2" using 9 by blast
also have "… = v⇩1 @ [a] @ v⇩2" by simp
also have "… = v" unfolding 4(1) by rule
finally show ?thesis by this
qed
lemma le_fininf_not_member':
assumes "[a] ≼⇩F⇩I u @- v" "a ∉ set u"
shows "[a] ≼⇩F⇩I v"
proof -
obtain v⇩2 where 1: "v⇩2 ≤⇩F⇩I u @- v" "[a] ≼⇩F v⇩2" using le_fininfE assms(1) by this
show ?thesis
using 1(1)
proof (cases rule: prefix_fininf_append)
case absorb
have "[a] ≼⇩F v⇩2" using 1(2) by this
also have "… ≤ u" using absorb by this
finally have 2: "a ∈ set u" by force
show ?thesis using assms(2) 2 by simp
next
case (extend z)
have "[a] ≼⇩F v⇩2" using 1(2) by this
also have "… = u @ z" using extend(1) by this
finally have 2: "[a] ≼⇩F u @ z" by this
have "[a] ≼⇩F z" using le_fin_not_member' 2 assms(2) by this
also have "… ≤⇩F⇩I v" using extend(2) by this
finally show ?thesis by this
qed
qed

lemma le_fin_ind'':
assumes "[a] ≼⇩F w" "[b] ≼⇩F w" "a ≠ b"
shows "ind a b"
proof -
obtain u where 1: "[a] @ u =⇩F w" using assms(1) by rule
obtain v where 2: "[b] @ v =⇩F w" using assms(2) by rule
have 3: "[a] @ u =⇩F [b] @ v" using 1 2[symmetric] by auto
have 4: "a ∈ set v" using 3 assms(3)
by (metis append_Cons append_Nil eq_fin_range list.set_intros(1) set_ConsD)
obtain v⇩1 v⇩2 where 5: "v = v⇩1 @ [a] @ v⇩2" "a ∉ set v⇩1" using split_list_first[OF 4] by auto
have 7: "Ind {a} (set ([b] @ v⇩1))"
proof (rule eq_fin_ind')
show "[a] @ u =⇩F ([b] @ v⇩1) @ [a] @ v⇩2" using 3 unfolding 5(1) by simp
show "a ∉ set ([b] @ v⇩1)" using assms(3) 5(2) by auto
qed
show ?thesis using 7 by auto
qed
lemma le_fin_ind':
assumes "[a] ≼⇩F w" "v ≼⇩F w" "a ∉ set v"
shows "Ind {a} (set v)"
using assms
proof (induct v arbitrary: w)
case Nil
show ?case by simp
next
case (Cons b v)
have 1: "ind a b"
proof (rule le_fin_ind'')
show "[a] ≼⇩F w" using Cons(2) by this
show "[b] ≼⇩F w" using Cons(3) by auto
show "a ≠ b" using Cons(4) by auto
qed
obtain w' where 2: "[b] @ w' =⇩F w" using Cons(3) by auto
have 3: "Ind {a} (set v)"
proof (rule Cons(1))
show "[a] ≼⇩F w'"
proof (rule le_fin_not_member')
show "[a] ≼⇩F [b] @ w'" using Cons(2) 2 by auto
show "a ∉ set [b]" using Cons(4) by auto
qed
have "[b] @ v = b # v" by simp
also have "… ≼⇩F w" using Cons(3) by this
also have "… =⇩F [b] @ w'" using 2 by auto
finally show "v ≼⇩F w'" by blast
show "a ∉ set v" using Cons(4) by auto
qed
show ?case using 1 3 by auto
qed
lemma le_fininf_ind'':
assumes "[a] ≼⇩F⇩I w" "[b] ≼⇩F⇩I w" "a ≠ b"
shows "ind a b"
using subsume_fin le_fin_ind'' assms by metis
lemma le_fininf_ind':
assumes "[a] ≼⇩F⇩I w" "v ≼⇩F⇩I w" "a ∉ set v"
shows "Ind {a} (set v)"
using subsume_fin le_fin_ind' assms by metis

lemma indoc_alt_def: "indoc a v ⟷ v =⇩F [a] @ remove1 a v"
proof
assume 0: "indoc a v"
obtain v⇩1 v⇩2 where 1: "v = v⇩1 @ [a] @ v⇩2" "a ∉ set v⇩1" "Ind {a} (set v⇩1)"
using 0 unfolding indoc_def by blast
have 2: "Ind (set [a]) (set v⇩1)" using 1(3) by simp
have "v = v⇩1 @ [a] @ v⇩2" using 1(1) by this
also have "… = (v⇩1 @ [a]) @ v⇩2" by simp
also have "… =⇩F ([a] @ v⇩1) @ v⇩2" using 2 by blast
also have "… = [a] @ v⇩1 @ v⇩2" by simp
also have "… = [a] @ remove1 a v" unfolding 1(1) remove1_append using 1(2) by auto
finally show "v =⇩F [a] @ remove1 a v" by this
next
assume 0: "v =⇩F [a] @ remove1 a v"
have 1: "indoc a ([a] @ remove1 a v)" by simp
show "indoc a v" using eq_fin_indoc 0  1 by blast
qed

lemma levi_lemma:
assumes "t @ u =⇩F v @ w"
obtains p r s q
where "t =⇩F p @ r" "u =⇩F s @ q" "v =⇩F p @ s" "w =⇩F r @ q" "Ind (set r) (set s)"
using assms
proof (induct t arbitrary: thesis v w)
case Nil
show ?case
proof (rule Nil(1))
show "[] =⇩F [] @ []" by simp
show "v =⇩F [] @ v" by simp
show "u =⇩F v @ w" using Nil(2) by simp
show "w =⇩F [] @ w" by simp
show "Ind (set []) (set v)" by simp
qed
next
case (Cons a t')
have 1: "[a] ≼⇩F v @ w" using Cons(3) by blast
show ?case
proof (cases "a ∈ set v")
case False
have 2: "[a] ≼⇩F w" using le_fin_not_member' 1 False by this
obtain w' where 3: "w =⇩F [a] @ w'" using 2 by blast
have 4: "v ≼⇩F v @ w" by auto
have 5: "Ind (set [a]) (set v)" using le_fin_ind'[OF 1 4] False by simp
have "[a] @ t' @ u = (a # t') @ u" by simp
also have "… =⇩F v @ w" using Cons(3) by this
also have "… =⇩F v @ [a] @ w'" using 3 by blast
also have "… = (v @ [a]) @ w'" by simp
also have "… =⇩F ([a] @ v) @ w'" using 5 by blast
also have "… = [a] @ v @ w'" by simp
finally have 6: "t' @ u =⇩F v @ w'" by blast
obtain p r' s q where 7: "t' =⇩F p @ r'" "u =⇩F s @ q" "v =⇩F p @ s" "w' =⇩F r' @ q"
"Ind (set r') (set s)" using Cons(1)[OF _ 6] by this
have 8: "set v = set p ∪ set s" using eq_fin_range 7(3) by auto
have 9: "Ind (set [a]) (set p)" using 5 8 by auto
have 10: "Ind (set [a]) (set s)" using 5 8 by auto
show ?thesis
proof (rule Cons(2))
have "a # t' = [a] @ t'" by simp
also have "… =⇩F [a] @ p @ r'" using 7(1) by blast
also have "… = ([a] @ p) @ r'" by simp
also have "… =⇩F (p @ [a]) @ r'" using 9 by blast
also have "… = p @ [a] @ r'" by simp
finally show "a # t' =⇩F p @ [a] @ r'" by this
show "u =⇩F s @ q" using 7(2) by this
show "v =⇩F p @ s" using 7(3) by this
have "w =⇩F [a] @ w'" using 3 by this
also have "… =⇩F [a] @ r' @ q" using 7(4) by blast
also have "… = ([a] @ r') @ q" by simp
finally show "w =⇩F ([a] @ r') @ q" by this
show "Ind (set ([a] @ r')) (set s)" using 7(5) 10 by auto
qed
next
case True
have 2: "[a] ≼⇩F v" using le_fin_member' 1 True by this
obtain v' where 3: "v =⇩F [a] @ v'" using 2 by blast
have "[a] @ t' @ u = (a # t') @ u" by simp
also have "… =⇩F v @ w" using Cons(3) by this
also have "… =⇩F ([a] @ v') @ w" using 3 by blast
also have "… = [a] @ v' @ w" by simp
finally have 4: "t' @ u =⇩F v' @ w" by blast
obtain p' r s q where 7: "t' =⇩F p' @ r" "u =⇩F s @ q" "v' =⇩F p' @ s" "w =⇩F r @ q"
"Ind (set r) (set s)" using Cons(1)[OF _ 4] by this
show ?thesis
proof (rule Cons(2))
have "a # t' = [a] @ t'" by simp
also have "… =⇩F [a] @ p' @ r" using 7(1) by blast
also have "… = ([a] @ p') @ r" by simp
finally show "a # t' =⇩F ([a] @ p') @ r" by this
show "u =⇩F s @ q" using 7(2) by this
have "v =⇩F [a] @ v'" using 3 by this
also have "… =⇩F [a] @ p' @ s" using 7(3) by blast
also have "… = ([a] @ p') @ s" by simp
finally show "v =⇩F ([a] @ p') @ s" by this
show "w =⇩F r @ q" using 7(4) by this
show "Ind (set r) (set s)" using 7(5) by this
qed
qed
qed

end

end


# Theory Transition_System_Traces

section ‹Transition Systems and Trace Theory›

theory Transition_System_Traces
imports
Transition_System_Extensions
Traces
begin

lemma (in transition_system) words_infI_construct[rule_format, intro?]:
assumes "∀ v. v ≤⇩F⇩I w ⟶ path v p"
shows "run w p"
using assms by coinduct auto

lemma (in transition_system) words_infI_construct':
assumes "⋀ k. ∃ v. v ≤⇩F⇩I w ∧ k < length v ∧ path v p"
shows "run w p"
proof
fix u
assume 1: "u ≤⇩F⇩I w"
obtain v where 2: "v ≤⇩F⇩I w" "length u < length v" "path v p" using assms(1) by auto
have 3: "length u ≤ length v" using 2(2) by simp
have 4: "u ≤ v" using prefix_fininf_length 1 2(1) 3 by this
show "path u p" using 4 2(3) by auto
qed

lemma (in transition_system) words_infI_construct_chain[intro]:
assumes "chain w" "⋀ k. path (w k) p"
shows "run (limit w) p"
proof (rule words_infI_construct')
fix k
obtain l where 1: "k < length (w l)" using assms(1) by rule
show "∃ v. v ≤⇩F⇩I limit w ∧ k < length v ∧ path v p"
proof (intro exI conjI)
show "w l ≤⇩F⇩I limit w" using chain_prefix_limit assms(1) by this
show "k < length (w l)" using 1 by this
show "path (w l) p" using assms(2) by this
qed
qed

lemma (in transition_system) words_fin_blocked:
assumes "⋀ w. path w p ⟹ A ∩ set w = {} ⟹ A ∩ {a. enabled a (target w p)} ⊆ A ∩ {a. enabled a p}"
assumes "path w p" "A ∩ {a. enabled a p} ∩ set w = {}"
shows "A ∩ set w = {}"
using assms by (induct w rule: rev_induct, auto)

locale transition_system_traces =
transition_system ex en +
traces ind
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and ind :: "'action ⇒ 'action ⇒ bool"
+
assumes en: "ind a b ⟹ en a p ⟹ en b p ⟷ en b (ex a p)"
assumes ex: "ind a b ⟹ en a p ⟹ en b p ⟹ ex b (ex a p) = ex a (ex b p)"
begin

lemma diamond_bottom:
assumes "ind a b"
assumes "en a p" "en b p"
shows "en a (ex b p)" "en b (ex a p)" "ex b (ex a p) = ex a (ex b p)"
using assms independence_symmetric en ex by metis+
lemma diamond_right:
assumes "ind a b"
assumes "en a p" "en b (ex a p)"
shows "en a (ex b p)" "en b p" "ex b (ex a p) = ex a (ex b p)"
using assms independence_symmetric en ex by metis+
lemma diamond_left:
assumes "ind a b"
assumes "en a (ex b p)" "en b p"
shows "en a p" "en b (ex a p)" "ex b (ex a p) = ex a (ex b p)"
using assms independence_symmetric en ex by metis+

lemma eq_swap_word:
assumes "w⇩1 =⇩S w⇩2" "path w⇩1 p"
shows "path w⇩2 p"
using assms diamond_right by (induct, auto)
lemma eq_fin_word:
assumes "w⇩1 =⇩F w⇩2" "path w⇩1 p"
shows "path w⇩2 p"
using assms eq_swap_word by (induct, auto)
lemma le_fin_word:
assumes "w⇩1 ≼⇩F w⇩2" "path w⇩2 p"
shows "path w⇩1 p"
using assms eq_fin_word by blast
lemma le_fininf_word:
assumes "w⇩1 ≼⇩F⇩I w⇩2" "run w⇩2 p"
shows "path w⇩1 p"
using assms le_fin_word by blast
lemma le_inf_word:
assumes "w⇩2 ≼⇩I w⇩1" "run w⇩1 p"
shows "run w⇩2 p"
using assms le_fininf_word by (blast intro: words_infI_construct)
lemma eq_inf_word:
assumes "w⇩1 =⇩I w⇩2" "run w⇩1 p"
shows "run w⇩2 p"
using assms le_inf_word by auto

lemma eq_swap_execute:
assumes "path w⇩1 p" "w⇩1 =⇩S w⇩2"
shows "fold ex w⇩1 p = fold ex w⇩2 p"
using assms(2, 1) diamond_right by (induct, auto)
lemma eq_fin_execute:
assumes "path w⇩1 p" "w⇩1 =⇩F w⇩2"
shows "fold ex w⇩1 p = fold ex w⇩2 p"
using assms(2, 1) eq_fin_word eq_swap_execute by (induct, auto)

lemma diamond_fin_word_step:
assumes "Ind {a} (set v)" "en a p" "path v p"
shows "path v (ex a p)"
using diamond_bottom assms by (induct v arbitrary: p, auto, metis)
lemma diamond_inf_word_step:
assumes "Ind {a} (sset w)" "en a p" "run w p"
shows "run w (ex a p)"
using diamond_fin_word_step assms by (fast intro: words_infI_construct)
lemma diamond_fin_word_inf_word:
assumes "Ind (set v) (sset w)" "path v p" "run w p"
shows "run w (fold ex v p)"
using diamond_inf_word_step assms by (induct v arbitrary: p, auto)
lemma diamond_fin_word_inf_word':
assumes "Ind (set v) (sset w)" "path (u @ v) p" "run (u @- w) p"
shows "run (u @- v @- w) p"
using assms diamond_fin_word_inf_word by auto

end

end


# Theory Functions

section ‹Functions›

theory Functions
imports "../Extensions/Set_Extensions"
begin

locale bounded_function =
fixes A :: "'a set"
fixes B :: "'b set"
fixes f :: "'a ⇒ 'b"
assumes wellformed[intro?, simp]: "x ∈ A ⟹ f x ∈ B"

locale bounded_function_pair =
f: bounded_function A B f +
g: bounded_function B A g
for A :: "'a set"
and B :: "'b set"
and f :: "'a ⇒ 'b"
and g :: "'b ⇒ 'a"

locale injection = bounded_function_pair +
assumes left_inverse[simp]: "x ∈ A ⟹ g (f x) = x"
begin

lemma inj_on[intro]: "inj_on f A" using inj_onI left_inverse by metis

lemma injective_on:
assumes "x ∈ A" "y ∈ A" "f x = f y"
shows "x = y"
using assms left_inverse by metis

end

locale injective = bounded_function +
assumes injection: "∃ g. injection A B f g"
begin

definition "g ≡ SOME g. injection A B f g"

sublocale injection A B f g unfolding g_def using someI_ex[OF injection] by this

end

locale surjection = bounded_function_pair +
assumes right_inverse[simp]: "y ∈ B ⟹ f (g y) = y"
begin

lemma image_superset[intro]: "f  A ⊇ B"
using g.wellformed image_iff right_inverse subsetI by metis

lemma image_eq[simp]: "f  A = B" using image_superset by auto

end

locale surjective = bounded_function +
assumes surjection: "∃ g. surjection A B f g"
begin

definition "g ≡ SOME g. surjection A B f g"

sublocale surjection A B f g unfolding g_def using someI_ex[OF surjection] by this

end

locale bijection = injection + surjection

lemma inj_on_bijection:
assumes "inj_on f A"
shows "bijection A (f  A) f (inv_into A f)"
proof
show "⋀ x. x ∈ A ⟹ f x ∈ f  A" using imageI by this
show "⋀ y. y ∈ f  A ⟹ inv_into A f y ∈ A" using inv_into_into by this
show "⋀ x. x ∈ A ⟹ inv_into A f (f x) = x" using inv_into_f_f assms by this
show "⋀ y. y ∈ f  A ⟹ f (inv_into A f y) = y" using f_inv_into_f by this
qed

end


# Theory ENat_Extensions

section ‹Extended Natural Numbers›

theory ENat_Extensions
imports
Coinductive.Coinductive_Nat
begin

declare eSuc_enat[simp]
declare enat_0[simp] enat_1[simp] one_eSuc[simp]
declare enat_0_iff[iff] enat_1_iff[iff]
declare Suc_ile_eq[iff]

lemma enat_Suc0[simp]: "enat (Suc 0) = eSuc 0" by (metis One_nat_def one_eSuc one_enat_def)

lemma le_epred[iff]: "l < epred k ⟷ eSuc l < k"
by (metis eSuc_le_iff epred_eSuc epred_le_epredI less_le_not_le not_le)

lemma eq_infI[intro]:
assumes "⋀ n. enat n ≤ m"
shows "m = ∞"
using assms by (metis enat_less_imp_le enat_ord_simps(5) less_le_not_le)

end

# Theory CCPO_Extensions

section ‹Chain-Complete Partial Orders›

theory CCPO_Extensions
imports
"HOL-Library.Complete_Partial_Order2"
ENat_Extensions
Set_Extensions
begin

lemma chain_split[dest]:
assumes "Complete_Partial_Order.chain ord C" "x ∈ C"
shows "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}"
proof -
have 1: "⋀ y. y ∈ C ⟹ ord x y ∨ ord y x" using chainD assms by this
show ?thesis using 1 by blast
qed

lemma infinite_chain_below[dest]:
assumes "Complete_Partial_Order.chain ord C" "infinite C" "x ∈ C"
assumes "finite {y ∈ C. ord x y}"
shows "infinite {y ∈ C. ord y x}"
proof -
have 1: "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}" using assms(1, 3) by rule
show ?thesis using finite_Un assms(2, 4) 1 by (metis (poly_guards_query))
qed
lemma infinite_chain_above[dest]:
assumes "Complete_Partial_Order.chain ord C" "infinite C" "x ∈ C"
assumes "finite {y ∈ C. ord y x}"
shows "infinite {y ∈ C. ord x y}"
proof -
have 1: "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}" using assms(1, 3) by rule
show ?thesis using finite_Un assms(2, 4) 1 by (metis (poly_guards_query))
qed

lemma (in ccpo) ccpo_Sup_upper_inv:
assumes "Complete_Partial_Order.chain less_eq C" "x > ⨆ C"
shows "x ∉ C"
using assms ccpo_Sup_upper by fastforce
lemma (in ccpo) ccpo_Sup_least_inv:
assumes "Complete_Partial_Order.chain less_eq C" "⨆ C > x"
obtains y
where "y ∈ C" "¬ y ≤ x"
using assms ccpo_Sup_least that by fastforce

lemma ccpo_Sup_least_inv':
fixes C :: "'a :: {ccpo, linorder} set"
assumes "Complete_Partial_Order.chain less_eq C" "⨆ C > x"
obtains y
where "y ∈ C" "y > x"
proof -
obtain y where 1: "y ∈ C" "¬ y ≤ x" using ccpo_Sup_least_inv assms by this
show ?thesis using that 1 by simp
qed

lemma mcont2mcont_lessThan[THEN lfp.mcont2mcont, simp, cont_intro]:
shows mcont_lessThan: "mcont Sup less_eq Sup less_eq
(lessThan :: 'a :: {ccpo, linorder} ⇒ 'a set)"
proof
show "monotone less_eq less_eq (lessThan :: 'a ⇒ 'a set)" by (rule, auto)
show "cont Sup less_eq Sup less_eq (lessThan :: 'a ⇒ 'a set)"
proof
fix C :: "'a set"
assume 1: "Complete_Partial_Order.chain less_eq C"
show "{..< ⨆ C} = ⋃ (lessThan  C)"
proof (intro equalityI subsetI)
fix A
assume 2: "A ∈ {..< ⨆ C}"
obtain B where 3: "B ∈ C" "B > A" using ccpo_Sup_least_inv' 1 2 by blast
show "A ∈ ⋃ (lessThan  C)" using 3 by auto
next
fix A
assume 2: "A ∈ ⋃ (lessThan  C)"
show "A ∈ {..< ⨆ C}" using ccpo_Sup_upper 2 by force
qed
qed
qed

class esize =
fixes esize :: "'a ⇒ enat"

class esize_order = esize + order +
assumes esize_finite[dest]: "esize x ≠ ∞ ⟹ finite {y. y ≤ x}"
assumes esize_mono[intro]: "x ≤ y ⟹ esize x ≤ esize y"
assumes esize_strict_mono[intro]: "esize x ≠ ∞ ⟹ x < y ⟹ esize x < esize y"
begin

lemma infinite_chain_eSuc_esize[dest]:
assumes "Complete_Partial_Order.chain less_eq C" "infinite C" "x ∈ C"
obtains y
where "y ∈ C" "esize y ≥ eSuc (esize x)"
proof (cases "esize x")
case (enat k)
have 1: "finite {y ∈ C. y ≤ x}" using esize_finite enat by simp
have 2: "infinite {y ∈ C. y ≥ x}" using assms 1 by rule
have 3: "{y ∈ C. y > x} = {y ∈ C. y ≥ x} - {x}" by auto
have 4: "infinite {y ∈ C. y > x}" using 2 unfolding 3 by simp
obtain y where 5: "y ∈ C" "y > x" using 4 by auto
have 6: "esize y > esize x" using esize_strict_mono enat 5(2) by blast
show ?thesis using that 5(1) 6 ileI1 by simp
next
case (infinity)
show ?thesis using that infinity assms(3) by simp
qed

lemma infinite_chain_arbitrary_esize[dest]:
assumes "Complete_Partial_Order.chain less_eq C" "infinite C"
obtains x
where "x ∈ C" "esize x ≥ enat n"
proof (induct n arbitrary: thesis)
case 0
show ?case using assms(2) 0 by force
next
case (Suc n)
obtain x where 1: "x ∈ C" "esize x ≥ enat n" using Suc(1) by blast
obtain y where 2: "y ∈ C" "esize y ≥ eSuc (esize x)" using assms 1(1) by rule
show ?case using gfp.leq_trans Suc(2) 1(2) 2 by fastforce
qed

end

class esize_ccpo = esize_order + ccpo
begin

lemma esize_cont[dest]:
assumes "Complete_Partial_Order.chain less_eq C" "C ≠ {}"
shows "esize (⨆ C) = ⨆ (esize  C)"
proof (cases "finite C")
case False
have 1: "esize (⨆ C) = ∞"
proof
fix n
obtain A where 1: "A ∈ C" "esize A ≥ enat n" using assms(1) False by rule
have 2: "A ≤ ⨆ C" using ccpo_Sup_upper assms(1) 1(1) by this
have "enat n ≤ esize A" using 1(2) by this
also have "… ≤ esize (⨆ C)" using 2 by rule
finally show "enat n ≤ esize (⨆ C)" by this
qed
have 2: "(⨆ A ∈ C. esize A) = ∞"
proof
fix n
obtain A where 1: "A ∈ C" "esize A ≥ enat n" using assms(1) False by rule
show "enat n ≤ (⨆ A ∈ C. esize A)" using SUP_upper2 1 by this
qed
show ?thesis using 1 2 by simp
next
case True
have 1: "esize (⨆ C) = (⨆ x ∈ C. esize x)"
proof (intro order_class.order.antisym SUP_upper SUP_least esize_mono)
show "⨆ C ∈ C" using in_chain_finite assms(1) True assms(2) by this
show "⋀ x. x ∈ C ⟹ x ≤ ⨆ C" using ccpo_Sup_upper assms(1) by this
qed
show ?thesis using 1 by simp
qed

lemma esize_mcont: "mcont Sup less_eq Sup less_eq esize"
by (blast intro: mcontI monotoneI contI)

lemmas mcont2mcont_esize = esize_mcont[THEN lfp.mcont2mcont, simp, cont_intro]

end

end


# Theory ESet_Extensions

section ‹Sets and Extended Natural Numbers›

theory ESet_Extensions
imports
"../Basics/Functions"
Basic_Extensions
CCPO_Extensions
begin

lemma card_lessThan_enat[simp]: "card {..< enat k} = card {..< k}"
proof -
have 1: "{..< enat k} = enat  {..< k}"
unfolding lessThan_def image_Collect using enat_iless by force
have "card {..< enat k} = card (enat  {..< k})" unfolding 1 by rule
also have "… = card {..< k}" using card_image inj_enat by metis
finally show ?thesis by this
qed
lemma card_atMost_enat[simp]: "card {.. enat k} = card {.. k}"
proof -
have 1: "{.. enat k} = enat  {.. k}"
unfolding atMost_def image_Collect using enat_ile by force
have "card {.. enat k} = card (enat  {.. k})" unfolding 1 by rule
also have "… = card {.. k}" using card_image inj_enat by metis
finally show ?thesis by this
qed

lemma enat_Collect:
assumes "∞ ∉ A"
shows "{i. enat i ∈ A} = the_enat  A"
using assms by (safe, force) (metis enat_the_enat)

lemma Collect_lessThan: "{i. enat i < n} = the_enat  {..< n}"
proof -
have 1: "∞ ∉ {..< n}" by simp
have "{i. enat i < n} = {i. enat i ∈ {..< n}}" by simp
also have "… = the_enat  {..< n}" using enat_Collect 1 by this
finally show ?thesis by this
qed

instantiation set :: (type) esize_ccpo
begin

function esize_set where "finite A ⟹ esize A = enat (card A)" | "infinite A ⟹ esize A = ∞"
by auto termination by lexicographic_order

lemma esize_iff_empty[iff]: "esize A = 0 ⟷ A = {}" by (cases "finite A", auto)
lemma esize_iff_infinite[iff]: "esize A = ∞ ⟷ infinite A" by force
lemma esize_singleton[simp]: "esize {a} = eSuc 0" by simp
lemma esize_infinite_enat[dest, simp]: "infinite A ⟹ enat k < esize A" by force

instance
proof
fix A :: "'a set"
assume 1: "esize A ≠ ∞"
show "finite {B. B ⊆ A}" using 1 by simp
next
fix A B :: "'a set"
assume 1: "A ⊆ B"
show "esize A ≤ esize B"
proof (cases "finite B")
case False
show ?thesis using False by auto
next
case True
have 2: "finite A" using True 1 by auto
show ?thesis using card_mono True 1 2 by auto
qed
next
fix A B :: "'a set"
assume 1: "esize A ≠ ∞" "A ⊂ B"
show "esize A < esize B" using psubset_card_mono 1 by (cases "finite B", auto)
qed

end

lemma esize_image[simp, intro]:
assumes "inj_on f A"
shows "esize (f  A) = esize A"
using card_image finite_imageD assms by (cases "finite A", auto)
lemma esize_insert1[simp]: "a ∉ A ⟹ esize (insert a A) = eSuc (esize A)"
by (cases "finite A", force+)
lemma esize_insert2[simp]: "a ∈ A ⟹ esize (insert a A) = esize A"
using insert_absorb by metis
lemma esize_remove1[simp]: "a ∉ A ⟹ esize (A - {a}) = esize A"
by (cases "finite A", force+)
lemma esize_remove2[simp]: "a ∈ A ⟹ esize (A - {a}) = epred (esize A)"
by (cases "finite A", force+)
lemma esize_union_disjoint[simp]:
assumes "A ∩ B = {}"
shows "esize (A ∪ B) = esize A + esize B"
proof (cases "finite (A ∪ B)")
case True
show ?thesis using card_Un_disjoint assms True by auto
next
case False
show ?thesis using False by (cases "finite A", auto)
qed
lemma esize_lessThan[simp]: "esize {..< n} = n"
proof (cases n)
case (enat k)
have 1: "finite {..< n}" unfolding enat by (metis finite_lessThan_enat_iff not_enat_eq)
show ?thesis using 1 unfolding enat by simp
next
case (infinity)
have 1: "infinite {..< n}" unfolding infinity using infinite_lessThan_infty by simp
show ?thesis using 1 unfolding infinity by simp
qed
lemma esize_atMost[simp]: "esize {.. n} = eSuc n"
proof (cases n)
case (enat k)
have 1: "finite {.. n}" unfolding enat by (metis atMost_iff finite_enat_bounded)
show ?thesis using 1 unfolding enat by simp
next
case (infinity)
have 1: "infinite {.. n}"
unfolding infinity
by (metis atMost_iff enat_ord_code(3) infinite_lessThan_infty infinite_super subsetI)
show ?thesis using 1 unfolding infinity by simp
qed

lemma least_eSuc[simp]:
assumes "A ≠ {}"
shows "least (eSuc  A) = eSuc (least A)"
proof (rule antisym)
obtain k where 10: "k ∈ A" using assms by blast
have 11: "eSuc k ∈ eSuc  A" using 10 by auto
have 20: "least A ∈ A" using 10 LeastI by metis
have 21: "least (eSuc  A) ∈ eSuc  A" using 11 LeastI by metis
have 30: "⋀ l. l ∈ A ⟹ least A ≤ l" using 10 Least_le by metis
have 31: "⋀ l. l ∈ eSuc  A ⟹ least (eSuc  A) ≤ l" using 11 Least_le by metis
show "least (eSuc  A) ≤ eSuc (least A)" using 20 31 by auto
show "eSuc (least A) ≤ least (eSuc  A)" using 21 30 by auto
qed

lemma Inf_enat_eSuc[simp]: "⨅ (eSuc  A) = eSuc (⨅ A)" unfolding Inf_enat_def by simp

definition lift :: "nat set ⇒ nat set"
where "lift A ≡ insert 0 (Suc  A)"

lemma liftI_0[intro, simp]: "0 ∈ lift A" unfolding lift_def by auto
lemma liftI_Suc[intro]: "a ∈ A ⟹ Suc a ∈ lift A" unfolding lift_def by auto
lemma liftE[elim]:
assumes "b ∈ lift A"
obtains (0) "b = 0" | (Suc) a where "b = Suc a" "a ∈ A"
using assms unfolding lift_def by auto

lemma lift_esize[simp]: "esize (lift A) = eSuc (esize A)" unfolding lift_def by auto
lemma lift_least[simp]: "least (lift A) = 0" unfolding lift_def by auto

primrec nth_least :: "'a set ⇒ nat ⇒ 'a :: wellorder"
where "nth_least A 0 = least A" | "nth_least A (Suc n) = nth_least (A - {least A}) n"

lemma nth_least_wellformed[intro?, simp]:
assumes "enat n < esize A"
shows "nth_least A n ∈ A"
using assms
proof (induct n arbitrary: A)
case 0
show ?case using 0 by simp
next
case (Suc n)
have 1: "A ≠ {}" using Suc(2) by auto
have 2: "enat n < esize (A - {least A})" using Suc(2) 1 by simp
have 3: "nth_least (A - {least A}) n ∈ A - {least A}" using Suc(1) 2 by this
show ?case using 3 by simp
qed

lemma card_wellformed[intro?, simp]:
fixes k :: "'a :: wellorder"
assumes "k ∈ A"
shows "enat (card {i ∈ A. i < k}) < esize A"
proof (cases "finite A")
case False
show ?thesis using False by simp
next
case True
have 1: "esize {i ∈ A. i < k} < esize A" using True assms by fastforce
show ?thesis using True 1 by simp
qed

lemma nth_least_strict_mono:
assumes "enat l < esize A" "k < l"
shows "nth_least A k < nth_least A l"
using assms
proof (induct k arbitrary: A l)
case 0
obtain l' where 1: "l = Suc l'" using 0(2) by (metis gr0_conv_Suc)
have 2: "A ≠ {}" using 0(1) by auto
have 3: "enat l' < esize (A - {least A})" using 0(1) 2 unfolding 1 by simp
have 4: "nth_least (A - {least A}) l' ∈ A - {least A}" using 3 by rule
show ?case using 1 4 by (auto intro: le_neq_trans)
next
case (Suc k)
obtain l' where 1: "l = Suc l'" using Suc(3) by (metis Suc_lessE)
have 2: "A ≠ {}" using Suc(2) by auto
show ?case using Suc 2 unfolding 1 by simp
qed

lemma nth_least_mono[intro, simp]:
assumes "enat l < esize A" "k ≤ l"
shows "nth_least A k ≤ nth_least A l"
using nth_least_strict_mono le_less assms by metis

lemma card_nth_least[simp]:
assumes "enat n < esize A"
shows "card {k ∈ A. k < nth_least A n} = n"
using assms
proof (induct n arbitrary: A)
case 0
have 1: "{k ∈ A. k < least A} = {}" using least_not_less by auto
show ?case using nth_least.simps(1) card.empty 1 by metis
next
case (Suc n)
have 1: "A ≠ {}" using Suc(2) by auto
have 2: "enat n < esize (A - {least A})" using Suc(2) 1 by simp
have 3: "nth_least A 0 < nth_least A (Suc n)" using nth_least_strict_mono Suc(2) by blast
have 4: "{k ∈ A. k < nth_least A (Suc n)} =
{least A} ∪ {k ∈ A - {least A}. k < nth_least (A - {least A}) n}" using 1 3 by auto
have 5: "card {k ∈ A - {least A}. k < nth_least (A - {least A}) n} = n" using Suc(1) 2 by this
have 6: "finite {k ∈ A - {least A}. k < nth_least (A - {least A}) n}"
using 5 Collect_empty_eq card.infinite infinite_imp_nonempty least_not_less nth_least.simps(1)
by (metis (no_types, lifting))
have "card {k ∈ A. k < nth_least A (Suc n)} =
card ({least A} ∪ {k ∈ A - {least A}. k < nth_least (A - {least A}) n})" using 4 by simp
also have "… = card {least A} + card {k ∈ A - {least A}. k < nth_least (A - {least A}) n}"
using 6 by simp
also have "… = Suc n" using 5 by simp
finally show ?case by this
qed

lemma card_nth_least_le[simp]:
assumes "enat n < esize A"
shows "card {k ∈ A. k ≤ nth_least A n} = Suc n"
proof -
have 1: "{k ∈ A. k ≤ nth_least A n} = {nth_least A n} ∪ {k ∈ A. k < nth_least A n}"
using assms by auto
have 2: "card {k ∈ A. k < nth_least A n} = n" using assms by simp
have 3: "finite {k ∈ A. k < nth_least A n}"
using 2 Collect_empty_eq card.infinite infinite_imp_nonempty least_not_less nth_least.simps(1)
by (metis (no_types, lifting))
have "card {k ∈ A. k ≤ nth_least A n} = card ({nth_least A n} ∪ {k ∈ A. k < nth_least A n})"
unfolding 1 by rule
also have "… = card {nth_least A n} + card {k ∈ A. k < nth_least A n}" using 3 by simp
also have "… = Suc n" using assms by simp
finally show ?thesis by this
qed

lemma nth_least_card:
fixes k :: nat
assumes "k ∈ A"
shows "nth_least A (card {i ∈ A. i < k}) = k"
proof (rule nat_set_card_equality_less)
have 1: "enat (card {l ∈ A. l < k}) < esize A"
proof (cases "finite A")
case False
show ?thesis using False by simp
next
case True
have 1: "{l ∈ A. l < k} ⊂ A" using assms by blast
have 2: "card {l ∈ A. l < k} < card A" using psubset_card_mono True 1 by this
show ?thesis using True 2 by simp
qed
show "nth_least A (card {l ∈ A. l < k}) ∈ A" using 1 by rule
show "k ∈ A" using assms by this
show "card {z ∈ A. z < nth_least A (card {i ∈ A. i < k})} = card {z ∈ A. z < k}" using 1 by simp
qed

interpretation nth_least:
bounded_function_pair "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}"
using nth_least_wellformed card_wellformed by (unfold_locales, blast+)

interpretation nth_least:
injection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}"
using card_nth_least by (unfold_locales, blast)

interpretation nth_least:
surjection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}"
for A :: "nat set"
using nth_least_card by (unfold_locales, blast)

interpretation nth_least:
bijection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}"
for A :: "nat set"
by unfold_locales

lemma nth_least_strict_mono_inverse:
fixes A :: "nat set"
assumes "enat k < esize A" "enat l < esize A" "nth_least A k < nth_least A l"
shows "k < l"
using assms by (metis not_less_iff_gr_or_eq nth_least_strict_mono)

lemma nth_least_less_card_less:
fixes k :: nat
shows "enat n < esize A ∧ nth_least A n < k ⟷ n < card {i ∈ A. i < k}"
proof safe
assume 1: "enat n < esize A" "nth_least A n < k"
have 2: "nth_least A n ∈ A" using 1(1) by rule
have "n = card {i ∈ A. i < nth_least A n}" using 1 by simp
also have "… < card {i ∈ A. i < k}" using 1(2) 2 by simp
finally show "n < card {i ∈ A. i < k}" by this
next
assume 1: "n < card {i ∈ A. i < k}"
have "enat n < enat (card {i ∈ A. i < k})" using 1 by simp
also have "… = esize {i ∈ A. i < k}" by simp
also have "… ≤ esize A" by blast
finally show 2: "enat n < esize A" by this
have 3: "n = card {i ∈ A. i < nth_least A n}" using 2 by simp
have 4: "card {i ∈ A. i < nth_least A n} < card {i ∈ A. i < k}" using 1 2 by simp
have 5: "nth_least A n ∈ A" using 2 by rule
show "nth_least A n < k" using 4 5 by simp
qed

lemma nth_least_less_esize_less:
"enat n < esize A ∧ enat (nth_least A n) < k ⟷ enat n < esize {i ∈ A. enat i < k}"
using nth_least_less_card_less by (cases k, simp+)

lemma nth_least_le:
assumes "enat n < esize A"
shows "n ≤ nth_least A n"
using assms
proof (induct n)
case 0
show ?case using 0 by simp
next
case (Suc n)
have "n ≤ nth_least A n" using Suc by (metis Suc_ile_eq less_imp_le)
also have "… < nth_least A (Suc n)" using nth_least_strict_mono Suc(2) by blast
finally show ?case by simp
qed

lemma nth_least_eq:
assumes "enat n < esize A" "enat n < esize B"
assumes "⋀ i. i ≤ nth_least A n ⟹ i ≤ nth_least B n ⟹ i ∈ A ⟷ i ∈ B"
shows "nth_least A n = nth_least B n"
using assms
proof (induct n arbitrary: A B)
case 0
have 1: "least A = least B"
proof (rule least_eq)
show "A ≠ {}" using 0(1) by simp
show "B ≠ {}" using 0(2) by simp
next
fix i
assume 2: "i ≤ least A" "i ≤ least B"
show "i ∈ A ⟷ i ∈ B" using 0(3) 2 unfolding nth_least.simps by this
qed
show ?case using 1 by simp
next
case (Suc n)
have 1: "A ≠ {}" "B ≠ {}" using Suc(2, 3) by auto
have 2: "least A = least B"
proof (rule least_eq)
show "A ≠ {}" using 1(1) by this
show "B ≠ {}" using 1(2) by this
next
fix i
assume 3: "i ≤ least A" "i ≤ least B"
have 4: "nth_least A 0 ≤ nth_least A (Suc n)" using Suc(2) by blast
have 5: "nth_least B 0 ≤ nth_least B (Suc n)" using Suc(3) by blast
have 6: "i ≤ nth_least A (Suc n)" "i ≤ nth_least B (Suc n)" using 3 4 5 by auto
show "i ∈ A ⟷ i ∈ B" using Suc(4) 6 by this
qed
have 3: "nth_least (A - {least A}) n = nth_least (B - {least B}) n"
proof (rule Suc(1))
show "enat n < esize (A - {least A})" using Suc(2) 1(1) by simp
show "enat n < esize (B - {least B})" using Suc(3) 1(2) by simp
next
fix i
assume 3: "i ≤ nth_least (A - {least A}) n" "i ≤ nth_least (B - {least B}) n"
have 4: "i ≤ nth_least A (Suc n)" "i ≤ nth_least B (Suc n)" using 3 by simp+
have 5: "i ∈ A ⟷ i ∈ B" using Suc(4) 4 by this
show "i ∈ A - {least A} ⟷ i ∈ B - {least B}" using 2 5 by auto
qed
show ?case using 3 by simp
qed

lemma nth_least_restrict[simp]:
assumes "enat i < esize {i ∈ s. enat i < k}"
shows "nth_least {i ∈ s. enat i < k} i = nth_least s i"
proof (rule nth_least_eq)
show "enat i < esize {i ∈ s. enat i < k}" using assms by this
show "enat i < esize s" using nth_least_less_esize_less assms by auto
next
fix l
assume 1: "l ≤ nth_least {i ∈ s. enat i < k} i"
have 2: "nth_least {i ∈ s. enat i < k} i ∈ {i ∈ s. enat i < k}" using assms by rule
have "enat l ≤ enat (nth_least {i ∈ s. enat i < k} i)" using 1 by simp
also have "… < k" using 2 by simp
finally show "l ∈ {i ∈ s. enat i < k} ⟷ l ∈ s" by auto
qed

lemma least_nth_least[simp]:
assumes "A ≠ {}" "⋀ i. i ∈ A ⟹ enat i < esize B"
shows "least (nth_least B  A) = nth_least B (least A)"
using assms by simp

lemma nth_least_nth_least[simp]:
assumes "enat n < esize A" "⋀ i. i ∈ A ⟹ enat i < esize B"
shows "nth_least B (nth_least A n) = nth_least (nth_least B  A) n"
using assms
proof (induct n arbitrary: A)
case 0
show ?case using 0 by simp
next
case (Suc n)
have 1: "A ≠ {}" using Suc(2) by auto
have 2: "nth_least B  (A - {least A}) = nth_least B  A - nth_least B  {least A}"
proof (rule inj_on_image_set_diff)
show "inj_on (nth_least B) {i. enat i < esize B}" using nth_least.inj_on by this
show "A - {least A} ⊆ {i. enat i < esize B}" using Suc(3) by blast
show "{least A} ⊆ {i. enat i < esize B}" using Suc(3) 1 by force
qed
have "nth_least B (nth_least A (Suc n)) = nth_least B (nth_least (A - {least A}) n)" by simp
also have "… = nth_least (nth_least B  (A - {least A})) n" using Suc 1 by force
also have "… = nth_least (nth_least B  A - nth_least B  {least A}) n" unfolding 2 by rule
also have "… = nth_least (nth_least B  A - {nth_least B (least A)}) n" by simp
also have "… = nth_least (nth_least B  A - {least (nth_least B  A)}) n" using Suc(3) 1 by auto
also have "… = nth_least (nth_least B  A) (Suc n)" by simp
finally show ?case by this
qed

lemma nth_least_Max[simp]:
assumes "finite A" "A ≠ {}"
shows "nth_least A (card A - 1) = Max A"
using assms
proof (induct "card A - 1" arbitrary: A)
case 0
have 1: "card A = 1" using 0 by (metis One_nat_def Suc_diff_1 card_gt_0_iff)
obtain a where 2: "A = {a}" using 1 by rule
show ?case unfolding 2 by (simp del: insert_iff)
next
case (Suc n)
have 1: "least A ∈ A" using Suc(4) by rule
have 2: "card (A - {least A}) = Suc n" using Suc(2, 3) 1 by simp
have 3: "A - {least A} ≠ {}" using 2 Suc(3) by fastforce
have "nth_least A (card A - 1) = nth_least A (Suc n)" unfolding Suc(2) by rule
also have "… = nth_least (A - {least A}) n" by simp
also have "… = nth_least (A - {least A}) (card (A - {least A}) - 1)" unfolding 2 by simp
also have "… = Max (A - {least A})"
proof (rule Suc(1))
show "n = card (A - {least A}) - 1" unfolding 2 by simp
show "finite (A - {least A})" using Suc(3) by simp
show "A - {least A} ≠ {}" using 3 by this
qed
also have "… = Max A" using Suc(3) 3 by simp
finally show ?case by this
qed

lemma nth_least_le_Max:
assumes "finite A" "A ≠ {}" "enat n < esize A"
shows "nth_least A n ≤ Max A"
proof -
have "nth_least A n ≤ nth_least A (card A - 1)"
proof (rule nth_least_mono)
show "enat (card A - 1) < esize A" by (metis Suc_diff_1 Suc_ile_eq assms(1) assms(2)
card_eq_0_iff esize_set.simps(1) not_gr0 order_refl)
show "n ≤ card A - 1" by (metis Suc_diff_1 Suc_leI antisym_conv assms(1) assms(3)
enat_ord_simps(2) esize_set.simps(1) le_less neq_iff not_gr0)
qed
also have "… = Max A" using nth_least_Max assms(1, 2) by this
finally show ?thesis by this
qed

lemma nth_least_not_contains:
fixes k :: nat
assumes "enat (Suc n) < esize A" "nth_least A n < k" "k < nth_least A (Suc n)"
shows "k ∉ A"
proof
assume 1: "k ∈ A"
have 2: "nth_least A (card {i ∈ A. i < k}) = k" using nth_least.right_inverse 1 by this
have 3: "n < card {i ∈ A. i < k}"
proof (rule nth_least_strict_mono_inverse)
show "enat n < esize A" using assms(1) by auto
show "enat (card {i ∈ A. i < k}) < esize A" using nth_least.g.wellformed 1 by simp
show "nth_least A n < nth_least A (card {i ∈ A. i < k})" using assms(2) 2 by simp
qed
have 4: "card {i ∈ A. i < k} < Suc n"
proof (rule nth_least_strict_mono_inverse)
show "enat (card {i ∈ A. i < k}) < esize A" using nth_least.g.wellformed 1 by simp
show "enat (Suc n) < esize A" using assms(1) by this
show "nth_least A (card {i ∈ A. i < k}) < nth_least A (Suc n)" using assms(3) 2 by simp
qed
show "False" using 3 4 by auto
qed

lemma nth_least_Suc[simp]:
assumes "enat n < esize A"
shows "nth_least (Suc  A) n = Suc (nth_least A n)"
using assms
proof (induct n arbitrary: A)
case (0)
have 1: "A ≠ {}" using 0 by auto
show ?case using 1 by simp
next
case (Suc n)
have 1: "enat n < esize (A - {least A})"
proof -
have 2: "A ≠ {}" using Suc(2) by auto
have 3: "least A ∈ A" using LeastI 2 by fast
have 4: "A = insert (least A) A" using 3 by auto
have "eSuc (enat n) = enat (Suc n)" by simp
also have "… < esize A" using Suc(2) by this
also have "… = esize (insert (least A) A)" using 4 by simp
also have "… = eSuc (esize (A - {least A}))" using 3 2 by simp
finally show ?thesis using Extended_Nat.eSuc_mono by metis
qed
have "nth_least (Suc  A) (Suc n) = nth_least (Suc  A - {least (Suc  A)}) n" by simp
also have "… = nth_least (Suc  (A - {least A})) n" by simp
also have "… = Suc (nth_least (A - {least A}) n)" using Suc(1) 1 by this
also have "… = Suc (nth_least A (Suc n))" by simp
finally show ?case by this
qed

lemma nth_least_lift[simp]:
"nth_least (lift A) 0 = 0"
"enat n < esize A ⟹ nth_least (lift A) (Suc n) = Suc (nth_least A n)"
unfolding lift_def by simp+

lemma nth_least_list_card[simp]:
assumes "enat n ≤ esize A"
shows "card {k ∈ A. k < nth_least (lift A) n} = n"
using less_Suc_eq_le assms by (cases n, auto simp del: nth_least.simps)

end

# Theory Coinductive_List_Extensions

section ‹Coinductive Lists›

theory Coinductive_List_Extensions
imports
Coinductive.Coinductive_List
Coinductive.Coinductive_List_Prefix
Coinductive.Coinductive_Stream
"../Extensions/List_Extensions"
"../Extensions/ESet_Extensions"
begin

hide_const (open) Sublist.prefix
hide_const (open) Sublist.suffix

declare list_of_lappend[simp]
declare lnth_lappend1[simp]
declare lnth_lappend2[simp]
declare lprefix_llength_le[dest]
declare Sup_llist_def[simp]
declare length_list_of[simp]
declare llast_linfinite[simp]
declare lnth_ltake[simp]
declare lappend_assoc[simp]
declare lprefix_lappend[simp]

lemma lprefix_lSup_revert: "lSup = Sup" "lprefix = less_eq" by auto
assumes "mcont lub ord lSup lprefix f"
assumes "mcont lub ord lSup lprefix g"
shows "ccpo.admissible lub ord (λ x. lprefix (f x) (g x))"
using ccpo_class.admissible_leI assms unfolding lprefix_lSup_revert by this
assumes "⋀ u. u ≤ v ⟹ lfinite u ⟹ P u"
shows "P v"
using assms by (metis LNil_lprefix le_llist_conv_lprefix lfinite.simps llist_gen_induct)

abbreviation "linfinite w ≡ ¬ lfinite w"

notation LNil ("<>")
notation LCons (infixr "%" 65)
notation lzip (infixr "¦¦" 51)
notation lappend (infixr "\$" 65)
notation lnth (infixl "?!" 100)

syntax "_llist" :: "args ⇒ 'a llist" ("<_>")
translations
"<a, x>" ⇌ "a % <x>"
"<a>" ⇌ "a % <>"

lemma eq_LNil_conv_lnull[simp]: "w = <> ⟷ lnull w" by auto
lemma Collect_lnull[simp]: "{w. lnull w} = {<>}" by auto

lemma inj_on_ltake: "inj_on (λ k. ltake k w) {.. llength w`