author | wenzelm |
Mon, 16 Mar 2009 18:24:30 +0100 | |
changeset 30549 | d2d7874648bd |
parent 23477 | f4b83f03cac9 |
permissions | -rw-r--r-- |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/Adder.thy |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
2 |
ID: $Id$ |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
3 |
Author: Sergey Tverdyshev (Universitaet des Saarlandes) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
4 |
*) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
5 |
|
17388 | 6 |
header {* Implementation of carry chain incrementor and adder *} |
14569 | 7 |
|
16417 | 8 |
theory Adder imports Main Word begin |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
9 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
10 |
lemma [simp]: "bv_to_nat [b] = bitval b" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
11 |
by (simp add: bv_to_nat_helper) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
12 |
|
20811 | 13 |
lemma bv_to_nat_helper': |
14 |
"bv \<noteq> [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)" |
|
15 |
by (cases bv) (simp_all add: bv_to_nat_helper) |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
16 |
|
19736 | 17 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20811
diff
changeset
|
18 |
half_adder :: "[bit, bit] => bit list" where |
20811 | 19 |
"half_adder a b = [a bitand b, a bitxor b]" |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
20 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
21 |
lemma half_adder_correct: "bv_to_nat (half_adder a b) = bitval a + bitval b" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
22 |
apply (simp add: half_adder_def) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
23 |
apply (cases a, auto) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
24 |
apply (cases b, auto) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
25 |
done |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
26 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
27 |
lemma [simp]: "length (half_adder a b) = 2" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
28 |
by (simp add: half_adder_def) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
29 |
|
19736 | 30 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20811
diff
changeset
|
31 |
full_adder :: "[bit, bit, bit] => bit list" where |
19736 | 32 |
"full_adder a b c = |
20811 | 33 |
(let x = a bitxor b in [a bitand b bitor c bitand x, x bitxor c])" |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
34 |
|
15002 | 35 |
lemma full_adder_correct: |
20811 | 36 |
"bv_to_nat (full_adder a b c) = bitval a + bitval b + bitval c" |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
37 |
apply (simp add: full_adder_def Let_def) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
38 |
apply (cases a, auto) |
20811 | 39 |
apply (case_tac [!] b, auto) |
40 |
apply (case_tac [!] c, auto) |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
41 |
done |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
42 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
43 |
lemma [simp]: "length (full_adder a b c) = 2" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
44 |
by (simp add: full_adder_def Let_def) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
45 |
|
20811 | 46 |
|
47 |
subsection {* Carry chain incrementor *} |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
48 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
49 |
consts |
20811 | 50 |
carry_chain_inc :: "[bit list, bit] => bit list" |
51 |
primrec |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
52 |
"carry_chain_inc [] c = [c]" |
20811 | 53 |
"carry_chain_inc (a#as) c = |
54 |
(let chain = carry_chain_inc as c |
|
55 |
in half_adder a (hd chain) @ tl chain)" |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
56 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
57 |
lemma cci_nonnull: "carry_chain_inc as c \<noteq> []" |
20811 | 58 |
by (cases as) (auto simp add: Let_def half_adder_def) |
59 |
||
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
60 |
lemma cci_length [simp]: "length (carry_chain_inc as c) = length as + 1" |
20811 | 61 |
by (induct as) (simp_all add: Let_def) |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
62 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
63 |
lemma cci_correct: "bv_to_nat (carry_chain_inc as c) = bv_to_nat as + bitval c" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
64 |
apply (induct as) |
20811 | 65 |
apply (cases c, simp_all add: Let_def bv_to_nat_dist_append) |
15002 | 66 |
apply (simp add: half_adder_correct bv_to_nat_helper' [OF cci_nonnull] |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
21404
diff
changeset
|
67 |
ring_distribs bv_to_nat_helper) |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
68 |
done |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
69 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
70 |
consts |
20811 | 71 |
carry_chain_adder :: "[bit list, bit list, bit] => bit list" |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
72 |
primrec |
20811 | 73 |
"carry_chain_adder [] bs c = [c]" |
74 |
"carry_chain_adder (a # as) bs c = |
|
15002 | 75 |
(let chain = carry_chain_adder as (tl bs) c |
76 |
in full_adder a (hd bs) (hd chain) @ tl chain)" |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
77 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
78 |
lemma cca_nonnull: "carry_chain_adder as bs c \<noteq> []" |
20811 | 79 |
by (cases as) (auto simp add: full_adder_def Let_def) |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
80 |
|
20811 | 81 |
lemma cca_length: "length as = length bs \<Longrightarrow> |
82 |
length (carry_chain_adder as bs c) = Suc (length bs)" |
|
83 |
by (induct as arbitrary: bs) (auto simp add: Let_def) |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
84 |
|
20811 | 85 |
theorem cca_correct: |
86 |
"length as = length bs \<Longrightarrow> |
|
87 |
bv_to_nat (carry_chain_adder as bs c) = |
|
88 |
bv_to_nat as + bv_to_nat bs + bitval c" |
|
89 |
proof (induct as arbitrary: bs) |
|
90 |
case Nil |
|
91 |
then show ?case by simp |
|
92 |
next |
|
93 |
case (Cons a as xs) |
|
94 |
note ind = Cons.hyps |
|
95 |
from Cons.prems have len: "Suc (length as) = length xs" by simp |
|
96 |
show ?case |
|
97 |
proof (cases xs) |
|
98 |
case Nil |
|
99 |
with len show ?thesis by simp |
|
100 |
next |
|
101 |
case (Cons b bs) |
|
102 |
with len have len': "length as = length bs" by simp |
|
103 |
then have "bv_to_nat (carry_chain_adder as bs c) = bv_to_nat as + bv_to_nat bs + bitval c" |
|
104 |
by (rule ind) |
|
105 |
with len' and Cons |
|
106 |
show ?thesis |
|
107 |
apply (simp add: Let_def) |
|
108 |
apply (subst bv_to_nat_dist_append) |
|
109 |
apply (simp add: full_adder_correct bv_to_nat_helper' [OF cca_nonnull] |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
21404
diff
changeset
|
110 |
ring_distribs bv_to_nat_helper cca_length) |
20811 | 111 |
done |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
112 |
qed |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
113 |
qed |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
114 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
115 |
end |