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