src/ZF/listfn.ML
author lcp
Tue, 05 Oct 1993 15:21:29 +0100
changeset 25 3ac1c0c0016e
parent 14 1c0926788772
permissions -rw-r--r--
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many changes epsilon,arith: many changes ordinal/succ_mem_succI/E: deleted; use succ_leI/E nat/nat_0_in_succ: deleted; use nat_0_le univ/Vset_rankI: deleted; use VsetI
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
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    11
(** hd and tl **)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    12
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    13
goalw ListFn.thy [hd_def] "hd(Cons(a,l)) = a";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    14
by (resolve_tac List.case_eqns 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    15
val hd_Cons = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    16
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    17
goalw ListFn.thy [tl_def] "tl(Nil) = Nil";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    18
by (resolve_tac List.case_eqns 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    19
val tl_Nil = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    20
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    21
goalw ListFn.thy [tl_def] "tl(Cons(a,l)) = l";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    22
by (resolve_tac List.case_eqns 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    23
val tl_Cons = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    24
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    25
goal ListFn.thy "!!l. l: list(A) ==> tl(l) : list(A)";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    26
by (etac List.elim 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    27
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.intrs @ [tl_Nil,tl_Cons]))));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    28
val tl_type = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    29
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    30
(** drop **)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    31
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    32
goalw ListFn.thy [drop_def] "drop(0, l) = l";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    33
by (rtac rec_0 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    34
val drop_0 = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    35
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    36
goalw ListFn.thy [drop_def] "!!i. i:nat ==> drop(i, Nil) = Nil";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    37
by (etac nat_induct 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    38
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Nil])));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    39
val drop_Nil = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    40
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    41
goalw ListFn.thy [drop_def]
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    42
    "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    43
by (etac nat_induct 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    44
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Cons])));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    45
val drop_succ_Cons = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    46
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    47
goalw ListFn.thy [drop_def] 
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    48
    "!!i l. [| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    49
