Quelle  Complete_Partial_Order2.thy

(*  Title:      HOL/Library/Complete_Partial_Order2.thy
  Author: Andreas Lochbihler, ETH Zurich
*)

section ‹Formalisation of chain-complete partial orders, continuity and admissibility›

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
  ==> 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
  ==> 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
  ==> 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 ‹⊑› 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 ‹x' = f x› also
    from ‹f ∈ Y› ‹x ⊑ y› have "f x ≤ f y" by(blast dest: mono monotoneD)
    also have "… ≤ ⊔((λf. f y) ` Y)" using chain''
      by(rule ccpo_Sup_upper)(simp add: ‹f ∈ Y›)
    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' ∈ Y" "x' = f x y'" by blast note this(2)
  also from mono1[OF ‹y' ∈ Y›] le have "… ≤ f y y'" by(rule monotoneD)
  also have "… ≤ ?rhs" using chain'[OF y]
    by (auto intro!: ccpo_Sup_upper simp add: ‹y' ∈ Y›)
  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' ∈ Y" "x' = ⊔(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 ‹y ∈ Y› ‹y' ∈ Y› have "y ⊑ y' ∨ y' ⊑ 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 ‹y ∈ Y› ‹y' ∈ Y› have "y'' ∈ 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 ‹⊑› 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 ‹f ∈ Z›] show "⊔(f ` Y) ≤ ⊔(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: ‹y ∈ Y›)
      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) ‹x ⊑ y› 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) ‹f ∈ Z› 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) ‹y ∈ Y› 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 ‹x ⊑ y› 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 ‹Continuity›

definition cont :: "('a set ==> 'a) ==> ('a ==> 'a ==> bool) ==> ('b set ==> 'b) ==> ('b ==> 'b ==> bool) ==> ('a ==> 'b) ==> bool"
where
  "cont luba orda lubb ordb f ⟷
  (∀Y. Complete_Partial_Order.chain orda Y ⟶ Y ≠ {} ⟶ 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 ∧ cont luba orda lubb ordb f"

subsubsection ‹Theorem collection ‹cont_intro›\›

named_theorems cont_intro "continuity and admissibility intro rules"
ML ‹
 (* 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 🍋‹cont_intro›)))
  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 🍋‹ccpo.admissible _ for _ _ _› => mk_thm t
    | t as 🍋‹mcont _ _ for _ _ _ _ _› => mk_thm t
    | t as 🍋‹monotone_on _ _ for _ _ _ _› => mk_thm t
    | _ => NONE
  end
  handle THM _ => NONE 
  | TYPE _ => NONE
›

simproc_setup "cont_intro"
  ( "ccpo.admissible lub ord P"
  | "mcont lub ord lub' ord' f"
  | "monotone ord ord' f"
  ) = ‹K cont_intro_simproc›

lemmas [cont_intro] =
  call_mono
  let_mono
  if_mono
  option.const_mono
  tailrec.const_mono
  bind_mono

experiment begin

text ‹The following proof by simplification diverges if variables are not handled properly.›

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 ]
  ==> monotone (fun_ord orda) (fun_ord ordb) (λ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))
  ==> 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 ≠ {} ]
  ==> 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 ]
  ==> cont luba orda lubb ordb (λ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 ≠ {} ]
  ==> 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) ]
  ==> mcont luba orda lubb ordb (λ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);
     ∧y. mcont lub ord Sup (≤) (λx. f x y);
     mcont lub ord lub' ord' (λy. t y) ]
  ==> mcont lub ord Sup (≤) (λ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)]
  ==> mcont lub ord Sup (≤) (λ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;
    ∀f∈M. mcont lub ord Sup (≤) f ]
  ==> mcont lub (⊑) Sup (≤) (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)
    ≤ (⊔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 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 (‹∨›) 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 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 ‹Admissibility›

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 ]
  ==> ccpo.admissible lub ord (λx. P x ∨ Q x)"
  by(rule ccpo.admissible_disj)

lemma admissible_imp' [cont_intro]:
  "[ class.ccpo lub ord (mk_less ord);
     ccpo.admissible lub ord (λx. ¬ P x);
     ccpo.admissible lub ord (λx. Q x) ]
  ==> ccpo.admissible lub ord (λx. P x ⟶ Q x)"
  unfolding imp_conv_disj by(rule ccpo.admissible_disj)

lemma admissible_imp [cont_intro]:
  "(Q ==> ccpo.admissible lub ord (λx. P x))
  ==> ccpo.admissible lub ord (λx. Q ⟶ 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 (λx. g x) ]
  ==> ccpo.admissible luba orda (λ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) ]
  ==> ccpo.admissible lub ord (λx. P x ⟷ 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 ‹Sign.map_naming (Name_Space.mandatory_path "ccpo")›

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 (λy. x ≠ y) ]
  ==> compact lub ord x"

setup ‹Sign.map_naming Name_Space.parent_path›

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 ‹🍋‹(=)› as order›

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 ]
  ==> mcont the_Sup (=) lub ord f"
  by(simp add: mcont_def cont_eqI monotone_eqI)

subsection ‹ccpo for products›

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) ]
  ==> 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 ⟷
   (∀a. monotone ordb ordc (λb. f (a, b))) ∧
   (∀b. monotone orda ordc (λ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) ⟷
   (∀a. monotone ordb ordc (f a)) ∧ (∀b. monotone orda ordc (λ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)
  ==> monotone orda ordb (case_prod (λ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))
  ==> monotone orda ordb (λ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))
  ==> cont luba orda lubb ordb (λ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)
  ==> cont luba orda lubb ordb (case_prod (λ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 (λ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 ‹Y ≠ {}› 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] ‹Y ≠ {}›)
  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] ‹Y ≠ {}›)
  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 ]
  ==> cont (prod_lub luba lubb) (rel_prod orda ordb) Sup (≤) (case_prod f) ⟷
   (∀x. cont lubb ordb Sup (≤) (λy. f x y)) ∧ (∀y. cont luba orda Sup (≤) (λ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);
    ∧x. cont lubb ordb lub leq (λy. f x y);
    ∧y. cont luba orda lub leq (λx. f x y);
    class.preorder orda (mk_less orda);
    class.preorder ordb (mk_less ordb) ]
  ==> 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 ]
  ==> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) ⟷
   (∀x. cont lubb ordb lub leq (λy. f x y)) ∧ (∀y. cont luba orda lub leq (λ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 ]
  ==> mcont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) ⟷
   (∀x. mcont lubb ordb lub leq (λy. f x y)) ∧ (∀y. mcont luba orda lub leq (λ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 ‹Complete lattices as ccpo›

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 ‹z ∈ Y› have "z ≤ ⊔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' ∈ 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 (≤) (λx. g x) ]
  ==> mcont lub ord Sup (≤) (λx. f x ⊔ 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 (≤) (λx. g x) ]
  ==> mcont lub ord Sup (≤) (λx. f x ⊓ 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 ‹Partial_Function.init "lfp" 🍋‹lfp.fixp_fun› \<^term>‹lfp.mono_body›
  @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE›

interpretation gfp: partial_function_definitions "(≥) :: _ :: complete_lattice ==> _" Inf
  by(rule complete_lattice_partial_function_definitions_dual)

declaration ‹Partial_Function.init "gfp" 🍋‹gfp.fixp_fun› \<^term>‹gfp.mono_body›
  @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE›

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 ≠ {}]
         ==> ⊔ ∪ (f ` Y) = (⊔x∈Y. ⊔ f x)"
    by (blast intro: Sup_least Sup_upper order_trans order.antisym)
  with assms show ?thesis
    by (force simp: cont_def)
qed

lemma mcont_Sup: "mcont lub ord Union (⊆) f ==> mcont lub ord Sup (≤) (λx. ⊔f x)"
  unfolding mcont_def by(blast intro: monotone_Sup cont_Sup)

lemma monotone_SUP:
  "[ monotone ord (⊆) f; ∧y. monotone ord (≤) (λx. g x y) ] ==> monotone ord (≤) (λx. ⊔y∈f x. g x y)"
  by(rule monotoneI)(blast dest: monotoneD intro: Sup_upper order_trans intro!: Sup_least)

lemma monotone_SUP2:
  "(∧y. y ∈ A ==> monotone ord (≤) (λx. g x y)) ==> monotone ord (≤) (λx. ⊔y∈A. g x y)"
  by(rule monotoneI)(blast intro: Sup_upper order_trans dest: monotoneD intro!: Sup_least)

lemma cont_SUP:
  assumes f: "mcont lub ord Union (⊆) f"
  and g: "∧y. mcont lub ord Sup (≤) (λx. g x y)"
  shows "cont lub ord Sup (≤) (λx. ⊔y∈f x. g x y)"
proof(rule contI)
  fix Y
  assume chain: "Complete_Partial_Order.chain ord Y"
    and Y: "Y ≠ {}"
  show "⊔(g (lub Y) ` f (lub Y)) = ⊔((λx. ⊔(g x ` f x)) ` Y)" (is "?lhs = ?rhs")
  proof(rule order.antisym)
    show "?lhs ≤ ?rhs"
    proof(rule Sup_least)
      fix x
      assume "x ∈ g (lub Y) ` f (lub Y)"
      with mcont_contD[OF f chain Y] mcont_contD[OF g chain Y]
      obtain y z where "y ∈ Y" "z ∈ f y"
        and x: "x = ⊔((λx. g x z) ` Y)" by auto
      show "x ≤ ?rhs" unfolding x
      proof(rule Sup_least)
        fix u
        assume "u ∈ (λx. g x z) ` Y"
        then obtain y' where "u = g y' z" "y' ∈ Y" by auto
        from chain ‹y ∈ Y› ‹y' ∈ Y› have "ord y y' ∨ ord y' y" by(rule chainD)
        thus "u ≤ ?rhs"
        proof
          note ‹u = g y' z› also
          assume "ord y y'"
          with f have "f y ⊆ f y'" by(rule mcont_monoD)
          with ‹z ∈ f y›
          have "g y' z ≤ ⊔(g y' ` f y')" by(auto intro: Sup_upper)
          also have "… ≤ ?rhs" using ‹y' ∈ Y› by(auto intro: Sup_upper)
          finally show ?thesis .
        next
          note ‹u = g y' z› also
          assume "ord y' y"
          with g have "g y' z ≤ g y z" by(rule mcont_monoD)
          also have "… ≤ ⊔(g y ` f y)" using ‹z ∈ f y›
            by(auto intro: Sup_upper)
          also have "… ≤ ?rhs" using ‹y ∈ Y› by(auto intro: Sup_upper)
          finally show ?thesis .
        qed
      qed
    qed
  next
    show "?rhs ≤ ?lhs"
    proof(rule Sup_least)
      fix x
      assume "x ∈ (λx. ⊔(g x ` f x)) ` Y"
      then obtain y where x: "x = ⊔(g y ` f y)" and "y ∈ Y" by auto
      show "x ≤ ?lhs" unfolding x
      proof(rule Sup_least)
        fix u
        assume "u ∈ g y ` f y"
        then obtain z where "u = g y z" "z ∈ f y" by auto
        note ‹u = g y z›
        also have "g y z ≤ ⊔((λx. g x z) ` Y)"
          using ‹y ∈ Y› by(auto intro: Sup_upper)
        also have "… = g (lub Y) z" by(simp add: mcont_contD[OF g chain Y])
        also have "… ≤ ?lhs" using ‹z ∈ f y› ‹y ∈ Y›
          by(auto intro: Sup_upper simp add: mcont_contD[OF f chain Y])
        finally show "u ≤ ?lhs" .
      qed
    qed
  qed
qed

lemma mcont_SUP [cont_intro, simp]:
  "[ mcont lub ord Union (⊆) f; ∧y. mcont lub ord Sup (≤) (λx. g x y) ]
  ==> mcont lub ord Sup (≤) (λx. ⊔y∈f x. g x y)"
by(blast intro: mcontI cont_SUP monotone_SUP mcont_mono)

end

lemma admissible_Ball [cont_intro, simp]:
  "[ ∧x. ccpo.admissible lub ord (λA. P A x);
     mcont lub ord Union (⊆) f;
     class.ccpo lub ord (mk_less ord) ]
  ==> ccpo.admissible lub ord (λA. ∀x∈f A. P A x)"
unfolding Ball_def by simp

lemma admissible_Bex'[THEN admissible_subst, cont_intro, simp]:
  shows admissible_Bex: "ccpo.admissible Union (⊆) (λA. ∃x∈A. P x)"
  using ccpo.admissible_def by fastforce

subsection ‹Parallel fixpoint induction›

context
  fixes luba :: "'a set ==> 'a"
  and orda :: "'a ==> 'a ==> bool"
  and lubb :: "'b set ==> 'b"
  and ordb :: "'b ==> 'b ==> bool"
  assumes a: "class.ccpo luba orda (mk_less orda)"
  and b: "class.ccpo lubb ordb (mk_less ordb)"
begin

interpretation a: ccpo luba orda "mk_less orda" by(rule a)
interpretation b: ccpo lubb ordb "mk_less ordb" by(rule b)

lemma ccpo_rel_prodI:
  "class.ccpo (prod_lub luba lubb) (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
  (is "class.ccpo ?lub ?ord ?ord'")
proof(intro class.ccpo.intro class.ccpo_axioms.intro)
  show "class.order ?ord ?ord'" 
    by(rule order_rel_prodI) intro_locales
  show "∧A x. [Complete_Partial_Order.chain (rel_prod orda ordb) A; x ∈ A]
           ==> rel_prod orda ordb x (prod_lub luba lubb A)"
    by (simp add: a.ccpo_Sup_upper b.ccpo_Sup_upper chain_rel_prodD1 chain_rel_prodD2
        prod_lub_def rel_prod_sel)
  show "∧A z. [Complete_Partial_Order.chain (rel_prod orda ordb) A;
            ∧x. x ∈ A ==> rel_prod orda ordb x z]
           ==> rel_prod orda ordb (prod_lub luba lubb A) z"
    by (metis (full_types) a.ccpo_Sup_below_iff b.ccpo_Sup_least chain_rel_prodD1
        chain_rel_prodD2 imageE prod.sel prod_lub_def rel_prod_sel)
qed

interpretation ab: ccpo "prod_lub luba lubb" "rel_prod orda ordb" "mk_less (rel_prod orda ordb)"
by(rule ccpo_rel_prodI)

lemma monotone_map_prod [simp]:
  "monotone (rel_prod orda ordb) (rel_prod ordc ordd) (map_prod f g) ⟷
   monotone orda ordc f ∧ monotone ordb ordd g"
by(auto simp add: monotone_def)

lemma parallel_fixp_induct:
  assumes adm: "ccpo.admissible (prod_lub luba lubb) (rel_prod orda ordb) (λx. P (fst x) (snd x))"
  and f: "monotone orda orda f"
  and g: "monotone ordb ordb g"
  and bot: "P (luba {}) (lubb {})"
  and step: "∧x y. P x y ==> P (f x) (g y)"
  shows "P (ccpo.fixp luba orda f) (ccpo.fixp lubb ordb g)"
proof -
  let ?lub = "prod_lub luba lubb"
    and ?ord = "rel_prod orda ordb"
    and ?P = "λ(x, y). P x y"
  from adm have adm': "ccpo.admissible ?lub ?ord ?P" by(simp add: split_def)
  hence "?P (ccpo.fixp (prod_lub luba lubb) (rel_prod orda ordb) (map_prod f g))"
    by(rule ab.fixp_induct)(auto simp add: f g step bot)
  also have "ccpo.fixp (prod_lub luba lubb) (rel_prod orda ordb) (map_prod f g) =
            (ccpo.fixp luba orda f, ccpo.fixp lubb ordb g)" (is "?lhs = (?rhs1, ?rhs2)")
  proof(rule ab.order.antisym)
    have "ccpo.admissible ?lub ?ord (λxy. ?ord xy (?rhs1, ?rhs2))"
      by(rule admissible_leI[OF ccpo_rel_prodI])(auto simp add: prod_lub_def chain_empty intro: a.ccpo_Sup_least b.ccpo_Sup_least)
    thus "?ord ?lhs (?rhs1, ?rhs2)"
      by(rule ab.fixp_induct)(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] simp add: b.fixp_unfold[OF g, symmetric] a.fixp_unfold[OF f, symmetric] f g intro: a.ccpo_Sup_least b.ccpo_Sup_least chain_empty)
  next
    have "ccpo.admissible luba orda (λx. orda x (fst ?lhs))"
      by(rule admissible_leI[OF a])(auto intro: a.ccpo_Sup_least simp add: chain_empty)
    hence "orda ?rhs1 (fst ?lhs)" using f
    proof(rule a.fixp_induct)
      fix x
      assume "orda x (fst ?lhs)"
      thus "orda (f x) (fst ?lhs)"
        by(subst ab.fixp_unfold)(auto simp add: f g dest: monotoneD[OF f])
    qed(auto intro: a.ccpo_Sup_least chain_empty)
    moreover
    have "ccpo.admissible lubb ordb (λy. ordb y (snd ?lhs))"
      by(rule admissible_leI[OF b])(auto intro: b.ccpo_Sup_least simp add: chain_empty)
    hence "ordb ?rhs2 (snd ?lhs)" using g
    proof(rule b.fixp_induct)
      fix y
      assume "ordb y (snd ?lhs)"
      thus "ordb (g y) (snd ?lhs)"
        by (smt (verit, best) ab.fixp_unfold f g monotoneD monotone_map_prod
            snd_map_prod)
    qed(auto intro: b.ccpo_Sup_least chain_empty)
    ultimately show "?ord (?rhs1, ?rhs2) ?lhs"
      by(simp add: rel_prod_conv split_beta)
  qed
  finally show ?thesis by simp
