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

Reply via email to