Theory Finiteness

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