Theory Partial_Order_Reduction.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