src/HOL/HOLCF/IOA/meta_theory/Seq.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 40329 src/HOLCF/IOA/meta_theory/Seq.thy@73f2b99b549d
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/Seq.thy
wenzelm@12218
     2
    Author:     Olaf Müller
wenzelm@17233
     3
*)
mueller@3071
     4
wenzelm@17233
     5
header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
mueller@3071
     6
wenzelm@17233
     7
theory Seq
wenzelm@17233
     8
imports HOLCF
wenzelm@17233
     9
begin
mueller@3071
    10
huffman@40329
    11
default_sort pcpo
huffman@40329
    12
huffman@40329
    13
domain (unsafe) 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
mueller@3071
    14
huffman@35286
    15
(*
wenzelm@17233
    16
   sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"
mueller@3071
    17
   smap          :: "('a -> 'b) -> 'a seq -> 'b seq"
mueller@3071
    18
   sforall       :: "('a -> tr) => 'a seq => bool"
mueller@3071
    19
   sforall2      :: "('a -> tr) -> 'a seq -> tr"
mueller@3071
    20
   slast         :: "'a seq     -> 'a"
mueller@3071
    21
   sconc         :: "'a seq     -> 'a seq -> 'a seq"
huffman@35286
    22
   sdropwhile    :: "('a -> tr)  -> 'a seq -> 'a seq"
huffman@35286
    23
   stakewhile    :: "('a -> tr)  -> 'a seq -> 'a seq"
huffman@35286
    24
   szip          :: "'a seq      -> 'b seq -> ('a*'b) seq"
mueller@3071
    25
   sflat        :: "('a seq) seq  -> 'a seq"
mueller@3071
    26
mueller@3071
    27
   sfinite       :: "'a seq set"
huffman@35286
    28
   Partial       :: "'a seq => bool"
huffman@35286
    29
   Infinite      :: "'a seq => bool"
mueller@3071
    30
mueller@3071
    31
   nproj        :: "nat => 'a seq => 'a"
mueller@4282
    32
   sproj        :: "nat => 'a seq => 'a seq"
huffman@35286
    33
*)
mueller@3071
    34
berghofe@23778
    35
inductive
berghofe@23778
    36
  Finite :: "'a seq => bool"
berghofe@23778
    37
  where
berghofe@23778
    38
    sfinite_0:  "Finite nil"
berghofe@23778
    39
  | sfinite_n:  "[| Finite tr; a~=UU |] ==> Finite (a##tr)"
mueller@3071
    40
huffman@35286
    41
declare Finite.intros [simp]
mueller@3071
    42
huffman@35286
    43
definition
huffman@35286
    44
  Partial :: "'a seq => bool"
huffman@35286
    45
where
mueller@3071
    46
  "Partial x  == (seq_finite x) & ~(Finite x)"
mueller@3071
    47
huffman@35286
    48
definition
huffman@35286
    49
  Infinite :: "'a seq => bool"
huffman@35286
    50
where
mueller@3071
    51
  "Infinite x == ~(seq_finite x)"
mueller@3071
    52
mueller@3071
    53
huffman@19550
    54
subsection {* recursive equations of operators *}
huffman@19550
    55
huffman@19550
    56
subsubsection {* smap *}
huffman@19550
    57
huffman@35286
    58
fixrec
huffman@35286
    59
  smap :: "('a -> 'b) -> 'a seq -> 'b seq"
huffman@35286
    60
where
huffman@35286
    61
  smap_nil: "smap$f$nil=nil"
huffman@35286
    62
| smap_cons: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"
huffman@19550
    63
huffman@19550
    64
lemma smap_UU [simp]: "smap$f$UU=UU"
huffman@35286
    65
by fixrec_simp
huffman@19550
    66
huffman@19550
    67
subsubsection {* sfilter *}
huffman@19550
    68
huffman@35286
    69
fixrec
huffman@35286
    70
   sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
huffman@35286
    71
where
huffman@35286
    72
  sfilter_nil: "sfilter$P$nil=nil"
huffman@35286
    73
| sfilter_cons:
huffman@35286
    74
    "x~=UU ==> sfilter$P$(x##xs)=
