author | hoelzl |
Mon, 13 Jul 2015 14:39:50 +0200 | |
changeset 60714 | ff8aa76d6d1c |
parent 60636 | ee18efe9b246 |
child 61585 | a9599d3d7610 |
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 |
11355 | 2 |
Author: David von Oheimb, TU Muenchen |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
3 |
*) |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
4 |
|
60500 | 5 |
section \<open>Continuity and iterations (of set transformers)\<close> |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
6 |
|
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
|
7 |
theory Order_Continuity |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
8 |
imports Complex_Main |
15131 | 9 |
begin |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
10 |
|
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
|
11 |
(* 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
|
12 |
|
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 |
lemma SUP_nat_binary: |
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 |
"(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::complete_lattice)" |
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
|
15 |
apply (auto intro!: antisym 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
|
16 |
apply (rule SUP_upper2[where i=0]) |
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
|
17 |
apply simp_all |
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 |
apply (rule SUP_upper2[where i=1]) |
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 |
apply simp_all |
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 |
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
|
21 |
|
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
|
22 |
lemma INF_nat_binary: |
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
|
23 |
"(INF n::nat. if n = 0 then A else B) = (inf A B::'a::complete_lattice)" |
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 |
apply (auto intro!: antisym 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
|
25 |
apply (rule INF_lower2[where i=0]) |
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
|
26 |
apply simp_all |
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
|
27 |
apply (rule INF_lower2[where i=1]) |
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
|
28 |
apply simp_all |
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
|
29 |
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
|
30 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
31 |
text \<open> |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
32 |
The name @{text continuous} is already taken in @{text "Complex_Main"}, so we use |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
33 |
@{text "sup_continuous"} and @{text "inf_continuous"}. These names appear sometimes in literature |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
34 |
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
|
35 |
\<close> |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
36 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
37 |
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
|
38 |
|
60500 | 39 |
subsection \<open>Continuity for complete lattices\<close> |
21312 | 40 |
|
22367 | 41 |
definition |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
42 |
sup_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" 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
|
43 |
"sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))" |
22367 | 44 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
45 |
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
|
46 |
by (auto simp: sup_continuous_def) |
21312 | 47 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
48 |
lemma sup_continuous_mono: |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
49 |
assumes [simp]: "sup_continuous F" shows "mono F" |
21312 | 50 |
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
|
51 |
fix A B :: "'a" assume [simp]: "A \<le> B" |
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
|
52 |
have "F B = F (SUP n::nat. if n = 0 then A else B)" |
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
|
53 |
by (simp add: sup_absorb2 SUP_nat_binary) |
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
|
54 |
also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)" |
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
55 |
by (auto simp: sup_continuousD mono_def intro!: 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
|
56 |
finally show "F A \<le> F B" |
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
|
57 |
by (simp add: SUP_nat_binary le_iff_sup) |
21312 | 58 |
qed |
59 |
||
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
60 |
lemma [order_continuous_intros]: |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
61 |
shows sup_continuous_const: "sup_continuous (\<lambda>x. c)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
62 |
and sup_continuous_id: "sup_continuous (\<lambda>x. x)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
63 |
and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
64 |
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
|
65 |
and sup_continuous_If: "sup_continuous F \<Longrightarrow> sup_continuous G \<Longrightarrow> sup_continuous (\<lambda>f. if C then F f else G f)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
66 |
by (auto simp: sup_continuous_def) |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
67 |
|
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
68 |
lemma sup_continuous_compose: |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
69 |
assumes f: "sup_continuous f" and g: "sup_continuous g" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
70 |
shows "sup_continuous (\<lambda>x. f (g x))" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
71 |
unfolding sup_continuous_def |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
72 |
proof safe |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
73 |
fix M :: "nat \<Rightarrow> 'c" assume "mono M" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
74 |
moreover then have "mono (\<lambda>i. g (M i))" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
75 |
using sup_continuous_mono[OF g] by (auto simp: mono_def) |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
76 |
ultimately show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
77 |
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
|
78 |
qed |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
79 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
80 |
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
|
81 |
"sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
82 |
by (simp add: sup_continuous_def SUP_sup_distrib) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
83 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
84 |
lemma sup_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
|
85 |
fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
86 |
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
|
87 |
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
|
88 |
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
|
89 |
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
|
90 |
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
|
91 |
have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP j i. inf (P (M i)) (Q (M j)))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
92 |
unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_SUP SUP_inf .. |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
93 |
also have "\<dots> \<le> (SUP i. inf (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
|
94 |
proof (intro SUP_least) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
95 |
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)))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
96 |
by (intro SUP_upper2[of "sup i j"] inf_mono) (auto simp: mono_def) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
97 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
98 |
finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP i. inf (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
|
99 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
100 |
show "(SUP i. inf (P (M i)) (Q (M i))) \<le> inf (P (SUP i. M i)) (Q (SUP i. M i))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
101 |
unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro SUP_least inf_mono SUP_upper) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
102 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
103 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
104 |
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
|
105 |
"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
|
106 |
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
|
107 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
108 |
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
|
109 |
"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
|
110 |
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
|
111 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
112 |
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
|
113 |
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
|
114 |
proof (rule antisym) |
60500 | 115 |
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
|
116 |
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
|
117 |
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
|
118 |
fix i show "(F ^^ i) bot \<le> lfp F" |
21312 | 119 |
proof (induct i) |
120 |
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
|
121 |
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
|
122 |
also have "\<dots> \<le> F (lfp F)" 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
|
123 |
also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric]) |
21312 | 124 |
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
|
125 |
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
|
126 |
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
|
127 |
show "lfp F \<le> ?U" |
21312 | 128 |
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
|
129 |
have "mono (\<lambda>i::nat. (F ^^ i) bot)" |
21312 | 130 |
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
|
131 |
{ 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
|
132 |
proof (induct i) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
133 |
case 0 show ?case by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
134 |
next |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
135 |
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
|
136 |
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
|
137 |
thus ?thesis by (auto simp add: mono_iff_le_Suc) |
21312 | 138 |
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
|
139 |
hence "F ?U = (SUP i. (F ^^ Suc i) bot)" |
60500 | 140 |
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
|
141 |
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
|
142 |
by (fast intro: SUP_least SUP_upper) |
21312 | 143 |
finally show "F ?U \<le> ?U" . |
144 |
qed |
|
145 |
qed |
|
146 |
||
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
147 |
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
|
148 |
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
|
149 |
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
|
150 |
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
|
151 |
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
|
152 |
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
|
153 |
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
|
154 |
proof (rule antisym) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
155 |
note mono_g = sup_continuous_mono[OF g] |
60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
156 |
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
|
157 |
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
|
158 |
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
|
159 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
160 |
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
|
161 |
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
|
162 |
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
|
163 |
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
|
164 |
proof |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
165 |
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
|
166 |
proof (induct i) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
167 |
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
|
168 |
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
|
169 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
170 |
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
|
171 |
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
|
172 |
|
60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
173 |
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
|
174 |
apply (induction n) |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
175 |
apply simp |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
176 |
apply (subst lfp_unfold[OF mono_f]) |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
177 |
apply (auto intro!: monoD[OF mono_f]) |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
178 |
done |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
179 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
180 |
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
|
181 |
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
|
182 |
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
|
183 |
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
|
184 |
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
|
185 |
proof (induction i) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
186 |
case (Suc n) then show ?case |
60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
187 |
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
|
188 |
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
|
189 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
190 |
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
|
191 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
192 |
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
|
193 |
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
|
194 |
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
|
195 |
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
|
196 |
(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
|
197 |
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
|
198 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
199 |
|
60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
200 |
lemma lfp_transfer: |
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset
|
201 |
"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
|
202 |
(\<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
|
203 |
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
|
204 |
|
19736 | 205 |
definition |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
206 |
inf_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" 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
|
207 |
"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
|
208 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
209 |
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
|
210 |
by (auto simp: inf_continuous_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
211 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
212 |
lemma inf_continuous_mono: |
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
213 |
assumes [simp]: "inf_continuous F" shows "mono 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
|
214 |
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
|
215 |
fix A B :: "'a" assume [simp]: "A \<le> B" |
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
|
216 |
have "F A = F (INF n::nat. if n = 0 then B else A)" |
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
|
217 |
by (simp add: inf_absorb2 INF_nat_binary) |
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
|
218 |
also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)" |
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
219 |
by (auto simp: inf_continuousD antimono_def intro!: 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
|
220 |
finally show "F A \<le> F B" |
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
|
221 |
by (simp add: INF_nat_binary le_iff_inf inf_commute) |
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
|
222 |
qed |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
223 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
224 |
lemma [order_continuous_intros]: |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
225 |
shows inf_continuous_const: "inf_continuous (\<lambda>x. c)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
226 |
and inf_continuous_id: "inf_continuous (\<lambda>x. x)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
227 |
and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
228 |
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
|
229 |
and inf_continuous_If: "inf_continuous F \<Longrightarrow> inf_continuous G \<Longrightarrow> inf_continuous (\<lambda>f. if C then F f else G f)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
230 |
by (auto simp: inf_continuous_def) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
231 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
232 |
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
|
233 |
"inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
234 |
by (simp add: inf_continuous_def INF_inf_distrib) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
235 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
236 |
lemma inf_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
|
237 |
fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
238 |
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
|
239 |
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
|
240 |
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
|
241 |
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
|
242 |
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
|
243 |
show "sup (P (INF i. M i)) (Q (INF i. M i)) \<le> (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
|
244 |
unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro INF_greatest sup_mono INF_lower) |
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 |
have "(INF i. sup (P (M i)) (Q (M i))) \<le> (INF j i. sup (P (M i)) (Q (M j)))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
247 |
proof (intro INF_greatest) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
248 |
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)))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
249 |
by (intro INF_lower2[of "sup i j"] sup_mono) (auto simp: mono_def antimono_def) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
250 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
251 |
also have "\<dots> \<le> sup (P (INF i. M i)) (Q (INF i. M i))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
252 |
unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] INF_sup sup_INF .. |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
253 |
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
|
254 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
255 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
256 |
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
|
257 |
"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
|
258 |
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
|
259 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
260 |
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
|
261 |
"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
|
262 |
using inf_continuous_sup[of P Q] by simp |
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
263 |
|
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
264 |
lemma inf_continuous_compose: |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
265 |
assumes f: "inf_continuous f" and g: "inf_continuous g" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
266 |
shows "inf_continuous (\<lambda>x. f (g x))" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
267 |
unfolding inf_continuous_def |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
268 |
proof safe |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
269 |
fix M :: "nat \<Rightarrow> 'c" assume "antimono M" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
270 |
moreover then have "antimono (\<lambda>i. g (M i))" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
271 |
using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def) |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
272 |
ultimately show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))" |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
273 |
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
|
274 |
qed |
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset
|
275 |
|
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset
|
276 |
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
|
277 |
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
|
278 |
proof (rule antisym) |
60500 | 279 |
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
|
280 |
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
|
281 |
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
|
282 |
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
|
283 |
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
|
284 |
case (Suc 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
|
285 |
have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric]) |
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
|
286 |
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
|
287 |
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
|
288 |
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
|
289 |
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
|
290 |
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
|
291 |
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
|
292 |
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
|
293 |
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
|
294 |
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
|
295 |
{ 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
|
296 |
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
|
297 |
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
|
298 |
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
|
299 |
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
|
300 |
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
|
301 |
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
|
302 |
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
|
303 |
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
|
304 |
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
|
305 |
also have "\<dots> \<le> F ?U" |
60500 | 306 |
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
|
307 |
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
|
308 |
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
|
309 |
qed |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
310 |
|
60427 | 311 |
lemma gfp_transfer: |
312 |
assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g" |
|
313 |
assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)" |
|
314 |
shows "\<alpha> (gfp f) = gfp g" |
|
315 |
proof - |
|
316 |
have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))" |
|
317 |
unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono) |
|
318 |
moreover have "\<alpha> ((f^^i) top) = (g^^i) top" for i |
|
319 |
by (induction i; simp) |
|
320 |
ultimately show ?thesis |
|
321 |
unfolding inf_continuous_gfp[OF g] by simp |
|
322 |
qed |
|
323 |
||
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
324 |
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
|
325 |
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
|
326 |
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
|
327 |
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
|
328 |
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
|
329 |
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
|
330 |
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
|
331 |
proof (rule antisym) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
332 |
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
|
333 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
334 |
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
|
335 |
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
|
336 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
337 |
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
|
338 |
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
|
339 |
proof |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
340 |
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
|
341 |
proof (induct i) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
342 |
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
|
343 |
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
|
344 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
345 |
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
|
346 |
proof |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
347 |
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
|
348 |
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
|
349 |
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
|
350 |
qed |
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 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
|
353 |
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
|
354 |
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
|
355 |
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
|
356 |
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
|
357 |
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
|
358 |
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
|
359 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
360 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
361 |
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
|
362 |
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
|
363 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
364 |
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
|
365 |
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
|
366 |
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
|
367 |
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
|
368 |
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
|
369 |
proof (induction i) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
370 |
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
|
371 |
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
|
372 |
next |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
373 |
case 0 |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
374 |
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
|
375 |
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
|
376 |
then show ?case |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
377 |
by simp |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
378 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
379 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
380 |
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
|
381 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
382 |
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
|
383 |
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
|
384 |
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
|
385 |
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
|
386 |
(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
|
387 |
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
|
388 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset
|
389 |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
390 |
end |