Re: [isabelle] need help with quantified ints

Hi Perry,

You need to use case_tac rather than cases when n is bound by a meta- quantifier in a subgoal, at least if you are carrying out an apply- style proof. case_tac also works when the variable is not bound, and like all other proof methods ending in _tac, you can apply it to other than the first subgoal (e.g. apply (case_tac[3] ...)), to multiple subgoals (e.g. apply (case_tac[1-3]...)), or to all subgoals (e.g. apply (case_tac[!] ...)).

I'm not sure why cases doesn't allow you to split on meta-bound variables, as this would be less confusing for new users. Similarly for induct vs. induct_tac. Feature request?


On Jun 19, 2008, at 2:32 PM, 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.