Theory Util

section ‹Utility Definitions and Properties›

text ‹This file contains various definitions and lemmata not closely related to finite state
      machines or testing.›


theory Util
  imports Main "HOL-Library.FSet" "HOL-Library.Sublist" "HOL-Library.Mapping"
begin

subsection ‹Converting Sets to Maps›

text ‹This subsection introduces a function @{text "set_as_map"} that transforms a set of 
      @{text "('a × 'b)"} tuples to a map mapping each first value @{text "x"} of the contained tuples
      to all second values @{text "y"} such that @{text "(x,y)"} is contained in the set.›

definition set_as_map :: "('a × 'c) set ⇒ ('a ⇒ 'c set option)" where
  "set_as_map s = (λ x . if (∃ z . (x,z) ∈ s) then Some {z . (x,z) ∈ s} else None)"


lemma set_as_map_code[code] : 
  "set_as_map (set xs) = (foldl (λ m (x,z) . case m x of
                                                None ⇒ m (x ↦ {z}) |
                                                Some zs ⇒ m (x ↦  (insert z zs)))
                                Map.empty
                                xs)"
proof - 
  let ?f = "λ xs . (foldl (λ m (x,z) . case m x of
                                          None ⇒ m (x ↦ {z}) |
                                          Some zs ⇒ m (x ↦  (insert z zs)))
                          Map.empty
                          xs)"
  have "(?f xs) = (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None)"
  proof (induction xs rule: rev_induct)
    case Nil
    then show ?case by auto
  next
    case (snoc xz xs)
    then obtain x z where "xz = (x,z)"
      by force 

    have *: "(?f (xs@[(x,z)])) = (case (?f xs) x of
                                None ⇒ (?f xs) (x ↦ {z}) |
                                Some zs ⇒ (?f xs) (x ↦ (insert z zs)))"
      by auto

    then show ?case proof (cases "(?f xs) x")
      case None
      then have **: "(?f (xs@[(x,z)])) = (?f xs) (x ↦ {z})" using * by auto

      have scheme: "⋀ m k v . (m(k ↦ v)) = (λk' . if k' = k then Some v else m k')"
        by auto

      have m1: "(?f (xs@[(x,z)])) = (λ x' . if x' = x then Some {z} else (?f xs) x')"
        unfolding ** 
        unfolding scheme by force

      have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = None"
        using None snoc by auto
      then have "¬(∃ z . (x,z) ∈ set xs)"
        by (metis (mono_tags, lifting) option.distinct(1))
      then have "(∃ z . (x,z) ∈ set (xs@[(x,z)]))" and "{z' . (x,z') ∈ set (xs@[(x,z)])} = {z}"
        by auto
      then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) 
                                then Some {z' . (x',z') ∈ set (xs@[(x,z)])} 
                                else None)
                   = (λ x' . if x' = x 
                                then Some {z} else (λ x . if (∃ z . (x,z) ∈ set xs) 
                                                            then Some {z . (x,z) ∈ set xs} 
                                                            else None) x')"
        by force

      show ?thesis using m1 m2 snoc
        using ‹xz = (x, z)› by presburger
    next
      case (Some zs)
      then have **: "(?f (xs@[(x,z)])) = (?f xs) (x ↦ (insert z zs))" using * by auto
      have scheme: "⋀ m k v . (m(k ↦ v)) = (λk' . if k' = k then Some v else m k')"
        by auto

      have m1: "(?f (xs@[(x,z)])) = (λ x' . if x' = x then Some (insert z zs) else (?f xs) x')"
        unfolding ** 
        unfolding scheme by force

      have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = Some zs"
        using Some snoc by auto
      then have "(∃ z . (x,z) ∈ set xs)"
        unfolding case_prod_conv using  option.distinct(2) by metis
      then have "(∃ z . (x,z) ∈ set (xs@[(x,z)]))" by simp

      have "{z' . (x,z') ∈ set (xs@[(x,z)])} = insert z zs"
      proof -
        have "Some {z . (x,z) ∈ set xs} = Some zs"
          using ‹(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x 
                  = Some zs›
          unfolding case_prod_conv using  option.distinct(2) by metis
        then have "{z . (x,z) ∈ set xs} = zs" by auto
        then show ?thesis by auto
      qed

      have "⋀ a  . (λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) 
                              then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
                   = (λ x' . if x' = x 
                              then Some (insert z zs) 
                              else (λ x . if (∃ z . (x,z) ∈ set xs) 
                                            then Some {z . (x,z) ∈ set xs} else None) x') a" 
      proof -
        fix a show "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) 
                              then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
                   = (λ x' . if x' = x 
                              then Some (insert z zs) 
                              else (λ x . if (∃ z . (x,z) ∈ set xs) 
                                            then Some {z . (x,z) ∈ set xs} else None) x') a"
        using ‹{z' . (x,z') ∈ set (xs@[(x,z)])} = insert z zs› ‹(∃ z . (x,z) ∈ set (xs@[(x,z)]))›
        by (cases "a = x"; auto)
      qed

      then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) 
                                then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None)
                   = (λ x' . if x' = x 
                                then Some (insert z zs) 
                                else (λ x . if (∃ z . (x,z) ∈ set xs) 
                                              then Some {z . (x,z) ∈ set xs} else None) x')"
        by auto


      show ?thesis using m1 m2 snoc
        using ‹xz = (x, z)› by presburger
    qed
  qed

  then show ?thesis
    unfolding set_as_map_def by simp
qed


abbreviation "member_option x ms ≡ (case ms of None ⇒ False | Some xs ⇒ x ∈ xs)"
notation member_option ("(_∈⇩o_)" [1000] 1000)

abbreviation(input) "lookup_with_default f d ≡ (λ x . case f x of None ⇒ d | Some xs ⇒ xs)"
abbreviation(input) "m2f f ≡ lookup_with_default f {}" 

abbreviation(input) "lookup_with_default_by f g d ≡ (λ x . case f x of None ⇒ g d | Some xs ⇒ g xs)"
abbreviation(input) "m2f_by g f ≡ lookup_with_default_by f g {}" 

lemma m2f_by_from_m2f :
  "(m2f_by g f xs) = g (m2f f xs)"
  by (simp add: option.case_eq_if) 


lemma set_as_map_containment :
  assumes "(x,y) ∈ zs"
  shows "y ∈ (m2f (set_as_map zs)) x"
  using assms unfolding set_as_map_def
  by auto 

lemma set_as_map_elem :
  assumes "y ∈ m2f (set_as_map xs) x" 
shows "(x,y) ∈ xs" 
using assms unfolding set_as_map_def
proof -
  assume a1: "y ∈ (case if ∃z. (x, z) ∈ xs then Some {z. (x, z) ∈ xs} else None of None ⇒ {} | Some xs ⇒ xs)"
  then have "∃a. (x, a) ∈ xs"
    using all_not_in_conv by fastforce
  then show ?thesis
    using a1 by simp
qed 


subsection ‹Utility Lemmata for existing functions on lists›

subsubsection ‹Utility Lemmata for @{text "find"}›

lemma find_result_props : 
  assumes "find P xs = Some x" 
  shows "x ∈ set xs" and "P x"
proof -
  show "x ∈ set xs" using assms by (metis find_Some_iff nth_mem)
  show "P x" using assms by (metis find_Some_iff)
qed

lemma find_set : 
  assumes "find P xs = Some x"
  shows "x ∈ set xs"
using assms proof(induction xs)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)
  then show ?case
    by (metis find.simps(2) list.set_intros(1) list.set_intros(2) option.inject) 
qed

lemma find_condition : 
  assumes "find P xs = Some x"
  shows "P x"
using assms proof(induction xs)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)
  then show ?case
    by (metis find.simps(2) option.inject)     
qed

lemma find_from : 
  assumes "∃ x ∈ set xs . P x"
  shows "find P xs ≠ None"
  by (metis assms find_None_iff)


lemma find_sort_containment :
  assumes "find P (sort xs) = Some x"
shows "x ∈ set xs"
  using assms find_set by force


lemma find_sort_index :
  assumes "find P xs = Some x"
  shows "∃ i < length xs . xs ! i = x ∧ (∀ j < i . ¬ P (xs ! j))"
using assms proof (induction xs arbitrary: x)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)
  show ?case proof (cases "P a")
    case True
    then show ?thesis 
      using Cons.prems unfolding find.simps by auto
  next
    case False
    then have "find P (a#xs) = find P xs"
      unfolding find.simps by auto
    then have "find P xs = Some x"
      using Cons.prems by auto
    then show ?thesis 
      using Cons.IH False
      by (metis Cons.prems find_Some_iff)  
  qed
qed


lemma find_sort_least :
  assumes "find P (sort xs) = Some x"
  shows "∀ x' ∈ set xs . x ≤ x' ∨ ¬ P x'"
  and   "x = (LEAST x' ∈ set xs . P x')"
proof -
  obtain i where "i < length (sort xs)" 
           and   "(sort xs) ! i = x" 
           and   "(∀ j < i . ¬ P ((sort xs) ! j))"
    using find_sort_index[OF assms] by blast
  
  have "⋀ j . j > i ⟹ j < length xs ⟹ (sort xs) ! i ≤ (sort xs) ! j"
    by (simp add: sorted_nth_mono)
  then have "⋀ j . j < length xs ⟹ (sort xs) ! i ≤ (sort xs) ! j ∨ ¬ P ((sort xs) ! j)"
    using ‹(∀ j < i . ¬ P ((sort xs) ! j))›
    by (metis not_less_iff_gr_or_eq order_refl) 
  then show "∀ x' ∈ set xs . x ≤ x' ∨ ¬ P x'"
    by (metis ‹sort xs ! i = x› in_set_conv_nth length_sort set_sort)
  then show "x = (LEAST x' ∈ set xs . P x')"
    using find_set[OF assms] find_condition[OF assms]
    by (metis (mono_tags, lifting) Least_equality set_sort) 
qed



subsubsection ‹Utility Lemmata for @{text "filter"}›

lemma filter_take_length :
  "length (filter P (take i xs)) ≤ length (filter P xs)"
  by (metis append_take_drop_id filter_append le0 le_add_same_cancel1 length_append)


lemma filter_double :
  assumes "x ∈ set (filter P1 xs)"
  and     "P2 x"
shows "x ∈ set (filter P2 (filter P1 xs))"
  by (metis (no_types) assms(1) assms(2) filter_set member_filter)

lemma filter_list_set :
  assumes "x ∈ set xs"
  and     "P x"
shows "x ∈ set (filter P xs)"
  by (simp add: assms(1) assms(2))

lemma filter_list_set_not_contained :
  assumes "x ∈ set xs"
  and     "¬ P x"
shows "x ∉ set (filter P xs)"
  by (simp add: assms(1) assms(2))

lemma filter_map_elem : "t ∈ set (map g (filter f xs)) ⟹ ∃ x ∈ set xs . f x ∧ t = g x" 
  by auto



subsubsection ‹Utility Lemmata for @{text "concat"}›

lemma concat_map_elem :
  assumes "y ∈ set (concat (map f xs))"
  obtains x where "x ∈ set xs"
              and "y ∈ set (f x)"
using assms proof (induction xs)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)
  then show ?case 
  proof (cases "y ∈ set (f a)")
    case True
    then show ?thesis 
      using Cons.prems(1) by auto
  next
    case False
    then have "y ∈ set (concat (map f xs))"
      using Cons by auto
    have "∃ x . x ∈ set xs ∧ y ∈ set (f x)"  
    proof (rule ccontr)
      assume "¬(∃x. x ∈ set xs ∧ y ∈ set (f x))"
      then have "¬(y ∈ set (concat (map f xs)))"
        by auto
      then show False 
        using ‹y ∈ set (concat (map f xs))› by auto
    qed
    then show ?thesis
      using Cons.prems(1) by auto     
  qed
qed

lemma set_concat_map_sublist :
  assumes "x ∈ set (concat (map f xs))"
  and     "set xs ⊆ set xs'"
shows "x ∈ set (concat (map f xs'))"
using assms by (induction xs) (auto)

lemma set_concat_map_elem :
  assumes "x ∈ set (concat (map f xs))"
  shows "∃ x' ∈ set xs . x ∈ set (f x')"
using assms by auto

lemma concat_replicate_length : "length (concat (replicate n xs)) = n * (length xs)"
  by (induction n; simp)




subsection ‹Enumerating Lists›

fun lists_of_length :: "'a list ⇒ nat ⇒ 'a list list" where
  "lists_of_length T 0 = [[]]" |
  "lists_of_length T (Suc n) = concat (map (λ xs . map (λ x . x#xs) T ) (lists_of_length T n))" 

lemma lists_of_length_containment :
  assumes "set xs ⊆ set T"
  and     "length xs = n"
shows "xs ∈ set (lists_of_length T n)"
using assms proof (induction xs arbitrary: n)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)
  then obtain k where "n = Suc k" 
    by auto
  then have "xs ∈ set (lists_of_length T k)" 
    using Cons by auto
  moreover have "a ∈ set T" 
    using Cons by auto
  ultimately show ?case 
    using ‹n = Suc k› by auto
qed


lemma lists_of_length_length :
  assumes "xs ∈ set (lists_of_length T n)"
  shows "length xs = n"
proof -
  have "∀ xs ∈ set (lists_of_length T n) . length xs = n"
    by (induction n; simp)
  then show ?thesis using assms by blast
qed

lemma lists_of_length_elems :
  assumes "xs ∈ set (lists_of_length T n)"
  shows "set xs ⊆ set T"
proof -
  have "∀ xs ∈ set (lists_of_length T n) . set xs ⊆ set T"
    by (induction n; simp)
  then show ?thesis using assms by blast
qed
  
lemma lists_of_length_list_set : 
  "set (lists_of_length xs k) = {xs' . length xs' = k ∧ set xs' ⊆ set xs}"
  using lists_of_length_containment[of _ xs k] 
        lists_of_length_length[of _ xs k] 
        lists_of_length_elems[of _ xs k] 
  by blast
    


subsubsection ‹Enumerating List Subsets›

fun generate_selector_lists :: "nat ⇒ bool list list" where
  "generate_selector_lists k = lists_of_length [False,True] k"
  

lemma generate_selector_lists_set : 
  "set (generate_selector_lists k) = {(bs :: bool list) . length bs = k}"
  using lists_of_length_list_set by auto 

lemma selector_list_index_set:
  assumes "length ms = length bs"
  shows "set (map fst (filter snd (zip ms bs))) = { ms ! i | i . i < length bs ∧ bs ! i}"
using assms proof (induction bs arbitrary: ms rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc b bs)
  let ?ms = "butlast ms"
  let ?m = "last ms"

  have "length ?ms = length bs" using snoc.prems by auto

  have "map fst (filter snd (zip ms (bs @ [b]))) 
          = (map fst (filter snd (zip ?ms bs))) @ (map fst (filter snd (zip [?m] [b])))"
    by (metis ‹length (butlast ms) = length bs› append_eq_conv_conj filter_append length_0_conv 
        map_append snoc.prems snoc_eq_iff_butlast zip_append2)
  then have *: "set (map fst (filter snd (zip ms (bs @ [b])))) 
              = set (map fst (filter snd (zip ?ms bs))) ∪ set (map fst (filter snd (zip [?m] [b])))"
    by simp
    

  have "{ms ! i |i. i < length (bs @ [b]) ∧ (bs @ [b]) ! i} 
        = {ms ! i |i. i ≤ (length bs) ∧ (bs @ [b]) ! i}"
    by auto
  moreover have "{ms ! i |i. i ≤ (length bs) ∧ (bs @ [b]) ! i} 
                  = {ms ! i |i. i < length bs ∧ (bs @ [b]) ! i} 
                    ∪ {ms ! i |i. i = length bs ∧ (bs @ [b]) ! i}"
    by fastforce
  moreover have "{ms ! i |i. i < length bs ∧ (bs @ [b]) ! i} = {?ms ! i |i. i < length bs ∧ bs ! i}"
    using ‹length ?ms = length bs› by (metis butlast_snoc nth_butlast)  
  ultimately have **: "{ms ! i |i. i < length (bs @ [b]) ∧ (bs @ [b]) ! i} 
                      = {?ms ! i |i. i < length bs ∧ bs ! i} 
                        ∪ {ms ! i |i. i = length bs ∧ (bs @ [b]) ! i}"
    by simp
  

  have "set (map fst (filter snd (zip [?m] [b]))) = {ms ! i |i. i = length bs ∧ (bs @ [b]) ! i}"
  proof (cases b)
    case True
    then have "set (map fst (filter snd (zip [?m] [b]))) = {?m}" by fastforce
    moreover have "{ms ! i |i. i = length bs ∧ (bs @ [b]) ! i} = {?m}" 
    proof -
      have "(bs @ [b]) ! length bs"
        by (simp add: True) 
      moreover have "ms ! length bs = ?m"
        by (metis last_conv_nth length_0_conv length_butlast snoc.prems snoc_eq_iff_butlast) 
      ultimately show ?thesis by fastforce
    qed
    ultimately show ?thesis by auto
  next
    case False
    then show ?thesis by auto
  qed

  then have "set (map fst (filter snd (zip (butlast ms) bs))) 
                ∪ set (map fst (filter snd (zip [?m] [b])))
             = {butlast ms ! i |i. i < length bs ∧ bs ! i} 
                ∪ {ms ! i |i. i = length bs ∧ (bs @ [b]) ! i}"
    using snoc.IH[OF ‹length ?ms = length bs›] by blast

  then show ?case using * **
    by simp 
qed

lemma selector_list_ex :
  assumes "set xs ⊆ set ms"
  shows "∃ bs . length bs = length ms ∧ set xs = set (map fst (filter snd (zip ms bs)))"
using assms proof (induction xs rule: rev_induct)
  case Nil
  let ?bs = "replicate (length ms) False"
  have "set [] = set (map fst (filter snd (zip ms ?bs)))"
    by (metis filter_False in_set_zip length_replicate list.simps(8) nth_replicate)
  moreover have "length ?bs = length ms" by auto
  ultimately show ?case by blast
next
  case (snoc a xs)
  then have "set xs ⊆ set ms" and "a ∈ set ms" by auto
  then obtain bs where "length bs = length ms" and "set xs = set (map fst (filter snd (zip ms bs)))" 
    using snoc.IH by auto

  from ‹a ∈ set ms› obtain i where "i < length ms" and "ms ! i = a"
    by (meson in_set_conv_nth) 

  let ?bs = "list_update bs i True"
  have "length ms = length ?bs" using ‹length bs = length ms› by auto
  have "length ?bs = length bs" by auto

  have "set (map fst (filter snd (zip ms ?bs))) = {ms ! i |i. i < length ?bs ∧ ?bs ! i}"
    using selector_list_index_set[OF ‹length ms = length ?bs›] by assumption

  have "⋀ j . j < length ?bs ⟹ j ≠ i ⟹ ?bs ! j = bs ! j"
    by auto
  then have "{ms ! j |j. j < length bs ∧ j ≠ i ∧ bs ! j} 
              = {ms ! j |j. j < length ?bs ∧ j ≠ i ∧ ?bs ! j}"
    using ‹length ?bs = length bs› by fastforce
  
  
  
  have "{ms ! j |j. j < length ?bs ∧ j = i ∧ ?bs ! j} = {a}"
    using ‹length bs = length ms› ‹i < length ms› ‹ms ! i = a› by auto
  then have "{ms ! i |i. i < length ?bs ∧ ?bs ! i} 
              = insert a {ms ! j |j. j < length ?bs ∧ j ≠ i ∧ ?bs ! j}"
    by fastforce
  

  have "{ms ! j |j. j < length bs ∧ j = i ∧ bs ! j} ⊆ {ms ! j |j. j < length ?bs ∧ j = i ∧ ?bs ! j}"
    by (simp add: Collect_mono)
  then have "{ms ! j |j. j < length bs ∧ j = i ∧ bs ! j} ⊆ {a}"
    using ‹{ms ! j |j. j < length ?bs ∧ j = i ∧ ?bs ! j} = {a}› 
    by auto
  moreover have "{ms ! j |j. j < length bs ∧ bs ! j} 
                = {ms ! j |j. j < length bs ∧ j = i ∧ bs ! j} 
                    ∪ {ms ! j |j. j < length bs ∧ j ≠ i ∧ bs ! j}"
    by fastforce

  ultimately have "{ms ! i |i. i < length ?bs ∧ ?bs ! i} 
                    = insert a {ms ! i |i. i < length bs ∧ bs ! i}"
    using ‹{ms ! j |j. j < length bs ∧ j ≠ i ∧ bs ! j} 
            = {ms ! j |j. j < length ?bs ∧ j ≠ i ∧ ?bs ! j}›
    using ‹{ms ! ia |ia. ia < length (bs[i := True]) 
                      ∧ bs[i := True] ! ia} 
                          = insert a {ms ! j |j. j < length (bs[i := True]) 
                              ∧ j ≠ i ∧ bs[i := True] ! j}› 
    by auto 

  moreover have "set (map fst (filter snd (zip ms bs))) = {ms ! i |i. i < length bs ∧ bs ! i}"
    using selector_list_index_set[of ms bs] ‹length bs = length ms› by auto

  ultimately have "set (a#xs) = set (map fst (filter snd (zip ms ?bs)))"
    using ‹set (map fst (filter snd (zip ms ?bs))) = {ms ! i |i. i < length ?bs ∧ ?bs ! i}› 
          ‹set xs = set (map fst (filter snd (zip ms bs)))› 
    by auto
  then show ?case
    using ‹length ms = length ?bs›
    by (metis Un_commute insert_def list.set(1) list.simps(15) set_append singleton_conv) 
