# Theory Abstract_Rules

theory Abstract_Rules
imports
Abstract_Formula
begin
text ‹
Next, we can define a logic, by giving a set of rules.
In order to connect to the AFP entry Abstract Completeness, the set of rules is a stream; the only
relevant effect of this is that the set is guaranteed to be non-empty and at most countable. This
has no further significance in our development.
Each antecedent of a rule consists of
▪ a set of fresh variables
▪ a set of hypotheses that may be used in proving the conclusion of the antecedent and
▪ the conclusion of the antecedent.
Our rules allow for multiple conclusions (but must have at least one).
In order to prove the completeness (but incidentally not to prove correctness) of the incredible
proof graphs, there are some extra conditions about the fresh variables in a rule.
▪ These need to be disjoint for different antecedents.
▪ They need to list all local variables occurring in either the hypothesis and the conclusion.
▪ The conclusions of a rule must not contain any local variables.
›