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
    qed
  end

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:

facts:
<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".

Regards,
GB














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