equal
deleted
inserted
replaced
402 by (erule contrapos_nn) (erule sym) |
402 by (erule contrapos_nn) (erule sym) |
403 |
403 |
404 lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y" |
404 lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y" |
405 by (erule subst, erule ssubst, assumption) |
405 by (erule subst, erule ssubst, assumption) |
406 |
406 |
407 (*still used in HOLCF*) |
|
408 lemma rev_contrapos: |
|
409 assumes pq: "P ==> Q" |
|
410 and nq: "~Q" |
|
411 shows "~P" |
|
412 apply (rule nq [THEN contrapos_nn]) |
|
413 apply (erule pq) |
|
414 done |
|
415 |
407 |
416 subsubsection {*Existential quantifier*} |
408 subsubsection {*Existential quantifier*} |
417 |
409 |
418 lemma exI: "P x ==> EX x::'a. P x" |
410 lemma exI: "P x ==> EX x::'a. P x" |
419 apply (unfold Ex_def) |
411 apply (unfold Ex_def) |