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:

notepad
begin
fix n :: nat
have "P n"
proof (induct n)
case 0
show ?case sorry
next
case (Suc n)
from Suc.hyps show ?case sorry
qed
end

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:

notepad
  begin
  fix n :: nat and P
  proof (induct n rule: nat.induct[case_names Foo Bar])
    case Foo show ?case sorry
  next
    case (Bar n) show ...





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