# HG changeset patch
# User paulson
# Date 1078496395 -3600
# Node ID 77017c49c0041b3c459f710b8bed2d68f545fb7f
# Parent  9e22eeccf1298cf07ffe319a0c0832e0ec083b4a
some new results

diff -r 9e22eeccf129 -r 77017c49c004 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Fri Mar 05 15:18:59 2004 +0100
+++ b/src/HOL/Integ/IntArith.thy	Fri Mar 05 15:19:55 2004 +0100
@@ -140,6 +140,10 @@
 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_ring,number_ring})"
 by (simp add: abs_if)
 
+lemma abs_power_minus_one [simp]:
+     "abs(-1 ^ n) = (1::'a::{ordered_ring,number_ring,ringpower})"
+by (simp add: power_abs)
+
 lemma of_int_number_of_eq:
      "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
 apply (induct v)
diff -r 9e22eeccf129 -r 77017c49c004 src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Fri Mar 05 15:18:59 2004 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy	Fri Mar 05 15:19:55 2004 +0100
@@ -87,10 +87,27 @@
 
 subsubsection{*Evens and Odds, for Mutilated Chess Board*}
 
-(*Case analysis on b<2*)
+text{*Lemmas for specialist use, NOT as default simprules*}
+lemma nat_mult_2: "2 * z = (z+z::nat)"
+proof -
+  have "2*z = (1 + 1)*z" by simp
+  also have "... = z+z" by (simp add: left_distrib)
+  finally show ?thesis .
+qed
+
+lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
+by (subst mult_commute, rule nat_mult_2)
+
+text{*Case analysis on @{term "n<2"}*}
 lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
 by arith
 
+lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
+by arith
+
+lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
+by (simp add: nat_mult_2 [symmetric])
+
 lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
 apply (subgoal_tac "m mod 2 < 2")
 apply (erule less_2_cases [THEN disjE])
@@ -206,6 +223,9 @@
      "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
 by (simp add: divide_inverse inverse_minus_eq)
 
+
+
+
 ML
 {*
 val divide_minus1 = thm "divide_minus1";
diff -r 9e22eeccf129 -r 77017c49c004 src/HOL/Integ/Parity.thy
--- a/src/HOL/Integ/Parity.thy	Fri Mar 05 15:18:59 2004 +0100
+++ b/src/HOL/Integ/Parity.thy	Fri Mar 05 15:19:55 2004 +0100
@@ -156,9 +156,12 @@
   apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym])
   done
 
-lemma even_nat_suc: "even (Suc x) = odd x"
+lemma even_nat_Suc: "even (Suc x) = odd x"
   by (simp add: even_nat_def)
 
+text{*Compatibility, in case Avigad uses this*}
+lemmas even_nat_suc = even_nat_Suc
+
 lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
   by (simp add: even_nat_def zpow_int)
 
@@ -166,7 +169,7 @@
   by (simp add: even_nat_def)
 
 lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] 
-  even_nat_zero even_nat_suc even_nat_product even_nat_sum even_nat_power
+  even_nat_zero even_nat_Suc even_nat_product even_nat_sum even_nat_power
 
 
 subsection {* Equivalent definitions *}
@@ -238,10 +241,12 @@
   apply (simp, simp add: power_Suc)
   done
 
-lemma neg_one_even_power: "even x ==> (-1::'a::{number_ring,ringpower})^x = 1"
+lemma neg_one_even_power [simp]:
+     "even x ==> (-1::'a::{number_ring,ringpower})^x = 1"
   by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption)
 
-lemma neg_one_odd_power: "odd x ==> (-1::'a::{number_ring,ringpower})^x = -1"
+lemma neg_one_odd_power [simp]:
+     "odd x ==> (-1::'a::{number_ring,ringpower})^x = -1"
   by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption)