src/Doc/IsarImplementation/Proof.thy
author wenzelm
Tue, 13 Aug 2013 16:25:47 +0200
changeset 53015 a1119cf551e8
parent 52463 c45a6939217f
child 54883 dd04a8b654fc
permissions -rw-r--r--
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29755
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 28541
diff changeset
     1
theory Proof
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 28541
diff changeset
     2
imports Base
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 28541
diff changeset
     3
begin
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20218
diff changeset
     5
chapter {* Structured proofs *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
20474
wenzelm
parents: 20472
diff changeset
     7
section {* Variables \label{sec:variables} *}
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
     8
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
     9
text {*
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    10
  Any variable that is not explicitly bound by @{text "\<lambda>"}-abstraction
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    11
  is considered as ``free''.  Logically, free variables act like
20474
wenzelm
parents: 20472
diff changeset
    12
  outermost universal quantification at the sequent level: @{text
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
    13
  "A\<^sub>1(x), \<dots>, A\<^sub>n(x) \<turnstile> B(x)"} means that the result
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    14
  holds \emph{for all} values of @{text "x"}.  Free variables for
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    15
  terms (not types) can be fully internalized into the logic: @{text
20474
wenzelm
parents: 20472
diff changeset
    16
  "\<turnstile> B(x)"} and @{text "\<turnstile> \<And>x. B(x)"} are interchangeable, provided
wenzelm
parents: 20472
diff changeset
    17
  that @{text "x"} does not occur elsewhere in the context.
wenzelm
parents: 20472
diff changeset
    18
  Inspecting @{text "\<turnstile> \<And>x. B(x)"} more closely, we see that inside the
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    19
  quantifier, @{text "x"} is essentially ``arbitrary, but fixed'',
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    20
  while from outside it appears as a place-holder for instantiation
20474
wenzelm
parents: 20472
diff changeset
    21
  (thanks to @{text "\<And>"} elimination).
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    22
20474
wenzelm
parents: 20472
diff changeset
    23
  The Pure logic represents the idea of variables being either inside
wenzelm
parents: 20472
diff changeset
    24
  or outside the current scope by providing separate syntactic
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    25
  categories for \emph{fixed variables} (e.g.\ @{text "x"}) vs.\
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    26
  \emph{schematic variables} (e.g.\ @{text "?x"}).  Incidently, a
20474
wenzelm
parents: 20472
diff changeset
    27
  universal result @{text "\<turnstile> \<And>x. B(x)"} has the HHF normal form @{text
34930
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
    28
  "\<turnstile> B(?x)"}, which represents its generality without requiring an
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
    29
  explicit quantifier.  The same principle works for type variables:
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
    30
  @{text "\<turnstile> B(?\<alpha>)"} represents the idea of ``@{text "\<turnstile> \<forall>\<alpha>. B(\<alpha>)"}''
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
    31
  without demanding a truly polymorphic framework.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    32
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    33
  \medskip Additional care is required to treat type variables in a
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    34
  way that facilitates type-inference.  In principle, term variables
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    35
  depend on type variables, which means that type variables would have
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    36
  to be declared first.  For example, a raw type-theoretic framework
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    37
  would demand the context to be constructed in stages as follows:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
    38
  @{text "\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^sub>\<alpha>)"}.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    39
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    40
  We allow a slightly less formalistic mode of operation: term
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    41
  variables @{text "x"} are fixed without specifying a type yet
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    42
  (essentially \emph{all} potential occurrences of some instance
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
    43
  @{text "x\<^sub>\<tau>"} are fixed); the first occurrence of @{text "x"}
20474
wenzelm
parents: 20472
diff changeset
    44
  within a specific term assigns its most general type, which is then
wenzelm
parents: 20472
diff changeset
    45
  maintained consistently in the context.  The above example becomes
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
    46
  @{text "\<Gamma> = x: term, \<alpha>: type, A(x\<^sub>\<alpha>)"}, where type @{text
20474
wenzelm
parents: 20472
diff changeset
    47
  "\<alpha>"} is fixed \emph{after} term @{text "x"}, and the constraint
wenzelm
parents: 20472
diff changeset
    48
  @{text "x :: \<alpha>"} is an implicit consequence of the occurrence of
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
    49
  @{text "x\<^sub>\<alpha>"} in the subsequent proposition.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    50
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    51
  This twist of dependencies is also accommodated by the reverse
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    52
  operation of exporting results from a context: a type variable
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    53
  @{text "\<alpha>"} is considered fixed as long as it occurs in some fixed
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    54
  term variable of the context.  For example, exporting @{text "x:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
    55
  term, \<alpha>: type \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>"} produces in the first step @{text "x: term
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
    56
  \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>"} for fixed @{text "\<alpha>"}, and only in the second step
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
    57
  @{text "\<turnstile> ?x\<^sub>?\<^sub>\<alpha> \<equiv> ?x\<^sub>?\<^sub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}.
39841
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    58
  The following Isar source text illustrates this scenario.
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    59
*}
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    60
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40153
diff changeset
    61
notepad
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40153
diff changeset
    62
begin
39841
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    63
  {
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    64
    fix x  -- {* all potential occurrences of some @{text "x::\<tau>"} are fixed *}
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    65
    {
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    66
      have "x::'a \<equiv> x"  -- {* implicit type assigment by concrete occurrence *}
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    67
        by (rule reflexive)
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    68
    }
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    69
    thm this  -- {* result still with fixed type @{text "'a"} *}
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    70
  }
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    71
  thm this  -- {* fully general result for arbitrary @{text "?x::?'a"} *}
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40153
diff changeset
    72
end
39841
c7f3efe59e4e more examples;
wenzelm
parents: 39821
diff changeset
    73
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39853
diff changeset
    74
text {* The Isabelle/Isar proof context manages the details of term
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39853
diff changeset
    75
  vs.\ type variables, with high-level principles for moving the
20474
wenzelm
parents: 20472
diff changeset
    76
  frontier between fixed and schematic variables.
wenzelm
parents: 20472
diff changeset
    77
wenzelm
parents: 20472
diff changeset
    78
  The @{text "add_fixes"} operation explictly declares fixed
wenzelm
parents: 20472
diff changeset
    79
  variables; the @{text "declare_term"} operation absorbs a term into
wenzelm
parents: 20472
diff changeset
    80
  a context by fixing new type variables and adding syntactic
wenzelm
parents: 20472
diff changeset
    81
  constraints.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    82
20474
wenzelm
parents: 20472
diff changeset
    83
  The @{text "export"} operation is able to perform the main work of
wenzelm
parents: 20472
diff changeset
    84
  generalizing term and type variables as sketched above, assuming
wenzelm
parents: 20472
diff changeset
    85
  that fixing variables and terms have been declared properly.
wenzelm
parents: 20472
diff changeset
    86
wenzelm
parents: 20472
diff changeset
    87
  There @{text "import"} operation makes a generalized fact a genuine
wenzelm
parents: 20472
diff changeset
    88
  part of the context, by inventing fixed variables for the schematic
wenzelm
parents: 20472
diff changeset
    89
  ones.  The effect can be reversed by using @{text "export"} later,
wenzelm
parents: 20472
diff changeset
    90
  potentially with an extended context; the result is equivalent to
wenzelm
parents: 20472
diff changeset
    91
  the original modulo renaming of schematic variables.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    92
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    93
  The @{text "focus"} operation provides a variant of @{text "import"}
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    94
  for nested propositions (with explicit quantification): @{text
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
    95
  "\<And>x\<^sub>1 \<dots> x\<^sub>n. B(x\<^sub>1, \<dots>, x\<^sub>n)"} is
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
    96
  decomposed by inventing fixed variables @{text "x\<^sub>1, \<dots>,
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
    97
  x\<^sub>n"} for the body.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
    98
*}
20064
wenzelm
parents: 20041
diff changeset
    99
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   100
text %mlref {*
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   101
  \begin{mldecls}
20474
wenzelm
parents: 20472
diff changeset
   102
  @{index_ML Variable.add_fixes: "
wenzelm
parents: 20472
diff changeset
   103
  string list -> Proof.context -> string list * Proof.context"} \\
20797
c1f0bc7e7d80 renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents: 20547
diff changeset
   104
  @{index_ML Variable.variant_fixes: "
20474
wenzelm
parents: 20472
diff changeset
   105
  string list -> Proof.context -> string list * Proof.context"} \\
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   106
  @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   107
  @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   108
  @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   109
  @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
31794
71af1fd6a5e4 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents: 30272
diff changeset
   110
  @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
32302
aa48c2b8f8e0 updated Variable.import;
wenzelm
parents: 32201
diff changeset
   111
  (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\
42509
9d107a52b634 updated Variable.focus;
wenzelm
parents: 42361
diff changeset
   112
  @{index_ML Variable.focus: "term -> Proof.context ->
9d107a52b634 updated Variable.focus;
wenzelm
parents: 42361
diff changeset
   113
  ((string * (string * typ)) list * term) * Proof.context"} \\
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   114
  \end{mldecls}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   115
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   116
  \begin{description}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   117
20064
wenzelm
parents: 20041
diff changeset
   118
  \item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   119
  variables @{text "xs"}, returning the resulting internal names.  By
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   120
  default, the internal representation coincides with the external
20474
wenzelm
parents: 20472
diff changeset
   121
  one, which also means that the given variables must not be fixed
wenzelm
parents: 20472
diff changeset
   122
  already.  There is a different policy within a local proof body: the
wenzelm
parents: 20472
diff changeset
   123
  given names are just hints for newly invented Skolem variables.
20064
wenzelm
parents: 20041
diff changeset
   124
20797
c1f0bc7e7d80 renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents: 20547
diff changeset
   125
  \item @{ML Variable.variant_fixes} is similar to @{ML
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   126
  Variable.add_fixes}, but always produces fresh variants of the given
20474
wenzelm
parents: 20472
diff changeset
   127
  names.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   128
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   129
  \item @{ML Variable.declare_term}~@{text "t ctxt"} declares term
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   130
  @{text "t"} to belong to the context.  This automatically fixes new
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   131
  type variables, but not term variables.  Syntactic constraints for
20474
wenzelm
parents: 20472
diff changeset
   132
  type and term variables are declared uniformly, though.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   133
20474
wenzelm
parents: 20472
diff changeset
   134
  \item @{ML Variable.declare_constraints}~@{text "t ctxt"} declares
wenzelm
parents: 20472
diff changeset
   135
  syntactic constraints from term @{text "t"}, without making it part
wenzelm
parents: 20472
diff changeset
   136
  of the context yet.
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   137
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   138
  \item @{ML Variable.export}~@{text "inner outer thms"} generalizes
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   139
  fixed type and term variables in @{text "thms"} according to the
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   140
  difference of the @{text "inner"} and @{text "outer"} context,
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   141
  following the principles sketched above.
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   142
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   143
  \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   144
  variables in @{text "ts"} as far as possible, even those occurring
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   145
  in fixed term variables.  The default policy of type-inference is to
20474
wenzelm
parents: 20472
diff changeset
   146
  fix newly introduced type variables, which is essentially reversed
wenzelm
parents: 20472
diff changeset
   147
  with @{ML Variable.polymorphic}: here the given terms are detached
wenzelm
parents: 20472
diff changeset
   148
  from the context as far as possible.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20460
diff changeset
   149
31794
71af1fd6a5e4 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents: 30272
diff changeset
   150
  \item @{ML Variable.import}~@{text "open thms ctxt"} invents fixed
20474
wenzelm
parents: 20472
diff changeset
   151
  type and term variables for the schematic ones occurring in @{text
wenzelm
parents: 20472
diff changeset
   152
  "thms"}.  The @{text "open"} flag indicates whether the fixed names
wenzelm
parents: 20472
diff changeset
   153
  should be accessible to the user, otherwise newly introduced names
wenzelm
parents: 20472
diff changeset
   154
  are marked as ``internal'' (\secref{sec:names}).
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   155
20474
wenzelm
parents: 20472
diff changeset
   156
  \item @{ML Variable.focus}~@{text B} decomposes the outermost @{text
wenzelm
parents: 20472
diff changeset
   157
  "\<And>"} prefix of proposition @{text "B"}.
20026
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   158
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   159
  \end{description}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   160
*}
3469df62fe21 Local variables;
wenzelm
parents: 18537
diff changeset
   161
39846
cb6634eb8926 examples in Isabelle/HOL;
wenzelm
parents: 39841
diff changeset
   162
text %mlex {* The following example shows how to work with fixed term
cb6634eb8926 examples in Isabelle/HOL;
wenzelm
parents: 39841
diff changeset
   163
  and type parameters and with type-inference.  *}
34932
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   164
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   165
ML {*
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   166
  (*static compile-time context -- for testing only*)
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   167
  val ctxt0 = @{context};
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   168
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   169
  (*locally fixed parameters -- no type assignment yet*)
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   170
  val ([x, y], ctxt1) = ctxt0 |> Variable.add_fixes ["x", "y"];
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   171
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   172
  (*t1: most general fixed type; t1': most general arbitrary type*)
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   173
  val t1 = Syntax.read_term ctxt1 "x";
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   174
  val t1' = singleton (Variable.polymorphic ctxt1) t1;
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   175
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   176
  (*term u enforces specific type assignment*)
39846
cb6634eb8926 examples in Isabelle/HOL;
wenzelm
parents: 39841
diff changeset
   177
  val u = Syntax.read_term ctxt1 "(x::nat) \<equiv> y";
34932
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   178
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   179
  (*official declaration of u -- propagates constraints etc.*)
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   180
  val ctxt2 = ctxt1 |> Variable.declare_term u;
39846
cb6634eb8926 examples in Isabelle/HOL;
wenzelm
parents: 39841
diff changeset
   181
  val t2 = Syntax.read_term ctxt2 "x";  (*x::nat is enforced*)
34932
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   182
*}
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   183
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 39864
diff changeset
   184
text {* In the above example, the starting context is derived from the
916cb4a28ffd misc tuning;
wenzelm
parents: 39864
diff changeset
   185
  toplevel theory, which means that fixed variables are internalized
40153
wenzelm
parents: 40126
diff changeset
   186
  literally: @{text "x"} is mapped again to @{text "x"}, and
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 39864
diff changeset
   187
  attempting to fix it again in the subsequent context is an error.
916cb4a28ffd misc tuning;
wenzelm
parents: 39864
diff changeset
   188
  Alternatively, fixed parameters can be renamed explicitly as
916cb4a28ffd misc tuning;
wenzelm
parents: 39864
diff changeset
   189
  follows: *}
34932
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   190
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   191
ML {*
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   192
  val ctxt0 = @{context};
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   193
  val ([x1, x2, x3], ctxt1) =
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   194
    ctxt0 |> Variable.variant_fixes ["x", "x", "x"];
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   195
*}
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   196
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39853
diff changeset
   197
text {* The following ML code can now work with the invented names of
40153
wenzelm
parents: 40126
diff changeset
   198
  @{text x1}, @{text x2}, @{text x3}, without depending on
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39853
diff changeset
   199
  the details on the system policy for introducing these variants.
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39853
diff changeset
   200
  Recall that within a proof body the system always invents fresh
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39853
diff changeset
   201
  ``skolem constants'', e.g.\ as follows: *}
34932
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   202
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40153
diff changeset
   203
notepad
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40153
diff changeset
   204
begin
34932
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   205
  ML_prf %"ML" {*
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   206
    val ctxt0 = @{context};
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   207
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   208
    val ([x1], ctxt1) = ctxt0 |> Variable.add_fixes ["x"];
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   209
    val ([x2], ctxt2) = ctxt1 |> Variable.add_fixes ["x"];
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   210
    val ([x3], ctxt3) = ctxt2 |> Variable.add_fixes ["x"];
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   211
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   212
    val ([y1, y2], ctxt4) =
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   213
      ctxt3 |> Variable.variant_fixes ["y", "y"];
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   214
  *}
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40153
diff changeset
   215
end
34932
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   216
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39853
diff changeset
   217
text {* In this situation @{ML Variable.add_fixes} and @{ML
34932
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   218
  Variable.variant_fixes} are very similar, but identical name
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   219
  proposals given in a row are only accepted by the second version.
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39853
diff changeset
   220
  *}
34932
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   221
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   222
20474
wenzelm
parents: 20472
diff changeset
   223
section {* Assumptions \label{sec:assumptions} *}
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20218
diff changeset
   224
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   225
text {*
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   226
  An \emph{assumption} is a proposition that it is postulated in the
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   227
  current context.  Local conclusions may use assumptions as
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   228
  additional facts, but this imposes implicit hypotheses that weaken
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   229
  the overall statement.
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   230
20474
wenzelm
parents: 20472
diff changeset
   231
  Assumptions are restricted to fixed non-schematic statements, i.e.\
wenzelm
parents: 20472
diff changeset
   232
  all generality needs to be expressed by explicit quantifiers.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   233
  Nevertheless, the result will be in HHF normal form with outermost
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   234
  quantifiers stripped.  For example, by assuming @{text "\<And>x :: \<alpha>. P
20474
wenzelm
parents: 20472
diff changeset
   235
  x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for schematic @{text "?x"}
wenzelm
parents: 20472
diff changeset
   236
  of fixed type @{text "\<alpha>"}.  Local derivations accumulate more and
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
   237
  more explicit references to hypotheses: @{text "A\<^sub>1, \<dots>,
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52463
diff changeset
   238
  A\<^sub>n \<turnstile> B"} where @{text "A\<^sub>1, \<dots>, A\<^sub>n"} needs to
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   239
  be covered by the assumptions of the current context.
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   240
20459
wenzelm
parents: 20458
diff changeset
   241
  \medskip The @{text "add_assms"} operation augments the context by
wenzelm
parents: 20458
diff changeset
   242
  local assumptions, which are parameterized by an arbitrary @{text
wenzelm
parents: 20458
diff changeset
   243
  "export"} rule (see below).
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   244
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   245
  The @{text "export"} operation moves facts from a (larger) inner
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   246
  context into a (smaller) outer context, by discharging the
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   247
  difference of the assumptions as specified by the associated export
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   248
  rules.  Note that the discharged portion is determined by the
34930
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   249
  difference of contexts, not the facts being exported!  There is a
20459
wenzelm
parents: 20458
diff changeset
   250
  separate flag to indicate a goal context, where the result is meant
29760
9c6c1b3f3eb6 tuned refs;
wenzelm
parents: 29755
diff changeset
   251
  to refine an enclosing sub-goal of a structured proof state.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   252
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   253
  \medskip The most basic export rule discharges assumptions directly
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   254
  by means of the @{text "\<Longrightarrow>"} introduction rule:
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   255
  \[
42666
fee67c099d03 use existing \<hyphen>;
wenzelm
parents: 42509
diff changeset
   256
  \infer[(@{text "\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   257
  \]
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   258
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   259
  The variant for goal refinements marks the newly introduced
20474
wenzelm
parents: 20472
diff changeset
   260
  premises, which causes the canonical Isar goal refinement scheme to
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   261
  enforce unification with local premises within the goal:
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   262
  \[
42666
fee67c099d03 use existing \<hyphen>;
wenzelm
parents: 42509
diff changeset
   263
  \infer[(@{text "#\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   264
  \]
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   265
20474
wenzelm
parents: 20472
diff changeset
   266
  \medskip Alternative versions of assumptions may perform arbitrary
wenzelm
parents: 20472
diff changeset
   267
  transformations on export, as long as the corresponding portion of
20459
wenzelm
parents: 20458
diff changeset
   268
  hypotheses is removed from the given facts.  For example, a local
wenzelm
parents: 20458
diff changeset
   269
  definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"},
wenzelm
parents: 20458
diff changeset
   270
  with the following export rule to reverse the effect:
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   271
  \[
42666
fee67c099d03 use existing \<hyphen>;
wenzelm
parents: 42509
diff changeset
   272
  \infer[(@{text "\<equiv>\<hyphen>expand"})]{@{text "\<Gamma> - (x \<equiv> t) \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   273
  \]
20474
wenzelm
parents: 20472
diff changeset
   274
  This works, because the assumption @{text "x \<equiv> t"} was introduced in
wenzelm
parents: 20472
diff changeset
   275
  a context with @{text "x"} being fresh, so @{text "x"} does not
wenzelm
parents: 20472
diff changeset
   276
  occur in @{text "\<Gamma>"} here.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   277
*}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   278
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   279
text %mlref {*
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   280
  \begin{mldecls}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   281
  @{index_ML_type Assumption.export} \\
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   282
  @{index_ML Assumption.assume: "cterm -> thm"} \\
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   283
  @{index_ML Assumption.add_assms:
20459
wenzelm
parents: 20458
diff changeset
   284
    "Assumption.export ->
wenzelm
parents: 20458
diff changeset
   285
  cterm list -> Proof.context -> thm list * Proof.context"} \\
wenzelm
parents: 20458
diff changeset
   286
  @{index_ML Assumption.add_assumes: "
wenzelm
parents: 20458
diff changeset
   287
  cterm list -> Proof.context -> thm list * Proof.context"} \\
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   288
  @{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   289
  \end{mldecls}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   290
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   291
  \begin{description}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   292
39864
wenzelm
parents: 39861
diff changeset
   293
  \item Type @{ML_type Assumption.export} represents arbitrary export
wenzelm
parents: 39861
diff changeset
   294
  rules, which is any function of type @{ML_type "bool -> cterm list
wenzelm
parents: 39861
diff changeset
   295
  -> thm -> thm"}, where the @{ML_type "bool"} indicates goal mode,
wenzelm
parents: 39861
diff changeset
   296
  and the @{ML_type "cterm list"} the collection of assumptions to be
wenzelm
parents: 39861
diff changeset
   297
  discharged simultaneously.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   298
20459
wenzelm
parents: 20458
diff changeset
   299
  \item @{ML Assumption.assume}~@{text "A"} turns proposition @{text
34930
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   300
  "A"} into a primitive assumption @{text "A \<turnstile> A'"}, where the
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   301
  conclusion @{text "A'"} is in HHF normal form.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   302
20474
wenzelm
parents: 20472
diff changeset
   303
  \item @{ML Assumption.add_assms}~@{text "r As"} augments the context
wenzelm
parents: 20472
diff changeset
   304
  by assumptions @{text "As"} with export rule @{text "r"}.  The
wenzelm
parents: 20472
diff changeset
   305
  resulting facts are hypothetical theorems as produced by the raw
wenzelm
parents: 20472
diff changeset
   306
  @{ML Assumption.assume}.
20459
wenzelm
parents: 20458
diff changeset
   307
wenzelm
parents: 20458
diff changeset
   308
  \item @{ML Assumption.add_assumes}~@{text "As"} is a special case of
wenzelm
parents: 20458
diff changeset
   309
  @{ML Assumption.add_assms} where the export rule performs @{text
42666
fee67c099d03 use existing \<hyphen>;
wenzelm
parents: 42509
diff changeset
   310
  "\<Longrightarrow>\<hyphen>intro"} or @{text "#\<Longrightarrow>\<hyphen>intro"}, depending on goal
34930
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   311
  mode.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   312
20474
wenzelm
parents: 20472
diff changeset
   313
  \item @{ML Assumption.export}~@{text "is_goal inner outer thm"}
wenzelm
parents: 20472
diff changeset
   314
  exports result @{text "thm"} from the the @{text "inner"} context
20459
wenzelm
parents: 20458
diff changeset
   315
  back into the @{text "outer"} one; @{text "is_goal = true"} means
wenzelm
parents: 20458
diff changeset
   316
  this is a goal context.  The result is in HHF normal form.  Note
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 40964
diff changeset
   317
  that @{ML "Proof_Context.export"} combines @{ML "Variable.export"}
20459
wenzelm
parents: 20458
diff changeset
   318
  and @{ML "Assumption.export"} in the canonical way.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   319
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   320
  \end{description}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   321
*}
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20218
diff changeset
   322
34932
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   323
text %mlex {* The following example demonstrates how rules can be
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   324
  derived by building up a context of assumptions first, and exporting
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   325
  some local fact afterwards.  We refer to @{theory Pure} equality
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   326
  here for testing purposes.
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   327
*}
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   328
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   329
ML {*
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   330
  (*static compile-time context -- for testing only*)
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   331
  val ctxt0 = @{context};
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   332
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   333
  val ([eq], ctxt1) =
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   334
    ctxt0 |> Assumption.add_assumes [@{cprop "x \<equiv> y"}];
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   335
  val eq' = Thm.symmetric eq;
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   336
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   337
  (*back to original context -- discharges assumption*)
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   338
  val r = Assumption.export false ctxt1 ctxt0 eq';
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   339
*}
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   340
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39853
diff changeset
   341
text {* Note that the variables of the resulting rule are not
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39853
diff changeset
   342
  generalized.  This would have required to fix them properly in the
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39853
diff changeset
   343
  context beforehand, and export wrt.\ variables afterwards (cf.\ @{ML
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 40964
diff changeset
   344
  Variable.export} or the combined @{ML "Proof_Context.export"}).  *}
34932
28e231e4144b some examples for basic context operations;
wenzelm
parents: 34930
diff changeset
   345
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20218
diff changeset
   346
34930
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   347
section {* Structured goals and results \label{sec:struct-goals} *}
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20218
diff changeset
   348
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   349
text {*
20472
wenzelm
parents: 20470
diff changeset
   350
  Local results are established by monotonic reasoning from facts
20474
wenzelm
parents: 20472
diff changeset
   351
  within a context.  This allows common combinations of theorems,
wenzelm
parents: 20472
diff changeset
   352
  e.g.\ via @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or equational
wenzelm
parents: 20472
diff changeset
   353
  reasoning, see \secref{sec:thms}.  Unaccounted context manipulations
wenzelm
parents: 20472
diff changeset
   354
  should be avoided, notably raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc
20472
wenzelm
parents: 20470
diff changeset
   355
  references to free variables or assumptions not present in the proof
wenzelm
parents: 20470
diff changeset
   356
  context.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   357
20491
wenzelm
parents: 20474
diff changeset
   358
  \medskip The @{text "SUBPROOF"} combinator allows to structure a
wenzelm
parents: 20474
diff changeset
   359
  tactical proof recursively by decomposing a selected sub-goal:
wenzelm
parents: 20474
diff changeset
   360
  @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"}
wenzelm
parents: 20474
diff changeset
   361
  after fixing @{text "x"} and assuming @{text "A(x)"}.  This means
wenzelm
parents: 20474
diff changeset
   362
  the tactic needs to solve the conclusion, but may use the premise as
wenzelm
parents: 20474
diff changeset
   363
  a local fact, for locally fixed variables.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   364
34930
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   365
  The family of @{text "FOCUS"} combinators is similar to @{text
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   366
  "SUBPROOF"}, but allows to retain schematic variables and pending
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   367
  subgoals in the resulting goal state.
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   368
20491
wenzelm
parents: 20474
diff changeset
   369
  The @{text "prove"} operation provides an interface for structured
wenzelm
parents: 20474
diff changeset
   370
  backwards reasoning under program control, with some explicit sanity
wenzelm
parents: 20474
diff changeset
   371
  checks of the result.  The goal context can be augmented by
wenzelm
parents: 20474
diff changeset
   372
  additional fixed variables (cf.\ \secref{sec:variables}) and
wenzelm
parents: 20474
diff changeset
   373
  assumptions (cf.\ \secref{sec:assumptions}), which will be available
wenzelm
parents: 20474
diff changeset
   374
  as local facts during the proof and discharged into implications in
wenzelm
parents: 20474
diff changeset
   375
  the result.  Type and term variables are generalized as usual,
wenzelm
parents: 20474
diff changeset
   376
  according to the context.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   377
20491
wenzelm
parents: 20474
diff changeset
   378
  The @{text "obtain"} operation produces results by eliminating
wenzelm
parents: 20474
diff changeset
   379
  existing facts by means of a given tactic.  This acts like a dual
wenzelm
parents: 20474
diff changeset
   380
  conclusion: the proof demonstrates that the context may be augmented
34930
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   381
  by parameters and assumptions, without affecting any conclusions
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   382
  that do not mention these parameters.  See also
39851
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   383
  \cite{isabelle-isar-ref} for the user-level @{command obtain} and
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   384
  @{command guess} elements.  Final results, which may not refer to
20491
wenzelm
parents: 20474
diff changeset
   385
  the parameters in the conclusion, need to exported explicitly into
39851
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   386
  the original context.  *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   387
20472
wenzelm
parents: 20470
diff changeset
   388
text %mlref {*
wenzelm
parents: 20470
diff changeset
   389
  \begin{mldecls}
39821
bf164c153d10 minor tuning and updating;
wenzelm
parents: 34932
diff changeset
   390
  @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) ->
bf164c153d10 minor tuning and updating;
wenzelm
parents: 34932
diff changeset
   391
  Proof.context -> int -> tactic"} \\
bf164c153d10 minor tuning and updating;
wenzelm
parents: 34932
diff changeset
   392
  @{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) ->
bf164c153d10 minor tuning and updating;
wenzelm
parents: 34932
diff changeset
   393
  Proof.context -> int -> tactic"} \\
bf164c153d10 minor tuning and updating;
wenzelm
parents: 34932
diff changeset
   394
  @{index_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) ->
bf164c153d10 minor tuning and updating;
wenzelm
parents: 34932
diff changeset
   395
  Proof.context -> int -> tactic"} \\
bf164c153d10 minor tuning and updating;
wenzelm
parents: 34932
diff changeset
   396
  @{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) ->
bf164c153d10 minor tuning and updating;
wenzelm
parents: 34932
diff changeset
   397
  Proof.context -> int -> tactic"} \\
39853
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   398
  @{index_ML Subgoal.focus: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   399
  @{index_ML Subgoal.focus_prems: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   400
  @{index_ML Subgoal.focus_params: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
20547
wenzelm
parents: 20542
diff changeset
   401
  \end{mldecls}
34930
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   402
20547
wenzelm
parents: 20542
diff changeset
   403
  \begin{mldecls}
20472
wenzelm
parents: 20470
diff changeset
   404
  @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
wenzelm
parents: 20470
diff changeset
   405
  ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
wenzelm
parents: 20470
diff changeset
   406
  @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
wenzelm
parents: 20470
diff changeset
   407
  ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
20547
wenzelm
parents: 20542
diff changeset
   408
  \end{mldecls}
wenzelm
parents: 20542
diff changeset
   409
  \begin{mldecls}
39821
bf164c153d10 minor tuning and updating;
wenzelm
parents: 34932
diff changeset
   410
  @{index_ML Obtain.result: "(Proof.context -> tactic) -> thm list ->
bf164c153d10 minor tuning and updating;
wenzelm
parents: 34932
diff changeset
   411
  Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\
20472
wenzelm
parents: 20470
diff changeset
   412
  \end{mldecls}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   413
20472
wenzelm
parents: 20470
diff changeset
   414
  \begin{description}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   415
29761
2b658e50683a minor tuning and typographic fixes;
wenzelm
parents: 29760
diff changeset
   416
  \item @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure
2b658e50683a minor tuning and typographic fixes;
wenzelm
parents: 29760
diff changeset
   417
  of the specified sub-goal, producing an extended context and a
2b658e50683a minor tuning and typographic fixes;
wenzelm
parents: 29760
diff changeset
   418
  reduced goal, which needs to be solved by the given tactic.  All
2b658e50683a minor tuning and typographic fixes;
wenzelm
parents: 29760
diff changeset
   419
  schematic parameters of the goal are imported into the context as
2b658e50683a minor tuning and typographic fixes;
wenzelm
parents: 29760
diff changeset
   420
  fixed ones, which may not be instantiated in the sub-proof.
20491
wenzelm
parents: 20474
diff changeset
   421
34930
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   422
  \item @{ML Subgoal.FOCUS}, @{ML Subgoal.FOCUS_PREMS}, and @{ML
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   423
  Subgoal.FOCUS_PARAMS} are similar to @{ML SUBPROOF}, but are
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   424
  slightly more flexible: only the specified parts of the subgoal are
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   425
  imported into the context, and the body tactic may introduce new
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   426
  subgoals and schematic variables.
f3bce1cc513c added Subgoal.FOCUS;
wenzelm
parents: 32302
diff changeset
   427
39853
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   428
  \item @{ML Subgoal.focus}, @{ML Subgoal.focus_prems}, @{ML
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   429
  Subgoal.focus_params} extract the focus information from a goal
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   430
  state in the same way as the corresponding tacticals above.  This is
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   431
  occasionally useful to experiment without writing actual tactics
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   432
  yet.
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   433
20472
wenzelm
parents: 20470
diff changeset
   434
  \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
20474
wenzelm
parents: 20472
diff changeset
   435
  "C"} in the context augmented by fixed variables @{text "xs"} and
wenzelm
parents: 20472
diff changeset
   436
  assumptions @{text "As"}, and applies tactic @{text "tac"} to solve
wenzelm
parents: 20472
diff changeset
   437
  it.  The latter may depend on the local assumptions being presented
wenzelm
parents: 20472
diff changeset
   438
  as facts.  The result is in HHF normal form.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   439
20472
wenzelm
parents: 20470
diff changeset
   440
  \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
20491
wenzelm
parents: 20474
diff changeset
   441
  states several conclusions simultaneously.  The goal is encoded by
21827
0b1d07f79c1e updated;
wenzelm
parents: 20797
diff changeset
   442
  means of Pure conjunction; @{ML Goal.conjunction_tac} will turn this
0b1d07f79c1e updated;
wenzelm
parents: 20797
diff changeset
   443
  into a collection of individual subgoals.
20472
wenzelm
parents: 20470
diff changeset
   444
20491
wenzelm
parents: 20474
diff changeset
   445
  \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the
wenzelm
parents: 20474
diff changeset
   446
  given facts using a tactic, which results in additional fixed
wenzelm
parents: 20474
diff changeset
   447
  variables and assumptions in the context.  Final results need to be
wenzelm
parents: 20474
diff changeset
   448
  exported explicitly.
20472
wenzelm
parents: 20470
diff changeset
   449
wenzelm
parents: 20470
diff changeset
   450
  \end{description}
wenzelm
parents: 20470
diff changeset
   451
*}
30272
2d612824e642 regenerated document;
wenzelm
parents: 30270
diff changeset
   452
39853
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   453
text %mlex {* The following minimal example illustrates how to access
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   454
  the focus information of a structured goal state. *}
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   455
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40153
diff changeset
   456
notepad
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40153
diff changeset
   457
begin
39853
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   458
  fix A B C :: "'a \<Rightarrow> bool"
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   459
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   460
  have "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   461
    ML_val
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   462
    {*
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   463
      val {goal, context = goal_ctxt, ...} = @{Isar.goal};
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   464
      val (focus as {params, asms, concl, ...}, goal') =
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   465
        Subgoal.focus goal_ctxt 1 goal;
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   466
      val [A, B] = #prems focus;
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   467
      val [(_, x)] = #params focus;
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   468
    *}
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   469
    oops
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   470
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   471
text {* \medskip The next example demonstrates forward-elimination in
a5a731dec31c more examples;
wenzelm
parents: 39851
diff changeset
   472
  a local context, using @{ML Obtain.result}.  *}
39851
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   473
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40153
diff changeset
   474
notepad
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40153
diff changeset
   475
begin
39851
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   476
  assume ex: "\<exists>x. B x"
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   477
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   478
  ML_prf %"ML" {*
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   479
    val ctxt0 = @{context};
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   480
    val (([(_, x)], [B]), ctxt1) = ctxt0
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   481
      |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}];
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   482
  *}
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   483
  ML_prf %"ML" {*
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 40964
diff changeset
   484
    singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl};
39851
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   485
  *}
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   486
  ML_prf %"ML" {*
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 40964
diff changeset
   487
    Proof_Context.export ctxt1 ctxt0 [Thm.reflexive x]
39851
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   488
      handle ERROR msg => (warning msg; []);
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   489
  *}
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40153
diff changeset
   490
end
39851
7219a771ab63 more examples;
wenzelm
parents: 39846
diff changeset
   491
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   492
end