Theory TLList_CCPO_Examples

(*  Title:       TLList_CCPO_Examples.thy
    Author:      Andreas Lochbihler, ETH Zurich
*)

section ‹Example definitions using the CCPO structure on terminated lazy lists›

theory TLList_CCPO_Examples imports
   "../TLList_CCPO"
begin

context fixes b :: 'b begin
interpretation tllist_pf b .

context fixes P :: "'a ⇒ bool"
  notes [[function_internals]]
begin

partial_function (tllist) tfilter :: "('a, 'b) tllist ⇒ ('a, 'b) tllist"
where
  "tfilter xs = (case xs of TNil b' ⇒ TNil b' | TCons x xs' ⇒ if P x then TCons x (tfilter xs') else tfilter xs')"

end

simps_of_case tfilter_simps [simp]: tfilter.simps

lemma is_TNil_tfilter: "is_TNil (tfilter P xs) ⟷ (∀x ∈ tset xs. ¬ P x)" (is "?lhs ⟷ ?rhs")
proof(rule iffI ballI)+
  fix x
  assume "x ∈ tset xs" ?lhs
  thus "¬ P x"
  proof(induct rule: tllist_set_induct)
    case (find xs)
    thus ?case by(cases xs)(simp_all split: if_split_asm)
  next
    case (step xs x)
    thus ?case by(cases xs)(simp_all split: if_split_asm)
  qed
next
  assume ?rhs
  thus ?lhs
    by(induct arbitrary: xs rule: tfilter.fixp_induct)(simp_all split: tllist.split)
qed

end

lemma mcont2mcont_tfilter[THEN tllist.mcont2mcont, simp, cont_intro]:
  shows mcont_tfilter: "mcont (tSup b) (tllist_ord b) (tSup b) (tllist_ord b) (tfilter b P)"
apply(rule tllist.fixp_preserves_mcont1[OF tfilter.mono tfilter_def])
apply(rule mcont_lprefix_case_aux)
apply simp_all
done

lemma tfilter_tfilter:
  "tfilter b P (tfilter b Q xs) = tfilter b (λx. P x ∧ Q x) xs" (is "?lhs xs = ?rhs xs")
proof(rule tllist.leq_antisym)
  have "∀xs. tllist_ord b (?lhs xs) (?rhs xs)"
    by(rule tfilter.fixp_induct[where Pa="λf. ∀xs. tllist_ord b (tfilter b P (f xs)) (?rhs xs)"])(auto split: tllist.split)
  thus "tllist_ord b (?lhs xs) (?rhs xs)" ..

  have "∀xs. tllist_ord b (?rhs xs) (?lhs xs)"
    by(rule tfilter.fixp_induct[where Pa="λf. ∀xs. tllist_ord b (f xs) (?lhs xs)"])(auto split: tllist.split)
  thus "tllist_ord b (?rhs xs) (?lhs xs)" ..
qed

declare ccpo.admissible_leI[OF complete_lattice_ccpo, cont_intro, simp]

lemma tset_tfilter: "tset (tfilter b P xs) = {x∈tset xs. P x}"
proof(rule equalityI[OF _ subsetI])
  show "tset (tfilter b P xs) ⊆ {x ∈ tset xs. P x}"
    by(induct arbitrary: xs rule: tfilter.fixp_induct)(auto split: tllist.split)
  fix x
  assume "x ∈ {x ∈ tset xs. P x}"
  hence "x ∈ tset xs" "P x" by simp_all
  thus "x ∈ tset (tfilter b P xs)"
    by(induct rule: tset_induct) simp_all
qed

context fixes b :: 'b begin
interpretation tllist_pf b .

partial_function (tllist) tconcat :: "('a llist, 'b) tllist ⇒ ('a, 'b) tllist"
where
  "tconcat xs = (case xs of TNil b ⇒ TNil b | TCons x xs' ⇒ lappendt x (tconcat xs'))"

end

simps_of_case tconcat2_simps [simp]: tconcat.simps

end