src/HOL/LOrder.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 15524 2ef571f80a55 child 17508 c84af7f39a6b permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:   HOL/LOrder.thy

     2     ID:      $Id$

     3     Author:  Steven Obua, TU Muenchen

     4 *)

     5

     6 header {* Lattice Orders *}

     7

     8 theory LOrder

     9 imports Orderings

    10 begin

    11

    12 text {*

    13   The theory of lattices developed here is taken from the book:

    14   \begin{itemize}

    15   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979.

    16   \end{itemize}

    17 *}

    18

    19 constdefs

    20   is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"

    21   "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)"

    22   is_join :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"

    23   "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)"

    24

    25 lemma is_meet_unique:

    26   assumes "is_meet u" "is_meet v" shows "u = v"

    27 proof -

    28   {

    29     fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

    30     assume a: "is_meet a"

    31     assume b: "is_meet b"

    32     {

    33       fix x y

    34       let ?za = "a x y"

    35       let ?zb = "b x y"

    36       from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def)

    37       with b have "?za <= ?zb" by (auto simp add: is_meet_def)

    38     }

    39   }

    40   note f_le = this

    41   show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)

    42 qed

    43

    44 lemma is_join_unique:

    45   assumes "is_join u" "is_join v" shows "u = v"

    46 proof -

    47   {

    48     fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

    49     assume a: "is_join a"

    50     assume b: "is_join b"

    51     {

    52       fix x y

    53       let ?za = "a x y"

    54       let ?zb = "b x y"

    55       from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def)

    56       with b have "?zb <= ?za" by (auto simp add: is_join_def)

    57     }

    58   }

    59   note f_le = this

    60   show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)

    61 qed

    62

    63 axclass join_semilorder < order

    64   join_exists: "? j. is_join j"

    65

    66 axclass meet_semilorder < order

    67   meet_exists: "? m. is_meet m"

    68

    69 axclass lorder < join_semilorder, meet_semilorder

    70

    71 constdefs

    72   meet :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"

    73   "meet == THE m. is_meet m"

    74   join :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"

    75   "join ==  THE j. is_join j"

    76

    77 lemma is_meet_meet: "is_meet (meet::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"

    78 proof -

    79   from meet_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_meet k" ..

    80   with is_meet_unique[of _ k] show ?thesis

    81     by (simp add: meet_def theI[of is_meet])

    82 qed

    83

    84 lemma meet_unique: "(is_meet m) = (m = meet)"

    85 by (insert is_meet_meet, auto simp add: is_meet_unique)

    86

    87 lemma is_join_join: "is_join (join::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"

    88 proof -

    89   from join_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_join k" ..

    90   with is_join_unique[of _ k] show ?thesis

    91     by (simp add: join_def theI[of is_join])

    92 qed

    93

    94 lemma join_unique: "(is_join j) = (j = join)"

    95 by (insert is_join_join, auto simp add: is_join_unique)

    96

    97 lemma meet_left_le: "meet a b \<le> (a::'a::meet_semilorder)"

    98 by (insert is_meet_meet, auto simp add: is_meet_def)

    99

   100 lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"

   101 by (insert is_meet_meet, auto simp add: is_meet_def)

   102

   103 lemma meet_imp_le: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"

   104 by (insert is_meet_meet, auto simp add: is_meet_def)

   105

   106 lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"

   107 by (insert is_join_join, auto simp add: is_join_def)

   108

   109 lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"

   110 by (insert is_join_join, auto simp add: is_join_def)

   111

   112 lemma join_imp_le: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"

   113 by (insert is_join_join, auto simp add: is_join_def)

   114

   115 lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le

   116

   117 lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"

   118 by (auto simp add: is_meet_def min_def)

   119

   120 lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"

   121 by (auto simp add: is_join_def max_def)

   122

   123 instance linorder \<subseteq> meet_semilorder

   124 proof

   125   from is_meet_min show "? (m::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_meet m" by auto

   126 qed

   127

   128 instance linorder \<subseteq> join_semilorder

   129 proof

   130   from is_join_max show "? (j::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_join j" by auto

   131 qed

   132

   133 instance linorder \<subseteq> lorder ..

   134

   135 lemma meet_min: "meet = (min :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"

   136 by (simp add: is_meet_meet is_meet_min is_meet_unique)

   137

   138 lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"

   139 by (simp add: is_join_join is_join_max is_join_unique)

   140

   141 lemma meet_idempotent[simp]: "meet x x = x"

   142 by (rule order_antisym, simp_all add: meet_left_le meet_imp_le)

   143

   144 lemma join_idempotent[simp]: "join x x = x"

   145 by (rule order_antisym, simp_all add: join_left_le join_imp_le)

   146

   147 lemma meet_comm: "meet x y = meet y x"

   148 by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+)

   149

   150 lemma join_comm: "join x y = join y x"

   151 by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+)

   152

   153 lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r")

   154 proof -

   155   have "?l <= meet x y & meet x y <= x & ?l <= z & meet x y <= y" by (simp add: meet_left_le meet_right_le)

   156   hence "?l <= x & ?l <= y & ?l <= z" by auto

   157   hence "?l <= ?r" by (simp add: meet_imp_le)

   158   hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le)

   159   have "?r <= meet y z & meet y z <= y & meet y z <= z & ?r <= x" by (simp add: meet_left_le meet_right_le)

   160   hence "?r <= x & ?r <= y & ?r <= z" by (auto)

   161   hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le)

   162   hence b:"?r <= ?l" by (simp add: meet_imp_le)

   163   from a b show "?l = ?r" by auto

   164 qed

   165

   166 lemma join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r")

   167 proof -

   168   have "join x y <= ?l & x <= join x y & z <= ?l & y <= join x y" by (simp add: join_left_le join_right_le)

   169   hence "x <= ?l & y <= ?l & z <= ?l" by auto

   170   hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le)

   171   hence a:"?r <= ?l" by (simp add: join_imp_le)

   172   have "join y z <= ?r & y <= join y z & z <= join y z & x <= ?r" by (simp add: join_left_le join_right_le)

   173   hence "y <= ?r & z <= ?r & x <= ?r" by auto

   174   hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le)

   175   hence b:"?l <= ?r" by (simp add: join_imp_le)

   176   from a b show "?l = ?r" by auto

   177 qed

   178

   179 lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"

   180 by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)

   181

   182 lemma meet_left_idempotent: "meet y (meet y x) = meet y x"

   183 by (simp add: meet_assoc meet_comm meet_left_comm)

   184

   185 lemma join_left_comm: "join a (join b c) = join b (join a c)"

   186 by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc)

   187

   188 lemma join_left_idempotent: "join y (join y x) = join y x"

   189 by (simp add: join_assoc join_comm join_left_comm)

   190

   191 lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent

   192

   193 lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent

   194

   195 lemma le_def_meet: "(x <= y) = (meet x y = x)"

   196 proof -

   197   have u: "x <= y \<longrightarrow> meet x y = x"

   198   proof

   199     assume "x <= y"

   200     hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le)

   201     thus "meet x y = x" by auto

   202   qed

   203   have v:"meet x y = x \<longrightarrow> x <= y"

   204   proof

   205     have a:"meet x y <= y" by (simp add: meet_right_le)

   206     assume "meet x y = x"

   207     hence "x = meet x y" by auto

   208     with a show "x <= y" by (auto)

   209   qed

   210   from u v show ?thesis by blast

   211 qed

   212

   213 lemma le_def_join: "(x <= y) = (join x y = y)"

   214 proof -

   215   have u: "x <= y \<longrightarrow> join x y = y"

   216   proof

   217     assume "x <= y"

   218     hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le)

   219     thus "join x y = y" by auto

   220   qed

   221   have v:"join x y = y \<longrightarrow> x <= y"

   222   proof

   223     have a:"x <= join x y" by (simp add: join_left_le)

   224     assume "join x y = y"

   225     hence "y = join x y" by auto

   226     with a show "x <= y" by (auto)

   227   qed

   228   from u v show ?thesis by blast

   229 qed

   230

   231 lemma meet_join_absorp: "meet x (join x y) = x"

   232 proof -

   233   have a:"meet x (join x y) <= x" by (simp add: meet_left_le)

   234   have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le)

   235   from a b show ?thesis by auto

   236 qed

   237

   238 lemma join_meet_absorp: "join x (meet x y) = x"

   239 proof -

   240   have a:"x <= join x (meet x y)" by (simp add: join_left_le)

   241   have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le)

   242   from a b show ?thesis by auto

   243 qed

   244

   245 lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"

   246 proof -

   247   assume a: "y <= z"

   248   have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le)

   249   with a have "meet x y <= x & meet x y <= z" by auto

   250   thus "meet x y <= meet x z" by (simp add: meet_imp_le)

   251 qed

   252

   253 lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"

   254 proof -

   255   assume a: "y \<le> z"

   256   have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le)

   257   with a have "x <= join x z & y <= join x z" by auto

   258   thus "join x y <= join x z" by (simp add: join_imp_le)

   259 qed

   260

   261 lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")

   262 proof -

   263   have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le)

   264   from meet_join_le have b: "meet y z <= ?r"

   265     by (rule_tac meet_imp_le, (blast intro: order_trans)+)

   266   from a b show ?thesis by (simp add: join_imp_le)

   267 qed

   268

   269 lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")

   270 proof -

   271   have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le)

   272   from meet_join_le have b: "?l <= join y z"

   273     by (rule_tac join_imp_le, (blast intro: order_trans)+)

   274   from a b show ?thesis by (simp add: meet_imp_le)

   275 qed

   276

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

   278 by (insert meet_join_le, blast intro: order_trans)

   279

   280 lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")

   281 proof -

   282   assume a: "x <= z"

   283   have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le)

   284   have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a)

   285   from b c show ?thesis by (simp add: meet_imp_le)

   286 qed

   287

   288 ML {*

   289 val is_meet_unique = thm "is_meet_unique";

   290 val is_join_unique = thm "is_join_unique";

   291 val join_exists = thm "join_exists";

   292 val meet_exists = thm "meet_exists";

   293 val is_meet_meet = thm "is_meet_meet";

   294 val meet_unique = thm "meet_unique";

   295 val is_join_join = thm "is_join_join";

   296 val join_unique = thm "join_unique";

   297 val meet_left_le = thm "meet_left_le";

   298 val meet_right_le = thm "meet_right_le";

   299 val meet_imp_le = thm "meet_imp_le";

   300 val join_left_le = thm "join_left_le";

   301 val join_right_le = thm "join_right_le";

   302 val join_imp_le = thm "join_imp_le";

   303 val meet_join_le = thms "meet_join_le";

   304 val is_meet_min = thm "is_meet_min";

   305 val is_join_max = thm "is_join_max";

   306 val meet_min = thm "meet_min";

   307 val join_max = thm "join_max";

   308 val meet_idempotent = thm "meet_idempotent";

   309 val join_idempotent = thm "join_idempotent";

   310 val meet_comm = thm "meet_comm";

   311 val join_comm = thm "join_comm";

   312 val meet_assoc = thm "meet_assoc";

   313 val join_assoc = thm "join_assoc";

   314 val meet_left_comm = thm "meet_left_comm";

   315 val meet_left_idempotent = thm "meet_left_idempotent";

   316 val join_left_comm = thm "join_left_comm";

   317 val join_left_idempotent = thm "join_left_idempotent";

   318 val meet_aci = thms "meet_aci";

   319 val join_aci = thms "join_aci";

   320 val le_def_meet = thm "le_def_meet";

   321 val le_def_join = thm "le_def_join";

   322 val meet_join_absorp = thm "meet_join_absorp";

   323 val join_meet_absorp = thm "join_meet_absorp";

   324 val meet_mono = thm "meet_mono";

   325 val join_mono = thm "join_mono";

   326 val distrib_join_le = thm "distrib_join_le";

   327 val distrib_meet_le = thm "distrib_meet_le";

   328 val meet_join_eq_imp_le = thm "meet_join_eq_imp_le";

   329 val modular_le = thm "modular_le";

   330 *}

   331

   332 end