[isabelle] Proof_Context abstraction



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
Description: This is a digitally signed message part



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