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:

For readability I'd sometimes like to make it explicit to what assumption I'm referring when there is more than one.

When explicitly restating them with 'assume "... (Suc n) ..."' that's no problem. With "Suc" I found, e.g., Suc.prems(1) to work. A symbolic name, e.g. Suc.prems(foo), if the original statement says 'assumes foo: "..."', would be even nicer – but that's not possible, I suppose.

Restating case/assume is not a big deal, it is done occasionally and not bad style, only a bit redundant and less formally checked than could be done otherwise.

To make it more tight, you can do it via literal fact references or the corresponing "fact" method like this:

notepad
begin

  fix n :: nat

  have "P n"
  proof (induct n)
    case 0
    then show ?case sorry
  next
    case (Suc n)
    then show ?case sorry
  qed

  have "P n"
  proof (induct n)
    case 0
    show "P 0" sorry
  next
    case (Suc n)
    from `P n` show "P (Suc n)" sorry
  qed

  have "P n"
  proof (induct n)
    case 0
    show "P 0" sorry
  next
    case (Suc n)
    have "P n" by fact
    then show "P (Suc n)" sorry
  qed

  have "P n"
  proof (induct n)
    case 0
    show "P 0" sorry
  next
    case (Suc n)
    assume "P n"
    then show "P (Suc n)" sorry
  qed

  have "P n"
  proof (induct n)
    show "P 0" sorry
  next
    fix n
    assume "P n"
    then show "P (Suc n)" sorry
  qed

end


BTW, according to the way the logical framework works, you can have redundant 'assume' statements in your proof body, but not redundant 'fix'. The "fix n" is already part of the case (Suc n). Another fix n would postulate a different hyptothetical entity in the context, that is not the same, and its assumptions unrelated to what you have already after invoking the case.

The funny thing is that textbook logicians often omit the formal "fix n" altogether. I've seen this even in some implementations of logic, where the global absence of a declaration over the whole text is taken as an implicit fix of a local variable.


	Makarius


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