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.21 -text{*By Jeremy Avigad*}
    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