src/HOLCF/IOA/meta_theory/Sequence.thy
author wenzelm
Fri Mar 20 15:24:18 2009 +0100 (2009-03-20)
changeset 30607 c3d1590debd8
parent 27239 f2f42f9fa09d
child 30807 a167ed35ec0d
permissions -rw-r--r--
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
wenzelm@12218
     2
    Author:     Olaf Müller
mueller@3071
     3
wenzelm@12218
     4
Sequences over flat domains with lifted elements.
wenzelm@17233
     5
*)
mueller@3071
     6
wenzelm@17233
     7
theory Sequence
wenzelm@17233
     8
imports Seq
wenzelm@17233
     9
begin
mueller@3071
    10
wenzelm@17233
    11
defaultsort type
wenzelm@17233
    12
wenzelm@17233
    13
types 'a Seq = "'a::type lift seq"
mueller@3071
    14
wenzelm@3952
    15
consts
mueller@3071
    16
wenzelm@7229
    17
  Consq            ::"'a            => 'a Seq -> 'a Seq"
mueller@3071
    18
  Filter           ::"('a => bool)  => 'a Seq -> 'a Seq"
mueller@3071
    19
  Map              ::"('a => 'b)    => 'a Seq -> 'b Seq"
mueller@3071
    20
  Forall           ::"('a => bool)  => 'a Seq => bool"
mueller@3071
    21
  Last             ::"'a Seq        -> 'a lift"
wenzelm@17233
    22
  Dropwhile        ::"('a => bool)  => 'a Seq -> 'a Seq"
wenzelm@17233
    23
  Takewhile        ::"('a => bool)  => 'a Seq -> 'a Seq"
mueller@3071
    24
  Zip              ::"'a Seq        -> 'b Seq -> ('a * 'b) Seq"
mueller@3071
    25
  Flat             ::"('a Seq) seq   -> 'a Seq"
mueller@3071
    26
mueller@3071
    27
  Filter2          ::"('a => bool)  => 'a Seq -> 'a Seq"
mueller@3071
    28
wenzelm@25131
    29
abbreviation
wenzelm@25131
    30
  Consq_syn  ("(_/>>_)"  [66,65] 65) where
wenzelm@25131
    31
  "a>>s == Consq a$s"
mueller@3071
    32
wenzelm@25131
    33
notation (xsymbols)
wenzelm@25131
    34
  Consq_syn  ("(_\<leadsto>_)"  [66,65] 65)
mueller@4283
    35
mueller@3071
    36
wenzelm@25131
    37
(* list Enumeration *)
wenzelm@25131
    38
syntax
wenzelm@25131
    39
  "_totlist"      :: "args => 'a Seq"              ("[(_)!]")
wenzelm@25131
    40
  "_partlist"     :: "args => 'a Seq"              ("[(_)?]")
mueller@3071
    41
translations
mueller@4283
    42
  "[x, xs!]"     == "x>>[xs!]"
wenzelm@25131
    43
  "[x!]"         == "x>>CONST nil"
mueller@4283
    44
  "[x, xs?]"     == "x>>[xs?]"
wenzelm@25131
    45
  "[x?]"         == "x>>CONST UU"
mueller@3071
    46
mueller@3071
    47
defs
mueller@3071
    48
wenzelm@17233
    49
Consq_def:     "Consq a == LAM s. Def a ## s"
mueller@3071
    50
wenzelm@17233
    51
Filter_def:    "Filter P == sfilter$(flift2 P)"
mueller@3071
    52
wenzelm@17233
    53
Map_def:       "Map f  == smap$(flift2 f)"
mueller@3071
    54
wenzelm@17233
    55
Forall_def:    "Forall P == sforall (flift2 P)"
mueller@3071
    56
wenzelm@17233
    57
Last_def:      "Last == slast"
mueller@3071
    58
wenzelm@17233
    59
Dropwhile_def: "Dropwhile P == sdropwhile$(flift2 P)"
mueller@3071
    60
wenzelm@17233
    61
Takewhile_def: "Takewhile P == stakewhile$(flift2 P)"
mueller@3071
    62
wenzelm@17233
    63
Flat_def:      "Flat == sflat"
mueller@3071
    64
wenzelm@17233
    65
Zip_def:
wenzelm@17233
    66
  "Zip == (fix$(LAM h t1 t2. case t1 of
mueller@3071
    67
               nil   => nil
wenzelm@17233
    68
             | x##xs => (case t2 of
wenzelm@17233
    69
                          nil => UU
wenzelm@17233
    70
                        | y##ys => (case x of
wenzelm@12028
    71
                                      UU  => UU
wenzelm@17233
    72
                                    | Def a => (case y of
wenzelm@12028
    73
                                                  UU => UU
nipkow@10835
    74
                                                | Def b => Def (a,b)##(h$xs$ys))))))"
mueller@3071
    75
wenzelm@17233
    76
Filter2_def:    "Filter2 P == (fix$(LAM h t. case t of
mueller@3071
    77
            nil => nil
wenzelm@17233
    78
          | x##xs => (case x of UU => UU | Def y => (if P y
nipkow@10835
    79
                     then x##(h$xs)
wenzelm@17233
    80
                     else     h$xs))))"
mueller@3071
    81
huffman@19551
    82
declare andalso_and [simp]
huffman@19551
    83
declare andalso_or [simp]
huffman@19551
    84
huffman@19551
    85
subsection "recursive equations of operators"
huffman@19551
    86
huffman@19551
    87
subsubsection "Map"
huffman@19551
    88
huffman@19551
    89
lemma Map_UU: "Map f$UU =UU"
huffman@19551
    90
by (simp add: Map_def)
huffman@19551
    91
huffman@19551
    92
lemma Map_nil: "Map f$nil =nil"
huffman@19551
    93
by (simp add: Map_def)
huffman@19551
    94
huffman@19551
    95
lemma Map_cons: "Map f$(x>>xs)=(f x) >> Map f$xs"
huffman@19551
    96
by (simp add: Map_def Consq_def flift2_def)
huffman@19551
    97
huffman@19551
    98
huffman@19551
    99
subsubsection {* Filter *}
huffman@19551
   100
huffman@19551
   101
lemma Filter_UU: "Filter P$UU =UU"
huffman@19551
   102
by (simp add: Filter_def)
huffman@19551
   103
huffman@19551
   104
lemma Filter_nil: "Filter P$nil =nil"
huffman@19551
   105
by (simp add: Filter_def)
huffman@19551
   106
huffman@19551
   107
lemma Filter_cons:
huffman@19551
   108
  "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)"
huffman@19551
   109
by (simp add: Filter_def Consq_def flift2_def If_and_if)
huffman@19551
   110
huffman@19551
   111
huffman@19551
   112
subsubsection {* Forall *}
huffman@19551
   113
huffman@19551
   114
lemma Forall_UU: "Forall P UU"
huffman@19551
   115
by (simp add: Forall_def sforall_def)
huffman@19551
   116
huffman@19551
   117
lemma Forall_nil: "Forall P nil"
huffman@19551
   118
by (simp add: Forall_def sforall_def)
huffman@19551
   119
huffman@19551
   120
lemma Forall_cons: "Forall P (x>>xs)= (P x & Forall P xs)"
huffman@19551
   121
by (simp add: Forall_def sforall_def Consq_def flift2_def)
huffman@19551
   122
huffman@19551
   123
huffman@19551
   124
subsubsection {* Conc *}
huffman@19551
   125
huffman@19551
   126
lemma Conc_cons: "(x>>xs) @@ y = x>>(xs @@y)"
huffman@19551
   127
by (simp add: Consq_def)
huffman@19551
   128