qed

end

lemma parallel_fixp_induct_uc:
  assumes a: "partial_function_definitions orda luba"
  and b: "partial_function_definitions ordb lubb"
  and F: "∧x. monotone (fun_ord orda) orda (λf. U1 (F (C1 f)) x)"
  and G: "∧y. monotone (fun_ord ordb) ordb (λg. U2 (G (C2 g)) y)"
  and eq1: "f ≡ C1 (ccpo.fixp (fun_lub luba) (fun_ord orda) (λf. U1 (F (C1 f))))"
  and eq2: "g ≡ C2 (ccpo.fixp (fun_lub lubb) (fun_ord ordb) (λg. U2 (G (C2 g))))"
  and inverse: "∧f. U1 (C1 f) = f"
  and inverse2: "∧g. U2 (C2 g) = g"
  and adm: "ccpo.admissible (prod_lub (fun_lub luba) (fun_lub lubb)) (rel_prod (fun_ord orda) (fun_ord ordb)) (λx. P (fst x) (snd x))"
  and bot: "P (λ_. luba {}) (λ_. lubb {})"
  and step: "∧f g. P (U1 f) (U2 g) ==> P (U1 (F f)) (U2 (G g))"
shows "P (U1 f) (U2 g)"
  unfolding eq1 eq2 inverse inverse2
