src/HOL/Int.thy
changeset 47255 30a1692557b0
parent 47228 4f4d85c3516f
child 48044 fea6f3060b65
equal deleted inserted replaced
47244:a7f85074c169 47255:30a1692557b0
   988 
   988 
   989 lemma nat_numeral_diff_1 [simp]:
   989 lemma nat_numeral_diff_1 [simp]:
   990   "numeral v - (1::nat) = nat (numeral v - 1)"
   990   "numeral v - (1::nat) = nat (numeral v - 1)"
   991   using diff_nat_numeral [of v Num.One] by simp
   991   using diff_nat_numeral [of v Num.One] by simp
   992 
   992 
       
   993 lemmas nat_arith = diff_nat_numeral
       
   994 
   993 
   995 
   994 subsection "Induction principles for int"
   996 subsection "Induction principles for int"
   995 
   997 
   996 text{*Well-founded segments of the integers*}
   998 text{*Well-founded segments of the integers*}
   997 
   999 
  1754 lemmas int_Suc = of_nat_Suc [where 'a=int]
  1756 lemmas int_Suc = of_nat_Suc [where 'a=int]
  1755 lemmas int_numeral = of_nat_numeral [where 'a=int]
  1757 lemmas int_numeral = of_nat_numeral [where 'a=int]
  1756 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
  1758 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
  1757 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
  1759 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
  1758 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
  1760 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
       
  1761 lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
       
  1762 lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
  1759 
  1763 
  1760 lemma zpower_zpower:
  1764 lemma zpower_zpower:
  1761   "(x ^ y) ^ z = (x ^ (y * z)::int)"
  1765   "(x ^ y) ^ z = (x ^ (y * z)::int)"
  1762   by (rule power_mult [symmetric])
  1766   by (rule power_mult [symmetric])
  1763 
  1767