(*  Title:      src/HOL/Library/Complete_Partial_Order2

    Author:     Andreas Lochbihler, ETH Zurich

*)

section {* Formalisation of chain-complete partial orders, continuity and admissibility *}

theory Complete_Partial_Order2 imports 

  Main

  "~~/src/HOL/Library/Lattice_Syntax"

begin

context begin interpretation lifting_syntax .

lemma chain_transfer [transfer_rule]:

  "((A ===> A ===> op =) ===> rel_set A ===> op =) Complete_Partial_Order.chain Complete_Partial_Order.chain"

unfolding chain_def[abs_def] by transfer_prover

end

lemma linorder_chain [simp, intro!]:

  fixes Y :: "_ :: linorder set"

  shows "Complete_Partial_Order.chain op \<le> Y"

by(auto intro: chainI)

lemma fun_lub_apply: "\<And>Sup. fun_lub Sup Y x = Sup ((\<lambda>f. f x) ` Y)"

by(simp add: fun_lub_def image_def)

lemma fun_lub_empty [simp]: "fun_lub lub {} = (\<lambda>_. 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 ((\<lambda>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 op \<le>) (mk_less (fun_ord op \<le>))"

  by standard (auto 4 3 simp add: mk_less_def fun_ord_def fun_lub_apply

    intro: order.trans antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)

lemma ccpo_Sup_below_iff: "Complete_Partial_Order.chain op \<le> Y \<Longrightarrow> Sup Y \<le> x \<longleftrightarrow> (\<forall>y\<in>Y. y \<le> x)"

by(fast intro: order_trans[OF ccpo_Sup_upper] ccpo_Sup_least)

lemma Sup_minus_bot: 

  assumes chain: "Complete_Partial_Order.chain op \<le> A"

  shows "\<Squnion>(A - {\<Squnion>{}}) = \<Squnion>A"

apply(rule antisym)

 apply(blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])

apply(rule ccpo_Sup_least[OF chain])

apply(case_tac "x = \<Squnion>{}")

by(blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+

lemma mono_lub:

  fixes le_b (infix "\<sqsubseteq>" 60)

  assumes chain: "Complete_Partial_Order.chain (fun_ord op \<le>) Y"

  and mono: "\<And>f. f \<in> Y \<Longrightarrow> monotone le_b op \<le> f"

  shows "monotone op \<sqsubseteq> op \<le> (fun_lub Sup Y)"

proof(rule monotoneI)

  fix x y

  assume "x \<sqsubseteq> y"

  have chain'': "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` Y)"

    using chain by(rule chain_imageI)(simp add: fun_ord_def)

  then show "fun_lub Sup Y x \<le> fun_lub Sup Y y" unfolding fun_lub_apply

  proof(rule ccpo_Sup_least)

    fix x'

    assume "x' \<in> (\<lambda>f. f x) ` Y"

    then obtain f where "f \<in> Y" "x' = f x" by blast

    note `x' = f x` also

    from `f \<in> Y` `x \<sqsubseteq> y` have "f x \<le> f y" by(blast dest: mono monotoneD)

    also have "\<dots> \<le> \<Squnion>((\<lambda>f. f y) ` Y)" using chain''

      by(rule ccpo_Sup_upper)(simp add: `f \<in> Y`)

    finally show "x' \<le> \<Squnion>((\<lambda>f. f y) ` Y)" .

  qed

qed

context

  fixes le_b (infix "\<sqsubseteq>" 60) and Y f

  assumes chain: "Complete_Partial_Order.chain le_b Y" 

  and mono1: "\<And>y. y \<in> Y \<Longrightarrow> monotone le_b op \<le> (\<lambda>x. f x y)"

  and mono2: "\<And>x a b. \<lbrakk> x \<in> Y; a \<sqsubseteq> b; a \<in> Y; b \<in> Y \<rbrakk> \<Longrightarrow> f x a \<le> f x b"

begin

lemma Sup_mono: 

  assumes le: "x \<sqsubseteq> y" and x: "x \<in> Y" and y: "y \<in> Y"

  shows "\<Squnion>(f x ` Y) \<le> \<Squnion>(f y ` Y)" (is "_ \<le> ?rhs")

proof(rule ccpo_Sup_least)

  from chain show chain': "Complete_Partial_Order.chain op \<le> (f x ` Y)" when "x \<in> Y" for x

    by(rule chain_imageI) (insert that, auto dest: mono2)

  fix x'

  assume "x' \<in> f x ` Y"

  then obtain y' where "y' \<in> Y" "x' = f x y'" by blast note this(2)

  also from mono1[OF `y' \<in> Y`] le have "\<dots> \<le> f y y'" by(rule monotoneD)

  also have "\<dots> \<le> ?rhs" using chain'[OF y]

    by (auto intro!: ccpo_Sup_upper simp add: `y' \<in> Y`)

  finally show "x' \<le> ?rhs" .

qed(rule x)

lemma diag_Sup: "\<Squnion>((\<lambda>x. \<Squnion>(f x ` Y)) ` Y) = \<Squnion>((\<lambda>x. f x x) ` Y)" (is "?lhs = ?rhs")

proof(rule antisym)

  have chain1: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>(f x ` Y)) ` Y)"

    using chain by(rule chain_imageI)(rule Sup_mono)

  have chain2: "\<And>y'. y' \<in> Y \<Longrightarrow> Complete_Partial_Order.chain op \<le> (f y' ` Y)" using chain

    by(rule chain_imageI)(auto dest: mono2)

  have chain3: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. f x x) ` Y)"

    using chain by(rule chain_imageI)(auto intro: monotoneD[OF mono1] mono2 order.trans)

  show "?lhs \<le> ?rhs" using chain1

  proof(rule ccpo_Sup_least)

    fix x'

    assume "x' \<in> (\<lambda>x. \<Squnion>(f x ` Y)) ` Y"

    then obtain y' where "y' \<in> Y" "x' = \<Squnion>(f y' ` Y)" by blast note this(2)

    also have "\<dots> \<le> ?rhs" using chain2[OF `y' \<in> Y`]

    proof(rule ccpo_Sup_least)

      fix x

      assume "x \<in> f y' ` Y"

      then obtain y where "y \<in> Y" and x: "x = f y' y" by blast

      def y'' \<equiv> "if y \<sqsubseteq> y' then y' else y"

      from chain `y \<in> Y` `y' \<in> Y` have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)

      hence "f y' y \<le> f y'' y''" using `y \<in> Y` `y' \<in> Y`

        by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1])

      also from `y \<in> Y` `y' \<in> Y` have "y'' \<in> Y" by(simp add: y''_def)

      from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: `y'' \<in> Y`)

      finally show "x \<le> ?rhs" by(simp add: x)

    qed

    finally show "x' \<le> ?rhs" .

  qed

  show "?rhs \<le> ?lhs" using chain3

  proof(rule ccpo_Sup_least)

    fix y

    assume "y \<in> (\<lambda>x. f x x) ` Y"

    then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2)

    also from chain2[OF `x \<in> Y`] have "\<dots> \<le> \<Squnion>(f x ` Y)"

      by(rule ccpo_Sup_upper)(simp add: `x \<in> Y`)

    also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: `x \<in> Y`)

    finally show "y \<le> ?lhs" .

  qed

qed

end

lemma Sup_image_mono_le:

  fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>_" [900] 900)

  assumes ccpo: "class.ccpo Sup_b op \<sqsubseteq> lt_b"

  assumes chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"

  and mono: "\<And>x y. \<lbrakk> x \<sqsubseteq> y; x \<in> Y \<rbrakk> \<Longrightarrow> f x \<le> f y"

  shows "Sup (f ` Y) \<le> f (\<Or>Y)"

proof(rule ccpo_Sup_least)

  show "Complete_Partial_Order.chain op \<le> (f ` Y)"

    using chain by(rule chain_imageI)(rule mono)

  fix x

  assume "x \<in> f ` Y"

  then obtain y where "y \<in> Y" and "x = f y" by blast note this(2)

  also have "y \<sqsubseteq> \<Or>Y" using ccpo chain `y \<in> Y` by(rule ccpo.ccpo_Sup_upper)

  hence "f y \<le> f (\<Or>Y)" using `y \<in> Y` by(rule mono)

  finally show "x \<le> \<dots>" .

qed

lemma swap_Sup:

  fixes le_b (infix "\<sqsubseteq>" 60)

  assumes Y: "Complete_Partial_Order.chain op \<sqsubseteq> Y"

  and Z: "Complete_Partial_Order.chain (fun_ord op \<le>) Z"

  and mono: "\<And>f. f \<in> Z \<Longrightarrow> monotone op \<sqsubseteq> op \<le> f"

  shows "\<Squnion>((\<lambda>x. \<Squnion>(x ` Y)) ` Z) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y)"

  (is "?lhs = ?rhs")

proof(cases "Y = {}")

  case True

  then show ?thesis

    by (simp add: image_constant_conv cong del: strong_SUP_cong)

next

  case False

  have chain1: "\<And>f. f \<in> Z \<Longrightarrow> Complete_Partial_Order.chain op \<le> (f ` Y)"

    by(rule chain_imageI[OF Y])(rule monotoneD[OF mono])

  have chain2: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>(x ` Y)) ` Z)" using Z

  proof(rule chain_imageI)

    fix f g

    assume "f \<in> Z" "g \<in> Z"

      and "fun_ord op \<le> f g"

    from chain1[OF `f \<in> Z`] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"

    proof(rule ccpo_Sup_least)

      fix x

      assume "x \<in> f ` Y"

      then obtain y where "y \<in> Y" "x = f y" by blast note this(2)

      also have "\<dots> \<le> g y" using `fun_ord op \<le> f g` by(simp add: fun_ord_def)

      also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF `g \<in> Z`]

        by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)

      finally show "x \<le> \<Squnion>(g ` Y)" .

    qed

  qed

  have chain3: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` Z)"

    using Z by(rule chain_imageI)(simp add: fun_ord_def)

  have chain4: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y)"

    using Y

  proof(rule chain_imageI)

    fix f x y

    assume "x \<sqsubseteq> y"

    show "\<Squnion>((\<lambda>f. f x) ` Z) \<le> \<Squnion>((\<lambda>f. f y) ` Z)" (is "_ \<le> ?rhs") using chain3

    proof(rule ccpo_Sup_least)

      fix x'

      assume "x' \<in> (\<lambda>f. f x) ` Z"

      then obtain f where "f \<in> Z" "x' = f x" by blast note this(2)

      also have "f x \<le> f y" using `f \<in> Z` `x \<sqsubseteq> y` by(rule monotoneD[OF mono])

      also have "f y \<le> ?rhs" using chain3

        by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)

      finally show "x' \<le> ?rhs" .

    qed

  qed

  from chain2 have "?lhs \<le> ?rhs"

  proof(rule ccpo_Sup_least)

    fix x

    assume "x \<in> (\<lambda>x. \<Squnion>(x ` Y)) ` Z"

    then obtain f where "f \<in> Z" "x = \<Squnion>(f ` Y)" by blast note this(2)

    also have "\<dots> \<le> ?rhs" using chain1[OF `f \<in> Z`]

    proof(rule ccpo_Sup_least)

      fix x'

      assume "x' \<in> f ` Y"

      then obtain y where "y \<in> Y" "x' = f y" by blast note this(2)

      also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3

        by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)

      also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)

      finally show "x' \<le> ?rhs" .

    qed

    finally show "x \<le> ?rhs" .

  qed

  moreover

  have "?rhs \<le> ?lhs" using chain4

  proof(rule ccpo_Sup_least)

    fix x

    assume "x \<in> (\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y"

    then obtain y where "y \<in> Y" "x = \<Squnion>((\<lambda>f. f y) ` Z)" by blast note this(2)

    also have "\<dots> \<le> ?lhs" using chain3

    proof(rule ccpo_Sup_least)

      fix x'

      assume "x' \<in> (\<lambda>f. f y) ` Z"

      then obtain f where "f \<in> Z" "x' = f y" by blast note this(2)

      also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF `f \<in> Z`]

        by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)

      also have "\<dots> \<le> ?lhs" using chain2

        by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)

      finally show "x' \<le> ?lhs" .

    qed

    finally show "x \<le> ?lhs" .

  qed

  ultimately show "?lhs = ?rhs" by(rule antisym)

qed

lemma fixp_mono:

  assumes fg: "fun_ord op \<le> f g"

  and f: "monotone op \<le> op \<le> f"

  and g: "monotone op \<le> op \<le> g"

  shows "ccpo_class.fixp f \<le> ccpo_class.fixp g"

unfolding fixp_def

proof(rule ccpo_Sup_least)

  fix x

  assume "x \<in> ccpo_class.iterates f"

  thus "x \<le> \<Squnion>ccpo_class.iterates g"

  proof induction

    case (step x)

    from f step.IH have "f x \<le> f (\<Squnion>ccpo_class.iterates g)" by(rule monotoneD)

    also have "\<dots> \<le> g (\<Squnion>ccpo_class.iterates g)" using fg by(simp add: fun_ord_def)

    also have "\<dots> = \<Squnion>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 \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) begin

lemma iterates_mono:

  assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"

  and mono: "\<And>f. monotone op \<sqsubseteq> op \<le> f \<Longrightarrow> monotone op \<sqsubseteq> op \<le> (F f)"

  shows "monotone op \<sqsubseteq> op \<le> f"

using f

by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mono_lub)+

lemma fixp_preserves_mono:

  assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. F f x)"

  and mono2: "\<And>f. monotone op \<sqsubseteq> op \<le> f \<Longrightarrow> monotone op \<sqsubseteq> op \<le> (F f)"

  shows "monotone op \<sqsubseteq> op \<le> (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) F)"

  (is "monotone _ _ ?fixp")

proof(rule monotoneI)

  have mono: "monotone (fun_ord op \<le>) (fun_ord op \<le>) F"

    by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])

  let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"

  have chain: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>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 \<sqsubseteq> y"

  show "?fixp x \<le> ?fixp y"

    unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain

  proof(rule ccpo_Sup_least)

    fix x'

    assume "x' \<in> (\<lambda>f. f x) ` ?iter"

    then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)

    also have "f x \<le> f y"

      by(rule monotoneD[OF iterates_mono[OF `f \<in> ?iter` mono2]])(blast intro: `x \<sqsubseteq> y`)+

    also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain

      by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)

    finally show "x' \<le> \<dots>" .

  qed

qed

end

end

lemma monotone2monotone:

  assumes 2: "\<And>x. monotone ordb ordc (\<lambda>y. f x y)"

  and t: "monotone orda ordb (\<lambda>x. t x)"

  and 1: "\<And>y. monotone orda ordc (\<lambda>x. f x y)"

  and trans: "transp ordc"

  shows "monotone orda ordc (\<lambda>x. f x (t x))"

by(blast intro: monotoneI transpD[OF trans] monotoneD[OF t] monotoneD[OF 2] monotoneD[OF 1])

subsection {* Continuity *}

definition cont :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"

where

  "cont luba orda lubb ordb f \<longleftrightarrow> 

  (\<forall>Y. Complete_Partial_Order.chain orda Y \<longrightarrow> Y \<noteq> {} \<longrightarrow> f (luba Y) = lubb (f ` Y))"

definition mcont :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"

where

  "mcont luba orda lubb ordb f \<longleftrightarrow>

   monotone orda ordb f \<and> cont luba orda lubb ordb f"

subsubsection {* Theorem collection @{text 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 @{named_theorems 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 =

      case SINGLE (cont_intro_tac ctxt 1) (mk_stmt t) of

        SOME thm => SOME (Goal.finish ctxt thm RS @{thm Eq_TrueI})

      | NONE => NONE

  in

    case Thm.term_of ct of

      t as Const (@{const_name ccpo.admissible}, _) $ _ $ _ $ _ => mk_thm t

    | t as Const (@{const_name mcont}, _) $ _ $ _ $ _ $ _ $ _ => mk_thm t

    | t as Const (@{const_name monotone}, _) $ _ $ _ $ _ => 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

declare if_mono[simp]

lemma monotone_id' [cont_intro]: "monotone ord ord (\<lambda>x. x)"

by(simp add: monotone_def)

lemma monotone_applyI:

  "monotone orda ordb F \<Longrightarrow> monotone (fun_ord orda) ordb (\<lambda>f. F (f x))"

by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)

lemma monotone_if_fun [partial_function_mono]:

  "\<lbrakk> monotone (fun_ord orda) (fun_ord ordb) F; monotone (fun_ord orda) (fun_ord ordb) G \<rbrakk>

  \<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) (\<lambda>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 \<longleftrightarrow> (\<forall>x. monotone orda ordb (\<lambda>y. f y x))"

by(auto simp add: monotone_def fun_ord_def)

context preorder begin

lemma transp_le [simp, cont_intro]: "transp op \<le>"

by(rule transpI)(rule order_trans)

lemma monotone_const [simp, cont_intro]: "monotone ord op \<le> (\<lambda>_. c)"

by(rule monotoneI) simp

end

lemma transp_le [cont_intro, simp]:

  "class.preorder ord (mk_less ord) \<Longrightarrow> transp ord"

by(rule preorder.transp_le)

context partial_function_definitions begin

declare const_mono [cont_intro, simp]

lemma transp_le [cont_intro, simp]: "transp leq"

by(rule transpI)(rule leq_trans)

lemma preorder [cont_intro, simp]: "class.preorder leq (mk_less leq)"

by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans)

declare ccpo[cont_intro, simp]

end

lemma contI [intro?]:

  "(\<And>Y. \<lbrakk> Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> \<Longrightarrow> f (luba Y) = lubb (f ` Y)) 

  \<Longrightarrow> cont luba orda lubb ordb f"

unfolding cont_def by blast

