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 = bs = t)

theorem Cons_inject_less_eq:

  a>>s << b>>t = (a = bs << 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 yx << 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 xQ xs

theorem FilterConc:

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

Map

theorem MapMap:

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

theorem MapConc:

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

theorem MapFilter:

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

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 xs = Takewhile Q·s

theorem ForallPDropwhileQnP:

  Forall P s --> Dropwhile (%x. Q x ∨ ¬ P xs = 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 xy @@ x>>TL·(Dropwhile (%a. ¬ P ay) ∧
  Finite (Takewhile (%x. ¬ P xy) ∧ P x

theorem divide_Seq:

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

theorem nForall_HDFilter:

  ¬ Forall P y --> (∃x. HD·(Filter (%a. ¬ P ay) = 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 xQ x)) s -->
  Filter P·(Filter Q·s) = Filter (%x. P xQ xs

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 xQ xs = nil

theorem FilterPQ_takelemma:

  Filter P·(Filter Q·s) = Filter (%x. P xQ xs

theorem MapConc_takelemma:

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