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.