syntactic type class for operation mod named after mod;
authorhaftmann
Mon Sep 26 07:56:54 2016 +0200 (2016-09-26)
changeset 63950cdc1e59aa513
parent 63949 e7e41db7221b
child 63951 8739c1cd2851
child 63952 354808e9f44b
syntactic type class for operation mod named after mod;
simplified assumptions of type class semiring_div
NEWS
src/Doc/Main/Main_Doc.thy
src/Doc/Tutorial/Misc/appendix.thy
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Enum.thy
src/HOL/Import/HOL_Light_Maps.thy
src/HOL/Library/Old_SMT/old_smt_normalize.ML
src/HOL/Library/Old_SMT/old_z3_interface.ML
src/HOL/Library/Polynomial.thy
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Nonstandard_Analysis/StarDef.thy
src/HOL/Rings.thy
src/HOL/SMT_Examples/SMT_Examples.certs
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/String.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Word/Word.thy
src/HOL/ex/Arith_Examples.thy
     1.1 --- a/NEWS	Mon Sep 26 07:56:54 2016 +0200
     1.2 +++ b/NEWS	Mon Sep 26 07:56:54 2016 +0200
     1.3 @@ -240,6 +240,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Type class "div" with operation "mod" renamed to type class "modulo" with
     1.8 +operation "modulo", analogously to type class "divide".  This eliminates the
     1.9 +need to qualify any of those names in the presence of infix "mod" syntax.
    1.10 +INCOMPATIBILITY.
    1.11 +
    1.12  * The unique existence quantifier no longer provides 'binder' syntax,
    1.13  but uses syntax translations (as for bounded unique existence). Thus
    1.14  iterated quantification \<exists>!x y. P x y with its slightly confusing
     2.1 --- a/src/Doc/Main/Main_Doc.thy	Mon Sep 26 07:56:54 2016 +0200
     2.2 +++ b/src/Doc/Main/Main_Doc.thy	Mon Sep 26 07:56:54 2016 +0200
     2.3 @@ -325,9 +325,9 @@
     2.4  @{const divide} & @{typeof divide}\\
     2.5  @{const abs} & @{typeof abs}\\
     2.6  @{const sgn} & @{typeof sgn}\\
     2.7 -@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\
     2.8 -@{const Rings.divide} & @{typeof Rings.divide}\\
     2.9 -@{const div_class.mod} & @{typeof "div_class.mod"}\\
    2.10 +@{const Rings.dvd} & @{typeof Rings.dvd}\\
    2.11 +@{const divide} & @{typeof divide}\\
    2.12 +@{const modulo} & @{typeof modulo}\\
    2.13  \end{supertabular}
    2.14  
    2.15  \subsubsection*{Syntax}
     3.1 --- a/src/Doc/Tutorial/Misc/appendix.thy	Mon Sep 26 07:56:54 2016 +0200
     3.2 +++ b/src/Doc/Tutorial/Misc/appendix.thy	Mon Sep 26 07:56:54 2016 +0200
     3.3 @@ -16,7 +16,7 @@
     3.4  @{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\
     3.5  @{term [source] inverse_divide} & @{typeof [show_sorts] "inverse_divide"} & (infixl $/$ 70) \\
     3.6  @{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $div$ 70) \\
     3.7 -@{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\
     3.8 +@{term [source] modulo} & @{typeof [show_sorts] "modulo"} & (infixl $mod$ 70) \\
     3.9  @{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\
    3.10  @{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\
    3.11  @{term [source] less_eq} & @{typeof [show_sorts] "less_eq"} & (infixl $\le$ 50) \\
     4.1 --- a/src/HOL/Code_Numeral.thy	Mon Sep 26 07:56:54 2016 +0200
     4.2 +++ b/src/HOL/Code_Numeral.thy	Mon Sep 26 07:56:54 2016 +0200
     4.3 @@ -175,11 +175,11 @@
     4.4  
     4.5  declare divide_integer.rep_eq [simp]
     4.6  
     4.7 -lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
     4.8 -  is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
     4.9 +lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    4.10 +  is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
    4.11    .
    4.12  
    4.13 -declare mod_integer.rep_eq [simp]
    4.14 +declare modulo_integer.rep_eq [simp]
    4.15  
    4.16  lift_definition abs_integer :: "integer \<Rightarrow> integer"
    4.17    is "abs :: int \<Rightarrow> int"
    4.18 @@ -534,7 +534,7 @@
    4.19    moreover have "2 * (j div 2) = j - j mod 2"
    4.20      by (simp add: zmult_div_cancel mult.commute)
    4.21    ultimately show ?thesis
    4.22 -    by (auto simp add: split_def Let_def mod_integer_def nat_of_integer_def not_le
    4.23 +    by (auto simp add: split_def Let_def modulo_integer_def nat_of_integer_def not_le
    4.24        nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1)
    4.25        (auto simp add: mult_2 [symmetric])
    4.26  qed
    4.27 @@ -761,11 +761,11 @@
    4.28  
    4.29  declare divide_natural.rep_eq [simp]
    4.30  
    4.31 -lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
    4.32 -  is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
    4.33 +lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
    4.34 +  is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
    4.35    .
    4.36  
    4.37 -declare mod_natural.rep_eq [simp]
    4.38 +declare modulo_natural.rep_eq [simp]
    4.39  
    4.40  lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
    4.41    is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
    4.42 @@ -973,7 +973,7 @@
    4.43    functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural"
    4.44      "plus :: natural \<Rightarrow> _" "minus :: natural \<Rightarrow> _"
    4.45      "times :: natural \<Rightarrow> _" "divide :: natural \<Rightarrow> _"
    4.46 -    "Divides.mod :: natural \<Rightarrow> _"
    4.47 +    "modulo :: natural \<Rightarrow> _"
    4.48      integer_of_natural natural_of_integer
    4.49  
    4.50  end
     5.1 --- a/src/HOL/Divides.thy	Mon Sep 26 07:56:54 2016 +0200
     5.2 +++ b/src/HOL/Divides.thy	Mon Sep 26 07:56:54 2016 +0200
     5.3 @@ -11,13 +11,10 @@
     5.4  
     5.5  subsection \<open>Abstract division in commutative semirings.\<close>
     5.6  
     5.7 -class div = dvd + divide +
     5.8 -  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
     5.9 -
    5.10 -class semiring_div = semidom + div +
    5.11 +class semiring_div = semidom + modulo +
    5.12    assumes mod_div_equality: "a div b * b + a mod b = a"
    5.13 -    and div_by_0 [simp]: "a div 0 = 0"
    5.14 -    and div_0 [simp]: "0 div a = 0"
    5.15 +    and div_by_0: "a div 0 = 0"
    5.16 +    and div_0: "0 div a = 0"
    5.17      and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
    5.18      and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
    5.19  begin
    5.20 @@ -27,8 +24,8 @@
    5.21    fix b a
    5.22    assume "b \<noteq> 0"
    5.23    then show "a * b div b = a"
    5.24 -    using div_mult_self1 [of b 0 a] by (simp add: ac_simps)
    5.25 -qed simp
    5.26 +    using div_mult_self1 [of b 0 a] by (simp add: ac_simps div_0)
    5.27 +qed (simp add: div_by_0)
    5.28  
    5.29  lemma div_by_1:
    5.30    "a div 1 = a"
    5.31 @@ -42,7 +39,7 @@
    5.32    "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    5.33    by (fact nonzero_mult_divide_cancel_right)
    5.34  
    5.35 -text \<open>@{const divide} and @{const mod}\<close>
    5.36 +text \<open>@{const divide} and @{const modulo}\<close>
    5.37  
    5.38  lemma mod_div_equality2: "b * (a div b) + a mod b = a"
    5.39    unfolding mult.commute [of b]
    5.40 @@ -836,7 +833,7 @@
    5.41  begin
    5.42  
    5.43  text \<open>
    5.44 -  We define @{const divide} and @{const mod} on @{typ nat} by means
    5.45 +  We define @{const divide} and @{const modulo} on @{typ nat} by means
    5.46    of a characteristic relation with two input arguments
    5.47    @{term "m::nat"}, @{term "n::nat"} and two output arguments
    5.48    @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
    5.49 @@ -953,8 +950,8 @@
    5.50  definition divide_nat where
    5.51    div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
    5.52  
    5.53 -definition mod_nat where
    5.54 -  "m mod n = snd (Divides.divmod_nat m n)"
    5.55 +definition modulo_nat where
    5.56 +  mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
    5.57  
    5.58  lemma fst_divmod_nat [simp]:
    5.59    "fst (Divides.divmod_nat m n) = m div n"
    5.60 @@ -981,7 +978,7 @@
    5.61  lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
    5.62    using Divides.divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
    5.63  
    5.64 -text \<open>The ''recursion'' equations for @{const divide} and @{const mod}\<close>
    5.65 +text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
    5.66  
    5.67  lemma div_less [simp]:
    5.68    fixes m n :: nat
    5.69 @@ -1059,7 +1056,7 @@
    5.70      let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
    5.71    by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
    5.72  
    5.73 -text \<open>Simproc for cancelling @{const divide} and @{const mod}\<close>
    5.74 +text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
    5.75  
    5.76  ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
    5.77  
    5.78 @@ -1067,7 +1064,7 @@
    5.79  structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
    5.80  (
    5.81    val div_name = @{const_name divide};
    5.82 -  val mod_name = @{const_name mod};
    5.83 +  val mod_name = @{const_name modulo};
    5.84    val mk_binop = HOLogic.mk_binop;
    5.85    val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    5.86    val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
    5.87 @@ -1732,7 +1729,7 @@
    5.88  apply (blast intro: unique_quotient)
    5.89  done
    5.90  
    5.91 -instantiation int :: Divides.div
    5.92 +instantiation int :: modulo
    5.93  begin
    5.94  
    5.95  definition divide_int
    5.96 @@ -1743,7 +1740,7 @@
    5.97          if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
    5.98          else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
    5.99  
   5.100 -definition mod_int
   5.101 +definition modulo_int
   5.102    where "k mod l = (if l = 0 then k else if l dvd k then 0
   5.103      else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
   5.104        then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
   5.105 @@ -1755,7 +1752,7 @@
   5.106  
   5.107  lemma divmod_int_rel:
   5.108    "divmod_int_rel k l (k div l, k mod l)"
   5.109 -  unfolding divmod_int_rel_def divide_int_def mod_int_def
   5.110 +  unfolding divmod_int_rel_def divide_int_def modulo_int_def
   5.111    apply (cases k rule: int_cases3)
   5.112    apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
   5.113    apply (cases l rule: int_cases3)
   5.114 @@ -1849,15 +1846,15 @@
   5.115    by (simp add: divide_int_def)
   5.116  
   5.117  lemma zmod_int: "int (a mod b) = int a mod int b"
   5.118 -  by (simp add: mod_int_def int_dvd_iff)
   5.119 +  by (simp add: modulo_int_def int_dvd_iff)
   5.120    
   5.121  text \<open>Tool setup\<close>
   5.122  
   5.123  ML \<open>
   5.124  structure Cancel_Div_Mod_Int = Cancel_Div_Mod
   5.125  (
   5.126 -  val div_name = @{const_name Rings.divide};
   5.127 -  val mod_name = @{const_name mod};
   5.128 +  val div_name = @{const_name divide};
   5.129 +  val mod_name = @{const_name modulo};
   5.130    val mk_binop = HOLogic.mk_binop;
   5.131    val mk_sum = Arith_Data.mk_sum HOLogic.intT;
   5.132    val dest_sum = Arith_Data.dest_sum;
   5.133 @@ -2223,7 +2220,7 @@
   5.134                        split_neg_lemma [of concl: "%x y. P y"])
   5.135  done
   5.136  
   5.137 -text \<open>Enable (lin)arith to deal with @{const divide} and @{const mod}
   5.138 +text \<open>Enable (lin)arith to deal with @{const divide} and @{const modulo}
   5.139    when these are applied to some constant that is of the form
   5.140    @{term "numeral k"}:\<close>
   5.141  declare split_zdiv [of _ _ "numeral k", arith_split] for k
   5.142 @@ -2327,7 +2324,7 @@
   5.143  by (simp add: divide_int_def)
   5.144  
   5.145  lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
   5.146 -by (simp add: mod_int_def)
   5.147 +by (simp add: modulo_int_def)
   5.148  
   5.149  lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
   5.150  apply (subgoal_tac "a div b \<le> -1", force)
   5.151 @@ -2445,9 +2442,9 @@
   5.152    "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
   5.153  proof -
   5.154    have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
   5.155 -    using that by (simp only: snd_divmod mod_int_def) auto
   5.156 +    using that by (simp only: snd_divmod modulo_int_def) auto
   5.157    then show ?thesis
   5.158 -    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def mod_int_def)
   5.159 +    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
   5.160  qed
   5.161  
   5.162  lemma numeral_div_minus_numeral [simp]:
   5.163 @@ -2463,9 +2460,9 @@
   5.164    "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
   5.165  proof -
   5.166    have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
   5.167 -    using that by (simp only: snd_divmod mod_int_def) auto
   5.168 +    using that by (simp only: snd_divmod modulo_int_def) auto
   5.169    then show ?thesis
   5.170 -    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def mod_int_def)
   5.171 +    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
   5.172  qed
   5.173  
   5.174  lemma minus_one_div_numeral [simp]:
     6.1 --- a/src/HOL/Enum.thy	Mon Sep 26 07:56:54 2016 +0200
     6.2 +++ b/src/HOL/Enum.thy	Mon Sep 26 07:56:54 2016 +0200
     6.3 @@ -580,7 +580,7 @@
     6.4  instantiation finite_1 :: 
     6.5    "{linordered_ring_strict, linordered_comm_semiring_strict, ordered_comm_ring,
     6.6      ordered_cancel_comm_monoid_diff, comm_monoid_mult, ordered_ring_abs,
     6.7 -    one, Divides.div, sgn_if, inverse}"
     6.8 +    one, modulo, sgn_if, inverse}"
     6.9  begin
    6.10  definition [simp]: "Groups.zero = a\<^sub>1"
    6.11  definition [simp]: "Groups.one = a\<^sub>1"
    6.12 @@ -698,7 +698,7 @@
    6.13  instance
    6.14  by intro_classes
    6.15    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
    6.16 -       inverse_finite_2_def divide_finite_2_def abs_finite_2_def mod_finite_2_def sgn_finite_2_def
    6.17 +       inverse_finite_2_def divide_finite_2_def abs_finite_2_def modulo_finite_2_def sgn_finite_2_def
    6.18       split: finite_2.splits)
    6.19  end
    6.20  
    6.21 @@ -825,7 +825,7 @@
    6.22  instance
    6.23  by intro_classes
    6.24    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
    6.25 -       inverse_finite_3_def divide_finite_3_def abs_finite_3_def mod_finite_3_def sgn_finite_3_def
    6.26 +       inverse_finite_3_def divide_finite_3_def abs_finite_3_def modulo_finite_3_def sgn_finite_3_def
    6.27         less_finite_3_def
    6.28       split: finite_3.splits)
    6.29  end
     7.1 --- a/src/HOL/Import/HOL_Light_Maps.thy	Mon Sep 26 07:56:54 2016 +0200
     7.2 +++ b/src/HOL/Import/HOL_Light_Maps.thy	Mon Sep 26 07:56:54 2016 +0200
     7.3 @@ -197,7 +197,7 @@
     7.4    "fact (id 0) = id (bit1 0) \<and> (\<forall>n. fact (Suc n) = Suc n * fact n)"
     7.5    by simp
     7.6  
     7.7 -import_const_map MOD : mod
     7.8 +import_const_map MOD : modulo
     7.9  import_const_map DIV : divide
    7.10  
    7.11  lemma DIVISION_0:
     8.1 --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Mon Sep 26 07:56:54 2016 +0200
     8.2 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Mon Sep 26 07:56:54 2016 +0200
     8.3 @@ -430,7 +430,7 @@
     8.4      @{const Suc}, @{const plus (nat)}, @{const minus (nat)}]
     8.5  
     8.6    val mult_nat_ops =
     8.7 -    [@{const times (nat)}, @{const divide (nat)}, @{const mod (nat)}]
     8.8 +    [@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}]
     8.9  
    8.10    val nat_ops = simple_nat_ops @ mult_nat_ops
    8.11  
     9.1 --- a/src/HOL/Library/Old_SMT/old_z3_interface.ML	Mon Sep 26 07:56:54 2016 +0200
     9.2 +++ b/src/HOL/Library/Old_SMT/old_z3_interface.ML	Mon Sep 26 07:56:54 2016 +0200
     9.3 @@ -42,7 +42,7 @@
     9.4      end
     9.5  
     9.6    fun is_div_mod @{const divide (int)} = true
     9.7 -    | is_div_mod @{const mod (int)} = true
     9.8 +    | is_div_mod @{const modulo (int)} = true
     9.9      | is_div_mod _ = false
    9.10  
    9.11    val div_by_z3div = @{lemma
    10.1 --- a/src/HOL/Library/Polynomial.thy	Mon Sep 26 07:56:54 2016 +0200
    10.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Sep 26 07:56:54 2016 +0200
    10.3 @@ -1894,8 +1894,8 @@
    10.4  instantiation poly :: (field) ring_div
    10.5  begin
    10.6  
    10.7 -definition mod_poly where
    10.8 -  "f mod g \<equiv>
    10.9 +definition modulo_poly where
   10.10 +  mod_poly_def: "f mod g \<equiv>
   10.11      if g = 0 then f
   10.12      else pseudo_mod (smult ((1/coeff g (degree g)) ^ (Suc (degree f) - degree g)) f) g"
   10.13  
    11.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Mon Sep 26 07:56:54 2016 +0200
    11.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Mon Sep 26 07:56:54 2016 +0200
    11.3 @@ -67,7 +67,7 @@
    11.4  definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
    11.5  definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
    11.6  definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
    11.7 -definition [simp]: "mod_real = (mod_field :: real \<Rightarrow> _)"
    11.8 +definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
    11.9  
   11.10  instance by standard (simp_all add: dvd_field_iff divide_simps)
   11.11  end
   11.12 @@ -94,7 +94,7 @@
   11.13  definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
   11.14  definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
   11.15  definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
   11.16 -definition [simp]: "mod_rat = (mod_field :: rat \<Rightarrow> _)"
   11.17 +definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
   11.18  
   11.19  instance by standard (simp_all add: dvd_field_iff divide_simps)
   11.20  end
   11.21 @@ -121,7 +121,7 @@
   11.22  definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
   11.23  definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
   11.24  definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
   11.25 -definition [simp]: "mod_complex = (mod_field :: complex \<Rightarrow> _)"
   11.26 +definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
   11.27  
   11.28  instance by standard (simp_all add: dvd_field_iff divide_simps)
   11.29  end
    12.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Sep 26 07:56:54 2016 +0200
    12.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Sep 26 07:56:54 2016 +0200
    12.3 @@ -59,7 +59,7 @@
    12.4  setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Char}]\<close>
    12.5  setup \<open>Predicate_Compile_Data.keep_functions [@{const_name Char}]\<close>
    12.6  
    12.7 -setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name mod}, @{const_name times}]\<close>
    12.8 +setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name modulo}, @{const_name times}]\<close>
    12.9  
   12.10  section \<open>Arithmetic operations\<close>
   12.11  
    13.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Sep 26 07:56:54 2016 +0200
    13.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Sep 26 07:56:54 2016 +0200
    13.3 @@ -283,12 +283,12 @@
    13.4     (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
    13.5     (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
    13.6     (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
    13.7 -      (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
    13.8 +   (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
    13.9     (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}),
   13.10     (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
   13.11     (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
   13.12     (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
   13.13 -   (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
   13.14 +   (@{const_name "Rings.modulo"}, @{typ "prop => prop => prop"}),
   13.15     (@{const_name Rings.divide}, @{typ "prop => prop => prop"}),
   13.16     (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
   13.17     (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
    14.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Mon Sep 26 07:56:54 2016 +0200
    14.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Mon Sep 26 07:56:54 2016 +0200
    14.3 @@ -527,7 +527,7 @@
    14.4  
    14.5  instance star :: (Rings.dvd) Rings.dvd ..
    14.6  
    14.7 -instantiation star :: (Divides.div) Divides.div
    14.8 +instantiation star :: (modulo) modulo
    14.9  begin
   14.10  
   14.11  definition
    15.1 --- a/src/HOL/Rings.thy	Mon Sep 26 07:56:54 2016 +0200
    15.2 +++ b/src/HOL/Rings.thy	Mon Sep 26 07:56:54 2016 +0200
    15.3 @@ -542,6 +542,8 @@
    15.4      \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
    15.5  \<close>
    15.6  
    15.7 +text \<open>Syntactic division operator\<close>
    15.8 +
    15.9  class divide =
   15.10    fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
   15.11  
   15.12 @@ -569,6 +571,13 @@
   15.13  
   15.14  setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
   15.15  
   15.16 +text \<open>Syntactic division remainder operator\<close>
   15.17 +
   15.18 +class modulo = dvd + divide +
   15.19 +  fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
   15.20 +
   15.21 +text \<open>Algebraic classes with division\<close>
   15.22 +  
   15.23  class semidom_divide = semidom + divide +
   15.24    assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
   15.25    assumes divide_zero [simp]: "a div 0 = 0"
    16.1 --- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Sep 26 07:56:54 2016 +0200
    16.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Sep 26 07:56:54 2016 +0200
    16.3 @@ -6057,3 +6057,579 @@
    16.4  (let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
    16.5  (mp (asserted $x32) @x42 false))))))))
    16.6  
    16.7 +0b997744cf42fde45b98a34c933b0698332e657f 113 0
    16.8 +unsat
    16.9 +((set-logic <null>)
   16.10 +(proof
   16.11 +(let ((?x228 (mod x$ 2)))
   16.12 +(let ((?x262 (* (- 1) ?x228)))
   16.13 +(let ((?x31 (modulo$ x$ 2)))
   16.14 +(let ((?x263 (+ ?x31 ?x262)))
   16.15 +(let (($x280 (>= ?x263 0)))
   16.16 +(let (($x264 (= ?x263 0)))
   16.17 +(let (($x205 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x136 (mod ?v0 ?v1)))
   16.18 +(let ((?x93 (* (- 1) ?v1)))
   16.19 +(let ((?x90 (* (- 1) ?v0)))
   16.20 +(let ((?x144 (mod ?x90 ?x93)))
   16.21 +(let ((?x150 (* (- 1) ?x144)))
   16.22 +(let (($x111 (<= ?v1 0)))
   16.23 +(let ((?x170 (ite $x111 ?x150 ?x136)))
   16.24 +(let (($x78 (= ?v1 0)))
   16.25 +(let ((?x175 (ite $x78 ?v0 ?x170)))
   16.26 +(let ((?x135 (modulo$ ?v0 ?v1)))
   16.27 +(= ?x135 ?x175))))))))))) :pattern ( (modulo$ ?v0 ?v1) ) :qid k!9))
   16.28 +))
   16.29 +(let (($x181 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x136 (mod ?v0 ?v1)))
   16.30 +(let ((?x93 (* (- 1) ?v1)))
   16.31 +(let ((?x90 (* (- 1) ?v0)))
   16.32 +(let ((?x144 (mod ?x90 ?x93)))
   16.33 +(let ((?x150 (* (- 1) ?x144)))
   16.34 +(let (($x111 (<= ?v1 0)))
   16.35 +(let ((?x170 (ite $x111 ?x150 ?x136)))
   16.36 +(let (($x78 (= ?v1 0)))
   16.37 +(let ((?x175 (ite $x78 ?v0 ?x170)))
   16.38 +(let ((?x135 (modulo$ ?v0 ?v1)))
   16.39 +(= ?x135 ?x175))))))))))) :qid k!9))
   16.40 +))
   16.41 +(let ((?x136 (mod ?1 ?0)))
   16.42 +(let ((?x93 (* (- 1) ?0)))
   16.43 +(let ((?x90 (* (- 1) ?1)))
   16.44 +(let ((?x144 (mod ?x90 ?x93)))
   16.45 +(let ((?x150 (* (- 1) ?x144)))
   16.46 +(let (($x111 (<= ?0 0)))
   16.47 +(let ((?x170 (ite $x111 ?x150 ?x136)))
   16.48 +(let (($x78 (= ?0 0)))
   16.49 +(let ((?x175 (ite $x78 ?1 ?x170)))
   16.50 +(let ((?x135 (modulo$ ?1 ?0)))
   16.51 +(let (($x178 (= ?x135 ?x175)))
   16.52 +(let (($x142 (forall ((?v0 Int) (?v1 Int) )(! (let (($x78 (= ?v1 0)))
   16.53 +(let ((?x140 (ite $x78 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
   16.54 +(let ((?x135 (modulo$ ?v0 ?v1)))
   16.55 +(= ?x135 ?x140)))) :qid k!9))
   16.56 +))
   16.57 +(let (($x164 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x93 (* (- 1) ?v1)))
   16.58 +(let ((?x90 (* (- 1) ?v0)))
   16.59 +(let ((?x144 (mod ?x90 ?x93)))
   16.60 +(let ((?x150 (* (- 1) ?x144)))
   16.61 +(let ((?x136 (mod ?v0 ?v1)))
   16.62 +(let (($x79 (< 0 ?v1)))
   16.63 +(let ((?x155 (ite $x79 ?x136 ?x150)))
   16.64 +(let (($x78 (= ?v1 0)))
   16.65 +(let ((?x158 (ite $x78 ?v0 ?x155)))
   16.66 +(let ((?x135 (modulo$ ?v0 ?v1)))
   16.67 +(= ?x135 ?x158))))))))))) :qid k!9))
   16.68 +))
   16.69 +(let ((@x169 (monotonicity (rewrite (= (< 0 ?0) (not $x111))) (= (ite (< 0 ?0) ?x136 ?x150) (ite (not $x111) ?x136 ?x150)))))
   16.70 +(let ((@x174 (trans @x169 (rewrite (= (ite (not $x111) ?x136 ?x150) ?x170)) (= (ite (< 0 ?0) ?x136 ?x150) ?x170))))
   16.71 +(let ((@x177 (monotonicity @x174 (= (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150)) ?x175))))
   16.72 +(let ((@x180 (monotonicity @x177 (= (= ?x135 (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150))) $x178))))
   16.73 +(let (($x79 (< 0 ?0)))
   16.74 +(let ((?x155 (ite $x79 ?x136 ?x150)))
   16.75 +(let ((?x158 (ite $x78 ?1 ?x155)))
   16.76 +(let (($x161 (= ?x135 ?x158)))
   16.77 +(let (($x162 (= (= ?x135 (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))))) $x161)))
   16.78 +(let ((@x146 (monotonicity (rewrite (= (- ?1) ?x90)) (rewrite (= (- ?0) ?x93)) (= (mod (- ?1) (- ?0)) ?x144))))
   16.79 +(let ((@x154 (trans (monotonicity @x146 (= (- (mod (- ?1) (- ?0))) (- ?x144))) (rewrite (= (- ?x144) ?x150)) (= (- (mod (- ?1) (- ?0))) ?x150))))
   16.80 +(let ((@x157 (monotonicity @x154 (= (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))) ?x155))))
   16.81 +(let ((@x160 (monotonicity @x157 (= (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0))))) ?x158))))
   16.82 +(let ((@x185 (trans (quant-intro (monotonicity @x160 $x162) (= $x142 $x164)) (quant-intro @x180 (= $x164 $x181)) (= $x142 $x181))))
   16.83 +(let ((@x196 (mp~ (mp (asserted $x142) @x185 $x181) (nnf-pos (refl (~ $x178 $x178)) (~ $x181 $x181)) $x181)))
   16.84 +(let ((@x210 (mp @x196 (quant-intro (refl (= $x178 $x178)) (= $x181 $x205)) $x205)))
   16.85 +(let (($x270 (or (not $x205) $x264)))
   16.86 +(let ((?x225 (* (- 1) 2)))
   16.87 +(let ((?x224 (* (- 1) x$)))
   16.88 +(let ((?x226 (mod ?x224 ?x225)))
   16.89 +(let ((?x227 (* (- 1) ?x226)))
   16.90 +(let (($x223 (<= 2 0)))
   16.91 +(let ((?x229 (ite $x223 ?x227 ?x228)))
   16.92 +(let (($x222 (= 2 0)))
   16.93 +(let ((?x230 (ite $x222 x$ ?x229)))
   16.94 +(let (($x231 (= ?x31 ?x230)))
   16.95 +(let ((@x244 (monotonicity (monotonicity (rewrite (= ?x225 (- 2))) (= ?x226 (mod ?x224 (- 2)))) (= ?x227 (* (- 1) (mod ?x224 (- 2)))))))
   16.96 +(let ((@x247 (monotonicity (rewrite (= $x223 false)) @x244 (= ?x229 (ite false (* (- 1) (mod ?x224 (- 2))) ?x228)))))
   16.97 +(let ((@x251 (trans @x247 (rewrite (= (ite false (* (- 1) (mod ?x224 (- 2))) ?x228) ?x228)) (= ?x229 ?x228))))
   16.98 +(let ((@x254 (monotonicity (rewrite (= $x222 false)) @x251 (= ?x230 (ite false x$ ?x228)))))
   16.99 +(let ((@x261 (monotonicity (trans @x254 (rewrite (= (ite false x$ ?x228) ?x228)) (= ?x230 ?x228)) (= $x231 (= ?x31 ?x228)))))
  16.100 +(let ((@x274 (monotonicity (trans @x261 (rewrite (= (= ?x31 ?x228) $x264)) (= $x231 $x264)) (= (or (not $x205) $x231) $x270))))
  16.101 +(let ((@x277 (trans @x274 (rewrite (= $x270 $x270)) (= (or (not $x205) $x231) $x270))))
  16.102 +(let ((@x278 (mp ((_ quant-inst x$ 2) (or (not $x205) $x231)) @x277 $x270)))
  16.103 +(let ((@x332 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x264) $x280)) (unit-resolution @x278 @x210 $x264) $x280)))
  16.104 +(let (($x305 (>= ?x228 0)))
  16.105 +(let (($x64 (>= ?x31 0)))
  16.106 +(let (($x67 (not $x64)))
  16.107 +(let (($x36 (not (<= (+ x$ 1) (+ x$ (+ (* 2 ?x31) 1))))))
  16.108 +(let ((@x69 (monotonicity (rewrite (= (>= (* 2 ?x31) 0) $x64)) (= (not (>= (* 2 ?x31) 0)) $x67))))
  16.109 +(let ((?x32 (* 2 ?x31)))
  16.110 +(let ((?x47 (+ 1 x$ ?x32)))
  16.111 +(let (($x52 (<= (+ 1 x$) ?x47)))
  16.112 +(let (($x55 (not $x52)))
  16.113 +(let ((@x63 (monotonicity (rewrite (= $x52 (>= ?x32 0))) (= $x55 (not (>= ?x32 0))))))
  16.114 +(let ((@x46 (monotonicity (rewrite (= (+ ?x32 1) (+ 1 ?x32))) (= (+ x$ (+ ?x32 1)) (+ x$ (+ 1 ?x32))))))
  16.115 +(let ((@x51 (trans @x46 (rewrite (= (+ x$ (+ 1 ?x32)) ?x47)) (= (+ x$ (+ ?x32 1)) ?x47))))
  16.116 +(let ((@x54 (monotonicity (rewrite (= (+ x$ 1) (+ 1 x$))) @x51 (= (<= (+ x$ 1) (+ x$ (+ ?x32 1))) $x52))))
  16.117 +(let ((@x73 (trans (monotonicity @x54 (= $x36 $x55)) (trans @x63 @x69 (= $x55 $x67)) (= $x36 $x67))))
  16.118 +(let ((@x74 (mp (asserted $x36) @x73 $x67)))
  16.119 +((_ th-lemma arith farkas -1 1 1) @x74 (unit-resolution ((_ th-lemma arith) (or false $x305)) (true-axiom true) $x305) @x332 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  16.120 +
  16.121 +2e67f9e254b2a35a9d35027c6e63de01bc5086bd 112 0
  16.122 +unsat
  16.123 +((set-logic <null>)
  16.124 +(proof
  16.125 +(let ((?x224 (mod x$ 2)))
  16.126 +(let (($x318 (>= ?x224 2)))
  16.127 +(let (($x319 (not $x318)))
  16.128 +(let ((?x258 (* (- 1) ?x224)))
  16.129 +(let ((?x29 (modulo$ x$ 2)))
  16.130 +(let ((?x259 (+ ?x29 ?x258)))
  16.131 +(let (($x275 (<= ?x259 0)))
  16.132 +(let (($x260 (= ?x259 0)))
  16.133 +(let (($x201 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x132 (mod ?v0 ?v1)))
  16.134 +(let ((?x89 (* (- 1) ?v1)))
  16.135 +(let ((?x86 (* (- 1) ?v0)))
  16.136 +(let ((?x140 (mod ?x86 ?x89)))
  16.137 +(let ((?x146 (* (- 1) ?x140)))
  16.138 +(let (($x107 (<= ?v1 0)))
  16.139 +(let ((?x166 (ite $x107 ?x146 ?x132)))
  16.140 +(let (($x74 (= ?v1 0)))
  16.141 +(let ((?x171 (ite $x74 ?v0 ?x166)))
  16.142 +(let ((?x131 (modulo$ ?v0 ?v1)))
  16.143 +(= ?x131 ?x171))))))))))) :pattern ( (modulo$ ?v0 ?v1) ) :qid k!9))
  16.144 +))
  16.145 +(let (($x177 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x132 (mod ?v0 ?v1)))
  16.146 +(let ((?x89 (* (- 1) ?v1)))
  16.147 +(let ((?x86 (* (- 1) ?v0)))
  16.148 +(let ((?x140 (mod ?x86 ?x89)))
  16.149 +(let ((?x146 (* (- 1) ?x140)))
  16.150 +(let (($x107 (<= ?v1 0)))
  16.151 +(let ((?x166 (ite $x107 ?x146 ?x132)))
  16.152 +(let (($x74 (= ?v1 0)))
  16.153 +(let ((?x171 (ite $x74 ?v0 ?x166)))
  16.154 +(let ((?x131 (modulo$ ?v0 ?v1)))
  16.155 +(= ?x131 ?x171))))))))))) :qid k!9))
  16.156 +))
  16.157 +(let ((?x132 (mod ?1 ?0)))
  16.158 +(let ((?x89 (* (- 1) ?0)))
  16.159 +(let ((?x86 (* (- 1) ?1)))
  16.160 +(let ((?x140 (mod ?x86 ?x89)))
  16.161 +(let ((?x146 (* (- 1) ?x140)))
  16.162 +(let (($x107 (<= ?0 0)))
  16.163 +(let ((?x166 (ite $x107 ?x146 ?x132)))
  16.164 +(let (($x74 (= ?0 0)))
  16.165 +(let ((?x171 (ite $x74 ?1 ?x166)))
  16.166 +(let ((?x131 (modulo$ ?1 ?0)))
  16.167 +(let (($x174 (= ?x131 ?x171)))
  16.168 +(let (($x138 (forall ((?v0 Int) (?v1 Int) )(! (let (($x74 (= ?v1 0)))
  16.169 +(let ((?x136 (ite $x74 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
  16.170 +(let ((?x131 (modulo$ ?v0 ?v1)))
  16.171 +(= ?x131 ?x136)))) :qid k!9))
  16.172 +))
  16.173 +(let (($x160 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x89 (* (- 1) ?v1)))
  16.174 +(let ((?x86 (* (- 1) ?v0)))
  16.175 +(let ((?x140 (mod ?x86 ?x89)))
  16.176 +(let ((?x146 (* (- 1) ?x140)))
  16.177 +(let ((?x132 (mod ?v0 ?v1)))
  16.178 +(let (($x75 (< 0 ?v1)))
  16.179 +(let ((?x151 (ite $x75 ?x132 ?x146)))
  16.180 +(let (($x74 (= ?v1 0)))
  16.181 +(let ((?x154 (ite $x74 ?v0 ?x151)))
  16.182 +(let ((?x131 (modulo$ ?v0 ?v1)))
  16.183 +(= ?x131 ?x154))))))))))) :qid k!9))
  16.184 +))
  16.185 +(let ((@x165 (monotonicity (rewrite (= (< 0 ?0) (not $x107))) (= (ite (< 0 ?0) ?x132 ?x146) (ite (not $x107) ?x132 ?x146)))))
  16.186 +(let ((@x170 (trans @x165 (rewrite (= (ite (not $x107) ?x132 ?x146) ?x166)) (= (ite (< 0 ?0) ?x132 ?x146) ?x166))))
  16.187 +(let ((@x173 (monotonicity @x170 (= (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146)) ?x171))))
  16.188 +(let ((@x176 (monotonicity @x173 (= (= ?x131 (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146))) $x174))))
  16.189 +(let (($x75 (< 0 ?0)))
  16.190 +(let ((?x151 (ite $x75 ?x132 ?x146)))
  16.191 +(let ((?x154 (ite $x74 ?1 ?x151)))
  16.192 +(let (($x157 (= ?x131 ?x154)))
  16.193 +(let (($x158 (= (= ?x131 (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))))) $x157)))
  16.194 +(let ((@x142 (monotonicity (rewrite (= (- ?1) ?x86)) (rewrite (= (- ?0) ?x89)) (= (mod (- ?1) (- ?0)) ?x140))))
  16.195 +(let ((@x150 (trans (monotonicity @x142 (= (- (mod (- ?1) (- ?0))) (- ?x140))) (rewrite (= (- ?x140) ?x146)) (= (- (mod (- ?1) (- ?0))) ?x146))))
  16.196 +(let ((@x153 (monotonicity @x150 (= (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))) ?x151))))
  16.197 +(let ((@x156 (monotonicity @x153 (= (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0))))) ?x154))))
  16.198 +(let ((@x181 (trans (quant-intro (monotonicity @x156 $x158) (= $x138 $x160)) (quant-intro @x176 (= $x160 $x177)) (= $x138 $x177))))
  16.199 +(let ((@x192 (mp~ (mp (asserted $x138) @x181 $x177) (nnf-pos (refl (~ $x174 $x174)) (~ $x177 $x177)) $x177)))
  16.200 +(let ((@x206 (mp @x192 (quant-intro (refl (= $x174 $x174)) (= $x177 $x201)) $x201)))
  16.201 +(let (($x266 (or (not $x201) $x260)))
  16.202 +(let ((?x221 (* (- 1) 2)))
  16.203 +(let ((?x220 (* (- 1) x$)))
  16.204 +(let ((?x222 (mod ?x220 ?x221)))
  16.205 +(let ((?x223 (* (- 1) ?x222)))
  16.206 +(let (($x219 (<= 2 0)))
  16.207 +(let ((?x225 (ite $x219 ?x223 ?x224)))
  16.208 +(let (($x218 (= 2 0)))
  16.209 +(let ((?x226 (ite $x218 x$ ?x225)))
  16.210 +(let (($x227 (= ?x29 ?x226)))
  16.211 +(let ((@x240 (monotonicity (monotonicity (rewrite (= ?x221 (- 2))) (= ?x222 (mod ?x220 (- 2)))) (= ?x223 (* (- 1) (mod ?x220 (- 2)))))))
  16.212 +(let ((@x243 (monotonicity (rewrite (= $x219 false)) @x240 (= ?x225 (ite false (* (- 1) (mod ?x220 (- 2))) ?x224)))))
  16.213 +(let ((@x247 (trans @x243 (rewrite (= (ite false (* (- 1) (mod ?x220 (- 2))) ?x224) ?x224)) (= ?x225 ?x224))))
  16.214 +(let ((@x250 (monotonicity (rewrite (= $x218 false)) @x247 (= ?x226 (ite false x$ ?x224)))))
  16.215 +(let ((@x257 (monotonicity (trans @x250 (rewrite (= (ite false x$ ?x224) ?x224)) (= ?x226 ?x224)) (= $x227 (= ?x29 ?x224)))))
  16.216 +(let ((@x270 (monotonicity (trans @x257 (rewrite (= (= ?x29 ?x224) $x260)) (= $x227 $x260)) (= (or (not $x201) $x227) $x266))))
  16.217 +(let ((@x273 (trans @x270 (rewrite (= $x266 $x266)) (= (or (not $x201) $x227) $x266))))
  16.218 +(let ((@x274 (mp ((_ quant-inst x$ 2) (or (not $x201) $x227)) @x273 $x266)))
  16.219 +(let ((@x331 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x260) $x275)) (unit-resolution @x274 @x206 $x260) $x275)))
  16.220 +(let (($x63 (>= ?x29 2)))
  16.221 +(let ((?x37 (* 2 ?x29)))
  16.222 +(let (($x56 (>= ?x37 3)))
  16.223 +(let (($x46 (< (+ x$ ?x37) (+ 3 x$))))
  16.224 +(let (($x49 (not $x46)))
  16.225 +(let ((@x58 (monotonicity (rewrite (= $x46 (not $x56))) (= $x49 (not (not $x56))))))
  16.226 +(let ((@x67 (trans (trans @x58 (rewrite (= (not (not $x56)) $x56)) (= $x49 $x56)) (rewrite (= $x56 $x63)) (= $x49 $x63))))
  16.227 +(let ((@x42 (monotonicity (rewrite (= (+ ?x29 ?x29) ?x37)) (= (+ x$ (+ ?x29 ?x29)) (+ x$ ?x37)))))
  16.228 +(let ((@x48 (monotonicity @x42 (rewrite (= (+ x$ 3) (+ 3 x$))) (= (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)) $x46))))
  16.229 +(let ((@x51 (monotonicity @x48 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x49))))
  16.230 +(let ((@x69 (trans @x51 @x67 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x63))))
  16.231 +(let ((@x70 (mp (asserted (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)))) @x69 $x63)))
  16.232 +((_ th-lemma arith farkas -1 1 1) @x70 @x331 (unit-resolution ((_ th-lemma arith) (or false $x319)) (true-axiom true) $x319) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  16.233 +
  16.234 +b6d44e20599d4862894eecfa4c98fcb043a6336d 348 0
  16.235 +unsat
  16.236 +((set-logic <null>)
  16.237 +(proof
  16.238 +(let ((?x96 (map$ uu$ xs$)))
  16.239 +(let ((?x97 (eval_dioph$ ks$ ?x96)))
  16.240 +(let ((?x424 (+ l$ ?x97)))
  16.241 +(let ((?x425 (mod ?x424 2)))
  16.242 +(let (($x482 (>= ?x425 2)))
  16.243 +(let (($x564 (not $x482)))
  16.244 +(let ((@x26 (true-axiom true)))
  16.245 +(let ((?x369 (* (- 1) l$)))
  16.246 +(let ((?x93 (eval_dioph$ ks$ xs$)))
  16.247 +(let ((?x678 (+ ?x93 ?x369)))
  16.248 +(let (($x679 (<= ?x678 0)))
  16.249 +(let (($x95 (= ?x93 l$)))
  16.250 +(let ((?x110 (* (- 1) ?x97)))
  16.251 +(let ((?x111 (+ l$ ?x110)))
  16.252 +(let ((?x114 (divide$ ?x111 2)))
  16.253 +(let ((?x101 (map$ uua$ xs$)))
  16.254 +(let ((?x102 (eval_dioph$ ks$ ?x101)))
  16.255 +(let (($x117 (= ?x102 ?x114)))
  16.256 +(let (($x282 (not $x117)))
  16.257 +(let ((?x99 (modulo$ l$ 2)))
  16.258 +(let ((?x98 (modulo$ ?x97 2)))
  16.259 +(let (($x100 (= ?x98 ?x99)))
  16.260 +(let (($x281 (not $x100)))
  16.261 +(let (($x283 (or $x281 $x282)))
  16.262 +(let (($x465 (>= ?x425 0)))
  16.263 +(let ((?x496 (* (- 2) ?x102)))
  16.264 +(let ((?x497 (+ ?x93 ?x110 ?x496)))
  16.265 +(let (($x504 (<= ?x497 0)))
  16.266 +(let (($x498 (= ?x497 0)))
  16.267 +(let (($x304 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1)))
  16.268 +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
  16.269 +(= ?x83 0))) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :pattern ( (eval_dioph$ ?v0 (map$ uua$ ?v1)) ) :qid k!19))
  16.270 +))
  16.271 +(let (($x85 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1)))
  16.272 +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
  16.273 +(= ?x83 0))) :qid k!19))
  16.274 +))
  16.275 +(let ((?x45 (eval_dioph$ ?1 ?0)))
  16.276 +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?1 (map$ uu$ ?0))) (* (- 2) (eval_dioph$ ?1 (map$ uua$ ?0))))))
  16.277 +(let (($x79 (= ?x83 0)))
  16.278 +(let (($x58 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1)))
  16.279 +(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
  16.280 +(let ((?x56 (+ (* (eval_dioph$ ?v0 (map$ uua$ ?v1)) 2) ?x48)))
  16.281 +(= ?x56 ?x45)))) :qid k!19))
  16.282 +))
  16.283 +(let (($x74 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1)))
  16.284 +(let ((?x54 (eval_dioph$ ?v0 (map$ uua$ ?v1))))
  16.285 +(let ((?x60 (* 2 ?x54)))
  16.286 +(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
  16.287 +(let ((?x66 (+ ?x48 ?x60)))
  16.288 +(= ?x66 ?x45)))))) :qid k!19))
  16.289 +))
  16.290 +(let ((?x54 (eval_dioph$ ?1 (map$ uua$ ?0))))
  16.291 +(let ((?x60 (* 2 ?x54)))
  16.292 +(let ((?x48 (eval_dioph$ ?1 (map$ uu$ ?0))))
  16.293 +(let ((?x66 (+ ?x48 ?x60)))
  16.294 +(let (($x71 (= ?x66 ?x45)))
  16.295 +(let ((@x65 (monotonicity (rewrite (= (* ?x54 2) ?x60)) (= (+ (* ?x54 2) ?x48) (+ ?x60 ?x48)))))
  16.296 +(let ((@x70 (trans @x65 (rewrite (= (+ ?x60 ?x48) ?x66)) (= (+ (* ?x54 2) ?x48) ?x66))))
  16.297 +(let ((@x76 (quant-intro (monotonicity @x70 (= (= (+ (* ?x54 2) ?x48) ?x45) $x71)) (= $x58 $x74))))
  16.298 +(let ((@x89 (trans @x76 (quant-intro (rewrite (= $x71 $x79)) (= $x74 $x85)) (= $x58 $x85))))
  16.299 +(let ((@x270 (mp~ (mp (asserted $x58) @x89 $x85) (nnf-pos (refl (~ $x79 $x79)) (~ $x85 $x85)) $x85)))
  16.300 +(let ((@x309 (mp @x270 (quant-intro (refl (= $x79 $x79)) (= $x85 $x304)) $x304)))
  16.301 +(let (($x502 (or (not $x304) $x498)))
  16.302 +(let ((@x503 ((_ quant-inst ks$ xs$) $x502)))
  16.303 +(let ((@x795 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x498) $x504)) (unit-resolution @x503 @x309 $x498) $x504)))
  16.304 +(let (($x815 (not $x679)))
  16.305 +(let (($x680 (>= ?x678 0)))
  16.306 +(let ((?x592 (mod ?x97 2)))
  16.307 +(let ((?x619 (* (- 1) ?x592)))
  16.308 +(let ((?x511 (mod l$ 2)))
  16.309 +(let ((?x538 (* (- 1) ?x511)))
  16.310 +(let ((?x776 (* (- 1) ?x102)))
  16.311 +(let ((?x759 (+ l$ ?x98 ?x776 ?x538 (* (- 1) (div l$ 2)) ?x619 (* (- 1) (div ?x97 2)))))
  16.312 +(let (($x760 (>= ?x759 1)))
  16.313 +(let (($x747 (not $x760)))
  16.314 +(let ((?x674 (* (- 1) ?x99)))
  16.315 +(let ((?x675 (+ ?x98 ?x674)))
  16.316 +(let (($x676 (<= ?x675 0)))
  16.317 +(let (($x284 (not $x283)))
  16.318 +(let ((@x493 (hypothesis $x284)))
  16.319 +(let ((@x781 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x281 $x676)) (unit-resolution (def-axiom (or $x283 $x100)) @x493 $x100) $x676)))
  16.320 +(let ((?x670 (* (- 1) ?x114)))
  16.321 +(let ((?x671 (+ ?x102 ?x670)))
  16.322 +(let (($x673 (>= ?x671 0)))
  16.323 +(let ((@x787 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x673)) (unit-resolution (def-axiom (or $x283 $x117)) @x493 $x117) $x673)))
  16.324 +(let ((?x557 (div l$ 2)))
  16.325 +(let ((?x570 (* (- 2) ?x557)))
  16.326 +(let ((?x571 (+ l$ ?x538 ?x570)))
  16.327 +(let (($x576 (<= ?x571 0)))
  16.328 +(let (($x569 (= ?x571 0)))
  16.329 +(let ((@x568 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x569) $x576)) (unit-resolution ((_ th-lemma arith) (or false $x569)) @x26 $x569) $x576)))
  16.330 +(let ((?x620 (+ ?x98 ?x619)))
  16.331 +(let (($x635 (<= ?x620 0)))
  16.332 +(let (($x621 (= ?x620 0)))
  16.333 +(let (($x318 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x200 (mod ?v0 ?v1)))
  16.334 +(let ((?x157 (* (- 1) ?v1)))
  16.335 +(let ((?x154 (* (- 1) ?v0)))
  16.336 +(let ((?x208 (mod ?x154 ?x157)))
  16.337 +(let ((?x214 (* (- 1) ?x208)))
  16.338 +(let (($x175 (<= ?v1 0)))
  16.339 +(let ((?x234 (ite $x175 ?x214 ?x200)))
  16.340 +(let (($x143 (= ?v1 0)))
  16.341 +(let ((?x239 (ite $x143 ?v0 ?x234)))
  16.342 +(let ((?x199 (modulo$ ?v0 ?v1)))
  16.343 +(= ?x199 ?x239))))))))))) :pattern ( (modulo$ ?v0 ?v1) ) :qid k!22))
  16.344 +))
  16.345 +(let (($x245 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x200 (mod ?v0 ?v1)))
  16.346 +(let ((?x157 (* (- 1) ?v1)))
  16.347 +(let ((?x154 (* (- 1) ?v0)))
  16.348 +(let ((?x208 (mod ?x154 ?x157)))
  16.349 +(let ((?x214 (* (- 1) ?x208)))
  16.350 +(let (($x175 (<= ?v1 0)))
  16.351 +(let ((?x234 (ite $x175 ?x214 ?x200)))
  16.352 +(let (($x143 (= ?v1 0)))
  16.353 +(let ((?x239 (ite $x143 ?v0 ?x234)))
  16.354 +(let ((?x199 (modulo$ ?v0 ?v1)))
  16.355 +(= ?x199 ?x239))))))))))) :qid k!22))
  16.356 +))
  16.357 +(let ((?x200 (mod ?1 ?0)))
  16.358 +(let ((?x157 (* (- 1) ?0)))
  16.359 +(let ((?x154 (* (- 1) ?1)))
  16.360 +(let ((?x208 (mod ?x154 ?x157)))
  16.361 +(let ((?x214 (* (- 1) ?x208)))
  16.362 +(let (($x175 (<= ?0 0)))
  16.363 +(let ((?x234 (ite $x175 ?x214 ?x200)))
  16.364 +(let (($x143 (= ?0 0)))
  16.365 +(let ((?x239 (ite $x143 ?1 ?x234)))
  16.366 +(let ((?x199 (modulo$ ?1 ?0)))
  16.367 +(let (($x242 (= ?x199 ?x239)))
  16.368 +(let (($x206 (forall ((?v0 Int) (?v1 Int) )(! (let (($x143 (= ?v1 0)))
  16.369 +(let ((?x204 (ite $x143 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
  16.370 +(let ((?x199 (modulo$ ?v0 ?v1)))
  16.371 +(= ?x199 ?x204)))) :qid k!22))
  16.372 +))
  16.373 +(let (($x228 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x157 (* (- 1) ?v1)))
  16.374 +(let ((?x154 (* (- 1) ?v0)))
  16.375 +(let ((?x208 (mod ?x154 ?x157)))
  16.376 +(let ((?x214 (* (- 1) ?x208)))
  16.377 +(let ((?x200 (mod ?v0 ?v1)))
  16.378 +(let (($x144 (< 0 ?v1)))
  16.379 +(let ((?x219 (ite $x144 ?x200 ?x214)))
  16.380 +(let (($x143 (= ?v1 0)))
  16.381 +(let ((?x222 (ite $x143 ?v0 ?x219)))
  16.382 +(let ((?x199 (modulo$ ?v0 ?v1)))
  16.383 +(= ?x199 ?x222))))))))))) :qid k!22))
  16.384 +))
  16.385 +(let ((@x233 (monotonicity (rewrite (= (< 0 ?0) (not $x175))) (= (ite (< 0 ?0) ?x200 ?x214) (ite (not $x175) ?x200 ?x214)))))
  16.386 +(let ((@x238 (trans @x233 (rewrite (= (ite (not $x175) ?x200 ?x214) ?x234)) (= (ite (< 0 ?0) ?x200 ?x214) ?x234))))
  16.387 +(let ((@x241 (monotonicity @x238 (= (ite $x143 ?1 (ite (< 0 ?0) ?x200 ?x214)) ?x239))))
  16.388 +(let ((@x244 (monotonicity @x241 (= (= ?x199 (ite $x143 ?1 (ite (< 0 ?0) ?x200 ?x214))) $x242))))
  16.389 +(let (($x144 (< 0 ?0)))
  16.390 +(let ((?x219 (ite $x144 ?x200 ?x214)))
  16.391 +(let ((?x222 (ite $x143 ?1 ?x219)))
  16.392 +(let (($x225 (= ?x199 ?x222)))
  16.393 +(let (($x226 (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))))) $x225)))
  16.394 +(let ((@x210 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (mod (- ?1) (- ?0)) ?x208))))
  16.395 +(let ((@x218 (trans (monotonicity @x210 (= (- (mod (- ?1) (- ?0))) (- ?x208))) (rewrite (= (- ?x208) ?x214)) (= (- (mod (- ?1) (- ?0))) ?x214))))
  16.396 +(let ((@x221 (monotonicity @x218 (= (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))) ?x219))))
  16.397 +(let ((@x224 (monotonicity @x221 (= (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0))))) ?x222))))
  16.398 +(let ((@x249 (trans (quant-intro (monotonicity @x224 $x226) (= $x206 $x228)) (quant-intro @x244 (= $x228 $x245)) (= $x206 $x245))))
  16.399 +(let ((@x280 (mp~ (mp (asserted $x206) @x249 $x245) (nnf-pos (refl (~ $x242 $x242)) (~ $x245 $x245)) $x245)))
  16.400 +(let ((@x323 (mp @x280 (quant-intro (refl (= $x242 $x242)) (= $x245 $x318)) $x318)))
  16.401 +(let (($x545 (not $x318)))
  16.402 +(let (($x626 (or $x545 $x621)))
  16.403 +(let ((?x359 (* (- 1) 2)))
  16.404 +(let ((?x590 (mod ?x110 ?x359)))
  16.405 +(let ((?x591 (* (- 1) ?x590)))
  16.406 +(let (($x357 (<= 2 0)))
  16.407 +(let ((?x593 (ite $x357 ?x591 ?x592)))
  16.408 +(let (($x356 (= 2 0)))
  16.409 +(let ((?x594 (ite $x356 ?x97 ?x593)))
  16.410 +(let (($x595 (= ?x98 ?x594)))
  16.411 +(let ((@x601 (monotonicity (monotonicity (rewrite (= ?x359 (- 2))) (= ?x590 (mod ?x110 (- 2)))) (= ?x591 (* (- 1) (mod ?x110 (- 2)))))))
  16.412 +(let ((@x368 (rewrite (= $x357 false))))
  16.413 +(let ((@x604 (monotonicity @x368 @x601 (= ?x593 (ite false (* (- 1) (mod ?x110 (- 2))) ?x592)))))
  16.414 +(let ((@x608 (trans @x604 (rewrite (= (ite false (* (- 1) (mod ?x110 (- 2))) ?x592) ?x592)) (= ?x593 ?x592))))
  16.415 +(let ((@x366 (rewrite (= $x356 false))))
  16.416 +(let ((@x615 (trans (monotonicity @x366 @x608 (= ?x594 (ite false ?x97 ?x592))) (rewrite (= (ite false ?x97 ?x592) ?x592)) (= ?x594 ?x592))))
  16.417 +(let ((@x625 (trans (monotonicity @x615 (= $x595 (= ?x98 ?x592))) (rewrite (= (= ?x98 ?x592) $x621)) (= $x595 $x621))))
  16.418 +(let ((@x633 (trans (monotonicity @x625 (= (or $x545 $x595) $x626)) (rewrite (= $x626 $x626)) (= (or $x545 $x595) $x626))))
  16.419 +(let ((@x634 (mp ((_ quant-inst (eval_dioph$ ks$ ?x96) 2) (or $x545 $x595)) @x633 $x626)))
  16.420 +(let ((@x431 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x621) $x635)) (unit-resolution @x634 @x323 $x621) $x635)))
  16.421 +(let ((?x637 (div ?x97 2)))
  16.422 +(let ((?x650 (* (- 2) ?x637)))
  16.423 +(let ((?x651 (+ ?x97 ?x619 ?x650)))
  16.424 +(let (($x656 (<= ?x651 0)))
  16.425 +(let (($x649 (= ?x651 0)))
  16.426 +(let ((@x661 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x649) $x656)) (unit-resolution ((_ th-lemma arith) (or false $x649)) @x26 $x649) $x656)))
  16.427 +(let ((?x539 (+ ?x99 ?x538)))
  16.428 +(let (($x555 (<= ?x539 0)))
  16.429 +(let (($x540 (= ?x539 0)))
  16.430 +(let (($x546 (or $x545 $x540)))
  16.431 +(let ((?x506 (mod ?x369 ?x359)))
  16.432 +(let ((?x507 (* (- 1) ?x506)))
  16.433 +(let ((?x512 (ite $x357 ?x507 ?x511)))
  16.434 +(let ((?x513 (ite $x356 l$ ?x512)))
  16.435 +(let (($x514 (= ?x99 ?x513)))
  16.436 +(let ((@x520 (monotonicity (monotonicity (rewrite (= ?x359 (- 2))) (= ?x506 (mod ?x369 (- 2)))) (= ?x507 (* (- 1) (mod ?x369 (- 2)))))))
  16.437 +(let ((@x523 (monotonicity @x368 @x520 (= ?x512 (ite false (* (- 1) (mod ?x369 (- 2))) ?x511)))))
  16.438 +(let ((@x527 (trans @x523 (rewrite (= (ite false (* (- 1) (mod ?x369 (- 2))) ?x511) ?x511)) (= ?x512 ?x511))))
  16.439 +(let ((@x534 (trans (monotonicity @x366 @x527 (= ?x513 (ite false l$ ?x511))) (rewrite (= (ite false l$ ?x511) ?x511)) (= ?x513 ?x511))))
  16.440 +(let ((@x544 (trans (monotonicity @x534 (= $x514 (= ?x99 ?x511))) (rewrite (= (= ?x99 ?x511) $x540)) (= $x514 $x540))))
  16.441 +(let ((@x553 (trans (monotonicity @x544 (= (or $x545 $x514) $x546)) (rewrite (= $x546 $x546)) (= (or $x545 $x514) $x546))))
  16.442 +(let ((@x554 (mp ((_ quant-inst l$ 2) (or $x545 $x514)) @x553 $x546)))
  16.443 +(let ((@x668 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x540) $x555)) (unit-resolution @x554 @x323 $x540) $x555)))
  16.444 +(let ((?x361 (div ?x111 2)))
  16.445 +(let ((?x395 (* (- 1) ?x361)))
  16.446 +(let ((?x396 (+ ?x114 ?x395)))
  16.447 +(let (($x414 (>= ?x396 0)))
  16.448 +(let (($x397 (= ?x396 0)))
  16.449 +(let (($x311 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x145 (div ?v0 ?v1)))
  16.450 +(let ((?x157 (* (- 1) ?v1)))
  16.451 +(let ((?x154 (* (- 1) ?v0)))
  16.452 +(let ((?x160 (div ?x154 ?x157)))
  16.453 +(let (($x175 (<= ?v1 0)))
  16.454 +(let ((?x182 (ite $x175 ?x160 ?x145)))
  16.455 +(let (($x143 (= ?v1 0)))
  16.456 +(let ((?x141 (divide$ ?v0 ?v1)))
  16.457 +(= ?x141 (ite $x143 0 ?x182)))))))))) :pattern ( (divide$ ?v0 ?v1) ) :qid k!21))
  16.458 +))
  16.459 +(let (($x193 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x145 (div ?v0 ?v1)))
  16.460 +(let ((?x157 (* (- 1) ?v1)))
  16.461 +(let ((?x154 (* (- 1) ?v0)))
  16.462 +(let ((?x160 (div ?x154 ?x157)))
  16.463 +(let (($x175 (<= ?v1 0)))
  16.464 +(let ((?x182 (ite $x175 ?x160 ?x145)))
  16.465 +(let (($x143 (= ?v1 0)))
  16.466 +(let ((?x141 (divide$ ?v0 ?v1)))
  16.467 +(= ?x141 (ite $x143 0 ?x182)))))))))) :qid k!21))
  16.468 +))
  16.469 +(let ((?x141 (divide$ ?1 ?0)))
  16.470 +(let (($x190 (= ?x141 (ite $x143 0 (ite $x175 (div ?x154 ?x157) (div ?1 ?0))))))
  16.471 +(let (($x152 (forall ((?v0 Int) (?v1 Int) )(! (let (($x143 (= ?v1 0)))
  16.472 +(let ((?x150 (ite $x143 0 (ite (< 0 ?v1) (div ?v0 ?v1) (div (- ?v0) (- ?v1))))))
  16.473 +(let ((?x141 (divide$ ?v0 ?v1)))
  16.474 +(= ?x141 ?x150)))) :qid k!21))
  16.475 +))
  16.476 +(let (($x172 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x157 (* (- 1) ?v1)))
  16.477 +(let ((?x154 (* (- 1) ?v0)))
  16.478 +(let ((?x160 (div ?x154 ?x157)))
  16.479 +(let ((?x145 (div ?v0 ?v1)))
  16.480 +(let (($x144 (< 0 ?v1)))
  16.481 +(let ((?x163 (ite $x144 ?x145 ?x160)))
  16.482 +(let (($x143 (= ?v1 0)))
  16.483 +(let ((?x166 (ite $x143 0 ?x163)))
  16.484 +(let ((?x141 (divide$ ?v0 ?v1)))
  16.485 +(= ?x141 ?x166)))))))))) :qid k!21))
  16.486 +))
  16.487 +(let ((?x160 (div ?x154 ?x157)))
  16.488 +(let ((?x145 (div ?1 ?0)))
  16.489 +(let ((?x163 (ite $x144 ?x145 ?x160)))
  16.490 +(let ((?x166 (ite $x143 0 ?x163)))
  16.491 +(let (($x169 (= ?x141 ?x166)))
  16.492 +(let ((@x181 (monotonicity (rewrite (= $x144 (not $x175))) (= ?x163 (ite (not $x175) ?x145 ?x160)))))
  16.493 +(let ((@x186 (trans @x181 (rewrite (= (ite (not $x175) ?x145 ?x160) (ite $x175 ?x160 ?x145))) (= ?x163 (ite $x175 ?x160 ?x145)))))
  16.494 +(let ((@x192 (monotonicity (monotonicity @x186 (= ?x166 (ite $x143 0 (ite $x175 ?x160 ?x145)))) (= $x169 $x190))))
  16.495 +(let (($x170 (= (= ?x141 (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0))))) $x169)))
  16.496 +(let ((@x162 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (div (- ?1) (- ?0)) ?x160))))
  16.497 +(let ((@x168 (monotonicity (monotonicity @x162 (= (ite $x144 ?x145 (div (- ?1) (- ?0))) ?x163)) (= (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0)))) ?x166))))
  16.498 +(let ((@x197 (trans (quant-intro (monotonicity @x168 $x170) (= $x152 $x172)) (quant-intro @x192 (= $x172 $x193)) (= $x152 $x193))))
  16.499 +(let ((@x275 (mp~ (mp (asserted $x152) @x197 $x193) (nnf-pos (refl (~ $x190 $x190)) (~ $x193 $x193)) $x193)))
  16.500 +(let ((@x316 (mp @x275 (quant-intro (refl (= $x190 $x190)) (= $x193 $x311)) $x311)))
  16.501 +(let (($x403 (or (not $x311) $x397)))
  16.502 +(let ((?x358 (* (- 1) ?x111)))
  16.503 +(let ((?x360 (div ?x358 ?x359)))
  16.504 +(let ((?x362 (ite $x357 ?x360 ?x361)))
  16.505 +(let ((?x363 (ite $x356 0 ?x362)))
  16.506 +(let (($x364 (= ?x114 ?x363)))
  16.507 +(let ((@x374 (rewrite (= ?x359 (- 2)))))
  16.508 +(let ((@x377 (monotonicity (rewrite (= ?x358 (+ ?x369 ?x97))) @x374 (= ?x360 (div (+ ?x369 ?x97) (- 2))))))
  16.509 +(let ((@x380 (monotonicity @x368 @x377 (= ?x362 (ite false (div (+ ?x369 ?x97) (- 2)) ?x361)))))
  16.510 +(let ((@x384 (trans @x380 (rewrite (= (ite false (div (+ ?x369 ?x97) (- 2)) ?x361) ?x361)) (= ?x362 ?x361))))
  16.511 +(let ((@x391 (trans (monotonicity @x366 @x384 (= ?x363 (ite false 0 ?x361))) (rewrite (= (ite false 0 ?x361) ?x361)) (= ?x363 ?x361))))
  16.512 +(let ((@x401 (trans (monotonicity @x391 (= $x364 (= ?x114 ?x361))) (rewrite (= (= ?x114 ?x361) $x397)) (= $x364 $x397))))
  16.513 +(let ((@x410 (trans (monotonicity @x401 (= (or (not $x311) $x364) $x403)) (rewrite (= $x403 $x403)) (= (or (not $x311) $x364) $x403))))
  16.514 +(let ((@x411 (mp ((_ quant-inst (+ l$ ?x110) 2) (or (not $x311) $x364)) @x410 $x403)))
  16.515 +(let ((@x485 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x414)) (unit-resolution @x411 @x316 $x397) $x414)))
  16.516 +(let ((?x436 (* (- 1) ?x425)))
  16.517 +(let ((?x435 (* (- 2) ?x361)))
  16.518 +(let ((?x437 (+ l$ ?x110 ?x435 ?x436)))
  16.519 +(let (($x442 (<= ?x437 0)))
  16.520 +(let (($x434 (= ?x437 0)))
  16.521 +(let ((@x745 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x442)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x442)))
  16.522 +(let ((@x746 ((_ th-lemma arith farkas 1 -2 -2 -2 1 1 1 1 1 1) @x745 @x485 (hypothesis $x673) (hypothesis $x760) (hypothesis $x676) @x668 @x661 @x431 @x568 (unit-resolution ((_ th-lemma arith) (or false $x564)) @x26 $x564) false)))
  16.523 +(let ((@x788 (unit-resolution (lemma @x746 (or $x747 (not $x673) (not $x676))) @x787 @x781 $x747)))
  16.524 +(let (($x677 (>= ?x675 0)))
  16.525 +(let ((@x812 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x281 $x677)) (unit-resolution (def-axiom (or $x283 $x100)) @x493 $x100) $x677)))
  16.526 +(let (($x577 (>= ?x571 0)))
  16.527 +(let ((@x778 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x569) $x577)) (unit-resolution ((_ th-lemma arith) (or false $x569)) @x26 $x569) $x577)))
  16.528 +(let (($x556 (>= ?x539 0)))
  16.529 +(let ((@x645 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x540) $x556)) (unit-resolution @x554 @x323 $x540) $x556)))
  16.530 +(let (($x636 (>= ?x620 0)))
  16.531 +(let ((@x652 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x621) $x636)) (unit-resolution @x634 @x323 $x621) $x636)))
  16.532 +(let (($x505 (>= ?x497 0)))
  16.533 +(let ((@x488 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x498) $x505)) (unit-resolution @x503 @x309 $x498) $x505)))
  16.534 +(let (($x657 (>= ?x651 0)))
  16.535 +(let ((@x581 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x649) $x657)) (unit-resolution ((_ th-lemma arith) (or false $x649)) @x26 $x649) $x657)))
  16.536 +(let ((@x582 ((_ th-lemma arith farkas -1/2 -1/2 -1/2 1/2 -1/2 -1/2 -1/2 1) @x581 (hypothesis $x677) @x488 (hypothesis (not $x680)) @x652 @x645 @x778 (hypothesis $x747) false)))
  16.537 +(let ((@x813 (unit-resolution (lemma @x582 (or $x680 (not $x677) $x760)) @x812 @x788 $x680)))
  16.538 +(let (($x134 (not $x95)))
  16.539 +(let (($x290 (= $x95 $x283)))
  16.540 +(let ((@x289 (monotonicity (rewrite (= (and $x100 $x117) $x284)) (= (= $x134 (and $x100 $x117)) (= $x134 $x284)))))
  16.541 +(let ((@x294 (trans @x289 (rewrite (= (= $x134 $x284) $x290)) (= (= $x134 (and $x100 $x117)) $x290))))
  16.542 +(let (($x120 (and $x100 $x117)))
  16.543 +(let (($x135 (= $x134 $x120)))
  16.544 +(let (($x107 (= $x95 (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))))))
  16.545 +(let (($x108 (not $x107)))
  16.546 +(let ((@x116 (monotonicity (rewrite (= (- l$ ?x97) ?x111)) (= (divide$ (- l$ ?x97) 2) ?x114))))
  16.547 +(let ((@x122 (monotonicity (monotonicity @x116 (= (= ?x102 (divide$ (- l$ ?x97) 2)) $x117)) (= (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))) $x120))))
  16.548 +(let ((@x130 (trans (monotonicity @x122 (= $x107 (= $x95 $x120))) (rewrite (= (= $x95 $x120) (= $x95 $x120))) (= $x107 (= $x95 $x120)))))
  16.549 +(let ((@x139 (trans (monotonicity @x130 (= $x108 (not (= $x95 $x120)))) (rewrite (= (not (= $x95 $x120)) $x135)) (= $x108 $x135))))
  16.550 +(let ((@x295 (mp (mp (asserted $x108) @x139 $x135) @x294 $x290)))
  16.551 +(let ((@x344 (unit-resolution (def-axiom (or $x134 $x283 (not $x290))) @x295 (or $x134 $x283))))
  16.552 +(let ((@x819 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x95 $x815 (not $x680))) (unit-resolution @x344 @x493 $x134) (or $x815 (not $x680)))))
  16.553 +(let (($x672 (<= ?x671 0)))
  16.554 +(let ((@x823 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x672)) (unit-resolution (def-axiom (or $x283 $x117)) @x493 $x117) $x672)))
  16.555 +(let (($x413 (<= ?x396 0)))
  16.556 +(let ((@x802 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) (unit-resolution @x411 @x316 $x397) $x413)))
  16.557 +(let (($x443 (>= ?x437 0)))
  16.558 +(let ((@x826 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x443)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x443)))
  16.559 +(let ((@x827 ((_ th-lemma arith farkas 1 -2 -2 1 -1 1) @x826 @x802 @x823 (unit-resolution @x819 @x813 $x815) @x795 (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) false)))
  16.560 +(let ((@x828 (lemma @x827 $x283)))
  16.561 +(let ((@x340 (unit-resolution (def-axiom (or $x95 $x284 (not $x290))) @x295 (or $x95 $x284))))
  16.562 +(let ((@x584 (unit-resolution @x340 @x828 $x95)))
  16.563 +(let (($x807 (not $x672)))
  16.564 +(let ((@x888 ((_ th-lemma arith assign-bounds 1 -1/2 -1/2 1/2 -1/2) (or $x673 (not $x413) (not $x465) (not $x443) (not $x504) (not $x680)))))
  16.565 +(let ((@x889 (unit-resolution @x888 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x680)) @x584 $x680) @x802 @x826 (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) @x795 $x673)))
  16.566 +(let ((@x728 (monotonicity (symm @x584 (= l$ ?x93)) (= ?x99 (modulo$ ?x93 2)))))
  16.567 +(let ((?x499 (modulo$ ?x93 2)))
  16.568 +(let (($x500 (= ?x499 ?x98)))
  16.569 +(let (($x297 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (= (modulo$ (eval_dioph$ ?v0 ?v1) 2) (modulo$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :qid k!18))
  16.570 +))
  16.571 +(let (($x51 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (= (modulo$ (eval_dioph$ ?v0 ?v1) 2) (modulo$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :qid k!18))
  16.572 +))
  16.573 +(let (($x50 (= (modulo$ ?x45 2) (modulo$ ?x48 2))))
  16.574 +(let ((@x265 (mp~ (asserted $x51) (nnf-pos (refl (~ $x50 $x50)) (~ $x51 $x51)) $x51)))
  16.575 +(let ((@x302 (mp @x265 (quant-intro (refl (= $x50 $x50)) (= $x51 $x297)) $x297)))
  16.576 +(let (($x464 (or (not $x297) $x500)))
  16.577 +(let ((@x578 ((_ quant-inst ks$ xs$) $x464)))
  16.578 +(let ((@x748 (trans (symm (unit-resolution @x578 @x302 $x500) (= ?x98 ?x499)) (symm @x728 (= ?x499 ?x99)) $x100)))
  16.579 +(let ((@x891 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x828 $x283) (lemma (unit-resolution (hypothesis $x281) @x748 false) $x100) $x282)))
  16.580 +(let ((@x895 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x807 (not $x673))) @x891 (or $x807 (not $x673)))))
  16.581 +((_ th-lemma arith farkas -2 -2 1 -1 1 1) (unit-resolution @x895 @x889 $x807) @x485 @x745 @x488 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x679)) @x584 $x679) (unit-resolution ((_ th-lemma arith) (or false $x564)) @x26 $x564) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  16.582 +
    17.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Sep 26 07:56:54 2016 +0200
    17.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Sep 26 07:56:54 2016 +0200
    17.3 @@ -441,7 +441,7 @@
    17.4        | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv}
    17.5            (fst (tm_of vs e), fst (tm_of vs e')), integerN)
    17.6  
    17.7 -      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name mod}
    17.8 +      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name modulo}
    17.9            (fst (tm_of vs e), fst (tm_of vs e')), integerN)
   17.10  
   17.11        | tm_of vs (Funct ("-", [e])) =
    18.1 --- a/src/HOL/String.thy	Mon Sep 26 07:56:54 2016 +0200
    18.2 +++ b/src/HOL/String.thy	Mon Sep 26 07:56:54 2016 +0200
    18.3 @@ -147,7 +147,7 @@
    18.4  lemma integer_of_char_Char [simp]:
    18.5    "integer_of_char (Char k) = numeral k mod 256"
    18.6    by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
    18.7 -    id_apply zmod_int mod_integer.abs_eq [symmetric]) simp
    18.8 +    id_apply zmod_int modulo_integer.abs_eq [symmetric]) simp
    18.9  
   18.10  lemma less_256_integer_of_char_Char:
   18.11    assumes "numeral k < (256 :: integer)"
    19.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Sep 26 07:56:54 2016 +0200
    19.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Sep 26 07:56:54 2016 +0200
    19.3 @@ -757,7 +757,7 @@
    19.4   | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r
    19.5   | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
    19.6   | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
    19.7 - | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
    19.8 + | Const(@{const_name Rings.modulo},_)$l$r => isnum l andalso isnum r
    19.9   | Const(@{const_name Rings.divide},_)$l$r => isnum l andalso isnum r
   19.10   | _ => is_number t orelse can HOLogic.dest_nat t
   19.11  
    20.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Mon Sep 26 07:56:54 2016 +0200
    20.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Mon Sep 26 07:56:54 2016 +0200
    20.3 @@ -35,7 +35,7 @@
    20.4       serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
    20.5  
    20.6    fun is_div_mod @{const divide (int)} = true
    20.7 -    | is_div_mod @{const mod (int)} = true
    20.8 +    | is_div_mod @{const modulo (int)} = true
    20.9      | is_div_mod _ = false
   20.10  
   20.11    val have_int_div_mod = exists (Term.exists_subterm is_div_mod o Thm.prop_of)
    21.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Sep 26 07:56:54 2016 +0200
    21.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Sep 26 07:56:54 2016 +0200
    21.3 @@ -299,7 +299,7 @@
    21.4            @{const_name Groups.abs},
    21.5            @{const_name Groups.minus},
    21.6            "Int.nat" (*DYNAMIC BINDING!*),
    21.7 -          "Divides.div_class.mod" (*DYNAMIC BINDING!*),
    21.8 +          @{const_name Rings.modulo},
    21.9            @{const_name Rings.divide}] a
   21.10      | _ =>
   21.11        (if Context_Position.is_visible ctxt then
   21.12 @@ -467,7 +467,7 @@
   21.13      (* ?P ((?n::nat) mod (numeral ?k)) =
   21.14           ((numeral ?k = 0 --> ?P ?n) & (~ (numeral ?k = 0) -->
   21.15             (ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P j))) *)
   21.16 -    | (Const ("Divides.div_class.mod", Type ("fun", [@{typ nat}, _])), (*DYNAMIC BINDING!*) [t1, t2]) =>
   21.17 +    | (Const (@{const_name Rings.modulo}, Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
   21.18        let
   21.19          val rev_terms               = rev terms
   21.20          val zero                    = Const (@{const_name Groups.zero}, split_type)
   21.21 @@ -536,7 +536,7 @@
   21.22            (numeral ?k < 0 -->
   21.23              (ALL i j.
   21.24                numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P j))) *)
   21.25 -    | (Const ("Divides.div_class.mod",
   21.26 +    | (Const (@{const_name Rings.modulo},
   21.27          Type ("fun", [Type ("Int.int", []), _])), (*DYNAMIC BINDING!*) [t1, t2]) =>
   21.28        let
   21.29          val rev_terms               = rev terms
    22.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Mon Sep 26 07:56:54 2016 +0200
    22.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Sep 26 07:56:54 2016 +0200
    22.3 @@ -551,8 +551,8 @@
    22.4  
    22.5  structure ModCancelFactor = ExtractCommonTermFun
    22.6   (open CancelFactorCommon
    22.7 -  val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
    22.8 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} dummyT
    22.9 +  val mk_bal   = HOLogic.mk_binop @{const_name modulo}
   22.10 +  val dest_bal = HOLogic.dest_bin @{const_name modulo} dummyT
   22.11    fun simp_conv _ _ = SOME @{thm mod_mult_mult1}
   22.12  );
   22.13  
    23.1 --- a/src/HOL/Word/Word.thy	Mon Sep 26 07:56:54 2016 +0200
    23.2 +++ b/src/HOL/Word/Word.thy	Mon Sep 26 07:56:54 2016 +0200
    23.3 @@ -287,7 +287,7 @@
    23.4  lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x - 1"
    23.5    by (metis bintr_ariths(7))
    23.6  
    23.7 -instantiation word :: (len0) "{neg_numeral, Divides.div, comm_monoid_mult, comm_ring}"
    23.8 +instantiation word :: (len0) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}"
    23.9  begin
   23.10  
   23.11  lift_definition zero_word :: "'a word" is "0" .
    24.1 --- a/src/HOL/ex/Arith_Examples.thy	Mon Sep 26 07:56:54 2016 +0200
    24.2 +++ b/src/HOL/ex/Arith_Examples.thy	Mon Sep 26 07:56:54 2016 +0200
    24.3 @@ -30,7 +30,7 @@
    24.4  
    24.5  
    24.6  subsection \<open>Splitting of Operators: @{term max}, @{term min}, @{term abs},
    24.7 -           @{term minus}, @{term nat}, @{term Divides.mod},
    24.8 +           @{term minus}, @{term nat}, @{term modulo},
    24.9             @{term divide}\<close>
   24.10  
   24.11  lemma "(i::nat) <= max i j"