529 |
529 |
530 lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A" |
530 lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A" |
531 by (lifting fcard_raw_suc_memb) |
531 by (lifting fcard_raw_suc_memb) |
532 |
532 |
533 lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0" |
533 lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0" |
534 by (lifting mem_card_not_0) |
534 by (lifting memb_card_not_0) |
535 |
535 |
536 text {* funion *} |
536 text {* funion *} |
537 |
537 |
538 lemma funion_simps[simp]: |
538 lemma funion_simps[simp]: |
539 shows "{||} |\<union>| S = S" |
539 shows "{||} |\<union>| S = S" |
540 and "finsert x S |\<union>| T = finsert x (S |\<union>| T)" |
540 and "finsert x S |\<union>| T = finsert x (S |\<union>| T)" |
541 by (lifting append.simps) |
541 by (lifting append.simps) |
542 |
542 |
|
543 lemma funion_empty[simp]: |
|
544 shows "S |\<union>| {||} = S" |
|
545 by (lifting append_Nil2) |
|
546 |
543 lemma funion_sym: |
547 lemma funion_sym: |
544 shows "S |\<union>| T = T |\<union>| S" |
548 shows "S |\<union>| T = T |\<union>| S" |
545 by (lifting funion_sym_pre) |
549 by (lifting funion_sym_pre) |
546 |
550 |
547 lemma funion_assoc: |
551 lemma funion_assoc: |
548 shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)" |
552 shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)" |
549 by (lifting append_assoc) |
553 by (lifting append_assoc) |
|
554 |
|
555 lemma singleton_union_left: |
|
556 "{|a|} |\<union>| S = finsert a S" |
|
557 by simp |
|
558 |
|
559 lemma singleton_union_right: |
|
560 "S |\<union>| {|a|} = finsert a S" |
|
561 by (subst funion_sym) simp |
550 |
562 |
551 section {* Induction and Cases rules for finite sets *} |
563 section {* Induction and Cases rules for finite sets *} |
552 |
564 |
553 lemma fset_strong_cases: |
565 lemma fset_strong_cases: |
554 "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)" |
566 "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)" |