Subject: Fragments

Keywords: ::general

Title: Alpha generalized fragments

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

In an Alpha fragments all hyp id variable names are normalized
according to the bound occurences of the variables in the hyps.
Similarly the order of the hyps is normalized. Occasionally,
modifying the names or order causes the step to fail. 
By convention tactics success should not depend on hyp ids.
Thus in most cases a fragment which fails to generalize due to 
hyp id renaming is modified to reduce such dependency.
A fragment which fails to generalize due to hyp order is more 
problemmatical. There is a deeply rooted algorithmic dependency
on hyp order of equality hyps that would be difficult to fix.
Thus instead the fragment is annotated and when used 
the sequent is reordered to match the fragment prior to tactic
application. 

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

Authors: 

Contributors: RICH:t

⋅

Home