# HG changeset patch
# User paulson
# Date 1026981475 -7200
# Node ID b7464ca2ebbb715b32a507f18f25e90bf440ad1c
# Parent  f3e9e8b21aba2095d869e7631b40f5d46bacc126
new theorems to support Constructible proofs

diff -r f3e9e8b21aba -r b7464ca2ebbb src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 17 16:41:32 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 18 10:37:55 2002 +0200
@@ -996,4 +996,26 @@
 text{*NB The proofs for type @{term formula} are virtually identical to those
 for @{term "list(A)"}.  It was a cut-and-paste job! *}
 
+
+subsubsection{*Instantiating the locale @{text M_datatypes}*}
+ML
+{*
+val list_replacement1 = thm "list_replacement1"; 
+val list_replacement2 = thm "list_replacement2";
+val formula_replacement1 = thm "formula_replacement1";
+val formula_replacement2 = thm "formula_replacement2";
+
+val m_datatypes = [list_replacement1, list_replacement2, 
+                   formula_replacement1, formula_replacement2];
+
+fun datatypes_L th =
+    kill_flex_triv_prems (m_datatypes MRS (wfrank_L th));
+
+bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed"));
+bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed"));
+*}
+
+declare list_closed [intro,simp]
+declare formula_closed [intro,simp]
+
 end
diff -r f3e9e8b21aba -r b7464ca2ebbb src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Wed Jul 17 16:41:32 2002 +0200
+++ b/src/ZF/Epsilon.thy	Thu Jul 18 10:37:55 2002 +0200
@@ -116,6 +116,17 @@
 apply (rule subset_refl)
 done
 
+text{*A transitive set either is empty or contains the empty set.*}
+lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A --> 0\<in>A";
+apply (simp add: Transset_def) 
+apply (rule_tac a=x in eps_induct, clarify) 
+apply (drule bspec, assumption) 
+apply (rule_tac P = "x=0" in case_split_thm, auto)
+done
+
+lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A";
+by (blast dest: Transset_0_lemma)
+
 
 subsection{*Epsilon Recursion*}
 
diff -r f3e9e8b21aba -r b7464ca2ebbb src/ZF/List.thy
--- a/src/ZF/List.thy	Wed Jul 17 16:41:32 2002 +0200
+++ b/src/ZF/List.thy	Thu Jul 18 10:37:55 2002 +0200
@@ -86,7 +86,7 @@
 
 primrec
   drop_0:    "drop(0,l) = l"
-  drop_SUCC: "drop(succ(i), l) = tl (drop(i,l))"
+  drop_succ: "drop(succ(i), l) = tl (drop(i,l))"
 
 
 (*** Thanks to Sidi Ehmety for the following ***)
@@ -97,10 +97,11 @@
   "take(n, as) == list_rec(lam n:nat. [],
 		%a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
 
