src/FOL/IFOL.thy
 changeset 23393 31781b2de73d parent 23171 861f63a35d31 child 24097 86734ba03ca2
```--- a/src/FOL/IFOL.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/FOL/IFOL.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -319,27 +319,23 @@
***)

lemma ex1I:
-  assumes "P(a)"
-    and "!!x. P(x) ==> x=a"
-  shows "EX! x. P(x)"
+  "P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)"
apply (unfold ex1_def)
-  apply (assumption | rule assms exI conjI allI impI)+
+  apply (assumption | rule exI conjI allI impI)+
done

(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
lemma ex_ex1I:
-  assumes ex: "EX x. P(x)"
-    and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
-  shows "EX! x. P(x)"
-  apply (rule ex [THEN exE])
-  apply (assumption | rule ex1I eq)+
+  "EX x. P(x) \<Longrightarrow> (!!x y. [| P(x); P(y) |] ==> x=y) \<Longrightarrow> EX! x. P(x)"
+  apply (erule exE)
+  apply (rule ex1I)
+   apply assumption
+  apply assumption
done

lemma ex1E:
-  assumes ex1: "EX! x. P(x)"
-    and r: "!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R"
-  shows R
-  apply (insert ex1, unfold ex1_def)
+  "EX! x. P(x) \<Longrightarrow> (!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R) \<Longrightarrow> R"
+  apply (unfold ex1_def)
apply (assumption | erule exE conjE)+
done

@@ -572,11 +568,11 @@
(*Simplifies the implication.  Classical version is stronger.
Still UNSAFE since ~P must be provable -- backtracking needed.  *)
lemma not_impE:
-  assumes major: "~P --> S"
-    and r1: "P ==> False"
-    and r2: "S ==> R"
-  shows R
-  apply (assumption | rule notI impI major [THEN mp] r1 r2)+
+  "~P --> S \<Longrightarrow> (P ==> False) \<Longrightarrow> (S ==> R) \<Longrightarrow> R"
+  apply (drule mp)
+   apply (rule notI)
+   apply assumption
+  apply assumption
done

(*Simplifies the implication.   UNSAFE.  *)
@@ -595,7 +591,7 @@
and r1: "!!x. P(x)"
and r2: "S ==> R"
shows R
-  apply (assumption | rule allI impI major [THEN mp] r1 r2)+
+  apply (rule allI impI major [THEN mp] r1 r2)+
done

(*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
@@ -609,10 +605,8 @@
(*** Courtesy of Krzysztof Grabczewski ***)

lemma disj_imp_disj:
-  assumes major: "P|Q"
-    and "P==>R" and "Q==>S"
-  shows "R|S"
-  apply (rule disjE [OF major])
+  "P|Q \<Longrightarrow> (P==>R) \<Longrightarrow> (Q==>S) \<Longrightarrow> R|S"
+  apply (erule disjE)
apply (rule disjI1) apply assumption
apply (rule disjI2) apply assumption
done```