finprod takes 1 in case of infinite sets => remove several "finite A" assumptions
--- a/src/HOL/Algebra/FiniteProduct.thy Fri Apr 17 09:56:12 2015 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Fri Apr 17 11:52:36 2015 +0200
@@ -292,7 +292,7 @@
where "finprod G f A =
(if finite A
then foldD (carrier G) (mult G o f) \<one>\<^bsub>G\<^esub> A
- else undefined)"
+ else \<one>\<^bsub>G\<^esub>)"
syntax
"_finprod" :: "index => idt => 'a set => 'b => 'b"
@@ -311,6 +311,10 @@
"finprod G f {} = \<one>"
by (simp add: finprod_def)
+lemma (in comm_monoid) finprod_infinite[simp]:
+ "\<not> finite A \<Longrightarrow> finprod G f A = \<one>"
+ by (simp add: finprod_def)
+
declare funcsetI [intro]
funcset_mem [dest]
@@ -335,28 +339,28 @@
done
lemma finprod_one [simp]:
- "finite A ==> (\<Otimes>i:A. \<one>) = \<one>"
-proof (induct set: finite)
+ "(\<Otimes>i:A. \<one>) = \<one>"
+proof (induct A rule: infinite_finite_induct)
case empty show ?case by simp
next
case (insert a A)
have "(%i. \<one>) \<in> A -> carrier G" by auto
with insert show ?case by simp
-qed
+qed simp
lemma finprod_closed [simp]:
fixes A
- assumes fin: "finite A" and f: "f \<in> A -> carrier G"
+ assumes f: "f \<in> A -> carrier G"
shows "finprod G f A \<in> carrier G"
-using fin f
-proof induct
+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 \<in> carrier G" by fast
from insert have A: "f \<in> A -> carrier G" by fast
from insert A a show ?case by simp
-qed
+qed simp
lemma funcset_Int_left [simp, intro]:
"[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
@@ -390,9 +394,9 @@
done
lemma finprod_multf:
- "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
+ "[| f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
-proof (induct set: finite)
+proof (induct A rule: infinite_finite_induct)
case empty show ?case by simp
next
case (insert a A) then
@@ -404,7 +408,7 @@
by (simp add: Pi_def)
show ?case
by (simp add: insert fA fa gA ga fgA m_ac)
-qed
+qed simp
lemma finprod_cong':
"[| A = B; g \<in> B -> carrier G;
@@ -443,7 +447,7 @@
qed
with prems show ?thesis by simp
next
- case False with prems show ?thesis by (simp add: finprod_def)
+ case False with prems show ?thesis by simp
qed
qed
@@ -494,23 +498,26 @@
(* The following two were contributed by Jeremy Avigad. *)
lemma finprod_reindex:
- assumes fin: "finite A"
- shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow>
+ "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow>
inj_on h A ==> finprod G f (h ` A) = finprod G (%x. f (h x)) A"
- using fin
- by induct (auto simp add: Pi_def)
+proof (induct A rule: infinite_finite_induct)
+ case (infinite A)
+ hence "\<not> finite (h ` A)"
+ using finite_imageD by blast
+ with `\<not> finite A` show ?case by simp
+qed (auto simp add: Pi_def)
lemma finprod_const:
- assumes fin [simp]: "finite A"
- and a [simp]: "a : carrier G"
+ assumes a [simp]: "a : carrier G"
shows "finprod G (%x. a) A = a (^) card A"
- using fin apply induct
- apply force
- apply (subst finprod_insert)
- apply auto
- apply (subst m_comm)
- apply auto
- done
+proof (induct A rule: infinite_finite_induct)
+ case (insert b A)
+ show ?case
+ proof (subst finprod_insert[OF insert(1-2)])
+ show "a \<otimes> (\<Otimes>x\<in>A. a) = a (^) card (insert b A)"
+ by (insert insert, auto, subst m_comm, auto)
+ qed auto
+qed auto
(* The following lemma was contributed by Jesus Aransay. *)
--- a/src/HOL/Algebra/IntRing.thy Fri Apr 17 09:56:12 2015 +0200
+++ b/src/HOL/Algebra/IntRing.thy Fri Apr 17 11:52:36 2015 +0200
@@ -73,7 +73,7 @@
qed
interpretation int: comm_monoid \<Z>
- where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
+ where "finprod \<Z> f A = setprod f A"
proof -
-- "Specification"
show "comm_monoid \<Z>" by default auto
@@ -83,28 +83,15 @@
{ fix x y have "mult \<Z> x y = x * y" by simp }
note mult = this
have one: "one \<Z> = 1" by simp
- show "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
- proof (cases "finite A")
- case True
- then show ?thesis
- proof induct
- case empty
- show ?case by (simp add: one)
- next
- case insert
- then show ?case by (simp add: Pi_def mult)
- qed
- next
- case False
- then show ?thesis by (simp add: finprod_def)
- qed
+ show "finprod \<Z> f A = setprod f A"
+ by (induct A rule: infinite_finite_induct, auto)
qed
interpretation int: abelian_monoid \<Z>
where int_carrier_eq: "carrier \<Z> = UNIV"
and int_zero_eq: "zero \<Z> = 0"
and int_add_eq: "add \<Z> x y = x + y"
- and int_finsum_eq: "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
+ and int_finsum_eq: "finsum \<Z> f A = setsum f A"
proof -
-- "Specification"
show "abelian_monoid \<Z>" by default auto
@@ -118,21 +105,8 @@
note add = this
show zero: "zero \<Z> = 0"
by simp
- show "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
- proof (cases "finite A")
- case True
- then show ?thesis
- proof induct
- case empty
- show ?case by (simp add: zero)
- next
- case insert
- then show ?case by (simp add: Pi_def add)
- qed
- next
- case False
- then show ?thesis by (simp add: finsum_def finprod_def)
- qed
+ show "finsum \<Z> f A = setsum f A"
+ by (induct A rule: infinite_finite_induct, auto)
qed
interpretation int: abelian_group \<Z>
@@ -143,7 +117,7 @@
where "carrier \<Z> = UNIV"
and "zero \<Z> = 0"
and "add \<Z> x y = x + y"
- and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
+ and "finsum \<Z> f A = setsum f A"
and int_a_inv_eq: "a_inv \<Z> x = - x"
and int_a_minus_eq: "a_minus \<Z> x y = x - y"
proof -
@@ -176,7 +150,7 @@
where "carrier \<Z> = UNIV"
and "zero \<Z> = 0"
and "add \<Z> x y = x + y"
- and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
+ and "finsum \<Z> f A = setsum f A"
and "a_inv \<Z> x = - x"
and "a_minus \<Z> x y = x - y"
proof -
--- a/src/HOL/Algebra/Ring.thy Fri Apr 17 09:56:12 2015 +0200
+++ b/src/HOL/Algebra/Ring.thy Fri Apr 17 11:52:36 2015 +0200
@@ -143,6 +143,7 @@
lemmas finsum_Suc = add.finprod_Suc
lemmas finsum_Suc2 = add.finprod_Suc2
lemmas finsum_add = add.finprod_mult
+lemmas finsum_infinite = add.finprod_infinite
lemmas finsum_cong = add.finprod_cong
text {*Usually, if this rule causes a failed congruence proof error,
@@ -680,22 +681,14 @@
qed
lemma (in ring_hom_cring) hom_finsum [simp]:
- "[| finite A; f \<in> A -> carrier R |] ==>
+ "f \<in> A -> carrier R ==>
h (finsum R f A) = finsum S (h o f) A"
-proof (induct set: finite)
- case empty then show ?case by simp
-next
- case insert then show ?case by (simp add: Pi_def)
-qed
+ by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
lemma (in ring_hom_cring) hom_finprod:
- "[| finite A; f \<in> A -> carrier R |] ==>
+ "f \<in> A -> carrier R ==>
h (finprod R f A) = finprod S (h o f) A"
-proof (induct set: finite)
- case empty then show ?case by simp
-next
- case insert then show ?case by (simp add: Pi_def)
-qed
+ by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
declare ring_hom_cring.hom_finprod [simp]
--- a/src/HOL/Algebra/UnivPoly.thy Fri Apr 17 09:56:12 2015 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Fri Apr 17 11:52:36 2015 +0200
@@ -1208,13 +1208,9 @@
maybe it is not that necessary.*}
lemma (in ring_hom_ring) hom_finsum [simp]:
- "[| finite A; f \<in> A -> carrier R |] ==>
+ "f \<in> A -> carrier R ==>
h (finsum R f A) = finsum S (h o f) A"
-proof (induct set: finite)
- case empty then show ?case by simp
-next
- case insert then show ?case by (simp add: Pi_def)
-qed
+ by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
context UP_pre_univ_prop
begin