author wenzelm Mon, 12 Oct 2015 21:42:14 +0200 changeset 61420 ee42cba50933 parent 61419 3c3f8b182e4b child 61421 e0825405d398
redundant due to \parindent 0pt;
 src/Doc/Isar_Ref/First_Order_Logic.thy file | annotate | diff | comparison | revisions src/Doc/Isar_Ref/Framework.thy file | annotate | diff | comparison | revisions src/Doc/Isar_Ref/HOL_Specific.thy file | annotate | diff | comparison | revisions src/Doc/Isar_Ref/Spec.thy file | annotate | diff | comparison | revisions
--- a/src/Doc/Isar_Ref/First_Order_Logic.thy	Mon Oct 12 21:15:10 2015 +0200
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy	Mon Oct 12 21:42:14 2015 +0200
@@ -6,7 +6,7 @@
begin

text \<open>
-  \noindent In order to commence a new object-logic within
+  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
@@ -20,7 +20,7 @@
Trueprop :: "o \<Rightarrow> prop"    ("_" 5)

text \<open>
-  \noindent Note that the object-logic judgment is implicit in the
+  Note that the object-logic judgment is implicit in the
syntax: writing @{prop A} produces @{term "Trueprop A"} internally.
From the Pure perspective this means @{prop A} is derivable in the
object-logic''.
@@ -45,7 +45,7 @@
subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y"

text \<open>
-  \noindent Substitution is very powerful, but also hard to control in
+  Substitution is very powerful, but also hard to control in
full generality.  We derive some common symmetry~/ transitivity
schemes of @{term equal} as particular consequences.
\<close>
@@ -124,7 +124,7 @@
qed

text \<open>
-  \noindent Reasoning from basic axioms is often tedious.  Our proofs
+  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
@@ -157,7 +157,7 @@
(*>*)

text \<open>
-  \noindent Here we have re-used the built-in mechanism for unfolding
+  Here we have re-used the built-in mechanism for unfolding
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
@@ -195,7 +195,7 @@
conjD\<^sub>2: "A \<and> B \<Longrightarrow> B"

text \<open>
-  \noindent The conjunctive destructions have the disadvantage that
+  The conjunctive destructions have the disadvantage that
decomposing @{prop "A \<and> B"} involves an immediate decision which
component should be projected.  The more convenient simultaneous
elimination @{prop "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"} can be derived as
@@ -211,7 +211,7 @@
qed

text \<open>
-  \noindent Here is an example of swapping conjuncts with a single
+  Here is an example of swapping conjuncts with a single
intermediate elimination step:
\<close>

@@ -227,7 +227,7 @@
(*>*)

text \<open>
-  \noindent Note that the analogous elimination rule for disjunction
+  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}.

@@ -248,7 +248,7 @@
unfolding true_def ..

text \<open>
-  \medskip\noindent Now negation represents an implication towards
+  \medskip Now negation represents an implication towards
absurdity:
\<close>

@@ -312,7 +312,7 @@
qed

text \<open>
-  \noindent These examples illustrate both classical reasoning and
+  These examples illustrate both classical reasoning and
non-trivial 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
@@ -350,7 +350,7 @@
exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C"

