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