# HG changeset patch
# User wenzelm
# Date 1164317908 -3600
# Node ID 9c97af4a156721529dce01bbb97e84355f71f9b3
# Parent  c4ea7e8c39370179d551b4fdf8ec4e3bf0de6b47
tuned proofs;

diff -r c4ea7e8c3937 -r 9c97af4a1567 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Nov 23 22:14:26 2006 +0100
+++ b/src/HOL/HOL.thy	Thu Nov 23 22:38:28 2006 +0100
@@ -306,8 +306,8 @@
 
 subsubsection {*Equality of booleans -- iff*}
 
-lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q"
-  by (iprover intro: iff [THEN mp, THEN mp] impI prems)
+lemma iffI: assumes "P ==> Q" and "Q ==> P" shows "P=Q"
+  by (iprover intro: iff [THEN mp, THEN mp] impI assms)
 
 lemma iffD2: "[| P=Q; Q |] ==> P"
   by (erule ssubst)
@@ -315,12 +315,15 @@
 lemma rev_iffD2: "[| Q; P=Q |] ==> P"
   by (erule iffD2)
 
-lemmas iffD1 = sym [THEN iffD2, standard]
-lemmas rev_iffD1 = sym [THEN [2] rev_iffD2, standard]
+lemma iffD1: "Q = P \<Longrightarrow> Q \<Longrightarrow> P"
+  by (drule sym) (rule iffD2)
+
+lemma rev_iffD1: "Q \<Longrightarrow> Q = P \<Longrightarrow> P"
+  by (drule sym) (rule rev_iffD2)
 
 lemma iffE:
   assumes major: "P=Q"
-      and minor: "[| P --> Q; Q --> P |] ==> R"
+    and minor: "[| P --> Q; Q --> P |] ==> R"
   shows R
   by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
 
@@ -328,23 +331,19 @@
 subsubsection {*True*}
 
 lemma TrueI: "True"
-  by (unfold True_def) (rule refl)
+  unfolding True_def by (rule refl)
 
-lemma eqTrueI: "P ==> P=True"
+lemma eqTrueI: "P ==> P = True"
   by (iprover intro: iffI TrueI)
 
-lemma eqTrueE: "P=True ==> P"
-apply (erule iffD2)
-apply (rule TrueI)
-done
+lemma eqTrueE: "P = True ==> P"
+  by (erule iffD2) (rule TrueI)
 
 
 subsubsection {*Universal quantifier*}
 
-lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)"
-apply (unfold All_def)
-apply (iprover intro: ext eqTrueI p)
-done
+lemma allI: assumes "!!x::'a. P(x)" shows "ALL x. P(x)"
+  unfolding All_def by (iprover intro: ext eqTrueI assms)
 
 lemma spec: "ALL x::'a. P(x) ==> P(x)"
 apply (unfold All_def)
@@ -354,57 +353,61 @@
 
 lemma allE:
   assumes major: "ALL x. P(x)"
-      and minor: "P(x) ==> R"
-  shows "R"
-by (iprover intro: minor major [THEN spec])
+    and minor: "P(x) ==> R"
+  shows R
+  by (iprover intro: minor major [THEN spec])
 
 lemma all_dupE:
   assumes major: "ALL x. P(x)"
-      and minor: "[| P(x); ALL x. P(x) |] ==> R"
-  shows "R"
-by (iprover intro: minor major major [THEN spec])
+    and minor: "[| P(x); ALL x. P(x) |] ==> R"
+  shows R
+  by (iprover intro: minor major major [THEN spec])
 
 
-subsubsection {*False*}
-(*Depends upon spec; it is impossible to do propositional logic before quantifiers!*)
+subsubsection {* False *}
+
+text {*
+  Depends upon @{text spec}; it is impossible to do propositional
+  logic before quantifiers!
+*}
 
 lemma FalseE: "False ==> P"
-apply (unfold False_def)
-apply (erule spec)
-done
+  apply (unfold False_def)
+  apply (erule spec)
+  done
 
-lemma False_neq_True: "False=True ==> P"
-by (erule eqTrueE [THEN FalseE])
+lemma False_neq_True: "False = True ==> P"
+  by (erule eqTrueE [THEN FalseE])
 
 
-subsubsection {*Negation*}
+subsubsection {* Negation *}
 
 lemma notI:
-  assumes p: "P ==> False"
+  assumes "P ==> False"
   shows "~P"
-apply (unfold not_def)
-apply (iprover intro: impI p)
-done
+  apply (unfold not_def)
+  apply (iprover intro: impI assms)
+  done
 
 lemma False_not_True: "False ~= True"
-apply (rule notI)
-apply (erule False_neq_True)
-done
+  apply (rule notI)
+  apply (erule False_neq_True)
+  done
 
 lemma True_not_False: "True ~= False"
-apply (rule notI)
-apply (drule sym)
-apply (erule False_neq_True)
-done
+  apply (rule notI)
+  apply (drule sym)
+  apply (erule False_neq_True)
+  done
 
 lemma notE: "[| ~P;  P |] ==> R"
-apply (unfold not_def)
-apply (erule mp [THEN FalseE])
-apply assumption
-done
+  apply (unfold not_def)
+  apply (erule mp [THEN FalseE])
+  apply assumption
+  done
 
-(* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *)
-lemmas notI2 = notE [THEN notI, standard]
+lemma notI2: "(P \<Longrightarrow> \<not> Pa) \<Longrightarrow> (P \<Longrightarrow> Pa) \<Longrightarrow> \<not> P"
+  by (erule notE [THEN notI]) (erule meta_mp)
 
 
 subsubsection {*Implication*}