# [isabelle] Specification.definition: Getting theorem for Const, not Free?

```Hi List,

I have a problem with Specification.definition:

I want to implement the following functionality on ML-level:

context
fixes a::'a
begin

(* Want to implement these 3 definitions: *)
definition "bar = ((a,1::nat),(a,True))"
definition "foo b = (a,b)"
lemmas test = bar_def[folded foo_def]
>>> theorem test: local.bar = (local.foo 1, local.foo True)

My first attempt was:

context
fixes a::'a
begin

local_setup âfn lthy => let
val ((_,(_,bar'_thm)),lthy) = Specification.definition (NONE,
((Binding.empty,[]),@{prop "bar' = ((a,1::nat),(a,True))"})) lthy
val ((_,(_,foo'_thm)),lthy) = Specification.definition (NONE,
((Binding.empty,[]),@{prop "foo' b = (a,b)"})) lthy

val _ = @{make_string} [foo'_thm, bar'_thm] |> tracing

val test_thm = Local_Defs.fold lthy [foo'_thm] bar'_thm

val (_,lthy) = Local_Theory.note ((@{binding test'},[]),
[test_thm]) lthy

in
lthy
end
â
thm test'

However, the theorem does not look as expected, foo is not folded. A
quick inspection of the generated theorems (see tracing-output) quickly
reveals the reason for that:

tracing output is:
["foo' ?b = (a, ?b)"  [.], "bar' = ((a, 1), a, True)"  [.]]

where foo' and bar' are free variables (!) rather than constants, and
the type of ?b is ?b::'b, which, obviously, does not unify with nat nor
bool.

My question:
What is the correct way to implement the above in Isabelle-ML?
Is there a way to get a _def-theorem that contains a Const rather than
a Free, and a ?b::?'b rather than ?b::'b  ?

Thanks in advance for any help,
Peter

```

• Follow-Ups:

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