equal
deleted
inserted
replaced
7 |
7 |
8 theory SPARK |
8 theory SPARK |
9 imports SPARK_Setup |
9 imports SPARK_Setup |
10 begin |
10 begin |
11 |
11 |
12 text {* Bitwise logical operators *} |
12 text \<open>Bitwise logical operators\<close> |
13 |
13 |
14 spark_proof_functions |
14 spark_proof_functions |
15 bit__and (integer, integer) : integer = "op AND" |
15 bit__and (integer, integer) : integer = "op AND" |
16 bit__or (integer, integer) : integer = "op OR" |
16 bit__or (integer, integer) : integer = "op OR" |
17 bit__xor (integer, integer) : integer = "op XOR" |
17 bit__xor (integer, integer) : integer = "op XOR" |
52 bit_not_spark_eq [where 'a=16, simplified] |
52 bit_not_spark_eq [where 'a=16, simplified] |
53 bit_not_spark_eq [where 'a=32, simplified] |
53 bit_not_spark_eq [where 'a=32, simplified] |
54 bit_not_spark_eq [where 'a=64, simplified] |
54 bit_not_spark_eq [where 'a=64, simplified] |
55 |
55 |
56 |
56 |
57 text {* Minimum and maximum *} |
57 text \<open>Minimum and maximum\<close> |
58 |
58 |
59 spark_proof_functions |
59 spark_proof_functions |
60 integer__min = "min :: int \<Rightarrow> int \<Rightarrow> int" |
60 integer__min = "min :: int \<Rightarrow> int \<Rightarrow> int" |
61 integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int" |
61 integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int" |
62 |
62 |