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

    instead of your apply unfold, apply auto, done

  * About your funny comments (* by contradiction *): according to the
    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:

notepad
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


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