# HG changeset patch # User wenzelm # Date 1234434975 -3600 # Node ID 0a643dd9e0f5dcf3d7073d1299fc3db356b6f0ab # Parent efcbbd7baa0216254a5e59ad6be07870d2c12cd8 tuned; diff -r efcbbd7baa02 -r 0a643dd9e0f5 doc-src/IsarRef/Thy/First_Order_Logic.thy --- 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 - "\ A \ B \ A \ B"}'' coincides with the - original axiomatization of @{text "disjE"}. + \noindent Note that the analogous elimination rule for disjunction + ``@{text "\ A \ B \ A \ 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 "(\ C \ C) \ C"} fits again into our format for + Note that @{prop "(\ C \ C) \ 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 "\ \ 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 "\"}-terms - of type @{text "i \ o"}. Specific binder notation relates @{text - "All (\x. B x)"} to @{text "\x. B x"} etc. + of type @{typ "i \ o"}. Binder notation turns @{text "All (\x. B + x)"} into @{text "\x. B x"} etc. *} axiomatization diff -r efcbbd7baa02 -r 0a643dd9e0f5 doc-src/IsarRef/Thy/Framework.thy --- 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 "\"}, @{text "\"}, @{text "\"} etc. - Due to the flexibility of rule composition + relations of @{text "="}, @{text "<"}, @{text "\"}, @{text "\"}, + @{text "\"} 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 involving monotonicity conditions; see also \cite[\S6]{Wenzel-PhD} @@ -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"} \\