10.6092/issn.1972-5787/6298
The use of a functional language to implement proof strategies as proof tactics in interactive theorem provers, often provides short, concise and elegant implementations. Whilst being elegant, the use of higher order features and combinator languages often results in a very procedural view of a strategy, which may deviate significantly from the high-level ideas behind it. This can make a tactic hard to understand and hence difficult to to debug and maintain for experts and non-experts alike: one often has to tear apart complex combinations of lower level tactics manually in order to analyse a failure in the overall strategy.In an industrial technology transfer project, we have been working on porting a very large and complex proof tactic into PSGraph, a graphical language for representing proof strategies. The goal of this work is to improve understandability and maintainability of tactics. Motivated by some initial successes with this, we here extend PSGraph with additional features for development and debugging. Through the re-implementation and refactoring of several existing tactics, we demonstrates the advantages of PSGraph compared with a typical sentential tactic language with respect to debugging, readability and maintenance. In order to act as guidance for others, we give a fairly detailed comparison of the user experience with the two approaches. The paper is supported by a web page providing further details about the implementation as well as interactive illustrations of the examples.
application/pdf
1972-5787
6298
2
en
Rob Arthan
Journal of Formalized Reasoning
graphical tactic language
Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
Text.Serial.Journal
https://jfr.unibo.it/
9
Articles
2016-12-15
2016-08-22
2016-12-01
2017-09-04
69-130
JFR
Rob Arthan
2016/12/15
10.6092/issn.1972-5787/6298
69
Lemma1, UK
1972-5787
2
graphical tactic language
en
130
Iain Whiteside. Refactoring Proofs. PhD thesis, University of Edinburgh, 2013. 50
Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
https://jfr.unibo.it/article/download/6298/6286
9
Understanding and maintaining tactics graphically
OR how we are learning that a diagram can be worth
more than 10K LoC
Yuhui Lin, Gudmund Grov
Heriot-Watt University, UK
and
Rob Arthan
Lemma1, UK


The use of a functional language to implement proof strategies as proof tactics in interactive
theorem provers, often provides short, concise and elegant implementations. Whilst being elegant,
the use of higher order features and combinator languages often results in a very procedural view
of a strategy, which may deviate significantly from the high-level ideas behind it. This can make a
tactic hard to understand and hence difficult to to debug and maintain for experts and non-experts
alike: one often has to tear apart complex combinations of lower level tactics manually in order
to analyse a failure in the overall strategy.
   In an industrial technology transfer project, we have been working on porting a very large
and complex proof tactic into PSGraph, a graphical language for representing proof strategies,
supported by the Tinker tool. The goal of this work is to improve understandability and main-
tainability of tactics. Motivated by some initial successes with this, we here extend PSGraph with
additional features for development and debugging. Through the re-implementation and refac-
toring of several existing tactics, we demonstrates the advantages of PSGraph compared with a
typical linear (term-based) tactic language with respect to debugging, readability and mainte-
nance. In order to act as guidance for others, we give a fairly detailed comparison of the user
experience with the two approaches. The paper is supported by a web page providing further
details about the implementation as well as interactive illustrations of the examples.




1.   INTRODUCTION
Proof tactics have played an important role in reducing user interaction and proof
development time for interactive theorem provers. However, tactics tend to be dif-
ficult to debug and maintain: (1) they may not fail outright and instead generate
undesirable subgoals; (2) each layer of a (reasonably) large and powerful (hierar-
chically composed) tactic may involve search which makes it hard to identify why
it failed and where the culprit for the failure resides.
   We will illustrate the maintenance issue with an industrial example: D-RisQ

This work has been predominantly supported by EPSRC platform grants EP/J001058 and
EP/N014758 and IAA grant EP/K503915. The second author is supported by a SICSA industrial
fellowship and the first author by EPSRC grant EP/M018407. The development of PSGraph
was started in the AI4FM EPSRC grant (EP/H023852 and EP/H024204). We would also like to
thank D-RisQ, in particular Colin O’Halloran and Priiya G, for excellent discussions. We would
also like to thank the anonymous reviewers for the suggested improvements to the paper.




                                       Journal of Formalized Reasoning Vol. 9, No. 2, 2016, Pages 69–130.
70     ·     Lin, Grov and Arthan

Software Systems1 deploys a very powerful tactic to automate formal proofs of
correctness of code auto-generated from Simulink models [47]. This tactic has been
developed over a number of years and now constitutes around 10K lines of dense
ML code (50K LoC if scripts to prove supporting lemmas are included). Both a
high degree of automation and ease of maintenance is crucial for D-RisQ’s business
model: when a conjecture fails a developer must have an efficient way of finding
and fixing the problem. The tactic must be intuitive to use and understand so
that, as personnel move on, new developers can take over maintenance and further
development. Proofs of low-level properties of automatically generated code are
not interesting in themselves: what is important is the ability to produce proofs
automatically as evidence that the code generator has not introduced bugs. To
support this, the tactic developers will want to exploit insights from one failed and
patched proof to increase the level of automation on other conjectures.
   Crucial to such debugging and refactoring of tactics is a suitable tactic represen-
tation. If one think of tactics as flow networks, where subgoals flow between tactics,
then there is evidence that the human brain finds it more natural to understand
such networks diagrammatically compared with linear (term-based) representations
[39]. Our PSGraph [26] language was designed to make proof strategies more intu-
itive to understand and easier to debug and change than is the case with existing
tactic languages. In PSGraph, the ‘flow graph’ view is followed literally and tactics
are represented as directed, typed and hierarchical graphs. Boxes are labelled by
(smaller) tactics and wire labels are used to direct subgoals as they ‘flow’ through
the graph. This flow can be inspected step-by-step when debugging a graph. The
PSGraph language is implemented in the Tinker tool [27, 44], which includes a
graphical user interface to support the development and analysis of PSGraphs.
The tool can support a range of theorem provers and has currently been instanti-
ated for Isabelle [27], Rodin [40] and ProofPower [4]. In this paper, we concentrate
on ProofPower, a system which is comparable with other provers in the HOL family
such as HOL4 [59], HOL Light [32] and Isabelle/HOL [45].
   Motivated by work with D-RisQ on their tactic in PSGraph [43], our main hy-
pothesis of this research is that
      understanding, debugging and maintaining2 proof strategies is easier
      with PSGraph than with traditional linear tactic languages.
The hypothesis relates to our overall research vision. We have already reported
some evidence for it in an industrial setting [43]. This paper has an exploratory
objective, where the goal is to study PSGraph’s relative strengths and weaknesses
with respect to our given hypothesis. The contributions of this paper are three-fold.
  The first contribution, discussed in §3, comprises recent extensions to PSGraph
and the Tinker tool, with new features to improve development and debugging.
The most notable extension is the introduction of a new language for specifying
wire labels.
1 http://www.drisq.com
2 Software maintainability refers to the ease in which a software system or component can be

modified or adapted to a changed environment [1]. This will naturally include both understanding
and debugging software. However, as the main loci is on these two aspects of maintainability, the
hypothesis is explicit about them.
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                            Understanding and maintaining tactics graphically        ·     71

   The second and, in our view, main contribution is found in §4, where we address
our hypothesis by means of three case studies, each with a distinctive flavour and
level of complexity. Evaluation based upon case-studies is motivated by the work
being exploratory and improvement-driven [57]; the aim is to identify actionable
limitations of PSGraph with respect to the hypothesis – and to provide the neces-
sary armoury to address D-RisQ’s tactic in full. We reflect on alternative evaluation
approaches in §5.
   To expose the differences between the user experience with the traditional linear
representation of proofs and proof procedures and the user experience with our
graphical representation, we work through several simple but instructive aspects of
the case studies in some detail. Our aim is to give a good understanding of what
goes on in the two approaches and to guide future work on and with PSGraph
by ourselves and others. This leads us to the third contribution of this paper: to
provide a tutorial-like introduction to PSGraph and how to go about connecting
Tinker to a theorem prover. To support this, we therefore provide a fairly detailed
background on ProofPower and PSGraph/Tinker in §2. Furthermore, §2.2.2 and
§2.2.3 are fully devoted to prover integration, while parts of §2.1 and §3.1 discuss
such integration. These parts can be skipped if desired. Some aspects of the case
studies are very detailed for the same reasons. However, space does not permit a
discussion of every detail and so particularly in the second case study, we have tried
to give the flavour of the bigger picture supported by enough information to help
interested readers find their way around the original source material.
   After the description of each case study, we reflect and analyse our approach
and provide recommendations which we hope can be used as a template for other
developments. Crucially, while two of the authors (Lin and Grov) are developers
of PSGraph, the third author (Arthan) had never used PSGraph before we started
this work. Arthan was the developer of the original version of the case studies.
   Our three case studies consider already extant proofs and proof procedures imple-
mented in ProofPower: they comprise (i) a proof procedure for tautologies supplied
as part of the standard proof infrastructure, (ii) some application-specific tactics
used to finesse a tricky lemma forming part of the proof of security properties of a
database system and (iii) a decision procedure taken from a collection of case stud-
ies on pure mathematics in ProofPower that automates problems such as proving
the continuity of real-valued functions.
   In §5 we discuss related work, and we conclude and discuss further work in §6.
Additional supporting materials, including animations of the examples and detailed
instructions are available from a dedicated webpage [42].

2.    BACKGROUND
2.1   ProofPower
ProofPower [4] is a suite of tools supporting specification and proof. At its heart is
an implementation in Standard ML of Mike Gordon’s HOL logic (the same logic as is
implemented in HOL4 [59] and HOL Light [32] and the core of the logic implemented
in Isabelle/HOL [45]). It is implemented in the well-known LCF style [24, 25]. In
this paper, we assume some familiarity with basic LCF concepts, but we will briefly
review how these concepts are realised in ProofPower. The purpose of this section

                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
72     ·      Lin, Grov and Arthan

is to provide a miniature primer on ProofPower and how it is implemented. This
is intended to give a feel for the user experience using and programming an LCF
style system in the traditional way for comparison with the Tinker approach. This
section also provides technical background for those interested in the details of how
Tinker is connected to the theorem prover. Readers familiar with some member of
the LCF family are invited to skip or skim this section on a first reading.
   Recall that in LCF terminology, the programming language used to implement
the system is referred to as the metalanguage (or ML) while the language of the
logic implemented by the system is referred to as the object language. ProofPower
is implemented as a large library of functions that are invoked from its metalan-
guage ProofPower-ML, which is the interactive functional programming language
Standard ML with extensions to support convenient entry of object language con-
structs. Object language terms are represented by an abstract data type TERM
with a constructor for each syntactic category in the object language. Values of
type TERM can be entered using object language concrete syntax enclosed in Quine
corners, ‘p’ and ‘q’. So, for example, the following ML command line:
SML

val tm1 = p(λx•λf • f x) 1q;
causes the string of symbols between the Quine corners to be parsed and type-
checked resulting in a value of type TERM that is bound to the ML variable tm1.
(For customer-oriented reasons, the design of the concrete syntax for HOL in Proof-
Power was heavily influenced by the Z notation [60], hence the rather heavyweight
bullets in the λ-abstraction.)
   In the HOL logic, a theorem is a sequent φ1 , . . . , φn ` φ, asserting that, if the
hypotheses φ1 , . . . , φn hold, then so does the conclusion φ (here φ and the φi are
propositions, i.e., terms of type BOOL). Theorems are implemented as an abstract
data type THM with a constructor for each primitive inference rule schema of the
logic, parametrised by the antecedents of the rule schema and any other informa-
tion needed to instantiate the schema. For example, one primitive inference rule
schema is an axiom schema asserting that any β-redex is equal to its β-reduct.
It is implemented by a constructor simple β conv with a single parameter that
identifies the β-reduct. If (after executing the command above), we execute:
SML

val thm1 = simple β conv tm1 ;
the system responds with:
ProofPower Output

val thm1 = ` (λ x f • f x ) 1 = (λ f • f 1 ): THM
indicating that a value of type THM with the appropriate instance of the β-
reduction axiom as its conclusion has been bound to the ML variable thm. (Note
that the pretty-printer has used a short-hand form for the nested λ-abstraction, as
shall we in future examples.)
  The constructor asm rule implements the axiom schema containing all theorems
of the form φ ` φ and the constructor eq trans rule implements the rule schema
for transitivity of equality. Putting these together, if we execute:


Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                            Understanding and maintaining tactics graphically        ·     73

SML

val thm2 = eq trans rule (asm rule pH = (λx f •f x ) 1 q) thm1 ;
the system responds with
ProofPower Output

val thm2 = H = (λ x f • f x ) 1 ` H = (λ f • f 1 ): THM
   Typically, ProofPower users do not use the primitive inference rules directly, but
instead use derived proof procedures that operate at a higher-level. One widely
used abstraction supporting equational reasoning is the notion of conversion [51].
A conversion is a function of type TERM − > THM , which, by convention, when
passed a term t, returns a theorem with conclusion of the form t = t0 . The primitive
inference rule simple β conv discussed above is an example of a conversion, which
proves all theorems of the form ` (λx • t)u = t[u/x ]. Conversions are often
used to package various kinds of normal form. For example, the conversion anf
conv implements a normal form for natural number arithmetic expressions. If we
execute:
SML

val thm3 = anf conv p7 ∗(11 + x )∗(13 + y)q;
the system responds with:
ProofPower Output

val thm3 = ` 7 ∗ (11 + x ) ∗ (13 + y) =
       1001 + 91 ∗ x + 77 ∗ y + 7 ∗ x ∗ y: THM
   There is a heavily used family of conversions that work by rewriting with equa-
tional theorems such as the definitions of library functions:
SML

val thm4 = rewrite conv [map def , pair ops def ]
                      pMap Fst [(1 , 2 ); (3 , 4 ); (5 , 6 )]q;
Here map def and pair ops def refer to the theorems representing the definitions
of the Map combinator and the constructor (, ) and destructors Fst and Snd for
pairs. (The ProofPower syntax follows the old HOL tradition of using semi-colons
to separate the elements of lists.) This results in:
ProofPower Output

val thm4 = ` Map Fst [(1 , 2 ); (3 , 4 ); (5 , 6 )] = [1 ; 3 ; 5 ]: THM
  Many of the standard proof procedures provided in ProofPower are parametrised
by what is called a proof context: a named collection of standard transformations
to apply to a problem. The proof context allows the standard proof procedures
to be tailored to particular problem domains and proof techniques. Higher-order
functions are provided to allow proof procedures of various types to be executed in
a specified proof context. For example, the function PC C1 executes a function
returning a conversion in a specified proof context. Thus the following command
performs a single step of rewriting in the proof context sets ext designed for rea-
soning about sets using extensionality:



                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
74     ·      Lin, Grov and Arthan

SML

val thm5 = PC C1 "sets ext" once rewrite conv []
                    p{x | x < 20 } = {x | x ≤ 19 }q;

val thm5 = ` {x |x < 20 } = {x |x ≤ 19 } ⇔
              (∀ x • x ∈ {x |x < 20 } ⇔ x ∈ {x |x ≤ 19 }): THM
The following command rewrites in the proof context sets ext until no more rewrit-
ing is possible:
SML

val thm5 = PC C1 "sets ext" rewrite conv [] p{x | x < 20 } = {x | x ≤ 19 }q;
which reduces the problem to pure arithmetic:
ProofPower Output

val thm5 = ` {x |x < 20 } = {x |x ≤ 19 } ⇔ (∀ x • x < 20 ⇔ x ≤ 19 ): THM
  Conversions can be composed using the infix combinator THEN C. If we compose
rewriting in the proof context sets ext with rewriting in a proof context designed
to deal with linear natural number arithmetic the problem reduces to truth and we
can derive a proof of our original equation:
SML

val thm7 = (PC C1 "sets ext" rewrite conv [] THEN C
              PC C1 "lin arith" rewrite conv [])
                      p{x | x < 20 } = {x | x ≤ 19 }q;
val thm8 = ⇔ t elim thm7 ;
yielding:
ProofPower Output

val thm7 = ` {x |x < 20 } = {x |x ≤ 19 } ⇔ T : THM
val thm8 = ` {x |x < 20 } = {x |x ≤ 19 }: THM
  While forward proof using conversions and other inference rules gives a powerful
approach to programming proof procedures, a more natural and productive ap-
proach to finding proofs interactively is a goal-directed search, starting with the
assertion you wish to prove as the initial goal and transforming each goal into
subgoals that entail that the goal and are (hopefully) easier to prove. The trans-
formations are effected by what Milner christened tactics: ML functions that map
a goal to a pair comprising (i) the list of subgoals and (ii) a proof, i.e., a function
that will prove the goal given theorems validating the subgoals. As in other HOL
systems, goals in ProofPower comprise a list of assumptions and a conclusion, so
this simple but powerful idea is captured in the following type declarations:
           type GOAL          = TERM list ∗ TERM ;
           type PROOF         = THM list −> THM ;
           type TACTIC        = GOAL −> GOAL list ∗ PROOF ;
For example, consider the goal: ([], p1 < 2 ∧ 2 < 3 q )(with an empty list of as-
sumptions). A tactic (namely ∧ tac) might reduce this goal to:
           ([([], p1 < 2 q) , ([], p2 < 3 q)],
                     fn [th1 , th2 ] => ∧ intro th1 th2 ) : GOAL list ∗ PROOF

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                            Understanding and maintaining tactics graphically        ·     75

I.e., it gives us two subgoals with conclusions 1 < 2 and 2 < 3 respectively, together
with a function, which, given a list comprising two theorems that validate these
subgoals, will use ∧-introduction to return a theorem validating our original goal.
   This approach to interactive proof was supported from the earliest days of LCF
(see [25] for the history) and came into its own when Paulson implemented the first
interactive package for managing the subgoal state during the user’s search for a
combination of tactics that will prove their goal.
   In the ProofPower subgoal package, the goal with assumptions t1 , . . . , tn and
conclusion t is internally represented as a single term that is logically equivalent
to the universal closure of t1 ∧ . . . ∧ tn ⇒ t. The logical state of the proof search
is captured in a theorem whose conclusion represents the original goal and whose
assumptions represent the outstanding subgoals. When a tactic is applied to a goal,
the corresponding assumption is replaced by terms representing the list of subgoals
returned by the tactic. Assumptions are labelled by dot-separated lists of natural
numbers, representing a position in a tree whose root corresponds to the original
goal and whose nodes correspond to tactic applications which result in more than
one subgoal. In any state there is a current subgoal that tactics are applied to.
A function set labelled goal is provided to allow the user to navigate around the
outstanding subgoals.
   A session with the subgoal package may be initiated with the set goal command:
SML

set goal ([], p∀x • (1 , x ) ∈ {(a, b) | a = 1 ∨ b ≥ 2 } ∧ (x ≥ 3 ∨ x ≤ 4 )q);
The system responds by printing out the state of the proof search. There is 1 goal
and its label is the empty string:
ProofPower Output

Now 1 goal on the main goal stack

(∗ ∗∗∗ Goal "" ∗∗∗ ∗)

(∗ ?` ∗)p∀ x • (1 , x ) ∈ {(a, b)|a = 1 ∨ b ≥ 2 } ∧ (x ≥ 3 ∨ x ≤ 4 )q
Here the symbol ? ` is used in the display of a goal as indicative of a sequent that
has not yet been proved. It is included as an ML comment to facilitate copying
and pasting the output as executable code in an ML script.
  At this point, we have several choices about the tactic to apply. If we want to
take a fine-grained approach, we could apply tactics that exactly match the outer
two layers of the logical structure:
SML

a(∀ tac THEN ∧ tac);
Here T HEN is a tactical, i.e., an operator that constructs new tactics from old, in
this case by a form of sequential composition. This results in:




                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
76     ·      Lin, Grov and Arthan

ProofPower Output

Tactic produced 2 subgoals:

(∗ ∗∗∗ Goal "2 " ∗∗∗ ∗)

(∗ ?` ∗)px ≥ 3 ∨ x ≤ 4 q


(∗ ∗∗∗ Goal "1 " ∗∗∗ ∗)

(∗ ?` ∗)p(1 , x ) ∈ {(a, b)|a = 1 ∨ b ≥ 2 }q
  Alternatively, we could repeatedly apply the general purpose tactic strip tac
which applies a standard simplification to logical connectives if possible and proof
context-dependent transformations to atomic formulas. The following command
does this after undoing what we have just done:
SML

undo 1 ; a(REPEAT strip tac);
ProofPower Output

Tactic produced 2 subgoals:

(∗ ∗∗∗ Goal "2 " ∗∗∗ ∗)

(∗ 1 ∗)p¬ x ≥ 3 q

(∗ ?` ∗)px ≤ 4 q


(∗ ∗∗∗ Goal "1 " ∗∗∗ ∗)

(∗ ?` ∗)p(1 , x ) ∈ {(a, b)|a = 1 ∨ b ≥ 2 }q
Note how in goal 2, the disjunction has been dealt with by asking us to prove its
right-hand side on the assumption that its left-hand side is false. (The assumptions
are displayed above the conclusion of the goals with numbers in ML comments to
identify them. In this case there is just one assumption.) Let us assume that this
is not quite what we wanted; so we undo it and try again but only stripping off two
layers of connective:
SML

undo 1 ; a (strip tac THEN strip tac);
This gives us:




Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                           Understanding and maintaining tactics graphically        ·     77

ProofPower Output

Tactic produced 2 subgoals:

(∗ ∗∗∗ Goal "2 " ∗∗∗ ∗)

(∗ ?` ∗)px ≥ 3 ∨ x ≤ 4 q


(∗ ∗∗∗ Goal "1 " ∗∗∗ ∗)

(∗ ?` ∗)p(1 , x ) ∈ {(a, b)|a = 1 ∨ b ≥ 2 }q
   Looking at goal 1, we see it should become trivial once the set notation has been
eliminated using standard properties of set comprehensions and pairs. So iterating
strip tac should do just what we want in the sets ext proof context. To do this we
use the tactical PC T1 , which does for tactics what PC C1 , discussed above, does
for conversions:
SML

a(PC T1 "sets ext" REPEAT strip tac);
which results in:
ProofPower Output

Tactic produced 0 subgoals:
Current goal achieved , next goal is:

(∗ ∗∗∗ Goal "2 " ∗∗∗ ∗)

(∗ ?` ∗)px ≥ 3 ∨ x ≤ 4 q
  We recognise that this problem is entirely in the domain of linear natural num-
ber arithmetic. The proof context lin arith for this domain includes a decision
procedure that we can access via a generic tactic prove tac:
SML

a(PC T1 "lin arith" prove tac[]);
This completes the proof search:
ProofPower Output

