src/Doc/Isar_Ref/Generic.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 59785 4e6ab5831cc0
child 59853 4039d8aecda4
permissions -rw-r--r--
tuned signature;
     1 theory Generic
     2 imports Base Main
     3 begin
     4 
     5 chapter \<open>Generic tools and packages \label{ch:gen-tools}\<close>
     6 
     7 section \<open>Configuration options \label{sec:config}\<close>
     8 
     9 text \<open>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 \<close>
    20 
    21 declare [[show_main_goal = false]]
    22 
    23 notepad
    24 begin
    25   note [[show_main_goal = true]]
    26 end
    27 
    28 text \<open>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 \<open>
    38     @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?
    39   \<close>}
    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 \<close>
    53 
    54 
    55 section \<open>Basic proof tools\<close>
    56 
    57 subsection \<open>Miscellaneous methods and attributes \label{sec:misc-meth-att}\<close>
    58 
    59 text \<open>
    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 \<open>
    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   \<close>}
    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 no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
   136   \end{matharray}
   137 
   138   @{rail \<open>
   139     @@{attribute tagged} @{syntax name} @{syntax name}
   140     ;
   141     @@{attribute untagged} @{syntax name}
   142     ;
   143     @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref}
   144     ;
   145     (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
   146     ;
   147     @@{attribute rotated} @{syntax int}?
   148   \<close>}
   149 
   150   \begin{description}
   151 
   152   \item @{attribute tagged}~@{text "name value"} and @{attribute
   153   untagged}~@{text name} add and remove \emph{tags} of some theorem.
   154   Tags may be any list of string pairs that serve as formal comment.
   155   The first string is considered the tag name, the second its value.
   156   Note that @{attribute untagged} removes any tags of the same name.
   157 
   158   \item @{attribute THEN}~@{text a} composes rules by resolution; it
   159   resolves with the first premise of @{text a} (an alternative
   160   position may be also specified).  See also @{ML_op "RS"} in
   161   @{cite "isabelle-implementation"}.
   162   
   163   \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
   164   folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
   165   definitions throughout a rule.
   166 
   167   \item @{attribute abs_def} turns an equation of the form @{prop "f x
   168   y \<equiv> t"} into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method
   169   simp} or @{method unfold} steps always expand it.  This also works
   170   for object-logic equality.
   171 
   172   \item @{attribute rotated}~@{text n} rotate the premises of a
   173   theorem by @{text n} (default 1).
   174 
   175   \item @{attribute (Pure) elim_format} turns a destruction rule into
   176   elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
   177   (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
   178   
   179   Note that the Classical Reasoner (\secref{sec:classical}) provides
   180   its own version of this operation.
   181 
   182   \item @{attribute no_vars} replaces schematic variables by free
   183   ones; this is mainly for tuning output of pretty printed theorems.
   184 
   185   \end{description}
   186 \<close>
   187 
   188 
   189 subsection \<open>Low-level equational reasoning\<close>
   190 
   191 text \<open>
   192   \begin{matharray}{rcl}
   193     @{method_def subst} & : & @{text method} \\
   194     @{method_def hypsubst} & : & @{text method} \\
   195     @{method_def split} & : & @{text method} \\
   196   \end{matharray}
   197 
   198   @{rail \<open>
   199     @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thmref}
   200     ;
   201     @@{method split} @{syntax thmrefs}
   202   \<close>}
   203 
   204   These methods provide low-level facilities for equational reasoning
   205   that are intended for specialized applications only.  Normally,
   206   single step calculations would be performed in a structured text
   207   (see also \secref{sec:calculation}), while the Simplifier methods
   208   provide the canonical way for automated normalization (see
   209   \secref{sec:simplifier}).
   210 
   211   \begin{description}
   212 
   213   \item @{method subst}~@{text eq} performs a single substitution step
   214   using rule @{text eq}, which may be either a meta or object
   215   equality.
   216 
   217   \item @{method subst}~@{text "(asm) eq"} substitutes in an
   218   assumption.
   219 
   220   \item @{method subst}~@{text "(i \<dots> j) eq"} performs several
   221   substitutions in the conclusion. The numbers @{text i} to @{text j}
   222   indicate the positions to substitute at.  Positions are ordered from
   223   the top of the term tree moving down from left to right. For
   224   example, in @{text "(a + b) + (c + d)"} there are three positions
   225   where commutativity of @{text "+"} is applicable: 1 refers to @{text
   226   "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}.
   227 
   228   If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
   229   (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
   230   assume all substitutions are performed simultaneously.  Otherwise
   231   the behaviour of @{text subst} is not specified.
   232 
   233   \item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the
   234   substitutions in the assumptions. The positions refer to the
   235   assumptions in order from left to right.  For example, given in a
   236   goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of
   237   commutativity of @{text "+"} is the subterm @{text "a + b"} and
   238   position 2 is the subterm @{text "c + d"}.
   239 
   240   \item @{method hypsubst} performs substitution using some
   241   assumption; this only works for equations of the form @{text "x =
   242   t"} where @{text x} is a free or bound variable.
   243 
   244   \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
   245   splitting using the given rules.  Splitting is performed in the
   246   conclusion or some assumption of the subgoal, depending of the
   247   structure of the rule.
   248   
   249   Note that the @{method simp} method already involves repeated
   250   application of split rules as declared in the current context, using
   251   @{attribute split}, for example.
   252 
   253   \end{description}
   254 \<close>
   255 
   256 
   257 subsection \<open>Further tactic emulations \label{sec:tactics}\<close>
   258 
   259 text \<open>
   260   The following improper proof methods emulate traditional tactics.
   261   These admit direct access to the goal state, which is normally
   262   considered harmful!  In particular, this may involve both numbered
   263   goal addressing (default 1), and dynamic instantiation within the
   264   scope of some subgoal.
   265 
   266   \begin{warn}
   267     Dynamic instantiations refer to universally quantified parameters
   268     of a subgoal (the dynamic context) rather than fixed variables and
   269     term abbreviations of a (static) Isar context.
   270   \end{warn}
   271 
   272   Tactic emulation methods, unlike their ML counterparts, admit
   273   simultaneous instantiation from both dynamic and static contexts.
   274   If names occur in both contexts goal parameters hide locally fixed
   275   variables.  Likewise, schematic variables refer to term
   276   abbreviations, if present in the static context.  Otherwise the
   277   schematic variable is interpreted as a schematic variable and left
   278   to be solved by unification with certain parts of the subgoal.
   279 
   280   Note that the tactic emulation proof methods in Isabelle/Isar are
   281   consistently named @{text foo_tac}.  Note also that variable names
   282   occurring on left hand sides of instantiations must be preceded by a
   283   question mark if they coincide with a keyword or contain dots.  This
   284   is consistent with the attribute @{attribute "where"} (see
   285   \secref{sec:pure-meth-att}).
   286 
   287   \begin{matharray}{rcl}
   288     @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   289     @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   290     @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   291     @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   292     @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
   293     @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
   294     @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
   295     @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
   296     @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
   297     @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
   298     @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
   299   \end{matharray}
   300 
   301   @{rail \<open>
   302     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
   303       @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
   304     ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
   305     ;
   306     dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') @{syntax for_fixes}
   307     ;
   308     @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
   309     ;
   310     @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
   311     ;
   312     @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
   313     ;
   314     @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
   315     ;
   316     (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
   317   \<close>}
   318 
   319 \begin{description}
   320 
   321   \item @{method rule_tac} etc. do resolution of rules with explicit
   322   instantiation.  This works the same way as the ML tactics @{ML
   323   Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
   324 
   325   Multiple rules may be only given if there is no instantiation; then
   326   @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
   327   @{cite "isabelle-implementation"}).
   328 
   329   \item @{method cut_tac} inserts facts into the proof state as
   330   assumption of a subgoal; instantiations may be given as well.  Note
   331   that the scope of schematic variables is spread over the main goal
   332   statement and rule premises are turned into new subgoals.  This is
   333   in contrast to the regular method @{method insert} which inserts
   334   closed rule statements.
   335 
   336   \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
   337   from a subgoal.  Note that @{text \<phi>} may contain schematic
   338   variables, to abbreviate the intended proposition; the first
   339   matching subgoal premise will be deleted.  Removing useless premises
   340   from a subgoal increases its readability and can make search tactics
   341   run faster.
   342 
   343   \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
   344   @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
   345   as new subgoals (in the original context).
   346 
   347   \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
   348   goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
   349   \emph{suffix} of variables.
   350 
   351   \item @{method rotate_tac}~@{text n} rotates the premises of a
   352   subgoal by @{text n} positions: from right to left if @{text n} is
   353   positive, and from left to right if @{text n} is negative; the
   354   default value is 1.
   355 
   356   \item @{method tactic}~@{text "text"} produces a proof method from
   357   any ML text of type @{ML_type tactic}.  Apart from the usual ML
   358   environment and the current proof context, the ML code may refer to
   359   the locally bound values @{ML_text facts}, which indicates any
   360   current facts used for forward-chaining.
   361 
   362   \item @{method raw_tactic} is similar to @{method tactic}, but
   363   presents the goal state in its raw internal form, where simultaneous
   364   subgoals appear as conjunction of the logical framework instead of
   365   the usual split into several subgoals.  While feature this is useful
   366   for debugging of complex method definitions, it should not never
   367   appear in production theories.
   368 
   369   \end{description}
   370 \<close>
   371 
   372 
   373 section \<open>The Simplifier \label{sec:simplifier}\<close>
   374 
   375 text \<open>The Simplifier performs conditional and unconditional
   376   rewriting and uses contextual information: rule declarations in the
   377   background theory or local proof context are taken into account, as
   378   well as chained facts and subgoal premises (``local assumptions'').
   379   There are several general hooks that allow to modify the
   380   simplification strategy, or incorporate other proof tools that solve
   381   sub-problems, produce rewrite rules on demand etc.
   382 
   383   The rewriting strategy is always strictly bottom up, except for
   384   congruence rules, which are applied while descending into a term.
   385   Conditions in conditional rewrite rules are solved recursively
   386   before the rewrite rule is applied.
   387 
   388   The default Simplifier setup of major object logics (HOL, HOLCF,
   389   FOL, ZF) makes the Simplifier ready for immediate use, without
   390   engaging into the internal structures.  Thus it serves as
   391   general-purpose proof tool with the main focus on equational
   392   reasoning, and a bit more than that.
   393 \<close>
   394 
   395 
   396 subsection \<open>Simplification methods \label{sec:simp-meth}\<close>
   397 
   398 text \<open>
   399   \begin{tabular}{rcll}
   400     @{method_def simp} & : & @{text method} \\
   401     @{method_def simp_all} & : & @{text method} \\
   402     @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\
   403   \end{tabular}
   404   \medskip
   405 
   406   @{rail \<open>
   407     (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
   408     ;
   409 
   410     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
   411     ;
   412     @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |
   413       'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
   414   \<close>}
   415 
   416   \begin{description}
   417 
   418   \item @{method simp} invokes the Simplifier on the first subgoal,
   419   after inserting chained facts as additional goal premises; further
   420   rule declarations may be included via @{text "(simp add: facts)"}.
   421   The proof method fails if the subgoal remains unchanged after
   422   simplification.
   423 
   424   Note that the original goal premises and chained facts are subject
   425   to simplification themselves, while declarations via @{text
   426   "add"}/@{text "del"} merely follow the policies of the object-logic
   427   to extract rewrite rules from theorems, without further
   428   simplification.  This may lead to slightly different behavior in
   429   either case, which might be required precisely like that in some
   430   boundary situations to perform the intended simplification step!
   431 
   432   \medskip The @{text only} modifier first removes all other rewrite
   433   rules, looper tactics (including split rules), congruence rules, and
   434   then behaves like @{text add}.  Implicit solvers remain, which means
   435   that trivial rules like reflexivity or introduction of @{text
   436   "True"} are available to solve the simplified subgoals, but also
   437   non-trivial tools like linear arithmetic in HOL.  The latter may
   438   lead to some surprise of the meaning of ``only'' in Isabelle/HOL
   439   compared to English!
   440 
   441   \medskip The @{text split} modifiers add or delete rules for the
   442   Splitter (see also \secref{sec:simp-strategies} on the looper).
   443   This works only if the Simplifier method has been properly setup to
   444   include the Splitter (all major object logics such HOL, HOLCF, FOL,
   445   ZF do this already).
   446 
   447   There is also a separate @{method_ref split} method available for
   448   single-step case splitting.  The effect of repeatedly applying
   449   @{text "(split thms)"} can be imitated by ``@{text "(simp only:
   450   split: thms)"}''.
   451 
   452   \medskip The @{text cong} modifiers add or delete Simplifier
   453   congruence rules (see also \secref{sec:simp-rules}); the default is
   454   to add.
   455 
   456   \item @{method simp_all} is similar to @{method simp}, but acts on
   457   all goals, working backwards from the last to the first one as usual
   458   in Isabelle.\footnote{The order is irrelevant for goals without
   459   schematic variables, so simplification might actually be performed
   460   in parallel here.}
   461 
   462   Chained facts are inserted into all subgoals, before the
   463   simplification process starts.  Further rule declarations are the
   464   same as for @{method simp}.
   465 
   466   The proof method fails if all subgoals remain unchanged after
   467   simplification.
   468 
   469   \item @{attribute simp_depth_limit} limits the number of recursive
   470   invocations of the Simplifier during conditional rewriting.
   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{tabular}{|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{tabular}
   508   \end{center}
   509 \<close>
   510 
   511 
   512 subsubsection \<open>Examples\<close>
   513 
   514 text \<open>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 \<close>
   518 
   519 lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops
   520 
   521 text \<open>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:\<close>
   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 \<open>
   532   \medskip In many cases, assumptions of a subgoal are also needed in
   533   the simplification process.  For example:
   534 \<close>
   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 \<open>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 \<close>
   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 \<open>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 \<close>
   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 \<open>\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 \<close>
   590 
   591 lemma "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> Q"
   592   apply simp
   593   oops
   594 
   595 text \<open>See also \secref{sec:simp-trace} for options to enable
   596   Simplifier trace mode, which often helps to diagnose problems with
   597   rewrite systems.
   598 \<close>
   599 
   600 
   601 subsection \<open>Declaring rules \label{sec:simp-rules}\<close>
   602 
   603 text \<open>
   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 \<open>
   612     (@@{attribute simp} | @@{attribute split} | @@{attribute cong})
   613       (() | 'add' | 'del')
   614   \<close>}
   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 \<close>
   767 
   768 
   769 subsection \<open>Ordered rewriting with permutative rules\<close>
   770 
   771 text \<open>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.\<close>
   795 
   796 
   797 subsubsection \<open>Rewriting with AC operators\<close>
   798 
   799 text \<open>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 \<close>
   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 \<open>Thus the Simplifier is able to establish equalities with
   836   arbitrary permutations of subterms, by normalizing to a common
   837   standard form.  For example:\<close>
   838 
   839 lemma "(b \<bullet> c) \<bullet> a = xxx"
   840   apply (simp only: AC_rules)
   841   txt \<open>@{subgoals}\<close>
   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 \<open>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 \<close>
   855 
   856 
   857 subsubsection \<open>Re-orienting equalities\<close>
   858 
   859 text \<open>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.\<close>
   866 
   867 
   868 subsection \<open>Simplifier tracing and debugging \label{sec:simp-trace}\<close>
   869 
   870 text \<open>
   871   \begin{tabular}{rcll}
   872     @{attribute_def simp_trace} & : & @{text attribute} & default @{text false} \\
   873     @{attribute_def simp_trace_depth_limit} & : & @{text attribute} & default @{text 1} \\
   874     @{attribute_def simp_debug} & : & @{text attribute} & default @{text false} \\
   875     @{attribute_def simp_trace_new} & : & @{text attribute} \\
   876     @{attribute_def simp_break} & : & @{text attribute} \\
   877   \end{tabular}
   878   \medskip
   879 
   880   @{rail \<open>
   881     @@{attribute simp_trace_new} ('interactive')? \<newline>
   882       ('mode' '=' ('full' | 'normal'))? \<newline>
   883       ('depth' '=' @{syntax nat})?
   884     ;
   885 
   886     @@{attribute simp_break} (@{syntax term}*)
   887   \<close>}
   888 
   889   These attributes and configurations options control various aspects of
   890   Simplifier tracing and debugging.
   891 
   892   \begin{description}
   893 
   894   \item @{attribute simp_trace} makes the Simplifier output internal
   895   operations.  This includes rewrite steps, but also bookkeeping like
   896   modifications of the simpset.
   897 
   898   \item @{attribute simp_trace_depth_limit} limits the effect of
   899   @{attribute simp_trace} to the given depth of recursive Simplifier
   900   invocations (when solving conditions of rewrite rules).
   901 
   902   \item @{attribute simp_debug} makes the Simplifier output some extra
   903   information about internal operations.  This includes any attempted
   904   invocation of simplification procedures.
   905 
   906   \item @{attribute simp_trace_new} controls Simplifier tracing within
   907   Isabelle/PIDE applications, notably Isabelle/jEdit @{cite "isabelle-jedit"}.
   908   This provides a hierarchical representation of the rewriting steps
   909   performed by the Simplifier.
   910 
   911   Users can configure the behaviour by specifying breakpoints, verbosity and
   912   enabling or disabling the interactive mode. In normal verbosity (the
   913   default), only rule applications matching a breakpoint will be shown to
   914   the user. In full verbosity, all rule applications will be logged.
   915   Interactive mode interrupts the normal flow of the Simplifier and defers
   916   the decision how to continue to the user via some GUI dialog.
   917 
   918   \item @{attribute simp_break} declares term or theorem breakpoints for
   919   @{attribute simp_trace_new} as described above. Term breakpoints are
   920   patterns which are checked for matches on the redex of a rule application.
   921   Theorem breakpoints trigger when the corresponding theorem is applied in a
   922   rewrite step. For example:
   923 
   924   \end{description}
   925 \<close>
   926 
   927 declare conjI [simp_break]
   928 declare [[simp_break "?x \<and> ?y"]]
   929 
   930 
   931 subsection \<open>Simplification procedures \label{sec:simproc}\<close>
   932 
   933 text \<open>Simplification procedures are ML functions that produce proven
   934   rewrite rules on demand.  They are associated with higher-order
   935   patterns that approximate the left-hand sides of equations.  The
   936   Simplifier first matches the current redex against one of the LHS
   937   patterns; if this succeeds, the corresponding ML function is
   938   invoked, passing the Simplifier context and redex term.  Thus rules
   939   may be specifically fashioned for particular situations, resulting
   940   in a more powerful mechanism than term rewriting by a fixed set of
   941   rules.
   942 
   943   Any successful result needs to be a (possibly conditional) rewrite
   944   rule @{text "t \<equiv> u"} that is applicable to the current redex.  The
   945   rule will be applied just as any ordinary rewrite rule.  It is
   946   expected to be already in \emph{internal form}, bypassing the
   947   automatic preprocessing of object-level equivalences.
   948 
   949   \begin{matharray}{rcl}
   950     @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   951     simproc & : & @{text attribute} \\
   952   \end{matharray}
   953 
   954   @{rail \<open>
   955     @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
   956       @{syntax text} \<newline> (@'identifier' (@{syntax nameref}+))?
   957     ;
   958 
   959     @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
   960   \<close>}
   961 
   962   \begin{description}
   963 
   964   \item @{command "simproc_setup"} defines a named simplification
   965   procedure that is invoked by the Simplifier whenever any of the
   966   given term patterns match the current redex.  The implementation,
   967   which is provided as ML source text, needs to be of type @{ML_type
   968   "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type
   969   cterm} represents the current redex @{text r} and the result is
   970   supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a
   971   generalized version), or @{ML NONE} to indicate failure.  The
   972   @{ML_type simpset} argument holds the full context of the current
   973   Simplifier invocation, including the actual Isar proof context.  The
   974   @{ML_type morphism} informs about the difference of the original
   975   compilation context wrt.\ the one of the actual application later
   976   on.  The optional @{keyword "identifier"} specifies theorems that
   977   represent the logical content of the abstract theory of this
   978   simproc.
   979 
   980   Morphisms and identifiers are only relevant for simprocs that are
   981   defined within a local target context, e.g.\ in a locale.
   982 
   983   \item @{text "simproc add: name"} and @{text "simproc del: name"}
   984   add or delete named simprocs to the current Simplifier context.  The
   985   default is to add a simproc.  Note that @{command "simproc_setup"}
   986   already adds the new simproc to the subsequent context.
   987 
   988   \end{description}
   989 \<close>
   990 
   991 
   992 subsubsection \<open>Example\<close>
   993 
   994 text \<open>The following simplification procedure for @{thm
   995   [source=false, show_types] unit_eq} in HOL performs fine-grained
   996   control over rule application, beyond higher-order pattern matching.
   997   Declaring @{thm unit_eq} as @{attribute simp} directly would make
   998   the Simplifier loop!  Note that a version of this simplification
   999   procedure is already active in Isabelle/HOL.\<close>
  1000 
  1001 simproc_setup unit ("x::unit") =
  1002   \<open>fn _ => fn _ => fn ct =>
  1003     if HOLogic.is_unit (Thm.term_of ct) then NONE
  1004     else SOME (mk_meta_eq @{thm unit_eq})\<close>
  1005 
  1006 text \<open>Since the Simplifier applies simplification procedures
  1007   frequently, it is important to make the failure check in ML
  1008   reasonably fast.\<close>
  1009 
  1010 
  1011 subsection \<open>Configurable Simplifier strategies \label{sec:simp-strategies}\<close>
  1012 
  1013 text \<open>The core term-rewriting engine of the Simplifier is normally
  1014   used in combination with some add-on components that modify the
  1015   strategy and allow to integrate other non-Simplifier proof tools.
  1016   These may be reconfigured in ML as explained below.  Even if the
  1017   default strategies of object-logics like Isabelle/HOL are used
  1018   unchanged, it helps to understand how the standard Simplifier
  1019   strategies work.\<close>
  1020 
  1021 
  1022 subsubsection \<open>The subgoaler\<close>
  1023 
  1024 text \<open>
  1025   \begin{mldecls}
  1026   @{index_ML Simplifier.set_subgoaler: "(Proof.context -> int -> tactic) ->
  1027   Proof.context -> Proof.context"} \\
  1028   @{index_ML Simplifier.prems_of: "Proof.context -> thm list"} \\
  1029   \end{mldecls}
  1030 
  1031   The subgoaler is the tactic used to solve subgoals arising out of
  1032   conditional rewrite rules or congruence rules.  The default should
  1033   be simplification itself.  In rare situations, this strategy may
  1034   need to be changed.  For example, if the premise of a conditional
  1035   rule is an instance of its conclusion, as in @{text "Suc ?m < ?n \<Longrightarrow>
  1036   ?m < ?n"}, the default strategy could loop.  % FIXME !??
  1037 
  1038   \begin{description}
  1039 
  1040   \item @{ML Simplifier.set_subgoaler}~@{text "tac ctxt"} sets the
  1041   subgoaler of the context to @{text "tac"}.  The tactic will
  1042   be applied to the context of the running Simplifier instance.
  1043 
  1044   \item @{ML Simplifier.prems_of}~@{text "ctxt"} retrieves the current
  1045   set of premises from the context.  This may be non-empty only if
  1046   the Simplifier has been told to utilize local assumptions in the
  1047   first place (cf.\ the options in \secref{sec:simp-meth}).
  1048 
  1049   \end{description}
  1050 
  1051   As an example, consider the following alternative subgoaler:
  1052 \<close>
  1053 
  1054 ML \<open>
  1055   fun subgoaler_tac ctxt =
  1056     assume_tac ctxt ORELSE'
  1057     resolve_tac ctxt (Simplifier.prems_of ctxt) ORELSE'
  1058     asm_simp_tac ctxt
  1059 \<close>
  1060 
  1061 text \<open>This tactic first tries to solve the subgoal by assumption or
  1062   by resolving with with one of the premises, calling simplification
  1063   only if that fails.\<close>
  1064 
  1065 
  1066 subsubsection \<open>The solver\<close>
  1067 
  1068 text \<open>
  1069   \begin{mldecls}
  1070   @{index_ML_type solver} \\
  1071   @{index_ML Simplifier.mk_solver: "string ->
  1072   (Proof.context -> int -> tactic) -> solver"} \\
  1073   @{index_ML_op setSolver: "Proof.context * solver -> Proof.context"} \\
  1074   @{index_ML_op addSolver: "Proof.context * solver -> Proof.context"} \\
  1075   @{index_ML_op setSSolver: "Proof.context * solver -> Proof.context"} \\
  1076   @{index_ML_op addSSolver: "Proof.context * solver -> Proof.context"} \\
  1077   \end{mldecls}
  1078 
  1079   A solver is a tactic that attempts to solve a subgoal after
  1080   simplification.  Its core functionality is to prove trivial subgoals
  1081   such as @{prop "True"} and @{text "t = t"}, but object-logics might
  1082   be more ambitious.  For example, Isabelle/HOL performs a restricted
  1083   version of linear arithmetic here.
  1084 
  1085   Solvers are packaged up in abstract type @{ML_type solver}, with
  1086   @{ML Simplifier.mk_solver} as the only operation to create a solver.
  1087 
  1088   \medskip Rewriting does not instantiate unknowns.  For example,
  1089   rewriting alone cannot prove @{text "a \<in> ?A"} since this requires
  1090   instantiating @{text "?A"}.  The solver, however, is an arbitrary
  1091   tactic and may instantiate unknowns as it pleases.  This is the only
  1092   way the Simplifier can handle a conditional rewrite rule whose
  1093   condition contains extra variables.  When a simplification tactic is
  1094   to be combined with other provers, especially with the Classical
  1095   Reasoner, it is important whether it can be considered safe or not.
  1096   For this reason a simpset contains two solvers: safe and unsafe.
  1097 
  1098   The standard simplification strategy solely uses the unsafe solver,
  1099   which is appropriate in most cases.  For special applications where
  1100   the simplification process is not allowed to instantiate unknowns
  1101   within the goal, simplification starts with the safe solver, but may
  1102   still apply the ordinary unsafe one in nested simplifications for
  1103   conditional rules or congruences. Note that in this way the overall
  1104   tactic is not totally safe: it may instantiate unknowns that appear
  1105   also in other subgoals.
  1106 
  1107   \begin{description}
  1108 
  1109   \item @{ML Simplifier.mk_solver}~@{text "name tac"} turns @{text
  1110   "tac"} into a solver; the @{text "name"} is only attached as a
  1111   comment and has no further significance.
  1112 
  1113   \item @{text "ctxt setSSolver solver"} installs @{text "solver"} as
  1114   the safe solver of @{text "ctxt"}.
  1115 
  1116   \item @{text "ctxt addSSolver solver"} adds @{text "solver"} as an
  1117   additional safe solver; it will be tried after the solvers which had
  1118   already been present in @{text "ctxt"}.
  1119 
  1120   \item @{text "ctxt setSolver solver"} installs @{text "solver"} as the
  1121   unsafe solver of @{text "ctxt"}.
  1122 
  1123   \item @{text "ctxt addSolver solver"} adds @{text "solver"} as an
  1124   additional unsafe solver; it will be tried after the solvers which
  1125   had already been present in @{text "ctxt"}.
  1126 
  1127   \end{description}
  1128 
  1129   \medskip The solver tactic is invoked with the context of the
  1130   running Simplifier.  Further operations
  1131   may be used to retrieve relevant information, such as the list of
  1132   local Simplifier premises via @{ML Simplifier.prems_of} --- this
  1133   list may be non-empty only if the Simplifier runs in a mode that
  1134   utilizes local assumptions (see also \secref{sec:simp-meth}).  The
  1135   solver is also presented the full goal including its assumptions in
  1136   any case.  Thus it can use these (e.g.\ by calling @{ML
  1137   assume_tac}), even if the Simplifier proper happens to ignore local
  1138   premises at the moment.
  1139 
  1140   \medskip As explained before, the subgoaler is also used to solve
  1141   the premises of congruence rules.  These are usually of the form
  1142   @{text "s = ?x"}, where @{text "s"} needs to be simplified and
  1143   @{text "?x"} needs to be instantiated with the result.  Typically,
  1144   the subgoaler will invoke the Simplifier at some point, which will
  1145   eventually call the solver.  For this reason, solver tactics must be
  1146   prepared to solve goals of the form @{text "t = ?x"}, usually by
  1147   reflexivity.  In particular, reflexivity should be tried before any
  1148   of the fancy automated proof tools.
  1149 
  1150   It may even happen that due to simplification the subgoal is no
  1151   longer an equality.  For example, @{text "False \<longleftrightarrow> ?Q"} could be
  1152   rewritten to @{text "\<not> ?Q"}.  To cover this case, the solver could
  1153   try resolving with the theorem @{text "\<not> False"} of the
  1154   object-logic.
  1155 
  1156   \medskip
  1157 
  1158   \begin{warn}
  1159   If a premise of a congruence rule cannot be proved, then the
  1160   congruence is ignored.  This should only happen if the rule is
  1161   \emph{conditional} --- that is, contains premises not of the form
  1162   @{text "t = ?x"}.  Otherwise it indicates that some congruence rule,
  1163   or possibly the subgoaler or solver, is faulty.
  1164   \end{warn}
  1165 \<close>
  1166 
  1167 
  1168 subsubsection \<open>The looper\<close>
  1169 
  1170 text \<open>
  1171   \begin{mldecls}
  1172   @{index_ML_op setloop: "Proof.context *
  1173   (Proof.context -> int -> tactic) -> Proof.context"} \\
  1174   @{index_ML_op addloop: "Proof.context *
  1175   (string * (Proof.context -> int -> tactic))
  1176   -> Proof.context"} \\
  1177   @{index_ML_op delloop: "Proof.context * string -> Proof.context"} \\
  1178   @{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
  1179   @{index_ML Splitter.del_split: "thm -> Proof.context -> Proof.context"} \\
  1180   \end{mldecls}
  1181 
  1182   The looper is a list of tactics that are applied after
  1183   simplification, in case the solver failed to solve the simplified
  1184   goal.  If the looper succeeds, the simplification process is started
  1185   all over again.  Each of the subgoals generated by the looper is
  1186   attacked in turn, in reverse order.
  1187 
  1188   A typical looper is \emph{case splitting}: the expansion of a
  1189   conditional.  Another possibility is to apply an elimination rule on
  1190   the assumptions.  More adventurous loopers could start an induction.
  1191 
  1192   \begin{description}
  1193 
  1194   \item @{text "ctxt setloop tac"} installs @{text "tac"} as the only
  1195   looper tactic of @{text "ctxt"}.
  1196 
  1197   \item @{text "ctxt addloop (name, tac)"} adds @{text "tac"} as an
  1198   additional looper tactic with name @{text "name"}, which is
  1199   significant for managing the collection of loopers.  The tactic will
  1200   be tried after the looper tactics that had already been present in
  1201   @{text "ctxt"}.
  1202 
  1203   \item @{text "ctxt delloop name"} deletes the looper tactic that was
  1204   associated with @{text "name"} from @{text "ctxt"}.
  1205 
  1206   \item @{ML Splitter.add_split}~@{text "thm ctxt"} adds split tactics
  1207   for @{text "thm"} as additional looper tactics of @{text "ctxt"}.
  1208 
  1209   \item @{ML Splitter.del_split}~@{text "thm ctxt"} deletes the split
  1210   tactic corresponding to @{text thm} from the looper tactics of
  1211   @{text "ctxt"}.
  1212 
  1213   \end{description}
  1214 
  1215   The splitter replaces applications of a given function; the
  1216   right-hand side of the replacement can be anything.  For example,
  1217   here is a splitting rule for conditional expressions:
  1218 
  1219   @{text [display] "?P (if ?Q ?x ?y) \<longleftrightarrow> (?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y)"}
  1220 
  1221   Another example is the elimination operator for Cartesian products
  1222   (which happens to be called @{text split} in Isabelle/HOL:
  1223 
  1224   @{text [display] "?P (split ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"}
  1225 
  1226   For technical reasons, there is a distinction between case splitting
  1227   in the conclusion and in the premises of a subgoal.  The former is
  1228   done by @{ML Splitter.split_tac} with rules like @{thm [source]
  1229   split_if} or @{thm [source] option.split}, which do not split the
  1230   subgoal, while the latter is done by @{ML Splitter.split_asm_tac}
  1231   with rules like @{thm [source] split_if_asm} or @{thm [source]
  1232   option.split_asm}, which split the subgoal.  The function @{ML
  1233   Splitter.add_split} automatically takes care of which tactic to
  1234   call, analyzing the form of the rules given as argument; it is the
  1235   same operation behind @{text "split"} attribute or method modifier
  1236   syntax in the Isar source language.
  1237 
  1238   Case splits should be allowed only when necessary; they are
  1239   expensive and hard to control.  Case-splitting on if-expressions in
  1240   the conclusion is usually beneficial, so it is enabled by default in
  1241   Isabelle/HOL and Isabelle/FOL/ZF.
  1242 
  1243   \begin{warn}
  1244   With @{ML Splitter.split_asm_tac} as looper component, the
  1245   Simplifier may split subgoals!  This might cause unexpected problems
  1246   in tactic expressions that silently assume 0 or 1 subgoals after
  1247   simplification.
  1248   \end{warn}
  1249 \<close>
  1250 
  1251 
  1252 subsection \<open>Forward simplification \label{sec:simp-forward}\<close>
  1253 
  1254 text \<open>
  1255   \begin{matharray}{rcl}
  1256     @{attribute_def simplified} & : & @{text attribute} \\
  1257   \end{matharray}
  1258 
  1259   @{rail \<open>
  1260     @@{attribute simplified} opt? @{syntax thmrefs}?
  1261     ;
  1262 
  1263     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
  1264   \<close>}
  1265 
  1266   \begin{description}
  1267   
  1268   \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to
  1269   be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,
  1270   a\<^sub>n"}, or the implicit Simplifier context if no arguments are given.
  1271   The result is fully simplified by default, including assumptions and
  1272   conclusion; the options @{text no_asm} etc.\ tune the Simplifier in
  1273   the same way as the for the @{text simp} method.
  1274 
  1275   Note that forward simplification restricts the Simplifier to its
  1276   most basic operation of term rewriting; solver and looper tactics
  1277   (\secref{sec:simp-strategies}) are \emph{not} involved here.  The
  1278   @{attribute simplified} attribute should be only rarely required
  1279   under normal circumstances.
  1280 
  1281   \end{description}
  1282 \<close>
  1283 
  1284 
  1285 section \<open>The Classical Reasoner \label{sec:classical}\<close>
  1286 
  1287 subsection \<open>Basic concepts\<close>
  1288 
  1289 text \<open>Although Isabelle is generic, many users will be working in
  1290   some extension of classical first-order logic.  Isabelle/ZF is built
  1291   upon theory FOL, while Isabelle/HOL conceptually contains
  1292   first-order logic as a fragment.  Theorem-proving in predicate logic
  1293   is undecidable, but many automated strategies have been developed to
  1294   assist in this task.
  1295 
  1296   Isabelle's classical reasoner is a generic package that accepts
  1297   certain information about a logic and delivers a suite of automatic
  1298   proof tools, based on rules that are classified and declared in the
  1299   context.  These proof procedures are slow and simplistic compared
  1300   with high-end automated theorem provers, but they can save
  1301   considerable time and effort in practice.  They can prove theorems
  1302   such as Pelletier's @{cite pelletier86} problems 40 and 41 in a few
  1303   milliseconds (including full proof reconstruction):\<close>
  1304 
  1305 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)"
  1306   by blast
  1307 
  1308 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)"
  1309   by blast
  1310 
  1311 text \<open>The proof tools are generic.  They are not restricted to
  1312   first-order logic, and have been heavily used in the development of
  1313   the Isabelle/HOL library and applications.  The tactics can be
  1314   traced, and their components can be called directly; in this manner,
  1315   any proof can be viewed interactively.\<close>
  1316 
  1317 
  1318 subsubsection \<open>The sequent calculus\<close>
  1319 
  1320 text \<open>Isabelle supports natural deduction, which is easy to use for
  1321   interactive proof.  But natural deduction does not easily lend
  1322   itself to automation, and has a bias towards intuitionism.  For
  1323   certain proofs in classical logic, it can not be called natural.
  1324   The \emph{sequent calculus}, a generalization of natural deduction,
  1325   is easier to automate.
  1326 
  1327   A \textbf{sequent} has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"}
  1328   and @{text "\<Delta>"} are sets of formulae.\footnote{For first-order
  1329   logic, sequents can equivalently be made from lists or multisets of
  1330   formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is
  1331   \textbf{valid} if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or>
  1332   Q\<^sub>n"}.  Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which
  1333   is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals.  A
  1334   sequent is \textbf{basic} if its left and right sides have a common
  1335   formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially
  1336   valid.
  1337 
  1338   Sequent rules are classified as \textbf{right} or \textbf{left},
  1339   indicating which side of the @{text "\<turnstile>"} symbol they operate on.
  1340   Rules that operate on the right side are analogous to natural
  1341   deduction's introduction rules, and left rules are analogous to
  1342   elimination rules.  The sequent calculus analogue of @{text "(\<longrightarrow>I)"}
  1343   is the rule
  1344   \[
  1345   \infer[@{text "(\<longrightarrow>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<longrightarrow> Q"}}{@{text "P, \<Gamma> \<turnstile> \<Delta>, Q"}}
  1346   \]
  1347   Applying the rule backwards, this breaks down some implication on
  1348   the right side of a sequent; @{text "\<Gamma>"} and @{text "\<Delta>"} stand for
  1349   the sets of formulae that are unaffected by the inference.  The
  1350   analogue of the pair @{text "(\<or>I1)"} and @{text "(\<or>I2)"} is the
  1351   single rule
  1352   \[
  1353   \infer[@{text "(\<or>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<or> Q"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P, Q"}}
  1354   \]
  1355   This breaks down some disjunction on the right side, replacing it by
  1356   both disjuncts.  Thus, the sequent calculus is a kind of
  1357   multiple-conclusion logic.
  1358 
  1359   To illustrate the use of multiple formulae on the right, let us
  1360   prove the classical theorem @{text "(P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}.  Working
  1361   backwards, we reduce this formula to a basic sequent:
  1362   \[
  1363   \infer[@{text "(\<or>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}}
  1364     {\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q), (Q \<longrightarrow> P)"}}
  1365       {\infer[@{text "(\<longrightarrow>R)"}]{@{text "P \<turnstile> Q, (Q \<longrightarrow> P)"}}
  1366         {@{text "P, Q \<turnstile> Q, P"}}}}
  1367   \]
  1368 
  1369   This example is typical of the sequent calculus: start with the
  1370   desired theorem and apply rules backwards in a fairly arbitrary
  1371   manner.  This yields a surprisingly effective proof procedure.
  1372   Quantifiers add only few complications, since Isabelle handles
  1373   parameters and schematic variables.  See @{cite \<open>Chapter 10\<close>
  1374   "paulson-ml2"} for further discussion.\<close>
  1375 
  1376 
  1377 subsubsection \<open>Simulating sequents by natural deduction\<close>
  1378 
  1379 text \<open>Isabelle can represent sequents directly, as in the
  1380   object-logic LK.  But natural deduction is easier to work with, and
  1381   most object-logics employ it.  Fortunately, we can simulate the
  1382   sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} by the Isabelle formula
  1383   @{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
  1384   the assumptions and the choice of @{text "Q\<^sub>1"} are arbitrary.
  1385   Elim-resolution plays a key role in simulating sequent proofs.
  1386 
  1387   We can easily handle reasoning on the left.  Elim-resolution with
  1388   the rules @{text "(\<or>E)"}, @{text "(\<bottom>E)"} and @{text "(\<exists>E)"} achieves
  1389   a similar effect as the corresponding sequent rules.  For the other
  1390   connectives, we use sequent-style elimination rules instead of
  1391   destruction rules such as @{text "(\<and>E1, 2)"} and @{text "(\<forall>E)"}.
  1392   But note that the rule @{text "(\<not>L)"} has no effect under our
  1393   representation of sequents!
  1394   \[
  1395   \infer[@{text "(\<not>L)"}]{@{text "\<not> P, \<Gamma> \<turnstile> \<Delta>"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P"}}
  1396   \]
  1397 
  1398   What about reasoning on the right?  Introduction rules can only
  1399   affect the formula in the conclusion, namely @{text "Q\<^sub>1"}.  The
  1400   other right-side formulae are represented as negated assumptions,
  1401   @{text "\<not> Q\<^sub>2, \<dots>, \<not> Q\<^sub>n"}.  In order to operate on one of these, it
  1402   must first be exchanged with @{text "Q\<^sub>1"}.  Elim-resolution with the
  1403   @{text swap} rule has this effect: @{text "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"}
  1404 
  1405   To ensure that swaps occur only when necessary, each introduction
  1406   rule is converted into a swapped form: it is resolved with the
  1407   second premise of @{text "(swap)"}.  The swapped form of @{text
  1408   "(\<and>I)"}, which might be called @{text "(\<not>\<and>E)"}, is
  1409   @{text [display] "\<not> (P \<and> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (\<not> R \<Longrightarrow> Q) \<Longrightarrow> R"}
  1410 
  1411   Similarly, the swapped form of @{text "(\<longrightarrow>I)"} is
  1412   @{text [display] "\<not> (P \<longrightarrow> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P \<Longrightarrow> Q) \<Longrightarrow> R"}
  1413 
  1414   Swapped introduction rules are applied using elim-resolution, which
  1415   deletes the negated formula.  Our representation of sequents also
  1416   requires the use of ordinary introduction rules.  If we had no
  1417   regard for readability of intermediate goal states, we could treat
  1418   the right side more uniformly by representing sequents as @{text
  1419   [display] "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> \<bottom>"}
  1420 \<close>
  1421 
  1422 
  1423 subsubsection \<open>Extra rules for the sequent calculus\<close>
  1424 
  1425 text \<open>As mentioned, destruction rules such as @{text "(\<and>E1, 2)"} and
  1426   @{text "(\<forall>E)"} must be replaced by sequent-style elimination rules.
  1427   In addition, we need rules to embody the classical equivalence
  1428   between @{text "P \<longrightarrow> Q"} and @{text "\<not> P \<or> Q"}.  The introduction
  1429   rules @{text "(\<or>I1, 2)"} are replaced by a rule that simulates
  1430   @{text "(\<or>R)"}: @{text [display] "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"}
  1431 
  1432   The destruction rule @{text "(\<longrightarrow>E)"} is replaced by @{text [display]
  1433   "(P \<longrightarrow> Q) \<Longrightarrow> (\<not> P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"}
  1434 
  1435   Quantifier replication also requires special rules.  In classical
  1436   logic, @{text "\<exists>x. P x"} is equivalent to @{text "\<not> (\<forall>x. \<not> P x)"};
  1437   the rules @{text "(\<exists>R)"} and @{text "(\<forall>L)"} are dual:
  1438   \[
  1439   \infer[@{text "(\<exists>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x"}}{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x, P t"}}
  1440   \qquad
  1441   \infer[@{text "(\<forall>L)"}]{@{text "\<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}{@{text "P t, \<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}
  1442   \]
  1443   Thus both kinds of quantifier may be replicated.  Theorems requiring
  1444   multiple uses of a universal formula are easy to invent; consider
  1445   @{text [display] "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P a \<longrightarrow> P (f\<^sup>n a)"} for any
  1446   @{text "n > 1"}.  Natural examples of the multiple use of an
  1447   existential formula are rare; a standard one is @{text "\<exists>x. \<forall>y. P x
  1448   \<longrightarrow> P y"}.
  1449 
  1450   Forgoing quantifier replication loses completeness, but gains
  1451   decidability, since the search space becomes finite.  Many useful
  1452   theorems can be proved without replication, and the search generally
  1453   delivers its verdict in a reasonable time.  To adopt this approach,
  1454   represent the sequent rules @{text "(\<exists>R)"}, @{text "(\<exists>L)"} and
  1455   @{text "(\<forall>R)"} by @{text "(\<exists>I)"}, @{text "(\<exists>E)"} and @{text "(\<forall>I)"},
  1456   respectively, and put @{text "(\<forall>E)"} into elimination form: @{text
  1457   [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"}
  1458 
  1459   Elim-resolution with this rule will delete the universal formula
  1460   after a single use.  To replicate universal quantifiers, replace the
  1461   rule by @{text [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"}
  1462 
  1463   To replicate existential quantifiers, replace @{text "(\<exists>I)"} by
  1464   @{text [display] "(\<not> (\<exists>x. P x) \<Longrightarrow> P t) \<Longrightarrow> \<exists>x. P x"}
  1465 
  1466   All introduction rules mentioned above are also useful in swapped
  1467   form.
  1468 
  1469   Replication makes the search space infinite; we must apply the rules
  1470   with care.  The classical reasoner distinguishes between safe and
  1471   unsafe rules, applying the latter only when there is no alternative.
  1472   Depth-first search may well go down a blind alley; best-first search
  1473   is better behaved in an infinite search space.  However, quantifier
  1474   replication is too expensive to prove any but the simplest theorems.
  1475 \<close>
  1476 
  1477 
  1478 subsection \<open>Rule declarations\<close>
  1479 
  1480 text \<open>The proof tools of the Classical Reasoner depend on
  1481   collections of rules declared in the context, which are classified
  1482   as introduction, elimination or destruction and as \emph{safe} or
  1483   \emph{unsafe}.  In general, safe rules can be attempted blindly,
  1484   while unsafe rules must be used with care.  A safe rule must never
  1485   reduce a provable goal to an unprovable set of subgoals.
  1486 
  1487   The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P
  1488   \<or> Q"} to @{text "P"}, which might turn out as premature choice of an
  1489   unprovable subgoal.  Any rule is unsafe whose premises contain new
  1490   unknowns.  The elimination rule @{text "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} is
  1491   unsafe, since it is applied via elim-resolution, which discards the
  1492   assumption @{text "\<forall>x. P x"} and replaces it by the weaker
  1493   assumption @{text "P t"}.  The rule @{text "P t \<Longrightarrow> \<exists>x. P x"} is
  1494   unsafe for similar reasons.  The quantifier duplication rule @{text
  1495   "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} is unsafe in a different sense:
  1496   since it keeps the assumption @{text "\<forall>x. P x"}, it is prone to
  1497   looping.  In classical first-order logic, all rules are safe except
  1498   those mentioned above.
  1499 
  1500   The safe~/ unsafe distinction is vague, and may be regarded merely
  1501   as a way of giving some rules priority over others.  One could argue
  1502   that @{text "(\<or>E)"} is unsafe, because repeated application of it
  1503   could generate exponentially many subgoals.  Induction rules are
  1504   unsafe because inductive proofs are difficult to set up
  1505   automatically.  Any inference is unsafe that instantiates an unknown
  1506   in the proof state --- thus matching must be used, rather than
  1507   unification.  Even proof by assumption is unsafe if it instantiates
  1508   unknowns shared with other subgoals.
  1509 
  1510   \begin{matharray}{rcl}
  1511     @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
  1512     @{attribute_def intro} & : & @{text attribute} \\
  1513     @{attribute_def elim} & : & @{text attribute} \\
  1514     @{attribute_def dest} & : & @{text attribute} \\
  1515     @{attribute_def rule} & : & @{text attribute} \\
  1516     @{attribute_def iff} & : & @{text attribute} \\
  1517     @{attribute_def swapped} & : & @{text attribute} \\
  1518   \end{matharray}
  1519 
  1520   @{rail \<open>
  1521     (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
  1522     ;
  1523     @@{attribute rule} 'del'
  1524     ;
  1525     @@{attribute iff} (((() | 'add') '?'?) | 'del')
  1526   \<close>}
  1527 
  1528   \begin{description}
  1529 
  1530   \item @{command "print_claset"} prints the collection of rules
  1531   declared to the Classical Reasoner, i.e.\ the @{ML_type claset}
  1532   within the context.
  1533 
  1534   \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
  1535   declare introduction, elimination, and destruction rules,
  1536   respectively.  By default, rules are considered as \emph{unsafe}
  1537   (i.e.\ not applied blindly without backtracking), while ``@{text
  1538   "!"}'' classifies as \emph{safe}.  Rule declarations marked by
  1539   ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
  1540   \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
  1541   of the @{method rule} method).  The optional natural number
  1542   specifies an explicit weight argument, which is ignored by the
  1543   automated reasoning tools, but determines the search order of single
  1544   rule steps.
  1545 
  1546   Introduction rules are those that can be applied using ordinary
  1547   resolution.  Their swapped forms are generated internally, which
  1548   will be applied using elim-resolution.  Elimination rules are
  1549   applied using elim-resolution.  Rules are sorted by the number of
  1550   new subgoals they will yield; rules that generate the fewest
  1551   subgoals will be tried first.  Otherwise, later declarations take
  1552   precedence over earlier ones.
  1553 
  1554   Rules already present in the context with the same classification
  1555   are ignored.  A warning is printed if the rule has already been
  1556   added with some other classification, but the rule is added anyway
  1557   as requested.
  1558 
  1559   \item @{attribute rule}~@{text del} deletes all occurrences of a
  1560   rule from the classical context, regardless of its classification as
  1561   introduction~/ elimination~/ destruction and safe~/ unsafe.
  1562 
  1563   \item @{attribute iff} declares logical equivalences to the
  1564   Simplifier and the Classical reasoner at the same time.
  1565   Non-conditional rules result in a safe introduction and elimination
  1566   pair; conditional ones are considered unsafe.  Rules with negative
  1567   conclusion are automatically inverted (using @{text "\<not>"}-elimination
  1568   internally).
  1569 
  1570   The ``@{text "?"}'' version of @{attribute iff} declares rules to
  1571   the Isabelle/Pure context only, and omits the Simplifier
  1572   declaration.
  1573 
  1574   \item @{attribute swapped} turns an introduction rule into an
  1575   elimination, by resolving with the classical swap principle @{text
  1576   "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position.  This is mainly for
  1577   illustrative purposes: the Classical Reasoner already swaps rules
  1578   internally as explained above.
  1579 
  1580   \end{description}
  1581 \<close>
  1582 
  1583 
  1584 subsection \<open>Structured methods\<close>
  1585 
  1586 text \<open>
  1587   \begin{matharray}{rcl}
  1588     @{method_def rule} & : & @{text method} \\
  1589     @{method_def contradiction} & : & @{text method} \\
  1590   \end{matharray}
  1591 
  1592   @{rail \<open>
  1593     @@{method rule} @{syntax thmrefs}?
  1594   \<close>}
  1595 
  1596   \begin{description}
  1597 
  1598   \item @{method rule} as offered by the Classical Reasoner is a
  1599   refinement over the Pure one (see \secref{sec:pure-meth-att}).  Both
  1600   versions work the same, but the classical version observes the
  1601   classical rule context in addition to that of Isabelle/Pure.
  1602 
  1603   Common object logics (HOL, ZF, etc.) declare a rich collection of
  1604   classical rules (even if these would qualify as intuitionistic
  1605   ones), but only few declarations to the rule context of
  1606   Isabelle/Pure (\secref{sec:pure-meth-att}).
  1607 
  1608   \item @{method contradiction} solves some goal by contradiction,
  1609   deriving any result from both @{text "\<not> A"} and @{text A}.  Chained
  1610   facts, which are guaranteed to participate, may appear in either
  1611   order.
  1612 
  1613   \end{description}
  1614 \<close>
  1615 
  1616 
  1617 subsection \<open>Fully automated methods\<close>
  1618 
  1619 text \<open>
  1620   \begin{matharray}{rcl}
  1621     @{method_def blast} & : & @{text method} \\
  1622     @{method_def auto} & : & @{text method} \\
  1623     @{method_def force} & : & @{text method} \\
  1624     @{method_def fast} & : & @{text method} \\
  1625     @{method_def slow} & : & @{text method} \\
  1626     @{method_def best} & : & @{text method} \\
  1627     @{method_def fastforce} & : & @{text method} \\
  1628     @{method_def slowsimp} & : & @{text method} \\
  1629     @{method_def bestsimp} & : & @{text method} \\
  1630     @{method_def deepen} & : & @{text method} \\
  1631   \end{matharray}
  1632 
  1633   @{rail \<open>
  1634     @@{method blast} @{syntax nat}? (@{syntax clamod} * )
  1635     ;
  1636     @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )
  1637     ;
  1638     @@{method force} (@{syntax clasimpmod} * )
  1639     ;
  1640     (@@{method fast} | @@{method slow} | @@{method best}) (@{syntax clamod} * )
  1641     ;
  1642     (@@{method fastforce} | @@{method slowsimp} | @@{method bestsimp})
  1643       (@{syntax clasimpmod} * )
  1644     ;
  1645     @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
  1646     ;
  1647     @{syntax_def clamod}:
  1648       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
  1649     ;
  1650     @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
  1651       ('cong' | 'split') (() | 'add' | 'del') |
  1652       'iff' (((() | 'add') '?'?) | 'del') |
  1653       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
  1654   \<close>}
  1655 
  1656   \begin{description}
  1657 
  1658   \item @{method blast} is a separate classical tableau prover that
  1659   uses the same classical rule declarations as explained before.
  1660 
  1661   Proof search is coded directly in ML using special data structures.
  1662   A successful proof is then reconstructed using regular Isabelle
  1663   inferences.  It is faster and more powerful than the other classical
  1664   reasoning tools, but has major limitations too.
  1665 
  1666   \begin{itemize}
  1667 
  1668   \item It does not use the classical wrapper tacticals, such as the
  1669   integration with the Simplifier of @{method fastforce}.
  1670 
  1671   \item It does not perform higher-order unification, as needed by the
  1672   rule @{thm [source=false] rangeI} in HOL.  There are often
  1673   alternatives to such rules, for example @{thm [source=false]
  1674   range_eqI}.
  1675 
  1676   \item Function variables may only be applied to parameters of the
  1677   subgoal.  (This restriction arises because the prover does not use
  1678   higher-order unification.)  If other function variables are present
  1679   then the prover will fail with the message \texttt{Function Var's
  1680   argument not a bound variable}.
  1681 
  1682   \item Its proof strategy is more general than @{method fast} but can
  1683   be slower.  If @{method blast} fails or seems to be running forever,
  1684   try @{method fast} and the other proof tools described below.
  1685 
  1686   \end{itemize}
  1687 
  1688   The optional integer argument specifies a bound for the number of
  1689   unsafe steps used in a proof.  By default, @{method blast} starts
  1690   with a bound of 0 and increases it successively to 20.  In contrast,
  1691   @{text "(blast lim)"} tries to prove the goal using a search bound
  1692   of @{text "lim"}.  Sometimes a slow proof using @{method blast} can
  1693   be made much faster by supplying the successful search bound to this
  1694   proof method instead.
  1695 
  1696   \item @{method auto} combines classical reasoning with
  1697   simplification.  It is intended for situations where there are a lot
  1698   of mostly trivial subgoals; it proves all the easy ones, leaving the
  1699   ones it cannot prove.  Occasionally, attempting to prove the hard
  1700   ones may take a long time.
  1701 
  1702   The optional depth arguments in @{text "(auto m n)"} refer to its
  1703   builtin classical reasoning procedures: @{text m} (default 4) is for
  1704   @{method blast}, which is tried first, and @{text n} (default 2) is
  1705   for a slower but more general alternative that also takes wrappers
  1706   into account.
  1707 
  1708   \item @{method force} is intended to prove the first subgoal
  1709   completely, using many fancy proof tools and performing a rather
  1710   exhaustive search.  As a result, proof attempts may take rather long
  1711   or diverge easily.
  1712 
  1713   \item @{method fast}, @{method best}, @{method slow} attempt to
  1714   prove the first subgoal using sequent-style reasoning as explained
  1715   before.  Unlike @{method blast}, they construct proofs directly in
  1716   Isabelle.
  1717 
  1718   There is a difference in search strategy and back-tracking: @{method
  1719   fast} uses depth-first search and @{method best} uses best-first
  1720   search (guided by a heuristic function: normally the total size of
  1721   the proof state).
  1722 
  1723   Method @{method slow} is like @{method fast}, but conducts a broader
  1724   search: it may, when backtracking from a failed proof attempt, undo
  1725   even the step of proving a subgoal by assumption.
  1726 
  1727   \item @{method fastforce}, @{method slowsimp}, @{method bestsimp}
  1728   are like @{method fast}, @{method slow}, @{method best},
  1729   respectively, but use the Simplifier as additional wrapper. The name
  1730   @{method fastforce}, reflects the behaviour of this popular method
  1731   better without requiring an understanding of its implementation.
  1732 
  1733   \item @{method deepen} works by exhaustive search up to a certain
  1734   depth.  The start depth is 4 (unless specified explicitly), and the
  1735   depth is increased iteratively up to 10.  Unsafe rules are modified
  1736   to preserve the formula they act on, so that it be used repeatedly.
  1737   This method can prove more goals than @{method fast}, but is much
  1738   slower, for example if the assumptions have many universal
  1739   quantifiers.
  1740 
  1741   \end{description}
  1742 
  1743   Any of the above methods support additional modifiers of the context
  1744   of classical (and simplifier) rules, but the ones related to the
  1745   Simplifier are explicitly prefixed by @{text simp} here.  The
  1746   semantics of these ad-hoc rule declarations is analogous to the
  1747   attributes given before.  Facts provided by forward chaining are
  1748   inserted into the goal before commencing proof search.
  1749 \<close>
  1750 
  1751 
  1752 subsection \<open>Partially automated methods\<close>
  1753 
  1754 text \<open>These proof methods may help in situations when the
  1755   fully-automated tools fail.  The result is a simpler subgoal that
  1756   can be tackled by other means, such as by manual instantiation of
  1757   quantifiers.
  1758 
  1759   \begin{matharray}{rcl}
  1760     @{method_def safe} & : & @{text method} \\
  1761     @{method_def clarify} & : & @{text method} \\
  1762     @{method_def clarsimp} & : & @{text method} \\
  1763   \end{matharray}
  1764 
  1765   @{rail \<open>
  1766     (@@{method safe} | @@{method clarify}) (@{syntax clamod} * )
  1767     ;
  1768     @@{method clarsimp} (@{syntax clasimpmod} * )
  1769   \<close>}
  1770 
  1771   \begin{description}
  1772 
  1773   \item @{method safe} repeatedly performs safe steps on all subgoals.
  1774   It is deterministic, with at most one outcome.
  1775 
  1776   \item @{method clarify} performs a series of safe steps without
  1777   splitting subgoals; see also @{method clarify_step}.
  1778 
  1779   \item @{method clarsimp} acts like @{method clarify}, but also does
  1780   simplification.  Note that if the Simplifier context includes a
  1781   splitter for the premises, the subgoal may still be split.
  1782 
  1783   \end{description}
  1784 \<close>
  1785 
  1786 
  1787 subsection \<open>Single-step tactics\<close>
  1788 
  1789 text \<open>
  1790   \begin{matharray}{rcl}
  1791     @{method_def safe_step} & : & @{text method} \\
  1792     @{method_def inst_step} & : & @{text method} \\
  1793     @{method_def step} & : & @{text method} \\
  1794     @{method_def slow_step} & : & @{text method} \\
  1795     @{method_def clarify_step} & : &  @{text method} \\
  1796   \end{matharray}
  1797 
  1798   These are the primitive tactics behind the automated proof methods
  1799   of the Classical Reasoner.  By calling them yourself, you can
  1800   execute these procedures one step at a time.
  1801 
  1802   \begin{description}
  1803 
  1804   \item @{method safe_step} performs a safe step on the first subgoal.
  1805   The safe wrapper tacticals are applied to a tactic that may include
  1806   proof by assumption or Modus Ponens (taking care not to instantiate
  1807   unknowns), or substitution.
  1808 
  1809   \item @{method inst_step} is like @{method safe_step}, but allows
  1810   unknowns to be instantiated.
  1811 
  1812   \item @{method step} is the basic step of the proof procedure, it
  1813   operates on the first subgoal.  The unsafe wrapper tacticals are
  1814   applied to a tactic that tries @{method safe}, @{method inst_step},
  1815   or applies an unsafe rule from the context.
  1816 
  1817   \item @{method slow_step} resembles @{method step}, but allows
  1818   backtracking between using safe rules with instantiation (@{method
  1819   inst_step}) and using unsafe rules.  The resulting search space is
  1820   larger.
  1821 
  1822   \item @{method clarify_step} performs a safe step on the first
  1823   subgoal; no splitting step is applied.  For example, the subgoal
  1824   @{text "A \<and> B"} is left as a conjunction.  Proof by assumption,
  1825   Modus Ponens, etc., may be performed provided they do not
  1826   instantiate unknowns.  Assumptions of the form @{text "x = t"} may
  1827   be eliminated.  The safe wrapper tactical is applied.
  1828 
  1829   \end{description}
  1830 \<close>
  1831 
  1832 
  1833 subsection \<open>Modifying the search step\<close>
  1834 
  1835 text \<open>
  1836   \begin{mldecls}
  1837     @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
  1838     @{index_ML_op addSWrapper: "Proof.context *
  1839   (string * (Proof.context -> wrapper)) -> Proof.context"} \\
  1840     @{index_ML_op addSbefore: "Proof.context *
  1841   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
  1842     @{index_ML_op addSafter: "Proof.context *
  1843   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
  1844     @{index_ML_op delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
  1845     @{index_ML_op addWrapper: "Proof.context *
  1846   (string * (Proof.context -> wrapper)) -> Proof.context"} \\
  1847     @{index_ML_op addbefore: "Proof.context *
  1848   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
  1849     @{index_ML_op addafter: "Proof.context *
  1850   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
  1851     @{index_ML_op delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
  1852     @{index_ML addSss: "Proof.context -> Proof.context"} \\
  1853     @{index_ML addss: "Proof.context -> Proof.context"} \\
  1854   \end{mldecls}
  1855 
  1856   The proof strategy of the Classical Reasoner is simple.  Perform as
  1857   many safe inferences as possible; or else, apply certain safe rules,
  1858   allowing instantiation of unknowns; or else, apply an unsafe rule.
  1859   The tactics also eliminate assumptions of the form @{text "x = t"}
  1860   by substitution if they have been set up to do so.  They may perform
  1861   a form of Modus Ponens: if there are assumptions @{text "P \<longrightarrow> Q"} and
  1862   @{text "P"}, then replace @{text "P \<longrightarrow> Q"} by @{text "Q"}.
  1863 
  1864   The classical reasoning tools --- except @{method blast} --- allow
  1865   to modify this basic proof strategy by applying two lists of
  1866   arbitrary \emph{wrapper tacticals} to it.  The first wrapper list,
  1867   which is considered to contain safe wrappers only, affects @{method
  1868   safe_step} and all the tactics that call it.  The second one, which
  1869   may contain unsafe wrappers, affects the unsafe parts of @{method
  1870   step}, @{method slow_step}, and the tactics that call them.  A
  1871   wrapper transforms each step of the search, for example by
  1872   attempting other tactics before or after the original step tactic.
  1873   All members of a wrapper list are applied in turn to the respective
  1874   step tactic.
  1875 
  1876   Initially the two wrapper lists are empty, which means no
  1877   modification of the step tactics. Safe and unsafe wrappers are added
  1878   to a claset with the functions given below, supplying them with
  1879   wrapper names.  These names may be used to selectively delete
  1880   wrappers.
  1881 
  1882   \begin{description}
  1883 
  1884   \item @{text "ctxt addSWrapper (name, wrapper)"} adds a new wrapper,
  1885   which should yield a safe tactic, to modify the existing safe step
  1886   tactic.
  1887 
  1888   \item @{text "ctxt addSbefore (name, tac)"} adds the given tactic as a
  1889   safe wrapper, such that it is tried \emph{before} each safe step of
  1890   the search.
  1891 
  1892   \item @{text "ctxt addSafter (name, tac)"} adds the given tactic as a
  1893   safe wrapper, such that it is tried when a safe step of the search
  1894   would fail.
  1895 
  1896   \item @{text "ctxt delSWrapper name"} deletes the safe wrapper with
  1897   the given name.
  1898 
  1899   \item @{text "ctxt addWrapper (name, wrapper)"} adds a new wrapper to
  1900   modify the existing (unsafe) step tactic.
  1901 
  1902   \item @{text "ctxt addbefore (name, tac)"} adds the given tactic as an
  1903   unsafe wrapper, such that it its result is concatenated
  1904   \emph{before} the result of each unsafe step.
  1905 
  1906   \item @{text "ctxt addafter (name, tac)"} adds the given tactic as an
  1907   unsafe wrapper, such that it its result is concatenated \emph{after}
  1908   the result of each unsafe step.
  1909 
  1910   \item @{text "ctxt delWrapper name"} deletes the unsafe wrapper with
  1911   the given name.
  1912 
  1913   \item @{text "addSss"} adds the simpset of the context to its
  1914   classical set. The assumptions and goal will be simplified, in a
  1915   rather safe way, after each safe step of the search.
  1916 
  1917   \item @{text "addss"} adds the simpset of the context to its
  1918   classical set. The assumptions and goal will be simplified, before
  1919   the each unsafe step of the search.
  1920 
  1921   \end{description}
  1922 \<close>
  1923 
  1924 
  1925 section \<open>Object-logic setup \label{sec:object-logic}\<close>
  1926 
  1927 text \<open>
  1928   \begin{matharray}{rcl}
  1929     @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\
  1930     @{method_def atomize} & : & @{text method} \\
  1931     @{attribute_def atomize} & : & @{text attribute} \\
  1932     @{attribute_def rule_format} & : & @{text attribute} \\
  1933     @{attribute_def rulify} & : & @{text attribute} \\
  1934   \end{matharray}
  1935 
  1936   The very starting point for any Isabelle object-logic is a ``truth
  1937   judgment'' that links object-level statements to the meta-logic
  1938   (with its minimal language of @{text prop} that covers universal
  1939   quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).
  1940 
  1941   Common object-logics are sufficiently expressive to internalize rule
  1942   statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own
  1943   language.  This is useful in certain situations where a rule needs
  1944   to be viewed as an atomic statement from the meta-level perspective,
  1945   e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.
  1946 
  1947   From the following language elements, only the @{method atomize}
  1948   method and @{attribute rule_format} attribute are occasionally
  1949   required by end-users, the rest is for those who need to setup their
  1950   own object-logic.  In the latter case existing formulations of
  1951   Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
  1952 
  1953   Generic tools may refer to the information provided by object-logic
  1954   declarations internally.
  1955 
  1956   @{rail \<open>
  1957     @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}?
  1958     ;
  1959     @@{attribute atomize} ('(' 'full' ')')?
  1960     ;
  1961     @@{attribute rule_format} ('(' 'noasm' ')')?
  1962   \<close>}
  1963 
  1964   \begin{description}
  1965   
  1966   \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant
  1967   @{text c} as the truth judgment of the current object-logic.  Its
  1968   type @{text \<sigma>} should specify a coercion of the category of
  1969   object-level propositions to @{text prop} of the Pure meta-logic;
  1970   the mixfix annotation @{text "(mx)"} would typically just link the
  1971   object language (internally of syntactic category @{text logic})
  1972   with that of @{text prop}.  Only one @{command "judgment"}
  1973   declaration may be given in any theory development.
  1974   
  1975   \item @{method atomize} (as a method) rewrites any non-atomic
  1976   premises of a sub-goal, using the meta-level equations declared via
  1977   @{attribute atomize} (as an attribute) beforehand.  As a result,
  1978   heavily nested goals become amenable to fundamental operations such
  1979   as resolution (cf.\ the @{method (Pure) rule} method).  Giving the ``@{text
  1980   "(full)"}'' option here means to turn the whole subgoal into an
  1981   object-statement (if possible), including the outermost parameters
  1982   and assumptions as well.
  1983 
  1984   A typical collection of @{attribute atomize} rules for a particular
  1985   object-logic would provide an internalization for each of the
  1986   connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.
  1987   Meta-level conjunction should be covered as well (this is
  1988   particularly important for locales, see \secref{sec:locale}).
  1989 
  1990   \item @{attribute rule_format} rewrites a theorem by the equalities
  1991   declared as @{attribute rulify} rules in the current object-logic.
  1992   By default, the result is fully normalized, including assumptions
  1993   and conclusions at any depth.  The @{text "(no_asm)"} option
  1994   restricts the transformation to the conclusion of a rule.
  1995 
  1996   In common object-logics (HOL, FOL, ZF), the effect of @{attribute
  1997   rule_format} is to replace (bounded) universal quantification
  1998   (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
  1999   rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.
  2000 
  2001   \end{description}
  2002 \<close>
  2003 
  2004 
  2005 section \<open>Tracing higher-order unification\<close>
  2006 
  2007 text \<open>
  2008   \begin{tabular}{rcll}
  2009     @{attribute_def unify_trace_simp} & : & @{text "attribute"} & default @{text "false"} \\
  2010     @{attribute_def unify_trace_types} & : & @{text "attribute"} & default @{text "false"} \\
  2011     @{attribute_def unify_trace_bound} & : & @{text "attribute"} & default @{text "50"} \\
  2012     @{attribute_def unify_search_bound} & : & @{text "attribute"} & default @{text "60"} \\
  2013   \end{tabular}
  2014   \medskip
  2015 
  2016   Higher-order unification works well in most practical situations,
  2017   but sometimes needs extra care to identify problems.  These tracing
  2018   options may help.
  2019 
  2020   \begin{description}
  2021 
  2022   \item @{attribute unify_trace_simp} controls tracing of the
  2023   simplification phase of higher-order unification.
  2024 
  2025   \item @{attribute unify_trace_types} controls warnings of
  2026   incompleteness, when unification is not considering all possible
  2027   instantiations of schematic type variables.
  2028 
  2029   \item @{attribute unify_trace_bound} determines the depth where
  2030   unification starts to print tracing information once it reaches
  2031   depth; 0 for full tracing.  At the default value, tracing
  2032   information is almost never printed in practice.
  2033 
  2034   \item @{attribute unify_search_bound} prevents unification from
  2035   searching past the given depth.  Because of this bound, higher-order
  2036   unification cannot return an infinite sequence, though it can return
  2037   an exponentially long one.  The search rarely approaches the default
  2038   value in practice.  If the search is cut off, unification prints a
  2039   warning ``Unification bound exceeded''.
  2040 
  2041   \end{description}
  2042 
  2043   \begin{warn}
  2044   Options for unification cannot be modified in a local context.  Only
  2045   the global theory content is taken into account.
  2046   \end{warn}
  2047 \<close>
  2048 
  2049 end