Re: [isabelle] Syntax issue: lost between HOL and Isar
On 8/1/2012 5:07 PM, Yannick Duchêne (Hibou57) wrote:
case (Suc n)
from Suc.hyps show ?case sorry
So, what's the expression type of “(Suc n)” at the line whose text is
“case (Suc n)”? Isn't “(Suc n)” an HOL expression? It appears in the
text as if it was an Isar expression, but I feel sure it's not. I'm
lost with that point.
Christian already gave you the answer, but I was hot on the trail
because it occurred to me to use "print_theorem" under "case (Suc n)",
which Christian had given as a tip some days ago. This all ties into
differentiating between Isar and HOL.
"case" is an Isar command that's described on page 129 of isar-ref.pdf.
If you try to put quotes like this:
case ("Suc n")
then you get the error:
Outer syntax error: name declaration expected, but keyword ) was found
The outer syntax error substantiates that "case" is not HOL syntax,
because HOL syntax is inner syntax.
Put "print_theorems" under "case (Suc n)", and you get this:
<unnamed>: ((P∷(Nat.nat ⇒ HOL.bool)) (n∷Nat.nat))
local.Suc: ((P∷(Nat.nat ⇒ HOL.bool)) (n∷Nat.nat))
Somebody like me might not know what it means, but it definitely tells
me that "Suc" isn't the the HOL function "Nat.Suc::(nat => nat)", like I
had told you. You can't always know what something means, but you can
know what it isn't sometimes.
Page 45 of prog-prove.pdf explains "case".
This archive was generated by a fusion of
Pipermail (Mailman edition) and