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