src/ZF/listfn.ML
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/list-fn.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For list-fn.thy.  Lists in Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open ListFn;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
(** list_rec -- by Vset recursion **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
(*Used to verify list_rec*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
val list_rec_ss = ZF_ss 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
      addcongs (mk_typed_congs ListFn.thy [("h", "[i,i,i]=>i")])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
      addrews List.case_eqns;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
goal ListFn.thy "list_rec(Nil,c,h) = c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
by (SIMP_TAC list_rec_ss 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
val list_rec_Nil = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
by (SIMP_TAC (list_rec_ss addrews [Vset_rankI, rank_Cons2]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val list_rec_Cons = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
(*Type checking -- proved by induction, as usual*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
    "[| l: list(A);    \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
\       c: C(Nil);       \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
\       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
\    |] ==> list_rec(l,c,h) : C(l)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
by (list_ind_tac "l" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
by (ALLGOALS (ASM_SIMP_TAC
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
	      (ZF_ss addrews (prems@[list_rec_Nil,list_rec_Cons]))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val list_rec_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
(** Versions for use with definitions **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
val [rew] = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
by (rtac list_rec_Nil 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
val def_list_rec_Nil = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
val [rew] = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
by (rtac list_rec_Cons 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
val def_list_rec_Cons = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
fun list_recs def = map standard
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
    	([def] RL [def_list_rec_Nil, def_list_rec_Cons]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
(** map **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
val [map_Nil,map_Cons] = list_recs map_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
val prems = goalw ListFn.thy [map_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
    "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (REPEAT (ares_tac (prems@[list_rec_type, NilI, ConsI]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
val map_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
val [major] = goal ListFn.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
by (rtac (major RS map_type) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
by (etac RepFunI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
val map_type2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
(** length **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
val [length_Nil,length_Cons] = list_recs length_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val prems = goalw ListFn.thy [length_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
    "l: list(A) ==> length(l) : nat";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, nat_succI]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
val length_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
(** app **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
val [app_Nil,app_Cons] = list_recs app_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
val prems = goalw ListFn.thy [app_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
    "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
by (REPEAT (ares_tac (prems @ [list_rec_type, ConsI]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
val app_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
(** rev **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
val [rev_Nil,rev_Cons] = list_recs rev_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
val prems = goalw ListFn.thy [rev_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
    "xs: list(A) ==> rev(xs) : list(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
val rev_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
(** flat **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
val [flat_Nil,flat_Cons] = list_recs flat_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
val prems = goalw ListFn.thy [flat_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
    "ls: list(list(A)) ==> flat(ls) : list(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
val flat_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
(** list_add **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
val [list_add_Nil,list_add_Cons] = list_recs list_add_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
val prems = goalw ListFn.thy [list_add_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
    "xs: list(nat) ==> list_add(xs) : nat";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, add_type]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
val list_add_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
(** ListFn simplification **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
val list_typechecks =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
      [NilI, ConsI, list_rec_type,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
       map_type, map_type2, app_type, length_type, rev_type, flat_type,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
       list_add_type];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
val list_congs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
    List.congs @ 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
    mk_congs ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
        ["list_rec","map","op @","length","rev","flat","list_add"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
val list_ss = arith_ss 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
    addcongs list_congs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
    addrews List.case_eqns
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
    addrews list_typechecks
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
    addrews [list_rec_Nil, list_rec_Cons, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
	     map_Nil, map_Cons,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
	     app_Nil, app_Cons,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
	     length_Nil, length_Cons,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
	     rev_Nil, rev_Cons,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
	     flat_Nil, flat_Cons,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
	     list_add_Nil, list_add_Cons];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
(*** theorems about map ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
    "l: list(A) ==> map(%u.u, l) = l";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
by (list_ind_tac "l" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
by (ALLGOALS (ASM_SIMP_TAC list_ss));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
val map_ident = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
    "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
by (list_ind_tac "l" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
by (ALLGOALS (ASM_SIMP_TAC list_ss));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
val map_compose = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
    "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
by (list_ind_tac "xs" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
by (ALLGOALS (ASM_SIMP_TAC list_ss));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
val map_app_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
    "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
by (list_ind_tac "ls" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
val map_flat = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
    "l: list(A) ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
\    list_rec(map(h,l), c, d) = \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
\    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
by (list_ind_tac "l" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
by (ALLGOALS 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
    (ASM_SIMP_TAC 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
     (list_ss addcongs (mk_typed_congs ListFn.thy [("d", "[i,i,i]=>i")]))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
val list_rec_map = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
(* c : list(Collect(B,P)) ==> c : list(B) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
val list_CollectD = standard (Collect_subset RS list_mono RS subsetD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
    "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
by (list_ind_tac "l" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
by (ALLGOALS (ASM_SIMP_TAC list_ss));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
val map_list_Collect = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
(*** theorems about length ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
    "xs: list(A) ==> length(map(h,xs)) = length(xs)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
by (list_ind_tac "xs" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
by (ALLGOALS (ASM_SIMP_TAC list_ss));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
val length_map = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
    "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
by (list_ind_tac "xs" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
by (ALLGOALS (ASM_SIMP_TAC list_ss));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
val length_app = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
   Used for rewriting below*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
val add_commute_succ = nat_succI RSN (2,add_commute);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
    "xs: list(A) ==> length(rev(xs)) = length(xs)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
by (list_ind_tac "xs" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app, add_commute_succ])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
val length_rev = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
    "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
by (list_ind_tac "ls" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
val length_flat = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
(*** theorems about app ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
by (rtac (major RS List.induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
by (ALLGOALS (ASM_SIMP_TAC list_ss));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
val app_right_Nil = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
by (list_ind_tac "xs" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
by (ALLGOALS (ASM_SIMP_TAC list_ss));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
val app_assoc = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
    "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
by (list_ind_tac "ls" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_assoc])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
val flat_app_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
(*** theorems about rev ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
by (list_ind_tac "l" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
val rev_map_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
(*Simplifier needs the premises as assumptions because rewriting will not
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
  instantiate the variable ?A in the rules' typing conditions; note that
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
  rev_type does not instantiate ?A.  Only the premises do.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
    "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
by (etac List.induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_right_Nil,app_assoc])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
val rev_app_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
by (list_ind_tac "l" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [rev_app_distrib])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
val rev_rev_ident = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
    "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
by (list_ind_tac "ls" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
       [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
val rev_flat = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
(*** theorems about list_add ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
    "[| xs: list(nat);  ys: list(nat) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
\    list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
by (list_ind_tac "xs" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
by (ALLGOALS 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
    (ASM_SIMP_TAC (list_ss addrews [add_0_right, add_assoc RS sym])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
by (resolve_tac arith_congs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
by (REPEAT (ares_tac [refl, list_add_type, add_commute] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
val list_add_app = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
    "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
by (list_ind_tac "l" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
by (ALLGOALS
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
    (ASM_SIMP_TAC (list_ss addrews [list_add_app, add_0_right])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
val list_add_rev = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
    "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
by (list_ind_tac "ls" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [list_add_app])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
val list_add_flat = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
(** New induction rule **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
val major::prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
    "[| l: list(A);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
\       P(Nil);        \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
\       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x]) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
\    |] ==> P(l)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
by (rtac (major RS rev_rev_ident RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
by (rtac (major RS rev_type RS List.induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews prems)));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
val list_append_induct = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306