equal
deleted
inserted
replaced
19 goalw Setplus.thy [ssubset_def] "A < B = ((A <= B) & ~(A=B))"; |
19 goalw Setplus.thy [ssubset_def] "A < B = ((A <= B) & ~(A=B))"; |
20 by (rtac refl 1); |
20 by (rtac refl 1); |
21 qed "ssubset_iff"; |
21 qed "ssubset_iff"; |
22 |
22 |
23 goal Setplus.thy "((A::'a set) <= B) = ((A < B) | (A=B))"; |
23 goal Setplus.thy "((A::'a set) <= B) = ((A < B) | (A=B))"; |
24 by (simp_tac (set_ss addsimps [ssubset_iff]) 1); |
24 by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1); |
25 by (fast_tac set_cs 1); |
25 by (fast_tac set_cs 1); |
26 qed "subseteq_iff_subset_eq"; |
26 qed "subseteq_iff_subset_eq"; |
27 |
27 |
28 (*Rule in Modus Ponens style*) |
28 (*Rule in Modus Ponens style*) |
29 goal Setplus.thy "A < B --> c:A --> c:B"; |
29 goal Setplus.thy "A < B --> c:A --> c:B"; |
30 by (simp_tac (set_ss addsimps [ssubset_iff]) 1); |
30 by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1); |
31 by (fast_tac set_cs 1); |
31 by (fast_tac set_cs 1); |
32 qed "ssubsetD"; |
32 qed "ssubsetD"; |
33 |
33 |
34 (*********) |
34 (*********) |
35 |
35 |