proof (rule parallel_fixp_induct[OF partial_function_definitions.ccpo[OF a] partial_function_definitions.ccpo[OF b] adm])
  show "monotone (fun_ord orda) (fun_ord orda) (λf. U1 (F (C1 f)))"
    "monotone (fun_ord ordb) (fun_ord ordb) (λg. U2 (G (C2 g)))"
    using F G by(simp_all add: monotone_def fun_ord_def)
  show "P (fun_lub luba {}) (fun_lub lubb {})"
    by (simp add: fun_lub_def bot)
  show "∧x y. P x y ==> P (U1 (F (C1 x))) (U2 (G (C2 y)))"
    by (simp add: inverse inverse2 local.step)
qed

lemmas parallel_fixp_induct_1_1 = parallel_fixp_induct_uc[
  of _ _ _ _ "λx. x" _ "λx. x" "λx. x" _ "λx. x",
  OF _ _ _ _ _ _ refl refl]

lemmas parallel_fixp_induct_2_2 = parallel_fixp_induct_uc[
  of _ _ _ _ "case_prod" _ "curry" "case_prod" _ "curry",
  where P="λf g. P (curry f) (curry g)",
  unfolded case_prod_curry curry_case_prod curry_K,
  OF _ _ _ _ _ _ refl refl]
  for P

