move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
authorAndreas Lochbihler
Fri Mar 18 08:01:49 2016 +0100 (2016-03-18)
changeset 626527248d106c607
parent 62648 ee48e0b4f669
child 62653 d3a5b127eb81
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
CONTRIBUTORS
NEWS
src/HOL/Library/Complete_Partial_Order2.thy
src/HOL/Library/Library.thy
     1.1 --- a/CONTRIBUTORS	Thu Mar 17 14:48:14 2016 +0100
     1.2 +++ b/CONTRIBUTORS	Fri Mar 18 08:01:49 2016 +0100
     1.3 @@ -13,6 +13,9 @@
     1.4  * March 2016: Florian Haftmann
     1.5    Abstract factorial rings with unique factorization.
     1.6  
     1.7 +* March 2016: Andreas Lochbihler
     1.8 +  Reasoning support for monotonicity, continuity and
     1.9 +  admissibility in chain-complete partial orders.
    1.10  
    1.11  Contributions to Isabelle2016
    1.12  -----------------------------
     2.1 --- a/NEWS	Thu Mar 17 14:48:14 2016 +0100
     2.2 +++ b/NEWS	Fri Mar 18 08:01:49 2016 +0100
     2.3 @@ -113,6 +113,10 @@
     2.4  
     2.5  * Added topological_monoid
     2.6  
     2.7 +* Library/Complete_Partial_Order2.thy provides reasoning support for
     2.8 +proofs about monotonicity and continuity in chain-complete partial
     2.9 +orders and about admissibility conditions for fixpoint inductions.
    2.10 +
    2.11  * Library/Polynomial.thy contains also derivation of polynomials
    2.12  but not gcd/lcm on polynomials over fields.  This has been moved
    2.13  to a separate theory Library/Polynomial_GCD_euclidean.thy, to
    2.14 @@ -1092,9 +1096,9 @@
    2.15  performance.
    2.16  
    2.17  * Property values in etc/symbols may contain spaces, if written with the
    2.18 -replacement character "␣" (Unicode point 0x2324). For example:
    2.19 -
    2.20 -    \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
    2.21 +replacement character "?" (Unicode point 0x2324). For example:
    2.22 +
    2.23 +    \<star>  code: 0x0022c6  group: operator  font: Deja?Vu?Sans?Mono
    2.24  
    2.25  * Java runtime environment for x86_64-windows allows to use larger heap
    2.26  space.
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Complete_Partial_Order2.thy	Fri Mar 18 08:01:49 2016 +0100
     3.3 @@ -0,0 +1,1708 @@
     3.4 +(*  Title:      src/HOL/Library/Complete_Partial_Order2
     3.5 +    Author:     Andreas Lochbihler, ETH Zurich
     3.6 +*)
     3.7 +
     3.8 +section {* Formalisation of chain-complete partial orders, continuity and admissibility *}
     3.9 +
    3.10 +theory Complete_Partial_Order2 imports 
    3.11 +  Main
    3.12 +  "~~/src/HOL/Library/Lattice_Syntax"
    3.13 +begin
    3.14 +
    3.15 +context begin interpretation lifting_syntax .
    3.16 +
    3.17 +lemma chain_transfer [transfer_rule]:
    3.18 +  "((A ===> A ===> op =) ===> rel_set A ===> op =) Complete_Partial_Order.chain Complete_Partial_Order.chain"
    3.19 +unfolding chain_def[abs_def] by transfer_prover
    3.20 +
    3.21 +end
    3.22 +
    3.23 +lemma linorder_chain [simp, intro!]:
    3.24 +  fixes Y :: "_ :: linorder set"
    3.25 +  shows "Complete_Partial_Order.chain op \<le> Y"
    3.26 +by(auto intro: chainI)
    3.27 +
    3.28 +lemma fun_lub_apply: "\<And>Sup. fun_lub Sup Y x = Sup ((\<lambda>f. f x) ` Y)"
    3.29 +by(simp add: fun_lub_def image_def)
    3.30 +
    3.31 +lemma fun_lub_empty [simp]: "fun_lub lub {} = (\<lambda>_. lub {})"
    3.32 +by(rule ext)(simp add: fun_lub_apply)
    3.33 +
    3.34 +lemma chain_fun_ordD: 
    3.35 +  assumes "Complete_Partial_Order.chain (fun_ord le) Y"
    3.36 +  shows "Complete_Partial_Order.chain le ((\<lambda>f. f x) ` Y)"
    3.37 +by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def)
    3.38 +
    3.39 +lemma chain_Diff:
    3.40 +  "Complete_Partial_Order.chain ord A
    3.41 +  \<Longrightarrow> Complete_Partial_Order.chain ord (A - B)"
    3.42 +by(erule chain_subset) blast
    3.43 +
    3.44 +lemma chain_rel_prodD1:
    3.45 +  "Complete_Partial_Order.chain (rel_prod orda ordb) Y
    3.46 +  \<Longrightarrow> Complete_Partial_Order.chain orda (fst ` Y)"
    3.47 +by(auto 4 3 simp add: chain_def)
    3.48 +
    3.49 +lemma chain_rel_prodD2:
    3.50 +  "Complete_Partial_Order.chain (rel_prod orda ordb) Y
    3.51 +  \<Longrightarrow> Complete_Partial_Order.chain ordb (snd ` Y)"
    3.52 +by(auto 4 3 simp add: chain_def)
    3.53 +
    3.54 +
    3.55 +context ccpo begin
    3.56 +
    3.57 +lemma ccpo_fun: "class.ccpo (fun_lub Sup) (fun_ord op \<le>) (mk_less (fun_ord op \<le>))"
    3.58 +  by standard (auto 4 3 simp add: mk_less_def fun_ord_def fun_lub_apply
    3.59 +    intro: order.trans antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
    3.60 +
    3.61 +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)"
    3.62 +by(fast intro: order_trans[OF ccpo_Sup_upper] ccpo_Sup_least)
    3.63 +
    3.64 +lemma Sup_minus_bot: 
    3.65 +  assumes chain: "Complete_Partial_Order.chain op \<le> A"
    3.66 +  shows "\<Squnion>(A - {\<Squnion>{}}) = \<Squnion>A"
    3.67 +apply(rule antisym)
    3.68 + apply(blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])
    3.69 +apply(rule ccpo_Sup_least[OF chain])
    3.70 +apply(case_tac "x = \<Squnion>{}")
    3.71 +by(blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+
    3.72 +
    3.73 +lemma mono_lub:
    3.74 +  fixes le_b (infix "\<sqsubseteq>" 60)
    3.75 +  assumes chain: "Complete_Partial_Order.chain (fun_ord op \<le>) Y"
    3.76 +  and mono: "\<And>f. f \<in> Y \<Longrightarrow> monotone le_b op \<le> f"
    3.77 +  shows "monotone op \<sqsubseteq> op \<le> (fun_lub Sup Y)"
    3.78 +proof(rule monotoneI)
    3.79 +  fix x y
    3.80 +  assume "x \<sqsubseteq> y"
    3.81 +
    3.82 +  have chain'': "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` Y)"
    3.83 +    using chain by(rule chain_imageI)(simp add: fun_ord_def)
    3.84 +  then show "fun_lub Sup Y x \<le> fun_lub Sup Y y" unfolding fun_lub_apply
    3.85 +  proof(rule ccpo_Sup_least)
    3.86 +    fix x'
    3.87 +    assume "x' \<in> (\<lambda>f. f x) ` Y"
    3.88 +    then obtain f where "f \<in> Y" "x' = f x" by blast
    3.89 +    note `x' = f x` also
    3.90 +    from `f \<in> Y` `x \<sqsubseteq> y` have "f x \<le> f y" by(blast dest: mono monotoneD)
    3.91 +    also have "\<dots> \<le> \<Squnion>((\<lambda>f. f y) ` Y)" using chain''
    3.92 +      by(rule ccpo_Sup_upper)(simp add: `f \<in> Y`)
    3.93 +    finally show "x' \<le> \<Squnion>((\<lambda>f. f y) ` Y)" .
    3.94 +  qed
    3.95 +qed
    3.96 +
    3.97 +context
    3.98 +  fixes le_b (infix "\<sqsubseteq>" 60) and Y f
    3.99 +  assumes chain: "Complete_Partial_Order.chain le_b Y" 
   3.100 +  and mono1: "\<And>y. y \<in> Y \<Longrightarrow> monotone le_b op \<le> (\<lambda>x. f x y)"
   3.101 +  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"
   3.102 +begin
   3.103 +
   3.104 +lemma Sup_mono: 
   3.105 +  assumes le: "x \<sqsubseteq> y" and x: "x \<in> Y" and y: "y \<in> Y"
   3.106 +  shows "\<Squnion>(f x ` Y) \<le> \<Squnion>(f y ` Y)" (is "_ \<le> ?rhs")
   3.107 +proof(rule ccpo_Sup_least)
   3.108 +  from chain show chain': "Complete_Partial_Order.chain op \<le> (f x ` Y)" when "x \<in> Y" for x
   3.109 +    by(rule chain_imageI) (insert that, auto dest: mono2)
   3.110 +
   3.111 +  fix x'
   3.112 +  assume "x' \<in> f x ` Y"
   3.113 +  then obtain y' where "y' \<in> Y" "x' = f x y'" by blast note this(2)
   3.114 +  also from mono1[OF `y' \<in> Y`] le have "\<dots> \<le> f y y'" by(rule monotoneD)
   3.115 +  also have "\<dots> \<le> ?rhs" using chain'[OF y]
   3.116 +    by (auto intro!: ccpo_Sup_upper simp add: `y' \<in> Y`)
   3.117 +  finally show "x' \<le> ?rhs" .
   3.118 +qed(rule x)
   3.119 +
   3.120 +lemma diag_Sup: "\<Squnion>((\<lambda>x. \<Squnion>(f x ` Y)) ` Y) = \<Squnion>((\<lambda>x. f x x) ` Y)" (is "?lhs = ?rhs")
   3.121 +proof(rule antisym)
   3.122 +  have chain1: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>(f x ` Y)) ` Y)"
   3.123 +    using chain by(rule chain_imageI)(rule Sup_mono)
   3.124 +  have chain2: "\<And>y'. y' \<in> Y \<Longrightarrow> Complete_Partial_Order.chain op \<le> (f y' ` Y)" using chain
   3.125 +    by(rule chain_imageI)(auto dest: mono2)
   3.126 +  have chain3: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. f x x) ` Y)"
   3.127 +    using chain by(rule chain_imageI)(auto intro: monotoneD[OF mono1] mono2 order.trans)
   3.128 +
   3.129 +  show "?lhs \<le> ?rhs" using chain1
   3.130 +  proof(rule ccpo_Sup_least)
   3.131 +    fix x'
   3.132 +    assume "x' \<in> (\<lambda>x. \<Squnion>(f x ` Y)) ` Y"
   3.133 +    then obtain y' where "y' \<in> Y" "x' = \<Squnion>(f y' ` Y)" by blast note this(2)
   3.134 +    also have "\<dots> \<le> ?rhs" using chain2[OF `y' \<in> Y`]
   3.135 +    proof(rule ccpo_Sup_least)
   3.136 +      fix x
   3.137 +      assume "x \<in> f y' ` Y"
   3.138 +      then obtain y where "y \<in> Y" and x: "x = f y' y" by blast
   3.139 +      def y'' \<equiv> "if y \<sqsubseteq> y' then y' else y"
   3.140 +      from chain `y \<in> Y` `y' \<in> Y` have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
   3.141 +      hence "f y' y \<le> f y'' y''" using `y \<in> Y` `y' \<in> Y`
   3.142 +        by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1])
   3.143 +      also from `y \<in> Y` `y' \<in> Y` have "y'' \<in> Y" by(simp add: y''_def)
   3.144 +      from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: `y'' \<in> Y`)
   3.145 +      finally show "x \<le> ?rhs" by(simp add: x)
   3.146 +    qed
   3.147 +    finally show "x' \<le> ?rhs" .
   3.148 +  qed
   3.149 +
   3.150 +  show "?rhs \<le> ?lhs" using chain3
   3.151 +  proof(rule ccpo_Sup_least)
   3.152 +    fix y
   3.153 +    assume "y \<in> (\<lambda>x. f x x) ` Y"
   3.154 +    then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2)
   3.155 +    also from chain2[OF `x \<in> Y`] have "\<dots> \<le> \<Squnion>(f x ` Y)"
   3.156 +      by(rule ccpo_Sup_upper)(simp add: `x \<in> Y`)
   3.157 +    also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: `x \<in> Y`)
   3.158 +    finally show "y \<le> ?lhs" .
   3.159 +  qed
   3.160 +qed
   3.161 +
   3.162 +end
   3.163 +
   3.164 +lemma Sup_image_mono_le:
   3.165 +  fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>_" [900] 900)
   3.166 +  assumes ccpo: "class.ccpo Sup_b op \<sqsubseteq> lt_b"
   3.167 +  assumes chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
   3.168 +  and mono: "\<And>x y. \<lbrakk> x \<sqsubseteq> y; x \<in> Y \<rbrakk> \<Longrightarrow> f x \<le> f y"
   3.169 +  shows "Sup (f ` Y) \<le> f (\<Or>Y)"
   3.170 +proof(rule ccpo_Sup_least)
   3.171 +  show "Complete_Partial_Order.chain op \<le> (f ` Y)"
   3.172 +    using chain by(rule chain_imageI)(rule mono)
   3.173 +
   3.174 +  fix x
   3.175 +  assume "x \<in> f ` Y"
   3.176 +  then obtain y where "y \<in> Y" and "x = f y" by blast note this(2)
   3.177 +  also have "y \<sqsubseteq> \<Or>Y" using ccpo chain `y \<in> Y` by(rule ccpo.ccpo_Sup_upper)
   3.178 +  hence "f y \<le> f (\<Or>Y)" using `y \<in> Y` by(rule mono)
   3.179 +  finally show "x \<le> \<dots>" .
   3.180 +qed
   3.181 +
   3.182 +lemma swap_Sup:
   3.183 +  fixes le_b (infix "\<sqsubseteq>" 60)
   3.184 +  assumes Y: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
   3.185 +  and Z: "Complete_Partial_Order.chain (fun_ord op \<le>) Z"
   3.186 +  and mono: "\<And>f. f \<in> Z \<Longrightarrow> monotone op \<sqsubseteq> op \<le> f"
   3.187 +  shows "\<Squnion>((\<lambda>x. \<Squnion>(x ` Y)) ` Z) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y)"
   3.188 +  (is "?lhs = ?rhs")
   3.189 +proof(cases "Y = {}")
   3.190 +  case True
   3.191 +  then show ?thesis
   3.192 +    by (simp add: image_constant_conv cong del: strong_SUP_cong)
   3.193 +next
   3.194 +  case False
   3.195 +  have chain1: "\<And>f. f \<in> Z \<Longrightarrow> Complete_Partial_Order.chain op \<le> (f ` Y)"
   3.196 +    by(rule chain_imageI[OF Y])(rule monotoneD[OF mono])
   3.197 +  have chain2: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>(x ` Y)) ` Z)" using Z
   3.198 +  proof(rule chain_imageI)
   3.199 +    fix f g
   3.200 +    assume "f \<in> Z" "g \<in> Z"
   3.201 +      and "fun_ord op \<le> f g"
   3.202 +    from chain1[OF `f \<in> Z`] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
   3.203 +    proof(rule ccpo_Sup_least)
   3.204 +      fix x
   3.205 +      assume "x \<in> f ` Y"
   3.206 +      then obtain y where "y \<in> Y" "x = f y" by blast note this(2)
   3.207 +      also have "\<dots> \<le> g y" using `fun_ord op \<le> f g` by(simp add: fun_ord_def)
   3.208 +      also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF `g \<in> Z`]
   3.209 +        by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
   3.210 +      finally show "x \<le> \<Squnion>(g ` Y)" .
   3.211 +    qed
   3.212 +  qed
   3.213 +  have chain3: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` Z)"
   3.214 +    using Z by(rule chain_imageI)(simp add: fun_ord_def)
   3.215 +  have chain4: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y)"
   3.216 +    using Y
   3.217 +  proof(rule chain_imageI)
   3.218 +    fix f x y
   3.219 +    assume "x \<sqsubseteq> y"
   3.220 +    show "\<Squnion>((\<lambda>f. f x) ` Z) \<le> \<Squnion>((\<lambda>f. f y) ` Z)" (is "_ \<le> ?rhs") using chain3
   3.221 +    proof(rule ccpo_Sup_least)
   3.222 +      fix x'
   3.223 +      assume "x' \<in> (\<lambda>f. f x) ` Z"
   3.224 +      then obtain f where "f \<in> Z" "x' = f x" by blast note this(2)
   3.225 +      also have "f x \<le> f y" using `f \<in> Z` `x \<sqsubseteq> y` by(rule monotoneD[OF mono])
   3.226 +      also have "f y \<le> ?rhs" using chain3
   3.227 +        by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
   3.228 +      finally show "x' \<le> ?rhs" .
   3.229 +    qed
   3.230 +  qed
   3.231 +
   3.232 +  from chain2 have "?lhs \<le> ?rhs"
   3.233 +  proof(rule ccpo_Sup_least)
   3.234 +    fix x
   3.235 +    assume "x \<in> (\<lambda>x. \<Squnion>(x ` Y)) ` Z"
   3.236 +    then obtain f where "f \<in> Z" "x = \<Squnion>(f ` Y)" by blast note this(2)
   3.237 +    also have "\<dots> \<le> ?rhs" using chain1[OF `f \<in> Z`]
   3.238 +    proof(rule ccpo_Sup_least)
   3.239 +      fix x'
   3.240 +      assume "x' \<in> f ` Y"
   3.241 +      then obtain y where "y \<in> Y" "x' = f y" by blast note this(2)
   3.242 +      also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3
   3.243 +        by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
   3.244 +      also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
   3.245 +      finally show "x' \<le> ?rhs" .
   3.246 +    qed
   3.247 +    finally show "x \<le> ?rhs" .
   3.248 +  qed
   3.249 +  moreover
   3.250 +  have "?rhs \<le> ?lhs" using chain4
   3.251 +  proof(rule ccpo_Sup_least)
   3.252 +    fix x
   3.253 +    assume "x \<in> (\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y"
   3.254 +    then obtain y where "y \<in> Y" "x = \<Squnion>((\<lambda>f. f y) ` Z)" by blast note this(2)
   3.255 +    also have "\<dots> \<le> ?lhs" using chain3
   3.256 +    proof(rule ccpo_Sup_least)
   3.257 +      fix x'
   3.258 +      assume "x' \<in> (\<lambda>f. f y) ` Z"
   3.259 +      then obtain f where "f \<in> Z" "x' = f y" by blast note this(2)
   3.260 +      also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF `f \<in> Z`]
   3.261 +        by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
   3.262 +      also have "\<dots> \<le> ?lhs" using chain2
   3.263 +        by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
   3.264 +      finally show "x' \<le> ?lhs" .
   3.265 +    qed
   3.266 +    finally show "x \<le> ?lhs" .
   3.267 +  qed
   3.268 +  ultimately show "?lhs = ?rhs" by(rule antisym)
   3.269 +qed
   3.270 +
   3.271 +lemma fixp_mono:
   3.272 +  assumes fg: "fun_ord op \<le> f g"
   3.273 +  and f: "monotone op \<le> op \<le> f"
   3.274 +  and g: "monotone op \<le> op \<le> g"
   3.275 +  shows "ccpo_class.fixp f \<le> ccpo_class.fixp g"
   3.276 +unfolding fixp_def
   3.277 +proof(rule ccpo_Sup_least)
   3.278 +  fix x
   3.279 +  assume "x \<in> ccpo_class.iterates f"
   3.280 +  thus "x \<le> \<Squnion>ccpo_class.iterates g"
   3.281 +  proof induction
   3.282 +    case (step x)
   3.283 +    from f step.IH have "f x \<le> f (\<Squnion>ccpo_class.iterates g)" by(rule monotoneD)
   3.284 +    also have "\<dots> \<le> g (\<Squnion>ccpo_class.iterates g)" using fg by(simp add: fun_ord_def)
   3.285 +    also have "\<dots> = \<Squnion>ccpo_class.iterates g" by(fold fixp_def fixp_unfold[OF g]) simp
   3.286 +    finally show ?case .
   3.287 +  qed(blast intro: ccpo_Sup_least)
   3.288 +qed(rule chain_iterates[OF f])
   3.289 +
   3.290 +context fixes ordb :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) begin
   3.291 +
   3.292 +lemma iterates_mono:
   3.293 +  assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
   3.294 +  and mono: "\<And>f. monotone op \<sqsubseteq> op \<le> f \<Longrightarrow> monotone op \<sqsubseteq> op \<le> (F f)"
   3.295 +  shows "monotone op \<sqsubseteq> op \<le> f"
   3.296 +using f
   3.297 +by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mono_lub)+
   3.298 +
   3.299 +lemma fixp_preserves_mono:
   3.300 +  assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. F f x)"
   3.301 +  and mono2: "\<And>f. monotone op \<sqsubseteq> op \<le> f \<Longrightarrow> monotone op \<sqsubseteq> op \<le> (F f)"
   3.302 +  shows "monotone op \<sqsubseteq> op \<le> (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) F)"
   3.303 +  (is "monotone _ _ ?fixp")
   3.304 +proof(rule monotoneI)
   3.305 +  have mono: "monotone (fun_ord op \<le>) (fun_ord op \<le>) F"
   3.306 +    by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])
   3.307 +  let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
   3.308 +  have chain: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` ?iter)"
   3.309 +    by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def)
   3.310 +
   3.311 +  fix x y
   3.312 +  assume "x \<sqsubseteq> y"
   3.313 +  show "?fixp x \<le> ?fixp y"
   3.314 +    unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain
   3.315 +  proof(rule ccpo_Sup_least)
   3.316 +    fix x'
   3.317 +    assume "x' \<in> (\<lambda>f. f x) ` ?iter"
   3.318 +    then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
   3.319 +    also have "f x \<le> f y"
   3.320 +      by(rule monotoneD[OF iterates_mono[OF `f \<in> ?iter` mono2]])(blast intro: `x \<sqsubseteq> y`)+
   3.321 +    also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
   3.322 +      by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)
   3.323 +    finally show "x' \<le> \<dots>" .
   3.324 +  qed
   3.325 +qed
   3.326 +
   3.327 +end
   3.328 +
   3.329 +end
   3.330 +
   3.331 +lemma monotone2monotone:
   3.332 +  assumes 2: "\<And>x. monotone ordb ordc (\<lambda>y. f x y)"
   3.333 +  and t: "monotone orda ordb (\<lambda>x. t x)"
   3.334 +  and 1: "\<And>y. monotone orda ordc (\<lambda>x. f x y)"
   3.335 +  and trans: "transp ordc"
   3.336 +  shows "monotone orda ordc (\<lambda>x. f x (t x))"
   3.337 +by(blast intro: monotoneI transpD[OF trans] monotoneD[OF t] monotoneD[OF 2] monotoneD[OF 1])
   3.338 +
   3.339 +subsection {* Continuity *}
   3.340 +
   3.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"
   3.342 +where
   3.343 +  "cont luba orda lubb ordb f \<longleftrightarrow> 
   3.344 +  (\<forall>Y. Complete_Partial_Order.chain orda Y \<longrightarrow> Y \<noteq> {} \<longrightarrow> f (luba Y) = lubb (f ` Y))"
   3.345 +
   3.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"
   3.347 +where
   3.348 +  "mcont luba orda lubb ordb f \<longleftrightarrow>
   3.349 +   monotone orda ordb f \<and> cont luba orda lubb ordb f"
   3.350 +
   3.351 +subsubsection {* Theorem collection @{text cont_intro} *}
   3.352 +
   3.353 +named_theorems cont_intro "continuity and admissibility intro rules"
   3.354 +ML {*
   3.355 +(* apply cont_intro rules as intro and try to solve 
   3.356 +   the remaining of the emerging subgoals with simp *)
   3.357 +fun cont_intro_tac ctxt =
   3.358 +  REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems cont_intro})))
   3.359 +  THEN_ALL_NEW (SOLVED' (simp_tac ctxt))
   3.360 +
   3.361 +fun cont_intro_simproc ctxt ct =
   3.362 +  let
   3.363 +    fun mk_stmt t = t
   3.364 +      |> HOLogic.mk_Trueprop
   3.365 +      |> Thm.cterm_of ctxt
   3.366 +      |> Goal.init
   3.367 +    fun mk_thm t =
   3.368 +      case SINGLE (cont_intro_tac ctxt 1) (mk_stmt t) of
   3.369 +        SOME thm => SOME (Goal.finish ctxt thm RS @{thm Eq_TrueI})
   3.370 +      | NONE => NONE
   3.371 +  in
   3.372 +    case Thm.term_of ct of
   3.373 +      t as Const (@{const_name ccpo.admissible}, _) $ _ $ _ $ _ => mk_thm t
   3.374 +    | t as Const (@{const_name mcont}, _) $ _ $ _ $ _ $ _ $ _ => mk_thm t
   3.375 +    | t as Const (@{const_name monotone}, _) $ _ $ _ $ _ => mk_thm t
   3.376 +    | _ => NONE
   3.377 +  end
   3.378 +  handle THM _ => NONE 
   3.379 +  | TYPE _ => NONE
   3.380 +*}
   3.381 +
   3.382 +simproc_setup "cont_intro"
   3.383 +  ( "ccpo.admissible lub ord P"
   3.384 +  | "mcont lub ord lub' ord' f"
   3.385 +  | "monotone ord ord' f"
   3.386 +  ) = {* K cont_intro_simproc *}
   3.387 +
   3.388 +lemmas [cont_intro] =
   3.389 +  call_mono
   3.390 +  let_mono
   3.391 +  if_mono
   3.392 +  option.const_mono
   3.393 +  tailrec.const_mono
   3.394 +  bind_mono
   3.395 +
   3.396 +declare if_mono[simp]
   3.397 +
   3.398 +lemma monotone_id' [cont_intro]: "monotone ord ord (\<lambda>x. x)"
   3.399 +by(simp add: monotone_def)
   3.400 +
   3.401 +lemma monotone_applyI:
   3.402 +  "monotone orda ordb F \<Longrightarrow> monotone (fun_ord orda) ordb (\<lambda>f. F (f x))"
   3.403 +by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
   3.404 +
   3.405 +lemma monotone_if_fun [partial_function_mono]:
   3.406 +  "\<lbrakk> monotone (fun_ord orda) (fun_ord ordb) F; monotone (fun_ord orda) (fun_ord ordb) G \<rbrakk>
   3.407 +  \<Longrightarrow> monotone (fun_ord orda) (fun_ord ordb) (\<lambda>f n. if c n then F f n else G f n)"
   3.408 +by(simp add: monotone_def fun_ord_def)
   3.409 +
   3.410 +lemma monotone_fun_apply_fun [partial_function_mono]: 
   3.411 +  "monotone (fun_ord (fun_ord ord)) (fun_ord ord) (\<lambda>f n. f t (g n))"
   3.412 +by(rule monotoneI)(simp add: fun_ord_def)
   3.413 +
   3.414 +lemma monotone_fun_ord_apply: 
   3.415 +  "monotone orda (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. monotone orda ordb (\<lambda>y. f y x))"
   3.416 +by(auto simp add: monotone_def fun_ord_def)
   3.417 +
   3.418 +context preorder begin
   3.419 +
   3.420 +lemma transp_le [simp, cont_intro]: "transp op \<le>"
   3.421 +by(rule transpI)(rule order_trans)
   3.422 +
   3.423 +lemma monotone_const [simp, cont_intro]: "monotone ord op \<le> (\<lambda>_. c)"
   3.424 +by(rule monotoneI) simp
   3.425 +
   3.426 +end
   3.427 +
   3.428 +lemma transp_le [cont_intro, simp]:
   3.429 +  "class.preorder ord (mk_less ord) \<Longrightarrow> transp ord"
   3.430 +by(rule preorder.transp_le)
   3.431 +
   3.432 +context partial_function_definitions begin
   3.433 +
   3.434 +declare const_mono [cont_intro, simp]
   3.435 +
   3.436 +lemma transp_le [cont_intro, simp]: "transp leq"
   3.437 +by(rule transpI)(rule leq_trans)
   3.438 +
   3.439 +lemma preorder [cont_intro, simp]: "class.preorder leq (mk_less leq)"
   3.440 +by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans)
   3.441 +
   3.442 +declare ccpo[cont_intro, simp]
   3.443 +
   3.444 +end
   3.445 +
   3.446 +lemma contI [intro?]:
   3.447 +  "(\<And>Y. \<lbrakk> Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> \<Longrightarrow> f (luba Y) = lubb (f ` Y)) 
   3.448 +  \<Longrightarrow> cont luba orda lubb ordb f"
   3.449 +unfolding cont_def by blast
   3.450 +
   3.451 +lemma contD:
   3.452 +  "\<lbrakk> cont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> 
   3.453 +  \<Longrightarrow> f (luba Y) = lubb (f ` Y)"
   3.454 +unfolding cont_def by blast
   3.455 +
   3.456 +lemma cont_id [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord id"
   3.457 +by(rule contI) simp
   3.458 +
   3.459 +lemma cont_id' [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord (\<lambda>x. x)"
   3.460 +using cont_id[unfolded id_def] .
   3.461 +
   3.462 +lemma cont_applyI [cont_intro]:
   3.463 +  assumes cont: "cont luba orda lubb ordb g"
   3.464 +  shows "cont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. g (f x))"
   3.465 +by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont])
   3.466 +
   3.467 +lemma call_cont: "cont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
   3.468 +by(simp add: cont_def fun_lub_apply)
   3.469 +
   3.470 +lemma cont_if [cont_intro]:
   3.471 +  "\<lbrakk> cont luba orda lubb ordb f; cont luba orda lubb ordb g \<rbrakk>
   3.472 +  \<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
   3.473 +by(cases c) simp_all
   3.474 +
   3.475 +lemma mcontI [intro?]:
   3.476 +   "\<lbrakk> monotone orda ordb f; cont luba orda lubb ordb f \<rbrakk> \<Longrightarrow> mcont luba orda lubb ordb f"
   3.477 +by(simp add: mcont_def)
   3.478 +
   3.479 +lemma mcont_mono: "mcont luba orda lubb ordb f \<Longrightarrow> monotone orda ordb f"
   3.480 +by(simp add: mcont_def)
   3.481 +
   3.482 +lemma mcont_cont [simp]: "mcont luba orda lubb ordb f \<Longrightarrow> cont luba orda lubb ordb f"
   3.483 +by(simp add: mcont_def)
   3.484 +
   3.485 +lemma mcont_monoD:
   3.486 +  "\<lbrakk> mcont luba orda lubb ordb f; orda x y \<rbrakk> \<Longrightarrow> ordb (f x) (f y)"
   3.487 +by(auto simp add: mcont_def dest: monotoneD)
   3.488 +
   3.489 +lemma mcont_contD:
   3.490 +  "\<lbrakk> mcont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk>
   3.491 +  \<Longrightarrow> f (luba Y) = lubb (f ` Y)"
   3.492 +by(auto simp add: mcont_def dest: contD)
   3.493 +
   3.494 +lemma mcont_call [cont_intro, simp]:
   3.495 +  "mcont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
   3.496 +by(simp add: mcont_def call_mono call_cont)
   3.497 +
   3.498 +lemma mcont_id' [cont_intro, simp]: "mcont lub ord lub ord (\<lambda>x. x)"
   3.499 +by(simp add: mcont_def monotone_id')
   3.500 +
   3.501 +lemma mcont_applyI:
   3.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))"
   3.503 +by(simp add: mcont_def monotone_applyI cont_applyI)
   3.504 +
   3.505 +lemma mcont_if [cont_intro, simp]:
   3.506 +  "\<lbrakk> mcont luba orda lubb ordb (\<lambda>x. f x); mcont luba orda lubb ordb (\<lambda>x. g x) \<rbrakk>
   3.507 +  \<Longrightarrow> mcont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
   3.508 +by(simp add: mcont_def cont_if)
   3.509 +
   3.510 +lemma cont_fun_lub_apply: 
   3.511 +  "cont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. cont luba orda lubb ordb (\<lambda>y. f y x))"
   3.512 +by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def)
   3.513 +
   3.514 +lemma mcont_fun_lub_apply: 
   3.515 +  "mcont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. mcont luba orda lubb ordb (\<lambda>y. f y x))"
   3.516 +by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def)
   3.517 +
   3.518 +context ccpo begin
   3.519 +
   3.520 +lemma cont_const [simp, cont_intro]: "cont luba orda Sup op \<le> (\<lambda>x. c)"
   3.521 +by (rule contI) (simp add: image_constant_conv cong del: strong_SUP_cong)
   3.522 +
   3.523 +lemma mcont_const [cont_intro, simp]:
   3.524 +  "mcont luba orda Sup op \<le> (\<lambda>x. c)"
   3.525 +by(simp add: mcont_def)
   3.526 +
   3.527 +lemma cont_apply:
   3.528 +  assumes 2: "\<And>x. cont lubb ordb Sup op \<le> (\<lambda>y. f x y)"
   3.529 +  and t: "cont luba orda lubb ordb (\<lambda>x. t x)"
   3.530 +  and 1: "\<And>y. cont luba orda Sup op \<le> (\<lambda>x. f x y)"
   3.531 +  and mono: "monotone orda ordb (\<lambda>x. t x)"
   3.532 +  and mono2: "\<And>x. monotone ordb op \<le> (\<lambda>y. f x y)"
   3.533 +  and mono1: "\<And>y. monotone orda op \<le> (\<lambda>x. f x y)"
   3.534 +  shows "cont luba orda Sup op \<le> (\<lambda>x. f x (t x))"
   3.535 +proof
   3.536 +  fix Y
   3.537 +  assume chain: "Complete_Partial_Order.chain orda Y" and "Y \<noteq> {}"
   3.538 +  moreover from chain have chain': "Complete_Partial_Order.chain ordb (t ` Y)"
   3.539 +    by(rule chain_imageI)(rule monotoneD[OF mono])
   3.540 +  ultimately show "f (luba Y) (t (luba Y)) = \<Squnion>((\<lambda>x. f x (t x)) ` Y)"
   3.541 +    by(simp add: contD[OF 1] contD[OF t] contD[OF 2] image_image)
   3.542 +      (rule diag_Sup[OF chain], auto intro: monotone2monotone[OF mono2 mono monotone_const transpI] monotoneD[OF mono1])
   3.543 +qed
   3.544 +
   3.545 +lemma mcont2mcont':
   3.546 +  "\<lbrakk> \<And>x. mcont lub' ord' Sup op \<le> (\<lambda>y. f x y);
   3.547 +     \<And>y. mcont lub ord Sup op \<le> (\<lambda>x. f x y);
   3.548 +     mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk>
   3.549 +  \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f x (t x))"
   3.550 +unfolding mcont_def by(blast intro: transp_le monotone2monotone cont_apply)
   3.551 +
   3.552 +lemma mcont2mcont:
   3.553 +  "\<lbrakk>mcont lub' ord' Sup op \<le> (\<lambda>x. f x); mcont lub ord lub' ord' (\<lambda>x. t x)\<rbrakk> 
   3.554 +  \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f (t x))"
   3.555 +by(rule mcont2mcont'[OF _ mcont_const]) 
   3.556 +
   3.557 +context
   3.558 +  fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) 
   3.559 +  and lub :: "'b set \<Rightarrow> 'b" ("\<Or>_" [900] 900)
   3.560 +begin
   3.561 +
   3.562 +lemma cont_fun_lub_Sup:
   3.563 +  assumes chainM: "Complete_Partial_Order.chain (fun_ord op \<le>) M"
   3.564 +  and mcont [rule_format]: "\<forall>f\<in>M. mcont lub op \<sqsubseteq> Sup op \<le> f"
   3.565 +  shows "cont lub op \<sqsubseteq> Sup op \<le> (fun_lub Sup M)"
   3.566 +proof(rule contI)
   3.567 +  fix Y
   3.568 +  assume chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
   3.569 +    and Y: "Y \<noteq> {}"
   3.570 +  from swap_Sup[OF chain chainM mcont[THEN mcont_mono]]
   3.571 +  show "fun_lub Sup M (\<Or>Y) = \<Squnion>(fun_lub Sup M ` Y)"
   3.572 +    by(simp add: mcont_contD[OF mcont chain Y] fun_lub_apply cong: image_cong)
   3.573 +qed
   3.574 +
   3.575 +lemma mcont_fun_lub_Sup:
   3.576 +  "\<lbrakk> Complete_Partial_Order.chain (fun_ord op \<le>) M;
   3.577 +    \<forall>f\<in>M. mcont lub ord Sup op \<le> f \<rbrakk>
   3.578 +  \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (fun_lub Sup M)"
   3.579 +by(simp add: mcont_def cont_fun_lub_Sup mono_lub)
   3.580 +
   3.581 +lemma iterates_mcont:
   3.582 +  assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
   3.583 +  and mono: "\<And>f. mcont lub op \<sqsubseteq> Sup op \<le> f \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (F f)"
   3.584 +  shows "mcont lub op \<sqsubseteq> Sup op \<le> f"
   3.585 +using f
   3.586 +by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mcont_fun_lub_Sup)+
   3.587 +
   3.588 +lemma fixp_preserves_mcont:
   3.589 +  assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. F f x)"
   3.590 +  and mcont: "\<And>f. mcont lub op \<sqsubseteq> Sup op \<le> f \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (F f)"
   3.591 +  shows "mcont lub op \<sqsubseteq> Sup op \<le> (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) F)"
   3.592 +  (is "mcont _ _ _ _ ?fixp")
   3.593 +unfolding mcont_def
   3.594 +proof(intro conjI monotoneI contI)
   3.595 +  have mono: "monotone (fun_ord op \<le>) (fun_ord op \<le>) F"
   3.596 +    by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])
   3.597 +  let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
   3.598 +  have chain: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` ?iter)"
   3.599 +    by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def)
   3.600 +
   3.601 +  {
   3.602 +    fix x y
   3.603 +    assume "x \<sqsubseteq> y"
   3.604 +    show "?fixp x \<le> ?fixp y"
   3.605 +      unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain
   3.606 +    proof(rule ccpo_Sup_least)
   3.607 +      fix x'
   3.608 +      assume "x' \<in> (\<lambda>f. f x) ` ?iter"
   3.609 +      then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
   3.610 +      also from _ `x \<sqsubseteq> y` have "f x \<le> f y"
   3.611 +        by(rule mcont_monoD[OF iterates_mcont[OF `f \<in> ?iter` mcont]])
   3.612 +      also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
   3.613 +        by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)
   3.614 +      finally show "x' \<le> \<dots>" .
   3.615 +    qed
   3.616 +  next
   3.617 +    fix Y
   3.618 +    assume chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
   3.619 +      and Y: "Y \<noteq> {}"
   3.620 +    { fix f
   3.621 +      assume "f \<in> ?iter"
   3.622 +      hence "f (\<Or>Y) = \<Squnion>(f ` Y)"
   3.623 +        using mcont chain Y by(rule mcont_contD[OF iterates_mcont]) }
   3.624 +    moreover have "\<Squnion>((\<lambda>f. \<Squnion>(f ` Y)) ` ?iter) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` ?iter)) ` Y)"
   3.625 +      using chain ccpo.chain_iterates[OF ccpo_fun mono]
   3.626 +      by(rule swap_Sup)(rule mcont_mono[OF iterates_mcont[OF _ mcont]])
   3.627 +    ultimately show "?fixp (\<Or>Y) = \<Squnion>(?fixp ` Y)" unfolding ccpo.fixp_def[OF ccpo_fun]
   3.628 +      by(simp add: fun_lub_apply cong: image_cong)
   3.629 +  }
   3.630 +qed
   3.631 +
   3.632 +end
   3.633 +
   3.634 +context
   3.635 +  fixes F :: "'c \<Rightarrow> 'c" and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and f
   3.636 +  assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. U (F (C f)) x)"
   3.637 +  and eq: "f \<equiv> C (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) (\<lambda>f. U (F (C f))))"
   3.638 +  and inverse: "\<And>f. U (C f) = f"
   3.639 +begin
   3.640 +
   3.641 +lemma fixp_preserves_mono_uc:
   3.642 +  assumes mono2: "\<And>f. monotone ord op \<le> (U f) \<Longrightarrow> monotone ord op \<le> (U (F f))"
   3.643 +  shows "monotone ord op \<le> (U f)"
   3.644 +using fixp_preserves_mono[OF mono mono2] by(subst eq)(simp add: inverse)
   3.645 +
   3.646 +lemma fixp_preserves_mcont_uc:
   3.647 +  assumes mcont: "\<And>f. mcont lubb ordb Sup op \<le> (U f) \<Longrightarrow> mcont lubb ordb Sup op \<le> (U (F f))"
   3.648 +  shows "mcont lubb ordb Sup op \<le> (U f)"
   3.649 +using fixp_preserves_mcont[OF mono mcont] by(subst eq)(simp add: inverse)
   3.650 +
   3.651 +end
   3.652 +
   3.653 +lemmas fixp_preserves_mono1 = fixp_preserves_mono_uc[of "\<lambda>x. x" _ "\<lambda>x. x", OF _ _ refl]
   3.654 +lemmas fixp_preserves_mono2 =
   3.655 +  fixp_preserves_mono_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
   3.656 +lemmas fixp_preserves_mono3 =
   3.657 +  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]
   3.658 +lemmas fixp_preserves_mono4 =
   3.659 +  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]
   3.660 +
   3.661 +lemmas fixp_preserves_mcont1 = fixp_preserves_mcont_uc[of "\<lambda>x. x" _ "\<lambda>x. x", OF _ _ refl]
   3.662 +lemmas fixp_preserves_mcont2 =
   3.663 +  fixp_preserves_mcont_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
   3.664 +lemmas fixp_preserves_mcont3 =
   3.665 +  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]
   3.666 +lemmas fixp_preserves_mcont4 =
   3.667 +  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]
   3.668 +
   3.669 +end
   3.670 +
   3.671 +lemma (in preorder) monotone_if_bot:
   3.672 +  fixes bot
   3.673 +  assumes mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> (x \<le> bound) \<rbrakk> \<Longrightarrow> ord (f x) (f y)"
   3.674 +  and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> ord bot (f x)" "ord bot bot"
   3.675 +  shows "monotone op \<le> ord (\<lambda>x. if x \<le> bound then bot else f x)"
   3.676 +by(rule monotoneI)(auto intro: bot intro: mono order_trans)
   3.677 +
   3.678 +lemma (in ccpo) mcont_if_bot:
   3.679 +  fixes bot and lub ("\<Or>_" [900] 900) and ord (infix "\<sqsubseteq>" 60)
   3.680 +  assumes ccpo: "class.ccpo lub op \<sqsubseteq> lt"
   3.681 +  and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
   3.682 +  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)"
   3.683 +  and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> bot \<sqsubseteq> f x"
   3.684 +  shows "mcont Sup op \<le> lub op \<sqsubseteq> (\<lambda>x. if x \<le> bound then bot else f x)" (is "mcont _ _ _ _ ?g")
   3.685 +proof(intro mcontI contI)
   3.686 +  interpret c: ccpo lub "op \<sqsubseteq>" lt by(fact ccpo)
   3.687 +  show "monotone op \<le> op \<sqsubseteq> ?g" by(rule monotone_if_bot)(simp_all add: mono bot)
   3.688 +
   3.689 +  fix Y
   3.690 +  assume chain: "Complete_Partial_Order.chain op \<le> Y" and Y: "Y \<noteq> {}"
   3.691 +  show "?g (\<Squnion>Y) = \<Or>(?g ` Y)"
   3.692 +  proof(cases "Y \<subseteq> {x. x \<le> bound}")
   3.693 +    case True
   3.694 +    hence "\<Squnion>Y \<le> bound" using chain by(auto intro: ccpo_Sup_least)
   3.695 +    moreover have "Y \<inter> {x. \<not> x \<le> bound} = {}" using True by auto
   3.696 +    ultimately show ?thesis using True Y
   3.697 +      by (auto simp add: image_constant_conv cong del: c.strong_SUP_cong)
   3.698 +  next
   3.699 +    case False
   3.700 +    let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"
   3.701 +    have chain': "Complete_Partial_Order.chain op \<le> ?Y"
   3.702 +      using chain by(rule chain_subset) simp
   3.703 +
   3.704 +    from False obtain y where ybound: "\<not> y \<le> bound" and y: "y \<in> Y" by blast
   3.705 +    hence "\<not> \<Squnion>Y \<le> bound" by (metis ccpo_Sup_upper chain order.trans)
   3.706 +    hence "?g (\<Squnion>Y) = f (\<Squnion>Y)" by simp
   3.707 +    also have "\<Squnion>Y \<le> \<Squnion>?Y" using chain
   3.708 +    proof(rule ccpo_Sup_least)
   3.709 +      fix x
   3.710 +      assume x: "x \<in> Y"
   3.711 +      show "x \<le> \<Squnion>?Y"
   3.712 +      proof(cases "x \<le> bound")
   3.713 +        case True
   3.714 +        with chainD[OF chain x y] have "x \<le> y" using ybound by(auto intro: order_trans)
   3.715 +        thus ?thesis by(rule order_trans)(auto intro: ccpo_Sup_upper[OF chain'] simp add: y ybound)
   3.716 +      qed(auto intro: ccpo_Sup_upper[OF chain'] simp add: x)
   3.717 +    qed
   3.718 +    hence "\<Squnion>Y = \<Squnion>?Y" by(rule antisym)(blast intro: ccpo_Sup_least[OF chain'] ccpo_Sup_upper[OF chain])
   3.719 +    hence "f (\<Squnion>Y) = f (\<Squnion>?Y)" by simp
   3.720 +    also have "f (\<Squnion>?Y) = \<Or>(f ` ?Y)" using chain' by(rule cont)(insert y ybound, auto)
   3.721 +    also have "\<Or>(f ` ?Y) = \<Or>(?g ` Y)"
   3.722 +    proof(cases "Y \<inter> {x. x \<le> bound} = {}")
   3.723 +      case True
   3.724 +      hence "f ` ?Y = ?g ` Y" by auto
   3.725 +      thus ?thesis by(rule arg_cong)
   3.726 +    next
   3.727 +      case False
   3.728 +      have chain'': "Complete_Partial_Order.chain op \<sqsubseteq> (insert bot (f ` ?Y))"
   3.729 +        using chain by(auto intro!: chainI bot dest: chainD intro: mono)
   3.730 +      hence chain''': "Complete_Partial_Order.chain op \<sqsubseteq> (f ` ?Y)" by(rule chain_subset) blast
   3.731 +      have "bot \<sqsubseteq> \<Or>(f ` ?Y)" using y ybound by(blast intro: c.order_trans[OF bot] c.ccpo_Sup_upper[OF chain'''])
   3.732 +      hence "\<Or>(insert bot (f ` ?Y)) \<sqsubseteq> \<Or>(f ` ?Y)" using chain''
   3.733 +        by(auto intro: c.ccpo_Sup_least c.ccpo_Sup_upper[OF chain''']) 
   3.734 +      with _ have "\<dots> = \<Or>(insert bot (f ` ?Y))"
   3.735 +        by(rule c.antisym)(blast intro: c.ccpo_Sup_least[OF chain'''] c.ccpo_Sup_upper[OF chain''])
   3.736 +      also have "insert bot (f ` ?Y) = ?g ` Y" using False by auto
   3.737 +      finally show ?thesis .
   3.738 +    qed
   3.739 +    finally show ?thesis .
   3.740 +  qed
   3.741 +qed
   3.742 +
   3.743 +context partial_function_definitions begin
   3.744 +
   3.745 +lemma mcont_const [cont_intro, simp]:
   3.746 +  "mcont luba orda lub leq (\<lambda>x. c)"
   3.747 +by(rule ccpo.mcont_const)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
   3.748 +
   3.749 +lemmas [cont_intro, simp] =
   3.750 +  ccpo.cont_const[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.751 +
   3.752 +lemma mono2mono:
   3.753 +  assumes "monotone ordb leq (\<lambda>y. f y)" "monotone orda ordb (\<lambda>x. t x)"
   3.754 +  shows "monotone orda leq (\<lambda>x. f (t x))"
   3.755 +using assms by(rule monotone2monotone) simp_all
   3.756 +
   3.757 +lemmas mcont2mcont' = ccpo.mcont2mcont'[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.758 +lemmas mcont2mcont = ccpo.mcont2mcont[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.759 +
   3.760 +lemmas fixp_preserves_mono1 = ccpo.fixp_preserves_mono1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.761 +lemmas fixp_preserves_mono2 = ccpo.fixp_preserves_mono2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.762 +lemmas fixp_preserves_mono3 = ccpo.fixp_preserves_mono3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.763 +lemmas fixp_preserves_mono4 = ccpo.fixp_preserves_mono4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.764 +lemmas fixp_preserves_mcont1 = ccpo.fixp_preserves_mcont1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.765 +lemmas fixp_preserves_mcont2 = ccpo.fixp_preserves_mcont2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.766 +lemmas fixp_preserves_mcont3 = ccpo.fixp_preserves_mcont3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.767 +lemmas fixp_preserves_mcont4 = ccpo.fixp_preserves_mcont4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.768 +
   3.769 +lemma monotone_if_bot:
   3.770 +  fixes bot
   3.771 +  assumes g: "\<And>x. g x = (if leq x bound then bot else f x)"
   3.772 +  and mono: "\<And>x y. \<lbrakk> leq x y; \<not> leq x bound \<rbrakk> \<Longrightarrow> ord (f x) (f y)"
   3.773 +  and bot: "\<And>x. \<not> leq x bound \<Longrightarrow> ord bot (f x)" "ord bot bot"
   3.774 +  shows "monotone leq ord g"
   3.775 +unfolding g[abs_def] using preorder mono bot by(rule preorder.monotone_if_bot)
   3.776 +
   3.777 +lemma mcont_if_bot:
   3.778 +  fixes bot
   3.779 +  assumes ccpo: "class.ccpo lub' ord (mk_less ord)"
   3.780 +  and bot: "\<And>x. \<not> leq x bound \<Longrightarrow> ord bot (f x)"
   3.781 +  and g: "\<And>x. g x = (if leq x bound then bot else f x)"
   3.782 +  and mono: "\<And>x y. \<lbrakk> leq x y; \<not> leq x bound \<rbrakk> \<Longrightarrow> ord (f x) (f y)"
   3.783 +  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)"
   3.784 +  shows "mcont lub leq lub' ord g"
   3.785 +unfolding g[abs_def] using ccpo mono cont bot by(rule ccpo.mcont_if_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]])
   3.786 +
   3.787 +end
   3.788 +
   3.789 +subsection {* Admissibility *}
   3.790 +
   3.791 +lemma admissible_subst:
   3.792 +  assumes adm: "ccpo.admissible luba orda (\<lambda>x. P x)"
   3.793 +  and mcont: "mcont lubb ordb luba orda f"
   3.794 +  shows "ccpo.admissible lubb ordb (\<lambda>x. P (f x))"
   3.795 +apply(rule ccpo.admissibleI)
   3.796 +apply(frule (1) mcont_contD[OF mcont])
   3.797 +apply(auto intro: ccpo.admissibleD[OF adm] chain_imageI dest: mcont_monoD[OF mcont])
   3.798 +done
   3.799 +
   3.800 +lemmas [simp, cont_intro] = 
   3.801 +  admissible_all
   3.802 +  admissible_ball
   3.803 +  admissible_const
   3.804 +  admissible_conj
   3.805 +
   3.806 +lemma admissible_disj' [simp, cont_intro]:
   3.807 +  "\<lbrakk> class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord P; ccpo.admissible lub ord Q \<rbrakk>
   3.808 +  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<or> Q x)"
   3.809 +by(rule ccpo.admissible_disj)
   3.810 +
   3.811 +lemma admissible_imp' [cont_intro]:
   3.812 +  "\<lbrakk> class.ccpo lub ord (mk_less ord);
   3.813 +     ccpo.admissible lub ord (\<lambda>x. \<not> P x);
   3.814 +     ccpo.admissible lub ord (\<lambda>x. Q x) \<rbrakk>
   3.815 +  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x)"
   3.816 +unfolding imp_conv_disj by(rule ccpo.admissible_disj)
   3.817 +
   3.818 +lemma admissible_imp [cont_intro]:
   3.819 +  "(Q \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x))
   3.820 +  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. Q \<longrightarrow> P x)"
   3.821 +by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD)
   3.822 +
   3.823 +lemma admissible_not_mem' [THEN admissible_subst, cont_intro, simp]:
   3.824 +  shows admissible_not_mem: "ccpo.admissible Union op \<subseteq> (\<lambda>A. x \<notin> A)"
   3.825 +by(rule ccpo.admissibleI) auto
   3.826 +
   3.827 +lemma admissible_eqI:
   3.828 +  assumes f: "cont luba orda lub ord (\<lambda>x. f x)"
   3.829 +  and g: "cont luba orda lub ord (\<lambda>x. g x)"
   3.830 +  shows "ccpo.admissible luba orda (\<lambda>x. f x = g x)"
   3.831 +apply(rule ccpo.admissibleI)
   3.832 +apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong)
   3.833 +done
   3.834 +
   3.835 +corollary admissible_eq_mcontI [cont_intro]:
   3.836 +  "\<lbrakk> mcont luba orda lub ord (\<lambda>x. f x); 
   3.837 +    mcont luba orda lub ord (\<lambda>x. g x) \<rbrakk>
   3.838 +  \<Longrightarrow> ccpo.admissible luba orda (\<lambda>x. f x = g x)"
   3.839 +by(rule admissible_eqI)(auto simp add: mcont_def)
   3.840 +
   3.841 +lemma admissible_iff [cont_intro, simp]:
   3.842 +  "\<lbrakk> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x); ccpo.admissible lub ord (\<lambda>x. Q x \<longrightarrow> P x) \<rbrakk>
   3.843 +  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longleftrightarrow> Q x)"
   3.844 +by(subst iff_conv_conj_imp)(rule admissible_conj)
   3.845 +
   3.846 +context ccpo begin
   3.847 +
   3.848 +lemma admissible_leI:
   3.849 +  assumes f: "mcont luba orda Sup op \<le> (\<lambda>x. f x)"
   3.850 +  and g: "mcont luba orda Sup op \<le> (\<lambda>x. g x)"
   3.851 +  shows "ccpo.admissible luba orda (\<lambda>x. f x \<le> g x)"
   3.852 +proof(rule ccpo.admissibleI)
   3.853 +  fix A
   3.854 +  assume chain: "Complete_Partial_Order.chain orda A"
   3.855 +    and le: "\<forall>x\<in>A. f x \<le> g x"
   3.856 +    and False: "A \<noteq> {}"
   3.857 +  have "f (luba A) = \<Squnion>(f ` A)" by(simp add: mcont_contD[OF f] chain False)
   3.858 +  also have "\<dots> \<le> \<Squnion>(g ` A)"
   3.859 +  proof(rule ccpo_Sup_least)
   3.860 +    from chain show "Complete_Partial_Order.chain op \<le> (f ` A)"
   3.861 +      by(rule chain_imageI)(rule mcont_monoD[OF f])
   3.862 +    
   3.863 +    fix x
   3.864 +    assume "x \<in> f ` A"
   3.865 +    then obtain y where "y \<in> A" "x = f y" by blast note this(2)
   3.866 +    also have "f y \<le> g y" using le `y \<in> A` by simp
   3.867 +    also have "Complete_Partial_Order.chain op \<le> (g ` A)"
   3.868 +      using chain by(rule chain_imageI)(rule mcont_monoD[OF g])
   3.869 +    hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: `y \<in> A`)
   3.870 +    finally show "x \<le> \<dots>" .
   3.871 +  qed
   3.872 +  also have "\<dots> = g (luba A)" by(simp add: mcont_contD[OF g] chain False)
   3.873 +  finally show "f (luba A) \<le> g (luba A)" .
   3.874 +qed
   3.875 +
   3.876 +end
   3.877 +
   3.878 +lemma admissible_leI:
   3.879 +  fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or>_" [900] 900)
   3.880 +  assumes "class.ccpo lub op \<sqsubseteq> (mk_less op \<sqsubseteq>)"
   3.881 +  and "mcont luba orda lub op \<sqsubseteq> (\<lambda>x. f x)"
   3.882 +  and "mcont luba orda lub op \<sqsubseteq> (\<lambda>x. g x)"
   3.883 +  shows "ccpo.admissible luba orda (\<lambda>x. f x \<sqsubseteq> g x)"
   3.884 +using assms by(rule ccpo.admissible_leI)
   3.885 +
   3.886 +declare ccpo_class.admissible_leI[cont_intro]
   3.887 +
   3.888 +context ccpo begin
   3.889 +
   3.890 +lemma admissible_not_below: "ccpo.admissible Sup op \<le> (\<lambda>x. \<not> op \<le> x y)"
   3.891 +by(rule ccpo.admissibleI)(simp add: ccpo_Sup_below_iff)
   3.892 +
   3.893 +end
   3.894 +
   3.895 +lemma (in preorder) preorder [cont_intro, simp]: "class.preorder op \<le> (mk_less op \<le>)"
   3.896 +by(unfold_locales)(auto simp add: mk_less_def intro: order_trans)
   3.897 +
   3.898 +context partial_function_definitions begin
   3.899 +
   3.900 +lemmas [cont_intro, simp] =
   3.901 +  admissible_leI[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.902 +  ccpo.admissible_not_below[THEN admissible_subst, OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.903 +
   3.904 +end
   3.905 +
   3.906 +
   3.907 +inductive compact :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   3.908 +  for lub ord x 
   3.909 +where compact:
   3.910 +  "\<lbrakk> ccpo.admissible lub ord (\<lambda>y. \<not> ord x y);
   3.911 +     ccpo.admissible lub ord (\<lambda>y. x \<noteq> y) \<rbrakk>
   3.912 +  \<Longrightarrow> compact lub ord x"
   3.913 +
   3.914 +hide_fact (open) compact
   3.915 +
   3.916 +context ccpo begin
   3.917 +
   3.918 +lemma compactI:
   3.919 +  assumes "ccpo.admissible Sup op \<le> (\<lambda>y. \<not> x \<le> y)"
   3.920 +  shows "compact Sup op \<le> x"
   3.921 +using assms
   3.922 +proof(rule compact.intros)
   3.923 +  have neq: "(\<lambda>y. x \<noteq> y) = (\<lambda>y. \<not> x \<le> y \<or> \<not> y \<le> x)" by(auto)
   3.924 +  show "ccpo.admissible Sup op \<le> (\<lambda>y. x \<noteq> y)"
   3.925 +    by(subst neq)(rule admissible_disj admissible_not_below assms)+
   3.926 +qed
   3.927 +
   3.928 +lemma compact_bot:
   3.929 +  assumes "x = Sup {}"
   3.930 +  shows "compact Sup op \<le> x"
   3.931 +proof(rule compactI)
   3.932 +  show "ccpo.admissible Sup op \<le> (\<lambda>y. \<not> x \<le> y)" using assms
   3.933 +    by(auto intro!: ccpo.admissibleI intro: ccpo_Sup_least chain_empty)
   3.934 +qed
   3.935 +
   3.936 +end
   3.937 +
   3.938 +lemma admissible_compact_neq' [THEN admissible_subst, cont_intro, simp]:
   3.939 +  shows admissible_compact_neq: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. k \<noteq> x)"
   3.940 +by(simp add: compact.simps)
   3.941 +
   3.942 +lemma admissible_neq_compact' [THEN admissible_subst, cont_intro, simp]:
   3.943 +  shows admissible_neq_compact: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. x \<noteq> k)"
   3.944 +by(subst eq_commute)(rule admissible_compact_neq)
   3.945 +
   3.946 +context partial_function_definitions begin
   3.947 +
   3.948 +lemmas [cont_intro, simp] = ccpo.compact_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
   3.949 +
   3.950 +end
   3.951 +
   3.952 +context ccpo begin
   3.953 +
   3.954 +lemma fixp_strong_induct:
   3.955 +  assumes [cont_intro]: "ccpo.admissible Sup op \<le> P"
   3.956 +  and mono: "monotone op \<le> op \<le> f"
   3.957 +  and bot: "P (\<Squnion>{})"
   3.958 +  and step: "\<And>x. \<lbrakk> x \<le> ccpo_class.fixp f; P x \<rbrakk> \<Longrightarrow> P (f x)"
   3.959 +  shows "P (ccpo_class.fixp f)"
   3.960 +proof(rule fixp_induct[where P="\<lambda>x. x \<le> ccpo_class.fixp f \<and> P x", THEN conjunct2])
   3.961 +  note [cont_intro] = admissible_leI
   3.962 +  show "ccpo.admissible Sup op \<le> (\<lambda>x. x \<le> ccpo_class.fixp f \<and> P x)" by simp
   3.963 +next
   3.964 +  show "\<Squnion>{} \<le> ccpo_class.fixp f \<and> P (\<Squnion>{})"
   3.965 +    by(auto simp add: bot intro: ccpo_Sup_least chain_empty)
   3.966 +next
   3.967 +  fix x
   3.968 +  assume "x \<le> ccpo_class.fixp f \<and> P x"
   3.969 +  thus "f x \<le> ccpo_class.fixp f \<and> P (f x)"
   3.970 +    by(subst fixp_unfold[OF mono])(auto dest: monotoneD[OF mono] intro: step)
   3.971 +qed(rule mono)
   3.972 +
   3.973 +end
   3.974 +
   3.975 +context partial_function_definitions begin
   3.976 +
   3.977 +lemma fixp_strong_induct_uc:
   3.978 +  fixes F :: "'c \<Rightarrow> 'c"
   3.979 +    and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a"
   3.980 +    and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
   3.981 +    and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
   3.982 +  assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
   3.983 +    and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
   3.984 +    and inverse: "\<And>f. U (C f) = f"
   3.985 +    and adm: "ccpo.admissible lub_fun le_fun P"
   3.986 +    and bot: "P (\<lambda>_. lub {})"
   3.987 +    and step: "\<And>f'. \<lbrakk> P (U f'); le_fun (U f') (U f) \<rbrakk> \<Longrightarrow> P (U (F f'))"
   3.988 +  shows "P (U f)"
   3.989 +unfolding eq inverse
   3.990 +apply (rule ccpo.fixp_strong_induct[OF ccpo adm])
   3.991 +apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
   3.992 +apply (rule_tac f'5="C x" in step)
   3.993 +apply (simp_all add: inverse eq)
   3.994 +done
   3.995 +
   3.996 +end
   3.997 +
   3.998 +subsection {* @{term "op ="} as order *}
   3.999 +
  3.1000 +definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool"
  3.1001 +where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
  3.1002 +
  3.1003 +definition the_Sup :: "'a set \<Rightarrow> 'a"
  3.1004 +where "the_Sup A = (THE a. a \<in> A)"
  3.1005 +
  3.1006 +lemma lub_singleton_the_Sup [cont_intro, simp]: "lub_singleton the_Sup"
  3.1007 +by(simp add: lub_singleton_def the_Sup_def)
  3.1008 +
  3.1009 +lemma (in ccpo) lub_singleton: "lub_singleton Sup"
  3.1010 +by(simp add: lub_singleton_def)
  3.1011 +
  3.1012 +lemma (in partial_function_definitions) lub_singleton [cont_intro, simp]: "lub_singleton lub"
  3.1013 +by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
  3.1014 +
  3.1015 +lemma preorder_eq [cont_intro, simp]:
  3.1016 +  "class.preorder op = (mk_less op =)"
  3.1017 +by(unfold_locales)(simp_all add: mk_less_def)
  3.1018 +
  3.1019 +lemma monotone_eqI [cont_intro]:
  3.1020 +  assumes "class.preorder ord (mk_less ord)"
  3.1021 +  shows "monotone op = ord f"
  3.1022 +proof -
  3.1023 +  interpret preorder ord "mk_less ord" by fact
  3.1024 +  show ?thesis by(simp add: monotone_def)
  3.1025 +qed
  3.1026 +
  3.1027 +lemma cont_eqI [cont_intro]: 
  3.1028 +  fixes f :: "'a \<Rightarrow> 'b"
  3.1029 +  assumes "lub_singleton lub"
  3.1030 +  shows "cont the_Sup op = lub ord f"
  3.1031 +proof(rule contI)
  3.1032 +  fix Y :: "'a set"
  3.1033 +  assume "Complete_Partial_Order.chain op = Y" "Y \<noteq> {}"
  3.1034 +  then obtain a where "Y = {a}" by(auto simp add: chain_def)
  3.1035 +  thus "f (the_Sup Y) = lub (f ` Y)" using assms
  3.1036 +    by(simp add: the_Sup_def lub_singleton_def)
  3.1037 +qed
  3.1038 +
  3.1039 +lemma mcont_eqI [cont_intro, simp]:
  3.1040 +  "\<lbrakk> class.preorder ord (mk_less ord); lub_singleton lub \<rbrakk>
  3.1041 +  \<Longrightarrow> mcont the_Sup op = lub ord f"
  3.1042 +by(simp add: mcont_def cont_eqI monotone_eqI)
  3.1043 +
  3.1044 +subsection {* ccpo for products *}
  3.1045 +
  3.1046 +definition prod_lub :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b"
  3.1047 +where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
  3.1048 +
  3.1049 +lemma lub_singleton_prod_lub [cont_intro, simp]:
  3.1050 +  "\<lbrakk> lub_singleton luba; lub_singleton lubb \<rbrakk> \<Longrightarrow> lub_singleton (prod_lub luba lubb)"
  3.1051 +by(simp add: lub_singleton_def prod_lub_def)
  3.1052 +
  3.1053 +lemma prod_lub_empty [simp]: "prod_lub luba lubb {} = (luba {}, lubb {})"
  3.1054 +by(simp add: prod_lub_def)
  3.1055 +
  3.1056 +lemma preorder_rel_prodI [cont_intro, simp]:
  3.1057 +  assumes "class.preorder orda (mk_less orda)"
  3.1058 +  and "class.preorder ordb (mk_less ordb)"
  3.1059 +  shows "class.preorder (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
  3.1060 +proof -
  3.1061 +  interpret a: preorder orda "mk_less orda" by fact
  3.1062 +  interpret b: preorder ordb "mk_less ordb" by fact
  3.1063 +  show ?thesis by(unfold_locales)(auto simp add: mk_less_def intro: a.order_trans b.order_trans)
  3.1064 +qed
  3.1065 +
  3.1066 +lemma order_rel_prodI:
  3.1067 +  assumes a: "class.order orda (mk_less orda)"
  3.1068 +  and b: "class.order ordb (mk_less ordb)"
  3.1069 +  shows "class.order (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
  3.1070 +  (is "class.order ?ord ?ord'")
  3.1071 +proof(intro class.order.intro class.order_axioms.intro)
  3.1072 +  interpret a: order orda "mk_less orda" by(fact a)
  3.1073 +  interpret b: order ordb "mk_less ordb" by(fact b)
  3.1074 +  show "class.preorder ?ord ?ord'" by(rule preorder_rel_prodI) unfold_locales
  3.1075 +
  3.1076 +  fix x y
  3.1077 +  assume "?ord x y" "?ord y x"
  3.1078 +  thus "x = y" by(cases x y rule: prod.exhaust[case_product prod.exhaust]) auto
  3.1079 +qed
  3.1080 +
  3.1081 +lemma monotone_rel_prodI:
  3.1082 +  assumes mono2: "\<And>a. monotone ordb ordc (\<lambda>b. f (a, b))"
  3.1083 +  and mono1: "\<And>b. monotone orda ordc (\<lambda>a. f (a, b))"
  3.1084 +  and a: "class.preorder orda (mk_less orda)"
  3.1085 +  and b: "class.preorder ordb (mk_less ordb)"
  3.1086 +  and c: "class.preorder ordc (mk_less ordc)"
  3.1087 +  shows "monotone (rel_prod orda ordb) ordc f"
  3.1088 +proof -
  3.1089 +  interpret a: preorder orda "mk_less orda" by(rule a)
  3.1090 +  interpret b: preorder ordb "mk_less ordb" by(rule b)
  3.1091 +  interpret c: preorder ordc "mk_less ordc" by(rule c)
  3.1092 +  show ?thesis using mono2 mono1
  3.1093 +    by(auto 7 2 simp add: monotone_def intro: c.order_trans)
  3.1094 +qed
  3.1095 +
  3.1096 +lemma monotone_rel_prodD1:
  3.1097 +  assumes mono: "monotone (rel_prod orda ordb) ordc f"
  3.1098 +  and preorder: "class.preorder ordb (mk_less ordb)"
  3.1099 +  shows "monotone orda ordc (\<lambda>a. f (a, b))"
  3.1100 +proof -
  3.1101 +  interpret preorder ordb "mk_less ordb" by(rule preorder)
  3.1102 +  show ?thesis using mono by(simp add: monotone_def)
  3.1103 +qed
  3.1104 +
  3.1105 +lemma monotone_rel_prodD2:
  3.1106 +  assumes mono: "monotone (rel_prod orda ordb) ordc f"
  3.1107 +  and preorder: "class.preorder orda (mk_less orda)"
  3.1108 +  shows "monotone ordb ordc (\<lambda>b. f (a, b))"
  3.1109 +proof -
  3.1110 +  interpret preorder orda "mk_less orda" by(rule preorder)
  3.1111 +  show ?thesis using mono by(simp add: monotone_def)
  3.1112 +qed
  3.1113 +
  3.1114 +lemma monotone_case_prodI:
  3.1115 +  "\<lbrakk> \<And>a. monotone ordb ordc (f a); \<And>b. monotone orda ordc (\<lambda>a. f a b);
  3.1116 +    class.preorder orda (mk_less orda); class.preorder ordb (mk_less ordb);
  3.1117 +    class.preorder ordc (mk_less ordc) \<rbrakk>
  3.1118 +  \<Longrightarrow> monotone (rel_prod orda ordb) ordc (case_prod f)"
  3.1119 +by(rule monotone_rel_prodI) simp_all
  3.1120 +
  3.1121 +lemma monotone_case_prodD1:
  3.1122 +  assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
  3.1123 +  and preorder: "class.preorder ordb (mk_less ordb)"
  3.1124 +  shows "monotone orda ordc (\<lambda>a. f a b)"
  3.1125 +using monotone_rel_prodD1[OF assms] by simp
  3.1126 +
  3.1127 +lemma monotone_case_prodD2:
  3.1128 +  assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
  3.1129 +  and preorder: "class.preorder orda (mk_less orda)"
  3.1130 +  shows "monotone ordb ordc (f a)"
  3.1131 +using monotone_rel_prodD2[OF assms] by simp
  3.1132 +
  3.1133 +context 
  3.1134 +  fixes orda ordb ordc
  3.1135 +  assumes a: "class.preorder orda (mk_less orda)"
  3.1136 +  and b: "class.preorder ordb (mk_less ordb)"
  3.1137 +  and c: "class.preorder ordc (mk_less ordc)"
  3.1138 +begin
  3.1139 +
  3.1140 +lemma monotone_rel_prod_iff:
  3.1141 +  "monotone (rel_prod orda ordb) ordc f \<longleftrightarrow>
  3.1142 +   (\<forall>a. monotone ordb ordc (\<lambda>b. f (a, b))) \<and> 
  3.1143 +   (\<forall>b. monotone orda ordc (\<lambda>a. f (a, b)))"
  3.1144 +using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2)
  3.1145 +
  3.1146 +lemma monotone_case_prod_iff [simp]:
  3.1147 +  "monotone (rel_prod orda ordb) ordc (case_prod f) \<longleftrightarrow>
  3.1148 +   (\<forall>a. monotone ordb ordc (f a)) \<and> (\<forall>b. monotone orda ordc (\<lambda>a. f a b))"
  3.1149 +by(simp add: monotone_rel_prod_iff)
  3.1150 +
  3.1151 +end
  3.1152 +
  3.1153 +lemma monotone_case_prod_apply_iff:
  3.1154 +  "monotone orda ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
  3.1155 +by(simp add: monotone_def)
  3.1156 +
  3.1157 +lemma monotone_case_prod_applyD:
  3.1158 +  "monotone orda ordb (\<lambda>x. (case_prod f x) y)
  3.1159 +  \<Longrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
  3.1160 +by(simp add: monotone_case_prod_apply_iff)
  3.1161 +
  3.1162 +lemma monotone_case_prod_applyI:
  3.1163 +  "monotone orda ordb (case_prod (\<lambda>a b. f a b y))
  3.1164 +  \<Longrightarrow> monotone orda ordb (\<lambda>x. (case_prod f x) y)"
  3.1165 +by(simp add: monotone_case_prod_apply_iff)
  3.1166 +
  3.1167 +
  3.1168 +lemma cont_case_prod_apply_iff:
  3.1169 +  "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))"
  3.1170 +by(simp add: cont_def split_def)
  3.1171 +
  3.1172 +lemma cont_case_prod_applyI:
  3.1173 +  "cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))
  3.1174 +  \<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)"
  3.1175 +by(simp add: cont_case_prod_apply_iff)
  3.1176 +
  3.1177 +lemma cont_case_prod_applyD:
  3.1178 +  "cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)
  3.1179 +  \<Longrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
  3.1180 +by(simp add: cont_case_prod_apply_iff)
  3.1181 +
  3.1182 +lemma mcont_case_prod_apply_iff [simp]:
  3.1183 +  "mcont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> 
  3.1184 +   mcont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
  3.1185 +by(simp add: mcont_def monotone_case_prod_apply_iff cont_case_prod_apply_iff)
  3.1186 +
  3.1187 +lemma cont_prodD1: 
  3.1188 +  assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f"
  3.1189 +  and "class.preorder orda (mk_less orda)"
  3.1190 +  and luba: "lub_singleton luba"
  3.1191 +  shows "cont lubb ordb lubc ordc (\<lambda>y. f (x, y))"
  3.1192 +proof(rule contI)
  3.1193 +  interpret preorder orda "mk_less orda" by fact
  3.1194 +
  3.1195 +  fix Y :: "'b set"
  3.1196 +  let ?Y = "{x} \<times> Y"
  3.1197 +  assume "Complete_Partial_Order.chain ordb Y" "Y \<noteq> {}"
  3.1198 +  hence "Complete_Partial_Order.chain (rel_prod orda ordb) ?Y" "?Y \<noteq> {}" 
  3.1199 +    by(simp_all add: chain_def)
  3.1200 +  with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
  3.1201 +  moreover have "f ` ?Y = (\<lambda>y. f (x, y)) ` Y" by auto
  3.1202 +  ultimately show "f (x, lubb Y) = lubc ((\<lambda>y. f (x, y)) ` Y)" using luba
  3.1203 +    by(simp add: prod_lub_def `Y \<noteq> {}` lub_singleton_def)
  3.1204 +qed
  3.1205 +
  3.1206 +lemma cont_prodD2: 
  3.1207 +  assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f"
  3.1208 +  and "class.preorder ordb (mk_less ordb)"
  3.1209 +  and lubb: "lub_singleton lubb"
  3.1210 +  shows "cont luba orda lubc ordc (\<lambda>x. f (x, y))"
  3.1211 +proof(rule contI)
  3.1212 +  interpret preorder ordb "mk_less ordb" by fact
  3.1213 +
  3.1214 +  fix Y
  3.1215 +  assume Y: "Complete_Partial_Order.chain orda Y" "Y \<noteq> {}"
  3.1216 +  let ?Y = "Y \<times> {y}"
  3.1217 +  have "f (luba Y, y) = f (prod_lub luba lubb ?Y)"
  3.1218 +    using lubb by(simp add: prod_lub_def Y lub_singleton_def)
  3.1219 +  also from Y have "Complete_Partial_Order.chain (rel_prod orda ordb) ?Y" "?Y \<noteq> {}"
  3.1220 +    by(simp_all add: chain_def)
  3.1221 +  with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
  3.1222 +  also have "f ` ?Y = (\<lambda>x. f (x, y)) ` Y" by auto
  3.1223 +  finally show "f (luba Y, y) = lubc \<dots>" .
  3.1224 +qed
  3.1225 +
  3.1226 +lemma cont_case_prodD1:
  3.1227 +  assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)"
  3.1228 +  and "class.preorder orda (mk_less orda)"
  3.1229 +  and "lub_singleton luba"
  3.1230 +  shows "cont lubb ordb lubc ordc (f x)"
  3.1231 +using cont_prodD1[OF assms] by simp
  3.1232 +
  3.1233 +lemma cont_case_prodD2:
  3.1234 +  assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)"
  3.1235 +  and "class.preorder ordb (mk_less ordb)"
  3.1236 +  and "lub_singleton lubb"
  3.1237 +  shows "cont luba orda lubc ordc (\<lambda>x. f x y)"
  3.1238 +using cont_prodD2[OF assms] by simp
  3.1239 +
  3.1240 +context ccpo begin
  3.1241 +
  3.1242 +lemma cont_prodI: 
  3.1243 +  assumes mono: "monotone (rel_prod orda ordb) op \<le> f"
  3.1244 +  and cont1: "\<And>x. cont lubb ordb Sup op \<le> (\<lambda>y. f (x, y))"
  3.1245 +  and cont2: "\<And>y. cont luba orda Sup op \<le> (\<lambda>x. f (x, y))"
  3.1246 +  and "class.preorder orda (mk_less orda)"
  3.1247 +  and "class.preorder ordb (mk_less ordb)"
  3.1248 +  shows "cont (prod_lub luba lubb) (rel_prod orda ordb) Sup op \<le> f"
  3.1249 +proof(rule contI)
  3.1250 +  interpret a: preorder orda "mk_less orda" by fact 
  3.1251 +  interpret b: preorder ordb "mk_less ordb" by fact
  3.1252 +  
  3.1253 +  fix Y
  3.1254 +  assume chain: "Complete_Partial_Order.chain (rel_prod orda ordb) Y"
  3.1255 +    and "Y \<noteq> {}"
  3.1256 +  have "f (prod_lub luba lubb Y) = f (luba (fst ` Y), lubb (snd ` Y))"
  3.1257 +    by(simp add: prod_lub_def)
  3.1258 +  also from cont2 have "f (luba (fst ` Y), lubb (snd ` Y)) = \<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y)"
  3.1259 +    by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] `Y \<noteq> {}`)
  3.1260 +  also from cont1 have "\<And>x. f (x, lubb (snd ` Y)) = \<Squnion>((\<lambda>y. f (x, y)) ` snd ` Y)"
  3.1261 +    by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] `Y \<noteq> {}`)
  3.1262 +  hence "\<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y) = \<Squnion>((\<lambda>x. \<dots> x) ` fst ` Y)" by simp
  3.1263 +  also have "\<dots> = \<Squnion>((\<lambda>x. f (fst x, snd x)) ` Y)"
  3.1264 +    unfolding image_image split_def using chain
  3.1265 +    apply(rule diag_Sup)
  3.1266 +    using monotoneD[OF mono]
  3.1267 +    by(auto intro: monotoneI)
  3.1268 +  finally show "f (prod_lub luba lubb Y) = \<Squnion>(f ` Y)" by simp
  3.1269 +qed
  3.1270 +
  3.1271 +lemma cont_case_prodI:
  3.1272 +  assumes "monotone (rel_prod orda ordb) op \<le> (case_prod f)"
  3.1273 +  and "\<And>x. cont lubb ordb Sup op \<le> (\<lambda>y. f x y)"
  3.1274 +  and "\<And>y. cont luba orda Sup op \<le> (\<lambda>x. f x y)"
  3.1275 +  and "class.preorder orda (mk_less orda)"
  3.1276 +  and "class.preorder ordb (mk_less ordb)"
  3.1277 +  shows "cont (prod_lub luba lubb) (rel_prod orda ordb) Sup op \<le> (case_prod f)"
  3.1278 +by(rule cont_prodI)(simp_all add: assms)
  3.1279 +
  3.1280 +lemma cont_case_prod_iff:
  3.1281 +  "\<lbrakk> monotone (rel_prod orda ordb) op \<le> (case_prod f);
  3.1282 +     class.preorder orda (mk_less orda); lub_singleton luba;
  3.1283 +     class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
  3.1284 +  \<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) Sup op \<le> (case_prod f) \<longleftrightarrow>
  3.1285 +   (\<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))"
  3.1286 +by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
  3.1287 +
  3.1288 +end
  3.1289 +
  3.1290 +context partial_function_definitions begin
  3.1291 +
  3.1292 +lemma mono2mono2:
  3.1293 +  assumes f: "monotone (rel_prod ordb ordc) leq (\<lambda>(x, y). f x y)"
  3.1294 +  and t: "monotone orda ordb (\<lambda>x. t x)"
  3.1295 +  and t': "monotone orda ordc (\<lambda>x. t' x)"
  3.1296 +  shows "monotone orda leq (\<lambda>x. f (t x) (t' x))"
  3.1297 +proof(rule monotoneI)
  3.1298 +  fix x y
  3.1299 +  assume "orda x y"
  3.1300 +  hence "rel_prod ordb ordc (t x, t' x) (t y, t' y)"
  3.1301 +    using t t' by(auto dest: monotoneD)
  3.1302 +  from monotoneD[OF f this] show "leq (f (t x) (t' x)) (f (t y) (t' y))" by simp
  3.1303 +qed
  3.1304 +
  3.1305 +lemma cont_case_prodI [cont_intro]:
  3.1306 +  "\<lbrakk> monotone (rel_prod orda ordb) leq (case_prod f);
  3.1307 +    \<And>x. cont lubb ordb lub leq (\<lambda>y. f x y);
  3.1308 +    \<And>y. cont luba orda lub leq (\<lambda>x. f x y);
  3.1309 +    class.preorder orda (mk_less orda);
  3.1310 +    class.preorder ordb (mk_less ordb) \<rbrakk>
  3.1311 +  \<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f)"
  3.1312 +by(rule ccpo.cont_case_prodI)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
  3.1313 +
  3.1314 +lemma cont_case_prod_iff:
  3.1315 +  "\<lbrakk> monotone (rel_prod orda ordb) leq (case_prod f);
  3.1316 +     class.preorder orda (mk_less orda); lub_singleton luba;
  3.1317 +     class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
  3.1318 +  \<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
  3.1319 +   (\<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))"
  3.1320 +by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
  3.1321 +
  3.1322 +lemma mcont_case_prod_iff [simp]:
  3.1323 +  "\<lbrakk> class.preorder orda (mk_less orda); lub_singleton luba;
  3.1324 +     class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
  3.1325 +  \<Longrightarrow> mcont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
  3.1326 +   (\<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))"
  3.1327 +unfolding mcont_def by(auto simp add: cont_case_prod_iff)
  3.1328 +
  3.1329 +end
  3.1330 +
  3.1331 +lemma mono2mono_case_prod [cont_intro]:
  3.1332 +  assumes "\<And>x y. monotone orda ordb (\<lambda>f. pair f x y)"
  3.1333 +  shows "monotone orda ordb (\<lambda>f. case_prod (pair f) x)"
  3.1334 +by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
  3.1335 +
  3.1336 +subsection {* Complete lattices as ccpo *}
  3.1337 +
  3.1338 +context complete_lattice begin
  3.1339 +
  3.1340 +lemma complete_lattice_ccpo: "class.ccpo Sup op \<le> op <"
  3.1341 +by(unfold_locales)(fast intro: Sup_upper Sup_least)+
  3.1342 +
  3.1343 +lemma complete_lattice_ccpo': "class.ccpo Sup op \<le> (mk_less op \<le>)"
  3.1344 +by(unfold_locales)(auto simp add: mk_less_def intro: Sup_upper Sup_least)
  3.1345 +
  3.1346 +lemma complete_lattice_partial_function_definitions: 
  3.1347 +  "partial_function_definitions op \<le> Sup"
  3.1348 +by(unfold_locales)(auto intro: Sup_least Sup_upper)
  3.1349 +
  3.1350 +lemma complete_lattice_partial_function_definitions_dual:
  3.1351 +  "partial_function_definitions op \<ge> Inf"
  3.1352 +by(unfold_locales)(auto intro: Inf_lower Inf_greatest)
  3.1353 +
  3.1354 +lemmas [cont_intro, simp] =
  3.1355 +  Partial_Function.ccpo[OF complete_lattice_partial_function_definitions]
  3.1356 +  Partial_Function.ccpo[OF complete_lattice_partial_function_definitions_dual]
  3.1357 +
  3.1358 +lemma mono2mono_inf:
  3.1359 +  assumes f: "monotone ord op \<le> (\<lambda>x. f x)" 
  3.1360 +  and g: "monotone ord op \<le> (\<lambda>x. g x)"
  3.1361 +  shows "monotone ord op \<le> (\<lambda>x. f x \<sqinter> g x)"
  3.1362 +by(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] intro: le_infI1 le_infI2 intro!: monotoneI)
  3.1363 +
  3.1364 +lemma mcont_const [simp]: "mcont lub ord Sup op \<le> (\<lambda>_. c)"
  3.1365 +by(rule ccpo.mcont_const[OF complete_lattice_ccpo])
  3.1366 +
  3.1367 +lemma mono2mono_sup:
  3.1368 +  assumes f: "monotone ord op \<le> (\<lambda>x. f x)"
  3.1369 +  and g: "monotone ord op \<le> (\<lambda>x. g x)"
  3.1370 +  shows "monotone ord op \<le> (\<lambda>x. f x \<squnion> g x)"
  3.1371 +by(auto 4 3 intro!: monotoneI intro: sup.coboundedI1 sup.coboundedI2 dest: monotoneD[OF f] monotoneD[OF g])
  3.1372 +
  3.1373 +lemma Sup_image_sup: 
  3.1374 +  assumes "Y \<noteq> {}"
  3.1375 +  shows "\<Squnion>(op \<squnion> x ` Y) = x \<squnion> \<Squnion>Y"
  3.1376 +proof(rule Sup_eqI)
  3.1377 +  fix y
  3.1378 +  assume "y \<in> op \<squnion> x ` Y"
  3.1379 +  then obtain z where "y = x \<squnion> z" and "z \<in> Y" by blast
  3.1380 +  from `z \<in> Y` have "z \<le> \<Squnion>Y" by(rule Sup_upper)
  3.1381 +  with _ show "y \<le> x \<squnion> \<Squnion>Y" unfolding `y = x \<squnion> z` by(rule sup_mono) simp
  3.1382 +next
  3.1383 +  fix y
  3.1384 +  assume upper: "\<And>z. z \<in> op \<squnion> x ` Y \<Longrightarrow> z \<le> y"
  3.1385 +  show "x \<squnion> \<Squnion>Y \<le> y" unfolding Sup_insert[symmetric]
  3.1386 +  proof(rule Sup_least)
  3.1387 +    fix z
  3.1388 +    assume "z \<in> insert x Y"
  3.1389 +    from assms obtain z' where "z' \<in> Y" by blast
  3.1390 +    let ?z = "if z \<in> Y then x \<squnion> z else x \<squnion> z'"
  3.1391 +    have "z \<le> x \<squnion> ?z" using `z' \<in> Y` `z \<in> insert x Y` by auto
  3.1392 +    also have "\<dots> \<le> y" by(rule upper)(auto split: if_split_asm intro: `z' \<in> Y`)
  3.1393 +    finally show "z \<le> y" .
  3.1394 +  qed
  3.1395 +qed
  3.1396 +
  3.1397 +lemma mcont_sup1: "mcont Sup op \<le> Sup op \<le> (\<lambda>y. x \<squnion> y)"
  3.1398 +by(auto 4 3 simp add: mcont_def sup.coboundedI1 sup.coboundedI2 intro!: monotoneI contI intro: Sup_image_sup[symmetric])
  3.1399 +
  3.1400 +lemma mcont_sup2: "mcont Sup op \<le> Sup op \<le> (\<lambda>x. x \<squnion> y)"
  3.1401 +by(subst sup_commute)(rule mcont_sup1)
  3.1402 +
  3.1403 +lemma mcont2mcont_sup [cont_intro, simp]:
  3.1404 +  "\<lbrakk> mcont lub ord Sup op \<le> (\<lambda>x. f x);
  3.1405 +     mcont lub ord Sup op \<le> (\<lambda>x. g x) \<rbrakk>
  3.1406 +  \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f x \<squnion> g x)"
  3.1407 +by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_sup1 mcont_sup2 ccpo.mcont_const[OF complete_lattice_ccpo])
  3.1408 +
  3.1409 +end
  3.1410 +
  3.1411 +lemmas [cont_intro] = admissible_leI[OF complete_lattice_ccpo']
  3.1412 +
  3.1413 +context complete_distrib_lattice begin
  3.1414 +
  3.1415 +lemma mcont_inf1: "mcont Sup op \<le> Sup op \<le> (\<lambda>y. x \<sqinter> y)"
  3.1416 +by(auto intro: monotoneI contI simp add: le_infI2 inf_Sup mcont_def)
  3.1417 +
  3.1418 +lemma mcont_inf2: "mcont Sup op \<le> Sup op \<le> (\<lambda>x. x \<sqinter> y)"
  3.1419 +by(auto intro: monotoneI contI simp add: le_infI1 Sup_inf mcont_def)
  3.1420 +
  3.1421 +lemma mcont2mcont_inf [cont_intro, simp]:
  3.1422 +  "\<lbrakk> mcont lub ord Sup op \<le> (\<lambda>x. f x);
  3.1423 +    mcont lub ord Sup op \<le> (\<lambda>x. g x) \<rbrakk>
  3.1424 +  \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f x \<sqinter> g x)"
  3.1425 +by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_inf1 mcont_inf2 ccpo.mcont_const[OF complete_lattice_ccpo])
  3.1426 +
  3.1427 +end
  3.1428 +
  3.1429 +interpretation lfp: partial_function_definitions "op \<le> :: _ :: complete_lattice \<Rightarrow> _" Sup
  3.1430 +by(rule complete_lattice_partial_function_definitions)
  3.1431 +
  3.1432 +declaration {* Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body}
  3.1433 +  @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE *}
  3.1434 +
  3.1435 +interpretation gfp: partial_function_definitions "op \<ge> :: _ :: complete_lattice \<Rightarrow> _" Inf
  3.1436 +by(rule complete_lattice_partial_function_definitions_dual)
  3.1437 +
  3.1438 +declaration {* Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body}
  3.1439 +  @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE *}
  3.1440 +
  3.1441 +lemma insert_mono [partial_function_mono]:
  3.1442 +   "monotone (fun_ord op \<subseteq>) op \<subseteq> A \<Longrightarrow> monotone (fun_ord op \<subseteq>) op \<subseteq> (\<lambda>y. insert x (A y))"
  3.1443 +by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
  3.1444 +
  3.1445 +lemma mono2mono_insert [THEN lfp.mono2mono, cont_intro, simp]:
  3.1446 +  shows monotone_insert: "monotone op \<subseteq> op \<subseteq> (insert x)"
  3.1447 +by(rule monotoneI) blast
  3.1448 +
  3.1449 +lemma mcont2mcont_insert[THEN lfp.mcont2mcont, cont_intro, simp]:
  3.1450 +  shows mcont_insert: "mcont Union op \<subseteq> Union op \<subseteq> (insert x)"
  3.1451 +by(blast intro: mcontI contI monotone_insert)
  3.1452 +
  3.1453 +lemma mono2mono_image [THEN lfp.mono2mono, cont_intro, simp]:
  3.1454 +  shows monotone_image: "monotone op \<subseteq> op \<subseteq> (op ` f)"
  3.1455 +by(rule monotoneI) blast
  3.1456 +
  3.1457 +lemma cont_image: "cont Union op \<subseteq> Union op \<subseteq> (op ` f)"
  3.1458 +by(rule contI)(auto)
  3.1459 +
  3.1460 +lemma mcont2mcont_image [THEN lfp.mcont2mcont, cont_intro, simp]:
  3.1461 +  shows mcont_image: "mcont Union op \<subseteq> Union op \<subseteq> (op ` f)"
  3.1462 +by(blast intro: mcontI monotone_image cont_image)
  3.1463 +
  3.1464 +context complete_lattice begin
  3.1465 +
  3.1466 +lemma monotone_Sup [cont_intro, simp]:
  3.1467 +  "monotone ord op \<subseteq> f \<Longrightarrow> monotone ord op \<le> (\<lambda>x. \<Squnion>f x)"
  3.1468 +by(blast intro: monotoneI Sup_least Sup_upper dest: monotoneD)
  3.1469 +
  3.1470 +lemma cont_Sup:
  3.1471 +  assumes "cont lub ord Union op \<subseteq> f"
  3.1472 +  shows "cont lub ord Sup op \<le> (\<lambda>x. \<Squnion>f x)"
  3.1473 +apply(rule contI)
  3.1474 +apply(simp add: contD[OF assms])
  3.1475 +apply(blast intro: Sup_least Sup_upper order_trans antisym)
  3.1476 +done
  3.1477 +
  3.1478 +lemma mcont_Sup: "mcont lub ord Union op \<subseteq> f \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. \<Squnion>f x)"
  3.1479 +unfolding mcont_def by(blast intro: monotone_Sup cont_Sup)
  3.1480 +
  3.1481 +lemma monotone_SUP:
  3.1482 +  "\<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)"
  3.1483 +by(rule monotoneI)(blast dest: monotoneD intro: Sup_upper order_trans intro!: Sup_least)
  3.1484 +
  3.1485 +lemma monotone_SUP2:
  3.1486 +  "(\<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)"
  3.1487 +by(rule monotoneI)(blast intro: Sup_upper order_trans dest: monotoneD intro!: Sup_least)
  3.1488 +
  3.1489 +lemma cont_SUP:
  3.1490 +  assumes f: "mcont lub ord Union op \<subseteq> f"
  3.1491 +  and g: "\<And>y. mcont lub ord Sup op \<le> (\<lambda>x. g x y)"
  3.1492 +  shows "cont lub ord Sup op \<le> (\<lambda>x. \<Squnion>y\<in>f x. g x y)"
  3.1493 +proof(rule contI)
  3.1494 +  fix Y
  3.1495 +  assume chain: "Complete_Partial_Order.chain ord Y"
  3.1496 +    and Y: "Y \<noteq> {}"
  3.1497 +  show "\<Squnion>(g (lub Y) ` f (lub Y)) = \<Squnion>((\<lambda>x. \<Squnion>(g x ` f x)) ` Y)" (is "?lhs = ?rhs")
  3.1498 +  proof(rule antisym)
  3.1499 +    show "?lhs \<le> ?rhs"
  3.1500 +    proof(rule Sup_least)
  3.1501 +      fix x
  3.1502 +      assume "x \<in> g (lub Y) ` f (lub Y)"
  3.1503 +      with mcont_contD[OF f chain Y] mcont_contD[OF g chain Y]
  3.1504 +      obtain y z where "y \<in> Y" "z \<in> f y"
  3.1505 +        and x: "x = \<Squnion>((\<lambda>x. g x z) ` Y)" by auto
  3.1506 +      show "x \<le> ?rhs" unfolding x
  3.1507 +      proof(rule Sup_least)
  3.1508 +        fix u
  3.1509 +        assume "u \<in> (\<lambda>x. g x z) ` Y"
  3.1510 +        then obtain y' where "u = g y' z" "y' \<in> Y" by auto
  3.1511 +        from chain `y \<in> Y` `y' \<in> Y` have "ord y y' \<or> ord y' y" by(rule chainD)
  3.1512 +        thus "u \<le> ?rhs"
  3.1513 +        proof
  3.1514 +          note `u = g y' z` also
  3.1515 +          assume "ord y y'"
  3.1516 +          with f have "f y \<subseteq> f y'" by(rule mcont_monoD)
  3.1517 +          with `z \<in> f y`
  3.1518 +          have "g y' z \<le> \<Squnion>(g y' ` f y')" by(auto intro: Sup_upper)
  3.1519 +          also have "\<dots> \<le> ?rhs" using `y' \<in> Y` by(auto intro: Sup_upper)
  3.1520 +          finally show ?thesis .
  3.1521 +        next
  3.1522 +          note `u = g y' z` also
  3.1523 +          assume "ord y' y"
  3.1524 +          with g have "g y' z \<le> g y z" by(rule mcont_monoD)
  3.1525 +          also have "\<dots> \<le> \<Squnion>(g y ` f y)" using `z \<in> f y`
  3.1526 +            by(auto intro: Sup_upper)
  3.1527 +          also have "\<dots> \<le> ?rhs" using `y \<in> Y` by(auto intro: Sup_upper)
  3.1528 +          finally show ?thesis .
  3.1529 +        qed
  3.1530 +      qed
  3.1531 +    qed
  3.1532 +  next
  3.1533 +    show "?rhs \<le> ?lhs"
  3.1534 +    proof(rule Sup_least)
  3.1535 +      fix x
  3.1536 +      assume "x \<in> (\<lambda>x. \<Squnion>(g x ` f x)) ` Y"
  3.1537 +      then obtain y where x: "x = \<Squnion>(g y ` f y)" and "y \<in> Y" by auto
  3.1538 +      show "x \<le> ?lhs" unfolding x
  3.1539 +      proof(rule Sup_least)
  3.1540 +        fix u
  3.1541 +        assume "u \<in> g y ` f y"
  3.1542 +        then obtain z where "u = g y z" "z \<in> f y" by auto
  3.1543 +        note `u = g y z`
  3.1544 +        also have "g y z \<le> \<Squnion>((\<lambda>x. g x z) ` Y)"
  3.1545 +          using `y \<in> Y` by(auto intro: Sup_upper)
  3.1546 +        also have "\<dots> = g (lub Y) z" by(simp add: mcont_contD[OF g chain Y])
  3.1547 +        also have "\<dots> \<le> ?lhs" using `z \<in> f y` `y \<in> Y`
  3.1548 +          by(auto intro: Sup_upper simp add: mcont_contD[OF f chain Y])
  3.1549 +        finally show "u \<le> ?lhs" .
  3.1550 +      qed
  3.1551 +    qed
  3.1552 +  qed
  3.1553 +qed
  3.1554 +
  3.1555 +lemma mcont_SUP [cont_intro, simp]:
  3.1556 +  "\<lbrakk> mcont lub ord Union op \<subseteq> f; \<And>y. mcont lub ord Sup op \<le> (\<lambda>x. g x y) \<rbrakk>
  3.1557 +  \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. \<Squnion>y\<in>f x. g x y)"
  3.1558 +by(blast intro: mcontI cont_SUP[OF assms] monotone_SUP mcont_mono)
  3.1559 +
  3.1560 +end
  3.1561 +
  3.1562 +lemma admissible_Ball [cont_intro, simp]:
  3.1563 +  "\<lbrakk> \<And>x. ccpo.admissible lub ord (\<lambda>A. P A x);
  3.1564 +     mcont lub ord Union op \<subseteq> f;
  3.1565 +     class.ccpo lub ord (mk_less ord) \<rbrakk>
  3.1566 +  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>A. \<forall>x\<in>f A. P A x)"
  3.1567 +unfolding Ball_def by simp
  3.1568 +
  3.1569 +lemma admissible_Bex'[THEN admissible_subst, cont_intro, simp]:
  3.1570 +  shows admissible_Bex: "ccpo.admissible Union op \<subseteq> (\<lambda>A. \<exists>x\<in>A. P x)"
  3.1571 +by(rule ccpo.admissibleI)(auto)
  3.1572 +
  3.1573 +subsection {* Parallel fixpoint induction *}
  3.1574 +
  3.1575 +context
  3.1576 +  fixes luba :: "'a set \<Rightarrow> 'a"
  3.1577 +  and orda :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  3.1578 +  and lubb :: "'b set \<Rightarrow> 'b"
  3.1579 +  and ordb :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
  3.1580 +  assumes a: "class.ccpo luba orda (mk_less orda)"
  3.1581 +  and b: "class.ccpo lubb ordb (mk_less ordb)"
  3.1582 +begin
  3.1583 +
  3.1584 +interpretation a: ccpo luba orda "mk_less orda" by(rule a)
  3.1585 +interpretation b: ccpo lubb ordb "mk_less ordb" by(rule b)
  3.1586 +
  3.1587 +lemma ccpo_rel_prodI:
  3.1588 +  "class.ccpo (prod_lub luba lubb) (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
  3.1589 +  (is "class.ccpo ?lub ?ord ?ord'")
  3.1590 +proof(intro class.ccpo.intro class.ccpo_axioms.intro)
  3.1591 +  show "class.order ?ord ?ord'" by(rule order_rel_prodI) intro_locales
  3.1592 +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)
  3.1593 +
  3.1594 +interpretation ab: ccpo "prod_lub luba lubb" "rel_prod orda ordb" "mk_less (rel_prod orda ordb)"
  3.1595 +by(rule ccpo_rel_prodI)
  3.1596 +
  3.1597 +lemma monotone_map_prod [simp]:
  3.1598 +  "monotone (rel_prod orda ordb) (rel_prod ordc ordd) (map_prod f g) \<longleftrightarrow>
  3.1599 +   monotone orda ordc f \<and> monotone ordb ordd g"
  3.1600 +by(auto simp add: monotone_def)
  3.1601 +
  3.1602 +lemma parallel_fixp_induct:
  3.1603 +  assumes adm: "ccpo.admissible (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. P (fst x) (snd x))"
  3.1604 +  and f: "monotone orda orda f"
  3.1605 +  and g: "monotone ordb ordb g"
  3.1606 +  and bot: "P (luba {}) (lubb {})"
  3.1607 +  and step: "\<And>x y. P x y \<Longrightarrow> P (f x) (g y)"
  3.1608 +  shows "P (ccpo.fixp luba orda f) (ccpo.fixp lubb ordb g)"
  3.1609 +proof -
  3.1610 +  let ?lub = "prod_lub luba lubb"
  3.1611 +    and ?ord = "rel_prod orda ordb"
  3.1612 +    and ?P = "\<lambda>(x, y). P x y"
  3.1613 +  from adm have adm': "ccpo.admissible ?lub ?ord ?P" by(simp add: split_def)
  3.1614 +  hence "?P (ccpo.fixp (prod_lub luba lubb) (rel_prod orda ordb) (map_prod f g))"
  3.1615 +    by(rule ab.fixp_induct)(auto simp add: f g step bot)
  3.1616 +  also have "ccpo.fixp (prod_lub luba lubb) (rel_prod orda ordb) (map_prod f g) = 
  3.1617 +            (ccpo.fixp luba orda f, ccpo.fixp lubb ordb g)" (is "?lhs = (?rhs1, ?rhs2)")
  3.1618 +  proof(rule ab.antisym)
  3.1619 +    have "ccpo.admissible ?lub ?ord (\<lambda>xy. ?ord xy (?rhs1, ?rhs2))"
  3.1620 +      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)
  3.1621 +    thus "?ord ?lhs (?rhs1, ?rhs2)"
  3.1622 +      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)
  3.1623 +  next
  3.1624 +    have "ccpo.admissible luba orda (\<lambda>x. orda x (fst ?lhs))"
  3.1625 +      by(rule admissible_leI[OF a])(auto intro: a.ccpo_Sup_least simp add: chain_empty)
  3.1626 +    hence "orda ?rhs1 (fst ?lhs)" using f
  3.1627 +    proof(rule a.fixp_induct)
  3.1628 +      fix x
  3.1629 +      assume "orda x (fst ?lhs)"
  3.1630 +      thus "orda (f x) (fst ?lhs)"
  3.1631 +        by(subst ab.fixp_unfold)(auto simp add: f g dest: monotoneD[OF f])
  3.1632 +    qed(auto intro: a.ccpo_Sup_least chain_empty)
  3.1633 +    moreover
  3.1634 +    have "ccpo.admissible lubb ordb (\<lambda>y. ordb y (snd ?lhs))"
  3.1635 +      by(rule admissible_leI[OF b])(auto intro: b.ccpo_Sup_least simp add: chain_empty)
  3.1636 +    hence "ordb ?rhs2 (snd ?lhs)" using g
  3.1637 +    proof(rule b.fixp_induct)
  3.1638 +      fix y
  3.1639 +      assume "ordb y (snd ?lhs)"
  3.1640 +      thus "ordb (g y) (snd ?lhs)"
  3.1641 +        by(subst ab.fixp_unfold)(auto simp add: f g dest: monotoneD[OF g])
  3.1642 +    qed(auto intro: b.ccpo_Sup_least chain_empty)
  3.1643 +    ultimately show "?ord (?rhs1, ?rhs2) ?lhs"
  3.1644 +      by(simp add: rel_prod_conv split_beta)
  3.1645 +  qed
  3.1646 +  finally show ?thesis by simp
  3.1647 +qed
  3.1648 +
  3.1649 +end
  3.1650 +
  3.1651 +lemma parallel_fixp_induct_uc:
  3.1652 +  assumes a: "partial_function_definitions orda luba"
  3.1653 +  and b: "partial_function_definitions ordb lubb"
  3.1654 +  and F: "\<And>x. monotone (fun_ord orda) orda (\<lambda>f. U1 (F (C1 f)) x)"
  3.1655 +  and G: "\<And>y. monotone (fun_ord ordb) ordb (\<lambda>g. U2 (G (C2 g)) y)"
  3.1656 +  and eq1: "f \<equiv> C1 (ccpo.fixp (fun_lub luba) (fun_ord orda) (\<lambda>f. U1 (F (C1 f))))"
  3.1657 +  and eq2: "g \<equiv> C2 (ccpo.fixp (fun_lub lubb) (fun_ord ordb) (\<lambda>g. U2 (G (C2 g))))"
  3.1658 +  and inverse: "\<And>f. U1 (C1 f) = f"
  3.1659 +  and inverse2: "\<And>g. U2 (C2 g) = g"
  3.1660 +  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))"
  3.1661 +  and bot: "P (\<lambda>_. luba {}) (\<lambda>_. lubb {})"
  3.1662 +  and step: "\<And>f g. P (U1 f) (U2 g) \<Longrightarrow> P (U1 (F f)) (U2 (G g))"
  3.1663 +  shows "P (U1 f) (U2 g)"
  3.1664 +apply(unfold eq1 eq2 inverse inverse2)
  3.1665 +apply(rule parallel_fixp_induct[OF partial_function_definitions.ccpo[OF a] partial_function_definitions.ccpo[OF b] adm])
  3.1666 +using F apply(simp add: monotone_def fun_ord_def)
  3.1667 +using G apply(simp add: monotone_def fun_ord_def)
  3.1668 +apply(simp add: fun_lub_def bot)
  3.1669 +apply(rule step, simp add: inverse inverse2)
  3.1670 +done
  3.1671 +
  3.1672 +lemmas parallel_fixp_induct_1_1 = parallel_fixp_induct_uc[
  3.1673 +  of _ _ _ _ "\<lambda>x. x" _ "\<lambda>x. x" "\<lambda>x. x" _ "\<lambda>x. x",
  3.1674 +  OF _ _ _ _ _ _ refl refl]
  3.1675 +
  3.1676 +lemmas parallel_fixp_induct_2_2 = parallel_fixp_induct_uc[
  3.1677 +  of _ _ _ _ "case_prod" _ "curry" "case_prod" _ "curry",
  3.1678 +  where P="\<lambda>f g. P (curry f) (curry g)",
  3.1679 +  unfolded case_prod_curry curry_case_prod curry_K,
  3.1680 +  OF _ _ _ _ _ _ refl refl]
  3.1681 +  for P
  3.1682 +
  3.1683 +lemma monotone_fst: "monotone (rel_prod orda ordb) orda fst"
  3.1684 +by(auto intro: monotoneI)
  3.1685 +
  3.1686 +lemma mcont_fst: "mcont (prod_lub luba lubb) (rel_prod orda ordb) luba orda fst"
  3.1687 +by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
  3.1688 +
  3.1689 +lemma mcont2mcont_fst [cont_intro, simp]:
  3.1690 +  "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
  3.1691 +  \<Longrightarrow> mcont lub ord luba orda (\<lambda>x. fst (t x))"
  3.1692 +by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
  3.1693 +
  3.1694 +lemma monotone_snd: "monotone (rel_prod orda ordb) ordb snd"
  3.1695 +by(auto intro: monotoneI)
  3.1696 +
  3.1697 +lemma mcont_snd: "mcont (prod_lub luba lubb) (rel_prod orda ordb) lubb ordb snd"
  3.1698 +by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
  3.1699 +
  3.1700 +lemma mcont2mcont_snd [cont_intro, simp]:
  3.1701 +  "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
  3.1702 +  \<Longrightarrow> mcont lub ord lubb ordb (\<lambda>x. snd (t x))"
  3.1703 +by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
  3.1704 +
  3.1705 +context partial_function_definitions begin
  3.1706 +text \<open>Specialised versions of @{thm [source] mcont_call} for admissibility proofs for parallel fixpoint inductions\<close>
  3.1707 +lemmas mcont_call_fst [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_fst]
  3.1708 +lemmas mcont_call_snd [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_snd]
  3.1709 +end
  3.1710 +
  3.1711 +end
     4.1 --- a/src/HOL/Library/Library.thy	Thu Mar 17 14:48:14 2016 +0100
     4.2 +++ b/src/HOL/Library/Library.thy	Fri Mar 18 08:01:49 2016 +0100
     4.3 @@ -11,6 +11,7 @@
     4.4    Code_Test
     4.5    ContNotDenum
     4.6    Convex
     4.7 +  Complete_Partial_Order2
     4.8    Countable
     4.9    Countable_Complete_Lattices
    4.10    Countable_Set_Type