# HG changeset patch
# User wenzelm
# Date 1429273802 -7200
# Node ID 63194f9141b9920bba57285da5c0c0a362bd8caf
# Parent  3eaa39b3a0b7758f35fdd3fbad2521526a13f0fd# Parent  3eab4acaa035d88fd3e925082dd7a6b41606a985
merged;

diff -r 3eaa39b3a0b7 -r 63194f9141b9 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Fri Apr 17 13:01:09 2015 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Apr 17 14:30:02 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. *)
 
diff -r 3eaa39b3a0b7 -r 63194f9141b9 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Fri Apr 17 13:01:09 2015 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Fri Apr 17 14:30:02 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 -
diff -r 3eaa39b3a0b7 -r 63194f9141b9 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Fri Apr 17 13:01:09 2015 +0200
+++ b/src/HOL/Algebra/Ring.thy	Fri Apr 17 14:30:02 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]
 
diff -r 3eaa39b3a0b7 -r 63194f9141b9 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Apr 17 13:01:09 2015 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Apr 17 14:30:02 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