wenzelm@30056: 
wenzelm@30056: header {* Example: First-Order Logic *}
wenzelm@30056: 
wenzelm@30056: theory %visible First_Order_Logic
wenzelm@43522: imports Base  (* FIXME Pure!? *)
wenzelm@30056: begin
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30058:   \noindent In order to commence a new object-logic within
wenzelm@30058:   Isabelle/Pure we introduce abstract syntactic categories @{text "i"}
wenzelm@30058:   for individuals and @{text "o"} for object-propositions.  The latter
wenzelm@30058:   is embedded into the language of Pure propositions by means of a
wenzelm@30058:   separate judgment.
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: typedecl i
wenzelm@30056: typedecl o
wenzelm@30056: 
wenzelm@30056: judgment
wenzelm@30056:   Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30056:   \noindent Note that the object-logic judgement is implicit in the
wenzelm@30056:   syntax: writing @{prop A} produces @{term "Trueprop A"} internally.
wenzelm@30056:   From the Pure perspective this means ``@{prop A} is derivable in the
wenzelm@30056:   object-logic''.
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: 
wenzelm@30056: subsection {* Equational reasoning \label{sec:framework-ex-equal} *}
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30056:   Equality is axiomatized as a binary predicate on individuals, with
wenzelm@30056:   reflexivity as introduction, and substitution as elimination
wenzelm@30056:   principle.  Note that the latter is particularly convenient in a
wenzelm@30056:   framework like Isabelle, because syntactic congruences are
wenzelm@30056:   implicitly produced by unification of @{term "B x"} against
wenzelm@30056:   expressions containing occurrences of @{term x}.
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: axiomatization
wenzelm@30056:   equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infix "=" 50)
wenzelm@30056: where
wenzelm@30056:   refl [intro]: "x = x" and
wenzelm@30056:   subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y"
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30056:   \noindent Substitution is very powerful, but also hard to control in
wenzelm@30056:   full generality.  We derive some common symmetry~/ transitivity
wenzelm@45988:   schemes of @{term equal} as particular consequences.
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: theorem sym [sym]:
wenzelm@30056:   assumes "x = y"
wenzelm@30056:   shows "y = x"
wenzelm@30056: proof -
wenzelm@30056:   have "x = x" ..
wenzelm@30056:   with `x = y` show "y = x" ..
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30056: theorem forw_subst [trans]:
wenzelm@30056:   assumes "y = x" and "B x"
wenzelm@30056:   shows "B y"
wenzelm@30056: proof -
wenzelm@30056:   from `y = x` have "x = y" ..
wenzelm@30056:   from this and `B x` show "B y" ..
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30056: theorem back_subst [trans]:
wenzelm@30056:   assumes "B x" and "x = y"
wenzelm@30056:   shows "B y"
wenzelm@30056: proof -
wenzelm@30056:   from `x = y` and `B x`
wenzelm@30056:   show "B y" ..
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30056: theorem trans [trans]:
wenzelm@30056:   assumes "x = y" and "y = z"
wenzelm@30056:   shows "x = z"
wenzelm@30056: proof -
wenzelm@30056:   from `y = z` and `x = y`
wenzelm@30056:   show "x = z" ..
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30056: 
wenzelm@30056: subsection {* Basic group theory *}
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30056:   As an example for equational reasoning we consider some bits of
wenzelm@30056:   group theory.  The subsequent locale definition postulates group
wenzelm@30056:   operations and axioms; we also derive some consequences of this
wenzelm@30056:   specification.
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: locale group =
wenzelm@30056:   fixes prod :: "i \<Rightarrow> i \<Rightarrow> i"  (infix "\<circ>" 70)
wenzelm@30056:     and inv :: "i \<Rightarrow> i"  ("(_\<inverse>)" [1000] 999)
wenzelm@30056:     and unit :: i  ("1")
wenzelm@30056:   assumes assoc: "(x \<circ> y) \<circ> z = x \<circ> (y \<circ> z)"
wenzelm@30056:     and left_unit:  "1 \<circ> x = x"
wenzelm@30056:     and left_inv: "x\<inverse> \<circ> x = 1"
wenzelm@30056: begin
wenzelm@30056: 
wenzelm@30056: theorem right_inv: "x \<circ> x\<inverse> = 1"
wenzelm@30056: proof -
wenzelm@30056:   have "x \<circ> x\<inverse> = 1 \<circ> (x \<circ> x\<inverse>)" by (rule left_unit [symmetric])
wenzelm@30056:   also have "\<dots> = (1 \<circ> x) \<circ> x\<inverse>" by (rule assoc [symmetric])
wenzelm@30056:   also have "1 = (x\<inverse>)\<inverse> \<circ> x\<inverse>" by (rule left_inv [symmetric])
wenzelm@30056:   also have "\<dots> \<circ> x = (x\<inverse>)\<inverse> \<circ> (x\<inverse> \<circ> x)" by (rule assoc)
wenzelm@30056:   also have "x\<inverse> \<circ> x = 1" by (rule left_inv)
wenzelm@30056:   also have "((x\<inverse>)\<inverse> \<circ> \<dots>) \<circ> x\<inverse> = (x\<inverse>)\<inverse> \<circ> (1 \<circ> x\<inverse>)" by (rule assoc)
wenzelm@30056:   also have "1 \<circ> x\<inverse> = x\<inverse>" by (rule left_unit)
wenzelm@30056:   also have "(x\<inverse>)\<inverse> \<circ> \<dots> = 1" by (rule left_inv)
wenzelm@30056:   finally show "x \<circ> x\<inverse> = 1" .
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30056: theorem right_unit: "x \<circ> 1 = x"
wenzelm@30056: proof -
wenzelm@30056:   have "1 = x\<inverse> \<circ> x" by (rule left_inv [symmetric])
wenzelm@30056:   also have "x \<circ> \<dots> = (x \<circ> x\<inverse>) \<circ> x" by (rule assoc [symmetric])
wenzelm@30056:   also have "x \<circ> x\<inverse> = 1" by (rule right_inv)
wenzelm@30056:   also have "\<dots> \<circ> x = x" by (rule left_unit)
wenzelm@30056:   finally show "x \<circ> 1 = x" .
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30058:   \noindent Reasoning from basic axioms is often tedious.  Our proofs
wenzelm@30058:   work by producing various instances of the given rules (potentially
wenzelm@30058:   the symmetric form) using the pattern ``@{command have}~@{text
wenzelm@30056:   eq}~@{command "by"}~@{text "(rule r)"}'' and composing the chain of
wenzelm@30056:   results via @{command also}/@{command finally}.  These steps may
wenzelm@30056:   involve any of the transitivity rules declared in
wenzelm@30056:   \secref{sec:framework-ex-equal}, namely @{thm trans} in combining
wenzelm@30056:   the first two results in @{thm right_inv} and in the final steps of
wenzelm@30056:   both proofs, @{thm forw_subst} in the first combination of @{thm
wenzelm@30056:   right_unit}, and @{thm back_subst} in all other calculational steps.
wenzelm@30056: 
wenzelm@30056:   Occasional substitutions in calculations are adequate, but should
wenzelm@30056:   not be over-emphasized.  The other extreme is to compose a chain by
wenzelm@30056:   plain transitivity only, with replacements occurring always in
wenzelm@30056:   topmost position. For example:
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: (*<*)
wenzelm@30056: theorem "\<And>A. PROP A \<Longrightarrow> PROP A"
wenzelm@30056: proof -
wenzelm@30056:   assume [symmetric, defn]: "\<And>x y. (x \<equiv> y) \<equiv> Trueprop (x = y)"
wenzelm@30056: (*>*)
wenzelm@30056:   have "x \<circ> 1 = x \<circ> (x\<inverse> \<circ> x)" unfolding left_inv ..
wenzelm@30056:   also have "\<dots> = (x \<circ> x\<inverse>) \<circ> x" unfolding assoc ..
wenzelm@30056:   also have "\<dots> = 1 \<circ> x" unfolding right_inv ..
wenzelm@30056:   also have "\<dots> = x" unfolding left_unit ..
wenzelm@30056:   finally have "x \<circ> 1 = x" .
wenzelm@30056: (*<*)
wenzelm@30056: qed
wenzelm@30056: (*>*)
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30056:   \noindent Here we have re-used the built-in mechanism for unfolding
wenzelm@30056:   definitions in order to normalize each equational problem.  A more
wenzelm@30056:   realistic object-logic would include proper setup for the Simplifier
wenzelm@30056:   (\secref{sec:simplifier}), the main automated tool for equational
wenzelm@30058:   reasoning in Isabelle.  Then ``@{command unfolding}~@{thm
wenzelm@30056:   left_inv}~@{command ".."}'' would become ``@{command "by"}~@{text
wenzelm@30061:   "(simp only: left_inv)"}'' etc.
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: end
wenzelm@30056: 
wenzelm@30056: 
wenzelm@30060: subsection {* Propositional logic \label{sec:framework-ex-prop} *}
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30056:   We axiomatize basic connectives of propositional logic: implication,
wenzelm@30056:   disjunction, and conjunction.  The associated rules are modeled
wenzelm@30058:   after Gentzen's system of Natural Deduction \cite{Gentzen:1935}.
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: axiomatization
wenzelm@30056:   imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25) where
wenzelm@30056:   impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
wenzelm@30056:   impD [dest]: "(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B"
wenzelm@30056: 
wenzelm@30056: axiomatization
wenzelm@30056:   disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30) where
wenzelm@30056:   disjI\<^isub>1 [intro]: "A \<Longrightarrow> A \<or> B" and
wenzelm@30060:   disjI\<^isub>2 [intro]: "B \<Longrightarrow> A \<or> B" and
wenzelm@30060:   disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@30056: 
wenzelm@30056: axiomatization
wenzelm@30056:   conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35) where
wenzelm@30056:   conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and
wenzelm@30060:   conjD\<^isub>1: "A \<and> B \<Longrightarrow> A" and
wenzelm@30060:   conjD\<^isub>2: "A \<and> B \<Longrightarrow> B"
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30056:   \noindent The conjunctive destructions have the disadvantage that
wenzelm@30056:   decomposing @{prop "A \<and> B"} involves an immediate decision which
wenzelm@30056:   component should be projected.  The more convenient simultaneous
wenzelm@30056:   elimination @{prop "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"} can be derived as
wenzelm@30056:   follows:
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: theorem conjE [elim]:
wenzelm@30056:   assumes "A \<and> B"
wenzelm@30056:   obtains A and B
wenzelm@30056: proof
wenzelm@30060:   from `A \<and> B` show A by (rule conjD\<^isub>1)
wenzelm@30060:   from `A \<and> B` show B by (rule conjD\<^isub>2)
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30056:   \noindent Here is an example of swapping conjuncts with a single
wenzelm@30056:   intermediate elimination step:
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: (*<*)
wenzelm@30056: lemma "\<And>A. PROP A \<Longrightarrow> PROP A"
wenzelm@30056: proof -
wenzelm@30056: (*>*)
wenzelm@30056:   assume "A \<and> B"
wenzelm@30056:   then obtain B and A ..
wenzelm@30056:   then have "B \<and> A" ..
wenzelm@30056: (*<*)
wenzelm@30056: qed
wenzelm@30056: (*>*)
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30058:   \noindent Note that the analogous elimination rule for disjunction
wenzelm@30058:   ``@{text "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with
wenzelm@30058:   the original axiomatization of @{thm disjE}.
wenzelm@30056: 
wenzelm@30056:   \medskip We continue propositional logic by introducing absurdity
wenzelm@30056:   with its characteristic elimination.  Plain truth may then be
wenzelm@30056:   defined as a proposition that is trivially true.
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: axiomatization
wenzelm@30056:   false :: o  ("\<bottom>") where
wenzelm@30056:   falseE [elim]: "\<bottom> \<Longrightarrow> A"
wenzelm@30056: 
wenzelm@30056: definition
wenzelm@30056:   true :: o  ("\<top>") where
wenzelm@30056:   "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
wenzelm@30056: 
wenzelm@30056: theorem trueI [intro]: \<top>
wenzelm@30056:   unfolding true_def ..
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30058:   \medskip\noindent Now negation represents an implication towards
wenzelm@30058:   absurdity:
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: definition
wenzelm@30056:   not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40) where
wenzelm@30056:   "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
wenzelm@30056: 
wenzelm@30056: theorem notI [intro]:
wenzelm@30056:   assumes "A \<Longrightarrow> \<bottom>"
wenzelm@30056:   shows "\<not> A"
wenzelm@30056: unfolding not_def
wenzelm@30056: proof
wenzelm@30056:   assume A
wenzelm@30056:   then show \<bottom> by (rule `A \<Longrightarrow> \<bottom>`)
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30056: theorem notE [elim]:
wenzelm@30056:   assumes "\<not> A" and A
wenzelm@30056:   shows B
wenzelm@30056: proof -
wenzelm@30056:   from `\<not> A` have "A \<longrightarrow> \<bottom>" unfolding not_def .
wenzelm@30056:   from `A \<longrightarrow> \<bottom>` and `A` have \<bottom> ..
wenzelm@30056:   then show B ..
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30056: 
wenzelm@30056: subsection {* Classical logic *}
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30056:   Subsequently we state the principle of classical contradiction as a
wenzelm@30056:   local assumption.  Thus we refrain from forcing the object-logic
wenzelm@30056:   into the classical perspective.  Within that context, we may derive
wenzelm@30056:   well-known consequences of the classical principle.
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: locale classical =
wenzelm@30056:   assumes classical: "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@30056: begin
wenzelm@30056: 
wenzelm@30056: theorem double_negation:
wenzelm@30056:   assumes "\<not> \<not> C"
wenzelm@30056:   shows C
wenzelm@30056: proof (rule classical)
wenzelm@30056:   assume "\<not> C"
wenzelm@30056:   with `\<not> \<not> C` show C ..
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30056: theorem tertium_non_datur: "C \<or> \<not> C"
wenzelm@30056: proof (rule double_negation)
wenzelm@30056:   show "\<not> \<not> (C \<or> \<not> C)"
wenzelm@30056:   proof
wenzelm@30056:     assume "\<not> (C \<or> \<not> C)"
wenzelm@30056:     have "\<not> C"
wenzelm@30056:     proof
wenzelm@30056:       assume C then have "C \<or> \<not> C" ..
wenzelm@30056:       with `\<not> (C \<or> \<not> C)` show \<bottom> ..
wenzelm@30056:     qed
wenzelm@30056:     then have "C \<or> \<not> C" ..
wenzelm@30056:     with `\<not> (C \<or> \<not> C)` show \<bottom> ..
wenzelm@30056:   qed
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30061:   \noindent These examples illustrate both classical reasoning and
wenzelm@30061:   non-trivial propositional proofs in general.  All three rules
wenzelm@30061:   characterize classical logic independently, but the original rule is
wenzelm@30061:   already the most convenient to use, because it leaves the conclusion
wenzelm@30061:   unchanged.  Note that @{prop "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"} fits again into our
wenzelm@30061:   format for eliminations, despite the additional twist that the
wenzelm@30061:   context refers to the main conclusion.  So we may write @{thm
wenzelm@30061:   classical} as the Isar statement ``@{text "\<OBTAINS> \<not> thesis"}''.
wenzelm@30061:   This also explains nicely how classical reasoning really works:
wenzelm@30061:   whatever the main @{text thesis} might be, we may always assume its
wenzelm@30061:   negation!
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: end
wenzelm@30056: 
wenzelm@30056: 
wenzelm@30060: subsection {* Quantifiers \label{sec:framework-ex-quant} *}
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30056:   Representing quantifiers is easy, thanks to the higher-order nature
wenzelm@30056:   of the underlying framework.  According to the well-known technique
wenzelm@30056:   introduced by Church \cite{church40}, quantifiers are operators on
wenzelm@30056:   predicates, which are syntactically represented as @{text "\<lambda>"}-terms
wenzelm@30058:   of type @{typ "i \<Rightarrow> o"}.  Binder notation turns @{text "All (\<lambda>x. B
wenzelm@30058:   x)"} into @{text "\<forall>x. B x"} etc.
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: axiomatization
wenzelm@30056:   All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10) where
wenzelm@30056:   allI [intro]: "(\<And>x. B x) \<Longrightarrow> \<forall>x. B x" and
wenzelm@30056:   allD [dest]: "(\<forall>x. B x) \<Longrightarrow> B a"
wenzelm@30056: 
wenzelm@30056: axiomatization
wenzelm@30056:   Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10) where
wenzelm@30056:   exI [intro]: "B a \<Longrightarrow> (\<exists>x. B x)" and
wenzelm@30056:   exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@30056: 
wenzelm@30056: text {*
wenzelm@30061:   \noindent The statement of @{thm exE} corresponds to ``@{text
wenzelm@30061:   "\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x"}'' in Isar.  In the
wenzelm@30061:   subsequent example we illustrate quantifier reasoning involving all
wenzelm@30061:   four rules:
wenzelm@30056: *}
wenzelm@30056: 
wenzelm@30056: theorem
wenzelm@30056:   assumes "\<exists>x. \<forall>y. R x y"
wenzelm@30056:   shows "\<forall>y. \<exists>x. R x y"
wenzelm@30056: proof    -- {* @{text "\<forall>"} introduction *}
wenzelm@30056:   obtain x where "\<forall>y. R x y" using `\<exists>x. \<forall>y. R x y` ..    -- {* @{text "\<exists>"} elimination *}
wenzelm@30056:   fix y have "R x y" using `\<forall>y. R x y` ..    -- {* @{text "\<forall>"} destruction *}
wenzelm@30056:   then show "\<exists>x. R x y" ..    -- {* @{text "\<exists>"} introduction *}
wenzelm@30056: qed
wenzelm@30056: 
wenzelm@30060: 
wenzelm@30060: subsection {* Canonical reasoning patterns *}
wenzelm@30060: 
wenzelm@30060: text {*
wenzelm@30060:   The main rules of first-order predicate logic from
wenzelm@30060:   \secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant}
wenzelm@30060:   can now be summarized as follows, using the native Isar statement
wenzelm@30060:   format of \secref{sec:framework-stmt}.
wenzelm@30060: 
wenzelm@30060:   \medskip
wenzelm@30060:   \begin{tabular}{l}
wenzelm@30060:   @{text "impI: \<ASSUMES> A \<Longrightarrow> B \<SHOWS> A \<longrightarrow> B"} \\
wenzelm@30060:   @{text "impD: \<ASSUMES> A \<longrightarrow> B \<AND> A \<SHOWS> B"} \\[1ex]
wenzelm@30060: 
wenzelm@30060:   @{text "disjI\<^isub>1: \<ASSUMES> A \<SHOWS> A \<or> B"} \\
wenzelm@30060:   @{text "disjI\<^isub>2: \<ASSUMES> B \<SHOWS> A \<or> B"} \\
wenzelm@30060:   @{text "disjE: \<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"} \\[1ex]
wenzelm@30060: 
wenzelm@30060:   @{text "conjI: \<ASSUMES> A \<AND> B \<SHOWS> A \<and> B"} \\
wenzelm@30060:   @{text "conjE: \<ASSUMES> A \<and> B \<OBTAINS> A \<AND> B"} \\[1ex]
wenzelm@30060: 
wenzelm@30060:   @{text "falseE: \<ASSUMES> \<bottom> \<SHOWS> A"} \\
wenzelm@30060:   @{text "trueI: \<SHOWS> \<top>"} \\[1ex]
wenzelm@30060: 
wenzelm@30060:   @{text "notI: \<ASSUMES> A \<Longrightarrow> \<bottom> \<SHOWS> \<not> A"} \\
wenzelm@30060:   @{text "notE: \<ASSUMES> \<not> A \<AND> A \<SHOWS> B"} \\[1ex]
wenzelm@30060: 
wenzelm@30060:   @{text "allI: \<ASSUMES> \<And>x. B x \<SHOWS> \<forall>x. B x"} \\
wenzelm@30060:   @{text "allE: \<ASSUMES> \<forall>x. B x \<SHOWS> B a"} \\[1ex]
wenzelm@30060: 
wenzelm@30060:   @{text "exI: \<ASSUMES> B a \<SHOWS> \<exists>x. B x"} \\
wenzelm@30060:   @{text "exE: \<ASSUMES> \<exists>x. B x \<OBTAINS> a \<WHERE> B a"}
wenzelm@30060:   \end{tabular}
wenzelm@30060:   \medskip
wenzelm@30060: 
wenzelm@30060:   \noindent This essentially provides a declarative reading of Pure
wenzelm@30060:   rules as Isar reasoning patterns: the rule statements tells how a
wenzelm@30060:   canonical proof outline shall look like.  Since the above rules have
wenzelm@30061:   already been declared as @{attribute (Pure) intro}, @{attribute
wenzelm@30061:   (Pure) elim}, @{attribute (Pure) dest} --- each according to its
wenzelm@30061:   particular shape --- we can immediately write Isar proof texts as
wenzelm@30061:   follows:
wenzelm@30060: *}
wenzelm@30060: 
wenzelm@30060: (*<*)
wenzelm@30060: theorem "\<And>A. PROP A \<Longrightarrow> PROP A"
wenzelm@30060: proof -
wenzelm@30060: (*>*)
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "A \<longrightarrow> B"
wenzelm@30060:   proof
wenzelm@30060:     assume A
wenzelm@30060:     show B sorry %noproof
wenzelm@30060:   qed
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "A \<longrightarrow> B" and A sorry %noproof
wenzelm@30060:   then have B ..
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have A sorry %noproof
wenzelm@30060:   then have "A \<or> B" ..
wenzelm@30060: 
wenzelm@30060:   have B sorry %noproof
wenzelm@30060:   then have "A \<or> B" ..
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "A \<or> B" sorry %noproof
wenzelm@30060:   then have C
wenzelm@30060:   proof
wenzelm@30060:     assume A
wenzelm@30060:     then show C sorry %noproof
wenzelm@30060:   next
wenzelm@30060:     assume B
wenzelm@30060:     then show C sorry %noproof
wenzelm@30060:   qed
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have A and B sorry %noproof
wenzelm@30060:   then have "A \<and> B" ..
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "A \<and> B" sorry %noproof
wenzelm@30060:   then obtain A and B ..
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "\<bottom>" sorry %noproof
wenzelm@30060:   then have A ..
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "\<top>" ..
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "\<not> A"
wenzelm@30060:   proof
wenzelm@30060:     assume A
wenzelm@30060:     then show "\<bottom>" sorry %noproof
wenzelm@30060:   qed
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "\<not> A" and A sorry %noproof
wenzelm@30060:   then have B ..
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "\<forall>x. B x"
wenzelm@30060:   proof
wenzelm@30060:     fix x
wenzelm@30060:     show "B x" sorry %noproof
wenzelm@30060:   qed
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "\<forall>x. B x" sorry %noproof
wenzelm@30060:   then have "B a" ..
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "\<exists>x. B x"
wenzelm@30060:   proof
wenzelm@30060:     show "B a" sorry %noproof
wenzelm@30060:   qed
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}*}(*<*)next(*>*)
wenzelm@30060: 
wenzelm@30060:   have "\<exists>x. B x" sorry %noproof
wenzelm@30060:   then obtain a where "B a" ..
wenzelm@30060: 
wenzelm@30060:   txt_raw {*\end{minipage}*}
wenzelm@30060: 
wenzelm@30060: (*<*)
wenzelm@30060: qed
wenzelm@30060: (*>*)
wenzelm@30060: 
wenzelm@30060: text {*
wenzelm@30060:   \bigskip\noindent Of course, these proofs are merely examples.  As
wenzelm@30060:   sketched in \secref{sec:framework-subproof}, there is a fair amount
wenzelm@30060:   of flexibility in expressing Pure deductions in Isar.  Here the user
wenzelm@30060:   is asked to express himself adequately, aiming at proof texts of
wenzelm@30060:   literary quality.
wenzelm@30060: *}
wenzelm@30060: 
wenzelm@30056: end %visible