# HG changeset patch
# User wenzelm
# Date 1448907128 -3600
# Node ID 49353865e5395827a6b0d6d38509abd9bf3204ef
# Parent  df6258b7e53f262d4ab83c3a0d15b682114c64b2
misc tuning and modernization;

diff -r df6258b7e53f -r 49353865e539 src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Mon Nov 30 15:23:02 2015 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Mon Nov 30 19:12:08 2015 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/ex/Higher_Order_Logic.thy
-    Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
+    Author:     Makarius
 *)
 
 section \<open>Foundations of HOL\<close>
@@ -9,12 +9,11 @@
 begin
 
 text \<open>
-  The following theory development demonstrates Higher-Order Logic
-  itself, represented directly within the Pure framework of Isabelle.
-  The ``HOL'' logic given here is essentially that of Gordon
-  @{cite "Gordon:1985:HOL"}, although we prefer to present basic concepts
-  in a slightly more conventional manner oriented towards plain
-  Natural Deduction.
+  The following theory development demonstrates Higher-Order Logic itself,
+  represented directly within the Pure framework of Isabelle. The ``HOL''
+  logic given here is essentially that of Gordon @{cite "Gordon:1985:HOL"},
+  although we prefer to present basic concepts in a slightly more conventional
+  manner oriented towards plain Natural Deduction.
 \<close>
 
 
@@ -30,35 +29,31 @@
 
 subsubsection \<open>Basic logical connectives\<close>
 
-judgment Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
+judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
 
-axiomatization
-  imp :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longrightarrow>" 25) and
-  All :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<forall>" 10)
-where
-  impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
-  impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and
-  allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
-  allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
+axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
+  where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
+    and impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
+
+axiomatization All :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
+  where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
+    and allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
 
 
 subsubsection \<open>Extensional equality\<close>
 
-axiomatization
-  equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infixl "=" 50)
-where
-  refl [intro]: "x = x" and
-  subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
+axiomatization equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "=" 50)
+  where refl [intro]: "x = x"
+    and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
 
-axiomatization where
-  ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" and
-  iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
+axiomatization
+  where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
+    and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
 
-theorem sym [sym]: "x = y \<Longrightarrow> y = x"
-proof -
-  assume "x = y"
-  then show "y = x" by (rule subst) (rule refl)
-qed
+theorem sym [sym]:
+  assumes "x = y"
+  shows "y = x"
+  using assms by (rule subst) (rule refl)
 
 lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
   by (rule subst) (rule sym)
@@ -80,173 +75,187 @@
 
 definition false :: o  ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
 
+theorem falseE [elim]:
+  assumes "\<bottom>"
+  shows A
+proof -
+  from \<open>\<bottom>\<close> have "\<forall>A. A" unfolding false_def .
+  then show A ..
+qed
+
+
 definition true :: o  ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
 
+theorem trueI [intro]: \<top>
+  unfolding true_def ..
+
+
 definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
   where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
 
-definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
-  where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
-
-definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
-  where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-
-definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
-  where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
-
 abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50)
   where "x \<noteq> y \<equiv> \<not> (x = y)"
 
-theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
-proof (unfold false_def)
-  assume "\<forall>A. A"
-  then show A ..
-qed
-
-theorem trueI [intro]: \<top>
-proof (unfold true_def)
-  show "\<bottom> \<longrightarrow> \<bottom>" ..
-qed
+theorem notI [intro]:
+  assumes "A \<Longrightarrow> \<bottom>"
+  shows "\<not> A"
+  using assms unfolding not_def ..
 
-theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
-proof (unfold not_def)
-  assume "A \<Longrightarrow> \<bottom>"
-  then show "A \<longrightarrow> \<bottom>" ..
-qed
-
-theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
-proof (unfold not_def)
-  assume "A \<longrightarrow> \<bottom>" and A
-  then have \<bottom> ..
+theorem notE [elim]:
+  assumes "\<not> A" and A
+  shows B
+proof -
+  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def .
+  from this and \<open>A\<close> have "\<bottom>" ..
   then show B ..
 qed
 
 lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
   by (rule notE)
 
-lemmas contradiction = notE notE'  -- \<open>proof by contradiction in any order\<close>
+lemmas contradiction = notE notE'  \<comment> \<open>proof by contradiction in any order\<close>
+
+
+definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
+  where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
 
-theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
-proof (unfold conj_def)
-  assume A and B
-  show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
+theorem conjI [intro]:
+  assumes A and B
+  shows "A \<and> B"
+  unfolding conj_def
+proof
+  fix C
+  show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   proof
-    fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
-    proof
-      assume "A \<longrightarrow> B \<longrightarrow> C"
-      also note \<open>A\<close>
-      also note \<open>B\<close>
-      finally show C .
-    qed
+    assume "A \<longrightarrow> B \<longrightarrow> C"
+    also note \<open>A\<close>
+    also note \<open>B\<close>
+    finally show C .
   qed
 qed
 
-theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
-proof (unfold conj_def)
-  assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
-  assume "A \<Longrightarrow> B \<Longrightarrow> C"
-  moreover {
-    from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..
+theorem conjE [elim]:
+  assumes "A \<and> B"
+  obtains A and B
+proof
+  from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C
+    unfolding conj_def ..
+  show A
+  proof -
+    note * [of A]
     also have "A \<longrightarrow> B \<longrightarrow> A"
     proof
       assume A
       then show "B \<longrightarrow> A" ..
     qed
-    finally have A .
-  } moreover {
-    from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..
+    finally show ?thesis .
+  qed
+  show B
+  proof -
+    note * [of B]
     also have "A \<longrightarrow> B \<longrightarrow> B"
     proof
       show "B \<longrightarrow> B" ..
     qed
-    finally have B .
-  } ultimately show C .
-qed
-
-theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
-proof (unfold disj_def)
-  assume A
-  show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-  proof
-    fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-    proof
-      assume "A \<longrightarrow> C"
-      also note \<open>A\<close>
-      finally have C .
-      then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
-    qed
+    finally show ?thesis .
   qed
 qed
 
-theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
-proof (unfold disj_def)
-  assume B
-  show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+
+definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
+  where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+
+theorem disjI1 [intro]:
+  assumes A
+  shows "A \<or> B"
+  unfolding disj_def
+proof
+  fix C
+  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   proof
-    fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+    assume "A \<longrightarrow> C"
+    from this and \<open>A\<close> have C ..
+    then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
+  qed
+qed
+
+theorem disjI2 [intro]:
+  assumes B
+  shows "A \<or> B"
+  unfolding disj_def
+proof
+  fix C
+  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+  proof
+    show "(B \<longrightarrow> C) \<longrightarrow> C"
     proof
-      show "(B \<longrightarrow> C) \<longrightarrow> C"
-      proof
-        assume "B \<longrightarrow> C"
-        also note \<open>B\<close>
-        finally show C .
-      qed
+      assume "B \<longrightarrow> C"
+      from this and \<open>B\<close> show C ..
     qed
   qed
 qed
 
-theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
-proof (unfold disj_def)
-  assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-  assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"
-  from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
-  also have "A \<longrightarrow> C"
+theorem disjE [elim]:
+  assumes "A \<or> B"
+  obtains (a) A | (b) B
+proof -
+  from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis"
+    unfolding disj_def ..
+  also have "A \<longrightarrow> thesis"
   proof
     assume A
-    then show C by (rule r1)
+    then show thesis by (rule a)
   qed
-  also have "B \<longrightarrow> C"
+  also have "B \<longrightarrow> thesis"
   proof
     assume B
-    then show C by (rule r2)
+    then show thesis by (rule b)
   qed
-  finally show C .
+  finally show thesis .
 qed
 
+
+definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
+  where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+
 theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
-proof (unfold Ex_def)
+  unfolding Ex_def
+proof
+  fix C
   assume "P a"
-  show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+  show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   proof
-    fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
-    proof
-      assume "\<forall>x. P x \<longrightarrow> C"
-      then have "P a \<longrightarrow> C" ..
-      also note \<open>P a\<close>
-      finally show C .
-    qed
+    assume "\<forall>x. P x \<longrightarrow> C"
+    then have "P a \<longrightarrow> C" ..
+    from this and \<open>P a\<close> show C ..
   qed
 qed
 
-theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
-proof (unfold Ex_def)
-  assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
-  assume r: "\<And>x. P x \<Longrightarrow> C"
-  from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" ..
-  also have "\<forall>x. P x \<longrightarrow> C"
+theorem exE [elim]:
+  assumes "\<exists>x. P x"
+  obtains (that) x where "P x"
+proof -
+  from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis"
+    unfolding Ex_def ..
+  also have "\<forall>x. P x \<longrightarrow> thesis"
   proof
-    fix x show "P x \<longrightarrow> C"
+    fix x
+    show "P x \<longrightarrow> thesis"
     proof
       assume "P x"
-      then show C by (rule r)
+      then show thesis by (rule that)
     qed
   qed
-  finally show C .
+  finally show thesis .
 qed
 
 
 subsection \<open>Classical logic\<close>
 
+text \<open>
+  The subsequent rules of classical reasoning are all equivalent.
+\<close>
+
 locale classical =
   assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
 
@@ -265,14 +274,12 @@
   qed
 qed
 
-theorem (in classical) double_negation: "\<not> \<not> A \<Longrightarrow> A"
-proof -
-  assume "\<not> \<not> A"
-  show A
-  proof (rule classical)
-    assume "\<not> A"
-    with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
-  qed
+theorem (in classical) double_negation:
+  assumes "\<not> \<not> A"
+  shows A
+proof (rule classical)
+  assume "\<not> A"
+  with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
 qed
 
 theorem (in classical) tertium_non_datur: "A \<or> \<not> A"
@@ -290,27 +297,30 @@
   qed
 qed
 
-theorem (in classical) classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
-proof -
-  assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
-  from tertium_non_datur show C
-  proof
+theorem (in classical) classical_cases:
+  obtains A | "\<not> A"
+  using tertium_non_datur
+proof
+  assume A
+  then show thesis ..
+next
+  assume "\<not> A"
+  then show thesis ..
+qed
+
+lemma
+  assumes classical_cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
+  shows "PROP classical"
+proof
+  fix A
+  assume *: "\<not> A \<Longrightarrow> A"
+  show A
+  proof (rule classical_cases)
     assume A
-    then show ?thesis by (rule r1)
+    then show A .
   next
     assume "\<not> A"
-    then show ?thesis by (rule r2)
-  qed
-qed
-
-lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"  (* FIXME *)
-proof -
-  assume r: "\<not> A \<Longrightarrow> A"
-  show A
-  proof (rule classical_cases)
-    assume A then show A .
-  next
-    assume "\<not> A" then show A by (rule r)
+    then show A by (rule *)
   qed
 qed