src/HOL/IntDef.thy
 changeset 23705 315c638d5856 parent 23477 f4b83f03cac9 child 23852 3736cdf9398b
```     1.1 --- a/src/HOL/IntDef.thy	Tue Jul 10 16:46:37 2007 +0200
1.2 +++ b/src/HOL/IntDef.thy	Tue Jul 10 17:30:43 2007 +0200
1.3 @@ -11,6 +11,7 @@
1.4  imports Equiv_Relations Nat
1.5  begin
1.6
1.7 +
1.8  text {* the equivalence relation underlying the integers *}
1.9
1.10  definition
1.11 @@ -622,52 +623,6 @@
1.12    by (rule Ints_cases) auto
1.13
1.14
1.15 -(* int (Suc n) = 1 + int n *)
1.16 -
1.17 -
1.18 -
1.19 -subsection{*More Properties of @{term setsum} and  @{term setprod}*}
1.20 -
1.22 -
1.23 -
1.24 -lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
1.25 -  apply (cases "finite A")
1.26 -  apply (erule finite_induct, auto)
1.27 -  done
1.28 -
1.29 -lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
1.30 -  apply (cases "finite A")
1.31 -  apply (erule finite_induct, auto)
1.32 -  done
1.33 -
1.34 -lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
1.35 -  apply (cases "finite A")
1.36 -  apply (erule finite_induct, auto simp add: of_nat_mult)
1.37 -  done
1.38 -
1.39 -lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
1.40 -  apply (cases "finite A")
1.41 -  apply (erule finite_induct, auto)
1.42 -  done
1.43 -
1.44 -lemma setprod_nonzero_nat:
1.45 -    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
1.46 -  by (rule setprod_nonzero, auto)
1.47 -
1.48 -lemma setprod_zero_eq_nat:
1.49 -    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
1.50 -  by (rule setprod_zero_eq, auto)
1.51 -
1.52 -lemma setprod_nonzero_int:
1.53 -    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
1.54 -  by (rule setprod_nonzero, auto)
1.55 -
1.56 -lemma setprod_zero_eq_int:
1.57 -    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
1.58 -  by (rule setprod_zero_eq, auto)
1.59 -
1.60 -
1.61  subsection {* Further properties *}
1.62
1.63  text{*Now we replace the case analysis rule by a more conventional one:
1.64 @@ -766,8 +721,6 @@
1.65  lemmas int_Suc = of_nat_Suc [where ?'a_1.0=int]
1.66  lemmas abs_int_eq = abs_of_nat [where 'a=int and n="?m"]
1.67  lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
1.68 -lemmas int_setsum = of_nat_setsum [where 'a=int]
1.69 -lemmas int_setprod = of_nat_setprod [where 'a=int]
1.70  lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
1.71  lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
1.72  lemmas int_eq_of_nat = TrueI
```