modify proofs to avoid referring to int::nat=>int
authorhuffman
Mon Jun 11 05:20:05 2007 +0200 (2007-06-11)
changeset 233072fe3345035c7
parent 23306 cdb027d0637e
child 23308 95a01ddfb024
modify proofs to avoid referring to int::nat=>int
src/HOL/IntDef.thy
src/HOL/IntDiv.thy
src/HOL/NatBin.thy
src/HOL/Numeral.thy
     1.1 --- a/src/HOL/IntDef.thy	Mon Jun 11 02:25:55 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Mon Jun 11 05:20:05 2007 +0200
     1.3 @@ -416,7 +416,7 @@
     1.4  lemma nat_zminus_int_of_nat [simp]: "nat (- (int_of_nat n)) = 0"
     1.5  by (simp add: int_of_nat_def minus nat Zero_int_def) 
     1.6  
     1.7 -lemma zless_nat_eq_int_zless: "(m < nat z) = (int_of_nat m < z)"
     1.8 +lemma zless_nat_eq_int_zless': "(m < nat z) = (int_of_nat m < z)"
     1.9  by (cases z, simp add: nat less int_of_nat_def, arith)
    1.10  
    1.11  
    1.12 @@ -779,7 +779,7 @@
    1.13  apply (rule_tac x="y - Suc x" in exI, arith)
    1.14  done
    1.15  
    1.16 -theorem int_cases':
    1.17 +theorem int_cases' [case_names nonneg neg]:
    1.18       "[|!! n. z = int_of_nat n ==> P;  !! n. z =  - (int_of_nat (Suc n)) ==> P |] ==> P"
    1.19  apply (cases "z < 0", blast dest!: negD')
    1.20  apply (simp add: linorder_not_less del: of_nat_Suc)
    1.21 @@ -954,37 +954,30 @@
    1.22  qed
    1.23  
    1.24  lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
    1.25 -by (simp add: int_eq_of_nat)
    1.26 +unfolding int_eq_of_nat by (rule of_int_of_nat_eq)
    1.27  
    1.28  lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
    1.29 -  by (simp add: int_eq_of_nat of_nat_setsum)
    1.30 +unfolding int_eq_of_nat by (rule of_nat_setsum)
    1.31  
    1.32  lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
    1.33 -  by (simp add: int_eq_of_nat of_nat_setprod)
    1.34 +unfolding int_eq_of_nat by (rule of_nat_setprod)
    1.35  
    1.36  text{*Now we replace the case analysis rule by a more conventional one:
    1.37  whether an integer is negative or not.*}
    1.38  
    1.39  lemma zless_iff_Suc_zadd:
    1.40      "(w < z) = (\<exists>n. z = w + int(Suc n))"
    1.41 -apply (cases z, cases w)
    1.42 -apply (auto simp add: le add int_def linorder_not_le [symmetric]) 
    1.43 -apply (rename_tac a b c d) 
    1.44 -apply (rule_tac x="a+d - Suc(c+b)" in exI) 
    1.45 -apply arith
    1.46 -done
    1.47 +unfolding int_eq_of_nat by (rule zless_iff_Suc_zadd')
    1.48  
    1.49  lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
    1.50 -apply (cases x)
    1.51 -apply (auto simp add: le minus Zero_int_def int_def order_less_le) 
    1.52 -apply (rule_tac x="y - Suc x" in exI, arith)
    1.53 -done
    1.54 +unfolding int_eq_of_nat by (rule negD')
    1.55  
    1.56  theorem int_cases [cases type: int, case_names nonneg neg]:
    1.57       "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
    1.58 -apply (cases "z < 0", blast dest!: negD)
    1.59 +unfolding int_eq_of_nat
    1.60 +apply (cases "z < 0", blast dest!: negD')
    1.61  apply (simp add: linorder_not_less)
    1.62 -apply (blast dest: nat_0_le [THEN sym])
    1.63 +apply (blast dest: nat_0_le' [THEN sym])
    1.64  done
    1.65  
    1.66  theorem int_induct [induct type: int, case_names nonneg neg]:
     2.1 --- a/src/HOL/IntDiv.thy	Mon Jun 11 02:25:55 2007 +0200
     2.2 +++ b/src/HOL/IntDiv.thy	Mon Jun 11 05:20:05 2007 +0200
     2.3 @@ -1327,10 +1327,10 @@
     2.4    done
     2.5  
     2.6  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
     2.7 -  apply (rule_tac z=n in int_cases)
     2.8 -  apply (auto simp add: dvd_int_iff) 
     2.9 -  apply (rule_tac z=z in int_cases) 
    2.10 -  apply (auto simp add: dvd_imp_le) 
    2.11 +  apply (rule_tac z=n in int_cases')
    2.12 +  apply (auto simp add: dvd_int_of_nat_iff)
    2.13 +  apply (rule_tac z=z in int_cases')
    2.14 +  apply (auto simp add: dvd_imp_le)
    2.15    done
    2.16  
    2.17  
     3.1 --- a/src/HOL/NatBin.thy	Mon Jun 11 02:25:55 2007 +0200
     3.2 +++ b/src/HOL/NatBin.thy	Mon Jun 11 05:20:05 2007 +0200
     3.3 @@ -58,29 +58,32 @@
     3.4  apply (case_tac "0 <= z'")
     3.5  apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV)
     3.6  apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
     3.7 -apply (auto elim!: nonneg_eq_int)
     3.8 +apply (auto elim!: nonneg_eq_int_of_nat)
     3.9  apply (rename_tac m m')
    3.10 -apply (subgoal_tac "0 <= int m div int m'")
    3.11 +apply (subgoal_tac "0 <= int_of_nat m div int_of_nat m'")
    3.12   prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) 
    3.13 -apply (rule inj_int [THEN injD], simp)
    3.14 -apply (rule_tac r = "int (m mod m') " in quorem_div)
    3.15 +apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
    3.16 +apply (rule_tac r = "int_of_nat (m mod m') " in quorem_div)
    3.17   prefer 2 apply force
    3.18 -apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int 
    3.19 -                 zmult_int)
    3.20 +apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
    3.21 +                 of_nat_add [symmetric] of_nat_mult [symmetric]
    3.22 +            del: of_nat_add of_nat_mult)
    3.23  done
    3.24  
    3.25  (*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
    3.26  lemma nat_mod_distrib:
    3.27       "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
    3.28  apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
    3.29 -apply (auto elim!: nonneg_eq_int)
    3.30 +apply (auto elim!: nonneg_eq_int_of_nat)
    3.31  apply (rename_tac m m')
    3.32 -apply (subgoal_tac "0 <= int m mod int m'")
    3.33 +apply (subgoal_tac "0 <= int_of_nat m mod int_of_nat m'")
    3.34   prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign) 
    3.35 -apply (rule inj_int [THEN injD], simp)
    3.36 -apply (rule_tac q = "int (m div m') " in quorem_mod)
    3.37 +apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
    3.38 +apply (rule_tac q = "int_of_nat (m div m') " in quorem_mod)
    3.39   prefer 2 apply force
    3.40 -apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int zmult_int)
    3.41 +apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
    3.42 +                 of_nat_add [symmetric] of_nat_mult [symmetric]
    3.43 +            del: of_nat_add of_nat_mult)
    3.44  done
    3.45  
    3.46  text{*Suggested by Matthias Daum*}
    3.47 @@ -100,6 +103,13 @@
    3.48  by (simp del: nat_number_of
    3.49  	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
    3.50  
    3.51 +lemma int_of_nat_number_of [simp]:
    3.52 +     "int_of_nat (number_of v) =  
    3.53 +         (if neg (number_of v :: int) then 0  
    3.54 +          else (number_of v :: int))"
    3.55 +by (simp del: nat_number_of
    3.56 +	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
    3.57 +
    3.58  
    3.59  subsubsection{*Successor *}
    3.60  
     4.1 --- a/src/HOL/Numeral.thy	Mon Jun 11 02:25:55 2007 +0200
     4.2 +++ b/src/HOL/Numeral.thy	Mon Jun 11 05:20:05 2007 +0200
     4.3 @@ -457,14 +457,14 @@
     4.4  
     4.5  lemma odd_less_0:
     4.6    "(1 + z + z < 0) = (z < (0::int))";
     4.7 -proof (cases z rule: int_cases)
     4.8 +proof (cases z rule: int_cases')
     4.9    case (nonneg n)
    4.10    thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
    4.11                               le_imp_0_less [THEN order_less_imp_le])  
    4.12  next
    4.13    case (neg n)
    4.14 -  thus ?thesis by (simp del: int_Suc
    4.15 -    add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
    4.16 +  thus ?thesis by (simp del: of_nat_Suc of_nat_add
    4.17 +    add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
    4.18  qed
    4.19  
    4.20  text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}