equal
deleted
inserted
replaced
1285 |
1285 |
1286 lemma bot_less: |
1286 lemma bot_less: |
1287 "a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a" |
1287 "a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a" |
1288 by (fact bot.not_eq_extremum) |
1288 by (fact bot.not_eq_extremum) |
1289 |
1289 |
|
1290 lemma max_bot[simp]: "max bot x = x" |
|
1291 by(simp add: max_def bot_unique) |
|
1292 |
|
1293 lemma max_bot2[simp]: "max x bot = x" |
|
1294 by(simp add: max_def bot_unique) |
|
1295 |
|
1296 lemma min_bot[simp]: "min bot x = bot" |
|
1297 by(simp add: min_def bot_unique) |
|
1298 |
|
1299 lemma min_bot2[simp]: "min x bot = bot" |
|
1300 by(simp add: min_def bot_unique) |
|
1301 |
1290 end |
1302 end |
1291 |
1303 |
1292 class top = |
1304 class top = |
1293 fixes top :: 'a ("\<top>") |
1305 fixes top :: 'a ("\<top>") |
1294 |
1306 |
1312 by (fact top.extremum_strict) |
1324 by (fact top.extremum_strict) |
1313 |
1325 |
1314 lemma less_top: |
1326 lemma less_top: |
1315 "a \<noteq> \<top> \<longleftrightarrow> a < \<top>" |
1327 "a \<noteq> \<top> \<longleftrightarrow> a < \<top>" |
1316 by (fact top.not_eq_extremum) |
1328 by (fact top.not_eq_extremum) |
|
1329 |
|
1330 lemma max_top[simp]: "max top x = top" |
|
1331 by(simp add: max_def top_unique) |
|
1332 |
|
1333 lemma max_top2[simp]: "max x top = top" |
|
1334 by(simp add: max_def top_unique) |
|
1335 |
|
1336 lemma min_top[simp]: "min top x = x" |
|
1337 by(simp add: min_def top_unique) |
|
1338 |
|
1339 lemma min_top2[simp]: "min x top = x" |
|
1340 by(simp add: min_def top_unique) |
1317 |
1341 |
1318 end |
1342 end |
1319 |
1343 |
1320 |
1344 |
1321 subsection \<open>Dense orders\<close> |
1345 subsection \<open>Dense orders\<close> |