754 text {* proper subset relation on finite sets *} |
754 text {* proper subset relation on finite sets *} |
755 |
755 |
756 definition finite_psubset :: "('a set * 'a set) set" |
756 definition finite_psubset :: "('a set * 'a set) set" |
757 where "finite_psubset == {(A,B). A < B & finite B}" |
757 where "finite_psubset == {(A,B). A < B & finite B}" |
758 |
758 |
759 lemma wf_finite_psubset: "wf(finite_psubset)" |
759 lemma wf_finite_psubset[simp]: "wf(finite_psubset)" |
760 apply (unfold finite_psubset_def) |
760 apply (unfold finite_psubset_def) |
761 apply (rule wf_measure [THEN wf_subset]) |
761 apply (rule wf_measure [THEN wf_subset]) |
762 apply (simp add: measure_def inv_image_def less_than_def less_eq) |
762 apply (simp add: measure_def inv_image_def less_than_def less_eq) |
763 apply (fast elim!: psubset_card_mono) |
763 apply (fast elim!: psubset_card_mono) |
764 done |
764 done |
765 |
765 |
766 lemma trans_finite_psubset: "trans finite_psubset" |
766 lemma trans_finite_psubset: "trans finite_psubset" |
767 by (simp add: finite_psubset_def less_le trans_def, blast) |
767 by (simp add: finite_psubset_def less_le trans_def, blast) |
768 |
768 |
769 |
769 lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset = (A < B & finite B)" |
|
770 unfolding finite_psubset_def by auto |
770 |
771 |
771 |
772 |
772 text {*Wellfoundedness of @{text same_fst}*} |
773 text {*Wellfoundedness of @{text same_fst}*} |
773 |
774 |
774 definition |
775 definition |