# HG changeset patch
# User huffman
# Date 1187632261 -7200
# Node ID 9a7a9b19e9251f9cef0bf53b9cab599a9cf754aa
# Parent  eda777a2785b4a186608b1cfa44ab0898d38923f
use overloaded bitwise operators at type int

diff -r eda777a2785b -r 9a7a9b19e925 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Mon Aug 20 19:14:18 2007 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Mon Aug 20 19:51:01 2007 +0200
@@ -440,7 +440,7 @@
 
 lemma bl_xor_aux_bin [rule_format] : "ALL v w bs cs. 
     app2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
-    bin_to_bl_aux n (int_xor v w) (app2 (%x y. x ~= y) bs cs)"
+    bin_to_bl_aux n (v XOR w) (app2 (%x y. x ~= y) bs cs)"
   apply (induct_tac n)
    apply safe
    apply simp
@@ -453,7 +453,7 @@
     
 lemma bl_or_aux_bin [rule_format] : "ALL v w bs cs. 
     app2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
-    bin_to_bl_aux n (int_or v w) (app2 (op | ) bs cs)" 
+    bin_to_bl_aux n (v OR w) (app2 (op | ) bs cs)" 
   apply (induct_tac n)
    apply safe
    apply simp
@@ -466,7 +466,7 @@
     
 lemma bl_and_aux_bin [rule_format] : "ALL v w bs cs. 
     app2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
-    bin_to_bl_aux n (int_and v w) (app2 (op & ) bs cs)" 
+    bin_to_bl_aux n (v AND w) (app2 (op & ) bs cs)" 
   apply (induct_tac n)
    apply safe
    apply simp
@@ -479,7 +479,7 @@
     
 lemma bl_not_aux_bin [rule_format] : 
   "ALL w cs. map Not (bin_to_bl_aux n w cs) = 
-    bin_to_bl_aux n (int_not w) (map Not cs)"
+    bin_to_bl_aux n (NOT w) (map Not cs)"
   apply (induct n)
    apply clarsimp
   apply clarsimp
diff -r eda777a2785b -r 9a7a9b19e925 src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Mon Aug 20 19:14:18 2007 +0200
+++ b/src/HOL/Word/BinOperations.thy	Mon Aug 20 19:51:01 2007 +0200
@@ -9,12 +9,27 @@
 
 header {* Bitwise Operations on Binary Integers *}
 
-theory BinOperations imports BinGeneral
+theory BinOperations imports BinGeneral BitSyntax
 
 begin
 
