Quelle Finite_Set.thy Sprache: Isabelle

(*  Title:      HOL/Finite_Set.thy
    Author:     Tobias Nipkow
    Author:     Lawrence C Paulson
    Author:     Markus Wenzel
    Author:     Jeremy Avigad
    Author:     Andrei Popescu
*)

section \<open>Finite sets\<close>

theory Finite_Set
  imports Product_Type Sum_Type Fields Relation
begin

subsection \<open>Predicate for finite sets\<close>

context notes [[inductive_internals]]
begin

inductive finite :: "'a set \ bool"
  where
    emptyI [simp, intro!]: "finite {}"
  | insertI [simp, intro!]: "finite A \ finite (insert a A)"

end

simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.proc\<close>

declare [[simproc del: finite_Collect]]

lemma finite_induct [case_names empty insert, induct set: finite]:
  \<comment> \<open>Discharging \<open>x \<notin> F\<close> entails extra work.\<close>
  assumes "finite F"
  assumes "P {}"
    and insert: "\x F. finite F \ x \ F \ P F \ P (insert x F)"
  shows "P F"
  using \<open>finite F\<close>
proof induct
  show "P {}" by fact
next
  fix x F
  assume F: "finite F" and P: "P F"
  show "P (insert x F)"
  proof cases
    assume "x \ F"
    then have "insert x F = F" by (rule insert_absorb)
    with P show ?thesis by (simp only:)
  next
    assume "x \ F"
    from F this P show ?thesis by (rule insert)
  qed
qed

lemma infinite_finite_induct [case_names infinite empty insert]:
  assumes infinite: "\A. \ finite A \ P A"
    and empty: "P {}"
    and insert: "\x F. finite F \ x \ F \ P F \ P (insert x F)"
  shows "P A"
proof (cases "finite A")
  case False
  with infinite show ?thesis .
next
  case True
  then show ?thesis by (induct A) (fact empty insert)+
qed

subsubsection \<open>Choice principles\<close>

lemma ex_new_if_finite: \<comment> \<open>does not depend on def of finite at all\<close>
  assumes "\ finite (UNIV :: 'a set)" and "finite A"
  shows "\a::'a. a \ A"
proof -
  from assms have "A \ UNIV" by blast
  then show ?thesis by blast
qed

text \<open>A finite choice principle. Does not need the SOME choice operator.\<close>

lemma finite_set_choice: "finite A \ \x\A. \y. P x y \ \f. \x\A. P x (f x)"
proof (induct rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert a A)
  then obtain f b where f: "\x\A. P x (f x)" and ab: "P a b"
    by auto
  show ?case (is "\f. ?P f")
  proof
    show "?P (\x. if x = a then b else f x)"
      using f ab by auto
  qed
qed

subsubsection \<open>Finite sets are the images of initial segments of natural numbers\<close>

lemma finite_imp_nat_seg_image_inj_on:
  assumes "finite A"
  shows "\(n::nat) f. A = f ` {i. i < n} \ inj_on f {i. i < n}"
  using assms
proof induct
  case empty
  show ?case
  proof
    show "\f. {} = f ` {i::nat. i < 0} \ inj_on f {i. i < 0}"
      by simp
  qed
next
  case (insert a A)
  have notinA: "a \ A" by fact
  from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}"
    by blast
  then have "insert a A = f(n:=a) ` {i. i < Suc n}" and "inj_on (f(n:=a)) {i. i < Suc n}"
    using notinA by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
  then show ?case by blast
qed

lemma nat_seg_image_imp_finite: "A = f ` {i::nat. i < n} \ finite A"
proof (induct n arbitrary: A)
  case 0
  then show ?case by simp
next
  case (Suc n)
  let ?B = "f ` {i. i < n}"
  have finB: "finite ?B" by (rule Suc.hyps[OF refl])
  show ?case
  proof (cases "\k
    case True
    then have "A = ?B"
      using Suc.prems by (auto simp:less_Suc_eq)
    then show ?thesis
      using finB by simp
  next
    case False
    then have "A = insert (f n) ?B"
      using Suc.prems by (auto simp:less_Suc_eq)
    then show ?thesis using finB by simp
  qed
qed

lemma finite_conv_nat_seg_image: "finite A \ (\n f. A = f ` {i::nat. i < n})"
  by (blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)

lemma finite_imp_inj_to_nat_seg:
  assumes "finite A"
  shows "\f n. f ` A = {i::nat. i < n} \ inj_on f A"
proof -
  from finite_imp_nat_seg_image_inj_on [OF \<open>finite A\<close>]
  obtain f and n :: nat where bij: "bij_betw f {i. i
    by (auto simp: bij_betw_def)
  let ?f = "the_inv_into {i. i
  have "inj_on ?f A \ ?f ` A = {i. i
    by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij])
  then show ?thesis by blast
qed

lemma finite_Collect_less_nat [iff]: "finite {n::nat. n < k}"
  by (fastforce simp: finite_conv_nat_seg_image)

lemma finite_Collect_le_nat [iff]: "finite {n::nat. n \ k}"
  by (simp add: le_eq_less_or_eq Collect_disj_eq)

subsection \<open>Finiteness and common set operations\<close>

lemma rev_finite_subset: "finite B \ A \ B \ finite A"
proof (induct arbitrary: A rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert x F A)
  have A: "A \ insert x F" and r: "A - {x} \ F \ finite (A - {x})"
    by fact+
  show "finite A"
  proof cases
    assume x: "x \ A"
    with A have "A - {x} \ F" by (simp add: subset_insert_iff)
    with r have "finite (A - {x})" .
    then have "finite (insert x (A - {x}))" ..
    also have "insert x (A - {x}) = A"
      using x by (rule insert_Diff)
    finally show ?thesis .
  next
    show ?thesis when "A \ F"
      using that by fact
    assume "x \ A"
    with A show "A \ F"
      by (simp add: subset_insert_iff)
  qed
qed

lemma finite_subset: "A \ B \ finite B \ finite A"
  by (rule rev_finite_subset)

