# HG changeset patch
# User huffman
# Date 1273640141 25200
# Node ID ce939b5fd77b056f755597635fa455cba72b0a17
# Parent  99745a4b9cc98e818a800186794a53096656c198
speed up some proofs, fixing linarith_split_limit warnings

diff -r 99745a4b9cc9 -r ce939b5fd77b src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Tue May 11 19:38:16 2010 -0700
+++ b/src/HOL/Library/Char_nat.thy	Tue May 11 21:55:41 2010 -0700
@@ -51,7 +51,7 @@
 
 lemma nibble_of_nat_norm:
   "nibble_of_nat (n mod 16) = nibble_of_nat n"
-  unfolding nibble_of_nat_def Let_def by auto
+  unfolding nibble_of_nat_def mod_mod_trivial ..
 
 lemmas [code] = nibble_of_nat_norm [symmetric]
 
@@ -72,7 +72,7 @@
   "nibble_of_nat 13 = NibbleD"
   "nibble_of_nat 14 = NibbleE"
   "nibble_of_nat 15 = NibbleF"
-  unfolding nibble_of_nat_def Let_def by auto
+  unfolding nibble_of_nat_def by auto
 
 lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
   [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
@@ -83,15 +83,15 @@
 lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16"
 proof -
   have nibble_nat_enum:
-    "n mod 16 \<in> {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15}"
+    "n mod 16 \<in> {15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0}"
   proof -
     have set_unfold: "\<And>n. {0..Suc n} = insert (Suc n) {0..n}" by auto
     have "(n\<Colon>nat) mod 16 \<in> {0..Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
       (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))}" by simp
     from this [simplified set_unfold atLeastAtMost_singleton]
-    show ?thesis by auto
+    show ?thesis by (simp add: numeral_2_eq_2 [symmetric])
   qed
-  then show ?thesis unfolding nibble_of_nat_def Let_def
+  then show ?thesis unfolding nibble_of_nat_def
   by auto
 qed