src/HOL/LOrder.thy
author kleing
Tue Jun 29 11:18:34 2004 +0200 (2004-06-29)
changeset 15010 72fbe711e414
parent 14738 83f1a514dcb4
child 15131 c69542757a4d
permissions -rw-r--r--
license change to BSD
     1 (*  Title:   HOL/LOrder.thy
     2     ID:      $Id$
     3     Author:  Steven Obua, TU Muenchen
     4 *)
     5 
     6 header {* Lattice Orders *}
     7 
     8 theory LOrder = HOL:
     9 
    10 text {*
    11   The theory of lattices developed here is taken from the book:
    12   \begin{itemize}
    13   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979. 
    14   \end{itemize}
    15 *}
    16 
    17 constdefs
    18   is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
    19   "is_meet m == ! a b x. m a b \<le> a \<and> m a b \<le> b \<and> (x \<le> a \<and> x \<le> b \<longrightarrow> x \<le> m a b)"
    20   is_join :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
    21   "is_join j == ! a b x. a \<le> j a b \<and> b \<le> j a b \<and> (a \<le> x \<and> b \<le> x \<longrightarrow> j a b \<le> x)"  
    22 
    23 lemma is_meet_unique: 
    24   assumes "is_meet u" "is_meet v" shows "u = v"
    25 proof -
    26   {
    27     fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    28     assume a: "is_meet a"
    29     assume b: "is_meet b"
    30     {
    31       fix x y 
    32       let ?za = "a x y"
    33       let ?zb = "b x y"
    34       from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def)
    35       with b have "?za <= ?zb" by (auto simp add: is_meet_def)
    36     }
    37   }
    38   note f_le = this
    39   show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le) 
    40 qed
    41 
    42 lemma is_join_unique: 
    43   assumes "is_join u" "is_join v" shows "u = v"
    44 proof -
    45   {
    46     fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    47     assume a: "is_join a"
    48     assume b: "is_join b"
    49     {
    50       fix x y 
    51       let ?za = "a x y"
    52       let ?zb = "b x y"
    53       from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def)
    54       with b have "?zb <= ?za" by (auto simp add: is_join_def)
    55     }
    56   }
    57   note f_le = this
    58   show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le) 
    59 qed
    60 
    61 axclass join_semilorder < order
    62   join_exists: "? j. is_join j"
    63 
    64 axclass meet_semilorder < order
    65   meet_exists: "? m. is_meet m"
    66 
    67 axclass lorder < join_semilorder, meet_semilorder
    68 
    69 constdefs
    70   meet :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
    71   "meet == THE m. is_meet m"
    72   join :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
    73   "join ==  THE j. is_join j"
    74 
    75 lemma is_meet_meet: "is_meet (meet::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"
    76 proof -
    77   from meet_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_meet k" ..
    78   with is_meet_unique[of _ k] show ?thesis
    79     by (simp add: meet_def theI[of is_meet])    
    80 qed
    81 
    82 lemma meet_unique: "(is_meet m) = (m = meet)" 
    83 by (insert is_meet_meet, auto simp add: is_meet_unique)
    84 
    85 lemma is_join_join: "is_join (join::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"
    86 proof -
    87   from join_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_join k" ..
    88   with is_join_unique[of _ k] show ?thesis
    89     by (simp add: join_def theI[of is_join])    
    90 qed
    91 
    92 lemma join_unique: "(is_join j) = (j = join)"
    93 by (insert is_join_join, auto simp add: is_join_unique)
    94 
    95 lemma meet_left_le: "meet a b \<le> (a::'a::meet_semilorder)"
    96 by (insert is_meet_meet, auto simp add: is_meet_def)
    97 
    98 lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"
    99 by (insert is_meet_meet, auto simp add: is_meet_def)
   100 
   101 lemma meet_imp_le: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
   102 by (insert is_meet_meet, auto simp add: is_meet_def)
   103 
   104 lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"
   105 by (insert is_join_join, auto simp add: is_join_def)
   106 
   107 lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"
   108 by (insert is_join_join, auto simp add: is_join_def)
   109 
   110 lemma join_imp_le: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
   111 by (insert is_join_join, auto simp add: is_join_def)
   112 
   113 lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
   114 
   115 lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
   116 by (auto simp add: is_meet_def min_def)
   117 
   118 lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
   119 by (auto simp add: is_join_def max_def)
   120 
   121 instance linorder \<subseteq> meet_semilorder
   122 proof
   123   from is_meet_min show "? (m::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_meet m" by auto
   124 qed
   125 
   126 instance linorder \<subseteq> join_semilorder
   127 proof
   128   from is_join_max show "? (j::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_join j" by auto 
   129 qed
   130     
   131 instance linorder \<subseteq> lorder ..
   132 
   133 lemma meet_min: "meet = (min :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))" 
   134 by (simp add: is_meet_meet is_meet_min is_meet_unique)
   135 
   136 lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
   137 by (simp add: is_join_join is_join_max is_join_unique)
   138 
   139 lemma meet_idempotent[simp]: "meet x x = x"
   140 by (rule order_antisym, simp_all add: meet_left_le meet_imp_le)
   141 
   142 lemma join_idempotent[simp]: "join x x = x"
   143 by (rule order_antisym, simp_all add: join_left_le join_imp_le)
   144 
   145 lemma meet_comm: "meet x y = meet y x" 
   146 by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+)
   147 
   148 lemma join_comm: "join x y = join y x"
   149 by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+)
   150 
   151 lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r")
   152 proof - 
   153   have "?l <= meet x y & meet x y <= x & ?l <= z & meet x y <= y" by (simp add: meet_left_le meet_right_le)
   154   hence "?l <= x & ?l <= y & ?l <= z" by auto
   155   hence "?l <= ?r" by (simp add: meet_imp_le)
   156   hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le)
   157   have "?r <= meet y z & meet y z <= y & meet y z <= z & ?r <= x" by (simp add: meet_left_le meet_right_le)  
   158   hence "?r <= x & ?r <= y & ?r <= z" by (auto) 
   159   hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le)
   160   hence b:"?r <= ?l" by (simp add: meet_imp_le)
   161   from a b show "?l = ?r" by auto
   162 qed
   163 
   164 lemma join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r")
   165 proof -
   166   have "join x y <= ?l & x <= join x y & z <= ?l & y <= join x y" by (simp add: join_left_le join_right_le)
   167   hence "x <= ?l & y <= ?l & z <= ?l" by auto
   168   hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le)
   169   hence a:"?r <= ?l" by (simp add: join_imp_le)
   170   have "join y z <= ?r & y <= join y z & z <= join y z & x <= ?r" by (simp add: join_left_le join_right_le)
   171   hence "y <= ?r & z <= ?r & x <= ?r" by auto
   172   hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le)
   173   hence b:"?l <= ?r" by (simp add: join_imp_le)
   174   from a b show "?l = ?r" by auto
   175 qed
   176 
   177 lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"
   178 by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)
   179 
   180 lemma meet_left_idempotent: "meet y (meet y x) = meet y x"
   181 by (simp add: meet_assoc meet_comm meet_left_comm)
   182 
   183 lemma join_left_comm: "join a (join b c) = join b (join a c)"
   184 by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc)
   185 
   186 lemma join_left_idempotent: "join y (join y x) = join y x"
   187 by (simp add: join_assoc join_comm join_left_comm)
   188     
   189 lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent
   190 
   191 lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
   192 
   193 lemma le_def_meet: "(x <= y) = (meet x y = x)" 
   194 proof -
   195   have u: "x <= y \<longrightarrow> meet x y = x"
   196   proof 
   197     assume "x <= y"
   198     hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le)
   199     thus "meet x y = x" by auto
   200   qed
   201   have v:"meet x y = x \<longrightarrow> x <= y" 
   202   proof 
   203     have a:"meet x y <= y" by (simp add: meet_right_le)
   204     assume "meet x y = x"
   205     hence "x = meet x y" by auto
   206     with a show "x <= y" by (auto)
   207   qed
   208   from u v show ?thesis by blast
   209 qed
   210 
   211 lemma le_def_join: "(x <= y) = (join x y = y)" 
   212 proof -
   213   have u: "x <= y \<longrightarrow> join x y = y"
   214   proof 
   215     assume "x <= y"
   216     hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le)
   217     thus "join x y = y" by auto
   218   qed
   219   have v:"join x y = y \<longrightarrow> x <= y" 
   220   proof 
   221     have a:"x <= join x y" by (simp add: join_left_le)
   222     assume "join x y = y"
   223     hence "y = join x y" by auto
   224     with a show "x <= y" by (auto)
   225   qed
   226   from u v show ?thesis by blast
   227 qed
   228 
   229 lemma meet_join_absorp: "meet x (join x y) = x"
   230 proof -
   231   have a:"meet x (join x y) <= x" by (simp add: meet_left_le)
   232   have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le)
   233   from a b show ?thesis by auto
   234 qed
   235 
   236 lemma join_meet_absorp: "join x (meet x y) = x"
   237 proof - 
   238   have a:"x <= join x (meet x y)" by (simp add: join_left_le)
   239   have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le)
   240   from a b show ?thesis by auto
   241 qed
   242 
   243 lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"
   244 proof -
   245   assume a: "y <= z"
   246   have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le)
   247   with a have "meet x y <= x & meet x y <= z" by auto 
   248   thus "meet x y <= meet x z" by (simp add: meet_imp_le)
   249 qed
   250 
   251 lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
   252 proof -
   253   assume a: "y \<le> z"
   254   have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le)
   255   with a have "x <= join x z & y <= join x z" by auto
   256   thus "join x y <= join x z" by (simp add: join_imp_le)
   257 qed
   258 
   259 lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")
   260 proof -
   261   have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le)
   262   from meet_join_le have b: "meet y z <= ?r" 
   263     by (rule_tac meet_imp_le, (blast intro: order_trans)+)
   264   from a b show ?thesis by (simp add: join_imp_le)
   265 qed
   266   
   267 lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _") 
   268 proof -
   269   have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le)
   270   from meet_join_le have b: "?l <= join y z" 
   271     by (rule_tac join_imp_le, (blast intro: order_trans)+)
   272   from a b show ?thesis by (simp add: meet_imp_le)
   273 qed
   274 
   275 lemma meet_join_eq_imp_le: "a = c \<or> a = d \<or> b = c \<or> b = d \<Longrightarrow> meet a b \<le> join c d"
   276 by (insert meet_join_le, blast intro: order_trans)
   277 
   278 lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")
   279 proof -
   280   assume a: "x <= z"
   281   have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le)
   282   have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a)
   283   from b c show ?thesis by (simp add: meet_imp_le)
   284 qed
   285 
   286 ML {*
   287 val is_meet_unique = thm "is_meet_unique";
   288 val is_join_unique = thm "is_join_unique";
   289 val join_exists = thm "join_exists";
   290 val meet_exists = thm "meet_exists";
   291 val is_meet_meet = thm "is_meet_meet";
   292 val meet_unique = thm "meet_unique";
   293 val is_join_join = thm "is_join_join";
   294 val join_unique = thm "join_unique";
   295 val meet_left_le = thm "meet_left_le";
   296 val meet_right_le = thm "meet_right_le";
   297 val meet_imp_le = thm "meet_imp_le";
   298 val join_left_le = thm "join_left_le";
   299 val join_right_le = thm "join_right_le";
   300 val join_imp_le = thm "join_imp_le";
   301 val meet_join_le = thms "meet_join_le";
   302 val is_meet_min = thm "is_meet_min";
   303 val is_join_max = thm "is_join_max";
   304 val meet_min = thm "meet_min";
   305 val join_max = thm "join_max";
   306 val meet_idempotent = thm "meet_idempotent";
   307 val join_idempotent = thm "join_idempotent";
   308 val meet_comm = thm "meet_comm";
   309 val join_comm = thm "join_comm";
   310 val meet_assoc = thm "meet_assoc";
   311 val join_assoc = thm "join_assoc";
   312 val meet_left_comm = thm "meet_left_comm";
   313 val meet_left_idempotent = thm "meet_left_idempotent";
   314 val join_left_comm = thm "join_left_comm";
   315 val join_left_idempotent = thm "join_left_idempotent";
   316 val meet_aci = thms "meet_aci";
   317 val join_aci = thms "join_aci";
   318 val le_def_meet = thm "le_def_meet";
   319 val le_def_join = thm "le_def_join";
   320 val meet_join_absorp = thm "meet_join_absorp";
   321 val join_meet_absorp = thm "join_meet_absorp";
   322 val meet_mono = thm "meet_mono";
   323 val join_mono = thm "join_mono";
   324 val distrib_join_le = thm "distrib_join_le";
   325 val distrib_meet_le = thm "distrib_meet_le";
   326 val meet_join_eq_imp_le = thm "meet_join_eq_imp_le";
   327 val modular_le = thm "modular_le";
   328 *}
   329 
   330 end