simproc_setup finite ("finite A") = \<open>
let
  val finite_subset = @{thm finite_subset}
  val Eq_TrueI = @{thm Eq_TrueI}

  fun is_subset A th = case Thm.prop_of th of
        (_ $ \<^Const_>\<open>less_eq \<^Type>\<open>set _\<close> for A' B\<close>)
        => if A aconv A' then SOME(B,th) else NONE
      | _ => NONE;

  fun is_finite th = case Thm.prop_of th of
        (_ $ \<^Const_>\<open>finite _ for A\<close>) => SOME(A,th)
      |  _ => NONE;

  fun comb (A,sub_th) (A',fin_th) ths = if A aconv A' then (sub_th,fin_th) :: ths else ths

  fun proc ctxt ct =
    (let
       val _ $ A = Thm.term_of ct
       val prems = Simplifier.prems_of ctxt
       val fins = map_filter is_finite prems
       val subsets = map_filter (is_subset A) prems
     in case fold_product comb subsets fins [] of
          (sub_th,fin_th) :: _ => SOME((fin_th RS (sub_th RS finite_subset)) RS Eq_TrueI)
        | _ => NONE
     end)
in K proc end
\<close>

(* Needs to be used with care *)
declare [[simproc del: finite]]

lemma finite_UnI:
  assumes "finite F" and "finite G"
  shows "finite (F \ G)"
  using assms by induct simp_all

lemma finite_Un [iff]: "finite (F \ G) \ finite F \ finite G"
  by (blast intro: finite_UnI finite_subset [of _ "F \ G"])

lemma finite_insert [simp]: "finite (insert a A) \ finite A"
proof -
  have "finite {a} \ finite A \ finite A" by simp
  then have "finite ({a} \ A) \ finite A" by (simp only: finite_Un)
  then show ?thesis by simp
qed

lemma finite_Int [simp, intro]: "finite F \ finite G \ finite (F \ G)"
  by (blast intro: finite_subset)

lemma finite_Collect_conjI [simp, intro]:
  "finite {x. P x} \ finite {x. Q x} \ finite {x. P x \ Q x}"
  by (simp add: Collect_conj_eq)

lemma finite_Collect_disjI [simp]:
  "finite {x. P x \ Q x} \ finite {x. P x} \ finite {x. Q x}"
  by (simp add: Collect_disj_eq)

lemma finite_Diff [simp, intro]: "finite A \ finite (A - B)"
  by (rule finite_subset, rule Diff_subset)

lemma finite_Diff2 [simp]:
  assumes "finite B"
  shows "finite (A - B) \ finite A"
proof -
  have "finite A \ finite ((A - B) \ (A \ B))"
    by (simp add: Un_Diff_Int)
  also have "\ \ finite (A - B)"
    using \<open>finite B\<close> by simp
  finally show ?thesis ..
qed

lemma finite_Diff_insert [iff]: "finite (A - insert a B) \ finite (A - B)"
proof -
  have "finite (A - B) \ finite (A - B - {a})" by simp
  moreover have "A - insert a B = A - B - {a}" by auto
  ultimately show ?thesis by simp
qed

lemma finite_compl [simp]:
  "finite (A :: 'a set) \ finite (- A) \ finite (UNIV :: 'a set)"
  by (simp add: Compl_eq_Diff_UNIV)

lemma finite_Collect_not [simp]:
  "finite {x :: 'a. P x} \ finite {x. \ P x} \ finite (UNIV :: 'a set)"
  by (simp add: Collect_neg_eq)

lemma finite_Union [simp, intro]:
  "finite A \ (\M. M \ A \ finite M) \ finite (\A)"
  by (induct rule: finite_induct) simp_all

lemma finite_UN_I [intro]:
  "finite A \ (\a. a \ A \ finite (B a)) \ finite (\a\A. B a)"
  by (induct rule: finite_induct) simp_all

lemma finite_UN [simp]: "finite A \ finite (\(B ` A)) \ (\x\A. finite (B x))"
  by (blast intro: finite_subset)

lemma finite_Inter [intro]: "\A\M. finite A \ finite (\M)"
  by (blast intro: Inter_lower finite_subset)

lemma finite_INT [intro]: "\x\I. finite (A x) \ finite (\x\I. A x)"
  by (blast intro: INT_lower finite_subset)

lemma finite_imageI [simp, intro]: "finite F \ finite (h ` F)"
  by (induct rule: finite_induct) simp_all

lemma finite_image_set [simp]: "finite {x. P x} \ finite {f x |x. P x}"
  by (simp add: image_Collect [symmetric])

lemma finite_image_set2:
  "finite {x. P x} \ finite {y. Q y} \ finite {f x y |x y. P x \ Q y}"
  by (rule finite_subset [where B = "\x \ {x. P x}. \y \ {y. Q y}. {f x y}"]) auto

lemma finite_imageD:
  assumes "finite (f ` A)" and "inj_on f A"
  shows "finite A"
  using assms
proof (induct "f ` A" arbitrary: A)
  case empty
  then show ?case by simp
next
  case (insert x B)
  then have B_A: "insert x B = f ` A"
    by simp
  then obtain y where "x = f y" and "y \ A"
    by blast
  from B_A \<open>x \<notin> B\<close> have "B = f ` A - {x}"
    by blast
  with B_A \<open>x \<notin> B\<close> \<open>x = f y\<close> \<open>inj_on f A\<close> \<open>y \<in> A\<close> have "B = f ` (A - {y})"
    by (simp add: inj_on_image_set_diff)
  moreover from \<open>inj_on f A\<close> have "inj_on f (A - {y})"
    by (rule inj_on_diff)
  ultimately have "finite (A - {y})"
    by (rule insert.hyps)
  then show "finite A"
    by simp
qed

lemma finite_image_iff: "inj_on f A \ finite (f ` A) \ finite A"
  using finite_imageD by blast

lemma finite_surj: "finite A \ B \ f ` A \ finite B"
  by (erule finite_subset) (rule finite_imageI)

lemma finite_range_imageI: "finite (range g) \ finite (range (\x. f (g x)))"
  by (drule finite_imageI) (simp add: range_composition)

lemma finite_subset_image:
  assumes "finite B"
  shows "B \ f ` A \ \C\A. finite C \ B = f ` C"
  using assms
proof induct
  case empty
  then show ?case by simp
next
  case insert
  then show ?case
    by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast
qed

lemma all_subset_image: "(\B. B \ f ` A \ P B) \ (\B. B \ A \ P(f ` B))"
  by (safe elim!: subset_imageE) (use image_mono in \<open>blast+\<close>) (* slow *)

lemma all_finite_subset_image:
  "(\B. finite B \ B \ f ` A \ P B) \ (\B. finite B \ B \ A \ P (f ` B))"
proof safe
  fix B :: "'a set"
  assume B: "finite B" "B \ f ` A" and P: "\B. finite B \ B \ A \ P (f ` B)"
  show "P B"
    using finite_subset_image [OF B] P by blast
qed blast

lemma ex_finite_subset_image:
  "(\B. finite B \ B \ f ` A \ P B) \ (\B. finite B \ B \ A \ P (f ` B))"
proof safe
  fix B :: "'a set"
  assume B: "finite B" "B \ f ` A" and "P B"
  show "\B. finite B \ B \ A \ P (f ` B)"
    using finite_subset_image [OF B] \<open>P B\<close> by blast
qed blast

lemma finite_vimage_IntI: "finite F \ inj_on h A \ finite (h -` F \ A)"
proof (induct rule: finite_induct)
  case (insert x F)
  then show ?case
    by (simp add: vimage_insert [of h x F] finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
qed simp

lemma finite_finite_vimage_IntI:
  assumes "finite F"
    and "\y. y \ F \ finite ((h -` {y}) \ A)"
  shows "finite (h -` F \ A)"
proof -
  have *: "h -` F \ A = (\ y\F. (h -` {y}) \ A)"
    by blast
  show ?thesis
    by (simp only: * assms finite_UN_I)
qed

lemma finite_vimageI: "finite F \ inj h \ finite (h -` F)"
  using finite_vimage_IntI[of F h UNIV] by auto

lemma finite_vimageD': "finite (f -` A) \ A \ range f \ finite A"
  by (auto simp add: subset_image_iff intro: finite_subset[rotated])

lemma finite_vimageD: "finite (h -` F) \ surj h \ finite F"
  by (auto dest: finite_vimageD')

lemma finite_vimage_iff: "bij h \ finite (h -` F) \ finite F"
  unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)

lemma finite_inverse_image_gen:
  assumes "finite A" "inj_on f D"
  shows "finite {j\D. f j \ A}"
  using finite_vimage_IntI [OF assms]
  by (simp add: Collect_conj_eq inf_commute vimage_def)

lemma finite_inverse_image:
  assumes "finite A" "inj f"
  shows "finite {j. f j \ A}"
  using finite_inverse_image_gen [OF assms] by simp

lemma finite_Collect_bex [simp]:
  assumes "finite A"
  shows "finite {x. \y\A. Q x y} \ (\y\A. finite {x. Q x y})"
proof -
  have "{x. \y\A. Q x y} = (\y\A. {x. Q x y})" by auto
  with assms show ?thesis by simp
qed

lemma finite_Collect_bounded_ex [simp]:
  assumes "finite {y. P y}"
  shows "finite {x. \y. P y \ Q x y} \ (\y. P y \ finite {x. Q x y})"
proof -
  have "{x. \y. P y \ Q x y} = (\y\{y. P y}. {x. Q x y})"
    by auto
  with assms show ?thesis
    by simp
qed

lemma finite_Plus: "finite A \ finite B \ finite (A <+> B)"
  by (simp add: Plus_def)

lemma finite_PlusD:
  fixes A :: "'a set" and B :: "'b set"
  assumes fin: "finite (A <+> B)"
  shows "finite A" "finite B"
proof -
  have "Inl ` A \ A <+> B"
    by auto
  then have "finite (Inl ` A :: ('a + 'b) set)"
    using fin by (rule finite_subset)
  then show "finite A"
    by (rule finite_imageD) (auto intro: inj_onI)
next
  have "Inr ` B \ A <+> B"
    by auto
  then have "finite (Inr ` B :: ('a + 'b) set)"
    using fin by (rule finite_subset)
  then show "finite B"
    by (rule finite_imageD) (auto intro: inj_onI)
qed

lemma finite_Plus_iff [simp]: "finite (A <+> B) \ finite A \ finite B"
  by (auto intro: finite_PlusD finite_Plus)

lemma finite_Plus_UNIV_iff [simp]:
  "finite (UNIV :: ('a + 'b) set) \ finite (UNIV :: 'a set) \ finite (UNIV :: 'b set)"
  by (subst UNIV_Plus_UNIV [symmetric]) (rule finite_Plus_iff)

lemma finite_SigmaI [simp, intro]:
  "finite A \ (\a. a\A \ finite (B a)) \ finite (SIGMA a:A. B a)"
  unfolding Sigma_def by blast

lemma finite_SigmaI2:
  assumes "finite {x\A. B x \ {}}"
  and "\a. a \ A \ finite (B a)"
  shows "finite (Sigma A B)"
proof -
  from assms have "finite (Sigma {x\A. B x \ {}} B)"
    by auto
  also have "Sigma {x:A. B x \ {}} B = Sigma A B"
    by auto
  finally show ?thesis .
qed

lemma finite_cartesian_product: "finite A \ finite B \ finite (A \ B)"
  by (rule finite_SigmaI)

lemma finite_Prod_UNIV:
  "finite (UNIV :: 'a set) \ finite (UNIV :: 'b set) \ finite (UNIV :: ('a \ 'b) set)"
  by (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product)

lemma finite_cartesian_productD1:
  assumes "finite (A \ B)" and "B \ {}"
  shows "finite A"
proof -
  from assms obtain n f where "A \ B = f ` {i::nat. i < n}"
    by (auto simp add: finite_conv_nat_seg_image)
  then have "fst ` (A \ B) = fst ` f ` {i::nat. i < n}"
    by simp
  with \<open>B \<noteq> {}\<close> have "A = (fst \<circ> f) ` {i::nat. i < n}"
    by (simp add: image_comp)
  then have "\n f. A = f ` {i::nat. i < n}"
    by blast
  then show ?thesis
    by (auto simp add: finite_conv_nat_seg_image)
qed

lemma finite_cartesian_productD2:
  assumes "finite (A \ B)" and "A \ {}"
  shows "finite B"
proof -
  from assms obtain n f where "A \ B = f ` {i::nat. i < n}"
    by (auto simp add: finite_conv_nat_seg_image)
  then have "snd ` (A \ B) = snd ` f ` {i::nat. i < n}"
    by simp
  with \<open>A \<noteq> {}\<close> have "B = (snd \<circ> f) ` {i::nat. i < n}"
    by (simp add: image_comp)
  then have "\n f. B = f ` {i::nat. i < n}"
    by blast
  then show ?thesis
    by (auto simp add: finite_conv_nat_seg_image)
qed

lemma finite_cartesian_product_iff:
  "finite (A \ B) \ (A = {} \ B = {} \ (finite A \ finite B))"
  by (auto dest: finite_cartesian_productD1 finite_cartesian_productD2 finite_cartesian_product)

lemma finite_prod:
  "finite (UNIV :: ('a \ 'b) set) \ finite (UNIV :: 'a set) \ finite (UNIV :: 'b set)"
  using finite_cartesian_product_iff[of UNIV UNIV] by simp

lemma finite_Pow_iff [iff]: "finite (Pow A) \ finite A"
proof
  assume "finite (Pow A)"
  then have "finite ((\x. {x}) ` A)"
    by (blast intro: finite_subset)  (* somewhat slow *)
  then show "finite A"
    by (rule finite_imageD [unfolded inj_on_def]) simp
next
  assume "finite A"
  then show "finite (Pow A)"
    by induct (simp_all add: Pow_insert)
qed

corollary finite_Collect_subsets [simp, intro]: "finite A \ finite {B. B \ A}"
  by (simp add: Pow_def [symmetric])

lemma finite_set: "finite (UNIV :: 'a set set) \ finite (UNIV :: 'a set)"
  by (simp only: finite_Pow_iff Pow_UNIV[symmetric])

lemma finite_UnionD: "finite (\A) \ finite A"
  by (blast intro: finite_subset [OF subset_Pow_Union])

lemma finite_bind:
  assumes "finite S"
  assumes "\x \ S. finite (f x)"
  shows "finite (Set.bind S f)"
using assms by (simp add: bind_UNION)

lemma finite_filter [simp]: "finite S \ finite (Set.filter P S)"
  by (simp add:)

lemma finite_set_of_finite_funs:
  assumes "finite A" "finite B"
  shows "finite {f. \x. (x \ A \ f x \ B) \ (x \ A \ f x = d)}" (is "finite ?S")
proof -
  let ?F = "\f. {(a,b). a \ A \ b = f a}"
  have "?F ` ?S \ Pow(A \ B)"
    by auto
  from finite_subset[OF this] assms have 1: "finite (?F ` ?S)"
    by simp
  have 2: "inj_on ?F ?S"
    by (fastforce simp add: inj_on_def set_eq_iff fun_eq_iff)  (* somewhat slow *)
  show ?thesis
    by (rule finite_imageD [OF 1 2])
qed

lemma not_finite_existsD:
  assumes "\ finite {a. P a}"
  shows "\a. P a"
proof (rule classical)
  assume "\ ?thesis"
  with assms show ?thesis by auto
qed

lemma finite_converse [iff]: "finite (r\) \ finite r"
  unfolding converse_def conversep_iff
  using [[simproc add: finite_Collect]]
  by (auto elim: finite_imageD simp: inj_on_def)

lemma finite_Domain: "finite r \ finite (Domain r)"
  by (induct set: finite) auto

lemma finite_Range: "finite r \ finite (Range r)"
  by (induct set: finite) auto

lemma finite_Field: "finite r \ finite (Field r)"
  by (simp add: Field_def finite_Domain finite_Range)

lemma finite_Image[simp]: "finite R \ finite (R `` A)"
  by(rule finite_subset[OF _ finite_Range]) auto

subsection \<open>Further induction rules on finite sets\<close>

lemma finite_ne_induct [case_names singleton insert, consumes 2]:
  assumes "finite F" and "F \ {}"
  assumes "\x. P {x}"
    and "\x F. finite F \ F \ {} \ x \ F \ P F \ P (insert x F)"
  shows "P F"
  using assms
proof induct
  case empty
  then show ?case by simp
next
  case (insert x F)
  then show ?case by cases auto
qed

lemma finite_subset_induct [consumes 2, case_names empty insert]:
  assumes "finite F" and "F \ A"
    and empty: "P {}"
    and insert: "\a F. finite F \ a \ A \ a \ F \ P F \ P (insert a F)"
  shows "P F"
  using \<open>finite F\<close> \<open>F \<subseteq> A\<close>
proof induct
  show "P {}" by fact
next
  fix x F
  assume "finite F" and "x \ F" and P: "F \ A \ P F" and i: "insert x F \ A"
  show "P (insert x F)"
  proof (rule insert)
    from i show "x \ A" by blast
    from i have "F \ A" by blast
    with P show "P F" .
    show "finite F" by fact
    show "x \ F" by fact
  qed
qed

lemma finite_empty_induct:
  assumes "finite A"
    and "P A"
    and remove: "\a A. finite A \ a \ A \ P A \ P (A - {a})"
  shows "P {}"
proof -
  have "P (A - B)" if "B \ A" for B :: "'a set"
  proof -
    from \<open>finite A\<close> that have "finite B"
      by (rule rev_finite_subset)
    from this \<open>B \<subseteq> A\<close> show "P (A - B)"
    proof induct
      case empty
      from \<open>P A\<close> show ?case by simp
    next
      case (insert b B)
      have "P (A - B - {b})"
      proof (rule remove)
        from \<open>finite A\<close> show "finite (A - B)"
          by induct auto
        from insert show "b \ A - B"
          by simp
        from insert show "P (A - B)"
          by simp
      qed
      also have "A - B - {b} = A - insert b B"
        by (rule Diff_insert [symmetric])
      finally show ?case .
    qed
  qed
  then have "P (A - A)" by blast
  then show ?thesis by simp
qed

lemma finite_update_induct [consumes 1, case_names const update]:
  assumes finite: "finite {a. f a \ c}"
    and const: "P (\a. c)"
    and update: "\a b f. finite {a. f a \ c} \ f a = c \ b \ c \ P f \ P (f(a := b))"
  shows "P f"
  using finite
proof (induct "{a. f a \ c}" arbitrary: f)
  case empty
  with const show ?case by simp
next
  case (insert a A)
  then have "A = {a'. (f(a := c)) a' \ c}" and "f a \ c"
    by auto
  with \<open>finite A\<close> have "finite {a'. (f(a := c)) a' \<noteq> c}"
    by simp
  have "(f(a := c)) a = c"
    by simp
  from insert \<open>A = {a'. (f(a := c)) a' \<noteq> c}\<close> have "P (f(a := c))"
    by simp
  with \<open>finite {a'. (f(a := c)) a' \<noteq> c}\<close> \<open>(f(a := c)) a = c\<close> \<open>f a \<noteq> c\<close>
  have "P ((f(a := c))(a := f a))"
    by (rule update)
  then show ?case by simp
qed

lemma finite_subset_induct' [consumes 2, case_names empty insert]:
  assumes "finite F" and "F \ A"
    and empty: "P {}"
    and insert: "\a F. \finite F; a \ A; F \ A; a \ F; P F \ \ P (insert a F)"
  shows "P F"
  using assms(1,2)
proof induct
  show "P {}" by fact
next
  fix x F
  assume "finite F" and "x \ F" and
    P: "F \ A \ P F" and i: "insert x F \ A"
  show "P (insert x F)"
  proof (rule insert)
    from i show "x \ A" by blast
    from i have "F \ A" by blast
    with P show "P F" .
    show "finite F" by fact
    show "x \ F" by fact
    show "F \ A" by fact
  qed
qed

subsection \<open>Class \<open>finite\<close>\<close>

class finite =
  assumes finite_UNIV: "finite (UNIV :: 'a set)"
begin

lemma finite [simp]: "finite (A :: 'a set)"
  by (rule subset_UNIV finite_UNIV finite_subset)+

lemma finite_code [code]: "finite (A :: 'a set) \ True"
  by simp

end

instance prod :: (finite, finite) finite
  by standard (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)

lemma inj_graph: "inj (\f. {(x, y). y = f x})"
  by (rule inj_onI) (auto simp add: set_eq_iff fun_eq_iff)

instance "fun" :: (finite, finite) finite
proof
  show "finite (UNIV :: ('a \ 'b) set)"
  proof (rule finite_imageD)
    let ?graph = "\f::'a \ 'b. {(x, y). y = f x}"
    have "range ?graph \ Pow UNIV"
      by simp
    moreover have "finite (Pow (UNIV :: ('a * 'b) set))"
      by (simp only: finite_Pow_iff finite)
    ultimately show "finite (range ?graph)"
      by (rule finite_subset)
    show "inj ?graph"
      by (rule inj_graph)
  qed
qed

instance bool :: finite
  by standard (simp add: UNIV_bool)

instance set :: (finite) finite
  by standard (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)

instance unit :: finite
  by standard (simp add: UNIV_unit)

instance sum :: (finite, finite) finite
  by standard (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)

subsection \<open>A basic fold functional for finite sets\<close>

text \<open>
  The intended behaviour is \<open>fold f z {x\<^sub>1, \<dots>, x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)\<close>
  if \<open>f\<close> is ``left-commutative''.
  The commutativity requirement is relativised to the carrier set \<open>S\<close>:
\<close>

locale comp_fun_commute_on =
  fixes S :: "'a set"
  fixes f :: "'a \ 'b \ 'b"
  assumes comp_fun_commute_on: "x \ S \ y \ S \ f y \ f x = f x \ f y"
begin

lemma fun_left_comm: "x \ S \ y \ S \ f y (f x z) = f x (f y z)"
  using comp_fun_commute_on by (simp add: fun_eq_iff)

lemma commute_left_comp: "x \ S \ y \ S \ f y \ (f x \ g) = f x \ (f y \ g)"
  by (simp add: o_assoc comp_fun_commute_on)

end

inductive fold_graph :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b \ bool"
  for f :: "'a \ 'b \ 'b" and z :: 'b
  where
    emptyI [intro]: "fold_graph f z {} z"
  | insertI [intro]: "x \ A \ fold_graph f z A y \ fold_graph f z (insert x A) (f x y)"

inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"

lemma fold_graph_closed_lemma:
  "fold_graph f z A x \ x \ B"
  if "fold_graph g z A x"
    "\a b. a \ A \ b \ B \ f a b = g a b"
    "\a b. a \ A \ b \ B \ g a b \ B"
    "z \ B"
  using that(1-3)
proof (induction rule: fold_graph.induct)
  case (insertI x A y)
  have "fold_graph f z A y" "y \ B"
    unfolding atomize_conj
    by (rule insertI.IH) (auto intro: insertI.prems)
  then have "g x y \ B" and f_eq: "f x y = g x y"
    by (auto simp: insertI.prems)
  moreover have "fold_graph f z (insert x A) (f x y)"
    by (rule fold_graph.insertI; fact)
  ultimately
  show ?case
    by (simp add: f_eq)
qed (auto intro!: that)

lemma fold_graph_closed_eq:
  "fold_graph f z A = fold_graph g z A"
  if "\a b. a \ A \ b \ B \ f a b = g a b"
     "\a b. a \ A \ b \ B \ g a b \ B"
     "z \ B"
  using fold_graph_closed_lemma[of f z A _ B g] fold_graph_closed_lemma[of g z A _ B f] that
  by auto

definition fold :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b"
  where "fold f z A = (if finite A then (THE y. fold_graph f z A y) else z)"

lemma fold_closed_eq: "fold f z A = fold g z A"
  if "\a b. a \ A \ b \ B \ f a b = g a b"
     "\a b. a \ A \ b \ B \ g a b \ B"
     "z \ B"
  unfolding Finite_Set.fold_def
  by (subst fold_graph_closed_eq[where B=B and g=g]) (auto simp: that)

text \<open>
  A tempting alternative for the definition is
  \<^term>\<open>if finite A then THE y. fold_graph f z A y else e\<close>.
  It allows the removal of finiteness assumptions from the theorems
  \<open>fold_comm\<close>, \<open>fold_reindex\<close> and \<open>fold_distrib\<close>.
  The proofs become ugly. It is not worth the effort. (???)
\<close>

lemma finite_imp_fold_graph: "finite A \ \x. fold_graph f z A x"
  by (induct rule: finite_induct) auto

subsubsection \<open>From \<^const>\<open>fold_graph\<close> to \<^term>\<open>fold\<close>\<close>

context comp_fun_commute_on
begin

lemma fold_graph_finite:
  assumes "fold_graph f z A y"
  shows "finite A"
  using assms by induct simp_all

lemma fold_graph_insertE_aux:
  assumes "A \ S"
  assumes "fold_graph f z A y" "a \ A"
  shows "\y'. y = f a y' \ fold_graph f z (A - {a}) y'"
  using assms(2-,1)
proof (induct set: fold_graph)
  case emptyI
  then show ?case by simp
next
  case (insertI x A y)
  show ?case
  proof (cases "x = a")
    case True
    with insertI show ?thesis by auto
  next
    case False
    then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'"
      using insertI by auto
    from insertI have "x \ S" "a \ S" by auto
    then have "f x y = f a (f x y')"
      unfolding y by (intro fun_left_comm; simp)
    moreover have "fold_graph f z (insert x A - {a}) (f x y')"
      using y' and \x \ a\ and \x \ A\
      by (simp add: insert_Diff_if fold_graph.insertI)
    ultimately show ?thesis
      by fast
  qed
qed

lemma fold_graph_insertE:
  assumes "insert x A \ S"
  assumes "fold_graph f z (insert x A) v" and "x \ A"
  obtains y where "v = f x y" and "fold_graph f z A y"
  using assms by (auto dest: fold_graph_insertE_aux[OF \<open>insert x A \<subseteq> S\<close> _ insertI1])

lemma fold_graph_determ:
  assumes "A \ S"
  assumes "fold_graph f z A x" "fold_graph f z A y"
  shows "y = x"
  using assms(2-,1)
proof (induct arbitrary: y set: fold_graph)
  case emptyI
  then show ?case by fast
next
  case (insertI x A y v)
  from \<open>insert x A \<subseteq> S\<close> and \<open>fold_graph f z (insert x A) v\<close> and \<open>x \<notin> A\<close>
  obtain y' where "v = f x y'" and "fold_graph f z A y'"
    by (rule fold_graph_insertE)
  from \<open>fold_graph f z A y'\<close> insertI have "y' = y"
    by simp
  with \<open>v = f x y'\<close> show "v = f x y"
    by simp
qed

lemma fold_equality: "A \ S \ fold_graph f z A y \ fold f z A = y"
  by (cases "finite A") (auto simp add: fold_def intro: fold_graph_determ dest: fold_graph_finite)

lemma fold_graph_fold:
  assumes "A \ S"
  assumes "finite A"
  shows "fold_graph f z A (fold f z A)"
proof -
  from \<open>finite A\<close> have "\<exists>x. fold_graph f z A x"
    by (rule finite_imp_fold_graph)
  moreover note fold_graph_determ[OF \<open>A \<subseteq> S\<close>]
  ultimately have "\!x. fold_graph f z A x"
    by (rule ex_ex1I)
  then have "fold_graph f z A (The (fold_graph f z A))"
    by (rule theI')
  with assms show ?thesis
    by (simp add: fold_def)
qed

text \<open>The base case for \<open>fold\<close>:\<close>

lemma (in -) fold_infinite [simp]: "\ finite A \ fold f z A = z"
  by (auto simp: fold_def)

lemma (in -) fold_empty [simp]: "fold f z {} = z"
  by (auto simp: fold_def)

text \<open>The various recursion equations for \<^const>\<open>fold\<close>:\<close>

lemma fold_insert [simp]:
  assumes "insert x A \ S"
  assumes "finite A" and "x \ A"
  shows "fold f z (insert x A) = f x (fold f z A)"
proof (rule fold_equality[OF \<open>insert x A \<subseteq> S\<close>])
  fix z
  from \<open>insert x A \<subseteq> S\<close> \<open>finite A\<close> have "fold_graph f z A (fold f z A)"
    by (blast intro: fold_graph_fold)
  with \<open>x \<notin> A\<close> have "fold_graph f z (insert x A) (f x (fold f z A))"
    by (rule fold_graph.insertI)
  then show "fold_graph f z (insert x A) (f x (fold f z A))"
    by simp
qed

declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del]
  \<comment> \<open>No more proofs involve these.\<close>

lemma fold_fun_left_comm:
  assumes "insert x A \ S" "finite A"
  shows "f x (fold f z A) = fold f (f x z) A"
  using assms(2,1)
proof (induct rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert y F)
  then have "fold f (f x z) (insert y F) = f y (fold f (f x z) F)"
    by simp
  also have "\ = f x (f y (fold f z F))"
    using insert by (simp add: fun_left_comm[where ?y=x])
  also have "\ = f x (fold f z (insert y F))"
  proof -
    from insert have "insert y F \ S" by simp
    from fold_insert[OF this] insert show ?thesis by simp
  qed
  finally show ?case ..
qed

lemma fold_insert2:
  "insert x A \ S \ finite A \ x \ A \ fold f z (insert x A) = fold f (f x z) A"
  by (simp add: fold_fun_left_comm)

lemma fold_rec:
  assumes "A \ S"
  assumes "finite A" and "x \ A"
  shows "fold f z A = f x (fold f z (A - {x}))"
proof -
  have A: "A = insert x (A - {x})"
    using \<open>x \<in> A\<close> by blast
  then have "fold f z A = fold f z (insert x (A - {x}))"
    by simp
  also have "\ = f x (fold f z (A - {x}))"
    by (rule fold_insert) (use assms in \<open>auto\<close>)
  finally show ?thesis .
qed

lemma fold_insert_remove:
  assumes "insert x A \ S"
  assumes "finite A"
  shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
proof -
  from \<open>finite A\<close> have "finite (insert x A)"
    by auto
  moreover have "x \ insert x A"
    by auto
  ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"
    using \<open>insert x A \<subseteq> S\<close> by (blast intro: fold_rec)
  then show ?thesis
    by simp
qed

lemma fold_set_union_disj:
  assumes "A \ S" "B \ S"
  assumes "finite A" "finite B" "A \ B = {}"
  shows "Finite_Set.fold f z (A \ B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
  using \<open>finite B\<close> assms(1,2,3,5)
proof induct
  case (insert x F)
  have "fold f z (A \ insert x F) = f x (fold f (fold f z A) F)"
    using insert by auto
  also have "\ = fold f (fold f z A) (insert x F)"
    using insert by (blast intro: fold_insert[symmetric])
  finally show ?case .
qed simp

end

text \<open>Other properties of \<^const>\<open>fold\<close>:\<close>

lemma finite_set_fold_single [simp]: "Finite_Set.fold f z {x} = f x z"
proof -
  have "fold_graph f z {x} (f x z)"
    by (auto intro: fold_graph.intros)
  moreover
  {
    fix X y
    have "fold_graph f z X y \ (X = {} \ y = z) \ (X = {x} \ y = f x z)"
      by (induct rule: fold_graph.induct) auto
  }
  ultimately have "(THE y. fold_graph f z {x} y) = f x z"
    by blast
  thus ?thesis
    by (simp add: Finite_Set.fold_def)
qed

lemma fold_graph_image:
  assumes "inj_on g A"
  shows "fold_graph f z (g ` A) = fold_graph (f \ g) z A"
proof
  fix w
  show "fold_graph f z (g ` A) w = fold_graph (f o g) z A w"
  proof
    assume "fold_graph f z (g ` A) w"
    then show "fold_graph (f \ g) z A w"
      using assms
    proof (induct "g ` A" w arbitrary: A)
      case emptyI
      then show ?case by (auto intro: fold_graph.emptyI)
    next
      case (insertI x A r B)
      from \<open>inj_on g B\<close> \<open>x \<notin> A\<close> \<open>insert x A = image g B\<close> obtain x' A'
        where "x' \ A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
        by (rule inj_img_insertE)
      from insertI.prems have "fold_graph (f \ g) z A' r"
        by (auto intro: insertI.hyps)
      with \<open>x' \<notin> A'\<close> have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
        by (rule fold_graph.insertI)
      then show ?case
        by simp
    qed
  next
    assume "fold_graph (f \ g) z A w"
    then show "fold_graph f z (g ` A) w"
      using assms
    proof induct
      case emptyI
      then show ?case
        by (auto intro: fold_graph.emptyI)
    next
      case (insertI x A r)
      from \<open>x \<notin> A\<close> insertI.prems have "g x \<notin> g ` A"
        by auto
      moreover from insertI have "fold_graph f z (g ` A) r"
        by simp
      ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
        by (rule fold_graph.insertI)
      then show ?case
        by simp
    qed
  qed
qed

lemma fold_image:
  assumes "inj_on g A"
  shows "fold f z (g ` A) = fold (f \ g) z A"
proof (cases "finite A")
  case False
  with assms show ?thesis
    by (auto dest: finite_imageD simp add: fold_def)
next
  case True
  then show ?thesis
    by (auto simp add: fold_def fold_graph_image[OF assms])
qed

lemma fold_cong:
  assumes "comp_fun_commute_on S f" "comp_fun_commute_on S g"
    and "A \ S" "finite A"
    and cong: "\x. x \ A \ f x = g x"
    and "s = t" and "A = B"
  shows "fold f s A = fold g t B"
proof -
  have "fold f s A = fold g s A"
    using \<open>finite A\<close> \<open>A \<subseteq> S\<close> cong
  proof (induct A)
    case empty
    then show ?case by simp
  next
    case insert
    interpret f: comp_fun_commute_on S f by (fact \<open>comp_fun_commute_on S f\<close>)
    interpret g: comp_fun_commute_on S g by (fact \<open>comp_fun_commute_on S g\<close>)
    from insert show ?case by simp
  qed
  with assms show ?thesis by simp
qed

text \<open>A simplified version for idempotent functions:\<close>

locale comp_fun_idem_on = comp_fun_commute_on +
  assumes comp_fun_idem_on: "x \ S \ f x \ f x = f x"
begin

lemma fun_left_idem: "x \ S \ f x (f x z) = f x z"
  using comp_fun_idem_on by (simp add: fun_eq_iff)

lemma fold_insert_idem:
  assumes "insert x A \ S"
  assumes fin: "finite A"
  shows "fold f z (insert x A) = f x (fold f z A)"
proof cases
  assume "x \ A"
  then obtain B where "A = insert x B" and "x \ B"
    by (rule set_insert)
  then show ?thesis
    using assms by (simp add: comp_fun_idem_on fun_left_idem)
next
  assume "x \ A"
  then show ?thesis
    using assms by auto
qed

declare fold_insert [simp del] fold_insert_idem [simp]

lemma fold_insert_idem2: "insert x A \ S \ finite A \ fold f z (insert x A) = fold f (f x z) A"
  by (simp add: fold_fun_left_comm)

end

subsubsection \<open>Liftings to \<open>comp_fun_commute_on\<close> etc.\<close>

lemma (in comp_fun_commute_on) comp_comp_fun_commute_on:
  "range g \ S \ comp_fun_commute_on R (f \ g)"
  by standard (force intro: comp_fun_commute_on)

lemma (in comp_fun_idem_on) comp_comp_fun_idem_on:
  assumes "range g \ S"
  shows "comp_fun_idem_on R (f \ g)"
proof
  interpret f_g: comp_fun_commute_on R "f o g"
    by (fact comp_comp_fun_commute_on[OF \<open>range g \<subseteq> S\<close>])
  show "x \ R \ y \ R \ (f \ g) y \ (f \ g) x = (f \ g) x \ (f \ g) y" for x y
    by (fact f_g.comp_fun_commute_on)
qed (use \<open>range g \<subseteq> S\<close> in \<open>force intro: comp_fun_idem_on\<close>)

lemma (in comp_fun_commute_on) comp_fun_commute_on_funpow:
  "comp_fun_commute_on S (\x. f x ^^ g x)"
proof
  fix x y assume "x \ S" "y \ S"
  show "f y ^^ g y \ f x ^^ g x = f x ^^ g x \ f y ^^ g y"
  proof (cases "x = y")
    case True
    then show ?thesis by simp
  next
    case False
    show ?thesis
    proof (induct "g x" arbitrary: g)
      case 0
      then show ?case by simp
    next
      case (Suc n g)
      have hyp1: "f y ^^ g y \ f x = f x \ f y ^^ g y"
      proof (induct "g y" arbitrary: g)
        case 0
        then show ?case by simp
      next
        case (Suc n g)
        define h where "h z = g z - 1" for z
        with Suc have "n = h y"
          by simp
        with Suc have hyp: "f y ^^ h y \ f x = f x \ f y ^^ h y"
          by auto
        from Suc h_def have "g y = Suc (h y)"
          by simp
        with \<open>x \<in> S\<close> \<open>y \<in> S\<close> show ?case
          by (simp add: comp_assoc hyp) (simp add: o_assoc comp_fun_commute_on)
      qed
      define h where "h z = (if z = x then g x - 1 else g z)" for z
      with Suc have "n = h x"
        by simp
      with Suc have "f y ^^ h y \ f x ^^ h x = f x ^^ h x \ f y ^^ h y"
        by auto
      with False h_def have hyp2: "f y ^^ g y \ f x ^^ h x = f x ^^ h x \ f y ^^ g y"
        by simp
      from Suc h_def have "g x = Suc (h x)"
        by simp
      then show ?case
        by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2) (simp add: comp_assoc hyp1)
    qed
  qed
qed

subsubsection \<open>\<^term>\<open>UNIV\<close> as carrier set\<close>

locale comp_fun_commute =
  fixes f :: "'a \ 'b \ 'b"
  assumes comp_fun_commute: "f y \ f x = f x \ f y"
begin

lemma (in -) comp_fun_commute_def': "comp_fun_commute f = comp_fun_commute_on UNIV f"
  unfolding comp_fun_commute_def comp_fun_commute_on_def by blast

text \<open>
  We abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
  result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
\<close>
sublocale comp_fun_commute_on UNIV f
  rewrites "\X. (X \ UNIV) \ True"
       and "\x. x \ UNIV \ True"
       and "\P. (True \ P) \ Trueprop P"
       and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)"
proof -
  show "comp_fun_commute_on UNIV f"
    by standard  (simp add: comp_fun_commute)
qed simp_all

end

lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f o g)"
  unfolding comp_fun_commute_def' by (fact comp_comp_fun_commute_on)

