src/HOL/Library/Order_Continuity.thy
author hoelzl
Mon, 04 May 2015 17:35:31 +0200
changeset 60172 423273355b55
parent 58881 b9556a055632
child 60427 b4b672f09270
permissions -rw-r--r--
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
wenzelm
parents: 11351
diff changeset
     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
b9556a055632 modernized header;
wenzelm
parents: 56020
diff changeset
     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
ec9630fe9ca7 tuned imports;
wenzelm
parents: 44928
diff changeset
     8
imports Main
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14981
diff changeset
     9
begin
11351
c5c403d30c77 added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff changeset
    10
56020
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    11
(* TODO: Generalize theory to chain-complete partial orders *)
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    12
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    13
lemma SUP_nat_binary:
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    14
  "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::complete_lattice)"
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    15
  apply (auto intro!: antisym SUP_least)
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    16
  apply (rule SUP_upper2[where i=0])
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    17
  apply simp_all
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    18
  apply (rule SUP_upper2[where i=1])
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    19
  apply simp_all
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    20
  done
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    21
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    22
lemma INF_nat_binary:
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    23
  "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::complete_lattice)"
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    24
  apply (auto intro!: antisym INF_greatest)
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    25
  apply (rule INF_lower2[where i=0])
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    26
  apply simp_all
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    27
  apply (rule INF_lower2[where i=1])
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    28
  apply simp_all
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    29
  done
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 54257
diff changeset
    30
60172
423273355b55 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents: 58881
diff changeset
    31
text \<open>
423273355b55 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents: 58881
diff changeset
    32
  The name @{text continuous} is already taken in @{text "Complex_Main"}, so we use
423273355b55 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents: 58881
diff changeset
    33
  @{text "sup_continuous"} and @{text "inf_continuous"}. These names appear sometimes in literature
423273355b55 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents: 58881
diff changeset
    34
  and have the advantage that these names are duals.
423273355b55 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents: 58881
diff changeset
    35
\<close>
423273355b55 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents: 58881
diff changeset
    36
22367
6860f09242bf tuned document;
wenzelm
parents: 21404
diff changeset
    37
subsection {* Continuity for complete lattices *}
21312
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    38
22367
6860f09242bf tuned document;
wenzelm
parents: 21404
diff changeset
    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
6860f09242bf tuned document;
wenzelm
parents: 21404
diff changeset
    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
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    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
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    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
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    57
qed
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    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
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    66
    proof (induct i)
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    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
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    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
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    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
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    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 tab-width;
wenzelm
parents: 32456
diff changeset
    79
        proof (induct i)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
    80
          case 0 show ?case by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
    81
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
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 tab-width;
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
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    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
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    90
    finally show "F ?U \<le> ?U" .
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    91
  qed
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    92
qed
1d39091a3208 started reorgnization of lattice theories
nipkow
parents: 19736
diff changeset
    93
19736
wenzelm
parents: 15140
diff changeset
    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