author huffman Tue, 11 May 2010 21:55:41 -0700 changeset 36843 ce939b5fd77b parent 36842 99745a4b9cc9 child 36848 7e6f334b294b child 36851 5135adb33157 child 36867 6c28c702ed22
speed up some proofs, fixing linarith_split_limit warnings
```--- 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
@@ -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
```