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