# Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]

```On Thu, 22 Nov 2012, Christoph LANGE wrote:

```
```I'm now back at our auction formalisation and catching up with emails.

http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/Vickrey.thy
```
```
```
A few more hints on the version that happens to be behind this inversion link right now:
```
* 'definition' with Pure equality (==) is quite old-fashioned.  Normally
you just use HOL = or its abbreviation for bool <-> here, as you would
for 'primrec', 'fun', 'function'

(In contrast HOL --> and ! are old-fashioned/cumbersome, where Pure
==> and !! would do the job better.)

* I recommend to put the whole 'head' of some definition on one line,
this works best with jEdit folding:

definition a :: A
where "a = t"

fun b :: B
where "b x = t"

Where the 'where' goes depends on the length of A and t; it is not
informative for the head, so I prefer to have it second by default.

* 'done' should be indented like the 'apply' script.  Don't ask why,
Isar indentation is an arcane discipline, and still awaits tool
support in Isabelle/jEdit.

BTW, the shortest structured proof that is not a script looks like
this:

lemma A unfolding a_def b_def c_def auto

Isar philosophy, you always strive to make things clear by formal
means, and avoid comments.  Thus can be done by putting a suitable
"proof (rule ...)" standard step here.

According to my experience, informal or semi-formal people often have
problems to understand what not-introduction, not-elimination, and
classical reasoning means.  The following examples explore this in the
formal playground:

begin

have "¬ A"
proof (rule notI)
assume A
then show False sorry
qed

next

have "¬ A" sorry
have A sorry
from `¬ A` and `A` have C by (rule notE)

from `¬ A` and `A` have C by contradiction
from `A` and `¬ A` have C by contradiction

next

have C
proof (rule ccontr)
assume "¬ C"
then show False sorry
qed

next

have C
proof (rule classical)
assume "¬ ?thesis"
then show ?thesis sorry
qed

next

have C
proof (rule classical)
assume "¬ ?thesis"
then have False sorry
then show ?thesis by (rule FalseE)
qed

end

```
Here the rule steps with notI, notE, FalseE have been made explicit for illustration: these default rules are normally omitted, i.e. you would just write 'proof' without anything or '..' in instead of 'by (rule ...)'.
```
```
The Isar method "contradiction" allows to present to two preconditions in either order -- this often happens in practice. For notE the negated formula has to come first, to eliminate it properly.
```
```
There is nothing special behind any of these intro/elim steps so far: just plain intuitionistic natural deduction. Nonetheless, people sometimes think that notI is "proof by contradiction", because they have to show False in the end.
```
```
This might also stem from the ccontr rule above, which is often seen in text books (without this Isabelle-specific name). I usually prefer the one called "classical", because it lacks the builtin False step and illustrates the brutality of classical reasoning in a pure way: you may assume that the thesis does not hold, then you have to show that it holds. The latter proof often works "by contradiction" in the above formal sense, to explain once more while you might get confused informally.
```
```
Formally, everything should be clear at this pure Isar level, because there is no magic built-in apart from higher-order unification and proof-by-assumption to solve trivial "end-games" in natural deduction.
```

Makarius```

• Follow-Ups:
• References:

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