text \<open>
-  \noindent The statement of @{thm exE} corresponds to @{text
+  The statement of @{thm exE} corresponds to @{text
"\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x"}'' in Isar.  In the
subsequent example we illustrate quantifier reasoning involving all
four rules:
@@ -400,7 +400,7 @@
\end{tabular}
\medskip

-  \noindent This essentially provides a declarative reading of Pure
+  This essentially provides a declarative reading of Pure
rules as Isar reasoning patterns: the rule statements tells how a
canonical proof outline shall look like.  Since the above rules have
already been declared as @{attribute (Pure) intro}, @{attribute
@@ -511,7 +511,7 @@
(*>*)

text \<open>
-  \bigskip\noindent Of course, these proofs are merely examples.  As
+  \bigskip Of course, these proofs are merely examples.  As
sketched in \secref{sec:framework-subproof}, there is a fair amount
of flexibility in expressing Pure deductions in Isar.  Here the user
is asked to express himself adequately, aiming at proof texts of
--- a/src/Doc/Isar_Ref/Framework.thy	Mon Oct 12 21:15:10 2015 +0200
+++ b/src/Doc/Isar_Ref/Framework.thy	Mon Oct 12 21:42:14 2015 +0200
@@ -97,7 +97,7 @@
text_raw \<open>\end{minipage}\<close>

text \<open>
-  \medskip\noindent Note that @{command assume} augments the proof
+  \medskip Note that @{command assume} augments the proof
context, @{command then} indicates that the current fact shall be
used in the next step, and @{command have} states an intermediate
goal.  The two dots @{command ".."}'' refer to a complete proof of
@@ -117,7 +117,7 @@
(*>*)

text \<open>
-  \noindent The format of the @{text "\<inter>"}-introduction rule represents
+  The format of the @{text "\<inter>"}-introduction rule represents
the most basic inference, which proceeds from given premises to a
conclusion, without any nested proof context involved.

@@ -152,7 +152,7 @@
text_raw \<open>\end{minipage}\<close>

text \<open>
-  \medskip\noindent This Isar reasoning pattern again refers to the
+  \medskip This Isar reasoning pattern again refers to the
primitive rule depicted above.  The system determines it in the
@{command proof}'' step, which could have been spelled out more
explicitly as @{command proof}~@{text "(rule InterI)"}''.  Note
@@ -201,7 +201,7 @@
text_raw \<open>\end{minipage}\<close>

text \<open>
-  \medskip\noindent Although the Isar proof follows the natural
+  \medskip Although the Isar proof follows the natural
deduction rule closely, the text reads not as natural as
anticipated.  There is a double occurrence of an arbitrary
conclusion @{prop "C"}, which represents the final result, but is
@@ -222,7 +222,7 @@
(*>*)

text \<open>
-  \noindent Here we avoid to mention the final conclusion @{prop "C"}
+  Here we avoid to mention the final conclusion @{prop "C"}
and return to plain forward reasoning.  The rule involved in the
@{command ".."}'' proof is the same as before.
\<close>
@@ -244,7 +244,7 @@
\end{tabular}
\medskip

-  \noindent Here only the types of syntactic terms, and the
+  Here only the types of syntactic terms, and the
propositions of proof terms have been shown.  The @{text
"\<lambda>"}-structure of proofs can be recorded as an optional feature of
the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"}, but
@@ -340,7 +340,7 @@
@{text "IntI:"}~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"}
\]

-  \noindent This is a plain Horn clause, since no further nesting on
+  This is a plain Horn clause, since no further nesting on
the left is involved.  The general @{text "\<Inter>"}-introduction
corresponds to a Hereditary Harrop Formula with one additional level
of nesting:
@@ -363,7 +363,7 @@
\end{array}
\]

-  \noindent Goal states are refined in intermediate proof steps until
+  Goal states are refined in intermediate proof steps until
a finished form is achieved.  Here the two main reasoning principles
are @{inference resolution}, for back-chaining a rule against a
sub-goal (replacing it by zero or more sub-goals), and @{inference
@@ -436,7 +436,7 @@
\end{tabular}}
\]

-  \noindent Here the @{text "sub\<hyphen>proof"} rule stems from the
+  Here the @{text "sub\<hyphen>proof"} rule stems from the
main @{command fix}-@{command assume}-@{command show} outline of
Isar (cf.\ \secref{sec:framework-subproof}): each assumption
indicated in the text results in a marked premise @{text "G"} above.
@@ -634,7 +634,7 @@
\end{tabular}}
\]

