# HG changeset patch
# User paulson
# Date 1088092288 -7200
# Node ID bc050f23c3f83a93a14968094224cafaac244ac2
# Parent  fb2141a9f8c07173a6a1e1f7b951a3d624a1ef06
tidied

diff -r fb2141a9f8c0 -r bc050f23c3f8 src/HOL/ex/Adder.thy
--- a/src/HOL/ex/Adder.thy	Wed Jun 23 14:44:22 2004 +0200
+++ b/src/HOL/ex/Adder.thy	Thu Jun 24 17:51:28 2004 +0200
@@ -30,9 +30,11 @@
 
 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]"
+  "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"
+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)
@@ -60,9 +62,9 @@
 
 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)
-  apply (subst bv_to_nat_dist_append,simp)
-  apply (simp add: half_adder_correct bv_to_nat_helper' [OF cci_nonnull] ring_distrib bv_to_nat_helper)
+  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
@@ -70,17 +72,21 @@
 
 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)"
+  "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)
 
-lemma cca_length [rule_format]: "\<forall>bs. length as = length bs --> length (carry_chain_adder as bs c) = length as + 1"
+lemma cca_length [rule_format]:
+     "\<forall>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: "\<forall>bs. length as = length bs --> length (carry_chain_adder as bs c) = Suc (length bs)"
+  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)
@@ -93,12 +99,16 @@
   qed
 qed
 
-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"
+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: "\<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"
+  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)