[isabelle] Parsing specification for lemma
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.
even and odd
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"*
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and