by (etac nat_induct 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    50
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_type])));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    51
val drop_type = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
(** list_rec -- by Vset recursion **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
goal ListFn.thy "list_rec(Nil,c,h) = c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
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
    57
by (simp_tac (ZF_ss addsimps List.case_eqns) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
val list_rec_Nil = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
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
    61
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
    62
by (simp_tac (rank_ss addsimps (rank_Cons2::List.case_eqns)) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
val list_rec_Cons = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
(*Type checking -- proved by induction, as usual*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
    "[| l: list(A);    \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
\       c: C(Nil);       \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
\       !!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
    70
\    |] ==> list_rec(l,c,h) : C(l)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
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
    72
by (ALLGOALS (asm_simp_tac
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    73
	      (ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons]))));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
val list_rec_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
(** Versions for use with definitions **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
val [rew] = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
by (rtac list_rec_Nil 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
val def_list_rec_Nil = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
val [rew] = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
by (rtac list_rec_Cons 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
val def_list_rec_Cons = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
fun list_recs def = map standard
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
    	([def] RL [def_list_rec_Nil, def_list_rec_Cons]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
(** map **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
val [map_Nil,map_Cons] = list_recs map_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
val prems = goalw ListFn.thy [map_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
    "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
by (REPEAT (ares_tac (prems@[list_rec_type, NilI, ConsI]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
val map_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
val [major] = goal ListFn.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
by (rtac (major RS map_type) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
by (etac RepFunI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
val map_type2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
(** length **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
val [length_Nil,length_Cons] = list_recs length_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   111
goalw ListFn.thy [length_def] 
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   112
    "!!l. l: list(A) ==> length(l) : nat";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   113
by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
val length_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
(** app **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
val [app_Nil,app_Cons] = list_recs app_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   120
goalw ListFn.thy [app_def] 
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   121
    "!!xs ys. [| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   122
by (REPEAT (ares_tac [list_rec_type, ConsI] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
val app_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
(** rev **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
val [rev_Nil,rev_Cons] = list_recs rev_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
val prems = goalw ListFn.thy [rev_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
    "xs: list(A) ==> rev(xs) : list(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
val rev_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
(** flat **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
val [flat_Nil,flat_Cons] = list_recs flat_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
val prems = goalw ListFn.thy [flat_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
    "ls: list(list(A)) ==> flat(ls) : list(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
val flat_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
(** list_add **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
val [list_add_Nil,list_add_Cons] = list_recs list_add_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
val prems = goalw ListFn.thy [list_add_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
    "xs: list(nat) ==> list_add(xs) : nat";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, add_type]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
val list_add_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
(** ListFn simplification **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
val list_typechecks =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
      [NilI, ConsI, list_rec_type,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
       map_type, map_type2, app_type, length_type, rev_type, flat_type,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
       list_add_type];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
val list_ss = arith_ss 
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   162
    addsimps List.case_eqns
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   163
    addsimps [list_rec_Nil, list_rec_Cons, 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
	     map_Nil, map_Cons,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
	     app_Nil, app_Cons,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
	     length_Nil, length_Cons,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
	     rev_Nil, rev_Cons,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
	     flat_Nil, flat_Cons,
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   169
	     list_add_Nil, list_add_Cons]
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   170
    setsolver (type_auto_tac list_typechecks);
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   171
(*Could also rewrite using the list_typechecks...*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
(*** theorems about map ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
    "l: list(A) ==> map(%u.u, l) = l";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
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
   178
by (ALLGOALS (asm_simp_tac list_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
val map_ident = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
    "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
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
   184
by (ALLGOALS (asm_simp_tac list_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
val map_compose = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
    "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
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
   190
by (ALLGOALS (asm_simp_tac list_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
val map_app_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
    "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
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
   196
by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
val map_flat = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
    "l: list(A) ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
\    list_rec(map(h,l), c, d) = \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
\    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
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
   204
by (ALLGOALS (asm_simp_tac list_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
val list_rec_map = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
(* c : list(Collect(B,P)) ==> c : list(B) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
val list_CollectD = standard (Collect_subset RS list_mono RS subsetD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
    "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
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
   215
by (ALLGOALS (asm_simp_tac list_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
val map_list_Collect = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
(*** theorems about length ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
    "xs: list(A) ==> length(map(h,xs)) = length(xs)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
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
   223
by (ALLGOALS (asm_simp_tac list_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
val length_map = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
    "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
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
   229
by (ALLGOALS (asm_simp_tac list_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
val length_app = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
   Used for rewriting below*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
val add_commute_succ = nat_succI RSN (2,add_commute);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
    "xs: list(A) ==> length(rev(xs)) = length(xs)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
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
   239
by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
val length_rev = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
    "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
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
   245
by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
val length_flat = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   248
(** Length and drop **)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   249
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   250
(*Lemma for the inductive step of drop_length*)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   251
goal ListFn.thy
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   252
    "!!xs. xs: list(A) ==> \
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   253
\          ALL x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   254
by (etac List.induct 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   255
by (ALLGOALS (asm_simp_tac (list_ss addsimps [drop_0,drop_succ_Cons])));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   256
by (fast_tac ZF_cs 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   257
val drop_length_Cons_lemma = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   258
val drop_length_Cons = standard (drop_length_Cons_lemma RS spec);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   259
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   260
goal ListFn.thy
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   261
    "!!l. l: list(A) ==> ALL i: length(l).  EX z zs. drop(i,l) = Cons(z,zs)";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   262
by (etac List.induct 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   263
by (ALLGOALS (asm_simp_tac (list_ss addsimps bquant_simps)));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   264
by (rtac conjI 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   265
by (etac drop_length_Cons 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   266
by (rtac ballI 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   267
by (rtac natE 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   268
by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   269
by (assume_tac 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   270
by (asm_simp_tac (list_ss addsimps [drop_0]) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   271
by (fast_tac ZF_cs 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   272
by (asm_simp_tac (list_ss addsimps [drop_succ_Cons]) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   273
by (dtac bspec 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   274
by (fast_tac ZF_cs 2);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   275
by (fast_tac (ZF_cs addEs [succ_in_naturalD,length_type]) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   276
val drop_length_lemma = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   277
val drop_length = standard (drop_length_lemma RS bspec);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   278
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   279
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
(*** theorems about app ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
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
   284
by (ALLGOALS (asm_simp_tac list_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
val app_right_Nil = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
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
   289
by (ALLGOALS (asm_simp_tac list_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
val app_assoc = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
    "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
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
   295
by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
val flat_app_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
(*** theorems about rev ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
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
   302
by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
val rev_map_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
(*Simplifier needs the premises as assumptions because rewriting will not
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
  instantiate the variable ?A in the rules' typing conditions; note that
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
  rev_type does not instantiate ?A.  Only the premises do.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
*)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   309
goal ListFn.thy
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   310
    "!!xs. [| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
by (etac List.induct 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   312
by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
val rev_app_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
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
   317
by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
val rev_rev_ident = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
    "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
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
   323
by (ALLGOALS (asm_simp_tac (list_ss addsimps 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
       [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
val rev_flat = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
(*** theorems about list_add ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
    "[| xs: list(nat);  ys: list(nat) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
\    list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
by (list_ind_tac "xs" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
by (ALLGOALS 
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   336
    (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
   337
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
   338
by (REPEAT (ares_tac [refl, list_add_type] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
val list_add_app = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
    "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
by (list_ind_tac "l" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
by (ALLGOALS
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   345
    (asm_simp_tac (list_ss addsimps [list_add_app, add_0_right])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
val list_add_rev = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
val prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
    "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
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
   351
by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
val list_add_flat = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
(** New induction rule **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
val major::prems = goal ListFn.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
    "[| l: list(A);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
\       P(Nil);        \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
\       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x]) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
\    |] ==> P(l)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
by (rtac (major RS rev_rev_ident RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
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
   364
by (ALLGOALS (asm_simp_tac (list_ss addsimps prems)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
val list_append_induct = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366