Re: [isabelle] accessing ML definitions in isabelle_process





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 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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.