Re: [isabelle] getting past ConstDefs.add_constdefs_i

On Tue, 28 Feb 2006, Michael Norrish wrote:

>   > cterm_of thy eqt;
>   val it =
>      "foo_body ==
>       TRY \<acute>j :== the (h_val \<acute>the_heap \<acute>i) CATCH SKIP END"
>   : Thm.cterm
> But, if I try to use this as the basis for a definition, I get an
> error from the constant certification part of the code:
>   > thy |> Constdefs.add_constdefs_i ([], [(NONE, (("", []), eqt))]);
>   Exception-
>      TYPE
>         ("Illegal type for constant \"mytest.globals.the_heap\" :: globals => addr => word8",
>            [],
>            []) raised
> What am I likely to be doing wrong in my invocation of add_constdefs_i?

This is hard to guess from a distance.

Generally speaking, add_constdefs_i is just the internal version of a 
user-level command -- it is common practice to provide both external and 
internal version just to make sure that ML packages can always invoke each 
other.  For basic definitions the primitive add_consts/add_defs are 
usually easier to use in ML.  Even more, constdefs is about to become a 
legacy feature pretty soon, being superceded by a more general 
'definition' element.

Anyway, add_constdefs_i actually does work for me as follows:

  val eq = Logic.mk_equals (Free ("x", HOLogic.boolT), Const ("True", HOLogic.boolT));
  val thy =
    Theory.begin_theory "Test" [Main.thy]
    |> Constdefs.add_constdefs_i ([], [(NONE, (("", []), eq))]);

  print_theory thy;

Note that Constdefs.add_constdefs_i produces extra noise on the message 
channel -- this is a toplevel command after all.


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