diff --git a/src/ZF/Bin.thy b/src/ZF/Bin.thy
--- a/src/ZF/Bin.thy
+++ b/src/ZF/Bin.thy
@@ -1,761 +1,763 @@
 (*  Title:      ZF/Bin.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
    The sign Pls stands for an infinite string of leading 0's.
    The sign Min stands for an infinite string of leading 1's.
 
 A number can have multiple representations, namely leading 0's with sign
 Pls and leading 1's with sign Min.  See twos-compl.ML/int_of_binary for
 the numerical interpretation.
 
 The representation expects that (m mod 2) is 0 or 1, even if m is negative;
 For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
 *)
 
 section\<open>Arithmetic on Binary Integers\<close>
 
 theory Bin
 imports Int Datatype
 begin
 
 consts  bin :: i
 datatype
   "bin" = Pls
         | Min
         | Bit ("w \<in> bin", "b \<in> bool")     (infixl \<open>BIT\<close> 90)
 
 consts
   integ_of  :: "i=>i"
   NCons     :: "[i,i]=>i"
   bin_succ  :: "i=>i"
   bin_pred  :: "i=>i"
   bin_minus :: "i=>i"
   bin_adder :: "i=>i"
   bin_mult  :: "[i,i]=>i"
 
 primrec
   integ_of_Pls:  "integ_of (Pls)     = $# 0"
   integ_of_Min:  "integ_of (Min)     = $-($#1)"
   integ_of_BIT:  "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)"
 
     (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
 
 primrec (*NCons adds a bit, suppressing leading 0s and 1s*)
   NCons_Pls: "NCons (Pls,b)     = cond(b,Pls BIT b,Pls)"
   NCons_Min: "NCons (Min,b)     = cond(b,Min,Min BIT b)"
   NCons_BIT: "NCons (w BIT c,b) = w BIT c BIT b"
 
 primrec (*successor.  If a BIT, can change a 0 to a 1 without recursion.*)
   bin_succ_Pls:  "bin_succ (Pls)     = Pls BIT 1"
   bin_succ_Min:  "bin_succ (Min)     = Pls"
   bin_succ_BIT:  "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
 
 primrec (*predecessor*)
   bin_pred_Pls:  "bin_pred (Pls)     = Min"
   bin_pred_Min:  "bin_pred (Min)     = Min BIT 0"
   bin_pred_BIT:  "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
 
 primrec (*unary negation*)
   bin_minus_Pls:
     "bin_minus (Pls)       = Pls"
   bin_minus_Min:
     "bin_minus (Min)       = Pls BIT 1"
   bin_minus_BIT:
     "bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)),
                                 bin_minus(w) BIT 0)"
 
 primrec (*sum*)
   bin_adder_Pls:
     "bin_adder (Pls)     = (\<lambda>w\<in>bin. w)"
   bin_adder_Min:
     "bin_adder (Min)     = (\<lambda>w\<in>bin. bin_pred(w))"
   bin_adder_BIT:
     "bin_adder (v BIT x) =
        (\<lambda>w\<in>bin.
          bin_case (v BIT x, bin_pred(v BIT x),
                    %w y. NCons(bin_adder (v) ` cond(x and y, bin_succ(w), w),
                                x xor y),
                    w))"
 
 (*The bin_case above replaces the following mutually recursive function:
 primrec
   "adding (v,x,Pls)     = v BIT x"
   "adding (v,x,Min)     = bin_pred(v BIT x)"
   "adding (v,x,w BIT y) = NCons(bin_adder (v, cond(x and y, bin_succ(w), w)),
                                 x xor y)"
 *)
 
 definition
   bin_add   :: "[i,i]=>i"  where
     "bin_add(v,w) == bin_adder(v)`w"
 
 
 primrec
   bin_mult_Pls:
     "bin_mult (Pls,w)     = Pls"
   bin_mult_Min:
     "bin_mult (Min,w)     = bin_minus(w)"
   bin_mult_BIT:
     "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
                                  NCons(bin_mult(v,w),0))"
 
 syntax
   "_Int0" :: i  (\<open>#()0\<close>)
   "_Int1" :: i  (\<open>#()1\<close>)
   "_Int2" :: i  (\<open>#()2\<close>)
   "_Neg_Int1" :: i  (\<open>#-()1\<close>)
   "_Neg_Int2" :: i  (\<open>#-()2\<close>)
 translations
   "#0" \<rightleftharpoons> "CONST integ_of(CONST Pls)"
   "#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)"
   "#2" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1 BIT 0)"
   "#-1" \<rightleftharpoons> "CONST integ_of(CONST Min)"
   "#-2" \<rightleftharpoons> "CONST integ_of(CONST Min BIT 0)"
 
 syntax
   "_Int" :: "num_token => i"  (\<open>#_\<close> 1000)
   "_Neg_Int" :: "num_token => i"  (\<open>#-_\<close> 1000)
 
 ML_file \<open>Tools/numeral_syntax.ML\<close>
 
 
 declare bin.intros [simp,TC]
 
 lemma NCons_Pls_0: "NCons(Pls,0) = Pls"
 by simp
 
 lemma NCons_Pls_1: "NCons(Pls,1) = Pls BIT 1"
 by simp
 
 lemma NCons_Min_0: "NCons(Min,0) = Min BIT 0"
 by simp
 
 lemma NCons_Min_1: "NCons(Min,1) = Min"
 by simp
 
 lemma NCons_BIT: "NCons(w BIT x,b) = w BIT x BIT b"
 by (simp add: bin.case_eqns)
 
 lemmas NCons_simps [simp] =
     NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
 
 
 
 (** Type checking **)
 
 lemma integ_of_type [TC]: "w \<in> bin ==> integ_of(w) \<in> int"
 apply (induct_tac "w")
 apply (simp_all add: bool_into_nat)
 done
 
 lemma NCons_type [TC]: "[| w \<in> bin; b \<in> bool |] ==> NCons(w,b) \<in> bin"
 by (induct_tac "w", auto)
 
 lemma bin_succ_type [TC]: "w \<in> bin ==> bin_succ(w) \<in> bin"
 by (induct_tac "w", auto)
 
 lemma bin_pred_type [TC]: "w \<in> bin ==> bin_pred(w) \<in> bin"
 by (induct_tac "w", auto)
 
 lemma bin_minus_type [TC]: "w \<in> bin ==> bin_minus(w) \<in> bin"
 by (induct_tac "w", auto)
 
 (*This proof is complicated by the mutual recursion*)
-lemma bin_add_type [rule_format,TC]:
+lemma bin_add_type [rule_format]:
      "v \<in> bin ==> \<forall>w\<in>bin. bin_add(v,w) \<in> bin"
 apply (unfold bin_add_def)
 apply (induct_tac "v")
 apply (rule_tac [3] ballI)
 apply (rename_tac [3] "w'")
 apply (induct_tac [3] "w'")
 apply (simp_all add: NCons_type)
 done
 
+declare bin_add_type [TC]
+
 lemma bin_mult_type [TC]: "[| v \<in> bin; w \<in> bin |] ==> bin_mult(v,w) \<in> bin"
 by (induct_tac "v", auto)
 
 
 subsubsection\<open>The Carry and Borrow Functions,
             \<^term>\<open>bin_succ\<close> and \<^term>\<open>bin_pred\<close>\<close>
 
 (*NCons preserves the integer value of its argument*)
 lemma integ_of_NCons [simp]:
      "[| w \<in> bin; b \<in> bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)"
 apply (erule bin.cases)
 apply (auto elim!: boolE)
 done
 
 lemma integ_of_succ [simp]:
      "w \<in> bin ==> integ_of(bin_succ(w)) = $#1 $+ integ_of(w)"
 apply (erule bin.induct)
 apply (auto simp add: zadd_ac elim!: boolE)
 done
 
 lemma integ_of_pred [simp]:
      "w \<in> bin ==> integ_of(bin_pred(w)) = $- ($#1) $+ integ_of(w)"
 apply (erule bin.induct)
 apply (auto simp add: zadd_ac elim!: boolE)
 done
 
 
 subsubsection\<open>\<^term>\<open>bin_minus\<close>: Unary Negation of Binary Integers\<close>
 
 lemma integ_of_minus: "w \<in> bin ==> integ_of(bin_minus(w)) = $- integ_of(w)"
 apply (erule bin.induct)
 apply (auto simp add: zadd_ac zminus_zadd_distrib  elim!: boolE)
 done
 
 
 subsubsection\<open>\<^term>\<open>bin_add\<close>: Binary Addition\<close>
 
 lemma bin_add_Pls [simp]: "w \<in> bin ==> bin_add(Pls,w) = w"
 by (unfold bin_add_def, simp)
 
 lemma bin_add_Pls_right: "w \<in> bin ==> bin_add(w,Pls) = w"
 apply (unfold bin_add_def)
 apply (erule bin.induct, auto)
 done
 
 lemma bin_add_Min [simp]: "w \<in> bin ==> bin_add(Min,w) = bin_pred(w)"
 by (unfold bin_add_def, simp)
 
 lemma bin_add_Min_right: "w \<in> bin ==> bin_add(w,Min) = bin_pred(w)"
 apply (unfold bin_add_def)
 apply (erule bin.induct, auto)
 done
 
 lemma bin_add_BIT_Pls [simp]: "bin_add(v BIT x,Pls) = v BIT x"
 by (unfold bin_add_def, simp)
 
 lemma bin_add_BIT_Min [simp]: "bin_add(v BIT x,Min) = bin_pred(v BIT x)"
 by (unfold bin_add_def, simp)
 
 lemma bin_add_BIT_BIT [simp]:
      "[| w \<in> bin;  y \<in> bool |]
       ==> bin_add(v BIT x, w BIT y) =
           NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)"
 by (unfold bin_add_def, simp)
 
 lemma integ_of_add [rule_format]:
      "v \<in> bin ==>
           \<forall>w\<in>bin. integ_of(bin_add(v,w)) = integ_of(v) $+ integ_of(w)"
 apply (erule bin.induct, simp, simp)
 apply (rule ballI)
 apply (induct_tac "wa")
 apply (auto simp add: zadd_ac elim!: boolE)
 done
 
 (*Subtraction*)
 lemma diff_integ_of_eq:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))"
 apply (unfold zdiff_def)
 apply (simp add: integ_of_add integ_of_minus)
 done
 
 
 subsubsection\<open>\<^term>\<open>bin_mult\<close>: Binary Multiplication\<close>
 
 lemma integ_of_mult:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)"
 apply (induct_tac "v", simp)
 apply (simp add: integ_of_minus)
 apply (auto simp add: zadd_ac integ_of_add zadd_zmult_distrib  elim!: boolE)
 done
 
 
 subsection\<open>Computations\<close>
 
 (** extra rules for bin_succ, bin_pred **)
 
 lemma bin_succ_1: "bin_succ(w BIT 1) = bin_succ(w) BIT 0"
 by simp
 
 lemma bin_succ_0: "bin_succ(w BIT 0) = NCons(w,1)"
 by simp
 
 lemma bin_pred_1: "bin_pred(w BIT 1) = NCons(w,0)"
 by simp
 
 lemma bin_pred_0: "bin_pred(w BIT 0) = bin_pred(w) BIT 1"
 by simp
 
 (** extra rules for bin_minus **)
 
 lemma bin_minus_1: "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))"
 by simp
 
 lemma bin_minus_0: "bin_minus(w BIT 0) = bin_minus(w) BIT 0"
 by simp
 
 (** extra rules for bin_add **)
 
 lemma bin_add_BIT_11: "w \<in> bin ==> bin_add(v BIT 1, w BIT 1) =
                      NCons(bin_add(v, bin_succ(w)), 0)"
 by simp
 
 lemma bin_add_BIT_10: "w \<in> bin ==> bin_add(v BIT 1, w BIT 0) =
                      NCons(bin_add(v,w), 1)"
 by simp
 
 lemma bin_add_BIT_0: "[| w \<in> bin;  y \<in> bool |]
       ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)"
 by simp
 
 (** extra rules for bin_mult **)
 
 lemma bin_mult_1: "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)"
 by simp
 
 lemma bin_mult_0: "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)"
 by simp
 
 
 (** Simplification rules with integer constants **)
 
 lemma int_of_0: "$#0 = #0"
 by simp
 
 lemma int_of_succ: "$# succ(n) = #1 $+ $#n"
 by (simp add: int_of_add [symmetric] natify_succ)
 
 lemma zminus_0 [simp]: "$- #0 = #0"
 by simp
 
 lemma zadd_0_intify [simp]: "#0 $+ z = intify(z)"
 by simp
 
 lemma zadd_0_right_intify [simp]: "z $+ #0 = intify(z)"
 by simp
 
 lemma zmult_1_intify [simp]: "#1 $* z = intify(z)"
 by simp
 
 lemma zmult_1_right_intify [simp]: "z $* #1 = intify(z)"
 by (subst zmult_commute, simp)
 
 lemma zmult_0 [simp]: "#0 $* z = #0"
 by simp
 
 lemma zmult_0_right [simp]: "z $* #0 = #0"
 by (subst zmult_commute, simp)
 
 lemma zmult_minus1 [simp]: "#-1 $* z = $-z"
 by (simp add: zcompare_rls)
 
 lemma zmult_minus1_right [simp]: "z $* #-1 = $-z"
 apply (subst zmult_commute)
 apply (rule zmult_minus1)
 done
 
 
 subsection\<open>Simplification Rules for Comparison of Binary Numbers\<close>
 text\<open>Thanks to Norbert Voelker\<close>
 
 (** Equals (=) **)
 
 lemma eq_integ_of_eq:
      "[| v \<in> bin;  w \<in> bin |]
       ==> ((integ_of(v)) = integ_of(w)) \<longleftrightarrow>
           iszero (integ_of (bin_add (v, bin_minus(w))))"
 apply (unfold iszero_def)
 apply (simp add: zcompare_rls integ_of_add integ_of_minus)
 done
 
 lemma iszero_integ_of_Pls: "iszero (integ_of(Pls))"
 by (unfold iszero_def, simp)
 
 
 lemma nonzero_integ_of_Min: "~ iszero (integ_of(Min))"
 apply (unfold iszero_def)
 apply (simp add: zminus_equation)
 done
 
 lemma iszero_integ_of_BIT:
      "[| w \<in> bin; x \<in> bool |]
       ==> iszero (integ_of (w BIT x)) \<longleftrightarrow> (x=0 & iszero (integ_of(w)))"
 apply (unfold iszero_def, simp)
 apply (subgoal_tac "integ_of (w) \<in> int")
 apply typecheck
 apply (drule int_cases)
 apply (safe elim!: boolE)
 apply (simp_all (asm_lr) add: zcompare_rls zminus_zadd_distrib [symmetric]
                      int_of_add [symmetric])
 done
 
 lemma iszero_integ_of_0:
      "w \<in> bin ==> iszero (integ_of (w BIT 0)) \<longleftrightarrow> iszero (integ_of(w))"
 by (simp only: iszero_integ_of_BIT, blast)
 
 lemma iszero_integ_of_1: "w \<in> bin ==> ~ iszero (integ_of (w BIT 1))"
 by (simp only: iszero_integ_of_BIT, blast)
 
 
 
 (** Less-than (<) **)
 
 lemma less_integ_of_eq_neg:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $< integ_of(w)
           \<longleftrightarrow> znegative (integ_of (bin_add (v, bin_minus(w))))"
 apply (unfold zless_def zdiff_def)
 apply (simp add: integ_of_minus integ_of_add)
 done
 
 lemma not_neg_integ_of_Pls: "~ znegative (integ_of(Pls))"
 by simp
 
 lemma neg_integ_of_Min: "znegative (integ_of(Min))"
 by simp
 
 lemma neg_integ_of_BIT:
      "[| w \<in> bin; x \<in> bool |]
       ==> znegative (integ_of (w BIT x)) \<longleftrightarrow> znegative (integ_of(w))"
 apply simp
 apply (subgoal_tac "integ_of (w) \<in> int")
 apply typecheck
 apply (drule int_cases)
 apply (auto elim!: boolE simp add: int_of_add [symmetric]  zcompare_rls)
 apply (simp_all add: zminus_zadd_distrib [symmetric] zdiff_def
                      int_of_add [symmetric])
 apply (subgoal_tac "$#1 $- $# succ (succ (n #+ n)) = $- $# succ (n #+ n) ")
  apply (simp add: zdiff_def)
 apply (simp add: equation_zminus int_of_diff [symmetric])
 done
 
 (** Less-than-or-equals (<=) **)
 
 lemma le_integ_of_eq_not_less:
      "(integ_of(x) $\<le> (integ_of(w))) \<longleftrightarrow> ~ (integ_of(w) $< (integ_of(x)))"
 by (simp add: not_zless_iff_zle [THEN iff_sym])
 
 
 (*Delete the original rewrites, with their clumsy conditional expressions*)
 declare bin_succ_BIT [simp del]
         bin_pred_BIT [simp del]
         bin_minus_BIT [simp del]
         NCons_Pls [simp del]
         NCons_Min [simp del]
         bin_adder_BIT [simp del]
         bin_mult_BIT [simp del]
 
 (*Hide the binary representation of integer constants*)
 declare integ_of_Pls [simp del] integ_of_Min [simp del] integ_of_BIT [simp del]
 
 
 lemmas bin_arith_extra_simps =
      integ_of_add [symmetric]
      integ_of_minus [symmetric]
      integ_of_mult [symmetric]
      bin_succ_1 bin_succ_0
      bin_pred_1 bin_pred_0
      bin_minus_1 bin_minus_0
      bin_add_Pls_right bin_add_Min_right
      bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
      diff_integ_of_eq
      bin_mult_1 bin_mult_0 NCons_simps
 
 
 (*For making a minimal simpset, one must include these default simprules
   of thy.  Also include simp_thms, or at least (~False)=True*)
 lemmas bin_arith_simps =
      bin_pred_Pls bin_pred_Min
      bin_succ_Pls bin_succ_Min
      bin_add_Pls bin_add_Min
      bin_minus_Pls bin_minus_Min
      bin_mult_Pls bin_mult_Min
      bin_arith_extra_simps
 
 (*Simplification of relational operations*)
 lemmas bin_rel_simps =
      eq_integ_of_eq iszero_integ_of_Pls nonzero_integ_of_Min
      iszero_integ_of_0 iszero_integ_of_1
      less_integ_of_eq_neg
      not_neg_integ_of_Pls neg_integ_of_Min neg_integ_of_BIT
      le_integ_of_eq_not_less
 
 declare bin_arith_simps [simp]
 declare bin_rel_simps [simp]
 
 
 (** Simplification of arithmetic when nested to the right **)
 
 lemma add_integ_of_left [simp]:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $+ (integ_of(w) $+ z) = (integ_of(bin_add(v,w)) $+ z)"
 by (simp add: zadd_assoc [symmetric])
 
 lemma mult_integ_of_left [simp]:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $* (integ_of(w) $* z) = (integ_of(bin_mult(v,w)) $* z)"
 by (simp add: zmult_assoc [symmetric])
 
 lemma add_integ_of_diff1 [simp]:
     "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)"
 apply (unfold zdiff_def)
 apply (rule add_integ_of_left, auto)
 done
 
 lemma add_integ_of_diff2 [simp]:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $+ (c $- integ_of(w)) =
           integ_of (bin_add (v, bin_minus(w))) $+ (c)"
 apply (subst diff_integ_of_eq [symmetric])
 apply (simp_all add: zdiff_def zadd_ac)
 done
 
 
 (** More for integer constants **)
 
 declare int_of_0 [simp] int_of_succ [simp]
 
 lemma zdiff0 [simp]: "#0 $- x = $-x"
 by (simp add: zdiff_def)
 
 lemma zdiff0_right [simp]: "x $- #0 = intify(x)"
 by (simp add: zdiff_def)
 
 lemma zdiff_self [simp]: "x $- x = #0"
 by (simp add: zdiff_def)
 
 lemma znegative_iff_zless_0: "k \<in> int ==> znegative(k) \<longleftrightarrow> k $< #0"
 by (simp add: zless_def)
 
 lemma zero_zless_imp_znegative_zminus: "[|#0 $< k; k \<in> int|] ==> znegative($-k)"
 by (simp add: zless_def)
 
 lemma zero_zle_int_of [simp]: "#0 $\<le> $# n"
 by (simp add: not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym])
 
 lemma nat_of_0 [simp]: "nat_of(#0) = 0"
 by (simp only: natify_0 int_of_0 [symmetric] nat_of_int_of)
 
 lemma nat_le_int0_lemma: "[| z $\<le> $#0; z \<in> int |] ==> nat_of(z) = 0"
 by (auto simp add: znegative_iff_zless_0 [THEN iff_sym] zle_def zneg_nat_of)
 
 lemma nat_le_int0: "z $\<le> $#0 ==> nat_of(z) = 0"
 apply (subgoal_tac "nat_of (intify (z)) = 0")
 apply (rule_tac [2] nat_le_int0_lemma, auto)
 done
 
 lemma int_of_eq_0_imp_natify_eq_0: "$# n = #0 ==> natify(n) = 0"
 by (rule not_znegative_imp_zero, auto)
 
 lemma nat_of_zminus_int_of: "nat_of($- $# n) = 0"
 by (simp add: nat_of_def int_of_def raw_nat_of zminus image_intrel_int)
 
 lemma int_of_nat_of: "#0 $\<le> z ==> $# nat_of(z) = intify(z)"
 apply (rule not_zneg_nat_of_intify)
 apply (simp add: znegative_iff_zless_0 not_zless_iff_zle)
 done
 
 declare int_of_nat_of [simp] nat_of_zminus_int_of [simp]
 
 lemma int_of_nat_of_if: "$# nat_of(z) = (if #0 $\<le> z then intify(z) else #0)"
 by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless)
 
 lemma zless_nat_iff_int_zless: "[| m \<in> nat; z \<in> int |] ==> (m < nat_of(z)) \<longleftrightarrow> ($#m $< z)"
 apply (case_tac "znegative (z) ")
 apply (erule_tac [2] not_zneg_nat_of [THEN subst])
 apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans]
             simp add: znegative_iff_zless_0)
 done
 
 
 (** nat_of and zless **)
 
 (*An alternative condition is  @{term"$#0 \<subseteq> w"}  *)
 lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) \<longleftrightarrow> (w $< z)"
 apply (rule iff_trans)
 apply (rule zless_int_of [THEN iff_sym])
 apply (auto simp add: int_of_nat_of_if simp del: zless_int_of)
 apply (auto elim: zless_asym simp add: not_zle_iff_zless)
 apply (blast intro: zless_zle_trans)
 done
 
 lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) \<longleftrightarrow> ($#0 $< z & w $< z)"
 apply (case_tac "$#0 $< z")
 apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle)
 done
 
 (*This simprule cannot be added unless we can find a way to make eq_integ_of_eq
   unconditional!
   [The condition "True" is a hack to prevent looping.
     Conditional rewrite rules are tried after unconditional ones, so a rule
     like eq_nat_number_of will be tried first to eliminate #mm=#nn.]
   lemma integ_of_reorient [simp]:
        "True ==> (integ_of(w) = x) \<longleftrightarrow> (x = integ_of(w))"
   by auto
 *)
 
 lemma integ_of_minus_reorient [simp]:
      "(integ_of(w) = $- x) \<longleftrightarrow> ($- x = integ_of(w))"
 by auto
 
 lemma integ_of_add_reorient [simp]:
      "(integ_of(w) = x $+ y) \<longleftrightarrow> (x $+ y = integ_of(w))"
 by auto
 
 lemma integ_of_diff_reorient [simp]:
      "(integ_of(w) = x $- y) \<longleftrightarrow> (x $- y = integ_of(w))"
 by auto
 
 lemma integ_of_mult_reorient [simp]:
      "(integ_of(w) = x $* y) \<longleftrightarrow> (x $* y = integ_of(w))"
 by auto
 
 (** To simplify inequalities involving integer negation and literals,
     such as -x = #3
 **)
 
 lemmas [simp] =
   zminus_equation [where y = "integ_of(w)"]
   equation_zminus [where x = "integ_of(w)"]
   for w
 
 lemmas [iff] =
   zminus_zless [where y = "integ_of(w)"]
   zless_zminus [where x = "integ_of(w)"]
   for w
 
 lemmas [iff] =
   zminus_zle [where y = "integ_of(w)"]
   zle_zminus [where x = "integ_of(w)"]
   for w
 
 lemmas [simp] =
   Let_def [where s = "integ_of(w)"] for w
 
 
 (*** Simprocs for numeric literals ***)
 
 (** Combining of literal coefficients in sums of products **)
 
 lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)"
   by (simp add: zcompare_rls)
 
 lemma eq_iff_zdiff_eq_0: "[| x \<in> int; y \<in> int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)"
   by (simp add: zcompare_rls)
 
 lemma zle_iff_zdiff_zle_0: "(x $\<le> y) \<longleftrightarrow> (x$-y $\<le> #0)"
   by (simp add: zcompare_rls)
 
 
 (** For combine_numerals **)
 
 lemma left_zadd_zmult_distrib: "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k"
   by (simp add: zadd_zmult_distrib zadd_ac)
 
 
 (** For cancel_numerals **)
 
 lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
   done
 
 lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> (intify(m) = (j$-i)$*u $+ n)"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
   done
 
 context fixes n :: i
 begin
 
 lemmas rel_iff_rel_0_rls =
   zless_iff_zdiff_zless_0 [where y = "u $+ v"]
   eq_iff_zdiff_eq_0 [where y = "u $+ v"]
   zle_iff_zdiff_zle_0 [where y = "u $+ v"]
   zless_iff_zdiff_zless_0 [where y = n]
   eq_iff_zdiff_eq_0 [where y = n]
   zle_iff_zdiff_zle_0 [where y = n]
   for u v
 
 lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)"
   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
   done
 
 lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> (m $< (j$-i)$*u $+ n)"
   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
   done
 
 end
 
 lemma le_add_iff1: "(i$*u $+ m $\<le> j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $\<le> n)"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
   done
 
 lemma le_add_iff2: "(i$*u $+ m $\<le> j$*u $+ n) \<longleftrightarrow> (m $\<le> (j$-i)$*u $+ n)"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
   done
 
 ML_file \<open>int_arith.ML\<close>
 
 subsection \<open>examples:\<close>
 
 text \<open>\<open>combine_numerals_prod\<close> (products of separate literals)\<close>
 lemma "#5 $* x $* #3 = y" apply simp oops
 
 schematic_goal "y2 $+ ?x42 = y $+ y2" apply simp oops
 
 lemma "oo : int ==> l $+ (l $+ #2) $+ oo = oo" apply simp oops
 
 lemma "#9$*x $+ y = x$*#23 $+ z" apply simp oops
 lemma "y $+ x = x $+ z" apply simp oops
 
 lemma "x : int ==> x $+ y $+ z = x $+ z" apply simp oops
 lemma "x : int ==> y $+ (z $+ x) = z $+ x" apply simp oops
 lemma "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)" apply simp oops
 lemma "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)" apply simp oops
 
 lemma "#-3 $* x $+ y $\<le> x $* #2 $+ z" apply simp oops
 lemma "y $+ x $\<le> x $+ z" apply simp oops
 lemma "x $+ y $+ z $\<le> x $+ z" apply simp oops
 
 lemma "y $+ (z $+ x) $< z $+ x" apply simp oops
 lemma "x $+ y $+ z $< (z $+ y) $+ (x $+ w)" apply simp oops
 lemma "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)" apply simp oops
 
 lemma "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu" apply simp oops
 lemma "u : int ==> #2 $* u = u" apply simp oops
 lemma "(i $+ j $+ #12 $+ k) $- #15 = y" apply simp oops
 lemma "(i $+ j $+ #12 $+ k) $- #5 = y" apply simp oops
 
 lemma "y $- b $< b" apply simp oops
 lemma "y $- (#3 $* b $+ c) $< b $- #2 $* c" apply simp oops
 
 lemma "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w" apply simp oops
 lemma "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w" apply simp oops
 lemma "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w" apply simp oops
 lemma "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w" apply simp oops
 
 lemma "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y" apply simp oops
 lemma "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y" apply simp oops
 
 lemma "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv" apply simp oops
 
 lemma "a $+ $-(b$+c) $+ b = d" apply simp oops
 lemma "a $+ $-(b$+c) $- b = d" apply simp oops
 
 text \<open>negative numerals\<close>
 lemma "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz" apply simp oops
 lemma "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y" apply simp oops
 lemma "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y" apply simp oops
 lemma "(i $+ j $+ #-12 $+ k) $- #15 = y" apply simp oops
 lemma "(i $+ j $+ #12 $+ k) $- #-15 = y" apply simp oops
 lemma "(i $+ j $+ #-12 $+ k) $- #-15 = y" apply simp oops
 
 text \<open>Multiplying separated numerals\<close>
 lemma "#6 $* ($# x $* #2) =  uu" apply simp oops
 lemma "#4 $* ($# x $* $# x) $* (#2 $* $# x) =  uu" apply simp oops
 
 end
