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` skalberg@14494 ` 13` ```lemma bv_to_nat_helper': "bv \ [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)" ``` skalberg@14494 ` 14` ``` by (cases bv,simp_all add: bv_to_nat_helper) ``` skalberg@14494 ` 15` skalberg@14494 ` 16` ```constdefs ``` skalberg@14494 ` 17` ``` half_adder :: "[bit,bit] => bit list" ``` skalberg@14494 ` 18` ``` "half_adder a b == [a bitand b,a bitxor b]" ``` skalberg@14494 ` 19` skalberg@14494 ` 20` ```lemma half_adder_correct: "bv_to_nat (half_adder a b) = bitval a + bitval b" ``` skalberg@14494 ` 21` ``` apply (simp add: half_adder_def) ``` skalberg@14494 ` 22` ``` apply (cases a, auto) ``` skalberg@14494 ` 23` ``` apply (cases b, auto) ``` skalberg@14494 ` 24` ``` done ``` skalberg@14494 ` 25` skalberg@14494 ` 26` ```lemma [simp]: "length (half_adder a b) = 2" ``` skalberg@14494 ` 27` ``` by (simp add: half_adder_def) ``` skalberg@14494 ` 28` skalberg@14494 ` 29` ```constdefs ``` skalberg@14494 ` 30` ``` full_adder :: "[bit,bit,bit] => bit list" ``` paulson@15002 ` 31` ``` "full_adder a b c == ``` paulson@15002 ` 32` ``` let x = a bitxor b in [a bitand b bitor c bitand x,x bitxor c]" ``` skalberg@14494 ` 33` paulson@15002 ` 34` ```lemma full_adder_correct: ``` paulson@15002 ` 35` ``` "bv_to_nat (full_adder a b c) = bitval a + bitval b + bitval c" ``` skalberg@14494 ` 36` ``` apply (simp add: full_adder_def Let_def) ``` skalberg@14494 ` 37` ``` apply (cases a, auto) ``` skalberg@14494 ` 38` ``` apply (case_tac[!] b, auto) ``` skalberg@14494 ` 39` ``` apply (case_tac[!] c, auto) ``` skalberg@14494 ` 40` ``` done ``` skalberg@14494 ` 41` skalberg@14494 ` 42` ```lemma [simp]: "length (full_adder a b c) = 2" ``` skalberg@14494 ` 43` ``` by (simp add: full_adder_def Let_def) ``` skalberg@14494 ` 44` skalberg@14494 ` 45` ```(*carry chain incrementor*) ``` skalberg@14494 ` 46` skalberg@14494 ` 47` ```consts ``` skalberg@14494 ` 48` ``` carry_chain_inc :: "[bit list,bit] => bit list" ``` skalberg@14494 ` 49` skalberg@14494 ` 50` ```primrec ``` skalberg@14494 ` 51` ``` "carry_chain_inc [] c = [c]" ``` skalberg@14494 ` 52` ``` "carry_chain_inc (a#as) c = (let chain = carry_chain_inc as c ``` skalberg@14494 ` 53` ``` in half_adder a (hd chain) @ tl chain)" ``` skalberg@14494 ` 54` skalberg@14494 ` 55` ```lemma cci_nonnull: "carry_chain_inc as c \ []" ``` skalberg@14494 ` 56` ``` by (cases as,auto simp add: Let_def half_adder_def) ``` skalberg@14494 ` 57` ``` ``` skalberg@14494 ` 58` ```lemma cci_length [simp]: "length (carry_chain_inc as c) = length as + 1" ``` skalberg@14494 ` 59` ``` by (induct as, simp_all add: Let_def) ``` skalberg@14494 ` 60` skalberg@14494 ` 61` ```lemma cci_correct: "bv_to_nat (carry_chain_inc as c) = bv_to_nat as + bitval c" ``` skalberg@14494 ` 62` ``` apply (induct as) ``` paulson@15002 ` 63` ``` apply (cases c,simp_all add: Let_def bv_to_nat_dist_append) ``` paulson@15002 ` 64` ``` apply (simp add: half_adder_correct bv_to_nat_helper' [OF cci_nonnull] ``` paulson@15002 ` 65` ``` ring_distrib bv_to_nat_helper) ``` skalberg@14494 ` 66` ``` done ``` skalberg@14494 ` 67` skalberg@14494 ` 68` ```consts ``` skalberg@14494 ` 69` ``` carry_chain_adder :: "[bit list,bit list,bit] => bit list" ``` skalberg@14494 ` 70` skalberg@14494 ` 71` ```primrec ``` skalberg@14494 ` 72` ``` "carry_chain_adder [] bs c = [c]" ``` paulson@15002 ` 73` ``` "carry_chain_adder (a#as) bs c = ``` paulson@15002 ` 74` ``` (let chain = carry_chain_adder as (tl bs) c ``` paulson@15002 ` 75` ``` in full_adder a (hd bs) (hd chain) @ tl chain)" ``` skalberg@14494 ` 76` skalberg@14494 ` 77` ```lemma cca_nonnull: "carry_chain_adder as bs c \ []" ``` skalberg@14494 ` 78` ``` by (cases as,auto simp add: full_adder_def Let_def) ``` skalberg@14494 ` 79` paulson@15002 ` 80` ```lemma cca_length [rule_format]: ``` paulson@15002 ` 81` ``` "\bs. length as = length bs --> ``` paulson@15002 ` 82` ``` length (carry_chain_adder as bs c) = Suc (length bs)" ``` paulson@15002 ` 83` ``` (is "?P as") ``` skalberg@14494 ` 84` ```proof (induct as,auto simp add: Let_def) ``` skalberg@14494 ` 85` ``` fix as :: "bit list" ``` skalberg@14494 ` 86` ``` fix xs :: "bit list" ``` paulson@15002 ` 87` ``` assume ind: "?P as" ``` skalberg@14494 ` 88` ``` assume len: "Suc (length as) = length xs" ``` skalberg@14494 ` 89` ``` thus "Suc (length (carry_chain_adder as (tl xs) c) - Suc 0) = length xs" ``` skalberg@14494 ` 90` ``` proof (cases xs,simp_all) ``` skalberg@14494 ` 91` ``` fix b bs ``` skalberg@14494 ` 92` ``` assume [simp]: "xs = b # bs" ``` skalberg@14494 ` 93` ``` assume "length as = length bs" ``` skalberg@14494 ` 94` ``` with ind ``` skalberg@14494 ` 95` ``` show "length (carry_chain_adder as bs c) - Suc 0 = length bs" ``` skalberg@14494 ` 96` ``` by auto ``` skalberg@14494 ` 97` ``` qed ``` skalberg@14494 ` 98` ```qed ``` skalberg@14494 ` 99` paulson@15002 ` 100` ```lemma cca_correct [rule_format]: ``` paulson@15002 ` 101` ``` "\bs. length as = length bs --> ``` paulson@15002 ` 102` ``` bv_to_nat (carry_chain_adder as bs c) = ``` paulson@15002 ` 103` ``` bv_to_nat as + bv_to_nat bs + bitval c" ``` paulson@15002 ` 104` ``` (is "?P as") ``` skalberg@14494 ` 105` ```proof (induct as,auto simp add: Let_def) ``` skalberg@14494 ` 106` ``` fix a :: bit ``` skalberg@14494 ` 107` ``` fix as :: "bit list" ``` skalberg@14494 ` 108` ``` fix xs :: "bit list" ``` paulson@15002 ` 109` ``` assume ind: "?P as" ``` skalberg@14494 ` 110` ``` assume len: "Suc (length as) = length xs" ``` skalberg@14494 ` 111` ``` 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" ``` skalberg@14494 ` 112` ``` proof (cases xs,simp_all) ``` skalberg@14494 ` 113` ``` fix b bs ``` skalberg@14494 ` 114` ``` assume [simp]: "xs = b # bs" ``` skalberg@14494 ` 115` ``` assume len: "length as = length bs" ``` skalberg@14494 ` 116` ``` with ind ``` skalberg@14494 ` 117` ``` have "bv_to_nat (carry_chain_adder as bs c) = bv_to_nat as + bv_to_nat bs + bitval c" ``` skalberg@14494 ` 118` ``` by blast ``` skalberg@14494 ` 119` ``` with len ``` skalberg@14494 ` 120` ``` 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" ``` skalberg@14494 ` 121` ``` 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) ``` skalberg@14494 ` 122` ``` qed ``` skalberg@14494 ` 123` ```qed ``` skalberg@14494 ` 124` skalberg@14494 ` 125` ```end ```