huffman@19551
   129
huffman@19551
   130
subsubsection {* Takewhile *}
huffman@19551
   131
huffman@19551
   132
lemma Takewhile_UU: "Takewhile P$UU =UU"
huffman@19551
   133
by (simp add: Takewhile_def)
huffman@19551
   134
huffman@19551
   135
lemma Takewhile_nil: "Takewhile P$nil =nil"
huffman@19551
   136
by (simp add: Takewhile_def)
huffman@19551
   137
huffman@19551
   138
lemma Takewhile_cons:
huffman@19551
   139
  "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)"
huffman@19551
   140
by (simp add: Takewhile_def Consq_def flift2_def If_and_if)
huffman@19551
   141
huffman@19551
   142
huffman@19551
   143
subsubsection {* DropWhile *}
huffman@19551
   144
huffman@19551
   145
lemma Dropwhile_UU: "Dropwhile P$UU =UU"
huffman@19551
   146
by (simp add: Dropwhile_def)
huffman@19551
   147
huffman@19551
   148
lemma Dropwhile_nil: "Dropwhile P$nil =nil"
huffman@19551
   149
by (simp add: Dropwhile_def)
huffman@19551
   150
huffman@19551
   151
lemma Dropwhile_cons:
huffman@19551
   152
  "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)"
huffman@19551
   153
by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)
huffman@19551
   154
huffman@19551
   155
huffman@19551
   156
subsubsection {* Last *}
huffman@19551
   157
huffman@19551
   158
lemma Last_UU: "Last$UU =UU"
huffman@19551
   159
by (simp add: Last_def)
huffman@19551
   160
huffman@19551
   161
lemma Last_nil: "Last$nil =UU"
huffman@19551
   162
by (simp add: Last_def)
huffman@19551
   163
huffman@19551
   164
lemma Last_cons: "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"
huffman@19551
   165
apply (simp add: Last_def Consq_def)
huffman@19551
   166
apply (rule_tac x="xs" in seq.casedist)
huffman@19551
   167
apply simp
huffman@19551
   168
apply simp_all
huffman@19551
   169
done
huffman@19551
   170
huffman@19551
   171
huffman@19551
   172
subsubsection {* Flat *}
huffman@19551
   173
huffman@19551
   174
lemma Flat_UU: "Flat$UU =UU"
huffman@19551
   175
by (simp add: Flat_def)
huffman@19551
   176
huffman@19551
   177
lemma Flat_nil: "Flat$nil =nil"
huffman@19551
   178
by (simp add: Flat_def)
huffman@19551
   179
huffman@19551
   180
lemma Flat_cons: "Flat$(x##xs)= x @@ (Flat$xs)"
huffman@19551
   181
by (simp add: Flat_def Consq_def)
huffman@19551
   182
huffman@19551
   183
huffman@19551
   184
subsubsection {* Zip *}
huffman@19551
   185
huffman@19551
   186
lemma Zip_unfold:
huffman@19551
   187
"Zip = (LAM t1 t2. case t1 of
huffman@19551
   188
                nil   => nil
huffman@19551
   189
              | x##xs => (case t2 of
huffman@19551
   190
                           nil => UU
huffman@19551
   191
                         | y##ys => (case x of
huffman@19551
   192
                                       UU  => UU
huffman@19551
   193
                                     | Def a => (case y of
huffman@19551
   194
                                                   UU => UU
huffman@19551
   195
                                                 | Def b => Def (a,b)##(Zip$xs$ys)))))"
huffman@19551
   196
apply (rule trans)
huffman@19551
   197
apply (rule fix_eq2)
huffman@19551
   198
apply (rule Zip_def)
huffman@19551
   199
apply (rule beta_cfun)
huffman@19551
   200
apply simp
huffman@19551
   201
done
huffman@19551
   202
huffman@19551
   203
lemma Zip_UU1: "Zip$UU$y =UU"
huffman@19551
   204
apply (subst Zip_unfold)
huffman@19551
   205
apply simp
huffman@19551
   206
done
huffman@19551
   207
huffman@19551
   208
lemma Zip_UU2: "x~=nil ==> Zip$x$UU =UU"
huffman@19551
   209
apply (subst Zip_unfold)
huffman@19551
   210
apply simp
huffman@19551
   211
apply (rule_tac x="x" in seq.casedist)
huffman@19551
   212
apply simp_all
huffman@19551
   213
done
huffman@19551
   214
huffman@19551
   215
lemma Zip_nil: "Zip$nil$y =nil"
huffman@19551
   216
apply (subst Zip_unfold)
huffman@19551
   217
apply simp
huffman@19551
   218
done
huffman@19551
   219
huffman@19551
   220
lemma Zip_cons_nil: "Zip$(x>>xs)$nil= UU"
huffman@19551
   221
apply (subst Zip_unfold)
huffman@19551
   222
apply (simp add: Consq_def)
huffman@19551
   223
done
huffman@19551
   224
huffman@19551
   225
lemma Zip_cons: "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys"
huffman@19551
   226
apply (rule trans)
huffman@19551
   227
apply (subst Zip_unfold)
huffman@19551
   228
apply simp
huffman@19551
   229
apply (simp add: Consq_def)
huffman@19551
   230
done
huffman@19551
   231
huffman@19551
   232
lemmas [simp del] =
huffman@19551
   233
  sfilter_UU sfilter_nil sfilter_cons
huffman@19551
   234
  smap_UU smap_nil smap_cons
huffman@19551
   235
  sforall2_UU sforall2_nil sforall2_cons
huffman@19551
   236
  slast_UU slast_nil slast_cons
huffman@19551
   237
  stakewhile_UU  stakewhile_nil  stakewhile_cons
huffman@19551
   238
  sdropwhile_UU  sdropwhile_nil  sdropwhile_cons
huffman@19551
   239
  sflat_UU sflat_nil sflat_cons
huffman@19551
   240
  szip_UU1 szip_UU2 szip_nil szip_cons_nil szip_cons
huffman@19551
   241
huffman@19551
   242
lemmas [simp] =
huffman@19551
   243
  Filter_UU Filter_nil Filter_cons
huffman@19551
   244
  Map_UU Map_nil Map_cons
huffman@19551
   245
  Forall_UU Forall_nil Forall_cons
huffman@19551
   246
  Last_UU Last_nil Last_cons
huffman@19551
   247
  Conc_cons
huffman@19551
   248
  Takewhile_UU Takewhile_nil Takewhile_cons
huffman@19551
   249
  Dropwhile_UU Dropwhile_nil Dropwhile_cons
huffman@19551
   250
  Zip_UU1 Zip_UU2 Zip_nil Zip_cons_nil Zip_cons
huffman@19551
   251
huffman@19551
   252
huffman@19551
   253
huffman@19551
   254
section "Cons"
huffman@19551
   255
huffman@19551
   256
lemma Consq_def2: "a>>s = (Def a)##s"
huffman@19551
   257
apply (simp add: Consq_def)
huffman@19551
   258
done
huffman@19551
   259
huffman@19551
   260
lemma Seq_exhaust: "x = UU | x = nil | (? a s. x = a >> s)"
huffman@19551
   261
apply (simp add: Consq_def2)
huffman@19551
   262
apply (cut_tac seq.exhaust)
huffman@19551
   263
apply (fast dest: not_Undef_is_Def [THEN iffD1])
huffman@19551
   264
done
huffman@19551
   265
huffman@19551
   266
huffman@19551
   267
lemma Seq_cases:
huffman@19551
   268
"!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s  ==> P |] ==> P"
huffman@19551
   269
apply (cut_tac x="x" in Seq_exhaust)
huffman@19551
   270
apply (erule disjE)
huffman@19551
   271
apply simp
huffman@19551
   272
apply (erule disjE)
huffman@19551
   273
apply simp
huffman@19551
   274
apply (erule exE)+
huffman@19551
   275
apply simp
huffman@19551
   276
done
huffman@19551
   277
huffman@19551
   278
(*
huffman@19551
   279
fun Seq_case_tac s i = rule_tac x",s)] Seq_cases i
huffman@19551
   280
          THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
huffman@19551
   281
*)
huffman@19551
   282
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
huffman@19551
   283
(*
huffman@19551
   284
fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2)
huffman@19551
   285
                                             THEN Asm_full_simp_tac (i+1)
huffman@19551
   286
                                             THEN Asm_full_simp_tac i;
huffman@19551
   287
*)
huffman@19551
   288
