Proving A ==> B ==> C ==> B in Isabelle

Question

I am puzzled about proving

A ==> B ==> C ==> B 

in Isabelle. Obviously you could

apply simp

but how could I prove this with using rules?

Alternatively, is there a way to dump the rules simp used? Thanks.

Answer 1

If you really want to understand how proofs work, you should forget both about funny tactics and automated reasoning tools as a start.

The statement A ==> B ==> C ==> B (using this special ==> connective) of Isabelle/Pure is immediately true, so its proof in Isabelle/Isar is:

lemma "A ==> B ==> C ==> B" .

That's it, just . (which abbreviates by this, but the this is actually empty here).

As slightly less vacuous proof uses actual Isabelle/HOL connectives, which you can then handle by standard introduction or elimination steps. E.g. like this:

lemma "A --> B --> C --> B"
proof
  show "B --> C --> B"
  proof
    assume b: B
    show "C --> B"
    proof
      show B by (rule b)
    qed
  qed
qed

But that is not so interesting either: you build up a boring implication that that is then decomposed until you are finished.

To find more interesting Isabelle/Isar proofs just do some web search, or look through the sources that come with the system. A totally arbitrary example is here: Drinker.

There are also tons of manuals, actually too many of them.