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.

Accepted Answer

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.

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

Solution

Problem