author  hoelzl 
Mon, 04 May 2015 17:35:31 +0200  
changeset 60172  423273355b55 
parent 58881  b9556a055632 
child 60427  b4b672f09270 
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 

58881  5 
section {* Continuity and iterations (of set transformers) *} 
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 

22367  37 
subsection {* Continuity for complete lattices *} 
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) 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

62 
note mono = sup_continuous_mono[OF `sup_continuous F`] 
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset

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)" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

87 
using `sup_continuous F` by (simp add: sup_continuous_def) 
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 

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

95 
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

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

97 

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

98 
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

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

100 

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

101 
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

102 
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

103 
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

104 
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

105 
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

106 
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

107 
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

108 
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

109 
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

110 
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

111 
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

112 
qed 
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_gfp: 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
58881
diff
changeset

115 
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

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

117 
note mono = inf_continuous_mono[OF `inf_continuous F`] 
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset

118 
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

119 
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

120 
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

121 
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

122 
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

123 
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

124 
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

125 
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

126 
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

127 
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

128 
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

129 
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

130 
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

131 
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

132 
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

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

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

136 
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

137 
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

138 
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

139 
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

140 
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

141 
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

142 
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

143 
also have "\<dots> \<le> F ?U" 
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 
by (simp add: inf_continuousD `inf_continuous F` *) 
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54257
diff
changeset

145 
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

146 
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

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

148 

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

149 
end 