author | Manuel Eberl <eberlm@in.tum.de> |
Fri, 29 Mar 2024 19:28:59 +0100 | |
changeset 80061 | 4c1347e172b1 |
parent 69872 | bb16c0bb7520 |
permissions | -rw-r--r-- |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
1 |
(* Title: HOL/Library/Order_Continuity.thy |
62373 | 2 |
Author: David von Oheimb, TU München |
3 |
Author: Johannes Hölzl, TU München |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
4 |
*) |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
5 |
|
62373 | 6 |
section \<open>Continuity and iterations\<close> |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
7 |
|
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
8 |
theory Order_Continuity |
62373 | 9 |
imports Complex_Main Countable_Complete_Lattices |
15131 | 10 |
begin |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
11 |
|
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
12 |
(* TODO: Generalize theory to chain-complete partial orders *) |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
13 |
|
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
14 |
lemma SUP_nat_binary: |
69661 | 15 |
"(sup A (SUP x\<in>Collect ((<) (0::nat)). B)) = (sup A B::'a::countable_complete_lattice)" |
16 |
apply (subst image_constant) |
|
17 |
apply auto |
|
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
18 |
done |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
19 |
|
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
20 |
lemma INF_nat_binary: |
69661 | 21 |
"inf A (INF x\<in>Collect ((<) (0::nat)). B) = (inf A B::'a::countable_complete_lattice)" |
22 |
apply (subst image_constant) |
|
23 |
apply auto |
|
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
24 |
done |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
25 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
26 |
text \<open> |
61585 | 27 |
The name \<open>continuous\<close> is already taken in \<open>Complex_Main\<close>, so we use |
28 |
\<open>sup_continuous\<close> and \<open>inf_continuous\<close>. These names appear sometimes in literature |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
29 |
and have the advantage that these names are duals. |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
30 |
\<close> |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
31 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
32 |
named_theorems order_continuous_intros |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
33 |
|
60500 | 34 |
subsection \<open>Continuity for complete lattices\<close> |
21312 | 35 |
|
22367 | 36 |
definition |
62373 | 37 |
sup_continuous :: "('a::countable_complete_lattice \<Rightarrow> 'b::countable_complete_lattice) \<Rightarrow> bool" |
38 |
where |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
39 |
"sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))" |
22367 | 40 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
41 |
lemma sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))" |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
42 |
by (auto simp: sup_continuous_def) |
21312 | 43 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
44 |
lemma sup_continuous_mono: |
69661 | 45 |
"mono F" if "sup_continuous F" |
21312 | 46 |
proof |
69661 | 47 |
fix A B :: "'a" |
48 |
assume "A \<le> B" |
|
49 |
let ?f = "\<lambda>n::nat. if n = 0 then A else B" |
|
50 |
from \<open>A \<le> B\<close> have "incseq ?f" |
|
51 |
by (auto intro: monoI) |
|
52 |
with \<open>sup_continuous F\<close> have *: "F (SUP i. ?f i) = (SUP i. F (?f i))" |
|
53 |
by (auto dest: sup_continuousD) |
|
54 |
from \<open>A \<le> B\<close> have "B = sup A B" |
|
55 |
by (simp add: le_iff_sup) |
|
56 |
then have "F B = F (sup A B)" |
|
57 |
by simp |
|
58 |
also have "\<dots> = sup (F A) (F B)" |
|
59 |
using * by (simp add: if_distrib SUP_nat_binary cong del: SUP_cong) |
|
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
60 |
finally show "F A \<le> F B" |
69661 | 61 |
by (simp add: le_iff_sup) |
21312 | 62 |
qed |
63 |
||
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
64 |
lemma [order_continuous_intros]: |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
65 |
shows sup_continuous_const: "sup_continuous (\<lambda>x. c)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
66 |
and sup_continuous_id: "sup_continuous (\<lambda>x. x)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
67 |
and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
68 |
and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P" |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
69 |
and sup_continuous_If: "sup_continuous F \<Longrightarrow> sup_continuous G \<Longrightarrow> sup_continuous (\<lambda>f. if C then F f else G f)" |
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69661
diff
changeset
|
70 |
by (auto simp: sup_continuous_def image_comp) |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
71 |
|
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
72 |
lemma sup_continuous_compose: |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
73 |
assumes f: "sup_continuous f" and g: "sup_continuous g" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
74 |
shows "sup_continuous (\<lambda>x. f (g x))" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
75 |
unfolding sup_continuous_def |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
76 |
proof safe |
63540 | 77 |
fix M :: "nat \<Rightarrow> 'c" |
78 |
assume M: "mono M" |
|
79 |
then have "mono (\<lambda>i. g (M i))" |
|
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
80 |
using sup_continuous_mono[OF g] by (auto simp: mono_def) |
69313 | 81 |
with M show "f (g (Sup (M ` UNIV))) = (SUP i. f (g (M i)))" |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
82 |
by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD]) |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
83 |
qed |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
84 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
85 |
lemma sup_continuous_sup[order_continuous_intros]: |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
86 |
"sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))" |
62373 | 87 |
by (simp add: sup_continuous_def ccSUP_sup_distrib) |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
88 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
89 |
lemma sup_continuous_inf[order_continuous_intros]: |
62373 | 90 |
fixes P Q :: "'a :: countable_complete_lattice \<Rightarrow> 'b :: countable_complete_distrib_lattice" |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
91 |
assumes P: "sup_continuous P" and Q: "sup_continuous Q" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
92 |
shows "sup_continuous (\<lambda>x. inf (P x) (Q x))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
93 |
unfolding sup_continuous_def |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
94 |
proof (safe intro!: antisym) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
95 |
fix M :: "nat \<Rightarrow> 'a" assume M: "incseq M" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
96 |
have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP j i. inf (P (M i)) (Q (M j)))" |
62373 | 97 |
by (simp add: sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_ccSUP ccSUP_inf) |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
98 |
also have "\<dots> \<le> (SUP i. inf (P (M i)) (Q (M i)))" |
62373 | 99 |
proof (intro ccSUP_least) |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
100 |
fix i j from M assms[THEN sup_continuous_mono] show "inf (P (M i)) (Q (M j)) \<le> (SUP i. inf (P (M i)) (Q (M i)))" |
62373 | 101 |
by (intro ccSUP_upper2[of _ "sup i j"] inf_mono) (auto simp: mono_def) |
102 |
qed auto |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
103 |
finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP i. inf (P (M i)) (Q (M i)))" . |
62373 | 104 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
105 |
show "(SUP i. inf (P (M i)) (Q (M i))) \<le> inf (P (SUP i. M i)) (Q (SUP i. M i))" |
62373 | 106 |
unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro ccSUP_least inf_mono ccSUP_upper) auto |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
107 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
108 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
109 |
lemma sup_continuous_and[order_continuous_intros]: |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
110 |
"sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<and> Q x)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
111 |
using sup_continuous_inf[of P Q] by simp |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
112 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
113 |
lemma sup_continuous_or[order_continuous_intros]: |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
114 |
"sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<or> Q x)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
115 |
by (auto simp: sup_continuous_def) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
116 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
117 |
lemma sup_continuous_lfp: |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
118 |
assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U") |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
119 |
proof (rule antisym) |
60500 | 120 |
note mono = sup_continuous_mono[OF \<open>sup_continuous F\<close>] |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
121 |
show "?U \<le> lfp F" |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
122 |
proof (rule SUP_least) |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
123 |
fix i show "(F ^^ i) bot \<le> lfp F" |
21312 | 124 |
proof (induct i) |
125 |
case (Suc i) |
|
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
126 |
have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
127 |
also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc]) |
63979 | 128 |
also have "\<dots> = lfp F" by (simp add: lfp_fixpoint[OF mono]) |
21312 | 129 |
finally show ?case . |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
130 |
qed simp |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
131 |
qed |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
132 |
show "lfp F \<le> ?U" |
21312 | 133 |
proof (rule lfp_lowerbound) |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
134 |
have "mono (\<lambda>i::nat. (F ^^ i) bot)" |
21312 | 135 |
proof - |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
136 |
{ fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
137 |
proof (induct i) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
138 |
case 0 show ?case by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
139 |
next |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
140 |
case Suc thus ?case using monoD[OF mono Suc] by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
141 |
qed } |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
142 |
thus ?thesis by (auto simp add: mono_iff_le_Suc) |
21312 | 143 |
qed |
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
144 |
hence "F ?U = (SUP i. (F ^^ Suc i) bot)" |
60500 | 145 |
using \<open>sup_continuous F\<close> by (simp add: sup_continuous_def) |
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
146 |
also have "\<dots> \<le> ?U" |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
147 |
by (fast intro: SUP_least SUP_upper) |
21312 | 148 |
finally show "F ?U \<le> ?U" . |
149 |
qed |
|
150 |
qed |
|
151 |
||
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
152 |
lemma lfp_transfer_bounded: |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
153 |
assumes P: "P bot" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. (\<And>i. P (M i)) \<Longrightarrow> P (SUP i::nat. M i)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
154 |
assumes \<alpha>: "\<And>M. mono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (SUP i. M i) = (SUP i. \<alpha> (M i))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
155 |
assumes f: "sup_continuous f" and g: "sup_continuous g" |
60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
156 |
assumes [simp]: "\<And>x. P x \<Longrightarrow> x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)" |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
157 |
assumes g_bound: "\<And>x. \<alpha> bot \<le> g x" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
158 |
shows "\<alpha> (lfp f) = lfp g" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
159 |
proof (rule antisym) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
160 |
note mono_g = sup_continuous_mono[OF g] |
60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
161 |
note mono_f = sup_continuous_mono[OF f] |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
162 |
have lfp_bound: "\<alpha> bot \<le> lfp g" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
163 |
by (subst lfp_unfold[OF mono_g]) (rule g_bound) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
164 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
165 |
have P_pow: "P ((f ^^ i) bot)" for i |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
166 |
by (induction i) (auto intro!: P) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
167 |
have incseq_pow: "mono (\<lambda>i. (f ^^ i) bot)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
168 |
unfolding mono_iff_le_Suc |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
169 |
proof |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
170 |
fix i show "(f ^^ i) bot \<le> (f ^^ (Suc i)) bot" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
171 |
proof (induct i) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
172 |
case Suc thus ?case using monoD[OF sup_continuous_mono[OF f] Suc] by auto |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
173 |
qed (simp add: le_fun_def) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
174 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
175 |
have P_lfp: "P (lfp f)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
176 |
using P_pow unfolding sup_continuous_lfp[OF f] by (auto intro!: P) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
177 |
|
60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
178 |
have iter_le_lfp: "(f ^^ n) bot \<le> lfp f" for n |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
179 |
apply (induction n) |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
180 |
apply simp |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
181 |
apply (subst lfp_unfold[OF mono_f]) |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
182 |
apply (auto intro!: monoD[OF mono_f]) |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
183 |
done |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
184 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
185 |
have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
186 |
unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule \<alpha>) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
187 |
also have "\<dots> \<le> lfp g" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
188 |
proof (rule SUP_least) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
189 |
fix i show "\<alpha> ((f^^i) bot) \<le> lfp g" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
190 |
proof (induction i) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
191 |
case (Suc n) then show ?case |
60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
192 |
by (subst lfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow iter_le_lfp) |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
193 |
qed (simp add: lfp_bound) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
194 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
195 |
finally show "\<alpha> (lfp f) \<le> lfp g" . |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
196 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
197 |
show "lfp g \<le> \<alpha> (lfp f)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
198 |
proof (induction rule: lfp_ordinal_induct[OF mono_g]) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
199 |
case (1 S) then show ?case |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
200 |
by (subst lfp_unfold[OF sup_continuous_mono[OF f]]) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
201 |
(simp add: monoD[OF mono_g] P_lfp) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
202 |
qed (auto intro: Sup_least) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
203 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
204 |
|
60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
205 |
lemma lfp_transfer: |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
206 |
"sup_continuous \<alpha> \<Longrightarrow> sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
207 |
(\<And>x. \<alpha> bot \<le> g x) \<Longrightarrow> (\<And>x. x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)) \<Longrightarrow> \<alpha> (lfp f) = lfp g" |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
208 |
by (rule lfp_transfer_bounded[where P=top]) (auto dest: sup_continuousD) |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
209 |
|
19736 | 210 |
definition |
62373 | 211 |
inf_continuous :: "('a::countable_complete_lattice \<Rightarrow> 'b::countable_complete_lattice) \<Rightarrow> bool" |
212 |
where |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
213 |
"inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
214 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
215 |
lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))" |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
216 |
by (auto simp: inf_continuous_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
217 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
218 |
lemma inf_continuous_mono: |
69661 | 219 |
"mono F" if "inf_continuous F" |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
220 |
proof |
69661 | 221 |
fix A B :: "'a" |
222 |
assume "A \<le> B" |
|
223 |
let ?f = "\<lambda>n::nat. if n = 0 then B else A" |
|
224 |
from \<open>A \<le> B\<close> have "decseq ?f" |
|
225 |
by (auto intro: antimonoI) |
|
226 |
with \<open>inf_continuous F\<close> have *: "F (INF i. ?f i) = (INF i. F (?f i))" |
|
227 |
by (auto dest: inf_continuousD) |
|
228 |
from \<open>A \<le> B\<close> have "A = inf B A" |
|
229 |
by (simp add: inf.absorb_iff2) |
|
230 |
then have "F A = F (inf B A)" |
|
231 |
by simp |
|
232 |
also have "\<dots> = inf (F B) (F A)" |
|
233 |
using * by (simp add: if_distrib INF_nat_binary cong del: INF_cong) |
|
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
234 |
finally show "F A \<le> F B" |
69661 | 235 |
by (simp add: inf.absorb_iff2) |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
236 |
qed |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
237 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
238 |
lemma [order_continuous_intros]: |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
239 |
shows inf_continuous_const: "inf_continuous (\<lambda>x. c)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
240 |
and inf_continuous_id: "inf_continuous (\<lambda>x. x)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
241 |
and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
242 |
and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P" |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
243 |
and inf_continuous_If: "inf_continuous F \<Longrightarrow> inf_continuous G \<Longrightarrow> inf_continuous (\<lambda>f. if C then F f else G f)" |
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69661
diff
changeset
|
244 |
by (auto simp: inf_continuous_def image_comp) |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
245 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
246 |
lemma inf_continuous_inf[order_continuous_intros]: |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
247 |
"inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))" |
62373 | 248 |
by (simp add: inf_continuous_def ccINF_inf_distrib) |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
249 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
250 |
lemma inf_continuous_sup[order_continuous_intros]: |
62373 | 251 |
fixes P Q :: "'a :: countable_complete_lattice \<Rightarrow> 'b :: countable_complete_distrib_lattice" |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
252 |
assumes P: "inf_continuous P" and Q: "inf_continuous Q" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
253 |
shows "inf_continuous (\<lambda>x. sup (P x) (Q x))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
254 |
unfolding inf_continuous_def |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
255 |
proof (safe intro!: antisym) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
256 |
fix M :: "nat \<Rightarrow> 'a" assume M: "decseq M" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
257 |
show "sup (P (INF i. M i)) (Q (INF i. M i)) \<le> (INF i. sup (P (M i)) (Q (M i)))" |
62373 | 258 |
unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro ccINF_greatest sup_mono ccINF_lower) auto |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
259 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
260 |
have "(INF i. sup (P (M i)) (Q (M i))) \<le> (INF j i. sup (P (M i)) (Q (M j)))" |
62373 | 261 |
proof (intro ccINF_greatest) |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
262 |
fix i j from M assms[THEN inf_continuous_mono] show "sup (P (M i)) (Q (M j)) \<ge> (INF i. sup (P (M i)) (Q (M i)))" |
62373 | 263 |
by (intro ccINF_lower2[of _ "sup i j"] sup_mono) (auto simp: mono_def antimono_def) |
264 |
qed auto |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
265 |
also have "\<dots> \<le> sup (P (INF i. M i)) (Q (INF i. M i))" |
62373 | 266 |
by (simp add: inf_continuousD[OF P M] inf_continuousD[OF Q M] ccINF_sup sup_ccINF) |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
267 |
finally show "sup (P (INF i. M i)) (Q (INF i. M i)) \<ge> (INF i. sup (P (M i)) (Q (M i)))" . |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
268 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
269 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
270 |
lemma inf_continuous_and[order_continuous_intros]: |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
271 |
"inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<and> Q x)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
272 |
using inf_continuous_inf[of P Q] by simp |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
273 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
274 |
lemma inf_continuous_or[order_continuous_intros]: |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
275 |
"inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<or> Q x)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
276 |
using inf_continuous_sup[of P Q] by simp |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
277 |
|
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
278 |
lemma inf_continuous_compose: |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
279 |
assumes f: "inf_continuous f" and g: "inf_continuous g" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
280 |
shows "inf_continuous (\<lambda>x. f (g x))" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
281 |
unfolding inf_continuous_def |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
282 |
proof safe |
63540 | 283 |
fix M :: "nat \<Rightarrow> 'c" |
284 |
assume M: "antimono M" |
|
285 |
then have "antimono (\<lambda>i. g (M i))" |
|
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
286 |
using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def) |
69313 | 287 |
with M show "f (g (Inf (M ` UNIV))) = (INF i. f (g (M i)))" |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
288 |
by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD]) |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
289 |
qed |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
290 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
291 |
lemma inf_continuous_gfp: |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
292 |
assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U") |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
293 |
proof (rule antisym) |
60500 | 294 |
note mono = inf_continuous_mono[OF \<open>inf_continuous F\<close>] |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
295 |
show "gfp F \<le> ?U" |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
296 |
proof (rule INF_greatest) |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
297 |
fix i show "gfp F \<le> (F ^^ i) top" |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
298 |
proof (induct i) |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
299 |
case (Suc i) |
63979 | 300 |
have "gfp F = F (gfp F)" by (simp add: gfp_fixpoint[OF mono]) |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
301 |
also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc]) |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
302 |
also have "\<dots> = (F ^^ Suc i) top" by simp |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
303 |
finally show ?case . |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
304 |
qed simp |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
305 |
qed |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
306 |
show "?U \<le> gfp F" |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
307 |
proof (rule gfp_upperbound) |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
308 |
have *: "antimono (\<lambda>i::nat. (F ^^ i) top)" |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
309 |
proof - |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
310 |
{ fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top" |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
311 |
proof (induct i) |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
312 |
case 0 show ?case by simp |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
313 |
next |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
314 |
case Suc thus ?case using monoD[OF mono Suc] by auto |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
315 |
qed } |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
316 |
thus ?thesis by (auto simp add: antimono_iff_le_Suc) |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
317 |
qed |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
318 |
have "?U \<le> (INF i. (F ^^ Suc i) top)" |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
319 |
by (fast intro: INF_greatest INF_lower) |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
320 |
also have "\<dots> \<le> F ?U" |
60500 | 321 |
by (simp add: inf_continuousD \<open>inf_continuous F\<close> *) |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
322 |
finally show "?U \<le> F ?U" . |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
323 |
qed |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset
|
324 |
qed |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
325 |
|
60427 | 326 |
lemma gfp_transfer: |
327 |
assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g" |
|
328 |
assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)" |
|
329 |
shows "\<alpha> (gfp f) = gfp g" |
|
330 |
proof - |
|
331 |
have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))" |
|
332 |
unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono) |
|
333 |
moreover have "\<alpha> ((f^^i) top) = (g^^i) top" for i |
|
334 |
by (induction i; simp) |
|
335 |
ultimately show ?thesis |
|
336 |
unfolding inf_continuous_gfp[OF g] by simp |
|
337 |
qed |
|
338 |
||
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
339 |
lemma gfp_transfer_bounded: |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
340 |
assumes P: "P (f top)" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. antimono M \<Longrightarrow> (\<And>i. P (M i)) \<Longrightarrow> P (INF i::nat. M i)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
341 |
assumes \<alpha>: "\<And>M. antimono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (INF i. M i) = (INF i. \<alpha> (M i))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
342 |
assumes f: "inf_continuous f" and g: "inf_continuous g" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
343 |
assumes [simp]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
344 |
assumes g_bound: "\<And>x. g x \<le> \<alpha> (f top)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
345 |
shows "\<alpha> (gfp f) = gfp g" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
346 |
proof (rule antisym) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
347 |
note mono_g = inf_continuous_mono[OF g] |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
348 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
349 |
have P_pow: "P ((f ^^ i) (f top))" for i |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
350 |
by (induction i) (auto intro!: P) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
351 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
352 |
have antimono_pow: "antimono (\<lambda>i. (f ^^ i) top)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
353 |
unfolding antimono_iff_le_Suc |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
354 |
proof |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
355 |
fix i show "(f ^^ Suc i) top \<le> (f ^^ i) top" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
356 |
proof (induct i) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
357 |
case Suc thus ?case using monoD[OF inf_continuous_mono[OF f] Suc] by auto |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
358 |
qed (simp add: le_fun_def) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
359 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
360 |
have antimono_pow2: "antimono (\<lambda>i. (f ^^ i) (f top))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
361 |
proof |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
362 |
show "x \<le> y \<Longrightarrow> (f ^^ y) (f top) \<le> (f ^^ x) (f top)" for x y |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
363 |
using antimono_pow[THEN antimonoD, of "Suc x" "Suc y"] |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
364 |
unfolding funpow_Suc_right by simp |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
365 |
qed |
62373 | 366 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
367 |
have gfp_f: "gfp f = (INF i. (f ^^ i) (f top))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
368 |
unfolding inf_continuous_gfp[OF f] |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
369 |
proof (rule INF_eq) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
370 |
show "\<exists>j\<in>UNIV. (f ^^ j) (f top) \<le> (f ^^ i) top" for i |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
371 |
by (intro bexI[of _ "i - 1"]) (auto simp: diff_Suc funpow_Suc_right simp del: funpow.simps(2) split: nat.split) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
372 |
show "\<exists>j\<in>UNIV. (f ^^ j) top \<le> (f ^^ i) (f top)" for i |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
373 |
by (intro bexI[of _ "Suc i"]) (auto simp: funpow_Suc_right simp del: funpow.simps(2)) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
374 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
375 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
376 |
have P_lfp: "P (gfp f)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
377 |
unfolding gfp_f by (auto intro!: P P_pow antimono_pow2) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
378 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
379 |
have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) (f top)))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
380 |
unfolding gfp_f by (rule \<alpha>) (auto intro!: P_pow antimono_pow2) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
381 |
also have "\<dots> \<ge> gfp g" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
382 |
proof (rule INF_greatest) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
383 |
fix i show "gfp g \<le> \<alpha> ((f^^i) (f top))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
384 |
proof (induction i) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
385 |
case (Suc n) then show ?case |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
386 |
by (subst gfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
387 |
next |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
388 |
case 0 |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
389 |
have "gfp g \<le> \<alpha> (f top)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
390 |
by (subst gfp_unfold[OF mono_g]) (rule g_bound) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
391 |
then show ?case |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
392 |
by simp |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
393 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
394 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
395 |
finally show "gfp g \<le> \<alpha> (gfp f)" . |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
396 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
397 |
show "\<alpha> (gfp f) \<le> gfp g" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
398 |
proof (induction rule: gfp_ordinal_induct[OF mono_g]) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
399 |
case (1 S) then show ?case |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
400 |
by (subst gfp_unfold[OF inf_continuous_mono[OF f]]) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
401 |
(simp add: monoD[OF mono_g] P_lfp) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
402 |
qed (auto intro: Inf_greatest) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
403 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
404 |
|
62373 | 405 |
subsubsection \<open>Least fixed points in countable complete lattices\<close> |
406 |
||
407 |
definition (in countable_complete_lattice) cclfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" |
|
62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
62373
diff
changeset
|
408 |
where "cclfp f = (SUP i. (f ^^ i) bot)" |
62373 | 409 |
|
410 |
lemma cclfp_unfold: |
|
411 |
assumes "sup_continuous F" shows "cclfp F = F (cclfp F)" |
|
412 |
proof - |
|
62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
62373
diff
changeset
|
413 |
have "cclfp F = (SUP i. F ((F ^^ i) bot))" |
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69661
diff
changeset
|
414 |
unfolding cclfp_def |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69661
diff
changeset
|
415 |
by (subst UNIV_nat_eq) (simp add: image_comp) |
62373 | 416 |
also have "\<dots> = F (cclfp F)" |
417 |
unfolding cclfp_def |
|
418 |
by (intro sup_continuousD[symmetric] assms mono_funpow sup_continuous_mono) |
|
419 |
finally show ?thesis . |
|
420 |
qed |
|
421 |
||
422 |
lemma cclfp_lowerbound: assumes f: "mono f" and A: "f A \<le> A" shows "cclfp f \<le> A" |
|
423 |
unfolding cclfp_def |
|
424 |
proof (intro ccSUP_least) |
|
62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
62373
diff
changeset
|
425 |
fix i show "(f ^^ i) bot \<le> A" |
62373 | 426 |
proof (induction i) |
427 |
case (Suc i) from monoD[OF f this] A show ?case |
|
428 |
by auto |
|
429 |
qed simp |
|
430 |
qed simp |
|
431 |
||
432 |
lemma cclfp_transfer: |
|
433 |
assumes "sup_continuous \<alpha>" "mono f" |
|
62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
62373
diff
changeset
|
434 |
assumes "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)" |
62373 | 435 |
shows "\<alpha> (cclfp f) = cclfp g" |
436 |
proof - |
|
62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
62373
diff
changeset
|
437 |
have "\<alpha> (cclfp f) = (SUP i. \<alpha> ((f ^^ i) bot))" |
62373 | 438 |
unfolding cclfp_def by (intro sup_continuousD assms mono_funpow sup_continuous_mono) |
62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
62373
diff
changeset
|
439 |
moreover have "\<alpha> ((f ^^ i) bot) = (g ^^ i) bot" for i |
62373 | 440 |
by (induction i) (simp_all add: assms) |
441 |
ultimately show ?thesis |
|
442 |
by (simp add: cclfp_def) |
|
443 |
qed |
|
444 |
||
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
445 |
end |