Tactic produced 0 subgoals:
Current and main goal achieved
We can now extract our theorem from the subgoal package:
SML

val thm9 = pop thm();
ProofPower Output

Now 0 goals on the main goal stack
val thm9 = ` ∀ x • (1 , x ) ∈ {(a, b)|a = 1 ∨ b ≥ 2 } ∧ (x ≥ 3 ∨ x ≤ 4 ): THM



                                         Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
78     ·     Lin, Grov and Arthan

                            ···              ···          ···
                                             OR/ORELSE

                          TT(Args)
                            (Args)         TT(Args)
                                             (Args)                  G
                            ···                           ···
                                             ···

                      atomic tactic     graph tactic identity tactic goal

                           Fig. 1.    Types of graph nodes for PSGraph

2.2   PSGraph
In PSGraph, tactics are represented as directed, typed, hierarchical and open
graphs. A graph consists of boxes, representing “processes” and typed (labelled)
wires that connect them together. A process box is labelled by a tactic, which can
either be an existing ProofPower tactic or another graph, where the latter intro-
duces hierarchies. The graphs are open in that wires need not be connected to a
box at both ends, but can be left open to represent graph inputs and graph outputs.
Evaluation is achieved by adding input goals to a graph input wire. The goals will
then flow through the graph; each step will apply a tactic to an incoming goal,
consume the goal, and add the resulting subgoals to its output wires. This process
will continue until all subgoals appear on the graph output wires. These subgoals
will then be returned. All wires are labelled by goal types, which are predicates on
a goal that are used to direct goals to the correct tactic.
   Fig. 1 shows the types of boxes that can appear in a PSGraph. An atomic tactic
is an existing ProofPower tactic, possibly parametrised. A parameter could for
example be the name of a rewrite rule to apply or a term used to instantiate a
variable. Note that if the list of parameters (Args) is empty, then we can write T
instead of T (). A graph tactic is labelled by a named graph, which we can look
up. For graph tactics, the arguments (Args) relate to the scope of the variables
of the goal node environment, which we return to in §3.1. An identity tactic is
used to split and merge multiple wires and, as discussed below, will not have any
side-effects on the proof state or goal nodes. The final type of box is a goal. This
is only used for evaluation and cannot be added to a PSGraph by the user. It
contains sufficient information to evaluate and link to the ProofPower proof state,
including:
—the name given by ProofPower for the goal;
—the internal representation of the goal in ProofPower; and
—an environment that is used to support variables in the graph, which is discussed
 in detail in §3.1.
When displaying the goals, we will only show the name (see e.g. Fig. 4). We return
to goals when discussing evaluation below.
   Finally, the wires are labelled by goal types, which are predicates defined on goals.
Intuitively, these provide information about some characteristics, such as “shape”,
of a goal, which are used to influence the path a goal takes as it passes through the
graph. We develop a language for expressing these in §3.2, and defer the details to
that section.
   A simple but complete example of a PSGraph is given in Fig. 2. This is a
PSGraph encoding of the proof discussed in §2.1. The input wire is labelled by

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                                           Understanding and maintaining tactics graphically                        ·        79

                                                 c(forall)
                                                             c(conj)
                                                  ∀_tac             ∧_tac

                                                              any


                                                is_sets()                     is_arith()

                                                PC_T1 "sets_ext" REPEAT strip_tac


                                                       PC_T1 "lin_arith" prove_tac []

                      Fig. 2.     A PSGraph encoding of the proof discussed in §2.1


            hdefs,atomsi ` h10 : H1 · · · hdefs,atomsi ` h1m : H1
                                                                                                                        
                                                                                                                        
                                                 ..
          
                                                                                                                        
                                                                                                                         
          
                                                                                                                        
                                                                                                                         
          
          
          
                                                 .                                                                      
                                                                                                                         
                                                                                                                         
                                                                                                                         
            hdefs,atomsi ` hn0 : Hn · · · hdefs,atomsi ` hnk : Hn                                  hdefs,atomsi ` g : G 
          
                                                                                                                        
          
                                                                                                                        
                                                                                                                         
             ([h10 , · · · , hn0 , · · · , hn0 , · · · , hnk ], ) = T (Args) g
          
                                                                                                                        
                                                                                                                         
                                                                                                                        
                                                                                                                 ... ...
                                                                                                                        
                                                                                                 ...    ...
          
                                                                                                                        
                                                                                                                         
          
                                   G
                                    G
                                                                                                                         
                                                                                                                         
          
                                                                                                    gg                  
                                                                                                                         
                            · · · gg · · ·
                                                                                                                        
          
          
                                                            ··· G ···                                                   
                                                                                                                         
                                                                                                                         
          
                                   G
                                    G                                                                       ,→       G
                                                                                                                     G
                                                                                                                         
                                                                                                                         
Reval =                                                                                    ,                  ...   gg ...
                             TT(Args)
                                (Args)
                               T(Args)                             TT(Args)
                                                                     (Args)
                                                                    T(Args)                      ... G ...
                                                                                                                             
                                                                                                     G
                                                                                                                            
                                                                                                                      G
                                                                                                                            
                                                                                                                      G
                                                                                                                            
                                                 ,→
                                                                                                                            
          
          
                                                            H11
                                                             H         ···     H
                                                                               Hnn
                                                                                                                             
                                                                                                                             
                                                                                                                             
                                                                 h10         hn0
                                                                                                                            
          
                                                                 l0          n0                                             
                                                                                                                             
                                                                                                                            
                                                                  .           ..
                                                                                                                            
                                ···                          H11 ..
                                                                                                                            
                        H
                        H11              HHnn                H                 .HHnn
          
                                                                                                                            
                                                                                                                             
          
                                                                                                                            
                                                                                                                             
                                                                                                                            
                                                                             hnk
                                                                                                                            
          
                                                               h1m
                                                                 lm           nk
                                                                                                                             
                                                                                                                             
                                                                               H
                                                                                                                            
          
          
                                                            H
                                                             H11               Hnn                                           
                                                                                                                             
                                                                                                                             
          
                                                                                                                            
                                                                                                                             
                                                                                                                            


                                           Fig. 3.      Evaluation of PSGraph.

c(f orall) which means that the conclusion (c) must be a universal quantifier. The
∀ tac tactic is applied to it followed by the ∧ tac tactic, as long as the conclusion of
the goal is a conjunction. The any goal type always succeeds. The identity tactic
is then used to separate the goals that are arithmetic (is arith) from those that
are set theoretic (is sets), where the suitable tactic is applied in both instances.
  2.2.1 Evaluation. In order to initialise the evaluation (i.e. proof of) of a subgoal
by a PSGraph, a ProofPower goal must be provided. This is achieved by calling top
goal(), which will provide the first subgoal from the ProofPower subgoal package.
From this subgoal, a goal node with an empty environment is created, and added
to a graph input wire where the goal type is satisfied. A step of the proof will apply
a tactic box to a goal that is on an input wire. Each generated subgoal (if any)
will be added to an output wire where the goal type is satisfied. This process will
continue until termination:
  Definition (Termination). A graph has terminated, if for all goals g of the
graph, g is either on a graph output wire or it is wired to another goal.
  It follows by induction over the number of goals present that all goals are (directly
or indirectly) on graph output wires.

                                                                       Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
80       ·   Lin, Grov and Arthan

  It is worth noting that (as with other tactic languages) termination is not guar-
anteed. One example of non-termination is that an atomic tactic from the theorem
prover may not terminate; another example is a PSGraph that contains a non-
terminating loop, e.g. as a result of rewriting in presence of commutative operators.
  As the proof state is handled by ProofPower’s subgoal package, evaluation is only
concerned with how the subgoals “flow” from the graph input to the graph output
wires. Two properties are crucial for a successful evaluation step:
—No subgoals are lost, that is if a tactic produces a subgoal then it will appear on
 the graph.
—No subgoals are duplicated in the graph.
   At the graph level, evaluation is achieved by graphical rewriting, where l ,→ r
is a rule that rewrites l to r3 . Fig. 3 gives the set Reval of rewrite rules used to
evaluate a PSGraph. We use a notation where side-conditions are above the line
and the rewrite is below the line. Each rule is non-deterministic in the sense that
there may be several ways to apply it in a given situation. Evaluation of a graph is
achieved by applying rules from Reval repeatedly until no rules are applicable. At
this point evaluation have either failed or successfully terminated.
   The simplest case is the identity box, shown rightmost in Fig. 3. Here, the input
goal and the output goal is the same as the node is essentially used to fork the goal
to the correct target box. hdefs,atomsi ` g : G is a predicate that holds if goal g
satisfies goal type G. The ellipses illustrate that there could be other input and
output wires. Note that if there are more than one output wire where g satisfies
the goal type then there will be multiple rewrites. Each of these rewrites will be a
separate branch of the search space. We will return to the goal type predicate in
§3.2.
   The leftmost rule of Fig. 3 shows the evaluation of an atomic or graph tactic.
For an atomic tactic, T (Args) g is the result of applying the tactic (in ProofPower).
This is described in §2.2.3. For a graph tactic, this is the result of evaluating the
nested graph as discussed below. For these tactics, there will be a side-effect on
the proof state, which we return to in §2.2.3. The case when T (Args) is an atomic
tactic can be summarised as follows:
(1) Apply tactic T (Args) to obtain a list of subgoal nodes.
(2) Consume g from the graph.
(3) Add all valid combination of the resulting subgoals to output wires.
  Fig. 4 illustrates some of the steps of the flow through the proof strategy of Fig. 2
applied to the example of §2.1. In the left-most graph, g holds the initial goal:
(∗ ?` ∗)p∀ x • (1 , x ) ∈ {(a, b)|a = 1 ∨ b ≥ 2 } ∧ (x ≥ 3 ∨ x ≤ 4 )q
  It then applies Reval twice, which will first apply universal introduction followed
by conjunction introduction, introducing two new subgoals, h1:
(∗ ?` ∗)p(1 , x ) ∈ {(a, b)|a = 1 ∨ b ≥ 2 }q

3 When applied to a graph, this rule will match l with a subgraph and replace this with r. For
more details see [17, 18].
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                                              Understanding and maintaining tactics graphically                                  ·           81
                                                      c(forall)
                                                                  c(conj)                            c(forall)
      g c(forall)                                      ∀_tac             ∧_tac                                   c(conj)
         c(conj)                                                                                      ∀_tac             ∧_tac
   ∀_tac        ∧_tac                                                   h1
                                                                                                                 any
             any                                                        h2
                                                                  any
                                              2                                               2                                 h2
                                                                                                  is_sets()      h1
 is_sets()                                                                                                                      is_arith()
                            is_arith()              is_sets()
                                                                                 is_arith()
                                                                                                   PC_T1 "sets_ext" REPEAT strip_tac
 PC_T1 "sets_ext" REPEAT strip_tac
                                                    PC_T1 "sets_ext" REPEAT strip_tac
                                                                                                              PC_T1 "lin_arith" prove_tac
         PC_T1 "lin_arith" prove_tac []                    PC_T1 "lin_arith" prove_tac []



                                          Fig. 4.   Example evaluation of PSGraph.

and h2:
(∗ ?` ∗)px ≥ 3 ∨ x ≤ 4 q
Next it applies the identity tactic to h2 and then h1, with the result shown in
the right-most graph. This is used to route the goals to the correct tactic to
complete the proof. h1 is set-theoretic and thus goes down the left branch while
h2 is arithmetic and follows the right branch. Note that when there are multiple
goals, as in the right most graph, the order in which goals are evaluated will have
no impact on the end result4 .
  When T in the leftmost rule of Fig. 3 is a graph tactic, the arguments Args of
T are used to introduce local scoping: any variable not in Args is “fresh” in the
nested scope and will not have global effect. The evaluation can be summarised as:
(1) Consume g from the graph.
(2) Lookup the graph G which T points to.
(3) Constrain the environment of g to variables in Args and add this to an input
    wire of G (such that the goal type is satisfied). If there are multiple satisfying
    input wires, then one branch will be generated for each.
(4) Evaluate G until termination.
(5) Add all valid combination of the goals on the output wires of G to the output
    wires of the graph tactic T .
If any steps fail then evaluation of this node fails. Note that when adding a resulting
subgoal to the output of T in the last step, the subgoal will be given the environment
of g, with values of Args replaced by those in the resulting subgoal. We will return
to how this works in §3.1, after introducing environments more formally.
   To illustrate how a graph tactic is evaluated, consider the PSGraph in Fig. 5.
It contains a graph tactic conj imp, with two input wires and one output wire.
The input wires require that the conclusion of the a goal is either an implication
(c(implies)) or a conjunction (c(conj)). The output must have an hypothesis that
is the same as the conclusion. It is then proven by assumption by concl in asms
tac.
4 This would not have been the case in presence of shared meta-variables between goals, a feature
that is not currently supported in either ProofPower’s subgoal package or PSGraph.


                                                                        Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
82         ·       Lin, Grov and Arthan
                                                                                   any


                                       c(implies)          c(conj)             c(conj)    c(implies)

                                              conj_imp                      ∧_tac
                                                                                   c(implies)
                                            has_hyp(concl)              !c(implies)
                                                                                strip_ _concl_tac
                                        concl_in_asms_tac
                                                                                               any



                                  Fig. 5.      Example PSGraph with graph tactic.

                                        c(implies)        c(conj)                    c(implies)      c(conj)
                                                      `
                                                  B B∧(A A)                                    any                  c(implies)    c(conj)
                                              g
      `
     B B∧(A A)                                    any
                   g                                                                     c(conj)                         conj_imp
     c(implies)                                                                                       c(implies)
                       c(conj)
                                            c(conj)        c(implies)
            conj_imp
                                                                                         ∧_tac                           `has_hyp(concl)
                                          ∧_tac                            3                  c(implies)               B B   h1
                                                                                   !c(implies)
           has_hyp(concl)                        c(implies)                                                                            `
                                      !c(implies)                                         strip_ _concl_tac
                                                                                                                             h2   B, A A
                                                                                          `                    `
                                             strip_ _concl_tac                      h1   B B
      concl_in_asms_tac                                                                              h2 B, A A
                                                            any
                                                                                                                    concl_in_asms_tac
                                                      has_hyp(concl)                               has_hyp(concl)

                                       concl_in_asms_tac                            concl_in_asms_tac




                            Fig. 6.   Example evaluation of graph tactic in PSGraph.

   The graph nested by conj imp is shown in the red stippled box of Fig. 5 (right).
Depending on the input goal, it will either break up the conjunction or the disjunc-
tion, and in the former case, it may also be followed by breaking up a disjunction.
In order to illustrate several aspects of evaluation, the number of input/output
wires of the nested graph, and their goal types, deviates from the parent conj imp
graph tactic.
   Consider Fig. 6, which shows the key evaluation steps for a goal g:
