equal
deleted
inserted
replaced
517 by (etac (rewrite_rule [le_def] Least_le RS notE) 1 THEN assume_tac 1); |
517 by (etac (rewrite_rule [le_def] Least_le RS notE) 1 THEN assume_tac 1); |
518 qed "not_less_Least"; |
518 qed "not_less_Least"; |
519 |
519 |
520 (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *) |
520 (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *) |
521 bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE); |
521 bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE); |
|
522 |
|
523 Goal "(S::nat set) ~= {} ==> ? x:S. ! y:S. x <= y"; |
|
524 by (cut_facts_tac [wf_pred_nat RS wf_trancl RS (wf_eq_minimal RS iffD1)] 1); |
|
525 by (dres_inst_tac [("x","S")] spec 1); |
|
526 by (Asm_full_simp_tac 1); |
|
527 by (etac impE 1); |
|
528 by (Force_tac 1); |
|
529 by (force_tac (claset(), simpset() addsimps [less_eq,not_le_iff_less]) 1); |
|
530 qed "nonempty_has_least"; |