Theory Finitely_Bounded_Set_Counterexample
section ‹Sets Bounded by a Finite Cardinal $>2$ Are Not BNFs›
theory Finitely_Bounded_Set_Counterexample
imports
"HOL-Cardinals.Cardinals"
begin
text ‹Do not import this theory. It contains an inconsistent axiomatization.
The point is to exhibit the particular inconsistency.›
typedef ('a, 'k) bset ("_ set[_]" [22, 21] 21) =
"{A :: 'a set. |A| <o |UNIV :: 'k set|}"
morphisms set_bset Abs_bset
by (rule exI[of _ "{}"]) (auto simp: card_of_empty4 csum_def)
setup_lifting type_definition_bset
lift_definition map_bset ::
"('a ⇒ 'b) ⇒ 'a set['k] ⇒ 'b set['k]" is image
using card_of_image ordLeq_ordLess_trans by blast
inductive rel_bset :: "('a ⇒ 'b ⇒ bool) ⇒ ('a, 'k) bset ⇒ ('b, 'k) bset ⇒ bool" for R where
"set_bset x ⊆ {(x, y). R x y} ⟹ rel_bset R (map_bset fst x) (map_bset snd x)"
text ‹
We axiomatize the relator commutation property and show that we can deduce @{term False} from it.
We cannot do this with a locale, since we need the fully polymorphic version of the following axiom.
›
axiomatization where
inconsistent: "rel_bset R1 OO rel_bset R2 ≤ rel_bset (R1 OO R2)"
bnf "('a, 'k) bset"
map: map_bset
sets: set_bset
bd: "natLeq +c card_suc ( |UNIV :: 'k set| )"
rel: rel_bset
proof (standard, goal_cases)
case 1 then show ?case
by transfer simp
next
case 2 then show ?case
apply (rule ext)
apply transfer
apply auto
done
next
case 3 then show ?case
apply transfer
apply (auto simp: image_iff)
done
next
case 4 then show ?case
apply (rule ext)
apply transfer
apply simp
done
next
case 5 then show ?case by (rule card_order_bd_fun)
next
case 6 then show ?case by (rule Cinfinite_bd_fun[THEN conjunct1])
next
case 7 then show ?case by (rule regularCard_bd_fun)
next
case 8 then show ?case
by transfer
(erule ordLess_ordLeq_trans[OF _ ordLeq_transitive[OF _ ordLeq_csum2]];
simp add: card_suc_greater ordLess_imp_ordLeq Card_order_card_suc)
next
case 9 then show ?case by (rule inconsistent)
next
case 10 then show ?case
by (auto simp: fun_eq_iff intro: rel_bset.intros elim: rel_bset.cases)
qed
lemma card_option_finite[simp]:
assumes "finite (UNIV :: 'k set)"
shows "card (UNIV :: 'k option set) = Suc (card (UNIV :: 'k set))"
(is "card ?L = Suc (card ?R)")
proof -
have "card ?L = Suc (card (?L - {None}))" by (rule card.remove) (auto simp: assms)
also have "card (?L - {None}) = card ?R"
by (rule bij_betw_same_card[of the])
(auto simp: bij_betw_def inj_on_def image_iff intro!: bexI[of _ "Some x" for x])
finally show ?thesis .
qed