tuned proofs;
authorwenzelm
Thu Jul 23 14:20:51 2015 +0200 (2015-07-23)
changeset 60769cf7f3465eaf1
parent 60768 f47bd91fdc75
child 60770 240563fbf41d
tuned proofs;
src/FOL/ex/First_Order_Logic.thy
src/HOL/ex/Higher_Order_Logic.thy
     1.1 --- a/src/FOL/ex/First_Order_Logic.thy	Thu Jul 23 13:28:34 2015 +0200
     1.2 +++ b/src/FOL/ex/First_Order_Logic.thy	Thu Jul 23 14:20:51 2015 +0200
     1.3 @@ -51,17 +51,14 @@
     1.4    from `A \<and> B` show B by (rule conjD2)
     1.5  qed
     1.6  
     1.7 -definition
     1.8 -  true :: o  ("\<top>") where
     1.9 -  "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
    1.10 +definition true :: o  ("\<top>")
    1.11 +  where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
    1.12  
    1.13 -definition
    1.14 -  not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40) where
    1.15 -  "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
    1.16 +definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
    1.17 +  where "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
    1.18  
    1.19 -definition
    1.20 -  iff :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longleftrightarrow>" 25) where
    1.21 -  "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
    1.22 +definition iff :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longleftrightarrow>" 25)
    1.23 +  where "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
    1.24  
    1.25  
    1.26  theorem trueI [intro]: \<top>
    1.27 @@ -78,7 +75,8 @@
    1.28  theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
    1.29  proof (unfold not_def)
    1.30    assume "A \<longrightarrow> \<bottom>" and A
    1.31 -  then have \<bottom> .. then show B ..
    1.32 +  then have \<bottom> ..
    1.33 +  then show B ..
    1.34  qed
    1.35  
    1.36  theorem iffI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B"
     2.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Thu Jul 23 13:28:34 2015 +0200
     2.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Thu Jul 23 14:20:51 2015 +0200
     2.3 @@ -4,7 +4,9 @@
     2.4  
     2.5  section \<open>Foundations of HOL\<close>
     2.6  
     2.7 -theory Higher_Order_Logic imports Pure begin
     2.8 +theory Higher_Order_Logic
     2.9 +imports Pure
    2.10 +begin
    2.11  
    2.12  text \<open>
    2.13    The following theory development demonstrates Higher-Order Logic
    2.14 @@ -28,8 +30,7 @@
    2.15  
    2.16  subsubsection \<open>Basic logical connectives\<close>
    2.17  
    2.18 -judgment
    2.19 -  Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
    2.20 +judgment Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
    2.21  
    2.22  axiomatization
    2.23    imp :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longrightarrow>" 25) and
    2.24 @@ -115,9 +116,8 @@
    2.25  
    2.26  theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
    2.27  proof (unfold not_def)
    2.28 -  assume "A \<longrightarrow> \<bottom>"
    2.29 -  also assume A
    2.30 -  finally have \<bottom> ..
    2.31 +  assume "A \<longrightarrow> \<bottom>" and A
    2.32 +  then have \<bottom> ..
    2.33    then show B ..
    2.34  qed
    2.35  
    2.36 @@ -202,11 +202,13 @@
    2.37    from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
    2.38    also have "A \<longrightarrow> C"
    2.39    proof
    2.40 -    assume A then show C by (rule r1)
    2.41 +    assume A
    2.42 +    then show C by (rule r1)
    2.43    qed
    2.44    also have "B \<longrightarrow> C"
    2.45    proof
    2.46 -    assume B then show C by (rule r2)
    2.47 +    assume B
    2.48 +    then show C by (rule r2)
    2.49    qed
    2.50    finally show C .
    2.51  qed
    2.52 @@ -248,8 +250,7 @@
    2.53  locale classical =
    2.54    assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
    2.55  
    2.56 -theorem (in classical)
    2.57 -  Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
    2.58 +theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
    2.59  proof
    2.60    assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
    2.61    show A
    2.62 @@ -264,8 +265,7 @@
    2.63    qed
    2.64  qed
    2.65  
    2.66 -theorem (in classical)
    2.67 -  double_negation: "\<not> \<not> A \<Longrightarrow> A"
    2.68 +theorem (in classical) double_negation: "\<not> \<not> A \<Longrightarrow> A"
    2.69  proof -
    2.70    assume "\<not> \<not> A"
    2.71    show A
    2.72 @@ -275,8 +275,7 @@
    2.73    qed
    2.74  qed
    2.75  
    2.76 -theorem (in classical)
    2.77 -  tertium_non_datur: "A \<or> \<not> A"
    2.78 +theorem (in classical) tertium_non_datur: "A \<or> \<not> A"
    2.79  proof (rule double_negation)
    2.80    show "\<not> \<not> (A \<or> \<not> A)"
    2.81    proof
    2.82 @@ -291,8 +290,7 @@
    2.83    qed
    2.84  qed
    2.85  
    2.86 -theorem (in classical)
    2.87 -  classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
    2.88 +theorem (in classical) classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
    2.89  proof -
    2.90    assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
    2.91    from tertium_non_datur show C