huffman@40322
    75
              (If P$x then x##(sfilter$P$xs) else sfilter$P$xs)"
huffman@19550
    76
huffman@19550
    77
lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
huffman@35286
    78
by fixrec_simp
huffman@19550
    79
huffman@19550
    80
subsubsection {* sforall2 *}
huffman@19550
    81
huffman@35286
    82
fixrec
huffman@35286
    83
  sforall2 :: "('a -> tr) -> 'a seq -> tr"
huffman@35286
    84
where
huffman@35286
    85
  sforall2_nil: "sforall2$P$nil=TT"
huffman@35286
    86
| sforall2_cons:
huffman@35286
    87
    "x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)"
huffman@19550
    88
huffman@19550
    89
lemma sforall2_UU [simp]: "sforall2$P$UU=UU"
huffman@35286
    90
by fixrec_simp
huffman@19550
    91
huffman@35286
    92
definition
huffman@35286
    93
  sforall_def: "sforall P t == (sforall2$P$t ~=FF)"
huffman@19550
    94
huffman@19550
    95
subsubsection {* stakewhile *}
huffman@19550
    96
huffman@35286
    97
fixrec
huffman@35286
    98
  stakewhile :: "('a -> tr)  -> 'a seq -> 'a seq"
huffman@35286
    99
where
huffman@35286
   100
  stakewhile_nil: "stakewhile$P$nil=nil"
huffman@35286
   101
| stakewhile_cons:
huffman@35286
   102
    "x~=UU ==> stakewhile$P$(x##xs) =
huffman@40322
   103
              (If P$x then x##(stakewhile$P$xs) else nil)"
huffman@19550
   104
huffman@19550
   105
lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
huffman@35286
   106
by fixrec_simp
huffman@19550
   107
huffman@19550
   108
subsubsection {* sdropwhile *}
huffman@19550
   109
huffman@35286
   110
fixrec
huffman@35286
   111
  sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq"
huffman@35286
   112
where
huffman@35286
   113
  sdropwhile_nil: "sdropwhile$P$nil=nil"
huffman@35286
   114
| sdropwhile_cons:
huffman@35286
   115
    "x~=UU ==> sdropwhile$P$(x##xs) =
huffman@40322
   116
              (If P$x then sdropwhile$P$xs else x##xs)"
huffman@19550
   117
huffman@19550
   118
lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
huffman@35286
   119
by fixrec_simp
huffman@19550
   120
huffman@19550
   121
subsubsection {* slast *}
huffman@19550
   122
huffman@35286
   123
fixrec
huffman@35286
   124
  slast :: "'a seq -> 'a"
huffman@35286
   125
where
huffman@35286
   126
  slast_nil: "slast$nil=UU"
huffman@35286
   127
| slast_cons:
huffman@40322
   128
    "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs)"
huffman@19550
   129
huffman@19550
   130
lemma slast_UU [simp]: "slast$UU=UU"
huffman@35286
   131
by fixrec_simp
huffman@19550
   132
huffman@19550
   133
subsubsection {* sconc *}
huffman@19550
   134
huffman@35286
   135
fixrec
huffman@35286
   136
  sconc :: "'a seq -> 'a seq -> 'a seq"
huffman@35286
   137
where
huffman@35286
   138
  sconc_nil: "sconc$nil$y = y"
huffman@35286
   139
| sconc_cons':
huffman@35286
   140
    "x~=UU ==> sconc$(x##xs)$y = x##(sconc$xs$y)"
huffman@19550
   141
huffman@35286
   142
abbreviation
huffman@35286
   143
  sconc_syn :: "'a seq => 'a seq => 'a seq"  (infixr "@@" 65) where
huffman@35286
   144
  "xs @@ ys == sconc $ xs $ ys"
huffman@19550
   145
huffman@19550
   146
lemma sconc_UU [simp]: "UU @@ y=UU"
huffman@35286
   147
by fixrec_simp
huffman@19550
   148
huffman@19550
   149
lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)"
huffman@35286
   150
apply (cases "x=UU")
huffman@19550
   151
apply simp_all
huffman@19550
   152
done
huffman@19550
   153
huffman@35286
   154
declare sconc_cons' [simp del]
huffman@19550
   155
huffman@19550
   156
subsubsection {* sflat *}
huffman@19550
   157
huffman@35286
   158
fixrec
huffman@35286
   159
  sflat :: "('a seq) seq -> 'a seq"
huffman@35286
   160
where
huffman@35286
   161
  sflat_nil: "sflat$nil=nil"
huffman@35286
   162
| sflat_cons': "x~=UU ==> sflat$(x##xs)= x@@(sflat$xs)"
huffman@19550
   163
huffman@19550
   164
lemma sflat_UU [simp]: "sflat$UU=UU"
huffman@35286
   165
by fixrec_simp
huffman@19550
   166
huffman@19550
   167
lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)"
huffman@35286
   168
by (cases "x=UU", simp_all)
huffman@19550
   169
huffman@35286
   170
declare sflat_cons' [simp del]
huffman@19550
   171
huffman@19550
   172
subsubsection {* szip *}
huffman@19550
   173
huffman@35286
   174
fixrec
huffman@35286
   175
  szip :: "'a seq -> 'b seq -> ('a*'b) seq"
huffman@35286
   176
where
huffman@35286
   177
  szip_nil: "szip$nil$y=nil"
huffman@35286
   178
| szip_cons_nil: "x~=UU ==> szip$(x##xs)$nil=UU"
huffman@35286
   179
| szip_cons:
huffman@35924
   180
    "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = (x,y)##szip$xs$ys"
huffman@19550
   181
huffman@19550
   182
lemma szip_UU1 [simp]: "szip$UU$y=UU"
huffman@35286
   183
by fixrec_simp
huffman@19550
   184
huffman@19550
   185
lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU"
huffman@35286
   186
by (cases x, simp_all, fixrec_simp)
huffman@19550
   187
huffman@19550
   188
huffman@19550
   189
subsection "scons, nil"
huffman@19550
   190
huffman@19550
   191
lemma scons_inject_eq:
huffman@19550
   192
 "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)"
huffman@35215
   193
by simp
huffman@19550
   194
huffman@19550
   195
lemma nil_less_is_nil: "nil<<x ==> nil=x"
huffman@35532
   196
apply (cases x)
huffman@19550
   197
apply simp
huffman@19550
   198
apply simp
huffman@19550
   199
apply simp
huffman@19550
   200
done
huffman@19550
   201
huffman@19550
   202
subsection "sfilter, sforall, sconc"
huffman@19550
   203
huffman@19550
   204
lemma if_and_sconc [simp]: "(if b then tr1 else tr2) @@ tr
huffman@19550
   205
        = (if b then tr1 @@ tr else tr2 @@ tr)"
huffman@19550
   206
by simp
huffman@19550
   207
huffman@19550
   208
huffman@19550
   209
lemma sfiltersconc: "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)"
huffman@35781
   210
apply (induct x)
huffman@19550
   211
(* adm *)
huffman@19550
   212
apply simp
huffman@19550
   213
(* base cases *)
huffman@19550
   214
apply simp
huffman@19550
   215
apply simp
huffman@19550
   216
(* main case *)
huffman@19550
   217
apply (rule_tac p="P$a" in trE)
huffman@19550
   218
apply simp
huffman@19550
   219
apply simp
huffman@19550
   220
apply simp
huffman@19550
   221
done
huffman@19550
   222
huffman@19550
   223
lemma sforallPstakewhileP: "sforall P (stakewhile$P$x)"
huffman@19550
   224
apply (simp add: sforall_def)
huffman@35781
   225
apply (induct x)
huffman@19550
   226
(* adm *)
huffman@19550
   227
apply simp
huffman@19550
   228
(* base cases *)
huffman@19550
   229
apply simp
huffman@19550
   230
apply simp
huffman@19550
   231
(* main case *)
huffman@19550
   232
apply (rule_tac p="P$a" in trE)
huffman@19550
   233
apply simp
huffman@19550
   234
apply simp
huffman@19550
   235
apply simp
huffman@19550
   236
done
huffman@19550
   237
huffman@19550
   238
lemma forallPsfilterP: "sforall P (sfilter$P$x)"
huffman@19550
   239
apply (simp add: sforall_def)
huffman@35781
   240
apply (induct x)
huffman@19550
   241
(* adm *)
huffman@19550
   242
apply simp
huffman@19550
   243
(* base cases *)
huffman@19550
   244
apply simp
huffman@19550
   245
apply simp
huffman@19550
   246
(* main case *)
huffman@19550
   247
apply (rule_tac p="P$a" in trE)
huffman@19550
   248
apply simp
huffman@19550
   249
apply simp
huffman@19550
   250
apply simp
huffman@19550
   251
done
huffman@19550
   252
huffman@19550
   253
huffman@19550
   254
subsection "Finite"
huffman@19550
   255
huffman@19550
   256
(* ----------------------------------------------------  *)
huffman@19550
   257
(* Proofs of rewrite rules for Finite:                  *)
huffman@19550
   258
(* 1. Finite(nil),   (by definition)                    *)
huffman@19550
   259
(* 2. ~Finite(UU),                                      *)
huffman@19550
   260
(* 3. a~=UU==> Finite(a##x)=Finite(x)                  *)
huffman@19550
   261
(* ----------------------------------------------------  *)
huffman@19550
   262
huffman@19550
   263
lemma Finite_UU_a: "Finite x --> x~=UU"
huffman@19550
   264
apply (rule impI)
berghofe@23778
   265
apply (erule Finite.induct)
huffman@19550
   266
 apply simp
huffman@19550
   267
apply simp
huffman@19550
   268
done
huffman@19550
   269
huffman@19550
   270
lemma Finite_UU [simp]: "~(Finite UU)"
huffman@19550
   271
apply (cut_tac x="UU" in Finite_UU_a)
huffman@19550
   272
apply fast
huffman@19550
   273
done
huffman@19550
   274
huffman@19550
   275
lemma Finite_cons_a: "Finite x --> a~=UU --> x=a##xs --> Finite xs"
huffman@19550
   276
apply (intro strip)
berghofe@23778
   277
apply (erule Finite.cases)
huffman@19550
   278
apply fastsimp
huffman@35215
   279
apply simp
huffman@19550
   280
done
huffman@19550
   281
huffman@19550
   282
lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)"
huffman@19550
   283
apply (rule iffI)
huffman@19550
   284
apply (erule (1) Finite_cons_a [rule_format])
huffman@19550
   285
apply fast
huffman@19550
   286
apply simp
huffman@19550
   287
done
huffman@19550
   288
huffman@25803
   289
lemma Finite_upward: "\<lbrakk>Finite x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> Finite y"
huffman@25803
   290
apply (induct arbitrary: y set: Finite)
huffman@35532
   291
apply (case_tac y, simp, simp, simp)
huffman@35532
   292
apply (case_tac y, simp, simp)
huffman@35215
   293
apply simp
huffman@25803
   294
done
huffman@25803
   295
huffman@25803
   296
lemma adm_Finite [simp]: "adm Finite"
huffman@25803
   297
by (rule adm_upward, rule Finite_upward)
huffman@25803
   298
huffman@19550
   299
huffman@19550
   300
subsection "induction"
huffman@19550
   301
huffman@19550
   302
huffman@19550
   303
(*--------------------------------   *)
huffman@19550
   304
(* Extensions to Induction Theorems  *)
huffman@19550
   305
(*--------------------------------   *)
huffman@19550
   306
huffman@19550
   307
huffman@19550
   308
lemma seq_finite_ind_lemma:
huffman@19550
   309
  assumes "(!!n. P(seq_take n$s))"
huffman@19550
   310
  shows "seq_finite(s) -->P(s)"
huffman@19550
   311
apply (unfold seq.finite_def)
huffman@19550
   312
apply (intro strip)
huffman@19550
   313
apply (erule exE)
huffman@19550
   314
apply (erule subst)
huffman@19550
   315
apply (rule prems)
huffman@19550
   316
done
huffman@19550
   317
huffman@19550
   318
huffman@19550
   319
lemma seq_finite_ind: "!!P.[|P(UU);P(nil);
huffman@19550
   320
   !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)
huffman@19550
   321
   |] ==> seq_finite(s) --> P(s)"
huffman@19550
   322
apply (rule seq_finite_ind_lemma)
huffman@35781
   323
apply (erule seq.finite_induct)
huffman@19550
   324
 apply assumption
huffman@19550
   325
apply simp
huffman@19550
   326
done
huffman@19550
   327
mueller@3071
   328
end