1.1 --- a/doc-src/IsarRef/Thy/Generic.thy Sat Jun 04 22:09:42 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy Sun Jun 05 20:15:47 2011 +0200
1.3 @@ -773,6 +773,111 @@
1.4 *}
1.5
1.6
1.7 +subsection {* Rule declarations *}
1.8 +
1.9 +text {* The proof tools of the Classical Reasoner depend on
1.10 + collections of rules declared in the context, which are classified
1.11 + as introduction, elimination or destruction and as \emph{safe} or
1.12 + \emph{unsafe}. In general, safe rules can be attempted blindly,
1.13 + while unsafe rules must be used with care. A safe rule must never
1.14 + reduce a provable goal to an unprovable set of subgoals.
1.15 +
1.16 + The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P
1.17 + \<or> Q"} to @{text "P"}, which might turn out as premature choice of an
1.18 + unprovable subgoal. Any rule is unsafe whose premises contain new
1.19 + unknowns. The elimination rule @{text "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} is
1.20 + unsafe, since it is applied via elim-resolution, which discards the
1.21 + assumption @{text "\<forall>x. P x"} and replaces it by the weaker
1.22 + assumption @{text "P t"}. The rule @{text "P t \<Longrightarrow> \<exists>x. P x"} is
1.23 + unsafe for similar reasons. The quantifier duplication rule @{text
1.24 + "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} is unsafe in a different sense:
1.25 + since it keeps the assumption @{text "\<forall>x. P x"}, it is prone to
1.26 + looping. In classical first-order logic, all rules are safe except
1.27 + those mentioned above.
1.28 +
1.29 + The safe~/ unsafe distinction is vague, and may be regarded merely
1.30 + as a way of giving some rules priority over others. One could argue
1.31 + that @{text "(\<or>E)"} is unsafe, because repeated application of it
1.32 + could generate exponentially many subgoals. Induction rules are
1.33 + unsafe because inductive proofs are difficult to set up
1.34 + automatically. Any inference is unsafe that instantiates an unknown
1.35 + in the proof state --- thus matching must be used, rather than
1.36 + unification. Even proof by assumption is unsafe if it instantiates
1.37 + unknowns shared with other subgoals.
1.38 +
1.39 + \begin{matharray}{rcl}
1.40 + @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.41 + @{attribute_def intro} & : & @{text attribute} \\
1.42 + @{attribute_def elim} & : & @{text attribute} \\
1.43 + @{attribute_def dest} & : & @{text attribute} \\
1.44 + @{attribute_def rule} & : & @{text attribute} \\
1.45 + @{attribute_def iff} & : & @{text attribute} \\
1.46 + @{attribute_def swapped} & : & @{text attribute} \\
1.47 + \end{matharray}
1.48 +
1.49 + @{rail "
1.50 + (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
1.51 + ;
1.52 + @@{attribute rule} 'del'
1.53 + ;
1.54 + @@{attribute iff} (((() | 'add') '?'?) | 'del')
1.55 + "}
1.56 +
1.57 + \begin{description}
1.58 +
1.59 + \item @{command "print_claset"} prints the collection of rules
1.60 + declared to the Classical Reasoner, i.e.\ the @{ML_type claset}
1.61 + within the context.
1.62 +
1.63 + \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
1.64 + declare introduction, elimination, and destruction rules,
1.65 + respectively. By default, rules are considered as \emph{unsafe}
1.66 + (i.e.\ not applied blindly without backtracking), while ``@{text
1.67 + "!"}'' classifies as \emph{safe}. Rule declarations marked by
1.68 + ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
1.69 + \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
1.70 + of the @{method rule} method). The optional natural number
1.71 + specifies an explicit weight argument, which is ignored by the
1.72 + automated reasoning tools, but determines the search order of single
1.73 + rule steps.
1.74 +
1.75 + Introduction rules are those that can be applied using ordinary
1.76 + resolution. Their swapped forms are generated internally, which
1.77 + will be applied using elim-resolution. Elimination rules are
1.78 + applied using elim-resolution. Rules are sorted by the number of
1.79 + new subgoals they will yield; rules that generate the fewest
1.80 + subgoals will be tried first. Otherwise, later declarations take
1.81 + precedence over earlier ones.
1.82 +
1.83 + Rules already present in the context with the same classification
1.84 + are ignored. A warning is printed if the rule has already been
1.85 + added with some other classification, but the rule is added anyway
1.86 + as requested.
1.87 +
1.88 + \item @{attribute rule}~@{text del} deletes all occurrences of a
1.89 + rule from the classical context, regardless of its classification as
1.90 + introduction~/ elimination~/ destruction and safe~/ unsafe.
1.91 +
1.92 + \item @{attribute iff} declares logical equivalences to the
1.93 + Simplifier and the Classical reasoner at the same time.
1.94 + Non-conditional rules result in a safe introduction and elimination
1.95 + pair; conditional ones are considered unsafe. Rules with negative
1.96 + conclusion are automatically inverted (using @{text "\<not>"}-elimination
1.97 + internally).
1.98 +
1.99 + The ``@{text "?"}'' version of @{attribute iff} declares rules to
1.100 + the Isabelle/Pure context only, and omits the Simplifier
1.101 + declaration.
1.102 +
1.103 + \item @{attribute swapped} turns an introduction rule into an
1.104 + elimination, by resolving with the classical swap principle @{text
1.105 + "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position. This is mainly for
1.106 + illustrative purposes: the Classical Reasoner already swaps rules
1.107 + internally as explained above.
1.108 +
1.109 + \end{description} *}
1.110 +
1.111 +
1.112 subsection {* Basic methods *}
1.113
1.114 text {*
1.115 @@ -904,78 +1009,6 @@
1.116 *}
1.117
1.118
1.119 -subsection {* Declaring rules *}
1.120 -
1.121 -text {*
1.122 - \begin{matharray}{rcl}
1.123 - @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.124 - @{attribute_def intro} & : & @{text attribute} \\
1.125 - @{attribute_def elim} & : & @{text attribute} \\
1.126 - @{attribute_def dest} & : & @{text attribute} \\
1.127 - @{attribute_def rule} & : & @{text attribute} \\
1.128 - @{attribute_def iff} & : & @{text attribute} \\
1.129 - \end{matharray}
1.130 -
1.131 - @{rail "
1.132 - (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
1.133 - ;
1.134 - @@{attribute rule} 'del'
1.135 - ;
1.136 - @@{attribute iff} (((() | 'add') '?'?) | 'del')
1.137 - "}
1.138 -
1.139 - \begin{description}
1.140 -
1.141 - \item @{command "print_claset"} prints the collection of rules
1.142 - declared to the Classical Reasoner, which is also known as
1.143 - ``claset'' internally \cite{isabelle-ref}.
1.144 -
1.145 - \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
1.146 - declare introduction, elimination, and destruction rules,
1.147 - respectively. By default, rules are considered as \emph{unsafe}
1.148 - (i.e.\ not applied blindly without backtracking), while ``@{text
1.149 - "!"}'' classifies as \emph{safe}. Rule declarations marked by
1.150 - ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
1.151 - \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
1.152 - of the @{method rule} method). The optional natural number
1.153 - specifies an explicit weight argument, which is ignored by automated
1.154 - tools, but determines the search order of single rule steps.
1.155 -
1.156 - \item @{attribute rule}~@{text del} deletes introduction,
1.157 - elimination, or destruction rules from the context.
1.158 -
1.159 - \item @{attribute iff} declares logical equivalences to the
1.160 - Simplifier and the Classical reasoner at the same time.
1.161 - Non-conditional rules result in a ``safe'' introduction and
1.162 - elimination pair; conditional ones are considered ``unsafe''. Rules
1.163 - with negative conclusion are automatically inverted (using @{text
1.164 - "\<not>"}-elimination internally).
1.165 -
1.166 - The ``@{text "?"}'' version of @{attribute iff} declares rules to
1.167 - the Isabelle/Pure context only, and omits the Simplifier
1.168 - declaration.
1.169 -
1.170 - \end{description}
1.171 -*}
1.172 -
1.173 -
1.174 -subsection {* Classical operations *}
1.175 -
1.176 -text {*
1.177 - \begin{matharray}{rcl}
1.178 - @{attribute_def swapped} & : & @{text attribute} \\
1.179 - \end{matharray}
1.180 -
1.181 - \begin{description}
1.182 -
1.183 - \item @{attribute swapped} turns an introduction rule into an
1.184 - elimination, by resolving with the classical swap principle @{text
1.185 - "(\<not> B \<Longrightarrow> A) \<Longrightarrow> (\<not> A \<Longrightarrow> B)"}.
1.186 -
1.187 - \end{description}
1.188 -*}
1.189 -
1.190 -
1.191 section {* Object-logic setup \label{sec:object-logic} *}
1.192
1.193 text {*