theory SetUtils imports Main begin ― ‹TODO use Inf instead of Min where necessary.› ― ‹TODO can be replaced by @{term "card_Un_disjoint (⟦finite A; finite B; A ∩ B = {}⟧ ⟹ card (A ∪ B) = card A + card B)"} ?› lemma card_union': "(finite s) ∧ (finite t) ∧ (disjnt s t) ⟹ (card (s ∪ t) = card s + card t)" by (simp add: card_Un_disjoint disjnt_def) lemma CARD_INJ_IMAGE_2: fixes f s assumes "finite s" "(∀x y. ((x ∈ s) ∧ (y ∈ s)) ⟶ ((f x = f y) ⟷ (x = y)))" shows "(card (f ` s) = card s)" proof - { fix x y assume "x ∈ s" "y ∈ s" then have "f x = f y ⟶ x = y" using assms(2) by blast } then have "inj_on f s" by (simp add: inj_onI) then show ?thesis using assms(1) inj_on_iff_eq_card by blast qed lemma scc_main_lemma_x: "⋀s t x. (x ∈ s) ∧ ¬(x ∈ t) ⟹ ¬(s = t)" by blast lemma neq_funs_neq_images: fixes s assumes "∀x. x ∈ s ⟶ (∀y. y ∈ s ⟶ f1 x ≠ f2 y)" "∃x. x ∈ s" shows "f1 ` s ≠ f2 ` s" using assms by blast subsection "Sets of Numbers" ― ‹TODO Is '<=' natural number lte or overloaded? If it's overloaded for reals, this might be wrong (e.g. the real set s = [0; 1] is not finite even though @{term "∀ x ∈ s. x ≤ 1"} holds).› lemma mems_le_finite_i: fixes s :: "nat set" and k :: nat shows "(∀ x. x ∈ s ⟶ x ≤ k) ⟹ finite s" proof - assume P: "(∀ x. x ∈ s ⟶ x ≤ k)" let ?f = "id :: nat ⇒ nat" let ?S = "{i. i ≤ k}" have "s ⊆ ?S" using P by blast moreover have "?f ` ?S = ?S" by auto moreover have "finite ?S" using nat_seg_image_imp_finite by auto moreover have "finite s" using calculation finite_subset by auto ultimately show ?thesis by auto qed lemma mems_le_finite: fixes s :: "nat set" and k :: nat shows "⋀(s :: nat set) k. (∀ x. x ∈ s ⟶ x ≤ k) ⟹ finite s" using mems_le_finite_i by auto ― ‹NOTE translated `s` to `nat set` (more generality wasn't required.).› lemma mem_le_imp_MIN_le: fixes s :: "nat set" and k :: nat assumes "∃x. (x ∈ s) ∧ (x ≤ k)" shows "(Inf s ≤ k)" proof - from assms obtain x where 1: "x ∈ s" "x ≤ k" by blast { assume C: "Inf s > k" then have "Inf s > x" using 1(2) by fastforce then have False using 1(1) cInf_lower leD by fast } then show ?thesis by fastforce qed ― ‹NOTE nat --> bool is the type of a HOL4 set and was translated to 'nat set'.› ― ‹NOTE We cannot use 'Min' instead of 'Inf' because there is no indication that '{n. s n}' will be finite. Without that @{term "Min {n. s n} ∈ {n. s n}"} is not necessarily true.› lemma mem_lt_imp_MIN_lt: fixes s :: "nat set" and k :: nat assumes "(∃x. x ∈ s ∧ x < k)" shows "(Inf s) < k" proof - obtain x where 1: "x ∈ s" "x < k" using assms by blast then have 2: "s ≠ {}" by blast then have "Inf s ∈ s" using Inf_nat_def LeastI by force moreover have "∀x∈s. Inf s ≤ x" by (simp add: cInf_lower) ultimately show "(Inf s) < k" using assms leD by force qed ― ‹NOTE type for 'k' had to be fixed (type unordered error; also not true for e.g. real sets).› lemma bound_child_parent_neq_mems_state_set_neq_len: fixes s and k :: nat assumes "(∀x. x ∈ s ⟶ x < k)" shows "finite s" using assms bounded_nat_set_is_finite by blast lemma bound_main_lemma_2: "⋀(s :: nat set) k. (s ≠ {}) ∧ (∀x. x ∈ s ⟶ x ≤ k) ⟹ Sup s ≤ k" proof - fix s :: "nat set" and k { assume P1: "s ≠ {}" assume P2: "(∀x. x ∈ s ⟶ x ≤ k)" have "finite s" using P2 mems_le_finite by auto moreover have "Max s ∈ s" using P1 calculation Max_in by auto moreover have "Max s ≤ k" using P2 calculation by auto } then show "(s ≠ {}) ∧ (∀x. x ∈ s ⟶ x ≤ k) ⟹ Sup s ≤ k" by (simp add: Sup_nat_def) qed ― ‹NOTE type of 'k' fixed to nat to be able to use 'bound\_child\_parent\_neq\_mems\_state\_set\_neq\_len'.› lemma bound_child_parent_not_eq_last_diff_paths: "⋀s (k :: nat). (s ≠ {}) ⟹ (∀x. x ∈ s ⟶ x < k) ⟹ Sup s < k " by (simp add: Sup_nat_def bound_child_parent_neq_mems_state_set_neq_len) lemma FINITE_ALL_DISTINCT_LISTS_i: fixes P assumes "finite P" shows " {p. distinct p ∧ set p ⊆ P} = {[]} ∪ (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P))" proof - let ?A="{p. distinct p ∧ set p ⊆ P }" let ?B="{[]} ∪ (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P))" { { fix a assume P: "a ∈ ?A" then have "a ∈ ?B" proof (cases a) text ‹ The empty list is distinct and its corresponding set is the empty set which is a trivial subset of `?B`. The `Nil` case can therefore be derived by automation. › case (Cons h list) { let ?b'="h" { from P have "set a ⊆ P" by simp then have "set list ⊆ (P - {h})" using P dual_order.trans local.Cons by auto } moreover from P Cons have "distinct list" by force ultimately have "a ∈ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ?b')" using Cons by blast moreover { from P Cons have "?b' ∈ set a" by simp moreover from P have "set a ⊆ P" by simp ultimately have "?b' ∈ P" by auto } ultimately have "∃b' ∈ P. a ∈ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) b')" by meson } then obtain b' where "b' ∈ P" "a ∈ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) b')" by blast then show ?thesis by blast qed blast } then have "?A ⊆ ?B" by auto } moreover { { fix b assume P: "b ∈ ?B" have "b ∈ ?A" text ‹ The empty list is in `?B` by construction. The `Nil` case can therefore be derived straightforwardly.› proof (cases b) case (Cons a list) from P Cons obtain b' where a: "b' ∈ P" "b ∈ {b' # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {b'})}" by fast then obtain p0 where b: "b = b' # p0" "distinct p0" "set p0 ⊆ (P - {b'})" by blast then have "distinct (b' # p0)" by (simp add: subset_Diff_insert) moreover have "set (b' # p0) ⊆ P" using a(1) b(3) by auto ultimately show ?thesis using b(1) by fast qed simp } then have "?B ⊆ ?A" by blast } ultimately show ?thesis using set_eq_subset by blast qed lemma FINITE_ALL_DISTINCT_LISTS: fixes P assumes "finite P" shows "finite {p. distinct p ∧ set p ⊆ P}" using assms proof (induction "card P" arbitrary: P) case 0 then have "P = {}" by force then show ?case using 0 by simp next case (Suc x) { text ‹ Proof the finiteness of the union by proving both sets of the union are finite. The singleton set `{[]}` is trivially finite. › { { fix e assume P: "e ∈ P" have " {e # p0 | p0. distinct p0 ∧ set p0 ⊆ P - {e}} = (λp. e # p) ` { p. distinct p ∧ set p ⊆ P - {e}}" by blast moreover { let ?P'="P - {e}" from Suc.prems have "finite ?P'" by blast text ‹ The finiteness can now be shown using the induction hypothesis. However `e` might already be contained in `?P`, so we have to split cases first. › have "finite ((λp. e # p) ` {p. distinct p ∧ set p ⊆ ?P'})" proof (cases "e ∈ P") case True then have "x = card ?P'" using Suc.prems Suc(2) by fastforce moreover from Suc.prems have "finite ?P'" by blast ultimately show ?thesis using Suc(1) by blast next case False then have "?P' = P" by simp then have "finite {p. distinct p ∧ set p ⊆ ?P'}" using False P by linarith then show ?thesis using finite_imageI by blast qed } ultimately have "finite {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}" by argo } then have "finite (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P))" using Suc.prems by blast } then have "finite ({[]} ∪ (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P)))" using finite_Un by blast } then show ?case using FINITE_ALL_DISTINCT_LISTS_i[OF Suc.prems] by force qed lemma subset_inter_diff_empty: assumes "s ⊆ t" shows "(s ∩ (u - t) = {})" using assms by auto end