10 An Isar proof body serves as mathematical notepad to compose logical
11 content, consisting of types, terms, facts.
15 subsection {* Types and terms *}
19 txt {* Locally fixed entities: *}
20 fix x -- {* local constant, without any type information yet *}
21 fix x :: 'a -- {* variant with explicit type-constraint for subsequent use*}
24 assume "a = b" -- {* type assignment at first occurrence in concrete term *}
26 txt {* Definitions (non-polymorphic): *}
27 def x \<equiv> "t::'a"
29 txt {* Abbreviations (polymorphic): *}
30 let ?f = "\<lambda>x. x"
38 subsection {* Facts *}
41 A fact is a simultaneous list of theorems.
45 subsubsection {* Producing facts *}
50 txt {* Via assumption (``lambda''): *}
53 txt {* Via proof (``let''): *}
56 txt {* Via abbreviation (``let''): *}
62 subsubsection {* Referencing facts *}
66 txt {* Via explicit name: *}
70 txt {* Via implicit name: *}
74 txt {* Via literal proposition (unification with results from the proof text): *}
84 subsubsection {* Manipulating facts *}
88 txt {* Instantiation: *}
89 assume a: "\<And>x. B x"
94 txt {* Backchaining: *}
96 assume 2: "A \<Longrightarrow> C"
100 txt {* Symmetric results: *}
102 note this [symmetric]
104 assume "x \<noteq> y"
105 note this [symmetric]
107 txt {* Adhoc-simplification (take care!): *}
109 note this [simplified]
113 subsubsection {* Projections *}
116 Isar facts consist of multiple theorems. There is notation to project
122 assume stuff: A B C D
129 subsubsection {* Naming conventions *}
134 \item Lower-case identifiers are usually preferred.
136 \item Facts can be named after the main term within the proposition.
138 \item Facts should \emph{not} be named after the command that
139 introduced them (@{command "assume"}, @{command "have"}). This is
140 misleading and hard to maintain.
142 \item Natural numbers can be used as ``meaningless'' names (more
143 appropriate than @{text "a1"}, @{text "a2"} etc.)
145 \item Symbolic identifiers are supported (e.g. @{text "*"}, @{text
146 "**"}, @{text "***"}).
152 subsection {* Block structure *}
155 The formal notepad is block structured. The fact produced by the last
156 entry of a block is exported into the outer context.
171 text {* Explicit blocks as well as implicit blocks of nested goal
172 statements (e.g.\ @{command have}) automatically introduce one extra
173 pair of parentheses in reserve. The @{command next} command allows
174 to ``jump'' between these sub-blocks. *}
192 txt {* Alternative version with explicit parentheses everywhere: *}
217 section {* Calculational reasoning \label{sec:calculations-synopsis} *}
220 For example, see @{file "~~/src/HOL/Isar_Examples/Group.thy"}.
224 subsection {* Special names in Isar proofs *}
229 \item term @{text "?thesis"} --- the main conclusion of the
230 innermost pending claim
232 \item term @{text "\<dots>"} --- the argument of the last explicitly
233 stated result (for infix application this is the right-hand side)
235 \item fact @{text "this"} --- the last result produced in the text
246 term ?thesis -- {* static! *}
252 text {* Calculational reasoning maintains the special fact called
253 ``@{text calculation}'' in the background. Certain language
254 elements combine primary @{text this} with secondary @{text
258 subsection {* Transitive chains *}
260 text {* The Idea is to combine @{text this} and @{text calculation}
261 via typical @{text trans} rules (see also @{command
262 print_trans_rules}): *}
270 txt {* Plain bottom-up calculation: *}
279 txt {* Variant using the @{text "\<dots>"} abbreviation: *}
282 have "\<dots> = c" sorry
284 have "\<dots> = d" sorry
288 txt {* Top-down version with explicit claim at the head: *}
293 have "\<dots> = c" sorry
295 have "\<dots> = d" sorry
300 txt {* Mixed inequalities (require suitable base type): *}
305 have "b \<le> c" sorry
313 subsubsection {* Notes *}
318 \item The notion of @{text trans} rule is very general due to the
319 flexibility of Isabelle/Pure rule composition.
321 \item User applications may declare their own rules, with some care
322 about the operational details of higher-order unification.
328 subsection {* Degenerate calculations and bigstep reasoning *}
330 text {* The Idea is to append @{text this} to @{text calculation},
331 without rule composition. *}
335 txt {* A vacuous proof: *}
344 txt {* Slightly more content (trivial bigstep reasoning): *}
351 have "A \<and> B \<and> C" by blast
353 txt {* More ambitious bigstep reasoning involving structured results: *}
354 have "A \<or> B \<or> C" sorry
356 { assume A have R sorry }
358 { assume B have R sorry }
360 { assume C have R sorry }
362 have R by blast -- {* ``big-bang integration'' of proof blocks (occasionally fragile) *}
366 section {* Induction *}
368 subsection {* Induction as Natural Deduction *}
370 text {* In principle, induction is just a special case of Natural
371 Deduction (see also \secref{sec:natural-deduction-synopsis}). For
375 print_statement nat.induct
381 proof (rule nat.induct) -- {* fragile rule application! *}
386 show "P (Suc n)" sorry
391 In practice, much more proof infrastructure is required.
393 The proof method @{method induct} provides:
396 \item implicit rule selection and robust instantiation
398 \item context elements via symbolic case names
400 \item support for rule-structured induction statements, with local
401 parameters, premises, etc.
415 from Suc.hyps show ?case sorry
420 subsubsection {* Example *}
423 The subsequent example combines the following proof patterns:
426 \item outermost induction (over the datatype structure of natural
427 numbers), to decompose the proof problem in top-down manner
429 \item calculational reasoning (\secref{sec:calculations-synopsis})
430 to compose the result in each case
432 \item solving local claims within the calculation by simplification
439 shows "(\<Sum>i=0..n. i) = n * (n + 1) div 2"
442 have "(\<Sum>i=0..0. i) = (0::nat)" by simp
443 also have "\<dots> = 0 * (0 + 1) div 2" by simp
447 have "(\<Sum>i=0..Suc n. i) = (\<Sum>i=0..n. i) + (n + 1)" by simp
448 also have "\<dots> = n * (n + 1) div 2 + (n + 1)" by (simp add: Suc.hyps)
449 also have "\<dots> = (n * (n + 1) + 2 * (n + 1)) div 2" by simp
450 also have "\<dots> = (Suc n * (Suc n + 1)) div 2" by simp
454 text {* This demonstrates how induction proofs can be done without
455 having to consider the raw Natural Deduction structure. *}
458 subsection {* Induction with local parameters and premises *}
460 text {* Idea: Pure rule statements are passed through the induction
461 rule. This achieves convenient proof patterns, thanks to some
462 internal trickery in the @{method induct} method.
464 Important: Using compact HOL formulae with @{text "\<forall>/\<longrightarrow>"} is a
465 well-known anti-pattern! It would produce useless formal noise.
471 fix P :: "nat \<Rightarrow> bool"
472 fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool"
480 from `P n` show "P (Suc n)" sorry
483 have "A n \<Longrightarrow> P n"
486 from `A 0` show "P 0" sorry
489 from `A n \<Longrightarrow> P n`
490 and `A (Suc n)` show "P (Suc n)" sorry
493 have "\<And>x. Q x n"
499 from `\<And>x. Q x n` show "Q x (Suc n)" sorry
500 txt {* Local quantification admits arbitrary instances: *}
501 note `Q a n` and `Q b n`
506 subsection {* Implicit induction context *}
508 text {* The @{method induct} method can isolate local parameters and
509 premises directly from the given statement. This is convenient in
510 practical applications, but requires some understanding of what is
511 going on internally (as explained above). *}
516 fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool"
521 proof (induct n arbitrary: x)
523 from `A x 0` show "Q x 0" sorry
526 from `\<And>x. A x n \<Longrightarrow> Q x n` -- {* arbitrary instances can be produced here *}
527 and `A x (Suc n)` show "Q x (Suc n)" sorry
532 subsection {* Advanced induction with term definitions *}
534 text {* Induction over subexpressions of a certain shape are delicate
535 to formalize. The Isar @{method induct} method provides
536 infrastructure for this.
538 Idea: sub-expressions of the problem are turned into a defined
539 induction variable; often accompanied with fixing of auxiliary
540 parameters in the original expression. *}
544 fix a :: "'a \<Rightarrow> nat"
545 fix A :: "nat \<Rightarrow> bool"
549 proof (induct "a x" arbitrary: x)
551 note prem = `A (a x)`
556 note hyp = `\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)`
558 and defn = `Suc n = a x`
564 section {* Natural Deduction \label{sec:natural-deduction-synopsis} *}
566 subsection {* Rule statements *}
569 Isabelle/Pure ``theorems'' are always natural deduction rules,
570 which sometimes happen to consist of a conclusion only.
572 The framework connectives @{text "\<And>"} and @{text "\<Longrightarrow>"} indicate the
573 rule structure declaratively. For example: *}
580 The object-logic is embedded into the Pure framework via an implicit
581 derivability judgment @{term "Trueprop :: bool \<Rightarrow> prop"}.
583 Thus any HOL formulae appears atomic to the Pure framework, while
584 the rule structure outlines the corresponding proof pattern.
586 This can be made explicit as follows:
591 write Trueprop ("Tr")
599 Isar provides first-class notation for rule statements as follows.
602 print_statement conjI
604 print_statement nat.induct
607 subsubsection {* Examples *}
610 Introductions and eliminations of some standard connectives of
611 the object-logic can be written as rule statements as follows. (The
612 proof ``@{command "by"}~@{method blast}'' serves as sanity check.)
615 lemma "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P" by blast
616 lemma "\<not> P \<Longrightarrow> P \<Longrightarrow> Q" by blast
618 lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" by blast
619 lemma "P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R" by blast
621 lemma "P \<Longrightarrow> P \<or> Q" by blast
622 lemma "Q \<Longrightarrow> P \<or> Q" by blast
623 lemma "P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" by blast
625 lemma "(\<And>x. P x) \<Longrightarrow> (\<forall>x. P x)" by blast
626 lemma "(\<forall>x. P x) \<Longrightarrow> P x" by blast
628 lemma "P x \<Longrightarrow> (\<exists>x. P x)" by blast
629 lemma "(\<exists>x. P x) \<Longrightarrow> (\<And>x. P x \<Longrightarrow> R) \<Longrightarrow> R" by blast
631 lemma "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B" by blast
632 lemma "x \<in> A \<inter> B \<Longrightarrow> (x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast
634 lemma "x \<in> A \<Longrightarrow> x \<in> A \<union> B" by blast
635 lemma "x \<in> B \<Longrightarrow> x \<in> A \<union> B" by blast
636 lemma "x \<in> A \<union> B \<Longrightarrow> (x \<in> A \<Longrightarrow> R) \<Longrightarrow> (x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast
639 subsection {* Isar context elements *}
641 text {* We derive some results out of the blue, using Isar context
642 elements and some explicit blocks. This illustrates their meaning
643 wrt.\ Pure connectives, without goal states getting in the way. *}
651 have "\<And>x. B x" by fact
659 have "A \<Longrightarrow> B" by fact
672 obtain x :: 'a where "B x" sorry
680 subsection {* Pure rule composition *}
683 The Pure framework provides means for:
687 \item backward-chaining of rules by @{inference resolution}
689 \item closing of branches by @{inference assumption}
693 Both principles involve higher-order unification of @{text \<lambda>}-terms
694 modulo @{text "\<alpha>\<beta>\<eta>"}-equivalence (cf.\ Huet and Miller). *}
700 thm conjI [of A B] -- "instantiation"
701 thm conjI [of A B, OF a b] -- "instantiation and composition"
702 thm conjI [OF a b] -- "composition via unification (trivial)"
703 thm conjI [OF `A` `B`]
705 thm conjI [OF disjI1]
708 text {* Note: Low-level rule composition is tedious and leads to
709 unreadable~/ unmaintainable expressions in the text. *}
712 subsection {* Structured backward reasoning *}
714 text {* Idea: Canonical proof decomposition via @{command fix}~/
715 @{command assume}~/ @{command show}, where the body produces a
716 natural deduction rule to refine some goal. *}
720 fix A B :: "'a \<Rightarrow> bool"
722 have "\<And>x. A x \<Longrightarrow> B x"
729 have "\<And>x. A x \<Longrightarrow> B x"
735 } -- "implicit block structure made explicit"
736 note `\<And>x. A x \<Longrightarrow> B x`
737 -- "side exit for the resulting rule"
742 subsection {* Structured rule application *}
745 Idea: Previous facts and new claims are composed with a rule from
746 the context (or background library).
751 assume r1: "A \<Longrightarrow> B \<Longrightarrow> C" -- {* simple rule (Horn clause) *}
753 have A sorry -- "prefix of facts via outer sub-proof"
756 show B sorry -- "remaining rule premises via inner sub-proof"
771 then have C by (rule r1)
775 assume r2: "A \<Longrightarrow> (\<And>x. B1 x \<Longrightarrow> B2 x) \<Longrightarrow> C" -- {* nested rule *}
785 txt {* The compound rule premise @{prop "\<And>x. B1 x \<Longrightarrow> B2 x"} is better
786 addressed via @{command fix}~/ @{command assume}~/ @{command show}
787 in the nested proof body. *}
791 subsection {* Example: predicate logic *}
794 Using the above principles, standard introduction and elimination proofs
795 of predicate logic connectives of HOL work as follows.
800 have "A \<longrightarrow> B" and A sorry
804 then have "A \<or> B" ..
807 then have "A \<or> B" ..
809 have "A \<or> B" sorry
820 then have "A \<and> B" ..
822 have "A \<and> B" sorry
825 have "A \<and> B" sorry
836 then show False sorry
839 have "\<not> A" and A sorry
842 have "\<forall>x. P x"
848 have "\<forall>x. P x" sorry
851 have "\<exists>x. P x"
856 have "\<exists>x. P x" sorry
864 txt {* Less awkward version using @{command obtain}: *}
865 have "\<exists>x. P x" sorry
866 then obtain a where "P a" ..
869 text {* Further variations to illustrate Isar sub-proofs involving
875 proof -- {* two strictly isolated subproofs *}
882 proof -- {* one simultaneous sub-proof *}
887 proof -- {* two subproofs in the same context *}
893 proof -- {* swapped order *}
899 proof -- {* sequential subproofs *}
901 show B using `A` sorry
906 subsubsection {* Example: set-theoretic operators *}
908 text {* There is nothing special about logical connectives (@{text
909 "\<and>"}, @{text "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"} etc.). Operators from
910 set-theory or lattice-theory work analogously. It is only a matter
911 of rule declarations in the library; rules can be also specified
917 have "x \<in> A" and "x \<in> B" sorry
918 then have "x \<in> A \<inter> B" ..
920 have "x \<in> A" sorry
921 then have "x \<in> A \<union> B" ..
923 have "x \<in> B" sorry
924 then have "x \<in> A \<union> B" ..
926 have "x \<in> A \<union> B" sorry
937 have "x \<in> \<Inter>A"
941 show "x \<in> a" sorry
944 have "x \<in> \<Inter>A" sorry
945 then have "x \<in> a"
947 show "a \<in> A" sorry
950 have "a \<in> A" and "x \<in> a" sorry
951 then have "x \<in> \<Union>A" ..
953 have "x \<in> \<Union>A" sorry
954 then obtain a where "a \<in> A" and "x \<in> a" ..
958 section {* Generalized elimination and cases *}
960 subsection {* General elimination rules *}
963 The general format of elimination rules is illustrated by the
964 following typical representatives:
967 thm exE -- {* local parameter *}
968 thm conjE -- {* local premises *}
969 thm disjE -- {* split into cases *}
972 Combining these characteristics leads to the following general scheme
973 for elimination rules with cases:
977 \item prefix of assumptions (or ``major premises'')
979 \item one or more cases that enable to establish the main conclusion
980 in an augmented context
988 "A1 \<Longrightarrow> A2 \<Longrightarrow> (* assumptions *)
989 (\<And>x y. B1 x y \<Longrightarrow> C1 x y \<Longrightarrow> R) \<Longrightarrow> (* case 1 *)
990 (\<And>x y. B2 x y \<Longrightarrow> C2 x y \<Longrightarrow> R) \<Longrightarrow> (* case 2 *)
991 R (* main conclusion *)"
997 assume "B1 x y" and "C1 x y"
1001 assume "B2 x y" and "C2 x y"
1006 text {* Here @{text "?thesis"} is used to refer to the unchanged goal
1010 subsection {* Rules with cases *}
1013 Applying an elimination rule to some goal, leaves that unchanged
1014 but allows to augment the context in the sub-proof of each case.
1016 Isar provides some infrastructure to support this:
1020 \item native language elements to state eliminations
1022 \item symbolic case names
1024 \item method @{method cases} to recover this structure in a
1031 print_statement conjE
1032 print_statement disjE
1035 assumes A1 and A2 -- {* assumptions *}
1037 (case1) x y where "B1 x y" and "C1 x y"
1038 | (case2) x y where "B2 x y" and "C2 x y"
1042 subsubsection {* Example *}
1044 lemma tertium_non_datur:
1054 proof (cases "x = y" rule: tertium_non_datur)
1056 from `x = y` show ?thesis sorry
1059 from `x \<noteq> y` show ?thesis sorry
1064 subsubsection {* Example *}
1067 Isabelle/HOL specification mechanisms (datatype, inductive, etc.)
1068 provide suitable derived cases rules.
1071 datatype foo = Foo | Bar foo
1079 from `x = Foo` show ?thesis sorry
1082 from `x = Bar a` show ?thesis sorry
1087 subsection {* Obtaining local contexts *}
1089 text {* A single ``case'' branch may be inlined into Isar proof text
1090 via @{command obtain}. This proves @{prop "(\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow>
1091 thesis"} on the spot, and augments the context afterwards. *}
1095 fix B :: "'a \<Rightarrow> bool"
1097 obtain x where "B x" sorry
1100 txt {* Conclusions from this context may not mention @{term x} again! *}
1102 obtain x where "B x" sorry
1103 from `B x` have C sorry