On 12 Apr 2011, at 12:00, Phil Clayton wrote:

> Rob Arthan wrote:
>> a) Alongside the functions set_pc, set_merge_pcs, PC_T, MERGE_PCS_T, etc. 
>> there are now functions set_extend_pc, set_extend_pcs, EXTEND_PC_T, 
>> EXTEND_PCS_T etc., that extend the current proof context rather than 
>> overwrite it. This facilitates proof contexts that just change the behaviour 
>> of particular proof procedures like forward chaining.
> 
> I've noticed some change to the proof context output of print_status (as
> supplied by get_current_pc):
> 
> 1. The output of print_status now includes the all proof contexts
> implicitly included by the specified proof context.  For example, for
> 
>  set_pc "z_library"
> 
> print_status produces
> 
>  Current proof context name(s): ['z_predicates, 'z_decl,
>   z_predicates, 'z_%mem%_set_lang, 'z_bindings, 'z_schemas,
>   'z_tuples, z_language, 'z_normal, 'z_%mem%_set_lib,
>   'z_sets_alg, z_sets_alg, 'z_rel_alg, 'z_fun_alg,
>   'z_numbers, z_library];
> 
> 2. If a proof context is requested more than once, explicitly or
> implicitly, it appears more than once in the list printed by
> print_status.  For example, for
> 
>  set_merge_pcs ["z_library", "z_predicates"];
> 
> print_status produces
> 
>  Current proof context name(s): ['z_predicates, 'z_decl,
>   z_predicates, 'z_%mem%_set_lang, 'z_bindings, 'z_schemas,
>   'z_tuples, z_language, 'z_normal, 'z_%mem%_set_lib,
>   'z_sets_alg, z_sets_alg, 'z_rel_alg, 'z_fun_alg,
>   'z_numbers, z_library, 'z_predicates, 'z_decl,
>   z_predicates];
> 
> I suspect 1 and 2 are really the same thing.  I presume this is
> unintended as it does not fit the behaviour described for get_current_pc
> in the manual.

It's an unintended side-effect of some rationalisations in the code that I did 
while implementing set_extend_pcs etc. I will fix it in the next release.

>  I actually found it quite useful to see the component
> parts of the proof context without having to refer to the manual,

I can see what you mean. Unfortunately just knowing the names of the component 
proof contexts that have been merged into a proof context doesn't tell you what 
extra facilities have been added piecemeal to it. So it isn't very clear 
whether we could make a useful separate feature to tell you what the components 
are.

> though
> I think the old behaviour should still be present for print_status, i.e.
> telling the user what they specified.
> 
Agreed.

> 
> Regarding this new capability, given a current proof context e.g.
> ["z_library", "'z_reals"], is it more efficient to do e.g.
>  set_extend_pcs ["a", "b"];
> than
>  set_merge_pcs ["z_library", "'z_reals", "a", "b"]
> ?  It looks like it is from reading the source code but I didn't fully
> digest everything.

It will be a little bit more efficient, but I wouldn't expect it to be 
significant. It won't bypass any of the inference involved in preprocessing 
proof context fields.

> 
> Also I noticed imp051.doc, line 1594:
> fun Ûset_extend_pcsÝ ([]: string list): unit = fail "set_merge_pcs" 51020 []
> should probably not say "set_merge_pcs".
> 

Thanks for pointing that out.

> 
>> b) A variable capture problem in %implies%_match_mp_rule1 that made forward 
>> chaining fail has been addressed in a new rule %implies%_match_mp_rule2. The 
>> new behaviour has been adopted as the default, but this can make some 
>> existing proofs break. Component proof contexts "'mmp1" and "'mmp2" are 
>> provided that let you switch between the new and old behaviour. Using, 
>> set_extend_pc"'mmp1" or EXTEND_PC_T "'mmp1" will revert to the old behaviour 
>> and gives a quick way of fixing any broken proof scripts.
> 
> Glad to see that has been fixed.  I have stumbled on that one every so
> often for years but never got around to looking into it.
> 

Regards,

Rob.

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to