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:
"m ~= (0 :: nat) ==>
(n < m) = (n = m - 1 | n < m - 1)"
apply (case_tac n, simp_all)
apply (case_tac m, simp_all)
"n < (12 :: nat) ==> P"
apply (simp add: n_less_val_disj)
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.
On Thu, 19 Jun 2008, Perry James wrote:
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?
Thanks in advance,
lemma " !! q qa n. [| 0 < n; int n <= 12; int n * q = 12; int n * qa = 18 |]
==> int n <= 6"
This archive was generated by a fusion of
Pipermail (Mailman edition) and