1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/IsarImplementation/Thy/Proof.thy Mon Feb 16 20:47:44 2009 +0100
1.3 @@ -0,0 +1,331 @@
1.4 +theory Proof
1.5 +imports Base
1.6 +begin
1.7 +
1.8 +chapter {* Structured proofs *}
1.9 +
1.10 +section {* Variables \label{sec:variables} *}
1.11 +
1.12 +text {*
1.13 + Any variable that is not explicitly bound by @{text "\<lambda>"}-abstraction
1.14 + is considered as ``free''. Logically, free variables act like
1.15 + outermost universal quantification at the sequent level: @{text
1.16 + "A\<^isub>1(x), \<dots>, A\<^isub>n(x) \<turnstile> B(x)"} means that the result
1.17 + holds \emph{for all} values of @{text "x"}. Free variables for
1.18 + terms (not types) can be fully internalized into the logic: @{text
1.19 + "\<turnstile> B(x)"} and @{text "\<turnstile> \<And>x. B(x)"} are interchangeable, provided
1.20 + that @{text "x"} does not occur elsewhere in the context.
1.21 + Inspecting @{text "\<turnstile> \<And>x. B(x)"} more closely, we see that inside the
1.22 + quantifier, @{text "x"} is essentially ``arbitrary, but fixed'',
1.23 + while from outside it appears as a place-holder for instantiation
1.24 + (thanks to @{text "\<And>"} elimination).
1.25 +
1.26 + The Pure logic represents the idea of variables being either inside
1.27 + or outside the current scope by providing separate syntactic
1.28 + categories for \emph{fixed variables} (e.g.\ @{text "x"}) vs.\
1.29 + \emph{schematic variables} (e.g.\ @{text "?x"}). Incidently, a
1.30 + universal result @{text "\<turnstile> \<And>x. B(x)"} has the HHF normal form @{text
1.31 + "\<turnstile> B(?x)"}, which represents its generality nicely without requiring
1.32 + an explicit quantifier. The same principle works for type
1.33 + variables: @{text "\<turnstile> B(?\<alpha>)"} represents the idea of ``@{text "\<turnstile>
1.34 + \<forall>\<alpha>. B(\<alpha>)"}'' without demanding a truly polymorphic framework.
1.35 +
1.36 + \medskip Additional care is required to treat type variables in a
1.37 + way that facilitates type-inference. In principle, term variables
1.38 + depend on type variables, which means that type variables would have
1.39 + to be declared first. For example, a raw type-theoretic framework
1.40 + would demand the context to be constructed in stages as follows:
1.41 + @{text "\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^isub>\<alpha>)"}.
1.42 +
1.43 + We allow a slightly less formalistic mode of operation: term
1.44 + variables @{text "x"} are fixed without specifying a type yet
1.45 + (essentially \emph{all} potential occurrences of some instance
1.46 + @{text "x\<^isub>\<tau>"} are fixed); the first occurrence of @{text "x"}
1.47 + within a specific term assigns its most general type, which is then
1.48 + maintained consistently in the context. The above example becomes
1.49 + @{text "\<Gamma> = x: term, \<alpha>: type, A(x\<^isub>\<alpha>)"}, where type @{text
1.50 + "\<alpha>"} is fixed \emph{after} term @{text "x"}, and the constraint
1.51 + @{text "x :: \<alpha>"} is an implicit consequence of the occurrence of
1.52 + @{text "x\<^isub>\<alpha>"} in the subsequent proposition.
1.53 +
1.54 + This twist of dependencies is also accommodated by the reverse
1.55 + operation of exporting results from a context: a type variable
1.56 + @{text "\<alpha>"} is considered fixed as long as it occurs in some fixed
1.57 + term variable of the context. For example, exporting @{text "x:
1.58 + term, \<alpha>: type \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} produces in the first step
1.59 + @{text "x: term \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} for fixed @{text "\<alpha>"},
1.60 + and only in the second step @{text "\<turnstile> ?x\<^isub>?\<^isub>\<alpha> =
1.61 + ?x\<^isub>?\<^isub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}.
1.62 +
1.63 + \medskip The Isabelle/Isar proof context manages the gory details of
1.64 + term vs.\ type variables, with high-level principles for moving the
1.65 + frontier between fixed and schematic variables.
1.66 +
1.67 + The @{text "add_fixes"} operation explictly declares fixed
1.68 + variables; the @{text "declare_term"} operation absorbs a term into
1.69 + a context by fixing new type variables and adding syntactic
1.70 + constraints.
1.71 +
1.72 + The @{text "export"} operation is able to perform the main work of
1.73 + generalizing term and type variables as sketched above, assuming
1.74 + that fixing variables and terms have been declared properly.
1.75 +
1.76 + There @{text "import"} operation makes a generalized fact a genuine
1.77 + part of the context, by inventing fixed variables for the schematic
1.78 + ones. The effect can be reversed by using @{text "export"} later,
1.79 + potentially with an extended context; the result is equivalent to
1.80 + the original modulo renaming of schematic variables.
1.81 +
1.82 + The @{text "focus"} operation provides a variant of @{text "import"}
1.83 + for nested propositions (with explicit quantification): @{text
1.84 + "\<And>x\<^isub>1 \<dots> x\<^isub>n. B(x\<^isub>1, \<dots>, x\<^isub>n)"} is
1.85 + decomposed by inventing fixed variables @{text "x\<^isub>1, \<dots>,
1.86 + x\<^isub>n"} for the body.
1.87 +*}
1.88 +
1.89 +text %mlref {*
1.90 + \begin{mldecls}
1.91 + @{index_ML Variable.add_fixes: "
1.92 + string list -> Proof.context -> string list * Proof.context"} \\
1.93 + @{index_ML Variable.variant_fixes: "
1.94 + string list -> Proof.context -> string list * Proof.context"} \\
1.95 + @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
1.96 + @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
1.97 + @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
1.98 + @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
1.99 + @{index_ML Variable.import_thms: "bool -> thm list -> Proof.context ->
1.100 + ((ctyp list * cterm list) * thm list) * Proof.context"} \\
1.101 + @{index_ML Variable.focus: "cterm -> Proof.context -> (cterm list * cterm) * Proof.context"} \\
1.102 + \end{mldecls}
1.103 +
1.104 + \begin{description}
1.105 +
1.106 + \item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term
1.107 + variables @{text "xs"}, returning the resulting internal names. By
1.108 + default, the internal representation coincides with the external
1.109 + one, which also means that the given variables must not be fixed
1.110 + already. There is a different policy within a local proof body: the
1.111 + given names are just hints for newly invented Skolem variables.
1.112 +
1.113 + \item @{ML Variable.variant_fixes} is similar to @{ML
1.114 + Variable.add_fixes}, but always produces fresh variants of the given
1.115 + names.
1.116 +
1.117 + \item @{ML Variable.declare_term}~@{text "t ctxt"} declares term
1.118 + @{text "t"} to belong to the context. This automatically fixes new
1.119 + type variables, but not term variables. Syntactic constraints for
1.120 + type and term variables are declared uniformly, though.
1.121 +
1.122 + \item @{ML Variable.declare_constraints}~@{text "t ctxt"} declares
1.123 + syntactic constraints from term @{text "t"}, without making it part
1.124 + of the context yet.
1.125 +
1.126 + \item @{ML Variable.export}~@{text "inner outer thms"} generalizes
1.127 + fixed type and term variables in @{text "thms"} according to the
1.128 + difference of the @{text "inner"} and @{text "outer"} context,
1.129 + following the principles sketched above.
1.130 +
1.131 + \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
1.132 + variables in @{text "ts"} as far as possible, even those occurring
1.133 + in fixed term variables. The default policy of type-inference is to
1.134 + fix newly introduced type variables, which is essentially reversed
1.135 + with @{ML Variable.polymorphic}: here the given terms are detached
1.136 + from the context as far as possible.
1.137 +
1.138 + \item @{ML Variable.import_thms}~@{text "open thms ctxt"} invents fixed
1.139 + type and term variables for the schematic ones occurring in @{text
1.140 + "thms"}. The @{text "open"} flag indicates whether the fixed names
1.141 + should be accessible to the user, otherwise newly introduced names
1.142 + are marked as ``internal'' (\secref{sec:names}).
1.143 +
1.144 + \item @{ML Variable.focus}~@{text B} decomposes the outermost @{text
1.145 + "\<And>"} prefix of proposition @{text "B"}.
1.146 +
1.147 + \end{description}
1.148 +*}
1.149 +
1.150 +
1.151 +section {* Assumptions \label{sec:assumptions} *}
1.152 +
1.153 +text {*
1.154 + An \emph{assumption} is a proposition that it is postulated in the
1.155 + current context. Local conclusions may use assumptions as
1.156 + additional facts, but this imposes implicit hypotheses that weaken
1.157 + the overall statement.
1.158 +
1.159 + Assumptions are restricted to fixed non-schematic statements, i.e.\
1.160 + all generality needs to be expressed by explicit quantifiers.
1.161 + Nevertheless, the result will be in HHF normal form with outermost
1.162 + quantifiers stripped. For example, by assuming @{text "\<And>x :: \<alpha>. P
1.163 + x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for schematic @{text "?x"}
1.164 + of fixed type @{text "\<alpha>"}. Local derivations accumulate more and
1.165 + more explicit references to hypotheses: @{text "A\<^isub>1, \<dots>,
1.166 + A\<^isub>n \<turnstile> B"} where @{text "A\<^isub>1, \<dots>, A\<^isub>n"} needs to
1.167 + be covered by the assumptions of the current context.
1.168 +
1.169 + \medskip The @{text "add_assms"} operation augments the context by
1.170 + local assumptions, which are parameterized by an arbitrary @{text
1.171 + "export"} rule (see below).
1.172 +
1.173 + The @{text "export"} operation moves facts from a (larger) inner
1.174 + context into a (smaller) outer context, by discharging the
1.175 + difference of the assumptions as specified by the associated export
1.176 + rules. Note that the discharged portion is determined by the
1.177 + difference contexts, not the facts being exported! There is a
1.178 + separate flag to indicate a goal context, where the result is meant
1.179 + to refine an enclosing sub-goal of a structured proof state (cf.\
1.180 + \secref{sec:isar-proof-state}).
1.181 +
1.182 + \medskip The most basic export rule discharges assumptions directly
1.183 + by means of the @{text "\<Longrightarrow>"} introduction rule:
1.184 + \[
1.185 + \infer[(@{text "\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
1.186 + \]
1.187 +
1.188 + The variant for goal refinements marks the newly introduced
1.189 + premises, which causes the canonical Isar goal refinement scheme to
1.190 + enforce unification with local premises within the goal:
1.191 + \[
1.192 + \infer[(@{text "#\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
1.193 + \]
1.194 +
1.195 + \medskip Alternative versions of assumptions may perform arbitrary
1.196 + transformations on export, as long as the corresponding portion of
1.197 + hypotheses is removed from the given facts. For example, a local
1.198 + definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"},
1.199 + with the following export rule to reverse the effect:
1.200 + \[
1.201 + \infer[(@{text "\<equiv>-expand"})]{@{text "\<Gamma> \\ x \<equiv> t \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
1.202 + \]
1.203 + This works, because the assumption @{text "x \<equiv> t"} was introduced in
1.204 + a context with @{text "x"} being fresh, so @{text "x"} does not
1.205 + occur in @{text "\<Gamma>"} here.
1.206 +*}
1.207 +
1.208 +text %mlref {*
1.209 + \begin{mldecls}
1.210 + @{index_ML_type Assumption.export} \\
1.211 + @{index_ML Assumption.assume: "cterm -> thm"} \\
1.212 + @{index_ML Assumption.add_assms:
1.213 + "Assumption.export ->
1.214 + cterm list -> Proof.context -> thm list * Proof.context"} \\
1.215 + @{index_ML Assumption.add_assumes: "
1.216 + cterm list -> Proof.context -> thm list * Proof.context"} \\
1.217 + @{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
1.218 + \end{mldecls}
1.219 +
1.220 + \begin{description}
1.221 +
1.222 + \item @{ML_type Assumption.export} represents arbitrary export
1.223 + rules, which is any function of type @{ML_type "bool -> cterm list -> thm -> thm"},
1.224 + where the @{ML_type "bool"} indicates goal mode, and the @{ML_type
1.225 + "cterm list"} the collection of assumptions to be discharged
1.226 + simultaneously.
1.227 +
1.228 + \item @{ML Assumption.assume}~@{text "A"} turns proposition @{text
1.229 + "A"} into a raw assumption @{text "A \<turnstile> A'"}, where the conclusion
1.230 + @{text "A'"} is in HHF normal form.
1.231 +
1.232 + \item @{ML Assumption.add_assms}~@{text "r As"} augments the context
1.233 + by assumptions @{text "As"} with export rule @{text "r"}. The
1.234 + resulting facts are hypothetical theorems as produced by the raw
1.235 + @{ML Assumption.assume}.
1.236 +
1.237 + \item @{ML Assumption.add_assumes}~@{text "As"} is a special case of
1.238 + @{ML Assumption.add_assms} where the export rule performs @{text
1.239 + "\<Longrightarrow>_intro"} or @{text "#\<Longrightarrow>_intro"}, depending on goal mode.
1.240 +
1.241 + \item @{ML Assumption.export}~@{text "is_goal inner outer thm"}
1.242 + exports result @{text "thm"} from the the @{text "inner"} context
1.243 + back into the @{text "outer"} one; @{text "is_goal = true"} means
1.244 + this is a goal context. The result is in HHF normal form. Note
1.245 + that @{ML "ProofContext.export"} combines @{ML "Variable.export"}
1.246 + and @{ML "Assumption.export"} in the canonical way.
1.247 +
1.248 + \end{description}
1.249 +*}
1.250 +
1.251 +
1.252 +section {* Results \label{sec:results} *}
1.253 +
1.254 +text {*
1.255 + Local results are established by monotonic reasoning from facts
1.256 + within a context. This allows common combinations of theorems,
1.257 + e.g.\ via @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or equational
1.258 + reasoning, see \secref{sec:thms}. Unaccounted context manipulations
1.259 + should be avoided, notably raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc
1.260 + references to free variables or assumptions not present in the proof
1.261 + context.
1.262 +
1.263 + \medskip The @{text "SUBPROOF"} combinator allows to structure a
1.264 + tactical proof recursively by decomposing a selected sub-goal:
1.265 + @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"}
1.266 + after fixing @{text "x"} and assuming @{text "A(x)"}. This means
1.267 + the tactic needs to solve the conclusion, but may use the premise as
1.268 + a local fact, for locally fixed variables.
1.269 +
1.270 + The @{text "prove"} operation provides an interface for structured
1.271 + backwards reasoning under program control, with some explicit sanity
1.272 + checks of the result. The goal context can be augmented by
1.273 + additional fixed variables (cf.\ \secref{sec:variables}) and
1.274 + assumptions (cf.\ \secref{sec:assumptions}), which will be available
1.275 + as local facts during the proof and discharged into implications in
1.276 + the result. Type and term variables are generalized as usual,
1.277 + according to the context.
1.278 +
1.279 + The @{text "obtain"} operation produces results by eliminating
1.280 + existing facts by means of a given tactic. This acts like a dual
1.281 + conclusion: the proof demonstrates that the context may be augmented
1.282 + by certain fixed variables and assumptions. See also
1.283 + \cite{isabelle-isar-ref} for the user-level @{text "\<OBTAIN>"} and
1.284 + @{text "\<GUESS>"} elements. Final results, which may not refer to
1.285 + the parameters in the conclusion, need to exported explicitly into
1.286 + the original context.
1.287 +*}
1.288 +
1.289 +text %mlref {*
1.290 + \begin{mldecls}
1.291 + @{index_ML SUBPROOF:
1.292 + "({context: Proof.context, schematics: ctyp list * cterm list,
1.293 + params: cterm list, asms: cterm list, concl: cterm,
1.294 + prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\
1.295 + \end{mldecls}
1.296 + \begin{mldecls}
1.297 + @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
1.298 + ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
1.299 + @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
1.300 + ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
1.301 + \end{mldecls}
1.302 + \begin{mldecls}
1.303 + @{index_ML Obtain.result: "(Proof.context -> tactic) ->
1.304 + thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\
1.305 + \end{mldecls}
1.306 +
1.307 + \begin{description}
1.308 +
1.309 + \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a
1.310 + particular sub-goal, producing an extended context and a reduced
1.311 + goal, which needs to be solved by the given tactic. All schematic
1.312 + parameters of the goal are imported into the context as fixed ones,
1.313 + which may not be instantiated in the sub-proof.
1.314 +
1.315 + \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
1.316 + "C"} in the context augmented by fixed variables @{text "xs"} and
1.317 + assumptions @{text "As"}, and applies tactic @{text "tac"} to solve
1.318 + it. The latter may depend on the local assumptions being presented
1.319 + as facts. The result is in HHF normal form.
1.320 +
1.321 + \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
1.322 + states several conclusions simultaneously. The goal is encoded by
1.323 + means of Pure conjunction; @{ML Goal.conjunction_tac} will turn this
1.324 + into a collection of individual subgoals.
1.325 +
1.326 + \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the
1.327 + given facts using a tactic, which results in additional fixed
1.328 + variables and assumptions in the context. Final results need to be
1.329 + exported explicitly.
1.330 +
1.331 + \end{description}
1.332 +*}
1.333 +
1.334 +end