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