152 text_raw {*\end{minipage}*} |
152 text_raw {*\end{minipage}*} |
153 |
153 |
154 text {* |
154 text {* |
155 \medskip\noindent This Isar reasoning pattern again refers to the |
155 \medskip\noindent This Isar reasoning pattern again refers to the |
156 primitive rule depicted above. The system determines it in the |
156 primitive rule depicted above. The system determines it in the |
157 ``@{command "proof"}'' step, which could have been spelt out more |
157 ``@{command proof}'' step, which could have been spelt out more |
158 explicitly as ``@{command "proof"}~@{text "(rule InterI)"}''. Note |
158 explicitly as ``@{command proof}~@{text "(rule InterI)"}''. Note |
159 that the rule involves both a local parameter @{term "A"} and an |
159 that the rule involves both a local parameter @{term "A"} and an |
160 assumption @{prop "A \<in> \<A>"} in the nested reasoning. This kind of |
160 assumption @{prop "A \<in> \<A>"} in the nested reasoning. This kind of |
161 compound rule typically demands a genuine sub-proof in Isar, working |
161 compound rule typically demands a genuine sub-proof in Isar, working |
162 backwards rather than forwards as seen before. In the proof body we |
162 backwards rather than forwards as seen before. In the proof body we |
163 encounter the @{command "fix"}-@{command "assume"}-@{command "show"} |
163 encounter the @{command fix}-@{command assume}-@{command show} |
164 skeleton of nested sub-proofs that is typical for Isar. The final |
164 outline of nested sub-proofs that is typical for Isar. The final |
165 @{command "show"} is like @{command "have"} followed by an |
165 @{command show} is like @{command have} followed by an additional |
166 additional refinement of the enclosing claim, using the rule derived |
166 refinement of the enclosing claim, using the rule derived from the |
167 from the proof body. |
167 proof body. |
168 |
168 |
169 \medskip The next example involves @{term "\<Union>\<A>"}, which can be |
169 \medskip The next example involves @{term "\<Union>\<A>"}, which can be |
170 characterized as the set of all @{term "x"} such that @{prop "\<exists>A. x |
170 characterized as the set of all @{term "x"} such that @{prop "\<exists>A. x |
171 \<in> A \<and> A \<in> \<A>"}. The elimination rule for @{prop "x \<in> \<Union>\<A>"} does |
171 \<in> A \<and> A \<in> \<A>"}. The elimination rule for @{prop "x \<in> \<Union>\<A>"} does |
172 not mention @{text "\<exists>"} and @{text "\<and>"} at all, but admits to obtain |
172 not mention @{text "\<exists>"} and @{text "\<and>"} at all, but admits to obtain |
492 Pure (and the object-logic). A @{text "pattern"} is a @{text |
491 Pure (and the object-logic). A @{text "pattern"} is a @{text |
493 "term"} with schematic variables, to be bound by higher-order |
492 "term"} with schematic variables, to be bound by higher-order |
494 matching. |
493 matching. |
495 |
494 |
496 \medskip Facts may be referenced by name or proposition. For |
495 \medskip Facts may be referenced by name or proposition. For |
497 example, the result of ``@{command "have"}~@{text "a: A \<langle>proof\<rangle>"}'' |
496 example, the result of ``@{command have}~@{text "a: A \<langle>proof\<rangle>"}'' |
498 becomes available both as @{text "a"} and |
497 becomes available both as @{text "a"} and |
499 \isacharbackquoteopen@{text "A"}\isacharbackquoteclose. Moreover, |
498 \isacharbackquoteopen@{text "A"}\isacharbackquoteclose. Moreover, |
500 fact expressions may involve attributes that modify either the |
499 fact expressions may involve attributes that modify either the |
501 theorem or the background context. For example, the expression |
500 theorem or the background context. For example, the expression |
502 ``@{text "a [OF b]"}'' refers to the composition of two facts |
501 ``@{text "a [OF b]"}'' refers to the composition of two facts |
503 according to the @{inference resolution} inference of |
502 according to the @{inference resolution} inference of |
504 \secref{sec:framework-resolution}, while ``@{text "a [intro]"}'' |
503 \secref{sec:framework-resolution}, while ``@{text "a [intro]"}'' |
505 declares a fact as introduction rule in the context. |
504 declares a fact as introduction rule in the context. |
506 |
505 |
507 The special fact called ``@{fact this}'' always refers to the last |
506 The special fact called ``@{fact this}'' always refers to the last |
508 result, as produced by @{command note}, @{text "\<ASSM>"}, @{command |
507 result, as produced by @{command note}, @{command assume}, @{command |
509 "have"}, or @{command "show"}. Since @{command "note"} occurs |
508 have}, or @{command show}. Since @{command note} occurs |
510 frequently together with @{command "then"} we provide some |
509 frequently together with @{command then} we provide some |
511 abbreviations: ``@{command "from"}~@{text a}'' for ``@{command |
510 abbreviations: |
512 "note"}~@{text a}~@{command "then"}'', and ``@{command |
511 |
513 "with"}~@{text a}'' for ``@{command "from"}~@{text a}~@{keyword |
512 \medskip |
514 "and"}~@{fact this}''. |
513 \begin{tabular}{rcl} |
515 |
514 @{command from}~@{text a} & @{text "\<equiv>"} & @{command note}~@{text a}~@{command then} \\ |
516 \medskip The @{text "method"} category is essentially a parameter |
515 @{command with}~@{text a} & @{text "\<equiv>"} & @{command from}~@{text "a \<AND> this"} \\ |
517 and may be populated later. Methods use the facts indicated by |
516 \end{tabular} |
518 @{command "then"} or @{command "using"}, and then operate on the |
517 \medskip |
519 goal state. Some basic methods are predefined: ``@{method "-"}'' |
518 |
520 leaves the goal unchanged, ``@{method this}'' applies the facts as |
519 The @{text "method"} category is essentially a parameter and may be |
521 rules to the goal, ``@{method "rule"}'' applies the facts to another |
520 populated later. Methods use the facts indicated by @{command |
522 rule and the result to the goal (both ``@{method this}'' and |
521 "then"} or @{command using}, and then operate on the goal state. |
523 ``@{method rule}'' refer to @{inference resolution} of |
522 Some basic methods are predefined: ``@{method "-"}'' leaves the goal |
|
523 unchanged, ``@{method this}'' applies the facts as rules to the |
|
524 goal, ``@{method "rule"}'' applies the facts to another rule and the |
|
525 result to the goal (both ``@{method this}'' and ``@{method rule}'' |
|
526 refer to @{inference resolution} of |
524 \secref{sec:framework-resolution}). The secondary arguments to |
527 \secref{sec:framework-resolution}). The secondary arguments to |
525 ``@{method rule}'' may be specified explicitly as in ``@{text "(rule |
528 ``@{method rule}'' may be specified explicitly as in ``@{text "(rule |
526 a)"}'', or picked from the context. In the latter case, the system |
529 a)"}'', or picked from the context. In the latter case, the system |
527 first tries rules declared as @{attribute (Pure) elim} or |
530 first tries rules declared as @{attribute (Pure) elim} or |
528 @{attribute (Pure) dest}, followed by those declared as @{attribute |
531 @{attribute (Pure) dest}, followed by those declared as @{attribute |
529 (Pure) intro}. |
532 (Pure) intro}. |
530 |
533 |
531 The default method for @{command "proof"} is ``@{method rule}'' |
534 The default method for @{command proof} is ``@{method rule}'' |
532 (arguments picked from the context), for @{command "qed"} it is |
535 (arguments picked from the context), for @{command qed} it is |
533 ``@{method "-"}''. Further abbreviations for terminal proof steps |
536 ``@{method "-"}''. Further abbreviations for terminal proof steps |
534 are ``@{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for |
537 are ``@{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for |
535 ``@{command "proof"}~@{text "method\<^sub>1"}~@{command |
538 ``@{command proof}~@{text "method\<^sub>1"}~@{command qed}~@{text |
536 "qed"}~@{text "method\<^sub>2"}'', and ``@{command ".."}'' for |
539 "method\<^sub>2"}'', and ``@{command ".."}'' for ``@{command |
537 ``@{command "by"}~@{method rule}, and ``@{command "."}'' for |
540 "by"}~@{method rule}, and ``@{command "."}'' for ``@{command |
538 ``@{command "by"}~@{method this}''. The @{command "unfolding"} |
541 "by"}~@{method this}''. The @{command unfolding} element operates |
539 element operates directly on the current facts and goal by applying |
542 directly on the current facts and goal by applying equalities. |
540 equalities. |
543 |
541 |
544 \medskip Block structure can be indicated explicitly by ``@{command |
542 \medskip Block structure can be indicated explicitly by |
545 "{"}~@{text "\<dots>"}~@{command "}"}'', although the body of a sub-proof |
543 ``@{command "{"}~@{text "\<dots>"}~@{command "}"}'', although the body of |
546 already involves implicit nesting. In any case, @{command next} |
544 a sub-proof already involves implicit nesting. In any case, |
547 jumps into the next section of a block, i.e.\ it acts like closing |
545 @{command "next"} jumps into the next section of a block, i.e.\ it |
548 an implicit block scope and opening another one; there is no direct |
546 acts like closing an implicit block scope and opening another one; |
549 correspondence to subgoals here. |
547 there is no direct correspondence to subgoals here. |
550 |
548 |
551 The remaining elements @{command fix} and @{command assume} build up |
549 The remaining elements @{command "fix"} and @{text "\<ASSM>"} build |
552 a local context (see \secref{sec:framework-context}), while |
550 up a local context (see \secref{sec:framework-context}), while |
553 @{command show} refines a pending sub-goal by the rule resulting |
551 @{command "show"} refines a pending sub-goal by the rule resulting |
|
552 from a nested sub-proof (see \secref{sec:framework-subproof}). |
554 from a nested sub-proof (see \secref{sec:framework-subproof}). |
553 Further derived concepts will support calculational reasoning (see |
555 Further derived concepts will support calculational reasoning (see |
554 \secref{sec:framework-calc}). |
556 \secref{sec:framework-calc}). |
555 *} |
557 *} |
556 |
558 |
561 In judgments @{text "\<Gamma> \<turnstile> \<phi>"} of the primitive framework, @{text "\<Gamma>"} |
563 In judgments @{text "\<Gamma> \<turnstile> \<phi>"} of the primitive framework, @{text "\<Gamma>"} |
562 essentially acts like a proof context. Isar elaborates this idea |
564 essentially acts like a proof context. Isar elaborates this idea |
563 towards a higher-level notion, with additional information for |
565 towards a higher-level notion, with additional information for |
564 type-inference, term abbreviations, local facts, hypotheses etc. |
566 type-inference, term abbreviations, local facts, hypotheses etc. |
565 |
567 |
566 The element @{command "fix"}~@{text "x :: \<alpha>"} declares a local |
568 The element @{command fix}~@{text "x :: \<alpha>"} declares a local |
567 parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in |
569 parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in |
568 results exported from the context, @{text "x"} may become anything. |
570 results exported from the context, @{text "x"} may become anything. |
569 The @{text "\<ASSM>"} element provides a general interface to |
571 The @{command assume}~@{text "\<guillemotleft>inference\<guillemotright>"} element provides a |
570 hypotheses: ``@{text "\<ASSM> \<guillemotleft>inference\<guillemotright> A"}'' produces @{text "A \<turnstile> |
572 general interface to hypotheses: ``@{command assume}~@{text |
571 A"} locally, while the included inference tells how to discharge |
573 "\<guillemotleft>inference\<guillemotright> A"}'' produces @{text "A \<turnstile> A"} locally, while the |
572 @{text "A"} from results @{text "A \<turnstile> B"} later on. There is no |
574 included inference tells how to discharge @{text A} from results |
573 user-syntax for @{text "\<guillemotleft>inference\<guillemotright>"}, i.e.\ @{text "\<ASSM>"} may |
575 @{text "A \<turnstile> B"} later on. There is no user-syntax for @{text |
574 only occur in derived elements that provide a suitable inference |
576 "\<guillemotleft>inference\<guillemotright>"}, i.e.\ it may only occur internally when derived |
575 internally. In particular, ``@{command "assume"}~@{text A}'' |
577 commands are defined in ML. |
576 abbreviates ``@{text "\<ASSM> \<guillemotleft>discharge\<guillemotright> A"}'', and ``@{command |
578 |
577 "def"}~@{text "x \<equiv> a"}'' abbreviates ``@{command "fix"}~@{text "x |
579 At the user-level, the default inference for @{command assume} is |
578 \<ASSM> \<guillemotleft>expansion\<guillemotright> x \<equiv> a"}'', involving the following inferences: |
580 @{inference discharge} as given below. The additional variants |
579 |
581 @{command presume} and @{command def} are defined as follows: |
580 \[ |
582 |
581 \infer[(@{inference_def "discharge"})]{@{text "\<strut>\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}} |
583 \medskip |
582 \qquad |
584 \begin{tabular}{rcl} |
|
585 @{command presume}~@{text A} & @{text "\<equiv>"} & @{command assume}~@{text "\<guillemotleft>weak\<dash>discharge\<guillemotright> A"} \\ |
|
586 @{command def}~@{text "x \<equiv> a"} & @{text "\<equiv>"} & @{command fix}~@{text x}~@{command assume}~@{text "\<guillemotleft>expansion\<guillemotright> x \<equiv> a"} \\ |
|
587 \end{tabular} |
|
588 \medskip |
|
589 |
|
590 \[ |
|
591 \infer[(@{inference_def discharge})]{@{text "\<strut>\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}} |
|
592 \] |
|
593 \[ |
|
594 \infer[(@{inference_def "weak\<dash>discharge"})]{@{text "\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}} |
|
595 \] |
|
596 \[ |
583 \infer[(@{inference_def expansion})]{@{text "\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a"}}{@{text "\<strut>\<Gamma> \<turnstile> B x"}} |
597 \infer[(@{inference_def expansion})]{@{text "\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a"}}{@{text "\<strut>\<Gamma> \<turnstile> B x"}} |
584 \] |
598 \] |
585 |
599 |
586 \medskip The most interesting derived element in Isar is @{command |
600 \medskip Note that @{inference discharge} and @{inference |
587 "obtain"} \cite[\S5.3]{Wenzel-PhD}, which supports generalized |
601 "weak\<dash>discharge"} differ in the marker for @{prop A}, which is |
588 elimination steps in a purely forward manner. |
602 relevant when the result of a @{command fix}-@{command |
589 |
603 assume}-@{command show} outline is composed with a pending goal, |
590 The @{command "obtain"} element takes a specification of parameters |
604 cf.\ \secref{sec:framework-subproof}. |
591 @{text "\<^vec>x"} and assumptions @{text "\<^vec>A"} to be added to |
605 |
592 the context, together with a proof of a case rule stating that this |
606 The most interesting derived context element in Isar is @{command |
593 extension is conservative (i.e.\ may be removed from closed results |
607 obtain} \cite[\S5.3]{Wenzel-PhD}, which supports generalized |
594 later on): |
608 elimination steps in a purely forward manner. The @{command obtain} |
|
609 element takes a specification of parameters @{text "\<^vec>x"} and |
|
610 assumptions @{text "\<^vec>A"} to be added to the context, together |
|
611 with a proof of a case rule stating that this extension is |
|
612 conservative (i.e.\ may be removed from closed results later on): |
595 |
613 |
596 \medskip |
614 \medskip |
597 \begin{tabular}{l} |
615 \begin{tabular}{l} |
598 @{text "\<langle>facts\<rangle>"}~~@{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x \<langle>proof\<rangle> \<equiv>"} \\[0.5ex] |
616 @{text "\<langle>facts\<rangle>"}~~@{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x \<langle>proof\<rangle> \<equiv>"} \\[0.5ex] |
599 \quad @{command have}~@{text "case: \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<rangle>"} \\ |
617 \quad @{command have}~@{text "case: \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<rangle>"} \\ |
600 \quad @{command proof}~@{method "-"} \\ |
618 \quad @{command proof}~@{method "-"} \\ |
601 \qquad @{command fix}~@{text thesis} \\ |
619 \qquad @{command fix}~@{text thesis} \\ |
602 \qquad @{command assume}~@{text "[intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\ |
620 \qquad @{command assume}~@{text "[intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\ |
603 \qquad @{command show}~@{text thesis}~@{command using}~@{text "\<langle>facts\<rangle> \<langle>proof\<rangle>"} \\ |
621 \qquad @{command show}~@{text thesis}~@{command using}~@{text "\<langle>facts\<rangle> \<langle>proof\<rangle>"} \\ |
604 \quad @{command qed} \\ |
622 \quad @{command qed} \\ |
605 \quad @{command fix}~@{text "\<^vec>x \<ASSM> \<guillemotleft>elimination case\<guillemotright> \<^vec>A \<^vec>x"} \\ |
623 \quad @{command fix}~@{text "\<^vec>x"}~@{command assume}~@{text "\<guillemotleft>elimination case\<guillemotright> \<^vec>A \<^vec>x"} \\ |
606 \end{tabular} |
624 \end{tabular} |
607 \medskip |
625 \medskip |
608 |
626 |
609 \[ |
627 \[ |
610 \infer[(@{inference elimination})]{@{text "\<Gamma> \<turnstile> B"}}{ |
628 \infer[(@{inference elimination})]{@{text "\<Gamma> \<turnstile> B"}}{ |
617 \] |
635 \] |
618 |
636 |
619 \noindent Here the name ``@{text thesis}'' is a specific convention |
637 \noindent Here the name ``@{text thesis}'' is a specific convention |
620 for an arbitrary-but-fixed proposition; in the primitive natural |
638 for an arbitrary-but-fixed proposition; in the primitive natural |
621 deduction rules shown before we have occasionally used @{text C}. |
639 deduction rules shown before we have occasionally used @{text C}. |
622 The whole statement of ``@{command "obtain"}~@{text x}~@{keyword |
640 The whole statement of ``@{command obtain}~@{text x}~@{keyword |
623 "where"}~@{text "A x"}'' may be read as a claim that @{text "A x"} |
641 "where"}~@{text "A x"}'' may be read as a claim that @{text "A x"} |
624 may be assumed for some arbitrary-but-fixed @{text "x"}. Also note |
642 may be assumed for some arbitrary-but-fixed @{text "x"}. Also note |
625 that ``@{command "obtain"}~@{text A}~@{keyword "and"}~@{text B}'' |
643 that ``@{command obtain}~@{text "A \<AND> B"}'' without parameters |
626 without parameters is similar to ``@{command "have"}~@{text |
644 is similar to ``@{command have}~@{text "A \<AND> B"}'', but the |
627 A}~@{keyword "and"}~@{text B}'', but the latter involves multiple |
645 latter involves multiple sub-goals. |
628 sub-goals. |
|
629 |
646 |
630 \medskip The subsequent Isar proof texts explain all context |
647 \medskip The subsequent Isar proof texts explain all context |
631 elements introduced above using the formal proof language itself. |
648 elements introduced above using the formal proof language itself. |
632 After finishing a local proof within a block, we indicate the |
649 After finishing a local proof within a block, we indicate the |
633 exported result via @{command "note"}. This illustrates the meaning |
650 exported result via @{command note}. This illustrates the meaning |
634 of Isar context elements without goals getting in between. |
651 of Isar context elements without goals getting in between. |
635 *} |
652 *} |
636 |
653 |
637 (*<*) |
654 (*<*) |
638 theorem True |
655 theorem True |