# Re: [isabelle] need help with quantified ints

Firstly, you can use (case_tac n) instead of (cases n) to do more or less exactly the same thing, except that n can be a qyantified variable. This follows a pattern in isabelle, with induct_tac, rule_tac, drule_tac etc allowing in various ways the specification of a constant that only exists within the context of the rule.
```
```
Something to think about for your particular case - you're working with an assumption that a variable is less than a constant, in this case n <= 12. There's a trick for getting all the cases at once. Oddly, I don't seem to be able to get it working for <= thisevening, but consider the trick for
```n < 12:

lemma n_less_val_disj:
"m ~= (0 :: nat) ==>
(n < m) = (n = m - 1 | n < m - 1)"
apply (case_tac n, simp_all)
apply fastsimp
apply (case_tac m, simp_all)
apply fastsimp
done

lemma test_this:
"n < (12 :: nat) ==> P"
oops

```
The reduction to cases can more or less take care of itself. I'm sure there's a nice way to do this for int n <= 12, but I'll leave you to figure out what it might be.
```
Yours,
Thomas.

On Thu, 19 Jun 2008, Perry James wrote:

```
```Hi,
I'm having trouble proving the lemma below.  My first idea was to "apply
(cases n)" since there are only 12 values of n that satisfy the assumption,
but that's not possible since n is bound. Also, applying arith, algebra, and
auto have no effect.
Is there any way to make progress?
```