# HG changeset patch
# User wenzelm
# Date 1455111310 -3600
# Node ID f054c364b53fe5df3f3e296169b25c020bdd0d88
# Parent  c04e97be39d39efa207b0d9150d350efb848e5fa
misc tuning;

diff -r c04e97be39d3 -r f054c364b53f src/Doc/Isar_Ref/First_Order_Logic.thy
--- a/src/Doc/Isar_Ref/First_Order_Logic.thy	Wed Feb 10 14:14:43 2016 +0100
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy	Wed Feb 10 14:35:10 2016 +0100
@@ -7,24 +7,21 @@
 begin
 
 text \<open>
-  In order to commence a new object-logic within
-  Isabelle/Pure we introduce abstract syntactic categories \<open>i\<close>
-  for individuals and \<open>o\<close> for object-propositions.  The latter
-  is embedded into the language of Pure propositions by means of a
-  separate judgment.
+  In order to commence a new object-logic within Isabelle/Pure we introduce
+  abstract syntactic categories \<open>i\<close> for individuals and \<open>o\<close> for
+  object-propositions. The latter is embedded into the language of Pure
+  propositions by means of a separate judgment.
 \<close>
 
 typedecl i
 typedecl o
 
-judgment
-  Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
+judgment Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
 
 text \<open>
-  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''.
+  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''.
 \<close>
 
 
@@ -32,23 +29,20 @@
 
 text \<open>
   Equality is axiomatized as a binary predicate on individuals, with
-  reflexivity as introduction, and substitution as elimination
-  principle.  Note that the latter is particularly convenient in a
-  framework like Isabelle, because syntactic congruences are
-  implicitly produced by unification of @{term "B x"} against
-  expressions containing occurrences of @{term x}.
+  reflexivity as introduction, and substitution as elimination principle. Note
+  that the latter is particularly convenient in a framework like Isabelle,
+  because syntactic congruences are implicitly produced by unification of
+  \<open>B x\<close> against expressions containing occurrences of \<open>x\<close>.
 \<close>
 
-axiomatization
-  equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infix "=" 50)
-where
-  refl [intro]: "x = x" and
-  subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y"
+axiomatization equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infix "=" 50)
+  where refl [intro]: "x = x"
+    and subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y"
 
 text \<open>
-  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.
+  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>
 
 theorem sym [sym]:
@@ -87,10 +81,9 @@
 subsection \<open>Basic group theory\<close>
 
 text \<open>
-  As an example for equational reasoning we consider some bits of
-  group theory.  The subsequent locale definition postulates group
-  operations and axioms; we also derive some consequences of this
-  specification.
+  As an example for equational reasoning we consider some bits of group
+  theory. The subsequent locale definition postulates group operations and
+  axioms; we also derive some consequences of this specification.
 \<close>
 
 locale group =
@@ -125,20 +118,19 @@
 qed
 
 text \<open>
