src/ZF/List_ZF.thy
 author wenzelm Sun Nov 09 17:04:14 2014 +0100 (2014-11-09) changeset 58957 c9e744ea8a38 parent 58871 c399ae4b836f child 60770 240563fbf41d permissions -rw-r--r--
proper context for match_tac etc.;
```     1 (*  Title:      ZF/List_ZF.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   1994  University of Cambridge
```
```     4 *)
```
```     5
```
```     6 section{*Lists in Zermelo-Fraenkel Set Theory*}
```
```     7
```
```     8 theory List_ZF imports Datatype_ZF ArithSimp begin
```
```     9
```
```    10 consts
```
```    11   list       :: "i=>i"
```
```    12
```
```    13 datatype
```
```    14   "list(A)" = Nil | Cons ("a \<in> A", "l \<in> list(A)")
```
```    15
```
```    16
```
```    17 syntax
```
```    18  "_Nil" :: i  ("[]")
```
```    19  "_List" :: "is => i"  ("[(_)]")
```
```    20
```
```    21 translations
```
```    22   "[x, xs]"     == "CONST Cons(x, [xs])"
```
```    23   "[x]"         == "CONST Cons(x, [])"
```
```    24   "[]"          == "CONST Nil"
```
```    25
```
```    26
```
```    27 consts
```
```    28   length :: "i=>i"
```
```    29   hd     :: "i=>i"
```
```    30   tl     :: "i=>i"
```
```    31
```
```    32 primrec
```
```    33   "length([]) = 0"
```
```    34   "length(Cons(a,l)) = succ(length(l))"
```
```    35
```
```    36 primrec
```
```    37   "hd([]) = 0"
```
```    38   "hd(Cons(a,l)) = a"
```
```    39
```
```    40 primrec
```
```    41   "tl([]) = []"
```
```    42   "tl(Cons(a,l)) = l"
```
```    43
```
```    44
```
```    45 consts
```
```    46   map         :: "[i=>i, i] => i"
```
```    47   set_of_list :: "i=>i"
```
```    48   app         :: "[i,i]=>i"                        (infixr "@" 60)
```
```    49
```
```    50 (*map is a binding operator -- it applies to meta-level functions, not
```
```    51 object-level functions.  This simplifies the final form of term_rec_conv,
```
```    52 although complicating its derivation.*)
```
```    53 primrec
```
```    54   "map(f,[]) = []"
```
```    55   "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
```
```    56
```
```    57 primrec
```
```    58   "set_of_list([]) = 0"
```
```    59   "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))"
```
```    60
```
```    61 primrec
```
```    62   app_Nil:  "[] @ ys = ys"
```
```    63   app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
```
```    64
```
```    65
```
```    66 consts
```
```    67   rev :: "i=>i"
```
```    68   flat       :: "i=>i"
```
```    69   list_add   :: "i=>i"
```
```    70
```
```    71 primrec
```
```    72   "rev([]) = []"
```
```    73   "rev(Cons(a,l)) = rev(l) @ [a]"
```
```    74
```
```    75 primrec
```
```    76   "flat([]) = []"
```
```    77   "flat(Cons(l,ls)) = l @ flat(ls)"
```
```    78
```
```    79 primrec
```
```    80   "list_add([]) = 0"
```
```    81   "list_add(Cons(a,l)) = a #+ list_add(l)"
```
```    82
```
```    83 consts
```
```    84   drop       :: "[i,i]=>i"
```
```    85
```
```    86 primrec
```
```    87   drop_0:    "drop(0,l) = l"
```
```    88   drop_succ: "drop(succ(i), l) = tl (drop(i,l))"
```
```    89
```
```    90
```
```    91 (*** Thanks to Sidi Ehmety for the following ***)
```
```    92
```
```    93 definition
```
```    94 (* Function `take' returns the first n elements of a list *)
```
```    95   take     :: "[i,i]=>i"  where
```
```    96   "take(n, as) == list_rec(\<lambda>n\<in>nat. [],
```
```    97                 %a l r. \<lambda>n\<in>nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
```
```    98
```
```    99 definition
```
```   100   nth :: "[i, i]=>i"  where
```
```   101   --{*returns the (n+1)th element of a list, or 0 if the
```
```   102    list is too short.*}
```
```   103   "nth(n, as) == list_rec(\<lambda>n\<in>nat. 0,
```
```   104                           %a l r. \<lambda>n\<in>nat. nat_case(a, %m. r`m, n), as) ` n"
```
```   105
```
```   106 definition
```
```   107   list_update :: "[i, i, i]=>i"  where
```
```   108   "list_update(xs, i, v) == list_rec(\<lambda>n\<in>nat. Nil,
```
```   109       %u us vs. \<lambda>n\<in>nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i"
```
```   110
```
```   111 consts
```
```   112   filter :: "[i=>o, i] => i"
```
```   113   upt :: "[i, i] =>i"
```
```   114
```
```   115 primrec
```
```   116   "filter(P, Nil) = Nil"
```
```   117   "filter(P, Cons(x, xs)) =
```
```   118      (if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))"
```
```   119
```
```   120 primrec
```
```   121   "upt(i, 0) = Nil"
```
```   122   "upt(i, succ(j)) = (if i \<le> j then upt(i, j)@[j] else Nil)"
```
```   123
```
```   124 definition
```
```   125   min :: "[i,i] =>i"  where
```
```   126     "min(x, y) == (if x \<le> y then x else y)"
```
```   127
```
```   128 definition
```
```   129   max :: "[i, i] =>i"  where
```
```   130     "max(x, y) == (if x \<le> y then y else x)"
```
```   131
```
```   132 (*** Aspects of the datatype definition ***)
```
```   133
```
```   134 declare list.intros [simp,TC]
```
```   135
```
```   136 (*An elimination rule, for type-checking*)
```
```   137 inductive_cases ConsE: "Cons(a,l) \<in> list(A)"
```
```   138
```
```   139 lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) \<longleftrightarrow> a \<in> A & l \<in> list(A)"
```
```   140 by (blast elim: ConsE)
```
```   141
```
```   142 (*Proving freeness results*)
```
```   143 lemma Cons_iff: "Cons(a,l)=Cons(a',l') \<longleftrightarrow> a=a' & l=l'"
```
```   144 by auto
```
```   145
```
```   146 lemma Nil_Cons_iff: "~ Nil=Cons(a,l)"
```
```   147 by auto
```
```   148
```
```   149 lemma list_unfold: "list(A) = {0} + (A * list(A))"
```
```   150 by (blast intro!: list.intros [unfolded list.con_defs]
```
```   151           elim: list.cases [unfolded list.con_defs])
```
```   152
```
```   153
```
```   154 (**  Lemmas to justify using "list" in other recursive type definitions **)
```
```   155
```
```   156 lemma list_mono: "A<=B ==> list(A) \<subseteq> list(B)"
```
```   157 apply (unfold list.defs )
```
```   158 apply (rule lfp_mono)
```
```   159 apply (simp_all add: list.bnd_mono)
```
```   160 apply (assumption | rule univ_mono basic_monos)+
```
```   161 done
```
```   162
```
```   163 (*There is a similar proof by list induction.*)
```
```   164 lemma list_univ: "list(univ(A)) \<subseteq> univ(A)"
```
```   165 apply (unfold list.defs list.con_defs)
```
```   166 apply (rule lfp_lowerbound)
```
```   167 apply (rule_tac [2] A_subset_univ [THEN univ_mono])
```
```   168 apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
```
```   169 done
```
```   170
```
```   171 (*These two theorems justify datatypes involving list(nat), list(A), ...*)
```
```   172 lemmas list_subset_univ = subset_trans [OF list_mono list_univ]
```
```   173
```
```   174 lemma list_into_univ: "[| l \<in> list(A);  A \<subseteq> univ(B) |] ==> l \<in> univ(B)"
```
```   175 by (blast intro: list_subset_univ [THEN subsetD])
```
```   176
```
```   177 lemma list_case_type:
```
```   178     "[| l \<in> list(A);
```
```   179         c \<in> C(Nil);
```
```   180         !!x y. [| x \<in> A;  y \<in> list(A) |] ==> h(x,y): C(Cons(x,y))
```
```   181      |] ==> list_case(c,h,l) \<in> C(l)"
```
```   182 by (erule list.induct, auto)
```
```   183
```
```   184 lemma list_0_triv: "list(0) = {Nil}"
```
```   185 apply (rule equalityI, auto)
```
```   186 apply (induct_tac x, auto)
```
```   187 done
```
```   188
```
```   189
```
```   190 (*** List functions ***)
```
```   191
```
```   192 lemma tl_type: "l \<in> list(A) ==> tl(l) \<in> list(A)"
```
```   193 apply (induct_tac "l")
```
```   194 apply (simp_all (no_asm_simp) add: list.intros)
```
```   195 done
```
```   196
```
```   197 (** drop **)
```
```   198
```
```   199 lemma drop_Nil [simp]: "i \<in> nat ==> drop(i, Nil) = Nil"
```
```   200 apply (induct_tac "i")
```
```   201 apply (simp_all (no_asm_simp))
```
```   202 done
```
```   203
```
```   204 lemma drop_succ_Cons [simp]: "i \<in> nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"
```
```   205 apply (rule sym)
```
```   206 apply (induct_tac "i")
```
```   207 apply (simp (no_asm))
```
```   208 apply (simp (no_asm_simp))
```
```   209 done
```
```   210
```
```   211 lemma drop_type [simp,TC]: "[| i \<in> nat; l \<in> list(A) |] ==> drop(i,l) \<in> list(A)"
```
```   212 apply (induct_tac "i")
```
```   213 apply (simp_all (no_asm_simp) add: tl_type)
```
```   214 done
```
```   215
```
```   216 declare drop_succ [simp del]
```
```   217
```
```   218
```
```   219 (** Type checking -- proved by induction, as usual **)
```
```   220
```
```   221 lemma list_rec_type [TC]:
```
```   222     "[| l \<in> list(A);
```
```   223         c \<in> C(Nil);
```
```   224         !!x y r. [| x \<in> A;  y \<in> list(A);  r \<in> C(y) |] ==> h(x,y,r): C(Cons(x,y))
```
```   225      |] ==> list_rec(c,h,l) \<in> C(l)"
```
```   226 by (induct_tac "l", auto)
```
```   227
```
```   228 (** map **)
```
```   229
```
```   230 lemma map_type [TC]:
```
```   231     "[| l \<in> list(A);  !!x. x \<in> A ==> h(x): B |] ==> map(h,l) \<in> list(B)"
```
```   232 apply (simp add: map_list_def)
```
```   233 apply (typecheck add: list.intros list_rec_type, blast)
```
```   234 done
```
```   235
```
```   236 lemma map_type2 [TC]: "l \<in> list(A) ==> map(h,l) \<in> list({h(u). u \<in> A})"
```
```   237 apply (erule map_type)
```
```   238 apply (erule RepFunI)
```
```   239 done
```
```   240
```
```   241 (** length **)
```
```   242
```
```   243 lemma length_type [TC]: "l \<in> list(A) ==> length(l) \<in> nat"
```
```   244 by (simp add: length_list_def)
```
```   245
```
```   246 lemma lt_length_in_nat:
```
```   247    "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
```
```   248 by (frule lt_nat_in_nat, typecheck)
```
```   249
```
```   250 (** app **)
```
```   251
```
```   252 lemma app_type [TC]: "[| xs: list(A);  ys: list(A) |] ==> xs@ys \<in> list(A)"
```
```   253 by (simp add: app_list_def)
```
```   254
```
```   255 (** rev **)
```
```   256
```
```   257 lemma rev_type [TC]: "xs: list(A) ==> rev(xs) \<in> list(A)"
```
```   258 by (simp add: rev_list_def)
```
```   259
```
```   260
```
```   261 (** flat **)
```
```   262
```
```   263 lemma flat_type [TC]: "ls: list(list(A)) ==> flat(ls) \<in> list(A)"
```
```   264 by (simp add: flat_list_def)
```
```   265
```
```   266
```
```   267 (** set_of_list **)
```
```   268
```
```   269 lemma set_of_list_type [TC]: "l \<in> list(A) ==> set_of_list(l) \<in> Pow(A)"
```
```   270 apply (unfold set_of_list_list_def)
```
```   271 apply (erule list_rec_type, auto)
```
```   272 done
```
```   273
```
```   274 lemma set_of_list_append:
```
```   275      "xs: list(A) ==> set_of_list (xs@ys) = set_of_list(xs) \<union> set_of_list(ys)"
```
```   276 apply (erule list.induct)
```
```   277 apply (simp_all (no_asm_simp) add: Un_cons)
```
```   278 done
```
```   279
```
```   280
```
```   281 (** list_add **)
```
```   282
```
```   283 lemma list_add_type [TC]: "xs: list(nat) ==> list_add(xs) \<in> nat"
```
```   284 by (simp add: list_add_list_def)
```
```   285
```
```   286
```
```   287 (*** theorems about map ***)
```
```   288
```
```   289 lemma map_ident [simp]: "l \<in> list(A) ==> map(%u. u, l) = l"
```
```   290 apply (induct_tac "l")
```
```   291 apply (simp_all (no_asm_simp))
```
```   292 done
```
```   293
```
```   294 lemma map_compose: "l \<in> list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)"
```
```   295 apply (induct_tac "l")
```
```   296 apply (simp_all (no_asm_simp))
```
```   297 done
```
```   298
```
```   299 lemma map_app_distrib: "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"
```
```   300 apply (induct_tac "xs")
```
```   301 apply (simp_all (no_asm_simp))
```
```   302 done
```
```   303
```
```   304 lemma map_flat: "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"
```
```   305 apply (induct_tac "ls")
```
```   306 apply (simp_all (no_asm_simp) add: map_app_distrib)
```
```   307 done
```
```   308
```
```   309 lemma list_rec_map:
```
```   310      "l \<in> list(A) ==>
```
```   311       list_rec(c, d, map(h,l)) =
```
```   312       list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)"
```
```   313 apply (induct_tac "l")
```
```   314 apply (simp_all (no_asm_simp))
```
```   315 done
```
```   316
```
```   317 (** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **)
```
```   318
```
```   319 (* @{term"c \<in> list(Collect(B,P)) ==> c \<in> list"} *)
```
```   320 lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD]
```
```   321
```
```   322 lemma map_list_Collect: "l \<in> list({x \<in> A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"
```
```   323 apply (induct_tac "l")
```
```   324 apply (simp_all (no_asm_simp))
```
```   325 done
```
```   326
```
```   327 (*** theorems about length ***)
```
```   328
```
```   329 lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)"
```
```   330 by (induct_tac "xs", simp_all)
```
```   331
```
```   332 lemma length_app [simp]:
```
```   333      "[| xs: list(A); ys: list(A) |]
```
```   334       ==> length(xs@ys) = length(xs) #+ length(ys)"
```
```   335 by (induct_tac "xs", simp_all)
```
```   336
```
```   337 lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)"
```
```   338 apply (induct_tac "xs")
```
```   339 apply (simp_all (no_asm_simp) add: length_app)
```
```   340 done
```
```   341
```
```   342 lemma length_flat:
```
```   343      "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"
```
```   344 apply (induct_tac "ls")
```
```   345 apply (simp_all (no_asm_simp) add: length_app)
```
```   346 done
```
```   347
```
```   348 (** Length and drop **)
```
```   349
```
```   350 (*Lemma for the inductive step of drop_length*)
```
```   351 lemma drop_length_Cons [rule_format]:
```
```   352      "xs: list(A) ==>
```
```   353            \<forall>x.  \<exists>z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
```
```   354 by (erule list.induct, simp_all)
```
```   355
```
```   356 lemma drop_length [rule_format]:
```
```   357      "l \<in> list(A) ==> \<forall>i \<in> length(l). (\<exists>z zs. drop(i,l) = Cons(z,zs))"
```
```   358 apply (erule list.induct, simp_all, safe)
```
```   359 apply (erule drop_length_Cons)
```
```   360 apply (rule natE)
```
```   361 apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all)
```
```   362 apply (blast intro: succ_in_naturalD length_type)
```
```   363 done
```
```   364
```
```   365
```
```   366 (*** theorems about app ***)
```
```   367
```
```   368 lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs"
```
```   369 by (erule list.induct, simp_all)
```
```   370
```
```   371 lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"
```
```   372 by (induct_tac "xs", simp_all)
```
```   373
```
```   374 lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"
```
```   375 apply (induct_tac "ls")
```
```   376 apply (simp_all (no_asm_simp) add: app_assoc)
```
```   377 done
```
```   378
```
```   379 (*** theorems about rev ***)
```
```   380
```
```   381 lemma rev_map_distrib: "l \<in> list(A) ==> rev(map(h,l)) = map(h,rev(l))"
```
```   382 apply (induct_tac "l")
```
```   383 apply (simp_all (no_asm_simp) add: map_app_distrib)
```
```   384 done
```
```   385
```
```   386 (*Simplifier needs the premises as assumptions because rewriting will not
```
```   387   instantiate the variable ?A in the rules' typing conditions; note that
```
```   388   rev_type does not instantiate ?A.  Only the premises do.
```
```   389 *)
```
```   390 lemma rev_app_distrib:
```
```   391      "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"
```
```   392 apply (erule list.induct)
```
```   393 apply (simp_all add: app_assoc)
```
```   394 done
```
```   395
```
```   396 lemma rev_rev_ident [simp]: "l \<in> list(A) ==> rev(rev(l))=l"
```
```   397 apply (induct_tac "l")
```
```   398 apply (simp_all (no_asm_simp) add: rev_app_distrib)
```
```   399 done
```
```   400
```
```   401 lemma rev_flat: "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"
```
```   402 apply (induct_tac "ls")
```
```   403 apply (simp_all add: map_app_distrib flat_app_distrib rev_app_distrib)
```
```   404 done
```
```   405
```
```   406
```
```   407 (*** theorems about list_add ***)
```
```   408
```
```   409 lemma list_add_app:
```
```   410      "[| xs: list(nat);  ys: list(nat) |]
```
```   411       ==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)"
```
```   412 apply (induct_tac "xs", simp_all)
```
```   413 done
```
```   414
```
```   415 lemma list_add_rev: "l \<in> list(nat) ==> list_add(rev(l)) = list_add(l)"
```
```   416 apply (induct_tac "l")
```
```   417 apply (simp_all (no_asm_simp) add: list_add_app)
```
```   418 done
```
```   419
```
```   420 lemma list_add_flat:
```
```   421      "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"
```
```   422 apply (induct_tac "ls")
```
```   423 apply (simp_all (no_asm_simp) add: list_add_app)
```
```   424 done
```
```   425
```
```   426 (** New induction rules **)
```
```   427
```
```   428 lemma list_append_induct [case_names Nil snoc, consumes 1]:
```
```   429     "[| l \<in> list(A);
```
```   430         P(Nil);
```
```   431         !!x y. [| x \<in> A;  y \<in> list(A);  P(y) |] ==> P(y @ [x])
```
```   432      |] ==> P(l)"
```
```   433 apply (subgoal_tac "P(rev(rev(l)))", simp)
```
```   434 apply (erule rev_type [THEN list.induct], simp_all)
```
```   435 done
```
```   436
```
```   437 lemma list_complete_induct_lemma [rule_format]:
```
```   438  assumes ih:
```
```   439     "\<And>l. [| l \<in> list(A);
```
```   440              \<forall>l' \<in> list(A). length(l') < length(l) \<longrightarrow> P(l')|]
```
```   441           ==> P(l)"
```
```   442   shows "n \<in> nat ==> \<forall>l \<in> list(A). length(l) < n \<longrightarrow> P(l)"
```
```   443 apply (induct_tac n, simp)
```
```   444 apply (blast intro: ih elim!: leE)
```
```   445 done
```
```   446
```
```   447 theorem list_complete_induct:
```
```   448       "[| l \<in> list(A);
```
```   449           \<And>l. [| l \<in> list(A);
```
```   450                   \<forall>l' \<in> list(A). length(l') < length(l) \<longrightarrow> P(l')|]
```
```   451                ==> P(l)
```
```   452        |] ==> P(l)"
```
```   453 apply (rule list_complete_induct_lemma [of A])
```
```   454    prefer 4 apply (rule le_refl, simp)
```
```   455   apply blast
```
```   456  apply simp
```
```   457 apply assumption
```
```   458 done
```
```   459
```
```   460
```
```   461 (*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)
```
```   462
```
```   463 (** min FIXME: replace by Int! **)
```
```   464 (* Min theorems are also true for i, j ordinals *)
```
```   465 lemma min_sym: "[| i \<in> nat; j \<in> nat |] ==> min(i,j)=min(j,i)"
```
```   466 apply (unfold min_def)
```
```   467 apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym)
```
```   468 done
```
```   469
```
```   470 lemma min_type [simp,TC]: "[| i \<in> nat; j \<in> nat |] ==> min(i,j):nat"
```
```   471 by (unfold min_def, auto)
```
```   472
```
```   473 lemma min_0 [simp]: "i \<in> nat ==> min(0,i) = 0"
```
```   474 apply (unfold min_def)
```
```   475 apply (auto dest: not_lt_imp_le)
```
```   476 done
```
```   477
```
```   478 lemma min_02 [simp]: "i \<in> nat ==> min(i, 0) = 0"
```
```   479 apply (unfold min_def)
```
```   480 apply (auto dest: not_lt_imp_le)
```
```   481 done
```
```   482
```
```   483 lemma lt_min_iff: "[| i \<in> nat; j \<in> nat; k \<in> nat |] ==> i<min(j,k) \<longleftrightarrow> i<j & i<k"
```
```   484 apply (unfold min_def)
```
```   485 apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
```
```   486 done
```
```   487
```
```   488 lemma min_succ_succ [simp]:
```
```   489      "[| i \<in> nat; j \<in> nat |] ==>  min(succ(i), succ(j))= succ(min(i, j))"
```
```   490 apply (unfold min_def, auto)
```
```   491 done
```
```   492
```
```   493 (*** more theorems about lists ***)
```
```   494
```
```   495 (** filter **)
```
```   496
```
```   497 lemma filter_append [simp]:
```
```   498      "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)"
```
```   499 by (induct_tac "xs", auto)
```
```   500
```
```   501 lemma filter_type [simp,TC]: "xs:list(A) ==> filter(P, xs):list(A)"
```
```   502 by (induct_tac "xs", auto)
```
```   503
```
```   504 lemma length_filter: "xs:list(A) ==> length(filter(P, xs)) \<le> length(xs)"
```
```   505 apply (induct_tac "xs", auto)
```
```   506 apply (rule_tac j = "length (l) " in le_trans)
```
```   507 apply (auto simp add: le_iff)
```
```   508 done
```
```   509
```
```   510 lemma filter_is_subset: "xs:list(A) ==> set_of_list(filter(P,xs)) \<subseteq> set_of_list(xs)"
```
```   511 by (induct_tac "xs", auto)
```
```   512
```
```   513 lemma filter_False [simp]: "xs:list(A) ==> filter(%p. False, xs) = Nil"
```
```   514 by (induct_tac "xs", auto)
```
```   515
```
```   516 lemma filter_True [simp]: "xs:list(A) ==> filter(%p. True, xs) = xs"
```
```   517 by (induct_tac "xs", auto)
```
```   518
```
```   519 (** length **)
```
```   520
```
```   521 lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 \<longleftrightarrow> xs=Nil"
```
```   522 by (erule list.induct, auto)
```
```   523
```
```   524 lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) \<longleftrightarrow> xs=Nil"
```
```   525 by (erule list.induct, auto)
```
```   526
```
```   527 lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1"
```
```   528 by (erule list.induct, auto)
```
```   529
```
```   530 lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) \<longleftrightarrow> xs \<noteq> Nil"
```
```   531 by (erule list.induct, auto)
```
```   532
```
```   533 lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) \<longleftrightarrow> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)"
```
```   534 by (erule list.induct, auto)
```
```   535
```
```   536 (** more theorems about append **)
```
```   537
```
```   538 lemma append_is_Nil_iff [simp]:
```
```   539      "xs:list(A) ==> (xs@ys = Nil) \<longleftrightarrow> (xs=Nil & ys = Nil)"
```
```   540 by (erule list.induct, auto)
```
```   541
```
```   542 lemma append_is_Nil_iff2 [simp]:
```
```   543      "xs:list(A) ==> (Nil = xs@ys) \<longleftrightarrow> (xs=Nil & ys = Nil)"
```
```   544 by (erule list.induct, auto)
```
```   545
```
```   546 lemma append_left_is_self_iff [simp]:
```
```   547      "xs:list(A) ==> (xs@ys = xs) \<longleftrightarrow> (ys = Nil)"
```
```   548 by (erule list.induct, auto)
```
```   549
```
```   550 lemma append_left_is_self_iff2 [simp]:
```
```   551      "xs:list(A) ==> (xs = xs@ys) \<longleftrightarrow> (ys = Nil)"
```
```   552 by (erule list.induct, auto)
```
```   553
```
```   554 (*TOO SLOW as a default simprule!*)
```
```   555 lemma append_left_is_Nil_iff [rule_format]:
```
```   556      "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
```
```   557    length(ys)=length(zs) \<longrightarrow> (xs@ys=zs \<longleftrightarrow> (xs=Nil & ys=zs))"
```
```   558 apply (erule list.induct)
```
```   559 apply (auto simp add: length_app)
```
```   560 done
```
```   561
```
```   562 (*TOO SLOW as a default simprule!*)
```
```   563 lemma append_left_is_Nil_iff2 [rule_format]:
```
```   564      "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
```
```   565    length(ys)=length(zs) \<longrightarrow> (zs=ys@xs \<longleftrightarrow> (xs=Nil & ys=zs))"
```
```   566 apply (erule list.induct)
```
```   567 apply (auto simp add: length_app)
```
```   568 done
```
```   569
```
```   570 lemma append_eq_append_iff [rule_format,simp]:
```
```   571      "xs:list(A) ==> \<forall>ys \<in> list(A).
```
```   572       length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys & us=vs)"
```
```   573 apply (erule list.induct)
```
```   574 apply (simp (no_asm_simp))
```
```   575 apply clarify
```
```   576 apply (erule_tac a = ys in list.cases, auto)
```
```   577 done
```
```   578
```
```   579 lemma append_eq_append [rule_format]:
```
```   580   "xs:list(A) ==>
```
```   581    \<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> list(A).
```
```   582    length(us) = length(vs) \<longrightarrow> (xs@us = ys@vs) \<longrightarrow> (xs=ys & us=vs)"
```
```   583 apply (induct_tac "xs")
```
```   584 apply (force simp add: length_app, clarify)
```
```   585 apply (erule_tac a = ys in list.cases, simp)
```
```   586 apply (subgoal_tac "Cons (a, l) @ us =vs")
```
```   587  apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all, blast)
```
```   588 done
```
```   589
```
```   590 lemma append_eq_append_iff2 [simp]:
```
```   591  "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |]
```
```   592   ==>  xs@us = ys@vs \<longleftrightarrow> (xs=ys & us=vs)"
```
```   593 apply (rule iffI)
```
```   594 apply (rule append_eq_append, auto)
```
```   595 done
```
```   596
```
```   597 lemma append_self_iff [simp]:
```
```   598      "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs \<longleftrightarrow> ys=zs"
```
```   599 by simp
```
```   600
```
```   601 lemma append_self_iff2 [simp]:
```
```   602      "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs \<longleftrightarrow> ys=zs"
```
```   603 by simp
```
```   604
```
```   605 (* Can also be proved from append_eq_append_iff2,
```
```   606 but the proof requires two more hypotheses: x \<in> A and y \<in> A *)
```
```   607 lemma append1_eq_iff [rule_format,simp]:
```
```   608      "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)"
```
```   609 apply (erule list.induct)
```
```   610  apply clarify
```
```   611  apply (erule list.cases)
```
```   612  apply simp_all
```
```   613 txt{*Inductive step*}
```
```   614 apply clarify
```
```   615 apply (erule_tac a=ys in list.cases, simp_all)
```
```   616 done
```
```   617
```
```   618
```
```   619 lemma append_right_is_self_iff [simp]:
```
```   620      "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) \<longleftrightarrow> (xs=Nil)"
```
```   621 by (simp (no_asm_simp) add: append_left_is_Nil_iff)
```
```   622
```
```   623 lemma append_right_is_self_iff2 [simp]:
```
```   624      "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) \<longleftrightarrow> (xs=Nil)"
```
```   625 apply (rule iffI)
```
```   626 apply (drule sym, auto)
```
```   627 done
```
```   628
```
```   629 lemma hd_append [rule_format,simp]:
```
```   630      "xs:list(A) ==> xs \<noteq> Nil \<longrightarrow> hd(xs @ ys) = hd(xs)"
```
```   631 by (induct_tac "xs", auto)
```
```   632
```
```   633 lemma tl_append [rule_format,simp]:
```
```   634      "xs:list(A) ==> xs\<noteq>Nil \<longrightarrow> tl(xs @ ys) = tl(xs)@ys"
```
```   635 by (induct_tac "xs", auto)
```
```   636
```
```   637 (** rev **)
```
```   638 lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil \<longleftrightarrow> xs = Nil)"
```
```   639 by (erule list.induct, auto)
```
```   640
```
```   641 lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) \<longleftrightarrow> xs = Nil)"
```
```   642 by (erule list.induct, auto)
```
```   643
```
```   644 lemma rev_is_rev_iff [rule_format,simp]:
```
```   645      "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) \<longleftrightarrow> xs=ys"
```
```   646 apply (erule list.induct, force, clarify)
```
```   647 apply (erule_tac a = ys in list.cases, auto)
```
```   648 done
```
```   649
```
```   650 lemma rev_list_elim [rule_format]:
```
```   651      "xs:list(A) ==>
```
```   652       (xs=Nil \<longrightarrow> P) \<longrightarrow> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] \<longrightarrow>P)\<longrightarrow>P"
```
```   653 by (erule list_append_induct, auto)
```
```   654
```
```   655
```
```   656 (** more theorems about drop **)
```
```   657
```
```   658 lemma length_drop [rule_format,simp]:
```
```   659      "n \<in> nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) #- n"
```
```   660 apply (erule nat_induct)
```
```   661 apply (auto elim: list.cases)
```
```   662 done
```
```   663
```
```   664 lemma drop_all [rule_format,simp]:
```
```   665      "n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n \<longrightarrow> drop(n, xs)=Nil"
```
```   666 apply (erule nat_induct)
```
```   667 apply (auto elim: list.cases)
```
```   668 done
```
```   669
```
```   670 lemma drop_append [rule_format]:
```
```   671      "n \<in> nat ==>
```
```   672       \<forall>xs \<in> list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)"
```
```   673 apply (induct_tac "n")
```
```   674 apply (auto elim: list.cases)
```
```   675 done
```
```   676
```
```   677 lemma drop_drop:
```
```   678     "m \<in> nat ==> \<forall>xs \<in> list(A). \<forall>n \<in> nat. drop(n, drop(m, xs))=drop(n #+ m, xs)"
```
```   679 apply (induct_tac "m")
```
```   680 apply (auto elim: list.cases)
```
```   681 done
```
```   682
```
```   683 (** take **)
```
```   684
```
```   685 lemma take_0 [simp]: "xs:list(A) ==> take(0, xs) =  Nil"
```
```   686 apply (unfold take_def)
```
```   687 apply (erule list.induct, auto)
```
```   688 done
```
```   689
```
```   690 lemma take_succ_Cons [simp]:
```
```   691     "n \<in> nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))"
```
```   692 by (simp add: take_def)
```
```   693
```
```   694 (* Needed for proving take_all *)
```
```   695 lemma take_Nil [simp]: "n \<in> nat ==> take(n, Nil) = Nil"
```
```   696 by (unfold take_def, auto)
```
```   697
```
```   698 lemma take_all [rule_format,simp]:
```
```   699      "n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n  \<longrightarrow> take(n, xs) = xs"
```
```   700 apply (erule nat_induct)
```
```   701 apply (auto elim: list.cases)
```
```   702 done
```
```   703
```
```   704 lemma take_type [rule_format,simp,TC]:
```
```   705      "xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
```
```   706 apply (erule list.induct, simp, clarify)
```
```   707 apply (erule natE, auto)
```
```   708 done
```
```   709
```
```   710 lemma take_append [rule_format,simp]:
```
```   711  "xs:list(A) ==>
```
```   712   \<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) =
```
```   713                             take(n, xs) @ take(n #- length(xs), ys)"
```
```   714 apply (erule list.induct, simp, clarify)
```
```   715 apply (erule natE, auto)
```
```   716 done
```
```   717
```
```   718 lemma take_take [rule_format]:
```
```   719    "m \<in> nat ==>
```
```   720     \<forall>xs \<in> list(A). \<forall>n \<in> nat. take(n, take(m,xs))= take(min(n, m), xs)"
```
```   721 apply (induct_tac "m", auto)
```
```   722 apply (erule_tac a = xs in list.cases)
```
```   723 apply (auto simp add: take_Nil)
```
```   724 apply (erule_tac n=n in natE)
```
```   725 apply (auto intro: take_0 take_type)
```
```   726 done
```
```   727
```
```   728 (** nth **)
```
```   729
```
```   730 lemma nth_0 [simp]: "nth(0, Cons(a, l)) = a"
```
```   731 by (simp add: nth_def)
```
```   732
```
```   733 lemma nth_Cons [simp]: "n \<in> nat ==> nth(succ(n), Cons(a,l)) = nth(n,l)"
```
```   734 by (simp add: nth_def)
```
```   735
```
```   736 lemma nth_empty [simp]: "nth(n, Nil) = 0"
```
```   737 by (simp add: nth_def)
```
```   738
```
```   739 lemma nth_type [rule_format,simp,TC]:
```
```   740      "xs:list(A) ==> \<forall>n. n < length(xs) \<longrightarrow> nth(n,xs) \<in> A"
```
```   741 apply (erule list.induct, simp, clarify)
```
```   742 apply (subgoal_tac "n \<in> nat")
```
```   743  apply (erule natE, auto dest!: le_in_nat)
```
```   744 done
```
```   745
```
```   746 lemma nth_eq_0 [rule_format]:
```
```   747      "xs:list(A) ==> \<forall>n \<in> nat. length(xs) \<le> n \<longrightarrow> nth(n,xs) = 0"
```
```   748 apply (erule list.induct, simp, clarify)
```
```   749 apply (erule natE, auto)
```
```   750 done
```
```   751
```
```   752 lemma nth_append [rule_format]:
```
```   753   "xs:list(A) ==>
```
```   754    \<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs)
```
```   755                                 else nth(n #- length(xs), ys))"
```
```   756 apply (induct_tac "xs", simp, clarify)
```
```   757 apply (erule natE, auto)
```
```   758 done
```
```   759
```
```   760 lemma set_of_list_conv_nth:
```
```   761     "xs:list(A)
```
```   762      ==> set_of_list(xs) = {x \<in> A. \<exists>i\<in>nat. i<length(xs) & x = nth(i,xs)}"
```
```   763 apply (induct_tac "xs", simp_all)
```
```   764 apply (rule equalityI, auto)
```
```   765 apply (rule_tac x = 0 in bexI, auto)
```
```   766 apply (erule natE, auto)
```
```   767 done
```
```   768
```
```   769 (* Other theorems about lists *)
```
```   770
```
```   771 lemma nth_take_lemma [rule_format]:
```
```   772  "k \<in> nat ==>
```
```   773   \<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k \<le> length(xs) \<longrightarrow> k \<le> length(ys) \<longrightarrow>
```
```   774       (\<forall>i \<in> nat. i<k \<longrightarrow> nth(i,xs) = nth(i,ys))\<longrightarrow> take(k,xs) = take(k,ys))"
```
```   775 apply (induct_tac "k")
```
```   776 apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib)
```
```   777 apply clarify
```
```   778 (*Both lists are non-empty*)
```
```   779 apply (erule_tac a=xs in list.cases, simp)
```
```   780 apply (erule_tac a=ys in list.cases, clarify)
```
```   781 apply (simp (no_asm_use) )
```
```   782 apply clarify
```
```   783 apply (simp (no_asm_simp))
```
```   784 apply (rule conjI, force)
```
```   785 apply (rename_tac y ys z zs)
```
```   786 apply (drule_tac x = zs and x1 = ys in bspec [THEN bspec], auto)
```
```   787 done
```
```   788
```
```   789 lemma nth_equalityI [rule_format]:
```
```   790      "[| xs:list(A); ys:list(A); length(xs) = length(ys);
```
```   791          \<forall>i \<in> nat. i < length(xs) \<longrightarrow> nth(i,xs) = nth(i,ys) |]
```
```   792       ==> xs = ys"
```
```   793 apply (subgoal_tac "length (xs) \<le> length (ys) ")
```
```   794 apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma)
```
```   795 apply (simp_all add: take_all)
```
```   796 done
```
```   797
```
```   798 (*The famous take-lemma*)
```
```   799
```
```   800 lemma take_equalityI [rule_format]:
```
```   801     "[| xs:list(A); ys:list(A); (\<forall>i \<in> nat. take(i, xs) = take(i,ys)) |]
```
```   802      ==> xs = ys"
```
```   803 apply (case_tac "length (xs) \<le> length (ys) ")
```
```   804 apply (drule_tac x = "length (ys) " in bspec)
```
```   805 apply (drule_tac [3] not_lt_imp_le)
```
```   806 apply (subgoal_tac [5] "length (ys) \<le> length (xs) ")
```
```   807 apply (rule_tac [6] j = "succ (length (ys))" in le_trans)
```
```   808 apply (rule_tac [6] leI)
```
```   809 apply (drule_tac [5] x = "length (xs) " in bspec)
```
```   810 apply (simp_all add: take_all)
```
```   811 done
```
```   812
```
```   813 lemma nth_drop [rule_format]:
```
```   814   "n \<in> nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)"
```
```   815 apply (induct_tac "n", simp_all, clarify)
```
```   816 apply (erule list.cases, auto)
```
```   817 done
```
```   818
```
```   819 lemma take_succ [rule_format]:
```
```   820   "xs\<in>list(A)
```
```   821    ==> \<forall>i. i < length(xs) \<longrightarrow> take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]"
```
```   822 apply (induct_tac "xs", auto)
```
```   823 apply (subgoal_tac "i\<in>nat")
```
```   824 apply (erule natE)
```
```   825 apply (auto simp add: le_in_nat)
```
```   826 done
```
```   827
```
```   828 lemma take_add [rule_format]:
```
```   829      "[|xs\<in>list(A); j\<in>nat|]
```
```   830       ==> \<forall>i\<in>nat. take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))"
```
```   831 apply (induct_tac "xs", simp_all, clarify)
```
```   832 apply (erule_tac n = i in natE, simp_all)
```
```   833 done
```
```   834
```
```   835 lemma length_take:
```
```   836      "l\<in>list(A) ==> \<forall>n\<in>nat. length(take(n,l)) = min(n, length(l))"
```
```   837 apply (induct_tac "l", safe, simp_all)
```
```   838 apply (erule natE, simp_all)
```
```   839 done
```
```   840
```
```   841 subsection{*The function zip*}
```
```   842
```
```   843 text{*Crafty definition to eliminate a type argument*}
```
```   844
```
```   845 consts
```
```   846   zip_aux        :: "[i,i]=>i"
```
```   847
```
```   848 primrec (*explicit lambda is required because both arguments of "un" vary*)
```
```   849   "zip_aux(B,[]) =
```
```   850      (\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))"
```
```   851
```
```   852   "zip_aux(B,Cons(x,l)) =
```
```   853      (\<lambda>ys \<in> list(B).
```
```   854         list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))"
```
```   855
```
```   856 definition
```
```   857   zip :: "[i, i]=>i"  where
```
```   858    "zip(xs, ys) == zip_aux(set_of_list(ys),xs)`ys"
```
```   859
```
```   860
```
```   861 (* zip equations *)
```
```   862
```
```   863 lemma list_on_set_of_list: "xs \<in> list(A) ==> xs \<in> list(set_of_list(xs))"
```
```   864 apply (induct_tac xs, simp_all)
```
```   865 apply (blast intro: list_mono [THEN subsetD])
```
```   866 done
```
```   867
```
```   868 lemma zip_Nil [simp]: "ys:list(A) ==> zip(Nil, ys)=Nil"
```
```   869 apply (simp add: zip_def list_on_set_of_list [of _ A])
```
```   870 apply (erule list.cases, simp_all)
```
```   871 done
```
```   872
```
```   873 lemma zip_Nil2 [simp]: "xs:list(A) ==> zip(xs, Nil)=Nil"
```
```   874 apply (simp add: zip_def list_on_set_of_list [of _ A])
```
```   875 apply (erule list.cases, simp_all)
```
```   876 done
```
```   877
```
```   878 lemma zip_aux_unique [rule_format]:
```
```   879      "[|B<=C;  xs \<in> list(A)|]
```
```   880       ==> \<forall>ys \<in> list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys"
```
```   881 apply (induct_tac xs)
```
```   882  apply simp_all
```
```   883  apply (blast intro: list_mono [THEN subsetD], clarify)
```
```   884 apply (erule_tac a=ys in list.cases, auto)
```
```   885 apply (blast intro: list_mono [THEN subsetD])
```
```   886 done
```
```   887
```
```   888 lemma zip_Cons_Cons [simp]:
```
```   889      "[| xs:list(A); ys:list(B); x \<in> A; y \<in> B |] ==>
```
```   890       zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))"
```
```   891 apply (simp add: zip_def, auto)
```
```   892 apply (rule zip_aux_unique, auto)
```
```   893 apply (simp add: list_on_set_of_list [of _ B])
```
```   894 apply (blast intro: list_on_set_of_list list_mono [THEN subsetD])
```
```   895 done
```
```   896
```
```   897 lemma zip_type [rule_format,simp,TC]:
```
```   898      "xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)"
```
```   899 apply (induct_tac "xs")
```
```   900 apply (simp (no_asm))
```
```   901 apply clarify
```
```   902 apply (erule_tac a = ys in list.cases, auto)
```
```   903 done
```
```   904
```
```   905 (* zip length *)
```
```   906 lemma length_zip [rule_format,simp]:
```
```   907      "xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
```
```   908                                      min(length(xs), length(ys))"
```
```   909 apply (unfold min_def)
```
```   910 apply (induct_tac "xs", simp_all, clarify)
```
```   911 apply (erule_tac a = ys in list.cases, auto)
```
```   912 done
```
```   913
```
```   914 lemma zip_append1 [rule_format]:
```
```   915  "[| ys:list(A); zs:list(B) |] ==>
```
```   916   \<forall>xs \<in> list(A). zip(xs @ ys, zs) =
```
```   917                  zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))"
```
```   918 apply (induct_tac "zs", force, clarify)
```
```   919 apply (erule_tac a = xs in list.cases, simp_all)
```
```   920 done
```
```   921
```
```   922 lemma zip_append2 [rule_format]:
```
```   923  "[| xs:list(A); zs:list(B) |] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) =
```
```   924        zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)"
```
```   925 apply (induct_tac "xs", force, clarify)
```
```   926 apply (erule_tac a = ys in list.cases, auto)
```
```   927 done
```
```   928
```
```   929 lemma zip_append [simp]:
```
```   930  "[| length(xs) = length(us); length(ys) = length(vs);
```
```   931      xs:list(A); us:list(B); ys:list(A); vs:list(B) |]
```
```   932   ==> zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)"
```
```   933 by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0)
```
```   934
```
```   935
```
```   936 lemma zip_rev [rule_format,simp]:
```
```   937  "ys:list(B) ==> \<forall>xs \<in> list(A).
```
```   938     length(xs) = length(ys) \<longrightarrow> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
```
```   939 apply (induct_tac "ys", force, clarify)
```
```   940 apply (erule_tac a = xs in list.cases)
```
```   941 apply (auto simp add: length_rev)
```
```   942 done
```
```   943
```
```   944 lemma nth_zip [rule_format,simp]:
```
```   945    "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
```
```   946                     i < length(xs) \<longrightarrow> i < length(ys) \<longrightarrow>
```
```   947                     nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
```
```   948 apply (induct_tac "ys", force, clarify)
```
```   949 apply (erule_tac a = xs in list.cases, simp)
```
```   950 apply (auto elim: natE)
```
```   951 done
```
```   952
```
```   953 lemma set_of_list_zip [rule_format]:
```
```   954      "[| xs:list(A); ys:list(B); i \<in> nat |]
```
```   955       ==> set_of_list(zip(xs, ys)) =
```
```   956           {<x, y>:A*B. \<exists>i\<in>nat. i < min(length(xs), length(ys))
```
```   957           & x = nth(i, xs) & y = nth(i, ys)}"
```
```   958 by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth)
```
```   959
```
```   960 (** list_update **)
```
```   961
```
```   962 lemma list_update_Nil [simp]: "i \<in> nat ==>list_update(Nil, i, v) = Nil"
```
```   963 by (unfold list_update_def, auto)
```
```   964
```
```   965 lemma list_update_Cons_0 [simp]: "list_update(Cons(x, xs), 0, v)= Cons(v, xs)"
```
```   966 by (unfold list_update_def, auto)
```
```   967
```
```   968 lemma list_update_Cons_succ [simp]:
```
```   969   "n \<in> nat ==>
```
```   970     list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))"
```
```   971 apply (unfold list_update_def, auto)
```
```   972 done
```
```   973
```
```   974 lemma list_update_type [rule_format,simp,TC]:
```
```   975      "[| xs:list(A); v \<in> A |] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)"
```
```   976 apply (induct_tac "xs")
```
```   977 apply (simp (no_asm))
```
```   978 apply clarify
```
```   979 apply (erule natE, auto)
```
```   980 done
```
```   981
```
```   982 lemma length_list_update [rule_format,simp]:
```
```   983      "xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)"
```
```   984 apply (induct_tac "xs")
```
```   985 apply (simp (no_asm))
```
```   986 apply clarify
```
```   987 apply (erule natE, auto)
```
```   988 done
```
```   989
```
```   990 lemma nth_list_update [rule_format]:
```
```   991      "[| xs:list(A) |] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs)  \<longrightarrow>
```
```   992          nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))"
```
```   993 apply (induct_tac "xs")
```
```   994  apply simp_all
```
```   995 apply clarify
```
```   996 apply (rename_tac i j)
```
```   997 apply (erule_tac n=i in natE)
```
```   998 apply (erule_tac [2] n=j in natE)
```
```   999 apply (erule_tac n=j in natE, simp_all, force)
```
```  1000 done
```
```  1001
```
```  1002 lemma nth_list_update_eq [simp]:
```
```  1003      "[| i < length(xs); xs:list(A) |] ==> nth(i, list_update(xs, i,x)) = x"
```
```  1004 by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update)
```
```  1005
```
```  1006
```
```  1007 lemma nth_list_update_neq [rule_format,simp]:
```
```  1008   "xs:list(A) ==>
```
```  1009      \<forall>i \<in> nat. \<forall>j \<in> nat. i \<noteq> j \<longrightarrow> nth(j, list_update(xs,i,x)) = nth(j,xs)"
```
```  1010 apply (induct_tac "xs")
```
```  1011  apply (simp (no_asm))
```
```  1012 apply clarify
```
```  1013 apply (erule natE)
```
```  1014 apply (erule_tac [2] natE, simp_all)
```
```  1015 apply (erule natE, simp_all)
```
```  1016 done
```
```  1017
```
```  1018 lemma list_update_overwrite [rule_format,simp]:
```
```  1019      "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs)
```
```  1020    \<longrightarrow> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)"
```
```  1021 apply (induct_tac "xs")
```
```  1022  apply (simp (no_asm))
```
```  1023 apply clarify
```
```  1024 apply (erule natE, auto)
```
```  1025 done
```
```  1026
```
```  1027 lemma list_update_same_conv [rule_format]:
```
```  1028      "xs:list(A) ==>
```
```  1029       \<forall>i \<in> nat. i < length(xs) \<longrightarrow>
```
```  1030                  (list_update(xs, i, x) = xs) \<longleftrightarrow> (nth(i, xs) = x)"
```
```  1031 apply (induct_tac "xs")
```
```  1032  apply (simp (no_asm))
```
```  1033 apply clarify
```
```  1034 apply (erule natE, auto)
```
```  1035 done
```
```  1036
```
```  1037 lemma update_zip [rule_format]:
```
```  1038      "ys:list(B) ==>
```
```  1039       \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A).
```
```  1040         length(xs) = length(ys) \<longrightarrow>
```
```  1041         list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)),
```
```  1042                                               list_update(ys, i, snd(xy)))"
```
```  1043 apply (induct_tac "ys")
```
```  1044  apply auto
```
```  1045 apply (erule_tac a = xs in list.cases)
```
```  1046 apply (auto elim: natE)
```
```  1047 done
```
```  1048
```
```  1049 lemma set_update_subset_cons [rule_format]:
```
```  1050   "xs:list(A) ==>
```
```  1051    \<forall>i \<in> nat. set_of_list(list_update(xs, i, x)) \<subseteq> cons(x, set_of_list(xs))"
```
```  1052 apply (induct_tac "xs")
```
```  1053  apply simp
```
```  1054 apply (rule ballI)
```
```  1055 apply (erule natE, simp_all, auto)
```
```  1056 done
```
```  1057
```
```  1058 lemma set_of_list_update_subsetI:
```
```  1059      "[| set_of_list(xs) \<subseteq> A; xs:list(A); x \<in> A; i \<in> nat|]
```
```  1060    ==> set_of_list(list_update(xs, i,x)) \<subseteq> A"
```
```  1061 apply (rule subset_trans)
```
```  1062 apply (rule set_update_subset_cons, auto)
```
```  1063 done
```
```  1064
```
```  1065 (** upt **)
```
```  1066
```
```  1067 lemma upt_rec:
```
```  1068      "j \<in> nat ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)"
```
```  1069 apply (induct_tac "j", auto)
```
```  1070 apply (drule not_lt_imp_le)
```
```  1071 apply (auto simp: lt_Ord intro: le_anti_sym)
```
```  1072 done
```
```  1073
```
```  1074 lemma upt_conv_Nil [simp]: "[| j \<le> i; j \<in> nat |] ==> upt(i,j) = Nil"
```
```  1075 apply (subst upt_rec, auto)
```
```  1076 apply (auto simp add: le_iff)
```
```  1077 apply (drule lt_asym [THEN notE], auto)
```
```  1078 done
```
```  1079
```
```  1080 (*Only needed if upt_Suc is deleted from the simpset*)
```
```  1081 lemma upt_succ_append:
```
```  1082      "[| i \<le> j; j \<in> nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]"
```
```  1083 by simp
```
```  1084
```
```  1085 lemma upt_conv_Cons:
```
```  1086      "[| i<j; j \<in> nat |]  ==> upt(i,j) = Cons(i,upt(succ(i),j))"
```
```  1087 apply (rule trans)
```
```  1088 apply (rule upt_rec, auto)
```
```  1089 done
```
```  1090
```
```  1091 lemma upt_type [simp,TC]: "j \<in> nat ==> upt(i,j):list(nat)"
```
```  1092 by (induct_tac "j", auto)
```
```  1093
```
```  1094 (*LOOPS as a simprule, since j<=j*)
```
```  1095 lemma upt_add_eq_append:
```
```  1096      "[| i \<le> j; j \<in> nat; k \<in> nat |] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)"
```
```  1097 apply (induct_tac "k")
```
```  1098 apply (auto simp add: app_assoc app_type)
```
```  1099 apply (rule_tac j = j in le_trans, auto)
```
```  1100 done
```
```  1101
```
```  1102 lemma length_upt [simp]: "[| i \<in> nat; j \<in> nat |] ==>length(upt(i,j)) = j #- i"
```
```  1103 apply (induct_tac "j")
```
```  1104 apply (rule_tac [2] sym)
```
```  1105 apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff)
```
```  1106 done
```
```  1107
```
```  1108 lemma nth_upt [rule_format,simp]:
```
```  1109      "[| i \<in> nat; j \<in> nat; k \<in> nat |] ==> i #+ k < j \<longrightarrow> nth(k, upt(i,j)) = i #+ k"
```
```  1110 apply (induct_tac "j", simp)
```
```  1111 apply (simp add: nth_append le_iff)
```
```  1112 apply (auto dest!: not_lt_imp_le
```
```  1113             simp add: nth_append less_diff_conv add_commute)
```
```  1114 done
```
```  1115
```
```  1116 lemma take_upt [rule_format,simp]:
```
```  1117      "[| m \<in> nat; n \<in> nat |] ==>
```
```  1118          \<forall>i \<in> nat. i #+ m \<le> n \<longrightarrow> take(m, upt(i,n)) = upt(i,i#+m)"
```
```  1119 apply (induct_tac "m")
```
```  1120 apply (simp (no_asm_simp) add: take_0)
```
```  1121 apply clarify
```
```  1122 apply (subst upt_rec, simp)
```
```  1123 apply (rule sym)
```
```  1124 apply (subst upt_rec, simp)
```
```  1125 apply (simp_all del: upt.simps)
```
```  1126 apply (rule_tac j = "succ (i #+ x) " in lt_trans2)
```
```  1127 apply auto
```
```  1128 done
```
```  1129
```
```  1130 lemma map_succ_upt:
```
```  1131      "[| m \<in> nat; n \<in> nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))"
```
```  1132 apply (induct_tac "n")
```
```  1133 apply (auto simp add: map_app_distrib)
```
```  1134 done
```
```  1135
```
```  1136 lemma nth_map [rule_format,simp]:
```
```  1137      "xs:list(A) ==>
```
```  1138       \<forall>n \<in> nat. n < length(xs) \<longrightarrow> nth(n, map(f, xs)) = f(nth(n, xs))"
```
```  1139 apply (induct_tac "xs", simp)
```
```  1140 apply (rule ballI)
```
```  1141 apply (induct_tac "n", auto)
```
```  1142 done
```
```  1143
```
```  1144 lemma nth_map_upt [rule_format]:
```
```  1145      "[| m \<in> nat; n \<in> nat |] ==>
```
```  1146       \<forall>i \<in> nat. i < n #- m \<longrightarrow> nth(i, map(f, upt(m,n))) = f(m #+ i)"
```
```  1147 apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp)
```
```  1148 apply (subst map_succ_upt [symmetric], simp_all, clarify)
```
```  1149 apply (subgoal_tac "i < length (upt (0, x))")
```
```  1150  prefer 2
```
```  1151  apply (simp add: less_diff_conv)
```
```  1152  apply (rule_tac j = "succ (i #+ y) " in lt_trans2)
```
```  1153   apply simp
```
```  1154  apply simp
```
```  1155 apply (subgoal_tac "i < length (upt (y, x))")
```
```  1156  apply (simp_all add: add_commute less_diff_conv)
```
```  1157 done
```
```  1158
```
```  1159 (** sublist (a generalization of nth to sets) **)
```
```  1160
```
```  1161 definition
```
```  1162   sublist :: "[i, i] => i"  where
```
```  1163     "sublist(xs, A)==
```
```  1164      map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))"
```
```  1165
```
```  1166 lemma sublist_0 [simp]: "xs:list(A) ==>sublist(xs, 0) =Nil"
```
```  1167 by (unfold sublist_def, auto)
```
```  1168
```
```  1169 lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil"
```
```  1170 by (unfold sublist_def, auto)
```
```  1171
```
```  1172 lemma sublist_shift_lemma:
```
```  1173  "[| xs:list(B); i \<in> nat |] ==>
```
```  1174   map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) =
```
```  1175   map(fst, filter(%p. snd(p):nat & snd(p) #+ i \<in> A, zip(xs,upt(0,length(xs)))))"
```
```  1176 apply (erule list_append_induct)
```
```  1177 apply (simp (no_asm_simp))
```
```  1178 apply (auto simp add: add_commute length_app filter_append map_app_distrib)
```
```  1179 done
```
```  1180
```
```  1181 lemma sublist_type [simp,TC]:
```
```  1182      "xs:list(B) ==> sublist(xs, A):list(B)"
```
```  1183 apply (unfold sublist_def)
```
```  1184 apply (induct_tac "xs")
```
```  1185 apply (auto simp add: filter_append map_app_distrib)
```
```  1186 done
```
```  1187
```
```  1188 lemma upt_add_eq_append2:
```
```  1189      "[| i \<in> nat; j \<in> nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)"
```
```  1190 by (simp add: upt_add_eq_append [of 0] nat_0_le)
```
```  1191
```
```  1192 lemma sublist_append:
```
```  1193  "[| xs:list(B); ys:list(B)  |] ==>
```
```  1194   sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j \<in> nat. j #+ length(xs): A})"
```
```  1195 apply (unfold sublist_def)
```
```  1196 apply (erule_tac l = ys in list_append_induct, simp)
```
```  1197 apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric])
```
```  1198 apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc)
```
```  1199 apply (simp_all add: add_commute)
```
```  1200 done
```
```  1201
```
```  1202
```
```  1203 lemma sublist_Cons:
```
```  1204      "[| xs:list(B); x \<in> B |] ==>
```
```  1205       sublist(Cons(x, xs), A) =
```
```  1206       (if 0 \<in> A then [x] else []) @ sublist(xs, {j \<in> nat. succ(j) \<in> A})"
```
```  1207 apply (erule_tac l = xs in list_append_induct)
```
```  1208 apply (simp (no_asm_simp) add: sublist_def)
```
```  1209 apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp)
```
```  1210 done
```
```  1211
```
```  1212 lemma sublist_singleton [simp]:
```
```  1213      "sublist([x], A) = (if 0 \<in> A then [x] else [])"
```
```  1214 by (simp add: sublist_Cons)
```
```  1215
```
```  1216 lemma sublist_upt_eq_take [rule_format, simp]:
```
```  1217     "xs:list(A) ==> \<forall>n\<in>nat. sublist(xs,n) = take(n,xs)"
```
```  1218 apply (erule list.induct, simp)
```
```  1219 apply (clarify )
```
```  1220 apply (erule natE)
```
```  1221 apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
```
```  1222 done
```
```  1223
```
```  1224 lemma sublist_Int_eq:
```
```  1225      "xs \<in> list(B) ==> sublist(xs, A \<inter> nat) = sublist(xs, A)"
```
```  1226 apply (erule list.induct)
```
```  1227 apply (simp_all add: sublist_Cons)
```
```  1228 done
```
```  1229
```
```  1230 text{*Repetition of a List Element*}
```
```  1231
```
```  1232 consts   repeat :: "[i,i]=>i"
```
```  1233 primrec
```
```  1234   "repeat(a,0) = []"
```
```  1235
```
```  1236   "repeat(a,succ(n)) = Cons(a,repeat(a,n))"
```
```  1237
```
```  1238 lemma length_repeat: "n \<in> nat ==> length(repeat(a,n)) = n"
```
```  1239 by (induct_tac n, auto)
```
```  1240
```
```  1241 lemma repeat_succ_app: "n \<in> nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]"
```
```  1242 apply (induct_tac n)
```
```  1243 apply (simp_all del: app_Cons add: app_Cons [symmetric])
```
```  1244 done
```
```  1245
```
```  1246 lemma repeat_type [TC]: "[|a \<in> A; n \<in> nat|] ==> repeat(a,n) \<in> list(A)"
```
```  1247 by (induct_tac n, auto)
```
```  1248
```
```  1249 end
```