Re: [isabelle] Syntax issue: lost between HOL and Isar
On 01.08.2012 22:02, Yannick Duchêne (Hibou57) wrote:
Hi all proof lovers,
After the Isar reference, I typed this in Isabelle/jEdit:
fix n :: nat
have "P n"
proof (induct n)
show ?case sorry
case (Suc n)
from Suc.hyps show ?case sorry
As the syntax from the PDF is not always exact (mainly characters
issues), I though there was an error there too, and felt “(Suc n)”
should be enclosed in quote, as an HOL expression. But doing so, I get
this in the Output pan:
Unknown case: "(Suc n)"
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?
The Isar command "case" (in its long form) takes a case name and a list
of inner syntax expressions (probably what you mean with HOL
expressions). The case name "Suc" happens to be the same as the name of
the constructor "Suc"; but this is just coincidence:
fix n :: nat and P
proof (induct n rule: nat.induct[case_names Foo Bar])
case Foo show ?case sorry
case (Bar n) show ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and