separated bit operations on type bit from generic syntactic bit operations
authorhaftmann
Thu Oct 31 11:44:20 2013 +0100 (2013-10-31)
changeset 542249fda41a04c32
parent 54223 85705ba18add
child 54225 8a49a5a30284
separated bit operations on type bit from generic syntactic bit operations
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Word/Bit_Bit.thy
src/HOL/Word/Bit_Int.thy
src/HOL/Word/Bit_Operations.thy
src/HOL/Word/Word.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Word/Bit_Bit.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -0,0 +1,73 @@
     1.4 +(*  Title:      HOL/Word/Bit_Bit.thy
     1.5 +    Author:     Author: Brian Huffman, PSU and Gerwin Klein, NICTA
     1.6 +*)
     1.7 +
     1.8 +header {* Bit operations in \<Z>\<^sub>2*}
     1.9 +
    1.10 +theory Bit_Bit
    1.11 +imports Bit_Operations "~~/src/HOL/Library/Bit"
    1.12 +begin
    1.13 +
    1.14 +instantiation bit :: bit
    1.15 +begin
    1.16 +
    1.17 +primrec bitNOT_bit where
    1.18 +  "NOT 0 = (1::bit)"
    1.19 +  | "NOT 1 = (0::bit)"
    1.20 +
    1.21 +primrec bitAND_bit where
    1.22 +  "0 AND y = (0::bit)"
    1.23 +  | "1 AND y = (y::bit)"
    1.24 +
    1.25 +primrec bitOR_bit where
    1.26 +  "0 OR y = (y::bit)"
    1.27 +  | "1 OR y = (1::bit)"
    1.28 +
    1.29 +primrec bitXOR_bit where
    1.30 +  "0 XOR y = (y::bit)"
    1.31 +  | "1 XOR y = (NOT y :: bit)"
    1.32 +
    1.33 +instance  ..
    1.34 +
    1.35 +end
    1.36 +
    1.37 +lemmas bit_simps =
    1.38 +  bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
    1.39 +
    1.40 +lemma bit_extra_simps [simp]: 
    1.41 +  "x AND 0 = (0::bit)"
    1.42 +  "x AND 1 = (x::bit)"
    1.43 +  "x OR 1 = (1::bit)"
    1.44 +  "x OR 0 = (x::bit)"
    1.45 +  "x XOR 1 = NOT (x::bit)"
    1.46 +  "x XOR 0 = (x::bit)"
    1.47 +  by (cases x, auto)+
    1.48 +
    1.49 +lemma bit_ops_comm: 
    1.50 +  "(x::bit) AND y = y AND x"
    1.51 +  "(x::bit) OR y = y OR x"
    1.52 +  "(x::bit) XOR y = y XOR x"
    1.53 +  by (cases y, auto)+
    1.54 +
    1.55 +lemma bit_ops_same [simp]: 
    1.56 +  "(x::bit) AND x = x"
    1.57 +  "(x::bit) OR x = x"
    1.58 +  "(x::bit) XOR x = 0"
    1.59 +  by (cases x, auto)+
    1.60 +
    1.61 +lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
    1.62 +  by (cases x) auto
    1.63 +
    1.64 +lemma bit_or_def: "(b::bit) OR c = NOT (NOT b AND NOT c)"
    1.65 +  by (induct b, simp_all)
    1.66 +
    1.67 +lemma bit_xor_def: "(b::bit) XOR c = (b AND NOT c) OR (NOT b AND c)"
    1.68 +  by (induct b, simp_all)
    1.69 +
    1.70 +lemma bit_NOT_eq_1_iff [simp]: "NOT (b::bit) = 1 \<longleftrightarrow> b = 0"
    1.71 +  by (induct b, simp_all)
    1.72 +
    1.73 +lemma bit_AND_eq_1_iff [simp]: "(a::bit) AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
    1.74 +  by (induct a, simp_all)
    1.75 +
    1.76 +end
     2.1 --- a/src/HOL/Word/Bit_Int.thy	Thu Oct 31 11:44:20 2013 +0100
     2.2 +++ b/src/HOL/Word/Bit_Int.thy	Thu Oct 31 11:44:20 2013 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  header {* Bitwise Operations on Binary Integers *}
     2.5  
     2.6  theory Bit_Int
     2.7 -imports Bit_Representation Bit_Operations
     2.8 +imports Bit_Representation Bit_Bit
     2.9  begin
    2.10  
    2.11  subsection {* Logical operations *}
     3.1 --- a/src/HOL/Word/Bit_Operations.thy	Thu Oct 31 11:44:20 2013 +0100
     3.2 +++ b/src/HOL/Word/Bit_Operations.thy	Thu Oct 31 11:44:20 2013 +0100
     3.3 @@ -8,8 +8,6 @@
     3.4  imports "~~/src/HOL/Library/Bit"
     3.5  begin
     3.6  
     3.7 -subsection {* Abstract syntactic bit operations *}
     3.8 -
     3.9  class bit =
    3.10    fixes bitNOT :: "'a \<Rightarrow> 'a"       ("NOT _" [70] 71)
    3.11      and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
    3.12 @@ -37,69 +35,5 @@
    3.13  class bitss = bits +
    3.14    fixes msb      :: "'a \<Rightarrow> bool"
    3.15  
    3.16 -  
    3.17 -subsection {* Bitwise operations on @{typ bit} *}
    3.18 -
    3.19 -instantiation bit :: bit
    3.20 -begin
    3.21 -
    3.22 -primrec bitNOT_bit where
    3.23 -  "NOT 0 = (1::bit)"
    3.24 -  | "NOT 1 = (0::bit)"
    3.25 -
    3.26 -primrec bitAND_bit where
    3.27 -  "0 AND y = (0::bit)"
    3.28 -  | "1 AND y = (y::bit)"
    3.29 -
    3.30 -primrec bitOR_bit where
    3.31 -  "0 OR y = (y::bit)"
    3.32 -  | "1 OR y = (1::bit)"
    3.33 -
    3.34 -primrec bitXOR_bit where
    3.35 -  "0 XOR y = (y::bit)"
    3.36 -  | "1 XOR y = (NOT y :: bit)"
    3.37 -
    3.38 -instance  ..
    3.39 -
    3.40  end
    3.41  
    3.42 -lemmas bit_simps =
    3.43 -  bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
    3.44 -
    3.45 -lemma bit_extra_simps [simp]: 
    3.46 -  "x AND 0 = (0::bit)"
    3.47 -  "x AND 1 = (x::bit)"
    3.48 -  "x OR 1 = (1::bit)"
    3.49 -  "x OR 0 = (x::bit)"
    3.50 -  "x XOR 1 = NOT (x::bit)"
    3.51 -  "x XOR 0 = (x::bit)"
    3.52 -  by (cases x, auto)+
    3.53 -
    3.54 -lemma bit_ops_comm: 
    3.55 -  "(x::bit) AND y = y AND x"
    3.56 -  "(x::bit) OR y = y OR x"
    3.57 -  "(x::bit) XOR y = y XOR x"
    3.58 -  by (cases y, auto)+
    3.59 -
    3.60 -lemma bit_ops_same [simp]: 
    3.61 -  "(x::bit) AND x = x"
    3.62 -  "(x::bit) OR x = x"
    3.63 -  "(x::bit) XOR x = 0"
    3.64 -  by (cases x, auto)+
    3.65 -
    3.66 -lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
    3.67 -  by (cases x) auto
    3.68 -
    3.69 -lemma bit_or_def: "(b::bit) OR c = NOT (NOT b AND NOT c)"
    3.70 -  by (induct b, simp_all)
    3.71 -
    3.72 -lemma bit_xor_def: "(b::bit) XOR c = (b AND NOT c) OR (NOT b AND c)"
    3.73 -  by (induct b, simp_all)
    3.74 -
    3.75 -lemma bit_NOT_eq_1_iff [simp]: "NOT (b::bit) = 1 \<longleftrightarrow> b = 0"
    3.76 -  by (induct b, simp_all)
    3.77 -
    3.78 -lemma bit_AND_eq_1_iff [simp]: "(a::bit) AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
    3.79 -  by (induct a, simp_all)
    3.80 -
    3.81 -end
     4.1 --- a/src/HOL/Word/Word.thy	Thu Oct 31 11:44:20 2013 +0100
     4.2 +++ b/src/HOL/Word/Word.thy	Thu Oct 31 11:44:20 2013 +0100
     4.3 @@ -8,6 +8,7 @@
     4.4  imports
     4.5    Type_Length
     4.6    "~~/src/HOL/Library/Boolean_Algebra"
     4.7 +  Bit_Bit
     4.8    Bool_List_Representation
     4.9    Misc_Typedef
    4.10    Word_Miscellaneous