*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Specification.definition: Getting theorem for Const, not Free?*From*: Lars Hupel <hupel at in.tum.de>*Date*: Thu, 23 Jun 2016 08:24:33 +0200*In-reply-to*: <1466638256.20921.22.camel@lapnipkow10>*References*: <1466638256.20921.22.camel@lapnipkow10>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.1.1

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

**References**:**[isabelle] Specification.definition: Getting theorem for Const, not Free?***From:*Peter Lammich

- Previous by Date: [isabelle] CfP: F-IDE2016, 3rd Workshop on Formal Integrated Development Environment
- Next by Date: [isabelle] Permutations
- Previous by Thread: [isabelle] Specification.definition: Getting theorem for Const, not Free?
- Next by Thread: [isabelle] CfP: F-IDE2016, 3rd Workshop on Formal Integrated Development Environment
- Cl-isabelle-users June 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list