--- a/src/HOL/ex/Adder.thy Sun Oct 01 18:29:28 2006 +0200
+++ b/src/HOL/ex/Adder.thy Sun Oct 01 18:29:30 2006 +0200
@@ -10,12 +10,13 @@
lemma [simp]: "bv_to_nat [b] = bitval b"
by (simp add: bv_to_nat_helper)
-lemma bv_to_nat_helper': "bv \<noteq> [] ==> 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)
+lemma bv_to_nat_helper':
+ "bv \<noteq> [] ==> 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)
definition
- half_adder :: "[bit,bit] => bit list"
- "half_adder a b = [a bitand b,a bitxor b]"
+ 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)
@@ -27,83 +28,87 @@
by (simp add: half_adder_def)
definition
- full_adder :: "[bit,bit,bit] => bit list"
+ 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])"
+ (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"
+ "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)
+ 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*)
+
+subsection {* Carry chain incrementor *}
consts
- carry_chain_inc :: "[bit list,bit] => bit list"
-
-primrec
+ 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)"
+ "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 \<noteq> []"
- by (cases as,auto simp add: Let_def half_adder_def)
-
+ 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)
+ 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 (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)
+ ring_distrib bv_to_nat_helper)
done
consts
- carry_chain_adder :: "[bit list,bit list,bit] => bit list"
-
+ carry_chain_adder :: "[bit list, bit list, bit] => bit list"
primrec
- "carry_chain_adder [] bs c = [c]"
- "carry_chain_adder (a#as) bs c =
+ "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 \<noteq> []"
- by (cases as,auto simp add: full_adder_def Let_def)
+ by (cases as) (auto simp add: full_adder_def Let_def)
-lemma cca_length [rule_format]:
- "\<forall>bs. length as = length bs -->
- length (carry_chain_adder as bs c) = Suc (length bs)"
- by (induct as,auto simp add: Let_def)
+lemma cca_length: "length as = length bs \<Longrightarrow>
+ length (carry_chain_adder as bs c) = Suc (length bs)"
+ by (induct as arbitrary: bs) (auto simp add: Let_def)
-lemma cca_correct [rule_format]:
- "\<forall>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)
+theorem cca_correct:
+ "length as = length bs \<Longrightarrow>
+ bv_to_nat (carry_chain_adder as bs c) =
+ bv_to_nat as + bv_to_nat bs + bitval c"
+proof (induct as arbitrary: bs)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a as xs)
+ note ind = Cons.hyps
+ from Cons.prems have len: "Suc (length as) = length xs" by simp
+ show ?case
+ proof (cases xs)
+ case Nil
+ with len show ?thesis by simp
+ next
+ case (Cons b bs)
+ with len have len': "length as = length bs" by simp
+ then have "bv_to_nat (carry_chain_adder as bs c) = bv_to_nat as + bv_to_nat bs + bitval c"
+ by (rule ind)
+ with len' and Cons
+ show ?thesis
+ apply (simp add: Let_def)
+ apply (subst bv_to_nat_dist_append)
+ apply (simp add: full_adder_correct bv_to_nat_helper' [OF cca_nonnull]
+ ring_distrib bv_to_nat_helper cca_length)
+ done
qed
qed