1.1 --- a/doc-src/IsarRef/IsaMakefile Wed Feb 11 21:41:05 2009 +0100
1.2 +++ b/doc-src/IsarRef/IsaMakefile Thu Feb 12 11:19:12 2009 +0100
1.3 @@ -22,10 +22,11 @@
1.4 HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
1.5
1.6 $(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML \
1.7 - Thy/Framework.thy Thy/Inner_Syntax.thy Thy/Introduction.thy \
1.8 - Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy Thy/Misc.thy \
1.9 - Thy/Document_Preparation.thy Thy/Generic.thy Thy/HOL_Specific.thy \
1.10 - Thy/Quick_Reference.thy Thy/Symbols.thy Thy/ML_Tactic.thy
1.11 + Thy/First_Order_Logic.thy Thy/Framework.thy Thy/Inner_Syntax.thy \
1.12 + Thy/Introduction.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy \
1.13 + Thy/Misc.thy Thy/Document_Preparation.thy Thy/Generic.thy \
1.14 + Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/Symbols.thy \
1.15 + Thy/ML_Tactic.thy
1.16 @$(USEDIR) -s IsarRef HOL Thy
1.17
1.18
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy Thu Feb 12 11:19:12 2009 +0100
2.3 @@ -0,0 +1,365 @@
2.4 +
2.5 +header {* Example: First-Order Logic *}
2.6 +
2.7 +theory %visible First_Order_Logic
2.8 +imports Pure
2.9 +begin
2.10 +
2.11 +text {*
2.12 + In order to commence a new object-logic within Isabelle/Pure we
2.13 + introduce abstract syntactic categories @{text "i"} for individuals
2.14 + and @{text "o"} for object-propositions. The latter is embedded
2.15 + into the language of Pure propositions by means of a separate
2.16 + judgment.
2.17 +*}
2.18 +
2.19 +typedecl i
2.20 +typedecl o
2.21 +
2.22 +judgment
2.23 + Trueprop :: "o \<Rightarrow> prop" ("_" 5)
2.24 +
2.25 +text {*
2.26 + \noindent Note that the object-logic judgement is implicit in the
2.27 + syntax: writing @{prop A} produces @{term "Trueprop A"} internally.
2.28 + From the Pure perspective this means ``@{prop A} is derivable in the
2.29 + object-logic''.
2.30 +*}
2.31 +
2.32 +
2.33 +subsection {* Equational reasoning \label{sec:framework-ex-equal} *}
2.34 +
2.35 +text {*
2.36 + Equality is axiomatized as a binary predicate on individuals, with
2.37 + reflexivity as introduction, and substitution as elimination
2.38 + principle. Note that the latter is particularly convenient in a
2.39 + framework like Isabelle, because syntactic congruences are
2.40 + implicitly produced by unification of @{term "B x"} against
2.41 + expressions containing occurrences of @{term x}.
2.42 +*}
2.43 +
2.44 +axiomatization
2.45 + equal :: "i \<Rightarrow> i \<Rightarrow> o" (infix "=" 50)
2.46 +where
2.47 + refl [intro]: "x = x" and
2.48 + subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y"
2.49 +
2.50 +text {*
2.51 + \noindent Substitution is very powerful, but also hard to control in
2.52 + full generality. We derive some common symmetry~/ transitivity
2.53 + schemes of as particular consequences.
2.54 +*}
2.55 +
2.56 +theorem sym [sym]:
2.57 + assumes "x = y"
2.58 + shows "y = x"
2.59 +proof -
2.60 + have "x = x" ..
2.61 + with `x = y` show "y = x" ..
2.62 +qed
2.63 +
2.64 +theorem forw_subst [trans]:
2.65 + assumes "y = x" and "B x"
2.66 + shows "B y"
2.67 +proof -
2.68 + from `y = x` have "x = y" ..
2.69 + from this and `B x` show "B y" ..
2.70 +qed
2.71 +
2.72 +theorem back_subst [trans]:
2.73 + assumes "B x" and "x = y"
2.74 + shows "B y"
2.75 +proof -
2.76 + from `x = y` and `B x`
2.77 + show "B y" ..
2.78 +qed
2.79 +
2.80 +theorem trans [trans]:
2.81 + assumes "x = y" and "y = z"
2.82 + shows "x = z"
2.83 +proof -
2.84 + from `y = z` and `x = y`
2.85 + show "x = z" ..
2.86 +qed
2.87 +
2.88 +
2.89 +subsection {* Basic group theory *}
2.90 +
2.91 +text {*
2.92 + As an example for equational reasoning we consider some bits of
2.93 + group theory. The subsequent locale definition postulates group
2.94 + operations and axioms; we also derive some consequences of this
2.95 + specification.
2.96 +*}
2.97 +
2.98 +locale group =
2.99 + fixes prod :: "i \<Rightarrow> i \<Rightarrow> i" (infix "\<circ>" 70)
2.100 + and inv :: "i \<Rightarrow> i" ("(_\<inverse>)" [1000] 999)
2.101 + and unit :: i ("1")
2.102 + assumes assoc: "(x \<circ> y) \<circ> z = x \<circ> (y \<circ> z)"
2.103 + and left_unit: "1 \<circ> x = x"
2.104 + and left_inv: "x\<inverse> \<circ> x = 1"
2.105 +begin
2.106 +
2.107 +theorem right_inv: "x \<circ> x\<inverse> = 1"
2.108 +proof -
2.109 + have "x \<circ> x\<inverse> = 1 \<circ> (x \<circ> x\<inverse>)" by (rule left_unit [symmetric])
2.110 + also have "\<dots> = (1 \<circ> x) \<circ> x\<inverse>" by (rule assoc [symmetric])
2.111 + also have "1 = (x\<inverse>)\<inverse> \<circ> x\<inverse>" by (rule left_inv [symmetric])
2.112 + also have "\<dots> \<circ> x = (x\<inverse>)\<inverse> \<circ> (x\<inverse> \<circ> x)" by (rule assoc)
2.113 + also have "x\<inverse> \<circ> x = 1" by (rule left_inv)
2.114 + also have "((x\<inverse>)\<inverse> \<circ> \<dots>) \<circ> x\<inverse> = (x\<inverse>)\<inverse> \<circ> (1 \<circ> x\<inverse>)" by (rule assoc)
2.115 + also have "1 \<circ> x\<inverse> = x\<inverse>" by (rule left_unit)
2.116 + also have "(x\<inverse>)\<inverse> \<circ> \<dots> = 1" by (rule left_inv)
2.117 + finally show "x \<circ> x\<inverse> = 1" .
2.118 +qed
2.119 +
2.120 +theorem right_unit: "x \<circ> 1 = x"
2.121 +proof -
2.122 + have "1 = x\<inverse> \<circ> x" by (rule left_inv [symmetric])
2.123 + also have "x \<circ> \<dots> = (x \<circ> x\<inverse>) \<circ> x" by (rule assoc [symmetric])
2.124 + also have "x \<circ> x\<inverse> = 1" by (rule right_inv)
2.125 + also have "\<dots> \<circ> x = x" by (rule left_unit)
2.126 + finally show "x \<circ> 1 = x" .
2.127 +qed
2.128 +
2.129 +text {*
2.130 + Reasoning from basic axioms is often tedious. Our proofs work by
2.131 + producing various instances of the given rules (potentially the
2.132 + symmetric form) using the pattern ``@{command have}~@{text
2.133 + eq}~@{command "by"}~@{text "(rule r)"}'' and composing the chain of
2.134 + results via @{command also}/@{command finally}. These steps may
2.135 + involve any of the transitivity rules declared in
2.136 + \secref{sec:framework-ex-equal}, namely @{thm trans} in combining
2.137 + the first two results in @{thm right_inv} and in the final steps of
2.138 + both proofs, @{thm forw_subst} in the first combination of @{thm
2.139 + right_unit}, and @{thm back_subst} in all other calculational steps.
2.140 +
2.141 + Occasional substitutions in calculations are adequate, but should
2.142 + not be over-emphasized. The other extreme is to compose a chain by
2.143 + plain transitivity only, with replacements occurring always in
2.144 + topmost position. For example:
2.145 +*}
2.146 +
2.147 +(*<*)
2.148 +theorem "\<And>A. PROP A \<Longrightarrow> PROP A"
2.149 +proof -
2.150 + assume [symmetric, defn]: "\<And>x y. (x \<equiv> y) \<equiv> Trueprop (x = y)"
2.151 +(*>*)
2.152 + have "x \<circ> 1 = x \<circ> (x\<inverse> \<circ> x)" unfolding left_inv ..
2.153 + also have "\<dots> = (x \<circ> x\<inverse>) \<circ> x" unfolding assoc ..
2.154 + also have "\<dots> = 1 \<circ> x" unfolding right_inv ..
2.155 + also have "\<dots> = x" unfolding left_unit ..
2.156 + finally have "x \<circ> 1 = x" .
2.157 +(*<*)
2.158 +qed
2.159 +(*>*)
2.160 +
2.161 +text {*
2.162 + \noindent Here we have re-used the built-in mechanism for unfolding
2.163 + definitions in order to normalize each equational problem. A more
2.164 + realistic object-logic would include proper setup for the Simplifier
2.165 + (\secref{sec:simplifier}), the main automated tool for equational
2.166 + reasoning in Isabelle. Then ``@{command unfolding}~@{text
2.167 + left_inv}~@{command ".."}'' would become ``@{command "by"}~@{text
2.168 + "(simp add: left_inv)"}'' etc.
2.169 +*}
2.170 +
2.171 +end
2.172 +
2.173 +
2.174 +subsection {* Propositional logic *}
2.175 +
2.176 +text {*
2.177 + We axiomatize basic connectives of propositional logic: implication,
2.178 + disjunction, and conjunction. The associated rules are modeled
2.179 + after Gentzen's natural deduction \cite{Gentzen:1935}.
2.180 +*}
2.181 +
2.182 +axiomatization
2.183 + imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) where
2.184 + impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
2.185 + impD [dest]: "(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B"
2.186 +
2.187 +axiomatization
2.188 + disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) where
2.189 + disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C" and
2.190 + disjI\<^isub>1 [intro]: "A \<Longrightarrow> A \<or> B" and
2.191 + disjI\<^isub>2 [intro]: "B \<Longrightarrow> A \<or> B"
2.192 +
2.193 +axiomatization
2.194 + conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) where
2.195 + conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and
2.196 + conjD\<^isub>1 [dest]: "A \<and> B \<Longrightarrow> A" and
2.197 + conjD\<^isub>2 [dest]: "A \<and> B \<Longrightarrow> B"
2.198 +
2.199 +text {*
2.200 + \noindent The conjunctive destructions have the disadvantage that
2.201 + decomposing @{prop "A \<and> B"} involves an immediate decision which
2.202 + component should be projected. The more convenient simultaneous
2.203 + elimination @{prop "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"} can be derived as
2.204 + follows:
2.205 +*}
2.206 +
2.207 +theorem conjE [elim]:
2.208 + assumes "A \<and> B"
2.209 + obtains A and B
2.210 +proof
2.211 + from `A \<and> B` show A ..
2.212 + from `A \<and> B` show B ..
2.213 +qed
2.214 +
2.215 +text {*
2.216 + \noindent Here is an example of swapping conjuncts with a single
2.217 + intermediate elimination step:
2.218 +*}
2.219 +
2.220 +(*<*)
2.221 +lemma "\<And>A. PROP A \<Longrightarrow> PROP A"
2.222 +proof -
2.223 +(*>*)
2.224 + assume "A \<and> B"
2.225 + then obtain B and A ..
2.226 + then have "B \<and> A" ..
2.227 +(*<*)
2.228 +qed
2.229 +(*>*)
2.230 +
2.231 +text {*
2.232 + Note that the analogous elimination for disjunction ``@{text
2.233 + "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with the
2.234 + original axiomatization of @{text "disjE"}.
2.235 +
2.236 + \medskip We continue propositional logic by introducing absurdity
2.237 + with its characteristic elimination. Plain truth may then be
2.238 + defined as a proposition that is trivially true.
2.239 +*}
2.240 +
2.241 +axiomatization
2.242 + false :: o ("\<bottom>") where
2.243 + falseE [elim]: "\<bottom> \<Longrightarrow> A"
2.244 +
2.245 +definition
2.246 + true :: o ("\<top>") where
2.247 + "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
2.248 +
2.249 +theorem trueI [intro]: \<top>
2.250 + unfolding true_def ..
2.251 +
2.252 +text {*
2.253 + \medskip Now negation represents an implication towards absurdity:
2.254 +*}
2.255 +
2.256 +definition
2.257 + not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) where
2.258 + "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
2.259 +
2.260 +theorem notI [intro]:
2.261 + assumes "A \<Longrightarrow> \<bottom>"
2.262 + shows "\<not> A"
2.263 +unfolding not_def
2.264 +proof
2.265 + assume A
2.266 + then show \<bottom> by (rule `A \<Longrightarrow> \<bottom>`)
2.267 +qed
2.268 +
2.269 +theorem notE [elim]:
2.270 + assumes "\<not> A" and A
2.271 + shows B
2.272 +proof -
2.273 + from `\<not> A` have "A \<longrightarrow> \<bottom>" unfolding not_def .
2.274 + from `A \<longrightarrow> \<bottom>` and `A` have \<bottom> ..
2.275 + then show B ..
2.276 +qed
2.277 +
2.278 +
2.279 +subsection {* Classical logic *}
2.280 +
2.281 +text {*
2.282 + Subsequently we state the principle of classical contradiction as a
2.283 + local assumption. Thus we refrain from forcing the object-logic
2.284 + into the classical perspective. Within that context, we may derive
2.285 + well-known consequences of the classical principle.
2.286 +*}
2.287 +
2.288 +locale classical =
2.289 + assumes classical: "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"
2.290 +begin
2.291 +
2.292 +theorem double_negation:
2.293 + assumes "\<not> \<not> C"
2.294 + shows C
2.295 +proof (rule classical)
2.296 + assume "\<not> C"
2.297 + with `\<not> \<not> C` show C ..
2.298 +qed
2.299 +
2.300 +theorem tertium_non_datur: "C \<or> \<not> C"
2.301 +proof (rule double_negation)
2.302 + show "\<not> \<not> (C \<or> \<not> C)"
2.303 + proof
2.304 + assume "\<not> (C \<or> \<not> C)"
2.305 + have "\<not> C"
2.306 + proof
2.307 + assume C then have "C \<or> \<not> C" ..
2.308 + with `\<not> (C \<or> \<not> C)` show \<bottom> ..
2.309 + qed
2.310 + then have "C \<or> \<not> C" ..
2.311 + with `\<not> (C \<or> \<not> C)` show \<bottom> ..
2.312 + qed
2.313 +qed
2.314 +
2.315 +text {*
2.316 + These examples illustrate both classical reasoning and non-trivial
2.317 + propositional proofs in general. All three rules characterize
2.318 + classical logic independently, but the original rule is already the
2.319 + most convenient to use, because it leaves the conclusion unchanged.
2.320 + Note that @{text "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"} fits again into our format for
2.321 + eliminations, despite the additional twist that the context refers
2.322 + to the main conclusion. So we may write @{text "classical"} as the
2.323 + Isar statement ``@{text "\<OBTAINS> \<not> thesis"}''. This also
2.324 + explains nicely how classical reasoning really works: whatever the
2.325 + main @{text thesis} might be, we may always assume its negation!
2.326 +*}
2.327 +
2.328 +end
2.329 +
2.330 +
2.331 +subsection {* Quantifiers *}
2.332 +
2.333 +text {*
2.334 + Representing quantifiers is easy, thanks to the higher-order nature
2.335 + of the underlying framework. According to the well-known technique
2.336 + introduced by Church \cite{church40}, quantifiers are operators on
2.337 + predicates, which are syntactically represented as @{text "\<lambda>"}-terms
2.338 + of type @{text "i \<Rightarrow> o"}. Specific binder notation relates @{text
2.339 + "All (\<lambda>x. B x)"} to @{text "\<forall>x. B x"} etc.
2.340 +*}
2.341 +
2.342 +axiomatization
2.343 + All :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) where
2.344 + allI [intro]: "(\<And>x. B x) \<Longrightarrow> \<forall>x. B x" and
2.345 + allD [dest]: "(\<forall>x. B x) \<Longrightarrow> B a"
2.346 +
2.347 +axiomatization
2.348 + Ex :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) where
2.349 + exI [intro]: "B a \<Longrightarrow> (\<exists>x. B x)" and
2.350 + exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C"
2.351 +
2.352 +text {*
2.353 + \noindent The @{thm exE} rule corresponds to an Isar statement
2.354 + ``@{text "\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x"}''. In the
2.355 + following example we illustrate quantifier reasoning with all four
2.356 + rules:
2.357 +*}
2.358 +
2.359 +theorem
2.360 + assumes "\<exists>x. \<forall>y. R x y"
2.361 + shows "\<forall>y. \<exists>x. R x y"
2.362 +proof -- {* @{text "\<forall>"} introduction *}
2.363 + obtain x where "\<forall>y. R x y" using `\<exists>x. \<forall>y. R x y` .. -- {* @{text "\<exists>"} elimination *}
2.364 + fix y have "R x y" using `\<forall>y. R x y` .. -- {* @{text "\<forall>"} destruction *}
2.365 + then show "\<exists>x. R x y" .. -- {* @{text "\<exists>"} introduction *}
2.366 +qed
2.367 +
2.368 +end %visible
3.1 --- a/doc-src/IsarRef/Thy/ROOT.ML Wed Feb 11 21:41:05 2009 +0100
3.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML Thu Feb 12 11:19:12 2009 +0100
3.3 @@ -4,6 +4,7 @@
3.4
3.5 use_thy "Introduction";
3.6 use_thy "Framework";
3.7 +use_thy "First_Order_Logic";
3.8 use_thy "Outer_Syntax";
3.9 use_thy "Document_Preparation";
3.10 use_thy "Spec";
4.1 --- a/doc-src/IsarRef/isar-ref.tex Wed Feb 11 21:41:05 2009 +0100
4.2 +++ b/doc-src/IsarRef/isar-ref.tex Thu Feb 12 11:19:12 2009 +0100
4.3 @@ -82,6 +82,7 @@
4.4 \part{Basic Concepts}
4.5 \input{Thy/document/Introduction.tex}
4.6 \input{Thy/document/Framework.tex}
4.7 +\input{Thy/document/First_Order_Logic.tex}
4.8 \part{General Language Elements}
4.9 \input{Thy/document/Outer_Syntax.tex}
4.10 \input{Thy/document/Document_Preparation.tex}