12360

1 
(* Title: HOL/ex/Higher_Order_Logic.thy


2 
ID: $Id$


3 
Author: Gertrud Bauer and Markus Wenzel, TU Muenchen


4 
*)


5 


6 
header {* Foundations of HOL *}


7 

16417

8 
theory Higher_Order_Logic imports CPure begin

12360

9 


10 
text {*


11 
The following theory development demonstrates HigherOrder Logic


12 
itself, represented directly within the Pure framework of Isabelle.


13 
The ``HOL'' logic given here is essentially that of Gordon


14 
\cite{Gordon:1985:HOL}, although we prefer to present basic concepts


15 
in a slightly more conventional manner oriented towards plain


16 
Natural Deduction.


17 
*}


18 


19 


20 
subsection {* Pure Logic *}


21 

14854

22 
classes type

12360

23 
defaultsort type


24 


25 
typedecl o


26 
arities


27 
o :: type


28 
fun :: (type, type) type


29 


30 


31 
subsubsection {* Basic logical connectives *}


32 


33 
judgment


34 
Trueprop :: "o \<Rightarrow> prop" ("_" 5)


35 


36 
consts


37 
imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25)


38 
All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10)


39 


40 
axioms


41 
impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"


42 
impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"


43 
allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"


44 
allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"


45 


46 


47 
subsubsection {* Extensional equality *}


48 


49 
consts


50 
equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "=" 50)


51 


52 
axioms


53 
refl [intro]: "x = x"


54 
subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"


55 
ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"


56 
iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"


57 

12394

58 
theorem sym [sym]: "x = y \<Longrightarrow> y = x"

12360

59 
proof 


60 
assume "x = y"


61 
thus "y = x" by (rule subst) (rule refl)


62 
qed


63 


64 
lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"


65 
by (rule subst) (rule sym)


66 


67 
lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y"


68 
by (rule subst)


69 


70 
theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"


71 
by (rule subst)


72 


73 
theorem iff1 [elim]: "A = B \<Longrightarrow> A \<Longrightarrow> B"


74 
by (rule subst)


75 


76 
theorem iff2 [elim]: "A = B \<Longrightarrow> B \<Longrightarrow> A"


77 
by (rule subst) (rule sym)


78 


79 


80 
subsubsection {* Derived connectives *}


81 

19736

82 
definition

12360

83 
false :: o ("\<bottom>")


84 
"\<bottom> \<equiv> \<forall>A. A"


85 
true :: o ("\<top>")


86 
"\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"


87 
not :: "o \<Rightarrow> o" ("\<not> _" [40] 40)


88 
"not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"


89 
conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35)


90 
"conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"


91 
disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30)


92 
"disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"


93 
Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)


94 
"Ex \<equiv> \<lambda>P. \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"


95 

19380

96 
abbreviation


97 
not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50)


98 
"x \<noteq> y \<equiv> \<not> (x = y)"

12360

99 


100 
theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"


101 
proof (unfold false_def)


102 
assume "\<forall>A. A"


103 
thus A ..


104 
qed


105 


106 
theorem trueI [intro]: \<top>


107 
proof (unfold true_def)


108 
show "\<bottom> \<longrightarrow> \<bottom>" ..


109 
qed


110 


111 
theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"


112 
proof (unfold not_def)


113 
assume "A \<Longrightarrow> \<bottom>"


114 
thus "A \<longrightarrow> \<bottom>" ..


115 
qed


116 


117 
theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"


118 
proof (unfold not_def)


119 
assume "A \<longrightarrow> \<bottom>"


120 
also assume A


121 
finally have \<bottom> ..


122 
thus B ..


123 
qed


124 


125 
lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"


126 
by (rule notE)


127 


128 
lemmas contradiction = notE notE'  {* proof by contradiction in any order *}


129 


130 
theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"


131 
proof (unfold conj_def)


132 
assume A and B


133 
show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"


134 
proof


135 
fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"


136 
proof


137 
assume "A \<longrightarrow> B \<longrightarrow> C"


138 
also have A .


139 
also have B .


140 
finally show C .


141 
qed


142 
qed


143 
qed


144 


145 
theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"


146 
proof (unfold conj_def)


147 
assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"


148 
assume "A \<Longrightarrow> B \<Longrightarrow> C"


