[isabelle] Parsing specification for lemma



Hello Everyone,
Presently I am learning from Isabelle cookbook and mostly referring
Chapter 5 and 7.
There is an example of even and odd where  predicate is given as follows.

*simple_inductive
  even and odd
  where
  even: "even 0" |
  evenS: "odd n ⟹ even (Suc n)"|
  oddS: "even n ⟹ odd (Suc n)"*

After following the ML coding given in Ch 5 and 7 and practised in JEdit,
intro and induction theorems were seen for this predicate.
I am interesting to know that, how to write following   lemma statement

*lemma "i≥0 ⟹ i1 = i + Suc(0) ⟹ i1 > 0"*

as

*Transition
 Pre_condition :   " i ≥ 0" |
 guard1 : "i1 = i + Suc(0)" |
 final : " i1 > 0 "*

I need guidance to perform this task. I am trying to find special purpose
parsers that help with parsing specification for the above lemma.

I will be thankful  for your advices and suggestions.

Best regards
Charmi Panchal




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