src/HOL/Library/Order_Continuity.thy
author hoelzl
Mon Mar 10 20:04:40 2014 +0100 (2014-03-10)
changeset 56020 f92479477c52
parent 54257 src/HOL/Library/Continuity.thy@5c7a3b6b05a9
child 58881 b9556a055632
permissions -rw-r--r--
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
     1 (*  Title:      HOL/Library/Order_Continuity.thy
     2     Author:     David von Oheimb, TU Muenchen
     3 *)
     4 
     5 header {* Continuity and iterations (of set transformers) *}
     6 
     7 theory Order_Continuity
     8 imports Main
     9 begin
    10 
    11 (* TODO: Generalize theory to chain-complete partial orders *)
    12 
    13 lemma SUP_nat_binary:
    14   "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::complete_lattice)"
    15   apply (auto intro!: antisym SUP_least)
    16   apply (rule SUP_upper2[where i=0])
    17   apply simp_all
    18   apply (rule SUP_upper2[where i=1])
    19   apply simp_all
    20   done
    21 
    22 lemma INF_nat_binary:
    23   "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::complete_lattice)"
    24   apply (auto intro!: antisym INF_greatest)
    25   apply (rule INF_lower2[where i=0])
    26   apply simp_all
    27   apply (rule INF_lower2[where i=1])
    28   apply simp_all
    29   done
    30 
    31 subsection {* Continuity for complete lattices *}
    32 
    33 definition
    34   continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    35   "continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    36 
    37 lemma continuousD: "continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
    38   by (auto simp: continuous_def)
    39 
    40 lemma continuous_mono:
    41   fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    42   assumes [simp]: "continuous F" shows "mono F"
    43 proof
    44   fix A B :: "'a" assume [simp]: "A \<le> B"
    45   have "F B = F (SUP n::nat. if n = 0 then A else B)"
    46     by (simp add: sup_absorb2 SUP_nat_binary)
    47   also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
    48     by (auto simp: continuousD mono_def intro!: SUP_cong)
    49   finally show "F A \<le> F B"
    50     by (simp add: SUP_nat_binary le_iff_sup)
    51 qed
    52 
    53 lemma continuous_lfp:
    54   assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
    55 proof (rule antisym)
    56   note mono = continuous_mono[OF `continuous F`]
    57   show "?U \<le> lfp F"
    58   proof (rule SUP_least)
    59     fix i show "(F ^^ i) bot \<le> lfp F"
    60     proof (induct i)
    61       case (Suc i)
    62       have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
    63       also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
    64       also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
    65       finally show ?case .
    66     qed simp
    67   qed
    68   show "lfp F \<le> ?U"
    69   proof (rule lfp_lowerbound)
    70     have "mono (\<lambda>i::nat. (F ^^ i) bot)"
    71     proof -
    72       { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
    73         proof (induct i)
    74           case 0 show ?case by simp
    75         next
    76           case Suc thus ?case using monoD[OF mono Suc] by auto
    77         qed }
    78       thus ?thesis by (auto simp add: mono_iff_le_Suc)
    79     qed
    80     hence "F ?U = (SUP i. (F ^^ Suc i) bot)" using `continuous F` by (simp add: continuous_def)
    81     also have "\<dots> \<le> ?U" by (fast intro: SUP_least SUP_upper)
    82     finally show "F ?U \<le> ?U" .
    83   qed
    84 qed
    85 
    86 definition
    87   down_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    88   "down_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
    89 
    90 lemma down_continuousD: "down_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
    91   by (auto simp: down_continuous_def)
    92 
    93 lemma down_continuous_mono:
    94   fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    95   assumes [simp]: "down_continuous F" shows "mono F"
    96 proof
    97   fix A B :: "'a" assume [simp]: "A \<le> B"
    98   have "F A = F (INF n::nat. if n = 0 then B else A)"
    99     by (simp add: inf_absorb2 INF_nat_binary)
   100   also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
   101     by (auto simp: down_continuousD antimono_def intro!: INF_cong)
   102   finally show "F A \<le> F B"
   103     by (simp add: INF_nat_binary le_iff_inf inf_commute)
   104 qed
   105 
   106 lemma down_continuous_gfp:
   107   assumes "down_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
   108 proof (rule antisym)
   109   note mono = down_continuous_mono[OF `down_continuous F`]
   110   show "gfp F \<le> ?U"
   111   proof (rule INF_greatest)
   112     fix i show "gfp F \<le> (F ^^ i) top"
   113     proof (induct i)
   114       case (Suc i)
   115       have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
   116       also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
   117       also have "\<dots> = (F ^^ Suc i) top" by simp
   118       finally show ?case .
   119     qed simp
   120   qed
   121   show "?U \<le> gfp F"
   122   proof (rule gfp_upperbound)
   123     have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
   124     proof -
   125       { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
   126         proof (induct i)
   127           case 0 show ?case by simp
   128         next
   129           case Suc thus ?case using monoD[OF mono Suc] by auto
   130         qed }
   131       thus ?thesis by (auto simp add: antimono_iff_le_Suc)
   132     qed
   133     have "?U \<le> (INF i. (F ^^ Suc i) top)"
   134       by (fast intro: INF_greatest INF_lower)
   135     also have "\<dots> \<le> F ?U"
   136       by (simp add: down_continuousD `down_continuous F` *)
   137     finally show "?U \<le> F ?U" .
   138   qed
   139 qed
   140 
   141 end