src/HOL/Word/Examples/WordExamples.thy

--- a/src/HOL/Word/Examples/WordExamples.thy	Mon Apr 03 21:17:47 2017 +0200
+++ b/src/HOL/Word/Examples/WordExamples.thy	Mon Apr 03 23:12:16 2017 +0200
@@ -1,13 +1,13 @@
-(* 
-  Authors: Gerwin Klein and Thomas Sewell, NICTA
+(*  Title:      HOL/Word/Examples/WordExamples.thy
+    Authors:    Gerwin Klein and Thomas Sewell, NICTA
 
-  Examples demonstrating and testing various word operations.
+Examples demonstrating and testing various word operations.
 *)
 
 section "Examples of word operations"
 
 theory WordExamples
-imports "../Word" "../WordBitwise"
+  imports "../Word" "../WordBitwise"
 begin
 
 type_synonym word32 = "32 word"
@@ -28,7 +28,7 @@
 
 text "number ring simps"
 
-lemma 
+lemma
   "27 + 11 = (38::'a::len word)"
   "27 + 11 = (6::5 word)"
   "7 * 3 = (21::'a::len word)"
@@ -40,7 +40,7 @@
 lemma "word_pred 2 = 1" by simp
 
 lemma "word_succ (- 3) = -2" by simp
-  
+
 lemma "23 < (27::8 word)" by simp
 lemma "23 \<le> (27::8 word)" by simp
 lemma "\<not> 23 < (27::2 word)" by simp
@@ -69,8 +69,10 @@
 lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp
 
 text "reducing goals to nat or int and arith:"
-lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by unat_arith
-lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by uint_arith
+lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
+  by unat_arith
+lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
+  by unat_arith
 
 text "bool lists"
 
@@ -111,7 +113,7 @@
 lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
 lemma "\<not> (1 :: 3 word) !! 2" by simp
 
-lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)" 
+lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
   by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
 
 lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
@@ -133,7 +135,7 @@
 lemma "\<not> msb (0::4 word)" by simp
 
 lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
-lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" 
+lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
   by simp
 
 lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
@@ -171,20 +173,24 @@
 
 text "more proofs using bitwise expansion"
 
-lemma "((x :: 10 word) AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
+lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
+  for x :: "10 word"
   by word_bitwise
 
-lemma "(((x :: 12 word) AND -8) >> 3) AND 7 = (x AND 56) >> 3"
+lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3"
+  for x :: "12 word"
   by word_bitwise
 
 text "some problems require further reasoning after bit expansion"
 
-lemma "x \<le> (42 :: 8 word) \<Longrightarrow> x \<le> 89"
+lemma "x \<le> 42 \<Longrightarrow> x \<le> 89"
+  for x :: "8 word"
   apply word_bitwise
   apply blast
   done
 
-lemma "((x :: word32) AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
+lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
+  for x :: word32
   apply word_bitwise
   apply clarsimp
   done
@@ -192,11 +198,10 @@
 text "operations like shifts by non-numerals will expose some internal list
  representations but may still be easy to solve"
 
-lemma shiftr_overflow:
-  "32 \<le> a \<Longrightarrow> (b::word32) >> a = 0"
-  apply (word_bitwise)
+lemma shiftr_overflow: "32 \<le> a \<Longrightarrow> b >> a = 0"
+  for b :: word32
+  apply word_bitwise
   apply simp
   done
 
-
 end