diff --git a/src/ZF/List.thy b/src/ZF/List.thy
--- a/src/ZF/List.thy
+++ b/src/ZF/List.thy
@@ -1,1249 +1,1271 @@
 (*  Title:      ZF/List.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
 
 section\<open>Lists in Zermelo-Fraenkel Set Theory\<close>
 
 theory List imports Datatype ArithSimp begin
 
 consts
   list       :: "i=>i"
 
 datatype
   "list(A)" = Nil | Cons ("a \<in> A", "l \<in> list(A)")
 
 
 syntax
  "_Nil" :: i  (\<open>[]\<close>)
  "_List" :: "is => i"  (\<open>[(_)]\<close>)
 
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
   "[x]"         == "CONST Cons(x, [])"
   "[]"          == "CONST Nil"
 
 
 consts
   length :: "i=>i"
   hd     :: "i=>i"
   tl     :: "i=>i"
 
 primrec
   "length([]) = 0"
   "length(Cons(a,l)) = succ(length(l))"
 
 primrec
   "hd([]) = 0"
   "hd(Cons(a,l)) = a"
 
 primrec
   "tl([]) = []"
   "tl(Cons(a,l)) = l"
 
 
 consts
   map         :: "[i=>i, i] => i"
   set_of_list :: "i=>i"
   app         :: "[i,i]=>i"                        (infixr \<open>@\<close> 60)
 
 (*map is a binding operator -- it applies to meta-level functions, not
 object-level functions.  This simplifies the final form of term_rec_conv,
 although complicating its derivation.*)
 primrec
   "map(f,[]) = []"
   "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
 
 primrec
   "set_of_list([]) = 0"
   "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))"
 
 primrec
   app_Nil:  "[] @ ys = ys"
   app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
 
 
 consts
   rev :: "i=>i"
   flat       :: "i=>i"
   list_add   :: "i=>i"
 
 primrec
   "rev([]) = []"
   "rev(Cons(a,l)) = rev(l) @ [a]"
 
 primrec
   "flat([]) = []"
   "flat(Cons(l,ls)) = l @ flat(ls)"
 
 primrec
   "list_add([]) = 0"
   "list_add(Cons(a,l)) = a #+ list_add(l)"
 
 consts
   drop       :: "[i,i]=>i"
 
 primrec
   drop_0:    "drop(0,l) = l"
   drop_succ: "drop(succ(i), l) = tl (drop(i,l))"
 
 
 (*** Thanks to Sidi Ehmety for the following ***)
 
 definition
 (* Function `take' returns the first n elements of a list *)
   take     :: "[i,i]=>i"  where
   "take(n, as) == list_rec(\<lambda>n\<in>nat. [],
                 %a l r. \<lambda>n\<in>nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
 
 definition
   nth :: "[i, i]=>i"  where
   \<comment> \<open>returns the (n+1)th element of a list, or 0 if the
    list is too short.\<close>
   "nth(n, as) == list_rec(\<lambda>n\<in>nat. 0,
                           %a l r. \<lambda>n\<in>nat. nat_case(a, %m. r`m, n), as) ` n"
 
 definition
   list_update :: "[i, i, i]=>i"  where
   "list_update(xs, i, v) == list_rec(\<lambda>n\<in>nat. Nil,
       %u us vs. \<lambda>n\<in>nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i"
 
 consts
   filter :: "[i=>o, i] => i"
   upt :: "[i, i] =>i"
 
 primrec
   "filter(P, Nil) = Nil"
   "filter(P, Cons(x, xs)) =
      (if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))"
 
 primrec
   "upt(i, 0) = Nil"
   "upt(i, succ(j)) = (if i \<le> j then upt(i, j)@[j] else Nil)"
 
 definition
   min :: "[i,i] =>i"  where
     "min(x, y) == (if x \<le> y then x else y)"
 
 definition
   max :: "[i, i] =>i"  where
     "max(x, y) == (if x \<le> y then y else x)"
 
 (*** Aspects of the datatype definition ***)
 
 declare list.intros [simp,TC]
 
 (*An elimination rule, for type-checking*)
 inductive_cases ConsE: "Cons(a,l) \<in> list(A)"
 
 lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) \<longleftrightarrow> a \<in> A & l \<in> list(A)"
 by (blast elim: ConsE)
 
 (*Proving freeness results*)
 lemma Cons_iff: "Cons(a,l)=Cons(a',l') \<longleftrightarrow> a=a' & l=l'"
 by auto
 
 lemma Nil_Cons_iff: "~ Nil=Cons(a,l)"
 by auto
 
 lemma list_unfold: "list(A) = {0} + (A * list(A))"
 by (blast intro!: list.intros [unfolded list.con_defs]
           elim: list.cases [unfolded list.con_defs])
 
 
 (**  Lemmas to justify using "list" in other recursive type definitions **)
 
 lemma list_mono: "A<=B ==> list(A) \<subseteq> list(B)"
 apply (unfold list.defs )
 apply (rule lfp_mono)
 apply (simp_all add: list.bnd_mono)
 apply (assumption | rule univ_mono basic_monos)+
 done
 
 (*There is a similar proof by list induction.*)
 lemma list_univ: "list(univ(A)) \<subseteq> univ(A)"
 apply (unfold list.defs list.con_defs)
 apply (rule lfp_lowerbound)
 apply (rule_tac [2] A_subset_univ [THEN univ_mono])
 apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
 done
 
 (*These two theorems justify datatypes involving list(nat), list(A), ...*)
 lemmas list_subset_univ = subset_trans [OF list_mono list_univ]
 
 lemma list_into_univ: "[| l \<in> list(A);  A \<subseteq> univ(B) |] ==> l \<in> univ(B)"
 by (blast intro: list_subset_univ [THEN subsetD])
 
 lemma list_case_type:
     "[| l \<in> list(A);
         c \<in> C(Nil);
         !!x y. [| x \<in> A;  y \<in> list(A) |] ==> h(x,y): C(Cons(x,y))
      |] ==> list_case(c,h,l) \<in> C(l)"
 by (erule list.induct, auto)
 
 lemma list_0_triv: "list(0) = {Nil}"
 apply (rule equalityI, auto)
 apply (induct_tac x, auto)
 done
 
 
 (*** List functions ***)
 
 lemma tl_type: "l \<in> list(A) ==> tl(l) \<in> list(A)"
 apply (induct_tac "l")
 apply (simp_all (no_asm_simp) add: list.intros)
 done
 
 (** drop **)
 
 lemma drop_Nil [simp]: "i \<in> nat ==> drop(i, Nil) = Nil"
 apply (induct_tac "i")
 apply (simp_all (no_asm_simp))
 done
 
 lemma drop_succ_Cons [simp]: "i \<in> nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"
 apply (rule sym)
 apply (induct_tac "i")
 apply (simp (no_asm))
 apply (simp (no_asm_simp))
 done
 
 lemma drop_type [simp,TC]: "[| i \<in> nat; l \<in> list(A) |] ==> drop(i,l) \<in> list(A)"
 apply (induct_tac "i")
 apply (simp_all (no_asm_simp) add: tl_type)
 done
 
 declare drop_succ [simp del]
 
 
 (** Type checking -- proved by induction, as usual **)
 
 lemma list_rec_type [TC]:
     "[| l \<in> list(A);
         c \<in> C(Nil);
         !!x y r. [| x \<in> A;  y \<in> list(A);  r \<in> C(y) |] ==> h(x,y,r): C(Cons(x,y))
      |] ==> list_rec(c,h,l) \<in> C(l)"
 by (induct_tac "l", auto)
 
 (** map **)
 
 lemma map_type [TC]:
     "[| l \<in> list(A);  !!x. x \<in> A ==> h(x): B |] ==> map(h,l) \<in> list(B)"
 apply (simp add: map_list_def)
 apply (typecheck add: list.intros list_rec_type, blast)
 done
 
 lemma map_type2 [TC]: "l \<in> list(A) ==> map(h,l) \<in> list({h(u). u \<in> A})"
 apply (erule map_type)
 apply (erule RepFunI)
 done
 
 (** length **)
 
 lemma length_type [TC]: "l \<in> list(A) ==> length(l) \<in> nat"
 by (simp add: length_list_def)
 
 lemma lt_length_in_nat:
    "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
 by (frule lt_nat_in_nat, typecheck)
 
 (** app **)
 
 lemma app_type [TC]: "[| xs: list(A);  ys: list(A) |] ==> xs@ys \<in> list(A)"
 by (simp add: app_list_def)
 
 (** rev **)
 
 lemma rev_type [TC]: "xs: list(A) ==> rev(xs) \<in> list(A)"
 by (simp add: rev_list_def)
 
 
 (** flat **)
 
 lemma flat_type [TC]: "ls: list(list(A)) ==> flat(ls) \<in> list(A)"
 by (simp add: flat_list_def)
 
 
 (** set_of_list **)
 
 lemma set_of_list_type [TC]: "l \<in> list(A) ==> set_of_list(l) \<in> Pow(A)"
 apply (unfold set_of_list_list_def)
 apply (erule list_rec_type, auto)
 done
 
 lemma set_of_list_append:
      "xs: list(A) ==> set_of_list (xs@ys) = set_of_list(xs) \<union> set_of_list(ys)"
 apply (erule list.induct)
 apply (simp_all (no_asm_simp) add: Un_cons)
 done
 
 
 (** list_add **)
 
 lemma list_add_type [TC]: "xs: list(nat) ==> list_add(xs) \<in> nat"
 by (simp add: list_add_list_def)
 
 
 (*** theorems about map ***)
 
 lemma map_ident [simp]: "l \<in> list(A) ==> map(%u. u, l) = l"
 apply (induct_tac "l")
 apply (simp_all (no_asm_simp))
 done
 
 lemma map_compose: "l \<in> list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)"
 apply (induct_tac "l")
 apply (simp_all (no_asm_simp))
 done
 
 lemma map_app_distrib: "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"
 apply (induct_tac "xs")
 apply (simp_all (no_asm_simp))
 done
 
 lemma map_flat: "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"
 apply (induct_tac "ls")
 apply (simp_all (no_asm_simp) add: map_app_distrib)
 done
 
 lemma list_rec_map:
      "l \<in> list(A) ==>
       list_rec(c, d, map(h,l)) =
       list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)"
 apply (induct_tac "l")
 apply (simp_all (no_asm_simp))
 done
 
 (** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **)
 
 (* @{term"c \<in> list(Collect(B,P)) ==> c \<in> list"} *)
 lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD]
 
 lemma map_list_Collect: "l \<in> list({x \<in> A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"
 apply (induct_tac "l")
 apply (simp_all (no_asm_simp))
 done
 
 (*** theorems about length ***)
 
 lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)"
 by (induct_tac "xs", simp_all)
 
 lemma length_app [simp]:
      "[| xs: list(A); ys: list(A) |]
       ==> length(xs@ys) = length(xs) #+ length(ys)"
 by (induct_tac "xs", simp_all)
 
 lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)"
 apply (induct_tac "xs")
 apply (simp_all (no_asm_simp) add: length_app)
 done
 
 lemma length_flat:
      "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"
 apply (induct_tac "ls")
 apply (simp_all (no_asm_simp) add: length_app)
 done
 
 (** Length and drop **)
 
 (*Lemma for the inductive step of drop_length*)
 lemma drop_length_Cons [rule_format]:
      "xs: list(A) ==>
            \<forall>x.  \<exists>z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
 by (erule list.induct, simp_all)
 
 lemma drop_length [rule_format]:
      "l \<in> list(A) ==> \<forall>i \<in> length(l). (\<exists>z zs. drop(i,l) = Cons(z,zs))"
 apply (erule list.induct, simp_all, safe)
 apply (erule drop_length_Cons)
 apply (rule natE)
 apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all)
 apply (blast intro: succ_in_naturalD length_type)
 done
 
 
 (*** theorems about app ***)
 
 lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs"
 by (erule list.induct, simp_all)
 
 lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"
 by (induct_tac "xs", simp_all)
 
 lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"
 apply (induct_tac "ls")
 apply (simp_all (no_asm_simp) add: app_assoc)
 done
 
 (*** theorems about rev ***)
 
 lemma rev_map_distrib: "l \<in> list(A) ==> rev(map(h,l)) = map(h,rev(l))"
 apply (induct_tac "l")
 apply (simp_all (no_asm_simp) add: map_app_distrib)
 done
 
 (*Simplifier needs the premises as assumptions because rewriting will not
   instantiate the variable ?A in the rules' typing conditions; note that
   rev_type does not instantiate ?A.  Only the premises do.
 *)
 lemma rev_app_distrib:
      "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"
 apply (erule list.induct)
 apply (simp_all add: app_assoc)
 done
 
 lemma rev_rev_ident [simp]: "l \<in> list(A) ==> rev(rev(l))=l"
 apply (induct_tac "l")
 apply (simp_all (no_asm_simp) add: rev_app_distrib)
 done
 
 lemma rev_flat: "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"
 apply (induct_tac "ls")
 apply (simp_all add: map_app_distrib flat_app_distrib rev_app_distrib)
 done
 
 
 (*** theorems about list_add ***)
 
 lemma list_add_app:
      "[| xs: list(nat);  ys: list(nat) |]
       ==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)"
 apply (induct_tac "xs", simp_all)
 done
 
 lemma list_add_rev: "l \<in> list(nat) ==> list_add(rev(l)) = list_add(l)"
 apply (induct_tac "l")
 apply (simp_all (no_asm_simp) add: list_add_app)
 done
 
 lemma list_add_flat:
      "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"
 apply (induct_tac "ls")
 apply (simp_all (no_asm_simp) add: list_add_app)
 done
 
 (** New induction rules **)
 
 lemma list_append_induct [case_names Nil snoc, consumes 1]:
     "[| l \<in> list(A);
         P(Nil);
         !!x y. [| x \<in> A;  y \<in> list(A);  P(y) |] ==> P(y @ [x])
      |] ==> P(l)"
 apply (subgoal_tac "P(rev(rev(l)))", simp)
 apply (erule rev_type [THEN list.induct], simp_all)
 done
 
 lemma list_complete_induct_lemma [rule_format]:
  assumes ih:
     "\<And>l. [| l \<in> list(A);
              \<forall>l' \<in> list(A). length(l') < length(l) \<longrightarrow> P(l')|]
           ==> P(l)"
   shows "n \<in> nat ==> \<forall>l \<in> list(A). length(l) < n \<longrightarrow> P(l)"
 apply (induct_tac n, simp)
 apply (blast intro: ih elim!: leE)
 done
 
 theorem list_complete_induct:
       "[| l \<in> list(A);
           \<And>l. [| l \<in> list(A);
                   \<forall>l' \<in> list(A). length(l') < length(l) \<longrightarrow> P(l')|]
                ==> P(l)
        |] ==> P(l)"
 apply (rule list_complete_induct_lemma [of A])
    prefer 4 apply (rule le_refl, simp)
   apply blast
  apply simp
 apply assumption
 done
 
 
 (*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)
 
 (** min FIXME: replace by Int! **)
 (* Min theorems are also true for i, j ordinals *)
 lemma min_sym: "[| i \<in> nat; j \<in> nat |] ==> min(i,j)=min(j,i)"
 apply (unfold min_def)
 apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym)
 done
 
 lemma min_type [simp,TC]: "[| i \<in> nat; j \<in> nat |] ==> min(i,j):nat"
 by (unfold min_def, auto)
 
 lemma min_0 [simp]: "i \<in> nat ==> min(0,i) = 0"
 apply (unfold min_def)
 apply (auto dest: not_lt_imp_le)
 done
 
 lemma min_02 [simp]: "i \<in> nat ==> min(i, 0) = 0"
 apply (unfold min_def)
 apply (auto dest: not_lt_imp_le)
 done
 
 lemma lt_min_iff: "[| i \<in> nat; j \<in> nat; k \<in> nat |] ==> i<min(j,k) \<longleftrightarrow> i<j & i<k"
 apply (unfold min_def)
 apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
 done
 
 lemma min_succ_succ [simp]:
      "[| i \<in> nat; j \<in> nat |] ==>  min(succ(i), succ(j))= succ(min(i, j))"
 apply (unfold min_def, auto)
 done
 
 (*** more theorems about lists ***)
 
 (** filter **)
 
 lemma filter_append [simp]:
      "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)"
 by (induct_tac "xs", auto)
 
 lemma filter_type [simp,TC]: "xs:list(A) ==> filter(P, xs):list(A)"
 by (induct_tac "xs", auto)
 
 lemma length_filter: "xs:list(A) ==> length(filter(P, xs)) \<le> length(xs)"
 apply (induct_tac "xs", auto)
 apply (rule_tac j = "length (l) " in le_trans)
 apply (auto simp add: le_iff)
 done
 
 lemma filter_is_subset: "xs:list(A) ==> set_of_list(filter(P,xs)) \<subseteq> set_of_list(xs)"
 by (induct_tac "xs", auto)
 
 lemma filter_False [simp]: "xs:list(A) ==> filter(%p. False, xs) = Nil"
 by (induct_tac "xs", auto)
 
 lemma filter_True [simp]: "xs:list(A) ==> filter(%p. True, xs) = xs"
 by (induct_tac "xs", auto)
 
 (** length **)
 
 lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 \<longleftrightarrow> xs=Nil"
 by (erule list.induct, auto)
 
 lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) \<longleftrightarrow> xs=Nil"
 by (erule list.induct, auto)
 
 lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1"
 by (erule list.induct, auto)
 
 lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) \<longleftrightarrow> xs \<noteq> Nil"
 by (erule list.induct, auto)
 
 lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) \<longleftrightarrow> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)"
 by (erule list.induct, auto)
 
 (** more theorems about append **)
 
 lemma append_is_Nil_iff [simp]:
      "xs:list(A) ==> (xs@ys = Nil) \<longleftrightarrow> (xs=Nil & ys = Nil)"
 by (erule list.induct, auto)
 
 lemma append_is_Nil_iff2 [simp]:
      "xs:list(A) ==> (Nil = xs@ys) \<longleftrightarrow> (xs=Nil & ys = Nil)"
 by (erule list.induct, auto)
 
 lemma append_left_is_self_iff [simp]:
      "xs:list(A) ==> (xs@ys = xs) \<longleftrightarrow> (ys = Nil)"
 by (erule list.induct, auto)
 
 lemma append_left_is_self_iff2 [simp]:
      "xs:list(A) ==> (xs = xs@ys) \<longleftrightarrow> (ys = Nil)"
 by (erule list.induct, auto)
 
 (*TOO SLOW as a default simprule!*)
 lemma append_left_is_Nil_iff [rule_format]:
      "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
    length(ys)=length(zs) \<longrightarrow> (xs@ys=zs \<longleftrightarrow> (xs=Nil & ys=zs))"
 apply (erule list.induct)
 apply (auto simp add: length_app)
 done
 
 (*TOO SLOW as a default simprule!*)
 lemma append_left_is_Nil_iff2 [rule_format]:
      "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
    length(ys)=length(zs) \<longrightarrow> (zs=ys@xs \<longleftrightarrow> (xs=Nil & ys=zs))"
 apply (erule list.induct)
 apply (auto simp add: length_app)
 done
 
-lemma append_eq_append_iff [rule_format,simp]:
+lemma append_eq_append_iff [rule_format]:
      "xs:list(A) ==> \<forall>ys \<in> list(A).
       length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys & us=vs)"
 apply (erule list.induct)
 apply (simp (no_asm_simp))
 apply clarify
 apply (erule_tac a = ys in list.cases, auto)
 done
+declare append_eq_append_iff [simp]
 
 lemma append_eq_append [rule_format]:
   "xs:list(A) ==>
    \<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> list(A).
    length(us) = length(vs) \<longrightarrow> (xs@us = ys@vs) \<longrightarrow> (xs=ys & us=vs)"
 apply (induct_tac "xs")
 apply (force simp add: length_app, clarify)
 apply (erule_tac a = ys in list.cases, simp)
 apply (subgoal_tac "Cons (a, l) @ us =vs")
  apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all, blast)
 done
 
 lemma append_eq_append_iff2 [simp]:
  "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |]
   ==>  xs@us = ys@vs \<longleftrightarrow> (xs=ys & us=vs)"
 apply (rule iffI)
 apply (rule append_eq_append, auto)
 done
 
 lemma append_self_iff [simp]:
      "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs \<longleftrightarrow> ys=zs"
 by simp
 
 lemma append_self_iff2 [simp]:
      "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs \<longleftrightarrow> ys=zs"
 by simp
 
 (* Can also be proved from append_eq_append_iff2,
 but the proof requires two more hypotheses: x \<in> A and y \<in> A *)
-lemma append1_eq_iff [rule_format,simp]:
+lemma append1_eq_iff [rule_format]:
      "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)"
 apply (erule list.induct)
  apply clarify
  apply (erule list.cases)
  apply simp_all
 txt\<open>Inductive step\<close>
 apply clarify
 apply (erule_tac a=ys in list.cases, simp_all)
 done
-
+declare append1_eq_iff [simp]
 
 lemma append_right_is_self_iff [simp]:
      "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) \<longleftrightarrow> (xs=Nil)"
 by (simp (no_asm_simp) add: append_left_is_Nil_iff)
 
 lemma append_right_is_self_iff2 [simp]:
      "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) \<longleftrightarrow> (xs=Nil)"
 apply (rule iffI)
 apply (drule sym, auto)
 done
 
-lemma hd_append [rule_format,simp]:
+lemma hd_append [rule_format]:
      "xs:list(A) ==> xs \<noteq> Nil \<longrightarrow> hd(xs @ ys) = hd(xs)"
 by (induct_tac "xs", auto)
+declare hd_append [simp]
 
-lemma tl_append [rule_format,simp]:
+lemma tl_append [rule_format]:
      "xs:list(A) ==> xs\<noteq>Nil \<longrightarrow> tl(xs @ ys) = tl(xs)@ys"
 by (induct_tac "xs", auto)
+declare tl_append [simp]
 
 (** rev **)
 lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil \<longleftrightarrow> xs = Nil)"
 by (erule list.induct, auto)
 
 lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) \<longleftrightarrow> xs = Nil)"
 by (erule list.induct, auto)
 
-lemma rev_is_rev_iff [rule_format,simp]:
+lemma rev_is_rev_iff [rule_format]:
      "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) \<longleftrightarrow> xs=ys"
 apply (erule list.induct, force, clarify)
 apply (erule_tac a = ys in list.cases, auto)
 done
+declare rev_is_rev_iff [simp]
 
 lemma rev_list_elim [rule_format]:
      "xs:list(A) ==>
       (xs=Nil \<longrightarrow> P) \<longrightarrow> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] \<longrightarrow>P)\<longrightarrow>P"
 by (erule list_append_induct, auto)
 
 
 (** more theorems about drop **)
 
-lemma length_drop [rule_format,simp]:
+lemma length_drop [rule_format]:
      "n \<in> nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) #- n"
 apply (erule nat_induct)
 apply (auto elim: list.cases)
 done
+declare length_drop [simp]
 
-lemma drop_all [rule_format,simp]:
+lemma drop_all [rule_format]:
      "n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n \<longrightarrow> drop(n, xs)=Nil"
 apply (erule nat_induct)
 apply (auto elim: list.cases)
 done
+declare drop_all [simp]
 
 lemma drop_append [rule_format]:
      "n \<in> nat ==>
       \<forall>xs \<in> list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)"
 apply (induct_tac "n")
 apply (auto elim: list.cases)
 done
 
 lemma drop_drop:
     "m \<in> nat ==> \<forall>xs \<in> list(A). \<forall>n \<in> nat. drop(n, drop(m, xs))=drop(n #+ m, xs)"
 apply (induct_tac "m")
 apply (auto elim: list.cases)
 done
 
 (** take **)
 
 lemma take_0 [simp]: "xs:list(A) ==> take(0, xs) =  Nil"
 apply (unfold take_def)
 apply (erule list.induct, auto)
 done
 
 lemma take_succ_Cons [simp]:
     "n \<in> nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))"
 by (simp add: take_def)
 
 (* Needed for proving take_all *)
 lemma take_Nil [simp]: "n \<in> nat ==> take(n, Nil) = Nil"
 by (unfold take_def, auto)
 
-lemma take_all [rule_format,simp]:
+lemma take_all [rule_format]:
      "n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n  \<longrightarrow> take(n, xs) = xs"
 apply (erule nat_induct)
 apply (auto elim: list.cases)
 done
+declare take_all [simp]
 
-lemma take_type [rule_format,simp,TC]:
+lemma take_type [rule_format]:
      "xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
 apply (erule list.induct, simp, clarify)
 apply (erule natE, auto)
 done
+declare take_type [simp,TC]
 
-lemma take_append [rule_format,simp]:
+lemma take_append [rule_format]:
  "xs:list(A) ==>
   \<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) =
                             take(n, xs) @ take(n #- length(xs), ys)"
 apply (erule list.induct, simp, clarify)
 apply (erule natE, auto)
 done
+declare take_append [simp]
 
 lemma take_take [rule_format]:
    "m \<in> nat ==>
     \<forall>xs \<in> list(A). \<forall>n \<in> nat. take(n, take(m,xs))= take(min(n, m), xs)"
 apply (induct_tac "m", auto)
 apply (erule_tac a = xs in list.cases)
 apply (auto simp add: take_Nil)
 apply (erule_tac n=n in natE)
 apply (auto intro: take_0 take_type)
 done
 
 (** nth **)
 
 lemma nth_0 [simp]: "nth(0, Cons(a, l)) = a"
 by (simp add: nth_def)
 
 lemma nth_Cons [simp]: "n \<in> nat ==> nth(succ(n), Cons(a,l)) = nth(n,l)"
 by (simp add: nth_def)
 
 lemma nth_empty [simp]: "nth(n, Nil) = 0"
 by (simp add: nth_def)
 
-lemma nth_type [rule_format,simp,TC]:
+lemma nth_type [rule_format]:
      "xs:list(A) ==> \<forall>n. n < length(xs) \<longrightarrow> nth(n,xs) \<in> A"
 apply (erule list.induct, simp, clarify)
 apply (subgoal_tac "n \<in> nat")
  apply (erule natE, auto dest!: le_in_nat)
 done
+declare nth_type [simp,TC]
 
 lemma nth_eq_0 [rule_format]:
      "xs:list(A) ==> \<forall>n \<in> nat. length(xs) \<le> n \<longrightarrow> nth(n,xs) = 0"
 apply (erule list.induct, simp, clarify)
 apply (erule natE, auto)
 done
 
 lemma nth_append [rule_format]:
   "xs:list(A) ==>
    \<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs)
                                 else nth(n #- length(xs), ys))"
 apply (induct_tac "xs", simp, clarify)
 apply (erule natE, auto)
 done
 
 lemma set_of_list_conv_nth:
     "xs:list(A)
      ==> set_of_list(xs) = {x \<in> A. \<exists>i\<in>nat. i<length(xs) & x = nth(i,xs)}"
 apply (induct_tac "xs", simp_all)
 apply (rule equalityI, auto)
 apply (rule_tac x = 0 in bexI, auto)
 apply (erule natE, auto)
 done
 
 (* Other theorems about lists *)
 
 lemma nth_take_lemma [rule_format]:
  "k \<in> nat ==>
   \<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k \<le> length(xs) \<longrightarrow> k \<le> length(ys) \<longrightarrow>
       (\<forall>i \<in> nat. i<k \<longrightarrow> nth(i,xs) = nth(i,ys))\<longrightarrow> take(k,xs) = take(k,ys))"
 apply (induct_tac "k")
 apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib)
 apply clarify
 (*Both lists are non-empty*)
 apply (erule_tac a=xs in list.cases, simp)
 apply (erule_tac a=ys in list.cases, clarify)
 apply (simp (no_asm_use) )
 apply clarify
 apply (simp (no_asm_simp))
 apply (rule conjI, force)
 apply (rename_tac y ys z zs)
 apply (drule_tac x = zs and x1 = ys in bspec [THEN bspec], auto)
 done
 
 lemma nth_equalityI [rule_format]:
      "[| xs:list(A); ys:list(A); length(xs) = length(ys);
          \<forall>i \<in> nat. i < length(xs) \<longrightarrow> nth(i,xs) = nth(i,ys) |]
       ==> xs = ys"
 apply (subgoal_tac "length (xs) \<le> length (ys) ")
 apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma)
 apply (simp_all add: take_all)
 done
 
 (*The famous take-lemma*)
 
 lemma take_equalityI [rule_format]:
     "[| xs:list(A); ys:list(A); (\<forall>i \<in> nat. take(i, xs) = take(i,ys)) |]
      ==> xs = ys"
 apply (case_tac "length (xs) \<le> length (ys) ")
 apply (drule_tac x = "length (ys) " in bspec)
 apply (drule_tac [3] not_lt_imp_le)
 apply (subgoal_tac [5] "length (ys) \<le> length (xs) ")
 apply (rule_tac [6] j = "succ (length (ys))" in le_trans)
 apply (rule_tac [6] leI)
 apply (drule_tac [5] x = "length (xs) " in bspec)
 apply (simp_all add: take_all)
 done
 
 lemma nth_drop [rule_format]:
   "n \<in> nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)"
 apply (induct_tac "n", simp_all, clarify)
 apply (erule list.cases, auto)
 done
 
 lemma take_succ [rule_format]:
   "xs\<in>list(A)
    ==> \<forall>i. i < length(xs) \<longrightarrow> take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]"
 apply (induct_tac "xs", auto)
 apply (subgoal_tac "i\<in>nat")
 apply (erule natE)
 apply (auto simp add: le_in_nat)
 done
 
 lemma take_add [rule_format]:
      "[|xs\<in>list(A); j\<in>nat|]
       ==> \<forall>i\<in>nat. take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))"
 apply (induct_tac "xs", simp_all, clarify)
 apply (erule_tac n = i in natE, simp_all)
 done
 
 lemma length_take:
      "l\<in>list(A) ==> \<forall>n\<in>nat. length(take(n,l)) = min(n, length(l))"
 apply (induct_tac "l", safe, simp_all)
 apply (erule natE, simp_all)
 done
 
 subsection\<open>The function zip\<close>
 
 text\<open>Crafty definition to eliminate a type argument\<close>
 
 consts
   zip_aux        :: "[i,i]=>i"
 
 primrec (*explicit lambda is required because both arguments of "un" vary*)
   "zip_aux(B,[]) =
      (\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))"
 
   "zip_aux(B,Cons(x,l)) =
      (\<lambda>ys \<in> list(B).
         list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))"
 
 definition
   zip :: "[i, i]=>i"  where
    "zip(xs, ys) == zip_aux(set_of_list(ys),xs)`ys"
 
 
 (* zip equations *)
 
 lemma list_on_set_of_list: "xs \<in> list(A) ==> xs \<in> list(set_of_list(xs))"
 apply (induct_tac xs, simp_all)
 apply (blast intro: list_mono [THEN subsetD])
 done
 
 lemma zip_Nil [simp]: "ys:list(A) ==> zip(Nil, ys)=Nil"
 apply (simp add: zip_def list_on_set_of_list [of _ A])
 apply (erule list.cases, simp_all)
 done
 
 lemma zip_Nil2 [simp]: "xs:list(A) ==> zip(xs, Nil)=Nil"
 apply (simp add: zip_def list_on_set_of_list [of _ A])
 apply (erule list.cases, simp_all)
 done
 
 lemma zip_aux_unique [rule_format]:
      "[|B<=C;  xs \<in> list(A)|]
       ==> \<forall>ys \<in> list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys"
 apply (induct_tac xs)
  apply simp_all
  apply (blast intro: list_mono [THEN subsetD], clarify)
 apply (erule_tac a=ys in list.cases, auto)
 apply (blast intro: list_mono [THEN subsetD])
 done
 
 lemma zip_Cons_Cons [simp]:
      "[| xs:list(A); ys:list(B); x \<in> A; y \<in> B |] ==>
       zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))"
 apply (simp add: zip_def, auto)
 apply (rule zip_aux_unique, auto)
 apply (simp add: list_on_set_of_list [of _ B])
 apply (blast intro: list_on_set_of_list list_mono [THEN subsetD])
 done
 
