move lemmas from Nat_Numeral to Int.thy and Num.thy
authorhuffman
Fri Mar 30 08:10:28 2012 +0200 (2012-03-30)
changeset 472079368aa814518
parent 47196 6012241abe93
child 47208 9a91b163bb71
move lemmas from Nat_Numeral to Int.thy and Num.thy
src/HOL/Int.thy
src/HOL/Nat_Numeral.thy
src/HOL/Num.thy
src/HOL/Tools/SMT/smt_normalize.ML
     1.1 --- a/src/HOL/Int.thy	Thu Mar 29 14:47:31 2012 +0200
     1.2 +++ b/src/HOL/Int.thy	Fri Mar 30 08:10:28 2012 +0200
     1.3 @@ -575,6 +575,10 @@
     1.4       "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
     1.5    by (cases z) auto
     1.6  
     1.7 +lemma nonneg_int_cases:
     1.8 +  assumes "0 \<le> k" obtains n where "k = int n"
     1.9 +  using assms by (cases k, simp, simp del: of_nat_Suc)
    1.10 +
    1.11  text{*Contributed by Brian Huffman*}
    1.12  theorem int_diff_cases:
    1.13    obtains (diff) m n where "z = int m - int n"
    1.14 @@ -888,7 +892,7 @@
    1.15  lemma nat_0 [simp]: "nat 0 = 0"
    1.16  by (simp add: nat_eq_iff)
    1.17  
    1.18 -lemma nat_1: "nat 1 = Suc 0"
    1.19 +lemma nat_1 [simp]: "nat 1 = Suc 0"
    1.20  by (subst nat_eq_iff, simp)
    1.21  
    1.22  lemma nat_2: "nat 2 = Suc (Suc 0)"
    1.23 @@ -896,7 +900,7 @@
    1.24  
    1.25  lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
    1.26  apply (insert zless_nat_conj [of 1 z])
    1.27 -apply (auto simp add: nat_1)
    1.28 +apply auto
    1.29  done
    1.30  
    1.31  text{*This simplifies expressions of the form @{term "int n = z"} where
    1.32 @@ -963,6 +967,41 @@
    1.33                        nat_mult_distrib_neg [symmetric] mult_less_0_iff)
    1.34  done
    1.35  
    1.36 +lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
    1.37 +apply (rule sym)
    1.38 +apply (simp add: nat_eq_iff)
    1.39 +done
    1.40 +
    1.41 +lemma diff_nat_eq_if:
    1.42 +     "nat z - nat z' =  
    1.43 +        (if z' < 0 then nat z   
    1.44 +         else let d = z-z' in     
    1.45 +              if d < 0 then 0 else nat d)"
    1.46 +by (simp add: Let_def nat_diff_distrib [symmetric])
    1.47 +
    1.48 +(* nat_diff_distrib has too-strong premises *)
    1.49 +lemma nat_diff_distrib': "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x - y) = nat x - nat y"
    1.50 +apply (rule int_int_eq [THEN iffD1], clarsimp)
    1.51 +apply (subst of_nat_diff)
    1.52 +apply (rule nat_mono, simp_all)
    1.53 +done
    1.54 +
    1.55 +lemma nat_numeral [simp, code_abbrev]:
    1.56 +  "nat (numeral k) = numeral k"
    1.57 +  by (simp add: nat_eq_iff)
    1.58 +
    1.59 +lemma nat_neg_numeral [simp]:
    1.60 +  "nat (neg_numeral k) = 0"
    1.61 +  by simp
    1.62 +
    1.63 +lemma diff_nat_numeral [simp]: 
    1.64 +  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
    1.65 +  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
    1.66 +
    1.67 +lemma nat_numeral_diff_1 [simp]:
    1.68 +  "numeral v - (1::nat) = nat (numeral v - 1)"
    1.69 +  using diff_nat_numeral [of v Num.One] by simp
    1.70 +
    1.71  
    1.72  subsection "Induction principles for int"
    1.73  
    1.74 @@ -1681,10 +1720,6 @@
    1.75    "Neg k < Neg l \<longleftrightarrow> l < k"
    1.76    by simp_all
    1.77  
    1.78 -lemma nat_numeral [simp, code_abbrev]:
    1.79 -  "nat (numeral k) = numeral k"
    1.80 -  by (simp add: nat_eq_iff)
    1.81 -
    1.82  lemma nat_code [code]:
    1.83    "nat (Int.Neg k) = 0"
    1.84    "nat 0 = 0"
    1.85 @@ -1729,6 +1764,7 @@
    1.86  lemmas int_0 = of_nat_0 [where 'a=int]
    1.87  lemmas int_1 = of_nat_1 [where 'a=int]
    1.88  lemmas int_Suc = of_nat_Suc [where 'a=int]
    1.89 +lemmas int_numeral = of_nat_numeral [where 'a=int]
    1.90  lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
    1.91  lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
    1.92  lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
    1.93 @@ -1744,4 +1780,3 @@
    1.94  lemmas zpower_int = int_power [symmetric]
    1.95  
    1.96  end
    1.97 -
     2.1 --- a/src/HOL/Nat_Numeral.thy	Thu Mar 29 14:47:31 2012 +0200
     2.2 +++ b/src/HOL/Nat_Numeral.thy	Fri Mar 30 08:10:28 2012 +0200
     2.3 @@ -9,69 +9,8 @@
     2.4  imports Int
     2.5  begin
     2.6  
     2.7 -subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
     2.8 -
     2.9 -declare nat_1 [simp]
    2.10 -
    2.11 -lemma nat_neg_numeral [simp]: "nat (neg_numeral w) = 0"
    2.12 -  by simp
    2.13 -
    2.14 -lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
    2.15 -  by simp
    2.16 -
    2.17 -
    2.18 -subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
    2.19 -
    2.20 -lemma int_numeral: "int (numeral v) = numeral v"
    2.21 -  by (rule of_nat_numeral) (* already simp *)
    2.22 -
    2.23 -lemma nonneg_int_cases:
    2.24 -  fixes k :: int assumes "0 \<le> k" obtains n where "k = of_nat n"
    2.25 -  using assms by (cases k, simp, simp)
    2.26 -
    2.27 -subsubsection{*Successor *}
    2.28 -
    2.29 -lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
    2.30 -apply (rule sym)
    2.31 -apply (simp add: nat_eq_iff)
    2.32 -done
    2.33 -
    2.34 -lemma Suc_nat_number_of_add:
    2.35 -  "Suc (numeral v + n) = numeral (v + Num.One) + n"
    2.36 -  by simp
    2.37 -
    2.38 -
    2.39 -subsubsection{*Subtraction *}
    2.40 -
    2.41 -lemma diff_nat_eq_if:
    2.42 -     "nat z - nat z' =  
    2.43 -        (if z' < 0 then nat z   
    2.44 -         else let d = z-z' in     
    2.45 -              if d < 0 then 0 else nat d)"
    2.46 -by (simp add: Let_def nat_diff_distrib [symmetric])
    2.47 -
    2.48 -(* Int.nat_diff_distrib has too-strong premises *)
    2.49 -lemma nat_diff_distrib': "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x - y) = nat x - nat y"
    2.50 -apply (rule int_int_eq [THEN iffD1], clarsimp)
    2.51 -apply (subst zdiff_int [symmetric])
    2.52 -apply (rule nat_mono, simp_all)
    2.53 -done
    2.54 -
    2.55 -lemma diff_nat_numeral [simp]: 
    2.56 -  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
    2.57 -  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
    2.58 -
    2.59 -lemma nat_numeral_diff_1 [simp]:
    2.60 -  "numeral v - (1::nat) = nat (numeral v - 1)"
    2.61 -  using diff_nat_numeral [of v Num.One] by simp
    2.62 -
    2.63 -
    2.64  subsection{*Comparisons*}
    2.65  
    2.66 -(*Maps #n to n for n = 1, 2*)
    2.67 -lemmas numerals = numeral_1_eq_1 [where 'a=nat] numeral_2_eq_2
    2.68 -
    2.69 -
    2.70  text{*Simprules for comparisons where common factors can be cancelled.*}
    2.71  lemmas zero_compare_simps =
    2.72      add_strict_increasing add_strict_increasing2 add_increasing
     3.1 --- a/src/HOL/Num.thy	Thu Mar 29 14:47:31 2012 +0200
     3.2 +++ b/src/HOL/Num.thy	Fri Mar 30 08:10:28 2012 +0200
     3.3 @@ -876,6 +876,16 @@
     3.4  lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
     3.5    by (simp add: nat_number(2-4))
     3.6  
     3.7 +lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
     3.8 +  by (simp only: numeral_One One_nat_def)
     3.9 +
    3.10 +lemma Suc_nat_number_of_add:
    3.11 +  "Suc (numeral v + n) = numeral (v + Num.One) + n"
    3.12 +  by simp
    3.13 +
    3.14 +(*Maps #n to n for n = 1, 2*)
    3.15 +lemmas numerals = numeral_One [where 'a=nat] numeral_2_eq_2
    3.16 +
    3.17  
    3.18  subsection {* Numeral equations as default simplification rules *}
    3.19  
     4.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 29 14:47:31 2012 +0200
     4.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 30 08:10:28 2012 +0200
     4.3 @@ -467,7 +467,7 @@
     4.4      let
     4.5        val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
     4.6        val ss = HOL_ss
     4.7 -        addsimps [@{thm Nat_Numeral.int_numeral}]
     4.8 +        addsimps [@{thm Int.int_numeral}]
     4.9        fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1       
    4.10      in Goal.norm_result (Goal.prove_internal [] eq tac) end
    4.11