-  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}~\<open>eq\<close>~@{command "by"}~\<open>(rule r)\<close>'' and composing the chain of
-  results via @{command also}/@{command finally}.  These steps may
-  involve any of the transitivity rules declared in
-  \secref{sec:framework-ex-equal}, namely @{thm trans} in combining
-  the first two results in @{thm right_inv} and in the final steps of
-  both proofs, @{thm forw_subst} in the first combination of @{thm
+  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 ``\<^theory_text>\<open>have eq by (rule r)\<close>'' and composing the chain of results
+  via \<^theory_text>\<open>also\<close>/\<^theory_text>\<open>finally\<close>. These steps may involve any of the transitivity
+  rules declared in \secref{sec:framework-ex-equal}, namely @{thm trans} in
+  combining the first two results in @{thm right_inv} and in the final steps
+  of both proofs, @{thm forw_subst} in the first combination of @{thm
   right_unit}, and @{thm back_subst} in all other calculational steps.
 
-  Occasional substitutions in calculations are adequate, but should
-  not be over-emphasized.  The other extreme is to compose a chain by
-  plain transitivity only, with replacements occurring always in
-  topmost position. For example:
+  Occasional substitutions in calculations are adequate, but should not be
+  over-emphasized. The other extreme is to compose a chain by plain
+  transitivity only, with replacements occurring always in topmost position.
+  For example:
 \<close>
 
 (*<*)
@@ -157,12 +149,11 @@
 (*>*)
 
 text \<open>
-  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
-  reasoning in Isabelle.  Then ``@{command unfolding}~@{thm
-  left_inv}~@{command ".."}'' would become ``@{command "by"}~\<open>(simp only: left_inv)\<close>'' etc.
+  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 reasoning in Isabelle. Then ``\<^theory_text>\<open>unfolding
+  left_inv ..\<close>'' would become ``\<^theory_text>\<open>by (simp only: left_inv)\<close>'' etc.
 \<close>
 
 end
@@ -172,33 +163,29 @@
 
 text \<open>
   We axiomatize basic connectives of propositional logic: implication,
-  disjunction, and conjunction.  The associated rules are modeled
-  after Gentzen's system of Natural Deduction @{cite "Gentzen:1935"}.
+  disjunction, and conjunction. The associated rules are modeled after
+  Gentzen's system of Natural Deduction @{cite "Gentzen:1935"}.
 \<close>
 
-axiomatization
-  imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25) where
-  impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
-  impD [dest]: "(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B"
+axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
+  where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
+    and impD [dest]: "(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B"
 
-axiomatization
-  disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30) where
-  disjI\<^sub>1 [intro]: "A \<Longrightarrow> A \<or> B" and
-  disjI\<^sub>2 [intro]: "B \<Longrightarrow> A \<or> B" and
-  disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
+axiomatization disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
+  where disjI\<^sub>1 [intro]: "A \<Longrightarrow> A \<or> B"
+    and disjI\<^sub>2 [intro]: "B \<Longrightarrow> A \<or> B"
+    and disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
 
-axiomatization
-  conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35) where
-  conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and
-  conjD\<^sub>1: "A \<and> B \<Longrightarrow> A" and
-  conjD\<^sub>2: "A \<and> B \<Longrightarrow> B"
+axiomatization conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
+  where conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
+    and conjD\<^sub>1: "A \<and> B \<Longrightarrow> A"
+    and conjD\<^sub>2: "A \<and> B \<Longrightarrow> B"
 
 text \<open>
-  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
-  follows:
+  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 follows:
 \<close>
 
 theorem conjE [elim]:
@@ -210,13 +197,14 @@
 qed
 
 text \<open>
-  Here is an example of swapping conjuncts with a single
-  intermediate elimination step:
+  Here is an example of swapping conjuncts with a single intermediate
+  elimination step:
 \<close>
 
 (*<*)
 lemma "\<And>A. PROP A \<Longrightarrow> PROP A"
 proof -
+  fix A B
 (*>*)
   assume "A \<and> B"
   then obtain B and A ..
@@ -226,23 +214,21 @@
 (*>*)
 
 text \<open>
-  Note that the analogous elimination rule for disjunction
-  ``\<open>\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B\<close>'' coincides with
-  the original axiomatization of @{thm disjE}.
+  Note that the analogous elimination rule for disjunction ``\<^theory_text>\<open>assumes "A \<or> B"
+  obtains A \<BBAR> B\<close>'' 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
-  defined as a proposition that is trivially true.
+  We continue propositional logic by introducing absurdity with its
+  characteristic elimination. Plain truth may then be defined as a proposition
+  that is trivially true.
 \<close>
 
-axiomatization
-  false :: o  ("\<bottom>") where
-  falseE [elim]: "\<bottom> \<Longrightarrow> A"
+axiomatization false :: o  ("\<bottom>")
+  where falseE [elim]: "\<bottom> \<Longrightarrow> A"
 
-definition
-  true :: o  ("\<top>") where
-  "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+definition true :: o  ("\<top>")
+  where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
 
 theorem trueI [intro]: \<top>
   unfolding true_def ..
