src/HOL/ex/Adder.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17388 495c799df31d
child 19736 d8d0f8f51d69
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
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 \<noteq> [] ==> 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 \<noteq> []"
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 \<noteq> []"
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
     "\<forall>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
     "\<forall>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