Mark Staples, University of Cambridge Computer Laboratory.
Window inference is a transformational style of reasoning which provides an intuitive framework for managing the transformation of sub-terms.
A term is transformed under (reflexive and transitive) relations within a window by appealing to transformation rules. Sub-terms are transformed using the same mechanism, with corresponding sub-windows maintained in a window stack. Opening rules justify the transformation of windows by the transformation of their sub-windows. Opening rules also provide additional contextual information which can be used in the transformation of sub-windows.
A simple window inference mechanism for Isabelle has been developed. It is based on Isabelle's subgoal package. It utilises Isabelle's meta-variables to effect sub-term rewriting, and Isabelle's meta-logic to elegantly represent transformation rules and opening rules.
The window inference style of reasoning is very similar to the standard presentation of program refinement (Back, Morris, Morgan) proofs. Because of this, window inference is gaining popularity as a basis for the construction of refinement tools in theorem provers -- refinement tools currently being constructed with the HOL and Ergo theorem provers are based on their window inference facilities.
However, the use of window inference for reasoning about program logics places new demands on the method, and especially on the notion of context. A more sophisticated window inference mechanism for Isabelle is being developed, which will support more complex notions of context, and will also provide more flexible facilities for the use of window inference as a basis for program refinement tools.