Re: [isabelle] need help with quantified ints



Perhaps a more direct specialisation to your problem is to use the
"int _ <= _" pattern in the helper lemma. Also, as Tobias points out,
these helpers can be proven by arith:

lemma int_le_val_disj:
  "m > 0 ==> (int n <= m) = (int n = m | int n <= m - 1)"
  by arith

lemma "int n <= 12 ==> P"
  apply (simp add: int_le_val_disj)
  oops

A similar trick was used in our project to prove that
{0 ..< 5} was equal to {0, 1, 2, 3, 4} - once again,
specialisation to the syntactic form in which the <
appears was helpful.

Yours,
	Thomas.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.