lemma contD:

  "\<lbrakk> cont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> 

  \<Longrightarrow> f (luba Y) = lubb (f ` Y)"

unfolding cont_def by blast

lemma cont_id [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord id"

by(rule contI) simp

lemma cont_id' [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord (\<lambda>x. x)"

using cont_id[unfolded id_def] .

lemma cont_applyI [cont_intro]:

  assumes cont: "cont luba orda lubb ordb g"

  shows "cont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. g (f x))"

by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont])

lemma call_cont: "cont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"

by(simp add: cont_def fun_lub_apply)

lemma cont_if [cont_intro]:

  "\<lbrakk> cont luba orda lubb ordb f; cont luba orda lubb ordb g \<rbrakk>

  \<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"

by(cases c) simp_all

lemma mcontI [intro?]:

   "\<lbrakk> monotone orda ordb f; cont luba orda lubb ordb f \<rbrakk> \<Longrightarrow> mcont luba orda lubb ordb f"

by(simp add: mcont_def)

lemma mcont_mono: "mcont luba orda lubb ordb f \<Longrightarrow> monotone orda ordb f"

by(simp add: mcont_def)

lemma mcont_cont [simp]: "mcont luba orda lubb ordb f \<Longrightarrow> cont luba orda lubb ordb f"

by(simp add: mcont_def)

lemma mcont_monoD:

  "\<lbrakk> mcont luba orda lubb ordb f; orda x y \<rbrakk> \<Longrightarrow> ordb (f x) (f y)"

by(auto simp add: mcont_def dest: monotoneD)

lemma mcont_contD:

  "\<lbrakk> mcont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk>

  \<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 (\<lambda>f. f t)"

by(simp add: mcont_def call_mono call_cont)

lemma mcont_id' [cont_intro, simp]: "mcont lub ord lub ord (\<lambda>x. x)"

by(simp add: mcont_def monotone_id')

lemma mcont_applyI:

  "mcont luba orda lubb ordb (\<lambda>x. F x) \<Longrightarrow> mcont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. F (f x))"

by(simp add: mcont_def monotone_applyI cont_applyI)

lemma mcont_if [cont_intro, simp]:

  "\<lbrakk> mcont luba orda lubb ordb (\<lambda>x. f x); mcont luba orda lubb ordb (\<lambda>x. g x) \<rbrakk>

  \<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 \<longleftrightarrow> (\<forall>x. cont luba orda lubb ordb (\<lambda>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 \<longleftrightarrow> (\<forall>x. mcont luba orda lubb ordb (\<lambda>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 op \<le> (\<lambda>x. c)"

by (rule contI) (simp add: image_constant_conv cong del: strong_SUP_cong)

lemma mcont_const [cont_intro, simp]:

  "mcont luba orda Sup op \<le> (\<lambda>x. c)"

by(simp add: mcont_def)

lemma cont_apply:

  assumes 2: "\<And>x. cont lubb ordb Sup op \<le> (\<lambda>y. f x y)"

  and t: "cont luba orda lubb ordb (\<lambda>x. t x)"

  and 1: "\<And>y. cont luba orda Sup op \<le> (\<lambda>x. f x y)"

  and mono: "monotone orda ordb (\<lambda>x. t x)"

  and mono2: "\<And>x. monotone ordb op \<le> (\<lambda>y. f x y)"

  and mono1: "\<And>y. monotone orda op \<le> (\<lambda>x. f x y)"

  shows "cont luba orda Sup op \<le> (\<lambda>x. f x (t x))"

proof

  fix Y

  assume chain: "Complete_Partial_Order.chain orda Y" and "Y \<noteq> {}"

  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)) = \<Squnion>((\<lambda>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':

  "\<lbrakk> \<And>x. mcont lub' ord' Sup op \<le> (\<lambda>y. f x y);

     \<And>y. mcont lub ord Sup op \<le> (\<lambda>x. f x y);

     mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk>

  \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f x (t x))"

unfolding mcont_def by(blast intro: transp_le monotone2monotone cont_apply)

lemma mcont2mcont:

  "\<lbrakk>mcont lub' ord' Sup op \<le> (\<lambda>x. f x); mcont lub ord lub' ord' (\<lambda>x. t x)\<rbrakk> 

  \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f (t x))"

by(rule mcont2mcont'[OF _ mcont_const]) 

context

  fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) 

  and lub :: "'b set \<Rightarrow> 'b" ("\<Or>_" [900] 900)

begin

lemma cont_fun_lub_Sup:

  assumes chainM: "Complete_Partial_Order.chain (fun_ord op \<le>) M"

  and mcont [rule_format]: "\<forall>f\<in>M. mcont lub op \<sqsubseteq> Sup op \<le> f"

  shows "cont lub op \<sqsubseteq> Sup op \<le> (fun_lub Sup M)"

proof(rule contI)

  fix Y

  assume chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"

    and Y: "Y \<noteq> {}"

  from swap_Sup[OF chain chainM mcont[THEN mcont_mono]]

  show "fun_lub Sup M (\<Or>Y) = \<Squnion>(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:

  "\<lbrakk> Complete_Partial_Order.chain (fun_ord op \<le>) M;

    \<forall>f\<in>M. mcont lub ord Sup op \<le> f \<rbrakk>

  \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (fun_lub Sup M)"

by(simp add: mcont_def cont_fun_lub_Sup mono_lub)

lemma iterates_mcont:

  assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"

  and mono: "\<And>f. mcont lub op \<sqsubseteq> Sup op \<le> f \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (F f)"

  shows "mcont lub op \<sqsubseteq> Sup op \<le> 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: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. F f x)"

  and mcont: "\<And>f. mcont lub op \<sqsubseteq> Sup op \<le> f \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (F f)"

  shows "mcont lub op \<sqsubseteq> Sup op \<le> (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) F)"

  (is "mcont _ _ _ _ ?fixp")

unfolding mcont_def

proof(intro conjI monotoneI contI)

  have mono: "monotone (fun_ord op \<le>) (fun_ord op \<le>) F"

    by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])

  let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"

  have chain: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>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 \<sqsubseteq> y"

    show "?fixp x \<le> ?fixp y"

      unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain

    proof(rule ccpo_Sup_least)

      fix x'

      assume "x' \<in> (\<lambda>f. f x) ` ?iter"

      then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)

      also from _ `x \<sqsubseteq> y` have "f x \<le> f y"

        by(rule mcont_monoD[OF iterates_mcont[OF `f \<in> ?iter` mcont]])

      also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain

        by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)

      finally show "x' \<le> \<dots>" .

    qed

  next

    fix Y

    assume chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"

      and Y: "Y \<noteq> {}"

    { fix f

      assume "f \<in> ?iter"

      hence "f (\<Or>Y) = \<Squnion>(f ` Y)"

        using mcont chain Y by(rule mcont_contD[OF iterates_mcont]) }

    moreover have "\<Squnion>((\<lambda>f. \<Squnion>(f ` Y)) ` ?iter) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` ?iter)) ` Y)"

      using chain ccpo.chain_iterates[OF ccpo_fun mono]

      by(rule swap_Sup)(rule mcont_mono[OF iterates_mcont[OF _ mcont]])

    ultimately show "?fixp (\<Or>Y) = \<Squnion>(?fixp ` Y)" unfolding ccpo.fixp_def[OF ccpo_fun]

      by(simp add: fun_lub_apply cong: image_cong)

  }

