src/HOL/Algebra/IntRing.thy
changeset 28524 644b62cf678f
parent 28085 914183e229e9
child 28823 dcbef866c9e2
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Tue Oct 07 16:07:50 2008 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  qed
     1.5  
     1.6  interpretation int: comm_monoid ["\<Z>"]
     1.7 -  where "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
     1.8 +  where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
     1.9  proof -
    1.10    -- "Specification"
    1.11    show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
    1.12 @@ -128,7 +128,7 @@
    1.13    { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
    1.14    note mult = this
    1.15    have one: "one \<Z> = 1" by (simp add: int_ring_def)
    1.16 -  show "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
    1.17 +  show "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
    1.18    proof (cases "finite A")
    1.19      case True then show ?thesis proof induct
    1.20        case empty show ?case by (simp add: one)
    1.21 @@ -143,7 +143,7 @@
    1.22  interpretation int: abelian_monoid ["\<Z>"]
    1.23    where "zero \<Z> = 0"
    1.24      and "add \<Z> x y = x + y"
    1.25 -    and "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
    1.26 +    and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
    1.27  proof -
    1.28    -- "Specification"
    1.29    show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
    1.30 @@ -153,7 +153,7 @@
    1.31    { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
    1.32    note add = this
    1.33    show zero: "zero \<Z> = 0" by (simp add: int_ring_def)
    1.34 -  show "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
    1.35 +  show "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
    1.36    proof (cases "finite A")
    1.37      case True then show ?thesis proof induct
    1.38        case empty show ?case by (simp add: zero)