Up to index of Isabelle/HOLCF/IOA
theory Sequence(* 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
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
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
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
theorem HD_Cons:
HD·(x>>y) = Def x
theorem TL_Cons:
TL·(x>>y) = y
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)
theorem Finite_flat:
[| Finite x; Finite y ∧ x << y |] ==> x = y
theorem adm_Finite:
adm (%x. Finite x)
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)
theorem Finite_Last1:
Finite s ==> s ≠ nil --> Last·s ≠ UU
theorem Finite_Last2:
Finite s ==> Last·s = UU --> s = nil
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
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
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
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
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
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
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
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