added Higher_Order_Logic.thy;
authorwenzelm
Tue Dec 04 17:59:36 2001 +0100 (2001-12-04)
changeset 123609c156045c8f2
parent 12359 86d3218a5410
child 12361 b7ca18198669
added Higher_Order_Logic.thy;
src/HOL/IsaMakefile
src/HOL/ex/Higher_Order_Logic.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/document/root.bib
     1.1 --- a/src/HOL/IsaMakefile	Tue Dec 04 14:26:22 2001 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Dec 04 17:59:36 2001 +0100
     1.3 @@ -528,7 +528,7 @@
     1.4  HOL-ex: HOL $(LOG)/HOL-ex.gz
     1.5  
     1.6  $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.ML ex/AVL.thy ex/Antiquote.thy \
     1.7 -  ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy \
     1.8 +  ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy ex/Higher_Order_Logic.thy \
     1.9    ex/Hilbert_Classical.thy ex/InSort.ML ex/InSort.thy ex/IntRing.ML \
    1.10    ex/IntRing.thy ex/Lagrange.ML ex/Lagrange.thy ex/Locales.thy \
    1.11    ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Tue Dec 04 17:59:36 2001 +0100
     2.3 @@ -0,0 +1,311 @@
     2.4 +(*  Title:      HOL/ex/Higher_Order_Logic.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
     2.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8 +*)
     2.9 +
    2.10 +header {* Foundations of HOL *}
    2.11 +
    2.12 +theory Higher_Order_Logic = CPure:
    2.13 +
    2.14 +text {*
    2.15 +  The following theory development demonstrates Higher-Order Logic
    2.16 +  itself, represented directly within the Pure framework of Isabelle.
    2.17 +  The ``HOL'' logic given here is essentially that of Gordon
    2.18 +  \cite{Gordon:1985:HOL}, although we prefer to present basic concepts
    2.19 +  in a slightly more conventional manner oriented towards plain
    2.20 +  Natural Deduction.
    2.21 +*}
    2.22 +
    2.23 +
    2.24 +subsection {* Pure Logic *}
    2.25 +
    2.26 +classes type \<subseteq> logic
    2.27 +defaultsort type
    2.28 +
    2.29 +typedecl o
    2.30 +arities
    2.31 +  o :: type
    2.32 +  fun :: (type, type) type
    2.33 +
    2.34 +
    2.35 +subsubsection {* Basic logical connectives *}
    2.36 +
    2.37 +judgment
    2.38 +  Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
    2.39 +
    2.40 +consts
    2.41 +  imp :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longrightarrow>" 25)
    2.42 +  All :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<forall>" 10)
    2.43 +
    2.44 +axioms
    2.45 +  impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
    2.46 +  impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
    2.47 +  allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
    2.48 +  allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
    2.49 +
    2.50 +
    2.51 +subsubsection {* Extensional equality *}
    2.52 +
    2.53 +consts
    2.54 +  equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infixl "=" 50)
    2.55 +
    2.56 +axioms
    2.57 +  refl [intro]: "x = x"
    2.58 +  subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
    2.59 +  ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
    2.60 +  iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
    2.61 +
    2.62 +theorem sym [elim]: "x = y \<Longrightarrow> y = x"
    2.63 +proof -
    2.64 +  assume "x = y"
    2.65 +  thus "y = x" by (rule subst) (rule refl)
    2.66 +qed
    2.67 +
    2.68 +lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
    2.69 +  by (rule subst) (rule sym)
    2.70 +
    2.71 +lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y"
    2.72 +  by (rule subst)
    2.73 +
    2.74 +theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
    2.75 +  by (rule subst)
    2.76 +
    2.77 +theorem iff1 [elim]: "A = B \<Longrightarrow> A \<Longrightarrow> B"
    2.78 +  by (rule subst)
    2.79 +
    2.80 +theorem iff2 [elim]: "A = B \<Longrightarrow> B \<Longrightarrow> A"
    2.81 +  by (rule subst) (rule sym)
    2.82 +
    2.83 +
    2.84 +subsubsection {* Derived connectives *}
    2.85 +
    2.86 +constdefs
    2.87 +  false :: o    ("\<bottom>")
    2.88 +  "\<bottom> \<equiv> \<forall>A. A"
    2.89 +  true :: o    ("\<top>")
    2.90 +  "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
    2.91 +  not :: "o \<Rightarrow> o"     ("\<not> _" [40] 40)
    2.92 +  "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
    2.93 +  conj :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<and>" 35)
    2.94 +  "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
    2.95 +  disj :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<or>" 30)
    2.96 +  "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
    2.97 +  Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<exists>" 10)
    2.98 +  "Ex \<equiv> \<lambda>P. \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
    2.99 +
   2.100 +syntax
   2.101 +  "_not_equal" :: "'a \<Rightarrow> 'a \<Rightarrow> o"    (infixl "\<noteq>" 50)
   2.102 +translations
   2.103 +  "x \<noteq> y"  \<rightleftharpoons>  "\<not> (x = y)"
   2.104 +
   2.105 +theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
   2.106 +proof (unfold false_def)
   2.107 +  assume "\<forall>A. A"
   2.108 +  thus A ..
   2.109 +qed
   2.110 +
   2.111 +theorem trueI [intro]: \<top>
   2.112 +proof (unfold true_def)
   2.113 +  show "\<bottom> \<longrightarrow> \<bottom>" ..
   2.114 +qed
   2.115 +
   2.116 +theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
   2.117 +proof (unfold not_def)
   2.118 +  assume "A \<Longrightarrow> \<bottom>"
   2.119 +  thus "A \<longrightarrow> \<bottom>" ..
   2.120 +qed
   2.121 +
   2.122 +theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
   2.123 +proof (unfold not_def)
   2.124 +  assume "A \<longrightarrow> \<bottom>"
   2.125 +  also assume A
   2.126 +  finally have \<bottom> ..
   2.127 +  thus B ..
   2.128 +qed
   2.129 +
   2.130 +lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
   2.131 +  by (rule notE)
   2.132 +
   2.133 +lemmas contradiction = notE notE'  -- {* proof by contradiction in any order *}
   2.134 +
   2.135 +theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
   2.136 +proof (unfold conj_def)
   2.137 +  assume A and B
   2.138 +  show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   2.139 +  proof
   2.140 +    fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   2.141 +    proof
   2.142 +      assume "A \<longrightarrow> B \<longrightarrow> C"
   2.143 +      also have A .
   2.144 +      also have B .
   2.145 +      finally show C .
   2.146 +    qed
   2.147 +  qed
   2.148 +qed
   2.149 +
   2.150 +theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
   2.151 +proof (unfold conj_def)
   2.152 +  assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   2.153 +  assume "A \<Longrightarrow> B \<Longrightarrow> C"
   2.154 +  moreover {
   2.155 +    from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..
   2.156 +    also have "A \<longrightarrow> B \<longrightarrow> A"
   2.157 +    proof
   2.158 +      assume A
   2.159 +      thus "B \<longrightarrow> A" ..
   2.160 +    qed
   2.161 +    finally have A .
   2.162 +  } moreover {
   2.163 +    from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..
   2.164 +    also have "A \<longrightarrow> B \<longrightarrow> B"
   2.165 +    proof
   2.166 +      show "B \<longrightarrow> B" ..
   2.167 +    qed
   2.168 +    finally have B .
   2.169 +  } ultimately show C .
   2.170 +qed
   2.171 +
   2.172 +theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
   2.173 +proof (unfold disj_def)
   2.174 +  assume A
   2.175 +  show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   2.176 +  proof
   2.177 +    fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   2.178 +    proof
   2.179 +      assume "A \<longrightarrow> C"
   2.180 +      also have A .
   2.181 +      finally have C .
   2.182 +      thus "(B \<longrightarrow> C) \<longrightarrow> C" ..
   2.183 +    qed
   2.184 +  qed
   2.185 +qed
   2.186 +
   2.187 +theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
   2.188 +proof (unfold disj_def)
   2.189 +  assume B
   2.190 +  show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   2.191 +  proof
   2.192 +    fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   2.193 +    proof
   2.194 +      show "(B \<longrightarrow> C) \<longrightarrow> C"
   2.195 +      proof
   2.196 +        assume "B \<longrightarrow> C"
   2.197 +        also have B .
   2.198 +        finally show C .
   2.199 +      qed
   2.200 +    qed
   2.201 +  qed
   2.202 +qed
   2.203 +
   2.204 +theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
   2.205 +proof (unfold disj_def)
   2.206 +  assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   2.207 +  assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"
   2.208 +  from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
   2.209 +  also have "A \<longrightarrow> C"
   2.210 +  proof
   2.211 +    assume A thus C by (rule r1)
   2.212 +  qed
   2.213 +  also have "B \<longrightarrow> C"
   2.214 +  proof
   2.215 +    assume B thus C by (rule r2)
   2.216 +  qed
   2.217 +  finally show C .
   2.218 +qed
   2.219 +
   2.220 +theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
   2.221 +proof (unfold Ex_def)
   2.222 +  assume "P a"
   2.223 +  show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   2.224 +  proof
   2.225 +    fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   2.226 +    proof
   2.227 +      assume "\<forall>x. P x \<longrightarrow> C"
   2.228 +      hence "P a \<longrightarrow> C" ..
   2.229 +      also have "P a" .
   2.230 +      finally show C .
   2.231 +    qed
   2.232 +  qed
   2.233 +qed
   2.234 +
   2.235 +theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
   2.236 +proof (unfold Ex_def)
   2.237 +  assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   2.238 +  assume r: "\<And>x. P x \<Longrightarrow> C"
   2.239 +  from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" ..
   2.240 +  also have "\<forall>x. P x \<longrightarrow> C"
   2.241 +  proof
   2.242 +    fix x show "P x \<longrightarrow> C"
   2.243 +    proof
   2.244 +      assume "P x"
   2.245 +      thus C by (rule r)
   2.246 +    qed
   2.247 +  qed
   2.248 +  finally show C .
   2.249 +qed
   2.250 +
   2.251 +
   2.252 +subsection {* Classical logic *}
   2.253 +
   2.254 +locale classical =
   2.255 +  assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
   2.256 +
   2.257 +theorem (in classical)
   2.258 +  Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
   2.259 +proof
   2.260 +  assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
   2.261 +  show A
   2.262 +  proof (rule classical)
   2.263 +    assume "\<not> A"
   2.264 +    have "A \<longrightarrow> B"
   2.265 +    proof
   2.266 +      assume A
   2.267 +      thus B by (rule contradiction)
   2.268 +    qed
   2.269 +    with a show A ..
   2.270 +  qed
   2.271 +qed
   2.272 +
   2.273 +theorem (in classical)
   2.274 +  double_negation: "\<not> \<not> A \<Longrightarrow> A"
   2.275 +proof -
   2.276 +  assume "\<not> \<not> A"
   2.277 +  show A
   2.278 +  proof (rule classical)
   2.279 +    assume "\<not> A"
   2.280 +    thus ?thesis by (rule contradiction)
   2.281 +  qed
   2.282 +qed
   2.283 +
   2.284 +theorem (in classical)
   2.285 +  tertium_non_datur: "A \<or> \<not> A"
   2.286 +proof (rule double_negation)
   2.287 +  show "\<not> \<not> (A \<or> \<not> A)"
   2.288 +  proof
   2.289 +    assume "\<not> (A \<or> \<not> A)"
   2.290 +    have "\<not> A"
   2.291 +    proof
   2.292 +      assume A hence "A \<or> \<not> A" ..
   2.293 +      thus \<bottom> by (rule contradiction)
   2.294 +    qed
   2.295 +    hence "A \<or> \<not> A" ..
   2.296 +    thus \<bottom> by (rule contradiction)
   2.297 +  qed
   2.298 +qed
   2.299 +
   2.300 +theorem (in classical)
   2.301 +  classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
   2.302 +proof -
   2.303 +  assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
   2.304 +  from tertium_non_datur show C
   2.305 +  proof
   2.306 +    assume A
   2.307 +    thus ?thesis by (rule r1)
   2.308 +  next
   2.309 +    assume "\<not> A"
   2.310 +    thus ?thesis by (rule r2)
   2.311 +  qed
   2.312 +qed
   2.313 +
   2.314 +end
     3.1 --- a/src/HOL/ex/ROOT.ML	Tue Dec 04 14:26:22 2001 +0100
     3.2 +++ b/src/HOL/ex/ROOT.ML	Tue Dec 04 17:59:36 2001 +0100
     3.3 @@ -4,6 +4,8 @@
     3.4  Miscellaneous examples for Higher-Order Logic.
     3.5  *)
     3.6  
     3.7 +time_use_thy "Higher_Order_Logic";
     3.8 +
     3.9  time_use_thy "Recdefs";
    3.10  time_use_thy "Primrec";
    3.11  time_use_thy "Locales";
     4.1 --- a/src/HOL/ex/document/root.bib	Tue Dec 04 14:26:22 2001 +0100
     4.2 +++ b/src/HOL/ex/document/root.bib	Tue Dec 04 17:59:36 2001 +0100
     4.3 @@ -1,3 +1,11 @@
     4.4 +
     4.5 +@TechReport{Gordon:1985:HOL,
     4.6 +  author =       {M. J. C. Gordon},
     4.7 +  title =        {{HOL}: A machine oriented formulation of higher order logic},
     4.8 +  institution =  {University of Cambridge Computer Laboratory},
     4.9 +  year =         1985,
    4.10 +  number =       68
    4.11 +}
    4.12  
    4.13  @InProceedings{Kamm-et-al:1999,
    4.14    author =       {Florian Kamm{\"u}ller and Markus Wenzel and