13 lemmas [intro!!] = isLub_isUb; |
13 lemmas [intro!!] = isLub_isUb; |
14 lemmas [intro!!] = chainD; |
14 lemmas [intro!!] = chainD; |
15 lemmas chainE2 = chainD2 [elimify]; |
15 lemmas chainE2 = chainD2 [elimify]; |
16 |
16 |
17 text_raw {* \medskip *}; |
17 text_raw {* \medskip *}; |
18 text{* Lemmas about sets: *}; |
18 text{* Lemmas about sets. *}; |
19 |
19 |
20 lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v"; |
20 lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v"; |
21 by (fast elim: equalityE); |
21 by (fast elim: equalityE); |
22 |
22 |
23 lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H"; |
23 lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H"; |
24 by (force simp add: psubset_eq); |
24 by (force simp add: psubset_eq); |
25 |
25 |
26 text_raw {* \medskip *}; |
26 text_raw {* \medskip *}; |
27 text{* Some lemmas about orders: *}; |
27 text{* Some lemmas about orders. *}; |
28 |
28 |
29 lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y"; |
29 lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y"; |
30 by (rule order_less_le[RS iffD1, RS conjunct2]); |
30 by (rule order_less_le[RS iffD1, RS conjunct2]); |
31 |
31 |
32 lemma le_noteq_imp_less: |
32 lemma le_noteq_imp_less: |