author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63979  95c3ae4baba8 
child 69313  b021008c5397 
permissions  rwrr 
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 chaincomplete 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: 
62373  15 
"(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::countable_complete_lattice)" 
16 
apply (auto intro!: antisym ccSUP_least) 

17 
apply (rule ccSUP_upper2[where i=0]) 

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 
apply simp_all 
62373  19 
apply (rule ccSUP_upper2[where i=1]) 
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

20 
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

21 
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

22 

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 
lemma INF_nat_binary: 
62373  24 
"(INF n::nat. if n = 0 then A else B) = (inf A B::'a::countable_complete_lattice)" 
25 
apply (auto intro!: antisym ccINF_greatest) 

26 
apply (rule ccINF_lower2[where i=0]) 

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

27 
apply simp_all 
62373  28 
apply (rule ccINF_lower2[where i=1]) 
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

29 
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

30 
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

31 

60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

32 
text \<open> 
61585  33 
The name \<open>continuous\<close> is already taken in \<open>Complex_Main\<close>, so we use 
34 
\<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

35 
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

36 
\<close> 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

37 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

38 
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

39 

60500  40 
subsection \<open>Continuity for complete lattices\<close> 
21312  41 

22367  42 
definition 
62373  43 
sup_continuous :: "('a::countable_complete_lattice \<Rightarrow> 'b::countable_complete_lattice) \<Rightarrow> bool" 
44 
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

45 
"sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))" 
22367  46 

60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

47 
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

48 
by (auto simp: sup_continuous_def) 
21312  49 

60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

50 
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

51 
assumes [simp]: "sup_continuous F" shows "mono F" 
21312  52 
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

53 
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

54 
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

55 
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

56 
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

57 
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

58 
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

59 
by (simp add: SUP_nat_binary le_iff_sup) 
21312  60 
qed 
61 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

62 
lemma [order_continuous_intros]: 
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

63 
shows sup_continuous_const: "sup_continuous (\<lambda>x. c)" 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

64 
and sup_continuous_id: "sup_continuous (\<lambda>x. x)" 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

65 
and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)" 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

66 
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

67 
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

68 
by (auto simp: sup_continuous_def) 
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

69 

e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

70 
lemma sup_continuous_compose: 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

71 
assumes f: "sup_continuous f" and g: "sup_continuous g" 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

72 
shows "sup_continuous (\<lambda>x. f (g x))" 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

73 
unfolding sup_continuous_def 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

74 
proof safe 
63540  75 
fix M :: "nat \<Rightarrow> 'c" 
76 
assume M: "mono M" 

77 
then have "mono (\<lambda>i. g (M i))" 

60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

78 
using sup_continuous_mono[OF g] by (auto simp: mono_def) 
63540  79 
with M show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))" 
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

80 
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

81 
qed 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

82 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

83 
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

84 
"sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))" 
62373  85 
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

86 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

87 
lemma sup_continuous_inf[order_continuous_intros]: 
62373  88 
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

89 
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

90 
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

91 
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

92 
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

93 
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

94 
have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP j i. inf (P (M i)) (Q (M j)))" 
62373  95 
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

96 
also have "\<dots> \<le> (SUP i. inf (P (M i)) (Q (M i)))" 
62373  97 
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

98 
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  99 
by (intro ccSUP_upper2[of _ "sup i j"] inf_mono) (auto simp: mono_def) 
100 
qed auto 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

101 
finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP i. inf (P (M i)) (Q (M i)))" . 
62373  102 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

103 
show "(SUP i. inf (P (M i)) (Q (M i))) \<le> inf (P (SUP i. M i)) (Q (SUP i. M i))" 
62373  104 
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

105 
qed 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

106 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

107 
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

108 
"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

109 
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

110 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

111 
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

112 
"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

113 
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

114 

60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

115 
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

116 
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

117 
proof (rule antisym) 
60500  118 
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

119 
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

120 
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

121 
fix i show "(F ^^ i) bot \<le> lfp F" 
21312  122 
proof (induct i) 
123 
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

124 
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

125 
also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc]) 
63979  126 
also have "\<dots> = lfp F" by (simp add: lfp_fixpoint[OF mono]) 
21312  127 
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

128 
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

129 
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

130 
show "lfp F \<le> ?U" 
21312  131 
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

