equal
deleted
inserted
replaced
830 |
830 |
831 |
831 |
832 subsubsection {* The ``proper subset'' relation *} |
832 subsubsection {* The ``proper subset'' relation *} |
833 |
833 |
834 lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B" |
834 lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B" |
|
835 by (unfold psubset_def) blast |
|
836 |
|
837 lemma psubsetE [elim!]: |
|
838 "[|A \<subset> B; [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R" |
835 by (unfold psubset_def) blast |
839 by (unfold psubset_def) blast |
836 |
840 |
837 lemma psubset_insert_iff: |
841 lemma psubset_insert_iff: |
838 "(A \<subset> insert x B) = (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)" |
842 "(A \<subset> insert x B) = (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)" |
839 by (auto simp add: psubset_def subset_insert_iff) |
843 by (auto simp add: psubset_def subset_insert_iff) |