src/ZF/List.ML
author paulson
Fri, 11 Aug 2000 13:26:40 +0200
changeset 9577 9e66e8ed8237
parent 9548 15bee2731e43
child 9907 473a6604da94
permissions -rw-r--r--
ZF arith
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*)
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6112
diff changeset
    12
val 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*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    15
val Cons_iff     = list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    16
val 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))";
525
e62519a8497d ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents: 516
diff changeset
    19
let open list;  val rew = rewrite_rule con_defs in  
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    20
by (blast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
525
e62519a8497d ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents: 516
diff changeset
    21
end;
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    22
qed "list_unfold";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    23
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
(**  Lemmas to justify using "list" in other recursive type definitions **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
    26
Goalw list.defs "A<=B ==> list(A) <= list(B)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
by (rtac lfp_mono 1);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    28
by (REPEAT (rtac list.bnd_mono 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    30
qed "list_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
(*There is a similar proof by list induction.*)
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
    33
Goalw (list.defs@list.con_defs) "list(univ(A)) <= univ(A)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
by (rtac lfp_lowerbound 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
by (rtac (A_subset_univ RS univ_mono) 2);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    36
by (blast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
    37
				Pair_in_univ]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    38
qed "list_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
908
1f99a44c10cb Updated comment about list_subset_univ and list_into_univ.
lcp
parents: 782
diff changeset
    40
(*These two theorems justify datatypes involving list(nat), list(A), ...*)
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
    41
bind_thm ("list_subset_univ", [list_mono, list_univ] MRS subset_trans);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
    43
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
    44
by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    45
qed "list_into_univ";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    46
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    47
val major::prems = Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
    "[| l: list(A);    \
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    49
\       c: C(Nil);       \
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    50
\       !!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
    51
\    |] ==> list_case(c,h,l) : C(l)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    52
by (rtac (major RS list.induct) 1);
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
    53
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    54
qed "list_case_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    57
(*** List functions ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    58
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
    59
Goal "l: list(A) ==> tl(l) : list(A)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
    60
by (exhaust_tac "l" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    61
by (ALLGOALS (asm_simp_tac (simpset() addsimps list.intrs)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    62
qed "tl_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    63
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    64
(** drop **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    65
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    66
Goal "i:nat ==> drop(i, Nil) = Nil";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    67
by (induct_tac "i" 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    68
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    69
qed "drop_Nil";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    70
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    71
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
    72
by (rtac sym 1);
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    73
by (induct_tac "i" 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    74
by (Simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    75
by (Asm_simp_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    76
qed "drop_succ_Cons";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    77
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    78
Addsimps [drop_Nil, drop_succ_Cons];
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    79
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    80
Goal "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    81
by (induct_tac "i" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    82
by (ALLGOALS (asm_simp_tac (simpset() addsimps [tl_type])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    83
qed "drop_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    84
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    85
Delsimps [drop_SUCC];
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6065
diff changeset
    86
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    87
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
    88
(** Type checking -- proved by induction, as usual **)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    89
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
    90
val prems = Goal
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    91
    "[| l: list(A);    \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    92
\       c: C(Nil);       \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    93
\       !!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
    94
\    |] ==> list_rec(c,h,l) : C(l)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
    95
by (cut_facts_tac prems 1);
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
    96
by (induct_tac "l" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    97
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    98
qed "list_rec_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    99
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   100
(** map **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   101
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
   102
val prems = Goalw [get_def thy "map_list"] 
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   103
    "[| 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
   104
by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   105
qed "map_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   106
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   107
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
   108
by (etac map_type 1);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   109
by (etac RepFunI 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   110
qed "map_type2";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   111
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   112
(** length **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   113
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
   114
Goalw [get_def thy "length_list"] 
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   115
    "l: list(A) ==> length(l) : nat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   116
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
   117
qed "length_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   118
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   119
(** app **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   120
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
   121
Goalw [get_def thy "op @_list"] 
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   122
    "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   123
by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   124
qed "app_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   125
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   126
(** rev **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   127
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
   128
Goalw [get_def thy "rev_list"] 
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   129
    "xs: list(A) ==> rev(xs) : list(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   130
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
   131
qed "rev_type";
516
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
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   134
(** flat **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   135
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
   136
Goalw [get_def thy "flat_list"] 
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   137
    "ls: list(list(A)) ==> flat(ls) : list(A)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   138
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
   139
qed "flat_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   140
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   141
1926
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   142
(** set_of_list **)
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   143
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
   144
Goalw [get_def thy "set_of_list_list"] 
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   145
    "l: list(A) ==> set_of_list(l) : Pow(A)";
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1926
diff changeset
   146
by (etac list_rec_type 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   147
by (ALLGOALS (Blast_tac));
1926
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   148
qed "set_of_list_type";
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   149
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   150
Goal "xs: list(A) ==> \
1926
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   151
\         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
   152
by (etac list.induct 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   153
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons])));
1926
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   154
qed "set_of_list_append";
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   155
1957ae3f9301 Addition of function set_of_list
paulson
parents: 1663
diff changeset
   156
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   157
(** list_add **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   158
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
   159
Goalw [get_def thy "list_add_list"] 
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   160
    "xs: list(nat) ==> list_add(xs) : nat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   161
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
   162
qed "list_add_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   163
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   164
val list_typechecks =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   165
    list.intrs @
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   166
    [list_rec_type, map_type, map_type2, app_type, length_type, 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   167
     rev_type, flat_type, list_add_type];
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   168
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6141
diff changeset
   169
AddTCs list_typechecks;
516
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
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   172
(*** theorems about map ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   173
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   174
Goal "l: list(A) ==> map(%u. u, l) = l";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   175
by (induct_tac "l" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   176
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   177
qed "map_ident";
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   178
Addsimps [map_ident];
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   179
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   180
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
   181
by (induct_tac "l" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   182
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   183
qed "map_compose";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   184
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   185
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
   186
by (induct_tac "xs" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   187
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   188
qed "map_app_distrib";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   189
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   190
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
   191
by (induct_tac "ls" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   192
by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   193
qed "map_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   194
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   195
Goal "l: list(A) ==> \
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
   196
\    list_rec(c, d, map(h,l)) = \
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 5529
diff changeset
   197
\    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
   198
by (induct_tac "l" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   199
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   200
qed "list_rec_map";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   201
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   202
(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   203
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   204
(* c : list(Collect(B,P)) ==> c : list(B) *)
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   205
bind_thm ("list_CollectD", Collect_subset RS list_mono RS subsetD);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   206
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   207
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
   208
by (induct_tac "l" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   209
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   210
qed "map_list_Collect";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   211
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   212
(*** theorems about length ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   213
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   214
Goal "xs: list(A) ==> length(map(h,xs)) = length(xs)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   215
by (induct_tac "xs" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   216
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   217
qed "length_map";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   218
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6153
diff changeset
   219
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
   220
\     ==> length(xs@ys) = length(xs) #+ length(ys)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   221
by (induct_tac "xs" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   222
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   223
qed "length_app";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   224
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   225
Goal "xs: list(A) ==> length(rev(xs)) = length(xs)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   226
by (induct_tac "xs" 1);
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   227
by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   228
qed "length_rev";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   229
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   230
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
   231
by (induct_tac "ls" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   232
by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   233
qed "length_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   234
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   235
(** Length and drop **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   236
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   237
(*Lemma for the inductive step of drop_length*)
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   238
Goal "xs: list(A) ==> \
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   239
\          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
   240
by (etac list.induct 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   241
by (ALLGOALS Asm_simp_tac);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   242
by (Blast_tac 1);
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   243
qed_spec_mp "drop_length_Cons";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   244
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   245
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
   246
by (etac list.induct 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   247
by (ALLGOALS Asm_simp_tac);
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   248
by Safe_tac;
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   249
by (etac drop_length_Cons 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   250
by (rtac natE 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   251
by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   252
by (assume_tac 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   253
by (ALLGOALS Asm_simp_tac);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   254
by (ALLGOALS (blast_tac (claset() addIs [succ_in_naturalD, length_type])));
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   255
qed_spec_mp "drop_length";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   256
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   257
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   258
(*** theorems about app ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   259
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   260
Goal "xs: list(A) ==> xs@Nil=xs";
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   261
by (etac list.induct 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   262
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   263
qed "app_right_Nil";
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   264
Addsimps [app_right_Nil];
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   265
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   266
Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   267
by (induct_tac "xs" 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   268
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   269
qed "app_assoc";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   270
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   271
Goal "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   272
by (induct_tac "ls" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   273
by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   274
qed "flat_app_distrib";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   275
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   276
(*** theorems about rev ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   277
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   278
Goal "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   279
by (induct_tac "l" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   280
by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   281
qed "rev_map_distrib";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   282
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   283
(*Simplifier needs the premises as assumptions because rewriting will not
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   284
  instantiate the variable ?A in the rules' typing conditions; note that
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   285
  rev_type does not instantiate ?A.  Only the premises do.
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   286
*)
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   287
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
   288
by (etac list.induct 1);
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   289
by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   290
qed "rev_app_distrib";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   291
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   292
Goal "l: list(A) ==> rev(rev(l))=l";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   293
by (induct_tac "l" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   294
by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   295
qed "rev_rev_ident";
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   296
Addsimps [rev_rev_ident];
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   297
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   298
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
   299
by (induct_tac "ls" 1);
6112
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   300
by (ALLGOALS
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   301
    (asm_simp_tac (simpset() addsimps 
5e4871c5136b datatype package improvements
paulson
parents: 6070
diff changeset
   302
		   [map_app_distrib, flat_app_distrib, rev_app_distrib])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   303
qed "rev_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   304
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   305
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   306
(*** theorems about list_add ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   307
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   308
Goal "[| xs: list(nat);  ys: list(nat) |] ==> \
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   309
\    list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   310
by (induct_tac "xs" 1);
9548
15bee2731e43 instantiated Cancel_Numerals for "nat" in ZF
paulson
parents: 9491
diff changeset
   311
by (ALLGOALS Asm_simp_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   312
qed "list_add_app";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   313
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   314
Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6053
diff changeset
   315
by (induct_tac "l" 1);
9548
15bee2731e43 instantiated Cancel_Numerals for "nat" in ZF
paulson
parents: 9491
diff changeset
   316
by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   317
qed "list_add_rev";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   318
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   319
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
   320
by (induct_tac "ls" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   321
by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   322
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
   323
qed "list_add_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   324
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   325
(** New induction rule **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   326
5321
f8848433d240 got rid of some goal thy commands
paulson
parents: 5147
diff changeset
   327
val major::prems = Goal
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   328
    "[| l: list(A);  \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   329
\       P(Nil);        \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   330
\       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x]) \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   331
\    |] ==> P(l)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   332
by (rtac (major RS rev_rev_ident RS subst) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   333
by (rtac (major RS rev_type RS list.induct) 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   334
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   335
qed "list_append_induct";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   336