author | Andreas Lochbihler |
Fri, 18 Mar 2016 08:01:49 +0100 | |
changeset 62652 | 7248d106c607 |
child 62837 | 237ef2bab6c7 |
permissions | -rw-r--r-- |
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
1 |
(* Title: src/HOL/Library/Complete_Partial_Order2 |
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 |
|
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
5 |
section {* Formalisation of chain-complete partial orders, continuity and admissibility *} |
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 |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
86 |
note `x' = f x` also |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
87 |
from `f \<in> Y` `x \<sqsubseteq> y` have "f x \<le> f y" by(blast dest: mono monotoneD) |
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'' |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
89 |
by(rule ccpo_Sup_upper)(simp add: `f \<in> Y`) |
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) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
111 |
also from mono1[OF `y' \<in> Y`] le have "\<dots> \<le> f y y'" by(rule monotoneD) |
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] |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
113 |
by (auto intro!: ccpo_Sup_upper simp add: `y' \<in> Y`) |
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) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
131 |
also have "\<dots> \<le> ?rhs" using chain2[OF `y' \<in> Y`] |
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 |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
136 |
def y'' \<equiv> "if y \<sqsubseteq> y' then y' else y" |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
137 |
from chain `y \<in> Y` `y' \<in> Y` have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
138 |
hence "f y' y \<le> f y'' y''" using `y \<in> Y` `y' \<in> Y` |
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]) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
140 |
also from `y \<in> Y` `y' \<in> Y` have "y'' \<in> Y" by(simp add: y''_def) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
141 |
from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: `y'' \<in> Y`) |
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) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
152 |
also from chain2[OF `x \<in> Y`] have "\<dots> \<le> \<Squnion>(f x ` Y)" |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
153 |
by(rule ccpo_Sup_upper)(simp add: `x \<in> Y`) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
154 |
also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: `x \<in> Y`) |
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) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
174 |
also have "y \<sqsubseteq> \<Or>Y" using ccpo chain `y \<in> Y` by(rule ccpo.ccpo_Sup_upper) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
175 |
hence "f y \<le> f (\<Or>Y)" using `y \<in> Y` by(rule mono) |
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" |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
199 |
from chain1[OF `f \<in> Z`] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)" |
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) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
204 |
also have "\<dots> \<le> g y" using `fun_ord op \<le> f g` by(simp add: fun_ord_def) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
205 |
also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF `g \<in> Z`] |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
206 |
by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`) |
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) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
222 |
also have "f x \<le> f y" using `f \<in> Z` `x \<sqsubseteq> y` by(rule monotoneD[OF mono]) |
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 |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
224 |
by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`) |
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) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
234 |
also have "\<dots> \<le> ?rhs" using chain1[OF `f \<in> Z`] |
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 |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
240 |
by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
241 |
also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`) |
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) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
257 |
also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF `f \<in> Z`] |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
258 |
by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
259 |
also have "\<dots> \<le> ?lhs" using chain2 |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
260 |
by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`) |
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" |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
317 |
by(rule monotoneD[OF iterates_mono[OF `f \<in> ?iter` mono2]])(blast intro: `x \<sqsubseteq> y`)+ |
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 |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
319 |
by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`) |
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 |
|
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
336 |
subsection {* Continuity *} |
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 |
|
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
348 |
subsubsection {* Theorem collection @{text cont_intro} *} |
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" |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
351 |
ML {* |
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 |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
377 |
*} |
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" |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
383 |
) = {* K cont_intro_simproc *} |
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) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
607 |
also from _ `x \<sqsubseteq> y` have "f x \<le> f y" |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
608 |
by(rule mcont_monoD[OF iterates_mcont[OF `f \<in> ?iter` mcont]]) |
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 |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
610 |
by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`) |
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 |
|
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
786 |
subsection {* Admissibility *} |
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) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
863 |
also have "f y \<le> g y" using le `y \<in> A` by simp |
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]) |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
866 |
hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: `y \<in> A`) |
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 |
|
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
995 |
subsection {* @{term "op ="} as order *} |
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 |
|
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
1041 |
subsection {* ccpo for products *} |
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 |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset
|
1200 |
by(simp add: prod_lub_def `Y \<noteq> {}` lub_singleton_def) |
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:
|