149 
moreover {


150 
from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..


151 
also have "A \<longrightarrow> B \<longrightarrow> A"


152 
proof


153 
assume A


154 
thus "B \<longrightarrow> A" ..


155 
qed


156 
finally have A .


157 
} moreover {


158 
from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..


159 
also have "A \<longrightarrow> B \<longrightarrow> B"


160 
proof


161 
show "B \<longrightarrow> B" ..


162 
qed


163 
finally have B .


164 
} ultimately show C .


165 
qed


166 


167 
theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"


168 
proof (unfold disj_def)


169 
assume A


170 
show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"


171 
proof


172 
fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"


173 
proof


174 
assume "A \<longrightarrow> C"


175 
also have A .


176 
finally have C .


177 
thus "(B \<longrightarrow> C) \<longrightarrow> C" ..


178 
qed


179 
qed


180 
qed


181 


182 
theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"


183 
proof (unfold disj_def)


184 
assume B


185 
show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"


186 
proof


187 
fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"


188 
proof


189 
show "(B \<longrightarrow> C) \<longrightarrow> C"


190 
proof


191 
assume "B \<longrightarrow> C"


192 
also have B .


193 
finally show C .


194 
qed


195 
qed


196 
qed


197 
qed


198 


199 
theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"


200 
proof (unfold disj_def)


201 
assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"


202 
assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"


203 
from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..


204 
also have "A \<longrightarrow> C"


205 
proof


206 
assume A thus C by (rule r1)


207 
qed


208 
also have "B \<longrightarrow> C"


209 
proof


210 
assume B thus C by (rule r2)


211 
qed


212 
finally show C .


213 
qed


214 


215 
theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"


216 
proof (unfold Ex_def)


217 
assume "P a"


218 
show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"


219 
proof


220 
fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"


221 
proof


222 
assume "\<forall>x. P x \<longrightarrow> C"


223 
hence "P a \<longrightarrow> C" ..


224 
also have "P a" .


225 
finally show C .


226 
qed


227 
qed


228 
qed


229 


230 
theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"


231 
proof (unfold Ex_def)


232 
assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"


233 
assume r: "\<And>x. P x \<Longrightarrow> C"


234 
from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" ..


235 
also have "\<forall>x. P x \<longrightarrow> C"


236 
proof


237 
fix x show "P x \<longrightarrow> C"


238 
proof


239 
assume "P x"


240 
thus C by (rule r)


241 
qed


242 
qed


243 
finally show C .


244 
qed


245 


246 


247 
subsection {* Classical logic *}


248 


249 
locale classical =


250 
assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"


251 


252 
theorem (in classical)


253 
Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"


254 
proof


255 
assume a: "(A \<longrightarrow> B) \<longrightarrow> A"


256 
show A


257 
proof (rule classical)


258 
assume "\<not> A"


259 
have "A \<longrightarrow> B"


260 
proof


261 
assume A


262 
thus B by (rule contradiction)


263 
qed


264 
with a show A ..


265 
qed


266 
qed


267 


268 
theorem (in classical)


269 
double_negation: "\<not> \<not> A \<Longrightarrow> A"


270 
proof 


271 
assume "\<not> \<not> A"


272 
show A


273 
proof (rule classical)


274 
assume "\<not> A"


275 
thus ?thesis by (rule contradiction)


276 
qed


277 
qed


278 


279 
theorem (in classical)


280 
tertium_non_datur: "A \<or> \<not> A"


281 
proof (rule double_negation)


282 
show "\<not> \<not> (A \<or> \<not> A)"


283 
proof


284 
assume "\<not> (A \<or> \<not> A)"


285 
have "\<not> A"


286 
proof


287 
assume A hence "A \<or> \<not> A" ..


288 
thus \<bottom> by (rule contradiction)


289 
qed


290 
hence "A \<or> \<not> A" ..


291 
thus \<bottom> by (rule contradiction)


292 
qed


293 
qed


294 


295 
theorem (in classical)


296 
classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"


297 
proof 


298 
assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"


299 
from tertium_non_datur show C


300 
proof


301 
assume A


302 
thus ?thesis by (rule r1)


303 
next


304 
assume "\<not> A"


305 
thus ?thesis by (rule r2)


306 
qed


307 
qed


308 

12573

309 
lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A" (* FIXME *)


310 
proof 


311 
assume r: "\<not> A \<Longrightarrow> A"


312 
show A


313 
proof (rule classical_cases)


314 
assume A thus A .


315 
next


316 
assume "\<not> A" thus A by (rule r)


317 
qed


318 
qed


319 

12360

320 
end
