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

4
votes

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.

2
isabelle

2 Answers

6
votes

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.

4
votes

You can enable simplifier tracing; in Proof General, you can do this with Isabelle → Settings → Tracing → Trace Simplifier, I don't know about jEdit.

EDIT: In this case the simp trace will not be very helpful, since simp does not use rewrite rules to solve this, instead it "sees" A, B, and C in the premises and concludes that it can, in the context of this statement, rewrite A = True, B = True, and C = True, then it rewrites the goal B to True and you're done.

However, the "normal" way of proving statements such as this is to use the assumption method, which matches the goal against a premise, in this case B. There is probably a way to prove this using rule as well, but that would be unnecessarily complicated. assumption uses assume_tac, which in turn is just a wrapper around the very basic function Thm.assumption, so this can really be considered one of the most elementary proof methods in Isabelle. So just write by assumption.