-  \noindent Here the name @{text thesis}'' is a specific convention
+  Here the name @{text thesis}'' is a specific convention
for an arbitrary-but-fixed proposition; in the primitive natural
deduction rules shown before we have occasionally used @{text C}.
The whole statement of @{command obtain}~@{text x}~@{keyword
@@ -684,7 +684,7 @@
(*>*)

text \<open>
-  \bigskip\noindent This illustrates the meaning of Isar context
+  \bigskip This illustrates the meaning of Isar context
elements without goals getting in between.
\<close>

@@ -707,7 +707,7 @@
& & \quad @{text "\<BBAR> \<dots>"} \\
\end{tabular}

-  \medskip\noindent A simple @{text "statement"} consists of named
+  \medskip A simple @{text "statement"} consists of named
propositions.  The full form admits local context elements followed
by the actual conclusions, such as @{keyword "fixes"}~@{text
x}~@{keyword "assumes"}~@{text "A x"}~@{keyword "shows"}~@{text "B
@@ -761,7 +761,7 @@
text_raw \<open>\end{minipage}\<close>

text \<open>
-  \medskip\noindent Here local facts \isacharbackquoteopen@{text "A
+  \medskip Here local facts \isacharbackquoteopen@{text "A
x"}\isacharbackquoteclose\ and \isacharbackquoteopen@{text "B
y"}\isacharbackquoteclose\ are referenced immediately; there is no
need to decompose the logical rule structure again.  In the second
@@ -863,7 +863,7 @@
text_raw \<open>\endgroup\<close>

text \<open>
-  \noindent Here the @{inference refinement} inference from
+  Here the @{inference refinement} inference from
\secref{sec:framework-resolution} mediates composition of Isar
sub-proofs nicely.  Observe that this principle incorporates some
degree of freedom in proof composition.  In particular, the proof
@@ -927,7 +927,7 @@
text_raw \<open>\end{minipage}\<close>

text \<open>
-  \medskip\noindent Such peephole optimizations'' of Isar texts are
+  \medskip Such peephole optimizations'' of Isar texts are
practically important to improve readability, by rearranging
contexts elements according to the natural flow of reasoning in the
body, while still observing the overall scoping rules.
@@ -974,7 +974,7 @@
@{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\
\end{matharray}

-  \noindent The start of a calculation is determined implicitly in the
+  The start of a calculation is determined implicitly in the
text: here @{command also} sets @{fact calculation} to the current
result; any subsequent occurrence will update @{fact calculation} by
combination with the next result and a transitivity rule.  The
@@ -998,7 +998,7 @@
(*>*)

text \<open>
-  \noindent The term @{text "\<dots>"}'' above is a special abbreviation
+  The term @{text "\<dots>"}'' above is a special abbreviation
provided by the Isabelle/Isar syntax layer: it statically refers to
the right-hand side argument of the previous statement given in the
text.  Thus it happens to coincide with relevant sub-expressions in
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Oct 12 21:15:10 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Oct 12 21:42:14 2015 +0200
@@ -876,7 +876,7 @@
\end{tabular}
\end{center}

-  \noindent The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text
+  The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text
"(| x = a |)"}.

A fixed record @{text "\<lparr>x = a, y = b\<rparr>"} has field @{text x} of value
@@ -1025,7 +1025,7 @@
\end{tabular}
\medskip

-  \noindent Some further operations address the extension aspect of a
+  Some further operations address the extension aspect of a
derived record scheme specifically: @{text "t.fields"} produces a record
fragment consisting of exactly the new fields introduced here (the result
may serve as a more part elsewhere); @{text "t.extend"} takes a fixed
@@ -1041,7 +1041,7 @@
\end{tabular}
\medskip

-  \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide for
+  Note that @{text "t.make"} and @{text "t.fields"} coincide for
root records.
\<close>

@@ -1281,7 +1281,7 @@
@{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>k \<Rightarrow> (\<^vec>\<alpha>\<^sub>n) t \<Rightarrow> (\<^vec>\<beta>\<^sub>n) t"} \\
\end{matharray}

-  \noindent where @{text t} is the type constructor, @{text "\<^vec>\<alpha>\<^sub>n"}
+  where @{text t} is the type constructor, @{text "\<^vec>\<alpha>\<^sub>n"}
and @{text "\<^vec>\<beta>\<^sub>n"} are distinct type variables free in the local
theory and @{text "\<sigma>\<^sub>1"}, \ldots, @{text "\<sigma>\<^sub>k"} is a subsequence of @{text
"\<alpha>\<^sub>1 \<Rightarrow> \<beta>\<^sub>1"}, @{text "\<beta>\<^sub>1 \<Rightarrow> \<alpha>\<^sub>1"}, \ldots, @{text "\<alpha>\<^sub>n \<Rightarrow> \<beta>\<^sub>n"}, @{text
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Oct 12 21:15:10 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Oct 12 21:42:14 2015 +0200
@@ -1097,7 +1097,7 @@
$@{text "t :: (\<^vec>s\<^sub>1)c\<^sub>1 \<Longrightarrow> t :: (\<^vec>s\<^sub>2)c\<^sub>2 \<Longrightarrow> c\<^sub>1 \<subseteq> c\<^sub>2 \<Longrightarrow> \<^vec>s\<^sub>1 \<subseteq> \<^vec>s\<^sub>2"}$
-  \noindent for all such arities.  In other words, whenever the result
+  for all such arities.  In other words, whenever the result
classes of some type-constructor arities are related, then the
argument sorts need to be related in the same way.