@@ -252,9 +238,8 @@
   Now negation represents an implication towards absurdity:
 \<close>
 
-definition
-  not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40) where
-  "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
+definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
+  where "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
 
 theorem notI [intro]:
   assumes "A \<Longrightarrow> \<bottom>"
@@ -278,10 +263,10 @@
 subsection \<open>Classical logic\<close>
 
 text \<open>
-  Subsequently we state the principle of classical contradiction as a
-  local assumption.  Thus we refrain from forcing the object-logic
-  into the classical perspective.  Within that context, we may derive
-  well-known consequences of the classical principle.
+  Subsequently we state the principle of classical contradiction as a local
+  assumption. Thus we refrain from forcing the object-logic into the classical
+  perspective. Within that context, we may derive well-known consequences of
+  the classical principle.
 \<close>
 
 locale classical =
@@ -312,17 +297,15 @@
 qed
 
 text \<open>
-  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
-  unchanged.  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 @{thm
-  classical} as the Isar statement ``\<open>\<OBTAINS> \<not> thesis\<close>''.
-  This also explains nicely how classical reasoning really works:
-  whatever the main \<open>thesis\<close> might be, we may always assume its
-  negation!
+  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 unchanged. 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 @{thm
+  classical} as the Isar statement ``\<^theory_text>\<open>obtains \<not> thesis\<close>''. This also explains
+  nicely how classical reasoning really works: whatever the main \<open>thesis\<close>
+  might be, we may always assume its negation!
 \<close>
 
 end
@@ -331,28 +314,25 @@
 subsection \<open>Quantifiers \label{sec:framework-ex-quant}\<close>
 
 text \<open>
-  Representing quantifiers is easy, thanks to the higher-order nature
-  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 \<open>\<lambda>\<close>-terms
-  of type @{typ "i \<Rightarrow> o"}.  Binder notation turns \<open>All (\<lambda>x. B
-  x)\<close> into \<open>\<forall>x. B x\<close> etc.
+  Representing quantifiers is easy, thanks to the higher-order nature 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 \<open>\<lambda>\<close>-terms of type @{typ "i \<Rightarrow> o"}. Binder
+  notation turns \<open>All (\<lambda>x. B x)\<close> into \<open>\<forall>x. B x\<close> etc.
 \<close>
 
-axiomatization
-  All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10) where
-  allI [intro]: "(\<And>x. B x) \<Longrightarrow> \<forall>x. B x" and
-  allD [dest]: "(\<forall>x. B x) \<Longrightarrow> B a"
+axiomatization All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
+  where allI [intro]: "(\<And>x. B x) \<Longrightarrow> \<forall>x. B x"
+    and allD [dest]: "(\<forall>x. B x) \<Longrightarrow> B a"
 
-axiomatization
-  Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10) where
-  exI [intro]: "B a \<Longrightarrow> (\<exists>x. B x)" and
-  exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C"
+axiomatization Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
+  where exI [intro]: "B a \<Longrightarrow> (\<exists>x. B x)"
+    and exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C"
 
 text \<open>
-  The statement of @{thm exE} corresponds to ``\<open>\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x\<close>'' in Isar.  In the
-  subsequent example we illustrate quantifier reasoning involving all
-  four rules:
+  The statement of @{thm exE} corresponds to ``\<^theory_text>\<open>assumes "\<exists>x. B x" obtains x
+  where "B x"\<close>'' in Isar. In the subsequent example we illustrate quantifier
+  reasoning involving all four rules:
 \<close>
 
 theorem
@@ -369,43 +349,42 @@
 
 text \<open>
   The main rules of first-order predicate logic from
-  \secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant}
-  can now be summarized as follows, using the native Isar statement
-  format of \secref{sec:framework-stmt}.
+  \secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant} can now
+  be summarized as follows, using the native Isar statement format of
+  \secref{sec:framework-stmt}.
 
   \<^medskip>
   \begin{tabular}{l}
