src/Doc/IsarRef/Generic.thy
changeset 48985 5386df44a037
parent 48958 12afbf6eb7f9
child 50063 7e491da6bcbd
equal deleted inserted replaced
48984:f51d4a302962 48985:5386df44a037
       
     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 intro} & : & @{text method} \\
       
    68     @{method_def elim} & : & @{text method} \\
       
    69     @{method_def succeed} & : & @{text method} \\
       
    70     @{method_def fail} & : & @{text method} \\
       
    71   \end{matharray}
       
    72 
       
    73   @{rail "
       
    74     (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
       
    75     ;
       
    76     (@@{method erule} | @@{method drule} | @@{method frule})
       
    77       ('(' @{syntax nat} ')')? @{syntax thmrefs}
       
    78     ;
       
    79     (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
       
    80   "}
       
    81 
       
    82   \begin{description}
       
    83   
       
    84   \item @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text
       
    85   "a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout
       
    86   all goals; any chained facts provided are inserted into the goal and
       
    87   subject to rewriting as well.
       
    88 
       
    89   \item @{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} inserts theorems as facts
       
    90   into all goals of the proof state.  Note that current facts
       
    91   indicated for forward chaining are ignored.
       
    92 
       
    93   \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method
       
    94   drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text
       
    95   "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule}
       
    96   method (see \secref{sec:pure-meth-att}), but apply rules by
       
    97   elim-resolution, destruct-resolution, and forward-resolution,
       
    98   respectively \cite{isabelle-implementation}.  The optional natural
       
    99   number argument (default 0) specifies additional assumption steps to
       
   100   be performed here.
       
   101 
       
   102   Note that these methods are improper ones, mainly serving for
       
   103   experimentation and tactic script emulation.  Different modes of
       
   104   basic rule application are usually expressed in Isar at the proof
       
   105   language level, rather than via implicit proof state manipulations.
       
   106   For example, a proper single-step elimination would be done using
       
   107   the plain @{method rule} method, with forward chaining of current
       
   108   facts.
       
   109 
       
   110   \item @{method intro} and @{method elim} repeatedly refine some goal
       
   111   by intro- or elim-resolution, after having inserted any chained
       
   112   facts.  Exactly the rules given as arguments are taken into account;
       
   113   this allows fine-tuned decomposition of a proof problem, in contrast
       
   114   to common automated tools.
       
   115 
       
   116   \item @{method succeed} yields a single (unchanged) result; it is
       
   117   the identity of the ``@{text ","}'' method combinator (cf.\
       
   118   \secref{sec:proof-meth}).
       
   119 
       
   120   \item @{method fail} yields an empty result sequence; it is the
       
   121   identity of the ``@{text "|"}'' method combinator (cf.\
       
   122   \secref{sec:proof-meth}).
       
   123 
       
   124   \end{description}
       
   125 
       
   126   \begin{matharray}{rcl}
       
   127     @{attribute_def tagged} & : & @{text attribute} \\
       
   128     @{attribute_def untagged} & : & @{text attribute} \\[0.5ex]
       
   129     @{attribute_def THEN} & : & @{text attribute} \\
       
   130     @{attribute_def unfolded} & : & @{text attribute} \\
       
   131     @{attribute_def folded} & : & @{text attribute} \\
       
   132     @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]
       
   133     @{attribute_def rotated} & : & @{text attribute} \\
       
   134     @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
       
   135     @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
       
   136     @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
       
   137   \end{matharray}
       
   138 
       
   139   @{rail "
       
   140     @@{attribute tagged} @{syntax name} @{syntax name}
       
   141     ;
       
   142     @@{attribute untagged} @{syntax name}
       
   143     ;
       
   144     @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref}
       
   145     ;
       
   146     (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
       
   147     ;
       
   148     @@{attribute rotated} @{syntax int}?
       
   149   "}
       
   150 
       
   151   \begin{description}
       
   152 
       
   153   \item @{attribute tagged}~@{text "name value"} and @{attribute
       
   154   untagged}~@{text name} add and remove \emph{tags} of some theorem.
       
   155   Tags may be any list of string pairs that serve as formal comment.
       
   156   The first string is considered the tag name, the second its value.
       
   157   Note that @{attribute untagged} removes any tags of the same name.
       
   158 
       
   159   \item @{attribute THEN}~@{text a} composes rules by resolution; it
       
   160   resolves with the first premise of @{text a} (an alternative
       
   161   position may be also specified).  See also @{ML_op "RS"} in
       
   162   \cite{isabelle-implementation}.
       
   163   
       
   164   \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
       
   165   folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
       
   166   definitions throughout a rule.
       
   167 
       
   168   \item @{attribute abs_def} turns an equation of the form @{prop "f x
       
   169   y \<equiv> t"} into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method
       
   170   simp} or @{method unfold} steps always expand it.  This also works
       
   171   for object-logic equality.
       
   172 
       
   173   \item @{attribute rotated}~@{text n} rotate the premises of a
       
   174   theorem by @{text n} (default 1).
       
   175 
       
   176   \item @{attribute (Pure) elim_format} turns a destruction rule into
       
   177   elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
       
   178   (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
       
   179   
       
   180   Note that the Classical Reasoner (\secref{sec:classical}) provides
       
   181   its own version of this operation.
       
   182 
       
   183   \item @{attribute standard} puts a theorem into the standard form of
       
   184   object-rules at the outermost theory level.  Note that this
       
   185   operation violates the local proof context (including active
       
   186   locales).
       
   187 
       
   188   \item @{attribute no_vars} replaces schematic variables by free
       
   189   ones; this is mainly for tuning output of pretty printed theorems.
       
   190 
       
   191   \end{description}
       
   192 *}
       
   193 
       
   194 
       
   195 subsection {* Low-level equational reasoning *}
       
   196 
       
   197 text {*
       
   198   \begin{matharray}{rcl}
       
   199     @{method_def subst} & : & @{text method} \\
       
   200     @{method_def hypsubst} & : & @{text method} \\
       
   201     @{method_def split} & : & @{text method} \\
       
   202   \end{matharray}
       
   203 
       
   204   @{rail "
       
   205     @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
       
   206     ;
       
   207     @@{method split} @{syntax thmrefs}
       
   208   "}
       
   209 
       
   210   These methods provide low-level facilities for equational reasoning
       
   211   that are intended for specialized applications only.  Normally,
       
   212   single step calculations would be performed in a structured text
       
   213   (see also \secref{sec:calculation}), while the Simplifier methods
       
   214   provide the canonical way for automated normalization (see
       
   215   \secref{sec:simplifier}).
       
   216 
       
   217   \begin{description}
       
   218 
       
   219   \item @{method subst}~@{text eq} performs a single substitution step
       
   220   using rule @{text eq}, which may be either a meta or object
       
   221   equality.
       
   222 
       
   223   \item @{method subst}~@{text "(asm) eq"} substitutes in an
       
   224   assumption.
       
   225 
       
   226   \item @{method subst}~@{text "(i \<dots> j) eq"} performs several
       
   227   substitutions in the conclusion. The numbers @{text i} to @{text j}
       
   228   indicate the positions to substitute at.  Positions are ordered from
       
   229   the top of the term tree moving down from left to right. For
       
   230   example, in @{text "(a + b) + (c + d)"} there are three positions
       
   231   where commutativity of @{text "+"} is applicable: 1 refers to @{text
       
   232   "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}.
       
   233 
       
   234   If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
       
   235   (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
       
   236   assume all substitutions are performed simultaneously.  Otherwise
       
   237   the behaviour of @{text subst} is not specified.
       
   238 
       
   239   \item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the
       
   240   substitutions in the assumptions. The positions refer to the
       
   241   assumptions in order from left to right.  For example, given in a
       
   242   goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of
       
   243   commutativity of @{text "+"} is the subterm @{text "a + b"} and
       
   244   position 2 is the subterm @{text "c + d"}.
       
   245 
       
   246   \item @{method hypsubst} performs substitution using some
       
   247   assumption; this only works for equations of the form @{text "x =
       
   248   t"} where @{text x} is a free or bound variable.
       
   249 
       
   250   \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
       
   251   splitting using the given rules.  Splitting is performed in the
       
   252   conclusion or some assumption of the subgoal, depending of the
       
   253   structure of the rule.
       
   254   
       
   255   Note that the @{method simp} method already involves repeated
       
   256   application of split rules as declared in the current context, using
       
   257   @{attribute split}, for example.
       
   258 
       
   259   \end{description}
       
   260 *}
       
   261 
       
   262 
       
   263 subsection {* Further tactic emulations \label{sec:tactics} *}
       
   264 
       
   265 text {*
       
   266   The following improper proof methods emulate traditional tactics.
       
   267   These admit direct access to the goal state, which is normally
       
   268   considered harmful!  In particular, this may involve both numbered
       
   269   goal addressing (default 1), and dynamic instantiation within the
       
   270   scope of some subgoal.
       
   271 
       
   272   \begin{warn}
       
   273     Dynamic instantiations refer to universally quantified parameters
       
   274     of a subgoal (the dynamic context) rather than fixed variables and
       
   275     term abbreviations of a (static) Isar context.
       
   276   \end{warn}
       
   277 
       
   278   Tactic emulation methods, unlike their ML counterparts, admit
       
   279   simultaneous instantiation from both dynamic and static contexts.
       
   280   If names occur in both contexts goal parameters hide locally fixed
       
   281   variables.  Likewise, schematic variables refer to term
       
   282   abbreviations, if present in the static context.  Otherwise the
       
   283   schematic variable is interpreted as a schematic variable and left
       
   284   to be solved by unification with certain parts of the subgoal.
       
   285 
       
   286   Note that the tactic emulation proof methods in Isabelle/Isar are
       
   287   consistently named @{text foo_tac}.  Note also that variable names
       
   288   occurring on left hand sides of instantiations must be preceded by a
       
   289   question mark if they coincide with a keyword or contain dots.  This
       
   290   is consistent with the attribute @{attribute "where"} (see
       
   291   \secref{sec:pure-meth-att}).
       
   292 
       
   293   \begin{matharray}{rcl}
       
   294     @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
       
   295     @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
       
   296     @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
       
   297     @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
       
   298     @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
       
   299     @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
       
   300     @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
       
   301     @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
       
   302     @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
       
   303     @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
       
   304     @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
       
   305   \end{matharray}
       
   306 
       
   307   @{rail "
       
   308     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
       
   309       @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \\
       
   310     ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
       
   311     ;
       
   312     @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
       
   313     ;
       
   314     @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
       
   315     ;
       
   316     @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
       
   317     ;
       
   318     (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
       
   319     ;
       
   320 
       
   321     dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
       
   322   "}
       
   323 
       
   324 \begin{description}
       
   325 
       
   326   \item @{method rule_tac} etc. do resolution of rules with explicit
       
   327   instantiation.  This works the same way as the ML tactics @{ML
       
   328   res_inst_tac} etc. (see \cite{isabelle-implementation})
       
   329 
       
   330   Multiple rules may be only given if there is no instantiation; then
       
   331   @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
       
   332   \cite{isabelle-implementation}).
       
   333 
       
   334   \item @{method cut_tac} inserts facts into the proof state as
       
   335   assumption of a subgoal; instantiations may be given as well.  Note
       
   336   that the scope of schematic variables is spread over the main goal
       
   337   statement and rule premises are turned into new subgoals.  This is
       
   338   in contrast to the regular method @{method insert} which inserts
       
   339   closed rule statements.
       
   340 
       
   341   \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
       
   342   from a subgoal.  Note that @{text \<phi>} may contain schematic
       
   343   variables, to abbreviate the intended proposition; the first
       
   344   matching subgoal premise will be deleted.  Removing useless premises
       
   345   from a subgoal increases its readability and can make search tactics
       
   346   run faster.
       
   347 
       
   348   \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
       
   349   @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
       
   350   as new subgoals (in the original context).
       
   351 
       
   352   \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
       
   353   goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
       
   354   \emph{suffix} of variables.
       
   355 
       
   356   \item @{method rotate_tac}~@{text n} rotates the premises of a
       
   357   subgoal by @{text n} positions: from right to left if @{text n} is
       
   358   positive, and from left to right if @{text n} is negative; the
       
   359   default value is 1.
       
   360 
       
   361   \item @{method tactic}~@{text "text"} produces a proof method from
       
   362   any ML text of type @{ML_type tactic}.  Apart from the usual ML
       
   363   environment and the current proof context, the ML code may refer to
       
   364   the locally bound values @{ML_text facts}, which indicates any
       
   365   current facts used for forward-chaining.
       
   366 
       
   367   \item @{method raw_tactic} is similar to @{method tactic}, but
       
   368   presents the goal state in its raw internal form, where simultaneous
       
   369   subgoals appear as conjunction of the logical framework instead of
       
   370   the usual split into several subgoals.  While feature this is useful
       
   371   for debugging of complex method definitions, it should not never
       
   372   appear in production theories.
       
   373 
       
   374   \end{description}
       
   375 *}
       
   376 
       
   377 
       
   378 section {* The Simplifier \label{sec:simplifier} *}
       
   379 
       
   380 subsection {* Simplification methods *}
       
   381 
       
   382 text {*
       
   383   \begin{matharray}{rcl}
       
   384     @{method_def simp} & : & @{text method} \\
       
   385     @{method_def simp_all} & : & @{text method} \\
       
   386   \end{matharray}
       
   387 
       
   388   @{rail "
       
   389     (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
       
   390     ;
       
   391 
       
   392     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
       
   393     ;
       
   394     @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
       
   395       'split' (() | 'add' | 'del')) ':' @{syntax thmrefs}
       
   396   "}
       
   397 
       
   398   \begin{description}
       
   399 
       
   400   \item @{method simp} invokes the Simplifier, after declaring
       
   401   additional rules according to the arguments given.  Note that the
       
   402   @{text only} modifier first removes all other rewrite rules,
       
   403   congruences, and looper tactics (including splits), and then behaves
       
   404   like @{text add}.
       
   405 
       
   406   \medskip The @{text cong} modifiers add or delete Simplifier
       
   407   congruence rules (see also \secref{sec:simp-cong}), the default is
       
   408   to add.
       
   409 
       
   410   \medskip The @{text split} modifiers add or delete rules for the
       
   411   Splitter (see also \cite{isabelle-ref}), the default is to add.
       
   412   This works only if the Simplifier method has been properly setup to
       
   413   include the Splitter (all major object logics such HOL, HOLCF, FOL,
       
   414   ZF do this already).
       
   415 
       
   416   \item @{method simp_all} is similar to @{method simp}, but acts on
       
   417   all goals (backwards from the last to the first one).
       
   418 
       
   419   \end{description}
       
   420 
       
   421   By default the Simplifier methods take local assumptions fully into
       
   422   account, using equational assumptions in the subsequent
       
   423   normalization process, or simplifying assumptions themselves (cf.\
       
   424   @{ML asm_full_simp_tac} in \cite{isabelle-ref}).  In structured
       
   425   proofs this is usually quite well behaved in practice: just the
       
   426   local premises of the actual goal are involved, additional facts may
       
   427   be inserted via explicit forward-chaining (via @{command "then"},
       
   428   @{command "from"}, @{command "using"} etc.).
       
   429 
       
   430   Additional Simplifier options may be specified to tune the behavior
       
   431   further (mostly for unstructured scripts with many accidental local
       
   432   facts): ``@{text "(no_asm)"}'' means assumptions are ignored
       
   433   completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means
       
   434   assumptions are used in the simplification of the conclusion but are
       
   435   not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text
       
   436   "(no_asm_use)"}'' means assumptions are simplified but are not used
       
   437   in the simplification of each other or the conclusion (cf.\ @{ML
       
   438   full_simp_tac}).  For compatibility reasons, there is also an option
       
   439   ``@{text "(asm_lr)"}'', which means that an assumption is only used
       
   440   for simplifying assumptions which are to the right of it (cf.\ @{ML
       
   441   asm_lr_simp_tac}).
       
   442 
       
   443   The configuration option @{text "depth_limit"} limits the number of
       
   444   recursive invocations of the simplifier during conditional
       
   445   rewriting.
       
   446 
       
   447   \medskip The Splitter package is usually configured to work as part
       
   448   of the Simplifier.  The effect of repeatedly applying @{ML
       
   449   split_tac} can be simulated by ``@{text "(simp only: split:
       
   450   a\<^sub>1 \<dots> a\<^sub>n)"}''.  There is also a separate @{text split}
       
   451   method available for single-step case splitting.
       
   452 *}
       
   453 
       
   454 
       
   455 subsection {* Declaring rules *}
       
   456 
       
   457 text {*
       
   458   \begin{matharray}{rcl}
       
   459     @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
       
   460     @{attribute_def simp} & : & @{text attribute} \\
       
   461     @{attribute_def split} & : & @{text attribute} \\
       
   462   \end{matharray}
       
   463 
       
   464   @{rail "
       
   465     (@@{attribute simp} | @@{attribute split}) (() | 'add' | 'del')
       
   466   "}
       
   467 
       
   468   \begin{description}
       
   469 
       
   470   \item @{command "print_simpset"} prints the collection of rules
       
   471   declared to the Simplifier, which is also known as ``simpset''
       
   472   internally \cite{isabelle-ref}.
       
   473 
       
   474   \item @{attribute simp} declares simplification rules.
       
   475 
       
   476   \item @{attribute split} declares case split rules.
       
   477 
       
   478   \end{description}
       
   479 *}
       
   480 
       
   481 
       
   482 subsection {* Congruence rules\label{sec:simp-cong} *}
       
   483 
       
   484 text {*
       
   485   \begin{matharray}{rcl}
       
   486     @{attribute_def cong} & : & @{text attribute} \\
       
   487   \end{matharray}
       
   488 
       
   489   @{rail "
       
   490     @@{attribute cong} (() | 'add' | 'del')
       
   491   "}
       
   492 
       
   493   \begin{description}
       
   494 
       
   495   \item @{attribute cong} declares congruence rules to the Simplifier
       
   496   context.
       
   497 
       
   498   \end{description}
       
   499 
       
   500   Congruence rules are equalities of the form @{text [display]
       
   501   "\<dots> \<Longrightarrow> f ?x\<^sub>1 \<dots> ?x\<^sub>n = f ?y\<^sub>1 \<dots> ?y\<^sub>n"}
       
   502 
       
   503   This controls the simplification of the arguments of @{text f}.  For
       
   504   example, some arguments can be simplified under additional
       
   505   assumptions: @{text [display] "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow> (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow>
       
   506   (?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"}
       
   507 
       
   508   Given this rule, the simplifier assumes @{text "?Q\<^sub>1"} and extracts
       
   509   rewrite rules from it when simplifying @{text "?P\<^sub>2"}.  Such local
       
   510   assumptions are effective for rewriting formulae such as @{text "x =
       
   511   0 \<longrightarrow> y + x = y"}.
       
   512 
       
   513   %FIXME
       
   514   %The local assumptions are also provided as theorems to the solver;
       
   515   %see \secref{sec:simp-solver} below.
       
   516 
       
   517   \medskip The following congruence rule for bounded quantifiers also
       
   518   supplies contextual information --- about the bound variable:
       
   519   @{text [display] "(?A = ?B) \<Longrightarrow> (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow>
       
   520     (\<forall>x \<in> ?A. ?P x) \<longleftrightarrow> (\<forall>x \<in> ?B. ?Q x)"}
       
   521 
       
   522   \medskip This congruence rule for conditional expressions can
       
   523   supply contextual information for simplifying the arms:
       
   524   @{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow>
       
   525     (if ?p then ?a else ?b) = (if ?q then ?c else ?d)"}
       
   526 
       
   527   A congruence rule can also \emph{prevent} simplification of some
       
   528   arguments.  Here is an alternative congruence rule for conditional
       
   529   expressions that conforms to non-strict functional evaluation:
       
   530   @{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"}
       
   531 
       
   532   Only the first argument is simplified; the others remain unchanged.
       
   533   This can make simplification much faster, but may require an extra
       
   534   case split over the condition @{text "?q"} to prove the goal.
       
   535 *}
       
   536 
       
   537 
       
   538 subsection {* Simplification procedures *}
       
   539 
       
   540 text {* Simplification procedures are ML functions that produce proven
       
   541   rewrite rules on demand.  They are associated with higher-order
       
   542   patterns that approximate the left-hand sides of equations.  The
       
   543   Simplifier first matches the current redex against one of the LHS
       
   544   patterns; if this succeeds, the corresponding ML function is
       
   545   invoked, passing the Simplifier context and redex term.  Thus rules
       
   546   may be specifically fashioned for particular situations, resulting
       
   547   in a more powerful mechanism than term rewriting by a fixed set of
       
   548   rules.
       
   549 
       
   550   Any successful result needs to be a (possibly conditional) rewrite
       
   551   rule @{text "t \<equiv> u"} that is applicable to the current redex.  The
       
   552   rule will be applied just as any ordinary rewrite rule.  It is
       
   553   expected to be already in \emph{internal form}, bypassing the
       
   554   automatic preprocessing of object-level equivalences.
       
   555 
       
   556   \begin{matharray}{rcl}
       
   557     @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
       
   558     simproc & : & @{text attribute} \\
       
   559   \end{matharray}
       
   560 
       
   561   @{rail "
       
   562     @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
       
   563       @{syntax text} \\ (@'identifier' (@{syntax nameref}+))?
       
   564     ;
       
   565 
       
   566     @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
       
   567   "}
       
   568 
       
   569   \begin{description}
       
   570 
       
   571   \item @{command "simproc_setup"} defines a named simplification
       
   572   procedure that is invoked by the Simplifier whenever any of the
       
   573   given term patterns match the current redex.  The implementation,
       
   574   which is provided as ML source text, needs to be of type @{ML_type
       
   575   "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type
       
   576   cterm} represents the current redex @{text r} and the result is
       
   577   supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a
       
   578   generalized version), or @{ML NONE} to indicate failure.  The
       
   579   @{ML_type simpset} argument holds the full context of the current
       
   580   Simplifier invocation, including the actual Isar proof context.  The
       
   581   @{ML_type morphism} informs about the difference of the original
       
   582   compilation context wrt.\ the one of the actual application later
       
   583   on.  The optional @{keyword "identifier"} specifies theorems that
       
   584   represent the logical content of the abstract theory of this
       
   585   simproc.
       
   586 
       
   587   Morphisms and identifiers are only relevant for simprocs that are
       
   588   defined within a local target context, e.g.\ in a locale.
       
   589 
       
   590   \item @{text "simproc add: name"} and @{text "simproc del: name"}
       
   591   add or delete named simprocs to the current Simplifier context.  The
       
   592   default is to add a simproc.  Note that @{command "simproc_setup"}
       
   593   already adds the new simproc to the subsequent context.
       
   594 
       
   595   \end{description}
       
   596 *}
       
   597 
       
   598 
       
   599 subsubsection {* Example *}
       
   600 
       
   601 text {* The following simplification procedure for @{thm
       
   602   [source=false, show_types] unit_eq} in HOL performs fine-grained
       
   603   control over rule application, beyond higher-order pattern matching.
       
   604   Declaring @{thm unit_eq} as @{attribute simp} directly would make
       
   605   the simplifier loop!  Note that a version of this simplification
       
   606   procedure is already active in Isabelle/HOL.  *}
       
   607 
       
   608 simproc_setup unit ("x::unit") = {*
       
   609   fn _ => fn _ => fn ct =>
       
   610     if HOLogic.is_unit (term_of ct) then NONE
       
   611     else SOME (mk_meta_eq @{thm unit_eq})
       
   612 *}
       
   613 
       
   614 text {* Since the Simplifier applies simplification procedures
       
   615   frequently, it is important to make the failure check in ML
       
   616   reasonably fast. *}
       
   617 
       
   618 
       
   619 subsection {* Forward simplification *}
       
   620 
       
   621 text {*
       
   622   \begin{matharray}{rcl}
       
   623     @{attribute_def simplified} & : & @{text attribute} \\
       
   624   \end{matharray}
       
   625 
       
   626   @{rail "
       
   627     @@{attribute simplified} opt? @{syntax thmrefs}?
       
   628     ;
       
   629 
       
   630     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
       
   631   "}
       
   632 
       
   633   \begin{description}
       
   634   
       
   635   \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to
       
   636   be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,
       
   637   a\<^sub>n"}, or the implicit Simplifier context if no arguments are given.
       
   638   The result is fully simplified by default, including assumptions and
       
   639   conclusion; the options @{text no_asm} etc.\ tune the Simplifier in
       
   640   the same way as the for the @{text simp} method.
       
   641 
       
   642   Note that forward simplification restricts the simplifier to its
       
   643   most basic operation of term rewriting; solver and looper tactics
       
   644   \cite{isabelle-ref} are \emph{not} involved here.  The @{text
       
   645   simplified} attribute should be only rarely required under normal
       
   646   circumstances.
       
   647 
       
   648   \end{description}
       
   649 *}
       
   650 
       
   651 
       
   652 section {* The Classical Reasoner \label{sec:classical} *}
       
   653 
       
   654 subsection {* Basic concepts *}
       
   655 
       
   656 text {* Although Isabelle is generic, many users will be working in
       
   657   some extension of classical first-order logic.  Isabelle/ZF is built
       
   658   upon theory FOL, while Isabelle/HOL conceptually contains
       
   659   first-order logic as a fragment.  Theorem-proving in predicate logic
       
   660   is undecidable, but many automated strategies have been developed to
       
   661   assist in this task.
       
   662 
       
   663   Isabelle's classical reasoner is a generic package that accepts
       
   664   certain information about a logic and delivers a suite of automatic
       
   665   proof tools, based on rules that are classified and declared in the
       
   666   context.  These proof procedures are slow and simplistic compared
       
   667   with high-end automated theorem provers, but they can save
       
   668   considerable time and effort in practice.  They can prove theorems
       
   669   such as Pelletier's \cite{pelletier86} problems 40 and 41 in a few
       
   670   milliseconds (including full proof reconstruction): *}
       
   671 
       
   672 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)"
       
   673   by blast
       
   674 
       
   675 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)"
       
   676   by blast
       
   677 
       
   678 text {* The proof tools are generic.  They are not restricted to
       
   679   first-order logic, and have been heavily used in the development of
       
   680   the Isabelle/HOL library and applications.  The tactics can be
       
   681   traced, and their components can be called directly; in this manner,
       
   682   any proof can be viewed interactively.  *}
       
   683 
       
   684 
       
   685 subsubsection {* The sequent calculus *}
       
   686 
       
   687 text {* Isabelle supports natural deduction, which is easy to use for
       
   688   interactive proof.  But natural deduction does not easily lend
       
   689   itself to automation, and has a bias towards intuitionism.  For
       
   690   certain proofs in classical logic, it can not be called natural.
       
   691   The \emph{sequent calculus}, a generalization of natural deduction,
       
   692   is easier to automate.
       
   693 
       
   694   A \textbf{sequent} has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"}
       
   695   and @{text "\<Delta>"} are sets of formulae.\footnote{For first-order
       
   696   logic, sequents can equivalently be made from lists or multisets of
       
   697   formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is
       
   698   \textbf{valid} if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or>
       
   699   Q\<^sub>n"}.  Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which
       
   700   is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals.  A
       
   701   sequent is \textbf{basic} if its left and right sides have a common
       
   702   formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially
       
   703   valid.
       
   704 
       
   705   Sequent rules are classified as \textbf{right} or \textbf{left},
       
   706   indicating which side of the @{text "\<turnstile>"} symbol they operate on.
       
   707   Rules that operate on the right side are analogous to natural
       
   708   deduction's introduction rules, and left rules are analogous to
       
   709   elimination rules.  The sequent calculus analogue of @{text "(\<longrightarrow>I)"}
       
   710   is the rule
       
   711   \[
       
   712   \infer[@{text "(\<longrightarrow>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<longrightarrow> Q"}}{@{text "P, \<Gamma> \<turnstile> \<Delta>, Q"}}
       
   713   \]
       
   714   Applying the rule backwards, this breaks down some implication on
       
   715   the right side of a sequent; @{text "\<Gamma>"} and @{text "\<Delta>"} stand for
       
   716   the sets of formulae that are unaffected by the inference.  The
       
   717   analogue of the pair @{text "(\<or>I1)"} and @{text "(\<or>I2)"} is the
       
   718   single rule
       
   719   \[
       
   720   \infer[@{text "(\<or>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<or> Q"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P, Q"}}
       
   721   \]
       
   722   This breaks down some disjunction on the right side, replacing it by
       
   723   both disjuncts.  Thus, the sequent calculus is a kind of
       
   724   multiple-conclusion logic.
       
   725 
       
   726   To illustrate the use of multiple formulae on the right, let us
       
   727   prove the classical theorem @{text "(P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}.  Working
       
   728   backwards, we reduce this formula to a basic sequent:
       
   729   \[
       
   730   \infer[@{text "(\<or>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}}
       
   731     {\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q), (Q \<longrightarrow> P)"}}
       
   732       {\infer[@{text "(\<longrightarrow>R)"}]{@{text "P \<turnstile> Q, (Q \<longrightarrow> P)"}}
       
   733         {@{text "P, Q \<turnstile> Q, P"}}}}
       
   734   \]
       
   735 
       
   736   This example is typical of the sequent calculus: start with the
       
   737   desired theorem and apply rules backwards in a fairly arbitrary
       
   738   manner.  This yields a surprisingly effective proof procedure.
       
   739   Quantifiers add only few complications, since Isabelle handles
       
   740   parameters and schematic variables.  See \cite[Chapter
       
   741   10]{paulson-ml2} for further discussion.  *}
       
   742 
       
   743 
       
   744 subsubsection {* Simulating sequents by natural deduction *}
       
   745 
       
   746 text {* Isabelle can represent sequents directly, as in the
       
   747   object-logic LK.  But natural deduction is easier to work with, and
       
   748   most object-logics employ it.  Fortunately, we can simulate the
       
   749   sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} by the Isabelle formula
       
   750   @{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
       
   751   the assumptions and the choice of @{text "Q\<^sub>1"} are arbitrary.
       
   752   Elim-resolution plays a key role in simulating sequent proofs.
       
   753 
       
   754   We can easily handle reasoning on the left.  Elim-resolution with
       
   755   the rules @{text "(\<or>E)"}, @{text "(\<bottom>E)"} and @{text "(\<exists>E)"} achieves
       
   756   a similar effect as the corresponding sequent rules.  For the other
       
   757   connectives, we use sequent-style elimination rules instead of
       
   758   destruction rules such as @{text "(\<and>E1, 2)"} and @{text "(\<forall>E)"}.
       
   759   But note that the rule @{text "(\<not>L)"} has no effect under our
       
   760   representation of sequents!
       
   761   \[
       
   762   \infer[@{text "(\<not>L)"}]{@{text "\<not> P, \<Gamma> \<turnstile> \<Delta>"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P"}}
       
   763   \]
       
   764 
       
   765   What about reasoning on the right?  Introduction rules can only
       
   766   affect the formula in the conclusion, namely @{text "Q\<^sub>1"}.  The
       
   767   other right-side formulae are represented as negated assumptions,
       
   768   @{text "\<not> Q\<^sub>2, \<dots>, \<not> Q\<^sub>n"}.  In order to operate on one of these, it
       
   769   must first be exchanged with @{text "Q\<^sub>1"}.  Elim-resolution with the
       
   770   @{text swap} rule has this effect: @{text "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"}
       
   771 
       
   772   To ensure that swaps occur only when necessary, each introduction
       
   773   rule is converted into a swapped form: it is resolved with the
       
   774   second premise of @{text "(swap)"}.  The swapped form of @{text
       
   775   "(\<and>I)"}, which might be called @{text "(\<not>\<and>E)"}, is
       
   776   @{text [display] "\<not> (P \<and> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (\<not> R \<Longrightarrow> Q) \<Longrightarrow> R"}
       
   777 
       
   778   Similarly, the swapped form of @{text "(\<longrightarrow>I)"} is
       
   779   @{text [display] "\<not> (P \<longrightarrow> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P \<Longrightarrow> Q) \<Longrightarrow> R"}
       
   780 
       
   781   Swapped introduction rules are applied using elim-resolution, which
       
   782   deletes the negated formula.  Our representation of sequents also
       
   783   requires the use of ordinary introduction rules.  If we had no
       
   784   regard for readability of intermediate goal states, we could treat
       
   785   the right side more uniformly by representing sequents as @{text
       
   786   [display] "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> \<bottom>"}
       
   787 *}
       
   788 
       
   789 
       
   790 subsubsection {* Extra rules for the sequent calculus *}
       
   791 
       
   792 text {* As mentioned, destruction rules such as @{text "(\<and>E1, 2)"} and
       
   793   @{text "(\<forall>E)"} must be replaced by sequent-style elimination rules.
       
   794   In addition, we need rules to embody the classical equivalence
       
   795   between @{text "P \<longrightarrow> Q"} and @{text "\<not> P \<or> Q"}.  The introduction
       
   796   rules @{text "(\<or>I1, 2)"} are replaced by a rule that simulates
       
   797   @{text "(\<or>R)"}: @{text [display] "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"}
       
   798 
       
   799   The destruction rule @{text "(\<longrightarrow>E)"} is replaced by @{text [display]
       
   800   "(P \<longrightarrow> Q) \<Longrightarrow> (\<not> P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"}
       
   801 
       
   802   Quantifier replication also requires special rules.  In classical
       
   803   logic, @{text "\<exists>x. P x"} is equivalent to @{text "\<not> (\<forall>x. \<not> P x)"};
       
   804   the rules @{text "(\<exists>R)"} and @{text "(\<forall>L)"} are dual:
       
   805   \[
       
   806   \infer[@{text "(\<exists>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x"}}{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x, P t"}}
       
   807   \qquad
       
   808   \infer[@{text "(\<forall>L)"}]{@{text "\<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}{@{text "P t, \<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}
       
   809   \]
       
   810   Thus both kinds of quantifier may be replicated.  Theorems requiring
       
   811   multiple uses of a universal formula are easy to invent; consider
       
   812   @{text [display] "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P a \<longrightarrow> P (f\<^sup>n a)"} for any
       
   813   @{text "n > 1"}.  Natural examples of the multiple use of an
       
   814   existential formula are rare; a standard one is @{text "\<exists>x. \<forall>y. P x
       
   815   \<longrightarrow> P y"}.
       
   816 
       
   817   Forgoing quantifier replication loses completeness, but gains
       
   818   decidability, since the search space becomes finite.  Many useful
       
   819   theorems can be proved without replication, and the search generally
       
   820   delivers its verdict in a reasonable time.  To adopt this approach,
       
   821   represent the sequent rules @{text "(\<exists>R)"}, @{text "(\<exists>L)"} and
       
   822   @{text "(\<forall>R)"} by @{text "(\<exists>I)"}, @{text "(\<exists>E)"} and @{text "(\<forall>I)"},
       
   823   respectively, and put @{text "(\<forall>E)"} into elimination form: @{text
       
   824   [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"}
       
   825 
       
   826   Elim-resolution with this rule will delete the universal formula
       
   827   after a single use.  To replicate universal quantifiers, replace the
       
   828   rule by @{text [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"}
       
   829 
       
   830   To replicate existential quantifiers, replace @{text "(\<exists>I)"} by
       
   831   @{text [display] "(\<not> (\<exists>x. P x) \<Longrightarrow> P t) \<Longrightarrow> \<exists>x. P x"}
       
   832 
       
   833   All introduction rules mentioned above are also useful in swapped
       
   834   form.
       
   835 
       
   836   Replication makes the search space infinite; we must apply the rules
       
   837   with care.  The classical reasoner distinguishes between safe and
       
   838   unsafe rules, applying the latter only when there is no alternative.
       
   839   Depth-first search may well go down a blind alley; best-first search
       
   840   is better behaved in an infinite search space.  However, quantifier
       
   841   replication is too expensive to prove any but the simplest theorems.
       
   842 *}
       
   843 
       
   844 
       
   845 subsection {* Rule declarations *}
       
   846 
       
   847 text {* The proof tools of the Classical Reasoner depend on
       
   848   collections of rules declared in the context, which are classified
       
   849   as introduction, elimination or destruction and as \emph{safe} or
       
   850   \emph{unsafe}.  In general, safe rules can be attempted blindly,
       
   851   while unsafe rules must be used with care.  A safe rule must never
       
   852   reduce a provable goal to an unprovable set of subgoals.
       
   853 
       
   854   The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P
       
   855   \<or> Q"} to @{text "P"}, which might turn out as premature choice of an
       
   856   unprovable subgoal.  Any rule is unsafe whose premises contain new
       
   857   unknowns.  The elimination rule @{text "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} is
       
   858   unsafe, since it is applied via elim-resolution, which discards the
       
   859   assumption @{text "\<forall>x. P x"} and replaces it by the weaker
       
   860   assumption @{text "P t"}.  The rule @{text "P t \<Longrightarrow> \<exists>x. P x"} is
       
   861   unsafe for similar reasons.  The quantifier duplication rule @{text
       
   862   "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} is unsafe in a different sense:
       
   863   since it keeps the assumption @{text "\<forall>x. P x"}, it is prone to
       
   864   looping.  In classical first-order logic, all rules are safe except
       
   865   those mentioned above.
       
   866 
       
   867   The safe~/ unsafe distinction is vague, and may be regarded merely
       
   868   as a way of giving some rules priority over others.  One could argue
       
   869   that @{text "(\<or>E)"} is unsafe, because repeated application of it
       
   870   could generate exponentially many subgoals.  Induction rules are
       
   871   unsafe because inductive proofs are difficult to set up
       
   872   automatically.  Any inference is unsafe that instantiates an unknown
       
   873   in the proof state --- thus matching must be used, rather than
       
   874   unification.  Even proof by assumption is unsafe if it instantiates
       
   875   unknowns shared with other subgoals.
       
   876 
       
   877   \begin{matharray}{rcl}
       
   878     @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
       
   879     @{attribute_def intro} & : & @{text attribute} \\
       
   880     @{attribute_def elim} & : & @{text attribute} \\
       
   881     @{attribute_def dest} & : & @{text attribute} \\
       
   882     @{attribute_def rule} & : & @{text attribute} \\
       
   883     @{attribute_def iff} & : & @{text attribute} \\
       
   884     @{attribute_def swapped} & : & @{text attribute} \\
       
   885   \end{matharray}
       
   886 
       
   887   @{rail "
       
   888     (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
       
   889     ;
       
   890     @@{attribute rule} 'del'
       
   891     ;
       
   892     @@{attribute iff} (((() | 'add') '?'?) | 'del')
       
   893   "}
       
   894 
       
   895   \begin{description}
       
   896 
       
   897   \item @{command "print_claset"} prints the collection of rules
       
   898   declared to the Classical Reasoner, i.e.\ the @{ML_type claset}
       
   899   within the context.
       
   900 
       
   901   \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
       
   902   declare introduction, elimination, and destruction rules,
       
   903   respectively.  By default, rules are considered as \emph{unsafe}
       
   904   (i.e.\ not applied blindly without backtracking), while ``@{text
       
   905   "!"}'' classifies as \emph{safe}.  Rule declarations marked by
       
   906   ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
       
   907   \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
       
   908   of the @{method rule} method).  The optional natural number
       
   909   specifies an explicit weight argument, which is ignored by the
       
   910   automated reasoning tools, but determines the search order of single
       
   911   rule steps.
       
   912 
       
   913   Introduction rules are those that can be applied using ordinary
       
   914   resolution.  Their swapped forms are generated internally, which
       
   915   will be applied using elim-resolution.  Elimination rules are
       
   916   applied using elim-resolution.  Rules are sorted by the number of
       
   917   new subgoals they will yield; rules that generate the fewest
       
   918   subgoals will be tried first.  Otherwise, later declarations take
       
   919   precedence over earlier ones.
       
   920 
       
   921   Rules already present in the context with the same classification
       
   922   are ignored.  A warning is printed if the rule has already been
       
   923   added with some other classification, but the rule is added anyway
       
   924   as requested.
       
   925 
       
   926   \item @{attribute rule}~@{text del} deletes all occurrences of a
       
   927   rule from the classical context, regardless of its classification as
       
   928   introduction~/ elimination~/ destruction and safe~/ unsafe.
       
   929 
       
   930   \item @{attribute iff} declares logical equivalences to the
       
   931   Simplifier and the Classical reasoner at the same time.
       
   932   Non-conditional rules result in a safe introduction and elimination
       
   933   pair; conditional ones are considered unsafe.  Rules with negative
       
   934   conclusion are automatically inverted (using @{text "\<not>"}-elimination
       
   935   internally).
       
   936 
       
   937   The ``@{text "?"}'' version of @{attribute iff} declares rules to
       
   938   the Isabelle/Pure context only, and omits the Simplifier
       
   939   declaration.
       
   940 
       
   941   \item @{attribute swapped} turns an introduction rule into an
       
   942   elimination, by resolving with the classical swap principle @{text
       
   943   "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position.  This is mainly for
       
   944   illustrative purposes: the Classical Reasoner already swaps rules
       
   945   internally as explained above.
       
   946 
       
   947   \end{description}
       
   948 *}
       
   949 
       
   950 
       
   951 subsection {* Structured methods *}
       
   952 
       
   953 text {*
       
   954   \begin{matharray}{rcl}
       
   955     @{method_def rule} & : & @{text method} \\
       
   956     @{method_def contradiction} & : & @{text method} \\
       
   957   \end{matharray}
       
   958 
       
   959   @{rail "
       
   960     @@{method rule} @{syntax thmrefs}?
       
   961   "}
       
   962 
       
   963   \begin{description}
       
   964 
       
   965   \item @{method rule} as offered by the Classical Reasoner is a
       
   966   refinement over the Pure one (see \secref{sec:pure-meth-att}).  Both
       
   967   versions work the same, but the classical version observes the
       
   968   classical rule context in addition to that of Isabelle/Pure.
       
   969 
       
   970   Common object logics (HOL, ZF, etc.) declare a rich collection of
       
   971   classical rules (even if these would qualify as intuitionistic
       
   972   ones), but only few declarations to the rule context of
       
   973   Isabelle/Pure (\secref{sec:pure-meth-att}).
       
   974 
       
   975   \item @{method contradiction} solves some goal by contradiction,
       
   976   deriving any result from both @{text "\<not> A"} and @{text A}.  Chained
       
   977   facts, which are guaranteed to participate, may appear in either
       
   978   order.
       
   979 
       
   980   \end{description}
       
   981 *}
       
   982 
       
   983 
       
   984 subsection {* Automated methods *}
       
   985 
       
   986 text {*
       
   987   \begin{matharray}{rcl}
       
   988     @{method_def blast} & : & @{text method} \\
       
   989     @{method_def auto} & : & @{text method} \\
       
   990     @{method_def force} & : & @{text method} \\
       
   991     @{method_def fast} & : & @{text method} \\
       
   992     @{method_def slow} & : & @{text method} \\
       
   993     @{method_def best} & : & @{text method} \\
       
   994     @{method_def fastforce} & : & @{text method} \\
       
   995     @{method_def slowsimp} & : & @{text method} \\
       
   996     @{method_def bestsimp} & : & @{text method} \\
       
   997     @{method_def deepen} & : & @{text method} \\
       
   998   \end{matharray}
       
   999 
       
  1000   @{rail "
       
  1001     @@{method blast} @{syntax nat}? (@{syntax clamod} * )
       
  1002     ;
       
  1003     @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )
       
  1004     ;
       
  1005     @@{method force} (@{syntax clasimpmod} * )
       
  1006     ;
       
  1007     (@@{method fast} | @@{method slow} | @@{method best}) (@{syntax clamod} * )
       
  1008     ;
       
  1009     (@@{method fastforce} | @@{method slowsimp} | @@{method bestsimp})
       
  1010       (@{syntax clasimpmod} * )
       
  1011     ;
       
  1012     @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
       
  1013     ;
       
  1014     @{syntax_def clamod}:
       
  1015       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
       
  1016     ;
       
  1017     @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
       
  1018       ('cong' | 'split') (() | 'add' | 'del') |
       
  1019       'iff' (((() | 'add') '?'?) | 'del') |
       
  1020       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
       
  1021   "}
       
  1022 
       
  1023   \begin{description}
       
  1024 
       
  1025   \item @{method blast} is a separate classical tableau prover that
       
  1026   uses the same classical rule declarations as explained before.
       
  1027 
       
  1028   Proof search is coded directly in ML using special data structures.
       
  1029   A successful proof is then reconstructed using regular Isabelle
       
  1030   inferences.  It is faster and more powerful than the other classical
       
  1031   reasoning tools, but has major limitations too.
       
  1032 
       
  1033   \begin{itemize}
       
  1034 
       
  1035   \item It does not use the classical wrapper tacticals, such as the
       
  1036   integration with the Simplifier of @{method fastforce}.
       
  1037 
       
  1038   \item It does not perform higher-order unification, as needed by the
       
  1039   rule @{thm [source=false] rangeI} in HOL.  There are often
       
  1040   alternatives to such rules, for example @{thm [source=false]
       
  1041   range_eqI}.
       
  1042 
       
  1043   \item Function variables may only be applied to parameters of the
       
  1044   subgoal.  (This restriction arises because the prover does not use
       
  1045   higher-order unification.)  If other function variables are present
       
  1046   then the prover will fail with the message \texttt{Function Var's
       
  1047   argument not a bound variable}.
       
  1048 
       
  1049   \item Its proof strategy is more general than @{method fast} but can
       
  1050   be slower.  If @{method blast} fails or seems to be running forever,
       
  1051   try @{method fast} and the other proof tools described below.
       
  1052 
       
  1053   \end{itemize}
       
  1054 
       
  1055   The optional integer argument specifies a bound for the number of
       
  1056   unsafe steps used in a proof.  By default, @{method blast} starts
       
  1057   with a bound of 0 and increases it successively to 20.  In contrast,
       
  1058   @{text "(blast lim)"} tries to prove the goal using a search bound
       
  1059   of @{text "lim"}.  Sometimes a slow proof using @{method blast} can
       
  1060   be made much faster by supplying the successful search bound to this
       
  1061   proof method instead.
       
  1062 
       
  1063   \item @{method auto} combines classical reasoning with
       
  1064   simplification.  It is intended for situations where there are a lot
       
  1065   of mostly trivial subgoals; it proves all the easy ones, leaving the
       
  1066   ones it cannot prove.  Occasionally, attempting to prove the hard
       
  1067   ones may take a long time.
       
  1068 
       
  1069   The optional depth arguments in @{text "(auto m n)"} refer to its
       
  1070   builtin classical reasoning procedures: @{text m} (default 4) is for
       
  1071   @{method blast}, which is tried first, and @{text n} (default 2) is
       
  1072   for a slower but more general alternative that also takes wrappers
       
  1073   into account.
       
  1074 
       
  1075   \item @{method force} is intended to prove the first subgoal
       
  1076   completely, using many fancy proof tools and performing a rather
       
  1077   exhaustive search.  As a result, proof attempts may take rather long
       
  1078   or diverge easily.
       
  1079 
       
  1080   \item @{method fast}, @{method best}, @{method slow} attempt to
       
  1081   prove the first subgoal using sequent-style reasoning as explained
       
  1082   before.  Unlike @{method blast}, they construct proofs directly in
       
  1083   Isabelle.
       
  1084 
       
  1085   There is a difference in search strategy and back-tracking: @{method
       
  1086   fast} uses depth-first search and @{method best} uses best-first
       
  1087   search (guided by a heuristic function: normally the total size of
       
  1088   the proof state).
       
  1089 
       
  1090   Method @{method slow} is like @{method fast}, but conducts a broader
       
  1091   search: it may, when backtracking from a failed proof attempt, undo
       
  1092   even the step of proving a subgoal by assumption.
       
  1093 
       
  1094   \item @{method fastforce}, @{method slowsimp}, @{method bestsimp}
       
  1095   are like @{method fast}, @{method slow}, @{method best},
       
  1096   respectively, but use the Simplifier as additional wrapper. The name
       
  1097   @{method fastforce}, reflects the behaviour of this popular method
       
  1098   better without requiring an understanding of its implementation.
       
  1099 
       
  1100   \item @{method deepen} works by exhaustive search up to a certain
       
  1101   depth.  The start depth is 4 (unless specified explicitly), and the
       
  1102   depth is increased iteratively up to 10.  Unsafe rules are modified
       
  1103   to preserve the formula they act on, so that it be used repeatedly.
       
  1104   This method can prove more goals than @{method fast}, but is much
       
  1105   slower, for example if the assumptions have many universal
       
  1106   quantifiers.
       
  1107 
       
  1108   \end{description}
       
  1109 
       
  1110   Any of the above methods support additional modifiers of the context
       
  1111   of classical (and simplifier) rules, but the ones related to the
       
  1112   Simplifier are explicitly prefixed by @{text simp} here.  The
       
  1113   semantics of these ad-hoc rule declarations is analogous to the
       
  1114   attributes given before.  Facts provided by forward chaining are
       
  1115   inserted into the goal before commencing proof search.
       
  1116 *}
       
  1117 
       
  1118 
       
  1119 subsection {* Semi-automated methods *}
       
  1120 
       
  1121 text {* These proof methods may help in situations when the
       
  1122   fully-automated tools fail.  The result is a simpler subgoal that
       
  1123   can be tackled by other means, such as by manual instantiation of
       
  1124   quantifiers.
       
  1125 
       
  1126   \begin{matharray}{rcl}
       
  1127     @{method_def safe} & : & @{text method} \\
       
  1128     @{method_def clarify} & : & @{text method} \\
       
  1129     @{method_def clarsimp} & : & @{text method} \\
       
  1130   \end{matharray}
       
  1131 
       
  1132   @{rail "
       
  1133     (@@{method safe} | @@{method clarify}) (@{syntax clamod} * )
       
  1134     ;
       
  1135     @@{method clarsimp} (@{syntax clasimpmod} * )
       
  1136   "}
       
  1137 
       
  1138   \begin{description}
       
  1139 
       
  1140   \item @{method safe} repeatedly performs safe steps on all subgoals.
       
  1141   It is deterministic, with at most one outcome.
       
  1142 
       
  1143   \item @{method clarify} performs a series of safe steps without
       
  1144   splitting subgoals; see also @{ML clarify_step_tac}.
       
  1145 
       
  1146   \item @{method clarsimp} acts like @{method clarify}, but also does
       
  1147   simplification.  Note that if the Simplifier context includes a
       
  1148   splitter for the premises, the subgoal may still be split.
       
  1149 
       
  1150   \end{description}
       
  1151 *}
       
  1152 
       
  1153 
       
  1154 subsection {* Single-step tactics *}
       
  1155 
       
  1156 text {*
       
  1157   \begin{matharray}{rcl}
       
  1158     @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\
       
  1159     @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\
       
  1160     @{index_ML step_tac: "Proof.context -> int -> tactic"} \\
       
  1161     @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\
       
  1162     @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
       
  1163   \end{matharray}
       
  1164 
       
  1165   These are the primitive tactics behind the (semi)automated proof
       
  1166   methods of the Classical Reasoner.  By calling them yourself, you
       
  1167   can execute these procedures one step at a time.
       
  1168 
       
  1169   \begin{description}
       
  1170 
       
  1171   \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on
       
  1172   subgoal @{text i}.  The safe wrapper tacticals are applied to a
       
  1173   tactic that may include proof by assumption or Modus Ponens (taking
       
  1174   care not to instantiate unknowns), or substitution.
       
  1175 
       
  1176   \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows
       
  1177   unknowns to be instantiated.
       
  1178 
       
  1179   \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof
       
  1180   procedure.  The unsafe wrapper tacticals are applied to a tactic
       
  1181   that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe
       
  1182   rule from the context.
       
  1183 
       
  1184   \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows
       
  1185   backtracking between using safe rules with instantiation (@{ML
       
  1186   inst_step_tac}) and using unsafe rules.  The resulting search space
       
  1187   is larger.
       
  1188 
       
  1189   \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step
       
  1190   on subgoal @{text i}.  No splitting step is applied; for example,
       
  1191   the subgoal @{text "A \<and> B"} is left as a conjunction.  Proof by
       
  1192   assumption, Modus Ponens, etc., may be performed provided they do
       
  1193   not instantiate unknowns.  Assumptions of the form @{text "x = t"}
       
  1194   may be eliminated.  The safe wrapper tactical is applied.
       
  1195 
       
  1196   \end{description}
       
  1197 *}
       
  1198 
       
  1199 
       
  1200 section {* Object-logic setup \label{sec:object-logic} *}
       
  1201 
       
  1202 text {*
       
  1203   \begin{matharray}{rcl}
       
  1204     @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\
       
  1205     @{method_def atomize} & : & @{text method} \\
       
  1206     @{attribute_def atomize} & : & @{text attribute} \\
       
  1207     @{attribute_def rule_format} & : & @{text attribute} \\
       
  1208     @{attribute_def rulify} & : & @{text attribute} \\
       
  1209   \end{matharray}
       
  1210 
       
  1211   The very starting point for any Isabelle object-logic is a ``truth
       
  1212   judgment'' that links object-level statements to the meta-logic
       
  1213   (with its minimal language of @{text prop} that covers universal
       
  1214   quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).
       
  1215 
       
  1216   Common object-logics are sufficiently expressive to internalize rule
       
  1217   statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own
       
  1218   language.  This is useful in certain situations where a rule needs
       
  1219   to be viewed as an atomic statement from the meta-level perspective,
       
  1220   e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.
       
  1221 
       
  1222   From the following language elements, only the @{method atomize}
       
  1223   method and @{attribute rule_format} attribute are occasionally
       
  1224   required by end-users, the rest is for those who need to setup their
       
  1225   own object-logic.  In the latter case existing formulations of
       
  1226   Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
       
  1227 
       
  1228   Generic tools may refer to the information provided by object-logic
       
  1229   declarations internally.
       
  1230 
       
  1231   @{rail "
       
  1232     @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}?
       
  1233     ;
       
  1234     @@{attribute atomize} ('(' 'full' ')')?
       
  1235     ;
       
  1236     @@{attribute rule_format} ('(' 'noasm' ')')?
       
  1237   "}
       
  1238 
       
  1239   \begin{description}
       
  1240   
       
  1241   \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant
       
  1242   @{text c} as the truth judgment of the current object-logic.  Its
       
  1243   type @{text \<sigma>} should specify a coercion of the category of
       
  1244   object-level propositions to @{text prop} of the Pure meta-logic;
       
  1245   the mixfix annotation @{text "(mx)"} would typically just link the
       
  1246   object language (internally of syntactic category @{text logic})
       
  1247   with that of @{text prop}.  Only one @{command "judgment"}
       
  1248   declaration may be given in any theory development.
       
  1249   
       
  1250   \item @{method atomize} (as a method) rewrites any non-atomic
       
  1251   premises of a sub-goal, using the meta-level equations declared via
       
  1252   @{attribute atomize} (as an attribute) beforehand.  As a result,
       
  1253   heavily nested goals become amenable to fundamental operations such
       
  1254   as resolution (cf.\ the @{method (Pure) rule} method).  Giving the ``@{text
       
  1255   "(full)"}'' option here means to turn the whole subgoal into an
       
  1256   object-statement (if possible), including the outermost parameters
       
  1257   and assumptions as well.
       
  1258 
       
  1259   A typical collection of @{attribute atomize} rules for a particular
       
  1260   object-logic would provide an internalization for each of the
       
  1261   connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.
       
  1262   Meta-level conjunction should be covered as well (this is
       
  1263   particularly important for locales, see \secref{sec:locale}).
       
  1264 
       
  1265   \item @{attribute rule_format} rewrites a theorem by the equalities
       
  1266   declared as @{attribute rulify} rules in the current object-logic.
       
  1267   By default, the result is fully normalized, including assumptions
       
  1268   and conclusions at any depth.  The @{text "(no_asm)"} option
       
  1269   restricts the transformation to the conclusion of a rule.
       
  1270 
       
  1271   In common object-logics (HOL, FOL, ZF), the effect of @{attribute
       
  1272   rule_format} is to replace (bounded) universal quantification
       
  1273   (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
       
  1274   rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.
       
  1275 
       
  1276   \end{description}
       
  1277 *}
       
  1278 
       
  1279 end