Session Partial_Order_Reduction

Theory List_Prefixes

section ‹List Prefixes›

theory List_Prefixes
imports "HOL-Library.Prefix_Order"
begin

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

  lemmas [intro?] = take_is_prefix[folded less_eq_list_def]

  hide_const (open) Sublist.prefix Sublist.suffix

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

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

end

Theory List_Extensions

section ‹Lists›

theory List_Extensions
imports "HOL-Library.Sublist"
begin

  declare remove1_idem[simp]

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

  notation zip (infixr "||" 51)

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

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

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

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

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

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

  lemma split_list_first_unique:
    assumes "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
  "../Extensions/List_Extensions"
  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
  "HOL-Library.Infinite_Set"
begin

  declare finite_subset[intro]

  lemma set_not_emptyI[intro 0]: "x  S  S  {}" by auto
  lemma sets_empty_iffI[intro 0]:
    assumes " a. a  A   b. b  B"
    assumes " b. b  B   a. a  A"
    shows "A = {}  B = {}"
    using assms by auto
  lemma disjointI[intro 0]:
    assumes " x. x  A  x  B  False"
    shows "A  B = {}"
    using assms by auto
  lemma range_subsetI[intro 0]:
    assumes " x. f x  S"
    shows "range f  S"
    using assms by blast

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

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

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

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

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

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

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

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

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

  abbreviation "least A  LEAST k. k  A"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end

Theory Basic_Extensions

section ‹Basics›

theory Basic_Extensions
imports "HOL-Library.Infinite_Set"
begin

  subsection ‹Types›

    type_synonym 'a step = "'a  'a"

  subsection ‹Rules›

    declare less_imp_le[dest, simp]
  
    declare le_funI[intro]
    declare le_funE[elim]
    declare le_funD[dest]
  
    lemma IdI'[intro]:
      assumes "x = y"
      shows "(x, y)  Id"
      using assms by auto

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

    lemma (in linorder) linorder_cases':
      obtains (le) "x  y" | (gt) "x > y"
      by force
  
    lemma monoI_comp[intro]:
      assumes "mono f" "mono g"
      shows "mono (f  g)"
      using assms by (intro monoI, auto dest: monoD)
    lemma strict_monoI_comp[intro]:
      assumes "strict_mono f" "strict_mono g"
      shows "strict_mono (f  g)"
      using assms by (intro strict_monoI, auto dest: strict_monoD)

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

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

  subsection ‹Constants›

    definition const :: "'a  'b  'a"
      where "const x  λ _. x"
    definition const2 :: "'a  'b  'c  'a"
      where "const2 x  λ _ _. x"
    definition const3 :: "'a  'b  'c  'd  'a"
      where "const3 x  λ _ _ _. x"
    definition const4 :: "'a  'b  'c  'd  'e  'a"
      where "const4 x  λ _ _ _ _. x"
    definition const5 :: "'a  'b  'c  'd  'e  'f  'a"
      where "const5 x  λ _ _ _ _ _. x"
  
    lemma const_apply[simp]: "const x y = x" unfolding const_def by rule
    lemma const2_apply[simp]: "const2 x y z = x" unfolding const2_def by rule
    lemma const3_apply[simp]: "const3 x y z u = x" unfolding const3_def by rule
    lemma const4_apply[simp]: "const4 x y z u v = x" unfolding const4_def by rule
    lemma const5_apply[simp]: "const5 x y z u v w = x" unfolding const5_def by rule

    definition zip_fun :: "('a  'b)  ('a  'c)  'a  'b × 'c" (infixr "" 51)
      where "f  g  λ x. (f x, g x)"
  
    lemma zip_fun_simps[simp]:
      "(f  g) x = (f x, g x)"
      "fst  (f  g) = f"
      "snd  (f  g) = g"
      "fst  h  snd  h = h"
      "fst ` range (f  g) = range f"
      "snd ` range (f  g) = range g"
      unfolding zip_fun_def by force+
  
    lemma zip_fun_eq[dest]:
      assumes "f  g = h  i"
      shows "f = h" "g = i"
      using assms unfolding zip_fun_def by (auto dest: fun_cong)
  
    lemma zip_fun_range_subset[intro, simp]: "range (f  g)  range f × range g"
      unfolding zip_fun_def by blast
    lemma zip_fun_range_finite[elim]:
      assumes "finite (range (f  g))"
      obtains "finite (range f)" "finite (range g)"
    proof
      show "finite (range f)" using finite_imageI [OF assms(1), of fst]
        by (simp add: image_image)
      show "finite (range g)" using finite_imageI [OF assms(1), of snd]
        by (simp add: image_image)
    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
  "Basics/Word_Prefixes"
  "Extensions/Set_Extensions"
  "Extensions/Relation_Extensions"
  Transition_Systems_and_Automata.Transition_System
  Transition_Systems_and_Automata.Transition_System_Extra
  Transition_Systems_and_Automata.Transition_System_Construction
begin

  context transition_system_initial
  begin

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

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

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

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

  end

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

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

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

    abbreviation "invisible  - visible"

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

  end

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

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

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

  end

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

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

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

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

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

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

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

  end

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

end

Theory Traces

section ‹Trace Theory›

theory Traces
imports "Basics/Word_Prefixes"
begin

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

    abbreviation Ind :: "'item set  'item set  bool"
      where "Ind A B   a  A.  b  B. ind a b"

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

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

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

    lemma eq_swap_length[dest]: "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 "../Extensions/Set_Extensions"
begin

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

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

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

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

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

  end

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

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

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

  end

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

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

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

  end

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

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

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

  end

  locale bijection = injection + surjection

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

end

Theory ENat_Extensions

section ‹Extended Natural Numbers›

theory ENat_Extensions
imports
  Coinductive.Coinductive_Nat
begin

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

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

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

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

end

Theory CCPO_Extensions

section ‹Chain-Complete Partial Orders›

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

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

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

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

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

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

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

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

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

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

  end

  class esize_ccpo = esize_order + ccpo
  begin

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

    lemma esize_mcont: "mcont Sup less_eq Sup less_eq esize"
      by (blast intro: mcontI monotoneI contI)
  
    lemmas mcont2mcont_esize = esize_mcont[THEN lfp.mcont2mcont, simp, cont_intro]

  end

end

Theory ESet_Extensions

section ‹Sets and Extended Natural Numbers›

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

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

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

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

  instantiation set :: (type) esize_ccpo
  begin

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

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

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

  end

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end

Theory Coinductive_List_Extensions

section ‹Coinductive Lists›

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

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

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

  lemma lprefix_lSup_revert: "lSup = Sup" "lprefix = less_eq" by auto
  lemma admissible_lprefixI[cont_intro]:
    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
  lemma llist_lift_admissible:
    assumes "ccpo.admissible lSup lprefix P"
    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