Re: [isabelle-dev] Updating the current theory

[Alexander Krauss]

Hi Michael,

Thanks, Alex. Indeed, the effect I'm after is like using setup {* *}, 
but ultimately I'd like this effect to be produced by calling a tactic, 
i.e. let a tactic make updates to the current theory when invoked using 
'apply (tac...)'.


AFAIK, this is impossible. Tactics/methods cannot update the theory, 
they just operate on goals. To change the theory you need to issue a 
declaration, either via setup or a command of your own, or by using 
attributes.


Don't try to use imperative things like Isar. and don't mess with the 
Toplevel. It will almost certainly break some fundamental invariants and 
not solve your problem. Instead, try to move the theory transformation 
elsewhere.


Alex


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Updating the current theory

[Makarius]

On Sat, 27 Nov 2010, Michael Chan wrote:

ultimately I'd like this effect to be produced by calling a tactic, i.e. 
let a tactic make updates to the current theory when invoked using 
'apply (tac...)'.


Within a proof the background theory is strictly read-only. I don't know 
what happens if you try to change it.  Probably the system will halt and 
catch fire at some point.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Updating the current theory

[Michael Chan]

On 27/11/10 17:12, Alexander Krauss wrote:

Hi Michael,

I think you want to use

setup {*
ml_expression
*}

where ml_expression has type theory - theory.



Thanks, Alex. Indeed, the effect I'm after is like using setup {* *}, 
but ultimately I'd like this effect to be produced by calling a tactic, 
i.e. let a tactic make updates to the current theory when invoked using 
'apply (tac...)'. I'll look at the implementation of 'setup'.


Michael


Alex


Michael Chan wrote:

Hello,

I'm trying to update the current theory at the ML-level, e.g.,
creating a new table in the current theory.

For example, I have a function foo that does very much what
Locale.register_locale does -- mainly, adding an entry into a table in
the name space:

ML {*

val thy' = foo x @{theory};
Bar.get thy';

*}
thy' is therefore the updated theory (containing the new table). Let
Bar be

structure Bar = Theory_Data (...)

So Bar.get thy' returns the Name_Space-table pair, in which the table
is updated. This is fine if I call Bar.get thy' rather than Bar.get
@{theory} because the current theory hasn't been updated. Now, what
if I want the update to be made in the current theory such that I can
get the updated table using Bar.get @{theory} instead?

What I have tried so far is to rebuild HOL with datatype node = ...
and val transaction ... declared in signature TOPLEVEL and I
transform the state using Isar.:

ML {*
val thy' = foo x @{theory};

val update_thy = Toplevel.transaction (fn int =
(fn Toplevel.Proof (prf, (finish,_)) = Toplevel.Proof (prf, (finish,
Context.Theory thy'))
| Toplevel.Theory (_,c) = Toplevel.Theory (Context.Theory thy', c)
));

val tr = Toplevel.name test_tr Toplevel.empty;
update_thy tr | Isar.;

Bar.get @{theory};
*}

Here, Bar.get @{theory} still doesn't give me the updated table.
However, if I undo one step and add

ML {*
Bar.get @{theory}
*}

then do one step, I see the updated table! I must be transforming the
states incorrectly -- perhaps I shouldn't use Isar.? Also, I have a
strong feeling that I'm not supposed to rebuild HOL with those hacks
in TOPLEVEL...

Thanks for the help in advance.

Michael



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev