1.1 --- a/src/HOL/Real/rat_arith.ML	Fri Aug 06 16:55:14 2004 +0200
     1.2 +++ b/src/HOL/Real/rat_arith.ML	Fri Aug 06 17:07:04 2004 +0200
     1.3 @@ -23,18 +23,6 @@
     1.4  
     1.5  val simprocs = field_cancel_numeral_factors
     1.6  
     1.7 -val mono_ss = simpset() addsimps
     1.8 -                [add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono];
     1.9 -
    1.10 -val add_mono_thms_ordered_field =
    1.11 -  map (fn s => prove_goal (the_context ()) s
    1.12 -                 (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
    1.13 -    ["(i < j) & (k = l)   ==> i + k < j + (l::'a::ordered_field)",
    1.14 -     "(i = j) & (k < l)   ==> i + k < j + (l::'a::ordered_field)",
    1.15 -     "(i < j) & (k <= l)  ==> i + k < j + (l::'a::ordered_field)",
    1.16 -     "(i <= j) & (k < l)  ==> i + k < j + (l::'a::ordered_field)",
    1.17 -     "(i < j) & (k < l)   ==> i + k < j + (l::'a::ordered_field)"];
    1.18 -
    1.19  fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
    1.20  
    1.21  val rat_mult_mono_thms =
    1.22 @@ -68,7 +56,7 @@
    1.23  
    1.24  val rat_arith_setup =
    1.25   [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    1.26 -   {add_mono_thms = add_mono_thms @ add_mono_thms_ordered_field,
    1.27 +   {add_mono_thms = add_mono_thms,
    1.28      mult_mono_thms = mult_mono_thms @ rat_mult_mono_thms,
    1.29      inj_thms = int_inj_thms @ inj_thms,
    1.30      lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the rats are dense!*)

     2.1 --- a/src/HOL/arith_data.ML	Fri Aug 06 16:55:14 2004 +0200
     2.2 +++ b/src/HOL/arith_data.ML	Fri Aug 06 17:07:04 2004 +0200
     2.3 @@ -336,14 +336,26 @@
     2.4  fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
     2.5    | negate None = None;
     2.6  
     2.7 -fun decomp1 (discrete,inj_consts) (T,xxx) =
     2.8 +fun of_lin_arith_sort sg U =
     2.9 +  Type.of_sort (Sign.tsig_of sg) (U,["Ring_and_Field.ordered_idom"])
    2.10 +
    2.11 +(* FIXME: "discrete" should only contain discrete types *)
    2.12 +fun allows_lin_arith sg discrete (U as Type(D,[])) =
    2.13 +      if of_lin_arith_sort sg U
    2.14 +      then (true, case assoc(discrete,D) of None => false
    2.15 +                  | Some d => d)
    2.16 +      else (* special cases *)
    2.17 +           (case assoc(discrete,D) of None => (false,false)
    2.18 +            | Some d => (true,d))
    2.19 +  | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
    2.20 +
    2.21 +fun decomp1 (sg,discrete,inj_consts) (T,xxx) =
    2.22    (case T of
    2.23 -     Type("fun",[Type(D,[]),_]) =>
    2.24 -       (case assoc(discrete,D) of
    2.25 -          None => None
    2.26 -        | Some d => (case decomp2 inj_consts xxx of
    2.27 -                       None => None
    2.28 -                     | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d)))
    2.29 +     Type("fun",[U,_]) =>
    2.30 +       (case allows_lin_arith sg discrete U of
    2.31 +          (true,d) => (case decomp2 inj_consts xxx of None => None
    2.32 +                       | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d))
    2.33 +        | (false,_) => None)
    2.34     | _ => None);
    2.35  
    2.36  fun decomp2 data (_$(Const(rel,T)$lhs$rhs)) = decomp1 data (T,(rel,lhs,rhs))
    2.37 @@ -353,7 +365,7 @@
    2.38  
    2.39  fun decomp sg =
    2.40    let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg
    2.41 -  in decomp2 (discrete,inj_consts) end
    2.42 +  in decomp2 (sg,discrete,inj_consts) end
    2.43  
    2.44  fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n)
    2.45  
    2.46 @@ -386,18 +398,31 @@
    2.47  val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
    2.48   (fn prems => [cut_facts_tac prems 1,
    2.49                 blast_tac (claset() addIs [add_mono]) 1]))
    2.50 -["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semidom)",
    2.51 - "(i  = j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semidom)",
    2.52 - "(i <= j) & (k  = l) ==> i + k <= j + (l::'a::ordered_semidom)",
    2.53 - "(i  = j) & (k  = l) ==> i + k  = j + (l::'a::ordered_semidom)"
    2.54 +["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
    2.55 + "(i  = j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
    2.56 + "(i <= j) & (k  = l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
    2.57 + "(i  = j) & (k  = l) ==> i + k  = j + (l::'a::pordered_ab_semigroup_add)"
    2.58  ];
    2.59  
    2.60 +val mono_ss = simpset() addsimps
    2.61 +                [add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono];
    2.62 +
    2.63 +val add_mono_thms_ordered_field =
    2.64 +  map (fn s => prove_goal (the_context ()) s
    2.65 +                 (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
    2.66 +    ["(i<j) & (k=l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
    2.67 +     "(i=j) & (k<l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
    2.68 +     "(i<j) & (k<=l)  ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
    2.69 +     "(i<=j) & (k<l)  ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
    2.70 +     "(i<j) & (k<l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)"];
    2.71 +
    2.72  in
    2.73  
    2.74  val init_lin_arith_data =
    2.75   Fast_Arith.setup @
    2.76   [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset = _} =>
    2.77 -   {add_mono_thms = add_mono_thms @ add_mono_thms_ordered_semiring,
    2.78 +   {add_mono_thms = add_mono_thms @
    2.79 +    add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
    2.80      mult_mono_thms = mult_mono_thms,
    2.81      inj_thms = inj_thms,
    2.82      lessD = lessD @ [Suc_leI],