qed

end

context

  fixes F :: "'c \<Rightarrow> 'c" and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and f

  assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. U (F (C f)) x)"

  and eq: "f \<equiv> C (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) (\<lambda>f. U (F (C f))))"

  and inverse: "\<And>f. U (C f) = f"

begin

lemma fixp_preserves_mono_uc:

  assumes mono2: "\<And>f. monotone ord op \<le> (U f) \<Longrightarrow> monotone ord op \<le> (U (F f))"

  shows "monotone ord op \<le> (U f)"

using fixp_preserves_mono[OF mono mono2] by(subst eq)(simp add: inverse)

lemma fixp_preserves_mcont_uc:

  assumes mcont: "\<And>f. mcont lubb ordb Sup op \<le> (U f) \<Longrightarrow> mcont lubb ordb Sup op \<le> (U (F f))"

  shows "mcont lubb ordb Sup op \<le> (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 "\<lambda>x. x" _ "\<lambda>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 "\<lambda>f. case_prod (case_prod f)" _ "\<lambda>f. curry (curry f)", unfolded case_prod_curry curry_case_prod, OF _ _ refl]

lemmas fixp_preserves_mono4 =

  fixp_preserves_mono_uc[of "\<lambda>f. case_prod (case_prod (case_prod f))" _ "\<lambda>f. curry (curry (curry f))", unfolded case_prod_curry curry_case_prod, OF _ _ refl]

