src/HOL/Library/Complete_Partial_Order2.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 63243 1bc6816fd525
child 63649 e690d6f2185b
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title:      HOL/Library/Complete_Partial_Order2.thy
     2     Author:     Andreas Lochbihler, ETH Zurich
     3 *)
     4 
     5 section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
     6 
     7 theory Complete_Partial_Order2 imports 
     8   Main
     9   "~~/src/HOL/Library/Lattice_Syntax"
    10 begin
    11 
    12 lemma chain_transfer [transfer_rule]:
    13   includes lifting_syntax
    14   shows "((A ===> A ===> op =) ===> rel_set A ===> op =) Complete_Partial_Order.chain Complete_Partial_Order.chain"
    15 unfolding chain_def[abs_def] by transfer_prover
    16 
    17 lemma linorder_chain [simp, intro!]:
    18   fixes Y :: "_ :: linorder set"
    19   shows "Complete_Partial_Order.chain op \<le> Y"
    20 by(auto intro: chainI)
    21 
    22 lemma fun_lub_apply: "\<And>Sup. fun_lub Sup Y x = Sup ((\<lambda>f. f x) ` Y)"
    23 by(simp add: fun_lub_def image_def)
    24 
    25 lemma fun_lub_empty [simp]: "fun_lub lub {} = (\<lambda>_. lub {})"
    26 by(rule ext)(simp add: fun_lub_apply)
    27 
    28 lemma chain_fun_ordD: 
    29   assumes "Complete_Partial_Order.chain (fun_ord le) Y"
    30   shows "Complete_Partial_Order.chain le ((\<lambda>f. f x) ` Y)"
    31 by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def)
    32 
    33 lemma chain_Diff:
    34   "Complete_Partial_Order.chain ord A
    35   \<Longrightarrow> Complete_Partial_Order.chain ord (A - B)"
    36 by(erule chain_subset) blast
    37 
    38 lemma chain_rel_prodD1:
    39   "Complete_Partial_Order.chain (rel_prod orda ordb) Y
    40   \<Longrightarrow> Complete_Partial_Order.chain orda (fst ` Y)"
    41 by(auto 4 3 simp add: chain_def)
    42 
    43 lemma chain_rel_prodD2:
    44   "Complete_Partial_Order.chain (rel_prod orda ordb) Y
    45   \<Longrightarrow> Complete_Partial_Order.chain ordb (snd ` Y)"
    46 by(auto 4 3 simp add: chain_def)
    47 
    48 
    49 context ccpo begin
    50 
    51 lemma ccpo_fun: "class.ccpo (fun_lub Sup) (fun_ord op \<le>) (mk_less (fun_ord op \<le>))"
    52   by standard (auto 4 3 simp add: mk_less_def fun_ord_def fun_lub_apply
    53     intro: order.trans antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
    54 
    55 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)"
    56 by(fast intro: order_trans[OF ccpo_Sup_upper] ccpo_Sup_least)
    57 
    58 lemma Sup_minus_bot: 
    59   assumes chain: "Complete_Partial_Order.chain op \<le> A"
    60   shows "\<Squnion>(A - {\<Squnion>{}}) = \<Squnion>A"
    61 apply(rule antisym)
    62  apply(blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])
    63 apply(rule ccpo_Sup_least[OF chain])
    64 apply(case_tac "x = \<Squnion>{}")
    65 by(blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+
    66 
    67 lemma mono_lub:
    68   fixes le_b (infix "\<sqsubseteq>" 60)
    69   assumes chain: "Complete_Partial_Order.chain (fun_ord op \<le>) Y"
    70   and mono: "\<And>f. f \<in> Y \<Longrightarrow> monotone le_b op \<le> f"
    71   shows "monotone op \<sqsubseteq> op \<le> (fun_lub Sup Y)"
    72 proof(rule monotoneI)
    73   fix x y
    74   assume "x \<sqsubseteq> y"
    75 
    76   have chain'': "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` Y)"
    77     using chain by(rule chain_imageI)(simp add: fun_ord_def)
    78   then show "fun_lub Sup Y x \<le> fun_lub Sup Y y" unfolding fun_lub_apply
    79   proof(rule ccpo_Sup_least)
    80     fix x'
    81     assume "x' \<in> (\<lambda>f. f x) ` Y"
    82     then obtain f where "f \<in> Y" "x' = f x" by blast
    83     note \<open>x' = f x\<close> also
    84     from \<open>f \<in> Y\<close> \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y" by(blast dest: mono monotoneD)
    85     also have "\<dots> \<le> \<Squnion>((\<lambda>f. f y) ` Y)" using chain''
    86       by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Y\<close>)
    87     finally show "x' \<le> \<Squnion>((\<lambda>f. f y) ` Y)" .
    88   qed
    89 qed
    90 
    91 context
    92   fixes le_b (infix "\<sqsubseteq>" 60) and Y f
    93   assumes chain: "Complete_Partial_Order.chain le_b Y" 
    94   and mono1: "\<And>y. y \<in> Y \<Longrightarrow> monotone le_b op \<le> (\<lambda>x. f x y)"
    95   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"
    96 begin
    97 
    98 lemma Sup_mono: 
    99   assumes le: "x \<sqsubseteq> y" and x: "x \<in> Y" and y: "y \<in> Y"
   100   shows "\<Squnion>(f x ` Y) \<le> \<Squnion>(f y ` Y)" (is "_ \<le> ?rhs")
   101 proof(rule ccpo_Sup_least)
   102   from chain show chain': "Complete_Partial_Order.chain op \<le> (f x ` Y)" when "x \<in> Y" for x
   103     by(rule chain_imageI) (insert that, auto dest: mono2)
   104 
   105   fix x'
   106   assume "x' \<in> f x ` Y"
   107   then obtain y' where "y' \<in> Y" "x' = f x y'" by blast note this(2)
   108   also from mono1[OF \<open>y' \<in> Y\<close>] le have "\<dots> \<le> f y y'" by(rule monotoneD)
   109   also have "\<dots> \<le> ?rhs" using chain'[OF y]
   110     by (auto intro!: ccpo_Sup_upper simp add: \<open>y' \<in> Y\<close>)
   111   finally show "x' \<le> ?rhs" .
   112 qed(rule x)
   113 
   114 lemma diag_Sup: "\<Squnion>((\<lambda>x. \<Squnion>(f x ` Y)) ` Y) = \<Squnion>((\<lambda>x. f x x) ` Y)" (is "?lhs = ?rhs")
   115 proof(rule antisym)
   116   have chain1: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>(f x ` Y)) ` Y)"
   117     using chain by(rule chain_imageI)(rule Sup_mono)
   118   have chain2: "\<And>y'. y' \<in> Y \<Longrightarrow> Complete_Partial_Order.chain op \<le> (f y' ` Y)" using chain
   119     by(rule chain_imageI)(auto dest: mono2)
   120   have chain3: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. f x x) ` Y)"
   121     using chain by(rule chain_imageI)(auto intro: monotoneD[OF mono1] mono2 order.trans)
   122 
   123   show "?lhs \<le> ?rhs" using chain1
   124   proof(rule ccpo_Sup_least)
   125     fix x'
   126     assume "x' \<in> (\<lambda>x. \<Squnion>(f x ` Y)) ` Y"
   127     then obtain y' where "y' \<in> Y" "x' = \<Squnion>(f y' ` Y)" by blast note this(2)
   128     also have "\<dots> \<le> ?rhs" using chain2[OF \<open>y' \<in> Y\<close>]
   129     proof(rule ccpo_Sup_least)
   130       fix x
   131       assume "x \<in> f y' ` Y"
   132       then obtain y where "y \<in> Y" and x: "x = f y' y" by blast
   133       define y'' where "y'' = (if y \<sqsubseteq> y' then y' else y)"
   134       from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
   135       hence "f y' y \<le> f y'' y''" using \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close>
   136         by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1])
   137       also from \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y'' \<in> Y" by(simp add: y''_def)
   138       from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: \<open>y'' \<in> Y\<close>)
   139       finally show "x \<le> ?rhs" by(simp add: x)
   140     qed
   141     finally show "x' \<le> ?rhs" .
   142   qed
   143 
   144   show "?rhs \<le> ?lhs" using chain3
   145   proof(rule ccpo_Sup_least)
   146     fix y
   147     assume "y \<in> (\<lambda>x. f x x) ` Y"
   148     then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2)
   149     also from chain2[OF \<open>x \<in> Y\<close>] have "\<dots> \<le> \<Squnion>(f x ` Y)"
   150       by(rule ccpo_Sup_upper)(simp add: \<open>x \<in> Y\<close>)
   151     also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \<open>x \<in> Y\<close>)
   152     finally show "y \<le> ?lhs" .
   153   qed
   154 qed
   155 
   156 end
   157 
   158 lemma Sup_image_mono_le:
   159   fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>_" [900] 900)
   160   assumes ccpo: "class.ccpo Sup_b op \<sqsubseteq> lt_b"
   161   assumes chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
   162   and mono: "\<And>x y. \<lbrakk> x \<sqsubseteq> y; x \<in> Y \<rbrakk> \<Longrightarrow> f x \<le> f y"
   163   shows "Sup (f ` Y) \<le> f (\<Or>Y)"
   164 proof(rule ccpo_Sup_least)
   165   show "Complete_Partial_Order.chain op \<le> (f ` Y)"
   166     using chain by(rule chain_imageI)(rule mono)
   167 
   168   fix x
   169   assume "x \<in> f ` Y"
   170   then obtain y where "y \<in> Y" and "x = f y" by blast note this(2)
   171   also have "y \<sqsubseteq> \<Or>Y" using ccpo chain \<open>y \<in> Y\<close> by(rule ccpo.ccpo_Sup_upper)
   172   hence "f y \<le> f (\<Or>Y)" using \<open>y \<in> Y\<close> by(rule mono)
   173   finally show "x \<le> \<dots>" .
   174 qed
   175 
   176 lemma swap_Sup:
   177   fixes le_b (infix "\<sqsubseteq>" 60)
   178   assumes Y: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
   179   and Z: "Complete_Partial_Order.chain (fun_ord op \<le>) Z"
   180   and mono: "\<And>f. f \<in> Z \<Longrightarrow> monotone op \<sqsubseteq> op \<le> f"
   181   shows "\<Squnion>((\<lambda>x. \<Squnion>(x ` Y)) ` Z) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y)"
   182   (is "?lhs = ?rhs")
   183 proof(cases "Y = {}")
   184   case True
   185   then show ?thesis
   186     by (simp add: image_constant_conv cong del: strong_SUP_cong)
   187 next
   188   case False
   189   have chain1: "\<And>f. f \<in> Z \<Longrightarrow> Complete_Partial_Order.chain op \<le> (f ` Y)"
   190     by(rule chain_imageI[OF Y])(rule monotoneD[OF mono])
   191   have chain2: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>(x ` Y)) ` Z)" using Z
   192   proof(rule chain_imageI)
   193     fix f g
   194     assume "f \<in> Z" "g \<in> Z"
   195       and "fun_ord op \<le> f g"
   196     from chain1[OF \<open>f \<in> Z\<close>] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
   197     proof(rule ccpo_Sup_least)
   198       fix x
   199       assume "x \<in> f ` Y"
   200       then obtain y where "y \<in> Y" "x = f y" by blast note this(2)
   201       also have "\<dots> \<le> g y" using \<open>fun_ord op \<le> f g\<close> by(simp add: fun_ord_def)
   202       also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF \<open>g \<in> Z\<close>]
   203         by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
   204       finally show "x \<le> \<Squnion>(g ` Y)" .
   205     qed
   206   qed
   207   have chain3: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` Z)"
   208     using Z by(rule chain_imageI)(simp add: fun_ord_def)
   209   have chain4: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y)"
   210     using Y
   211   proof(rule chain_imageI)
   212     fix f x y
   213     assume "x \<sqsubseteq> y"
   214     show "\<Squnion>((\<lambda>f. f x) ` Z) \<le> \<Squnion>((\<lambda>f. f y) ` Z)" (is "_ \<le> ?rhs") using chain3
   215     proof(rule ccpo_Sup_least)
   216       fix x'
   217       assume "x' \<in> (\<lambda>f. f x) ` Z"
   218       then obtain f where "f \<in> Z" "x' = f x" by blast note this(2)
   219       also have "f x \<le> f y" using \<open>f \<in> Z\<close> \<open>x \<sqsubseteq> y\<close> by(rule monotoneD[OF mono])
   220       also have "f y \<le> ?rhs" using chain3
   221         by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
   222       finally show "x' \<le> ?rhs" .
   223     qed
   224   qed
   225 
   226   from chain2 have "?lhs \<le> ?rhs"
   227   proof(rule ccpo_Sup_least)
   228     fix x
   229     assume "x \<in> (\<lambda>x. \<Squnion>(x ` Y)) ` Z"
   230     then obtain f where "f \<in> Z" "x = \<Squnion>(f ` Y)" by blast note this(2)
   231     also have "\<dots> \<le> ?rhs" using chain1[OF \<open>f \<in> Z\<close>]
   232     proof(rule ccpo_Sup_least)
   233       fix x'
   234       assume "x' \<in> f ` Y"
   235       then obtain y where "y \<in> Y" "x' = f y" by blast note this(2)
   236       also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3
   237         by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
   238       also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
   239       finally show "x' \<le> ?rhs" .
   240     qed
   241     finally show "x \<le> ?rhs" .
   242   qed
   243   moreover
   244   have "?rhs \<le> ?lhs" using chain4
   245   proof(rule ccpo_Sup_least)
   246     fix x
   247     assume "x \<in> (\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y"
   248     then obtain y where "y \<in> Y" "x = \<Squnion>((\<lambda>f. f y) ` Z)" by blast note this(2)
   249     also have "\<dots> \<le> ?lhs" using chain3
   250     proof(rule ccpo_Sup_least)
   251       fix x'
   252       assume "x' \<in> (\<lambda>f. f y) ` Z"
   253       then obtain f where "f \<in> Z" "x' = f y" by blast note this(2)
   254       also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF \<open>f \<in> Z\<close>]
   255         by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
   256       also have "\<dots> \<le> ?lhs" using chain2
   257         by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
   258       finally show "x' \<le> ?lhs" .
   259     qed
   260     finally show "x \<le> ?lhs" .
   261   qed
   262   ultimately show "?lhs = ?rhs" by(rule antisym)
   263 qed
   264 
   265 lemma fixp_mono:
   266   assumes fg: "fun_ord op \<le> f g"
   267   and f: "monotone op \<le> op \<le> f"
   268   and g: "monotone op \<le> op \<le> g"
   269   shows "ccpo_class.fixp f \<le> ccpo_class.fixp g"
   270 unfolding fixp_def
   271 proof(rule ccpo_Sup_least)
   272   fix x
   273   assume "x \<in> ccpo_class.iterates f"
   274   thus "x \<le> \<Squnion>ccpo_class.iterates g"
   275   proof induction
   276     case (step x)
   277     from f step.IH have "f x \<le> f (\<Squnion>ccpo_class.iterates g)" by(rule monotoneD)
   278     also have "\<dots> \<le> g (\<Squnion>ccpo_class.iterates g)" using fg by(simp add: fun_ord_def)
   279     also have "\<dots> = \<Squnion>ccpo_class.iterates g" by(fold fixp_def fixp_unfold[OF g]) simp
   280     finally show ?case .
   281   qed(blast intro: ccpo_Sup_least)
   282 qed(rule chain_iterates[OF f])
   283 
   284 context fixes ordb :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) begin
   285 
   286 lemma iterates_mono:
   287   assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
   288   and mono: "\<And>f. monotone op \<sqsubseteq> op \<le> f \<Longrightarrow> monotone op \<sqsubseteq> op \<le> (F f)"
   289   shows "monotone op \<sqsubseteq> op \<le> f"
   290 using f
   291 by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mono_lub)+
   292 
   293 lemma fixp_preserves_mono:
   294   assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. F f x)"
   295   and mono2: "\<And>f. monotone op \<sqsubseteq> op \<le> f \<Longrightarrow> monotone op \<sqsubseteq> op \<le> (F f)"
   296   shows "monotone op \<sqsubseteq> op \<le> (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) F)"
   297   (is "monotone _ _ ?fixp")
   298 proof(rule monotoneI)
   299   have mono: "monotone (fun_ord op \<le>) (fun_ord op \<le>) F"
   300     by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])
   301   let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
   302   have chain: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` ?iter)"
   303     by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def)
   304 
   305   fix x y
   306   assume "x \<sqsubseteq> y"
   307   show "?fixp x \<le> ?fixp y"
   308     apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
   309     using chain
   310   proof(rule ccpo_Sup_least)
   311     fix x'
   312     assume "x' \<in> (\<lambda>f. f x) ` ?iter"
   313     then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
   314     also have "f x \<le> f y"
   315       by(rule monotoneD[OF iterates_mono[OF \<open>f \<in> ?iter\<close> mono2]])(blast intro: \<open>x \<sqsubseteq> y\<close>)+
   316     also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
   317       by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
   318     finally show "x' \<le> \<dots>" .
   319   qed
   320 qed
   321 
   322 end
   323 
   324 end
   325 
   326 lemma monotone2monotone:
   327   assumes 2: "\<And>x. monotone ordb ordc (\<lambda>y. f x y)"
   328   and t: "monotone orda ordb (\<lambda>x. t x)"
   329   and 1: "\<And>y. monotone orda ordc (\<lambda>x. f x y)"
   330   and trans: "transp ordc"
   331   shows "monotone orda ordc (\<lambda>x. f x (t x))"
   332 by(blast intro: monotoneI transpD[OF trans] monotoneD[OF t] monotoneD[OF 2] monotoneD[OF 1])
   333 
   334 subsection \<open>Continuity\<close>
   335 
   336 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"
   337 where
   338   "cont luba orda lubb ordb f \<longleftrightarrow> 
   339   (\<forall>Y. Complete_Partial_Order.chain orda Y \<longrightarrow> Y \<noteq> {} \<longrightarrow> f (luba Y) = lubb (f ` Y))"
   340 
   341 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"
   342 where
   343   "mcont luba orda lubb ordb f \<longleftrightarrow>
   344    monotone orda ordb f \<and> cont luba orda lubb ordb f"
   345 
   346 subsubsection \<open>Theorem collection \<open>cont_intro\<close>\<close>
   347 
   348 named_theorems cont_intro "continuity and admissibility intro rules"
   349 ML \<open>
   350 (* apply cont_intro rules as intro and try to solve 
   351    the remaining of the emerging subgoals with simp *)
   352 fun cont_intro_tac ctxt =
   353   REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems cont_intro})))
   354   THEN_ALL_NEW (SOLVED' (simp_tac ctxt))
   355 
   356 fun cont_intro_simproc ctxt ct =
   357   let
   358     fun mk_stmt t = t
   359       |> HOLogic.mk_Trueprop
   360       |> Thm.cterm_of ctxt
   361       |> Goal.init
   362     fun mk_thm t =
   363       case SINGLE (cont_intro_tac ctxt 1) (mk_stmt t) of
   364         SOME thm => SOME (Goal.finish ctxt thm RS @{thm Eq_TrueI})
   365       | NONE => NONE
   366   in
   367     case Thm.term_of ct of
   368       t as Const (@{const_name ccpo.admissible}, _) $ _ $ _ $ _ => mk_thm t
   369     | t as Const (@{const_name mcont}, _) $ _ $ _ $ _ $ _ $ _ => mk_thm t
   370     | t as Const (@{const_name monotone}, _) $ _ $ _ $ _ => mk_thm t
   371     | _ => NONE
   372   end
   373   handle THM _ => NONE 
   374   | TYPE _ => NONE
   375 \<close>
   376 
   377 simproc_setup "cont_intro"
   378   ( "ccpo.admissible lub ord P"
   379   | "mcont lub ord lub' ord' f"
   380   | "monotone ord ord' f"
   381   ) = \<open>K cont_intro_simproc\<close>
   382 
   383 lemmas [cont_intro] =
   384   call_mono
   385   let_mono
   386   if_mono
   387   option.const_mono
   388   tailrec.const_mono
   389   bind_mono
   390 
   391 declare if_mono[simp]
   392 
   393 lemma monotone_id' [cont_intro]: "monotone ord ord (\<lambda>x. x)"
   394 by(simp add: monotone_def)
   395 
   396 lemma monotone_applyI:
   397   "monotone orda ordb F \<Longrightarrow> monotone (fun_ord orda) ordb (\<lambda>f. F (f x))"
   398 by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
   399 
   400 lemma monotone_if_fun [partial_function_mono]:
   401   "\<lbrakk> monotone (fun_ord orda) (fun_ord ordb) F; monotone (fun_ord orda) (fun_ord ordb) G \<rbrakk>
   402   \<Longrightarrow> monotone (fun_ord orda) (fun_ord ordb) (\<lambda>f n. if c n then F f n else G f n)"
   403 by(simp add: monotone_def fun_ord_def)
   404 
   405 lemma monotone_fun_apply_fun [partial_function_mono]: 
   406   "monotone (fun_ord (fun_ord ord)) (fun_ord ord) (\<lambda>f n. f t (g n))"
   407 by(rule monotoneI)(simp add: fun_ord_def)
   408 
   409 lemma monotone_fun_ord_apply: 
   410   "monotone orda (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. monotone orda ordb (\<lambda>y. f y x))"
   411 by(auto simp add: monotone_def fun_ord_def)
   412 
   413 context preorder begin
   414 
   415 lemma transp_le [simp, cont_intro]: "transp op \<le>"
   416 by(rule transpI)(rule order_trans)
   417 
   418 lemma monotone_const [simp, cont_intro]: "monotone ord op \<le> (\<lambda>_. c)"
   419 by(rule monotoneI) simp
   420 
   421 end
   422 
   423 lemma transp_le [cont_intro, simp]:
   424   "class.preorder ord (mk_less ord) \<Longrightarrow> transp ord"
   425 by(rule preorder.transp_le)
   426 
   427 context partial_function_definitions begin
   428 
   429 declare const_mono [cont_intro, simp]
   430 
   431 lemma transp_le [cont_intro, simp]: "transp leq"
   432 by(rule transpI)(rule leq_trans)
   433 
   434 lemma preorder [cont_intro, simp]: "class.preorder leq (mk_less leq)"
   435 by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans)
   436 
   437 declare ccpo[cont_intro, simp]
   438 
   439 end
   440 
   441 lemma contI [intro?]:
   442   "(\<And>Y. \<lbrakk> Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> \<Longrightarrow> f (luba Y) = lubb (f ` Y)) 
   443   \<Longrightarrow> cont luba orda lubb ordb f"
   444 unfolding cont_def by blast
   445 
   446 lemma contD:
   447   "\<lbrakk> cont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> 
   448   \<Longrightarrow> f (luba Y) = lubb (f ` Y)"
   449 unfolding cont_def by blast
   450 
   451 lemma cont_id [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord id"
   452 by(rule contI) simp
   453 
   454 lemma cont_id' [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord (\<lambda>x. x)"
   455 using cont_id[unfolded id_def] .
   456 
   457 lemma cont_applyI [cont_intro]:
   458   assumes cont: "cont luba orda lubb ordb g"
   459   shows "cont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. g (f x))"
   460 by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont])
   461 
   462 lemma call_cont: "cont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
   463 by(simp add: cont_def fun_lub_apply)
   464 
   465 lemma cont_if [cont_intro]:
   466   "\<lbrakk> cont luba orda lubb ordb f; cont luba orda lubb ordb g \<rbrakk>
   467   \<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
   468 by(cases c) simp_all
   469 
   470 lemma mcontI [intro?]:
   471    "\<lbrakk> monotone orda ordb f; cont luba orda lubb ordb f \<rbrakk> \<Longrightarrow> mcont luba orda lubb ordb f"
   472 by(simp add: mcont_def)
   473 
   474 lemma mcont_mono: "mcont luba orda lubb ordb f \<Longrightarrow> monotone orda ordb f"
   475 by(simp add: mcont_def)
   476 
   477 lemma mcont_cont [simp]: "mcont luba orda lubb ordb f \<Longrightarrow> cont luba orda lubb ordb f"
   478 by(simp add: mcont_def)
   479 
   480 lemma mcont_monoD:
   481   "\<lbrakk> mcont luba orda lubb ordb f; orda x y \<rbrakk> \<Longrightarrow> ordb (f x) (f y)"
   482 by(auto simp add: mcont_def dest: monotoneD)
   483 
   484 lemma mcont_contD:
   485   "\<lbrakk> mcont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk>
   486   \<Longrightarrow> f (luba Y) = lubb (f ` Y)"
   487 by(auto simp add: mcont_def dest: contD)
   488 
   489 lemma mcont_call [cont_intro, simp]:
   490   "mcont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
   491 by(simp add: mcont_def call_mono call_cont)
   492 
   493 lemma mcont_id' [cont_intro, simp]: "mcont lub ord lub ord (\<lambda>x. x)"
   494 by(simp add: mcont_def monotone_id')
   495 
   496 lemma mcont_applyI:
   497   "mcont luba orda lubb ordb (\<lambda>x. F x) \<Longrightarrow> mcont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. F (f x))"
   498 by(simp add: mcont_def monotone_applyI cont_applyI)
   499 
   500 lemma mcont_if [cont_intro, simp]:
   501   "\<lbrakk> mcont luba orda lubb ordb (\<lambda>x. f x); mcont luba orda lubb ordb (\<lambda>x. g x) \<rbrakk>
   502   \<Longrightarrow> mcont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
   503 by(simp add: mcont_def cont_if)
   504 
   505 lemma cont_fun_lub_apply: 
   506   "cont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. cont luba orda lubb ordb (\<lambda>y. f y x))"
   507 by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def)
   508 
   509 lemma mcont_fun_lub_apply: 
   510   "mcont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. mcont luba orda lubb ordb (\<lambda>y. f y x))"
   511 by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def)
   512 
   513 context ccpo begin
   514 
   515 lemma cont_const [simp, cont_intro]: "cont luba orda Sup op \<le> (\<lambda>x. c)"
   516 by (rule contI) (simp add: image_constant_conv cong del: strong_SUP_cong)
   517 
   518 lemma mcont_const [cont_intro, simp]:
   519   "mcont luba orda Sup op \<le> (\<lambda>x. c)"
   520 by(simp add: mcont_def)
   521 
   522 lemma cont_apply:
   523   assumes 2: "\<And>x. cont lubb ordb Sup op \<le> (\<lambda>y. f x y)"
   524   and t: "cont luba orda lubb ordb (\<lambda>x. t x)"
   525   and 1: "\<And>y. cont luba orda Sup op \<le> (\<lambda>x. f x y)"
   526   and mono: "monotone orda ordb (\<lambda>x. t x)"
   527   and mono2: "\<And>x. monotone ordb op \<le> (\<lambda>y. f x y)"
   528   and mono1: "\<And>y. monotone orda op \<le> (\<lambda>x. f x y)"
   529   shows "cont luba orda Sup op \<le> (\<lambda>x. f x (t x))"
   530 proof
   531   fix Y
   532   assume chain: "Complete_Partial_Order.chain orda Y" and "Y \<noteq> {}"
   533   moreover from chain have chain': "Complete_Partial_Order.chain ordb (t ` Y)"
   534     by(rule chain_imageI)(rule monotoneD[OF mono])
   535   ultimately show "f (luba Y) (t (luba Y)) = \<Squnion>((\<lambda>x. f x (t x)) ` Y)"
   536     by(simp add: contD[OF 1] contD[OF t] contD[OF 2] image_image)
   537       (rule diag_Sup[OF chain], auto intro: monotone2monotone[OF mono2 mono monotone_const transpI] monotoneD[OF mono1])
   538 qed
   539 
   540 lemma mcont2mcont':
   541   "\<lbrakk> \<And>x. mcont lub' ord' Sup op \<le> (\<lambda>y. f x y);
   542      \<And>y. mcont lub ord Sup op \<le> (\<lambda>x. f x y);
   543      mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk>
   544   \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f x (t x))"
   545 unfolding mcont_def by(blast intro: transp_le monotone2monotone cont_apply)
   546 
   547 lemma mcont2mcont:
   548   "\<lbrakk>mcont lub' ord' Sup op \<le> (\<lambda>x. f x); mcont lub ord lub' ord' (\<lambda>x. t x)\<rbrakk> 
   549   \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f (t x))"
   550 by(rule mcont2mcont'[OF _ mcont_const]) 
   551 
   552 context
   553   fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) 
   554   and lub :: "'b set \<Rightarrow> 'b" ("\<Or>_" [900] 900)
   555 begin
   556 
   557 lemma cont_fun_lub_Sup:
   558   assumes chainM: "Complete_Partial_Order.chain (fun_ord op \<le>) M"
   559   and mcont [rule_format]: "\<forall>f\<in>M. mcont lub op \<sqsubseteq> Sup op \<le> f"
   560   shows "cont lub op \<sqsubseteq> Sup op \<le> (fun_lub Sup M)"
   561 proof(rule contI)
   562   fix Y
   563   assume chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
   564     and Y: "Y \<noteq> {}"
   565   from swap_Sup[OF chain chainM mcont[THEN mcont_mono]]
   566   show "fun_lub Sup M (\<Or>Y) = \<Squnion>(fun_lub Sup M ` Y)"
   567     by(simp add: mcont_contD[OF mcont chain Y] fun_lub_apply cong: image_cong)
   568 qed
   569 
   570 lemma mcont_fun_lub_Sup:
   571   "\<lbrakk> Complete_Partial_Order.chain (fun_ord op \<le>) M;
   572     \<forall>f\<in>M. mcont lub ord Sup op \<le> f \<rbrakk>
   573   \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (fun_lub Sup M)"
   574 by(simp add: mcont_def cont_fun_lub_Sup mono_lub)
   575 
   576 lemma iterates_mcont:
   577   assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
   578   and mono: "\<And>f. mcont lub op \<sqsubseteq> Sup op \<le> f \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (F f)"
   579   shows "mcont lub op \<sqsubseteq> Sup op \<le> f"
   580 using f
   581 by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mcont_fun_lub_Sup)+
   582 
   583 lemma fixp_preserves_mcont:
   584   assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. F f x)"
   585   and mcont: "\<And>f. mcont lub op \<sqsubseteq> Sup op \<le> f \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (F f)"
   586   shows "mcont lub op \<sqsubseteq> Sup op \<le> (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) F)"
   587   (is "mcont _ _ _ _ ?fixp")
   588 unfolding mcont_def
   589 proof(intro conjI monotoneI contI)
   590   have mono: "monotone (fun_ord op \<le>) (fun_ord op \<le>) F"
   591     by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])
   592   let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
   593   have chain: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` ?iter)"
   594     by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def)
   595 
   596   {
   597     fix x y
   598     assume "x \<sqsubseteq> y"
   599     show "?fixp x \<le> ?fixp y"
   600       apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
   601       using chain
   602     proof(rule ccpo_Sup_least)
   603       fix x'
   604       assume "x' \<in> (\<lambda>f. f x) ` ?iter"
   605       then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
   606       also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y"
   607         by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]])
   608       also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
   609         by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
   610       finally show "x' \<le> \<dots>" .
   611     qed
   612   next
   613     fix Y
   614     assume chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
   615       and Y: "Y \<noteq> {}"
   616     { fix f
   617       assume "f \<in> ?iter"
   618       hence "f (\<Or>Y) = \<Squnion>(f ` Y)"
   619         using mcont chain Y by(rule mcont_contD[OF iterates_mcont]) }
   620     moreover have "\<Squnion>((\<lambda>f. \<Squnion>(f ` Y)) ` ?iter) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` ?iter)) ` Y)"
   621       using chain ccpo.chain_iterates[OF ccpo_fun mono]
   622       by(rule swap_Sup)(rule mcont_mono[OF iterates_mcont[OF _ mcont]])
   623     ultimately show "?fixp (\<Or>Y) = \<Squnion>(?fixp ` Y)" unfolding ccpo.fixp_def[OF ccpo_fun]
   624       by(simp add: fun_lub_apply cong: image_cong)
   625   }
   626 qed
   627 
   628 end
   629 
   630 context
   631   fixes F :: "'c \<Rightarrow> 'c" and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and f
   632   assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. U (F (C f)) x)"
   633   and eq: "f \<equiv> C (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) (\<lambda>f. U (F (C f))))"
   634   and inverse: "\<And>f. U (C f) = f"
   635 begin
   636 
   637 lemma fixp_preserves_mono_uc:
   638   assumes mono2: "\<And>f. monotone ord op \<le> (U f) \<Longrightarrow> monotone ord op \<le> (U (F f))"
   639   shows "monotone ord op \<le> (U f)"
   640 using fixp_preserves_mono[OF mono mono2] by(subst eq)(simp add: inverse)
   641 
   642 lemma fixp_preserves_mcont_uc:
   643   assumes mcont: "\<And>f. mcont lubb ordb Sup op \<le> (U f) \<Longrightarrow> mcont lubb ordb Sup op \<le> (U (F f))"
   644   shows "mcont lubb ordb Sup op \<le> (U f)"
   645 using fixp_preserves_mcont[OF mono mcont] by(subst eq)(simp add: inverse)
   646 
   647 end
   648 
   649 lemmas fixp_preserves_mono1 = fixp_preserves_mono_uc[of "\<lambda>x. x" _ "\<lambda>x. x", OF _ _ refl]
   650 lemmas fixp_preserves_mono2 =
   651   fixp_preserves_mono_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
   652 lemmas fixp_preserves_mono3 =
   653   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]
   654 lemmas fixp_preserves_mono4 =
   655   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]
   656 
   657 lemmas fixp_preserves_mcont1 = fixp_preserves_mcont_uc[of "\<lambda>x. x" _ "\<lambda>x. x", OF _ _ refl]
   658 lemmas fixp_preserves_mcont2 =
   659   fixp_preserves_mcont_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
   660 lemmas fixp_preserves_mcont3 =
   661   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]
   662 lemmas fixp_preserves_mcont4 =
   663   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]
   664 
   665 end
   666 
   667 lemma (in preorder) monotone_if_bot:
   668   fixes bot
   669   assumes mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> (x \<le> bound) \<rbrakk> \<Longrightarrow> ord (f x) (f y)"
   670   and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> ord bot (f x)" "ord bot bot"
   671   shows "monotone op \<le> ord (\<lambda>x. if x \<le> bound then bot else f x)"
   672 by(rule monotoneI)(auto intro: bot intro: mono order_trans)
   673 
   674 lemma (in ccpo) mcont_if_bot:
   675   fixes bot and lub ("\<Or>_" [900] 900) and ord (infix "\<sqsubseteq>" 60)
   676   assumes ccpo: "class.ccpo lub op \<sqsubseteq> lt"
   677   and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
   678   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)"
   679   and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> bot \<sqsubseteq> f x"
   680   shows "mcont Sup op \<le> lub op \<sqsubseteq> (\<lambda>x. if x \<le> bound then bot else f x)" (is "mcont _ _ _ _ ?g")
   681 proof(intro mcontI contI)
   682   interpret c: ccpo lub "op \<sqsubseteq>" lt by(fact ccpo)
   683   show "monotone op \<le> op \<sqsubseteq> ?g" by(rule monotone_if_bot)(simp_all add: mono bot)
   684 
   685   fix Y
   686   assume chain: "Complete_Partial_Order.chain op \<le> Y" and Y: "Y \<noteq> {}"
   687   show "?g (\<Squnion>Y) = \<Or>(?g ` Y)"
   688   proof(cases "Y \<subseteq> {x. x \<le> bound}")
   689     case True
   690     hence "\<Squnion>Y \<le> bound" using chain by(auto intro: ccpo_Sup_least)
   691     moreover have "Y \<inter> {x. \<not> x \<le> bound} = {}" using True by auto
   692     ultimately show ?thesis using True Y
   693       by (auto simp add: image_constant_conv cong del: c.strong_SUP_cong)
   694   next
   695     case False
   696     let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"
   697     have chain': "Complete_Partial_Order.chain op \<le> ?Y"
   698       using chain by(rule chain_subset) simp
   699 
   700     from False obtain y where ybound: "\<not> y \<le> bound" and y: "y \<in> Y" by blast
   701     hence "\<not> \<Squnion>Y \<le> bound" by (metis ccpo_Sup_upper chain order.trans)
   702     hence "?g (\<Squnion>Y) = f (\<Squnion>Y)" by simp
   703     also have "\<Squnion>Y \<le> \<Squnion>?Y" using chain
   704     proof(rule ccpo_Sup_least)
   705       fix x
   706       assume x: "x \<in> Y"
   707       show "x \<le> \<Squnion>?Y"
   708       proof(cases "x \<le> bound")
   709         case True
   710         with chainD[OF chain x y] have "x \<le> y" using ybound by(auto intro: order_trans)
   711         thus ?thesis by(rule order_trans)(auto intro: ccpo_Sup_upper[OF chain'] simp add: y ybound)
   712       qed(auto intro: ccpo_Sup_upper[OF chain'] simp add: x)
   713     qed
   714     hence "\<Squnion>Y = \<Squnion>?Y" by(rule antisym)(blast intro: ccpo_Sup_least[OF chain'] ccpo_Sup_upper[OF chain])
   715     hence "f (\<Squnion>Y) = f (\<Squnion>?Y)" by simp
   716     also have "f (\<Squnion>?Y) = \<Or>(f ` ?Y)" using chain' by(rule cont)(insert y ybound, auto)
   717     also have "\<Or>(f ` ?Y) = \<Or>(?g ` Y)"
   718     proof(cases "Y \<inter> {x. x \<le> bound} = {}")
   719       case True
   720       hence "f ` ?Y = ?g ` Y" by auto
   721       thus ?thesis by(rule arg_cong)
   722     next
   723       case False
   724       have chain'': "Complete_Partial_Order.chain op \<sqsubseteq> (insert bot (f ` ?Y))"
   725         using chain by(auto intro!: chainI bot dest: chainD intro: mono)
   726       hence chain''': "Complete_Partial_Order.chain op \<sqsubseteq> (f ` ?Y)" by(rule chain_subset) blast
   727       have "bot \<sqsubseteq> \<Or>(f ` ?Y)" using y ybound by(blast intro: c.order_trans[OF bot] c.ccpo_Sup_upper[OF chain'''])
   728       hence "\<Or>(insert bot (f ` ?Y)) \<sqsubseteq> \<Or>(f ` ?Y)" using chain''
   729         by(auto intro: c.ccpo_Sup_least c.ccpo_Sup_upper[OF chain''']) 
   730       with _ have "\<dots> = \<Or>(insert bot (f ` ?Y))"
   731         by(rule c.antisym)(blast intro: c.ccpo_Sup_least[OF chain'''] c.ccpo_Sup_upper[OF chain''])
   732       also have "insert bot (f ` ?Y) = ?g ` Y" using False by auto
   733       finally show ?thesis .
   734     qed
   735     finally show ?thesis .
   736   qed
   737 qed
   738 
   739 context partial_function_definitions begin
   740 
   741 lemma mcont_const [cont_intro, simp]:
   742   "mcont luba orda lub leq (\<lambda>x. c)"
   743 by(rule ccpo.mcont_const)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
   744 
   745 lemmas [cont_intro, simp] =
   746   ccpo.cont_const[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   747 
   748 lemma mono2mono:
   749   assumes "monotone ordb leq (\<lambda>y. f y)" "monotone orda ordb (\<lambda>x. t x)"
   750   shows "monotone orda leq (\<lambda>x. f (t x))"
   751 using assms by(rule monotone2monotone) simp_all
   752 
   753 lemmas mcont2mcont' = ccpo.mcont2mcont'[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   754 lemmas mcont2mcont = ccpo.mcont2mcont[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   755 
   756 lemmas fixp_preserves_mono1 = ccpo.fixp_preserves_mono1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   757 lemmas fixp_preserves_mono2 = ccpo.fixp_preserves_mono2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   758 lemmas fixp_preserves_mono3 = ccpo.fixp_preserves_mono3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   759 lemmas fixp_preserves_mono4 = ccpo.fixp_preserves_mono4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   760 lemmas fixp_preserves_mcont1 = ccpo.fixp_preserves_mcont1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   761 lemmas fixp_preserves_mcont2 = ccpo.fixp_preserves_mcont2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   762 lemmas fixp_preserves_mcont3 = ccpo.fixp_preserves_mcont3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   763 lemmas fixp_preserves_mcont4 = ccpo.fixp_preserves_mcont4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   764 
   765 lemma monotone_if_bot:
   766   fixes bot
   767   assumes g: "\<And>x. g x = (if leq x bound then bot else f x)"
   768   and mono: "\<And>x y. \<lbrakk> leq x y; \<not> leq x bound \<rbrakk> \<Longrightarrow> ord (f x) (f y)"
   769   and bot: "\<And>x. \<not> leq x bound \<Longrightarrow> ord bot (f x)" "ord bot bot"
   770   shows "monotone leq ord g"
   771 unfolding g[abs_def] using preorder mono bot by(rule preorder.monotone_if_bot)
   772 
   773 lemma mcont_if_bot:
   774   fixes bot
   775   assumes ccpo: "class.ccpo lub' ord (mk_less ord)"
   776   and bot: "\<And>x. \<not> leq x bound \<Longrightarrow> ord bot (f x)"
   777   and g: "\<And>x. g x = (if leq x bound then bot else f x)"
   778   and mono: "\<And>x y. \<lbrakk> leq x y; \<not> leq x bound \<rbrakk> \<Longrightarrow> ord (f x) (f y)"
   779   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)"
   780   shows "mcont lub leq lub' ord g"
   781 unfolding g[abs_def] using ccpo mono cont bot by(rule ccpo.mcont_if_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]])
   782 
   783 end
   784 
   785 subsection \<open>Admissibility\<close>
   786 
   787 lemma admissible_subst:
   788   assumes adm: "ccpo.admissible luba orda (\<lambda>x. P x)"
   789   and mcont: "mcont lubb ordb luba orda f"
   790   shows "ccpo.admissible lubb ordb (\<lambda>x. P (f x))"
   791 apply(rule ccpo.admissibleI)
   792 apply(frule (1) mcont_contD[OF mcont])
   793 apply(auto intro: ccpo.admissibleD[OF adm] chain_imageI dest: mcont_monoD[OF mcont])
   794 done
   795 
   796 lemmas [simp, cont_intro] = 
   797   admissible_all
   798   admissible_ball
   799   admissible_const
   800   admissible_conj
   801 
   802 lemma admissible_disj' [simp, cont_intro]:
   803   "\<lbrakk> class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord P; ccpo.admissible lub ord Q \<rbrakk>
   804   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<or> Q x)"
   805 by(rule ccpo.admissible_disj)
   806 
   807 lemma admissible_imp' [cont_intro]:
   808   "\<lbrakk> class.ccpo lub ord (mk_less ord);
   809      ccpo.admissible lub ord (\<lambda>x. \<not> P x);
   810      ccpo.admissible lub ord (\<lambda>x. Q x) \<rbrakk>
   811   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x)"
   812 unfolding imp_conv_disj by(rule ccpo.admissible_disj)
   813 
   814 lemma admissible_imp [cont_intro]:
   815   "(Q \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x))
   816   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. Q \<longrightarrow> P x)"
   817 by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD)
   818 
   819 lemma admissible_not_mem' [THEN admissible_subst, cont_intro, simp]:
   820   shows admissible_not_mem: "ccpo.admissible Union op \<subseteq> (\<lambda>A. x \<notin> A)"
   821 by(rule ccpo.admissibleI) auto
   822 
   823 lemma admissible_eqI:
   824   assumes f: "cont luba orda lub ord (\<lambda>x. f x)"
   825   and g: "cont luba orda lub ord (\<lambda>x. g x)"
   826   shows "ccpo.admissible luba orda (\<lambda>x. f x = g x)"
   827 apply(rule ccpo.admissibleI)
   828 apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong)
   829 done
   830 
   831 corollary admissible_eq_mcontI [cont_intro]:
   832   "\<lbrakk> mcont luba orda lub ord (\<lambda>x. f x); 
   833     mcont luba orda lub ord (\<lambda>x. g x) \<rbrakk>
   834   \<Longrightarrow> ccpo.admissible luba orda (\<lambda>x. f x = g x)"
   835 by(rule admissible_eqI)(auto simp add: mcont_def)
   836 
   837 lemma admissible_iff [cont_intro, simp]:
   838   "\<lbrakk> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x); ccpo.admissible lub ord (\<lambda>x. Q x \<longrightarrow> P x) \<rbrakk>
   839   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longleftrightarrow> Q x)"
   840 by(subst iff_conv_conj_imp)(rule admissible_conj)
   841 
   842 context ccpo begin
   843 
   844 lemma admissible_leI:
   845   assumes f: "mcont luba orda Sup op \<le> (\<lambda>x. f x)"
   846   and g: "mcont luba orda Sup op \<le> (\<lambda>x. g x)"
   847   shows "ccpo.admissible luba orda (\<lambda>x. f x \<le> g x)"
   848 proof(rule ccpo.admissibleI)
   849   fix A
   850   assume chain: "Complete_Partial_Order.chain orda A"
   851     and le: "\<forall>x\<in>A. f x \<le> g x"
   852     and False: "A \<noteq> {}"
   853   have "f (luba A) = \<Squnion>(f ` A)" by(simp add: mcont_contD[OF f] chain False)
   854   also have "\<dots> \<le> \<Squnion>(g ` A)"
   855   proof(rule ccpo_Sup_least)
   856     from chain show "Complete_Partial_Order.chain op \<le> (f ` A)"
   857       by(rule chain_imageI)(rule mcont_monoD[OF f])
   858     
   859     fix x
   860     assume "x \<in> f ` A"
   861     then obtain y where "y \<in> A" "x = f y" by blast note this(2)
   862     also have "f y \<le> g y" using le \<open>y \<in> A\<close> by simp
   863     also have "Complete_Partial_Order.chain op \<le> (g ` A)"
   864       using chain by(rule chain_imageI)(rule mcont_monoD[OF g])
   865     hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> A\<close>)
   866     finally show "x \<le> \<dots>" .
   867   qed
   868   also have "\<dots> = g (luba A)" by(simp add: mcont_contD[OF g] chain False)
   869   finally show "f (luba A) \<le> g (luba A)" .
   870 qed
   871 
   872 end
   873 
   874 lemma admissible_leI:
   875   fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or>_" [900] 900)
   876   assumes "class.ccpo lub op \<sqsubseteq> (mk_less op \<sqsubseteq>)"
   877   and "mcont luba orda lub op \<sqsubseteq> (\<lambda>x. f x)"
   878   and "mcont luba orda lub op \<sqsubseteq> (\<lambda>x. g x)"
   879   shows "ccpo.admissible luba orda (\<lambda>x. f x \<sqsubseteq> g x)"
   880 using assms by(rule ccpo.admissible_leI)
   881 
   882 declare ccpo_class.admissible_leI[cont_intro]
   883 
   884 context ccpo begin
   885 
   886 lemma admissible_not_below: "ccpo.admissible Sup op \<le> (\<lambda>x. \<not> op \<le> x y)"
   887 by(rule ccpo.admissibleI)(simp add: ccpo_Sup_below_iff)
   888 
   889 end
   890 
   891 lemma (in preorder) preorder [cont_intro, simp]: "class.preorder op \<le> (mk_less op \<le>)"
   892 by(unfold_locales)(auto simp add: mk_less_def intro: order_trans)
   893 
   894 context partial_function_definitions begin
   895 
   896 lemmas [cont_intro, simp] =
   897   admissible_leI[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   898   ccpo.admissible_not_below[THEN admissible_subst, OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   899 
   900 end
   901 
   902 
   903 inductive compact :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   904   for lub ord x 
   905 where compact:
   906   "\<lbrakk> ccpo.admissible lub ord (\<lambda>y. \<not> ord x y);
   907      ccpo.admissible lub ord (\<lambda>y. x \<noteq> y) \<rbrakk>
   908   \<Longrightarrow> compact lub ord x"
   909 
   910 hide_fact (open) compact
   911 
   912 context ccpo begin
   913 
   914 lemma compactI:
   915   assumes "ccpo.admissible Sup op \<le> (\<lambda>y. \<not> x \<le> y)"
   916   shows "compact Sup op \<le> x"
   917 using assms
   918 proof(rule compact.intros)
   919   have neq: "(\<lambda>y. x \<noteq> y) = (\<lambda>y. \<not> x \<le> y \<or> \<not> y \<le> x)" by(auto)
   920   show "ccpo.admissible Sup op \<le> (\<lambda>y. x \<noteq> y)"
   921     by(subst neq)(rule admissible_disj admissible_not_below assms)+
   922 qed
   923 
   924 lemma compact_bot:
   925   assumes "x = Sup {}"
   926   shows "compact Sup op \<le> x"
   927 proof(rule compactI)
   928   show "ccpo.admissible Sup op \<le> (\<lambda>y. \<not> x \<le> y)" using assms
   929     by(auto intro!: ccpo.admissibleI intro: ccpo_Sup_least chain_empty)
   930 qed
   931 
   932 end
   933 
   934 lemma admissible_compact_neq' [THEN admissible_subst, cont_intro, simp]:
   935   shows admissible_compact_neq: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. k \<noteq> x)"
   936 by(simp add: compact.simps)
   937 
   938 lemma admissible_neq_compact' [THEN admissible_subst, cont_intro, simp]:
   939   shows admissible_neq_compact: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. x \<noteq> k)"
   940 by(subst eq_commute)(rule admissible_compact_neq)
   941 
   942 context partial_function_definitions begin
   943 
   944 lemmas [cont_intro, simp] = ccpo.compact_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   945 
   946 end
   947 
   948 context ccpo begin
   949 
   950 lemma fixp_strong_induct:
   951   assumes [cont_intro]: "ccpo.admissible Sup op \<le> P"
   952   and mono: "monotone op \<le> op \<le> f"
   953   and bot: "P (\<Squnion>{})"
   954   and step: "\<And>x. \<lbrakk> x \<le> ccpo_class.fixp f; P x \<rbrakk> \<Longrightarrow> P (f x)"
   955   shows "P (ccpo_class.fixp f)"
   956 proof(rule fixp_induct[where P="\<lambda>x. x \<le> ccpo_class.fixp f \<and> P x", THEN conjunct2])
   957   note [cont_intro] = admissible_leI
   958   show "ccpo.admissible Sup op \<le> (\<lambda>x. x \<le> ccpo_class.fixp f \<and> P x)" by simp
   959 next
   960   show "\<Squnion>{} \<le> ccpo_class.fixp f \<and> P (\<Squnion>{})"
   961     by(auto simp add: bot intro: ccpo_Sup_least chain_empty)
   962 next
   963   fix x
   964   assume "x \<le> ccpo_class.fixp f \<and> P x"
   965   thus "f x \<le> ccpo_class.fixp f \<and> P (f x)"
   966     by(subst fixp_unfold[OF mono])(auto dest: monotoneD[OF mono] intro: step)
   967 qed(rule mono)
   968 
   969 end
   970 
   971 context partial_function_definitions begin
   972 
   973 lemma fixp_strong_induct_uc:
   974   fixes F :: "'c \<Rightarrow> 'c"
   975     and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a"
   976     and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
   977     and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
   978   assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
   979     and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
   980     and inverse: "\<And>f. U (C f) = f"
   981     and adm: "ccpo.admissible lub_fun le_fun P"
   982     and bot: "P (\<lambda>_. lub {})"
   983     and step: "\<And>f'. \<lbrakk> P (U f'); le_fun (U f') (U f) \<rbrakk> \<Longrightarrow> P (U (F f'))"
   984   shows "P (U f)"
   985 unfolding eq inverse
   986 apply (rule ccpo.fixp_strong_induct[OF ccpo adm])
   987 apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
   988 apply (rule_tac f'5="C x" in step)
   989 apply (simp_all add: inverse eq)
   990 done
   991 
   992 end
   993 
   994 subsection \<open>@{term "op ="} as order\<close>
   995 
   996 definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool"
   997 where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
   998 
   999 definition the_Sup :: "'a set \<Rightarrow> 'a"
  1000 where "the_Sup A = (THE a. a \<in> A)"
  1001 
  1002 lemma lub_singleton_the_Sup [cont_intro, simp]: "lub_singleton the_Sup"
  1003 by(simp add: lub_singleton_def the_Sup_def)
  1004 
  1005 lemma (in ccpo) lub_singleton: "lub_singleton Sup"
  1006 by(simp add: lub_singleton_def)
  1007 
  1008 lemma (in partial_function_definitions) lub_singleton [cont_intro, simp]: "lub_singleton lub"
  1009 by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
  1010 
  1011 lemma preorder_eq [cont_intro, simp]:
  1012   "class.preorder op = (mk_less op =)"
  1013 by(unfold_locales)(simp_all add: mk_less_def)
  1014 
  1015 lemma monotone_eqI [cont_intro]:
  1016   assumes "class.preorder ord (mk_less ord)"
  1017   shows "monotone op = ord f"
  1018 proof -
  1019   interpret preorder ord "mk_less ord" by fact
  1020   show ?thesis by(simp add: monotone_def)
  1021 qed
  1022 
  1023 lemma cont_eqI [cont_intro]: 
  1024   fixes f :: "'a \<Rightarrow> 'b"
  1025   assumes "lub_singleton lub"
  1026   shows "cont the_Sup op = lub ord f"
  1027 proof(rule contI)
  1028   fix Y :: "'a set"
  1029   assume "Complete_Partial_Order.chain op = Y" "Y \<noteq> {}"
  1030   then obtain a where "Y = {a}" by(auto simp add: chain_def)
  1031   thus "f (the_Sup Y) = lub (f ` Y)" using assms
  1032     by(simp add: the_Sup_def lub_singleton_def)
  1033 qed
  1034 
  1035 lemma mcont_eqI [cont_intro, simp]:
  1036   "\<lbrakk> class.preorder ord (mk_less ord); lub_singleton lub \<rbrakk>
  1037   \<Longrightarrow> mcont the_Sup op = lub ord f"
  1038 by(simp add: mcont_def cont_eqI monotone_eqI)
  1039 
  1040 subsection \<open>ccpo for products\<close>
  1041 
  1042 definition prod_lub :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b"
  1043 where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
  1044 
  1045 lemma lub_singleton_prod_lub [cont_intro, simp]:
  1046   "\<lbrakk> lub_singleton luba; lub_singleton lubb \<rbrakk> \<Longrightarrow> lub_singleton (prod_lub luba lubb)"
  1047 by(simp add: lub_singleton_def prod_lub_def)
  1048 
  1049 lemma prod_lub_empty [simp]: "prod_lub luba lubb {} = (luba {}, lubb {})"
  1050 by(simp add: prod_lub_def)
  1051 
  1052 lemma preorder_rel_prodI [cont_intro, simp]:
  1053   assumes "class.preorder orda (mk_less orda)"
  1054   and "class.preorder ordb (mk_less ordb)"
  1055   shows "class.preorder (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
  1056 proof -
  1057   interpret a: preorder orda "mk_less orda" by fact
  1058   interpret b: preorder ordb "mk_less ordb" by fact
  1059   show ?thesis by(unfold_locales)(auto simp add: mk_less_def intro: a.order_trans b.order_trans)
  1060 qed
  1061 
  1062 lemma order_rel_prodI:
  1063   assumes a: "class.order orda (mk_less orda)"
  1064   and b: "class.order ordb (mk_less ordb)"
  1065   shows "class.order (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
  1066   (is "class.order ?ord ?ord'")
  1067 proof(intro class.order.intro class.order_axioms.intro)
  1068   interpret a: order orda "mk_less orda" by(fact a)
  1069   interpret b: order ordb "mk_less ordb" by(fact b)
  1070   show "class.preorder ?ord ?ord'" by(rule preorder_rel_prodI) unfold_locales
  1071 
  1072   fix x y
  1073   assume "?ord x y" "?ord y x"
  1074   thus "x = y" by(cases x y rule: prod.exhaust[case_product prod.exhaust]) auto
  1075 qed
  1076 
  1077 lemma monotone_rel_prodI:
  1078   assumes mono2: "\<And>a. monotone ordb ordc (\<lambda>b. f (a, b))"
  1079   and mono1: "\<And>b. monotone orda ordc (\<lambda>a. f (a, b))"
  1080   and a: "class.preorder orda (mk_less orda)"
  1081   and b: "class.preorder ordb (mk_less ordb)"
  1082   and c: "class.preorder ordc (mk_less ordc)"
  1083   shows "monotone (rel_prod orda ordb) ordc f"
  1084 proof -
  1085   interpret a: preorder orda "mk_less orda" by(rule a)
  1086   interpret b: preorder ordb "mk_less ordb" by(rule b)
  1087   interpret c: preorder ordc "mk_less ordc" by(rule c)
  1088   show ?thesis using mono2 mono1
  1089     by(auto 7 2 simp add: monotone_def intro: c.order_trans)
  1090 qed
  1091 
  1092 lemma monotone_rel_prodD1:
  1093   assumes mono: "monotone (rel_prod orda ordb) ordc f"
  1094   and preorder: "class.preorder ordb (mk_less ordb)"
  1095   shows "monotone orda ordc (\<lambda>a. f (a, b))"
  1096 proof -
  1097   interpret preorder ordb "mk_less ordb" by(rule preorder)
  1098   show ?thesis using mono by(simp add: monotone_def)
  1099 qed
  1100 
  1101 lemma monotone_rel_prodD2:
  1102   assumes mono: "monotone (rel_prod orda ordb) ordc f"
  1103   and preorder: "class.preorder orda (mk_less orda)"
  1104   shows "monotone ordb ordc (\<lambda>b. f (a, b))"
  1105 proof -
  1106   interpret preorder orda "mk_less orda" by(rule preorder)
  1107   show ?thesis using mono by(simp add: monotone_def)
  1108 qed
  1109 
  1110 lemma monotone_case_prodI:
  1111   "\<lbrakk> \<And>a. monotone ordb ordc (f a); \<And>b. monotone orda ordc (\<lambda>a. f a b);
  1112     class.preorder orda (mk_less orda); class.preorder ordb (mk_less ordb);
  1113     class.preorder ordc (mk_less ordc) \<rbrakk>
  1114   \<Longrightarrow> monotone (rel_prod orda ordb) ordc (case_prod f)"
  1115 by(rule monotone_rel_prodI) simp_all
  1116 
  1117 lemma monotone_case_prodD1:
  1118   assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
  1119   and preorder: "class.preorder ordb (mk_less ordb)"
  1120   shows "monotone orda ordc (\<lambda>a. f a b)"
  1121 using monotone_rel_prodD1[OF assms] by simp
  1122 
  1123 lemma monotone_case_prodD2:
  1124   assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
  1125   and preorder: "class.preorder orda (mk_less orda)"
  1126   shows "monotone ordb ordc (f a)"
  1127 using monotone_rel_prodD2[OF assms] by simp
  1128 
  1129 context 
  1130   fixes orda ordb ordc
  1131   assumes a: "class.preorder orda (mk_less orda)"
  1132   and b: "class.preorder ordb (mk_less ordb)"
  1133   and c: "class.preorder ordc (mk_less ordc)"
  1134 begin
  1135 
  1136 lemma monotone_rel_prod_iff:
  1137   "monotone (rel_prod orda ordb) ordc f \<longleftrightarrow>
  1138    (\<forall>a. monotone ordb ordc (\<lambda>b. f (a, b))) \<and> 
  1139    (\<forall>b. monotone orda ordc (\<lambda>a. f (a, b)))"
  1140 using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2)
  1141 
  1142 lemma monotone_case_prod_iff [simp]:
  1143   "monotone (rel_prod orda ordb) ordc (case_prod f) \<longleftrightarrow>
  1144    (\<forall>a. monotone ordb ordc (f a)) \<and> (\<forall>b. monotone orda ordc (\<lambda>a. f a b))"
  1145 by(simp add: monotone_rel_prod_iff)
  1146 
  1147 end
  1148 
  1149 lemma monotone_case_prod_apply_iff:
  1150   "monotone orda ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
  1151 by(simp add: monotone_def)
  1152 
  1153 lemma monotone_case_prod_applyD:
  1154   "monotone orda ordb (\<lambda>x. (case_prod f x) y)
  1155   \<Longrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
  1156 by(simp add: monotone_case_prod_apply_iff)
  1157 
  1158 lemma monotone_case_prod_applyI:
  1159   "monotone orda ordb (case_prod (\<lambda>a b. f a b y))
  1160   \<Longrightarrow> monotone orda ordb (\<lambda>x. (case_prod f x) y)"
  1161 by(simp add: monotone_case_prod_apply_iff)
  1162 
  1163 
  1164 lemma cont_case_prod_apply_iff:
  1165   "cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
  1166 by(simp add: cont_def split_def)
  1167 
  1168 lemma cont_case_prod_applyI:
  1169   "cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))
  1170   \<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)"
  1171 by(simp add: cont_case_prod_apply_iff)
  1172 
  1173 lemma cont_case_prod_applyD:
  1174   "cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)
  1175   \<Longrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
  1176 by(simp add: cont_case_prod_apply_iff)
  1177 
  1178 lemma mcont_case_prod_apply_iff [simp]:
  1179   "mcont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> 
  1180    mcont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
  1181 by(simp add: mcont_def monotone_case_prod_apply_iff cont_case_prod_apply_iff)
  1182 
  1183 lemma cont_prodD1: 
  1184   assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f"
  1185   and "class.preorder orda (mk_less orda)"
  1186   and luba: "lub_singleton luba"
  1187   shows "cont lubb ordb lubc ordc (\<lambda>y. f (x, y))"
  1188 proof(rule contI)
  1189   interpret preorder orda "mk_less orda" by fact
  1190 
  1191   fix Y :: "'b set"
  1192   let ?Y = "{x} \<times> Y"
  1193   assume "Complete_Partial_Order.chain ordb Y" "Y \<noteq> {}"
  1194   hence "Complete_Partial_Order.chain (rel_prod orda ordb) ?Y" "?Y \<noteq> {}" 
  1195     by(simp_all add: chain_def)
  1196   with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
  1197   moreover have "f ` ?Y = (\<lambda>y. f (x, y)) ` Y" by auto
  1198   ultimately show "f (x, lubb Y) = lubc ((\<lambda>y. f (x, y)) ` Y)" using luba
  1199     by(simp add: prod_lub_def \<open>Y \<noteq> {}\<close> lub_singleton_def)
  1200 qed
  1201 
  1202 lemma cont_prodD2: 
  1203   assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f"
  1204   and "class.preorder ordb (mk_less ordb)"
  1205   and lubb: "lub_singleton lubb"
  1206   shows "cont luba orda lubc ordc (\<lambda>x. f (x, y))"
  1207 proof(rule contI)
  1208   interpret preorder ordb "mk_less ordb" by fact
  1209 
  1210   fix Y
  1211   assume Y: "Complete_Partial_Order.chain orda Y" "Y \<noteq> {}"
  1212   let ?Y = "Y \<times> {y}"
  1213   have "f (luba Y, y) = f (prod_lub luba lubb ?Y)"
  1214     using lubb by(simp add: prod_lub_def Y lub_singleton_def)
  1215   also from Y have "Complete_Partial_Order.chain (rel_prod orda ordb) ?Y" "?Y \<noteq> {}"
  1216     by(simp_all add: chain_def)
  1217   with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
  1218   also have "f ` ?Y = (\<lambda>x. f (x, y)) ` Y" by auto
  1219   finally show "f (luba Y, y) = lubc \<dots>" .
  1220 qed
  1221 
  1222 lemma cont_case_prodD1:
  1223   assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)"
  1224   and "class.preorder orda (mk_less orda)"
  1225   and "lub_singleton luba"
  1226   shows "cont lubb ordb lubc ordc (f x)"
  1227 using cont_prodD1[OF assms] by simp
  1228 
  1229 lemma cont_case_prodD2:
  1230   assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)"
  1231   and "class.preorder ordb (mk_less ordb)"
  1232   and "lub_singleton lubb"
  1233   shows "cont luba orda lubc ordc (\<lambda>x. f x y)"
  1234 using cont_prodD2[OF assms] by simp
  1235 
  1236 context ccpo begin
  1237 
  1238 lemma cont_prodI: 
  1239   assumes mono: "monotone (rel_prod orda ordb) op \<le> f"
  1240   and cont1: "\<And>x. cont lubb ordb Sup op \<le> (\<lambda>y. f (x, y))"
  1241   and cont2: "\<And>y. cont luba orda Sup op \<le> (\<lambda>x. f (x, y))"
  1242   and "class.preorder orda (mk_less orda)"
  1243   and "class.preorder ordb (mk_less ordb)"
  1244   shows "cont (prod_lub luba lubb) (rel_prod orda ordb) Sup op \<le> f"
  1245 proof(rule contI)
  1246   interpret a: preorder orda "mk_less orda" by fact 
  1247   interpret b: preorder ordb "mk_less ordb" by fact
  1248   
  1249   fix Y
  1250   assume chain: "Complete_Partial_Order.chain (rel_prod orda ordb) Y"
  1251     and "Y \<noteq> {}"
  1252   have "f (prod_lub luba lubb Y) = f (luba (fst ` Y), lubb (snd ` Y))"
  1253     by(simp add: prod_lub_def)
  1254   also from cont2 have "f (luba (fst ` Y), lubb (snd ` Y)) = \<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y)"
  1255     by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] \<open>Y \<noteq> {}\<close>)
  1256   also from cont1 have "\<And>x. f (x, lubb (snd ` Y)) = \<Squnion>((\<lambda>y. f (x, y)) ` snd ` Y)"
  1257     by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] \<open>Y \<noteq> {}\<close>)
  1258   hence "\<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y) = \<Squnion>((\<lambda>x. \<dots> x) ` fst ` Y)" by simp
  1259   also have "\<dots> = \<Squnion>((\<lambda>x. f (fst x, snd x)) ` Y)"
  1260     unfolding image_image split_def using chain
  1261     apply(rule diag_Sup)
  1262     using monotoneD[OF mono]
  1263     by(auto intro: monotoneI)
  1264   finally show "f (prod_lub luba lubb Y) = \<Squnion>(f ` Y)" by simp
  1265 qed
  1266 
  1267 lemma cont_case_prodI:
  1268   assumes "monotone (rel_prod orda ordb) op \<le> (case_prod f)"
  1269   and "\<And>x. cont lubb ordb Sup op \<le> (\<lambda>y. f x y)"
  1270   and "\<And>y. cont luba orda Sup op \<le> (\<lambda>x. f x y)"
  1271   and "class.preorder orda (mk_less orda)"
  1272   and "class.preorder ordb (mk_less ordb)"
  1273   shows "cont (prod_lub luba lubb) (rel_prod orda ordb) Sup op \<le> (case_prod f)"
  1274 by(rule cont_prodI)(simp_all add: assms)
  1275 
  1276 lemma cont_case_prod_iff:
  1277   "\<lbrakk> monotone (rel_prod orda ordb) op \<le> (case_prod f);
  1278      class.preorder orda (mk_less orda); lub_singleton luba;
  1279      class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
  1280   \<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) Sup op \<le> (case_prod f) \<longleftrightarrow>
  1281    (\<forall>x. cont lubb ordb Sup op \<le> (\<lambda>y. f x y)) \<and> (\<forall>y. cont luba orda Sup op \<le> (\<lambda>x. f x y))"
  1282 by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
  1283 
  1284 end
  1285 
  1286 context partial_function_definitions begin
  1287 
  1288 lemma mono2mono2:
  1289   assumes f: "monotone (rel_prod ordb ordc) leq (\<lambda>(x, y). f x y)"
  1290   and t: "monotone orda ordb (\<lambda>x. t x)"
  1291   and t': "monotone orda ordc (\<lambda>x. t' x)"
  1292   shows "monotone orda leq (\<lambda>x. f (t x) (t' x))"
  1293 proof(rule monotoneI)
  1294   fix x y
  1295   assume "orda x y"
  1296   hence "rel_prod ordb ordc (t x, t' x) (t y, t' y)"
  1297     using t t' by(auto dest: monotoneD)
  1298   from monotoneD[OF f this] show "leq (f (t x) (t' x)) (f (t y) (t' y))" by simp
  1299 qed
  1300 
  1301 lemma cont_case_prodI [cont_intro]:
  1302   "\<lbrakk> monotone (rel_prod orda ordb) leq (case_prod f);
  1303     \<And>x. cont lubb ordb lub leq (\<lambda>y. f x y);
  1304     \<And>y. cont luba orda lub leq (\<lambda>x. f x y);
  1305     class.preorder orda (mk_less orda);
  1306     class.preorder ordb (mk_less ordb) \<rbrakk>
  1307   \<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f)"
  1308 by(rule ccpo.cont_case_prodI)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
  1309 
  1310 lemma cont_case_prod_iff:
  1311   "\<lbrakk> monotone (rel_prod orda ordb) leq (case_prod f);
  1312      class.preorder orda (mk_less orda); lub_singleton luba;
  1313      class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
  1314   \<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
  1315    (\<forall>x. cont lubb ordb lub leq (\<lambda>y. f x y)) \<and> (\<forall>y. cont luba orda lub leq (\<lambda>x. f x y))"
  1316 by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
  1317 
  1318 lemma mcont_case_prod_iff [simp]:
  1319   "\<lbrakk> class.preorder orda (mk_less orda); lub_singleton luba;
  1320      class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
  1321   \<Longrightarrow> mcont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
  1322    (\<forall>x. mcont lubb ordb lub leq (\<lambda>y. f x y)) \<and> (\<forall>y. mcont luba orda lub leq (\<lambda>x. f x y))"
  1323 unfolding mcont_def by(auto simp add: cont_case_prod_iff)
  1324 
  1325 end
  1326 
  1327 lemma mono2mono_case_prod [cont_intro]:
  1328   assumes "\<And>x y. monotone orda ordb (\<lambda>f. pair f x y)"
  1329   shows "monotone orda ordb (\<lambda>f. case_prod (pair f) x)"
  1330 by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
  1331 
  1332 subsection \<open>Complete lattices as ccpo\<close>
  1333 
  1334 context complete_lattice begin
  1335 
  1336 lemma complete_lattice_ccpo: "class.ccpo Sup op \<le> op <"
  1337 by(unfold_locales)(fast intro: Sup_upper Sup_least)+
  1338 
  1339 lemma complete_lattice_ccpo': "class.ccpo Sup op \<le> (mk_less op \<le>)"
  1340 by(unfold_locales)(auto simp add: mk_less_def intro: Sup_upper Sup_least)
  1341 
  1342 lemma complete_lattice_partial_function_definitions: 
  1343   "partial_function_definitions op \<le> Sup"
  1344 by(unfold_locales)(auto intro: Sup_least Sup_upper)
  1345 
  1346 lemma complete_lattice_partial_function_definitions_dual:
  1347   "partial_function_definitions op \<ge> Inf"
  1348 by(unfold_locales)(auto intro: Inf_lower Inf_greatest)
  1349 
  1350 lemmas [cont_intro, simp] =
  1351   Partial_Function.ccpo[OF complete_lattice_partial_function_definitions]
  1352   Partial_Function.ccpo[OF complete_lattice_partial_function_definitions_dual]
  1353 
  1354 lemma mono2mono_inf:
  1355   assumes f: "monotone ord op \<le> (\<lambda>x. f x)" 
  1356   and g: "monotone ord op \<le> (\<lambda>x. g x)"
  1357   shows "monotone ord op \<le> (\<lambda>x. f x \<sqinter> g x)"
  1358 by(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] intro: le_infI1 le_infI2 intro!: monotoneI)
  1359 
  1360 lemma mcont_const [simp]: "mcont lub ord Sup op \<le> (\<lambda>_. c)"
  1361 by(rule ccpo.mcont_const[OF complete_lattice_ccpo])
  1362 
  1363 lemma mono2mono_sup:
  1364   assumes f: "monotone ord op \<le> (\<lambda>x. f x)"
  1365   and g: "monotone ord op \<le> (\<lambda>x. g x)"
  1366   shows "monotone ord op \<le> (\<lambda>x. f x \<squnion> g x)"
  1367 by(auto 4 3 intro!: monotoneI intro: sup.coboundedI1 sup.coboundedI2 dest: monotoneD[OF f] monotoneD[OF g])
  1368 
  1369 lemma Sup_image_sup: 
  1370   assumes "Y \<noteq> {}"
  1371   shows "\<Squnion>(op \<squnion> x ` Y) = x \<squnion> \<Squnion>Y"
  1372 proof(rule Sup_eqI)
  1373   fix y
  1374   assume "y \<in> op \<squnion> x ` Y"
  1375   then obtain z where "y = x \<squnion> z" and "z \<in> Y" by blast
  1376   from \<open>z \<in> Y\<close> have "z \<le> \<Squnion>Y" by(rule Sup_upper)
  1377   with _ show "y \<le> x \<squnion> \<Squnion>Y" unfolding \<open>y = x \<squnion> z\<close> by(rule sup_mono) simp
  1378 next
  1379   fix y
  1380   assume upper: "\<And>z. z \<in> op \<squnion> x ` Y \<Longrightarrow> z \<le> y"
  1381   show "x \<squnion> \<Squnion>Y \<le> y" unfolding Sup_insert[symmetric]
  1382   proof(rule Sup_least)
  1383     fix z
  1384     assume "z \<in> insert x Y"
  1385     from assms obtain z' where "z' \<in> Y" by blast
  1386     let ?z = "if z \<in> Y then x \<squnion> z else x \<squnion> z'"
  1387     have "z \<le> x \<squnion> ?z" using \<open>z' \<in> Y\<close> \<open>z \<in> insert x Y\<close> by auto
  1388     also have "\<dots> \<le> y" by(rule upper)(auto split: if_split_asm intro: \<open>z' \<in> Y\<close>)
  1389     finally show "z \<le> y" .
  1390   qed
  1391 qed
  1392 
  1393 lemma mcont_sup1: "mcont Sup op \<le> Sup op \<le> (\<lambda>y. x \<squnion> y)"
  1394 by(auto 4 3 simp add: mcont_def sup.coboundedI1 sup.coboundedI2 intro!: monotoneI contI intro: Sup_image_sup[symmetric])
  1395 
  1396 lemma mcont_sup2: "mcont Sup op \<le> Sup op \<le> (\<lambda>x. x \<squnion> y)"
  1397 by(subst sup_commute)(rule mcont_sup1)
  1398 
  1399 lemma mcont2mcont_sup [cont_intro, simp]:
  1400   "\<lbrakk> mcont lub ord Sup op \<le> (\<lambda>x. f x);
  1401      mcont lub ord Sup op \<le> (\<lambda>x. g x) \<rbrakk>
  1402   \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f x \<squnion> g x)"
  1403 by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_sup1 mcont_sup2 ccpo.mcont_const[OF complete_lattice_ccpo])
  1404 
  1405 end
  1406 
  1407 lemmas [cont_intro] = admissible_leI[OF complete_lattice_ccpo']
  1408 
  1409 context complete_distrib_lattice begin
  1410 
  1411 lemma mcont_inf1: "mcont Sup op \<le> Sup op \<le> (\<lambda>y. x \<sqinter> y)"
  1412 by(auto intro: monotoneI contI simp add: le_infI2 inf_Sup mcont_def)
  1413 
  1414 lemma mcont_inf2: "mcont Sup op \<le> Sup op \<le> (\<lambda>x. x \<sqinter> y)"
  1415 by(auto intro: monotoneI contI simp add: le_infI1 Sup_inf mcont_def)
  1416 
  1417 lemma mcont2mcont_inf [cont_intro, simp]:
  1418   "\<lbrakk> mcont lub ord Sup op \<le> (\<lambda>x. f x);
  1419     mcont lub ord Sup op \<le> (\<lambda>x. g x) \<rbrakk>
  1420   \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f x \<sqinter> g x)"
  1421 by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_inf1 mcont_inf2 ccpo.mcont_const[OF complete_lattice_ccpo])
  1422 
  1423 end
  1424 
  1425 interpretation lfp: partial_function_definitions "op \<le> :: _ :: complete_lattice \<Rightarrow> _" Sup
  1426 by(rule complete_lattice_partial_function_definitions)
  1427 
  1428 declaration \<open>Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body}
  1429   @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE\<close>
  1430 
  1431 interpretation gfp: partial_function_definitions "op \<ge> :: _ :: complete_lattice \<Rightarrow> _" Inf
  1432 by(rule complete_lattice_partial_function_definitions_dual)
  1433 
  1434 declaration \<open>Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body}
  1435   @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE\<close>
  1436 
  1437 lemma insert_mono [partial_function_mono]:
  1438    "monotone (fun_ord op \<subseteq>) op \<subseteq> A \<Longrightarrow> monotone (fun_ord op \<subseteq>) op \<subseteq> (\<lambda>y. insert x (A y))"
  1439 by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
  1440 
  1441 lemma mono2mono_insert [THEN lfp.mono2mono, cont_intro, simp]:
  1442   shows monotone_insert: "monotone op \<subseteq> op \<subseteq> (insert x)"
  1443 by(rule monotoneI) blast
  1444 
  1445 lemma mcont2mcont_insert[THEN lfp.mcont2mcont, cont_intro, simp]:
  1446   shows mcont_insert: "mcont Union op \<subseteq> Union op \<subseteq> (insert x)"
  1447 by(blast intro: mcontI contI monotone_insert)
  1448 
  1449 lemma mono2mono_image [THEN lfp.mono2mono, cont_intro, simp]:
  1450   shows monotone_image: "monotone op \<subseteq> op \<subseteq> (op ` f)"
  1451 by(rule monotoneI) blast
  1452 
  1453 lemma cont_image: "cont Union op \<subseteq> Union op \<subseteq> (op ` f)"
  1454 by(rule contI)(auto)
  1455 
  1456 lemma mcont2mcont_image [THEN lfp.mcont2mcont, cont_intro, simp]:
  1457   shows mcont_image: "mcont Union op \<subseteq> Union op \<subseteq> (op ` f)"
  1458 by(blast intro: mcontI monotone_image cont_image)
  1459 
  1460 context complete_lattice begin
  1461 
  1462 lemma monotone_Sup [cont_intro, simp]:
  1463   "monotone ord op \<subseteq> f \<Longrightarrow> monotone ord op \<le> (\<lambda>x. \<Squnion>f x)"
  1464 by(blast intro: monotoneI Sup_least Sup_upper dest: monotoneD)
  1465 
  1466 lemma cont_Sup:
  1467   assumes "cont lub ord Union op \<subseteq> f"
  1468   shows "cont lub ord Sup op \<le> (\<lambda>x. \<Squnion>f x)"
  1469 apply(rule contI)
  1470 apply(simp add: contD[OF assms])
  1471 apply(blast intro: Sup_least Sup_upper order_trans antisym)
  1472 done
  1473 
  1474 lemma mcont_Sup: "mcont lub ord Union op \<subseteq> f \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. \<Squnion>f x)"
  1475 unfolding mcont_def by(blast intro: monotone_Sup cont_Sup)
  1476 
  1477 lemma monotone_SUP:
  1478   "\<lbrakk> monotone ord op \<subseteq> f; \<And>y. monotone ord op \<le> (\<lambda>x. g x y) \<rbrakk> \<Longrightarrow> monotone ord op \<le> (\<lambda>x. \<Squnion>y\<in>f x. g x y)"
  1479 by(rule monotoneI)(blast dest: monotoneD intro: Sup_upper order_trans intro!: Sup_least)
  1480 
  1481 lemma monotone_SUP2:
  1482   "(\<And>y. y \<in> A \<Longrightarrow> monotone ord op \<le> (\<lambda>x. g x y)) \<Longrightarrow> monotone ord op \<le> (\<lambda>x. \<Squnion>y\<in>A. g x y)"
  1483 by(rule monotoneI)(blast intro: Sup_upper order_trans dest: monotoneD intro!: Sup_least)
  1484 
  1485 lemma cont_SUP:
  1486   assumes f: "mcont lub ord Union op \<subseteq> f"
  1487   and g: "\<And>y. mcont lub ord Sup op \<le> (\<lambda>x. g x y)"
  1488   shows "cont lub ord Sup op \<le> (\<lambda>x. \<Squnion>y\<in>f x. g x y)"
  1489 proof(rule contI)
  1490   fix Y
  1491   assume chain: "Complete_Partial_Order.chain ord Y"
  1492     and Y: "Y \<noteq> {}"
  1493   show "\<Squnion>(g (lub Y) ` f (lub Y)) = \<Squnion>((\<lambda>x. \<Squnion>(g x ` f x)) ` Y)" (is "?lhs = ?rhs")
  1494   proof(rule antisym)
  1495     show "?lhs \<le> ?rhs"
  1496     proof(rule Sup_least)
  1497       fix x
  1498       assume "x \<in> g (lub Y) ` f (lub Y)"
  1499       with mcont_contD[OF f chain Y] mcont_contD[OF g chain Y]
  1500       obtain y z where "y \<in> Y" "z \<in> f y"
  1501         and x: "x = \<Squnion>((\<lambda>x. g x z) ` Y)" by auto
  1502       show "x \<le> ?rhs" unfolding x
  1503       proof(rule Sup_least)
  1504         fix u
  1505         assume "u \<in> (\<lambda>x. g x z) ` Y"
  1506         then obtain y' where "u = g y' z" "y' \<in> Y" by auto
  1507         from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "ord y y' \<or> ord y' y" by(rule chainD)
  1508         thus "u \<le> ?rhs"
  1509         proof
  1510           note \<open>u = g y' z\<close> also
  1511           assume "ord y y'"
  1512           with f have "f y \<subseteq> f y'" by(rule mcont_monoD)
  1513           with \<open>z \<in> f y\<close>
  1514           have "g y' z \<le> \<Squnion>(g y' ` f y')" by(auto intro: Sup_upper)
  1515           also have "\<dots> \<le> ?rhs" using \<open>y' \<in> Y\<close> by(auto intro: Sup_upper)
  1516           finally show ?thesis .
  1517         next
  1518           note \<open>u = g y' z\<close> also
  1519           assume "ord y' y"
  1520           with g have "g y' z \<le> g y z" by(rule mcont_monoD)
  1521           also have "\<dots> \<le> \<Squnion>(g y ` f y)" using \<open>z \<in> f y\<close>
  1522             by(auto intro: Sup_upper)
  1523           also have "\<dots> \<le> ?rhs" using \<open>y \<in> Y\<close> by(auto intro: Sup_upper)
  1524           finally show ?thesis .
  1525         qed
  1526       qed
  1527     qed
  1528   next
  1529     show "?rhs \<le> ?lhs"
  1530     proof(rule Sup_least)
  1531       fix x
  1532       assume "x \<in> (\<lambda>x. \<Squnion>(g x ` f x)) ` Y"
  1533       then obtain y where x: "x = \<Squnion>(g y ` f y)" and "y \<in> Y" by auto
  1534       show "x \<le> ?lhs" unfolding x
  1535       proof(rule Sup_least)
  1536         fix u
  1537         assume "u \<in> g y ` f y"
  1538         then obtain z where "u = g y z" "z \<in> f y" by auto
  1539         note \<open>u = g y z\<close>
  1540         also have "g y z \<le> \<Squnion>((\<lambda>x. g x z) ` Y)"
  1541           using \<open>y \<in> Y\<close> by(auto intro: Sup_upper)
  1542         also have "\<dots> = g (lub Y) z" by(simp add: mcont_contD[OF g chain Y])
  1543         also have "\<dots> \<le> ?lhs" using \<open>z \<in> f y\<close> \<open>y \<in> Y\<close>
  1544           by(auto intro: Sup_upper simp add: mcont_contD[OF f chain Y])
  1545         finally show "u \<le> ?lhs" .
  1546       qed
  1547     qed
  1548   qed
  1549 qed
  1550 
  1551 lemma mcont_SUP [cont_intro, simp]:
  1552   "\<lbrakk> mcont lub ord Union op \<subseteq> f; \<And>y. mcont lub ord Sup op \<le> (\<lambda>x. g x y) \<rbrakk>
  1553   \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. \<Squnion>y\<in>f x. g x y)"
  1554 by(blast intro: mcontI cont_SUP monotone_SUP mcont_mono)
  1555 
  1556 end
  1557 
  1558 lemma admissible_Ball [cont_intro, simp]:
  1559   "\<lbrakk> \<And>x. ccpo.admissible lub ord (\<lambda>A. P A x);
  1560      mcont lub ord Union op \<subseteq> f;
  1561      class.ccpo lub ord (mk_less ord) \<rbrakk>
  1562   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>A. \<forall>x\<in>f A. P A x)"
  1563 unfolding Ball_def by simp
  1564 
  1565 lemma admissible_Bex'[THEN admissible_subst, cont_intro, simp]:
  1566   shows admissible_Bex: "ccpo.admissible Union op \<subseteq> (\<lambda>A. \<exists>x\<in>A. P x)"
  1567 by(rule ccpo.admissibleI)(auto)
  1568 
  1569 subsection \<open>Parallel fixpoint induction\<close>
  1570 
  1571 context
  1572   fixes luba :: "'a set \<Rightarrow> 'a"
  1573   and orda :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  1574   and lubb :: "'b set \<Rightarrow> 'b"
  1575   and ordb :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
  1576   assumes a: "class.ccpo luba orda (mk_less orda)"
  1577   and b: "class.ccpo lubb ordb (mk_less ordb)"
  1578 begin
  1579 
  1580 interpretation a: ccpo luba orda "mk_less orda" by(rule a)
  1581 interpretation b: ccpo lubb ordb "mk_less ordb" by(rule b)
  1582 
  1583 lemma ccpo_rel_prodI:
  1584   "class.ccpo (prod_lub luba lubb) (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
  1585   (is "class.ccpo ?lub ?ord ?ord'")
  1586 proof(intro class.ccpo.intro class.ccpo_axioms.intro)
  1587   show "class.order ?ord ?ord'" by(rule order_rel_prodI) intro_locales
  1588 qed(auto 4 4 simp add: prod_lub_def intro: a.ccpo_Sup_upper b.ccpo_Sup_upper a.ccpo_Sup_least b.ccpo_Sup_least rev_image_eqI dest: chain_rel_prodD1 chain_rel_prodD2)
  1589 
  1590 interpretation ab: ccpo "prod_lub luba lubb" "rel_prod orda ordb" "mk_less (rel_prod orda ordb)"
  1591 by(rule ccpo_rel_prodI)
  1592 
  1593 lemma monotone_map_prod [simp]:
  1594   "monotone (rel_prod orda ordb) (rel_prod ordc ordd) (map_prod f g) \<longleftrightarrow>
  1595    monotone orda ordc f \<and> monotone ordb ordd g"
  1596 by(auto simp add: monotone_def)
  1597 
  1598 lemma parallel_fixp_induct:
  1599   assumes adm: "ccpo.admissible (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. P (fst x) (snd x))"
  1600   and f: "monotone orda orda f"
  1601   and g: "monotone ordb ordb g"
  1602   and bot: "P (luba {}) (lubb {})"
  1603   and step: "\<And>x y. P x y \<Longrightarrow> P (f x) (g y)"
  1604   shows "P (ccpo.fixp luba orda f) (ccpo.fixp lubb ordb g)"
  1605 proof -
  1606   let ?lub = "prod_lub luba lubb"
  1607     and ?ord = "rel_prod orda ordb"
  1608     and ?P = "\<lambda>(x, y). P x y"
  1609   from adm have adm': "ccpo.admissible ?lub ?ord ?P" by(simp add: split_def)
  1610   hence "?P (ccpo.fixp (prod_lub luba lubb) (rel_prod orda ordb) (map_prod f g))"
  1611     by(rule ab.fixp_induct)(auto simp add: f g step bot)
  1612   also have "ccpo.fixp (prod_lub luba lubb) (rel_prod orda ordb) (map_prod f g) = 
  1613             (ccpo.fixp luba orda f, ccpo.fixp lubb ordb g)" (is "?lhs = (?rhs1, ?rhs2)")
  1614   proof(rule ab.antisym)
  1615     have "ccpo.admissible ?lub ?ord (\<lambda>xy. ?ord xy (?rhs1, ?rhs2))"
  1616       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)
  1617     thus "?ord ?lhs (?rhs1, ?rhs2)"
  1618       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)
  1619   next
  1620     have "ccpo.admissible luba orda (\<lambda>x. orda x (fst ?lhs))"
  1621       by(rule admissible_leI[OF a])(auto intro: a.ccpo_Sup_least simp add: chain_empty)
  1622     hence "orda ?rhs1 (fst ?lhs)" using f
  1623     proof(rule a.fixp_induct)
  1624       fix x
  1625       assume "orda x (fst ?lhs)"
  1626       thus "orda (f x) (fst ?lhs)"
  1627         by(subst ab.fixp_unfold)(auto simp add: f g dest: monotoneD[OF f])
  1628     qed(auto intro: a.ccpo_Sup_least chain_empty)
  1629     moreover
  1630     have "ccpo.admissible lubb ordb (\<lambda>y. ordb y (snd ?lhs))"
  1631       by(rule admissible_leI[OF b])(auto intro: b.ccpo_Sup_least simp add: chain_empty)
  1632     hence "ordb ?rhs2 (snd ?lhs)" using g
  1633     proof(rule b.fixp_induct)
  1634       fix y
  1635       assume "ordb y (snd ?lhs)"
  1636       thus "ordb (g y) (snd ?lhs)"
  1637         by(subst ab.fixp_unfold)(auto simp add: f g dest: monotoneD[OF g])
  1638     qed(auto intro: b.ccpo_Sup_least chain_empty)
  1639     ultimately show "?ord (?rhs1, ?rhs2) ?lhs"
  1640       by(simp add: rel_prod_conv split_beta)
  1641   qed
  1642   finally show ?thesis by simp
  1643 qed
  1644 
  1645 end
  1646 
  1647 lemma parallel_fixp_induct_uc:
  1648   assumes a: "partial_function_definitions orda luba"
  1649   and b: "partial_function_definitions ordb lubb"
  1650   and F: "\<And>x. monotone (fun_ord orda) orda (\<lambda>f. U1 (F (C1 f)) x)"
  1651   and G: "\<And>y. monotone (fun_ord ordb) ordb (\<lambda>g. U2 (G (C2 g)) y)"
  1652   and eq1: "f \<equiv> C1 (ccpo.fixp (fun_lub luba) (fun_ord orda) (\<lambda>f. U1 (F (C1 f))))"
  1653   and eq2: "g \<equiv> C2 (ccpo.fixp (fun_lub lubb) (fun_ord ordb) (\<lambda>g. U2 (G (C2 g))))"
  1654   and inverse: "\<And>f. U1 (C1 f) = f"
  1655   and inverse2: "\<And>g. U2 (C2 g) = g"
  1656   and adm: "ccpo.admissible (prod_lub (fun_lub luba) (fun_lub lubb)) (rel_prod (fun_ord orda) (fun_ord ordb)) (\<lambda>x. P (fst x) (snd x))"
  1657   and bot: "P (\<lambda>_. luba {}) (\<lambda>_. lubb {})"
  1658   and step: "\<And>f g. P (U1 f) (U2 g) \<Longrightarrow> P (U1 (F f)) (U2 (G g))"
  1659   shows "P (U1 f) (U2 g)"
  1660 apply(unfold eq1 eq2 inverse inverse2)
  1661 apply(rule parallel_fixp_induct[OF partial_function_definitions.ccpo[OF a] partial_function_definitions.ccpo[OF b] adm])
  1662 using F apply(simp add: monotone_def fun_ord_def)
  1663 using G apply(simp add: monotone_def fun_ord_def)
  1664 apply(simp add: fun_lub_def bot)
  1665 apply(rule step, simp add: inverse inverse2)
  1666 done
  1667 
  1668 lemmas parallel_fixp_induct_1_1 = parallel_fixp_induct_uc[
  1669   of _ _ _ _ "\<lambda>x. x" _ "\<lambda>x. x" "\<lambda>x. x" _ "\<lambda>x. x",
  1670   OF _ _ _ _ _ _ refl refl]
  1671 
  1672 lemmas parallel_fixp_induct_2_2 = parallel_fixp_induct_uc[
  1673   of _ _ _ _ "case_prod" _ "curry" "case_prod" _ "curry",
  1674   where P="\<lambda>f g. P (curry f) (curry g)",
  1675   unfolded case_prod_curry curry_case_prod curry_K,
  1676   OF _ _ _ _ _ _ refl refl]
  1677   for P
  1678 
  1679 lemma monotone_fst: "monotone (rel_prod orda ordb) orda fst"
  1680 by(auto intro: monotoneI)
  1681 
  1682 lemma mcont_fst: "mcont (prod_lub luba lubb) (rel_prod orda ordb) luba orda fst"
  1683 by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
  1684 
  1685 lemma mcont2mcont_fst [cont_intro, simp]:
  1686   "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
  1687   \<Longrightarrow> mcont lub ord luba orda (\<lambda>x. fst (t x))"
  1688 by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
  1689 
  1690 lemma monotone_snd: "monotone (rel_prod orda ordb) ordb snd"
  1691 by(auto intro: monotoneI)
  1692 
  1693 lemma mcont_snd: "mcont (prod_lub luba lubb) (rel_prod orda ordb) lubb ordb snd"
  1694 by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
  1695 
  1696 lemma mcont2mcont_snd [cont_intro, simp]:
  1697   "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
  1698   \<Longrightarrow> mcont lub ord lubb ordb (\<lambda>x. snd (t x))"
  1699 by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
  1700 
  1701 lemma monotone_Pair:
  1702   "\<lbrakk> monotone ord orda f; monotone ord ordb g \<rbrakk>
  1703   \<Longrightarrow> monotone ord (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
  1704 by(simp add: monotone_def)
  1705 
  1706 lemma cont_Pair:
  1707   "\<lbrakk> cont lub ord luba orda f; cont lub ord lubb ordb g \<rbrakk>
  1708   \<Longrightarrow> cont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
  1709 by(rule contI)(auto simp add: prod_lub_def image_image dest!: contD)
  1710 
  1711 lemma mcont_Pair:
  1712   "\<lbrakk> mcont lub ord luba orda f; mcont lub ord lubb ordb g \<rbrakk>
  1713   \<Longrightarrow> mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
  1714 by(rule mcontI)(simp_all add: monotone_Pair mcont_mono cont_Pair)
  1715 
  1716 context partial_function_definitions begin
  1717 text \<open>Specialised versions of @{thm [source] mcont_call} for admissibility proofs for parallel fixpoint inductions\<close>
  1718 lemmas mcont_call_fst [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_fst]
  1719 lemmas mcont_call_snd [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_snd]
  1720 end
  1721 
  1722 lemma map_option_mono [partial_function_mono]:
  1723   "mono_option B \<Longrightarrow> mono_option (\<lambda>f. map_option g (B f))"
  1724 unfolding map_conv_bind_option by(rule bind_mono) simp_all
  1725 
  1726 lemma compact_flat_lub [cont_intro]: "compact (flat_lub x) (flat_ord x) y"
  1727 using flat_interpretation[THEN ccpo]
  1728 proof(rule ccpo.compactI[OF _ ccpo.admissibleI])
  1729   fix A
  1730   assume chain: "Complete_Partial_Order.chain (flat_ord x) A"
  1731     and A: "A \<noteq> {}"
  1732     and *: "\<forall>z\<in>A. \<not> flat_ord x y z"
  1733   from A obtain z where "z \<in> A" by blast
  1734   with * have z: "\<not> flat_ord x y z" ..
  1735   hence y: "x \<noteq> y" "y \<noteq> z" by(auto simp add: flat_ord_def)
  1736   { assume "\<not> A \<subseteq> {x}"
  1737     then obtain z' where "z' \<in> A" "z' \<noteq> x" by auto
  1738     then have "(THE z. z \<in> A - {x}) = z'"
  1739       by(intro the_equality)(auto dest: chainD[OF chain] simp add: flat_ord_def)
  1740     moreover have "z' \<noteq> y" using \<open>z' \<in> A\<close> * by(auto simp add: flat_ord_def)
  1741     ultimately have "y \<noteq> (THE z. z \<in> A - {x})" by simp }
  1742   with z show "\<not> flat_ord x y (flat_lub x A)" by(simp add: flat_ord_def flat_lub_def)
  1743 qed
  1744 
  1745 end