--- a/NEWS Tue Jun 02 13:14:36 2015 +0200
+++ b/NEWS Wed Jun 03 09:32:49 2015 +0200
@@ -13,6 +13,17 @@
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.
+*** Pure ***
+
+* Abbreviations in type classes now carry proper sort constraint.
+Rare INCOMPATIBILITY in situations where the previous misbehaviour
+has been exploited previously.
+
+* Refinement of user-space type system in type classes: pseudo-local
+operations behave more similar to abbreviations. Potential
+INCOMPATIBILITY in exotic situations.
+
+
*** HOL ***
* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
@@ -25,6 +36,14 @@
* Nitpick:
- Removed "check_potential" and "check_genuine" options.
+* Constants Fields.divide (... / ...) and Divides.div (... div ...)
+are logically unified to Rings.divide in syntactic type class
+Rings.divide, with particular infix syntax added as abbreviations
+in classes Fields.inverse and Divides.div respectively. INCOMPATIBILITY,
+instantiatios must refer to Rings.divide rather than the former
+separate constants, and infix syntax is usually not available during
+instantiation.
+
New in Isabelle2015 (May 2015)
------------------------------
--- a/src/Doc/Main/Main_Doc.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Doc/Main/Main_Doc.thy Wed Jun 03 09:32:49 2015 +0200
@@ -325,7 +325,7 @@
@{const abs} & @{typeof abs}\\
@{const sgn} & @{typeof sgn}\\
@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\
-@{const div_class.div} & @{typeof "div_class.div"}\\
+@{const Rings.divide} & @{typeof Rings.divide}\\
@{const div_class.mod} & @{typeof "div_class.mod"}\\
\end{supertabular}
--- a/src/HOL/Code_Numeral.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Code_Numeral.thy Wed Jun 03 09:32:49 2015 +0200
@@ -150,11 +150,11 @@
instantiation integer :: "{ring_div, equal, linordered_idom}"
begin
-lift_definition div_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
- is "Divides.div :: int \<Rightarrow> int \<Rightarrow> int"
+lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "divide :: int \<Rightarrow> int \<Rightarrow> int"
.
-declare div_integer.rep_eq [simp]
+declare divide_integer.rep_eq [simp]
lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
@@ -709,11 +709,11 @@
instantiation natural :: "{semiring_div, equal, linordered_semiring}"
begin
-lift_definition div_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
- is "Divides.div :: nat \<Rightarrow> nat \<Rightarrow> nat"
+lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
.
-declare div_natural.rep_eq [simp]
+declare divide_natural.rep_eq [simp]
lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
--- a/src/HOL/Complex.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Complex.thy Wed Jun 03 09:32:49 2015 +0200
@@ -70,7 +70,7 @@
"Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
| "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
-definition "x / (y\<Colon>complex) = x * inverse y"
+definition "divide x (y\<Colon>complex) = x * inverse y"
instance
by intro_classes
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Jun 03 09:32:49 2015 +0200
@@ -710,7 +710,7 @@
fun dest_frac ct =
case Thm.term_of ct of
- Const (@{const_name Fields.divide},_) $ a $ b=>
+ Const (@{const_name Rings.divide},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
| Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
| t => Rat.rat_of_int (snd (HOLogic.dest_number t))
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Jun 03 09:32:49 2015 +0200
@@ -4033,7 +4033,7 @@
@{code poly.Mul} (num_of_term ps a, num_of_term ps b)
| num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) =
@{code poly.Pw} (num_of_term ps a, @{code nat_of_integer} (dest_nat n))
- | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) =
+ | num_of_term ps (Const (@{const_name Rings.divide}, _) $ a $ b) =
mk_C (dest_num a, dest_num b)
| num_of_term ps t =
(case try_dest_num t of
@@ -4087,7 +4087,7 @@
(if d = 1 then HOLogic.mk_number T c
else if d = 0 then Const (@{const_name Groups.zero}, T)
else
- Const (@{const_name Fields.divide}, binopT T) $
+ Const (@{const_name Rings.divide}, binopT T) $
HOLogic.mk_number T c $ HOLogic.mk_number T d)
end
| term_of_num T ps (@{code poly.Bound} i) = nth ps (@{code integer_of_nat} i)
--- a/src/HOL/Divides.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Divides.thy Wed Jun 03 09:32:49 2015 +0200
@@ -11,10 +11,15 @@
subsection {* Syntactic division operations *}
-class div = dvd +
- fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
- and mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
-
+class div = dvd + divide +
+ fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
+begin
+
+abbreviation div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
+where
+ "op div \<equiv> divide"
+
+end
subsection {* Abstract division in commutative semirings. *}
@@ -26,7 +31,13 @@
and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
begin
-subclass semiring_no_zero_divisors ..
+subclass semidom_divide
+proof
+ fix b a
+ assume "b \<noteq> 0"
+ then show "a * b div b = a"
+ using div_mult_self1 [of b 0 a] by (simp add: ac_simps)
+qed simp
lemma power_not_zero: -- \<open>FIXME cf. @{text field_power_not_zero}\<close>
"a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
@@ -102,11 +113,13 @@
"(b * c + a) mod b = a mod b"
by (simp add: add.commute)
-lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
- using div_mult_self2 [of b 0 a] by simp
-
-lemma div_mult_self2_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
- using div_mult_self1 [of b 0 a] by simp
+lemma div_mult_self1_is_id:
+ "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
+ by (fact nonzero_mult_divide_cancel_left)
+
+lemma div_mult_self2_is_id:
+ "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
+ by (fact nonzero_mult_divide_cancel_right)
lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
using mod_mult_self2 [of 0 b a] by simp
@@ -434,21 +447,21 @@
next
assume "b div a = c"
then have "b div a * a = c * a" by simp
- moreover from `a dvd b` have "b div a * a = b" by (simp add: dvd_div_mult_self)
+ moreover from `a dvd b` have "b div a * a = b" by simp
ultimately show "b = c * a" by simp
qed
lemma dvd_div_div_eq_mult:
assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
- using assms by (auto simp add: mult.commute [of _ a] dvd_div_mult_self dvd_div_eq_mult div_mult_swap intro: sym)
+ using assms by (auto simp add: mult.commute [of _ a] dvd_div_eq_mult div_mult_swap intro: sym)
end
class ring_div = comm_ring_1 + semiring_div
begin
-subclass idom ..
+subclass idom_divide ..
text {* Negation respects modular equivalence. *}
@@ -951,19 +964,26 @@
shows "divmod_nat m n = qr"
using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
+instantiation nat :: "Divides.div"
+begin
+
+definition divide_nat where
+ div_nat_def: "divide m n = fst (divmod_nat m n)"
+
+definition mod_nat where
+ "m mod n = snd (divmod_nat m n)"
+
+instance ..
+
+end
+
instantiation nat :: semiring_div
begin
-definition div_nat where
- "m div n = fst (divmod_nat m n)"
-
lemma fst_divmod_nat [simp]:
"fst (divmod_nat m n) = m div n"
by (simp add: div_nat_def)
-definition mod_nat where
- "m mod n = snd (divmod_nat m n)"
-
lemma snd_divmod_nat [simp]:
"snd (divmod_nat m n) = m mod n"
by (simp add: mod_nat_def)
@@ -1069,7 +1089,7 @@
ML {*
structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
(
- val div_name = @{const_name div};
+ val div_name = @{const_name divide};
val mod_name = @{const_name mod};
val mk_binop = HOLogic.mk_binop;
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
@@ -1184,18 +1204,23 @@
"(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
-lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
- apply (cut_tac m = q and n = c in mod_less_divisor)
- apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
- apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
- apply (simp add: add_mult_distrib2)
- done
-
lemma divmod_nat_rel_mult2_eq:
- "divmod_nat_rel a b (q, r)
- \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
-by (auto simp add: mult.commute mult.left_commute divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
-
+ assumes "divmod_nat_rel a b (q, r)"
+ shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
+proof -
+ { assume "r < b" and "0 < c"
+ then have "b * (q mod c) + r < b * c"
+ apply (cut_tac m = q and n = c in mod_less_divisor)
+ apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
+ apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
+ apply (simp add: add_mult_distrib2)
+ done
+ then have "r + b * (q mod c) < b * c"
+ by (simp add: ac_simps)
+ } with assms show ?thesis
+ by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
+qed
+
lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
@@ -1583,8 +1608,16 @@
using odd_succ_div_two [of n] by simp
lemma odd_two_times_div_two_nat [simp]:
- "odd n \<Longrightarrow> 2 * (n div 2) = n - (1 :: nat)"
- using odd_two_times_div_two_succ [of n] by simp
+ assumes "odd n"
+ shows "2 * (n div 2) = n - (1 :: nat)"
+proof -
+ from assms have "2 * (n div 2) + 1 = n"
+ by (rule odd_two_times_div_two_succ)
+ then have "Suc (2 * (n div 2)) - 1 = n - 1"
+ by simp
+ then show ?thesis
+ by simp
+qed
lemma odd_Suc_minus_one [simp]:
"odd n \<Longrightarrow> Suc (n - Suc 0) = n"
@@ -1669,24 +1702,24 @@
instantiation int :: Divides.div
begin
-definition div_int where
- "a div b = fst (divmod_int a b)"
+definition divide_int where
+ div_int_def: "divide a b = fst (divmod_int a b)"
+
+definition mod_int where
+ "a mod b = snd (divmod_int a b)"
+
+instance ..
+
+end
lemma fst_divmod_int [simp]:
"fst (divmod_int a b) = a div b"
by (simp add: div_int_def)
-definition mod_int where
- "a mod b = snd (divmod_int a b)"
-
lemma snd_divmod_int [simp]:
"snd (divmod_int a b) = a mod b"
by (simp add: mod_int_def)
-instance ..
-
-end
-
lemma divmod_int_mod_div:
"divmod_int p q = (p div q, p mod q)"
by (simp add: prod_eq_iff)
@@ -1909,7 +1942,7 @@
ML {*
structure Cancel_Div_Mod_Int = Cancel_Div_Mod
(
- val div_name = @{const_name div};
+ val div_name = @{const_name Rings.divide};
val mod_name = @{const_name mod};
val mk_binop = HOLogic.mk_binop;
val mk_sum = Arith_Data.mk_sum HOLogic.intT;
--- a/src/HOL/Enum.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Enum.thy Wed Jun 03 09:32:49 2015 +0200
@@ -585,12 +585,11 @@
definition [simp]: "Groups.one = a\<^sub>1"
definition [simp]: "op + = (\<lambda>_ _. a\<^sub>1)"
definition [simp]: "op * = (\<lambda>_ _. a\<^sub>1)"
-definition [simp]: "op div = (\<lambda>_ _. a\<^sub>1)"
definition [simp]: "op mod = (\<lambda>_ _. a\<^sub>1)"
definition [simp]: "abs = (\<lambda>_. a\<^sub>1)"
definition [simp]: "sgn = (\<lambda>_. a\<^sub>1)"
definition [simp]: "inverse = (\<lambda>_. a\<^sub>1)"
-definition [simp]: "op / = (\<lambda>_ _. a\<^sub>1)"
+definition [simp]: "divide = (\<lambda>_ _. a\<^sub>1)"
instance by intro_classes(simp_all add: less_finite_1_def)
end
@@ -691,15 +690,14 @@
definition "op - = (op + :: finite_2 \<Rightarrow> _)"
definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
definition "inverse = (\<lambda>x :: finite_2. x)"
-definition "op / = (op * :: finite_2 \<Rightarrow> _)"
+definition "divide = (op * :: finite_2 \<Rightarrow> _)"
definition "abs = (\<lambda>x :: finite_2. x)"
-definition "op div = (op / :: finite_2 \<Rightarrow> _)"
definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
definition "sgn = (\<lambda>x :: finite_2. x)"
instance
by intro_classes
(simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
- inverse_finite_2_def divide_finite_2_def abs_finite_2_def div_finite_2_def mod_finite_2_def sgn_finite_2_def
+ inverse_finite_2_def divide_finite_2_def abs_finite_2_def mod_finite_2_def sgn_finite_2_def
split: finite_2.splits)
end
@@ -819,15 +817,14 @@
definition "x - y = x + (- y :: finite_3)"
definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
definition "inverse = (\<lambda>x :: finite_3. x)"
-definition "x / y = x * inverse (y :: finite_3)"
+definition "divide x y = x * inverse (y :: finite_3)"
definition "abs = (\<lambda>x :: finite_3. x)"
-definition "op div = (op / :: finite_3 \<Rightarrow> _)"
definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
instance
by intro_classes
(simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
- inverse_finite_3_def divide_finite_3_def abs_finite_3_def div_finite_3_def mod_finite_3_def sgn_finite_3_def
+ inverse_finite_3_def divide_finite_3_def abs_finite_3_def mod_finite_3_def sgn_finite_3_def
less_finite_3_def
split: finite_3.splits)
end
--- a/src/HOL/Fields.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Fields.thy Wed Jun 03 09:32:49 2015 +0200
@@ -19,35 +19,16 @@
A division ring is like a field, but without the commutativity requirement.
*}
-class inverse =
+class inverse = divide +
fixes inverse :: "'a \<Rightarrow> 'a"
- and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
-
-setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
-
-
-context semiring
begin
-
-lemma [field_simps]:
- shows distrib_left_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
- and distrib_right_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
- by (rule distrib_left distrib_right)+
+
+abbreviation inverse_divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
+where
+ "inverse_divide \<equiv> divide"
end
-context ring
-begin
-
-lemma [field_simps]:
- shows left_diff_distrib_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
- and right_diff_distrib_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
- by (rule left_diff_distrib right_diff_distrib)+
-
-end
-
-setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
-
text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
named_theorems divide_simps "rewrite rules to eliminate divisions"
@@ -240,7 +221,7 @@
"z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
by (simp add: divide_diff_eq_iff[symmetric])
-lemma divide_zero [simp]:
+lemma division_ring_divide_zero [simp]:
"a / 0 = 0"
by (simp add: divide_inverse)
@@ -319,18 +300,31 @@
by (fact field_inverse_zero)
qed
-subclass idom ..
+subclass idom_divide
+proof
+ fix b a
+ assume "b \<noteq> 0"
+ then show "a * b / b = a"
+ by (simp add: divide_inverse ac_simps)
+next
+ fix a
+ show "a / 0 = 0"
+ by (simp add: divide_inverse)
+qed
text{*There is no slick version using division by zero.*}
lemma inverse_add:
- "[| a \<noteq> 0; b \<noteq> 0 |]
- ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
-by (simp add: division_ring_inverse_add ac_simps)
+ "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = (a + b) * inverse a * inverse b"
+ by (simp add: division_ring_inverse_add ac_simps)
lemma nonzero_mult_divide_mult_cancel_left [simp]:
-assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
-proof -
- have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
+ assumes [simp]: "c \<noteq> 0"
+ shows "(c * a) / (c * b) = a / b"
+proof (cases "b = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
by (simp add: divide_inverse nonzero_inverse_mult_distrib)
also have "... = a * inverse b * (inverse c * c)"
by (simp only: ac_simps)
@@ -339,8 +333,8 @@
qed
lemma nonzero_mult_divide_mult_cancel_right [simp]:
- "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
-by (simp add: mult.commute [of _ c])
+ "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
+ using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
by (simp add: divide_inverse ac_simps)
@@ -359,29 +353,21 @@
text{*Special Cancellation Simprules for Division*}
-lemma nonzero_mult_divide_cancel_right [simp]:
- "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
- using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
-
-lemma nonzero_mult_divide_cancel_left [simp]:
- "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
-using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
-
lemma nonzero_divide_mult_cancel_right [simp]:
- "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
-using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
+ "b \<noteq> 0 \<Longrightarrow> b / (a * b) = 1 / a"
+ using nonzero_mult_divide_mult_cancel_right [of b 1 a] by simp
lemma nonzero_divide_mult_cancel_left [simp]:
- "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
-using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
+ "a \<noteq> 0 \<Longrightarrow> a / (a * b) = 1 / b"
+ using nonzero_mult_divide_mult_cancel_left [of a 1 b] by simp
lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
- "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
-using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: ac_simps)
+ "c \<noteq> 0 \<Longrightarrow> (c * a) / (b * c) = a / b"
+ using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
- "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
-using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
+ "c \<noteq> 0 \<Longrightarrow> (a * c) / (c * b) = a / b"
+ using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
lemma diff_frac_eq:
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
@@ -445,7 +431,7 @@
lemma mult_divide_mult_cancel_left_if [simp]:
shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
- by (simp add: mult_divide_mult_cancel_left)
+ by simp
text {* Division and Unary Minus *}
--- a/src/HOL/Groups_Big.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Groups_Big.thy Wed Jun 03 09:32:49 2015 +0200
@@ -1153,10 +1153,29 @@
shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
using assms by (induct A) (auto simp: no_zero_divisors)
-lemma (in field) setprod_diff1:
- "finite A \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow>
- (setprod f (A - {a})) = (if a \<in> A then setprod f A / f a else setprod f A)"
- by (induct A rule: finite_induct) (auto simp add: insert_Diff_if)
+lemma (in semidom_divide) setprod_diff1:
+ assumes "finite A" and "f a \<noteq> 0"
+ shows "setprod f (A - {a}) = (if a \<in> A then divide (setprod f A) (f a) else setprod f A)"
+proof (cases "a \<notin> A")
+ case True then show ?thesis by simp
+next
+ case False with assms show ?thesis
+ proof (induct A rule: finite_induct)
+ case empty then show ?case by simp
+ next
+ case (insert b B)
+ then show ?case
+ proof (cases "a = b")
+ case True with insert show ?thesis by simp
+ next
+ case False with insert have "a \<in> B" by simp
+ def C \<equiv> "B - {a}"
+ with `finite B` `a \<in> B`
+ have *: "B = insert a C" "finite C" "a \<notin> C" by auto
+ with insert show ?thesis by (auto simp add: insert_commute ac_simps)
+ qed
+ qed
+qed
lemma (in field) setprod_inversef:
"finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
--- a/src/HOL/Library/Bit.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Bit.thy Wed Jun 03 09:32:49 2015 +0200
@@ -117,7 +117,7 @@
"inverse x = (x :: bit)"
definition divide_bit_def [simp]:
- "x / y = (x * y :: bit)"
+ "divide x y = (x * y :: bit)"
lemmas field_bit_defs =
plus_bit_def times_bit_def minus_bit_def uminus_bit_def
@@ -201,4 +201,3 @@
hide_const (open) set
end
-
--- a/src/HOL/Library/Extended.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Extended.thy Wed Jun 03 09:32:49 2015 +0200
@@ -25,7 +25,7 @@
case_of_simps less_eq_extended_case: less_eq_extended.simps
definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
-"((x::'a extended) < y) = (x \<le> y & \<not> x \<ge> y)"
+"((x::'a extended) < y) = (x \<le> y & \<not> y \<le> x)"
instance
by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
--- a/src/HOL/Library/Extended_Real.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy Wed Jun 03 09:32:49 2015 +0200
@@ -1403,7 +1403,7 @@
by (auto intro: ereal_cases)
termination by (relation "{}") simp
-definition "x / y = x * inverse (y :: ereal)"
+definition "divide x y = x * inverse (y :: ereal)"
instance ..
--- a/src/HOL/Library/Fraction_Field.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Wed Jun 03 09:32:49 2015 +0200
@@ -241,9 +241,9 @@
by (simp add: Fract_def inverse_fract_def UN_fractrel)
qed
-definition divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
+definition divide_fract_def: "divide q r = q * inverse (r:: 'a fract)"
-lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
+lemma divide_fract [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
by (simp add: divide_fract_def)
instance
@@ -255,7 +255,7 @@
(simp_all add: fract_expand eq_fract mult.commute)
next
fix q r :: "'a fract"
- show "q / r = q * inverse r" by (simp add: divide_fract_def)
+ show "divide q r = q * inverse r" by (simp add: divide_fract_def)
next
show "inverse 0 = (0:: 'a fract)"
by (simp add: fract_expand) (simp add: fract_collapse)
--- a/src/HOL/Library/Function_Division.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Function_Division.thy Wed Jun 03 09:32:49 2015 +0200
@@ -15,7 +15,7 @@
definition "inverse f = inverse \<circ> f"
-definition "(f / g) = (\<lambda>x. f x / g x)"
+definition "divide f g = (\<lambda>x. f x / g x)"
instance ..
@@ -63,4 +63,3 @@
*}
end
-
--- a/src/HOL/Library/Nat_Bijection.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Nat_Bijection.thy Wed Jun 03 09:32:49 2015 +0200
@@ -336,10 +336,19 @@
lemma set_decode_plus_power_2:
"n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)"
- apply (induct n arbitrary: z, simp_all)
- apply (rule set_eqI, induct_tac x, simp, simp)
- apply (rule set_eqI, induct_tac x, simp, simp add: add.commute)
-done
+proof (induct n arbitrary: z)
+ case 0 show ?case
+ proof (rule set_eqI)
+ fix q show "q \<in> set_decode (2 ^ 0 + z) \<longleftrightarrow> q \<in> insert 0 (set_decode z)"
+ by (induct q) (insert 0, simp_all)
+ qed
+next
+ case (Suc n) show ?case
+ proof (rule set_eqI)
+ fix q show "q \<in> set_decode (2 ^ Suc n + z) \<longleftrightarrow> q \<in> insert (Suc n) (set_decode z)"
+ by (induct q) (insert Suc, simp_all)
+ qed
+qed
lemma finite_set_decode [simp]: "finite (set_decode n)"
apply (induct n rule: nat_less_induct)
@@ -389,4 +398,3 @@
qed
end
-
--- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Wed Jun 03 09:32:49 2015 +0200
@@ -429,7 +429,7 @@
@{const Suc}, @{const plus (nat)}, @{const minus (nat)}]
val mult_nat_ops =
- [@{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
+ [@{const times (nat)}, @{const divide (nat)}, @{const mod (nat)}]
val nat_ops = simple_nat_ops @ mult_nat_ops
--- a/src/HOL/Library/Old_SMT/old_z3_interface.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_interface.ML Wed Jun 03 09:32:49 2015 +0200
@@ -41,7 +41,7 @@
has_datatypes=true}
end
- fun is_div_mod @{const div (int)} = true
+ fun is_div_mod @{const divide (int)} = true
| is_div_mod @{const mod (int)} = true
| is_div_mod _ = false
--- a/src/HOL/Library/Polynomial.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy Wed Jun 03 09:32:49 2015 +0200
@@ -1360,14 +1360,14 @@
instantiation poly :: (field) ring_div
begin
-definition div_poly where
- "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
+definition divide_poly where
+ div_poly_def: "divide x y = (THE q. \<exists>r. pdivmod_rel x y q r)"
definition mod_poly where
"x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
lemma div_poly_eq:
- "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
+ "pdivmod_rel x y q r \<Longrightarrow> divide x y = q"
unfolding div_poly_def
by (fast elim: pdivmod_rel_unique_div)
@@ -1377,7 +1377,7 @@
by (fast elim: pdivmod_rel_unique_mod)
lemma pdivmod_rel:
- "pdivmod_rel x y (x div y) (x mod y)"
+ "pdivmod_rel x y (divide x y) (x mod y)"
proof -
from pdivmod_rel_exists
obtain q r where "pdivmod_rel x y q r" by fast
@@ -1387,41 +1387,41 @@
instance proof
fix x y :: "'a poly"
- show "x div y * y + x mod y = x"
+ show "divide x y * y + x mod y = x"
using pdivmod_rel [of x y]
by (simp add: pdivmod_rel_def)
next
fix x :: "'a poly"
have "pdivmod_rel x 0 0 x"
by (rule pdivmod_rel_by_0)
- thus "x div 0 = 0"
+ thus "divide x 0 = 0"
by (rule div_poly_eq)
next
fix y :: "'a poly"
have "pdivmod_rel 0 y 0 0"
by (rule pdivmod_rel_0)
- thus "0 div y = 0"
+ thus "divide 0 y = 0"
by (rule div_poly_eq)
next
fix x y z :: "'a poly"
assume "y \<noteq> 0"
- hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
+ hence "pdivmod_rel (x + z * y) y (z + divide x y) (x mod y)"
using pdivmod_rel [of x y]
by (simp add: pdivmod_rel_def distrib_right)
- thus "(x + z * y) div y = z + x div y"
+ thus "divide (x + z * y) y = z + divide x y"
by (rule div_poly_eq)
next
fix x y z :: "'a poly"
assume "x \<noteq> 0"
- show "(x * y) div (x * z) = y div z"
+ show "divide (x * y) (x * z) = divide y z"
proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
by (rule pdivmod_rel_by_0)
- then have [simp]: "\<And>x::'a poly. x div 0 = 0"
+ then have [simp]: "\<And>x::'a poly. divide x 0 = 0"
by (rule div_poly_eq)
have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
by (rule pdivmod_rel_0)
- then have [simp]: "\<And>x::'a poly. 0 div x = 0"
+ then have [simp]: "\<And>x::'a poly. divide 0 x = 0"
by (rule div_poly_eq)
case False then show ?thesis by auto
next
@@ -1430,8 +1430,8 @@
have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
by (auto simp add: pdivmod_rel_def algebra_simps)
(rule classical, simp add: degree_mult_eq)
- moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
- ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
+ moreover from pdivmod_rel have "pdivmod_rel y z (divide y z) (y mod z)" .
+ ultimately have "pdivmod_rel (x * y) (x * z) (divide y z) (x * (y mod z))" .
then show ?thesis by (simp add: div_poly_eq)
qed
qed
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Jun 03 09:32:49 2015 +0200
@@ -53,7 +53,7 @@
setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}
setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name mod}, @{const_name times}] *}
section {* Arithmetic operations *}
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Jun 03 09:32:49 2015 +0200
@@ -283,14 +283,13 @@
(@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
(@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
(@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
- (@{const_name "Fields.inverse_class.divide"}, @{typ "prop => prop => prop"}),
- (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
(@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}),
(@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
(@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
(@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
(@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
- (@{const_name "Divides.div_class.div"}, @{typ "prop => prop => prop"}),
+ (@{const_name Rings.divide}, @{typ "prop => prop => prop"}),
(@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
(@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
(@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
--- a/src/HOL/NSA/StarDef.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy Wed Jun 03 09:32:49 2015 +0200
@@ -505,11 +505,18 @@
end
-instantiation star :: (inverse) inverse
+instantiation star :: (divide) divide
begin
definition
- star_divide_def: "(op /) \<equiv> *f2* (op /)"
+ star_divide_def: "divide \<equiv> *f2* divide"
+
+instance ..
+
+end
+
+instantiation star :: (inverse) inverse
+begin
definition
star_inverse_def: "inverse \<equiv> *f* inverse"
@@ -524,9 +531,6 @@
begin
definition
- star_div_def: "(op div) \<equiv> *f2* (op div)"
-
-definition
star_mod_def: "(op mod) \<equiv> *f2* (op mod)"
instance ..
@@ -551,7 +555,7 @@
star_add_def star_diff_def star_minus_def
star_mult_def star_divide_def star_inverse_def
star_le_def star_less_def star_abs_def star_sgn_def
- star_div_def star_mod_def
+ star_mod_def
text {* Class operations preserve standard elements *}
@@ -573,7 +577,7 @@
lemma Standard_mult: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x * y \<in> Standard"
by (simp add: star_mult_def)
-lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x / y \<in> Standard"
+lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> divide x y \<in> Standard"
by (simp add: star_divide_def)
lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
@@ -582,17 +586,14 @@
lemma Standard_abs: "x \<in> Standard \<Longrightarrow> abs x \<in> Standard"
by (simp add: star_abs_def)
-lemma Standard_div: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x div y \<in> Standard"
-by (simp add: star_div_def)
-
lemma Standard_mod: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x mod y \<in> Standard"
by (simp add: star_mod_def)
lemmas Standard_simps [simp] =
Standard_zero Standard_one
- Standard_add Standard_diff Standard_minus
+ Standard_add Standard_diff Standard_minus
Standard_mult Standard_divide Standard_inverse
- Standard_abs Standard_div Standard_mod
+ Standard_abs Standard_mod
text {* @{term star_of} preserves class operations *}
@@ -614,9 +615,6 @@
lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
by transfer (rule refl)
-lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
-by transfer (rule refl)
-
lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
by transfer (rule refl)
@@ -665,7 +663,7 @@
lemmas star_of_simps [simp] =
star_of_add star_of_diff star_of_minus
star_of_mult star_of_divide star_of_inverse
- star_of_div star_of_mod star_of_abs
+ star_of_mod star_of_abs
star_of_zero star_of_one
star_of_less star_of_le star_of_eq
star_of_0_less star_of_0_le star_of_0_eq
@@ -855,6 +853,13 @@
instance star :: (ring_1) ring_1 ..
instance star :: (comm_ring_1) comm_ring_1 ..
instance star :: (semidom) semidom ..
+instance star :: (semidom_divide) semidom_divide
+proof
+ show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
+ by transfer simp
+ show "\<And>a :: 'a star. divide a 0 = 0"
+ by transfer simp
+qed
instance star :: (semiring_div) semiring_div
apply intro_classes
apply(transfer, rule mod_div_equality)
@@ -867,6 +872,7 @@
instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
instance star :: (idom) idom ..
+instance star :: (idom_divide) idom_divide ..
instance star :: (division_ring) division_ring
apply (intro_classes)
--- a/src/HOL/Nat.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Nat.thy Wed Jun 03 09:32:49 2015 +0200
@@ -1484,6 +1484,14 @@
lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
+lemma of_nat_neq_0 [simp]:
+ "of_nat (Suc n) \<noteq> 0"
+ unfolding of_nat_eq_0_iff by simp
+
+lemma of_nat_0_neq [simp]:
+ "0 \<noteq> of_nat (Suc n)"
+ unfolding of_nat_0_eq_iff by simp
+
end
context linordered_semidom
--- a/src/HOL/Parity.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Parity.thy Wed Jun 03 09:32:49 2015 +0200
@@ -118,75 +118,60 @@
subsection {* Instances for @{typ nat} and @{typ int} *}
lemma even_Suc_Suc_iff [simp]:
- "even (Suc (Suc n)) \<longleftrightarrow> even n"
+ "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
using dvd_add_triv_right_iff [of 2 n] by simp
lemma even_Suc [simp]:
- "even (Suc n) \<longleftrightarrow> odd n"
+ "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
by (induct n) auto
lemma even_diff_nat [simp]:
fixes m n :: nat
- shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
+ shows "2 dvd (m - n) \<longleftrightarrow> m < n \<or> 2 dvd (m + n)"
proof (cases "n \<le> m")
case True
then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
- moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
- ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
+ moreover have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m - n + n * 2)" by simp
+ ultimately have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m + n)" by (simp only:)
then show ?thesis by auto
next
case False
then show ?thesis by simp
qed
-lemma even_diff_iff [simp]:
- fixes k l :: int
- shows "even (k - l) \<longleftrightarrow> even (k + l)"
- using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
-
-lemma even_abs_add_iff [simp]:
- fixes k l :: int
- shows "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)"
- by (cases "k \<ge> 0") (simp_all add: ac_simps)
-
-lemma even_add_abs_iff [simp]:
- fixes k l :: int
- shows "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)"
- using even_abs_add_iff [of l k] by (simp add: ac_simps)
-
instance nat :: semiring_parity
proof
- show "odd (1 :: nat)"
+ show "\<not> 2 dvd (1 :: nat)"
by (rule notI, erule dvdE) simp
next
fix m n :: nat
- assume "odd m"
- moreover assume "odd n"
- ultimately have *: "even (Suc m) \<and> even (Suc n)"
+ assume "\<not> 2 dvd m"
+ moreover assume "\<not> 2 dvd n"
+ ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
by simp
- then have "even (Suc m + Suc n)"
+ then have "2 dvd (Suc m + Suc n)"
by (blast intro: dvd_add)
also have "Suc m + Suc n = m + n + 2"
by simp
- finally show "even (m + n)"
+ finally show "2 dvd (m + n)"
using dvd_add_triv_right_iff [of 2 "m + n"] by simp
next
fix m n :: nat
- assume *: "even (m * n)"
- show "even m \<or> even n"
+ assume *: "2 dvd (m * n)"
+ show "2 dvd m \<or> 2 dvd n"
proof (rule disjCI)
- assume "odd n"
- then have "even (Suc n)" by simp
+ assume "\<not> 2 dvd n"
+ then have "2 dvd (Suc n)" by simp
then obtain r where "Suc n = 2 * r" ..
moreover from * obtain s where "m * n = 2 * s" ..
then have "2 * s + m = m * Suc n" by simp
ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
then have "m = 2 * (m * r - s)" by simp
- then show "even m" ..
+ then show "2 dvd m" ..
qed
next
fix n :: nat
- assume "odd n"
+ assume "\<not> 2 dvd n"
then show "\<exists>m. n = m + 1"
by (cases n) simp_all
qed
@@ -194,23 +179,38 @@
lemma odd_pos:
"odd (n :: nat) \<Longrightarrow> 0 < n"
by (auto elim: oddE)
-
+
+lemma even_diff_iff [simp]:
+ fixes k l :: int
+ shows "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
+ using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
+
+lemma even_abs_add_iff [simp]:
+ fixes k l :: int
+ shows "2 dvd (\<bar>k\<bar> + l) \<longleftrightarrow> 2 dvd (k + l)"
+ by (cases "k \<ge> 0") (simp_all add: ac_simps)
+
+lemma even_add_abs_iff [simp]:
+ fixes k l :: int
+ shows "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
+ using even_abs_add_iff [of l k] by (simp add: ac_simps)
+
instance int :: ring_parity
proof
- show "odd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
+ show "\<not> 2 dvd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
fix k l :: int
- assume "odd k"
- moreover assume "odd l"
- ultimately have "even (nat \<bar>k\<bar> + nat \<bar>l\<bar>)"
+ assume "\<not> 2 dvd k"
+ moreover assume "\<not> 2 dvd l"
+ ultimately have "2 dvd (nat \<bar>k\<bar> + nat \<bar>l\<bar>)"
by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
- then have "even (\<bar>k\<bar> + \<bar>l\<bar>)"
+ then have "2 dvd (\<bar>k\<bar> + \<bar>l\<bar>)"
by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
- then show "even (k + l)"
+ then show "2 dvd (k + l)"
by simp
next
fix k l :: int
- assume "even (k * l)"
- then show "even k \<or> even l"
+ assume "2 dvd (k * l)"
+ then show "2 dvd k \<or> 2 dvd l"
by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
next
fix k :: int
@@ -352,4 +352,3 @@
]
end
-
--- a/src/HOL/Rat.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Rat.thy Wed Jun 03 09:32:49 2015 +0200
@@ -162,9 +162,9 @@
by transfer simp
definition
- divide_rat_def: "q / r = q * inverse (r::rat)"
+ divide_rat_def: "divide q r = q * inverse (r::rat)"
-lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
+lemma divide_rat [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
by (simp add: divide_rat_def)
instance proof
@@ -191,7 +191,7 @@
by transfer simp
{ assume "q \<noteq> 0" thus "inverse q * q = 1"
by transfer simp }
- show "q / r = q * inverse r"
+ show "divide q r = q * inverse r"
by (fact divide_rat_def)
show "inverse 0 = (0::rat)"
by transfer simp
@@ -1158,8 +1158,8 @@
val {mant = i, exp = n} = Lexicon.read_float str;
val exp = Syntax.const @{const_syntax Power.power};
val ten = Numeral.mk_number_syntax 10;
- val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n;;
- in Syntax.const @{const_syntax divide} $ Numeral.mk_number_syntax i $ exp10 end;
+ val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n;
+ in Syntax.const @{const_syntax Fields.inverse_divide} $ Numeral.mk_number_syntax i $ exp10 end;
fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
| float_tr [t as Const (str, _)] = mk_frac str
--- a/src/HOL/Real.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Real.thy Wed Jun 03 09:32:49 2015 +0200
@@ -438,7 +438,7 @@
"x - y = (x::real) + - y"
definition
- "x / y = (x::real) * inverse y"
+ "divide x y = (x::real) * inverse y"
lemma add_Real:
assumes X: "cauchy X" and Y: "cauchy Y"
@@ -501,7 +501,7 @@
apply (rule_tac x=k in exI, clarify)
apply (drule_tac x=n in spec, simp)
done
- show "a / b = a * inverse b"
+ show "divide a b = a * inverse b"
by (rule divide_real_def)
show "inverse (0::real) = 0"
by transfer (simp add: realrel_def)
--- a/src/HOL/Rings.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Rings.thy Wed Jun 03 09:32:49 2015 +0200
@@ -558,6 +558,46 @@
\end{itemize}
*}
+class divide =
+ fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
+context semiring
+begin
+
+lemma [field_simps]:
+ shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
+ and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
+ by (rule distrib_left distrib_right)+
+
+end
+
+context ring
+begin
+
+lemma [field_simps]:
+ shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
+ and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
+ by (rule left_diff_distrib right_diff_distrib)+
+
+end
+
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
+class semidom_divide = semidom + divide +
+ assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
+ assumes divide_zero [simp]: "divide a 0 = 0"
+begin
+
+lemma nonzero_mult_divide_cancel_left [simp]:
+ "a \<noteq> 0 \<Longrightarrow> divide (a * b) a = b"
+ using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
+
+end
+
+class idom_divide = idom + semidom_divide
+
class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
--- a/src/HOL/SMT_Examples/SMT_Examples.certs Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Wed Jun 03 09:32:49 2015 +0200
@@ -4415,6 +4415,1608 @@
(let ((@x128 (asserted $x127)))
(unit-resolution @x128 @x546 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+0f7f4a10f8a84029fd3a6efddc4408fa429b0cda 113 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x228 (mod x$ 2)))
+(let ((?x262 (* (- 1) ?x228)))
+(let ((?x31 (mod$ x$ 2)))
+(let ((?x263 (+ ?x31 ?x262)))
+(let (($x280 (>= ?x263 0)))
+(let (($x264 (= ?x263 0)))
+(let (($x205 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x136 (mod ?v0 ?v1)))
+(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?v1 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?v1 0)))
+(let ((?x175 (ite $x78 ?v0 ?x170)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x175))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x181 (forall ((?v0 Int) (?v1 Int) )(let ((?x136 (mod ?v0 ?v1)))
+(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?v1 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?v1 0)))
+(let ((?x175 (ite $x78 ?v0 ?x170)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x175))))))))))))
+))
+(let ((?x136 (mod ?1 ?0)))
+(let ((?x93 (* (- 1) ?0)))
+(let ((?x90 (* (- 1) ?1)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?0 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?0 0)))
+(let ((?x175 (ite $x78 ?1 ?x170)))
+(let ((?x135 (mod$ ?1 ?0)))
+(let (($x178 (= ?x135 ?x175)))
+(let (($x142 (forall ((?v0 Int) (?v1 Int) )(let (($x78 (= ?v1 0)))
+(let ((?x140 (ite $x78 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x140)))))
+))
+(let (($x164 (forall ((?v0 Int) (?v1 Int) )(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let ((?x136 (mod ?v0 ?v1)))
+(let (($x79 (< 0 ?v1)))
+(let ((?x155 (ite $x79 ?x136 ?x150)))
+(let (($x78 (= ?v1 0)))
+(let ((?x158 (ite $x78 ?v0 ?x155)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x158))))))))))))
+))
+(let ((@x169 (monotonicity (rewrite (= (< 0 ?0) (not $x111))) (= (ite (< 0 ?0) ?x136 ?x150) (ite (not $x111) ?x136 ?x150)))))
+(let ((@x174 (trans @x169 (rewrite (= (ite (not $x111) ?x136 ?x150) ?x170)) (= (ite (< 0 ?0) ?x136 ?x150) ?x170))))
+(let ((@x177 (monotonicity @x174 (= (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150)) ?x175))))
+(let ((@x180 (monotonicity @x177 (= (= ?x135 (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150))) $x178))))
+(let (($x79 (< 0 ?0)))
+(let ((?x155 (ite $x79 ?x136 ?x150)))
+(let ((?x158 (ite $x78 ?1 ?x155)))
+(let (($x161 (= ?x135 ?x158)))
+(let (($x162 (= (= ?x135 (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))))) $x161)))
+(let ((@x146 (monotonicity (rewrite (= (- ?1) ?x90)) (rewrite (= (- ?0) ?x93)) (= (mod (- ?1) (- ?0)) ?x144))))
+(let ((@x154 (trans (monotonicity @x146 (= (- (mod (- ?1) (- ?0))) (- ?x144))) (rewrite (= (- ?x144) ?x150)) (= (- (mod (- ?1) (- ?0))) ?x150))))
+(let ((@x157 (monotonicity @x154 (= (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))) ?x155))))
+(let ((@x160 (monotonicity @x157 (= (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0))))) ?x158))))
+(let ((@x185 (trans (quant-intro (monotonicity @x160 $x162) (= $x142 $x164)) (quant-intro @x180 (= $x164 $x181)) (= $x142 $x181))))
+(let ((@x196 (mp~ (mp (asserted $x142) @x185 $x181) (nnf-pos (refl (~ $x178 $x178)) (~ $x181 $x181)) $x181)))
+(let ((@x210 (mp @x196 (quant-intro (refl (= $x178 $x178)) (= $x181 $x205)) $x205)))
+(let (($x270 (or (not $x205) $x264)))
+(let ((?x225 (* (- 1) 2)))
+(let ((?x224 (* (- 1) x$)))
+(let ((?x226 (mod ?x224 ?x225)))
+(let ((?x227 (* (- 1) ?x226)))
+(let (($x223 (<= 2 0)))
+(let ((?x229 (ite $x223 ?x227 ?x228)))
+(let (($x222 (= 2 0)))
+(let ((?x230 (ite $x222 x$ ?x229)))
+(let (($x231 (= ?x31 ?x230)))
+(let ((@x244 (monotonicity (monotonicity (rewrite (= ?x225 (- 2))) (= ?x226 (mod ?x224 (- 2)))) (= ?x227 (* (- 1) (mod ?x224 (- 2)))))))
+(let ((@x247 (monotonicity (rewrite (= $x223 false)) @x244 (= ?x229 (ite false (* (- 1) (mod ?x224 (- 2))) ?x228)))))
+(let ((@x251 (trans @x247 (rewrite (= (ite false (* (- 1) (mod ?x224 (- 2))) ?x228) ?x228)) (= ?x229 ?x228))))
+(let ((@x254 (monotonicity (rewrite (= $x222 false)) @x251 (= ?x230 (ite false x$ ?x228)))))
+(let ((@x261 (monotonicity (trans @x254 (rewrite (= (ite false x$ ?x228) ?x228)) (= ?x230 ?x228)) (= $x231 (= ?x31 ?x228)))))
+(let ((@x274 (monotonicity (trans @x261 (rewrite (= (= ?x31 ?x228) $x264)) (= $x231 $x264)) (= (or (not $x205) $x231) $x270))))
+(let ((@x277 (trans @x274 (rewrite (= $x270 $x270)) (= (or (not $x205) $x231) $x270))))
+(let ((@x278 (mp ((_ quant-inst x$ 2) (or (not $x205) $x231)) @x277 $x270)))
+(let ((@x337 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x264) $x280)) (unit-resolution @x278 @x210 $x264) $x280)))
+(let (($x305 (>= ?x228 0)))
+(let (($x64 (>= ?x31 0)))
+(let (($x67 (not $x64)))
+(let (($x36 (not (<= (+ x$ 1) (+ x$ (+ (* 2 ?x31) 1))))))
+(let ((@x69 (monotonicity (rewrite (= (>= (* 2 ?x31) 0) $x64)) (= (not (>= (* 2 ?x31) 0)) $x67))))
+(let ((?x32 (* 2 ?x31)))
+(let ((?x47 (+ 1 x$ ?x32)))
+(let (($x52 (<= (+ 1 x$) ?x47)))
+(let (($x55 (not $x52)))
+(let ((@x63 (monotonicity (rewrite (= $x52 (>= ?x32 0))) (= $x55 (not (>= ?x32 0))))))
+(let ((@x46 (monotonicity (rewrite (= (+ ?x32 1) (+ 1 ?x32))) (= (+ x$ (+ ?x32 1)) (+ x$ (+ 1 ?x32))))))
+(let ((@x51 (trans @x46 (rewrite (= (+ x$ (+ 1 ?x32)) ?x47)) (= (+ x$ (+ ?x32 1)) ?x47))))
+(let ((@x54 (monotonicity (rewrite (= (+ x$ 1) (+ 1 x$))) @x51 (= (<= (+ x$ 1) (+ x$ (+ ?x32 1))) $x52))))
+(let ((@x73 (trans (monotonicity @x54 (= $x36 $x55)) (trans @x63 @x69 (= $x55 $x67)) (= $x36 $x67))))
+(let ((@x74 (mp (asserted $x36) @x73 $x67)))
+((_ th-lemma arith farkas -1 1 1) @x74 (unit-resolution ((_ th-lemma arith) (or false $x305)) (true-axiom true) $x305) @x337 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+fa5abc269019f00f5093218b287856c2a08c0adf 112 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x224 (mod x$ 2)))
+(let (($x318 (>= ?x224 2)))
+(let (($x319 (not $x318)))
+(let ((?x258 (* (- 1) ?x224)))
+(let ((?x29 (mod$ x$ 2)))
+(let ((?x259 (+ ?x29 ?x258)))
+(let (($x275 (<= ?x259 0)))
+(let (($x260 (= ?x259 0)))
+(let (($x201 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x132 (mod ?v0 ?v1)))
+(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?v1 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?v1 0)))
+(let ((?x171 (ite $x74 ?v0 ?x166)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x171))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x177 (forall ((?v0 Int) (?v1 Int) )(let ((?x132 (mod ?v0 ?v1)))
+(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?v1 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?v1 0)))
+(let ((?x171 (ite $x74 ?v0 ?x166)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x171))))))))))))
+))
+(let ((?x132 (mod ?1 ?0)))
+(let ((?x89 (* (- 1) ?0)))
+(let ((?x86 (* (- 1) ?1)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?0 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?0 0)))
+(let ((?x171 (ite $x74 ?1 ?x166)))
+(let ((?x131 (mod$ ?1 ?0)))
+(let (($x174 (= ?x131 ?x171)))
+(let (($x138 (forall ((?v0 Int) (?v1 Int) )(let (($x74 (= ?v1 0)))
+(let ((?x136 (ite $x74 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x136)))))
+))
+(let (($x160 (forall ((?v0 Int) (?v1 Int) )(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let ((?x132 (mod ?v0 ?v1)))
+(let (($x75 (< 0 ?v1)))
+(let ((?x151 (ite $x75 ?x132 ?x146)))
+(let (($x74 (= ?v1 0)))
+(let ((?x154 (ite $x74 ?v0 ?x151)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x154))))))))))))
+))
+(let ((@x165 (monotonicity (rewrite (= (< 0 ?0) (not $x107))) (= (ite (< 0 ?0) ?x132 ?x146) (ite (not $x107) ?x132 ?x146)))))
+(let ((@x170 (trans @x165 (rewrite (= (ite (not $x107) ?x132 ?x146) ?x166)) (= (ite (< 0 ?0) ?x132 ?x146) ?x166))))
+(let ((@x173 (monotonicity @x170 (= (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146)) ?x171))))
+(let ((@x176 (monotonicity @x173 (= (= ?x131 (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146))) $x174))))
+(let (($x75 (< 0 ?0)))
+(let ((?x151 (ite $x75 ?x132 ?x146)))
+(let ((?x154 (ite $x74 ?1 ?x151)))
+(let (($x157 (= ?x131 ?x154)))
+(let (($x158 (= (= ?x131 (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))))) $x157)))
+(let ((@x142 (monotonicity (rewrite (= (- ?1) ?x86)) (rewrite (= (- ?0) ?x89)) (= (mod (- ?1) (- ?0)) ?x140))))
+(let ((@x150 (trans (monotonicity @x142 (= (- (mod (- ?1) (- ?0))) (- ?x140))) (rewrite (= (- ?x140) ?x146)) (= (- (mod (- ?1) (- ?0))) ?x146))))
+(let ((@x153 (monotonicity @x150 (= (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))) ?x151))))
+(let ((@x156 (monotonicity @x153 (= (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0))))) ?x154))))
+(let ((@x181 (trans (quant-intro (monotonicity @x156 $x158) (= $x138 $x160)) (quant-intro @x176 (= $x160 $x177)) (= $x138 $x177))))
+(let ((@x192 (mp~ (mp (asserted $x138) @x181 $x177) (nnf-pos (refl (~ $x174 $x174)) (~ $x177 $x177)) $x177)))
+(let ((@x206 (mp @x192 (quant-intro (refl (= $x174 $x174)) (= $x177 $x201)) $x201)))
+(let (($x266 (or (not $x201) $x260)))
+(let ((?x221 (* (- 1) 2)))
+(let ((?x220 (* (- 1) x$)))
+(let ((?x222 (mod ?x220 ?x221)))
+(let ((?x223 (* (- 1) ?x222)))
+(let (($x219 (<= 2 0)))
+(let ((?x225 (ite $x219 ?x223 ?x224)))
+(let (($x218 (= 2 0)))
+(let ((?x226 (ite $x218 x$ ?x225)))
+(let (($x227 (= ?x29 ?x226)))
+(let ((@x240 (monotonicity (monotonicity (rewrite (= ?x221 (- 2))) (= ?x222 (mod ?x220 (- 2)))) (= ?x223 (* (- 1) (mod ?x220 (- 2)))))))
+(let ((@x243 (monotonicity (rewrite (= $x219 false)) @x240 (= ?x225 (ite false (* (- 1) (mod ?x220 (- 2))) ?x224)))))
+(let ((@x247 (trans @x243 (rewrite (= (ite false (* (- 1) (mod ?x220 (- 2))) ?x224) ?x224)) (= ?x225 ?x224))))
+(let ((@x250 (monotonicity (rewrite (= $x218 false)) @x247 (= ?x226 (ite false x$ ?x224)))))
+(let ((@x257 (monotonicity (trans @x250 (rewrite (= (ite false x$ ?x224) ?x224)) (= ?x226 ?x224)) (= $x227 (= ?x29 ?x224)))))
+(let ((@x270 (monotonicity (trans @x257 (rewrite (= (= ?x29 ?x224) $x260)) (= $x227 $x260)) (= (or (not $x201) $x227) $x266))))
+(let ((@x273 (trans @x270 (rewrite (= $x266 $x266)) (= (or (not $x201) $x227) $x266))))
+(let ((@x274 (mp ((_ quant-inst x$ 2) (or (not $x201) $x227)) @x273 $x266)))
+(let ((@x336 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x260) $x275)) (unit-resolution @x274 @x206 $x260) $x275)))
+(let (($x63 (>= ?x29 2)))
+(let ((?x37 (* 2 ?x29)))
+(let (($x56 (>= ?x37 3)))
+(let (($x46 (< (+ x$ ?x37) (+ 3 x$))))
+(let (($x49 (not $x46)))
+(let ((@x58 (monotonicity (rewrite (= $x46 (not $x56))) (= $x49 (not (not $x56))))))
+(let ((@x67 (trans (trans @x58 (rewrite (= (not (not $x56)) $x56)) (= $x49 $x56)) (rewrite (= $x56 $x63)) (= $x49 $x63))))
+(let ((@x42 (monotonicity (rewrite (= (+ ?x29 ?x29) ?x37)) (= (+ x$ (+ ?x29 ?x29)) (+ x$ ?x37)))))
+(let ((@x48 (monotonicity @x42 (rewrite (= (+ x$ 3) (+ 3 x$))) (= (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)) $x46))))
+(let ((@x51 (monotonicity @x48 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x49))))
+(let ((@x69 (trans @x51 @x67 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x63))))
+(let ((@x70 (mp (asserted (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)))) @x69 $x63)))
+((_ th-lemma arith farkas -1 1 1) @x70 @x336 (unit-resolution ((_ th-lemma arith) (or false $x319)) (true-axiom true) $x319) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+1880f0ed1cb3d1cfa006dff17f1b5553ce3a5158 236 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x410 (div n$ 2)))
+(let ((?x704 (* (- 1) ?x410)))
+(let ((?x381 (div n$ 4)))
+(let ((?x601 (* (- 2) ?x381)))
+(let ((?x329 (mod n$ 4)))
+(let ((?x363 (* (- 1) ?x329)))
+(let ((?x35 (mod$ n$ 4)))
+(let ((?x705 (+ n$ ?x35 ?x363 ?x601 ?x704)))
+(let (($x706 (>= ?x705 2)))
+(let ((?x39 (mod$ n$ 2)))
+(let (($x515 (>= ?x39 1)))
+(let (($x725 (not $x515)))
+(let (($x514 (<= ?x39 1)))
+(let ((?x519 (mod n$ 2)))
+(let ((?x534 (* (- 1) ?x519)))
+(let ((?x535 (+ ?x39 ?x534)))
+(let (($x408 (<= ?x535 0)))
+(let (($x490 (= ?x535 0)))
+(let (($x191 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x108 (mod ?v0 ?v1)))
+(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?v1 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?v1 0)))
+(let ((?x147 (ite $x50 ?v0 ?x142)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x147))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x153 (forall ((?v0 Int) (?v1 Int) )(let ((?x108 (mod ?v0 ?v1)))
+(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?v1 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?v1 0)))
+(let ((?x147 (ite $x50 ?v0 ?x142)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x147))))))))))))
+))
+(let ((?x108 (mod ?1 ?0)))
+(let ((?x65 (* (- 1) ?0)))
+(let ((?x62 (* (- 1) ?1)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?0 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?0 0)))
+(let ((?x147 (ite $x50 ?1 ?x142)))
+(let ((?x107 (mod$ ?1 ?0)))
+(let (($x150 (= ?x107 ?x147)))
+(let (($x114 (forall ((?v0 Int) (?v1 Int) )(let (($x50 (= ?v1 0)))
+(let ((?x112 (ite $x50 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x112)))))
+))
+(let (($x136 (forall ((?v0 Int) (?v1 Int) )(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let ((?x108 (mod ?v0 ?v1)))
+(let (($x51 (< 0 ?v1)))
+(let ((?x127 (ite $x51 ?x108 ?x122)))
+(let (($x50 (= ?v1 0)))
+(let ((?x130 (ite $x50 ?v0 ?x127)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x130))))))))))))
+))
+(let ((@x141 (monotonicity (rewrite (= (< 0 ?0) (not $x83))) (= (ite (< 0 ?0) ?x108 ?x122) (ite (not $x83) ?x108 ?x122)))))
+(let ((@x146 (trans @x141 (rewrite (= (ite (not $x83) ?x108 ?x122) ?x142)) (= (ite (< 0 ?0) ?x108 ?x122) ?x142))))
+(let ((@x149 (monotonicity @x146 (= (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122)) ?x147))))
+(let ((@x152 (monotonicity @x149 (= (= ?x107 (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122))) $x150))))
+(let (($x51 (< 0 ?0)))
+(let ((?x127 (ite $x51 ?x108 ?x122)))
+(let ((?x130 (ite $x50 ?1 ?x127)))
+(let (($x133 (= ?x107 ?x130)))
+(let (($x134 (= (= ?x107 (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))))) $x133)))
+(let ((@x118 (monotonicity (rewrite (= (- ?1) ?x62)) (rewrite (= (- ?0) ?x65)) (= (mod (- ?1) (- ?0)) ?x116))))
+(let ((@x126 (trans (monotonicity @x118 (= (- (mod (- ?1) (- ?0))) (- ?x116))) (rewrite (= (- ?x116) ?x122)) (= (- (mod (- ?1) (- ?0))) ?x122))))
+(let ((@x129 (monotonicity @x126 (= (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))) ?x127))))
+(let ((@x132 (monotonicity @x129 (= (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0))))) ?x130))))
+(let ((@x157 (trans (quant-intro (monotonicity @x132 $x134) (= $x114 $x136)) (quant-intro @x152 (= $x136 $x153)) (= $x114 $x153))))
+(let ((@x168 (mp~ (mp (asserted $x114) @x157 $x153) (nnf-pos (refl (~ $x150 $x150)) (~ $x153 $x153)) $x153)))
+(let ((@x196 (mp @x168 (quant-intro (refl (= $x150 $x150)) (= $x153 $x191)) $x191)))
+(let (($x260 (not $x191)))
+(let (($x541 (or $x260 $x490)))
+(let ((?x211 (* (- 1) 2)))
+(let ((?x222 (* (- 1) n$)))
+(let ((?x517 (mod ?x222 ?x211)))
+(let ((?x518 (* (- 1) ?x517)))
+(let (($x209 (<= 2 0)))
+(let ((?x520 (ite $x209 ?x518 ?x519)))
+(let (($x208 (= 2 0)))
+(let ((?x521 (ite $x208 n$ ?x520)))
+(let (($x485 (= ?x39 ?x521)))
+(let ((@x593 (monotonicity (monotonicity (rewrite (= ?x211 (- 2))) (= ?x517 (mod ?x222 (- 2)))) (= ?x518 (* (- 1) (mod ?x222 (- 2)))))))
+(let ((@x221 (rewrite (= $x209 false))))
+(let ((@x596 (monotonicity @x221 @x593 (= ?x520 (ite false (* (- 1) (mod ?x222 (- 2))) ?x519)))))
+(let ((@x599 (trans @x596 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 2))) ?x519) ?x519)) (= ?x520 ?x519))))
+(let ((@x219 (rewrite (= $x208 false))))
+(let ((@x487 (trans (monotonicity @x219 @x599 (= ?x521 (ite false n$ ?x519))) (rewrite (= (ite false n$ ?x519) ?x519)) (= ?x521 ?x519))))
+(let ((@x538 (trans (monotonicity @x487 (= $x485 (= ?x39 ?x519))) (rewrite (= (= ?x39 ?x519) $x490)) (= $x485 $x490))))
+(let ((@x406 (trans (monotonicity @x538 (= (or $x260 $x485) $x541)) (rewrite (= $x541 $x541)) (= (or $x260 $x485) $x541))))
+(let ((@x407 (mp ((_ quant-inst n$ 2) (or $x260 $x485)) @x406 $x541)))
+(let ((@x715 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x408)) (unit-resolution @x407 @x196 $x490) $x408)))
+(let (($x303 (>= ?x519 2)))
+(let (($x304 (not $x303)))
+(let ((@x26 (true-axiom true)))
+(let ((@x722 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x514 $x303 (not $x408))) (unit-resolution ((_ th-lemma arith) (or false $x304)) @x26 $x304) @x715 $x514)))
+(let (($x41 (= ?x39 1)))
+(let (($x169 (not $x41)))
+(let ((?x42 (mod$ m$ 2)))
+(let (($x43 (= ?x42 1)))
+(let ((?x29 (+ n$ m$)))
+(let ((?x214 (mod ?x29 2)))
+(let ((?x253 (* (- 1) ?x214)))
+(let ((?x31 (mod$ ?x29 2)))
+(let ((?x603 (+ n$ m$ ?x31 ?x35 ?x253 (* (- 1) (div ?x29 2)) ?x363 ?x601 (* (- 1) (div m$ 2)))))
+(let (($x604 (>= ?x603 2)))
+(let (($x523 (>= ?x42 1)))
+(let (($x609 (not $x523)))
+(let (($x522 (<= ?x42 1)))
+(let ((?x439 (mod m$ 2)))
+(let ((?x466 (* (- 1) ?x439)))
+(let ((?x467 (+ ?x42 ?x466)))
+(let (($x482 (<= ?x467 0)))
+(let (($x468 (= ?x467 0)))
+(let (($x473 (or $x260 $x468)))
+(let ((?x440 (ite $x209 (* (- 1) (mod (* (- 1) m$) ?x211)) ?x439)))
+(let ((?x441 (ite $x208 m$ ?x440)))
+(let (($x442 (= ?x42 ?x441)))
+(let ((@x453 (rewrite (= (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439) ?x439))))
+(let (($x447 (= (* (- 1) (mod (* (- 1) m$) ?x211)) (* (- 1) (mod (* (- 1) m$) (- 2))))))
+(let ((@x229 (rewrite (= ?x211 (- 2)))))
+(let ((@x445 (monotonicity @x229 (= (mod (* (- 1) m$) ?x211) (mod (* (- 1) m$) (- 2))))))
+(let ((@x451 (monotonicity @x221 (monotonicity @x445 $x447) (= ?x440 (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439)))))
+(let ((@x458 (monotonicity @x219 (trans @x451 @x453 (= ?x440 ?x439)) (= ?x441 (ite false m$ ?x439)))))
+(let ((@x465 (monotonicity (trans @x458 (rewrite (= (ite false m$ ?x439) ?x439)) (= ?x441 ?x439)) (= $x442 (= ?x42 ?x439)))))
+(let ((@x477 (monotonicity (trans @x465 (rewrite (= (= ?x42 ?x439) $x468)) (= $x442 $x468)) (= (or $x260 $x442) $x473))))
+(let ((@x481 (mp ((_ quant-inst m$ 2) (or $x260 $x442)) (trans @x477 (rewrite (= $x473 $x473)) (= (or $x260 $x442) $x473)) $x473)))
+(let ((@x277 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) $x482)) (unit-resolution @x481 @x196 $x468) $x482)))
+(let ((@x386 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x439 2)))) @x26 (not (>= ?x439 2)))))
+(let ((@x384 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x522 (>= ?x439 2) (not $x482))) @x386 @x277 $x522)))
+(let ((@x564 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x43 (not $x522) $x609)) (hypothesis (not $x43)) (or (not $x522) $x609))))
+(let ((?x272 (div ?x29 2)))
+(let ((?x288 (* (- 2) ?x272)))
+(let ((?x289 (+ n$ m$ ?x253 ?x288)))
+(let (($x294 (<= ?x289 0)))
+(let (($x287 (= ?x289 0)))
+(let ((@x617 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x294)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x294)))
+(let (($x433 (<= ?x31 0)))
+(let (($x32 (= ?x31 0)))
+(let ((@x33 (asserted $x32)))
+(let ((?x254 (+ ?x31 ?x253)))
+(let (($x270 (<= ?x254 0)))
+(let (($x255 (= ?x254 0)))
+(let (($x261 (or $x260 $x255)))
+(let ((?x215 (ite $x209 (* (- 1) (mod (* (- 1) ?x29) ?x211)) ?x214)))
+(let ((?x216 (ite $x208 ?x29 ?x215)))
+(let (($x217 (= ?x31 ?x216)))
+(let (($x239 (= (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214) ?x214)))
+(let (($x237 (= ?x215 (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214))))
+(let (($x234 (= (* (- 1) (mod (* (- 1) ?x29) ?x211)) (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
+(let ((@x232 (monotonicity (rewrite (= (* (- 1) ?x29) (+ ?x222 (* (- 1) m$)))) @x229 (= (mod (* (- 1) ?x29) ?x211) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
+(let ((@x242 (trans (monotonicity @x221 (monotonicity @x232 $x234) $x237) (rewrite $x239) (= ?x215 ?x214))))
+(let ((@x249 (trans (monotonicity @x219 @x242 (= ?x216 (ite false ?x29 ?x214))) (rewrite (= (ite false ?x29 ?x214) ?x214)) (= ?x216 ?x214))))
+(let ((@x259 (trans (monotonicity @x249 (= $x217 (= ?x31 ?x214))) (rewrite (= (= ?x31 ?x214) $x255)) (= $x217 $x255))))
+(let ((@x268 (trans (monotonicity @x259 (= (or $x260 $x217) $x261)) (rewrite (= $x261 $x261)) (= (or $x260 $x217) $x261))))
+(let ((@x269 (mp ((_ quant-inst (+ n$ m$) 2) (or $x260 $x217)) @x268 $x261)))
+(let ((@x626 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x270)) (unit-resolution @x269 @x196 $x255) $x270)))
+(let ((?x498 (+ m$ ?x466 (* (- 2) (div m$ 2)))))
+(let (($x496 (= ?x498 0)))
+(let ((@x633 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x496) (<= ?x498 0))) (unit-resolution ((_ th-lemma arith) (or false $x496)) @x26 $x496) (<= ?x498 0))))
+(let ((?x397 (* (- 4) ?x381)))
+(let ((?x398 (+ n$ ?x363 ?x397)))
+(let (($x403 (<= ?x398 0)))
+(let (($x396 (= ?x398 0)))
+(let ((@x640 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x403)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x403)))
+(let ((?x364 (+ ?x35 ?x363)))
+(let (($x379 (<= ?x364 0)))
+(let (($x365 (= ?x364 0)))
+(let (($x370 (or $x260 $x365)))
+(let ((?x330 (ite (<= 4 0) (* (- 1) (mod ?x222 (* (- 1) 4))) ?x329)))
+(let ((?x331 (ite (= 4 0) n$ ?x330)))
+(let (($x332 (= ?x35 ?x331)))
+(let ((@x342 (monotonicity (rewrite (= (* (- 1) 4) (- 4))) (= (mod ?x222 (* (- 1) 4)) (mod ?x222 (- 4))))))
+(let ((@x345 (monotonicity @x342 (= (* (- 1) (mod ?x222 (* (- 1) 4))) (* (- 1) (mod ?x222 (- 4)))))))
+(let ((@x348 (monotonicity (rewrite (= (<= 4 0) false)) @x345 (= ?x330 (ite false (* (- 1) (mod ?x222 (- 4))) ?x329)))))
+(let ((@x352 (trans @x348 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 4))) ?x329) ?x329)) (= ?x330 ?x329))))
+(let ((@x355 (monotonicity (rewrite (= (= 4 0) false)) @x352 (= ?x331 (ite false n$ ?x329)))))
+(let ((@x362 (monotonicity (trans @x355 (rewrite (= (ite false n$ ?x329) ?x329)) (= ?x331 ?x329)) (= $x332 (= ?x35 ?x329)))))
+(let ((@x374 (monotonicity (trans @x362 (rewrite (= (= ?x35 ?x329) $x365)) (= $x332 $x365)) (= (or $x260 $x332) $x370))))
+(let ((@x378 (mp ((_ quant-inst n$ 4) (or $x260 $x332)) (trans @x374 (rewrite (= $x370 $x370)) (= (or $x260 $x332) $x370)) $x370)))
+(let ((@x645 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x379)) (unit-resolution @x378 @x196 $x365) $x379)))
+(let (($x435 (<= ?x35 3)))
+(let (($x37 (= ?x35 3)))
+(let ((@x38 (asserted $x37)))
+(let ((@x655 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) (>= ?x467 0))) (unit-resolution @x481 @x196 $x468) (>= ?x467 0))))
+(let ((@x656 ((_ th-lemma arith farkas -1 1 -2 1 1 1 1 1 1 1) @x655 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x435)) @x38 $x435) (hypothesis $x604) @x645 @x640 @x633 @x626 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x32) $x433)) @x33 $x433) @x617 (hypothesis $x609) false)))
+(let ((@x565 (unit-resolution (lemma @x656 (or (not $x604) $x523)) (unit-resolution @x564 @x384 $x609) (not $x604))))
+(let (($x295 (>= ?x289 0)))
+(let ((@x566 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x295)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x295)))
+(let (($x434 (>= ?x31 0)))
+(let (($x271 (>= ?x254 0)))
+(let ((@x531 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x271)) (unit-resolution @x269 @x196 $x255) $x271)))
+(let ((@x537 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x496) (>= ?x498 0))) (unit-resolution ((_ th-lemma arith) (or false $x496)) @x26 $x496) (>= ?x498 0))))
+(let ((@x549 (unit-resolution ((_ th-lemma arith) (or false (>= ?x439 0))) @x26 (>= ?x439 0))))
+(let (($x404 (>= ?x398 0)))
+(let ((@x552 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x404)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x404)))
+(let (($x380 (>= ?x364 0)))
+(let ((@x273 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x380)) (unit-resolution @x378 @x196 $x365) $x380)))
+(let (($x436 (>= ?x35 3)))
+(let ((@x545 ((_ th-lemma arith farkas -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 1) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x436)) @x38 $x436) @x273 @x552 @x549 @x537 @x531 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x32) $x434)) @x33 $x434) @x566 @x565 false)))
+(let (($x171 (or $x169 (not $x43))))
+(let ((@x177 (monotonicity (rewrite (= (and $x41 $x43) (not $x171))) (= (not (and $x41 $x43)) (not (not $x171))))))
+(let ((@x181 (trans @x177 (rewrite (= (not (not $x171)) $x171)) (= (not (and $x41 $x43)) $x171))))
+(let ((@x182 (mp (asserted (not (and $x41 $x43))) @x181 $x171)))
+(let ((@x729 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x41 (not $x514) $x725)) (unit-resolution @x182 (lemma @x545 $x43) $x169) (or (not $x514) $x725))))
+(let ((?x420 (* (- 2) ?x410)))
+(let ((?x421 (+ n$ ?x420 ?x534)))
+(let (($x426 (<= ?x421 0)))
+(let (($x419 (= ?x421 0)))
+(let ((@x737 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x426)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x426)))
+(let (($x409 (>= ?x535 0)))
+(let ((@x741 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x409)) (unit-resolution @x407 @x196 $x490) $x409)))
+(let ((@x742 ((_ th-lemma arith farkas -1 1 -2 1 1 1 1) @x741 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x435)) @x38 $x435) (hypothesis $x706) @x640 @x737 @x645 (unit-resolution @x729 @x722 $x725) false)))
+(let (($x427 (>= ?x421 0)))
+(let ((@x584 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x427)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x427)))
+(let (($x542 (>= ?x519 0)))
+((_ th-lemma arith farkas -1/2 -1/2 -1/2 -1/2 -1/2 1) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x436)) @x38 $x436) @x552 (unit-resolution ((_ th-lemma arith) (or false $x542)) @x26 $x542) @x584 @x273 (lemma @x742 (not $x706)) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+f6a4c40290fd6742c0b08a1fe90b3664e90c2143 336 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x99 (mod$ l$ 2)))
+(let ((?x96 (map$ uu$ xs$)))
+(let ((?x97 (eval_dioph$ ks$ ?x96)))
+(let ((?x98 (mod$ ?x97 2)))
+(let (($x100 (= ?x98 ?x99)))
+(let ((?x93 (eval_dioph$ ks$ xs$)))
+(let (($x95 (= ?x93 l$)))
+(let ((?x110 (* (- 1) ?x97)))
+(let ((?x111 (+ l$ ?x110)))
+(let ((?x114 (divide$ ?x111 2)))
+(let ((?x101 (map$ uua$ xs$)))
+(let ((?x102 (eval_dioph$ ks$ ?x101)))
+(let (($x117 (= ?x102 ?x114)))
+(let (($x282 (not $x117)))
+(let (($x281 (not $x100)))
+(let (($x283 (or $x281 $x282)))
+(let ((?x744 (div ?x93 2)))
+(let ((?x970 (* (- 1) ?x744)))
+(let ((?x699 (mod ?x93 2)))
+(let ((?x726 (* (- 1) ?x699)))
+(let ((?x516 (mod l$ 2)))
+(let ((?x543 (* (- 1) ?x516)))
+(let (($x972 (>= (+ l$ ?x99 ?x543 (* (- 1) (div l$ 2)) ?x726 ?x970) 1)))
+(let ((?x369 (* (- 1) l$)))
+(let ((?x693 (+ ?x93 ?x369)))
+(let (($x695 (>= ?x693 0)))
+(let (($x861 (not $x695)))
+(let (($x694 (<= ?x693 0)))
+(let ((?x686 (+ ?x102 (* (- 1) ?x114))))
+(let (($x687 (<= ?x686 0)))
+(let (($x284 (not $x283)))
+(let ((@x466 (hypothesis $x284)))
+(let ((@x856 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x687)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x687)))
+(let ((?x437 (+ l$ ?x110 (* (- 2) (div ?x111 2)) (* (- 1) (mod (+ l$ ?x97) 2)))))
+(let (($x443 (>= ?x437 0)))
+(let (($x434 (= ?x437 0)))
+(let ((@x26 (true-axiom true)))
+(let ((@x793 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x443)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x443)))
+(let ((?x501 (* (- 2) ?x102)))
+(let ((?x502 (+ ?x93 ?x110 ?x501)))
+(let (($x509 (<= ?x502 0)))
+(let (($x503 (= ?x502 0)))
+(let (($x304 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :pattern ( (eval_dioph$ ?v0 (map$ uua$ ?v1)) )))
+))
+(let (($x85 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))))
+))
+(let ((?x45 (eval_dioph$ ?1 ?0)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?1 (map$ uu$ ?0))) (* (- 2) (eval_dioph$ ?1 (map$ uua$ ?0))))))
+(let (($x79 (= ?x83 0)))
+(let (($x58 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x56 (+ (* (eval_dioph$ ?v0 (map$ uua$ ?v1)) 2) ?x48)))
+(= ?x56 ?x45)))))
+))
+(let (($x74 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x54 (eval_dioph$ ?v0 (map$ uua$ ?v1))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x66 (+ ?x48 ?x60)))
+(= ?x66 ?x45)))))))
+))
+(let ((?x54 (eval_dioph$ ?1 (map$ uua$ ?0))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?1 (map$ uu$ ?0))))
+(let ((?x66 (+ ?x48 ?x60)))
+(let (($x71 (= ?x66 ?x45)))
+(let ((@x65 (monotonicity (rewrite (= (* ?x54 2) ?x60)) (= (+ (* ?x54 2) ?x48) (+ ?x60 ?x48)))))
+(let ((@x70 (trans @x65 (rewrite (= (+ ?x60 ?x48) ?x66)) (= (+ (* ?x54 2) ?x48) ?x66))))
+(let ((@x76 (quant-intro (monotonicity @x70 (= (= (+ (* ?x54 2) ?x48) ?x45) $x71)) (= $x58 $x74))))
+(let ((@x89 (trans @x76 (quant-intro (rewrite (= $x71 $x79)) (= $x74 $x85)) (= $x58 $x85))))
+(let ((@x270 (mp~ (mp (asserted $x58) @x89 $x85) (nnf-pos (refl (~ $x79 $x79)) (~ $x85 $x85)) $x85)))
+(let ((@x309 (mp @x270 (quant-intro (refl (= $x79 $x79)) (= $x85 $x304)) $x304)))
+(let (($x507 (or (not $x304) $x503)))
+(let ((@x508 ((_ quant-inst ks$ xs$) $x507)))
+(let ((@x800 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x509)) (unit-resolution @x508 @x309 $x503) $x509)))
+(let ((?x396 (+ ?x114 (* (- 1) (div ?x111 2)))))
+(let (($x413 (<= ?x396 0)))
+(let (($x397 (= ?x396 0)))
+(let (($x311 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))) :pattern ( (divide$ ?v0 ?v1) )))
+))
+(let (($x193 (forall ((?v0 Int) (?v1 Int) )(let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))))
+))
+(let ((?x145 (div ?1 ?0)))
+(let ((?x157 (* (- 1) ?0)))
+(let ((?x154 (* (- 1) ?1)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?0 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?0 0)))
+(let ((?x141 (divide$ ?1 ?0)))
+(let (($x190 (= ?x141 (ite $x143 0 ?x182))))
+(let (($x152 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
+(let ((?x150 (ite $x143 0 (ite (< 0 ?v1) (div ?v0 ?v1) (div (- ?v0) (- ?v1))))))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 ?x150)))))
+))
+(let (($x172 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let ((?x145 (div ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let (($x143 (= ?v1 0)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 ?x166)))))))))))
+))
+(let (($x144 (< 0 ?0)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let ((@x181 (monotonicity (rewrite (= $x144 (not $x175))) (= ?x163 (ite (not $x175) ?x145 ?x160)))))
+(let ((@x186 (trans @x181 (rewrite (= (ite (not $x175) ?x145 ?x160) ?x182)) (= ?x163 ?x182))))
+(let ((@x192 (monotonicity (monotonicity @x186 (= ?x166 (ite $x143 0 ?x182))) (= (= ?x141 ?x166) $x190))))
+(let (($x169 (= ?x141 ?x166)))
+(let (($x170 (= (= ?x141 (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0))))) $x169)))
+(let ((@x162 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (div (- ?1) (- ?0)) ?x160))))
+(let ((@x168 (monotonicity (monotonicity @x162 (= (ite $x144 ?x145 (div (- ?1) (- ?0))) ?x163)) (= (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0)))) ?x166))))
+(let ((@x197 (trans (quant-intro (monotonicity @x168 $x170) (= $x152 $x172)) (quant-intro @x192 (= $x172 $x193)) (= $x152 $x193))))
+(let ((@x275 (mp~ (mp (asserted $x152) @x197 $x193) (nnf-pos (refl (~ $x190 $x190)) (~ $x193 $x193)) $x193)))
+(let ((@x316 (mp @x275 (quant-intro (refl (= $x190 $x190)) (= $x193 $x311)) $x311)))
+(let (($x403 (or (not $x311) $x397)))
+(let ((?x361 (div ?x111 2)))
+(let (($x357 (<= 2 0)))
+(let ((?x362 (ite $x357 (div (* (- 1) ?x111) (* (- 1) 2)) ?x361)))
+(let (($x356 (= 2 0)))
+(let ((?x363 (ite $x356 0 ?x362)))
+(let (($x364 (= ?x114 ?x363)))
+(let ((@x374 (rewrite (= (* (- 1) 2) (- 2)))))
+(let ((@x377 (monotonicity (rewrite (= (* (- 1) ?x111) (+ ?x369 ?x97))) @x374 (= (div (* (- 1) ?x111) (* (- 1) 2)) (div (+ ?x369 ?x97) (- 2))))))
+(let ((@x368 (rewrite (= $x357 false))))
+(let ((@x380 (monotonicity @x368 @x377 (= ?x362 (ite false (div (+ ?x369 ?x97) (- 2)) ?x361)))))
+(let ((@x384 (trans @x380 (rewrite (= (ite false (div (+ ?x369 ?x97) (- 2)) ?x361) ?x361)) (= ?x362 ?x361))))
+(let ((@x366 (rewrite (= $x356 false))))
+(let ((@x391 (trans (monotonicity @x366 @x384 (= ?x363 (ite false 0 ?x361))) (rewrite (= (ite false 0 ?x361) ?x361)) (= ?x363 ?x361))))
+(let ((@x401 (trans (monotonicity @x391 (= $x364 (= ?x114 ?x361))) (rewrite (= (= ?x114 ?x361) $x397)) (= $x364 $x397))))
+(let ((@x410 (trans (monotonicity @x401 (= (or (not $x311) $x364) $x403)) (rewrite (= $x403 $x403)) (= (or (not $x311) $x364) $x403))))
+(let ((@x802 (unit-resolution (mp ((_ quant-inst (+ l$ ?x110) 2) (or (not $x311) $x364)) @x410 $x403) @x316 $x397)))
+(let ((?x425 (mod (+ l$ ?x97) 2)))
+(let (($x465 (>= ?x425 0)))
+(let ((@x810 ((_ th-lemma arith farkas 1 -2 -2 -1 1 1) (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) @x802 $x413) (hypothesis $x687) @x800 (hypothesis (not $x694)) @x793 false)))
+(let (($x134 (not $x95)))
+(let (($x290 (= $x95 $x283)))
+(let ((@x289 (monotonicity (rewrite (= (and $x100 $x117) $x284)) (= (= $x134 (and $x100 $x117)) (= $x134 $x284)))))
+(let ((@x294 (trans @x289 (rewrite (= (= $x134 $x284) $x290)) (= (= $x134 (and $x100 $x117)) $x290))))
+(let (($x120 (and $x100 $x117)))
+(let (($x135 (= $x134 $x120)))
+(let (($x107 (= $x95 (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))))))
+(let (($x108 (not $x107)))
+(let ((@x116 (monotonicity (rewrite (= (- l$ ?x97) ?x111)) (= (divide$ (- l$ ?x97) 2) ?x114))))
+(let ((@x122 (monotonicity (monotonicity @x116 (= (= ?x102 (divide$ (- l$ ?x97) 2)) $x117)) (= (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))) $x120))))
+(let ((@x130 (trans (monotonicity @x122 (= $x107 (= $x95 $x120))) (rewrite (= (= $x95 $x120) (= $x95 $x120))) (= $x107 (= $x95 $x120)))))
+(let ((@x139 (trans (monotonicity @x130 (= $x108 (not (= $x95 $x120)))) (rewrite (= (not (= $x95 $x120)) $x135)) (= $x108 $x135))))
+(let ((@x295 (mp (mp (asserted $x108) @x139 $x135) @x294 $x290)))
+(let ((@x344 (unit-resolution (def-axiom (or $x134 $x283 (not $x290))) @x295 (or $x134 $x283))))
+(let ((@x898 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x95 (not $x694) $x861)) (unit-resolution @x344 @x466 $x134) (or (not $x694) $x861))))
+(let ((@x899 (unit-resolution @x898 (unit-resolution (lemma @x810 (or $x694 (not $x687))) @x856 $x694) $x861)))
+(let ((?x544 (+ ?x99 ?x543)))
+(let (($x561 (>= ?x544 0)))
+(let (($x545 (= ?x544 0)))
+(let (($x318 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x245 (forall ((?v0 Int) (?v1 Int) )(let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))))
+))
+(let ((?x200 (mod ?1 ?0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let ((?x239 (ite $x143 ?1 ?x234)))
+(let ((?x199 (mod$ ?1 ?0)))
+(let (($x242 (= ?x199 ?x239)))
+(let (($x206 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
+(let ((?x204 (ite $x143 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x204)))))
+))
+(let (($x228 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let ((?x200 (mod ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let (($x143 (= ?v1 0)))
+(let ((?x222 (ite $x143 ?v0 ?x219)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x222))))))))))))
+))
+(let ((@x233 (monotonicity (rewrite (= $x144 (not $x175))) (= (ite $x144 ?x200 ?x214) (ite (not $x175) ?x200 ?x214)))))
+(let ((@x238 (trans @x233 (rewrite (= (ite (not $x175) ?x200 ?x214) ?x234)) (= (ite $x144 ?x200 ?x214) ?x234))))
+(let ((@x244 (monotonicity (monotonicity @x238 (= (ite $x143 ?1 (ite $x144 ?x200 ?x214)) ?x239)) (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 ?x214))) $x242))))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let ((?x222 (ite $x143 ?1 ?x219)))
+(let (($x225 (= ?x199 ?x222)))
+(let (($x226 (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))))) $x225)))
+(let ((@x210 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (mod (- ?1) (- ?0)) ?x208))))
+(let ((@x218 (trans (monotonicity @x210 (= (- (mod (- ?1) (- ?0))) (- ?x208))) (rewrite (= (- ?x208) ?x214)) (= (- (mod (- ?1) (- ?0))) ?x214))))
+(let ((@x221 (monotonicity @x218 (= (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))) ?x219))))
+(let ((@x224 (monotonicity @x221 (= (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0))))) ?x222))))
+(let ((@x249 (trans (quant-intro (monotonicity @x224 $x226) (= $x206 $x228)) (quant-intro @x244 (= $x228 $x245)) (= $x206 $x245))))
+(let ((@x280 (mp~ (mp (asserted $x206) @x249 $x245) (nnf-pos (refl (~ $x242 $x242)) (~ $x245 $x245)) $x245)))
+(let ((@x323 (mp @x280 (quant-intro (refl (= $x242 $x242)) (= $x245 $x318)) $x318)))
+(let (($x550 (not $x318)))
+(let (($x551 (or $x550 $x545)))
+(let ((?x359 (* (- 1) 2)))
+(let ((?x511 (mod ?x369 ?x359)))
+(let ((?x512 (* (- 1) ?x511)))
+(let ((?x517 (ite $x357 ?x512 ?x516)))
+(let ((?x518 (ite $x356 l$ ?x517)))
+(let (($x519 (= ?x99 ?x518)))
+(let ((@x525 (monotonicity (monotonicity @x374 (= ?x511 (mod ?x369 (- 2)))) (= ?x512 (* (- 1) (mod ?x369 (- 2)))))))
+(let ((@x528 (monotonicity @x368 @x525 (= ?x517 (ite false (* (- 1) (mod ?x369 (- 2))) ?x516)))))
+(let ((@x532 (trans @x528 (rewrite (= (ite false (* (- 1) (mod ?x369 (- 2))) ?x516) ?x516)) (= ?x517 ?x516))))
+(let ((@x539 (trans (monotonicity @x366 @x532 (= ?x518 (ite false l$ ?x516))) (rewrite (= (ite false l$ ?x516) ?x516)) (= ?x518 ?x516))))
+(let ((@x549 (trans (monotonicity @x539 (= $x519 (= ?x99 ?x516))) (rewrite (= (= ?x99 ?x516) $x545)) (= $x519 $x545))))
+(let ((@x558 (trans (monotonicity @x549 (= (or $x550 $x519) $x551)) (rewrite (= $x551 $x551)) (= (or $x550 $x519) $x551))))
+(let ((@x559 (mp ((_ quant-inst l$ 2) (or $x550 $x519)) @x558 $x551)))
+(let ((@x902 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x561)) (unit-resolution @x559 @x323 $x545) $x561)))
+(let ((?x757 (* (- 2) ?x744)))
+(let ((?x758 (+ ?x93 ?x726 ?x757)))
+(let (($x764 (>= ?x758 0)))
+(let (($x756 (= ?x758 0)))
+(let ((@x872 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x764)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x764)))
+(let ((?x562 (div l$ 2)))
+(let ((?x575 (* (- 2) ?x562)))
+(let ((?x576 (+ l$ ?x543 ?x575)))
+(let (($x582 (>= ?x576 0)))
+(let (($x574 (= ?x576 0)))
+(let ((@x880 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x582)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x582)))
+(let ((?x504 (mod$ ?x93 2)))
+(let ((?x727 (+ ?x504 ?x726)))
+(let (($x728 (= ?x727 0)))
+(let (($x733 (or $x550 $x728)))
+(let ((?x696 (* (- 1) ?x93)))
+(let ((?x697 (mod ?x696 ?x359)))
+(let ((?x698 (* (- 1) ?x697)))
+(let ((?x700 (ite $x357 ?x698 ?x699)))
+(let ((?x701 (ite $x356 ?x93 ?x700)))
+(let (($x702 (= ?x504 ?x701)))
+(let ((@x708 (monotonicity (monotonicity @x374 (= ?x697 (mod ?x696 (- 2)))) (= ?x698 (* (- 1) (mod ?x696 (- 2)))))))
+(let ((@x711 (monotonicity @x368 @x708 (= ?x700 (ite false (* (- 1) (mod ?x696 (- 2))) ?x699)))))
+(let ((@x715 (trans @x711 (rewrite (= (ite false (* (- 1) (mod ?x696 (- 2))) ?x699) ?x699)) (= ?x700 ?x699))))
+(let ((@x722 (trans (monotonicity @x366 @x715 (= ?x701 (ite false ?x93 ?x699))) (rewrite (= (ite false ?x93 ?x699) ?x699)) (= ?x701 ?x699))))
+(let ((@x732 (trans (monotonicity @x722 (= $x702 (= ?x504 ?x699))) (rewrite (= (= ?x504 ?x699) $x728)) (= $x702 $x728))))
+(let ((@x740 (trans (monotonicity @x732 (= (or $x550 $x702) $x733)) (rewrite (= $x733 $x733)) (= (or $x550 $x702) $x733))))
+(let ((@x427 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x728) (>= ?x727 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x550 $x702)) @x740 $x733) @x323 $x728) (>= ?x727 0))))
+(let ((?x783 (* (- 1) ?x504)))
+(let ((?x784 (+ ?x99 ?x783)))
+(let (($x786 (>= ?x784 0)))
+(let (($x782 (= ?x99 ?x504)))
+(let (($x821 (= ?x98 ?x504)))
+(let (($x505 (= ?x504 ?x98)))
+(let (($x297 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) )))
+))
+(let (($x51 (forall ((?v0 Int_list$) (?v1 Int_list$) )(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)))
+))
+(let (($x50 (= (mod$ ?x45 2) (mod$ ?x48 2))))
+(let ((@x265 (mp~ (asserted $x51) (nnf-pos (refl (~ $x50 $x50)) (~ $x51 $x51)) $x51)))
+(let ((@x302 (mp @x265 (quant-intro (refl (= $x50 $x50)) (= $x51 $x297)) $x297)))
+(let (($x514 (or (not $x297) $x505)))
+(let ((@x515 ((_ quant-inst ks$ xs$) $x514)))
+(let ((@x824 (symm (unit-resolution (def-axiom (or $x283 $x100)) @x466 $x100) (= ?x99 ?x98))))
+(let ((@x939 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x786)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x786)))
+(let (($x785 (<= ?x784 0)))
+(let ((@x887 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x785)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x785)))
+(let (($x688 (>= ?x686 0)))
+(let ((@x855 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x688)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x688)))
+(let ((@x979 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x425 2)))) @x26 (not (>= ?x425 2)))))
+(let (($x560 (<= ?x544 0)))
+(let ((@x461 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x560)) (unit-resolution @x559 @x323 $x545) $x560)))
+(let (($x763 (<= ?x758 0)))
+(let ((@x658 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x763)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x763)))
+(let (($x581 (<= ?x576 0)))
+(let ((@x986 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x581)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x581)))
+(let ((@x989 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x728) (<= ?x727 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x550 $x702)) @x740 $x733) @x323 $x728) (<= ?x727 0))))
+(let (($x510 (>= ?x502 0)))
+(let ((@x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x510)) (unit-resolution @x508 @x309 $x503) $x510)))
+(let ((@x998 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) (>= ?x396 0))) @x802 (>= ?x396 0))))
+(let ((@x1001 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) (<= ?x437 0))) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) (<= ?x437 0))))
+(let ((@x1002 ((_ th-lemma arith farkas 1 -2 -2 -1 -2 1 1 1 1 1 1) @x1001 @x998 (hypothesis $x688) @x994 (hypothesis $x972) (hypothesis $x785) @x989 @x986 @x658 @x461 @x979 false)))
+(let ((@x474 (unit-resolution (lemma @x1002 (or (not $x972) (not $x688) (not $x785))) @x855 @x887 (not $x972))))
+(let ((@x941 (unit-resolution @x474 ((_ th-lemma arith) @x939 @x427 @x880 @x872 @x902 @x899 $x972) false)))
+(let ((@x942 (lemma @x941 $x283)))
+(let ((@x340 (unit-resolution (def-axiom (or $x95 $x284 (not $x290))) @x295 (or $x95 $x284))))
+(let ((@x679 (unit-resolution @x340 @x942 $x95)))
+(let ((@x889 (trans (symm (unit-resolution @x515 @x302 $x505) $x821) (monotonicity @x679 (= ?x504 ?x99)) $x100)))
+(let (($x811 (not $x687)))
+(let ((@x845 ((_ th-lemma arith assign-bounds 1 -1/2 -1/2 1/2 -1/2) (or $x688 (not $x413) (not $x465) (not $x443) (not $x509) $x861))))
+(let ((@x892 (unit-resolution @x845 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) @x802 $x413) (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x695)) @x679 $x695) @x793 (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) @x800 $x688)))
+(let ((@x935 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x811 (not $x688))) (hypothesis $x282) (or $x811 (not $x688)))))
+(let ((@x955 ((_ th-lemma arith farkas -2 -2 1 -1 1 1) (unit-resolution @x935 @x892 $x811) @x998 @x1001 @x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x694)) @x679 $x694) @x979 false)))
+(let ((@x472 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x942 $x283) (lemma @x955 $x117) $x281)))
+(unit-resolution @x472 @x889 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+0f7f4a10f8a84029fd3a6efddc4408fa429b0cda 113 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x228 (mod x$ 2)))
+(let ((?x262 (* (- 1) ?x228)))
+(let ((?x31 (mod$ x$ 2)))
+(let ((?x263 (+ ?x31 ?x262)))
+(let (($x280 (>= ?x263 0)))
+(let (($x264 (= ?x263 0)))
+(let (($x205 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x136 (mod ?v0 ?v1)))
+(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?v1 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?v1 0)))
+(let ((?x175 (ite $x78 ?v0 ?x170)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x175))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x181 (forall ((?v0 Int) (?v1 Int) )(let ((?x136 (mod ?v0 ?v1)))
+(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?v1 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?v1 0)))
+(let ((?x175 (ite $x78 ?v0 ?x170)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x175))))))))))))
+))
+(let ((?x136 (mod ?1 ?0)))
+(let ((?x93 (* (- 1) ?0)))
+(let ((?x90 (* (- 1) ?1)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?0 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?0 0)))
+(let ((?x175 (ite $x78 ?1 ?x170)))
+(let ((?x135 (mod$ ?1 ?0)))
+(let (($x178 (= ?x135 ?x175)))
+(let (($x142 (forall ((?v0 Int) (?v1 Int) )(let (($x78 (= ?v1 0)))
+(let ((?x140 (ite $x78 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x140)))))
+))
+(let (($x164 (forall ((?v0 Int) (?v1 Int) )(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let ((?x136 (mod ?v0 ?v1)))
+(let (($x79 (< 0 ?v1)))
+(let ((?x155 (ite $x79 ?x136 ?x150)))
+(let (($x78 (= ?v1 0)))
+(let ((?x158 (ite $x78 ?v0 ?x155)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x158))))))))))))
+))
+(let ((@x169 (monotonicity (rewrite (= (< 0 ?0) (not $x111))) (= (ite (< 0 ?0) ?x136 ?x150) (ite (not $x111) ?x136 ?x150)))))
+(let ((@x174 (trans @x169 (rewrite (= (ite (not $x111) ?x136 ?x150) ?x170)) (= (ite (< 0 ?0) ?x136 ?x150) ?x170))))
+(let ((@x177 (monotonicity @x174 (= (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150)) ?x175))))
+(let ((@x180 (monotonicity @x177 (= (= ?x135 (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150))) $x178))))
+(let (($x79 (< 0 ?0)))
+(let ((?x155 (ite $x79 ?x136 ?x150)))
+(let ((?x158 (ite $x78 ?1 ?x155)))
+(let (($x161 (= ?x135 ?x158)))
+(let (($x162 (= (= ?x135 (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))))) $x161)))
+(let ((@x146 (monotonicity (rewrite (= (- ?1) ?x90)) (rewrite (= (- ?0) ?x93)) (= (mod (- ?1) (- ?0)) ?x144))))
+(let ((@x154 (trans (monotonicity @x146 (= (- (mod (- ?1) (- ?0))) (- ?x144))) (rewrite (= (- ?x144) ?x150)) (= (- (mod (- ?1) (- ?0))) ?x150))))
+(let ((@x157 (monotonicity @x154 (= (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))) ?x155))))
+(let ((@x160 (monotonicity @x157 (= (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0))))) ?x158))))
+(let ((@x185 (trans (quant-intro (monotonicity @x160 $x162) (= $x142 $x164)) (quant-intro @x180 (= $x164 $x181)) (= $x142 $x181))))
+(let ((@x196 (mp~ (mp (asserted $x142) @x185 $x181) (nnf-pos (refl (~ $x178 $x178)) (~ $x181 $x181)) $x181)))
+(let ((@x210 (mp @x196 (quant-intro (refl (= $x178 $x178)) (= $x181 $x205)) $x205)))
+(let (($x270 (or (not $x205) $x264)))
+(let ((?x225 (* (- 1) 2)))
+(let ((?x224 (* (- 1) x$)))
+(let ((?x226 (mod ?x224 ?x225)))
+(let ((?x227 (* (- 1) ?x226)))
+(let (($x223 (<= 2 0)))
+(let ((?x229 (ite $x223 ?x227 ?x228)))
+(let (($x222 (= 2 0)))
+(let ((?x230 (ite $x222 x$ ?x229)))
+(let (($x231 (= ?x31 ?x230)))
+(let ((@x244 (monotonicity (monotonicity (rewrite (= ?x225 (- 2))) (= ?x226 (mod ?x224 (- 2)))) (= ?x227 (* (- 1) (mod ?x224 (- 2)))))))
+(let ((@x247 (monotonicity (rewrite (= $x223 false)) @x244 (= ?x229 (ite false (* (- 1) (mod ?x224 (- 2))) ?x228)))))
+(let ((@x251 (trans @x247 (rewrite (= (ite false (* (- 1) (mod ?x224 (- 2))) ?x228) ?x228)) (= ?x229 ?x228))))
+(let ((@x254 (monotonicity (rewrite (= $x222 false)) @x251 (= ?x230 (ite false x$ ?x228)))))
+(let ((@x261 (monotonicity (trans @x254 (rewrite (= (ite false x$ ?x228) ?x228)) (= ?x230 ?x228)) (= $x231 (= ?x31 ?x228)))))
+(let ((@x274 (monotonicity (trans @x261 (rewrite (= (= ?x31 ?x228) $x264)) (= $x231 $x264)) (= (or (not $x205) $x231) $x270))))
+(let ((@x277 (trans @x274 (rewrite (= $x270 $x270)) (= (or (not $x205) $x231) $x270))))
+(let ((@x278 (mp ((_ quant-inst x$ 2) (or (not $x205) $x231)) @x277 $x270)))
+(let ((@x337 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x264) $x280)) (unit-resolution @x278 @x210 $x264) $x280)))
+(let (($x305 (>= ?x228 0)))
+(let (($x64 (>= ?x31 0)))
+(let (($x67 (not $x64)))
+(let (($x36 (not (<= (+ x$ 1) (+ x$ (+ (* 2 ?x31) 1))))))
+(let ((@x69 (monotonicity (rewrite (= (>= (* 2 ?x31) 0) $x64)) (= (not (>= (* 2 ?x31) 0)) $x67))))
+(let ((?x32 (* 2 ?x31)))
+(let ((?x47 (+ 1 x$ ?x32)))
+(let (($x52 (<= (+ 1 x$) ?x47)))
+(let (($x55 (not $x52)))
+(let ((@x63 (monotonicity (rewrite (= $x52 (>= ?x32 0))) (= $x55 (not (>= ?x32 0))))))
+(let ((@x46 (monotonicity (rewrite (= (+ ?x32 1) (+ 1 ?x32))) (= (+ x$ (+ ?x32 1)) (+ x$ (+ 1 ?x32))))))
+(let ((@x51 (trans @x46 (rewrite (= (+ x$ (+ 1 ?x32)) ?x47)) (= (+ x$ (+ ?x32 1)) ?x47))))
+(let ((@x54 (monotonicity (rewrite (= (+ x$ 1) (+ 1 x$))) @x51 (= (<= (+ x$ 1) (+ x$ (+ ?x32 1))) $x52))))
+(let ((@x73 (trans (monotonicity @x54 (= $x36 $x55)) (trans @x63 @x69 (= $x55 $x67)) (= $x36 $x67))))
+(let ((@x74 (mp (asserted $x36) @x73 $x67)))
+((_ th-lemma arith farkas -1 1 1) @x74 (unit-resolution ((_ th-lemma arith) (or false $x305)) (true-axiom true) $x305) @x337 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+fa5abc269019f00f5093218b287856c2a08c0adf 112 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x224 (mod x$ 2)))
+(let (($x318 (>= ?x224 2)))
+(let (($x319 (not $x318)))
+(let ((?x258 (* (- 1) ?x224)))
+(let ((?x29 (mod$ x$ 2)))
+(let ((?x259 (+ ?x29 ?x258)))
+(let (($x275 (<= ?x259 0)))
+(let (($x260 (= ?x259 0)))
+(let (($x201 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x132 (mod ?v0 ?v1)))
+(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?v1 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?v1 0)))
+(let ((?x171 (ite $x74 ?v0 ?x166)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x171))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x177 (forall ((?v0 Int) (?v1 Int) )(let ((?x132 (mod ?v0 ?v1)))
+(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?v1 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?v1 0)))
+(let ((?x171 (ite $x74 ?v0 ?x166)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x171))))))))))))
+))
+(let ((?x132 (mod ?1 ?0)))
+(let ((?x89 (* (- 1) ?0)))
+(let ((?x86 (* (- 1) ?1)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?0 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?0 0)))
+(let ((?x171 (ite $x74 ?1 ?x166)))
+(let ((?x131 (mod$ ?1 ?0)))
+(let (($x174 (= ?x131 ?x171)))
+(let (($x138 (forall ((?v0 Int) (?v1 Int) )(let (($x74 (= ?v1 0)))
+(let ((?x136 (ite $x74 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x136)))))
+))
+(let (($x160 (forall ((?v0 Int) (?v1 Int) )(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let ((?x132 (mod ?v0 ?v1)))
+(let (($x75 (< 0 ?v1)))
+(let ((?x151 (ite $x75 ?x132 ?x146)))
+(let (($x74 (= ?v1 0)))
+(let ((?x154 (ite $x74 ?v0 ?x151)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x154))))))))))))
+))
+(let ((@x165 (monotonicity (rewrite (= (< 0 ?0) (not $x107))) (= (ite (< 0 ?0) ?x132 ?x146) (ite (not $x107) ?x132 ?x146)))))
+(let ((@x170 (trans @x165 (rewrite (= (ite (not $x107) ?x132 ?x146) ?x166)) (= (ite (< 0 ?0) ?x132 ?x146) ?x166))))
+(let ((@x173 (monotonicity @x170 (= (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146)) ?x171))))
+(let ((@x176 (monotonicity @x173 (= (= ?x131 (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146))) $x174))))
+(let (($x75 (< 0 ?0)))
+(let ((?x151 (ite $x75 ?x132 ?x146)))
+(let ((?x154 (ite $x74 ?1 ?x151)))
+(let (($x157 (= ?x131 ?x154)))
+(let (($x158 (= (= ?x131 (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))))) $x157)))
+(let ((@x142 (monotonicity (rewrite (= (- ?1) ?x86)) (rewrite (= (- ?0) ?x89)) (= (mod (- ?1) (- ?0)) ?x140))))
+(let ((@x150 (trans (monotonicity @x142 (= (- (mod (- ?1) (- ?0))) (- ?x140))) (rewrite (= (- ?x140) ?x146)) (= (- (mod (- ?1) (- ?0))) ?x146))))
+(let ((@x153 (monotonicity @x150 (= (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))) ?x151))))
+(let ((@x156 (monotonicity @x153 (= (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0))))) ?x154))))
+(let ((@x181 (trans (quant-intro (monotonicity @x156 $x158) (= $x138 $x160)) (quant-intro @x176 (= $x160 $x177)) (= $x138 $x177))))
+(let ((@x192 (mp~ (mp (asserted $x138) @x181 $x177) (nnf-pos (refl (~ $x174 $x174)) (~ $x177 $x177)) $x177)))
+(let ((@x206 (mp @x192 (quant-intro (refl (= $x174 $x174)) (= $x177 $x201)) $x201)))
+(let (($x266 (or (not $x201) $x260)))
+(let ((?x221 (* (- 1) 2)))
+(let ((?x220 (* (- 1) x$)))
+(let ((?x222 (mod ?x220 ?x221)))
+(let ((?x223 (* (- 1) ?x222)))
+(let (($x219 (<= 2 0)))
+(let ((?x225 (ite $x219 ?x223 ?x224)))
+(let (($x218 (= 2 0)))
+(let ((?x226 (ite $x218 x$ ?x225)))
+(let (($x227 (= ?x29 ?x226)))
+(let ((@x240 (monotonicity (monotonicity (rewrite (= ?x221 (- 2))) (= ?x222 (mod ?x220 (- 2)))) (= ?x223 (* (- 1) (mod ?x220 (- 2)))))))
+(let ((@x243 (monotonicity (rewrite (= $x219 false)) @x240 (= ?x225 (ite false (* (- 1) (mod ?x220 (- 2))) ?x224)))))
+(let ((@x247 (trans @x243 (rewrite (= (ite false (* (- 1) (mod ?x220 (- 2))) ?x224) ?x224)) (= ?x225 ?x224))))
+(let ((@x250 (monotonicity (rewrite (= $x218 false)) @x247 (= ?x226 (ite false x$ ?x224)))))
+(let ((@x257 (monotonicity (trans @x250 (rewrite (= (ite false x$ ?x224) ?x224)) (= ?x226 ?x224)) (= $x227 (= ?x29 ?x224)))))
+(let ((@x270 (monotonicity (trans @x257 (rewrite (= (= ?x29 ?x224) $x260)) (= $x227 $x260)) (= (or (not $x201) $x227) $x266))))
+(let ((@x273 (trans @x270 (rewrite (= $x266 $x266)) (= (or (not $x201) $x227) $x266))))
+(let ((@x274 (mp ((_ quant-inst x$ 2) (or (not $x201) $x227)) @x273 $x266)))
+(let ((@x336 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x260) $x275)) (unit-resolution @x274 @x206 $x260) $x275)))
+(let (($x63 (>= ?x29 2)))
+(let ((?x37 (* 2 ?x29)))
+(let (($x56 (>= ?x37 3)))
+(let (($x46 (< (+ x$ ?x37) (+ 3 x$))))
+(let (($x49 (not $x46)))
+(let ((@x58 (monotonicity (rewrite (= $x46 (not $x56))) (= $x49 (not (not $x56))))))
+(let ((@x67 (trans (trans @x58 (rewrite (= (not (not $x56)) $x56)) (= $x49 $x56)) (rewrite (= $x56 $x63)) (= $x49 $x63))))
+(let ((@x42 (monotonicity (rewrite (= (+ ?x29 ?x29) ?x37)) (= (+ x$ (+ ?x29 ?x29)) (+ x$ ?x37)))))
+(let ((@x48 (monotonicity @x42 (rewrite (= (+ x$ 3) (+ 3 x$))) (= (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)) $x46))))
+(let ((@x51 (monotonicity @x48 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x49))))
+(let ((@x69 (trans @x51 @x67 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x63))))
+(let ((@x70 (mp (asserted (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)))) @x69 $x63)))
+((_ th-lemma arith farkas -1 1 1) @x70 @x336 (unit-resolution ((_ th-lemma arith) (or false $x319)) (true-axiom true) $x319) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+1880f0ed1cb3d1cfa006dff17f1b5553ce3a5158 236 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x410 (div n$ 2)))
+(let ((?x704 (* (- 1) ?x410)))
+(let ((?x381 (div n$ 4)))
+(let ((?x601 (* (- 2) ?x381)))
+(let ((?x329 (mod n$ 4)))
+(let ((?x363 (* (- 1) ?x329)))
+(let ((?x35 (mod$ n$ 4)))
+(let ((?x705 (+ n$ ?x35 ?x363 ?x601 ?x704)))
+(let (($x706 (>= ?x705 2)))
+(let ((?x39 (mod$ n$ 2)))
+(let (($x515 (>= ?x39 1)))
+(let (($x725 (not $x515)))
+(let (($x514 (<= ?x39 1)))
+(let ((?x519 (mod n$ 2)))
+(let ((?x534 (* (- 1) ?x519)))
+(let ((?x535 (+ ?x39 ?x534)))
+(let (($x408 (<= ?x535 0)))
+(let (($x490 (= ?x535 0)))
+(let (($x191 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x108 (mod ?v0 ?v1)))
+(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?v1 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?v1 0)))
+(let ((?x147 (ite $x50 ?v0 ?x142)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x147))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x153 (forall ((?v0 Int) (?v1 Int) )(let ((?x108 (mod ?v0 ?v1)))
+(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?v1 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?v1 0)))
+(let ((?x147 (ite $x50 ?v0 ?x142)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x147))))))))))))
+))
+(let ((?x108 (mod ?1 ?0)))
+(let ((?x65 (* (- 1) ?0)))
+(let ((?x62 (* (- 1) ?1)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?0 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?0 0)))
+(let ((?x147 (ite $x50 ?1 ?x142)))
+(let ((?x107 (mod$ ?1 ?0)))
+(let (($x150 (= ?x107 ?x147)))
+(let (($x114 (forall ((?v0 Int) (?v1 Int) )(let (($x50 (= ?v1 0)))
+(let ((?x112 (ite $x50 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x112)))))
+))
+(let (($x136 (forall ((?v0 Int) (?v1 Int) )(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let ((?x108 (mod ?v0 ?v1)))
+(let (($x51 (< 0 ?v1)))
+(let ((?x127 (ite $x51 ?x108 ?x122)))
+(let (($x50 (= ?v1 0)))
+(let ((?x130 (ite $x50 ?v0 ?x127)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x130))))))))))))
+))
+(let ((@x141 (monotonicity (rewrite (= (< 0 ?0) (not $x83))) (= (ite (< 0 ?0) ?x108 ?x122) (ite (not $x83) ?x108 ?x122)))))
+(let ((@x146 (trans @x141 (rewrite (= (ite (not $x83) ?x108 ?x122) ?x142)) (= (ite (< 0 ?0) ?x108 ?x122) ?x142))))
+(let ((@x149 (monotonicity @x146 (= (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122)) ?x147))))
+(let ((@x152 (monotonicity @x149 (= (= ?x107 (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122))) $x150))))
+(let (($x51 (< 0 ?0)))
+(let ((?x127 (ite $x51 ?x108 ?x122)))
+(let ((?x130 (ite $x50 ?1 ?x127)))
+(let (($x133 (= ?x107 ?x130)))
+(let (($x134 (= (= ?x107 (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))))) $x133)))
+(let ((@x118 (monotonicity (rewrite (= (- ?1) ?x62)) (rewrite (= (- ?0) ?x65)) (= (mod (- ?1) (- ?0)) ?x116))))
+(let ((@x126 (trans (monotonicity @x118 (= (- (mod (- ?1) (- ?0))) (- ?x116))) (rewrite (= (- ?x116) ?x122)) (= (- (mod (- ?1) (- ?0))) ?x122))))
+(let ((@x129 (monotonicity @x126 (= (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))) ?x127))))
+(let ((@x132 (monotonicity @x129 (= (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0))))) ?x130))))
+(let ((@x157 (trans (quant-intro (monotonicity @x132 $x134) (= $x114 $x136)) (quant-intro @x152 (= $x136 $x153)) (= $x114 $x153))))
+(let ((@x168 (mp~ (mp (asserted $x114) @x157 $x153) (nnf-pos (refl (~ $x150 $x150)) (~ $x153 $x153)) $x153)))
+(let ((@x196 (mp @x168 (quant-intro (refl (= $x150 $x150)) (= $x153 $x191)) $x191)))
+(let (($x260 (not $x191)))
+(let (($x541 (or $x260 $x490)))
+(let ((?x211 (* (- 1) 2)))
+(let ((?x222 (* (- 1) n$)))
+(let ((?x517 (mod ?x222 ?x211)))
+(let ((?x518 (* (- 1) ?x517)))
+(let (($x209 (<= 2 0)))
+(let ((?x520 (ite $x209 ?x518 ?x519)))
+(let (($x208 (= 2 0)))
+(let ((?x521 (ite $x208 n$ ?x520)))
+(let (($x485 (= ?x39 ?x521)))
+(let ((@x593 (monotonicity (monotonicity (rewrite (= ?x211 (- 2))) (= ?x517 (mod ?x222 (- 2)))) (= ?x518 (* (- 1) (mod ?x222 (- 2)))))))
+(let ((@x221 (rewrite (= $x209 false))))
+(let ((@x596 (monotonicity @x221 @x593 (= ?x520 (ite false (* (- 1) (mod ?x222 (- 2))) ?x519)))))
+(let ((@x599 (trans @x596 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 2))) ?x519) ?x519)) (= ?x520 ?x519))))
+(let ((@x219 (rewrite (= $x208 false))))
+(let ((@x487 (trans (monotonicity @x219 @x599 (= ?x521 (ite false n$ ?x519))) (rewrite (= (ite false n$ ?x519) ?x519)) (= ?x521 ?x519))))
+(let ((@x538 (trans (monotonicity @x487 (= $x485 (= ?x39 ?x519))) (rewrite (= (= ?x39 ?x519) $x490)) (= $x485 $x490))))
+(let ((@x406 (trans (monotonicity @x538 (= (or $x260 $x485) $x541)) (rewrite (= $x541 $x541)) (= (or $x260 $x485) $x541))))
+(let ((@x407 (mp ((_ quant-inst n$ 2) (or $x260 $x485)) @x406 $x541)))
+(let ((@x715 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x408)) (unit-resolution @x407 @x196 $x490) $x408)))
+(let (($x303 (>= ?x519 2)))
+(let (($x304 (not $x303)))
+(let ((@x26 (true-axiom true)))
+(let ((@x722 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x514 $x303 (not $x408))) (unit-resolution ((_ th-lemma arith) (or false $x304)) @x26 $x304) @x715 $x514)))
+(let (($x41 (= ?x39 1)))
+(let (($x169 (not $x41)))
+(let ((?x42 (mod$ m$ 2)))
+(let (($x43 (= ?x42 1)))
+(let ((?x29 (+ n$ m$)))
+(let ((?x214 (mod ?x29 2)))
+(let ((?x253 (* (- 1) ?x214)))
+(let ((?x31 (mod$ ?x29 2)))
+(let ((?x603 (+ n$ m$ ?x31 ?x35 ?x253 (* (- 1) (div ?x29 2)) ?x363 ?x601 (* (- 1) (div m$ 2)))))
+(let (($x604 (>= ?x603 2)))
+(let (($x523 (>= ?x42 1)))
+(let (($x609 (not $x523)))
+(let (($x522 (<= ?x42 1)))
+(let ((?x439 (mod m$ 2)))
+(let ((?x466 (* (- 1) ?x439)))
+(let ((?x467 (+ ?x42 ?x466)))
+(let (($x482 (<= ?x467 0)))
+(let (($x468 (= ?x467 0)))
+(let (($x473 (or $x260 $x468)))
+(let ((?x440 (ite $x209 (* (- 1) (mod (* (- 1) m$) ?x211)) ?x439)))
+(let ((?x441 (ite $x208 m$ ?x440)))
+(let (($x442 (= ?x42 ?x441)))
+(let ((@x453 (rewrite (= (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439) ?x439))))
+(let (($x447 (= (* (- 1) (mod (* (- 1) m$) ?x211)) (* (- 1) (mod (* (- 1) m$) (- 2))))))
+(let ((@x229 (rewrite (= ?x211 (- 2)))))
+(let ((@x445 (monotonicity @x229 (= (mod (* (- 1) m$) ?x211) (mod (* (- 1) m$) (- 2))))))
+(let ((@x451 (monotonicity @x221 (monotonicity @x445 $x447) (= ?x440 (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439)))))
+(let ((@x458 (monotonicity @x219 (trans @x451 @x453 (= ?x440 ?x439)) (= ?x441 (ite false m$ ?x439)))))
+(let ((@x465 (monotonicity (trans @x458 (rewrite (= (ite false m$ ?x439) ?x439)) (= ?x441 ?x439)) (= $x442 (= ?x42 ?x439)))))
+(let ((@x477 (monotonicity (trans @x465 (rewrite (= (= ?x42 ?x439) $x468)) (= $x442 $x468)) (= (or $x260 $x442) $x473))))
+(let ((@x481 (mp ((_ quant-inst m$ 2) (or $x260 $x442)) (trans @x477 (rewrite (= $x473 $x473)) (= (or $x260 $x442) $x473)) $x473)))
+(let ((@x277 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) $x482)) (unit-resolution @x481 @x196 $x468) $x482)))
+(let ((@x386 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x439 2)))) @x26 (not (>= ?x439 2)))))
+(let ((@x384 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x522 (>= ?x439 2) (not $x482))) @x386 @x277 $x522)))
+(let ((@x564 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x43 (not $x522) $x609)) (hypothesis (not $x43)) (or (not $x522) $x609))))
+(let ((?x272 (div ?x29 2)))
+(let ((?x288 (* (- 2) ?x272)))
+(let ((?x289 (+ n$ m$ ?x253 ?x288)))
+(let (($x294 (<= ?x289 0)))
+(let (($x287 (= ?x289 0)))
+(let ((@x617 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x294)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x294)))
+(let (($x433 (<= ?x31 0)))
+(let (($x32 (= ?x31 0)))
+(let ((@x33 (asserted $x32)))
+(let ((?x254 (+ ?x31 ?x253)))
+(let (($x270 (<= ?x254 0)))
+(let (($x255 (= ?x254 0)))
+(let (($x261 (or $x260 $x255)))
+(let ((?x215 (ite $x209 (* (- 1) (mod (* (- 1) ?x29) ?x211)) ?x214)))
+(let ((?x216 (ite $x208 ?x29 ?x215)))
+(let (($x217 (= ?x31 ?x216)))
+(let (($x239 (= (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214) ?x214)))
+(let (($x237 (= ?x215 (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214))))
+(let (($x234 (= (* (- 1) (mod (* (- 1) ?x29) ?x211)) (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
+(let ((@x232 (monotonicity (rewrite (= (* (- 1) ?x29) (+ ?x222 (* (- 1) m$)))) @x229 (= (mod (* (- 1) ?x29) ?x211) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
+(let ((@x242 (trans (monotonicity @x221 (monotonicity @x232 $x234) $x237) (rewrite $x239) (= ?x215 ?x214))))
+(let ((@x249 (trans (monotonicity @x219 @x242 (= ?x216 (ite false ?x29 ?x214))) (rewrite (= (ite false ?x29 ?x214) ?x214)) (= ?x216 ?x214))))
+(let ((@x259 (trans (monotonicity @x249 (= $x217 (= ?x31 ?x214))) (rewrite (= (= ?x31 ?x214) $x255)) (= $x217 $x255))))
+(let ((@x268 (trans (monotonicity @x259 (= (or $x260 $x217) $x261)) (rewrite (= $x261 $x261)) (= (or $x260 $x217) $x261))))
+(let ((@x269 (mp ((_ quant-inst (+ n$ m$) 2) (or $x260 $x217)) @x268 $x261)))
+(let ((@x626 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x270)) (unit-resolution @x269 @x196 $x255) $x270)))
+(let ((?x498 (+ m$ ?x466 (* (- 2) (div m$ 2)))))
+(let (($x496 (= ?x498 0)))
+(let ((@x633 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x496) (<= ?x498 0))) (unit-resolution ((_ th-lemma arith) (or false $x496)) @x26 $x496) (<= ?x498 0))))
+(let ((?x397 (* (- 4) ?x381)))
+(let ((?x398 (+ n$ ?x363 ?x397)))
+(let (($x403 (<= ?x398 0)))
+(let (($x396 (= ?x398 0)))
+(let ((@x640 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x403)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x403)))
+(let ((?x364 (+ ?x35 ?x363)))
+(let (($x379 (<= ?x364 0)))
+(let (($x365 (= ?x364 0)))
+(let (($x370 (or $x260 $x365)))
+(let ((?x330 (ite (<= 4 0) (* (- 1) (mod ?x222 (* (- 1) 4))) ?x329)))
+(let ((?x331 (ite (= 4 0) n$ ?x330)))
+(let (($x332 (= ?x35 ?x331)))
+(let ((@x342 (monotonicity (rewrite (= (* (- 1) 4) (- 4))) (= (mod ?x222 (* (- 1) 4)) (mod ?x222 (- 4))))))
+(let ((@x345 (monotonicity @x342 (= (* (- 1) (mod ?x222 (* (- 1) 4))) (* (- 1) (mod ?x222 (- 4)))))))
+(let ((@x348 (monotonicity (rewrite (= (<= 4 0) false)) @x345 (= ?x330 (ite false (* (- 1) (mod ?x222 (- 4))) ?x329)))))
+(let ((@x352 (trans @x348 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 4))) ?x329) ?x329)) (= ?x330 ?x329))))
+(let ((@x355 (monotonicity (rewrite (= (= 4 0) false)) @x352 (= ?x331 (ite false n$ ?x329)))))
+(let ((@x362 (monotonicity (trans @x355 (rewrite (= (ite false n$ ?x329) ?x329)) (= ?x331 ?x329)) (= $x332 (= ?x35 ?x329)))))
+(let ((@x374 (monotonicity (trans @x362 (rewrite (= (= ?x35 ?x329) $x365)) (= $x332 $x365)) (= (or $x260 $x332) $x370))))
+(let ((@x378 (mp ((_ quant-inst n$ 4) (or $x260 $x332)) (trans @x374 (rewrite (= $x370 $x370)) (= (or $x260 $x332) $x370)) $x370)))
+(let ((@x645 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x379)) (unit-resolution @x378 @x196 $x365) $x379)))
+(let (($x435 (<= ?x35 3)))
+(let (($x37 (= ?x35 3)))
+(let ((@x38 (asserted $x37)))
+(let ((@x655 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) (>= ?x467 0))) (unit-resolution @x481 @x196 $x468) (>= ?x467 0))))
+(let ((@x656 ((_ th-lemma arith farkas -1 1 -2 1 1 1 1 1 1 1) @x655 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x435)) @x38 $x435) (hypothesis $x604) @x645 @x640 @x633 @x626 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x32) $x433)) @x33 $x433) @x617 (hypothesis $x609) false)))
+(let ((@x565 (unit-resolution (lemma @x656 (or (not $x604) $x523)) (unit-resolution @x564 @x384 $x609) (not $x604))))
+(let (($x295 (>= ?x289 0)))
+(let ((@x566 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x295)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x295)))
+(let (($x434 (>= ?x31 0)))
+(let (($x271 (>= ?x254 0)))
+(let ((@x531 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x271)) (unit-resolution @x269 @x196 $x255) $x271)))
+(let ((@x537 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x496) (>= ?x498 0))) (unit-resolution ((_ th-lemma arith) (or false $x496)) @x26 $x496) (>= ?x498 0))))
+(let ((@x549 (unit-resolution ((_ th-lemma arith) (or false (>= ?x439 0))) @x26 (>= ?x439 0))))
+(let (($x404 (>= ?x398 0)))
+(let ((@x552 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x404)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x404)))
+(let (($x380 (>= ?x364 0)))
+(let ((@x273 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x380)) (unit-resolution @x378 @x196 $x365) $x380)))
+(let (($x436 (>= ?x35 3)))
+(let ((@x545 ((_ th-lemma arith farkas -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 1) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x436)) @x38 $x436) @x273 @x552 @x549 @x537 @x531 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x32) $x434)) @x33 $x434) @x566 @x565 false)))
+(let (($x171 (or $x169 (not $x43))))
+(let ((@x177 (monotonicity (rewrite (= (and $x41 $x43) (not $x171))) (= (not (and $x41 $x43)) (not (not $x171))))))
+(let ((@x181 (trans @x177 (rewrite (= (not (not $x171)) $x171)) (= (not (and $x41 $x43)) $x171))))
+(let ((@x182 (mp (asserted (not (and $x41 $x43))) @x181 $x171)))
+(let ((@x729 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x41 (not $x514) $x725)) (unit-resolution @x182 (lemma @x545 $x43) $x169) (or (not $x514) $x725))))
+(let ((?x420 (* (- 2) ?x410)))
+(let ((?x421 (+ n$ ?x420 ?x534)))
+(let (($x426 (<= ?x421 0)))
+(let (($x419 (= ?x421 0)))
+(let ((@x737 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x426)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x426)))
+(let (($x409 (>= ?x535 0)))
+(let ((@x741 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x409)) (unit-resolution @x407 @x196 $x490) $x409)))
+(let ((@x742 ((_ th-lemma arith farkas -1 1 -2 1 1 1 1) @x741 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x435)) @x38 $x435) (hypothesis $x706) @x640 @x737 @x645 (unit-resolution @x729 @x722 $x725) false)))
+(let (($x427 (>= ?x421 0)))
+(let ((@x584 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x427)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x427)))
+(let (($x542 (>= ?x519 0)))
+((_ th-lemma arith farkas -1/2 -1/2 -1/2 -1/2 -1/2 1) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x436)) @x38 $x436) @x552 (unit-resolution ((_ th-lemma arith) (or false $x542)) @x26 $x542) @x584 @x273 (lemma @x742 (not $x706)) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+f6a4c40290fd6742c0b08a1fe90b3664e90c2143 336 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x99 (mod$ l$ 2)))
+(let ((?x96 (map$ uu$ xs$)))
+(let ((?x97 (eval_dioph$ ks$ ?x96)))
+(let ((?x98 (mod$ ?x97 2)))
+(let (($x100 (= ?x98 ?x99)))
+(let ((?x93 (eval_dioph$ ks$ xs$)))
+(let (($x95 (= ?x93 l$)))
+(let ((?x110 (* (- 1) ?x97)))
+(let ((?x111 (+ l$ ?x110)))
+(let ((?x114 (divide$ ?x111 2)))
+(let ((?x101 (map$ uua$ xs$)))
+(let ((?x102 (eval_dioph$ ks$ ?x101)))
+(let (($x117 (= ?x102 ?x114)))
+(let (($x282 (not $x117)))
+(let (($x281 (not $x100)))
+(let (($x283 (or $x281 $x282)))
+(let ((?x744 (div ?x93 2)))
+(let ((?x970 (* (- 1) ?x744)))
+(let ((?x699 (mod ?x93 2)))
+(let ((?x726 (* (- 1) ?x699)))
+(let ((?x516 (mod l$ 2)))
+(let ((?x543 (* (- 1) ?x516)))
+(let (($x972 (>= (+ l$ ?x99 ?x543 (* (- 1) (div l$ 2)) ?x726 ?x970) 1)))
+(let ((?x369 (* (- 1) l$)))
+(let ((?x693 (+ ?x93 ?x369)))
+(let (($x695 (>= ?x693 0)))
+(let (($x861 (not $x695)))
+(let (($x694 (<= ?x693 0)))
+(let ((?x686 (+ ?x102 (* (- 1) ?x114))))
+(let (($x687 (<= ?x686 0)))
+(let (($x284 (not $x283)))
+(let ((@x466 (hypothesis $x284)))
+(let ((@x856 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x687)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x687)))
+(let ((?x437 (+ l$ ?x110 (* (- 2) (div ?x111 2)) (* (- 1) (mod (+ l$ ?x97) 2)))))
+(let (($x443 (>= ?x437 0)))
+(let (($x434 (= ?x437 0)))
+(let ((@x26 (true-axiom true)))
+(let ((@x793 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x443)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x443)))
+(let ((?x501 (* (- 2) ?x102)))
+(let ((?x502 (+ ?x93 ?x110 ?x501)))
+(let (($x509 (<= ?x502 0)))
+(let (($x503 (= ?x502 0)))
+(let (($x304 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :pattern ( (eval_dioph$ ?v0 (map$ uua$ ?v1)) )))
+))
+(let (($x85 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))))
+))
+(let ((?x45 (eval_dioph$ ?1 ?0)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?1 (map$ uu$ ?0))) (* (- 2) (eval_dioph$ ?1 (map$ uua$ ?0))))))
+(let (($x79 (= ?x83 0)))
+(let (($x58 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x56 (+ (* (eval_dioph$ ?v0 (map$ uua$ ?v1)) 2) ?x48)))
+(= ?x56 ?x45)))))
+))
+(let (($x74 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x54 (eval_dioph$ ?v0 (map$ uua$ ?v1))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x66 (+ ?x48 ?x60)))
+(= ?x66 ?x45)))))))
+))
+(let ((?x54 (eval_dioph$ ?1 (map$ uua$ ?0))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?1 (map$ uu$ ?0))))
+(let ((?x66 (+ ?x48 ?x60)))
+(let (($x71 (= ?x66 ?x45)))
+(let ((@x65 (monotonicity (rewrite (= (* ?x54 2) ?x60)) (= (+ (* ?x54 2) ?x48) (+ ?x60 ?x48)))))
+(let ((@x70 (trans @x65 (rewrite (= (+ ?x60 ?x48) ?x66)) (= (+ (* ?x54 2) ?x48) ?x66))))
+(let ((@x76 (quant-intro (monotonicity @x70 (= (= (+ (* ?x54 2) ?x48) ?x45) $x71)) (= $x58 $x74))))
+(let ((@x89 (trans @x76 (quant-intro (rewrite (= $x71 $x79)) (= $x74 $x85)) (= $x58 $x85))))
+(let ((@x270 (mp~ (mp (asserted $x58) @x89 $x85) (nnf-pos (refl (~ $x79 $x79)) (~ $x85 $x85)) $x85)))
+(let ((@x309 (mp @x270 (quant-intro (refl (= $x79 $x79)) (= $x85 $x304)) $x304)))
+(let (($x507 (or (not $x304) $x503)))
+(let ((@x508 ((_ quant-inst ks$ xs$) $x507)))
+(let ((@x800 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x509)) (unit-resolution @x508 @x309 $x503) $x509)))
+(let ((?x396 (+ ?x114 (* (- 1) (div ?x111 2)))))
+(let (($x413 (<= ?x396 0)))
+(let (($x397 (= ?x396 0)))
+(let (($x311 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))) :pattern ( (divide$ ?v0 ?v1) )))
+))
+(let (($x193 (forall ((?v0 Int) (?v1 Int) )(let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))))
+))
+(let ((?x145 (div ?1 ?0)))
+(let ((?x157 (* (- 1) ?0)))
+(let ((?x154 (* (- 1) ?1)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?0 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?0 0)))
+(let ((?x141 (divide$ ?1 ?0)))
+(let (($x190 (= ?x141 (ite $x143 0 ?x182))))
+(let (($x152 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
+(let ((?x150 (ite $x143 0 (ite (< 0 ?v1) (div ?v0 ?v1) (div (- ?v0) (- ?v1))))))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 ?x150)))))
+))
+(let (($x172 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let ((?x145 (div ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let (($x143 (= ?v1 0)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 ?x166)))))))))))
+))
+(let (($x144 (< 0 ?0)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let ((@x181 (monotonicity (rewrite (= $x144 (not $x175))) (= ?x163 (ite (not $x175) ?x145 ?x160)))))
+(let ((@x186 (trans @x181 (rewrite (= (ite (not $x175) ?x145 ?x160) ?x182)) (= ?x163 ?x182))))
+(let ((@x192 (monotonicity (monotonicity @x186 (= ?x166 (ite $x143 0 ?x182))) (= (= ?x141 ?x166) $x190))))
+(let (($x169 (= ?x141 ?x166)))
+(let (($x170 (= (= ?x141 (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0))))) $x169)))
+(let ((@x162 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (div (- ?1) (- ?0)) ?x160))))
+(let ((@x168 (monotonicity (monotonicity @x162 (= (ite $x144 ?x145 (div (- ?1) (- ?0))) ?x163)) (= (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0)))) ?x166))))
+(let ((@x197 (trans (quant-intro (monotonicity @x168 $x170) (= $x152 $x172)) (quant-intro @x192 (= $x172 $x193)) (= $x152 $x193))))
+(let ((@x275 (mp~ (mp (asserted $x152) @x197 $x193) (nnf-pos (refl (~ $x190 $x190)) (~ $x193 $x193)) $x193)))
+(let ((@x316 (mp @x275 (quant-intro (refl (= $x190 $x190)) (= $x193 $x311)) $x311)))
+(let (($x403 (or (not $x311) $x397)))
+(let ((?x361 (div ?x111 2)))
+(let (($x357 (<= 2 0)))
+(let ((?x362 (ite $x357 (div (* (- 1) ?x111) (* (- 1) 2)) ?x361)))
+(let (($x356 (= 2 0)))
+(let ((?x363 (ite $x356 0 ?x362)))
+(let (($x364 (= ?x114 ?x363)))
+(let ((@x374 (rewrite (= (* (- 1) 2) (- 2)))))
+(let ((@x377 (monotonicity (rewrite (= (* (- 1) ?x111) (+ ?x369 ?x97))) @x374 (= (div (* (- 1) ?x111) (* (- 1) 2)) (div (+ ?x369 ?x97) (- 2))))))
+(let ((@x368 (rewrite (= $x357 false))))
+(let ((@x380 (monotonicity @x368 @x377 (= ?x362 (ite false (div (+ ?x369 ?x97) (- 2)) ?x361)))))
+(let ((@x384 (trans @x380 (rewrite (= (ite false (div (+ ?x369 ?x97) (- 2)) ?x361) ?x361)) (= ?x362 ?x361))))
+(let ((@x366 (rewrite (= $x356 false))))
+(let ((@x391 (trans (monotonicity @x366 @x384 (= ?x363 (ite false 0 ?x361))) (rewrite (= (ite false 0 ?x361) ?x361)) (= ?x363 ?x361))))
+(let ((@x401 (trans (monotonicity @x391 (= $x364 (= ?x114 ?x361))) (rewrite (= (= ?x114 ?x361) $x397)) (= $x364 $x397))))
+(let ((@x410 (trans (monotonicity @x401 (= (or (not $x311) $x364) $x403)) (rewrite (= $x403 $x403)) (= (or (not $x311) $x364) $x403))))
+(let ((@x802 (unit-resolution (mp ((_ quant-inst (+ l$ ?x110) 2) (or (not $x311) $x364)) @x410 $x403) @x316 $x397)))
+(let ((?x425 (mod (+ l$ ?x97) 2)))
+(let (($x465 (>= ?x425 0)))
+(let ((@x810 ((_ th-lemma arith farkas 1 -2 -2 -1 1 1) (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) @x802 $x413) (hypothesis $x687) @x800 (hypothesis (not $x694)) @x793 false)))
+(let (($x134 (not $x95)))
+(let (($x290 (= $x95 $x283)))
+(let ((@x289 (monotonicity (rewrite (= (and $x100 $x117) $x284)) (= (= $x134 (and $x100 $x117)) (= $x134 $x284)))))
+(let ((@x294 (trans @x289 (rewrite (= (= $x134 $x284) $x290)) (= (= $x134 (and $x100 $x117)) $x290))))
+(let (($x120 (and $x100 $x117)))
+(let (($x135 (= $x134 $x120)))
+(let (($x107 (= $x95 (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))))))
+(let (($x108 (not $x107)))
+(let ((@x116 (monotonicity (rewrite (= (- l$ ?x97) ?x111)) (= (divide$ (- l$ ?x97) 2) ?x114))))
+(let ((@x122 (monotonicity (monotonicity @x116 (= (= ?x102 (divide$ (- l$ ?x97) 2)) $x117)) (= (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))) $x120))))
+(let ((@x130 (trans (monotonicity @x122 (= $x107 (= $x95 $x120))) (rewrite (= (= $x95 $x120) (= $x95 $x120))) (= $x107 (= $x95 $x120)))))
+(let ((@x139 (trans (monotonicity @x130 (= $x108 (not (= $x95 $x120)))) (rewrite (= (not (= $x95 $x120)) $x135)) (= $x108 $x135))))
+(let ((@x295 (mp (mp (asserted $x108) @x139 $x135) @x294 $x290)))
+(let ((@x344 (unit-resolution (def-axiom (or $x134 $x283 (not $x290))) @x295 (or $x134 $x283))))
+(let ((@x898 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x95 (not $x694) $x861)) (unit-resolution @x344 @x466 $x134) (or (not $x694) $x861))))
+(let ((@x899 (unit-resolution @x898 (unit-resolution (lemma @x810 (or $x694 (not $x687))) @x856 $x694) $x861)))
+(let ((?x544 (+ ?x99 ?x543)))
+(let (($x561 (>= ?x544 0)))
+(let (($x545 (= ?x544 0)))
+(let (($x318 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x245 (forall ((?v0 Int) (?v1 Int) )(let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))))
+))
+(let ((?x200 (mod ?1 ?0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let ((?x239 (ite $x143 ?1 ?x234)))
+(let ((?x199 (mod$ ?1 ?0)))
+(let (($x242 (= ?x199 ?x239)))
+(let (($x206 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
+(let ((?x204 (ite $x143 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x204)))))
+))
+(let (($x228 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let ((?x200 (mod ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let (($x143 (= ?v1 0)))
+(let ((?x222 (ite $x143 ?v0 ?x219)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x222))))))))))))
+))
+(let ((@x233 (monotonicity (rewrite (= $x144 (not $x175))) (= (ite $x144 ?x200 ?x214) (ite (not $x175) ?x200 ?x214)))))
+(let ((@x238 (trans @x233 (rewrite (= (ite (not $x175) ?x200 ?x214) ?x234)) (= (ite $x144 ?x200 ?x214) ?x234))))
+(let ((@x244 (monotonicity (monotonicity @x238 (= (ite $x143 ?1 (ite $x144 ?x200 ?x214)) ?x239)) (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 ?x214))) $x242))))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let ((?x222 (ite $x143 ?1 ?x219)))
+(let (($x225 (= ?x199 ?x222)))
+(let (($x226 (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))))) $x225)))
+(let ((@x210 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (mod (- ?1) (- ?0)) ?x208))))
+(let ((@x218 (trans (monotonicity @x210 (= (- (mod (- ?1) (- ?0))) (- ?x208))) (rewrite (= (- ?x208) ?x214)) (= (- (mod (- ?1) (- ?0))) ?x214))))
+(let ((@x221 (monotonicity @x218 (= (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))) ?x219))))
+(let ((@x224 (monotonicity @x221 (= (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0))))) ?x222))))
+(let ((@x249 (trans (quant-intro (monotonicity @x224 $x226) (= $x206 $x228)) (quant-intro @x244 (= $x228 $x245)) (= $x206 $x245))))
+(let ((@x280 (mp~ (mp (asserted $x206) @x249 $x245) (nnf-pos (refl (~ $x242 $x242)) (~ $x245 $x245)) $x245)))
+(let ((@x323 (mp @x280 (quant-intro (refl (= $x242 $x242)) (= $x245 $x318)) $x318)))
+(let (($x550 (not $x318)))
+(let (($x551 (or $x550 $x545)))
+(let ((?x359 (* (- 1) 2)))
+(let ((?x511 (mod ?x369 ?x359)))
+(let ((?x512 (* (- 1) ?x511)))
+(let ((?x517 (ite $x357 ?x512 ?x516)))
+(let ((?x518 (ite $x356 l$ ?x517)))
+(let (($x519 (= ?x99 ?x518)))
+(let ((@x525 (monotonicity (monotonicity @x374 (= ?x511 (mod ?x369 (- 2)))) (= ?x512 (* (- 1) (mod ?x369 (- 2)))))))
+(let ((@x528 (monotonicity @x368 @x525 (= ?x517 (ite false (* (- 1) (mod ?x369 (- 2))) ?x516)))))
+(let ((@x532 (trans @x528 (rewrite (= (ite false (* (- 1) (mod ?x369 (- 2))) ?x516) ?x516)) (= ?x517 ?x516))))
+(let ((@x539 (trans (monotonicity @x366 @x532 (= ?x518 (ite false l$ ?x516))) (rewrite (= (ite false l$ ?x516) ?x516)) (= ?x518 ?x516))))
+(let ((@x549 (trans (monotonicity @x539 (= $x519 (= ?x99 ?x516))) (rewrite (= (= ?x99 ?x516) $x545)) (= $x519 $x545))))
+(let ((@x558 (trans (monotonicity @x549 (= (or $x550 $x519) $x551)) (rewrite (= $x551 $x551)) (= (or $x550 $x519) $x551))))
+(let ((@x559 (mp ((_ quant-inst l$ 2) (or $x550 $x519)) @x558 $x551)))
+(let ((@x902 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x561)) (unit-resolution @x559 @x323 $x545) $x561)))
+(let ((?x757 (* (- 2) ?x744)))
+(let ((?x758 (+ ?x93 ?x726 ?x757)))
+(let (($x764 (>= ?x758 0)))
+(let (($x756 (= ?x758 0)))
+(let ((@x872 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x764)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x764)))
+(let ((?x562 (div l$ 2)))
+(let ((?x575 (* (- 2) ?x562)))
+(let ((?x576 (+ l$ ?x543 ?x575)))
+(let (($x582 (>= ?x576 0)))
+(let (($x574 (= ?x576 0)))
+(let ((@x880 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x582)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x582)))
+(let ((?x504 (mod$ ?x93 2)))
+(let ((?x727 (+ ?x504 ?x726)))
+(let (($x728 (= ?x727 0)))
+(let (($x733 (or $x550 $x728)))
+(let ((?x696 (* (- 1) ?x93)))
+(let ((?x697 (mod ?x696 ?x359)))
+(let ((?x698 (* (- 1) ?x697)))
+(let ((?x700 (ite $x357 ?x698 ?x699)))
+(let ((?x701 (ite $x356 ?x93 ?x700)))
+(let (($x702 (= ?x504 ?x701)))
+(let ((@x708 (monotonicity (monotonicity @x374 (= ?x697 (mod ?x696 (- 2)))) (= ?x698 (* (- 1) (mod ?x696 (- 2)))))))
+(let ((@x711 (monotonicity @x368 @x708 (= ?x700 (ite false (* (- 1) (mod ?x696 (- 2))) ?x699)))))
+(let ((@x715 (trans @x711 (rewrite (= (ite false (* (- 1) (mod ?x696 (- 2))) ?x699) ?x699)) (= ?x700 ?x699))))
+(let ((@x722 (trans (monotonicity @x366 @x715 (= ?x701 (ite false ?x93 ?x699))) (rewrite (= (ite false ?x93 ?x699) ?x699)) (= ?x701 ?x699))))
+(let ((@x732 (trans (monotonicity @x722 (= $x702 (= ?x504 ?x699))) (rewrite (= (= ?x504 ?x699) $x728)) (= $x702 $x728))))
+(let ((@x740 (trans (monotonicity @x732 (= (or $x550 $x702) $x733)) (rewrite (= $x733 $x733)) (= (or $x550 $x702) $x733))))
+(let ((@x427 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x728) (>= ?x727 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x550 $x702)) @x740 $x733) @x323 $x728) (>= ?x727 0))))
+(let ((?x783 (* (- 1) ?x504)))
+(let ((?x784 (+ ?x99 ?x783)))
+(let (($x786 (>= ?x784 0)))
+(let (($x782 (= ?x99 ?x504)))
+(let (($x821 (= ?x98 ?x504)))
+(let (($x505 (= ?x504 ?x98)))
+(let (($x297 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) )))
+))
+(let (($x51 (forall ((?v0 Int_list$) (?v1 Int_list$) )(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)))
+))
+(let (($x50 (= (mod$ ?x45 2) (mod$ ?x48 2))))
+(let ((@x265 (mp~ (asserted $x51) (nnf-pos (refl (~ $x50 $x50)) (~ $x51 $x51)) $x51)))
+(let ((@x302 (mp @x265 (quant-intro (refl (= $x50 $x50)) (= $x51 $x297)) $x297)))
+(let (($x514 (or (not $x297) $x505)))
+(let ((@x515 ((_ quant-inst ks$ xs$) $x514)))
+(let ((@x824 (symm (unit-resolution (def-axiom (or $x283 $x100)) @x466 $x100) (= ?x99 ?x98))))
+(let ((@x939 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x786)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x786)))
+(let (($x785 (<= ?x784 0)))
+(let ((@x887 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x785)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x785)))
+(let (($x688 (>= ?x686 0)))
+(let ((@x855 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x688)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x688)))
+(let ((@x979 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x425 2)))) @x26 (not (>= ?x425 2)))))
+(let (($x560 (<= ?x544 0)))
+(let ((@x461 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x560)) (unit-resolution @x559 @x323 $x545) $x560)))
+(let (($x763 (<= ?x758 0)))
+(let ((@x658 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x763)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x763)))
+(let (($x581 (<= ?x576 0)))
+(let ((@x986 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x581)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x581)))
+(let ((@x989 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x728) (<= ?x727 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x550 $x702)) @x740 $x733) @x323 $x728) (<= ?x727 0))))
+(let (($x510 (>= ?x502 0)))
+(let ((@x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x510)) (unit-resolution @x508 @x309 $x503) $x510)))
+(let ((@x998 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) (>= ?x396 0))) @x802 (>= ?x396 0))))
+(let ((@x1001 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) (<= ?x437 0))) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) (<= ?x437 0))))
+(let ((@x1002 ((_ th-lemma arith farkas 1 -2 -2 -1 -2 1 1 1 1 1 1) @x1001 @x998 (hypothesis $x688) @x994 (hypothesis $x972) (hypothesis $x785) @x989 @x986 @x658 @x461 @x979 false)))
+(let ((@x474 (unit-resolution (lemma @x1002 (or (not $x972) (not $x688) (not $x785))) @x855 @x887 (not $x972))))
+(let ((@x941 (unit-resolution @x474 ((_ th-lemma arith) @x939 @x427 @x880 @x872 @x902 @x899 $x972) false)))
+(let ((@x942 (lemma @x941 $x283)))
+(let ((@x340 (unit-resolution (def-axiom (or $x95 $x284 (not $x290))) @x295 (or $x95 $x284))))
+(let ((@x679 (unit-resolution @x340 @x942 $x95)))
+(let ((@x889 (trans (symm (unit-resolution @x515 @x302 $x505) $x821) (monotonicity @x679 (= ?x504 ?x99)) $x100)))
+(let (($x811 (not $x687)))
+(let ((@x845 ((_ th-lemma arith assign-bounds 1 -1/2 -1/2 1/2 -1/2) (or $x688 (not $x413) (not $x465) (not $x443) (not $x509) $x861))))
+(let ((@x892 (unit-resolution @x845 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) @x802 $x413) (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x695)) @x679 $x695) @x793 (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) @x800 $x688)))
+(let ((@x935 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x811 (not $x688))) (hypothesis $x282) (or $x811 (not $x688)))))
+(let ((@x955 ((_ th-lemma arith farkas -2 -2 1 -1 1 1) (unit-resolution @x935 @x892 $x811) @x998 @x1001 @x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x694)) @x679 $x694) @x979 false)))
+(let ((@x472 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x942 $x283) (lemma @x955 $x117) $x281)))
+(unit-resolution @x472 @x889 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
785615f585a02b3e6ed8608ecc9660ba5c4025e2 2 0
sat
(error "line 9 column 10: proof is not available")
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Jun 03 09:32:49 2015 +0200
@@ -402,7 +402,7 @@
((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
- ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
+ ((@{const_name Rings.divide}, nat_T --> nat_T --> nat_T), 0),
((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
((@{const_name of_nat}, nat_T --> int_T), 0),
@@ -411,7 +411,7 @@
((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
- ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
+ ((@{const_name Rings.divide}, int_T --> int_T --> int_T), 0),
((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Jun 03 09:32:49 2015 +0200
@@ -553,7 +553,7 @@
| (Const (x as (s as @{const_name times_class.times}, T)), []) =>
if is_built_in_const x then Cst (Multiply, T, Any)
else ConstName (s, T, Any)
- | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
+ | (Const (x as (s as @{const_name Rings.divide}, T)), []) =>
if is_built_in_const x then Cst (Divide, T, Any)
else ConstName (s, T, Any)
| (t0 as Const (x as (@{const_name ord_class.less}, _)),
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Jun 03 09:32:49 2015 +0200
@@ -56,7 +56,7 @@
let
fun aux (t1 $ t2) = aux t1 orelse aux t2
| aux (Const (s, T)) =
- ((s = @{const_name times} orelse s = @{const_name div}) andalso
+ ((s = @{const_name times} orelse s = @{const_name Rings.divide}) andalso
is_integer_type (body_type T)) orelse
(String.isPrefix numeral_prefix s andalso
let val n = the (Int.fromString (unprefix numeral_prefix s)) in
--- a/src/HOL/Tools/Qelim/cooper.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Jun 03 09:32:49 2015 +0200
@@ -756,7 +756,7 @@
| Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
| Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
| Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Rings.divide},_)$l$r => isnum l andalso isnum r
| _ => is_number t orelse can HOLogic.dest_nat t
fun ty cts t =
--- a/src/HOL/Tools/SMT/z3_interface.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Jun 03 09:32:49 2015 +0200
@@ -34,7 +34,7 @@
{logic = K "", fp_kinds = [BNF_Util.Least_FP],
serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
- fun is_div_mod @{const div (int)} = true
+ fun is_div_mod @{const divide (int)} = true
| is_div_mod @{const mod (int)} = true
| is_div_mod _ = false
--- a/src/HOL/Tools/SMT/z3_real.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_real.ML Wed Jun 03 09:32:49 2015 +0200
@@ -12,13 +12,13 @@
fun real_term_parser (SMTLIB.Dec (i, 0), []) = SOME (HOLogic.mk_number @{typ Real.real} i)
| real_term_parser (SMTLIB.Sym "/", [t1, t2]) =
- SOME (@{term "inverse_class.divide :: real => _"} $ t1 $ t2)
+ SOME (@{term "Rings.divide :: real => _"} $ t1 $ t2)
| real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (@{term "Real.real :: int => _"} $ t)
| real_term_parser _ = NONE
fun abstract abs t =
(case t of
- (c as @{term "inverse_class.divide :: real => _"}) $ t1 $ t2 =>
+ (c as @{term "Rings.divide :: real => _"}) $ t1 $ t2 =>
abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
| (c as @{term "Real.real :: int => _"}) $ t =>
abs t #>> (fn u => SOME (c $ u))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Wed Jun 03 09:32:49 2015 +0200
@@ -135,8 +135,7 @@
| Fastforce_Method => Clasimp.fast_force_tac ctxt
| Force_Method => Clasimp.force_tac ctxt
| Moura_Method => moura_tac ctxt
- | Linarith_Method =>
- let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end
+ | Linarith_Method => Lin_Arith.tac ctxt
| Presburger_Method => Cooper.tac true [] [] ctxt
| Algebra_Method => Groebner.algebra_tac [] [] ctxt))
--- a/src/HOL/Tools/lin_arith.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed Jun 03 09:32:49 2015 +0200
@@ -21,7 +21,6 @@
val global_setup: theory -> theory
val split_limit: int Config.T
val neq_limit: int Config.T
- val verbose: bool Config.T
val trace: bool Config.T
end;
@@ -102,15 +101,13 @@
val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9);
val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9);
-val verbose = Attrib.setup_config_bool @{binding linarith_verbose} (K true);
val trace = Attrib.setup_config_bool @{binding linarith_trace} (K false);
-structure LA_Data =
+structure LA_Data: LIN_ARITH_DATA =
struct
val neq_limit = neq_limit;
-val verbose = verbose;
val trace = trace;
@@ -139,7 +136,9 @@
returns either (SOME term, associated multiplicity) or (NONE, constant)
*)
-fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
+fun of_field_sort thy U = Sign.of_sort thy (U, @{sort inverse});
+
+fun demult thy (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
let
fun demult ((mC as Const (@{const_name Groups.times}, _)) $ s $ t, m) =
(case s of Const (@{const_name Groups.times}, _) $ s1 $ s2 =>
@@ -153,24 +152,26 @@
(SOME t', m'') => (SOME (mC $ s' $ t'), m'')
| (NONE, m'') => (SOME s', m''))
| (NONE, m') => demult (t, m')))
- | demult ((mC as Const (@{const_name Fields.divide}, _)) $ s $ t, m) =
+ | demult (atom as (mC as Const (@{const_name Rings.divide}, T)) $ s $ t, m) =
(* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ? Note that
if we choose to do so here, the simpset used by arith must be able to
perform the same simplifications. *)
(* quotient 's / t', where the denominator t can be NONE *)
(* Note: will raise Rat.DIVZERO iff m' is Rat.zero *)
- let val (os',m') = demult (s, m);
+ if of_field_sort thy (domain_type T) then
+ let
+ val (os',m') = demult (s, m);
val (ot',p) = demult (t, Rat.one)
- in (case (os',ot') of
+ in (case (os',ot') of
(SOME s', SOME t') => SOME (mC $ s' $ t')
| (SOME s', NONE) => SOME s'
| (NONE, SOME t') =>
- let val Const(_,T) = mC
- in SOME (mC $ Const (@{const_name Groups.one}, domain_type T) $ t') end
+ SOME (mC $ Const (@{const_name Groups.one}, domain_type (snd (dest_Const mC))) $ t')
| (NONE, NONE) => NONE,
Rat.mult m' (Rat.inv p))
- end
+ end
+ else (SOME atom, m)
(* terms that evaluate to numeric constants *)
| demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m)
| demult (Const (@{const_name Groups.zero}, _), _) = (NONE, Rat.zero)
@@ -192,7 +193,7 @@
| demult (atom, m) = (SOME atom, m)
in demult end;
-fun decomp0 (inj_consts : (string * typ) list) (rel : string, lhs : term, rhs : term) :
+fun decomp0 thy (inj_consts : (string * typ) list) (rel : string, lhs : term, rhs : term) :
((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat) option =
let
(* Turns a term 'all' and associated multiplicity 'm' into a list 'p' of
@@ -215,13 +216,15 @@
| poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
poly (t, m, (p, Rat.add i m))
| poly (all as Const (@{const_name Groups.times}, _) $ _ $ _, m, pi as (p, i)) =
- (case demult inj_consts (all, m) of
+ (case demult thy inj_consts (all, m) of
(NONE, m') => (p, Rat.add i m')
| (SOME u, m') => add_atom u m' pi)
- | poly (all as Const (@{const_name Fields.divide}, _) $ _ $ _, m, pi as (p, i)) =
- (case demult inj_consts (all, m) of
- (NONE, m') => (p, Rat.add i m')
- | (SOME u, m') => add_atom u m' pi)
+ | poly (all as Const (@{const_name Rings.divide}, T) $ _ $ _, m, pi as (p, i)) =
+ if of_field_sort thy (domain_type T) then
+ (case demult thy inj_consts (all, m) of
+ (NONE, m') => (p, Rat.add i m')
+ | (SOME u, m') => add_atom u m' pi)
+ else add_atom all m pi
| poly (all as Const f $ x, m, pi) =
if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
| poly (all, m, pi) =
@@ -244,12 +247,12 @@
else if member (op =) discrete D then (true, true) else (false, false)
| allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
-fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decomp option =
+fun decomp_typecheck thy (discrete, inj_consts) (T : typ, xxx) : decomp option =
case T of
Type ("fun", [U, _]) =>
(case allows_lin_arith thy discrete U of
(true, d) =>
- (case decomp0 inj_consts xxx of
+ (case decomp0 thy inj_consts xxx of
NONE => NONE
| SOME (p, i, rel, q, j) => SOME (p, i, rel, q, j, d))
| (false, _) =>
@@ -259,20 +262,20 @@
fun negate (SOME (x, i, rel, y, j, d)) = SOME (x, i, "~" ^ rel, y, j, d)
| negate NONE = NONE;
-fun decomp_negation data
- ((Const (@{const_name Trueprop}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
- decomp_typecheck data (T, (rel, lhs, rhs))
- | decomp_negation data ((Const (@{const_name Trueprop}, _)) $
- (Const (@{const_name Not}, _) $ (Const (rel, T) $ lhs $ rhs))) =
- negate (decomp_typecheck data (T, (rel, lhs, rhs)))
- | decomp_negation data _ =
+fun decomp_negation thy data
+ ((Const (@{const_name Trueprop}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
+ decomp_typecheck thy data (T, (rel, lhs, rhs))
+ | decomp_negation thy data
+ ((Const (@{const_name Trueprop}, _)) $ (Const (@{const_name Not}, _) $ (Const (rel, T) $ lhs $ rhs))) =
+ negate (decomp_typecheck thy data (T, (rel, lhs, rhs)))
+ | decomp_negation thy data _ =
NONE;
fun decomp ctxt : term -> decomp option =
let
val thy = Proof_Context.theory_of ctxt
val {discrete, inj_consts, ...} = get_arith_data ctxt
- in decomp_negation (thy, discrete, inj_consts) end;
+ in decomp_negation thy (discrete, inj_consts) end;
fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T
| domain_is_nat (_ $ (Const (@{const_name Not}, _) $ (Const (_, T) $ _ $ _))) = nT T
@@ -299,7 +302,7 @@
@{const_name Groups.minus},
"Int.nat" (*DYNAMIC BINDING!*),
"Divides.div_class.mod" (*DYNAMIC BINDING!*),
- "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
+ @{const_name Rings.divide}] a
| _ =>
(if Context_Position.is_visible ctxt then
warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
@@ -498,7 +501,7 @@
(* ?P ((?n::nat) div (numeral ?k)) =
((numeral ?k = 0 --> ?P 0) & (~ (numeral ?k = 0) -->
(ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P i))) *)
- | (Const ("Divides.div_class.div", Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
+ | (Const (@{const_name Rings.divide}, Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
let
val rev_terms = rev terms
val zero = Const (@{const_name Groups.zero}, split_type)
@@ -589,7 +592,7 @@
(numeral ?k < 0 -->
(ALL i j.
numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P i))) *)
- | (Const ("Divides.div_class.div",
+ | (Const (@{const_name Rings.divide},
Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Wed Jun 03 09:32:49 2015 +0200
@@ -288,8 +288,8 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
+ val mk_bal = HOLogic.mk_binop @{const_name Rings.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} HOLogic.natT
val cancel = @{thm nat_mult_div_cancel1} RS trans
val neg_exchanges = false
);
@@ -393,8 +393,8 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
+ val mk_bal = HOLogic.mk_binop @{const_name Rings.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} HOLogic.natT
fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj}
);
--- a/src/HOL/Tools/numeral_simprocs.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Wed Jun 03 09:32:49 2015 +0200
@@ -116,7 +116,7 @@
Fractions are reduced later by the cancel_numeral_factor simproc.*)
fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
-val mk_divide = HOLogic.mk_binop @{const_name Fields.divide};
+val mk_divide = HOLogic.mk_binop @{const_name Rings.divide};
(*Build term (p / q) * t*)
fun mk_fcoeff ((p, q), t) =
@@ -125,7 +125,7 @@
(*Express t as a product of a fraction with other sorted terms*)
fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t
- | dest_fcoeff sign (Const (@{const_name Fields.divide}, _) $ t $ u) =
+ | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) =
let val (p, t') = dest_coeff sign t
val (q, u') = dest_coeff 1 u
in (mk_frac (p, q), mk_divide (t', u')) end
@@ -401,8 +401,8 @@
(*Version for semiring_div*)
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Rings.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
val cancel = @{thm div_mult_mult1} RS trans
val neg_exchanges = false
)
@@ -410,8 +410,8 @@
(*Version for fields*)
structure DivideCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val mk_bal = HOLogic.mk_binop @{const_name Fields.divide}
- val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Rings.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
val cancel = @{thm mult_divide_mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -548,8 +548,8 @@
(*for semirings with division*)
structure DivCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Rings.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
);
@@ -571,8 +571,8 @@
(*Version for all fields, including unordered ones (type complex).*)
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val mk_bal = HOLogic.mk_binop @{const_name Fields.divide}
- val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Rings.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
);
@@ -620,13 +620,13 @@
val (l,r) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm l
in (case (Thm.term_of l, Thm.term_of r) of
- (Const(@{const_name Fields.divide},_)$_$_, _) =>
+ (Const(@{const_name Rings.divide},_)$_$_, _) =>
let val (x,y) = Thm.dest_binop l val z = r
val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
val ynz = prove_nz ctxt T y
in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
end
- | (_, Const (@{const_name Fields.divide},_)$_$_) =>
+ | (_, Const (@{const_name Rings.divide},_)$_$_) =>
let val (x,y) = Thm.dest_binop r val z = l
val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
val ynz = prove_nz ctxt T y
@@ -636,49 +636,49 @@
end
handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
- fun is_number (Const(@{const_name Fields.divide},_)$a$b) = is_number a andalso is_number b
+ fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
| is_number t = can HOLogic.dest_number t
val is_number = is_number o Thm.term_of
fun proc3 phi ctxt ct =
(case Thm.term_of ct of
- Const(@{const_name Orderings.less},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
+ Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = Thm.ctyp_of_cterm c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
+ | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = Thm.ctyp_of_cterm c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name HOL.eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
+ | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = Thm.ctyp_of_cterm c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
+ | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = Thm.ctyp_of_cterm c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
+ | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = Thm.ctyp_of_cterm c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
+ | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
--- a/src/HOL/Tools/semiring_normalizer.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Wed Jun 03 09:32:49 2015 +0200
@@ -127,12 +127,12 @@
let
fun numeral_is_const ct =
case Thm.term_of ct of
- Const (@{const_name Fields.divide},_) $ a $ b =>
+ Const (@{const_name Rings.divide},_) $ a $ b =>
can HOLogic.dest_number a andalso can HOLogic.dest_number b
| Const (@{const_name Fields.inverse},_)$t => can HOLogic.dest_number t
| t => can HOLogic.dest_number t
fun dest_const ct = ((case Thm.term_of ct of
- Const (@{const_name Fields.divide},_) $ a $ b=>
+ Const (@{const_name Rings.divide},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
| Const (@{const_name Fields.inverse},_)$t =>
Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
--- a/src/HOL/Tools/try0.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/try0.ML Wed Jun 03 09:32:49 2015 +0200
@@ -105,7 +105,6 @@
bound exceeded" warnings and the like. *)
fun silence_methods debug =
Config.put Metis_Tactic.verbose debug
- #> Config.put Lin_Arith.verbose debug
#> not debug ? (fn ctxt =>
ctxt
|> Context_Position.set_visible false
--- a/src/HOL/Word/Word.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Word/Word.thy Wed Jun 03 09:32:49 2015 +0200
@@ -307,7 +307,7 @@
by (metis bintr_ariths(4))
definition
- word_div_def: "a div b = word_of_int (uint a div uint b)"
+ word_div_def: "divide a b = word_of_int (uint a div uint b)"
definition
word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
--- a/src/HOL/ex/Dedekind_Real.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Wed Jun 03 09:32:49 2015 +0200
@@ -102,7 +102,7 @@
preal_inverse_def:
"inverse R == Abs_preal (inverse_set (Rep_preal R))"
-definition "R / S = R * inverse (S\<Colon>preal)"
+definition "divide R S = R * inverse (S\<Colon>preal)"
definition
preal_one_def:
@@ -1222,7 +1222,7 @@
real_inverse_def: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
definition
- real_divide_def: "R / (S::real) = R * inverse S"
+ real_divide_def: "divide R (S::real) = R * inverse S"
definition
real_le_def: "z \<le> (w::real) \<longleftrightarrow>
--- a/src/HOL/ex/FinFunPred.thy Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/ex/FinFunPred.thy Wed Jun 03 09:32:49 2015 +0200
@@ -15,7 +15,7 @@
definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f $ x \<le> g $ x)"
-definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g"
+definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> g \<le> f"
instance ..
--- a/src/Provers/Arith/fast_lin_arith.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Jun 03 09:32:49 2015 +0200
@@ -207,105 +207,6 @@
Need to know if it is a lower or upper bound for unambiguous interpretation!
*)
-fun elim_eqns (Lineq (i, Le, cs, _)) = [(i, true, cs)]
- | elim_eqns (Lineq (i, Eq, cs, _)) = [(i, true, cs),(~i, true, map ~ cs)]
- | elim_eqns (Lineq (i, Lt, cs, _)) = [(i, false, cs)];
-
-(* PRE: ex[v] must be 0! *)
-fun eval ex v (a, le, cs) =
- let
- val rs = map Rat.rat_of_int cs;
- val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero;
- in (Rat.mult (Rat.add (Rat.rat_of_int a) (Rat.neg rsum)) (Rat.inv (nth rs v)), le) end;
-(* If nth rs v < 0, le should be negated.
- Instead this swap is taken into account in ratrelmin2.
-*)
-
-fun ratrelmin2 (x as (r, ler), y as (s, les)) =
- case Rat.ord (r, s)
- of EQUAL => (r, (not ler) andalso (not les))
- | LESS => x
- | GREATER => y;
-
-fun ratrelmax2 (x as (r, ler), y as (s, les)) =
- case Rat.ord (r, s)
- of EQUAL => (r, ler andalso les)
- | LESS => y
- | GREATER => x;
-
-val ratrelmin = foldr1 ratrelmin2;
-val ratrelmax = foldr1 ratrelmax2;
-
-fun ratexact up (r, exact) =
- if exact then r else
- let
- val (_, q) = Rat.quotient_of_rat r;
- val nth = Rat.inv (Rat.rat_of_int q);
- in Rat.add r (if up then nth else Rat.neg nth) end;
-
-fun ratmiddle (r, s) = Rat.mult (Rat.add r s) (Rat.inv Rat.two);
-
-fun choose2 d ((lb, exactl), (ub, exactu)) =
- let val ord = Rat.sign lb in
- if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu)
- then Rat.zero
- else if not d then
- if ord = GREATER
- then if exactl then lb else ratmiddle (lb, ub)
- else if exactu then ub else ratmiddle (lb, ub)
- else (*discrete domain, both bounds must be exact*)
- if ord = GREATER
- then let val lb' = Rat.roundup lb in
- if Rat.le lb' ub then lb' else raise NoEx end
- else let val ub' = Rat.rounddown ub in
- if Rat.le lb ub' then ub' else raise NoEx end
- end;
-
-fun findex1 discr (v, lineqs) ex =
- let
- val nz = filter (fn (Lineq (_, _, cs, _)) => nth cs v <> 0) lineqs;
- val ineqs = maps elim_eqns nz;
- val (ge, le) = List.partition (fn (_,_,cs) => nth cs v > 0) ineqs
- val lb = ratrelmax (map (eval ex v) ge)
- val ub = ratrelmin (map (eval ex v) le)
- in nth_map v (K (choose2 (nth discr v) (lb, ub))) ex end;
-
-fun elim1 v x =
- map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (nth bs v) x)), le,
- nth_map v (K Rat.zero) bs));
-
-fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.sign) cs
- of [x] => x =/ nth cs v
- | _ => false;
-
-(* The base case:
- all variables occur only with positive or only with negative coefficients *)
-fun pick_vars discr (ineqs,ex) =
- let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.sign) cs) ineqs
- in case nz of [] => ex
- | (_,_,cs) :: _ =>
- let val v = find_index (not o curry (op =) EQUAL o Rat.sign) cs
- val d = nth discr v;
- val pos = not (Rat.sign (nth cs v) = LESS);
- val sv = filter (single_var v) nz;
- val minmax =
- if pos then if d then Rat.roundup o fst o ratrelmax
- else ratexact true o ratrelmax
- else if d then Rat.rounddown o fst o ratrelmin
- else ratexact false o ratrelmin
- val bnds = map (fn (a,le,bs) => (Rat.mult a (Rat.inv (nth bs v)), le)) sv
- val x = minmax((Rat.zero,if pos then true else false)::bnds)
- val ineqs' = elim1 v x nz
- val ex' = nth_map v (K x) ex
- in pick_vars discr (ineqs',ex') end
- end;
-
-fun findex0 discr n lineqs =
- let val ineqs = maps elim_eqns lineqs
- val rineqs = map (fn (a,le,cs) => (Rat.rat_of_int a, le, map Rat.rat_of_int cs))
- ineqs
- in pick_vars discr (rineqs,replicate n Rat.zero) end;
-
(* ------------------------------------------------------------------------- *)
(* End of counterexample finder. The actual decision procedure starts here. *)
(* ------------------------------------------------------------------------- *)
@@ -432,7 +333,7 @@
val nziblows = filter_out (fn (i, _) => i = 0) iblows
in if null nziblows then Failure((~1,nontriv)::hist)
else
- let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows)
+ let val (_,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows)
val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ineqs
val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => nth l v > 0) yes
in elim ctxt (no @ map_product (elim_var v) pos neg, (v,nontriv)::hist) end
@@ -458,7 +359,6 @@
if Config.get ctxt LA_Data.trace then tracing msg else ();
val union_term = union Envir.aeconv;
-val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Envir.aeconv (t, t'));
fun add_atoms (lhs, _, _, rhs, _, _) =
union_term (map fst lhs) o union_term (map fst rhs);
@@ -607,46 +507,6 @@
(* Print (counter) example *)
(* ------------------------------------------------------------------------- *)
-fun print_atom((a,d),r) =
- let val (p,q) = Rat.quotient_of_rat r
- val s = if d then string_of_int p else
- if p = 0 then "0"
- else string_of_int p ^ "/" ^ string_of_int q
- in a ^ " = " ^ s end;
-
-fun is_variable (Free _) = true
- | is_variable (Var _) = true
- | is_variable (Bound _) = true
- | is_variable _ = false
-
-fun trace_ex ctxt params atoms discr n (hist: history) =
- case hist of
- [] => ()
- | (v, lineqs) :: hist' =>
- let
- val frees = map Free params
- fun show_term t = Syntax.string_of_term ctxt (subst_bounds (frees, t))
- val start =
- if v = ~1 then (hist', findex0 discr n lineqs)
- else (hist, replicate n Rat.zero)
- val produce_ex =
- map print_atom #> commas #>
- prefix "Counterexample (possibly spurious):\n"
- val ex = (
- uncurry (fold (findex1 discr)) start
- |> map2 pair (atoms ~~ discr)
- |> filter (fn ((t, _), _) => is_variable t)
- |> map (apfst (apfst show_term))
- |> (fn [] => NONE | sdss => SOME (produce_ex sdss)))
- handle NoEx => NONE
- in
- case ex of
- SOME s =>
- (warning "Linear arithmetic failed -- see trace for a (potentially spurious) counterexample.";
- tracing s)
- | NONE => warning "Linear arithmetic failed"
- end;
-
(* ------------------------------------------------------------------------- *)
fun mknat (pTs : typ list) (ixs : int list) (atom : term, i : int) : lineq option =
@@ -731,9 +591,6 @@
result
end;
-fun add_datoms ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _) (dats : (bool * term) list) =
- union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats);
-
fun refutes ctxt :
(typ list * (LA_Data.decomp * int) list) list -> injust list -> injust list option =
let
--- a/src/Pure/Isar/class.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Pure/Isar/class.ML Wed Jun 03 09:32:49 2015 +0200
@@ -13,12 +13,12 @@
val rules: theory -> class -> thm option * thm
val these_defs: theory -> sort -> thm list
val these_operations: theory -> sort
- -> (string * (class * (typ * term))) list
+ -> (string * (class * ((typ * term) * bool))) list
val print_classes: Proof.context -> unit
val init: class -> theory -> Proof.context
val begin: class list -> sort -> Proof.context -> Proof.context
val const: class -> (binding * mixfix) * term -> term list * term list -> local_theory -> local_theory
- val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> term -> term list * term list -> local_theory -> local_theory
+ val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
val class_prefix: string -> string
val register: class -> class list -> ((string * typ) * (string * typ)) list
@@ -74,7 +74,7 @@
(* dynamic part *)
defs: thm list,
- operations: (string * (class * (typ * term))) list
+ operations: (string * (class * ((typ * term) * bool))) list
(* n.b.
params = logical parameters of class
@@ -216,7 +216,7 @@
some_axiom some_assm_intro of_class thy =
let
val operations = map (fn (v_ty as (_, ty), (c, _)) =>
- (c, (class, (ty, Free v_ty)))) params;
+ (c, (class, ((ty, Free v_ty), false)))) params;
val add_class = Graph.new_node (class,
make_class_data (((map o apply2) fst params, base_sort,
base_morph, export_morph, some_assm_intro, of_class, some_axiom), ([], operations)))
@@ -230,7 +230,7 @@
(eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
| NONE => thy);
-fun register_operation class (c, t) thy =
+fun register_operation class (c, t) input_only thy =
let
val base_sort = base_sort thy class;
val prep_typ = map_type_tfree
@@ -241,7 +241,7 @@
in
thy
|> (Class_Data.map o Graph.map_node class o map_class_data o apsnd o apsnd)
- (cons (c, (class, (ty', t'))))
+ (cons (c, (class, ((ty', t'), input_only))))
end;
fun register_def class def_thm thy =
@@ -259,8 +259,22 @@
(* class context syntax *)
-fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
- o these_operations thy;
+fun make_rewrite t c_ty =
+ let
+ val (vs, t') = strip_abs t;
+ val vts = map snd vs
+ |> Name.invent_names Name.context Name.uu
+ |> map (fn (v, T) => Var ((v, 0), T));
+ in (betapplys (t, vts), betapplys (Const c_ty, vts)) end;
+
+fun these_unchecks thy =
+ these_operations thy
+ #> map_filter (fn (c, (_, ((ty, t), input_only))) =>
+ if input_only then NONE else SOME (make_rewrite t (c, ty)));
+
+fun these_unchecks_reversed thy =
+ these_operations thy
+ #> map (fn (c, (_, ((ty, t), _))) => (Const (c, ty), t));
fun redeclare_const thy c =
let val b = Long_Name.base_name c
@@ -273,9 +287,9 @@
val operations = these_operations thy sort;
fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
val primary_constraints =
- (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
+ (map o apsnd) (subst_class_typ base_sort o fst o fst o snd) operations;
val secondary_constraints =
- (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
+ (map o apsnd) (fn (class, ((ty, _), _)) => subst_class_typ [class] ty) operations;
fun improve (c, ty) =
(case AList.lookup (op =) primary_constraints c of
SOME ty' =>
@@ -289,13 +303,14 @@
| _ => NONE)
| NONE => NONE)
| NONE => NONE);
- fun subst (c, _) = Option.map snd (AList.lookup (op =) operations c);
+ fun subst (c, _) = Option.map (fst o snd) (AList.lookup (op =) operations c);
val unchecks = these_unchecks thy sort;
in
ctxt
|> fold (redeclare_const thy o fst) primary_constraints
- |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
- (((improve, subst), true), unchecks)), false))
+ |> Overloading.map_improvable_syntax (K {primary_constraints = primary_constraints,
+ secondary_constraints = secondary_constraints, improve = improve, subst = subst,
+ no_subst_in_abbrev_mode = true, unchecks = unchecks})
|> Overloading.set_primary_constraints
end;
@@ -324,8 +339,6 @@
val class_prefix = Logic.const_of_class o Long_Name.base_name;
-local
-
fun guess_morphism_identity (b, rhs) phi1 phi2 =
let
(*FIXME proper concept to identify morphism instead of educated guess*)
@@ -336,15 +349,19 @@
val rhs2 = Morphism.term phi2 rhs;
in n1 = n2 andalso Term.aconv_untyped (rhs1, rhs2) end;
-fun target_const class phi0 prmode ((b, _), rhs) =
+fun target_const class phi0 prmode (b, rhs) lthy =
let
- val guess_identity = guess_morphism_identity (b, rhs) Morphism.identity;
- val guess_canonical = guess_morphism_identity (b, rhs) phi0;
+ val export = Variable.export_morphism lthy (Local_Theory.target_of lthy);
+ val guess_identity = guess_morphism_identity (b, rhs) export;
+ val guess_canonical = guess_morphism_identity (b, rhs) (export $> phi0);
in
- Generic_Target.locale_target_const class
+ lthy
+ |> Generic_Target.locale_target_const class
(not o (guess_identity orf guess_canonical)) prmode ((b, NoSyn), rhs)
end;
+local
+
fun dangling_params_for lthy class (type_params, term_params) =
let
val class_param_names =
@@ -374,28 +391,10 @@
|> snd
|> global_def (b_def, def_eq)
|-> (fn def_thm => register_def class def_thm)
- |> null dangling_params ? register_operation class (c, rhs)
+ |> null dangling_params ? register_operation class (c, rhs) false
|> Sign.add_const_constraint (c, SOME ty)
end;
-fun canonical_abbrev class phi prmode dangling_term_params ((b, mx), rhs) thy =
- let
- val unchecks = these_unchecks thy [class];
- val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
- val c' = Sign.full_name thy b;
- val ty' = map Term.fastype_of dangling_term_params ---> Term.fastype_of rhs';
- val ty'' = Morphism.typ phi ty';
- val rhs'' = map_types (Morphism.typ phi) (fold lambda dangling_term_params rhs');
- in
- thy
- |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global rhs'')
- |> snd
- |> Sign.notation true prmode [(Const (c', ty''), mx)]
- |> (null dangling_term_params andalso not (#1 prmode = Print_Mode.input))
- ? register_operation class (c', rhs')
- |> Sign.add_const_constraint (c', SOME ty')
- end;
-
in
fun const class ((b, mx), lhs) params lthy =
@@ -404,7 +403,7 @@
val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params));
in
lthy
- |> target_const class phi Syntax.mode_default ((b, mx), lhs)
+ |> target_const class phi Syntax.mode_default (b, lhs)
|> Local_Theory.raw_theory (canonical_const class phi dangling_params
((Morphism.binding phi b, if null dangling_params then mx else NoSyn), Morphism.term phi lhs))
|> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other)
@@ -412,18 +411,57 @@
|> synchronize_class_syntax_target class
end;
-fun abbrev class prmode ((b, mx), lhs) rhs' params lthy =
+end;
+
+local
+
+fun canonical_abbrev class phi prmode with_syntax ((b, mx), rhs) thy =
let
- val phi = morphism (Proof_Context.theory_of lthy) class;
- val dangling_term_params = map (Morphism.term phi) (snd (dangling_params_for lthy class params));
+ val c = Sign.full_name thy b;
+ val constrain = map_atyps (fn T as TFree (v, _) =>
+ if v = Name.aT then TFree (v, [class]) else T | T => T);
+ val rhs' = map_types constrain rhs;
+ in
+ thy
+ |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global rhs')
+ |> snd
+ |> with_syntax ? Sign.notation true prmode [(Const (c, fastype_of rhs), mx)]
+ |> with_syntax ? register_operation class (c, rhs)
+ (#1 prmode = Print_Mode.input)
+ |> Sign.add_const_constraint (c, SOME (fastype_of rhs'))
+ end;
+
+fun canonical_abbrev_target class phi prmode ((b, mx), rhs) lthy =
+ let
+ val thy = Proof_Context.theory_of lthy;
+ val preprocess = perhaps (try (Pattern.rewrite_term_top thy (these_unchecks thy [class]) []));
+ val (global_rhs, (extra_tfrees, (type_params, term_params))) =
+ Generic_Target.export_abbrev lthy preprocess rhs;
+ val mx' = Generic_Target.check_mixfix_global (b, null term_params) mx;
in
lthy
- |> target_const class phi prmode ((b, mx), lhs)
- |> Local_Theory.raw_theory (canonical_abbrev class phi prmode dangling_term_params
- ((Morphism.binding phi b, if null dangling_term_params then mx else NoSyn), rhs'))
- |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other)
- prmode ((b, if null dangling_term_params then NoSyn else mx), lhs)
- |> synchronize_class_syntax_target class
+ |> Local_Theory.raw_theory (canonical_abbrev class phi prmode (null term_params)
+ ((Morphism.binding phi b, mx'), Logic.unvarify_types_global global_rhs))
+ end;
+
+fun further_abbrev_target class phi prmode (b, mx) rhs params =
+ Generic_Target.background_abbrev (b, rhs) (snd params)
+ #-> (fn (lhs, _) => target_const class phi prmode (b, lhs)
+ #> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), lhs))
+
+in
+
+fun abbrev class prmode ((b, mx), rhs) lthy =
+ let
+ val thy = Proof_Context.theory_of lthy;
+ val phi = morphism thy class;
+ val rhs_generic =
+ perhaps (try (Pattern.rewrite_term_top thy (these_unchecks_reversed thy [class]) [])) rhs;
+ in
+ lthy
+ |> canonical_abbrev_target class phi prmode ((b, mx), rhs)
+ |> Generic_Target.abbrev (further_abbrev_target class phi) prmode ((b, mx), rhs_generic)
+ ||> synchronize_class_syntax_target class
end;
end;
@@ -545,9 +583,10 @@
map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
in
ctxt
- |> Overloading.map_improvable_syntax
- (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
- (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
+ |> Overloading.map_improvable_syntax (fn {primary_constraints, improve, ...} =>
+ {primary_constraints = primary_constraints, secondary_constraints = [],
+ improve = improve, subst = subst, no_subst_in_abbrev_mode = false,
+ unchecks = unchecks})
end;
fun resort_terms ctxt algebra consts constraints ts =
@@ -578,7 +617,7 @@
SOME c =>
if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
- | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params);
+ | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
fun pretty lthy =
let
@@ -635,15 +674,16 @@
|> Instantiation.put (make_instantiation ((tycos, vs, sort), params))
|> fold (Variable.declare_typ o TFree) vs
|> fold (Variable.declare_names o Free o snd) params
- |> (Overloading.map_improvable_syntax o apfst)
- (K ((primary_constraints, []), (((improve, K NONE), false), [])))
+ |> (Overloading.map_improvable_syntax) (K {primary_constraints = primary_constraints,
+ secondary_constraints = [], improve = improve, subst = K NONE,
+ no_subst_in_abbrev_mode = false, unchecks = []})
|> Overloading.activate_improvable_syntax
|> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
|> synchronize_inst_syntax
|> Local_Theory.init (Sign.naming_of thy)
{define = Generic_Target.define foundation,
- notes = Generic_Target.notes Generic_Target.theory_notes,
- abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
+ notes = Generic_Target.notes Generic_Target.theory_target_notes,
+ abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
declaration = K Generic_Target.theory_declaration,
subscription = Generic_Target.theory_registration,
pretty = pretty,
--- a/src/Pure/Isar/class_declaration.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Pure/Isar/class_declaration.ML Wed Jun 03 09:32:49 2015 +0200
@@ -116,7 +116,7 @@
else fold inter_sort (map (Class.base_sort thy) sups) [];
val is_param = member (op =) (map fst (Class.these_params thy sups));
val base_constraints = (map o apsnd)
- (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
+ (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o fst o snd)
(Class.these_operations thy sups);
fun singleton_fixateT Ts =
let
--- a/src/Pure/Isar/generic_target.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML Wed Jun 03 09:32:49 2015 +0200
@@ -7,17 +7,22 @@
signature GENERIC_TARGET =
sig
- (*consts*)
- val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
- local_theory -> local_theory
+ (*auxiliary*)
+ val export_abbrev: Proof.context ->
+ (term -> term) -> term -> term * ((string * sort) list * (term list * term list))
+ val check_mixfix_global: binding * bool -> mixfix -> mixfix
- (*background operations*)
+ (*background primitives*)
val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory
val background_declaration: declaration -> local_theory -> local_theory
val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
- (*lifting primitives to local theory operations*)
+ (*nested local theories primitives*)
+ val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
+ local_theory -> local_theory
+
+ (*lifting target primitives to local theory operations*)
val define: (((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory) ->
bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
@@ -27,33 +32,43 @@
(Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) ->
string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory ->
(string * thm list) list * local_theory
- val abbrev: (string * bool -> binding * mixfix -> term ->
+ val abbrev: (Syntax.mode -> binding * mixfix -> term ->
term list * term list -> local_theory -> local_theory) ->
- string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
+ Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
- (*theory operations*)
- val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
- term list * term list -> local_theory -> (term * thm) * local_theory
- val theory_notes: string ->
+ (*theory target primitives*)
+ val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) ->
+ term list * term list -> local_theory -> (term * thm) * local_theory
+ val theory_target_notes: string ->
(Attrib.binding * (thm list * Token.src list) list) list ->
(Attrib.binding * (thm list * Token.src list) list) list ->
local_theory -> local_theory
+ val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
+ local_theory -> local_theory
+
+ (*theory target operations*)
+ val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
+ local_theory -> (term * term) * local_theory
val theory_declaration: declaration -> local_theory -> local_theory
- val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
- local_theory -> local_theory
val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
local_theory -> local_theory
- (*locale operations*)
- val locale_notes: string -> string ->
+ (*locale target primitives*)
+ val locale_target_notes: string -> string ->
(Attrib.binding * (thm list * Token.src list) list) list ->
(Attrib.binding * (thm list * Token.src list) list) list ->
local_theory -> local_theory
+ val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
+ local_theory -> local_theory
val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
+ val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
+ (binding * mixfix) * term -> local_theory -> local_theory
+
+ (*locale operations*)
+ val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term ->
+ local_theory -> (term * term) * local_theory
val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
local_theory -> local_theory
- val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
- (binding * mixfix) * term -> local_theory -> local_theory
val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
@@ -63,30 +78,23 @@
structure Generic_Target: GENERIC_TARGET =
struct
-(** notes **)
-
-fun standard_facts lthy ctxt =
- Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
+(** consts **)
-fun standard_notes pred kind facts lthy =
- Local_Theory.map_contexts (fn level => fn ctxt =>
- if pred (Local_Theory.level lthy, level)
- then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
- else ctxt) lthy;
-
+fun export_abbrev lthy preprocess rhs =
+ let
+ val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
-
-(** declarations **)
+ val rhs' = rhs
+ |> Assumption.export_term lthy (Local_Theory.target_of lthy)
+ |> preprocess;
+ val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' []));
+ val u = fold_rev lambda term_params rhs';
+ val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
-fun standard_declaration pred decl lthy =
- Local_Theory.map_contexts (fn level => fn ctxt =>
- if pred (Local_Theory.level lthy, level)
- then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
- else ctxt) lthy;
-
-
-
-(** consts **)
+ val extra_tfrees =
+ subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+ val type_params = map (Logic.mk_type o TFree) extra_tfrees;
+ in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
fun check_mixfix ctxt (b, extra_tfrees) mx =
if null extra_tfrees then mx
@@ -139,9 +147,6 @@
end
else context;
-fun standard_const pred prmode ((b, mx), rhs) =
- standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
-
(** background primitives **)
@@ -174,7 +179,28 @@
-(** lifting primitive to local theory operations **)
+(** nested local theories primitives **)
+
+fun standard_facts lthy ctxt =
+ Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
+
+fun standard_notes pred kind facts lthy =
+ Local_Theory.map_contexts (fn level => fn ctxt =>
+ if pred (Local_Theory.level lthy, level)
+ then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
+ else ctxt) lthy;
+
+fun standard_declaration pred decl lthy =
+ Local_Theory.map_contexts (fn level => fn ctxt =>
+ if pred (Local_Theory.level lthy, level)
+ then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
+ else ctxt) lthy;
+
+fun standard_const pred prmode ((b, mx), rhs) =
+ standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
+
+
+(** lifting target primitives to local theory operations **)
(* define *)
@@ -264,7 +290,7 @@
in
-fun notes notes' kind facts lthy =
+fun notes target_notes kind facts lthy =
let
val facts' = facts
|> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
@@ -274,7 +300,7 @@
val global_facts = Global_Theory.map_facts #2 facts';
in
lthy
- |> notes' kind global_facts (Attrib.partial_evaluation lthy local_facts)
+ |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
|> Attrib.local_notes kind local_facts
end;
@@ -283,43 +309,31 @@
(* abbrev *)
-fun abbrev abbrev' prmode ((b, mx), rhs) lthy =
+fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
let
- val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
-
- val rhs' = Assumption.export_term lthy (Local_Theory.target_of lthy) rhs;
- val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' []));
- val u = fold_rev lambda term_params rhs';
- val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
-
- val extra_tfrees =
- subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+ val (global_rhs, (extra_tfrees, (type_params, term_params))) = export_abbrev lthy I rhs;
val mx' = check_mixfix lthy (b, extra_tfrees) mx;
- val type_params = map (Logic.mk_type o TFree) extra_tfrees;
in
lthy
- |> abbrev' prmode (b, mx') global_rhs (type_params, term_params)
+ |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params)
|> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
|> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
end;
-(** theory operations **)
+(** theory target primitives **)
-fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+fun theory_target_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
#-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs)
#> pair (lhs, def));
-fun theory_notes kind global_facts local_facts =
+fun theory_target_notes kind global_facts local_facts =
Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd)
#> standard_notes (op <>) kind local_facts;
-fun theory_declaration decl =
- background_declaration decl #> standard_declaration (K true) decl;
-
-fun theory_abbrev prmode (b, mx) global_rhs params =
+fun theory_target_abbrev prmode (b, mx) global_rhs params =
Local_Theory.background_theory_result
(Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
(fn (lhs, _) => (* FIXME type_params!? *)
@@ -327,14 +341,22 @@
#-> (fn lhs => standard_const (op <>) prmode
((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params)));
+
+(** theory operations **)
+
+val theory_abbrev = abbrev theory_target_abbrev;
+
+fun theory_declaration decl =
+ background_declaration decl #> standard_declaration (K true) decl;
+
val theory_registration =
Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
-(** locale operations **)
+(** locale target primitives **)
-fun locale_notes locale kind global_facts local_facts =
+fun locale_target_notes locale kind global_facts local_facts =
Local_Theory.background_theory
(Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
(fn lthy => lthy |>
@@ -347,14 +369,17 @@
Locale.add_declaration locale syntax
(Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
+fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
+ locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
+
+
+(** locale operations **)
+
fun locale_declaration locale {syntax, pervasive} decl =
pervasive ? background_declaration decl
#> locale_target_declaration locale syntax decl
#> standard_declaration (fn (_, other) => other <> 0) decl;
-fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
- locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
-
fun locale_const locale prmode ((b, mx), rhs) =
locale_target_const locale (K true) prmode ((b, mx), rhs)
#> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
@@ -363,4 +388,13 @@
(Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
#> Locale.activate_fragment_nonbrittle dep_morph mixin export;
+
+(** locale abbreviations **)
+
+fun locale_target_abbrev locale prmode (b, mx) global_rhs params =
+ background_abbrev (b, global_rhs) (snd params)
+ #-> (fn (lhs, _) => locale_const locale prmode ((b, mx), lhs));
+
+fun locale_abbrev locale = abbrev (locale_target_abbrev locale);
+
end;
--- a/src/Pure/Isar/named_target.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Pure/Isar/named_target.ML Wed Jun 03 09:32:49 2015 +0200
@@ -75,30 +75,22 @@
#-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params
#> pair (lhs, def));
-fun foundation ("", _) = Generic_Target.theory_foundation
+fun foundation ("", _) = Generic_Target.theory_target_foundation
| foundation (locale, false) = locale_foundation locale
| foundation (class, true) = class_foundation class;
(* notes *)
-fun notes ("", _) = Generic_Target.theory_notes
- | notes (locale, _) = Generic_Target.locale_notes locale;
+fun notes ("", _) = Generic_Target.theory_target_notes
+ | notes (locale, _) = Generic_Target.locale_target_notes locale;
(* abbrev *)
-fun locale_abbrev locale prmode (b, mx) global_rhs params =
- Generic_Target.background_abbrev (b, global_rhs) (snd params)
- #-> (fn (lhs, _) => Generic_Target.locale_const locale prmode ((b, mx), lhs));
-
-fun class_abbrev class prmode (b, mx) global_rhs params =
- Generic_Target.background_abbrev (b, global_rhs) (snd params)
- #-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs params);
-
fun abbrev ("", _) = Generic_Target.theory_abbrev
- | abbrev (locale, false) = locale_abbrev locale
- | abbrev (class, true) = class_abbrev class;
+ | abbrev (locale, false) = Generic_Target.locale_abbrev locale
+ | abbrev (class, true) = Class.abbrev class;
(* declaration *)
@@ -165,7 +157,7 @@
|> Local_Theory.init background_naming
{define = Generic_Target.define (foundation name_data),
notes = Generic_Target.notes (notes name_data),
- abbrev = Generic_Target.abbrev (abbrev name_data),
+ abbrev = abbrev name_data,
declaration = declaration name_data,
subscription = subscription name_data,
pretty = pretty name_data,
--- a/src/Pure/Isar/overloading.ML Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Pure/Isar/overloading.ML Wed Jun 03 09:32:49 2015 +0200
@@ -11,6 +11,7 @@
val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
-> Proof.context -> Proof.context
val set_primary_constraints: Proof.context -> Proof.context
+ val show_reverted_improvements: bool Config.T;
val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
val overloading_cmd: (string * string * bool) list -> theory -> local_theory
@@ -21,63 +22,46 @@
(* generic check/uncheck combinators for improvable constants *)
-type improvable_syntax = ((((string * typ) list * (string * typ) list) *
- ((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) *
- (term * term) list)) * bool);
+type improvable_syntax = {
+ primary_constraints: (string * typ) list,
+ secondary_constraints: (string * typ) list,
+ improve: string * typ -> (typ * typ) option,
+ subst: string * typ -> (typ * term) option,
+ no_subst_in_abbrev_mode: bool,
+ unchecks: (term * term) list
+}
structure Improvable_Syntax = Proof_Data
(
- type T = {
- primary_constraints: (string * typ) list,
- secondary_constraints: (string * typ) list,
- improve: string * typ -> (typ * typ) option,
- subst: string * typ -> (typ * term) option,
- consider_abbrevs: bool,
- unchecks: (term * term) list,
- passed: bool
- };
- val empty: T = {
- primary_constraints = [],
- secondary_constraints = [],
- improve = K NONE,
- subst = K NONE,
- consider_abbrevs = false,
- unchecks = [],
- passed = true
- };
- fun init _ = empty;
+ type T = {syntax: improvable_syntax, secondary_pass: bool}
+ fun init _ = {syntax = {
+ primary_constraints = [],
+ secondary_constraints = [],
+ improve = K NONE,
+ subst = K NONE,
+ no_subst_in_abbrev_mode = false,
+ unchecks = []
+ }, secondary_pass = false}: T;
);
-fun map_improvable_syntax f = Improvable_Syntax.map (fn {primary_constraints,
- secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed} =>
- let
- val (((primary_constraints', secondary_constraints'),
- (((improve', subst'), consider_abbrevs'), unchecks')), passed')
- = f (((primary_constraints, secondary_constraints),
- (((improve, subst), consider_abbrevs), unchecks)), passed)
- in
- {primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
- improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
- unchecks = unchecks', passed = passed'}
- end);
+fun map_improvable_syntax f =
+ Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = f syntax, secondary_pass = secondary_pass});
-val mark_passed = (map_improvable_syntax o apsnd) (K true);
+val mark_passed =
+ Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = syntax, secondary_pass = true});
fun improve_term_check ts ctxt =
let
val thy = Proof_Context.theory_of ctxt;
- val {secondary_constraints, improve, subst, consider_abbrevs, passed, ...} =
+ val {syntax = {secondary_constraints, improve, subst, no_subst_in_abbrev_mode, ...}, secondary_pass} =
Improvable_Syntax.get ctxt;
- val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
- val passed_or_abbrev = passed orelse is_abbrev;
+ val no_subst = Proof_Context.abbrev_mode ctxt andalso no_subst_in_abbrev_mode;
fun accumulate_improvements (Const (c, ty)) =
(case improve (c, ty) of
SOME ty_ty' => Sign.typ_match thy ty_ty'
| _ => I)
| accumulate_improvements _ = I;
- val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
- val ts' = (map o map_types) (Envir.subst_type improvements) ts;
fun apply_subst t =
Envir.expand_term
(fn Const (c, ty) =>
@@ -87,30 +71,40 @@
then SOME (ty', apply_subst t') else NONE
| NONE => NONE)
| _ => NONE) t;
- val ts'' = if is_abbrev then ts' else map apply_subst ts';
+ val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
+ val ts' =
+ ts
+ |> (map o map_types) (Envir.subst_type improvements)
+ |> not no_subst ? map apply_subst;
in
- if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE
- else if passed_or_abbrev then SOME (ts'', ctxt)
+ if secondary_pass orelse no_subst then
+ if eq_list (op aconv) (ts, ts') then NONE
+ else SOME (ts', ctxt)
else
- SOME (ts'', ctxt
+ SOME (ts', ctxt
|> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints
|> mark_passed)
end;
fun rewrite_liberal thy unchecks t =
- (case try (Pattern.rewrite_term thy unchecks []) t of
+ (case try (Pattern.rewrite_term_top thy unchecks []) t of
NONE => NONE
| SOME t' => if t aconv t' then NONE else SOME t');
+val show_reverted_improvements =
+ Attrib.setup_config_bool @{binding "show_reverted_improvements"} (K true);
+
fun improve_term_uncheck ts ctxt =
let
val thy = Proof_Context.theory_of ctxt;
- val {unchecks, ...} = Improvable_Syntax.get ctxt;
+ val {syntax = {unchecks, ...}, ...} = Improvable_Syntax.get ctxt;
+ val revert = Config.get ctxt show_reverted_improvements;
val ts' = map (rewrite_liberal thy unchecks) ts;
- in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
+ in if revert andalso exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
fun set_primary_constraints ctxt =
- let val {primary_constraints, ...} = Improvable_Syntax.get ctxt;
+ let
+ val {syntax = {primary_constraints, ...}, ...} = Improvable_Syntax.get ctxt;
in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
val activate_improvable_syntax =
@@ -147,7 +141,9 @@
map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
in
ctxt
- |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
+ |> map_improvable_syntax (K {primary_constraints = [],
+ secondary_constraints = [], improve = K NONE, subst = subst,
+ no_subst_in_abbrev_mode = false, unchecks = unchecks})
end;
fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
@@ -165,7 +161,7 @@
if mx <> NoSyn
then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
- | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params);
+ | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
fun pretty lthy =
let
@@ -205,8 +201,8 @@
|> synchronize_syntax
|> Local_Theory.init (Sign.naming_of thy)
{define = Generic_Target.define foundation,
- notes = Generic_Target.notes Generic_Target.theory_notes,
- abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
+ notes = Generic_Target.notes Generic_Target.theory_target_notes,
+ abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
declaration = K Generic_Target.theory_declaration,
subscription = Generic_Target.theory_registration,
pretty = pretty,