(* Title: HOL/ex/Adder.thy ID: $Id: Adder.thy,v 1.5 2005/09/14 20:08:08 wenzelm Exp $ Author: Sergey Tverdyshev (Universitaet des Saarlandes) *) header {* Implementation of carry chain incrementor and adder *} theory Adder imports Main Word begin lemma [simp]: "bv_to_nat [b] = bitval b" by (simp add: bv_to_nat_helper) lemma bv_to_nat_helper': "bv ≠ [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)" by (cases bv,simp_all add: bv_to_nat_helper) constdefs half_adder :: "[bit,bit] => bit list" "half_adder a b == [a bitand b,a bitxor b]" lemma half_adder_correct: "bv_to_nat (half_adder a b) = bitval a + bitval b" apply (simp add: half_adder_def) apply (cases a, auto) apply (cases b, auto) done lemma [simp]: "length (half_adder a b) = 2" by (simp add: half_adder_def) constdefs full_adder :: "[bit,bit,bit] => bit list" "full_adder a b c == let x = a bitxor b in [a bitand b bitor c bitand x,x bitxor c]" lemma full_adder_correct: "bv_to_nat (full_adder a b c) = bitval a + bitval b + bitval c" apply (simp add: full_adder_def Let_def) apply (cases a, auto) apply (case_tac[!] b, auto) apply (case_tac[!] c, auto) done lemma [simp]: "length (full_adder a b c) = 2" by (simp add: full_adder_def Let_def) (*carry chain incrementor*) consts carry_chain_inc :: "[bit list,bit] => bit list" primrec "carry_chain_inc [] c = [c]" "carry_chain_inc (a#as) c = (let chain = carry_chain_inc as c in half_adder a (hd chain) @ tl chain)" lemma cci_nonnull: "carry_chain_inc as c ≠ []" by (cases as,auto simp add: Let_def half_adder_def) lemma cci_length [simp]: "length (carry_chain_inc as c) = length as + 1" by (induct as, simp_all add: Let_def) lemma cci_correct: "bv_to_nat (carry_chain_inc as c) = bv_to_nat as + bitval c" apply (induct as) apply (cases c,simp_all add: Let_def bv_to_nat_dist_append) apply (simp add: half_adder_correct bv_to_nat_helper' [OF cci_nonnull] ring_distrib bv_to_nat_helper) done consts carry_chain_adder :: "[bit list,bit list,bit] => bit list" primrec "carry_chain_adder [] bs c = [c]" "carry_chain_adder (a#as) bs c = (let chain = carry_chain_adder as (tl bs) c in full_adder a (hd bs) (hd chain) @ tl chain)" lemma cca_nonnull: "carry_chain_adder as bs c ≠ []" by (cases as,auto simp add: full_adder_def Let_def) lemma cca_length [rule_format]: "∀bs. length as = length bs --> length (carry_chain_adder as bs c) = Suc (length bs)" (is "?P as") proof (induct as,auto simp add: Let_def) fix as :: "bit list" fix xs :: "bit list" assume ind: "?P as" assume len: "Suc (length as) = length xs" thus "Suc (length (carry_chain_adder as (tl xs) c) - Suc 0) = length xs" proof (cases xs,simp_all) fix b bs assume [simp]: "xs = b # bs" assume "length as = length bs" with ind show "length (carry_chain_adder as bs c) - Suc 0 = length bs" by auto qed qed lemma cca_correct [rule_format]: "∀bs. length as = length bs --> bv_to_nat (carry_chain_adder as bs c) = bv_to_nat as + bv_to_nat bs + bitval c" (is "?P as") proof (induct as,auto simp add: Let_def) fix a :: bit fix as :: "bit list" fix xs :: "bit list" assume ind: "?P as" assume len: "Suc (length as) = length xs" 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" proof (cases xs,simp_all) fix b bs assume [simp]: "xs = b # bs" assume len: "length as = length bs" with ind have "bv_to_nat (carry_chain_adder as bs c) = bv_to_nat as + bv_to_nat bs + bitval c" by blast with len 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" 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) qed qed end
lemma
bv_to_nat [b] = bitval b
lemma bv_to_nat_helper':
bv ≠ [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)
lemma half_adder_correct:
bv_to_nat (half_adder a b) = bitval a + bitval b
lemma
length (half_adder a b) = 2
lemma full_adder_correct:
bv_to_nat (full_adder a b c) = bitval a + bitval b + bitval c
lemma
length (full_adder a b c) = 2
lemma cci_nonnull:
carry_chain_inc as c ≠ []
lemma cci_length:
length (carry_chain_inc as c) = length as + 1
lemma cci_correct:
bv_to_nat (carry_chain_inc as c) = bv_to_nat as + bitval c
lemma cca_nonnull:
carry_chain_adder as bs c ≠ []
lemma cca_length:
length as = length bs ==> length (carry_chain_adder as bs c) = Suc (length bs)
lemma cca_correct:
length as = length bs ==> bv_to_nat (carry_chain_adder as bs c) = bv_to_nat as + bv_to_nat bs + bitval c