qed


subsubsection ‹Enumerating Choices from Lists of Lists›


fun generate_choices :: "('a × ('b list)) list ⇒ ('a × 'b option) list list" where
  "generate_choices [] = [[]]" |
  "generate_choices (xys#xyss) = 
    concat (map (λ xy' . map (λ xys' . xy' # xys') (generate_choices xyss)) 
                ((fst xys, None) # (map (λ y . (fst xys, Some y)) (snd xys))))"


lemma concat_map_hd_tl_elem: 
  assumes "hd cs ∈ set P1"
  and     "tl cs ∈ set P2"
  and     "length cs > 0"
shows "cs ∈ set (concat (map (λ xy' . map (λ xys' . xy' # xys') P2) P1))"
proof -
  have "hd cs # tl cs = cs" using assms(3) by auto
  moreover have "hd cs # tl cs ∈ set (concat (map (λ xy' . map (λ xys' . xy' # xys') P2) P1))" 
    using assms(1,2) by auto
  ultimately show ?thesis 
    by auto
qed


lemma generate_choices_hd_tl : 
  "cs ∈ set (generate_choices (xys#xyss)) 
    = (length cs = length (xys#xyss) 
      ∧ fst (hd cs) = fst xys 
      ∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)))) 
      ∧ (tl cs ∈ set (generate_choices xyss)))"
