(* Title: HOLCF/IOA/meta_theory/Seq.thy ID: $Id: Seq.thy,v 1.12 2005/09/02 15:24:02 wenzelm Exp $ Author: Olaf Müller *) header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *} theory Seq imports HOLCF begin domain 'a seq = nil | "##" (HD :: 'a) (lazy TL :: "'a seq") (infixr 65) consts sfilter :: "('a -> tr) -> 'a seq -> 'a seq" smap :: "('a -> 'b) -> 'a seq -> 'b seq" sforall :: "('a -> tr) => 'a seq => bool" sforall2 :: "('a -> tr) -> 'a seq -> tr" slast :: "'a seq -> 'a" sconc :: "'a seq -> 'a seq -> 'a seq" sdropwhile ::"('a -> tr) -> 'a seq -> 'a seq" stakewhile ::"('a -> tr) -> 'a seq -> 'a seq" szip ::"'a seq -> 'b seq -> ('a*'b) seq" sflat :: "('a seq) seq -> 'a seq" sfinite :: "'a seq set" Partial ::"'a seq => bool" Infinite ::"'a seq => bool" nproj :: "nat => 'a seq => 'a" sproj :: "nat => 'a seq => 'a seq" syntax "@@" :: "'a seq => 'a seq => 'a seq" (infixr 65) "Finite" :: "'a seq => bool" translations "xs @@ ys" == "sconc $ xs $ ys" "Finite x" == "x:sfinite" "~(Finite x)" =="x~:sfinite" defs (* f not possible at lhs, as "pattern matching" only for % x arguments, f cannot be written at rhs in front, as fix_eq3 does not apply later *) smap_def: "smap == (fix$(LAM h f tr. case tr of nil => nil | x##xs => f$x ## h$f$xs))" sfilter_def: "sfilter == (fix$(LAM h P t. case t of nil => nil | x##xs => If P$x then x##(h$P$xs) else h$P$xs fi))" sforall_def: "sforall P t == (sforall2$P$t ~=FF)" sforall2_def: "sforall2 == (fix$(LAM h P t. case t of nil => TT | x##xs => P$x andalso h$P$xs))" sconc_def: "sconc == (fix$(LAM h t1 t2. case t1 of nil => t2 | x##xs => x##(h$xs$t2)))" slast_def: "slast == (fix$(LAM h t. case t of nil => UU | x##xs => (If is_nil$xs then x else h$xs fi)))" stakewhile_def: "stakewhile == (fix$(LAM h P t. case t of nil => nil | x##xs => If P$x then x##(h$P$xs) else nil fi))" sdropwhile_def: "sdropwhile == (fix$(LAM h P t. case t of nil => nil | x##xs => If P$x then h$P$xs else t fi))" sflat_def: "sflat == (fix$(LAM h t. case t of nil => nil | x##xs => x @@ (h$xs)))" szip_def: "szip == (fix$(LAM h t1 t2. case t1 of nil => nil | x##xs => (case t2 of nil => UU | y##ys => <x,y>##(h$xs$ys))))" Partial_def: "Partial x == (seq_finite x) & ~(Finite x)" Infinite_def: "Infinite x == ~(seq_finite x)" inductive "sfinite" intros sfinite_0: "nil:sfinite" sfinite_n: "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite" ML {* use_legacy_bindings (the_context ()) *} ML {* structure seq = struct open seq val injects = [injects] val inverts = [inverts] val finites = [finites] val take_lemmas = [take_lemmas] end structure sfinite = struct open sfinite val elim = elims val elims = [elims] end *} end
theorem smap_unfold:
smap = (LAM f tr. case tr of nil => nil | x ## xs => f·x ## smap·f·xs)
theorem smap_nil:
smap·f·nil = nil
theorem smap_UU:
smap·f·UU = UU
theorem smap_cons:
x ≠ UU ==> smap·f·(x ## xs) = f·x ## smap·f·xs
theorem sfilter_unfold:
sfilter = (LAM P tr. case tr of nil => nil | x ## xs => If P·x then x ## sfilter·P·xs else sfilter·P·xs fi)
theorem sfilter_nil:
sfilter·P·nil = nil
theorem sfilter_UU:
sfilter·P·UU = UU
theorem sfilter_cons:
x ≠ UU ==> sfilter·P·(x ## xs) = If P·x then x ## sfilter·P·xs else sfilter·P·xs fi
theorem sforall2_unfold:
sforall2 = (LAM P tr. case tr of nil => TT | x ## xs => P·x andalso sforall2·P·xs)
theorem sforall2_nil:
sforall2·P·nil = TT
theorem sforall2_UU:
sforall2·P·UU = UU
theorem sforall2_cons:
x ≠ UU ==> sforall2·P·(x ## xs) = (P·x andalso sforall2·P·xs)
theorem stakewhile_unfold:
stakewhile = (LAM P tr. case tr of nil => nil | x ## xs => If P·x then x ## stakewhile·P·xs else nil fi)
theorem stakewhile_nil:
stakewhile·P·nil = nil
theorem stakewhile_UU:
stakewhile·P·UU = UU
theorem stakewhile_cons:
x ≠ UU ==> stakewhile·P·(x ## xs) = If P·x then x ## stakewhile·P·xs else nil fi
theorem sdropwhile_unfold:
sdropwhile = (LAM P tr. case tr of nil => nil | x ## xs => If P·x then sdropwhile·P·xs else tr fi)
theorem sdropwhile_nil:
sdropwhile·P·nil = nil
theorem sdropwhile_UU:
sdropwhile·P·UU = UU
theorem sdropwhile_cons:
x ≠ UU ==> sdropwhile·P·(x ## xs) = If P·x then sdropwhile·P·xs else x ## xs fi
theorem slast_unfold:
slast = (LAM tr. case tr of nil => UU | x ## xs => If is_nil·xs then x else slast·xs fi)
theorem slast_nil:
slast·nil = UU
theorem slast_UU:
slast·UU = UU
theorem slast_cons:
x ≠ UU ==> slast·(x ## xs) = If is_nil·xs then x else slast·xs fi
theorem sconc_unfold:
sconc = (LAM t1 t2. case t1 of nil => t2 | x ## xs => x ## xs @@ t2)
theorem sconc_nil:
nil @@ y = y
theorem sconc_UU:
UU @@ y = UU
theorem sconc_cons:
(x ## xs) @@ y = x ## xs @@ y
theorem sflat_unfold:
sflat = (LAM tr. case tr of nil => nil | x ## xs => x @@ sflat·xs)
theorem sflat_nil:
sflat·nil = nil
theorem sflat_UU:
sflat·UU = UU
theorem sflat_cons:
sflat·(x ## xs) = x @@ sflat·xs
theorem szip_unfold:
szip = (LAM t1 t2. case t1 of nil => nil | x ## xs => case t2 of nil => UU | y ## ys => <x, y> ## szip·xs·ys)
theorem szip_nil:
szip·nil·y = nil
theorem szip_UU1:
szip·UU·y = UU
theorem szip_UU2:
x ≠ nil ==> szip·x·UU = UU
theorem szip_cons_nil:
x ≠ UU ==> szip·(x ## xs)·nil = UU
theorem szip_cons:
[| x ≠ UU; y ≠ UU |] ==> szip·(x ## xs)·(y ## ys) = <x, y> ## szip·xs·ys
theorem scons_inject_eq:
[| x ≠ UU; y ≠ UU |] ==> (x ## xs = y ## ys) = (x = y ∧ xs = ys)
theorem nil_less_is_nil:
nil << x ==> nil = x
theorem if_and_sconc:
(if b then tr1.0 else tr2.0) @@ tr = (if b then tr1.0 @@ tr else tr2.0 @@ tr)
theorem sfiltersconc:
sfilter·P·(x @@ y) = sfilter·P·x @@ sfilter·P·y
theorem sforallPstakewhileP:
sforall P (stakewhile·P·x)
theorem forallPsfilterP:
sforall P (sfilter·P·x)
theorem Finite_UU_a:
Finite x --> x ≠ UU
theorem Finite_UU:
¬ Finite UU
theorem Finite_cons_a:
Finite x --> a ≠ UU --> x = a ## xs --> Finite xs
theorem Finite_cons:
a ≠ UU ==> Finite (a ## x) = Finite x
theorem seq_finite_ind_lemma:
(!!n. P (seq_take n·s)) ==> seq_finite s --> P s
theorem seq_finite_ind:
[| P UU; P nil; !!x s1. [| x ≠ UU; P s1 |] ==> P (x ## s1) |] ==> seq_finite s --> P s