src/HOL/ex/Adder.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 23477 f4b83f03cac9
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
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 \<noteq> [] ==> 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 \<noteq> []"
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 \<noteq> []"
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 \<Longrightarrow>
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 \<Longrightarrow>
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