[isabelle-dev] How to hack isabelle in order to print proof output in batch mode?

Qian Hong fracting at gmail.com
Wed May 17 16:04:16 CEST 2017

Dear folks,

I'm working on some Math-rich Natural Language Processing research, using
Archive of Formal Proofs and Isabelle as the source of training data.

I can imagine I might have to change Isabelle code in order to solve my
problems, so I decided to post in isabelle-dev instead of isabelle-user,
sorry if it's the wrong place.

Here are my goals. Start from a toy problem.

1. We have 90k lemmas in 300 articles, I'm looking for a command line which
can extract all lemmas and do some very basic processing.

Assume the lemma looks like this:
lemma "exec (comp a) s stk_option = (case stk_option of
                                     None ⇒ None |
                                     Some stk ⇒ Some (aval a s # stk))"

The expected result is like this (with no line break - gmail might add
unexpected line break):
 exec (comp a) s stk_option = (case stk_option of None ⇒ None | Some
(stk::int list) ⇒ Some (aval a s # stk))

I know it is trivial to do that in Isabelle JEdit GUI, but how to do that
in command line? I tried several `isabelle build` arguments but with no
luck yet.

2. Similar to the previous one, but I also want to show the result of
`declare [[show_brackets]]` `declare [[show_types]]` and `declare
[[show_consts]]`. Not sure if it is trivial given the previous goal is
 ((exec (comp a) s stk_option) = (case stk_option of (None ⇒ None) | ((Some
stk) ⇒ (Some ((aval a s) # stk)))))

  Pure.prop :: (prop ⇒ prop)
  aval :: (aexp ⇒ ((char list ⇒ int) ⇒ int))
  op # :: (int ⇒ (int list ⇒ int list))
  Some :: (int list ⇒ int list option)
  None :: int list option
  case_option :: (int list option ⇒ ((int list ⇒ int list option) ⇒ (int
list option ⇒ int list option)))
  comp :: (aexp ⇒ instr list)
  exec :: (instr list ⇒ ((char list ⇒ int) ⇒ (int list option ⇒ int list
  op = :: (int list option ⇒ (int list option ⇒ bool))
  Trueprop :: (bool ⇒ prop)
  op ⟹ :: (prop ⇒ (prop ⇒ prop))
  stk_option :: int list option
  s :: (char list ⇒ int)
  a :: aexp

3. What if I want to embed all the type signatures into the above formula?
((exec :: (instr list ...) (comp :: (aexp ... ) a :: aexp) s :: (char list
=> int) stk_option :: int list option) = .... # stk :: (int list))))))

I know the question I ask sounds weird to most people, basically I'm trying
to create some dataset to train a Deep Learning model on Mathematics
Part-of-Speech task. If anyone is interested I'm happy to explain more

Thanks in advance!

[1] http://prodg.org/talks/mnlp_billion_token_corpora

Qian Hong
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170518/b8bdce04/attachment.html>

More information about the isabelle-dev mailing list