Re: [isabelle] Proof by contradiction



Thanks...this is *exactly* what I was looking for. It leads me to a few
more questions, though,

* First, T (from "T = A2Point u v") is not bound. Isabelle/jEdit is showing
> that with the different background. You want something along:
>     obtain T where
>       ‹…›
>   * Similarly, you have to use obtain for u and v, not fix.


Can you suggest somewhere that I can learn the distinction between "obtain"
and "fix"? The reference manual has a paragraph that's too cryptic for my
current understanding of logic (which is quite basic); Ballarin's tutorial
slides basically say "they're different". I think I need something in the
middle. :)

  * Then the last step has to be "show False" instead of "have False". Then
> you will get an error ("Failed to refine any pending goal"), because "rule
> ccontr is only negating once more ‹¬ (∃ T. a2meets T l  ∧ a2meets T k)›.
> You can fix that by removing "rule ccontr" and rely on the default rule
> to do the right thing.


If I actually *wanted* to do a proof by contradiction, even though it's not
necessary here, would I have to start with

 proof (rule ccontr)
    assume "¬¬ (∃ T. a2meets T l  ∧ a2meets T k)"

Perhaps choosing a theorem with a negation in the conclusion was a bad
place to start trying to use proof-by-contradiction. But I'd really like to
see how to do such a proof.

Later you suggest restating the theorem as its contrapositive (which may or
may not be a good idea...I don't know whether Isabelle can use the
contrapositive as effectively for what I need to do next), and propose
three things (which I've reordered):
* use cartouche
* use "defines" instead of "assumes"
* remove the "exist" quantifier

My questions:

 -- Typing double-quotes is easy; typing cartouches is tough (for me) ---
is there some simple way to do this, and are they the preferred form now?
 -- the reference manual, page 102) says that 'defines" defines a
previously declared parameter, but in your use

> lemma A2_vert2:
>   fixes x0 x1 :: real
>   defines l_form: ‹l ≡ A2Vertical x0›
>   defines k_form: ‹k ≡ A2Vertical x1›
>   assumes ‹a2meets T l› and ‹a2meets T k›
>   shows ‹l = k›
>   by (cases T) (use assms in auto)
>
the parameters l and k haven't been previously  declared (as far as I can
tell). Of course, that description of "defines" is in the section about
locales in the reference manual, so it's probably the wrong one. But it's
the only mention of that keyword in the whole manual, so I'm at a loss for
what this actually means here.

-- does this form of the statement really remove the "exists" quantifier?
Or is there an implicit "exists" in the "assumes" line? And does removing
it (assuming it's really gone) make things easier for the prover?

--John



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