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. I actually found it quite useful to see the component parts of the proof context without having to refer to the manual, though I think the old behaviour should still be present for print_status, i.e. telling the user what they specified. 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. 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".
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. Phil _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com