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 uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML") |
13 uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") |
|
14 ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML") |
14 begin |
15 begin |
15 |
16 |
16 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*} |
17 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*} |
17 |
18 |
18 theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)" |
19 theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)" |
980 |
981 |
981 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" |
982 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" |
982 by (simp cong: conj_cong) |
983 by (simp cong: conj_cong) |
983 |
984 |
984 use "cooper_dec.ML" |
985 use "cooper_dec.ML" |
|
986 use "reflected_presburger.ML" |
|
987 use "reflected_cooper.ML" |
985 oracle |
988 oracle |
986 presburger_oracle ("term") = CooperDec.presburger_oracle |
989 presburger_oracle ("term") = ReflectedCooper.presburger_oracle |
987 |
990 |
988 use "cooper_proof.ML" |
991 use "cooper_proof.ML" |
989 use "qelim.ML" |
992 use "qelim.ML" |
990 use "presburger.ML" |
993 use "presburger.ML" |
991 |
994 |