src/HOL/LOrder.thy
author nipkow
Sun Nov 12 19:22:10 2006 +0100 (2006-11-12)
changeset 21312 1d39091a3208
parent 21249 d594c58e24ed
child 21380 c4f79922bc81
permissions -rw-r--r--
started reorgnization of lattice theories
obua@14738
     1
(*  Title:   HOL/LOrder.thy
obua@14738
     2
    ID:      $Id$
obua@14738
     3
    Author:  Steven Obua, TU Muenchen
obua@14738
     4
*)
obua@14738
     5
nipkow@21312
     6
header "Lattice Orders"
obua@14738
     7
nipkow@15131
     8
theory LOrder
haftmann@21249
     9
imports Lattices
nipkow@15131
    10
begin
obua@14738
    11
nipkow@21312
    12
text {* The theory of lattices developed here is taken from
nipkow@21312
    13
\cite{Birkhoff79}.  *}
obua@14738
    14
obua@14738
    15
constdefs
obua@14738
    16
  is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
obua@14738
    17
  "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
    18
  is_join :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
obua@14738
    19
  "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
    20
obua@14738
    21
lemma is_meet_unique: 
obua@14738
    22
  assumes "is_meet u" "is_meet v" shows "u = v"
obua@14738
    23
proof -
obua@14738
    24
  {
obua@14738
    25
    fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
obua@14738
    26
    assume a: "is_meet a"
obua@14738
    27
    assume b: "is_meet b"
obua@14738
    28
    {
obua@14738
    29
      fix x y 
obua@14738
    30
      let ?za = "a x y"
obua@14738
    31
      let ?zb = "b x y"
obua@14738
    32
      from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def)
obua@14738
    33
      with b have "?za <= ?zb" by (auto simp add: is_meet_def)
obua@14738
    34
    }
obua@14738
    35
  }
obua@14738
    36
  note f_le = this
obua@14738
    37
  show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le) 
obua@14738
    38
qed
obua@14738
    39
obua@14738
    40
lemma is_join_unique: 
obua@14738
    41
  assumes "is_join u" "is_join v" shows "u = v"
obua@14738
    42
proof -
obua@14738
    43
  {
obua@14738
    44
    fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
obua@14738
    45
    assume a: "is_join a"
obua@14738
    46
    assume b: "is_join b"
obua@14738
    47
    {
obua@14738
    48
      fix x y 
obua@14738
    49
      let ?za = "a x y"
obua@14738
    50
      let ?zb = "b x y"
obua@14738
    51
      from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def)
obua@14738
    52
      with b have "?zb <= ?za" by (auto simp add: is_join_def)
obua@14738
    53
    }
obua@14738
    54
  }
obua@14738
    55
  note f_le = this
obua@14738
    56
  show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le) 
obua@14738
    57
qed
obua@14738
    58
obua@14738
    59
axclass join_semilorder < order
obua@14738
    60
  join_exists: "? j. is_join j"
obua@14738
    61
obua@14738
    62
axclass meet_semilorder < order
obua@14738
    63
  meet_exists: "? m. is_meet m"
obua@14738
    64
obua@14738
    65
axclass lorder < join_semilorder, meet_semilorder
obua@14738
    66
obua@14738
    67
constdefs
obua@14738
    68
  meet :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
obua@14738
    69
  "meet == THE m. is_meet m"
obua@14738
    70
  join :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
obua@14738
    71
  "join ==  THE j. is_join j"
obua@14738
    72
obua@14738
    73
lemma is_meet_meet: "is_meet (meet::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"
obua@14738
    74
proof -
obua@14738
    75
  from meet_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_meet k" ..
obua@14738
    76
  with is_meet_unique[of _ k] show ?thesis
obua@14738
    77
    by (simp add: meet_def theI[of is_meet])    
obua@14738
    78
qed
obua@14738
    79
obua@14738
    80
lemma meet_unique: "(is_meet m) = (m = meet)" 
obua@14738
    81
by (insert is_meet_meet, auto simp add: is_meet_unique)
obua@14738
    82
obua@14738
    83
lemma is_join_join: "is_join (join::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"
obua@14738
    84
proof -
obua@14738
    85
  from join_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_join k" ..
obua@14738
    86
  with is_join_unique[of _ k] show ?thesis
obua@14738
    87
    by (simp add: join_def theI[of is_join])    
obua@14738
    88
qed
obua@14738
    89
obua@14738
    90
lemma join_unique: "(is_join j) = (j = join)"
obua@14738
    91
by (insert is_join_join, auto simp add: is_join_unique)
obua@14738
    92
obua@14738
    93
lemma meet_left_le: "meet a b \<le> (a::'a::meet_semilorder)"
obua@14738
    94
by (insert is_meet_meet, auto simp add: is_meet_def)
obua@14738
    95
obua@14738
    96
lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"
obua@14738
    97
by (insert is_meet_meet, auto simp add: is_meet_def)
obua@14738
    98
nipkow@21312
    99
(* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *)
nipkow@21312
   100
lemma le_meetI:
nipkow@21312
   101
 "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
obua@14738
   102
by (insert is_meet_meet, auto simp add: is_meet_def)
obua@14738
   103
