equal
deleted
inserted
replaced
8 |
8 |
9 header {* Presburger Arithmetic: Cooper's Algorithm *} |
9 header {* Presburger Arithmetic: Cooper's Algorithm *} |
10 |
10 |
11 theory Presburger |
11 theory Presburger |
12 imports NatSimprocs SetInterval |
12 imports NatSimprocs SetInterval |
13 files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML") |
13 uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML") |
14 begin |
14 begin |
15 |
15 |
16 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*} |
16 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*} |
17 |
17 |
18 theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)" |
18 theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)" |