src/FOL/ex/Intro.thy

--- a/src/FOL/ex/Intro.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Intro.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -13,7 +13,7 @@
 
 subsubsection \<open>Some simple backward proofs\<close>
 
-lemma mythm: "P|P --> P"
+lemma mythm: "P \<or> P \<longrightarrow> P"
 apply (rule impI)
 apply (rule disjE)
 prefer 3 apply (assumption)
@@ -21,7 +21,7 @@
 apply assumption
 done
 
-lemma "(P & Q) | R --> (P | R)"
+lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R)"
 apply (rule impI)
 apply (erule disjE)
 apply (drule conjunct1)
@@ -30,8 +30,8 @@
 apply assumption+
 done
 
-(*Correct version, delaying use of "spec" until last*)
-lemma "(ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
+text \<open>Correct version, delaying use of @{text spec} until last.\<close>
+lemma "(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>z w. P(w,z))"
 apply (rule impI)
 apply (rule allI)
 apply (rule allI)
@@ -43,14 +43,12 @@
 
 subsubsection \<open>Demonstration of @{text "fast"}\<close>
 
-lemma "(EX y. ALL x. J(y,x) <-> ~J(x,x))
-        -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
+lemma "(\<exists>y. \<forall>x. J(y,x) \<longleftrightarrow> \<not> J(x,x)) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. J(z,y) \<longleftrightarrow> \<not> J(z,x))"
 apply fast
 done
 
 
-lemma "ALL x. P(x,f(x)) <->
-        (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
+lemma "\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
 apply fast
 done
 
@@ -58,8 +56,8 @@
 subsubsection \<open>Derivation of conjunction elimination rule\<close>
 
 lemma
-  assumes major: "P&Q"
-    and minor: "[| P; Q |] ==> R"
+  assumes major: "P \<and> Q"
+    and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
   shows R
 apply (rule minor)
 apply (rule major [THEN conjunct1])
@@ -72,8 +70,8 @@
 text \<open>Derivation of negation introduction\<close>
 
 lemma
-  assumes "P ==> False"
-  shows "~ P"
+  assumes "P \<Longrightarrow> False"
+  shows "\<not> P"
 apply (unfold not_def)
 apply (rule impI)
 apply (rule assms)
@@ -81,7 +79,7 @@
 done
 
 lemma
-  assumes major: "~P"
+  assumes major: "\<not> P"
     and minor: P
   shows R
 apply (rule FalseE)
@@ -92,7 +90,7 @@
 
 text \<open>Alternative proof of the result above\<close>
 lemma
-  assumes major: "~P"
+  assumes major: "\<not> P"
     and minor: P
   shows R
 apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])