equal
deleted
inserted
replaced
10 begin |
10 begin |
11 |
11 |
12 text \<open>Bitwise logical operators\<close> |
12 text \<open>Bitwise logical operators\<close> |
13 |
13 |
14 spark_proof_functions |
14 spark_proof_functions |
15 bit__and (integer, integer) : integer = "(AND)" |
15 bit__and (integer, integer) : integer = Bit_Operations.and |
16 bit__or (integer, integer) : integer = "(OR)" |
16 bit__or (integer, integer) : integer = Bit_Operations.or |
17 bit__xor (integer, integer) : integer = "(XOR)" |
17 bit__xor (integer, integer) : integer = Bit_Operations.xor |
18 |
18 |
19 lemmas [simp] = |
19 lemmas [simp] = |
20 OR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified] |
20 OR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified] |
21 OR_upper [of _ 8, simplified] |
21 OR_upper [of _ 8, simplified] |
22 OR_upper [of _ 16, simplified zle_diff1_eq [symmetric], simplified] |
22 OR_upper [of _ 16, simplified zle_diff1_eq [symmetric], simplified] |