lemma monotone_fst: "monotone (rel_prod orda ordb) orda fst"
  by(auto intro: monotoneI)

lemma mcont_fst: "mcont (prod_lub luba lubb) (rel_prod orda ordb) luba orda fst"
  by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)

lemma mcont2mcont_fst [cont_intro, simp]:
  "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
  ==> mcont lub ord luba orda (λx. fst (t x))"
  by (simp add: mcont_def monotone_on_def prod_lub_def cont_def image_image rel_prod_sel)

lemma monotone_snd: "monotone (rel_prod orda ordb) ordb snd"
  by(auto intro: monotoneI)

lemma mcont_snd: "mcont (prod_lub luba lubb) (rel_prod orda ordb) lubb ordb snd"
  by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)

lemma mcont2mcont_snd [cont_intro, simp]:
  "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
  ==> mcont lub ord lubb ordb (λx. snd (t x))"
by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)

lemma monotone_Pair:
  "[ monotone ord orda f; monotone ord ordb g ]
  ==> monotone ord (rel_prod orda ordb) (λx. (f x, g x))"
  by(simp add: monotone_def)

lemma cont_Pair:
  "[ cont lub ord luba orda f; cont lub ord lubb ordb g ]
  ==> cont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (λx. (f x, g x))"
  by(rule contI)(auto simp add: prod_lub_def image_image dest!: contD)

