equal
deleted
inserted
replaced
4 |
4 |
5 File containing necessary theorems for the proof |
5 File containing necessary theorems for the proof |
6 generation for Cooper Algorithm |
6 generation for Cooper Algorithm |
7 *) |
7 *) |
8 |
8 |
9 header {* Presburger Arithmetic: Cooper Algorithm *} |
9 header {* Presburger Arithmetic: Cooper's Algorithm *} |
10 |
10 |
11 theory Presburger = NatSimprocs + SetInterval |
11 theory Presburger |
12 files |
12 import NatSimprocs SetInterval |
13 ("cooper_dec.ML") |
13 files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML") |
14 ("cooper_proof.ML") |
14 begin |
15 ("qelim.ML") |
|
16 ("presburger.ML"): |
|
17 |
15 |
18 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*} |
19 |
17 |
20 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)" |
21 apply (rule iffI) |
19 apply (rule iffI) |