Quelle FiniteProduct.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/FiniteProduct.thy
    Author:     Clemens Ballarin, started 19 November 2002

This file is largely based on HOL/Finite_Set.thy.
*)

theory FiniteProduct
imports Group
begin

subsection \<open>Product Operator for Commutative Monoids\<close>

subsubsection \<open>Inductive Definition of a Relation for Products over Sets\<close>

text \<open>Instantiation of locale \<open>LC\<close> of theory \<open>Finite_Set\<close> is not
  possible, because here we have explicit typing rules like
  \<open>x \<in> carrier G\<close>.  We introduce an explicit argument for the domain
  \<open>D\<close>.\<close>

inductive_set
  foldSetD :: "['a set, 'b \ 'a \ 'a, 'a] \ ('b set * 'a) set"
  for D :: "'a set" and f :: "'b \ 'a \ 'a" and e :: 'a
  where
    emptyI [intro]: "e \ D \ ({}, e) \ foldSetD D f e"
  | insertI [intro]: "\x \ A; f x y \ D; (A, y) \ foldSetD D f e\ \
                      (insert x A, f x y) \<in> foldSetD D f e"

inductive_cases empty_foldSetDE [elim!]: "({}, x) \ foldSetD D f e"

definition
  foldD :: "['a set, 'b \ 'a \ 'a, 'a, 'b set] \ 'a"
  where "foldD D f e A = (THE x. (A, x) \ foldSetD D f e)"

lemma foldSetD_closed: "(A, z) \ foldSetD D f e \ z \ D"
  by (erule foldSetD.cases) auto

lemma Diff1_foldSetD:
  "\(A - {x}, y) \ foldSetD D f e; x \ A; f x y \ D\ \
   (A, f x y) \<in> foldSetD D f e"
  by (metis Diff_insert_absorb foldSetD.insertI mk_disjoint_insert)

lemma foldSetD_imp_finite [simp]: "(A, x) \ foldSetD D f e \ finite A"
  by (induct set: foldSetD) auto

lemma finite_imp_foldSetD:
  "\finite A; e \ D; \x y. \x \ A; y \ D\ \ f x y \ D\
    \<Longrightarrow> \<exists>x. (A, x) \<in> foldSetD D f e"
proof (induct set: finite)
  case empty then show ?case by auto
next
  case (insert x F)
  then obtain y where y: "(F, y) \ foldSetD D f e" by auto
  with insert have "y \ D" by (auto dest: foldSetD_closed)
  with y and insert have "(insert x F, f x y) \ foldSetD D f e"
    by (intro foldSetD.intros) auto
  then show ?case ..
qed

lemma foldSetD_backwards:
  assumes "A \ {}" "(A, z) \ foldSetD D f e"
  shows "\x y. x \ A \ (A - { x }, y) \ foldSetD D f e \ z = f x y"
  using assms(2) by (cases) (simp add: assms(1), metis Diff_insert_absorb insertI1)

subsubsection \<open>Left-Commutative Operations\<close>

locale LCD =
  fixes B :: "'b set"
  and D :: "'a set"
  and f :: "'b \ 'a \ 'a" (infixl \\\ 70)
  assumes left_commute:
    "\x \ B; y \ B; z \ D\ \ x \ (y \ z) = y \ (x \ z)"
  and f_closed [simp, intro!]: "!!x y. \x \ B; y \ D\ \ f x y \ D"

lemma (in LCD) foldSetD_closed [dest]: "(A, z) \ foldSetD D f e \ z \ D"
  by (erule foldSetD.cases) auto

lemma (in LCD) Diff1_foldSetD:
  "\(A - {x}, y) \ foldSetD D f e; x \ A; A \ B\ \
  (A, f x y) \<in> foldSetD D f e"
  by (meson Diff1_foldSetD f_closed local.foldSetD_closed subsetCE)

lemma (in LCD) finite_imp_foldSetD:
  "\finite A; A \ B; e \ D\ \ \x. (A, x) \ foldSetD D f e"
proof (induct set: finite)
  case empty then show ?case by auto
