Email Gateway (Aug 19 2022 at 08:32): Email Gateway (Aug 19 2022 at 08:32):From: charmi panchal <charmipanchal2006@gmail.com>
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
Email Gateway (Aug 19 2022 at 08:32):From: Makarius <makarius@sketis.net>
Included is a minimal example to make your own command that defines
various terms, with simultaneous type checking that is typical for
applications as you have sketched above.
Since you are already using Isbelle/jEdit, most of the historic
complications of keyword tables disappear. You just work directly in the
given A.thy file.
The other notable thing is this: first you use several isolated Parse.term
invocations for "outer syntax" parsing of string tokens that will be
interpreted as terms later. Then you do the actual "innter syntax"
parsing via Syntax.parse_terms, with simultaneous type-checking of the
given list of items.
In your sketch above you could probably need Syntx.parse_props, or
full-scala Specification.read_specification (which requires a different
outer syntax parser).
Makarius
A.thy
Email Gateway (Aug 19 2022 at 08:32):From: Makarius <makarius@sketis.net>
One more thing: CTRL with mouse hovering gives you information about
inferred ML types, and hyperlinks of defined ML items, which is
indispensible to work with Isabelle/ML effectively -- and to learn it in
the first place. (Mac users need to use COMMAND instead of CTRL.)
Makarius
Last updated: Apr 20 2024 at 12:26 UTC