src/HOL/Integ/presburger.ML
changeset 20053 7f32ce6354d6
parent 19277 f7602e74d948
child 20194 c9dbce9a23a1
equal deleted inserted replaced
20052:3d4ff822d0b3 20053:7f32ce6354d6
    28 (*cooper_pp: provefunction for the one-exstance quantifier elimination*)
    28 (*cooper_pp: provefunction for the one-exstance quantifier elimination*)
    29 (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
    29 (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
    30 (*-----------------------------------------------------------------*)
    30 (*-----------------------------------------------------------------*)
    31 
    31 
    32 
    32 
    33 val presburger_ss = simpset_of (theory "Presburger");
    33 val presburger_ss = simpset ();
    34 val binarith = map thm
    34 val binarith = map thm
    35   ["Pls_0_eq", "Min_1_eq",
    35   ["Pls_0_eq", "Min_1_eq",
    36  "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
    36  "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
    37   "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
    37   "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
    38   "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
    38   "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",