Re: [isabelle] Parsing specification for lemma

On Mon, 6 Aug 2012, charmi panchal wrote:

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.

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).

theory A
imports Main
keywords "define_terms" :: thy_decl

subsection "Main ML implementation"

ML {*
  fun define_terms args lthy =
      val ts = Syntax.read_terms lthy (map snd args);  (* simultaneous read *)
      val specs =
        map2 (fn (b, _) => fn t => ((b, NoSyn), ((Thm.def_binding b, []), t)))
          args ts;
      val (results, lthy') = fold_map Local_Theory.define specs lthy;
      val _ = writeln (PolyML.makestring results);  (* FIXME not for production version *)
    in lthy' end

subsection "Outer syntax wrapper"

ML {*
  Outer_Syntax.local_theory @{command_spec "define_terms"} "define some terms"
    (Parse.and_list1 (Parse.binding -- (@{keyword "="} |-- Parse.term)) >> define_terms)

subsection "Example"

define_terms foo = "True" and bar = "\<lambda>x. x"
term foo thm foo_def
term bar thm bar_def


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