src/ZF/List.ML
author paulson
Wed, 15 May 2002 10:42:32 +0200
changeset 13149 773657d466cb
parent 13143 adb0c97883cf
child 13160 eca781285662
permissions -rw-r--r--
better simplification of trivial existential equalities
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 908
diff changeset
     1
(*  Title:      ZF/List.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 908
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Datatype definition of Lists
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
     9
(*** Aspects of the datatype definition ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
(*An elimination rule, for type-checking*)
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9548
diff changeset
    12
bind_thm ("ConsE", list.mk_cases "Cons(a,l) : list(A)");
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
(*Proving freeness results*)
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9548
diff changeset
    15
bind_thm ("Cons_iff", list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'");
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9548
diff changeset
    16
bind_thm ("Nil_Cons_iff", list.mk_free "~ Nil=Cons(a,l)");
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
    18
Goal "list(A) = {0} + (A * list(A))";
12789
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
    19
by (blast_tac (claset() addSIs (map (rewrite_rule list.con_defs) list.intrs) 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
    20
                        addEs [rewrite_rule list.con_defs list.elim]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    21
qed "list_unfold";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    22
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
(**  Lemmas to justify using "list" in other recursive type definitions **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
    25
Goalw list.defs "A<=B ==> list(A) <= list(B)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
by (rtac lfp_mono 1);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    27
by (REPEAT (rtac list.bnd_mono 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    29
qed "list_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
(*There is a similar proof by list induction.*)
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
    32
Goalw (list.defs@list.con_defs) "list(univ(A)) <= univ(A)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
by (rtac lfp_lowerbound 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
by (rtac (A_subset_univ RS univ_mono) 2);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    35
by (blast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
    36
				Pair_in_univ]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    37
qed "list_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
908
1f99a44c10cb Updated comment about list_subset_univ and list_into_univ.
lcp
parents: 782
diff changeset
    39
(*These two theorems justify datatypes involving list(nat), list(A), ...*)
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
    40
bind_thm ("list_subset_univ", [list_mono, list_univ] MRS subset_trans);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
    42
Goal "[| l: list(A);  A <= univ(B) |] ==> l: univ(B)";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    43
by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    44
qed "list_into_univ";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    45
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    46
val major::prems = Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
    "[| l: list(A);    \
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    48
\       c: C(Nil);       \
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    49
\       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))  \
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    50
\    |] ==> list_case(c,h,l) : C(l)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    51
by (rtac (major RS list.induct) 1);
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
    52
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    53
qed "list_case_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    56
(*** List functions ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    57
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
    58
Goal "l: list(A) ==> tl(l) : list(A)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
    59
by (exhaust_tac "l" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    60
by (ALLGOALS (asm_simp_tac (simpset() addsimps list.intrs)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    61
qed "tl_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    62
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    63
(** drop **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    64
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    65
Goal "i:nat ==> drop(i, Nil) = Nil";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    66
by (induct_tac "i" 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    67
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    68
qed "drop_Nil";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    69
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    70
Goal "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
2493
bdeb5024353a Removal of sum_cs and eq_cs
paulson
parents: 2469
diff changeset
    71
by (rtac sym 1);
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    72
by (induct_tac "i" 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    73
by (Simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    74
by (Asm_simp_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    75
qed "drop_succ_Cons";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    76
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    77
Addsimps [drop_Nil, drop_succ_Cons];
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    78
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    79
Goal "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    80
by (induct_tac "i" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    81
by (ALLGOALS (asm_simp_tac (simpset() addsimps [tl_type])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    82
qed "drop_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    83
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    84
Delsimps [drop_SUCC];
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    85
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    86
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
    87
(** Type checking -- proved by induction, as usual **)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    88
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    89
val prems = Goal
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    90
    "[| l: list(A);    \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    91
\       c: C(Nil);       \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    92
\       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
    93
\    |] ==> list_rec(c,h,l) : C(l)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
    94
by (cut_facts_tac prems 1);
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
    95
by (induct_tac "l" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    96
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    97
qed "list_rec_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    98
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    99
(** map **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   100
11145
3e47692e3a3e eliminate get_def;
wenzelm
parents: 9907
diff changeset
   101
val prems = Goalw [thm "map_list_def"]
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   102
    "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   103
by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   104
qed "map_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   105
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   106
Goal "l: list(A) ==> map(h,l) : list({h(u). u:A})";
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   107
by (etac map_type 1);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   108
by (etac RepFunI 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   109
qed "map_type2";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   110
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   111
(** length **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   112
11145
3e47692e3a3e eliminate get_def;
wenzelm
parents: 9907
diff changeset
   113
Goalw [thm "length_list_def"]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   114
    "l: list(A) ==> length(l) : nat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   115
by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   116
qed "length_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   117
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   118
(** app **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   119
11145
3e47692e3a3e eliminate get_def;
wenzelm
parents: 9907
diff changeset
   120
Goalw [thm "op @_list_def"]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   121
    "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   122
by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   123
qed "app_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   124
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   125
(** rev **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   126
11145
3e47692e3a3e eliminate get_def;
wenzelm
parents: 9907
diff changeset
   127
Goalw [thm "rev_list_def"]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   128
    "xs: list(A) ==> rev(xs) : list(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   129
by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   130
qed "rev_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   131
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   132
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   133
(** flat **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   134
11145
3e47692e3a3e eliminate get_def;
wenzelm
parents: 9907
diff changeset
   135
Goalw [thm "flat_list_def"]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   136
    "ls: list(list(A)) ==> flat(ls) : list(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   137
by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   138
qed "flat_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   139
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   140
1926
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   141
(** set_of_list **)
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   142
11145
3e47692e3a3e eliminate get_def;
wenzelm
parents: 9907
diff changeset
   143
Goalw [thm "set_of_list_list_def"]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   144
    "l: list(A) ==> set_of_list(l) : Pow(A)";
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1926
diff changeset
   145
by (etac list_rec_type 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   146
by (ALLGOALS (Blast_tac));
1926
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   147
qed "set_of_list_type";
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   148
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   149
Goal "xs: list(A) ==> \
1926
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   150
\         set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)";
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   151
by (etac list.induct 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   152
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons])));
1926
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   153
qed "set_of_list_append";
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   154
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   155
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   156
(** list_add **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   157
11145
3e47692e3a3e eliminate get_def;
wenzelm
parents: 9907
diff changeset
   158
Goalw [thm "list_add_list_def"] 
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   159
    "xs: list(nat) ==> list_add(xs) : nat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   160
by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   161
qed "list_add_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   162
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9548
diff changeset
   163
bind_thms ("list_typechecks",
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   164
    list.intrs @
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   165
    [list_rec_type, map_type, map_type2, app_type, length_type, 
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9548
diff changeset
   166
     rev_type, flat_type, list_add_type]);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   167
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6141
diff changeset
   168
AddTCs list_typechecks;
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   169
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   170
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   171
(*** theorems about map ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   172
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   173
Goal "l: list(A) ==> map(%u. u, l) = l";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   174
by (induct_tac "l" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   175
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   176
qed "map_ident";
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   177
Addsimps [map_ident];
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   178
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   179
Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   180
by (induct_tac "l" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   181
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   182
qed "map_compose";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   183
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   184
Goal "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   185
by (induct_tac "xs" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   186
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   187
qed "map_app_distrib";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   188
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   189
Goal "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   190
by (induct_tac "ls" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   191
by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   192
qed "map_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   193
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   194
Goal "l: list(A) ==> \
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
   195
\    list_rec(c, d, map(h,l)) = \
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
   196
\    list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   197
by (induct_tac "l" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   198
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   199
qed "list_rec_map";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   200
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   201
(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   202
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   203
(* c : list(Collect(B,P)) ==> c : list(B) *)
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   204
bind_thm ("list_CollectD", Collect_subset RS list_mono RS subsetD);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   205
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   206
Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   207
by (induct_tac "l" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   208
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   209
qed "map_list_Collect";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   210
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   211
(*** theorems about length ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   212
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   213
Goal "xs: list(A) ==> length(map(h,xs)) = length(xs)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   214
by (induct_tac "xs" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   215
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   216
qed "length_map";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   217
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6153
diff changeset
   218
Goal "[| xs: list(A); ys: list(A) |] \
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6153
diff changeset
   219
\     ==> length(xs@ys) = length(xs) #+ length(ys)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   220
by (induct_tac "xs" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   221
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   222
qed "length_app";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   223
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   224
Goal "xs: list(A) ==> length(rev(xs)) = length(xs)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   225
by (induct_tac "xs" 1);
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   226
by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   227
qed "length_rev";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   228
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   229
Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   230
by (induct_tac "ls" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   231
by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   232
qed "length_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   233
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   234
(** Length and drop **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   235
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   236
(*Lemma for the inductive step of drop_length*)
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   237
Goal "xs: list(A) ==> \
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   238
\          ALL x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   239
by (etac list.induct 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   240
by (ALLGOALS Asm_simp_tac);
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   241
qed_spec_mp "drop_length_Cons";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   242
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   243
Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   244
by (etac list.induct 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   245
by (ALLGOALS Asm_simp_tac);
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   246
by Safe_tac;
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   247
by (etac drop_length_Cons 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   248
by (rtac natE 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   249
by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   250
by (assume_tac 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   251
by (ALLGOALS Asm_simp_tac);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   252
by (ALLGOALS (blast_tac (claset() addIs [succ_in_naturalD, length_type])));
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   253
qed_spec_mp "drop_length";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   254
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   255
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   256
(*** theorems about app ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   257
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   258
Goal "xs: list(A) ==> xs@Nil=xs";
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   259
by (etac list.induct 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   260
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   261
qed "app_right_Nil";
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   262
Addsimps [app_right_Nil];
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   263
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   264
Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   265
by (induct_tac "xs" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   266
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   267
qed "app_assoc";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   268
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   269
Goal "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   270
by (induct_tac "ls" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   271
by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   272
qed "flat_app_distrib";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   273
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   274
(*** theorems about rev ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   275
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   276
Goal "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   277
by (induct_tac "l" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   278
by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   279
qed "rev_map_distrib";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   280
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   281
(*Simplifier needs the premises as assumptions because rewriting will not
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   282
  instantiate the variable ?A in the rules' typing conditions; note that
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   283
  rev_type does not instantiate ?A.  Only the premises do.
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   284
*)
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   285
Goal "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   286
by (etac list.induct 1);
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   287
by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   288
qed "rev_app_distrib";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   289
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   290
Goal "l: list(A) ==> rev(rev(l))=l";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   291
by (induct_tac "l" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   292
by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   293
qed "rev_rev_ident";
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   294
Addsimps [rev_rev_ident];
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   295
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   296
Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   297
by (induct_tac "ls" 1);
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   298
by (ALLGOALS
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   299
    (asm_simp_tac (simpset() addsimps 
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   300
		   [map_app_distrib, flat_app_distrib, rev_app_distrib])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   301
qed "rev_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   302
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   303
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   304
(*** theorems about list_add ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   305
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   306
Goal "[| xs: list(nat);  ys: list(nat) |] ==> \
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   307
\    list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   308
by (induct_tac "xs" 1);
9548
15bee2731e43 instantiated Cancel_Numerals for "nat" in ZF
paulson
parents: 9491
diff changeset
   309
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   310
qed "list_add_app";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   311
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   312
Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   313
by (induct_tac "l" 1);
9548
15bee2731e43 instantiated Cancel_Numerals for "nat" in ZF
paulson
parents: 9491
diff changeset
   314
by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   315
qed "list_add_rev";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   316
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   317
Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   318
by (induct_tac "ls" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   319
by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   320
by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   321
qed "list_add_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   322
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   323
(** New induction rule **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   324
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   325
val major::prems = Goal
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   326
    "[| l: list(A);  \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   327
\       P(Nil);        \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   328
\       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x]) \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   329
\    |] ==> P(l)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   330
by (rtac (major RS rev_rev_ident RS subst) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   331
by (rtac (major RS rev_type RS list.induct) 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   332
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   333
qed "list_append_induct";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   334
12789
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   335
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   336
(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   337
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   338
(** min **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   339
(* Min theorems are also true for i, j ordinals *)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   340
Goalw [min_def] "[| i:nat; j:nat |] ==> min(i,j)=min(j,i)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   341
by (auto_tac (claset() addSDs [not_lt_imp_le] 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   342
                       addDs [lt_not_sym] 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   343
                       addIs [le_anti_sym], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   344
qed "min_sym";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   345
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   346
Goalw [min_def] "[| i:nat; j:nat |] ==> min(i,j):nat";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   347
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   348
qed "min_type";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   349
AddTCs [min_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   350
Addsimps [min_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   351
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   352
Goalw [min_def]  "i:nat ==> min(0,i) = 0";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   353
by (auto_tac (claset() addDs [not_lt_imp_le], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   354
qed "min_0";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   355
Addsimps [min_0];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   356
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   357
Goalw [min_def] "i:nat ==> min(i, 0) = 0";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   358
by (auto_tac (claset() addDs [not_lt_imp_le], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   359
qed "min_02";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   360
Addsimps [min_02];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   361
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   362
Goalw [min_def] "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) <-> i<j & i<k";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   363
by (auto_tac (claset() addSDs [not_lt_imp_le]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   364
                       addIs [lt_trans2, lt_trans], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   365
qed "lt_min_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   366
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   367
Goalw [min_def]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   368
     "[| i:nat; j:nat |] ==>  min(succ(i), succ(j))= succ(min(i, j))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   369
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   370
qed "min_succ_succ";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   371
Addsimps [min_succ_succ];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   372
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   373
(*** more theorems about lists ***)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   374
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   375
Goal "xs:list(A) ==> (xs~=Nil)<->(EX y:A. EX ys:list(A). xs=Cons(y,ys))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   376
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   377
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   378
qed "neq_Nil_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   379
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   380
(** filter **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   381
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   382
Goal "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   383
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   384
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   385
qed "filter_append";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   386
Addsimps [filter_append];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   387
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   388
Goal "xs:list(A) ==> filter(P, xs):list(A)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   389
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   390
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   391
qed "filter_type";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   392
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   393
Goal "xs:list(A) ==> length(filter(P, xs)) le length(xs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   394
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   395
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   396
by (res_inst_tac [("j", "length(l)")] le_trans 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   397
by (auto_tac (claset(), simpset() addsimps [le_iff]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   398
qed "length_filter";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   399
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   400
Goal "xs:list(A) ==> set_of_list(filter(P,xs)) <= set_of_list(xs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   401
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   402
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   403
qed "filter_is_subset";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   404
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   405
Goal "xs:list(A) ==> filter(%p. False, xs) = Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   406
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   407
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   408
qed "filter_False";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   409
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   410
Goal "xs:list(A) ==> filter(%p. True, xs) = xs";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   411
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   412
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   413
qed "filter_True";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   414
Addsimps [filter_False, filter_True];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   415
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   416
(** length **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   417
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   418
Goal "xs:list(A) ==> length(xs)=0 <-> xs=Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   419
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   420
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   421
qed "length_is_0_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   422
Addsimps [length_is_0_iff];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   423
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   424
Goal "xs:list(A) ==> 0 = length(xs) <-> xs=Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   425
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   426
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   427
qed "length_is_0_iff2";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   428
Addsimps [length_is_0_iff2];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   429
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   430
Goal "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   431
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   432
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   433
qed "length_tl";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   434
Addsimps [length_tl];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   435
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   436
Goal "xs:list(A) ==> 0<length(xs) <-> xs ~= Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   437
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   438
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   439
qed "length_greater_0_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   440
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   441
Goal "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   442
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   443
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   444
qed "length_succ_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   445
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   446
(** more theorems about append **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   447
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   448
Goal "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   449
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   450
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   451
qed "append_is_Nil_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   452
Addsimps [append_is_Nil_iff];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   453
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   454
Goal "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   455
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   456
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   457
qed "append_is_Nil_iff2";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   458
Addsimps [append_is_Nil_iff2];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   459
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   460
Goal "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   461
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   462
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   463
qed "append_left_is_self_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   464
Addsimps [append_left_is_self_iff];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   465
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   466
Goal "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   467
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   468
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   469
qed "append_left_is_self_iff2";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   470
Addsimps [append_left_is_self_iff2];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   471
13143
adb0c97883cf Deleting two simprules saves 21 seconds!
paulson
parents: 12825
diff changeset
   472
(*TOO SLOW as a default simprule!*)
12789
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   473
Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   474
\  length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   475
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   476
by (auto_tac (claset(), simpset() addsimps [length_app]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   477
qed_spec_mp "append_left_is_Nil_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   478
13143
adb0c97883cf Deleting two simprules saves 21 seconds!
paulson
parents: 12825
diff changeset
   479
(*TOO SLOW as a default simprule!*)
12789
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   480
Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   481
\  length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   482
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   483
by (auto_tac (claset(), simpset() addsimps [length_app]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   484
qed_spec_mp "append_left_is_Nil_iff2";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   485
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   486
Goal "xs:list(A) ==> ALL ys:list(A). \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   487
\     length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   488
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   489
by (Asm_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   490
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   491
by (eres_inst_tac [("a", "ys")] list.elim 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   492
by (ALLGOALS(Asm_full_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   493
qed_spec_mp "append_eq_append_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   494
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   495
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   496
Goal "xs:list(A) ==>  \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   497
\  ALL ys:list(A). ALL us:list(A). ALL vs:list(A). \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   498
\  length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   499
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   500
by (ALLGOALS(Clarify_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   501
by (asm_full_simp_tac (simpset() addsimps [length_app]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   502
by (eres_inst_tac [("a", "ys")] list.elim 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   503
by (Asm_full_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   504
by (subgoal_tac "Cons(a, l) @ us =vs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   505
by (dtac (rotate_prems 4 (append_left_is_Nil_iff RS iffD1)) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   506
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   507
qed_spec_mp "append_eq_append";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   508
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   509
Goal "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |] \ 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   510
\ ==>  xs@us = ys@vs <-> (xs=ys & us=vs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   511
by (rtac iffI 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   512
by (rtac append_eq_append 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   513
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   514
qed "append_eq_append_iff2";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   515
Addsimps [append_eq_append_iff, append_eq_append_iff2];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   516
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   517
Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   518
by (Asm_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   519
qed "append_self_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   520
Addsimps [append_self_iff];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   521
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   522
Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   523
by (Asm_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   524
qed "append_self_iff2";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   525
Addsimps [append_self_iff2];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   526
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   527
(* Can also be proved from append_eq_append_iff2,
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   528
but the proof requires two more hypotheses: x:A and y:A *)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   529
Goal "xs:list(A) ==> ALL ys:list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   530
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   531
by (ALLGOALS(Clarify_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   532
by (ALLGOALS(eres_inst_tac [("a", "ys")] list.elim));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   533
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   534
qed_spec_mp "append1_eq_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   535
Addsimps [append1_eq_iff];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   536
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   537
Goal "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)";
13143
adb0c97883cf Deleting two simprules saves 21 seconds!
paulson
parents: 12825
diff changeset
   538
by (asm_simp_tac (simpset() addsimps [append_left_is_Nil_iff]) 1);
12789
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   539
qed "append_right_is_self_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   540
Addsimps [append_right_is_self_iff];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   541
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   542
Goal "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   543
by (rtac iffI 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   544
by (dtac sym 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   545
by (ALLGOALS(Asm_full_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   546
qed "append_right_is_self_iff2";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   547
Addsimps [append_right_is_self_iff2];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   548
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   549
Goal "xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   550
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   551
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   552
qed_spec_mp "hd_append";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   553
Addsimps [hd_append];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   554
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   555
Goal "xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   556
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   557
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   558
qed_spec_mp "tl_append";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   559
Addsimps [tl_append];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   560
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   561
(** rev **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   562
Goal "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   563
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   564
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   565
qed "rev_is_Nil_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   566
Addsimps [rev_is_Nil_iff];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   567
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   568
Goal "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   569
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   570
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   571
qed "Nil_is_rev_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   572
Addsimps [Nil_is_rev_iff];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   573
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   574
Goal "xs:list(A) ==> ALL ys:list(A). rev(xs)=rev(ys) <-> xs=ys";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   575
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   576
by (Force_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   577
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   578
by (eres_inst_tac [("a", "ys")] list.elim 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   579
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   580
qed_spec_mp "rev_is_rev_iff";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   581
Addsimps [rev_is_rev_iff];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   582
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   583
Goal "xs:list(A) ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   584
\ (xs=Nil --> P) --> (ALL ys:list(A). ALL y:A. xs =ys@[y] -->P)-->P";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   585
by (etac list_append_induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   586
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   587
qed_spec_mp "rev_list_elim_aux";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   588
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   589
bind_thm("rev_list_elim", impI RS ballI RS ballI RSN(3, rev_list_elim_aux));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   590
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   591
(** more theorems about drop **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   592
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   593
Goal "n:nat ==> ALL xs:list(A). length(drop(n, xs)) = length(xs) #- n";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   594
by (etac nat_induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   595
by (auto_tac (claset() addEs [list.elim], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   596
qed_spec_mp "length_drop";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   597
Addsimps [length_drop];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   598
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   599
Goal "n:nat ==> ALL xs:list(A). length(xs) le n --> drop(n, xs)=Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   600
by (etac nat_induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   601
by (auto_tac (claset() addEs [list.elim], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   602
qed_spec_mp "drop_all";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   603
Addsimps [drop_all];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   604
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   605
Goal "n:nat ==> ALL xs:list(A). drop(n, xs@ys) = \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   606
\ drop(n,xs) @ drop(n #- length(xs), ys)"; 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   607
by (induct_tac "n" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   608
by (auto_tac (claset() addEs [list.elim], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   609
qed_spec_mp "drop_append";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   610
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   611
Goal "m:nat ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   612
\ ALL xs:list(A). ALL n:nat. drop(n, drop(m, xs))=drop(n #+ m, xs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   613
by (induct_tac "m" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   614
by (auto_tac (claset() addEs [list.elim], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   615
qed "drop_drop";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   616
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   617
(** take **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   618
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   619
Goalw [take_def]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   620
 "xs:list(A) ==> take(0, xs) =  Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   621
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   622
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   623
qed "take_0";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   624
Addsimps [take_0];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   625
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   626
Goalw [take_def]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   627
"n:nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   628
by (Asm_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   629
qed "take_succ_Cons";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   630
Addsimps [take_succ_Cons];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   631
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   632
(* Needed for proving take_all *)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   633
Goalw [take_def]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   634
 "n:nat ==> take(n, Nil) = Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   635
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   636
qed "take_Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   637
Addsimps [take_Nil];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   638
 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   639
Goal "n:nat ==> ALL xs:list(A). length(xs) le n  --> take(n, xs) = xs";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   640
by (etac nat_induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   641
by (auto_tac (claset() addEs [list.elim], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   642
qed_spec_mp  "take_all";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   643
Addsimps [take_all];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   644
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   645
Goal "xs:list(A) ==> ALL n:nat. take(n, xs):list(A)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   646
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   647
by (Clarify_tac 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   648
by (etac natE 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   649
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   650
qed_spec_mp "take_type";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   651
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   652
Goal "xs:list(A) ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   653
\ ALL ys:list(A). ALL n:nat. take(n, xs @ ys) = \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   654
\                           take(n, xs) @ take(n #- length(xs), ys)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   655
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   656
by (Clarify_tac 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   657
by (etac natE 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   658
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   659
qed_spec_mp "take_append";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   660
Addsimps [take_append];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   661
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   662
Goal
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   663
"m:nat ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   664
\ ALL xs:list(A). ALL n:nat. take(n, take(m,xs))= take(min(n, m), xs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   665
by (induct_tac "m" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   666
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   667
by (eres_inst_tac [("a", "xs")] list.elim 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   668
by (auto_tac (claset(), simpset() addsimps [take_Nil]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   669
by (rotate_tac 1 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   670
by (etac natE 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   671
by (auto_tac (claset() addIs [take_0, take_type], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   672
qed_spec_mp "take_take";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   673
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   674
(** nth **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   675
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   676
Goalw [nth_def] "nth(0, Cons(a, l))= a";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   677
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   678
qed "nth_0";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   679
Addsimps [nth_0];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   680
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   681
Goalw [nth_def]  
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   682
   "n:nat ==> nth(succ(n), Cons(a, l)) = nth(n, l)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   683
by (Asm_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   684
qed "nth_Cons";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   685
Addsimps [nth_Cons];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   686
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   687
Goal "xs:list(A) ==> ALL n:nat. n < length(xs) --> nth(n, xs):A";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   688
by (etac list.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   689
by (ALLGOALS(Clarify_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   690
by (etac natE 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   691
by (ALLGOALS(Asm_full_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   692
qed_spec_mp "nth_type";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   693
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   694
AddTCs [nth_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   695
Addsimps [nth_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   696
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   697
Goal 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   698
"xs:list(A) ==> ALL n:nat. \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   699
\ nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs) \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   700
\                      else nth(n #- length(xs),ys))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   701
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   702
by (Clarify_tac 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   703
by (etac natE 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   704
by (ALLGOALS(Asm_full_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   705
qed_spec_mp "nth_append";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   706
12825
f1f7964ed05c new simprules and classical rules
paulson
parents: 12789
diff changeset
   707
Goal "xs:list(A) \
f1f7964ed05c new simprules and classical rules
paulson
parents: 12789
diff changeset
   708
\     ==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x=nth(i, xs)}";
12789
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   709
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   710
by (ALLGOALS(Asm_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   711
by (rtac equalityI 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   712
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   713
by (res_inst_tac [("x", "0")] bexI 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   714
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   715
by (etac natE 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   716
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   717
qed "set_of_list_conv_nth";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   718
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   719
(* Other theorems about lists *)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   720
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   721
Goalw [Ball_def]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   722
 "k:nat ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   723
\ ALL xs:list(A). (ALL ys:list(A). k le length(xs) --> k le length(ys) -->  \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   724
\     (ALL i:nat. i<k --> nth(i,xs)= nth(i,ys))--> take(k, xs) = take(k,ys))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   725
by (induct_tac "k" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   726
by (ALLGOALS (asm_simp_tac (simpset() addsimps 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   727
             [lt_succ_eq_0_disj, all_conj_distrib])));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   728
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   729
(*Both lists must be non-empty*)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   730
by (case_tac "xa=Nil" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   731
by (case_tac "xb=Nil" 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   732
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   733
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   734
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   735
(*prenexing's needed, not miniscoping*)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   736
by (Asm_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   737
by (rtac conjI 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   738
by (Force_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   739
by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [iff_sym])  
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   740
                                       delsimps (all_simps))));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   741
by (dres_inst_tac [("x", "ys"), ("x1", "ysa")] (spec RS spec) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   742
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   743
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   744
qed_spec_mp "nth_take_lemma";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   745
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   746
Goal "[| xs:list(A); ys:list(A); length(xs) = length(ys);  \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   747
\        ALL i:nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |]  \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   748
\     ==> xs = ys";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   749
by (subgoal_tac "length(xs) le length(ys)" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   750
by (forw_inst_tac [("ys", "ys")] (rotate_prems 1 nth_take_lemma) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   751
by (ALLGOALS(Asm_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   752
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [take_all])));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   753
qed_spec_mp "nth_equalityI";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   754
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   755
(*The famous take-lemma*)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   756
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   757
Goal "[| xs:list(A); ys:list(A); (ALL i:nat. take(i, xs) = take(i,ys)) |] ==> xs = ys";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   758
by (case_tac "length(xs) le length(ys)" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   759
by (dres_inst_tac [("x", "length(ys)")] bspec 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   760
by (dtac not_lt_imp_le 3);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   761
by (subgoal_tac "length(ys) le length(xs)" 5);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   762
by (res_inst_tac [("j", "succ(length(ys))")] le_trans 6);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   763
by (rtac leI 6);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   764
by (dres_inst_tac [("x", "length(xs)")] bspec 5);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   765
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [take_all])));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   766
qed_spec_mp "take_equalityI";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   767
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   768
Goal "n:nat ==> ALL i:nat. ALL xs:list(A). n #+ i le length(xs) \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   769
\               --> nth(i, drop(n, xs)) = nth(n #+ i, xs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   770
by (induct_tac "n" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   771
by (ALLGOALS(Asm_full_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   772
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   773
by (case_tac "xb=Nil" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   774
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   775
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   776
by (auto_tac (claset() addSEs [ConsE], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   777
qed_spec_mp "nth_drop";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   778
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   779
(** zip **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   780
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   781
Goal "l:list(A) ==> l:list(set_of_list(l))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   782
by (induct_tac "l" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   783
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   784
by (res_inst_tac [("A1", "set_of_list(l)")] (list_mono RS subsetD) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   785
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   786
qed "list_on_set_of_list";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   787
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   788
Goal "A<=C ==> ziprel(A, B) <= ziprel(C,B)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   789
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   790
by (forward_tac [ziprel.dom_subset RS subsetD] 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   791
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   792
by (etac ziprel.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   793
by (auto_tac (claset() addIs [list_mono RS subsetD]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   794
                       addSIs ziprel.intrs, simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   795
qed "ziprel_mono1";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   796
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   797
Goal "B<=C ==> ziprel(A, B) <= ziprel(A,C)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   798
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   799
by (forward_tac [ziprel.dom_subset RS subsetD] 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   800
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   801
by (etac ziprel.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   802
by (auto_tac (claset() addIs [list_mono RS subsetD]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   803
                       addSIs ziprel.intrs, simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   804
qed "ziprel_mono2";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   805
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   806
Goal "[| A<=C; B<=D |] ==> ziprel(A, B) <= ziprel(C,D)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   807
by (rtac subset_trans 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   808
by (rtac ziprel_mono1 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   809
by (rtac ziprel_mono2 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   810
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   811
qed "ziprel_mono";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   812
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   813
(* ziprel is a function *)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   814
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   815
Goal "<xs, ys, zs>:ziprel(A,B) \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   816
\     ==> ALL ks. <xs, ys, ks>:ziprel(A, B) --> ks=zs";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   817
by (etac ziprel.induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   818
by (ALLGOALS(Clarify_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   819
by (rotate_tac 1 3);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   820
by (ALLGOALS(etac ziprel.elim));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   821
by Safe_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   822
(* These hypotheses make Auto_tac loop! *)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   823
by (thin_tac "ALL k. ?P(k)" 3);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   824
by (thin_tac "ALL k. ?P(k)" 4);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   825
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   826
qed "ziprel_is_fun";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   827
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   828
Goal "ys:list(B)  ==> ALL xs:list(A). EX zs. <xs, ys, zs>:ziprel(A,B)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   829
by (induct_tac "ys" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   830
by (auto_tac (claset() addIs ziprel.intrs, simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   831
by (eres_inst_tac [("a", "xs")] list.elim 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   832
by (auto_tac (claset() addIs ziprel.intrs, simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   833
qed_spec_mp "ziprel_exist"; 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   834
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   835
Goalw [zip_def]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   836
 "[|xs:list(A); ys:list(B) |] ==> <xs, ys, zip(xs,ys)>:ziprel(A,B)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   837
by (rtac theI2 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   838
by (asm_full_simp_tac (simpset() addsimps [set_of_list_append]) 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   839
by (REPEAT(dtac set_of_list_type 2));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   840
by (rtac (ziprel_mono RS subsetD) 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   841
by (Blast_tac 3);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   842
by (dtac list_on_set_of_list 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   843
by (dtac list_on_set_of_list 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   844
by (subgoal_tac "xs:list(set_of_list(xs@ys)) & \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   845
\                ys:list(set_of_list(xs@ys))" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   846
by (auto_tac (claset() addIs [list_mono RS subsetD],
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   847
              simpset() addsimps [set_of_list_append]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   848
by (rtac (ziprel_is_fun RS spec RS mp) 2); 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   849
by (rtac ziprel_exist 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   850
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   851
qed "zip_in_ziprel";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   852
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   853
Goal
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   854
"<xs, ys, zs>:ziprel(A,B) ==> zip(xs, ys)=zs";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   855
by (rtac (ziprel_is_fun RS spec RS mp) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   856
by (Blast_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   857
by (blast_tac (claset() addDs [ziprel.dom_subset RS subsetD]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   858
                        addIs [zip_in_ziprel]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   859
qed "zip_eq";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   860
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   861
(* zip equations *)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   862
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   863
Goal "ys:list(A) ==> zip(Nil, ys)=Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   864
by (res_inst_tac [("A", "A")] zip_eq 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   865
by (auto_tac (claset() addIs ziprel.intrs, simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   866
qed "zip_Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   867
Addsimps [zip_Nil];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   868
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   869
Goal "xs:list(A) ==> zip(xs, Nil)=Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   870
by (res_inst_tac [("A", "A")] zip_eq 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   871
by (auto_tac (claset() addIs ziprel.intrs, simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   872
qed "zip_Nil2";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   873
Addsimps [zip_Nil2];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   874
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   875
Goal "[| xs:list(A); ys:list(B); x:A; y:B |] ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   876
\ zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   877
by (res_inst_tac [("A", "A")] zip_eq 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   878
by (forw_inst_tac [("ys", "ys")] zip_in_ziprel 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   879
by (auto_tac (claset() addIs ziprel.intrs, simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   880
qed "zip_Cons_Cons";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   881
Addsimps [zip_Cons_Cons];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   882
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   883
Goal "xs:list(A) ==> ALL ys:list(B). zip(xs, ys):list(A*B)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   884
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   885
by (Simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   886
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   887
by (eres_inst_tac [("a", "ys")] list.elim 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   888
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   889
qed_spec_mp "zip_type";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   890
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   891
AddTCs [zip_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   892
Addsimps [zip_type];    
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   893
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   894
(* zip length *)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   895
Goalw [min_def] "xs:list(A) ==> ALL ys:list(B). length(zip(xs,ys)) = \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   896
\                               min(length(xs), length(ys))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   897
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   898
by (Clarify_tac 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   899
by (eres_inst_tac [("a", "ys")] list.elim 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   900
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   901
qed_spec_mp "length_zip";  
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   902
Addsimps [length_zip];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   903
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   904
AddTCs [take_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   905
Addsimps [take_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   906
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   907
Goal "[| ys:list(A); zs:list(B) |] ==> ALL xs:list(A). zip(xs @ ys, zs) = \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   908
\ zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   909
by (induct_tac "zs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   910
by (Clarify_tac 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   911
by (eres_inst_tac [("a", "xs")] list.elim 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   912
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   913
qed_spec_mp "zip_append1";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   914
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   915
Goal
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   916
 "[| xs:list(A); zs:list(B) |] ==> ALL ys:list(B). zip(xs, ys@zs) = \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   917
\      zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   918
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   919
by (Clarify_tac 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   920
by (eres_inst_tac [("a", "ys")] list.elim 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   921
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   922
qed_spec_mp "zip_append2";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   923
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   924
Goal
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   925
 "[| length(xs) = length(us); length(ys) = length(vs); \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   926
\  xs:list(A); us:list(B); ys:list(A); vs:list(B) |] ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   927
\ zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   928
by (asm_simp_tac (simpset() addsimps 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   929
                  [zip_append1, drop_append, diff_self_eq_0]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   930
qed_spec_mp "zip_append";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   931
Addsimps [zip_append];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   932
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   933
Goal "ys:list(B) ==> ALL xs:list(A).  \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   934
\ length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   935
by (induct_tac "ys" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   936
by (Clarify_tac 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   937
by (eres_inst_tac [("a", "xs")] list.elim 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   938
by (auto_tac (claset(), simpset() addsimps [length_rev]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   939
qed_spec_mp "zip_rev";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   940
Addsimps [zip_rev];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   941
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   942
Goal
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   943
"ys:list(B) ==> ALL i:nat. ALL xs:list(A). \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   944
\                   i < length(xs) --> i < length(ys) --> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   945
\                   nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   946
by (induct_tac "ys" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   947
by (Clarify_tac 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   948
by (eres_inst_tac [("a", "xs")] list.elim 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   949
by (auto_tac (claset() addEs [natE], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   950
qed_spec_mp "nth_zip";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   951
Addsimps [nth_zip];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   952
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   953
Goal "[| xs:list(A); ys:list(B); i:nat |] \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   954
\     ==> set_of_list(zip(xs, ys)) = \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   955
\         {<x, y>:A*B. EX i:nat. i < min(length(xs), length(ys))  \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   956
\         & x=nth(i, xs) & y=nth(i, ys)}";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   957
by (force_tac (claset() addSIs [Collect_cong], 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   958
               simpset() addsimps [lt_min_iff, set_of_list_conv_nth]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   959
qed_spec_mp "set_of_list_zip";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   960
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   961
(** list_update **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   962
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   963
Goalw [list_update_def] "i:nat ==>list_update(Nil, i, v) = Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   964
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   965
qed "list_update_Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   966
Addsimps [list_update_Nil];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   967
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   968
Goalw [list_update_def] 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   969
"list_update(Cons(x, xs), 0, v)= Cons(v, xs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   970
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   971
qed "list_update_Cons_0";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   972
Addsimps [list_update_Cons_0];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   973
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   974
Goalw [list_update_def] 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   975
"n:nat ==>\
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   976
\ list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   977
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   978
qed "list_update_Cons_succ";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   979
Addsimps [list_update_Cons_succ];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   980
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   981
Goal "[| xs:list(A); v:A |] ==> ALL n:nat. list_update(xs, n, v):list(A)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   982
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   983
by (Simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   984
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   985
by (etac natE 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   986
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   987
qed_spec_mp "list_update_type";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   988
Addsimps [list_update_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   989
AddTCs [list_update_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   990
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   991
Goal "xs:list(A) ==> ALL i:nat. length(list_update(xs, i, v))=length(xs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   992
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   993
by (Simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   994
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   995
by (etac natE 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   996
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   997
qed_spec_mp "length_list_update";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   998
Addsimps [length_list_update];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
   999
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1000
Goal "[| xs:list(A) |] ==> ALL i:nat. ALL j:nat. i < length(xs)  --> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1001
\ nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1002
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1003
 by (Simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1004
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1005
by (etac natE 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1006
by (ALLGOALS(Asm_full_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1007
by (ALLGOALS(Clarify_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1008
by (etac natE 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1009
by (ALLGOALS(Asm_full_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1010
by Safe_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1011
by (etac natE 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1012
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nth_Cons])));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1013
qed_spec_mp "nth_list_update";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1014
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1015
Goal "[| i < length(xs); xs:list(A); i:nat |] \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1016
\  ==> nth(i, list_update(xs, i,x)) = x";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1017
by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1018
qed "nth_list_update_eq";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1019
Addsimps [nth_list_update_eq];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1020
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1021
Goal "xs:list(A) ==> ALL i:nat. ALL j:nat. i ~= j \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1022
\ --> nth(j, list_update(xs, i,x)) = nth(j, xs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1023
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1024
 by (Simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1025
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1026
by (etac natE 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1027
by (etac natE 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1028
by (ALLGOALS(Asm_full_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1029
by (etac natE 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1030
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nth_Cons])));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1031
qed_spec_mp "nth_list_update_neq";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1032
Addsimps [nth_list_update_neq];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1033
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1034
Goal "xs:list(A) ==> ALL i:nat. i < length(xs)\
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1035
\  --> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1036
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1037
 by (Simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1038
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1039
by (etac natE 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1040
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1041
qed_spec_mp "list_update_overwrite";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1042
Addsimps [list_update_overwrite];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1043
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1044
Goal "xs:list(A) ==> ALL i:nat. i < length(xs) --> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1045
\ (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1046
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1047
 by (Simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1048
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1049
by (etac natE 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1050
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1051
qed_spec_mp "list_update_same_conv";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1052
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1053
Goal "ys:list(B) ==> ALL i:nat. ALL xy:A*B. ALL xs:list(A). \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1054
\ length(xs) = length(ys) --> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1055
\     list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)), \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1056
\                                         list_update(ys, i, snd(xy)))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1057
by (induct_tac "ys" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1058
 by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1059
by (eres_inst_tac [("a", "xc")] list.elim 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1060
by (auto_tac (claset() addEs [natE], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1061
qed_spec_mp "update_zip";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1062
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1063
Goal "xs:list(A) ==> ALL i:nat. set_of_list(list_update(xs, i, x)) \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1064
\  <= cons(x, set_of_list(xs))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1065
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1066
 by (asm_full_simp_tac (simpset() addsimps []) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1067
by (rtac ballI 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1068
by (etac natE 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1069
by (ALLGOALS(Asm_full_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1070
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1071
qed_spec_mp "set_update_subset_cons";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1072
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1073
Goal "[| set_of_list(xs) <= A; xs:list(A); x:A; i:nat|]  \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1074
\  ==> set_of_list(list_update(xs, i,x)) <= A";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1075
by (rtac subset_trans 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1076
by (rtac set_update_subset_cons 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1077
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1078
qed "set_of_list_update_subsetI";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1079
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1080
(** upt **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1081
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1082
Goal "[| i:nat; j:nat |] \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1083
\ ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1084
by (induct_tac "j" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1085
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1086
by (dtac not_lt_imp_le 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1087
by (auto_tac (claset() addIs [le_anti_sym], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1088
qed "upt_rec";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1089
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1090
Goal "[| j le i; i:nat; j:nat |] ==> upt(i,j) = Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1091
by (stac upt_rec 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1092
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1093
by (auto_tac (claset(), simpset() addsimps [le_iff]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1094
by (dtac (lt_asym RS notE) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1095
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1096
qed "upt_conv_Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1097
Addsimps [upt_conv_Nil];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1098
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1099
(*Only needed if upt_Suc is deleted from the simpset*)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1100
Goal "[| i le j; i:nat; j:nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1101
by (Asm_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1102
qed "upt_succ_append";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1103
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1104
Goal "[| i<j; i:nat; j:nat |]  ==> upt(i,j) = Cons(i,upt(succ(i),j))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1105
by (rtac trans 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1106
by (stac upt_rec 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1107
by (rtac refl 4);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1108
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1109
qed "upt_conv_Cons";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1110
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1111
Goal "[| i:nat; j:nat |] ==> upt(i,j):list(nat)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1112
by (induct_tac "j" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1113
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1114
qed "upt_type";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1115
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1116
AddTCs [upt_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1117
Addsimps [upt_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1118
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1119
(*LOOPS as a simprule, since j<=j*)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1120
Goal "[| i le j; i:nat; j:nat; k:nat |] ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1121
\ upt(i, j #+k) = upt(i,j)@upt(j,j#+k)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1122
by (induct_tac "k" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1123
by (auto_tac (claset(), simpset() addsimps [app_assoc, app_type]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1124
by (res_inst_tac [("j", "j")] le_trans 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1125
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1126
qed "upt_add_eq_append";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1127
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1128
Goal "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1129
by (induct_tac "j" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1130
by (rtac sym 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1131
by (auto_tac (claset() addSDs [not_lt_imp_le], 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1132
              simpset() addsimps [length_app, diff_succ, diff_is_0_iff]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1133
qed "length_upt";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1134
Addsimps [length_upt];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1135
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1136
Goal "[| i:nat; j:nat; k:nat |] ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1137
\ i #+ k < j --> nth(k, upt(i,j)) = i #+ k";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1138
by (induct_tac "j" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1139
by (Asm_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1140
by (asm_full_simp_tac (simpset() addsimps [nth_append,lt_succ_iff] 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1141
                                 addsplits [nat_diff_split]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1142
by Safe_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1143
by (auto_tac (claset() addSDs [not_lt_imp_le], 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1144
              simpset() addsimps [nth_append, diff_self_eq_0, 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1145
                                  less_diff_conv, add_commute])); 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1146
by (dres_inst_tac [("j", "x")] lt_trans2 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1147
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1148
qed_spec_mp "nth_upt";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1149
Addsimps [nth_upt];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1150
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1151
Goal "[| m:nat; n:nat |] ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1152
\ ALL i:nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1153
by (induct_tac "m" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1154
by (asm_simp_tac (simpset() addsimps [take_0]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1155
by (Clarify_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1156
by (stac upt_rec 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1157
by (rtac sym 3);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1158
by (stac upt_rec 3);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1159
by (ALLGOALS(asm_full_simp_tac (simpset() delsimps (thms"upt.simps"))));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1160
by (res_inst_tac [("j", "succ(i #+ x)")] lt_trans2 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1161
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1162
qed_spec_mp "take_upt";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1163
Addsimps [take_upt];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1164
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1165
Goal "[| m:nat; n:nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1166
by (induct_tac "n" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1167
by (auto_tac (claset(), simpset() addsimps [map_app_distrib]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1168
qed "map_succ_upt";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1169
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1170
Goal "xs:list(A) ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1171
\ ALL n:nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1172
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1173
by (Asm_full_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1174
by (rtac ballI 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1175
by (induct_tac "n" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1176
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1177
qed_spec_mp "nth_map";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1178
Addsimps [nth_map];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1179
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1180
Goal "[| m:nat; n:nat |] ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1181
\ ALL i:nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1182
by (res_inst_tac [("n", "m"), ("m", "n")] diff_induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1183
by (stac (map_succ_upt RS sym) 5);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1184
by (ALLGOALS(Asm_full_simp_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1185
by (ALLGOALS(Clarify_tac));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1186
by (subgoal_tac "xa < length(upt(0, x))" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1187
by (Asm_simp_tac 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1188
by (subgoal_tac "xa < length(upt(y, x))" 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1189
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [map_compose, 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1190
          nth_map, add_commute, less_diff_conv])));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1191
by (res_inst_tac [("j", "succ(xa #+ y)")] lt_trans2 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1192
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1193
qed_spec_mp "nth_map_upt";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1194
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1195
(** sublist (a generalization of nth to sets) **)
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1196
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1197
Goalw [sublist_def] "xs:list(A) ==>sublist(xs, 0) =Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1198
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1199
qed "sublist_0";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1200
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1201
Goalw [sublist_def] "sublist(Nil, A) = Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1202
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1203
qed "sublist_Nil";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1204
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1205
AddTCs [filter_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1206
Addsimps [filter_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1207
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1208
Goal "[| xs:list(B); i:nat |] ==>\
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1209
\    map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) = \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1210
\    map(fst, filter(%p. snd(p):nat & snd(p) #+ i:A, zip(xs,upt(0,length(xs)))))";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1211
by (etac list_append_induct  1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1212
by (Asm_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1213
by (auto_tac (claset(), simpset() addsimps 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1214
         [add_commute, length_app, filter_append, map_app_distrib]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1215
qed "sublist_shift_lemma";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1216
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1217
Goalw [sublist_def]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1218
 "xs:list(B) ==> sublist(xs, A):list(B)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1219
by (induct_tac "xs" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1220
by (auto_tac (claset(), simpset() addsimps [filter_append, map_app_distrib]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1221
by (auto_tac (claset() addIs [map_type,filter_type,zip_type], simpset()));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1222
qed "sublist_type";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1223
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1224
AddTCs [sublist_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1225
Addsimps [sublist_type];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1226
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1227
Goal "[| i:nat; j:nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1228
by (asm_simp_tac (simpset() addsimps 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1229
                [inst "i" "0" upt_add_eq_append, nat_0_le]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1230
qed "upt_add_eq_append2";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1231
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1232
Goalw [sublist_def]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1233
     "[| xs:list(B); ys:list(B)  |] ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1234
\ sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1235
by (eres_inst_tac [("l", "ys")] list_append_induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1236
by (Asm_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1237
by (asm_simp_tac (simpset() addsimps [upt_add_eq_append2, 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1238
                                      zip_append, length_app,  app_assoc RS sym]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1239
by (auto_tac (claset(), simpset() addsimps [sublist_shift_lemma, 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1240
                                           length_type, map_app_distrib, app_assoc]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1241
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [add_commute])));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1242
qed "sublist_append";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1243
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1244
Addsimps [sublist_0, sublist_Nil];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1245
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1246
Goal "[| xs:list(B); x:B |] ==> \
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1247
\ sublist(Cons(x, xs), A) = (if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1248
by (eres_inst_tac [("l", "xs")] list_append_induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1249
by (asm_simp_tac (simpset() addsimps [sublist_def]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1250
by (asm_simp_tac (simpset() delsimps (thms "op @.simps") 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1251
                 addsimps [(hd (tl (thms "op @.simps"))) RS sym, sublist_append]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1252
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1253
qed "sublist_Cons";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1254
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1255
Goal "sublist([x], A) = (if 0 : A then [x] else [])";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1256
by (simp_tac (simpset() addsimps [sublist_Cons]) 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1257
qed "sublist_singleton";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1258
Addsimps [sublist_singleton];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1259
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1260
Goalw [less_than_def]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1261
    "[| xs:list(A); n:nat |] ==> sublist(xs, less_than(n)) = take(n,xs)";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1262
by (eres_inst_tac [("l", "xs")] list_append_induct 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1263
 by (asm_simp_tac (simpset() addsplits [nat_diff_split]
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1264
                             addsimps [sublist_append]) 2);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1265
by Auto_tac;
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1266
by (subgoal_tac "n #- length(y) = 0" 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1267
by (Asm_simp_tac 1);
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1268
by (auto_tac (claset() addSDs [not_lt_imp_le], 
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1269
          simpset() addsimps [diff_is_0_iff]));
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1270
qed "sublist_upt_eq_take";
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1271
Addsimps [sublist_upt_eq_take];
459b5de466b2 new definitions from Sidi Ehmety
paulson
parents: 11145
diff changeset
  1272