theory Finiteness imports Main "HOL-Eisbach.Eisbach_Tools" begin section ‹Two Eisbach proof methods for finiteness of sets› text ‹ The first method is intended to act more conservatively (think ‹safe›), leaving subgoals for the user where it couldn't proceed any further. The second method is more powerful, acting more in a succeed-or-die manner, similarly to ‹force› and friends. The examples in the second section should give a good impression of where these methods can help. › text ‹This slot is intended to provide more ‹intro› theorems for finite sets.› named_theorems finite (* Trick from Dan Matichuk on isabelle-users *) method add_finite_Collect_simproc methods m = match termI in H[simproc add: finite_Collect]:_ ⇒ m (* Trick from Dan Matichuk on isabelle-users. Turns a structured method into a simple one. *) method_setup simple_method = ‹Method.text_closure >> (fn m => fn ctxt => let val facts = Method.get_facts ctxt val insert' = Method.Basic (K (Method.insert facts)) val m' = Method.Combinator (Method.no_combinator_info, Method.Then, [insert', m]) in Method.evaluate m' ctxt end)› method finite_tup = match conclusion in "finite (_ × _)" ⇒ ‹rule finite_cartesian_product; finite_tup› ¦ "finite S" for S :: "(_ * _) set" ⇒ ‹print_term S, (rule finite_subset[where A = S and B = "fst ` S × snd ` S"]; finite_tup? | (rule finite_subset; assumption?; fastforce))› ¦ "finite X" for X ⇒ ‹print_term X, (simp add: image_def, finite_tup?)?, (solves ‹(rule finite_subset; assumption?; fastforce)›)?› ¦ _ ⇒ ‹fastforce simp: image_def› method finite_search = match conclusion in "finite (_ × _)" ⇒ ‹rule finite_cartesian_product; finite_search› ¦ "finite (_ ` _)" ⇒ ‹simp; finite_search | rule finite_imageI; finite_search› ¦ "finite S" for S :: "(_ * _) set" ⇒ ‹print_term S, (solves ‹rule finite_subset; auto› | rule finite_subset[where A = S and B = "fst ` S × snd ` S"]; finite_tup?)› ¦ "finite (Collect f)" for f ⇒ ‹print_term f, (add_finite_Collect_simproc simp)?; (solves ‹auto intro: finite› | print_term v, simp?, rule finite; (assumption | finite_search) | rule finite_imageI; finite_search | rule finite_vimageI; finite_search | print_term x, rule finite_subset; assumption?; fastforce)› ¦ "finite X" for X ⇒ ‹print_term X, (rule finite; (assumption | finite_search) |(simp add: image_def, finite_search?)?, (solves ‹(rule finite_subset; assumption?; fastforce)›)?)› ¦ _ ⇒ ‹fastforce simp: image_def› method finite = simple_method finite_search section ‹Tests› subsection ‹Counterexamples› lemma inj_finite_single: assumes "inj f" shows "finite {y. x = f y}" using assms Collect_mem_eq Collect_mono_iff infinite_iff_countable_subset inj_eq not_finite_existsD rangeI by fastforce lemmas inj_finite_single[finite] text ‹It's hard to guess the right set› lemma inj_finite_single': assumes "inj f" shows "finite {z. f z = x}" apply (rule finite_subset[of _ "{z. x = f z}"]) apply blast using assms by finite (* Due to Lars Hupel *) definition select :: "('a ⇀ 'b) ⇒ 'a set ⇒ 'b set" where "select f S = {z | z. ∃x ∈ S. f x = Some z}" lemma select_finite: assumes "finite S" shows "finite (select f S)" using assms unfolding select_def by finite lemmas inj_finite_single'[finite] subsection ‹Working Examples› lemma assumes "finite A" shows "finite {x. x ∈ A ∧ P x}" using assms by finite_search lemma collect_pair_finite[finite]: assumes "finite {x. P x}" "finite {x. Q x}" shows "finite {(x, y) . P x ∧ Q y ∧ R x y}" using assms by - finite lemma collect_pair_finite'[finite]: assumes "finite {(x, y). P x y}" shows "finite {(x, y) . P x y ∧ R x y}" using assms by - finite text ‹This is what we actually need in this theory› lemma collect_pair_finite''[finite]: assumes "finite {(x, y). P x ∧ Q y}" shows "finite {(x, y) . P x ∧ Q y ∧ R x y}" using assms by - finite lemma finite_imageI': assumes "finite {(x, y). P x y}" shows "finite {f x y | x y. P x y}" using assms by finite lemma assumes "finite (A × B)" shows "finite {(x, y) | x y. x ∈ A ∧ y ∈ B ∧ R x y}" using assms by - finite lemma finite_imageI'': assumes "finite (A × B)" shows "finite {f x y | x y. x ∈ A ∧ y ∈ B ∧ R x y}" using assms by - finite text ‹‹finite_Collect› can also rewrite to ‹vimage›› lemma assumes "inj f" "finite S" shows "finite {y. ∃ x ∈ S. x = f y}" using assms by - finite lemma assumes "inj f" "finite S" shows "finite {y. ∃ x ∈ S. f y = x}" using assms by - finite text ‹Another counter-example› lemma assumes "finite (A × B)" shows "finite {f x y | x y. x ∈ A ∧ y ∈ B ∧ R x y ∧ Q x y ∧ T x ∧ TT y}" (is "finite ?S") proof - have "?S = (λ (x, y). f x y) ` {(x, y). x ∈ A ∧ y ∈ B ∧ R x y ∧ Q x y ∧ T x ∧ TT y}" by auto also have "finite …" using assms by - finite ultimately show ?thesis by simp qed text ‹ Easier proof. The problem for our method is that the simproc fails to turn ?S into the form used in the proof above. Note that the declaration of the ‹finite› attribute below is the only one that is ∗‹necessary› in this theory. › lemma notes finite_imageI''[finite] assumes "finite (A × B)" shows "finite {f x y | x y. x ∈ A ∧ y ∈ B ∧ R x y ∧ Q x y ∧ T x ∧ TT y}" (is "finite ?S") using assms by finite lemma assumes "finite A" "finite B" shows "finite {(x, y) | x y. x ∈ A ∧ y ∈ B ∧ R y ∧ S x}" using assms by - finite lemma fixes P Q R :: "'a ⇒ bool" assumes "finite {x. P x ∧ R x}" shows "finite {x. P x ∧ Q x ∧ R x}" using assms by - finite lemma R: assumes "finite A" "A = B" shows "finite B" using assms by finite lemma pairwise_finiteI: assumes "finite {b. ∃a. P a b}" (is "finite ?B") assumes "finite {a. ∃b. P a b}" shows "finite {(a,b). P a b}" (is "finite ?C") using assms by - finite lemma pairwise_finiteI3: assumes "finite {b. ∃a c. P a b c}" assumes "finite {a. ∃b c. P a b c}" assumes "finite {c. ∃a b. P a b c}" shows "finite {(a,b,c). P a b c}" (is "finite ?C") using assms by - finite lemma pairwise_finiteI4: assumes "finite {b. ∃a c d. P a b c d}" assumes "finite {a. ∃b c d. P a b c d}" assumes "finite {c. ∃a b d. P a b c d}" assumes "finite {d. ∃a b c. P a b c d}" shows "finite {(a,b,c,d). P a b c d}" (is "finite ?C") using assms by - finite lemma finite_ex_and1: assumes "finite {b. ∃a. P a b}" (is "finite ?A") shows "finite {b. ∃a. P a b ∧ Q a b}" (is "finite ?B") using assms by - finite lemma finite_ex_and2: assumes "finite {b. ∃a. Q a b}" (is "finite ?A") shows "finite {b. ∃a. P a b ∧ Q a b}" (is "finite ?B") using assms by - finite text ‹ This is the only lemma where our methods cannot help us so far due to the fairly complex argument that is used in the interactive proof. › lemma finite_set_of_finite_funs2: fixes A :: "'a set" and B :: "'b set" and C :: "'c set" and d :: "'c" assumes "finite A" and "finite B" and "finite C" shows "finite {f. ∀x. ∀y. (x ∈ A ∧ y ∈ B ⟶ f x y ∈ C) ∧ (x ∉ A ⟶ f x y = d) ∧ (y ∉ B ⟶ f x y = d)}" (is "finite ?S") proof - let ?R = "{g. ∀x. (x ∈ B ⟶ g x ∈ C) ∧ (x ∉ B ⟶ g x = d)}" let ?Q = "{f. ∀x. (x ∈ A ⟶ f x ∈ ?R) ∧ (x ∉ A ⟶ f x = (λy. d))}" from finite_set_of_finite_funs[OF assms(2,3)] have "finite ?R" . from finite_set_of_finite_funs[OF assms(1) this, of "λ y. d"] have "finite ?Q" . moreover have "?S = ?Q" by auto (case_tac "xa ∈ A", auto) ultimately show ?thesis by simp qed end