# Theory Sequence

Up to index of Isabelle/HOLCF/IOA

theory Sequence
imports Seq
uses [Sequence.ML]
begin

    (*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
        ID:         $Id: Sequence.thy,v 1.13 2005/09/02 15:24:02 wenzelm Exp $
        Author:     Olaf Müller

    Sequences over flat domains with lifted elements.
    *)

    theory Sequence
    imports Seq
    begin

    defaultsort type

    types 'a Seq = "'a::type lift seq"

    consts

      Consq            ::"'a            => 'a Seq -> 'a Seq"
      Filter           ::"('a => bool)  => 'a Seq -> 'a Seq"
      Map              ::"('a => 'b)    => 'a Seq -> 'b Seq"
      Forall           ::"('a => bool)  => 'a Seq => bool"
      Last             ::"'a Seq        -> 'a lift"
      Dropwhile        ::"('a => bool)  => 'a Seq -> 'a Seq"
      Takewhile        ::"('a => bool)  => 'a Seq -> 'a Seq"
      Zip              ::"'a Seq        -> 'b Seq -> ('a * 'b) Seq"
      Flat             ::"('a Seq) seq   -> 'a Seq"

      Filter2          ::"('a => bool)  => 'a Seq -> 'a Seq"

    syntax

     "@Consq"         ::"'a => 'a Seq => 'a Seq"       ("(_/>>_)"  [66,65] 65)
     (* list Enumeration *)
      "_totlist"      :: "args => 'a Seq"              ("[(_)!]")
      "_partlist"     :: "args => 'a Seq"              ("[(_)?]")

    syntax (xsymbols)
      "@Consq"     ::"'a => 'a Seq => 'a Seq"       ("(_\<leadsto>_)"  [66,65] 65)

    translations
      "a>>s"         == "Consq a$s"
      "[x, xs!]"     == "x>>[xs!]"
      "[x!]"         == "x>>nil"
      "[x, xs?]"     == "x>>[xs?]"
      "[x?]"         == "x>>UU"

    defs

    Consq_def:     "Consq a == LAM s. Def a ## s"

    Filter_def:    "Filter P == sfilter$(flift2 P)"

    Map_def:       "Map f  == smap$(flift2 f)"

    Forall_def:    "Forall P == sforall (flift2 P)"

    Last_def:      "Last == slast"

    Dropwhile_def: "Dropwhile P == sdropwhile$(flift2 P)"

    Takewhile_def: "Takewhile P == stakewhile$(flift2 P)"

    Flat_def:      "Flat == sflat"

    Zip_def:
      "Zip == (fix$(LAM h t1 t2. case t1 of
                   nil   => nil
                 | x##xs => (case t2 of
                              nil => UU
                            | y##ys => (case x of
                                          UU  => UU
                                        | Def a => (case y of
                                                      UU => UU
                                                    | Def b => Def (a,b)##(h$xs$ys))))))"

    Filter2_def:    "Filter2 P == (fix$(LAM h t. case t of
                nil => nil
              | x##xs => (case x of UU => UU | Def y => (if P y
                         then x##(h$xs)
                         else     h$xs))))"

    axioms  -- {* for test purposes should be deleted FIX !! *}  (* FIXME *)
      adm_all: "adm f"

    ML {* use_legacy_bindings (the_context ()) *}

    end

## recursive equations of operators

theorem Map_UU:

      Map f·UU = UU

theorem Map_nil:

      Map f·nil = nil

theorem Map_cons:

      Map f·(x>>xs) = f x>>Map f·xs

theorem Filter_UU:

      Filter P·UU = UU

theorem Filter_nil:

      Filter P·nil = nil

theorem Filter_cons:

      Filter P·(x>>xs) = (if P x then x>>Filter P·xs else Filter P·xs)

theorem Forall_UU:

      Forall P UU

theorem Forall_nil:

      Forall P nil

theorem Forall_cons:

      Forall P (x>>xs) = (P x ∧ Forall P xs)

