Theory List-Infinite.SetInterval2

(*  Title:      SetInterval2.thy
    Date:       Oct 2006
    Author:     David Trachtenherz
*)

section ‹Sets of natural numbers›

theory SetInterval2
imports
  "HOL-Library.Infinite_Set"
  Util_Set
  "../CommonArith/Util_MinMax"
  "../CommonArith/Util_NatInf"
  "../CommonArith/Util_Div"
begin

subsection ‹Auxiliary results for monotonic, injective and surjective functions over sets›

subsubsection ‹Monotonicity›

definition mono_on :: "('a::order  'b::order)  'a set  bool"
  where "mono_on f A  aA. bA. a  b  f a  f b"

definition strict_mono_on :: "('a::order  'b::order)  'a set  bool"
  where "strict_mono_on f A  aA. bA. a < b  f a < f b"


lemma mono_on_subset: " mono_on f A ; B  A   mono_on f B"
unfolding mono_on_def by blast

lemma strict_mono_on_subset: " strict_mono_on f A ; B  A   strict_mono_on f B"
unfolding strict_mono_on_def by blast


lemma mono_on_UNIV_mono_conv: "mono_on f UNIV = mono f"
unfolding mono_on_def mono_def by blast
lemma strict_mono_on_UNIV_strict_mono_conv: "
  strict_mono_on f UNIV = strict_mono f"
unfolding strict_mono_on_def strict_mono_def by blast

lemma mono_imp_mono_on: "mono f  mono_on f A"
unfolding mono_on_def mono_def by blast
lemma strict_mono_imp_strict_mono_on: "strict_mono f  strict_mono_on f A"
unfolding strict_mono_on_def strict_mono_def by blast

lemma strict_mono_on_imp_mono_on: "strict_mono_on f A  mono_on f A"
apply (unfold strict_mono_on_def mono_on_def)
apply (fastforce simp: order_le_less)
done


subsubsection ‹Injectivity›

lemma inj_imp_inj_on: "inj f  inj_on f A"
unfolding inj_on_def by blast

