# HG changeset patch # User haftmann # Date 1262617223 -3600 # Node ID 3b619abaa67a441f18ce0a23a8f6b02408ae52a7 # Parent 54621a41b03c8a48d0ca00341e586315ad276fa0 moved name duplicates to end of theory; reduced warning noise diff -r 54621a41b03c -r 3b619abaa67a src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Mon Jan 04 14:10:13 2010 +0100 +++ b/src/HOL/Orderings.thy Mon Jan 04 16:00:23 2010 +0100 @@ -550,44 +550,6 @@ *} -subsection {* Name duplicates *} - -lemmas order_less_le = less_le -lemmas order_eq_refl = preorder_class.eq_refl -lemmas order_less_irrefl = preorder_class.less_irrefl -lemmas order_le_less = order_class.le_less -lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq -lemmas order_less_imp_le = preorder_class.less_imp_le -lemmas order_less_imp_not_eq = order_class.less_imp_not_eq -lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2 -lemmas order_neq_le_trans = order_class.neq_le_trans -lemmas order_le_neq_trans = order_class.le_neq_trans - -lemmas order_antisym = antisym -lemmas order_less_not_sym = preorder_class.less_not_sym -lemmas order_less_asym = preorder_class.less_asym -lemmas order_eq_iff = order_class.eq_iff -lemmas order_antisym_conv = order_class.antisym_conv -lemmas order_less_trans = preorder_class.less_trans -lemmas order_le_less_trans = preorder_class.le_less_trans -lemmas order_less_le_trans = preorder_class.less_le_trans -lemmas order_less_imp_not_less = preorder_class.less_imp_not_less -lemmas order_less_imp_triv = preorder_class.less_imp_triv -lemmas order_less_asym' = preorder_class.less_asym' - -lemmas linorder_linear = linear -lemmas linorder_less_linear = linorder_class.less_linear -lemmas linorder_le_less_linear = linorder_class.le_less_linear -lemmas linorder_le_cases = linorder_class.le_cases -lemmas linorder_not_less = linorder_class.not_less -lemmas linorder_not_le = linorder_class.not_le -lemmas linorder_neq_iff = linorder_class.neq_iff -lemmas linorder_neqE = linorder_class.neqE -lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1 -lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2 -lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3 - - subsection {* Bounded quantifiers *} syntax @@ -698,7 +660,7 @@ assume r: "!!x y. x < y ==> f x < f y" assume "a < b" hence "f a < f b" by (rule r) also assume "f b < c" - finally (order_less_trans) show ?thesis . + finally (less_trans) show ?thesis . qed lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==> @@ -707,7 +669,7 @@ assume r: "!!x y. x < y ==> f x < f y" assume "a < f b" also assume "b < c" hence "f b < f c" by (rule r) - finally (order_less_trans) show ?thesis . + finally (less_trans) show ?thesis . qed lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==> @@ -716,7 +678,7 @@ assume r: "!!x y. x <= y ==> f x <= f y" assume "a <= b" hence "f a <= f b" by (rule r) also assume "f b < c" - finally (order_le_less_trans) show ?thesis . + finally (le_less_trans) show ?thesis . qed lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==> @@ -725,7 +687,7 @@ assume r: "!!x y. x < y ==> f x < f y" assume "a <= f b" also assume "b < c" hence "f b < f c" by (rule r) - finally (order_le_less_trans) show ?thesis . + finally (le_less_trans) show ?thesis . qed lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==> @@ -734,7 +696,7 @@ assume r: "!!x y. x < y ==> f x < f y" assume "a < b" hence "f a < f b" by (rule r) also assume "f b <= c" - finally (order_less_le_trans) show ?thesis . + finally (less_le_trans) show ?thesis . qed lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==> @@ -743,7 +705,7 @@ assume r: "!!x y. x <= y ==> f x <= f y" assume "a < f b" also assume "b <= c" hence "f b <= f c" by (rule r) - finally (order_less_le_trans) show ?thesis . + finally (less_le_trans) show ?thesis . qed lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==> @@ -876,8 +838,6 @@ ord_eq_less_trans trans -(* FIXME cleanup *) - text {* These support proving chains of decreasing inequalities a >= b >= c ... in Isar proofs. *} @@ -1070,12 +1030,12 @@ lemma min_leastR: "(\x\'a\order. least \ x) \ min x least = least" apply (simp add: min_def) -apply (blast intro: order_antisym) +apply (blast intro: antisym) done lemma max_leastR: "(\x\'a\order. least \ x) \ max x least = x" apply (simp add: max_def) -apply (blast intro: order_antisym) +apply (blast intro: antisym) done @@ -1107,7 +1067,7 @@ lemma wellorder_Least_lemma: fixes k :: 'a assumes "P k" - shows "P (LEAST x. P x)" and "(LEAST x. P x) \ k" + shows LeastI: "P (LEAST x. P x)" and Least_le: "(LEAST x. P x) \ k" proof - have "P (LEAST x. P x) \ (LEAST x. P x) \ k" using assms proof (induct k rule: less_induct) @@ -1132,9 +1092,6 @@ then show "P (LEAST x. P x)" and "(LEAST x. P x) \ k" by auto qed -lemmas LeastI = wellorder_Least_lemma(1) -lemmas Least_le = wellorder_Least_lemma(2) - -- "The following 3 lemmas are due to Brian Huffman" lemma LeastI_ex: "\x. P x \ P (Least P)" by (erule exE) (erule LeastI) @@ -1174,7 +1131,7 @@ bot_bool_eq: "bot = False" instance proof -qed (auto simp add: le_bool_def less_bool_def top_bool_eq bot_bool_eq) +qed (auto simp add: bot_bool_eq top_bool_eq less_bool_def, auto simp add: le_bool_def) end @@ -1221,10 +1178,10 @@ instance "fun" :: (type, preorder) preorder proof qed (auto simp add: le_fun_def less_fun_def - intro: order_trans order_antisym intro!: ext) + intro: order_trans antisym intro!: ext) instance "fun" :: (type, order) order proof -qed (auto simp add: le_fun_def intro: order_antisym ext) +qed (auto simp add: le_fun_def intro: antisym ext) instantiation "fun" :: (type, top) top begin @@ -1257,4 +1214,42 @@ lemma le_funD: "f \ g \ f x \ g x" unfolding le_fun_def by simp + +subsection {* Name duplicates *} + +lemmas order_eq_refl = preorder_class.eq_refl +lemmas order_less_irrefl = preorder_class.less_irrefl +lemmas order_less_imp_le = preorder_class.less_imp_le +lemmas order_less_not_sym = preorder_class.less_not_sym +lemmas order_less_asym = preorder_class.less_asym +lemmas order_less_trans = preorder_class.less_trans +lemmas order_le_less_trans = preorder_class.le_less_trans +lemmas order_less_le_trans = preorder_class.less_le_trans +lemmas order_less_imp_not_less = preorder_class.less_imp_not_less +lemmas order_less_imp_triv = preorder_class.less_imp_triv +lemmas order_less_asym' = preorder_class.less_asym' + +lemmas order_less_le = order_class.less_le +lemmas order_le_less = order_class.le_less +lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq +lemmas order_less_imp_not_eq = order_class.less_imp_not_eq +lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2 +lemmas order_neq_le_trans = order_class.neq_le_trans +lemmas order_le_neq_trans = order_class.le_neq_trans +lemmas order_antisym = order_class.antisym +lemmas order_eq_iff = order_class.eq_iff +lemmas order_antisym_conv = order_class.antisym_conv + +lemmas linorder_linear = linorder_class.linear +lemmas linorder_less_linear = linorder_class.less_linear +lemmas linorder_le_less_linear = linorder_class.le_less_linear +lemmas linorder_le_cases = linorder_class.le_cases +lemmas linorder_not_less = linorder_class.not_less +lemmas linorder_not_le = linorder_class.not_le +lemmas linorder_neq_iff = linorder_class.neq_iff +lemmas linorder_neqE = linorder_class.neqE +lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1 +lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2 +lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3 + end