lemmas fixp_preserves_mcont1 = fixp_preserves_mcont_uc[of "\<lambda>x. x" _ "\<lambda>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 "\<lambda>f. case_prod (case_prod f)" _ "\<lambda>f. curry (curry f)", unfolded case_prod_curry curry_case_prod, OF _ _ refl]

lemmas fixp_preserves_mcont4 =

  fixp_preserves_mcont_uc[of "\<lambda>f. case_prod (case_prod (case_prod f))" _ "\<lambda>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: "\<And>x y. \<lbrakk> x \<le> y; \<not> (x \<le> bound) \<rbrakk> \<Longrightarrow> ord (f x) (f y)"

  and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> ord bot (f x)" "ord bot bot"

  shows "monotone op \<le> ord (\<lambda>x. if x \<le> 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 ("\<Or>_" [900] 900) and ord (infix "\<sqsubseteq>" 60)

  assumes ccpo: "class.ccpo lub op \<sqsubseteq> lt"

  and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"

  and cont: "\<And>Y. \<lbrakk> Complete_Partial_Order.chain op \<le> Y; Y \<noteq> {}; \<And>x. x \<in> Y \<Longrightarrow> \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f (\<Squnion>Y) = \<Or>(f ` Y)"

  and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> bot \<sqsubseteq> f x"

  shows "mcont Sup op \<le> lub op \<sqsubseteq> (\<lambda>x. if x \<le> bound then bot else f x)" (is "mcont _ _ _ _ ?g")

proof(intro mcontI contI)

  interpret c: ccpo lub "op \<sqsubseteq>" lt by(fact ccpo)

  show "monotone op \<le> op \<sqsubseteq> ?g" by(rule monotone_if_bot)(simp_all add: mono bot)

  fix Y

  assume chain: "Complete_Partial_Order.chain op \<le> Y" and Y: "Y \<noteq> {}"

  show "?g (\<Squnion>Y) = \<Or>(?g ` Y)"

  proof(cases "Y \<subseteq> {x. x \<le> bound}")

    case True

    hence "\<Squnion>Y \<le> bound" using chain by(auto intro: ccpo_Sup_least)

    moreover have "Y \<inter> {x. \<not> x \<le> bound} = {}" using True by auto

    ultimately show ?thesis using True Y

      by (auto simp add: image_constant_conv cong del: c.strong_SUP_cong)

  next

    case False

    let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"

    have chain': "Complete_Partial_Order.chain op \<le> ?Y"

      using chain by(rule chain_subset) simp

    from False obtain y where ybound: "\<not> y \<le> bound" and y: "y \<in> Y" by blast

    hence "\<not> \<Squnion>Y \<le> bound" by (metis ccpo_Sup_upper chain order.trans)

    hence "?g (\<Squnion>Y) = f (\<Squnion>Y)" by simp

    also have "\<Squnion>Y \<le> \<Squnion>?Y" using chain

    proof(rule ccpo_Sup_least)

      fix x

      assume x: "x \<in> Y"

      show "x \<le> \<Squnion>?Y"

      proof(cases "x \<le> bound")

        case True

        with chainD[OF chain x y] have "x \<le> 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 "\<Squnion>Y = \<Squnion>?Y" by(rule antisym)(blast intro: ccpo_Sup_least[OF chain'] ccpo_Sup_upper[OF chain])

    hence "f (\<Squnion>Y) = f (\<Squnion>?Y)" by simp

    also have "f (\<Squnion>?Y) = \<Or>(f ` ?Y)" using chain' by(rule cont)(insert y ybound, auto)

    also have "\<Or>(f ` ?Y) = \<Or>(?g ` Y)"

    proof(cases "Y \<inter> {x. x \<le> 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 op \<sqsubseteq> (insert bot (f ` ?Y))"

        using chain by(auto intro!: chainI bot dest: chainD intro: mono)

      hence chain''': "Complete_Partial_Order.chain op \<sqsubseteq> (f ` ?Y)" by(rule chain_subset) blast

      have "bot \<sqsubseteq> \<Or>(f ` ?Y)" using y ybound by(blast intro: c.order_trans[OF bot] c.ccpo_Sup_upper[OF chain'''])

      hence "\<Or>(insert bot (f ` ?Y)) \<sqsubseteq> \<Or>(f ` ?Y)" using chain''

        by(auto intro: c.ccpo_Sup_least c.ccpo_Sup_upper[OF chain''']) 

      with _ have "\<dots> = \<Or>(insert bot (f ` ?Y))"

        by(rule c.antisym)(blast intro: c.ccpo_Sup_least[OF chain'''] c.ccpo_Sup_upper[OF chain''])

      also have "insert bot (f ` ?Y) = ?g ` Y" using False by auto

      finally show ?thesis .

    qed

    finally show ?thesis .

  qed

qed

context partial_function_definitions begin

lemma mcont_const [cont_intro, simp]:

  "mcont luba orda lub leq (\<lambda>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 (\<lambda>y. f y)" "monotone orda ordb (\<lambda>x. t x)"

  shows "monotone orda leq (\<lambda>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: "\<And>x. g x = (if leq x bound then bot else f x)"

  and mono: "\<And>x y. \<lbrakk> leq x y; \<not> leq x bound \<rbrakk> \<Longrightarrow> ord (f x) (f y)"

  and bot: "\<And>x. \<not> leq x bound \<Longrightarrow> 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: "\<And>x. \<not> leq x bound \<Longrightarrow> ord bot (f x)"

  and g: "\<And>x. g x = (if leq x bound then bot else f x)"

  and mono: "\<And>x y. \<lbrakk> leq x y; \<not> leq x bound \<rbrakk> \<Longrightarrow> ord (f x) (f y)"

  and cont: "\<And>Y. \<lbrakk> Complete_Partial_Order.chain leq Y; Y \<noteq> {}; \<And>x. x \<in> Y \<Longrightarrow> \<not> leq x bound \<rbrakk> \<Longrightarrow> 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 (\<lambda>x. P x)"

  and mcont: "mcont lubb ordb luba orda f"

  shows "ccpo.admissible lubb ordb (\<lambda>x. P (f x))"

apply(rule ccpo.admissibleI)

apply(frule (1) mcont_contD[OF mcont])

apply(auto intro: ccpo.admissibleD[OF adm] chain_imageI dest: mcont_monoD[OF mcont])

done

lemmas [simp, cont_intro] = 

  admissible_all

  admissible_ball

  admissible_const

  admissible_conj

lemma admissible_disj' [simp, cont_intro]:

  "\<lbrakk> class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord P; ccpo.admissible lub ord Q \<rbrakk>

  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<or> Q x)"

by(rule ccpo.admissible_disj)

lemma admissible_imp' [cont_intro]:

  "\<lbrakk> 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 \<Longrightarrow> ccpo.admissible lub ord (\<lambda>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 op \<subseteq> (\<lambda>A. x \<notin> A)"

by(rule ccpo.admissibleI) auto

lemma admissible_eqI:

  assumes f: "cont luba orda lub ord (\<lambda>x. f x)"

  and g: "cont luba orda lub ord (\<lambda>x. g x)"

  shows "ccpo.admissible luba orda (\<lambda>x. f x = g x)"

apply(rule ccpo.admissibleI)

apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong)

done

corollary admissible_eq_mcontI [cont_intro]:

  "\<lbrakk> mcont luba orda lub ord (\<lambda>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]:

  "\<lbrakk> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x); ccpo.admissible lub ord (\<lambda>x. Q x \<longrightarrow> P x) \<rbrakk>

  \<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 op \<le> (\<lambda>x. f x)"

  and g: "mcont luba orda Sup op \<le> (\<lambda>x. g x)"

  shows "ccpo.admissible luba orda (\<lambda>x. f x \<le> g x)"

