src/HOL/Library/Complete_Partial_Order2.thy
author wenzelm
Mon, 25 Apr 2016 16:09:26 +0200
changeset 63040 eb4ddd18d635
parent 62858 d72a6f9ee690
child 63092 a949b2a5f51d
permissions -rw-r--r--
eliminated old 'def'; tuned comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62858
d72a6f9ee690 tuned headers;
wenzelm
parents: 62837
diff changeset
     1
(*  Title:      HOL/Library/Complete_Partial_Order2.thy
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
     2
    Author:     Andreas Lochbihler, ETH Zurich
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
     3
*)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
     4
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
     5
section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
     6
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
     7
theory Complete_Partial_Order2 imports 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
     8
  Main
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
     9
  "~~/src/HOL/Library/Lattice_Syntax"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    10
begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    11
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    12
context begin interpretation lifting_syntax .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    13
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    14
lemma chain_transfer [transfer_rule]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    15
  "((A ===> A ===> op =) ===> rel_set A ===> op =) Complete_Partial_Order.chain Complete_Partial_Order.chain"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    16
unfolding chain_def[abs_def] by transfer_prover
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    17
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    18
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    19
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    20
lemma linorder_chain [simp, intro!]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    21
  fixes Y :: "_ :: linorder set"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    22
  shows "Complete_Partial_Order.chain op \<le> Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    23
