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