1.1 --- a/src/HOL/Word/BinOperations.thy Fri Oct 10 06:45:50 2008 +0200
1.2 +++ b/src/HOL/Word/BinOperations.thy Fri Oct 10 06:45:53 2008 +0200
1.3 @@ -21,19 +21,19 @@
1.4 begin
1.5
1.6 definition
1.7 - int_not_def [code func del]: "bitNOT = bin_rec Int.Min Int.Pls
1.8 + int_not_def [code del]: "bitNOT = bin_rec Int.Min Int.Pls
1.9 (\<lambda>w b s. s BIT (NOT b))"
1.10
1.11 definition
1.12 - int_and_def [code func del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y)
1.13 + int_and_def [code del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y)
1.14 (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
1.15
1.16 definition
1.17 - int_or_def [code func del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min)
1.18 + int_or_def [code del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min)
1.19 (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
1.20
1.21 definition
1.22 - int_xor_def [code func del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
1.23 + int_xor_def [code del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
1.24 (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
1.25
1.26 instance ..
1.27 @@ -48,13 +48,13 @@
1.28 "NOT (w BIT b) = (NOT w) BIT (NOT b)"
1.29 unfolding int_not_def by (simp_all add: bin_rec_simps)
1.30
1.31 -declare int_not_simps(1-4) [code func]
1.32 +declare int_not_simps(1-4) [code]
1.33
1.34 -lemma int_xor_Pls [simp, code func]:
1.35 +lemma int_xor_Pls [simp, code]:
1.36 "Int.Pls XOR x = x"
1.37 unfolding int_xor_def by (simp add: bin_rec_PM)
1.38
1.39 -lemma int_xor_Min [simp, code func]:
1.40 +lemma int_xor_Min [simp, code]:
1.41 "Int.Min XOR x = NOT x"
1.42 unfolding int_xor_def by (simp add: bin_rec_PM)
1.43
1.44 @@ -69,7 +69,7 @@
1.45 apply (simp add: int_not_simps [symmetric])
1.46 done
1.47
1.48 -lemma int_xor_Bits2 [simp, code func]:
1.49 +lemma int_xor_Bits2 [simp, code]:
1.50 "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
1.51 "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
1.52 "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
1.53 @@ -85,16 +85,16 @@
1.54 apply clarsimp+
1.55 done
1.56
1.57 -lemma int_xor_extra_simps [simp, code func]:
1.58 +lemma int_xor_extra_simps [simp, code]:
1.59 "w XOR Int.Pls = w"
1.60 "w XOR Int.Min = NOT w"
1.61 using int_xor_x_simps' by simp_all
1.62
1.63 -lemma int_or_Pls [simp, code func]:
1.64 +lemma int_or_Pls [simp, code]:
1.65 "Int.Pls OR x = x"
1.66 by (unfold int_or_def) (simp add: bin_rec_PM)
1.67
1.68 -lemma int_or_Min [simp, code func]:
1.69 +lemma int_or_Min [simp, code]:
1.70 "Int.Min OR x = Int.Min"
1.71 by (unfold int_or_def) (simp add: bin_rec_PM)
1.72
1.73 @@ -102,7 +102,7 @@
1.74 "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
1.75 unfolding int_or_def by (simp add: bin_rec_simps)
1.76
1.77 -lemma int_or_Bits2 [simp, code func]:
1.78 +lemma int_or_Bits2 [simp, code]:
1.79 "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
1.80 "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
1.81 "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
1.82 @@ -118,16 +118,16 @@
1.83 apply clarsimp+
1.84 done
1.85
1.86 -lemma int_or_extra_simps [simp, code func]:
1.87 +lemma int_or_extra_simps [simp, code]:
1.88 "w OR Int.Pls = w"
1.89 "w OR Int.Min = Int.Min"
1.90 using int_or_x_simps' by simp_all
1.91
1.92 -lemma int_and_Pls [simp, code func]:
1.93 +lemma int_and_Pls [simp, code]:
1.94 "Int.Pls AND x = Int.Pls"
1.95 unfolding int_and_def by (simp add: bin_rec_PM)
1.96
1.97 -lemma int_and_Min [simp, code func]:
1.98 +lemma int_and_Min [simp, code]:
1.99 "Int.Min AND x = x"
1.100 unfolding int_and_def by (simp add: bin_rec_PM)
1.101
1.102 @@ -135,7 +135,7 @@
1.103 "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"
1.104 unfolding int_and_def by (simp add: bin_rec_simps)
1.105
1.106 -lemma int_and_Bits2 [simp, code func]:
1.107 +lemma int_and_Bits2 [simp, code]:
1.108 "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
1.109 "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
1.110 "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
1.111 @@ -151,7 +151,7 @@
1.112 apply clarsimp+
1.113 done
1.114
1.115 -lemma int_and_extra_simps [simp, code func]:
1.116 +lemma int_and_extra_simps [simp, code]:
1.117 "w AND Int.Pls = Int.Pls"
1.118 "w AND Int.Min = w"
1.119 using int_and_x_simps' by simp_all