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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
