291 end |
291 end |
292 |
292 |
293 axclass linorder < order |
293 axclass linorder < order |
294 linorder_linear: "x <= y | y <= x" |
294 linorder_linear: "x <= y | y <= x" |
295 |
295 |
296 interpretation linorder: |
296 interpretation order: |
297 linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool"] |
297 linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool"] |
298 by unfold_locales (rule linorder_linear) |
298 by unfold_locales (rule linorder_linear) |
299 |
299 |
300 |
300 |
301 subsection {* Name duplicates *} |
301 subsection {* Name duplicates *} |
318 lemmas order_less_imp_not_eq [where 'b = "?'a::order"] = order.less_imp_not_eq |
318 lemmas order_less_imp_not_eq [where 'b = "?'a::order"] = order.less_imp_not_eq |
319 lemmas order_less_imp_not_eq2 [where 'b = "?'a::order"] = order.less_imp_not_eq2 |
319 lemmas order_less_imp_not_eq2 [where 'b = "?'a::order"] = order.less_imp_not_eq2 |
320 lemmas order_neq_le_trans [where 'b = "?'a::order"] = order.neq_le_trans |
320 lemmas order_neq_le_trans [where 'b = "?'a::order"] = order.neq_le_trans |
321 lemmas order_le_neq_trans [where 'b = "?'a::order"] = order.le_neq_trans |
321 lemmas order_le_neq_trans [where 'b = "?'a::order"] = order.le_neq_trans |
322 lemmas order_less_asym' [where 'b = "?'a::order"] = order.less_asym' |
322 lemmas order_less_asym' [where 'b = "?'a::order"] = order.less_asym' |
323 lemmas linorder_less_linear [where 'b = "?'a::linorder"] = linorder.less_linear |
323 lemmas linorder_less_linear [where 'b = "?'a::linorder"] = order.less_linear |
324 lemmas linorder_le_less_linear [where 'b = "?'a::linorder"] = linorder.le_less_linear |
324 lemmas linorder_le_less_linear [where 'b = "?'a::linorder"] = order.le_less_linear |
325 lemmas linorder_le_cases [where 'b = "?'a::linorder"] = linorder.le_cases |
325 lemmas linorder_le_cases [where 'b = "?'a::linorder"] = order.le_cases |
326 lemmas linorder_cases [where 'b = "?'a::linorder"] = linorder.cases |
326 lemmas linorder_cases [where 'b = "?'a::linorder"] = order.cases |
327 lemmas linorder_not_less [where 'b = "?'a::linorder"] = linorder.not_less |
327 lemmas linorder_not_less [where 'b = "?'a::linorder"] = order.not_less |
328 lemmas linorder_not_le [where 'b = "?'a::linorder"] = linorder.not_le |
328 lemmas linorder_not_le [where 'b = "?'a::linorder"] = order.not_le |
329 lemmas linorder_neq_iff [where 'b = "?'a::linorder"] = linorder.neq_iff |
329 lemmas linorder_neq_iff [where 'b = "?'a::linorder"] = order.neq_iff |
330 lemmas linorder_neqE [where 'b = "?'a::linorder"] = linorder.neqE |
330 lemmas linorder_neqE [where 'b = "?'a::linorder"] = order.neqE |
331 lemmas linorder_antisym_conv1 [where 'b = "?'a::linorder"] = linorder.antisym_conv1 |
331 lemmas linorder_antisym_conv1 [where 'b = "?'a::linorder"] = order.antisym_conv1 |
332 lemmas linorder_antisym_conv2 [where 'b = "?'a::linorder"] = linorder.antisym_conv2 |
332 lemmas linorder_antisym_conv2 [where 'b = "?'a::linorder"] = order.antisym_conv2 |
333 lemmas linorder_antisym_conv3 [where 'b = "?'a::linorder"] = linorder.antisym_conv3 |
333 lemmas linorder_antisym_conv3 [where 'b = "?'a::linorder"] = order.antisym_conv3 |
334 lemmas leI [where 'b = "?'a::linorder"] = linorder.leI |
334 lemmas leI [where 'b = "?'a::linorder"] = order.leI |
335 lemmas leD [where 'b = "?'a::linorder"] = linorder.leD |
335 lemmas leD [where 'b = "?'a::linorder"] = order.leD |
336 lemmas not_leE [where 'b = "?'a::linorder"] = linorder.not_leE |
336 lemmas not_leE [where 'b = "?'a::linorder"] = order.not_leE |
337 |
337 |
338 |
338 |
339 subsection {* Reasoning tools setup *} |
339 subsection {* Reasoning tools setup *} |
340 |
340 |
341 ML {* |
341 ML {* |
864 min :: "['a::ord, 'a] => 'a" |
864 min :: "['a::ord, 'a] => 'a" |
865 "min a b == (if a <= b then a else b)" |
865 "min a b == (if a <= b then a else b)" |
866 max :: "['a::ord, 'a] => 'a" |
866 max :: "['a::ord, 'a] => 'a" |
867 "max a b == (if a <= b then b else a)" |
867 "max a b == (if a <= b then b else a)" |
868 |
868 |
869 hide const linorder.less_eq_less.max linorder.less_eq_less.min (* FIXME !? *) |
869 hide const order.less_eq_less.max order.less_eq_less.min (* FIXME !? *) |
870 |
870 |
871 lemma min_linorder: |
871 lemma min_linorder: |
872 "linorder.min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = min" |
872 "linorder.min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = min" |
873 by (rule+) (simp add: min_def linorder.min_def) |
873 by (rule+) (simp add: min_def order.min_def) |
874 |
874 |
875 lemma max_linorder: |
875 lemma max_linorder: |
876 "linorder.max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = max" |
876 "linorder.max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = max" |
877 by (rule+) (simp add: max_def linorder.max_def) |
877 by (rule+) (simp add: max_def order.max_def) |
878 |
878 |
879 lemmas min_le_iff_disj = linorder.min_le_iff_disj [where 'b = "?'a::linorder", simplified min_linorder] |
879 lemmas min_le_iff_disj = order.min_le_iff_disj [where 'b = "?'a::linorder", simplified min_linorder] |
880 lemmas le_max_iff_disj = linorder.le_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder] |
880 lemmas le_max_iff_disj = order.le_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder] |
881 lemmas min_less_iff_disj = linorder.min_less_iff_disj [where 'b = "?'a::linorder", simplified min_linorder] |
881 lemmas min_less_iff_disj = order.min_less_iff_disj [where 'b = "?'a::linorder", simplified min_linorder] |
882 lemmas less_max_iff_disj = linorder.less_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder] |
882 lemmas less_max_iff_disj = order.less_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder] |
883 lemmas min_less_iff_conj [simp] = linorder.min_less_iff_conj [where 'b = "?'a::linorder", simplified min_linorder] |
883 lemmas min_less_iff_conj [simp] = order.min_less_iff_conj [where 'b = "?'a::linorder", simplified min_linorder] |
884 lemmas max_less_iff_conj [simp] = linorder.max_less_iff_conj [where 'b = "?'a::linorder", simplified max_linorder] |
884 lemmas max_less_iff_conj [simp] = order.max_less_iff_conj [where 'b = "?'a::linorder", simplified max_linorder] |
885 lemmas split_min = linorder.split_min [where 'b = "?'a::linorder", simplified min_linorder] |
885 lemmas split_min = order.split_min [where 'b = "?'a::linorder", simplified min_linorder] |
886 lemmas split_max = linorder.split_max [where 'b = "?'a::linorder", simplified max_linorder] |
886 lemmas split_max = order.split_max [where 'b = "?'a::linorder", simplified max_linorder] |
887 |
887 |
888 lemma min_leastL: "(!!x. least <= x) ==> min least x = least" |
888 lemma min_leastL: "(!!x. least <= x) ==> min least x = least" |
889 by (simp add: min_def) |
889 by (simp add: min_def) |
890 |
890 |
891 lemma max_leastL: "(!!x. least <= x) ==> max least x = x" |
891 lemma max_leastL: "(!!x. least <= x) ==> max least x = x" |