src/HOLCF/IOA/meta_theory/Seq.thy
author wenzelm
Thu Apr 26 14:24:08 2007 +0200 (2007-04-26)
changeset 22808 a7daa74e2980
parent 19804 d0318ae1141c
child 23778 18f426a137a9
permissions -rw-r--r--
eliminated unnamed infixes, tuned syntax;
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/Seq.thy
mueller@3275
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
wenzelm@17233
     4
*)
mueller@3071
     5
wenzelm@17233
     6
header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
mueller@3071
     7
wenzelm@17233
     8
theory Seq
wenzelm@17233
     9
imports HOLCF
wenzelm@17233
    10
begin
mueller@3071
    11
wenzelm@22808
    12
domain 'a seq = nil | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
mueller@3071
    13
wenzelm@17233
    14
consts
wenzelm@17233
    15
   sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"
mueller@3071
    16
   smap          :: "('a -> 'b) -> 'a seq -> 'b seq"
mueller@3071
    17
   sforall       :: "('a -> tr) => 'a seq => bool"
mueller@3071
    18
   sforall2      :: "('a -> tr) -> 'a seq -> tr"
mueller@3071
    19
   slast         :: "'a seq     -> 'a"
mueller@3071
    20
   sconc         :: "'a seq     -> 'a seq -> 'a seq"
wenzelm@17233
    21
   sdropwhile    ::"('a -> tr)  -> 'a seq -> 'a seq"
wenzelm@17233
    22
   stakewhile    ::"('a -> tr)  -> 'a seq -> 'a seq"
wenzelm@17233
    23
   szip          ::"'a seq      -> 'b seq -> ('a*'b) seq"
mueller@3071
    24
   sflat        :: "('a seq) seq  -> 'a seq"
mueller@3071
    25
mueller@3071
    26
   sfinite       :: "'a seq set"
mueller@3071
    27
   Partial       ::"'a seq => bool"
mueller@3071
    28
   Infinite      ::"'a seq => bool"
mueller@3071
    29
mueller@3071
    30
   nproj        :: "nat => 'a seq => 'a"
mueller@4282
    31
   sproj        :: "nat => 'a seq => 'a seq"
mueller@3071
    32
wenzelm@22808
    33
abbreviation
wenzelm@22808
    34
  sconc_syn :: "'a seq => 'a seq => 'a seq"  (infixr "@@" 65) where
wenzelm@22808
    35
  "xs @@ ys == sconc $ xs $ ys"
mueller@3071
    36
wenzelm@22808
    37
abbreviation
wenzelm@22808
    38
  Finite :: "'a seq => bool" where
wenzelm@22808
    39
  "Finite x == x:sfinite"
mueller@3071
    40
wenzelm@17233
    41
defs
mueller@3071
    42
mueller@3071
    43
(* f not possible at lhs, as "pattern matching" only for % x arguments,
mueller@3071
    44
   f cannot be written at rhs in front, as fix_eq3 does not apply later *)
wenzelm@17233
    45
smap_def:
wenzelm@17233
    46
  "smap == (fix$(LAM h f tr. case tr of
mueller@3071
    47
      nil   => nil
nipkow@10835
    48
    | x##xs => f$x ## h$f$xs))"
mueller@3071
    49
wenzelm@17233
    50
sfilter_def:
wenzelm@17233
    51
  "sfilter == (fix$(LAM h P t. case t of
wenzelm@17233
    52
           nil => nil
wenzelm@17233
    53
         | x##xs => If P$x
nipkow@10835
    54
                    then x##(h$P$xs)
nipkow@10835
    55
                    else     h$P$xs
wenzelm@17233
    56
                    fi))"
wenzelm@17233
    57
sforall_def:
wenzelm@17233
    58
  "sforall P t == (sforall2$P$t ~=FF)"
mueller@3071
    59
mueller@3071
    60
wenzelm@17233
    61
sforall2_def:
wenzelm@17233
    62
  "sforall2 == (fix$(LAM h P t. case t of
wenzelm@17233
    63
           nil => TT
wenzelm@17233
    64
         | x##xs => P$x andalso h$P$xs))"
wenzelm@17233
    65
wenzelm@17233
    66
sconc_def:
wenzelm@17233
    67
  "sconc == (fix$(LAM h t1 t2. case t1 of
mueller@3071
    68
               nil       => t2
nipkow@10835
    69
             | x##xs => x##(h$xs$t2)))"
mueller@3071
    70
wenzelm@17233
    71
slast_def:
wenzelm@17233
    72
  "slast == (fix$(LAM h t. case t of
wenzelm@17233
    73
           nil => UU
wenzelm@17233
    74
         | x##xs => (If is_nil$xs
mueller@3071
    75
                          then x
nipkow@10835
    76
                         else h$xs fi)))"
mueller@3071
    77
wenzelm@17233
    78
stakewhile_def:
wenzelm@17233
    79
  "stakewhile == (fix$(LAM h P t. case t of
wenzelm@17233
    80
           nil => nil
wenzelm@17233
    81
         | x##xs => If P$x
nipkow@10835
    82
                    then x##(h$P$xs)
mueller@3071
    83
                    else nil
wenzelm@17233
    84
                    fi))"
wenzelm@17233
    85
sdropwhile_def:
wenzelm@17233
    86
  "sdropwhile == (fix$(LAM h P t. case t of
wenzelm@17233
    87
           nil => nil
wenzelm@17233
    88
         | x##xs => If P$x
nipkow@10835
    89
                    then h$P$xs
mueller@3071
    90
                    else t
wenzelm@17233
    91
                    fi))"
wenzelm@17233
    92
sflat_def:
wenzelm@17233
    93
  "sflat == (fix$(LAM h t. case t of
wenzelm@17233
    94
           nil => nil
wenzelm@17233
    95
         | x##xs => x @@ (h$xs)))"
mueller@3071
    96
wenzelm@17233
    97
szip_def:
wenzelm@17233
    98
  "szip == (fix$(LAM h t1 t2. case t1 of
mueller@3071
    99
               nil   => nil
wenzelm@17233
   100
             | x##xs => (case t2 of
wenzelm@17233
   101
                          nil => UU
nipkow@10835
   102
                        | y##ys => <x,y>##(h$xs$ys))))"
mueller@3071
   103
wenzelm@17233
   104
Partial_def:
mueller@3071
   105
  "Partial x  == (seq_finite x) & ~(Finite x)"
mueller@3071
   106
wenzelm@17233
   107
Infinite_def:
mueller@3071
   108
  "Infinite x == ~(seq_finite x)"
mueller@3071
   109
mueller@3071
   110
wenzelm@17233
   111
inductive "sfinite"
wenzelm@17233
   112
   intros
wenzelm@17233
   113
    sfinite_0:  "nil:sfinite"
wenzelm@17233
   114
    sfinite_n:  "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite"
mueller@3071
   115
huffman@19550
   116
declare sfinite.intros [simp]
huffman@19550
   117
declare seq.rews [simp]
huffman@19550
   118
wenzelm@19804
   119
huffman@19550
   120
subsection {* recursive equations of operators *}
huffman@19550
   121
huffman@19550
   122
subsubsection {* smap *}
huffman@19550
   123
huffman@19550
   124
lemma smap_unfold:
huffman@19550
   125
  "smap = (LAM f tr. case tr of nil  => nil | x##xs => f$x ## smap$f$xs)"
huffman@19550
   126
by (subst fix_eq2 [OF smap_def], simp)
huffman@19550
   127
huffman@19550
   128
lemma smap_nil [simp]: "smap$f$nil=nil"
huffman@19550
   129
by (subst smap_unfold, simp)
huffman@19550
   130
huffman@19550
   131
lemma smap_UU [simp]: "smap$f$UU=UU"
huffman@19550
   132
by (subst smap_unfold, simp)
huffman@19550
   133
huffman@19550
   134
lemma smap_cons [simp]: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"
huffman@19550
   135
apply (rule trans)
huffman@19550
   136
apply (subst smap_unfold)
huffman@19550
   137
apply simp
huffman@19550
   138
apply (rule refl)
huffman@19550
   139
done
huffman@19550
   140
huffman@19550
   141
subsubsection {* sfilter *}
huffman@19550
   142
huffman@19550
   143
lemma sfilter_unfold:
huffman@19550
   144
  "sfilter = (LAM P tr. case tr of
huffman@19550
   145
           nil   => nil
huffman@19550
   146
         | x##xs => If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"
huffman@19550
   147
by (subst fix_eq2 [OF sfilter_def], simp)
huffman@19550
   148