huffman@19551
   289
lemma Cons_not_UU: "a>>s ~= UU"
huffman@19551
   290
apply (subst Consq_def2)
huffman@19551
   291
apply (rule seq.con_rews)
huffman@19551
   292
apply (rule Def_not_UU)
huffman@19551
   293
done
huffman@19551
   294
huffman@19551
   295
huffman@19551
   296
lemma Cons_not_less_UU: "~(a>>x) << UU"
huffman@19551
   297
apply (rule notI)
huffman@19551
   298
apply (drule antisym_less)
huffman@19551
   299
apply simp
huffman@19551
   300
apply (simp add: Cons_not_UU)
huffman@19551
   301
done
huffman@19551
   302
huffman@19551
   303
lemma Cons_not_less_nil: "~a>>s << nil"
huffman@19551
   304
apply (subst Consq_def2)
huffman@19551
   305
apply (rule seq.rews)
huffman@19551
   306
apply (rule Def_not_UU)
huffman@19551
   307
done
huffman@19551
   308
huffman@19551
   309
lemma Cons_not_nil: "a>>s ~= nil"
huffman@19551
   310
apply (subst Consq_def2)
huffman@19551
   311
apply (rule seq.rews)
huffman@19551
   312
done
huffman@19551
   313
huffman@19551
   314
lemma Cons_not_nil2: "nil ~= a>>s"
huffman@19551
   315
apply (simp add: Consq_def2)
huffman@19551
   316
done
huffman@19551
   317
huffman@19551
   318
lemma Cons_inject_eq: "(a>>s = b>>t) = (a = b & s = t)"
huffman@19551
   319
apply (simp only: Consq_def2)
huffman@19551
   320
apply (simp add: scons_inject_eq)
huffman@19551
   321
done
huffman@19551
   322
huffman@19551
   323
lemma Cons_inject_less_eq: "(a>>s<<b>>t) = (a = b & s<<t)"
huffman@19551
   324
apply (simp add: Consq_def2)
huffman@19551
   325
apply (simp add: seq.inverts)
huffman@19551
   326
done
huffman@19551
   327
huffman@19551
   328
lemma seq_take_Cons: "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)"
huffman@19551
   329
apply (simp add: Consq_def)
huffman@19551
   330
done
huffman@19551
   331
huffman@19551
   332
lemmas [simp] =
huffman@19551
   333
  Cons_not_nil2 Cons_inject_eq Cons_inject_less_eq seq_take_Cons
huffman@19551
   334
  Cons_not_UU Cons_not_less_UU Cons_not_less_nil Cons_not_nil
huffman@19551
   335
huffman@19551
   336
huffman@19551
   337
subsection "induction"
huffman@19551
   338
huffman@19551
   339
lemma Seq_induct:
huffman@19551
   340
"!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x"
huffman@19551
   341
apply (erule (2) seq.ind)
wenzelm@30607
   342
apply defined
huffman@19551
   343
apply (simp add: Consq_def)
huffman@19551
   344
done
huffman@19551
   345
huffman@19551
   346
lemma Seq_FinitePartial_ind:
huffman@19551
   347
"!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]
huffman@19551
   348
                ==> seq_finite x --> P x"
huffman@19551
   349
apply (erule (1) seq_finite_ind)
wenzelm@30607
   350
apply defined
huffman@19551
   351
apply (simp add: Consq_def)
huffman@19551
   352
done
huffman@19551
   353
huffman@19551
   354
lemma Seq_Finite_ind:
huffman@19551
   355
"!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x"
berghofe@23778
   356
apply (erule (1) Finite.induct)
wenzelm@30607
   357
apply defined
huffman@19551
   358
apply (simp add: Consq_def)
huffman@19551
   359
done
huffman@19551
   360
huffman@19551
   361
huffman@19551
   362
(* rws are definitions to be unfolded for admissibility check *)
huffman@19551
   363
(*
huffman@19551
   364
fun Seq_induct_tac s rws i = rule_tac x",s)] Seq_induct i
huffman@19551
   365
                         THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
huffman@19551
   366
                         THEN simp add: rws) i;
huffman@19551
   367
huffman@19551
   368
fun Seq_Finite_induct_tac i = erule Seq_Finite_ind i
huffman@19551
   369
                              THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
huffman@19551
   370
huffman@19551
   371
fun pair_tac s = rule_tac p",s)] PairE
huffman@19551
   372
                          THEN' hyp_subst_tac THEN' Simp_tac;
huffman@19551
   373
*)
huffman@19551
   374
(* induction on a sequence of pairs with pairsplitting and simplification *)
huffman@19551
   375
(*
huffman@19551
   376
fun pair_induct_tac s rws i =
huffman@19551
   377
           rule_tac x",s)] Seq_induct i
huffman@19551
   378
           THEN pair_tac "a" (i+3)
huffman@19551
   379
           THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1))))
huffman@19551
   380
           THEN simp add: rws) i;
huffman@19551
   381
*)
huffman@19551
   382
huffman@19551
   383
huffman@19551
   384
(* ------------------------------------------------------------------------------------ *)
huffman@19551
   385
huffman@19551
   386
subsection "HD,TL"
huffman@19551
   387
huffman@19551
   388
lemma HD_Cons [simp]: "HD$(x>>y) = Def x"
huffman@19551
   389
apply (simp add: Consq_def)
huffman@19551
   390
done
huffman@19551
   391
huffman@19551
   392
lemma TL_Cons [simp]: "TL$(x>>y) = y"
huffman@19551
   393
apply (simp add: Consq_def)
huffman@19551
   394
done
huffman@19551
   395
huffman@19551
   396
(* ------------------------------------------------------------------------------------ *)
huffman@19551
   397
huffman@19551
   398
subsection "Finite, Partial, Infinite"
huffman@19551
   399
huffman@19551
   400
lemma Finite_Cons [simp]: "Finite (a>>xs) = Finite xs"
huffman@19551
   401
apply (simp add: Consq_def2 Finite_cons)
huffman@19551
   402
done
huffman@19551
   403
huffman@19551
   404
lemma FiniteConc_1: "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)"
huffman@19551
   405
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
   406
done
huffman@19551
   407
huffman@19551
   408
lemma FiniteConc_2:
huffman@19551
   409
"Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)"
huffman@19551
   410
apply (erule Seq_Finite_ind)
huffman@19551
   411
(* nil*)
huffman@19551
   412
apply (intro strip)
huffman@19551
   413
apply (rule_tac x="x" in Seq_cases, simp_all)
huffman@19551
   414
(* cons *)
huffman@19551
   415
apply (intro strip)
huffman@19551
   416
apply (rule_tac x="x" in Seq_cases, simp_all)
huffman@19551
   417
apply (rule_tac x="y" in Seq_cases, simp_all)
huffman@19551
   418
done
huffman@19551
   419
huffman@19551
   420
