# HG changeset patch # User haftmann # Date 1163428985 -3600 # Node ID 73bb86d0f483dcf5949b408da51362510c9092f2 # Parent 2b3c41d02e87925dca812c82117fb3648d815be0 dropped Inductive dependency diff -r 2b3c41d02e87 -r 73bb86d0f483 src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Mon Nov 13 15:43:04 2006 +0100 +++ b/src/HOL/OrderedGroup.thy Mon Nov 13 15:43:05 2006 +0100 @@ -7,7 +7,7 @@ header {* Ordered Groups *} theory OrderedGroup -imports Inductive LOrder +imports Set LOrder uses "~~/src/Provers/Arith/abel_cancel.ML" begin diff -r 2b3c41d02e87 -r 73bb86d0f483 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Mon Nov 13 15:43:04 2006 +0100 +++ b/src/HOL/Ring_and_Field.thy Mon Nov 13 15:43:05 2006 +0100 @@ -215,7 +215,7 @@ instance ordered_semiring_strict \ pordered_cancel_semiring apply intro_classes -apply (case_tac "a < b & 0 < c") +apply (cases "a < b & 0 < c") apply (auto simp add: mult_strict_left_mono order_less_le) apply (auto simp add: mult_strict_left_mono order_le_less) apply (simp add: mult_strict_right_mono) @@ -253,7 +253,7 @@ instance ordered_comm_semiring_strict \ pordered_cancel_comm_semiring apply (intro_classes) -apply (case_tac "a < b & 0 < c") +apply (cases "a < b & 0 < c") apply (auto simp add: mult_strict_left_mono order_less_le) apply (auto simp add: mult_strict_left_mono order_le_less) done @@ -400,7 +400,7 @@ lemma zero_less_mult_pos: "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)" -apply (case_tac "b\0") +apply (cases "b\0") apply (auto simp add: order_le_less linorder_not_less) apply (drule_tac mult_pos_neg [of a b]) apply (auto dest: order_less_not_sym) @@ -408,7 +408,7 @@ lemma zero_less_mult_pos2: "[| 0 < b*a; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)" -apply (case_tac "b\0") +apply (cases "b\0") apply (auto simp add: order_le_less linorder_not_less) apply (drule_tac mult_pos_neg2 [of a b]) apply (auto dest: order_less_not_sym) @@ -425,7 +425,7 @@ text{*A field has no "zero divisors", and this theorem holds without the assumption of an ordering. See @{text field_mult_eq_0_iff} below.*} lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring_strict)) = (a = 0 | b = 0)" -apply (case_tac "a < 0") +apply (cases "a < 0") apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff) apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+ done @@ -489,7 +489,7 @@ text{*Strict monotonicity in both arguments*} lemma mult_strict_mono: "[|ac|] ==> a * c < b * (d::'a::ordered_semiring_strict)" -apply (case_tac "c=0") +apply (cases "c=0") apply (simp add: mult_pos_pos) apply (erule mult_strict_right_mono [THEN order_less_trans]) apply (force simp add: order_le_less) @@ -552,7 +552,7 @@ lemma mult_less_cancel_right_disj: "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))" -apply (case_tac "c = 0") +apply (cases "c = 0") apply (auto simp add: linorder_neq_iff mult_strict_right_mono mult_strict_right_mono_neg) apply (auto simp add: linorder_not_less @@ -565,7 +565,7 @@ lemma mult_less_cancel_left_disj: "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))" -apply (case_tac "c = 0") +apply (cases "c = 0") apply (auto simp add: linorder_neq_iff mult_strict_left_mono mult_strict_left_mono_neg) apply (auto simp add: linorder_not_less @@ -877,7 +877,7 @@ lemma inverse_eq_imp_eq: "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})" -apply (case_tac "a=0 | b=0") +apply (cases "a=0 | b=0") apply (force dest!: inverse_zero_imp_zero simp add: eq_commute [of "0::'a"]) apply (force dest!: nonzero_inverse_eq_imp_eq) @@ -988,7 +988,7 @@ lemma mult_divide_cancel_left: "c\0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})" -apply (case_tac "b = 0") +apply (cases "b = 0") apply (simp_all add: nonzero_mult_divide_cancel_left) done @@ -998,7 +998,7 @@ lemma mult_divide_cancel_right: "c\0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})" -apply (case_tac "b = 0") +apply (cases "b = 0") apply (simp_all add: nonzero_mult_divide_cancel_right) done @@ -1122,7 +1122,7 @@ lemma minus_divide_divide [simp]: "(-a)/(-b) = a / (b::'a::{field,division_by_zero})" -apply (case_tac "b=0", simp) +apply (cases "b=0", simp) apply (simp add: nonzero_minus_divide_divide) done @@ -1184,7 +1184,7 @@ lemma inverse_positive_iff_positive [simp]: "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))" -apply (case_tac "a = 0", simp) +apply (cases "a = 0", simp) apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive) done @@ -1201,7 +1201,7 @@ lemma inverse_negative_iff_negative [simp]: "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))" -apply (case_tac "a = 0", simp) +apply (cases "a = 0", simp) apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative) done @@ -1362,7 +1362,7 @@ (if 0 < c then a*c \ b else if c < 0 then b \ a*c else a \ (0::'a::{ordered_field,division_by_zero}))" -apply (case_tac "c=0", simp) +apply (cases "c=0", simp) apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) done @@ -1391,7 +1391,7 @@ (if 0 < c then b \ a*c else if c < 0 then a*c \ b else 0 \ (a::'a::{ordered_field,division_by_zero}))" -apply (case_tac "c=0", simp) +apply (cases "c=0", simp) apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) done @@ -1422,7 +1422,7 @@ (if 0 < c then a*c < b else if c < 0 then b < a*c else a < (0::'a::{ordered_field,division_by_zero}))" -apply (case_tac "c=0", simp) +apply (cases "c=0", simp) apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) done @@ -1453,7 +1453,7 @@ (if 0 < c then b < a*c else if c < 0 then a*c < b else 0 < (a::'a::{ordered_field,division_by_zero}))" -apply (case_tac "c=0", simp) +apply (cases "c=0", simp) apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) done @@ -1583,13 +1583,13 @@ lemma divide_cancel_right [simp]: "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))" -apply (case_tac "c=0", simp) +apply (cases "c=0", simp) apply (simp add: divide_inverse field_mult_cancel_right) done lemma divide_cancel_left [simp]: "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" -apply (case_tac "c=0", simp) +apply (cases "c=0", simp) apply (simp add: divide_inverse field_mult_cancel_left) done @@ -1598,7 +1598,7 @@ text{*Simplify expressions equated with 1*} lemma divide_eq_1_iff [simp]: "(a/b = 1) = (b \ 0 & a = (b::'a::{field,division_by_zero}))" -apply (case_tac "b=0", simp) +apply (cases "b=0", simp) apply (simp add: right_inverse_eq) done @@ -1608,13 +1608,13 @@ lemma zero_eq_1_divide_iff [simp]: "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)" -apply (case_tac "a=0", simp) +apply (cases "a=0", simp) apply (auto simp add: nonzero_eq_divide_eq) done lemma one_divide_eq_0_iff [simp]: "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)" -apply (case_tac "a=0", simp) +apply (cases "a=0", simp) apply (insert zero_neq_one [THEN not_sym]) apply (auto simp add: nonzero_divide_eq_eq) done @@ -1666,7 +1666,7 @@ apply (subgoal_tac "a \ 0 & b \ 0") prefer 2 apply (force simp add: zero_less_mult_iff order_less_imp_not_eq) - apply (case_tac "c=0", simp add: divide_inverse) + apply (cases "c=0", simp add: divide_inverse) apply (force simp add: divide_strict_left_mono order_le_less) done @@ -1949,7 +1949,7 @@ lemma abs_inverse [simp]: "abs (inverse (a::'a::{ordered_field,division_by_zero})) = inverse (abs a)" -apply (case_tac "a=0", simp) +apply (cases "a=0", simp) apply (simp add: nonzero_abs_inverse) done @@ -1959,7 +1959,7 @@ lemma abs_divide [simp]: "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b" -apply (case_tac "b=0", simp) +apply (cases "b=0", simp) apply (simp add: nonzero_abs_divide) done