# Theory List_Prefixes

section ‹List Prefixes›

theory List_Prefixes
imports
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
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 "u1 @ [a] @ u2 = v1 @ [a] @ v2" "a  set u1" "a  set v1"
shows "u1 = v1"
proof -
obtain w where "u1 = v1 @ w  w @ [a] @ u2 = [a] @ v2
u1 @ w = v1  [a] @ u2 = w @ [a] @ v2" 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

Transition_Systems_and_Automata.Sequence
begin

definition prefix_fininf :: "'a list  'a stream  bool" (infix "FI" 50)
where "u FI v   w. u @- w = v"

lemma prefix_fininfI[intro]:
assumes "u @- w = v"
shows "u FI v"
using assms unfolding prefix_fininf_def by auto
lemma prefix_fininfE[elim]:
assumes "u FI v"
obtains w
where "v = u @- w"
using assms unfolding prefix_fininf_def by auto

lemma prefix_fininfI_empty[intro!]: "[] FI w" by force
lemma prefix_fininfI_item[intro!]:
assumes "a = b" "u FI v"
shows "a # u FI b ## v"
using assms by force
lemma prefix_fininfE_item[elim!]:
assumes "a # u FI b ## v"
obtains "a = b" "u FI v"
using assms by force

lemma prefix_fininf_item[simp]: "a # u FI a ## v  u FI v" by force
lemma prefix_fininf_list[simp]: "w @ u FI w @- v  u FI v" by (induct w, auto)
lemma prefix_fininf_conc[intro]: "u FI u @- v" by auto
lemma prefix_fininf_prefix[intro]: "stake k w FI w" using stake_sdrop by blast
lemma prefix_fininf_set_range[dest]: "u FI v  set u  sset v" by auto

lemma prefix_fininf_absorb:
assumes "u FI 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 FI 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 FI w" "v FI 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 FI v @- w"
obtains (absorb) "u  v" | (extend) z where "u = v @ z" "z FI 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 FI w" by rule
qed
qed

lemma prefix_fin_prefix_fininf_trans[trans, intro]: "u  v  v FI w  u FI 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 FI 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 FI 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 x0" " 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 x0" " 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 x0 x'"
have [simp]: "Q 0 = x0" " 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 x0" " 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 x0" " 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 x0 x'"
have [simp]: "Q 0 = x0" " 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 u0 v0" " 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 (u0, v0)" 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

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
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 "r1 <*rlex*> r2  inv_image (r2 <*lex*> r1) 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

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
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]: "w1 =S w2  length w1 = length w2" by force
lemma eq_swap_range[dest]: "w1 =S w2  set w1 = set w2" by force

lemma eq_swap_extend:
assumes "w1 =S w2"
shows "u @ w1 @ v =S u @ w2 @ 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 "w1 =S w2"
obtains (equal) "remove1 c w1 = remove1 c w2" | (swap) "remove1 c w1 =S remove1 c w2"
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 "w1 =S w2"
shows "rev w1 =S rev w2"
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]: "w1 =F w2  length w1 = length w2"
by (induct rule: rtranclp.induct, auto)
lemma eq_fin_range[dest]: "w1 =F w2  set w1 = set w2"
by (induct rule: rtranclp.induct, auto)

lemma eq_fin_remove1:
assumes "w1 =F w2"
shows "remove1 c w1 =F remove1 c w2"
using assms
proof induct
case (base)
show ?case by simp
next
case (step w2 w3)
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 "w1 =F w2"
shows "rev w1 =F rev w2"
using assms by (induct, auto dest: eq_swap_rev)

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

