Re: [isabelle] Syntax issue: lost between HOL and Isar



To answer the original question:

On 08/02/2012 05:02 AM, Yannick Duchêne (Hibou57) wrote:
     proof (induct n)
       case 0
         show ?case sorry
     next
       case (Suc n)
         from Suc.hyps show ?case sorry
    qed
Is “(Suc n)”, and HOL or Isar expression? If that's an HOL expression as
I believe, then why do I get that error report?
Here 'case (Suc n)' as well as 'case 0' (above) are part of Isar not HOL. We could also just use 'case 0' and 'case Suc', then it is more clear that we are just giving names of facts (those names are automatically established when starting with 'proof (induct n)'). The variant 'case (Suc n)' of 'case Suc' is just a nicety to allow giving explicit names to variables (which makes proofs more robust). If you want to see to what fact 'Suc' refers, just use 'from Suc' directly below the 'case' line.

cheers

chris






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