
wenzelm@12360: (*  Title:      HOL/ex/Higher_Order_Logic.thy
wenzelm@12360:     Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
wenzelm@12360: *)
wenzelm@12360: 
wenzelm@12360: header {* Foundations of HOL *}
wenzelm@12360: 
wenzelm@26957: theory Higher_Order_Logic imports Pure begin
wenzelm@12360: 
wenzelm@12360: text {*
wenzelm@12360:   The following theory development demonstrates Higher-Order Logic
wenzelm@12360:   itself, represented directly within the Pure framework of Isabelle.
wenzelm@12360:   The ``HOL'' logic given here is essentially that of Gordon
wenzelm@12360:   \cite{Gordon:1985:HOL}, although we prefer to present basic concepts
wenzelm@12360:   in a slightly more conventional manner oriented towards plain
wenzelm@12360:   Natural Deduction.
wenzelm@12360: *}
wenzelm@12360: 
wenzelm@12360: 
wenzelm@12360: subsection {* Pure Logic *}
wenzelm@12360: 
wenzelm@14854: classes type
wenzelm@36452: default_sort type
wenzelm@12360: 
wenzelm@12360: typedecl o
wenzelm@12360: arities
wenzelm@12360:   o :: type
krauss@20523:   "fun" :: (type, type) type
wenzelm@12360: 
wenzelm@12360: 
wenzelm@12360: subsubsection {* Basic logical connectives *}
wenzelm@12360: 
wenzelm@12360: judgment
wenzelm@12360:   Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
wenzelm@12360: 
wenzelm@23822: axiomatization
wenzelm@23822:   imp :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longrightarrow>" 25) and
wenzelm@12360:   All :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<forall>" 10)
wenzelm@23822: where
wenzelm@23822:   impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
wenzelm@23822:   impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and
wenzelm@23822:   allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
wenzelm@12360:   allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
wenzelm@12360: 
wenzelm@12360: 
wenzelm@12360: subsubsection {* Extensional equality *}
wenzelm@12360: 
wenzelm@23822: axiomatization
wenzelm@12360:   equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infixl "=" 50)
wenzelm@23822: where
wenzelm@23822:   refl [intro]: "x = x" and
wenzelm@23822:   subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
wenzelm@12360: 
wenzelm@23822: axiomatization where
wenzelm@23822:   ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" and
wenzelm@12360:   iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
wenzelm@12360: 
wenzelm@12394: theorem sym [sym]: "x = y \<Longrightarrow> y = x"
wenzelm@12360: proof -
wenzelm@12360:   assume "x = y"
wenzelm@23373:   then show "y = x" by (rule subst) (rule refl)
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
wenzelm@12360:   by (rule subst) (rule sym)
wenzelm@12360: 
wenzelm@12360: lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y"
wenzelm@12360:   by (rule subst)
wenzelm@12360: 
wenzelm@12360: theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
wenzelm@12360:   by (rule subst)
wenzelm@12360: 
wenzelm@12360: theorem iff1 [elim]: "A = B \<Longrightarrow> A \<Longrightarrow> B"
wenzelm@12360:   by (rule subst)
wenzelm@12360: 
wenzelm@12360: theorem iff2 [elim]: "A = B \<Longrightarrow> B \<Longrightarrow> A"
wenzelm@12360:   by (rule subst) (rule sym)
wenzelm@12360: 
wenzelm@12360: 
wenzelm@12360: subsubsection {* Derived connectives *}
wenzelm@12360: 
wenzelm@19736: definition
wenzelm@21404:   false :: o  ("\<bottom>") where
wenzelm@12360:   "\<bottom> \<equiv> \<forall>A. A"
wenzelm@21404: 
wenzelm@21404: definition
wenzelm@21404:   true :: o  ("\<top>") where
wenzelm@12360:   "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
wenzelm@21404: 
wenzelm@21404: definition
wenzelm@21404:   not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40) where
wenzelm@12360:   "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
wenzelm@21404: 
wenzelm@21404: definition
wenzelm@21404:   conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35) where
wenzelm@12360:   "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@21404: 
wenzelm@21404: definition
wenzelm@21404:   disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30) where
wenzelm@12360:   "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@21404: 
wenzelm@21404: definition
wenzelm@21404:   Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10) where
wenzelm@23822:   "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360: 
wenzelm@19380: abbreviation
wenzelm@21404:   not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50) where
wenzelm@19380:   "x \<noteq> y \<equiv> \<not> (x = y)"
wenzelm@12360: 
wenzelm@12360: theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
wenzelm@12360: proof (unfold false_def)
wenzelm@12360:   assume "\<forall>A. A"
wenzelm@23373:   then show A ..
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem trueI [intro]: \<top>
wenzelm@12360: proof (unfold true_def)
wenzelm@12360:   show "\<bottom> \<longrightarrow> \<bottom>" ..
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
wenzelm@12360: proof (unfold not_def)
wenzelm@12360:   assume "A \<Longrightarrow> \<bottom>"
wenzelm@23373:   then show "A \<longrightarrow> \<bottom>" ..
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
wenzelm@12360: proof (unfold not_def)
wenzelm@12360:   assume "A \<longrightarrow> \<bottom>"
wenzelm@12360:   also assume A
wenzelm@12360:   finally have \<bottom> ..
wenzelm@23373:   then show B ..
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
wenzelm@12360:   by (rule notE)
wenzelm@12360: 
wenzelm@12360: lemmas contradiction = notE notE'  -- {* proof by contradiction in any order *}
wenzelm@12360: 
wenzelm@12360: theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
wenzelm@12360: proof (unfold conj_def)
wenzelm@12360:   assume A and B
wenzelm@12360:   show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:   proof
wenzelm@12360:     fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:     proof
wenzelm@12360:       assume "A \<longrightarrow> B \<longrightarrow> C"
wenzelm@23373:       also note `A`
wenzelm@23373:       also note `B`
wenzelm@12360:       finally show C .
wenzelm@12360:     qed
wenzelm@12360:   qed
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@12360: proof (unfold conj_def)
wenzelm@12360:   assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:   assume "A \<Longrightarrow> B \<Longrightarrow> C"
wenzelm@12360:   moreover {
wenzelm@12360:     from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..
wenzelm@12360:     also have "A \<longrightarrow> B \<longrightarrow> A"
wenzelm@12360:     proof
wenzelm@12360:       assume A
wenzelm@23373:       then show "B \<longrightarrow> A" ..
wenzelm@12360:     qed
wenzelm@12360:     finally have A .
wenzelm@12360:   } moreover {
wenzelm@12360:     from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..
wenzelm@12360:     also have "A \<longrightarrow> B \<longrightarrow> B"
wenzelm@12360:     proof
wenzelm@12360:       show "B \<longrightarrow> B" ..
wenzelm@12360:     qed
wenzelm@12360:     finally have B .
wenzelm@12360:   } ultimately show C .
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
wenzelm@12360: proof (unfold disj_def)
wenzelm@12360:   assume A
wenzelm@12360:   show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:   proof
wenzelm@12360:     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:     proof
wenzelm@12360:       assume "A \<longrightarrow> C"
wenzelm@23373:       also note `A`
wenzelm@12360:       finally have C .
wenzelm@23373:       then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
wenzelm@12360:     qed
wenzelm@12360:   qed
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
wenzelm@12360: proof (unfold disj_def)
wenzelm@12360:   assume B
wenzelm@12360:   show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:   proof
wenzelm@12360:     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:     proof
wenzelm@12360:       show "(B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:       proof
wenzelm@12360:         assume "B \<longrightarrow> C"
wenzelm@23373:         also note `B`
wenzelm@12360:         finally show C .
wenzelm@12360:       qed
wenzelm@12360:     qed
wenzelm@12360:   qed
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@12360: proof (unfold disj_def)
wenzelm@12360:   assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:   assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"
wenzelm@12360:   from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
wenzelm@12360:   also have "A \<longrightarrow> C"
wenzelm@12360:   proof
wenzelm@23373:     assume A then show C by (rule r1)
wenzelm@12360:   qed
wenzelm@12360:   also have "B \<longrightarrow> C"
wenzelm@12360:   proof
wenzelm@23373:     assume B then show C by (rule r2)
wenzelm@12360:   qed
wenzelm@12360:   finally show C .
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
wenzelm@12360: proof (unfold Ex_def)
wenzelm@12360:   assume "P a"
wenzelm@12360:   show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:   proof
wenzelm@12360:     fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:     proof
wenzelm@12360:       assume "\<forall>x. P x \<longrightarrow> C"
wenzelm@23373:       then have "P a \<longrightarrow> C" ..
wenzelm@23373:       also note `P a`
wenzelm@12360:       finally show C .
wenzelm@12360:     qed
wenzelm@12360:   qed
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@12360: proof (unfold Ex_def)
wenzelm@12360:   assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360:   assume r: "\<And>x. P x \<Longrightarrow> C"
wenzelm@12360:   from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" ..
wenzelm@12360:   also have "\<forall>x. P x \<longrightarrow> C"
wenzelm@12360:   proof
wenzelm@12360:     fix x show "P x \<longrightarrow> C"
wenzelm@12360:     proof
wenzelm@12360:       assume "P x"
wenzelm@23373:       then show C by (rule r)
wenzelm@12360:     qed
wenzelm@12360:   qed
wenzelm@12360:   finally show C .
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: 
wenzelm@12360: subsection {* Classical logic *}
wenzelm@12360: 
wenzelm@12360: locale classical =
wenzelm@12360:   assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
wenzelm@12360: 
wenzelm@12360: theorem (in classical)
wenzelm@12360:   Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
wenzelm@12360: proof
wenzelm@12360:   assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
wenzelm@12360:   show A
wenzelm@12360:   proof (rule classical)
wenzelm@12360:     assume "\<not> A"
wenzelm@12360:     have "A \<longrightarrow> B"
wenzelm@12360:     proof
wenzelm@12360:       assume A
wenzelm@23373:       with `\<not> A` show B by (rule contradiction)
wenzelm@12360:     qed
wenzelm@12360:     with a show A ..
wenzelm@12360:   qed
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem (in classical)
wenzelm@12360:   double_negation: "\<not> \<not> A \<Longrightarrow> A"
wenzelm@12360: proof -
wenzelm@12360:   assume "\<not> \<not> A"
wenzelm@12360:   show A
wenzelm@12360:   proof (rule classical)
wenzelm@12360:     assume "\<not> A"
wenzelm@23373:     with `\<not> \<not> A` show ?thesis by (rule contradiction)
wenzelm@12360:   qed
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem (in classical)
wenzelm@12360:   tertium_non_datur: "A \<or> \<not> A"
wenzelm@12360: proof (rule double_negation)
wenzelm@12360:   show "\<not> \<not> (A \<or> \<not> A)"
wenzelm@12360:   proof
wenzelm@12360:     assume "\<not> (A \<or> \<not> A)"
wenzelm@12360:     have "\<not> A"
wenzelm@12360:     proof
wenzelm@23373:       assume A then have "A \<or> \<not> A" ..
wenzelm@23373:       with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
wenzelm@12360:     qed
wenzelm@23373:     then have "A \<or> \<not> A" ..
wenzelm@23373:     with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
wenzelm@12360:   qed
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12360: theorem (in classical)
wenzelm@12360:   classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@12360: proof -
wenzelm@12360:   assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
wenzelm@12360:   from tertium_non_datur show C
wenzelm@12360:   proof
wenzelm@12360:     assume A
wenzelm@23373:     then show ?thesis by (rule r1)
wenzelm@12360:   next
wenzelm@12360:     assume "\<not> A"
wenzelm@23373:     then show ?thesis by (rule r2)
wenzelm@12360:   qed
wenzelm@12360: qed
wenzelm@12360: 
wenzelm@12573: lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"  (* FIXME *)
wenzelm@12573: proof -
wenzelm@12573:   assume r: "\<not> A \<Longrightarrow> A"
wenzelm@12573:   show A
wenzelm@12573:   proof (rule classical_cases)
wenzelm@23373:     assume A then show A .
wenzelm@12573:   next
wenzelm@23373:     assume "\<not> A" then show A by (rule r)
wenzelm@12573:   qed
wenzelm@12573: qed
wenzelm@12573: 
wenzelm@12360: end




