src/FOL/ex/First_Order_Logic.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 31974 e81979a703a4
child 60769 cf7f3465eaf1
permissions -rw-r--r--
modernized header uniformly as section;
wenzelm@12369
     1
(*  Title:      FOL/ex/First_Order_Logic.thy
wenzelm@12369
     2
    Author:     Markus Wenzel, TU Munich
wenzelm@12369
     3
*)
wenzelm@12369
     4
wenzelm@58889
     5
section {* A simple formulation of First-Order Logic *}
wenzelm@12369
     6
haftmann@16417
     7
theory First_Order_Logic imports Pure begin
wenzelm@12369
     8
wenzelm@12369
     9
text {*
wenzelm@12369
    10
  The subsequent theory development illustrates single-sorted
wenzelm@12369
    11
  intuitionistic first-order logic with equality, formulated within
wenzelm@12369
    12
  the Pure framework.  Actually this is not an example of
wenzelm@12369
    13
  Isabelle/FOL, but of Isabelle/Pure.
wenzelm@12369
    14
*}
wenzelm@12369
    15
wenzelm@12369
    16
subsection {* Syntax *}
wenzelm@12369
    17
wenzelm@12369
    18
typedecl i
wenzelm@12369
    19
typedecl o
wenzelm@12369
    20
wenzelm@12369
    21
judgment
wenzelm@12369
    22
  Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
wenzelm@12369
    23
wenzelm@12369
    24
wenzelm@12369
    25
subsection {* Propositional logic *}
wenzelm@12369
    26
wenzelm@21939
    27
axiomatization
wenzelm@21939
    28
  false :: o  ("\<bottom>") and
wenzelm@21939
    29
  imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25) and
wenzelm@21939
    30
  conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35) and
wenzelm@21939
    31
  disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
wenzelm@21939
    32
where
wenzelm@21939
    33
  falseE [elim]: "\<bottom> \<Longrightarrow> A" and
wenzelm@12369
    34
wenzelm@21939
    35
  impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
wenzelm@21939
    36
  mp [dest]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and
wenzelm@12369
    37
wenzelm@21939
    38
  conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and
wenzelm@21939
    39
  conjD1: "A \<and> B \<Longrightarrow> A" and
wenzelm@21939
    40
  conjD2: "A \<and> B \<Longrightarrow> B" and
wenzelm@12369
    41
wenzelm@21939
    42
  disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C" and
wenzelm@21939
    43
  disjI1 [intro]: "A \<Longrightarrow> A \<or> B" and
wenzelm@12369
    44
  disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
wenzelm@12369
    45
wenzelm@21939
    46
theorem conjE [elim]:
wenzelm@21939
    47
  assumes "A \<and> B"
wenzelm@21939
    48
  obtains A and B
wenzelm@21939
    49
proof
wenzelm@21939
    50
  from `A \<and> B` show A by (rule conjD1)
wenzelm@21939
    51
  from `A \<and> B` show B by (rule conjD2)
wenzelm@12369
    52
qed
wenzelm@12369
    53
wenzelm@21939
    54
definition
wenzelm@21939
    55
  true :: o  ("\<top>") where
wenzelm@12369
    56
  "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
wenzelm@21939
    57
wenzelm@21939
    58
definition
wenzelm@21939
    59
  not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40) where
wenzelm@12369
    60
  "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
wenzelm@21939
    61
wenzelm@21939
    62
definition
wenzelm@21939
    63
  iff :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longleftrightarrow>" 25) where
wenzelm@12392
    64
  "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
wenzelm@12392
    65
wenzelm@12369
    66
wenzelm@12369
    67
theorem trueI [intro]: \<top>
wenzelm@12369
    68
proof (unfold true_def)
wenzelm@12369
    69
  show "\<bottom> \<longrightarrow> \<bottom>" ..
wenzelm@12369
    70
qed
wenzelm@12369
    71
wenzelm@12369
    72
theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
wenzelm@12369
    73
proof (unfold not_def)
wenzelm@12369
    74
  assume "A \<Longrightarrow> \<bottom>"
wenzelm@21939
    75
  then show "A \<longrightarrow> \<bottom>" ..
wenzelm@12369
    76
qed
wenzelm@12369
    77
wenzelm@12369
    78
theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
wenzelm@12369
    79
