author wenzelm Thu, 12 Feb 2009 11:36:15 +0100 changeset 29732 0a643dd9e0f5 parent 29731 efcbbd7baa02 child 29733 f38ccabb2edc
tuned;
--- 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
*}
@@ -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
--- a/doc-src/IsarRef/Thy/Framework.thy	Thu Feb 12 11:19:54 2009 +0100
+++ b/doc-src/IsarRef/Thy/Framework.thy	Thu Feb 12 11:36:15 2009 +0100
@@ -886,10 +886,10 @@
The present Isar infrastructure is sufficiently flexible to support
calculational reasoning (chains of transitivity steps) as derived
concept.  The generic proof elements introduced below depend on
-  rules declared as @{text "[trans]"} in the context.  It is left to
+  rules declared as @{attribute trans} in the context.  It is left to
the object-logic to provide a suitable rule collection for mixed
-  @{text "="}, @{text "<"}, @{text "\<le>"}, @{text "\<subset>"}, @{text "\<subseteq>"} etc.
-  Due to the flexibility of rule composition
+  relations of @{text "="}, @{text "<"}, @{text "\<le>"}, @{text "\<subset>"},
+  @{text "\<subseteq>"} etc.  Due to the flexibility of rule composition
(\secref{sec:framework-resolution}), substitution of equals by
equals is covered as well, even substitution of inequalities
@@ -902,10 +902,10 @@
selected from the context.  The course of reasoning is organized by
maintaining a secondary fact called @{fact calculation}'', apart
from the primary @{fact this}'' already provided by the Isar
-  primitives.  In the definitions below, @{attribute OF} is
+  primitives.  In the definitions below, @{attribute OF} refers to
@{inference resolution} (\secref{sec:framework-resolution}) with
-  multiple rule arguments, and @{text "trans"} refers to a suitable
-  rule from the context:
+  multiple rule arguments, and @{text "trans"} represents to a
+  suitable rule from the context:

\begin{matharray}{rcl}
@{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\