--- a/doc-src/IsarRef/Thy/First_Order_Logic.thy Thu Feb 12 11:19:54 2009 +0100
+++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy Thu Feb 12 11:36:15 2009 +0100
@@ -6,11 +6,11 @@
begin
text {*
- In order to commence a new object-logic within Isabelle/Pure we
- introduce abstract syntactic categories @{text "i"} for individuals
- and @{text "o"} for object-propositions. The latter is embedded
- into the language of Pure propositions by means of a separate
- judgment.
+ \noindent In order to commence a new object-logic within
+ Isabelle/Pure we introduce abstract syntactic categories @{text "i"}
+ for individuals and @{text "o"} for object-propositions. The latter
+ is embedded into the language of Pure propositions by means of a
+ separate judgment.
*}
typedecl i
@@ -124,9 +124,9 @@
qed
text {*
- Reasoning from basic axioms is often tedious. Our proofs work by
- producing various instances of the given rules (potentially the
- symmetric form) using the pattern ``@{command have}~@{text
+ \noindent Reasoning from basic axioms is often tedious. Our proofs
+ work by producing various instances of the given rules (potentially
+ the symmetric form) using the pattern ``@{command have}~@{text
eq}~@{command "by"}~@{text "(rule r)"}'' and composing the chain of
results via @{command also}/@{command finally}. These steps may
involve any of the transitivity rules declared in
@@ -160,7 +160,7 @@
definitions in order to normalize each equational problem. A more
realistic object-logic would include proper setup for the Simplifier
(\secref{sec:simplifier}), the main automated tool for equational
- reasoning in Isabelle. Then ``@{command unfolding}~@{text
+ reasoning in Isabelle. Then ``@{command unfolding}~@{thm
left_inv}~@{command ".."}'' would become ``@{command "by"}~@{text
"(simp add: left_inv)"}'' etc.
*}
@@ -173,7 +173,7 @@
text {*
We axiomatize basic connectives of propositional logic: implication,
disjunction, and conjunction. The associated rules are modeled
- after Gentzen's natural deduction \cite{Gentzen:1935}.
+ after Gentzen's system of Natural Deduction \cite{Gentzen:1935}.
*}
axiomatization
@@ -226,9 +226,9 @@
(*>*)
text {*
- Note that the analogous elimination for disjunction ``@{text
- "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with the
- original axiomatization of @{text "disjE"}.
+ \noindent Note that the analogous elimination rule for disjunction
+ ``@{text "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with
+ the original axiomatization of @{thm disjE}.
\medskip We continue propositional logic by introducing absurdity
with its characteristic elimination. Plain truth may then be
@@ -247,7 +247,8 @@
unfolding true_def ..
text {*
- \medskip Now negation represents an implication towards absurdity:
+ \medskip\noindent Now negation represents an implication towards
+ absurdity:
*}
definition
@@ -314,9 +315,9 @@
propositional proofs in general. All three rules characterize
classical logic independently, but the original rule is already the
most convenient to use, because it leaves the conclusion unchanged.
- Note that @{text "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"} fits again into our format for
+ Note that @{prop "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"} fits again into our format for
eliminations, despite the additional twist that the context refers
- to the main conclusion. So we may write @{text "classical"} as the
+ to the main conclusion. So we may write @{thm classical} as the
Isar statement ``@{text "\<OBTAINS> \<not> thesis"}''. This also
explains nicely how classical reasoning really works: whatever the
main @{text thesis} might be, we may always assume its negation!
@@ -332,8 +333,8 @@
of the underlying framework. According to the well-known technique
introduced by Church \cite{church40}, quantifiers are operators on
predicates, which are syntactically represented as @{text "\<lambda>"}-terms
- of type @{text "i \<Rightarrow> o"}. Specific binder notation relates @{text
- "All (\<lambda>x. B x)"} to @{text "\<forall>x. B x"} etc.
+ of type @{typ "i \<Rightarrow> o"}. Binder notation turns @{text "All (\<lambda>x. B
+ x)"} into @{text "\<forall>x. B x"} etc.
*}
axiomatization