132 
have "mono (\<lambda>i::nat. (F ^^ i) bot)" 
21312  133 
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

134 
{ fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

135 
proof (induct i) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

136 
case 0 show ?case by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

137 
next 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

138 
case Suc thus ?case using monoD[OF mono Suc] by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

139 
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

140 
thus ?thesis by (auto simp add: mono_iff_le_Suc) 
21312  141 
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

142 
hence "F ?U = (SUP i. (F ^^ Suc i) bot)" 
60500  143 
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

144 
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

145 
by (fast intro: SUP_least SUP_upper) 
21312  146 
finally show "F ?U \<le> ?U" . 
147 
qed 

148 
qed 

149 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

150 
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

151 
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

152 
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

153 
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

154 
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

155 
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

156 
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

157 
proof (rule antisym) 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

158 
note mono_g = sup_continuous_mono[OF g] 
60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset

159 
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

160 
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

161 
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

162 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

163 
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

164 
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

165 
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

166 
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

167 
proof 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

168 
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

169 
proof (induct i) 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

170 
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

171 
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

172 
qed 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

173 
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

174 
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

175 

60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset

176 
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

177 
apply (induction n) 
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset

178 
apply simp 
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset

179 
apply (subst lfp_unfold[OF mono_f]) 
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset

180 
apply (auto intro!: monoD[OF mono_f]) 
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset

181 
done 
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset

182 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

183 
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

184 
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

185 
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

186 
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

187 
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

188 
proof (induction i) 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

189 
case (Suc n) then show ?case 
60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset

190 
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

191 
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

192 
qed 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

193 
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

194 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

195 
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

196 
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

197 
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

198 
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

199 
(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

200 
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

201 
qed 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

202 

60714
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset

203 
lemma lfp_transfer: 
ff8aa76d6d1c
stronger induction assumption in lfp_transfer and emeasure_lfp
hoelzl
parents:
60636
diff
changeset

204 
"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

205 
(\<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

206 
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

207 

19736  208 
definition 
62373  209 
inf_continuous :: "('a::countable_complete_lattice \<Rightarrow> 'b::countable_complete_lattice) \<Rightarrow> bool" 
210 
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

211 
"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

212 

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 
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

214 
by (auto simp: inf_continuous_def) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

215 

60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

216 
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

217 
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

218 
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

219 
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

220 
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

221 
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

222 
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

223 
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

224 
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

225 
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

226 
qed 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

227 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

228 
lemma [order_continuous_intros]: 
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

229 
shows inf_continuous_const: "inf_continuous (\<lambda>x. c)" 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

230 
and inf_continuous_id: "inf_continuous (\<lambda>x. x)" 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

231 
and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)" 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

232 
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

233 
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

234 
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

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_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

237 
"inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))" 
62373  238 
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

239 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

240 
lemma inf_continuous_sup[order_continuous_intros]: 
62373  241 
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

242 
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

243 
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

244 
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

245 
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

246 
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

247 
show "sup (P (INF i. M i)) (Q (INF i. M i)) \<le> (INF i. sup (P (M i)) (Q (M i)))" 
62373  248 
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

249 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

250 
have "(INF i. sup (P (M i)) (Q (M i))) \<le> (INF j i. sup (P (M i)) (Q (M j)))" 
62373  251 
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

252 
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  253 
by (intro ccINF_lower2[of _ "sup i j"] sup_mono) (auto simp: mono_def antimono_def) 
254 
qed auto 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

255 
also have "\<dots> \<le> sup (P (INF i. M i)) (Q (INF i. M i))" 
62373  256 
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

257 
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

258 
qed 
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_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

261 
"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

262 
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

263 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

264 
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

265 
"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

266 
using inf_continuous_sup[of P Q] by simp 
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

267 

e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

268 
lemma inf_continuous_compose: 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

269 
assumes f: "inf_continuous f" and g: "inf_continuous g" 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

270 
shows "inf_continuous (\<lambda>x. f (g x))" 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

271 
unfolding inf_continuous_def 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

272 
proof safe 
63540  273 
fix M :: "nat \<Rightarrow> 'c" 
274 
assume M: "antimono M" 

275 
then have "antimono (\<lambda>i. g (M i))" 

60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

276 
using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def) 
63540  277 
with M show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))" 
60614
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

