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

[Qian Hong]

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
reached.
Goal:
```
 ((exec (comp a) s stk_option) = (case stk_option of (None ⇒ None) | ((Some
stk) ⇒ (Some ((aval a s) # stk)))))

constants:
  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
option)))
  op = :: (int list option ⇒ (int list option ⇒ bool))
  Trueprop :: (bool ⇒ prop)
  op ⟹ :: (prop ⇒ (prop ⇒ prop))
variables:
  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?
Like:
```
((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
details.

Thanks in advance!

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

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