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