lemma FiniteConc [simp]: "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)"
huffman@19551
   421
apply (rule iffI)
huffman@19551
   422
apply (erule FiniteConc_2 [rule_format])
huffman@19551
   423
apply (rule refl)
huffman@19551
   424
apply (rule FiniteConc_1 [rule_format])
huffman@19551
   425
apply auto
huffman@19551
   426
done
huffman@19551
   427
huffman@19551
   428
huffman@19551
   429
lemma FiniteMap1: "Finite s ==> Finite (Map f$s)"
huffman@19551
   430
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
   431
done
huffman@19551
   432
huffman@19551
   433
lemma FiniteMap2: "Finite s ==> ! t. (s = Map f$t) --> Finite t"
huffman@19551
   434
apply (erule Seq_Finite_ind)
huffman@19551
   435
apply (intro strip)
huffman@19551
   436
apply (rule_tac x="t" in Seq_cases, simp_all)
huffman@19551
   437
(* main case *)
huffman@19551
   438
apply auto
huffman@19551
   439
apply (rule_tac x="t" in Seq_cases, simp_all)
huffman@19551
   440
done
huffman@19551
   441
huffman@19551
   442
lemma Map2Finite: "Finite (Map f$s) = Finite s"
huffman@19551
   443
apply auto
huffman@19551
   444
apply (erule FiniteMap2 [rule_format])
huffman@19551
   445
apply (rule refl)
huffman@19551
   446
apply (erule FiniteMap1)
huffman@19551
   447
done
huffman@19551
   448
huffman@19551
   449
huffman@19551
   450
lemma FiniteFilter: "Finite s ==> Finite (Filter P$s)"
huffman@19551
   451
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
   452
done
huffman@19551
   453
huffman@19551
   454
huffman@19551
   455
(* ----------------------------------------------------------------------------------- *)
huffman@19551
   456
huffman@19551
   457
subsection "Conc"
huffman@19551
   458
huffman@19551
   459
lemma Conc_cong: "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)"
huffman@19551
   460
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
   461
done
huffman@19551
   462
huffman@19551
   463
lemma Conc_assoc: "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z"
huffman@19551
   464
apply (rule_tac x="x" in Seq_induct, simp_all)
huffman@19551
   465
done
huffman@19551
   466
huffman@19551
   467
lemma nilConc [simp]: "s@@ nil = s"
huffman@19551
   468
apply (rule_tac x="s" in seq.ind)
huffman@19551
   469
apply simp
huffman@19551
   470
apply simp
huffman@19551
   471
apply simp
huffman@19551
   472
apply simp
huffman@19551
   473
done
huffman@19551
   474
huffman@19551
   475
huffman@19551
   476
(* should be same as nil_is_Conc2 when all nils are turned to right side !! *)
huffman@19551
   477
lemma nil_is_Conc: "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)"
huffman@19551
   478
apply (rule_tac x="x" in Seq_cases)
huffman@19551
   479
apply auto
huffman@19551
   480
done
huffman@19551
   481
huffman@19551
   482
lemma nil_is_Conc2: "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)"
huffman@19551
   483
apply (rule_tac x="x" in Seq_cases)
huffman@19551
   484
apply auto
huffman@19551
   485
done
huffman@19551
   486
huffman@19551
   487
huffman@19551
   488
(* ------------------------------------------------------------------------------------ *)
huffman@19551
   489
huffman@19551
   490
subsection "Last"
huffman@19551
   491
huffman@19551
   492
lemma Finite_Last1: "Finite s ==> s~=nil --> Last$s~=UU"
huffman@19551
   493
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
   494
done
huffman@19551
   495
huffman@19551
   496
lemma Finite_Last2: "Finite s ==> Last$s=UU --> s=nil"
huffman@19551
   497
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
   498
apply fast
huffman@19551
   499
done
huffman@19551
   500
huffman@19551
   501
huffman@19551
   502
(* ------------------------------------------------------------------------------------ *)
huffman@19551
   503
huffman@19551
   504
huffman@19551
   505
subsection "Filter, Conc"
huffman@19551
   506
huffman@19551
   507
huffman@19551
   508
lemma FilterPQ: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
huffman@19551
   509
apply (rule_tac x="s" in Seq_induct, simp_all)
huffman@19551
   510
done
huffman@19551
   511
huffman@19551
   512
lemma FilterConc: "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)"
huffman@19551
   513
apply (simp add: Filter_def sfiltersconc)
huffman@19551
   514
done
huffman@19551
   515
huffman@19551
   516
(* ------------------------------------------------------------------------------------ *)
huffman@19551
   517
huffman@19551
   518
subsection "Map"
huffman@19551
   519
huffman@19551
   520
lemma MapMap: "Map f$(Map g$s) = Map (f o g)$s"
huffman@19551
   521
apply (rule_tac x="s" in Seq_induct, simp_all)
huffman@19551
   522
done
huffman@19551
   523
huffman@19551
   524
lemma MapConc: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
huffman@19551
   525
apply (rule_tac x="x" in Seq_induct, simp_all)
huffman@19551
   526
done
huffman@19551
   527
huffman@19551
   528
lemma MapFilter: "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)"
huffman@19551
   529
apply (rule_tac x="x" in Seq_induct, simp_all)
huffman@19551
   530
done
huffman@19551
   531
huffman@19551
   532
lemma nilMap: "nil = (Map f$s) --> s= nil"
huffman@19551
   533
apply (rule_tac x="s" in Seq_cases, simp_all)
huffman@19551
   534
done
huffman@19551
   535
huffman@19551
   536
huffman@19551
   537
lemma ForallMap: "Forall P (Map f$s) = Forall (P o f) s"
huffman@19551
   538
apply (rule_tac x="s" in Seq_induct)
huffman@19551
   539
apply (simp add: Forall_def sforall_def)
huffman@19551
   540
apply simp_all
huffman@19551
   541
done
huffman@19551
   542
huffman@19551
   543
huffman@19551
   544
huffman@19551
   545
huffman@19551
   546
(* ------------------------------------------------------------------------------------ *)
huffman@19551
   547
huffman@19551
   548
subsection "Forall"
huffman@19551
   549
huffman@19551
   550
wenzelm@26008
   551
lemma ForallPForallQ1: "Forall P ys & (! x. P x --> Q x)
wenzelm@26008
   552
         --> Forall Q ys"
huffman@19551
   553
apply (rule_tac x="ys" in Seq_induct)
huffman@19551
   554
apply (simp add: Forall_def sforall_def)
huffman@19551
   555
apply simp_all
huffman@19551
   556
done
huffman@19551
   557
huffman@19551
   558
lemmas ForallPForallQ =
huffman@19551
   559
  ForallPForallQ1 [THEN mp, OF conjI, OF _ allI, OF _ impI]
huffman@19551
   560
huffman@19551
   561
lemma Forall_Conc_impl: "(Forall P x & Forall P y) --> Forall P (x @@ y)"
huffman@19551
   562
apply (rule_tac x="x" in Seq_induct)
huffman@19551
   563
apply (simp add: Forall_def sforall_def)
huffman@19551
   564
apply simp_all
huffman@19551
   565
done
huffman@19551
   566
huffman@19551
   567
lemma Forall_Conc [simp]:
huffman@19551
   568
  "Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)"
huffman@19551
   569
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
   570
done
huffman@19551
   571
huffman@19551
   572
lemma ForallTL1: "Forall P s  --> Forall P (TL$s)"
huffman@19551
   573
apply (rule_tac x="s" in Seq_induct)
huffman@19551
   574
apply (simp add: Forall_def sforall_def)
huffman@19551
   575
apply simp_all
huffman@19551
   576
done
huffman@19551
   577
