Simplifier doesn't work with constants greater than 10?

Question 1

To answer for the workaround, you can use the "arith" or the "presburger" method:

lemma "n ≠ counter ⟹
  n ≠ Suc counter ⟹
  n ≠ Suc (Suc counter) ⟹
  n ≠ counter + 3 ⟹
  n ≠ counter + 4 ⟹
  n ≠ counter + 5 ⟹
  n ≠ counter + 6 ⟹
  n ≠ counter + 7 ⟹
  n ≠ counter + 8 ⟹ 
  n ≠ counter + 9 ⟹ 
  counter ≤ n ⟹ n < counter + 10 ⟹ False"
  by presburger (* or by arith *)

arith also works but raises a warning (linarith failed) in this case, while this warning does not appear for the smaller lemma. There should be a correlation somewhere but I don't know exactly why the simp method fails though...

You could have discovered this by using the commands "try" or "try0" that try several provers and methods.

Question 2

Thanks for the other answer for showing that arith can be used to prove the theorem, because arith is not one of the try0 methods.

By all appearances, this message from linarith_trace gives you the answer:

neq_limit exceeded (current value is 9), ignoring all inequalities

The value 10 comes into play not because you're using the constant 10, but because you're using 10 inequalities, as I show below. As usual, because I can't verify with someone what seems to be obvious (from looking at source files), I could be wrong.

I grepped on neq_limit in Isabelle2013-2/src and it shows up in two files. There's also an applicable example theory:

Below, I quote from the files above, and I show, using [[simp_trace, linarith_trace]], whether I use apply(simp only:) or apply(arith), there's a lot of interaction between simp and various linear arithmetic methods.

I deleted my first answer. If anyone wants to see what I had to say about (simp only:), and other things about trying to track down things, you can click on edit somewhere below to see the old entries.

As shown below, whether I use apply(simp only:) or apply(arith), I get the neq_limit exceeded trace message above.

I speculate that the difference is between fast_lin_arith.ML and lin_arith.ML. In fast_lin_arith.ML, there is a check, at line 788, that's not in lin_arith.ML.

  val split_neq = count is_neq (map (LA_Data.decomp ctxt) Hs') <= neq_limit
in
  if split_neq then ()
  else
    trace_msg ctxt ("neq_limit exceeded (current value is " ^

This is related to a comment in that file:

(*the limit on the number of ~= allowed; because each ~= is split
  into two cases, this can lead to an explosion*)
val neq_limit: int Config.T

In general, there's a lot of interaction between simp and the linear arithmetic automatic proof methods, as shown by a comment in Arith_Examples.thy.

The @{text arith} method combines them both, and tries other methods 
(e.g.~@{text presburger}) as well.  This is the one that you should use 
in your proofs!

Now, I get rid of one not equal in your counter + 10 lemma (because it's redundant), which allows simp to prove it.

(*_SRC.0_*)    
(*If we get rid of one inequality, and change the <= to <, it works.*)
lemma "(*n ≠ counter ==> *)
       counter < n ==> 
       n ≠ Suc counter ==>
       n ≠ Suc (Suc counter) ==>
       n ≠ counter + 3 ==>
       n ≠ counter + 4 ==>
       n ≠ counter + 5 ==>
       n ≠ counter + 6 ==>
       n ≠ counter + 7 ==>
       n ≠ counter + 8 ==> 
       n ≠ counter + 9 ==>
       n < counter + 10 ==> False"
by(simp)

I show here that there's interaction between simp and a linear arithmetic tactic. (The comment in Arith_Examples.thy explains there are variations.)

(*_SRC.1_*)
lemma "
  n ≠ counter ==>
  n ≠ Suc counter ==>
  n ≠ Suc (Suc counter) ==>
  counter ≤ n ==> 
  n < counter + 3 ==> False"
  using[[simp_trace, linarith_trace]] 
(*Click "1000" at the bottom of the output panel to get it to finish.

  The trace shows that `arith` is called very soon, but that there's also
  a lot of simp rule rewriting, such as with the rule `Groups.add_ac_2`.*)
apply(simp only:)
done

I show that you get the same trace message about neq_limit with both apply(simp only:) and apply(arith), but one proof goes through, and one doesn't. Apparently, simp uses one form of a linear arithmetic tactic, and arith uses another.

(*_SRC.2_*)    
lemma "n ≠ counter ==>
       n ≠ Suc counter ==>
       n ≠ Suc (Suc counter) ==>
       n ≠ counter + 3 ==>
       n ≠ counter + 4 ==>
       n ≠ counter + 5 ==>
       n ≠ counter + 6 ==>
       n ≠ counter + 7 ==>
       n ≠ counter + 8 ==> 
       n ≠ counter + 9 ==> 
       counter ≤ n ==> 
       n < counter + 10 ==> False"
  using[[linarith_trace]]
  apply(simp only:)
(*Gets the following error message, and it goes no further:

  Trying to refute subgoal 1...
  neq_limit exceeded (current value is 9), ignoring all inequalities 
*)
oops

(*_SRC.3_*)    
lemma "n ≠ counter ==>
       n ≠ Suc counter ==>
       n ≠ Suc (Suc counter) ==>
       n ≠ counter + 3 ==>
       n ≠ counter + 4 ==>
       n ≠ counter + 5 ==>
       n ≠ counter + 6 ==>
       n ≠ counter + 7 ==>
       n ≠ counter + 8 ==> 
       n ≠ counter + 9 ==> 
       counter ≤ n ==> 
       n < counter + 10 ==> False"
  using[[simp_trace, linarith_trace]]
  apply(arith)
(*Same complaint about "9", but the proof will go through if there's no trace:

  Trying to refute subgoal 1...
  neq_limit exceeded (current value is 9), ignoring all inequalities 
*)
oops