*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Proof_Context abstraction*From*: Joachim Breitner <breitner at kit.edu>*Date*: Tue, 29 Jul 2014 11:00:47 +0200

Hi, I’m trying to learn hacking Isabelle/ML, and I started with the seemingly simple task of “For all local facts with a name, add a "foo" to their name”. Here is what I tried: theory Scratch imports Main keywords "foobar" :: prf_decl begin ML {* fun named_local_facts ctxt = let val facts = Proof_Context.facts_of ctxt; in Facts.dest_static false [Global_Theory.facts_of (Proof_Context.theory_of ctxt)] facts end; val foobar_cmd = Proof.map_context (fn ctxt => let val facts = named_local_facts ctxt val renamed = map (apfst (suffix "foo")) facts in fold (Proof_Context.put_thms true) (map (apsnd SOME) renamed) ctxt end ); Outer_Syntax.command @{command_spec "foobar"} "my test command" (Scan.succeed (Toplevel.proof foobar_cmd)); *} notepad begin assume bar: "p = (a,b)" and X foobar end end Unfortunately, I get Bad name binding: "local.barfoo" It seems to me that Proof_Context provides a certain abstraction over local facts, where I can still retrieve them in a raw way (“facts_of”), but I can only add them via an interface (“put_thms”) that expect the names in a certain, yet-to-be-mangled name. Is that roughly correct? Is there a way to mess with the internals of the Proof_Context directly, or would I have to change proof_context.ml for that (such as exposing map_data)? Or am I approach this task in a wrong way? Thanks, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Proof_Context abstraction***From:*Joachim Breitner

**Re: [isabelle] Proof_Context abstraction***From:*Makarius

- Previous by Date: Re: [isabelle] Undefined facts in skip_proofs mode
- Next by Date: Re: [isabelle] Isabelle2014-RC1 available for testing
- Previous by Thread: Re: [isabelle] Undefined facts in skip_proofs mode
- Next by Thread: Re: [isabelle] Proof_Context abstraction
- Cl-isabelle-users July 2014 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