-(* Function `nth' returns the (n+1)th element in a list (not defined at Nil) *)
   nth :: "[i, i]=>i"
+  --{*returns the (n+1)th element of a list, or 0 if the
+   list is too short.*}
   "nth(n, as) == list_rec(lam n:nat. 0,
-		%a l r. lam n:nat. nat_case(a, %m. r`m, n), as)`n"
+ 		          %a l r. lam n:nat. nat_case(a, %m. r`m, n), as) ` n"
 
   list_update :: "[i, i, i]=>i"
   "list_update(xs, i, v) == list_rec(lam n:nat. Nil,
@@ -173,7 +174,11 @@
         c: C(Nil);
         !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))
      |] ==> list_case(c,h,l) : C(l)"
-apply (erule list.induct, auto)
+by (erule list.induct, auto)
+
+lemma list_0_triv: "list(0) = {Nil}"
+apply (rule equalityI, auto) 
+apply (induct_tac x, auto) 
 done
 
 
@@ -203,7 +208,7 @@
 apply (simp_all (no_asm_simp) add: tl_type)
 done
 
-declare drop_SUCC [simp del]
+declare drop_succ [simp del]
 
 
 (** Type checking -- proved by induction, as usual **)
@@ -317,16 +322,12 @@
 (*** theorems about length ***)
 
 lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)"
-apply (induct_tac "xs")
-apply simp_all
-done
+by (induct_tac "xs", simp_all)
 
 lemma length_app [simp]:
      "[| xs: list(A); ys: list(A) |]
       ==> length(xs@ys) = length(xs) #+ length(ys)"
-apply (induct_tac "xs")
-apply simp_all
-done
+by (induct_tac "xs", simp_all)
 
 lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)"
 apply (induct_tac "xs")
@@ -345,19 +346,15 @@
 lemma drop_length_Cons [rule_format]:
      "xs: list(A) ==>
            \<forall>x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
-apply (erule list.induct)
-apply simp_all
-done
+by (erule list.induct, simp_all)
 
 lemma drop_length [rule_format]:
      "l: list(A) ==> \<forall>i \<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
-apply (erule list.induct)
-apply simp_all
+apply (erule list.induct, simp_all)
 apply safe
 apply (erule drop_length_Cons)
 apply (rule natE)
-apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption)
-apply simp_all
+apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all)
 apply (blast intro: succ_in_naturalD length_type)
 done
 
@@ -365,14 +362,10 @@
 (*** theorems about app ***)
 
 lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs"
-apply (erule list.induct)
-apply simp_all
-done
+by (erule list.induct, simp_all)
 
 lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"
-apply (induct_tac "xs")
-apply simp_all
-done
+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")
@@ -412,8 +405,7 @@
 lemma list_add_app:
      "[| xs: list(nat);  ys: list(nat) |]
       ==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)"
-apply (induct_tac "xs")
-apply simp_all
+apply (induct_tac "xs", simp_all)
 done
 
 lemma list_add_rev: "l: list(nat) ==> list_add(rev(l)) = list_add(l)"
@@ -557,7 +549,7 @@
 apply (erule list.induct)
 apply (simp (no_asm_simp))
 apply clarify
-apply (erule_tac a = "ys" in list.cases, auto)
+apply (erule_tac a = ys in list.cases, auto)
 done
 
 lemma append_eq_append [rule_format]:
@@ -566,10 +558,9 @@
    length(us) = length(vs) --> (xs@us = ys@vs) --> (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 (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)
-apply blast
+ apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all, blast)
 done
 
 lemma append_eq_append_iff2 [simp]:
@@ -631,9 +622,8 @@
 
 lemma rev_is_rev_iff [rule_format,simp]:
      "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) <-> xs=ys"
-apply (erule list.induct, force)
-apply clarify
-apply (erule_tac a = "ys" in list.cases, auto)
+apply (erule list.induct, force, clarify)
+apply (erule_tac a = ys in list.cases, auto)
 done
 
 lemma rev_list_elim [rule_format]:
@@ -693,8 +683,7 @@
 
 lemma take_type [rule_format,simp,TC]:
      "xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
-apply (erule list.induct, simp) 
-apply clarify 
+apply (erule list.induct, simp, clarify) 
 apply (erule natE, auto)
 done
 
@@ -702,8 +691,7 @@
  "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) 
-apply clarify 
+apply (erule list.induct, simp, clarify) 
 apply (erule natE, auto)
 done
 
@@ -711,7 +699,7 @@
    "m : 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 (erule_tac a = xs in list.cases)
 apply (auto simp add: take_Nil)
 apply (rotate_tac 1)
 apply (erule natE)
@@ -720,36 +708,41 @@
 
 (** nth **)
 
-lemma nth_0 [simp]: "nth(0, Cons(a, l))= a"
-by (unfold nth_def, auto)
+lemma nth_0 [simp]: "nth(0, Cons(a, l)) = a"
+by (simp add: nth_def) 
+
+lemma nth_Cons [simp]: "n:nat ==> nth(succ(n), Cons(a,l)) = nth(n,l)"
+by (simp add: nth_def) 
 
-lemma nth_Cons [simp]: "n:nat ==> nth(succ(n), Cons(a, l)) = nth(n, l)"
-apply (unfold nth_def)
-apply (simp (no_asm_simp))
+lemma nth_empty [simp]: "nth(n, Nil) = 0"
+by (simp add: nth_def) 
+
+lemma nth_type [rule_format,simp,TC]:
+     "xs:list(A) ==> \<forall>n \<in> nat. n < length(xs) --> nth(n,xs) : A"
+apply (erule list.induct, simp, clarify) 
+apply (erule natE, auto)
 done
 
-lemma nth_type [rule_format,simp,TC]:
-     "xs:list(A) ==> \<forall>n \<in> nat. n < length(xs) --> nth(n, xs):A"
-apply (erule list.induct, simp) 
-apply clarify 
+lemma nth_eq_0 [rule_format]:
+     "xs:list(A) ==> \<forall>n \<in> nat. length(xs) le n --> 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) 
-apply clarify 
+                                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:A. EX i:nat. i<length(xs) & x=nth(i, xs)}"
+     ==> set_of_list(xs) = {x:A. EX i: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 (rule_tac x = 0 in bexI, auto)
 apply (erule natE, auto)
 done
 
@@ -758,19 +751,19 @@
 lemma nth_take_lemma [rule_format]:
  "k:nat ==>
   \<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k le length(xs) --> k le length(ys) -->
-      (\<forall>i \<in> nat. i<k --> nth(i,xs)= nth(i,ys))--> take(k, xs) = take(k,ys))"
+      (\<forall>i \<in> nat. i<k --> nth(i,xs) = nth(i,ys))--> 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 (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)   
+apply (drule_tac x = zs and x1 = ys in bspec [THEN bspec], auto)   
 done
 
 lemma nth_equalityI [rule_format]:
@@ -798,12 +791,9 @@
 done
 
 lemma nth_drop [rule_format]:
-      "n:nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). n #+ i le length(xs)
-                      --> nth(i, drop(n, xs)) = nth(n #+ i, xs)"
-apply (induct_tac "n", simp_all) 
-apply clarify
-apply (erule list.cases) 
-apply (auto elim!: ConsE)
+  "n: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
 
 subsection{*The function zip*}
@@ -849,7 +839,7 @@
 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 (erule_tac a=ys in list.cases, auto) 
 apply (blast intro: list_mono [THEN subsetD]) 
 done
 
@@ -867,7 +857,7 @@
 apply (induct_tac "xs")
 apply (simp (no_asm))
 apply clarify
-apply (erule_tac a = "ys" in list.cases, auto)
+apply (erule_tac a = ys in list.cases, auto)
 done
 
 (* zip length *)
@@ -875,8 +865,7 @@
      "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) 
-apply clarify 
+apply (induct_tac "xs", simp_all, clarify) 
 apply (erule_tac a = ys in list.cases, auto)
 done
 
@@ -884,17 +873,15 @@
  "[| 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) 
-apply clarify 
-apply (erule_tac a = "xs" in list.cases, simp_all) 
+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) 
-apply clarify 
-apply (erule_tac a = "ys" in list.cases, auto)
+apply (induct_tac "xs", force, clarify) 
+apply (erule_tac a = ys in list.cases, auto)
 done
 
 lemma zip_append [simp]:
@@ -907,9 +894,8 @@
 lemma zip_rev [rule_format,simp]:
  "ys:list(B) ==> \<forall>xs \<in> list(A).
     length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
-apply (induct_tac "ys", force) 
-apply clarify 
-apply (erule_tac a = "xs" in list.cases)
+apply (induct_tac "ys", force, clarify) 
+apply (erule_tac a = xs in list.cases)
 apply (auto simp add: length_rev)
 done
 
@@ -917,9 +903,8 @@
    "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
                     i < length(xs) --> i < length(ys) -->
                     nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
-apply (induct_tac "ys", force) 
-apply clarify 
-apply (erule_tac a = "xs" in list.cases, simp) 
+apply (induct_tac "ys", force, clarify) 
+apply (erule_tac a = xs in list.cases, simp) 
 apply (auto elim: natE)
 done
 
@@ -927,7 +912,7 @@
      "[| xs:list(A); ys:list(B); i:nat |]
       ==> set_of_list(zip(xs, ys)) =
           {<x, y>:A*B. EX i:nat. i < min(length(xs), length(ys))
-          & x=nth(i, xs) & y=nth(i, 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 **)
@@ -978,8 +963,8 @@
 
 
 lemma nth_list_update_neq [rule_format,simp]:
-     "xs:list(A) ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i ~= j
-  --> nth(j, list_update(xs, i,x)) = nth(j, xs)"
+  "xs:list(A) ==> 
+     \<forall>i \<in> nat. \<forall>j \<in> nat. i ~= j --> nth(j, list_update(xs,i,x)) = nth(j,xs)"
 apply (induct_tac "xs")
  apply (simp (no_asm))
 apply clarify
@@ -998,8 +983,9 @@
 done
 
 lemma list_update_same_conv [rule_format]:
-     "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs) -->
-  (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
+     "xs:list(A) ==> 
+      \<forall>i \<in> nat. i < length(xs) --> 
+                 (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
 apply (induct_tac "xs")
  apply (simp (no_asm))
 apply clarify
@@ -1007,13 +993,14 @@
 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) -->
-      list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)),
-                                          list_update(ys, i, snd(xy)))"
+     "ys:list(B) ==> 
+      \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A).
+        length(xs) = length(ys) -->
+        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 (erule_tac a = xs in list.cases)
 apply (auto elim: natE)
 done
 
@@ -1023,8 +1010,7 @@
 apply (induct_tac "xs")
  apply simp
 apply (rule ballI)
-apply (erule natE, simp_all)
-apply auto
+apply (erule natE, simp_all, auto)
 done
 
 lemma set_of_list_update_subsetI:
@@ -1068,7 +1054,7 @@
      "[| i le j; j:nat; k: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)
+apply (rule_tac j = j in le_trans, auto)
 done
 
 lemma length_upt [simp]: "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i"
@@ -1079,17 +1065,16 @@
 
 lemma nth_upt [rule_format,simp]:
      "[| i:nat; j:nat; k:nat |] ==> i #+ k < j --> nth(k, upt(i,j)) = i #+ k"
-apply (induct_tac "j")
-apply (simp (no_asm_simp))
-apply (simp add: nth_append le_iff split add: nat_diff_split, safe)
-apply (auto dest!: not_lt_imp_le simp add: nth_append diff_self_eq_0 
-                   less_diff_conv add_commute)
-apply (drule_tac j = "x" in lt_trans2, auto)
+apply (induct_tac "j", simp)
+apply (simp add: nth_append le_iff split add: nat_diff_split)
+apply (auto dest!: not_lt_imp_le 
+            simp add: nth_append diff_self_eq_0 less_diff_conv add_commute)
+apply (drule_tac j = x in lt_trans2, auto)
 done
 
 lemma take_upt [rule_format,simp]:
      "[| m:nat; n:nat |] ==>
-      \<forall>i \<in> nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)"
+         \<forall>i \<in> nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)"
 apply (induct_tac "m")
 apply (simp (no_asm_simp) add: take_0)
 apply clarify
@@ -1118,11 +1103,9 @@
 lemma nth_map_upt [rule_format]:
      "[| m:nat; n:nat |] ==>
       \<forall>i \<in> nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"
-apply (rule_tac n = "m" and m = "n" in diff_induct, typecheck)
-apply simp 
+apply (rule_tac n = m and m = n in diff_induct, typecheck, simp) 
 apply simp 
-apply (subst map_succ_upt [symmetric], simp_all)
-apply clarify 
+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) 
@@ -1170,8 +1153,7 @@
  "[| xs:list(B); ys:list(B)  |] ==>
   sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})"
 apply (unfold sublist_def)
-apply (erule_tac l = "ys" in list_append_induct)
-apply (simp)
+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)
@@ -1182,7 +1164,7 @@
      "[| xs:list(B); x:B |] ==>
       sublist(Cons(x, xs), A) = 
       (if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})"
-apply (erule_tac l = "xs" in list_append_induct)
+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
@@ -1195,13 +1177,33 @@
 lemma sublist_upt_eq_take [simp]:
     "[| xs:list(A); n:nat |] ==> sublist(xs, less_than(n)) = take(n,xs)"
 apply (unfold less_than_def)
-apply (erule_tac l = "xs" in list_append_induct, simp) 
+apply (erule_tac l = xs in list_append_induct, simp) 
 apply (simp split add: nat_diff_split add: sublist_append, auto)
 apply (subgoal_tac "n #- length (y) = 0")
 apply (simp (no_asm_simp))
 apply (auto dest!: not_lt_imp_le simp add: diff_is_0_iff)
 done
 
+text{*Repetition of a List Element*}
+
+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)
+
+
 ML
 {*
 val ConsE = thm "ConsE";