*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] accessing ML definitions in isabelle_process*From*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Date*: Tue, 28 Apr 2015 21:20:22 +0300*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1504281940020.19676@lxbroy10.informatik.tu-muenchen.de>*References*: <553FA17B.4020002@aalto.fi> <alpine.LNX.2.00.1504281940020.19676@lxbroy10.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.3; WOW64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

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}; *} 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.Almost everything in Isabelle lives within a formal theory context,including the ML environment. It is merely a historical accident ofthe Isabelle/Pure bootstrap process that the ML content of Pure.thy isalso dumped onto the naked ML toplevel of isabelle_process or isabelleconsole.

So the canonical approach is to evaluate Isabelle/ML snippets inside aproper theory context like Main above. The remaining question is howto 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,

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 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_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};

using the context and the theory.

without generating a new file for every call that I need. Viorel

**Follow-Ups**:**Re: [isabelle] accessing ML definitions in isabelle_process***From:*Makarius

**References**:**[isabelle] accessing ML definitions in isabelle_process***From:*Viorel Preoteasa

**Re: [isabelle] accessing ML definitions in isabelle_process***From:*Makarius

- Previous by Date: Re: [isabelle] accessing ML definitions in isabelle_process
- Next by Date: Re: [isabelle] accessing ML definitions in isabelle_process
- Previous by Thread: Re: [isabelle] accessing ML definitions in isabelle_process
- Next by Thread: Re: [isabelle] accessing ML definitions in isabelle_process
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list