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