lemma eq_fin_concat: "u @ w1 @ v =F u @ w2 @ v  w1 =F w2"
proof
assume 0: "u @ w1 @ v =F u @ w2 @ v"
have 1: "w1 @ v =F w2 @ v" using eq_fin_concat_eq_fin_start 0 by this
have 2: "rev (w1 @ v) =F rev (w2 @ v)" using 1 by (blast dest: eq_fin_rev)
have 3: "rev v @ rev w1 =F rev v @ rev w2" using 2 by simp
have 4: "rev w1 =F rev w2" using eq_fin_concat_eq_fin_start 3 by this
have 5: "rev (rev w1) =F rev (rev w2)" using 4 by (blast dest: eq_fin_rev)
show "w1 =F w2" using 5 by simp
next
show "u @ w1 @ v =F u @ w2 @ v" if "w1 =F w2"
using that by (induct, auto dest: eq_swap_extend[of _ _ u v])
qed
lemma eq_fin_concat_start[iff]: "w @ w1 =F w @ w2  w1 =F w2"
using eq_fin_concat[of "w" _ "[]"] by simp
lemma eq_fin_concat_end[iff]: "w1 @ w =F w2 @ w  w1 =F w2"
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 "w1 F w2   v1. w1 @ v1 =F w2"

lemma le_finI[intro 0]:
assumes "w1 @ v1 =F w2"
shows "w1 F w2"
using assms unfolding le_fin_def by auto
lemma le_finE[elim 0]:
assumes "w1 F w2"
obtains v1
where "w1 @ v1 =F w2"
using assms unfolding le_fin_def by auto

lemma le_fin_empty[simp]: "[] F w" by force
lemma le_fin_trivial[intro]: "w1 =F w2  w1 F w2"
proof
assume 1: "w1 =F w2"
show "w1 @ [] =F w2" using 1 by simp
qed

lemma le_fin_length[dest]: "w1 F w2  length w1  length w2" by force
lemma le_fin_range[dest]: "w1 F w2  set w1  set w2" by force

lemma eq_fin_alt_def: "w1 =F w2  w1 F w2  w2 F w1"
proof
show "w1 F w2  w2 F w1" if "w1 =F w2" using that by blast
next
assume 0: "w1 F w2  w2 F w1"
have 1: "w1 F w2" "w2 F w1" using 0 by auto
have 10: "length w1 = length w2" using 1 by force
obtain v1 v2 where 2: "w1 @ v1 =F w2" "w2 @ v2 =F w1" using 1 by (elim le_finE)
have 3: "length w1 = length (w1 @ v1)" using 2 10 by force
have 4: "w1 = w1 @ v1" using 3 by auto
have 5: "length w2 = length (w2 @ v2)" using 2 10 by force
have 6: "w2 = w2 @ v2" using 5 by auto
show "w1 =F w2" 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 "w1 F w2" "w2 F w3"
shows "w1 F w3"
proof -
obtain v1 where 1: "w1 @ v1 =F w2" using assms(1) by rule
obtain v2 where 2: "w2 @ v2 =F w3" using assms(2) by rule
show ?thesis
proof
have "w1 @ v1 @ v2 = (w1 @ v1) @ v2" by simp
also have " =F w2 @ v2" using 1 by blast
also have " =F w3" using 2 by blast
finally show "w1 @ v1 @ v2 =F w3" by this
qed
qed
lemma eq_fin_le_fin_transp[intro, trans]:
assumes "w1 =F w2" "w2 F w3"
shows "w1 F w3"
using assms by auto
lemma le_fin_eq_fin_transp[intro, trans]:
assumes "w1 F w2" "w2 =F w3"
shows "w1 F w3"
using assms by auto
lemma prefix_le_fin_transp[intro, trans]:
assumes "w1  w2" "w2 F w3"
shows "w1 F w3"
proof -
obtain v1 where 1: "w2 = w1 @ v1" using assms(1) by rule
obtain v2 where 2: "w2 @ v2 =F w3" using assms(2) by rule
show ?thesis
proof
show "w1 @ v1 @ v2 =F w3" using 1 2 by simp
qed
qed
lemma le_fin_prefix_transp[intro, trans]:
assumes "w1 F w2" "w2  w3"
shows "w1 F w3"
proof -
obtain v1 where 1: "w1 @ v1 =F w2" using assms(1) by rule
obtain v2 where 2: "w3 = w2 @ v2" using assms(2) by rule
show ?thesis
proof
have "w1 @ v1 @ v2 = (w1 @ v1) @ v2" by simp
also have " =F w2 @ v2" using 1 by blast
also have " = w3" using 2 by simp
finally show "w1 @ v1 @ v2 =F w3" by this
qed
qed
lemma prefix_eq_fin_transp[intro, trans]:
assumes "w1  w2" "w2 =F w3"
shows "w1 F w3"
using assms by auto

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

