merged
authorhuffman
Fri, 30 Mar 2012 09:55:03 +0200
changeset 47212 c610b61c74a3
parent 47211 e1b0c8236ae4 (diff)
parent 47206 d3168cf76258 (current diff)
child 47213 eb5f812d15e2
child 47216 4d0878d54ca5
merged
--- a/src/HOL/Finite_Set.thy	Fri Mar 30 09:32:18 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Mar 30 09:55:03 2012 +0200
@@ -2084,6 +2084,9 @@
 lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
   unfolding UNIV_unit by simp
 
+lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2"
+  unfolding UNIV_bool by simp
+
 
 subsubsection {* Cardinality of image *}
 
--- a/src/HOL/Int.thy	Fri Mar 30 09:32:18 2012 +0200
+++ b/src/HOL/Int.thy	Fri Mar 30 09:55:03 2012 +0200
@@ -575,6 +575,10 @@
      "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   by (cases z) auto
 
+lemma nonneg_int_cases:
+  assumes "0 \<le> k" obtains n where "k = int n"
+  using assms by (cases k, simp, simp del: of_nat_Suc)
+
 text{*Contributed by Brian Huffman*}
 theorem int_diff_cases:
   obtains (diff) m n where "z = int m - int n"
@@ -888,7 +892,7 @@
 lemma nat_0 [simp]: "nat 0 = 0"
 by (simp add: nat_eq_iff)
 
-lemma nat_1: "nat 1 = Suc 0"
+lemma nat_1 [simp]: "nat 1 = Suc 0"
 by (subst nat_eq_iff, simp)
 
 lemma nat_2: "nat 2 = Suc (Suc 0)"
@@ -896,7 +900,7 @@
 
 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
 apply (insert zless_nat_conj [of 1 z])