huffman@19551
   578
lemmas ForallTL = ForallTL1 [THEN mp]
huffman@19551
   579
huffman@19551
   580
lemma ForallDropwhile1: "Forall P s  --> Forall P (Dropwhile Q$s)"
huffman@19551
   581
apply (rule_tac x="s" in Seq_induct)
huffman@19551
   582
apply (simp add: Forall_def sforall_def)
huffman@19551
   583
apply simp_all
huffman@19551
   584
done
huffman@19551
   585
huffman@19551
   586
lemmas ForallDropwhile = ForallDropwhile1 [THEN mp]
huffman@19551
   587
huffman@19551
   588
huffman@19551
   589
(* only admissible in t, not if done in s *)
huffman@19551
   590
huffman@19551
   591
lemma Forall_prefix: "! s. Forall P s --> t<<s --> Forall P t"
huffman@19551
   592
apply (rule_tac x="t" in Seq_induct)
huffman@19551
   593
apply (simp add: Forall_def sforall_def)
huffman@19551
   594
apply simp_all
huffman@19551
   595
apply (intro strip)
huffman@19551
   596
apply (rule_tac x="sa" in Seq_cases)
huffman@19551
   597
apply simp
huffman@19551
   598
apply auto
huffman@19551
   599
done
huffman@19551
   600
huffman@19551
   601
lemmas Forall_prefixclosed = Forall_prefix [rule_format]
huffman@19551
   602
huffman@19551
   603
lemma Forall_postfixclosed:
huffman@19551
   604
  "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t"
huffman@19551
   605
apply auto
huffman@19551
   606
done
huffman@19551
   607
huffman@19551
   608
huffman@19551
   609
lemma ForallPFilterQR1:
huffman@19551
   610
  "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr"
huffman@19551
   611
apply (rule_tac x="tr" in Seq_induct)
huffman@19551
   612
apply (simp add: Forall_def sforall_def)
huffman@19551
   613
apply simp_all
huffman@19551
   614
done
huffman@19551
   615
huffman@19551
   616
lemmas ForallPFilterQR = ForallPFilterQR1 [THEN mp, OF conjI, OF allI]
huffman@19551
   617
huffman@19551
   618
huffman@19551
   619
(* ------------------------------------------------------------------------------------- *)
huffman@19551
   620
huffman@19551
   621
subsection "Forall, Filter"
huffman@19551
   622
huffman@19551
   623
huffman@19551
   624
lemma ForallPFilterP: "Forall P (Filter P$x)"
huffman@19551
   625
apply (simp add: Filter_def Forall_def forallPsfilterP)
huffman@19551
   626
done
huffman@19551
   627
huffman@19551
   628
(* holds also in other direction, then equal to forallPfilterP *)
huffman@19551
   629
lemma ForallPFilterPid1: "Forall P x --> Filter P$x = x"
huffman@19551
   630
apply (rule_tac x="x" in Seq_induct)
huffman@19551
   631
apply (simp add: Forall_def sforall_def Filter_def)
huffman@19551
   632
apply simp_all
huffman@19551
   633
done
huffman@19551
   634
huffman@19551
   635
lemmas ForallPFilterPid = ForallPFilterPid1 [THEN mp]
huffman@19551
   636
huffman@19551
   637
huffman@19551
   638
(* holds also in other direction *)
huffman@19551
   639
lemma ForallnPFilterPnil1: "!! ys . Finite ys ==>
huffman@19551
   640
   Forall (%x. ~P x) ys --> Filter P$ys = nil "
huffman@19551
   641
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
   642
done
huffman@19551
   643
huffman@19551
   644
lemmas ForallnPFilterPnil = ForallnPFilterPnil1 [THEN mp]
huffman@19551
   645
huffman@19551
   646
huffman@19551
   647
(* holds also in other direction *)
wenzelm@26008
   648
lemma ForallnPFilterPUU1: "~Finite ys & Forall (%x. ~P x) ys
wenzelm@26008
   649
                  --> Filter P$ys = UU "
huffman@19551
   650
apply (rule_tac x="ys" in Seq_induct)
huffman@19551
   651
apply (simp add: Forall_def sforall_def)
huffman@19551
   652
apply simp_all
huffman@19551
   653
done
huffman@19551
   654
huffman@19551
   655
lemmas ForallnPFilterPUU = ForallnPFilterPUU1 [THEN mp, OF conjI]
huffman@19551
   656
huffman@19551
   657
huffman@19551
   658
(* inverse of ForallnPFilterPnil *)
huffman@19551
   659
huffman@19551
   660
lemma FilternPnilForallP1: "!! ys . Filter P$ys = nil -->
huffman@19551
   661
   (Forall (%x. ~P x) ys & Finite ys)"
huffman@19551
   662
apply (rule_tac x="ys" in Seq_induct)
huffman@19551
   663
(* adm *)
huffman@19551
   664
apply (simp add: seq.compacts Forall_def sforall_def)
huffman@19551
   665
(* base cases *)
huffman@19551
   666
apply simp
huffman@19551
   667
apply simp
huffman@19551
   668
(* main case *)
huffman@19551
   669
apply simp
huffman@19551
   670
done
huffman@19551
   671
huffman@19551
   672
lemmas FilternPnilForallP = FilternPnilForallP1 [THEN mp]
huffman@19551
   673
huffman@19551
   674
(* inverse of ForallnPFilterPUU. proved apply 2 lemmas because of adm problems *)
huffman@19551
   675
huffman@19551
   676
lemma FilterUU_nFinite_lemma1: "Finite ys ==> Filter P$ys ~= UU"
huffman@19551
   677
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
   678
done
huffman@19551
   679
huffman@19551
   680
lemma FilterUU_nFinite_lemma2: "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU"
huffman@19551
   681
apply (rule_tac x="ys" in Seq_induct)
huffman@19551
   682
apply (simp add: Forall_def sforall_def)
huffman@19551
   683
apply simp_all
huffman@19551
   684
done
huffman@19551
   685
huffman@19551
   686
lemma FilternPUUForallP:
huffman@19551
   687
  "Filter P$ys = UU ==> (Forall (%x. ~P x) ys  & ~Finite ys)"
huffman@19551
   688
apply (rule conjI)
huffman@19551
   689
apply (cut_tac FilterUU_nFinite_lemma2 [THEN mp, COMP rev_contrapos])
huffman@19551
   690
apply auto
huffman@19551
   691
apply (blast dest!: FilterUU_nFinite_lemma1)
huffman@19551
   692
done
huffman@19551
   693
huffman@19551
   694
huffman@19551
   695
lemma ForallQFilterPnil:
huffman@19551
   696
  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|]
huffman@19551
   697
    ==> Filter P$ys = nil"
huffman@19551
   698
apply (erule ForallnPFilterPnil)
huffman@19551
   699
apply (erule ForallPForallQ)
huffman@19551
   700
apply auto
huffman@19551
   701
done
huffman@19551
   702
huffman@19551
   703
lemma ForallQFilterPUU:
huffman@19551
   704
 "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|]
huffman@19551
   705
    ==> Filter P$ys = UU "
huffman@19551
   706
apply (erule ForallnPFilterPUU)
huffman@19551
   707
apply (erule ForallPForallQ)
huffman@19551
   708
apply auto
huffman@19551
   709
done
huffman@19551
   710
huffman@19551
   711
huffman@19551
   712
huffman@19551
   713
(* ------------------------------------------------------------------------------------- *)
huffman@19551
   714
huffman@19551
   715
subsection "Takewhile, Forall, Filter"
huffman@19551
   716
huffman@19551
   717
huffman@19551
   718
lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P$x)"
huffman@19551
   719