--- "bit-wise logical operations on the int type"
+subsection {* NOT, AND, OR, XOR *}
+
+text "bit-wise logical operations on the int type"
+
+instance int :: bit
+  int_not_def: "bitNOT \<equiv> bin_rec Numeral.Min Numeral.Pls 
+    (\<lambda>w b s. s BIT (NOT b))"
+  int_and_def: "bitAND \<equiv> bin_rec (\<lambda>x. Numeral.Pls) (\<lambda>y. y) 
+    (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
+  int_or_def: "bitOR \<equiv> bin_rec (\<lambda>x. x) (\<lambda>y. Numeral.Min) 
+    (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
+  int_xor_def: "bitXOR \<equiv> bin_rec (\<lambda>x. x) bitNOT 
+    (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
+  ..
+
 consts
+(*
   int_and :: "int => int => int"
   int_or :: "int => int => int"
   bit_not :: "bit => bit"
@@ -23,8 +38,10 @@
   bit_xor :: "bit => bit => bit"
   int_not :: "int => int"
   int_xor :: "int => int => int"
+*)
   bin_sc :: "nat => bit => int => int"
 
+(*
 primrec
   B0 : "bit_not bit.B0 = bit.B1"
   B1 : "bit_not bit.B1 = bit.B0"
@@ -40,13 +57,15 @@
 primrec
   B0 : "bit_and bit.B0 x = bit.B0"
   B1 : "bit_and bit.B1 x = x"
+*)
 
 primrec
   Z : "bin_sc 0 b w = bin_rest w BIT b"
   Suc :
     "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
 
-defs
+(*
+defs (overloaded)
   int_not_def : "int_not == bin_rec Numeral.Min Numeral.Pls 
     (%w b s. s BIT bit_not b)"
     int_and_def : "int_and == bin_rec (%x. Numeral.Pls) (%y. y) 
@@ -55,6 +74,7 @@
     (%w b s y. s (bin_rest y) BIT (bit_or b (bin_last y)))"
   int_xor_def : "int_xor == bin_rec (%x. x) int_not 
     (%w b s y. s (bin_rest y) BIT (bit_xor b (bin_last y)))"
+*)
 
 consts
   bin_to_bl :: "nat => int => bool list"
@@ -124,45 +144,45 @@
      
  
 lemma int_not_simps [simp]:
-  "int_not Numeral.Pls = Numeral.Min"
-  "int_not Numeral.Min = Numeral.Pls"
-  "int_not (w BIT b) = int_not w BIT bit_not b"
+  "NOT Numeral.Pls = Numeral.Min"
+  "NOT Numeral.Min = Numeral.Pls"
+  "NOT (w BIT b) = (NOT w) BIT (NOT b)"
   by (unfold int_not_def) (auto intro: bin_rec_simps)
 
 lemma bit_extra_simps [simp]: 
-  "bit_and x bit.B0 = bit.B0"
-  "bit_and x bit.B1 = x"
-  "bit_or x bit.B1 = bit.B1"
-  "bit_or x bit.B0 = x"
-  "bit_xor x bit.B1 = bit_not x"
-  "bit_xor x bit.B0 = x"
+  "x AND bit.B0 = bit.B0"
+  "x AND bit.B1 = x"
+  "x OR bit.B1 = bit.B1"
+  "x OR bit.B0 = x"
+  "x XOR bit.B1 = NOT x"
+  "x XOR bit.B0 = x"
   by (cases x, auto)+
 
 lemma bit_ops_comm: 
-  "bit_and x y = bit_and y x"
-  "bit_or x y = bit_or y x"
-  "bit_xor x y = bit_xor y x"
+  "(x::bit) AND y = y AND x"
+  "(x::bit) OR y = y OR x"
+  "(x::bit) XOR y = y XOR x"
   by (cases y, auto)+
 
 lemma bit_ops_same [simp]: 
-  "bit_and x x = x"
-  "bit_or x x = x"
-  "bit_xor x x = bit.B0"
+  "(x::bit) AND x = x"
+  "(x::bit) OR x = x"
+  "(x::bit) XOR x = bit.B0"
   by (cases x, auto)+
 
-lemma bit_not_not [simp]: "bit_not (bit_not x) = x"
+lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
   by (cases x) auto
 
 lemma int_xor_Pls [simp]: 
-  "int_xor Numeral.Pls x = x"
+  "Numeral.Pls XOR x = x"
   unfolding int_xor_def by (simp add: bin_rec_PM)
 
 lemma int_xor_Min [simp]: 
-  "int_xor Numeral.Min x = int_not x"
+  "Numeral.Min XOR x = NOT x"
   unfolding int_xor_def by (simp add: bin_rec_PM)
 
 lemma int_xor_Bits [simp]: 
-  "int_xor (x BIT b) (y BIT c) = int_xor x y BIT bit_xor b c"
+  "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
   apply (unfold int_xor_def)
   apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans])
     apply (rule ext, simp)
@@ -173,8 +193,8 @@
   done
 
 lemma int_xor_x_simps':
-  "int_xor w (Numeral.Pls BIT bit.B0) = w"
-  "int_xor w (Numeral.Min BIT bit.B1) = int_not w"
+  "w XOR (Numeral.Pls BIT bit.B0) = w"
+  "w XOR (Numeral.Min BIT bit.B1) = NOT w"
   apply (induct w rule: bin_induct)
        apply simp_all[4]
    apply (unfold int_xor_Bits)
@@ -184,20 +204,20 @@
 lemmas int_xor_extra_simps [simp] = int_xor_x_simps' [simplified arith_simps]
 
 lemma int_or_Pls [simp]: 
-  "int_or Numeral.Pls x = x"
+  "Numeral.Pls OR x = x"
   by (unfold int_or_def) (simp add: bin_rec_PM)
   
 lemma int_or_Min [simp]:
-  "int_or Numeral.Min x = Numeral.Min"
+  "Numeral.Min OR x = Numeral.Min"
   by (unfold int_or_def) (simp add: bin_rec_PM)
 
 lemma int_or_Bits [simp]: 
-  "int_or (x BIT b) (y BIT c) = int_or x y BIT bit_or b c"
+  "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
   unfolding int_or_def by (simp add: bin_rec_simps)
 
 lemma int_or_x_simps': 
-  "int_or w (Numeral.Pls BIT bit.B0) = w"
-  "int_or w (Numeral.Min BIT bit.B1) = Numeral.Min"
+  "w OR (Numeral.Pls BIT bit.B0) = w"
+  "w OR (Numeral.Min BIT bit.B1) = Numeral.Min"
   apply (induct w rule: bin_induct)
        apply simp_all[4]
    apply (unfold int_or_Bits)
@@ -208,20 +228,20 @@
 
 
 lemma int_and_Pls [simp]:
-  "int_and Numeral.Pls x = Numeral.Pls"
+  "Numeral.Pls AND x = Numeral.Pls"
   unfolding int_and_def by (simp add: bin_rec_PM)
 
-lemma  int_and_Min [simp]:
-  "int_and Numeral.Min x = x"
+lemma int_and_Min [simp]:
+  "Numeral.Min AND x = x"
   unfolding int_and_def by (simp add: bin_rec_PM)
 
 lemma int_and_Bits [simp]: 
-  "int_and (x BIT b) (y BIT c) = int_and x y BIT bit_and b c" 
+  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
   unfolding int_and_def by (simp add: bin_rec_simps)
 
 lemma int_and_x_simps': 
-  "int_and w (Numeral.Pls BIT bit.B0) = Numeral.Pls"
-  "int_and w (Numeral.Min BIT bit.B1) = w"
+  "w AND (Numeral.Pls BIT bit.B0) = Numeral.Pls"
+  "w AND (Numeral.Min BIT bit.B1) = w"
   apply (induct w rule: bin_induct)
        apply simp_all[4]
    apply (unfold int_and_Bits)
@@ -233,21 +253,21 @@
 (* commutativity of the above *)
 lemma bin_ops_comm:
   shows
-  int_and_comm: "!!y. int_and x y = int_and y x" and
-  int_or_comm:  "!!y. int_or x y = int_or y x" and
-  int_xor_comm: "!!y. int_xor x y = int_xor y x"
+  int_and_comm: "!!y::int. x AND y = y AND x" and
+  int_or_comm:  "!!y::int. x OR y = y OR x" and
+  int_xor_comm: "!!y::int. x XOR y = y XOR x"
   apply (induct x rule: bin_induct)
           apply simp_all[6]
     apply (case_tac y rule: bin_exhaust, simp add: bit_ops_comm)+
   done
 
 lemma bin_ops_same [simp]:
-  "int_and x x = x" 
-  "int_or x x = x" 
-  "int_xor x x = Numeral.Pls"
+  "(x::int) AND x = x" 
+  "(x::int) OR x = x" 
+  "(x::int) XOR x = Numeral.Pls"
   by (induct x rule: bin_induct) auto
 
-lemma int_not_not [simp]: "int_not (int_not x) = x"
+lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
   by (induct x rule: bin_induct) auto
 
 lemmas bin_log_esimps = 
@@ -375,7 +395,7 @@
 (* basic properties of logical (bit-wise) operations *)
 
 lemma bbw_ao_absorb: 
-  "!!y. int_and x (int_or y x) = x & int_or x (int_and y x) = x"
+  "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
   apply (induct x rule: bin_induct)
     apply auto 
    apply (case_tac [!] y rule: bin_exhaust)
@@ -385,9 +405,9 @@
   done
 
 lemma bbw_ao_absorbs_other:
-  "int_and x (int_or x y) = x \<and> int_or (int_and y x) x = x"
-  "int_and (int_or y x) x = x \<and> int_or x (int_and x y) = x"
-  "int_and (int_or x y) x = x \<and> int_or (int_and x y) x = x"
+  "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
+  "(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
+  "(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
   apply (auto simp: bbw_ao_absorb int_or_comm)  
       apply (subst int_or_comm)
     apply (simp add: bbw_ao_absorb)
@@ -397,12 +417,12 @@
   apply (subst int_and_comm)
   apply (simp add: bbw_ao_absorb)
   done
-  
+
 lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
 
 lemma int_xor_not:
-  "!!y. int_xor (int_not x) y = int_not (int_xor x y) & 
-        int_xor x (int_not y) = int_not (int_xor x y)"
+  "!!y::int. (NOT x) XOR y = NOT (x XOR y) & 
+        x XOR (NOT y) = NOT (x XOR y)"
   apply (induct x rule: bin_induct)
     apply auto
    apply (case_tac y rule: bin_exhaust, auto, 
@@ -410,9 +430,9 @@
   done
 
 lemma bbw_assocs': 
-  "!!y z. int_and (int_and x y) z = int_and x (int_and y z) & 
-          int_or (int_or x y) z = int_or x (int_or y z) & 
-          int_xor (int_xor x y) z = int_xor x (int_xor y z)"
+  "!!y z::int. (x AND y) AND z = x AND (y AND z) & 
+          (x OR y) OR z = x OR (y OR z) & 
+          (x XOR y) XOR z = x XOR (y XOR z)"
   apply (induct x rule: bin_induct)
     apply (auto simp: int_xor_not)
     apply (case_tac [!] y rule: bin_exhaust)
@@ -423,30 +443,30 @@
   done
 
 lemma int_and_assoc:
-  "int_and (int_and x y) z = int_and x (int_and y z)"
+  "(x AND y) AND (z::int) = x AND (y AND z)"
   by (simp add: bbw_assocs')
 
 lemma int_or_assoc:
-  "int_or (int_or x y) z = int_or x (int_or y z)"
+  "(x OR y) OR (z::int) = x OR (y OR z)"
   by (simp add: bbw_assocs')
 
 lemma int_xor_assoc:
-  "int_xor (int_xor x y) z = int_xor x (int_xor y z)"
+  "(x XOR y) XOR (z::int) = x XOR (y XOR z)"
   by (simp add: bbw_assocs')
 
 lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
 
 lemma bbw_lcs [simp]: 
-  "int_and y (int_and x z) = int_and x (int_and y z)"
-  "int_or y (int_or x z) = int_or x (int_or y z)"
-  "int_xor y (int_xor x z) = int_xor x (int_xor y z)" 
+  "(y::int) AND (x AND z) = x AND (y AND z)"
+  "(y::int) OR (x OR z) = x OR (y OR z)"
+  "(y::int) XOR (x XOR z) = x XOR (y XOR z)" 
   apply (auto simp: bbw_assocs [symmetric])
   apply (auto simp: bin_ops_comm)
   done
 
 lemma bbw_not_dist: 
-  "!!y. int_not (int_or x y) = int_and (int_not x) (int_not y)" 
-  "!!y. int_not (int_and x y) = int_or (int_not x) (int_not y)"
+  "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)" 
+  "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
   apply (induct x rule: bin_induct)
        apply auto
    apply (case_tac [!] y rule: bin_exhaust)
@@ -454,8 +474,8 @@
   done
 
 lemma bbw_oa_dist: 
-  "!!y z. int_or (int_and x y) z = 
-          int_and (int_or x z) (int_or y z)"
+  "!!y z::int. (x AND y) OR z = 
+          (x OR z) AND (y OR z)"
   apply (induct x rule: bin_induct)
     apply auto
   apply (case_tac y rule: bin_exhaust)
@@ -464,8 +484,8 @@
   done
 
 lemma bbw_ao_dist: 
-  "!!y z. int_and (int_or x y) z = 
-          int_or (int_and x z) (int_and y z)"
+  "!!y z::int. (x OR y) AND z = 
+          (x AND z) OR (y AND z)"
    apply (induct x rule: bin_induct)
     apply auto
   apply (case_tac y rule: bin_exhaust)
@@ -476,7 +496,7 @@
 declare bin_ops_comm [simp] bbw_assocs [simp] 
 
 lemma plus_and_or [rule_format]:
-  "ALL y. int_and x y + int_or x y = x + y"
+  "ALL y::int. (x AND y) + (x OR y) = x + y"
   apply (induct x rule: bin_induct)
     apply clarsimp
    apply clarsimp
@@ -490,7 +510,7 @@
   done
 
 lemma le_int_or:
-  "!!x.  bin_sign y = Numeral.Pls ==> x <= int_or x y"
+  "!!x.  bin_sign y = Numeral.Pls ==> x <= x OR y"
   apply (induct y rule: bin_induct)
     apply clarsimp
    apply clarsimp
@@ -582,10 +602,10 @@
   done
 
 lemma bin_nth_ops:
-  "!!x y. bin_nth (int_and x y) n = (bin_nth x n & bin_nth y n)" 
-  "!!x y. bin_nth (int_or x y) n = (bin_nth x n | bin_nth y n)"
-  "!!x y. bin_nth (int_xor x y) n = (bin_nth x n ~= bin_nth y n)" 
-  "!!x. bin_nth (int_not x) n = (~ bin_nth x n)"
+  "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)" 
+  "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
+  "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)" 
+  "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
   apply (induct n)
          apply safe
                          apply (case_tac [!] x rule: bin_exhaust)
@@ -615,7 +635,7 @@
 
 (* interaction between bit-wise and arithmetic *)
 (* good example of bin_induction *)
-lemma bin_add_not: "x + int_not x = Numeral.Min"
+lemma bin_add_not: "x + NOT x = Numeral.Min"
   apply (induct x rule: bin_induct)
     apply clarsimp
    apply clarsimp
@@ -624,8 +644,8 @@
 
 (* truncating results of bit-wise operations *)
 lemma bin_trunc_ao: 
-  "!!x y. int_and (bintrunc n x) (bintrunc n y) = bintrunc n (int_and x y)" 
-  "!!x y. int_or (bintrunc n x) (bintrunc n y) = bintrunc n (int_or x y)"
+  "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)" 
+  "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
   apply (induct n)
       apply auto
       apply (case_tac [!] x rule: bin_exhaust)
@@ -634,8 +654,8 @@
   done
 
 lemma bin_trunc_xor: 
-  "!!x y. bintrunc n (int_xor (bintrunc n x) (bintrunc n y)) = 
-          bintrunc n (int_xor x y)"
+  "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) = 
+          bintrunc n (x XOR y)"
   apply (induct n)
    apply auto
    apply (case_tac [!] x rule: bin_exhaust)
@@ -644,7 +664,7 @@
   done
 
 lemma bin_trunc_not: 
-  "!!x. bintrunc n (int_not (bintrunc n x)) = bintrunc n (int_not x)"
+  "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
   apply (induct n)
    apply auto
    apply (case_tac [!] x rule: bin_exhaust)
diff -r eda777a2785b -r 9a7a9b19e925 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Mon Aug 20 19:14:18 2007 +0200
+++ b/src/HOL/Word/WordBitwise.thy	Mon Aug 20 19:51:01 2007 +0200
@@ -29,11 +29,11 @@
 
 lemmas word_wi_log_defs = word_no_log_defs [unfolded word_no_wi]
 
-lemma uint_or: "uint (x OR y) = int_or (uint x) (uint y)"
+lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
   by (simp add: word_or_def word_no_wi [symmetric] int_number_of
                 bin_trunc_ao(2) [symmetric])
 
-lemma uint_and: "uint (x AND y) = int_and (uint x) (uint y)"
+lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"
   by (simp add: word_and_def int_number_of word_no_wi [symmetric]
                 bin_trunc_ao(1) [symmetric]) 
 
diff -r eda777a2785b -r 9a7a9b19e925 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Mon Aug 20 19:14:18 2007 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Mon Aug 20 19:51:01 2007 +0200
@@ -140,16 +140,16 @@
 
 defs (overloaded)
   word_and_def: 
-  "(a::'a::len0 word) AND b == word_of_int (int_and (uint a) (uint b))"
+  "(a::'a::len0 word) AND b == word_of_int (uint a AND uint b)"
 
   word_or_def:  
-  "(a::'a::len0 word) OR b == word_of_int (int_or (uint a) (uint b))"
+  "(a::'a::len0 word) OR b == word_of_int (uint a OR uint b)"
 
   word_xor_def: 
-  "(a::'a::len0 word) XOR b == word_of_int (int_xor (uint a) (uint b))"
+  "(a::'a::len0 word) XOR b == word_of_int (uint a XOR uint b)"
 
   word_not_def: 
-  "NOT (a::'a::len0 word) == word_of_int (int_not (uint a))"
+  "NOT (a::'a::len0 word) == word_of_int (NOT (uint a))"
 
   word_test_bit_def: 
   "test_bit (a::'a::len0 word) == bin_nth (uint a)"