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", |