Quelle Complete_Partial_Order2.thy Sprache: Isabelle

(*  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
begin

unbundle lattice_syntax

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 order.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 (meson local.ccpo_Sup_least local.ccpo_Sup_upper local.dual_order.trans)

lemma Sup_minus_bot:
  assumes chain: "Complete_Partial_Order.chain (\) A"
  shows "\(A - {\{}}) = \A"
    (is "?lhs = ?rhs")
proof (rule order.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 \<open>\<sqsubseteq>\<close> 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 \<open>\<sqsubseteq>\<close> 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 order.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
    then show "y \ ?lhs"
      by (metis (no_types, lifting) chain1 chain2 imageI ccpo_Sup_upper order.trans)
  qed
qed

end

lemma Sup_image_mono_le:
  fixes le_b (infix \<open>\<sqsubseteq>\<close> 60) and Sup_b (\<open>\<Or>\<close>)
  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 \<open>\<sqsubseteq>\<close> 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
      then show "x' \ ?rhs"
        by (metis (mono_tags, lifting) \<open>x \<sqsubseteq> y\<close> chain3 imageI ccpo_Sup_upper
            order_trans mono monotoneD)
    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
      then show "x' \ ?rhs"
        by (metis (mono_tags, lifting) \<open>f \<in> Z\<close> chain3 chain4 imageI local.ccpo_Sup_upper
            order.trans)
    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
      then show "x' \ ?lhs"
        by (metis (mono_tags, lifting) \<open>y \<in> Y\<close> ccpo_Sup_below_iff chain1 chain2 imageI
            ccpo_Sup_upper)
    qed
    finally show "x \ ?lhs" .
  qed
  ultimately show "?lhs = ?rhs"
    by (rule order.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])(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"
  have "(\f\?iter. f x) \ (\f\?iter. f y)"
    using chain
  proof(rule ccpo_Sup_least)
    fix x'
    assume "x' \ (\f. f x) ` ?iter"
    then obtain f where f: "f \ ?iter" "x' = f x" by blast
    then have "f x \ f y"
      by (metis \<open>x \<sqsubseteq> y\<close> iterates_mono mono2 monotoneD)
    also have "f y \ \((\f. f y) ` ?iter)"
      using chain f local.ccpo_Sup_upper by auto
    finally show "x' \ \"
      using f(2) by blast
  qed
  then show "?fixp x \ ?fixp y"
    unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply .
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))"
  using assms unfolding monotone_on_def by (metis UNIV_I transpE)

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 =
      if exists_subterm Term.is_Var t then
        NONE
      else
        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_>\<open>ccpo.admissible _ for _ _ _\<close> => mk_thm t
    | t as \<^Const_>\<open>mcont _ _ for _ _ _ _ _\<close> => mk_thm t
    | t as \<^Const_>\<open>monotone_on _ _ for _ _ _ _\<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

experiment begin

text \<open>The following proof by simplification diverges if variables are not handled properly.\<close>

lemma "(\f. monotone R S f \ thesis) \ monotone R S g \ thesis"
  by simp

end

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_on_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_on_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)"
  by (simp add: Inf.INF_identity_eq contI)

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))"
  using assms by (simp add: cont_def chain_fun_ordD fun_lub_apply image_image)

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_on_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)

  show "?fixp x \ ?fixp y" if "x \ y" for x y
  proof -
    have "(\f\?iter. f x)
    \<le> (\<Squnion>f\<in>?iter. f y)"
      using chain
    proof(rule ccpo_Sup_least)
      fix x'
      assume "x' \ (\f. f x) ` ?iter"
      then obtain f where f: "f \ ?iter" "x' = f x" by blast
      then have "f x \ f y"
        by (metis iterates_mcont mcont mcont_monoD that)
      also have "f y \ \((\f. f y) ` ?iter)"
        using chain f local.ccpo_Sup_upper by auto
      finally show "x' \ \"
        using f(2) by blast
    qed
    then show ?thesis
      by (simp add: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
  qed
  show "?fixp (\Y) = \(?fixp ` Y)"
    if chain: "Complete_Partial_Order.chain (\) Y" and Y: "Y \ {}" for Y
  proof -
    have "f (\Y) = \(f ` Y)" if "f \ ?iter" for f
      using that 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 ?thesis
      unfolding ccpo.fixp_def[OF ccpo_fun]
      by (simp add: fun_lub_apply cong: image_cong)
  qed
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 (\<open>\<Or>\<close>) and ord (infix \<open>\<sqsubseteq>\<close> 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 order.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.order.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))"
  using assms by (simp add: ccpo.admissible_def chain_imageI mcont_contD mcont_monoD)

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)"
  by (smt (verit, best) Sup.SUP_cong ccpo.admissible_def contD assms)

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 \<open>\<sqsubseteq>\<close> 60) and lub (\<open>\<Or>\<close>)
  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  using chain
  proof (rule diag_Sup)
    show "\y. y \ Y \ monotone (rel_prod orda ordb) (\) (\x. f (fst x, snd y))"
      by (smt (verit, best) b.order_refl mono monotoneD monotoneI rel_prod_inject rel_prod_sel)
  qed (use mono monotoneD in fastforce)
  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))"
  by (metis (mono_tags, lifting) case_prod_conv monotoneD monotoneI rel_prod.intros
      assms)

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 (simp add: image_mono monoI)

lemma cont_image: "cont Union (\) Union (\) ((`) f)"
  by (meson contI image_Union)

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)"
proof -
  have "\Y. \Complete_Partial_Order.chain ord Y; Y \ {}\
         \<Longrightarrow> \<Squnion> \<Union> (f ` Y) = (\<Squnion>x\<in>Y. \<Squnion> f x)"
--> --------------------

--> maximum size reached

--> --------------------

quality98%

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.