11 by (simp add: bv_to_nat_helper) |
11 by (simp add: bv_to_nat_helper) |
12 |
12 |
13 lemma bv_to_nat_helper': "bv \<noteq> [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)" |
13 lemma bv_to_nat_helper': "bv \<noteq> [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)" |
14 by (cases bv,simp_all add: bv_to_nat_helper) |
14 by (cases bv,simp_all add: bv_to_nat_helper) |
15 |
15 |
16 constdefs |
16 definition |
17 half_adder :: "[bit,bit] => bit list" |
17 half_adder :: "[bit,bit] => bit list" |
18 "half_adder a b == [a bitand b,a bitxor b]" |
18 "half_adder a b = [a bitand b,a bitxor b]" |
19 |
19 |
20 lemma half_adder_correct: "bv_to_nat (half_adder a b) = bitval a + bitval b" |
20 lemma half_adder_correct: "bv_to_nat (half_adder a b) = bitval a + bitval b" |
21 apply (simp add: half_adder_def) |
21 apply (simp add: half_adder_def) |
22 apply (cases a, auto) |
22 apply (cases a, auto) |
23 apply (cases b, auto) |
23 apply (cases b, auto) |
24 done |
24 done |
25 |
25 |
26 lemma [simp]: "length (half_adder a b) = 2" |
26 lemma [simp]: "length (half_adder a b) = 2" |
27 by (simp add: half_adder_def) |
27 by (simp add: half_adder_def) |
28 |
28 |
29 constdefs |
29 definition |
30 full_adder :: "[bit,bit,bit] => bit list" |
30 full_adder :: "[bit,bit,bit] => bit list" |
31 "full_adder a b c == |
31 "full_adder a b c = |
32 let x = a bitxor b in [a bitand b bitor c bitand x,x bitxor c]" |
32 (let x = a bitxor b in [a bitand b bitor c bitand x,x bitxor c])" |
33 |
33 |
34 lemma full_adder_correct: |
34 lemma full_adder_correct: |
35 "bv_to_nat (full_adder a b c) = bitval a + bitval b + bitval c" |
35 "bv_to_nat (full_adder a b c) = bitval a + bitval b + bitval c" |
36 apply (simp add: full_adder_def Let_def) |
36 apply (simp add: full_adder_def Let_def) |
37 apply (cases a, auto) |
37 apply (cases a, auto) |