author | huffman |
Sun, 24 Sep 2006 05:49:50 +0200 | |
changeset 20692 | 6df83a636e67 |
parent 20217 | 25b068a99d2b |
child 20811 | eccbfaf2bc0e |
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 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
13 |
lemma bv_to_nat_helper': "bv \<noteq> [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
14 |
by (cases bv,simp_all add: bv_to_nat_helper) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
15 |
|
19736 | 16 |
definition |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
17 |
half_adder :: "[bit,bit] => bit list" |
19736 | 18 |
"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
|
19 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
20 |
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
|
21 |
apply (simp add: half_adder_def) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
22 |
apply (cases a, auto) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
23 |
apply (cases b, auto) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
24 |
done |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
25 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
26 |
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
|
27 |
by (simp add: half_adder_def) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
28 |
|
19736 | 29 |
definition |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
30 |
full_adder :: "[bit,bit,bit] => bit list" |
19736 | 31 |
"full_adder a b c = |
32 |
(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
|
33 |
|
15002 | 34 |
lemma full_adder_correct: |
35 |
"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
|
36 |
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
|
37 |
apply (cases a, auto) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
38 |
apply (case_tac[!] b, auto) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
39 |
apply (case_tac[!] c, auto) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
40 |
done |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
41 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
42 |
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
|
43 |
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
|
44 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
45 |
(*carry chain incrementor*) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
46 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
47 |
consts |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
48 |
carry_chain_inc :: "[bit list,bit] => bit list" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
49 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
50 |
primrec |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
51 |
"carry_chain_inc [] c = [c]" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
52 |
"carry_chain_inc (a#as) c = (let chain = carry_chain_inc as c |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
53 |
in half_adder a (hd chain) @ tl chain)" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
54 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
55 |
lemma cci_nonnull: "carry_chain_inc as c \<noteq> []" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
56 |
by (cases as,auto simp add: Let_def half_adder_def) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
57 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
58 |
lemma cci_length [simp]: "length (carry_chain_inc as c) = length as + 1" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
59 |
by (induct as, simp_all add: Let_def) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
60 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
61 |
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
|
62 |
apply (induct as) |
15002 | 63 |
apply (cases c,simp_all add: Let_def bv_to_nat_dist_append) |
64 |
apply (simp add: half_adder_correct bv_to_nat_helper' [OF cci_nonnull] |
|
65 |
ring_distrib bv_to_nat_helper) |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
66 |
done |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
67 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
68 |
consts |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
69 |
carry_chain_adder :: "[bit list,bit list,bit] => bit list" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
70 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
71 |
primrec |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
72 |
"carry_chain_adder [] bs c = [c]" |
15002 | 73 |
"carry_chain_adder (a#as) bs c = |
74 |
(let chain = carry_chain_adder as (tl bs) c |
|
75 |
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
|
76 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
77 |
lemma cca_nonnull: "carry_chain_adder as bs c \<noteq> []" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
78 |
by (cases as,auto 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
|
79 |
|
15002 | 80 |
lemma cca_length [rule_format]: |
81 |
"\<forall>bs. length as = length bs --> |
|
82 |
length (carry_chain_adder as bs c) = Suc (length bs)" |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19736
diff
changeset
|
83 |
by (induct as,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 |
|
15002 | 85 |
lemma cca_correct [rule_format]: |
86 |
"\<forall>bs. length as = length bs --> |
|
87 |
bv_to_nat (carry_chain_adder as bs c) = |
|
88 |
bv_to_nat as + bv_to_nat bs + bitval c" |
|
89 |
(is "?P as") |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
90 |
proof (induct as,auto simp add: Let_def) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
91 |
fix a :: bit |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
92 |
fix as :: "bit list" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
93 |
fix xs :: "bit list" |
15002 | 94 |
assume ind: "?P as" |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
95 |
assume len: "Suc (length as) = length xs" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
96 |
thus "bv_to_nat (full_adder a (hd xs) (hd (carry_chain_adder as (tl xs) c)) @ tl (carry_chain_adder as (tl xs) c)) = bv_to_nat (a # as) + bv_to_nat xs + bitval c" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
97 |
proof (cases xs,simp_all) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
98 |
fix b bs |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
99 |
assume [simp]: "xs = b # bs" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
100 |
assume len: "length as = length bs" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
101 |
with ind |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
102 |
have "bv_to_nat (carry_chain_adder as bs c) = bv_to_nat as + bv_to_nat bs + bitval c" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
103 |
by blast |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
104 |
with len |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
105 |
show "bv_to_nat (full_adder a b (hd (carry_chain_adder as bs c)) @ tl (carry_chain_adder as bs c)) = bv_to_nat (a # as) + bv_to_nat (b # bs) + bitval c" |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
106 |
by (subst bv_to_nat_dist_append,simp add: full_adder_correct bv_to_nat_helper' [OF cca_nonnull] ring_distrib bv_to_nat_helper cca_length) |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
107 |
qed |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
108 |
qed |
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
109 |
|
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff
changeset
|
110 |
end |