equal
deleted
inserted
replaced
202 val prems = Goalw [ex1_def] |
202 val prems = Goalw [ex1_def] |
203 "[| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)"; |
203 "[| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)"; |
204 by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ; |
204 by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ; |
205 qed "ex1I"; |
205 qed "ex1I"; |
206 |
206 |
207 (*Sometimes easier to use: the premises have no shared variables. Safe!*) |
207 (*SOMEtimes easier to use: the premises have no shared variables. Safe!*) |
208 val [ex,eq] = Goal |
208 val [ex,eq] = Goal |
209 "[| EX x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"; |
209 "[| EX x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"; |
210 by (rtac (ex RS exE) 1); |
210 by (rtac (ex RS exE) 1); |
211 by (REPEAT (ares_tac [ex1I,eq] 1)) ; |
211 by (REPEAT (ares_tac [ex1I,eq] 1)) ; |
212 qed "ex_ex1I"; |
212 qed "ex_ex1I"; |