doc-src/IsarImplementation/Thy/unused.thy
author wenzelm
Mon Sep 04 19:49:39 2006 +0200 (2006-09-04 ago)
changeset 20474 af069653f1d7
parent 20470 c839b38a1f32
child 20477 e623b0e30541
permissions -rw-r--r--
tuned;
     1 
     2 text {*
     3 
     4 
     5   \medskip The general concept supports block-structured reasoning
     6   nicely, with arbitrary mechanisms for introducing local assumptions.
     7   The common reasoning pattern is as follows:
     8 
     9   \medskip
    10   \begin{tabular}{l}
    11   @{text "add_assms e\<^isub>1 A\<^isub>1"} \\
    12   @{text "\<dots>"} \\
    13   @{text "add_assms e\<^isub>n A\<^isub>n"} \\
    14   @{text "export"} \\
    15   \end{tabular}
    16   \medskip
    17 
    18   \noindent The final @{text "export"} will turn any fact @{text
    19   "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} into some @{text "\<turnstile> B'"}, by
    20   applying the export rules @{text "e\<^isub>1, \<dots>, e\<^isub>n"}
    21   inside-out.
    22   
    23 
    24   A \emph{fixed variable} acts like a local constant in the current
    25   context, representing some simple type @{text "\<alpha>"}, or some value
    26   @{text "x: \<tau>"} (for a fixed type expression @{text "\<tau>"}).  A
    27   \emph{schematic variable} acts like a placeholder for arbitrary
    28   elements, similar to outermost quantification.  The division between
    29   fixed and schematic variables tells which abstract entities are
    30   inside and outside the current context.
    31 
    32 
    33   @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
    34 
    35 
    36 
    37   \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML
    38   Variable.export}, i.e.\ it provides a view on facts with all
    39   variables being fixed in the current context.
    40 
    41 
    42   In practice, super-contexts emerge either by merging existing ones,
    43   or by adding explicit declarations.  For example, new theories are
    44   usually derived by importing existing theories from the library
    45   @{text "\<Theta> = \<Theta>\<^sub>1 + \<dots> + \<Theta>\<^isub>n"}, or 
    46 
    47 
    48 
    49   The Isar toplevel works differently for interactive developments
    50   vs.\ batch processing of theory sources.  For example, diagnostic
    51   commands produce a warning batch mode, because they are considered
    52   alien to the final theory document being produced eventually.
    53   Moreover, full @{text undo} with intermediate checkpoints to protect
    54   against destroying theories accidentally are limited to interactive
    55   mode.  In batch mode there is only a single strictly linear stream
    56   of potentially desctructive theory transformations.
    57 
    58   \item @{ML Toplevel.empty} is an empty transition; the Isar command
    59   dispatcher internally applies @{ML Toplevel.name} (for the command)
    60   name and @{ML Toplevel.position} for the source position.
    61 
    62 *}
    63