summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 12 Oct 2015 21:42:14 +0200 | |

changeset 61420 | ee42cba50933 |

parent 61419 | 3c3f8b182e4b |

child 61421 | e0825405d398 |

redundant due to \parindent 0pt;

--- 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.