(∗ 1 ∗)pB q
(∗ ?` ∗)pB ∧ (A ⇒ A)q
applied to one of the input wires of the graph of Fig. 5.
  In the first step, this goal is consumed from the parent graph and added to
one of the input wires of the nested graph. Note that for evaluation there is no
correspondence between the input wires of the parent box (in this case labelled
by c(conj)), and the input wire of the nested graph (here any). The goal g is
simply added to any input wire of the nested graph where the goal type holds (with
a separate branch in the search space for each such wire). In this case there is
only one possibility. It will then go through three steps of evaluation of the nested
graph, and at the end there are two goals, h1 and h2, on the output wires of the
nested graph. According to the definition of termination, the graph tactic has now
terminated. The (nested) graph will then “return” the list of goals [h1, h2]5 . These
are then added to the output wires where the goal type is satisfied, as the case

5 The     order of the goals returned is irrelevant.

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                             Understanding and maintaining tactics graphically              ·     83


                                    ProofPower                  PP_Tinker
                                                                TP config
                                   Tinker GUI        JSON
                                                                Tinker core
                                     Scala                      Poly/ML

                               Fig. 7.   Tinker architecture.

is for an atomic tactic. In this case, both matches the goal type of conj imp’s
output wire (has hyp(concl)) since the conclusion is found in the list of hypothesis.
Again, note that there is no relationship between the goal types of the output wires
of the nested graph (!c(implies and any), and those of the nesting graph tactic
(has hyp(concl)). The concl in assms tac tactic will then discharge both h1 and
h2 by assumption.
   2.2.2 Architecture & GUI of the Tinker tool. The Tinker tool [27, 44] imple-
ments PSGraph with support for the Isabelle, Rodin and ProofPower theorem
provers. Here, we will focus on the ProofPower version only. Tinker consists of
two parts: the CORE and the GUI. These are shaded in separate boxes in Fig. 7.
The core implements the main functions of Tinker. Most of the functions are im-
plemented using ML functors to achieve theorem prover independence. In order
to connect a theorem prover to Tinker, and use its GUI and basic functionality,
a ML structure that implements a provided ML signature called PROVER has to
be provided. This will enable basic usage of Tinker and the GUI. In Fig. 7 the
structure implementing this signature is called PP Tinker.
   Note that our ambition is not to replace the existing tactic language, but to
offer a different view of tactics. Tinker is designed to support a dynamic interplay
between a PSGraph and the existing tactic language, where the level of atomicity
of the atomic tactics used in PSGraph is flexible. This enables developers to decide
themselves which parts are best to express in PSGraph and which are not.
   The remaining of this subsection, as well as the next subsection, are intended for
readers interested in the details of how Tinker connects to theorem provers. Other
re.
   The PROVER signature includes both the types and functions required. It has
to know how types, terms, theorems and contexts are represented:
type   typ
type   term
type   thm
type   context
To illustrate, in ProofPower these are instantiated to:
type   typ = TYPE
type   term = TERM
type   thm = THM
type   context = string list ∗ string
   The CORE communicates with the GUI (written in Scala) over a JSON socket
protocol, which requires serialisation functions for some of this types (via strings),
e.g.:
                                                 Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
84     ·      Lin, Grov and Arthan

val trm of string : context −> string −> term
val string of trm : context −> term −> string
  The GUI allows users to develop proof strategies in a mostly graphical approach,
and to debug proof strategies with controlled interactive inspections.



                                                  2
                                                       3
                                                                                         5
                          1


                                                         4
                                                                                       6

       1: Library panel         2: Hierarchy utilities               5: Hierarchical node inspector
                                3: Drawing and evaluation controls   6: Information panel
                                4: Graph panel

                                  Fig. 8.   The Tinker GUI [44].


   Fig. 8 shows the components of the GUI. The graph panel is the main area where
users view and edit the graph of current proof strategies. With the interactive
options in the drawing and evaluation control panel, users can develop graphs in
a click and drag style, and step through evaluation with controls such as step
over a graph tactic. When a user selects a node or edge in the graph panel, the
detail information of the node or edge will be showed in the information panel.
To facilitate developing hierarchical graphs, the hierarchical node inspector panel
allows users to preview the sub-graphs of a graph tactic; and the hierarchy utility
panel shows the depth and path of the graph in the graph panel. For reusing
existing proof strategies, there is also a library panel to preview existing PSGraphs,
and import them to the graph panel. The core is implemented on top of the
Quantomatic graphical rewrite system [36]. Videos of interaction with the different
features of the GUI are available from [42].
   Tinker also needs to know about tactics and their execution, also provided via
implementation of the PROVER signature:
type tactic
Tinker uses the underlying prover’s proof state and goal representation augmented
with some additional book-keeping information represented in the following ML
types:


Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                            Understanding and maintaining tactics graphically        ·     85

type pplan
type pnode
The proof state (type pplan) is mainly used to link with the proof state of the
theorem prover and keep track of the goals that are “active” in the PSGraph. To
illustrate, in ProofPower this is a record where the main fields are the underlying
goal state of ProofPower and the goals that the PSGraph are allowed to work on:
type pplan = {gstate: GOAL STATE , opengs : pnode table, ...}
The type pnode table is a map from a string to a pnode. The key fields of the goal
representation (pnode) are the name of the goal, its internal representation and an
environment:
type pnode = {pname : string, g: GOAL, env : env , ...}
The Tinker representation of a tactic uses these types, and therefore has type:
type appf = pnode ∗ pplan −> (pnode list ∗ pplan) Seq.seq
To be used in Tinker, the underlying prover’s tactics (i.e. functions of type tactic)
have to be “lifted” to application functions with the above type appf.
   2.2.3 Tactic “lifting”. An atomic tactic T (Args) encapsulates a tactic of the
underlying theorem prover, i.e., ProofPower for the purposes of the present paper.
Recall from §2.1 that a ProofPower tactic maps a goal to a pair of new subgoals and
a validation function. PSGraph uses ProofPower’s existing package for handling the
subgoal state, meaning we can ignore the validation function at this level. We write
                                 (gs, ) = T (Args) g
to denote that T (Args) returns the list of subgoals gs when applied to g.
   We need to be able to connect ProofPower tactics, which works on goals, to our
atomic tactic boxes, which works on goal nodes (i.e. type pnode). The simplest case
is when there are no arguments, which we can just write T . All the atomic tactics
of Fig. 2 are examples of this case. Here, the label of the atomic box, e.g. PC T1
”lin arith” prove tac[], is wrapped into a function that will take a goal node and
produce a list of new goal nodes as follows. It will extract the goal name from the
input goal node and set this to be the top goal in ProofPower’s goal stack, using a
ProofPower function called set labelled goal. It will then apply the wrapped tactic
(to the goal at the top of the stack), and finally it will put each goal name and goal
into a goal node, together with the environment of the input node. We call this
process “lifting” of the ProofPower tactic to PSGraph.
   As there are no arguments, the string of the atomic tactic box is simply parsed as
ML code and applied. Such parsing has to be provided in the PROVER signature:
val exec str : string −> unit
This is a generic parser interface, which is also used for other parsing tasks. Inter-
nally, Tinker provides functionality to cast it to the correct type after some minor
user configurations. For tactics, it will cast it to the type tactic. The “lifting” into
the appf type is trivial.


                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
86       ·      Lin, Grov and Arthan

  When there are arguments, then we need to manually provide some ML code for
this6 . To illustrate, consider the ProofPower tactic prove tac discussed above. We
would like to parameterise over the proof context, which we can do by providing
the name of a proof context as a parameter:
fun prove with ctxt0 ctxt = PC T1 ctxt prove tac [];
  However, this will not work in PSGraph. In order to use such parametrised
tactics, the function needs to have a different type. Internally, the arguments of an
atomic tactic are represented using a deep embedding, i.e. as a list of an inductive
datatype with a constructor for each type:
datatype arg data = A Trms of term list | A Var of string | A Str of string | ···
   Arguments must be passed as a list of arg data, and such arguments have to be
reflected in the tactic type of PROVER; for ProofPower it is7 :
type tactic = arg data list −> TACTIC
  With this type, the signature has to be provided an interpretation of tactics in
terms of the defined application function (type apps):
val apply tactic : arg data list −> tactic −> appf
  Returning to our example, we represent the context as a string, so we provide
the following “lifting” function:
fun prove with ctxt [A Str ctxt] = PC T1 ctxt prove tac []
  | prove with ctxt = fail tac;
   As a result, prove with ctxt(A Str lin arith) will apply this function, with lin
arith parsed as a string.
   We will introduce a new type of tactic in §3.1, while §4 contains many examples
of tactics with and without arguments.

3.      A (MOSTLY) GRAPHICAL DEVELOPMENT & DEBUGGING FRAMEWORK
In §4 we will showcase PSGraph and the Tinker tool by developing, debugging and
refactoring several case studies adapted from the existing ProofPower developments.
To support this we first extend PSGraph and Tinker with new features.
   In §3.1 and §3.2 we add features that are mainly beneficial for development:
in §3.1 we introduce a new family of tactics used to exchange information and
constraints between tactics and goal types; while in §3.2 we develop a goal type
that allows us to hide low-level details in the graphs to improve readability.
   In §3.3 and §3.4 we develop support for debugging: §3.3 introduces breakpoints to
PSGraph, while §3.4 describes a simple, yet useful, logging mechanism for Tinker.
3.1      “Environment” tactics
Recall that the type of a tactic is from a goal to a pair consisting of a list of new
subgoals and a validation function. In an atomic tactic box, such tactic is then

6 We    hope to introduce some level of automation for this process in the future.
7 For   example, Isabelle in addition needs the context and the index of the subgoal as arguments.


Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                                Understanding and maintaining tactics graphically          ·     87


                                                     h(implies)
                                        ENV_top_symb_asm
                                       (hyps, "implies", ?asm)
                                                     any
                                       elim_⇒_asm_tac (?asm)
                                                     any

                          Fig. 9.   An example of “environment” tactic

“lifted” to work on the goal nodes that are in the graph. In addition to the actual
goal, such a goal node also contains an environment, which we introduce here:
  Definition (Environment). An environment Env is a function
                                         Var → EnvVal
where Var is a finite set of variables named by strings prefixed with a ‘?’ and EnvVal
is the disjoint union
                                       T ] N ] T∗ ] N∗
where T and N denote the set of all terms and names respectively, where a name is
an arbitrary uncapitalised string and X ∗ denotes the set of lists of elements of X 8 .
  The validity of a name depends on the context. For example, it could be a named
lemma, which will only be valid if that lemma exists. Two special names are: concl,
which refers to the conclusion of a given goal; and hyps, which refers to the (list of)
hypothesis of the goal.
  An environment is used to pass information between tactics and between tactics
and goal types. This could be to extract some information at one point in the proof
and use it later. For example, consider Fig. 9. Here, ENV top symb asm looks for
a hypothesis that starts with an implication, and binds it to a variable ?asm. In
the next atomic tactic, elim ⇒ asm tac will apply implication elimination to the
hypothesis that ?asm is bound to.
  Within graph tactics, local scoping of the environment is achieved by using the
arguments Args of the box. Recall the evaluation steps of graph tactics, as given
in §2.2.1. We are given a goal with an environment {?x 7→ v1 , ?y 7→ v2 } and a
graph tactic t(?x). When evaluating g for the graph t references, the environment
{?x 7→ v1 } is provided. Assume that on termination of t that a new goal g 0 has
the environment {?x 7→ v3 , ?z 7→ v4 }. This will return a goal g 0 with environment
{?x 7→ v3 , ?y 7→ v2 }. This illustrates how environments are constrains for “local
computation” within graph tactics.
  Now, the problem with ENV top symb asm, discussed above, is that it binds
?asm, meaning the result of applying it is a change to the environment, while
a “lifted” tactic will change the goal (and proof state) and cannot change the
environment. In this case, this issue could be overcome by combining these two

8 Note  that T and N are redundant as they can be represented as singleton sequences of T ∗ and
N ∗ , respectively. We find it more natural to separate them, as they are often treated differently
(e.g. some tactics only work on a single term). This will also simplify static checking, which we
plan to add in the future.

                                                Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
88     ·     Lin, Grov and Arthan

atomic tactics into a single ProofPower tactic. However, part of the reason to have
them as a separate boxes is to enable users to inspect the flow, and use Tinker’s
debugging features if a tactic application fails. By combining them into a single
tactic the granularity becomes too terse for such analysis. A second problem is that
there are more complex examples where there are tactic in between binding and
using a variable, which we will see examples of in §4. For these cases the solution
of merging boxes will not work.
   Instead we introduce a type of atomic tactic that works on the environment,
which we call environment tactics 9 :
   Definition (Environment tactic). An environment tactic, is an atomic tac-
tic, with a name prefixed by ‘ENV ’, whose underlying function is a function
                                           Env → Env∗
The rest of this section focuses on implementation issues of environments and en-
vironment tactics. This material is intended for readers interested in the technical
details of the connection between Tinker and a theorem prover. It can can be
skipped if desired. To support environment tactics, the PROVER signature is
augmented with new types for an environment and an environment tactic:
type env = env data table
type env tac
The type env data table is a map from a string to the type env data, which holds
the types an environment may contain
datatype env data = E Str of string | E Trm of term | ···
  As environment tactics may also have arguments (Args), they have a dual type
and application function to ProofPower tactics:
type env tac = arg data list −> env −> env list
val apply env tactic : arg data list −> env tac −> appf
From the types one can see that an environment tactic will not change the under-
lying proof state; it will only change the environment of a goal node (type pnode).
However, they may still require features of the provers, such as matching of terms.
   ENV top symb asm is an example of an environment tactic. As we can see from
Fig. 9, it takes three arguments: the first (hyps) is a list of terms, the second
(”implies”) is a string, and the third (?asm) is a variable. The underlying function
that has to be provided by the user will look something like:
fun ENV top symb asm [A Trms ts, A Str s, A Var var ] env = ···
  Note that Tinker will automatically lookup hyps, which is the list of hypothesis,
before calling this function. We will see many examples of environment tactics in
§4.

9 An alternative to environment tactics, is to bind variables during matching in goal types, which is
explained in §3.2. We have made a design decision to treat goal types as predicates, and therefore
to not support this. This is a deliberately compromise made in order to cleanly separate concerns
and to simplify the semantics of PSGraph composition (see [26]).

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                               Understanding and maintaining tactics graphically         ·     89

3.2   A constraint language to express goal types
Goal types are crucial in order to achieve maintainable proof strategies and to
reduce the search space. These are represented as constraints on the goal, and to
represent these, we develop goal types as a Prolog inspired constraint language.
Prolog is a natural starting point as constraints can be combined in an elegant and
declarative manner10 , and enables support for machine learning goal types using a
technique based upon logic-based learning [19]. Analogous to how graphs are used
to compose tactics, this language acts as a way of combining and re-using low-level
atomic constraints, which the underlying prover needs to provide. By supporting
recursive definitions, expressive constraints can be encoded, and lower-level details
can be hidden in the goal types appearing on the graphs.
   A relation may have (goal type) variables that are instantiated. This is discussed
below. However, a goal type appearing in a graph cannot have any such variables.
We therefore distinguish goal type schemas, which may have goal type variables,
from goal types, which does not allow the use of such variables:
   Definition (Goal type & goal type schema). A goal type schema (GTS)
is a predicate on a goal, defined by the following BNF:
                   GT S ::= C, GT S | C.            Oa ::= As | 
                     C ::= L | !L                   As ::= A | A, As
                      L ::= F (Oa)                   A ::= T | N | GVar
Following from Definition 2 (Environment): T denotes a term; F denotes a named
fact and N denotes a name, which in either case is an arbitrary uncapitalised string;
and GVar denotes a goal type variable, which is an arbitrary capitalised string. A
goal type is a goal type schema without any goal type variables, i.e. with A ::= T | N
To illustrate, the goal type schema
                                     top symbol(T, Y ).
expresses that the top level symbol of (goal type variable) T has to be (goal type
variable) Y . An example goal type using this schema:
                     top symbol(concl, ∧), has top symbol(hyps, ∧).
It states that the conclusion and one hypothesis of the goal has to be a conjunction;
as we shall see later, has top symbol can be defined in terms of top symbol.
   In practice, we have found that most goal types, such as top symbol(T, Y ), are
constraints over terms. These may have to be provided by the underlying theorem
prover, and we call them atomic goal types. One example atomic goal type is
top symbol(T, Y ), while any(), which we can also write any, is provided by default.
The any predicate will always succeed.
   As will be seen in case studies, many goal types combines such atomic goal types.
To achieve readable and intuitive proof strategies, low-level implementation details
needs to be hidden to highlight the high-level concepts of the graph. To support
that, a user can define a new goal type schemas, which can be used by a goal type:


10 Compared   with for example using the underlying implementation language of Tinker (ML).
                                              Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
90     ·      Lin, Grov and Arthan

  Definition (Goal type schema definition). A goal type schema definition
(GTSD) is a rule defined by:
           GT SD ::= N (Ov) ← GT S                       Ov ::= V s | 
                   | N (Ov) ← GT S GT SD                 V s ::= GVar | GVar, V s
We often call the left hand side of ‘←’ the head and the right hand side the body.
 To illustrate, the goal type scheme definition:
             g h(X, Y ) ← top symbol(concl, X), has top symbol(hyps, Y ).
requires that the first argument is the top symbols of the conclusion and that there
exists a hypothesis that has the top symbol of the second argument. This is used
in the following definition:
                                      g(X) ← g h(X, ∧).
                                      g(X) ← g h(X, ∨).
Here, g(X) is defined to be a goal type scheme where the conclusion has the top
symbol given by the argument X, and there is a hypothesis with either ∧ or ∨ as
top symbol. g(∧) is an example of a a valid goal type using this schema.
  One can also use variables in the body not present in the head. This is used to
pass arguments between literals of the body. For example,
      concl top in hyp() ← top symbol(concl, X), has top symbol(hyps, X).
expresses that there is a hypothesis with the same top symbol as the conclusion.
  Recall from Fig. 3 (§2.2.1) that in an evaluation step of a PSGraph, we need to
check if a goal g satisfies a goal type G. This depends on the provided atomic goal
types atoms and goal type definitions defs. We write
                                      hdefs,atomsi ` g : G
to express that such relation holds. In order to determine this, information about
the values of variables has to be passed between the clauses. For example, consider
concl top in hyp(). Here, the X of both the clauses in the body has to be the
same; in other words, has top symbol(hyps, X) needs to know the value of X
from top symbol(concl, X). To achieve this, an environment is passed between the
literals. This environment is different from the environment in the goal node in
that goal type variables are bound, and we call it a goal type environment:
   Definition (Goal type environment). A goal type environment (GTEnv)
is a function:
                                        GVar → EnvVal.
For concl top in hyp(), the result of applying the first top symbol will be an envi-
ronment with X bound, which is then used in the second application of top symbol.
  In order to specify hdefs,atomsi ` g : G, we introduce a relation that generates a
goal type environment:
                                hdefs,atomsi ` hg, Gi ⇓ gtenv
This should be read as: given a context consisting of a pair of the atomic goal types
atoms and goal type definitions defs, and an input consisting of a pair of a goal g
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                            Understanding and maintaining tactics graphically          ·     91

and a goal type G, a goal type environment gtenv is produced. hdefs,atomsi ` g : G
can then be defined in terms of the existence of such a goal type environment:
         (hdefs,atomsi ` g : G) ⇔ (∃ gtenv. hdefs,atomsi ` hg, Gi ⇓ gtenv)
 The semantics of the ⇓ relation is inspired by Prolog with some key differences.
Firstly, due to the “lifted” nature over atomic goal types, most of the unification
work is provided by the underlying prover. Secondly, we have to work with two dis-
tinct environments. Thirdly, we have to communicate with the underlying theorem
prover. We can therefore not use Prolog directly in a natural way, and decided to
develop a domain specific version, which we provide big-step operational semantics
for next.
   The semantics of ⇓ are non-deterministic, in that it can generate multiple valid
goal type environments (gtenv ). As hdefs,atomsi ` g : G is only concerned with the
existence of a valid goal type environment, it does not matter which of the valid
ones is found. The definition of the semantics uses auxiliary relations ⇓b and ⇓c .
   The evaluation of a goal type is a special case of the evaluation of the body
of a goal type schema, the difference being that the relation is over a goal type
environment, which is updated. This is evaluated by the relation ⇓b , where b
stands for ‘body’. This is evaluated over an environment and a clause body. As
there are no side-effects on the goal, the goal and its environment are moved to the
context:
                     henv(g), def s, atoms, gi ` h{}, Gi ⇓b gtenv
                            hdefs,atomsi ` hg, Gi ⇓ gtenv
The body is either a single clause ‘C.’, or a clause followed by more clauses ‘C, GT S’.
As a result there are four cases: ‘C, GT S’, ‘C.’, atomic goal types and negated
literals.
   For the second case, the clause is evaluated. We write this as f vs where vs is
a list of the arguments. To evaluate this we try to find a definition of f in all the
definitions. This is achieved by the ⇓c relation, where c stands for ‘clause’:
                henv, def s, atoms, gi ` hgtenv, f vs, defsi ⇓c gtenv 0
                  henv, def s, atoms, gi ` hgtenv, f vs.i ⇓b gtenv 0
Each definition is terminated by ‘.’; we therefore ensure that all clauses are evalu-
ated:
              henv, def s, atoms, gi ` hgtenv, f vs, clausesi ⇓c gtenv 0
          henv, def s, atoms, gi ` hgtenv, f vs, clause. clausesi ⇓c gtenv 0
The main work happens in the case where we find a definition with a head f Vs
of the same name. The formal parameter list Vs is a list of variable names of the
same length as vs. To illustrate, assume we are evaluating the underlined f in
                         · · · ← h(X), f (concl, X, Y, ?x), · · · .
As a result of evaluating h, X may be bound to some value e1 in the goal type
environment. Furthermore, assume that concl is e2 and ?x is bound to e3 in the
environment. When a definition of the same name, such as

                                f (A, B, C, D) ← body.
                                            Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
92     ·     Lin, Grov and Arthan

is found, then the formal parameters must be instantiated. In this case it should
generate an environment {A 7→ e2 , B 7→ e1 , D 7→ e3 }. Note that these are con-
straints of the variables; as Y is not bound it is unconstrained, and is therefore
not included. To achieve this instantiation we first introduce the partial function
lookup:
                                     
                                      get name(goal, v) if v ∈ name
        lookup(goal, env, gtenv, v) = env(v)             if v ∈ dom(env)
                                       gtenv(v)          if v ∈ dom(gtenv)
                                     

This function looks up values of names or variables when present in one of the
environments. Note that concl and hyps are examples of names, and get name
will in those cases return the underlying conclusion (a term) or list of hypothesis
(list of terms), respectively. We then define a function that is used to apply the
instantiations:
       inst gtenv(goal, env, gtenv, [V1 , · · · , Vn ], [vi , · · · , vn ]) :=
        {Vi 7→ lookup(goal, env, gtenv, vi )|(goal, env, gtenv, vi ) ∈ dom(lookup)}
   Returning to our example, the body of f is then evaluated, starting with the initial
environment {A 7→ e2 , B 7→ e1 , D 7→ e3 } generated. A result of this evaluation is
a new environment. Let’s assume that this binds C and a new variable F : {A 7→
e2 , B 7→ e1 , D 7→ e3 , C 7→ e4 , F 7→ e5 }. The clause should return an environment
with only the variables in the actual parameters bound. In this case, the call made
was f (concl, X, Y, ?x), meaning only X and Y should be in the domain – which
corresponds to variables B and C: {X 7→ e1 , Y 7→ e4 }. This functionality is handled
by the res gtenv function:
                   res gtenv(gtenv, [V1 , · · · , Vn ], [vi , · · · , vn ]) :=
                        {vi 7→ gtenv(Vi )|vi ∈ var ∧ Vi ∈ dom(gtenv)}.
As a result, the derivation rule for evaluating a single goal type schema becomes:
        length(vs) = length(Vs)       gtenv0 = inst gtenv(g, env, gtenv, Vs, vs)
                    henv, def s, atoms, gi ` hgtenv0 , bodyi ⇓b gtenv1
                         gtenv 0 = res gtenv(g, gtenv1 , Vs, vs)
         henv, def s, atoms, gi ` hgtenv, f vs, f Vs ← body. clausesi ⇓c gtenv 0
with a special case when f is the last definition:
        length(vs) = length(Vs)       gtenv0 = inst gtenv(g, env, gtenv, Vs, vs)
                    henv, def s, atoms, gi ` hgtenv0 , bodyi ⇓b gtenv1
                          gtenv 0 = res gtenv(g, gtenv1 , Vs, vs)
             henv, def s, atoms, gi ` hgtenv, f vs, f Vs ← body.i ⇓c gtenv 0
Another option is that f is an atomic goal type, which is then applied to generate
the new environment:
             f ∈ dom(atoms)        gtenv 0 ∈ atoms(f ) gtenv (v1 , · · · , vn ) g
               henv, def s, atoms, gi ` hgtenv, f (v1 , · · · , vn )i ⇓b gtenv 0
We have already mentioned any and top symbol(X, Y ) which are both atomic goal
types. Other generic atomic goal types include:
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                                Understanding and maintaining tactics graphically          ·     93

—trm var(X) holds if term X is a variable.
—member(XS, X) holds if X is a member of list XS.
—eq trm(X, Y ) holds if the terms X and Y are syntactically equal (α-equivalence).
These can for example be used in a schema to check if a given term is the same as
a hypothesis or the conclusion:
                    is goal(X) ← eq trm(concl, X).
                    has hyp(X) ← member(hyps, Y ), eq trm(X, Y ).
We can also use member to define the above has top symbol(X, Y ):
              has top symbol(X, Y ) ← member(X, Z), top symbol(Z, Y ).
 A third case is negation. This case will behave as an identity function on the
environment, if the non-negated version fails:
       ¬ ∃ gtenv 0 .henv, def s, atoms, gi ` hgtenv, f (v1 , · · · , vn )i ⇓b gtenv 0
                                                                                      

             henv, def s, atoms, gi ` hgtenv, !f (v1 , · · · , vn )i ⇓b gtenv
  The final case is the evaluation of the body of a goal type of multiple clauses, i.e.
the case: ‘C, GT S’. Here, evaluation is sequential: first C is evaluated by ⇓c , then
the rest GT S is evaluated recursively by ⇓b . However, the goal type environments
cannot just be passed sequentially as the following example illustrates. Consider:
                             p(X, Y, Z) ← a(X, Z), b(Y ), c(Z).
Assume we have the following application: p(t1 , t2 , A). Here, the initial environment
will be
                                        {X 7→ t1 , Y 7→ t2 }
However, when applying a this is restricted to X and Z, so a will only return an
environment with X and Z in. If we use this directly the Y binding is lost.
   Instead, the environment is updated with the new values. Note that the con-
straints are checked in each element – thus it is safe to override. Finally, the two
environments are combined, where the latter overrides11 the former:
                   henv, def s, atoms, gi ` hgtenv, c1 , defsi ⇓c gtenv 00
               henv, def s, atoms, gi ` hgtenv † gtenv00 , (c1 , c2 )i ⇓b gtenv 000
                            gtenv0 = (gtenv † gtenv00 ) † gtenv000
                   henv, def s, atoms, gi ` hgtenv, (c1 , c2 )i ⇓b gtenv 0
As the example above illustrates, the environment following b only contains Y .
Thus X and Z are added, whilst X and Z have to be added after evaluating c.
This completes the evaluation semantics of goal types.
  To illustrate more complex usage of goal types, we provide an example from
ongoing work by Farquhar and others on machine learning PSGraphs and goal
types using a technique called meta interpretive learning [19]. Here, we provide
low-level operations on terms and, using a small set of examples, learn suitable
goal type definitions from them.

11   A † B denotes that B overrides A

                                                Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
94      ·    Lin, Grov and Arthan

     To achieve this, we introduce an atomic goal type
                                       dest trm(X, L, R),
which holds if term X is “destructed” into its left L and right R sub-terms, when
such exists12 For example dest trm(pf x y q ,pf x q ,py q ) holds, meaning that
pf x q is the left sub-term and py q is right sub-term of pf x y q . By using dest
trm, we can define left and right as:
                             left(X, L) ← dest trm(X, L, ).
                             right(X, R) ← dest trm(X, , R).
Next, we introduce another atomic goal type
                                           const(X, C)
which holds if and only if term X is a the constant (name) C. For example,
const(pf q , f ) holds. Instead of treating top symbol(T,Y) as an atomic goal type
we can define it using these more primitive atomic goal types and recursion:
                   top symbol(T, Y ) ← const(T, Y ).
                   top symbol(T, Y ) ← left(T, Z), top symbol(Z, Y ).
This goal type will traverse the left side of the term until the end is reached and
check if this is the correct constant (or bind it to variable Y ). Note that it will
not work if the top-level function is higher-order (i.e. a lambda abstraction). We
can also define a function that checks both the left and right side of an application.
This amounts to checking if a symbol is present at any place of the term13 :
                  has symbol(T, Y ) ← const(T, Y ).
                  has symbol(T, Y ) ← right(T, Z), has symbol(Z, Y ).
                  has symbol(T, Y ) ← left(T, Z), has symbol(Z, Y ).
  These examples show that, as with PSGraph, we can work with the goal types
at different levels of abstraction. This is illustrated by treating top symbol as an
atomic goal type or by defining it in the language in terms of lower-level more
primitive atomic goal types.

3.3    Graphical breakpoints
There are two ways to apply a PSGraph to a goal in Tinker: (1) in the automatic
mode it is applied as a black box and all you see is the final subgoals on the
output wires; (2) in the interactive mode the user can step through and guide the
proof of the goal. When debugging a large proof, such as our current work with
D-RisQ’s tactic [43], one often wants to combine these modes: one would like to use
an automatic/black-box execution until the problematic part of the proof strategy
is reached, and at that point enter an interactive mode where the user can step
through the proof.

12 Applications  may also instantiate variables. For example, dest trm(pf x y q , V1 , V2 ) will in-
stantiate V1 to pf x q and V2 to py q , if they are not bound in the goal type environment.
13 For simplicity, this definition does not work in presence of binders (lambda abstractions), but

can easily be extended to support this with a new atomic goal type.


Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                            Understanding and maintaining tactics graphically            ·     95

                                             G           G
                                            gg
                                                       STOP
                                              G
                                 RB =             ,→       G
                                                           G
                                           STOP         gg
                                             G
                                             G            GG

                                Fig. 10.    Breakpoint rule

  This is essentially how breakpoints of modern IDEs work: the user inserts a
breakpoint in the program text, and the debugger will execute the code until the
breakpoint is reached. At that point the user can manually step through the code.
Inspired by this idea for debugging programs, we extend PSGraph with a new
special breakpoint node, which can be seen in Fig. 10.
  We also introduce a third mode called debug mode. The intuition behind this
mode is to achieve exactly the requirement above: the graph is executed as in au-
tomatic mode until it cannot execute any further, either because it has successfully
terminated or because the goals are followed by a debug node. In order to keep the
semantics of PSGraph, we only need to update the termination condition for the
debug mode:
  Definition (Termination in debug mode). A graph has terminated in de-
bug mode, if for all goals g of the graph, g is either on a graph output wire or it is
wired to another goal, or is wired to a debug node.
   If the graph has successfully terminated in debug mode, it will enter interactive
mode and the user can step through the graph manually. In this case, goals needs
to be able to “step over” breakpoints, which is achieved by adding the rule RB
from Fig. 10 to the ruleset Reval (Fig. 3) when we are in interactive and automatic
modes, whilst omitting it from Reval in debug mode.
   This very small extension turns out to be a very powerful aid for debugging
PSGraphs. We will see it in action in the case studies in §4.
3.4   A logging mechanism
Another recent extension, which as we will show later has been very useful in
our case studies, is a logging mechanism. Introducing such a mechanism is an
engineering problem rather than a scientific one, but as logging forms part of the
user experience, it merits a brief discussion here.
  To illustrate logging, consider the example in Fig. 11 (left), where lemma tac
applies the cut rule with the term bound in ?g. The goal types is goal(?g) and
is not goal(?g) check if the goal is or is not the same as ?g respectively. The
logging mechanism will then print the logging messages as shown in Fig. 11 (right).
First, it prints the information about the environment of goal g, which says it has
a variable ?g bound. The next two lines shows the open goals afterwards, which
are i and j. It then displays the results from evaluating the goal types: First we
see that i success for the wire labelled by is goal(?g). As all possible combinations
will be generated, it also checks if i succeeds for the other wire, which fails. It then
does the same for j, which will only succeeds for is not goal(?g). The final line
states that one branch was generated, with i and j on separate wires.
                                              Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                  96      ·       Lin, Grov and Arthan

                                        any
                                                            > ENV_DATA :
                                    g         Debugging and
                                                          g: refactoring
                                                              E_Trm (...)tactics graphically                     ·       11
                                                                    > GOAL : Open goals
   c(forall)
                                                                        [Goal i] ...
             c(conj)                lemma_tac(?g) c(forall)
    ∀_tac           ∧_tac                                   c(conj)
                                                                        [Goal j] ...               c(forall)
                                                                                                             c(conj)
                              is_goal(?g) !is_goal(?g)
                                                    ∀_tac           > GOALTYPE : evaluating ∀_tac
                                                                    ∧_tac                            is_goal(?g)    ∧_tac
                                                                                                                          with
                     h1                                              pnode i env g => E_Trm(...)
                                                             any > SUCCESS                                     any
                   h2
             any                                                    > GOALTYPE : evaluating !is_goal(?g) with
                                             2                              h2                2
                                                                     pnode i env g => E_Trm(...)
                                                is_sets() h1                                      is_sets()                is_arith()
                                                                    >        is_arith()
                                                                       FAILURE
 is_sets()                                  any
                           is_arith()                               > GOALTYPE         : evaluating  is_goal(?g)
                                                                                                  PC_T1 "sets_ext" REPEATwith
                                                                                                                            strip_tac
                                                  PC_T1 "sets_ext" REPEAT strip_tac

 PC_T1 "sets_ext" REPEAT strip_tac lemma_tac(?g)                     pnode j env g => E_Trm(...)
                                                                    > FAILURE
                                                          PC_T1 "lin_arith"   prove_tac                  PC_T1 "lin_arith" prove_tac []
                                 is_goal(?g) !is_goal(?g)
        PC_T1 "lin_arith" prove_tac []                              > GOALTYPE : evaluating !is_goal(?g) with
                                      i           j                  pnode j env g => E_Trm(...)
                                                                    > SUCCESS
                                        Fig. 4. Example evaluation of PSGraph.
                                                                    > EVAL : Branch(goals on the output edges): | i | j |

wire where g satisfies the goal type then        there
                                              Fig. 11. Awill be multiple
                                                          logging example rewrites. Each of
these rewrites will be a separate branch of the search space. We will return to the
                      in §3.2.of a complex strategy with many branches can be very verbose. Our
                Full logging
goal type predicate
             logging
  The leftmost    rulemechanism
                       of Figure allows
                                    3 showthe  user
                                             the     to use theof
                                                  evaluation    tags
                                                                   ansuch  as ENV_DATA,
                                                                       atomic   tactic. In thisetc. seen
                                                                                         GOAL
             in  Fig. 11 to filter the types  of message   that are  displayed.
case, there will be a side-e↵ect on the proof state, as detailed above in §2.2.1. This
rule can be summarised as follows:
                  4.    CASE STUDIES
(1) Set g to This
             be atsection
                     the topwill
                              of address
                                  the goalour
                                            stack  in ProofPower
                                               hypothesis  through with
                                                                    threethe
                                                                          casecommand    set first ex-
                                                                               studies. The
    labelled goal g.
             ample re-engineers a tautology-proving tactic into PSGraph. We will express the
(2) Apply tactic   T (Args)
             high-level  ideas(to  the goal
                               behind         at theintop
                                        the tactic        of the stack)
                                                       an abstract       to obtain
                                                                   way and          a listan
                                                                             then obtain   of efficient
    subgoals implementation by a sequence of refactorings adding goal types to direct the proof
(3) Consumesearch.
               g fromTinker’s
                       the graph;debugging capabilities are utilised to find and correct mistakes in
             the encoding. The second example looks at a set of ad hoc domain-specific tactics
(4) Add all valid  combination
             developed   to finesseofthe
                                      theproof
                                           resulting  sub-goals
                                                of a lemma       to output
                                                             forming part ofwires.
                                                                             the proof of security of
             a database
  The rule-set           system.
                R does not         Wea will
                             contain    rulesee
                                             forhow  to tactic
                                                 graph  use PSGraph     to represent
                                                                as it would  look theproof
                                                                                       samepatterns
             involving tacticals (tactic combinators).   The  final case  study
as the atomic tactic. Here, the interpretation of Args is very di↵erent, and itsconsiders a decision
             procedure  for problems
evaluation can be summarised as:      such  as proving continuity  of real-valued functions. We will
                  see how PSGraph can be used to express complex recursive rewriting strategies.
(1) Consume gAfrom     the graph;
                  case-study  approach for evaluation was chosen as the work is exploratory and
(2) Lookup the graph G which TThe
             improvement-driven.         threeto;
                                      points    case studies have different, yet relevant, challenges
             and thus provide us with necessary armoury for larger scale problems found in
(3) Constrain the environment of g to variables in Args and add this to an input
             industrial settings. They also enables analyses of PSGraph from different aspects,
    wire of G (such that the goal type is satisfied). If there are multiple then one
             which is known as triangulation in software engineering [57]. We have deliberately
    branch will be generated for each;
             addressed unfamiliar problems, as opposed to types of problems that we know that
(4) EvaluatePSGraph
              G until termination;
                        will excel for. For reasons discussed in §5, our analysis is qualitative in
             nature.
(5) Add all valid combination of the goals on the output wires of G to the output
    wires of the graph tactic T .
                  4.1    A tautology tactic for propositional logic
If any steps For
              fail the
                    then   evaluation
                        purposes         ofsection,
                                   of this  this node     fails. Note
                                                      a tautology         that to
                                                                    is defined when
                                                                                  be a adding  a re-instance
                                                                                       substitution
sulting sub-goal   to formula
              of any   the output     of T in
                                 χ formed      theboolean
                                            from     last step,    the sub-goal
                                                              variables   and thewill  be given
                                                                                   boolean       the T and
                                                                                           constants
environment of g, with values of Args replaced by those in the resulting sub-goal.
   Fig. 4 illustrates    some of Reasoning
              Journal of Formalized the stepsVol.of9, the  flow
                                                      No. 2, 2016.through the proof strategy of
Fig. 2 applied to the example of §2.1. In the initial graph, g holds the initial goal.
It then applies R twice, which will first apply universal introduction followed by
conjunction introduction, introducing two new subgoals h1 and h2. Next it applies
the identity tactic to h2 and then h1, with the result shown in the right-most graph.
This is used to filter the goals to the correct tactic to complete the proof. h1 is
                                                   Journal of Formalized Reasoning Vol. ?, No. ?, Month Year.
                             Understanding and maintaining tactics graphically        ·     97

F using the connectives ¬, ∧, ∨, ⇒ , ⇔ , if then else , such that χ evaluates to T
under any substitution of the constants T or F for its propositional variables. We
will describe the design and implementation of a tactic that takes a goal which we
assume (for simplicity) has no assumptions: ? ` φ and will prove any such goal
where φ is a tautology.
  The decision procedure underlying the tautology tactic transforms its goal to a
set S of subgoals:

          Γ 1 ?` t 1 , ..., Γ n ?` t n

where the Γ i and the t i comprise only propositional literals, i.e., atoms or negated
atoms(but not ¬T or ¬F ). The transformation ensures that S is is logically equiv-
alent equivalent to the original goal when viewed as a conjunction of implications.
The original goal is then a tautology iff each of the subgoals in S has one of the
following forms (which we refer to below as structural tautological forms):

          Γ , t, ¬t ?` u
          Γ , t ?` t
          Γ , F ?` u
          Γ ?` T .

The implementation will realise these transformations as tactics and will apply a
tactic that will recognise and discharge structural tautological subgoals as they are
created. Realising the decision procedure using tactics in this way converts it from
an algorithm that merely recognises tautologies into an algorithm that finds a proof.
   The tactic that implements the decision procedure uses two rewrite systems. The
rewrite systems are defined by theorems giving universally quantified bi-implications
which are instantiated as appropriate and used as left-to-right rewrite rules. The
first rewrite system is applied to the conclusions of subgoals:

          `   ∀ a• ¬ ¬ a ⇔ a
          `   ∀ a b• ¬ (a ∧ b) ⇔ ¬ a ∨ ¬ b
          `   ∀ a b• ¬ (a ∨ b) ⇔ ¬ a ∧ ¬ b
          `   ∀ a b• ¬ (a ⇒ b) ⇔ a ∧ ¬ b
          `   ∀ a b• ¬ (a ⇔ b) ⇔ a ∧ ¬ b ∨ b ∧ ¬ a
          `   ¬T ⇔F
          `   ¬F ⇔T
          `   ∀ a b c• ¬ (if a then b else c) ⇔ (if a then ¬ b else ¬ c)
          `   ∀ a b• (a ⇔ b) ⇔ (a ⇒ b) ∧ (b ⇒ a)
          `   ∀ a t1 t2 • (if a then t1 else t2 ) ⇔ (a ⇒ t1 ) ∧ (¬ a ⇒ t2 )
          `   ∀ a b• a ∨ ¬ b ⇔ b ⇒ a
          `   ∀ a b• ¬ a ∨ b ⇔ a ⇒ b
          `   ∀ a b• a ∨ b ⇔ ¬ a ⇒ b

  The following ProofPower idiom implements the above rewrite system:



                                           Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
98     ·     Lin, Grov and Arthan

val taut strip concl conv : CONV = (
        eqn cxt conv (
        map thm eqn cxt
        [¬ ¬ thm, ¬ ∧ thm, ¬ ∨ thm, ¬ ⇒ thm,
         ¬ ⇔ thm, ¬ t thm, ¬ f thm, ¬ if thm,
        ⇔ thm, local if thm,
        a ∨ ¬b thm, ¬a ∨ b thm, a ∨ b thm]));
Here ¬ ¬ thm, ¬ ∧ thm etc. name the theorems of the rewrite system in the
order given above. Repeated application of these rewrite rules will transform the
conclusion of a subgoal into either a propositional literal or a conjunction or an
implication. If the conclusion is a propositional literal, the tactic will test whether
the subgoal has one of the structural tautological forms, discharging the subgoal if
it passes the test and reporting an error if it fails. If the conclusion is a conjunction,
the subgoal splits into two subgoals, one for each conjunct. If the conclusion is an
implication say φ ⇒ ψ, the subgoal will reduce to a set of subgoals obtained from
the original subgoal by adding certain literals to its assumptions. These literals
are obtained by “stripping” the logical connectives out of the antecedent φ while
making case splits as appropriate.
   The following list of functions captures the processing described above but defers
the stripping of new assumptions to a parameter that is a function of type
           THM TACTIC = THM −> TACTIC ,
(Functions of this type are referred to as theorem continuations and play an im-
portant role in the traditional approach to programming LCF style systems [52].)
For a conclusion of the form φ ⇒ ψ, the tactical ⇒ T will carry out the strip-
ping process by passing the theorem φ ` φ representing the new assumption to
the parameter function. For the cases other than implications, this parameter is
ignored.
val taut strip concl ts : (THM TACTIC −> TACTIC ) list = [
        fn => ∧ tac,
        ⇒ T,
        fn => t tac,
        fn => conv tac taut strip concl conv ,
        fn => concl in asms tac];
  Stripping the antecedent φ of an implication φ ⇒ ψ into the assumptions is dual
to the processing of a conclusion. If φ is not a conjunction or a disjunction, it is
rewritten using a second rewrite system. This second system is like the first but
with the rules for disjunctions replaced by the following rule for implications:

            ` ∀ a b• a ⇒ b ⇔ ¬ a ∨ b




Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                            Understanding and maintaining tactics graphically        ·     99

val taut strip thm conv : CONV = (
        eqn cxt conv (
        map thm eqn cxt
        [¬ ¬ thm, ¬ ∧ thm, ¬ ∨ thm, ¬ ⇒ thm,
         ¬ ⇔ thm, ¬ t thm, ¬ f thm, ¬ if thm,
        ⇒ thm, ⇔ thm, local if thm]));
   The new subgoals derived by stripping φ into the assumptions are then produced
by iterating around the following list of functions: if φ is a conjunction, φ1 ∧ φ2 , we
strip φ1 and φ2 into the assumptions separately; if φ is disjunction, φ1 ∨ φ2 , we get
two subgoals, one with φ1 stripped into its assumptions and one with φ2 stripped
into its assumptions; otherwise we attempt to apply the rewrite rules:
val taut strip thm thens : THM TACTICAL list = [
        ∧ THEN ,
        ∨ THEN ,
        CONV THEN taut strip thm conv ];
Here ∧ THEN and ∨ THEN are operators on theorem continuations that per-
form one logical transformation and pass the theorems representing the result on
to their operands. Operators like this provide a powerful continuation-passing style
for programming tactics. This style was introduced and popularised by Paulson
[52] and widely adopted by developers of tactics in LCF-style systems.
  The following tactic implements a single step in the above process as determined
by the principal connective of the conclusion of the goal. The expression begin-
ning REPEAT TTCL is the theorem continuation parameter for ⇒ T mentioned
above. It uses taut strip thm thens to strip a new assumption into atoms and then
uses the tactic check asm tac to add these assumptions to the resulting subgoals
while checking for and discharging subgoals having one of the structural tautological
forms.
val taut strip tac : TACTIC = (
         FIRST
         (map(fn t => t(REPEAT TTCL (FIRST TTCL taut strip thm thens)
                          check asm tac))
                 taut strip concl ts));
Here REPEAT TTCL and FIRST TTCL are combinators on theorem continu-
ations that provide repetition until failure and selection of the first non-failing
theorem continuation from a list.
   For an example of taut strip tac in action, let us see how it will work given
Peirce’s law: ((a ⇒ b) ⇒ a) ⇒ a. It will actually prove this immediately by strip-
ping the antecedent (a ⇒ b) ⇒ a into the assumptions of a goal with conclusion a.
The new assumption will first be rewritten in the form ¬(a ⇒ b) ∨ a resulting in a
case split into two goals, one with assumption ¬(a ⇒ b) and one with assumption
a. The assumption ¬(a ⇒ b) will be rewritten as a ∧ ¬b which will be stripped
into two new assumption literals, a and ¬b. In both cases, the resulting subgoal is
a structural tautology that will be discharged by check asm tac.



                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
100        ·     Lin, Grov and Arthan

                                              any       any

                                             taut_strip_tac


                                 Fig. 12.   simp taut tac version 1

  The tautology tactic then simply repeats the single step tactic until there are no
subgoals left or until no further progress can be made, in which case it raises an
exception.
val simple taut tac : TACTIC = (fn gl =>
        case REPEAT taut strip tac gl of
                done as ([], ) => done
        |         => fail "simple taut tac" 28121 []);
(The number 28121 here is an error code identifying a message reporting that the
conclusion of the goal is not a tautology.)
   Failure-driven higher-order functional programming using combinators to control
iteration and sequencing has proved very successful in programming LCF-style sys-
tems. Here it enables us to code a rather complex recursion scheme in a compact
way that does reveal the structure of the algorithm to those familiar with the ap-
proach. Although we have spent several pages here describing the tautology tactic,
the actual source code we have presented is only 32 lines of which all but 9 do
little more than set up tables. However, we agree with Paulson, who concedes that
while higher-order functions provide good control and efficiency, they can be hard
to understand [52].
   Looking at even a simple example of the higher-order programming style bring
several questions to mind: is the high-level proof plan visible to a non-expert looking
at the implementation? How easy would it be to locate a mistake in the code if
it failed to prove a tautology? How would we go about refactoring the code?
In the rest of this section, we will illustrate how to encode simple taut tac in
PSGraph using the Tinker system. We will show how to support developing a
correct and optimised PSGraph implementation through a set of refactoring and
analysis supported by the Tinker framework. For the most readable version of this
tactic, we refer to the final version (Fig. 18)14 .
   4.1.1 Version 1: A generic PSGraph of the tautology tactic. simple taut tac
repeats taut strip tac until it is no longer applicable; if all subgoals are discharged
at this point then the tactic succeeds, and it fails otherwise. Fig. 12 implements
this tactic at a very high level of atomicity where taut strip tac is treated as an
atomic tactic.
   Graphically, repetition is simply represented as a feedback loop. By making this
feedback loop the only output wire we achieve the same termination semantics as
simple taut tac. This can be justified as follows: if taut strip tac fails on any
subgoal then the overall tactic will fail: in simple taut tac this means that the
REPEAT combinator will terminate with a subgoals which result in failure. If the
tactic produces subgoals then taut strip tac is re-applied, as is the case for the

14 It   may be easier to understand the example by working backwards from this final version.


Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                                                 Understanding and maintaining tactics graphically                                                                ·           101

                                                any                                    any                                any
                  concl_in_asms_tac                   any           ENV_all_asms                                                    ENV_top_symb_non_literal_asm
                                          any                                                  strip_ _concl_tac
            any                                                    (hyps, ?oriAsms)                                                      (hyps, "not", ?asm)
  any                                                                                                                     any
                                    any                     any                                any
                      t_tac                                                                                any                           ENV_top_symb_asm
 taut_strip_tac                                                                                                         any
                                    any                           strip_ _concl_tac                                                   (hyps, "if_then_else", ?asm)
                                                                                        ENV_top_symb_asm
                                           any
                                                  any        any                        (hyps, ""conj, ?asm)            any               ENV_top_symb_asm
                       ∧_tac                                                                                                              (hyps, "equiv", ?asm)
                                                                                                  ENV_top_symb_asm
                                strip_∨_concl_tac           strip_¬_concl_tac                      (hyps, "disj", ?asm)
                                                                                                                                 ENV_top_symb_asm                       any
                                                                                         any                     any            (hyps, "implies", ?asm)          any

                              any               strip_if_concl_tac            any                                               any
                                                                                                 elim_∨_asm_tac(?asm)                      elim_ _asm_tac (?asm)
                                          any

                                                                  any          elim_∧_asm_tac (?asm)                                                                     any
                                                                                                                  elim_ _asm_tac (?asm)
                                                  any

                                                                                                     any          any                                elim_if_asm_tac (?asm)
                                                                                                                          any     any
                                                                                                                                         any
                                                                        any                                                                            elim_¬_asm_tac (?asm)
                                                                                                                                               any
                                                  any                                                 check_new_asms_tac
                                                                                                        (?oriAsms, hyps)


                              Fig. 13.           Version 2: Flat and parallel tactic application.

REPEAT combinator. Finally, if there are no more subgoals, then the PSGraph
will successfully terminate; this is also the success case for PSGraph.
   4.1.2 Version 2: From sequential to parallel tactic application. The example of
Fig. 12 does not show sufficient details to understand how simple taut tac works.
This require a further “unfolding” of taut strip tac into a graph. Fig. 13 shows
the same tactic as a graph tactic and its subgraph.
   This is achieved by “unpacking” all the tacticals, and represent each of the com-
ponents as a tactic, with some minor modifications. To illustrate, the left part
of the subgraph in Fig. 13 corresponds to the taut strip concl ts tactic, with the
conversions in the list of taut strip concl conv represented by the 4 atomic tactics
starting with ‘strip’.
   The right part of the subgraph corresponds to the work conducted on the hypoth-
esis by taut strip thm thens when an implication introduction rule is applied. It
first uses the ENV all asms environment tactic to store all hypothesis in a variable
?oriAsms, before applying the introduction rule. For each propositional combina-
tors, there is then a case adapted from taut strip thm thens and the conversions
in taut strip thm conv. In most cases, they follow the pattern illustrated in Fig. 9
(§3.1), where the hypothesis is first bound by one environment tactic and then the
elimination rule is applied. At the end of this branch of the graph, check new
asms tac will get the lists of new hypothesis by comparing the current hypothesis
(hyps) with the hypothesis on entry (?oriAsms) to this part of the graph.
   A conceptual difference between Fig. 13 and the simple taut tac ProofPower
tactic is that in PSGraph we no longer need to enforce a sequential order; if two or
more tactics are mutually independent, we can put them next to each other using
identity tactics as necessary to split inputs and merge outputs.
   Note that each wire is labelled by any, meaning it will always succeed. This
means that for a given subgoal generated by a given tactic, all possible output
wires will be attempted in a separate branch of the search space. Thus, this graph
can be seen as a generalisation of taut strip tac in the sense that it will succeed if
taut strip tac succeeds (albeit it is not as efficient).
  4.1.3 Version 3: Modularising the graph through hierarchies. PSGraph aims to
support development of proof strategies that are easy understand, maintain and

                                                                                      Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
102     ·           Lin, Grov and Arthan


                                       any                                                                     any
      concl_in_asms_tac          any         any                                       ENV_all_asms (hyps, ?oriAsms)
                                                              strip_ _concl
                          any                  any                                                             any
            t_tac
                                                     strip_ _concl_tac
                         any                                                                      strip_ _concl_tac
                                  any
                                         any       any
            ∧_tac                                                        any                             any

                       strip_∨_concl_tac           strip_¬_concl_tac                        taut_strip_asm
                                                                                                         any
                      any       any    strip_if_concl_tac                                         check_new_asms_tac
                                                              any                                   (?oriAsms, hyps)
                                         any       any
                                                                                                         any

                                any
                                                                                      any

                                                                                                   any
                                                                                                                elim_   _asm
                                  any                                    any
                                                                                                any
                    ENV_top_symb_asm                                           any            any        elim_ _asm
                    (hyps, "conj", ?asm)                    elim_∧_asm                any

                                  any                                                                elim_ ¬_asm
                                                                       elim_ ∨_asm
               elim_∧_asm_tac (?asm)                          any                                        any
                                                                                       elim_if_asm              any any
                                  any                                           any
                                                                                        any


                                                                                            any


                                Fig. 14.       simp taut tac version 3: with hierarchies

refactor. To achieve this it should be intuitive to see what the proof strategy is
meant to do. Whilst the flat graph of Fig. 13 gives a detailed account of how the
goals flow, it mixes high-level descriptive details of the proof strategy with low-
level implementation details that are required to run it. It also “merges” different
operations which are best to split, e.g. operations on the conclusion and operations
on the hypothesis. This should be avoided when a more declarative and readable
strategy is sought.
   For tactic languages modularity is handled by sub-tactics, as is the case for
taut strip tac. Within PSGraph such modularity is achieved through hierarchical
graph tactics. Fig. 14 refactors the graph of Fig. 13 into a more modular graph.
   The top-level graph (top-left) contains the atomic operations on the goal, but
has refactored the case that handles implications (and following operations on the
hypothesis) into a graph tactic called strip ⇒ concl. This is shown in the top-right
corner of Fig. 14. Within strip ⇒ concl, the actual operations on the hypothe-
sis are refactored into a graph tactic taut strip asm, which is comparable to the
taut strip thms thens tactic, shown on the bottom left corner of Fig. 14. Each
case of this level corresponds to a propositional operator and is a nested graph
tactic, where each of these follow the structure shown on the bottom right side.
Here, an environment tactic first bind the operator and then the tactic is applied.
The example illustrates the case for a conjunction, but the other cases are similar.
  4.1.4 Version 4: The use of goal types to explain and optimise the tactic. The
hierarchies help in exposing the high-level proof idea by hiding lower-level details
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                                            Understanding and maintaining tactics graphically                            ·   103

                     is_goal(true) any
                                                                                                            c(implies)
     concl_in_asms_tac                       c(implies)
                                                              strip_ _concl
                                                                                     ENV_all_asms (hyps, ?oriAsms)
      has_hyp(concl)                         c(equiv)
                                  c(disj)            strip_ _concl_tac                                    any
     t_tac            c(conj)
                                  c(if_then_else)                                           strip_ _concl_tac
             ∧_tac                              c_not_var(not)            any
                                                                                                    any
                      strip_∨_concl_tac           strip_¬_concl_tac
                                                                                     taut_strip_asm

                     any        any   strip_if_concl_tac                                              any
                                                              any
                                                                                            check_new_asms_tac
                                            any    any
                                                                                              (?oriAsms, hyps)
                                                                                                      any
                                any



                                                                                    any
                                                                                            h(implies)
                                                                         h(conj)                      elim_ _asm
                                 h(conj)                                               h(equiv)
                                                                            h(disj)
               ENV_top_symb_asm                                                                  elim_ _asm
                                                          elim_∧_asm         h(if_then_else)
               (hyps, "conj", ?asm)
                                                                                      h_not_var(not)
                                any                               elim_ ∨_asm              elim_ ¬_asm
              elim_∧_asm_tac (?asm)                         any                     elim_if_asm   any       any any
                                any                                           any
                                                                                     any


                                                                                      any


                 Fig. 15.         simp taut tac version 4: with hierarchies and goal types

and “grouping” together sub-strategies, such as separating operations on hypothesis
from operations on the conclusion. However, all wires are labelled by the any goal
type, which always succeeds. This use of any has at least threes problems:
—Explanation: the proof strategy does not explain why a goal should choose a
 particular path. This is crucial in order to understand the proof strategy.
—Evaluation: the use of any means is that all paths are attempted, which is in-
 efficient.
—Debugging: a side-effect of the evaluation is that it debugging becomes hard as:
 —there more (failed) branches in the search space to analyse;
 —it is not clear what the intention of a particular path is which makes it hard
    (and time consuming) to find the “correct” branch;
 —the error may manifest itself at different place further down the “flow” of the
    strategy.
Developing goal types is one of the more challenging tasks of developing PSGraphs,
and is also where development deviates most from standard tactic developments.
In tactics we often end up trying one tactic first (e.g. if it is very quick or normally
works) and if it fails we try something else. This is essentially what the tacticals
in the list used by taut strip tac does. Although this is possible in PSGraph, it is
better to think about why a particular tactic (or sub-strategy) should be applied.

                                                                  Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
104      ·     Lin, Grov and Arthan

                                         c(implies)
                                                                                      c(implies)
                  ENV_all_asms (hyps, ?oriAsms)
                                     any                       ENV_all_asms (hyps, ?oriAsms)
                        strip_ _concl_tac                                         any

                                                                     strip_ _concl_tac
                            any
                                         i
                                                           asm_to_strip() any
                           STOP


                                                              taut_strip_asm
                  taut_strip_asm                                       !asm_to_strip()
                                   any                              check_new_asms_tac
                                                                      (?oriAsms, hyps)
                        check_new_asms_tac
                          (?oriAsms, hyps)                                      any
                                   any


Fig. 16. Left: strip ⇒ concl (version 4) illustrating a bug with a breakpoint. Right: strip ⇒
concl (version 5) with bug fixed by feedback loop.

Moreover, when it fails it is hard to analyse where and why the failure happened.
If the tactic/PSGraph also contains the “reason” for why a tactic is applied, in
form of a goal type, then any failure is likely to show up at the right place and not
several tactic applications later. This will create much more maintainable proof
strategies; as we will illustrate below, it also becomes easier to analyse and patch
a mistake in a proof strategy.
   Fig. 15 updates the graph of Fig. 14 with goal types. Some of these goal types
were introduced in §3.2, while we will introduce some new ones here. Firstly, recall
the atomic goal type
                                                dest trm(X, Y, Z)
from §3.2, which holds if term X is “destructed” into its left Y and right Z sub-
terms. We use c(X) and h(X) as shorthand for the top symbol of the conclusion
and a hypothesis, respectively:
                      c(X) ← top symbol(concl, X).
                      h(X) ← member(hyps, Z), top symbol(Z, X).
The conversions applied to deal with negations by strip ¬ concl tac (conclusion)
and elim ¬ asm (hypothesis) require that the top level symbol is a negation, and
the body is not just a variable (i.e. it is either compound or a constant). These
properties are expressed by the goal types:
       c not var() ← c(not), dest trm(concl, , Z), !trm var(Z).
       h not var() ← member(hyps, Y ), top symbol(Y, not), dest trm(Y, , Z),
                     !trm var(Z).
With the goal types one can see in which cases a tactic should be applied, and
evaluation will only try the branches where a goal satisfies the goal type.
  4.1.5 Version 5: Discovery and patching of a bug. The proof strategy of Fig. 15
will succeed for a large set of propositional tautologies, such as:
GOAL

(∗ ?` ∗)pA ∧ B ⇒ B ∧ Aq

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                             Understanding and maintaining tactics graphically         ·     105

However, it fails for the following (correct) goal:
GOAL

(∗ ?` ∗)pA ∧ B ∧ C ⇒ C ∧ B ∧ Aq
   As we have an idea where the problem is, we insert a breakpoint and automat-
ically evaluate the strategy until the break point is reached15 . This is shown in
Fig. 16 (left). At this point the goal, labelled by i, has been simplified to:
GOAL

(∗ 1 ∗)pA ∧ B ∧ C q
(∗ ?` ∗)pC ∧ B ∧ Aq
  We can now step through the proof from that point in the nested taut strip asm
graph tactic. The goal satisfies h(conj), as the top level symbol of an hypothesis is
a conjection, and correctly splits up the conjunction in the hypothesis (* 1 *):
GOAL

(∗ 1 ∗)pAq
(∗ 2 ∗)pB ∧ C q
(∗ ?` ∗)pC ∧ B ∧ Aq
At this point it will exit the graph tactic, and (via check new asms tac) return to
the top of the top-level graph. The problem is that one hypothesis (* 2 *) contains
a conjunction, and the aim of the overall proof plan is that all connectives in the
hypothesis should have been eliminated. One could still continue to run the proof,
where it will eventually will have the goal:
GOAL

(∗ 1 ∗)pAq
(∗ 2 ∗)pB ∧ C q
(∗ ?` ∗)pC q
which will not satisfy the goal type (of the top level graph), and thus fail. The
problem is that taut strip asm has to be repeated until there are no more con-
nectives. This is reflected in the updated proof strategy shown in Fig. 16 (right).
Here, we need a goal type to identify when there are more goals to be satisfied and
label the loop with this:
                        asm   to   strip()   ←   h(conj).
                        asm   to   strip()   ←   h(disj).
                        asm   to   strip()   ←   h(equiv).
                        asm   to   strip()   ←   h(implies).
                        asm   to   strip()   ←   h(if then else).
                        asm   to   strip()   ←   h not literal(not).
This is essentially a disjunction of all the possible symbols. The output wire,
representing termination of the loop, is labelled by its negation: !asm to strip().
Note that if we had this goal type instead of any as output of taut strip asm in
Fig. 15 (left), then the error would manifested itself at the correct place, which
illustrates the importance of goal types. The above goal will now succeed.
15 If
    we had no idea where the problem may have been we could just have evaluated the strategy
from the beginning – the same approach as described in the rest of the section would still be
applicable.
                                             Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
106     ·      Lin, Grov and Arthan

                                         c(implies)
                                                                                   c(implies)
                  ENV_all_asms (hyps, ?oriAsms)
                                                            ENV_all_asms (hyps, ?oriAsms)
                                          h                                     any

                                     any       STOP                      strip_ _concl_tac
                                                                  asm_to_strip()
                        strip_ _concl_tac
                                                       asm_to_strip()
               asm_to_strip()      any                                          !asm_to_strip()
                                                            taut_strip_asm
                  taut_strip_asm                              !asm_to_strip()
                           !asm_to_strip()                        check_new_asms_tac
                        check_new_asms_tac                          (?oriAsms, hyps)
                          (?oriAsms, hyps)                                   any
                                   any


Fig. 17. Left: strip ⇒ concl (version 5) illustrating bug with goal node and breakpoint. Right:
strip ⇒ concl (final version 6) with bug fixed by new wire.

  4.1.6 Version 6 & final version: Discovery and patching of another bug. Next,
we try to prove the following goal:
GOAL

(∗ ?` ∗)pA ⇒ A ∧ Aq
  Again, the tautology strategy fails. As with the previous case, one would suspect
the issues is related to the hypothesis, thus we insert a breakpoint just before this
part as shown in Fig. 17 (left). At this point, the goal is the same as the original
goal. In the next step, strip ⇒ concl tac is applied generating:
GOAL

(∗ 1 ∗)pAq
(∗ ?` ∗)pA ∧ Aq
   It will then enter the taut strip asm graph tactic, but it will then fail when
stepping over the identity tactic. At this point, we can use the logging mechanism
of Tinker, which gives the following message:
      FAILURE : Fail to match any Loop for the output goal node:
               [Goal i : A |- A & A]
In this case, the only assumption is
ASSUMPTIONS

(∗ 1 ∗)pAq
which does not have any logical connectives and should therefore not be further
simplified. The problem is that we have forgotten to bypass taut strip asm when
there are no assumptions to simplify. To rectify the strategy, this missing case is
added, using the asm to strip() goal type to separate the two cases. This is shown
in Fig. 17 (right)
   This completes the development of simple taut tac as a PSGraph. A complete
version of the tautology tactic is shown in Fig. 18. In this final version we have
also added a goal type to the input of of the overall strategy to show which type of



Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                                                  Understanding and maintaining tactics graphically                              ·       107

                              taut_simp()                                                                        c(implies)
                                           taut_simp()
                               taut_strip_tac                                             ENV_all_asms (hyps, ?oriAsms)
                                                                                                              any

                                                                                                       strip_ _concl_tac
                  is_goal(true) any                                                             asm_to_strip()
 concl_in_asms_tac                        c(implies)                              asm_to_strip()
                                                              strip_ _concl
                                                                                                                 !asm_to_strip()
  has_hyp(concl)                          c(equiv)                                        taut_strip_asm
                               c(disj)            strip_ _concl_tac                           !asm_to_strip()
  t_tac            c(conj)
                               c(if_then_else)
                                                    c_not_var(not)                              check_new_asms_tac
          ∧_tac                                                         any
                                                                                                  (?oriAsms, hyps)
                   strip_∨_concl_tac             strip_¬_concl_tac
                                                                                                           any

                  any        any   strip_if_concl_tac
                                                              any                                    any
                                         any     any                                                            h(implies)
                                                                                           h(conj)                            elim_   _asm
                                                                                                             h(equiv)
                             any                                                                h(disj)
                                                                                elim_∧_asm       h(if_then_else)     elim_ _asm
                                                                                                          h_not_var(not)
                                                  h(conj)                             elim_ ∨_asm              elim_ ¬_asm
                               ENV_top_symb_asm                                 any
                                (hyps, "conj", ?asm)                                                 elim_if_asm        any    any any
                                                                                               any
                                                 any                                                   any
                              elim_∧_asm_tac (?asm)
                                                 any                                                    any


                                               Fig. 18.      simp taut tac completed version

goals it will work for:
                        taut       simp()           ←       is goal(true).
                        taut       simp()           ←       has hyp(concl).
                        taut       simp()           ←       has no hyp(concl), c(conj).
                        taut       simp()           ←       has no hyp(concl), c(disj).
                        taut       simp()           ←       has no hyp(concl), c(if then else).
                        taut       simp()           ←       has no hyp(concl), c(equiv).
                        taut       simp()           ←       has no hyp(concl), c(implies).
                        taut       simp()           ←       has no hyp(concl), c not literal(not).
  4.1.7 Discussion. A simple and instructive example has been used to illustrate
many features of PSGraph and Tinker, which can be contrasted to the existing
sentential encoding of simple taut tac in ML. One of the key advantages is that
a non-expert can read the overall proof plan directly from the graph. Compare
that for example Fig. 18 (starting from top-left) with the use of the REPEAT
TTCL tactical used in taut strip tac. Without a deep understanding of underlying
semantics of this (and other) tactical, it is very hard to see what the tactic does.
For example, it matters if REPEAT TTCL is applied 1 or more times or 0 or more
times. Our original version only applied it a single time; the second version 1
or more times; and the final version got it right and applied it 0 or more times.
Through the debugging features of Tinker and PSGraph, this was fairly easy to



                                                                         Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
108       ·    Lin, Grov and Arthan

find16 . To find a similar mistake in the original code would not be as easy, and
would very likely require us to tear the tactic apart so that we can step through
the execution, which in itself is not always an easy task. For a subset of ML,
the Tactician tool for HOL light [2] can automate such tearing apart of tacticals,
but in most cases it has to be done manually. To summarise, while short “one
liners”, such as taut strip tac, are elegant, they are not necessarily that easy to
understand. Anecdotally, getting the ML code right is hard even for an expert –
then what about novel users and non-experts? Would you show the one-liner to
your (non-technical) line manager or would you draw up a high-level diagram?
   We have also found other advantages of the graphical representation. One ex-
ample is that PSGraph allows us to delay decision on control flow, and make it
efficient later (by adding goal types). This is not possible in ML, where we must
give the order straightaway. Secondly, hierarchies enable hiding of low-level (im-
plementation) details: we can use the top-level graph(s) to show the high-level
(often declarative) proof ides, while the graph tactic contains implementation de-
tails. Consider for example how elim ∧ asm hides how we use an environment
tactic to apply conjunction elimination in Fig. 18. Thirdly, meta-level properties of
the proof strategies can be read directly from the graph – which is not as obvious
in the ML code. One example of this is the symmetry between the proof steps in
the conclusion (top-left) and the hypothesis (bottom-right) of Fig. 18.
   As a general guidance, picking sensible names for goal types and tactics is crucial
if the PSGraph should act as an explanation of a proof strategy. It is also useful
to try to combine parts that “belong” together in graph tactics. To work with
PSGraph, one need to change to a more declarative way of thinking compared with
the more procedural way of developing LCF tactics. It is important to think about
why certain tactics should be applied, and encode this knowledge into the goal
types. It is also important to be aware that there is still work required at the ML
level: one has to develop atomic tactics and atomic goal types, and also think about
the arguments (if any) of them. Through goal types, PSGraph ensures locality when
changing part of the proof strategy. You can safely assume that changes you make
will only effect goals that satisfy the goal types leading to the sub-graph that is
change: it will not have any impact on parallel sub-graphs.
   This case study has highlighted a current limitation with respect to parametrised
graph tactics. All the tactics within taut strip asm of Fig. 18 have the structure
illustrated by elim ∧ asm. The only difference is that logical connective and tactic
used. It would have been desirable to be able to make this an argument for a generic
graph tactic, to avoid having to re-implement each version. The next example will
illustrate how we can parametrise over tactic and goal type arguments, but not the
actual tactics.

4.2   Domain specific tactics from the Front End Filter (FEF) project
The FEF Project [55] was an early application of ProofPower to verify the security
properties of a multi-level secure database system called SWORD. In this section
we will look at some very domain-specific tactics taken from the FEF proof scripts

16 Notethat these bugs where not artificial by any means: they were genuine mistakes we did
during development and the graphical representation help to locate.

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                           Understanding and maintaining tactics graphically         ·     109

as an experiment in porting an existing application proof to PSGraph with a view
to making future maintenance easier by presenting the proof at a higher level.
   It would be inappropriate here to give a very detailed description of the four
tactics we investigate. Such a description would be long and not very instructive
and would not reflect the process by which the tactics came into existence, which
was by interactive trial and error. The best way to get a feeling for this kind
of process is by replaying the proofs interactively. See [55] for instructions for
downloading the proof scripts. The ProofPower documents that are most relevant
to the present paper are fef032.doc for specifications and fef033.doc for the
proofs. In the present paper, we will set the relevant proof in context, which should
give enough background to understand our transcription of the tactics into PSGraph
and should help anyone who is interested in more detail to locate and work with
the FEF documents.
   The query language for the SWORD database was Secure SQL (SSQL) an exten-
sion of standard SQL whose semantics support a notion of security classification.
Data in the database would be a assigned a classification drawn from some lattice.
e.g., SECRET > COMPANY-RESTRICTED > COMPANY-IN-CONFIDENCE >
UNCLASSIFIED. If c1 and c2 are elements of the lattice we say c1 dominates c2 if
c1 ≥ c2 . Database users are assigned a security clearance which is also drawn from
the lattice of classifications: a user cleared at classification c is only allowed to see
data whose classification is dominated by c. SSQL was implemented via a prepro-
cessor (referred to as the Front End Filter or FEF) that translates SSQL queries to
queries in ordinary SQL on a database whose schema augmented the SSQL schema
with security classification for each item of data. The translated query uses these
classifications to prohibit information flows that would violate the security policy,
e.g., by revealing SECRET data to a user who is only cleared to see information at
COMPANY-IN-CONFIDENCE or UNCLASSIFIED.
   The high-level security property for FEF requires that for every query q and every
user u, if two states s1 and s2 differ only in respect of data that u is not cleared to
see, then, when executed by u, q will deliver the same result in state s1 as it doesn in
state s2 . To achieve this, the semantics of SSQL label the result of any calculation
with a security classification. If the label on the end result of a query is c, then
the implementation will erase the information content of the result if the user is
not cleared to see data of classification c. The formal specification of the SSQL
semantics includes for each language construct both the derivation of the result
and the derivation of the classification label from the values and classifications of
the operands of the construct and of the database items it accesses. There is then a
proof obligation to show that the semantics satisfies the high-level security property.
Like conventional SQL, the syntax of SSQL queries involves a mutual recursion
between table-expressions and value-expressions. These are given formal semantics
as what we refer to as table computations and value computations. To prove that
the semantics satisfies the high-level security property involves an induction over
the syntax to prove a property OK TC d on table computations that can be used
fairly directly to prove the high-level security property. OK TC d is parametrised
by a security classification c and is defined as follows:



                                           Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
110     ·      Lin, Grov and Arthan

∀c tc• tc ∈ OK TC d c ⇔
       ∀tl 0 tl 1 •
                  Map (HideDerTable c) tl 0 = Map (HideDerTable c) tl 1
       ∧          ¬HideDerTable c (Snd (tc tl 0 )) = HideDerTable c (Snd (tc tl 1 ))
       ⇒          ¬c dominates Fst(tc tl 0 )
   Here we see that the table computation tc is a function with one argument: a
list of tables. The result of the table computation is a pair whose first component
is the classification label and whose second is the computed result. The function
HideDerTable is parametrised by the classification c of a user and replaces all items
in its operand that the user is not cleared to see by dummy values. The antecedent
of the implication in the theorem therefore asserts that a value calculated by tc
has revealed information about the operands that a user at classification c is not
cleared to see. A table computation tc belongs to the set OK TC d ciff whenever
the antecedent holds tc labels the return value with a classification that will prevent
a user with classification c from seeing it.
   To get the induction to go through, the property OK TC d needs to be strength-
ened by adding an additional property OK TC c (which ensures that the classifi-
cation labels do not provide a covert channel) and we have to define analogous
properties OK VC d and OK TC c on the value computations (the definition of
OK VC d is given below; see [55, fef032.doc] for the other definitions).
   As we shall see in the example, these properties are actually repesented as sets
and are parametrised by a security classification (and the induction proves that the
SSQL table and value computations belong to the appropriate sets at every classi-
fication). In this paper, we are going to look at some tactics defined to complete
the proof of a lemma about CASE-expressions that is needed in the induction. The
goal is as follows:
?` ∀c te cel ee•
        te ∈ OK VC d c ∧
        Elems (Map Fst cel ) ⊆ OK VC d c ∧
        Elems (Map Snd cel ) ⊆ OK VC d c ∧
        ee ∈ OK VC d c ⇒
        CaseVal c te cel ee ∈ OK VC d c
  Here CaseVal is the constant that captures the semantics of the SSQL CASE-
expression. As in SQL, this has the syntax:
CASE <te> WHEN <c1> THEN <e1> ... WHEN <cN> THEN <eN> ELSE <ee>
In the goal, c is the security classification of a user executing the query and te, cel
and ee give the semantic values of the operands of the CASE-expression, with the
WHEN/THEN pairs combined into a list of pairs cel. Elems is the function that
maps a list to its set of elements and Fst and Snd are the projections. Hence the
four conjuncts in the antecedent in the goal assert in turn that the semantics of the
test expression <te>, the condition expressions <c1>. . . <cN>, the result expressions
<e1>. . . <eN> and the else expression <ee> satisfy the OK VC d part of the inductive
hypothesis. So our lemma asserts that the CASE-expression preserves this part of
the inductive hypothesis.
  The property OK VC d has the following defining theorem:
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                           Understanding and maintaining tactics graphically        ·     111

∀c vc• vc ∈ OK VC d c ⇔
       ∀tl 0 tl 1 rl 0 rl 1 r 0 r 1 •
                  Map (HideDerTable c) tl 0 = Map (HideDerTable c) tl 1
       ∧          Map (HideDerTableRow c) rl 0 = Map (HideDerTableRow c) rl 1
       ∧          HideDerTableRow c r 0 = HideDerTableRow c r 1
       ∧          ¬Snd (vc tl 0 rl 0 r 0 ) = Snd (vc tl 1 rl 1 r 1 )
       ⇒          ¬c dominates Fst(vc tl 0 rl 0 r 0 )
    Here we see that the value computation vc is a function with three arguments:
a list of tables (needed for nested SELECTs), a list of table rows (needed for
GROUPBY) and a table row (the row from which individual values are extracted
by name in simple expressions). The result of the value computation is a pair
whose first component is the classification label and whose second is the value
of the expression. The hide functions set items in their operand that the user
is not cleared to see to dummy values. So very like OK TC d discussed above,
membership of OK VC d c asserts that if a value calculated by vc has revealed
information about the operands that a user at classification c is not cleared to see
then vc must label the value with a classification that will prevent that user seeing
it.
    A design goal of SSQL was to classify data as liberally as the security requirements
and the desire for an efficient and maintainable implementation permitted. For
the CASE-expression, the classification is that of the test-expression if the user
is not cleared to see the test expression; if the user is not allowed to read one
of the condition expressions that comes before the selected condition, then the
classification is the classification of that condition expression (since the fact that
that condition was not selected reveals information about the expression); otherwise
the classification is the classification is that of the selected result expression. The
main proof plan for the lemma is an induction on the list of WHEN/THEN pairs.
The inductive step is the following goal:
(∗   5   ∗)pCaseVal c te cel ee ∈ OK VC d cq
(∗   4   ∗)pte ∈ OK VC d cq
(∗   3   ∗)pElems (Map Fst (Cons x cel )) ⊆ OK VC d cq
(∗   2   ∗)pElems (Map Snd (Cons x cel )) ⊆ OK VC d cq
(∗   1   ∗)pee ∈ OK VC d cq

(∗ ?` ∗)pCaseVal c te (Cons x cel ) ee ∈ OK VC d cq
   To make the presentation more readable, the calculation of the classification of
a CASE-expression is defined separately from the calculation of the value of the
expression. To make the inductive hypothesis (assumption 5) usable, these defini-
tions have to be combined (in the lemma CaseVal lemma) into a single primitive
recursion over the WHEN/THEN list. Unfortunately, this combined definition in-
volves 5 conditionals and when we expand the definition of OK VC d and do some
normalisation, the goal ends up containing 15 conditionals: 5 in each expression
corresponding to the 3 applications of vc in the definition OK VC d . The last few
lines of the goal are as follows:


                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
112     ·      Lin, Grov and Arthan

...
⇒ ¬ c dominates (
       if Snd (te tl 0 rl 0 r 0 ) = Snd (Fst x tl 0 rl 0 r 0 )
       then
                if c dominates Fst (te tl 0 rl 0 r 0 )
                         ∧ c dominates Fst (Fst x tl 0 rl 0 r 0 )
                then Fst (Snd x tl 0 rl 0 r 0 )
                else if ¬ c dominates Fst (te tl 0 rl 0 r 0 )
                then Fst (te tl 0 rl 0 r 0 )
                else Fst (Fst x tl 0 rl 0 r 0 )
       else if c dominates Fst (te tl 0 rl 0 r 0 )
                ∧ c dominates Fst (Fst x tl 0 rl 0 r 0 )
       then Fst (CaseVal c te cel ee tl 0 rl 0 r 0 )
       else if ¬ c dominates Fst (te tl 0 rl 0 r 0 )
       then Fst (te tl 0 rl 0 r 0 )
       else Fst (Fst x tl 0 rl 0 r 0 ))
   A case split on the first 3 tests and some rewriting eliminates 6 of the 8 cases
leaving 2 outstanding subgoals ‘4.1’ and ‘4.2’. In each of these subgoals, a case
split on what are now the first 3 tests and some rewriting simplifies away all the
conditionals leaving 16 outstanding subgoals ‘4.1.1’ . . . ‘4.1.8’ and ‘4.2.1’ . . . ‘4.2.8’.
An interactive attack on ‘4.1.1’ finds a combination of tactics that proves both it
and ‘4.1.2’, so we package this up into an ad hoc tactic tac1 and try it on all of
‘4.1.1’ . . . ‘4.1.8’ and find that it proves the first 4 of them leaving ‘4.1.5’ to prove.
Continuing in this way we end up with 4 very application-specific tactics each of
which proves 4 of the 16 subgoals and with these we can complete the proof. The
ML code of the 4 tactics is shown in Figure 19.
   Representing these application-specific tactics in PSGraph prevents novel chal-
lenges. In the tautology example we were faced with mature production level code,
implementing a clear underlying proof plan. In this example, we are faced with a
set of ad hoc tactics that “did the job”. An interesting problem is to understand
the underlying proof idea, with the ultimate aim of providing a tactic that is robust
to changes and can be re-used for similar proofs. In the remainder of this section
we will make steps by showing a systematic and modular way of transferring tactics
to PSGraph to improve understandability and maintainability.
   4.2.1 Encoding common proof patterns. The first observation we make about
the four FEF tactics is that of code repetition, which we can extract into separate
proof patterns. Our first step is to develop these patterns in PSGraph; this will
enable us to develop a library and re-use the patterns using the library functionality
of Tinker (see §2.2.2) We have found three patters, which we call LEMMA THEN1,
CASE THENLIST and DROP ASM. These are highlighted in Fig. 19, which shows
the ProofPower code of the tactics. Note that code is only included to show the
repetition: we will not go into details of the actual tactics except for the encoding
of the patterns.
 4.2.1.1 The LEMMA THEN1 pattern. The LEMMA THEN1 can be imple-
mented as follows:

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                              Understanding and maintaining
                                         Debugging          tactics graphically
                                                     and refactoring              · 113
                                                                        tactics graphically                    ·   35

SML

val tac1 = REPEAT strip tac THEN
  LEMMA T pSnd x 2 OK VC d cq                                  LEMMA_THEN1
  (fn th => all fc tac[rewrite rule(map get spec[pOK VC d q])th])
  THEN1 PC T1 "sets ext" asm prove tac(map get spec[pElemsq, pMapq]);

val tac2 = REPEAT strip tac THEN
  cases tacpSnd (te tl 0 rl 0 r 0 ) = Snd (te tl 1 rl 1 r 1 )q        CASE_THENLIST
  THEN LIST [
  asm ante tac p¬ Snd (te tl 1 rl 1 r 1 ) = Snd (Fst x tl 1 rl 1 r 1 )q
  THEN POP ASM T (asm rewrite thm tac o eq sym rule)
  THEN REPEAT strip tac THEN
  LEMMA T pFst x 2 OK VC d cq                                         LEMMA_THEN1
    (fn th => all fc tac[rewrite rule(map get spec[pOK VC d q])th])
  THEN1 PC T1 "sets ext" asm prove tac(map get spec[pElemsq, pMapq]),
 DROP ASM T pte 2 OK VC d cq                                       DROP_ASM
 (fn th => all fc tac[rewrite rule(map get spec[pOK VC d q])th])];

val tac3 = REPEAT strip tac THEN
  cases tacpSnd (te tl 0 rl 0 r 0 ) = Snd (te tl 1 rl 1 r 1 )q        CASE_THENLIST
  THEN LIST [
  asm ante tac p¬ Snd (te tl 0 rl 0 r 0 ) = Snd (Fst x tl 0 rl 0 r 0 )q
  THEN asm rewrite tac[]
  THEN STRIP T (asm tac o conv rule(RAND C eq sym conv )) THEN
  LEMMA T pFst x 2 OK VC d cq                                         LEMMA_THEN1
    (fn th => all fc tac[rewrite rule(map get spec[pOK VC d q])th])
  THEN1 PC T1 "sets ext" asm prove tac(map get spec[pElemsq, pMapq]),
 DROP ASM T pte 2 OK VC d cq                                       DROP_ASM
 (fn th => all fc tac[rewrite rule(map get spec[pOK VC d q])th])];

val tac4 = REPEAT strip tac THEN
  DROP ASM T pCaseVal c te cel ee 2 OK VC d cq                    DROP_ASM
  (fn th => all fc tac[rewrite rule(map get spec[pOK VC d q])th]);

                           Fig. FEF
                      Fig. 19.  17. tactics
                                     FEF tactics    with highlighted
                                            with patterns patterns highlighted

                                                                                    any

                                                                  any      lemma_tac (?g)
                                                             is_goal(?g)
                                                          lemma_tac (?g)                    !is_goal(?g)
                                            is_goal(?g)             !is_goal(?g)
              is_term(?g)                                     config_tac      ?gThm := @{thm" asm_rule ?g "}
                             is_term(?g)    config_tac      ?gThm := @{thm"
                                                                     any asm_rule ?g "}       any
               LEMMA_THEN1(?g)
               LEMMA_THEN1(?g)                    any                        any config_thm_tac(?gThm)
                             any                                config_thm_tac(?gThm)
                             any                                                              any
                                                                             any

                            Fig. 18.       PSGraph encoding of LEMMA THEN1
                     Fig. 20.      PSGraph encoding of LEMMA THEN1

It will apply the cut rule by adding   a new sub-goal ?g. It will apply ?thm tac to
                                   Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
the original goal (with ?g add to the list of hypothesis), and tactic ?tac to the new
subgoal. This pattern can for example be seen in tac1 of Fig. 17, where ?tac is
instantiated to:
SML

 (fn th => all fc tac[rewrite rule(map get spec[pOK VC d q])th])
114     ·      Lin, Grov and Arthan


                                                                      any
                                                            case_tac (?case)

                  is_term(?case)                  has_hyp(?case)    !has_hyp(?case)

                   CASE_THENLIST(?case)                config_pos    config_neg
                                   any                       any               any

                        Fig. 21.   PSGraph encoding of CASE THENLIST

fun LEMMA THEN1 g thm tac tac = (LEMMA T g thm tac) THEN1 tac;
It will apply the cut rule by adding a new subgoal g. This is followed by an applica-
tion of tactic thm tac to the original goal (with g added to the list of hypothesis),
and tactic tac to the new subgoal. This pattern can for example be seen in tac1 of
Fig. 19, where we can instantiate the pattern as follows:
 LEMMA THEN1
     pSnd x ∈ OK VC d cq
     PC T1 "sets ext" asm prove tac(map get spec[pElemsq, pMapq])
     (fn th => all fc tac[rewrite rule(map get spec[pOK VC d q])th])
  Fig. 20 shows the PSGraph encoding of the LEMMA THEN1 pattern. The
tactic is encapsulated in a graph tactic LEMMA THEN1(?g) (left), where ?g is
the subgoal in which the pattern is parametrised over. The ?g argument of the
LEMMA THEN1 graph tactic is used to make ?g available for the nested graph,
while the incoming goal type is term(?g) ensures that ?g is bound to a term in the
environment before the pattern is applied.
  The right hand side of the figure shows the body of the tactic, which “unfolds” the
LEMMA T and THEN1 tacticals. First, lemma tac(?g) is applied, which applies
the cut rule. The graph then depicts the parallel nature of how the new subgoal
?g and the existing subgoal are handled separately. The goal type is used to guide
the goal to the correct tactic. However, the example highlights the limitation of
parametrised graph tactics we have already discussed (and return to in §4.2.3). We
need to introduce two dummy tactics, config tac and config thm tac, which has to
be manually replaced (renamed) when this pattern is used (as shown below).
  4.2.1.2 The CASE THENLIST pattern. The second pattern applies a case-split
on a given variable case, followed by tactic tac1 when case holds, and tactic tac2
for its negation. This is called CASE THENLIST :
fun CASE THENLIST case tac1 tac2 = case tac case THEN LIST [tac1 , tac2 ];
  The PSGraph encoding of this pattern can be seen in Fig. 21. It is similar in struc-
ture of LEMMA THEN1, and also illustrates how naturally PSGraph highlights
that the two cases should be handled separately. It should be noted that, albeit
sufficient in this case, case tac may simplify the hypothesis thus !has hyp(?case)
will not work as expected in all cases.
  4.2.1.3 The DROP ASM pattern. In Fig. 19, the final pattern DROP ASM, are
instances of the DROP ASM T tactical. For purposes of the underlying pattern


Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                                     Understanding and maintaining tactics graphically                     ·   115


                                                               has_hyp(?hyp)

                           is_term(?hyp)                      config_tac(?hyp)

                                  DROP_ASM(?hyp)                            any

                                              any           drop_asm_tac(?hyp)
                                                                            any


                                 Fig. 22.   PSGraph encoding of DROP ASM


                           any
                  repeat_strip_tac                                                   any

                                                                           lemma_tac (?g)
                           any
                                                              is_goal(?g)                   !is_goal(?g)
         ?g := @{term" Snd x ∈ OK_VC⋎d c "}                                 ?gThm := @{thm" asm_rule ?g "}

                            is_term(?g)                                                           any
                                                         PC_T1_asm_prove_tac
                LEMMA_THEN1(?g)                                      any           asm_fc_thm_tac(?gThm)
                            any                                                                    any


Fig. 23. PSGraph tac1 : top level (left) and the sub-graphs of node LEMMA THEN1(?g)(right)


representation in PSGraph, we unfold the meaning of DROP ASM T , creating
the ML function:
fun DROP ASM hyp thm tac = thm tac hyp THEN drop asm tac hyp;
  It will first apply a tactic thm tac using the given hypothesis hyp, and then
remove the hypothesis by the drop asm tac tactic. Fig. 22 shows the PSGraph
version.
  4.2.2 Encoding the FEF tactics in PSGraph. The patterns can easily be used
with Tinker’s library functionality in a drag-and-drop manner17 .
  We can then develop the tactics tac1, · · · , tac4 in a modular way. The two small-
est tactics are tac1 and tac4. They only use one single pattern. To illustrate, Fig. 23
shows tac1 encoded in PSGraph. In the figure, the stippled boxes illustrates the
instantiation of the parametrised components of the pattern. ProofPower’s strip
tac is first applied, followed by an environment tactics that binds variable ?g to
pSnd x ∈ OK V C d c q 18 . This is followed by the LEMMA THEN1 pattern, where
config tac is replaced by PC T1 asm prove tac, which is defined as
SML

 PC T1 "sets ext" asm prove tac(map get spec[pElemsq, pMapq]);
and dummy thm tac is replaced by asm fc thm tac(?gThm), which is defined as
SML

 all fc tac[rewrite rule(map get spec[pOK VC d q]) ?gThm]

17 See
     the dedicate web page [42] for a screencast of the library functionality.
18 Note
      that within the Tinker tool, we have followed the syntax used by Isabelle’s anti-quotation
mechanism where a term t is written @{term ”t”}.

                                                     Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                   THEN LIST [

  36         ·     asmLin,
                        ante     p¬ Arthan
                             tacand
                           Grov     Snd (te tl 1 rl 1 r 1 ) = Snd (Fst x tl 1 rl 1 r 1 )q
                   THEN POP ASM T (asm rewrite thm tac o eq sym rule)

  SML
                   THEN REPEAT strip tac THEN
  val tac1 =LEMMA     pFst xtac2 THEN
                  T strip
             REPEAT               OK VC d cq
                  (fn  th =>
           LEMMA T pSnd x 2 OK  all fc VC
                                       tac[rewrite
                                             cq    rule(map get spec[pOK VC d q])th])
                                                         d
                   THEN1
                  (fn  th =>PCall T1  "sets ext" asm
                                   fc tac[rewrite       prove get
                                                   rule(map    tac(map      VC d q])th]) pMapq]),
                                                                        get spec[pElemsq,
                                                                  spec[pOK
                                      pte
116         ·      DROP
                  THEN1    ASM
                           PC and
                     Lin, Grov     T
                                T1 Arthan 2 OK    VC  d cq
                                      "sets ext" asm prove tac(map get spec[pElemsq, pMapq]);
                   (fn th => all fc tac[rewrite rule(map get spec[pOK VC d q])th])];
  val tac2 = REPEAT strip tac THEN
  val tac3 cases
           = REPEAT
                 tacpSndstrip  tac
                          (te tl     THEN
                                 0 rl 0 r 0 ) = Snd (te tl 1 rl 1 r 1 )q                       X: CASE_THENLIST
           cases  tacpSnd
           THEN LIST [     (te  tl 0 rl 0 r 0 ) = Snd (te tl 1 rl 1 r 1 )q
                  THEN
                  asm anteLIST   [ Snd (te tl 1 rl 1 r 1 ) = Snd (Fst x tl 1 rl 1 r 1 )q
                            tac p¬                                                                           Y_pos
                  asm ante   tac
                  THEN POP ASM   p¬ Snd (te tl 0rewrite
                                     T (asm       rl 0 r 0 thm
                                                           ) = Snd
                                                               tac o(Fst x tl 0 rule)
                                                                      eq sym     rl 0 r 0 )q
                  THEN REPEAT
                  THEN asm rewrite  tac[]
                                strip tac THEN
                  THEN STRIP
                  LEMMA T pFstTx (asm
                                  2 OKtac  o dconv
                                          VC   cq rule(RAND C eq sym  conv )) THEN
                                                                  Z: LEMMA_THEN1
                         T pFst
                  LEMMA (fn  th =>x 2allOK    VC d cq
                                          fc tac[rewrite  rule(map get spec[pOK VC d q])th])
                         (fn T1
                  THEN1 PC    th =>
                                 "setsallext"
                                           fc tac[rewrite
                                               asm prove rule(map   get spec[pElemsq,
                                                           tac(map get                d q])th])
                                                                         spec[pOK VCpMapq]),
                   THEN1ASM
                  DROP          T pte
                            PC T1   "sets ext"VC
                                       2 OK    asm  prove tac(map get spec[pElemsq, pMapq]),
                                                 d cq
                                   pte  2                                 Y_neg: DROP_ASM
                   DROP    ASM  T         OK   VC d cq
                  (fn th => all fc tac[rewrite rule(map  get spec[pOK VC d q])th])];
                   (fn th => all fc tac[rewrite rule(map get spec[pOK VC d q])th])];
  val tac3 = REPEAT strip tac THEN
  val tac4 cases
           = REPEAT    Fig.
                         (te24.
                       strip
                 tacpSnd      tac
                             tl   ProofPower
                                  THEN         code of FEF tac2 tactic
                                0 rl 0 r 0 ) = Snd (te tl 1 rl 1 r 1 )q
                   ASM [T pCaseVal c te cel ee 2 OK VC d cq
           DROP LIST
           THEN
                      any                                     any
                  (fn th
                  asm  ante
            repeat_strip_tacall p¬
                         =>tac   fc Snd
                                    tac[rewrite    rule(map
                                         (te tl 0case_tac 0 ) = get
                                                   rl 0 r(?case) Sndspec[pOK      rl d0 q])th]);
                                                                      (Fst x tl 0VC      r 0 )qhas_hyp(?hyp)
                      any
           THEN
       assume    asmthese
              that    rewrite  tac[]
                            definitions
                              has_hyp(?case)   !has_hyp(?case)
                                             are                  asm_fc_thm_tac(?hyp)
                                                   covered in the above    explanation
    ?case := @{term "Snd(te tl⋎0 rl⋎0
                                                                                            any
                  THEN STRIP T (asm tac o conv
      r⋎0) = Snd(te tl⋎1 rl⋎1 r⋎1)"}               rule(RAND
                                          ?hyp := @{term" "te ∈ OK_VC⋎dC
                                                                       c "} eq sym conv )) THEN

      4.2.1 LEMMA
                Encoding
                  is_term(?case)    similarities          as patterns. We        any observe that       the definitions of the
                                                                                                     drop_asm_tac(?hyp)
       CASE_THENLIST(?case) T pFst x 2 OK VC d cq DROP_ASM(?hyp)
                                          POS_CASE(?case)
                                                                                                                  any
   four tactics        in    fef    share     similarities.
                                             any                       Thus,    one     efficient  approach
                                                               label: Y_neg rule(map get spec[pOK VC q])th])
                                                                                 any
                                                                                                                  to develop the
                 any           (fnX th => all fc tac[rewrite
                            label:                                                                             d label: Y_neg
   fef tactics in PSGraph is to generalise the similarities as patterns and encode each
                                                 label: Y_pos
              THEN1 PC T1 "sets ext" asm prove tac(map get spec[pElemsq, pMapq]),
   pattern
     Fig. 25. into
                 The atop-level,
                             PSGraphs.  second-levelThe and  fef subgraphs
                                                                   tactics can        then ASM
                                                                                of DROP       be incrementally
                                                                                                   of tac2 in PSGraph  developped
              DROP ASM T pte 2 OK VC d cq
   by reusing        these PSGraphs. To ease presentation, we name the three patterns as
    For more
   LEMMA      (fnTHEN1,
                     th => allCASE
                  complicated         fc tactics,
                                           tac[rewrite
                                                THENLIST suchrule(map
                                                                 as tac2 andget
                                                                              and spec[pOK
                                                                               DROP         weVC
                                                                                     tac3,ASM.    d q])th])];
                                                                                                have
                                                                                                  The  broken
                                                                                                         ML code   thedefinition
                                                                                                                         tactic of
upthese
     into components
            patterns are:representing the identified proof patterns (where appropriate).
Weval will
       tac4 demonstrate
              = REPEAT strip        this tacwithTHEN   tac2. Fig. 24 gives the ProofPower code for this
tactic, where DROP    theASM  patterns      have been
                                     T pCaseVal           c te highlighted
                                                                  cel ee 2 OK as     VCfollows:
                                                                                         d cq
                                                                                                  the green box shows
the CASE(fn     THENLIST               pattern;         the   red    boxes    show
                     th => all fc tac[rewrite rule(map get spec[pOK VC d q])th]);      the  positive  and negative cases
for CASE THENLIST. Within the positive                          Journal case,     the blueReasoning
                                                                           of Formalized      box shows Vol. the  LEMMA
                                                                                                              ?, No.  ?, Month Year.
THEN1 assume        thatwhile
             pattern,           these thedefinitions
                                             negative case         are usescovered
                                                                             the DROP    in the
                                                                                              ASMabovepattern.explanation
    Fig.
      4.2.125 (left)
                Encoding   shows       the top-level
                                   similarities                 view of the
                                                          as patterns.         We graph,
                                                                                      observewhich     follows
                                                                                                that the           the same
                                                                                                             definitions     of the
structure as tac1, albeit with the CASE THENLIST pattern applied. The body of
  four tactics in fef share similarities. Thus, one efficient approach to develop the
this graph tactic is shown in the middle of the figure. Here, ?case is first instantiated
  fef tactics in PSGraph is to generalise the similarities as patterns and encode each
to pSnd(tetl0 rl0 r0 ) = Snd(tetl1 rl1 r1 ) q .Note the use of stippled labelled boxes to
  pattern into a PSGraphs. The fef tactics can then be incrementally developped
show which part of the ProofPower code each sub-graph corresponds to.
  by reusing these PSGraphs. To ease presentation, we name the three patterns as
    In the instantiation of CASE THENLIST (middle), the tactics for the positive
  LEMMA THEN1, CASE THENLIST and DROP ASM. The ML code definition of
and negative cases, i.e. conf ig pos and conf ig neg, are replaced by two sub-
  these patterns
components.          Theare:  positive case is an instance of the DROP ASM tactic, shown at
the right hand side of Fig. 25. Here, ?hyp is initialised to pte ∈ OK V C d c q and
config tac(?hyp) is replaced by asm fc thm tac(?hyp), which is defined to be
SML
  Journal of Formalized Reasoning Vol. ?, No. ?, Month Year.
  all fc tac[rewrite rule(map get spec[pOK VC d q])                              ?hyp])
  The positive case is wrapped in a graph tactic POS CASE shown in Fig. 26.
The left hand side shows a flat version. Here, ?z is first bound to the term

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                                            Understanding and maintaining tactics graphically                          ·       117

 label: Y_pos
                       has_hyp(?case)
  ?z := @{term "¬ Snd(te tl⋎1 rl⋎1 r⋎1) =       label: Y_pos
         Snd(Fst x tl⋎1 rl⋎1 r⋎1)"}                                                                           has_hyp(?case)
                        any                                                              ?z := @{term "¬ Snd(te tl⋎1 rl⋎1 r⋎1) =
            asm_ante_tac (?z)                                                                   Snd(Fst x tl⋎1 rl⋎1 r⋎1)"}
                                                                     has_hyp(?case)                            any
                      any
      rewrite_sym_thm_tac(?case)                           apply_asm_ante                          asm_ante_tac (?z)

                       any                                           any                                     any
          drop_asm_tac(?case)                          pop_asm_rewrite(?case)
                                                                pop
                      any                                          any
                                                                                                                any
        default_asm_rewrite_tac                            repeat_strip_tac
                       any                                                                       rewrite_sym_thm_tac(?case)
                                                                      any
             repeat_strip_tac                                                                                    any
                                                 ?g := @{term" Snd x ∈ OK_VC⋎d c "}
                       any
                                                                     is_term(?g)                    drop_asm_tac(?case)
  ?g := @{term" Snd x ∈ OK_VC⋎d c "}
                                                         LEMMA_THEN1(?g)                                         any
                      is_term(?g)
                                                                                                  default_asm_rewrite_tac
           LEMMA_THEN1(?g)                                           any      label: Z
                                                                                                                 any
                   any    label: Z



         Fig. 26.        POS CASE of tac2: flat version (left) and a hierarchical version (right)

p¬Snd(tetl1 rl1 r1 ) = Snd(F stxtl1 rl1 r1 )q. The asm ante tac(?z) tactic is then ap-
plied. This is followed by a sequential application of rewrite sym thm tac(?case),
rewrite sym thm tac(?case) and def ault asm rewrite tac. The remaining part
are the same as tac1, i.e. it can be developed by using the LEMMA THEN1 pat-
tern. The right hand of Fig. 26 is the same as the left hand side, with hierarchies
introduced for increased readability.
   4.2.3 Discussion. The FEF case study is both ad hoc and domain specific, which
is very different from the tautology example in the previous section. It has provided
useful principles of how to apply PSGraph with a new perspective, where the goal
is to extract/understand rather than reflect the proof structure. As a result, the
proof structure follows more from instantiation of discovered proof patterns, rather
than an overall proof plan.
   The case study has provided us with a workbench to test robustness, and our
next step will be to change the FEF specification and see how to fix the proofs
in both ML and PSGraph and then compare the relative advantages. We could
also re-create the real world issue that the proof is part of a big induction and the
induction hypothesis has to be strengthened. This is a very common problem for
inductive proofs.
   The example has shown use of Tinker’s library function to reuse patterns and
how graph tactics can be parametrised by its input. However, it has also further
indicated the need to parametrise graph tactic by actual tactics rather than their
arguments, as we saw in the tautology example. Here, we provided dummy graph
nodes that had to be manually replaced. One example to overcome this, is to
allow tactics to be bound in the goal node environment; another example is to
configure/replace tactics in the graph tactics. For example,
 LEMMA THEN (config tac := another tac,?g)
   would replace tactic conf ig tac with a tactic another tac for this particular use
of the LEMMA THEN graph tactic.
                                                               Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
118     ·      Lin, Grov and Arthan

   As the Tinker tool is foremost a research vehicle we have by design made it generic
to work with multiple provers. Whilst we still think this is the right choice, a more
specialised version for a particular prover could offer a closer level of integration,
e.g. within the tool we have used @{term “ − ”}, more familiar for Isabelle users,
compared with ProofPower’s p − q representation.
4.3   Developing conversions
In this section we consider part of the implementation of a proof procedure de-
scribed in [3] that automates proofs that a function formed from a given set of
atomic morphisms by composition and pairing is a morphism in a concrete cat-
egory. The proof procedure is itself parametrized by theorems that characterize
the concrete category of interest and identify the atomic morphisms. So, for ex-
ample, when instantiated for the category of topological spaces and continuous
functions, with the arithmetic operators and the basic transcendental functions
as the atomic morphisms, the proof procedure will automatically prove that the
function λ(x, y)• (sin(x) + cos(y) + 1)2 is continuous.
  The first step in the decision procedure is to rewrite the λ-abstraction into a
combinator form. In our example, the first step will prove the following theorem
(which we state using the notation of [3] rather than ProofPower concrete syntax):
            `(λ(x, y)• (sin(x) + cos(y) + 1)2 ) =                                            (*)
                      2
              (λx• x ) ◦ Uncurry(+) ◦ hsin ◦ π1 , Uncurry(+) ◦ hcos ◦ π2 , K 1ii
The proof procedure then proves that the right-hand side of (*) is a morphism in
our category (i.e., a continuous function) by a process of backchaining with theo-
rems stating that the combinators preserve morhphismhood and that the atomic
functions are morphisms. See [3] for details. In this paper, we are only concerned
with the implementation of the first step.
   The implementation proves (*) by first applying a conversion λ unpair conv to
eliminate the paired abstraction19 , yielding
      ` (λ(x, y)• (sin(x) + cos(y) + 1)2 ) = (λp • (sin(π1 (p)) + cos(π2 (p)) + 1)2 )
(*) is then obtained by repeated application of the following system of rewrite rules
to the right-hand side of the above equation.
             (λx• x)       ;   I
              (λx• t)      ;   Kt                                    x 6∈ frees(t)
        (λx• (t1 , t2 ))   ;   h(λx• t1 ), (λx• t2 )i
            (λx• f t)      ;   f ◦ (λx• t)                           f ∈ unary
         (λx• g t1 t2 )    ;   Uncurry g ◦ h(λx• t1 ), (λx• t2 )i    g ∈ binary
           (λx• h t j)     ;   (λx • h x j) ◦ (λx• t)                h ∈ parametrized
Here I and K are the identity and constant combinators, ◦ is functional compo-
sition, hf, gi is λ(x, y)• (f x, g y) and Uncurry g is λ(x, y)• g x y. unary, binary and
parametrized denote sets of atomic morphisms that are parameters to the proof pro-
cedure: unary and binary contain functions of one and two arguments respectively

19 The implementation described here is slightly different from the algorithm described in [3] in
that it handles paired abstractions by pre-processing rather than inside the rewrite system.

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                           Understanding and maintaining tactics graphically        ·     119

and parametrized contains functions of two arguments where the second argument
is expected to be a constant. (The set parametrized is used to deal with families of
functions like exponentiation with natural number coefficients.)
   The ProofPower code that implements this rewrite system is the following.
ProofPower Code

val rec rec conv : CONV = (fn t => (FIRST C [
         i conv ,
         k conv ,
         pair conv THEN C RAND C (RANDS C (TRY C rec conv )),
         unary conv THEN C RIGHT C (TRY C rec conv ),
         binary conv THEN C
                  RIGHT C (RAND C (RANDS C (TRY C rec conv ))),
         parametrized conv THEN C RIGHT C (TRY C rec conv )]
                  AND OR C simp conv ) t);
   Here we have a conversion for each rule in the rewrite system, these are combined
using the function FIRST C which applies its argument conversions to a term in
turn until it finds one that does not fail. Note the above definition local to a
function morphism conv which takes as parameters the sets of unary, binary and
parametrized operators. The conversions i conv, k conv etc. each perform one
rewriting step. k conv, for example, attempts to rewrite a term at the outermost
level using the theorem
                                 ` ∀c• (λx• c) = K c
while binary conv attempts to rewrite at the outermost level using theorems ob-
tained from the following theorem:
                      ` ∀s t• (λx• f (sx)(tx) = Uncurry f ◦ hs, ti
by instantiating f to each of the binary atomic morphisms. If either of the first
two conversions succeeds there is nothing more to do. In the other four cases,
we must recursively apply the rewrite system to the λ-abstractions introduced by
the conversion. This is done using functions RAND C and RANDS C of type
CONV − > CONV , which apply their argument to the operand, respectively
operands, of a function application. I.e., if conv proves ` t = s, ` t1 = s1 , . . . , `
tm = sm , then RAND C conv proves all theorems of the form ` f t = f s and
RANDS C conv proves all theorems of the form ` g t1 . . . tm = g s1 . . . sm , where g
is not itself an application. The reader will observe that rec conv also does some-
thing that is not specified in the rewrite system: simp conv is a minor optimisation:
it was found in practice that the rewrite system is prone to produce subterms of the
form f ◦ I. While such subterms cause no problems with later processing, it is tidy
to rewrite away the unnecessary composition and this is done by simp conv, which
is combined with the implementation of the rewrite system using the conversion
combinator AND OR C, which does what its name suggests.
  4.3.1 The problem of transforming conversions into tactics. As with the other
case studies, we would like to transfer rec conv into PSGraph in order to achieve
a more intuitive representation to support future maintenance. However, PSGraph
works with tactics while rec conv is a conversion, and in order to use a conversion
                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
120     ·      Lin, Grov and Arthan

in PSGraph a conversion must first be transformed into a tactic. Functionality to
achieve this is provided by ProofPower via
SML

 val conv tac : CONV −> TACTIC
  Using this function we can for example turn our rec conv conversion into a tactic:
SML

 val conv rec tac : TACTIC = conv tac rec conv
  As we have seen, conversions are combined via a set of conversion combinators,
comparable to tacticals for tactics. To follow the same approach as in the previous
examples, we need to turn these into tacticals instead. For some examples we can
define algebraic laws to support this. For example, sequential composition:
  conv tac(conv1 THEN C conv2) = (conv tac conv1) THEN (conv tac conv2)
We can then use the same approach as before and turn conv tacconv1 and conv tac
conv2 into atomic tactics with a wire between them. The problem with this ap-
proach is in the presence of combinators such as RAND C, which doesn’t apply a
conversion to a term, but to the operands of a function of the term. E.g. given a
term pf x q , RAN D Cconv will apply conversion conv to px q . We will call the
family of conversion combinators that changes the “focus” of a term to a sub-term,
such as RAND C and RANDS C, for term focus combinators.
  Now, consider a conversion
SML

 RAND C (conv1 THEN C conv2 )
This will first change the focus of the term to the operand, and then apply conv1
followed by conv2 to the operand. We cannot naively break up the THEN C
combinator into the THEN tactical, as conv2 should work on the sub-term as a
result of the use of RAND C. For this case, we could again develop suitable algebraic
laws and “push” RAND C inwards, i.e.
SML

 (RAND C conv1 ) THEN C (RAND C conv2 ) )
We can then use the same approach as above to turn this into a tactic.
   A deeper problem for rec conv is the recursion: in several cases a conversion
is applied, followed by a recursive call wrapped in a term focus combiner, before
simp conv is applied to the pre-recursive focus. To achieve this in PSGraph, where
recursion becomes a feedback loop, each call needs to keep track of the “current”
term focus, together with the focus of the pre-call in order to apply simp conv
correctly.
  4.3.2 Encoding recursion with “term focusing” in PSGraph. Our solution when
implementing the rec conv conversion, is to augment the PSGraph with a variable
?rec. This will act as a stack (frame) that keeps track of each change of focus to a
term when entering a recursive step. This variable has type20

20 We have updated the allowed types in an environment for simplicity – we could just as well
used a list of names, and developed a parser to turn this into a conversion.

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                                     Understanding and maintaining tactics graphically                                        ·   121

                   is_cconv1_list(?cc)
                                                                                              any
                    rec_conv(?cc)                                                     ?rec:= ?cc
                            any                                                       any
                                                                                                      more_conv(?rec)
                                         any
                                                                                                 is_rec_conv(?rec)
                                                                             is_k_conv(?rec)
                             is_simp_conv(?rec)
                                                         is_i_conv(?rec)           lift_conv            recursion(?rec)
                                lift_conv                                       (k_conv, ?rec)
                           (simp_conv, ?rec)                                                           !more_conv(?rec)
                                                               lift_conv               any
               !is_simp_conv(?rec)     any                  (i_conv, ?rec)                             ENV_pop(?rec)
                                                                                any             any
                           any                                  eq(?rec, ?cc)
                                                                                                             !eq(?rec, ?cc)
                TRY_simp_conv(?rec)                      TRY_simp_conv(?rec)                !eq(?rec, ?cc)

                            any                                   any         eq(?rec, ?cc)     post_recursion(?rec)

                   ENV_pop(?rec)
                            any



                       is_param_conv(?rec)                         is_pair_conv(?rec)
                                                          any
                                                                                     lift_conv
                               lift_conv
                                                                                (pair_conv, ?rec)
                          (unary_conv, ?rec)
                                                            is_binary_conv(?rec)          any
                                     is_unary_conv(?rec)
                                                        lift_conv
                                                  (binary_conv, ?rec)                   ENV_push
                           any                                                  (RAND_C o RANDS_C, ?rec)
                                         lift_conv
                                                                   any
                                    (param_conv, ?rec)
                                        any                                                                    any
                                                                      ENV_push
                               ENV_push
                                                         (RIGHT_C o RAND_C o RANDS_C, ?rec)
                            (RIGHT_C, ?rec)
                                    any                                         any



              Fig. 27.        Encoding recursion with “term focusing” in PSGraph

 ?rec : (CONV −> CONV ) list
   The idea is as follows. For each application of a conversion, we first sequentially
compose all elements of ?rec and apply this to focus the correct place in a term
followed by the application of a conversion. We specialise conv tac with a tactic
that takes these two arguments:
ML

lift conv : (CONV −> CONV ) list −> CONV −> tactic
Here, the first argument is a list of term focusing combinators and the second
argument is desired conversion. lift conv has the following semantics:
                                                                                
             lift conv [f1 ; . . . ; fn ]conv = conv tac (fn ◦ . . . ◦ f1 ) conv
   If this conversion is followed by a recursive application, then the “term focus
combinators” are pushed to the ?rec stack. This is achieved by an environment
tactic ENV push(conv,var), which takes one of these conversion combinators and
a variable as argument.
   Once the recursion has completed simp conv should be applied to each operand,
in the inverse order of the recursion (i.e. the last sub-term that a conversion was ap-
plied to should be simplified first). This is achieved by using ?rec, and apply simp
conv, followed by popping an element of it until ?rec is empty. The environment
tactic ENV pop(var) applies such a single ‘pop’ operation.
   The encoding of this strategy is shown in Fig. 27. It takes an input goal with
an environment containing a variable ?cc, which has the “term focus” on entry

                                                                 Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
122     ·      Lin, Grov and Arthan

(and exit). It initialises ?rec to this value. The i conv and k conv conversions
are applied without any recursion, as described above. For the other cases, the
recursion graph tactic is added. For each case conversion c, i.e. each element of
the list of rec conv we develop an atomic goal type, called is c conv. For the graph
tactic, is rec conv is just the disjunction of the four recursive cases:
                          is   rec   conv(X)   ←   is   unary conv(X).
                          is   rec   conv(X)   ←   is   param conv(X).
                          is   rec   conv(X)   ←   is   binary conv(X).
                          is   rec   conv(X)   ←   is   pair conv(X).
For each of the cases, the conversion is applied and then the focus of the term is
changed. For example pair conv is followed by two applications of RAND C and
then a recursive call again to rec conv. Thus, for this case, RAND C ◦ RAND C is
added to ?rec.
  The recursion stops when there are no further applicable conversions, i.e. when
none of the goal types succeed. This is the negation of the case where any of the
conversion goal types are satisfied, i.e.:
                               more conv(X) ← is i conv(X).
                               more conv(X) ← is k conv(X).
                               more conv(X) ← is rec conv(X).
On exit, the last change of focus is removed (as it failed for this application), and we
enter the post recursion graph tactic, unless the case where ?rec is still the same as
?cc. This indicates that none of the recursive calls succeeded. In this graph tactic,
the simp conv will be applied for the same sub-terms as in the recursive case (due
to the feedback loop around the tactic). When ?rec is the same as ?cc, the loop is
terminated, which ends the proof.
   4.3.3 Discussion. When contrasting the ML code of rec conv in the start of the
section with the corresponding PSGraph in Fig. 27, one can see that choices made
are much more declarative; the parallel view of the choice of conversion, which one
had in mind in the first place, is clear to see compared with the sequential ordering
of the ML code. One of the most common bugs in such development is to get the
scheduling wrong, and, as we saw with the tautology example, PSGraph is good at
supporting this type of debugging.
   The use of conversions is very common: they are used heavily in our work with
D-RisQ’s powerful tactic [43], where we are developing conversions to port the tactic
from verification of Ada programs to C. The work presented here is a starting point
which has exposed a lot interesting questions when dealing with low-levels issue
involving terms and rewriting. In particular, how to evaluate sub-parts of terms
within a given context across multiple boxes in an efficient way. In the presented
solution we had to re-build data structures from outside and inwards for each box
before actually applying the rewriting, which is very expensive.
   One way to overcome this in the future is to augment the goal node with the
current focus of a goal (conclusion and/or hypothesis). Huet’s Zippers [33], which
combines a tree with a sub-tree of focus, including operations to this focus move
up/down/sideways could for example be applied. This has been implemented for
a term representation similar to ProofPower’s in [16]. Another option is Grundy’s
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                          Understanding and maintaining tactics graphically        ·     123

window inference[28], which will also build up contextual information when focus
is shifted to a sub-term.
   Another question is whether tactics and conversions should be treated uniformly
or separately. To treat conversions separately would be a more radical extension to
PSGraph, perhaps involving a new conversion graph notation devoted to equational
reasoning, in which the boxes would denote conversions rather than tactics.

5.   RELATED WORK
Motivated mainly by large scale proof developments, such as the Coq proof of the
four colour theorems [23], the HOL light proof of the Kepler conjecture [29] and the
Isabelle verification of the seL4 micro-kernel [38], ideas from software engineering
have started to make their way into proof development. The term proof engineering
has been used for this new discipline [37]. This includes topics such as productivity
of proofs [62] as well as proof metrics [7].
   Whilst we put the work presented here in this context of proof engineering, our
motivation and focus is different from the above work. Instead of being motivated
by large proof developments and their proofs, our motivation has been development
and maintenance of a large proof strategy (i.e. tactic) in an industrial setting,
using a graphical representation [43]. There has been a considerable amount of
work on visualising proof trees, including: LΩUI [58] for Ωmega; XIsabelle [49] for
Isabelle; ProveEasy [12] and Jape [9] for teaching; and some more recent work for
Mizar [41, 50]. However, none of these visualise the high-level strategy. This raises
the question of what the difference between a proof and proof strategy is (in a
mechanical theorem proving setting)? If one think of tactics as proof strategies,
then a proof strategy is really just a procedural description of how to conduct the
search for a proof. Bundy [11] on the other hand, has argued for the additional role
of explanation. We hope that we have shown how PSGraph can help explaining the
strategy of a proof in addition to be used to guide the search. Such explanation
is important for maintenance when team changes, and our work with D-RisQ [43]
has had very promising initial results when porting their proof tactics from Ada to
C verification.
   Through case studies, we have conducted a comprehensive comparison of PS-
Graph with ProofPower’s tactic language. This language is very similar to the
tactic languages found in LCF-based provers such as HOL4, HOL light, and Is-
abelle. LTac for Coq [15] and Eisbach for Isabelle [46] provide support for tactic
development within the proof scripts. They support matching features similar to
the environment tactic and goal types of PSGraph. However, the composition of
tactics is closer to the more traditional tactic languages and they do not contain
debugging features as presented for PSGraph here. In proof planning [10] tactics
are given pre-conditions and post-conditions, which can be achieved by the goal
types of PSGraph. IsaPlanner [16] is a proof planner for Isabelle, and the PSGraph
project started out as a new composition (tactic) language for IsaPlanner (which
was similar to ProofPower’s tactic language). There are also several typed tactic
languages, e.g. VeriML [61], Beluga [53], Delphin [54] and Mtac [67]. Here the
types contain information about the relationship between tactics and the proofs
produced. For VeriML, Beluga and Delphin there is a clear separation between
the tactic and the base logic. It is not clear how they can be incorporated in an
                                         Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
124       ·     Lin, Grov and Arthan

established theorem prover, as we have detailed for PSGraph and ProofPower here.
Mtac is an extension to Coq and, as with LTac, does not address the issues of
maintenance and usability we are focusing on, albeit with improved static (com-
position) properties through types. Autexier and Dietrich [8] have developed a
declarative tactic language on top of a declarative proof language where a strategy
is represented as a schema which needs to be instantiated. Their work is more
declarative than PSGraph, whilst PSGraph handles tactic compositions in a more
declarative way. However, it is not clear how issues such as debugging is helped by
such schemas. There have also been several attempts to create declarative tactic
languages on top of procedural tactic languages [31, 22]. Asperti et al [5] argues
that these approaches suffer from two drawbacks: goal selection for multiple sub-
goals, and information flow between tactics – both of these are addressed by goal
types in PSGraph. Finally, HiTac is a tactic language with additional support for
hiding complexities using hierarchies [6], which our notion of hierarchies is based
upon. Hierarchies in HiTacs are restricted to single inputs, which probably makes
the semantics simpler and more elegant, whereas our approach, which utilises goal
types, has followed from a more practical and empirical approach. HiTac has pre-
dominantly been used for more theoretical work, and as with VeriML, Beluga and
Delphin, it has not been integrated into an established theorem prover.
   As the evaluation was partly exploratory in nature, a case study approach was
chosen as case studies are considered suitable for qualitative analysis [57]. The fact
that the third author (Arthan) was new to PSGraph also provide new and more
objective reflections in this work. For quantitative results, an alternative approach
would have been to set up a controlled experiments, e.g. where participants are
given suitable training with both ProofPower’s tactic languages and PSGraph, and
are then asked to explain and identify/repair faulty proof strategies. We can then
measure the time and compute and compare their mean time to repair (MTTR)
metric [20, p.462]. There are also models for maintainability that are based upon
activities, which may be more suitable as they have been applied to both text-
based code and (graphical) Simulink models (in industrial settings) [14]. This can
form the basis for future experiments. We could also try to measure and compare
structural factors of the two representations, however metrics for both usability [20,
p.460] and maintainability (e.g. the maintainability index (MI) [48]) are tailored
for linear languages and would not be applicable to our graphical language. To
illustrate, MI combines measures such as lines of code, cyclomatic complexity and
Halstead effort21 [30].
   We have studied and contrasted programs written in different languages. How-
ever, what we are really interested is the usabilty and maintainability provided by
the languages themselves. In §1 we gave one example from cognitive science that
shows that humans find it more natural to comprehend flow networks diagram-
matically compared with linear (term-based) representations [39]. Block-based lan-
guages, such as Logo [21], Scratch [56], Alice [13] and AppInventor [66], are similar
to PSGraph in that programs are inter-connecting blocks. Block-based languages
are popular within CS education and there have been some studies comparing them
with traditional languages. E.g. [63] found that the drag-and-drop mechanism

21 This   is computed using the number of operators, operands and program length.

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                            Understanding and maintaining tactics graphically         ·     125

and the ease of browsing block-based libraries were advantageous; whilst perceived
drawbacks relate to expressibility and scalability. Besides this, we are not familiar
with any work comparing actual languages22 . Simulink’s popularity for embedded
systems shows industrial use of graphical languages for certain types of systems.
   We are not familiar with any work on case studies in refactoring proof tactics as
comprehensive as the work presented in the present paper. Whiteside (with others)
has developed a refactoring framework for hierarchical proofs (HiProofs) [65, 64],
however this work focused mainly on proofs rather than proof strategies, albeit
including some work on folding and unfolding tactics. The most relevant tool to
ours, which we are familiar with, is the aforementioned Tactician tool to refactor
proofs in HOL light [2]. In HOL light (as is also the case for ProofPower) a proof
can be a sequence of (interactive) ‘apply’ step, or they can be combined into a single
step (by means of tactic combinators) which is then applied. Tactician is a tool
to fold sequences into a single tactic and unfold a tactic into a sequence of steps.
This can then be used for debugging by enable users to step through a large tactic,
similar to how this can be achieved with Tinker. However, it only work for a small
subset of ML and it is not clear how this approach can be generalised to arbitrary
tactics. Moreover, it unfolds only one particular branch of the proof which does
not necessarily reflect the underlying proof strategy.
   Another tool recently developed to support debugging is the new tracing mech-
anism for the simp tactic in Isabelle [34]. This is implemented as plug-in for the
Isabelle/jEdit Prover IDE. It supports hierarchical viewing of simplification traces,
and, as with Tinker, it enables breakpoints to be inserted where the user can step
through and interact with the tactic. The breakpoints can either be an application
of certain theorems or if the subgoal matches certain patterns. Note that it is not
used to debug the (sub-)tactics used to implement the simplifier: it will only show
how the simplifier applies rewrite steps. Our logging mechanism is considerably
simpler, and closer to the more rudimentary ones supported in other ITP systems
(including the previous tracing mechanism for the simp tactic in Isabelle). How-
ever, in practice we have found that our logging mechanisms is sufficient as it only
relates to a step at a time, while the simp tactic could involve hundreds of steps.

6.   CONCLUSION & FUTURE WORK
We have extended our graphical approach for tactic development with features to
support development and debugging of proof strategies. Through examples, we
have shown relative advantages when it comes to understanding and debugging
proof strategies compared with ML code, which is part of the hypothesis addressed
here. We would argue that maintenance is a consequence of this, and aim to further
study this this by completing the tasks set out in the FEF case study.
   The experiments have provided some valuable lessons. The inclusion of PSGraph
into a theorem prover should be seen to be evolutionary rather than revolutionary;
it should be seen as a new tool in the ecosystem for LCF-style theorem proving
systems. An important feature is that you can still develop standard tactics using
tacticals and treat them as atomic in PSGraph. This is a positive, and, with some

22 There
       has been some more interest recently, as illustrated by a SIG meeting on usability of
programming languages at CHI 2016.

                                            Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
126     ·      Lin, Grov and Arthan

better integration with particular theorem proving and SML system, you will still
have the old version with an additional tool. It should also be noted that Tinker
has been connected to a non-SML based prover: Rodin is developed using Java
[40].
   To use PSGraph effectively, one needs to change from a purely procedural view
of tactics to more declarative thinking. There are trade-offs to be made between a
graphical, declarative and parallel approach on the one hand and the (hopefully)
concise higher-order functional programming approach on the other. Whilst losing
some of the power of functional programming, the graphical approach is intrinsically
more accessible. In a world where teams change, a solution perceived as elegant by
the original developer may be perceived as incomprehensible and unmaintainable by
his or her successors, particularly as the raw code of a tactic does not document why
design choices were made. If this is true for experts on tactics – then what would
‘Joe Engineer’ prefer if this technology is to become mainstream? One compromise
between procedural and declarative styles may be to think about how to represent
tacticals graphically. PSGraph is essentially a way of composing tactics. A way
forward may be to first just replace tacticals with similar graphical tactics: this
was illustrated this in the FEF case study, while [26] shows some common tacticals
graphically.
   Technically, in order to use PSGraph with a new theorem prover all that has to
be done is to implement a ML signature which tells PSGraph how to work with the
proof state of that prover. Detailed information of how this is done in ProofPower
can be found in [42].
   The case studies have shown some limitations with PSGraph that need to be
addressed. This includes, more parametric graph tactics to enable better re-use and
modularity; closer integration with the theorem proving system to make it more
natural for users; and low level term manipulations and rewriting, as illustrated
by our encoding of conversions. Building on the FEF case study we would also
like to test the robustness and maintainability, and contrast this with the linear
tactic language such as ML. Another experiment we would like to conduct is to
start from scratch and implement known (or even unknown) decision procedures in
PSGraph (e.g. quantifier elimination), and start building up a library that can help
in general. It will also be interesting to see how PSGraph can be used as explanation
of existing large libraries (e.g. the AFP for Isabelle or the Mizar library) – or even
as a good representation when writing papers on new decision procedures.
   As PSGraph is implemented as a generic tool, and not specialised to a particular
theorem prover, it may provide a way of translating proof strategies between the-
orem proving systems. While OpenTheory [35] relies on the low-level similarities
of the LCF kernels to translate proofs, PSGraph could potentially help exporting
high-level proof strategies. This would require some minimal set of atomic tactics
and goal types and just use them (with a defined semantics). Short term we could
at least carry across structures of proof strategies, where the user needs to fill in
the details in terms of atomic tactics and goal types. PSGraph could also be an
experimental way of developing proof procedures, acting as the “source code” with
tactic languages as the “target code” as they are likely to be more efficient than
our graph interpreter. It is however not clear how to do such compilation; possibly
bottom-up in an interactive manner.
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                             Understanding and maintaining tactics graphically          ·     127

  We have shown how our graphical representation can help to explain and support
maintenance of selected examples from a real-world system. The next challenge is
to continue our work with D-RisQ [43] on their 10K LoC tactic. Here, we believe
that PSGraph can provide real economic advantages in terms of reduced develop-
ment costs, reduced maintenance costs and improved communication with the user
community.

References
 [1] IEEE Standard 610.12-1990. Standard Glossary of Software Engineering, Terminology. IEEE
     Computer Society Press, 1993. 70
 [2] Mark Adams. Refactoring proofs with tactician. In Domenico Bianculli, Radu Calinescu, and
     Bernhard Rumpe, editors, Software Engineering and Formal Methods: SEFM 2015. Revised
     Selected Papers, pages 53–67, Berlin, Heidelberg, 2015. Springer. 108, 125
 [3] Rob Arthan. Now f is continuous (exercise!). Journal of Formalized Reasoning, 9(1):33–52,
     2016. 118
 [4] Rob Arthan and Roger Bishop Jones. Z in HOL in ProofPower. BCS FACS FACTS, 2005-1.
     http://www.bcs.org/upload/pdf/facts200503.pdf. 70, 71
 [5] Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. A new type
     for tactics. In PLMMS’09, pages 229–232, 2009. 124
 [6] David Aspinall, Ewen Denney, and Christoph Lüth. A Tactic Language for Hiproofs. In
     MKM’08, pages 339–354, Berlin, Heidelberg, 2008. Springer-Verlag. 124
 [7] David Aspinall and Cezary Kaliszyk. Towards formal proof metrics. In Perdita Stevens
     and Andrzej Wasowski, editors, Fundamental Approaches to Software Engineering: 19th
     International Conference, FASE 2016, pages 325–341, Berlin, Heidelberg, 2016. Springer.
     123
 [8] Serge Autexier and Dominik Dietrich. A Tactic Language for Declarative Proofs. In ITP’10,
     volume 6172 of LNCS, pages 99–114. Springer, 7 2010. 124
 [9] Richard Bornat and Bernard Sufrin. Jape: A calculator for animating proof-on-paper. In
     CADE-14, pages 412–415. Springer, 1997. 123
[10] Alan Bundy. A science of reasoning. In Computational Logic - Essays in Honor of Alan
     Robinson, pages 178–198, 1991. 123
[11] Alan Bundy. A science of reasoning. In International Conference on Automated Reasoning
     with Analytic Tableaux and Related Methods, pages 10–17. Springer, 1998. 123
[12] Rod Burstall. Proveeasy: Helping people learn to do proofs. ENTCS, 31(0):16 – 32, 2000.
     123
[13] Stephen Cooper, Wanda Dann, and Randy Pausch. Alice: a 3-d tool for introductory pro-
     gramming concepts. In Journal of Computing Sciences in Colleges, volume 15, pages 107–116.
     Consortium for Computing Sciences in Colleges, 2000. 124
[14] Florian Deissenboeck, Stefan Wagner, Markus Pizka, Stefan Teuchert, and J-F Girard. An
     Activity-Based Quality Model for Maintainability. In 2007 IEEE International Conference
     on Software Maintenance, pages 184–193. IEEE, 2007. 124
[15] David Delahaye. A Proof Dedicated Meta-Language. Electronic Notes in Theoretical Com-
     puter Science, 70(2):96–109, 2002. 123
[16] Lucas Dixon and Jacques D. Fleuriot. IsaPlanner: A Prototype Proof Planner in Isabelle.
     In CADE-19, volume 2741 of LNCS, pages 279–283. Springer, 2003. 122, 123
[17] Lucas Dixon and Aleks Kissinger.        Open Graphs and Monoidal Theories.          CoRR,
     abs/1011.4114, 2010. 80
[18] Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. Fundamentals of
     Algebraic Graph Transformation. Monographs in Theoretical Computer Science. Springer,
     2006. 80
[19] Colin Farquhar, Gudmund Grov, Andrew Cropper, Stephen Muggleton, and Alan Bundy.
     Typed meta-interpretive learning for proof strategies. In Late Breaking Papers of ILP2015,
     volume 1636, pages 17–32. CEUR Workshop Proceedings, 2016. 89, 93
                                              Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
128     ·      Lin, Grov and Arthan

[20] Norman Fenton and James Bieman. Software Metrics: A Rigorous and Practical Approach.
     CRC Press, 2014. 124
[21] Wallace Feurzeig et al. Programming-languages as a conceptual framework for teaching
     mathematics. final report on the first fifteen months of the logo project. 1969. 124
[22] Mariusz Giero and Freek Wiedijk. MMode, a Mizar Mode for the proof assistant Coq.
     Technical report, January 07 2004. 124
[23] Georges Gonthier. A computer-checked proof of the four colour theorem, 2005. 123
[24] Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF, vol-
     ume 78 of Lecture Notes in Computer Science. Springer, 1979. 71
[25] Mike Gordon. From LCF to HOL: a short history. In Gordon D. Plotkin, Colin Stirling, and
     Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner,
     pages 169–186. The MIT Press, 2000. 71, 75
[26] Gudmund Grov, Aleks Kissinger, and Yuhui Lin. A Graphical Language for Proof Strategies.
     In LPAR, pages 324–339. Springer, 2013. 70, 88, 126
[27] Gudmund Grov, Aleks Kissinger, and Yuhui Lin. Tinker, Tailor, Solver, Proof. In UITP
     2014, volume 167 of ENTCS, pages 23–34. Open Publishing Association, 2014. 70, 83
[28] Jim Grundy. Window inference in the HOL system. In International Workshop on HOL
     Theorem Proving System and Its Applications, pages 177–189. IEEE, 1991. 123
[29] Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le
     Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, et al. A
     formal proof of the kepler conjecture. arXiv preprint arXiv:1501.02155, 2015. 123
[30] Maurice Howard Halstead. Elements of software science, volume 7. Elsevier, 1977. 124
[31] John Harrison. A Mizar Mode for HOL. In TPHOLs, volume 1125 of LNCS, pages 203–220.
     Springer, 1996. 124
[32] John Harrison. HOL light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian
     Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd Inter-
     national Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings,
     volume 5674 of LNCS, pages 60–66. Springer, 2009. 70, 71
[33] Gérard Huet. The zipper. Journal of functional programming, 7(05):549–554, 1997. 122
[34] Lars Hupel. Interactive simplifier tracing and debugging in isabelle. In Stephen M. Watt,
     James H. Davenport, Alan P. Sexton, Petr Sojka, and Josef Urban, editors, CICM, pages
     328–343, Cham, 2014. Springer. 125
[35] Joe Hurd. OpenTheory: Package management for higher order logic theories. In Gabriel Dos
     Reis and Laurent Théry, editors, PLMMS ’09: Proceedings of the ACM SIGSAM 2009
     International Workshop on Programming Languages for Mechanized Mathematics Systems,
     pages 31–37, August 2009. 126
[36] Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A Proof Assistant for Diagrammatic
     Reasoning. In CADE-25, volume 9195 of LNCS, pages 326–336. Springer, 2015. 84
[37] Gerwin Klein. Proof engineering considered essential. In FM 2014: Formal Methods, pages
     16–21. Springer, 2014. 123
[38] Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal
     Kolanski, and Gernot Heiser. Comprehensive formal verification of an os microkernel. ACM
     Transactions on Computer Systems (TOCS), 32(1):2, 2014. 123
[39] Jill H Larkin and Herbert A Simon. Why a diagram is (sometimes) worth ten thousand
     words. Cognitive science, 11(1):65–100, 1987. 70, 124
[40] Yibo Liang, Yuhui Lin, and Gudmund Grov. ‘the tinker’ for rodin. In Michael Butler, Klaus-
     Dieter Schewe, Atif Mashkoor, and Miklos Biro, editors, Abstract State Machines, Alloy, B,
     TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27,
     2016, Proceedings, pages 262–268. Springer, 2016. 70, 126
[41] Tomer Libal, Martin Riener, and Mikheil Rukhaia. Advanced Proof Viewing in ProofTool.
     In UITP 2014, volume 167 of EPTCS, pages 35–47. Open Publishing Association, 2014. 123
[42] Yuhui Lin, Gudmund Grov, and Rob Arthan. Debugging and refactoring tactics graphically
     – paper resources. http://ggrov.github.io/tinker/jfr16/. Accessed: July 2016. 71, 84,
     115, 126

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                             Understanding and maintaining tactics graphically          ·     129

[43] Yuhui Lin, Gudmund Grov, Colin O’Halloran, and G Priiya. A Super Industrial Application
     of PSGraph. In International Conference on Abstract State Machines, Alloy, B, TLA, VDM,
     and Z, pages 319–325. Springer, 2016. 70, 94, 122, 123, 127
[44] Yuhui Lin, Pierre Le Bras, and Gudmund Grov. Developing and debugging proof strategies
     by tinkering. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms
     for the Construction and Analysis of Systems (TACAS), pages 573–579, Berlin, Heidelberg,
     2016. Springer. 70, 83, 84
[45] Makarius Wenzel and many others. The Isabelle/Isar Reference Manual.
     http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/isar-ref.pdf. 70, 71
[46] Daniel Matichuk, Makarius Wenzel, and Toby Murray. An isabelle proof method language.
     In Gerwin Klein and Ruben Gamboa, editors, 5th International Conference on Interactive
     Theorem Proving, pages 390–405, Cham, 2014. Springer. 123
[47] Colin O’Halloran. Automated Verification of Code Automatically Generated from Simulink.
     ASE, 20(2):237–264, 2013. 70
[48] P Oman, J Hagemeister, and D Ash. A definition and taxonomy for software maintainability,
     report setl report 91-08-tr. University of Idaho, 1991. 124
[49] Maris A Ozols, Anthony Cant, and Katherine A Eastaughffe. Xisabelle: A system description.
     In CADE-14, pages 400–403. Springer, 1997. 123
[50] Karol Pak. The algorithms for improving and reorganizing natural deduction proofs. Studies
     in Logic, Grammar and Rhetoric, 22(35):95–112, 2010. 123
[51] Lawrence C. Paulson. A higher-order implementation of rewriting. Sci. Comput. Program.,
     3(2):119–149, 1983. 73
[52] Lawrence C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF.
     Cambridge University Press, New York, NY, USA, 1987. 98, 99, 100
[53] Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract
     syntax and first-class substitutions. In ACM SIGPLAN Notices, volume 43, pages 371–382.
     ACM, 2008. 123
[54] Adam Poswolsky and Carsten Schürmann. System description: Delphin–a functional pro-
     gramming language for deductive systems. Electronic Notes in Theoretical Computer Science,
     228:113–120, 2009. 123
[55] Gill Prout, Rob Arthan, Roger Jones, and Roger Stokes. The Front End Filter Project:
     specification and verification of a secure database system. http://www.lemma-one.com/
     ProofPower/fef/fef.html. 108, 109, 110
[56] Mitchel Resnick, John Maloney, Andrés Monroy-Hernández, Natalie Rusk, Evelyn Eastmond,
     Karen Brennan, Amon Millner, Eric Rosenbaum, Jay Silver, Brian Silverman, et al. Scratch:
     programming for all. Communications of the ACM, 52(11):60–67, 2009. 124
[57] Per Runeson and Martin Höst. Guidelines for conducting and reporting case study research
     in software engineering. Empirical software engineering, 14(2):131–164, 2009. 71, 96, 124
[58] Jörg H. Siekmann, Stephan M. Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin
     Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis,
     Martin Pollet, and Volker Sorge. LOUI: Lovely OMEGA User Interface. Formal Asp. Comput,
     11(3):326–342, 1999. 123
[59] Konrad Slind and Michael Norrish. A brief overview of HOL4. In Theorem Proving in Higher
     Order Logics (TPHOLs), volume 5170 of LNCS. Springer, 2008. 70, 71
[60] J Michael Spivey. The Z Notation: A Reference Manual, Second Edition. Prentice-Hall,
     1992. 72
[61] A. Stampoulis and Z. Shao. VeriML: Typed Computation of Logical Terms inside a Language
     with Effects. In ICFP, pages 333–344. ACM, 2010. 123
[62] Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein, and Rafal Kolanski.
     Productivity for proof engineering. In Proceedings of the 8th ACM/IEEE International
     Symposium on Empirical Software Engineering and Measurement, page 15. ACM, 2014. 123
[63] David Weintrop and Uri Wilensky. To block or not to block, that is the question: stu-
     dents’ perceptions of blocks-based programming. In Proceedings of the 14th International
     Conference on Interaction Design and Children, pages 199–208. ACM, 2015. 124

                                              Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
130     ·      Lin, Grov and Arthan

[64] Iain Whiteside. Refactoring Proofs. PhD thesis, University of Edinburgh, 2013. 125
[65] Iain Whiteside, David Aspinall, Lucas Dixon, and Gudmund Grov. Towards Formal Proof
     Script Refactoring. In CICM’11, volume 6824 of LNCS, pages 260–275. Springer, 2011. 125
[66] David Wolber, Hal Abelson, Ellen Spertus, and Liz Looney. App Inventor. ” O’Reilly Media,
     Inc.”, 2011. 124
[67] Beta Ziliani, Derek Dreyer, Neelakantan R Krishnaswami, Aleksandar Nanevski, and Viktor
     Vafeiadis. Mtac: a monad for typed tactic programming in coq. In ACM SIGPLAN Notices,
     volume 48, pages 87–100. ACM, 2013. 123




Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
