author  wenzelm 
Wed, 17 Jun 2015 11:03:05 +0200  
changeset 60500  903bb1495239 
parent 60427  b4b672f09270 
child 60614  e39e6881985c 
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 
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 
46508  8 
imports 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 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

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 

60500  37 
subsection \<open>Continuity for complete lattices\<close> 
21312  38 

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

40 
sup_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

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

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

44 
by (auto simp: sup_continuous_def) 
21312  45 

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

46 
lemma sup_continuous_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

47 
fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice" 
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 
assumes [simp]: "sup_continuous F" shows "mono F" 
21312  49 
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

50 
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

51 
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

52 
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

53 
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

54 
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

55 
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

56 
by (simp add: SUP_nat_binary le_iff_sup) 
21312  57 
qed 
58 

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

59 
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

60 
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

61 
proof (rule antisym) 
60500  62 
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

63 
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

64 
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

65 
fix i show "(F ^^ i) bot \<le> lfp F" 
21312  66 
proof (induct i) 
67 
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

68 
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

69 
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

70 
also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric]) 
21312  71 
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

72 
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

73 
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

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

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

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

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

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

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

82 
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

83 
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

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

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

88 
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

89 
by (fast intro: SUP_least SUP_upper) 
21312  90 
finally show "F ?U \<le> ?U" . 
91 
qed 

92 
qed 

93 

60427  94 
lemma lfp_transfer: 
95 
assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and g: "sup_continuous g" 

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

97 
shows "\<alpha> (lfp f) = lfp g" 

98 
proof  

99 
have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))" 

100 
unfolding sup_continuous_lfp[OF f] by (intro f \<alpha> sup_continuousD mono_funpow sup_continuous_mono) 

101 
moreover have "\<alpha> ((f^^i) bot) = (g^^i) bot" for i 

102 
by (induction i; simp) 

103 
ultimately show ?thesis 

104 
unfolding sup_continuous_lfp[OF g] by simp 

105 
qed 

106 

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

108 
inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

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

110 

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

111 
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

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

113 

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

114 
lemma inf_continuous_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

115 
fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice" 
60172
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 [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

117 
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

118 
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

119 
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

120 
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

121 
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

122 
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

123 
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

124 
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

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

126 

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

127 
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

128 
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

129 
proof (rule antisym) 
60500  130 
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

131 
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

132 
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

133 
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

134 
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

135 
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

136 
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

137 
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

138 
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

139 
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

140 
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

141 
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

142 
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

143 
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

144 
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

145 
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

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

147 
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

148 
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

149 
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

150 
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

151 
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

152 
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

153 
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

154 
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

155 
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

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

158 
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

159 
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

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

161 

60427  162 
lemma gfp_transfer: 
163 
assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g" 

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

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

166 
proof  

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

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

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

170 
by (induction i; simp) 

171 
ultimately show ?thesis 

172 
unfolding inf_continuous_gfp[OF g] by simp 

173 
qed 

174 

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

175 
end 