doc-src/IsarRef/Thy/Generic.thy
author wenzelm
Tue May 03 16:00:29 2011 +0200 (2011-05-03)
changeset 42655 eb95e2f3b218
parent 42651 e3fdb7c96be5
child 42704 3f19e324ff59
permissions -rw-r--r--
updated configuration options -- no ML here;
     1 theory Generic
     2 imports Base Main
     3 begin
     4 
     5 chapter {* Generic tools and packages \label{ch:gen-tools} *}
     6 
     7 section {* Configuration options \label{sec:config} *}
     8 
     9 text {* Isabelle/Pure maintains a record of named configuration
    10   options within the theory or proof context, with values of type
    11   @{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type
    12   string}.  Tools may declare options in ML, and then refer to these
    13   values (relative to the context).  Thus global reference variables
    14   are easily avoided.  The user may change the value of a
    15   configuration option by means of an associated attribute of the same
    16   name.  This form of context declaration works particularly well with
    17   commands such as @{command "declare"} or @{command "using"} like
    18   this:
    19 *}
    20 
    21 declare [[show_main_goal = false]]
    22 
    23 notepad
    24 begin
    25   note [[show_main_goal = true]]
    26 end
    27 
    28 text {* For historical reasons, some tools cannot take the full proof
    29   context into account and merely refer to the background theory.
    30   This is accommodated by configuration options being declared as
    31   ``global'', which may not be changed within a local context.
    32 
    33   \begin{matharray}{rcll}
    34     @{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\
    35   \end{matharray}
    36 
    37   @{rail "
    38     @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?
    39   "}
    40 
    41   \begin{description}
    42   
    43   \item @{command "print_configs"} prints the available configuration
    44   options, with names, types, and current values.
    45   
    46   \item @{text "name = value"} as an attribute expression modifies the
    47   named option, with the syntax of the value depending on the option's
    48   type.  For @{ML_type bool} the default value is @{text true}.  Any
    49   attempt to change a global option in a local context is ignored.
    50 
    51   \end{description}
    52 *}
    53 
    54 
    55 section {* Basic proof tools *}
    56 
    57 subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *}
    58 
    59 text {*
    60   \begin{matharray}{rcl}
    61     @{method_def unfold} & : & @{text method} \\
    62     @{method_def fold} & : & @{text method} \\
    63     @{method_def insert} & : & @{text method} \\[0.5ex]
    64     @{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\
    65     @{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\
    66     @{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
    67     @{method_def succeed} & : & @{text method} \\
    68     @{method_def fail} & : & @{text method} \\
    69   \end{matharray}
    70 
    71   @{rail "
    72     (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
    73     ;
    74     (@@{method erule} | @@{method drule} | @@{method frule})
    75       ('(' @{syntax nat} ')')? @{syntax thmrefs}
    76   "}
    77 
    78   \begin{description}
    79   
    80   \item @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text
    81   "a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout
    82   all goals; any chained facts provided are inserted into the goal and
    83   subject to rewriting as well.
    84 
    85   \item @{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} inserts theorems as facts
    86   into all goals of the proof state.  Note that current facts
    87   indicated for forward chaining are ignored.
    88 
    89   \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method
    90   drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text
    91   "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule}
    92   method (see \secref{sec:pure-meth-att}), but apply rules by
    93   elim-resolution, destruct-resolution, and forward-resolution,
    94   respectively \cite{isabelle-implementation}.  The optional natural
    95   number argument (default 0) specifies additional assumption steps to
    96   be performed here.
    97 
    98   Note that these methods are improper ones, mainly serving for
    99   experimentation and tactic script emulation.  Different modes of
   100   basic rule application are usually expressed in Isar at the proof
   101   language level, rather than via implicit proof state manipulations.
   102   For example, a proper single-step elimination would be done using
   103   the plain @{method rule} method, with forward chaining of current
   104   facts.
   105 
   106   \item @{method succeed} yields a single (unchanged) result; it is
   107   the identity of the ``@{text ","}'' method combinator (cf.\
   108   \secref{sec:proof-meth}).
   109 
   110   \item @{method fail} yields an empty result sequence; it is the
   111   identity of the ``@{text "|"}'' method combinator (cf.\
   112   \secref{sec:proof-meth}).
   113 
   114   \end{description}
   115 
   116   \begin{matharray}{rcl}
   117     @{attribute_def tagged} & : & @{text attribute} \\
   118     @{attribute_def untagged} & : & @{text attribute} \\[0.5ex]
   119     @{attribute_def THEN} & : & @{text attribute} \\
   120     @{attribute_def COMP} & : & @{text attribute} \\[0.5ex]
   121     @{attribute_def unfolded} & : & @{text attribute} \\
   122     @{attribute_def folded} & : & @{text attribute} \\[0.5ex]
   123     @{attribute_def rotated} & : & @{text attribute} \\
   124     @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
   125     @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
   126     @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
   127   \end{matharray}
   128 
   129   @{rail "
   130     @@{attribute tagged} @{syntax name} @{syntax name}
   131     ;
   132     @@{attribute untagged} @{syntax name}
   133     ;
   134     (@@{attribute THEN} | @@{attribute COMP}) ('[' @{syntax nat} ']')? @{syntax thmref}
   135     ;
   136     (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
   137     ;
   138     @@{attribute rotated} @{syntax int}?
   139   "}
   140 
   141   \begin{description}
   142 
   143   \item @{attribute tagged}~@{text "name value"} and @{attribute
   144   untagged}~@{text name} add and remove \emph{tags} of some theorem.
   145   Tags may be any list of string pairs that serve as formal comment.
   146   The first string is considered the tag name, the second its value.
   147   Note that @{attribute untagged} removes any tags of the same name.
   148 
   149   \item @{attribute THEN}~@{text a} and @{attribute COMP}~@{text a}
   150   compose rules by resolution.  @{attribute THEN} resolves with the
   151   first premise of @{text a} (an alternative position may be also
   152   specified); the @{attribute COMP} version skips the automatic
   153   lifting process that is normally intended (cf.\ @{ML "op RS"} and
   154   @{ML "op COMP"} in \cite{isabelle-implementation}).
   155   
   156   \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
   157   folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
   158   definitions throughout a rule.
   159 
   160   \item @{attribute rotated}~@{text n} rotate the premises of a
   161   theorem by @{text n} (default 1).
   162 
   163   \item @{attribute (Pure) elim_format} turns a destruction rule into
   164   elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
   165   (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
   166   
   167   Note that the Classical Reasoner (\secref{sec:classical}) provides
   168   its own version of this operation.
   169 
   170   \item @{attribute standard} puts a theorem into the standard form of
   171   object-rules at the outermost theory level.  Note that this
   172   operation violates the local proof context (including active
   173   locales).
   174 
   175   \item @{attribute no_vars} replaces schematic variables by free
   176   ones; this is mainly for tuning output of pretty printed theorems.
   177 
   178   \end{description}
   179 *}
   180 
   181 
   182 subsection {* Low-level equational reasoning *}
   183 
   184 text {*
   185   \begin{matharray}{rcl}
   186     @{method_def subst} & : & @{text method} \\
   187     @{method_def hypsubst} & : & @{text method} \\
   188     @{method_def split} & : & @{text method} \\
   189   \end{matharray}
   190 
   191   @{rail "
   192     @@{method subst} ('(' 'asm' ')')? ('(' (@{syntax nat}+) ')')? @{syntax thmref}
   193     ;
   194     @@{method split} ('(' 'asm' ')')? @{syntax thmrefs}
   195   "}
   196 
   197   These methods provide low-level facilities for equational reasoning
   198   that are intended for specialized applications only.  Normally,
   199   single step calculations would be performed in a structured text
   200   (see also \secref{sec:calculation}), while the Simplifier methods
   201   provide the canonical way for automated normalization (see
   202   \secref{sec:simplifier}).
   203 
   204   \begin{description}
   205 
   206   \item @{method subst}~@{text eq} performs a single substitution step
   207   using rule @{text eq}, which may be either a meta or object
   208   equality.
   209 
   210   \item @{method subst}~@{text "(asm) eq"} substitutes in an
   211   assumption.
   212 
   213   \item @{method subst}~@{text "(i \<dots> j) eq"} performs several
   214   substitutions in the conclusion. The numbers @{text i} to @{text j}
   215   indicate the positions to substitute at.  Positions are ordered from
   216   the top of the term tree moving down from left to right. For
   217   example, in @{text "(a + b) + (c + d)"} there are three positions
   218   where commutativity of @{text "+"} is applicable: 1 refers to @{text
   219   "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}.
   220 
   221   If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
   222   (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
   223   assume all substitutions are performed simultaneously.  Otherwise
   224   the behaviour of @{text subst} is not specified.
   225 
   226   \item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the
   227   substitutions in the assumptions. The positions refer to the
   228   assumptions in order from left to right.  For example, given in a
   229   goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of
   230   commutativity of @{text "+"} is the subterm @{text "a + b"} and
   231   position 2 is the subterm @{text "c + d"}.
   232 
   233   \item @{method hypsubst} performs substitution using some
   234   assumption; this only works for equations of the form @{text "x =
   235   t"} where @{text x} is a free or bound variable.
   236 
   237   \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
   238   splitting using the given rules.  By default, splitting is performed
   239   in the conclusion of a goal; the @{text "(asm)"} option indicates to
   240   operate on assumptions instead.
   241   
   242   Note that the @{method simp} method already involves repeated
   243   application of split rules as declared in the current context.
   244 
   245   \end{description}
   246 *}
   247 
   248 
   249 subsection {* Further tactic emulations \label{sec:tactics} *}
   250 
   251 text {*
   252   The following improper proof methods emulate traditional tactics.
   253   These admit direct access to the goal state, which is normally
   254   considered harmful!  In particular, this may involve both numbered
   255   goal addressing (default 1), and dynamic instantiation within the
   256   scope of some subgoal.
   257 
   258   \begin{warn}
   259     Dynamic instantiations refer to universally quantified parameters
   260     of a subgoal (the dynamic context) rather than fixed variables and
   261     term abbreviations of a (static) Isar context.
   262   \end{warn}
   263 
   264   Tactic emulation methods, unlike their ML counterparts, admit
   265   simultaneous instantiation from both dynamic and static contexts.
   266   If names occur in both contexts goal parameters hide locally fixed
   267   variables.  Likewise, schematic variables refer to term
   268   abbreviations, if present in the static context.  Otherwise the
   269   schematic variable is interpreted as a schematic variable and left
   270   to be solved by unification with certain parts of the subgoal.
   271 
   272   Note that the tactic emulation proof methods in Isabelle/Isar are
   273   consistently named @{text foo_tac}.  Note also that variable names
   274   occurring on left hand sides of instantiations must be preceded by a
   275   question mark if they coincide with a keyword or contain dots.  This
   276   is consistent with the attribute @{attribute "where"} (see
   277   \secref{sec:pure-meth-att}).
   278 
   279   \begin{matharray}{rcl}
   280     @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   281     @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   282     @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   283     @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   284     @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
   285     @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
   286     @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
   287     @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
   288     @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
   289     @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
   290     @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
   291   \end{matharray}
   292 
   293   @{rail "
   294     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
   295       @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}?
   296     ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
   297     ;
   298     @@{method subgoal_tac} @{syntax goalspec}? (@{syntax prop} +)
   299     ;
   300     @@{method rename_tac} @{syntax goalspec}? (@{syntax name} +)
   301     ;
   302     @@{method rotate_tac} @{syntax goalspec}? @{syntax int}?
   303     ;
   304     (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
   305     ;
   306 
   307     dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
   308   "}
   309 
   310 \begin{description}
   311 
   312   \item @{method rule_tac} etc. do resolution of rules with explicit
   313   instantiation.  This works the same way as the ML tactics @{ML
   314   res_inst_tac} etc. (see \cite{isabelle-implementation})
   315 
   316   Multiple rules may be only given if there is no instantiation; then
   317   @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
   318   \cite{isabelle-implementation}).
   319 
   320   \item @{method cut_tac} inserts facts into the proof state as
   321   assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
   322   \cite{isabelle-implementation}.  Note that the scope of schematic
   323   variables is spread over the main goal statement.  Instantiations
   324   may be given as well, see also ML tactic @{ML cut_inst_tac} in
   325   \cite{isabelle-implementation}.
   326 
   327   \item @{method thin_tac}~@{text \<phi>} deletes the specified assumption
   328   from a subgoal; note that @{text \<phi>} may contain schematic variables.
   329   See also @{ML thin_tac} in \cite{isabelle-implementation}.
   330 
   331   \item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an
   332   assumption to a subgoal.  See also @{ML subgoal_tac} and @{ML
   333   subgoals_tac} in \cite{isabelle-implementation}.
   334 
   335   \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
   336   goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
   337   \emph{suffix} of variables.
   338 
   339   \item @{method rotate_tac}~@{text n} rotates the assumptions of a
   340   goal by @{text n} positions: from right to left if @{text n} is
   341   positive, and from left to right if @{text n} is negative; the
   342   default value is 1.  See also @{ML rotate_tac} in
   343   \cite{isabelle-implementation}.
   344 
   345   \item @{method tactic}~@{text "text"} produces a proof method from
   346   any ML text of type @{ML_type tactic}.  Apart from the usual ML
   347   environment and the current proof context, the ML code may refer to
   348   the locally bound values @{ML_text facts}, which indicates any
   349   current facts used for forward-chaining.
   350 
   351   \item @{method raw_tactic} is similar to @{method tactic}, but
   352   presents the goal state in its raw internal form, where simultaneous
   353   subgoals appear as conjunction of the logical framework instead of
   354   the usual split into several subgoals.  While feature this is useful
   355   for debugging of complex method definitions, it should not never
   356   appear in production theories.
   357 
   358   \end{description}
   359 *}
   360 
   361 
   362 section {* The Simplifier \label{sec:simplifier} *}
   363 
   364 subsection {* Simplification methods *}
   365 
   366 text {*
   367   \begin{matharray}{rcl}
   368     @{method_def simp} & : & @{text method} \\
   369     @{method_def simp_all} & : & @{text method} \\
   370   \end{matharray}
   371 
   372   @{rail "
   373     (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
   374     ;
   375 
   376     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
   377     ;
   378     @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
   379       'split' (() | 'add' | 'del')) ':' @{syntax thmrefs}
   380   "}
   381 
   382   \begin{description}
   383 
   384   \item @{method simp} invokes the Simplifier, after declaring
   385   additional rules according to the arguments given.  Note that the
   386   @{text only} modifier first removes all other rewrite rules,
   387   congruences, and looper tactics (including splits), and then behaves
   388   like @{text add}.
   389 
   390   \medskip The @{text cong} modifiers add or delete Simplifier
   391   congruence rules (see also \cite{isabelle-ref}), the default is to
   392   add.
   393 
   394   \medskip The @{text split} modifiers add or delete rules for the
   395   Splitter (see also \cite{isabelle-ref}), the default is to add.
   396   This works only if the Simplifier method has been properly setup to
   397   include the Splitter (all major object logics such HOL, HOLCF, FOL,
   398   ZF do this already).
   399 
   400   \item @{method simp_all} is similar to @{method simp}, but acts on
   401   all goals (backwards from the last to the first one).
   402 
   403   \end{description}
   404 
   405   By default the Simplifier methods take local assumptions fully into
   406   account, using equational assumptions in the subsequent
   407   normalization process, or simplifying assumptions themselves (cf.\
   408   @{ML asm_full_simp_tac} in \cite{isabelle-ref}).  In structured
   409   proofs this is usually quite well behaved in practice: just the
   410   local premises of the actual goal are involved, additional facts may
   411   be inserted via explicit forward-chaining (via @{command "then"},
   412   @{command "from"}, @{command "using"} etc.).
   413 
   414   Additional Simplifier options may be specified to tune the behavior
   415   further (mostly for unstructured scripts with many accidental local
   416   facts): ``@{text "(no_asm)"}'' means assumptions are ignored
   417   completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means
   418   assumptions are used in the simplification of the conclusion but are
   419   not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text
   420   "(no_asm_use)"}'' means assumptions are simplified but are not used
   421   in the simplification of each other or the conclusion (cf.\ @{ML
   422   full_simp_tac}).  For compatibility reasons, there is also an option
   423   ``@{text "(asm_lr)"}'', which means that an assumption is only used
   424   for simplifying assumptions which are to the right of it (cf.\ @{ML
   425   asm_lr_simp_tac}).
   426 
   427   The configuration option @{text "depth_limit"} limits the number of
   428   recursive invocations of the simplifier during conditional
   429   rewriting.
   430 
   431   \medskip The Splitter package is usually configured to work as part
   432   of the Simplifier.  The effect of repeatedly applying @{ML
   433   split_tac} can be simulated by ``@{text "(simp only: split:
   434   a\<^sub>1 \<dots> a\<^sub>n)"}''.  There is also a separate @{text split}
   435   method available for single-step case splitting.
   436 *}
   437 
   438 
   439 subsection {* Declaring rules *}
   440 
   441 text {*
   442   \begin{matharray}{rcl}
   443     @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   444     @{attribute_def simp} & : & @{text attribute} \\
   445     @{attribute_def cong} & : & @{text attribute} \\
   446     @{attribute_def split} & : & @{text attribute} \\
   447   \end{matharray}
   448 
   449   @{rail "
   450     (@@{attribute simp} | @@{attribute cong} | @@{attribute split}) (() | 'add' | 'del')
   451   "}
   452 
   453   \begin{description}
   454 
   455   \item @{command "print_simpset"} prints the collection of rules
   456   declared to the Simplifier, which is also known as ``simpset''
   457   internally \cite{isabelle-ref}.
   458 
   459   \item @{attribute simp} declares simplification rules.
   460 
   461   \item @{attribute cong} declares congruence rules.
   462 
   463   \item @{attribute split} declares case split rules.
   464 
   465   \end{description}
   466 *}
   467 
   468 
   469 subsection {* Simplification procedures *}
   470 
   471 text {*
   472   \begin{matharray}{rcl}
   473     @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   474     simproc & : & @{text attribute} \\
   475   \end{matharray}
   476 
   477   @{rail "
   478     @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
   479       @{syntax text} \\ (@'identifier' (@{syntax nameref}+))?
   480     ;
   481 
   482     @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
   483   "}
   484 
   485   \begin{description}
   486 
   487   \item @{command "simproc_setup"} defines a named simplification
   488   procedure that is invoked by the Simplifier whenever any of the
   489   given term patterns match the current redex.  The implementation,
   490   which is provided as ML source text, needs to be of type @{ML_type
   491   "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type
   492   cterm} represents the current redex @{text r} and the result is
   493   supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a
   494   generalized version), or @{ML NONE} to indicate failure.  The
   495   @{ML_type simpset} argument holds the full context of the current
   496   Simplifier invocation, including the actual Isar proof context.  The
   497   @{ML_type morphism} informs about the difference of the original
   498   compilation context wrt.\ the one of the actual application later
   499   on.  The optional @{keyword "identifier"} specifies theorems that
   500   represent the logical content of the abstract theory of this
   501   simproc.
   502 
   503   Morphisms and identifiers are only relevant for simprocs that are
   504   defined within a local target context, e.g.\ in a locale.
   505 
   506   \item @{text "simproc add: name"} and @{text "simproc del: name"}
   507   add or delete named simprocs to the current Simplifier context.  The
   508   default is to add a simproc.  Note that @{command "simproc_setup"}
   509   already adds the new simproc to the subsequent context.
   510 
   511   \end{description}
   512 *}
   513 
   514 
   515 subsection {* Forward simplification *}
   516 
   517 text {*
   518   \begin{matharray}{rcl}
   519     @{attribute_def simplified} & : & @{text attribute} \\
   520   \end{matharray}
   521 
   522   @{rail "
   523     @@{attribute simplified} opt? @{syntax thmrefs}?
   524     ;
   525 
   526     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
   527   "}
   528 
   529   \begin{description}
   530   
   531   \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to
   532   be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,
   533   a\<^sub>n"}, or the implicit Simplifier context if no arguments are given.
   534   The result is fully simplified by default, including assumptions and
   535   conclusion; the options @{text no_asm} etc.\ tune the Simplifier in
   536   the same way as the for the @{text simp} method.
   537 
   538   Note that forward simplification restricts the simplifier to its
   539   most basic operation of term rewriting; solver and looper tactics
   540   \cite{isabelle-ref} are \emph{not} involved here.  The @{text
   541   simplified} attribute should be only rarely required under normal
   542   circumstances.
   543 
   544   \end{description}
   545 *}
   546 
   547 
   548 section {* The Classical Reasoner \label{sec:classical} *}
   549 
   550 subsection {* Basic methods *}
   551 
   552 text {*
   553   \begin{matharray}{rcl}
   554     @{method_def rule} & : & @{text method} \\
   555     @{method_def contradiction} & : & @{text method} \\
   556     @{method_def intro} & : & @{text method} \\
   557     @{method_def elim} & : & @{text method} \\
   558   \end{matharray}
   559 
   560   @{rail "
   561     (@@{method rule} | @@{method intro} | @@{method elim}) @{syntax thmrefs}?
   562   "}
   563 
   564   \begin{description}
   565 
   566   \item @{method rule} as offered by the Classical Reasoner is a
   567   refinement over the primitive one (see \secref{sec:pure-meth-att}).
   568   Both versions essentially work the same, but the classical version
   569   observes the classical rule context in addition to that of
   570   Isabelle/Pure.
   571 
   572   Common object logics (HOL, ZF, etc.) declare a rich collection of
   573   classical rules (even if these would qualify as intuitionistic
   574   ones), but only few declarations to the rule context of
   575   Isabelle/Pure (\secref{sec:pure-meth-att}).
   576 
   577   \item @{method contradiction} solves some goal by contradiction,
   578   deriving any result from both @{text "\<not> A"} and @{text A}.  Chained
   579   facts, which are guaranteed to participate, may appear in either
   580   order.
   581 
   582   \item @{method intro} and @{method elim} repeatedly refine some goal
   583   by intro- or elim-resolution, after having inserted any chained
   584   facts.  Exactly the rules given as arguments are taken into account;
   585   this allows fine-tuned decomposition of a proof problem, in contrast
   586   to common automated tools.
   587 
   588   \end{description}
   589 *}
   590 
   591 
   592 subsection {* Automated methods *}
   593 
   594 text {*
   595   \begin{matharray}{rcl}
   596     @{method_def blast} & : & @{text method} \\
   597     @{method_def fast} & : & @{text method} \\
   598     @{method_def slow} & : & @{text method} \\
   599     @{method_def best} & : & @{text method} \\
   600     @{method_def safe} & : & @{text method} \\
   601     @{method_def clarify} & : & @{text method} \\
   602   \end{matharray}
   603 
   604   @{rail "
   605     @@{method blast} @{syntax nat}? (@{syntax clamod} * )
   606     ;
   607     (@@{method fast} | @@{method slow} | @@{method best} | @@{method safe} | @@{method clarify})
   608       (@{syntax clamod} * )
   609     ;
   610 
   611     @{syntax_def clamod}:
   612       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
   613   "}
   614 
   615   \begin{description}
   616 
   617   \item @{method blast} refers to the classical tableau prover (see
   618   @{ML blast_tac} in \cite{isabelle-ref}).  The optional argument
   619   specifies a user-supplied search bound (default 20).
   620 
   621   \item @{method fast}, @{method slow}, @{method best}, @{method
   622   safe}, and @{method clarify} refer to the generic classical
   623   reasoner.  See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML
   624   safe_tac}, and @{ML clarify_tac} in \cite{isabelle-ref} for more
   625   information.
   626 
   627   \end{description}
   628 
   629   Any of the above methods support additional modifiers of the context
   630   of classical rules.  Their semantics is analogous to the attributes
   631   given before.  Facts provided by forward chaining are inserted into
   632   the goal before commencing proof search.
   633 *}
   634 
   635 
   636 subsection {* Combined automated methods \label{sec:clasimp} *}
   637 
   638 text {*
   639   \begin{matharray}{rcl}
   640     @{method_def auto} & : & @{text method} \\
   641     @{method_def force} & : & @{text method} \\
   642     @{method_def clarsimp} & : & @{text method} \\
   643     @{method_def fastsimp} & : & @{text method} \\
   644     @{method_def slowsimp} & : & @{text method} \\
   645     @{method_def bestsimp} & : & @{text method} \\
   646   \end{matharray}
   647 
   648   @{rail "
   649     @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )
   650     ;
   651     (@@{method force} | @@{method clarsimp} | @@{method fastsimp} | @@{method slowsimp} |
   652       @@{method bestsimp}) (@{syntax clasimpmod} * )
   653     ;
   654 
   655     @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
   656       ('cong' | 'split') (() | 'add' | 'del') |
   657       'iff' (((() | 'add') '?'?) | 'del') |
   658       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
   659   "}
   660 
   661   \begin{description}
   662 
   663   \item @{method auto}, @{method force}, @{method clarsimp}, @{method
   664   fastsimp}, @{method slowsimp}, and @{method bestsimp} provide access
   665   to Isabelle's combined simplification and classical reasoning
   666   tactics.  These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML
   667   clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
   668   added as wrapper, see \cite{isabelle-ref} for more information.  The
   669   modifier arguments correspond to those given in
   670   \secref{sec:simplifier} and \secref{sec:classical}.  Just note that
   671   the ones related to the Simplifier are prefixed by @{text simp}
   672   here.
   673 
   674   Facts provided by forward chaining are inserted into the goal before
   675   doing the search.
   676 
   677   \end{description}
   678 *}
   679 
   680 
   681 subsection {* Declaring rules *}
   682 
   683 text {*
   684   \begin{matharray}{rcl}
   685     @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   686     @{attribute_def intro} & : & @{text attribute} \\
   687     @{attribute_def elim} & : & @{text attribute} \\
   688     @{attribute_def dest} & : & @{text attribute} \\
   689     @{attribute_def rule} & : & @{text attribute} \\
   690     @{attribute_def iff} & : & @{text attribute} \\
   691   \end{matharray}
   692 
   693   @{rail "
   694     (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
   695     ;
   696     @@{attribute rule} 'del'
   697     ;
   698     @@{attribute iff} (((() | 'add') '?'?) | 'del')
   699   "}
   700 
   701   \begin{description}
   702 
   703   \item @{command "print_claset"} prints the collection of rules
   704   declared to the Classical Reasoner, which is also known as
   705   ``claset'' internally \cite{isabelle-ref}.
   706   
   707   \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
   708   declare introduction, elimination, and destruction rules,
   709   respectively.  By default, rules are considered as \emph{unsafe}
   710   (i.e.\ not applied blindly without backtracking), while ``@{text
   711   "!"}'' classifies as \emph{safe}.  Rule declarations marked by
   712   ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
   713   \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
   714   of the @{method rule} method).  The optional natural number
   715   specifies an explicit weight argument, which is ignored by automated
   716   tools, but determines the search order of single rule steps.
   717 
   718   \item @{attribute rule}~@{text del} deletes introduction,
   719   elimination, or destruction rules from the context.
   720 
   721   \item @{attribute iff} declares logical equivalences to the
   722   Simplifier and the Classical reasoner at the same time.
   723   Non-conditional rules result in a ``safe'' introduction and
   724   elimination pair; conditional ones are considered ``unsafe''.  Rules
   725   with negative conclusion are automatically inverted (using @{text
   726   "\<not>"}-elimination internally).
   727 
   728   The ``@{text "?"}'' version of @{attribute iff} declares rules to
   729   the Isabelle/Pure context only, and omits the Simplifier
   730   declaration.
   731 
   732   \end{description}
   733 *}
   734 
   735 
   736 subsection {* Classical operations *}
   737 
   738 text {*
   739   \begin{matharray}{rcl}
   740     @{attribute_def swapped} & : & @{text attribute} \\
   741   \end{matharray}
   742 
   743   \begin{description}
   744 
   745   \item @{attribute swapped} turns an introduction rule into an
   746   elimination, by resolving with the classical swap principle @{text
   747   "(\<not> B \<Longrightarrow> A) \<Longrightarrow> (\<not> A \<Longrightarrow> B)"}.
   748 
   749   \end{description}
   750 *}
   751 
   752 
   753 section {* Object-logic setup \label{sec:object-logic} *}
   754 
   755 text {*
   756   \begin{matharray}{rcl}
   757     @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\
   758     @{method_def atomize} & : & @{text method} \\
   759     @{attribute_def atomize} & : & @{text attribute} \\
   760     @{attribute_def rule_format} & : & @{text attribute} \\
   761     @{attribute_def rulify} & : & @{text attribute} \\
   762   \end{matharray}
   763 
   764   The very starting point for any Isabelle object-logic is a ``truth
   765   judgment'' that links object-level statements to the meta-logic
   766   (with its minimal language of @{text prop} that covers universal
   767   quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).
   768 
   769   Common object-logics are sufficiently expressive to internalize rule
   770   statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own
   771   language.  This is useful in certain situations where a rule needs
   772   to be viewed as an atomic statement from the meta-level perspective,
   773   e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.
   774 
   775   From the following language elements, only the @{method atomize}
   776   method and @{attribute rule_format} attribute are occasionally
   777   required by end-users, the rest is for those who need to setup their
   778   own object-logic.  In the latter case existing formulations of
   779   Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
   780 
   781   Generic tools may refer to the information provided by object-logic
   782   declarations internally.
   783 
   784   @{rail "
   785     @@{command judgment} @{syntax constdecl}
   786     ;
   787     @@{attribute atomize} ('(' 'full' ')')?
   788     ;
   789     @@{attribute rule_format} ('(' 'noasm' ')')?
   790   "}
   791 
   792   \begin{description}
   793   
   794   \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant
   795   @{text c} as the truth judgment of the current object-logic.  Its
   796   type @{text \<sigma>} should specify a coercion of the category of
   797   object-level propositions to @{text prop} of the Pure meta-logic;
   798   the mixfix annotation @{text "(mx)"} would typically just link the
   799   object language (internally of syntactic category @{text logic})
   800   with that of @{text prop}.  Only one @{command "judgment"}
   801   declaration may be given in any theory development.
   802   
   803   \item @{method atomize} (as a method) rewrites any non-atomic
   804   premises of a sub-goal, using the meta-level equations declared via
   805   @{attribute atomize} (as an attribute) beforehand.  As a result,
   806   heavily nested goals become amenable to fundamental operations such
   807   as resolution (cf.\ the @{method (Pure) rule} method).  Giving the ``@{text
   808   "(full)"}'' option here means to turn the whole subgoal into an
   809   object-statement (if possible), including the outermost parameters
   810   and assumptions as well.
   811 
   812   A typical collection of @{attribute atomize} rules for a particular
   813   object-logic would provide an internalization for each of the
   814   connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.
   815   Meta-level conjunction should be covered as well (this is
   816   particularly important for locales, see \secref{sec:locale}).
   817 
   818   \item @{attribute rule_format} rewrites a theorem by the equalities
   819   declared as @{attribute rulify} rules in the current object-logic.
   820   By default, the result is fully normalized, including assumptions
   821   and conclusions at any depth.  The @{text "(no_asm)"} option
   822   restricts the transformation to the conclusion of a rule.
   823 
   824   In common object-logics (HOL, FOL, ZF), the effect of @{attribute
   825   rule_format} is to replace (bounded) universal quantification
   826   (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
   827   rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.
   828 
   829   \end{description}
   830 *}
   831 
   832 end