src/Doc/IsarRef/Generic.thy
author wenzelm
Fri May 17 20:53:28 2013 +0200 (2013-05-17)
changeset 52060 179236c82c2a
parent 52037 837211662fb8
child 55029 61a6bf7d4b02
permissions -rw-r--r--
renamed 'print_configs' to 'print_options';
     1 theory Generic
     2 imports Base Main
     3 begin
     4 
     5 chapter {* Generic tools and packages \label{ch:gen-tools} *}
     6 
     7 section {* Configuration options \label{sec:config} *}
     8 
     9 text {* Isabelle/Pure maintains a record of named configuration
    10   options within the theory or proof context, with values of type
    11   @{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type
    12   string}.  Tools may declare options in ML, and then refer to these
    13   values (relative to the context).  Thus global reference variables
    14   are easily avoided.  The user may change the value of a
    15   configuration option by means of an associated attribute of the same
    16   name.  This form of context declaration works particularly well with
    17   commands such as @{command "declare"} or @{command "using"} like
    18   this:
    19 *}
    20 
    21 declare [[show_main_goal = false]]
    22 
    23 notepad
    24 begin
    25   note [[show_main_goal = true]]
    26 end
    27 
    28 text {* For historical reasons, some tools cannot take the full proof
    29   context into account and merely refer to the background theory.
    30   This is accommodated by configuration options being declared as
    31   ``global'', which may not be changed within a local context.
    32 
    33   \begin{matharray}{rcll}
    34     @{command_def "print_options"} & : & @{text "context \<rightarrow>"} \\
    35   \end{matharray}
    36 
    37   @{rail "
    38     @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?
    39   "}
    40 
    41   \begin{description}
    42   
    43   \item @{command "print_options"} prints the available configuration
    44   options, with names, types, and current values.
    45   
    46   \item @{text "name = value"} as an attribute expression modifies the
    47   named option, with the syntax of the value depending on the option's
    48   type.  For @{ML_type bool} the default value is @{text true}.  Any
    49   attempt to change a global option in a local context is ignored.
    50 
    51   \end{description}
    52 *}
    53 
    54 
    55 section {* Basic proof tools *}
    56 
    57 subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *}
    58 
    59 text {*
    60   \begin{matharray}{rcl}
    61     @{method_def unfold} & : & @{text method} \\
    62     @{method_def fold} & : & @{text method} \\
    63     @{method_def insert} & : & @{text method} \\[0.5ex]
    64     @{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\
    65     @{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\
    66     @{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
    67     @{method_def intro} & : & @{text method} \\
    68     @{method_def elim} & : & @{text method} \\
    69     @{method_def succeed} & : & @{text method} \\
    70     @{method_def fail} & : & @{text method} \\
    71   \end{matharray}
    72 
    73   @{rail "
    74     (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
    75     ;
    76     (@@{method erule} | @@{method drule} | @@{method frule})
    77       ('(' @{syntax nat} ')')? @{syntax thmrefs}
    78     ;
    79     (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
    80   "}
    81 
    82   \begin{description}
    83   
    84   \item @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text
    85   "a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout
    86   all goals; any chained facts provided are inserted into the goal and
    87   subject to rewriting as well.
    88 
    89   \item @{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} inserts theorems as facts
    90   into all goals of the proof state.  Note that current facts
    91   indicated for forward chaining are ignored.
    92 
    93   \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method
    94   drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text
    95   "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule}
    96   method (see \secref{sec:pure-meth-att}), but apply rules by
    97   elim-resolution, destruct-resolution, and forward-resolution,
    98   respectively \cite{isabelle-implementation}.  The optional natural
    99   number argument (default 0) specifies additional assumption steps to
   100   be performed here.
   101 
   102   Note that these methods are improper ones, mainly serving for
   103   experimentation and tactic script emulation.  Different modes of
   104   basic rule application are usually expressed in Isar at the proof
   105   language level, rather than via implicit proof state manipulations.
   106   For example, a proper single-step elimination would be done using
   107   the plain @{method rule} method, with forward chaining of current
   108   facts.
   109 
   110   \item @{method intro} and @{method elim} repeatedly refine some goal
   111   by intro- or elim-resolution, after having inserted any chained
   112   facts.  Exactly the rules given as arguments are taken into account;
   113   this allows fine-tuned decomposition of a proof problem, in contrast
   114   to common automated tools.
   115 
   116   \item @{method succeed} yields a single (unchanged) result; it is
   117   the identity of the ``@{text ","}'' method combinator (cf.\
   118   \secref{sec:proof-meth}).
   119 
   120   \item @{method fail} yields an empty result sequence; it is the
   121   identity of the ``@{text "|"}'' method combinator (cf.\
   122   \secref{sec:proof-meth}).
   123 
   124   \end{description}
   125 
   126   \begin{matharray}{rcl}
   127     @{attribute_def tagged} & : & @{text attribute} \\
   128     @{attribute_def untagged} & : & @{text attribute} \\[0.5ex]
   129     @{attribute_def THEN} & : & @{text attribute} \\
   130     @{attribute_def unfolded} & : & @{text attribute} \\
   131     @{attribute_def folded} & : & @{text attribute} \\
   132     @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]
   133     @{attribute_def rotated} & : & @{text attribute} \\
   134     @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
   135     @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
   136     @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
   137   \end{matharray}
   138 
   139   @{rail "
   140     @@{attribute tagged} @{syntax name} @{syntax name}
   141     ;
   142     @@{attribute untagged} @{syntax name}
   143     ;
   144     @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref}
   145     ;
   146     (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
   147     ;
   148     @@{attribute rotated} @{syntax int}?
   149   "}
   150 
   151   \begin{description}
   152 
   153   \item @{attribute tagged}~@{text "name value"} and @{attribute
   154   untagged}~@{text name} add and remove \emph{tags} of some theorem.
   155   Tags may be any list of string pairs that serve as formal comment.
   156   The first string is considered the tag name, the second its value.
   157   Note that @{attribute untagged} removes any tags of the same name.
   158 
   159   \item @{attribute THEN}~@{text a} composes rules by resolution; it
   160   resolves with the first premise of @{text a} (an alternative
   161   position may be also specified).  See also @{ML_op "RS"} in
   162   \cite{isabelle-implementation}.
   163   
   164   \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
   165   folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
   166   definitions throughout a rule.
   167 
   168   \item @{attribute abs_def} turns an equation of the form @{prop "f x
   169   y \<equiv> t"} into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method
   170   simp} or @{method unfold} steps always expand it.  This also works
   171   for object-logic equality.
   172 
   173   \item @{attribute rotated}~@{text n} rotate the premises of a
   174   theorem by @{text n} (default 1).
   175 
   176   \item @{attribute (Pure) elim_format} turns a destruction rule into
   177   elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
   178   (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
   179   
   180   Note that the Classical Reasoner (\secref{sec:classical}) provides
   181   its own version of this operation.
   182 
   183   \item @{attribute standard} puts a theorem into the standard form of
   184   object-rules at the outermost theory level.  Note that this
   185   operation violates the local proof context (including active
   186   locales).
   187 
   188   \item @{attribute no_vars} replaces schematic variables by free
   189   ones; this is mainly for tuning output of pretty printed theorems.
   190 
   191   \end{description}
   192 *}
   193 
   194 
   195 subsection {* Low-level equational reasoning *}
   196 
   197 text {*
   198   \begin{matharray}{rcl}
   199     @{method_def subst} & : & @{text method} \\
   200     @{method_def hypsubst} & : & @{text method} \\
   201     @{method_def split} & : & @{text method} \\
   202   \end{matharray}
   203 
   204   @{rail "
   205     @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
   206     ;
   207     @@{method split} @{syntax thmrefs}
   208   "}
   209 
   210   These methods provide low-level facilities for equational reasoning
   211   that are intended for specialized applications only.  Normally,
   212   single step calculations would be performed in a structured text
   213   (see also \secref{sec:calculation}), while the Simplifier methods
   214   provide the canonical way for automated normalization (see
   215   \secref{sec:simplifier}).
   216 
   217   \begin{description}
   218 
   219   \item @{method subst}~@{text eq} performs a single substitution step
   220   using rule @{text eq}, which may be either a meta or object
   221   equality.
   222 
   223   \item @{method subst}~@{text "(asm) eq"} substitutes in an
   224   assumption.
   225 
   226   \item @{method subst}~@{text "(i \<dots> j) eq"} performs several
   227   substitutions in the conclusion. The numbers @{text i} to @{text j}
   228   indicate the positions to substitute at.  Positions are ordered from
   229   the top of the term tree moving down from left to right. For
   230   example, in @{text "(a + b) + (c + d)"} there are three positions
   231   where commutativity of @{text "+"} is applicable: 1 refers to @{text
   232   "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}.
   233 
   234   If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
   235   (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
   236   assume all substitutions are performed simultaneously.  Otherwise
   237   the behaviour of @{text subst} is not specified.
   238 
   239   \item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the
   240   substitutions in the assumptions. The positions refer to the
   241   assumptions in order from left to right.  For example, given in a
   242   goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of
   243   commutativity of @{text "+"} is the subterm @{text "a + b"} and
   244   position 2 is the subterm @{text "c + d"}.
   245 
   246   \item @{method hypsubst} performs substitution using some
   247   assumption; this only works for equations of the form @{text "x =
   248   t"} where @{text x} is a free or bound variable.
   249 
   250   \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
   251   splitting using the given rules.  Splitting is performed in the
   252   conclusion or some assumption of the subgoal, depending of the
   253   structure of the rule.
   254   
   255   Note that the @{method simp} method already involves repeated
   256   application of split rules as declared in the current context, using
   257   @{attribute split}, for example.
   258 
   259   \end{description}
   260 *}
   261 
   262 
   263 subsection {* Further tactic emulations \label{sec:tactics} *}
   264 
   265 text {*
   266   The following improper proof methods emulate traditional tactics.
   267   These admit direct access to the goal state, which is normally
   268   considered harmful!  In particular, this may involve both numbered
   269   goal addressing (default 1), and dynamic instantiation within the
   270   scope of some subgoal.
   271 
   272   \begin{warn}
   273     Dynamic instantiations refer to universally quantified parameters
   274     of a subgoal (the dynamic context) rather than fixed variables and
   275     term abbreviations of a (static) Isar context.
   276   \end{warn}
   277 
   278   Tactic emulation methods, unlike their ML counterparts, admit
   279   simultaneous instantiation from both dynamic and static contexts.
   280   If names occur in both contexts goal parameters hide locally fixed
   281   variables.  Likewise, schematic variables refer to term
   282   abbreviations, if present in the static context.  Otherwise the
   283   schematic variable is interpreted as a schematic variable and left
   284   to be solved by unification with certain parts of the subgoal.
   285 
   286   Note that the tactic emulation proof methods in Isabelle/Isar are
   287   consistently named @{text foo_tac}.  Note also that variable names
   288   occurring on left hand sides of instantiations must be preceded by a
   289   question mark if they coincide with a keyword or contain dots.  This
   290   is consistent with the attribute @{attribute "where"} (see
   291   \secref{sec:pure-meth-att}).
   292 
   293   \begin{matharray}{rcl}
   294     @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   295     @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   296     @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   297     @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   298     @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
   299     @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
   300     @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
   301     @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
   302     @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
   303     @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
   304     @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
   305   \end{matharray}
   306 
   307   @{rail "
   308     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
   309       @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \\
   310     ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
   311     ;
   312     @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
   313     ;
   314     @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
   315     ;
   316     @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
   317     ;
   318     (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
   319     ;
   320 
   321     dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
   322   "}
   323 
   324 \begin{description}
   325 
   326   \item @{method rule_tac} etc. do resolution of rules with explicit
   327   instantiation.  This works the same way as the ML tactics @{ML
   328   res_inst_tac} etc. (see \cite{isabelle-implementation})
   329 
   330   Multiple rules may be only given if there is no instantiation; then
   331   @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
   332   \cite{isabelle-implementation}).
   333 
   334   \item @{method cut_tac} inserts facts into the proof state as
   335   assumption of a subgoal; instantiations may be given as well.  Note
   336   that the scope of schematic variables is spread over the main goal
   337   statement and rule premises are turned into new subgoals.  This is
   338   in contrast to the regular method @{method insert} which inserts
   339   closed rule statements.
   340 
   341   \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
   342   from a subgoal.  Note that @{text \<phi>} may contain schematic
   343   variables, to abbreviate the intended proposition; the first
   344   matching subgoal premise will be deleted.  Removing useless premises
   345   from a subgoal increases its readability and can make search tactics
   346   run faster.
   347 
   348   \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
   349   @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
   350   as new subgoals (in the original context).
   351 
   352   \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
   353   goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
   354   \emph{suffix} of variables.
   355 
   356   \item @{method rotate_tac}~@{text n} rotates the premises of a
   357   subgoal by @{text n} positions: from right to left if @{text n} is
   358   positive, and from left to right if @{text n} is negative; the
   359   default value is 1.
   360 
   361   \item @{method tactic}~@{text "text"} produces a proof method from
   362   any ML text of type @{ML_type tactic}.  Apart from the usual ML
   363   environment and the current proof context, the ML code may refer to
   364   the locally bound values @{ML_text facts}, which indicates any
   365   current facts used for forward-chaining.
   366 
   367   \item @{method raw_tactic} is similar to @{method tactic}, but
   368   presents the goal state in its raw internal form, where simultaneous
   369   subgoals appear as conjunction of the logical framework instead of
   370   the usual split into several subgoals.  While feature this is useful
   371   for debugging of complex method definitions, it should not never
   372   appear in production theories.
   373 
   374   \end{description}
   375 *}
   376 
   377 
   378 section {* The Simplifier \label{sec:simplifier} *}
   379 
   380 text {* The Simplifier performs conditional and unconditional
   381   rewriting and uses contextual information: rule declarations in the
   382   background theory or local proof context are taken into account, as
   383   well as chained facts and subgoal premises (``local assumptions'').
   384   There are several general hooks that allow to modify the
   385   simplification strategy, or incorporate other proof tools that solve
   386   sub-problems, produce rewrite rules on demand etc.
   387 
   388   The rewriting strategy is always strictly bottom up, except for
   389   congruence rules, which are applied while descending into a term.
   390   Conditions in conditional rewrite rules are solved recursively
   391   before the rewrite rule is applied.
   392 
   393   The default Simplifier setup of major object logics (HOL, HOLCF,
   394   FOL, ZF) makes the Simplifier ready for immediate use, without
   395   engaging into the internal structures.  Thus it serves as
   396   general-purpose proof tool with the main focus on equational
   397   reasoning, and a bit more than that.
   398 *}
   399 
   400 
   401 subsection {* Simplification methods \label{sec:simp-meth} *}
   402 
   403 text {*
   404   \begin{matharray}{rcl}
   405     @{method_def simp} & : & @{text method} \\
   406     @{method_def simp_all} & : & @{text method} \\
   407   \end{matharray}
   408 
   409   @{rail "
   410     (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
   411     ;
   412 
   413     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
   414     ;
   415     @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |
   416       'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
   417   "}
   418 
   419   \begin{description}
   420 
   421   \item @{method simp} invokes the Simplifier on the first subgoal,
   422   after inserting chained facts as additional goal premises; further
   423   rule declarations may be included via @{text "(simp add: facts)"}.
   424   The proof method fails if the subgoal remains unchanged after
   425   simplification.
   426 
   427   Note that the original goal premises and chained facts are subject
   428   to simplification themselves, while declarations via @{text
   429   "add"}/@{text "del"} merely follow the policies of the object-logic
   430   to extract rewrite rules from theorems, without further
   431   simplification.  This may lead to slightly different behavior in
   432   either case, which might be required precisely like that in some
   433   boundary situations to perform the intended simplification step!
   434 
   435   \medskip The @{text only} modifier first removes all other rewrite
   436   rules, looper tactics (including split rules), congruence rules, and
   437   then behaves like @{text add}.  Implicit solvers remain, which means
   438   that trivial rules like reflexivity or introduction of @{text
   439   "True"} are available to solve the simplified subgoals, but also
   440   non-trivial tools like linear arithmetic in HOL.  The latter may
   441   lead to some surprise of the meaning of ``only'' in Isabelle/HOL
   442   compared to English!
   443 
   444   \medskip The @{text split} modifiers add or delete rules for the
   445   Splitter (see also \secref{sec:simp-strategies} on the looper).
   446   This works only if the Simplifier method has been properly setup to
   447   include the Splitter (all major object logics such HOL, HOLCF, FOL,
   448   ZF do this already).
   449 
   450   There is also a separate @{method_ref split} method available for
   451   single-step case splitting.  The effect of repeatedly applying
   452   @{text "(split thms)"} can be imitated by ``@{text "(simp only:
   453   split: thms)"}''.
   454 
   455   \medskip The @{text cong} modifiers add or delete Simplifier
   456   congruence rules (see also \secref{sec:simp-rules}); the default is
   457   to add.
   458 
   459   \item @{method simp_all} is similar to @{method simp}, but acts on
   460   all goals, working backwards from the last to the first one as usual
   461   in Isabelle.\footnote{The order is irrelevant for goals without
   462   schematic variables, so simplification might actually be performed
   463   in parallel here.}
   464 
   465   Chained facts are inserted into all subgoals, before the
   466   simplification process starts.  Further rule declarations are the
   467   same as for @{method simp}.
   468 
   469   The proof method fails if all subgoals remain unchanged after
   470   simplification.
   471 
   472   \end{description}
   473 
   474   By default the Simplifier methods above take local assumptions fully
   475   into account, using equational assumptions in the subsequent
   476   normalization process, or simplifying assumptions themselves.
   477   Further options allow to fine-tune the behavior of the Simplifier
   478   in this respect, corresponding to a variety of ML tactics as
   479   follows.\footnote{Unlike the corresponding Isar proof methods, the
   480   ML tactics do not insist in changing the goal state.}
   481 
   482   \begin{center}
   483   \small
   484   \begin{supertabular}{|l|l|p{0.3\textwidth}|}
   485   \hline
   486   Isar method & ML tactic & behavior \\\hline
   487 
   488   @{text "(simp (no_asm))"} & @{ML simp_tac} & assumptions are ignored
   489   completely \\\hline
   490 
   491   @{text "(simp (no_asm_simp))"} & @{ML asm_simp_tac} & assumptions
   492   are used in the simplification of the conclusion but are not
   493   themselves simplified \\\hline
   494 
   495   @{text "(simp (no_asm_use))"} & @{ML full_simp_tac} & assumptions
   496   are simplified but are not used in the simplification of each other
   497   or the conclusion \\\hline
   498 
   499   @{text "(simp)"} & @{ML asm_full_simp_tac} & assumptions are used in
   500   the simplification of the conclusion and to simplify other
   501   assumptions \\\hline
   502 
   503   @{text "(simp (asm_lr))"} & @{ML asm_lr_simp_tac} & compatibility
   504   mode: an assumption is only used for simplifying assumptions which
   505   are to the right of it \\\hline
   506 
   507   \end{supertabular}
   508   \end{center}
   509 *}
   510 
   511 
   512 subsubsection {* Examples *}
   513 
   514 text {* We consider basic algebraic simplifications in Isabelle/HOL.
   515   The rather trivial goal @{prop "0 + (x + 0) = x + 0 + 0"} looks like
   516   a good candidate to be solved by a single call of @{method simp}:
   517 *}
   518 
   519 lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops
   520 
   521 text {* The above attempt \emph{fails}, because @{term "0"} and @{term
   522   "op +"} in the HOL library are declared as generic type class
   523   operations, without stating any algebraic laws yet.  More specific
   524   types are required to get access to certain standard simplifications
   525   of the theory context, e.g.\ like this: *}
   526 
   527 lemma fixes x :: nat shows "0 + (x + 0) = x + 0 + 0" by simp
   528 lemma fixes x :: int shows "0 + (x + 0) = x + 0 + 0" by simp
   529 lemma fixes x :: "'a :: monoid_add" shows "0 + (x + 0) = x + 0 + 0" by simp
   530 
   531 text {*
   532   \medskip In many cases, assumptions of a subgoal are also needed in
   533   the simplification process.  For example:
   534 *}
   535 
   536 lemma fixes x :: nat shows "x = 0 \<Longrightarrow> x + x = 0" by simp
   537 lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" apply simp oops
   538 lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" using assms by simp
   539 
   540 text {* As seen above, local assumptions that shall contribute to
   541   simplification need to be part of the subgoal already, or indicated
   542   explicitly for use by the subsequent method invocation.  Both too
   543   little or too much information can make simplification fail, for
   544   different reasons.
   545 
   546   In the next example the malicious assumption @{prop "\<And>x::nat. f x =
   547   g (f (g x))"} does not contribute to solve the problem, but makes
   548   the default @{method simp} method loop: the rewrite rule @{text "f
   549   ?x \<equiv> g (f (g ?x))"} extracted from the assumption does not
   550   terminate.  The Simplifier notices certain simple forms of
   551   nontermination, but not this one.  The problem can be solved
   552   nonetheless, by ignoring assumptions via special options as
   553   explained before:
   554 *}
   555 
   556 lemma "(\<And>x::nat. f x = g (f (g x))) \<Longrightarrow> f 0 = f 0 + 0"
   557   by (simp (no_asm))
   558 
   559 text {* The latter form is typical for long unstructured proof
   560   scripts, where the control over the goal content is limited.  In
   561   structured proofs it is usually better to avoid pushing too many
   562   facts into the goal state in the first place.  Assumptions in the
   563   Isar proof context do not intrude the reasoning if not used
   564   explicitly.  This is illustrated for a toplevel statement and a
   565   local proof body as follows:
   566 *}
   567 
   568 lemma
   569   assumes "\<And>x::nat. f x = g (f (g x))"
   570   shows "f 0 = f 0 + 0" by simp
   571 
   572 notepad
   573 begin
   574   assume "\<And>x::nat. f x = g (f (g x))"
   575   have "f 0 = f 0 + 0" by simp
   576 end
   577 
   578 text {* \medskip Because assumptions may simplify each other, there
   579   can be very subtle cases of nontermination. For example, the regular
   580   @{method simp} method applied to @{prop "P (f x) \<Longrightarrow> y = x \<Longrightarrow> f x = f y
   581   \<Longrightarrow> Q"} gives rise to the infinite reduction sequence
   582   \[
   583   @{text "P (f x)"} \stackrel{@{text "f x \<equiv> f y"}}{\longmapsto}
   584   @{text "P (f y)"} \stackrel{@{text "y \<equiv> x"}}{\longmapsto}
   585   @{text "P (f x)"} \stackrel{@{text "f x \<equiv> f y"}}{\longmapsto} \cdots
   586   \]
   587   whereas applying the same to @{prop "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow>
   588   Q"} terminates (without solving the goal):
   589 *}
   590 
   591 lemma "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> Q"
   592   apply simp
   593   oops
   594 
   595 text {* See also \secref{sec:simp-config} for options to enable
   596   Simplifier trace mode, which often helps to diagnose problems with
   597   rewrite systems.
   598 *}
   599 
   600 
   601 subsection {* Declaring rules \label{sec:simp-rules} *}
   602 
   603 text {*
   604   \begin{matharray}{rcl}
   605     @{attribute_def simp} & : & @{text attribute} \\
   606     @{attribute_def split} & : & @{text attribute} \\
   607     @{attribute_def cong} & : & @{text attribute} \\
   608     @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   609   \end{matharray}
   610 
   611   @{rail "
   612     (@@{attribute simp} | @@{attribute split} | @@{attribute cong})
   613       (() | 'add' | 'del')
   614   "}
   615 
   616   \begin{description}
   617 
   618   \item @{attribute simp} declares rewrite rules, by adding or
   619   deleting them from the simpset within the theory or proof context.
   620   Rewrite rules are theorems expressing some form of equality, for
   621   example:
   622 
   623   @{text "Suc ?m + ?n = ?m + Suc ?n"} \\
   624   @{text "?P \<and> ?P \<longleftrightarrow> ?P"} \\
   625   @{text "?A \<union> ?B \<equiv> {x. x \<in> ?A \<or> x \<in> ?B}"}
   626 
   627   \smallskip
   628   Conditional rewrites such as @{text "?m < ?n \<Longrightarrow> ?m div ?n = 0"} are
   629   also permitted; the conditions can be arbitrary formulas.
   630 
   631   \medskip Internally, all rewrite rules are translated into Pure
   632   equalities, theorems with conclusion @{text "lhs \<equiv> rhs"}. The
   633   simpset contains a function for extracting equalities from arbitrary
   634   theorems, which is usually installed when the object-logic is
   635   configured initially. For example, @{text "\<not> ?x \<in> {}"} could be
   636   turned into @{text "?x \<in> {} \<equiv> False"}. Theorems that are declared as
   637   @{attribute simp} and local assumptions within a goal are treated
   638   uniformly in this respect.
   639 
   640   The Simplifier accepts the following formats for the @{text "lhs"}
   641   term:
   642 
   643   \begin{enumerate}
   644 
   645   \item First-order patterns, considering the sublanguage of
   646   application of constant operators to variable operands, without
   647   @{text "\<lambda>"}-abstractions or functional variables.
   648   For example:
   649 
   650   @{text "(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)"} \\
   651   @{text "f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)"}
   652 
   653   \item Higher-order patterns in the sense of \cite{nipkow-patterns}.
   654   These are terms in @{text "\<beta>"}-normal form (this will always be the
   655   case unless you have done something strange) where each occurrence
   656   of an unknown is of the form @{text "?F x\<^sub>1 \<dots> x\<^sub>n"}, where the
   657   @{text "x\<^sub>i"} are distinct bound variables.
   658 
   659   For example, @{text "(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>x. ?Q x)"}
   660   or its symmetric form, since the @{text "rhs"} is also a
   661   higher-order pattern.
   662 
   663   \item Physical first-order patterns over raw @{text "\<lambda>"}-term
   664   structure without @{text "\<alpha>\<beta>\<eta>"}-equality; abstractions and bound
   665   variables are treated like quasi-constant term material.
   666 
   667   For example, the rule @{text "?f ?x \<in> range ?f = True"} rewrites the
   668   term @{text "g a \<in> range g"} to @{text "True"}, but will fail to
   669   match @{text "g (h b) \<in> range (\<lambda>x. g (h x))"}. However, offending
   670   subterms (in our case @{text "?f ?x"}, which is not a pattern) can
   671   be replaced by adding new variables and conditions like this: @{text
   672   "?y = ?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is acceptable as a conditional
   673   rewrite rule of the second category since conditions can be
   674   arbitrary terms.
   675 
   676   \end{enumerate}
   677 
   678   \item @{attribute split} declares case split rules.
   679 
   680   \item @{attribute cong} declares congruence rules to the Simplifier
   681   context.
   682 
   683   Congruence rules are equalities of the form @{text [display]
   684   "\<dots> \<Longrightarrow> f ?x\<^sub>1 \<dots> ?x\<^sub>n = f ?y\<^sub>1 \<dots> ?y\<^sub>n"}
   685 
   686   This controls the simplification of the arguments of @{text f}.  For
   687   example, some arguments can be simplified under additional
   688   assumptions: @{text [display] "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow> (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow>
   689   (?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"}
   690 
   691   Given this rule, the simplifier assumes @{text "?Q\<^sub>1"} and extracts
   692   rewrite rules from it when simplifying @{text "?P\<^sub>2"}.  Such local
   693   assumptions are effective for rewriting formulae such as @{text "x =
   694   0 \<longrightarrow> y + x = y"}.
   695 
   696   %FIXME
   697   %The local assumptions are also provided as theorems to the solver;
   698   %see \secref{sec:simp-solver} below.
   699 
   700   \medskip The following congruence rule for bounded quantifiers also
   701   supplies contextual information --- about the bound variable:
   702   @{text [display] "(?A = ?B) \<Longrightarrow> (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow>
   703     (\<forall>x \<in> ?A. ?P x) \<longleftrightarrow> (\<forall>x \<in> ?B. ?Q x)"}
   704 
   705   \medskip This congruence rule for conditional expressions can
   706   supply contextual information for simplifying the arms:
   707   @{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow>
   708     (if ?p then ?a else ?b) = (if ?q then ?c else ?d)"}
   709 
   710   A congruence rule can also \emph{prevent} simplification of some
   711   arguments.  Here is an alternative congruence rule for conditional
   712   expressions that conforms to non-strict functional evaluation:
   713   @{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"}
   714 
   715   Only the first argument is simplified; the others remain unchanged.
   716   This can make simplification much faster, but may require an extra
   717   case split over the condition @{text "?q"} to prove the goal.
   718 
   719   \item @{command "print_simpset"} prints the collection of rules
   720   declared to the Simplifier, which is also known as ``simpset''
   721   internally.
   722 
   723   For historical reasons, simpsets may occur independently from the
   724   current context, but are conceptually dependent on it.  When the
   725   Simplifier is invoked via one of its main entry points in the Isar
   726   source language (as proof method \secref{sec:simp-meth} or rule
   727   attribute \secref{sec:simp-meth}), its simpset is derived from the
   728   current proof context, and carries a back-reference to that for
   729   other tools that might get invoked internally (e.g.\ simplification
   730   procedures \secref{sec:simproc}).  A mismatch of the context of the
   731   simpset and the context of the problem being simplified may lead to
   732   unexpected results.
   733 
   734   \end{description}
   735 
   736   The implicit simpset of the theory context is propagated
   737   monotonically through the theory hierarchy: forming a new theory,
   738   the union of the simpsets of its imports are taken as starting
   739   point.  Also note that definitional packages like @{command
   740   "datatype"}, @{command "primrec"}, @{command "fun"} routinely
   741   declare Simplifier rules to the target context, while plain
   742   @{command "definition"} is an exception in \emph{not} declaring
   743   anything.
   744 
   745   \medskip It is up the user to manipulate the current simpset further
   746   by explicitly adding or deleting theorems as simplification rules,
   747   or installing other tools via simplification procedures
   748   (\secref{sec:simproc}).  Good simpsets are hard to design.  Rules
   749   that obviously simplify, like @{text "?n + 0 \<equiv> ?n"} are good
   750   candidates for the implicit simpset, unless a special
   751   non-normalizing behavior of certain operations is intended.  More
   752   specific rules (such as distributive laws, which duplicate subterms)
   753   should be added only for specific proof steps.  Conversely,
   754   sometimes a rule needs to be deleted just for some part of a proof.
   755   The need of frequent additions or deletions may indicate a poorly
   756   designed simpset.
   757 
   758   \begin{warn}
   759   The union of simpsets from theory imports (as described above) is
   760   not always a good starting point for the new theory.  If some
   761   ancestors have deleted simplification rules because they are no
   762   longer wanted, while others have left those rules in, then the union
   763   will contain the unwanted rules, and thus have to be deleted again
   764   in the theory body.
   765   \end{warn}
   766 *}
   767 
   768 
   769 subsection {* Ordered rewriting with permutative rules *}
   770 
   771 text {* A rewrite rule is \emph{permutative} if the left-hand side and
   772   right-hand side are the equal up to renaming of variables.  The most
   773   common permutative rule is commutativity: @{text "?x + ?y = ?y +
   774   ?x"}.  Other examples include @{text "(?x - ?y) - ?z = (?x - ?z) -
   775   ?y"} in arithmetic and @{text "insert ?x (insert ?y ?A) = insert ?y
   776   (insert ?x ?A)"} for sets.  Such rules are common enough to merit
   777   special attention.
   778 
   779   Because ordinary rewriting loops given such rules, the Simplifier
   780   employs a special strategy, called \emph{ordered rewriting}.
   781   Permutative rules are detected and only applied if the rewriting
   782   step decreases the redex wrt.\ a given term ordering.  For example,
   783   commutativity rewrites @{text "b + a"} to @{text "a + b"}, but then
   784   stops, because the redex cannot be decreased further in the sense of
   785   the term ordering.
   786 
   787   The default is lexicographic ordering of term structure, but this
   788   could be also changed locally for special applications via
   789   @{index_ML Simplifier.set_termless} in Isabelle/ML.
   790 
   791   \medskip Permutative rewrite rules are declared to the Simplifier
   792   just like other rewrite rules.  Their special status is recognized
   793   automatically, and their application is guarded by the term ordering
   794   accordingly. *}
   795 
   796 
   797 subsubsection {* Rewriting with AC operators *}
   798 
   799 text {* Ordered rewriting is particularly effective in the case of
   800   associative-commutative operators.  (Associativity by itself is not
   801   permutative.)  When dealing with an AC-operator @{text "f"}, keep
   802   the following points in mind:
   803 
   804   \begin{itemize}
   805 
   806   \item The associative law must always be oriented from left to
   807   right, namely @{text "f (f x y) z = f x (f y z)"}.  The opposite
   808   orientation, if used with commutativity, leads to looping in
   809   conjunction with the standard term order.
   810 
   811   \item To complete your set of rewrite rules, you must add not just
   812   associativity (A) and commutativity (C) but also a derived rule
   813   \emph{left-commutativity} (LC): @{text "f x (f y z) = f y (f x z)"}.
   814 
   815   \end{itemize}
   816 
   817   Ordered rewriting with the combination of A, C, and LC sorts a term
   818   lexicographically --- the rewriting engine imitates bubble-sort.
   819 *}
   820 
   821 locale AC_example =
   822   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infix "\<bullet>" 60)
   823   assumes assoc: "(x \<bullet> y) \<bullet> z = x \<bullet> (y \<bullet> z)"
   824   assumes commute: "x \<bullet> y = y \<bullet> x"
   825 begin
   826 
   827 lemma left_commute: "x \<bullet> (y \<bullet> z) = y \<bullet> (x \<bullet> z)"
   828 proof -
   829   have "(x \<bullet> y) \<bullet> z = (y \<bullet> x) \<bullet> z" by (simp only: commute)
   830   then show ?thesis by (simp only: assoc)
   831 qed
   832 
   833 lemmas AC_rules = assoc commute left_commute
   834 
   835 text {* Thus the Simplifier is able to establish equalities with
   836   arbitrary permutations of subterms, by normalizing to a common
   837   standard form.  For example: *}
   838 
   839 lemma "(b \<bullet> c) \<bullet> a = xxx"
   840   apply (simp only: AC_rules)
   841   txt {* @{subgoals} *}
   842   oops
   843 
   844 lemma "(b \<bullet> c) \<bullet> a = a \<bullet> (b \<bullet> c)" by (simp only: AC_rules)
   845 lemma "(b \<bullet> c) \<bullet> a = c \<bullet> (b \<bullet> a)" by (simp only: AC_rules)
   846 lemma "(b \<bullet> c) \<bullet> a = (c \<bullet> b) \<bullet> a" by (simp only: AC_rules)
   847 
   848 end
   849 
   850 text {* Martin and Nipkow \cite{martin-nipkow} discuss the theory and
   851   give many examples; other algebraic structures are amenable to
   852   ordered rewriting, such as boolean rings.  The Boyer-Moore theorem
   853   prover \cite{bm88book} also employs ordered rewriting.
   854 *}
   855 
   856 
   857 subsubsection {* Re-orienting equalities *}
   858 
   859 text {* Another application of ordered rewriting uses the derived rule
   860   @{thm [source] eq_commute}: @{thm [source = false] eq_commute} to
   861   reverse equations.
   862 
   863   This is occasionally useful to re-orient local assumptions according
   864   to the term ordering, when other built-in mechanisms of
   865   reorientation and mutual simplification fail to apply.  *}
   866 
   867 
   868 subsection {* Configuration options \label{sec:simp-config} *}
   869 
   870 text {*
   871   \begin{tabular}{rcll}
   872     @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\
   873     @{attribute_def simp_trace} & : & @{text attribute} & default @{text false} \\
   874     @{attribute_def simp_trace_depth_limit} & : & @{text attribute} & default @{text 1} \\
   875     @{attribute_def simp_debug} & : & @{text attribute} & default @{text false} \\
   876   \end{tabular}
   877   \medskip
   878 
   879   These configurations options control further aspects of the Simplifier.
   880   See also \secref{sec:config}.
   881 
   882   \begin{description}
   883 
   884   \item @{attribute simp_depth_limit} limits the number of recursive
   885   invocations of the Simplifier during conditional rewriting.
   886 
   887   \item @{attribute simp_trace} makes the Simplifier output internal
   888   operations.  This includes rewrite steps, but also bookkeeping like
   889   modifications of the simpset.
   890 
   891   \item @{attribute simp_trace_depth_limit} limits the effect of
   892   @{attribute simp_trace} to the given depth of recursive Simplifier
   893   invocations (when solving conditions of rewrite rules).
   894 
   895   \item @{attribute simp_debug} makes the Simplifier output some extra
   896   information about internal operations.  This includes any attempted
   897   invocation of simplification procedures.
   898 
   899   \end{description}
   900 *}
   901 
   902 
   903 subsection {* Simplification procedures \label{sec:simproc} *}
   904 
   905 text {* Simplification procedures are ML functions that produce proven
   906   rewrite rules on demand.  They are associated with higher-order
   907   patterns that approximate the left-hand sides of equations.  The
   908   Simplifier first matches the current redex against one of the LHS
   909   patterns; if this succeeds, the corresponding ML function is
   910   invoked, passing the Simplifier context and redex term.  Thus rules
   911   may be specifically fashioned for particular situations, resulting
   912   in a more powerful mechanism than term rewriting by a fixed set of
   913   rules.
   914 
   915   Any successful result needs to be a (possibly conditional) rewrite
   916   rule @{text "t \<equiv> u"} that is applicable to the current redex.  The
   917   rule will be applied just as any ordinary rewrite rule.  It is
   918   expected to be already in \emph{internal form}, bypassing the
   919   automatic preprocessing of object-level equivalences.
   920 
   921   \begin{matharray}{rcl}
   922     @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   923     simproc & : & @{text attribute} \\
   924   \end{matharray}
   925 
   926   @{rail "
   927     @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
   928       @{syntax text} \\ (@'identifier' (@{syntax nameref}+))?
   929     ;
   930 
   931     @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
   932   "}
   933 
   934   \begin{description}
   935 
   936   \item @{command "simproc_setup"} defines a named simplification
   937   procedure that is invoked by the Simplifier whenever any of the
   938   given term patterns match the current redex.  The implementation,
   939   which is provided as ML source text, needs to be of type @{ML_type
   940   "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type
   941   cterm} represents the current redex @{text r} and the result is
   942   supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a
   943   generalized version), or @{ML NONE} to indicate failure.  The
   944   @{ML_type simpset} argument holds the full context of the current
   945   Simplifier invocation, including the actual Isar proof context.  The
   946   @{ML_type morphism} informs about the difference of the original
   947   compilation context wrt.\ the one of the actual application later
   948   on.  The optional @{keyword "identifier"} specifies theorems that
   949   represent the logical content of the abstract theory of this
   950   simproc.
   951 
   952   Morphisms and identifiers are only relevant for simprocs that are
   953   defined within a local target context, e.g.\ in a locale.
   954 
   955   \item @{text "simproc add: name"} and @{text "simproc del: name"}
   956   add or delete named simprocs to the current Simplifier context.  The
   957   default is to add a simproc.  Note that @{command "simproc_setup"}
   958   already adds the new simproc to the subsequent context.
   959 
   960   \end{description}
   961 *}
   962 
   963 
   964 subsubsection {* Example *}
   965 
   966 text {* The following simplification procedure for @{thm
   967   [source=false, show_types] unit_eq} in HOL performs fine-grained
   968   control over rule application, beyond higher-order pattern matching.
   969   Declaring @{thm unit_eq} as @{attribute simp} directly would make
   970   the simplifier loop!  Note that a version of this simplification
   971   procedure is already active in Isabelle/HOL.  *}
   972 
   973 simproc_setup unit ("x::unit") = {*
   974   fn _ => fn _ => fn ct =>
   975     if HOLogic.is_unit (term_of ct) then NONE
   976     else SOME (mk_meta_eq @{thm unit_eq})
   977 *}
   978 
   979 text {* Since the Simplifier applies simplification procedures
   980   frequently, it is important to make the failure check in ML
   981   reasonably fast. *}
   982 
   983 
   984 subsection {* Configurable Simplifier strategies \label{sec:simp-strategies} *}
   985 
   986 text {* The core term-rewriting engine of the Simplifier is normally
   987   used in combination with some add-on components that modify the
   988   strategy and allow to integrate other non-Simplifier proof tools.
   989   These may be reconfigured in ML as explained below.  Even if the
   990   default strategies of object-logics like Isabelle/HOL are used
   991   unchanged, it helps to understand how the standard Simplifier
   992   strategies work. *}
   993 
   994 
   995 subsubsection {* The subgoaler *}
   996 
   997 text {*
   998   \begin{mldecls}
   999   @{index_ML Simplifier.set_subgoaler: "(Proof.context -> int -> tactic) ->
  1000   Proof.context -> Proof.context"} \\
  1001   @{index_ML Simplifier.prems_of: "Proof.context -> thm list"} \\
  1002   \end{mldecls}
  1003 
  1004   The subgoaler is the tactic used to solve subgoals arising out of
  1005   conditional rewrite rules or congruence rules.  The default should
  1006   be simplification itself.  In rare situations, this strategy may
  1007   need to be changed.  For example, if the premise of a conditional
  1008   rule is an instance of its conclusion, as in @{text "Suc ?m < ?n \<Longrightarrow>
  1009   ?m < ?n"}, the default strategy could loop.  % FIXME !??
  1010 
  1011   \begin{description}
  1012 
  1013   \item @{ML Simplifier.set_subgoaler}~@{text "tac ctxt"} sets the
  1014   subgoaler of the context to @{text "tac"}.  The tactic will
  1015   be applied to the context of the running Simplifier instance.
  1016 
  1017   \item @{ML Simplifier.prems_of}~@{text "ctxt"} retrieves the current
  1018   set of premises from the context.  This may be non-empty only if
  1019   the Simplifier has been told to utilize local assumptions in the
  1020   first place (cf.\ the options in \secref{sec:simp-meth}).
  1021 
  1022   \end{description}
  1023 
  1024   As an example, consider the following alternative subgoaler:
  1025 *}
  1026 
  1027 ML {*
  1028   fun subgoaler_tac ctxt =
  1029     assume_tac ORELSE'
  1030     resolve_tac (Simplifier.prems_of ctxt) ORELSE'
  1031     asm_simp_tac ctxt
  1032 *}
  1033 
  1034 text {* This tactic first tries to solve the subgoal by assumption or
  1035   by resolving with with one of the premises, calling simplification
  1036   only if that fails. *}
  1037 
  1038 
  1039 subsubsection {* The solver *}
  1040 
  1041 text {*
  1042   \begin{mldecls}
  1043   @{index_ML_type solver} \\
  1044   @{index_ML Simplifier.mk_solver: "string ->
  1045   (Proof.context -> int -> tactic) -> solver"} \\
  1046   @{index_ML_op setSolver: "Proof.context * solver -> Proof.context"} \\
  1047   @{index_ML_op addSolver: "Proof.context * solver -> Proof.context"} \\
  1048   @{index_ML_op setSSolver: "Proof.context * solver -> Proof.context"} \\
  1049   @{index_ML_op addSSolver: "Proof.context * solver -> Proof.context"} \\
  1050   \end{mldecls}
  1051 
  1052   A solver is a tactic that attempts to solve a subgoal after
  1053   simplification.  Its core functionality is to prove trivial subgoals
  1054   such as @{prop "True"} and @{text "t = t"}, but object-logics might
  1055   be more ambitious.  For example, Isabelle/HOL performs a restricted
  1056   version of linear arithmetic here.
  1057 
  1058   Solvers are packaged up in abstract type @{ML_type solver}, with
  1059   @{ML Simplifier.mk_solver} as the only operation to create a solver.
  1060 
  1061   \medskip Rewriting does not instantiate unknowns.  For example,
  1062   rewriting alone cannot prove @{text "a \<in> ?A"} since this requires
  1063   instantiating @{text "?A"}.  The solver, however, is an arbitrary
  1064   tactic and may instantiate unknowns as it pleases.  This is the only
  1065   way the Simplifier can handle a conditional rewrite rule whose
  1066   condition contains extra variables.  When a simplification tactic is
  1067   to be combined with other provers, especially with the Classical
  1068   Reasoner, it is important whether it can be considered safe or not.
  1069   For this reason a simpset contains two solvers: safe and unsafe.
  1070 
  1071   The standard simplification strategy solely uses the unsafe solver,
  1072   which is appropriate in most cases.  For special applications where
  1073   the simplification process is not allowed to instantiate unknowns
  1074   within the goal, simplification starts with the safe solver, but may
  1075   still apply the ordinary unsafe one in nested simplifications for
  1076   conditional rules or congruences. Note that in this way the overall
  1077   tactic is not totally safe: it may instantiate unknowns that appear
  1078   also in other subgoals.
  1079 
  1080   \begin{description}
  1081 
  1082   \item @{ML Simplifier.mk_solver}~@{text "name tac"} turns @{text
  1083   "tac"} into a solver; the @{text "name"} is only attached as a
  1084   comment and has no further significance.
  1085 
  1086   \item @{text "ctxt setSSolver solver"} installs @{text "solver"} as
  1087   the safe solver of @{text "ctxt"}.
  1088 
  1089   \item @{text "ctxt addSSolver solver"} adds @{text "solver"} as an
  1090   additional safe solver; it will be tried after the solvers which had
  1091   already been present in @{text "ctxt"}.
  1092 
  1093   \item @{text "ctxt setSolver solver"} installs @{text "solver"} as the
  1094   unsafe solver of @{text "ctxt"}.
  1095 
  1096   \item @{text "ctxt addSolver solver"} adds @{text "solver"} as an
  1097   additional unsafe solver; it will be tried after the solvers which
  1098   had already been present in @{text "ctxt"}.
  1099 
  1100   \end{description}
  1101 
  1102   \medskip The solver tactic is invoked with the context of the
  1103   running Simplifier.  Further operations
  1104   may be used to retrieve relevant information, such as the list of
  1105   local Simplifier premises via @{ML Simplifier.prems_of} --- this
  1106   list may be non-empty only if the Simplifier runs in a mode that
  1107   utilizes local assumptions (see also \secref{sec:simp-meth}).  The
  1108   solver is also presented the full goal including its assumptions in
  1109   any case.  Thus it can use these (e.g.\ by calling @{ML
  1110   assume_tac}), even if the Simplifier proper happens to ignore local
  1111   premises at the moment.
  1112 
  1113   \medskip As explained before, the subgoaler is also used to solve
  1114   the premises of congruence rules.  These are usually of the form
  1115   @{text "s = ?x"}, where @{text "s"} needs to be simplified and
  1116   @{text "?x"} needs to be instantiated with the result.  Typically,
  1117   the subgoaler will invoke the Simplifier at some point, which will
  1118   eventually call the solver.  For this reason, solver tactics must be
  1119   prepared to solve goals of the form @{text "t = ?x"}, usually by
  1120   reflexivity.  In particular, reflexivity should be tried before any
  1121   of the fancy automated proof tools.
  1122 
  1123   It may even happen that due to simplification the subgoal is no
  1124   longer an equality.  For example, @{text "False \<longleftrightarrow> ?Q"} could be
  1125   rewritten to @{text "\<not> ?Q"}.  To cover this case, the solver could
  1126   try resolving with the theorem @{text "\<not> False"} of the
  1127   object-logic.
  1128 
  1129   \medskip
  1130 
  1131   \begin{warn}
  1132   If a premise of a congruence rule cannot be proved, then the
  1133   congruence is ignored.  This should only happen if the rule is
  1134   \emph{conditional} --- that is, contains premises not of the form
  1135   @{text "t = ?x"}.  Otherwise it indicates that some congruence rule,
  1136   or possibly the subgoaler or solver, is faulty.
  1137   \end{warn}
  1138 *}
  1139 
  1140 
  1141 subsubsection {* The looper *}
  1142 
  1143 text {*
  1144   \begin{mldecls}
  1145   @{index_ML_op setloop: "Proof.context *
  1146   (Proof.context -> int -> tactic) -> Proof.context"} \\
  1147   @{index_ML_op addloop: "Proof.context *
  1148   (string * (Proof.context -> int -> tactic))
  1149   -> Proof.context"} \\
  1150   @{index_ML_op delloop: "Proof.context * string -> Proof.context"} \\
  1151   @{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
  1152   @{index_ML Splitter.del_split: "thm -> Proof.context -> Proof.context"} \\
  1153   \end{mldecls}
  1154 
  1155   The looper is a list of tactics that are applied after
  1156   simplification, in case the solver failed to solve the simplified
  1157   goal.  If the looper succeeds, the simplification process is started
  1158   all over again.  Each of the subgoals generated by the looper is
  1159   attacked in turn, in reverse order.
  1160 
  1161   A typical looper is \emph{case splitting}: the expansion of a
  1162   conditional.  Another possibility is to apply an elimination rule on
  1163   the assumptions.  More adventurous loopers could start an induction.
  1164 
  1165   \begin{description}
  1166 
  1167   \item @{text "ctxt setloop tac"} installs @{text "tac"} as the only
  1168   looper tactic of @{text "ctxt"}.
  1169 
  1170   \item @{text "ctxt addloop (name, tac)"} adds @{text "tac"} as an
  1171   additional looper tactic with name @{text "name"}, which is
  1172   significant for managing the collection of loopers.  The tactic will
  1173   be tried after the looper tactics that had already been present in
  1174   @{text "ctxt"}.
  1175 
  1176   \item @{text "ctxt delloop name"} deletes the looper tactic that was
  1177   associated with @{text "name"} from @{text "ctxt"}.
  1178 
  1179   \item @{ML Splitter.add_split}~@{text "thm ctxt"} adds split tactics
  1180   for @{text "thm"} as additional looper tactics of @{text "ctxt"}.
  1181 
  1182   \item @{ML Splitter.del_split}~@{text "thm ctxt"} deletes the split
  1183   tactic corresponding to @{text thm} from the looper tactics of
  1184   @{text "ctxt"}.
  1185 
  1186   \end{description}
  1187 
  1188   The splitter replaces applications of a given function; the
  1189   right-hand side of the replacement can be anything.  For example,
  1190   here is a splitting rule for conditional expressions:
  1191 
  1192   @{text [display] "?P (if ?Q ?x ?y) \<longleftrightarrow> (?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y)"}
  1193 
  1194   Another example is the elimination operator for Cartesian products
  1195   (which happens to be called @{text split} in Isabelle/HOL:
  1196 
  1197   @{text [display] "?P (split ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"}
  1198 
  1199   For technical reasons, there is a distinction between case splitting
  1200   in the conclusion and in the premises of a subgoal.  The former is
  1201   done by @{ML Splitter.split_tac} with rules like @{thm [source]
  1202   split_if} or @{thm [source] option.split}, which do not split the
  1203   subgoal, while the latter is done by @{ML Splitter.split_asm_tac}
  1204   with rules like @{thm [source] split_if_asm} or @{thm [source]
  1205   option.split_asm}, which split the subgoal.  The function @{ML
  1206   Splitter.add_split} automatically takes care of which tactic to
  1207   call, analyzing the form of the rules given as argument; it is the
  1208   same operation behind @{text "split"} attribute or method modifier
  1209   syntax in the Isar source language.
  1210 
  1211   Case splits should be allowed only when necessary; they are
  1212   expensive and hard to control.  Case-splitting on if-expressions in
  1213   the conclusion is usually beneficial, so it is enabled by default in
  1214   Isabelle/HOL and Isabelle/FOL/ZF.
  1215 
  1216   \begin{warn}
  1217   With @{ML Splitter.split_asm_tac} as looper component, the
  1218   Simplifier may split subgoals!  This might cause unexpected problems
  1219   in tactic expressions that silently assume 0 or 1 subgoals after
  1220   simplification.
  1221   \end{warn}
  1222 *}
  1223 
  1224 
  1225 subsection {* Forward simplification \label{sec:simp-forward} *}
  1226 
  1227 text {*
  1228   \begin{matharray}{rcl}
  1229     @{attribute_def simplified} & : & @{text attribute} \\
  1230   \end{matharray}
  1231 
  1232   @{rail "
  1233     @@{attribute simplified} opt? @{syntax thmrefs}?
  1234     ;
  1235 
  1236     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
  1237   "}
  1238 
  1239   \begin{description}
  1240   
  1241   \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to
  1242   be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,
  1243   a\<^sub>n"}, or the implicit Simplifier context if no arguments are given.
  1244   The result is fully simplified by default, including assumptions and
  1245   conclusion; the options @{text no_asm} etc.\ tune the Simplifier in
  1246   the same way as the for the @{text simp} method.
  1247 
  1248   Note that forward simplification restricts the simplifier to its
  1249   most basic operation of term rewriting; solver and looper tactics
  1250   (\secref{sec:simp-strategies}) are \emph{not} involved here.  The
  1251   @{attribute simplified} attribute should be only rarely required
  1252   under normal circumstances.
  1253 
  1254   \end{description}
  1255 *}
  1256 
  1257 
  1258 section {* The Classical Reasoner \label{sec:classical} *}
  1259 
  1260 subsection {* Basic concepts *}
  1261 
  1262 text {* Although Isabelle is generic, many users will be working in
  1263   some extension of classical first-order logic.  Isabelle/ZF is built
  1264   upon theory FOL, while Isabelle/HOL conceptually contains
  1265   first-order logic as a fragment.  Theorem-proving in predicate logic
  1266   is undecidable, but many automated strategies have been developed to
  1267   assist in this task.
  1268 
  1269   Isabelle's classical reasoner is a generic package that accepts
  1270   certain information about a logic and delivers a suite of automatic
  1271   proof tools, based on rules that are classified and declared in the
  1272   context.  These proof procedures are slow and simplistic compared
  1273   with high-end automated theorem provers, but they can save
  1274   considerable time and effort in practice.  They can prove theorems
  1275   such as Pelletier's \cite{pelletier86} problems 40 and 41 in a few
  1276   milliseconds (including full proof reconstruction): *}
  1277 
  1278 lemma "(\<exists>y. \<forall>x. F x y \<longleftrightarrow> F x x) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. F z y \<longleftrightarrow> \<not> F z x)"
  1279   by blast
  1280 
  1281 lemma "(\<forall>z. \<exists>y. \<forall>x. f x y \<longleftrightarrow> f x z \<and> \<not> f x x) \<longrightarrow> \<not> (\<exists>z. \<forall>x. f x z)"
  1282   by blast
  1283 
  1284 text {* The proof tools are generic.  They are not restricted to
  1285   first-order logic, and have been heavily used in the development of
  1286   the Isabelle/HOL library and applications.  The tactics can be
  1287   traced, and their components can be called directly; in this manner,
  1288   any proof can be viewed interactively.  *}
  1289 
  1290 
  1291 subsubsection {* The sequent calculus *}
  1292 
  1293 text {* Isabelle supports natural deduction, which is easy to use for
  1294   interactive proof.  But natural deduction does not easily lend
  1295   itself to automation, and has a bias towards intuitionism.  For
  1296   certain proofs in classical logic, it can not be called natural.
  1297   The \emph{sequent calculus}, a generalization of natural deduction,
  1298   is easier to automate.
  1299 
  1300   A \textbf{sequent} has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"}
  1301   and @{text "\<Delta>"} are sets of formulae.\footnote{For first-order
  1302   logic, sequents can equivalently be made from lists or multisets of
  1303   formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is
  1304   \textbf{valid} if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or>
  1305   Q\<^sub>n"}.  Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which
  1306   is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals.  A
  1307   sequent is \textbf{basic} if its left and right sides have a common
  1308   formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially
  1309   valid.
  1310 
  1311   Sequent rules are classified as \textbf{right} or \textbf{left},
  1312   indicating which side of the @{text "\<turnstile>"} symbol they operate on.
  1313   Rules that operate on the right side are analogous to natural
  1314   deduction's introduction rules, and left rules are analogous to
  1315   elimination rules.  The sequent calculus analogue of @{text "(\<longrightarrow>I)"}
  1316   is the rule
  1317   \[
  1318   \infer[@{text "(\<longrightarrow>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<longrightarrow> Q"}}{@{text "P, \<Gamma> \<turnstile> \<Delta>, Q"}}
  1319   \]
  1320   Applying the rule backwards, this breaks down some implication on
  1321   the right side of a sequent; @{text "\<Gamma>"} and @{text "\<Delta>"} stand for
  1322   the sets of formulae that are unaffected by the inference.  The
  1323   analogue of the pair @{text "(\<or>I1)"} and @{text "(\<or>I2)"} is the
  1324   single rule
  1325   \[
  1326   \infer[@{text "(\<or>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<or> Q"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P, Q"}}
  1327   \]
  1328   This breaks down some disjunction on the right side, replacing it by
  1329   both disjuncts.  Thus, the sequent calculus is a kind of
  1330   multiple-conclusion logic.
  1331 
  1332   To illustrate the use of multiple formulae on the right, let us
  1333   prove the classical theorem @{text "(P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}.  Working
  1334   backwards, we reduce this formula to a basic sequent:
  1335   \[
  1336   \infer[@{text "(\<or>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}}
  1337     {\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q), (Q \<longrightarrow> P)"}}
  1338       {\infer[@{text "(\<longrightarrow>R)"}]{@{text "P \<turnstile> Q, (Q \<longrightarrow> P)"}}
  1339         {@{text "P, Q \<turnstile> Q, P"}}}}
  1340   \]
  1341 
  1342   This example is typical of the sequent calculus: start with the
  1343   desired theorem and apply rules backwards in a fairly arbitrary
  1344   manner.  This yields a surprisingly effective proof procedure.
  1345   Quantifiers add only few complications, since Isabelle handles
  1346   parameters and schematic variables.  See \cite[Chapter
  1347   10]{paulson-ml2} for further discussion.  *}
  1348 
  1349 
  1350 subsubsection {* Simulating sequents by natural deduction *}
  1351 
  1352 text {* Isabelle can represent sequents directly, as in the
  1353   object-logic LK.  But natural deduction is easier to work with, and
  1354   most object-logics employ it.  Fortunately, we can simulate the
  1355   sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} by the Isabelle formula
  1356   @{text "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>2 \<Longrightarrow> ... \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> Q\<^sub>1"} where the order of
  1357   the assumptions and the choice of @{text "Q\<^sub>1"} are arbitrary.
  1358   Elim-resolution plays a key role in simulating sequent proofs.
  1359 
  1360   We can easily handle reasoning on the left.  Elim-resolution with
  1361   the rules @{text "(\<or>E)"}, @{text "(\<bottom>E)"} and @{text "(\<exists>E)"} achieves
  1362   a similar effect as the corresponding sequent rules.  For the other
  1363   connectives, we use sequent-style elimination rules instead of
  1364   destruction rules such as @{text "(\<and>E1, 2)"} and @{text "(\<forall>E)"}.
  1365   But note that the rule @{text "(\<not>L)"} has no effect under our
  1366   representation of sequents!
  1367   \[
  1368   \infer[@{text "(\<not>L)"}]{@{text "\<not> P, \<Gamma> \<turnstile> \<Delta>"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P"}}
  1369   \]
  1370 
  1371   What about reasoning on the right?  Introduction rules can only
  1372   affect the formula in the conclusion, namely @{text "Q\<^sub>1"}.  The
  1373   other right-side formulae are represented as negated assumptions,
  1374   @{text "\<not> Q\<^sub>2, \<dots>, \<not> Q\<^sub>n"}.  In order to operate on one of these, it
  1375   must first be exchanged with @{text "Q\<^sub>1"}.  Elim-resolution with the
  1376   @{text swap} rule has this effect: @{text "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"}
  1377 
  1378   To ensure that swaps occur only when necessary, each introduction
  1379   rule is converted into a swapped form: it is resolved with the
  1380   second premise of @{text "(swap)"}.  The swapped form of @{text
  1381   "(\<and>I)"}, which might be called @{text "(\<not>\<and>E)"}, is
  1382   @{text [display] "\<not> (P \<and> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (\<not> R \<Longrightarrow> Q) \<Longrightarrow> R"}
  1383 
  1384   Similarly, the swapped form of @{text "(\<longrightarrow>I)"} is
  1385   @{text [display] "\<not> (P \<longrightarrow> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P \<Longrightarrow> Q) \<Longrightarrow> R"}
  1386 
  1387   Swapped introduction rules are applied using elim-resolution, which
  1388   deletes the negated formula.  Our representation of sequents also
  1389   requires the use of ordinary introduction rules.  If we had no
  1390   regard for readability of intermediate goal states, we could treat
  1391   the right side more uniformly by representing sequents as @{text
  1392   [display] "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> \<bottom>"}
  1393 *}
  1394 
  1395 
  1396 subsubsection {* Extra rules for the sequent calculus *}
  1397 
  1398 text {* As mentioned, destruction rules such as @{text "(\<and>E1, 2)"} and
  1399   @{text "(\<forall>E)"} must be replaced by sequent-style elimination rules.
  1400   In addition, we need rules to embody the classical equivalence
  1401   between @{text "P \<longrightarrow> Q"} and @{text "\<not> P \<or> Q"}.  The introduction
  1402   rules @{text "(\<or>I1, 2)"} are replaced by a rule that simulates
  1403   @{text "(\<or>R)"}: @{text [display] "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"}
  1404 
  1405   The destruction rule @{text "(\<longrightarrow>E)"} is replaced by @{text [display]
  1406   "(P \<longrightarrow> Q) \<Longrightarrow> (\<not> P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"}
  1407 
  1408   Quantifier replication also requires special rules.  In classical
  1409   logic, @{text "\<exists>x. P x"} is equivalent to @{text "\<not> (\<forall>x. \<not> P x)"};
  1410   the rules @{text "(\<exists>R)"} and @{text "(\<forall>L)"} are dual:
  1411   \[
  1412   \infer[@{text "(\<exists>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x"}}{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x, P t"}}
  1413   \qquad
  1414   \infer[@{text "(\<forall>L)"}]{@{text "\<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}{@{text "P t, \<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}
  1415   \]
  1416   Thus both kinds of quantifier may be replicated.  Theorems requiring
  1417   multiple uses of a universal formula are easy to invent; consider
  1418   @{text [display] "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P a \<longrightarrow> P (f\<^sup>n a)"} for any
  1419   @{text "n > 1"}.  Natural examples of the multiple use of an
  1420   existential formula are rare; a standard one is @{text "\<exists>x. \<forall>y. P x
  1421   \<longrightarrow> P y"}.
  1422 
  1423   Forgoing quantifier replication loses completeness, but gains
  1424   decidability, since the search space becomes finite.  Many useful
  1425   theorems can be proved without replication, and the search generally
  1426   delivers its verdict in a reasonable time.  To adopt this approach,
  1427   represent the sequent rules @{text "(\<exists>R)"}, @{text "(\<exists>L)"} and
  1428   @{text "(\<forall>R)"} by @{text "(\<exists>I)"}, @{text "(\<exists>E)"} and @{text "(\<forall>I)"},
  1429   respectively, and put @{text "(\<forall>E)"} into elimination form: @{text
  1430   [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"}
  1431 
  1432   Elim-resolution with this rule will delete the universal formula
  1433   after a single use.  To replicate universal quantifiers, replace the
  1434   rule by @{text [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"}
  1435 
  1436   To replicate existential quantifiers, replace @{text "(\<exists>I)"} by
  1437   @{text [display] "(\<not> (\<exists>x. P x) \<Longrightarrow> P t) \<Longrightarrow> \<exists>x. P x"}
  1438 
  1439   All introduction rules mentioned above are also useful in swapped
  1440   form.
  1441 
  1442   Replication makes the search space infinite; we must apply the rules
  1443   with care.  The classical reasoner distinguishes between safe and
  1444   unsafe rules, applying the latter only when there is no alternative.
  1445   Depth-first search may well go down a blind alley; best-first search
  1446   is better behaved in an infinite search space.  However, quantifier
  1447   replication is too expensive to prove any but the simplest theorems.
  1448 *}
  1449 
  1450 
  1451 subsection {* Rule declarations *}
  1452 
  1453 text {* The proof tools of the Classical Reasoner depend on
  1454   collections of rules declared in the context, which are classified
  1455   as introduction, elimination or destruction and as \emph{safe} or
  1456   \emph{unsafe}.  In general, safe rules can be attempted blindly,
  1457   while unsafe rules must be used with care.  A safe rule must never
  1458   reduce a provable goal to an unprovable set of subgoals.
  1459 
  1460   The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P
  1461   \<or> Q"} to @{text "P"}, which might turn out as premature choice of an
  1462   unprovable subgoal.  Any rule is unsafe whose premises contain new
  1463   unknowns.  The elimination rule @{text "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} is
  1464   unsafe, since it is applied via elim-resolution, which discards the
  1465   assumption @{text "\<forall>x. P x"} and replaces it by the weaker
  1466   assumption @{text "P t"}.  The rule @{text "P t \<Longrightarrow> \<exists>x. P x"} is
  1467   unsafe for similar reasons.  The quantifier duplication rule @{text
  1468   "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} is unsafe in a different sense:
  1469   since it keeps the assumption @{text "\<forall>x. P x"}, it is prone to
  1470   looping.  In classical first-order logic, all rules are safe except
  1471   those mentioned above.
  1472 
  1473   The safe~/ unsafe distinction is vague, and may be regarded merely
  1474   as a way of giving some rules priority over others.  One could argue
  1475   that @{text "(\<or>E)"} is unsafe, because repeated application of it
  1476   could generate exponentially many subgoals.  Induction rules are
  1477   unsafe because inductive proofs are difficult to set up
  1478   automatically.  Any inference is unsafe that instantiates an unknown
  1479   in the proof state --- thus matching must be used, rather than
  1480   unification.  Even proof by assumption is unsafe if it instantiates
  1481   unknowns shared with other subgoals.
  1482 
  1483   \begin{matharray}{rcl}
  1484     @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
  1485     @{attribute_def intro} & : & @{text attribute} \\
  1486     @{attribute_def elim} & : & @{text attribute} \\
  1487     @{attribute_def dest} & : & @{text attribute} \\
  1488     @{attribute_def rule} & : & @{text attribute} \\
  1489     @{attribute_def iff} & : & @{text attribute} \\
  1490     @{attribute_def swapped} & : & @{text attribute} \\
  1491   \end{matharray}
  1492 
  1493   @{rail "
  1494     (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
  1495     ;
  1496     @@{attribute rule} 'del'
  1497     ;
  1498     @@{attribute iff} (((() | 'add') '?'?) | 'del')
  1499   "}
  1500 
  1501   \begin{description}
  1502 
  1503   \item @{command "print_claset"} prints the collection of rules
  1504   declared to the Classical Reasoner, i.e.\ the @{ML_type claset}
  1505   within the context.
  1506 
  1507   \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
  1508   declare introduction, elimination, and destruction rules,
  1509   respectively.  By default, rules are considered as \emph{unsafe}
  1510   (i.e.\ not applied blindly without backtracking), while ``@{text
  1511   "!"}'' classifies as \emph{safe}.  Rule declarations marked by
  1512   ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
  1513   \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
  1514   of the @{method rule} method).  The optional natural number
  1515   specifies an explicit weight argument, which is ignored by the
  1516   automated reasoning tools, but determines the search order of single
  1517   rule steps.
  1518 
  1519   Introduction rules are those that can be applied using ordinary
  1520   resolution.  Their swapped forms are generated internally, which
  1521   will be applied using elim-resolution.  Elimination rules are
  1522   applied using elim-resolution.  Rules are sorted by the number of
  1523   new subgoals they will yield; rules that generate the fewest
  1524   subgoals will be tried first.  Otherwise, later declarations take
  1525   precedence over earlier ones.
  1526 
  1527   Rules already present in the context with the same classification
  1528   are ignored.  A warning is printed if the rule has already been
  1529   added with some other classification, but the rule is added anyway
  1530   as requested.
  1531 
  1532   \item @{attribute rule}~@{text del} deletes all occurrences of a
  1533   rule from the classical context, regardless of its classification as
  1534   introduction~/ elimination~/ destruction and safe~/ unsafe.
  1535 
  1536   \item @{attribute iff} declares logical equivalences to the
  1537   Simplifier and the Classical reasoner at the same time.
  1538   Non-conditional rules result in a safe introduction and elimination
  1539   pair; conditional ones are considered unsafe.  Rules with negative
  1540   conclusion are automatically inverted (using @{text "\<not>"}-elimination
  1541   internally).
  1542 
  1543   The ``@{text "?"}'' version of @{attribute iff} declares rules to
  1544   the Isabelle/Pure context only, and omits the Simplifier
  1545   declaration.
  1546 
  1547   \item @{attribute swapped} turns an introduction rule into an
  1548   elimination, by resolving with the classical swap principle @{text
  1549   "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position.  This is mainly for
  1550   illustrative purposes: the Classical Reasoner already swaps rules
  1551   internally as explained above.
  1552 
  1553   \end{description}
  1554 *}
  1555 
  1556 
  1557 subsection {* Structured methods *}
  1558 
  1559 text {*
  1560   \begin{matharray}{rcl}
  1561     @{method_def rule} & : & @{text method} \\
  1562     @{method_def contradiction} & : & @{text method} \\
  1563   \end{matharray}
  1564 
  1565   @{rail "
  1566     @@{method rule} @{syntax thmrefs}?
  1567   "}
  1568 
  1569   \begin{description}
  1570 
  1571   \item @{method rule} as offered by the Classical Reasoner is a
  1572   refinement over the Pure one (see \secref{sec:pure-meth-att}).  Both
  1573   versions work the same, but the classical version observes the
  1574   classical rule context in addition to that of Isabelle/Pure.
  1575 
  1576   Common object logics (HOL, ZF, etc.) declare a rich collection of
  1577   classical rules (even if these would qualify as intuitionistic
  1578   ones), but only few declarations to the rule context of
  1579   Isabelle/Pure (\secref{sec:pure-meth-att}).
  1580 
  1581   \item @{method contradiction} solves some goal by contradiction,
  1582   deriving any result from both @{text "\<not> A"} and @{text A}.  Chained
  1583   facts, which are guaranteed to participate, may appear in either
  1584   order.
  1585 
  1586   \end{description}
  1587 *}
  1588 
  1589 
  1590 subsection {* Fully automated methods *}
  1591 
  1592 text {*
  1593   \begin{matharray}{rcl}
  1594     @{method_def blast} & : & @{text method} \\
  1595     @{method_def auto} & : & @{text method} \\
  1596     @{method_def force} & : & @{text method} \\
  1597     @{method_def fast} & : & @{text method} \\
  1598     @{method_def slow} & : & @{text method} \\
  1599     @{method_def best} & : & @{text method} \\
  1600     @{method_def fastforce} & : & @{text method} \\
  1601     @{method_def slowsimp} & : & @{text method} \\
  1602     @{method_def bestsimp} & : & @{text method} \\
  1603     @{method_def deepen} & : & @{text method} \\
  1604   \end{matharray}
  1605 
  1606   @{rail "
  1607     @@{method blast} @{syntax nat}? (@{syntax clamod} * )
  1608     ;
  1609     @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )
  1610     ;
  1611     @@{method force} (@{syntax clasimpmod} * )
  1612     ;
  1613     (@@{method fast} | @@{method slow} | @@{method best}) (@{syntax clamod} * )
  1614     ;
  1615     (@@{method fastforce} | @@{method slowsimp} | @@{method bestsimp})
  1616       (@{syntax clasimpmod} * )
  1617     ;
  1618     @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
  1619     ;
  1620     @{syntax_def clamod}:
  1621       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
  1622     ;
  1623     @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
  1624       ('cong' | 'split') (() | 'add' | 'del') |
  1625       'iff' (((() | 'add') '?'?) | 'del') |
  1626       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
  1627   "}
  1628 
  1629   \begin{description}
  1630 
  1631   \item @{method blast} is a separate classical tableau prover that
  1632   uses the same classical rule declarations as explained before.
  1633 
  1634   Proof search is coded directly in ML using special data structures.
  1635   A successful proof is then reconstructed using regular Isabelle
  1636   inferences.  It is faster and more powerful than the other classical
  1637   reasoning tools, but has major limitations too.
  1638 
  1639   \begin{itemize}
  1640 
  1641   \item It does not use the classical wrapper tacticals, such as the
  1642   integration with the Simplifier of @{method fastforce}.
  1643 
  1644   \item It does not perform higher-order unification, as needed by the
  1645   rule @{thm [source=false] rangeI} in HOL.  There are often
  1646   alternatives to such rules, for example @{thm [source=false]
  1647   range_eqI}.
  1648 
  1649   \item Function variables may only be applied to parameters of the
  1650   subgoal.  (This restriction arises because the prover does not use
  1651   higher-order unification.)  If other function variables are present
  1652   then the prover will fail with the message \texttt{Function Var's
  1653   argument not a bound variable}.
  1654 
  1655   \item Its proof strategy is more general than @{method fast} but can
  1656   be slower.  If @{method blast} fails or seems to be running forever,
  1657   try @{method fast} and the other proof tools described below.
  1658 
  1659   \end{itemize}
  1660 
  1661   The optional integer argument specifies a bound for the number of
  1662   unsafe steps used in a proof.  By default, @{method blast} starts
  1663   with a bound of 0 and increases it successively to 20.  In contrast,
  1664   @{text "(blast lim)"} tries to prove the goal using a search bound
  1665   of @{text "lim"}.  Sometimes a slow proof using @{method blast} can
  1666   be made much faster by supplying the successful search bound to this
  1667   proof method instead.
  1668 
  1669   \item @{method auto} combines classical reasoning with
  1670   simplification.  It is intended for situations where there are a lot
  1671   of mostly trivial subgoals; it proves all the easy ones, leaving the
  1672   ones it cannot prove.  Occasionally, attempting to prove the hard
  1673   ones may take a long time.
  1674 
  1675   The optional depth arguments in @{text "(auto m n)"} refer to its
  1676   builtin classical reasoning procedures: @{text m} (default 4) is for
  1677   @{method blast}, which is tried first, and @{text n} (default 2) is
  1678   for a slower but more general alternative that also takes wrappers
  1679   into account.
  1680 
  1681   \item @{method force} is intended to prove the first subgoal
  1682   completely, using many fancy proof tools and performing a rather
  1683   exhaustive search.  As a result, proof attempts may take rather long
  1684   or diverge easily.
  1685 
  1686   \item @{method fast}, @{method best}, @{method slow} attempt to
  1687   prove the first subgoal using sequent-style reasoning as explained
  1688   before.  Unlike @{method blast}, they construct proofs directly in
  1689   Isabelle.
  1690 
  1691   There is a difference in search strategy and back-tracking: @{method
  1692   fast} uses depth-first search and @{method best} uses best-first
  1693   search (guided by a heuristic function: normally the total size of
  1694   the proof state).
  1695 
  1696   Method @{method slow} is like @{method fast}, but conducts a broader
  1697   search: it may, when backtracking from a failed proof attempt, undo
  1698   even the step of proving a subgoal by assumption.
  1699 
  1700   \item @{method fastforce}, @{method slowsimp}, @{method bestsimp}
  1701   are like @{method fast}, @{method slow}, @{method best},
  1702   respectively, but use the Simplifier as additional wrapper. The name
  1703   @{method fastforce}, reflects the behaviour of this popular method
  1704   better without requiring an understanding of its implementation.
  1705 
  1706   \item @{method deepen} works by exhaustive search up to a certain
  1707   depth.  The start depth is 4 (unless specified explicitly), and the
  1708   depth is increased iteratively up to 10.  Unsafe rules are modified
  1709   to preserve the formula they act on, so that it be used repeatedly.
  1710   This method can prove more goals than @{method fast}, but is much
  1711   slower, for example if the assumptions have many universal
  1712   quantifiers.
  1713 
  1714   \end{description}
  1715 
  1716   Any of the above methods support additional modifiers of the context
  1717   of classical (and simplifier) rules, but the ones related to the
  1718   Simplifier are explicitly prefixed by @{text simp} here.  The
  1719   semantics of these ad-hoc rule declarations is analogous to the
  1720   attributes given before.  Facts provided by forward chaining are
  1721   inserted into the goal before commencing proof search.
  1722 *}
  1723 
  1724 
  1725 subsection {* Partially automated methods *}
  1726 
  1727 text {* These proof methods may help in situations when the
  1728   fully-automated tools fail.  The result is a simpler subgoal that
  1729   can be tackled by other means, such as by manual instantiation of
  1730   quantifiers.
  1731 
  1732   \begin{matharray}{rcl}
  1733     @{method_def safe} & : & @{text method} \\
  1734     @{method_def clarify} & : & @{text method} \\
  1735     @{method_def clarsimp} & : & @{text method} \\
  1736   \end{matharray}
  1737 
  1738   @{rail "
  1739     (@@{method safe} | @@{method clarify}) (@{syntax clamod} * )
  1740     ;
  1741     @@{method clarsimp} (@{syntax clasimpmod} * )
  1742   "}
  1743 
  1744   \begin{description}
  1745 
  1746   \item @{method safe} repeatedly performs safe steps on all subgoals.
  1747   It is deterministic, with at most one outcome.
  1748 
  1749   \item @{method clarify} performs a series of safe steps without
  1750   splitting subgoals; see also @{method clarify_step}.
  1751 
  1752   \item @{method clarsimp} acts like @{method clarify}, but also does
  1753   simplification.  Note that if the Simplifier context includes a
  1754   splitter for the premises, the subgoal may still be split.
  1755 
  1756   \end{description}
  1757 *}
  1758 
  1759 
  1760 subsection {* Single-step tactics *}
  1761 
  1762 text {*
  1763   \begin{matharray}{rcl}
  1764     @{method_def safe_step} & : & @{text method} \\
  1765     @{method_def inst_step} & : & @{text method} \\
  1766     @{method_def step} & : & @{text method} \\
  1767     @{method_def slow_step} & : & @{text method} \\
  1768     @{method_def clarify_step} & : &  @{text method} \\
  1769   \end{matharray}
  1770 
  1771   These are the primitive tactics behind the automated proof methods
  1772   of the Classical Reasoner.  By calling them yourself, you can
  1773   execute these procedures one step at a time.
  1774 
  1775   \begin{description}
  1776 
  1777   \item @{method safe_step} performs a safe step on the first subgoal.
  1778   The safe wrapper tacticals are applied to a tactic that may include
  1779   proof by assumption or Modus Ponens (taking care not to instantiate
  1780   unknowns), or substitution.
  1781 
  1782   \item @{method inst_step} is like @{method safe_step}, but allows
  1783   unknowns to be instantiated.
  1784 
  1785   \item @{method step} is the basic step of the proof procedure, it
  1786   operates on the first subgoal.  The unsafe wrapper tacticals are
  1787   applied to a tactic that tries @{method safe}, @{method inst_step},
  1788   or applies an unsafe rule from the context.
  1789 
  1790   \item @{method slow_step} resembles @{method step}, but allows
  1791   backtracking between using safe rules with instantiation (@{method
  1792   inst_step}) and using unsafe rules.  The resulting search space is
  1793   larger.
  1794 
  1795   \item @{method clarify_step} performs a safe step on the first
  1796   subgoal; no splitting step is applied.  For example, the subgoal
  1797   @{text "A \<and> B"} is left as a conjunction.  Proof by assumption,
  1798   Modus Ponens, etc., may be performed provided they do not
  1799   instantiate unknowns.  Assumptions of the form @{text "x = t"} may
  1800   be eliminated.  The safe wrapper tactical is applied.
  1801 
  1802   \end{description}
  1803 *}
  1804 
  1805 
  1806 subsection {* Modifying the search step *}
  1807 
  1808 text {*
  1809   \begin{mldecls}
  1810     @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
  1811     @{index_ML_op addSWrapper: "Proof.context *
  1812   (string * (Proof.context -> wrapper)) -> Proof.context"} \\
  1813     @{index_ML_op addSbefore: "Proof.context *
  1814   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
  1815     @{index_ML_op addSafter: "Proof.context *
  1816   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
  1817     @{index_ML_op delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
  1818     @{index_ML_op addWrapper: "Proof.context *
  1819   (string * (Proof.context -> wrapper)) -> Proof.context"} \\
  1820     @{index_ML_op addbefore: "Proof.context *
  1821   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
  1822     @{index_ML_op addafter: "Proof.context *
  1823   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
  1824     @{index_ML_op delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
  1825     @{index_ML addSss: "Proof.context -> Proof.context"} \\
  1826     @{index_ML addss: "Proof.context -> Proof.context"} \\
  1827   \end{mldecls}
  1828 
  1829   The proof strategy of the Classical Reasoner is simple.  Perform as
  1830   many safe inferences as possible; or else, apply certain safe rules,
  1831   allowing instantiation of unknowns; or else, apply an unsafe rule.
  1832   The tactics also eliminate assumptions of the form @{text "x = t"}
  1833   by substitution if they have been set up to do so.  They may perform
  1834   a form of Modus Ponens: if there are assumptions @{text "P \<longrightarrow> Q"} and
  1835   @{text "P"}, then replace @{text "P \<longrightarrow> Q"} by @{text "Q"}.
  1836 
  1837   The classical reasoning tools --- except @{method blast} --- allow
  1838   to modify this basic proof strategy by applying two lists of
  1839   arbitrary \emph{wrapper tacticals} to it.  The first wrapper list,
  1840   which is considered to contain safe wrappers only, affects @{method
  1841   safe_step} and all the tactics that call it.  The second one, which
  1842   may contain unsafe wrappers, affects the unsafe parts of @{method
  1843   step}, @{method slow_step}, and the tactics that call them.  A
  1844   wrapper transforms each step of the search, for example by
  1845   attempting other tactics before or after the original step tactic.
  1846   All members of a wrapper list are applied in turn to the respective
  1847   step tactic.
  1848 
  1849   Initially the two wrapper lists are empty, which means no
  1850   modification of the step tactics. Safe and unsafe wrappers are added
  1851   to a claset with the functions given below, supplying them with
  1852   wrapper names.  These names may be used to selectively delete
  1853   wrappers.
  1854 
  1855   \begin{description}
  1856 
  1857   \item @{text "ctxt addSWrapper (name, wrapper)"} adds a new wrapper,
  1858   which should yield a safe tactic, to modify the existing safe step
  1859   tactic.
  1860 
  1861   \item @{text "ctxt addSbefore (name, tac)"} adds the given tactic as a
  1862   safe wrapper, such that it is tried \emph{before} each safe step of
  1863   the search.
  1864 
  1865   \item @{text "ctxt addSafter (name, tac)"} adds the given tactic as a
  1866   safe wrapper, such that it is tried when a safe step of the search
  1867   would fail.
  1868 
  1869   \item @{text "ctxt delSWrapper name"} deletes the safe wrapper with
  1870   the given name.
  1871 
  1872   \item @{text "ctxt addWrapper (name, wrapper)"} adds a new wrapper to
  1873   modify the existing (unsafe) step tactic.
  1874 
  1875   \item @{text "ctxt addbefore (name, tac)"} adds the given tactic as an
  1876   unsafe wrapper, such that it its result is concatenated
  1877   \emph{before} the result of each unsafe step.
  1878 
  1879   \item @{text "ctxt addafter (name, tac)"} adds the given tactic as an
  1880   unsafe wrapper, such that it its result is concatenated \emph{after}
  1881   the result of each unsafe step.
  1882 
  1883   \item @{text "ctxt delWrapper name"} deletes the unsafe wrapper with
  1884   the given name.
  1885 
  1886   \item @{text "addSss"} adds the simpset of the context to its
  1887   classical set. The assumptions and goal will be simplified, in a
  1888   rather safe way, after each safe step of the search.
  1889 
  1890   \item @{text "addss"} adds the simpset of the context to its
  1891   classical set. The assumptions and goal will be simplified, before
  1892   the each unsafe step of the search.
  1893 
  1894   \end{description}
  1895 *}
  1896 
  1897 
  1898 section {* Object-logic setup \label{sec:object-logic} *}
  1899 
  1900 text {*
  1901   \begin{matharray}{rcl}
  1902     @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\
  1903     @{method_def atomize} & : & @{text method} \\
  1904     @{attribute_def atomize} & : & @{text attribute} \\
  1905     @{attribute_def rule_format} & : & @{text attribute} \\
  1906     @{attribute_def rulify} & : & @{text attribute} \\
  1907   \end{matharray}
  1908 
  1909   The very starting point for any Isabelle object-logic is a ``truth
  1910   judgment'' that links object-level statements to the meta-logic
  1911   (with its minimal language of @{text prop} that covers universal
  1912   quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).
  1913 
  1914   Common object-logics are sufficiently expressive to internalize rule
  1915   statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own
  1916   language.  This is useful in certain situations where a rule needs
  1917   to be viewed as an atomic statement from the meta-level perspective,
  1918   e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.
  1919 
  1920   From the following language elements, only the @{method atomize}
  1921   method and @{attribute rule_format} attribute are occasionally
  1922   required by end-users, the rest is for those who need to setup their
  1923   own object-logic.  In the latter case existing formulations of
  1924   Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
  1925 
  1926   Generic tools may refer to the information provided by object-logic
  1927   declarations internally.
  1928 
  1929   @{rail "
  1930     @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}?
  1931     ;
  1932     @@{attribute atomize} ('(' 'full' ')')?
  1933     ;
  1934     @@{attribute rule_format} ('(' 'noasm' ')')?
  1935   "}
  1936 
  1937   \begin{description}
  1938   
  1939   \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant
  1940   @{text c} as the truth judgment of the current object-logic.  Its
  1941   type @{text \<sigma>} should specify a coercion of the category of
  1942   object-level propositions to @{text prop} of the Pure meta-logic;
  1943   the mixfix annotation @{text "(mx)"} would typically just link the
  1944   object language (internally of syntactic category @{text logic})
  1945   with that of @{text prop}.  Only one @{command "judgment"}
  1946   declaration may be given in any theory development.
  1947   
  1948   \item @{method atomize} (as a method) rewrites any non-atomic
  1949   premises of a sub-goal, using the meta-level equations declared via
  1950   @{attribute atomize} (as an attribute) beforehand.  As a result,
  1951   heavily nested goals become amenable to fundamental operations such
  1952   as resolution (cf.\ the @{method (Pure) rule} method).  Giving the ``@{text
  1953   "(full)"}'' option here means to turn the whole subgoal into an
  1954   object-statement (if possible), including the outermost parameters
  1955   and assumptions as well.
  1956 
  1957   A typical collection of @{attribute atomize} rules for a particular
  1958   object-logic would provide an internalization for each of the
  1959   connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.
  1960   Meta-level conjunction should be covered as well (this is
  1961   particularly important for locales, see \secref{sec:locale}).
  1962 
  1963   \item @{attribute rule_format} rewrites a theorem by the equalities
  1964   declared as @{attribute rulify} rules in the current object-logic.
  1965   By default, the result is fully normalized, including assumptions
  1966   and conclusions at any depth.  The @{text "(no_asm)"} option
  1967   restricts the transformation to the conclusion of a rule.
  1968 
  1969   In common object-logics (HOL, FOL, ZF), the effect of @{attribute
  1970   rule_format} is to replace (bounded) universal quantification
  1971   (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
  1972   rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.
  1973 
  1974   \end{description}
  1975 *}
  1976 
  1977 
  1978 section {* Tracing higher-order unification *}
  1979 
  1980 text {*
  1981   \begin{tabular}{rcll}
  1982     @{attribute_def unify_trace_simp} & : & @{text "attribute"} & default @{text "false"} \\
  1983     @{attribute_def unify_trace_types} & : & @{text "attribute"} & default @{text "false"} \\
  1984     @{attribute_def unify_trace_bound} & : & @{text "attribute"} & default @{text "50"} \\
  1985     @{attribute_def unify_search_bound} & : & @{text "attribute"} & default @{text "60"} \\
  1986   \end{tabular}
  1987   \medskip
  1988 
  1989   Higher-order unification works well in most practical situations,
  1990   but sometimes needs extra care to identify problems.  These tracing
  1991   options may help.
  1992 
  1993   \begin{description}
  1994 
  1995   \item @{attribute unify_trace_simp} controls tracing of the
  1996   simplification phase of higher-order unification.
  1997 
  1998   \item @{attribute unify_trace_types} controls warnings of
  1999   incompleteness, when unification is not considering all possible
  2000   instantiations of schematic type variables.
  2001 
  2002   \item @{attribute unify_trace_bound} determines the depth where
  2003   unification starts to print tracing information once it reaches
  2004   depth; 0 for full tracing.  At the default value, tracing
  2005   information is almost never printed in practice.
  2006 
  2007   \item @{attribute unify_search_bound} prevents unification from
  2008   searching past the given depth.  Because of this bound, higher-order
  2009   unification cannot return an infinite sequence, though it can return
  2010   an exponentially long one.  The search rarely approaches the default
  2011   value in practice.  If the search is cut off, unification prints a
  2012   warning ``Unification bound exceeded''.
  2013 
  2014   \end{description}
  2015 
  2016   \begin{warn}
  2017   Options for unification cannot be modified in a local context.  Only
  2018   the global theory content is taken into account.
  2019   \end{warn}
  2020 *}
  2021 
  2022 end