Subject: Refiner

Keywords: ::proof
          ::usage
          ::replay

Title: Rebuild subtree reordering.

--------------------------------------------------

Due to tactic or context modifications proof structure may change.
In particular, improving Auto can reduce the number of subgoals of
a proof step. Rebuild can automatically repair such 
proofs by comparing a rebuild sugoal with the extant subtrees of 
the current proof and selecting the most appropriate subtree to 
apply to the subgoal.  

The method used to select the subtree is called rebuild_tactic_pick: 

rebuild_tactic_pick : term # term list -> int -> term -> term # term
  - first arg is list of tactic and subgoal pairs from original proof 
  - int is index of subgoal being rebuilt
  - term is current subgoal being rebuilt
  - return is tactic to be used and original subgoal
      * tac may differ from argument. 
      * subgoal must be identical to argument.
        it is used to identify the subtree to continue with after refinement
        with returned tactic.

The selection method is modifiable :    
set_rebuild_tactic_pick : term # term list -> int -> term -> term # term -> unit

The default selection is 
(\choices i g. 
   (find (\tac,goal. alpha_equal_terms g goal) choices)
   ? nth i choices
   ? hd choices)


These helper functions are available :

iinf_concl : term -> term
iinf_hyps : term -> bool # var # term list
iinf_num_hyps : term -> int
iinf_nth_hyp : int -> term -> bool # var # term
iinf_label : term -> token

⋅
--------------------------------------------------

Authors: NUPRL:t

⋅

Home