doc-src/IsarImplementation/Thy/proof.thy
author wenzelm
Wed, 13 Dec 2006 16:26:45 +0100
changeset 21827 0b1d07f79c1e
parent 20797 c1f0bc7e7d80
child 22568 ed7aa5a350ef
permissions -rw-r--r--
updated;
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
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20218
diff changeset
     6
chapter {* Structured proofs *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     7
20474
wenzelm
parents: 20472
diff changeset
     8
section {* Variables \label{sec:variables} *}
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
     9
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    10
text {*
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    11
  Any variable that is not explicitly bound by @{text "\<lambda>"}-abstraction
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    12
  is considered as ``free''.  Logically, free variables act like
20474
wenzelm
parents: 20472
diff changeset
    13
  outermost universal quantification at the sequent level: @{text
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    14
  "A\<^isub>1(x), \<dots>, A\<^isub>n(x) \<turnstile> B(x)"} means that the result
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    15
  holds \emph{for all} values of @{text "x"}.  Free variables for
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    16
  terms (not types) can be fully internalized into the logic: @{text
20474
wenzelm
parents: 20472
diff changeset
    17
  "\<turnstile> B(x)"} and @{text "\<turnstile> \<And>x. B(x)"} are interchangeable, provided
wenzelm
parents: 20472
diff changeset
    18
  that @{text "x"} does not occur elsewhere in the context.
wenzelm
parents: 20472
diff changeset
    19
  Inspecting @{text "\<turnstile> \<And>x. B(x)"} more closely, we see that inside the
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    20
  quantifier, @{text "x"} is essentially ``arbitrary, but fixed'',
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    21
  while from outside it appears as a place-holder for instantiation
20474
wenzelm
parents: 20472
diff changeset
    22
  (thanks to @{text "\<And>"} elimination).
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    23
20474
wenzelm
parents: 20472
diff changeset
    24
  The Pure logic represents the idea of variables being either inside
wenzelm
parents: 20472
diff changeset
    25
  or outside the current scope by providing separate syntactic
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    26
  categories for \emph{fixed variables} (e.g.\ @{text "x"}) vs.\
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    27
  \emph{schematic variables} (e.g.\ @{text "?x"}).  Incidently, a
20474
wenzelm
parents: 20472
diff changeset
    28
  universal result @{text "\<turnstile> \<And>x. B(x)"} has the HHF normal form @{text
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    29
  "\<turnstile> B(?x)"}, which represents its generality nicely without requiring
20474
wenzelm
parents: 20472
diff changeset
    30
  an explicit quantifier.  The same principle works for type
wenzelm
parents: 20472
diff changeset
    31
  variables: @{text "\<turnstile> B(?\<alpha>)"} represents the idea of ``@{text "\<turnstile>
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    32
  \<forall>\<alpha>. B(\<alpha>)"}'' without demanding a truly polymorphic framework.
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    33
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    34
  \medskip Additional care is required to treat type variables in a
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    35
  way that facilitates type-inference.  In principle, term variables
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    36
  depend on type variables, which means that type variables would have
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    37
  to be declared first.  For example, a raw type-theoretic framework
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    38
  would demand the context to be constructed in stages as follows:
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    39
  @{text "\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^isub>\<alpha>)"}.
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    40
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    41
  We allow a slightly less formalistic mode of operation: term
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    42
  variables @{text "x"} are fixed without specifying a type yet
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    43
  (essentially \emph{all} potential occurrences of some instance
20474
wenzelm
parents: 20472
diff changeset
    44
  @{text "x\<^isub>\<tau>"} are fixed); the first occurrence of @{text "x"}
wenzelm
parents: 20472
diff changeset
    45
  within a specific term assigns its most general type, which is then
wenzelm
parents: 20472
diff changeset
    46
  maintained consistently in the context.  The above example becomes
wenzelm
parents: 20472
diff changeset
    47
  @{text "\<Gamma> = x: term, \<alpha>: type, A(x\<^isub>\<alpha>)"}, where type @{text
wenzelm
parents: 20472
diff changeset
    48
  "\<alpha>"} is fixed \emph{after} term @{text "x"}, and the constraint
wenzelm
parents: 20472
diff changeset
    49
  @{text "x :: \<alpha>"} is an implicit consequence of the occurrence of
wenzelm
parents: 20472
diff changeset
    50
  @{text "x\<^isub>\<alpha>"} in the subsequent proposition.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    51
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    52
  This twist of dependencies is also accommodated by the reverse
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    53
  operation of exporting results from a context: a type variable
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    54
  @{text "\<alpha>"} is considered fixed as long as it occurs in some fixed
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    55
  term variable of the context.  For example, exporting @{text "x:
20474
wenzelm
parents: 20472
diff changeset
    56
  term, \<alpha>: type \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} produces in the first step
wenzelm
parents: 20472
diff changeset
    57
  @{text "x: term \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} for fixed @{text "\<alpha>"},
wenzelm
parents: 20472
diff changeset
    58
  and only in the second step @{text "\<turnstile> ?x\<^isub>?\<^isub>\<alpha> =
wenzelm
parents: 20472
diff changeset
    59
  ?x\<^isub>?\<^isub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    60
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    61
  \medskip The Isabelle/Isar proof context manages the gory details of
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    62
  term vs.\ type variables, with high-level principles for moving the
20474
wenzelm
parents: 20472
diff changeset
    63
  frontier between fixed and schematic variables.
wenzelm
parents: 20472
diff changeset
    64
wenzelm
parents: 20472
diff changeset
    65
  The @{text "add_fixes"} operation explictly declares fixed
wenzelm
parents: 20472
diff changeset
    66
  variables; the @{text "declare_term"} operation absorbs a term into
wenzelm
parents: 20472
diff changeset
    67
  a context by fixing new type variables and adding syntactic
wenzelm
parents: 20472
diff changeset
    68
  constraints.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    69
20474
wenzelm
parents: 20472
diff changeset
    70
  The @{text "export"} operation is able to perform the main work of
wenzelm
parents: 20472
diff changeset
    71
  generalizing term and type variables as sketched above, assuming
wenzelm
parents: 20472
diff changeset
    72
  that fixing variables and terms have been declared properly.
wenzelm
parents: 20472
diff changeset
    73
wenzelm
parents: 20472
diff changeset
    74
  There @{text "import"} operation makes a generalized fact a genuine
wenzelm
parents: 20472
diff changeset
    75
  part of the context, by inventing fixed variables for the schematic
wenzelm
parents: 20472
diff changeset
    76
  ones.  The effect can be reversed by using @{text "export"} later,
wenzelm
parents: 20472
diff changeset
    77
  potentially with an extended context; the result is equivalent to
wenzelm
parents: 20472
diff changeset
    78
  the original modulo renaming of schematic variables.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    79
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    80
  The @{text "focus"} operation provides a variant of @{text "import"}
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    81
  for nested propositions (with explicit quantification): @{text
20474
wenzelm
parents: 20472
diff changeset
    82
  "\<And>x\<^isub>1 \<dots> x\<^isub>n. B(x\<^isub>1, \<dots>, x\<^isub>n)"} is
wenzelm
parents: 20472
diff changeset
    83
  decomposed by inventing fixed variables @{text "x\<^isub>1, \<dots>,
wenzelm
parents: 20472
diff changeset
    84
  x\<^isub>n"} for the body.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    85
*}
20064
wenzelm
parents: 20041
diff changeset
    86
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    87
text %mlref {*
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    88
  \begin{mldecls}
20474
wenzelm
parents: 20472
diff changeset
    89
  @{index_ML Variable.add_fixes: "
wenzelm
parents: 20472
diff changeset
    90
  string list -> Proof.context -> string list * Proof.context"} \\
20797
c1f0bc7e7d80 renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents: 20547
diff changeset
    91
  @{index_ML Variable.variant_fixes: "
20474
wenzelm
parents: 20472
diff changeset
    92
  string list -> Proof.context -> string list * Proof.context"} \\
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
    93
  @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    94
  @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    95
  @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    96
  @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
20474
wenzelm
parents: 20472
diff changeset
    97
  @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
wenzelm
parents: 20472
diff changeset
    98
  ((ctyp list * cterm list) * thm list) * Proof.context"} \\
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    99
  @{index_ML Variable.focus: "cterm -> Proof.context -> (cterm list * cterm) * Proof.context"} \\
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   100
  \end{mldecls}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   101
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   102
  \begin{description}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   103
20064
wenzelm
parents: 20041
diff changeset
   104
  \item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   105
  variables @{text "xs"}, returning the resulting internal names.  By
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   106
  default, the internal representation coincides with the external
20474
wenzelm
parents: 20472
diff changeset
   107
  one, which also means that the given variables must not be fixed
wenzelm
parents: 20472
diff changeset
   108
  already.  There is a different policy within a local proof body: the
wenzelm
parents: 20472
diff changeset
   109
  given names are just hints for newly invented Skolem variables.
20064
wenzelm
parents: 20041
diff changeset
   110
20797
c1f0bc7e7d80 renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents: 20547
diff changeset
   111
  \item @{ML Variable.variant_fixes} is similar to @{ML
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   112
  Variable.add_fixes}, but always produces fresh variants of the given
20474
wenzelm
parents: 20472
diff changeset
   113
  names.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   114
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   115
  \item @{ML Variable.declare_term}~@{text "t ctxt"} declares term
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   116
  @{text "t"} to belong to the context.  This automatically fixes new
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   117
  type variables, but not term variables.  Syntactic constraints for
20474
wenzelm
parents: 20472
diff changeset
   118
  type and term variables are declared uniformly, though.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   119
20474
wenzelm
parents: 20472
diff changeset
   120
  \item @{ML Variable.declare_constraints}~@{text "t ctxt"} declares
wenzelm
parents: 20472
diff changeset
   121
  syntactic constraints from term @{text "t"}, without making it part
wenzelm
parents: 20472
diff changeset
   122
  of the context yet.
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   123
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   124
  \item @{ML Variable.export}~@{text "inner outer thms"} generalizes
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   125
  fixed type and term variables in @{text "thms"} according to the
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   126
  difference of the @{text "inner"} and @{text "outer"} context,
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   127
  following the principles sketched above.
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   128
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   129
  \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   130
  variables in @{text "ts"} as far as possible, even those occurring
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   131
  in fixed term variables.  The default policy of type-inference is to
20474
wenzelm
parents: 20472
diff changeset
   132
  fix newly introduced type variables, which is essentially reversed
wenzelm
parents: 20472
diff changeset
   133
  with @{ML Variable.polymorphic}: here the given terms are detached
wenzelm
parents: 20472
diff changeset
   134
  from the context as far as possible.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   135
20474
wenzelm
parents: 20472
diff changeset
   136
  \item @{ML Variable.import}~@{text "open thms ctxt"} invents fixed
wenzelm
parents: 20472
diff changeset
   137
  type and term variables for the schematic ones occurring in @{text
wenzelm
parents: 20472
diff changeset
   138
  "thms"}.  The @{text "open"} flag indicates whether the fixed names
wenzelm
parents: 20472
diff changeset
   139
  should be accessible to the user, otherwise newly introduced names
wenzelm
parents: 20472
diff changeset
   140
  are marked as ``internal'' (\secref{sec:names}).
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   141
20474
wenzelm
parents: 20472
diff changeset
   142
  \item @{ML Variable.focus}~@{text B} decomposes the outermost @{text
wenzelm
parents: 20472
diff changeset
   143
  "\<And>"} prefix of proposition @{text "B"}.
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   144
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   145
  \end{description}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   146
*}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   147
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   148
20474
wenzelm
parents: 20472
diff changeset
   149
section {* Assumptions \label{sec:assumptions} *}
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20218
diff changeset
   150
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   151
text {*
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   152
  An \emph{assumption} is a proposition that it is postulated in the
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   153
  current context.  Local conclusions may use assumptions as
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   154
  additional facts, but this imposes implicit hypotheses that weaken
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   155
  the overall statement.
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   156
20474
wenzelm
parents: 20472
diff changeset
   157
  Assumptions are restricted to fixed non-schematic statements, i.e.\
wenzelm
parents: 20472
diff changeset
   158
  all generality needs to be expressed by explicit quantifiers.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   159
  Nevertheless, the result will be in HHF normal form with outermost
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   160
  quantifiers stripped.  For example, by assuming @{text "\<And>x :: \<alpha>. P
20474
wenzelm
parents: 20472
diff changeset
   161
  x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for schematic @{text "?x"}
wenzelm
parents: 20472
diff changeset
   162
  of fixed type @{text "\<alpha>"}.  Local derivations accumulate more and
wenzelm
parents: 20472
diff changeset
   163
  more explicit references to hypotheses: @{text "A\<^isub>1, \<dots>,
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   164
  A\<^isub>n \<turnstile> B"} where @{text "A\<^isub>1, \<dots>, A\<^isub>n"} needs to
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   165
  be covered by the assumptions of the current context.
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   166
20459
wenzelm
parents: 20458
diff changeset
   167
  \medskip The @{text "add_assms"} operation augments the context by
wenzelm
parents: 20458
diff changeset
   168
  local assumptions, which are parameterized by an arbitrary @{text
wenzelm
parents: 20458
diff changeset
   169
  "export"} rule (see below).
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   170
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   171
  The @{text "export"} operation moves facts from a (larger) inner
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   172
  context into a (smaller) outer context, by discharging the
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   173
  difference of the assumptions as specified by the associated export
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   174
  rules.  Note that the discharged portion is determined by the
20459
wenzelm
parents: 20458
diff changeset
   175
  difference contexts, not the facts being exported!  There is a
wenzelm
parents: 20458
diff changeset
   176
  separate flag to indicate a goal context, where the result is meant
wenzelm
parents: 20458
diff changeset
   177
  to refine an enclosing sub-goal of a structured proof state (cf.\
wenzelm
parents: 20458
diff changeset
   178
  \secref{sec:isar-proof-state}).
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   179
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   180
  \medskip The most basic export rule discharges assumptions directly
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   181
  by means of the @{text "\<Longrightarrow>"} introduction rule:
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   182
  \[
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   183
  \infer[(@{text "\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   184
  \]
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   185
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   186
  The variant for goal refinements marks the newly introduced
20474
wenzelm
parents: 20472
diff changeset
   187
  premises, which causes the canonical Isar goal refinement scheme to
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   188
  enforce unification with local premises within the goal:
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   189
  \[
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   190
  \infer[(@{text "#\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   191
  \]
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   192
20474
wenzelm
parents: 20472
diff changeset
   193
  \medskip Alternative versions of assumptions may perform arbitrary
wenzelm
parents: 20472
diff changeset
   194
  transformations on export, as long as the corresponding portion of
20459
wenzelm
parents: 20458
diff changeset
   195
  hypotheses is removed from the given facts.  For example, a local
wenzelm
parents: 20458
diff changeset
   196
  definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"},
wenzelm
parents: 20458
diff changeset
   197
  with the following export rule to reverse the effect:
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   198
  \[
20491
wenzelm
parents: 20474
diff changeset
   199
  \infer[(@{text "\<equiv>-expand"})]{@{text "\<Gamma> \\ x \<equiv> t \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   200
  \]
20474
wenzelm
parents: 20472
diff changeset
   201
  This works, because the assumption @{text "x \<equiv> t"} was introduced in
wenzelm
parents: 20472
diff changeset
   202
  a context with @{text "x"} being fresh, so @{text "x"} does not
wenzelm
parents: 20472
diff changeset
   203
  occur in @{text "\<Gamma>"} here.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   204
*}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   205
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   206
text %mlref {*
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   207
  \begin{mldecls}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   208
  @{index_ML_type Assumption.export} \\
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   209
  @{index_ML Assumption.assume: "cterm -> thm"} \\
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   210
  @{index_ML Assumption.add_assms:
20459
wenzelm
parents: 20458
diff changeset
   211
    "Assumption.export ->
wenzelm
parents: 20458
diff changeset
   212
  cterm list -> Proof.context -> thm list * Proof.context"} \\
wenzelm
parents: 20458
diff changeset
   213
  @{index_ML Assumption.add_assumes: "
wenzelm
parents: 20458
diff changeset
   214
  cterm list -> Proof.context -> thm list * Proof.context"} \\
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   215
  @{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   216
  \end{mldecls}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   217
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   218
  \begin{description}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   219
20459
wenzelm
parents: 20458
diff changeset
   220
  \item @{ML_type Assumption.export} represents arbitrary export
wenzelm
parents: 20458
diff changeset
   221
  rules, which is any function of type @{ML_type "bool -> cterm list -> thm -> thm"},
wenzelm
parents: 20458
diff changeset
   222
  where the @{ML_type "bool"} indicates goal mode, and the @{ML_type
wenzelm
parents: 20458
diff changeset
   223
  "cterm list"} the collection of assumptions to be discharged
wenzelm
parents: 20458
diff changeset
   224
  simultaneously.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   225
20459
wenzelm
parents: 20458
diff changeset
   226
  \item @{ML Assumption.assume}~@{text "A"} turns proposition @{text
wenzelm
parents: 20458
diff changeset
   227
  "A"} into a raw assumption @{text "A \<turnstile> A'"}, where the conclusion
wenzelm
parents: 20458
diff changeset
   228
  @{text "A'"} is in HHF normal form.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   229
20474
wenzelm
parents: 20472
diff changeset
   230
  \item @{ML Assumption.add_assms}~@{text "r As"} augments the context
wenzelm
parents: 20472
diff changeset
   231
  by assumptions @{text "As"} with export rule @{text "r"}.  The
wenzelm
parents: 20472
diff changeset
   232
  resulting facts are hypothetical theorems as produced by the raw
wenzelm
parents: 20472
diff changeset
   233
  @{ML Assumption.assume}.
20459
wenzelm
parents: 20458
diff changeset
   234
wenzelm
parents: 20458
diff changeset
   235
  \item @{ML Assumption.add_assumes}~@{text "As"} is a special case of
wenzelm
parents: 20458
diff changeset
   236
  @{ML Assumption.add_assms} where the export rule performs @{text
wenzelm
parents: 20458
diff changeset
   237
  "\<Longrightarrow>_intro"} or @{text "#\<Longrightarrow>_intro"}, depending on goal mode.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   238
20474
wenzelm
parents: 20472
diff changeset
   239
  \item @{ML Assumption.export}~@{text "is_goal inner outer thm"}
wenzelm
parents: 20472
diff changeset
   240
  exports result @{text "thm"} from the the @{text "inner"} context
20459
wenzelm
parents: 20458
diff changeset
   241
  back into the @{text "outer"} one; @{text "is_goal = true"} means
wenzelm
parents: 20458
diff changeset
   242
  this is a goal context.  The result is in HHF normal form.  Note
wenzelm
parents: 20458
diff changeset
   243
  that @{ML "ProofContext.export"} combines @{ML "Variable.export"}
wenzelm
parents: 20458
diff changeset
   244
  and @{ML "Assumption.export"} in the canonical way.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   245
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   246
  \end{description}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   247
*}
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20218
diff changeset
   248
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20218
diff changeset
   249
20520
wenzelm
parents: 20491
diff changeset
   250
section {* Results *}
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20218
diff changeset
   251
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   252
text {*
20472
wenzelm
parents: 20470
diff changeset
   253
  Local results are established by monotonic reasoning from facts
20474
wenzelm
parents: 20472
diff changeset
   254
  within a context.  This allows common combinations of theorems,
wenzelm
parents: 20472
diff changeset
   255
  e.g.\ via @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or equational
wenzelm
parents: 20472
diff changeset
   256
  reasoning, see \secref{sec:thms}.  Unaccounted context manipulations
wenzelm
parents: 20472
diff changeset
   257
  should be avoided, notably raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc
20472
wenzelm
parents: 20470
diff changeset
   258
  references to free variables or assumptions not present in the proof
wenzelm
parents: 20470
diff changeset
   259
  context.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   260
20491
wenzelm
parents: 20474
diff changeset
   261
  \medskip The @{text "SUBPROOF"} combinator allows to structure a
wenzelm
parents: 20474
diff changeset
   262
  tactical proof recursively by decomposing a selected sub-goal:
wenzelm
parents: 20474
diff changeset
   263
  @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"}
wenzelm
parents: 20474
diff changeset
   264
  after fixing @{text "x"} and assuming @{text "A(x)"}.  This means
wenzelm
parents: 20474
diff changeset
   265
  the tactic needs to solve the conclusion, but may use the premise as
wenzelm
parents: 20474
diff changeset
   266
  a local fact, for locally fixed variables.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   267
20491
wenzelm
parents: 20474
diff changeset
   268
  The @{text "prove"} operation provides an interface for structured
wenzelm
parents: 20474
diff changeset
   269
  backwards reasoning under program control, with some explicit sanity
wenzelm
parents: 20474
diff changeset
   270
  checks of the result.  The goal context can be augmented by
wenzelm
parents: 20474
diff changeset
   271
  additional fixed variables (cf.\ \secref{sec:variables}) and
wenzelm
parents: 20474
diff changeset
   272
  assumptions (cf.\ \secref{sec:assumptions}), which will be available
wenzelm
parents: 20474
diff changeset
   273
  as local facts during the proof and discharged into implications in
wenzelm
parents: 20474
diff changeset
   274
  the result.  Type and term variables are generalized as usual,
wenzelm
parents: 20474
diff changeset
   275
  according to the context.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   276
20491
wenzelm
parents: 20474
diff changeset
   277
  The @{text "obtain"} operation produces results by eliminating
wenzelm
parents: 20474
diff changeset
   278
  existing facts by means of a given tactic.  This acts like a dual
wenzelm
parents: 20474
diff changeset
   279
  conclusion: the proof demonstrates that the context may be augmented
wenzelm
parents: 20474
diff changeset
   280
  by certain fixed variables and assumptions.  See also
wenzelm
parents: 20474
diff changeset
   281
  \cite{isabelle-isar-ref} for the user-level @{text "\<OBTAIN>"} and
wenzelm
parents: 20474
diff changeset
   282
  @{text "\<GUESS>"} elements.  Final results, which may not refer to
wenzelm
parents: 20474
diff changeset
   283
  the parameters in the conclusion, need to exported explicitly into
wenzelm
parents: 20474
diff changeset
   284
  the original context.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   285
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   286
20472
wenzelm
parents: 20470
diff changeset
   287
text %mlref {*
wenzelm
parents: 20470
diff changeset
   288
  \begin{mldecls}
20491
wenzelm
parents: 20474
diff changeset
   289
  @{index_ML SUBPROOF:
wenzelm
parents: 20474
diff changeset
   290
  "({context: Proof.context, schematics: ctyp list * cterm list,
wenzelm
parents: 20474
diff changeset
   291
    params: cterm list, asms: cterm list, concl: cterm,
wenzelm
parents: 20474
diff changeset
   292
    prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\
20547
wenzelm
parents: 20542
diff changeset
   293
  \end{mldecls}
wenzelm
parents: 20542
diff changeset
   294
  \begin{mldecls}
20472
wenzelm
parents: 20470
diff changeset
   295
  @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
wenzelm
parents: 20470
diff changeset
   296
  ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
wenzelm
parents: 20470
diff changeset
   297
  @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
wenzelm
parents: 20470
diff changeset
   298
  ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
20547
wenzelm
parents: 20542
diff changeset
   299
  \end{mldecls}
wenzelm
parents: 20542
diff changeset
   300
  \begin{mldecls}
20491
wenzelm
parents: 20474
diff changeset
   301
  @{index_ML Obtain.result: "(Proof.context -> tactic) ->
20542
a54ca4e90874 more on theorems;
wenzelm
parents: 20520
diff changeset
   302
  thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\
20472
wenzelm
parents: 20470
diff changeset
   303
  \end{mldecls}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   304
20472
wenzelm
parents: 20470
diff changeset
   305
  \begin{description}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   306
20491
wenzelm
parents: 20474
diff changeset
   307
  \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a
wenzelm
parents: 20474
diff changeset
   308
  particular sub-goal, producing an extended context and a reduced
wenzelm
parents: 20474
diff changeset
   309
  goal, which needs to be solved by the given tactic.  All schematic
wenzelm
parents: 20474
diff changeset
   310
  parameters of the goal are imported into the context as fixed ones,
wenzelm
parents: 20474
diff changeset
   311
  which may not be instantiated in the sub-proof.
wenzelm
parents: 20474
diff changeset
   312
20472
wenzelm
parents: 20470
diff changeset
   313
  \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
20474
wenzelm
parents: 20472
diff changeset
   314
  "C"} in the context augmented by fixed variables @{text "xs"} and
wenzelm
parents: 20472
diff changeset
   315
  assumptions @{text "As"}, and applies tactic @{text "tac"} to solve
wenzelm
parents: 20472
diff changeset
   316
  it.  The latter may depend on the local assumptions being presented
wenzelm
parents: 20472
diff changeset
   317
  as facts.  The result is in HHF normal form.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   318
20472
wenzelm
parents: 20470
diff changeset
   319
  \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
20491
wenzelm
parents: 20474
diff changeset
   320
  states several conclusions simultaneously.  The goal is encoded by
21827
0b1d07f79c1e updated;
wenzelm
parents: 20797
diff changeset
   321
  means of Pure conjunction; @{ML Goal.conjunction_tac} will turn this
0b1d07f79c1e updated;
wenzelm
parents: 20797
diff changeset
   322
  into a collection of individual subgoals.
20472
wenzelm
parents: 20470
diff changeset
   323
20491
wenzelm
parents: 20474
diff changeset
   324
  \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the
wenzelm
parents: 20474
diff changeset
   325
  given facts using a tactic, which results in additional fixed
wenzelm
parents: 20474
diff changeset
   326
  variables and assumptions in the context.  Final results need to be
wenzelm
parents: 20474
diff changeset
   327
  exported explicitly.
20472
wenzelm
parents: 20470
diff changeset
   328
wenzelm
parents: 20470
diff changeset
   329
  \end{description}
wenzelm
parents: 20470
diff changeset
   330
*}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   331
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   332
end