Re: [isabelle] need help with quantified ints



Hi Thomas,
   Thanks for your reply.  The trick in n_less_val_disj will be added to my
bag.  I've played with variations on it and am not having much luck.
   The problem I'm having is that the values in my lemma are ints, not
nats.  Even though n itself is a nat, it is cast to int for the
comparisons.  Thus all the nice tools for working with the much simpler nats
are not available (at least with my limited skills).
   Best regards,
   Perry

On Fri, Jun 20, 2008 at 7:16 AM, Thomas Arthur Leck Sewell <
tsewell at cse.unsw.edu.au> wrote:

> 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"
>  apply (simp add: n_less_val_disj)
>  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?
>>  Thanks in advance,
>>  Perry
>>
>> 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 MHonArc.