diff --git a/thys/Generalized_Counting_Sort/Stability.thy b/thys/Generalized_Counting_Sort/Stability.thy
--- a/thys/Generalized_Counting_Sort/Stability.thy
+++ b/thys/Generalized_Counting_Sort/Stability.thy
@@ -1,764 +1,763 @@
 (*  Title:       An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges
     Author:      Pasquale Noce
                  Software Engineer at HID Global, Italy
                  pasquale dot noce dot lavoro at gmail dot com
                  pasquale dot noce at hidglobal dot com
 *)
 
 section "Proof of algorithm's stability"
 
 theory Stability
   imports Sorting
 begin
 
 text \<open>
 \null
 
 In this section, it is formally proven that GCsort is \emph{stable}, viz. that the sublist of the
 output of function @{const gcsort} built by picking out the objects having a given key matches the
 sublist of the input objects' list built in the same way.
 
 Here below, steps 5, 6, and 7 of the proof method are accomplished. Particularly, @{text stab_inv}
 is the predicate that will be shown to be invariant over inductive set @{const gcsort_set}.
 
 \null
 \<close>
 
 fun stab_inv :: "('b \<Rightarrow> 'a list) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> nat \<times> nat list \<times> 'a list \<Rightarrow>
   bool" where
 "stab_inv f key (u, ns, xs) = (\<forall>k. [x\<leftarrow>xs. key x = k] = f k)"
 
 lemma gcsort_stab_input:
  "stab_inv (\<lambda>k. [x\<leftarrow>xs. key x = k]) key (0, [length xs], xs)"
 by simp
 
 lemma gcsort_stab_intro:
  "stab_inv f key t \<Longrightarrow> [x\<leftarrow>gcsort_out t. key x = k] = f k"
 by (cases t, simp add: gcsort_out_def)
 
 text \<open>
 \null
 
 In what follows, step 9 of the proof method is accomplished.
 
 First, lemma @{text fill_offs_enum_stable} proves that function @{const fill}, if its input offsets'
 list is computed via the composition of functions @{const offs} and @{const enum}, does not modify
 the sublist of its input objects' list formed by the objects having a given key. Moreover, lemmas
 @{text mini_stable} and @{text maxi_stable} prove that the extraction of the leftmost minimum and
 the rightmost maximum from an objects' list through functions @{const mini} and @{const maxi} is
 endowed with the same property.
 
 These lemmas are then used to prove lemma @{text gcsort_stab_inv}, which states that the sublist of
 the objects having a given key within the objects' list is still the same after any recursive round.
 
 \null
 \<close>
 
 lemma fill_stable [rule_format]:
   assumes
     A: "index_less index key" and
     B: "index_same index key"
   shows
    "(\<forall>x \<in> set xs. key x \<in> {mi..ma}) \<longrightarrow>
     ns \<noteq> [] \<longrightarrow>
     offs_pred ns ub xs index key mi ma \<longrightarrow>
       map the [w\<leftarrow>fill xs ns index key ub mi ma. \<exists>x. w = Some x \<and> key x = k] =
         [x\<leftarrow>xs. k = key x]"
 proof (induction xs arbitrary: ns, simp_all add: Let_def, rule conjI,
  (rule_tac [!] impI)+, (erule_tac [!] conjE)+, simp_all)
   fix x xs and ns :: "nat list"
   let ?i = "index key x (length ns) mi ma"
   let ?ns' = "ns[?i := Suc (ns ! ?i)]"
   let ?ws = "[w\<leftarrow>fill xs ?ns' index key ub mi ma.
     \<exists>y. w = Some y \<and> key y = key x]"
   let ?ws' = "[w\<leftarrow>(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x].
     \<exists>y. w = Some y \<and> key y = key x]"
   assume
     C: "\<forall>x \<in> set xs. mi \<le> key x \<and> key x \<le> ma" and
     D: "mi \<le> key x" and
     E: "key x \<le> ma" and
     F: "ns \<noteq> []" and
     G: "offs_pred ns ub (x # xs) index key mi ma"
   have H: "?i < length ns"
     using A and D and E and F by (simp add: index_less_def)
   assume "\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow>
     map the [w\<leftarrow>fill xs ns index key ub mi ma.
       \<exists>y. w = Some y \<and> key y = key x] =
     [y\<leftarrow>xs. key x = key y]"
   moreover have I: "offs_pred ?ns' ub xs index key mi ma"
     using G and H by (rule_tac offs_pred_cons, simp_all)
   ultimately have J: "map the ?ws = [y\<leftarrow>xs. key x = key y]"
     using F by simp
   have "ns ! ?i + offs_num (length ns) (x # xs) index key mi ma ?i \<le> ub"
     using G and H by (rule offs_pred_ub, simp add: offs_num_cons)
   hence K: "ns ! ?i < ub"
     by (simp add: offs_num_cons)
   moreover from this have
     L: "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! (ns ! ?i) = Some x"
     by (subst nth_list_update_eq, simp_all add: fill_length)
   ultimately have "0 < length ?ws'"
     by (simp add: length_filter_conv_card card_gt_0_iff,
      rule_tac exI [where x = "ns ! ?i"], simp add: fill_length)
   hence "\<exists>w ws. ?ws' = w # ws"
     by (rule_tac list.exhaust [of ?ws'], simp_all)
   then obtain w and ws where "?ws' = w # ws" by blast
   hence "\<exists>us vs y.
     (fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] = us @ w # vs \<and>
     (\<forall>u \<in> set us. \<forall>y. u = Some y \<longrightarrow> key y \<noteq> key x) \<and>
     w = Some y \<and> key y = key x \<and>
     ws = [w\<leftarrow>vs. \<exists>y. w = Some y \<and> key y = key x]"
     (is "\<exists>us vs y. ?P us vs y")
     by (simp add: filter_eq_Cons_iff, blast)
   then obtain us and vs and y where M: "?P us vs y" by blast
   let ?A = "{i. i < length ns \<and> 0 < offs_num (length ns) xs index key mi ma i \<and>
     ns ! i \<le> length us}"
   have "length us = ns ! ?i"
   proof (rule ccontr, erule neqE, cases "?A = {}",
    cases "0 < offs_num (length ns) xs index key mi ma 0", simp_all only: not_gr0)
     assume
       N: "length us < ns ! ?i" and
       O: "?A = {}" and
       P: "0 < offs_num (length ns) xs index key mi ma 0"
     have "length us < ns ! 0"
     proof (rule ccontr, simp add: not_less)
       assume "ns ! 0 \<le> length us"
       with F and P have "0 \<in> ?A" by simp
       with O show False by blast
     qed
     hence "length us < ?ns' ! 0"
       using F by (cases ?i, simp_all)
     hence "offs_none ?ns' ub xs index key mi ma (length us)"
       using P by (simp add: offs_none_def)
     hence "fill xs ?ns' index key ub mi ma ! (length us) = None"
       using C and F and I by (rule_tac fill_none [OF A], simp_all)
     hence "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! (length us) = None"
       using N by simp
     thus False
       using M by simp
   next
     assume
       N: "length us < ns ! ?i" and
       O: "?A = {}" and
       P: "offs_num (length ns) xs index key mi ma 0 = 0"
     from K and N have "length us < offs_next ?ns' ub xs index key mi ma 0"
     proof (rule_tac ccontr, simp only: not_less offs_next_def split: if_split_asm)
       assume "offs_set_next ?ns' xs index key mi ma 0 \<noteq> {}"
         (is "?B \<noteq> _")
       hence "Min ?B \<in> ?B"
         by (rule_tac Min_in, simp)
       moreover assume "?ns' ! Min ?B \<le> length us"
       hence "ns ! Min ?B \<le> length us"
         using H by (cases "Min ?B = ?i", simp_all)
       ultimately have "Min ?B \<in> ?A" by simp
       with O show False by blast
     qed
     hence "offs_none ?ns' ub xs index key mi ma (length us)"
       using P by (simp add: offs_none_def)
     hence "fill xs ?ns' index key ub mi ma ! (length us) = None"
       using C and F and I by (rule_tac fill_none [OF A], simp_all)
     hence "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! (length us) = None"
       using N by simp
     thus False
       using M by simp
   next
     assume N: "length us < ns ! ?i"
     assume "?A \<noteq> {}"
     hence "Max ?A \<in> ?A"
       by (rule_tac Max_in, simp)
     moreover from this have O: "Max ?A \<noteq> ?i"
       using N by (rule_tac notI, simp)
     ultimately have "index key y (length ?ns') mi ma = Max ?A"
     using C proof (rule_tac fill_index [OF A _ I, where j = "length us"], simp_all,
      rule_tac ccontr, simp only: not_less not_le offs_next_def split: if_split_asm)
       assume "ub \<le> length us"
       with N have "ub < ns ! ?i" by simp
       with K show False by simp
     next
       let ?B = "offs_set_next ?ns' xs index key mi ma (Max ?A)"
       assume "?ns' ! Min ?B \<le> length us"
       hence "ns ! Min ?B \<le> length us"
         using H by (cases "Min ?B = ?i", simp_all)
       moreover assume "?B \<noteq> {}"
       hence P: "Min ?B \<in> ?B"
         by (rule_tac Min_in, simp)
       ultimately have "Min ?B \<in> ?A" by simp
       hence "Min ?B \<le> Max ?A"
         by (rule_tac Max_ge, simp)
       thus False
         using P by simp
     next
       have "fill xs ?ns' index key ub mi ma ! length us =
         (fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! length us"
         using N by simp
       thus "fill xs ?ns' index key ub mi ma ! length us = Some y"
         using M by simp
     qed
     moreover have "index key y (length ?ns') mi ma = ?i"
       using B and D and E and M by (cases "y = x", simp_all add:
        index_same_def)
     ultimately show False
       using O by simp
   next
     assume N: "ns ! ?i < length us"
     hence "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! (ns ! ?i) =
       us ! (ns ! ?i)"
       using M by (simp add: nth_append)
     hence "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! (ns ! ?i) \<in> set us"
       using N by simp
     thus False
       using L and M by blast
   qed
   hence "take (ns ! ?i) ((fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x]) = us"
     using M by simp
   hence N: "take (ns ! ?i) (fill xs ?ns' index key ub mi ma) = us" by simp
   have "fill xs ?ns' index key ub mi ma =
     take (ns ! ?i) (fill xs ?ns' index key ub mi ma) @
     fill xs ?ns' index key ub mi ma ! (ns ! ?i) #
     drop (Suc (ns ! ?i)) (fill xs ?ns' index key ub mi ma)"
     (is "_ = ?ts @ _ # ?ds")
     using K by (rule_tac id_take_nth_drop, simp add: fill_length)
   moreover have "fill xs ?ns' index key ub mi ma ! (ns ! ?i) = None"
     using C and D and E and F and G by (rule_tac fill_index_none [OF A],
      simp_all)
   ultimately have O: "fill xs ?ns' index key ub mi ma = us @ None # ?ds"
     using N by simp
   have "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] =
     ?ts @ Some x # ?ds"
     using K by (rule_tac upd_conv_take_nth_drop, simp add: fill_length)
   hence "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] =
     us @ Some x # ?ds"
     using N by simp
   hence "?ws' = Some x # [w\<leftarrow>?ds. \<exists>y. w = Some y \<and> key y = key x]"
     using M by simp
   also have "\<dots> = Some x # ?ws"
     using M by (subst (2) O, simp)
   finally show "map the ?ws' = x # [y\<leftarrow>xs. key x = key y]"
     using J by simp
 next
   fix x xs and ns :: "nat list"
   let ?i = "index key x (length ns) mi ma"
   let ?ns' = "ns[?i := Suc (ns ! ?i)]"
   let ?ws = "[w\<leftarrow>fill xs ?ns' index key ub mi ma. \<exists>y. w = Some y \<and> key y = k]"
   let ?ws' = "[w\<leftarrow>(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x].
     \<exists>y. w = Some y \<and> key y = k]"
   assume
     C: "\<forall>x \<in> set xs. mi \<le> key x \<and> key x \<le> ma" and
     D: "mi \<le> key x" and
     E: "key x \<le> ma" and
     F: "ns \<noteq> []" and
     G: "offs_pred ns ub (x # xs) index key mi ma" and
     H: "k \<noteq> key x"
   have I: "?i < length ns"
     using A and D and E and F by (simp add: index_less_def)
   assume "\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow>
     map the [w\<leftarrow>fill xs ns index key ub mi ma.
       \<exists>y. w = Some y \<and> key y = k] =
     [y\<leftarrow>xs. k = key y]"
   moreover have "offs_pred ?ns' ub xs index key mi ma"
     using G and I by (rule_tac offs_pred_cons, simp_all)
   ultimately have J: "map the ?ws = [y\<leftarrow>xs. k = key y]"
     using F by simp
   have "ns ! ?i + offs_num (length ns) (x # xs) index key mi ma ?i \<le> ub"
     using G and I by (rule offs_pred_ub, simp add: offs_num_cons)
   hence K: "ns ! ?i < ub"
     by (simp add: offs_num_cons)
   have "fill xs ?ns' index key ub mi ma =
     take (ns ! ?i) (fill xs ?ns' index key ub mi ma) @
     fill xs ?ns' index key ub mi ma ! (ns ! ?i) #
     drop (Suc (ns ! ?i)) (fill xs ?ns' index key ub mi ma)"
     (is "_ = ?ts @ _ # ?ds")
     using K by (rule_tac id_take_nth_drop, simp add: fill_length)
   moreover have "fill xs ?ns' index key ub mi ma ! (ns ! ?i) = None"
     using C and D and E and F and G by (rule_tac fill_index_none [OF A],
      simp_all)
   ultimately have L: "fill xs ?ns' index key ub mi ma = ?ts @ None # ?ds"
     by simp
   have "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] =
     ?ts @ Some x # ?ds"
     using K by (rule_tac upd_conv_take_nth_drop, simp add: fill_length)
   moreover have "?ws = [w\<leftarrow>?ts. \<exists>y. w = Some y \<and> key y = k] @
     [w\<leftarrow>?ds. \<exists>y. w = Some y \<and> key y = k]"
     by (subst L, simp)
   ultimately have "?ws' = ?ws"
     using H by simp
   thus "map the ?ws' = [y\<leftarrow>xs. k = key y]"
     using J by simp
 qed
 
 lemma fill_offs_enum_stable [rule_format]:
   assumes
     A: "index_less index key" and
     B: "index_same index key"
   shows
    "\<forall>x \<in> set xs. key x \<in> {mi..ma} \<Longrightarrow>
     0 < n \<Longrightarrow>
       [x\<leftarrow>map the (fill xs (offs (enum xs index key n mi ma) 0)
         index key (length xs) mi ma). key x = k] = [x\<leftarrow>xs. k = key x]"
   (is "_ \<Longrightarrow> _ \<Longrightarrow> [_\<leftarrow>map the ?ys. _] = _"
    is "_ \<Longrightarrow> _ \<Longrightarrow> [_\<leftarrow>map the (fill _ ?ns _ _ _ _ _). _] = _")
 proof (subst fill_stable [symmetric, OF A B, of xs mi ma ?ns], simp,
  simp only: length_greater_0_conv [symmetric] offs_length enum_length,
  rule offs_enum_pred [OF A], simp, subst filter_map,
  simp add: filter_eq_nths fill_length)
   assume
     C: "\<forall>x \<in> set xs. mi \<le> key x \<and> key x \<le> ma" and
     D: "0 < n"
   have "{i. i < length xs \<and> key (the (?ys ! i)) = k} =
     {i. i < length xs \<and> (\<exists>x. ?ys ! i = Some x \<and> key x = k)}"
     (is "?A = ?B")
   proof (rule set_eqI, rule iffI, simp_all, erule_tac [!] conjE, erule_tac [2] exE,
    erule_tac [2] conjE, simp_all)
     fix i
     assume E: "i < length xs" and F: "key (the (?ys ! i)) = k"
     have "\<exists>x. ?ys ! i = Some x"
     proof (cases "?ys ! i", simp_all)
       assume "?ys ! i = None"
       moreover have "?ys ! i \<in> set ?ys"
         using E by (rule_tac nth_mem, simp add: fill_length)
       ultimately have "None \<in> set ?ys" by simp
       moreover have "count (mset ?ys) None = 0"
         using C and D by (rule_tac fill_offs_enum_count_none [OF A], simp)
       ultimately show False by simp
     qed
     then obtain x where "?ys ! i = Some x" ..
     moreover from this have "key x = k"
       using F by simp
     ultimately show "\<exists>x. ?ys ! i = Some x \<and> key x = k" by simp
   qed
   thus "map the (nths ?ys ?A) = map the (nths ?ys ?B)" by simp
 qed
 
 lemma mini_first [rule_format]:
  "xs \<noteq> [] \<longrightarrow> i < mini xs key \<longrightarrow>
     key (xs ! mini xs key) < key (xs ! i)"
 by (induction xs arbitrary: i, simp_all add: Let_def, (rule impI)+,
  erule conjE, simp add: not_le nth_Cons split: nat.split)
 
 lemma maxi_last [rule_format]:
  "xs \<noteq> [] \<longrightarrow> maxi xs key < i \<longrightarrow> i < length xs \<longrightarrow>
     key (xs ! i) < key (xs ! maxi xs key)"
 by (induction xs arbitrary: i, simp_all add: Let_def, (rule impI)+,
  rule le_less_trans, rule maxi_ub, rule nth_mem, simp)
 
 lemma nths_range:
  "nths xs A = nths xs (A \<inter> {..<length xs})"
 proof (induction xs arbitrary: A, simp_all add: nths_Cons)
   fix xs :: "'a list" and A
   assume "\<And>A. nths xs A = nths xs (A \<inter> {..<length xs})"
   hence "nths xs {i. Suc i \<in> A} = nths xs ({i. Suc i \<in> A} \<inter> {..<length xs})" .
   moreover have
    "{i. Suc i \<in> A} \<inter> {..<length xs} = {i. Suc i \<in> A \<and> i < length xs}"
     by blast
   ultimately show
    "nths xs {i. Suc i \<in> A} = nths xs {i. Suc i \<in> A \<and> i < length xs}"
     by simp
 qed
 
 lemma filter_nths_diff:
   assumes
     A: "i < length xs" and
     B: "\<not> P (xs ! i)"
   shows "[x\<leftarrow>nths xs (A - {i}). P x] = [x\<leftarrow>nths xs A. P x]"
 proof (cases "i \<in> A", simp_all)
   case True
   have C: "xs = take i xs @ xs ! i # drop (Suc i) xs"
     (is "_ = ?ts @ _ # ?ds")
     using A by (rule id_take_nth_drop)
   have "nths xs A = nths ?ts A @ nths (xs ! i # ?ds) {j. j + length ?ts \<in> A}"
     by (subst C, simp add: nths_append)
   moreover have D: "length ?ts = i"
     using A by simp
   ultimately have E: "nths xs A = nths ?ts (A \<inter> {..<i}) @ xs ! i #
     nths ?ds {j. Suc j + i \<in> A}"
     (is "_ = ?vs @ _ # ?ws")
     using True by (simp add: nths_Cons, subst nths_range, simp)
   have "nths xs (A - {i}) = nths ?ts (A - {i}) @
     nths (xs ! i # ?ds) {j. j + length ?ts \<in> A - {i}}"
     by (subst C, simp add: nths_append)
   moreover have "(A - {i}) \<inter> {..<i} = A \<inter> {..<i}"
     by (rule set_eqI, rule iffI, simp_all)
   ultimately have "nths xs (A - {i}) = ?vs @ ?ws"
     using D by (simp add: nths_Cons, subst nths_range, simp)
   thus ?thesis
     using B and E by simp
 qed
 
 lemma mini_stable:
   assumes
     A: "xs \<noteq> []" and
     B: "mini xs key \<in> A"
       (is "?nmi \<in> _")
   shows "[x\<leftarrow>[xs ! ?nmi] @ nths xs (A - {?nmi}). key x = k] =
     [x\<leftarrow>nths xs A. key x = k]"
     (is "[x\<leftarrow>[?xmi] @ _. _] = _")
 proof (simp, rule conjI, rule_tac [!] impI, rule_tac [2] filter_nths_diff,
  rule_tac [2] mini_less, simp_all add: A)
   assume C: "key ?xmi = k"
   moreover have "?nmi < length xs"
     using A by (rule_tac mini_less, simp)
   ultimately have "0 < length [x\<leftarrow>xs. key x = k]"
     by (simp add: length_filter_conv_card card_gt_0_iff, rule_tac exI, rule_tac conjI)
   hence "\<exists>y ys. [x\<leftarrow>xs. key x = k] = y # ys"
     by (rule_tac list.exhaust [of "[x\<leftarrow>xs. key x = k]"], simp_all)
   then obtain y and ys where "[x\<leftarrow>xs. key x = k] = y # ys" by blast
   hence "\<exists>us vs. xs = us @ y # vs \<and>
     (\<forall>u \<in> set us. key u \<noteq> k) \<and> key y = k \<and> ys = [x\<leftarrow>vs. key x = k]"
     (is "\<exists>us vs. ?P us vs")
     by (simp add: filter_eq_Cons_iff)
   then obtain us and vs where D: "?P us vs" by blast
   have E: "length us = ?nmi"
   proof (rule ccontr, erule neqE)
     assume "length us < ?nmi"
     with A have "key ?xmi < key (xs ! length us)"
       by (rule mini_first)
     also have "\<dots> = k"
       using D by simp
     finally show False
       using C by simp
   next
     assume F: "?nmi < length us"
     hence "?xmi = us ! ?nmi"
       using D by (simp add: nth_append)
     hence "?xmi \<in> set us"
       using F by simp
     thus False
       using C and D by simp
   qed
   moreover have "xs ! length us = y"
     using D by simp
   ultimately have F: "?xmi = y" by simp
   have "nths xs A = nths us A @ nths (y # vs) {i. i + ?nmi \<in> A}"
     using D and E by (simp add: nths_append)
   also have "\<dots> = nths us A @ y # nths vs {i. Suc i + ?nmi \<in> A}"
     (is "_ = _ @ _ # ?ws")
     using B by (simp add: nths_Cons)
   finally have G: "[x\<leftarrow>nths xs A. key x = k] = y # [x\<leftarrow>?ws. key x = k]"
     using D by (simp add: filter_empty_conv, rule_tac ballI,
      drule_tac in_set_nthsD, simp)
   have "nths xs (A - {?nmi}) = nths us (A - {?nmi}) @
     nths (y # vs) {i. i + ?nmi \<in> A - {?nmi}}"
     using D and E by (simp add: nths_append)
   also have "\<dots> = nths us (A - {?nmi}) @ ?ws"
     by (simp add: nths_Cons)
   finally have H: "[x\<leftarrow>nths xs (A - {?nmi}). key x = k] = [x\<leftarrow>?ws. key x = k]"
     using D by (simp add: filter_empty_conv, rule_tac ballI,
      drule_tac in_set_nthsD, simp)
   show "?xmi # [x\<leftarrow>nths xs (A - {?nmi}). key x = k] =
     [x\<leftarrow>nths xs A. key x = k]"
     using F and G and H by simp
 qed
 
 lemma maxi_stable:
   assumes
     A: "xs \<noteq> []" and
     B: "maxi xs key \<in> A"
       (is "?nma \<in> _")
   shows "[x\<leftarrow>nths xs (A - {?nma}) @ [xs ! ?nma]. key x = k] =
     [x\<leftarrow>nths xs A. key x = k]"
     (is "[x\<leftarrow>_ @ [?xma]. _] = _")
 proof (simp, rule conjI, rule_tac [!] impI, rule_tac [2] filter_nths_diff,
  rule_tac [2] maxi_less, simp_all add: A)
   assume C: "key ?xma = k"
   moreover have D: "?nma < length xs"
     using A by (rule_tac maxi_less, simp)
   ultimately have "0 < length [x\<leftarrow>rev xs. key x = k]"
     by (simp add: length_filter_conv_card card_gt_0_iff,
      rule_tac exI [where x = "length xs - Suc ?nma"], simp add: rev_nth)
   hence "\<exists>y ys. [x\<leftarrow>rev xs. key x = k] = y # ys"
     by (rule_tac list.exhaust [of "[x\<leftarrow>rev xs. key x = k]"], simp_all)
   then obtain y and ys where "[x\<leftarrow>rev xs. key x = k] = y # ys" by blast
   hence "\<exists>us vs. rev xs = us @ y # vs \<and>
     (\<forall>u \<in> set us. key u \<noteq> k) \<and> key y = k \<and> ys = [x\<leftarrow>vs. key x = k]"
     (is "\<exists>us vs. ?P us vs")
     by (simp add: filter_eq_Cons_iff)
   then obtain us and vs where E: "?P us vs" by blast
   hence F: "xs = rev vs @ y # rev us"
     by (simp add: rev_swap)
   have G: "length us = length xs - Suc ?nma"
   proof (rule ccontr, erule neqE)
     assume "length us < length xs - Suc ?nma"
     hence "?nma < length xs - Suc (length us)" by simp
     moreover have "length xs - Suc (length us) < length xs"
       using D by simp
     ultimately have "key (xs ! (length xs - Suc (length us))) < key ?xma"
       by (rule maxi_last [OF A])
     moreover have "length us < length xs"
       using F by simp
     ultimately have "key (rev xs ! length us) < key ?xma"
       by (simp add: rev_nth)
     moreover have "key (rev xs ! length us) = k"
       using E by simp
     ultimately show False
       using C by simp
   next
     assume H: "length xs - Suc ?nma < length us"
     hence "rev xs ! (length xs - Suc ?nma) = us ! (length xs - Suc ?nma)"
       using E by (simp add: nth_append)
     hence "rev xs ! (length xs - Suc ?nma) \<in> set us"
       using H by simp
     hence "?xma \<in> set us"
       using D by (simp add: rev_nth)
     thus False
       using C and E by simp
   qed
   moreover have "rev xs ! length us = y"
     using E by simp
   ultimately have H: "?xma = y"
     using D by (simp add: rev_nth)
   have "length xs = length us + Suc ?nma"
     using D and G by simp
   hence I: "length vs = ?nma"
     using F by simp
   hence "nths xs A = nths (rev vs) A @ nths (y # rev us) {i. i + ?nma \<in> A}"
     using F by (simp add: nths_append)
   also have "\<dots> = nths (rev vs) (A \<inter> {..<?nma}) @ y #
     nths (rev us) {i. Suc i + ?nma \<in> A}"
     (is "_ = ?ws @ _ # _")
     using B and I by (simp add: nths_Cons, subst nths_range, simp)
   finally have J: "[x\<leftarrow>nths xs A. key x = k] = [x\<leftarrow>?ws. key x = k] @ [y]"
     using E by (simp add: filter_empty_conv, rule_tac ballI,
      drule_tac in_set_nthsD, simp)
   have "nths xs (A - {?nma}) = nths (rev vs) (A - {?nma}) @
     nths (y # rev us) {i. i + ?nma \<in> A - {?nma}}"
     using F and I by (simp add: nths_append)
   hence "nths xs (A - {?nma}) = nths (rev vs) ((A - {?nma}) \<inter> {..<?nma}) @
     nths (rev us) {i. Suc i + ?nma \<in> A}"
     using I by (simp add: nths_Cons, subst nths_range, simp)
   moreover have "(A - {?nma}) \<inter> {..<?nma} = A \<inter> {..<?nma}"
     by (rule set_eqI, rule iffI, simp_all)
   ultimately have K: "[x\<leftarrow>nths xs (A - {?nma}). key x = k] =
     [x\<leftarrow>?ws. key x = k]"
     using E by (simp add: filter_empty_conv, rule_tac ballI,
      drule_tac in_set_nthsD, simp)
   show "[x\<leftarrow>nths xs (A - {?nma}). key x = k] @ [?xma] =
     [x\<leftarrow>nths xs A. key x = k]"
     using H and J and K by simp
 qed
 
 lemma round_stab_inv [rule_format]:
  "index_less index key \<longrightarrow> index_same index key \<longrightarrow> bn_inv p q t \<longrightarrow>
     add_inv n t \<longrightarrow> stab_inv f key t \<longrightarrow> stab_inv f key (round index key p q r t)"
 proof (induction index key p q r t arbitrary: n f rule: round.induct,
  (rule_tac [!] impI)+, simp, simp, simp_all only: simp_thms)
   fix index p q r u ns xs n f and key :: "'a \<Rightarrow> 'b"
   let ?t = "round index key p q r (u, ns, tl xs)"
   assume
    "\<And>n f. bn_inv p q (u, ns, tl xs) \<longrightarrow> add_inv n (u, ns, tl xs) \<longrightarrow>
       stab_inv f key (u, ns, tl xs) \<longrightarrow> stab_inv f key ?t" and
    "bn_inv p q (u, Suc 0 # ns, xs)" and
    "add_inv n (u, Suc 0 # ns, xs)" and
    "stab_inv f key (u, Suc 0 # ns, xs)"
   thus "stab_inv f key (round index key p q r (u, Suc 0 # ns, xs))"
   proof (cases ?t, cases xs, simp_all add: add_suc, arith, erule_tac conjE,
    rule_tac allI, simp)
     fix k y ys xs'
     let ?f' = "f(key y := tl (f (key y)))"
     assume "\<And>n' f'. foldl (+) 0 ns = n' \<and> length ys = n' \<longrightarrow>
       (\<forall>k'. [x\<leftarrow>ys. key x = k'] = f' k') \<longrightarrow> (\<forall>k'. [x\<leftarrow>xs'. key x = k'] = f' k')"
     moreover assume "Suc (foldl (+) 0 ns) = n" and "Suc (length ys) = n"
     ultimately have "(\<forall>k'. [x\<leftarrow>ys. key x = k'] = ?f' k') \<longrightarrow>
       (\<forall>k'. [x\<leftarrow>xs'. key x = k'] = ?f' k')"
       by blast
     moreover assume A: "\<forall>k'. (if key y = k'
       then y # [x\<leftarrow>ys. key x = k'] else [x\<leftarrow>ys. key x = k']) = f k'"
     hence B: "f (key y) = y # [x\<leftarrow>ys. key x = key y]"
       by (drule_tac spec [where x = "key y"], simp)
     hence "\<forall>k'. [x\<leftarrow>ys. key x = k'] = ?f' k'"
     proof (rule_tac allI, simp, rule_tac impI)
       fix k'
       assume "k' \<noteq> key y"
       thus "[x\<leftarrow>ys. key x = k'] = f k'"
         using A by (drule_tac spec [where x = k'], simp)
     qed
     ultimately have C: "\<forall>k'. [x\<leftarrow>xs'. key x = k'] = ?f' k'" ..
     show "(key y = k \<longrightarrow> y # [x\<leftarrow>xs'. key x = k] = f k) \<and>
       (key y \<noteq> k \<longrightarrow> [x\<leftarrow>xs'. key x = k] = f k)"
     proof (rule conjI, rule_tac [!] impI)
       assume "key y = k"
       moreover have "tl (f (key y)) = [x\<leftarrow>xs'. key x = key y]"
         using C by simp
       hence "f (key y) = y # [x\<leftarrow>xs'. key x = key y]"
         using B by (subst hd_Cons_tl [symmetric], simp_all)
       ultimately show "y # [x\<leftarrow>xs'. key x = k] = f k" by simp
     next
       assume "key y \<noteq> k"
       thus "[x\<leftarrow>xs'. key x = k] = f k"
         using C by simp
     qed
   qed
 next
   fix index p q r u m ns n f and key :: "'a \<Rightarrow> 'b" and xs :: "'a list"
   let ?ws = "take (Suc (Suc m)) xs"
   let ?ys = "drop (Suc (Suc m)) xs"
   let ?r = "\<lambda>m'. round_suc_suc index key ?ws m m' u"
   let ?t = "\<lambda>r' v. round index key p q r' (v, ns, ?ys)"
   assume
     A: "index_less index key" and
     B: "index_same index key"
   assume
    "\<And>ws a b c d e g h i n f.
       ws = ?ws \<Longrightarrow> a = bn_comp m p q r \<Longrightarrow> (b, c) = bn_comp m p q r \<Longrightarrow>
       d = ?r b \<Longrightarrow> (e, g) = ?r b \<Longrightarrow> (h, i) = g \<Longrightarrow>
         bn_inv p q (e, ns, ?ys) \<longrightarrow> add_inv n (e, ns, ?ys) \<longrightarrow>
           stab_inv f key (e, ns, ?ys) \<longrightarrow> stab_inv f key (?t c e)" and
    "bn_inv p q (u, Suc (Suc m) # ns, xs)" and
    "add_inv n (u, Suc (Suc m) # ns, xs)" and
    "stab_inv f key (u, Suc (Suc m) # ns, xs)"
   thus "stab_inv f key (round index key p q r (u, Suc (Suc m) # ns, xs))"
   using [[simproc del: defined_all]]
   proof (simp split: prod.split, ((rule_tac allI)+, ((rule_tac impI)+)?)+,
    (erule_tac conjE)+, subst (asm) (2) add_base_zero, simp)
     fix m' r' v ms' ws' xs' k
     let ?f = "\<lambda>k. [x\<leftarrow>?ys. key x = k]"
     let ?P = "\<lambda>f. \<forall>k. [x\<leftarrow>?ys. key x = k] = f k"
     let ?Q = "\<lambda>f. \<forall>k. [x\<leftarrow>xs'. key x = k] = f k"
     assume
       C: "?r m' = (v, ms', ws')" and
       D: "bn_comp m p q r = (m', r')" and
       E: "bn_valid m p q" and
       F: "Suc (Suc (foldl (+) 0 ns + m)) = n" and
       G: "length xs = n"
     assume "\<And>ws a b c d e g h i n' f.
       ws = ?ws \<Longrightarrow> a = (m', r') \<Longrightarrow> b = m' \<and> c = r' \<Longrightarrow>
       d = (v, ms', ws') \<Longrightarrow> e = v \<and> g = (ms', ws') \<Longrightarrow> h = ms' \<and> i = ws' \<Longrightarrow>
         foldl (+) 0 ns = n' \<and> n - Suc (Suc m) = n' \<longrightarrow> ?P f \<longrightarrow> ?Q f"
     hence "\<And>f. foldl (+) 0 ns = n - Suc (Suc m) \<longrightarrow> ?P f \<longrightarrow> ?Q f"
       by simp
     hence "\<And>f. ?P f \<longrightarrow> ?Q f"
       using F by simp
     hence "?P ?f \<longrightarrow> ?Q ?f" .
     hence "[x\<leftarrow>xs'. key x = k] = [x\<leftarrow>?ys. key x = k]" by simp
     moreover assume "\<forall>k. [x\<leftarrow>xs. key x = k] = f k"
     hence "f k = [x\<leftarrow>?ws @ ?ys. key x = k]" by simp
     ultimately have "f k = [x\<leftarrow>?ws. key x = k] @ [x\<leftarrow>xs'. key x = k]"
       by (subst (asm) filter_append, simp)
     with C [symmetric] show "[x\<leftarrow>ws'. key x = k] @ [x\<leftarrow>xs'. key x = k] = f k"
     proof (simp add: round_suc_suc_def Let_def del: filter.simps
      split: if_split_asm)
       let ?nmi = "mini ?ws key"
       let ?nma = "maxi ?ws key"
       let ?xmi = "?ws ! ?nmi"
       let ?xma = "?ws ! ?nma"
       let ?mi = "key ?xmi"
       let ?ma = "key ?xma"
       let ?k = "case m of 0 \<Rightarrow> m | Suc 0 \<Rightarrow> m | Suc (Suc i) \<Rightarrow> u + m'"
       let ?zs = "nths ?ws (- {?nmi, ?nma})"
       let ?ms = "enum ?zs index key ?k ?mi ?ma"
       have H: "length ?ws = Suc (Suc m)"
         using F and G by simp
       hence I: "?nmi \<noteq> ?nma"
         by (rule_tac mini_maxi_neq, simp)
       have "[x\<leftarrow>(([?xmi] @ map the (fill ?zs (offs ?ms 0) index key m ?mi ?ma))
         @ [?xma]). key x = k] = [x\<leftarrow>?ws. key x = k]"
       proof (cases "m = 0")
         case True
         have "?nmi < length ?ws"
           using H by (rule_tac mini_less, simp)
         hence J: "?nmi < Suc (Suc 0)"
           using True by simp
         moreover have "?nma < length ?ws"
           using H by (rule_tac maxi_less, simp)
         hence K: "?nma < Suc (Suc 0)"
           using True by simp
         ultimately have "card ({..<Suc (Suc 0)} - {?nma} - {?nmi}) = 0"
-          using I by ((subst card_Diff_singleton, simp, simp)+,
-           subst card_lessThan, simp)
+          using I by auto
         hence L: "{..<Suc (Suc 0)} - {?nma} - {?nmi} = {}" by simp
         have "length (fill ?zs (offs ?ms 0) index key m ?mi ?ma) = 0"
           using True by (simp add: fill_length)
         hence M: "map the (fill ?zs (offs ?ms 0) index key m ?mi ?ma) =
           nths ?ws ({..<Suc (Suc 0)} - {?nma} - {?nmi})"
           by (subst L, simp)
         show ?thesis
         proof (subst M, subst filter_append)
           show "[x\<leftarrow>[?xmi] @ nths ?ws ({..<Suc (Suc 0)} - {?nma} - {?nmi}).
             key x = k] @ [x\<leftarrow>[?xma]. key x = k] = [x\<leftarrow>?ws. key x = k]"
           proof (subst mini_stable, simp only: length_greater_0_conv
            [symmetric] H, simp add: I J, subst filter_append [symmetric])
             show "[x\<leftarrow>nths ?ws ({..<Suc (Suc 0)} - {?nma}) @ [?xma].
               key x = k] = [x\<leftarrow>?ws. key x = k]"
               by (subst maxi_stable, simp only: length_greater_0_conv
                [symmetric] H, simp add: K, simp add: True)
           qed
         qed
       next
         case False
         hence "0 < ?k"
           by (simp, drule_tac bn_comp_fst_nonzero [OF E], subst (asm) D,
            simp split: nat.split)
         hence "[x\<leftarrow>map the (fill ?zs (offs ?ms 0) index key (length ?zs) ?mi ?ma).
           key x = k] = [x\<leftarrow>?zs. k = key x]"
           by (rule_tac fill_offs_enum_stable [OF A B], simp, rule_tac conjI,
            ((rule_tac mini_lb | rule_tac maxi_ub), erule_tac in_set_nthsD)+)
         moreover have "[x\<leftarrow>?zs. k = key x] = [x\<leftarrow>?zs. key x = k]"
           by (rule filter_cong, simp, blast)
         ultimately have
           J: "[x\<leftarrow>map the (fill ?zs (offs ?ms 0) index key m ?mi ?ma).
             key x = k] = [x\<leftarrow>?zs. key x = k]"
           using H by (simp add: mini_maxi_nths)
         show ?thesis
         proof (simp only: filter_append J, subst Compl_eq_Diff_UNIV,
          subst Diff_insert, subst filter_append [symmetric])
           show "[x\<leftarrow>[?xmi] @ nths ?ws (UNIV - {?nma} - {?nmi}). key x = k]
             @ [x\<leftarrow>[?xma]. key x = k] = [x\<leftarrow>?ws. key x = k]"
           proof (subst mini_stable, simp only: length_greater_0_conv
            [symmetric] H, simp add: I, subst filter_append [symmetric])
             show "[x\<leftarrow>nths ?ws (UNIV - {?nma}) @ [?xma]. key x = k] =
               [x\<leftarrow>?ws. key x = k]"
               by (subst maxi_stable, simp only: length_greater_0_conv
                [symmetric] H, simp, subst nths_range, subst H, simp)
           qed
         qed
       qed
       thus "[x\<leftarrow>?xmi # map the (fill ?zs (offs ?ms 0) index key m ?mi ?ma) @
         [?xma]. key x = k] = [x\<leftarrow>?ws. key x = k]"
         by simp
     qed
   qed
 qed
 
 lemma gcsort_stab_inv:
   assumes
     A: "index_less index key" and
     B: "index_same index key" and
     C: "add_inv n t" and
     D: "n \<le> p"
   shows "\<lbrakk>t' \<in> gcsort_set index key p t; stab_inv f key t\<rbrakk> \<Longrightarrow>
     stab_inv f key t'"
 by (erule gcsort_set.induct, simp, drule gcsort_add_inv [OF A _ C D],
  rule round_stab_inv [OF A B], simp_all del: bn_inv.simps, erule conjE,
  frule sym, erule subst, rule bn_inv_intro, insert D, simp)
 
 text \<open>
 \null
 
 The only remaining task is to address step 10 of the proof method, which is done by proving theorem
 @{text gcsort_stable}. It holds under the conditions that the objects' number is not larger than the
 counters' upper bound and function @{text index} satisfies both predicates @{const index_less} and
 @{const index_same}, and states that function @{const gcsort} leaves unchanged the sublist of the
 objects having a given key within the input objects' list.
 
 \null
 \<close>
 
 theorem gcsort_stable:
   assumes
     A: "index_less index key" and
     B: "index_same index key" and
     C: "length xs \<le> p"
   shows "[x\<leftarrow>gcsort index key p xs. key x = k] = [x\<leftarrow>xs. key x = k]"
 proof -
   let ?t = "(0, [length xs], xs)"
   have "stab_inv (\<lambda>k. [x\<leftarrow>xs. key x = k]) key (gcsort_aux index key p ?t)"
     by (rule gcsort_stab_inv [OF A B _ C], rule gcsort_add_input,
      rule gcsort_aux_set, rule gcsort_stab_input)
   hence "[x\<leftarrow>gcsort_out (gcsort_aux index key p ?t). key x = k] =
     [x\<leftarrow>xs. key x = k]"
     by (rule gcsort_stab_intro)
   moreover have "?t = gcsort_in xs"
     by (simp add: gcsort_in_def)
   ultimately show ?thesis
     by (simp add: gcsort_def)
 qed
 
 end
diff --git a/thys/Matroids/Matroid.thy b/thys/Matroids/Matroid.thy
--- a/thys/Matroids/Matroid.thy
+++ b/thys/Matroids/Matroid.thy
@@ -1,1337 +1,1338 @@
 (*
   File:     Matroid.thy
   Author:   Jonas Keinholz
 *)
 section \<open>Matroids\<close>
 theory Matroid
   imports Indep_System
 begin
 
 lemma card_subset_ex:
   assumes "finite A" "n \<le> card A"
   shows "\<exists>B \<subseteq> A. card B = n"
 using assms
 proof (induction A arbitrary: n rule: finite_induct)
   case (insert x A)
   show ?case
   proof (cases n)
     case 0
     then show ?thesis using card.empty by blast
   next
     case (Suc k)
     then have "\<exists>B \<subseteq> A. card B = k" using insert by auto
     then obtain B where "B \<subseteq> A" "card B = k" by auto
     moreover from this have "finite B" using insert.hyps finite_subset by auto
     ultimately have "card (insert x B) = n"
       using Suc insert.hyps card_insert_disjoint by fastforce
     then show ?thesis using \<open>B \<subseteq> A\<close> by blast
   qed
 qed auto
 
 locale matroid = indep_system +
   assumes augment_aux:
     "indep X \<Longrightarrow> indep Y \<Longrightarrow> card X = Suc (card Y) \<Longrightarrow> \<exists>x \<in> X - Y. indep (insert x Y)"
 begin
 
 lemma augment:
   assumes "indep X" "indep Y" "card Y < card X"
   shows "\<exists>x \<in> X - Y. indep (insert x Y)"
 proof -
   obtain X' where "X' \<subseteq> X" "card X' = Suc (card Y)"
     using assms card_subset_ex[of X "Suc (card Y)"] indep_finite by auto
   then obtain x where "x \<in> X' - Y"  "indep (insert x Y)"
     using assms augment_aux[of X' Y] indep_subset by auto
   then show ?thesis using \<open>X' \<subseteq> X\<close> by auto
 qed
 
 lemma augment_psubset:
   assumes "indep X" "indep Y" "Y \<subset> X"
   shows "\<exists>x \<in> X - Y. indep (insert x Y)"
   using assms augment psubset_card_mono indep_finite by blast
 
 subsection \<open>Minors\<close>
 
 text \<open>
   A subset of the ground set induces a matroid.
 \<close>
 
 lemma matroid_subset [simp, intro]:
   assumes "\<E> \<subseteq> carrier"
   shows "matroid \<E> (indep_in \<E>)"
   unfolding matroid_def matroid_axioms_def
 proof (safe, goal_cases indep_system augment)
   case indep_system
   then show ?case using indep_system_subset[OF assms] .
 next
   case (augment X Y)
   then show ?case using augment_aux[of X Y] unfolding indep_in_def by auto
 qed
 
 context
   fixes \<E>
   assumes "\<E> \<subseteq> carrier"
 begin
 
 interpretation \<E>: matroid \<E> "indep_in \<E>"
   using \<open>\<E> \<subseteq> carrier\<close> by auto
 
 lemmas augment_aux_indep_in = \<E>.augment_aux
 lemmas augment_indep_in = \<E>.augment
 lemmas augment_psubset_indep_in = \<E>.augment_psubset
 
 end
 
 subsection \<open>Bases\<close>
 
 lemma basis_card:
   assumes "basis B\<^sub>1"
   assumes "basis B\<^sub>2"
   shows "card B\<^sub>1 = card B\<^sub>2"
 proof (rule ccontr, goal_cases False)
   case False
   then have "card B\<^sub>1 < card B\<^sub>2 \<or> card B\<^sub>2 < card B\<^sub>1" by auto
   moreover {
     fix B\<^sub>1 B\<^sub>2
     assume "basis B\<^sub>1" "basis B\<^sub>2" "card B\<^sub>1 < card B\<^sub>2"
     then obtain x where "x \<in> B\<^sub>2 - B\<^sub>1" "indep (insert x B\<^sub>1)"
       using augment basisD by blast
     then have "x \<in> carrier - B\<^sub>1"
       using \<open>basis B\<^sub>1\<close> basisD indep_subset_carrier by blast
     then have "\<not> indep (insert x B\<^sub>1)" using \<open>basis B\<^sub>1\<close> basisD by auto
     then have "False" using \<open>indep (insert x B\<^sub>1)\<close> by auto
   }
   ultimately show ?case using assms by auto
 qed
 
 lemma basis_indep_card:
   assumes "indep X"
   assumes "basis B"
   shows "card X \<le> card B"
 proof -
   obtain B' where "basis B'" "X \<subseteq> B'" using assms indep_imp_subset_basis by auto
   then show ?thesis using assms basis_finite basis_card[of B B'] by (auto intro: card_mono)
 qed
 
 lemma basis_augment:
   assumes "basis B\<^sub>1" "basis B\<^sub>2" "x \<in> B\<^sub>1 - B\<^sub>2"
   shows "\<exists>y \<in> B\<^sub>2 - B\<^sub>1. basis (insert y (B\<^sub>1 - {x}))"
 proof -
   let ?B\<^sub>1 = "B\<^sub>1 - {x}"
   have "card ?B\<^sub>1 < card B\<^sub>2"
     using assms basis_card[of B\<^sub>1 B\<^sub>2] card_Diff1_less[OF basis_finite, of B\<^sub>1] by auto
   moreover have "indep ?B\<^sub>1" using assms basis_indep[of B\<^sub>1] indep_subset[of B\<^sub>1 ?B\<^sub>1] by auto
   ultimately obtain y where y: "y \<in> B\<^sub>2 - ?B\<^sub>1" "indep (insert y ?B\<^sub>1)"
     using assms augment[of B\<^sub>2 ?B\<^sub>1] basis_indep by auto
   let ?B\<^sub>1' = "insert y ?B\<^sub>1"
   have "basis ?B\<^sub>1'" using \<open>indep ?B\<^sub>1'\<close>
   proof (rule basisI, goal_cases "insert")
     case (insert x)
     have "card (insert x ?B\<^sub>1') > card B\<^sub>1"
     proof -
       have "card (insert x ?B\<^sub>1') = Suc (card ?B\<^sub>1')"
         using insert card.insert_remove[OF indep_finite, of ?B\<^sub>1'] y by auto
       also have "\<dots> = Suc (Suc (card ?B\<^sub>1))"
         using card.insert_remove[OF indep_finite, of ?B\<^sub>1] \<open>indep ?B\<^sub>1\<close> y by auto
       also have "\<dots> = Suc (card B\<^sub>1)"
         using assms basis_finite[of B\<^sub>1] card.remove[of B\<^sub>1] by auto
       finally show ?thesis by auto
     qed
     then have "\<not>indep (insert x (insert y ?B\<^sub>1))"
       using assms basis_indep_card[of "insert x (insert y ?B\<^sub>1)" B\<^sub>1] by auto
     moreover have "insert x (insert y ?B\<^sub>1) \<subseteq> carrier"
       using assms insert y basis_finite indep_subset_carrier by auto
     ultimately show ?case by auto
   qed
   then show ?thesis using assms y by auto
 qed
 
 context
   fixes \<E>
   assumes *: "\<E> \<subseteq> carrier"
 begin
 
 interpretation \<E>: matroid \<E> "indep_in \<E>"
   using \<open>\<E> \<subseteq> carrier\<close> by auto
 
 lemmas basis_in_card = \<E>.basis_card[OF basis_inD_aux[OF *] basis_inD_aux[OF *]]
 lemmas basis_in_indep_in_card = \<E>.basis_indep_card[OF _ basis_inD_aux[OF *]]
 
 lemma basis_in_augment:
   assumes "basis_in \<E> B\<^sub>1" "basis_in \<E> B\<^sub>2" "x \<in> B\<^sub>1 - B\<^sub>2"
   shows "\<exists>y \<in> B\<^sub>2 - B\<^sub>1. basis_in \<E> (insert y (B\<^sub>1 - {x}))"
   using assms \<E>.basis_augment unfolding basis_in_def by auto
 
 end
 
 subsection \<open>Circuits\<close>
 
 lemma circuit_elim:
   assumes "circuit C\<^sub>1" "circuit C\<^sub>2" "C\<^sub>1 \<noteq> C\<^sub>2" "x \<in> C\<^sub>1 \<inter> C\<^sub>2"
   shows "\<exists>C\<^sub>3 \<subseteq> (C\<^sub>1 \<union> C\<^sub>2) - {x}. circuit C\<^sub>3"
 proof -
   let ?C = "(C\<^sub>1 \<union> C\<^sub>2) - {x}"
   let ?carrier = "C\<^sub>1 \<union> C\<^sub>2"
 
   have assms': "circuit_in carrier C\<^sub>1" "circuit_in carrier C\<^sub>2"
     using assms circuit_imp_circuit_in by auto
 
   have "?C \<subseteq> carrier" using assms circuit_subset_carrier by auto
   show ?thesis
   proof (cases "indep ?C")
     case False
     then show ?thesis using dep_iff_supset_circuit \<open>?C \<subseteq> carrier\<close> by auto
   next
     case True
     then have "indep_in ?carrier ?C" using \<open>?C \<subseteq> carrier\<close> by (auto intro: indep_inI)
 
     have *: "?carrier \<subseteq> carrier" using assms circuit_subset_carrier by auto
     obtain y where y: "y \<in> C\<^sub>2" "y \<notin> C\<^sub>1" using assms circuit_subset_eq by blast
     then have "indep_in ?carrier (C\<^sub>2 - {y})"
       using assms' circuit_in_min_dep_in[OF * circuit_in_supI[OF *, of C\<^sub>2]] by auto
     then obtain B where B: "basis_in ?carrier B" "C\<^sub>2 - {y} \<subseteq> B"
       using * assms indep_in_imp_subset_basis_in[of ?carrier "C\<^sub>2 - {y}"] by auto
 
     have "y \<notin> B"
     proof (rule ccontr, goal_cases False)
       case False
       then have "C\<^sub>2 \<subseteq> B" using B by auto
       moreover have "circuit_in ?carrier C\<^sub>2" using * assms' circuit_in_supI by auto
       ultimately have "\<not> indep_in ?carrier B"
         using B basis_in_subset_carrier[OF *] supset_circuit_in_imp_dep_in[OF *] by auto
       then show False using assms B basis_in_indep_in[OF *] by auto
     qed
 
     have "C\<^sub>1 - B \<noteq> {}"
     proof (rule ccontr, goal_cases False)
       case False
       then have "C\<^sub>1 - (C\<^sub>1 \<inter> B) = {}" by auto
       then have "C\<^sub>1 = C\<^sub>1 \<inter> B" using assms circuit_subset_eq by auto
       moreover have "indep (C\<^sub>1 \<inter> B)"
         using assms B basis_in_indep_in[OF *] indep_in_subset[OF *, of B "C\<^sub>1 \<inter> B"] indep_in_indep
         by auto
       ultimately show ?case using assms circuitD by auto
     qed
     then obtain z where z: "z \<in> C\<^sub>1" "z \<notin> B" by auto
 
     have "y \<noteq> z" using y z by auto
     have "x \<in> C\<^sub>1" "x \<in> C\<^sub>2" using assms by auto
 
     have "finite ?carrier" using assms carrier_finite finite_subset by auto
     have "card B \<le> card (?carrier - {y, z})"
     proof (rule card_mono)
       show "finite (C\<^sub>1 \<union> C\<^sub>2 - {y, z})" using \<open>finite ?carrier\<close> by auto
     next
       show "B \<subseteq> C\<^sub>1 \<union> C\<^sub>2 - {y, z}"
         using B basis_in_subset_carrier[OF *, of B] \<open>y \<notin> B\<close> \<open>z \<notin> B\<close> by auto
     qed
     also have "\<dots> = card ?carrier - 2"
       using \<open>finite ?carrier\<close> \<open>y \<in> C\<^sub>2\<close> \<open>z \<in> C\<^sub>1\<close> \<open>y \<noteq> z\<close> card_Diff_subset_Int by auto
     also have "\<dots> < card ?carrier - 1"
     proof -
       have "card ?carrier = card C\<^sub>1 + card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)"
         using assms \<open>finite ?carrier\<close> card_Un_Int[of C\<^sub>1 C\<^sub>2] by auto
       also have "\<dots> = card C\<^sub>1 + (card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2))"
         using assms \<open>finite ?carrier\<close> card_mono[of C\<^sub>2] by auto
       also have "\<dots> = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)"
       proof -
         have "card (C\<^sub>2 - C\<^sub>1) = card C\<^sub>2 - card (C\<^sub>2 \<inter> C\<^sub>1)"
           using assms \<open>finite ?carrier\<close> card_Diff_subset_Int[of C\<^sub>2 C\<^sub>1] by auto
         also have "\<dots> = card C\<^sub>2 - card (C\<^sub>1 \<inter> C\<^sub>2)" by (simp add: inf_commute)
         finally show ?thesis by auto
       qed
       finally have "card (C\<^sub>1 \<union> C\<^sub>2) = card C\<^sub>1 + card (C\<^sub>2 - C\<^sub>1)" .
       moreover have "card C\<^sub>1 > 0" using assms circuit_nonempty \<open>finite ?carrier\<close> by auto
       moreover have "card (C\<^sub>2 - C\<^sub>1) > 0" using assms \<open>finite ?carrier\<close> \<open>y \<in> C\<^sub>2\<close> \<open>y \<notin> C\<^sub>1\<close> by auto
       ultimately show ?thesis by auto
     qed
     also have "\<dots> = card ?C"
       using \<open>finite ?carrier\<close> card_Diff_singleton \<open>x \<in> C\<^sub>1\<close> \<open>x \<in> C\<^sub>2\<close> by auto
     finally have "card B < card ?C" .
     then have False
       using basis_in_indep_in_card[OF *, of ?C B] B \<open>indep_in ?carrier ?C\<close> by auto
     then show ?thesis by auto
   qed
 qed
 
 lemma min_dep_imp_supset_circuit:
   assumes "indep X"
   assumes "circuit C"
   assumes "C \<subseteq> insert x X"
   shows "x \<in> C"
 proof (rule ccontr)
   assume "x \<notin> C"
   then have "C \<subseteq> X" using assms by auto
   then have "indep C" using assms indep_subset by auto
   then show False using assms circuitD by auto
 qed
 
 lemma min_dep_imp_ex1_supset_circuit:
   assumes "x \<in> carrier"
   assumes "indep X"
   assumes "\<not> indep (insert x X)"
   shows "\<exists>!C. circuit C \<and> C \<subseteq> insert x X"
 proof -
   obtain C where C: "circuit C" "C \<subseteq> insert x X"
     using assms indep_subset_carrier dep_iff_supset_circuit by auto
 
   show ?thesis
   proof (rule ex1I, goal_cases ex unique)
     show "circuit C \<and> C \<subseteq> insert x X" using C by auto
   next
     {
       fix C'
       assume C': "circuit C'" "C' \<subseteq> insert x X"
       have "C' = C"
       proof (rule ccontr)
         assume "C' \<noteq> C"
         moreover have "x \<in> C' \<inter> C" using C C' assms min_dep_imp_supset_circuit by auto
         ultimately have "\<not> indep (C' \<union> C - {x})"
           using circuit_elim[OF C(1) C'(1), of x] supset_circuit_imp_dep[of _ "C' \<union> C - {x}"] by auto
         moreover have "C' \<union> C - {x} \<subseteq> X" using C C' by auto
         ultimately show False using assms indep_subset by auto
       qed
     }
     then show "\<And>C'. circuit C' \<and> C' \<subseteq> insert x X \<Longrightarrow> C' = C"
       by auto
   qed
 qed
 
 lemma basis_ex1_supset_circuit:
   assumes "basis B"
   assumes "x \<in> carrier - B"
   shows "\<exists>!C. circuit C \<and> C \<subseteq> insert x B"
   using assms min_dep_imp_ex1_supset_circuit basisD by auto
 
 definition fund_circuit :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   "fund_circuit x B \<equiv> (THE C. circuit C \<and> C \<subseteq> insert x B)"
 
 lemma circuit_iff_fund_circuit:
   "circuit C \<longleftrightarrow> (\<exists>x B. x \<in> carrier - B \<and> basis B \<and> C = fund_circuit x B)"
 proof (safe, goal_cases LTR RTL)
   case LTR
   then obtain x where "x \<in> C" using circuit_nonempty by auto
   then have "indep (C - {x})" using LTR unfolding circuit_def by auto
   then obtain B where B: "basis B" "C - {x} \<subseteq> B" using indep_imp_subset_basis by auto
   then have "x \<in> carrier" using LTR circuit_subset_carrier \<open>x \<in> C\<close> by auto
   moreover have "x \<notin> B"
   proof (rule ccontr, goal_cases False)
     case False
     then have "C \<subseteq> B" using \<open>C - {x} \<subseteq> B\<close> by auto
     then have "\<not> indep B" using LTR B basis_subset_carrier supset_circuit_imp_dep by auto
     then show ?case using B basis_indep by auto
   qed
   ultimately show ?case
     unfolding fund_circuit_def
     using LTR B theI_unique[OF basis_ex1_supset_circuit[of B x], of C] by auto
 next
   case (RTL x B)
   then have "\<exists>!C. circuit C \<and> C \<subseteq> insert x B"
     using min_dep_imp_ex1_supset_circuit basisD[of B] by auto
   then show ?case
     unfolding fund_circuit_def
     using theI[of "\<lambda>C. circuit C \<and> C \<subseteq> insert x B"] by fastforce
 qed
 
 lemma fund_circuitI:
   assumes "basis B"
   assumes "x \<in> carrier - B"
   assumes "circuit C"
   assumes "C \<subseteq> insert x B"
   shows "fund_circuit x B = C"
   unfolding fund_circuit_def
   using assms theI_unique[OF basis_ex1_supset_circuit, of B x C] by auto
 
 definition fund_circuit_in where "fund_circuit_in \<E> x B \<equiv> matroid.fund_circuit \<E> (indep_in \<E>) x B"
 
 context
   fixes \<E>
   assumes *: "\<E> \<subseteq> carrier"
 begin
 
 interpretation \<E>: matroid \<E> "indep_in \<E>"
   using \<open>\<E> \<subseteq> carrier\<close> by auto
 
 lemma fund_circuit_inI_aux: "\<E>.fund_circuit x B = fund_circuit_in \<E> x B"
   unfolding fund_circuit_in_def by auto
 
 lemma circuit_in_elim:
   assumes "circuit_in \<E> C\<^sub>1" "circuit_in \<E> C\<^sub>2" "C\<^sub>1 \<noteq> C\<^sub>2" "x \<in> C\<^sub>1 \<inter> C\<^sub>2"
   shows "\<exists>C\<^sub>3 \<subseteq> (C\<^sub>1 \<union> C\<^sub>2) - {x}. circuit_in \<E> C\<^sub>3"
   using assms \<E>.circuit_elim unfolding circuit_in_def by auto
 
 lemmas min_dep_in_imp_supset_circuit_in = \<E>.min_dep_imp_supset_circuit[OF _ circuit_inD_aux[OF *]]
 
 lemma min_dep_in_imp_ex1_supset_circuit_in:
   assumes "x \<in> \<E>"
   assumes "indep_in \<E> X"
   assumes "\<not> indep_in \<E> (insert x X)"
   shows "\<exists>!C. circuit_in \<E> C \<and> C \<subseteq> insert x X"
   using assms \<E>.min_dep_imp_ex1_supset_circuit unfolding circuit_in_def by auto
 
 lemma basis_in_ex1_supset_circuit_in:
   assumes "basis_in \<E> B"
   assumes "x \<in> \<E> - B"
   shows "\<exists>!C. circuit_in \<E> C \<and> C \<subseteq> insert x B"
   using assms \<E>.basis_ex1_supset_circuit unfolding circuit_in_def basis_in_def by auto
 
 lemma fund_circuit_inI:
   assumes "basis_in \<E> B"
   assumes "x \<in> \<E> - B"
   assumes "circuit_in \<E> C"
   assumes "C \<subseteq> insert x B"
   shows "fund_circuit_in \<E> x B = C"
   using assms \<E>.fund_circuitI
   unfolding basis_in_def circuit_in_def fund_circuit_in_def by auto
 
 end
 
 context
   fixes \<E>
   assumes *: "\<E> \<subseteq> carrier"
 begin
 
 interpretation \<E>: matroid \<E> "indep_in \<E>"
   using \<open>\<E> \<subseteq> carrier\<close> by auto
 
 lemma fund_circuit_in_sub_cong:
   assumes "\<E>' \<subseteq> \<E>"
   assumes "x \<in> \<E>' - B"
   assumes "basis_in \<E>' B"
   shows "\<E>.fund_circuit_in \<E>' x B = fund_circuit_in \<E>' x B"
 proof -
   obtain C where C: "circuit_in \<E>' C" "C \<subseteq> insert x B"
     using * assms basis_in_ex1_supset_circuit_in[of \<E>' B x] by auto
   then have "fund_circuit_in \<E>' x B = C"
     using * assms fund_circuit_inI by auto
   also have "\<dots> = \<E>.fund_circuit_in \<E>' x B"
     using * assms C \<E>.fund_circuit_inI basis_in_sub_cong[of \<E>] circuit_in_sub_cong[of \<E>] by auto
   finally show ?thesis by auto
 qed
 
 end
 
 subsection \<open>Ranks\<close>
 
 abbreviation rank_of where "rank_of \<equiv> lower_rank_of"
 
 lemmas rank_of_def = lower_rank_of_def
 lemmas rank_of_sub_cong = lower_rank_of_sub_cong
 lemmas rank_of_le = lower_rank_of_le
 
 context
   fixes \<E>
   assumes *: "\<E> \<subseteq> carrier"
 begin
 
 interpretation \<E>: matroid \<E> "indep_in \<E>"
   using * by auto
 
 lemma lower_rank_of_eq_upper_rank_of: "lower_rank_of \<E> = upper_rank_of \<E>"
 proof -
   obtain B where "basis_in \<E> B" using basis_in_ex[OF *] by auto
   then have "{card B | B. basis_in \<E> B} = {card B}"
     by safe (auto dest: basis_in_card[OF *])
   then show ?thesis unfolding lower_rank_of_def upper_rank_of_def by auto
 qed
 
 lemma rank_of_eq_card_basis_in:
   assumes "basis_in \<E> B"
   shows "rank_of \<E> = card B"
 proof -
   have "{card B | B. basis_in \<E> B} = {card B}" using assms by safe (auto dest: basis_in_card[OF *])
   then show ?thesis unfolding rank_of_def by auto
 qed
 
 lemma rank_of_indep_in_le:
   assumes "indep_in \<E> X"
   shows "card X \<le> rank_of \<E>"
 proof -
   {
     fix B
     assume "basis_in \<E> B"
     moreover obtain B' where "basis_in \<E> B'" "X \<subseteq> B'"
       using assms indep_in_imp_subset_basis_in[OF *] by auto
     ultimately have "card X \<le> card B"
       using card_mono[OF basis_in_finite[OF *]] basis_in_card[OF *, of B B'] by auto
   }
   moreover have "finite {card B | B. basis_in \<E> B}"
     using collect_basis_in_finite[OF *] by auto
   ultimately show ?thesis
     unfolding rank_of_def using basis_in_ex[OF *] by auto
 qed
 
 end
 
 lemma rank_of_mono:
   assumes "X \<subseteq> Y"
   assumes "Y \<subseteq> carrier"
   shows "rank_of X \<le> rank_of Y"
 proof -
   obtain B\<^sub>X where B\<^sub>X: "basis_in X  B\<^sub>X" using assms basis_in_ex[of X] by auto
   moreover obtain B\<^sub>Y where B\<^sub>Y: "basis_in Y B\<^sub>Y" using assms basis_in_ex[of Y] by auto
   moreover have "card B\<^sub>X \<le> card B\<^sub>Y"
     using assms basis_in_indep_in_card[OF _ _ B\<^sub>Y] basis_in_indep_in[OF _ B\<^sub>X] indep_in_subI_subset
     by auto
   ultimately show ?thesis using assms rank_of_eq_card_basis_in by auto
 qed
 
 lemma rank_of_insert_le:
   assumes "X \<subseteq> carrier"
   assumes "x \<in> carrier"
   shows "rank_of (insert x X) \<le> Suc (rank_of X)"
 proof -
   obtain B where B: "basis_in X B" using assms basis_in_ex[of X] by auto
   have "basis_in (insert x X) B \<or> basis_in (insert x X) (insert x B)"
   proof -
     obtain B' where B': "B' \<subseteq> insert x X - X" "basis_in (insert x X) (B \<union> B')"
       using assms B basis_in_subI[of "insert x X" X B] by auto
     then have "B' = {} \<or> B' = {x}" by auto
     then show ?thesis
     proof
       assume "B' = {}"
       then have "basis_in (insert x X) B" using B' by auto
       then show ?thesis by auto
     next
       assume "B' = {x}"
       then have "basis_in (insert x X) (insert x B)" using B' by auto
       then show ?thesis by auto
     qed
   qed
   then show ?thesis
   proof
     assume "basis_in (insert x X) B"
     then show ?thesis
       using assms B rank_of_eq_card_basis_in by auto
   next
     assume "basis_in (insert x X) (insert x B)"
     then have "rank_of (insert x X) = card (insert x B)"
       using assms rank_of_eq_card_basis_in by auto
     also have "\<dots> = Suc (card (B - {x}))"
       using assms card.insert_remove[of B x] using B basis_in_finite by auto
     also have "\<dots> \<le> Suc (card B)"
       using assms B basis_in_finite card_Diff1_le[of B] by auto
     also have "\<dots> = Suc (rank_of X)"
       using assms B rank_of_eq_card_basis_in by auto
     finally show ?thesis .
   qed
 qed
 
 lemma rank_of_Un_Int_le:
   assumes "X \<subseteq> carrier"
   assumes "Y \<subseteq> carrier"
   shows "rank_of (X \<union> Y) + rank_of (X \<inter> Y) \<le> rank_of X + rank_of Y"
 proof -
   obtain B_Int where B_Int: "basis_in (X \<inter> Y) B_Int" using assms basis_in_ex[of "X \<inter> Y"] by auto
   then have "indep_in (X \<union> Y) B_Int"
     using assms indep_in_subI_subset[OF _ basis_in_indep_in[of "X \<inter> Y" B_Int], of "X \<union> Y"] by auto
   then obtain B_Un where B_Un: "basis_in (X \<union> Y) B_Un" "B_Int \<subseteq> B_Un"
     using assms indep_in_imp_subset_basis_in[of "X \<union> Y" B_Int] by auto
 
   have "card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y)) = card ((B_Un \<inter> X) \<union> (B_Un \<inter> Y)) + card ((B_Un \<inter> X) \<inter> (B_Un \<inter> Y))"
     by (simp add: inf_assoc inf_left_commute inf_sup_distrib1)
   also have "\<dots> = card (B_Un \<inter> X) + card (B_Un \<inter> Y)"
   proof -
     have "finite (B_Un \<inter> X)" "finite (B_Un \<inter> Y)"
       using assms finite_subset[OF _ carrier_finite] by auto
     then show ?thesis using card_Un_Int[of "B_Un \<inter> X" "B_Un \<inter> Y"] by auto
   qed
   also have "\<dots> \<le> rank_of X + rank_of Y"
   proof -
     have "card (B_Un \<inter> X) \<le> rank_of X"
     proof -
       have "indep_in X (B_Un \<inter> X)" using assms basis_in_indep_in[OF _ B_Un(1)] indep_in_subI by auto
       then show ?thesis using assms rank_of_indep_in_le by auto
     qed
     moreover have "card (B_Un \<inter> Y) \<le> rank_of Y"
     proof -
       have "indep_in Y (B_Un \<inter> Y)" using assms basis_in_indep_in[OF _ B_Un(1)] indep_in_subI by auto
       then show ?thesis using assms rank_of_indep_in_le by auto
     qed
     ultimately show ?thesis by auto
   qed
   finally have "rank_of X + rank_of Y \<ge> card (B_Un \<inter> (X \<union> Y)) + card (B_Un \<inter> (X \<inter> Y))" .
   moreover have "B_Un \<inter> (X \<union> Y) = B_Un" using assms basis_in_subset_carrier[OF _ B_Un(1)] by auto
   moreover have "B_Un \<inter> (X \<inter> Y) = B_Int"
   proof -
     have "card (B_Un \<inter> (X \<inter> Y)) \<le> card B_Int"
     proof -
       have "indep_in (X \<inter> Y) (B_Un \<inter> (X \<inter> Y))"
         using assms basis_in_indep_in[OF _ B_Un(1)] indep_in_subI by auto
       then show ?thesis using assms basis_in_indep_in_card[of "X \<inter> Y" _ B_Int] B_Int by auto
     qed
     moreover have "finite (B_Un \<inter> (X \<inter> Y))"
       using assms carrier_finite finite_subset[of "B_Un \<inter> (X \<inter> Y)"] by auto
     moreover have "B_Int \<subseteq> B_Un \<inter> (X \<inter> Y)"
       using assms B_Un B_Int basis_in_subset_carrier[of "X \<inter> Y" B_Int] by auto
     ultimately show ?thesis using card_seteq by blast
   qed
   ultimately have "rank_of X + rank_of Y \<ge> card B_Un + card B_Int" by auto
   moreover have "card B_Un = rank_of (X \<union> Y)"
     using assms rank_of_eq_card_basis_in[OF _ B_Un(1)] by auto
   moreover have "card B_Int = rank_of (X \<inter> Y)"
     using assms rank_of_eq_card_basis_in[OF _ B_Int] by fastforce
   ultimately show "rank_of X + rank_of Y \<ge> rank_of (X \<union> Y) + rank_of (X \<inter> Y)" by auto
 qed
 
 lemma rank_of_Un_absorbI:
   assumes "X \<subseteq> carrier" "Y \<subseteq> carrier"
   assumes "\<And>y. y \<in> Y - X \<Longrightarrow> rank_of (insert y X) = rank_of X"
   shows "rank_of (X \<union> Y) = rank_of X"
 proof -
   have "finite (Y - X)" using finite_subset[OF \<open>Y \<subseteq> carrier\<close>] carrier_finite by auto
   then show ?thesis using assms
   proof (induction "Y - X" arbitrary: Y rule: finite_induct )
     case empty
     then have "X \<union> Y = X" by auto
     then show ?case by auto
   next
     case (insert y F)
     have "rank_of (X \<union> Y) + rank_of X \<le> rank_of X + rank_of X"
     proof -
       have "rank_of (X \<union> Y) + rank_of X = rank_of ((X \<union> (Y - {y})) \<union> (insert y X)) + rank_of ((X \<union> (Y - {y})) \<inter> (insert y X))"
       proof -
         have "X \<union> Y = (X \<union> (Y - {y})) \<union> (insert y X)" "X = (X \<union> (Y - {y})) \<inter> (insert y X)" using insert by auto
         then show ?thesis by auto
       qed
       also have "\<dots> \<le> rank_of (X \<union> (Y - {y})) +  rank_of (insert y X)"
       proof (rule rank_of_Un_Int_le)
         show "X \<union> (Y - {y}) \<subseteq> carrier" using insert by auto
       next
         show "insert y X \<subseteq> carrier" using insert by auto
       qed
       also have "\<dots> = rank_of (X \<union> (Y - {y})) + rank_of X"
       proof -
         have "y \<in> Y - X" using insert by auto
         then show ?thesis using insert by auto
       qed
       also have "\<dots> = rank_of X + rank_of X"
       proof -
         have "F = (Y - {y}) - X" "Y - {y} \<subseteq> carrier" using insert by auto
         then show ?thesis using insert insert(3)[of "Y - {y}"] by auto
       qed
       finally show ?thesis .
     qed
     moreover have "rank_of (X \<union> Y) + rank_of X \<ge> rank_of X + rank_of X"
       using insert rank_of_mono by auto
     ultimately show ?case by auto
   qed
 qed
 
 lemma indep_iff_rank_of:
   assumes "X \<subseteq> carrier"
   shows "indep X \<longleftrightarrow> rank_of X = card X"
 proof (standard, goal_cases LTR RTL)
   case LTR
   then have "indep_in X X" by (auto intro: indep_inI)
   then have "basis_in X X" by (auto intro: basis_inI[OF assms])
   then show ?case using rank_of_eq_card_basis_in[OF assms] by auto
 next
   case RTL
   obtain B where B: "basis_in X B" using basis_in_ex[OF assms] by auto
   then have "card B = card X" using RTL rank_of_eq_card_basis_in[OF assms] by auto
   then have "B = X"
     using basis_in_subset_carrier[OF assms B] card_seteq[OF finite_subset[OF assms carrier_finite]]
     by auto
   then show ?case using basis_in_indep_in[OF assms B] indep_in_indep by auto
 qed
 
 lemma basis_iff_rank_of:
   assumes "X \<subseteq> carrier"
   shows "basis X \<longleftrightarrow> rank_of X = card X \<and> rank_of X = rank_of carrier"
 proof (standard, goal_cases LTR RTL)
   case LTR
   then have "rank_of X = card X" using assms indep_iff_rank_of basis_indep by auto
   moreover have "\<dots> = rank_of carrier"
     using LTR rank_of_eq_card_basis_in[of carrier X] basis_iff_basis_in by auto
   ultimately show ?case by auto
 next
   case RTL
   show ?case
   proof (rule basisI)
     show "indep X" using assms RTL indep_iff_rank_of by blast
   next
     fix x
     assume x: "x \<in> carrier - X"
     show "\<not> indep (insert x X)"
     proof (rule ccontr, goal_cases False)
       case False
       then have "card (insert x X) \<le> rank_of carrier"
         using assms x indep_inI rank_of_indep_in_le by auto
       also have "\<dots> = card X" using RTL by auto
       finally show ?case using finite_subset[OF assms carrier_finite] x by auto
     qed
   qed
 qed
 
 lemma circuit_iff_rank_of:
   assumes "X \<subseteq> carrier"
   shows "circuit X \<longleftrightarrow> X \<noteq> {} \<and> (\<forall>x \<in> X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)"
 proof (standard, goal_cases LTR RTL)
   case LTR
   then have "X \<noteq> {}" using circuit_nonempty by auto
   moreover have indep_remove: "\<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})"
   proof -
     fix x
     assume "x \<in> X"
     then have "indep (X - {x})" using circuit_min_dep[OF LTR] by auto
     moreover have "X - {x} \<subseteq> carrier" using assms by auto
     ultimately show "rank_of (X - {x}) = card (X - {x})" using indep_iff_rank_of by auto
   qed
   moreover have "\<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X"
   proof -
     fix x
     assume *: "x \<in> X"
     have "rank_of X \<le> card X" using assms rank_of_le by auto
     moreover have "rank_of X \<noteq> card X" using assms LTR circuitD indep_iff_rank_of[of X] by auto
     ultimately have "rank_of X < card X" by auto
     then have "rank_of X \<le> card (X - {x})" using * finite_subset[OF assms] carrier_finite by auto
     also have "\<dots> = rank_of (X - {x})" using indep_remove \<open>x \<in> X\<close> by auto
     finally show "rank_of (X - {x}) = rank_of X" using assms rank_of_mono[of "X - {x}" X] by auto
   qed
   ultimately show ?case by auto
 next
   case RTL
   then have "X \<noteq> {}"
     and indep_remove: "\<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = card (X - {x})"
     and dep: "\<And>x. x \<in> X \<Longrightarrow> rank_of (X - {x}) = rank_of X"
     by auto
   show ?case using assms
   proof (rule circuitI)
     obtain x where x: "x \<in> X" using \<open>X \<noteq> {}\<close> by auto
     then have "rank_of X = card (X - {x})" using dep indep_remove by auto
     also have "\<dots> < card X" using card_Diff1_less[OF finite_subset[OF assms carrier_finite] x] .
     finally show "\<not> indep X" using indep_iff_rank_of[OF assms] by auto
   next
     fix x
     assume "x \<in> X"
     then show "indep (X - {x})" using assms indep_remove[of x] indep_iff_rank_of[of "X - {x}"]
       by auto
   qed
 qed
 
 context
   fixes \<E>
   assumes *: "\<E> \<subseteq> carrier"
 begin
 
 interpretation \<E>: matroid \<E> "indep_in \<E>"
   using * by auto
 
 lemma indep_in_iff_rank_of:
   assumes "X \<subseteq> \<E>"
   shows "indep_in \<E> X \<longleftrightarrow> rank_of X = card X"
   using assms \<E>.indep_iff_rank_of rank_of_sub_cong[OF * assms] by auto
 
 lemma basis_in_iff_rank_of:
   assumes "X \<subseteq> \<E>"
   shows "basis_in \<E> X \<longleftrightarrow> rank_of X = card X \<and> rank_of X = rank_of \<E>"
   using \<E>.basis_iff_rank_of[OF assms] rank_of_sub_cong[OF *] assms
   unfolding basis_in_def by auto
 
 lemma circuit_in_iff_rank_of:
   assumes "X \<subseteq> \<E>"
   shows "circuit_in \<E> X \<longleftrightarrow> X \<noteq> {} \<and> (\<forall>x \<in> X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)"
 proof -
   have "circuit_in \<E> X \<longleftrightarrow> \<E>.circuit X" unfolding circuit_in_def ..
   also have "\<dots> \<longleftrightarrow>  X \<noteq> {} \<and> (\<forall>x \<in> X. \<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X)"
     using \<E>.circuit_iff_rank_of[OF assms] .
   also have "\<dots> \<longleftrightarrow> X \<noteq> {} \<and> (\<forall>x \<in> X. rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X)"
   proof -
     {
       fix x
       have "\<E>.rank_of (X - {x}) = rank_of (X - {x})" "\<E>.rank_of X = rank_of X"
         using assms rank_of_sub_cong[OF *, of "X - {x}"] rank_of_sub_cong[OF *, of X] by auto
       then have "\<E>.rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = \<E>.rank_of X \<longleftrightarrow> rank_of (X - {x}) = card (X - {x}) \<and> card (X - {x}) = rank_of X"
         by auto
     }
-    then show ?thesis by auto
+    then show ?thesis
+      by (auto simp: simp del: card_Diff_insert)
   qed
   finally show ?thesis .
 qed
 
 end
 
 subsection \<open>Closure\<close>
 
 definition cl :: "'a set \<Rightarrow> 'a set" where
   "cl X \<equiv> {x \<in> carrier. rank_of (insert x X) = rank_of X}"
 
 lemma clI:
   assumes "x \<in> carrier"
   assumes "rank_of (insert x X) = rank_of X"
   shows "x \<in> cl X"
   unfolding cl_def using assms by auto
 
 lemma cl_altdef:
   assumes "X \<subseteq> carrier"
   shows "cl X = \<Union>{Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}"
 proof -
   {
     fix x
     assume *: "x \<in> cl X"
     have "x \<in> \<Union>{Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}"
     proof
       show "insert x X \<in> {Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}"
         using assms * unfolding cl_def by auto
     qed auto
   }
   moreover {
     fix x
     assume *: "x \<in> \<Union>{Y \<in> Pow carrier. X \<subseteq> Y \<and> rank_of Y = rank_of X}"
     then obtain Y where Y: "x \<in> Y" "Y \<subseteq> carrier" "X \<subseteq> Y" "rank_of Y = rank_of X" by auto
     have "rank_of (insert x X) = rank_of X"
     proof -
       have "rank_of (insert x X) \<le> rank_of X"
       proof -
         have "insert x X \<subseteq> Y" using Y by auto
         then show ?thesis using rank_of_mono[of "insert x X" Y] Y by auto
       qed
       moreover have "rank_of X \<le> rank_of (insert x X)" using Y by (auto intro: rank_of_mono)
       ultimately show ?thesis by auto
     qed
     then have "x \<in> cl X" using * unfolding cl_def by auto
   }
   ultimately show ?thesis by blast
 qed
 
 
 lemma cl_rank_of: "x \<in> cl X \<Longrightarrow> rank_of (insert x X) = rank_of X"
   unfolding cl_def by auto
 
 lemma cl_subset_carrier: "cl X \<subseteq> carrier"
   unfolding cl_def by auto
 
 lemmas clD = cl_rank_of cl_subset_carrier
 
 lemma cl_subset:
   assumes "X \<subseteq> carrier"
   shows "X \<subseteq> cl X"
   using assms using insert_absorb[of _ X] by (auto intro!: clI)
 
 lemma cl_mono:
   assumes "X \<subseteq> Y"
   assumes "Y \<subseteq> carrier"
   shows "cl X \<subseteq> cl Y"
 proof
   fix x
   assume "x \<in> cl X"
   then have "x \<in> carrier" using cl_subset_carrier by auto
 
   have "insert x X \<subseteq> carrier"
     using assms \<open>x \<in> cl X\<close> cl_subset_carrier[of X] by auto
   then interpret X_insert: matroid "insert x X" "indep_in (insert x X)" by auto
 
   have "insert x Y \<subseteq> carrier"
     using assms \<open>x \<in> cl X\<close> cl_subset_carrier[of X] by auto
   then interpret Y_insert: matroid "insert x Y" "indep_in (insert x Y)" by auto
 
   show "x \<in> cl Y" using \<open>x \<in> carrier\<close>
   proof (rule clI, cases "x \<in> X")
     case True
     then show "rank_of (insert x Y) = rank_of Y" using assms insert_absorb[of x Y] by auto
   next
     case False
     obtain B\<^sub>X where B\<^sub>X: "basis_in X B\<^sub>X" using assms basis_in_ex[of X] by auto
 
     have "basis_in (insert x X) B\<^sub>X"
     proof -
       have "rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of (insert x X)"
       proof -
         have "rank_of B\<^sub>X = card B\<^sub>X \<and> rank_of B\<^sub>X = rank_of X"
           using assms B\<^sub>X
             basis_in_subset_carrier[where \<E> = X and X = B\<^sub>X]
             basis_in_iff_rank_of[where \<E> = X and X = B\<^sub>X]
           by blast
         then show ?thesis using cl_rank_of[OF \<open>x \<in> cl X\<close>] by auto
       qed
       then show ?thesis
         using assms basis_in_subset_carrier[OF _ B\<^sub>X] \<open>x \<in> carrier\<close> basis_in_iff_rank_of[of "insert x X" B\<^sub>X]
         by auto
     qed
 
     have "indep_in (insert x Y) B\<^sub>X"
       using assms basis_in_indep_in[OF _ B\<^sub>X] indep_in_subI_subset[of X "insert x Y"] by auto
     then obtain B\<^sub>Y where B\<^sub>Y: "basis_in (insert x Y) B\<^sub>Y" "B\<^sub>X \<subseteq> B\<^sub>Y"
       using assms \<open>x \<in> carrier\<close> indep_in_iff_subset_basis_in[of "insert x Y" B\<^sub>X] by auto
 
     have "basis_in Y B\<^sub>Y"
     proof -
       have "x \<notin> B\<^sub>Y"
       proof (rule ccontr, goal_cases False)
         case False
         then have "insert x B\<^sub>X \<subseteq> B\<^sub>Y" using \<open>B\<^sub>X \<subseteq> B\<^sub>Y\<close> by auto
         then have "indep_in (insert x Y) (insert x B\<^sub>X)"
           using assms \<open>x \<in> carrier\<close>
             B\<^sub>Y basis_in_indep_in[where \<E> = "insert x Y" and X = B\<^sub>Y]
             indep_in_subset[where \<E> = "insert x Y" and X = B\<^sub>Y and Y = "insert x B\<^sub>X"]
           by auto
         then have "indep_in (insert x X) (insert x B\<^sub>X)"
           using assms B\<^sub>X
             basis_in_subset_carrier[where \<E> = X and X = B\<^sub>X]
             indep_in_supI[where \<E> = "insert x Y" and \<E>' = "insert x X" and X = "insert x B\<^sub>X"]
           by auto
         moreover have "x \<in> insert x X - B\<^sub>X"
           using assms \<open>x \<notin> X\<close> B\<^sub>X basis_in_subset_carrier[where \<E> = X and X = B\<^sub>X] by auto
         ultimately show ?case
           using assms \<open>x \<in> carrier\<close> \<open>basis_in (insert x X) B\<^sub>X\<close>
             basis_in_max_indep_in[where \<E> = "insert x X" and X = B\<^sub>X and x = x]
           by auto
       qed
       then show ?thesis
       using assms \<open>x \<in> carrier\<close> B\<^sub>Y basis_in_subset_carrier[of "insert x Y" B\<^sub>Y]
         basis_in_supI[where \<E> = "insert x Y" and \<E>' = Y and B = B\<^sub>Y] by auto
     qed
 
     show "rank_of (insert x Y) = rank_of Y"
     proof -
       have "rank_of (insert x Y) = card B\<^sub>Y"
         using assms \<open>x \<in> carrier\<close> \<open>basis_in (insert x Y) B\<^sub>Y\<close> basis_in_subset_carrier
         using basis_in_iff_rank_of[where \<E> = "insert x Y" and X = B\<^sub>Y]
         by auto
       also have "\<dots> = rank_of Y"
         using assms \<open>x \<in> carrier\<close> \<open>basis_in Y B\<^sub>Y\<close> basis_in_subset_carrier
         using basis_in_iff_rank_of[where \<E> = Y and X = B\<^sub>Y]
         by auto
       finally show ?thesis .
     qed
   qed
 qed
 
 lemma cl_insert_absorb:
   assumes "X \<subseteq> carrier"
   assumes "x \<in> cl X"
   shows "cl (insert x X) = cl X"
 proof
   show "cl (insert x X) \<subseteq> cl X"
   proof (standard, goal_cases elem)
     case (elem y)
     then have *: "x \<in> carrier" "y \<in> carrier" using assms cl_subset_carrier by auto
 
     have "rank_of (insert y X) = rank_of (insert y (insert x X))"
     proof -
       have "rank_of (insert y X) \<le> rank_of (insert y (insert x X))"
         using assms * by (auto intro: rank_of_mono)
       moreover have "rank_of (insert y (insert x X)) = rank_of (insert y X)"
       proof -
         have "insert y (insert x X) = insert x (insert y X)" by auto
         then have "rank_of (insert y (insert x X)) = rank_of (insert x (insert y X))" by auto
         also have "\<dots> = rank_of (insert y X)"
         proof -
           have "cl X \<subseteq> cl (insert y X)" by (rule cl_mono) (auto simp add: assms \<open>y \<in> carrier\<close>)
           then have "x \<in> cl (insert y X)" using assms by auto
           then show ?thesis unfolding cl_def by auto
         qed
         finally show ?thesis .
       qed
       ultimately show ?thesis by auto
     qed
     also have "\<dots> = rank_of (insert x X)" using elem using cl_rank_of by auto
     also have "\<dots> = rank_of X" using assms cl_rank_of by auto
     finally show "y \<in> cl X" using * by (auto intro: clI)
   qed
 next
   have "insert x X \<subseteq> carrier" using assms cl_subset_carrier by auto
   moreover have "X \<subseteq> insert x X" using assms by auto
   ultimately show "cl X \<subseteq> cl (insert x X)" using assms cl_subset_carrier cl_mono by auto
 qed
 
 lemma cl_cl_absorb:
   assumes "X \<subseteq> carrier"
   shows "cl (cl X) = cl X"
 proof
   show "cl (cl X) \<subseteq> cl X"
   proof (standard, goal_cases elem)
     case (elem x)
     then have "x \<in> carrier" using cl_subset_carrier by auto
     then show ?case
     proof (rule clI)
       have "rank_of (insert x X) \<ge> rank_of X"
         using assms \<open>x \<in> carrier\<close> rank_of_mono[of X "insert x X"] by auto
       moreover have "rank_of (insert x X) \<le> rank_of X"
       proof -
         have "rank_of (insert x X) \<le> rank_of (insert x (cl X))"
           using assms \<open>x \<in> carrier\<close> cl_subset_carrier cl_subset[of X]
                 rank_of_mono[of "insert x X" "insert x (cl X)"] by auto
         also have "\<dots> = rank_of (cl X)" using elem cl_rank_of by auto
         also have "\<dots> = rank_of (X \<union> (cl X - X))"
           using Diff_partition[OF cl_subset[OF assms]] by auto
         also have "\<dots> = rank_of X" using \<open>X \<subseteq> carrier\<close>
         proof (rule rank_of_Un_absorbI)
           show "cl X - X \<subseteq> carrier" using assms cl_subset_carrier by auto
         next
           fix y
           assume "y \<in> cl X - X - X"
           then show "rank_of (insert y X) = rank_of X" unfolding cl_def by auto
         qed
         finally show ?thesis .
       qed
       ultimately show "rank_of (insert x X) = rank_of X" by auto
     qed
   qed
 next
   show "cl X \<subseteq> cl (cl X)" using cl_subset[OF cl_subset_carrier] by auto
 qed
 
 lemma cl_augment:
   assumes "X \<subseteq> carrier"
   assumes "x \<in> carrier"
   assumes "y \<in> cl (insert x X) - cl X"
   shows "x \<in> cl (insert y X)"
   using \<open>x \<in> carrier\<close>
 proof (rule clI)
   have "rank_of (insert y X) \<le> rank_of (insert x (insert y X))"
     using assms cl_subset_carrier by (auto intro: rank_of_mono)
   moreover have "rank_of (insert x (insert y X)) \<le> rank_of (insert y X)"
   proof -
     have "rank_of (insert x (insert y X)) = rank_of (insert y (insert x X))"
     proof -
       have "insert x (insert y X) = insert y (insert x X)" by auto
       then show ?thesis by auto
     qed
     also have "rank_of (insert y (insert x X)) = rank_of (insert x X)"
       using assms cl_def by auto
     also have "\<dots> \<le> Suc (rank_of X)"
       using assms cl_subset_carrier by (auto intro: rank_of_insert_le)
     also have "\<dots> = rank_of (insert y X)"
     proof -
       have "rank_of (insert y X) \<le> Suc (rank_of X)"
         using assms cl_subset_carrier by (auto intro: rank_of_insert_le)
       moreover have "rank_of (insert y X) \<noteq> rank_of X"
         using assms cl_def by auto
       moreover have "rank_of X \<le> rank_of (insert y X)"
         using assms cl_subset_carrier by (auto intro: rank_of_mono)
       ultimately show ?thesis by auto
     qed
     finally show ?thesis .
   qed
   ultimately show "rank_of (insert x (insert y X)) = rank_of (insert y X)" by auto
 qed
 
 lemma clI_insert:
   assumes "x \<in> carrier"
   assumes "indep X"
   assumes "\<not> indep (insert x X)"
   shows "x \<in> cl X"
   using \<open>x \<in> carrier\<close>
 proof (rule clI)
   have *: "X \<subseteq> carrier" using assms indep_subset_carrier by auto
   then have **: "insert x X \<subseteq> carrier" using assms by auto
 
   have "indep_in (insert x X) X" using assms by (auto intro: indep_inI)
   then obtain B where B: "basis_in (insert x X) B" "X \<subseteq> B"
     using assms indep_in_iff_subset_basis_in[OF **] by auto
   have "x \<notin> B"
   proof (rule ccontr, goal_cases False)
     case False
     then have "indep_in (insert x X) (insert x X)"
       using B indep_in_subset[OF ** basis_in_indep_in[OF **]] by auto
     then show ?case using assms indep_in_indep by auto
   qed
 
   have "basis_in X B" using *
   proof (rule basis_inI, goal_cases indep max_indep)
     case indep
     show ?case
     proof (rule indep_in_supI[where \<E> = "insert x X"])
       show "B \<subseteq> X" using B basis_in_subset_carrier[OF **] \<open>x \<notin> B\<close> by auto
     next
       show "indep_in (insert x X) B" using basis_in_indep_in[OF ** B(1)] .
     qed auto
   next
     case (max_indep y)
     then have "\<not> indep_in (insert x X) (insert y B)"
       using B basis_in_max_indep_in[OF **] by auto
     then show ?case by (auto intro: indep_in_subI_subset)
   qed
   then show "rank_of (insert x X) = rank_of X"
     using B rank_of_eq_card_basis_in[OF *] rank_of_eq_card_basis_in[OF **] by auto
 qed
 
 lemma indep_in_carrier [simp]: "indep_in carrier = indep"
   using indep_subset_carrier by (auto simp: indep_in_def fun_eq_iff)
 
 context
   fixes I
   defines "I \<equiv> (\<lambda>X. X \<subseteq> carrier \<and> (\<forall>x\<in>X. x \<notin> cl (X - {x})))"
 begin
 
 lemma I_mono: "I Y" if "Y \<subseteq> X" "I X" for X Y :: "'a set"
 proof -
   have "\<forall>x\<in>Y. x \<notin> cl (Y - {x})"
   proof (intro ballI)
     fix x assume x: "x \<in> Y"
     with that have "cl (Y - {x}) \<subseteq> cl (X - {x})"
       by (intro cl_mono) (auto simp: I_def)
     with that and x show "x \<notin> cl (Y - {x})" by (auto simp: I_def)
   qed
   with that show ?thesis by (auto simp: I_def)
 qed
 
 lemma clI':
   assumes "I X" "x \<in> carrier" "\<not>I (insert x X)"
   shows   "x \<in> cl X"
 proof -
   from assms have x: "x \<notin> X" by (auto simp: insert_absorb)
   from assms obtain y where y: "y \<in> insert x X" "y \<in> cl (insert x X - {y})"
     by (force simp: I_def)
   show "x \<in> cl X"
   proof (cases "x = y")
     case True
     thus ?thesis using assms x y by (auto simp: I_def)
   next
     case False
     have "y \<in> cl (insert x X - {y})" by fact
     also from False have "insert x X - {y} = insert x (X - {y})" by auto
     finally have "y \<in> cl (insert x (X - {y})) - cl (X - {y})"
       using assms False y unfolding I_def by blast
     hence "x \<in> cl (insert y (X - {y}))"
       using cl_augment[of "X - {y}" x y] assms False y by (auto simp: I_def)
     also from y and False have "insert y (X - {y}) = X" by auto
     finally show ?thesis .
   qed
 qed
 
 
 lemma matroid_I: "matroid carrier I"
 proof (unfold_locales, goal_cases)
   show "finite carrier" by (rule carrier_finite)
 next
   case (4 X Y)
   have "\<forall>x\<in>Y. x \<notin> cl (Y - {x})"
   proof (intro ballI)
     fix x assume x: "x \<in> Y"
     with 4 have "cl (Y - {x}) \<subseteq> cl (X - {x})"
       by (intro cl_mono) (auto simp: I_def)
     with 4 and x show "x \<notin> cl (Y - {x})" by (auto simp: I_def)
   qed
   with 4 show ?case by (auto simp: I_def)
 next
   case (5 X Y)
   have "~(\<exists>X Y. I X \<and> I Y \<and> card X < card Y \<and> (\<forall>x\<in>Y-X. \<not>I (insert x X)))"
   proof
     assume *: "\<exists>X Y. I X \<and> I Y \<and> card X < card Y \<and> (\<forall>x\<in>Y-X. \<not>I (insert x X))" (is "\<exists>X Y. ?P X Y")
     define n where "n = Max ((\<lambda>(X, Y). card (X \<inter> Y)) ` {(X, Y). ?P X Y})"
     have "{(X, Y). ?P X Y} \<subseteq> Pow carrier \<times> Pow carrier"
       by (auto simp: I_def)
     hence finite: "finite {(X, Y). ?P X Y}"
       by (rule finite_subset) (insert carrier_finite, auto)
     hence "n \<in> ((\<lambda>(X, Y). card (X \<inter> Y)) ` {(X, Y). ?P X Y})"
       unfolding n_def using * by (intro Max_in finite_imageI) auto
     then obtain X Y where XY: "?P X Y" "n = card (X \<inter> Y)"
       by auto
     hence finite': "finite X" "finite Y"
       using finite_subset[OF _ carrier_finite] XY by (auto simp: I_def)
     from XY finite' have "~(Y \<subseteq> X)"
       using card_mono[of X Y] by auto
     then obtain y where y: "y \<in> Y - X" by blast
 
     have False
     proof (cases "X \<subseteq> cl (Y - {y})")
       case True
       from y XY have [simp]: "y \<in> carrier" by (auto simp: I_def)
       assume "X \<subseteq> cl (Y - {y})"
       hence "cl X \<subseteq> cl (cl (Y - {y}))"
         by (intro cl_mono cl_subset_carrier)
       also have "\<dots> = cl (Y - {y})"
         using XY by (intro cl_cl_absorb) (auto simp: I_def)
       finally have "cl X \<subseteq> cl (Y - {y})" .
       moreover have "y \<notin> cl (Y - {y})"
         using y I_def XY(1) by blast
       ultimately have "y \<notin> cl X" by blast
       thus False unfolding I_def
         using XY y clI' \<open>y \<in> carrier\<close> by blast
     next
       case False
       with y XY have [simp]: "y \<in> carrier" by (auto simp: I_def)
       assume "\<not>(X \<subseteq> cl (Y - {y}))"
       then obtain t where t: "t \<in> X" "t \<notin> cl (Y - {y})"
         by auto
       with XY have [simp]: "t \<in> carrier" by (auto simp: I_def)
 
       have "t \<in> X - Y"
         using t y clI[of t "Y - {y}"] by (cases "t = y") (auto simp: insert_absorb)
       moreover have "I  (Y - {y})" using XY(1) I_mono[of "Y - {y}" Y] by blast
       ultimately have *: "I (insert t (Y - {y}))"
         using clI'[of "Y - {y}" t] t by auto
 
       from XY have "finite Y"
         by (intro finite_subset[OF _ carrier_finite]) (auto simp: I_def)
       moreover from y have "Y \<noteq> {}" by auto
       ultimately have [simp]: "card (insert t (Y - {y})) = card Y" using \<open>t \<in> X - Y\<close> y
         by (simp add: Suc_diff_Suc card_gt_0_iff)
 
       have "\<exists>x\<in>Y - X. I (insert x X)"
       proof (rule ccontr)
         assume "\<not>?thesis"
         hence "?P X (insert t (Y - {y}))" using XY * \<open>t \<in> X - Y\<close>
           by auto
         hence "card (X \<inter> insert t (Y - {y})) \<le> n"
           unfolding n_def using finite by (intro Max_ge) auto
         also have "X \<inter> insert t (Y - {y}) = insert t ((X \<inter> Y) - {y})"
           using y \<open>t \<in> X - Y\<close> by blast
         also have "card \<dots> = Suc (card (X \<inter> Y))"
           using y \<open>t \<in> X - Y\<close> \<open>finite Y\<close> by (simp add: card.insert_remove)
         finally show False using XY by simp
       qed
       with XY show False by blast
     qed
     thus False .
   qed
   with 5 show ?case by auto
 qed (auto simp: I_def)
 
 end
 
 definition cl_in where "cl_in \<E> X = matroid.cl \<E> (indep_in \<E>) X"
 
 lemma cl_eq_cl_in:
   assumes "X \<subseteq> carrier"
   shows "cl X = cl_in carrier X"
 proof -
   interpret \<E>: matroid carrier "indep_in carrier"
     by (intro matroid_subset) auto
   have "cl X = {x \<in> carrier. rank_of (insert x X) = rank_of X}"
     unfolding cl_def by auto
   also have "\<dots> = {x \<in> carrier. \<E>.rank_of (insert x X) = \<E>.rank_of X}"
     using rank_of_sub_cong[of carrier] assms by auto
   also have "\<dots> = cl_in carrier X"
     unfolding cl_in_def \<E>.cl_def by auto
   finally show ?thesis .
 qed
 
 context
   fixes \<E>
   assumes *: "\<E> \<subseteq> carrier"
 begin
 
 interpretation \<E>: matroid \<E> "indep_in \<E>"
   using * by auto
 
 lemma cl_inI_aux: "x \<in> \<E>.cl X \<Longrightarrow> x \<in> cl_in \<E> X"
   unfolding cl_in_def by auto
 
 lemma cl_inD_aux: "x \<in> cl_in \<E> X \<Longrightarrow> x \<in> \<E>.cl X"
   unfolding cl_in_def by auto
 
 lemma cl_inI:
   assumes "X \<subseteq> \<E>"
   assumes "x \<in> \<E>"
   assumes "rank_of (insert x X) = rank_of X"
   shows "x \<in> cl_in \<E> X"
 proof -
   have "\<E>.rank_of (insert x X) = rank_of (insert x X)" "\<E>.rank_of X = rank_of X"
     using assms rank_of_sub_cong[OF *] by auto
   then show ?thesis unfolding cl_in_def using assms by (auto intro: \<E>.clI)
 qed
 
 lemma cl_in_altdef:
   assumes "X \<subseteq> \<E>"
   shows "cl_in \<E> X = \<Union>{Y \<in> Pow \<E>. X \<subseteq> Y \<and> rank_of Y = rank_of X}"
   unfolding cl_in_def
 proof (safe, goal_cases LTR RTL)
   case (LTR x)
   then have "x \<in> \<Union>{Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}"
     using \<E>.cl_altdef[OF assms] by auto
   then obtain Y where Y: "x \<in> Y" "Y \<in> Pow \<E>" "X \<subseteq> Y" "\<E>.rank_of Y = \<E>.rank_of X" by auto
   then show ?case using rank_of_sub_cong[OF *] by auto
 next
   case (RTL x Y)
   then have "x \<in> \<Union>{Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}"
      using rank_of_sub_cong[OF *, of X] rank_of_sub_cong[OF *, of Y] by auto
   then show ?case using \<E>.cl_altdef[OF assms] by auto
 qed
 
 lemma cl_in_subset_carrier: "cl_in \<E> X \<subseteq> \<E>"
   using \<E>.cl_subset_carrier unfolding cl_in_def .
 
 lemma cl_in_rank_of:
   assumes "X \<subseteq> \<E>"
   assumes "x \<in> cl_in \<E> X"
   shows "rank_of (insert x X) = rank_of X"
 proof -
   have "\<E>.rank_of (insert x X) = \<E>.rank_of X"
     using assms \<E>.cl_rank_of unfolding cl_in_def by auto
   moreover have "\<E>.rank_of (insert x X) = rank_of (insert x X)"
     using assms rank_of_sub_cong[OF *, of "insert x X"] cl_in_subset_carrier by auto
   moreover have "\<E>.rank_of X = rank_of X"
     using assms rank_of_sub_cong[OF *] by auto
   ultimately show ?thesis by auto
 qed
 
 lemmas cl_inD = cl_in_rank_of cl_in_subset_carrier
 
 lemma cl_in_subset:
   assumes "X \<subseteq> \<E>"
   shows "X \<subseteq> cl_in \<E> X"
   using \<E>.cl_subset[OF assms] unfolding cl_in_def .
 
 lemma cl_in_mono:
   assumes "X \<subseteq> Y"
   assumes "Y \<subseteq> \<E>"
   shows "cl_in \<E> X \<subseteq> cl_in \<E> Y"
   using \<E>.cl_mono[OF assms] unfolding cl_in_def .
 
 lemma cl_in_insert_absorb:
   assumes "X \<subseteq> \<E>"
   assumes "x \<in> cl_in \<E> X"
   shows "cl_in \<E> (insert x X) = cl_in \<E> X"
   using assms \<E>.cl_insert_absorb unfolding cl_in_def by auto
 
 lemma cl_in_augment:
   assumes "X \<subseteq> \<E>"
   assumes "x \<in> \<E>"
   assumes "y \<in> cl_in \<E> (insert x X) - cl_in \<E> X"
   shows "x \<in> cl_in \<E> (insert y X)"
   using assms \<E>.cl_augment unfolding cl_in_def by auto
 
 lemmas cl_inI_insert = cl_inI_aux[OF \<E>.clI_insert]
 
 end
 
 lemma cl_in_subI:
   assumes "X \<subseteq> \<E>'" "\<E>' \<subseteq> \<E>" "\<E> \<subseteq> carrier"
   shows "cl_in \<E>' X \<subseteq> cl_in \<E> X"
 proof (safe, goal_cases elem)
   case (elem x)
   then have "x \<in> \<E>'" "rank_of (insert x X) = rank_of X"
     using assms cl_inD[where \<E> = \<E>' and X = X] by auto
   then show "x \<in> cl_in \<E> X" using assms by (auto intro: cl_inI)
 qed
 
 context
   fixes \<E>
   assumes *: "\<E> \<subseteq> carrier"
 begin
 
 interpretation \<E>: matroid \<E> "indep_in \<E>"
   using * by auto
 
 lemma cl_in_sub_cong:
   assumes "X \<subseteq> \<E>'" "\<E>' \<subseteq> \<E>"
   shows "\<E>.cl_in \<E>' X = cl_in \<E>' X"
 proof (safe, goal_cases LTR RTL)
   case (LTR x)
   then have "x \<in> \<E>'" "\<E>.rank_of (insert x X) = \<E>.rank_of X"
     using assms
       \<E>.cl_in_rank_of[where \<E> = \<E>' and X = X and x = x]
       \<E>.cl_in_subset_carrier[where \<E> = \<E>']
     by auto
   moreover have "\<E>.rank_of X = rank_of X"
     using assms rank_of_sub_cong[OF *] by auto
   moreover have "\<E>.rank_of (insert x X) = rank_of (insert x X)"
     using assms rank_of_sub_cong[OF *, of "insert x X"] \<open>x \<in> \<E>'\<close> by auto
   ultimately show ?case using assms * by (auto intro: cl_inI)
 next
   case (RTL x)
   then have "x \<in> \<E>'" "rank_of (insert x X) = rank_of X"
     using * assms cl_inD[where \<E> = \<E>' and X = X] by auto
   moreover have "\<E>.rank_of X = rank_of X"
     using assms rank_of_sub_cong[OF *] by auto
   moreover have "\<E>.rank_of (insert x X) = rank_of (insert x X)"
     using assms rank_of_sub_cong[OF *, of "insert x X"] \<open>x \<in> \<E>'\<close> by auto
   ultimately show ?case using assms by (auto intro: \<E>.cl_inI)
 qed
 
 end
 end
 end
\ No newline at end of file
diff --git a/thys/Ordinal_Partitions/Library_Additions.thy b/thys/Ordinal_Partitions/Library_Additions.thy
--- a/thys/Ordinal_Partitions/Library_Additions.thy
+++ b/thys/Ordinal_Partitions/Library_Additions.thy
@@ -1,338 +1,338 @@
 section \<open>Library additions\<close>
 
 theory Library_Additions
   imports "ZFC_in_HOL.Ordinal_Exp" "HOL-Library.Ramsey" "Nash_Williams.Nash_Williams"
 
 begin
 
 lemma finite_enumerate_Diff_singleton:
   fixes S :: "'a::wellorder set"
   assumes "finite S" and i: "i < card S" "enumerate S i < x"
   shows "enumerate (S - {x}) i = enumerate S i"
   using i
 proof (induction i)
   case 0
   have "(LEAST i. i \<in> S \<and> i\<noteq>x) = (LEAST i. i \<in> S)"
   proof (rule Least_equality)
     have "\<exists>t. t \<in> S \<and> t\<noteq>x"
       using 0 \<open>finite S\<close> finite_enumerate_in_set by blast
     then show "(LEAST i. i \<in> S) \<in> S \<and> (LEAST i. i \<in> S) \<noteq> x"
       by (metis "0.prems"(2) LeastI enumerate_0 not_less_Least)
   qed (simp add: Least_le)
   then show ?case
     by (auto simp: enumerate_0)
 next
   case (Suc i)
   then have x: "enumerate S i < x"
     by (meson enumerate_step finite_enumerate_step less_trans)
   have cardSx: "Suc i < card (S - {x})" and "i < card S"
-    using Suc \<open>finite S\<close> card_Diff_singleton_if finite_enumerate_Ex by fastforce+
+    using Suc \<open>finite S\<close> card_Diff_singleton_if[of S] finite_enumerate_Ex by fastforce+
   have "(LEAST s. s \<in> S \<and> s\<noteq>x \<and> enumerate (S - {x}) i < s) = (LEAST s. s \<in> S \<and> enumerate S i < s)"
        (is "_ = ?r")
   proof (intro Least_equality conjI)
     show "?r \<in> S"
       by (metis (lifting) LeastI Suc.prems(1) assms(1) finite_enumerate_in_set finite_enumerate_step)
     show "?r \<noteq> x"
       using Suc.prems not_less_Least [of _ "\<lambda>t. t \<in> S \<and> enumerate S i < t"] 
        \<open>finite S\<close> finite_enumerate_in_set finite_enumerate_step by blast
     show "enumerate (S - {x}) i < ?r"
       by (metis (full_types) Suc.IH Suc.prems(1) \<open>i < card S\<close> enumerate_Suc'' enumerate_step finite_enumerate_Suc'' finite_enumerate_step x)
     show "\<And>y. y \<in> S \<and> y \<noteq> x \<and> enumerate (S - {x}) i < y \<Longrightarrow> ?r \<le> y"
       by (simp add: Least_le Suc.IH \<open>i < card S\<close> x)
   qed
   then show ?case
     using Suc assms by (simp add: finite_enumerate_Suc'' cardSx)
 qed
 
 lemma hd_lex: "\<lbrakk>hd ms < hd ns; length ms = length ns; ns \<noteq> []\<rbrakk> \<Longrightarrow> (ms, ns) \<in> lex less_than"
   by (metis hd_Cons_tl length_0_conv less_than_iff lexord_cons_cons lexord_lex)
 
 lemma sorted_hd_le:
   assumes "sorted xs" "x \<in> list.set xs"
   shows "hd xs \<le> x"
   using assms by (induction xs) (auto simp: less_imp_le)
 
 lemma sorted_le_last:
   assumes "sorted xs" "x \<in> list.set xs"
   shows "x \<le> last xs"
   using assms by (induction xs) (auto simp: less_imp_le)
 
 lemma hd_list_of:
   assumes "finite A" "A \<noteq> {}"
   shows "hd (sorted_list_of_set A) = Min A" 
 proof (rule antisym)
   have "Min A \<in> A"
     by (simp add: assms)
   then show "hd (sorted_list_of_set A) \<le> Min A"
     by (simp add: sorted_hd_le \<open>finite A\<close>)
 next
   show "Min A \<le> hd (sorted_list_of_set A)"
     by (metis Min_le assms hd_in_set set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff)
 qed
 
 lemma sorted_hd_le_last:
   assumes "sorted xs" "xs \<noteq> []"
   shows "hd xs \<le> last xs"
   using assms by (simp add: sorted_hd_le)
 
 lemma sorted_list_of_set_set_of [simp]: "strict_sorted l \<Longrightarrow> sorted_list_of_set (list.set l) = l"
   by (simp add: strict_sorted_equal)
 
 lemma range_strict_mono_ext:
   fixes f::"nat \<Rightarrow> 'a::linorder"
   assumes eq: "range f = range g"
       and sm: "strict_mono f" "strict_mono g"
     shows "f = g"
 proof
   fix n
   show "f n = g n"
   proof (induction n rule: less_induct)
     case (less n)
     obtain x y where xy: "f n = g y" "f x = g n"
       by (metis eq imageE rangeI)
     then have "n = y"
       by (metis (no_types) less.IH neq_iff sm strict_mono_less xy)
     then show ?case using xy by auto
   qed
 qed
 
 subsection \<open>Other material\<close>
 
 definition strict_mono_sets :: "['a::order set, 'a::order \<Rightarrow> 'b::order set] \<Rightarrow> bool" where
   "strict_mono_sets A f \<equiv> \<forall>x\<in>A. \<forall>y\<in>A. x < y \<longrightarrow> less_sets (f x) (f y)"
 
 lemma strict_mono_setsD:
   assumes "strict_mono_sets A f" "x < y" "x \<in> A" "y \<in> A"
   shows "less_sets (f x) (f y)"
   using assms by (auto simp: strict_mono_sets_def)
 
 lemma strict_mono_on_o: "\<lbrakk>strict_mono_on r A; strict_mono_on s B; s ` B \<subseteq> A\<rbrakk> \<Longrightarrow> strict_mono_on (r \<circ> s) B"
   by (auto simp: image_subset_iff strict_mono_on_def)
 
 lemma strict_mono_sets_imp_disjoint:
   fixes A :: "'a::linorder set"
   assumes "strict_mono_sets A f"
   shows "pairwise (\<lambda>x y. disjnt (f x) (f y)) A"
   using assms unfolding strict_mono_sets_def pairwise_def
   by (meson antisym_conv3 disjnt_sym less_sets_imp_disjnt)
 
 lemma strict_mono_sets_subset:
   assumes "strict_mono_sets B f" "A \<subseteq> B"
   shows "strict_mono_sets A f"
   using assms by (auto simp: strict_mono_sets_def)
 
 lemma strict_mono_less_sets_Min:
   assumes "strict_mono_sets I f" "finite I" "I \<noteq> {}"
   shows "less_sets (f (Min I)) (\<Union> (f ` (I - {Min I})))"
   using assms by (simp add: strict_mono_sets_def less_sets_UN2 dual_order.strict_iff_order)
 
 lemma pair_less_iff1 [simp]: "((x,y), (x,z)) \<in> pair_less \<longleftrightarrow> y<z"
   by (simp add: pair_less_def)
 
 lemma infinite_finite_Inter:
   assumes "finite \<A>" "\<A>\<noteq>{}" "\<And>A. A \<in> \<A> \<Longrightarrow> infinite A"
     and "\<And>A B. \<lbrakk>A \<in> \<A>; B \<in> \<A>\<rbrakk> \<Longrightarrow> A \<inter> B \<in> \<A>"
   shows "infinite (\<Inter>\<A>)"
   by (simp add: assms finite_Inf_in)
 
 lemma atLeast_less_sets: "\<lbrakk>less_sets A {x}; B \<subseteq> {x..}\<rbrakk> \<Longrightarrow> less_sets A B"
   by (force simp: less_sets_def subset_iff)
 
 
 
 subsection \<open>The list-of function\<close>
 
 lemma sorted_list_of_set_insert_remove_cons:
   assumes "finite A" "less_sets {a} A"
   shows "sorted_list_of_set (insert a A) = a # sorted_list_of_set A"
 proof -
   have "strict_sorted (a # sorted_list_of_set A)"
     using assms less_setsD by auto
   moreover have "list.set (a # sorted_list_of_set A) = insert a A"
     using assms by force
   moreover have "length (a # sorted_list_of_set A) = card (insert a A)"
     using assms card_insert_if less_setsD by fastforce
   ultimately show ?thesis
     by (metis \<open>finite A\<close> finite_insert sorted_list_of_set_unique)
 qed
 
 lemma sorted_list_of_set_Un:
   assumes AB: "less_sets A B" and fin: "finite A" "finite B"
   shows "sorted_list_of_set (A \<union> B) = sorted_list_of_set A @ sorted_list_of_set B"
 proof -
   have "strict_sorted (sorted_list_of_set A @ sorted_list_of_set B)"
     using AB unfolding less_sets_def
     by (metis fin set_sorted_list_of_set sorted_wrt_append strict_sorted_list_of_set)
   moreover have "card A + card B = card (A \<union> B)"
     using less_sets_imp_disjnt [OF AB]
     by (simp add: assms card_Un_disjoint disjnt_def)
   ultimately show ?thesis
     by (simp add: assms strict_sorted_equal)
 qed
 
 lemma sorted_list_of_set_UN_lessThan:
   fixes k::nat
   assumes sm: "strict_mono_sets {..<k} A" and "\<And>i. i < k \<Longrightarrow> finite (A i)"
   shows "sorted_list_of_set (\<Union>i<k. A i) = concat (map (sorted_list_of_set \<circ> A) (sorted_list_of_set {..<k}))"
   using assms
 proof (induction k)
   case 0
   then show ?case
     by auto
 next
   case (Suc k)
   have ls: "less_sets (\<Union> (A ` {..<k})) (A k)"
     using sm Suc.prems(1) strict_mono_setsD by (force simp: less_sets_UN1)
   have "sorted_list_of_set (\<Union> (A ` {..<Suc k})) = sorted_list_of_set (\<Union> (A ` {..<k}) \<union> A k)"
     by (simp add: Un_commute lessThan_Suc)
   also have "\<dots> = sorted_list_of_set (\<Union> (A ` {..<k})) @ sorted_list_of_set (A k)"
     by (rule sorted_list_of_set_Un) (auto simp: Suc.prems ls)
   also have "\<dots> = concat (map (sorted_list_of_set \<circ> A) (sorted_list_of_set {..<k})) @ sorted_list_of_set (A k)"
     using Suc strict_mono_sets_def by fastforce
   also have "\<dots> = concat (map (sorted_list_of_set \<circ> A) (sorted_list_of_set {..<Suc k}))"
     using strict_mono_sets_def by fastforce
   finally show ?case .
 qed
 
 lemma sorted_list_of_set_UN_atMost:
   fixes k::nat
   assumes "strict_mono_sets {..k} A" and "\<And>i. i \<le> k \<Longrightarrow> finite (A i)"
   shows "sorted_list_of_set (\<Union>i\<le>k. A i) = concat (map (sorted_list_of_set \<circ> A) (sorted_list_of_set {..k}))"
   by (metis assms lessThan_Suc_atMost less_Suc_eq_le sorted_list_of_set_UN_lessThan)
 
 subsection \<open>Monotonic enumeration of a countably infinite set\<close>
 
 abbreviation "enum \<equiv> enumerate"
 
 text \<open>Could be generalised to infinite countable sets of any type\<close>
 lemma nat_infinite_iff:
   fixes N :: "nat set"
   shows "infinite N \<longleftrightarrow> (\<exists>f::nat\<Rightarrow>nat. N = range f \<and> strict_mono f)"
 proof safe
   assume "infinite N"
   then show "\<exists>f. N = range (f::nat \<Rightarrow> nat) \<and> strict_mono f"
     by (metis bij_betw_imp_surj_on bij_enumerate enumerate_mono strict_mono_def)
 next
   fix f :: "nat \<Rightarrow> nat"
   assume "strict_mono f" and "N = range f" and "finite (range f)"
   then show False
     using range_inj_infinite strict_mono_imp_inj_on by blast
 qed
 
 lemma enum_works:
   fixes N :: "nat set"
   assumes "infinite N"
   shows "N = range (enum N) \<and> strict_mono (enum N)"
   by (metis assms bij_betw_imp_surj_on bij_enumerate enumerate_mono strict_monoI)
 
 lemma range_enum: "range (enum N) = N" and strict_mono_enum: "strict_mono (enum N)"
   if "infinite N" for N :: "nat set"
   using enum_works [OF that] by auto
 
 lemma enum_0_eq_Inf:
   fixes N :: "nat set"
   assumes "infinite N"
   shows "enum N 0 = Inf N"
 proof -
   have "enum N 0 \<in> N"
     using assms range_enum by auto
   moreover have "\<And>x. x \<in> N \<Longrightarrow> enum N 0 \<le> x"
     by (metis (mono_tags, opaque_lifting) assms imageE le0 less_mono_imp_le_mono range_enum strict_monoD strict_mono_enum)
   ultimately show ?thesis
     by (metis cInf_eq_minimum)
 qed
 
 lemma enum_works_finite:
   fixes N :: "nat set"
   assumes "finite N"
   shows "N = enum N ` {..<card N} \<and> strict_mono_on (enum N) {..<card N}"
   using assms
   by (metis bij_betw_imp_surj_on finite_bij_enumerate finite_enumerate_mono lessThan_iff strict_mono_onI)
 
 lemma enum_obtain_index_finite:
   fixes N :: "nat set"
   assumes "x \<in> N" "finite N" 
   obtains i where "i < card N" "x = enum N i"
   by (metis \<open>x \<in> N\<close> \<open>finite N\<close> enum_works_finite imageE lessThan_iff)
 
 lemma enum_0_eq_Inf_finite:
   fixes N :: "nat set"
   assumes "finite N" "N \<noteq> {}"
   shows "enum N 0 = Inf N"
 proof -
   have "enum N 0 \<in> N"
     by (metis Nat.neq0_conv assms empty_is_image enum_works_finite image_eqI lessThan_empty_iff lessThan_iff)
   moreover have "enum N 0 \<le> x" if "x \<in> N" for x
   proof -
     obtain i where "i < card N" "x = enum N i"
       by (metis \<open>x \<in> N\<close> \<open>finite N\<close> enum_obtain_index_finite)
     with assms show ?thesis
       by (metis Nat.neq0_conv finite_enumerate_mono less_or_eq_imp_le)
   qed
   ultimately show ?thesis
     by (metis cInf_eq_minimum)
 qed
 
 lemma greaterThan_less_enum:
   fixes N :: "nat set"
   assumes "N \<subseteq> {x<..}" "infinite N"
   shows "x < enum N i"
   using assms range_enum by fastforce
 
 lemma atLeast_le_enum:
   fixes N :: "nat set"
   assumes "N \<subseteq> {x..}" "infinite N"
   shows "x \<le> enum N i"
   using assms range_enum by fastforce
 
 lemma less_sets_empty1 [simp]: "less_sets {} A" and less_sets_empty2 [simp]: "less_sets A {}"
   by (simp_all add: less_sets_def)
 
 lemma less_sets_singleton1 [simp]: "less_sets {a} A \<longleftrightarrow> (\<forall>x\<in>A. a < x)" 
   and less_sets_singleton2 [simp]: "less_sets A {a} \<longleftrightarrow> (\<forall>x\<in>A. x < a)"
   by (simp_all add: less_sets_def)
 
 lemma less_sets_atMost [simp]: "less_sets {..a} A \<longleftrightarrow> (\<forall>x\<in>A. a < x)" 
   and less_sets_alLeast [simp]: "less_sets A {a..} \<longleftrightarrow> (\<forall>x\<in>A. x < a)"
   by (auto simp: less_sets_def)
 
 lemma less_sets_imp_strict_mono_sets:
   assumes "\<And>i. less_sets (A i) (A (Suc i))" "\<And>i. i>0 \<Longrightarrow> A i \<noteq> {}"
   shows "strict_mono_sets UNIV A"
 proof (clarsimp simp: strict_mono_sets_def)
   fix i j::nat
   assume "i < j"
   then show "less_sets (A i) (A j)"
   proof (induction "j-i" arbitrary: i j)
     case (Suc x)
     then show ?case
       by (metis Suc_diff_Suc Suc_inject Suc_mono assms less_Suc_eq less_sets_trans zero_less_Suc)
   qed auto
 qed
 
 lemma less_sets_Suc_Max:  
   assumes "finite A"
   shows "less_sets A {Suc (Max A)..}"
 proof (cases "A = {}")
   case False
   then show ?thesis
     by (simp add: assms less_Suc_eq_le)
 qed auto
 
 lemma infinite_nat_greaterThan:
   fixes m::nat
   assumes "infinite N"
   shows "infinite (N \<inter> {m<..})"
 proof -
   have "N \<subseteq> -{m<..} \<union> (N \<inter> {m<..})"
     by blast
   moreover have "finite (-{m<..})"
     by simp
   ultimately show ?thesis
     using assms finite_subset by blast
 qed
 
 end
 
     
 
diff --git a/thys/Regular-Sets/pEquivalence_Checking.thy b/thys/Regular-Sets/pEquivalence_Checking.thy
--- a/thys/Regular-Sets/pEquivalence_Checking.thy
+++ b/thys/Regular-Sets/pEquivalence_Checking.thy
@@ -1,306 +1,307 @@
 section \<open>Deciding Regular Expression Equivalence (2)\<close>
 
 theory pEquivalence_Checking
 imports Equivalence_Checking Derivatives
 begin
 
 text\<open>\noindent Similar to theory @{theory "Regular-Sets.Equivalence_Checking"}, but
 with partial derivatives instead of derivatives.\<close>
 
 text\<open>Lifting many notions to sets:\<close>
 
 definition "Lang R == UN r:R. lang r"
 definition "Nullable R == EX r:R. nullable r"
 definition "Pderiv a R == UN r:R. pderiv a r"
 definition "Atoms R == UN r:R. atoms r"
 
 (* FIXME: rename pderiv_set in Derivatives to Pderiv and drop the one above *)
 
 lemma Atoms_pderiv: "Atoms(pderiv a r) \<subseteq> atoms r"
 apply (induct r)
 apply (auto simp: Atoms_def UN_subset_iff)
 apply (fastforce)+
 done
 
 lemma Atoms_Pderiv: "Atoms(Pderiv a R) \<subseteq> Atoms R"
 using Atoms_pderiv by (fastforce simp: Atoms_def Pderiv_def)
 
 lemma pderiv_no_occurrence: 
   "x \<notin> atoms r \<Longrightarrow> pderiv x r = {}"
 by (induct r) auto
 
 lemma Pderiv_no_occurrence: 
   "x \<notin> Atoms R \<Longrightarrow> Pderiv x R = {}"
 by(auto simp:pderiv_no_occurrence Atoms_def Pderiv_def)
 
 lemma Deriv_Lang: "Deriv c (Lang R) = Lang (Pderiv c R)"
 by(auto simp: Deriv_pderiv Pderiv_def Lang_def)
 
 lemma Nullable_pderiv[simp]: "Nullable(pderivs w r) = (w : lang r)"
 apply(induction w arbitrary: r)
 apply (simp add: Nullable_def nullable_iff singleton_iff)
 using eqset_imp_iff[OF Deriv_pderiv[where 'a = 'a]]
 apply (simp add: Nullable_def Deriv_def)
 done
 
 
 type_synonym 'a Rexp_pair = "'a rexp set * 'a rexp set"
 type_synonym 'a Rexp_pairs = "'a Rexp_pair list"
 
 definition is_Bisimulation :: "'a list \<Rightarrow> 'a Rexp_pairs \<Rightarrow> bool"
 where
 "is_Bisimulation as ps =
   (\<forall>(R,S)\<in> set ps. Atoms R \<union> Atoms S \<subseteq> set as \<and>
     (Nullable R \<longleftrightarrow> Nullable S) \<and>
     (\<forall>a\<in>set as. (Pderiv a R, Pderiv a S) \<in> set ps))"
 
 lemma Bisim_Lang_eq:
 assumes Bisim: "is_Bisimulation as ps"
 assumes "(R, S) \<in> set ps"
 shows "Lang R = Lang S"
 proof -
   define ps' where "ps' = ({}, {}) # ps"
   from Bisim have Bisim': "is_Bisimulation as ps'"
     by (fastforce simp: ps'_def is_Bisimulation_def UN_subset_iff Pderiv_def Atoms_def)
   let ?R = "\<lambda>K L. (\<exists>(R,S)\<in>set ps'. K = Lang R \<and> L = Lang S)"
   show ?thesis
   proof (rule language_coinduct[where R="?R"])
     from \<open>(R,S) \<in> set ps\<close>
     have "(R,S) \<in> set ps'" by (auto simp: ps'_def)
     thus "?R (Lang R) (Lang S)" by auto
   next
     fix K L assume "?R K L"
     then obtain R S where rs: "(R, S) \<in> set ps'"
       and KL: "K = Lang R" "L = Lang S" by auto
     with Bisim' have "Nullable R \<longleftrightarrow> Nullable S"
       by (auto simp: is_Bisimulation_def)
     thus "[] \<in> K \<longleftrightarrow> [] \<in> L"
       by (auto simp: nullable_iff KL Nullable_def Lang_def)
     fix a
     show "?R (Deriv a K) (Deriv a L)"
     proof cases
       assume "a \<in> set as"
       with rs Bisim'
       have "(Pderiv a R, Pderiv a S) \<in> set ps'"
         by (auto simp: is_Bisimulation_def)
       thus ?thesis by (fastforce simp: KL Deriv_Lang)
     next
       assume "a \<notin> set as"
       with Bisim' rs
       have "a \<notin> Atoms R \<union> Atoms S"
         by (fastforce simp: is_Bisimulation_def UN_subset_iff)
       then have "Pderiv a R = {}" "Pderiv a S = {}"
         by (metis Pderiv_no_occurrence Un_iff)+
       then have "Deriv a K = Lang {}" "Deriv a L = Lang {}" 
         unfolding KL Deriv_Lang by auto
       thus ?thesis by (auto simp: ps'_def)
     qed
   qed
 qed
 
 
 subsection \<open>Closure computation\<close>
 
 fun test :: "'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> bool" where
 "test (ws, ps) = (case ws of [] \<Rightarrow>  False | (R,S)#_ \<Rightarrow> Nullable R = Nullable S)"
 
 fun step :: "'a list \<Rightarrow>
   'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> 'a Rexp_pairs * 'a Rexp_pairs"
 where "step as (ws,ps) =
     (let
       (R,S) = hd ws;
       ps' = (R,S) # ps;
       succs = map (\<lambda>a. (Pderiv a R, Pderiv a S)) as;
       new = filter (\<lambda>p. p \<notin> set ps \<union> set ws) succs
     in (remdups new @ tl ws, ps'))"
 
 definition closure ::
   "'a list \<Rightarrow> 'a Rexp_pairs * 'a Rexp_pairs
    \<Rightarrow> ('a Rexp_pairs * 'a Rexp_pairs) option" where
 "closure as = while_option test (step as)"
 
 definition pre_Bisim :: "'a list \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set \<Rightarrow>
  'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> bool"
 where
 "pre_Bisim as R S = (\<lambda>(ws,ps).
  ((R,S) \<in> set ws \<union> set ps) \<and>
  (\<forall>(R,S)\<in> set ws \<union> set ps. Atoms R \<union> Atoms S \<subseteq> set as) \<and>
  (\<forall>(R,S)\<in> set ps. (Nullable R \<longleftrightarrow> Nullable S) \<and>
    (\<forall>a\<in>set as. (Pderiv a R, Pderiv a S) \<in> set ps \<union> set ws)))"
 
 lemma step_set_eq: "\<lbrakk> test (ws,ps); step as (ws,ps) = (ws',ps') \<rbrakk>
   \<Longrightarrow> set ws' \<union> set ps' =
      set ws \<union> set ps
      \<union> (\<Union>a\<in>set as. {(Pderiv a (fst(hd ws)), Pderiv a (snd(hd ws)))})"
 by(auto split: list.splits)
 
 theorem closure_sound:
 assumes result: "closure as ([(R,S)],[]) = Some([],ps)"
 and atoms: "Atoms R \<union> Atoms S \<subseteq> set as"
 shows "Lang R = Lang S"
 proof-
   { fix st
     have "pre_Bisim as R S st \<Longrightarrow> test st \<Longrightarrow> pre_Bisim as R S (step as st)"
     unfolding pre_Bisim_def
     proof(split prod.splits, elim case_prodE conjE, intro allI impI conjI, goal_cases)
       case 1 thus ?case by(auto split: list.splits)
     next
       case prems: (2 ws ps ws' ps')
       note prems(2)[simp]
       from \<open>test st\<close> obtain wstl R S where [simp]: "ws = (R,S)#wstl"
         by (auto split: list.splits)
       from \<open>step as st = (ws',ps')\<close> obtain P where [simp]: "ps' = (R,S) # ps"
         and [simp]: "ws' = remdups(filter P (map (\<lambda>a. (Pderiv a R, Pderiv a S)) as)) @ wstl"
         by auto
       have "\<forall>(R',S')\<in>set wstl \<union> set ps'. Atoms R' \<union> Atoms S' \<subseteq> set as"
         using prems(4) by auto
       moreover
       have "\<forall>a\<in>set as. Atoms(Pderiv a R) \<union> Atoms(Pderiv a S) \<subseteq> set as"
         using prems(4) by simp (metis (lifting) Atoms_Pderiv order_trans)
       ultimately show ?case by simp blast
     next
       case 3 thus ?case
         apply (clarsimp simp: image_iff split: prod.splits list.splits)
         by hypsubst_thin metis
     qed
   }
   moreover
   from atoms
   have "pre_Bisim as R S ([(R,S)],[])" by (simp add: pre_Bisim_def)
   ultimately have pre_Bisim_ps: "pre_Bisim as R S ([],ps)"
     by (rule while_option_rule[OF _ result[unfolded closure_def]])
   then have "is_Bisimulation as ps" "(R,S) \<in> set ps"
     by (auto simp: pre_Bisim_def is_Bisimulation_def)
   thus "Lang R = Lang S" by (rule Bisim_Lang_eq)
 qed
 
 
 subsection \<open>The overall procedure\<close>
 
 definition check_eqv :: "'a rexp \<Rightarrow> 'a rexp \<Rightarrow> bool"
 where
 "check_eqv r s =
   (case closure (add_atoms r (add_atoms s [])) ([({r}, {s})], []) of
      Some([],_) \<Rightarrow> True | _ \<Rightarrow> False)"
 
 lemma soundness: assumes "check_eqv r s" shows "lang r = lang s"
 proof -
   let ?as = "add_atoms r (add_atoms s [])"
   obtain ps where 1: "closure ?as ([({r},{s})],[]) = Some([],ps)"
     using assms by (auto simp: check_eqv_def split:option.splits list.splits)
   then have "lang r = lang s"
     by(rule closure_sound[of _ "{r}" "{s}", simplified Lang_def, simplified])
       (auto simp: set_add_atoms Atoms_def)
   thus "lang r = lang s" by simp
 qed
 
 text\<open>Test:\<close>
 lemma "check_eqv
   (Plus One (Times (Atom 0) (Star(Atom 0))))
   (Star(Atom(0::nat)))"
 by eval
 
 
 subsection "Termination and Completeness"
 
 definition PDERIVS :: "'a rexp set => 'a rexp set" where
 "PDERIVS R = (UN r:R. pderivs_lang UNIV r)"
 
 lemma PDERIVS_incr[simp]: "R \<subseteq> PDERIVS R"
 apply(auto simp add: PDERIVS_def pderivs_lang_def)
 by (metis pderivs.simps(1) insertI1)
 
 lemma Pderiv_PDERIVS: assumes "R' \<subseteq> PDERIVS R" shows "Pderiv a R' \<subseteq> PDERIVS R"
 proof
   fix r assume "r : Pderiv a R'"
   then obtain r' where "r' : R'" "r : pderiv a r'" by(auto simp: Pderiv_def)
   from \<open>r' : R'\<close> \<open>R' \<subseteq> PDERIVS R\<close> obtain s w where "s : R" "r' : pderivs w s"
     by(auto simp: PDERIVS_def pderivs_lang_def)
   hence "r \<in> pderivs (w @ [a]) s" using \<open>r : pderiv a r'\<close> by(auto simp add:pderivs_snoc)
   thus "r : PDERIVS R" using \<open>s : R\<close> by(auto simp: PDERIVS_def pderivs_lang_def)
 qed
 
 lemma finite_PDERIVS: "finite R \<Longrightarrow> finite(PDERIVS R)"
 by(simp add: PDERIVS_def finite_pderivs_lang_UNIV)
 
 lemma closure_Some: assumes "finite R0" "finite S0" shows "\<exists>p. closure as ([(R0,S0)],[]) = Some p"
 proof(unfold closure_def)
   let ?Inv = "%(ws,bs).  distinct ws \<and> (ALL (R,S) : set ws. R \<subseteq> PDERIVS R0 \<and> S \<subseteq> PDERIVS S0 \<and> (R,S) \<notin> set bs)"
   let ?m1 = "%bs. Pow(PDERIVS R0) \<times> Pow(PDERIVS S0) - set bs"
   let ?m2 = "%(ws,bs). card(?m1 bs)"
   have Inv0: "?Inv ([(R0, S0)], [])" by simp
   { fix s assume "test s" "?Inv s"
     obtain ws bs where [simp]: "s = (ws,bs)" by fastforce
     from \<open>test s\<close> obtain R S ws' where [simp]: "ws = (R,S)#ws'"
       by(auto split: prod.splits list.splits)
     let ?bs' = "(R,S) # bs"
     let ?succs = "map (\<lambda>a. (Pderiv a R, Pderiv a S)) as"
     let ?new = "filter (\<lambda>p. p \<notin> set bs \<union> set ws) ?succs"
     let ?ws' = "remdups ?new @ ws'"
     have *: "?Inv (step as s)"
     proof -
       from \<open>?Inv s\<close> have "distinct ?ws'" by auto
       have "ALL (R,S) : set ?ws'. R \<subseteq> PDERIVS R0 \<and> S \<subseteq> PDERIVS S0 \<and> (R,S) \<notin> set ?bs'" using \<open>?Inv s\<close>
         by(simp add: Ball_def image_iff) (metis Pderiv_PDERIVS)
       with \<open>distinct ?ws'\<close> show ?thesis by(simp)
     qed
     have "?m2(step as s) < ?m2 s"
     proof -
-      have "finite(?m1 bs)"
+      have fin: "finite(?m1 bs)"
         by(metis assms finite_Diff finite_PDERIVS finite_cartesian_product finite_Pow_iff)
-      moreover have "?m2(step as s) < ?m2 s" using \<open>?Inv s\<close>
-        by(auto intro: psubset_card_mono[OF \<open>finite(?m1 bs)\<close>])
+      have "?m2(step as s) < ?m2 s" using \<open>?Inv s\<close> psubset_card_mono[OF \<open>finite(?m1 bs)\<close>]
+        apply (simp split: prod.split_asm)
+        by (metis Diff_iff Pow_iff SigmaI fin card_gt_0_iff diff_Suc_less emptyE)
       then show ?thesis using \<open>?Inv s\<close> by simp
     qed
     note * and this
   } note step = this
   show "\<exists>p. while_option test (step as) ([(R0, S0)], []) = Some p" 
     by(rule measure_while_option_Some [where P = ?Inv and f = ?m2, OF _ Inv0])(simp add: step)
 qed
 
 theorem closure_Some_Inv: assumes "closure as ([({r},{s})],[]) = Some p"
 shows "\<forall>(R,S)\<in>set(fst p). \<exists>w. R = pderivs w r \<and> S = pderivs w s" (is "?Inv p")
 proof-
   from assms have 1: "while_option test (step as) ([({r},{s})],[]) = Some p"
     by(simp add: closure_def)
   have Inv0: "?Inv ([({r},{s})],[])" by simp (metis pderivs.simps(1))
   { fix p assume "?Inv p" "test p"
     obtain ws bs where [simp]: "p = (ws,bs)" by fastforce
     from \<open>test p\<close> obtain R S ws' where [simp]: "ws = (R,S)#ws'"
       by(auto split: prod.splits list.splits)
     let ?succs = "map (\<lambda>a. (Pderiv a R, Pderiv a S)) as"
     let ?new = "filter (\<lambda>p. p \<notin> set bs \<union> set ws) ?succs"
     let ?ws' = "remdups ?new @ ws'"
     from \<open>?Inv p\<close> obtain w where [simp]: "R = pderivs w r" "S = pderivs w s"
       by auto
     { fix x assume "x : set as"
       have "EX w. Pderiv x R = pderivs w r \<and> Pderiv x S = pderivs w s"
         by(rule_tac x="w@[x]" in exI)(simp add: pderivs_append Pderiv_def)
     }
     with \<open>?Inv p\<close> have "?Inv (step as p)" by auto
   } note Inv_step = this
   show ?thesis
     apply(rule while_option_rule[OF _ 1])
     apply(erule (1) Inv_step)
     apply(rule Inv0)
     done
 qed
 
 lemma closure_complete: assumes "lang r = lang s"
  shows "EX bs. closure as ([({r},{s})],[]) = Some([],bs)" (is ?C)
 proof(rule ccontr)
   assume "\<not> ?C"
   then obtain R S ws bs
     where cl: "closure as ([({r},{s})],[]) = Some((R,S)#ws,bs)"
     using closure_Some[of "{r}" "{s}", simplified]
     by (metis (opaque_lifting, no_types) list.exhaust prod.exhaust)
   from assms closure_Some_Inv[OF this]
     while_option_stop[OF cl[unfolded closure_def]]
   show "False" by auto
 qed
 
 corollary completeness: "lang r = lang s \<Longrightarrow> check_eqv r s"
 by(auto simp add: check_eqv_def dest!: closure_complete
       split: option.split list.split)
 
 end
diff --git a/thys/SenSocialChoice/Arrow.thy b/thys/SenSocialChoice/Arrow.thy
--- a/thys/SenSocialChoice/Arrow.thy
+++ b/thys/SenSocialChoice/Arrow.thy
@@ -1,637 +1,637 @@
 (*
  * Arrow's General Possibility Theorem, following Sen.
  * (C)opyright Peter Gammie, peteg42 at gmail.com, commenced July 2006.
  * License: BSD
  *)
 
 (*<*)
 theory Arrow
 
 imports SCFs
 
 begin
 (*>*)
 
 section\<open>Arrow's General Possibility Theorem\<close>
 
 text\<open>
 
 The proof falls into two parts: showing that a semi-decisive individual is
 in fact a dictator, and that a semi-decisive individual exists. I take them
 in that order.
 
 It might be good to do some of this in a locale. The complication is
 untangling where various witnesses need to be quantified over.
 
 \<close>
 
 (* **************************************** *)
 
 subsection\<open>Semi-decisiveness Implies Decisiveness\<close>
 
 text\<open>
 
 I follow \cite[Chapter~3*]{Sen:70a} quite closely here. Formalising his
 appeal to the @{term "iia"} assumption is the main complication here.
 
 \<close>
 
 text\<open>The witness for the first lemma: in the profile $P'$, special agent
 $j$ strictly prefers $x$ to $y$ to $z$, and doesn't care about the other
 alternatives. Everyone else strictly prefers $y$ to each of $x$ to $z$, and
 inherits the relative preferences between $x$ and $z$ from profile $P$.
 
 The model has to be specific about ordering all the other alternatives, but
 these are immaterial in the proof that uses this witness. Note also that the
 following lemma is used with different instantiations of $x$, $y$ and $z$,
 so we need to quantify over them here. This happens implicitly, but in a
 locale we would have to be more explicit.
 
 This is just tedious.\<close>
 
 lemma decisive1_witness:
   assumes has3A: "hasw [x,y,z] A"
       and profileP: "profile A Is P"
       and jIs: "j \<in> Is"
   obtains P'
   where "profile A Is P'"
     and "x \<^bsub>(P' j)\<^esub>\<prec> y \<and> y \<^bsub>(P' j)\<^esub>\<prec> z"
     and "\<And>i. i \<noteq> j \<Longrightarrow> y \<^bsub>(P' i)\<^esub>\<prec> x \<and> y \<^bsub>(P' i)\<^esub>\<prec> z \<and> ((x \<^bsub>(P' i)\<^esub>\<preceq> z) = (x \<^bsub>(P i)\<^esub>\<preceq> z)) \<and> ((z \<^bsub>(P' i)\<^esub>\<preceq> x) = (z \<^bsub>(P i)\<^esub>\<preceq> x))"
 proof
   let ?P' = "\<lambda>i. (if i = j then ({ (x, u) | u. u \<in> A }
                                \<union> { (y, u) | u. u \<in> A - {x} }
                                \<union> { (z, u) | u. u \<in> A - {x,y} })
                            else ({ (y, u) | u. u \<in> A }
                                \<union> { (x, u) | u. u \<in> A - {y,z} }
                                \<union> { (z, u) | u. u \<in> A - {x,y} }
                                \<union> (if x \<^bsub>(P i)\<^esub>\<preceq> z then {(x,z)} else {})
                                \<union> (if z \<^bsub>(P i)\<^esub>\<preceq> x then {(z,x)} else {})))
                       \<union> (A - {x,y,z}) \<times> (A - {x,y,z})"
   show "profile A Is ?P'"
   proof
     fix i assume iIs: "i \<in> Is"
     show "rpr A (?P' i)"
     proof(cases "i = j")
       case True with has3A show ?thesis
         by - (rule rprI, simp_all add: trans_def, blast+)
     next
       case False hence ij: "i \<noteq> j" .
       show ?thesis
       proof
         from iIs profileP have "complete A (P i)" by (blast dest: rpr_complete)
         with ij show "complete A (?P' i)" by (simp add: complete_def, blast)
         from iIs profileP have "refl_on A (P i)" by (auto simp add: rpr_def)
         with has3A ij show "refl_on A (?P' i)" by (simp, blast)
         from ij has3A show "trans (?P' i)" by (clarsimp simp add: trans_def)
       qed
     qed
   next
     from profileP show "Is \<noteq> {}" by (rule profile_non_empty)
   qed
   from has3A
   show "x \<^bsub>(?P' j)\<^esub>\<prec> y \<and> y \<^bsub>(?P' j)\<^esub>\<prec> z"
    and "\<And>i. i \<noteq> j \<Longrightarrow> y \<^bsub>(?P' i)\<^esub>\<prec> x \<and> y \<^bsub>(?P' i)\<^esub>\<prec> z \<and> ((x \<^bsub>(?P' i)\<^esub>\<preceq> z) = (x \<^bsub>(P i)\<^esub>\<preceq> z)) \<and> ((z \<^bsub>(?P' i)\<^esub>\<preceq> x) = (z \<^bsub>(P i)\<^esub>\<preceq> x))"
     unfolding strict_pref_def by auto
 qed
 
 text \<open>The key lemma: in the presence of Arrow's assumptions, an individual
 who is semi-decisive for $x$ and $y$ is actually decisive for $x$ over any
 other alternative $z$. (This is where the quantification becomes important.) 
 \<close>
 
 lemma decisive1:
   assumes has3A: "hasw [x,y,z] A"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
       and sd: "semidecisive swf A Is {j} x y"
   shows "decisive swf A Is {j} x z"
 proof
   from sd show jIs: "{j} \<subseteq> Is" by blast
   fix P
   assume profileP: "profile A Is P"
      and jxzP: "\<And>i. i \<in> {j} \<Longrightarrow> x \<^bsub>(P i)\<^esub>\<prec> z"
   from has3A profileP jIs
   obtain P'
     where profileP': "profile A Is P'"
       and jxyzP': "x \<^bsub>(P' j)\<^esub>\<prec> y" "y \<^bsub>(P' j)\<^esub>\<prec> z"
       and ixyzP': "\<And>i. i \<noteq> j \<longrightarrow> y \<^bsub>(P' i)\<^esub>\<prec> x \<and> y \<^bsub>(P' i)\<^esub>\<prec> z \<and> ((x \<^bsub>(P' i)\<^esub>\<preceq> z) = (x \<^bsub>(P i)\<^esub>\<preceq> z)) \<and> ((z \<^bsub>(P' i)\<^esub>\<preceq> x) = (z \<^bsub>(P i)\<^esub>\<preceq> x))"
     by - (rule decisive1_witness, blast+)
   from iia have "\<And>a b. \<lbrakk> a \<in> {x, z}; b \<in> {x, z} \<rbrakk> \<Longrightarrow> (a \<^bsub>(swf P)\<^esub>\<preceq> b) = (a \<^bsub>(swf P')\<^esub>\<preceq> b)"
   proof(rule iiaE)
     from has3A show "{x,z} \<subseteq> A" by simp
   next
     fix i assume iIs: "i \<in> Is"
     fix a b assume ab: "a \<in> {x, z}" "b \<in> {x, z}"
     show "(a \<^bsub>(P' i)\<^esub>\<preceq> b) = (a \<^bsub>(P i)\<^esub>\<preceq> b)"
     proof(cases "i = j")
       case False
       with ab iIs ixyzP' profileP profileP' has3A
       show ?thesis unfolding profile_def by auto
     next
       case True
       from profileP' jIs jxyzP' have "x \<^bsub>(P' j)\<^esub>\<prec> z"
         by (auto dest: rpr_less_trans)
       with True ab iIs jxzP profileP profileP' has3A
       show ?thesis unfolding profile_def strict_pref_def by auto
     qed
   qed (simp_all add: profileP profileP')
   moreover have "x \<^bsub>(swf P')\<^esub>\<prec> z"
   proof -
     from profileP' sd jxyzP' ixyzP' have "x \<^bsub>(swf P')\<^esub>\<prec> y" by (simp add: semidecisive_def)
     moreover
     from jxyzP' ixyzP' have "\<And>i. i \<in> Is \<Longrightarrow> y \<^bsub>(P' i)\<^esub>\<prec> z" by (case_tac "i=j", auto)
     with wp profileP' has3A have "y \<^bsub>(swf P')\<^esub>\<prec> z" by (auto dest: weak_paretoD)
     moreover note SWF_rpr[OF swf] profileP'
     ultimately show "x \<^bsub>(swf P')\<^esub>\<prec> z"
       unfolding universal_domain_def by (blast dest: rpr_less_trans)
   qed
   ultimately show "x \<^bsub>(swf P)\<^esub>\<prec> z" unfolding strict_pref_def by blast
 qed
 
 text\<open>The witness for the second lemma: special agent $j$ strictly prefers
 $z$ to $x$ to $y$, and everyone else strictly prefers $z$ to $x$ and $y$ to
 $x$. (In some sense the last part is upside-down with respect to the first
 witness.)\<close>
 
 lemma decisive2_witness:
   assumes has3A: "hasw [x,y,z] A"
       and profileP: "profile A Is P"
       and jIs: "j \<in> Is"
   obtains P'
     where "profile A Is P'"
       and "z \<^bsub>(P' j)\<^esub>\<prec> x \<and> x \<^bsub>(P' j)\<^esub>\<prec> y"
       and "\<And>i. i \<noteq> j \<Longrightarrow> z \<^bsub>(P' i)\<^esub>\<prec> x \<and> y \<^bsub>(P' i)\<^esub>\<prec> x \<and> ((y \<^bsub>(P' i)\<^esub>\<preceq> z) = (y \<^bsub>(P i)\<^esub>\<preceq> z)) \<and> ((z \<^bsub>(P' i)\<^esub>\<preceq> y) = (z \<^bsub>(P i)\<^esub>\<preceq> y))"
 proof
   let ?P' = "\<lambda>i. (if i = j then ({ (z, u) | u. u \<in> A }
                                \<union> { (x, u) | u. u \<in> A - {z} }
                                \<union> { (y, u) | u. u \<in> A - {x,z} })
                            else ({ (z, u) | u. u \<in> A - {y} }
                                \<union> { (y, u) | u. u \<in> A - {z} }
                                \<union> { (x, u) | u. u \<in> A - {y,z} }
                                \<union> (if y \<^bsub>(P i)\<^esub>\<preceq> z then {(y,z)} else {})
                                \<union> (if z \<^bsub>(P i)\<^esub>\<preceq> y then {(z,y)} else {})))
                       \<union> (A - {x,y,z}) \<times> (A - {x,y,z})"
   show "profile A Is ?P'"
   proof
     fix i assume iIs: "i \<in> Is"
     show "rpr A (?P' i)"
     proof(cases "i = j")
       case True with has3A show ?thesis
         by - (rule rprI, simp_all add: trans_def, blast+)
     next
       case False hence ij: "i \<noteq> j" .
       show ?thesis
       proof
         from iIs profileP have "complete A (P i)" by (auto simp add: rpr_def)
         with ij show "complete A (?P' i)" by (simp add: complete_def, blast)
         from iIs profileP have "refl_on A (P i)" by (auto simp add: rpr_def)
         with has3A ij show "refl_on A (?P' i)" by (simp, blast)
         from ij has3A show "trans (?P' i)" by (clarsimp simp add: trans_def)
       qed
     qed
   next
     show "Is \<noteq> {}" by (rule profile_non_empty[OF profileP])
   qed
   from has3A
   show "z \<^bsub>(?P' j)\<^esub>\<prec> x \<and> x \<^bsub>(?P' j)\<^esub>\<prec> y"
    and "\<And>i. i \<noteq> j \<Longrightarrow> z \<^bsub>(?P' i)\<^esub>\<prec> x \<and> y \<^bsub>(?P' i)\<^esub>\<prec> x \<and> ((y \<^bsub>(?P' i)\<^esub>\<preceq> z) = (y \<^bsub>(P i)\<^esub>\<preceq> z)) \<and> ((z \<^bsub>(?P' i)\<^esub>\<preceq> y) = (z \<^bsub>(P i)\<^esub>\<preceq> y))"
     unfolding strict_pref_def by auto
 qed
 
 lemma decisive2:
   assumes has3A: "hasw [x,y,z] A"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
       and sd: "semidecisive swf A Is {j} x y"
   shows "decisive swf A Is {j} z y"
 proof
   from sd show jIs: "{j} \<subseteq> Is" by blast
   fix P
   assume profileP: "profile A Is P"
      and jyzP: "\<And>i. i \<in> {j} \<Longrightarrow> z \<^bsub>(P i)\<^esub>\<prec> y"
   from has3A profileP jIs
   obtain P'
     where profileP': "profile A Is P'"
       and jxyzP': "z \<^bsub>(P' j)\<^esub>\<prec> x" "x \<^bsub>(P' j)\<^esub>\<prec> y"
       and ixyzP': "\<And>i. i \<noteq> j \<longrightarrow> z \<^bsub>(P' i)\<^esub>\<prec> x \<and> y \<^bsub>(P' i)\<^esub>\<prec> x \<and> ((y \<^bsub>(P' i)\<^esub>\<preceq> z) = (y \<^bsub>(P i)\<^esub>\<preceq> z)) \<and> ((z \<^bsub>(P' i)\<^esub>\<preceq> y) = (z \<^bsub>(P i)\<^esub>\<preceq> y))"
     by - (rule decisive2_witness, blast+)
   from iia have "\<And>a b. \<lbrakk> a \<in> {y, z}; b \<in> {y, z} \<rbrakk> \<Longrightarrow> (a \<^bsub>(swf P)\<^esub>\<preceq> b) = (a \<^bsub>(swf P')\<^esub>\<preceq> b)"
   proof(rule iiaE)
     from has3A show "{y,z} \<subseteq> A" by simp
   next
     fix i assume iIs: "i \<in> Is"
     fix a b assume ab: "a \<in> {y, z}" "b \<in> {y, z}"
     show "(a \<^bsub>(P' i)\<^esub>\<preceq> b) = (a \<^bsub>(P i)\<^esub>\<preceq> b)"
     proof(cases "i = j")
       case False
       with ab iIs ixyzP' profileP profileP' has3A
       show ?thesis unfolding profile_def by auto
     next
       case True
       from profileP' jIs jxyzP' have "z \<^bsub>(P' j)\<^esub>\<prec> y"
         by (auto dest: rpr_less_trans)
       with True ab iIs jyzP profileP profileP' has3A
       show ?thesis unfolding profile_def strict_pref_def by auto
     qed
   qed (simp_all add: profileP profileP')
   moreover have "z \<^bsub>(swf P')\<^esub>\<prec> y"
   proof -
     from profileP' sd jxyzP' ixyzP' have "x \<^bsub>(swf P')\<^esub>\<prec> y" by (simp add: semidecisive_def)
     moreover
     from jxyzP' ixyzP' have "\<And>i. i \<in> Is \<Longrightarrow> z \<^bsub>(P' i)\<^esub>\<prec> x" by (case_tac "i=j", auto)
     with wp profileP' has3A have "z \<^bsub>(swf P')\<^esub>\<prec> x" by (auto dest: weak_paretoD)
     moreover note SWF_rpr[OF swf] profileP'
     ultimately show "z \<^bsub>(swf P')\<^esub>\<prec> y"
       unfolding universal_domain_def by (blast dest: rpr_less_trans)
   qed
   ultimately show "z \<^bsub>(swf P)\<^esub>\<prec> y" unfolding strict_pref_def by blast
 qed
 
 text \<open>The following results permute $x$, $y$ and $z$ to show how
 decisiveness can be obtained from semi-decisiveness in all cases. Again,
 quite tedious.\<close>
 
 lemma decisive3:
   assumes has3A: "hasw [x,y,z] A"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
       and sd: "semidecisive swf A Is {j} x z"
   shows "decisive swf A Is {j} y z"
   using has3A decisive2[OF _ iia swf wp sd] by (simp, blast)
 
 lemma decisive4:
   assumes has3A: "hasw [x,y,z] A"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
       and sd: "semidecisive swf A Is {j} y z"
   shows "decisive swf A Is {j} y x"
   using has3A decisive1[OF _ iia swf wp sd] by (simp, blast)
 
 lemma decisive5:
   assumes has3A: "hasw [x,y,z] A"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
       and sd: "semidecisive swf A Is {j} x y"
   shows "decisive swf A Is {j} y x"
 proof -
   from sd
   have "decisive swf A Is {j} x z" by (rule decisive1[OF has3A iia swf wp])
   hence "semidecisive swf A Is {j} x z" by (rule d_imp_sd)
   hence "decisive swf A Is {j} y z" by (rule decisive3[OF has3A iia swf wp])
   hence "semidecisive swf A Is {j} y z" by (rule d_imp_sd)
   thus "decisive swf A Is {j} y x" by (rule decisive4[OF has3A iia swf wp])
 qed
 
 lemma decisive6:
   assumes has3A: "hasw [x,y,z] A"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
       and sd: "semidecisive swf A Is {j} y x"
   shows "decisive swf A Is {j} y z" "decisive swf A Is {j} z x" "decisive swf A Is {j} x y"
 proof -
   from has3A have has3A': "hasw [y,x,z] A" by auto
   show "decisive swf A Is {j} y z" by (rule decisive1[OF has3A' iia swf wp sd])
   show "decisive swf A Is {j} z x" by (rule decisive2[OF has3A' iia swf wp sd])
   show "decisive swf A Is {j} x y" by (rule decisive5[OF has3A' iia swf wp sd])
 qed
 
 lemma decisive7:
   assumes has3A: "hasw [x,y,z] A"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
       and sd: "semidecisive swf A Is {j} x y"
   shows "decisive swf A Is {j} y z" "decisive swf A Is {j} z x" "decisive swf A Is {j} x y"
 proof -
   from sd
   have "decisive swf A Is {j} y x" by (rule decisive5[OF has3A iia swf wp])
   hence "semidecisive swf A Is {j} y x" by (rule d_imp_sd)
   thus "decisive swf A Is {j} y z" "decisive swf A Is {j} z x" "decisive swf A Is {j} x y"
     by (rule decisive6[OF has3A iia swf wp])+
 qed
 
 lemma j_decisive_xy:
   assumes has3A: "hasw [x,y,z] A"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
       and sd: "semidecisive swf A Is {j} x y"
       and uv: "hasw [u,v] {x,y,z}"
   shows "decisive swf A Is {j} u v"
   using uv decisive1[OF has3A iia swf wp sd]
            decisive2[OF has3A iia swf wp sd]
            decisive5[OF has3A iia swf wp sd]
            decisive7[OF has3A iia swf wp sd]
   by (simp, blast)
 
 lemma j_decisive:
   assumes has3A: "has 3 A"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
       and xyA: "hasw [x,y] A"
       and sd: "semidecisive swf A Is {j} x y"
       and uv: "hasw [u,v] A"
   shows "decisive swf A Is {j} u v"
 proof -
   from has_extend_witness'[OF has3A xyA]
   obtain z where xyzA: "hasw [x,y,z] A" by auto
   {
     assume ux: "u = x" and vy: "v = y"
     with xyzA iia swf wp sd have ?thesis by (auto intro: j_decisive_xy)
   }
   moreover
   {
     assume ux: "u = x" and vNEy: "v \<noteq> y"
     with uv xyA iia swf wp sd have ?thesis by(auto intro: j_decisive_xy[of x y])
   }
   moreover
   {
     assume uy: "u = y" and vx: "v = x"
     with xyzA iia swf wp sd have ?thesis by (auto intro: j_decisive_xy)
   }
   moreover
   {
     assume uy: "u = y" and vNEx: "v \<noteq> x"
     with uv xyA iia swf wp sd have ?thesis by (auto intro: j_decisive_xy)
   }
   moreover
   {
     assume uNExy: "u \<notin> {x,y}" and vx: "v = x"
     with uv xyA iia swf wp sd have ?thesis by (auto intro: j_decisive_xy[of x y])
   }
   moreover
   {
     assume uNExy: "u \<notin> {x,y}" and vy: "v = y"
     with uv xyA iia swf wp sd have ?thesis by (auto intro: j_decisive_xy[of x y])
   }
   moreover
   {
     assume uNExy: "u \<notin> {x,y}" and vNExy: "v \<notin> {x,y}"
     with uv xyA iia swf wp sd
     have "decisive swf A Is {j} x u" by (auto intro: j_decisive_xy[where x=x and z=u])
     hence sdxu: "semidecisive swf A Is {j} x u" by (rule d_imp_sd)
     with uNExy vNExy uv xyA iia swf wp have ?thesis by (auto intro: j_decisive_xy[of x])
   }
   ultimately show ?thesis by blast
 qed
 
 text \<open>The first result: if $j$ is semidecisive for some alternatives $u$
 and $v$, then they are actually a dictator.\<close>
 
 lemma sd_imp_dictator:
   assumes has3A: "has 3 A"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
       and uv: "hasw [u,v] A"
       and sd: "semidecisive swf A Is {j} u v"
   shows "dictator swf A Is j"
 proof
   fix x y assume x: "x \<in> A" and y: "y \<in> A"
   show "decisive swf A Is {j} x y"
   proof(cases "x = y")
     case True with sd show "decisive swf A Is {j} x y" by (blast intro: d_refl)
   next
     case False
     with x y iia swf wp has3A uv sd show "decisive swf A Is {j} x y"
       by (auto intro: j_decisive)
   qed
 next
   from sd show "j \<in> Is" by blast
 qed
 
 (* **************************************** *)
 
 subsection\<open>The Existence of a Semi-decisive Individual\<close>
 
 text\<open>The second half of the proof establishes the existence of a
 semi-decisive individual. The required witness is essentially an encoding of
 the Condorcet pardox (aka "the paradox of voting" that shows we get tied up
 in knots if a certain agent didn't have dictatorial powers.\<close>
 
 lemma sd_exists_witness:
   assumes has3A: "hasw [x,y,z] A"
       and Vs: "Is = V1 \<union> V2 \<union> V3
                 \<and> V1 \<inter> V2 = {} \<and> V1 \<inter> V3 = {} \<and> V2 \<inter> V3 = {}"
       and Is: "Is \<noteq> {}"
   obtains P
     where "profile A Is P"
       and "\<forall>i \<in> V1. x \<^bsub>(P i)\<^esub>\<prec> y \<and> y \<^bsub>(P i)\<^esub>\<prec> z"
       and "\<forall>i \<in> V2. z \<^bsub>(P i)\<^esub>\<prec> x \<and> x \<^bsub>(P i)\<^esub>\<prec> y"
       and "\<forall>i \<in> V3. y \<^bsub>(P i)\<^esub>\<prec> z \<and> z \<^bsub>(P i)\<^esub>\<prec> x"
 proof
   let ?P =
     "\<lambda>i. (if i \<in> V1 then  ({ (x, u) | u. u \<in> A }
                          \<union> { (y, u) | u. u \<in> A \<and> u \<noteq> x }
                          \<union> { (z, u) | u. u \<in> A \<and> u \<noteq> x \<and> u \<noteq> y })
                     else 
           if i \<in> V2 then ({ (z, u) | u. u \<in> A }
                         \<union> { (x, u) | u. u \<in> A \<and> u \<noteq> z }
                         \<union> { (y, u) | u. u \<in> A \<and> u \<noteq> x \<and> u \<noteq> z }) 
                    else  ({ (y, u) | u. u \<in> A }
                         \<union> { (z, u) | u. u \<in> A \<and> u \<noteq> y }
                         \<union> { (x, u) | u. u \<in> A \<and> u \<noteq> y \<and> u \<noteq> z }))
                       \<union> { (u, v) | u v. u \<in> A - {x,y,z} \<and> v \<in> A - {x,y,z}}"
   show "profile A Is ?P"
   proof
     fix i assume iIs: "i \<in> Is"
     show "rpr A (?P i)"
     proof
       show "complete A (?P i)" by (simp add: complete_def, blast)
       from has3A iIs show "refl_on A (?P i)" by - (simp, blast)
       from has3A iIs show "trans (?P i)" by (clarsimp simp add: trans_def)
     qed
   next
     from Is show "Is \<noteq> {}" .
   qed
   from has3A Vs
   show "\<forall>i \<in> V1. x \<^bsub>(?P i)\<^esub>\<prec> y \<and> y \<^bsub>(?P i)\<^esub>\<prec> z"
    and "\<forall>i \<in> V2. z \<^bsub>(?P i)\<^esub>\<prec> x \<and> x \<^bsub>(?P i)\<^esub>\<prec> y"
    and "\<forall>i \<in> V3. y \<^bsub>(?P i)\<^esub>\<prec> z \<and> z \<^bsub>(?P i)\<^esub>\<prec> x"
     unfolding strict_pref_def by auto
 qed
 
 text \<open>This proof is unfortunately long. Many of the statements rely on a
 lot of context, making it difficult to split it up.\<close>
 
 lemma sd_exists:
   assumes has3A: "has 3 A"
       and finiteIs: "finite Is"
       and twoIs: "has 2 Is"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
   shows "\<exists>j u v. hasw [u,v] A \<and> semidecisive swf A Is {j} u v"
 proof -
   let ?P = "\<lambda>S. S \<subseteq> Is \<and> S \<noteq> {} \<and> (\<exists>u v. hasw [u,v] A \<and> semidecisive swf A Is S u v)"
   obtain u v where uvA: "hasw [u,v] A" 
     using has_witness_two[OF has3A] by auto
       \<comment> \<open>The weak pareto requirement implies that the set of all
       individuals is decisive between any given alternatives.\<close>
   hence "decisive swf A Is Is u v"
     by - (rule, auto intro: weak_paretoD[OF wp])
   hence "semidecisive swf A Is Is u v" by (rule d_imp_sd)
   with uvA twoIs has_suc_notempty[where n=1] nat_2[symmetric]
   have "?P Is" by auto
       \<comment> \<open>Obtain a minimally-sized semi-decisive set.\<close>
   from ex_has_least_nat[where P="?P" and m="card", OF this]
   obtain V x y where VIs: "V \<subseteq> Is"
     and Vnotempty: "V \<noteq> {}"
     and xyA: "hasw [x,y] A"
     and Vsd: "semidecisive swf A Is V x y"
     and Vmin: "\<And>V'. ?P V' \<Longrightarrow> card V \<le> card V'"
     by blast
   from VIs finiteIs have Vfinite: "finite V" by (rule finite_subset)
       \<comment> \<open>Show that minimal set contains a single individual.\<close>
   from Vfinite Vnotempty have "\<exists>j. V = {j}"
   proof(rule finite_set_singleton_contra)
     assume Vcard: "1 < card V"
     then obtain j where jV: "{j} \<subseteq> V"
       using has_extend_witness[where xs="[]", OF card_has[where n="card V"]] by auto
         \<comment> \<open>Split an individual from the "minimal" set.\<close>
     let ?V1 = "{j}"
     let ?V2 = "V - ?V1"
     let ?V3 = "Is - V"
-    from jV card_Diff_singleton[OF Vfinite] Vcard
+    from jV card_Diff_singleton Vcard
     have V2card: "card ?V2 > 0" "card ?V2 < card V" by auto
     hence V2notempty: "{} \<noteq> ?V2" by auto
     from jV VIs
     have jV2V3: "Is = ?V1 \<union> ?V2 \<union> ?V3 \<and> ?V1 \<inter> ?V2 = {} \<and> ?V1 \<inter> ?V3 = {} \<and> ?V2 \<inter> ?V3 = {}"
       by auto
         \<comment> \<open>Show that that individual is semi-decisive for $x$ over $z$.\<close>
     from has_extend_witness'[OF has3A xyA]
     obtain z where threeDist: "hasw [x,y,z] A" by auto
     from sd_exists_witness[OF threeDist jV2V3] VIs Vnotempty
     obtain P where profileP: "profile A Is P"
                and V1xyzP: "x \<^bsub>(P j)\<^esub>\<prec> y \<and> y \<^bsub>(P j)\<^esub>\<prec> z"
                and V2xyzP: "\<forall>i \<in> ?V2. z \<^bsub>(P i)\<^esub>\<prec> x \<and> x \<^bsub>(P i)\<^esub>\<prec> y"
                and V3xyzP: "\<forall>i \<in> ?V3. y \<^bsub>(P i)\<^esub>\<prec> z \<and> z \<^bsub>(P i)\<^esub>\<prec> x"
       by (simp, blast)
     have xPz: "x \<^bsub>(swf P)\<^esub>\<prec> z"
     proof(rule rpr_less_le_trans[where y="y"])
       from profileP swf show "rpr A (swf P)" by auto
     next
         \<comment> \<open>V2 is semi-decisive, and everyone else opposes their choice. Ergo they prevail.\<close>
       show "x \<^bsub>(swf P)\<^esub>\<prec> y"
       proof -
         from profileP V3xyzP
         have "\<forall>i \<in> ?V3. y \<^bsub>(P i)\<^esub>\<prec> x" by (blast dest: rpr_less_trans)
         with profileP V1xyzP V2xyzP Vsd
         show ?thesis unfolding semidecisive_def by auto
       qed
     next
       \<comment> \<open>This result is unfortunately quite tortuous.\<close>
       from SWF_rpr[OF swf] show "y \<^bsub>(swf P)\<^esub>\<preceq> z"
       proof(rule rpr_less_not[OF _ _ notI])
         from threeDist show "hasw [z, y] A" by auto
       next
         assume zPy: "z \<^bsub>(swf P)\<^esub>\<prec> y"
         have "semidecisive swf A Is ?V2 z y"
         proof
           from VIs show "V - {j} \<subseteq> Is" by blast
         next
           fix P'
           assume profileP': "profile A Is P'"
             and V2yz': "\<And>i. i \<in> ?V2 \<Longrightarrow> z \<^bsub>(P' i)\<^esub>\<prec> y"
             and nV2yz': "\<And>i. i \<in> Is - ?V2 \<Longrightarrow> y \<^bsub>(P' i)\<^esub>\<prec> z"
           from iia have "\<And>a b. \<lbrakk> a \<in> {y, z}; b \<in> {y, z} \<rbrakk> \<Longrightarrow> (a \<^bsub>(swf P)\<^esub>\<preceq> b) = (a \<^bsub>(swf P')\<^esub>\<preceq> b)"
           proof(rule iiaE)
             from threeDist show yzA: "{y,z} \<subseteq> A" by simp
           next
             fix i assume iIs: "i \<in> Is"
             fix a b assume ab: "a \<in> {y, z}" "b \<in> {y, z}"
             with VIs profileP V2xyzP
             have V2yzP: "\<forall>i \<in> ?V2. z \<^bsub>(P i)\<^esub>\<prec> y" by (blast dest: rpr_less_trans)
             show "(a \<^bsub>(P' i)\<^esub>\<preceq> b) = (a \<^bsub>(P i)\<^esub>\<preceq> b)"
             proof(cases "i \<in> ?V2")
               case True
               with VIs profileP profileP' ab V2yz' V2yzP threeDist
               show ?thesis unfolding strict_pref_def profile_def by auto
             next
               case False
               from V1xyzP V3xyzP
               have "\<forall>i \<in> Is - ?V2. y \<^bsub>(P i)\<^esub>\<prec> z" by auto
               with iIs False VIs jV profileP profileP' ab nV2yz' threeDist
               show ?thesis unfolding profile_def strict_pref_def by auto
             qed
           qed (simp_all add: profileP profileP')
           with zPy show "z \<^bsub>(swf P')\<^esub>\<prec> y" unfolding strict_pref_def by blast
         qed
         with VIs Vsd Vmin[where V'="?V2"] V2card V2notempty threeDist show False
           by auto
       qed (simp add: profileP threeDist)
     qed
     have "semidecisive swf A Is ?V1 x z"
     proof
       from jV VIs show "{j} \<subseteq> Is" by blast
     next
       \<comment> \<open>Use @{term "iia"} to show the SWF must allow the individual to prevail.\<close>
       fix P'
       assume profileP': "profile A Is P'"
          and V1yz': "\<And>i. i \<in> ?V1 \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> z"
          and nV1yz': "\<And>i. i \<in> Is - ?V1 \<Longrightarrow> z \<^bsub>(P' i)\<^esub>\<prec> x"
       from iia have "\<And>a b. \<lbrakk> a \<in> {x, z}; b \<in> {x, z} \<rbrakk> \<Longrightarrow> (a \<^bsub>(swf P)\<^esub>\<preceq> b) = (a \<^bsub>(swf P')\<^esub>\<preceq> b)"
       proof(rule iiaE)
         from threeDist show xzA: "{x,z} \<subseteq> A" by simp
       next
         fix i assume iIs: "i \<in> Is"
         fix a b assume ab: "a \<in> {x, z}" "b \<in> {x, z}"
         show "(a \<^bsub>(P' i)\<^esub>\<preceq> b) = (a \<^bsub>(P i)\<^esub>\<preceq> b)"
         proof(cases "i \<in> ?V1")
           case True
           with jV VIs profileP V1xyzP
           have "\<forall>i \<in> ?V1. x \<^bsub>(P i)\<^esub>\<prec> z" by (blast dest: rpr_less_trans)
           with True jV VIs profileP profileP' ab V1yz' threeDist
           show ?thesis unfolding strict_pref_def profile_def by auto
         next
           case False
           from V2xyzP V3xyzP
           have "\<forall>i \<in> Is - ?V1. z \<^bsub>(P i)\<^esub>\<prec> x" by auto
           with iIs False VIs jV profileP profileP' ab nV1yz' threeDist
           show ?thesis unfolding strict_pref_def profile_def by auto
         qed
       qed (simp_all add: profileP profileP')
       with xPz show "x \<^bsub>(swf P')\<^esub>\<prec> z" unfolding strict_pref_def by blast
     qed
     with jV VIs Vsd Vmin[where V'="?V1"] V2card threeDist show False
       by auto
   qed
   with xyA Vsd show ?thesis by blast
 qed
 
 (* **************************************** *)
 
 subsection\<open>Arrow's General Possibility Theorem\<close>
 
 text\<open>
 
 Finally we conclude with the celebrated ``possibility'' result. Note that we
 assume the set of individuals is finite; \cite{Routley:79} relaxes this with
 some fancier set theory. Having an infinite set of alternatives doesn't
 matter, though the result is a bit more plausible if we assume finiteness
 \cite[p54]{Sen:70a}.
 
 \<close>
 
 theorem ArrowGeneralPossibility:
   assumes has3A: "has 3 A"
       and finiteIs: "finite Is"
       and has2Is: "has 2 Is"
       and iia: "iia swf A Is"
       and swf: "SWF swf A Is universal_domain"
       and wp: "weak_pareto swf A Is universal_domain"
   obtains j where "dictator swf A Is j"
   using sd_imp_dictator[OF has3A iia swf wp]
         sd_exists[OF has3A finiteIs has2Is iia swf wp]
   by blast
 
 (*<*)
 end
 (*>*)