lemma mcont_Pair:
  "[ mcont lub ord luba orda f; mcont lub ord lubb ordb g ]
  ==> mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (λx. (f x, g x))"
  by(rule mcontI)(simp_all add: monotone_Pair mcont_mono cont_Pair)

context partial_function_definitions 
begin
text ‹Specialised versions of @{thm [source] mcont_call} for admissibility proofs for parallel fixpoint inductions›
lemmas mcont_call_fst [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_fst]
lemmas mcont_call_snd [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_snd]
end

lemma map_option_mono [partial_function_mono]:
  "mono_option B ==> mono_option (λf. map_option g (B f))"
unfolding map_conv_bind_option by(rule bind_mono) simp_all

lemma compact_flat_lub [cont_intro]: "ccpo.compact (flat_lub x) (flat_ord x) y"
using flat_interpretation[THEN ccpo]
proof(rule ccpo.compactI[OF _ ccpo.admissibleI])
  fix A
  assume chain: "Complete_Partial_Order.chain (flat_ord x) A"
    and A: "A ≠ {}"
    and *: "∀z∈A. ¬ flat_ord x y z"
  from A obtain z where "z ∈ A" by blast
  with * have z: "¬ flat_ord x y z" ..
  hence y: "x ≠ y" "y ≠ z" by(auto simp add: flat_ord_def)
  have "y ≠ (THE z. z ∈ A - {x})" if "¬ A ⊆ {x}"
  proof -
    from that obtain z' where "z' ∈ A" "z' ≠ x" by auto
    then have "(THE z. z ∈ A - {x}) = z'"
      by(intro the_equality)(auto dest: chainD[OF chain] simp add: flat_ord_def)
    moreover have "z' ≠ y" using ‹z' ∈ A› * by(auto simp add: flat_ord_def)
    ultimately show ?thesis by simp
  qed
  with z show "¬ flat_ord x y (flat_lub x A)" 
    by(simp add: flat_ord_def flat_lub_def)
qed

end