Theory TLList_CCPO
section ‹Ccpo structure for terminated lazy lists›
theory TLList_CCPO imports TLList begin
lemma Set_is_empty_parametric [transfer_rule]:
includes lifting_syntax
shows "(rel_set A ===> (=)) Set.is_empty Set.is_empty"
by(auto simp add: rel_fun_def Set.is_empty_def dest: rel_setD1 rel_setD2)
lemma monotone_comp: "⟦ monotone orda ordb g; monotone ordb ordc f ⟧ ⟹ monotone orda ordc (f ∘ g)"
by(rule monotoneI)(simp add: monotoneD)
lemma cont_comp: "⟦ mcont luba orda lubb ordb g; cont lubb ordb lubc ordc f ⟧ ⟹ cont luba orda lubc ordc (f ∘ g)"
apply(rule contI)
apply(frule (2) mcont_contD)
apply(simp)
apply(drule (1) contD[OF _ chain_imageI])
apply(erule (1) mcont_monoD)
apply(simp_all add: image_image o_def)
done
lemma mcont_comp: "⟦ mcont luba orda lubb ordb g; mcont lubb ordb lubc ordc f ⟧ ⟹ mcont luba orda lubc ordc (f ∘ g)"
by(auto simp add: mcont_def intro: cont_comp monotone_comp)
context includes lifting_syntax
begin
lemma monotone_parametric [transfer_rule]:
assumes [transfer_rule]: "bi_total A"
shows "((A ===> A ===> (=)) ===> (B ===> B ===> (=)) ===> (A ===> B) ===> (=)) monotone monotone"
unfolding monotone_def[abs_def] by transfer_prover
lemma cont_parametric [transfer_rule]:
assumes [transfer_rule]: "bi_total A" "bi_unique B"
shows "((rel_set A ===> A) ===> (A ===> A ===> (=)) ===> (rel_set B ===> B) ===> (B ===> B ===> (=)) ===> (A ===> B) ===> (=)) cont cont"
unfolding cont_def[abs_def] Set.is_empty_def[symmetric] by transfer_prover
lemma mcont_parametric [transfer_rule]:
assumes [transfer_rule]: "bi_total A" "bi_unique B"
shows "((rel_set A ===> A) ===> (A ===> A ===> (=)) ===> (rel_set B ===> B) ===> (B ===> B ===> (=)) ===> (A ===> B) ===> (=)) mcont mcont"
unfolding mcont_def[abs_def] by transfer_prover
end
lemma (in ccpo) Sup_Un_less:
assumes chain: "Complete_Partial_Order.chain (≤) (A ∪ B)"
and AB: "∀x∈A. ∃y∈B. x ≤ y"
shows "Sup (A ∪ B) = Sup B"
proof(rule order.antisym)
from chain have chain': "Complete_Partial_Order.chain (≤) B"
by(blast intro: chain_subset)
show "Sup (A ∪ B) ≤ Sup B" using chain
proof(rule ccpo_Sup_least)
fix x
assume "x ∈ A ∪ B"
thus "x ≤ Sup B"
proof
assume "x ∈ A"
then obtain y where "x ≤ y" "y ∈ B" using AB by blast
note ‹x ≤ y›
also from chain' ‹y ∈ B› have "y ≤ Sup B" by(rule ccpo_Sup_upper)
finally show ?thesis .
qed(rule ccpo_Sup_upper[OF chain'])
qed
show "Sup B ≤ Sup (A ∪ B)"
using chain chain' by(blast intro: ccpo_Sup_least ccpo_Sup_upper)
qed
subsection ‹The ccpo structure›
context includes tllist.lifting fixes b :: 'b begin
lift_definition tllist_ord :: "('a, 'b) tllist ⇒ ('a, 'b) tllist ⇒ bool"
is "λ(xs1, b1) (xs2, b2). if lfinite xs1 then b1 = b ∧ lprefix xs1 xs2 ∨ xs1 = xs2 ∧ flat_ord b b1 b2 else xs1 = xs2"
by auto
lift_definition tSup :: "('a, 'b) tllist set ⇒ ('a, 'b) tllist"
is "λA. (lSup (fst ` A), flat_lub b (snd ` (A ∩ {(xs, _). lfinite xs})))"
proof goal_cases
case (1 A1 A2)
hence "fst ` A1 = fst ` A2" "snd ` (A1 ∩ {(xs, _). lfinite xs}) = snd ` (A2 ∩ {(xs, _). lfinite xs})"
by(auto 4 3 simp add: rel_set_def intro: rev_image_eqI)
thus ?case by simp
qed
lemma tllist_ord_simps [simp, code]:
shows tllist_ord_TNil_TNil: "tllist_ord (TNil b1) (TNil b2) ⟷ flat_ord b b1 b2"
and tllist_ord_TNil_TCons: "tllist_ord (TNil b1) (TCons y ys) ⟷ b1 = b"
and tllist_ord_TCons_TNil: "tllist_ord (TCons x xs) (TNil b2) ⟷ False"
and tllist_ord_TCons_TCons: "tllist_ord (TCons x xs) (TCons y ys) ⟷ x = y ∧ tllist_ord xs ys"
by(auto simp add: tllist_ord.rep_eq flat_ord_def)
lemma tllist_ord_refl [simp]: "tllist_ord xs xs"
by transfer(auto simp add: flat_ord_def)
lemma tllist_ord_antisym: "⟦ tllist_ord xs ys; tllist_ord ys xs ⟧ ⟹ xs = ys"
by transfer(auto simp add: flat_ord_def split: if_split_asm intro: lprefix_antisym)
lemma tllist_ord_trans [trans]: "⟦ tllist_ord xs ys; tllist_ord ys zs ⟧ ⟹ tllist_ord xs zs"
by transfer(auto simp add: flat_ord_def split: if_split_asm intro: lprefix_trans)
lemma chain_tllist_llist_of_tllist:
assumes "Complete_Partial_Order.chain tllist_ord A"
shows "Complete_Partial_Order.chain lprefix (llist_of_tllist ` A)"
by(rule chainI)(auto 4 3 simp add: tllist_ord.rep_eq split: if_split_asm dest: chainD[OF assms])
lemma chain_tllist_terminal:
assumes "Complete_Partial_Order.chain tllist_ord A"
shows "Complete_Partial_Order.chain (flat_ord b) {terminal xs|xs. xs ∈ A ∧ tfinite xs}"
by(rule chainI)(auto simp add: tllist_ord.rep_eq flat_ord_def dest: chainD[OF assms])
lemma flat_ord_chain_finite:
assumes "Complete_Partial_Order.chain (flat_ord b) A"
shows "finite A"
proof -
from assms have "∃z. ∀x∈A. x = b ∨ x = z"
by(clarsimp simp add: chain_def flat_ord_def) metis
then obtain z where "⋀x. x ∈ A ⟹ x = b ∨ x = z" by blast
hence "A ⊆ {b, z}" by auto
thus ?thesis by(rule finite_subset) simp
qed
lemma tSup_empty [simp]: "tSup {} = TNil b"
by(transfer)(simp add: flat_lub_def)
lemma is_TNil_tSup [simp]: "is_TNil (tSup A) ⟷ (∀x∈A. is_TNil x)"
by transfer(simp add: split_beta)
lemma chain_tllist_ord_tSup:
assumes chain: "Complete_Partial_Order.chain tllist_ord A"
and A: "xs ∈ A"
shows "tllist_ord xs (tSup A)"
proof(cases "tfinite xs")
case True
show ?thesis
proof(cases "llist_of_tllist xs = llist_of_tllist (tSup A)")
case True
with ‹tfinite xs› have "lfinite (lSup (llist_of_tllist ` A))"
by(simp add: tSup_def image_image)
hence "terminal (tSup A) = flat_lub b {terminal xs|xs. xs ∈ A ∧ tfinite xs}" (is "_ = flat_lub _ ?A")
by(simp add: tSup_def terminal_tllist_of_llist image_image)(auto intro: rev_image_eqI intro!: arg_cong[where f="flat_lub b"])
moreover have "flat_ord b (terminal xs) (flat_lub b ?A)"
by(rule ccpo.ccpo_Sup_upper[OF Partial_Function.ccpo[OF flat_interpretation]])(blast intro: chain_tllist_terminal[OF chain] A ‹tfinite xs›)+
ultimately show ?thesis using True by(simp add: tllist_ord.rep_eq)
next
case False
hence "∃ys∈A. ¬ tllist_ord ys xs"
by(rule contrapos_np)(auto intro!: lprefix_antisym chain_lSup_lprefix chain_lprefix_lSup simp add: tSup_def image_image A chain_tllist_llist_of_tllist[OF chain] tllist_ord.rep_eq split: if_split_asm)
then obtain ys where "ys ∈ A" "¬ tllist_ord ys xs" by blast
with A have "tllist_ord xs ys" "xs ≠ ys" by(auto dest: chainD[OF chain])
with True have "terminal xs = b" by transfer(auto simp add: flat_ord_def)
with True False show ?thesis
by(simp add: tllist_ord.rep_eq tSup_def image_image chain_lprefix_lSup chain_tllist_llist_of_tllist chain A)
qed
next
case False
thus ?thesis using assms by(simp add: tllist_ord.rep_eq tSup_def image_image chain_lprefix_lSup chain_tllist_llist_of_tllist not_lfinite_lprefix_conv_eq[THEN iffD1] terminal_tllist_of_llist split: if_split_asm)
qed
lemma chain_tSup_tllist_ord:
assumes chain: "Complete_Partial_Order.chain tllist_ord A"
and lub: "⋀xs'. xs' ∈ A ⟹ tllist_ord xs' xs"
shows "tllist_ord (tSup A) xs"
proof -
have "⋀xs'. xs' ∈ llist_of_tllist ` A ⟹ lprefix xs' (llist_of_tllist xs)"
by(auto dest!: lub simp add: tllist_ord.rep_eq split: if_split_asm)
with chain_tllist_llist_of_tllist[OF chain]
have prefix: "lprefix (lSup (llist_of_tllist ` A)) (llist_of_tllist xs)"
by(rule chain_lSup_lprefix)
show ?thesis
proof(cases "tfinite (tSup A)")
case False thus ?thesis using prefix
by(simp add: tllist_ord.rep_eq tSup_def image_image not_lfinite_lprefix_conv_eq[THEN iffD1])
next
case True
from True have fin: "lfinite (lSup (llist_of_tllist ` A))" by(simp add: tSup_def image_image)
have eq: "terminal (tSup A) = flat_lub b {terminal xs|xs. xs ∈ A ∧ tfinite xs}" (is "_ = flat_lub _ ?A")
by(simp add: tSup_def terminal_tllist_of_llist image_image fin)(auto intro: rev_image_eqI intro!: arg_cong[where f="flat_lub b"])
show ?thesis
proof(cases "lprefix (llist_of_tllist xs) (lSup (llist_of_tllist ` A))")
case True
with prefix have "lSup (llist_of_tllist ` A) = llist_of_tllist xs" by(rule lprefix_antisym)
moreover have "flat_ord b (flat_lub b ?A) (terminal xs)"
by(rule ccpo.ccpo_Sup_least[OF Partial_Function.ccpo[OF flat_interpretation]])(auto intro: chain_tllist_terminal[OF chain] dest: lub simp add: tllist_ord.rep_eq flat_ord_def)
ultimately show ?thesis using eq by(simp add: tllist_ord.rep_eq tSup_def image_image)
next
case False
{ fix xs'
assume "xs' ∈ A"
with False have "¬ lprefix (llist_of_tllist xs) (llist_of_tllist xs')"
by-(erule contrapos_nn, auto 4 4 intro: lprefix_trans chain_lprefix_lSup chain_tllist_llist_of_tllist chain)
with lub[OF ‹xs' ∈ A›] have "terminal xs' = b"
by(auto simp add: tllist_ord.rep_eq split: if_split_asm) }
with chain_tllist_terminal[OF chain] have "flat_ord b (flat_lub b ?A) b"
by -(rule ccpo.ccpo_Sup_least[OF Partial_Function.ccpo[OF flat_interpretation]], auto simp add: flat_ord_def)
hence "flat_lub b ?A = b" by(simp add: flat_ord_def)
thus ?thesis using True eq prefix
by(simp add: tSup_def terminal_tllist_of_llist tllist_ord.rep_eq image_image)
qed
qed
qed
lemma tllist_ord_ccpo [simp, cont_intro]:
"class.ccpo tSup tllist_ord (mk_less tllist_ord)"
by unfold_locales(auto simp add: mk_less_def intro: tllist_ord_antisym tllist_ord_trans chain_tllist_ord_tSup chain_tSup_tllist_ord)
lemma tllist_ord_partial_function_definitions: "partial_function_definitions tllist_ord tSup"
by unfold_locales(auto simp add: mk_less_def intro: tllist_ord_antisym tllist_ord_trans chain_tllist_ord_tSup chain_tSup_tllist_ord)
interpretation tllist: partial_function_definitions "tllist_ord" "tSup"
by(rule tllist_ord_partial_function_definitions)
lemma admissible_mcont_is_TNil [THEN admissible_subst, cont_intro, simp]:
shows admissible_is_TNil: "ccpo.admissible tSup tllist_ord is_TNil"
by(rule ccpo.admissibleI)(simp)
lemma terminal_tSup:
"∀xs∈Y. is_TNil xs ⟹ terminal (tSup Y) = flat_lub b (terminal ` Y)"
including tllist.lifting apply transfer
apply (auto simp add: split_def)
apply (rule arg_cong [where f = "flat_lub b"])
apply force
done
lemma thd_tSup:
"∃xs ∈ Y. ¬ is_TNil xs
⟹ thd (tSup Y) = (THE x. x ∈ thd ` (Y ∩ {xs. ¬ is_TNil xs}))"
apply(simp add: tSup_def image_image)
apply(rule arg_cong[where f=The])
apply(auto intro: rev_image_eqI intro!: ext)
done
lemma ex_TCons_raw_parametric:
includes lifting_syntax
shows "(rel_set (rel_prod (llist_all2 A) B) ===> (=)) (λY. ∃(xs, b) ∈ Y. ¬ lnull xs) (λY. ∃(xs, b) ∈ Y. ¬ lnull xs)"
by(auto 4 4 simp add: rel_fun_def dest: rel_setD1 rel_setD2 llist_all2_lnullD intro: rev_bexI)
lift_definition ex_TCons :: "('a, 'b) tllist set ⇒ bool"
is "λY. ∃(xs, b) ∈ Y. ¬ lnull xs" parametric ex_TCons_raw_parametric
by (blast dest: rel_setD1 rel_setD2)+
lemma ex_TCons_iff: "ex_TCons Y ⟷ (∃xs ∈ Y. ¬ is_TNil xs)"
by transfer auto
lemma retain_TCons_raw_parametric:
includes lifting_syntax
shows "(rel_set (rel_prod (llist_all2 A) B) ===> rel_set (rel_prod (llist_all2 A) B))
(λA. A ∩ {(xs, b). ¬ lnull xs}) (λA. A ∩ {(xs, b). ¬ lnull xs})"
by(rule rel_funI rel_setI)+(auto 4 4 dest: llist_all2_lnullD rel_setD2 rel_setD1 intro: rev_bexI)
lift_definition retain_TCons :: "('a, 'b) tllist set ⇒ ('a, 'b) tllist set"
is "λA. A ∩ {(xs, b). ¬ lnull xs}" parametric retain_TCons_raw_parametric
by(rule rel_setI)(fastforce dest: rel_setD1 rel_setD2)+
lemma retain_TCons_conv: "retain_TCons A = A ∩ {xs. ¬ is_TNil xs}"
by(auto simp add: retain_TCons_def intro: rev_image_eqI)
lemma ttl_tSup:
"⟦ Complete_Partial_Order.chain tllist_ord Y; ∃xs ∈ Y. ¬ is_TNil xs ⟧
⟹ ttl (tSup Y) = tSup (ttl ` (Y ∩ {xs. ¬ is_TNil xs}))"
unfolding ex_TCons_iff[symmetric] retain_TCons_conv[symmetric]
proof (transfer, goal_cases)
case prems: (1 Y)
then obtain xs b' where xsb: "(xs, b') ∈ Y" "¬ lnull xs" by blast
note chain = prems(1)
have "flat_lub b (snd ` (Y ∩ {(xs, _). lfinite xs})) = flat_lub b (insert b (snd ` (Y ∩ {(xs, _). lfinite xs})))"
by(auto simp add: flat_lub_def)
also have "insert b (snd ` (Y ∩ {(xs, _). lfinite xs})) = insert b (snd ` (apfst ltl ` (Y ∩ {(xs, b). ¬ lnull xs}) ∩ {(xs, _). lfinite xs}))"
apply(auto intro: rev_image_eqI)
apply(erule contrapos_np)
apply(frule chainD[OF chain ‹(xs, b') ∈ Y›])
using ‹¬ lnull xs› xsb
by(fastforce split: if_split_asm simp add: lprefix_lnull intro!: rev_image_eqI)
also have "flat_lub b … = flat_lub b (snd ` (apfst ltl ` (Y ∩ {(xs, b). ¬ lnull xs}) ∩ {(xs, _). lfinite xs}))"
by(auto simp add: flat_lub_def)
also
have "ltl ` (fst ` Y ∩ {xs. ¬ lnull xs}) = fst ` apfst ltl ` (Y ∩ {(xs, b). ¬ lnull xs})"
by(auto simp add: image_image)
ultimately show ?case using prems by clarsimp
qed
lemma tSup_TCons: "A ≠ {} ⟹ tSup (TCons x ` A) = TCons x (tSup A)"
unfolding Set.is_empty_def[symmetric]
apply transfer
unfolding Set.is_empty_def
apply(clarsimp simp add: image_image lSup_LCons[symmetric])
apply(rule arg_cong[where f="flat_lub b"])
apply(auto 4 3 intro: rev_image_eqI)
done
lemma tllist_ord_terminalD:
"⟦ tllist_ord xs ys; is_TNil ys ⟧ ⟹ flat_ord b (terminal xs) (terminal ys)"
by(cases xs)(auto simp add: is_TNil_def)
lemma tllist_ord_bot [simp]: "tllist_ord (TNil b) xs"
by(cases xs)(simp_all add: flat_ord_def)
lemma tllist_ord_ttlI:
"tllist_ord xs ys ⟹ tllist_ord (ttl xs) (ttl ys)"
by(cases xs ys rule: tllist.exhaust[case_product tllist.exhaust])(simp_all)
lemma not_is_TNil_conv: "¬ is_TNil xs ⟷ (∃x xs'. xs = TCons x xs')"
by(cases xs) simp_all
subsection ‹Continuity of predefined constants›
lemma mono_tllist_ord_case:
fixes bot
assumes mono: "⋀x. monotone tllist_ord ord (λxs. f x xs (TCons x xs))"
and ord: "class.preorder ord (mk_less ord)"
and bot: "⋀x. ord (bot b) x"
shows "monotone tllist_ord ord (λxs. case xs of TNil b ⇒ bot b | TCons x xs' ⇒ f x xs' xs)"
proof -
interpret preorder ord "mk_less ord" by (fact ord)
show ?thesis by(rule monotoneI)(auto split: tllist.split dest: monotoneD[OF mono] simp add: flat_ord_def bot)
qed
lemma mcont_lprefix_case_aux:
fixes f bot ord
defines "g ≡ λxs. f (thd xs) (ttl xs) (TCons (thd xs) (ttl xs))"
assumes mcont: "⋀x. mcont tSup tllist_ord lub ord (λxs. f x xs (TCons x xs))"
and ccpo: "class.ccpo lub ord (mk_less ord)"
and bot: "⋀x. ord (bot b) x"
and cont_bot: "cont (flat_lub b) (flat_ord b) lub ord bot"
shows "mcont tSup tllist_ord lub ord (λxs. case xs of TNil b ⇒ bot b | TCons x xs' ⇒ f x xs' xs)"
(is "mcont _ _ _ _ ?f")
proof(rule mcontI)
interpret b: ccpo lub ord "mk_less ord" by(rule ccpo)
show "cont tSup tllist_ord lub ord ?f"
proof(rule contI)
fix Y :: "('a, 'b) tllist set"
assume chain: "Complete_Partial_Order.chain tllist_ord Y"
and Y: "Y ≠ {}"
from chain have chain': "Complete_Partial_Order.chain ord (?f ` Y)"
by(rule chain_imageI)(auto split: tllist.split simp add: flat_ord_def intro!: bot mcont_monoD[OF mcont])
show "?f (tSup Y) = lub (?f ` Y)"
proof(cases "is_TNil (tSup Y)")
case True
hence "?f ` Y = bot ` terminal ` Y"
by(auto 4 3 split: tllist.split intro: rev_image_eqI intro!: imageI)
moreover from True have "tSup Y = TNil (flat_lub b (terminal ` Y))"
by -(rule tllist.expand, simp_all add: terminal_tSup)
moreover have "Complete_Partial_Order.chain (flat_ord b) (terminal ` Y)"
using chain True by(auto intro: chain_imageI tllist_ord_terminalD)
ultimately show ?thesis using Y
by (simp add: contD [OF cont_bot] cong del: b.SUP_cong_simp)
next
case False
hence eq: "tSup Y = TCons (thd (tSup Y)) (ttl (tSup Y))" by simp
have eq':
"?f ` Y =
(λx. bot (terminal x)) ` (Y ∩ {xs. is_TNil xs}) ∪
(λxs. f (thd xs) (ttl xs) xs) ` (Y ∩ {xs. ¬ is_TNil xs})"
by(auto 4 3 split: tllist.splits intro: rev_image_eqI)
from False obtain xs where xs: "xs ∈ Y" "¬ is_TNil xs" by auto
{ fix ys
assume "ys ∈ Y" "is_TNil ys"
hence "terminal ys = b" using xs
by(cases xs ys rule: tllist.exhaust[case_product tllist.exhaust])(auto dest: chainD[OF chain]) }
then have lub: "lub (?f ` Y) = lub ((λxs. f (thd xs) (ttl xs) xs) ` (Y ∩ {xs. ¬ is_TNil xs}))"
using xs chain' unfolding eq'
by -(erule ccpo.Sup_Un_less[OF ccpo], auto simp add: intro!: bot)
{ fix xs
assume xs: "xs ∈ Y ∩ {xs. ¬ is_TNil xs}"
hence "(THE x. x ∈ thd ` (Y ∩ {xs. ¬ is_TNil xs})) = thd xs"
by(auto dest: chainD[OF chain] simp add: not_is_TNil_conv intro!: the_equality)
hence "f (THE x. x ∈ thd ` (Y ∩ {xs. ¬ is_TNil xs})) (ttl xs) (TCons (THE x. x ∈ thd ` (Y ∩ {xs. ¬ is_TNil xs})) (ttl xs)) = f (thd xs) (ttl xs) xs"
using xs by simp }
moreover have "Complete_Partial_Order.chain tllist_ord (ttl ` (Y ∩ {xs. ¬ is_TNil xs}))"
using chain by(rule chain_imageI[OF chain_subset])(auto simp add: tllist_ord_ttlI)
moreover from False have "Y ∩ {xs. ¬ is_TNil xs} ≠ {}" by auto
ultimately show ?thesis
apply(subst (1 2) eq)
using False
apply(simp add: thd_tSup ttl_tSup[OF chain] mcont_contD[OF mcont] image_image lub)
done
qed
qed
from mcont_mono[OF mcont] _ bot
show "monotone tllist_ord ord ?f"
by(rule mono_tllist_ord_case)(unfold_locales)
qed
lemma cont_TNil [simp, cont_intro]: "cont (flat_lub b) (flat_ord b) tSup tllist_ord TNil"
apply(rule contI)
apply transfer
apply(simp add: image_image image_constant_conv)
apply(rule arg_cong[where f="flat_lub b"])
apply(auto intro: rev_image_eqI)
done
lemma monotone_TCons: "monotone tllist_ord tllist_ord (TCons x)"
by(rule monotoneI) simp
lemmas mono2mono_TCons[cont_intro] = monotone_TCons[THEN tllist.mono2mono]
lemma mcont_TCons: "mcont tSup tllist_ord tSup tllist_ord (TCons x)"
apply(rule mcontI)
apply(rule monotone_TCons)
apply(rule contI)
apply(simp add: tSup_TCons)
done
lemmas mcont2mcont_TCons[cont_intro] = mcont_TCons[THEN tllist.mcont2mcont]
lemmas [transfer_rule del] = tllist_ord.transfer tSup.transfer
lifting_update tllist.lifting
lifting_forget tllist.lifting
lemmas [transfer_rule] = tllist_ord.transfer tSup.transfer
lemma mono2mono_tset[THEN lfp.mono2mono, cont_intro]:
shows smonotone_tset: "monotone tllist_ord (⊆) tset"
including tllist.lifting
by transfer(rule monotone_comp[OF _ monotone_lset], auto intro: monotoneI)
lemma mcont2mcont_tset [THEN lfp.mcont2mcont, cont_intro]:
shows mcont_tset: "mcont tSup tllist_ord Union (⊆) tset"
including tllist.lifting
apply transfer
apply(rule mcont_comp[OF _ mcont_lset])
unfolding mcont_def by(auto intro: monotoneI contI )
end
context includes lifting_syntax
begin
lemma rel_fun_lift:
"(⋀x. A (f x) (g x)) ⟹ ((=) ===> A) f g"
by(simp add: rel_fun_def)
lemma tllist_ord_transfer [transfer_rule]:
"((=) ===> pcr_tllist (=) (=) ===> pcr_tllist (=) (=) ===> (=))
(λb (xs1, b1) (xs2, b2). if lfinite xs1 then b1 = b ∧ lprefix xs1 xs2 ∨ xs1 = xs2 ∧ flat_ord b b1 b2 else xs1 = xs2)
tllist_ord"
by(rule rel_fun_lift)(rule tllist_ord.transfer)
lemma tSup_transfer [transfer_rule]:
"((=) ===> rel_set (pcr_tllist (=) (=)) ===> pcr_tllist (=) (=))
(λb A. (lSup (fst ` A), flat_lub b (snd ` (A ∩ {(xs, _). lfinite xs}))))
tSup"
by(rule rel_fun_lift)(rule tSup.transfer)
end
lifting_update tllist.lifting
lifting_forget tllist.lifting
interpretation tllist: partial_function_definitions "tllist_ord b" "tSup b" for b
by(rule tllist_ord_partial_function_definitions)
lemma tllist_case_mono [partial_function_mono, cont_intro]:
assumes tnil: "⋀b. monotone orda ordb (λf. tnil f b)"
and tcons: "⋀x xs. monotone orda ordb (λf. tcons f x xs)"
shows "monotone orda ordb (λf. case_tllist (tnil f) (tcons f) xs)"
by(rule monotoneI)(auto split: tllist.split dest: monotoneD[OF tnil] monotoneD[OF tcons])
subsection ‹Definition of recursive functions›
locale tllist_pf = fixes b :: 'b
begin
declaration ‹Partial_Function.init "tllist" @{term "tllist.fixp_fun b"}
@{term "tllist.mono_body b"} @{thm tllist.fixp_rule_uc[where b=b]} @{thm tllist.fixp_induct_uc[where b=b]} NONE›
abbreviation mono_tllist where "mono_tllist ≡ monotone (fun_ord (tllist_ord b)) (tllist_ord b)"
lemma LCons_mono [partial_function_mono, cont_intro]:
"mono_tllist A ⟹ mono_tllist (λf. TCons x (A f))"
by(rule monotoneI)(auto dest: monotoneD)
end
lemma mono_tllist_lappendt2 [partial_function_mono]:
"tllist_pf.mono_tllist b A ⟹ tllist_pf.mono_tllist b (λf. lappendt xs (A f))"
apply(rule monotoneI)
apply(drule (1) monotoneD)
apply(simp add: tllist_ord.rep_eq split: if_split_asm)
apply(auto simp add: lappend_inf)
done
lemma mono_tllist_tappend2 [partial_function_mono]:
assumes "⋀y. tllist_pf.mono_tllist b (C y)"
shows "tllist_pf.mono_tllist b (λf. tappend xs (λy. C y f))"
apply(cases "tfinite xs")
apply(rule monotoneI)
apply(drule monotoneD[OF assms[where y="terminal xs"]])
including tllist.lifting
apply transfer
apply(fastforce split: if_split_asm)
apply(simp add: tappend_inf)
done
end