moved algebraic classes to Ring_and_Field
authorhaftmann
Thu Oct 29 11:41:37 2009 +0100 (2009-10-29)
changeset 3331974f0dcc0b5fb
parent 33318 ddd97d9dfbfb
child 33320 73998ef6ea91
moved algebraic classes to Ring_and_Field
src/HOL/Fact.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Fact.thy	Thu Oct 29 11:41:36 2009 +0100
     1.2 +++ b/src/HOL/Fact.thy	Thu Oct 29 11:41:37 2009 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header{*Factorial Function*}
     1.5  
     1.6  theory Fact
     1.7 -imports Nat_Transfer
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  class fact =
    1.12 @@ -266,9 +266,6 @@
    1.13  lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
    1.14  by auto
    1.15  
    1.16 -class ordered_semiring_1 = ordered_semiring + semiring_1
    1.17 -class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
    1.18 -
    1.19  lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
    1.20  
    1.21  lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
     2.1 --- a/src/HOL/Ring_and_Field.thy	Thu Oct 29 11:41:36 2009 +0100
     2.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Oct 29 11:41:37 2009 +0100
     2.3 @@ -767,6 +767,8 @@
     2.4  
     2.5  end
     2.6  
     2.7 +class ordered_semiring_1 = ordered_semiring + semiring_1
     2.8 +
     2.9  class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
    2.10    assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
    2.11    assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
    2.12 @@ -884,6 +886,8 @@
    2.13  
    2.14  end
    2.15  
    2.16 +class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
    2.17 +
    2.18  class mult_mono1 = times + zero + ord +
    2.19    assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    2.20  
    2.21 @@ -2025,15 +2029,15 @@
    2.22  
    2.23  lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
    2.24      ==> x * y <= x"
    2.25 -by (auto simp add: mult_compare_simps);
    2.26 +by (auto simp add: mult_compare_simps)
    2.27  
    2.28  lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
    2.29      ==> y * x <= x"
    2.30 -by (auto simp add: mult_compare_simps);
    2.31 +by (auto simp add: mult_compare_simps)
    2.32  
    2.33  lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
    2.34 -    x / y <= z";
    2.35 -by (subst pos_divide_le_eq, assumption+);
    2.36 +    x / y <= z"
    2.37 +by (subst pos_divide_le_eq, assumption+)
    2.38  
    2.39  lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
    2.40      z <= x / y"
    2.41 @@ -2060,8 +2064,8 @@
    2.42  lemma frac_less: "(0::'a::ordered_field) <= x ==> 
    2.43      x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
    2.44    apply (rule mult_imp_div_pos_less)
    2.45 -  apply simp;
    2.46 -  apply (subst times_divide_eq_left);
    2.47 +  apply simp
    2.48 +  apply (subst times_divide_eq_left)
    2.49    apply (rule mult_imp_less_div_pos, assumption)
    2.50    apply (erule mult_less_le_imp_less)
    2.51    apply simp_all
    2.52 @@ -2071,7 +2075,7 @@
    2.53      x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
    2.54    apply (rule mult_imp_div_pos_less)
    2.55    apply simp_all
    2.56 -  apply (subst times_divide_eq_left);
    2.57 +  apply (subst times_divide_eq_left)
    2.58    apply (rule mult_imp_less_div_pos, assumption)
    2.59    apply (erule mult_le_less_imp_less)
    2.60    apply simp_all