proof (unfold not_def)
wenzelm@12369
    80
  assume "A \<longrightarrow> \<bottom>" and A
wenzelm@21939
    81
  then have \<bottom> .. then show B ..
wenzelm@12369
    82
qed
wenzelm@12369
    83
wenzelm@12392
    84
theorem iffI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B"
wenzelm@12392
    85
proof (unfold iff_def)
wenzelm@21939
    86
  assume "A \<Longrightarrow> B" then have "A \<longrightarrow> B" ..
wenzelm@21939
    87
  moreover assume "B \<Longrightarrow> A" then have "B \<longrightarrow> A" ..
wenzelm@12392
    88
  ultimately show "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)" ..
wenzelm@12392
    89
qed
wenzelm@12392
    90
wenzelm@12392
    91
theorem iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
wenzelm@12392
    92
proof (unfold iff_def)
wenzelm@12392
    93
  assume "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
wenzelm@21939
    94
  then have "A \<longrightarrow> B" ..
wenzelm@21939
    95
  then show "A \<Longrightarrow> B" ..
wenzelm@12392
    96
qed
wenzelm@12392
    97
wenzelm@12392
    98
theorem iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"
wenzelm@12392
    99
proof (unfold iff_def)
wenzelm@12392
   100
  assume "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
wenzelm@21939
   101
  then have "B \<longrightarrow> A" ..
wenzelm@21939
   102
  then show "B \<Longrightarrow> A" ..
wenzelm@12392
   103
qed
wenzelm@12392
   104
wenzelm@12369
   105
wenzelm@12369
   106
subsection {* Equality *}
wenzelm@12369
   107
wenzelm@21939
   108
axiomatization
wenzelm@21939
   109
  equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infixl "=" 50)
wenzelm@21939
   110
where
wenzelm@21939
   111
  refl [intro]: "x = x" and
wenzelm@26958
   112
  subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
wenzelm@12369
   113
wenzelm@12369
   114
theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
wenzelm@12369
   115
  by (rule subst)
wenzelm@12369
   116
wenzelm@12369
   117
theorem sym [sym]: "x = y \<Longrightarrow> y = x"
wenzelm@12369
   118
proof -
wenzelm@12369
   119
  assume "x = y"
wenzelm@12369
   120
  from this and refl show "y = x" by (rule subst)
wenzelm@12369
   121
qed
wenzelm@12369
   122
wenzelm@12369
   123
wenzelm@12369
   124
subsection {* Quantifiers *}
wenzelm@12369
   125
wenzelm@21939
   126
axiomatization
wenzelm@21939
   127
  All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10) and
wenzelm@21939
   128
  Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
wenzelm@21939
   129
where
wenzelm@26958
   130
  allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
wenzelm@26958
   131
  allD [dest]: "\<forall>x. P x \<Longrightarrow> P a" and
wenzelm@26958
   132
  exI [intro]: "P a \<Longrightarrow> \<exists>x. P x" and
wenzelm@26958
   133
  exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@12369
   134
wenzelm@12369
   135
wenzelm@26958
   136
lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
wenzelm@12369
   137
proof
wenzelm@26958
   138
  assume "\<exists>x. P (f x)"
wenzelm@26958
   139
  then show "\<exists>y. P y"
wenzelm@12369
   140
  proof
wenzelm@26958
   141
    fix x assume "P (f x)"
wenzelm@21939
   142
    then show ?thesis ..
wenzelm@12369
   143
  qed
wenzelm@12369
   144
qed
wenzelm@12369
   145
wenzelm@26958
   146
lemma "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
wenzelm@12369
   147
proof
wenzelm@26958
   148
  assume "\<exists>x. \<forall>y. R x y"
wenzelm@26958
   149
  then show "\<forall>y. \<exists>x. R x y"
wenzelm@12369
   150
  proof
wenzelm@26958
   151
    fix x assume a: "\<forall>y. R x y"
wenzelm@12369
   152
    show ?thesis
wenzelm@12369
   153
    proof
wenzelm@26958
   154
      fix y from a have "R x y" ..
wenzelm@26958
   155
      then show "\<exists>x. R x y" ..
wenzelm@12369
   156
    qed
wenzelm@12369
   157
  qed
wenzelm@12369
   158
qed
wenzelm@12369
   159
wenzelm@12369
   160
end