by(auto intro: chainI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    24
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    25
lemma fun_lub_apply: "\<And>Sup. fun_lub Sup Y x = Sup ((\<lambda>f. f x) ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    26
by(simp add: fun_lub_def image_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    27
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    28
lemma fun_lub_empty [simp]: "fun_lub lub {} = (\<lambda>_. lub {})"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    29
by(rule ext)(simp add: fun_lub_apply)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    30
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    31
lemma chain_fun_ordD: 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    32
  assumes "Complete_Partial_Order.chain (fun_ord le) Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    33
  shows "Complete_Partial_Order.chain le ((\<lambda>f. f x) ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    34
by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    35
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    36
lemma chain_Diff:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    37
  "Complete_Partial_Order.chain ord A
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    38
  \<Longrightarrow> Complete_Partial_Order.chain ord (A - B)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    39
by(erule chain_subset) blast
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    40
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    41
lemma chain_rel_prodD1:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    42
  "Complete_Partial_Order.chain (rel_prod orda ordb) Y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    43
  \<Longrightarrow> Complete_Partial_Order.chain orda (fst ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    44
by(auto 4 3 simp add: chain_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    45
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    46
lemma chain_rel_prodD2:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    47
  "Complete_Partial_Order.chain (rel_prod orda ordb) Y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    48
  \<Longrightarrow> Complete_Partial_Order.chain ordb (snd ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    49
by(auto 4 3 simp add: chain_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    50
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    51
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    52
context ccpo begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    53
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    54
lemma ccpo_fun: "class.ccpo (fun_lub Sup) (fun_ord op \<le>) (mk_less (fun_ord op \<le>))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    55
  by standard (auto 4 3 simp add: mk_less_def fun_ord_def fun_lub_apply
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    56
    intro: order.trans antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    57
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    58
lemma ccpo_Sup_below_iff: "Complete_Partial_Order.chain op \<le> Y \<Longrightarrow> Sup Y \<le> x \<longleftrightarrow> (\<forall>y\<in>Y. y \<le> x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    59
by(fast intro: order_trans[OF ccpo_Sup_upper] ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    60
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    61
lemma Sup_minus_bot: 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    62
  assumes chain: "Complete_Partial_Order.chain op \<le> A"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    63
  shows "\<Squnion>(A - {\<Squnion>{}}) = \<Squnion>A"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    64
apply(rule antisym)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    65
 apply(blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    66
apply(rule ccpo_Sup_least[OF chain])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    67
apply(case_tac "x = \<Squnion>{}")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    68
by(blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    69
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    70
lemma mono_lub:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    71
  fixes le_b (infix "\<sqsubseteq>" 60)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    72
  assumes chain: "Complete_Partial_Order.chain (fun_ord op \<le>) Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    73
  and mono: "\<And>f. f \<in> Y \<Longrightarrow> monotone le_b op \<le> f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    74
  shows "monotone op \<sqsubseteq> op \<le> (fun_lub Sup Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    75
proof(rule monotoneI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    76
  fix x y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    77
  assume "x \<sqsubseteq> y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    78
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    79
  have chain'': "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    80
    using chain by(rule chain_imageI)(simp add: fun_ord_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    81
  then show "fun_lub Sup Y x \<le> fun_lub Sup Y y" unfolding fun_lub_apply
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    82
  proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    83
    fix x'
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    84
    assume "x' \<in> (\<lambda>f. f x) ` Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    85
    then obtain f where "f \<in> Y" "x' = f x" by blast
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
    86
    note \<open>x' = f x\<close> also
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
    87
    from \<open>f \<in> Y\<close> \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y" by(blast dest: mono monotoneD)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    88
    also have "\<dots> \<le> \<Squnion>((\<lambda>f. f y) ` Y)" using chain''
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
    89
      by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Y\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    90
    finally show "x' \<le> \<Squnion>((\<lambda>f. f y) ` Y)" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    91
  qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    92
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    93
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    94
context
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    95
  fixes le_b (infix "\<sqsubseteq>" 60) and Y f
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    96
  assumes chain: "Complete_Partial_Order.chain le_b Y" 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    97
  and mono1: "\<And>y. y \<in> Y \<Longrightarrow> monotone le_b op \<le> (\<lambda>x. f x y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    98
  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"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
    99
begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   100
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   101
lemma Sup_mono: 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   102
  assumes le: "x \<sqsubseteq> y" and x: "x \<in> Y" and y: "y \<in> Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   103
  shows "\<Squnion>(f x ` Y) \<le> \<Squnion>(f y ` Y)" (is "_ \<le> ?rhs")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   104
proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   105
  from chain show chain': "Complete_Partial_Order.chain op \<le> (f x ` Y)" when "x \<in> Y" for x
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   106
    by(rule chain_imageI) (insert that, auto dest: mono2)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   107
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   108
  fix x'
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   109
  assume "x' \<in> f x ` Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   110
  then obtain y' where "y' \<in> Y" "x' = f x y'" by blast note this(2)
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   111
  also from mono1[OF \<open>y' \<in> Y\<close>] le have "\<dots> \<le> f y y'" by(rule monotoneD)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   112
  also have "\<dots> \<le> ?rhs" using chain'[OF y]
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   113
    by (auto intro!: ccpo_Sup_upper simp add: \<open>y' \<in> Y\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   114
  finally show "x' \<le> ?rhs" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   115
qed(rule x)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   116
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   117
lemma diag_Sup: "\<Squnion>((\<lambda>x. \<Squnion>(f x ` Y)) ` Y) = \<Squnion>((\<lambda>x. f x x) ` Y)" (is "?lhs = ?rhs")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   118
proof(rule antisym)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   119
  have chain1: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>(f x ` Y)) ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   120
    using chain by(rule chain_imageI)(rule Sup_mono)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   121
  have chain2: "\<And>y'. y' \<in> Y \<Longrightarrow> Complete_Partial_Order.chain op \<le> (f y' ` Y)" using chain
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   122
    by(rule chain_imageI)(auto dest: mono2)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   123
  have chain3: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. f x x) ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   124
    using chain by(rule chain_imageI)(auto intro: monotoneD[OF mono1] mono2 order.trans)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   125
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   126
  show "?lhs \<le> ?rhs" using chain1
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   127
  proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   128
    fix x'
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   129
    assume "x' \<in> (\<lambda>x. \<Squnion>(f x ` Y)) ` Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   130
    then obtain y' where "y' \<in> Y" "x' = \<Squnion>(f y' ` Y)" by blast note this(2)
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   131
    also have "\<dots> \<le> ?rhs" using chain2[OF \<open>y' \<in> Y\<close>]
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   132
    proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   133
      fix x
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   134
      assume "x \<in> f y' ` Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   135
      then obtain y where "y \<in> Y" and x: "x = f y' y" by blast
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62858
diff changeset
   136
      define y'' where "y'' = (if y \<sqsubseteq> y' then y' else y)"
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   137
      from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   138
      hence "f y' y \<le> f y'' y''" using \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close>
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   139
        by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1])
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   140
      also from \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y'' \<in> Y" by(simp add: y''_def)
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   141
      from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: \<open>y'' \<in> Y\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   142
      finally show "x \<le> ?rhs" by(simp add: x)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   143
    qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   144
    finally show "x' \<le> ?rhs" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   145
  qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   146
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   147
  show "?rhs \<le> ?lhs" using chain3
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   148
  proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   149
    fix y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   150
    assume "y \<in> (\<lambda>x. f x x) ` Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   151
    then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2)
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   152
    also from chain2[OF \<open>x \<in> Y\<close>] have "\<dots> \<le> \<Squnion>(f x ` Y)"
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   153
      by(rule ccpo_Sup_upper)(simp add: \<open>x \<in> Y\<close>)
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   154
    also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \<open>x \<in> Y\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   155
    finally show "y \<le> ?lhs" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   156
  qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   157
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   158
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   159
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   160
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   161
lemma Sup_image_mono_le:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   162
  fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>_" [900] 900)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   163
  assumes ccpo: "class.ccpo Sup_b op \<sqsubseteq> lt_b"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   164
  assumes chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   165
  and mono: "\<And>x y. \<lbrakk> x \<sqsubseteq> y; x \<in> Y \<rbrakk> \<Longrightarrow> f x \<le> f y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   166
  shows "Sup (f ` Y) \<le> f (\<Or>Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   167
proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   168
  show "Complete_Partial_Order.chain op \<le> (f ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   169
    using chain by(rule chain_imageI)(rule mono)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   170
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   171
  fix x
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   172
  assume "x \<in> f ` Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   173
  then obtain y where "y \<in> Y" and "x = f y" by blast note this(2)
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   174
  also have "y \<sqsubseteq> \<Or>Y" using ccpo chain \<open>y \<in> Y\<close> by(rule ccpo.ccpo_Sup_upper)
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   175
  hence "f y \<le> f (\<Or>Y)" using \<open>y \<in> Y\<close> by(rule mono)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   176
  finally show "x \<le> \<dots>" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   177
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   178
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   179
lemma swap_Sup:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   180
  fixes le_b (infix "\<sqsubseteq>" 60)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   181
  assumes Y: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   182
  and Z: "Complete_Partial_Order.chain (fun_ord op \<le>) Z"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   183
  and mono: "\<And>f. f \<in> Z \<Longrightarrow> monotone op \<sqsubseteq> op \<le> f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   184
  shows "\<Squnion>((\<lambda>x. \<Squnion>(x ` Y)) ` Z) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   185
  (is "?lhs = ?rhs")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   186
proof(cases "Y = {}")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   187
  case True
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   188
  then show ?thesis
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   189
    by (simp add: image_constant_conv cong del: strong_SUP_cong)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   190
next
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   191
  case False
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   192
  have chain1: "\<And>f. f \<in> Z \<Longrightarrow> Complete_Partial_Order.chain op \<le> (f ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   193
    by(rule chain_imageI[OF Y])(rule monotoneD[OF mono])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   194
  have chain2: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>(x ` Y)) ` Z)" using Z
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   195
  proof(rule chain_imageI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   196
    fix f g
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   197
    assume "f \<in> Z" "g \<in> Z"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   198
      and "fun_ord op \<le> f g"
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   199
    from chain1[OF \<open>f \<in> Z\<close>] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   200
    proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   201
      fix x
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   202
      assume "x \<in> f ` Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   203
      then obtain y where "y \<in> Y" "x = f y" by blast note this(2)
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   204
      also have "\<dots> \<le> g y" using \<open>fun_ord op \<le> f g\<close> by(simp add: fun_ord_def)
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   205
      also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF \<open>g \<in> Z\<close>]
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   206
        by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   207
      finally show "x \<le> \<Squnion>(g ` Y)" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   208
    qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   209
  qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   210
  have chain3: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` Z)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   211
    using Z by(rule chain_imageI)(simp add: fun_ord_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   212
  have chain4: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   213
    using Y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   214
  proof(rule chain_imageI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   215
    fix f x y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   216
    assume "x \<sqsubseteq> y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   217
    show "\<Squnion>((\<lambda>f. f x) ` Z) \<le> \<Squnion>((\<lambda>f. f y) ` Z)" (is "_ \<le> ?rhs") using chain3
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   218
    proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   219
      fix x'
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   220
      assume "x' \<in> (\<lambda>f. f x) ` Z"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   221
      then obtain f where "f \<in> Z" "x' = f x" by blast note this(2)
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   222
      also have "f x \<le> f y" using \<open>f \<in> Z\<close> \<open>x \<sqsubseteq> y\<close> by(rule monotoneD[OF mono])
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   223
      also have "f y \<le> ?rhs" using chain3
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   224
        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   225
      finally show "x' \<le> ?rhs" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   226
    qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   227
  qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   228
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   229
  from chain2 have "?lhs \<le> ?rhs"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   230
  proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   231
    fix x
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   232
    assume "x \<in> (\<lambda>x. \<Squnion>(x ` Y)) ` Z"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   233
    then obtain f where "f \<in> Z" "x = \<Squnion>(f ` Y)" by blast note this(2)
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   234
    also have "\<dots> \<le> ?rhs" using chain1[OF \<open>f \<in> Z\<close>]
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   235
    proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   236
      fix x'
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   237
      assume "x' \<in> f ` Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   238
      then obtain y where "y \<in> Y" "x' = f y" by blast note this(2)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   239
      also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   240
        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   241
      also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   242
      finally show "x' \<le> ?rhs" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   243
    qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   244
    finally show "x \<le> ?rhs" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   245
  qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   246
  moreover
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   247
  have "?rhs \<le> ?lhs" using chain4
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   248
  proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   249
    fix x
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   250
    assume "x \<in> (\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   251
    then obtain y where "y \<in> Y" "x = \<Squnion>((\<lambda>f. f y) ` Z)" by blast note this(2)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   252
    also have "\<dots> \<le> ?lhs" using chain3
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   253
    proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   254
      fix x'
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   255
      assume "x' \<in> (\<lambda>f. f y) ` Z"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   256
      then obtain f where "f \<in> Z" "x' = f y" by blast note this(2)
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   257
      also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF \<open>f \<in> Z\<close>]
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   258
        by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   259
      also have "\<dots> \<le> ?lhs" using chain2
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   260
        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   261
      finally show "x' \<le> ?lhs" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   262
    qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   263
    finally show "x \<le> ?lhs" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   264
  qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   265
  ultimately show "?lhs = ?rhs" by(rule antisym)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   266
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   267
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   268
lemma fixp_mono:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   269
  assumes fg: "fun_ord op \<le> f g"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   270
  and f: "monotone op \<le> op \<le> f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   271
  and g: "monotone op \<le> op \<le> g"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   272
  shows "ccpo_class.fixp f \<le> ccpo_class.fixp g"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   273
unfolding fixp_def
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   274
proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   275
  fix x
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   276
  assume "x \<in> ccpo_class.iterates f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   277
  thus "x \<le> \<Squnion>ccpo_class.iterates g"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   278
  proof induction
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   279
    case (step x)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   280
    from f step.IH have "f x \<le> f (\<Squnion>ccpo_class.iterates g)" by(rule monotoneD)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   281
    also have "\<dots> \<le> g (\<Squnion>ccpo_class.iterates g)" using fg by(simp add: fun_ord_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   282
    also have "\<dots> = \<Squnion>ccpo_class.iterates g" by(fold fixp_def fixp_unfold[OF g]) simp
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   283
    finally show ?case .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   284
  qed(blast intro: ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   285
qed(rule chain_iterates[OF f])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   286
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   287
context fixes ordb :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   288
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   289
lemma iterates_mono:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   290
  assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   291
  and mono: "\<And>f. monotone op \<sqsubseteq> op \<le> f \<Longrightarrow> monotone op \<sqsubseteq> op \<le> (F f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   292
  shows "monotone op \<sqsubseteq> op \<le> f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   293
using f
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   294
by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mono_lub)+
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   295
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   296
lemma fixp_preserves_mono:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   297
  assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. F f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   298
  and mono2: "\<And>f. monotone op \<sqsubseteq> op \<le> f \<Longrightarrow> monotone op \<sqsubseteq> op \<le> (F f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   299
  shows "monotone op \<sqsubseteq> op \<le> (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) F)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   300
  (is "monotone _ _ ?fixp")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   301
proof(rule monotoneI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   302
  have mono: "monotone (fun_ord op \<le>) (fun_ord op \<le>) F"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   303
    by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   304
  let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   305
  have chain: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` ?iter)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   306
    by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   307
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   308
  fix x y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   309
  assume "x \<sqsubseteq> y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   310
  show "?fixp x \<le> ?fixp y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   311
    unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   312
  proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   313
    fix x'
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   314
    assume "x' \<in> (\<lambda>f. f x) ` ?iter"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   315
    then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   316
    also have "f x \<le> f y"
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   317
      by(rule monotoneD[OF iterates_mono[OF \<open>f \<in> ?iter\<close> mono2]])(blast intro: \<open>x \<sqsubseteq> y\<close>)+
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   318
    also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   319
      by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   320
    finally show "x' \<le> \<dots>" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   321
  qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   322
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   323
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   324
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   325
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   326
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   327
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   328
lemma monotone2monotone:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   329
  assumes 2: "\<And>x. monotone ordb ordc (\<lambda>y. f x y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   330
  and t: "monotone orda ordb (\<lambda>x. t x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   331
  and 1: "\<And>y. monotone orda ordc (\<lambda>x. f x y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   332
  and trans: "transp ordc"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   333
  shows "monotone orda ordc (\<lambda>x. f x (t x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   334
by(blast intro: monotoneI transpD[OF trans] monotoneD[OF t] monotoneD[OF 2] monotoneD[OF 1])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   335
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   336
subsection \<open>Continuity\<close>
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   337
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   338
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"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   339
where
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   340
  "cont luba orda lubb ordb f \<longleftrightarrow> 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   341
  (\<forall>Y. Complete_Partial_Order.chain orda Y \<longrightarrow> Y \<noteq> {} \<longrightarrow> f (luba Y) = lubb (f ` Y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   342
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   343
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"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   344
where
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   345
  "mcont luba orda lubb ordb f \<longleftrightarrow>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   346
   monotone orda ordb f \<and> cont luba orda lubb ordb f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   347
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   348
subsubsection \<open>Theorem collection \<open>cont_intro\<close>\<close>
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   349
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   350
named_theorems cont_intro "continuity and admissibility intro rules"
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   351
ML \<open>
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   352
(* apply cont_intro rules as intro and try to solve 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   353
   the remaining of the emerging subgoals with simp *)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   354
fun cont_intro_tac ctxt =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   355
  REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems cont_intro})))
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   356
  THEN_ALL_NEW (SOLVED' (simp_tac ctxt))
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   357
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   358
fun cont_intro_simproc ctxt ct =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   359
  let
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   360
    fun mk_stmt t = t
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   361
      |> HOLogic.mk_Trueprop
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   362
      |> Thm.cterm_of ctxt
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   363
      |> Goal.init
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   364
    fun mk_thm t =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   365
      case SINGLE (cont_intro_tac ctxt 1) (mk_stmt t) of
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   366
        SOME thm => SOME (Goal.finish ctxt thm RS @{thm Eq_TrueI})
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   367
      | NONE => NONE
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   368
  in
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   369
    case Thm.term_of ct of
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   370
      t as Const (@{const_name ccpo.admissible}, _) $ _ $ _ $ _ => mk_thm t
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   371
    | t as Const (@{const_name mcont}, _) $ _ $ _ $ _ $ _ $ _ => mk_thm t
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   372
    | t as Const (@{const_name monotone}, _) $ _ $ _ $ _ => mk_thm t
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   373
    | _ => NONE
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   374
  end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   375
  handle THM _ => NONE 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   376
  | TYPE _ => NONE
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   377
\<close>
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   378
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   379
simproc_setup "cont_intro"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   380
  ( "ccpo.admissible lub ord P"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   381
  | "mcont lub ord lub' ord' f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   382
  | "monotone ord ord' f"
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   383
  ) = \<open>K cont_intro_simproc\<close>
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   384
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   385
lemmas [cont_intro] =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   386
  call_mono
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   387
  let_mono
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   388
  if_mono
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   389
  option.const_mono
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   390
  tailrec.const_mono
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   391
  bind_mono
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   392
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   393
declare if_mono[simp]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   394
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   395
lemma monotone_id' [cont_intro]: "monotone ord ord (\<lambda>x. x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   396
by(simp add: monotone_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   397
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   398
lemma monotone_applyI:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   399
  "monotone orda ordb F \<Longrightarrow> monotone (fun_ord orda) ordb (\<lambda>f. F (f x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   400
by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   401
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   402
lemma monotone_if_fun [partial_function_mono]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   403
  "\<lbrakk> monotone (fun_ord orda) (fun_ord ordb) F; monotone (fun_ord orda) (fun_ord ordb) G \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   404
  \<Longrightarrow> monotone (fun_ord orda) (fun_ord ordb) (\<lambda>f n. if c n then F f n else G f n)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   405
by(simp add: monotone_def fun_ord_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   406
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   407
lemma monotone_fun_apply_fun [partial_function_mono]: 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   408
  "monotone (fun_ord (fun_ord ord)) (fun_ord ord) (\<lambda>f n. f t (g n))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   409
by(rule monotoneI)(simp add: fun_ord_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   410
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   411
lemma monotone_fun_ord_apply: 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   412
  "monotone orda (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. monotone orda ordb (\<lambda>y. f y x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   413
by(auto simp add: monotone_def fun_ord_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   414
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   415
context preorder begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   416
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   417
lemma transp_le [simp, cont_intro]: "transp op \<le>"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   418
by(rule transpI)(rule order_trans)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   419
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   420
lemma monotone_const [simp, cont_intro]: "monotone ord op \<le> (\<lambda>_. c)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   421
by(rule monotoneI) simp
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   422
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   423
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   424
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   425
lemma transp_le [cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   426
  "class.preorder ord (mk_less ord) \<Longrightarrow> transp ord"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   427
by(rule preorder.transp_le)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   428
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   429
context partial_function_definitions begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   430
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   431
declare const_mono [cont_intro, simp]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   432
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   433
lemma transp_le [cont_intro, simp]: "transp leq"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   434
by(rule transpI)(rule leq_trans)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   435
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   436
lemma preorder [cont_intro, simp]: "class.preorder leq (mk_less leq)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   437
by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   438
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   439
declare ccpo[cont_intro, simp]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   440
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   441
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   442
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   443
lemma contI [intro?]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   444
  "(\<And>Y. \<lbrakk> Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> \<Longrightarrow> f (luba Y) = lubb (f ` Y)) 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   445
  \<Longrightarrow> cont luba orda lubb ordb f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   446
unfolding cont_def by blast
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   447
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   448
lemma contD:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   449
  "\<lbrakk> cont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   450
  \<Longrightarrow> f (luba Y) = lubb (f ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   451
unfolding cont_def by blast
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   452
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   453
lemma cont_id [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord id"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   454
by(rule contI) simp
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   455
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   456
lemma cont_id' [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord (\<lambda>x. x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   457
using cont_id[unfolded id_def] .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   458
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   459
lemma cont_applyI [cont_intro]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   460
  assumes cont: "cont luba orda lubb ordb g"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   461
  shows "cont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. g (f x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   462
by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   463
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   464
lemma call_cont: "cont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   465
by(simp add: cont_def fun_lub_apply)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   466
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   467
lemma cont_if [cont_intro]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   468
  "\<lbrakk> cont luba orda lubb ordb f; cont luba orda lubb ordb g \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   469
  \<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   470
by(cases c) simp_all
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   471
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   472
lemma mcontI [intro?]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   473
   "\<lbrakk> monotone orda ordb f; cont luba orda lubb ordb f \<rbrakk> \<Longrightarrow> mcont luba orda lubb ordb f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   474
by(simp add: mcont_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   475
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   476
lemma mcont_mono: "mcont luba orda lubb ordb f \<Longrightarrow> monotone orda ordb f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   477
by(simp add: mcont_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   478
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   479
lemma mcont_cont [simp]: "mcont luba orda lubb ordb f \<Longrightarrow> cont luba orda lubb ordb f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   480
by(simp add: mcont_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   481
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   482
lemma mcont_monoD:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   483
  "\<lbrakk> mcont luba orda lubb ordb f; orda x y \<rbrakk> \<Longrightarrow> ordb (f x) (f y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   484
by(auto simp add: mcont_def dest: monotoneD)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   485
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   486
lemma mcont_contD:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   487
  "\<lbrakk> mcont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   488
  \<Longrightarrow> f (luba Y) = lubb (f ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   489
by(auto simp add: mcont_def dest: contD)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   490
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   491
lemma mcont_call [cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   492
  "mcont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   493
by(simp add: mcont_def call_mono call_cont)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   494
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   495
lemma mcont_id' [cont_intro, simp]: "mcont lub ord lub ord (\<lambda>x. x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   496
by(simp add: mcont_def monotone_id')
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   497
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   498
lemma mcont_applyI:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   499
  "mcont luba orda lubb ordb (\<lambda>x. F x) \<Longrightarrow> mcont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. F (f x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   500
by(simp add: mcont_def monotone_applyI cont_applyI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   501
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   502
lemma mcont_if [cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   503
  "\<lbrakk> mcont luba orda lubb ordb (\<lambda>x. f x); mcont luba orda lubb ordb (\<lambda>x. g x) \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   504
  \<Longrightarrow> mcont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   505
by(simp add: mcont_def cont_if)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   506
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   507
lemma cont_fun_lub_apply: 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   508
  "cont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. cont luba orda lubb ordb (\<lambda>y. f y x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   509
by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   510
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   511
lemma mcont_fun_lub_apply: 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   512
  "mcont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. mcont luba orda lubb ordb (\<lambda>y. f y x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   513
by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   514
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   515
context ccpo begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   516
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   517
lemma cont_const [simp, cont_intro]: "cont luba orda Sup op \<le> (\<lambda>x. c)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   518
by (rule contI) (simp add: image_constant_conv cong del: strong_SUP_cong)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   519
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   520
lemma mcont_const [cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   521
  "mcont luba orda Sup op \<le> (\<lambda>x. c)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   522
by(simp add: mcont_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   523
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   524
lemma cont_apply:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   525
  assumes 2: "\<And>x. cont lubb ordb Sup op \<le> (\<lambda>y. f x y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   526
  and t: "cont luba orda lubb ordb (\<lambda>x. t x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   527
  and 1: "\<And>y. cont luba orda Sup op \<le> (\<lambda>x. f x y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   528
  and mono: "monotone orda ordb (\<lambda>x. t x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   529
  and mono2: "\<And>x. monotone ordb op \<le> (\<lambda>y. f x y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   530
  and mono1: "\<And>y. monotone orda op \<le> (\<lambda>x. f x y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   531
  shows "cont luba orda Sup op \<le> (\<lambda>x. f x (t x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   532
proof
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   533
  fix Y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   534
  assume chain: "Complete_Partial_Order.chain orda Y" and "Y \<noteq> {}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   535
  moreover from chain have chain': "Complete_Partial_Order.chain ordb (t ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   536
    by(rule chain_imageI)(rule monotoneD[OF mono])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   537
  ultimately show "f (luba Y) (t (luba Y)) = \<Squnion>((\<lambda>x. f x (t x)) ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   538
    by(simp add: contD[OF 1] contD[OF t] contD[OF 2] image_image)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   539
      (rule diag_Sup[OF chain], auto intro: monotone2monotone[OF mono2 mono monotone_const transpI] monotoneD[OF mono1])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   540
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   541
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   542
lemma mcont2mcont':
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   543
  "\<lbrakk> \<And>x. mcont lub' ord' Sup op \<le> (\<lambda>y. f x y);
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   544
     \<And>y. mcont lub ord Sup op \<le> (\<lambda>x. f x y);
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   545
     mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   546
  \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f x (t x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   547
unfolding mcont_def by(blast intro: transp_le monotone2monotone cont_apply)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   548
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   549
lemma mcont2mcont:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   550
  "\<lbrakk>mcont lub' ord' Sup op \<le> (\<lambda>x. f x); mcont lub ord lub' ord' (\<lambda>x. t x)\<rbrakk> 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   551
  \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f (t x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   552
by(rule mcont2mcont'[OF _ mcont_const]) 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   553
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   554
context
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   555
  fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   556
  and lub :: "'b set \<Rightarrow> 'b" ("\<Or>_" [900] 900)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   557
begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   558
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   559
lemma cont_fun_lub_Sup:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   560
  assumes chainM: "Complete_Partial_Order.chain (fun_ord op \<le>) M"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   561
  and mcont [rule_format]: "\<forall>f\<in>M. mcont lub op \<sqsubseteq> Sup op \<le> f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   562
  shows "cont lub op \<sqsubseteq> Sup op \<le> (fun_lub Sup M)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   563
proof(rule contI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   564
  fix Y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   565
  assume chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   566
    and Y: "Y \<noteq> {}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   567
  from swap_Sup[OF chain chainM mcont[THEN mcont_mono]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   568
  show "fun_lub Sup M (\<Or>Y) = \<Squnion>(fun_lub Sup M ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   569
    by(simp add: mcont_contD[OF mcont chain Y] fun_lub_apply cong: image_cong)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   570
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   571
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   572
lemma mcont_fun_lub_Sup:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   573
  "\<lbrakk> Complete_Partial_Order.chain (fun_ord op \<le>) M;
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   574
    \<forall>f\<in>M. mcont lub ord Sup op \<le> f \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   575
  \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (fun_lub Sup M)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   576
by(simp add: mcont_def cont_fun_lub_Sup mono_lub)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   577
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   578
lemma iterates_mcont:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   579
  assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   580
  and mono: "\<And>f. mcont lub op \<sqsubseteq> Sup op \<le> f \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (F f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   581
  shows "mcont lub op \<sqsubseteq> Sup op \<le> f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   582
using f
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   583
by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mcont_fun_lub_Sup)+
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   584
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   585
lemma fixp_preserves_mcont:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   586
  assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. F f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   587
  and mcont: "\<And>f. mcont lub op \<sqsubseteq> Sup op \<le> f \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (F f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   588
  shows "mcont lub op \<sqsubseteq> Sup op \<le> (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) F)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   589
  (is "mcont _ _ _ _ ?fixp")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   590
unfolding mcont_def
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   591
proof(intro conjI monotoneI contI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   592
  have mono: "monotone (fun_ord op \<le>) (fun_ord op \<le>) F"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   593
    by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   594
  let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   595
  have chain: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` ?iter)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   596
    by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   597
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   598
  {
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   599
    fix x y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   600
    assume "x \<sqsubseteq> y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   601
    show "?fixp x \<le> ?fixp y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   602
      unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   603
    proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   604
      fix x'
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   605
      assume "x' \<in> (\<lambda>f. f x) ` ?iter"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   606
      then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   607
      also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y"
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   608
        by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]])
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   609
      also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   610
        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   611
      finally show "x' \<le> \<dots>" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   612
    qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   613
  next
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   614
    fix Y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   615
    assume chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   616
      and Y: "Y \<noteq> {}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   617
    { fix f
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   618
      assume "f \<in> ?iter"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   619
      hence "f (\<Or>Y) = \<Squnion>(f ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   620
        using mcont chain Y by(rule mcont_contD[OF iterates_mcont]) }
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   621
    moreover have "\<Squnion>((\<lambda>f. \<Squnion>(f ` Y)) ` ?iter) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` ?iter)) ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   622
      using chain ccpo.chain_iterates[OF ccpo_fun mono]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   623
      by(rule swap_Sup)(rule mcont_mono[OF iterates_mcont[OF _ mcont]])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   624
    ultimately show "?fixp (\<Or>Y) = \<Squnion>(?fixp ` Y)" unfolding ccpo.fixp_def[OF ccpo_fun]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   625
      by(simp add: fun_lub_apply cong: image_cong)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   626
  }
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   627
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   628
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   629
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   630
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   631
context
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   632
  fixes F :: "'c \<Rightarrow> 'c" and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and f
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   633
  assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. U (F (C f)) x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   634
  and eq: "f \<equiv> C (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) (\<lambda>f. U (F (C f))))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   635
  and inverse: "\<And>f. U (C f) = f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   636
begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   637
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   638
lemma fixp_preserves_mono_uc:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   639
  assumes mono2: "\<And>f. monotone ord op \<le> (U f) \<Longrightarrow> monotone ord op \<le> (U (F f))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   640
  shows "monotone ord op \<le> (U f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   641
using fixp_preserves_mono[OF mono mono2] by(subst eq)(simp add: inverse)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   642
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   643
lemma fixp_preserves_mcont_uc:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   644
  assumes mcont: "\<And>f. mcont lubb ordb Sup op \<le> (U f) \<Longrightarrow> mcont lubb ordb Sup op \<le> (U (F f))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   645
  shows "mcont lubb ordb Sup op \<le> (U f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   646
using fixp_preserves_mcont[OF mono mcont] by(subst eq)(simp add: inverse)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   647
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   648
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   649
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   650
lemmas fixp_preserves_mono1 = fixp_preserves_mono_uc[of "\<lambda>x. x" _ "\<lambda>x. x", OF _ _ refl]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   651
lemmas fixp_preserves_mono2 =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   652
  fixp_preserves_mono_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   653
lemmas fixp_preserves_mono3 =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   654
  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]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   655
lemmas fixp_preserves_mono4 =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   656
  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]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   657
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   658
lemmas fixp_preserves_mcont1 = fixp_preserves_mcont_uc[of "\<lambda>x. x" _ "\<lambda>x. x", OF _ _ refl]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   659
lemmas fixp_preserves_mcont2 =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   660
  fixp_preserves_mcont_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   661
lemmas fixp_preserves_mcont3 =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   662
  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]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   663
lemmas fixp_preserves_mcont4 =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   664
  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]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   665
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   666
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   667
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   668
lemma (in preorder) monotone_if_bot:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   669
  fixes bot
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   670
  assumes mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> (x \<le> bound) \<rbrakk> \<Longrightarrow> ord (f x) (f y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   671
  and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> ord bot (f x)" "ord bot bot"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   672
  shows "monotone op \<le> ord (\<lambda>x. if x \<le> bound then bot else f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   673
by(rule monotoneI)(auto intro: bot intro: mono order_trans)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   674
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   675
lemma (in ccpo) mcont_if_bot:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   676
  fixes bot and lub ("\<Or>_" [900] 900) and ord (infix "\<sqsubseteq>" 60)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   677
  assumes ccpo: "class.ccpo lub op \<sqsubseteq> lt"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   678
  and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   679
  and cont: "\<And>Y. \<lbrakk> Complete_Partial_Order.chain op \<le> Y; Y \<noteq> {}; \<And>x. x \<in> Y \<Longrightarrow> \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f (\<Squnion>Y) = \<Or>(f ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   680
  and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> bot \<sqsubseteq> f x"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   681
  shows "mcont Sup op \<le> lub op \<sqsubseteq> (\<lambda>x. if x \<le> bound then bot else f x)" (is "mcont _ _ _ _ ?g")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   682
proof(intro mcontI contI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   683
  interpret c: ccpo lub "op \<sqsubseteq>" lt by(fact ccpo)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   684
  show "monotone op \<le> op \<sqsubseteq> ?g" by(rule monotone_if_bot)(simp_all add: mono bot)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   685
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   686
  fix Y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   687
  assume chain: "Complete_Partial_Order.chain op \<le> Y" and Y: "Y \<noteq> {}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   688
  show "?g (\<Squnion>Y) = \<Or>(?g ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   689
  proof(cases "Y \<subseteq> {x. x \<le> bound}")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   690
    case True
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   691
    hence "\<Squnion>Y \<le> bound" using chain by(auto intro: ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   692
    moreover have "Y \<inter> {x. \<not> x \<le> bound} = {}" using True by auto
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   693
    ultimately show ?thesis using True Y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   694
      by (auto simp add: image_constant_conv cong del: c.strong_SUP_cong)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   695
  next
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   696
    case False
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   697
    let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   698
    have chain': "Complete_Partial_Order.chain op \<le> ?Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   699
      using chain by(rule chain_subset) simp
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   700
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   701
    from False obtain y where ybound: "\<not> y \<le> bound" and y: "y \<in> Y" by blast
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   702
    hence "\<not> \<Squnion>Y \<le> bound" by (metis ccpo_Sup_upper chain order.trans)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   703
    hence "?g (\<Squnion>Y) = f (\<Squnion>Y)" by simp
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   704
    also have "\<Squnion>Y \<le> \<Squnion>?Y" using chain
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   705
    proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   706
      fix x
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   707
      assume x: "x \<in> Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   708
      show "x \<le> \<Squnion>?Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   709
      proof(cases "x \<le> bound")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   710
        case True
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   711
        with chainD[OF chain x y] have "x \<le> y" using ybound by(auto intro: order_trans)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   712
        thus ?thesis by(rule order_trans)(auto intro: ccpo_Sup_upper[OF chain'] simp add: y ybound)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   713
      qed(auto intro: ccpo_Sup_upper[OF chain'] simp add: x)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   714
    qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   715
    hence "\<Squnion>Y = \<Squnion>?Y" by(rule antisym)(blast intro: ccpo_Sup_least[OF chain'] ccpo_Sup_upper[OF chain])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   716
    hence "f (\<Squnion>Y) = f (\<Squnion>?Y)" by simp
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   717
    also have "f (\<Squnion>?Y) = \<Or>(f ` ?Y)" using chain' by(rule cont)(insert y ybound, auto)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   718
    also have "\<Or>(f ` ?Y) = \<Or>(?g ` Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   719
    proof(cases "Y \<inter> {x. x \<le> bound} = {}")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   720
      case True
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   721
      hence "f ` ?Y = ?g ` Y" by auto
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   722
      thus ?thesis by(rule arg_cong)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   723
    next
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   724
      case False
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   725
      have chain'': "Complete_Partial_Order.chain op \<sqsubseteq> (insert bot (f ` ?Y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   726
        using chain by(auto intro!: chainI bot dest: chainD intro: mono)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   727
      hence chain''': "Complete_Partial_Order.chain op \<sqsubseteq> (f ` ?Y)" by(rule chain_subset) blast
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   728
      have "bot \<sqsubseteq> \<Or>(f ` ?Y)" using y ybound by(blast intro: c.order_trans[OF bot] c.ccpo_Sup_upper[OF chain'''])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   729
      hence "\<Or>(insert bot (f ` ?Y)) \<sqsubseteq> \<Or>(f ` ?Y)" using chain''
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   730
        by(auto intro: c.ccpo_Sup_least c.ccpo_Sup_upper[OF chain''']) 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   731
      with _ have "\<dots> = \<Or>(insert bot (f ` ?Y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   732
        by(rule c.antisym)(blast intro: c.ccpo_Sup_least[OF chain'''] c.ccpo_Sup_upper[OF chain''])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   733
      also have "insert bot (f ` ?Y) = ?g ` Y" using False by auto
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   734
      finally show ?thesis .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   735
    qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   736
    finally show ?thesis .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   737
  qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   738
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   739
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   740
context partial_function_definitions begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   741
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   742
lemma mcont_const [cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   743
  "mcont luba orda lub leq (\<lambda>x. c)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   744
by(rule ccpo.mcont_const)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   745
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   746
lemmas [cont_intro, simp] =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   747
  ccpo.cont_const[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   748
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   749
lemma mono2mono:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   750
  assumes "monotone ordb leq (\<lambda>y. f y)" "monotone orda ordb (\<lambda>x. t x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   751
  shows "monotone orda leq (\<lambda>x. f (t x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   752
using assms by(rule monotone2monotone) simp_all
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   753
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   754
lemmas mcont2mcont' = ccpo.mcont2mcont'[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   755
lemmas mcont2mcont = ccpo.mcont2mcont[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   756
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   757
lemmas fixp_preserves_mono1 = ccpo.fixp_preserves_mono1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   758
lemmas fixp_preserves_mono2 = ccpo.fixp_preserves_mono2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   759
lemmas fixp_preserves_mono3 = ccpo.fixp_preserves_mono3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   760
lemmas fixp_preserves_mono4 = ccpo.fixp_preserves_mono4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   761
lemmas fixp_preserves_mcont1 = ccpo.fixp_preserves_mcont1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   762
lemmas fixp_preserves_mcont2 = ccpo.fixp_preserves_mcont2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   763
lemmas fixp_preserves_mcont3 = ccpo.fixp_preserves_mcont3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   764
lemmas fixp_preserves_mcont4 = ccpo.fixp_preserves_mcont4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   765
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   766
lemma monotone_if_bot:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   767
  fixes bot
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   768
  assumes g: "\<And>x. g x = (if leq x bound then bot else f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   769
  and mono: "\<And>x y. \<lbrakk> leq x y; \<not> leq x bound \<rbrakk> \<Longrightarrow> ord (f x) (f y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   770
  and bot: "\<And>x. \<not> leq x bound \<Longrightarrow> ord bot (f x)" "ord bot bot"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   771
  shows "monotone leq ord g"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   772
unfolding g[abs_def] using preorder mono bot by(rule preorder.monotone_if_bot)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   773
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   774
lemma mcont_if_bot:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   775
  fixes bot
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   776
  assumes ccpo: "class.ccpo lub' ord (mk_less ord)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   777
  and bot: "\<And>x. \<not> leq x bound \<Longrightarrow> ord bot (f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   778
  and g: "\<And>x. g x = (if leq x bound then bot else f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   779
  and mono: "\<And>x y. \<lbrakk> leq x y; \<not> leq x bound \<rbrakk> \<Longrightarrow> ord (f x) (f y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   780
  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)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   781
  shows "mcont lub leq lub' ord g"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   782
unfolding g[abs_def] using ccpo mono cont bot by(rule ccpo.mcont_if_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   783
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   784
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   785
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   786
subsection \<open>Admissibility\<close>
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   787
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   788
lemma admissible_subst:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   789
  assumes adm: "ccpo.admissible luba orda (\<lambda>x. P x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   790
  and mcont: "mcont lubb ordb luba orda f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   791
  shows "ccpo.admissible lubb ordb (\<lambda>x. P (f x))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   792
apply(rule ccpo.admissibleI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   793
apply(frule (1) mcont_contD[OF mcont])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   794
apply(auto intro: ccpo.admissibleD[OF adm] chain_imageI dest: mcont_monoD[OF mcont])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   795
done
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   796
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   797
lemmas [simp, cont_intro] = 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   798
  admissible_all
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   799
  admissible_ball
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   800
  admissible_const
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   801
  admissible_conj
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   802
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   803
lemma admissible_disj' [simp, cont_intro]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   804
  "\<lbrakk> class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord P; ccpo.admissible lub ord Q \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   805
  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<or> Q x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   806
by(rule ccpo.admissible_disj)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   807
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   808
lemma admissible_imp' [cont_intro]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   809
  "\<lbrakk> class.ccpo lub ord (mk_less ord);
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   810
     ccpo.admissible lub ord (\<lambda>x. \<not> P x);
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   811
     ccpo.admissible lub ord (\<lambda>x. Q x) \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   812
  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   813
unfolding imp_conv_disj by(rule ccpo.admissible_disj)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   814
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   815
lemma admissible_imp [cont_intro]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   816
  "(Q \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x))
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   817
  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. Q \<longrightarrow> P x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   818
by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   819
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   820
lemma admissible_not_mem' [THEN admissible_subst, cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   821
  shows admissible_not_mem: "ccpo.admissible Union op \<subseteq> (\<lambda>A. x \<notin> A)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   822
by(rule ccpo.admissibleI) auto
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   823
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   824
lemma admissible_eqI:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   825
  assumes f: "cont luba orda lub ord (\<lambda>x. f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   826
  and g: "cont luba orda lub ord (\<lambda>x. g x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   827
  shows "ccpo.admissible luba orda (\<lambda>x. f x = g x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   828
apply(rule ccpo.admissibleI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   829
apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   830
done
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   831
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   832
corollary admissible_eq_mcontI [cont_intro]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   833
  "\<lbrakk> mcont luba orda lub ord (\<lambda>x. f x); 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   834
    mcont luba orda lub ord (\<lambda>x. g x) \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   835
  \<Longrightarrow> ccpo.admissible luba orda (\<lambda>x. f x = g x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   836
by(rule admissible_eqI)(auto simp add: mcont_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   837
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   838
lemma admissible_iff [cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   839
  "\<lbrakk> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x); ccpo.admissible lub ord (\<lambda>x. Q x \<longrightarrow> P x) \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   840
  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longleftrightarrow> Q x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   841
by(subst iff_conv_conj_imp)(rule admissible_conj)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   842
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   843
context ccpo begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   844
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   845
lemma admissible_leI:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   846
  assumes f: "mcont luba orda Sup op \<le> (\<lambda>x. f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   847
  and g: "mcont luba orda Sup op \<le> (\<lambda>x. g x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   848
  shows "ccpo.admissible luba orda (\<lambda>x. f x \<le> g x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   849
proof(rule ccpo.admissibleI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   850
  fix A
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   851
  assume chain: "Complete_Partial_Order.chain orda A"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   852
    and le: "\<forall>x\<in>A. f x \<le> g x"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   853
    and False: "A \<noteq> {}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   854
  have "f (luba A) = \<Squnion>(f ` A)" by(simp add: mcont_contD[OF f] chain False)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   855
  also have "\<dots> \<le> \<Squnion>(g ` A)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   856
  proof(rule ccpo_Sup_least)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   857
    from chain show "Complete_Partial_Order.chain op \<le> (f ` A)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   858
      by(rule chain_imageI)(rule mcont_monoD[OF f])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   859
    
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   860
    fix x
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   861
    assume "x \<in> f ` A"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   862
    then obtain y where "y \<in> A" "x = f y" by blast note this(2)
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   863
    also have "f y \<le> g y" using le \<open>y \<in> A\<close> by simp
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   864
    also have "Complete_Partial_Order.chain op \<le> (g ` A)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   865
      using chain by(rule chain_imageI)(rule mcont_monoD[OF g])
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   866
    hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> A\<close>)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   867
    finally show "x \<le> \<dots>" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   868
  qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   869
  also have "\<dots> = g (luba A)" by(simp add: mcont_contD[OF g] chain False)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   870
  finally show "f (luba A) \<le> g (luba A)" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   871
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   872
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   873
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   874
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   875
lemma admissible_leI:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   876
  fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or>_" [900] 900)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   877
  assumes "class.ccpo lub op \<sqsubseteq> (mk_less op \<sqsubseteq>)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   878
  and "mcont luba orda lub op \<sqsubseteq> (\<lambda>x. f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   879
  and "mcont luba orda lub op \<sqsubseteq> (\<lambda>x. g x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   880
  shows "ccpo.admissible luba orda (\<lambda>x. f x \<sqsubseteq> g x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   881
using assms by(rule ccpo.admissible_leI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   882
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   883
declare ccpo_class.admissible_leI[cont_intro]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   884
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   885
context ccpo begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   886
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   887
lemma admissible_not_below: "ccpo.admissible Sup op \<le> (\<lambda>x. \<not> op \<le> x y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   888
by(rule ccpo.admissibleI)(simp add: ccpo_Sup_below_iff)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   889
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   890
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   891
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   892
lemma (in preorder) preorder [cont_intro, simp]: "class.preorder op \<le> (mk_less op \<le>)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   893
by(unfold_locales)(auto simp add: mk_less_def intro: order_trans)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   894
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   895
context partial_function_definitions begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   896
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   897
lemmas [cont_intro, simp] =
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   898
  admissible_leI[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   899
  ccpo.admissible_not_below[THEN admissible_subst, OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   900
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   901
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   902
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   903
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   904
inductive compact :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   905
  for lub ord x 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   906
where compact:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   907
  "\<lbrakk> ccpo.admissible lub ord (\<lambda>y. \<not> ord x y);
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   908
     ccpo.admissible lub ord (\<lambda>y. x \<noteq> y) \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   909
  \<Longrightarrow> compact lub ord x"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   910
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   911
hide_fact (open) compact
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   912
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   913
context ccpo begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   914
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   915
lemma compactI:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   916
  assumes "ccpo.admissible Sup op \<le> (\<lambda>y. \<not> x \<le> y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   917
  shows "compact Sup op \<le> x"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   918
using assms
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   919
proof(rule compact.intros)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   920
  have neq: "(\<lambda>y. x \<noteq> y) = (\<lambda>y. \<not> x \<le> y \<or> \<not> y \<le> x)" by(auto)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   921
  show "ccpo.admissible Sup op \<le> (\<lambda>y. x \<noteq> y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   922
    by(subst neq)(rule admissible_disj admissible_not_below assms)+
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   923
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   924
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   925
lemma compact_bot:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   926
  assumes "x = Sup {}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   927
  shows "compact Sup op \<le> x"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   928
proof(rule compactI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   929
  show "ccpo.admissible Sup op \<le> (\<lambda>y. \<not> x \<le> y)" using assms
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   930
    by(auto intro!: ccpo.admissibleI intro: ccpo_Sup_least chain_empty)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   931
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   932
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   933
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   934
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   935
lemma admissible_compact_neq' [THEN admissible_subst, cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   936
  shows admissible_compact_neq: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. k \<noteq> x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   937
by(simp add: compact.simps)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   938
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   939
lemma admissible_neq_compact' [THEN admissible_subst, cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   940
  shows admissible_neq_compact: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. x \<noteq> k)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   941
by(subst eq_commute)(rule admissible_compact_neq)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   942
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   943
context partial_function_definitions begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   944
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   945
lemmas [cont_intro, simp] = ccpo.compact_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   946
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   947
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   948
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   949
context ccpo begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   950
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   951
lemma fixp_strong_induct:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   952
  assumes [cont_intro]: "ccpo.admissible Sup op \<le> P"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   953
  and mono: "monotone op \<le> op \<le> f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   954
  and bot: "P (\<Squnion>{})"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   955
  and step: "\<And>x. \<lbrakk> x \<le> ccpo_class.fixp f; P x \<rbrakk> \<Longrightarrow> P (f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   956
  shows "P (ccpo_class.fixp f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   957
proof(rule fixp_induct[where P="\<lambda>x. x \<le> ccpo_class.fixp f \<and> P x", THEN conjunct2])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   958
  note [cont_intro] = admissible_leI
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   959
  show "ccpo.admissible Sup op \<le> (\<lambda>x. x \<le> ccpo_class.fixp f \<and> P x)" by simp
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   960
next
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   961
  show "\<Squnion>{} \<le> ccpo_class.fixp f \<and> P (\<Squnion>{})"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   962
    by(auto simp add: bot intro: ccpo_Sup_least chain_empty)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   963
next
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   964
  fix x
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   965
  assume "x \<le> ccpo_class.fixp f \<and> P x"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   966
  thus "f x \<le> ccpo_class.fixp f \<and> P (f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   967
    by(subst fixp_unfold[OF mono])(auto dest: monotoneD[OF mono] intro: step)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   968
qed(rule mono)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   969
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   970
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   971
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   972
context partial_function_definitions begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   973
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   974
lemma fixp_strong_induct_uc:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   975
  fixes F :: "'c \<Rightarrow> 'c"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   976
    and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   977
    and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   978
    and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   979
  assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   980
    and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   981
    and inverse: "\<And>f. U (C f) = f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   982
    and adm: "ccpo.admissible lub_fun le_fun P"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   983
    and bot: "P (\<lambda>_. lub {})"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   984
    and step: "\<And>f'. \<lbrakk> P (U f'); le_fun (U f') (U f) \<rbrakk> \<Longrightarrow> P (U (F f'))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   985
  shows "P (U f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   986
unfolding eq inverse
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   987
apply (rule ccpo.fixp_strong_induct[OF ccpo adm])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   988
apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   989
apply (rule_tac f'5="C x" in step)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   990
apply (simp_all add: inverse eq)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   991
done
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   992
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   993
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   994
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
   995
subsection \<open>@{term "op ="} as order\<close>
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   996
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   997
definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   998
where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
   999
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1000
definition the_Sup :: "'a set \<Rightarrow> 'a"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1001
where "the_Sup A = (THE a. a \<in> A)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1002
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1003
lemma lub_singleton_the_Sup [cont_intro, simp]: "lub_singleton the_Sup"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1004
by(simp add: lub_singleton_def the_Sup_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1005
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1006
lemma (in ccpo) lub_singleton: "lub_singleton Sup"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1007
by(simp add: lub_singleton_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1008
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1009
lemma (in partial_function_definitions) lub_singleton [cont_intro, simp]: "lub_singleton lub"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1010
by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1011
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1012
lemma preorder_eq [cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1013
  "class.preorder op = (mk_less op =)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1014
by(unfold_locales)(simp_all add: mk_less_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1015
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1016
lemma monotone_eqI [cont_intro]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1017
  assumes "class.preorder ord (mk_less ord)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1018
  shows "monotone op = ord f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1019
proof -
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1020
  interpret preorder ord "mk_less ord" by fact
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1021
  show ?thesis by(simp add: monotone_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1022
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1023
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1024
lemma cont_eqI [cont_intro]: 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1025
  fixes f :: "'a \<Rightarrow> 'b"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1026
  assumes "lub_singleton lub"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1027
  shows "cont the_Sup op = lub ord f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1028
proof(rule contI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1029
  fix Y :: "'a set"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1030
  assume "Complete_Partial_Order.chain op = Y" "Y \<noteq> {}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1031
  then obtain a where "Y = {a}" by(auto simp add: chain_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1032
  thus "f (the_Sup Y) = lub (f ` Y)" using assms
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1033
    by(simp add: the_Sup_def lub_singleton_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1034
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1035
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1036
lemma mcont_eqI [cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1037
  "\<lbrakk> class.preorder ord (mk_less ord); lub_singleton lub \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1038
  \<Longrightarrow> mcont the_Sup op = lub ord f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1039
by(simp add: mcont_def cont_eqI monotone_eqI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1040
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
  1041
subsection \<open>ccpo for products\<close>
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1042
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1043
definition prod_lub :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1044
where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1045
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1046
lemma lub_singleton_prod_lub [cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1047
  "\<lbrakk> lub_singleton luba; lub_singleton lubb \<rbrakk> \<Longrightarrow> lub_singleton (prod_lub luba lubb)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1048
by(simp add: lub_singleton_def prod_lub_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1049
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1050
lemma prod_lub_empty [simp]: "prod_lub luba lubb {} = (luba {}, lubb {})"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1051
by(simp add: prod_lub_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1052
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1053
lemma preorder_rel_prodI [cont_intro, simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1054
  assumes "class.preorder orda (mk_less orda)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1055
  and "class.preorder ordb (mk_less ordb)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1056
  shows "class.preorder (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1057
proof -
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1058
  interpret a: preorder orda "mk_less orda" by fact
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1059
  interpret b: preorder ordb "mk_less ordb" by fact
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1060
  show ?thesis by(unfold_locales)(auto simp add: mk_less_def intro: a.order_trans b.order_trans)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1061
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1062
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1063
lemma order_rel_prodI:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1064
  assumes a: "class.order orda (mk_less orda)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1065
  and b: "class.order ordb (mk_less ordb)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1066
  shows "class.order (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1067
  (is "class.order ?ord ?ord'")
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1068
proof(intro class.order.intro class.order_axioms.intro)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1069
  interpret a: order orda "mk_less orda" by(fact a)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1070
  interpret b: order ordb "mk_less ordb" by(fact b)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1071
  show "class.preorder ?ord ?ord'" by(rule preorder_rel_prodI) unfold_locales
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1072
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1073
  fix x y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1074
  assume "?ord x y" "?ord y x"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1075
  thus "x = y" by(cases x y rule: prod.exhaust[case_product prod.exhaust]) auto
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1076
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1077
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1078
lemma monotone_rel_prodI:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1079
  assumes mono2: "\<And>a. monotone ordb ordc (\<lambda>b. f (a, b))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1080
  and mono1: "\<And>b. monotone orda ordc (\<lambda>a. f (a, b))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1081
  and a: "class.preorder orda (mk_less orda)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1082
  and b: "class.preorder ordb (mk_less ordb)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1083
  and c: "class.preorder ordc (mk_less ordc)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1084
  shows "monotone (rel_prod orda ordb) ordc f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1085
proof -
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1086
  interpret a: preorder orda "mk_less orda" by(rule a)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1087
  interpret b: preorder ordb "mk_less ordb" by(rule b)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1088
  interpret c: preorder ordc "mk_less ordc" by(rule c)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1089
  show ?thesis using mono2 mono1
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1090
    by(auto 7 2 simp add: monotone_def intro: c.order_trans)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1091
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1092
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1093
lemma monotone_rel_prodD1:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1094
  assumes mono: "monotone (rel_prod orda ordb) ordc f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1095
  and preorder: "class.preorder ordb (mk_less ordb)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1096
  shows "monotone orda ordc (\<lambda>a. f (a, b))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1097
proof -
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1098
  interpret preorder ordb "mk_less ordb" by(rule preorder)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1099
  show ?thesis using mono by(simp add: monotone_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1100
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1101
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1102
lemma monotone_rel_prodD2:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1103
  assumes mono: "monotone (rel_prod orda ordb) ordc f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1104
  and preorder: "class.preorder orda (mk_less orda)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1105
  shows "monotone ordb ordc (\<lambda>b. f (a, b))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1106
proof -
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1107
  interpret preorder orda "mk_less orda" by(rule preorder)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1108
  show ?thesis using mono by(simp add: monotone_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1109
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1110
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1111
lemma monotone_case_prodI:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1112
  "\<lbrakk> \<And>a. monotone ordb ordc (f a); \<And>b. monotone orda ordc (\<lambda>a. f a b);
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1113
    class.preorder orda (mk_less orda); class.preorder ordb (mk_less ordb);
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1114
    class.preorder ordc (mk_less ordc) \<rbrakk>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1115
  \<Longrightarrow> monotone (rel_prod orda ordb) ordc (case_prod f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1116
by(rule monotone_rel_prodI) simp_all
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1117
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1118
lemma monotone_case_prodD1:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1119
  assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1120
  and preorder: "class.preorder ordb (mk_less ordb)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1121
  shows "monotone orda ordc (\<lambda>a. f a b)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1122
using monotone_rel_prodD1[OF assms] by simp
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1123
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1124
lemma monotone_case_prodD2:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1125
  assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1126
  and preorder: "class.preorder orda (mk_less orda)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1127
  shows "monotone ordb ordc (f a)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1128
using monotone_rel_prodD2[OF assms] by simp
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1129
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1130
context 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1131
  fixes orda ordb ordc
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1132
  assumes a: "class.preorder orda (mk_less orda)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1133
  and b: "class.preorder ordb (mk_less ordb)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1134
  and c: "class.preorder ordc (mk_less ordc)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1135
begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1136
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1137
lemma monotone_rel_prod_iff:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1138
  "monotone (rel_prod orda ordb) ordc f \<longleftrightarrow>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1139
   (\<forall>a. monotone ordb ordc (\<lambda>b. f (a, b))) \<and> 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1140
   (\<forall>b. monotone orda ordc (\<lambda>a. f (a, b)))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1141
using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1142
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1143
lemma monotone_case_prod_iff [simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1144
  "monotone (rel_prod orda ordb) ordc (case_prod f) \<longleftrightarrow>
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1145
   (\<forall>a. monotone ordb ordc (f a)) \<and> (\<forall>b. monotone orda ordc (\<lambda>a. f a b))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1146
by(simp add: monotone_rel_prod_iff)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1147
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1148
end
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1149
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1150
lemma monotone_case_prod_apply_iff:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1151
  "monotone orda ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1152
by(simp add: monotone_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1153
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1154
lemma monotone_case_prod_applyD:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1155
  "monotone orda ordb (\<lambda>x. (case_prod f x) y)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1156
  \<Longrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1157
by(simp add: monotone_case_prod_apply_iff)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1158
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1159
lemma monotone_case_prod_applyI:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1160
  "monotone orda ordb (case_prod (\<lambda>a b. f a b y))
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1161
  \<Longrightarrow> monotone orda ordb (\<lambda>x. (case_prod f x) y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1162
by(simp add: monotone_case_prod_apply_iff)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1163
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1164
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1165
lemma cont_case_prod_apply_iff:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1166
  "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))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1167
by(simp add: cont_def split_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1168
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1169
lemma cont_case_prod_applyI:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1170
  "cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1171
  \<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1172
by(simp add: cont_case_prod_apply_iff)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1173
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1174
lemma cont_case_prod_applyD:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1175
  "cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1176
  \<Longrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1177
by(simp add: cont_case_prod_apply_iff)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1178
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1179
lemma mcont_case_prod_apply_iff [simp]:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1180
  "mcont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1181
   mcont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1182
by(simp add: mcont_def monotone_case_prod_apply_iff cont_case_prod_apply_iff)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1183
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1184
lemma cont_prodD1: 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1185
  assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1186
  and "class.preorder orda (mk_less orda)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1187
  and luba: "lub_singleton luba"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1188
  shows "cont lubb ordb lubc ordc (\<lambda>y. f (x, y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1189
proof(rule contI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1190
  interpret preorder orda "mk_less orda" by fact
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1191
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1192
  fix Y :: "'b set"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1193
  let ?Y = "{x} \<times> Y"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1194
  assume "Complete_Partial_Order.chain ordb Y" "Y \<noteq> {}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1195
  hence "Complete_Partial_Order.chain (rel_prod orda ordb) ?Y" "?Y \<noteq> {}" 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1196
    by(simp_all add: chain_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1197
  with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1198
  moreover have "f ` ?Y = (\<lambda>y. f (x, y)) ` Y" by auto
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1199
  ultimately show "f (x, lubb Y) = lubc ((\<lambda>y. f (x, y)) ` Y)" using luba
62837
237ef2bab6c7 isabelle update_cartouches -c -t;
wenzelm
parents: 62652
diff changeset
  1200
    by(simp add: prod_lub_def \<open>Y \<noteq> {}\<close> lub_singleton_def)
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1201
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1202
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1203
lemma cont_prodD2: 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1204
  assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1205
  and "class.preorder ordb (mk_less ordb)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1206
  and lubb: "lub_singleton lubb"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1207
  shows "cont luba orda lubc ordc (\<lambda>x. f (x, y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1208
proof(rule contI)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1209
  interpret preorder ordb "mk_less ordb" by fact
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1210
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1211
  fix Y
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1212
  assume Y: "Complete_Partial_Order.chain orda Y" "Y \<noteq> {}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1213
  let ?Y = "Y \<times> {y}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1214
  have "f (luba Y, y) = f (prod_lub luba lubb ?Y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1215
    using lubb by(simp add: prod_lub_def Y lub_singleton_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1216
  also from Y have "Complete_Partial_Order.chain (rel_prod orda ordb) ?Y" "?Y \<noteq> {}"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1217
    by(simp_all add: chain_def)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1218
  with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1219
  also have "f ` ?Y = (\<lambda>x. f (x, y)) ` Y" by auto
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1220
  finally show "f (luba Y, y) = lubc \<dots>" .
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1221
qed
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1222
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1223
lemma cont_case_prodD1:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1224
  assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1225
  and "class.preorder orda (mk_less orda)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1226
  and "lub_singleton luba"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1227
  shows "cont lubb ordb lubc ordc (f x)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1228
using cont_prodD1[OF assms] by simp
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1229
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1230
lemma cont_case_prodD2:
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1231
  assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1232
  and "class.preorder ordb (mk_less ordb)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1233
  and "lub_singleton lubb"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1234
  shows "cont luba orda lubc ordc (\<lambda>x. f x y)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1235
using cont_prodD2[OF assms] by simp
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1236
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1237
context ccpo begin
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1238
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1239
lemma cont_prodI: 
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1240
  assumes mono: "monotone (rel_prod orda ordb) op \<le> f"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1241
  and cont1: "\<And>x. cont lubb ordb Sup op \<le> (\<lambda>y. f (x, y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1242
  and cont2: "\<And>y. cont luba orda Sup op \<le> (\<lambda>x. f (x, y))"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1243
  and "class.preorder orda (mk_less orda)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff changeset
  1244
  and "class.preorder ordb (mk_less ordb)"
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff