# HG changeset patch
# User huffman
# Date 1325064643 -3600
# Node ID 96a5f44c22daa6b5a18c9bdc3193afea009e8e24
# Parent  ebbc2d5cd72065432f61cf0d376234ee2e53c139
replace 'lemmas' with explicit 'lemma'

diff -r ebbc2d5cd720 -r 96a5f44c22da src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Dec 28 07:58:17 2011 +0100
+++ b/src/HOL/Word/Word.thy	Wed Dec 28 10:30:43 2011 +0100
@@ -808,8 +808,11 @@
 
 lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
   unfolding uint_bl by (simp add : word_size)
-  
-lemmas uint_bl_bin [simp] = trans [OF bin_bl_bin word_ubin.norm_Rep]
+
+lemma uint_bl_bin:
+  fixes x :: "'a::len0 word"
+  shows "bl_to_bin (bin_to_bl (len_of TYPE('a)) (uint x)) = uint x"
+  by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
 
 (* FIXME: the next two lemmas should be unnecessary, because the lhs
 terms should never occur in practice *)
@@ -892,10 +895,21 @@
    word_of_int (sbintrunc (len_of TYPE('a) - Suc 0) (number_of w))"
   unfolding scast_def by simp
 
-lemmas source_size = source_size_def [unfolded Let_def word_size]
-lemmas target_size = target_size_def [unfolded Let_def word_size]
-lemmas is_down = is_down_def [unfolded source_size target_size]
-lemmas is_up = is_up_def [unfolded source_size target_size]
+lemma source_size: "source_size (c::'a::len0 word \<Rightarrow> _) = len_of TYPE('a)"
+  unfolding source_size_def word_size Let_def ..
+
+lemma target_size: "target_size (c::_ \<Rightarrow> 'b::len0 word) = len_of TYPE('b)"
+  unfolding target_size_def word_size Let_def ..
+
+lemma is_down:
+  fixes c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
+  shows "is_down c \<longleftrightarrow> len_of TYPE('b) \<le> len_of TYPE('a)"
+  unfolding is_down_def source_size target_size ..
+
+lemma is_up:
+  fixes c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
+  shows "is_up c \<longleftrightarrow> len_of TYPE('a) \<le> len_of TYPE('b)"
+  unfolding is_up_def source_size target_size ..
 
 lemmas is_up_down = trans [OF is_up is_down [symmetric]]
 
@@ -1039,7 +1053,7 @@
 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
 
 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
-lemmas word_log_bin_defs = word_log_defs
+lemmas word_log_bin_defs = word_log_defs (* FIXME: duplicate *)
 
 text {* Executable equality *}
 
@@ -1500,7 +1514,7 @@
 
 lemmas le_plus = le_plus' [rotated]
 
-lemmas le_minus = leD [THEN thin_rl, THEN le_minus']
+lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *)
 
 lemma word_plus_mono_right: 
   "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
@@ -2109,14 +2123,19 @@
 lemmas word_log_binary_defs = 
   word_and_def word_or_def word_xor_def
 
-lemmas word_no_log_defs [simp] = 
-  word_not_def  [where a="number_of a", 
-                 unfolded word_no_wi wils1, folded word_no_wi]
-  word_log_binary_defs [where a="number_of a" and b="number_of b",
-                        unfolded word_no_wi wils1, folded word_no_wi]
-  for a b
-
-lemmas word_wi_log_defs = word_no_log_defs [unfolded word_no_wi]
+lemma word_wi_log_defs:
+  "NOT word_of_int a = word_of_int (NOT a)"
+  "word_of_int a AND word_of_int b = word_of_int (a AND b)"
+  "word_of_int a OR word_of_int b = word_of_int (a OR b)"
+  "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"
+  unfolding word_not_def word_log_binary_defs wils1 by simp_all
+
+lemma word_no_log_defs [simp]:
+  "NOT number_of a = (number_of (NOT a) :: 'a::len0 word)"
+  "number_of a AND number_of b = (number_of (a AND b) :: 'a word)"
+  "number_of a OR number_of b = (number_of (a OR b) :: 'a word)"
+  "number_of a XOR number_of b = (number_of (a XOR b) :: 'a word)"
+  unfolding word_no_wi word_wi_log_defs by simp_all
 
 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
   by (simp add: word_or_def word_wi_log_defs word_ubin.eq_norm