theorem Conc_cons:

      (x>>xs) @@ y = x>>xs @@ y

theorem Takewhile_UU:

      Takewhile P·UU = UU

theorem Takewhile_nil:

      Takewhile P·nil = nil

theorem Takewhile_cons:

      Takewhile P·(x>>xs) = (if P x then x>>Takewhile P·xs else nil)

theorem Dropwhile_UU:

      Dropwhile P·UU = UU

theorem Dropwhile_nil:

      Dropwhile P·nil = nil

theorem Dropwhile_cons:

      Dropwhile P·(x>>xs) = (if P x then Dropwhile P·xs else x>>xs)

theorem Last_UU:

      Last·UU = UU

theorem Last_nil:

      Last·nil = UU

theorem Last_cons:

      Last·(x>>xs) = (if xs = nil then Def x else Last·xs)

theorem Flat_UU:

      Flat·UU = UU

theorem Flat_nil:

      Flat·nil = nil

theorem Flat_cons:

      Flat·(x ## xs) = x @@ Flat·xs

theorem Zip_unfold:

      Zip =
      (LAM t1 t2.
          case t1 of nil => nil
          | x ## xs =>
              case t2 of nil => UU
              | y ## ys =>
                  case x of UU => UU
                  | Def a => case y of UU => UU | Def b => Def (a, b) ## Zip·xs·ys)

theorem Zip_UU1:

      Zip·UU·y = UU

theorem Zip_UU2:

      x ≠ nil ==> Zip·x·UU = UU

theorem Zip_nil:

      Zip·nil·y = nil

theorem Zip_cons_nil:

      Zip·(x>>xs)·nil = UU

theorem Zip_cons:

      Zip·(x>>xs)·(y>>ys) = (x, y)>>Zip·xs·ys

## Cons

theorem Consq_def2:

      a>>s = Def a ## s

theorem Seq_exhaust:

      x = UU ∨ x = nil ∨ (∃a s. x = a>>s)

theorem Seq_cases:

      [| x = UU ==> P; x = nil ==> P; !!a s. x = a>>s ==> P |] ==> P

theorem Cons_not_UU:

      a>>s ≠ UU

theorem Cons_not_less_UU:

      ¬ a>>x << UU

theorem Cons_not_less_nil:

      ¬ a>>s << nil

theorem Cons_not_nil:

      a>>s ≠ nil

theorem Cons_not_nil2:

      nil ≠ a>>s

theorem Cons_inject_eq:

      (a>>s = b>>t) = (a = b ∧ s = t)

theorem Cons_inject_less_eq:

      a>>s << b>>t = (a = b ∧ s << t)

theorem seq_take_Cons:

      seq_take (Suc n)·(a>>x) = a>>seq_take n·x

## induction

theorem Seq_induct:

      [| adm P; P UU; P nil; !!a s. P s ==> P (a>>s) |] ==> P x

theorem Seq_FinitePartial_ind:

      [| P UU; P nil; !!a s. P s ==> P (a>>s) |] ==> seq_finite x --> P x

theorem Seq_Finite_ind:

      [| Finite x; P nil; !!a s. [| Finite s; P s |] ==> P (a>>s) |] ==> P x

## HD,TL

theorem HD_Cons:

      HD·(x>>y) = Def x

theorem TL_Cons:

      TL·(x>>y) = y

## Finite, Partial, Infinite

theorem Finite_Cons:

      Finite (a>>xs) = Finite xs

theorem FiniteConc_1:

      Finite x ==> Finite y --> Finite (x @@ y)

theorem FiniteConc_2:

      Finite z ==> ∀x y. z = x @@ y --> Finite x ∧ Finite y

theorem FiniteConc:

      Finite (x @@ y) = (Finite x ∧ Finite y)

theorem FiniteMap1:

      Finite s ==> Finite (Map f·s)

theorem FiniteMap2:

      Finite s ==> ∀t. s = Map f·t --> Finite t

theorem Map2Finite:

      Finite (Map f·s) = Finite s

theorem FiniteFilter:

      Finite s ==> Finite (Filter P·s)

## admissibility

theorem Finite_flat:

      [| Finite x; Finite y ∧ x << y |] ==> x = y

theorem adm_Finite:

      adm (%x. Finite x)

## Conc

theorem Conc_cong:

      Finite x ==> (x @@ y = x @@ z) = (y = z)

theorem Conc_assoc:

      (x @@ y) @@ z = x @@ y @@ z

theorem nilConc:

      s @@ nil = s

theorem nil_is_Conc:

      (nil = x @@ y) = (x = nil ∧ y = nil)

theorem nil_is_Conc2:

      (x @@ y = nil) = (x = nil ∧ y = nil)

## Last

theorem Finite_Last1:

      Finite s ==> s ≠ nil --> Last·s ≠ UU

theorem Finite_Last2:

      Finite s ==> Last·s = UU --> s = nil

## Filter, Conc

theorem FilterPQ:

      Filter P·(Filter Q·s) = Filter (%x. P x ∧ Q x)·s

theorem FilterConc:

      Filter P·(x @@ y) = Filter P·x @@ Filter P·y

## Map

theorem MapMap:

      Map f·(Map g·s) = Map (f o g)·s

theorem MapConc:

      Map f·(x @@ y) = Map f·x @@ Map f·y

theorem MapFilter:

      Filter P·(Map f·x) = Map f·(Filter (P o f)·x)

theorem nilMap:

      nil = Map f·s --> s = nil

theorem ForallMap:

      Forall P (Map f·s) = Forall (P o f) s

## Forall

theorem ForallPForallQ1:

      Forall P ys ∧ (∀x. P x --> Q x) --> Forall Q ys

theorem ForallPForallQ:

      [| Forall P ys; !!x. P x ==> Q x |] ==> Forall Q ys

theorem Forall_Conc_impl:

      Forall P x ∧ Forall P y --> Forall P (x @@ y)

theorem Forall_Conc:

      Finite x ==> Forall P (x @@ y) = (Forall P x ∧ Forall P y)

theorem ForallTL1:

      Forall P s --> Forall P (TL·s)

theorem ForallTL:

      Forall P s ==> Forall P (TL·s)

theorem ForallDropwhile1:

      Forall P s --> Forall P (Dropwhile Q·s)

theorem ForallDropwhile:

      Forall P s ==> Forall P (Dropwhile Q·s)

theorem Forall_prefix:

      ∀s. Forall P s --> t << s --> Forall P t

theorem Forall_prefixclosed:

      [| Forall P x; t << x |] ==> Forall P t

theorem Forall_postfixclosed:

      [| Finite h; Forall P s; s = h @@ t |] ==> Forall P t

theorem ForallPFilterQR1:

      (∀x. P x --> Q x = R x) ∧ Forall P tr --> Filter Q·tr = Filter R·tr

theorem ForallPFilterQR:

      [| !!x. P x --> Q x = R x; Forall P tr |] ==> Filter Q·tr = Filter R·tr

## Forall, Filter

theorem ForallPFilterP:

      Forall P (Filter P·x)

theorem ForallPFilterPid1:

      Forall P x --> Filter P·x = x

theorem ForallPFilterPid:

      Forall P x ==> Filter P·x = x

theorem ForallnPFilterPnil1:

      Finite ys ==> Forall (%x. ¬ P x) ys --> Filter P·ys = nil

theorem ForallnPFilterPnil:

      [| Finite ys; Forall (%x. ¬ P x) ys |] ==> Filter P·ys = nil

theorem ForallnPFilterPUU1:

      ¬ Finite ys ∧ Forall (%x. ¬ P x) ys --> Filter P·ys = UU

theorem ForallnPFilterPUU:

      [| ¬ Finite ys; Forall (%x. ¬ P x) ys |] ==> Filter P·ys = UU

theorem FilternPnilForallP1:

      Filter P·ys = nil --> Forall (%x. ¬ P x) ys ∧ Finite ys

theorem FilternPnilForallP:

      Filter P·ys = nil ==> Forall (%x. ¬ P x) ys ∧ Finite ys

theorem FilterUU_nFinite_lemma1:

      Finite ys ==> Filter P·ys ≠ UU

theorem FilterUU_nFinite_lemma2:

      ¬ Forall (%x. ¬ P x) ys --> Filter P·ys ≠ UU

theorem FilternPUUForallP:

      Filter P·ys = UU ==> Forall (%x. ¬ P x) ys ∧ ¬ Finite ys

theorem ForallQFilterPnil:

      [| Forall Q ys; Finite ys; !!x. Q x ==> ¬ P x |] ==> Filter P·ys = nil

theorem ForallQFilterPUU:

      [| ¬ Finite ys; Forall Q ys; !!x. Q x ==> ¬ P x |] ==> Filter P·ys = UU

## Takewhile, Forall, Filter

theorem ForallPTakewhileP:

      Forall P (Takewhile P·x)

theorem ForallPTakewhileQ:

      (!!x. Q x ==> P x) ==> Forall P (Takewhile Q·x)

theorem FilterPTakewhileQnil:

      [| Finite (Takewhile Q·ys); !!x. Q x ==> ¬ P x |]
      ==> Filter P·(Takewhile Q·ys) = nil

theorem FilterPTakewhileQid:

      (!!x. Q x ==> P x) ==> Filter P·(Takewhile Q·ys) = Takewhile Q·ys

theorem Takewhile_idempotent:

      Takewhile P·(Takewhile P·s) = Takewhile P·s

theorem ForallPTakewhileQnP:

      Forall P s --> Takewhile (%x. Q x ∨ ¬ P x)·s = Takewhile Q·s

theorem ForallPDropwhileQnP:

      Forall P s --> Dropwhile (%x. Q x ∨ ¬ P x)·s = Dropwhile Q·s

theorem TakewhileConc1:

      Forall P s --> Takewhile P·(s @@ t) = s @@ Takewhile P·t

theorem TakewhileConc:

      Forall P s ==> Takewhile P·(s @@ t) = s @@ Takewhile P·t

theorem DropwhileConc1:

      Finite s ==> Forall P s --> Dropwhile P·(s @@ t) = Dropwhile P·t

theorem DropwhileConc:

      [| Finite s; Forall P s |] ==> Dropwhile P·(s @@ t) = Dropwhile P·t

## coinductive characterizations of Filter

theorem divide_Seq_lemma:

      HD·(Filter P·y) = Def x -->
      y = Takewhile (%x. ¬ P x)·y @@ x>>TL·(Dropwhile (%a. ¬ P a)·y) ∧
      Finite (Takewhile (%x. ¬ P x)·y) ∧ P x

theorem divide_Seq:

      x>>xs << Filter P·y
      ==> y = Takewhile (%a. ¬ P a)·y @@ x>>TL·(Dropwhile (%a. ¬ P a)·y) ∧
          Finite (Takewhile (%a. ¬ P a)·y) ∧ P x

theorem nForall_HDFilter:

      ¬ Forall P y --> (∃x. HD·(Filter (%a. ¬ P a)·y) = Def x)

theorem divide_Seq2:

      ¬ Forall P y
      ==> ∃x. y = Takewhile P·y @@ x>>TL·(Dropwhile P·y) ∧
              Finite (Takewhile P·y) ∧ ¬ P x

theorem divide_Seq3:

      ¬ Forall P y ==> ∃x bs rs. y = bs @@ x>>rs ∧ Finite bs ∧ Forall P bs ∧ ¬ P x

## take_lemma

theorem seq_take_lemma:

      (∀n. seq_take n·x = seq_take n·x') = (x = x')

theorem take_reduction1:

      ∀n. (∀k<n. seq_take k·y1.0 = seq_take k·y2.0) -->
          seq_take n·(x @@ t>>y1.0) = seq_take n·(x @@ t>>y2.0)

theorem take_reduction:

      [| x = y; s = t; !!k. k < n ==> seq_take k·y1.0 = seq_take k·y2.0 |]
      ==> seq_take n·(x @@ s>>y1.0) = seq_take n·(y @@ t>>y2.0)

theorem take_reduction_less1:

      ∀n. (∀k<n. seq_take k·y1.0 << seq_take k·y2.0) -->
          seq_take n·(x @@ t>>y1.0) << seq_take n·(x @@ t>>y2.0)

theorem take_reduction_less:

      [| x = y; s = t; !!k. k < n ==> seq_take k·y1.0 << seq_take k·y2.0 |]
      ==> seq_take n·(x @@ s>>y1.0) << seq_take n·(y @@ t>>y2.0)

theorem take_lemma_less1:

      (!!n. seq_take n·s1.0 << seq_take n·s2.0) ==> s1.0 << s2.0

theorem take_lemma_less:

      (∀n. seq_take n·x << seq_take n·x') = x << x'

theorem take_lemma_principle1:

      [| !!s. [| Forall Q s; A s |] ==> f s = g s;
         !!s1 s2 y.
            [| Forall Q s1; Finite s1; ¬ Q y; A (s1 @@ y>>s2) |]
            ==> f (s1 @@ y>>s2) = g (s1 @@ y>>s2) |]
      ==> A x --> f x = g x

theorem take_lemma_principle2:

      [| !!s. [| Forall Q s; A s |] ==> f s = g s;
         !!s1 s2 y.
            [| Forall Q s1; Finite s1; ¬ Q y; A (s1 @@ y>>s2) |]
            ==> ∀n. seq_take n·(f (s1 @@ y>>s2)) = seq_take n·(g (s1 @@ y>>s2)) |]
      ==> A x --> f x = g x

theorem take_lemma_induct:

      [| !!s. [| Forall Q s; A s |] ==> f s = g s;
         !!s1 s2 y n.
            [| ∀t. A t --> seq_take n·(f t) = seq_take n·(g t); Forall Q s1;
               Finite s1; ¬ Q y; A (s1 @@ y>>s2) |]
            ==> seq_take (Suc n)·(f (s1 @@ y>>s2)) =
                seq_take (Suc n)·(g (s1 @@ y>>s2)) |]
      ==> A x --> f x = g x

theorem take_lemma_less_induct:

      [| !!s. [| Forall Q s; A s |] ==> f s = g s;
         !!s1 s2 y n.
            [| ∀t m. m < n --> A t --> seq_take m·(f t) = seq_take m·(g t);
               Forall Q s1; Finite s1; ¬ Q y; A (s1 @@ y>>s2) |]
            ==> seq_take n·(f (s1 @@ y>>s2)) = seq_take n·(g (s1 @@ y>>s2)) |]
      ==> A x --> f x = g x

theorem take_lemma_in_eq_out:

      [| A UU ==> f UU = g UU; A nil ==> f nil = g nil;
         !!s y n.
            [| ∀t. A t --> seq_take n·(f t) = seq_take n·(g t); A (y>>s) |]
            ==> seq_take (Suc n)·(f (y>>s)) = seq_take (Suc n)·(g (y>>s)) |]
      ==> A x --> f x = g x

## alternative take_lemma proofs

theorem Filter_lemma1:

      Forall (%x. ¬ (P x ∧ Q x)) s -->
      Filter P·(Filter Q·s) = Filter (%x. P x ∧ Q x)·s

theorem Filter_lemma2:

      Finite s ==> Forall (%x. ¬ P x ∨ ¬ Q x) s --> Filter P·(Filter Q·s) = nil

theorem Filter_lemma3:

      Finite s ==> Forall (%x. ¬ P x ∨ ¬ Q x) s --> Filter (%x. P x ∧ Q x)·s = nil

theorem FilterPQ_takelemma:

      Filter P·(Filter Q·s) = Filter (%x. P x ∧ Q x)·s

theorem MapConc_takelemma:

      Map f·(x @@ y) = Map f·x @@ Map f·y