# Theory Adder

Up to index of Isabelle/HOL/ex

theory Adder
imports Main Word
begin

    (*  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