definition le_fininf :: "'item list  'item stream  bool" (infix "FI" 50)
where "w1 FI w2   v2. v2 FI w2  w1 F v2"

lemma le_fininfI[intro 0]:
assumes "v2 FI w2" "w1 F v2"
shows "w1 FI w2"
using assms unfolding le_fininf_def by auto
lemma le_fininfE[elim 0]:
assumes "w1 FI w2"
obtains v2
where "v2 FI w2" "w1 F v2"
using assms unfolding le_fininf_def by auto

lemma le_fininf_empty[simp]: "[] FI w" by force

lemma le_fininf_range[dest]: "w1 FI w2  set w1  sset w2" by force

lemma eq_fin_le_fininf_transp[intro, trans]:
assumes "w1 =F w2" "w2 FI w3"
shows "w1 FI w3"
using assms by blast
lemma le_fin_le_fininf_transp[intro, trans]:
assumes "w1 F w2" "w2 FI w3"
shows "w1 FI w3"
using assms by blast
lemma prefix_le_fininf_transp[intro, trans]:
assumes "w1  w2" "w2 FI w3"
shows "w1 FI w3"
using assms by auto
lemma le_fin_prefix_fininf_transp[intro, trans]:
assumes "w1 F w2" "w2 FI w3"
shows "w1 FI w3"
using assms by auto
lemma eq_fin_prefix_fininf_transp[intro, trans]:
assumes "w1 =F w2" "w2 FI w3"
shows "w1 FI w3"
using assms by auto

lemma le_fininf_concat_start[iff]: "w @ w1 FI w @- w2  w1 FI w2"
proof
assume 0: "w @ w1 FI w @- w2"
obtain v2 where 1: "v2 FI w @- w2" "w @ w1 F v2" using 0 by rule
have 2: "length w  length v2" using 1(2) by force
have 4: "w  v2" using prefix_fininf_extend[OF 1(1) 2] by this
obtain v1 where 5: "v2 = w @ v1" using 4 by rule
show "w1 FI w2"
proof
show "v1 FI w2" using 1(1) unfolding 5 by auto
show "w1 F v1" using 1(2) unfolding 5 by simp
qed
next
assume 0: "w1 FI w2"
obtain v2 where 1: "v2 FI w2" "w1 F v2" using 0 by rule
show "w @ w1 FI w @- w2"
proof
show "w @ v2 FI (w @- w2)" using 1(1) by auto
show "w @ w1 F w @ v2" using 1(2) by auto
qed
qed

lemma le_fininf_singleton[intro, simp]: "[shd v] FI v"
proof -
have "[shd v] FI 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 "w1 I w2   v1. v1 FI w1  v1 FI w2"

lemma le_infI[intro 0]:
assumes " v1. v1 FI w1  v1 FI w2"
shows "w1 I w2"
using assms unfolding le_inf_def by auto
lemma le_infE[elim 0]:
assumes "w1 I w2" "v1 FI w1"
obtains "v1 FI w2"
using assms unfolding le_inf_def by auto

lemma le_inf_range[dest]:
assumes "w1 I w2"
shows "sset w1  sset w2"
proof
fix a
assume 1: "a  sset w1"
obtain i where 2: "a = w1 !! i" using 1 by (metis imageE sset_range)
have 3: "stake (Suc i) w1 FI w1" by rule
have 4: "stake (Suc i) w1 FI w2" using assms 3 by rule
have 5: "w1 !! i  set (stake (Suc i) w1)" by (meson lessI set_stake_snth)
show "a  sset w2" 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 "w1 FI w2" "w2 I w3"
shows "w1 FI w3"
using assms by blast
lemma le_fininf_le_inf_transp[intro, trans]:
assumes "w1 FI w2" "w2 I w3"
shows "w1 FI w3"
using assms by blast
lemma le_inf_transp[intro, trans]:
assumes "w1 I w2" "w2 I w3"
shows "w1 I w3"
using assms by blast