lemma (in comp_fun_commute) comp_fun_commute_funpow: "comp_fun_commute (\x. f x ^^ g x)"
  unfolding comp_fun_commute_def' by (fact comp_fun_commute_on_funpow)

locale comp_fun_idem = comp_fun_commute +
  assumes comp_fun_idem: "f x o f x = f x"
begin

lemma (in -) comp_fun_idem_def': "comp_fun_idem f = comp_fun_idem_on UNIV f"
  unfolding comp_fun_idem_on_def comp_fun_idem_def comp_fun_commute_def'
  unfolding comp_fun_idem_axioms_def comp_fun_idem_on_axioms_def
  by blast

text \<open>
  Again, we abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
  result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
\<close>
sublocale comp_fun_idem_on UNIV f
  rewrites "\X. (X \ UNIV) \ True"
       and "\x. x \ UNIV \ True"
       and "\P. (True \ P) \ Trueprop P"
       and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)"
proof -
  show "comp_fun_idem_on UNIV f"
    by standard (simp_all add: comp_fun_idem comp_fun_commute)
qed simp_all

end

lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f o g)"
  unfolding comp_fun_idem_def' by (fact comp_comp_fun_idem_on)

subsubsection \<open>Expressing set operations via \<^const>\<open>fold\<close>\<close>

