equal
deleted
inserted
replaced
1086 class bot = order + |
1086 class bot = order + |
1087 fixes bot :: 'a |
1087 fixes bot :: 'a |
1088 assumes bot_least [simp]: "bot \<le> x" |
1088 assumes bot_least [simp]: "bot \<le> x" |
1089 begin |
1089 begin |
1090 |
1090 |
|
1091 lemma bot_unique: |
|
1092 "a \<le> bot \<longleftrightarrow> a = bot" |
|
1093 by (auto simp add: intro: antisym) |
|
1094 |
1091 lemma bot_less: |
1095 lemma bot_less: |
1092 "a \<noteq> bot \<longleftrightarrow> bot < a" |
1096 "a \<noteq> bot \<longleftrightarrow> bot < a" |
1093 by (auto simp add: less_le_not_le intro!: antisym) |
1097 by (auto simp add: less_le_not_le intro!: antisym) |
1094 |
1098 |
1095 end |
1099 end |
1096 |
1100 |
1097 class top = order + |
1101 class top = order + |
1098 fixes top :: 'a |
1102 fixes top :: 'a |
1099 assumes top_greatest [simp]: "x \<le> top" |
1103 assumes top_greatest [simp]: "x \<le> top" |
1100 begin |
1104 begin |
|
1105 |
|
1106 lemma top_unique: |
|
1107 "top \<le> a \<longleftrightarrow> a = top" |
|
1108 by (auto simp add: intro: antisym) |
1101 |
1109 |
1102 lemma less_top: |
1110 lemma less_top: |
1103 "a \<noteq> top \<longleftrightarrow> a < top" |
1111 "a \<noteq> top \<longleftrightarrow> a < top" |
1104 by (auto simp add: less_le_not_le intro!: antisym) |
1112 by (auto simp add: less_le_not_le intro!: antisym) |
1105 |
1113 |