src/FOL/IFOL.thy
 changeset 23393 31781b2de73d parent 23171 861f63a35d31 child 24097 86734ba03ca2
```     1.1 --- a/src/FOL/IFOL.thy	Thu Jun 14 22:59:42 2007 +0200
1.2 +++ b/src/FOL/IFOL.thy	Thu Jun 14 23:04:36 2007 +0200
1.3 @@ -319,27 +319,23 @@
1.4  ***)
1.5
1.6  lemma ex1I:
1.7 -  assumes "P(a)"
1.8 -    and "!!x. P(x) ==> x=a"
1.9 -  shows "EX! x. P(x)"
1.10 +  "P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)"
1.11    apply (unfold ex1_def)
1.12 -  apply (assumption | rule assms exI conjI allI impI)+
1.13 +  apply (assumption | rule exI conjI allI impI)+
1.14    done
1.15
1.16  (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
1.17  lemma ex_ex1I:
1.18 -  assumes ex: "EX x. P(x)"
1.19 -    and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
1.20 -  shows "EX! x. P(x)"
1.21 -  apply (rule ex [THEN exE])
1.22 -  apply (assumption | rule ex1I eq)+
1.23 +  "EX x. P(x) \<Longrightarrow> (!!x y. [| P(x); P(y) |] ==> x=y) \<Longrightarrow> EX! x. P(x)"
1.24 +  apply (erule exE)
1.25 +  apply (rule ex1I)
1.26 +   apply assumption
1.27 +  apply assumption
1.28    done
1.29
1.30  lemma ex1E:
1.31 -  assumes ex1: "EX! x. P(x)"
1.32 -    and r: "!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R"
1.33 -  shows R
1.34 -  apply (insert ex1, unfold ex1_def)
1.35 +  "EX! x. P(x) \<Longrightarrow> (!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R) \<Longrightarrow> R"
1.36 +  apply (unfold ex1_def)
1.37    apply (assumption | erule exE conjE)+
1.38    done
1.39
1.40 @@ -572,11 +568,11 @@
1.41  (*Simplifies the implication.  Classical version is stronger.
1.42    Still UNSAFE since ~P must be provable -- backtracking needed.  *)
1.43  lemma not_impE:
1.44 -  assumes major: "~P --> S"
1.45 -    and r1: "P ==> False"
1.46 -    and r2: "S ==> R"
1.47 -  shows R
1.48 -  apply (assumption | rule notI impI major [THEN mp] r1 r2)+
1.49 +  "~P --> S \<Longrightarrow> (P ==> False) \<Longrightarrow> (S ==> R) \<Longrightarrow> R"
1.50 +  apply (drule mp)
1.51 +   apply (rule notI)
1.52 +   apply assumption
1.53 +  apply assumption
1.54    done
1.55
1.56  (*Simplifies the implication.   UNSAFE.  *)
1.57 @@ -595,7 +591,7 @@
1.58      and r1: "!!x. P(x)"
1.59      and r2: "S ==> R"
1.60    shows R
1.61 -  apply (assumption | rule allI impI major [THEN mp] r1 r2)+
1.62 +  apply (rule allI impI major [THEN mp] r1 r2)+
1.63    done
1.64
1.65  (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
1.66 @@ -609,10 +605,8 @@
1.67  (*** Courtesy of Krzysztof Grabczewski ***)
1.68
1.69  lemma disj_imp_disj:
1.70 -  assumes major: "P|Q"
1.71 -    and "P==>R" and "Q==>S"
1.72 -  shows "R|S"
1.73 -  apply (rule disjE [OF major])
1.74 +  "P|Q \<Longrightarrow> (P==>R) \<Longrightarrow> (Q==>S) \<Longrightarrow> R|S"
1.75 +  apply (erule disjE)
1.76    apply (rule disjI1) apply assumption
1.77    apply (rule disjI2) apply assumption
1.78    done
```