lemma comp_fun_commute_const: "comp_fun_commute (\_. f)"
  by standard (rule refl)

lemma comp_fun_idem_insert: "comp_fun_idem insert"
  by standard auto

lemma comp_fun_idem_remove: "comp_fun_idem Set.remove"
  by standard auto

lemma (in semilattice_inf) comp_fun_idem_inf: "comp_fun_idem inf"
  by standard (auto simp add: inf_left_commute)

lemma (in semilattice_sup) comp_fun_idem_sup: "comp_fun_idem sup"
  by standard (auto simp add: sup_left_commute)

lemma union_fold_insert:
  assumes "finite A"
  shows "A \ B = fold insert B A"
proof -
  interpret comp_fun_idem insert
    by (fact comp_fun_idem_insert)
  from \<open>finite A\<close> show ?thesis
    by (induct A arbitrary: B) simp_all
qed

lemma minus_fold_remove:
  assumes "finite A"
  shows "B - A = fold Set.remove B A"
proof -
  interpret comp_fun_idem Set.remove
    by (fact comp_fun_idem_remove)
  from \<open>finite A\<close> have "fold Set.remove B A = B - A"
    by (induct A arbitrary: B) auto  (* slow *)
  then show ?thesis ..
qed

lemma comp_fun_commute_filter_fold:
  "comp_fun_commute (\x A'. if P x then Set.insert x A' else A')"
proof -
  interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
  show ?thesis by standard (auto simp: fun_eq_iff)
qed

lemma Set_filter_fold:
  assumes "finite A"
  shows "Set.filter P A = fold (\x A'. if P x then Set.insert x A' else A') {} A"
  using assms
proof -
  interpret commute_insert: comp_fun_commute "(\x A'. if P x then Set.insert x A' else A')"
    by (fact comp_fun_commute_filter_fold)
  from \<open>finite A\<close> show ?thesis
    by induct (auto simp add: set_eq_iff)
qed

lemma inter_Set_filter:
  assumes "finite B"
  shows "A \ B = Set.filter (\x. x \ A) B"
  using assms by (simp add: set_eq_iff ac_simps)

lemma image_fold_insert:
  assumes "finite A"
  shows "image f A = fold (\k A. Set.insert (f k) A) {} A"
proof -
  interpret comp_fun_commute "\k A. Set.insert (f k) A"
    by standard auto
  show ?thesis
    using assms by (induct A) auto
qed

lemma Ball_fold:
  assumes "finite A"
  shows "Ball A P = fold (\k s. s \ P k) True A"
proof -
  interpret comp_fun_commute "\k s. s \ P k"
    by standard auto
  show ?thesis
    using assms by (induct A) auto
qed