huffman@19550
   149
lemma sfilter_nil [simp]: "sfilter$P$nil=nil"
huffman@19550
   150
by (subst sfilter_unfold, simp)
huffman@19550
   151
huffman@19550
   152
lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
huffman@19550
   153
by (subst sfilter_unfold, simp)
huffman@19550
   154
huffman@19550
   155
lemma sfilter_cons [simp]:
huffman@19550
   156
"x~=UU ==> sfilter$P$(x##xs)=
huffman@19550
   157
              (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"
huffman@19550
   158
apply (rule trans)
huffman@19550
   159
apply (subst sfilter_unfold)
huffman@19550
   160
apply simp
huffman@19550
   161
apply (rule refl)
huffman@19550
   162
done
huffman@19550
   163
huffman@19550
   164
subsubsection {* sforall2 *}
huffman@19550
   165
huffman@19550
   166
lemma sforall2_unfold:
huffman@19550
   167
   "sforall2 = (LAM P tr. case tr of
huffman@19550
   168
                           nil   => TT
huffman@19550
   169
                         | x##xs => (P$x andalso sforall2$P$xs))"
huffman@19550
   170
by (subst fix_eq2 [OF sforall2_def], simp)
huffman@19550
   171
huffman@19550
   172
lemma sforall2_nil [simp]: "sforall2$P$nil=TT"
huffman@19550
   173
by (subst sforall2_unfold, simp)
huffman@19550
   174
huffman@19550
   175
lemma sforall2_UU [simp]: "sforall2$P$UU=UU"
huffman@19550
   176
by (subst sforall2_unfold, simp)
huffman@19550
   177
huffman@19550
   178
lemma sforall2_cons [simp]:
huffman@19550
   179
"x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)"
huffman@19550
   180
apply (rule trans)
huffman@19550
   181
apply (subst sforall2_unfold)
huffman@19550
   182
apply simp
huffman@19550
   183
apply (rule refl)
huffman@19550
   184
done
huffman@19550
   185
huffman@19550
   186
huffman@19550
   187
subsubsection {* stakewhile *}
huffman@19550
   188
huffman@19550
   189
lemma stakewhile_unfold:
huffman@19550
   190
  "stakewhile = (LAM P tr. case tr of
huffman@19550
   191
     nil   => nil
huffman@19550
   192
   | x##xs => (If P$x then x##(stakewhile$P$xs) else nil fi))"
huffman@19550
   193
by (subst fix_eq2 [OF stakewhile_def], simp)
huffman@19550
   194
huffman@19550
   195
lemma stakewhile_nil [simp]: "stakewhile$P$nil=nil"
huffman@19550
   196
apply (subst stakewhile_unfold)
huffman@19550
   197
apply simp
huffman@19550
   198
done
huffman@19550
   199
huffman@19550
   200
lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
huffman@19550
   201
apply (subst stakewhile_unfold)
huffman@19550
   202
apply simp
huffman@19550
   203
done
huffman@19550
   204
huffman@19550
   205
lemma stakewhile_cons [simp]:
huffman@19550
   206
"x~=UU ==> stakewhile$P$(x##xs) =
huffman@19550
   207
              (If P$x then x##(stakewhile$P$xs) else nil fi)"
huffman@19550
   208
apply (rule trans)
huffman@19550
   209
apply (subst stakewhile_unfold)
huffman@19550
   210
apply simp
huffman@19550
   211
apply (rule refl)
huffman@19550
   212
done
huffman@19550
   213
huffman@19550
   214
subsubsection {* sdropwhile *}
huffman@19550
   215
huffman@19550
   216
lemma sdropwhile_unfold:
huffman@19550
   217
   "sdropwhile = (LAM P tr. case tr of
huffman@19550
   218
                           nil   => nil
huffman@19550
   219
                         | x##xs => (If P$x then sdropwhile$P$xs else tr fi))"
huffman@19550
   220
by (subst fix_eq2 [OF sdropwhile_def], simp)
huffman@19550
   221
huffman@19550
   222
lemma sdropwhile_nil [simp]: "sdropwhile$P$nil=nil"
huffman@19550
   223
apply (subst sdropwhile_unfold)
huffman@19550
   224
apply simp
huffman@19550
   225
done
huffman@19550
   226
huffman@19550
   227
lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
huffman@19550
   228
apply (subst sdropwhile_unfold)
huffman@19550
   229
apply simp
huffman@19550
   230
done
huffman@19550
   231
huffman@19550
   232
lemma sdropwhile_cons [simp]:
huffman@19550
   233
"x~=UU ==> sdropwhile$P$(x##xs) =
huffman@19550
   234
              (If P$x then sdropwhile$P$xs else x##xs fi)"
huffman@19550
   235
apply (rule trans)
huffman@19550
   236
apply (subst sdropwhile_unfold)
huffman@19550
   237
apply simp
huffman@19550
   238
apply (rule refl)
huffman@19550
   239
done
huffman@19550
   240
huffman@19550
   241
huffman@19550
   242
subsubsection {* slast *}
huffman@19550
   243
huffman@19550
   244
lemma slast_unfold:
huffman@19550
   245
   "slast = (LAM tr. case tr of
huffman@19550
   246
                           nil   => UU
huffman@19550
   247
                         | x##xs => (If is_nil$xs then x else slast$xs fi))"
huffman@19550
   248
by (subst fix_eq2 [OF slast_def], simp)
huffman@19550
   249
huffman@19550
   250
lemma slast_nil [simp]: "slast$nil=UU"
huffman@19550
   251
apply (subst slast_unfold)
huffman@19550
   252
apply simp
huffman@19550
   253
done
huffman@19550
   254
huffman@19550
   255
lemma slast_UU [simp]: "slast$UU=UU"
huffman@19550
   256
apply (subst slast_unfold)
huffman@19550
   257
apply simp
huffman@19550
   258
done
huffman@19550
   259
huffman@19550
   260
lemma slast_cons [simp]:
huffman@19550
   261
"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)"
huffman@19550
   262
apply (rule trans)
huffman@19550
   263
apply (subst slast_unfold)
huffman@19550
   264
apply simp
huffman@19550
   265
apply (rule refl)
huffman@19550
   266
done
huffman@19550
   267
huffman@19550
   268
huffman@19550
   269
subsubsection {* sconc *}
huffman@19550
   270
huffman@19550
   271
lemma sconc_unfold:
huffman@19550
   272
   "sconc = (LAM t1 t2. case t1 of
huffman@19550
   273
                           nil   => t2
huffman@19550
   274
                         | x##xs => x ## (xs @@ t2))"
huffman@19550
   275
by (subst fix_eq2 [OF sconc_def], simp)
huffman@19550
   276
huffman@19550
   277
lemma sconc_nil [simp]: "nil @@ y = y"
huffman@19550
   278
apply (subst sconc_unfold)
huffman@19550
   279
apply simp
huffman@19550
   280
done
huffman@19550
   281
huffman@19550
   282
lemma sconc_UU [simp]: "UU @@ y=UU"
huffman@19550
   283
apply (subst sconc_unfold)
huffman@19550
   284
apply simp
huffman@19550
   285
done
huffman@19550
   286
huffman@19550
   287
lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)"
huffman@19550
   288
apply (rule trans)
huffman@19550
   289
apply (subst sconc_unfold)
huffman@19550
   290
apply simp
huffman@19550
   291
apply (case_tac "x=UU")
huffman@19550
   292
apply simp_all
huffman@19550
   293
done
huffman@19550
   294
huffman@19550
   295
huffman@19550
   296
subsubsection {* sflat *}
huffman@19550
   297
huffman@19550
   298
lemma sflat_unfold:
huffman@19550
   299
   "sflat = (LAM tr. case tr of
huffman@19550
   300
                           nil   => nil
huffman@19550
   301
                         | x##xs => x @@ sflat$xs)"
huffman@19550
   302
by (subst fix_eq2 [OF sflat_def], simp)
huffman@19550
   303
huffman@19550
   304
lemma sflat_nil [simp]: "sflat$nil=nil"
huffman@19550
   305
apply (subst sflat_unfold)
huffman@19550
   306
apply simp
huffman@19550
   307
done
huffman@19550
   308
huffman@19550
   309
lemma sflat_UU [simp]: "sflat$UU=UU"
huffman@19550
   310
apply (subst sflat_unfold)
huffman@19550
   311
apply simp
huffman@19550
   312
done
huffman@19550
   313
huffman@19550
   314
lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)"
huffman@19550
   315
apply (rule trans)
huffman@19550
   316
apply (subst sflat_unfold)
huffman@19550
   317
apply simp
huffman@19550
   318
apply (case_tac "x=UU")
huffman@19550
   319
apply simp_all
huffman@19550
   320
done
huffman@19550
   321
huffman@19550
   322
huffman@19550
   323
subsubsection {* szip *}
huffman@19550
   324
huffman@19550
   325
lemma szip_unfold:
huffman@19550
   326
   "szip = (LAM t1 t2. case t1 of
huffman@19550
   327
                nil   => nil
huffman@19550
   328
              | x##xs => (case t2 of
huffman@19550
   329
                           nil => UU
huffman@19550
   330
                         | y##ys => <x,y>##(szip$xs$ys)))"
huffman@19550
   331
by (subst fix_eq2 [OF szip_def], simp)
huffman@19550
   332
huffman@19550
   333
lemma szip_nil [simp]: "szip$nil$y=nil"
huffman@19550
   334
apply (subst szip_unfold)
huffman@19550
   335
apply simp
huffman@19550
   336
done
huffman@19550
   337
huffman@19550
   338
lemma szip_UU1 [simp]: "szip$UU$y=UU"
huffman@19550
   339
apply (subst szip_unfold)
huffman@19550
   340
apply simp
huffman@19550
   341
done
huffman@19550
   342
huffman@19550
   343
lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU"
huffman@19550
   344
apply (subst szip_unfold)
huffman@19550
   345
apply simp
huffman@19550
   346
apply (rule_tac x="x" in seq.casedist)
huffman@19550
   347
apply simp_all
huffman@19550
   348
done
huffman@19550
   349
huffman@19550
   350
lemma szip_cons_nil [simp]: "x~=UU ==> szip$(x##xs)$nil=UU"
huffman@19550
   351
apply (rule trans)
huffman@19550
   352
apply (subst szip_unfold)
huffman@19550
   353
apply simp_all
huffman@19550
   354
done
huffman@19550
   355
huffman@19550
   356
lemma szip_cons [simp]:
huffman@19550
   357
"[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys"
huffman@19550
   358
apply (rule trans)
huffman@19550
   359
apply (subst szip_unfold)
huffman@19550
   360
apply simp_all
huffman@19550
   361
done
huffman@19550
   362
huffman@19550
   363
huffman@19550
   364
subsection "scons, nil"
huffman@19550
   365
huffman@19550
   366
lemma scons_inject_eq:
huffman@19550
   367
 "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)"
huffman@19550
   368
by (simp add: seq.injects)
huffman@19550
   369
huffman@19550
   370
lemma nil_less_is_nil: "nil<<x ==> nil=x"
huffman@19550
   371
apply (rule_tac x="x" in seq.casedist)
huffman@19550
   372
apply simp
huffman@19550
   373
apply simp
huffman@19550
   374
apply simp
huffman@19550
   375
done
huffman@19550
   376
huffman@19550
   377
subsection "sfilter, sforall, sconc"
huffman@19550
   378
huffman@19550
   379
lemma if_and_sconc [simp]: "(if b then tr1 else tr2) @@ tr
huffman@19550
   380
        = (if b then tr1 @@ tr else tr2 @@ tr)"
huffman@19550
   381
by simp
huffman@19550
   382
huffman@19550
   383
huffman@19550
   384
lemma sfiltersconc: "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)"
huffman@19550
   385
apply (rule_tac x="x" in seq.ind)
huffman@19550
   386
(* adm *)
huffman@19550
   387
apply simp
huffman@19550
   388
(* base cases *)
huffman@19550
   389
apply simp
huffman@19550
   390
apply simp
huffman@19550
   391
(* main case *)
huffman@19550
   392
apply (rule_tac p="P$a" in trE)
huffman@19550
   393
apply simp
huffman@19550
   394
apply simp
huffman@19550
   395
apply simp
huffman@19550
   396
done
huffman@19550
   397
huffman@19550
   398
lemma sforallPstakewhileP: "sforall P (stakewhile$P$x)"
huffman@19550
   399
apply (simp add: sforall_def)
huffman@19550
   400
apply (rule_tac x="x" in seq.ind)
huffman@19550
   401
(* adm *)
huffman@19550
   402
apply simp
huffman@19550
   403
(* base cases *)
huffman@19550
   404
apply simp
huffman@19550
   405
apply simp
huffman@19550
   406
(* main case *)
huffman@19550
   407
apply (rule_tac p="P$a" in trE)
huffman@19550
   408
apply simp
huffman@19550
   409
apply simp
huffman@19550
   410
apply simp
huffman@19550
   411
done
huffman@19550
   412
huffman@19550
   413
lemma forallPsfilterP: "sforall P (sfilter$P$x)"
huffman@19550
   414
apply (simp add: sforall_def)
huffman@19550
   415
apply (rule_tac x="x" in seq.ind)
huffman@19550
   416
(* adm *)
huffman@19550
   417
apply simp
huffman@19550
   418
(* base cases *)
huffman@19550
   419
apply simp
huffman@19550
   420
apply simp
huffman@19550
   421
(* main case *)
huffman@19550
   422
apply (rule_tac p="P$a" in trE)
huffman@19550
   423
apply simp
huffman@19550
   424
apply simp
huffman@19550
   425
apply simp
huffman@19550
   426
done
huffman@19550
   427
huffman@19550
   428
huffman@19550
   429
subsection "Finite"
huffman@19550
   430
huffman@19550
   431
(* ----------------------------------------------------  *)
huffman@19550
   432
(* Proofs of rewrite rules for Finite:                  *)
huffman@19550
   433
(* 1. Finite(nil),   (by definition)                    *)
huffman@19550
   434
(* 2. ~Finite(UU),                                      *)
huffman@19550
   435
(* 3. a~=UU==> Finite(a##x)=Finite(x)                  *)
huffman@19550
   436
(* ----------------------------------------------------  *)
huffman@19550
   437
huffman@19550
   438
lemma Finite_UU_a: "Finite x --> x~=UU"
huffman@19550
   439
apply (rule impI)
huffman@19550
   440
apply (erule sfinite.induct)
huffman@19550
   441
 apply simp
huffman@19550
   442
apply simp
huffman@19550
   443
done
huffman@19550
   444
huffman@19550
   445
lemma Finite_UU [simp]: "~(Finite UU)"
huffman@19550
   446
apply (cut_tac x="UU" in Finite_UU_a)
huffman@19550
   447
apply fast
huffman@19550
   448
done
huffman@19550
   449
huffman@19550
   450
lemma Finite_cons_a: "Finite x --> a~=UU --> x=a##xs --> Finite xs"
huffman@19550
   451
apply (intro strip)
huffman@19550
   452
apply (erule sfinite.elims)
huffman@19550
   453
apply fastsimp
huffman@19550
   454
apply (simp add: seq.injects)
huffman@19550
   455
done
huffman@19550
   456
huffman@19550
   457
lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)"
huffman@19550
   458
apply (rule iffI)
huffman@19550
   459
apply (erule (1) Finite_cons_a [rule_format])
huffman@19550
   460
apply fast
huffman@19550
   461
apply simp
huffman@19550
   462
done
huffman@19550
   463
huffman@19550
   464
huffman@19550
   465
subsection "induction"
huffman@19550
   466
huffman@19550
   467
huffman@19550
   468
(*--------------------------------   *)
huffman@19550
   469
(* Extensions to Induction Theorems  *)
huffman@19550
   470
(*--------------------------------   *)
huffman@19550
   471
huffman@19550
   472
huffman@19550
   473
lemma seq_finite_ind_lemma:
huffman@19550
   474
  assumes "(!!n. P(seq_take n$s))"
huffman@19550
   475
  shows "seq_finite(s) -->P(s)"
huffman@19550
   476
apply (unfold seq.finite_def)
huffman@19550
   477
apply (intro strip)
huffman@19550
   478
apply (erule exE)
huffman@19550
   479
apply (erule subst)
huffman@19550
   480
apply (rule prems)
huffman@19550
   481
done
huffman@19550
   482
huffman@19550
   483
huffman@19550
   484
lemma seq_finite_ind: "!!P.[|P(UU);P(nil);
huffman@19550
   485
   !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)
huffman@19550
   486
   |] ==> seq_finite(s) --> P(s)"
huffman@19550
   487
apply (rule seq_finite_ind_lemma)
huffman@19550
   488
apply (erule seq.finite_ind)
huffman@19550
   489
 apply assumption
huffman@19550
   490
apply simp
huffman@19550
   491
done
huffman@19550
   492
mueller@3071
   493
end