[isabelle-dev] Creating Theorems in ML
reto.achermann at inf.ethz.ch
Thu Feb 28 11:49:36 CET 2019
[apologies in advance if this should have gone to the isabelle-users list]
We are using ML in a project where we need to create a locale in HOL from ML code. We managed to create the locale (local_theory) using Expression.add_locale_cmd including any assumptions we defined in ML.
As a next step we would like to create a theorem from ML, e.g.
locale MyLocale =
fixes S::"nat set"
"A ==> (A ==> B) ==> B"
We tried using Local_Theory.note with the Goal or Thm structures, but apart from trivial True ==> True there is not much success. Moreover, the example (3.7 Theorems) in the cookbook doesn't seem to work with 'Illegal fixed variable: "P"'
I'm thankful for any pointers to examples or descriptions on how to add/define a lemma/theorem inside a locale from an ML file.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev