--- a/doc-src/IsarRef/Thy/Synopsis.thy Tue Aug 28 12:31:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1108 +0,0 @@
-theory Synopsis
-imports Base Main
-begin
-
-chapter {* Synopsis *}
-
-section {* Notepad *}
-
-text {*
- An Isar proof body serves as mathematical notepad to compose logical
- content, consisting of types, terms, facts.
-*}
-
-
-subsection {* Types and terms *}
-
-notepad
-begin
- txt {* Locally fixed entities: *}
- fix x -- {* local constant, without any type information yet *}
- fix x :: 'a -- {* variant with explicit type-constraint for subsequent use*}
-
- fix a b
- assume "a = b" -- {* type assignment at first occurrence in concrete term *}
-
- txt {* Definitions (non-polymorphic): *}
- def x \<equiv> "t::'a"
-
- txt {* Abbreviations (polymorphic): *}
- let ?f = "\<lambda>x. x"
- term "?f ?f"
-
- txt {* Notation: *}
- write x ("***")
-end
-
-
-subsection {* Facts *}
-
-text {*
- A fact is a simultaneous list of theorems.
-*}
-
-
-subsubsection {* Producing facts *}
-
-notepad
-begin
-
- txt {* Via assumption (``lambda''): *}
- assume a: A
-
- txt {* Via proof (``let''): *}
- have b: B sorry
-
- txt {* Via abbreviation (``let''): *}
- note c = a b
-
-end
-
-
-subsubsection {* Referencing facts *}
-
-notepad
-begin
- txt {* Via explicit name: *}
- assume a: A
- note a
-
- txt {* Via implicit name: *}
- assume A
- note this
-
- txt {* Via literal proposition (unification with results from the proof text): *}
- assume A
- note `A`
-
- assume "\<And>x. B x"
- note `B a`
- note `B b`
-end
-
-
-subsubsection {* Manipulating facts *}
-
-notepad
-begin
- txt {* Instantiation: *}
- assume a: "\<And>x. B x"
- note a
- note a [of b]
- note a [where x = b]
-
- txt {* Backchaining: *}
- assume 1: A
- assume 2: "A \<Longrightarrow> C"
- note 2 [OF 1]
- note 1 [THEN 2]
-
- txt {* Symmetric results: *}
- assume "x = y"
- note this [symmetric]
-
- assume "x \<noteq> y"
- note this [symmetric]
-
- txt {* Adhoc-simplification (take care!): *}
- assume "P ([] @ xs)"
- note this [simplified]
-end
-
-
-subsubsection {* Projections *}
-
-text {*
- Isar facts consist of multiple theorems. There is notation to project
- interval ranges.
-*}
-
-notepad
-begin
- assume stuff: A B C D
- note stuff(1)
- note stuff(2-3)
- note stuff(2-)
-end
-
-
-subsubsection {* Naming conventions *}
-
-text {*
- \begin{itemize}
-
- \item Lower-case identifiers are usually preferred.
-
- \item Facts can be named after the main term within the proposition.
-
- \item Facts should \emph{not} be named after the command that
- introduced them (@{command "assume"}, @{command "have"}). This is
- misleading and hard to maintain.
-
- \item Natural numbers can be used as ``meaningless'' names (more
- appropriate than @{text "a1"}, @{text "a2"} etc.)
-
- \item Symbolic identifiers are supported (e.g. @{text "*"}, @{text
- "**"}, @{text "***"}).
-
- \end{itemize}
-*}
-
-
-subsection {* Block structure *}
-
-text {*
- The formal notepad is block structured. The fact produced by the last
- entry of a block is exported into the outer context.
-*}
-
-notepad
-begin
- {
- have a: A sorry
- have b: B sorry
- note a b
- }
- note this
- note `A`
- note `B`
-end
-
-text {* Explicit blocks as well as implicit blocks of nested goal
- statements (e.g.\ @{command have}) automatically introduce one extra
- pair of parentheses in reserve. The @{command next} command allows
- to ``jump'' between these sub-blocks. *}
-
-notepad
-begin
-
- {
- have a: A sorry
- next
- have b: B
- proof -
- show B sorry
- next
- have c: C sorry
- next
- have d: D sorry
- qed
- }
-
- txt {* Alternative version with explicit parentheses everywhere: *}
-
- {
- {
- have a: A sorry
- }
- {
- have b: B
- proof -
- {
- show B sorry
- }
- {
- have c: C sorry
- }
- {
- have d: D sorry
- }
- qed
- }
- }
-
-end
-
-
-section {* Calculational reasoning \label{sec:calculations-synopsis} *}
-
-text {*
- For example, see @{file "~~/src/HOL/Isar_Examples/Group.thy"}.
-*}
-
-
-subsection {* Special names in Isar proofs *}
-
-text {*
- \begin{itemize}
-
- \item term @{text "?thesis"} --- the main conclusion of the
- innermost pending claim
-
- \item term @{text "\<dots>"} --- the argument of the last explicitly
- stated result (for infix application this is the right-hand side)
-
- \item fact @{text "this"} --- the last result produced in the text
-
- \end{itemize}
-*}
-
-notepad
-begin
- have "x = y"
- proof -
- term ?thesis
- show ?thesis sorry
- term ?thesis -- {* static! *}
- qed
- term "\<dots>"
- thm this
-end
-
-text {* Calculational reasoning maintains the special fact called
- ``@{text calculation}'' in the background. Certain language
- elements combine primary @{text this} with secondary @{text
- calculation}. *}
-
-
-subsection {* Transitive chains *}
-
-text {* The Idea is to combine @{text this} and @{text calculation}
- via typical @{text trans} rules (see also @{command
- print_trans_rules}): *}
-
-thm trans
-thm less_trans
-thm less_le_trans
-
-notepad
-begin
- txt {* Plain bottom-up calculation: *}
- have "a = b" sorry
- also
- have "b = c" sorry
- also
- have "c = d" sorry
- finally
- have "a = d" .
-
- txt {* Variant using the @{text "\<dots>"} abbreviation: *}
- have "a = b" sorry
- also
- have "\<dots> = c" sorry
- also
- have "\<dots> = d" sorry
- finally
- have "a = d" .
-
- txt {* Top-down version with explicit claim at the head: *}
- have "a = d"
- proof -
- have "a = b" sorry
- also
- have "\<dots> = c" sorry
- also
- have "\<dots> = d" sorry
- finally
- show ?thesis .
- qed
-next
- txt {* Mixed inequalities (require suitable base type): *}
- fix a b c d :: nat
-
- have "a < b" sorry
- also
- have "b \<le> c" sorry
- also
- have "c = d" sorry
- finally
- have "a < d" .
-end
-
-
-subsubsection {* Notes *}
-
-text {*
- \begin{itemize}
-
- \item The notion of @{text trans} rule is very general due to the
- flexibility of Isabelle/Pure rule composition.
-
- \item User applications may declare their own rules, with some care
- about the operational details of higher-order unification.
-
- \end{itemize}
-*}
-
-
-subsection {* Degenerate calculations and bigstep reasoning *}
-
-text {* The Idea is to append @{text this} to @{text calculation},
- without rule composition. *}
-
-notepad
-begin
- txt {* A vacuous proof: *}
- have A sorry
- moreover
- have B sorry
- moreover
- have C sorry
- ultimately
- have A and B and C .
-next
- txt {* Slightly more content (trivial bigstep reasoning): *}
- have A sorry
- moreover
- have B sorry
- moreover
- have C sorry
- ultimately
- have "A \<and> B \<and> C" by blast
-next
- txt {* More ambitious bigstep reasoning involving structured results: *}
- have "A \<or> B \<or> C" sorry
- moreover
- { assume A have R sorry }
- moreover
- { assume B have R sorry }
- moreover
- { assume C have R sorry }
- ultimately
- have R by blast -- {* ``big-bang integration'' of proof blocks (occasionally fragile) *}
-end
-
-
-section {* Induction *}
-
-subsection {* Induction as Natural Deduction *}
-
-text {* In principle, induction is just a special case of Natural
- Deduction (see also \secref{sec:natural-deduction-synopsis}). For
- example: *}
-
-thm nat.induct
-print_statement nat.induct
-
-notepad
-begin
- fix n :: nat
- have "P n"
- proof (rule nat.induct) -- {* fragile rule application! *}
- show "P 0" sorry
- next
- fix n :: nat
- assume "P n"
- show "P (Suc n)" sorry
- qed
-end
-
-text {*
- In practice, much more proof infrastructure is required.
-
- The proof method @{method induct} provides:
- \begin{itemize}
-
- \item implicit rule selection and robust instantiation
-
- \item context elements via symbolic case names
-
- \item support for rule-structured induction statements, with local
- parameters, premises, etc.
-
- \end{itemize}
-*}
-
-notepad
-begin
- fix n :: nat
- have "P n"
- proof (induct n)
- case 0
- show ?case sorry
- next
- case (Suc n)
- from Suc.hyps show ?case sorry
- qed
-end
-
-
-subsubsection {* Example *}
-
-text {*
- The subsequent example combines the following proof patterns:
- \begin{itemize}
-
- \item outermost induction (over the datatype structure of natural
- numbers), to decompose the proof problem in top-down manner
-
- \item calculational reasoning (\secref{sec:calculations-synopsis})
- to compose the result in each case
-
- \item solving local claims within the calculation by simplification
-
- \end{itemize}
-*}
-
-lemma
- fixes n :: nat
- shows "(\<Sum>i=0..n. i) = n * (n + 1) div 2"
-proof (induct n)
- case 0
- have "(\<Sum>i=0..0. i) = (0::nat)" by simp
- also have "\<dots> = 0 * (0 + 1) div 2" by simp
- finally show ?case .
-next
- case (Suc n)
- have "(\<Sum>i=0..Suc n. i) = (\<Sum>i=0..n. i) + (n + 1)" by simp
- also have "\<dots> = n * (n + 1) div 2 + (n + 1)" by (simp add: Suc.hyps)
- also have "\<dots> = (n * (n + 1) + 2 * (n + 1)) div 2" by simp
- also have "\<dots> = (Suc n * (Suc n + 1)) div 2" by simp
- finally show ?case .
-qed
-
-text {* This demonstrates how induction proofs can be done without
- having to consider the raw Natural Deduction structure. *}
-
-
-subsection {* Induction with local parameters and premises *}
-
-text {* Idea: Pure rule statements are passed through the induction
- rule. This achieves convenient proof patterns, thanks to some
- internal trickery in the @{method induct} method.
-
- Important: Using compact HOL formulae with @{text "\<forall>/\<longrightarrow>"} is a
- well-known anti-pattern! It would produce useless formal noise.
-*}
-
-notepad
-begin
- fix n :: nat
- fix P :: "nat \<Rightarrow> bool"
- fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool"
-
- have "P n"
- proof (induct n)
- case 0
- show "P 0" sorry
- next
- case (Suc n)
- from `P n` show "P (Suc n)" sorry
- qed
-
- have "A n \<Longrightarrow> P n"
- proof (induct n)
- case 0
- from `A 0` show "P 0" sorry
- next
- case (Suc n)
- from `A n \<Longrightarrow> P n`
- and `A (Suc n)` show "P (Suc n)" sorry
- qed
-
- have "\<And>x. Q x n"
- proof (induct n)
- case 0
- show "Q x 0" sorry
- next
- case (Suc n)
- from `\<And>x. Q x n` show "Q x (Suc n)" sorry
- txt {* Local quantification admits arbitrary instances: *}
- note `Q a n` and `Q b n`
- qed
-end
-
-
-subsection {* Implicit induction context *}
-
-text {* The @{method induct} method can isolate local parameters and
- premises directly from the given statement. This is convenient in
- practical applications, but requires some understanding of what is
- going on internally (as explained above). *}
-
-notepad
-begin
- fix n :: nat
- fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool"
-
- fix x :: 'a
- assume "A x n"
- then have "Q x n"
- proof (induct n arbitrary: x)
- case 0
- from `A x 0` show "Q x 0" sorry
- next
- case (Suc n)
- from `\<And>x. A x n \<Longrightarrow> Q x n` -- {* arbitrary instances can be produced here *}
- and `A x (Suc n)` show "Q x (Suc n)" sorry
- qed
-end
-
-
-subsection {* Advanced induction with term definitions *}
-
-text {* Induction over subexpressions of a certain shape are delicate
- to formalize. The Isar @{method induct} method provides
- infrastructure for this.
-
- Idea: sub-expressions of the problem are turned into a defined
- induction variable; often accompanied with fixing of auxiliary
- parameters in the original expression. *}
-
-notepad
-begin
- fix a :: "'a \<Rightarrow> nat"
- fix A :: "nat \<Rightarrow> bool"
-
- assume "A (a x)"
- then have "P (a x)"
- proof (induct "a x" arbitrary: x)
- case 0
- note prem = `A (a x)`
- and defn = `0 = a x`
- show "P (a x)" sorry
- next
- case (Suc n)
- note hyp = `\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)`
- and prem = `A (a x)`
- and defn = `Suc n = a x`
- show "P (a x)" sorry
- qed
-end
-
-
-section {* Natural Deduction \label{sec:natural-deduction-synopsis} *}
-
-subsection {* Rule statements *}
-
-text {*
- Isabelle/Pure ``theorems'' are always natural deduction rules,
- which sometimes happen to consist of a conclusion only.
-
- The framework connectives @{text "\<And>"} and @{text "\<Longrightarrow>"} indicate the
- rule structure declaratively. For example: *}
-
-thm conjI
-thm impI
-thm nat.induct
-
-text {*
- The object-logic is embedded into the Pure framework via an implicit
- derivability judgment @{term "Trueprop :: bool \<Rightarrow> prop"}.
-
- Thus any HOL formulae appears atomic to the Pure framework, while
- the rule structure outlines the corresponding proof pattern.
-
- This can be made explicit as follows:
-*}
-
-notepad
-begin
- write Trueprop ("Tr")
-
- thm conjI
- thm impI
- thm nat.induct
-end
-
-text {*
- Isar provides first-class notation for rule statements as follows.
-*}
-
-print_statement conjI
-print_statement impI
-print_statement nat.induct
-
-
-subsubsection {* Examples *}
-
-text {*
- Introductions and eliminations of some standard connectives of
- the object-logic can be written as rule statements as follows. (The
- proof ``@{command "by"}~@{method blast}'' serves as sanity check.)
-*}
-
-lemma "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P" by blast
-lemma "\<not> P \<Longrightarrow> P \<Longrightarrow> Q" by blast
-
-lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" by blast
-lemma "P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R" by blast
-
-lemma "P \<Longrightarrow> P \<or> Q" by blast
-lemma "Q \<Longrightarrow> P \<or> Q" by blast
-lemma "P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" by blast
-
-lemma "(\<And>x. P x) \<Longrightarrow> (\<forall>x. P x)" by blast
-lemma "(\<forall>x. P x) \<Longrightarrow> P x" by blast
-
-lemma "P x \<Longrightarrow> (\<exists>x. P x)" by blast
-lemma "(\<exists>x. P x) \<Longrightarrow> (\<And>x. P x \<Longrightarrow> R) \<Longrightarrow> R" by blast
-
-lemma "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B" by blast
-lemma "x \<in> A \<inter> B \<Longrightarrow> (x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast
-
-lemma "x \<in> A \<Longrightarrow> x \<in> A \<union> B" by blast
-lemma "x \<in> B \<Longrightarrow> x \<in> A \<union> B" by blast
-lemma "x \<in> A \<union> B \<Longrightarrow> (x \<in> A \<Longrightarrow> R) \<Longrightarrow> (x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast
-
-
-subsection {* Isar context elements *}
-
-text {* We derive some results out of the blue, using Isar context
- elements and some explicit blocks. This illustrates their meaning
- wrt.\ Pure connectives, without goal states getting in the way. *}
-
-notepad
-begin
- {
- fix x
- have "B x" sorry
- }
- have "\<And>x. B x" by fact
-
-next
-
- {
- assume A
- have B sorry
- }
- have "A \<Longrightarrow> B" by fact
-
-next
-
- {
- def x \<equiv> t
- have "B x" sorry
- }
- have "B t" by fact
-
-next
-
- {
- obtain x :: 'a where "B x" sorry
- have C sorry
- }
- have C by fact
-
-end
-
-
-subsection {* Pure rule composition *}
-
-text {*
- The Pure framework provides means for:
-
- \begin{itemize}
-
- \item backward-chaining of rules by @{inference resolution}
-
- \item closing of branches by @{inference assumption}
-
- \end{itemize}
-
- Both principles involve higher-order unification of @{text \<lambda>}-terms
- modulo @{text "\<alpha>\<beta>\<eta>"}-equivalence (cf.\ Huet and Miller). *}
-
-notepad
-begin
- assume a: A and b: B
- thm conjI
- thm conjI [of A B] -- "instantiation"
- thm conjI [of A B, OF a b] -- "instantiation and composition"
- thm conjI [OF a b] -- "composition via unification (trivial)"
- thm conjI [OF `A` `B`]
-
- thm conjI [OF disjI1]
-end
-
-text {* Note: Low-level rule composition is tedious and leads to
- unreadable~/ unmaintainable expressions in the text. *}
-
-
-subsection {* Structured backward reasoning *}
-
-text {* Idea: Canonical proof decomposition via @{command fix}~/
- @{command assume}~/ @{command show}, where the body produces a
- natural deduction rule to refine some goal. *}
-
-notepad
-begin
- fix A B :: "'a \<Rightarrow> bool"
-
- have "\<And>x. A x \<Longrightarrow> B x"
- proof -
- fix x
- assume "A x"
- show "B x" sorry
- qed
-
- have "\<And>x. A x \<Longrightarrow> B x"
- proof -
- {
- fix x
- assume "A x"
- show "B x" sorry
- } -- "implicit block structure made explicit"
- note `\<And>x. A x \<Longrightarrow> B x`
- -- "side exit for the resulting rule"
- qed
-end
-
-
-subsection {* Structured rule application *}
-
-text {*
- Idea: Previous facts and new claims are composed with a rule from
- the context (or background library).
-*}
-
-notepad
-begin
- assume r1: "A \<Longrightarrow> B \<Longrightarrow> C" -- {* simple rule (Horn clause) *}
-
- have A sorry -- "prefix of facts via outer sub-proof"
- then have C
- proof (rule r1)
- show B sorry -- "remaining rule premises via inner sub-proof"
- qed
-
- have C
- proof (rule r1)
- show A sorry
- show B sorry
- qed
-
- have A and B sorry
- then have C
- proof (rule r1)
- qed
-
- have A and B sorry
- then have C by (rule r1)
-
-next
-
- assume r2: "A \<Longrightarrow> (\<And>x. B1 x \<Longrightarrow> B2 x) \<Longrightarrow> C" -- {* nested rule *}
-
- have A sorry
- then have C
- proof (rule r2)
- fix x
- assume "B1 x"
- show "B2 x" sorry
- qed
-
- txt {* The compound rule premise @{prop "\<And>x. B1 x \<Longrightarrow> B2 x"} is better
- addressed via @{command fix}~/ @{command assume}~/ @{command show}
- in the nested proof body. *}
-end
-
-
-subsection {* Example: predicate logic *}
-
-text {*
- Using the above principles, standard introduction and elimination proofs
- of predicate logic connectives of HOL work as follows.
-*}
-
-notepad
-begin
- have "A \<longrightarrow> B" and A sorry
- then have B ..
-
- have A sorry
- then have "A \<or> B" ..
-
- have B sorry
- then have "A \<or> B" ..
-
- have "A \<or> B" sorry
- then have C
- proof
- assume A
- then show C sorry
- next
- assume B
- then show C sorry
- qed
-
- have A and B sorry
- then have "A \<and> B" ..
-
- have "A \<and> B" sorry
- then have A ..
-
- have "A \<and> B" sorry
- then have B ..
-
- have False sorry
- then have A ..
-
- have True ..
-
- have "\<not> A"
- proof
- assume A
- then show False sorry
- qed
-
- have "\<not> A" and A sorry
- then have B ..
-
- have "\<forall>x. P x"
- proof
- fix x
- show "P x" sorry
- qed
-
- have "\<forall>x. P x" sorry
- then have "P a" ..
-
- have "\<exists>x. P x"
- proof
- show "P a" sorry
- qed
-
- have "\<exists>x. P x" sorry
- then have C
- proof
- fix a
- assume "P a"
- show C sorry
- qed
-
- txt {* Less awkward version using @{command obtain}: *}
- have "\<exists>x. P x" sorry
- then obtain a where "P a" ..
-end
-
-text {* Further variations to illustrate Isar sub-proofs involving
- @{command show}: *}
-
-notepad
-begin
- have "A \<and> B"
- proof -- {* two strictly isolated subproofs *}
- show A sorry
- next
- show B sorry
- qed
-
- have "A \<and> B"
- proof -- {* one simultaneous sub-proof *}
- show A and B sorry
- qed
-
- have "A \<and> B"
- proof -- {* two subproofs in the same context *}
- show A sorry
- show B sorry
- qed
-
- have "A \<and> B"
- proof -- {* swapped order *}
- show B sorry
- show A sorry
- qed
-
- have "A \<and> B"
- proof -- {* sequential subproofs *}
- show A sorry
- show B using `A` sorry
- qed
-end
-
-
-subsubsection {* Example: set-theoretic operators *}
-
-text {* There is nothing special about logical connectives (@{text
- "\<and>"}, @{text "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"} etc.). Operators from
- set-theory or lattice-theory work analogously. It is only a matter
- of rule declarations in the library; rules can be also specified
- explicitly.
-*}
-
-notepad
-begin
- have "x \<in> A" and "x \<in> B" sorry
- then have "x \<in> A \<inter> B" ..
-
- have "x \<in> A" sorry
- then have "x \<in> A \<union> B" ..
-
- have "x \<in> B" sorry
- then have "x \<in> A \<union> B" ..
-
- have "x \<in> A \<union> B" sorry
- then have C
- proof
- assume "x \<in> A"
- then show C sorry
- next
- assume "x \<in> B"
- then show C sorry
- qed
-
-next
- have "x \<in> \<Inter>A"
- proof
- fix a
- assume "a \<in> A"
- show "x \<in> a" sorry
- qed
-
- have "x \<in> \<Inter>A" sorry
- then have "x \<in> a"
- proof
- show "a \<in> A" sorry
- qed
-
- have "a \<in> A" and "x \<in> a" sorry
- then have "x \<in> \<Union>A" ..
-
- have "x \<in> \<Union>A" sorry
- then obtain a where "a \<in> A" and "x \<in> a" ..
-end
-
-
-section {* Generalized elimination and cases *}
-
-subsection {* General elimination rules *}
-
-text {*
- The general format of elimination rules is illustrated by the
- following typical representatives:
-*}
-
-thm exE -- {* local parameter *}
-thm conjE -- {* local premises *}
-thm disjE -- {* split into cases *}
-
-text {*
- Combining these characteristics leads to the following general scheme
- for elimination rules with cases:
-
- \begin{itemize}
-
- \item prefix of assumptions (or ``major premises'')
-
- \item one or more cases that enable to establish the main conclusion
- in an augmented context
-
- \end{itemize}
-*}
-
-notepad
-begin
- assume r:
- "A1 \<Longrightarrow> A2 \<Longrightarrow> (* assumptions *)
- (\<And>x y. B1 x y \<Longrightarrow> C1 x y \<Longrightarrow> R) \<Longrightarrow> (* case 1 *)
- (\<And>x y. B2 x y \<Longrightarrow> C2 x y \<Longrightarrow> R) \<Longrightarrow> (* case 2 *)
- R (* main conclusion *)"
-
- have A1 and A2 sorry
- then have R
- proof (rule r)
- fix x y
- assume "B1 x y" and "C1 x y"
- show ?thesis sorry
- next
- fix x y
- assume "B2 x y" and "C2 x y"
- show ?thesis sorry
- qed
-end
-
-text {* Here @{text "?thesis"} is used to refer to the unchanged goal
- statement. *}
-
-
-subsection {* Rules with cases *}
-
-text {*
- Applying an elimination rule to some goal, leaves that unchanged
- but allows to augment the context in the sub-proof of each case.
-
- Isar provides some infrastructure to support this:
-
- \begin{itemize}
-
- \item native language elements to state eliminations
-
- \item symbolic case names
-
- \item method @{method cases} to recover this structure in a
- sub-proof
-
- \end{itemize}
-*}
-
-print_statement exE
-print_statement conjE
-print_statement disjE
-
-lemma
- assumes A1 and A2 -- {* assumptions *}
- obtains
- (case1) x y where "B1 x y" and "C1 x y"
- | (case2) x y where "B2 x y" and "C2 x y"
- sorry
-
-
-subsubsection {* Example *}
-
-lemma tertium_non_datur:
- obtains
- (T) A
- | (F) "\<not> A"
- by blast
-
-notepad
-begin
- fix x y :: 'a
- have C
- proof (cases "x = y" rule: tertium_non_datur)
- case T
- from `x = y` show ?thesis sorry
- next
- case F
- from `x \<noteq> y` show ?thesis sorry
- qed
-end
-
-
-subsubsection {* Example *}
-
-text {*
- Isabelle/HOL specification mechanisms (datatype, inductive, etc.)
- provide suitable derived cases rules.
-*}
-
-datatype foo = Foo | Bar foo
-
-notepad
-begin
- fix x :: foo
- have C
- proof (cases x)
- case Foo
- from `x = Foo` show ?thesis sorry
- next
- case (Bar a)
- from `x = Bar a` show ?thesis sorry
- qed
-end
-
-
-subsection {* Obtaining local contexts *}
-
-text {* A single ``case'' branch may be inlined into Isar proof text
- via @{command obtain}. This proves @{prop "(\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow>
- thesis"} on the spot, and augments the context afterwards. *}
-
-notepad
-begin
- fix B :: "'a \<Rightarrow> bool"
-
- obtain x where "B x" sorry
- note `B x`
-
- txt {* Conclusions from this context may not mention @{term x} again! *}
- {
- obtain x where "B x" sorry
- from `B x` have C sorry
- }
- note `C`
-end
-
-end