--- a/doc-src/IsarRef/IsaMakefile Wed Feb 11 21:41:05 2009 +0100
+++ b/doc-src/IsarRef/IsaMakefile Thu Feb 12 11:19:12 2009 +0100
@@ -22,10 +22,11 @@
HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML \
- Thy/Framework.thy Thy/Inner_Syntax.thy Thy/Introduction.thy \
- Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy Thy/Misc.thy \
- Thy/Document_Preparation.thy Thy/Generic.thy Thy/HOL_Specific.thy \
- Thy/Quick_Reference.thy Thy/Symbols.thy Thy/ML_Tactic.thy
+ Thy/First_Order_Logic.thy Thy/Framework.thy Thy/Inner_Syntax.thy \
+ Thy/Introduction.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy \
+ Thy/Misc.thy Thy/Document_Preparation.thy Thy/Generic.thy \
+ Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/Symbols.thy \
+ Thy/ML_Tactic.thy
@$(USEDIR) -s IsarRef HOL Thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy Thu Feb 12 11:19:12 2009 +0100
@@ -0,0 +1,365 @@
+
+header {* Example: First-Order Logic *}
+
+theory %visible First_Order_Logic
+imports Pure
+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.
+*}
+
+typedecl i
+typedecl o
+
+judgment
+ Trueprop :: "o \<Rightarrow> prop" ("_" 5)
+
+text {*
+ \noindent Note that the object-logic judgement 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''.
+*}
+
+
+subsection {* Equational reasoning \label{sec:framework-ex-equal} *}
+
+text {*
+ 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}.
+*}
+
+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 {*
+ \noindent Substitution is very powerful, but also hard to control in
+ full generality. We derive some common symmetry~/ transitivity
+ schemes of as particular consequences.
+*}
+
+theorem sym [sym]:
+ assumes "x = y"
+ shows "y = x"
+proof -
+ have "x = x" ..
+ with `x = y` show "y = x" ..
+qed
+
+theorem forw_subst [trans]:
+ assumes "y = x" and "B x"
+ shows "B y"
+proof -
+ from `y = x` have "x = y" ..
+ from this and `B x` show "B y" ..
+qed
+
+theorem back_subst [trans]:
+ assumes "B x" and "x = y"
+ shows "B y"
+proof -
+ from `x = y` and `B x`
+ show "B y" ..
+qed
+
+theorem trans [trans]:
+ assumes "x = y" and "y = z"
+ shows "x = z"
+proof -
+ from `y = z` and `x = y`
+ show "x = z" ..
+qed
+
+
+subsection {* Basic group theory *}
+
+text {*
+ 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.
+*}
+
+locale group =
+ fixes prod :: "i \<Rightarrow> i \<Rightarrow> i" (infix "\<circ>" 70)
+ and inv :: "i \<Rightarrow> i" ("(_\<inverse>)" [1000] 999)
+ and unit :: i ("1")
+ assumes assoc: "(x \<circ> y) \<circ> z = x \<circ> (y \<circ> z)"
+ and left_unit: "1 \<circ> x = x"
+ and left_inv: "x\<inverse> \<circ> x = 1"
+begin
+
+theorem right_inv: "x \<circ> x\<inverse> = 1"
+proof -
+ have "x \<circ> x\<inverse> = 1 \<circ> (x \<circ> x\<inverse>)" by (rule left_unit [symmetric])
+ also have "\<dots> = (1 \<circ> x) \<circ> x\<inverse>" by (rule assoc [symmetric])
+ also have "1 = (x\<inverse>)\<inverse> \<circ> x\<inverse>" by (rule left_inv [symmetric])
+ also have "\<dots> \<circ> x = (x\<inverse>)\<inverse> \<circ> (x\<inverse> \<circ> x)" by (rule assoc)
+ also have "x\<inverse> \<circ> x = 1" by (rule left_inv)
+ also have "((x\<inverse>)\<inverse> \<circ> \<dots>) \<circ> x\<inverse> = (x\<inverse>)\<inverse> \<circ> (1 \<circ> x\<inverse>)" by (rule assoc)
+ also have "1 \<circ> x\<inverse> = x\<inverse>" by (rule left_unit)
+ also have "(x\<inverse>)\<inverse> \<circ> \<dots> = 1" by (rule left_inv)
+ finally show "x \<circ> x\<inverse> = 1" .
+qed
+
+theorem right_unit: "x \<circ> 1 = x"
+proof -
+ have "1 = x\<inverse> \<circ> x" by (rule left_inv [symmetric])
+ also have "x \<circ> \<dots> = (x \<circ> x\<inverse>) \<circ> x" by (rule assoc [symmetric])
+ also have "x \<circ> x\<inverse> = 1" by (rule right_inv)
+ also have "\<dots> \<circ> x = x" by (rule left_unit)
+ finally show "x \<circ> 1 = x" .
+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
+ 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
+ \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:
+*}
+
+(*<*)
+theorem "\<And>A. PROP A \<Longrightarrow> PROP A"
+proof -
+ assume [symmetric, defn]: "\<And>x y. (x \<equiv> y) \<equiv> Trueprop (x = y)"
+(*>*)
+ have "x \<circ> 1 = x \<circ> (x\<inverse> \<circ> x)" unfolding left_inv ..
+ also have "\<dots> = (x \<circ> x\<inverse>) \<circ> x" unfolding assoc ..
+ also have "\<dots> = 1 \<circ> x" unfolding right_inv ..
+ also have "\<dots> = x" unfolding left_unit ..
+ finally have "x \<circ> 1 = x" .
+(*<*)
+qed
+(*>*)
+
+text {*
+ \noindent 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}~@{text
+ left_inv}~@{command ".."}'' would become ``@{command "by"}~@{text
+ "(simp add: left_inv)"}'' etc.
+*}
+
+end
+
+
+subsection {* Propositional logic *}
+
+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}.
+*}
+
+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
+ disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C" and
+ disjI\<^isub>1 [intro]: "A \<Longrightarrow> A \<or> B" and
+ disjI\<^isub>2 [intro]: "B \<Longrightarrow> A \<or> B"
+
+axiomatization
+ conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) where
+ conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and
+ conjD\<^isub>1 [dest]: "A \<and> B \<Longrightarrow> A" and
+ conjD\<^isub>2 [dest]: "A \<and> B \<Longrightarrow> B"
+
+text {*
+ \noindent 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:
+*}
+
+theorem conjE [elim]:
+ assumes "A \<and> B"
+ obtains A and B
+proof
+ from `A \<and> B` show A ..
+ from `A \<and> B` show B ..
+qed
+
+text {*
+ \noindent Here is an example of swapping conjuncts with a single
+ intermediate elimination step:
+*}
+
+(*<*)
+lemma "\<And>A. PROP A \<Longrightarrow> PROP A"
+proof -
+(*>*)
+ assume "A \<and> B"
+ then obtain B and A ..
+ then have "B \<and> A" ..
+(*<*)
+qed
+(*>*)
+
+text {*
+ Note that the analogous elimination for disjunction ``@{text
+ "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with the
+ original axiomatization of @{text "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.
+*}
+
+axiomatization
+ false :: o ("\<bottom>") where
+ falseE [elim]: "\<bottom> \<Longrightarrow> A"
+
+definition
+ true :: o ("\<top>") where
+ "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+
+theorem trueI [intro]: \<top>
+ unfolding true_def ..
+
+text {*
+ \medskip Now negation represents an implication towards absurdity:
+*}
+
+definition
+ not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) where
+ "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
+
+theorem notI [intro]:
+ assumes "A \<Longrightarrow> \<bottom>"
+ shows "\<not> A"
+unfolding not_def
+proof
+ assume A
+ then show \<bottom> by (rule `A \<Longrightarrow> \<bottom>`)
+qed
+
+theorem notE [elim]:
+ assumes "\<not> A" and A
+ shows B
+proof -
+ from `\<not> A` have "A \<longrightarrow> \<bottom>" unfolding not_def .
+ from `A \<longrightarrow> \<bottom>` and `A` have \<bottom> ..
+ then show B ..
+qed
+
+
+subsection {* Classical logic *}
+
+text {*
+ 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.
+*}
+
+locale classical =
+ assumes classical: "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"
+begin
+
+theorem double_negation:
+ assumes "\<not> \<not> C"
+ shows C
+proof (rule classical)
+ assume "\<not> C"
+ with `\<not> \<not> C` show C ..
+qed
+
+theorem tertium_non_datur: "C \<or> \<not> C"
+proof (rule double_negation)
+ show "\<not> \<not> (C \<or> \<not> C)"
+ proof
+ assume "\<not> (C \<or> \<not> C)"
+ have "\<not> C"
+ proof
+ assume C then have "C \<or> \<not> C" ..
+ with `\<not> (C \<or> \<not> C)` show \<bottom> ..
+ qed
+ then have "C \<or> \<not> C" ..
+ with `\<not> (C \<or> \<not> C)` show \<bottom> ..
+ qed
+qed
+
+text {*
+ 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 @{text "(\<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 @{text "classical"} as the
+ Isar statement ``@{text "\<OBTAINS> \<not> thesis"}''. This also
+ explains nicely how classical reasoning really works: whatever the
+ main @{text thesis} might be, we may always assume its negation!
+*}
+
+end
+
+
+subsection {* Quantifiers *}
+
+text {*
+ 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 @{text "\<lambda>"}-terms
+ of type @{text "i \<Rightarrow> o"}. Specific binder notation relates @{text
+ "All (\<lambda>x. B x)"} to @{text "\<forall>x. B x"} etc.
+*}
+
+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"
+
+text {*
+ \noindent The @{thm exE} rule corresponds to an Isar statement
+ ``@{text "\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x"}''. In the
+ following example we illustrate quantifier reasoning with all four
+ rules:
+*}
+
+theorem
+ assumes "\<exists>x. \<forall>y. R x y"
+ shows "\<forall>y. \<exists>x. R x y"
+proof -- {* @{text "\<forall>"} introduction *}
+ obtain x where "\<forall>y. R x y" using `\<exists>x. \<forall>y. R x y` .. -- {* @{text "\<exists>"} elimination *}
+ fix y have "R x y" using `\<forall>y. R x y` .. -- {* @{text "\<forall>"} destruction *}
+ then show "\<exists>x. R x y" .. -- {* @{text "\<exists>"} introduction *}
+qed
+
+end %visible
--- a/doc-src/IsarRef/Thy/ROOT.ML Wed Feb 11 21:41:05 2009 +0100
+++ b/doc-src/IsarRef/Thy/ROOT.ML Thu Feb 12 11:19:12 2009 +0100
@@ -4,6 +4,7 @@
use_thy "Introduction";
use_thy "Framework";
+use_thy "First_Order_Logic";
use_thy "Outer_Syntax";
use_thy "Document_Preparation";
use_thy "Spec";
--- a/doc-src/IsarRef/isar-ref.tex Wed Feb 11 21:41:05 2009 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Thu Feb 12 11:19:12 2009 +0100
@@ -82,6 +82,7 @@
\part{Basic Concepts}
\input{Thy/document/Introduction.tex}
\input{Thy/document/Framework.tex}
+\input{Thy/document/First_Order_Logic.tex}
\part{General Language Elements}
\input{Thy/document/Outer_Syntax.tex}
\input{Thy/document/Document_Preparation.tex}