src/HOLCF/IOA/meta_theory/Seq.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 6161 bc2a76ce1ea3
child 12218 6597093b77e7
permissions -rw-r--r--
` -> $
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/Seq.ML
mueller@3275
     2
    ID:         $Id$
mueller@3071
     3
    Author:     Olaf M"uller
mueller@3071
     4
    Copyright   1996  TU Muenchen
mueller@3071
     5
mueller@3071
     6
*)  
mueller@3071
     7
mueller@3071
     8
Addsimps (sfinite.intrs @ seq.rews);
mueller@3071
     9
mueller@3071
    10
mueller@3071
    11
(* Instead of adding UU_neq_nil every equation UU~=x could be changed to x~=UU *)
wenzelm@5068
    12
Goal "UU ~=nil";
mueller@3071
    13
by (res_inst_tac [("s1","UU"),("t1","nil")]  (sym RS rev_contrapos) 1);
mueller@3071
    14
by (REPEAT (Simp_tac 1));
mueller@3071
    15
qed"UU_neq_nil";
mueller@3071
    16
mueller@3071
    17
Addsimps [UU_neq_nil];
mueller@3071
    18
mueller@3275
    19
mueller@3275
    20
mueller@3275
    21
mueller@3071
    22
(* ------------------------------------------------------------------------------------- *)
mueller@3071
    23
mueller@3071
    24
mueller@3071
    25
(* ----------------------------------------------------  *)
mueller@3071
    26
       section "recursive equations of operators";
mueller@3071
    27
(* ----------------------------------------------------  *)
mueller@3071
    28
mueller@3071
    29
mueller@3071
    30
(* ----------------------------------------------------------- *)
mueller@3071
    31
(*                        smap                                 *)
mueller@3071
    32
(* ----------------------------------------------------------- *)
mueller@3071
    33
mueller@3071
    34
bind_thm ("smap_unfold", fix_prover2 thy smap_def 
mueller@3071
    35
   "smap = (LAM f tr. case tr of  \
mueller@3361
    36
 \                         nil  => nil \
nipkow@10835
    37
 \                       | x##xs => f$x ## smap$f$xs)");
mueller@3071
    38
nipkow@10835
    39
Goal "smap$f$nil=nil"; 
mueller@3071
    40
by (stac smap_unfold 1);
mueller@3071
    41
by (Simp_tac 1);
mueller@3071
    42
qed"smap_nil";
mueller@3071
    43
nipkow@10835
    44
Goal "smap$f$UU=UU"; 
mueller@3071
    45
by (stac smap_unfold 1);
mueller@3071
    46
by (Simp_tac 1);
mueller@3071
    47
qed"smap_UU";
mueller@3071
    48
wenzelm@5068
    49
Goal 
nipkow@10835
    50
"[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"; 
paulson@3457
    51
by (rtac trans 1);
mueller@3071
    52
by (stac smap_unfold 1);
mueller@3071
    53
by (Asm_full_simp_tac 1);
paulson@3457
    54
by (rtac refl 1);
mueller@3071
    55
qed"smap_cons";
mueller@3071
    56
mueller@3071
    57
(* ----------------------------------------------------------- *)
mueller@3071
    58
(*                        sfilter                              *)
mueller@3071
    59
(* ----------------------------------------------------------- *)
mueller@3071
    60
mueller@3071
    61
bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def 
mueller@3071
    62
  "sfilter = (LAM P tr. case tr of  \
mueller@3071
    63
 \         nil   => nil \
nipkow@10835
    64
 \       | x##xs => If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)");
mueller@3071
    65
nipkow@10835
    66
Goal "sfilter$P$nil=nil";
mueller@3071
    67
by (stac sfilter_unfold 1);
mueller@3071
    68
by (Simp_tac 1);
mueller@3071
    69
qed"sfilter_nil";
mueller@3071
    70
nipkow@10835
    71
Goal "sfilter$P$UU=UU";
mueller@3071
    72
by (stac sfilter_unfold 1);
mueller@3071
    73
by (Simp_tac 1);
mueller@3071
    74
qed"sfilter_UU";
mueller@3071
    75
wenzelm@5068
    76
Goal 
nipkow@10835
    77
"x~=UU ==> sfilter$P$(x##xs)=   \
nipkow@10835
    78
\             (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)";
paulson@3457
    79
by (rtac trans 1);
mueller@3071
    80
by (stac sfilter_unfold 1);
mueller@3071
    81
by (Asm_full_simp_tac 1);
paulson@3457
    82
by (rtac refl 1);
mueller@3071
    83
qed"sfilter_cons";
mueller@3071
    84
mueller@3071
    85
(* ----------------------------------------------------------- *)
mueller@3071
    86
(*                        sforall2                             *)
mueller@3071
    87
(* ----------------------------------------------------------- *)
mueller@3071
    88
mueller@3071
    89
bind_thm ("sforall2_unfold", fix_prover2 thy sforall2_def 
mueller@3071
    90
   "sforall2 = (LAM P tr. case tr of  \
mueller@3071
    91
 \                         nil   => TT \
nipkow@10835
    92
 \                       | x##xs => (P$x andalso sforall2$P$xs))");
mueller@3071
    93
nipkow@10835
    94
Goal "sforall2$P$nil=TT"; 
mueller@3071
    95
by (stac sforall2_unfold 1);
mueller@3071
    96
by (Simp_tac 1);
mueller@3071
    97
qed"sforall2_nil";
mueller@3071
    98
nipkow@10835
    99
Goal "sforall2$P$UU=UU"; 
mueller@3071
   100
by (stac sforall2_unfold 1);
mueller@3071
   101
by (Simp_tac 1);
mueller@3071
   102
qed"sforall2_UU";
mueller@3071
   103
wenzelm@5068
   104
Goal 
nipkow@10835
   105
"x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)";
paulson@3457
   106
by (rtac trans 1);
mueller@3071
   107
by (stac sforall2_unfold 1);
mueller@3071
   108
by (Asm_full_simp_tac 1);
paulson@3457
   109
by (rtac refl 1);
mueller@3071
   110
qed"sforall2_cons";
mueller@3071
   111
mueller@3071
   112
mueller@3071
   113
(* ----------------------------------------------------------- *)
mueller@3071
   114
(*                        stakewhile                           *)
mueller@3071
   115
(* ----------------------------------------------------------- *)
mueller@3071
   116
mueller@3071
   117
mueller@3071
   118
bind_thm ("stakewhile_unfold", fix_prover2 thy stakewhile_def 
mueller@3071
   119
   "stakewhile = (LAM P tr. case tr of  \
mueller@3071
   120
 \                         nil   => nil \
nipkow@10835
   121
 \                       | x##xs => (If P$x then x##(stakewhile$P$xs) else nil fi))");
mueller@3071
   122
nipkow@10835
   123
Goal "stakewhile$P$nil=nil"; 
mueller@3071
   124
by (stac stakewhile_unfold 1);
mueller@3071
   125
by (Simp_tac 1);
mueller@3071
   126
qed"stakewhile_nil";
mueller@3071
   127
nipkow@10835
   128
Goal "stakewhile$P$UU=UU"; 
mueller@3071
   129
by (stac stakewhile_unfold 1);
mueller@3071
   130
by (Simp_tac 1);
mueller@3071
   131
qed"stakewhile_UU";
mueller@3071
   132
wenzelm@5068
   133
Goal 
nipkow@10835
   134
"x~=UU ==> stakewhile$P$(x##xs) =   \
nipkow@10835
   135
\             (If P$x then x##(stakewhile$P$xs) else nil fi)";
paulson@3457
   136
by (rtac trans 1);
mueller@3071
   137
by (stac stakewhile_unfold 1);
mueller@3071
   138
by (Asm_full_simp_tac 1);
paulson@3457
   139
by (rtac refl 1);
mueller@3071
   140
qed"stakewhile_cons";
mueller@3071
   141
mueller@3071
   142
(* ----------------------------------------------------------- *)
mueller@3071
   143
(*                        sdropwhile                           *)
mueller@3071
   144
(* ----------------------------------------------------------- *)
mueller@3071
   145
mueller@3071
   146
mueller@3071
   147
bind_thm ("sdropwhile_unfold", fix_prover2 thy sdropwhile_def 
mueller@3071
   148
   "sdropwhile = (LAM P tr. case tr of  \
mueller@3071
   149
 \                         nil   => nil \
nipkow@10835
   150
 \                       | x##xs => (If P$x then sdropwhile$P$xs else tr fi))");
mueller@3071
   151
nipkow@10835
   152
Goal "sdropwhile$P$nil=nil"; 
mueller@3071
   153
by (stac sdropwhile_unfold 1);
mueller@3071
   154
by (Simp_tac 1);
mueller@3071
   155
qed"sdropwhile_nil";
mueller@3071
   156
nipkow@10835
   157
Goal "sdropwhile$P$UU=UU"; 
mueller@3071
   158
by (stac sdropwhile_unfold 1);
mueller@3071
   159
by (Simp_tac 1);
mueller@3071
   160
qed"sdropwhile_UU";
mueller@3071
   161
wenzelm@5068
   162
Goal 
nipkow@10835
   163
"x~=UU ==> sdropwhile$P$(x##xs) =   \
nipkow@10835
   164
\             (If P$x then sdropwhile$P$xs else x##xs fi)";
paulson@3457
   165
by (rtac trans 1);
mueller@3071
   166
by (stac sdropwhile_unfold 1);
mueller@3071
   167
by (Asm_full_simp_tac 1);
paulson@3457
   168
by (rtac refl 1);
mueller@3071
   169
qed"sdropwhile_cons";
mueller@3071
   170
mueller@3071
   171
mueller@3071
   172
(* ----------------------------------------------------------- *)
mueller@3071
   173
(*                        slast                                 *)
mueller@3071
   174
(* ----------------------------------------------------------- *)
mueller@3071
   175
mueller@3071
   176
mueller@3071
   177
bind_thm ("slast_unfold", fix_prover2 thy slast_def 
mueller@3071
   178
   "slast = (LAM tr. case tr of  \
mueller@3071
   179
 \                         nil   => UU \
nipkow@10835
   180
 \                       | x##xs => (If is_nil$xs then x else slast$xs fi))");
mueller@3071
   181
mueller@3071
   182
nipkow@10835
   183
Goal "slast$nil=UU"; 
mueller@3071
   184
by (stac slast_unfold 1);
mueller@3071
   185
by (Simp_tac 1);
mueller@3071
   186
qed"slast_nil";
mueller@3071
   187
nipkow@10835
   188
Goal "slast$UU=UU"; 
mueller@3071
   189
by (stac slast_unfold 1);
mueller@3071
   190
by (Simp_tac 1);
mueller@3071
   191
qed"slast_UU";
mueller@3071
   192
wenzelm@5068
   193
Goal 
nipkow@10835
   194
"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)";
paulson@3457
   195
by (rtac trans 1);
mueller@3071
   196
by (stac slast_unfold 1);
mueller@3071
   197
by (Asm_full_simp_tac 1);
paulson@3457
   198
by (rtac refl 1);
mueller@3071
   199
qed"slast_cons";
mueller@3071
   200
mueller@3071
   201
mueller@3071
   202
(* ----------------------------------------------------------- *)
mueller@3071
   203
(*                        sconc                                 *)
mueller@3071
   204
(* ----------------------------------------------------------- *)
mueller@3071
   205
mueller@3071
   206
bind_thm ("sconc_unfold", fix_prover2 thy sconc_def 
mueller@3071
   207
   "sconc = (LAM t1 t2. case t1 of  \
mueller@3071
   208
 \                         nil   => t2 \
mueller@3071
   209
 \                       | x##xs => x ## (xs @@ t2))");
mueller@3071
   210
mueller@3071
   211
wenzelm@5068
   212
Goal "nil @@ y = y"; 
mueller@3071
   213
by (stac sconc_unfold 1);
mueller@3071
   214
by (Simp_tac 1);
mueller@3071
   215
qed"sconc_nil";
mueller@3071
   216
wenzelm@5068
   217
Goal "UU @@ y=UU"; 
mueller@3071
   218
by (stac sconc_unfold 1);
mueller@3071
   219
by (Simp_tac 1);
mueller@3071
   220
qed"sconc_UU";
mueller@3071
   221
wenzelm@5068
   222
Goal "(x##xs) @@ y=x##(xs @@ y)";
paulson@3457
   223
by (rtac trans 1);
mueller@3071
   224
by (stac sconc_unfold 1);
mueller@3071
   225
by (Asm_full_simp_tac 1);
mueller@3071
   226
by (case_tac "x=UU" 1);
mueller@3071
   227
by (REPEAT (Asm_full_simp_tac 1));
mueller@3071
   228
qed"sconc_cons";
mueller@3071
   229
mueller@3275
   230
Addsimps [sconc_nil,sconc_UU,sconc_cons];
mueller@3071
   231
mueller@3071
   232
mueller@3071
   233
(* ----------------------------------------------------------- *)
mueller@3071
   234
(*                        sflat                                 *)
mueller@3071
   235
(* ----------------------------------------------------------- *)
mueller@3071
   236
mueller@3071
   237
bind_thm ("sflat_unfold", fix_prover2 thy sflat_def 
mueller@3071
   238
   "sflat = (LAM tr. case tr of  \
mueller@3071
   239
 \                         nil   => nil \
nipkow@10835
   240
 \                       | x##xs => x @@ sflat$xs)");
mueller@3071
   241
nipkow@10835
   242
Goal "sflat$nil=nil"; 
mueller@3071
   243
by (stac sflat_unfold 1);
mueller@3071
   244
by (Simp_tac 1);
mueller@3071
   245
qed"sflat_nil";
mueller@3071
   246
nipkow@10835
   247
Goal "sflat$UU=UU"; 
mueller@3071
   248
by (stac sflat_unfold 1);
mueller@3071
   249
by (Simp_tac 1);
mueller@3071
   250
qed"sflat_UU";
mueller@3071
   251
nipkow@10835
   252
Goal "sflat$(x##xs)= x@@(sflat$xs)"; 
paulson@3457
   253
by (rtac trans 1);
mueller@3071
   254
by (stac sflat_unfold 1);
mueller@3071
   255
by (Asm_full_simp_tac 1);
mueller@3071
   256
by (case_tac "x=UU" 1);
mueller@3071
   257
by (REPEAT (Asm_full_simp_tac 1));
mueller@3071
   258
qed"sflat_cons";
mueller@3071
   259
mueller@3071
   260
mueller@3071
   261
mueller@3071
   262
mueller@3071
   263
(* ----------------------------------------------------------- *)
mueller@3071
   264
(*                        szip                                 *)
mueller@3071
   265
(* ----------------------------------------------------------- *)
mueller@3071
   266
mueller@3071
   267
bind_thm ("szip_unfold", fix_prover2 thy szip_def 
mueller@3071
   268
   "szip = (LAM t1 t2. case t1 of \
mueller@3071
   269
\               nil   => nil    \
mueller@3071
   270
\             | x##xs => (case t2 of     \
mueller@3071
   271
\                          nil => UU    \
nipkow@10835
   272
\                        | y##ys => <x,y>##(szip$xs$ys)))");
mueller@3071
   273
nipkow@10835
   274
Goal "szip$nil$y=nil"; 
mueller@3071
   275
by (stac szip_unfold 1);
mueller@3071
   276
by (Simp_tac 1);
mueller@3071
   277
qed"szip_nil";
mueller@3071
   278
nipkow@10835
   279
Goal "szip$UU$y=UU"; 
mueller@3071
   280
by (stac szip_unfold 1);
mueller@3071
   281
by (Simp_tac 1);
mueller@3071
   282
qed"szip_UU1";
mueller@3071
   283
nipkow@10835
   284
Goal "x~=nil ==> szip$x$UU=UU"; 
mueller@3071
   285
by (stac szip_unfold 1);
mueller@3071
   286
by (Asm_full_simp_tac 1);
oheimb@4042
   287
by (res_inst_tac [("x","x")] seq.casedist 1);
mueller@3071
   288
by (REPEAT (Asm_full_simp_tac 1));
mueller@3071
   289
qed"szip_UU2";
mueller@3071
   290
nipkow@10835
   291
Goal "x~=UU ==> szip$(x##xs)$nil=UU";
paulson@3457
   292
by (rtac trans 1);
mueller@3071
   293
by (stac szip_unfold 1);
mueller@3071
   294
by (REPEAT (Asm_full_simp_tac 1));
mueller@3071
   295
qed"szip_cons_nil";
mueller@3071
   296
nipkow@10835
   297
Goal "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys";
paulson@3457
   298
by (rtac trans 1);
mueller@3071
   299
by (stac szip_unfold 1);
mueller@3071
   300
by (REPEAT (Asm_full_simp_tac 1));
mueller@3071
   301
qed"szip_cons";
mueller@3071
   302
mueller@3071
   303
mueller@3071
   304
Addsimps [sfilter_UU,sfilter_nil,sfilter_cons,
mueller@3071
   305
          smap_UU,smap_nil,smap_cons,
mueller@3071
   306
          sforall2_UU,sforall2_nil,sforall2_cons,
mueller@3071
   307
          slast_UU,slast_nil,slast_cons,
mueller@3071
   308
          stakewhile_UU, stakewhile_nil, stakewhile_cons, 
mueller@3071
   309
          sdropwhile_UU, sdropwhile_nil, sdropwhile_cons,
mueller@3071
   310
          sflat_UU,sflat_nil,sflat_cons,
mueller@3071
   311
          szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons]; 
mueller@3071
   312
mueller@3071
   313
mueller@3071
   314
mueller@3071
   315
(* ------------------------------------------------------------------------------------- *)
mueller@3071
   316
mueller@3275
   317
section "scons, nil";
mueller@3071
   318
wenzelm@5068
   319
Goal 
paulson@6161
   320
 "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
mueller@3071
   321
by (rtac iffI 1);
mueller@3071
   322
by (etac (hd seq.injects) 1);
paulson@4477
   323
by Auto_tac;
mueller@3071
   324
qed"scons_inject_eq";
mueller@3071
   325
paulson@6161
   326
Goal "nil<<x ==> nil=x";
oheimb@4042
   327
by (res_inst_tac [("x","x")] seq.casedist 1);
mueller@3275
   328
by (hyp_subst_tac 1);
mueller@3275
   329
by (etac antisym_less 1);
mueller@3275
   330
by (Asm_full_simp_tac 1);
mueller@3275
   331
by (Asm_full_simp_tac 1);
mueller@3275
   332
by (hyp_subst_tac 1);
mueller@3275
   333
by (Asm_full_simp_tac 1);
mueller@3275
   334
qed"nil_less_is_nil";
mueller@3071
   335
mueller@3071
   336
(* ------------------------------------------------------------------------------------- *)
mueller@3071
   337
mueller@3071
   338
section "sfilter, sforall, sconc";
mueller@3071
   339
mueller@3071
   340
wenzelm@5068
   341
Goal  "(if b then tr1 else tr2) @@ tr \
mueller@3071
   342
        \= (if b then tr1 @@ tr else tr2 @@ tr)";
mueller@3071
   343
by (res_inst_tac [("P","b"),("Q","b")] impCE 1);
mueller@3071
   344
by (fast_tac HOL_cs 1);
mueller@3071
   345
by (REPEAT (Asm_full_simp_tac 1));
mueller@3071
   346
qed"if_and_sconc";
mueller@3071
   347
mueller@3071
   348
Addsimps [if_and_sconc];
mueller@3071
   349
mueller@3071
   350
nipkow@10835
   351
Goal "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)";
mueller@3071
   352
mueller@3071
   353
by (res_inst_tac[("x","x")] seq.ind 1);
mueller@3071
   354
(* adm *)
mueller@3071
   355
by (Simp_tac 1);
mueller@3071
   356
(* base cases *)
mueller@3071
   357
by (Simp_tac 1);
mueller@3071
   358
by (Simp_tac 1);
mueller@3071
   359
(* main case *)
wenzelm@4098
   360
by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
mueller@3071
   361
qed"sfiltersconc";
mueller@3071
   362
nipkow@10835
   363
Goal "sforall P (stakewhile$P$x)";
wenzelm@4098
   364
by (simp_tac (simpset() addsimps [sforall_def]) 1);
mueller@3071
   365
by (res_inst_tac[("x","x")] seq.ind 1);
mueller@3071
   366
(* adm *)
wenzelm@4098
   367
by (simp_tac (simpset() addsimps [adm_trick_1]) 1);
mueller@3071
   368
(* base cases *)
mueller@3071
   369
by (Simp_tac 1);
mueller@3071
   370
by (Simp_tac 1);
mueller@3071
   371
(* main case *)
wenzelm@4098
   372
by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
mueller@3071
   373
qed"sforallPstakewhileP";
mueller@3071
   374
nipkow@10835
   375
Goal "sforall P (sfilter$P$x)";
wenzelm@4098
   376
by (simp_tac (simpset() addsimps [sforall_def]) 1);
mueller@3071
   377
by (res_inst_tac[("x","x")] seq.ind 1);
mueller@3071
   378
(* adm *)
wenzelm@4098
   379
by (simp_tac (simpset() addsimps [adm_trick_1]) 1);
mueller@3071
   380
(* base cases *)
mueller@3071
   381
by (Simp_tac 1);
mueller@3071
   382
by (Simp_tac 1);
mueller@3071
   383
(* main case *)
wenzelm@4098
   384
by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
mueller@3071
   385
qed"forallPsfilterP";
mueller@3071
   386
mueller@3071
   387
mueller@3071
   388
mueller@3071
   389
(* ------------------------------------------------------------------------------------- *)
mueller@3071
   390
mueller@3071
   391
section "Finite";
mueller@3071
   392
mueller@3071
   393
(* ----------------------------------------------------  *)
mueller@3071
   394
(* Proofs of rewrite rules for Finite:                  *)
mueller@3071
   395
(* 1. Finite(nil),   (by definition)                    *)
mueller@3071
   396
(* 2. ~Finite(UU),                                      *)
mueller@3071
   397
(* 3. a~=UU==> Finite(a##x)=Finite(x)                  *)
mueller@3071
   398
(* ----------------------------------------------------  *)
mueller@3071
   399
wenzelm@5068
   400
Goal "Finite x --> x~=UU";
paulson@3457
   401
by (rtac impI 1);
paulson@3457
   402
by (etac sfinite.induct 1);
mueller@3071
   403
 by (Asm_full_simp_tac 1);
mueller@3071
   404
by (Asm_full_simp_tac 1);
mueller@3071
   405
qed"Finite_UU_a";
mueller@3071
   406
wenzelm@5068
   407
Goal "~(Finite UU)";
mueller@3071
   408
by (cut_inst_tac [("x","UU")]Finite_UU_a  1);
mueller@3071
   409
by (fast_tac HOL_cs 1);
mueller@3071
   410
qed"Finite_UU";
mueller@3071
   411
wenzelm@5068
   412
Goal "Finite x --> a~=UU --> x=a##xs --> Finite xs";
mueller@3071
   413
by (strip_tac 1);
paulson@3457
   414
by (etac sfinite.elim 1);
wenzelm@4098
   415
by (fast_tac (HOL_cs addss simpset()) 1);
mueller@3071
   416
by (fast_tac (HOL_cs addSDs seq.injects) 1);
mueller@3071
   417
qed"Finite_cons_a";
mueller@3071
   418
paulson@6161
   419
Goal "a~=UU ==>(Finite (a##x)) = (Finite x)";
mueller@3071
   420
by (rtac iffI 1);
mueller@3071
   421
by (rtac (Finite_cons_a RS mp RS mp RS mp) 1);
mueller@3071
   422
by (REPEAT (assume_tac 1));
mueller@3071
   423
by (fast_tac HOL_cs 1);
mueller@3071
   424
by (Asm_full_simp_tac 1);
mueller@3071
   425
qed"Finite_cons";
mueller@3071
   426
mueller@3071
   427
Addsimps [Finite_UU];
mueller@3071
   428
mueller@3071
   429
mueller@3071
   430
(* ------------------------------------------------------------------------------------- *)
mueller@3071
   431
mueller@3071
   432
section "induction";
mueller@3071
   433
mueller@3071
   434
mueller@3071
   435
(*--------------------------------   *)
mueller@3071
   436
(* Extensions to Induction Theorems  *)
mueller@3071
   437
(*--------------------------------   *)
mueller@3071
   438
mueller@3071
   439
mueller@3071
   440
qed_goalw "seq_finite_ind_lemma" thy  [seq.finite_def]
nipkow@10835
   441
"(!!n. P(seq_take n$s)) ==>  seq_finite(s) -->P(s)"
mueller@3071
   442
 (fn prems =>
mueller@3071
   443
        [
mueller@3071
   444
        (strip_tac 1),
mueller@3071
   445
        (etac exE 1),
mueller@3071
   446
        (etac subst 1),
mueller@3071
   447
        (resolve_tac prems 1)
mueller@3071
   448
        ]);
mueller@3071
   449
mueller@3071
   450
paulson@6161
   451
Goal "!!P.[|P(UU);P(nil);\
mueller@3071
   452
\  !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\
mueller@3071
   453
\  |] ==> seq_finite(s) --> P(s)";
mueller@3071
   454
by (rtac seq_finite_ind_lemma 1);
paulson@3457
   455
by (etac seq.finite_ind 1);
paulson@3457
   456
 by (assume_tac 1);
mueller@3071
   457
by (Asm_full_simp_tac 1);
mueller@3071
   458
qed"seq_finite_ind";
mueller@3071
   459
mueller@3071
   460