tuned "discrete" field
authornipkow
Tue Sep 07 11:42:50 2004 +0200 (2004-09-07)
changeset 151858c43ffe2bb32
parent 15184 d2c19aea17bc
child 15186 1fb9a1fe8d0c
tuned "discrete" field
src/HOL/Integ/int_arith1.ML
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Sep 06 17:37:35 2004 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Tue Sep 07 11:42:50 2004 +0200
     1.3 @@ -524,7 +524,7 @@
     1.4                        addcongs [if_weak_cong]}),
     1.5    arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT),
     1.6    arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT),
     1.7 -  arith_discrete ("IntDef.int", true)];
     1.8 +  arith_discrete "IntDef.int"];
     1.9  
    1.10  end;
    1.11  
     2.1 --- a/src/HOL/arith_data.ML	Mon Sep 06 17:37:35 2004 +0200
     2.2 +++ b/src/HOL/arith_data.ML	Tue Sep 07 11:42:50 2004 +0200
     2.3 @@ -205,7 +205,7 @@
     2.4  structure ArithTheoryDataArgs =
     2.5  struct
     2.6    val name = "HOL/arith";
     2.7 -  type T = {splits: thm list, inj_consts: (string * typ)list, discrete: (string * bool) list, presburger: (int -> tactic) option};
     2.8 +  type T = {splits: thm list, inj_consts: (string * typ)list, discrete: string  list, presburger: (int -> tactic) option};
     2.9  
    2.10    val empty = {splits = [], inj_consts = [], discrete = [], presburger = None};
    2.11    val copy = I;
    2.12 @@ -214,7 +214,7 @@
    2.13               {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, presburger= presburger2}) =
    2.14     {splits = Drule.merge_rules (splits1, splits2),
    2.15      inj_consts = merge_lists inj_consts1 inj_consts2,
    2.16 -    discrete = merge_alists discrete1 discrete2,
    2.17 +    discrete = merge_lists discrete1 discrete2,
    2.18      presburger = (case presburger1 of None => presburger2 | p => p)};
    2.19    fun print _ _ = ();
    2.20  end;
    2.21 @@ -339,14 +339,11 @@
    2.22  fun of_lin_arith_sort sg U =
    2.23    Type.of_sort (Sign.tsig_of sg) (U,["Ring_and_Field.ordered_idom"])
    2.24  
    2.25 -(* FIXME: "discrete" should only contain discrete types *)
    2.26  fun allows_lin_arith sg discrete (U as Type(D,[])) =
    2.27        if of_lin_arith_sort sg U
    2.28 -      then (true, case assoc(discrete,D) of None => false
    2.29 -                  | Some d => d)
    2.30 +      then (true, D mem discrete)
    2.31        else (* special cases *)
    2.32 -           (case assoc(discrete,D) of None => (false,false)
    2.33 -            | Some d => (true,d))
    2.34 +           if D mem discrete then (true,true) else (false,false)
    2.35    | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
    2.36  
    2.37  fun decomp1 (sg,discrete,inj_consts) (T,xxx) =
    2.38 @@ -428,7 +425,7 @@
    2.39      inj_thms = inj_thms,
    2.40      lessD = lessD @ [Suc_leI],
    2.41      simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
    2.42 -  ArithTheoryData.init, arith_discrete ("nat", true)];
    2.43 +  ArithTheoryData.init, arith_discrete "nat"];
    2.44  
    2.45  end;
    2.46