# HG changeset patch # User haftmann # Date 1163805619 -3600 # Node ID a259061ad0b05983dc0677209f377824c94cc2de # Parent a9671d4f7c033d57a6fbed04b9f8bd182bab940f re-eliminated thm trichotomy diff -r a9671d4f7c03 -r a259061ad0b0 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Sat Nov 18 00:20:18 2006 +0100 +++ b/src/HOL/Orderings.thy Sat Nov 18 00:20:19 2006 +0100 @@ -208,11 +208,11 @@ assumes linear: "x \ y \ y \ x" begin -lemma trichotomy: "x \ y \ x = y \ y \ x" +lemma less_linear: "x \ y \ x = y \ y \ x" unfolding less_le using less_le linear by blast lemma le_less_linear: "x \ y \ y \ x" - by (simp add: le_less trichotomy) + by (simp add: le_less less_linear) lemma le_cases [case_names le ge]: "\ x \ y \ P; y \ x \ P\ \ P" @@ -220,7 +220,7 @@ lemma cases [case_names less equal greater]: "\ x \ y \ P; x = y \ P; y \ x \ P\ \ P" - using trichotomy by blast + using less_linear by blast lemma not_less: "\ x \ y \ y \ x" apply (simp add: less_le) @@ -233,7 +233,7 @@ done lemma neq_iff: "x \ y \ x \ y \ y \ x" - by (cut_tac x = x and y = y in trichotomy, auto) + by (cut_tac x = x and y = y in less_linear, auto) lemma neqE: "\ x \ y; x \ y \ R; y \ x \ R\ \ R" by (simp add: neq_iff) blast @@ -278,19 +278,19 @@ lemma min_less_iff_disj: "min x y \ z \ x \ z \ y \ z" - unfolding min_def le_less using trichotomy by (auto intro: less_trans) + unfolding min_def le_less using less_linear by (auto intro: less_trans) lemma less_max_iff_disj: "z \ max x y \ z \ x \ z \ y" - unfolding max_def le_less using trichotomy by (auto intro: less_trans) + unfolding max_def le_less using less_linear by (auto intro: less_trans) lemma min_less_iff_conj [simp]: "z \ min x y \ z \ x \ z \ y" - unfolding min_def le_less using trichotomy by (auto intro: less_trans) + unfolding min_def le_less using less_linear by (auto intro: less_trans) lemma max_less_iff_conj [simp]: "max x y \ z \ x \ z \ y \ z" - unfolding max_def le_less using trichotomy by (auto intro: less_trans) + unfolding max_def le_less using less_linear by (auto intro: less_trans) lemma split_min: "P (min i j) \ (i \ j \ P i) \ (\ i \ j \ P j)" @@ -332,7 +332,7 @@ lemmas order_neq_le_trans [where 'b = "?'a::order"] = order.neq_le_trans lemmas order_le_neq_trans [where 'b = "?'a::order"] = order.le_neq_trans lemmas order_less_asym' [where 'b = "?'a::order"] = order.less_asym' -lemmas linorder_less_linear [where 'b = "?'a::linorder"] = linorder.trichotomy +lemmas linorder_less_linear [where 'b = "?'a::linorder"] = linorder.less_linear lemmas linorder_le_less_linear [where 'b = "?'a::linorder"] = linorder.le_less_linear lemmas linorder_le_cases [where 'b = "?'a::linorder"] = linorder.le_cases lemmas linorder_cases [where 'b = "?'a::linorder"] = linorder.cases