Email Gateway (Aug 22 2022 at 09:31): Email Gateway (Aug 22 2022 at 09:31):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hello,
I have a theory which defines
theory TestML imports Main
begin
ML
{*
val Set_ex_bool_eq = @{thm Set.ex_bool_eq};
val Set_all_bool_eq = @{thm Set.all_bool_eq};
*}
end
How can I access these objects from the isabelle_process?
I know that I can load the theory file using use_thy "TestML",
but I could not figure out how to access these names.
Best regards,
Viorel Preoteasa
Email Gateway (Aug 22 2022 at 09:32):From: Makarius <makarius@sketis.net>
Almost everything in Isabelle lives within a formal theory context,
including the ML environment. It is merely a historical accident of the
Isabelle/Pure bootstrap process that the ML content of Pure.thy is also
dumped onto the naked ML toplevel of isabelle_process or isabelle console.
So the canonical approach is to evaluate Isabelle/ML snippets inside a
proper theory context like Main above. The remaining question is how to
achieve that for your application. E.g. one could produce a temporary
.thy file on the spot and load that with use_thy.
Makarius
Email Gateway (Aug 22 2022 at 09:32):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
On 4/28/2015 8:44 PM, Makarius wrote:
On Tue, 28 Apr 2015, Viorel Preoteasa wrote:
I have a theory which defines
theory TestML imports Main
begin
ML
{*
val Set_ex_bool_eq = @{thm Set.ex_bool_eq};
val Set_all_bool_eq = @{thm Set.all_bool_eq};
*}
endHow can I access these objects from the isabelle_process?
I know that I can load the theory file using use_thy "TestML",
but I could not figure out how to access these names.Almost everything in Isabelle lives within a formal theory context,
including the ML environment. It is merely a historical accident of
the Isabelle/Pure bootstrap process that the ML content of Pure.thy is
also dumped onto the naked ML toplevel of isabelle_process or isabelle
console.
But I guess, if I get this context, I can manipulate it from the ML top
level.So the canonical approach is to evaluate Isabelle/ML snippets inside a
proper theory context like Main above. The remaining question is how
to achieve that for your application. E.g. one could produce a temporary
.thy file on the spot and load that with use_thy.
Using Isabelle/ML snippets inside a proper theory context seems
oriented towards a user interface. But I need to do this in batch mode.
If I use this approach I have to create always a theory file,
and then load it using use_thy. I would need to do this for every small
call that I need.
I have the following Isabelle/ML:
ML
{*
val Set_ex_bool_eq = @{thm Set.ex_bool_eq};
val Set_all_bool_eq = @{thm Set.all_bool_eq};
fun bool_ctxt ctxt = Simplifier.add_simp Set_ex_bool_eq
(Simplifier.add_simp Set_all_bool_eq ctxt);
fun term_to_string ctxt t =
let
val ctxt' = Config.put show_markup false ctxt;
in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
fun simplifya s ct th =
let
(val _ = use_thy thy_name;)
val t = Syntax.read_term ct s;
val simp_term_a = Simplifier.rewrite ct (cterm_of th t) |> Thm.rhs_of;
val simp_term_b = Simplifier.rewrite (bool_ctxt ct) simp_term_a |>
Thm.rhs_of;
val simp_term_c = term_of simp_term_b;
val result = term_to_string ct simp_term_c;
in result end;
fun simplify s thy_name =
let
(val _ = use_thy thy_name;)
val thy = Thy_Info.get_theory thy_name;
val ctxt = Proof_Context.init_global thy;
in simplifya s ctxt thy end
*}
I can define this code in a ml file, except:
val Set_ex_bool_eq = @{thm Set.ex_bool_eq};
val Set_all_bool_eq = @{thm Set.all_bool_eq};
probably there is a way to get these theorems at the toplevel of
isabelle_process
using the context and the theory.
I like the possibility of writhing my functions within a theory, but I
would like
very much to be able to use these functions at the toplevel of
isabelle_process
without generating a new file for every call that I need.
Viorel
Email Gateway (Aug 22 2022 at 09:32):From: Makarius <makarius@sketis.net>
On Tue, 28 Apr 2015, Viorel Preoteasa wrote:
Using Isabelle/ML snippets inside a proper theory context seems oriented
towards a user interface. But I need to do this in batch mode. If I use
this approach I have to create always a theory file, and then load it
using use_thy. I would need to do this for every small call that I need.
I was talking about batch mode already. You could e.g. put all your tool
setup in a static .thy (or .thy that loads a .ML via ML_file). It could
refer to some environment variables to get dynamic input from somewhere
else, e.g. another tmp file.
There are many more possibilities, e.g. using Isabelle/Scala for the
systems programming.
fun simplifya s ct th =
The "ct" here seems to be a Proof.context, and the one and only one naming
convention is "ctxt". See also the "implementation" manual.
I can define this code in a ml file, except:
val Set_ex_bool_eq = @{thm Set.ex_bool_eq};
val Set_all_bool_eq = @{thm Set.all_bool_eq};probably there is a way to get these theorems at the toplevel of
isabelle_process
using the context and the theory.
Isabelle/ML files always refer to a proper theory context. So we are back
to the start.
Makarius
Email Gateway (Aug 22 2022 at 09:32):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
If I do this, and for example I define a value in a theory file:
theory TestML imports Main
begin
ML{*
val newline = writeln ""
*}
end
Now in isabelle_process I do:
use_thy "TestML"
The basic question is how do I access the value newline in the
isabelle_process?
If I try just newline it is not recognized. Is this value available
under some scope?
Is it so that I am not supposed to access it from other place, except
the theory?
Viorel
Email Gateway (Aug 22 2022 at 09:32):From: Makarius <makarius@sketis.net>
The value is part of the theory context of TextML. You can access it in a
theory that imports it, for example.
All of Isabelle/ML happens within some theory context. The standard
commands for that are 'ML' and 'ML_file' -- they are computationally
complete wrt. the ML language. You can do whatever you want with it,
including arbitrary I/O with the outside world.
Of course, you can define variants of the above 'ML' commands for your own
purposes. With some more efforts it is also possible to define variants
of use_thy + embedded Isabelle/ML in the raw ML toplevel environment, to
bypass files altogether -- it depends on the application what is really
required.
Here is an example to play with Isabelle/ML runtime-compilation-evaluation
in Isabelle2015-RC:
theory Scratch
imports Main
begin
ML ‹fun ML ctxt source = ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags source›
ML ‹ML @{context} ‹writeln @{const_name True}››
end
Here is the same for the raw ML toplevel of isabelle_process:
fun ML ctxt source = ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags source;
ML (Proof_Context.init_global (Thy_Info.get_theory "Main")) (Input.string "writeln @{const_name True}");
This works to some extent, but not all aspects of the normal
Isabelle/Isar/ML environment is imitated here (like proper handling of
interrrupts and exceptions).
Makarius
Last updated: Nov 04 2025 at 01:44 UTC