-lemma zip_type [rule_format,simp,TC]:
+lemma zip_type [rule_format]:
      "xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)"
 apply (induct_tac "xs")
 apply (simp (no_asm))
 apply clarify
 apply (erule_tac a = ys in list.cases, auto)
 done
+declare zip_type [simp,TC]
 
 (* zip length *)
-lemma length_zip [rule_format,simp]:
+lemma length_zip [rule_format]:
      "xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
                                      min(length(xs), length(ys))"
 apply (unfold min_def)
 apply (induct_tac "xs", simp_all, clarify)
 apply (erule_tac a = ys in list.cases, auto)
 done
+declare length_zip [simp]
 
 lemma zip_append1 [rule_format]:
  "[| ys:list(A); zs:list(B) |] ==>
   \<forall>xs \<in> list(A). zip(xs @ ys, zs) =
                  zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))"
 apply (induct_tac "zs", force, clarify)
 apply (erule_tac a = xs in list.cases, simp_all)
 done
 
 lemma zip_append2 [rule_format]:
  "[| xs:list(A); zs:list(B) |] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) =
        zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)"
 apply (induct_tac "xs", force, clarify)
 apply (erule_tac a = ys in list.cases, auto)
 done
 
 lemma zip_append [simp]:
  "[| length(xs) = length(us); length(ys) = length(vs);
      xs:list(A); us:list(B); ys:list(A); vs:list(B) |]
   ==> zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)"
 by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0)
 
 
-lemma zip_rev [rule_format,simp]:
+lemma zip_rev [rule_format]:
  "ys:list(B) ==> \<forall>xs \<in> list(A).
     length(xs) = length(ys) \<longrightarrow> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
 apply (induct_tac "ys", force, clarify)
 apply (erule_tac a = xs in list.cases)
 apply (auto simp add: length_rev)
 done
+declare zip_rev [simp]
 
-lemma nth_zip [rule_format,simp]:
+lemma nth_zip [rule_format]:
    "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
                     i < length(xs) \<longrightarrow> i < length(ys) \<longrightarrow>
                     nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
 apply (induct_tac "ys", force, clarify)
 apply (erule_tac a = xs in list.cases, simp)
 apply (auto elim: natE)
 done
+declare nth_zip [simp]
 
 lemma set_of_list_zip [rule_format]:
      "[| xs:list(A); ys:list(B); i \<in> nat |]
       ==> set_of_list(zip(xs, ys)) =
           {<x, y>:A*B. \<exists>i\<in>nat. i < min(length(xs), length(ys))
           & x = nth(i, xs) & y = nth(i, ys)}"
 by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth)
 
 (** list_update **)
 
 lemma list_update_Nil [simp]: "i \<in> nat ==>list_update(Nil, i, v) = Nil"
 by (unfold list_update_def, auto)
 
 lemma list_update_Cons_0 [simp]: "list_update(Cons(x, xs), 0, v)= Cons(v, xs)"
 by (unfold list_update_def, auto)
 
 lemma list_update_Cons_succ [simp]:
   "n \<in> nat ==>
     list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))"
 apply (unfold list_update_def, auto)
 done
 
-lemma list_update_type [rule_format,simp,TC]:
+lemma list_update_type [rule_format]:
      "[| xs:list(A); v \<in> A |] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)"
 apply (induct_tac "xs")
 apply (simp (no_asm))
 apply clarify
 apply (erule natE, auto)
 done
+declare list_update_type [simp,TC]
 
-lemma length_list_update [rule_format,simp]:
+lemma length_list_update [rule_format]:
      "xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)"
 apply (induct_tac "xs")
 apply (simp (no_asm))
 apply clarify
 apply (erule natE, auto)
 done
+declare length_list_update [simp]
 
 lemma nth_list_update [rule_format]:
      "[| xs:list(A) |] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs)  \<longrightarrow>
          nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))"
 apply (induct_tac "xs")
  apply simp_all
 apply clarify
 apply (rename_tac i j)
 apply (erule_tac n=i in natE)
 apply (erule_tac [2] n=j in natE)
 apply (erule_tac n=j in natE, simp_all, force)
 done
 
 lemma nth_list_update_eq [simp]:
      "[| i < length(xs); xs:list(A) |] ==> nth(i, list_update(xs, i,x)) = x"
 by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update)
 
 
-lemma nth_list_update_neq [rule_format,simp]:
+lemma nth_list_update_neq [rule_format]:
   "xs:list(A) ==>
      \<forall>i \<in> nat. \<forall>j \<in> nat. i \<noteq> j \<longrightarrow> nth(j, list_update(xs,i,x)) = nth(j,xs)"
 apply (induct_tac "xs")
  apply (simp (no_asm))
 apply clarify
 apply (erule natE)
 apply (erule_tac [2] natE, simp_all)
 apply (erule natE, simp_all)
 done
