[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-dev at 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.