# HG changeset patch
# User huffman
# Date 1181532005 -7200
# Node ID 2fe3345035c7388822d1c8479582bca0451c8b0b
# Parent  cdb027d0637edf3f88fcce86541fa0047400bf87
modify proofs to avoid referring to int::nat=>int

diff -r cdb027d0637e -r 2fe3345035c7 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Mon Jun 11 02:25:55 2007 +0200
+++ b/src/HOL/IntDef.thy	Mon Jun 11 05:20:05 2007 +0200
@@ -416,7 +416,7 @@
 lemma nat_zminus_int_of_nat [simp]: "nat (- (int_of_nat n)) = 0"
 by (simp add: int_of_nat_def minus nat Zero_int_def) 
 
-lemma zless_nat_eq_int_zless: "(m < nat z) = (int_of_nat m < z)"
+lemma zless_nat_eq_int_zless': "(m < nat z) = (int_of_nat m < z)"
 by (cases z, simp add: nat less int_of_nat_def, arith)
 
 
@@ -779,7 +779,7 @@
 apply (rule_tac x="y - Suc x" in exI, arith)
 done
 
-theorem int_cases':
+theorem int_cases' [case_names nonneg neg]:
      "[|!! n. z = int_of_nat n ==> P;  !! n. z =  - (int_of_nat (Suc n)) ==> P |] ==> P"
 apply (cases "z < 0", blast dest!: negD')
 apply (simp add: linorder_not_less del: of_nat_Suc)
@@ -954,37 +954,30 @@
 qed
 
 lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
-by (simp add: int_eq_of_nat)
+unfolding int_eq_of_nat by (rule of_int_of_nat_eq)
 
 lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
-  by (simp add: int_eq_of_nat of_nat_setsum)
+unfolding int_eq_of_nat by (rule of_nat_setsum)
 
 lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
-  by (simp add: int_eq_of_nat of_nat_setprod)
+unfolding int_eq_of_nat by (rule of_nat_setprod)
 
 text{*Now we replace the case analysis rule by a more conventional one:
 whether an integer is negative or not.*}
 
 lemma zless_iff_Suc_zadd:
     "(w < z) = (\<exists>n. z = w + int(Suc n))"
-apply (cases z, cases w)
-apply (auto simp add: le add int_def linorder_not_le [symmetric]) 
-apply (rename_tac a b c d) 
-apply (rule_tac x="a+d - Suc(c+b)" in exI) 
-apply arith
-done
+unfolding int_eq_of_nat by (rule zless_iff_Suc_zadd')
 
 lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
-apply (cases x)
-apply (auto simp add: le minus Zero_int_def int_def order_less_le) 
-apply (rule_tac x="y - Suc x" in exI, arith)
-done
+unfolding int_eq_of_nat by (rule negD')
 
 theorem int_cases [cases type: int, case_names nonneg neg]:
      "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
-apply (cases "z < 0", blast dest!: negD)
+unfolding int_eq_of_nat
+apply (cases "z < 0", blast dest!: negD')
 apply (simp add: linorder_not_less)
-apply (blast dest: nat_0_le [THEN sym])
+apply (blast dest: nat_0_le' [THEN sym])
 done
 
 theorem int_induct [induct type: int, case_names nonneg neg]:
diff -r cdb027d0637e -r 2fe3345035c7 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Mon Jun 11 02:25:55 2007 +0200
+++ b/src/HOL/IntDiv.thy	Mon Jun 11 05:20:05 2007 +0200
@@ -1327,10 +1327,10 @@
   done
 
 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
-  apply (rule_tac z=n in int_cases)
-  apply (auto simp add: dvd_int_iff) 
-  apply (rule_tac z=z in int_cases) 
-  apply (auto simp add: dvd_imp_le) 
+  apply (rule_tac z=n in int_cases')
+  apply (auto simp add: dvd_int_of_nat_iff)
+  apply (rule_tac z=z in int_cases')
+  apply (auto simp add: dvd_imp_le)
   done
 
 
diff -r cdb027d0637e -r 2fe3345035c7 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Mon Jun 11 02:25:55 2007 +0200
+++ b/src/HOL/NatBin.thy	Mon Jun 11 05:20:05 2007 +0200
@@ -58,29 +58,32 @@
 apply (case_tac "0 <= z'")
 apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV)
 apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
-apply (auto elim!: nonneg_eq_int)
+apply (auto elim!: nonneg_eq_int_of_nat)
 apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m div int m'")
+apply (subgoal_tac "0 <= int_of_nat m div int_of_nat m'")
  prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) 
-apply (rule inj_int [THEN injD], simp)
-apply (rule_tac r = "int (m mod m') " in quorem_div)
+apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
+apply (rule_tac r = "int_of_nat (m mod m') " in quorem_div)
  prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int 
-                 zmult_int)
+apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
+                 of_nat_add [symmetric] of_nat_mult [symmetric]
+            del: of_nat_add of_nat_mult)
 done
 
 (*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
 lemma nat_mod_distrib:
      "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
 apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
-apply (auto elim!: nonneg_eq_int)
+apply (auto elim!: nonneg_eq_int_of_nat)
 apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m mod int m'")
+apply (subgoal_tac "0 <= int_of_nat m mod int_of_nat m'")
  prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign) 
-apply (rule inj_int [THEN injD], simp)
-apply (rule_tac q = "int (m div m') " in quorem_mod)
+apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
+apply (rule_tac q = "int_of_nat (m div m') " in quorem_mod)
  prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int zmult_int)
+apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
+                 of_nat_add [symmetric] of_nat_mult [symmetric]
+            del: of_nat_add of_nat_mult)
 done
 
 text{*Suggested by Matthias Daum*}
@@ -100,6 +103,13 @@
 by (simp del: nat_number_of
 	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
 
+lemma int_of_nat_number_of [simp]:
+     "int_of_nat (number_of v) =  
+         (if neg (number_of v :: int) then 0  
+          else (number_of v :: int))"
+by (simp del: nat_number_of
+	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
+
 
 subsubsection{*Successor *}
 
diff -r cdb027d0637e -r 2fe3345035c7 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Mon Jun 11 02:25:55 2007 +0200
+++ b/src/HOL/Numeral.thy	Mon Jun 11 05:20:05 2007 +0200
@@ -457,14 +457,14 @@
 
 lemma odd_less_0:
   "(1 + z + z < 0) = (z < (0::int))";
-proof (cases z rule: int_cases)
+proof (cases z rule: int_cases')
   case (nonneg n)
   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
                              le_imp_0_less [THEN order_less_imp_le])  
 next
   case (neg n)
-  thus ?thesis by (simp del: int_Suc
-    add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
+  thus ?thesis by (simp del: of_nat_Suc of_nat_add
+    add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
 qed
 
 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}