lemma Bex_fold:
  assumes "finite A"
  shows "Bex A P = fold (\k s. s \ P k) False A"
proof -
  interpret comp_fun_commute "\k s. s \ P k"
    by standard auto
  show ?thesis
    using assms by (induct A) auto
qed

lemma comp_fun_commute_Pow_fold: "comp_fun_commute (\x A. A \ Set.insert x ` A)"
  by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast

lemma Pow_fold:
  assumes "finite A"
  shows "Pow A = fold (\x A. A \ Set.insert x ` A) {{}} A"
proof -
  interpret comp_fun_commute "\x A. A \ Set.insert x ` A"
    by (rule comp_fun_commute_Pow_fold)
  show ?thesis
    using assms by (induct A) (auto simp: Pow_insert)
qed

lemma fold_union_pair:
  assumes "finite B"
  shows "(\y\B. {(x, y)}) \ A = fold (\y. Set.insert (x, y)) A B"
proof -
  interpret comp_fun_commute "\y. Set.insert (x, y)"
    by standard auto
  show ?thesis
    using assms by (induct arbitrary: A) simp_all
qed

lemma comp_fun_commute_product_fold:
  "finite B \ comp_fun_commute (\x z. fold (\y. Set.insert (x, y)) z B)"
  by standard (auto simp: fold_union_pair [symmetric])

lemma product_fold:
  assumes "finite A" "finite B"
  shows "A \ B = fold (\x z. fold (\y. Set.insert (x, y)) z B) {} A"