proof(rule ccpo.admissibleI)

  fix A

  assume chain: "Complete_Partial_Order.chain orda A"

    and le: "\<forall>x\<in>A. f x \<le> g x"

    and False: "A \<noteq> {}"

  have "f (luba A) = \<Squnion>(f ` A)" by(simp add: mcont_contD[OF f] chain False)

  also have "\<dots> \<le> \<Squnion>(g ` A)"

  proof(rule ccpo_Sup_least)

    from chain show "Complete_Partial_Order.chain op \<le> (f ` A)"

      by(rule chain_imageI)(rule mcont_monoD[OF f])

    fix x

    assume "x \<in> f ` A"

    then obtain y where "y \<in> A" "x = f y" by blast note this(2)

    also have "f y \<le> g y" using le `y \<in> A` by simp

    also have "Complete_Partial_Order.chain op \<le> (g ` A)"

      using chain by(rule chain_imageI)(rule mcont_monoD[OF g])

    hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: `y \<in> A`)

    finally show "x \<le> \<dots>" .

  qed

  also have "\<dots> = g (luba A)" by(simp add: mcont_contD[OF g] chain False)

  finally show "f (luba A) \<le> g (luba A)" .

qed

end

lemma admissible_leI:

  fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or>_" [900] 900)

  assumes "class.ccpo lub op \<sqsubseteq> (mk_less op \<sqsubseteq>)"

  and "mcont luba orda lub op \<sqsubseteq> (\<lambda>x. f x)"

  and "mcont luba orda lub op \<sqsubseteq> (\<lambda>x. g x)"

  shows "ccpo.admissible luba orda (\<lambda>x. f x \<sqsubseteq> 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 op \<le> (\<lambda>x. \<not> op \<le> x y)"

by(rule ccpo.admissibleI)(simp add: ccpo_Sup_below_iff)

end

lemma (in preorder) preorder [cont_intro, simp]: "class.preorder op \<le> (mk_less op \<le>)"

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

inductive compact :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"

  for lub ord x 

where compact:

  "\<lbrakk> ccpo.admissible lub ord (\<lambda>y. \<not> ord x y);

     ccpo.admissible lub ord (\<lambda>y. x \<noteq> y) \<rbrakk>

  \<Longrightarrow> compact lub ord x"

hide_fact (open) compact

context ccpo begin

lemma compactI:

  assumes "ccpo.admissible Sup op \<le> (\<lambda>y. \<not> x \<le> y)"

  shows "compact Sup op \<le> x"

using assms

proof(rule compact.intros)

  have neq: "(\<lambda>y. x \<noteq> y) = (\<lambda>y. \<not> x \<le> y \<or> \<not> y \<le> x)" by(auto)

  show "ccpo.admissible Sup op \<le> (\<lambda>y. x \<noteq> y)"

    by(subst neq)(rule admissible_disj admissible_not_below assms)+

qed

lemma compact_bot:

  assumes "x = Sup {}"

  shows "compact Sup op \<le> x"

proof(rule compactI)

  show "ccpo.admissible Sup op \<le> (\<lambda>y. \<not> x \<le> 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: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. k \<noteq> x)"

by(simp add: compact.simps)

lemma admissible_neq_compact' [THEN admissible_subst, cont_intro, simp]:

  shows admissible_neq_compact: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. x \<noteq> 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 op \<le> P"

  and mono: "monotone op \<le> op \<le> f"

  and bot: "P (\<Squnion>{})"

  and step: "\<And>x. \<lbrakk> x \<le> ccpo_class.fixp f; P x \<rbrakk> \<Longrightarrow> P (f x)"

  shows "P (ccpo_class.fixp f)"

proof(rule fixp_induct[where P="\<lambda>x. x \<le> ccpo_class.fixp f \<and> P x", THEN conjunct2])

  note [cont_intro] = admissible_leI

  show "ccpo.admissible Sup op \<le> (\<lambda>x. x \<le> ccpo_class.fixp f \<and> P x)" by simp

next

  show "\<Squnion>{} \<le> ccpo_class.fixp f \<and> P (\<Squnion>{})"

    by(auto simp add: bot intro: ccpo_Sup_least chain_empty)

next

  fix x

  assume "x \<le> ccpo_class.fixp f \<and> P x"

  thus "f x \<le> ccpo_class.fixp f \<and> 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 \<Rightarrow> 'c"

    and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a"

    and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"

    and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"

  assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"

    and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"

    and inverse: "\<And>f. U (C f) = f"

    and adm: "ccpo.admissible lub_fun le_fun P"

    and bot: "P (\<lambda>_. lub {})"

    and step: "\<And>f'. \<lbrakk> P (U f'); le_fun (U f') (U f) \<rbrakk> \<Longrightarrow> 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