equal
deleted
inserted
replaced
11 |
11 |
12 datatype bit = B0 | B1 |
12 datatype bit = B0 | B1 |
13 |
13 |
14 definition |
14 definition |
15 Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where |
15 Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where |
16 [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k" |
16 "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k" |
17 |
17 |
18 lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w" |
18 lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w" |
19 unfolding Bit_def Bit0_def by simp |
19 unfolding Bit_def Bit0_def by simp |
20 |
20 |
21 lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w" |
21 lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w" |