+declare nth_list_update_neq [simp]
 
-lemma list_update_overwrite [rule_format,simp]:
+lemma list_update_overwrite [rule_format]:
      "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs)
    \<longrightarrow> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)"
 apply (induct_tac "xs")
  apply (simp (no_asm))
 apply clarify
 apply (erule natE, auto)
 done
+declare list_update_overwrite [simp]
 
 lemma list_update_same_conv [rule_format]:
      "xs:list(A) ==>
       \<forall>i \<in> nat. i < length(xs) \<longrightarrow>
                  (list_update(xs, i, x) = xs) \<longleftrightarrow> (nth(i, xs) = x)"
 apply (induct_tac "xs")
  apply (simp (no_asm))
 apply clarify
 apply (erule natE, auto)
 done
 
 lemma update_zip [rule_format]:
      "ys:list(B) ==>
       \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A).
         length(xs) = length(ys) \<longrightarrow>
         list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)),
                                               list_update(ys, i, snd(xy)))"
 apply (induct_tac "ys")
  apply auto
 apply (erule_tac a = xs in list.cases)
 apply (auto elim: natE)
 done
 
 lemma set_update_subset_cons [rule_format]:
   "xs:list(A) ==>
    \<forall>i \<in> nat. set_of_list(list_update(xs, i, x)) \<subseteq> cons(x, set_of_list(xs))"
 apply (induct_tac "xs")
  apply simp
 apply (rule ballI)
 apply (erule natE, simp_all, auto)
 done
 
 lemma set_of_list_update_subsetI:
      "[| set_of_list(xs) \<subseteq> A; xs:list(A); x \<in> A; i \<in> nat|]
    ==> set_of_list(list_update(xs, i,x)) \<subseteq> A"
 apply (rule subset_trans)
 apply (rule set_update_subset_cons, auto)
 done
 
 (** upt **)
 
 lemma upt_rec:
      "j \<in> nat ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)"
 apply (induct_tac "j", auto)
 apply (drule not_lt_imp_le)
 apply (auto simp: lt_Ord intro: le_anti_sym)
 done
 
 lemma upt_conv_Nil [simp]: "[| j \<le> i; j \<in> nat |] ==> upt(i,j) = Nil"
 apply (subst upt_rec, auto)
 apply (auto simp add: le_iff)
 apply (drule lt_asym [THEN notE], auto)
 done
 
 (*Only needed if upt_Suc is deleted from the simpset*)
 lemma upt_succ_append:
      "[| i \<le> j; j \<in> nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]"
 by simp
 
 lemma upt_conv_Cons:
      "[| i<j; j \<in> nat |]  ==> upt(i,j) = Cons(i,upt(succ(i),j))"
 apply (rule trans)
 apply (rule upt_rec, auto)
 done
 
 lemma upt_type [simp,TC]: "j \<in> nat ==> upt(i,j):list(nat)"
 by (induct_tac "j", auto)
 
 (*LOOPS as a simprule, since j<=j*)
 lemma upt_add_eq_append:
      "[| i \<le> j; j \<in> nat; k \<in> nat |] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)"
 apply (induct_tac "k")
 apply (auto simp add: app_assoc app_type)
 apply (rule_tac j = j in le_trans, auto)
 done
 
 lemma length_upt [simp]: "[| i \<in> nat; j \<in> nat |] ==>length(upt(i,j)) = j #- i"
 apply (induct_tac "j")
 apply (rule_tac [2] sym)
 apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff)
 done
 
