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