Re: [isabelle] Introduction rule for quantifiers over sets of pairs



On Fri, 16 Nov 2012, Stephan van Staden wrote:

Using allI twice (or with +) does not work for me, but clarify does the job perfectly. Thanks a lot!

Putting automated tools like "clarify" or "auto" in the initial "proof" position is actually an anti-pattern of structured proofs. Sometimes it cannot be avoided, but it should not be done by default.

Instead, the usual way is to make a bottom-up proof with automated re-composition like this:

notepad
begin

  have "∀(a, b) ∈ S. P"
  proof -
    {
      fix a b
      assume "(a, b) ∈ S"
      have P sorry
    }
    then show ?thesis
      by auto  -- "terminal auto, instead of initial clarify etc."
  qed

end


This can also cause surprises sometimes, especially with too general types for the body within { ... }, but it usually works in a reasonably robust way, and does not depend on the details of what automation does.


	Makarius


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