# HG changeset patch # User haftmann # Date 1265624010 -3600 # Node ID f2f1e50bf65d8190e6f688c4e1ec40212f7d1ae5 # Parent 0ea45a4d32f381bbf5a5b07727e926ea43e0b06b# Parent 22aab1c5e5a83438d6b9e0c632356926a7f861b3 merged diff -r 0ea45a4d32f3 -r f2f1e50bf65d NEWS --- a/NEWS Mon Feb 08 11:01:47 2010 +0100 +++ b/NEWS Mon Feb 08 11:13:30 2010 +0100 @@ -6,12 +6,63 @@ *** Pure *** -* Code generator: details of internal data cache have no impact on the -user space functionality any longer. +* Code generator: details of internal data cache have no impact on +the user space functionality any longer. *** HOL *** +* more consistent naming of type classes involving orderings (and lattices): + + lower_semilattice ~> semilattice_inf + upper_semilattice ~> semilattice_sup + + dense_linear_order ~> dense_linorder + + pordered_ab_group_add ~> ordered_ab_group_add + pordered_ab_group_add_abs ~> ordered_ab_group_add_abs + pordered_ab_semigroup_add ~> ordered_ab_semigroup_add + pordered_ab_semigroup_add_imp_le ~> ordered_ab_semigroup_add_imp_le + pordered_cancel_ab_semigroup_add ~> ordered_cancel_ab_semigroup_add + pordered_cancel_comm_semiring ~> ordered_cancel_comm_semiring + pordered_cancel_semiring ~> ordered_cancel_semiring + pordered_comm_monoid_add ~> ordered_comm_monoid_add + pordered_comm_ring ~> ordered_comm_ring + pordered_comm_semiring ~> ordered_comm_semiring + pordered_ring ~> ordered_ring + pordered_ring_abs ~> ordered_ring_abs + pordered_semiring ~> ordered_semiring + + lordered_ab_group_add ~> lattice_ab_group_add + lordered_ab_group_add_abs ~> lattice_ab_group_add_abs + lordered_ab_group_add_meet ~> semilattice_inf_ab_group_add + lordered_ab_group_add_join ~> semilattice_sup_ab_group_add + lordered_ring ~> lattice_ring + + ordered_ab_group_add ~> linordered_ab_group_add + ordered_ab_semigroup_add ~> linordered_ab_semigroup_add + ordered_cancel_ab_semigroup_add ~> linordered_cancel_ab_semigroup_add + ordered_comm_semiring_strict ~> linordered_comm_semiring_strict + ordered_field ~> linordered_field + ordered_field_no_lb ~> linordered_field_no_lb + ordered_field_no_ub ~> linordered_field_no_ub + ordered_field_dense_linear_order ~> dense_linordered_field + ordered_idom ~> linordered_idom + ordered_ring ~> linordered_ring + ordered_ring_le_cancel_factor ~> linordered_ring_le_cancel_factor + ordered_ring_less_cancel_factor ~> linordered_ring_less_cancel_factor + ordered_ring_strict ~> linordered_ring_strict + ordered_semidom ~> linordered_semidom + ordered_semiring ~> linordered_semiring + ordered_semiring_1 ~> linordered_semiring_1 + ordered_semiring_1_strict ~> linordered_semiring_1_strict + ordered_semiring_strict ~> linordered_semiring_strict + +INCOMPATIBILITY. + +* Index syntax for structures must be imported explicitly from library +theory Structure_Syntax. INCOMPATIBILITY. + * New theory Algebras contains generic algebraic structures and generic algebraic operations. INCOMPATIBILTY: constants zero, one, plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Algebras.thy --- a/src/HOL/Algebras.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Algebras.thy Mon Feb 08 11:13:30 2010 +0100 @@ -10,15 +10,30 @@ subsection {* Generic algebraic structures *} +text {* + These locales provide basic structures for interpretation into + bigger structures; extensions require careful thinking, otherwise + undesired effects may occur due to interpretation. +*} + +ML {* +structure Ac_Simps = Named_Thms( + val name = "ac_simps" + val description = "associativity and commutativity simplification rules" +) +*} + +setup Ac_Simps.setup + locale semigroup = fixes f :: "'a \ 'a \ 'a" (infixl "*" 70) - assumes assoc: "a * b * c = a * (b * c)" + assumes assoc [ac_simps]: "a * b * c = a * (b * c)" locale abel_semigroup = semigroup + - assumes commute: "a * b = b * a" + assumes commute [ac_simps]: "a * b = b * a" begin -lemma left_commute: +lemma left_commute [ac_simps]: "b * (a * c) = a * (b * c)" proof - have "(b * a) * c = (a * b) * c" @@ -39,25 +54,6 @@ end -locale lattice = inf!: abel_semigroup inf + sup!: abel_semigroup sup - for inf (infixl "\" 70) and sup (infixl "\" 70) + - assumes sup_inf_absorb: "a \ (a \ b) = a" - and inf_sup_absorb: "a \ (a \ b) = a" - -sublocale lattice < inf!: semilattice inf -proof - fix a - have "a \ (a \ (a \ a)) = a" by (fact inf_sup_absorb) - then show "a \ a = a" by (simp add: sup_inf_absorb) -qed - -sublocale lattice < sup!: semilattice sup -proof - fix a - have "a \ (a \ (a \ a)) = a" by (fact sup_inf_absorb) - then show "a \ a = a" by (simp add: inf_sup_absorb) -qed - subsection {* Generic algebraic operations *} @@ -158,9 +154,4 @@ end -syntax - "_index1" :: index ("\<^sub>1") -translations - (index) "\<^sub>1" => (index) "\<^bsub>\\<^esub>" - end \ No newline at end of file diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Archimedean_Field.thy Mon Feb 08 11:13:30 2010 +0100 @@ -12,7 +12,7 @@ text {* Archimedean fields have no infinite elements. *} -class archimedean_field = ordered_field + number_ring + +class archimedean_field = linordered_field + number_ring + assumes ex_le_of_int: "\z. x \ of_int z" lemma ex_less_of_int: diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Code_Numeral.thy Mon Feb 08 11:13:30 2010 +0100 @@ -144,7 +144,7 @@ subsection {* Basic arithmetic *} -instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}" +instantiation code_numeral :: "{minus, linordered_semidom, semiring_div, linorder}" begin definition [simp, code del]: diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Mon Feb 08 11:13:30 2010 +0100 @@ -1431,7 +1431,7 @@ moreover have "0 \ exp t / real (fact (get_even n)) * (real x) ^ (get_even n)" by (auto intro!: mult_nonneg_nonneg divide_nonneg_pos simp add: get_even zero_le_even_power exp_gt_zero) ultimately show ?thesis - using get_odd exp_gt_zero by (auto intro!: pordered_cancel_semiring_class.mult_nonneg_nonneg) + using get_odd exp_gt_zero by (auto intro!: mult_nonneg_nonneg) qed finally have "real (lb_exp_horner prec (get_even n) 1 1 x) \ exp (real x)" . } moreover @@ -1451,7 +1451,7 @@ moreover have "exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n) \ 0" by (auto intro!: mult_nonneg_nonpos divide_nonpos_pos simp add: x_less_zero exp_gt_zero) ultimately have "exp (real x) \ (\j = 0.. \ real (ub_exp_horner prec (get_odd n) 1 1 x)" using bounds(2) by auto finally have "exp (real x) \ real (ub_exp_horner prec (get_odd n) 1 1 x)" . diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Feb 08 11:13:30 2010 +0100 @@ -208,7 +208,7 @@ section {* The classical QE after Langford for dense linear orders *} -context dense_linear_order +context dense_linorder begin lemma interval_empty_iff: @@ -265,7 +265,7 @@ lemmas dlo_simps[noatp] = order_refl less_irrefl not_less not_le exists_neq le_less neq_iff linear less_not_permute -lemma axiom[noatp]: "dense_linear_order (op \) (op <)" by (rule dense_linear_order_axioms) +lemma axiom[noatp]: "dense_linorder (op \) (op <)" by (rule dense_linorder_axioms) lemma atoms[noatp]: shows "TERM (less :: 'a \ _)" and "TERM (less_eq :: 'a \ _)" @@ -409,17 +409,17 @@ end -locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub + +locale constr_dense_linorder = linorder_no_lb + linorder_no_ub + fixes between assumes between_less: "less x y \ less x (between x y) \ less (between x y) y" and between_same: "between x x = x" -sublocale constr_dense_linear_order < dense_linear_order +sublocale constr_dense_linorder < dense_linorder apply unfold_locales using gt_ex lt_ex between_less by (auto, rule_tac x="between x y" in exI, simp) -context constr_dense_linear_order +context constr_dense_linorder begin lemma rinf_U[noatp]: @@ -500,8 +500,8 @@ lemmas npi_thms[noatp] = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P lemmas lin_dense_thms[noatp] = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P -lemma ferrack_axiom[noatp]: "constr_dense_linear_order less_eq less between" - by (rule constr_dense_linear_order_axioms) +lemma ferrack_axiom[noatp]: "constr_dense_linorder less_eq less between" + by (rule constr_dense_linorder_axioms) lemma atoms[noatp]: shows "TERM (less :: 'a \ _)" and "TERM (less_eq :: 'a \ _)" @@ -551,7 +551,7 @@ subsection {* Ferrante and Rackoff algorithm over ordered fields *} -lemma neg_prod_lt:"(c\'a\ordered_field) < 0 \ ((c*x < 0) == (x > 0))" +lemma neg_prod_lt:"(c\'a\linordered_field) < 0 \ ((c*x < 0) == (x > 0))" proof- assume H: "c < 0" have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] algebra_simps) @@ -559,7 +559,7 @@ finally show "(c*x < 0) == (x > 0)" by simp qed -lemma pos_prod_lt:"(c\'a\ordered_field) > 0 \ ((c*x < 0) == (x < 0))" +lemma pos_prod_lt:"(c\'a\linordered_field) > 0 \ ((c*x < 0) == (x < 0))" proof- assume H: "c > 0" hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] algebra_simps) @@ -567,7 +567,7 @@ finally show "(c*x < 0) == (x < 0)" by simp qed -lemma neg_prod_sum_lt: "(c\'a\ordered_field) < 0 \ ((c*x + t< 0) == (x > (- 1/c)*t))" +lemma neg_prod_sum_lt: "(c\'a\linordered_field) < 0 \ ((c*x + t< 0) == (x > (- 1/c)*t))" proof- assume H: "c < 0" have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp) @@ -576,7 +576,7 @@ finally show "(c*x + t < 0) == (x > (- 1/c)*t)" by simp qed -lemma pos_prod_sum_lt:"(c\'a\ordered_field) > 0 \ ((c*x + t < 0) == (x < (- 1/c)*t))" +lemma pos_prod_sum_lt:"(c\'a\linordered_field) > 0 \ ((c*x + t < 0) == (x < (- 1/c)*t))" proof- assume H: "c > 0" have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp) @@ -585,10 +585,10 @@ finally show "(c*x + t < 0) == (x < (- 1/c)*t)" by simp qed -lemma sum_lt:"((x::'a::pordered_ab_group_add) + t < 0) == (x < - t)" +lemma sum_lt:"((x::'a::ordered_ab_group_add) + t < 0) == (x < - t)" using less_diff_eq[where a= x and b=t and c=0] by simp -lemma neg_prod_le:"(c\'a\ordered_field) < 0 \ ((c*x <= 0) == (x >= 0))" +lemma neg_prod_le:"(c\'a\linordered_field) < 0 \ ((c*x <= 0) == (x >= 0))" proof- assume H: "c < 0" have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] algebra_simps) @@ -596,7 +596,7 @@ finally show "(c*x <= 0) == (x >= 0)" by simp qed -lemma pos_prod_le:"(c\'a\ordered_field) > 0 \ ((c*x <= 0) == (x <= 0))" +lemma pos_prod_le:"(c\'a\linordered_field) > 0 \ ((c*x <= 0) == (x <= 0))" proof- assume H: "c > 0" hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] algebra_simps) @@ -604,7 +604,7 @@ finally show "(c*x <= 0) == (x <= 0)" by simp qed -lemma neg_prod_sum_le: "(c\'a\ordered_field) < 0 \ ((c*x + t <= 0) == (x >= (- 1/c)*t))" +lemma neg_prod_sum_le: "(c\'a\linordered_field) < 0 \ ((c*x + t <= 0) == (x >= (- 1/c)*t))" proof- assume H: "c < 0" have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp) @@ -613,7 +613,7 @@ finally show "(c*x + t <= 0) == (x >= (- 1/c)*t)" by simp qed -lemma pos_prod_sum_le:"(c\'a\ordered_field) > 0 \ ((c*x + t <= 0) == (x <= (- 1/c)*t))" +lemma pos_prod_sum_le:"(c\'a\linordered_field) > 0 \ ((c*x + t <= 0) == (x <= (- 1/c)*t))" proof- assume H: "c > 0" have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp) @@ -622,24 +622,24 @@ finally show "(c*x + t <= 0) == (x <= (- 1/c)*t)" by simp qed -lemma sum_le:"((x::'a::pordered_ab_group_add) + t <= 0) == (x <= - t)" +lemma sum_le:"((x::'a::ordered_ab_group_add) + t <= 0) == (x <= - t)" using le_diff_eq[where a= x and b=t and c=0] by simp -lemma nz_prod_eq:"(c\'a\ordered_field) \ 0 \ ((c*x = 0) == (x = 0))" by simp -lemma nz_prod_sum_eq: "(c\'a\ordered_field) \ 0 \ ((c*x + t = 0) == (x = (- 1/c)*t))" +lemma nz_prod_eq:"(c\'a\linordered_field) \ 0 \ ((c*x = 0) == (x = 0))" by simp +lemma nz_prod_sum_eq: "(c\'a\linordered_field) \ 0 \ ((c*x + t = 0) == (x = (- 1/c)*t))" proof- assume H: "c \ 0" have "c*x + t = 0 = (c*x = -t)" by (subst eq_iff_diff_eq_0 [of "c*x" "-t"], simp) also have "\ = (x = -t/c)" by (simp only: nonzero_eq_divide_eq[OF H] algebra_simps) finally show "(c*x + t = 0) == (x = (- 1/c)*t)" by simp qed -lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x = - t)" +lemma sum_eq:"((x::'a::ordered_ab_group_add) + t = 0) == (x = - t)" using eq_diff_eq[where a= x and b=t and c=0] by simp -interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order +interpretation class_dense_linlinordered_field: constr_dense_linorder "op <=" "op <" - "\ x y. 1/2 * ((x::'a::{ordered_field,number_ring}) + y)" + "\ x y. 1/2 * ((x::'a::{linordered_field,number_ring}) + y)" proof (unfold_locales, dlo, dlo, auto) fix x y::'a assume lt: "x < y" from less_half_sum[OF lt] show "x < (x + y) /2" by simp @@ -871,7 +871,7 @@ addsplits [@{thm "abs_split"},@{thm "split_max"}, @{thm "split_min"}] in -Ferrante_Rackoff_Data.funs @{thm "class_ordered_field_dense_linear_order.ferrack_axiom"} +Ferrante_Rackoff_Data.funs @{thm "class_dense_linlinordered_field.ferrack_axiom"} {isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss} end *} diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Decision_Procs/MIR.thy Mon Feb 08 11:13:30 2010 +0100 @@ -54,7 +54,7 @@ by clarsimp -lemma myl: "\ (a::'a::{pordered_ab_group_add}) (b::'a). (a \ b) = (0 \ b - a)" +lemma myl: "\ (a::'a::{ordered_ab_group_add}) (b::'a). (a \ b) = (0 \ b - a)" proof(clarify) fix x y ::"'a" have "(x \ y) = (x - y \ 0)" by (simp only: le_iff_diff_le_0[where a="x" and b="y"]) @@ -63,7 +63,7 @@ finally show "(x \ y) = (0 \ y - x)" . qed -lemma myless: "\ (a::'a::{pordered_ab_group_add}) (b::'a). (a < b) = (0 < b - a)" +lemma myless: "\ (a::'a::{ordered_ab_group_add}) (b::'a). (a < b) = (0 < b - a)" proof(clarify) fix x y ::"'a" have "(x < y) = (x - y < 0)" by (simp only: less_iff_diff_less_0[where a="x" and b="y"]) @@ -72,7 +72,7 @@ finally show "(x < y) = (0 < y - x)" . qed -lemma myeq: "\ (a::'a::{pordered_ab_group_add}) (b::'a). (a = b) = (0 = b - a)" +lemma myeq: "\ (a::'a::{ordered_ab_group_add}) (b::'a). (a = b) = (0 = b - a)" by auto (* Maybe should be added to the library \ *) diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Feb 08 11:13:30 2010 +0100 @@ -447,7 +447,7 @@ by (induct p rule: fmsize.induct) simp_all (* Semantics of formulae (fm) *) -consts Ifm ::"'a::{division_by_zero,ordered_field} list \ 'a list \ fm \ bool" +consts Ifm ::"'a::{division_by_zero,linordered_field} list \ 'a list \ fm \ bool" primrec "Ifm vs bs T = True" "Ifm vs bs F = False" @@ -1833,16 +1833,16 @@ ultimately show ?case by blast qed (auto simp add: nth_pos2 tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"] bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"]) -lemma one_plus_one_pos[simp]: "(1::'a::{ordered_field}) + 1 > 0" +lemma one_plus_one_pos[simp]: "(1::'a::{linordered_field}) + 1 > 0" proof- have op: "(1::'a) > 0" by simp from add_pos_pos[OF op op] show ?thesis . qed -lemma one_plus_one_nonzero[simp]: "(1::'a::{ordered_field}) + 1 \ 0" +lemma one_plus_one_nonzero[simp]: "(1::'a::{linordered_field}) + 1 \ 0" using one_plus_one_pos[where ?'a = 'a] by (simp add: less_le) -lemma half_sum_eq: "(u + u) / (1+1) = (u::'a::{ordered_field})" +lemma half_sum_eq: "(u + u) / (1+1) = (u::'a::{linordered_field})" proof- have "(u + u) = (1 + 1) * u" by (simp add: ring_simps) hence "(u + u) / (1+1) = (1 + 1)*u / (1 + 1)" by simp @@ -3172,54 +3172,54 @@ *} "Parametric QE for linear Arithmetic over fields, Version 2" -lemma "\(x::'a::{division_by_zero,ordered_field,number_ring}). y \ -1 \ (y + 1)*x < 0" - apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "y::'a::{division_by_zero,ordered_field,number_ring}") +lemma "\(x::'a::{division_by_zero,linordered_field,number_ring}). y \ -1 \ (y + 1)*x < 0" + apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "y::'a::{division_by_zero,linordered_field,number_ring}") apply (simp add: ring_simps) apply (rule spec[where x=y]) - apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "z::'a::{division_by_zero,ordered_field,number_ring}") + apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "z::'a::{division_by_zero,linordered_field,number_ring}") by simp text{* Collins/Jones Problem *} (* -lemma "\(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" +lemma "\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" proof- - have "(\(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \ (\(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \ r < 1 \ 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \ 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \ ?rhs") + have "(\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \ (\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \ 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \ ?rhs") by (simp add: ring_simps) have "?rhs" - apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "a::'a::{division_by_zero,ordered_field,number_ring}" "b::'a::{division_by_zero,ordered_field,number_ring}") + apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "a::'a::{division_by_zero,linordered_field,number_ring}" "b::'a::{division_by_zero,linordered_field,number_ring}") apply (simp add: ring_simps) oops *) (* -lemma "ALL (x::'a::{division_by_zero,ordered_field,number_ring}) y. (1 - t)*x \ (1+t)*y \ (1 - t)*y \ (1+t)*x --> 0 \ y" -apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "t::'a::{division_by_zero,ordered_field,number_ring}") +lemma "ALL (x::'a::{division_by_zero,linordered_field,number_ring}) y. (1 - t)*x \ (1+t)*y \ (1 - t)*y \ (1+t)*x --> 0 \ y" +apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "t::'a::{division_by_zero,linordered_field,number_ring}") oops *) -lemma "\(x::'a::{division_by_zero,ordered_field,number_ring}). y \ -1 \ (y + 1)*x < 0" - apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "y::'a::{division_by_zero,ordered_field,number_ring}") +lemma "\(x::'a::{division_by_zero,linordered_field,number_ring}). y \ -1 \ (y + 1)*x < 0" + apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "y::'a::{division_by_zero,linordered_field,number_ring}") apply (simp add: ring_simps) apply (rule spec[where x=y]) - apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "z::'a::{division_by_zero,ordered_field,number_ring}") + apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "z::'a::{division_by_zero,linordered_field,number_ring}") by simp text{* Collins/Jones Problem *} (* -lemma "\(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" +lemma "\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" proof- - have "(\(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \ (\(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \ r < 1 \ 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \ 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \ ?rhs") + have "(\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \ (\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \ 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \ ?rhs") by (simp add: ring_simps) have "?rhs" - apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "a::'a::{division_by_zero,ordered_field,number_ring}" "b::'a::{division_by_zero,ordered_field,number_ring}") + apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "a::'a::{division_by_zero,linordered_field,number_ring}" "b::'a::{division_by_zero,linordered_field,number_ring}") apply simp oops *) (* -lemma "ALL (x::'a::{division_by_zero,ordered_field,number_ring}) y. (1 - t)*x \ (1+t)*y \ (1 - t)*y \ (1+t)*x --> 0 \ y" -apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "t::'a::{division_by_zero,ordered_field,number_ring}") +lemma "ALL (x::'a::{division_by_zero,linordered_field,number_ring}) y. (1 - t)*x \ (1+t)*y \ (1 - t)*y \ (1+t)*x --> 0 \ y" +apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "t::'a::{division_by_zero,linordered_field,number_ring}") apply (simp add: field_simps linorder_neq_iff[symmetric]) apply ferrack oops diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Decision_Procs/Polynomial_List.thy --- a/src/HOL/Decision_Procs/Polynomial_List.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy Mon Feb 08 11:13:30 2010 +0100 @@ -772,7 +772,7 @@ text{*bound for polynomial.*} -lemma poly_mono: "abs(x) \ k ==> abs(poly p (x::'a::{ordered_idom})) \ poly (map abs p) k" +lemma poly_mono: "abs(x) \ k ==> abs(poly p (x::'a::{linordered_idom})) \ poly (map abs p) k" apply (induct "p", auto) apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans) apply (rule abs_triangle_ineq) diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Mon Feb 08 11:13:30 2010 +0100 @@ -7,147 +7,147 @@ begin lemma - "\(y::'a::{ordered_field,number_ring, division_by_zero}) <2. x + 3* y < 0 \ x - y >0" + "\(y::'a::{linordered_field,number_ring, division_by_zero}) <2. x + 3* y < 0 \ x - y >0" by ferrack -lemma "~ (ALL x (y::'a::{ordered_field,number_ring, division_by_zero}). x < y --> 10*x < 11*y)" +lemma "~ (ALL x (y::'a::{linordered_field,number_ring, division_by_zero}). x < y --> 10*x < 11*y)" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. x ~= y --> x < y" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y. x ~= y --> x < y" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX (y::'a::{ordered_field,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX (y::'a::{linordered_field,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) < 0. (EX (y::'a::{ordered_field,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) < 0. (EX (y::'a::{linordered_field,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)" by ferrack -lemma "EX x. (ALL (y::'a::{ordered_field,number_ring, division_by_zero}). y < 2 --> 2*(y - x) \ 0 )" +lemma "EX x. (ALL (y::'a::{linordered_field,number_ring, division_by_zero}). y < 2 --> 2*(y - x) \ 0 )" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \ abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \ abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \ 0 \ (EX z. 5*x - 3*abs y <= 7*z))" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \ 0 \ (EX z. 5*x - 3*abs y <= 7*z))" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)" by ferrack -lemma "~(ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))" +lemma "~(ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)" by ferrack -lemma "EX z. (ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))" +lemma "EX z. (ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))" by ferrack -lemma "EX z. (ALL (x::'a::{ordered_field,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))" +lemma "EX z. (ALL (x::'a::{linordered_field,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))" by ferrack -lemma "EX y. (ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))" +lemma "EX y. (ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y). +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y). (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (ALL y. (EX z > y. +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}). (ALL y. (EX z > y. (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))" by ferrack -lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" +lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))" by ferrack -lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))" +lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))" by ferrack end diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Fact.thy --- a/src/HOL/Fact.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Fact.thy Mon Feb 08 11:13:30 2010 +0100 @@ -266,15 +266,15 @@ lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \ (0::'a::semiring_char_0)" by auto -lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto +lemma of_nat_fact_gt_zero [simp]: "(0::'a::{linordered_semidom}) < of_nat(fact n)" by auto -lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \ of_nat(fact n)" +lemma of_nat_fact_ge_zero [simp]: "(0::'a::linordered_semidom) \ of_nat(fact n)" by simp -lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))" +lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::linordered_field) < inverse (of_nat (fact n))" by (auto simp add: positive_imp_inverse_positive) -lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \ inverse (of_nat (fact n))" +lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_field) \ inverse (of_nat (fact n))" by (auto intro: order_less_imp_le) end diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Finite_Set.thy Mon Feb 08 11:13:30 2010 +0100 @@ -830,7 +830,7 @@ end -context lower_semilattice +context semilattice_inf begin lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf" @@ -857,20 +857,20 @@ end -context upper_semilattice +context semilattice_sup begin lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup" -by (rule lower_semilattice.ab_semigroup_idem_mult_inf)(rule dual_semilattice) +by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice) lemma fold_sup_insert[simp]: "finite A \ fold sup b (insert a A) = sup a (fold sup b A)" -by(rule lower_semilattice.fold_inf_insert)(rule dual_semilattice) +by(rule semilattice_inf.fold_inf_insert)(rule dual_semilattice) lemma fold_sup_le_sup: "finite A \ ALL a:A. a \ b \ fold sup c A \ sup b c" -by(rule lower_semilattice.inf_le_fold_inf)(rule dual_semilattice) +by(rule semilattice_inf.inf_le_fold_inf)(rule dual_semilattice) lemma sup_le_fold_sup: "finite A \ a \ A \ sup a b \ fold sup b A" -by(rule lower_semilattice.fold_inf_le_inf)(rule dual_semilattice) +by(rule semilattice_inf.fold_inf_le_inf)(rule dual_semilattice) end @@ -1486,7 +1486,7 @@ qed lemma setsum_mono: - assumes le: "\i. i\K \ f (i::'a) \ ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))" + assumes le: "\i. i\K \ f (i::'a) \ ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))" shows "(\i\K. f i) \ (\i\K. g i)" proof (cases "finite K") case True @@ -1505,7 +1505,7 @@ qed lemma setsum_strict_mono: - fixes f :: "'a \ 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}" + fixes f :: "'a \ 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}" assumes "finite A" "A \ {}" and "!!x. x:A \ f x < g x" shows "setsum f A < setsum g A" @@ -1534,7 +1534,7 @@ qed lemma setsum_nonneg: - assumes nn: "\x\A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \ f x" + assumes nn: "\x\A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \ f x" shows "0 \ setsum f A" proof (cases "finite A") case True thus ?thesis using nn @@ -1550,7 +1550,7 @@ qed lemma setsum_nonpos: - assumes np: "\x\A. f x \ (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})" + assumes np: "\x\A. f x \ (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})" shows "setsum f A \ 0" proof (cases "finite A") case True thus ?thesis using np @@ -1566,7 +1566,7 @@ qed lemma setsum_mono2: -fixes f :: "'a \ 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}" +fixes f :: "'a \ 'b :: {ordered_ab_semigroup_add_imp_le,comm_monoid_add}" assumes fin: "finite B" and sub: "A \ B" and nn: "\b. b \ B-A \ 0 \ f b" shows "setsum f A \ setsum f B" proof - @@ -1580,7 +1580,7 @@ lemma setsum_mono3: "finite B ==> A <= B ==> ALL x: B - A. - 0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==> + 0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==> setsum f A <= setsum f B" apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)") apply (erule ssubst) @@ -1640,7 +1640,7 @@ qed lemma setsum_abs[iff]: - fixes f :: "'a => ('b::pordered_ab_group_add_abs)" + fixes f :: "'a => ('b::ordered_ab_group_add_abs)" shows "abs (setsum f A) \ setsum (%i. abs(f i)) A" proof (cases "finite A") case True @@ -1656,7 +1656,7 @@ qed lemma setsum_abs_ge_zero[iff]: - fixes f :: "'a => ('b::pordered_ab_group_add_abs)" + fixes f :: "'a => ('b::ordered_ab_group_add_abs)" shows "0 \ setsum (%i. abs(f i)) A" proof (cases "finite A") case True @@ -1671,7 +1671,7 @@ qed lemma abs_setsum_abs[simp]: - fixes f :: "'a => ('b::pordered_ab_group_add_abs)" + fixes f :: "'a => ('b::ordered_ab_group_add_abs)" shows "abs (\a\A. abs(f a)) = (\a\A. abs(f a))" proof (cases "finite A") case True @@ -1946,10 +1946,10 @@ done lemma setprod_nonneg [rule_format]: - "(ALL x: A. (0::'a::ordered_semidom) \ f x) --> 0 \ setprod f A" + "(ALL x: A. (0::'a::linordered_semidom) \ f x) --> 0 \ setprod f A" by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg) -lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_semidom) < f x) +lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x) --> 0 < setprod f A" by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos) @@ -2289,7 +2289,7 @@ lemma setsum_bounded: - assumes le: "\i. i\A \ f i \ (K::'a::{semiring_1, pordered_ab_semigroup_add})" + assumes le: "\i. i\A \ f i \ (K::'a::{semiring_1, ordered_ab_semigroup_add})" shows "setsum f A \ of_nat(card A) * K" proof (cases "finite A") case True @@ -2791,7 +2791,7 @@ over (non-empty) sets by means of @{text fold1}. *} -context lower_semilattice +context semilattice_inf begin lemma below_fold1_iff: @@ -2859,7 +2859,7 @@ apply(erule exE) apply(rule order_trans) apply(erule (1) fold1_belowI) -apply(erule (1) lower_semilattice.fold1_belowI [OF dual_semilattice]) +apply(erule (1) semilattice_inf.fold1_belowI [OF dual_semilattice]) done lemma sup_Inf_absorb [simp]: @@ -2871,7 +2871,7 @@ lemma inf_Sup_absorb [simp]: "finite A \ a \ A \ inf a (\\<^bsub>fin\<^esub>A) = a" by (simp add: Sup_fin_def inf_absorb1 - lower_semilattice.fold1_belowI [OF dual_semilattice]) + semilattice_inf.fold1_belowI [OF dual_semilattice]) end @@ -2991,7 +2991,7 @@ proof qed (auto simp add: max_def) lemma max_lattice: - "lower_semilattice (op \) (op >) max" + "semilattice_inf (op \) (op >) max" by (fact min_max.dual_semilattice) lemma dual_max: @@ -3158,7 +3158,7 @@ assumes "finite A" and "x \ A" shows "x \ Max A" proof - - interpret lower_semilattice "op \" "op >" max + interpret semilattice_inf "op \" "op >" max by (rule max_lattice) from assms show ?thesis by (simp add: Max_def fold1_belowI) qed @@ -3172,7 +3172,7 @@ assumes "finite A" and "A \ {}" shows "Max A \ x \ (\a\A. a \ x)" proof - - interpret lower_semilattice "op \" "op >" max + interpret semilattice_inf "op \" "op >" max by (rule max_lattice) from assms show ?thesis by (simp add: Max_def below_fold1_iff) qed @@ -3293,7 +3293,7 @@ end -context ordered_ab_semigroup_add +context linordered_ab_semigroup_add begin lemma add_Min_commute: @@ -3347,12 +3347,12 @@ proof qed auto -lemma (in lower_semilattice) fun_left_comm_idem_inf: +lemma (in semilattice_inf) fun_left_comm_idem_inf: "fun_left_comm_idem inf" proof qed (auto simp add: inf_left_commute) -lemma (in upper_semilattice) fun_left_comm_idem_sup: +lemma (in semilattice_sup) fun_left_comm_idem_sup: "fun_left_comm_idem sup" proof qed (auto simp add: sup_left_commute) diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/GCD.thy --- a/src/HOL/GCD.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/GCD.thy Mon Feb 08 11:13:30 2010 +0100 @@ -1445,12 +1445,12 @@ subsubsection {* The complete divisibility lattice *} -interpretation gcd_semilattice_nat: lower_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd +interpretation gcd_semilattice_nat: semilattice_inf "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd proof case goal3 thus ?case by(metis gcd_unique_nat) qed auto -interpretation lcm_semilattice_nat: upper_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm +interpretation lcm_semilattice_nat: semilattice_sup "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm proof case goal3 thus ?case by(metis lcm_unique_nat) qed auto diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Import/HOL/real.imp --- a/src/HOL/Import/HOL/real.imp Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Import/HOL/real.imp Mon Feb 08 11:13:30 2010 +0100 @@ -147,7 +147,7 @@ "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" "REAL_LT_SUB_RADD" > "OrderedGroup.compare_rls_6" "REAL_LT_SUB_LADD" > "OrderedGroup.compare_rls_7" - "REAL_LT_RMUL_IMP" > "Ring_and_Field.ordered_semiring_strict_class.mult_strict_right_mono" + "REAL_LT_RMUL_IMP" > "Ring_and_Field.mult_strict_right_mono" "REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0" "REAL_LT_RMUL" > "RealDef.real_mult_less_iff1" "REAL_LT_REFL" > "Orderings.order_less_irrefl" @@ -161,7 +161,7 @@ "REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE" "REAL_LT_MUL2" > "Ring_and_Field.mult_strict_mono'" "REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos" - "REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict_class.mult_strict_mono" + "REAL_LT_LMUL_IMP" > "Ring_and_Field.linordered_comm_semiring_strict_class.mult_strict_mono" "REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0" "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL" "REAL_LT_LE" > "Orderings.order_class.order_less_le" @@ -188,7 +188,7 @@ "REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1" "REAL_LT_ADD" > "OrderedGroup.add_pos_pos" "REAL_LT_1" > "HOL4Real.real.REAL_LT_1" - "REAL_LT_01" > "Ring_and_Field.ordered_semidom_class.zero_less_one" + "REAL_LT_01" > "Ring_and_Field.zero_less_one" "REAL_LTE_TRANS" > "Set.basic_trans_rules_24" "REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL" "REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM" @@ -204,7 +204,7 @@ "REAL_LE_SUB_LADD" > "OrderedGroup.compare_rls_9" "REAL_LE_SQUARE" > "Ring_and_Field.zero_le_square" "REAL_LE_RNEG" > "OrderedGroup.le_eq_neg" - "REAL_LE_RMUL_IMP" > "Ring_and_Field.pordered_semiring_class.mult_right_mono" + "REAL_LE_RMUL_IMP" > "Ring_and_Field.mult_right_mono" "REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1" "REAL_LE_REFL" > "Finite_Set.max.f_below.below_refl" "REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq" @@ -220,11 +220,11 @@ "REAL_LE_MUL" > "Ring_and_Field.mult_nonneg_nonneg" "REAL_LE_LT" > "Orderings.order_le_less" "REAL_LE_LNEG" > "RealDef.real_0_le_add_iff" - "REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring_class.mult_mono" + "REAL_LE_LMUL_IMP" > "Ring_and_Field.mult_mono" "REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2" "REAL_LE_LDIV_EQ" > "Ring_and_Field.pos_divide_le_eq" "REAL_LE_LDIV" > "Ring_and_Field.mult_imp_div_pos_le" - "REAL_LE_LADD_IMP" > "OrderedGroup.pordered_ab_semigroup_add_class.add_left_mono" + "REAL_LE_LADD_IMP" > "OrderedGroup.add_left_mono" "REAL_LE_LADD" > "OrderedGroup.add_le_cancel_left" "REAL_LE_INV_EQ" > "Ring_and_Field.inverse_nonnegative_iff_nonnegative" "REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Int.thy --- a/src/HOL/Int.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Int.thy Mon Feb 08 11:13:30 2010 +0100 @@ -208,7 +208,7 @@ end -instance int :: pordered_cancel_ab_semigroup_add +instance int :: ordered_cancel_ab_semigroup_add proof fix i j k :: int show "i \ j \ k + i \ k + j" @@ -245,7 +245,7 @@ done text{*The integers form an ordered integral domain*} -instance int :: ordered_idom +instance int :: linordered_idom proof fix i j k :: int show "i < j \ 0 < k \ k * i < k * j" @@ -256,7 +256,7 @@ by (simp only: zsgn_def) qed -instance int :: lordered_ring +instance int :: lattice_ring proof fix k :: int show "abs k = sup k (- k)" @@ -331,7 +331,7 @@ end -context ordered_idom +context linordered_idom begin lemma of_int_le_iff [simp]: @@ -370,8 +370,8 @@ end -text{*Every @{text ordered_idom} has characteristic zero.*} -subclass (in ordered_idom) ring_char_0 by intro_locales +text{*Every @{text linordered_idom} has characteristic zero.*} +subclass (in linordered_idom) ring_char_0 by intro_locales lemma of_int_eq_id [simp]: "of_int = id" proof @@ -529,7 +529,7 @@ in theory @{text Ring_and_Field}. But is it really better than just rewriting with @{text abs_if}?*} lemma abs_split [arith_split,noatp]: - "P(abs(a::'a::ordered_idom)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" + "P(abs(a::'a::linordered_idom)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) lemma negD: "(x \ int) < 0 \ \n. x = - (of_nat (Suc n))" @@ -804,7 +804,7 @@ text {* Preliminaries *} lemma even_less_0_iff: - "a + a < 0 \ a < (0::'a::ordered_idom)" + "a + a < 0 \ a < (0::'a::linordered_idom)" proof - have "a + a < 0 \ (1+1)*a < 0" by (simp add: left_distrib) also have "(1+1)*a < 0 \ a < 0" @@ -1147,7 +1147,7 @@ subsubsection {* The Less-Than Relation *} lemma double_less_0_iff: - "(a + a < 0) = (a < (0::'a::ordered_idom))" + "(a + a < 0) = (a < (0::'a::linordered_idom))" proof - have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib) also have "... = (a < 0)" @@ -1180,7 +1180,7 @@ text {* Absolute value (@{term abs}) *} lemma abs_number_of: - "abs(number_of x::'a::{ordered_idom,number_ring}) = + "abs(number_of x::'a::{linordered_idom,number_ring}) = (if number_of x < (0::'a) then -number_of x else number_of x)" by (simp add: abs_if) @@ -1214,11 +1214,11 @@ text {* Simplification of relational operations *} lemma less_number_of [simp]: - "(number_of x::'a::{ordered_idom,number_ring}) < number_of y \ x < y" + "(number_of x::'a::{linordered_idom,number_ring}) < number_of y \ x < y" unfolding number_of_eq by (rule of_int_less_iff) lemma le_number_of [simp]: - "(number_of x::'a::{ordered_idom,number_ring}) \ number_of y \ x \ y" + "(number_of x::'a::{linordered_idom,number_ring}) \ number_of y \ x \ y" unfolding number_of_eq by (rule of_int_le_iff) lemma eq_number_of [simp]: @@ -1362,7 +1362,7 @@ lemma Ints_odd_less_0: assumes in_Ints: "a \ Ints" - shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))" + shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))" proof - from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . then obtain z where a: "a = of_int z" .. @@ -1519,11 +1519,11 @@ finally show ?thesis . qed -lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})" +lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{linordered_idom,number_ring})" by (simp add: abs_if) lemma abs_power_minus_one [simp]: - "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring})" + "abs(-1 ^ n) = (1::'a::{linordered_idom,number_ring})" by (simp add: power_abs) lemma of_int_number_of_eq [simp]: @@ -1906,12 +1906,12 @@ text{*To Simplify Inequalities Where One Side is the Constant 1*} lemma less_minus_iff_1 [simp,noatp]: - fixes b::"'b::{ordered_idom,number_ring}" + fixes b::"'b::{linordered_idom,number_ring}" shows "(1 < - b) = (b < -1)" by auto lemma le_minus_iff_1 [simp,noatp]: - fixes b::"'b::{ordered_idom,number_ring}" + fixes b::"'b::{linordered_idom,number_ring}" shows "(1 \ - b) = (b \ -1)" by auto @@ -1921,12 +1921,12 @@ by (subst equation_minus_iff, auto) lemma minus_less_iff_1 [simp,noatp]: - fixes a::"'b::{ordered_idom,number_ring}" + fixes a::"'b::{linordered_idom,number_ring}" shows "(- a < 1) = (-1 < a)" by auto lemma minus_le_iff_1 [simp,noatp]: - fixes a::"'b::{ordered_idom,number_ring}" + fixes a::"'b::{linordered_idom,number_ring}" shows "(- a \ 1) = (-1 \ a)" by auto @@ -1990,7 +1990,7 @@ by (simp add: divide_inverse inverse_minus_eq) lemma half_gt_zero_iff: - "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))" + "(0 < r/2) = (0 < (r::'a::{linordered_field,division_by_zero,number_ring}))" by auto lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard] diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/IsaMakefile Mon Feb 08 11:13:30 2010 +0100 @@ -394,7 +394,7 @@ Library/Library/document/root.tex Library/Library/document/root.bib \ Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \ Library/Product_ord.thy Library/Char_nat.thy \ - Library/Char_ord.thy Library/Option_ord.thy \ + Library/Structure_Syntax.thy \ Library/Sublist_Order.thy Library/List_lexord.thy \ Library/Coinductive_List.thy Library/AssocList.thy \ Library/Formal_Power_Series.thy Library/Binomial.thy \ diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Lattices.thy Mon Feb 08 11:13:30 2010 +0100 @@ -16,13 +16,13 @@ top ("\") and bot ("\") -class lower_semilattice = order + +class semilattice_inf = order + fixes inf :: "'a \ 'a \ 'a" (infixl "\" 70) assumes inf_le1 [simp]: "x \ y \ x" and inf_le2 [simp]: "x \ y \ y" and inf_greatest: "x \ y \ x \ z \ x \ y \ z" -class upper_semilattice = order + +class semilattice_sup = order + fixes sup :: "'a \ 'a \ 'a" (infixl "\" 65) assumes sup_ge1 [simp]: "x \ x \ y" and sup_ge2 [simp]: "y \ x \ y" @@ -32,18 +32,18 @@ text {* Dual lattice *} lemma dual_semilattice: - "lower_semilattice (op \) (op >) sup" -by (rule lower_semilattice.intro, rule dual_order) + "semilattice_inf (op \) (op >) sup" +by (rule semilattice_inf.intro, rule dual_order) (unfold_locales, simp_all add: sup_least) end -class lattice = lower_semilattice + upper_semilattice +class lattice = semilattice_inf + semilattice_sup subsubsection {* Intro and elim rules*} -context lower_semilattice +context semilattice_inf begin lemma le_infI1: @@ -69,13 +69,13 @@ by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) lemma mono_inf: - fixes f :: "'a \ 'b\lower_semilattice" + fixes f :: "'a \ 'b\semilattice_inf" shows "mono f \ f (A \ B) \ f A \ f B" by (auto simp add: mono_def intro: Lattices.inf_greatest) end -context upper_semilattice +context semilattice_sup begin lemma le_supI1: @@ -103,7 +103,7 @@ by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) lemma mono_sup: - fixes f :: "'a \ 'b\upper_semilattice" + fixes f :: "'a \ 'b\semilattice_sup" shows "mono f \ f A \ f B \ f (A \ B)" by (auto simp add: mono_def intro: Lattices.sup_least) @@ -112,7 +112,7 @@ subsubsection {* Equational laws *} -sublocale lower_semilattice < inf!: semilattice inf +sublocale semilattice_inf < inf!: semilattice inf proof fix a b c show "(a \ b) \ c = a \ (b \ c)" @@ -123,7 +123,7 @@ by (rule antisym) auto qed -context lower_semilattice +context semilattice_inf begin lemma inf_assoc: "(x \ y) \ z = x \ (y \ z)" @@ -151,7 +151,7 @@ end -sublocale upper_semilattice < sup!: semilattice sup +sublocale semilattice_sup < sup!: semilattice sup proof fix a b c show "(a \ b) \ c = a \ (b \ c)" @@ -162,7 +162,7 @@ by (rule antisym) auto qed -context upper_semilattice +context semilattice_sup begin lemma sup_assoc: "(x \ y) \ z = x \ (y \ z)" @@ -195,7 +195,7 @@ lemma dual_lattice: "lattice (op \) (op >) sup inf" - by (rule lattice.intro, rule dual_semilattice, rule upper_semilattice.intro, rule dual_order) + by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order) (unfold_locales, auto) lemma inf_sup_absorb: "x \ (x \ y) = x" @@ -246,7 +246,7 @@ subsubsection {* Strict order *} -context lower_semilattice +context semilattice_inf begin lemma less_infI1: @@ -259,13 +259,13 @@ end -context upper_semilattice +context semilattice_sup begin lemma less_supI1: "x \ a \ x \ a \ b" proof - - interpret dual: lower_semilattice "op \" "op >" sup + interpret dual: semilattice_inf "op \" "op >" sup by (fact dual_semilattice) assume "x \ a" then show "x \ a \ b" @@ -275,7 +275,7 @@ lemma less_supI2: "x \ b \ x \ a \ b" proof - - interpret dual: lower_semilattice "op \" "op >" sup + interpret dual: semilattice_inf "op \" "op >" sup by (fact dual_semilattice) assume "x \ b" then show "x \ a \ b" @@ -492,7 +492,7 @@ subsection {* Uniqueness of inf and sup *} -lemma (in lower_semilattice) inf_unique: +lemma (in semilattice_inf) inf_unique: fixes f (infixl "\" 70) assumes le1: "\x y. x \ y \ x" and le2: "\x y. x \ y \ y" and greatest: "\x y z. x \ y \ x \ z \ x \ y \ z" @@ -504,7 +504,7 @@ show "x \ y \ x \ y" by (rule leI) simp_all qed -lemma (in upper_semilattice) sup_unique: +lemma (in semilattice_sup) sup_unique: fixes f (infixl "\" 70) assumes ge1 [simp]: "\x y. x \ x \ y" and ge2: "\x y. y \ x \ y" and least: "\x y z. y \ x \ z \ x \ y \ z \ x" @@ -527,10 +527,10 @@ by (auto simp add: min_def max_def) qed (auto simp add: min_def max_def not_le less_imp_le) -lemma inf_min: "inf = (min \ 'a\{lower_semilattice, linorder} \ 'a \ 'a)" +lemma inf_min: "inf = (min \ 'a\{semilattice_inf, linorder} \ 'a \ 'a)" by (rule ext)+ (auto intro: antisym) -lemma sup_max: "sup = (max \ 'a\{upper_semilattice, linorder} \ 'a \ 'a)" +lemma sup_max: "sup = (max \ 'a\{semilattice_sup, linorder} \ 'a \ 'a)" by (rule ext)+ (auto intro: antisym) lemmas le_maxI1 = min_max.sup_ge1 diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Library/Abstract_Rat.thy --- a/src/HOL/Library/Abstract_Rat.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Library/Abstract_Rat.thy Mon Feb 08 11:13:30 2010 +0100 @@ -332,7 +332,7 @@ lemma Ndiv[simp]: "INum (x \
\<^sub>N y) = INum x / (INum y ::'a :: {ring_char_0, division_by_zero,field})" by (simp add: Ndiv_def) lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field})< 0) = 0>\<^sub>N x " + shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field})< 0) = 0>\<^sub>N x " proof- have " \ a b. x = (a,b)" by simp then obtain a b where x[simp]:"x = (a,b)" by blast @@ -345,7 +345,7 @@ qed lemma Nle0_iff[simp]:assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field}) \ 0) = 0\\<^sub>N x" + shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) \ 0) = 0\\<^sub>N x" proof- have " \ a b. x = (a,b)" by simp then obtain a b where x[simp]:"x = (a,b)" by blast @@ -357,7 +357,7 @@ ultimately show ?thesis by blast qed -lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field})> 0) = 0<\<^sub>N x" +lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field})> 0) = 0<\<^sub>N x" proof- have " \ a b. x = (a,b)" by simp then obtain a b where x[simp]:"x = (a,b)" by blast @@ -369,7 +369,7 @@ ultimately show ?thesis by blast qed lemma Nge0_iff[simp]:assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field}) \ 0) = 0\\<^sub>N x" + shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) \ 0) = 0\\<^sub>N x" proof- have " \ a b. x = (a,b)" by simp then obtain a b where x[simp]:"x = (a,b)" by blast @@ -382,7 +382,7 @@ qed lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" - shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field}) < INum y) = (x <\<^sub>N y)" + shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) < INum y) = (x <\<^sub>N y)" proof- let ?z = "0::'a" have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp @@ -391,7 +391,7 @@ qed lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" - shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field})\ INum y) = (x \\<^sub>N y)" + shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field})\ INum y) = (x \\<^sub>N y)" proof- have "((INum x ::'a) \ INum y) = (INum (x -\<^sub>N y) \ (0::'a))" using nx ny by simp also have "\ = (0\\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Library/BigO.thy --- a/src/HOL/Library/BigO.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Library/BigO.thy Mon Feb 08 11:13:30 2010 +0100 @@ -38,11 +38,11 @@ subsection {* Definitions *} definition - bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set" ("(1O'(_'))") where + bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where "O(f::('a => 'b)) = {h. EX c. ALL x. abs (h x) <= c * abs (f x)}" -lemma bigo_pos_const: "(EX (c::'a::ordered_idom). +lemma bigo_pos_const: "(EX (c::'a::linordered_idom). ALL x. (abs (h x)) <= (c * (abs (f x)))) = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" apply auto @@ -352,7 +352,7 @@ done lemma bigo_mult5: "ALL x. f x ~= 0 ==> - O(f * g) <= (f::'a => ('b::ordered_field)) *o O(g)" + O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)" proof - assume "ALL x. f x ~= 0" show "O(f * g) <= f *o O(g)" @@ -381,14 +381,14 @@ qed lemma bigo_mult6: "ALL x. f x ~= 0 ==> - O(f * g) = (f::'a => ('b::ordered_field)) *o O(g)" + O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)" apply (rule equalityI) apply (erule bigo_mult5) apply (rule bigo_mult2) done lemma bigo_mult7: "ALL x. f x ~= 0 ==> - O(f * g) <= O(f::'a => ('b::ordered_field)) \ O(g)" + O(f * g) <= O(f::'a => ('b::linordered_field)) \ O(g)" apply (subst bigo_mult6) apply assumption apply (rule set_times_mono3) @@ -396,7 +396,7 @@ done lemma bigo_mult8: "ALL x. f x ~= 0 ==> - O(f * g) = O(f::'a => ('b::ordered_field)) \ O(g)" + O(f * g) = O(f::'a => ('b::linordered_field)) \ O(g)" apply (rule equalityI) apply (erule bigo_mult7) apply (rule bigo_mult) @@ -481,16 +481,16 @@ apply (rule bigo_const1) done -lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)" +lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)" apply (simp add: bigo_def) apply (rule_tac x = "abs(inverse c)" in exI) apply (simp add: abs_mult [symmetric]) done -lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)" +lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)" by (rule bigo_elt_subset, rule bigo_const3, assumption) -lemma bigo_const [simp]: "(c::'a::ordered_field) ~= 0 ==> +lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==> O(%x. c) = O(%x. 1)" by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption) @@ -503,21 +503,21 @@ lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)" by (rule bigo_elt_subset, rule bigo_const_mult1) -lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)" +lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)" apply (simp add: bigo_def) apply (rule_tac x = "abs(inverse c)" in exI) apply (simp add: abs_mult [symmetric] mult_assoc [symmetric]) done -lemma bigo_const_mult4: "(c::'a::ordered_field) ~= 0 ==> +lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==> O(f) <= O(%x. c * f x)" by (rule bigo_elt_subset, rule bigo_const_mult3, assumption) -lemma bigo_const_mult [simp]: "(c::'a::ordered_field) ~= 0 ==> +lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==> O(%x. c * f x) = O(f)" by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4) -lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==> +lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==> (%x. c) *o O(f) = O(f)" apply (auto del: subsetI) apply (rule order_trans) @@ -688,7 +688,7 @@ apply assumption+ done -lemma bigo_useful_const_mult: "(c::'a::ordered_field) ~= 0 ==> +lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==> (%x. c) * f =o O(h) ==> f =o O(h)" apply (rule subsetD) apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)") @@ -733,7 +733,7 @@ subsection {* Less than or equal to *} definition - lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)" + lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "'b::ordered_field) ==> +lemma bigo_lesso4: "f 'b::linordered_field) ==> g =o h +o O(k) ==> f y" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Library/Library.thy Mon Feb 08 11:13:30 2010 +0100 @@ -50,6 +50,7 @@ RBT SML_Quickcheck State_Monad + Structure_Syntax Sum_Of_Squares Transitive_Closure_Table Univ_Poly diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Library/Multiset.thy Mon Feb 08 11:13:30 2010 +0100 @@ -415,11 +415,11 @@ mset_le_trans simp: mset_less_def) interpretation mset_order_cancel_semigroup: - pordered_cancel_ab_semigroup_add "op +" "op \#" "op <#" + ordered_cancel_ab_semigroup_add "op +" "op \#" "op <#" proof qed (erule mset_le_mono_add [OF mset_le_refl]) interpretation mset_order_semigroup_cancel: - pordered_ab_semigroup_add_imp_le "op +" "op \#" "op <#" + ordered_ab_semigroup_add_imp_le "op +" "op \#" "op <#" proof qed simp lemma mset_lessD: "A \# B \ x \# A \ x \# B" @@ -1348,7 +1348,7 @@ lemma union_upper2: "B <= A + (B::'a::order multiset)" by (subst add_commute) (rule union_upper1) -instance multiset :: (order) pordered_ab_semigroup_add +instance multiset :: (order) ordered_ab_semigroup_add apply intro_classes apply (erule union_le_mono[OF mult_le_refl]) done diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Library/Nat_Infinity.thy --- a/src/HOL/Library/Nat_Infinity.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Library/Nat_Infinity.thy Mon Feb 08 11:13:30 2010 +0100 @@ -234,7 +234,7 @@ subsection {* Ordering *} -instantiation inat :: ordered_ab_semigroup_add +instantiation inat :: linordered_ab_semigroup_add begin definition @@ -268,7 +268,7 @@ end -instance inat :: pordered_comm_semiring +instance inat :: ordered_comm_semiring proof fix a b c :: inat assume "a \ b" and "0 \ c" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Library/Polynomial.thy Mon Feb 08 11:13:30 2010 +0100 @@ -706,7 +706,7 @@ subsection {* Polynomials form an ordered integral domain *} definition - pos_poly :: "'a::ordered_idom poly \ bool" + pos_poly :: "'a::linordered_idom poly \ bool" where "pos_poly p \ 0 < coeff p (degree p)" @@ -732,7 +732,7 @@ lemma pos_poly_total: "p = 0 \ pos_poly p \ pos_poly (- p)" by (induct p) (auto simp add: pos_poly_pCons) -instantiation poly :: (ordered_idom) ordered_idom +instantiation poly :: (linordered_idom) linordered_idom begin definition diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Library/Structure_Syntax.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Structure_Syntax.thy Mon Feb 08 11:13:30 2010 +0100 @@ -0,0 +1,14 @@ +(* Author: Florian Haftmann, TU Muenchen *) + +header {* Index syntax for structures *} + +theory Structure_Syntax +imports Pure +begin + +syntax + "_index1" :: index ("\<^sub>1") +translations + (index) "\<^sub>1" => (index) "\<^bsub>\\<^esub>" + +end diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Library/Univ_Poly.thy --- a/src/HOL/Library/Univ_Poly.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Library/Univ_Poly.thy Mon Feb 08 11:13:30 2010 +0100 @@ -990,7 +990,7 @@ text{*bound for polynomial.*} -lemma poly_mono: "abs(x) \ k ==> abs(poly p (x::'a::{ordered_idom})) \ poly (map abs p) k" +lemma poly_mono: "abs(x) \ k ==> abs(poly p (x::'a::{linordered_idom})) \ poly (map abs p) k" apply (induct "p", auto) apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans) apply (rule abs_triangle_ineq) diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Library/positivstellensatz.ML Mon Feb 08 11:13:30 2010 +0100 @@ -275,7 +275,7 @@ "((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))" by auto}; -val abs_split' = @{lemma "P (abs (x::'a::ordered_idom)) == (x >= 0 & P x | x < 0 & P (-x))" +val abs_split' = @{lemma "P (abs (x::'a::linordered_idom)) == (x >= 0 & P x | x < 0 & P (-x))" by (atomize (full)) (auto split add: abs_split)}; val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/List.thy --- a/src/HOL/List.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/List.thy Mon Feb 08 11:13:30 2010 +0100 @@ -2500,12 +2500,12 @@ by (induct xs, simp_all add: algebra_simps) lemma listsum_abs: - fixes xs :: "'a::pordered_ab_group_add_abs list" + fixes xs :: "'a::ordered_ab_group_add_abs list" shows "\listsum xs\ \ listsum (map abs xs)" by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq]) lemma listsum_mono: - fixes f g :: "'a \ 'b::{comm_monoid_add, pordered_ab_semigroup_add}" + fixes f g :: "'a \ 'b::{comm_monoid_add, ordered_ab_semigroup_add}" shows "(\x. x \ set xs \ f x \ g x) \ (\x\xs. f x) \ (\x\xs. g x)" by (induct xs, simp, simp add: add_mono) diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Matrix/ComputeNumeral.thy --- a/src/HOL/Matrix/ComputeNumeral.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Matrix/ComputeNumeral.thy Mon Feb 08 11:13:30 2010 +0100 @@ -109,22 +109,22 @@ lemmas compute_natarith = bitarith natnorm natsuc natadd natsub natmul nateq natless natle natfac.simps -lemma number_eq: "(((number_of x)::'a::{number_ring, ordered_idom}) = (number_of y)) = (x = y)" +lemma number_eq: "(((number_of x)::'a::{number_ring, linordered_idom}) = (number_of y)) = (x = y)" unfolding number_of_eq apply simp done -lemma number_le: "(((number_of x)::'a::{number_ring, ordered_idom}) \ (number_of y)) = (x \ y)" +lemma number_le: "(((number_of x)::'a::{number_ring, linordered_idom}) \ (number_of y)) = (x \ y)" unfolding number_of_eq apply simp done -lemma number_less: "(((number_of x)::'a::{number_ring, ordered_idom}) < (number_of y)) = (x < y)" +lemma number_less: "(((number_of x)::'a::{number_ring, linordered_idom}) < (number_of y)) = (x < y)" unfolding number_of_eq apply simp done -lemma number_diff: "((number_of x)::'a::{number_ring, ordered_idom}) - number_of y = number_of (x + (- y))" +lemma number_diff: "((number_of x)::'a::{number_ring, linordered_idom}) - number_of y = number_of (x + (- y))" apply (subst diff_number_of_eq) apply simp done diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Matrix/LP.thy --- a/src/HOL/Matrix/LP.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Matrix/LP.thy Mon Feb 08 11:13:30 2010 +0100 @@ -8,7 +8,7 @@ lemma linprog_dual_estimate: assumes - "A * x \ (b::'a::lordered_ring)" + "A * x \ (b::'a::lattice_ring)" "0 \ y" "abs (A - A') \ \A" "b \ b'" @@ -57,7 +57,7 @@ lemma le_ge_imp_abs_diff_1: assumes - "A1 <= (A::'a::lordered_ring)" + "A1 <= (A::'a::lattice_ring)" "A <= A2" shows "abs (A-A1) <= A2-A1" proof - @@ -72,7 +72,7 @@ lemma mult_le_prts: assumes - "a1 <= (a::'a::lordered_ring)" + "a1 <= (a::'a::lattice_ring)" "a <= a2" "b1 <= b" "b <= b2" @@ -120,7 +120,7 @@ lemma mult_le_dual_prts: assumes - "A * x \ (b::'a::lordered_ring)" + "A * x \ (b::'a::lattice_ring)" "0 \ y" "A1 \ A" "A \ A2" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Matrix/Matrix.thy --- a/src/HOL/Matrix/Matrix.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Matrix/Matrix.thy Mon Feb 08 11:13:30 2010 +0100 @@ -1545,7 +1545,7 @@ by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext) qed -instance matrix :: (pordered_ab_group_add) pordered_ab_group_add +instance matrix :: (ordered_ab_group_add) ordered_ab_group_add proof fix A B C :: "'a matrix" assume "A <= B" @@ -1556,8 +1556,8 @@ done qed -instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet .. -instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_join .. +instance matrix :: (lattice_ab_group_add) semilattice_inf_ab_group_add .. +instance matrix :: (lattice_ab_group_add) semilattice_sup_ab_group_add .. instance matrix :: (semiring_0) semiring_0 proof @@ -1583,7 +1583,7 @@ instance matrix :: (ring) ring .. -instance matrix :: (pordered_ring) pordered_ring +instance matrix :: (ordered_ring) ordered_ring proof fix A B C :: "'a matrix" assume a: "A \ B" @@ -1600,9 +1600,9 @@ done qed -instance matrix :: (lordered_ring) lordered_ring +instance matrix :: (lattice_ring) lattice_ring proof - fix A B C :: "('a :: lordered_ring) matrix" + fix A B C :: "('a :: lattice_ring) matrix" show "abs A = sup A (-A)" by (simp add: abs_matrix_def) qed @@ -1738,7 +1738,7 @@ by auto lemma Rep_matrix_zero_imp_mult_zero: - "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0 \ A * B = (0::('a::lordered_ring) matrix)" + "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0 \ A * B = (0::('a::lattice_ring) matrix)" apply (subst Rep_matrix_inject[symmetric]) apply (rule ext)+ apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero) @@ -1803,7 +1803,7 @@ lemma Rep_minus[simp]: "Rep_matrix (-(A::_::group_add)) x y = - (Rep_matrix A x y)" by (simp add: minus_matrix_def) -lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ab_group_add)) x y = abs (Rep_matrix A x y)" +lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lattice_ab_group_add)) x y = abs (Rep_matrix A x y)" by (simp add: abs_lattice sup_matrix_def) end diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Matrix/SparseMatrix.thy --- a/src/HOL/Matrix/SparseMatrix.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Matrix/SparseMatrix.thy Mon Feb 08 11:13:30 2010 +0100 @@ -103,7 +103,7 @@ "minus_spvec [] = []" | "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)" -primrec abs_spvec :: "('a::lordered_ab_group_add_abs) spvec \ 'a spvec" where +primrec abs_spvec :: "('a::lattice_ab_group_add_abs) spvec \ 'a spvec" where "abs_spvec [] = []" | "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)" @@ -116,12 +116,12 @@ apply simp done -instance matrix :: (lordered_ab_group_add_abs) lordered_ab_group_add_abs +instance matrix :: (lattice_ab_group_add_abs) lattice_ab_group_add_abs apply default unfolding abs_matrix_def .. (*FIXME move*) lemma sparse_row_vector_abs: - "sorted_spvec (v :: 'a::lordered_ring spvec) \ sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)" + "sorted_spvec (v :: 'a::lattice_ring spvec) \ sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)" apply (induct v) apply simp_all apply (frule_tac sorted_spvec_cons1, simp) @@ -174,7 +174,7 @@ lemma addmult_spvec_empty2[simp]: "addmult_spvec y a [] = a" by (induct a) auto -lemma sparse_row_vector_map: "(! x y. f (x+y) = (f x) + (f y)) \ (f::'a\('a::lordered_ring)) 0 = 0 \ +lemma sparse_row_vector_map: "(! x y. f (x+y) = (f x) + (f y)) \ (f::'a\('a::lattice_ring)) 0 = 0 \ sparse_row_vector (map (% x. (fst x, f (snd x))) a) = apply_matrix f (sparse_row_vector a)" apply (induct a) apply (simp_all add: apply_matrix_add) @@ -185,7 +185,7 @@ apply (simp_all add: smult_spvec_cons scalar_mult_add) done -lemma sparse_row_vector_addmult_spvec: "sparse_row_vector (addmult_spvec (y::'a::lordered_ring) a b) = +lemma sparse_row_vector_addmult_spvec: "sparse_row_vector (addmult_spvec (y::'a::lattice_ring) a b) = (sparse_row_vector a) + (scalar_mult y (sparse_row_vector b))" apply (induct y a b rule: addmult_spvec.induct) apply (simp add: scalar_mult_add smult_spvec_cons sparse_row_vector_smult singleton_matrix_add)+ @@ -235,7 +235,7 @@ apply (simp_all add: sorted_spvec_addmult_spvec_helper3) done -fun mult_spvec_spmat :: "('a::lordered_ring) spvec \ 'a spvec \ 'a spmat \ 'a spvec" where +fun mult_spvec_spmat :: "('a::lattice_ring) spvec \ 'a spvec \ 'a spmat \ 'a spvec" where (* recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))" *) "mult_spvec_spmat c [] brr = c" | "mult_spvec_spmat c arr [] = c" | @@ -244,7 +244,7 @@ else if (j < i) then mult_spvec_spmat c ((i,a)#arr) brr else mult_spvec_spmat (addmult_spvec a c b) arr brr)" -lemma sparse_row_mult_spvec_spmat[rule_format]: "sorted_spvec (a::('a::lordered_ring) spvec) \ sorted_spvec B \ +lemma sparse_row_mult_spvec_spmat[rule_format]: "sorted_spvec (a::('a::lattice_ring) spvec) \ sorted_spvec B \ sparse_row_vector (mult_spvec_spmat c a B) = (sparse_row_vector c) + (sparse_row_vector a) * (sparse_row_matrix B)" proof - have comp_1: "!! a b. a < b \ Suc 0 <= nat ((int b)-(int a))" by arith @@ -337,13 +337,13 @@ qed lemma sorted_mult_spvec_spmat[rule_format]: - "sorted_spvec (c::('a::lordered_ring) spvec) \ sorted_spmat B \ sorted_spvec (mult_spvec_spmat c a B)" + "sorted_spvec (c::('a::lattice_ring) spvec) \ sorted_spmat B \ sorted_spvec (mult_spvec_spmat c a B)" apply (induct c a B rule: mult_spvec_spmat.induct) apply (simp_all add: sorted_addmult_spvec) done consts - mult_spmat :: "('a::lordered_ring) spmat \ 'a spmat \ 'a spmat" + mult_spmat :: "('a::lattice_ring) spmat \ 'a spmat \ 'a spmat" primrec "mult_spmat [] A = []" @@ -357,7 +357,7 @@ done lemma sorted_spvec_mult_spmat[rule_format]: - "sorted_spvec (A::('a::lordered_ring) spmat) \ sorted_spvec (mult_spmat A B)" + "sorted_spvec (A::('a::lattice_ring) spmat) \ sorted_spvec (mult_spmat A B)" apply (induct A) apply (auto) apply (drule sorted_spvec_cons1, simp) @@ -366,13 +366,13 @@ done lemma sorted_spmat_mult_spmat: - "sorted_spmat (B::('a::lordered_ring) spmat) \ sorted_spmat (mult_spmat A B)" + "sorted_spmat (B::('a::lattice_ring) spmat) \ sorted_spmat (mult_spmat A B)" apply (induct A) apply (auto simp add: sorted_mult_spvec_spmat) done -fun add_spvec :: "('a::lordered_ab_group_add) spvec \ 'a spvec \ 'a spvec" where +fun add_spvec :: "('a::lattice_ab_group_add) spvec \ 'a spvec \ 'a spvec" where (* "measure (% (a, b). length a + (length b))" *) "add_spvec arr [] = arr" | "add_spvec [] brr = brr" | @@ -389,7 +389,7 @@ apply (simp_all add: singleton_matrix_add) done -fun add_spmat :: "('a::lordered_ab_group_add) spmat \ 'a spmat \ 'a spmat" where +fun add_spmat :: "('a::lattice_ab_group_add) spmat \ 'a spmat \ 'a spmat" where (* "measure (% (A,B). (length A)+(length B))" *) "add_spmat [] bs = bs" | "add_spmat as [] = as" | @@ -532,7 +532,7 @@ apply (simp_all add: sorted_spvec_add_spvec) done -fun le_spvec :: "('a::lordered_ab_group_add) spvec \ 'a spvec \ bool" where +fun le_spvec :: "('a::lattice_ab_group_add) spvec \ 'a spvec \ bool" where (* "measure (% (a,b). (length a) + (length b))" *) "le_spvec [] [] = True" | "le_spvec ((_,a)#as) [] = (a <= 0 & le_spvec as [])" | @@ -542,7 +542,7 @@ else if (j < i) then 0 <= b & le_spvec ((i,a)#as) bs else a <= b & le_spvec as bs)" -fun le_spmat :: "('a::lordered_ab_group_add) spmat \ 'a spmat \ bool" where +fun le_spmat :: "('a::lattice_ab_group_add) spmat \ 'a spmat \ bool" where (* "measure (% (a,b). (length a) + (length b))" *) "le_spmat [] [] = True" | "le_spmat ((i,a)#as) [] = (le_spvec a [] & le_spmat as [])" | @@ -566,7 +566,7 @@ lemma disj_matrices_add: "disj_matrices A B \ disj_matrices C D \ disj_matrices A D \ disj_matrices B C \ - (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group_add) matrix))" + (A + B <= C + D) = (A <= C & B <= (D::('a::lattice_ab_group_add) matrix))" apply (auto) apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def) apply (intro strip) @@ -596,19 +596,19 @@ by (auto simp add: disj_matrices_def) lemma disj_matrices_add_le_zero: "disj_matrices A B \ - (A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group_add) matrix) <= 0)" + (A + B <= 0) = (A <= 0 & (B::('a::lattice_ab_group_add) matrix) <= 0)" by (rule disj_matrices_add[of A B 0 0, simplified]) lemma disj_matrices_add_zero_le: "disj_matrices A B \ - (0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group_add) matrix))" + (0 <= A + B) = (0 <= A & 0 <= (B::('a::lattice_ab_group_add) matrix))" by (rule disj_matrices_add[of 0 0 A B, simplified]) lemma disj_matrices_add_x_le: "disj_matrices A B \ disj_matrices B C \ - (A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group_add) matrix))" + (A <= B + C) = (A <= C & 0 <= (B::('a::lattice_ab_group_add) matrix))" by (auto simp add: disj_matrices_add[of 0 A B C, simplified]) lemma disj_matrices_add_le_x: "disj_matrices A B \ disj_matrices B C \ - (B + A <= C) = (A <= C & (B::('a::lordered_ab_group_add) matrix) <= 0)" + (B + A <= C) = (A <= C & (B::('a::lattice_ab_group_add) matrix) <= 0)" by (auto simp add: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute) lemma disj_sparse_row_singleton: "i <= j \ sorted_spvec((j,y)#v) \ disj_matrices (sparse_row_vector v) (singleton_matrix 0 i x)" @@ -624,7 +624,7 @@ apply (simp_all) done -lemma disj_matrices_x_add: "disj_matrices A B \ disj_matrices A C \ disj_matrices (A::('a::lordered_ab_group_add) matrix) (B+C)" +lemma disj_matrices_x_add: "disj_matrices A B \ disj_matrices A C \ disj_matrices (A::('a::lattice_ab_group_add) matrix) (B+C)" apply (simp add: disj_matrices_def) apply (auto) apply (drule_tac j=j and i=i in spec2)+ @@ -633,7 +633,7 @@ apply (simp_all) done -lemma disj_matrices_add_x: "disj_matrices A B \ disj_matrices A C \ disj_matrices (B+C) (A::('a::lordered_ab_group_add) matrix)" +lemma disj_matrices_add_x: "disj_matrices A B \ disj_matrices A C \ disj_matrices (B+C) (A::('a::lattice_ab_group_add) matrix)" by (simp add: disj_matrices_x_add disj_matrices_commute) lemma disj_singleton_matrices[simp]: "disj_matrices (singleton_matrix j i x) (singleton_matrix u v y) = (j \ u | i \ v | x = 0 | y = 0)" @@ -731,11 +731,11 @@ declare [[simp_depth_limit = 999]] -primrec abs_spmat :: "('a::lordered_ring) spmat \ 'a spmat" where +primrec abs_spmat :: "('a::lattice_ring) spmat \ 'a spmat" where "abs_spmat [] = []" | "abs_spmat (a#as) = (fst a, abs_spvec (snd a))#(abs_spmat as)" -primrec minus_spmat :: "('a::lordered_ring) spmat \ 'a spmat" where +primrec minus_spmat :: "('a::lattice_ring) spmat \ 'a spmat" where "minus_spmat [] = []" | "minus_spmat (a#as) = (fst a, minus_spvec (snd a))#(minus_spmat as)" @@ -803,7 +803,7 @@ done constdefs - diff_spmat :: "('a::lordered_ring) spmat \ 'a spmat \ 'a spmat" + diff_spmat :: "('a::lattice_ring) spmat \ 'a spmat \ 'a spmat" "diff_spmat A B == add_spmat A (minus_spmat B)" lemma sorted_spmat_diff_spmat: "sorted_spmat A \ sorted_spmat B \ sorted_spmat (diff_spmat A B)" @@ -845,10 +845,10 @@ lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp consts - pprt_spvec :: "('a::{lordered_ab_group_add}) spvec \ 'a spvec" - nprt_spvec :: "('a::{lordered_ab_group_add}) spvec \ 'a spvec" - pprt_spmat :: "('a::{lordered_ab_group_add}) spmat \ 'a spmat" - nprt_spmat :: "('a::{lordered_ab_group_add}) spmat \ 'a spmat" + pprt_spvec :: "('a::{lattice_ab_group_add}) spvec \ 'a spvec" + nprt_spvec :: "('a::{lattice_ab_group_add}) spvec \ 'a spvec" + pprt_spmat :: "('a::{lattice_ab_group_add}) spmat \ 'a spmat" + nprt_spmat :: "('a::{lattice_ab_group_add}) spmat \ 'a spmat" primrec "pprt_spvec [] = []" @@ -869,7 +869,7 @@ (*case (nprt_spvec (snd a)) of [] \ (nprt_spmat as) | y#ys \ (fst a, y#ys)#(nprt_spmat as))"*) -lemma pprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \ pprt (A+B) = pprt A + pprt B" +lemma pprt_add: "disj_matrices A (B::(_::lattice_ring) matrix) \ pprt (A+B) = pprt A + pprt B" apply (simp add: pprt_def sup_matrix_def) apply (simp add: Rep_matrix_inject[symmetric]) apply (rule ext)+ @@ -878,7 +878,7 @@ apply (simp_all add: disj_matrices_contr1) done -lemma nprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \ nprt (A+B) = nprt A + nprt B" +lemma nprt_add: "disj_matrices A (B::(_::lattice_ring) matrix) \ nprt (A+B) = nprt A + nprt B" apply (simp add: nprt_def inf_matrix_def) apply (simp add: Rep_matrix_inject[symmetric]) apply (rule ext)+ @@ -887,14 +887,14 @@ apply (simp_all add: disj_matrices_contr1) done -lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (pprt x)" +lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lattice_ring)) = singleton_matrix j i (pprt x)" apply (simp add: pprt_def sup_matrix_def) apply (simp add: Rep_matrix_inject[symmetric]) apply (rule ext)+ apply simp done -lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (nprt x)" +lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lattice_ring)) = singleton_matrix j i (nprt x)" apply (simp add: nprt_def inf_matrix_def) apply (simp add: Rep_matrix_inject[symmetric]) apply (rule ext)+ @@ -903,7 +903,7 @@ lemma less_imp_le: "a < b \ a <= (b::_::order)" by (simp add: less_def) -lemma sparse_row_vector_pprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \ sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)" +lemma sparse_row_vector_pprt: "sorted_spvec (v :: 'a::lattice_ring spvec) \ sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)" apply (induct v) apply (simp_all) apply (frule sorted_spvec_cons1, auto) @@ -913,7 +913,7 @@ apply auto done -lemma sparse_row_vector_nprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \ sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)" +lemma sparse_row_vector_nprt: "sorted_spvec (v :: 'a::lattice_ring spvec) \ sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)" apply (induct v) apply (simp_all) apply (frule sorted_spvec_cons1, auto) @@ -924,7 +924,7 @@ done -lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (pprt A) j i" +lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lattice_ring) matrix) j i) = move_matrix (pprt A) j i" apply (simp add: pprt_def) apply (simp add: sup_matrix_def) apply (simp add: Rep_matrix_inject[symmetric]) @@ -932,7 +932,7 @@ apply (simp) done -lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (nprt A) j i" +lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lattice_ring) matrix) j i) = move_matrix (nprt A) j i" apply (simp add: nprt_def) apply (simp add: inf_matrix_def) apply (simp add: Rep_matrix_inject[symmetric]) @@ -940,7 +940,7 @@ apply (simp) done -lemma sparse_row_matrix_pprt: "sorted_spvec (m :: 'a::lordered_ring spmat) \ sorted_spmat m \ sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)" +lemma sparse_row_matrix_pprt: "sorted_spvec (m :: 'a::lattice_ring spmat) \ sorted_spmat m \ sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)" apply (induct m) apply simp apply simp @@ -956,7 +956,7 @@ apply (simp add: pprt_move_matrix) done -lemma sparse_row_matrix_nprt: "sorted_spvec (m :: 'a::lordered_ring spmat) \ sorted_spmat m \ sparse_row_matrix (nprt_spmat m) = nprt (sparse_row_matrix m)" +lemma sparse_row_matrix_nprt: "sorted_spvec (m :: 'a::lattice_ring spmat) \ sorted_spmat m \ sparse_row_matrix (nprt_spmat m) = nprt (sparse_row_matrix m)" apply (induct m) apply simp apply simp @@ -1015,7 +1015,7 @@ done constdefs - mult_est_spmat :: "('a::lordered_ring) spmat \ 'a spmat \ 'a spmat \ 'a spmat \ 'a spmat" + mult_est_spmat :: "('a::lattice_ring) spmat \ 'a spmat \ 'a spmat \ 'a spmat \ 'a spmat" "mult_est_spmat r1 r2 s1 s2 == add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2)) (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))" @@ -1057,7 +1057,7 @@ "sorted_spvec b" "sorted_spvec r" "le_spmat ([], y)" - "A * x \ sparse_row_matrix (b::('a::lordered_ring) spmat)" + "A * x \ sparse_row_matrix (b::('a::lattice_ring) spmat)" "sparse_row_matrix A1 <= A" "A <= sparse_row_matrix A2" "sparse_row_matrix c1 <= c" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Matrix/cplex/Cplex.thy --- a/src/HOL/Matrix/cplex/Cplex.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Matrix/cplex/Cplex.thy Mon Feb 08 11:13:30 2010 +0100 @@ -25,7 +25,7 @@ "c \ sparse_row_matrix c2" "sparse_row_matrix r1 \ x" "x \ sparse_row_matrix r2" - "A * x \ sparse_row_matrix (b::('a::lordered_ring) spmat)" + "A * x \ sparse_row_matrix (b::('a::lattice_ring) spmat)" shows "c * x \ sparse_row_matrix (add_spmat (mult_spmat y b) (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in @@ -55,7 +55,7 @@ "c \ sparse_row_matrix c2" "sparse_row_matrix r1 \ x" "x \ sparse_row_matrix r2" - "A * x \ sparse_row_matrix (b::('a::lordered_ring) spmat)" + "A * x \ sparse_row_matrix (b::('a::lattice_ring) spmat)" shows "c * x \ sparse_row_matrix (add_spmat (mult_spmat y b) (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Metis_Examples/BigO.thy --- a/src/HOL/Metis_Examples/BigO.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Metis_Examples/BigO.thy Mon Feb 08 11:13:30 2010 +0100 @@ -12,11 +12,11 @@ subsection {* Definitions *} -definition bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set" ("(1O'(_'))") where +definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where "O(f::('a => 'b)) == {h. EX c. ALL x. abs (h x) <= c * abs (f x)}" declare [[ atp_problem_prefix = "BigO__bigo_pos_const" ]] -lemma bigo_pos_const: "(EX (c::'a::ordered_idom). +lemma bigo_pos_const: "(EX (c::'a::linordered_idom). ALL x. (abs (h x)) <= (c * (abs (f x)))) = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" apply auto @@ -30,7 +30,7 @@ declare [[sledgehammer_modulus = 1]] -lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). ALL x. (abs (h x)) <= (c * (abs (f x)))) = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" apply auto @@ -39,59 +39,59 @@ apply (rule_tac x = "abs c" in exI, auto) proof (neg_clausify) fix c x -have 0: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. \X1 * X2\ = \X2 * X1\" +have 0: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \X1 * X2\ = \X2 * X1\" by (metis abs_mult mult_commute) -have 1: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. - X1 \ (0\'a\ordered_idom) \ \X2\ * X1 = \X2 * X1\" +have 1: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. + X1 \ (0\'a\linordered_idom) \ \X2\ * X1 = \X2 * X1\" by (metis abs_mult_pos linorder_linear) -have 2: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. - \ (0\'a\ordered_idom) < X1 * X2 \ - \ (0\'a\ordered_idom) \ X2 \ \ X1 \ (0\'a\ordered_idom)" +have 2: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. + \ (0\'a\linordered_idom) < X1 * X2 \ + \ (0\'a\linordered_idom) \ X2 \ \ X1 \ (0\'a\linordered_idom)" by (metis linorder_not_less mult_nonneg_nonpos2) assume 3: "\x\'b\type. - \(h\'b\type \ 'a\ordered_idom) x\ - \ (c\'a\ordered_idom) * \(f\'b\type \ 'a\ordered_idom) x\" -assume 4: "\ \(h\'b\type \ 'a\ordered_idom) (x\'b\type)\ - \ \c\'a\ordered_idom\ * \(f\'b\type \ 'a\ordered_idom) x\" -have 5: "\ \(h\'b\type \ 'a\ordered_idom) (x\'b\type)\ - \ \(c\'a\ordered_idom) * (f\'b\type \ 'a\ordered_idom) x\" + \(h\'b\type \ 'a\linordered_idom) x\ + \ (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) x\" +assume 4: "\ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ + \ \c\'a\linordered_idom\ * \(f\'b\type \ 'a\linordered_idom) x\" +have 5: "\ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ + \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) x\" by (metis 4 abs_mult) -have 6: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. - \ X1 \ (0\'a\ordered_idom) \ X1 \ \X2\" +have 6: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. + \ X1 \ (0\'a\linordered_idom) \ X1 \ \X2\" by (metis abs_ge_zero xt1(6)) -have 7: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. - X1 \ \X2\ \ (0\'a\ordered_idom) < X1" +have 7: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. + X1 \ \X2\ \ (0\'a\linordered_idom) < X1" by (metis not_leE 6) -have 8: "(0\'a\ordered_idom) < \(h\'b\type \ 'a\ordered_idom) (x\'b\type)\" +have 8: "(0\'a\linordered_idom) < \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\" by (metis 5 7) -have 9: "\X1\'a\ordered_idom. - \ \(h\'b\type \ 'a\ordered_idom) (x\'b\type)\ \ X1 \ - (0\'a\ordered_idom) < X1" +have 9: "\X1\'a\linordered_idom. + \ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ \ X1 \ + (0\'a\linordered_idom) < X1" by (metis 8 order_less_le_trans) -have 10: "(0\'a\ordered_idom) -< (c\'a\ordered_idom) * \(f\'b\type \ 'a\ordered_idom) (x\'b\type)\" +have 10: "(0\'a\linordered_idom) +< (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) (x\'b\type)\" by (metis 3 9) -have 11: "\ (c\'a\ordered_idom) \ (0\'a\ordered_idom)" +have 11: "\ (c\'a\linordered_idom) \ (0\'a\linordered_idom)" by (metis abs_ge_zero 2 10) -have 12: "\X1\'a\ordered_idom. (c\'a\ordered_idom) * \X1\ = \X1 * c\" +have 12: "\X1\'a\linordered_idom. (c\'a\linordered_idom) * \X1\ = \X1 * c\" by (metis mult_commute 1 11) have 13: "\X1\'b\type. - - (h\'b\type \ 'a\ordered_idom) X1 - \ (c\'a\ordered_idom) * \(f\'b\type \ 'a\ordered_idom) X1\" + - (h\'b\type \ 'a\linordered_idom) X1 + \ (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) X1\" by (metis 3 abs_le_D2) have 14: "\X1\'b\type. - - (h\'b\type \ 'a\ordered_idom) X1 - \ \(c\'a\ordered_idom) * (f\'b\type \ 'a\ordered_idom) X1\" + - (h\'b\type \ 'a\linordered_idom) X1 + \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) X1\" by (metis 0 12 13) -have 15: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. \X1 * \X2\\ = \X1 * X2\" +have 15: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \X1 * \X2\\ = \X1 * X2\" by (metis abs_mult abs_mult_pos abs_ge_zero) -have 16: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. X1 \ \X2\ \ \ X1 \ X2" +have 16: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. X1 \ \X2\ \ \ X1 \ X2" by (metis xt1(6) abs_ge_self) -have 17: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. \ \X1\ \ X2 \ X1 \ \X2\" +have 17: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \ \X1\ \ X2 \ X1 \ \X2\" by (metis 16 abs_le_D1) have 18: "\X1\'b\type. - (h\'b\type \ 'a\ordered_idom) X1 - \ \(c\'a\ordered_idom) * (f\'b\type \ 'a\ordered_idom) X1\" + (h\'b\type \ 'a\linordered_idom) X1 + \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) X1\" by (metis 17 3 15) show "False" by (metis abs_le_iff 5 18 14) @@ -99,7 +99,7 @@ declare [[sledgehammer_modulus = 2]] -lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). ALL x. (abs (h x)) <= (c * (abs (f x)))) = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" apply auto @@ -108,31 +108,31 @@ apply (rule_tac x = "abs c" in exI, auto); proof (neg_clausify) fix c x -have 0: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. \X1 * X2\ = \X2 * X1\" +have 0: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \X1 * X2\ = \X2 * X1\" by (metis abs_mult mult_commute) assume 1: "\x\'b\type. - \(h\'b\type \ 'a\ordered_idom) x\ - \ (c\'a\ordered_idom) * \(f\'b\type \ 'a\ordered_idom) x\" -assume 2: "\ \(h\'b\type \ 'a\ordered_idom) (x\'b\type)\ - \ \c\'a\ordered_idom\ * \(f\'b\type \ 'a\ordered_idom) x\" -have 3: "\ \(h\'b\type \ 'a\ordered_idom) (x\'b\type)\ - \ \(c\'a\ordered_idom) * (f\'b\type \ 'a\ordered_idom) x\" + \(h\'b\type \ 'a\linordered_idom) x\ + \ (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) x\" +assume 2: "\ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ + \ \c\'a\linordered_idom\ * \(f\'b\type \ 'a\linordered_idom) x\" +have 3: "\ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ + \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) x\" by (metis 2 abs_mult) -have 4: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. - \ X1 \ (0\'a\ordered_idom) \ X1 \ \X2\" +have 4: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. + \ X1 \ (0\'a\linordered_idom) \ X1 \ \X2\" by (metis abs_ge_zero xt1(6)) -have 5: "(0\'a\ordered_idom) < \(h\'b\type \ 'a\ordered_idom) (x\'b\type)\" +have 5: "(0\'a\linordered_idom) < \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\" by (metis not_leE 4 3) -have 6: "(0\'a\ordered_idom) -< (c\'a\ordered_idom) * \(f\'b\type \ 'a\ordered_idom) (x\'b\type)\" +have 6: "(0\'a\linordered_idom) +< (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) (x\'b\type)\" by (metis 1 order_less_le_trans 5) -have 7: "\X1\'a\ordered_idom. (c\'a\ordered_idom) * \X1\ = \X1 * c\" +have 7: "\X1\'a\linordered_idom. (c\'a\linordered_idom) * \X1\ = \X1 * c\" by (metis abs_ge_zero linorder_not_less mult_nonneg_nonpos2 6 linorder_linear abs_mult_pos mult_commute) have 8: "\X1\'b\type. - - (h\'b\type \ 'a\ordered_idom) X1 - \ \(c\'a\ordered_idom) * (f\'b\type \ 'a\ordered_idom) X1\" + - (h\'b\type \ 'a\linordered_idom) X1 + \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) X1\" by (metis 0 7 abs_le_D2 1) -have 9: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. \ \X1\ \ X2 \ X1 \ \X2\" +have 9: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \ \X1\ \ X2 \ X1 \ \X2\" by (metis abs_ge_self xt1(6) abs_le_D1) show "False" by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff) @@ -140,7 +140,7 @@ declare [[sledgehammer_modulus = 3]] -lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). ALL x. (abs (h x)) <= (c * (abs (f x)))) = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" apply auto @@ -150,20 +150,20 @@ proof (neg_clausify) fix c x assume 0: "\x\'b\type. - \(h\'b\type \ 'a\ordered_idom) x\ - \ (c\'a\ordered_idom) * \(f\'b\type \ 'a\ordered_idom) x\" -assume 1: "\ \(h\'b\type \ 'a\ordered_idom) (x\'b\type)\ - \ \c\'a\ordered_idom\ * \(f\'b\type \ 'a\ordered_idom) x\" -have 2: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. - X1 \ \X2\ \ (0\'a\ordered_idom) < X1" + \(h\'b\type \ 'a\linordered_idom) x\ + \ (c\'a\linordered_idom) * \(f\'b\type \ 'a\linordered_idom) x\" +assume 1: "\ \(h\'b\type \ 'a\linordered_idom) (x\'b\type)\ + \ \c\'a\linordered_idom\ * \(f\'b\type \ 'a\linordered_idom) x\" +have 2: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. + X1 \ \X2\ \ (0\'a\linordered_idom) < X1" by (metis abs_ge_zero xt1(6) not_leE) -have 3: "\ (c\'a\ordered_idom) \ (0\'a\ordered_idom)" +have 3: "\ (c\'a\linordered_idom) \ (0\'a\linordered_idom)" by (metis abs_ge_zero mult_nonneg_nonpos2 linorder_not_less order_less_le_trans 1 abs_mult 2 0) -have 4: "\(X1\'a\ordered_idom) X2\'a\ordered_idom. \X1 * \X2\\ = \X1 * X2\" +have 4: "\(X1\'a\linordered_idom) X2\'a\linordered_idom. \X1 * \X2\\ = \X1 * X2\" by (metis abs_ge_zero abs_mult_pos abs_mult) have 5: "\X1\'b\type. - (h\'b\type \ 'a\ordered_idom) X1 - \ \(c\'a\ordered_idom) * (f\'b\type \ 'a\ordered_idom) X1\" + (h\'b\type \ 'a\linordered_idom) X1 + \ \(c\'a\linordered_idom) * (f\'b\type \ 'a\linordered_idom) X1\" by (metis 4 0 xt1(6) abs_ge_self abs_le_D1) show "False" by (metis abs_mult mult_commute 3 abs_mult_pos linorder_linear 0 abs_le_D2 5 1 abs_le_iff) @@ -172,7 +172,7 @@ declare [[sledgehammer_modulus = 1]] -lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). ALL x. (abs (h x)) <= (c * (abs (f x)))) = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" apply auto @@ -181,7 +181,7 @@ apply (rule_tac x = "abs c" in exI, auto); proof (neg_clausify) fix c x (*sort/type constraint inserted by hand!*) -have 0: "\(X1\'a\ordered_idom) X2. \X1 * \X2\\ = \X1 * X2\" +have 0: "\(X1\'a\linordered_idom) X2. \X1 * \X2\\ = \X1 * X2\" by (metis abs_ge_zero abs_mult_pos abs_mult) assume 1: "\A. \h A\ \ c * \f A\" have 2: "\X1 X2. \ \X1\ \ X2 \ (0\'a) \ X2" @@ -383,11 +383,11 @@ by (metis 0 order_antisym_conv) have 3: "\X3. \ f (x \X3\) \ \X3 * g (x \X3\)\" by (metis 1 abs_mult) -have 4: "\X1 X3\'b\ordered_idom. X3 \ X1 \ X1 \ \X3\" +have 4: "\X1 X3\'b\linordered_idom. X3 \ X1 \ X1 \ \X3\" by (metis linorder_linear abs_le_D1) have 5: "\X3::'b. \X3\ * \X3\ = X3 * X3" by (metis abs_mult_self) -have 6: "\X3. \ X3 * X3 < (0\'b\ordered_idom)" +have 6: "\X3. \ X3 * X3 < (0\'b\linordered_idom)" by (metis not_square_less_zero) have 7: "\X1 X3::'b. \X1\ * \X3\ = \X3 * X1\" by (metis abs_mult mult_commute) @@ -438,26 +438,26 @@ proof (neg_clausify) fix x assume 0: "\A\'a\type. - (f\'a\type \ 'b\ordered_idom) A - \ (c\'b\ordered_idom) * (g\'a\type \ 'b\ordered_idom) A" -assume 1: "\A\'b\ordered_idom. - \ (f\'a\type \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a\type) A) - \ A * \(g\'a\type \ 'b\ordered_idom) (x A)\" + (f\'a\type \ 'b\linordered_idom) A + \ (c\'b\linordered_idom) * (g\'a\type \ 'b\linordered_idom) A" +assume 1: "\A\'b\linordered_idom. + \ (f\'a\type \ 'b\linordered_idom) ((x\'b\linordered_idom \ 'a\type) A) + \ A * \(g\'a\type \ 'b\linordered_idom) (x A)\" have 2: "\X2\'a\type. - \ (c\'b\ordered_idom) * (g\'a\type \ 'b\ordered_idom) X2 - < (f\'a\type \ 'b\ordered_idom) X2" + \ (c\'b\linordered_idom) * (g\'a\type \ 'b\linordered_idom) X2 + < (f\'a\type \ 'b\linordered_idom) X2" by (metis 0 linorder_not_le) -have 3: "\X2\'b\ordered_idom. - \ (f\'a\type \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a\type) \X2\) - \ \X2 * (g\'a\type \ 'b\ordered_idom) (x \X2\)\" +have 3: "\X2\'b\linordered_idom. + \ (f\'a\type \ 'b\linordered_idom) ((x\'b\linordered_idom \ 'a\type) \X2\) + \ \X2 * (g\'a\type \ 'b\linordered_idom) (x \X2\)\" by (metis abs_mult 1) -have 4: "\X2\'b\ordered_idom. - \X2 * (g\'a\type \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a\type) \X2\)\ - < (f\'a\type \ 'b\ordered_idom) (x \X2\)" +have 4: "\X2\'b\linordered_idom. + \X2 * (g\'a\type \ 'b\linordered_idom) ((x\'b\linordered_idom \ 'a\type) \X2\)\ + < (f\'a\type \ 'b\linordered_idom) (x \X2\)" by (metis 3 linorder_not_less) -have 5: "\X2\'b\ordered_idom. - X2 * (g\'a\type \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a\type) \X2\) - < (f\'a\type \ 'b\ordered_idom) (x \X2\)" +have 5: "\X2\'b\linordered_idom. + X2 * (g\'a\type \ 'b\linordered_idom) ((x\'b\linordered_idom \ 'a\type) \X2\) + < (f\'a\type \ 'b\linordered_idom) (x \X2\)" by (metis abs_less_iff 4) show "False" by (metis 2 5) @@ -603,54 +603,54 @@ just been done*) proof (neg_clausify) fix a c b ca x -assume 0: "(0\'b\ordered_idom) < (c\'b\ordered_idom)" -assume 1: "\(a\'a \ 'b\ordered_idom) (x\'a)\ -\ (c\'b\ordered_idom) * \(f\'a \ 'b\ordered_idom) x\" -assume 2: "\(b\'a \ 'b\ordered_idom) (x\'a)\ -\ (ca\'b\ordered_idom) * \(g\'a \ 'b\ordered_idom) x\" -assume 3: "\ \(a\'a \ 'b\ordered_idom) (x\'a)\ * - \(b\'a \ 'b\ordered_idom) x\ - \ (c\'b\ordered_idom) * \(f\'a \ 'b\ordered_idom) x\ * - ((ca\'b\ordered_idom) * \(g\'a \ 'b\ordered_idom) x\)" -have 4: "\c\'b\ordered_idom\ = c" +assume 0: "(0\'b\linordered_idom) < (c\'b\linordered_idom)" +assume 1: "\(a\'a \ 'b\linordered_idom) (x\'a)\ +\ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) x\" +assume 2: "\(b\'a \ 'b\linordered_idom) (x\'a)\ +\ (ca\'b\linordered_idom) * \(g\'a \ 'b\linordered_idom) x\" +assume 3: "\ \(a\'a \ 'b\linordered_idom) (x\'a)\ * + \(b\'a \ 'b\linordered_idom) x\ + \ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) x\ * + ((ca\'b\linordered_idom) * \(g\'a \ 'b\linordered_idom) x\)" +have 4: "\c\'b\linordered_idom\ = c" by (metis OrderedGroup.abs_of_pos 0) -have 5: "\X1\'b\ordered_idom. (c\'b\ordered_idom) * \X1\ = \c * X1\" +have 5: "\X1\'b\linordered_idom. (c\'b\linordered_idom) * \X1\ = \c * X1\" by (metis Ring_and_Field.abs_mult 4) -have 6: "(0\'b\ordered_idom) = (1\'b\ordered_idom) \ -(0\'b\ordered_idom) < (1\'b\ordered_idom)" - by (metis OrderedGroup.abs_not_less_zero Ring_and_Field.abs_one Ring_and_Field.linorder_neqE_ordered_idom) -have 7: "(0\'b\ordered_idom) < (1\'b\ordered_idom)" +have 6: "(0\'b\linordered_idom) = (1\'b\linordered_idom) \ +(0\'b\linordered_idom) < (1\'b\linordered_idom)" + by (metis OrderedGroup.abs_not_less_zero Ring_and_Field.abs_one Ring_and_Field.linorder_neqE_linordered_idom) +have 7: "(0\'b\linordered_idom) < (1\'b\linordered_idom)" by (metis 6 Ring_and_Field.one_neq_zero) -have 8: "\1\'b\ordered_idom\ = (1\'b\ordered_idom)" +have 8: "\1\'b\linordered_idom\ = (1\'b\linordered_idom)" by (metis OrderedGroup.abs_of_pos 7) -have 9: "\X1\'b\ordered_idom. (0\'b\ordered_idom) \ (c\'b\ordered_idom) * \X1\" +have 9: "\X1\'b\linordered_idom. (0\'b\linordered_idom) \ (c\'b\linordered_idom) * \X1\" by (metis OrderedGroup.abs_ge_zero 5) -have 10: "\X1\'b\ordered_idom. X1 * (1\'b\ordered_idom) = X1" +have 10: "\X1\'b\linordered_idom. X1 * (1\'b\linordered_idom) = X1" by (metis Ring_and_Field.mult_cancel_right2 mult_commute) -have 11: "\X1\'b\ordered_idom. \\X1\\ = \X1\ * \1\'b\ordered_idom\" +have 11: "\X1\'b\linordered_idom. \\X1\\ = \X1\ * \1\'b\linordered_idom\" by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 10) -have 12: "\X1\'b\ordered_idom. \\X1\\ = \X1\" +have 12: "\X1\'b\linordered_idom. \\X1\\ = \X1\" by (metis 11 8 10) -have 13: "\X1\'b\ordered_idom. (0\'b\ordered_idom) \ \X1\" +have 13: "\X1\'b\linordered_idom. (0\'b\linordered_idom) \ \X1\" by (metis OrderedGroup.abs_ge_zero 12) -have 14: "\ (0\'b\ordered_idom) - \ (c\'b\ordered_idom) * \(f\'a \ 'b\ordered_idom) (x\'a)\ \ -\ (0\'b\ordered_idom) \ \(b\'a \ 'b\ordered_idom) x\ \ -\ \b x\ \ (ca\'b\ordered_idom) * \(g\'a \ 'b\ordered_idom) x\ \ -\ \(a\'a \ 'b\ordered_idom) x\ \ c * \f x\" +have 14: "\ (0\'b\linordered_idom) + \ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) (x\'a)\ \ +\ (0\'b\linordered_idom) \ \(b\'a \ 'b\linordered_idom) x\ \ +\ \b x\ \ (ca\'b\linordered_idom) * \(g\'a \ 'b\linordered_idom) x\ \ +\ \(a\'a \ 'b\linordered_idom) x\ \ c * \f x\" by (metis 3 Ring_and_Field.mult_mono) -have 15: "\ (0\'b\ordered_idom) \ \(b\'a \ 'b\ordered_idom) (x\'a)\ \ -\ \b x\ \ (ca\'b\ordered_idom) * \(g\'a \ 'b\ordered_idom) x\ \ -\ \(a\'a \ 'b\ordered_idom) x\ - \ (c\'b\ordered_idom) * \(f\'a \ 'b\ordered_idom) x\" +have 15: "\ (0\'b\linordered_idom) \ \(b\'a \ 'b\linordered_idom) (x\'a)\ \ +\ \b x\ \ (ca\'b\linordered_idom) * \(g\'a \ 'b\linordered_idom) x\ \ +\ \(a\'a \ 'b\linordered_idom) x\ + \ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) x\" by (metis 14 9) -have 16: "\ \(b\'a \ 'b\ordered_idom) (x\'a)\ - \ (ca\'b\ordered_idom) * \(g\'a \ 'b\ordered_idom) x\ \ -\ \(a\'a \ 'b\ordered_idom) x\ - \ (c\'b\ordered_idom) * \(f\'a \ 'b\ordered_idom) x\" +have 16: "\ \(b\'a \ 'b\linordered_idom) (x\'a)\ + \ (ca\'b\linordered_idom) * \(g\'a \ 'b\linordered_idom) x\ \ +\ \(a\'a \ 'b\linordered_idom) x\ + \ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) x\" by (metis 15 13) -have 17: "\ \(a\'a \ 'b\ordered_idom) (x\'a)\ - \ (c\'b\ordered_idom) * \(f\'a \ 'b\ordered_idom) x\" +have 17: "\ \(a\'a \ 'b\linordered_idom) (x\'a)\ + \ (c\'b\linordered_idom) * \(f\'a \ 'b\linordered_idom) x\" by (metis 16 2) show 18: "False" by (metis 17 1) @@ -682,7 +682,7 @@ lemma bigo_mult5: "ALL x. f x ~= 0 ==> - O(f * g) <= (f::'a => ('b::ordered_field)) *o O(g)" + O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)" proof - assume "ALL x. f x ~= 0" show "O(f * g) <= f *o O(g)" @@ -712,14 +712,14 @@ declare [[ atp_problem_prefix = "BigO__bigo_mult6" ]] lemma bigo_mult6: "ALL x. f x ~= 0 ==> - O(f * g) = (f::'a => ('b::ordered_field)) *o O(g)" + O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)" by (metis bigo_mult2 bigo_mult5 order_antisym) (*proof requires relaxing relevance: 2007-01-25*) declare [[ atp_problem_prefix = "BigO__bigo_mult7" ]] declare bigo_mult6 [simp] lemma bigo_mult7: "ALL x. f x ~= 0 ==> - O(f * g) <= O(f::'a => ('b::ordered_field)) \ O(g)" + O(f * g) <= O(f::'a => ('b::linordered_field)) \ O(g)" (*sledgehammer*) apply (subst bigo_mult6) apply assumption @@ -731,7 +731,7 @@ declare [[ atp_problem_prefix = "BigO__bigo_mult8" ]] declare bigo_mult7[intro!] lemma bigo_mult8: "ALL x. f x ~= 0 ==> - O(f * g) = O(f::'a => ('b::ordered_field)) \ O(g)" + O(f * g) = O(f::'a => ('b::linordered_field)) \ O(g)" by (metis bigo_mult bigo_mult7 order_antisym_conv) lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)" @@ -810,11 +810,11 @@ lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)" by (metis bigo_const1 bigo_elt_subset); -lemma bigo_const2 [intro]: "O(%x. c::'b::ordered_idom) <= O(%x. 1)"; +lemma bigo_const2 [intro]: "O(%x. c::'b::linordered_idom) <= O(%x. 1)"; (*??FAILS because the two occurrences of COMBK have different polymorphic types proof (neg_clausify) -assume 0: "\ O(COMBK (c\'b\ordered_idom)) \ O(COMBK (1\'b\ordered_idom))" -have 1: "COMBK (c\'b\ordered_idom) \ O(COMBK (1\'b\ordered_idom))" +assume 0: "\ O(COMBK (c\'b\linordered_idom)) \ O(COMBK (1\'b\linordered_idom))" +have 1: "COMBK (c\'b\linordered_idom) \ O(COMBK (1\'b\linordered_idom))" apply (rule notI) apply (rule 0 [THEN notE]) apply (rule bigo_elt_subset) @@ -830,26 +830,26 @@ done declare [[ atp_problem_prefix = "BigO__bigo_const3" ]] -lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)" +lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)" apply (simp add: bigo_def) proof (neg_clausify) -assume 0: "(c\'a\ordered_field) \ (0\'a\ordered_field)" -assume 1: "\A\'a\ordered_field. \ (1\'a\ordered_field) \ A * \c\'a\ordered_field\" -have 2: "(0\'a\ordered_field) = \c\'a\ordered_field\ \ -\ (1\'a\ordered_field) \ (1\'a\ordered_field)" +assume 0: "(c\'a\linordered_field) \ (0\'a\linordered_field)" +assume 1: "\A\'a\linordered_field. \ (1\'a\linordered_field) \ A * \c\'a\linordered_field\" +have 2: "(0\'a\linordered_field) = \c\'a\linordered_field\ \ +\ (1\'a\linordered_field) \ (1\'a\linordered_field)" by (metis 1 field_inverse) -have 3: "\c\'a\ordered_field\ = (0\'a\ordered_field)" +have 3: "\c\'a\linordered_field\ = (0\'a\linordered_field)" by (metis linorder_neq_iff linorder_antisym_conv1 2) -have 4: "(0\'a\ordered_field) = (c\'a\ordered_field)" +have 4: "(0\'a\linordered_field) = (c\'a\linordered_field)" by (metis 3 abs_eq_0) show "False" by (metis 0 4) qed -lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)" +lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)" by (rule bigo_elt_subset, rule bigo_const3, assumption) -lemma bigo_const [simp]: "(c::'a::ordered_field) ~= 0 ==> +lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==> O(%x. c) = O(%x. 1)" by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption) @@ -858,9 +858,9 @@ apply (simp add: bigo_def abs_mult) proof (neg_clausify) fix x -assume 0: "\xa\'b\ordered_idom. - \ \c\'b\ordered_idom\ * - \(f\'a\type \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a\type) xa)\ +assume 0: "\xa\'b\linordered_idom. + \ \c\'b\linordered_idom\ * + \(f\'a\type \ 'b\linordered_idom) ((x\'b\linordered_idom \ 'a\type) xa)\ \ xa * \f (x xa)\" show "False" by (metis linorder_neq_iff linorder_antisym_conv1 0) @@ -870,7 +870,7 @@ by (rule bigo_elt_subset, rule bigo_const_mult1) declare [[ atp_problem_prefix = "BigO__bigo_const_mult3" ]] -lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)" +lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)" apply (simp add: bigo_def) (*sledgehammer [no luck]*); apply (rule_tac x = "abs(inverse c)" in exI) @@ -879,16 +879,16 @@ apply (auto ); done -lemma bigo_const_mult4: "(c::'a::ordered_field) ~= 0 ==> +lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==> O(f) <= O(%x. c * f x)" by (rule bigo_elt_subset, rule bigo_const_mult3, assumption) -lemma bigo_const_mult [simp]: "(c::'a::ordered_field) ~= 0 ==> +lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==> O(%x. c * f x) = O(f)" by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4) declare [[ atp_problem_prefix = "BigO__bigo_const_mult5" ]] -lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==> +lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==> (%x. c) *o O(f) = O(f)" apply (auto del: subsetI) apply (rule order_trans) @@ -1057,7 +1057,7 @@ apply assumption+ done -lemma bigo_useful_const_mult: "(c::'a::ordered_field) ~= 0 ==> +lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==> (%x. c) * f =o O(h) ==> f =o O(h)" apply (rule subsetD) apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)") @@ -1100,7 +1100,7 @@ subsection {* Less than or equal to *} constdefs - lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)" + lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "A. k A \ f A" -have 1: "\(X1\'b\ordered_idom) X2. \ max X1 X2 < X1" +have 1: "\(X1\'b\linordered_idom) X2. \ max X1 X2 < X1" by (metis linorder_not_less le_maxI1) (*sort inserted by hand*) assume 2: "(0\'b) \ k x - g x" have 3: "\ k x - g x < (0\'b)" @@ -1206,7 +1206,7 @@ apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute) done -lemma bigo_lesso4: "f 'b::ordered_field) ==> +lemma bigo_lesso4: "f 'b::linordered_field) ==> g =o h +o O(k) ==> f s" "0 < dist y x" "dist y x < e / (B * C * D)" have "norm (h (f' (y - x)) (g' (y - x))) \ norm (f' (y - x)) * norm (g' (y - x)) * B" using B by auto also have "\ \ (norm (y - x) * C) * (D * norm (y - x)) * B" apply(rule mult_right_mono) - apply(rule pordered_semiring_class.mult_mono) using B C D by (auto simp add: field_simps intro!:mult_nonneg_nonneg) + apply(rule mult_mono) using B C D by (auto simp add: field_simps intro!:mult_nonneg_nonneg) also have "\ = (B * C * D * norm (y - x)) * norm (y - x)" by(auto simp add:field_simps) also have "\ < e * norm (y - x)" apply(rule mult_strict_right_mono) using as(3)[unfolded vector_dist_norm] and as(2) unfolding pos_less_divide_eq[OF bcd] by (auto simp add:field_simps) diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Mon Feb 08 11:13:30 2010 +0100 @@ -44,7 +44,7 @@ else setprod f {m..n})" by (auto simp add: atLeastAtMostSuc_conv) -lemma setprod_le: assumes fS: "finite S" and fg: "\x\S. f x \ 0 \ f x \ (g x :: 'a::ordered_idom)" +lemma setprod_le: assumes fS: "finite S" and fg: "\x\S. f x \ 0 \ f x \ (g x :: 'a::linordered_idom)" shows "setprod f S \ setprod g S" using fS fg apply(induct S) @@ -61,7 +61,7 @@ apply simp done -lemma setprod_le_1: assumes fS: "finite S" and f: "\x\S. f x \ 0 \ f x \ (1::'a::ordered_idom)" +lemma setprod_le_1: assumes fS: "finite S" and f: "\x\S. f x \ 0 \ f x \ (1::'a::linordered_idom)" shows "setprod f S \ 1" using setprod_le[OF fS f] unfolding setprod_1 . @@ -277,7 +277,7 @@ qed lemma det_identical_rows: - fixes A :: "'a::ordered_idom^'n^'n" + fixes A :: "'a::linordered_idom^'n^'n" assumes ij: "i \ j" and r: "row i A = row j A" shows "det A = 0" @@ -295,7 +295,7 @@ qed lemma det_identical_columns: - fixes A :: "'a::ordered_idom^'n^'n" + fixes A :: "'a::linordered_idom^'n^'n" assumes ij: "i \ j" and r: "column i A = column j A" shows "det A = 0" @@ -407,7 +407,7 @@ unfolding vector_smult_lzero . lemma det_row_operation: - fixes A :: "'a::ordered_idom^'n^'n" + fixes A :: "'a::linordered_idom^'n^'n" assumes ij: "i \ j" shows "det (\ k. if k = i then row i A + c *s row j A else row k A) = det A" proof- @@ -421,7 +421,7 @@ qed lemma det_row_span: - fixes A :: "'a:: ordered_idom^'n^'n" + fixes A :: "'a:: linordered_idom^'n^'n" assumes x: "x \ span {row j A |j. j \ i}" shows "det (\ k. if k = i then row i A + x else row k A) = det A" proof- @@ -462,7 +462,7 @@ (* ------------------------------------------------------------------------- *) lemma det_dependent_rows: - fixes A:: "'a::ordered_idom^'n^'n" + fixes A:: "'a::linordered_idom^'n^'n" assumes d: "dependent (rows A)" shows "det A = 0" proof- @@ -488,7 +488,7 @@ ultimately show ?thesis by blast qed -lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n))" shows "det A = 0" +lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::linordered_idom^'n^'n))" shows "det A = 0" by (metis d det_dependent_rows rows_transp det_transp) (* ------------------------------------------------------------------------- *) @@ -608,7 +608,7 @@ qed lemma det_mul: - fixes A B :: "'a::ordered_idom^'n^'n" + fixes A B :: "'a::linordered_idom^'n^'n" shows "det (A ** B) = det A * det B" proof- let ?U = "UNIV :: 'n set" @@ -761,7 +761,7 @@ (* ------------------------------------------------------------------------- *) lemma cramer_lemma_transp: - fixes A:: "'a::ordered_idom^'n^'n" and x :: "'a ^'n" + fixes A:: "'a::linordered_idom^'n^'n" and x :: "'a ^'n" shows "det ((\ i. if i = k then setsum (\i. x$i *s row i A) (UNIV::'n set) else row i A)::'a^'n^'n) = x$k * det A" (is "?lhs = ?rhs") @@ -797,7 +797,7 @@ qed lemma cramer_lemma: - fixes A :: "'a::ordered_idom ^'n^'n" + fixes A :: "'a::linordered_idom ^'n^'n" shows "det((\ i j. if j = k then (A *v x)$i else A$i$j):: 'a^'n^'n) = x$k * det A" proof- let ?U = "UNIV :: 'n set" @@ -893,7 +893,7 @@ qed lemma det_orthogonal_matrix: - fixes Q:: "'a::ordered_idom^'n^'n" + fixes Q:: "'a::linordered_idom^'n^'n" assumes oQ: "orthogonal_matrix Q" shows "det Q = 1 \ det Q = - 1" proof- @@ -1034,7 +1034,7 @@ definition "rotoinversion_matrix Q \ orthogonal_matrix Q \ det Q = - 1" lemma orthogonal_rotation_or_rotoinversion: - fixes Q :: "'a::ordered_idom^'n^'n" + fixes Q :: "'a::linordered_idom^'n^'n" shows " orthogonal_matrix Q \ rotation_matrix Q \ rotoinversion_matrix Q" by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) (* ------------------------------------------------------------------------- *) diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Feb 08 11:13:30 2010 +0100 @@ -459,7 +459,7 @@ done lemma setsum_nonneg_eq_0_iff: - fixes f :: "'a \ 'b::pordered_ab_group_add" + fixes f :: "'a \ 'b::ordered_ab_group_add" shows "\finite A; \x\A. 0 \ f x\ \ setsum f A = 0 \ (\x\A. f x = 0)" apply (induct set: finite, simp) apply (simp add: add_nonneg_eq_0_iff setsum_nonneg) @@ -836,10 +836,10 @@ lemma dot_rneg: "(x::'a::ring ^ 'n) \ (-y) = -(x \ y)" by vector lemma dot_lzero[simp]: "0 \ x = (0::'a::{comm_monoid_add, mult_zero})" by vector lemma dot_rzero[simp]: "x \ 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector -lemma dot_pos_le[simp]: "(0::'a\ordered_ring_strict) <= x \ x" +lemma dot_pos_le[simp]: "(0::'a\linlinordered_ring_strict) <= x \ x" by (simp add: dot_def setsum_nonneg) -lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\x \ F. f x \ (0 ::'a::pordered_ab_group_add)" shows "setsum f F = 0 \ (ALL x:F. f x = 0)" +lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\x \ F. f x \ (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \ (ALL x:F. f x = 0)" using fS fp setsum_nonneg[OF fp] proof (induct set: finite) case empty thus ?case by simp @@ -852,10 +852,10 @@ show ?case by (simp add: h) qed -lemma dot_eq_0: "x \ x = 0 \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0" +lemma dot_eq_0: "x \ x = 0 \ (x::'a::{linlinordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0" by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq) -lemma dot_pos_lt[simp]: "(0 < x \ x) \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \ 0" using dot_eq_0[of x] dot_pos_le[of x] +lemma dot_pos_lt[simp]: "(0 < x \ x) \ (x::'a::{linlinordered_ring_strict,ring_no_zero_divisors} ^ 'n) \ 0" using dot_eq_0[of x] dot_pos_le[of x] by (auto simp add: le_less) subsection{* The collapse of the general concepts to dimension one. *} @@ -1146,7 +1146,7 @@ shows "norm x1 \ b1 \ norm x2 \ b2 \ norm (x1 + x2) \ b1 + b2" by (rule order_trans [OF norm_triangle_ineq add_mono]) -lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \ b == a - b \ 0" +lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \ b == a - b \ 0" by (simp add: ring_simps) lemma pth_1: @@ -3827,7 +3827,7 @@ (* FIXME : Move to some general theory ?*) definition "pairwise R S \ (\x \ S. \y\ S. x\y \ R x y)" -lemma vector_sub_project_orthogonal: "(b::'a::ordered_field^'n) \ (x - ((b \ x) / (b\b)) *s b) = 0" +lemma vector_sub_project_orthogonal: "(b::'a::linordered_field^'n) \ (x - ((b \ x) / (b\b)) *s b) = 0" apply (cases "b = 0", simp) apply (simp add: dot_rsub dot_rmult) unfolding times_divide_eq_right[symmetric] diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Feb 08 11:13:30 2010 +0100 @@ -5696,27 +5696,27 @@ by (simp add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric]) lemma real_affinity_le: - "0 < (m::'a::ordered_field) ==> (m * x + c \ y \ x \ inverse(m) * y + -(c / m))" + "0 < (m::'a::linordered_field) ==> (m * x + c \ y \ x \ inverse(m) * y + -(c / m))" by (simp add: field_simps inverse_eq_divide) lemma real_le_affinity: - "0 < (m::'a::ordered_field) ==> (y \ m * x + c \ inverse(m) * y + -(c / m) \ x)" + "0 < (m::'a::linordered_field) ==> (y \ m * x + c \ inverse(m) * y + -(c / m) \ x)" by (simp add: field_simps inverse_eq_divide) lemma real_affinity_lt: - "0 < (m::'a::ordered_field) ==> (m * x + c < y \ x < inverse(m) * y + -(c / m))" + "0 < (m::'a::linordered_field) ==> (m * x + c < y \ x < inverse(m) * y + -(c / m))" by (simp add: field_simps inverse_eq_divide) lemma real_lt_affinity: - "0 < (m::'a::ordered_field) ==> (y < m * x + c \ inverse(m) * y + -(c / m) < x)" + "0 < (m::'a::linordered_field) ==> (y < m * x + c \ inverse(m) * y + -(c / m) < x)" by (simp add: field_simps inverse_eq_divide) lemma real_affinity_eq: - "(m::'a::ordered_field) \ 0 ==> (m * x + c = y \ x = inverse(m) * y + -(c / m))" + "(m::'a::linordered_field) \ 0 ==> (m * x + c = y \ x = inverse(m) * y + -(c / m))" by (simp add: field_simps inverse_eq_divide) lemma real_eq_affinity: - "(m::'a::ordered_field) \ 0 ==> (y = m * x + c \ inverse(m) * y + -(c / m) = x)" + "(m::'a::linordered_field) \ 0 ==> (y = m * x + c \ inverse(m) * y + -(c / m) = x)" by (simp add: field_simps inverse_eq_divide) lemma vector_affinity_eq: diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/NSA/HyperDef.thy --- a/src/HOL/NSA/HyperDef.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/NSA/HyperDef.thy Mon Feb 08 11:13:30 2010 +0100 @@ -459,7 +459,7 @@ by transfer (rule power_inverse) lemma hyperpow_hrabs: - "\r n. abs (r::'a::{ordered_idom} star) pow n = abs (r pow n)" + "\r n. abs (r::'a::{linordered_idom} star) pow n = abs (r pow n)" by transfer (rule power_abs [symmetric]) lemma hyperpow_add: @@ -475,15 +475,15 @@ by transfer simp lemma hyperpow_gt_zero: - "\r n. (0::'a::{ordered_semidom} star) < r \ 0 < r pow n" + "\r n. (0::'a::{linordered_semidom} star) < r \ 0 < r pow n" by transfer (rule zero_less_power) lemma hyperpow_ge_zero: - "\r n. (0::'a::{ordered_semidom} star) \ r \ 0 \ r pow n" + "\r n. (0::'a::{linordered_semidom} star) \ r \ 0 \ r pow n" by transfer (rule zero_le_power) lemma hyperpow_le: - "\x y n. \(0::'a::{ordered_semidom} star) < x; x \ y\ + "\x y n. \(0::'a::{linordered_semidom} star) < x; x \ y\ \ x pow n \ y pow n" by transfer (rule power_mono [OF _ order_less_imp_le]) @@ -492,7 +492,7 @@ by transfer (rule power_one) lemma hrabs_hyperpow_minus_one [simp]: - "\n. abs(-1 pow n) = (1::'a::{number_ring,ordered_idom} star)" + "\n. abs(-1 pow n) = (1::'a::{number_ring,linordered_idom} star)" by transfer (rule abs_power_minus_one) lemma hyperpow_mult: @@ -501,16 +501,16 @@ by transfer (rule power_mult_distrib) lemma hyperpow_two_le [simp]: - "(0::'a::{monoid_mult,ordered_ring_strict} star) \ r pow (1 + 1)" + "(0::'a::{monoid_mult,linlinordered_ring_strict} star) \ r pow (1 + 1)" by (auto simp add: hyperpow_two zero_le_mult_iff) lemma hrabs_hyperpow_two [simp]: "abs(x pow (1 + 1)) = - (x::'a::{monoid_mult,ordered_ring_strict} star) pow (1 + 1)" + (x::'a::{monoid_mult,linlinordered_ring_strict} star) pow (1 + 1)" by (simp only: abs_of_nonneg hyperpow_two_le) lemma hyperpow_two_hrabs [simp]: - "abs(x::'a::{ordered_idom} star) pow (1 + 1) = x pow (1 + 1)" + "abs(x::'a::{linordered_idom} star) pow (1 + 1) = x pow (1 + 1)" by (simp add: hyperpow_hrabs) text{*The precondition could be weakened to @{term "0\x"}*} @@ -519,11 +519,11 @@ by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) lemma hyperpow_two_gt_one: - "\r::'a::{ordered_semidom} star. 1 < r \ 1 < r pow (1 + 1)" + "\r::'a::{linordered_semidom} star. 1 < r \ 1 < r pow (1 + 1)" by transfer (simp add: power_gt1 del: power_Suc) lemma hyperpow_two_ge_one: - "\r::'a::{ordered_semidom} star. 1 \ r \ 1 \ r pow (1 + 1)" + "\r::'a::{linordered_semidom} star. 1 \ r \ 1 \ r pow (1 + 1)" by transfer (simp add: one_le_power del: power_Suc) lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \ 2 pow n" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/NSA/HyperNat.thy --- a/src/HOL/NSA/HyperNat.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/NSA/HyperNat.thy Mon Feb 08 11:13:30 2010 +0100 @@ -386,39 +386,39 @@ by transfer (rule of_nat_mult) lemma of_hypnat_less_iff [simp]: - "\m n. (of_hypnat m < (of_hypnat n::'a::ordered_semidom star)) = (m < n)" + "\m n. (of_hypnat m < (of_hypnat n::'a::linordered_semidom star)) = (m < n)" by transfer (rule of_nat_less_iff) lemma of_hypnat_0_less_iff [simp]: - "\n. (0 < (of_hypnat n::'a::ordered_semidom star)) = (0 < n)" + "\n. (0 < (of_hypnat n::'a::linordered_semidom star)) = (0 < n)" by transfer (rule of_nat_0_less_iff) lemma of_hypnat_less_0_iff [simp]: - "\m. \ (of_hypnat m::'a::ordered_semidom star) < 0" + "\m. \ (of_hypnat m::'a::linordered_semidom star) < 0" by transfer (rule of_nat_less_0_iff) lemma of_hypnat_le_iff [simp]: - "\m n. (of_hypnat m \ (of_hypnat n::'a::ordered_semidom star)) = (m \ n)" + "\m n. (of_hypnat m \ (of_hypnat n::'a::linordered_semidom star)) = (m \ n)" by transfer (rule of_nat_le_iff) lemma of_hypnat_0_le_iff [simp]: - "\n. 0 \ (of_hypnat n::'a::ordered_semidom star)" + "\n. 0 \ (of_hypnat n::'a::linordered_semidom star)" by transfer (rule of_nat_0_le_iff) lemma of_hypnat_le_0_iff [simp]: - "\m. ((of_hypnat m::'a::ordered_semidom star) \ 0) = (m = 0)" + "\m. ((of_hypnat m::'a::linordered_semidom star) \ 0) = (m = 0)" by transfer (rule of_nat_le_0_iff) lemma of_hypnat_eq_iff [simp]: - "\m n. (of_hypnat m = (of_hypnat n::'a::ordered_semidom star)) = (m = n)" + "\m n. (of_hypnat m = (of_hypnat n::'a::linordered_semidom star)) = (m = n)" by transfer (rule of_nat_eq_iff) lemma of_hypnat_eq_0_iff [simp]: - "\m. ((of_hypnat m::'a::ordered_semidom star) = 0) = (m = 0)" + "\m. ((of_hypnat m::'a::linordered_semidom star) = 0) = (m = 0)" by transfer (rule of_nat_eq_0_iff) lemma HNatInfinite_of_hypnat_gt_zero: - "N \ HNatInfinite \ (0::'a::ordered_semidom star) < of_hypnat N" + "N \ HNatInfinite \ (0::'a::linordered_semidom star) < of_hypnat N" by (rule ccontr, simp add: linorder_not_less) end diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/NSA/StarDef.thy Mon Feb 08 11:13:30 2010 +0100 @@ -719,7 +719,7 @@ apply (transfer, erule (1) order_antisym) done -instantiation star :: (lower_semilattice) lower_semilattice +instantiation star :: (semilattice_inf) semilattice_inf begin definition @@ -730,7 +730,7 @@ end -instantiation star :: (upper_semilattice) upper_semilattice +instantiation star :: (semilattice_sup) semilattice_sup begin definition @@ -833,27 +833,27 @@ apply (transfer, rule diff_minus) done -instance star :: (pordered_ab_semigroup_add) pordered_ab_semigroup_add +instance star :: (ordered_ab_semigroup_add) ordered_ab_semigroup_add by (intro_classes, transfer, rule add_left_mono) -instance star :: (pordered_cancel_ab_semigroup_add) pordered_cancel_ab_semigroup_add .. +instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add .. -instance star :: (pordered_ab_semigroup_add_imp_le) pordered_ab_semigroup_add_imp_le +instance star :: (ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le by (intro_classes, transfer, rule add_le_imp_le_left) -instance star :: (pordered_comm_monoid_add) pordered_comm_monoid_add .. -instance star :: (pordered_ab_group_add) pordered_ab_group_add .. +instance star :: (ordered_comm_monoid_add) ordered_comm_monoid_add .. +instance star :: (ordered_ab_group_add) ordered_ab_group_add .. -instance star :: (pordered_ab_group_add_abs) pordered_ab_group_add_abs +instance star :: (ordered_ab_group_add_abs) ordered_ab_group_add_abs by intro_classes (transfer, simp add: abs_ge_self abs_leI abs_triangle_ineq)+ -instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add .. -instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet .. -instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet .. -instance star :: (lordered_ab_group_add) lordered_ab_group_add .. +instance star :: (linordered_cancel_ab_semigroup_add) linordered_cancel_ab_semigroup_add .. +instance star :: (semilattice_inf_ab_group_add) semilattice_inf_ab_group_add .. +instance star :: (semilattice_inf_ab_group_add) semilattice_inf_ab_group_add .. +instance star :: (lattice_ab_group_add) lattice_ab_group_add .. -instance star :: (lordered_ab_group_add_abs) lordered_ab_group_add_abs +instance star :: (lattice_ab_group_add_abs) lattice_ab_group_add_abs by (intro_classes, transfer, rule abs_lattice) subsection {* Ring and field classes *} @@ -909,32 +909,32 @@ instance star :: (division_by_zero) division_by_zero by (intro_classes, transfer, rule inverse_zero) -instance star :: (pordered_semiring) pordered_semiring +instance star :: (ordered_semiring) ordered_semiring apply (intro_classes) apply (transfer, erule (1) mult_left_mono) apply (transfer, erule (1) mult_right_mono) done -instance star :: (pordered_cancel_semiring) pordered_cancel_semiring .. +instance star :: (ordered_cancel_semiring) ordered_cancel_semiring .. -instance star :: (ordered_semiring_strict) ordered_semiring_strict +instance star :: (linlinordered_semiring_strict) linlinordered_semiring_strict apply (intro_classes) apply (transfer, erule (1) mult_strict_left_mono) apply (transfer, erule (1) mult_strict_right_mono) done -instance star :: (pordered_comm_semiring) pordered_comm_semiring +instance star :: (ordered_comm_semiring) ordered_comm_semiring by (intro_classes, transfer, rule mult_mono1_class.mult_mono1) -instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring .. +instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring .. -instance star :: (ordered_comm_semiring_strict) ordered_comm_semiring_strict -by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.mult_strict_left_mono_comm) +instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict +by (intro_classes, transfer, rule mult_strict_left_mono_comm) -instance star :: (pordered_ring) pordered_ring .. -instance star :: (pordered_ring_abs) pordered_ring_abs +instance star :: (ordered_ring) ordered_ring .. +instance star :: (ordered_ring_abs) ordered_ring_abs by intro_classes (transfer, rule abs_eq_mult) -instance star :: (lordered_ring) lordered_ring .. +instance star :: (lattice_ring) lattice_ring .. instance star :: (abs_if) abs_if by (intro_classes, transfer, rule abs_if) @@ -942,14 +942,14 @@ instance star :: (sgn_if) sgn_if by (intro_classes, transfer, rule sgn_if) -instance star :: (ordered_ring_strict) ordered_ring_strict .. -instance star :: (pordered_comm_ring) pordered_comm_ring .. +instance star :: (linlinordered_ring_strict) linlinordered_ring_strict .. +instance star :: (ordered_comm_ring) ordered_comm_ring .. -instance star :: (ordered_semidom) ordered_semidom +instance star :: (linordered_semidom) linordered_semidom by (intro_classes, transfer, rule zero_less_one) -instance star :: (ordered_idom) ordered_idom .. -instance star :: (ordered_field) ordered_field .. +instance star :: (linordered_idom) linordered_idom .. +instance star :: (linordered_field) linordered_field .. subsection {* Power *} diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Nat.thy Mon Feb 08 11:13:30 2010 +0100 @@ -741,7 +741,7 @@ done text{*The naturals form an ordered @{text comm_semiring_1_cancel}*} -instance nat :: ordered_semidom +instance nat :: linordered_semidom proof fix i j k :: nat show "0 < (1::nat)" by simp @@ -1289,7 +1289,7 @@ end -context ordered_semidom +context linordered_semidom begin lemma zero_le_imp_of_nat: "0 \ of_nat m" @@ -1316,7 +1316,7 @@ lemma of_nat_le_iff [simp]: "of_nat m \ of_nat n \ m \ n" by (simp add: not_less [symmetric] linorder_not_less [symmetric]) -text{*Every @{text ordered_semidom} has characteristic zero.*} +text{*Every @{text linordered_semidom} has characteristic zero.*} subclass semiring_char_0 proof qed (simp add: eq_iff order_eq_iff) @@ -1345,7 +1345,7 @@ end -context ordered_idom +context linordered_idom begin lemma abs_of_nat [simp]: "\of_nat n\ = of_nat n" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Nat_Numeral.thy Mon Feb 08 11:13:30 2010 +0100 @@ -113,7 +113,7 @@ end -context ordered_ring_strict +context linlinordered_ring_strict begin lemma sum_squares_ge_zero: @@ -145,7 +145,7 @@ end -context ordered_semidom +context linordered_semidom begin lemma power2_le_imp_le: @@ -162,7 +162,7 @@ end -context ordered_idom +context linordered_idom begin lemma zero_eq_power2 [simp]: diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Nitpick.thy Mon Feb 08 11:13:30 2010 +0100 @@ -224,13 +224,13 @@ "Nitpick_Nut" so that they handle the unexpanded overloaded constants directly, but this is slightly more tricky to implement. *) lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int - div_nat_inst.div_nat div_nat_inst.mod_nat lower_semilattice_fun_inst.inf_fun + div_nat_inst.div_nat div_nat_inst.mod_nat semilattice_inf_fun_inst.inf_fun minus_fun_inst.minus_fun minus_int_inst.minus_int minus_nat_inst.minus_nat one_int_inst.one_int one_nat_inst.one_nat ord_fun_inst.less_eq_fun ord_int_inst.less_eq_int ord_int_inst.less_int ord_nat_inst.less_eq_nat ord_nat_inst.less_nat plus_int_inst.plus_int plus_nat_inst.plus_nat times_int_inst.times_int times_nat_inst.times_nat uminus_int_inst.uminus_int - upper_semilattice_fun_inst.sup_fun zero_int_inst.zero_int + semilattice_sup_fun_inst.sup_fun zero_int_inst.zero_int zero_nat_inst.zero_nat use "Tools/Nitpick/kodkod.ML" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/OrderedGroup.thy Mon Feb 08 11:13:30 2010 +0100 @@ -353,7 +353,7 @@ subsection {* (Partially) Ordered Groups *} -class pordered_ab_semigroup_add = order + ab_semigroup_add + +class ordered_ab_semigroup_add = order + ab_semigroup_add + assumes add_left_mono: "a \ b \ c + a \ c + b" begin @@ -370,8 +370,8 @@ end -class pordered_cancel_ab_semigroup_add = - pordered_ab_semigroup_add + cancel_ab_semigroup_add +class ordered_cancel_ab_semigroup_add = + ordered_ab_semigroup_add + cancel_ab_semigroup_add begin lemma add_strict_left_mono: @@ -403,8 +403,8 @@ end -class pordered_ab_semigroup_add_imp_le = - pordered_cancel_ab_semigroup_add + +class ordered_ab_semigroup_add_imp_le = + ordered_cancel_ab_semigroup_add + assumes add_le_imp_le_left: "c + a \ c + b \ a \ b" begin @@ -464,8 +464,8 @@ subsection {* Support for reasoning about signs *} -class pordered_comm_monoid_add = - pordered_cancel_ab_semigroup_add + comm_monoid_add +class ordered_comm_monoid_add = + ordered_cancel_ab_semigroup_add + comm_monoid_add begin lemma add_pos_nonneg: @@ -550,13 +550,13 @@ end -class pordered_ab_group_add = - ab_group_add + pordered_ab_semigroup_add +class ordered_ab_group_add = + ab_group_add + ordered_ab_semigroup_add begin -subclass pordered_cancel_ab_semigroup_add .. +subclass ordered_cancel_ab_semigroup_add .. -subclass pordered_ab_semigroup_add_imp_le +subclass ordered_ab_semigroup_add_imp_le proof fix a b c :: 'a assume "c + a \ c + b" @@ -565,7 +565,7 @@ thus "a \ b" by simp qed -subclass pordered_comm_monoid_add .. +subclass ordered_comm_monoid_add .. lemma max_diff_distrib_left: shows "max x y - z = max (x - z) (y - z)" @@ -675,16 +675,16 @@ text{*Legacy - use @{text algebra_simps} *} lemmas group_simps[noatp] = algebra_simps -class ordered_ab_semigroup_add = - linorder + pordered_ab_semigroup_add +class linordered_ab_semigroup_add = + linorder + ordered_ab_semigroup_add -class ordered_cancel_ab_semigroup_add = - linorder + pordered_cancel_ab_semigroup_add +class linordered_cancel_ab_semigroup_add = + linorder + ordered_cancel_ab_semigroup_add begin -subclass ordered_ab_semigroup_add .. +subclass linordered_ab_semigroup_add .. -subclass pordered_ab_semigroup_add_imp_le +subclass ordered_ab_semigroup_add_imp_le proof fix a b c :: 'a assume le: "c + a <= c + b" @@ -705,11 +705,10 @@ end -class ordered_ab_group_add = - linorder + pordered_ab_group_add +class linordered_ab_group_add = linorder + ordered_ab_group_add begin -subclass ordered_cancel_ab_semigroup_add .. +subclass linordered_cancel_ab_semigroup_add .. lemma neg_less_eq_nonneg: "- a \ a \ 0 \ a" @@ -775,27 +774,27 @@ -- {* FIXME localize the following *} lemma add_increasing: - fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}" + fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" shows "[|0\a; b\c|] ==> b \ a + c" by (insert add_mono [of 0 a b c], simp) lemma add_increasing2: - fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}" + fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" shows "[|0\c; b\a|] ==> b \ a + c" by (simp add:add_increasing add_commute[of a]) lemma add_strict_increasing: - fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}" + fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" shows "[|0c|] ==> b < a + c" by (insert add_less_le_mono [of 0 a b c], simp) lemma add_strict_increasing2: - fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}" + fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" shows "[|0\a; b b < a + c" by (insert add_le_less_mono [of 0 a b c], simp) -class pordered_ab_group_add_abs = pordered_ab_group_add + abs + +class ordered_ab_group_add_abs = ordered_ab_group_add + abs + assumes abs_ge_zero [simp]: "\a\ \ 0" and abs_ge_self: "a \ \a\" and abs_leI: "a \ b \ - a \ b \ \a\ \ b" @@ -945,7 +944,7 @@ subsection {* Lattice Ordered (Abelian) Groups *} -class lordered_ab_group_add_meet = pordered_ab_group_add + lower_semilattice +class semilattice_inf_ab_group_add = ordered_ab_group_add + semilattice_inf begin lemma add_inf_distrib_left: @@ -967,7 +966,7 @@ end -class lordered_ab_group_add_join = pordered_ab_group_add + upper_semilattice +class semilattice_sup_ab_group_add = ordered_ab_group_add + semilattice_sup begin lemma add_sup_distrib_left: @@ -990,11 +989,11 @@ end -class lordered_ab_group_add = pordered_ab_group_add + lattice +class lattice_ab_group_add = ordered_ab_group_add + lattice begin -subclass lordered_ab_group_add_meet .. -subclass lordered_ab_group_add_join .. +subclass semilattice_inf_ab_group_add .. +subclass semilattice_sup_ab_group_add .. lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left @@ -1244,7 +1243,7 @@ lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left -class lordered_ab_group_add_abs = lordered_ab_group_add + abs + +class lattice_ab_group_add_abs = lattice_ab_group_add + abs + assumes abs_lattice: "\a\ = sup a (- a)" begin @@ -1262,7 +1261,7 @@ pprt_def nprt_def diff_minus abs_lattice) qed -subclass pordered_ab_group_add_abs +subclass ordered_ab_group_add_abs proof have abs_ge_zero [simp]: "\a. 0 \ \a\" proof - @@ -1297,7 +1296,7 @@ end lemma sup_eq_if: - fixes a :: "'a\{lordered_ab_group_add, linorder}" + fixes a :: "'a\{lattice_ab_group_add, linorder}" shows "sup a (- a) = (if a < 0 then - a else a)" proof - note add_le_cancel_right [of a a "- a", symmetric, simplified] @@ -1306,7 +1305,7 @@ qed lemma abs_if_lattice: - fixes a :: "'a\{lordered_ab_group_add_abs, linorder}" + fixes a :: "'a\{lattice_ab_group_add_abs, linorder}" shows "\a\ = (if a < 0 then - a else a)" by auto @@ -1324,10 +1323,10 @@ apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified]) done -lemma less_eqI: "(x::'a::pordered_ab_group_add) - y = x' - y' \ (x < y) = (x' < y')" +lemma less_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \ (x < y) = (x' < y')" by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y']) -lemma le_eqI: "(x::'a::pordered_ab_group_add) - y = x' - y' \ (y <= x) = (y' <= x')" +lemma le_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \ (y <= x) = (y' <= x')" apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of y' x']) apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0]) done @@ -1340,7 +1339,7 @@ lemma le_add_right_mono: assumes - "a <= b + (c::'a::pordered_ab_group_add)" + "a <= b + (c::'a::ordered_ab_group_add)" "c <= d" shows "a <= b + d" apply (rule_tac order_trans[where y = "b+c"]) @@ -1348,7 +1347,7 @@ done lemma estimate_by_abs: - "a + b <= (c::'a::lordered_ab_group_add_abs) \ a <= c + abs b" + "a + b <= (c::'a::lattice_ab_group_add_abs) \ a <= c + abs b" proof - assume "a+b <= c" hence 2: "a <= c+(-b)" by (simp add: algebra_simps) @@ -1358,16 +1357,16 @@ subsection {* Tools setup *} -lemma add_mono_thms_ordered_semiring [noatp]: - fixes i j k :: "'a\pordered_ab_semigroup_add" +lemma add_mono_thms_linordered_semiring [noatp]: + fixes i j k :: "'a\ordered_ab_semigroup_add" shows "i \ j \ k \ l \ i + k \ j + l" and "i = j \ k \ l \ i + k \ j + l" and "i \ j \ k = l \ i + k \ j + l" and "i = j \ k = l \ i + k = j + l" by (rule add_mono, clarify+)+ -lemma add_mono_thms_ordered_field [noatp]: - fixes i j k :: "'a\pordered_cancel_ab_semigroup_add" +lemma add_mono_thms_linordered_field [noatp]: + fixes i j k :: "'a\ordered_cancel_ab_semigroup_add" shows "i < j \ k = l \ i + k < j + l" and "i = j \ k < l \ i + k < j + l" and "i < j \ k \ l \ i + k < j + l" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Orderings.thy Mon Feb 08 11:13:30 2010 +0100 @@ -1052,7 +1052,7 @@ subsection {* Dense orders *} -class dense_linear_order = linorder + +class dense_linorder = linorder + assumes gt_ex: "\y. x < y" and lt_ex: "\y. y < x" and dense: "x < y \ (\z. x < z \ z < y)" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/PReal.thy --- a/src/HOL/PReal.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/PReal.thy Mon Feb 08 11:13:30 2010 +0100 @@ -23,7 +23,7 @@ (\y \ A. ((\z. 0 z \ A) & (\u \ A. y < u))))" lemma interval_empty_iff: - "{y. (x::'a::dense_linear_order) < y \ y < z} = {} \ \ x < z" + "{y. (x::'a::dense_linorder) < y \ y < z} = {} \ \ x < z" by (auto dest: dense) @@ -1155,7 +1155,7 @@ preal_add_le_cancel_right preal_add_le_cancel_left preal_add_left_cancel_iff preal_add_right_cancel_iff -instance preal :: ordered_cancel_ab_semigroup_add +instance preal :: linordered_cancel_ab_semigroup_add proof fix a b c :: preal show "a + b = a + c \ b = c" by (rule preal_add_left_cancel) diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Parity.thy --- a/src/HOL/Parity.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Parity.thy Mon Feb 08 11:13:30 2010 +0100 @@ -218,7 +218,7 @@ done lemma zero_le_even_power: "even n ==> - 0 <= (x::'a::{ordered_ring_strict,monoid_mult}) ^ n" + 0 <= (x::'a::{linlinordered_ring_strict,monoid_mult}) ^ n" apply (simp add: even_nat_equiv_def2) apply (erule exE) apply (erule ssubst) @@ -227,12 +227,12 @@ done lemma zero_le_odd_power: "odd n ==> - (0 <= (x::'a::{ordered_idom}) ^ n) = (0 <= x)" + (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)" apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff) apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square) done -lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{ordered_idom}) ^ n) = +lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) = (even n | (odd n & 0 <= x))" apply auto apply (subst zero_le_odd_power [symmetric]) @@ -240,19 +240,19 @@ apply (erule zero_le_even_power) done -lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{ordered_idom}) ^ n) = +lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{linordered_idom}) ^ n) = (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" unfolding order_less_le zero_le_power_eq by auto -lemma power_less_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n < 0) = +lemma power_less_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n < 0) = (odd n & x < 0)" apply (subst linorder_not_le [symmetric])+ apply (subst zero_le_power_eq) apply auto done -lemma power_le_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n <= 0) = +lemma power_le_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n <= 0) = (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))" apply (subst linorder_not_less [symmetric])+ apply (subst zero_less_power_eq) @@ -260,7 +260,7 @@ done lemma power_even_abs: "even n ==> - (abs (x::'a::{ordered_idom}))^n = x^n" + (abs (x::'a::{linordered_idom}))^n = x^n" apply (subst power_abs [symmetric]) apply (simp add: zero_le_even_power) done @@ -280,7 +280,7 @@ apply simp done -lemma power_mono_even: fixes x y :: "'a :: {ordered_idom}" +lemma power_mono_even: fixes x y :: "'a :: {linordered_idom}" assumes "even n" and "\x\ \ \y\" shows "x^n \ y^n" proof - @@ -292,7 +292,7 @@ lemma odd_pos: "odd (n::nat) \ 0 < n" by presburger -lemma power_mono_odd: fixes x y :: "'a :: {ordered_idom}" +lemma power_mono_odd: fixes x y :: "'a :: {linordered_idom}" assumes "odd n" and "x \ y" shows "x^n \ y^n" proof (cases "y < 0") @@ -372,11 +372,11 @@ subsection {* An Equivalence for @{term [source] "0 \ a^n"} *} lemma even_power_le_0_imp_0: - "a ^ (2*k) \ (0::'a::{ordered_idom}) ==> a=0" + "a ^ (2*k) \ (0::'a::{linordered_idom}) ==> a=0" by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) lemma zero_le_power_iff[presburger]: - "(0 \ a^n) = (0 \ (a::'a::{ordered_idom}) | even n)" + "(0 \ a^n) = (0 \ (a::'a::{linordered_idom}) | even n)" proof cases assume even: "even n" then obtain k where "n = 2*k" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Power.thy --- a/src/HOL/Power.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Power.thy Mon Feb 08 11:13:30 2010 +0100 @@ -130,7 +130,7 @@ end -context ordered_semidom +context linordered_semidom begin lemma zero_less_power [simp]: @@ -323,7 +323,7 @@ end -context ordered_idom +context linordered_idom begin lemma power_abs: diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Probability/Borel.thy --- a/src/HOL/Probability/Borel.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Probability/Borel.thy Mon Feb 08 11:13:30 2010 +0100 @@ -73,7 +73,7 @@ with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)" by (metis lessI order_le_less_trans real_natceiling_ge real_of_nat_less_iff) hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < inverse(inverse(g w - f w))" - by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_ordered_idom nz positive_imp_inverse_positive real_le_antisym real_less_def w) + by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_linordered_idom nz positive_imp_inverse_positive real_le_antisym real_less_def w) hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w" by (metis inverse_inverse_eq order_less_le_trans real_le_refl) thus "\n. f w \ g w - inverse(real(Suc n))" using w diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Quickcheck.thy Mon Feb 08 11:13:30 2010 +0100 @@ -164,7 +164,7 @@ where "union R1 R2 = (\s. let (P1, s') = R1 s; (P2, s'') = R2 s' - in (upper_semilattice_class.sup P1 P2, s''))" + in (semilattice_sup_class.sup P1 P2, s''))" definition if_randompred :: "bool \ unit randompred" where diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/RComplete.thy --- a/src/HOL/RComplete.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/RComplete.thy Mon Feb 08 11:13:30 2010 +0100 @@ -15,7 +15,7 @@ by simp lemma abs_diff_less_iff: - "(\x - a\ < (r::'a::ordered_idom)) = (a - r < x \ x < a + r)" + "(\x - a\ < (r::'a::linordered_idom)) = (a - r < x \ x < a + r)" by auto subsection {* Completeness of Positive Reals *} diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Rational.thy --- a/src/HOL/Rational.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Rational.thy Mon Feb 08 11:13:30 2010 +0100 @@ -613,7 +613,7 @@ end -instance rat :: ordered_field +instance rat :: linordered_field proof fix q r s :: rat show "q \ r ==> s + q \ s + r" @@ -760,7 +760,7 @@ class field_char_0 = field + ring_char_0 -subclass (in ordered_field) field_char_0 .. +subclass (in linordered_field) field_char_0 .. context field_char_0 begin @@ -832,7 +832,7 @@ done lemma of_rat_less: - "(of_rat r :: 'a::ordered_field) < of_rat s \ r < s" + "(of_rat r :: 'a::linordered_field) < of_rat s \ r < s" proof (induct r, induct s) fix a b c d :: int assume not_zero: "b > 0" "d > 0" @@ -841,14 +841,14 @@ "(of_int a :: 'a) / of_int b < of_int c / of_int d \ (of_int a :: 'a) * of_int d < of_int c * of_int b" using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq) - show "(of_rat (Fract a b) :: 'a::ordered_field) < of_rat (Fract c d) + show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d) \ Fract a b < Fract c d" using not_zero `b * d > 0` by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult) qed lemma of_rat_less_eq: - "(of_rat r :: 'a::ordered_field) \ of_rat s \ r \ s" + "(of_rat r :: 'a::linordered_field) \ of_rat s \ r \ s" unfolding le_less by (auto simp add: of_rat_less) lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified] @@ -1083,11 +1083,11 @@ finally show ?thesis using assms by simp qed -lemma (in ordered_idom) sgn_greater [simp]: +lemma (in linordered_idom) sgn_greater [simp]: "0 < sgn a \ 0 < a" unfolding sgn_if by auto -lemma (in ordered_idom) sgn_less [simp]: +lemma (in linordered_idom) sgn_less [simp]: "sgn a < 0 \ a < 0" unfolding sgn_if by auto diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Real.thy --- a/src/HOL/Real.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Real.thy Mon Feb 08 11:13:30 2010 +0100 @@ -3,7 +3,7 @@ begin lemma field_le_epsilon: - fixes x y :: "'a:: {number_ring,division_by_zero,ordered_field}" + fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}" assumes e: "(!!e. 0 < e ==> x \ y + e)" shows "x \ y" proof (rule ccontr) diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/RealDef.thy Mon Feb 08 11:13:30 2010 +0100 @@ -416,7 +416,7 @@ subsection{*The Reals Form an Ordered Field*} -instance real :: ordered_field +instance real :: linordered_field proof fix x y z :: real show "x \ y ==> z + x \ z + y" by (rule real_add_left_mono) @@ -426,7 +426,7 @@ by (simp only: real_sgn_def) qed -instance real :: lordered_ab_group_add .. +instance real :: lattice_ab_group_add .. text{*The function @{term real_of_preal} requires many proofs, but it seems to be essential for proving completeness of the reals from that of the @@ -1046,7 +1046,7 @@ lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \ abs(x + -l) + abs(y + -m)" by simp -instance real :: lordered_ring +instance real :: lattice_ring proof fix a::real show "abs a = sup a (-a)" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Ring_and_Field.thy Mon Feb 08 11:13:30 2010 +0100 @@ -706,7 +706,7 @@ assumes mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b" assumes mult_right_mono: "a \ b \ 0 \ c \ a * c \ b * c" -class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add +class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add begin lemma mult_mono: @@ -725,12 +725,12 @@ end -class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add +class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add + semiring + cancel_comm_monoid_add begin subclass semiring_0_cancel .. -subclass pordered_semiring .. +subclass ordered_semiring .. lemma mult_nonneg_nonneg: "0 \ a \ 0 \ b \ 0 \ a * b" using mult_left_mono [of zero b a] by simp @@ -750,12 +750,12 @@ end -class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono +class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono begin -subclass pordered_cancel_semiring .. - -subclass pordered_comm_monoid_add .. +subclass ordered_cancel_semiring .. + +subclass ordered_comm_monoid_add .. lemma mult_left_less_imp_less: "c * a < c * b \ 0 \ c \ a < b" @@ -767,16 +767,16 @@ end -class ordered_semiring_1 = ordered_semiring + semiring_1 - -class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + +class linlinordered_semiring_1 = linordered_semiring + semiring_1 + +class linlinordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + assumes mult_strict_left_mono: "a < b \ 0 < c \ c * a < c * b" assumes mult_strict_right_mono: "a < b \ 0 < c \ a * c < b * c" begin subclass semiring_0_cancel .. -subclass ordered_semiring +subclass linordered_semiring proof fix a b c :: 'a assume A: "a \ b" "0 \ c" @@ -886,16 +886,16 @@ end -class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1 +class linlinlinordered_semiring_1_strict = linlinordered_semiring_strict + semiring_1 class mult_mono1 = times + zero + ord + assumes mult_mono1: "a \ b \ 0 \ c \ c * a \ c * b" -class pordered_comm_semiring = comm_semiring_0 - + pordered_ab_semigroup_add + mult_mono1 +class ordered_comm_semiring = comm_semiring_0 + + ordered_ab_semigroup_add + mult_mono1 begin -subclass pordered_semiring +subclass ordered_semiring proof fix a b c :: 'a assume "a \ b" "0 \ c" @@ -905,20 +905,20 @@ end -class pordered_cancel_comm_semiring = comm_semiring_0_cancel - + pordered_ab_semigroup_add + mult_mono1 +class ordered_cancel_comm_semiring = comm_semiring_0_cancel + + ordered_ab_semigroup_add + mult_mono1 begin -subclass pordered_comm_semiring .. -subclass pordered_cancel_semiring .. +subclass ordered_comm_semiring .. +subclass ordered_cancel_semiring .. end -class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add + +class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add + assumes mult_strict_left_mono_comm: "a < b \ 0 < c \ c * a < c * b" begin -subclass ordered_semiring_strict +subclass linlinordered_semiring_strict proof fix a b c :: 'a assume "a < b" "0 < c" @@ -926,7 +926,7 @@ thus "a * c < b * c" by (simp only: mult_commute) qed -subclass pordered_cancel_comm_semiring +subclass ordered_cancel_comm_semiring proof fix a b c :: 'a assume "a \ b" "0 \ c" @@ -937,10 +937,10 @@ end -class pordered_ring = ring + pordered_cancel_semiring +class ordered_ring = ring + ordered_cancel_semiring begin -subclass pordered_ab_group_add .. +subclass ordered_ab_group_add .. text{*Legacy - use @{text algebra_simps} *} lemmas ring_simps[noatp] = algebra_simps @@ -991,32 +991,31 @@ lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0" by(simp add:sgn_if) -class ordered_ring = ring + ordered_semiring - + ordered_ab_group_add + abs_if +class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if begin -subclass pordered_ring .. - -subclass pordered_ab_group_add_abs +subclass ordered_ring .. + +subclass ordered_ab_group_add_abs proof fix a b show "\a + b\ \ \a\ + \b\" -by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos) - (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric] + by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos) + (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric] neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg) qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero) end -(* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors. - Basically, ordered_ring + no_zero_divisors = ordered_ring_strict. +(* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors. + Basically, linordered_ring + no_zero_divisors = linlinordered_ring_strict. *) -class ordered_ring_strict = ring + ordered_semiring_strict +class linlinordered_ring_strict = ring + linlinordered_semiring_strict + ordered_ab_group_add + abs_if begin -subclass ordered_ring .. +subclass linordered_ring .. lemma mult_strict_left_mono_neg: "b < a \ c < 0 \ c * a < c * b" using mult_strict_left_mono [of b a "- c"] by simp @@ -1168,16 +1167,16 @@ mult_pos_pos mult_pos_neg mult_neg_pos mult_neg_neg -class pordered_comm_ring = comm_ring + pordered_comm_semiring +class ordered_comm_ring = comm_ring + ordered_comm_semiring begin -subclass pordered_ring .. -subclass pordered_cancel_comm_semiring .. +subclass ordered_ring .. +subclass ordered_cancel_comm_semiring .. end -class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict + - (*previously ordered_semiring*) +class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict + + (*previously linordered_semiring*) assumes zero_less_one [simp]: "0 < 1" begin @@ -1202,23 +1201,23 @@ end -class ordered_idom = comm_ring_1 + - ordered_comm_semiring_strict + ordered_ab_group_add + +class linordered_idom = comm_ring_1 + + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn_if - (*previously ordered_ring*) + (*previously linordered_ring*) begin -subclass ordered_ring_strict .. -subclass pordered_comm_ring .. +subclass linlinordered_ring_strict .. +subclass ordered_comm_ring .. subclass idom .. -subclass ordered_semidom +subclass linordered_semidom proof have "0 \ 1 * 1" by (rule zero_le_square) thus "0 < 1" by (simp add: le_less) qed -lemma linorder_neqE_ordered_idom: +lemma linorder_neqE_linordered_idom: assumes "x \ y" obtains "x < y" | "y < x" using assms by (rule neqE) @@ -1307,7 +1306,7 @@ end -class ordered_field = field + ordered_idom +class linordered_field = field + linordered_idom text {* Simprules for comparisons where common factors can be cancelled. *} @@ -1437,7 +1436,7 @@ subsection {* Ordered Fields *} lemma positive_imp_inverse_positive: -assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::ordered_field)" +assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::linordered_field)" proof - have "0 < a * inverse a" by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one) @@ -1446,13 +1445,13 @@ qed lemma negative_imp_inverse_negative: - "a < 0 ==> inverse a < (0::'a::ordered_field)" + "a < 0 ==> inverse a < (0::'a::linordered_field)" by (insert positive_imp_inverse_positive [of "-a"], simp add: nonzero_inverse_minus_eq order_less_imp_not_eq) lemma inverse_le_imp_le: assumes invle: "inverse a \ inverse b" and apos: "0 < a" -shows "b \ (a::'a::ordered_field)" +shows "b \ (a::'a::linordered_field)" proof (rule classical) assume "~ b \ a" hence "a < b" by (simp add: linorder_not_le) @@ -1466,7 +1465,7 @@ lemma inverse_positive_imp_positive: assumes inv_gt_0: "0 < inverse a" and nz: "a \ 0" -shows "0 < (a::'a::ordered_field)" +shows "0 < (a::'a::linordered_field)" proof - have "0 < inverse (inverse a)" using inv_gt_0 by (rule positive_imp_inverse_positive) @@ -1475,14 +1474,14 @@ qed lemma inverse_positive_iff_positive [simp]: - "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))" + "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_by_zero}))" apply (cases "a = 0", simp) apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive) done lemma inverse_negative_imp_negative: assumes inv_less_0: "inverse a < 0" and nz: "a \ 0" -shows "a < (0::'a::ordered_field)" +shows "a < (0::'a::linordered_field)" proof - have "inverse (inverse a) < 0" using inv_less_0 by (rule negative_imp_inverse_negative) @@ -1490,20 +1489,20 @@ qed lemma inverse_negative_iff_negative [simp]: - "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))" + "(inverse a < 0) = (a < (0::'a::{linordered_field,division_by_zero}))" apply (cases "a = 0", simp) apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative) done lemma inverse_nonnegative_iff_nonnegative [simp]: - "(0 \ inverse a) = (0 \ (a::'a::{ordered_field,division_by_zero}))" + "(0 \ inverse a) = (0 \ (a::'a::{linordered_field,division_by_zero}))" by (simp add: linorder_not_less [symmetric]) lemma inverse_nonpositive_iff_nonpositive [simp]: - "(inverse a \ 0) = (a \ (0::'a::{ordered_field,division_by_zero}))" + "(inverse a \ 0) = (a \ (0::'a::{linordered_field,division_by_zero}))" by (simp add: linorder_not_less [symmetric]) -lemma ordered_field_no_lb: "\ x. \y. y < (x::'a::ordered_field)" +lemma linlinordered_field_no_lb: "\ x. \y. y < (x::'a::linordered_field)" proof fix x::'a have m1: "- (1::'a) < 0" by simp @@ -1512,7 +1511,7 @@ thus "\y. y < x" by blast qed -lemma ordered_field_no_ub: "\ x. \y. y > (x::'a::ordered_field)" +lemma linlinordered_field_no_ub: "\ x. \y. y > (x::'a::linordered_field)" proof fix x::'a have m1: " (1::'a) > 0" by simp @@ -1525,7 +1524,7 @@ lemma less_imp_inverse_less: assumes less: "a < b" and apos: "0 < a" -shows "inverse b < inverse (a::'a::ordered_field)" +shows "inverse b < inverse (a::'a::linordered_field)" proof (rule ccontr) assume "~ inverse b < inverse a" hence "inverse a \ inverse b" by (simp add: linorder_not_less) @@ -1535,29 +1534,29 @@ qed lemma inverse_less_imp_less: - "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)" + "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::linordered_field)" apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"]) apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) done text{*Both premises are essential. Consider -1 and 1.*} lemma inverse_less_iff_less [simp,noatp]: - "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))" + "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))" by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) lemma le_imp_inverse_le: - "[|a \ b; 0 < a|] ==> inverse b \ inverse (a::'a::ordered_field)" + "[|a \ b; 0 < a|] ==> inverse b \ inverse (a::'a::linordered_field)" by (force simp add: order_le_less less_imp_inverse_less) lemma inverse_le_iff_le [simp,noatp]: - "[|0 < a; 0 < b|] ==> (inverse a \ inverse b) = (b \ (a::'a::ordered_field))" + "[|0 < a; 0 < b|] ==> (inverse a \ inverse b) = (b \ (a::'a::linordered_field))" by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) text{*These results refer to both operands being negative. The opposite-sign case is trivial, since inverse preserves signs.*} lemma inverse_le_imp_le_neg: - "[|inverse a \ inverse b; b < 0|] ==> b \ (a::'a::ordered_field)" + "[|inverse a \ inverse b; b < 0|] ==> b \ (a::'a::linordered_field)" apply (rule classical) apply (subgoal_tac "a < 0") prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) @@ -1566,7 +1565,7 @@ done lemma less_imp_inverse_less_neg: - "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)" + "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::linordered_field)" apply (subgoal_tac "a < 0") prefer 2 apply (blast intro: order_less_trans) apply (insert less_imp_inverse_less [of "-b" "-a"]) @@ -1574,7 +1573,7 @@ done lemma inverse_less_imp_less_neg: - "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)" + "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::linordered_field)" apply (rule classical) apply (subgoal_tac "a < 0") prefer 2 @@ -1584,25 +1583,25 @@ done lemma inverse_less_iff_less_neg [simp,noatp]: - "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))" + "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))" apply (insert inverse_less_iff_less [of "-b" "-a"]) apply (simp del: inverse_less_iff_less add: order_less_imp_not_eq nonzero_inverse_minus_eq) done lemma le_imp_inverse_le_neg: - "[|a \ b; b < 0|] ==> inverse b \ inverse (a::'a::ordered_field)" + "[|a \ b; b < 0|] ==> inverse b \ inverse (a::'a::linordered_field)" by (force simp add: order_le_less less_imp_inverse_less_neg) lemma inverse_le_iff_le_neg [simp,noatp]: - "[|a < 0; b < 0|] ==> (inverse a \ inverse b) = (b \ (a::'a::ordered_field))" + "[|a < 0; b < 0|] ==> (inverse a \ inverse b) = (b \ (a::'a::linordered_field))" by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) subsection{*Inverses and the Number One*} lemma one_less_inverse_iff: - "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))" + "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_by_zero}))" proof cases assume "0 < x" with inverse_less_iff_less [OF zero_less_one, of x] @@ -1624,22 +1623,22 @@ by (insert inverse_eq_iff_eq [of x 1], simp) lemma one_le_inverse_iff: - "(1 \ inverse x) = (0 < x & x \ (1::'a::{ordered_field,division_by_zero}))" + "(1 \ inverse x) = (0 < x & x \ (1::'a::{linordered_field,division_by_zero}))" by (force simp add: order_le_less one_less_inverse_iff zero_less_one eq_commute [of 1]) lemma inverse_less_1_iff: - "(inverse x < 1) = (x \ 0 | 1 < (x::'a::{ordered_field,division_by_zero}))" + "(inverse x < 1) = (x \ 0 | 1 < (x::'a::{linordered_field,division_by_zero}))" by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) lemma inverse_le_1_iff: - "(inverse x \ 1) = (x \ 0 | 1 \ (x::'a::{ordered_field,division_by_zero}))" + "(inverse x \ 1) = (x \ 0 | 1 \ (x::'a::{linordered_field,division_by_zero}))" by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) subsection{*Simplification of Inequalities Involving Literal Divisors*} -lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \ b/c) = (a*c \ b)" +lemma pos_le_divide_eq: "0 < (c::'a::linordered_field) ==> (a \ b/c) = (a*c \ b)" proof - assume less: "0 b/c) = (a*c \ (b/c)*c)" @@ -1649,7 +1648,7 @@ finally show ?thesis . qed -lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \ b/c) = (b \ a*c)" +lemma neg_le_divide_eq: "c < (0::'a::linordered_field) ==> (a \ b/c) = (b \ a*c)" proof - assume less: "c<0" hence "(a \ b/c) = ((b/c)*c \ a*c)" @@ -1663,12 +1662,12 @@ "(a \ b/c) = (if 0 < c then a*c \ b else if c < 0 then b \ a*c - else a \ (0::'a::{ordered_field,division_by_zero}))" + else a \ (0::'a::{linordered_field,division_by_zero}))" apply (cases "c=0", simp) apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) done -lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \ a) = (b \ a*c)" +lemma pos_divide_le_eq: "0 < (c::'a::linordered_field) ==> (b/c \ a) = (b \ a*c)" proof - assume less: "0 a) = ((b/c)*c \ a*c)" @@ -1678,7 +1677,7 @@ finally show ?thesis . qed -lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \ a) = (a*c \ b)" +lemma neg_divide_le_eq: "c < (0::'a::linordered_field) ==> (b/c \ a) = (a*c \ b)" proof - assume less: "c<0" hence "(b/c \ a) = (a*c \ (b/c)*c)" @@ -1692,13 +1691,13 @@ "(b/c \ a) = (if 0 < c then b \ a*c else if c < 0 then a*c \ b - else 0 \ (a::'a::{ordered_field,division_by_zero}))" + else 0 \ (a::'a::{linordered_field,division_by_zero}))" apply (cases "c=0", simp) apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) done lemma pos_less_divide_eq: - "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)" + "0 < (c::'a::linordered_field) ==> (a < b/c) = (a*c < b)" proof - assume less: "0 (a < b/c) = (b < a*c)" + "c < (0::'a::linordered_field) ==> (a < b/c) = (b < a*c)" proof - assume less: "c<0" hence "(a < b/c) = ((b/c)*c < a*c)" @@ -1723,13 +1722,13 @@ "(a < b/c) = (if 0 < c then a*c < b else if c < 0 then b < a*c - else a < (0::'a::{ordered_field,division_by_zero}))" + else a < (0::'a::{linordered_field,division_by_zero}))" apply (cases "c=0", simp) apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) done lemma pos_divide_less_eq: - "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)" + "0 < (c::'a::linordered_field) ==> (b/c < a) = (b < a*c)" proof - assume less: "0 (b/c < a) = (a*c < b)" + "c < (0::'a::linordered_field) ==> (b/c < a) = (a*c < b)" proof - assume less: "c<0" hence "(b/c < a) = (a*c < (b/c)*c)" @@ -1754,7 +1753,7 @@ "(b/c < a) = (if 0 < c then b < a*c else if c < 0 then a*c < b - else 0 < (a::'a::{ordered_field,division_by_zero}))" + else 0 < (a::'a::{linordered_field,division_by_zero}))" apply (cases "c=0", simp) apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) done @@ -1784,7 +1783,7 @@ (* Only works once linear arithmetic is installed: text{*An example:*} -lemma fixes a b c d e f :: "'a::ordered_field" +lemma fixes a b c d e f :: "'a::linordered_field" shows "\a>b; c \ ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) < ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u" @@ -1800,21 +1799,21 @@ subsection{*Division and Signs*} lemma zero_less_divide_iff: - "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)" + "((0::'a::{linordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)" by (simp add: divide_inverse zero_less_mult_iff) lemma divide_less_0_iff: - "(a/b < (0::'a::{ordered_field,division_by_zero})) = + "(a/b < (0::'a::{linordered_field,division_by_zero})) = (0 < a & b < 0 | a < 0 & 0 < b)" by (simp add: divide_inverse mult_less_0_iff) lemma zero_le_divide_iff: - "((0::'a::{ordered_field,division_by_zero}) \ a/b) = + "((0::'a::{linordered_field,division_by_zero}) \ a/b) = (0 \ a & 0 \ b | a \ 0 & b \ 0)" by (simp add: divide_inverse zero_le_mult_iff) lemma divide_le_0_iff: - "(a/b \ (0::'a::{ordered_field,division_by_zero})) = + "(a/b \ (0::'a::{linordered_field,division_by_zero})) = (0 \ a & b \ 0 | a \ 0 & 0 \ b)" by (simp add: divide_inverse mult_le_0_iff) @@ -1823,36 +1822,36 @@ by (simp add: divide_inverse) lemma divide_pos_pos: - "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y" + "0 < (x::'a::linordered_field) ==> 0 < y ==> 0 < x / y" by(simp add:field_simps) lemma divide_nonneg_pos: - "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y" + "0 <= (x::'a::linordered_field) ==> 0 < y ==> 0 <= x / y" by(simp add:field_simps) lemma divide_neg_pos: - "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0" + "(x::'a::linordered_field) < 0 ==> 0 < y ==> x / y < 0" by(simp add:field_simps) lemma divide_nonpos_pos: - "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0" + "(x::'a::linordered_field) <= 0 ==> 0 < y ==> x / y <= 0" by(simp add:field_simps) lemma divide_pos_neg: - "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0" + "0 < (x::'a::linordered_field) ==> y < 0 ==> x / y < 0" by(simp add:field_simps) lemma divide_nonneg_neg: - "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0" + "0 <= (x::'a::linordered_field) ==> y < 0 ==> x / y <= 0" by(simp add:field_simps) lemma divide_neg_neg: - "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y" + "(x::'a::linordered_field) < 0 ==> y < 0 ==> 0 < x / y" by(simp add:field_simps) lemma divide_nonpos_neg: - "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y" + "(x::'a::linordered_field) <= 0 ==> y < 0 ==> 0 <= x / y" by(simp add:field_simps) @@ -1885,13 +1884,13 @@ by (simp add: eq_commute [of 1]) lemma zero_eq_1_divide_iff [simp,noatp]: - "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)" + "((0::'a::{linordered_field,division_by_zero}) = 1/a) = (a = 0)" apply (cases "a=0", simp) apply (auto simp add: nonzero_eq_divide_eq) done lemma one_divide_eq_0_iff [simp,noatp]: - "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)" + "(1/a = (0::'a::{linordered_field,division_by_zero})) = (a = 0)" apply (cases "a=0", simp) apply (insert zero_neq_one [THEN not_sym]) apply (auto simp add: nonzero_divide_eq_eq) @@ -1912,22 +1911,22 @@ subsection {* Ordering Rules for Division *} lemma divide_strict_right_mono: - "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)" + "[|a < b; 0 < c|] ==> a / c < b / (c::'a::linordered_field)" by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono positive_imp_inverse_positive) lemma divide_right_mono: - "[|a \ b; 0 \ c|] ==> a/c \ b/(c::'a::{ordered_field,division_by_zero})" + "[|a \ b; 0 \ c|] ==> a/c \ b/(c::'a::{linordered_field,division_by_zero})" by (force simp add: divide_strict_right_mono order_le_less) -lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b +lemma divide_right_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b ==> c <= 0 ==> b / c <= a / c" apply (drule divide_right_mono [of _ _ "- c"]) apply auto done lemma divide_strict_right_mono_neg: - "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)" + "[|b < a; c < 0|] ==> a / c < b / (c::'a::linordered_field)" apply (drule divide_strict_right_mono [of _ _ "-c"], simp) apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) done @@ -1935,43 +1934,43 @@ text{*The last premise ensures that @{term a} and @{term b} have the same sign*} lemma divide_strict_left_mono: - "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)" + "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)" by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono) lemma divide_left_mono: - "[|b \ a; 0 \ c; 0 < a*b|] ==> c / a \ c / (b::'a::ordered_field)" + "[|b \ a; 0 \ c; 0 < a*b|] ==> c / a \ c / (b::'a::linordered_field)" by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono) -lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b +lemma divide_left_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b" apply (drule divide_left_mono [of _ _ "- c"]) apply (auto simp add: mult_commute) done lemma divide_strict_left_mono_neg: - "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)" + "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)" by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg) text{*Simplify quotients that are compared with the value 1.*} lemma le_divide_eq_1 [noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "(1 \ b / a) = ((0 < a & a \ b) | (a < 0 & b \ a))" by (auto simp add: le_divide_eq) lemma divide_le_eq_1 [noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "(b / a \ 1) = ((0 < a & b \ a) | (a < 0 & a \ b) | a=0)" by (auto simp add: divide_le_eq) lemma less_divide_eq_1 [noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))" by (auto simp add: less_divide_eq) lemma divide_less_eq_1 [noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)" by (auto simp add: divide_less_eq) @@ -1979,83 +1978,83 @@ subsection{*Conditional Simplification Rules: No Case Splits*} lemma le_divide_eq_1_pos [simp,noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "0 < a \ (1 \ b/a) = (a \ b)" by (auto simp add: le_divide_eq) lemma le_divide_eq_1_neg [simp,noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "a < 0 \ (1 \ b/a) = (b \ a)" by (auto simp add: le_divide_eq) lemma divide_le_eq_1_pos [simp,noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "0 < a \ (b/a \ 1) = (b \ a)" by (auto simp add: divide_le_eq) lemma divide_le_eq_1_neg [simp,noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "a < 0 \ (b/a \ 1) = (a \ b)" by (auto simp add: divide_le_eq) lemma less_divide_eq_1_pos [simp,noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "0 < a \ (1 < b/a) = (a < b)" by (auto simp add: less_divide_eq) lemma less_divide_eq_1_neg [simp,noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "a < 0 \ (1 < b/a) = (b < a)" by (auto simp add: less_divide_eq) lemma divide_less_eq_1_pos [simp,noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "0 < a \ (b/a < 1) = (b < a)" by (auto simp add: divide_less_eq) lemma divide_less_eq_1_neg [simp,noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "a < 0 \ b/a < 1 <-> a < b" by (auto simp add: divide_less_eq) lemma eq_divide_eq_1 [simp,noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "(1 = b/a) = ((a \ 0 & a = b))" by (auto simp add: eq_divide_eq) lemma divide_eq_eq_1 [simp,noatp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" + fixes a :: "'a :: {linordered_field,division_by_zero}" shows "(b/a = 1) = ((a \ 0 & a = b))" by (auto simp add: divide_eq_eq) subsection {* Reasoning about inequalities with division *} -lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1 +lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1 ==> x * y <= x" by (auto simp add: mult_compare_simps) -lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1 +lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1 ==> y * x <= x" by (auto simp add: mult_compare_simps) -lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==> +lemma mult_imp_div_pos_le: "0 < (y::'a::linordered_field) ==> x <= z * y ==> x / y <= z" by (subst pos_divide_le_eq, assumption+) -lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==> +lemma mult_imp_le_div_pos: "0 < (y::'a::linordered_field) ==> z * y <= x ==> z <= x / y" by(simp add:field_simps) -lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==> +lemma mult_imp_div_pos_less: "0 < (y::'a::linordered_field) ==> x < z * y ==> x / y < z" by(simp add:field_simps) -lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==> +lemma mult_imp_less_div_pos: "0 < (y::'a::linordered_field) ==> z * y < x ==> z < x / y" by(simp add:field_simps) -lemma frac_le: "(0::'a::ordered_field) <= x ==> +lemma frac_le: "(0::'a::linordered_field) <= x ==> x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w" apply (rule mult_imp_div_pos_le) apply simp @@ -2065,7 +2064,7 @@ apply simp_all done -lemma frac_less: "(0::'a::ordered_field) <= x ==> +lemma frac_less: "(0::'a::linordered_field) <= x ==> x < y ==> 0 < w ==> w <= z ==> x / z < y / w" apply (rule mult_imp_div_pos_less) apply simp @@ -2075,7 +2074,7 @@ apply simp_all done -lemma frac_less2: "(0::'a::ordered_field) < x ==> +lemma frac_less2: "(0::'a::linordered_field) < x ==> x <= y ==> 0 < w ==> w < z ==> x / z < y / w" apply (rule mult_imp_div_pos_less) apply simp_all @@ -2095,7 +2094,7 @@ subsection {* Ordered Fields are Dense *} -context ordered_semidom +context linordered_semidom begin lemma less_add_one: "a < a + 1" @@ -2110,13 +2109,13 @@ end -lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)" +lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::linordered_field)" by (simp add: field_simps zero_less_two) -lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b" +lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::linordered_field) < b" by (simp add: field_simps zero_less_two) -instance ordered_field < dense_linear_order +instance linordered_field < dense_linorder proof fix x y :: 'a have "x < x + 1" by simp @@ -2129,7 +2128,7 @@ subsection {* Absolute Value *} -context ordered_idom +context linordered_idom begin lemma mult_sgn_abs: "sgn x * abs x = x" @@ -2137,23 +2136,23 @@ end -lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)" +lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)" by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) -class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs + +class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs + assumes abs_eq_mult: "(0 \ a \ a \ 0) \ (0 \ b \ b \ 0) \ \a * b\ = \a\ * \b\" -class lordered_ring = pordered_ring + lordered_ab_group_add_abs +class lattice_ring = ordered_ring + lattice_ab_group_add_abs begin -subclass lordered_ab_group_add_meet .. -subclass lordered_ab_group_add_join .. +subclass semilattice_inf_ab_group_add .. +subclass semilattice_sup_ab_group_add .. end -lemma abs_le_mult: "abs (a * b) \ (abs a) * (abs (b::'a::lordered_ring))" +lemma abs_le_mult: "abs (a * b) \ (abs a) * (abs (b::'a::lattice_ring))" proof - let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b" let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" @@ -2194,9 +2193,9 @@ done qed -instance lordered_ring \ pordered_ring_abs +instance lattice_ring \ ordered_ring_abs proof - fix a b :: "'a\ lordered_ring" + fix a b :: "'a\ lattice_ring" assume "(0 \ a \ a \ 0) \ (0 \ b \ b \ 0)" show "abs (a*b) = abs a * abs b" proof - @@ -2238,10 +2237,10 @@ qed qed -context ordered_idom +context linordered_idom begin -subclass pordered_ring_abs proof +subclass ordered_ring_abs proof qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff) lemma abs_mult: @@ -2255,31 +2254,31 @@ end lemma nonzero_abs_inverse: - "a \ 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)" + "a \ 0 ==> abs (inverse (a::'a::linordered_field)) = inverse (abs a)" apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq negative_imp_inverse_negative) apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) done lemma abs_inverse [simp]: - "abs (inverse (a::'a::{ordered_field,division_by_zero})) = + "abs (inverse (a::'a::{linordered_field,division_by_zero})) = inverse (abs a)" apply (cases "a=0", simp) apply (simp add: nonzero_abs_inverse) done lemma nonzero_abs_divide: - "b \ 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b" + "b \ 0 ==> abs (a / (b::'a::linordered_field)) = abs a / abs b" by (simp add: divide_inverse abs_mult nonzero_abs_inverse) lemma abs_divide [simp]: - "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b" + "abs (a / (b::'a::{linordered_field,division_by_zero})) = abs a / abs b" apply (cases "b=0", simp) apply (simp add: nonzero_abs_divide) done lemma abs_mult_less: - "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)" + "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::linordered_idom)" proof - assume ac: "abs a < c" hence cpos: "0 +lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==> (abs y) * x = abs (y * x)" apply (subst abs_mult) apply simp done -lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> +lemma abs_div_pos: "(0::'a::{division_by_zero,linordered_field}) < y ==> abs x / y = abs (x / y)" apply (subst abs_divide) apply (simp add: order_less_imp_le) @@ -2314,7 +2313,7 @@ lemma mult_le_prts: assumes - "a1 <= (a::'a::lordered_ring)" + "a1 <= (a::'a::lattice_ring)" "a <= a2" "b1 <= b" "b <= b2" @@ -2362,7 +2361,7 @@ lemma mult_ge_prts: assumes - "a1 <= (a::'a::lordered_ring)" + "a1 <= (a::'a::lattice_ring)" "a <= a2" "b1 <= b" "b <= b2" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Series.thy --- a/src/HOL/Series.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Series.thy Mon Feb 08 11:13:30 2010 +0100 @@ -381,7 +381,7 @@ shows "norm x < 1 \ summable (\n. x ^ n)" by (rule geometric_sums [THEN sums_summable]) -lemma half: "0 < 1 / (2::'a::{number_ring,division_by_zero,ordered_field})" +lemma half: "0 < 1 / (2::'a::{number_ring,division_by_zero,linordered_field})" by arith lemma power_half_series: "(\n. (1/2::real)^Suc n) sums 1" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/SupInf.thy --- a/src/HOL/SupInf.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/SupInf.thy Mon Feb 08 11:13:30 2010 +0100 @@ -7,17 +7,17 @@ begin lemma minus_max_eq_min: - fixes x :: "'a::{lordered_ab_group_add, linorder}" + fixes x :: "'a::{lattice_ab_group_add, linorder}" shows "- (max x y) = min (-x) (-y)" by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1) lemma minus_min_eq_max: - fixes x :: "'a::{lordered_ab_group_add, linorder}" + fixes x :: "'a::{lattice_ab_group_add, linorder}" shows "- (min x y) = max (-x) (-y)" by (metis minus_max_eq_min minus_minus) lemma minus_Max_eq_Min [simp]: - fixes S :: "'a::{lordered_ab_group_add, linorder} set" + fixes S :: "'a::{lattice_ab_group_add, linorder} set" shows "finite S \ S \ {} \ - (Max S) = Min (uminus ` S)" proof (induct S rule: finite_ne_induct) case (singleton x) @@ -28,7 +28,7 @@ qed lemma minus_Min_eq_Max [simp]: - fixes S :: "'a::{lordered_ab_group_add, linorder} set" + fixes S :: "'a::{lattice_ab_group_add, linorder} set" shows "finite S \ S \ {} \ - (Min S) = Max (uminus ` S)" proof (induct S rule: finite_ne_induct) case (singleton x) diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 08 11:13:30 2010 +0100 @@ -200,19 +200,19 @@ else raise NOT_SUPPORTED "transitive closure for function or pair type" | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1) - | Const (@{const_name lower_semilattice_class.inf}, + | Const (@{const_name semilattice_inf_class.inf}, Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 => Intersect (to_R_rep Ts t1, to_R_rep Ts t2) - | Const (@{const_name lower_semilattice_class.inf}, _) $ _ => + | Const (@{const_name semilattice_inf_class.inf}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1) - | Const (@{const_name lower_semilattice_class.inf}, _) => + | Const (@{const_name semilattice_inf_class.inf}, _) => to_R_rep Ts (eta_expand Ts t 2) - | Const (@{const_name upper_semilattice_class.sup}, + | Const (@{const_name semilattice_sup_class.sup}, Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 => Union (to_R_rep Ts t1, to_R_rep Ts t2) - | Const (@{const_name upper_semilattice_class.sup}, _) $ _ => + | Const (@{const_name semilattice_sup_class.sup}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1) - | Const (@{const_name upper_semilattice_class.sup}, _) => + | Const (@{const_name semilattice_sup_class.sup}, _) => to_R_rep Ts (eta_expand Ts t 2) | Const (@{const_name minus_class.minus}, Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 => diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 08 11:13:30 2010 +0100 @@ -343,8 +343,8 @@ [((@{const_name of_nat}, nat_T --> int_T), 0), ((@{const_name of_nat}, @{typ "unsigned_bit word => signed_bit word"}), 0)] val built_in_set_consts = - [(@{const_name lower_semilattice_fun_inst.inf_fun}, 2), - (@{const_name upper_semilattice_fun_inst.sup_fun}, 2), + [(@{const_name semilattice_inf_fun_inst.inf_fun}, 2), + (@{const_name semilattice_sup_fun_inst.sup_fun}, 2), (@{const_name minus_fun_inst.minus_fun}, 2), (@{const_name ord_fun_inst.less_eq_fun}, 2)] @@ -2592,11 +2592,11 @@ if gfp then (lbfp_prefix, @{const "op |"}, - @{const_name upper_semilattice_fun_inst.sup_fun}) + @{const_name semilattice_sup_fun_inst.sup_fun}) else (ubfp_prefix, @{const "op &"}, - @{const_name lower_semilattice_fun_inst.inf_fun}) + @{const_name semilattice_inf_fun_inst.inf_fun}) (* unit -> term *) fun pos () = unrolled_inductive_pred_const ext_ctxt gfp x |> aux ss Ts js depth polar diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Feb 08 11:13:30 2010 +0100 @@ -667,9 +667,9 @@ in (CFun (ab_set_C, S Minus, ba_set_C), accum) end | @{const_name trancl} => do_fragile_set_operation T accum | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable) - | @{const_name lower_semilattice_fun_inst.inf_fun} => + | @{const_name semilattice_inf_fun_inst.inf_fun} => do_robust_set_operation T accum - | @{const_name upper_semilattice_fun_inst.sup_fun} => + | @{const_name semilattice_sup_fun_inst.sup_fun} => do_robust_set_operation T accum | @{const_name finite} => let val C1 = ctype_for (domain_type (domain_type T)) in diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 08 11:13:30 2010 +0100 @@ -655,10 +655,10 @@ | (Const (@{const_name of_nat}, T as @{typ "unsigned_bit word => signed_bit word"}), []) => Cst (NatToInt, T, Any) - | (Const (@{const_name lower_semilattice_fun_inst.inf_fun}, T), + | (Const (@{const_name semilattice_inf_fun_inst.inf_fun}, T), [t1, t2]) => Op2 (Intersect, nth_range_type 2 T, Any, sub t1, sub t2) - | (Const (@{const_name upper_semilattice_fun_inst.sup_fun}, T), + | (Const (@{const_name semilattice_sup_fun_inst.sup_fun}, T), [t1, t2]) => Op2 (Union, nth_range_type 2 T, Any, sub t1, sub t2) | (t0 as Const (@{const_name minus_fun_inst.minus_fun}, T), [t1, t2]) => diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Tools/int_arith.ML Mon Feb 08 11:13:30 2010 +0100 @@ -71,8 +71,8 @@ val lhss' = [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"}, - @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"}, - @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}] + @{cpat "(?x::?'a::linordered_idom) < (?y::?'a)"}, + @{cpat "(?x::?'a::linordered_idom) <= (?y::?'a)"}] val zero_one_idom_simproc = make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", @@ -80,9 +80,9 @@ val fast_int_arith_simproc = Simplifier.simproc @{theory} "fast_int_arith" - ["(m::'a::{ordered_idom,number_ring}) < n", - "(m::'a::{ordered_idom,number_ring}) <= n", - "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.simproc); + ["(m::'a::{linordered_idom,number_ring}) < n", + "(m::'a::{linordered_idom,number_ring}) <= n", + "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc); val global_setup = Simplifier.map_simpset (fn simpset => simpset addsimprocs [fast_int_arith_simproc]); diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Tools/lin_arith.ML Mon Feb 08 11:13:30 2010 +0100 @@ -236,7 +236,7 @@ end handle Rat.DIVZERO => NONE; fun of_lin_arith_sort thy U = - Sign.of_sort thy (U, @{sort Ring_and_Field.ordered_idom}); + Sign.of_sort thy (U, @{sort Ring_and_Field.linordered_idom}); fun allows_lin_arith thy (discrete : string list) (U as Type (D, [])) : bool * bool = if of_lin_arith_sort thy U then (true, member (op =) discrete D) @@ -804,12 +804,12 @@ val init_arith_data = Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, number_of, ...} => - {add_mono_thms = @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field} @ add_mono_thms, + {add_mono_thms = @{thms add_mono_thms_linordered_semiring} @ @{thms add_mono_thms_linordered_field} @ add_mono_thms, mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: @{lemma "a = b ==> c*a = c*b" by (rule arg_cong)} :: mult_mono_thms, inj_thms = inj_thms, lessD = lessD @ [@{thm "Suc_leI"}], - neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}], + neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_linordered_idom}], simpset = HOL_basic_ss addsimps @{thms ring_distribs} addsimps [@{thm if_True}, @{thm if_False}] diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Tools/numeral_simprocs.ML Mon Feb 08 11:13:30 2010 +0100 @@ -255,20 +255,20 @@ "(l::'a::number_ring) = m * n"], K EqCancelNumerals.proc), ("intless_cancel_numerals", - ["(l::'a::{ordered_idom,number_ring}) + m < n", - "(l::'a::{ordered_idom,number_ring}) < m + n", - "(l::'a::{ordered_idom,number_ring}) - m < n", - "(l::'a::{ordered_idom,number_ring}) < m - n", - "(l::'a::{ordered_idom,number_ring}) * m < n", - "(l::'a::{ordered_idom,number_ring}) < m * n"], + ["(l::'a::{linordered_idom,number_ring}) + m < n", + "(l::'a::{linordered_idom,number_ring}) < m + n", + "(l::'a::{linordered_idom,number_ring}) - m < n", + "(l::'a::{linordered_idom,number_ring}) < m - n", + "(l::'a::{linordered_idom,number_ring}) * m < n", + "(l::'a::{linordered_idom,number_ring}) < m * n"], K LessCancelNumerals.proc), ("intle_cancel_numerals", - ["(l::'a::{ordered_idom,number_ring}) + m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m + n", - "(l::'a::{ordered_idom,number_ring}) - m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m - n", - "(l::'a::{ordered_idom,number_ring}) * m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m * n"], + ["(l::'a::{linordered_idom,number_ring}) + m <= n", + "(l::'a::{linordered_idom,number_ring}) <= m + n", + "(l::'a::{linordered_idom,number_ring}) - m <= n", + "(l::'a::{linordered_idom,number_ring}) <= m - n", + "(l::'a::{linordered_idom,number_ring}) * m <= n", + "(l::'a::{linordered_idom,number_ring}) <= m * n"], K LeCancelNumerals.proc)]; structure CombineNumeralsData = @@ -431,12 +431,12 @@ "(l::'a::{idom,number_ring}) = m * n"], K EqCancelNumeralFactor.proc), ("ring_less_cancel_numeral_factor", - ["(l::'a::{ordered_idom,number_ring}) * m < n", - "(l::'a::{ordered_idom,number_ring}) < m * n"], + ["(l::'a::{linordered_idom,number_ring}) * m < n", + "(l::'a::{linordered_idom,number_ring}) < m * n"], K LessCancelNumeralFactor.proc), ("ring_le_cancel_numeral_factor", - ["(l::'a::{ordered_idom,number_ring}) * m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m * n"], + ["(l::'a::{linordered_idom,number_ring}) * m <= n", + "(l::'a::{linordered_idom,number_ring}) <= m * n"], K LeCancelNumeralFactor.proc), ("int_div_cancel_numeral_factors", ["((l::'a::{semiring_div,number_ring}) * m) div n", @@ -581,13 +581,13 @@ ["(l::'a::idom) * m = n", "(l::'a::idom) = m * n"], K EqCancelFactor.proc), - ("ordered_ring_le_cancel_factor", - ["(l::'a::ordered_ring) * m <= n", - "(l::'a::ordered_ring) <= m * n"], + ("linlinordered_ring_le_cancel_factor", + ["(l::'a::linordered_ring) * m <= n", + "(l::'a::linordered_ring) <= m * n"], K LeCancelFactor.proc), - ("ordered_ring_less_cancel_factor", - ["(l::'a::ordered_ring) * m < n", - "(l::'a::ordered_ring) < m * n"], + ("linlinordered_ring_less_cancel_factor", + ["(l::'a::linordered_ring) * m < n", + "(l::'a::linordered_ring) < m * n"], K LessCancelFactor.proc), ("int_div_cancel_factor", ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"], diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/Transcendental.thy Mon Feb 08 11:13:30 2010 +0100 @@ -381,7 +381,7 @@ done lemma real_setsum_nat_ivl_bounded2: - fixes K :: "'a::ordered_semidom" + fixes K :: "'a::linordered_semidom" assumes f: "\p::nat. p < n \ f p \ K" assumes K: "0 \ K" shows "setsum f {0.. of_nat n * K" diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/ZF/Games.thy --- a/src/HOL/ZF/Games.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/ZF/Games.thy Mon Feb 08 11:13:30 2010 +0100 @@ -922,7 +922,7 @@ apply (auto simp add: Pg_def quotient_def) done -instance Pg :: pordered_ab_group_add +instance Pg :: ordered_ab_group_add proof fix a b c :: Pg show "a - b = a + (- b)" by (simp add: Pg_diff_def) diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/ex/Numeral.thy Mon Feb 08 11:13:30 2010 +0100 @@ -442,12 +442,12 @@ end subsubsection {* - Comparisons: class @{text ordered_semidom} + Comparisons: class @{text linordered_semidom} *} text {* Could be perhaps more general than here. *} -context ordered_semidom +context linordered_semidom begin lemma of_num_pos [numeral]: "0 < of_num n" @@ -490,7 +490,7 @@ end -context ordered_idom +context linordered_idom begin lemma minus_of_num_less_of_num_iff: "- of_num m < of_num n" @@ -896,19 +896,19 @@ declare (in semiring_char_0) of_num_eq_one_iff [simp] declare (in semiring_char_0) one_eq_of_num_iff [simp] -declare (in ordered_semidom) of_num_pos [simp] -declare (in ordered_semidom) of_num_less_eq_iff [simp] -declare (in ordered_semidom) of_num_less_eq_one_iff [simp] -declare (in ordered_semidom) one_less_eq_of_num_iff [simp] -declare (in ordered_semidom) of_num_less_iff [simp] -declare (in ordered_semidom) of_num_less_one_iff [simp] -declare (in ordered_semidom) one_less_of_num_iff [simp] -declare (in ordered_semidom) of_num_nonneg [simp] -declare (in ordered_semidom) of_num_less_zero_iff [simp] -declare (in ordered_semidom) of_num_le_zero_iff [simp] +declare (in linordered_semidom) of_num_pos [simp] +declare (in linordered_semidom) of_num_less_eq_iff [simp] +declare (in linordered_semidom) of_num_less_eq_one_iff [simp] +declare (in linordered_semidom) one_less_eq_of_num_iff [simp] +declare (in linordered_semidom) of_num_less_iff [simp] +declare (in linordered_semidom) of_num_less_one_iff [simp] +declare (in linordered_semidom) one_less_of_num_iff [simp] +declare (in linordered_semidom) of_num_nonneg [simp] +declare (in linordered_semidom) of_num_less_zero_iff [simp] +declare (in linordered_semidom) of_num_le_zero_iff [simp] -declare (in ordered_idom) le_signed_numeral_special [simp] -declare (in ordered_idom) less_signed_numeral_special [simp] +declare (in linordered_idom) le_signed_numeral_special [simp] +declare (in linordered_idom) less_signed_numeral_special [simp] declare (in semiring_1_minus) Dig_of_num_minus_one [simp] declare (in semiring_1_minus) Dig_one_minus_of_num [simp] diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/ex/RPred.thy --- a/src/HOL/ex/RPred.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/ex/RPred.thy Mon Feb 08 11:13:30 2010 +0100 @@ -25,7 +25,7 @@ (* (infixl "\" 80) *) where "supp RP1 RP2 = (\s. let (P1, s') = RP1 s; (P2, s'') = RP2 s' - in (upper_semilattice_class.sup P1 P2, s''))" + in (semilattice_sup_class.sup P1 P2, s''))" definition if_rpred :: "bool \ unit rpred" where diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/ex/ReflectionEx.thy --- a/src/HOL/ex/ReflectionEx.thy Mon Feb 08 11:01:47 2010 +0100 +++ b/src/HOL/ex/ReflectionEx.thy Mon Feb 08 11:13:30 2010 +0100 @@ -385,7 +385,7 @@ (* An example for equations containing type variables *) datatype prod = Zero | One | Var nat | Mul prod prod | Pw prod nat | PNM nat nat prod -consts Iprod :: " prod \ ('a::{ordered_idom}) list \'a" +consts Iprod :: " prod \ ('a::{linordered_idom}) list \'a" primrec "Iprod Zero vs = 0" "Iprod One vs = 1" @@ -397,7 +397,7 @@ datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F | Or sgn sgn | And sgn sgn -consts Isgn :: " sgn \ ('a::{ordered_idom}) list \bool" +consts Isgn :: " sgn \ ('a::{linordered_idom}) list \bool" primrec "Isgn Tr vs = True" "Isgn F vs = False" @@ -410,7 +410,7 @@ lemmas eqs = Isgn.simps Iprod.simps -lemma "(x::'a::{ordered_idom})^4 * y * z * y^2 * z^23 > 0" +lemma "(x::'a::{linordered_idom})^4 * y * z * y^2 * z^23 > 0" apply (reify eqs) oops