--- a/doc-src/IsarRef/Thy/Synopsis.thy Wed Jun 01 12:39:04 2011 +0200
+++ b/doc-src/IsarRef/Thy/Synopsis.thy Wed Jun 01 13:06:45 2011 +0200
@@ -332,7 +332,7 @@
notepad
begin
- txt {* A vacous proof: *}
+ txt {* A vacuous proof: *}
have A sorry
moreover
have B sorry
@@ -350,7 +350,7 @@
ultimately
have "A \<and> B \<and> C" by blast
next
- txt {* More ambitous bigstep reasoning involving structured results: *}
+ txt {* More ambitious bigstep reasoning involving structured results: *}
have "A \<or> B \<or> C" sorry
moreover
{ assume A have R sorry }
@@ -362,4 +362,398 @@
have R by blast -- {* ``big-bang integration'' of proof blocks (occasionally fragile) *}
end
+
+section {* Structured Natural Deduction *}
+
+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 for 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
+
end
\ No newline at end of file