Re: [isabelle] need help with quantified ints

Here is a proof:

  fixes q qa n
  assumes n0: "n > 0" and n12: "int n <= 12"
    and nq: "int n * q = 12" and nqa: "int n * qa = 18"
  shows "int n <= 6"
  from nq nqa
  have "int n dvd 12" "int n dvd 18" unfolding dvd_def by auto
  hence th: "n dvd 12" "n dvd 18" unfolding int_dvd_iff by auto
  from gcd_greatest[OF th] have "n dvd 6" by (simp add: gcd.simps)
   (* This is actually stronger than the final conclusion *)
  hence "n <= 6" by (rule dvd_imp_le, simp)
  then show "int n <= 6" by simp

Some parts of the proof should be done automatically by algebra, but apparently there is a bug (on my TODO).

Hope it helps,

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