lemma le_infI':
assumes " k.  v. v FI w1  k < length v  v FI w2"
shows "w1 I w2"
proof
fix u
assume 1: "u FI w1"
obtain v where 2: "v FI w1" "length u < length v" "v FI w2" 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 FI w2" using 4 2(3) by rule
qed

lemma le_infI_chain_left:
assumes "chain w" " k. w k FI 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 FI limit w  k < length va  va FI v"
proof (intro exI conjI)
show "w l FI limit w" using chain_prefix_limit assms(1) by this
show "k < length (w l)" using 1 by this
show "w l FI v" using assms(2) by this
qed
qed
lemma le_infI_chain_right:
assumes "chain w" " u. u FI v  u F w (l u)"
shows "v I limit w"
proof
fix u
assume 1: "u FI v"
show "u FI limit w"
proof
show "w (l u) FI 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 FI 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 "w1 =I w2  w1 I w2  w2 I w1"

lemma eq_infI[intro 0]:
assumes "w1 I w2" "w2 I w1"
shows "w1 =I w2"
using assms unfolding eq_inf_def by auto
lemma eq_infE[elim 0]:
assumes "w1 =I w2"
obtains "w1 I w2" "w2 I w1"
using assms unfolding eq_inf_def by auto

lemma eq_inf_range[dest]: "w1 =I w2  sset w1 = sset w2" by force

lemma eq_inf_reflp[simp, intro]: "w =I w" by auto
lemma eq_inf_symp[intro]: "w1 =I w2  w2 =I w1" by auto
lemma eq_inf_transp[intro, trans]:
assumes "w1 =I w2" "w2 =I w3"
shows "w1 =I w3"
using assms by blast
lemma le_fininf_eq_inf_transp[intro, trans]:
assumes "w1 FI w2" "w2 =I w3"
shows "w1 FI w3"
using assms by blast
lemma le_inf_eq_inf_transp[intro, trans]:
assumes "w1 I w2" "w2 =I w3"
shows "w1 I w3"
using assms by blast
lemma eq_inf_le_inf_transp[intro, trans]:
assumes "w1 =I w2" "w2 I w3"
shows "w1 I w3"
using assms by blast
lemma prefix_fininf_eq_inf_transp[intro, trans]:
assumes "w1 FI w2" "w2 =I w3"
shows "w1 FI w3"
using assms by blast

