equal
deleted
inserted
replaced
893 lemma subset_insertI: "B \<subseteq> insert a B" |
893 lemma subset_insertI: "B \<subseteq> insert a B" |
894 apply (rule subsetI) |
894 apply (rule subsetI) |
895 apply (erule insertI2) |
895 apply (erule insertI2) |
896 done |
896 done |
897 |
897 |
|
898 lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B" |
|
899 by blast |
|
900 |
898 lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)" |
901 lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)" |
899 by blast |
902 by blast |
900 |
903 |
901 |
904 |
902 text {* \medskip Big Union -- least upper bound of a set. *} |
905 text {* \medskip Big Union -- least upper bound of a set. *} |
958 |
961 |
959 text {* \medskip Set difference. *} |
962 text {* \medskip Set difference. *} |
960 |
963 |
961 lemma Diff_subset: "A - B \<subseteq> A" |
964 lemma Diff_subset: "A - B \<subseteq> A" |
962 by blast |
965 by blast |
|
966 |
|
967 lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)" |
|
968 by blast |
963 |
969 |
964 |
970 |
965 text {* \medskip Monotonicity. *} |
971 text {* \medskip Monotonicity. *} |
966 |
972 |
967 lemma mono_Un: includes mono shows "f A \<union> f B \<subseteq> f (A \<union> B)" |
973 lemma mono_Un: includes mono shows "f A \<union> f B \<subseteq> f (A \<union> B)" |
1050 by auto |
1056 by auto |
1051 |
1057 |
1052 lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)" |
1058 lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)" |
1053 by blast |
1059 by blast |
1054 |
1060 |
|
1061 lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)" |
|
1062 by blast |
|
1063 |
1055 lemma insert_disjoint[simp]: |
1064 lemma insert_disjoint[simp]: |
1056 "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})" |
1065 "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})" |
1057 by blast |
1066 by blast |
1058 |
1067 |
1059 lemma disjoint_insert[simp]: |
1068 lemma disjoint_insert[simp]: |
1493 by blast |
1502 by blast |
1494 |
1503 |
1495 lemma Diff_cancel [simp]: "A - A = {}" |
1504 lemma Diff_cancel [simp]: "A - A = {}" |
1496 by blast |
1505 by blast |
1497 |
1506 |
|
1507 lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)" |
|
1508 by blast |
|
1509 |
1498 lemma Diff_triv: "A \<inter> B = {} ==> A - B = A" |
1510 lemma Diff_triv: "A \<inter> B = {} ==> A - B = A" |
1499 by (blast elim: equalityE) |
1511 by (blast elim: equalityE) |
1500 |
1512 |
1501 lemma empty_Diff [simp]: "{} - A = {}" |
1513 lemma empty_Diff [simp]: "{} - A = {}" |
1502 by blast |
1514 by blast |
1521 lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))" |
1533 lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))" |
1522 by auto |
1534 by auto |
1523 |
1535 |
1524 lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B" |
1536 lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B" |
1525 by blast |
1537 by blast |
|
1538 |
|
1539 lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A" |
|
1540 by blast |
1526 |
1541 |
1527 lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A" |
1542 lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A" |
1528 by blast |
1543 by blast |
1529 |
1544 |
1530 lemma Diff_insert_absorb: "x \<notin> A ==> (insert x A) - {x} = A" |
1545 lemma Diff_insert_absorb: "x \<notin> A ==> (insert x A) - {x} = A" |