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

```Hi Peter,

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

that you get frees/tfrees out of Specification.definition is as
expected. In order to obtain something with schematic variables, you
need to look, or rather, obtain the "foundation" of the newly-introduced
definitions. This can be done with appropriate morphisms:

local_setup âfn lthy =>
let
val (_, lthy') = Local_Theory.open_target lthy

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 _ = map (Thm.pretty_thm lthy') [foo'_thm, bar'_thm]
|> Pretty.big_list "before" |> Pretty.writeln

val lthy'' = Local_Theory.close_target lthy'

val phi = Proof_Context.export_morphism lthy' lthy''

val foo'_thm = Morphism.thm phi foo'_thm
val bar'_thm = Morphism.thm phi bar'_thm

val _ = map (Thm.pretty_thm lthy') [foo'_thm, bar'_thm]
|> Pretty.big_list "after" |> Pretty.writeln

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'

The pattern open_target/close_target is used all over BNF, presumably
with the same intent, although I'm not quite sure whether I've
reproduced it fully canonically here.

Cheers
Lars

```

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