Theory More_Lists

theory More_Lists
  imports Main
begin

lemma list_2_preds_aux:
  "⟦x' ∈ set xs; P1 x'; ⋀xs1 x xs2. ⟦xs = xs1 @ [x] @ xs2; P1 x⟧ ⟹
      ∃ys1 y ys2. x # xs2 = ys1 @ [y] @ ys2 ∧ P2 y⟧ ⟹ 
     ∃ xs1 x xs2. xs = xs1 @ [x] @ xs2 ∧ P2 x ∧ (∀y∈set xs2. ¬ P1 y)"
proof(goal_cases)
  case assms: 1

  define property 
       where "property xs =
                (∀xs2 xs1 x. (xs = xs1 @ [x] @ xs2 ∧ P1 x) ⟶
                   (∃ys1 y ys2. x#xs2 = ys1 @ [y] @ ys2 ∧ P2 y))"
       for xs

  have propE: "⟦property xs;
               (⋀xs1 x xs2. ⟦xs = xs1 @ [x] @ xs2; P1 x⟧ ⟹
                  ∃ys1 y ys2. x#xs2 = ys1 @ [y] @ ys2 ∧ P2 y) ⟹ P⟧
              ⟹ P" for xs P
    by(auto simp add: property_def)

  have property_append: "property (xs @ ys) ⟹ property ys" for xs ys
    by(auto simp: property_def)

  have "property xs"
    using assms(3)
    by (force simp: property_def)



  thus  ?thesis
    using assms(1,2)
  proof(induction xs arbitrary: x')
    case Nil
    then show ?case 
      by auto
  next
    case (Cons a xs)
    hence "property xs" 
      by(auto intro: property_append[where xs = "[a]"])

    show ?case
    proof(cases "x' = a")
      case x_eq_a: True

      then obtain ys1 y ys2 where "x'#xs = ys1 @ [y] @ ys2" "P2 y"
        using ‹property (a # xs)› ‹P1 x'›
        apply(elim propE)
        by (auto 10 10)

      show ?thesis
      proof(cases "ys1 = []")
        case ys1_empty: True
        hence "xs = ys2"
          using ‹x'#xs = ys1 @ [y] @ ys2›
          by auto
        then show ?thesis
        proof(cases "∃x∈set ys2. P1 x")
          case x_in_ys2: True
          then obtain x where "x ∈ set ys2" "P1 x"
            by auto
          hence "∃xs1 x xs2. xs = xs1 @ [x] @ xs2 ∧ P2 x ∧ (∀y∈set xs2. ¬ P1 y)"
            using ‹property xs› ‹xs = ys2› ‹P2 y›
            apply(intro Cons(1))
            by auto
          then obtain xs1 x xs2 where "(a # xs) = (a #xs1) @ [x] @ xs2 ∧ P2 x ∧ (∀y∈set xs2. ¬ P1 y)"
            by auto
          then show ?thesis
            by metis
        next
          case x_notin_ys2: False
          hence "a # xs = a#ys2 ∧ P2 y ∧ (∀y∈set ys2. ¬ P1 y)"
            using ‹xs = ys2› ‹P2 y›
            by auto
          then show ?thesis
            using ‹x' # xs = ys1 @ [y] @ ys2› x_eq_a
            by blast
        qed
      next
        case ys2_nempty: False
        then obtain ys1' where "xs = ys1' @ [y] @ ys2"
          using ‹x'#xs = ys1 @ [y] @ ys2›
          by (auto simp: neq_Nil_conv)
        show ?thesis
        proof(cases "∃x∈set ys2. P1 x")
          case x_in_ys2: True
          then obtain x where "x ∈ set ys2" "P1 x"
            by auto
          hence "∃xs1 x xs2. xs = xs1 @ [x] @ xs2 ∧ P2 x ∧ (∀y∈set xs2. ¬ P1 y)"
            using ‹property xs› ‹xs = ys1' @ [y] @ ys2› ‹P2 y›
            apply(intro Cons(1))
            by auto
          then obtain xs1 x xs2 where "(a # xs) = (a #xs1) @ [x] @ xs2 ∧ P2 x ∧ (∀y∈set xs2. ¬ P1 y)"
            by auto
          then show ?thesis
            by metis
        next
          case x_notin_ys2: False
          hence "a # xs = (a# ys1') @ [y] @ ys2 ∧ P2 y ∧ (∀y∈set ys2. ¬ P1 y)"
            using ‹xs = ys1' @ [y] @ ys2› ‹P2 y›
            by auto
          then show ?thesis
            by metis
        qed
      qed
    next
      case x_neq_a: False
      hence "x' ∈ set xs"
        using Cons
        by auto
      then obtain xs1 x xs2 where "xs = xs1 @ [x] @ xs2" "P2 x" "(∀y∈set xs2. ¬ P1 y)"
        using Cons ‹property xs›
        by blast
      hence "a # xs = (a # xs1) @ [x] @ xs2 ∧ P2 x ∧ (∀y∈set xs2. ¬ P1 y)"
        by auto
      thus ?thesis
        by metis
    qed
  qed
qed

lemma list_2_preds:
  "⟦ x∈set xs; P1 x; ⋀xs1 x xs2. ⟦xs = xs1 @ [x] @ xs2; P1 x⟧ ⟹ ∃ys1 y ys2. x#xs2 = ys1 @ [y] @ ys2 ∧ P2 y⟧ ⟹ 
     ∃ xs1 x xs2. xs = xs1 @ [x] @ xs2 ∧ P2 x ∧ (∀y∈set xs2. ¬ P1 y ∧ ¬ P2 y)"
proof(goal_cases)
  case assms: 1
  hence "∃xs1 x xs2. xs = xs1 @ [x] @ xs2 ∧ P2 x ∧ (∀y∈set xs2. ¬ P1 y)"
    by (fastforce intro!: list_2_preds_aux)
  then obtain xs1 x xs2 where "xs = xs1 @ [x] @ xs2" "P2 x" "(∀y∈set xs2. ¬ P1 y)"
    by auto
  hence "∃ys1 y ys2. x # xs2 = ys1 @ [y] @ ys2 ∧ P2 y ∧ (∀z∈set ys2. ¬ P2 z)"
    by (auto intro!: split_list_last_prop)
  then obtain ys1 y ys2 where "x # xs2 = ys1 @ [y] @ ys2" "P2 y" "(∀z∈set ys2. ¬ P2 z)"
    by auto
  hence "(∀z∈set ys2. ¬P1 z ∧ ¬ P2 z)"
    using ‹(∀y∈set xs2. ¬ P1 y)› ‹P2 x›
    by (metis Un_iff insert_iff list.simps(15) set_append)
  moreover have "xs = (xs1 @ ys1) @ [y] @ ys2"
    using ‹xs = xs1 @ [x] @ xs2› ‹x # xs2 = ys1 @ [y] @ ys2›
    by auto
  ultimately show ?case
    using ‹P2 y›
    by fastforce
qed

lemma list_inter_mem_iff: "set xs ∩ s ≠ {} ⟷ (∃xs1 x xs2. xs = xs1 @ [x] @ xs2 ∧ x ∈ s)"
  by (metis append.left_neutral append_Cons disjoint_iff in_set_conv_decomp)
end