lemma le_inf_concat_start[iff]: "w @- w1 I w @- w2  w1 I w2"
proof
assume 1: "w @- w1 I w @- w2"
show "w1 I w2"
proof
fix v1
assume 2: "v1 FI w1"
have "w @ v1 FI w @- w1" using 2 by auto
also have " I w @- w2" using 1 by this
finally show "v1 FI w2" by rule
qed
next
assume 1: "w1 I w2"
show "w @- w1 I w @- w2"
proof
fix v1
assume 2: "v1 FI w @- w1"
then show "v1 FI w @- w2"
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]: "w1 =F w2  w1 @- w I w2 @- w"
proof
fix v1
assume 1: "w1 =F w2" "v1 FI w1 @- w"
show "v1 FI w2 @- w"
using 1(2)
proof (cases rule: prefix_fininf_append)
case (absorb)
show ?thesis
proof
show "w2 FI (w2 @- w)" by auto
show "v1 F w2" using absorb 1(1) by auto
qed
next
case (extend w')
show ?thesis
proof
show "w2 @ w' FI (w2 @- w)" using extend(2) by auto
show "v1 F w2 @ w'" unfolding extend(1) using 1(1) by auto
qed
qed
qed

lemma eq_inf_concat_start[iff]: "w @- w1 =I w @- w2  w1 =I w2" by blast
lemma eq_inf_concat_end[dest]: "w1 =F w2  w1 @- w =I w2 @- w"
proof -
assume 0: "w1 =F w2"
have 1: "w2 =F w1" using 0 by auto
show "w1 @- w =I w2 @- 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 w1 @- w2"
shows "w1 FI w"
using assms by blast
lemma le_fininf_suffixE[elim]:
assumes "w1 FI w"
obtains w2
where "w =I w1 @- w2"
proof -
obtain v2 where 1: "v2 FI w" "w1 F v2" using assms(1) by rule
obtain u1 where 2: "w1 @ u1 =F v2" using 1(2) by rule
obtain v2' where 3: "w = v2 @- v2'" using 1(1) by rule
show ?thesis
proof
show "w =I w1 @- u1 @- v2'" unfolding 3 using 2 by fastforce
qed
qed

lemma subsume_fin:
assumes "u1 FI w" "v1 FI w"
obtains w1
where "u1 F w1" "v1 F w1"
proof -
obtain u2 where 2: "u2 FI w" "u1 F u2" using assms(1) by rule
obtain v2 where 3: "v2 FI w" "v1 F v2" using assms(2) by rule
show ?thesis
proof (cases "length u2" "length v2" rule: le_cases)
case le
show ?thesis
proof
show "u1 F v2" using 2(2) prefix_fininf_length[OF 2(1) 3(1) le] by auto
show "v1 F v2" using 3(2) by this
qed
next
case ge
show ?thesis
proof
show "u1 F u2" using 2(2) by this
show "v1 F u2" using 3(2) prefix_fininf_length[OF 3(1) 2(1) ge] by auto
qed
qed
qed

lemma eq_fin_end:
assumes "u1 =F u2" "u1 @ v1 =F u2 @ v2"
shows "v1 =F v2"
proof -
have "u1 @ v2 =F u2 @ v2" using assms(1) by blast
also have " =F u1 @ v1" using assms(2) by blast
finally show ?thesis by blast
qed

definition indoc :: "'item  'item list  bool"
where "indoc a u   u1 u2. u = u1 @ [a] @ u2  a  set u1  Ind {a} (set u1)"

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 v1 v2 where 1: "v = v1 @ [a] @ v2" "a  set v1" "Ind {a} (set v1)"
using assms(3) unfolding indoc_def by blast
show ?thesis
proof (unfold indoc_def, intro exI conjI)
show "u @ v = (u @ v1) @ [a] @ v2" unfolding 1(1) by simp
show "a  set (u @ v1)" using assms(1) 1(2) by auto
show "Ind {a} (set (u @ v1))" 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 w1 w2 where 1: "u @ v = w1 @ [a] @ w2" "a  set w1" "Ind {a} (set w1)"
using assms unfolding indoc_def by blast
show ?thesis
proof (cases "a  set u")
case True
obtain u1 u2 where 2: "u = u1 @ [a] @ u2" "a  set u1"
using split_list_first[OF True] by auto
have 3: "w1 = u1"
proof (rule split_list_first_unique)
show "w1 @ [a] @ w2 = u1 @ [a] @ u2 @ v" using 1(1) unfolding 2(1) by simp
show "a  set w1" using 1(2) by auto
show "a  set u1" 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 = u1 @ [a] @ u2" using 2(1) by this
show "a  set u1" using 1(2) unfolding 3 by this
show "Ind {a} (set u1)" 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 v1 v2 where 3: "v = v1 @ [a] @ v2" "a  set v1"
using split_list_first[OF 2] by auto
have 4: "w1 = u @ v1"
proof (rule split_list_first_unique)
show "w1 @ [a] @ w2 = (u @ v1) @ [a] @ v2" using 1(1) unfolding 3(1) by simp
show "a  set w1" using 1(2) by auto
show "a  set (u @ v1)" 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 = v1 @ [a] @ v2" using 3(1) by this
show "a  set v1" using 1(2) unfolding 4 by auto
show "Ind {a} (set v1)" 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 u1 u2 where 2: "[b] = u1 @ [a] @ u2" "Ind {a} (set u1)"
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 u1 @ [a] @ u2" "a  set u1"
shows "Ind {a} (set u1)"
proof -
have 1: "indoc a ([a] @ u)" by simp
have 2: "indoc a (u1 @ [a] @ u2)" 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 u1 u2 where 2: "u = u1 @ [a] @ u2" "a  set u1"
using split_list_first[OF assms(2)] by auto
have 3: "Ind {a} (set u1)"
proof (rule eq_fin_ind')
show "[a] @ w =F u1 @ [a] @ u2 @ v" using 1 unfolding 2(1) by simp
show "a  set u1" using 2(2) by this
qed
have 4: "Ind (set [a]) (set u1)" using 3 by simp
have "[a]  [a] @ u1 @ u2" by auto
also have " = ([a] @ u1) @ u2" by simp
also have " =F (u1 @ [a]) @ u2" 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 v1 v2 where 4: "v = v1 @ [a] @ v2" "a  set v1" using split_list_first[OF 3] by auto
have 5: "[a] @ w =F u @ v1 @ [a] @ v2" using 1 unfolding 4(1) by this
have 6: "Ind {a} (set (u @ v1))"
proof (rule eq_fin_ind')
show "[a] @ w =F (u @ v1) @ [a] @ v2" using 5 by simp
show "a  set (u @ v1)" using assms(2) 4(2) by auto
qed
have 9: "Ind (set [a]) (set v1)" using 6 by auto
have "[a]  [a] @ v1 @ v2" by auto
also have " = ([a] @ v1) @ v2" by simp
also have " =F (v1 @ [a]) @ v2" using 9 by blast
also have " = v1 @ [a] @ v2" by simp
also have " = v" unfolding 4(1) by rule
finally show ?thesis by this
qed
lemma le_fininf_not_member':
assumes "[a] FI u @- v" "a  set u"
shows "[a] FI v"
proof -
obtain v2 where 1: "v2 FI u @- v" "[a] F v2" using le_fininfE assms(1) by this
show ?thesis
using 1(1)
proof (cases rule: prefix_fininf_append)
case absorb
have "[a] F v2" 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 v2" 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 " FI 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 v1 v2 where 5: "v = v1 @ [a] @ v2" "a  set v1" using split_list_first[OF 4] by auto
have 7: "Ind {a} (set ([b] @ v1))"
proof (rule eq_fin_ind')
show "[a] @ u =F ([b] @ v1) @ [a] @ v2" using 3 unfolding 5(1) by simp
show "a  set ([b] @ v1)" 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] FI w" "[b] FI w" "a  b"
shows "ind a b"
using subsume_fin le_fin_ind'' assms by metis
lemma le_fininf_ind':
assumes "[a] FI w" "v FI 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 v1 v2 where 1: "v = v1 @ [a] @ v2" "a  set v1" "Ind {a} (set v1)"
using 0 unfolding indoc_def by blast
have 2: "Ind (set [a]) (set v1)" using 1(3) by simp
have "v = v1 @ [a] @ v2" using 1(1) by this
also have " = (v1 @ [a]) @ v2" by simp
also have " =F ([a] @ v1) @ v2" using 2 by blast
also have " = [a] @ v1 @ v2" 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 FI w  path v p"
shows "run w p"
using assms by coinduct auto

lemma (in transition_system) words_infI_construct':
assumes " k.  v. v FI w  k < length v  path v p"
shows "run w p"
proof
fix u
assume 1: "u FI w"
obtain v where 2: "v FI 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 FI limit w  k < length v  path v p"
proof (intro exI conjI)
show "w l FI 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 "w1 =S w2" "path w1 p"
shows "path w2 p"
using assms diamond_right by (induct, auto)
lemma eq_fin_word:
assumes "w1 =F w2" "path w1 p"
shows "path w2 p"
using assms eq_swap_word by (induct, auto)
lemma le_fin_word:
assumes "w1 F w2" "path w2 p"
shows "path w1 p"
using assms eq_fin_word by blast
lemma le_fininf_word:
assumes "w1 FI w2" "run w2 p"
shows "path w1 p"
using assms le_fin_word by blast
lemma le_inf_word:
assumes "w2 I w1" "run w1 p"
shows "run w2 p"
using assms le_fininf_word by (blast intro: words_infI_construct)
lemma eq_inf_word:
assumes "w1 =I w2" "run w1 p"
shows "run w2 p"
using assms le_inf_word by auto

lemma eq_swap_execute:
assumes "path w1 p" "w1 =S w2"
shows "fold ex w1 p = fold ex w2 p"
using assms(2, 1) diamond_right by (induct, auto)
lemma eq_fin_execute:
assumes "path w1 p" "w1 =F w2"
shows "fold ex w1 p = fold ex w2 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
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

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

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

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