misc tuning and modernization;
authorwenzelm
Mon Nov 30 19:12:08 2015 +0100 (2015-11-30)
changeset 6175949353865e539
parent 61758 df6258b7e53f
child 61760 1647bb489522
child 61764 ac6e5de1a50b
misc tuning and modernization;
src/HOL/ex/Higher_Order_Logic.thy
     1.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Mon Nov 30 15:23:02 2015 +0100
     1.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Mon Nov 30 19:12:08 2015 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  (*  Title:      HOL/ex/Higher_Order_Logic.thy
     1.5 -    Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
     1.6 +    Author:     Makarius
     1.7  *)
     1.8  
     1.9  section \<open>Foundations of HOL\<close>
    1.10 @@ -9,12 +9,11 @@
    1.11  begin
    1.12  
    1.13  text \<open>
    1.14 -  The following theory development demonstrates Higher-Order Logic
    1.15 -  itself, represented directly within the Pure framework of Isabelle.
    1.16 -  The ``HOL'' logic given here is essentially that of Gordon
    1.17 -  @{cite "Gordon:1985:HOL"}, although we prefer to present basic concepts
    1.18 -  in a slightly more conventional manner oriented towards plain
    1.19 -  Natural Deduction.
    1.20 +  The following theory development demonstrates Higher-Order Logic itself,
    1.21 +  represented directly within the Pure framework of Isabelle. The ``HOL''
    1.22 +  logic given here is essentially that of Gordon @{cite "Gordon:1985:HOL"},
    1.23 +  although we prefer to present basic concepts in a slightly more conventional
    1.24 +  manner oriented towards plain Natural Deduction.
    1.25  \<close>
    1.26  
    1.27  
    1.28 @@ -30,35 +29,31 @@
    1.29  
    1.30  subsubsection \<open>Basic logical connectives\<close>
    1.31  
    1.32 -judgment Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
    1.33 +judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
    1.34  
    1.35 -axiomatization
    1.36 -  imp :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longrightarrow>" 25) and
    1.37 -  All :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<forall>" 10)
    1.38 -where
    1.39 -  impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
    1.40 -  impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and
    1.41 -  allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
    1.42 -  allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
    1.43 +axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
    1.44 +  where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
    1.45 +    and impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
    1.46 +
    1.47 +axiomatization All :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
    1.48 +  where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
    1.49 +    and allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
    1.50  
    1.51  
    1.52  subsubsection \<open>Extensional equality\<close>
    1.53  
    1.54 -axiomatization
    1.55 -  equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infixl "=" 50)
    1.56 -where
    1.57 -  refl [intro]: "x = x" and
    1.58 -  subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
    1.59 +axiomatization equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "=" 50)
    1.60 +  where refl [intro]: "x = x"
    1.61 +    and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
    1.62  
    1.63 -axiomatization where
    1.64 -  ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" and
    1.65 -  iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
    1.66 +axiomatization
    1.67 +  where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
    1.68 +    and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
    1.69  
    1.70 -theorem sym [sym]: "x = y \<Longrightarrow> y = x"
    1.71 -proof -
    1.72 -  assume "x = y"
    1.73 -  then show "y = x" by (rule subst) (rule refl)
    1.74 -qed
    1.75 +theorem sym [sym]:
    1.76 +  assumes "x = y"
    1.77 +  shows "y = x"
    1.78 +  using assms by (rule subst) (rule refl)
    1.79  
    1.80  lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
    1.81    by (rule subst) (rule sym)
    1.82 @@ -80,173 +75,187 @@
    1.83  
    1.84  definition false :: o  ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
    1.85  
    1.86 +theorem falseE [elim]:
    1.87 +  assumes "\<bottom>"
    1.88 +  shows A
    1.89 +proof -
    1.90 +  from \<open>\<bottom>\<close> have "\<forall>A. A" unfolding false_def .
    1.91 +  then show A ..
    1.92 +qed
    1.93 +
    1.94 +
    1.95  definition true :: o  ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
    1.96  
    1.97 +theorem trueI [intro]: \<top>
    1.98 +  unfolding true_def ..
    1.99 +
   1.100 +
   1.101  definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
   1.102    where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
   1.103  
   1.104 -definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
   1.105 -  where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   1.106 -
   1.107 -definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
   1.108 -  where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   1.109 -
   1.110 -definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
   1.111 -  where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   1.112 -
   1.113  abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50)
   1.114    where "x \<noteq> y \<equiv> \<not> (x = y)"
   1.115  
   1.116 -theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
   1.117 -proof (unfold false_def)
   1.118 -  assume "\<forall>A. A"
   1.119 -  then show A ..
   1.120 -qed
   1.121 -
   1.122 -theorem trueI [intro]: \<top>
   1.123 -proof (unfold true_def)
   1.124 -  show "\<bottom> \<longrightarrow> \<bottom>" ..
   1.125 -qed
   1.126 +theorem notI [intro]:
   1.127 +  assumes "A \<Longrightarrow> \<bottom>"
   1.128 +  shows "\<not> A"
   1.129 +  using assms unfolding not_def ..
   1.130  
   1.131 -theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
   1.132 -proof (unfold not_def)
   1.133 -  assume "A \<Longrightarrow> \<bottom>"
   1.134 -  then show "A \<longrightarrow> \<bottom>" ..
   1.135 -qed
   1.136 -
   1.137 -theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
   1.138 -proof (unfold not_def)
   1.139 -  assume "A \<longrightarrow> \<bottom>" and A
   1.140 -  then have \<bottom> ..
   1.141 +theorem notE [elim]:
   1.142 +  assumes "\<not> A" and A
   1.143 +  shows B
   1.144 +proof -
   1.145 +  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def .
   1.146 +  from this and \<open>A\<close> have "\<bottom>" ..
   1.147    then show B ..
   1.148  qed
   1.149  
   1.150  lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
   1.151    by (rule notE)
   1.152  
   1.153 -lemmas contradiction = notE notE'  -- \<open>proof by contradiction in any order\<close>
   1.154 +lemmas contradiction = notE notE'  \<comment> \<open>proof by contradiction in any order\<close>
   1.155 +
   1.156 +
   1.157 +definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
   1.158 +  where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   1.159  
   1.160 -theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
   1.161 -proof (unfold conj_def)
   1.162 -  assume A and B
   1.163 -  show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   1.164 +theorem conjI [intro]:
   1.165 +  assumes A and B
   1.166 +  shows "A \<and> B"
   1.167 +  unfolding conj_def
   1.168 +proof
   1.169 +  fix C
   1.170 +  show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   1.171    proof
   1.172 -    fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   1.173 -    proof
   1.174 -      assume "A \<longrightarrow> B \<longrightarrow> C"
   1.175 -      also note \<open>A\<close>
   1.176 -      also note \<open>B\<close>
   1.177 -      finally show C .
   1.178 -    qed
   1.179 +    assume "A \<longrightarrow> B \<longrightarrow> C"
   1.180 +    also note \<open>A\<close>
   1.181 +    also note \<open>B\<close>
   1.182 +    finally show C .
   1.183    qed
   1.184  qed
   1.185  
   1.186 -theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
   1.187 -proof (unfold conj_def)
   1.188 -  assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   1.189 -  assume "A \<Longrightarrow> B \<Longrightarrow> C"
   1.190 -  moreover {
   1.191 -    from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..
   1.192 +theorem conjE [elim]:
   1.193 +  assumes "A \<and> B"
   1.194 +  obtains A and B
   1.195 +proof
   1.196 +  from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C
   1.197 +    unfolding conj_def ..
   1.198 +  show A
   1.199 +  proof -
   1.200 +    note * [of A]
   1.201      also have "A \<longrightarrow> B \<longrightarrow> A"
   1.202      proof
   1.203        assume A
   1.204        then show "B \<longrightarrow> A" ..
   1.205      qed
   1.206 -    finally have A .
   1.207 -  } moreover {
   1.208 -    from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..
   1.209 +    finally show ?thesis .
   1.210 +  qed
   1.211 +  show B
   1.212 +  proof -
   1.213 +    note * [of B]
   1.214      also have "A \<longrightarrow> B \<longrightarrow> B"
   1.215      proof
   1.216        show "B \<longrightarrow> B" ..
   1.217      qed
   1.218 -    finally have B .
   1.219 -  } ultimately show C .
   1.220 -qed
   1.221 -
   1.222 -theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
   1.223 -proof (unfold disj_def)
   1.224 -  assume A
   1.225 -  show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   1.226 -  proof
   1.227 -    fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   1.228 -    proof
   1.229 -      assume "A \<longrightarrow> C"
   1.230 -      also note \<open>A\<close>
   1.231 -      finally have C .
   1.232 -      then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
   1.233 -    qed
   1.234 +    finally show ?thesis .
   1.235    qed
   1.236  qed
   1.237  
   1.238 -theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
   1.239 -proof (unfold disj_def)
   1.240 -  assume B
   1.241 -  show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   1.242 +
   1.243 +definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
   1.244 +  where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   1.245 +
   1.246 +theorem disjI1 [intro]:
   1.247 +  assumes A
   1.248 +  shows "A \<or> B"
   1.249 +  unfolding disj_def
   1.250 +proof
   1.251 +  fix C
   1.252 +  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   1.253    proof
   1.254 -    fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   1.255 +    assume "A \<longrightarrow> C"
   1.256 +    from this and \<open>A\<close> have C ..
   1.257 +    then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
   1.258 +  qed
   1.259 +qed
   1.260 +
   1.261 +theorem disjI2 [intro]:
   1.262 +  assumes B
   1.263 +  shows "A \<or> B"
   1.264 +  unfolding disj_def
   1.265 +proof
   1.266 +  fix C
   1.267 +  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   1.268 +  proof
   1.269 +    show "(B \<longrightarrow> C) \<longrightarrow> C"
   1.270      proof
   1.271 -      show "(B \<longrightarrow> C) \<longrightarrow> C"
   1.272 -      proof
   1.273 -        assume "B \<longrightarrow> C"
   1.274 -        also note \<open>B\<close>
   1.275 -        finally show C .
   1.276 -      qed
   1.277 +      assume "B \<longrightarrow> C"
   1.278 +      from this and \<open>B\<close> show C ..
   1.279      qed
   1.280    qed
   1.281  qed
   1.282  
   1.283 -theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
   1.284 -proof (unfold disj_def)
   1.285 -  assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   1.286 -  assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"
   1.287 -  from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
   1.288 -  also have "A \<longrightarrow> C"
   1.289 +theorem disjE [elim]:
   1.290 +  assumes "A \<or> B"
   1.291 +  obtains (a) A | (b) B
   1.292 +proof -
   1.293 +  from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis"
   1.294 +    unfolding disj_def ..
   1.295 +  also have "A \<longrightarrow> thesis"
   1.296    proof
   1.297      assume A
   1.298 -    then show C by (rule r1)
   1.299 +    then show thesis by (rule a)
   1.300    qed
   1.301 -  also have "B \<longrightarrow> C"
   1.302 +  also have "B \<longrightarrow> thesis"
   1.303    proof
   1.304      assume B
   1.305 -    then show C by (rule r2)
   1.306 +    then show thesis by (rule b)
   1.307    qed
   1.308 -  finally show C .
   1.309 +  finally show thesis .
   1.310  qed
   1.311  
   1.312 +
   1.313 +definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
   1.314 +  where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   1.315 +
   1.316  theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
   1.317 -proof (unfold Ex_def)
   1.318 +  unfolding Ex_def
   1.319 +proof
   1.320 +  fix C
   1.321    assume "P a"
   1.322 -  show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   1.323 +  show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   1.324    proof
   1.325 -    fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   1.326 -    proof
   1.327 -      assume "\<forall>x. P x \<longrightarrow> C"
   1.328 -      then have "P a \<longrightarrow> C" ..
   1.329 -      also note \<open>P a\<close>
   1.330 -      finally show C .
   1.331 -    qed
   1.332 +    assume "\<forall>x. P x \<longrightarrow> C"
   1.333 +    then have "P a \<longrightarrow> C" ..
   1.334 +    from this and \<open>P a\<close> show C ..
   1.335    qed
   1.336  qed
   1.337  
   1.338 -theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
   1.339 -proof (unfold Ex_def)
   1.340 -  assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   1.341 -  assume r: "\<And>x. P x \<Longrightarrow> C"
   1.342 -  from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" ..
   1.343 -  also have "\<forall>x. P x \<longrightarrow> C"
   1.344 +theorem exE [elim]:
   1.345 +  assumes "\<exists>x. P x"
   1.346 +  obtains (that) x where "P x"
   1.347 +proof -
   1.348 +  from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis"
   1.349 +    unfolding Ex_def ..
   1.350 +  also have "\<forall>x. P x \<longrightarrow> thesis"
   1.351    proof
   1.352 -    fix x show "P x \<longrightarrow> C"
   1.353 +    fix x
   1.354 +    show "P x \<longrightarrow> thesis"
   1.355      proof
   1.356        assume "P x"
   1.357 -      then show C by (rule r)
   1.358 +      then show thesis by (rule that)
   1.359      qed
   1.360    qed
   1.361 -  finally show C .
   1.362 +  finally show thesis .
   1.363  qed
   1.364  
   1.365  
   1.366  subsection \<open>Classical logic\<close>
   1.367  
   1.368 +text \<open>
   1.369 +  The subsequent rules of classical reasoning are all equivalent.
   1.370 +\<close>
   1.371 +
   1.372  locale classical =
   1.373    assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
   1.374  
   1.375 @@ -265,14 +274,12 @@
   1.376    qed
   1.377  qed
   1.378  
   1.379 -theorem (in classical) double_negation: "\<not> \<not> A \<Longrightarrow> A"
   1.380 -proof -
   1.381 -  assume "\<not> \<not> A"
   1.382 -  show A
   1.383 -  proof (rule classical)
   1.384 -    assume "\<not> A"
   1.385 -    with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
   1.386 -  qed
   1.387 +theorem (in classical) double_negation:
   1.388 +  assumes "\<not> \<not> A"
   1.389 +  shows A
   1.390 +proof (rule classical)
   1.391 +  assume "\<not> A"
   1.392 +  with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
   1.393  qed
   1.394  
   1.395  theorem (in classical) tertium_non_datur: "A \<or> \<not> A"
   1.396 @@ -290,27 +297,30 @@
   1.397    qed
   1.398  qed
   1.399  
   1.400 -theorem (in classical) classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
   1.401 -proof -
   1.402 -  assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
   1.403 -  from tertium_non_datur show C
   1.404 -  proof
   1.405 +theorem (in classical) classical_cases:
   1.406 +  obtains A | "\<not> A"
   1.407 +  using tertium_non_datur
   1.408 +proof
   1.409 +  assume A
   1.410 +  then show thesis ..
   1.411 +next
   1.412 +  assume "\<not> A"
   1.413 +  then show thesis ..
   1.414 +qed
   1.415 +
   1.416 +lemma
   1.417 +  assumes classical_cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
   1.418 +  shows "PROP classical"
   1.419 +proof
   1.420 +  fix A
   1.421 +  assume *: "\<not> A \<Longrightarrow> A"
   1.422 +  show A
   1.423 +  proof (rule classical_cases)
   1.424      assume A
   1.425 -    then show ?thesis by (rule r1)
   1.426 +    then show A .
   1.427    next
   1.428      assume "\<not> A"
   1.429 -    then show ?thesis by (rule r2)
   1.430 -  qed
   1.431 -qed
   1.432 -
   1.433 -lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"  (* FIXME *)
   1.434 -proof -
   1.435 -  assume r: "\<not> A \<Longrightarrow> A"
   1.436 -  show A
   1.437 -  proof (rule classical_cases)
   1.438 -    assume A then show A .
   1.439 -  next
   1.440 -    assume "\<not> A" then show A by (rule r)
   1.441 +    then show A by (rule *)
   1.442    qed
   1.443  qed
   1.444