-lemma nth_upt [rule_format,simp]:
+lemma nth_upt [rule_format]:
      "[| i \<in> nat; j \<in> nat; k \<in> nat |] ==> i #+ k < j \<longrightarrow> nth(k, upt(i,j)) = i #+ k"
 apply (induct_tac "j", simp)
 apply (simp add: nth_append le_iff)
 apply (auto dest!: not_lt_imp_le
             simp add: nth_append less_diff_conv add_commute)
 done
+declare nth_upt [simp]
 
-lemma take_upt [rule_format,simp]:
+lemma take_upt [rule_format]:
      "[| m \<in> nat; n \<in> nat |] ==>
          \<forall>i \<in> nat. i #+ m \<le> n \<longrightarrow> take(m, upt(i,n)) = upt(i,i#+m)"
 apply (induct_tac "m")
 apply (simp (no_asm_simp) add: take_0)
 apply clarify
 apply (subst upt_rec, simp)
 apply (rule sym)
 apply (subst upt_rec, simp)
 apply (simp_all del: upt.simps)
 apply (rule_tac j = "succ (i #+ x) " in lt_trans2)
 apply auto
 done
+declare take_upt [simp]
 
 lemma map_succ_upt:
      "[| m \<in> nat; n \<in> nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))"
 apply (induct_tac "n")
 apply (auto simp add: map_app_distrib)
 done
 
