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