new theorems to support Constructible proofs
authorpaulson
Thu Jul 18 10:37:55 2002 +0200 (2002-07-18)
changeset 13387b7464ca2ebbb
parent 13386 f3e9e8b21aba
child 13388 eff0ede61da1
new theorems to support Constructible proofs
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Epsilon.thy
src/ZF/List.thy
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 17 16:41:32 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 18 10:37:55 2002 +0200
     1.3 @@ -996,4 +996,26 @@
     1.4  text{*NB The proofs for type @{term formula} are virtually identical to those
     1.5  for @{term "list(A)"}.  It was a cut-and-paste job! *}
     1.6  
     1.7 +
     1.8 +subsubsection{*Instantiating the locale @{text M_datatypes}*}
     1.9 +ML
    1.10 +{*
    1.11 +val list_replacement1 = thm "list_replacement1"; 
    1.12 +val list_replacement2 = thm "list_replacement2";
    1.13 +val formula_replacement1 = thm "formula_replacement1";
    1.14 +val formula_replacement2 = thm "formula_replacement2";
    1.15 +
    1.16 +val m_datatypes = [list_replacement1, list_replacement2, 
    1.17 +                   formula_replacement1, formula_replacement2];
    1.18 +
    1.19 +fun datatypes_L th =
    1.20 +    kill_flex_triv_prems (m_datatypes MRS (wfrank_L th));
    1.21 +
    1.22 +bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed"));
    1.23 +bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed"));
    1.24 +*}
    1.25 +
    1.26 +declare list_closed [intro,simp]
    1.27 +declare formula_closed [intro,simp]
    1.28 +
    1.29  end
     2.1 --- a/src/ZF/Epsilon.thy	Wed Jul 17 16:41:32 2002 +0200
     2.2 +++ b/src/ZF/Epsilon.thy	Thu Jul 18 10:37:55 2002 +0200
     2.3 @@ -116,6 +116,17 @@
     2.4  apply (rule subset_refl)
     2.5  done
     2.6  
     2.7 +text{*A transitive set either is empty or contains the empty set.*}
     2.8 +lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A --> 0\<in>A";
     2.9 +apply (simp add: Transset_def) 
    2.10 +apply (rule_tac a=x in eps_induct, clarify) 
    2.11 +apply (drule bspec, assumption) 
    2.12 +apply (rule_tac P = "x=0" in case_split_thm, auto)
    2.13 +done
    2.14 +
    2.15 +lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A";
    2.16 +by (blast dest: Transset_0_lemma)
    2.17 +
    2.18  
    2.19  subsection{*Epsilon Recursion*}
    2.20  
     3.1 --- a/src/ZF/List.thy	Wed Jul 17 16:41:32 2002 +0200
     3.2 +++ b/src/ZF/List.thy	Thu Jul 18 10:37:55 2002 +0200
     3.3 @@ -86,7 +86,7 @@
     3.4  
     3.5  primrec
     3.6    drop_0:    "drop(0,l) = l"
     3.7 -  drop_SUCC: "drop(succ(i), l) = tl (drop(i,l))"
     3.8 +  drop_succ: "drop(succ(i), l) = tl (drop(i,l))"
     3.9  
    3.10  
    3.11  (*** Thanks to Sidi Ehmety for the following ***)
    3.12 @@ -97,10 +97,11 @@
    3.13    "take(n, as) == list_rec(lam n:nat. [],
    3.14  		%a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
    3.15  
    3.16 -(* Function `nth' returns the (n+1)th element in a list (not defined at Nil) *)
    3.17    nth :: "[i, i]=>i"
    3.18 +  --{*returns the (n+1)th element of a list, or 0 if the
    3.19 +   list is too short.*}
    3.20    "nth(n, as) == list_rec(lam n:nat. 0,
    3.21 -		%a l r. lam n:nat. nat_case(a, %m. r`m, n), as)`n"
    3.22 + 		          %a l r. lam n:nat. nat_case(a, %m. r`m, n), as) ` n"
    3.23  
    3.24    list_update :: "[i, i, i]=>i"
    3.25    "list_update(xs, i, v) == list_rec(lam n:nat. Nil,
    3.26 @@ -173,7 +174,11 @@
    3.27          c: C(Nil);
    3.28          !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))
    3.29       |] ==> list_case(c,h,l) : C(l)"
    3.30 -apply (erule list.induct, auto)
    3.31 +by (erule list.induct, auto)
    3.32 +
    3.33 +lemma list_0_triv: "list(0) = {Nil}"
    3.34 +apply (rule equalityI, auto) 
    3.35 +apply (induct_tac x, auto) 
    3.36  done
    3.37  
    3.38  
    3.39 @@ -203,7 +208,7 @@
    3.40  apply (simp_all (no_asm_simp) add: tl_type)
    3.41  done
    3.42  
    3.43 -declare drop_SUCC [simp del]
    3.44 +declare drop_succ [simp del]
    3.45  
    3.46  
    3.47  (** Type checking -- proved by induction, as usual **)
    3.48 @@ -317,16 +322,12 @@
    3.49  (*** theorems about length ***)
    3.50  
    3.51  lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)"
    3.52 -apply (induct_tac "xs")
    3.53 -apply simp_all
    3.54 -done
    3.55 +by (induct_tac "xs", simp_all)
    3.56  
    3.57  lemma length_app [simp]:
    3.58       "[| xs: list(A); ys: list(A) |]
    3.59        ==> length(xs@ys) = length(xs) #+ length(ys)"
    3.60 -apply (induct_tac "xs")
    3.61 -apply simp_all
    3.62 -done
    3.63 +by (induct_tac "xs", simp_all)
    3.64  
    3.65  lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)"
    3.66  apply (induct_tac "xs")
    3.67 @@ -345,19 +346,15 @@
    3.68  lemma drop_length_Cons [rule_format]:
    3.69       "xs: list(A) ==>
    3.70             \<forall>x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
    3.71 -apply (erule list.induct)
    3.72 -apply simp_all
    3.73 -done
    3.74 +by (erule list.induct, simp_all)
    3.75  
    3.76  lemma drop_length [rule_format]:
    3.77       "l: list(A) ==> \<forall>i \<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
    3.78 -apply (erule list.induct)
    3.79 -apply simp_all
    3.80 +apply (erule list.induct, simp_all)
    3.81  apply safe
    3.82  apply (erule drop_length_Cons)
    3.83  apply (rule natE)
    3.84 -apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption)
    3.85 -apply simp_all
    3.86 +apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all)
    3.87  apply (blast intro: succ_in_naturalD length_type)
    3.88  done
    3.89  
    3.90 @@ -365,14 +362,10 @@
    3.91  (*** theorems about app ***)
    3.92  
    3.93  lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs"
    3.94 -apply (erule list.induct)
    3.95 -apply simp_all
    3.96 -done
    3.97 +by (erule list.induct, simp_all)
    3.98  
    3.99  lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"
   3.100 -apply (induct_tac "xs")
   3.101 -apply simp_all
   3.102 -done
   3.103 +by (induct_tac "xs", simp_all)
   3.104  
   3.105  lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"
   3.106  apply (induct_tac "ls")
   3.107 @@ -412,8 +405,7 @@
   3.108  lemma list_add_app:
   3.109       "[| xs: list(nat);  ys: list(nat) |]
   3.110        ==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)"
   3.111 -apply (induct_tac "xs")
   3.112 -apply simp_all
   3.113 +apply (induct_tac "xs", simp_all)
   3.114  done
   3.115  
   3.116  lemma list_add_rev: "l: list(nat) ==> list_add(rev(l)) = list_add(l)"
   3.117 @@ -557,7 +549,7 @@
   3.118  apply (erule list.induct)
   3.119  apply (simp (no_asm_simp))
   3.120  apply clarify
   3.121 -apply (erule_tac a = "ys" in list.cases, auto)
   3.122 +apply (erule_tac a = ys in list.cases, auto)
   3.123  done
   3.124  
   3.125  lemma append_eq_append [rule_format]:
   3.126 @@ -566,10 +558,9 @@
   3.127     length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)"
   3.128  apply (induct_tac "xs")
   3.129  apply (force simp add: length_app, clarify)
   3.130 -apply (erule_tac a = "ys" in list.cases, simp)
   3.131 +apply (erule_tac a = ys in list.cases, simp)
   3.132  apply (subgoal_tac "Cons (a, l) @ us =vs")
   3.133 - apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all)
   3.134 -apply blast
   3.135 + apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all, blast)
   3.136  done
   3.137  
   3.138  lemma append_eq_append_iff2 [simp]:
   3.139 @@ -631,9 +622,8 @@
   3.140  
   3.141  lemma rev_is_rev_iff [rule_format,simp]:
   3.142       "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) <-> xs=ys"
   3.143 -apply (erule list.induct, force)
   3.144 -apply clarify
   3.145 -apply (erule_tac a = "ys" in list.cases, auto)
   3.146 +apply (erule list.induct, force, clarify)
   3.147 +apply (erule_tac a = ys in list.cases, auto)
   3.148  done
   3.149  
   3.150  lemma rev_list_elim [rule_format]:
   3.151 @@ -693,8 +683,7 @@
   3.152  
   3.153  lemma take_type [rule_format,simp,TC]:
   3.154       "xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
   3.155 -apply (erule list.induct, simp) 
   3.156 -apply clarify 
   3.157 +apply (erule list.induct, simp, clarify) 
   3.158  apply (erule natE, auto)
   3.159  done
   3.160  
   3.161 @@ -702,8 +691,7 @@
   3.162   "xs:list(A) ==>
   3.163    \<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) =
   3.164                              take(n, xs) @ take(n #- length(xs), ys)"
   3.165 -apply (erule list.induct, simp) 
   3.166 -apply clarify 
   3.167 +apply (erule list.induct, simp, clarify) 
   3.168  apply (erule natE, auto)
   3.169  done
   3.170  
   3.171 @@ -711,7 +699,7 @@
   3.172     "m : nat ==>
   3.173      \<forall>xs \<in> list(A). \<forall>n \<in> nat. take(n, take(m,xs))= take(min(n, m), xs)"
   3.174  apply (induct_tac "m", auto)
   3.175 -apply (erule_tac a = "xs" in list.cases)
   3.176 +apply (erule_tac a = xs in list.cases)
   3.177  apply (auto simp add: take_Nil)
   3.178  apply (rotate_tac 1)
   3.179  apply (erule natE)
   3.180 @@ -720,36 +708,41 @@
   3.181  
   3.182  (** nth **)
   3.183  
   3.184 -lemma nth_0 [simp]: "nth(0, Cons(a, l))= a"
   3.185 -by (unfold nth_def, auto)
   3.186 +lemma nth_0 [simp]: "nth(0, Cons(a, l)) = a"
   3.187 +by (simp add: nth_def) 
   3.188 +
   3.189 +lemma nth_Cons [simp]: "n:nat ==> nth(succ(n), Cons(a,l)) = nth(n,l)"
   3.190 +by (simp add: nth_def) 
   3.191  
   3.192 -lemma nth_Cons [simp]: "n:nat ==> nth(succ(n), Cons(a, l)) = nth(n, l)"
   3.193 -apply (unfold nth_def)
   3.194 -apply (simp (no_asm_simp))
   3.195 +lemma nth_empty [simp]: "nth(n, Nil) = 0"
   3.196 +by (simp add: nth_def) 
   3.197 +
   3.198 +lemma nth_type [rule_format,simp,TC]:
   3.199 +     "xs:list(A) ==> \<forall>n \<in> nat. n < length(xs) --> nth(n,xs) : A"
   3.200 +apply (erule list.induct, simp, clarify) 
   3.201 +apply (erule natE, auto)
   3.202  done
   3.203  
   3.204 -lemma nth_type [rule_format,simp,TC]:
   3.205 -     "xs:list(A) ==> \<forall>n \<in> nat. n < length(xs) --> nth(n, xs):A"
   3.206 -apply (erule list.induct, simp) 
   3.207 -apply clarify 
   3.208 +lemma nth_eq_0 [rule_format]:
   3.209 +     "xs:list(A) ==> \<forall>n \<in> nat. length(xs) le n --> nth(n,xs) = 0"
   3.210 +apply (erule list.induct, simp, clarify) 
   3.211  apply (erule natE, auto)
   3.212  done
   3.213  
   3.214  lemma nth_append [rule_format]:
   3.215    "xs:list(A) ==> 
   3.216     \<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs)
   3.217 -                                else nth(n #- length(xs),ys))"
   3.218 -apply (induct_tac "xs", simp) 
   3.219 -apply clarify 
   3.220 +                                else nth(n #- length(xs), ys))"
   3.221 +apply (induct_tac "xs", simp, clarify) 
   3.222  apply (erule natE, auto)
   3.223  done
   3.224  
   3.225  lemma set_of_list_conv_nth:
   3.226      "xs:list(A)
   3.227 -      ==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x=nth(i, xs)}"
   3.228 +     ==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x = nth(i,xs)}"
   3.229  apply (induct_tac "xs", simp_all)
   3.230  apply (rule equalityI, auto)
   3.231 -apply (rule_tac x = "0" in bexI, auto)
   3.232 +apply (rule_tac x = 0 in bexI, auto)
   3.233  apply (erule natE, auto)
   3.234  done
   3.235  
   3.236 @@ -758,19 +751,19 @@
   3.237  lemma nth_take_lemma [rule_format]:
   3.238   "k:nat ==>
   3.239    \<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k le length(xs) --> k le length(ys) -->
   3.240 -      (\<forall>i \<in> nat. i<k --> nth(i,xs)= nth(i,ys))--> take(k, xs) = take(k,ys))"
   3.241 +      (\<forall>i \<in> nat. i<k --> nth(i,xs) = nth(i,ys))--> take(k,xs) = take(k,ys))"
   3.242  apply (induct_tac "k")
   3.243  apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib)
   3.244  apply clarify
   3.245  (*Both lists are non-empty*)
   3.246 -apply (erule_tac a="xs" in list.cases, simp) 
   3.247 -apply (erule_tac a="ys" in list.cases, clarify) 
   3.248 +apply (erule_tac a=xs in list.cases, simp) 
   3.249 +apply (erule_tac a=ys in list.cases, clarify) 
   3.250  apply (simp (no_asm_use) )
   3.251  apply clarify
   3.252  apply (simp (no_asm_simp))
   3.253  apply (rule conjI, force)
   3.254  apply (rename_tac y ys z zs) 
   3.255 -apply (drule_tac x = "zs" and x1 = "ys" in bspec [THEN bspec], auto)   
   3.256 +apply (drule_tac x = zs and x1 = ys in bspec [THEN bspec], auto)   
   3.257  done
   3.258  
   3.259  lemma nth_equalityI [rule_format]:
   3.260 @@ -798,12 +791,9 @@
   3.261  done
   3.262  
   3.263  lemma nth_drop [rule_format]:
   3.264 -      "n:nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). n #+ i le length(xs)
   3.265 -                      --> nth(i, drop(n, xs)) = nth(n #+ i, xs)"
   3.266 -apply (induct_tac "n", simp_all) 
   3.267 -apply clarify
   3.268 -apply (erule list.cases) 
   3.269 -apply (auto elim!: ConsE)
   3.270 +  "n:nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)"
   3.271 +apply (induct_tac "n", simp_all, clarify)
   3.272 +apply (erule list.cases, auto)  
   3.273  done
   3.274  
   3.275  subsection{*The function zip*}
   3.276 @@ -849,7 +839,7 @@
   3.277  apply (induct_tac xs) 
   3.278   apply simp_all 
   3.279   apply (blast intro: list_mono [THEN subsetD], clarify) 
   3.280 -apply (erule_tac a=ys in list.cases , auto) 
   3.281 +apply (erule_tac a=ys in list.cases, auto) 
   3.282  apply (blast intro: list_mono [THEN subsetD]) 
   3.283  done
   3.284  
   3.285 @@ -867,7 +857,7 @@
   3.286  apply (induct_tac "xs")
   3.287  apply (simp (no_asm))
   3.288  apply clarify
   3.289 -apply (erule_tac a = "ys" in list.cases, auto)
   3.290 +apply (erule_tac a = ys in list.cases, auto)
   3.291  done
   3.292  
   3.293  (* zip length *)
   3.294 @@ -875,8 +865,7 @@
   3.295       "xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
   3.296                                       min(length(xs), length(ys))"
   3.297  apply (unfold min_def)
   3.298 -apply (induct_tac "xs", simp_all) 
   3.299 -apply clarify 
   3.300 +apply (induct_tac "xs", simp_all, clarify) 
   3.301  apply (erule_tac a = ys in list.cases, auto)
   3.302  done
   3.303  
   3.304 @@ -884,17 +873,15 @@
   3.305   "[| ys:list(A); zs:list(B) |] ==>
   3.306    \<forall>xs \<in> list(A). zip(xs @ ys, zs) = 
   3.307                   zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))"
   3.308 -apply (induct_tac "zs", force) 
   3.309 -apply clarify 
   3.310 -apply (erule_tac a = "xs" in list.cases, simp_all) 
   3.311 +apply (induct_tac "zs", force, clarify) 
   3.312 +apply (erule_tac a = xs in list.cases, simp_all) 
   3.313  done
   3.314  
   3.315  lemma zip_append2 [rule_format]:
   3.316   "[| xs:list(A); zs:list(B) |] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) =
   3.317         zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)"
   3.318 -apply (induct_tac "xs", force) 
   3.319 -apply clarify 
   3.320 -apply (erule_tac a = "ys" in list.cases, auto)
   3.321 +apply (induct_tac "xs", force, clarify) 
   3.322 +apply (erule_tac a = ys in list.cases, auto)
   3.323  done
   3.324  
   3.325  lemma zip_append [simp]:
   3.326 @@ -907,9 +894,8 @@
   3.327  lemma zip_rev [rule_format,simp]:
   3.328   "ys:list(B) ==> \<forall>xs \<in> list(A).
   3.329      length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
   3.330 -apply (induct_tac "ys", force) 
   3.331 -apply clarify 
   3.332 -apply (erule_tac a = "xs" in list.cases)
   3.333 +apply (induct_tac "ys", force, clarify) 
   3.334 +apply (erule_tac a = xs in list.cases)
   3.335  apply (auto simp add: length_rev)
   3.336  done
   3.337  
   3.338 @@ -917,9 +903,8 @@
   3.339     "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
   3.340                      i < length(xs) --> i < length(ys) -->
   3.341                      nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
   3.342 -apply (induct_tac "ys", force) 
   3.343 -apply clarify 
   3.344 -apply (erule_tac a = "xs" in list.cases, simp) 
   3.345 +apply (induct_tac "ys", force, clarify) 
   3.346 +apply (erule_tac a = xs in list.cases, simp) 
   3.347  apply (auto elim: natE)
   3.348  done
   3.349  
   3.350 @@ -927,7 +912,7 @@
   3.351       "[| xs:list(A); ys:list(B); i:nat |]
   3.352        ==> set_of_list(zip(xs, ys)) =
   3.353            {<x, y>:A*B. EX i:nat. i < min(length(xs), length(ys))
   3.354 -          & x=nth(i, xs) & y=nth(i, ys)}"
   3.355 +          & x = nth(i, xs) & y = nth(i, ys)}"
   3.356  by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth)
   3.357  
   3.358  (** list_update **)
   3.359 @@ -978,8 +963,8 @@
   3.360  
   3.361  
   3.362  lemma nth_list_update_neq [rule_format,simp]:
   3.363 -     "xs:list(A) ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i ~= j
   3.364 -  --> nth(j, list_update(xs, i,x)) = nth(j, xs)"
   3.365 +  "xs:list(A) ==> 
   3.366 +     \<forall>i \<in> nat. \<forall>j \<in> nat. i ~= j --> nth(j, list_update(xs,i,x)) = nth(j,xs)"
   3.367  apply (induct_tac "xs")
   3.368   apply (simp (no_asm))
   3.369  apply clarify
   3.370 @@ -998,8 +983,9 @@
   3.371  done
   3.372  
   3.373  lemma list_update_same_conv [rule_format]:
   3.374 -     "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs) -->
   3.375 -  (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
   3.376 +     "xs:list(A) ==> 
   3.377 +      \<forall>i \<in> nat. i < length(xs) --> 
   3.378 +                 (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
   3.379  apply (induct_tac "xs")
   3.380   apply (simp (no_asm))
   3.381  apply clarify
   3.382 @@ -1007,13 +993,14 @@
   3.383  done
   3.384  
   3.385  lemma update_zip [rule_format]:
   3.386 -     "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A).
   3.387 -  length(xs) = length(ys) -->
   3.388 -      list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)),
   3.389 -                                          list_update(ys, i, snd(xy)))"
   3.390 +     "ys:list(B) ==> 
   3.391 +      \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A).
   3.392 +        length(xs) = length(ys) -->
   3.393 +        list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)),
   3.394 +                                              list_update(ys, i, snd(xy)))"
   3.395  apply (induct_tac "ys")
   3.396   apply auto
   3.397 -apply (erule_tac a = "xs" in list.cases)
   3.398 +apply (erule_tac a = xs in list.cases)
   3.399  apply (auto elim: natE)
   3.400  done
   3.401  
   3.402 @@ -1023,8 +1010,7 @@
   3.403  apply (induct_tac "xs")
   3.404   apply simp
   3.405  apply (rule ballI)
   3.406 -apply (erule natE, simp_all)
   3.407 -apply auto
   3.408 +apply (erule natE, simp_all, auto)
   3.409  done
   3.410  
   3.411  lemma set_of_list_update_subsetI:
   3.412 @@ -1068,7 +1054,7 @@
   3.413       "[| i le j; j:nat; k:nat |] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)"
   3.414  apply (induct_tac "k")
   3.415  apply (auto simp add: app_assoc app_type)
   3.416 -apply (rule_tac j = "j" in le_trans, auto)
   3.417 +apply (rule_tac j = j in le_trans, auto)
   3.418  done
   3.419  
   3.420  lemma length_upt [simp]: "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i"
   3.421 @@ -1079,17 +1065,16 @@
   3.422  
   3.423  lemma nth_upt [rule_format,simp]:
   3.424       "[| i:nat; j:nat; k:nat |] ==> i #+ k < j --> nth(k, upt(i,j)) = i #+ k"
   3.425 -apply (induct_tac "j")
   3.426 -apply (simp (no_asm_simp))
   3.427 -apply (simp add: nth_append le_iff split add: nat_diff_split, safe)
   3.428 -apply (auto dest!: not_lt_imp_le simp add: nth_append diff_self_eq_0 
   3.429 -                   less_diff_conv add_commute)
   3.430 -apply (drule_tac j = "x" in lt_trans2, auto)
   3.431 +apply (induct_tac "j", simp)
   3.432 +apply (simp add: nth_append le_iff split add: nat_diff_split)
   3.433 +apply (auto dest!: not_lt_imp_le 
   3.434 +            simp add: nth_append diff_self_eq_0 less_diff_conv add_commute)
   3.435 +apply (drule_tac j = x in lt_trans2, auto)
   3.436  done
   3.437  
   3.438  lemma take_upt [rule_format,simp]:
   3.439       "[| m:nat; n:nat |] ==>
   3.440 -      \<forall>i \<in> nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)"
   3.441 +         \<forall>i \<in> nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)"
   3.442  apply (induct_tac "m")
   3.443  apply (simp (no_asm_simp) add: take_0)
   3.444  apply clarify
   3.445 @@ -1118,11 +1103,9 @@
   3.446  lemma nth_map_upt [rule_format]:
   3.447       "[| m:nat; n:nat |] ==>
   3.448        \<forall>i \<in> nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"
   3.449 -apply (rule_tac n = "m" and m = "n" in diff_induct, typecheck)
   3.450 -apply simp 
   3.451 +apply (rule_tac n = m and m = n in diff_induct, typecheck, simp) 
   3.452  apply simp 
   3.453 -apply (subst map_succ_upt [symmetric], simp_all)
   3.454 -apply clarify 
   3.455 +apply (subst map_succ_upt [symmetric], simp_all, clarify) 
   3.456  apply (subgoal_tac "i < length (upt (0, x))")
   3.457   prefer 2 
   3.458   apply (simp add: less_diff_conv) 
   3.459 @@ -1170,8 +1153,7 @@
   3.460   "[| xs:list(B); ys:list(B)  |] ==>
   3.461    sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})"
   3.462  apply (unfold sublist_def)
   3.463 -apply (erule_tac l = "ys" in list_append_induct)
   3.464 -apply (simp)
   3.465 +apply (erule_tac l = ys in list_append_induct, simp)
   3.466  apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric])
   3.467  apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc)
   3.468  apply (simp_all add: add_commute)
   3.469 @@ -1182,7 +1164,7 @@
   3.470       "[| xs:list(B); x:B |] ==>
   3.471        sublist(Cons(x, xs), A) = 
   3.472        (if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})"
   3.473 -apply (erule_tac l = "xs" in list_append_induct)
   3.474 +apply (erule_tac l = xs in list_append_induct)
   3.475  apply (simp (no_asm_simp) add: sublist_def)  
   3.476  apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp) 
   3.477  done
   3.478 @@ -1195,13 +1177,33 @@
   3.479  lemma sublist_upt_eq_take [simp]:
   3.480      "[| xs:list(A); n:nat |] ==> sublist(xs, less_than(n)) = take(n,xs)"
   3.481  apply (unfold less_than_def)
   3.482 -apply (erule_tac l = "xs" in list_append_induct, simp) 
   3.483 +apply (erule_tac l = xs in list_append_induct, simp) 
   3.484  apply (simp split add: nat_diff_split add: sublist_append, auto)
   3.485  apply (subgoal_tac "n #- length (y) = 0")
   3.486  apply (simp (no_asm_simp))
   3.487  apply (auto dest!: not_lt_imp_le simp add: diff_is_0_iff)
   3.488  done
   3.489  
   3.490 +text{*Repetition of a List Element*}
   3.491 +
   3.492 +consts   repeat :: "[i,i]=>i"
   3.493 +primrec
   3.494 +  "repeat(a,0) = []"
   3.495 +
   3.496 +  "repeat(a,succ(n)) = Cons(a,repeat(a,n))"
   3.497 +
   3.498 +lemma length_repeat: "n \<in> nat ==> length(repeat(a,n)) = n"
   3.499 +by (induct_tac n, auto)
   3.500 +
   3.501 +lemma repeat_succ_app: "n \<in> nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]"
   3.502 +apply (induct_tac n)
   3.503 +apply (simp_all del: app_Cons add: app_Cons [symmetric])
   3.504 +done
   3.505 +
   3.506 +lemma repeat_type [TC]: "[|a \<in> A; n \<in> nat|] ==> repeat(a,n) \<in> list(A)"
   3.507 +by (induct_tac n, auto)
   3.508 +
   3.509 +
   3.510  ML
   3.511  {*
   3.512  val ConsE = thm "ConsE";