# HG changeset patch
# User wenzelm
# Date 1159720170 -7200
# Node ID eccbfaf2bc0ed8e77a066f34ac76fb64095e4d18
# Parent  3377a830b727110b1a90082d9599e1be0c9f4a52
tuned proofs;

diff -r 3377a830b727 -r eccbfaf2bc0e src/HOL/ex/Adder.thy
--- 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
 
diff -r 3377a830b727 -r eccbfaf2bc0e src/HOL/ex/PER.thy
--- a/src/HOL/ex/PER.thy	Sun Oct 01 18:29:28 2006 +0200
+++ b/src/HOL/ex/PER.thy	Sun Oct 01 18:29:30 2006 +0200
@@ -49,10 +49,10 @@
   "domain = {x. x \<sim> x}"
 
 lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
-  by (unfold domain_def) blast
+  unfolding domain_def by blast
 
 lemma domainD [dest]: "x \<in> domain ==> x \<sim> x"
-  by (unfold domain_def) blast
+  unfolding domain_def by blast
 
 theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain"
 proof
@@ -75,18 +75,18 @@
 
 lemma partial_equiv_funI [intro?]:
     "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g"
-  by (unfold eqv_fun_def) blast
+  unfolding eqv_fun_def by blast
 
 lemma partial_equiv_funD [dest?]:
     "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"
-  by (unfold eqv_fun_def) blast
+  unfolding eqv_fun_def by blast
 
 text {*
   The class of partial equivalence relations is closed under function
   spaces (in \emph{both} argument positions).
 *}
 
-instance fun :: (partial_equiv, partial_equiv) partial_equiv
+instance "fun" :: (partial_equiv, partial_equiv) partial_equiv
 proof
   fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
   assume fg: "f \<sim> g"
@@ -94,9 +94,9 @@
   proof
     fix x y :: 'a
     assume x: "x \<in> domain" and y: "y \<in> domain"
-    assume "x \<sim> y" hence "y \<sim> x" ..
+    assume "x \<sim> y" then have "y \<sim> x" ..
     with fg y x have "f y \<sim> g x" ..
-    thus "g x \<sim> f y" ..
+    then show "g x \<sim> f y" ..
   qed
   assume gh: "g \<sim> h"
   show "f \<sim> h"
@@ -154,10 +154,10 @@
   by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
-  by (unfold quot_def) blast
+  unfolding quot_def by blast
 
 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
-  by (unfold quot_def) blast
+  unfolding quot_def by blast
 
 text {*
   \medskip Abstracted equivalence classes are the canonical
@@ -171,14 +171,14 @@
 theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
 proof (cases A)
   fix R assume R: "A = Abs_quot R"
-  assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
+  assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
   with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
-  thus ?thesis by (unfold eqv_class_def)
+  then show ?thesis by (unfold eqv_class_def)
 qed
 
-lemma quot_cases [case_names rep, cases type: quot]:
-    "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
-  by (insert quot_rep) blast
+lemma quot_cases [cases type: quot]:
+  obtains (rep) a where "A = \<lfloor>a\<rfloor>"
+  using quot_rep by blast
 
 
 subsection {* Equality on quotients *}
@@ -204,17 +204,17 @@
       finally show "a \<sim> x" .
     qed
   qed
-  thus ?thesis by (simp only: eqv_class_def)
+  then show ?thesis by (simp only: eqv_class_def)
 qed
 
 theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b"
 proof (unfold eqv_class_def)
   assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}"
-  hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)
-  moreover assume "a \<in> domain" hence "a \<sim> a" ..
+  then have "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)
+  moreover assume "a \<in> domain" then have "a \<sim> a" ..
   ultimately have "a \<in> {x. b \<sim> x}" by blast
-  hence "b \<sim> a" by blast
-  thus "a \<sim> b" ..
+  then have "b \<sim> a" by blast
+  then show "a \<sim> b" ..
 qed
 
 theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)"
@@ -223,10 +223,10 @@
 qed
 
 lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
-  by (insert eqv_class_eqI eqv_class_eqD') blast
+  using eqv_class_eqI eqv_class_eqD' by blast
 
 lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"
-  by (insert eqv_class_eqI eqv_class_eqD) blast
+  using eqv_class_eqI eqv_class_eqD by blast
 
 
 subsection {* Picking representing elements *}
@@ -242,8 +242,8 @@
   proof (rule someI2)
     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
-    hence "a \<sim> x" ..
-    thus "x \<sim> a" ..
+    then have "a \<sim> x" ..
+    then show "x \<sim> a" ..
   qed
 qed
 
@@ -255,8 +255,8 @@
 theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)"
 proof (cases A)
   fix a assume a: "A = \<lfloor>a\<rfloor>"
-  hence "pick A \<sim> a" by simp
-  hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp
+  then have "pick A \<sim> a" by simp
+  then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp
   with a show ?thesis by simp
 qed