doc-src/IsarImplementation/Thy/proof.thy
author wenzelm
Sat, 08 Jul 2006 14:01:40 +0200
changeset 20064 92aad017b847
parent 20041 ae7aba935986
child 20171 424739228123
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     1
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     2
(* $Id$ *)
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     3
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
theory "proof" imports base begin
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     5
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
chapter {* Structured reasoning *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     7
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     8
section {* Proof context *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     9
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    10
subsection {* Local variables *}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    11
20064
wenzelm
parents: 20041
diff changeset
    12
text FIXME
wenzelm
parents: 20041
diff changeset
    13
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    14
text %mlref {*
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    15
  \begin{mldecls}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    16
  @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
20064
wenzelm
parents: 20041
diff changeset
    17
  @{index_ML Variable.add_fixes: "string list -> Proof.context -> string list * Proof.context"} \\
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    18
  @{index_ML Variable.import: "bool -> thm list -> Proof.context -> thm list * Proof.context"} \\
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    19
  @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    20
  @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    21
  @{index_ML Variable.monomorphic: "Proof.context -> term list -> term list"} \\
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    22
  @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    23
  \end{mldecls}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    24
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    25
  \begin{description}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    26
20064
wenzelm
parents: 20041
diff changeset
    27
  \item @{ML Variable.declare_term}~@{text "t ctxt"} declares term
wenzelm
parents: 20041
diff changeset
    28
  @{text "t"} to belong to the context.  This fixes free type
wenzelm
parents: 20041
diff changeset
    29
  variables, but not term variables.  Constraints for type and term
wenzelm
parents: 20041
diff changeset
    30
  variables are declared uniformly.
wenzelm
parents: 20041
diff changeset
    31
wenzelm
parents: 20041
diff changeset
    32
  \item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term
wenzelm
parents: 20041
diff changeset
    33
  variables @{text "xs"} and returns the internal names of the
wenzelm
parents: 20041
diff changeset
    34
  resulting Skolem constants.  Note that term fixes refer to
wenzelm
parents: 20041
diff changeset
    35
  \emph{all} type instances that may occur in the future.
wenzelm
parents: 20041
diff changeset
    36
wenzelm
parents: 20041
diff changeset
    37
  \item @{ML Variable.invent_fixes} is similar to @{ML
wenzelm
parents: 20041
diff changeset
    38
  Variable.add_fixes}, but the given names merely act as hints for
wenzelm
parents: 20041
diff changeset
    39
  internal fixes produced here.
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    40
20064
wenzelm
parents: 20041
diff changeset
    41
  \item @{ML Variable.import}~@{text "open ths ctxt"} augments the
wenzelm
parents: 20041
diff changeset
    42
  context by new fixes for the schematic type and term variables
wenzelm
parents: 20041
diff changeset
    43
  occurring in @{text "ths"}.  The @{text "open"} flag indicates
wenzelm
parents: 20041
diff changeset
    44
  whether the fixed names should be accessible to the user, otherwise
wenzelm
parents: 20041
diff changeset
    45
  internal names are chosen.
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    46
20064
wenzelm
parents: 20041
diff changeset
    47
  \item @{ML Variable.export}~@{text "inner outer ths"} generalizes
wenzelm
parents: 20041
diff changeset
    48
  fixed type and term variables in @{text "ths"} according to the
wenzelm
parents: 20041
diff changeset
    49
  difference of the @{text "inner"} and @{text "outer"} context.  Note
wenzelm
parents: 20041
diff changeset
    50
  that type variables occurring in term variables are still fixed.
wenzelm
parents: 20041
diff changeset
    51
wenzelm
parents: 20041
diff changeset
    52
  @{ML Variable.export} essentially reverses the effect of @{ML
wenzelm
parents: 20041
diff changeset
    53
  Variable.import} (up to renaming of schematic variables.
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    54
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    55
  \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML
20041
ae7aba935986 added some bits on variables;
wenzelm
parents: 20026
diff changeset
    56
  Variable.export}, i.e.\ it provides a view on facts with all
ae7aba935986 added some bits on variables;
wenzelm
parents: 20026
diff changeset
    57
  variables being fixed in the current context.
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    58
20064
wenzelm
parents: 20041
diff changeset
    59
  \item @{ML Variable.monomorphic}~@{text "ctxt ts"} introduces fixed
wenzelm
parents: 20041
diff changeset
    60
  type variables for the schematic ones in @{text "ts"}.
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    61
20064
wenzelm
parents: 20041
diff changeset
    62
  \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
wenzelm
parents: 20041
diff changeset
    63
  variables in @{text "ts"} as far as possible, even those occurring
wenzelm
parents: 20041
diff changeset
    64
  in fixed term variables.  This operation essentially reverses the
wenzelm
parents: 20041
diff changeset
    65
  default policy of type-inference to introduce local polymorphism as
wenzelm
parents: 20041
diff changeset
    66
  fixed types.
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    67
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    68
  \end{description}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    69
*}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    70
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    71
text FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    72
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    73
section {* Proof state *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    74
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    75
text {*
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    76
  FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    77
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    78
\glossary{Proof state}{The whole configuration of a structured proof,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    79
consisting of a \seeglossary{proof context} and an optional
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    80
\seeglossary{structured goal}.  Internally, an Isar proof state is
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    81
organized as a stack to accomodate block structure of proof texts.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    82
For historical reasons, a low-level \seeglossary{tactical goal} is
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    83
occasionally called ``proof state'' as well.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    84
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    85
\glossary{Structured goal}{FIXME}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    86
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    87
\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    88
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    89
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    90
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    91
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    92
section {* Methods *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    93
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    94
text FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    95
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    96
section {* Attributes *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    97
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    98
text FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    99
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   100
end