apply (simp add: Forall_def Takewhile_def sforallPstakewhileP)
huffman@19551
   720
done
huffman@19551
   721
huffman@19551
   722
huffman@19551
   723
lemma ForallPTakewhileQ [simp]:
huffman@19551
   724
"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)"
huffman@19551
   725
apply (rule ForallPForallQ)
huffman@19551
   726
apply (rule ForallPTakewhileP)
huffman@19551
   727
apply auto
huffman@19551
   728
done
huffman@19551
   729
huffman@19551
   730
huffman@19551
   731
lemma FilterPTakewhileQnil [simp]:
wenzelm@26008
   732
  "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |]
wenzelm@26008
   733
   ==> Filter P$(Takewhile Q$ys) = nil"
huffman@19551
   734
apply (erule ForallnPFilterPnil)
huffman@19551
   735
apply (rule ForallPForallQ)
huffman@19551
   736
apply (rule ForallPTakewhileP)
huffman@19551
   737
apply auto
huffman@19551
   738
done
huffman@19551
   739
huffman@19551
   740
lemma FilterPTakewhileQid [simp]:
wenzelm@26008
   741
 "!! Q P. [| !!x. Q x ==> P x |] ==>
wenzelm@26008
   742
            Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)"
huffman@19551
   743
apply (rule ForallPFilterPid)
huffman@19551
   744
apply (rule ForallPForallQ)
huffman@19551
   745
apply (rule ForallPTakewhileP)
huffman@19551
   746
apply auto
huffman@19551
   747
done
huffman@19551
   748
huffman@19551
   749
huffman@19551
   750
lemma Takewhile_idempotent: "Takewhile P$(Takewhile P$s) = Takewhile P$s"
huffman@19551
   751
apply (rule_tac x="s" in Seq_induct)
huffman@19551
   752
apply (simp add: Forall_def sforall_def)
huffman@19551
   753
apply simp_all
huffman@19551
   754
done
huffman@19551
   755
huffman@19551
   756
lemma ForallPTakewhileQnP [simp]:
huffman@19551
   757
 "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s"
huffman@19551
   758
apply (rule_tac x="s" in Seq_induct)
huffman@19551
   759
apply (simp add: Forall_def sforall_def)
huffman@19551
   760
apply simp_all
huffman@19551
   761
done
huffman@19551
   762
huffman@19551
   763
lemma ForallPDropwhileQnP [simp]:
huffman@19551
   764
 "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s"
huffman@19551
   765
apply (rule_tac x="s" in Seq_induct)
huffman@19551
   766
apply (simp add: Forall_def sforall_def)
huffman@19551
   767
apply simp_all
huffman@19551
   768
done
huffman@19551
   769
huffman@19551
   770
huffman@19551
   771
lemma TakewhileConc1:
huffman@19551
   772
 "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)"
huffman@19551
   773
apply (rule_tac x="s" in Seq_induct)
huffman@19551
   774
apply (simp add: Forall_def sforall_def)
huffman@19551
   775
apply simp_all
huffman@19551
   776
done
huffman@19551
   777
huffman@19551
   778
lemmas TakewhileConc = TakewhileConc1 [THEN mp]
huffman@19551
   779
huffman@19551
   780
lemma DropwhileConc1:
huffman@19551
   781
 "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t"
huffman@19551
   782
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
   783
done
huffman@19551
   784
huffman@19551
   785
lemmas DropwhileConc = DropwhileConc1 [THEN mp]
huffman@19551
   786
huffman@19551
   787
huffman@19551
   788
huffman@19551
   789
(* ----------------------------------------------------------------------------------- *)
huffman@19551
   790
huffman@19551
   791
subsection "coinductive characterizations of Filter"
huffman@19551
   792
huffman@19551
   793
huffman@19551
   794
lemma divide_Seq_lemma:
huffman@19551
   795
 "HD$(Filter P$y) = Def x
huffman@19551
   796
    --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) 
huffman@19551
   797
             & Finite (Takewhile (%x. ~ P x)$y)  & P x"
huffman@19551
   798
huffman@19551
   799
(* FIX: pay attention: is only admissible with chain-finite package to be added to
huffman@19551
   800
        adm test and Finite f x admissibility *)
huffman@19551
   801
apply (rule_tac x="y" in Seq_induct)
huffman@19551
   802
apply (simp add: adm_subst [OF _ adm_Finite])
huffman@19551
   803
apply simp
huffman@19551
   804
apply simp
huffman@19551
   805
apply (case_tac "P a")
huffman@19551
   806
 apply simp
huffman@19551
   807
 apply blast
huffman@19551
   808
(* ~ P a *)
huffman@19551
   809
apply simp
huffman@19551
   810
done
huffman@19551
   811
huffman@19551
   812
lemma divide_Seq: "(x>>xs) << Filter P$y 
huffman@19551
   813
   ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y)))
huffman@19551
   814
      & Finite (Takewhile (%a. ~ P a)$y)  & P x"
huffman@19551
   815
apply (rule divide_Seq_lemma [THEN mp])
huffman@19551
   816
apply (drule_tac f="HD" and x="x>>xs" in  monofun_cfun_arg)
huffman@19551
   817
apply simp
huffman@19551
   818
done
huffman@19551
   819
huffman@19551
   820
huffman@19551
   821
lemma nForall_HDFilter:
huffman@19551
   822
 "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"
huffman@19551
   823
(* Pay attention: is only admissible with chain-finite package to be added to
huffman@19551
   824
        adm test *)
huffman@19551
   825
apply (rule_tac x="y" in Seq_induct)
huffman@19551
   826
apply (simp add: Forall_def sforall_def)
huffman@19551
   827
apply simp_all
huffman@19551
   828
done
huffman@19551
   829
huffman@19551
   830
huffman@19551
   831
lemma divide_Seq2: "~Forall P y
huffman@19551
   832
  ==> ? x. y= (Takewhile P$y @@ (x >> TL$(Dropwhile P$y))) &
huffman@19551
   833
      Finite (Takewhile P$y) & (~ P x)"
huffman@19551
   834
apply (drule nForall_HDFilter [THEN mp])
huffman@19551
   835
apply safe
huffman@19551
   836
apply (rule_tac x="x" in exI)
huffman@19551
   837
apply (cut_tac P1="%x. ~ P x" in divide_Seq_lemma [THEN mp])
huffman@19551
   838
apply auto
huffman@19551
   839
done
huffman@19551
   840
huffman@19551
   841
huffman@19551
   842
lemma divide_Seq3: "~Forall P y
huffman@19551
   843
  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)"
huffman@19551
   844
apply (drule divide_Seq2)
huffman@19551
   845
(*Auto_tac no longer proves it*)
huffman@19551
   846
apply fastsimp
huffman@19551
   847
done
huffman@19551
   848
huffman@19551
   849
lemmas [simp] = FilterPQ FilterConc Conc_cong
huffman@19551
   850
huffman@19551
   851
huffman@19551
   852
(* ------------------------------------------------------------------------------------- *)
huffman@19551
   853
huffman@19551
   854
huffman@19551
   855
subsection "take_lemma"
huffman@19551
   856
huffman@19551
   857
lemma seq_take_lemma: "(!n. seq_take n$x = seq_take n$x') = (x = x')"
huffman@19551
   858
apply (rule iffI)
huffman@19551
   859
apply (rule seq.take_lemmas)
huffman@19551
   860
apply auto
huffman@19551
   861
done
huffman@19551
   862
huffman@19551
   863
lemma take_reduction1:
huffman@19551
   864
"  ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2)
huffman@19551
   865
    --> seq_take n$(x @@ (t>>y1)) =  seq_take n$(x @@ (t>>y2)))"