proof -
  interpret commute_product: comp_fun_commute "(\x z. fold (\y. Set.insert (x, y)) z B)"
    by (fact comp_fun_commute_product_fold[OF \<open>finite B\<close>])
  from assms show ?thesis unfolding Sigma_def
    by (induct A) (simp_all add: fold_union_pair)
qed

context complete_lattice
begin

lemma inf_Inf_fold_inf:
  assumes "finite A"
  shows "inf (Inf A) B = fold inf B A"
proof -
  interpret comp_fun_idem inf
    by (fact comp_fun_idem_inf)
  from \<open>finite A\<close> fold_fun_left_comm show ?thesis
    by (induct A arbitrary: B) (simp_all add: inf_commute fun_eq_iff)
qed

lemma sup_Sup_fold_sup:
  assumes "finite A"
  shows "sup (Sup A) B = fold sup B A"
proof -
  interpret comp_fun_idem sup
    by (fact comp_fun_idem_sup)
  from \<open>finite A\<close> fold_fun_left_comm show ?thesis
    by (induct A arbitrary: B) (simp_all add: sup_commute fun_eq_iff)
qed

lemma Inf_fold_inf: "finite A \ Inf A = fold inf top A"
  using inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)

lemma Sup_fold_sup: "finite A \ Sup A = fold sup bot A"
  using sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)

lemma inf_INF_fold_inf:
  assumes "finite A"
  shows "inf B (\(f ` A)) = fold (inf \ f) B A" (is "?inf = ?fold")
proof -
  interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
  interpret comp_fun_idem "inf \ f" by (fact comp_comp_fun_idem)
  from \<open>finite A\<close> have "?fold = ?inf"
    by (induct A arbitrary: B) (simp_all add: inf_left_commute)
  then show ?thesis ..
qed

lemma sup_SUP_fold_sup:
  assumes "finite A"
  shows "sup B (\(f ` A)) = fold (sup \ f) B A" (is "?sup = ?fold")
proof -
  interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
  interpret comp_fun_idem "sup \ f" by (fact comp_comp_fun_idem)
  from \<open>finite A\<close> have "?fold = ?sup"
    by (induct A arbitrary: B) (simp_all add: sup_left_commute)
  then show ?thesis ..
qed

lemma INF_fold_inf: "finite A \ \(f ` A) = fold (inf \ f) top A"
  using inf_INF_fold_inf [of A top] by simp

lemma SUP_fold_sup: "finite A \ \(f ` A) = fold (sup \ f) bot A"
  using sup_SUP_fold_sup [of A bot] by simp

lemma finite_Inf_in:
  assumes "finite A" "A\{}" and inf: "\x y. \x \ A; y \ A\ \ inf x y \ A"
  shows "Inf A \ A"
proof -
  have "Inf B \ A" if "B \ A" "B\{}" for B
    using finite_subset [OF \<open>B \<subseteq> A\<close> \<open>finite A\<close>] that
  by (induction B) (use inf in \<open>force+\<close>)
  then show ?thesis
    by (simp add: assms)
qed

lemma finite_Sup_in:
  assumes "finite A" "A\{}" and sup: "\x y. \x \ A; y \ A\ \ sup x y \ A"
  shows "Sup A \ A"
proof -
  have "Sup B \ A" if "B \ A" "B\{}" for B
    using finite_subset [OF \<open>B \<subseteq> A\<close> \<open>finite A\<close>] that
  by (induction B) (use sup in \<open>force+\<close>)
  then show ?thesis
    by (simp add: assms)
qed

end

subsubsection \<open>Expressing relation operations via \<^const>\<open>fold\<close>\<close>

lemma Id_on_fold:
  assumes "finite A"
  shows "Id_on A = Finite_Set.fold (\x. Set.insert (Pair x x)) {} A"
proof -
  interpret comp_fun_commute "\x. Set.insert (Pair x x)"
    by standard auto
  from assms show ?thesis
    unfolding Id_on_def by (induct A) simp_all
qed

lemma comp_fun_commute_Image_fold:
  "comp_fun_commute (\(x,y) A. if x \ S then Set.insert y A else A)"
proof -
  interpret comp_fun_idem Set.insert
    by (fact comp_fun_idem_insert)
  show ?thesis
    by standard (auto simp: fun_eq_iff comp_fun_commute split: prod.split)
qed

lemma Image_fold:
  assumes "finite R"
  shows "R `` S = Finite_Set.fold (\(x,y) A. if x \ S then Set.insert y A else A) {} R"
proof -
  interpret comp_fun_commute "(\(x,y) A. if x \ S then Set.insert y A else A)"
    by (rule comp_fun_commute_Image_fold)
  have *: "\x F. Set.insert x F `` S = (if fst x \ S then Set.insert (snd x) (F `` S) else (F `` S))"
    by (force intro: rev_ImageI)
  show ?thesis
    using assms by (induct R) (auto simp: * )
qed

lemma insert_relcomp_union_fold:
  assumes "finite S"
  shows "{x} O S \ X = Finite_Set.fold (\(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') X S"
proof -
  interpret comp_fun_commute "\(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'"
  proof -
    interpret comp_fun_idem Set.insert
      by (fact comp_fun_idem_insert)
    show "comp_fun_commute (\(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')"
      by standard (auto simp add: fun_eq_iff split: prod.split)
  qed
  have *: "{x} O S = {(x', z). x' = fst x \ (snd x, z) \ S}"
    by (auto simp: relcomp_unfold intro!: exI)
  show ?thesis
    unfolding * using \<open>finite S\<close> by (induct S) (auto split: prod.split)
qed

lemma insert_relcomp_fold:
  assumes "finite S"
  shows "Set.insert x R O S =
    Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') (R O S) S"
proof -
  have "Set.insert x R O S = ({x} O S) \ (R O S)"
    by auto
  then show ?thesis
    by (auto simp: insert_relcomp_union_fold [OF assms])
qed

lemma comp_fun_commute_relcomp_fold:
  assumes "finite S"
  shows "comp_fun_commute (\(x,y) A.
    Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S)"
proof -
  have *: "\a b A.
    Finite_Set.fold (\<lambda>(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \<union> A"
    by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong)
  show ?thesis
    by standard (auto simp: * )
qed

lemma relcomp_fold:
  assumes "finite R" "finite S"
  shows "R O S = Finite_Set.fold
    (\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R"
proof -
  interpret commute_relcomp_fold: comp_fun_commute
    "(\(x, y) A. Finite_Set.fold (\(w, z) A'. if y = w then insert (x, z) A' else A') A S)"
    by (fact comp_fun_commute_relcomp_fold[OF \<open>finite S\<close>])
  from assms show ?thesis
    by (induct R) (auto simp: comp_fun_commute_relcomp_fold insert_relcomp_fold cong: if_cong)
qed

subsection \<open>Locales as mini-packages for fold operations\<close>

subsubsection \<open>The natural case\<close>

locale folding_on =
  fixes S :: "'a set"
  fixes f :: "'a \ 'b \ 'b" and z :: "'b"
  assumes comp_fun_commute_on: "x \ S \ y \ S \ f y o f x = f x o f y"
begin

interpretation fold?: comp_fun_commute_on S f
  by standard (simp add: comp_fun_commute_on)

definition F :: "'a set \ 'b"
  where eq_fold: "F A = Finite_Set.fold f z A"

lemma empty [simp]: "F {} = z"
  by (simp add: eq_fold)

lemma infinite [simp]: "\ finite A \ F A = z"
  by (simp add: eq_fold)

lemma insert [simp]:
  assumes "insert x A \ S" and "finite A" and "x \ A"
  shows "F (insert x A) = f x (F A)"
proof -
  from fold_insert assms
  have "Finite_Set.fold f z (insert x A)
      = f x (Finite_Set.fold f z A)"
    by simp
  with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
qed

lemma remove:
  assumes "A \ S" and "finite A" and "x \ A"
  shows "F A = f x (F (A - {x}))"
proof -
  from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
    by (auto dest: mk_disjoint_insert)
  moreover from \<open>finite A\<close> A have "finite B" by simp
  ultimately show ?thesis
    using \<open>A \<subseteq> S\<close> by auto
qed

lemma insert_remove:
  assumes "insert x A \ S" and "finite A"
  shows "F (insert x A) = f x (F (A - {x}))"
  using assms by (cases "x \ A") (simp_all add: remove insert_absorb)

end

subsubsection \<open>With idempotency\<close>

locale folding_idem_on = folding_on +
  assumes comp_fun_idem_on: "x \ S \ y \ S \ f x \ f x = f x"
begin

declare insert [simp del]

interpretation fold?: comp_fun_idem_on S f
  by standard (simp_all add: comp_fun_commute_on comp_fun_idem_on)

lemma insert_idem [simp]:
  assumes "insert x A \ S" and "finite A"
  shows "F (insert x A) = f x (F A)"
proof -
  from fold_insert_idem assms
  have "fold f z (insert x A) = f x (fold f z A)" by simp
  with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
qed

end

subsubsection \<open>\<^term>\<open>UNIV\<close> as the carrier set\<close>

locale folding =
  fixes f :: "'a \ 'b \ 'b" and z :: "'b"
  assumes comp_fun_commute: "f y \ f x = f x \ f y"
begin

lemma (in -) folding_def': "folding f = folding_on UNIV f"
  unfolding folding_def folding_on_def by blast

text \<open>
  Again, we abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
  result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
\<close>
sublocale folding_on UNIV f
  rewrites "\X. (X \ UNIV) \ True"
       and "\x. x \ UNIV \ True"
       and "\P. (True \ P) \ Trueprop P"
       and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)"
proof -
  show "folding_on UNIV f"
    by standard (simp add: comp_fun_commute)
qed simp_all

end

locale folding_idem = folding +
  assumes comp_fun_idem: "f x \ f x = f x"
begin

lemma (in -) folding_idem_def': "folding_idem f = folding_idem_on UNIV f"
  unfolding folding_idem_def folding_def' folding_idem_on_def
  unfolding folding_idem_axioms_def folding_idem_on_axioms_def
  by blast

text \<open>
  Again, we abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
  result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
\<close>
sublocale folding_idem_on UNIV f
  rewrites "\X. (X \ UNIV) \ True"
       and "\x. x \ UNIV \ True"
       and "\P. (True \ P) \ Trueprop P"
       and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)"