proof (induction xyss arbitrary: cs xys)
  case Nil
  have "(cs ∈ set (generate_choices [xys])) 
          = (cs ∈ set ([(fst xys, None)] # map (λy. [(fst xys, Some y)]) (snd xys)))" 
    unfolding generate_choices.simps by auto
  moreover have "(cs ∈ set ([(fst xys, None)] # map (λy. [(fst xys, Some y)]) (snd xys))) 
               ⟹ (length cs = length [xys] ∧
                   fst (hd cs) = fst xys ∧
                   (snd (hd cs) = None ∨ snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)) ∧
                   tl cs ∈ set (generate_choices []))"
    by auto
  moreover have "(length cs = length [xys] ∧
                   fst (hd cs) = fst xys ∧
                   (snd (hd cs) = None ∨ snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)) ∧
                   tl cs ∈ set (generate_choices [])) 
                ⟹ (cs ∈ set ([(fst xys, None)] # map (λy. [(fst xys, Some y)]) (snd xys)))"
    unfolding generate_choices.simps(1)
  proof -
    assume a1: "length cs = length [xys] 
                ∧ fst (hd cs) = fst xys 
                ∧ (snd (hd cs) = None ∨ snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)) 
                ∧ tl cs ∈ set [[]]"
    have f2: "∀ps. ps = [] ∨ ps = (hd ps::'a × 'b option) # tl ps"
      by (meson list.exhaust_sel)
    have f3: "cs ≠ []"
      using a1 by fastforce
    have "snd (hd cs) = None ⟶ (fst xys, None) = hd cs"
      using a1 by (metis prod.exhaust_sel)
    moreover
    { assume "hd cs # tl cs ≠ [(fst xys, Some (the (snd (hd cs))))]"
      then have "snd (hd cs) = None"
        using a1 by (metis (no_types) length_0_conv length_tl list.sel(3) 
                      option.collapse prod.exhaust_sel) }
    ultimately have "cs ∈ insert [(fst xys, None)] ((λb. [(fst xys, Some b)]) ` set (snd xys))"
      using f3 f2 a1 by fastforce
    then show ?thesis
      by simp
  qed 
  ultimately show ?case by blast
next
  case (Cons a xyss)

  have "length cs = length (xys#a#xyss) 
        ⟹ fst (hd cs) = fst xys 
        ⟹ (snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys))) 
        ⟹ (tl cs ∈ set (generate_choices (a#xyss))) 
        ⟹ cs ∈ set (generate_choices (xys#a#xyss))"
  proof -
    assume "length cs = length (xys#a#xyss)" 
       and "fst (hd cs) = fst xys" 
       and "(snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)))" 
       and "(tl cs ∈ set (generate_choices (a#xyss)))"
    then have "length cs > 0" by auto

    have "(hd cs) ∈ set ((fst xys, None) # (map (λ y . (fst xys, Some y)) (snd xys)))"
      using ‹fst (hd cs) = fst xys› 
            ‹(snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)))›
      by (metis (no_types, lifting) image_eqI list.set_intros(1) list.set_intros(2) 
            option.collapse prod.collapse set_map)  
    
    show "cs ∈ set (generate_choices ((xys#(a#xyss))))"
      using generate_choices.simps(2)[of xys "a#xyss"] 
            concat_map_hd_tl_elem[OF ‹(hd cs) ∈ set ((fst xys, None) # (map (λ y . (fst xys, Some y)) (snd xys)))› 
                                     ‹(tl cs ∈ set (generate_choices (a#xyss)))› 
                                     ‹length cs > 0›] 
      by auto
  qed

  moreover have "cs ∈ set (generate_choices (xys#a#xyss)) 
                ⟹ length cs = length (xys#a#xyss) 
                    ∧ fst (hd cs) = fst xys 
                    ∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None 
                    ∧ the (snd (hd cs)) ∈ set (snd xys)))) 
                    ∧ (tl cs ∈ set (generate_choices (a#xyss)))"
  proof -
    assume "cs ∈ set (generate_choices (xys#a#xyss))"
    then have p3: "tl cs ∈ set (generate_choices (a#xyss))"
      using generate_choices.simps(2)[of xys "a#xyss"] by fastforce
    then have "length (tl cs) = length (a # xyss)" using Cons.IH[of "tl cs" "a"] by simp
    then have p1: "length cs = length (xys#a#xyss)" by auto

    have p2 : "fst (hd cs) = fst xys ∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None 
                                ∧ the (snd (hd cs)) ∈ set (snd xys))))"
      using ‹cs ∈ set (generate_choices (xys#a#xyss))› generate_choices.simps(2)[of xys "a#xyss"] 
      by fastforce
    
    show ?thesis using p1 p2 p3 by simp
  qed

  ultimately show ?case by blast
qed 

lemma list_append_idx_prop : 
  "(∀ i . (i < length xs ⟶ P (xs ! i))) 
    = (∀ j . ((j < length (ys@xs) ∧ j ≥ length ys) ⟶ P ((ys@xs) ! j)))"
proof -
  have "⋀ j . ∀i<length xs. P (xs ! i) ⟹ j < length (ys @ xs) 
              ⟹ length ys ≤ j ⟶ P ((ys @ xs) ! j)"
    by (simp add: nth_append)
  moreover have "⋀ i . (∀ j . ((j < length (ys@xs) ∧ j ≥ length ys) ⟶ P ((ys@xs) ! j))) 
                  ⟹ i < length xs ⟹ P (xs ! i)"
  proof -
    fix i assume "(∀ j . ((j < length (ys@xs) ∧ j ≥ length ys) ⟶ P ((ys@xs) ! j)))" 
             and "i < length xs"
    then have "P ((ys@xs) ! (length ys + i))"
      by (metis add_strict_left_mono le_add1 length_append)
    moreover have "P (xs ! i) = P ((ys@xs) ! (length ys + i))"
      by simp
    ultimately show "P (xs ! i)" by blast
  qed
  ultimately show ?thesis by blast
qed

lemma list_append_idx_prop2 : 
  assumes "length xs' = length xs"
      and "length ys' = length ys"
  shows "(∀ i . (i < length xs ⟶ P (xs ! i) (xs' ! i))) 
          = (∀ j . ((j < length (ys@xs) ∧ j ≥ length ys) ⟶ P ((ys@xs) ! j) ((ys'@xs') ! j)))"
proof -
  have "∀i<length xs. P (xs ! i) (xs' ! i) ⟹
    ∀j. j < length (ys @ xs) ∧ length ys ≤ j ⟶ P ((ys @ xs) ! j) ((ys' @ xs') ! j)"
    using assms
  proof -
    assume a1: "∀i<length xs. P (xs ! i) (xs' ! i)"
    { fix nn :: nat
      have ff1: "∀n na. (na::nat) + n - n = na"
        by simp
      have ff2: "∀n na. (na::nat) ≤ n + na"
        by auto
      then have ff3: "∀as n. (ys' @ as) ! n = as ! (n - length ys) ∨ ¬ length ys ≤ n"
        using ff1 by (metis (no_types) add.commute assms(2) eq_diff_iff nth_append_length_plus)
      have ff4: "∀n bs bsa. ((bsa @ bs) ! n::'b) = bs ! (n - length bsa) ∨ ¬ length bsa ≤ n"
        using ff2 ff1 by (metis (no_types) add.commute eq_diff_iff nth_append_length_plus)
      have "∀n na nb. ((n::nat) + nb ≤ na ∨ ¬ n ≤ na - nb) ∨ ¬ nb ≤ na"
        using ff2 ff1 by (metis le_diff_iff)
      then have "(¬ nn < length (ys @ xs) ∨ ¬ length ys ≤ nn) 
                  ∨ P ((ys @ xs) ! nn) ((ys' @ xs') ! nn)"
        using ff4 ff3 a1 by (metis add.commute length_append not_le) }
    then show ?thesis
      by blast
  qed

  moreover have "(∀j. j < length (ys @ xs) ∧ length ys ≤ j ⟶ P ((ys @ xs) ! j) ((ys' @ xs') ! j)) 
                  ⟹ ∀i<length xs. P (xs ! i) (xs' ! i)"
    using assms
    by (metis le_add1 length_append nat_add_left_cancel_less nth_append_length_plus) 

  ultimately show ?thesis by blast
qed

lemma generate_choices_idx : 
  "cs ∈ set (generate_choices xyss) 
    = (length cs = length xyss 
        ∧ (∀ i < length cs . (fst (cs ! i)) = (fst (xyss ! i)) 
        ∧ ((snd (cs ! i)) = None 
            ∨ ((snd (cs ! i)) ≠ None ∧ the (snd (cs ! i)) ∈ set (snd (xyss ! i))))))"
proof (induction xyss arbitrary: cs)
  case Nil
  then show ?case by auto
next
  case (Cons xys xyss)

  have "cs ∈ set (generate_choices (xys#xyss)) 
        = (length cs = length (xys#xyss) 
            ∧ fst (hd cs) = fst xys 
            ∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)))) 
            ∧ (tl cs ∈ set (generate_choices xyss)))"
    using generate_choices_hd_tl by metis

  then have "cs ∈ set (generate_choices (xys#xyss)) 
    = (length cs = length (xys#xyss) 
      ∧ fst (hd cs) = fst xys 
      ∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)))) 
      ∧ (length (tl cs) = length xyss ∧
        (∀i<length (tl cs).
          fst (tl cs ! i) = fst (xyss ! i) ∧
          (snd (tl cs ! i) = None 
            ∨ snd (tl cs ! i) ≠ None ∧ the (snd (tl cs ! i)) ∈ set (snd (xyss ! i))))))"
    using Cons.IH[of "tl cs"] by blast
  then have *: "cs ∈ set (generate_choices (xys#xyss)) 
    = (length cs = length (xys#xyss) 
      ∧ fst (hd cs) = fst xys 
      ∧ ((snd (hd cs) = None ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys)))) 
      ∧ (∀i<length (tl cs).
          fst (tl cs ! i) = fst (xyss ! i) ∧
          (snd (tl cs ! i) = None 
            ∨ snd (tl cs ! i) ≠ None ∧ the (snd (tl cs ! i)) ∈ set (snd (xyss ! i)))))"
    by auto


  have "cs ∈ set (generate_choices (xys#xyss)) ⟹ (length cs = length (xys # xyss) ∧
                    (∀i<length cs.
                        fst (cs ! i) = fst ((xys # xyss) ! i) ∧
                        (snd (cs ! i) = None ∨
                        snd (cs ! i) ≠ None ∧ the (snd (cs ! i)) ∈ set (snd ((xys # xyss) ! i)))))"
  proof -
    assume "cs ∈ set (generate_choices (xys#xyss))"
    then have p1: "length cs = length (xys#xyss)"
          and p2: "fst (hd cs) = fst xys "
          and p3: "((snd (hd cs) = None 
                    ∨ (snd (hd cs) ≠ None ∧ the (snd (hd cs)) ∈ set (snd xys))))"
          and p4: "(∀i<length (tl cs).
                  fst (tl cs ! i) = fst (xyss ! i) ∧
                  (snd (tl cs ! i) = None 
                    ∨ snd (tl cs ! i) ≠ None ∧ the (snd (tl cs ! i)) ∈ set (snd (xyss ! i))))"
      using * by blast+
    then have "length xyss = length (tl cs)" and "length (xys # xyss) = length ([hd cs] @ tl cs)"
      by auto
    
    have "[hd cs]@(tl cs) = cs"
      by (metis (no_types) p1 append.left_neutral append_Cons length_greater_0_conv 
            list.collapse list.simps(3)) 
    then have p4b: "(∀i<length cs. i > 0 ⟶
                    (fst (cs ! i) = fst ((xys#xyss) ! i) ∧
                      (snd (cs ! i) = None 
                        ∨ snd (cs ! i) ≠ None ∧ the (snd (cs ! i)) ∈ set (snd ((xys#xyss) ! i)))))"
      using p4 list_append_idx_prop2[of xyss "tl cs" "xys#xyss" "[hd cs]@(tl cs)" 
                                        "λ x y . fst x = fst y 
                                                  ∧ (snd x = None 
                                                      ∨ snd x ≠ None ∧ the (snd x) ∈ set (snd y))", 
                                     OF ‹length xyss = length (tl cs)› 
                                        ‹length (xys # xyss) = length ([hd cs] @ tl cs)›]
      by (metis (no_types, lifting) One_nat_def Suc_pred 
            ‹length (xys # xyss) = length ([hd cs] @ tl cs)› ‹length xyss = length (tl cs)› 
            length_Cons list.size(3) not_less_eq nth_Cons_pos nth_append) 

    have p4a :"(fst (cs ! 0) = fst ((xys#xyss) ! 0) ∧ (snd (cs ! 0) = None 
                ∨ snd (cs ! 0) ≠ None ∧ the (snd (cs ! 0)) ∈ set (snd ((xys#xyss) ! 0))))"
      using p1 p2 p3 by (metis hd_conv_nth length_greater_0_conv list.simps(3) nth_Cons_0)

    show ?thesis using p1 p4a p4b by fastforce
  qed


  moreover have "(length cs = length (xys # xyss) ∧
                    (∀i<length cs.
                        fst (cs ! i) = fst ((xys # xyss) ! i) ∧
                        (snd (cs ! i) = None ∨
                        snd (cs ! i) ≠ None ∧ the (snd (cs ! i)) ∈ set (snd ((xys # xyss) ! i))))) 
                  ⟹ cs ∈ set (generate_choices (xys#xyss))"
    using * 
    by (metis (no_types, lifting) Nitpick.size_list_simp(2) Suc_mono hd_conv_nth 
        length_greater_0_conv length_tl list.sel(3) list.simps(3) nth_Cons_0 nth_tl) 

  ultimately show ?case by blast
qed


subsection ‹Finding the Index of the First Element of a List Satisfying a Property›


fun find_index :: "('a ⇒ bool) ⇒ 'a list ⇒ nat option" where
  "find_index f []  = None" |
  "find_index f (x#xs) = (if f x 
    then Some 0 
    else (case find_index f xs of Some k ⇒ Some (Suc k) | None ⇒ None))" 

lemma find_index_index :
  assumes "find_index f xs = Some k"
  shows "k < length xs" and "f (xs ! k)" and "⋀ j . j < k ⟹ ¬ f (xs ! j)"
proof -
  have "(k < length xs) ∧ (f (xs ! k)) ∧ (∀ j < k . ¬ (f (xs ! j)))"
    using assms proof (induction xs arbitrary: k)
    case Nil
    then show ?case by auto
  next
    case (Cons x xs)
    
    show ?case proof (cases "f x")
      case True
      then show ?thesis using Cons.prems by auto
    next
      case False
      then have "find_index f (x#xs) 
                  = (case find_index f xs of Some k ⇒ Some (Suc k) | None ⇒ None)"
        by auto
      then have "(case find_index f xs of Some k ⇒ Some (Suc k) | None ⇒ None) = Some k"
        using Cons.prems by auto
      then obtain k' where "find_index f xs = Some k'" and "k = Suc k'"
        by (metis option.case_eq_if option.collapse option.distinct(1) option.sel)
        
      have "k < length (x # xs) ∧ f ((x # xs) ! k)" 
        using Cons.IH[OF ‹find_index f xs = Some k'›] ‹k = Suc k'› 
        by auto
      moreover have "(∀j<k. ¬ f ((x # xs) ! j))"
        using Cons.IH[OF ‹find_index f xs = Some k'›] ‹k = Suc k'› False less_Suc_eq_0_disj 
        by auto 
      ultimately show ?thesis by presburger
    qed
  qed
  then show "k < length xs" and "f (xs ! k)" and "⋀ j . j < k ⟹ ¬ f (xs ! j)" by simp+
qed

lemma find_index_exhaustive : 
  assumes "∃ x ∈ set xs . f x"
  shows "find_index f xs ≠ None"
  using assms proof (induction xs)
case Nil
  then show ?case by auto
next
  case (Cons x xs)
  then show ?case by (cases "f x"; auto)
qed



subsection ‹List Distinctness from Sorting›

lemma non_distinct_repetition_indices :
  assumes "¬ distinct xs"
  shows "∃ i j . i < j ∧ j < length xs ∧ xs ! i = xs ! j"
  by (metis assms distinct_conv_nth le_neq_implies_less not_le)

lemma non_distinct_repetition_indices_rev :
  assumes "i < j" and "j < length xs" and "xs ! i = xs ! j"
  shows "¬ distinct xs"
  using assms nth_eq_iff_index_eq by fastforce 

lemma ordered_list_distinct :
  fixes xs :: "('a::preorder) list"
  assumes "⋀ i . Suc i < length xs ⟹ (xs ! i) < (xs ! (Suc i))"
  shows "distinct xs"
proof -
  have "⋀ i j . i < j ⟹ j < length xs ⟹ (xs ! i) < (xs ! j)"
  proof -
    fix i j assume "i < j" and "j < length xs"
    then show "xs ! i < xs ! j"
      using assms proof (induction xs arbitrary: i j rule: rev_induct)
      case Nil
      then show ?case by auto
    next
      case (snoc a xs)
      show ?case proof (cases "j < length xs")
        case True
        show ?thesis using snoc.IH[OF snoc.prems(1) True] snoc.prems(3)
        proof -
          have f1: "i < length xs"
            using True less_trans snoc.prems(1) by blast
          have f2: "∀is isa n. if n < length is then (is @ isa) ! n 
                    = (is ! n::integer) else (is @ isa) ! n = isa ! (n - length is)"
            by (meson nth_append)
          then have f3: "(xs @ [a]) ! i = xs ! i"
            using f1
            by (simp add: nth_append)
          have "xs ! i < xs ! j"
            using f2
            by (metis Suc_lessD ‹(⋀i. Suc i < length xs ⟹ xs ! i < xs ! Suc i) ⟹ xs ! i < xs ! j› 
                  butlast_snoc length_append_singleton less_SucI nth_butlast snoc.prems(3)) 
          then show ?thesis
            using f3 f2 True
            by (simp add: nth_append) 
        qed
      next
        case False
        then have "(xs @ [a]) ! j = a"
          using snoc.prems(2)
          by (metis length_append_singleton less_SucE nth_append_length)  
        
        consider "j = 1" | "j > 1"
          using ‹i < j›
          by linarith 
        then show ?thesis proof cases
          case 1
          then have "i = 0" and "j = Suc i" using ‹i < j› by linarith+ 
          then show ?thesis 
            using snoc.prems(3)
            using snoc.prems(2) by blast 
        next
          case 2
          then consider "i < j - 1" | "i = j - 1" using ‹i < j› by linarith+
          then show ?thesis proof cases
            case 1
            
            have "(⋀i. Suc i < length xs ⟹ xs ! i < xs ! Suc i) ⟹ xs ! i < xs ! (j - 1)"
              using snoc.IH[OF 1] snoc.prems(2) 2 by simp 
            then have le1: "(xs @ [a]) ! i < (xs @ [a]) ! (j -1)"
              using snoc.prems(2)
              by (metis "2" False One_nat_def Suc_diff_Suc Suc_lessD diff_zero snoc.prems(3)
                    length_append_singleton less_SucE not_less_eq nth_append snoc.prems(1))
            moreover have le2: "(xs @ [a]) ! (j -1) < (xs @ [a]) ! j"
              using snoc.prems(2,3) 2 less_trans
              by (metis (full_types) One_nat_def Suc_diff_Suc diff_zero less_numeral_extra(1))  
            ultimately show ?thesis 
              using less_trans by blast
          next
            case 2
            then have "j = Suc i" using ‹1 < j› by linarith
            then show ?thesis 
              using snoc.prems(3)
              using snoc.prems(2) by blast
          qed
        qed
      qed
    qed 
  qed

  then show ?thesis
    by (metis less_asym non_distinct_repetition_indices)
qed



lemma ordered_list_distinct_rev :
  fixes xs :: "('a::preorder) list"
  assumes "⋀ i . Suc i < length xs ⟹ (xs ! i) > (xs ! (Suc i))"
  shows "distinct xs"
proof -
  have "⋀ i . Suc i < length (rev xs) ⟹ ((rev xs) ! i) < ((rev xs) ! (Suc i))"
    using assms
  proof -
    fix i :: nat
    assume a1: "Suc i < length (rev xs)"
    obtain nn :: "nat ⇒ nat ⇒ nat" where
      "∀x0 x1. (∃v2. x1 = Suc v2 ∧ v2 < x0) = (x1 = Suc (nn x0 x1) ∧ nn x0 x1 < x0)"
      by moura
    then have f2: "∀n na. (¬ n < Suc na ∨ n = 0 ∨ n = Suc (nn na n) ∧ nn na n < na) 
                    ∧ (n < Suc na ∨ n ≠ 0 ∧ (∀nb. n ≠ Suc nb ∨ ¬ nb < na))"
      by (meson less_Suc_eq_0_disj)
    have f3: "Suc (length xs - Suc (Suc i)) = length (rev xs) - Suc i"
      using a1 by (simp add: Suc_diff_Suc)
    have "i < length (rev xs)"
      using a1 by (meson Suc_lessD)
    then have "i < length xs"
      by simp
    then show "rev xs ! i < rev xs ! Suc i"
      using f3 f2 a1 by (metis (no_types) assms diff_less length_rev not_less_iff_gr_or_eq rev_nth)
  qed 
  then have "distinct (rev xs)" 
    using ordered_list_distinct[of "rev xs"] by blast
  then show ?thesis by auto
qed



subsection ‹Calculating Prefixes and Suffixes›

fun suffixes :: "'a list ⇒ 'a list list" where
  "suffixes [] = [[]]" |
  "suffixes (x#xs) = (suffixes xs) @ [x#xs]"

lemma suffixes_set : 
  "set (suffixes xs) = {zs . ∃ ys . ys@zs = xs}"
proof (induction xs)
  case Nil
  then show ?case by auto
next
  case (Cons x xs)
  then have *: "set (suffixes (x#xs)) = {zs . ∃ ys . ys@zs = xs} ∪ {x#xs}"
    by auto
  
  have "{zs . ∃ ys . ys@zs = xs} = {zs . ∃ ys . x#ys@zs = x#xs}"
    by force
  then have "{zs . ∃ ys . ys@zs = xs} = {zs . ∃ ys . ys@zs = x#xs ∧ ys ≠ []}"
    by (metis Cons_eq_append_conv list.distinct(1))
  moreover have "{x#xs} = {zs . ∃ ys . ys@zs = x#xs ∧ ys = []}"
    by force
    
  ultimately show ?case using * by force
qed





lemma prefixes_set : "set (prefixes xs) = {xs' . ∃ xs'' . xs'@xs'' = xs}"
proof (induction xs)
  case Nil
  then show ?case by auto
next
  case (Cons x xs)
  moreover have "prefixes (x#xs) = [] # map ((#) x) (prefixes xs)"
    by auto
  ultimately have *: "set (prefixes (x#xs)) = insert [] (((#) x) ` {xs'. ∃xs''. xs' @ xs'' = xs})"
    by auto
  also have "… = {xs' . ∃ xs'' . xs'@xs'' = (x#xs)}" 
  proof 
    show "insert [] ((#) x ` {xs'. ∃xs''. xs' @ xs'' = xs}) ⊆ {xs'. ∃xs''. xs' @ xs'' = x # xs}" 
      by auto
    show "{xs'. ∃xs''. xs' @ xs'' = x # xs} ⊆ insert [] ((#) x ` {xs'. ∃xs''. xs' @ xs'' = xs})"
    proof 
      fix y assume "y ∈ {xs'. ∃xs''. xs' @ xs'' = x # xs}"
      then obtain y' where "y@y' = x # xs"
        by blast
      then show "y ∈ insert [] ((#) x ` {xs'. ∃xs''. xs' @ xs'' = xs})"
        by (cases y; auto)
    qed
  qed
  finally show ?case .
qed



fun is_prefix :: "'a list ⇒ 'a list ⇒ bool" where
  "is_prefix [] _ = True" |
  "is_prefix (x#xs) [] = False" |
  "is_prefix (x#xs) (y#ys) = (x = y ∧ is_prefix xs ys)" 

lemma is_prefix_prefix : "is_prefix xs ys = (∃ xs' . ys = xs@xs')"
proof (induction xs arbitrary: ys)
  case Nil
  then show ?case by auto
next
  case (Cons x xs)
  show ?case proof (cases "is_prefix (x#xs) ys")
    case True
    then show ?thesis using Cons.IH
      by (metis append_Cons is_prefix.simps(2) is_prefix.simps(3) neq_Nil_conv) 
  next
    case False
    then show ?thesis
      using Cons.IH by auto 
  qed
qed


fun add_prefixes :: "'a list list ⇒ 'a list list" where
  "add_prefixes xs = concat (map prefixes xs)"


lemma add_prefixes_set : "set (add_prefixes xs) = {xs' . ∃ xs'' . xs'@xs'' ∈ set xs}"
proof -
  have "set (add_prefixes xs) = {xs' . ∃ x ∈ set xs . xs' ∈ set (prefixes x)}"
    unfolding add_prefixes.simps by auto
  also have "… = {xs' . ∃ xs'' . xs'@xs'' ∈ set xs}"
  proof (induction xs)
    case Nil
    then show ?case using prefixes_set by auto
  next
    case (Cons a xs)
    then show ?case 
    proof -
      have "⋀ xs' . xs' ∈ {xs'. ∃x∈set (a # xs). xs' ∈ set (prefixes x)} 
              ⟷ xs' ∈ {xs'. ∃xs''. xs' @ xs'' ∈ set (a # xs)}"
      proof -
        fix xs' 
        show "xs' ∈ {xs'. ∃x∈set (a # xs). xs' ∈ set (prefixes x)} 
              ⟷ xs' ∈ {xs'. ∃xs''. xs' @ xs'' ∈ set (a # xs)}"
          unfolding prefixes_set by force
      qed
      then show ?thesis by blast
    qed
  qed
  finally show ?thesis by blast
qed


lemma prefixes_set_ob :
  assumes "xs ∈ set (prefixes xss)"
  obtains xs' where "xss = xs@xs'"
  using assms unfolding prefixes_set
  by auto 

lemma prefixes_finite : "finite { x ∈ set (prefixes xs) . P x}"
  by (metis Collect_mem_eq List.finite_set finite_Collect_conjI)
  

lemma prefixes_set_Cons_insert: "set (prefixes (w' @ [xy])) = Set.insert (w'@[xy]) (set (prefixes (w')))"
  unfolding prefixes_set 
proof (induction w' arbitrary: xy rule: rev_induct)
  case Nil
  then show ?case 
    by (auto; simp add: append_eq_Cons_conv) 
  next
    case (snoc x xs)
    then show ?case 
      by (auto; metis (no_types, opaque_lifting) butlast.simps(2) butlast_append butlast_snoc)
  qed

lemma prefixes_set_subset:
  "set (prefixes xs) ⊆ set (prefixes (xs@ys))"
  unfolding prefixes_set by auto

lemma prefixes_prefix_subset :
  assumes "xs ∈ set (prefixes ys)"
  shows "set (prefixes xs) ⊆ set (prefixes ys)"
  using assms unfolding prefixes_set by auto

lemma prefixes_butlast_is_prefix :
  "butlast xs ∈ set (prefixes xs)"
  unfolding prefixes_set
  by (metis (mono_tags, lifting) append_butlast_last_id butlast.simps(1) mem_Collect_eq self_append_conv2) 

lemma prefixes_take_iff :
  "xs ∈ set (prefixes ys) ⟷ take (length xs) ys = xs"
proof 
  show "xs ∈ set (prefixes ys) ⟹ take (length xs) ys = xs"
    unfolding prefixes_set
    by (simp add: append_eq_conv_conj) 

  show "take (length xs) ys = xs ⟹ xs ∈ set (prefixes ys)"
    unfolding prefixes_set
    by (metis (mono_tags, lifting) append_take_drop_id mem_Collect_eq)
qed

lemma prefixes_set_Nil : "[] ∈ list.set (prefixes xs)"
  by (metis append.left_neutral list.set_intros(1) prefixes.simps(1) prefixes_set_subset subset_iff) 

lemma prefixes_prefixes :
  assumes "ys ∈ list.set (prefixes xs)"
          "zs ∈ list.set (prefixes xs)"
  shows "ys ∈ list.set (prefixes zs) ∨ zs ∈ list.set (prefixes ys)"
proof (rule ccontr)
  let ?ys = "take (length ys) zs"
  let ?zs = "take (length zs) ys"
  
  assume "¬ (ys ∈ list.set (prefixes zs) ∨ zs ∈ list.set (prefixes ys))"
  then have "?ys ≠ ys" and "?zs ≠ zs"
    using prefixes_take_iff by blast+
  moreover have "?ys = ys ∨ ?zs = zs"
    using assms
    by (metis linear min.commute prefixes_take_iff take_all_iff take_take)
  ultimately show False
    by simp
qed


subsubsection ‹Pairs of Distinct Prefixes›

fun prefix_pairs :: "'a list ⇒ ('a list × 'a list) list" 
  where "prefix_pairs [] = []" |
        "prefix_pairs xs = prefix_pairs (butlast xs) @ (map (λ ys. (ys,xs)) (butlast (prefixes xs)))"


lemma prefixes_butlast :
  "set (butlast (prefixes xs)) = {ys . ∃ zs . ys@zs = xs ∧ zs ≠ []}"
proof (induction "length xs" arbitrary: xs)
  case 0
  then show ?case by auto
next
  case (Suc k)

  then obtain x xs' where "xs = x#xs'" and "k = length xs' "
    by (metis length_Suc_conv)

  then have "prefixes xs = [] # map ((#) x) (prefixes xs')"
    by auto
  then have "butlast (prefixes xs) = [] # map ((#) x) (butlast (prefixes xs'))"
    by (simp add: map_butlast)
  then have "set (butlast (prefixes xs)) = insert [] (((#) x) ` {ys . ∃ zs . ys@zs = xs' ∧ zs ≠ []})"
    using Suc.hyps(1)[OF ‹k = length xs'›]
    by auto
  also have "… = {ys . ∃ zs . ys@zs = (x#xs') ∧ zs ≠ []}"
  proof 
    show "insert [] ((#) x ` {ys. ∃zs. ys @ zs = xs' ∧ zs ≠ []}) ⊆ {ys. ∃zs. ys @ zs = x # xs' ∧ zs ≠ []}" 
      by auto
    show "{ys. ∃zs. ys @ zs = x # xs' ∧ zs ≠ []} ⊆ insert [] ((#) x ` {ys. ∃zs. ys @ zs = xs' ∧ zs ≠ []})"
    proof 
      fix ys assume "ys ∈ {ys. ∃zs. ys @ zs = x # xs' ∧ zs ≠ []}"
      then show "ys ∈ insert [] ((#) x ` {ys. ∃zs. ys @ zs = xs' ∧ zs ≠ []})"
        by (cases ys; auto)
    qed
  qed
  finally show ?case 
    unfolding ‹xs = x#xs'› .
qed


lemma prefix_pairs_set :
  "set (prefix_pairs xs) = {(zs,ys) | zs ys . ∃ xs1 xs2 . zs@xs1 = ys ∧ ys@xs2 = xs ∧ xs1 ≠ []}"  
proof (induction xs rule: rev_induct)
  case Nil
  then show ?case by auto 
next
  case (snoc x xs)
  have "prefix_pairs (xs @ [x]) = prefix_pairs (butlast (xs @ [x])) @ (map (λ ys. (ys,(xs @ [x]))) (butlast (prefixes (xs @ [x]))))"
    by (cases "(xs @ [x])"; auto)
  then have *: "prefix_pairs (xs @ [x]) = prefix_pairs xs @ (map (λ ys. (ys,(xs @ [x]))) (butlast (prefixes (xs @ [x]))))"
    by auto

  have "set (prefix_pairs xs) = {(zs, ys) |zs ys. ∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 = xs ∧ xs1 ≠ []}"
    using snoc.IH by assumption
  then have "set (prefix_pairs xs) = {(zs, ys) |zs ys. ∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 @ [x] = xs@[x] ∧ xs1 ≠ []}"
    by auto
  also have "... = {(zs, ys) |zs ys. ∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 = xs @[x] ∧ xs1 ≠ [] ∧ xs2 ≠ []}" 
  proof -
    let ?P1 = "λ zs ys . (∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 @ [x] = xs@[x] ∧ xs1 ≠ [])"
    let ?P2 = "λ zs ys . (∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 = xs @[x] ∧ xs1 ≠ [] ∧ xs2 ≠ [])"

    have "⋀ ys zs . ?P2 zs ys ⟹ ?P1 zs ys"
      by (metis append_assoc butlast_append butlast_snoc)
    then have "⋀ ys zs . ?P1 ys zs = ?P2 ys zs"
      by blast
    then show ?thesis by force           
  qed
  finally have "set (prefix_pairs xs) = {(zs, ys) |zs ys. ∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 = xs @ [x] ∧ xs1 ≠ [] ∧ xs2 ≠ []}"
    by assumption

  moreover have "set (map (λ ys. (ys,(xs @ [x]))) (butlast (prefixes (xs @ [x])))) = {(zs, ys) |zs ys. ∃xs1 xs2. zs @ xs1 = ys ∧ ys @ xs2 = xs @ [x] ∧ xs1 ≠ [] ∧ xs2 = []}"
    using prefixes_butlast[of "xs@[x]"] by force

  ultimately show ?case using * by force
qed

lemma prefix_pairs_set_alt :
  "set (prefix_pairs xs) = {(xs1,xs1@xs2) | xs1 xs2 . xs2 ≠ [] ∧ (∃ xs3 . xs1@xs2@xs3 = xs)}"
  unfolding prefix_pairs_set by auto

lemma prefixes_Cons :
  assumes "(x#xs) ∈ set (prefixes (y#ys))"
  shows "x = y" and "xs ∈ set (prefixes ys)"
proof -
  show "x = y"
    by (metis Cons_eq_appendI assms nth_Cons_0 prefixes_set_ob) 
  
  show "xs ∈ set (prefixes ys)"
  proof -
    obtain xs' xs'' where "(x#xs) = xs'" and "(y#ys) = xs'@xs''"
      by (meson assms prefixes_set_ob)
    then have "xs' = x#tl xs'"
      by auto
    then have "xs = tl xs'"
      using ‹(x#xs) = xs'› by auto
    moreover have "ys = (tl xs')@xs''"
      using ‹(y#ys) = xs'@xs''› ‹xs' = x#tl xs'›
      by (metis append_Cons list.inject) 
    ultimately show ?thesis 
      unfolding prefixes_set by blast
  qed
qed

lemma prefixes_prepend :
  assumes "xs' ∈ set (prefixes xs)"
  shows "ys@xs' ∈ set (prefixes (ys@xs))"
proof -
  obtain xs'' where "xs = xs'@xs''"
    using assms
    using prefixes_set_ob by auto
  then have "(ys@xs) = (ys@xs')@xs''"
    by auto
  then show ?thesis
    unfolding prefixes_set by auto
qed


lemma prefixes_prefix_suffix_ob :
  assumes "a ∈ set (prefixes (b@c))"
  and     "a ∉ set (prefixes b)"
obtains c' c'' where "c = c'@c''"
                 and "a = b@c'"
                 and "c' ≠ []"
proof -
  have "∃ c' c'' . c = c'@c'' ∧ a = b@c' ∧ c' ≠ []"
    using assms 
  proof (induction b arbitrary: a)
    case Nil
    then show ?case 
      unfolding prefixes_set
      by fastforce 
  next
    case (Cons x xs)
    show ?case proof (cases a)
      case Nil
      then show ?thesis
        by (metis Cons.prems(2) list.size(3) prefixes_take_iff take_eq_Nil) 
    next
      case (Cons a' as)
      then have "a' # as ∈ set (prefixes (x #(xs@c)))"
        using Cons.prems(1) by auto
  
      have "a' = x" and "as ∈ set (prefixes (xs@c))"
        using prefixes_Cons[OF ‹a' # as ∈ set (prefixes (x #(xs@c)))›] 
        by auto
      moreover have "as ∉ set (prefixes xs)"
        using ‹a ∉ set (prefixes (x # xs))› unfolding Cons ‹a' = x› prefixes_set by auto
  
      ultimately obtain c' c'' where "c = c'@c''"
                                 and "as = xs@c'"
                                 and "c' ≠ []"
        using Cons.IH by blast
      then have "c = c'@c''" and "a = (x#xs)@c'" and "c' ≠ []"
        unfolding Cons ‹a' = x› by auto
      then show ?thesis
        using that by blast
    qed
  qed
  then show ?thesis using that by blast
qed

fun list_ordered_pairs :: "'a list ⇒ ('a × 'a) list" where
  "list_ordered_pairs [] = []" |
  "list_ordered_pairs (x#xs) = (map (Pair x) xs) @ (list_ordered_pairs xs)"

lemma list_ordered_pairs_set_containment :
  assumes "x ∈ list.set xs"
  and     "y ∈ list.set xs"
  and     "x ≠ y"
shows "(x,y) ∈ list.set (list_ordered_pairs xs) ∨ (y,x) ∈ list.set (list_ordered_pairs xs)"
  using assms by (induction xs; auto)

subsection ‹Calculating Distinct Non-Reflexive Pairs over List Elements› 

fun non_sym_dist_pairs' :: "'a list ⇒ ('a × 'a) list" where
  "non_sym_dist_pairs' [] = []" |
  "non_sym_dist_pairs' (x#xs) = (map (λ y. (x,y)) xs) @ non_sym_dist_pairs' xs"

fun non_sym_dist_pairs :: "'a list ⇒ ('a × 'a) list" where
  "non_sym_dist_pairs xs = non_sym_dist_pairs' (remdups xs)"


lemma non_sym_dist_pairs_subset : "set (non_sym_dist_pairs xs) ⊆ (set xs) × (set xs)"
  by (induction xs; auto)

lemma non_sym_dist_pairs'_elems_distinct:
  assumes "distinct xs"
  and     "(x,y) ∈ set (non_sym_dist_pairs' xs)"
shows "x ∈ set xs" 
and   "y ∈ set xs"
and   "x ≠ y"
proof -
  show "x ∈ set xs" and "y ∈ set xs"
    using non_sym_dist_pairs_subset assms(2) by (induction xs; auto)+
  show "x ≠ y"
    using assms by (induction xs; auto)
qed

lemma non_sym_dist_pairs_elems_distinct:
  assumes "(x,y) ∈ set (non_sym_dist_pairs xs)"
shows "x ∈ set xs" 
and   "y ∈ set xs"
and   "x ≠ y"
  using non_sym_dist_pairs'_elems_distinct assms
  unfolding non_sym_dist_pairs.simps by fastforce+


lemma non_sym_dist_pairs_elems :
  assumes "x ∈ set xs"
  and     "y ∈ set xs"
  and     "x ≠ y"
shows "(x,y) ∈ set (non_sym_dist_pairs xs) ∨ (y,x) ∈ set (non_sym_dist_pairs xs)"
  using assms by (induction xs; auto)



lemma non_sym_dist_pairs'_elems_non_refl :
  assumes "distinct xs"
  and     "(x,y) ∈ set (non_sym_dist_pairs' xs)"
shows "(y,x) ∉ set (non_sym_dist_pairs' xs)"
  using assms  
proof (induction xs arbitrary: x y)
  case Nil
  then show ?case by auto
next
  case (Cons z zs)
  then have "distinct zs" by auto

  have "x ≠ y"
    using non_sym_dist_pairs'_elems_distinct[OF Cons.prems] by simp

  consider (a) "(x,y) ∈ set (map (Pair z) zs)" |
           (b) "(x,y) ∈ set (non_sym_dist_pairs' zs)"
    using ‹(x,y) ∈ set (non_sym_dist_pairs' (z#zs))› unfolding non_sym_dist_pairs'.simps by auto
  then show ?case proof cases
    case a
    then have "x = z" by auto
    then have "(y,x) ∉ set (map (Pair z) zs)"
      using ‹x ≠ y› by auto
    moreover have "x ∉ set zs"
      using ‹x = z› ‹distinct (z#zs)› by auto
    ultimately show ?thesis 
      using ‹distinct zs› non_sym_dist_pairs'_elems_distinct(2) by fastforce
  next
    case b
    then have "x ≠ z" and "y ≠ z"
      using Cons.prems unfolding non_sym_dist_pairs'.simps 
      by (meson distinct.simps(2) non_sym_dist_pairs'_elems_distinct(1,2))+
    
    then show ?thesis 
      using Cons.IH[OF ‹distinct zs› b] by auto
  qed
qed


lemma non_sym_dist_pairs_elems_non_refl :
  assumes "(x,y) ∈ set (non_sym_dist_pairs xs)"
  shows "(y,x) ∉ set (non_sym_dist_pairs xs)"
  using assms by (simp add: non_sym_dist_pairs'_elems_non_refl)


lemma non_sym_dist_pairs_set_iff :
  "(x,y) ∈ set (non_sym_dist_pairs xs) 
    ⟷ (x ≠ y ∧ x ∈ set xs ∧ y ∈ set xs ∧ (y,x) ∉ set (non_sym_dist_pairs xs))"
  using non_sym_dist_pairs_elems_non_refl[of x y xs] 
        non_sym_dist_pairs_elems[of x xs y] 
        non_sym_dist_pairs_elems_distinct[of x y xs] by blast 



subsection ‹Finite Linear Order From List Positions›

fun linear_order_from_list_position' :: "'a list ⇒ ('a × 'a) list" where
  "linear_order_from_list_position' [] = []" |
  "linear_order_from_list_position' (x#xs) 
      = (x,x) # (map (λ y . (x,y)) xs) @ (linear_order_from_list_position' xs)"

fun linear_order_from_list_position :: "'a list ⇒ ('a × 'a) list" where
  "linear_order_from_list_position xs = linear_order_from_list_position' (remdups xs)"



lemma linear_order_from_list_position_set :
  "set (linear_order_from_list_position xs) 
    = (set (map (λ x . (x,x)) xs)) ∪ set (non_sym_dist_pairs xs)"
  by (induction xs; auto)

lemma linear_order_from_list_position_total: 
  "total_on (set xs) (set (linear_order_from_list_position xs))"
  unfolding linear_order_from_list_position_set
  using non_sym_dist_pairs_elems[of _ xs]
  by (meson UnI2 total_onI)

lemma linear_order_from_list_position_refl: 
  "refl_on (set xs) (set (linear_order_from_list_position xs))"  
proof 
  show "set (linear_order_from_list_position xs) ⊆ set xs × set xs"
    unfolding linear_order_from_list_position_set
    using non_sym_dist_pairs_subset[of xs] by auto
  show "⋀x. x ∈ set xs ⟹ (x, x) ∈ set (linear_order_from_list_position xs)"
    unfolding linear_order_from_list_position_set
    using non_sym_dist_pairs_subset[of xs] by auto
qed

lemma linear_order_from_list_position_antisym: 
  "antisym (set (linear_order_from_list_position xs))"
proof 
  fix x y assume "(x, y) ∈ set (linear_order_from_list_position xs)" 
          and    "(y, x) ∈ set (linear_order_from_list_position xs)"
  then have "(x, y) ∈ set (map (λx. (x, x)) xs) ∪ set (non_sym_dist_pairs xs)"
       and  "(y, x) ∈ set (map (λx. (x, x)) xs) ∪ set (non_sym_dist_pairs xs)"
    unfolding linear_order_from_list_position_set by blast+
  then consider (a) "(x, y) ∈ set (map (λx. (x, x)) xs)" |
                (b) "(x, y) ∈ set (non_sym_dist_pairs xs)"
    by blast
  then show "x = y"
  proof cases
    case a
    then show ?thesis by auto
  next
    case b
    then have "x ≠ y" and "(y,x) ∉ set (non_sym_dist_pairs xs)"
      using non_sym_dist_pairs_set_iff[of x y xs] by simp+
    then have "(y, x) ∉ set (map (λx. (x, x)) xs) ∪ set (non_sym_dist_pairs xs)"
      by auto
    then show ?thesis 
     using ‹(y, x) ∈ set (map (λx. (x, x)) xs) ∪ set (non_sym_dist_pairs xs)› by blast
  qed
qed


lemma non_sym_dist_pairs'_indices : 
  "distinct xs ⟹ (x,y) ∈ set (non_sym_dist_pairs' xs) 
   ⟹ (∃ i j . xs ! i = x ∧ xs ! j = y ∧ i < j ∧ i < length xs ∧ j < length xs)"
proof (induction xs)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)
  show ?case proof (cases "a = x")
    case True
    then have "(a#xs) ! 0 = x" and "0 < length (a#xs)"
      by auto
    
    have "y ∈ set xs"
      using non_sym_dist_pairs'_elems_distinct(2,3)[OF Cons.prems(1,2)] True by auto
    then obtain j where "xs ! j = y" and "j < length xs"
      by (meson in_set_conv_nth)
    then have "(a#xs) ! (Suc j) = y" and "Suc j < length (a#xs)"
      by auto

    then show ?thesis 
      using ‹(a#xs) ! 0 = x› ‹0 < length (a#xs)› by blast
  next
    case False
    then have "(x,y) ∈ set (non_sym_dist_pairs' xs)"
      using Cons.prems(2) by auto
    then show ?thesis 
      using Cons.IH Cons.prems(1)
      by (metis Suc_mono distinct.simps(2) length_Cons nth_Cons_Suc)
  qed
qed



lemma non_sym_dist_pairs'_trans: "distinct xs ⟹ trans (set (non_sym_dist_pairs' xs))"
proof 
  fix x y z assume "distinct xs" 
            and    "(x, y) ∈ set (non_sym_dist_pairs' xs)" 
            and    "(y, z) ∈ set (non_sym_dist_pairs' xs)"

  obtain nx ny where "xs ! nx = x" and "xs ! ny = y" and "nx < ny" 
                 and "nx < length xs" and "ny < length xs"
    using non_sym_dist_pairs'_indices[OF ‹distinct xs› ‹(x, y) ∈ set (non_sym_dist_pairs' xs)›] 
    by blast

  obtain ny' nz where "xs ! ny' = y" and "xs ! nz = z" and "ny'< nz" 
                  and "ny' < length xs" and "nz < length xs"
    using non_sym_dist_pairs'_indices[OF ‹distinct xs› ‹(y, z) ∈ set (non_sym_dist_pairs' xs)›] 
    by blast

  have "ny' = ny"
    using ‹distinct xs› ‹xs ! ny = y› ‹xs ! ny' = y› ‹ny < length xs› ‹ny' < length xs› 
          nth_eq_iff_index_eq 
    by metis
  then have "nx < nz"
    using ‹nx < ny› ‹ny' < nz› by auto

  then have "nx ≠ nz" by simp
  then have "x ≠ z"
    using ‹distinct xs› ‹xs ! nx = x› ‹xs ! nz = z› ‹nx < length xs› ‹nz < length xs› 
          nth_eq_iff_index_eq 
    by metis

  have "remdups xs = xs"
    using ‹distinct xs› by auto

  have "¬(z, x) ∈ set (non_sym_dist_pairs' xs)"
  proof 
    assume "(z, x) ∈ set (non_sym_dist_pairs' xs)"
    then obtain nz' nx' where "xs ! nx' = x" and "xs ! nz' = z" and "nz'< nx'" 
                          and "nx' < length xs" and "nz' < length xs"
      using non_sym_dist_pairs'_indices[OF ‹distinct xs›, of z x] by metis

    have "nx' = nx"
      using ‹distinct xs› ‹xs ! nx = x› ‹xs ! nx' = x› ‹nx < length xs› ‹nx' < length xs› 
            nth_eq_iff_index_eq 
      by metis
    moreover have "nz' = nz"
      using ‹distinct xs› ‹xs ! nz = z› ‹xs ! nz' = z› ‹nz < length xs› ‹nz' < length xs› 
            nth_eq_iff_index_eq 
      by metis
    ultimately have "nz < nx"
      using ‹nz'< nx'› by auto
    then show "False"
      using ‹nx < nz› by simp    
  qed
  then show "(x, z) ∈ set (non_sym_dist_pairs' xs)" 
    using non_sym_dist_pairs'_elems_distinct(1)[OF ‹distinct xs› ‹(x, y) ∈ set (non_sym_dist_pairs' xs)›]
          non_sym_dist_pairs'_elems_distinct(2)[OF ‹distinct xs› ‹(y, z) ∈ set (non_sym_dist_pairs' xs)›]
          ‹x ≠ z›
          non_sym_dist_pairs_elems[of x xs z]
    unfolding non_sym_dist_pairs.simps ‹remdups xs = xs› 
    by blast
qed


lemma non_sym_dist_pairs_trans: "trans (set (non_sym_dist_pairs xs))"
  using non_sym_dist_pairs'_trans[of "remdups xs", OF distinct_remdups] 
  unfolding non_sym_dist_pairs.simps 
  by assumption



lemma linear_order_from_list_position_trans: "trans (set (linear_order_from_list_position xs))"
proof 
  fix x y z assume "(x, y) ∈ set (linear_order_from_list_position xs)" 
               and "(y, z) ∈ set (linear_order_from_list_position xs)"
  then consider (a) "(x, y) ∈ set (map (λx. (x, x)) xs) ∧ (y, z) ∈ set (map (λx. (x, x)) xs)" |
                (b) "(x, y) ∈ set (map (λx. (x, x)) xs) ∧ (y, z) ∈ set (non_sym_dist_pairs xs)" |
                (c) "(x, y) ∈ set (non_sym_dist_pairs xs) ∧ (y, z) ∈ set (map (λx. (x, x)) xs)" |
                (d) "(x, y) ∈ set (non_sym_dist_pairs xs) ∧ (y, z) ∈ set (non_sym_dist_pairs xs)"
    unfolding linear_order_from_list_position_set by blast+
  then show "(x, z) ∈ set (linear_order_from_list_position xs)"
  proof cases
    case a
    then show ?thesis unfolding linear_order_from_list_position_set by auto
  next
    case b
    then show ?thesis unfolding linear_order_from_list_position_set by auto
  next
    case c
    then show ?thesis unfolding linear_order_from_list_position_set by auto
  next
    case d
    then show ?thesis unfolding linear_order_from_list_position_set 
                      using non_sym_dist_pairs_trans 
                      by (metis UnI2 transE)
  qed
qed



subsection ‹Find And Remove in a Single Pass›

fun find_remove' :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ ('a × 'a list) option" where
  "find_remove' P [] _ = None" |
  "find_remove' P (x#xs) prev = (if P x
      then Some (x,prev@xs) 
      else find_remove' P xs (prev@[x]))"

fun find_remove :: "('a ⇒ bool) ⇒ 'a list ⇒ ('a × 'a list) option" where
  "find_remove P xs = find_remove' P xs []"

lemma find_remove'_set : 
  assumes "find_remove' P xs prev = Some (x,xs')"
shows "P x"
and   "x ∈ set xs"
and   "xs' = prev@(remove1 x xs)"
proof -
  have "P x ∧ x ∈ set xs ∧ xs' = prev@(remove1 x xs)"
    using assms proof (induction xs arbitrary: prev xs')
    case Nil
    then show ?case by auto
  next
    case (Cons x xs)
    show ?case proof (cases "P x")
      case True
      then show ?thesis using Cons by auto
    next
      case False
      then show ?thesis using Cons by fastforce 
    qed
  qed
  then show "P x"
      and   "x ∈ set xs"
      and   "xs' = prev@(remove1 x xs)"
    by blast+
qed

lemma find_remove'_set_rev :
  assumes "x ∈ set xs"
  and     "P x"
shows "find_remove' P xs prev ≠ None" 
using assms(1) proof(induction xs arbitrary: prev)
  case Nil
  then show ?case by auto
next
  case (Cons x' xs)
  show ?case proof (cases "P x")
    case True
    then show ?thesis using Cons by auto
  next
    case False
    then show ?thesis using Cons
      using assms(2) by auto 
  qed
qed


lemma find_remove_None_iff :
  "find_remove P xs = None ⟷ ¬ (∃x . x ∈ set xs ∧ P x)"
  unfolding find_remove.simps 
  using find_remove'_set(1,2) 
        find_remove'_set_rev
  by (metis old.prod.exhaust option.exhaust)

lemma find_remove_set : 
  assumes "find_remove P xs = Some (x,xs')"
shows "P x"
and   "x ∈ set xs"
and   "xs' = (remove1 x xs)"
  using assms find_remove'_set[of P xs "[]" x xs'] by auto




fun find_remove_2' :: "('a⇒'b⇒bool) ⇒ 'a list ⇒ 'b list ⇒ 'a list ⇒ ('a × 'b × 'a list) option" 
  where
  "find_remove_2' P [] _ _ = None" |
  "find_remove_2' P (x#xs) ys prev = (case find (λy . P x y) ys of
      Some y ⇒ Some (x,y,prev@xs) |
      None   ⇒ find_remove_2' P xs ys (prev@[x]))"

fun find_remove_2 :: "('a ⇒ 'b ⇒ bool) ⇒ 'a list ⇒ 'b list ⇒ ('a × 'b × 'a list) option" where
  "find_remove_2 P xs ys = find_remove_2' P xs ys []"


lemma find_remove_2'_set : 
  assumes "find_remove_2' P xs ys prev = Some (x,y,xs')"
shows "P x y"
and   "x ∈ set xs"
and   "y ∈ set ys"
and   "distinct (prev@xs) ⟹ set xs' = (set prev ∪ set xs) - {x}"
and   "distinct (prev@xs) ⟹ distinct xs'"
and   "xs' = prev@(remove1 x xs)"
and   "find (P x) ys = Some y"
proof -
  have "P x y 
        ∧ x ∈ set xs 
        ∧ y ∈ set ys 
        ∧ (distinct (prev@xs) ⟶ set xs' = (set prev ∪ set xs) - {x}) 
        ∧ (distinct (prev@xs) ⟶ distinct xs') 
        ∧ (xs' = prev@(remove1 x xs)) 
        ∧ find (P x) ys = Some y"
    using assms 
  proof (induction xs arbitrary: prev xs' x y)
    case Nil
    then show ?case by auto 
  next
    case (Cons x' xs)
    then show ?case proof (cases "find (λy . P x' y) ys")
      case None
      then have "find_remove_2' P (x' # xs) ys prev = find_remove_2' P xs ys (prev@[x'])"
        using Cons.prems(1) by auto
      hence *: "find_remove_2' P xs ys (prev@[x']) = Some (x, y, xs')"
        using Cons.prems(1) by simp
      
      have "x' ≠ x"
        by (metis "*" Cons.IH None find_from)
      moreover have "distinct (prev @ x' # xs) ⟶ distinct ((x' # prev) @ xs)"
        by auto
      ultimately show ?thesis using Cons.IH[OF *]
        by auto
    next
      case (Some y')
      then have "find_remove_2' P (x' # xs) ys prev = Some (x',y',prev@xs)"
        by auto
      then show ?thesis using Some
        using Cons.prems(1) find_condition find_set by fastforce 
    qed
  qed
  then show "P x y"
      and   "x ∈ set xs"
      and   "y ∈ set ys"
      and   "distinct (prev @ xs) ⟹ set xs' = (set prev ∪ set xs) - {x}"
      and   "distinct (prev@xs) ⟹ distinct xs'"
      and   "xs' = prev@(remove1 x xs)"
      and   "find (P x) ys = Some y"
    by blast+
qed



lemma find_remove_2'_strengthening : 
  assumes "find_remove_2' P xs ys prev = Some (x,y,xs')"
  and     "P' x y"
  and     "⋀ x' y' . P' x' y' ⟹ P x' y'"
shows "find_remove_2' P' xs ys prev = Some (x,y,xs')"
  using assms proof (induction xs arbitrary: prev)
  case Nil
  then show ?case by auto
next
  case (Cons x' xs)
  then show ?case proof (cases "find (λy . P x' y) ys")
    case None
    then show ?thesis using Cons
      by (metis (mono_tags, lifting) find_None_iff find_remove_2'.simps(2) option.simps(4))  
  next
    case (Some a)
    then have "x' = x" and "a = y"
      using Cons.prems(1) unfolding find_remove_2'.simps by auto
    then have "find (λy . P x y) ys = Some y"
      using find_remove_2'_set[OF Cons.prems(1)] by auto
    then have "find (λy . P' x y) ys = Some y"
      using Cons.prems(3) proof (induction ys)
      case Nil
      then show ?case by auto
    next
      case (Cons y' ys)
      then show ?case
        by (metis assms(2) find.simps(2) option.inject) 
    qed
      
    then show ?thesis  
      using find_remove_2'_set(6)[OF Cons.prems(1)]
      unfolding ‹x' = x› find_remove_2'.simps by auto      
  qed
qed

lemma find_remove_2_strengthening : 
  assumes "find_remove_2 P xs ys = Some (x,y,xs')"
  and     "P' x y"
  and     "⋀ x' y' . P' x' y' ⟹ P x' y'"
shows "find_remove_2 P' xs ys = Some (x,y,xs')"
  using assms find_remove_2'_strengthening
  by (metis find_remove_2.simps) 



lemma find_remove_2'_prev_independence :
  assumes "find_remove_2' P xs ys prev = Some (x,y,xs')"
  shows "∃ xs'' . find_remove_2' P xs ys prev' = Some (x,y,xs'')" 
  using assms proof (induction xs arbitrary: prev prev' xs')
  case Nil
  then show ?case by auto
next
  case (Cons x' xs)
  show ?case proof (cases "find (λy . P x' y) ys")
    case None
    then show ?thesis
      using Cons.IH Cons.prems by auto
      
  next
    case (Some a)
    then show ?thesis using Cons.prems unfolding find_remove_2'.simps
      by simp 
  qed
qed


lemma find_remove_2'_filter :
  assumes "find_remove_2' P (filter P' xs) ys prev = Some (x,y,xs')"
  and     "⋀ x y . ¬ P' x ⟹ ¬ P x y"
shows "∃ xs'' . find_remove_2' P xs ys prev = Some (x,y,xs'')"
  using assms(1) proof (induction xs arbitrary: prev prev xs')
  case Nil
  then show ?case by auto
next
  case (Cons x' xs)
  then show ?case proof (cases "P' x'")
    case True
    then have *:"find_remove_2' P (filter P' (x' # xs)) ys prev 
                = find_remove_2' P (x' # filter P' xs) ys prev" 
      by auto
      
    show ?thesis proof (cases "find (λy . P x' y) ys")
      case None
      then show ?thesis
        by (metis Cons.IH Cons.prems  find_remove_2'.simps(2) option.simps(4) *)
    next
      case (Some a) 
      then have "x' = x" and "a = y"
        using Cons.prems
        unfolding * find_remove_2'.simps by auto
        
      show ?thesis 
        using Some 
        unfolding ‹x' = x› ‹a = y› find_remove_2'.simps
        by simp
    qed
  next
    case False
    then have "find_remove_2' P (filter P' xs) ys prev = Some (x,y,xs')"
      using Cons.prems by auto

    from False assms(2) have "find (λy . P x' y) ys = None"
      by (simp add: find_None_iff)
    then have "find_remove_2' P (x'#xs) ys prev = find_remove_2' P xs ys (prev@[x'])"
      by auto
    
    show ?thesis 
      using Cons.IH[OF ‹find_remove_2' P (filter P' xs) ys prev = Some (x,y,xs')›] 
      unfolding ‹find_remove_2' P (x'#xs) ys prev = find_remove_2' P xs ys (prev@[x'])›
      using find_remove_2'_prev_independence by metis
  qed
qed


lemma find_remove_2_filter :
  assumes "find_remove_2 P (filter P' xs) ys = Some (x,y,xs')"
  and     "⋀ x y . ¬ P' x ⟹ ¬ P x y"
shows "∃ xs'' . find_remove_2 P xs ys = Some (x,y,xs'')"
  using assms by (simp add: find_remove_2'_filter)  


lemma find_remove_2'_index : 
  assumes "find_remove_2' P xs ys prev = Some (x,y,xs')"
  obtains i i' where "i < length xs" 
                     "xs ! i = x"
                     "⋀ j . j < i ⟹ find (λy . P (xs ! j) y) ys = None"
                     "i' < length ys"
                     "ys ! i' = y"
                     "⋀ j . j < i' ⟹ ¬ P (xs ! i) (ys ! j)"
proof -
  have "∃ i i' . i < length xs 
                  ∧ xs ! i = x 
                  ∧ (∀ j < i . find (λy . P (xs ! j) y) ys = None) 
                  ∧ i' < length ys ∧ ys ! i' = y 
                  ∧ (∀ j < i' . ¬ P (xs ! i) (ys ! j))"
    using assms 
  proof (induction xs arbitrary: prev xs' x y)
    case Nil
    then show ?case by auto 
  next
    case (Cons x' xs)
    then show ?case proof (cases "find (λy . P x' y) ys")
      case None
      then have "find_remove_2' P (x' # xs) ys prev = find_remove_2' P xs ys (prev@[x'])"
        using Cons.prems(1) by auto
      hence *: "find_remove_2' P xs ys (prev@[x']) = Some (x, y, xs')"
        using Cons.prems(1) by simp
      
      have "x' ≠ x"
        using find_remove_2'_set(1,3)[OF *] None unfolding find_None_iff
        by blast

      obtain i i' where "i < length xs" and "xs ! i = x" 
                    and "(∀ j < i . find (λy . P (xs ! j) y) ys = None)" and "i' < length ys" 
                    and "ys ! i' = y" and "(∀ j < i' . ¬ P (xs ! i) (ys ! j))"
        using Cons.IH[OF *] by blast

      have "Suc i < length (x'#xs)"
        using ‹i < length xs› by auto
      moreover have "(x'#xs) ! Suc i = x"
        using ‹xs ! i = x› by auto
      moreover have "(∀ j < Suc i . find (λy . P ((x'#xs) ! j) y) ys = None)"
      proof -
        have "⋀ j . j > 0 ⟹ j < Suc i ⟹ find (λy . P ((x'#xs) ! j) y) ys = None"
          using ‹(∀ j < i . find (λy . P (xs ! j) y) ys = None)› by auto 
        then show ?thesis using None
          by (metis neq0_conv nth_Cons_0) 
      qed
      moreover have "(∀ j < i' . ¬ P ((x'#xs) ! Suc i) (ys ! j))"
        using ‹(∀ j < i' . ¬ P (xs ! i) (ys ! j))›
        by simp 
      
      ultimately show ?thesis 
        using that ‹i' < length ys› ‹ys ! i' = y› by blast
    next
      case (Some y')
      then have "x' = x" and "y' = y"
        using Cons.prems by force+
      
      have "0 < length (x'#xs) ∧ (x'#xs) ! 0 = x' 
            ∧ (∀ j < 0 . find (λy . P ((x'#xs) ! j) y) ys = None)" 
        by auto
      moreover obtain i' where "i' < length ys" and "ys ! i' = y'" 
                           and "(∀ j < i' . ¬ P ((x'#xs) ! 0) (ys ! j))" 
        using find_sort_index[OF Some] by auto
      ultimately show ?thesis 
        unfolding ‹x' = x› ‹y' = y› by blast
    qed
  qed
  then show ?thesis using that by blast
qed

lemma find_remove_2_index : 
  assumes "find_remove_2 P xs ys = Some (x,y,xs')"
  obtains i i' where "i < length xs" 
                     "xs ! i = x"
                     "⋀ j . j < i ⟹ find (λy . P (xs ! j) y) ys = None"
                     "i' < length ys"
                     "ys ! i' = y"
                     "⋀ j . j < i' ⟹ ¬ P (xs ! i) (ys ! j)"
  using assms find_remove_2'_index[of P xs ys "[]" x y xs'] by auto


lemma find_remove_2'_set_rev :
  assumes "x ∈ set xs"
  and     "y ∈ set ys"
  and     "P x y"
shows "find_remove_2' P xs ys prev ≠ None" 
using assms(1) proof(induction xs arbitrary: prev)
  case Nil
  then show ?case by auto
next
  case (Cons x' xs)
  then show ?case proof (cases "find (λy . P x' y) ys")
    case None
    then have "x ≠ x'" 
      using assms(2,3) by (metis find_None_iff) 
    then have "x ∈ set xs"
      using Cons.prems by auto
    then show ?thesis 
      using Cons.IH unfolding find_remove_2'.simps None by auto
  next
    case (Some a)
    then show ?thesis by auto
  qed
qed


lemma find_remove_2'_diff_prev_None :
  "(find_remove_2' P xs ys prev = None ⟹ find_remove_2' P xs ys prev' = None)" 
proof (induction xs arbitrary: prev prev')
  case Nil
  then show ?case by auto
next
  case (Cons x xs)
  show ?case proof (cases "find (λy . P x y) ys")
    case None
    then have "find_remove_2' P (x#xs) ys prev = find_remove_2' P xs ys (prev@[x])" 
         and  "find_remove_2' P (x#xs) ys prev' = find_remove_2' P xs ys (prev'@[x])"
      by auto
    then show ?thesis using Cons by auto 
  next
    case (Some a)
    then show ?thesis using Cons by auto
  qed
qed

lemma find_remove_2'_diff_prev_Some :
  "(find_remove_2' P xs ys prev = Some (x,y,xs') 
    ⟹ ∃ xs'' . find_remove_2' P xs ys prev' = Some (x,y,xs''))" 
proof (induction xs arbitrary: prev prev')
  case Nil
  then show ?case by auto
next
  case (Cons x xs)
  show ?case proof (cases "find (λy . P x y) ys")
    case None
    then have "find_remove_2' P (x#xs) ys prev = find_remove_2' P xs ys (prev@[x])" 
         and  "find_remove_2' P (x#xs) ys prev' = find_remove_2' P xs ys (prev'@[x])"
      by auto
    then show ?thesis using Cons by auto 
  next
    case (Some a)
    then show ?thesis using Cons by auto
  qed
qed


lemma find_remove_2_None_iff :
  "find_remove_2 P xs ys = None ⟷ ¬ (∃x y . x ∈ set xs ∧ y ∈ set ys ∧ P x y)"
  unfolding find_remove_2.simps 
  using find_remove_2'_set(1-3) find_remove_2'_set_rev
  by (metis old.prod.exhaust option.exhaust)

lemma find_remove_2_set : 
  assumes "find_remove_2 P xs ys = Some (x,y,xs')"
shows "P x y"
and   "x ∈ set xs"
and   "y ∈ set ys"
and   "distinct xs ⟹ set xs' = (set xs) - {x}"
and   "distinct xs ⟹ distinct xs'"
and   "xs' = (remove1 x xs)"
  using assms find_remove_2'_set[of P xs ys "[]" x y xs'] 
  unfolding find_remove_2.simps by auto

lemma find_remove_2_removeAll :
  assumes "find_remove_2 P xs ys = Some (x,y,xs')"
  and     "distinct xs"
shows "xs' = removeAll x xs"
  using find_remove_2_set(6)[OF assms(1)]
  by (simp add: assms(2) distinct_remove1_removeAll) 

lemma find_remove_2_length :
  assumes "find_remove_2 P xs ys = Some (x,y,xs')"
  shows "length xs' = length xs - 1"
  using find_remove_2_set(2,6)[OF assms]
  by (simp add: length_remove1) 



fun separate_by :: "('a ⇒ bool) ⇒ 'a list ⇒ ('a list × 'a list)" where
  "separate_by P xs = (filter P xs, filter (λ x . ¬ P x) xs)"

lemma separate_by_code[code] :
  "separate_by P xs = foldr (λx (prevPass,prevFail) . if P x then (x#prevPass,prevFail) else (prevPass,x#prevFail)) xs ([],[])"
proof (induction xs)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)

  let ?f = "(λx (prevPass,prevFail) . if P x then (x#prevPass,prevFail) else (prevPass,x#prevFail))"

  have "(filter P xs, filter (λ x . ¬ P x) xs) = foldr ?f xs ([],[])"
    using Cons.IH by auto
  moreover have "separate_by P (a#xs) = ?f a (filter P xs, filter (λ x . ¬ P x) xs)"
    by auto
  ultimately show ?case 
    by (cases "P a"; auto)
qed

fun find_remove_2_all :: "('a ⇒ 'b ⇒ bool) ⇒ 'a list ⇒ 'b list ⇒ (('a × 'b) list × 'a list)" where
  "find_remove_2_all P xs ys =
    (map (λ x . (x, the (find (λy . P x y) ys))) (filter (λ x . find (λy . P x y) ys ≠ None) xs)
    ,filter (λ x . find (λy . P x y) ys = None) xs)"


fun find_remove_2_all' :: "('a ⇒ 'b ⇒ bool) ⇒ 'a list ⇒ 'b list ⇒ (('a × 'b) list × 'a list)" where
  "find_remove_2_all' P xs ys = 
    (let (successesWithWitnesses,failures) = separate_by (λ(x,y) . y ≠ None) (map (λ x . (x,find (λy . P x y) ys)) xs)
    in (map (λ (x,y) . (x, the y)) successesWithWitnesses, map fst failures))"

lemma find_remove_2_all_code[code] :
  "find_remove_2_all P xs ys = find_remove_2_all' P xs ys"
proof -
  let ?s1 = "map (λ x . (x, the (find (λy . P x y) ys))) (filter (λ x . find (λy . P x y) ys ≠ None) xs)"
  let ?f1 = "filter (λ x . find (λy . P x y) ys = None) xs"

  let ?s2 = "map (λ (x,y) . (x, the y)) (filter (λ(x,y) . y ≠ None) (map (λ x . (x,find (λy . P x y) ys)) xs))"
  let ?f2 = "map fst (filter (λ(x,y) . y = None) (map (λ x . (x,find (λy . P x y) ys)) xs))"

  have "find_remove_2_all P xs ys = (?s1,?f1)" 
    by simp
  moreover have "find_remove_2_all' P xs ys = (?s2,?f2)" 
  proof -
    have "∀p. (λpa. ¬ (case pa of (a::'a, x::'b option) ⇒ p x)) = (λ(a, z). ¬ p z)"
      by force
    then show ?thesis
      unfolding find_remove_2_all'.simps Let_def separate_by.simps  
      by force
  qed
  moreover have "?s1 = ?s2" 
    by (induction xs; auto)
  moreover have "?f1 = ?f2" 
    by (induction xs; auto)
  ultimately show ?thesis 
    by simp
qed
   






subsection ‹Set-Operations on Lists›

fun pow_list :: "'a list ⇒ 'a list list" where
  "pow_list [] = [[]]" |
  "pow_list (x#xs) = (let pxs = pow_list xs in pxs @ map (λ ys . x#ys) pxs)"


lemma pow_list_set :
  "set (map set (pow_list xs)) = Pow (set xs)"
proof (induction xs)
case Nil
  then show ?case by auto
next
  case (Cons x xs)

  moreover have "Pow (set (x # xs)) = Pow (set xs) ∪ (image (insert x) (Pow (set xs)))"
    by (simp add: Pow_insert)
    
  moreover have "set (map set (pow_list (x#xs))) 
                  = set (map set (pow_list xs)) ∪ (image (insert x) (set (map set (pow_list xs))))"
  proof -
    have "⋀ ys . ys ∈ set (map set (pow_list (x#xs))) 
            ⟹ ys ∈ set (map set (pow_list xs)) ∪ (image (insert x) (set (map set (pow_list xs))))" 
    proof -
      fix ys assume "ys ∈ set (map set (pow_list (x#xs)))"
      then consider (a) "ys ∈ set (map set (pow_list xs))" |
                    (b) "ys ∈ set (map set (map ((#) x) (pow_list xs)))"
        unfolding pow_list.simps Let_def by auto
      then show "ys ∈ set (map set (pow_list xs)) ∪ (image (insert x) (set (map set (pow_list xs))))" 
        by (cases; auto)
    qed
    moreover have "⋀ ys . ys ∈ set (map set (pow_list xs)) 
                            ∪ (image (insert x) (set (map set (pow_list xs)))) 
                    ⟹ ys ∈ set (map set (pow_list (x#xs)))"
    proof -
      fix ys assume "ys ∈ set (map set (pow_list xs)) 
                            ∪ (image (insert x) (set (map set (pow_list xs))))"
      then consider (a) "ys ∈ set (map set (pow_list xs))" |
                    (b) "ys ∈ (image (insert x) (set (map set (pow_list xs))))"
        by blast
      then show "ys ∈ set (map set (pow_list (x#xs)))" 
        unfolding pow_list.simps Let_def by (cases; auto)
    qed
    ultimately show ?thesis by blast
  qed
    
  ultimately show ?case
    by auto 
qed


fun inter_list :: "'a list ⇒ 'a list ⇒ 'a list" where
  "inter_list xs ys = filter (λ x . x ∈ set ys) xs"

lemma inter_list_set : "set (inter_list xs ys) = (set xs) ∩ (set ys)"
  by auto

fun subset_list :: "'a list ⇒ 'a list ⇒ bool" where
  "subset_list xs ys = list_all (λ x . x ∈ set ys) xs"

lemma subset_list_set : "subset_list xs ys = ((set xs) ⊆ (set ys))" 
  unfolding subset_list.simps
  by (simp add: Ball_set subset_code(1)) 


subsubsection ‹Removing Subsets in a List of Sets›

lemma remove1_length : "x ∈ set xs ⟹ length (remove1 x xs) < length xs" 
  by (induction xs; auto)


function remove_subsets :: "'a set list ⇒ 'a set list" where
  "remove_subsets [] = []" |
  "remove_subsets (x#xs) = (case find_remove (λ y . x ⊂ y) xs of
    Some (y',xs') ⇒ remove_subsets (y'# (filter (λ y . ¬(y ⊆ x)) xs')) |
    None          ⇒ x # (remove_subsets (filter (λ y . ¬(y ⊆ x)) xs)))"
  by pat_completeness auto
termination   
proof -
  have "⋀x xs. find_remove ((⊂) x) xs = None ⟹ (filter (λy. ¬ y ⊆ x) xs, x # xs) ∈ measure length"
    by (metis dual_order.trans impossible_Cons in_measure length_filter_le not_le_imp_less)
  moreover have "(⋀(x :: 'a set) xs x2 xa y. find_remove ((⊂) x) xs = Some x2 ⟹ (xa, y) = x2 ⟹ (xa # filter (λy. ¬ y ⊆ x) y, x # xs) ∈ measure length)"
  proof -
    fix x :: "'a set"
    fix xs y'xs' y' xs'    
    assume "find_remove ((⊂) x) xs = Some y'xs'" and "(y', xs') = y'xs'"
    then have "find_remove ((⊂) x) xs = Some (y',xs')"
      by auto

    have "length xs' = length xs - 1"
      using find_remove_set(2,3)[OF ‹find_remove ((⊂) x) xs = Some (y',xs')›]
      by (simp add: length_remove1) 
    then have "length (y'#xs') = length xs"
      using find_remove_set(2)[OF ‹find_remove ((⊂) x) xs = Some (y',xs')›]
      using remove1_length by fastforce 
    
    have "length (filter (λy. ¬ y ⊆ x) xs') ≤ length xs'"
      by simp
    then have "length (y' # filter (λy. ¬ y ⊆ x) xs') ≤ length xs' + 1"
      by simp
    then have "length (y' # filter (λy. ¬ y ⊆ x) xs') ≤ length xs" 
      unfolding ‹length (y'#xs') = length xs›[symmetric] by simp
    then show "(y' # filter (λy. ¬ y ⊆ x) xs', x # xs) ∈ measure length"
      by auto 
  qed
  ultimately show ?thesis
    by (relation "measure length"; auto)
qed


lemma remove_subsets_set : "set (remove_subsets xss) = {xs . xs ∈ set xss ∧ (∄ xs' . xs' ∈ set xss ∧ xs ⊂ xs')}"
proof (induction "length xss" arbitrary: xss rule: less_induct)
  case less
  
  show ?case proof (cases xss)

    case Nil
    then show ?thesis by auto
  next
    case (Cons x xss')
    
    show ?thesis proof (cases "find_remove (λ y . x ⊂ y) xss'")
      case None
      then have "(∄ xs' . xs' ∈ set xss' ∧ x ⊂ xs')"
        using find_remove_None_iff by metis

      have "length (filter (λ y . ¬(y ⊆ x)) xss') < length xss"
        using Cons
        by (meson dual_order.trans impossible_Cons leI length_filter_le) 
  
      have "remove_subsets (x#xss') = x # (remove_subsets (filter (λ y . ¬(y ⊆ x)) xss'))"
        using None by auto
      then have "set (remove_subsets (x#xss')) = insert x {xs ∈ set (filter (λy. ¬ y ⊆ x) xss'). ∄xs'. xs' ∈ set (filter (λy. ¬ y ⊆ x) xss') ∧ xs ⊂ xs'}"
        using less[OF ‹length (filter (λ y . ¬(y ⊆ x)) xss') < length xss›]
        by auto
      also have "… = {xs . xs ∈ set (x#xss') ∧ (∄ xs' . xs' ∈ set (x#xss') ∧ xs ⊂ xs')}"
      proof -
        have "⋀ xs . xs ∈ insert x {xs ∈ set (filter (λy. ¬ y ⊆ x) xss'). ∄xs'. xs' ∈ set (filter (λy. ¬ y ⊆ x) xss') ∧ xs ⊂ xs'}
              ⟹ xs ∈ {xs ∈ set (x # xss'). ∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'}"
        proof -
          fix xs assume "xs ∈ insert x {xs ∈ set (filter (λy. ¬ y ⊆ x) xss'). ∄xs'. xs' ∈ set (filter (λy. ¬ y ⊆ x) xss') ∧ xs ⊂ xs'}"
          then consider "xs = x" | "xs ∈ set (filter (λy. ¬ y ⊆ x) xss') ∧ (∄xs'. xs' ∈ set (filter (λy. ¬ y ⊆ x) xss') ∧ xs ⊂ xs')"
            by blast
          then show "xs ∈ {xs ∈ set (x # xss'). ∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'}"
            using ‹(∄ xs' . xs' ∈ set xss' ∧ x ⊂ xs')› by (cases; auto)
        qed
        moreover have "⋀ xs . xs ∈ {xs ∈ set (x # xss'). ∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'}
                        ⟹ xs ∈ insert x {xs ∈ set (filter (λy. ¬ y ⊆ x) xss'). ∄xs'. xs' ∈ set (filter (λy. ¬ y ⊆ x) xss') ∧ xs ⊂ xs'}" 
        proof -
          fix xs assume "xs ∈ {xs ∈ set (x # xss'). ∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'}"
          then have "xs ∈ set (x # xss')" and "∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'"
            by blast+
          then consider "xs = x" | "xs ∈ set xss'" by auto
          then show "xs ∈ insert x {xs ∈ set (filter (λy. ¬ y ⊆ x) xss'). ∄xs'. xs' ∈ set (filter (λy. ¬ y ⊆ x) xss') ∧ xs ⊂ xs'}"
          proof cases
            case 1
            then show ?thesis by auto
          next
            case 2
            show ?thesis proof (cases "xs ⊆ x")
              case True
              then show ?thesis
                using ‹∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'› by auto 
            next
              case False
              then have "xs ∈ set (filter (λy. ¬ y ⊆ x) xss')"
                using 2 by auto
              moreover have "∄xs'. xs' ∈ set (filter (λy. ¬ y ⊆ x) xss') ∧ xs ⊂ xs'"
                using ‹∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'› by auto
              ultimately show ?thesis by auto
            qed 
          qed
        qed
        ultimately show ?thesis
          by (meson subset_antisym subset_eq) 
      qed
      finally show ?thesis unfolding Cons[symmetric] by assumption
    next
      case (Some a)
      then obtain y' xs' where *: "find_remove (λ y . x ⊂ y) xss' = Some (y',xs')" by force
      

      have "length xs' = length xss' - 1"
        using find_remove_set(2,3)[OF *]
        by (simp add: length_remove1) 
      then have "length (y'#xs') = length xss'"
        using find_remove_set(2)[OF *]
        using remove1_length by fastforce 
      
      have "length (filter (λy. ¬ y ⊆ x) xs') ≤ length xs'"
        by simp
      then have "length (y' # filter (λy. ¬ y ⊆ x) xs') ≤ length xs' + 1"
        by simp
      then have "length (y' # filter (λy. ¬ y ⊆ x) xs') ≤ length xss'" 
        unfolding ‹length (y'#xs') = length xss'›[symmetric] by simp
      then have "length (y' # filter (λy. ¬ y ⊆ x) xs') < length xss" 
        unfolding Cons by auto


      have "remove_subsets (x#xss') = remove_subsets (y'# (filter (λ y . ¬(y ⊆ x)) xs'))"
        using * by auto
      then have "set (remove_subsets (x#xss')) = {xs ∈ set (y' # filter (λy. ¬ y ⊆ x) xs'). ∄xs'a. xs'a ∈ set (y' # filter (λy. ¬ y ⊆ x) xs') ∧ xs ⊂ xs'a}"
        using less[OF ‹length (y' # filter (λy. ¬ y ⊆ x) xs') < length xss›]
        by auto
      also have "… = {xs . xs ∈ set (x#xss') ∧ (∄ xs' . xs' ∈ set (x#xss') ∧ xs ⊂ xs')}"
      proof -
        have "⋀ xs . xs ∈ {xs ∈ set (y' # filter (λy. ¬ y ⊆ x) xs'). ∄xs'a. xs'a ∈ set (y' # filter (λy. ¬ y ⊆ x) xs') ∧ xs ⊂ xs'a} 
                ⟹ xs ∈ {xs ∈ set (x # xss'). ∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'}"
        proof -
          fix xs assume "xs ∈ {xs ∈ set (y' # filter (λy. ¬ y ⊆ x) xs'). ∄xs'a. xs'a ∈ set (y' # filter (λy. ¬ y ⊆ x) xs') ∧ xs ⊂ xs'a}"
          then have "xs ∈ set (y' # filter (λy. ¬ y ⊆ x) xs')" and "∄xs'a. xs'a ∈ set (y' # filter (λy. ¬ y ⊆ x) xs') ∧ xs ⊂ xs'a"
            by blast+

          have "xs ∈ set (x # xss')"
            using ‹xs ∈ set (y' # filter (λy. ¬ y ⊆ x) xs')› find_remove_set(2,3)[OF *]
            by auto 
          moreover have "∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'"
            using ‹∄xs'a. xs'a ∈ set (y' # filter (λy. ¬ y ⊆ x) xs') ∧ xs ⊂ xs'a› find_remove_set[OF *]
            by (metis dual_order.strict_trans filter_list_set in_set_remove1 list.set_intros(1) list.set_intros(2) psubsetI set_ConsD)
          ultimately show "xs ∈ {xs ∈ set (x # xss'). ∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'}" 
            by blast
        qed
        moreover have "⋀ xs . xs ∈ {xs ∈ set (x # xss'). ∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'} 
                ⟹ xs ∈ {xs ∈ set (y' # filter (λy. ¬ y ⊆ x) xs'). ∄xs'a. xs'a ∈ set (y' # filter (λy. ¬ y ⊆ x) xs') ∧ xs ⊂ xs'a}" 
        proof -
          fix xs assume "xs ∈ {xs ∈ set (x # xss'). ∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'}"
          then have "xs ∈ set (x # xss')" and  "∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'"
            by blast+

          then have "xs ∈ set (y' # filter (λy. ¬ y ⊆ x) xs')"
            using find_remove_set[OF *]
            by (metis filter_list_set in_set_remove1 list.set_intros(1) list.set_intros(2) psubsetI set_ConsD) 
          moreover have "∄xs'a. xs'a ∈ set (y' # filter (λy. ¬ y ⊆ x) xs') ∧ xs ⊂ xs'a"
            using ‹xs ∈ set (x # xss')› ‹∄xs'. xs' ∈ set (x # xss') ∧ xs ⊂ xs'› find_remove_set[OF *]
            by (metis filter_is_subset list.set_intros(2) notin_set_remove1 set_ConsD subset_iff)
          ultimately show "xs ∈ {xs ∈ set (y' # filter (λy. ¬ y ⊆ x) xs'). ∄xs'a. xs'a ∈ set (y' # filter (λy. ¬ y ⊆ x) xs') ∧ xs ⊂ xs'a}"
            by blast
        qed
        ultimately show ?thesis by blast
      qed
      finally show ?thesis unfolding Cons by assumption
    qed
  qed
qed

subsection ‹Linear Order on Sum›

instantiation sum :: (ord,ord) ord
begin

fun less_eq_sum ::  "'a + 'b ⇒ 'a + 'b ⇒ bool" where
  "less_eq_sum (Inl a) (Inl b) = (a ≤ b)" |
  "less_eq_sum (Inl a) (Inr b) = True" |
  "less_eq_sum (Inr a) (Inl b) = False" |
  "less_eq_sum (Inr a) (Inr b) = (a ≤ b)"

fun less_sum ::  "'a + 'b ⇒ 'a + 'b ⇒ bool" where
  "less_sum a b = (a ≤ b ∧ a ≠ b)"

instance by (intro_classes)
end


instantiation sum :: (linorder,linorder) linorder
begin

lemma less_le_not_le_sum :
  fixes x :: "'a + 'b"
  and   y :: "'a + 'b"
shows "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"  
  by (cases x; cases y; auto)
    
lemma order_refl_sum :
  fixes x :: "'a + 'b"
  shows "x ≤ x" 
  by (cases x; auto)

lemma order_trans_sum :
  fixes x :: "'a + 'b"
  fixes y :: "'a + 'b"
  fixes z :: "'a + 'b"
  shows "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
  by (cases x; cases y; cases z; auto)  

lemma antisym_sum :
  fixes x :: "'a + 'b"
  fixes y :: "'a + 'b"
  shows "x ≤ y ⟹ y ≤ x ⟹ x = y"
  by (cases x; cases y; auto)

lemma linear_sum :
  fixes x :: "'a + 'b"
  fixes y :: "'a + 'b"
  shows "x ≤ y ∨ y ≤ x"
  by (cases x; cases y; auto) 


instance 
  using less_le_not_le_sum order_refl_sum order_trans_sum antisym_sum linear_sum
  by (intro_classes; metis+)
end


subsection ‹Removing Proper Prefixes›

definition remove_proper_prefixes :: "'a list set ⇒ 'a list set" where
  "remove_proper_prefixes xs = {x . x ∈ xs ∧ (∄ x' . x' ≠ [] ∧ x@x' ∈ xs)}"

lemma remove_proper_prefixes_code[code] :
  "remove_proper_prefixes (set xs) = set (filter (λx . (∀ y ∈ set xs . is_prefix x y ⟶ x = y)) xs)"
proof -
  
  have *: "remove_proper_prefixes (set xs) = Set.filter (λ zs . ∄ys . ys ≠ [] ∧ zs @ ys ∈ (set xs)) (set xs)"
    unfolding remove_proper_prefixes_def by force

  have "⋀ zs . (∄ys . ys ≠ [] ∧ zs @ ys ∈ (set xs)) = (∀ ys ∈ set xs . is_prefix zs ys ⟶ zs = ys)"
    unfolding is_prefix_prefix by auto
  
  then show ?thesis
    unfolding * filter_set by auto
qed


subsection ‹Underspecified List Representations of Sets›

definition as_list_helper :: "'a set ⇒ 'a list" where
  "as_list_helper X = (SOME xs . set xs = X ∧ distinct xs)"

lemma as_list_helper_props :
  assumes "finite X"
  shows "set (as_list_helper X) = X"
    and "distinct (as_list_helper X)"
  using finite_distinct_list[OF assms]
  using someI[of "λ xs . set xs = X ∧ distinct xs"]
  by (metis as_list_helper_def)+


subsection ‹Assigning indices to elements of a finite set›

fun assign_indices :: "('a :: linorder) set ⇒ ('a ⇒ nat)" where
  "assign_indices xs = (λ x . the (find_index ((=)x) (sorted_list_of_set xs)))"

lemma assign_indices_bij:
  assumes "finite xs"
  shows "bij_betw (assign_indices xs) xs {..<card xs}"
proof -

  have *:"set (sorted_list_of_set xs) = xs"
    by (simp add: assms)
  

  have "⋀x y . x∈xs ⟹ y∈xs ⟹ assign_indices xs x = assign_indices xs y ⟹ x = y"
  proof -
    fix x y assume "x∈xs" and "y∈xs" and "assign_indices xs x = assign_indices xs y"

    obtain i where "find_index ((=)x) (sorted_list_of_set xs) = Some i"
      using find_index_exhaustive[of "sorted_list_of_set xs" "((=) x)"]
      using ‹x∈xs› unfolding *
      by blast
    then have "assign_indices xs x = i"
      by auto

    obtain j where "find_index ((=)y) (sorted_list_of_set xs) = Some j"
      using find_index_exhaustive[of "sorted_list_of_set xs" "((=) y)"]
      using ‹y∈xs› unfolding *
      by blast
    then have "assign_indices xs y = j"
      by auto
    then have "i = j"
      using ‹assign_indices xs x = assign_indices xs y› ‹assign_indices xs x = i›
      by auto
    then have "find_index ((=)y) (sorted_list_of_set xs) = Some i"
      using ‹find_index ((=)y) (sorted_list_of_set xs) = Some j›
      by auto

    show "x = y"
      using find_index_index(2)[OF ‹find_index ((=)x) (sorted_list_of_set xs) = Some i›]
      using find_index_index(2)[OF ‹find_index ((=)y) (sorted_list_of_set xs) = Some i›]
      by auto
  qed
  moreover have "(assign_indices xs) ` xs = {..<card xs}"
  proof 
    show "assign_indices xs ` xs ⊆ {..<card xs}"
    proof 
      fix i assume "i ∈ assign_indices xs ` xs"
      then obtain x where "x ∈ xs" and "i = assign_indices xs x"
        by blast
      moreover obtain j where "find_index ((=)x) (sorted_list_of_set xs) = Some j"
        using find_index_exhaustive[of "sorted_list_of_set xs" "((=) x)"]
        using ‹x∈xs› unfolding *
        by blast
      ultimately have "find_index ((=)x) (sorted_list_of_set xs) = Some i"
        by auto
      show "i ∈ {..<card xs}"
        using find_index_index(1)[OF ‹find_index ((=)x) (sorted_list_of_set xs) = Some i›] 
        by auto
    qed
    show "{..<card xs} ⊆ assign_indices xs ` xs"
    proof 
      fix i assume "i ∈ {..<card xs}"
      then have "i < length (sorted_list_of_set xs)"
        by auto
      then have "sorted_list_of_set xs ! i ∈ xs"
        using "*" nth_mem by blast
      then obtain j where "find_index ((=) (sorted_list_of_set xs ! i)) (sorted_list_of_set xs) = Some j"
        using find_index_exhaustive[of "sorted_list_of_set xs" "((=) (sorted_list_of_set xs ! i))"]
        unfolding *
        by blast
      have "i = j"
        using find_index_index(1,2)[OF ‹find_index ((=) (sorted_list_of_set xs ! i)) (sorted_list_of_set xs) = Some j›]
        using ‹i < length (sorted_list_of_set xs)› distinct_sorted_list_of_set nth_eq_iff_index_eq by blast 
      then show "i ∈ assign_indices xs ` xs"
        using ‹find_index ((=) (sorted_list_of_set xs ! i)) (sorted_list_of_set xs) = Some j›
        by (metis ‹sorted_list_of_set xs ! i ∈ xs› assign_indices.elims image_iff option.sel)
    qed
  qed
  ultimately show ?thesis
    unfolding bij_betw_def inj_on_def by blast
qed


subsection ‹Other Lemmata›

lemma foldr_elem_check: 
  assumes "list.set xs ⊆ A"
  shows "foldr (λ x y . if x ∉ A then y else f x y) xs v = foldr f xs v"
  using assms by (induction xs; auto)

lemma foldl_elem_check: 
  assumes "list.set xs ⊆ A"
  shows "foldl (λ y x . if x ∉ A then y else f y x) v xs = foldl f v xs"
  using assms by (induction xs rule: rev_induct; auto)

lemma foldr_length_helper :
  assumes "length xs = length ys"
  shows "foldr (λ_ x . f x) xs b = foldr (λa x . f x) ys b"
  using assms by (induction xs ys rule: list_induct2; auto)

lemma list_append_subset3 : "set xs1 ⊆ set ys1 ⟹ set xs2 ⊆ set ys2 ⟹ set xs3 ⊆ set ys3 ⟹ set (xs1@xs2@xs3) ⊆ set(ys1@ys2@ys3)" by auto

lemma subset_filter : "set xs ⊆ set ys ⟹ set xs = set (filter (λ x . x ∈ set xs) ys)"
  by auto

lemma map_filter_elem :
  assumes "y ∈ set (List.map_filter f xs)"
  obtains x where "x ∈ set xs" 
              and "f x = Some y"
  using assms unfolding List.map_filter_def
  by auto 

lemma filter_length_weakening :
  assumes "⋀ q . f1 q ⟹ f2 q"
  shows "length (filter f1 p) ≤ length (filter f2 p)"
proof (induction p)
  case Nil
  then show ?case by auto
next
  case (Cons a p)
  then show ?case using assms by (cases "f1 a"; auto)
qed

lemma max_length_elem :
  fixes xs :: "'a list set"
  assumes "finite xs"
  and     "xs ≠ {}"
shows "∃ x ∈ xs . ¬(∃ y ∈ xs . length y > length x)" 
using assms proof (induction xs)
  case empty
  then show ?case by auto
next
  case (insert x F)
  then show ?case proof (cases "F = {}")
    case True
    then show ?thesis by blast
  next
    case False
    then obtain y where "y ∈ F" and "¬(∃ y' ∈ F . length y' > length y)"
      using insert.IH by blast
    then show ?thesis using dual_order.strict_trans by (cases "length x > length y"; auto)
  qed
qed

lemma min_length_elem :
  fixes xs :: "'a list set"
  assumes "finite xs"
  and     "xs ≠ {}"
shows "∃ x ∈ xs . ¬(∃ y ∈ xs . length y < length x)" 
using assms proof (induction xs)
  case empty
  then show ?case by auto
next
  case (insert x F)
  then show ?case proof (cases "F = {}")
    case True
    then show ?thesis by blast
  next
    case False
    then obtain y where "y ∈ F" and "¬(∃ y' ∈ F . length y' < length y)"
      using insert.IH by blast
    then show ?thesis using dual_order.strict_trans by (cases "length x < length y"; auto)
  qed
qed

lemma list_property_from_index_property :
  assumes "⋀ i . i < length xs ⟹ P (xs ! i)"
  shows "⋀ x . x ∈ set xs ⟹ P x"
  by (metis assms in_set_conv_nth) 

lemma list_distinct_prefix :
  assumes "⋀ i . i < length xs ⟹ xs ! i ∉ set (take i xs)"
  shows "distinct xs"
proof -
  have "⋀ j . distinct (take j xs)"
  proof -
    fix j 
    show "distinct (take j xs)"
    proof (induction j)
      case 0
      then show ?case by auto
    next
      case (Suc j)
      then show ?case proof (cases "Suc j ≤ length xs")
        case True
        then have "take (Suc j) xs = (take j xs) @ [xs ! j]"
          by (simp add: Suc_le_eq take_Suc_conv_app_nth)
        then show ?thesis using Suc.IH assms[of j] True by auto
      next
        case False
        then have "take (Suc j) xs = take j xs" by auto
        then show ?thesis using Suc.IH by auto
      qed
    qed 
  qed
  then have "distinct (take (length xs) xs)"
    by blast
  then show ?thesis by auto 
qed


lemma concat_pair_set :
  "set (concat (map (λx. map (Pair x) ys) xs)) = {xy . fst xy ∈ set xs ∧ snd xy ∈ set ys}"
  by auto

lemma list_set_sym :
  "set (x@y) = set (y@x)" by auto



lemma list_contains_last_take :
  assumes "x ∈ set xs"
  shows "∃ i . 0 < i ∧ i ≤ length xs ∧ last (take i xs) = x"
  by (metis Suc_leI assms hd_drop_conv_nth in_set_conv_nth last_snoc take_hd_drop zero_less_Suc)
  
lemma take_last_index :
  assumes "i < length xs"
  shows "last (take (Suc i) xs) = xs ! i"
  by (simp add: assms take_Suc_conv_app_nth)

lemma integer_singleton_least :
  assumes "{x . P x} = {a::integer}"
  shows "a = (LEAST x . P x)"
  by (metis Collect_empty_eq Least_equality assms insert_not_empty mem_Collect_eq order_refl singletonD)


lemma sort_list_split :
  "∀ x ∈ set (take i (sort xs)) . ∀ y ∈ set (drop i (sort xs)) . x ≤ y"
  using sorted_append by fastforce


lemma set_map_subset :
  assumes "x ∈ set xs"
  and     "t ∈ set (map f [x])"
shows "t ∈ set (map f xs)"
  using assms by auto

lemma rev_induct2[consumes 1, case_names Nil snoc]: 
  assumes "length xs = length ys" 
      and "P [] []"
      and "(⋀x xs y ys. length xs = length ys ⟹ P xs ys ⟹ P (xs@[x]) (ys@[y]))"
    shows "P xs ys"
using assms proof (induct xs arbitrary: ys rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc x xs)
  then show ?case proof (cases ys)
    case Nil
    then show ?thesis
      using snoc.prems(1) by auto 
  next
    case (Cons a list)
    then show ?thesis
      by (metis append_butlast_last_id diff_Suc_1 length_append_singleton list.distinct(1) snoc.hyps snoc.prems) 
  qed
qed

lemma finite_set_min_param_ex :
  assumes "finite XS"
  and     "⋀ x . x ∈ XS ⟹ ∃ k . ∀ k' . k ≤ k' ⟶ P x k'"
shows "∃ (k::nat) . ∀ x ∈ XS . P x k"
proof -
  obtain f where f_def : "⋀ x . x ∈ XS ⟹ ∀ k' . (f x) ≤ k' ⟶ P x k'"
    using assms(2) by meson
  let ?k = "Max (image f XS)"
  have "∀ x ∈ XS . P x ?k"
    using f_def by (simp add: assms(1)) 
  then show ?thesis by blast
qed

fun list_max :: "nat list ⇒ nat" where
  "list_max [] = 0" |
  "list_max xs = Max (set xs)"

lemma list_max_is_max : "q ∈ set xs ⟹ q ≤ list_max xs"
  by (metis List.finite_set Max_ge length_greater_0_conv length_pos_if_in_set list_max.elims) 

lemma list_prefix_subset : "∃ ys . ts = xs@ys ⟹ set xs ⊆ set ts" by auto
lemma list_map_set_prop : "x ∈ set (map f xs) ⟹ ∀ y . P (f y) ⟹ P x" by auto
lemma list_concat_non_elem : "x ∉ set xs ⟹ x ∉ set ys ⟹ x ∉ set (xs@ys)" by auto
lemma list_prefix_elem : "x ∈ set (xs@ys) ⟹ x ∉ set ys ⟹ x ∈ set xs" by auto
lemma list_map_source_elem : "x ∈ set (map f xs) ⟹ ∃ x' ∈ set xs . x = f x'" by auto


lemma maximal_set_cover : 
  fixes X :: "'a set set"
  assumes "finite X" 
  and     "S ∈ X"  
shows "∃ S' ∈ X . S ⊆ S' ∧ (∀ S'' ∈ X . ¬(S' ⊂ S''))"
proof (rule ccontr)
  assume "¬ (∃S'∈X. S ⊆ S' ∧ (∀S''∈X. ¬ S' ⊂ S''))"
  then have *: "⋀ T . T ∈ X ⟹ S ⊆ T ⟹ ∃ T' ∈ X . T ⊂ T'"
    by auto

  have "⋀ k . ∃ ss . (length ss = Suc k) ∧ (hd ss = S) ∧ (∀ i < k . ss ! i ⊂ ss ! (Suc i)) ∧ (set ss ⊆ X)"
  proof -
    fix k show "∃ ss . (length ss = Suc k) ∧ (hd ss = S) ∧ (∀ i < k . ss ! i ⊂ ss ! (Suc i)) ∧ (set ss ⊆ X)"
    proof (induction k)
      case 0
      have "length [S] = Suc 0 ∧ hd [S] = S ∧ (∀ i < 0 . [S] ! i ⊂ [S] ! (Suc i)) ∧ (set [S] ⊆ X)" using assms(2) by auto
      then show ?case by blast
    next
      case (Suc k)
      then obtain ss where "length ss = Suc k" 
                       and "hd ss = S" 
                       and "(∀i<k. ss ! i ⊂ ss ! Suc i)" 
                       and "set ss ⊆ X"
        by blast
      then have "ss ! k ∈ X"
        by auto
      moreover have "S ⊆ (ss ! k)"
      proof -
        have "⋀ i . i < Suc k ⟹ S ⊆ (ss ! i)"
        proof -
          fix i assume "i < Suc k"
          then show "S ⊆ (ss ! i)"
          proof (induction i)
            case 0
            then show ?case using ‹hd ss = S› ‹length ss = Suc k›
              by (metis hd_conv_nth list.size(3) nat.distinct(1) order_refl) 
          next
            case (Suc i)
            then have "S ⊆ ss ! i" and "i < k" by auto
            then have "ss ! i ⊂ ss ! Suc i" using ‹(∀i<k. ss ! i ⊂ ss ! Suc i)› by blast
            then show ?case using ‹S ⊆ ss ! i› by auto
          qed
        qed
        then show ?thesis using ‹length ss = Suc k› by auto 
      qed
      ultimately obtain T' where "T' ∈ X" and "ss ! k ⊂ T'"
        using * by meson 

      let ?ss = "ss@[T']"

      have "length ?ss = Suc (Suc k)" 
        using ‹length ss = Suc k› by auto
      moreover have "hd ?ss = S" 
        using ‹hd ss = S› by (metis ‹length ss = Suc k› hd_append list.size(3) nat.distinct(1)) 
      moreover have "(∀i < Suc k. ?ss ! i ⊂ ?ss ! Suc i)" 
        using ‹(∀i<k. ss ! i ⊂ ss ! Suc i)› ‹ss ! k ⊂ T'› 
        by (metis Suc_lessI ‹length ss = Suc k› diff_Suc_1 less_SucE nth_append nth_append_length) 
      moreover have "set ?ss ⊆ X" 
        using ‹set ss ⊆ X› ‹T' ∈ X› by auto
      ultimately show ?case by blast
    qed
  qed

  then obtain ss where "(length ss = Suc (card X))"
                   and "(hd ss = S)" 
                   and "(∀ i < card X . ss ! i ⊂ ss ! (Suc i))" 
                   and "(set ss ⊆ X)" 
    by blast
  then have "(∀ i < length ss - 1 . ss ! i ⊂ ss ! (Suc i))"
    by auto

  have **: "⋀ i (ss :: 'a set list) . (∀ i < length ss - 1 . ss ! i ⊂ ss ! (Suc i)) ⟹ i < length ss  ⟹ ∀ s ∈ set (take i ss) . s ⊂ ss ! i"
  proof -
    fix i 
    fix ss :: "'a set list"
    assume "i < length ss " and "(∀ i < length ss - 1 . ss ! i ⊂ ss ! (Suc i))"
    then show "∀ s ∈ set (take i ss) . s ⊂ ss ! i"
    proof (induction i)
      case 0
      then show ?case by auto
    next
      case (Suc i)
      then have "∀s∈set (take i ss). s ⊂ ss ! i" by auto
      then have "∀s∈set (take i ss). s ⊂ ss ! (Suc i)" using Suc.prems
        by (metis One_nat_def Suc_diff_Suc Suc_lessE diff_zero dual_order.strict_trans nat.inject zero_less_Suc) 
      moreover have "ss ! i ⊂ ss ! (Suc i)" using Suc.prems by auto
      moreover have "(take (Suc i) ss) = (take i ss)@[ss ! i]" using Suc.prems(1)
        by (simp add: take_Suc_conv_app_nth)
      ultimately show ?case by auto 
    qed
  qed

  have "distinct ss"
    using ‹(∀ i < length ss - 1 . ss ! i ⊂ ss ! (Suc i))›
  proof (induction ss rule: rev_induct)
    case Nil
    then show ?case by auto
  next
    case (snoc a ss)
    from snoc.prems have "∀i<length ss - 1. ss ! i ⊂ ss ! Suc i"
      by (metis Suc_lessD diff_Suc_1 diff_Suc_eq_diff_pred length_append_singleton nth_append zero_less_diff) 
    then have "distinct ss"
      using snoc.IH by auto
    moreover have "a ∉ set ss"
      using **[OF snoc.prems, of "length (ss @ [a]) - 1"] by auto
    ultimately show ?case by auto
  qed

  then have "card (set ss) = Suc (card X)"
    using ‹(length ss = Suc (card X))› by (simp add: distinct_card) 
  then show "False"
    using ‹set ss ⊆ X› ‹finite X› by (metis Suc_n_not_le_n card_mono) 
qed



lemma map_set : 
  assumes "x ∈ set xs"
  shows "f x ∈ set (map f xs)" using assms by auto


lemma maximal_distinct_prefix :
  assumes "¬ distinct xs"
  obtains n where "distinct (take (Suc n) xs)"
            and   "¬ (distinct (take (Suc (Suc n)) xs))"
using assms proof (induction xs rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc x xs)
  
  show ?case proof (cases "distinct xs")
    case True
    then have "distinct (take (length xs) (xs@[x]))" by auto
    moreover have"¬ (distinct (take (Suc (length xs)) (xs@[x])))" using snoc.prems(2) by auto
    ultimately show ?thesis using that by (metis Suc_pred distinct_singleton length_greater_0_conv self_append_conv2 snoc.prems(1) snoc.prems(2))
  next
    case False
    
    then show ?thesis using snoc.IH that
      by (metis Suc_mono butlast_snoc length_append_singleton less_SucI linorder_not_le snoc.prems(1) take_all take_butlast) 
  qed
qed 


lemma distinct_not_in_prefix :
  assumes "⋀ i . (⋀ x . x ∈ set (take i xs) ⟹ xs ! i ≠ x)"
  shows "distinct xs"
  using assms list_distinct_prefix by blast 


lemma list_index_fun_gt : "⋀ xs (f::'a ⇒ nat) i j . 
                              (⋀ i . Suc i < length xs ⟹ f (xs ! i) > f (xs ! (Suc i))) 
                              ⟹ j < i 
                              ⟹ i < length xs 
                              ⟹ f (xs ! j) > f (xs ! i)"
proof -
  fix xs::"'a list" 
  fix f::"'a ⇒ nat" 
  fix i j 
  assume "(⋀ i . Suc i < length xs ⟹ f (xs ! i) > f (xs ! (Suc i)))"
     and "j < i"
     and "i < length xs"
  then show "f (xs ! j) > f (xs ! i)"
  proof (induction "i - j" arbitrary: i j)
    case 0
    then show ?case by auto
  next
    case (Suc x)
    then show ?case
    proof -
      have f1: "∀n. ¬ Suc n < length xs ∨ f (xs ! Suc n) < f (xs ! n)"
        using Suc.prems(1) by presburger
      have f2: "∀n na. ¬ n < na ∨ Suc n ≤ na"
        using Suc_leI by satx
      have "x = i - Suc j"
        by (metis Suc.hyps(2) Suc.prems(2) Suc_diff_Suc nat.simps(1))
      then have "¬ Suc j < i ∨ f (xs ! i) < f (xs ! Suc j)"
        using f1 Suc.hyps(1) Suc.prems(3) by blast
      then show ?thesis
        using f2 f1 by (metis Suc.prems(2) Suc.prems(3) leI le_less_trans not_less_iff_gr_or_eq)
    qed 
  qed
qed

lemma finite_set_elem_maximal_extension_ex :
  assumes "xs ∈ S"
  and     "finite S"
shows "∃ ys . xs@ys ∈ S ∧ ¬ (∃ zs . zs ≠ [] ∧ xs@ys@zs ∈ S)"
using ‹finite S› ‹xs ∈ S› proof (induction S arbitrary: xs)
  case empty
  then show ?case by auto
next
  case (insert x S)

  consider (a) "∃ ys . x = xs@ys ∧ ¬ (∃ zs . zs ≠ [] ∧ xs@ys@zs ∈ (insert x S))" |
           (b) "¬(∃ ys . x = xs@ys ∧ ¬ (∃ zs . zs ≠ [] ∧ xs@ys@zs ∈ (insert x S)))"
    by blast
  then show ?case proof cases
    case a
    then show ?thesis by auto
  next
    case b
    then show ?thesis proof (cases "∃ vs . vs ≠ [] ∧ xs@vs ∈ S")
      case True
      then obtain vs where "vs ≠ []" and "xs@vs ∈ S"
        by blast
      
      have "∃ys. xs @ (vs @ ys) ∈ S ∧ (∄zs. zs ≠ [] ∧ xs @ (vs @ ys) @ zs ∈ S)"
        using insert.IH[OF ‹xs@vs ∈ S›] by auto
      then have "∃ys. xs @ (vs @ ys) ∈ S ∧ (∄zs. zs ≠ [] ∧ xs @ (vs @ ys) @ zs ∈ (insert x S))"
        using b 
        unfolding append.assoc append_is_Nil_conv append_self_conv insert_iff
        by (metis append.assoc append_Nil2 append_is_Nil_conv same_append_eq) 
      then show ?thesis by blast
    next
      case False
      then show ?thesis using insert.prems
        by (metis append_is_Nil_conv append_self_conv insertE same_append_eq) 
    qed
  qed
qed


lemma list_index_split_set: 
  assumes "i < length xs"
shows "set xs = set ((xs ! i) # ((take i xs) @ (drop (Suc i) xs)))"  
using assms proof (induction xs arbitrary: i)
  case Nil
  then show ?case by auto
next
  case (Cons x xs)
  then show ?case proof (cases i)
    case 0
    then show ?thesis by auto
  next
    case (Suc j)
    then have "j < length xs" using Cons.prems by auto
    then have "set xs = set ((xs ! j) # ((take j xs) @ (drop (Suc j) xs)))" using Cons.IH[of j] by blast
    
    have *: "take (Suc j) (x#xs) = x#(take j xs)" by auto
    have **: "drop (Suc (Suc j)) (x#xs) = (drop (Suc j) xs)" by auto
    have ***: "(x # xs) ! Suc j = xs ! j" by auto
    
    show ?thesis
      using ‹set xs = set ((xs ! j) # ((take j xs) @ (drop (Suc j) xs)))›
      unfolding Suc * ** *** by auto
  qed
qed


lemma max_by_foldr :
  assumes "x ∈ set xs"
  shows "f x < Suc (foldr (λ x' m . max (f x') m) xs 0)"
  using assms by (induction xs; auto)

lemma Max_elem : "finite (xs :: 'a set) ⟹ xs ≠ {} ⟹ ∃ x ∈ xs . Max (image (f :: 'a ⇒ nat) xs) = f x"
  by (metis (mono_tags, opaque_lifting) Max_in empty_is_image finite_imageI imageE)


lemma card_union_of_singletons :
  assumes "⋀ S . S ∈ SS ⟹ (∃ t . S = {t})"
shows "card (⋃ SS) = card SS"
proof -
  let ?f = "λ x . {x}"
  have "bij_betw ?f (⋃ SS) SS" 
    unfolding bij_betw_def inj_on_def using assms by fastforce
  then show ?thesis 
    using bij_betw_same_card by blast 
qed

lemma card_union_of_distinct :
  assumes "⋀ S1 S2 . S1 ∈ SS ⟹ S2 ∈ SS ⟹ S1 = S2 ∨ f S1 ∩ f S2 = {}"
  and     "finite SS"
  and     "⋀ S . S ∈ SS ⟹ f S ≠ {}"
shows "card (image f SS) = card SS" 
proof -
  from assms(2) have "∀ S1 ∈ SS . ∀ S2 ∈ SS . S1 = S2 ∨ f S1 ∩ f S2 = {} 
                      ⟹ ∀ S ∈ SS . f S ≠ {} ⟹ ?thesis"
  proof (induction SS)
    case empty
    then show ?case by auto
  next
    case (insert x F)
    then have "¬ (∃ y ∈ F . f y = f x)" 
      by auto
    then have "f x ∉ image f F" 
      by auto
    then have "card (image f (insert x F)) = Suc (card (image f F))" 
      using insert by auto
    moreover have "card (f ` F) = card F" 
      using insert by auto
    moreover have "card (insert x F) = Suc (card F)" 
      using insert by auto
    ultimately show ?case 
      by simp
  qed
  then show ?thesis 
    using assms by simp
qed


lemma take_le :
  assumes "i ≤ length xs"
  shows "take i (xs@ys) = take i xs"
  by (simp add: assms less_imp_le_nat)


lemma butlast_take_le :
  assumes "i ≤ length (butlast xs)" 
  shows "take i (butlast xs) = take i xs" 
  using take_le[OF assms, of "[last xs]"]
  by (metis append_butlast_last_id butlast.simps(1)) 


lemma distinct_union_union_card :
  assumes "finite xs"
  and     "⋀ x1 x2 y1 y2 . x1 ≠ x2 ⟹ x1 ∈ xs ⟹ x2 ∈ xs ⟹ y1 ∈ f x1 ⟹ y2 ∈ f x2 ⟹ g y1 ∩ g y2 = {}"
  and     "⋀ x1 y1 y2 . y1 ∈ f x1 ⟹ y2 ∈ f x1 ⟹ y1 ≠ y2 ⟹ g y1 ∩ g y2 = {}"
  and     "⋀ x1 . finite (f x1)"
  and     "⋀ y1 . finite (g y1)"
  and     "⋀ y1 . g y1 ⊆ zs"
  and     "finite zs"
shows "(∑ x ∈ xs . card (⋃ y ∈ f x . g y)) ≤ card zs" 
proof -
  have "(∑ x ∈ xs . card (⋃ y ∈ f x . g y)) = card (⋃ x ∈ xs . (⋃ y ∈ f x . g y))"
    using assms(1,2) proof induction
    case empty
    then show ?case by auto
  next
    case (insert x xs)
    then have "(⋀x1 x2. x1 ∈ xs ⟹ x2 ∈ xs ⟹ x1 ≠ x2 ⟹ ⋃ (g ` f x1) ∩ ⋃ (g ` f x2) = {})" and "x ∈ insert x xs" by blast+
    then have "(∑x∈xs. card (⋃ (g ` f x))) = card (⋃x∈xs. ⋃ (g ` f x))" using insert.IH by blast

    moreover have "(∑x∈(insert x xs). card (⋃ (g ` f x))) = (∑x∈xs. card (⋃ (g ` f x))) + card (⋃ (g ` f x))"
      using insert.hyps by auto

    moreover have "card (⋃x∈(insert x xs). ⋃ (g ` f x)) = card (⋃x∈xs. ⋃ (g ` f x)) + card (⋃ (g ` f x))"
    proof -
      have "((⋃x∈xs. ⋃ (g ` f x)) ∪ ⋃ (g ` f x)) = (⋃x∈(insert x xs). ⋃ (g ` f x))"
        by blast

      have *: "(⋃x∈xs. ⋃ (g ` f x)) ∩ (⋃ (g ` f x)) = {}"
      proof (rule ccontr)
        assume "(⋃x∈xs. ⋃ (g ` f x)) ∩ ⋃ (g ` f x) ≠ {}"
        then obtain z where "z ∈ ⋃ (g ` f x)" and "z ∈ (⋃x∈xs. ⋃ (g ` f x))" by blast
        then obtain x' where "x' ∈ xs" and "z ∈ ⋃ (g ` f x')" by blast
        then have "x' ≠ x" and "x' ∈ insert x xs" using insert.hyps by blast+

        have "⋃ (g ` f x') ∩ ⋃ (g ` f x) = {}"
          using insert.prems[OF ‹x' ≠ x› ‹x' ∈ insert x xs› ‹x ∈ insert x xs› ]
          by blast 
        then show "False"
          using ‹z ∈ ⋃ (g ` f x')› ‹z ∈ ⋃ (g ` f x)› by blast
      qed
      have **: "finite (⋃ (g ` f x))"
        using assms(4) assms(5) by blast 
      have ***: "finite (⋃x∈xs. ⋃ (g ` f x))"
        by (simp add: assms(4) assms(5) insert.hyps(1))

      have "card ((⋃x∈xs. ⋃ (g ` f x)) ∪ ⋃ (g ` f x)) = card (⋃x∈xs. ⋃ (g ` f x)) + card (⋃ (g ` f x))" 
        using card_Un_disjoint[OF *** ** *] by simp

      
      then show ?thesis 
        unfolding ‹((⋃x∈xs. ⋃ (g ` f x)) ∪ ⋃ (g ` f x)) = (⋃x∈(insert x xs). ⋃ (g ` f x))› by assumption
    qed

    ultimately show ?case by linarith
  qed

  moreover have "card (⋃ x ∈ xs . (⋃ y ∈ f x . g y)) ≤ card zs"
  proof -
    have "(⋃ x ∈ xs . (⋃ y ∈ f x . g y)) ⊆ zs"
      using assms(6) by (simp add: UN_least) 
    moreover have "finite (⋃ x ∈ xs . (⋃ y ∈ f x . g y))"
      by (simp add: assms(1) assms(4) assms(5)) 
    ultimately show ?thesis
      using assms(7)
      by (simp add: card_mono) 
  qed

  ultimately show ?thesis
    by linarith 
qed


lemma set_concat_elem :
  assumes "x ∈ set (concat xss)"
  obtains xs where "xs ∈ set xss" and "x ∈ set xs" 
  using assms by auto

lemma set_map_elem :
  assumes "y ∈ set (map f xs)"
  obtains x where "y = f x" and "x ∈ set xs" 
  using assms by auto

lemma finite_snd_helper: 
  assumes "finite xs" 
  shows "finite {z. ((q, p), z) ∈ xs}" 
proof -
  have "{z. ((q, p), z) ∈ xs} ⊆ (λ((a,b),c) . c) ` xs" 
  proof 
    fix x assume "x ∈ {z. ((q, p), z) ∈ xs}"
    then have "((q,p),x) ∈ xs" by auto
    then show "x ∈ (λ((a,b),c) . c) ` xs" by force
  qed
  then show ?thesis using assms
    using finite_surj by blast 
qed

lemma fold_dual : "fold (λ x (a1,a2) . (g1 x a1, g2 x a2)) xs (a1,a2) = (fold g1 xs a1, fold g2 xs a2)"
  by (induction xs arbitrary: a1 a2; auto)

lemma recursion_renaming_helper :
  assumes "f1 = (λx . if P x then x else f1 (Suc x))"
  and     "f2 = (λx . if P x then x else f2 (Suc x))"
  and     "⋀ x . x ≥ k ⟹ P x"
shows "f1 = f2"
proof 
  fix x 
  show "f1 x = f2 x"
  proof (induction "k - x" arbitrary: x)
    case 0
    then have "x ≥ k" 
      by auto
    then show ?case 
      using assms(3) by (simp add: assms(1,2))
  next
    case (Suc k')
    show ?case proof (cases "P x")
      case True
      then show ?thesis by (simp add: assms(1,2))
    next
      case False
      moreover have "f1 (Suc x) = f2 (Suc x)"
        using Suc.hyps(1)[of "Suc x"] Suc.hyps(2) by auto
      ultimately show ?thesis by (simp add: assms(1,2))
    qed
  qed
qed


lemma minimal_fixpoint_helper :
  assumes "f = (λx . if P x then x else f (Suc x))"
  and     "⋀ x . x ≥ k ⟹ P x"
shows "P (f x)"
  and "⋀ x' . x' ≥ x ⟹ x' < f x ⟹ ¬ P x'"
proof -
  have "P (f x) ∧ (∀ x' . x' ≥ x ⟶ x' < f x ⟶ ¬ P x')"
  proof (induction "k-x" arbitrary: x)
    case 0
    then have "P x" 
      using assms(2) by auto
    moreover have "f x = x"
      using calculation by (simp add: assms(1))
    ultimately show ?case 
      using assms(1) by auto  
  next
    case (Suc k')
    then have "P (f (Suc x))" and "⋀ x' . x' ≥ Suc x ⟹ x' < f (Suc x) ⟹ ¬ P x'"
      by force+

    show ?case proof (cases "P x")
      case True
      then have "f x = x"
        by (simp add: assms(1))
      show ?thesis 
        using True unfolding ‹f x = x› by auto
    next
      case False
      then have "f x = f (Suc x)"
        by (simp add: assms(1))
      then have "P (f x)"
        using ‹P (f (Suc x))› by simp
      moreover have "(∀x'≥x. x' < f x ⟶ ¬ P x')"
        using ‹⋀ x' . x' ≥ Suc x ⟹ x' < f (Suc x) ⟹ ¬ P x'› False ‹f x = f (Suc x)›
        by (metis Suc_leI le_neq_implies_less) 
      ultimately show ?thesis
        by blast
    qed
  qed
  then show "P (f x)" and "⋀ x' . x' ≥ x ⟹ x' < f x ⟹ ¬ P x'"
    by blast+
qed

lemma map_set_index_helper :
  assumes "xs ≠ []"
  shows "set (map f xs) = (λi . f (xs ! i)) ` {.. (length xs - 1)}" 
using assms proof (induction xs rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc x xs)
  show ?case proof (cases "xs = []")
    case True
    show ?thesis 
      using snoc.prems unfolding True by auto
  next
    case False    

    have "{..length (xs@[x]) - 1} = insert (length (xs@[x]) - 1) {..length xs - 1}"
      by force
    moreover have "((λi. f ((xs@[x]) ! i)) (length (xs@[x]) - 1)) = f x"
      by auto
    moreover have "((λi. f ((xs@[x]) ! i)) ` {..length xs - 1}) = ((λi. f (xs ! i)) ` {..length xs - 1})"
    proof -
      have "⋀ i . i < length xs ⟹ f ((xs@[x]) ! i) = f (xs ! i)"
        by (simp add: nth_append)
      moreover have "⋀ i . i ∈ {..length xs - 1} ⟹ i < length xs"
        using False
        by (metis Suc_pred' atMost_iff length_greater_0_conv less_Suc_eq_le) 
      ultimately show ?thesis
        by (meson image_cong)
    qed
    ultimately have "(λi. f ((xs@[x]) ! i)) ` {..length (xs@[x]) - 1} = insert (f x) ((λi. f (xs ! i)) ` {..length xs - 1})"
      by auto
    moreover have "set (map f (xs@[x])) = insert (f x) (set (map f xs))"
      by auto
    moreover have "set (map f xs) = (λi. f (xs ! i)) ` {..length xs - 1}"
      using snoc.IH False by auto
    ultimately show ?thesis
      by force
  qed
qed

lemma partition_helper :
  assumes "finite X"
  and     "X ≠ {}"
  and     "⋀ x . x ∈ X ⟹ p x ⊆ X"
  and     "⋀ x . x ∈ X ⟹ p x ≠ {}"
  and     "⋀ x y . x ∈ X ⟹ y ∈ X ⟹ p x = p y ∨ p x ∩ p y = {}"
  and     "(⋃ x ∈ X . p x) = X"
obtains l::nat and p' where
  "p' ` {..l} = p ` X"
  "⋀ i j . i ≤ l ⟹ j ≤ l ⟹ i ≠ j ⟹ p' i ∩ p' j = {}"
  "card (p ` X) = Suc l"
proof -
  let ?P = "as_list_helper ((λx. as_list_helper (p x)) ` X)"


  have "?P ≠ []"
    using assms(1) assms(2)
    by (metis as_list_helper_props(1) finite_imageI image_is_empty set_empty) 

  define l where l: "l = length ?P - 1"
  define p' where p': "p' = (λ x . set (?P ! x))"

  have "finite ((λx. as_list_helper (p x)) ` X)"
    using assms(1)
    by simp 

  have "set ` ((λx. as_list_helper (p x)) ` X) = p ` X"
  proof -
    have "set ` ((λx. as_list_helper (p x)) ` X) = ((λx. set (as_list_helper (p x))) ` X)"
      by auto
    also have "… = p ` X"
      by (metis (no_types, lifting) as_list_helper_props(1) assms(1) assms(6) finite_UN image_cong)
    finally show ?thesis .
  qed
  moreover have "set ?P = (λx. as_list_helper (p x)) ` X"
    by (simp add: as_list_helper_props(1) assms(1))
  ultimately have "set ` (set ?P) = p ` X"
    by auto
  moreover have "(p' ` {..l}) = set (map set ?P)"
    using map_set_index_helper[OF ‹?P ≠ []›]
  proof -
    have "(λn. set (as_list_helper ((λn. as_list_helper (p n)) ` X) ! n)) ` {..l} = p' ` {..l}"
      using p' by force
    then show ?thesis
      by (metis ‹⋀f. set (map f (as_list_helper ((λx. as_list_helper (p x)) ` X))) = (λi. f (as_list_helper ((λx. as_list_helper (p x)) ` X) ! i)) ` {..length (as_list_helper ((λx. as_list_helper (p x)) ` X)) - 1}› l)
  qed
  ultimately have p1: "p' ` {..l} = p ` X"
    by (metis list.set_map)

  moreover have p2: "⋀ i j . i ≤ l ⟹ j ≤ l ⟹ i ≠ j ⟹ p' i ∩ p' j = {}"
  proof -
    fix i j assume "i ≤ l" "j ≤ l" "i ≠ j"
    moreover define PX where PX: "PX = ((λx. as_list_helper (p x)) ` X)"
    ultimately have "i < length (as_list_helper PX)" and "j < length (as_list_helper PX)"
      unfolding l by auto
    then have "?P ! i ≠ ?P ! j"
      using ‹i ≠ j› unfolding PX
      using as_list_helper_props(2)[OF ‹finite ((λx. as_list_helper (p x)) ` X)›]
      using nth_eq_iff_index_eq by blast
    moreover obtain xi where "xi ∈ X" and *:"?P ! i = as_list_helper (p xi)"
      by (metis (no_types, lifting) PX ‹i < length (as_list_helper PX)› ‹set (as_list_helper ((λx. as_list_helper (p x)) ` X)) = (λx. as_list_helper (p x)) ` X› image_iff nth_mem)
    moreover obtain xj where "xj ∈ X" and **:"?P ! j = as_list_helper (p xj)"
      by (metis (no_types, lifting) PX ‹j < length (as_list_helper PX)› ‹set (as_list_helper ((λx. as_list_helper (p x)) ` X)) = (λx. as_list_helper (p x)) ` X› image_iff nth_mem)
    ultimately have "p xi ≠ p xj"
      by metis
    then have "p' i ≠ p' j"
      unfolding p'
      by (metis "*" "**" ‹xi ∈ X› ‹xj ∈ X› as_list_helper_props(1) assms(1) assms(3) infinite_super)
    then show "p' i ∩ p' j = {}"
      using assms(5)
      by (metis "*" "**" ‹xi ∈ X› ‹xj ∈ X› as_list_helper_props(1) assms(1) assms(3) finite_subset p') 
  qed
  moreover have "card (p ` X) = Suc l" 
  proof -
    have "⋀ i . i ∈ {..l} ⟹ p' i ≠ {}"
      using p1 assms (4)
      by (metis imageE imageI) 
    then show ?thesis 
      unfolding p1[symmetric] 
      by (metis atMost_iff card_atMost card_union_of_distinct finite_atMost p2) 
  qed
  ultimately show ?thesis
    using that[of p' l]
    by blast
qed

lemma take_diff :
  assumes "i ≤ length xs"
  and     "j ≤ length xs"
  and     "i ≠ j"
shows "take i xs ≠ take j xs"
  by (metis assms(1) assms(2) assms(3) length_take min.commute min.order_iff)

lemma image_inj_card_helper :
  assumes "finite X"
  and     "⋀ a b . a ∈ X ⟹ b ∈ X ⟹ a ≠ b ⟹ f a ≠ f b"
shows "card (f ` X) = card X"
using assms proof (induction X)
  case empty
  then show ?case by auto
next
  case (insert x X)
  then have "f x ∉ f ` X"
    by (metis imageE insertCI) 
  then have "card (f ` (insert x X)) = Suc (card X)"
    using insert.IH insert.hyps(1) insert.prems by auto
  moreover have "card (insert x X) = Suc (card X)"
    by (meson card_insert_if insert.hyps(1) insert.hyps(2))  
  ultimately show ?case 
    by auto
qed


lemma sum_image_inj_card_helper :
  fixes l :: nat
  assumes "⋀ i . i ≤ l ⟹ finite (I i)"
  and     "⋀ i j . i ≤ l ⟹ j ≤ l ⟹ i ≠ j ⟹ I i ∩ I j = {}"
shows "(∑ i ∈ {..l} . (card (I i))) = card (⋃ i ∈ {..l} . I i)" 
  using assms proof (induction l)
case 0
  then show ?case by auto
next
  case (Suc l)
  then have "(∑i≤l. card (I i)) = card (⋃ (I ` {..l}))"
    using le_Suc_eq by presburger
  moreover have "(∑i≤Suc l. card (I i)) = card (I (Suc l)) + (∑i≤l. card (I i))"
    by auto
  moreover have "card (⋃ (I ` {..Suc l})) = card (I (Suc l)) + card (⋃ (I ` {..l}))"
    using Suc.prems(2)
    by (simp add: Suc.prems(1) card_UN_disjoint) 
  ultimately show ?case 
    by auto
qed

lemma Min_elem : "finite (xs :: 'a set) ⟹ xs ≠ {} ⟹ ∃ x ∈ xs . Min (image (f :: 'a ⇒ nat) xs) = f x"
  by (metis (mono_tags, opaque_lifting) Min_in empty_is_image finite_imageI imageE)

lemma finite_subset_mapping_limit :
  fixes f :: "nat ⇒ 'a set"
  assumes "finite (f 0)"
  and     "⋀ i j . i ≤ j ⟹ f j ⊆ f i"
obtains k where "⋀ k' . k ≤ k' ⟹ f k' = f k"  
proof (cases "f 0 = {}")
  case True
  then show ?thesis
    using assms(2) that by fastforce 
next
  case False
  then have "(f ` UNIV) ≠ {}"
    by auto

  have "∃ k . ∀ k' . k ≤ k' ⟶ f k' = f k"
  proof (rule ccontr)
    assume "∄k. ∀k'≥k. f k' = f k"
    then have "⋀ k . ∃ k' . k' > k ∧ f k' ⊂ f k"
      using assms(2)
      by (metis dual_order.order_iff_strict)

    have "f ` UNIV ⊆ Pow (f 0)"
      using assms(2)
      by (simp add: image_subset_iff) 
    moreover have "finite (Pow (f 0))"
      using assms(1) by simp
    ultimately have "finite (f ` UNIV)"
      using finite_subset by auto


    obtain x where "x ∈ f ` UNIV" and "⋀ x' . x' ∈ f ` UNIV ⟹ card x ≤ card x'"
      using Min_elem[OF ‹finite (f ` UNIV)› ‹(f ` UNIV) ≠ {}›, of card]
      by (metis (mono_tags, lifting) Min.boundedE ‹finite (range f)› ‹range f ≠ {}› ball_imageD finite_imageI image_is_empty order_refl)  

    obtain k where "f k = x"
      using ‹x ∈ f ` UNIV› by blast 
    then obtain k' where "f k' ⊂ x"
      using ‹⋀ k . ∃ k' . k' > k ∧ f k' ⊂ f k› by blast 
    moreover have "⋀ k . finite (f k)"
      by (meson assms(1) assms(2) infinite_super le0) 
    ultimately have "card (f k') < card x"
      using ‹f k = x› by (metis psubset_card_mono)  
    then show "False"
      using ‹⋀ x' . x' ∈ f ` UNIV ⟹ card x ≤ card x'›
      by (simp add: less_le_not_le) 
  qed
  then show ?thesis 
    using that by blast
qed

lemma finite_card_less_witnesses :
  assumes "finite A"
  and     "card (g ` A) < card (f ` A)" 
obtains a b where "a ∈ A" and "b ∈ A" and "f a ≠ f b" and "g a = g b" 
proof -
  have "∃ a b . a ∈ A ∧ b ∈ A ∧ f a ≠ f b ∧ g a = g b"
    using assms proof (induction A)
    case empty
    then show ?case by auto
  next
    case (insert x F)
    show ?case proof (cases "card (g ` F) < card (f ` F)")
      case True
      then show ?thesis using insert.IH by blast
    next
      case False 

      have "finite (g ` F)" and "finite (f ` F)"
        using insert.hyps(1) by auto
      have "card (g ` insert x F) = (if g x ∈ g ` F then card (g ` F) else Suc (card (g ` F)))"
        using card_insert_if[OF ‹finite (g ` F)›]
        by simp 
      moreover have "card (f ` insert x F) = (if f x ∈ f ` F then card (f ` F) else Suc (card (f ` F)))"
        using card_insert_if[OF ‹finite (f ` F)›]
        by simp
      ultimately have "card (g ` F) = card (f ` F)"
        using insert.prems False
        by (metis Suc_lessD not_less_less_Suc_eq) 
      then have "card (g ` insert x F) = card (g ` F)"
        using insert.prems
        by (metis Suc_lessD ‹card (f ` insert x F) = (if f x ∈ f ` F then card (f ` F) else Suc (card (f ` F)))› ‹card (g ` insert x F) = (if g x ∈ g ` F then card (g ` F) else Suc (card (g ` F)))› less_not_refl3) 

      then obtain y where "y ∈ F" and "g x = g y"
        using ‹finite F›
        by (metis ‹card (g ` insert x F) = (if g x ∈ g ` F then card (g ` F) else Suc (card (g ` F)))› imageE lessI less_irrefl_nat)

      have "card (f ` insert x F) > card (f ` F)"
        using ‹card (g ` F) = card (f ` F)› ‹card (g ` insert x F) = card (g ` F)› insert.prems by presburger
      then have "f x ≠ f y"
        using ‹y ∈ F›
        by (metis ‹card (f ` insert x F) = (if f x ∈ f ` F then card (f ` F) else Suc (card (f ` F)))› image_eqI less_irrefl_nat) 

      then show ?thesis
        using ‹y ∈ F› ‹g x = g y› by blast
    qed
  qed
  then show ?thesis
    using that by blast
qed

lemma monotone_function_with_limit_witness_helper :
  fixes f :: "nat ⇒ nat"
  assumes "⋀ i j . i ≤ j ⟹ f i ≤ f j"
  and     "⋀ i j m . i < j ⟹ f i = f j ⟹ j ≤ m ⟹ f i = f m"
  and     "⋀ i . f i ≤ k"
obtains x where "f (Suc x) = f x" and "x ≤ k - f 0"
proof -
  have "⋀ i . f (Suc i) ≥ f 0 + Suc i ∨ (f (Suc i) < f 0 + Suc i ∧ f i = f (Suc i))"
  proof -
    fix i 
    show "f (Suc i) ≥ f 0 + Suc i ∨ (f (Suc i) < f 0 + Suc i ∧ f i = f (Suc i))"
    proof (induction i)
      case 0
      then show ?case using assms(1)
        by (metis add.commute add.left_neutral add_Suc_shift le0 le_antisym lessI not_less_eq_eq) 
    next
      case (Suc i)
      then show ?case
      proof -
        have "∀n. n ≤ Suc n"
          by simp
        then show ?thesis
          by (metis Suc add_Suc_right assms(1) assms(2) le_antisym not_less not_less_eq_eq order_trans_rules(23))
      qed        
    qed
  qed

  have "∃ x . f (Suc x) = f x ∧ x ≤ k - f 0"
  using assms(3) proof (induction k)
    case 0
    then show ?case by auto
  next
    case (Suc k)
    
    consider "f 0 + Suc k ≤ f (Suc k)" | "f (Suc k) < f 0 + Suc k ∧ f k = f (Suc k)"
      using ‹⋀ i . f (Suc i) ≥ f 0 + Suc i ∨ (f (Suc i) < f 0 + Suc i ∧ f i = f (Suc i))›[of k]  
      by blast

    then show ?case proof cases
      case 1
      then have "f (Suc (Suc k)) = f (Suc k)"
        using Suc.prems[of "Suc (Suc k)"] assms(1)[of "Suc k" "Suc (Suc k)"]
        by auto
      then show ?thesis
        by (metis "1" Suc.prems add.commute add_diff_cancel_left' add_increasing2 le_add2 le_add_same_cancel2 le_antisym) 
    next
      case 2
      then have "f (Suc k) < f 0 + Suc k" and "f k = f (Suc k)"
        by auto
      then show ?thesis
        by (metis Suc.prems ‹⋀i. f 0 + Suc i ≤ f (Suc i) ∨ f (Suc i) < f 0 + Suc i ∧ f i = f (Suc i)› add_Suc_right add_diff_cancel_left' le0 le_Suc_ex nat_arith.rule0 not_less_eq_eq)
    qed
  qed

  then show ?thesis 
    using that by blast
qed

lemma different_lists_shared_prefix :
  assumes "xs ≠ xs'"
obtains i where "take i xs = take i xs'" 
            and "take (Suc i) xs ≠ take (Suc i) xs'"
proof -
  have "∃ i . take i xs = take i xs' ∧ take (Suc i) xs ≠ take (Suc i) xs'"
  proof (rule ccontr)
    assume "∄i. take i xs = take i xs' ∧ take (Suc i) xs ≠ take (Suc i) xs'"
    
    have "⋀ i . take i xs = take i xs'"
    proof -
      fix i show "take i xs = take i xs'" 
      proof (induction i)
        case 0
        then show ?case by auto
      next
        case (Suc i)
        then show ?case 
          using ‹∄i. take i xs = take i xs' ∧ take (Suc i) xs ≠ take (Suc i) xs'› by blast
      qed 
    qed
    
    have "xs = xs'"
      by (simp add: ‹⋀i. take i xs = take i xs'› take_equalityI) 
    then show "False"
      using assms by simp
  qed
  then show ?thesis using that by blast
qed

lemma foldr_funion_fempty : "foldr (|∪|) xs fempty = ffUnion (fset_of_list xs)"
  by (induction xs; auto)

lemma foldr_funion_fsingleton : "foldr (|∪|) xs x = ffUnion (fset_of_list (x#xs))"
  by (induction xs; auto)

lemma foldl_funion_fempty : "foldl (|∪|) fempty xs = ffUnion (fset_of_list xs)"
  by (induction xs rule: rev_induct; auto)

lemma foldl_funion_fsingleton : "foldl (|∪|) x xs = ffUnion (fset_of_list (x#xs))"
  by (induction xs rule: rev_induct; auto)

lemma ffUnion_fmember_ob : "x |∈| ffUnion XS ⟹ ∃ X . X |∈| XS ∧ x |∈| X"
  by (induction XS; auto)


lemma filter_not_all_length :
  "filter P xs ≠ [] ⟹ length (filter (λ x . ¬ P x) xs) < length xs"
  by (metis filter_False length_filter_less)

lemma foldr_funion_fmember : "B |⊆| (foldr (|∪|) A B)"
  by (induction A; auto)

lemma prefix_free_set_maximal_list_ob :
  assumes "finite xs"
  and     "x ∈ xs"
obtains x' where "x@x' ∈ xs" and "∄ y' . y' ≠ [] ∧ (x@x')@y' ∈ xs" 
proof -

  let ?xs = "{x' . x@x' ∈ xs}"
  let ?x' = "arg_max length (λ x . x ∈ ?xs)"

 
  have "⋀y. y ∈ ?xs ⟹ length y < Suc (Max (length ` xs))"
  proof -
    fix y assume "y ∈ ?xs"
    then have "x@y ∈ xs"
      by blast
    moreover have "⋀y. y ∈ xs ⟹ length y < Suc (Max (length ` xs))"
      using assms(1)
      by (simp add: le_imp_less_Suc) 
    ultimately show "length y < Suc (Max (length ` xs))"
      by fastforce 
  qed
  moreover have "[] ∈ ?xs"
    using assms(2) by auto
  ultimately have "?x' ∈ ?xs" and "(∀ x' . x' ∈ ?xs ⟶ length x' ≤ length ?x')"
    using arg_max_nat_lemma[of "(λ x . x ∈ ?xs)" "[]" length "Suc (Max (length ` xs))"]
    by blast+     
  
  have "∄ y' . y' ≠ [] ∧ (x@?x')@y' ∈ xs"
  proof 
    assume "∃ y' . y' ≠ [] ∧ (x@?x')@y' ∈ xs"
    then obtain y' where "y' ≠ [] ∧ x@(?x'@y')∈ xs"
      by auto
    then have "(?x'@y') ∈ ?xs" and "length (?x'@y') > length ?x'" 
      by auto
    then show False
      using ‹(∀ x' . x' ∈ ?xs ⟶ length x' ≤ length ?x')›
      by auto
  qed

  then show ?thesis
    using that using ‹?x' ∈ ?xs› by blast
qed

lemma map_upds_map_set_left :
  assumes "[map f xs [↦] xs] q = Some x"
  shows "x ∈ set xs" and "q = f x"
proof -
  have "x ∈ set xs ∧ q = f x"
  using assms proof (induction xs rule: rev_induct)
    case Nil
    then show ?case by auto
  next
    case (snoc x' xs)
    show ?case proof (cases "f x' = q")
      case True
      then have "x = x'"
        using snoc.prems by (induction xs; auto)
      then show ?thesis 
        using True by auto
    next
      case False
      then have "[map f (xs @ [x']) [↦] xs @ [x']] q = [map f (xs) [↦] xs] q" 
        by (induction xs; auto)
      then show ?thesis 
        using snoc by auto
    qed
  qed
  then show "x ∈ set xs" and "q = f x"
    by auto
qed

lemma map_upds_map_set_right :
  assumes "x ∈ set xs"
  shows "[xs [↦] map f xs] x = Some (f x)" 
using assms proof (induction xs rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc x' xs)
  show ?case proof (cases "x=x'")
    case True
    then show ?thesis 
      by (induction xs; auto)
  next
    case False
    then have "[xs @ [x'] [↦] map f (xs @ [x'])] x = [xs [↦] map f xs] x"
      by (induction xs; auto)
    then show ?thesis 
      using snoc False by auto
  qed
qed


lemma map_upds_overwrite :
  assumes "x ∈ set xs"
      and "length xs = length ys"
  shows "(m(xs[↦]ys)) x = [xs[↦]ys] x" 
  using assms(2,1) by (induction xs ys rule: rev_induct2; auto)


lemma ran_dom_the_eq : "(λk . the (m k)) ` dom m = ran m" 
  unfolding ran_def dom_def by force


lemma map_pair_fst :
  "map fst (map (λx . (x,f x)) xs) = xs"
  by (induction xs; auto)

lemma map_of_map_pair_entry: "map_of (map (λk. (k, f k)) xs) x = (if x ∈ list.set xs then Some (f x) else None)"
  by (induction xs; auto)

lemma map_filter_alt_def :
  "List.map_filter f1' xs = map the (filter (λx . x ≠ None) (map f1' xs))"
  by (induction xs; unfold map_filter_simps; auto)

lemma map_filter_Nil :
  "List.map_filter f1' xs = [] ⟷ (∀ x ∈ list.set xs . f1' x = None)"
  unfolding map_filter_alt_def by (induction xs; auto)

lemma sorted_list_of_set_set: "set ((sorted_list_of_set ∘ set) xs) = set xs"
  by auto

fun mapping_of :: "('a × 'b) list ⇒ ('a, 'b) mapping" where
  "mapping_of kvs = foldl (λm kv . Mapping.update (fst kv) (snd kv) m) Mapping.empty kvs"

lemma mapping_of_map_of :
  assumes "distinct (map fst kvs)"
  shows "Mapping.lookup (mapping_of kvs) = map_of kvs"
proof
  show "⋀x. Mapping.lookup (mapping_of kvs) x = map_of kvs x"
    using assms
  proof (induction kvs rule: rev_induct)
    case Nil
    then show ?case by auto
  next
    case (snoc xy xs)

    have *:"map_of (xs @ [xy]) = map_of (xy#xs)"
      using snoc.prems map_of_inject_set[of "xs @ [xy]" "xy#xs", OF snoc.prems]
      by simp 

    show ?case 
      using snoc unfolding *
      by (cases "x = fst xy"; auto)
  qed
qed


lemma map_pair_fst_helper :
  "map fst (map (λ (x1,x2) . ((x1,x2), f x1 x2)) xs) = xs"
  using map_pair_fst[of "λ (x1,x2) . f x1 x2" xs]
  by (metis (no_types, lifting) map_eq_conv prod.collapse split_beta) 

end