(* Title: HOL/Library/Complete_Partial_Order2.thy
Author: Andreas Lochbihler, ETH Zurich
*)
section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
theory Complete_Partial_Order2 imports
Main Lattice_Syntax
begin
lemma chain_transfer [transfer_rule]:
includes lifting_syntax
shows "((A ===> A ===> (=)) ===> rel_set A ===> (=)) Complete_Partial_Order.chain Complete_Partial_Order.chain"
unfolding chain_def[abs_def] by transfer_prover
lemma linorder_chain [simp, intro!]:
fixes Y :: "_ :: linorder set"
shows "Complete_Partial_Order.chain (\) Y"
by(auto intro: chainI)
lemma fun_lub_apply: "\Sup. fun_lub Sup Y x = Sup ((\f. f x) ` Y)"
by(simp add: fun_lub_def image_def)
lemma fun_lub_empty [simp]: "fun_lub lub {} = (\_. lub {})"
by(rule ext)(simp add: fun_lub_apply)
lemma chain_fun_ordD:
assumes "Complete_Partial_Order.chain (fun_ord le) Y"
shows "Complete_Partial_Order.chain le ((\f. f x) ` Y)"
by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def)
lemma chain_Diff:
"Complete_Partial_Order.chain ord A
\<Longrightarrow> Complete_Partial_Order.chain ord (A - B)"
by(erule chain_subset) blast
lemma chain_rel_prodD1:
"Complete_Partial_Order.chain (rel_prod orda ordb) Y
\<Longrightarrow> Complete_Partial_Order.chain orda (fst ` Y)"
by(auto 4 3 simp add: chain_def)
lemma chain_rel_prodD2:
"Complete_Partial_Order.chain (rel_prod orda ordb) Y
\<Longrightarrow> Complete_Partial_Order.chain ordb (snd ` Y)"
by(auto 4 3 simp add: chain_def)
context ccpo begin
lemma ccpo_fun: "class.ccpo (fun_lub Sup) (fun_ord (\)) (mk_less (fun_ord (\)))"
by standard (auto 4 3 simp add: mk_less_def fun_ord_def fun_lub_apply
intro: order.trans antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
lemma ccpo_Sup_below_iff: "Complete_Partial_Order.chain (\) Y \ Sup Y \ x \ (\y\Y. y \ x)"
by(fast intro: order_trans[OF ccpo_Sup_upper] ccpo_Sup_least)
lemma Sup_minus_bot:
assumes chain: "Complete_Partial_Order.chain (\) A"
shows "\(A - {\{}}) = \A"
(is "?lhs = ?rhs")
proof (rule antisym)
show "?lhs \ ?rhs"
by (blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])
show "?rhs \ ?lhs"
proof (rule ccpo_Sup_least [OF chain])
show "x \ A \ x \ ?lhs" for x
by (cases "x = \{}")
(blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+
qed
qed
lemma mono_lub:
fixes le_b (infix "\" 60)
assumes chain: "Complete_Partial_Order.chain (fun_ord (\)) Y"
and mono: "\f. f \ Y \ monotone le_b (\) f"
shows "monotone (\) (\) (fun_lub Sup Y)"
proof(rule monotoneI)
fix x y
assume "x \ y"
have chain'': "\x. Complete_Partial_Order.chain (\) ((\f. f x) ` Y)"
using chain by(rule chain_imageI)(simp add: fun_ord_def)
then show "fun_lub Sup Y x \ fun_lub Sup Y y" unfolding fun_lub_apply
proof(rule ccpo_Sup_least)
fix x'
assume "x' \ (\f. f x) ` Y"
then obtain f where "f \ Y" "x' = f x" by blast
note \<open>x' = f x\<close> also
from \<open>f \<in> Y\<close> \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y" by(blast dest: mono monotoneD)
also have "\ \ \((\f. f y) ` Y)" using chain''
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Y\<close>)
finally show "x' \ \((\f. f y) ` Y)" .
qed
qed
context
fixes le_b (infix "\" 60) and Y f
assumes chain: "Complete_Partial_Order.chain le_b Y"
and mono1: "\y. y \ Y \ monotone le_b (\) (\x. f x y)"
and mono2: "\x a b. \ x \ Y; a \ b; a \ Y; b \ Y \ \ f x a \ f x b"
begin
lemma Sup_mono:
assumes le: "x \ y" and x: "x \ Y" and y: "y \ Y"
shows "\(f x ` Y) \ \(f y ` Y)" (is "_ \ ?rhs")
proof(rule ccpo_Sup_least)
from chain show chain': "Complete_Partial_Order.chain (\) (f x ` Y)" when "x \ Y" for x
by(rule chain_imageI) (insert that, auto dest: mono2)
fix x'
assume "x' \ f x ` Y"
then obtain y' where "y' \<in> Y" "x' = f x y'" by blast note this(2)
also from mono1[OF \<open>y' \<in> Y\<close>] le have "\<dots> \<le> f y y'" by(rule monotoneD)
also have "\ \ ?rhs" using chain'[OF y]
by (auto intro!: ccpo_Sup_upper simp add: \<open>y' \<in> Y\<close>)
finally show "x' \ ?rhs" .
qed(rule x)
lemma diag_Sup: "\((\x. \(f x ` Y)) ` Y) = \((\x. f x x) ` Y)" (is "?lhs = ?rhs")
proof(rule antisym)
have chain1: "Complete_Partial_Order.chain (\) ((\x. \(f x ` Y)) ` Y)"
using chain by(rule chain_imageI)(rule Sup_mono)
have chain2: "\y'. y' \ Y \ Complete_Partial_Order.chain (\) (f y' ` Y)" using chain
by(rule chain_imageI)(auto dest: mono2)
have chain3: "Complete_Partial_Order.chain (\) ((\x. f x x) ` Y)"
using chain by(rule chain_imageI)(auto intro: monotoneD[OF mono1] mono2 order.trans)
show "?lhs \ ?rhs" using chain1
proof(rule ccpo_Sup_least)
fix x'
assume "x' \ (\x. \(f x ` Y)) ` Y"
then obtain y' where "y' \<in> Y" "x' = \<Squnion>(f y' ` Y)" by blast note this(2)
also have "\ \ ?rhs" using chain2[OF \y' \ Y\]
proof(rule ccpo_Sup_least)
fix x
assume "x \ f y' ` Y"
then obtain y where "y \ Y" and x: "x = f y' y" by blast
define y'' where "y'' = (if y \ y' then y' else y)"
from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
hence "f y' y \ f y'' y''" using \y \ Y\ \y' \ Y\
by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1])
also from \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y'' \<in> Y" by(simp add: y''_def)
from chain3 have "f y'' y'' \ ?rhs" by(rule ccpo_Sup_upper)(simp add: \y'' \ Y\)
finally show "x \ ?rhs" by(simp add: x)
qed
finally show "x' \ ?rhs" .
qed
show "?rhs \ ?lhs" using chain3
proof(rule ccpo_Sup_least)
fix y
assume "y \ (\x. f x x) ` Y"
then obtain x where "x \ Y" and "y = f x x" by blast note this(2)
also from chain2[OF \<open>x \<in> Y\<close>] have "\<dots> \<le> \<Squnion>(f x ` Y)"
by(rule ccpo_Sup_upper)(simp add: \<open>x \<in> Y\<close>)
also have "\ \ ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \x \ Y\)
finally show "y \ ?lhs" .
qed
qed
end
lemma Sup_image_mono_le:
fixes le_b (infix "\" 60) and Sup_b ("\")
assumes ccpo: "class.ccpo Sup_b (\) lt_b"
assumes chain: "Complete_Partial_Order.chain (\) Y"
and mono: "\x y. \ x \ y; x \ Y \ \ f x \ f y"
shows "Sup (f ` Y) \ f (\Y)"
proof(rule ccpo_Sup_least)
show "Complete_Partial_Order.chain (\) (f ` Y)"
using chain by(rule chain_imageI)(rule mono)
fix x
assume "x \ f ` Y"
then obtain y where "y \ Y" and "x = f y" by blast note this(2)
also have "y \ \Y" using ccpo chain \y \ Y\ by(rule ccpo.ccpo_Sup_upper)
hence "f y \ f (\Y)" using \y \ Y\ by(rule mono)
finally show "x \ \" .
qed
lemma swap_Sup:
fixes le_b (infix "\" 60)
assumes Y: "Complete_Partial_Order.chain (\) Y"
and Z: "Complete_Partial_Order.chain (fun_ord (\)) Z"
and mono: "\f. f \ Z \ monotone (\) (\) f"
shows "\((\x. \(x ` Y)) ` Z) = \((\x. \((\f. f x) ` Z)) ` Y)"
(is "?lhs = ?rhs")
proof(cases "Y = {}")
case True
then show ?thesis
by (simp add: image_constant_conv cong del: SUP_cong_simp)
next
case False
have chain1: "\f. f \ Z \ Complete_Partial_Order.chain (\) (f ` Y)"
by(rule chain_imageI[OF Y])(rule monotoneD[OF mono])
have chain2: "Complete_Partial_Order.chain (\) ((\x. \(x ` Y)) ` Z)" using Z
proof(rule chain_imageI)
fix f g
assume "f \ Z" "g \ Z"
and "fun_ord (\) f g"
from chain1[OF \<open>f \<in> Z\<close>] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
proof(rule ccpo_Sup_least)
fix x
assume "x \ f ` Y"
then obtain y where "y \ Y" "x = f y" by blast note this(2)
also have "\ \ g y" using \fun_ord (\) f g\ by(simp add: fun_ord_def)
also have "\ \ \(g ` Y)" using chain1[OF \g \ Z\]
by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
finally show "x \ \(g ` Y)" .
qed
qed
have chain3: "\x. Complete_Partial_Order.chain (\) ((\f. f x) ` Z)"
using Z by(rule chain_imageI)(simp add: fun_ord_def)
have chain4: "Complete_Partial_Order.chain (\) ((\x. \((\f. f x) ` Z)) ` Y)"
using Y
proof(rule chain_imageI)
fix f x y
assume "x \ y"
show "\((\f. f x) ` Z) \ \((\f. f y) ` Z)" (is "_ \ ?rhs") using chain3
proof(rule ccpo_Sup_least)
fix x'
assume "x' \ (\f. f x) ` Z"
then obtain f where "f \ Z" "x' = f x" by blast note this(2)
also have "f x \ f y" using \f \ Z\ \x \ y\ by(rule monotoneD[OF mono])
also have "f y \ ?rhs" using chain3
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
finally show "x' \ ?rhs" .
qed
qed
from chain2 have "?lhs \ ?rhs"
proof(rule ccpo_Sup_least)
fix x
assume "x \ (\x. \(x ` Y)) ` Z"
then obtain f where "f \ Z" "x = \(f ` Y)" by blast note this(2)
also have "\ \ ?rhs" using chain1[OF \f \ Z\]
proof(rule ccpo_Sup_least)
fix x'
assume "x' \ f ` Y"
then obtain y where "y \ Y" "x' = f y" by blast note this(2)
also have "f y \ \((\f. f y) ` Z)" using chain3
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
also have "\ \ ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \y \ Y\)
finally show "x' \ ?rhs" .
qed
finally show "x \ ?rhs" .
qed
moreover
have "?rhs \ ?lhs" using chain4
proof(rule ccpo_Sup_least)
fix x
assume "x \ (\x. \((\f. f x) ` Z)) ` Y"
then obtain y where "y \ Y" "x = \((\f. f y) ` Z)" by blast note this(2)
also have "\ \ ?lhs" using chain3
proof(rule ccpo_Sup_least)
fix x'
assume "x' \ (\f. f y) ` Z"
then obtain f where "f \ Z" "x' = f y" by blast note this(2)
also have "f y \ \(f ` Y)" using chain1[OF \f \ Z\]
by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
also have "\ \ ?lhs" using chain2
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
finally show "x' \ ?lhs" .
qed
finally show "x \ ?lhs" .
qed
ultimately show "?lhs = ?rhs" by(rule antisym)
qed
lemma fixp_mono:
assumes fg: "fun_ord (\) f g"
and f: "monotone (\) (\) f"
and g: "monotone (\) (\) g"
shows "ccpo_class.fixp f \ ccpo_class.fixp g"
unfolding fixp_def
proof(rule ccpo_Sup_least)
fix x
assume "x \ ccpo_class.iterates f"
thus "x \ \ccpo_class.iterates g"
proof induction
case (step x)
from f step.IH have "f x \ f (\ccpo_class.iterates g)" by(rule monotoneD)
also have "\ \ g (\ccpo_class.iterates g)" using fg by(simp add: fun_ord_def)
also have "\ = \ccpo_class.iterates g" by(fold fixp_def fixp_unfold[OF g]) simp
finally show ?case .
qed(blast intro: ccpo_Sup_least)
qed(rule chain_iterates[OF f])
context fixes ordb :: "'b \ 'b \ bool" (infix "\" 60) begin
lemma iterates_mono:
assumes f: "f \ ccpo.iterates (fun_lub Sup) (fun_ord (\)) F"
and mono: "\f. monotone (\) (\) f \ monotone (\) (\) (F f)"
shows "monotone (\) (\) f"
using f
by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mono_lub)+
lemma fixp_preserves_mono:
assumes mono: "\x. monotone (fun_ord (\)) (\) (\f. F f x)"
and mono2: "\f. monotone (\) (\) f \ monotone (\) (\) (F f)"
shows "monotone (\) (\) (ccpo.fixp (fun_lub Sup) (fun_ord (\)) F)"
(is "monotone _ _ ?fixp")
proof(rule monotoneI)
have mono: "monotone (fun_ord (\)) (fun_ord (\)) F"
by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])
let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord (\)) F"
have chain: "\x. Complete_Partial_Order.chain (\) ((\f. f x) ` ?iter)"
by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def)
fix x y
assume "x \ y"
show "?fixp x \ ?fixp y"
apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
using chain
proof(rule ccpo_Sup_least)
fix x'
assume "x' \ (\f. f x) ` ?iter"
then obtain f where "f \ ?iter" "x' = f x" by blast note this(2)
also have "f x \ f y"
by(rule monotoneD[OF iterates_mono[OF \<open>f \<in> ?iter\<close> mono2]])(blast intro: \<open>x \<sqsubseteq> y\<close>)+
also have "f y \ \((\f. f y) ` ?iter)" using chain
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
finally show "x' \ \" .
qed
qed
end
end
lemma monotone2monotone:
assumes 2: "\x. monotone ordb ordc (\y. f x y)"
and t: "monotone orda ordb (\x. t x)"
and 1: "\y. monotone orda ordc (\x. f x y)"
and trans: "transp ordc"
shows "monotone orda ordc (\x. f x (t x))"
by(blast intro: monotoneI transpD[OF trans] monotoneD[OF t] monotoneD[OF 2] monotoneD[OF 1])
subsection \<open>Continuity\<close>
definition cont :: "('a set \ 'a) \ ('a \ 'a \ bool) \ ('b set \ 'b) \ ('b \ 'b \ bool) \ ('a \ 'b) \ bool"
where
"cont luba orda lubb ordb f \
(\<forall>Y. Complete_Partial_Order.chain orda Y \<longrightarrow> Y \<noteq> {} \<longrightarrow> f (luba Y) = lubb (f ` Y))"
definition mcont :: "('a set \ 'a) \ ('a \ 'a \ bool) \ ('b set \ 'b) \ ('b \ 'b \ bool) \ ('a \ 'b) \ bool"
where
"mcont luba orda lubb ordb f \
monotone orda ordb f \<and> cont luba orda lubb ordb f"
subsubsection \<open>Theorem collection \<open>cont_intro\<close>\<close>
named_theorems cont_intro "continuity and admissibility intro rules"
ML \<open>
(* apply cont_intro rules as intro and try to solve
the remaining of the emerging subgoals with simp *)
fun cont_intro_tac ctxt =
REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>cont_intro\<close>)))
THEN_ALL_NEW (SOLVED' (simp_tac ctxt))
fun cont_intro_simproc ctxt ct =
let
fun mk_stmt t = t
|> HOLogic.mk_Trueprop
|> Thm.cterm_of ctxt
|> Goal.init
fun mk_thm t =
case SINGLE (cont_intro_tac ctxt 1) (mk_stmt t) of
SOME thm => SOME (Goal.finish ctxt thm RS @{thm Eq_TrueI})
| NONE => NONE
in
case Thm.term_of ct of
t as Const (\<^const_name>\<open>ccpo.admissible\<close>, _) $ _ $ _ $ _ => mk_thm t
| t as Const (\<^const_name>\<open>mcont\<close>, _) $ _ $ _ $ _ $ _ $ _ => mk_thm t
| t as Const (\<^const_name>\<open>monotone\<close>, _) $ _ $ _ $ _ => mk_thm t
| _ => NONE
end
handle THM _ => NONE
| TYPE _ => NONE
\<close>
simproc_setup "cont_intro"
( "ccpo.admissible lub ord P"
| "mcont lub ord lub' ord' f"
| "monotone ord ord' f"
) = \<open>K cont_intro_simproc\<close>
lemmas [cont_intro] =
call_mono
let_mono
if_mono
option.const_mono
tailrec.const_mono
bind_mono
declare if_mono[simp]
lemma monotone_id' [cont_intro]: "monotone ord ord (\x. x)"
by(simp add: monotone_def)
lemma monotone_applyI:
"monotone orda ordb F \ monotone (fun_ord orda) ordb (\f. F (f x))"
by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
lemma monotone_if_fun [partial_function_mono]:
"\ monotone (fun_ord orda) (fun_ord ordb) F; monotone (fun_ord orda) (fun_ord ordb) G \
\<Longrightarrow> monotone (fun_ord orda) (fun_ord ordb) (\<lambda>f n. if c n then F f n else G f n)"
by(simp add: monotone_def fun_ord_def)
lemma monotone_fun_apply_fun [partial_function_mono]:
"monotone (fun_ord (fun_ord ord)) (fun_ord ord) (\f n. f t (g n))"
by(rule monotoneI)(simp add: fun_ord_def)
lemma monotone_fun_ord_apply:
"monotone orda (fun_ord ordb) f \ (\x. monotone orda ordb (\y. f y x))"
by(auto simp add: monotone_def fun_ord_def)
context preorder begin
declare transp_le[cont_intro]
lemma monotone_const [simp, cont_intro]: "monotone ord (\) (\_. c)"
by(rule monotoneI) simp
end
lemma transp_le [cont_intro, simp]:
"class.preorder ord (mk_less ord) \ transp ord"
by(rule preorder.transp_le)
context partial_function_definitions begin
declare const_mono [cont_intro, simp]
lemma transp_le [cont_intro, simp]: "transp leq"
by(rule transpI)(rule leq_trans)
lemma preorder [cont_intro, simp]: "class.preorder leq (mk_less leq)"
by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans)
declare ccpo[cont_intro, simp]
end
lemma contI [intro?]:
"(\Y. \ Complete_Partial_Order.chain orda Y; Y \ {} \ \ f (luba Y) = lubb (f ` Y))
\<Longrightarrow> cont luba orda lubb ordb f"
unfolding cont_def by blast
lemma contD:
"\ cont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \ {} \
\<Longrightarrow> f (luba Y) = lubb (f ` Y)"
unfolding cont_def by blast
lemma cont_id [simp, cont_intro]: "\Sup. cont Sup ord Sup ord id"
by(rule contI) simp
lemma cont_id' [simp, cont_intro]: "\Sup. cont Sup ord Sup ord (\x. x)"
using cont_id[unfolded id_def] .
lemma cont_applyI [cont_intro]:
assumes cont: "cont luba orda lubb ordb g"
shows "cont (fun_lub luba) (fun_ord orda) lubb ordb (\f. g (f x))"
by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont])
lemma call_cont: "cont (fun_lub lub) (fun_ord ord) lub ord (\f. f t)"
by(simp add: cont_def fun_lub_apply)
lemma cont_if [cont_intro]:
"\ cont luba orda lubb ordb f; cont luba orda lubb ordb g \
\<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
by(cases c) simp_all
lemma mcontI [intro?]:
"\ monotone orda ordb f; cont luba orda lubb ordb f \ \ mcont luba orda lubb ordb f"
by(simp add: mcont_def)
lemma mcont_mono: "mcont luba orda lubb ordb f \ monotone orda ordb f"
by(simp add: mcont_def)
lemma mcont_cont [simp]: "mcont luba orda lubb ordb f \ cont luba orda lubb ordb f"
by(simp add: mcont_def)
lemma mcont_monoD:
"\ mcont luba orda lubb ordb f; orda x y \ \ ordb (f x) (f y)"
by(auto simp add: mcont_def dest: monotoneD)
lemma mcont_contD:
"\ mcont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \ {} \
\<Longrightarrow> f (luba Y) = lubb (f ` Y)"
by(auto simp add: mcont_def dest: contD)
lemma mcont_call [cont_intro, simp]:
"mcont (fun_lub lub) (fun_ord ord) lub ord (\f. f t)"
by(simp add: mcont_def call_mono call_cont)
lemma mcont_id' [cont_intro, simp]: "mcont lub ord lub ord (\x. x)"
by(simp add: mcont_def monotone_id')
lemma mcont_applyI:
"mcont luba orda lubb ordb (\x. F x) \ mcont (fun_lub luba) (fun_ord orda) lubb ordb (\f. F (f x))"
by(simp add: mcont_def monotone_applyI cont_applyI)
lemma mcont_if [cont_intro, simp]:
"\ mcont luba orda lubb ordb (\x. f x); mcont luba orda lubb ordb (\x. g x) \
\<Longrightarrow> mcont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
by(simp add: mcont_def cont_if)
lemma cont_fun_lub_apply:
"cont luba orda (fun_lub lubb) (fun_ord ordb) f \ (\x. cont luba orda lubb ordb (\y. f y x))"
by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def)
lemma mcont_fun_lub_apply:
"mcont luba orda (fun_lub lubb) (fun_ord ordb) f \ (\x. mcont luba orda lubb ordb (\y. f y x))"
by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def)
context ccpo begin
lemma cont_const [simp, cont_intro]: "cont luba orda Sup (\) (\x. c)"
by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp)
lemma mcont_const [cont_intro, simp]:
"mcont luba orda Sup (\) (\x. c)"
by(simp add: mcont_def)
lemma cont_apply:
assumes 2: "\x. cont lubb ordb Sup (\) (\y. f x y)"
and t: "cont luba orda lubb ordb (\x. t x)"
and 1: "\y. cont luba orda Sup (\) (\x. f x y)"
and mono: "monotone orda ordb (\x. t x)"
and mono2: "\x. monotone ordb (\) (\y. f x y)"
and mono1: "\y. monotone orda (\) (\x. f x y)"
shows "cont luba orda Sup (\) (\x. f x (t x))"
proof
fix Y
assume chain: "Complete_Partial_Order.chain orda Y" and "Y \ {}"
moreover from chain have chain': "Complete_Partial_Order.chain ordb (t ` Y)"
by(rule chain_imageI)(rule monotoneD[OF mono])
ultimately show "f (luba Y) (t (luba Y)) = \((\x. f x (t x)) ` Y)"
by(simp add: contD[OF 1] contD[OF t] contD[OF 2] image_image)
(rule diag_Sup[OF chain], auto intro: monotone2monotone[OF mono2 mono monotone_const transpI] monotoneD[OF mono1])
qed
lemma mcont2mcont':
"\ \x. mcont lub' ord' Sup (\) (\y. f x y);
\<And>y. mcont lub ord Sup (\<le>) (\<lambda>x. f x y);
mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk>
\<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x (t x))"
unfolding mcont_def by(blast intro: transp_le monotone2monotone cont_apply)
lemma mcont2mcont:
"\mcont lub' ord' Sup (\) (\x. f x); mcont lub ord lub' ord' (\x. t x)\
\<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f (t x))"
by(rule mcont2mcont'[OF _ mcont_const])
context
fixes ord :: "'b \ 'b \ bool" (infix "\" 60)
and lub :: "'b set \ 'b" ("\")
begin
lemma cont_fun_lub_Sup:
assumes chainM: "Complete_Partial_Order.chain (fun_ord (\)) M"
and mcont [rule_format]: "\f\M. mcont lub (\) Sup (\) f"
shows "cont lub (\) Sup (\) (fun_lub Sup M)"
proof(rule contI)
fix Y
assume chain: "Complete_Partial_Order.chain (\) Y"
and Y: "Y \ {}"
from swap_Sup[OF chain chainM mcont[THEN mcont_mono]]
show "fun_lub Sup M (\Y) = \(fun_lub Sup M ` Y)"
by(simp add: mcont_contD[OF mcont chain Y] fun_lub_apply cong: image_cong)
qed
lemma mcont_fun_lub_Sup:
"\ Complete_Partial_Order.chain (fun_ord (\)) M;
\<forall>f\<in>M. mcont lub ord Sup (\<le>) f \<rbrakk>
\<Longrightarrow> mcont lub (\<sqsubseteq>) Sup (\<le>) (fun_lub Sup M)"
by(simp add: mcont_def cont_fun_lub_Sup mono_lub)
lemma iterates_mcont:
assumes f: "f \ ccpo.iterates (fun_lub Sup) (fun_ord (\)) F"
and mono: "\f. mcont lub (\) Sup (\) f \ mcont lub (\) Sup (\) (F f)"
shows "mcont lub (\) Sup (\) f"
using f
by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mcont_fun_lub_Sup)+
lemma fixp_preserves_mcont:
assumes mono: "\x. monotone (fun_ord (\)) (\) (\f. F f x)"
and mcont: "\f. mcont lub (\) Sup (\) f \ mcont lub (\) Sup (\) (F f)"
shows "mcont lub (\) Sup (\) (ccpo.fixp (fun_lub Sup) (fun_ord (\)) F)"
(is "mcont _ _ _ _ ?fixp")
unfolding mcont_def
proof(intro conjI monotoneI contI)
have mono: "monotone (fun_ord (\)) (fun_ord (\)) F"
by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])
let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord (\)) F"
have chain: "\x. Complete_Partial_Order.chain (\) ((\f. f x) ` ?iter)"
by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def)
{
fix x y
assume "x \ y"
show "?fixp x \ ?fixp y"
apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
using chain
proof(rule ccpo_Sup_least)
fix x'
assume "x' \ (\f. f x) ` ?iter"
then obtain f where "f \ ?iter" "x' = f x" by blast note this(2)
also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y"
by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]])
also have "f y \ \((\f. f y) ` ?iter)" using chain
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
finally show "x' \ \" .
qed
next
fix Y
assume chain: "Complete_Partial_Order.chain (\) Y"
and Y: "Y \ {}"
{ fix f
assume "f \ ?iter"
hence "f (\Y) = \(f ` Y)"
using mcont chain Y by(rule mcont_contD[OF iterates_mcont]) }
moreover have "\((\f. \(f ` Y)) ` ?iter) = \((\x. \((\f. f x) ` ?iter)) ` Y)"
using chain ccpo.chain_iterates[OF ccpo_fun mono]
by(rule swap_Sup)(rule mcont_mono[OF iterates_mcont[OF _ mcont]])
ultimately show "?fixp (\Y) = \(?fixp ` Y)" unfolding ccpo.fixp_def[OF ccpo_fun]
by(simp add: fun_lub_apply cong: image_cong)
}
qed
end
context
fixes F :: "'c \ 'c" and U :: "'c \ 'b \ 'a" and C :: "('b \ 'a) \ 'c" and f
assumes mono: "\x. monotone (fun_ord (\)) (\) (\f. U (F (C f)) x)"
and eq: "f \ C (ccpo.fixp (fun_lub Sup) (fun_ord (\)) (\f. U (F (C f))))"
and inverse: "\f. U (C f) = f"
begin
lemma fixp_preserves_mono_uc:
assumes mono2: "\f. monotone ord (\) (U f) \ monotone ord (\) (U (F f))"
shows "monotone ord (\) (U f)"
using fixp_preserves_mono[OF mono mono2] by(subst eq)(simp add: inverse)
lemma fixp_preserves_mcont_uc:
assumes mcont: "\f. mcont lubb ordb Sup (\) (U f) \ mcont lubb ordb Sup (\) (U (F f))"
shows "mcont lubb ordb Sup (\) (U f)"
using fixp_preserves_mcont[OF mono mcont] by(subst eq)(simp add: inverse)
end
lemmas fixp_preserves_mono1 = fixp_preserves_mono_uc[of "\x. x" _ "\x. x", OF _ _ refl]
lemmas fixp_preserves_mono2 =
fixp_preserves_mono_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
lemmas fixp_preserves_mono3 =
fixp_preserves_mono_uc[of "\f. case_prod (case_prod f)" _ "\f. curry (curry f)", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
lemmas fixp_preserves_mono4 =
fixp_preserves_mono_uc[of "\f. case_prod (case_prod (case_prod f))" _ "\f. curry (curry (curry f))", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
lemmas fixp_preserves_mcont1 = fixp_preserves_mcont_uc[of "\x. x" _ "\x. x", OF _ _ refl]
lemmas fixp_preserves_mcont2 =
fixp_preserves_mcont_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
lemmas fixp_preserves_mcont3 =
fixp_preserves_mcont_uc[of "\f. case_prod (case_prod f)" _ "\f. curry (curry f)", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
lemmas fixp_preserves_mcont4 =
fixp_preserves_mcont_uc[of "\f. case_prod (case_prod (case_prod f))" _ "\f. curry (curry (curry f))", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
end
lemma (in preorder) monotone_if_bot:
fixes bot
assumes mono: "\x y. \ x \ y; \ (x \ bound) \ \ ord (f x) (f y)"
and bot: "\x. \ x \ bound \ ord bot (f x)" "ord bot bot"
shows "monotone (\) ord (\x. if x \ bound then bot else f x)"
by(rule monotoneI)(auto intro: bot intro: mono order_trans)
lemma (in ccpo) mcont_if_bot:
fixes bot and lub ("\") and ord (infix "\" 60)
assumes ccpo: "class.ccpo lub (\) lt"
and mono: "\x y. \ x \ y; \ x \ bound \ \ f x \ f y"
and cont: "\Y. \ Complete_Partial_Order.chain (\) Y; Y \ {}; \x. x \ Y \ \ x \ bound \ \ f (\Y) = \(f ` Y)"
and bot: "\x. \ x \ bound \ bot \ f x"
shows "mcont Sup (\) lub (\) (\x. if x \ bound then bot else f x)" (is "mcont _ _ _ _ ?g")
proof(intro mcontI contI)
interpret c: ccpo lub "(\)" lt by(fact ccpo)
show "monotone (\) (\) ?g" by(rule monotone_if_bot)(simp_all add: mono bot)
fix Y
assume chain: "Complete_Partial_Order.chain (\) Y" and Y: "Y \ {}"
show "?g (\Y) = \(?g ` Y)"
proof(cases "Y \ {x. x \ bound}")
case True
hence "\Y \ bound" using chain by(auto intro: ccpo_Sup_least)
moreover have "Y \ {x. \ x \ bound} = {}" using True by auto
ultimately show ?thesis using True Y
by (auto simp add: image_constant_conv cong del: c.SUP_cong_simp)
next
case False
let ?Y = "Y \ {x. \ x \ bound}"
have chain': "Complete_Partial_Order.chain (\) ?Y"
using chain by(rule chain_subset) simp
from False obtain y where ybound: "\ y \ bound" and y: "y \ Y" by blast
hence "\ \Y \ bound" by (metis ccpo_Sup_upper chain order.trans)
hence "?g (\Y) = f (\Y)" by simp
also have "\Y \ \?Y" using chain
proof(rule ccpo_Sup_least)
fix x
assume x: "x \ Y"
show "x \ \?Y"
proof(cases "x \ bound")
case True
with chainD[OF chain x y] have "x \ y" using ybound by(auto intro: order_trans)
thus ?thesis by(rule order_trans)(auto intro: ccpo_Sup_upper[OF chain'] simp add: y ybound)
qed(auto intro: ccpo_Sup_upper[OF chain'] simp add: x)
qed
hence "\Y = \?Y" by(rule antisym)(blast intro: ccpo_Sup_least[OF chain'] ccpo_Sup_upper[OF chain])
hence "f (\Y) = f (\?Y)" by simp
also have "f (\?Y) = \(f ` ?Y)" using chain' by(rule cont)(insert y ybound, auto)
also have "\(f ` ?Y) = \(?g ` Y)"
proof(cases "Y \ {x. x \ bound} = {}")
case True
hence "f ` ?Y = ?g ` Y" by auto
thus ?thesis by(rule arg_cong)
next
case False
have chain'': "Complete_Partial_Order.chain (\) (insert bot (f ` ?Y))"
using chain by(auto intro!: chainI bot dest: chainD intro: mono)
hence chain''': "Complete_Partial_Order.chain (\) (f ` ?Y)" by(rule chain_subset) blast
have "bot \ \(f ` ?Y)" using y ybound by(blast intro: c.order_trans[OF bot] c.ccpo_Sup_upper[OF chain'''])
hence "\(insert bot (f ` ?Y)) \ \(f ` ?Y)" using chain''
by(auto intro: c.ccpo_Sup_least c.ccpo_Sup_upper[OF chain'''])
with _ have "\ = \(insert bot (f ` ?Y))"
by(rule c.antisym)(blast intro: c.ccpo_Sup_least[OF chain'''] c.ccpo_Sup_upper[OF chain''])
also have "insert bot (f ` ?Y) = ?g ` Y" using False by auto
finally show ?thesis .
qed
finally show ?thesis .
qed
qed
context partial_function_definitions begin
lemma mcont_const [cont_intro, simp]:
"mcont luba orda lub leq (\x. c)"
by(rule ccpo.mcont_const)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
lemmas [cont_intro, simp] =
ccpo.cont_const[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
lemma mono2mono:
assumes "monotone ordb leq (\y. f y)" "monotone orda ordb (\x. t x)"
shows "monotone orda leq (\x. f (t x))"
using assms by(rule monotone2monotone) simp_all
lemmas mcont2mcont' = ccpo.mcont2mcont'[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
lemmas mcont2mcont = ccpo.mcont2mcont[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
lemmas fixp_preserves_mono1 = ccpo.fixp_preserves_mono1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
lemmas fixp_preserves_mono2 = ccpo.fixp_preserves_mono2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
lemmas fixp_preserves_mono3 = ccpo.fixp_preserves_mono3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
lemmas fixp_preserves_mono4 = ccpo.fixp_preserves_mono4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
lemmas fixp_preserves_mcont1 = ccpo.fixp_preserves_mcont1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
lemmas fixp_preserves_mcont2 = ccpo.fixp_preserves_mcont2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
lemmas fixp_preserves_mcont3 = ccpo.fixp_preserves_mcont3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
lemmas fixp_preserves_mcont4 = ccpo.fixp_preserves_mcont4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
lemma monotone_if_bot:
fixes bot
assumes g: "\x. g x = (if leq x bound then bot else f x)"
and mono: "\x y. \ leq x y; \ leq x bound \ \ ord (f x) (f y)"
and bot: "\x. \ leq x bound \ ord bot (f x)" "ord bot bot"
shows "monotone leq ord g"
unfolding g[abs_def] using preorder mono bot by(rule preorder.monotone_if_bot)
lemma mcont_if_bot:
fixes bot
assumes ccpo: "class.ccpo lub' ord (mk_less ord)"
and bot: "\x. \ leq x bound \ ord bot (f x)"
and g: "\x. g x = (if leq x bound then bot else f x)"
and mono: "\x y. \ leq x y; \ leq x bound \ \ ord (f x) (f y)"
and cont: "\Y. \ Complete_Partial_Order.chain leq Y; Y \ {}; \x. x \ Y \ \ leq x bound \ \ f (lub Y) = lub' (f ` Y)"
shows "mcont lub leq lub' ord g"
unfolding g[abs_def] using ccpo mono cont bot by(rule ccpo.mcont_if_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]])
end
subsection \<open>Admissibility\<close>
lemma admissible_subst:
assumes adm: "ccpo.admissible luba orda (\x. P x)"
and mcont: "mcont lubb ordb luba orda f"
shows "ccpo.admissible lubb ordb (\x. P (f x))"
apply(rule ccpo.admissibleI)
apply(frule (1) mcont_contD[OF mcont])
apply(auto intro: ccpo.admissibleD[OF adm] chain_imageI dest: mcont_monoD[OF mcont])
done
lemmas [simp, cont_intro] =
admissible_all
admissible_ball
admissible_const
admissible_conj
lemma admissible_disj' [simp, cont_intro]:
"\ class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord P; ccpo.admissible lub ord Q \
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<or> Q x)"
by(rule ccpo.admissible_disj)
lemma admissible_imp' [cont_intro]:
"\ class.ccpo lub ord (mk_less ord);
ccpo.admissible lub ord (\<lambda>x. \<not> P x);
ccpo.admissible lub ord (\<lambda>x. Q x) \<rbrakk>
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x)"
unfolding imp_conv_disj by(rule ccpo.admissible_disj)
lemma admissible_imp [cont_intro]:
"(Q \ ccpo.admissible lub ord (\x. P x))
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. Q \<longrightarrow> P x)"
by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD)
lemma admissible_not_mem' [THEN admissible_subst, cont_intro, simp]:
shows admissible_not_mem: "ccpo.admissible Union (\) (\A. x \ A)"
by(rule ccpo.admissibleI) auto
lemma admissible_eqI:
assumes f: "cont luba orda lub ord (\x. f x)"
and g: "cont luba orda lub ord (\x. g x)"
shows "ccpo.admissible luba orda (\x. f x = g x)"
apply(rule ccpo.admissibleI)
apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong)
done
corollary admissible_eq_mcontI [cont_intro]:
"\ mcont luba orda lub ord (\x. f x);
mcont luba orda lub ord (\<lambda>x. g x) \<rbrakk>
\<Longrightarrow> ccpo.admissible luba orda (\<lambda>x. f x = g x)"
by(rule admissible_eqI)(auto simp add: mcont_def)
lemma admissible_iff [cont_intro, simp]:
"\ ccpo.admissible lub ord (\x. P x \ Q x); ccpo.admissible lub ord (\x. Q x \ P x) \
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longleftrightarrow> Q x)"
by(subst iff_conv_conj_imp)(rule admissible_conj)
context ccpo begin
lemma admissible_leI:
assumes f: "mcont luba orda Sup (\) (\x. f x)"
and g: "mcont luba orda Sup (\) (\x. g x)"
shows "ccpo.admissible luba orda (\x. f x \ g x)"
proof(rule ccpo.admissibleI)
fix A
assume chain: "Complete_Partial_Order.chain orda A"
and le: "\x\A. f x \ g x"
and False: "A \ {}"
have "f (luba A) = \(f ` A)" by(simp add: mcont_contD[OF f] chain False)
also have "\ \ \(g ` A)"
proof(rule ccpo_Sup_least)
from chain show "Complete_Partial_Order.chain (\) (f ` A)"
by(rule chain_imageI)(rule mcont_monoD[OF f])
fix x
assume "x \ f ` A"
then obtain y where "y \ A" "x = f y" by blast note this(2)
also have "f y \ g y" using le \y \ A\ by simp
also have "Complete_Partial_Order.chain (\) (g ` A)"
using chain by(rule chain_imageI)(rule mcont_monoD[OF g])
hence "g y \ \(g ` A)" by(rule ccpo_Sup_upper)(simp add: \y \ A\)
finally show "x \ \" .
qed
also have "\ = g (luba A)" by(simp add: mcont_contD[OF g] chain False)
finally show "f (luba A) \ g (luba A)" .
qed
end
lemma admissible_leI:
fixes ord (infix "\" 60) and lub ("\")
assumes "class.ccpo lub (\) (mk_less (\))"
and "mcont luba orda lub (\) (\x. f x)"
and "mcont luba orda lub (\) (\x. g x)"
shows "ccpo.admissible luba orda (\x. f x \ g x)"
using assms by(rule ccpo.admissible_leI)
declare ccpo_class.admissible_leI[cont_intro]
context ccpo begin
lemma admissible_not_below: "ccpo.admissible Sup (\) (\x. \ (\) x y)"
by(rule ccpo.admissibleI)(simp add: ccpo_Sup_below_iff)
end
lemma (in preorder) preorder [cont_intro, simp]: "class.preorder (\) (mk_less (\))"
by(unfold_locales)(auto simp add: mk_less_def intro: order_trans)
context partial_function_definitions begin
lemmas [cont_intro, simp] =
admissible_leI[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
ccpo.admissible_not_below[THEN admissible_subst, OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
end
setup \<open>Sign.map_naming (Name_Space.mandatory_path "ccpo")\<close>
inductive compact :: "('a set \ 'a) \ ('a \ 'a \ bool) \ 'a \ bool"
for lub ord x
where compact:
"\ ccpo.admissible lub ord (\y. \ ord x y);
ccpo.admissible lub ord (\<lambda>y. x \<noteq> y) \<rbrakk>
\<Longrightarrow> compact lub ord x"
setup \<open>Sign.map_naming Name_Space.parent_path\<close>
context ccpo begin
lemma compactI:
assumes "ccpo.admissible Sup (\) (\y. \ x \ y)"
shows "ccpo.compact Sup (\) x"
using assms
proof(rule ccpo.compact.intros)
have neq: "(\y. x \ y) = (\y. \ x \ y \ \ y \ x)" by(auto)
show "ccpo.admissible Sup (\) (\y. x \ y)"
by(subst neq)(rule admissible_disj admissible_not_below assms)+
qed
lemma compact_bot:
assumes "x = Sup {}"
shows "ccpo.compact Sup (\) x"
proof(rule compactI)
show "ccpo.admissible Sup (\) (\y. \ x \ y)" using assms
by(auto intro!: ccpo.admissibleI intro: ccpo_Sup_least chain_empty)
qed
end
lemma admissible_compact_neq' [THEN admissible_subst, cont_intro, simp]:
shows admissible_compact_neq: "ccpo.compact lub ord k \ ccpo.admissible lub ord (\x. k \ x)"
by(simp add: ccpo.compact.simps)
lemma admissible_neq_compact' [THEN admissible_subst, cont_intro, simp]:
shows admissible_neq_compact: "ccpo.compact lub ord k \ ccpo.admissible lub ord (\x. x \ k)"
by(subst eq_commute)(rule admissible_compact_neq)
context partial_function_definitions begin
lemmas [cont_intro, simp] = ccpo.compact_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
end
context ccpo begin
lemma fixp_strong_induct:
assumes [cont_intro]: "ccpo.admissible Sup (\) P"
and mono: "monotone (\) (\) f"
and bot: "P (\{})"
and step: "\x. \ x \ ccpo_class.fixp f; P x \ \ P (f x)"
shows "P (ccpo_class.fixp f)"
proof(rule fixp_induct[where P="\x. x \ ccpo_class.fixp f \ P x", THEN conjunct2])
note [cont_intro] = admissible_leI
show "ccpo.admissible Sup (\) (\x. x \ ccpo_class.fixp f \ P x)" by simp
next
show "\{} \ ccpo_class.fixp f \ P (\{})"
by(auto simp add: bot intro: ccpo_Sup_least chain_empty)
next
fix x
assume "x \ ccpo_class.fixp f \ P x"
thus "f x \ ccpo_class.fixp f \ P (f x)"
by(subst fixp_unfold[OF mono])(auto dest: monotoneD[OF mono] intro: step)
qed(rule mono)
end
context partial_function_definitions begin
lemma fixp_strong_induct_uc:
fixes F :: "'c \ 'c"
and U :: "'c \ 'b \ 'a"
and C :: "('b \ 'a) \ 'c"
and P :: "('b \ 'a) \ bool"
assumes mono: "\x. mono_body (\f. U (F (C f)) x)"
and eq: "f \ C (fixp_fun (\f. U (F (C f))))"
and inverse: "\f. U (C f) = f"
and adm: "ccpo.admissible lub_fun le_fun P"
and bot: "P (\_. lub {})"
and step: "\f'. \ P (U f'); le_fun (U f') (U f) \ \ P (U (F f'))"
shows "P (U f)"
unfolding eq inverse
apply (rule ccpo.fixp_strong_induct[OF ccpo adm])
apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
apply (rule_tac f'5="C x" in step)
apply (simp_all add: inverse eq)
done
end
subsection \<open>\<^term>\<open>(=)\<close> as order\<close>
definition lub_singleton :: "('a set \ 'a) \ bool"
where "lub_singleton lub \ (\a. lub {a} = a)"
definition the_Sup :: "'a set \ 'a"
where "the_Sup A = (THE a. a \ A)"
lemma lub_singleton_the_Sup [cont_intro, simp]: "lub_singleton the_Sup"
by(simp add: lub_singleton_def the_Sup_def)
lemma (in ccpo) lub_singleton: "lub_singleton Sup"
by(simp add: lub_singleton_def)
lemma (in partial_function_definitions) lub_singleton [cont_intro, simp]: "lub_singleton lub"
by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
lemma preorder_eq [cont_intro, simp]:
"class.preorder (=) (mk_less (=))"
by(unfold_locales)(simp_all add: mk_less_def)
lemma monotone_eqI [cont_intro]:
assumes "class.preorder ord (mk_less ord)"
shows "monotone (=) ord f"
proof -
interpret preorder ord "mk_less ord" by fact
show ?thesis by(simp add: monotone_def)
qed
lemma cont_eqI [cont_intro]:
fixes f :: "'a \ 'b"
assumes "lub_singleton lub"
shows "cont the_Sup (=) lub ord f"
proof(rule contI)
fix Y :: "'a set"
assume "Complete_Partial_Order.chain (=) Y" "Y \ {}"
then obtain a where "Y = {a}" by(auto simp add: chain_def)
thus "f (the_Sup Y) = lub (f ` Y)" using assms
by(simp add: the_Sup_def lub_singleton_def)
qed
lemma mcont_eqI [cont_intro, simp]:
"\ class.preorder ord (mk_less ord); lub_singleton lub \
\<Longrightarrow> mcont the_Sup (=) lub ord f"
by(simp add: mcont_def cont_eqI monotone_eqI)
subsection \<open>ccpo for products\<close>
definition prod_lub :: "('a set \ 'a) \ ('b set \ 'b) \ ('a \ 'b) set \ 'a \ 'b"
where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
lemma lub_singleton_prod_lub [cont_intro, simp]:
"\ lub_singleton luba; lub_singleton lubb \ \ lub_singleton (prod_lub luba lubb)"
by(simp add: lub_singleton_def prod_lub_def)
lemma prod_lub_empty [simp]: "prod_lub luba lubb {} = (luba {}, lubb {})"
by(simp add: prod_lub_def)
lemma preorder_rel_prodI [cont_intro, simp]:
assumes "class.preorder orda (mk_less orda)"
and "class.preorder ordb (mk_less ordb)"
shows "class.preorder (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
proof -
interpret a: preorder orda "mk_less orda" by fact
interpret b: preorder ordb "mk_less ordb" by fact
show ?thesis by(unfold_locales)(auto simp add: mk_less_def intro: a.order_trans b.order_trans)
qed
lemma order_rel_prodI:
assumes a: "class.order orda (mk_less orda)"
and b: "class.order ordb (mk_less ordb)"
shows "class.order (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
(is "class.order ?ord ?ord'")
proof(intro class.order.intro class.order_axioms.intro)
interpret a: order orda "mk_less orda" by(fact a)
interpret b: order ordb "mk_less ordb" by(fact b)
show "class.preorder ?ord ?ord'" by(rule preorder_rel_prodI) unfold_locales
fix x y
assume "?ord x y" "?ord y x"
thus "x = y" by(cases x y rule: prod.exhaust[case_product prod.exhaust]) auto
qed
lemma monotone_rel_prodI:
assumes mono2: "\a. monotone ordb ordc (\b. f (a, b))"
and mono1: "\b. monotone orda ordc (\a. f (a, b))"
and a: "class.preorder orda (mk_less orda)"
and b: "class.preorder ordb (mk_less ordb)"
and c: "class.preorder ordc (mk_less ordc)"
shows "monotone (rel_prod orda ordb) ordc f"
proof -
interpret a: preorder orda "mk_less orda" by(rule a)
interpret b: preorder ordb "mk_less ordb" by(rule b)
interpret c: preorder ordc "mk_less ordc" by(rule c)
show ?thesis using mono2 mono1
by(auto 7 2 simp add: monotone_def intro: c.order_trans)
qed
lemma monotone_rel_prodD1:
assumes mono: "monotone (rel_prod orda ordb) ordc f"
and preorder: "class.preorder ordb (mk_less ordb)"
shows "monotone orda ordc (\a. f (a, b))"
proof -
interpret preorder ordb "mk_less ordb" by(rule preorder)
show ?thesis using mono by(simp add: monotone_def)
qed
lemma monotone_rel_prodD2:
assumes mono: "monotone (rel_prod orda ordb) ordc f"
and preorder: "class.preorder orda (mk_less orda)"
shows "monotone ordb ordc (\b. f (a, b))"
proof -
interpret preorder orda "mk_less orda" by(rule preorder)
show ?thesis using mono by(simp add: monotone_def)
qed
lemma monotone_case_prodI:
"\ \a. monotone ordb ordc (f a); \b. monotone orda ordc (\a. f a b);
class.preorder orda (mk_less orda); class.preorder ordb (mk_less ordb);
class.preorder ordc (mk_less ordc) \<rbrakk>
\<Longrightarrow> monotone (rel_prod orda ordb) ordc (case_prod f)"
by(rule monotone_rel_prodI) simp_all
lemma monotone_case_prodD1:
assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
and preorder: "class.preorder ordb (mk_less ordb)"
shows "monotone orda ordc (\a. f a b)"
using monotone_rel_prodD1[OF assms] by simp
lemma monotone_case_prodD2:
assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
and preorder: "class.preorder orda (mk_less orda)"
shows "monotone ordb ordc (f a)"
using monotone_rel_prodD2[OF assms] by simp
context
fixes orda ordb ordc
assumes a: "class.preorder orda (mk_less orda)"
and b: "class.preorder ordb (mk_less ordb)"
and c: "class.preorder ordc (mk_less ordc)"
begin
lemma monotone_rel_prod_iff:
"monotone (rel_prod orda ordb) ordc f \
(\<forall>a. monotone ordb ordc (\<lambda>b. f (a, b))) \<and>
(\<forall>b. monotone orda ordc (\<lambda>a. f (a, b)))"
using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2)
lemma monotone_case_prod_iff [simp]:
"monotone (rel_prod orda ordb) ordc (case_prod f) \
(\<forall>a. monotone ordb ordc (f a)) \<and> (\<forall>b. monotone orda ordc (\<lambda>a. f a b))"
by(simp add: monotone_rel_prod_iff)
end
lemma monotone_case_prod_apply_iff:
"monotone orda ordb (\x. (case_prod f x) y) \ monotone orda ordb (case_prod (\a b. f a b y))"
by(simp add: monotone_def)
lemma monotone_case_prod_applyD:
"monotone orda ordb (\x. (case_prod f x) y)
\<Longrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
by(simp add: monotone_case_prod_apply_iff)
lemma monotone_case_prod_applyI:
"monotone orda ordb (case_prod (\a b. f a b y))
\<Longrightarrow> monotone orda ordb (\<lambda>x. (case_prod f x) y)"
by(simp add: monotone_case_prod_apply_iff)
lemma cont_case_prod_apply_iff:
"cont luba orda lubb ordb (\x. (case_prod f x) y) \ cont luba orda lubb ordb (case_prod (\a b. f a b y))"
by(simp add: cont_def split_def)
lemma cont_case_prod_applyI:
"cont luba orda lubb ordb (case_prod (\a b. f a b y))
\<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)"
by(simp add: cont_case_prod_apply_iff)
lemma cont_case_prod_applyD:
"cont luba orda lubb ordb (\x. (case_prod f x) y)
\<Longrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
by(simp add: cont_case_prod_apply_iff)
lemma mcont_case_prod_apply_iff [simp]:
"mcont luba orda lubb ordb (\x. (case_prod f x) y) \
mcont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
by(simp add: mcont_def monotone_case_prod_apply_iff cont_case_prod_apply_iff)
lemma cont_prodD1:
assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f"
and "class.preorder orda (mk_less orda)"
and luba: "lub_singleton luba"
shows "cont lubb ordb lubc ordc (\y. f (x, y))"
proof(rule contI)
interpret preorder orda "mk_less orda" by fact
fix Y :: "'b set"
let ?Y = "{x} \ Y"
assume "Complete_Partial_Order.chain ordb Y" "Y \ {}"
hence "Complete_Partial_Order.chain (rel_prod orda ordb) ?Y" "?Y \ {}"
by(simp_all add: chain_def)
with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
moreover have "f ` ?Y = (\y. f (x, y)) ` Y" by auto
ultimately show "f (x, lubb Y) = lubc ((\y. f (x, y)) ` Y)" using luba
by(simp add: prod_lub_def \<open>Y \<noteq> {}\<close> lub_singleton_def)
qed
lemma cont_prodD2:
assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f"
and "class.preorder ordb (mk_less ordb)"
and lubb: "lub_singleton lubb"
shows "cont luba orda lubc ordc (\x. f (x, y))"
proof(rule contI)
interpret preorder ordb "mk_less ordb" by fact
fix Y
assume Y: "Complete_Partial_Order.chain orda Y" "Y \ {}"
let ?Y = "Y \ {y}"
have "f (luba Y, y) = f (prod_lub luba lubb ?Y)"
using lubb by(simp add: prod_lub_def Y lub_singleton_def)
also from Y have "Complete_Partial_Order.chain (rel_prod orda ordb) ?Y" "?Y \ {}"
by(simp_all add: chain_def)
with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
also have "f ` ?Y = (\x. f (x, y)) ` Y" by auto
finally show "f (luba Y, y) = lubc \" .
qed
lemma cont_case_prodD1:
assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)"
and "class.preorder orda (mk_less orda)"
and "lub_singleton luba"
shows "cont lubb ordb lubc ordc (f x)"
using cont_prodD1[OF assms] by simp
lemma cont_case_prodD2:
assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)"
and "class.preorder ordb (mk_less ordb)"
and "lub_singleton lubb"
shows "cont luba orda lubc ordc (\x. f x y)"
using cont_prodD2[OF assms] by simp
context ccpo begin
lemma cont_prodI:
assumes mono: "monotone (rel_prod orda ordb) (\) f"
and cont1: "\x. cont lubb ordb Sup (\) (\y. f (x, y))"
and cont2: "\y. cont luba orda Sup (\) (\x. f (x, y))"
and "class.preorder orda (mk_less orda)"
and "class.preorder ordb (mk_less ordb)"
shows "cont (prod_lub luba lubb) (rel_prod orda ordb) Sup (\) f"
proof(rule contI)
interpret a: preorder orda "mk_less orda" by fact
interpret b: preorder ordb "mk_less ordb" by fact
fix Y
assume chain: "Complete_Partial_Order.chain (rel_prod orda ordb) Y"
and "Y \ {}"
have "f (prod_lub luba lubb Y) = f (luba (fst ` Y), lubb (snd ` Y))"
by(simp add: prod_lub_def)
also from cont2 have "f (luba (fst ` Y), lubb (snd ` Y)) = \((\x. f (x, lubb (snd ` Y))) ` fst ` Y)"
by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] \<open>Y \<noteq> {}\<close>)
also from cont1 have "\x. f (x, lubb (snd ` Y)) = \((\y. f (x, y)) ` snd ` Y)"
by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] \<open>Y \<noteq> {}\<close>)
hence "\((\x. f (x, lubb (snd ` Y))) ` fst ` Y) = \((\x. \ x) ` fst ` Y)" by simp
also have "\ = \((\x. f (fst x, snd x)) ` Y)"
unfolding image_image split_def using chain
apply(rule diag_Sup)
using monotoneD[OF mono]
by(auto intro: monotoneI)
finally show "f (prod_lub luba lubb Y) = \(f ` Y)" by simp
qed
lemma cont_case_prodI:
assumes "monotone (rel_prod orda ordb) (\) (case_prod f)"
and "\x. cont lubb ordb Sup (\) (\y. f x y)"
and "\y. cont luba orda Sup (\) (\x. f x y)"
and "class.preorder orda (mk_less orda)"
and "class.preorder ordb (mk_less ordb)"
shows "cont (prod_lub luba lubb) (rel_prod orda ordb) Sup (\) (case_prod f)"
by(rule cont_prodI)(simp_all add: assms)
lemma cont_case_prod_iff:
"\ monotone (rel_prod orda ordb) (\) (case_prod f);
class.preorder orda (mk_less orda); lub_singleton luba;
class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
\<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) Sup (\<le>) (case_prod f) \<longleftrightarrow>
(\<forall>x. cont lubb ordb Sup (\<le>) (\<lambda>y. f x y)) \<and> (\<forall>y. cont luba orda Sup (\<le>) (\<lambda>x. f x y))"
by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
end
context partial_function_definitions begin
lemma mono2mono2:
assumes f: "monotone (rel_prod ordb ordc) leq (\(x, y). f x y)"
and t: "monotone orda ordb (\x. t x)"
and t': "monotone orda ordc (\x. t' x)"
shows "monotone orda leq (\x. f (t x) (t' x))"
proof(rule monotoneI)
fix x y
assume "orda x y"
hence "rel_prod ordb ordc (t x, t' x) (t y, t' y)"
using t t' by(auto dest: monotoneD)
from monotoneD[OF f this] show "leq (f (t x) (t' x)) (f (t y) (t' y))" by simp
qed
lemma cont_case_prodI [cont_intro]:
"\ monotone (rel_prod orda ordb) leq (case_prod f);
\<And>x. cont lubb ordb lub leq (\<lambda>y. f x y);
\<And>y. cont luba orda lub leq (\<lambda>x. f x y);
class.preorder orda (mk_less orda);
class.preorder ordb (mk_less ordb) \<rbrakk>
\<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f)"
by(rule ccpo.cont_case_prodI)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
lemma cont_case_prod_iff:
"\ monotone (rel_prod orda ordb) leq (case_prod f);
class.preorder orda (mk_less orda); lub_singleton luba;
class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
\<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
(\<forall>x. cont lubb ordb lub leq (\<lambda>y. f x y)) \<and> (\<forall>y. cont luba orda lub leq (\<lambda>x. f x y))"
by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
lemma mcont_case_prod_iff [simp]:
"\ class.preorder orda (mk_less orda); lub_singleton luba;
class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
\<Longrightarrow> mcont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
(\<forall>x. mcont lubb ordb lub leq (\<lambda>y. f x y)) \<and> (\<forall>y. mcont luba orda lub leq (\<lambda>x. f x y))"
unfolding mcont_def by(auto simp add: cont_case_prod_iff)
end
lemma mono2mono_case_prod [cont_intro]:
assumes "\x y. monotone orda ordb (\f. pair f x y)"
shows "monotone orda ordb (\f. case_prod (pair f) x)"
by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
subsection \<open>Complete lattices as ccpo\<close>
context complete_lattice begin
lemma complete_lattice_ccpo: "class.ccpo Sup (\) (<)"
by(unfold_locales)(fast intro: Sup_upper Sup_least)+
lemma complete_lattice_ccpo': "class.ccpo Sup (\) (mk_less (\))"
by(unfold_locales)(auto simp add: mk_less_def intro: Sup_upper Sup_least)
lemma complete_lattice_partial_function_definitions:
"partial_function_definitions (\) Sup"
by(unfold_locales)(auto intro: Sup_least Sup_upper)
lemma complete_lattice_partial_function_definitions_dual:
"partial_function_definitions (\) Inf"
by(unfold_locales)(auto intro: Inf_lower Inf_greatest)
lemmas [cont_intro, simp] =
Partial_Function.ccpo[OF complete_lattice_partial_function_definitions]
Partial_Function.ccpo[OF complete_lattice_partial_function_definitions_dual]
lemma mono2mono_inf:
assumes f: "monotone ord (\) (\x. f x)"
and g: "monotone ord (\) (\x. g x)"
shows "monotone ord (\) (\x. f x \ g x)"
by(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] intro: le_infI1 le_infI2 intro!: monotoneI)
lemma mcont_const [simp]: "mcont lub ord Sup (\) (\_. c)"
by(rule ccpo.mcont_const[OF complete_lattice_ccpo])
lemma mono2mono_sup:
assumes f: "monotone ord (\) (\x. f x)"
and g: "monotone ord (\) (\x. g x)"
shows "monotone ord (\) (\x. f x \ g x)"
by(auto 4 3 intro!: monotoneI intro: sup.coboundedI1 sup.coboundedI2 dest: monotoneD[OF f] monotoneD[OF g])
lemma Sup_image_sup:
assumes "Y \ {}"
shows "\((\) x ` Y) = x \ \Y"
proof(rule Sup_eqI)
fix y
assume "y \ (\) x ` Y"
then obtain z where "y = x \ z" and "z \ Y" by blast
from \<open>z \<in> Y\<close> have "z \<le> \<Squnion>Y" by(rule Sup_upper)
with _ show "y \ x \ \Y" unfolding \y = x \ z\ by(rule sup_mono) simp
next
fix y
assume upper: "\z. z \ (\) x ` Y \ z \ y"
show "x \ \Y \ y" unfolding Sup_insert[symmetric]
proof(rule Sup_least)
fix z
assume "z \ insert x Y"
from assms obtain z' where "z' \<in> Y" by blast
let ?z = "if z \ Y then x \ z else x \ z'"
have "z \ x \ ?z" using \z' \ Y\ \z \ insert x Y\ by auto
also have "\ \ y" by(rule upper)(auto split: if_split_asm intro: \z' \ Y\)
finally show "z \ y" .
qed
qed
lemma mcont_sup1: "mcont Sup (\) Sup (\) (\y. x \ y)"
by(auto 4 3 simp add: mcont_def sup.coboundedI1 sup.coboundedI2 intro!: monotoneI contI intro: Sup_image_sup[symmetric])
lemma mcont_sup2: "mcont Sup (\) Sup (\) (\x. x \ y)"
by(subst sup_commute)(rule mcont_sup1)
lemma mcont2mcont_sup [cont_intro, simp]:
"\ mcont lub ord Sup (\) (\x. f x);
mcont lub ord Sup (\<le>) (\<lambda>x. g x) \<rbrakk>
\<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x \<squnion> g x)"
by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_sup1 mcont_sup2 ccpo.mcont_const[OF complete_lattice_ccpo])
end
lemmas [cont_intro] = admissible_leI[OF complete_lattice_ccpo']
context complete_distrib_lattice begin
lemma mcont_inf1: "mcont Sup (\) Sup (\) (\y. x \ y)"
by(auto intro: monotoneI contI simp add: le_infI2 inf_Sup mcont_def)
lemma mcont_inf2: "mcont Sup (\) Sup (\) (\x. x \ y)"
by(auto intro: monotoneI contI simp add: le_infI1 Sup_inf mcont_def)
lemma mcont2mcont_inf [cont_intro, simp]:
"\ mcont lub ord Sup (\) (\x. f x);
mcont lub ord Sup (\<le>) (\<lambda>x. g x) \<rbrakk>
\<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x \<sqinter> g x)"
by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_inf1 mcont_inf2 ccpo.mcont_const[OF complete_lattice_ccpo])
end
interpretation lfp: partial_function_definitions "(\) :: _ :: complete_lattice \ _" Sup
by(rule complete_lattice_partial_function_definitions)
declaration \<open>Partial_Function.init "lfp" \<^term>\<open>lfp.fixp_fun\<close> \<^term>\<open>lfp.mono_body\<close>
@{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE\<close>
interpretation gfp: partial_function_definitions "(\) :: _ :: complete_lattice \ _" Inf
by(rule complete_lattice_partial_function_definitions_dual)
declaration \<open>Partial_Function.init "gfp" \<^term>\<open>gfp.fixp_fun\<close> \<^term>\<open>gfp.mono_body\<close>
@{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE\<close>
lemma insert_mono [partial_function_mono]:
"monotone (fun_ord (\)) (\) A \ monotone (fun_ord (\)) (\) (\y. insert x (A y))"
by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
lemma mono2mono_insert [THEN lfp.mono2mono, cont_intro, simp]:
shows monotone_insert: "monotone (\) (\) (insert x)"
by(rule monotoneI) blast
lemma mcont2mcont_insert[THEN lfp.mcont2mcont, cont_intro, simp]:
shows mcont_insert: "mcont Union (\) Union (\) (insert x)"
by(blast intro: mcontI contI monotone_insert)
lemma mono2mono_image [THEN lfp.mono2mono, cont_intro, simp]:
shows monotone_image: "monotone (\) (\) ((`) f)"
by(rule monotoneI) blast
lemma cont_image: "cont Union (\) Union (\) ((`) f)"
by(rule contI)(auto)
lemma mcont2mcont_image [THEN lfp.mcont2mcont, cont_intro, simp]:
shows mcont_image: "mcont Union (\) Union (\) ((`) f)"
by(blast intro: mcontI monotone_image cont_image)
context complete_lattice begin
lemma monotone_Sup [cont_intro, simp]:
"monotone ord (\) f \ monotone ord (\) (\x. \f x)"
by(blast intro: monotoneI Sup_least Sup_upper dest: monotoneD)
lemma cont_Sup:
assumes "cont lub ord Union (\) f"
shows "cont lub ord Sup (\) (\x. \f x)"
apply(rule contI)
apply(simp add: contD[OF assms])
apply(blast intro: Sup_least Sup_upper order_trans antisym)
done
lemma mcont_Sup: "mcont lub ord Union (\) f \ mcont lub ord Sup (\) (\x. \f x)"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.68 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