huffman@19551
   866
apply (rule_tac x="x" in Seq_induct)
huffman@19551
   867
apply simp_all
huffman@19551
   868
apply (intro strip)
huffman@19551
   869
apply (case_tac "n")
huffman@19551
   870
apply auto
huffman@19551
   871
apply (case_tac "n")
huffman@19551
   872
apply auto
huffman@19551
   873
done
huffman@19551
   874
huffman@19551
   875
huffman@19551
   876
lemma take_reduction:
huffman@19551
   877
 "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|]
huffman@19551
   878
  ==> seq_take n$(x @@ (s>>y1)) =  seq_take n$(y @@ (t>>y2))"
huffman@19551
   879
apply (auto intro!: take_reduction1 [rule_format])
huffman@19551
   880
done
huffman@19551
   881
huffman@19551
   882
(* ------------------------------------------------------------------
huffman@19551
   883
          take-lemma and take_reduction for << instead of =
huffman@19551
   884
   ------------------------------------------------------------------ *)
huffman@19551
   885
huffman@19551
   886
lemma take_reduction_less1:
huffman@19551
   887
"  ! n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2)
huffman@19551
   888
    --> seq_take n$(x @@ (t>>y1)) <<  seq_take n$(x @@ (t>>y2)))"
huffman@19551
   889
apply (rule_tac x="x" in Seq_induct)
huffman@19551
   890
apply simp_all
huffman@19551
   891
apply (intro strip)
huffman@19551
   892
apply (case_tac "n")
huffman@19551
   893
apply auto
huffman@19551
   894
apply (case_tac "n")
huffman@19551
   895
apply auto
huffman@19551
   896
done
huffman@19551
   897
huffman@19551
   898
huffman@19551
   899
lemma take_reduction_less:
huffman@19551
   900
 "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|]
huffman@19551
   901
  ==> seq_take n$(x @@ (s>>y1)) <<  seq_take n$(y @@ (t>>y2))"
huffman@19551
   902
apply (auto intro!: take_reduction_less1 [rule_format])
huffman@19551
   903
done
huffman@19551
   904
huffman@19551
   905
lemma take_lemma_less1:
huffman@19551
   906
  assumes "!! n. seq_take n$s1 << seq_take n$s2"
huffman@19551
   907
  shows "s1<<s2"
huffman@19551
   908
apply (rule_tac t="s1" in seq.reach [THEN subst])
huffman@19551
   909
apply (rule_tac t="s2" in seq.reach [THEN subst])
huffman@19551
   910
apply (rule fix_def2 [THEN ssubst])
huffman@19551
   911
apply (subst contlub_cfun_fun)
huffman@19551
   912
apply (rule chain_iterate)
huffman@19551
   913
apply (subst contlub_cfun_fun)
huffman@19551
   914
apply (rule chain_iterate)
huffman@19551
   915
apply (rule lub_mono)
huffman@19551
   916
apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
huffman@19551
   917
apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
huffman@19551
   918
apply (rule prems [unfolded seq.take_def])
huffman@19551
   919
done
huffman@19551
   920
huffman@19551
   921
huffman@19551
   922
lemma take_lemma_less: "(!n. seq_take n$x << seq_take n$x') = (x << x')"
huffman@19551
   923
apply (rule iffI)
huffman@19551
   924
apply (rule take_lemma_less1)
huffman@19551
   925
apply auto
huffman@19551
   926
apply (erule monofun_cfun_arg)
huffman@19551
   927
done
huffman@19551
   928
huffman@19551
   929
(* ------------------------------------------------------------------
huffman@19551
   930
          take-lemma proof principles
huffman@19551
   931
   ------------------------------------------------------------------ *)
huffman@19551
   932
huffman@19551
   933
lemma take_lemma_principle1:
huffman@19551
   934
 "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
huffman@19551
   935
            !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|]
huffman@19551
   936
                          ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |]
huffman@19551
   937
               ==> A x --> (f x)=(g x)"
huffman@19551
   938
apply (case_tac "Forall Q x")
huffman@19551
   939
apply (auto dest!: divide_Seq3)
huffman@19551
   940
done
huffman@19551
   941
huffman@19551
   942
lemma take_lemma_principle2:
huffman@19551
   943
  "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
huffman@19551
   944
           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|]
huffman@19551
   945
                          ==> ! n. seq_take n$(f (s1 @@ y>>s2))
huffman@19551
   946
                                 = seq_take n$(g (s1 @@ y>>s2)) |]
huffman@19551
   947
               ==> A x --> (f x)=(g x)"
huffman@19551
   948
apply (case_tac "Forall Q x")
huffman@19551
   949
apply (auto dest!: divide_Seq3)
huffman@19551
   950
apply (rule seq.take_lemmas)
huffman@19551
   951
apply auto
huffman@19551
   952
done
huffman@19551
   953
huffman@19551
   954
huffman@19551
   955
(* Note: in the following proofs the ordering of proof steps is very
huffman@19551
   956
         important, as otherwise either (Forall Q s1) would be in the IH as
huffman@19551
   957
         assumption (then rule useless) or it is not possible to strengthen
huffman@19551
   958
         the IH apply doing a forall closure of the sequence t (then rule also useless).
huffman@19551
   959
         This is also the reason why the induction rule (nat_less_induct or nat_induct) has to
huffman@19551
   960
         to be imbuilt into the rule, as induction has to be done early and the take lemma
huffman@19551
   961
         has to be used in the trivial direction afterwards for the (Forall Q x) case.  *)
huffman@19551
   962
huffman@19551
   963
lemma take_lemma_induct:
huffman@19551
   964
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
huffman@19551
   965
         !! s1 s2 y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);
huffman@19551
   966
                          Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |]
huffman@19551
   967
                          ==>   seq_take (Suc n)$(f (s1 @@ y>>s2))
huffman@19551
   968
                              = seq_take (Suc n)$(g (s1 @@ y>>s2)) |]
huffman@19551
   969
               ==> A x --> (f x)=(g x)"
huffman@19551
   970
apply (rule impI)
huffman@19551
   971
apply (rule seq.take_lemmas)
huffman@19551
   972
apply (rule mp)
huffman@19551
   973
prefer 2 apply assumption
huffman@19551
   974
apply (rule_tac x="x" in spec)
haftmann@27105
   975
apply (rule nat.induct)
huffman@19551
   976
apply simp
huffman@19551
   977
apply (rule allI)
huffman@19551
   978
apply (case_tac "Forall Q xa")
huffman@19551
   979
apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
huffman@19551
   980
apply (auto dest!: divide_Seq3)
huffman@19551
   981
done
huffman@19551
   982
huffman@19551
   983
huffman@19551
   984
lemma take_lemma_less_induct:
huffman@19551
   985
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
huffman@19551
   986
        !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m$(f t) = seq_take m$(g t);
huffman@19551
   987
                          Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |]
huffman@19551
   988
                          ==>   seq_take n$(f (s1 @@ y>>s2))
huffman@19551
   989
                              = seq_take n$(g (s1 @@ y>>s2)) |]
huffman@19551
   990
               ==> A x --> (f x)=(g x)"
huffman@19551
   991
apply (rule impI)
huffman@19551
   992
apply (rule seq.take_lemmas)
huffman@19551
   993
apply (rule mp)
huffman@19551
   994
prefer 2 apply assumption
huffman@19551
   995
apply (rule_tac x="x" in spec)
huffman@19551
   996
apply (rule nat_less_induct)
huffman@19551
   997
apply (rule allI)
huffman@19551
   998
apply (case_tac "Forall Q xa")
huffman@19551
   999
apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
huffman@19551
  1000