-apply (auto simp add: nat_1)
+apply auto
 done
 
 text{*This simplifies expressions of the form @{term "int n = z"} where
@@ -963,6 +967,41 @@
                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
 done
 
+lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
+apply (rule sym)
+apply (simp add: nat_eq_iff)
+done
+
+lemma diff_nat_eq_if:
+     "nat z - nat z' =  
+        (if z' < 0 then nat z   
+         else let d = z-z' in     
+              if d < 0 then 0 else nat d)"
+by (simp add: Let_def nat_diff_distrib [symmetric])
+
+(* nat_diff_distrib has too-strong premises *)
+lemma nat_diff_distrib': "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x - y) = nat x - nat y"
+apply (rule int_int_eq [THEN iffD1], clarsimp)
+apply (subst of_nat_diff)
+apply (rule nat_mono, simp_all)
+done
+
+lemma nat_numeral [simp, code_abbrev]:
+  "nat (numeral k) = numeral k"
+  by (simp add: nat_eq_iff)
+
+lemma nat_neg_numeral [simp]:
+  "nat (neg_numeral k) = 0"
+  by simp
+
+lemma diff_nat_numeral [simp]: 
+  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
+  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
+
+lemma nat_numeral_diff_1 [simp]:
+  "numeral v - (1::nat) = nat (numeral v - 1)"
+  using diff_nat_numeral [of v Num.One] by simp
+
 
 subsection "Induction principles for int"
 
@@ -1681,10 +1720,6 @@
   "Neg k < Neg l \<longleftrightarrow> l < k"
   by simp_all
 
-lemma nat_numeral [simp, code_abbrev]:
-  "nat (numeral k) = numeral k"
-  by (simp add: nat_eq_iff)
-
 lemma nat_code [code]:
   "nat (Int.Neg k) = 0"
   "nat 0 = 0"
@@ -1729,6 +1764,7 @@
 lemmas int_0 = of_nat_0 [where 'a=int]
 lemmas int_1 = of_nat_1 [where 'a=int]
 lemmas int_Suc = of_nat_Suc [where 'a=int]
+lemmas int_numeral = of_nat_numeral [where 'a=int]
 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
@@ -1744,4 +1780,3 @@
 lemmas zpower_int = int_power [symmetric]
 
 end
-
--- a/src/HOL/Nat.thy	Fri Mar 30 09:32:18 2012 +0200
+++ b/src/HOL/Nat.thy	Fri Mar 30 09:55:03 2012 +0200
@@ -252,6 +252,12 @@
   apply (simp add:o_def)
   done
 
+lemma Suc_eq_plus1: "Suc n = n + 1"
+  unfolding One_nat_def by simp
+
+lemma Suc_eq_plus1_left: "Suc n = 1 + n"
+  unfolding One_nat_def by simp
+
 
 subsubsection {* Difference *}
 
--- a/src/HOL/Nat_Numeral.thy	Fri Mar 30 09:32:18 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy	Fri Mar 30 09:55:03 2012 +0200
@@ -9,69 +9,8 @@
 imports Int
 begin
 
-subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
-
-declare nat_1 [simp]
-
-lemma nat_neg_numeral [simp]: "nat (neg_numeral w) = 0"
-  by simp
-
-lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
-  by simp
-
-
-subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
-
-lemma int_numeral: "int (numeral v) = numeral v"
-  by (rule of_nat_numeral) (* already simp *)
-
-lemma nonneg_int_cases:
-  fixes k :: int assumes "0 \<le> k" obtains n where "k = of_nat n"
-  using assms by (cases k, simp, simp)
-
-subsubsection{*Successor *}
-
-lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
-apply (rule sym)
-apply (simp add: nat_eq_iff)
-done
-
-lemma Suc_nat_number_of_add:
-  "Suc (numeral v + n) = numeral (v + Num.One) + n"
-  by simp
-
-
-subsubsection{*Subtraction *}
-
-lemma diff_nat_eq_if:
-     "nat z - nat z' =  
-        (if z' < 0 then nat z   
-         else let d = z-z' in     
-              if d < 0 then 0 else nat d)"
-by (simp add: Let_def nat_diff_distrib [symmetric])
-
-(* Int.nat_diff_distrib has too-strong premises *)
-lemma nat_diff_distrib': "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x - y) = nat x - nat y"
-apply (rule int_int_eq [THEN iffD1], clarsimp)
-apply (subst zdiff_int [symmetric])
-apply (rule nat_mono, simp_all)
-done
-
-lemma diff_nat_numeral [simp]: 
-  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
-  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
-
-lemma nat_numeral_diff_1 [simp]:
-  "numeral v - (1::nat) = nat (numeral v - 1)"
-  using diff_nat_numeral [of v Num.One] by simp
-
-
 subsection{*Comparisons*}
 
-(*Maps #n to n for n = 1, 2*)
-lemmas numerals = numeral_1_eq_1 [where 'a=nat] numeral_2_eq_2
-
-
 text{*Simprules for comparisons where common factors can be cancelled.*}
 lemmas zero_compare_simps =
     add_strict_increasing add_strict_increasing2 add_increasing
@@ -92,12 +31,6 @@
 
 subsubsection{*Arith *}
 
-lemma Suc_eq_plus1: "Suc n = n + 1"
-  unfolding One_nat_def by simp
-
-lemma Suc_eq_plus1_left: "Suc n = 1 + n"
-  unfolding One_nat_def by simp
-
 (* These two can be useful when m = numeral... *)
 
 lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
@@ -109,45 +42,6 @@
 lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
   unfolding One_nat_def by (cases m) simp_all
 
-
-subsection{*Comparisons involving  @{term Suc} *}
-
-lemma eq_numeral_Suc [simp]: "numeral v = Suc n \<longleftrightarrow> nat (numeral v - 1) = n"
-  by (subst expand_Suc, simp only: nat.inject nat_numeral_diff_1)
-
-lemma Suc_eq_numeral [simp]: "Suc n = numeral v \<longleftrightarrow> n = nat (numeral v - 1)"
-  by (subst expand_Suc, simp only: nat.inject nat_numeral_diff_1)
-
-lemma less_numeral_Suc [simp]: "numeral v < Suc n \<longleftrightarrow> nat (numeral v - 1) < n"
-  by (subst expand_Suc, simp only: Suc_less_eq nat_numeral_diff_1)
-
-lemma less_Suc_numeral [simp]: "Suc n < numeral v \<longleftrightarrow> n < nat (numeral v - 1)"
-  by (subst expand_Suc, simp only: Suc_less_eq nat_numeral_diff_1)
-
-lemma le_numeral_Suc [simp]: "numeral v \<le> Suc n \<longleftrightarrow> nat (numeral v - 1) \<le> n"
-  by (subst expand_Suc, simp only: Suc_le_mono nat_numeral_diff_1)
-
-lemma le_Suc_numeral [simp]: "Suc n \<le> numeral v \<longleftrightarrow> n \<le> nat (numeral v - 1)"
-  by (subst expand_Suc, simp only: Suc_le_mono nat_numeral_diff_1)
-
-
-subsection{*Max and Min Combined with @{term Suc} *}
-
-lemma max_Suc_numeral [simp]:
-  "max (Suc n) (numeral v) = Suc (max n (nat (numeral v - 1)))"
-  by (subst expand_Suc, simp only: max_Suc_Suc nat_numeral_diff_1)
-
-lemma max_numeral_Suc [simp]:
-  "max (numeral v) (Suc n) = Suc (max (nat (numeral v - 1)) n)"
-  by (subst expand_Suc, simp only: max_Suc_Suc nat_numeral_diff_1)
-
-lemma min_Suc_numeral [simp]:
-  "min (Suc n) (numeral v) = Suc (min n (nat (numeral v - 1)))"
-  by (subst expand_Suc, simp only: min_Suc_Suc nat_numeral_diff_1)
-
-lemma min_numeral_Suc [simp]:
-  "min (numeral v) (Suc n) = Suc (min (nat (numeral v - 1)) n)"
-  by (subst expand_Suc, simp only: min_Suc_Suc nat_numeral_diff_1)
  
 subsection{*Literal arithmetic involving powers*}
 
@@ -238,9 +132,6 @@
 
 subsubsection{*Various Other Lemmas*}
 
-lemma card_UNIV_bool[simp]: "card (UNIV :: bool set) = 2"
-by(simp add: UNIV_bool)
-
 text {*Evens and Odds, for Mutilated Chess Board*}
 
 text{*Lemmas for specialist use, NOT as default simprules*}
--- a/src/HOL/Num.thy	Fri Mar 30 09:32:18 2012 +0200
+++ b/src/HOL/Num.thy	Fri Mar 30 09:55:03 2012 +0200
@@ -230,10 +230,10 @@
   by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult)
 
 
-subsection {* Numary numerals *}
+subsection {* Binary numerals *}
 
 text {*
-  We embed numary representations into a generic algebraic
+  We embed binary representations into a generic algebraic
   structure using @{text numeral}.
 *}
 
@@ -863,6 +863,12 @@
 lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)"
   unfolding numeral_plus_one [symmetric] by simp
 
+definition pred_numeral :: "num \<Rightarrow> nat"
+  where [code del]: "pred_numeral k = numeral k - 1"
+
+lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
+  unfolding pred_numeral_def by simp
+
 lemma nat_number:
   "1 = Suc 0"
   "numeral One = Suc 0"
@@ -870,12 +876,65 @@
   "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
   by (simp_all add: numeral.simps BitM_plus_one)
 
+lemma pred_numeral_simps [simp]:
+  "pred_numeral Num.One = 0"
+  "pred_numeral (Num.Bit0 k) = numeral (Num.BitM k)"
+  "pred_numeral (Num.Bit1 k) = numeral (Num.Bit0 k)"
+  unfolding pred_numeral_def nat_number
+  by (simp_all only: diff_Suc_Suc diff_0)
+
 lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
   by (simp add: nat_number(2-4))
 
 lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
   by (simp add: nat_number(2-4))
 
+lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
+  by (simp only: numeral_One One_nat_def)
+
+lemma Suc_nat_number_of_add:
+  "Suc (numeral v + n) = numeral (v + Num.One) + n"
+  by simp
+
+(*Maps #n to n for n = 1, 2*)
+lemmas numerals = numeral_One [where 'a=nat] numeral_2_eq_2
+
+text {* Comparisons involving @{term Suc}. *}
+
+lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n"
+  by (simp add: numeral_eq_Suc)
+
+lemma Suc_eq_numeral [simp]: "Suc n = numeral k \<longleftrightarrow> n = pred_numeral k"
+  by (simp add: numeral_eq_Suc)
+
+lemma less_numeral_Suc [simp]: "numeral k < Suc n \<longleftrightarrow> pred_numeral k < n"
+  by (simp add: numeral_eq_Suc)
+
+lemma less_Suc_numeral [simp]: "Suc n < numeral k \<longleftrightarrow> n < pred_numeral k"
+  by (simp add: numeral_eq_Suc)
+
+lemma le_numeral_Suc [simp]: "numeral k \<le> Suc n \<longleftrightarrow> pred_numeral k \<le> n"
+  by (simp add: numeral_eq_Suc)
+
+lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k"
+  by (simp add: numeral_eq_Suc)
+
+lemma max_Suc_numeral [simp]:
+  "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"
+  by (simp add: numeral_eq_Suc)
+
+lemma max_numeral_Suc [simp]:
+  "max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)"
+  by (simp add: numeral_eq_Suc)
+
+lemma min_Suc_numeral [simp]:
+  "min (Suc n) (numeral k) = Suc (min n (pred_numeral k))"
+  by (simp add: numeral_eq_Suc)
+
+lemma min_numeral_Suc [simp]:
+  "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
+  by (simp add: numeral_eq_Suc)
+
 
 subsection {* Numeral equations as default simplification rules *}
 
@@ -908,7 +967,7 @@
   "inverse Numeral1 = (Numeral1::'a::division_ring)"
   by simp
 
-text{*Theorem lists for the cancellation simprocs. The use of a numary
+text{*Theorem lists for the cancellation simprocs. The use of a binary
 numeral for 1 reduces the number of special cases.*}
 
 lemmas mult_1s =
--- a/src/HOL/Power.thy	Fri Mar 30 09:32:18 2012 +0200
+++ b/src/HOL/Power.thy	Fri Mar 30 09:55:03 2012 +0200
@@ -115,7 +115,7 @@
   by (induct n) (simp_all add: of_nat_mult)
 
 lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0"
-  by (cases "numeral k :: nat", simp_all)
+  by (simp add: numeral_eq_Suc)
 
 lemma zero_power2: "0\<twosuperior> = 0" (* delete? *)
   by (rule power_zero_numeral)
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 30 09:32:18 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 30 09:55:03 2012 +0200
@@ -467,7 +467,7 @@
     let
       val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
       val ss = HOL_ss
-        addsimps [@{thm Nat_Numeral.int_numeral}]
+        addsimps [@{thm Int.int_numeral}]
       fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1       
     in Goal.norm_result (Goal.prove_internal [] eq tac) end
 
--- a/src/HOL/Tools/int_arith.ML	Fri Mar 30 09:32:18 2012 +0200
+++ b/src/HOL/Tools/int_arith.ML	Fri Mar 30 09:55:03 2012 +0200
@@ -86,6 +86,7 @@
   Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
   #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
+      @ @{thms pred_numeral_simps}
       @ @{thms arith_special} @ @{thms int_arith_rules})
   #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
   #> Lin_Arith.set_number_of number_of