Re: [isabelle-dev] Creating Theorems in ML

2019-02-28 Thread Makarius 
On 28/02/2019 11:49, Achermann  Reto wrote:
> 
> [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. 

Isabelle/ML belongs to the normal Isabelle user space, so isabelle-users
is the place to go.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Creating Theorems in ML

2019-02-28 Thread Achermann Reto 
Hi,

[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"
begin

lemma foo:
  "A ==> (A ==> B) ==> B"
  by(auto)

end


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.


Thanks,
-- Reto
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev