diff -r 4b03e3586f7f -r 31781b2de73d src/FOL/IFOL.thy --- 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) \ (!!x. P(x) ==> x=a) \ 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) \ (!!x y. [| P(x); P(y) |] ==> x=y) \ 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) \ (!!x. [| P(x); ALL y. P(y) --> y=x |] ==> R) \ 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 \ (P ==> False) \ (S ==> R) \ 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 \ (P==>R) \ (Q==>S) \ R|S" + apply (erule disjE) apply (rule disjI1) apply assumption apply (rule disjI2) apply assumption done