equal
deleted
inserted
replaced
1 (* Title: HOL/ex/Adder.thy |
1 (* Title: HOL/ex/Adder.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Sergey Tverdyshev (Universitaet des Saarlandes) |
3 Author: Sergey Tverdyshev (Universitaet des Saarlandes) |
4 |
|
5 Implementation of carry chain incrementor and adder. |
|
6 *) |
4 *) |
7 |
5 |
8 header{* Adder *} |
6 header {* Implementation of carry chain incrementor and adder *} |
9 |
7 |
10 theory Adder imports Main Word begin |
8 theory Adder imports Main Word begin |
11 |
9 |
12 lemma [simp]: "bv_to_nat [b] = bitval b" |
10 lemma [simp]: "bv_to_nat [b] = bitval b" |
13 by (simp add: bv_to_nat_helper) |
11 by (simp add: bv_to_nat_helper) |