Theory Stream_Fusion_LList
section ‹Stream fusion for coinductive lists›
theory Stream_Fusion_LList imports
Stream_Fusion_List
Coinductive.Coinductive_List
begin
text ‹
There are two choices of how many @{const Skip}s may occur consecutively.
\begin{itemize}
\item A generator for @{typ "'a llist"} may return only finitely many @{const Skip}s before
it has to decide on a @{const Done} or @{const Yield}. Then, we can define stream versions
for all functions that can be defined by corecursion up-to. This in particular excludes
@{const lfilter}. Moreover, we have to prove that every generator satisfies this
restriction.
\item A generator for @{typ "'a llist"} may return infinitely many @{const Skip}s in a row.
Then, the ‹lunstream› function suffers from the same difficulties as @{const lfilter} with
definitions, but we can define it using the least fixpoint approach described in
\<^cite>‹"LochbihlerHoelzl2014ITP"›. Consequently, we can only fuse transformers that are monotone and
continuous with respect to the ccpo ordering. This in particular excludes @{const lappend}.
\end{itemize}
Here, we take the both approaches where we consider the first preferable to the second.
Consequently, we define producers such that they produce generators of the first kind, if possible.
There will be multiple equations for transformers and consumers that deal with all the different
combinations for their parameter generators. Transformers should yield generators of the first
kind whenever possible. Consumers can be defined using ‹lunstream› and refined with custom
code equations, i.e., they can operate with infinitely many ‹Skip›s in a row. We just
have to lift the fusion equation to the first kind, too.
›
type_synonym ('a, 's) lgenerator = "'s ⇒ ('a, 's) step"
inductive_set productive_on :: "('a, 's) lgenerator ⇒ 's set"
for g :: "('a, 's) lgenerator"
where
Done: "g s = Done ⟹ s ∈ productive_on g"
| Skip: "⟦ g s = Skip s'; s' ∈ productive_on g ⟧ ⟹ s ∈ productive_on g"
| Yield: "g s = Yield x s' ⟹ s ∈ productive_on g"
definition productive :: "('a, 's) lgenerator ⇒ bool"
where "productive g ⟷ productive_on g = UNIV"
lemma productiveI [intro?]:
"(⋀s. s ∈ productive_on g) ⟹ productive g"
by(auto simp add: productive_def)
lemma productive_onI [dest?]: "productive g ⟹ s ∈ productive_on g"
by(simp add: productive_def)
text ‹A type of generators that eventually will yield something else than a skip.›
typedef ('a, 's) lgenerator' = "{g :: ('a, 's) lgenerator. productive g}"
morphisms lgenerator Abs_lgenerator'
proof
show "(λ_. Done) ∈ ?lgenerator'" by(auto intro: productive_on.intros productiveI)
qed
setup_lifting type_definition_lgenerator'
subsection ‹Conversions to @{typ "'a llist"}›
subsubsection ‹Infinitely many consecutive @{term Skip}s›
context fixes g :: "('a, 's) lgenerator"
notes [[function_internals]]
begin
partial_function (llist) lunstream :: "'s ⇒ 'a llist"
where
"lunstream s = (case g s of
Done ⇒ LNil | Skip s' ⇒ lunstream s' | Yield x s' ⇒ LCons x (lunstream s'))"
declare lunstream.simps[code]
lemma lunstream_simps:
"g s = Done ⟹ lunstream s = LNil"
"g s = Skip s' ⟹ lunstream s = lunstream s'"
"g s = Yield x s' ⟹ lunstream s = LCons x (lunstream s')"
by(simp_all add: lunstream.simps)
lemma lunstream_sels:
shows lnull_lunstream: "lnull (lunstream s) ⟷
(case g s of Done ⇒ True | Skip s' ⇒ lnull (lunstream s') | Yield _ _ ⇒ False)"
and lhd_lunstream: "lhd (lunstream s) =
(case g s of Skip s' ⇒ lhd (lunstream s') | Yield x _ ⇒ x)"
and ltl_lunstream: "ltl (lunstream s) =
(case g s of Done ⇒ LNil | Skip s' ⇒ ltl (lunstream s') | Yield _ s' ⇒ lunstream s')"
by(simp_all add: lhd_def lunstream_simps split: step.split)
end
subsubsection ‹Finitely many consecutive @{term Skip}s›
lift_definition lunstream' :: "('a, 's) lgenerator' ⇒ 's ⇒ 'a llist"
is lunstream .
lemma lunstream'_simps:
"lgenerator g s = Done ⟹ lunstream' g s = LNil"
"lgenerator g s = Skip s' ⟹ lunstream' g s = lunstream' g s'"
"lgenerator g s = Yield x s' ⟹ lunstream' g s = LCons x (lunstream' g s')"
by(transfer, simp add: lunstream_simps)+
lemma lunstream'_sels:
shows lnull_lunstream': "lnull (lunstream' g s) ⟷
(case lgenerator g s of Done ⇒ True | Skip s' ⇒ lnull (lunstream' g s') | Yield _ _ ⇒ False)"
and lhd_lunstream': "lhd (lunstream' g s) =
(case lgenerator g s of Skip s' ⇒ lhd (lunstream' g s') | Yield x _ ⇒ x)"
and ltl_lunstream': "ltl (lunstream' g s) =
(case lgenerator g s of Done ⇒ LNil | Skip s' ⇒ ltl (lunstream' g s') | Yield _ s' ⇒ lunstream' g s')"
by(transfer, simp add: lunstream_sels)+
setup ‹Context.theory_map (fold
Stream_Fusion.add_unstream [@{const_name lunstream}, @{const_name lunstream'}])›
subsection ‹Producers›
subsubsection ‹Conversion to streams›
fun lstream :: "('a, 'a llist) lgenerator"
where
"lstream LNil = Done"
| "lstream (LCons x xs) = Yield x xs"
lemma case_lstream_conv_case_llist:
"(case lstream xs of Done ⇒ done | Skip xs' ⇒ skip xs' | Yield x xs' ⇒ yield x xs') =
(case xs of LNil ⇒ done | LCons x xs' ⇒ yield x xs')"
by(simp split: llist.split)
lemma mcont2mcont_lunstream[THEN llist.mcont2mcont, simp, cont_intro]:
shows mcont_lunstream: "mcont lSup lprefix lSup lprefix (lunstream lstream)"
by(rule llist.fixp_preserves_mcont1[OF lunstream.mono lunstream_def])(simp add: case_lstream_conv_case_llist)
lemma lunstream_lstream: "lunstream lstream xs = xs"
by(induction xs)(simp_all add: lunstream_simps)
lift_definition lstream' :: "('a, 'a llist) lgenerator'"
is lstream
proof
fix s :: "'a llist"
show "s ∈ productive_on lstream" by(cases s)(auto intro: productive_on.intros)
qed
lemma lunstream'_lstream: "lunstream' lstream' xs = xs"
by(transfer)(rule lunstream_lstream)
subsubsection ‹@{const iterates}›
definition iterates_raw :: "('a ⇒ 'a) ⇒ ('a, 'a) lgenerator"
where "iterates_raw f s = Yield s (f s)"
lemma lunstream_iterates_raw: "lunstream (iterates_raw f) x = iterates f x"
by(coinduction arbitrary: x)(auto simp add: iterates_raw_def lunstream_sels)
lift_definition iterates_prod :: "('a ⇒ 'a) ⇒ ('a, 'a) lgenerator'" is iterates_raw
by(auto 4 3 intro: productiveI productive_on.intros simp add: iterates_raw_def)
lemma lunstream'_iterates_prod [stream_fusion]: "lunstream' (iterates_prod f) x = iterates f x"
by transfer(rule lunstream_iterates_raw)
subsubsection ‹@{const unfold_llist}›
definition unfold_llist_raw :: "('a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'a) ⇒ ('b, 'a) lgenerator"
where
"unfold_llist_raw stop head tail s = (if stop s then Done else Yield (head s) (tail s))"
lemma lunstream_unfold_llist_raw:
"lunstream (unfold_llist_raw stop head tail) s = unfold_llist stop head tail s"
by(coinduction arbitrary: s)(auto simp add: lunstream_sels unfold_llist_raw_def)
lift_definition unfold_llist_prod :: "('a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'a) ⇒ ('b, 'a) lgenerator'"
is unfold_llist_raw
proof(rule productiveI)
fix stop and head :: "'a ⇒ 'b" and tail s
show "s ∈ productive_on (unfold_llist_raw stop head tail)"
by(cases "stop s")(auto intro: productive_on.intros simp add: unfold_llist_raw_def)
qed
lemma lunstream'_unfold_llist_prod [stream_fusion]:
"lunstream' (unfold_llist_prod stop head tail) s = unfold_llist stop head tail s"
by transfer(rule lunstream_unfold_llist_raw)
subsubsection ‹@{const inf_llist}›
definition inf_llist_raw :: "(nat ⇒ 'a) ⇒ ('a, nat) lgenerator"
where "inf_llist_raw f n = Yield (f n) (Suc n)"
lemma lunstream_inf_llist_raw: "lunstream (inf_llist_raw f) n = ldropn n (inf_llist f)"
by(coinduction arbitrary: n)(auto simp add: lunstream_sels inf_llist_raw_def)
lift_definition inf_llist_prod :: "(nat ⇒ 'a) ⇒ ('a, nat) lgenerator'" is inf_llist_raw
by(auto 4 3 intro: productiveI productive_on.intros simp add: inf_llist_raw_def)
lemma inf_llist_prod_fusion [stream_fusion]:
"lunstream' (inf_llist_prod f) 0 = inf_llist f"
by transfer(simp add: lunstream_inf_llist_raw)
subsection ‹Consumers›
subsubsection ‹@{const lhd}›
context fixes g :: "('a, 's) lgenerator" begin
definition lhd_cons :: "'s ⇒ 'a"
where [stream_fusion]: "lhd_cons s = lhd (lunstream g s)"
lemma lhd_cons_code[code]:
"lhd_cons s = (case g s of Done ⇒ undefined | Skip s' ⇒ lhd_cons s' | Yield x _ ⇒ x)"
by(simp add: lhd_cons_def lunstream_simps lhd_def split: step.split)
end
lemma lhd_cons_fusion2 [stream_fusion]:
"lhd_cons (lgenerator g) s = lhd (lunstream' g s)"
by transfer(rule lhd_cons_def)
subsubsection ‹@{const llength}›
context fixes g :: "('a, 's) lgenerator" begin
definition gen_llength_cons :: "enat ⇒ 's ⇒ enat"
where "gen_llength_cons n s = n + llength (lunstream g s)"
lemma gen_llength_cons_code [code]:
"gen_llength_cons n s = (case g s of
Done ⇒ n | Skip s' ⇒ gen_llength_cons n s' | Yield _ s' ⇒ gen_llength_cons (eSuc n) s')"
by(simp add: gen_llength_cons_def lunstream_simps iadd_Suc_right iadd_Suc split: step.split)
lemma gen_llength_cons_fusion [stream_fusion]:
"gen_llength_cons 0 s = llength (lunstream g s)"
by(simp add: gen_llength_cons_def)
end
context fixes g :: "('a, 's) lgenerator'" begin
definition gen_llength_cons' :: "enat ⇒ 's ⇒ enat"
where "gen_llength_cons' = gen_llength_cons (lgenerator g)"
lemma gen_llength_cons'_code [code]:
"gen_llength_cons' n s = (case lgenerator g s of
Done ⇒ n | Skip s' ⇒ gen_llength_cons' n s' | Yield _ s' ⇒ gen_llength_cons' (eSuc n) s')"
by(simp add: gen_llength_cons'_def cong: step.case_cong)(rule gen_llength_cons_code)
lemma gen_llength_cons'_fusion [stream_fusion]:
"gen_llength_cons' 0 s = llength (lunstream' g s)"
by(simp add: gen_llength_cons'_def gen_llength_cons_fusion lunstream'.rep_eq)
end
subsubsection ‹@{const lnull}›
context fixes g :: "('a, 's) lgenerator" begin
definition lnull_cons :: "'s ⇒ bool"
where [stream_fusion]: "lnull_cons s ⟷ lnull (lunstream g s)"
lemma lnull_cons_code [code]:
"lnull_cons s ⟷ (case g s of
Done ⇒ True | Skip s' ⇒ lnull_cons s' | Yield _ _ ⇒ False)"
by(simp add: lnull_cons_def lunstream_simps split: step.split)
end
context fixes g :: "('a, 's) lgenerator'" begin
definition lnull_cons' :: "'s ⇒ bool"
where "lnull_cons' = lnull_cons (lgenerator g)"
lemma lnull_cons'_code [code]:
"lnull_cons' s ⟷ (case lgenerator g s of
Done ⇒ True | Skip s' ⇒ lnull_cons' s' | Yield _ _ ⇒ False)"
by(simp add: lnull_cons'_def cong: step.case_cong)(rule lnull_cons_code)
lemma lnull_cons'_fusion [stream_fusion]:
"lnull_cons' s ⟷ lnull (lunstream' g s)"
by(simp add: lnull_cons'_def lnull_cons_def lunstream'.rep_eq)
end
subsubsection ‹@{const llist_all2}›
context
fixes g :: "('a, 'sg) lgenerator"
and h :: "('b, 'sh) lgenerator"
and P :: "'a ⇒ 'b ⇒ bool"
begin
definition llist_all2_cons :: "'sg ⇒ 'sh ⇒ bool"
where [stream_fusion]: "llist_all2_cons sg sh ⟷ llist_all2 P (lunstream g sg) (lunstream h sh)"
definition llist_all2_cons1 :: "'a ⇒ 'sg ⇒ 'sh ⇒ bool"
where "llist_all2_cons1 x sg' sh = llist_all2 P (LCons x (lunstream g sg')) (lunstream h sh)"
lemma llist_all2_cons_code [code]:
"llist_all2_cons sg sh =
(case g sg of
Done ⇒ lnull_cons h sh
| Skip sg' ⇒ llist_all2_cons sg' sh
| Yield a sg' ⇒ llist_all2_cons1 a sg' sh)"
by(simp split: step.split add: llist_all2_cons_def lnull_cons_def llist_all2_cons1_def lunstream_simps lnull_def)
lemma llist_all2_cons1_code [code]:
"llist_all2_cons1 x sg' sh =
(case h sh of
Done ⇒ False
| Skip sh' ⇒ llist_all2_cons1 x sg' sh'
| Yield y sh' ⇒ P x y ∧ llist_all2_cons sg' sh')"
by(simp split: step.split add: llist_all2_cons_def lnull_cons_def lnull_def llist_all2_cons1_def lunstream_simps)
end
lemma llist_all2_cons_fusion2 [stream_fusion]:
"llist_all2_cons (lgenerator g) (lgenerator h) P sg sh ⟷ llist_all2 P (lunstream' g sg) (lunstream' h sh)"
by transfer(rule llist_all2_cons_def)
lemma llist_all2_cons_fusion3 [stream_fusion]:
"llist_all2_cons g (lgenerator h) P sg sh ⟷ llist_all2 P (lunstream g sg) (lunstream' h sh)"
by transfer(rule llist_all2_cons_def)
lemma llist_all2_cons_fusion4 [stream_fusion]:
"llist_all2_cons (lgenerator g) h P sg sh ⟷ llist_all2 P (lunstream' g sg) (lunstream h sh)"
by transfer(rule llist_all2_cons_def)
subsubsection ‹@{const lnth}›
context fixes g :: "('a, 's) lgenerator" begin
definition lnth_cons :: "nat ⇒ 's ⇒ 'a"
where [stream_fusion]: "lnth_cons n s = lnth (lunstream g s) n"
lemma lnth_cons_code [code]:
"lnth_cons n s = (case g s of
Done ⇒ undefined n
| Skip s' ⇒ lnth_cons n s'
| Yield x s' ⇒ (if n = 0 then x else lnth_cons (n - 1) s'))"
by(cases n)(simp_all add: lnth_cons_def lunstream_simps lnth_LNil split: step.split)
end
lemma lnth_cons_fusion2 [stream_fusion]:
"lnth_cons (lgenerator g) n s = lnth (lunstream' g s) n"
by transfer(rule lnth_cons_def)
subsubsection ‹@{const lprefix}›
context
fixes g :: "('a, 'sg) lgenerator"
and h :: "('a, 'sh) lgenerator"
begin
definition lprefix_cons :: "'sg ⇒ 'sh ⇒ bool"
where [stream_fusion]: "lprefix_cons sg sh ⟷ lprefix (lunstream g sg) (lunstream h sh)"
definition lprefix_cons1 :: "'a ⇒ 'sg ⇒ 'sh ⇒ bool"
where "lprefix_cons1 x sg' sh ⟷ lprefix (LCons x (lunstream g sg')) (lunstream h sh)"
lemma lprefix_cons_code [code]:
"lprefix_cons sg sh ⟷ (case g sg of
Done ⇒ True | Skip sg' ⇒ lprefix_cons sg' sh | Yield x sg' ⇒ lprefix_cons1 x sg' sh)"
by(simp add: lprefix_cons_def lprefix_cons1_def lunstream_simps split: step.split)
lemma lprefix_cons1_code [code]:
"lprefix_cons1 x sg' sh ⟷ (case h sh of
Done ⇒ False | Skip sh' ⇒ lprefix_cons1 x sg' sh'
| Yield y sh' ⇒ x = y ∧ lprefix_cons sg' sh')"
by(simp add: lprefix_cons_def lprefix_cons1_def lunstream_simps split: step.split)
end
lemma lprefix_cons_fusion2 [stream_fusion]:
"lprefix_cons (lgenerator g) (lgenerator h) sg sh ⟷ lprefix (lunstream' g sg) (lunstream' h sh)"
by transfer(rule lprefix_cons_def)
lemma lprefix_cons_fusion3 [stream_fusion]:
"lprefix_cons g (lgenerator h) sg sh ⟷ lprefix (lunstream g sg) (lunstream' h sh)"
by transfer(rule lprefix_cons_def)
lemma lprefix_cons_fusion4 [stream_fusion]:
"lprefix_cons (lgenerator g) h sg sh ⟷ lprefix (lunstream' g sg) (lunstream h sh)"
by transfer(rule lprefix_cons_def)
subsection ‹Transformers›
subsubsection ‹@{const lmap}›
definition lmap_trans :: "('a ⇒ 'b) ⇒ ('a, 's) lgenerator ⇒ ('b, 's) lgenerator"
where "lmap_trans = map_raw"
lemma lunstream_lmap_trans [stream_fusion]: fixes f g s
defines [simp]: "g' ≡ lmap_trans f g"
shows "lunstream g' s = lmap f (lunstream g s)" (is "?lhs = ?rhs")
proof(rule lprefix_antisym)
show "lprefix ?lhs ?rhs"
proof(induction g' arbitrary: s rule: lunstream.fixp_induct)
case (3 lunstream_g')
then show ?case
by(cases "g s")(simp_all add: lmap_trans_def map_raw_def lunstream_simps)
qed simp_all
next
note [cont_intro] = ccpo.admissible_leI[OF llist_ccpo]
show "lprefix ?rhs ?lhs"
proof(induction g arbitrary: s rule: lunstream.fixp_induct)
case (3 lunstream_g)
thus ?case by(cases "g s")(simp_all add: lmap_trans_def map_raw_def lunstream_simps)
qed simp_all
qed
lift_definition lmap_trans' :: "('a ⇒ 'b) ⇒ ('a, 's) lgenerator' ⇒ ('b, 's) lgenerator'"
is lmap_trans
proof
fix f :: "'a ⇒ 'b" and g :: "('a, 's) lgenerator" and s
assume "productive g"
hence "s ∈ productive_on g" ..
thus "s ∈ productive_on (lmap_trans f g)"
by induction(auto simp add: lmap_trans_def map_raw_def intro: productive_on.intros)
qed
lemma lunstream'_lmap_trans' [stream_fusion]:
"lunstream' (lmap_trans' f g) s = lmap f (lunstream' g s)"
by transfer(rule lunstream_lmap_trans)
subsubsection ‹@{const ltake}›
fun ltake_trans :: "('a, 's) lgenerator ⇒ ('a, (enat × 's)) lgenerator"
where
"ltake_trans g (n, s) =
(if n = 0 then Done else case g s of
Done ⇒ Done | Skip s' ⇒ Skip (n, s') | Yield a s' ⇒ Yield a (epred n, s'))"
lemma ltake_trans_fusion [stream_fusion]:
fixes g' g
defines [simp]: "g' ≡ ltake_trans g"
shows "lunstream g' (n, s) = ltake n (lunstream g s)" (is "?lhs = ?rhs")
proof(rule lprefix_antisym)
show "lprefix ?lhs ?rhs"
proof(induction g' arbitrary: n s rule: lunstream.fixp_induct)
case (3 lunstream_g')
thus ?case
by(cases "g s")(auto simp add: lunstream_simps neq_zero_conv_eSuc)
qed simp_all
show "lprefix ?rhs ?lhs"
proof(induction g arbitrary: s n rule: lunstream.fixp_induct)
case (3 lunstream_g)
thus ?case by(cases "g s" n rule: step.exhaust[case_product enat_coexhaust])(auto simp add: lunstream_simps)
qed simp_all
qed
lift_definition ltake_trans' :: "('a, 's) lgenerator' ⇒ ('a, (enat × 's)) lgenerator'"
is "ltake_trans"
proof
fix g :: "('a, 's) lgenerator" and s :: "enat × 's"
obtain n sg where s: "s = (n, sg)" by(cases s)
assume "productive g"
hence "sg ∈ productive_on g" ..
then show "s ∈ productive_on (ltake_trans g)" unfolding ‹s = (n, sg)›
apply(induction arbitrary: n)
apply(case_tac [!] n rule: enat_coexhaust)
apply(auto intro: productive_on.intros)
done
qed
lemma ltake_trans'_fusion [stream_fusion]:
"lunstream' (ltake_trans' g) (n, s) = ltake n (lunstream' g s)"
by transfer(rule ltake_trans_fusion)
subsubsection ‹@{const ldropn}›
abbreviation (input) ldropn_trans :: "('b, 'a) lgenerator ⇒ ('b, nat × 'a) lgenerator"
where "ldropn_trans ≡ drop_raw"
lemma ldropn_trans_fusion [stream_fusion]:
fixes g defines [simp]: "g' ≡ ldropn_trans g"
shows "lunstream g' (n, s) = ldropn n (lunstream g s)" (is "?lhs = ?rhs")
proof(rule lprefix_antisym)
show "lprefix ?lhs ?rhs"
proof(induction g' arbitrary: n s rule: lunstream.fixp_induct)
case (3 lunstream_g')
thus ?case
by(cases "g s" n rule: step.exhaust[case_product nat.exhaust])
(auto simp add: lunstream_simps elim: meta_allE[where x=0])
qed simp_all
note [cont_intro] = ccpo.admissible_leI[OF llist_ccpo]
show "lprefix ?rhs ?lhs"
proof(induction g arbitrary: n s rule: lunstream.fixp_induct)
case (3 lunstream_g)
thus ?case by(cases n)(auto split: step.split simp add: lunstream_simps elim: meta_allE[where x=0])
qed simp_all
qed
lift_definition ldropn_trans' :: "('a, 's) lgenerator' ⇒ ('a, nat × 's) lgenerator'"
is ldropn_trans
proof
fix g :: "('a, 's) lgenerator" and ns :: "nat × 's"
obtain n s where ns: "ns = (n, s)" by(cases ns)
assume g: "productive g"
show "ns ∈ productive_on (ldropn_trans g)" unfolding ns
proof(induction n arbitrary: s)
case 0
from g have "s ∈ productive_on g" ..
thus ?case by induction(auto intro: productive_on.intros)
next
case (Suc n)
from g have "s ∈ productive_on g" ..
thus ?case by induction(auto intro: productive_on.intros Suc.IH)
qed
qed
lemma ldropn_trans'_fusion [stream_fusion]:
"lunstream' (ldropn_trans' g) (n, s) = ldropn n (lunstream' g s)"
by transfer(rule ldropn_trans_fusion)
subsubsection ‹@{const ldrop}›
fun ldrop_trans :: "('a, 's) lgenerator ⇒ ('a, enat × 's) lgenerator"
where
"ldrop_trans g (n, s) = (case g s of
Done ⇒ Done | Skip s' ⇒ Skip (n, s')
| Yield x s' ⇒ (if n = 0 then Yield x (n, s') else Skip (epred n, s')))"
lemma ldrop_trans_fusion [stream_fusion]:
fixes g g' defines [simp]: "g' ≡ ldrop_trans g"
shows "lunstream g' (n, s) = ldrop n (lunstream g s)" (is "?lhs = ?rhs")
proof(rule lprefix_antisym)
show "lprefix ?lhs ?rhs"
by(induction g' arbitrary: n s rule: lunstream.fixp_induct)
(auto simp add: lunstream_simps neq_zero_conv_eSuc elim: meta_allE[where x=0] split: step.split)
show "lprefix ?rhs ?lhs"
proof(induction g arbitrary: n s rule: lunstream.fixp_induct)
case (3 lunstream_g)
thus ?case
by(cases n rule: enat_coexhaust)(auto simp add: lunstream_simps split: step.split elim: meta_allE[where x=0])
qed simp_all
qed
lemma ldrop_trans_fusion2 [stream_fusion]:
"lunstream (ldrop_trans (lgenerator g)) (n, s) = ldrop n (lunstream' g s)"
by transfer (rule ldrop_trans_fusion)
subsubsection ‹@{const ltakeWhile}›
abbreviation (input) ltakeWhile_trans :: "('a ⇒ bool) ⇒ ('a, 's) lgenerator ⇒ ('a, 's) lgenerator"
where "ltakeWhile_trans ≡ takeWhile_raw"
lemma ltakeWhile_trans_fusion [stream_fusion]:
fixes P g g' defines [simp]: "g' ≡ ltakeWhile_trans P g"
shows "lunstream g' s = ltakeWhile P (lunstream g s)" (is "?lhs = ?rhs")
proof(rule lprefix_antisym)
show "lprefix ?lhs ?rhs"
by(induction g' arbitrary: s rule: lunstream.fixp_induct)(auto simp add: lunstream_simps takeWhile_raw_def split: step.split)
show "lprefix ?rhs ?lhs"
by(induction g arbitrary: s rule: lunstream.fixp_induct)(auto split: step.split simp add: lunstream_simps takeWhile_raw_def)
qed
lift_definition ltakeWhile_trans' :: "('a ⇒ bool) ⇒ ('a, 's) lgenerator' ⇒ ('a, 's) lgenerator'"
is ltakeWhile_trans
proof
fix P and g :: "('a, 's) lgenerator" and s
assume "productive g"
hence "s ∈ productive_on g" ..
thus "s ∈ productive_on (ltakeWhile_trans P g)"
apply(induction)
apply(case_tac [3] "P x")
apply(auto intro: productive_on.intros simp add: takeWhile_raw_def)
done
qed
lemma ltakeWhile_trans'_fusion [stream_fusion]:
"lunstream' (ltakeWhile_trans' P g) s = ltakeWhile P (lunstream' g s)"
by transfer(rule ltakeWhile_trans_fusion)
subsubsection ‹@{const ldropWhile}›
abbreviation (input) ldropWhile_trans :: "('a ⇒ bool) ⇒ ('a, 'b) lgenerator ⇒ ('a, bool × 'b) lgenerator"
where "ldropWhile_trans ≡ dropWhile_raw"
lemma ldropWhile_trans_fusion [stream_fusion]:
fixes P g g' defines [simp]: "g' ≡ ldropWhile_trans P g"
shows "lunstream g' (True, s) = ldropWhile P (lunstream g s)" (is "?lhs = ?rhs")
proof -
have "lprefix ?lhs ?rhs" "lprefix (lunstream g' (False, s)) (lunstream g s)"
by(induction g' arbitrary: s rule: lunstream.fixp_induct)(simp_all add: lunstream_simps split: step.split)
moreover have "lprefix ?rhs ?lhs" "lprefix (lunstream g s) (lunstream g' (False, s))"
by(induction g arbitrary: s rule: lunstream.fixp_induct)(simp_all add: lunstream_simps split: step.split)
ultimately show ?thesis by(blast intro: lprefix_antisym)
qed
lemma ldropWhile_trans_fusion2 [stream_fusion]:
"lunstream (ldropWhile_trans P (lgenerator g)) (True, s) = ldropWhile P (lunstream' g s)"
by transfer(rule ldropWhile_trans_fusion)
subsubsection ‹@{const lzip}›
abbreviation (input) lzip_trans :: "('a, 's1) lgenerator ⇒ ('b, 's2) lgenerator ⇒ ('a × 'b, 's1 × 's2 × 'a option) lgenerator"
where "lzip_trans ≡ zip_raw"
lemma lzip_trans_fusion [stream_fusion]:
fixes g h gh defines [simp]: "gh ≡ lzip_trans g h"
shows "lunstream gh (sg, sh, None) = lzip (lunstream g sg) (lunstream h sh)"
(is "?lhs = ?rhs")
proof -
have "lprefix ?lhs ?rhs"
and "⋀x. lprefix (lunstream gh (sg, sh, Some x)) (lzip (LCons x (lunstream g sg)) (lunstream h sh))"
proof(induction gh arbitrary: sg sh rule: lunstream.fixp_induct)
case (3 lunstream)
{ case 1 show ?case using 3
by(cases "g sg")(simp_all add: lunstream_simps) }
{ case 2 show ?case using 3
by(cases "h sh")(simp_all add: lunstream_simps) }
qed simp_all
moreover
note [cont_intro] = ccpo.admissible_leI[OF llist_ccpo]
have "lprefix ?rhs ?lhs"
and "⋀x. lprefix (lzip (LCons x (lunstream g sg)) (lunstream h sh)) (lunstream gh (sg, sh, Some x))"
proof(induction g arbitrary: sg sh rule: lunstream.fixp_induct)
case (3 lunstream_g)
note IH = "3.IH"
{ case 1 show ?case using 3
by(cases "g sg")(simp_all add: lunstream_simps fun_ord_def) }
{ case 2 show ?case
proof(induction h arbitrary: sh sg x rule: lunstream.fixp_induct)
case (3 unstream_h)
thus ?case
proof(cases "h sh")
case (Yield y sh')
thus ?thesis using "3.prems" IH "3.hyps"
by(cases "g sg")(auto 4 3 simp add: lunstream_simps fun_ord_def intro: monotone_lzip2[THEN monotoneD] lprefix_trans)
qed(simp_all add: lunstream_simps)
qed simp_all }
next
case 2 case 2
show ?case
by(induction h arbitrary: sh rule: lunstream.fixp_induct)(simp_all add: lunstream_simps split: step.split)
qed simp_all
ultimately show ?thesis by(blast intro: lprefix_antisym)
qed
lemma lzip_trans_fusion2 [stream_fusion]:
"lunstream (lzip_trans (lgenerator g) h) (sg, sh, None) = lzip (lunstream' g sg) (lunstream h sh)"
by transfer(rule lzip_trans_fusion)
lemma lzip_trans_fusion3 [stream_fusion]:
"lunstream (lzip_trans g (lgenerator h)) (sg, sh, None) = lzip (lunstream g sg) (lunstream' h sh)"
by transfer(rule lzip_trans_fusion)
lift_definition lzip_trans' :: "('a, 's1) lgenerator' ⇒ ('b, 's2) lgenerator' ⇒ ('a × 'b, 's1 × 's2 × 'a option) lgenerator'"
is "lzip_trans"
proof
fix g :: "('a, 's1) lgenerator" and h :: "('b, 's2) lgenerator" and s :: "'s1 × 's2 × 'a option"
assume "productive g" and "productive h"
obtain sg sh mx where s: "s = (sg, sh, mx)" by(cases s)
{ fix x sg
from ‹productive h› have "sh ∈ productive_on h" ..
hence "(sg, sh, Some x) ∈ productive_on (lzip_trans g h)"
by(induction)(auto simp add: intro: productive_on.intros) }
moreover
from ‹productive g› have "sg ∈ productive_on g" ..
then have "(sg, sh, None) ∈ productive_on (lzip_trans g h)"
by induction(auto intro: productive_on.intros calculation)
ultimately show "s ∈ productive_on (lzip_trans g h)" unfolding s
by(cases mx) auto
qed
lemma lzip_trans'_fusion [stream_fusion]:
"lunstream' (lzip_trans' g h) (sg, sh, None) = lzip (lunstream' g sg) (lunstream' h sh)"
by transfer(rule lzip_trans_fusion)
subsubsection ‹@{const lappend}›
lift_definition lappend_trans :: "('a, 'sg) lgenerator' ⇒ ('a, 'sh) lgenerator ⇒ 'sh ⇒ ('a, 'sg + 'sh) lgenerator"
is append_raw .
lemma lunstream_append_raw:
fixes g h sh gh defines [simp]: "gh ≡ append_raw g h sh"
assumes "productive g"
shows "lunstream gh (Inl sg) = lappend (lunstream g sg) (lunstream h sh)"
proof(coinduction arbitrary: sg rule: llist.coinduct_strong)
case (Eq_llist sg)
{ fix sh'
have "lprefix (lunstream gh (Inr sh')) (lunstream h sh')"
by(induction gh arbitrary: sh' rule: lunstream.fixp_induct)(simp_all add: lunstream_simps split: step.split)
moreover have "lprefix (lunstream h sh') (lunstream gh (Inr sh'))"
by(induction h arbitrary: sh' rule: lunstream.fixp_induct)(simp_all add: lunstream_simps split: step.split)
ultimately have "lunstream gh (Inr sh') = lunstream h sh'"
by(blast intro: lprefix_antisym) }
note Inr = this[unfolded gh_def]
from ‹productive g› have sg: "sg ∈ productive_on g" ..
then show ?case by induction(auto simp add: lunstream_sels Inr)
qed
lemma lappend_trans_fusion [stream_fusion]:
"lunstream (lappend_trans g h sh) (Inl sg) = lappend (lunstream' g sg) (lunstream h sh)"
by transfer(rule lunstream_append_raw)
lift_definition lappend_trans' :: "('a, 'sg) lgenerator' ⇒ ('a, 'sh) lgenerator' ⇒ 'sh ⇒ ('a, 'sg + 'sh) lgenerator'"
is append_raw
proof
fix g :: "('a, 'sg) lgenerator" and h :: "('a, 'sh) lgenerator" and sh s
assume "productive g" "productive h"
{ fix sh'
from ‹productive h› have "sh' ∈ productive_on h" ..
then have "Inr sh' ∈ productive_on (append_raw g h sh)"
by induction (auto intro: productive_on.intros)
} moreover {
fix sg
from ‹productive g› have "sg ∈ productive_on g" ..
then have "Inl sg ∈ productive_on (append_raw g h sh)"
by induction(auto intro: productive_on.intros calculation) }
ultimately show "s ∈ productive_on (append_raw g h sh)" by(cases s) auto
qed
lemma lappend_trans'_fusion [stream_fusion]:
"lunstream' (lappend_trans' g h sh) (Inl sg) = lappend (lunstream' g sg) (lunstream' h sh)"
by transfer(rule lunstream_append_raw)
subsubsection ‹@{const lfilter}›
definition lfilter_trans :: "('a ⇒ bool) ⇒ ('a, 's) lgenerator ⇒ ('a, 's) lgenerator"
where "lfilter_trans = filter_raw"
lemma lunstream_lfilter_trans [stream_fusion]:
fixes P g g' defines [simp]: "g' ≡ lfilter_trans P g"
shows "lunstream g' s = lfilter P (lunstream g s)" (is "?lhs = ?rhs")
proof(rule lprefix_antisym)
show "lprefix ?lhs ?rhs"
by(induction g' arbitrary: s rule: lunstream.fixp_induct)
(simp_all add: lfilter_trans_def filter_raw_def lunstream_simps split: step.split)
show "lprefix ?rhs ?lhs"
by(induction g arbitrary: s rule: lunstream.fixp_induct)
(simp_all add: lfilter_trans_def filter_raw_def lunstream_simps split: step.split)
qed
lemma lunstream_lfilter_trans2 [stream_fusion]:
"lunstream (lfilter_trans P (lgenerator g)) s = lfilter P (lunstream' g s)"
by transfer(rule lunstream_lfilter_trans)
subsubsection ‹@{const llist_of}›
lift_definition llist_of_trans :: "('a, 's) generator ⇒ ('a, 's) lgenerator'"
is "λx. x"
proof
fix g :: "('a, 's) raw_generator" and s
assume "terminates g"
hence "s ∈ terminates_on g" by(simp add: terminates_def)
then show "s ∈ productive_on g"
by(induction)(auto intro: productive_on.intros)
qed
lemma lunstream_llist_of_trans [stream_fusion]:
"lunstream' (llist_of_trans g) s = llist_of (unstream g s)"
apply(induction s taking: g rule: unstream.induct)
apply(rule llist.expand)
apply(auto intro: llist.expand simp add: llist_of_trans.rep_eq lunstream_sels lunstream'.rep_eq split: step.split)
done
text ‹We cannot define a stream version of @{const list_of} because we would have to test
for finiteness first and therefore traverse the list twice.›
end