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