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"
  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.