apply (auto dest!: divide_Seq3)
huffman@19551
  1001
done
huffman@19551
  1002
huffman@19551
  1003
huffman@19551
  1004
huffman@19551
  1005
lemma take_lemma_in_eq_out:
huffman@19551
  1006
"!! Q. [| A UU  ==> (f UU) = (g UU) ;
huffman@19551
  1007
          A nil ==> (f nil) = (g nil) ;
huffman@19551
  1008
          !! s y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);
huffman@19551
  1009
                     A (y>>s) |]
huffman@19551
  1010
                     ==>   seq_take (Suc n)$(f (y>>s))
huffman@19551
  1011
                         = seq_take (Suc n)$(g (y>>s)) |]
huffman@19551
  1012
               ==> A x --> (f x)=(g x)"
huffman@19551
  1013
apply (rule impI)
huffman@19551
  1014
apply (rule seq.take_lemmas)
huffman@19551
  1015
apply (rule mp)
huffman@19551
  1016
prefer 2 apply assumption
huffman@19551
  1017
apply (rule_tac x="x" in spec)
haftmann@27105
  1018
apply (rule nat.induct)
huffman@19551
  1019
apply simp
huffman@19551
  1020
apply (rule allI)
huffman@19551
  1021
apply (rule_tac x="xa" in Seq_cases)
huffman@19551
  1022
apply simp_all
huffman@19551
  1023
done
huffman@19551
  1024
huffman@19551
  1025
huffman@19551
  1026
(* ------------------------------------------------------------------------------------ *)
huffman@19551
  1027
huffman@19551
  1028
subsection "alternative take_lemma proofs"
huffman@19551
  1029
huffman@19551
  1030
huffman@19551
  1031
(* --------------------------------------------------------------- *)
huffman@19551
  1032
(*              Alternative Proof of FilterPQ                      *)
huffman@19551
  1033
(* --------------------------------------------------------------- *)
huffman@19551
  1034
huffman@19551
  1035
declare FilterPQ [simp del]
huffman@19551
  1036
huffman@19551
  1037
huffman@19551
  1038
(* In general: How to do this case without the same adm problems
huffman@19551
  1039
   as for the entire proof ? *)
huffman@19551
  1040
lemma Filter_lemma1: "Forall (%x.~(P x & Q x)) s
huffman@19551
  1041
          --> Filter P$(Filter Q$s) =
huffman@19551
  1042
              Filter (%x. P x & Q x)$s"
huffman@19551
  1043
huffman@19551
  1044
apply (rule_tac x="s" in Seq_induct)
huffman@19551
  1045
apply (simp add: Forall_def sforall_def)
huffman@19551
  1046
apply simp_all
huffman@19551
  1047
done
huffman@19551
  1048
huffman@19551
  1049
lemma Filter_lemma2: "Finite s ==>
huffman@19551
  1050
          (Forall (%x. (~P x) | (~ Q x)) s
huffman@19551
  1051
          --> Filter P$(Filter Q$s) = nil)"
huffman@19551
  1052
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
  1053
done
huffman@19551
  1054
huffman@19551
  1055
lemma Filter_lemma3: "Finite s ==>
huffman@19551
  1056
          Forall (%x. (~P x) | (~ Q x)) s
huffman@19551
  1057
          --> Filter (%x. P x & Q x)$s = nil"
huffman@19551
  1058
apply (erule Seq_Finite_ind, simp_all)
huffman@19551
  1059
done
huffman@19551
  1060
huffman@19551
  1061
huffman@19551
  1062
lemma FilterPQ_takelemma: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
huffman@19551
  1063
apply (rule_tac A1="%x. True" and
huffman@19551
  1064
                 Q1="%x.~(P x & Q x)" and x1="s" in
huffman@19551
  1065
                 take_lemma_induct [THEN mp])
huffman@19551
  1066
(* better support for A = %x. True *)
huffman@19551
  1067
apply (simp add: Filter_lemma1)
huffman@19551
  1068
apply (simp add: Filter_lemma2 Filter_lemma3)
huffman@19551
  1069
apply simp
huffman@19551
  1070
done
huffman@19551
  1071
huffman@19551
  1072
declare FilterPQ [simp]
huffman@19551
  1073
huffman@19551
  1074
huffman@19551
  1075
(* --------------------------------------------------------------- *)
huffman@19551
  1076
(*              Alternative Proof of MapConc                       *)
huffman@19551
  1077
(* --------------------------------------------------------------- *)
huffman@19551
  1078
huffman@19551
  1079
huffman@19551
  1080
huffman@19551
  1081
lemma MapConc_takelemma: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
huffman@19551
  1082
apply (rule_tac A1="%x. True" and x1="x" in
huffman@19551
  1083
    take_lemma_in_eq_out [THEN mp])
huffman@19551
  1084
apply auto
huffman@19551
  1085
done
mueller@3071
  1086
wenzelm@19741
  1087
wenzelm@19741
  1088
ML {*
wenzelm@19741
  1089
wenzelm@27208
  1090
fun Seq_case_tac ctxt s i =
wenzelm@27239
  1091
  res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
wenzelm@27208
  1092
  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
wenzelm@19741
  1093
wenzelm@19741
  1094
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
wenzelm@27208
  1095
fun Seq_case_simp_tac ctxt s i =
wenzelm@27208
  1096
  let val ss = Simplifier.local_simpset_of ctxt in
wenzelm@27208
  1097
    Seq_case_tac ctxt s i
wenzelm@27208
  1098
    THEN asm_simp_tac ss (i+2)
wenzelm@27208
  1099
    THEN asm_full_simp_tac ss (i+1)
wenzelm@27208
  1100
    THEN asm_full_simp_tac ss i
wenzelm@27208
  1101
  end;
wenzelm@19741
  1102
wenzelm@19741
  1103
(* rws are definitions to be unfolded for admissibility check *)
wenzelm@27208
  1104
fun Seq_induct_tac ctxt s rws i =
wenzelm@27208
  1105
  let val ss = Simplifier.local_simpset_of ctxt in
wenzelm@27239
  1106
    res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
wenzelm@27208
  1107
    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1))))
wenzelm@27208
  1108
    THEN simp_tac (ss addsimps rws) i
wenzelm@27208
  1109
  end;
wenzelm@19741
  1110
wenzelm@27208
  1111
fun Seq_Finite_induct_tac ctxt i =
wenzelm@27208
  1112
  etac @{thm Seq_Finite_ind} i
wenzelm@27208
  1113
  THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (Simplifier.local_simpset_of ctxt) i)));
wenzelm@19741
  1114
wenzelm@27208
  1115
fun pair_tac ctxt s =
wenzelm@27239
  1116
  res_inst_tac ctxt [(("p", 0), s)] PairE
wenzelm@27208
  1117
  THEN' hyp_subst_tac THEN' asm_full_simp_tac (Simplifier.local_simpset_of ctxt);
wenzelm@19741
  1118
wenzelm@19741
  1119
(* induction on a sequence of pairs with pairsplitting and simplification *)
wenzelm@27208
  1120
fun pair_induct_tac ctxt s rws i =
wenzelm@27208
  1121
  let val ss = Simplifier.local_simpset_of ctxt in
wenzelm@27239
  1122
    res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
wenzelm@27208
  1123
    THEN pair_tac ctxt "a" (i+3)
wenzelm@27208
  1124
    THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1))))
wenzelm@27208
  1125
    THEN simp_tac (ss addsimps rws) i
wenzelm@27208
  1126
  end;
wenzelm@19741
  1127
wenzelm@19741
  1128
*}
wenzelm@19741
  1129
wenzelm@19741
  1130
end