-  \<open>impI: \<ASSUMES> A \<Longrightarrow> B \<SHOWS> A \<longrightarrow> B\<close> \\
-  \<open>impD: \<ASSUMES> A \<longrightarrow> B \<AND> A \<SHOWS> B\<close> \\[1ex]
+  \<^theory_text>\<open>impI: assumes "A \<Longrightarrow> B" shows "A \<longrightarrow> B"\<close> \\
+  \<^theory_text>\<open>impD: assumes "A \<longrightarrow> B" and A shows B\<close> \\[1ex]
 
-  \<open>disjI\<^sub>1: \<ASSUMES> A \<SHOWS> A \<or> B\<close> \\
-  \<open>disjI\<^sub>2: \<ASSUMES> B \<SHOWS> A \<or> B\<close> \\
-  \<open>disjE: \<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B\<close> \\[1ex]
+  \<^theory_text>\<open>disjI\<^sub>1: assumes A shows "A \<or> B"\<close> \\
+  \<^theory_text>\<open>disjI\<^sub>2: assumes B shows "A \<or> B"\<close> \\
+  \<^theory_text>\<open>disjE: assumes "A \<or> B" obtains A \<BBAR> B\<close> \\[1ex]
 
-  \<open>conjI: \<ASSUMES> A \<AND> B \<SHOWS> A \<and> B\<close> \\
-  \<open>conjE: \<ASSUMES> A \<and> B \<OBTAINS> A \<AND> B\<close> \\[1ex]
+  \<^theory_text>\<open>conjI: assumes A and B shows A \<and> B\<close> \\
+  \<^theory_text>\<open>conjE: assumes "A \<and> B" obtains A and B\<close> \\[1ex]
 
-  \<open>falseE: \<ASSUMES> \<bottom> \<SHOWS> A\<close> \\
-  \<open>trueI: \<SHOWS> \<top>\<close> \\[1ex]
+  \<^theory_text>\<open>falseE: assumes \<bottom> shows A\<close> \\
+  \<^theory_text>\<open>trueI: shows \<top>\<close> \\[1ex]
 
-  \<open>notI: \<ASSUMES> A \<Longrightarrow> \<bottom> \<SHOWS> \<not> A\<close> \\
-  \<open>notE: \<ASSUMES> \<not> A \<AND> A \<SHOWS> B\<close> \\[1ex]
+  \<^theory_text>\<open>notI: assumes "A \<Longrightarrow> \<bottom>" shows "\<not> A"\<close> \\
+  \<^theory_text>\<open>notE: assumes "\<not> A" and A shows B\<close> \\[1ex]
 
-  \<open>allI: \<ASSUMES> \<And>x. B x \<SHOWS> \<forall>x. B x\<close> \\
-  \<open>allE: \<ASSUMES> \<forall>x. B x \<SHOWS> B a\<close> \\[1ex]
+  \<^theory_text>\<open>allI: assumes "\<And>x. B x" shows "\<forall>x. B x"\<close> \\
+  \<^theory_text>\<open>allE: assumes "\<forall>x. B x" shows "B a"\<close> \\[1ex]
 
-  \<open>exI: \<ASSUMES> B a \<SHOWS> \<exists>x. B x\<close> \\
-  \<open>exE: \<ASSUMES> \<exists>x. B x \<OBTAINS> a \<WHERE> B a\<close>
+  \<^theory_text>\<open>exI: assumes "B a" shows "\<exists>x. B x"\<close> \\
+  \<^theory_text>\<open>exE: assumes "\<exists>x. B x" obtains a where "B a"\<close>
   \end{tabular}
   \<^medskip>
 
-  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
-  (Pure) elim}, @{attribute (Pure) dest} --- each according to its
-  particular shape --- we can immediately write Isar proof texts as
-  follows:
+  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 (Pure) elim}, @{attribute (Pure)
+  dest} --- each according to its particular shape --- we can immediately
+  write Isar proof texts as follows:
 \<close>
 
 (*<*)
@@ -511,11 +490,10 @@
 
 text \<open>
   \<^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
-  literary quality.
+  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 literary quality.
 \<close>
 
 end %visible