next
  case (insert x F)
  then obtain y where y: "(F, y) \ foldSetD D f e" by auto
  with insert have "y \ D" by auto
  with y and insert have "(insert x F, f x y) \ foldSetD D f e"
    by (intro foldSetD.intros) auto
  then show ?case ..
qed

lemma (in LCD) foldSetD_determ_aux:
  assumes "e \ D" and A: "card A < n" "A \ B" "(A, x) \ foldSetD D f e" "(A, y) \ foldSetD D f e"
  shows "y = x"
  using A
proof (induction n arbitrary: A x y)
  case 0
  then show ?case
    by auto
next
  case (Suc n)
  then consider "card A = n" | "card A < n"
    by linarith
  then show ?case
  proof cases
    case 1
    show ?thesis
      using foldSetD.cases [OF \<open>(A,x) \<in> foldSetD D (\<cdot>) e\<close>]
    proof cases
      case 1
      then show ?thesis
        using \<open>(A,y) \<in> foldSetD D (\<cdot>) e\<close> by auto
    next
      case A': (2 x' A' y')
      show ?thesis
        using foldSetD.cases [OF \<open>(A,y) \<in> foldSetD D (\<cdot>) e\<close>]
      proof cases
        case 1
        then show ?thesis
          using \<open>(A,x) \<in> foldSetD D (\<cdot>) e\<close> by auto
      next
        case A'': (2 x'' A'' y'')
        show ?thesis
        proof (cases "x' = x''")
          case True
          show ?thesis
          proof (cases "y' = y''")
            case True
            then show ?thesis
              using A' A'' \x' = x''\ by (blast elim!: equalityE)
          next
            case False
            then show ?thesis
              using A' A'' \x' = x''\
              by (metis \<open>card A = n\<close> Suc.IH Suc.prems(2) card_insert_disjoint foldSetD_imp_finite insert_eq_iff insert_subset lessI)
          qed
        next
          case False
          then have *: "A' - {x''} = A'' - {x'}" "x'' \ A'" "x' \ A''"
            using A' A'' by fastforce+
          then have "A' = insert x'' A'' - {x'}"
            using \<open>x' \<notin> A'\<close> by blast
          then have card: "card A' \ card A''"
            using A' A'' * by (metis card_Suc_Diff1 eq_refl foldSetD_imp_finite)
          obtain u where u: "(A' - {x''}, u) \ foldSetD D (\) e"
            using finite_imp_foldSetD [of "A' - {x''}"] A' Diff_insert \A \ B\ \e \ D\ by fastforce
          have "y' = f x'' u"
            using Diff1_foldSetD [OF u] \<open>x'' \<in> A'\<close> \<open>card A = n\<close> A' Suc.IH \<open>A \<subseteq> B\<close> by auto
          then have "(A'' - {x'}, u) \ foldSetD D f e"
            using "*"(1) u by auto
          then have "y'' = f x' u"
            using A'' by (metis * \<open>card A = n\<close> A'(1) Diff1_foldSetD Suc.IH \<open>A \<subseteq> B\<close>
                card card_Suc_Diff1 card_insert_disjoint foldSetD_imp_finite insert_subset le_imp_less_Suc)
          then show ?thesis
            using A' A''
            by (metis \<open>A \<subseteq> B\<close> \<open>y' = x'' \<cdot> u\<close> insert_subset left_commute local.foldSetD_closed u)
        qed
      qed
    qed
  next
    case 2 with Suc show ?thesis by blast
  qed
qed

lemma (in LCD) foldSetD_determ:
  "\(A, x) \ foldSetD D f e; (A, y) \ foldSetD D f e; e \ D; A \ B\
  \<Longrightarrow> y = x"
  by (blast intro: foldSetD_determ_aux [rule_format])

lemma (in LCD) foldD_equality:
  "\(A, y) \ foldSetD D f e; e \ D; A \ B\ \ foldD D f e A = y"
  by (unfold foldD_def) (blast intro: foldSetD_determ)

lemma foldD_empty [simp]:
  "e \ D \ foldD D f e {} = e"
  by (unfold foldD_def) blast

lemma (in LCD) foldD_insert_aux:
  "\x \ A; x \ B; e \ D; A \ B\
    \<Longrightarrow> ((insert x A, v) \<in> foldSetD D f e) \<longleftrightarrow> (\<exists>y. (A, y) \<in> foldSetD D f e \<and> v = f x y)"
  apply auto
  by (metis Diff_insert_absorb f_closed finite_Diff foldSetD.insertI foldSetD_determ foldSetD_imp_finite insert_subset local.finite_imp_foldSetD local.foldSetD_closed)

lemma (in LCD) foldD_insert:
  assumes "finite A" "x \ A" "x \ B" "e \ D" "A \ B"
  shows "foldD D f e (insert x A) = f x (foldD D f e A)"
proof -
  have "(THE v. \y. (A, y) \ foldSetD D (\) e \ v = x \ y) = x \ (THE y. (A, y) \ foldSetD D (\) e)"
    by (rule the_equality) (use assms foldD_def foldD_equality foldD_def finite_imp_foldSetD in \<open>metis+\<close>)
  then show ?thesis
    unfolding foldD_def using assms by (simp add: foldD_insert_aux)
qed

lemma (in LCD) foldD_closed [simp]:
  "\finite A; e \ D; A \ B\ \ foldD D f e A \ D"
proof (induct set: finite)
  case empty then show ?case by simp
next
  case insert then show ?case by (simp add: foldD_insert)
qed

lemma (in LCD) foldD_commute:
  "\finite A; x \ B; e \ D; A \ B\ \
   f x (foldD D f e A) = foldD D f (f x e) A"
  by (induct set: finite) (auto simp add: left_commute foldD_insert)

lemma Int_mono2:
  "\A \ C; B \ C\ \ A Int B \ C"
  by blast

lemma (in LCD) foldD_nest_Un_Int:
  "\finite A; finite C; e \ D; A \ B; C \ B\ \
   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
proof (induction set: finite)
  case (insert x F)
  then show ?case
    by (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb Int_mono2)
qed simp

lemma (in LCD) foldD_nest_Un_disjoint:
  "\finite A; finite B; A Int B = {}; e \ D; A \ B; C \ B\
    \<Longrightarrow> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
  by (simp add: foldD_nest_Un_Int)

\<comment> \<open>Delete rules to do with \<open>foldSetD\<close> relation.\<close>

declare foldSetD_imp_finite [simp del]
  empty_foldSetDE [rule del]
  foldSetD.intros [rule del]
declare (in LCD)
  foldSetD_closed [rule del]

text \<open>Commutative Monoids\<close>

text \<open>
  We enter a more restrictive context, with \<open>f :: 'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>
  instead of \<open>'b \<Rightarrow> 'a \<Rightarrow> 'a\<close>.
\<close>

locale ACeD =
  fixes D :: "'a set"
    and f :: "'a \ 'a \ 'a" (infixl \\\ 70)
    and e :: 'a
  assumes ident [simp]: "x \ D \ x \ e = x"
    and commute: "\x \ D; y \ D\ \ x \ y = y \ x"
    and assoc: "\x \ D; y \ D; z \ D\ \ (x \ y) \ z = x \ (y \ z)"
    and e_closed [simp]: "e \ D"
    and f_closed [simp]: "\x \ D; y \ D\ \ x \ y \ D"

lemma (in ACeD) left_commute:
  "\x \ D; y \ D; z \ D\ \ x \ (y \ z) = y \ (x \ z)"
proof -
  assume D: "x \ D" "y \ D" "z \ D"
  then have "x \ (y \ z) = (y \ z) \ x" by (simp add: commute)
  also from D have "... = y \ (z \ x)" by (simp add: assoc)
  also from D have "z \ x = x \ z" by (simp add: commute)
  finally show ?thesis .
qed

lemmas (in ACeD) AC = assoc commute left_commute

lemma (in ACeD) left_ident [simp]: "x \ D \ e \ x = x"
proof -
  assume "x \ D"
  then have "x \ e = x" by (rule ident)
  with \<open>x \<in> D\<close> show ?thesis by (simp add: commute)
qed

lemma (in ACeD) foldD_Un_Int:
  "\finite A; finite B; A \ D; B \ D\ \
    foldD D f e A \<cdot> foldD D f e B =
    foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
proof (induction set: finite)
  case empty
  then show ?case
    by(simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
next
  case (insert x F)
  then show ?case
    by(simp add: AC insert_absorb Int_insert_left Int_mono2
                 LCD.foldD_insert [OF LCD.intro [of D]]
                 LCD.foldD_closed [OF LCD.intro [of D]])
qed

lemma (in ACeD) foldD_Un_disjoint:
  "\finite A; finite B; A Int B = {}; A \ D; B \ D\ \
    foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
  by (simp add: foldD_Un_Int
    left_commute LCD.foldD_closed [OF LCD.intro [of D]])

subsubsection \<open>Products over Finite Sets\<close>

definition
  finprod :: "[('b, 'm) monoid_scheme, 'a \ 'b, 'a set] \ 'b"
  where "finprod G f A =
   (if finite A
    then foldD (carrier G) (mult G \<circ> f) \<one>\<^bsub>G\<^esub> A
    else \<one>\<^bsub>G\<^esub>)"

syntax
  "_finprod" :: "index \ idt \ 'a set \ 'b \ 'b"
    (\<open>(\<open>indent=3 notation=\<open>binder \<Otimes>\<close>\<close>\<Otimes>__\<in>_. _)\<close> [1000, 0, 51, 10] 10)
syntax_consts
  "_finprod" \<rightleftharpoons> finprod
translations
  "\\<^bsub>G\<^esub>i\A. b" \ "CONST finprod G (%i. b) A"
  \<comment> \<open>Beware of argument permutation!\<close>

lemma (in comm_monoid) finprod_empty [simp]:
  "finprod G f {} = \"
  by (simp add: finprod_def)

lemma (in comm_monoid) finprod_infinite[simp]:
  "\ finite A \ finprod G f A = \"
  by (simp add: finprod_def)

declare funcsetI [intro]
  funcset_mem [dest]

context comm_monoid begin

lemma finprod_insert [simp]:
  assumes "finite F" "a \ F" "f \ F \ carrier G" "f a \ carrier G"
  shows "finprod G f (insert a F) = f a \ finprod G f F"
proof -
  have "finprod G f (insert a F) = foldD (carrier G) ((\) \ f) \ (insert a F)"
    by (simp add: finprod_def assms)
  also have "... = ((\) \ f) a (foldD (carrier G) ((\) \ f) \ F)"
    by (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
      (use assms in \<open>auto simp: m_lcomm Pi_iff\<close>)
  also have "... = f a \ finprod G f F"
    using \<open>finite F\<close> by (auto simp add: finprod_def)
  finally show ?thesis .
qed

lemma finprod_one_eqI: "(\x. x \ A \ f x = \) \ finprod G f A = \"
proof (induct A rule: infinite_finite_induct)
  case empty show ?case by simp
next
  case (insert a A)
  have "(\i. \) \ A \ carrier G" by auto
  with insert show ?case by simp
qed simp

lemma finprod_one [simp]: "(\i\A. \) = \"
  by (simp add: finprod_one_eqI)

lemma finprod_closed [simp]:
  fixes A
  assumes f: "f \ A \ carrier G"
  shows "finprod G f A \ carrier G"
using f
proof (induct A rule: infinite_finite_induct)
  case empty show ?case by simp
next
  case (insert a A)
  then have a: "f a \ carrier G" by fast
  from insert have A: "f \ A \ carrier G" by fast
  from insert A a show ?case by simp
qed simp

lemma funcset_Int_left [simp, intro]:
  "\f \ A \ C; f \ B \ C\ \ f \ A Int B \ C"
  by fast

lemma funcset_Un_left [iff]:
  "(f \ A Un B \ C) = (f \ A \ C \ f \ B \ C)"
  by fast

lemma finprod_Un_Int:
  "\finite A; finite B; g \ A \ carrier G; g \ B \ carrier G\ \
     finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
     finprod G g A \<otimes> finprod G g B"
\<comment> \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
proof (induct set: finite)
  case empty then show ?case by simp
next
  case (insert a A)
  then have a: "g a \ carrier G" by fast
  from insert have A: "g \ A \ carrier G" by fast
  from insert A a show ?case
    by (simp add: m_ac Int_insert_left insert_absorb Int_mono2)
qed

lemma finprod_Un_disjoint:
  "\finite A; finite B; A Int B = {};
      g \<in> A \<rightarrow> carrier G; g \<in> B \<rightarrow> carrier G\<rbrakk>
   \<Longrightarrow> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
  by (metis Pi_split_domain finprod_Un_Int finprod_closed finprod_empty r_one)

lemma finprod_multf [simp]:
  "\f \ A \ carrier G; g \ A \ carrier G\ \
   finprod G (\<lambda>x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
proof (induct A rule: infinite_finite_induct)
  case empty show ?case by simp
next
  case (insert a A) then
  have fA: "f \ A \ carrier G" by fast
  from insert have fa: "f a \ carrier G" by fast
  from insert have gA: "g \ A \ carrier G" by fast
  from insert have ga: "g a \ carrier G" by fast
  from insert have fgA: "(%x. f x \ g x) \ A \ carrier G"
    by (simp add: Pi_def)
  show ?case
    by (simp add: insert fA fa gA ga fgA m_ac)
qed simp

lemma finprod_cong':
  "\A = B; g \ B \ carrier G;
      !!i. i \<in> B \<Longrightarrow> f i = g i\<rbrakk> \<Longrightarrow> finprod G f A = finprod G g B"
proof -
  assume prems: "A = B" "g \ B \ carrier G"
    "!!i. i \ B \ f i = g i"
  show ?thesis
  proof (cases "finite B")
    case True
    then have "!!A. \A = B; g \ B \ carrier G;
      !!i. i \<in> B \<Longrightarrow> f i = g i\<rbrakk> \<Longrightarrow> finprod G f A = finprod G g B"
    proof induct
      case empty thus ?case by simp
    next
      case (insert x B)
      then have "finprod G f A = finprod G f (insert x B)" by simp
      also from insert have "... = f x \ finprod G f B"
      proof (intro finprod_insert)
        show "finite B" by fact
      next
        show "x \ B" by fact
      next
        assume "x \ B" "!!i. i \ insert x B \ f i = g i"
          "g \ insert x B \ carrier G"
        thus "f \ B \ carrier G" by fastforce
      next
        assume "x \ B" "!!i. i \ insert x B \ f i = g i"
          "g \ insert x B \ carrier G"
        thus "f x \ carrier G" by fastforce
      qed
      also from insert have "... = g x \ finprod G g B" by fastforce
      also from insert have "... = finprod G g (insert x B)"
      by (intro finprod_insert [THEN sym]) auto
      finally show ?case .
    qed
    with prems show ?thesis by simp
  next
    case False with prems show ?thesis by simp
  qed
qed

lemma finprod_cong:
  "\A = B; f \ B \ carrier G = True;
      \<And>i. i \<in> B =simp=> f i = g i\<rbrakk> \<Longrightarrow> finprod G f A = finprod G g B"
  (* This order of prems is slightly faster (3%) than the last two swapped. *)
  by (rule finprod_cong') (auto simp add: simp_implies_def)

text \<open>Usually, if this rule causes a failed congruence proof error,
  the reason is that the premise \<open>g \<in> B \<rightarrow> carrier G\<close> cannot be shown.
  Adding @{thm [source] Pi_def} to the simpset is often useful.
  For this reason, @{thm [source] finprod_cong}
  is not added to the simpset by default.
\<close>

end

declare funcsetI [rule del]
  funcset_mem [rule del]

context comm_monoid begin

lemma finprod_0 [simp]:
  "f \ {0::nat} \ carrier G \ finprod G f {..0} = f 0"
  by (simp add: Pi_def)

lemma finprod_0':
  "f \ {..n} \ carrier G \ (f 0) \ finprod G f {Suc 0..n} = finprod G f {..n}"
proof -
  assume A: "f \ {.. n} \ carrier G"
  hence "(f 0) \ finprod G f {Suc 0..n} = finprod G f {..0} \ finprod G f {Suc 0..n}"
    using finprod_0[of f] by (simp add: funcset_mem)
  also have " ... = finprod G f ({..0} \ {Suc 0..n})"
    using finprod_Un_disjoint[of "{..0}" "{Suc 0..n}" f] A by (simp add: funcset_mem)
  also have " ... = finprod G f {..n}"
    by (simp add: atLeastAtMost_insertL atMost_atLeast0)
  finally show ?thesis .
qed

lemma finprod_Suc [simp]:
  "f \ {..Suc n} \ carrier G \
   finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
by (simp add: Pi_def atMost_Suc)

lemma finprod_Suc2:
  "f \ {..Suc n} \ carrier G \
   finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
proof (induct n)
  case 0 thus ?case by (simp add: Pi_def)
next
  case Suc thus ?case by (simp add: m_assoc Pi_def)
qed

lemma finprod_Suc3:
  assumes "f \ {..n :: nat} \ carrier G"
  shows "finprod G f {.. n} = (f n) \ finprod G f {..< n}"
proof (cases "n = 0")
  case True thus ?thesis
   using assms atMost_Suc by simp
next
  case False
  then obtain k where "n = Suc k"
    using not0_implies_Suc by blast
  thus ?thesis
    using finprod_Suc[of f k] assms atMost_Suc lessThan_Suc_atMost by simp
qed

lemma finprod_reindex: \<^marker>\<open>contributor \<open>Jeremy Avigad\<close>\<close>
  "f \ (h ` A) \ carrier G \
        inj_on h A \<Longrightarrow> finprod G f (h ` A) = finprod G (\<lambda>x. f (h x)) A"
proof (induct A rule: infinite_finite_induct)
  case (infinite A)
  hence "\ finite (h ` A)"
    using finite_imageD by blast
  with \<open>\<not> finite A\<close> show ?case by simp
qed (auto simp add: Pi_def)

lemma finprod_const: \<^marker>\<open>contributor \<open>Jeremy Avigad\<close>\<close>
  assumes a [simp]: "a \ carrier G"
    shows "finprod G (\x. a) A = a [^] card A"
proof (induct A rule: infinite_finite_induct)
  case (insert b A)
  show ?case
  proof (subst finprod_insert[OF insert(1-2)])
    show "a \ (\x\A. a) = a [^] card (insert b A)"
      by (insert insert, auto, subst m_comm, auto)
  qed auto
qed auto

lemma finprod_singleton: \<^marker>\<open>contributor \<open>Jesus Aransay\<close>\<close>
  assumes i_in_A: "i \ A" and fin_A: "finite A" and f_Pi: "f \ A \ carrier G"
  shows "(\j\A. if i = j then f j else \) = f i"
  using i_in_A finprod_insert [of "A - {i}" i "(\j. if i = j then f j else \)"]
    fin_A f_Pi finprod_one [of "A - {i}"]
    finprod_cong [of "A - {i}" "A - {i}" "(\j. if i = j then f j else \)" "(\i. \)"]
  unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)

lemma finprod_singleton_swap:
  assumes i_in_A: "i \ A" and fin_A: "finite A" and f_Pi: "f \ A \ carrier G"
  shows "(\j\A. if j = i then f j else \) = f i"
  using finprod_singleton [OF assms] by (simp add: eq_commute)

lemma finprod_mono_neutral_cong_left:
  assumes "finite B"
    and "A \ B"
    and 1: "\i. i \ B - A \ h i = \"
    and gh: "\x. x \ A \ g x = h x"
    and h: "h \ B \ carrier G"
  shows "finprod G g A = finprod G h B"
proof-
  have eq: "A \ (B - A) = B" using \A \ B\ by blast
  have d: "A \ (B - A) = {}" using \A \ B\ by blast
  from \<open>finite B\<close> \<open>A \<subseteq> B\<close> have f: "finite A" "finite (B - A)"
    by (auto intro: finite_subset)
  have "h \ A \ carrier G" "h \ B - A \ carrier G"
    using assms by (auto simp: image_subset_iff_funcset)
  moreover have "finprod G g A = finprod G h A \ finprod G h (B - A)"
  proof -
    have "finprod G h (B - A) = \"
      using "1" finprod_one_eqI by blast
    moreover have "finprod G g A = finprod G h A"
      using \<open>h \<in> A \<rightarrow> carrier G\<close> finprod_cong' gh by blast
    ultimately show ?thesis
      by (simp add: \<open>h \<in> A \<rightarrow> carrier G\<close>)
  qed
  ultimately show ?thesis
    by (simp add: finprod_Un_disjoint [OF f d, unfolded eq])
qed

lemma finprod_mono_neutral_cong_right:
  assumes "finite B"
    and "A \ B" "\i. i \ B - A \ g i = \" "\x. x \ A \ g x = h x" "g \ B \ carrier G"
  shows "finprod G g B = finprod G h A"
  using assms  by (auto intro!: finprod_mono_neutral_cong_left [symmetric])

lemma finprod_mono_neutral_cong:
  assumes [simp]: "finite B" "finite A"
    and *: "\i. i \ B - A \ h i = \" "\i. i \ A - B \ g i = \"
    and gh: "\x. x \ A \ B \ g x = h x"
    and g: "g \ A \ carrier G"
    and h: "h \ B \ carrier G"
shows "finprod G g A = finprod G h B"
proof-
  have "finprod G g A = finprod G g (A \ B)"
    by (rule finprod_mono_neutral_cong_right) (use assms in auto)
  also have "\ = finprod G h (A \ B)"
    by (rule finprod_cong) (use assms in auto)
  also have "\ = finprod G h B"
    by (rule finprod_mono_neutral_cong_left) (use assms in auto)
  finally show ?thesis .
qed

end

(* Jeremy Avigad. This should be generalized to arbitrary groups, not just commutative
   ones, using Lagrange's theorem. *)

lemma (in comm_group) power_order_eq_one:
  assumes fin [simp]: "finite (carrier G)"
    and a [simp]: "a \ carrier G"
  shows "a [^] card(carrier G) = one G"
proof -
  have "(\x\carrier G. x) = (\x\carrier G. a \ x)"
    by (subst (2) finprod_reindex [symmetric],
      auto simp add: Pi_def inj_on_cmult surj_const_mult)
  also have "\ = (\x\carrier G. a) \ (\x\carrier G. x)"
    by (auto simp add: finprod_multf Pi_def)
  also have "(\x\carrier G. a) = a [^] card(carrier G)"
    by (auto simp add: finprod_const)
  finally show ?thesis
    by auto
qed

lemma (in comm_monoid) finprod_UN_disjoint:
  assumes
    "finite I" "\i. i \ I \ finite (A i)" "pairwise (\i j. disjnt (A i) (A j)) I"
    "\i x. i \ I \ x \ A i \ g x \ carrier G"
shows "finprod G g (\(A ` I)) = finprod G (\i. finprod G g (A i)) I"
  using assms
proof (induction set: finite)
  case empty
  then show ?case
    by force
next
  case (insert i I)
  then show ?case
    unfolding pairwise_def disjnt_def
    apply clarsimp
    apply (subst finprod_Un_disjoint)
         apply (fastforce intro!: funcsetI finprod_closed)+
    done
qed

lemma (in comm_monoid) finprod_Union_disjoint:
  "\finite C; \A. A \ C \ finite A \ (\x\A. f x \ carrier G); pairwise disjnt C\ \
    finprod G f (\<Union>C) = finprod G (finprod G f) C"
  by (frule finprod_UN_disjoint [of C id f]) auto

end

quality94%

¤ Dauer der Verarbeitung: 0.8 Sekunden ¤

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.