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

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