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