obua@14738
   104
lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"
obua@14738
   105
by (insert is_join_join, auto simp add: is_join_def)
obua@14738
   106
obua@14738
   107
lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"
obua@14738
   108
by (insert is_join_join, auto simp add: is_join_def)
obua@14738
   109
nipkow@21312
   110
lemma join_leI:
nipkow@21312
   111
 "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
nipkow@21312
   114
lemmas meet_join_le[simp] = meet_left_le meet_right_le join_left_le join_right_le
nipkow@21312
   115
nipkow@21312
   116
lemma le_meet[simp]: "(x <= meet y z) = (x <= y & x <= z)" (is "?L = ?R")
nipkow@21312
   117
proof
nipkow@21312
   118
  assume ?L
nipkow@21312
   119
  moreover have "meet y z \<le> y" "meet y z <= z" by(simp_all)
nipkow@21312
   120
  ultimately show ?R by(blast intro:order_trans)
nipkow@21312
   121
next
nipkow@21312
   122
  assume ?R thus ?L by (blast intro!:le_meetI)
nipkow@21312
   123
qed
nipkow@21312
   124
nipkow@21312
   125
lemma join_le[simp]: "(join x y <= z) = (x <= z & y <= z)" (is "?L = ?R")
nipkow@21312
   126
proof
nipkow@21312
   127
  assume ?L
nipkow@21312
   128
  moreover have "x \<le> join x y" "y \<le> join x y" by(simp_all)
nipkow@21312
   129
  ultimately show ?R by(blast intro:order_trans)
nipkow@21312
   130
next
nipkow@21312
   131
  assume ?R thus ?L by (blast intro:join_leI)
nipkow@21312
   132
qed
nipkow@21312
   133
obua@14738
   134
obua@14738
   135
lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
obua@14738
   136
by (auto simp add: is_meet_def min_def)
obua@14738
   137
obua@14738
   138
lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
obua@14738
   139
by (auto simp add: is_join_def max_def)
obua@14738
   140
obua@14738
   141
instance linorder \<subseteq> meet_semilorder
obua@14738
   142
proof
obua@14738
   143
  from is_meet_min show "? (m::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_meet m" by auto
obua@14738
   144
qed
obua@14738
   145
obua@14738
   146
instance linorder \<subseteq> join_semilorder
obua@14738
   147
proof
obua@14738
   148
  from is_join_max show "? (j::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_join j" by auto 
obua@14738
   149
qed
obua@14738
   150
    
obua@14738
   151
instance linorder \<subseteq> lorder ..
obua@14738
   152
obua@14738
   153
lemma meet_min: "meet = (min :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))" 
obua@14738
   154
by (simp add: is_meet_meet is_meet_min is_meet_unique)
obua@14738
   155
obua@14738
   156
lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
obua@14738
   157
by (simp add: is_join_join is_join_max is_join_unique)
obua@14738
   158
obua@14738
   159
lemma meet_idempotent[simp]: "meet x x = x"
nipkow@21312
   160
by (rule order_antisym, simp_all add: le_meetI)
obua@14738
   161
obua@14738
   162
lemma join_idempotent[simp]: "join x x = x"
nipkow@21312
   163
by (rule order_antisym, simp_all add: join_leI)
obua@14738
   164
obua@14738
   165
lemma meet_comm: "meet x y = meet y x" 
nipkow@21312
   166
by (rule order_antisym, (simp add: le_meetI)+)
obua@14738
   167
obua@14738
   168
lemma join_comm: "join x y = join y x"
nipkow@21312
   169
by (rule order_antisym, (simp add: join_leI)+)
nipkow@21312
   170
nipkow@21312
   171
lemma meet_leI1: "x \<le> z \<Longrightarrow> meet x y \<le> z"
nipkow@21312
   172
apply(subgoal_tac "meet x y <= x")
nipkow@21312
   173
 apply(blast intro:order_trans)
nipkow@21312
   174
apply simp
nipkow@21312
   175
done
nipkow@21312
   176
nipkow@21312
   177
lemma meet_leI2: "y \<le> z \<Longrightarrow> meet x y \<le> z"
nipkow@21312
   178
apply(subgoal_tac "meet x y <= y")
nipkow@21312
   179
 apply(blast intro:order_trans)
nipkow@21312
   180
apply simp
nipkow@21312
   181
done
obua@14738
   182
nipkow@21312
   183
lemma le_joinI1: "x \<le> y \<Longrightarrow> x \<le> join y z"
nipkow@21312
   184
apply(subgoal_tac "y <= join y z")
nipkow@21312
   185
 apply(blast intro:order_trans)
nipkow@21312
   186
apply simp
nipkow@21312
   187
done
nipkow@21312
   188
nipkow@21312
   189
lemma le_joinI2: "x \<le> z \<Longrightarrow> x \<le> join y z"
nipkow@21312
   190
apply(subgoal_tac "z <= join y z")
nipkow@21312
   191
 apply(blast intro:order_trans)
nipkow@21312
   192
apply simp
nipkow@21312
   193
done
obua@14738
   194
nipkow@21312
   195
lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)"
nipkow@21312
   196
apply(rule order_antisym)
nipkow@21312
   197
apply (simp add:meet_leI1 meet_leI2)
nipkow@21312
   198
apply (simp add:meet_leI1 meet_leI2)
nipkow@21312
   199
done
nipkow@21312
   200
nipkow@21312
   201
lemma join_assoc: "join (join x y) z = join x (join y z)"
nipkow@21312
   202
apply(rule order_antisym)
nipkow@21312
   203
apply (simp add:le_joinI1 le_joinI2)
nipkow@21312
   204
apply (simp add:le_joinI1 le_joinI2)
nipkow@21312
   205
done
obua@14738
   206
obua@14738
   207
lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"
obua@14738
   208
by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)
obua@14738
   209
obua@14738
   210
lemma meet_left_idempotent: "meet y (meet y x) = meet y x"
obua@14738
   211
by (simp add: meet_assoc meet_comm meet_left_comm)
obua@14738
   212
obua@14738
   213
lemma join_left_comm: "join a (join b c) = join b (join a c)"
obua@14738
   214
by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc)
obua@14738
   215
obua@14738
   216
lemma join_left_idempotent: "join y (join y x) = join y x"
obua@14738
   217
by (simp add: join_assoc join_comm join_left_comm)
obua@14738
   218
    
obua@14738
   219
lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent
obua@14738
   220
obua@14738
   221
lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
obua@14738
   222
nipkow@21312
   223
lemma le_def_meet: "(x <= y) = (meet x y = x)"
nipkow@21312
   224
apply rule
nipkow@21312
   225
apply(simp add: order_antisym)
nipkow@21312
   226
apply(subgoal_tac "meet x y <= y")
nipkow@21312
   227
apply(simp)
nipkow@21312
   228
apply(simp (no_asm))
nipkow@21312
   229
done
obua@14738
   230
nipkow@21312
   231
lemma le_def_join: "(x <= y) = (join x y = y)"
nipkow@21312
   232
apply rule
nipkow@21312
   233
apply(simp add: order_antisym)
nipkow@21312
   234
apply(subgoal_tac "x <= join x y")
nipkow@21312
   235
apply(simp)
nipkow@21312
   236
apply(simp (no_asm))
nipkow@21312
   237
done
nipkow@21312
   238
nipkow@21312
   239
lemma join_absorp2: "a \<le> b \<Longrightarrow> join a b = b" 
nipkow@21312
   240
by (simp add: le_def_join)
nipkow@21312
   241
nipkow@21312
   242
lemma join_absorp1: "b \<le> a \<Longrightarrow> join a b = a"
nipkow@21312
   243
by (simp add: le_def_join join_aci)
nipkow@21312
   244
nipkow@21312
   245
lemma meet_absorp1: "a \<le> b \<Longrightarrow> meet a b = a"
nipkow@21312
   246
by (simp add: le_def_meet)
nipkow@21312
   247
nipkow@21312
   248
lemma meet_absorp2: "b \<le> a \<Longrightarrow> meet a b = b"
nipkow@21312
   249
by (simp add: le_def_meet meet_aci)
obua@14738
   250
obua@14738
   251
lemma meet_join_absorp: "meet x (join x y) = x"
nipkow@21312
   252
by(simp add:meet_absorp1)
obua@14738
   253
obua@14738
   254
lemma join_meet_absorp: "join x (meet x y) = x"
nipkow@21312
   255
by(simp add:join_absorp1)
obua@14738
   256
obua@14738
   257
lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"
nipkow@21312
   258
by(simp add:meet_leI2)
obua@14738
   259
obua@14738
   260
lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
nipkow@21312
   261
by(simp add:le_joinI2)
obua@14738
   262
obua@14738
   263
lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")
obua@14738
   264
proof -
nipkow@21312
   265
  have a: "x <= ?r" by (simp_all add:le_meetI)
nipkow@21312
   266
  have b: "meet y z <= ?r" by (simp add:le_joinI2)
nipkow@21312
   267
  from a b show ?thesis by (simp add: join_leI)
obua@14738
   268
qed
obua@14738
   269
  
nipkow@21312
   270
lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")
obua@14738
   271
proof -
nipkow@21312
   272
  have a: "?l <= x" by (simp_all add: join_leI)
nipkow@21312
   273
  have b: "?l <= join y z" by (simp add:meet_leI2)
nipkow@21312
   274
  from a b show ?thesis by (simp add: le_meetI)
obua@14738
   275
qed
obua@14738
   276
obua@14738
   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"
nipkow@21312
   278
by (auto simp:meet_leI2 meet_leI1)
obua@14738
   279
obua@14738
   280
lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")
obua@14738
   281
proof -
obua@14738
   282
  assume a: "x <= z"
nipkow@21312
   283
  have b: "?t <= join x y" by (simp_all add: join_leI meet_join_eq_imp_le )
nipkow@21312
   284
  have c: "?t <= z" by (simp_all add: a join_leI)
nipkow@21312
   285
  from b c show ?thesis by (simp add: le_meetI)
obua@14738
   286
qed
obua@14738
   287
nipkow@15131
   288
end