278 
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

279 
qed 
e39e6881985c
generalized inf and sup_continuous; added intro rules
hoelzl
parents:
60500
diff
changeset

280 

60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

281 
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

282 
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

283 
proof (rule antisym) 
60500  284 
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

285 
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

286 
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

287 
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

288 
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

289 
case (Suc i) 
63979  290 
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

291 
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

292 
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

293 
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

294 
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

295 
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

296 
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

297 
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

298 
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

299 
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

300 
{ 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

301 
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

302 
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

303 
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

304 
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

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 
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

307 
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

308 
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

309 
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

310 
also have "\<dots> \<le> F ?U" 
60500  311 
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

312 
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

313 
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

314 
qed 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

315 

60427  316 
lemma gfp_transfer: 
317 
assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g" 

318 
assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)" 

319 
shows "\<alpha> (gfp f) = gfp g" 

320 
proof  

321 
have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))" 

322 
unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono) 

323 
moreover have "\<alpha> ((f^^i) top) = (g^^i) top" for i 

324 
by (induction i; simp) 

325 
ultimately show ?thesis 

326 
unfolding inf_continuous_gfp[OF g] by simp 

327 
qed 

328 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

329 
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

330 
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

331 
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

332 
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

333 
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

334 
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

335 
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

336 
proof (rule antisym) 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

337 
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

338 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

339 
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

340 
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

341 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

342 
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

343 
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

344 
proof 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

345 
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

346 
proof (induct i) 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

347 
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

348 
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

349 
qed 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

350 
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

351 
proof 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

352 
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

353 
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

354 
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

355 
qed 
62373  356 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

357 
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

358 
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

359 
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

360 
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

361 
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

362 
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

363 
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

364 
qed 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

365 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

366 
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

367 
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

368 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

369 
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

370 
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

371 
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

372 
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

373 
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

374 
proof (induction i) 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

375 
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

376 
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

377 
next 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

378 
case 0 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

379 
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

380 
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

381 
then show ?case 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

382 
by simp 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

383 
qed 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

384 
qed 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

385 
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

386 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

387 
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

388 
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

389 
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

390 
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

391 
(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

392 
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

393 
qed 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60614
diff
changeset

394 

62373  395 
subsubsection \<open>Least fixed points in countable complete lattices\<close> 
396 

397 
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

398 
where "cclfp f = (SUP i. (f ^^ i) bot)" 
62373  399 

400 
lemma cclfp_unfold: 

401 
assumes "sup_continuous F" shows "cclfp F = F (cclfp F)" 

402 
proof  

62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
62373
diff
changeset

403 
have "cclfp F = (SUP i. F ((F ^^ i) bot))" 
62373  404 
unfolding cclfp_def by (subst UNIV_nat_eq) auto 
405 
also have "\<dots> = F (cclfp F)" 

406 
unfolding cclfp_def 

407 
by (intro sup_continuousD[symmetric] assms mono_funpow sup_continuous_mono) 

408 
finally show ?thesis . 

409 
qed 

410 

411 
lemma cclfp_lowerbound: assumes f: "mono f" and A: "f A \<le> A" shows "cclfp f \<le> A" 

412 
unfolding cclfp_def 

413 
proof (intro ccSUP_least) 

62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
62373
diff
changeset

414 
fix i show "(f ^^ i) bot \<le> A" 
62373  415 
proof (induction i) 
416 
case (Suc i) from monoD[OF f this] A show ?case 

417 
by auto 

418 
qed simp 

419 
qed simp 

420 

421 
lemma cclfp_transfer: 

422 
assumes "sup_continuous \<alpha>" "mono f" 

62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
62373
diff
changeset

423 
assumes "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)" 
62373  424 
shows "\<alpha> (cclfp f) = cclfp g" 
425 
proof  

62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
62373
diff
changeset

426 
have "\<alpha> (cclfp f) = (SUP i. \<alpha> ((f ^^ i) bot))" 
62373  427 
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

428 
moreover have "\<alpha> ((f ^^ i) bot) = (g ^^ i) bot" for i 
62373  429 
by (induction i) (simp_all add: assms) 
430 
ultimately show ?thesis 

431 
by (simp add: cclfp_def) 

432 
qed 

433 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

434 
end 