I have a finite set of distinct pairs of 'a × 'b set; I want to obtain choose from each 'b set a /distinct/ 'b. That is, I want to find out how to define choices below such that I can prove the two lemmas:
context
fixes X :: ‹('a × 'b set) set›
assumes ‹finite X›
assumes ‹(a, B) ∈ X ⟹ infinite B›
assumes ‹(a, B⇩1) ∈ X ⟹ (a, B⇩2) ∈ X ⟹ B⇩1 = B⇩2›
begin
definition choices :: ‹('a × 'b set) set => ('a × 'b) set› where ‹choices X ≡ ?›
lemma ‹(a, b) ∈ choices X ⟹ ∃B. b ∈ B ∧ (a, B) ∈ X› sorry
lemma ‹(a⇩1, b⇩1) ∈ X ⟹ (a⇩2, b⇩2) ∈ X ⟹ a⇩1 ≠ a⇩2 ⟹ b⇩1 ≠ b⇩2› sorry
end
As an example, if we knew that ‹X ≡ { (1, {7 <..}), (2, {5 <..}) }›, then example valid values of choices X would be { (1,8), (2,6) } or { (1,1982), (2, 9) }.
How do I define choices?
Mathias Fleury has already provided an outline of a plausible solution. I would like to provide a (not necessarily better) variation using inductive predicates. Please note that I relied heavily on sledgehammer and, overall, did not make any attempts to think the solution through.
definition add :: "'a × 'b ⇒ ('a × 'b) set ⇒ ('a × 'b) set"
where "add x C =
(if fst x ∉ Domain C ∧ snd x ∉ Range C then insert x C else C)"
inductive good_choice :: "('a × 'b set) set ⇒ ('a × 'b) set ⇒ bool"
for X :: "('a × 'b set) set"
where
"good_choice X {}"
| "good_choice X C ⟹ (a, B) ∈ X ⟹ b ∈ B ⟹ good_choice X (add (a, b) C)"
definition choices :: "('a × 'b set) set ⇒ ('a × 'b) set"
where "choices X = (SOME C. good_choice X C ∧ Domain X = Domain C)"
lemma single_valued_add:
assumes "single_valued C"
shows "single_valued (add x C)"
using assms unfolding add_def single_valued_def by auto
lemma good_choice_single_valued:
assumes "good_choice X C"
shows "single_valued C"
using assms by induction (auto simp: single_valued_add)
lemma good_choice_ab:
assumes "good_choice X C" and "(a, b) ∈ C"
shows "∃B. b ∈ B ∧ (a, B) ∈ X"
using assms
apply induction
subgoal by simp
subgoal by (metis add_def fst_conv insert_iff snd_conv)
done
lemma good_choice_inj:
assumes "good_choice X C" and "(a⇩1, b⇩1) ∈ C" and "(a⇩2, b⇩2) ∈ C" and "a⇩1 ≠ a⇩2"
shows "b⇩1 ≠ b⇩2"
using assms
apply induction
subgoal by simp
subgoal by (metis Range.intros add_def insert_iff prod.inject snd_conv)
done
lemma good_choice_insert:
assumes "good_choice X C"
shows "good_choice (insert x X) C"
using assms
apply induct
subgoal by (simp add: good_choice.intros(1))
subgoal by (meson good_choice.intros(2) insertI2)
done
lemma finite_Range:
assumes "finite (Domain R)" and "single_valued R"
shows "finite (Range R)"
proof-
define f where "f x = (THE y. (x, y) ∈ R)" for x
have "Range R = f ` (Domain R)"
proof(intro subset_antisym subsetI)
fix y assume "y ∈ Range R"
then obtain x where "(x, y) ∈ R" by auto
moreover with assms(2) have "f x = y" unfolding f_def
by (simp add: single_valued_def the_equality)
ultimately show "y ∈ f ` Domain R" by auto
next
fix y assume "y ∈ f ` Domain R"
then obtain x where "x ∈ Domain R" and "y = f x" by auto
with assms(2) show "y ∈ Range R"
unfolding f_def by (auto simp: single_valued_def the_equality)
qed
with assms(1) show ?thesis by simp
qed
lemma ex_good_choice:
assumes "finite X"
and "⋀a B. (a, B) ∈ X ⟹ infinite B"
and "⋀a B⇩1 B⇩2. (a, B⇩1) ∈ X ⟹ (a, B⇩2) ∈ X ⟹ B⇩1 = B⇩2"
shows "∃C. good_choice X C ∧ Domain X = Domain C"
using assms
proof(induction rule: finite_induct)
case empty then show ?case using good_choice.intros(1) by force
next
case (insert x F)
from insert(3,4,5) have "∃C. good_choice F C ∧ Domain F = Domain C"
unfolding insert_iff by metis
then obtain C where gc_C: "good_choice F C" and Dom_eq: "Domain F = Domain C"
by clarsimp
obtain a B where x_def: "x = (a, B)" by force+
from insert.hyps(2) insert.prems(2) have "a ∉ Domain F"
unfolding x_def by auto
with Dom_eq have "a ∉ Domain C" by simp
have inf_B: "infinite B" using insert.prems(1) unfolding x_def by auto
from insert have "finite (Domain C)" by (metis Dom_eq finite_Domain)
moreover from gc_C have "single_valued C"
by (auto intro: good_choice_single_valued)
ultimately have "finite (Range C)" using finite_Range by auto
then have "B - Range C ≠ {}" by (metis finite.emptyI finite_Diff2 inf_B)
then obtain b where "b ∈ B - Range C" by auto
then have "b ∈ B" by simp
from gc_C have gc_xC: "good_choice (insert x F) C"
by (auto intro: good_choice_insert)
have aB: "(a, B) ∈ insert x F" unfolding x_def by simp
have "good_choice (insert x F) (add (a, b) C)"
by (rule good_choice.intros(2)[OF gc_xC aB ‹b ∈ B›])
moreover have "Domain (insert x F) = Domain (add (a, b) C)"
unfolding x_def
by
(
metis
DiffD2
Dom_eq
Domain_insert
‹a ∉ Domain F›
‹b ∈ B - Range C›
add_def
fst_conv
snd_conv
)
ultimately show
"∃C. good_choice (insert x F) C ∧ Domain (insert x F) = Domain C"
by auto
qed
context
fixes X :: ‹('a × 'b set) set›
assumes fin: ‹finite X›
assumes inf: ‹(a, B) ∈ X ⟹ infinite B›
assumes sv: ‹(a, B⇩1) ∈ X ⟹ (a, B⇩2) ∈ X ⟹ B⇩1 = B⇩2›
begin
lemma good_choice_choices:
"good_choice X (choices X)" and "Domain X = Domain (choices X)"
proof-
from fin inf sv ex_good_choice obtain C
where "good_choice X C ∧ Domain X = Domain C"
by metis
then have "good_choice X (choices X) ∧ Domain X = Domain (choices X)"
unfolding choices_def by (rule someI)
then show "good_choice X (choices X)" and "Domain X = Domain (choices X)"
by simp_all
qed
lemma choices_ex:
assumes "(a, b) ∈ choices X"
shows "∃B. b ∈ B ∧ (a, B) ∈ X"
using good_choice_ab[OF _ assms] good_choice_choices .
lemma choices_inj:
assumes "(a⇩1, b⇩1) ∈ choices X" and "(a⇩2, b⇩2) ∈ choices X" and "a⇩1 ≠ a⇩2"
shows "b⇩1 ≠ b⇩2"
using good_choice_inj[OF good_choice_choices(1) assms] .
end