lemma strict_mono_on_imp_inj_on: "
  strict_mono_on f (A::'a::linorder set)  inj_on f A"
apply (unfold strict_mono_on_def inj_on_def, clarify)
apply (rule ccontr)
apply (fastforce simp add: linorder_neq_iff)
done



lemma strict_mono_imp_inj: "strict_mono (f::('a::linorder  'b::order))  inj f"
by (rule strict_mono_imp_inj_on)

lemma strict_mono_on_mono_on_conv: "
  strict_mono_on f (A::'a::linorder set) = (mono_on f A  inj_on f A)"
apply (rule iffI)
 apply (frule strict_mono_on_imp_mono_on)
 apply (frule strict_mono_on_imp_inj_on)
 apply blast
apply (erule conjE)
apply (unfold inj_on_def mono_on_def strict_mono_on_def, clarify)
apply fastforce
done

corollary strict_mono_mono_conv: "
  strict_mono (f::('a::linorder  'b::order)) = (mono f  inj f)"
by (simp only: strict_mono_on_UNIV_strict_mono_conv[symmetric]
  mono_on_UNIV_mono_conv[symmetric] strict_mono_on_mono_on_conv)


lemma inj_on_image_mem_iff: "
   inj_on f A; B  A; a  A   (f a  f ` B) = (a  B)"
unfolding inj_on_def by blast

corollary inj_on_union_image_Int: "
  inj_on f (A  B)  f ` (A  B) = f ` A  f ` B"
by (rule inj_on_image_Int[OF _ Un_upper1 Un_upper2])


subsubsection ‹Surjectivity›

definition surj_on :: "('a  'b)  'a set  'b set  bool"
  where "surj_on f A B  bB. aA. b = f a"

lemma surj_on_conv: "(surj_on f A B) = (bB. aA. b = f a)"
unfolding surj_on_def ..

lemma surj_on_image_conv: "(surj_on f A B) = (B  f ` A)"
unfolding surj_on_conv by blast

lemma surj_on_id: "surj_on id A A"
unfolding id_def surj_on_conv by blast

lemma
  surj_onI: " b  B. aA. b = f a   surj_on f A B" and
  surj_onD2: "surj_on f A B  b  B. aA. b = f a" and
  surj_onD: " surj_on f A B; b  B   aA. b = f a"
unfolding surj_on_conv
by blast+

lemma comp_surj_on: "
   surj_on f A B; surj_on g B C   surj_on (g  f) A C"
unfolding comp_def surj_on_image_conv by blast

lemma surj_on_Un_right: "surj_on f A (B1  B2) = (surj_on f A B1  surj_on f A B2)"
unfolding surj_on_image_conv
by blast

lemma surj_on_Un_left: "
  surj_on f (A1  A2) B =
  (B1. B2. B  B1  B2  surj_on f A1 B1  surj_on f A2 B2)"
unfolding surj_on_image_conv
apply (rule iffI)
 apply (rule_tac x="f ` A1" in exI)
 apply (rule_tac x="f ` A2" in exI)
 apply blast
apply blast
done

lemma surj_on_diff_right: "surj_on f A B  surj_on f A (B - B')"
unfolding surj_on_conv by blast

lemma surj_on_empty_right: "surj_on f A {}"
unfolding surj_on_conv by blast

lemma surj_on_empty_left: "surj_on f {} B = (B = {})"
unfolding surj_on_conv by blast

lemma surj_on_imageI: "surj_on (g  f) A B  surj_on g (f ` A) B"
unfolding surj_on_conv by fastforce

lemma surj_on_insert_right: "surj_on f A (insert b B) = (surj_on f A B  surj_on f A {b})"
unfolding surj_on_conv by blast

lemma surj_on_insert_left: "surj_on f (insert a A) B = (surj_on f A (B - {f a}))"
unfolding surj_on_conv by blast

lemma surj_on_subset_right: " surj_on f A B; B'  B   surj_on f A B'"
unfolding surj_on_conv by blast

lemma surj_on_subset_left: " surj_on f A B; A  A'   surj_on f A' B"
unfolding surj_on_conv by blast

lemma bij_betw_imp_surj_on: "bij_betw f A B  surj_on f A B"
unfolding bij_betw_def surj_on_image_conv by simp

lemma bij_betw_inj_on_surj_on_conv: "
  bij_betw f A B = (inj_on f A  surj_on f A B  f ` A  B)"
unfolding bij_betw_def surj_on_image_conv by blast


subsubsection ‹Induction over natural sets›

lemma image_nat_induct: "
   P (f 0); n. P (f n)  P (f (Suc n)); surj_on f UNIV I; a  I   P a"
proof -
  assume as_P0: "P (f 0)"
    and  as_IA: "n. P (f n)  P (f (Suc n))"
    and  as_surj_f: "surj_on f UNIV I"
    and  as_a: "a  I"
  have P_n:"n. P (f n)"
    apply (induct_tac n)
    apply (simp only: as_P0)
    apply (simp only: as_IA)
    done
  have "xI. n. x = f n"
    using as_surj_f
    by (unfold surj_on_conv, blast)
  hence "n. a = f n"
    using as_a by blast
  thus "P a"
    using P_n by blast
qed

lemma nat_induct'[rule_format]: "
   P n0; n.  n0  n;  P n   P (Suc n); n0  n   P n"
by (insert nat_induct[where n="n-n0" and P="λn. P (n0+n)"], simp)

lemma enat_induct: "
   P 0; P ; n. P n  P (eSuc n)  P n"
apply (case_tac n)
 prefer 2
 apply simp
apply (simp only: enat_defs)
apply (rename_tac n1)
apply (induct_tac n1)
apply (simp add: enat.splits)+
done


lemma eSuc_imp_Suc_aux_0:
  " n. P n  P (eSuc n); n0'  n'; P (enat n')  P (enat (Suc n'))"
by (simp only: enat_defs enat.splits)

lemma eSuc_imp_Suc_aux_n0:
  " n. enat n0'  n; P n  P (eSuc n); n0'  n'; P (enat n')  P (enat (Suc n'))"
proof -
  assume IA: "n. enat n0'  n; P n  P (eSuc n)"
    and n0_n: "n0'  n'"
    and Pn: "P (enat n')"
  from n0_n
  have "(enat n0'  enat n')" by simp
  with Pn IA
  have "P (eSuc (enat n'))" by blast
  thus "P (enat (Suc n'))" by (simp only: eSuc_enat)
qed

lemma enat_induct': "
   P (n0::enat); P ; n.  n0  n;  P n   P (eSuc n); n0  n   P n"
apply (case_tac n)
 prefer 2 apply simp
apply (case_tac n0)
 prefer 2 apply simp
apply (rename_tac n' n0', simp)
apply (rule_tac ?n0.0="n0'" and n=n' and P="λn. P (enat n)" in nat_induct')
  apply simp
 apply (simp add: eSuc_enat[symmetric])
apply simp
done

lemma wf_less_interval:"
  wf { (x,y). x  (I::nat set)  y  I  x < y }"
apply (rule wf_subset[where
  p="{ (x,y). x  I  y  I  x < y }" and
  r="{(x,y). x < y}"])
apply (rule wf_less)
apply blast
done

lemma interval_induct: "
   x. y. (x(I::nat set)  y  I  y < x  P y)  P x 
   P a"
  (is " x. y. ?IA x y  P x   P a")
apply (rule_tac r="{ (x,y). x  I  y  I  x < y }" in wf_induct)
apply (rule wf_less_interval)
apply simp
done

corollary interval_induct_rule:"
   x. (y. (x(I::nat set)  y  I  y < x  P y))  P x 
   P a"
by (blast intro: interval_induct)


subsubsection ‹Monotonicity and injectivity of artithmetic operators›

lemma add_left_inj: "inj (λx. n + (x::'a::cancel_ab_semigroup_add))"
by (simp add: inj_on_def)

lemma add_right_inj: "inj (λx. x + (n::'a::cancel_ab_semigroup_add))"
by (simp add: inj_on_def)

lemma mult_left_inj: "0 < n  inj (λx. (n::nat) * x)"
by (simp add: inj_on_def)

lemma mult_right_inj: "0 < n  inj (λx. x * (n::nat))"
by (simp add: inj_on_def)

lemma sub_left_inj_on: "inj_on (λx. (x::nat) - k) {k..}"
by (rule inj_onI, simp)

lemma sub_right_inj_on: "inj_on (λx. k - (x::nat)) {..k}"
by (rule inj_onI, simp)

lemma add_left_strict_mono: "strict_mono (λx. n + (x::'a::ordered_cancel_ab_semigroup_add))"
by (unfold strict_mono_def, clarify, rule add_strict_left_mono)

lemma add_right_strict_mono: "strict_mono (λx. x + (n::'a::ordered_cancel_ab_semigroup_add))"
by (unfold strict_mono_def, clarify, rule add_strict_right_mono)

lemma mult_left_strict_mono: "0 < n  strict_mono (λx. n * (x::nat))"
by (unfold strict_mono_def, clarify, simp)

lemma mult_right_strict_mono: "0 < n  strict_mono (λx. x * (n::nat))"
by (unfold strict_mono_def, clarify, simp)

lemma sub_left_strict_mono_on: "strict_mono_on (λx. (x::nat) - k) {k..}"
apply (rule strict_mono_on_mono_on_conv[THEN iffD2], rule conjI)
apply (unfold mono_on_def, clarify, simp)
apply (rule sub_left_inj_on)
done

lemma div_right_strict_mono_on: "
   0 < (k::nat); xI. yI. x < y  x + k  y  
  strict_mono_on (λx. x div k) I"
apply (unfold strict_mono_on_def, clarify)
apply (fastforce dest: div_le_mono[of _ _ k])
done

lemma mod_eq_div_right_strict_mono_on: "
   0 < (k::nat); xI. yI. x mod k = y mod k  
  strict_mono_on (λx. x div k) I"
apply (rule div_right_strict_mono_on, simp)
apply (blast intro: less_mod_eq_imp_add_divisor_le)
done

corollary div_right_inj_on: "
   0 < (k::nat); xI. yI. x < y  x + k  y  
  inj_on (λx. x div k) I"
by (rule strict_mono_on_imp_inj_on[OF div_right_strict_mono_on])

corollary mod_eq_imp_div_right_inj_on: "
   0 < (k::nat); xI. yI. x mod k = y mod k  
  inj_on (λx. x div k) I"
by (rule strict_mono_on_imp_inj_on[OF mod_eq_div_right_strict_mono_on])


subsection Min› and Max› elements of a set›

text ‹A special minimum operator is required for dealing with infinite wellordered sets
  because the standard operator @{term "Min"} is usable only with finite sets.›

definition iMin :: "'a::wellorder set  'a"
  where "iMin I  LEAST x. x  I"


subsubsection ‹Basic results, as for Least›

lemma iMinI: "k  I  iMin I  I"
unfolding iMin_def
by (rule_tac k=k in LeastI)

lemma iMinI_ex: "x. x  I  iMin I  I"
by (blast intro: iMinI)

corollary  iMinI_ex2: "I  {}  iMin I  I"
by (blast intro: iMinI_ex)

lemma iMinI2: " k  I; x. x  I  P x   P (iMin I)"
by (blast intro: iMinI)

lemma iMinI2_ex: " x. x  I; x. x  I  P x   P (iMin I)"
by (blast intro: iMinI_ex)

lemma iMinI2_ex2: " I  {} ; x. x  I  P x   P (iMin I)"
by (blast intro: iMinI_ex2)

lemma iMin_le[dest]: "k  I  iMin I  k"
by (simp only: iMin_def Least_le)

lemma iMin_neq_imp_greater[dest]: " k  I; k  iMin I   iMin I < k"
by (rule order_neq_le_trans[OF not_sym iMin_le])

lemma iMin_mono: "
   mono f; x. x  I   iMin (f ` I) = f (iMin I)"
apply (unfold iMin_def)
apply (rule Least_mono[of f I], simp)
apply (rule_tac x="iMin I" in bexI)
 apply (simp add: iMin_le)
apply (simp add: iMinI_ex)
done

corollary iMin_mono2: "
   mono f; I  {}   iMin (f ` I) = f (iMin I)"
by (blast intro: iMin_mono)

lemma not_less_iMin: "k < iMin I  k  I"
unfolding iMin_def
by (rule not_less_Least)

lemma Collect_not_less_iMin: "k < iMin {x. P x}  ¬ P k"
by (drule not_less_iMin, blast)

lemma Collect_iMin_le: "P k  iMin {x. P x}  k"
by (rule iMin_le, blast)

lemma Collect_minI: " k  I; P (k::('a::wellorder))   xI. P x  (yI. y < x  ¬ P y)"
apply (rule_tac x="iMin {y  I. P y}" in bexI)
 prefer 2
 apply (rule subsetD[OF _ iMinI, OF Collect_is_subset], blast)
apply (rule conjI)
 apply (blast intro: iMinI2)
apply (blast dest: not_less_iMin)
done

corollary Collect_minI_ex: "kI. P (k::('a::wellorder))  xI. P x  (yI. y < x  ¬ P y)"
by (erule bexE, rule Collect_minI)

corollary Collect_minI_ex2: "{kI. P (k::('a::wellorder))}  {}  xI. P x  (yI. y < x  ¬ P y)"
by (drule ex_in_conv[THEN iffD2], blast intro: Collect_minI)

lemma iMin_the:  "iMin I = (THE x. x  I  (y. y  I  x  y))"
by (simp add: iMin_def Least_def)

lemma iMin_the2: "iMin I = (THE x. x  I  (yI. x  y))"
apply (simp add: iMin_the)
apply (subgoal_tac "x. (y  I. x  y) = (y. y  I  x  y) ")
 prefer 2 apply blast
apply simp
done

lemma iMin_equality: "
   k  I; x. x  I  k  x   iMin I = k"
unfolding iMin_def
by (blast intro: Least_equality)

lemma iMin_mono_on: "
   mono_on f I; x. x  I   iMin (f ` I) = f (iMin I)"
apply (unfold mono_on_def)
apply (rule iMin_equality)
apply (blast intro: iMinI_ex)+
done

lemma iMin_mono_on2: "
   mono_on f I; I  {}   iMin (f ` I) = f (iMin I)"
by (rule iMin_mono_on, blast+)

lemma iMinI2_order:"
   k  I; y. y  I  k  y;
    x.  x  I; yI. x  y   P x  
  P (iMin I)"
by (simp add: iMin_def LeastI2_order)

lemma wellorder_iMin_lemma: "
  k  I  iMin I  I  iMin I  k"
by (blast intro: iMinI iMin_le)

lemma iMin_Min_conv: "
   finite I; I  {}   iMin I = Min I"
apply (rule order_antisym)
apply (rule Min_ge_iff[THEN iffD2], assumption+)
apply blast
apply (rule Min_le_iff[THEN iffD2], assumption+)
apply (blast intro: iMinI_ex2)
done

lemma Min_neq_imp_greater[dest]: " finite I; k  I; k  Min I   Min I < k"
by (rule order_neq_le_trans[OF not_sym Min_le])

lemma Max_neq_imp_less[dest]: " finite I; k  I; k  Max I   k < Max I"
by (rule order_neq_le_trans[OF _ Max_ge])

lemma nat_Least_mono: "
   A  {}; mono (f::(natnat))  
  (LEAST x. x  f ` A) = f (LEAST x. x  A)"
unfolding iMin_def[symmetric]
by (blast intro: iMin_mono2)


lemma Least_disj: "
   x. P x; x. Q x  
  (LEAST (x::'a::wellorder). (P x  Q x)) = min (LEAST x. P x) (LEAST x. Q x)"
apply (elim exE, rename_tac x1 x2)
apply (subgoal_tac "x1 x2 P Q. P x1; Q x2; Least P  Least Q  (LEAST x. P x  Q x) = Least P")
 prefer 2
 apply (rule Least_equality)
  apply (blast intro: LeastI Least_le)
  apply (erule disjE)
   apply (rule Least_le, assumption)
  apply (rule order_trans, assumption)
  apply (rule Least_le, assumption)
apply (unfold min_def, split if_split, safe)
 apply blast
apply (subst disj_commute)
apply (fastforce simp: linorder_not_le)
done

lemma Least_imp_le: "
   x. P x; x. P x  Q x  
  (LEAST (x::'a::wellorder). Q x)  (LEAST x. P x)"
by (blast intro: Least_le LeastI2_ex)

lemma Least_imp_disj_eq: "
   x. P x; x. P x  Q x  
  (LEAST (x::'a::wellorder). P x  Q x) = (LEAST x. Q x)"
apply (subst Least_disj, assumption, blast)
apply (subst min.commute)
apply (rule min.absorb_iff1[THEN iffD1])
apply (rule Least_imp_le, assumption, blast)
done

lemma Least_le_imp_le: "
   x. P x; x. Q x; x y.  P x; Q y   x  y  
  (LEAST (x::'a::wellorder). P x)  (LEAST (x::'a::wellorder). Q x)"
by (blast intro: LeastI)
lemma Least_le_imp_le_disj: "
   x. P x; x y.  P x; Q y   x  y  
  (LEAST (x::'a::wellorder). P x  Q x) = (LEAST (x::'a::wellorder). P x)"
apply (case_tac "x. Q x")
 apply (simp only: Least_disj min.absorb_iff1[THEN iffD1, OF Least_le_imp_le])
apply simp
done


lemma Max_equality: " (k::'a::linorder)  A; finite A; x. x  A  x  k  
  Max A = k"
by (rule Max_eqI)

lemma not_greater_Max: " finite A; Max A < k    k  A"
apply (rule ccontr, simp)
apply (frule Max_ge[of A k], blast)
apply (frule order_le_less_trans[of _ _ k], blast)
apply blast
done

lemma Collect_not_greater_Max: " finite {x. P x}; Max {x. P x} < k   ¬ P k"
by (drule not_greater_Max, assumption, drule Collect_not_in_imp_not)

lemma Collect_Max_ge: " finite {x. P x}; P k   k  Max {x. P x}"
by (rule Max_ge, assumption, rule CollectI)

lemma MaxI: " k  A; finite A   Max A  A"
by (case_tac "A = {}", simp_all)

lemma MaxI_ex: " x. x  A; finite A   Max A  A"
by (blast intro: MaxI)

lemma MaxI_ex2: " A  {}; finite A   Max A  A"
by (blast intro: MaxI)

lemma MaxI2: " k  A; x. x  A  P x; finite A   P (Max A)"
by (drule Max_in, blast+)

lemma MaxI2_ex:" x. x  A; x. x  A  P x; finite A   P (Max A)"
by (blast intro: MaxI2)

lemma MaxI2_ex2:" A  {}; x. x  A  P x; finite A   P (Max A)"
by (blast intro: MaxI2)

lemma Max_mono: " mono f; x. x  A; finite A   Max (f ` A) = f (Max A)"
apply (unfold mono_def)
apply clarify
apply (frule Max_in, blast)
apply (rule Max_equality, clarsimp+)
done

lemma Max_mono2:" mono f; A  {}; finite A   Max (f ` A) = f (Max A)"
by (blast intro: Max_mono)

lemma Max_mono_on: " mono_on f A; x. x  A; finite A   Max (f ` A) = f (Max A)"
apply (unfold mono_on_def)
apply (rule Max_equality)
  apply (blast intro: Max_in)
 apply (rule finite_imageI, assumption)
apply (blast intro: Max_in Max_ge)
done

lemma Max_mono_on2: "
   mono_on f A; A  {}; finite A   Max (f ` A) = f (Max A)"
by (rule Max_mono_on, blast+)

lemma Max_the: "
   A  {}; finite A  
  Max A = (THE x. x  A  (y. y  A  y  x))"
apply (rule iffD1[OF eq_commute])
apply (rule the_equality, simp)
apply (rule sym)
apply (rule Max_equality)
apply blast+
done

lemma Max_the2: " A  {}; finite A  
  Max A = (THE x. x  A  (yA. y  x))"
apply (simp add: Max_the)
apply (subgoal_tac "x. (yA. y  x) = (y. y  A  y  x) ")
 prefer 2
 apply blast
apply simp
done

lemma wellorder_Max_lemma: " k  A; finite A   Max A  A  k  Max A"
by (case_tac "A = {}", simp_all)

lemma MaxI2_order: " k  A; finite A; y. y  A  y  k;
  x.  x  A; yA. y  x   P x 
   P (Max A)"
by (simp add: Max_equality)

lemma Min_le_Max: " finite A; A  {}   Min A  Max A"
by (rule Max_ge[OF _ Min_in])

lemma iMin_le_Max: " finite A; A  {}   iMin A  Max A"
by (rule ssubst[OF iMin_Min_conv], assumption+, rule Min_le_Max)


subsubsection Max› for sets over enat›

definition iMax :: "nat set  enat"
  where "iMax i  if (finite i) then (enat (Max i)) else "

lemma iMax_finite_conv: "finite I = (iMax I  )"
by (simp add: iMax_def)

lemma iMax_infinite_conv: "infinite I = (iMax I = )"
by (simp add: iMax_def)

lemma "class.distrib_lattice (min::('a::linorder  'a  'a)) (≤) (<) max"
apply (subgoal_tac "class.order (≤) (<)")
 prefer 2
 apply (rule class.order.intro)
  apply (rule class.preorder.intro)
  apply (rule less_le_not_le)
  apply (rule order_refl)
  apply (rule order_trans, assumption+)
 apply (rule class.order_axioms.intro)
 apply (rule order_antisym, assumption+)
apply (subgoal_tac "class.linorder (≤) (<)")
 prefer 2
 apply (rule class.linorder.intro, assumption)
 apply (rule class.linorder_axioms.intro)
 apply (rule linorder_class.linear)
apply (rule class.distrib_lattice.intro)
 apply (rule class.lattice.intro)
  apply (rule class.semilattice_inf.intro, assumption)
  apply (rule class.semilattice_inf_axioms.intro)
    apply (rule le_minI1)
   apply (rule le_minI2)
  apply (rule conj_le_imp_min, assumption+)
 apply (rule class.semilattice_sup.intro, assumption)
 apply (rule class.semilattice_sup_axioms.intro)
   apply (rule max.cobounded1)
  apply (rule max.cobounded2)
 apply (rule conj_le_imp_max, assumption+)
apply (rule class.distrib_lattice_axioms.intro)
apply (rule max_min_distrib2)
done

print_locale Lattices.distrib_lattice

lemma max_Min_eq_Min_max[rule_format]: "
  finite A 
  A  {} 
  max x (Min A) = Min {max x a |a. a  A}"
apply (rule finite.induct[of A], simp_all del: insert_iff)
apply (rename_tac A1 a)
apply (case_tac "A1 = {}", simp)
apply (rule_tac
  t="{max x b |b. b  insert a A1}" and
  s="insert (max x a) {max x b |b. b  A1}"
  in subst)
 apply blast
apply (subst Min_insert, simp_all)
apply (case_tac "a  Min A1")
 apply (frule max_le_monoR[where x=x])
 apply (simp only: min_eqL)
apply (simp only: linorder_not_le)
apply (frule max_le_monoR[where x=x, OF less_imp_le])
apply (simp only: min_eqR)
done

lemma max_iMin_eq_iMin_max: "
   finite A; A  {}  
  max x (iMin A) = iMin {max x a |a. a  A}"
apply (simp add: iMin_Min_conv)
apply (insert iMin_Min_conv[of "{max x a |a. a  A}"], simp)
apply (subgoal_tac "finite {max x a |a. a  A}")
 prefer 2
 apply simp
apply (simp add: max_Min_eq_Min_max)
done

lemma " finite A; A {}   xA. x  Max A"
by simp


subsubsection Min› and Max› for set operations›

lemma iMin_subset: " A  {}; A  B   iMin B  iMin A"
by (blast intro: iMin_le iMinI_ex2)

lemma Max_subset: " A  {}; A  B; finite B   Max A  Max B"
by (rule linorder_class.Max_mono)

lemma Min_subset: " A  {}; A  B; finite B   Min B  Min A"
by (rule linorder_class.Min_antimono)

lemma iMin_Int_ge1: "(A  B)  {}  iMin A  iMin (A  B)"
by (rule iMin_subset[OF _ Int_lower1])

lemma iMin_Int_ge2: "(A  B)  {}  iMin B  iMin (A  B)"
by (rule iMin_subset[OF _ Int_lower2])

lemma iMin_Int_ge: "(A  B)  {}  max (iMin A) (iMin B)  iMin (A  B)"
apply (rule conj_le_imp_max)
apply (rule iMin_Int_ge1, assumption)
apply (rule iMin_Int_ge2, assumption)
done

lemma Max_Int_le1: " (A  B)  {}; finite A   Max (A  B)  Max A"
by (rule Max_subset[OF _ Int_lower1])

lemma Max_Int_le2: " (A  B)  {}; finite B   Max (A  B)  Max B"
by (rule Max_subset[OF _ Int_lower2])

lemma Max_Int_le: " (A  B)  {}; finite A; finite B  
  Max (A  B)  min (Max A) (Max B)"
apply (rule conj_le_imp_min)
apply (rule Max_Int_le1, assumption+)
apply (rule Max_Int_le2, assumption+)
done





lemma iMin_Un[rule_format]: "
   A  {}; B  {}  
  iMin (A  B) = min (iMin A) (iMin B)"
apply (rule order_antisym)
 apply simp
 apply (blast intro: iMin_subset)
apply (simp add: min_le_iff_disj)
apply (insert iMinI_ex2[of "AB"])
apply (blast intro: iMin_le)
done

lemma iMin_singleton[simp]: "iMin {a} = a"
by (rule singletonI[THEN iMinI, THEN singletonD])

lemma iMax_singleton[simp]: "iMax {a} = enat a"
by (simp add: iMax_def)

lemma Max_le_Min_imp_singleton: "
   finite A; A  {}; Max A  Min A   A = {Min A}"
apply (frule Max_le_iff[THEN iffD1, of _ "Min A"], assumption+)
apply (frule Min_ge_iff[THEN iffD1, of _ "Min A"], assumption, simp)
apply (rule set_eqI)
apply (unfold Ball_def)
apply (erule_tac x=x in allE, erule_tac x=x in allE)
apply (blast intro: order_antisym Min_in)
done
lemma Max_le_Min_conv_singleton: "
   finite A; A  {}   (Max A  Min A) = (x. A = {x})"
apply (rule iffI)
 apply (rule_tac x="Min A" in exI)
 apply (rule Max_le_Min_imp_singleton, assumption+)
apply fastforce
done



lemma Max_le_iMin_imp_le: "
   finite A; Max A  iMin B; a  A; b  B   a  b"
by (blast dest: Max_ge intro: order_trans)

lemma le_imp_Max_le_iMin: "
   finite A; A  {}; B  {}; aA. bB. a  b   Max A  iMin B"
by (blast intro: Max_in iMinI_ex2)

lemma Max_le_iMin_conv_le: "
   finite A; A  {}; B  {}   (Max A  iMin B) = (aA. bB. a  b)"
by (blast intro: Max_le_iMin_imp_le le_imp_Max_le_iMin)

lemma Max_less_iMin_imp_less: "
   finite A; Max A < iMin B; a  A; b  B   a < b"
by (blast dest: Max_less_iff intro: order_less_le_trans iMin_le)

lemma less_imp_Max_less_iMin: "
   finite A; A  {}; B  {}; aA. bB. a < b   Max A < iMin B"
by (blast intro: Max_in iMinI_ex2)

lemma Max_less_iMin_conv_less: "
   finite A; A  {}; B  {}   (Max A < iMin B) = (aA. bB. a < b)"
by (blast intro: Max_less_iMin_imp_less less_imp_Max_less_iMin)

lemma Max_less_iMin_imp_disjoint: "
   finite A; Max A < iMin B   A  B = {}"
apply (case_tac "A = {}", simp)
apply (case_tac "B = {}", simp)
apply (rule disjoint_iff_not_equal[THEN iffD2])
apply (intro ballI)
apply (rule less_imp_neq)
by (rule Max_less_iMin_imp_less)


lemma iMin_in_idem: "n  I  min n (iMin I) = iMin I"
by (simp add: iMin_le min_eqR)

lemma iMin_insert: "I  {}  iMin (insert n I) = min n (iMin I)"
apply (subst insert_is_Un)
apply (subst iMin_Un)
apply simp_all
done

lemma iMin_insert_remove: "
  iMin (insert n I) =
  (if I - {n} = {} then n else min n (iMin (I - {n})))"
by (metis iMin_insert iMin_singleton insert_Diff_single)

lemma iMin_remove: "n  I  iMin I = (if I - {n} = {} then n else min n (iMin (I - {n})))"
by (metis iMin_insert_remove insert_absorb)

lemma iMin_subset_idem: " B  {}; B  A   min (iMin B) (iMin A) = iMin A"
by (metis iMin_subset min.absorb2)

lemma iMin_union_inter: "A  B  {}  min (iMin (A  B)) (iMin (A  B)) = min (iMin A) (iMin B)"
by (metis Int_empty_left Int_lower2 Un_absorb2 Un_assoc Un_empty iMin_Un)

lemma iMin_ge_iff: "I  {}  (n  iMin I) = (aI. n  a)"
by (metis Collect_iMin_le Collect_mem_eq iMinI_ex2 order_trans)

lemma iMin_gr_iff: "I  {}  (n < iMin I) = (aI. n < a)"
by (metis iMinI_ex2 iMin_neq_imp_greater order_less_trans)

lemma iMin_le_iff: "I  {}  (iMin I  n) = (aI. a  n)"
by (metis Collect_iMin_le Collect_mem_eq iMinI_ex2 order_trans)

lemma iMin_less_iff: "I  {}  (iMin I < n) = (aI. a < n)"
by (metis iMinI_ex2 iMin_neq_imp_greater order_less_trans)

lemma hom_iMin_commute: " x y. h (min x y) = min (h x) (h y); I  {}   iMin (h ` I) = h (iMin I)"
apply (rule iMin_equality)
 apply (blast intro: iMinI_ex2)
apply (rename_tac y)
apply (drule_tac x="iMin I" in meta_spec)
apply (clarsimp simp: image_iff, rename_tac x)
apply (drule_tac x=x in meta_spec)
apply (rule_tac t="h (iMin I)" and s="min (h (iMin I)) (h x)" in subst)
 apply (simp add: min_eqL[OF iMin_le])
apply simp
done

text ‹Synonyms for similarity with theorem names for @{term Min}"›

lemmas iMin_eqI = iMin_equality

lemmas iMin_in = iMinI_ex2


subsection ‹Some auxiliary results for set operations›

subsubsection ‹Some additional abbreviations for relations›

text ‹Abbreviations for refl›, sym›, equiv›, refl›, trans›

abbreviation (input) reflP :: "('a  'a  bool)  bool" where
  "reflP r  refl {(x, y). r x y}"

abbreviation (input) symP :: "('a => 'a => bool) => bool" where
  "symP r == sym {(x, y). r x y}"

abbreviation (input) transP :: "('a => 'a => bool) => bool" where
  "transP r == trans {(x, y). r x y}"

abbreviation (input) equivP :: "('a  'a  bool)  bool" where
  "equivP r  reflP r  symP r  transp r"

abbreviation (input) irreflP :: "('a  'a  bool)  bool" where
  "irreflP r  irrefl {(x, y). r x y}"


text ‹Example for reflP›
lemma "reflP ((≤)::('a::preorder  'a  bool))"
by (simp add: refl_on_def)

text ‹Example for symP›
lemma "symP (=)"
by (simp add: sym_def)

text ‹Example for equivP›
lemma "equivP (=)"
by (simp add: trans_def refl_on_def sym_def)

text ‹Example for irreflP›
lemma "irreflP ((<)::('a::preorder  'a  bool))"
by (simp add: irrefl_def)


subsubsection ‹Auxiliary results for singletons›

lemma singleton_not_empty: "{a}  {}" by blast
lemma singleton_finite: "finite {a}" by blast

lemma singleton_ball: "(x{a}. P x) = P a" by blast
lemma singleton_bex: "(x{a}. P x) = P a" by blast

lemma subset_singleton_conv: "(A  {a}) = (A = {}  A = {a})" by blast
lemma singleton_subset_conv: "({a}  A) = (a  A)" by blast

lemma singleton_eq_conv: "({a} = {b}) = (a = b)" by blast
lemma singleton_subset_singleton_conv: "({a}  {b}) = (a = b)" by blast

lemma singleton_Int1_if: "{a}  A = (if a  A then {a} else {})"
by (split if_split, blast)

lemma singleton_Int2_if: "A  {a} = (if a  A then {a} else {})"
by (split if_split, blast)

lemma singleton_image: "f ` {a} = {f a}" by blast
lemma inj_on_singleton: "inj_on f {a}" by blast
lemma strict_mono_on_singleton: "strict_mono_on f {a}"
unfolding strict_mono_on_def by blast


subsubsection ‹Auxiliary results for finite› and infinite› sets›

lemma infinite_imp_not_singleton: "infinite A  ¬ (a. A = {a})" by blast

lemma infinite_insert: "infinite (insert a A) = infinite A"
by simp

lemma infinite_Diff_insert: "infinite (A - insert a B) = infinite (A - B)"
by simp

lemma subset_finite_imp_finite: " finite A; B  A   finite B"
by (rule finite_subset)

lemma infinite_not_subset_finite: " infinite A; finite B   ¬ A  B"
by (blast intro: subset_finite_imp_finite)

lemma Un_infinite_right: "infinite T  infinite (S  T)" by blast
lemma Un_infinite_iff: "infinite (S  T) = (infinite S  infinite T)" by blast

text ‹Give own name to the lemma about finiteness of the integer image of a nat set›
corollary finite_A_int_A_conv: "finite A = finite (int ` A)"
proof -
  have "inj_on int A"
    by (auto intro: inj_onI)
  then show ?thesis
    by (simp add: finite_image_iff)
qed

text ‹Corresponding fact fo infinite sets›
corollary infinite_A_int_A_conv: "infinite A = infinite (int ` A)"
by (simp only: finite_A_int_A_conv)


lemma cartesian_product_infiniteL_imp_infinite: " infinite A; B  {}   infinite (A × B)"
by (blast dest: finite_cartesian_productD1)

lemma cartesian_product_infiniteR_imp_infinite: " infinite B; A  {}   infinite (A × B)"
by (blast dest: finite_cartesian_productD2)

lemma finite_nat_iff_bounded2: "
  finite S = ((k::nat).nS. n < k)"
by (simp only: finite_nat_iff_bounded, blast)

lemma finite_nat_iff_bounded_le2: "
  finite S = ((k::nat).nS. n  k)"
by (simp only: finite_nat_iff_bounded_le, blast)

lemma nat_asc_chain_imp_unbounded: "
   S  {}; (mS. nS. m < (n::nat))   m. nS. m  n"
apply (rule allI)
apply (induct_tac m)
 apply blast
apply (erule bexE)
apply (rename_tac n1)
apply (erule_tac x=n1 in ballE)
  prefer 2
  apply simp
apply (clarify, rename_tac x, rule_tac x=x in bexI)
apply simp_all
done

lemma infinite_nat_iff_asc_chain: "
  S  {}  infinite S = (mS. nS. m < (n::nat))"
by (metis Max_in infinite_nat_iff_unbounded not_greater_Max)

lemma infinite_imp_asc_chain: "infinite S  mS. nS. m < (n::nat)"
by (rule infinite_nat_iff_asc_chain[THEN iffD1, OF infinite_imp_nonempty])


lemma infinite_image_imp_infinite: "infinite (f ` A)  infinite A"
by fastforce

lemma inj_on_imp_infinite_image: " infinite A; inj_on f A   infinite (f ` A)"
apply (frule card_image)
apply (fastforce simp: card_eq_0_iff)
done

lemma inj_on_infinite_image_iff: "inj_on f A  infinite (f ` A) = infinite A"
apply (rule iffI)
 apply (rule ccontr, simp)
apply (rule inj_on_imp_infinite_image, assumption+)
done

lemma inj_on_finite_image_iff: "inj_on f A  finite (f ` A) = finite A"
by (drule inj_on_infinite_image_iff, simp)

lemma nat_ex_greater_finite_Max_conv: "
  A  {}  (xA. (n::nat) < x) = (finite A  n < Max A)"
apply (rule iffI)
 apply (blast intro: order_less_le_trans Max_ge)
apply (case_tac "finite A")
 apply (blast intro: Max_in)
apply (drule infinite_nat_iff_unbounded[THEN iffD1, rule_format, of _ n])
apply blast
done

corollary nat_ex_greater_infinite_finite_Max_conv': "
  (xA. (n::nat) < x) = (finite A  A  {}  n < Max A  infinite A)"
apply (case_tac "A = {}", blast)
apply (drule nat_ex_greater_finite_Max_conv[of _ n])
apply blast
done


subsubsection ‹Some auxiliary results for disjoint sets›

lemma disjoint_iff_in_not_in1: "(A  B = {}) = (xA. x  B)" by blast
lemma disjoint_iff_in_not_in2: "(A  B = {}) = (xB. x  A)" by blast

lemma disjoint_in_Un: "
   A  B = {}; x  A  B   x  A  x  B"
by (blast intro: disjoint_iff_in_not_in1[THEN iffD1])+


lemma partition_Union: "A  C  (cC. A  c) = A" by blast

lemma disjoint_partition_Int: "
  c1C. c2C. c1  c2  c1  c2 = {} 
  a1{A  c| c. c  C}. a2{A  c| c. c  C}.
    a1  a2  a1  a2 = {}"
by blast

lemma "{f x |x. x  A} = (xA. {f x})"
by fastforce

text ‹This lemma version drops the superfluous precondition @{term "finite (C)"}
  (and turns the resulting equation to the sensible order card .. = k * card ..›).›
lemma card_partition: "
   finite C; c. c  C  card c = k; c1 c2. c1  C; c2  C; c1  c2  c1  c2 = {}  
  card (C) = k * card C"
by (metis card.infinite card_partition finite_Union mult_eq_if)



subsubsection ‹Some auxiliary results for subset relation›

lemma subset_image_Int: "A  B  f ` (A  B) = f ` A  f ` B"
by (simp only: Int_absorb2 image_mono)

lemma image_diff_disjoint_image_Int: "
   f ` (A - B)  f ` B = {}  
  f ` (A  B) = f ` A  f ` B"
apply (rule set_eqI)
apply (simp add: image_iff)
apply blast
done

lemma subset_imp_Int_subset1: "A  C  A  B  C"
by (rule subset_trans[of _ "C  B", OF Int_mono, OF _ subset_refl Int_lower1])

lemma subset_imp_Int_subset2: "B  C  A  B  C"
by (simp only: Int_commute[of A], rule subset_imp_Int_subset1)


subsubsection ‹Auxiliary results for intervals from SetInterval›

lemmas set_interval_defs =
  lessThan_def atMost_def
  greaterThan_def atLeast_def
  greaterThanLessThan_def atLeastLessThan_def
  greaterThanAtMost_def atLeastAtMost_def

lemma image_add_atLeast:
  "(λn::nat. n+k) ` {i..} = {i+k..}" (is "?A = ?B")
proof
  show "?A  ?B" by fastforce
next
  show "?B  ?A"
  proof
    fix n assume a: "n : ?B"
    hence "n - k  {i..}" by simp
    moreover have "n = (n - k) + k" using a by fastforce
    ultimately show "n  ?A" by blast
  qed
qed

lemma image_add_atMost:
  "(λn::nat. n+k) ` {..i} = {k..i+k}" (is "?A = ?B")
  
proof -
  have s1: "{..i} = {0..i}"
    by (simp add: set_interval_defs)
  then show "?A = ?B"
    by simp
qed

corollary image_Suc_atLeast: "Suc ` {i..} = {Suc i..}"
by (insert image_add_atLeast[of "Suc 0"], simp)

corollary image_Suc_atMost: "Suc ` {..i} = {Suc 0..Suc i}"
by (insert image_add_atMost[of "Suc 0"], simp)

lemmas image_add_lemmas =
  image_add_atLeastAtMost
  image_add_atLeast
  image_add_atMost
lemmas image_Suc_lemmas =
  image_Suc_atLeastAtMost
  image_Suc_atLeast
  image_Suc_atMost

lemma atMost_atLeastAtMost_0_conv: "{..i::nat} = {0..i}"
by (simp add: set_interval_defs)

lemma atLeastAtMost_subset_atMost: "(k::'a::order)  k'  {l..k}  {..k'}"
by (simp)

lemma lessThan_insert: "insert (n::'a::order) {..<n} = {..n}"
apply (rule set_eqI)
apply (clarsimp simp add: order_le_less)
apply blast
done

lemma greaterThan_insert: "insert (n::'a::order) {n<..} = {n..}"
apply (rule set_eqI)
apply (clarsimp simp add: order_le_less)
apply blast
done

lemma atMost_remove: "{..n} - {(n::'a::order)} = {..<n}"
apply (simp only: lessThan_insert[symmetric])
apply (rule Diff_insert_absorb)
apply simp
done

lemma atLeast_remove: "{n..} - {(n::'a::order)} = {n<..}"
apply (simp only: greaterThan_insert[symmetric])
apply (rule Diff_insert_absorb)
apply simp
done


lemma atMost_lessThan_conv: "{..n} = {..<Suc n}"
by (simp only: atMost_def lessThan_def less_Suc_eq_le)

lemma atLeastAtMost_atLeastLessThan_conv: "{l..u} = {l..<Suc u}"
by (simp only: atLeastAtMost_def atLeastLessThan_def atMost_lessThan_conv)

lemma atLeast_greaterThan_conv: "{Suc n..} = {n<..}"
by (simp only: atLeast_def greaterThan_def Suc_le_eq)

lemma atLeastAtMost_greaterThanAtMost_conv: "{Suc l..u} = {l<..u}"
by (simp only: greaterThanAtMost_def atLeastAtMost_def atLeast_greaterThan_conv)



lemma finite_subset_atLeastAtMost: "finite A  A  {Min A..Max A}"
by (simp add: subset_eq)

lemma Max_le_imp_subset_atMost: "
   finite A;  Max A  n   A  {..n}"
by (rule subset_trans[OF finite_subset_atLeastAtMost atLeastAtMost_subset_atMost])

lemma subset_atMost_imp_Max_le:"
   finite A; A  {}; A  {..n}   Max A  n"
by (simp add: subset_iff)

lemma subset_atMost_Max_le_conv: "
   finite A; A  {}   (A  {..n}) = (Max A  n)"
apply (rule iffI)
 apply (blast intro: subset_atMost_imp_Max_le)
apply (rule Max_le_imp_subset_atMost, assumption+)
done


lemma iMin_atLeast: "iMin {n..} = n"
by (rule iMin_equality, simp_all)

lemma iMin_greaterThan: "iMin {n<..} = Suc n"
by (simp only: atLeast_Suc_greaterThan[symmetric] iMin_atLeast)

lemma iMin_atMost: "iMin {..(n::nat)} = 0"
by (rule iMin_equality, simp_all)

lemma iMin_lessThan: "0 < n  iMin {..<(n::nat)} = 0"
by (rule iMin_equality, simp_all)

lemma Max_atMost: "Max {..(n::nat)} = n"
by (rule Max_equality[OF _ finite_atMost], simp_all)

lemma Max_lessThan: "0 < n  Max {..<n} = n - Suc 0"
by (rule Max_equality[OF _ finite_lessThan], simp_all)

lemma iMin_atLeastLessThan: "m < n  iMin {m..<n} = m"
by (rule iMin_equality, simp_all)

lemma Max_atLeastLessThan: "m < n  Max {m..<n} = n - Suc 0"
by (rule Max_equality[OF _ finite_atLeastLessThan], simp_all add: less_imp_le_pred)

lemma iMin_greaterThanLessThan: "Suc m < n  iMin {m<..<n} = Suc m"
by (simp only: atLeastSucLessThan_greaterThanLessThan[symmetric] iMin_atLeastLessThan)

lemma Max_greaterThanLessThan: "Suc m < n  Max {m<..<n} = n - Suc 0"
by (simp only: atLeastSucLessThan_greaterThanLessThan[symmetric] Max_atLeastLessThan)

lemma iMin_greaterThanAtMost: "m < n  iMin {m<..n} = Suc m"
by (simp only: atLeastSucAtMost_greaterThanAtMost[symmetric] atLeastLessThanSuc_atLeastAtMost[symmetric] iMin_atLeastLessThan)

lemma Max_greaterThanAtMost: "m < n  Max {m<..(n::nat)} = n"
by (simp add: atLeastSucAtMost_greaterThanAtMost[symmetric] atLeastLessThanSuc_atLeastAtMost[symmetric] Max_atLeastLessThan)

lemma iMin_atLeastAtMost: "m  n  iMin {m..n} = m"
by (rule iMin_equality, simp_all)

lemma Max_atLeastAtMost: "m  n  Max {m..(n::nat)} = n"
by (rule Max_equality[OF _ finite_atLeastAtMost], simp_all)

lemma infinite_atLeast: "infinite {(n::nat)..}"
by (rule unbounded_k_infinite[of n], fastforce)

lemma infinite_greaterThan: "infinite {(n::nat)<..}"
by (simp add: atLeast_Suc_greaterThan[symmetric] infinite_atLeast)

lemma infinite_atLeast_int: "infinite {(n::int)..}"
apply (rule_tac f="λx. nat (x - n)" in inj_on_infinite_image_iff[THEN iffD1, rule_format])
 apply (fastforce simp: inj_on_def)
apply (rule_tac t="((λx. nat (x - n)) ` {n..})" and s="{0..}" in subst)
 apply (simp add: set_eq_iff image_iff Bex_def)
 apply (clarify, rename_tac n1)
 apply (rule_tac x="n + int n1" in exI)
apply simp_all
done

lemma infinite_greaterThan_int: "infinite {(n::int)<..}"
apply (simp only: atLeast_remove[symmetric])
apply (rule Diff_infinite_finite[OF singleton_finite])
apply (rule infinite_atLeast_int)
done

lemma infinite_atMost_int: "infinite {..(n::int)}"
apply (rule_tac f="λx. n - x" in inj_on_infinite_image_iff[THEN iffD1, rule_format])
 apply (simp add: inj_on_def)
apply (rule_tac t="((-) n ` {..n})" and s="{0..}" in subst)
 apply (simp add: set_eq_iff image_iff Bex_def)
apply (rule infinite_atLeast_int)
done

lemma infinite_lessThan_int: "infinite {..<(n::int)}"
apply (simp only: atMost_remove[symmetric])
apply (rule Diff_infinite_finite[OF singleton_finite])
apply (rule infinite_atMost_int)
done


subsubsection ‹Auxiliary results for @{term card}

lemma sum_singleton: "(x{a}. f x) = f a"
by simp

lemma card_singleton: "card {a} = Suc 0"
by simp

lemma card_cartesian_product_singleton_right: "card (A × {x}) = card A"
by (simp add: card_cartesian_product)

lemma card_1_imp_singleton: "card A = Suc 0  (a. A = {a})"
by (metis card_eq_SucD)

lemma card_1_singleton_conv: "(card A = Suc 0) = (a. A = {a})"
apply (rule iffI)
apply (simp add: card_1_imp_singleton)
apply fastforce
done

lemma card_gr0_imp_finite: "0 < card A  finite A"
by (rule ccontr, simp)
lemma card_gr0_imp_not_empty: "(0 < card A)  A  {}"
by (rule ccontr, simp)
lemma not_empty_card_gr0_conv: "finite A  (A  {}) = (0 < card A)"
by fastforce

lemma nat_card_le_Max: "card (A::nat set)  Suc (Max A)"
apply (case_tac "finite A")
 prefer 2
 apply simp
apply (cut_tac card_mono[OF finite_atMost, of A "Max A"])
 apply simp
apply fastforce
done

lemma Int_card1: "finite A  card (A  B)  card A"
by (rule card_mono, simp_all)
lemma Int_card2: "finite B  card (A  B)  card B"
by (simp only: Int_commute[of A], rule Int_card1)
lemma Un_card1: " finite A; finite B   card A  card (A  B)"
by (rule card_mono, simp_all)
lemma Un_card2: " finite A; finite B   card B  card (A  B)"
by (simp only: Un_commute[of A], rule Un_card1)

lemma card_Un_conv: "
   finite A; finite B  
  card (A  B) = card A + card B - card (A  B)"
by (simp only: card_Un_Int diff_add_inverse2)
lemma card_Int_conv: "
   finite A; finite B  
  card (A  B) = card A + card B - card (A  B)"
by (simp only: card_Un_Int diff_add_inverse)



text ‹Pigeonhole principle, dirichlet's box principle›
lemma pigeonhole_principle[rule_format]: "
  card (f ` A) < card A  (xA. yA. x  y  f x = f y)"
apply (case_tac "finite A")
 prefer 2
 apply simp
apply (rule finite.induct[of A])
apply simp_all
apply (clarsimp, rename_tac A1 a)
apply (case_tac "a  A1", force simp: insert_absorb)
apply (case_tac "f a  f ` A1", fastforce+)
done

corollary pigeonhole_principle_linorder[rule_format]: "
  card (f ` A) < card (A::'a::linorder set)  (xA. yA. x < y  f x = f y)"
apply (drule pigeonhole_principle, clarify)
apply (drule neq_iff[THEN iffD1])
apply fastforce
done

corollary pigeonhole_mod: "
   0 < m; m < card A   xA. yA. x < y  x mod m = y mod m"
apply (rule pigeonhole_principle_linorder)
apply (rule le_less_trans[of _ "card {..<m}"])
apply (rule card_mono)
apply fastforce+
done

corollary pigeonhole_mod2: "
   (0::nat) < m; m  c; inj_on f {..c}   xc. yc. x < y  f x mod m = f y mod m"
apply (insert pigeonhole_mod[of m "f ` {..c}"])
apply (clarsimp simp add: card_image, rename_tac x y)
apply (subgoal_tac "x  y")
 prefer 2
 apply blast
apply (drule neq_iff[THEN iffD1], safe)
 apply blast
apply (blast intro: eq_commute[THEN iffD1])
done

end