src/ZF/List.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 1663 7e84d8712a0b
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
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
open List;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    11
(*** Aspects of the datatype definition ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
(*An elimination rule, for type-checking*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    14
val ConsE = list.mk_cases list.con_defs "Cons(a,l) : list(A)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
(*Proving freeness results*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    17
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
    18
val Nil_Cons_iff = list.mk_free "~ Nil=Cons(a,l)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
(*Perform induction on l, then prove the major premise using prems. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
fun list_ind_tac a prems i = 
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    22
    EVERY [res_inst_tac [("x",a)] list.induct i,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 908
diff changeset
    23
           rename_last_tac a ["1"] (i+2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 908
diff changeset
    24
           ares_tac prems i];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    26
goal List.thy "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
    27
let open list;  val rew = rewrite_rule con_defs in  
e62519a8497d ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents: 516
diff changeset
    28
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
e62519a8497d ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents: 516
diff changeset
    29
                     addEs [rew elim]) 1)
e62519a8497d ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents: 516
diff changeset
    30
end;
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    31
qed "list_unfold";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    32
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
(**  Lemmas to justify using "list" in other recursive type definitions **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    35
goalw List.thy list.defs "!!A B. A<=B ==> list(A) <= list(B)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
by (rtac lfp_mono 1);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    37
by (REPEAT (rtac list.bnd_mono 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    39
qed "list_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
(*There is a similar proof by list induction.*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    42
goalw List.thy (list.defs@list.con_defs) "list(univ(A)) <= univ(A)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
by (rtac lfp_lowerbound 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
by (rtac (A_subset_univ RS univ_mono) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 908
diff changeset
    46
                            Pair_in_univ]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    47
qed "list_univ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
908
1f99a44c10cb Updated comment about list_subset_univ and list_into_univ.
lcp
parents: 782
diff changeset
    49
(*These two theorems justify datatypes involving list(nat), list(A), ...*)
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
    50
bind_thm ("list_subset_univ", ([list_mono, list_univ] MRS subset_trans));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    52
goal List.thy "!!l A B. [| l: list(A);  A <= univ(B) |] ==> l: univ(B)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    53
by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    54
qed "list_into_univ";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 279
diff changeset
    55
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
val major::prems = goal List.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
    "[| l: list(A);    \
15
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    58
\       c: C(Nil);       \
6c6d2f6e3185 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    59
\       !!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
    60
\    |] ==> list_case(c,h,l) : C(l)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    61
by (rtac (major RS list.induct) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    62
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (list.case_eqns @ prems))));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    63
qed "list_case_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
(** For recursion **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    68
goalw List.thy list.con_defs "rank(a) < rank(Cons(a,l))";
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    69
by (simp_tac rank_ss 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    70
qed "rank_Cons1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    72
goalw List.thy list.con_defs "rank(l) < rank(Cons(a,l))";
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    73
by (simp_tac rank_ss 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    74
qed "rank_Cons2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    76
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    77
(*** List functions ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    78
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    79
(** hd and tl **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    80
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    81
goalw List.thy [hd_def] "hd(Cons(a,l)) = a";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    82
by (resolve_tac list.case_eqns 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    83
qed "hd_Cons";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    84
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    85
goalw List.thy [tl_def] "tl(Nil) = Nil";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    86
by (resolve_tac list.case_eqns 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    87
qed "tl_Nil";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    88
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    89
goalw List.thy [tl_def] "tl(Cons(a,l)) = l";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    90
by (resolve_tac list.case_eqns 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    91
qed "tl_Cons";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    92
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    93
goal List.thy "!!l. l: list(A) ==> tl(l) : list(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    94
by (etac list.elim 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    95
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (list.intrs @ [tl_Nil,tl_Cons]))));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
    96
qed "tl_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    97
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
    98
(** drop **)
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
goalw List.thy [drop_def] "drop(0, l) = l";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   101
by (rtac rec_0 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   102
qed "drop_0";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   103
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   104
goalw List.thy [drop_def] "!!i. i:nat ==> drop(i, Nil) = Nil";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   105
by (etac nat_induct 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   106
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Nil])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   107
qed "drop_Nil";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   108
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   109
goalw List.thy [drop_def]
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   110
    "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   111
by (etac nat_induct 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   112
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Cons])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   113
qed "drop_succ_Cons";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   114
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   115
goalw List.thy [drop_def] 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   116
    "!!i l. [| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   117
by (etac nat_induct 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   118
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_type])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   119
qed "drop_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   120
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   121
(** list_rec -- by Vset recursion **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   122
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   123
goal List.thy "list_rec(Nil,c,h) = c";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   124
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   125
by (simp_tac (ZF_ss addsimps list.case_eqns) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   126
qed "list_rec_Nil";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   127
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   128
goal List.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   129
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   130
by (simp_tac (rank_ss addsimps (rank_Cons2::list.case_eqns)) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   131
qed "list_rec_Cons";
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
(*Type checking -- proved by induction, as usual*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   134
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   135
    "[| l: list(A);    \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   136
\       c: C(Nil);       \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   137
\       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   138
\    |] ==> list_rec(l,c,h) : C(l)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   139
by (list_ind_tac "l" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   140
by (ALLGOALS (asm_simp_tac
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 908
diff changeset
   141
              (ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons]))));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   142
qed "list_rec_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   143
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   144
(** Versions for use with definitions **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   145
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   146
val [rew] = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   147
    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   148
by (rewtac rew);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   149
by (rtac list_rec_Nil 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   150
qed "def_list_rec_Nil";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   151
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   152
val [rew] = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   153
    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   154
by (rewtac rew);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   155
by (rtac list_rec_Cons 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   156
qed "def_list_rec_Cons";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   157
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   158
fun list_recs def = map standard
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 908
diff changeset
   159
        ([def] RL [def_list_rec_Nil, def_list_rec_Cons]);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   160
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   161
(** map **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   162
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   163
val [map_Nil,map_Cons] = list_recs map_def;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   164
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   165
val prems = goalw List.thy [map_def] 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   166
    "[| 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
   167
by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   168
qed "map_type";
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
val [major] = goal List.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   171
by (rtac (major RS map_type) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   172
by (etac RepFunI 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   173
qed "map_type2";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   174
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   175
(** length **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   176
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   177
val [length_Nil,length_Cons] = list_recs length_def;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   178
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   179
goalw List.thy [length_def] 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   180
    "!!l. l: list(A) ==> length(l) : nat";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   181
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
   182
qed "length_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   183
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   184
(** app **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   185
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   186
val [app_Nil,app_Cons] = list_recs app_def;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   187
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   188
goalw List.thy [app_def] 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   189
    "!!xs ys. [| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   190
by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   191
qed "app_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   192
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   193
(** rev **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   194
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   195
val [rev_Nil,rev_Cons] = list_recs rev_def;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   196
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   197
goalw List.thy [rev_def] 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   198
    "!!xs. xs: list(A) ==> rev(xs) : list(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   199
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
   200
qed "rev_type";
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
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   203
(** flat **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   204
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   205
val [flat_Nil,flat_Cons] = list_recs flat_def;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   206
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   207
goalw List.thy [flat_def] 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   208
    "!!ls. ls: list(list(A)) ==> flat(ls) : list(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   209
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
   210
qed "flat_type";
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
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   213
(** list_add **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   214
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   215
val [list_add_Nil,list_add_Cons] = list_recs list_add_def;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   216
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   217
goalw List.thy [list_add_def] 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   218
    "!!xs. xs: list(nat) ==> list_add(xs) : nat";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   219
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
   220
qed "list_add_type";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   221
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   222
(** List simplification **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   223
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   224
val list_typechecks =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   225
    list.intrs @
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   226
    [list_rec_type, map_type, map_type2, app_type, length_type, 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   227
     rev_type, flat_type, list_add_type];
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   228
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   229
val list_ss = arith_ss 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   230
    addsimps list.case_eqns
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   231
    addsimps [list_rec_Nil, list_rec_Cons, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 908
diff changeset
   232
              map_Nil, map_Cons, app_Nil, app_Cons,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 908
diff changeset
   233
              length_Nil, length_Cons, rev_Nil, rev_Cons,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 908
diff changeset
   234
              flat_Nil, flat_Cons, list_add_Nil, list_add_Cons]
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   235
    setsolver (type_auto_tac list_typechecks);
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
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   238
(*** theorems about map ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   239
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   240
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   241
    "l: list(A) ==> map(%u.u, l) = l";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   242
by (list_ind_tac "l" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   243
by (ALLGOALS (asm_simp_tac list_ss));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   244
qed "map_ident";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   245
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   246
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   247
    "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   248
by (list_ind_tac "l" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   249
by (ALLGOALS (asm_simp_tac list_ss));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   250
qed "map_compose";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   251
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   252
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   253
    "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   254
by (list_ind_tac "xs" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   255
by (ALLGOALS (asm_simp_tac list_ss));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   256
qed "map_app_distrib";
516
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
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   259
    "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   260
by (list_ind_tac "ls" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   261
by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   262
qed "map_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   263
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   264
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   265
    "l: list(A) ==> \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   266
\    list_rec(map(h,l), c, d) = \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   267
\    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   268
by (list_ind_tac "l" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   269
by (ALLGOALS (asm_simp_tac list_ss));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   270
qed "list_rec_map";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   271
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   272
(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
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
(* c : list(Collect(B,P)) ==> c : list(B) *)
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
   275
bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD));
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   276
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   277
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   278
    "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   279
by (list_ind_tac "l" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   280
by (ALLGOALS (asm_simp_tac list_ss));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   281
qed "map_list_Collect";
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
(*** theorems about length ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   284
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   285
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   286
    "xs: list(A) ==> length(map(h,xs)) = length(xs)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   287
by (list_ind_tac "xs" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   288
by (ALLGOALS (asm_simp_tac list_ss));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   289
qed "length_map";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   290
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   291
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   292
    "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   293
by (list_ind_tac "xs" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   294
by (ALLGOALS (asm_simp_tac list_ss));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   295
qed "length_app";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   296
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   297
(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   298
   Used for rewriting below*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   299
val add_commute_succ = nat_succI RSN (2,add_commute);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   300
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   301
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   302
    "xs: list(A) ==> length(rev(xs)) = length(xs)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   303
by (list_ind_tac "xs" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   304
by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   305
qed "length_rev";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   306
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   307
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   308
    "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   309
by (list_ind_tac "ls" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   310
by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   311
qed "length_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   312
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   313
(** Length and drop **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   314
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   315
(*Lemma for the inductive step of drop_length*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   316
goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   317
    "!!xs. xs: list(A) ==> \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   318
\          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
   319
by (etac list.induct 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   320
by (ALLGOALS (asm_simp_tac (list_ss addsimps [drop_0,drop_succ_Cons])));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   321
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   322
qed "drop_length_Cons_lemma";
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
   323
bind_thm ("drop_length_Cons", (drop_length_Cons_lemma RS spec));
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
goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   326
    "!!l. l: list(A) ==> ALL i: length(l).  EX z zs. drop(i,l) = Cons(z,zs)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   327
by (etac list.induct 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   328
by (ALLGOALS (asm_simp_tac (list_ss addsimps bquant_simps)));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   329
by (rtac conjI 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   330
by (etac drop_length_Cons 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   331
by (rtac ballI 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   332
by (rtac natE 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   333
by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   334
by (assume_tac 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   335
by (asm_simp_tac (list_ss addsimps [drop_0]) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   336
by (fast_tac ZF_cs 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   337
by (asm_simp_tac (list_ss addsimps [drop_succ_Cons]) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   338
by (dtac bspec 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   339
by (fast_tac ZF_cs 2);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   340
by (fast_tac (ZF_cs addEs [succ_in_naturalD,length_type]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   341
qed "drop_length_lemma";
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
   342
bind_thm ("drop_length", (drop_length_lemma RS bspec));
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   343
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   344
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   345
(*** theorems about app ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   346
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   347
val [major] = goal List.thy "xs: list(A) ==> xs@Nil=xs";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   348
by (rtac (major RS list.induct) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   349
by (ALLGOALS (asm_simp_tac list_ss));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   350
qed "app_right_Nil";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   351
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   352
val prems = goal List.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   353
by (list_ind_tac "xs" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   354
by (ALLGOALS (asm_simp_tac list_ss));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   355
qed "app_assoc";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   356
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   357
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   358
    "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   359
by (list_ind_tac "ls" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   360
by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   361
qed "flat_app_distrib";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   362
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   363
(*** theorems about rev ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   364
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   365
val prems = goal List.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   366
by (list_ind_tac "l" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   367
by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   368
qed "rev_map_distrib";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   369
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   370
(*Simplifier needs the premises as assumptions because rewriting will not
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   371
  instantiate the variable ?A in the rules' typing conditions; note that
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   372
  rev_type does not instantiate ?A.  Only the premises do.
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   373
*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   374
goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   375
    "!!xs. [| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   376
by (etac list.induct 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   377
by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   378
qed "rev_app_distrib";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   379
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   380
val prems = goal List.thy "l: list(A) ==> rev(rev(l))=l";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   381
by (list_ind_tac "l" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   382
by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   383
qed "rev_rev_ident";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   384
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   385
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   386
    "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   387
by (list_ind_tac "ls" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   388
by (ALLGOALS (asm_simp_tac (list_ss addsimps 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   389
       [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   390
qed "rev_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   391
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   392
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   393
(*** theorems about list_add ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   394
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   395
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   396
    "[| xs: list(nat);  ys: list(nat) |] ==> \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   397
\    list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   398
by (cut_facts_tac prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   399
by (list_ind_tac "xs" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   400
by (ALLGOALS 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   401
    (asm_simp_tac (list_ss addsimps [add_0_right, add_assoc RS sym])));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   402
by (rtac (add_commute RS subst_context) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   403
by (REPEAT (ares_tac [refl, list_add_type] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   404
qed "list_add_app";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   405
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   406
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   407
    "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   408
by (list_ind_tac "l" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   409
by (ALLGOALS
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   410
    (asm_simp_tac (list_ss addsimps [list_add_app, add_0_right])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   411
qed "list_add_rev";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   412
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   413
val prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   414
    "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   415
by (list_ind_tac "ls" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   416
by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app])));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   417
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
   418
qed "list_add_flat";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   419
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   420
(** New induction rule **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   421
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   422
val major::prems = goal List.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   423
    "[| l: list(A);  \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   424
\       P(Nil);        \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   425
\       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x]) \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   426
\    |] ==> P(l)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   427
by (rtac (major RS rev_rev_ident RS subst) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   428
by (rtac (major RS rev_type RS list.induct) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   429
by (ALLGOALS (asm_simp_tac (list_ss addsimps prems)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 525
diff changeset
   430
qed "list_append_induct";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
   431