-lemma nth_map [rule_format,simp]:
+lemma nth_map [rule_format]:
      "xs:list(A) ==>
       \<forall>n \<in> nat. n < length(xs) \<longrightarrow> nth(n, map(f, xs)) = f(nth(n, xs))"
 apply (induct_tac "xs", simp)
 apply (rule ballI)
 apply (induct_tac "n", auto)
 done
+declare nth_map [simp]
 
 lemma nth_map_upt [rule_format]:
      "[| m \<in> nat; n \<in> nat |] ==>
       \<forall>i \<in> nat. i < n #- m \<longrightarrow> nth(i, map(f, upt(m,n))) = f(m #+ i)"
 apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp)
 apply (subst map_succ_upt [symmetric], simp_all, clarify)
 apply (subgoal_tac "i < length (upt (0, x))")
  prefer 2
  apply (simp add: less_diff_conv)
  apply (rule_tac j = "succ (i #+ y) " in lt_trans2)
   apply simp
  apply simp
 apply (subgoal_tac "i < length (upt (y, x))")
  apply (simp_all add: add_commute less_diff_conv)
 done
 
 (** sublist (a generalization of nth to sets) **)
 
 definition
   sublist :: "[i, i] => i"  where
     "sublist(xs, A)==
      map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))"
 
 lemma sublist_0 [simp]: "xs:list(A) ==>sublist(xs, 0) =Nil"
 by (unfold sublist_def, auto)
 
 lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil"
 by (unfold sublist_def, auto)
 
 lemma sublist_shift_lemma:
  "[| xs:list(B); i \<in> nat |] ==>
   map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) =
   map(fst, filter(%p. snd(p):nat & snd(p) #+ i \<in> A, zip(xs,upt(0,length(xs)))))"
 apply (erule list_append_induct)
 apply (simp (no_asm_simp))
 apply (auto simp add: add_commute length_app filter_append map_app_distrib)
 done
 
 lemma sublist_type [simp,TC]:
      "xs:list(B) ==> sublist(xs, A):list(B)"
 apply (unfold sublist_def)
 apply (induct_tac "xs")
 apply (auto simp add: filter_append map_app_distrib)
 done
 
 lemma upt_add_eq_append2:
      "[| i \<in> nat; j \<in> nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)"
 by (simp add: upt_add_eq_append [of 0] nat_0_le)
 
 lemma sublist_append:
  "[| xs:list(B); ys:list(B)  |] ==>
   sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j \<in> nat. j #+ length(xs): A})"
 apply (unfold sublist_def)
 apply (erule_tac l = ys in list_append_induct, simp)
 apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric])
 apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc)
 apply (simp_all add: add_commute)
 done
 
 
 lemma sublist_Cons:
      "[| xs:list(B); x \<in> B |] ==>
       sublist(Cons(x, xs), A) =
       (if 0 \<in> A then [x] else []) @ sublist(xs, {j \<in> nat. succ(j) \<in> A})"
 apply (erule_tac l = xs in list_append_induct)
 apply (simp (no_asm_simp) add: sublist_def)
 apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp)
 done
 
 lemma sublist_singleton [simp]:
      "sublist([x], A) = (if 0 \<in> A then [x] else [])"
 by (simp add: sublist_Cons)
 
-lemma sublist_upt_eq_take [rule_format, simp]:
+lemma sublist_upt_eq_take [rule_format]:
     "xs:list(A) ==> \<forall>n\<in>nat. sublist(xs,n) = take(n,xs)"
 apply (erule list.induct, simp)
 apply (clarify )
 apply (erule natE)
 apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
 done
+declare sublist_upt_eq_take [simp]
 
 lemma sublist_Int_eq:
      "xs \<in> list(B) ==> sublist(xs, A \<inter> nat) = sublist(xs, A)"
 apply (erule list.induct)
 apply (simp_all add: sublist_Cons)
 done
 
 text\<open>Repetition of a List Element\<close>
 
 consts   repeat :: "[i,i]=>i"
 primrec
   "repeat(a,0) = []"
 
   "repeat(a,succ(n)) = Cons(a,repeat(a,n))"
 
 lemma length_repeat: "n \<in> nat ==> length(repeat(a,n)) = n"
 by (induct_tac n, auto)
 
 lemma repeat_succ_app: "n \<in> nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]"
 apply (induct_tac n)
 apply (simp_all del: app_Cons add: app_Cons [symmetric])
 done
 
 lemma repeat_type [TC]: "[|a \<in> A; n \<in> nat|] ==> repeat(a,n) \<in> list(A)"
 by (induct_tac n, auto)
 
 end