proof -
  show "folding_idem_on UNIV f"
    by standard (simp add: comp_fun_idem)
qed simp_all

end

subsection \<open>Finite cardinality\<close>

text \<open>
  The traditional definition
  \<^prop>\<open>card A \<equiv> LEAST n. \<exists>f. A = {f i |i. i < n}\<close>
  is ugly to work with.
  But now that we have \<^const>\<open>fold\<close> things are easy:
\<close>

global_interpretation card: folding "\_. Suc" 0
  defines card = "folding_on.F (\_. Suc) 0"
  by standard (rule refl)

lemma card_insert_disjoint: "finite A \ x \ A \ card (insert x A) = Suc (card A)"
  by (fact card.insert)

lemma card_insert_if: "finite A \ card (insert x A) = (if x \ A then card A else Suc (card A))"
  by auto (simp add: card.insert_remove card.remove)

lemma card_ge_0_finite: "card A > 0 \ finite A"
  by (rule ccontr) simp

lemma card_0_eq [simp]: "finite A \ card A = 0 \ A = {}"
  by (auto dest: mk_disjoint_insert)

lemma finite_UNIV_card_ge_0: "finite (UNIV :: 'a set) \ card (UNIV :: 'a set) > 0"
  by (rule ccontr) simp

lemma card_eq_0_iff: "card A = 0 \ A = {} \ \ finite A"
  by auto

lemma card_range_greater_zero: "finite (range f) \ card (range f) > 0"
  by (rule ccontr) (simp add: card_eq_0_iff)

lemma card_gt_0_iff: "0 < card A \ A \ {} \ finite A"
  by (simp add: neq0_conv [symmetric] card_eq_0_iff)

lemma card_Suc_Diff1:
  assumes "finite A" "x \ A" shows "Suc (card (A - {x})) = card A"
proof -
  have "Suc (card (A - {x})) = card (insert x (A - {x}))"
    using assms by (simp add: card.insert_remove)
  also have "... = card A"
    using assms by (simp add: card_insert_if)
  finally show ?thesis .
qed

lemma card_insert_le_m1:
  assumes "n > 0" "card y \ n - 1" shows "card (insert x y) \ n"
  using assms
  by (cases "finite y") (auto simp: card_insert_if)

lemma card_Diff_singleton:
  assumes "x \ A" shows "card (A - {x}) = card A - 1"
proof (cases "finite A")
  case True
  with assms show ?thesis
    by (simp add: card_Suc_Diff1 [symmetric])
qed auto

lemma card_Diff_singleton_if:
  "card (A - {x}) = (if x \ A then card A - 1 else card A)"
  by (simp add: card_Diff_singleton)

lemma card_Diff_insert[simp]:
  assumes "a \ A" and "a \ B"
  shows "card (A - insert a B) = card (A - B) - 1"
proof -
  have "A - insert a B = (A - B) - {a}"
    using assms by blast
  then show ?thesis
    using assms by (simp add: card_Diff_singleton)
qed

lemma card_insert_le: "card A \ card (insert x A)"
proof (cases "finite A")
  case True
  then show ?thesis   by (simp add: card_insert_if)
qed auto

lemma card_Collect_less_nat[simp]: "card {i::nat. i < n} = n"
  by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq)

lemma card_Collect_le_nat[simp]: "card {i::nat. i \ n} = Suc n"
  using card_Collect_less_nat[of "Suc n"] by (simp add: less_Suc_eq_le)

lemma card_mono:
  assumes "finite B" and "A \ B"
  shows "card A \ card B"
proof -
  from assms have "finite A"
    by (auto intro: finite_subset)
  then show ?thesis
    using assms
  proof (induct A arbitrary: B)
    case empty
    then show ?case by simp
  next
    case (insert x A)
    then have "x \ B"
      by simp
    from insert have "A \ B - {x}" and "finite (B - {x})"
      by auto
    with insert.hyps have "card A \ card (B - {x})"
      by auto
    with \<open>finite A\<close> \<open>x \<notin> A\<close> \<open>finite B\<close> \<open>x \<in> B\<close> show ?case
      by simp (simp only: card.remove)
  qed
qed

lemma card_seteq:
  assumes "finite B" and A: "A \ B" "card B \ card A"
  shows "A = B"
  using assms
proof (induction arbitrary: A rule: finite_induct)
  case (insert b B)
  then have A: "finite A" "A - {b} \ B"
    by force+
  then have "card B \ card (A - {b})"
    using insert by (auto simp add: card_Diff_singleton_if)
  then have "A - {b} = B"
    using A insert.IH by auto
  then show ?case
    using insert.hyps insert.prems by auto
qed auto

lemma psubset_card_mono: "finite B \ A < B \ card A < card B"
  using card_seteq [of B A] by (auto simp add: psubset_eq)

lemma card_Un_Int:
  assumes "finite A" "finite B"
  shows "card A + card B = card (A \ B) + card (A \ B)"
  using assms
proof (induct A)
  case empty
  then show ?case by simp
next
  case insert
  then show ?case
    by (auto simp add: insert_absorb Int_insert_left)
qed

lemma card_Un_disjoint: "finite A \ finite B \ A \ B = {} \ card (A \ B) = card A + card B"
  using card_Un_Int [of A B] by simp

lemma card_Un_disjnt: "\finite A; finite B; disjnt A B\ \ card (A \ B) = card A + card B"
  by (simp add: card_Un_disjoint disjnt_def)

lemma card_Un_le: "card (A \ B) \ card A + card B"
proof (cases "finite A \ finite B")
  case True
  then show ?thesis
    using le_iff_add card_Un_Int [of A B] by auto
qed auto

lemma card_Diff_subset:
  assumes "finite B"
    and "B \ A"
  shows "card (A - B) = card A - card B"
  using assms
proof (cases "finite A")
  case False
  with assms show ?thesis
    by simp
next
  case True
  with assms show ?thesis
    by (induct B arbitrary: A) simp_all
qed

lemma card_Diff_subset_Int:
  assumes "finite (A \ B)"
  shows "card (A - B) = card A - card (A \ B)"
proof -
  have "A - B = A - A \ B" by auto
  with assms show ?thesis
    by (simp add: card_Diff_subset)
qed

lemma card_Int_Diff:
  assumes "finite A"
  shows "card A = card (A \ B) + card (A - B)"
  by (simp add: assms card_Diff_subset_Int card_mono)

lemma diff_card_le_card_Diff:
  assumes "finite B"
  shows "card A - card B \ card (A - B)"
proof -
  have "card A - card B \ card A - card (A \ B)"
--> --------------------

--> maximum size reached

--> --------------------

quality93%

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.