diff --git a/thys/ZFC_in_HOL/ZFC_Typeclasses.thy b/thys/ZFC_in_HOL/ZFC_Typeclasses.thy
--- a/thys/ZFC_in_HOL/ZFC_Typeclasses.thy
+++ b/thys/ZFC_in_HOL/ZFC_Typeclasses.thy
@@ -1,291 +1,329 @@
section \Type Classes for ZFC\
theory ZFC_Typeclasses
- imports ZFC_Cardinals
+ imports ZFC_Cardinals Complex_Main
begin
subsection\The class of embeddable types\
class embeddable =
assumes ex_inj: "\V_of :: 'a \ V. inj V_of"
context countable
begin
subclass embeddable
proof -
have "inj (ord_of_nat \ to_nat)" if "inj to_nat"
for to_nat :: "'a \ nat"
using that by (simp add: inj_compose inj_ord_of_nat)
then show "class.embeddable TYPE('a)"
by intro_classes (meson local.ex_inj)
qed
end
instance unit :: embeddable ..
instance bool :: embeddable ..
instance nat :: embeddable ..
instance int :: embeddable ..
instance rat :: embeddable ..
instance char :: embeddable ..
instance String.literal :: embeddable ..
instance typerep :: embeddable ..
lemma embeddable_classI:
fixes f :: "'a \ V"
assumes "\x y. f x = f y \ x = y"
shows "OFCLASS('a, embeddable_class)"
proof (intro_classes, rule exI)
show "inj f"
by (rule injI [OF assms]) assumption
qed
instance V :: embeddable
by (rule embeddable_classI [where f=id]) auto
instance prod :: (embeddable,embeddable) embeddable
proof -
have "inj (\(x,y). \V_of1 x, V_of2 y\)" if "inj V_of1" "inj V_of2"
for V_of1 :: "'a \ V" and V_of2 :: "'b \ V"
using that by (auto simp: inj_on_def)
then show "OFCLASS('a \ 'b, embeddable_class)"
by intro_classes (meson embeddable_class.ex_inj)
qed
instance sum :: (embeddable,embeddable) embeddable
proof -
have "inj (case_sum (Inl \ V_of1) (Inr \ V_of2))" if "inj V_of1" "inj V_of2"
for V_of1 :: "'a \ V" and V_of2 :: "'b \ V"
using that by (auto simp: inj_on_def split: sum.split_asm)
then show "OFCLASS('a + 'b, embeddable_class)"
by intro_classes (meson embeddable_class.ex_inj)
qed
instance option :: (embeddable) embeddable
proof -
- have "inj (case_option 0 (\x. set{V_of x}))" if "inj V_of"
+ have "inj (case_option 0 (\x. ZFC_in_HOL.set{V_of x}))" if "inj V_of"
for V_of :: "'a \ V"
using that by (auto simp: inj_on_def split: option.split_asm)
then show "OFCLASS('a option, embeddable_class)"
by intro_classes (meson embeddable_class.ex_inj)
qed
primrec V_of_list where
"V_of_list V_of Nil = 0"
| "V_of_list V_of (x#xs) = \V_of x, V_of_list V_of xs\"
lemma inj_V_of_list:
assumes "inj V_of"
shows "inj (V_of_list V_of)"
proof -
note inj_eq [OF assms, simp]
have "x = y" if "V_of_list V_of x = V_of_list V_of y" for x y
using that
proof (induction x arbitrary: y)
case Nil
then show ?case
by (cases y) auto
next
case (Cons a x)
then show ?case
by (cases y) auto
qed
then show ?thesis
by (auto simp: inj_on_def)
qed
instance list :: (embeddable) embeddable
proof -
have "inj (rec_list 0 (\x xs r. \V_of x, r\))" (is "inj ?f")
if V_of: "inj V_of" for V_of :: "'a \ V"
proof -
note inj_eq [OF V_of, simp]
have "x = y" if "?f x = ?f y" for x y
using that
proof (induction x arbitrary: y)
case Nil
then show ?case
by (cases y) auto
next
case (Cons a x)
then show ?case
by (cases y) auto
qed
then show ?thesis
by (auto simp: inj_on_def)
qed
then show "OFCLASS('a list, embeddable_class)"
by intro_classes (meson embeddable_class.ex_inj)
qed
subsection\The class of small types\
class small =
assumes small: "small (UNIV::'a set)"
begin
subclass embeddable
by intro_classes (meson local.small small_def)
+lemma TC_small [iff]:
+ fixes A :: "'a set"
+ shows "small A"
+ using small smaller_than_small by blast
+
end
context countable
begin
subclass small
proof -
have *: "inj (ord_of_nat \ to_nat)" if "inj to_nat"
for to_nat :: "'a \ nat"
using that by (simp add: inj_compose inj_ord_of_nat)
then show "class.small TYPE('a)"
by intro_classes (metis small_image_nat local.ex_inj the_inv_into_onto)
qed
end
lemma lepoll_UNIV_imp_small: "X \ (UNIV::'a::small set) \ small X"
by (meson lepoll_iff replacement small smaller_than_small)
lemma lepoll_imp_small:
fixes A :: "'a::small set"
assumes "X \ A"
shows "small X"
by (metis lepoll_UNIV_imp_small UNIV_I assms lepoll_def subsetI)
instance unit :: small ..
instance bool :: small ..
instance nat :: small ..
instance int :: small ..
instance rat :: small ..
instance char :: small ..
instance String.literal :: small ..
instance typerep :: small ..
instance prod :: (small,small) small
proof -
have "inj (\(x,y). \V_of1 x, V_of2 y\)"
"range (\(x,y). \V_of1 x, V_of2 y\) \ elts (VSigma A (\x. B))"
if "inj V_of1" "inj V_of2" "range V_of1 \ elts A" "range V_of2 \ elts B"
for V_of1 :: "'a \ V" and V_of2 :: "'b \ V" and A B
using that by (auto simp: inj_on_def)
with small [where 'a='a] small [where 'a='b]
show "OFCLASS('a \ 'b, small_class)"
apply intro_classes
- apply (clarsimp simp add: small_def)
+ unfolding small_def
+ apply clarify
by (metis down_raw dual_order.refl)
qed
instance sum :: (small,small) small
proof -
have "inj (case_sum (Inl \ V_of1) (Inr \ V_of2))"
"range (case_sum (Inl \ V_of1) (Inr \ V_of2)) \ elts (A \ B)"
if "inj V_of1" "inj V_of2" "range V_of1 \ elts A" "range V_of2 \ elts B"
for V_of1 :: "'a \ V" and V_of2 :: "'b \ V" and A B
using that by (force simp: inj_on_def split: sum.split)+
with small [where 'a='a] small [where 'a='b]
show "OFCLASS('a + 'b, small_class)"
apply intro_classes
- apply (clarsimp simp add: small_def)
+ unfolding small_def
+ apply clarify
by (metis down_raw dual_order.refl)
qed
instance option :: (small) small
proof -
- have "inj (\x. case x of None \ 0 | Some x \ set {V_of x})"
- "range (\x. case x of None \ 0 | Some x \ set {V_of x}) \ insert 0 (elts (VPow A))"
+ have "inj (\x. case x of None \ 0 | Some x \ ZFC_in_HOL.set {V_of x})"
+ "range (\x. case x of None \ 0 | Some x \ ZFC_in_HOL.set {V_of x}) \ insert 0 (elts (VPow A))"
if "inj V_of" "range V_of \ elts A"
for V_of :: "'a \ V" and A
using that by (auto simp: inj_on_def split: option.split_asm)
with small [where 'a='a]
show "OFCLASS('a option, small_class)"
apply intro_classes
- apply (clarsimp simp add: small_def)
+ unfolding small_def
+ apply clarify
by (metis down_raw elts_vinsert subset_insertI)
qed
instance list :: (small) small
proof -
have "small (range (V_of_list V_of))"
if "inj V_of" "range V_of \ elts A"
for V_of :: "'a \ V" and A
proof -
have "range (V_of_list V_of) \ (UNIV :: 'a list set)"
using that by (simp add: inj_V_of_list)
also have "\ \ lists (UNIV :: 'a set)"
by simp
also have "\ \ (UNIV :: 'a set) \ (UNIV :: nat set)"
proof (cases "finite (range (V_of::'a \ V))")
case True
then have "lists (UNIV :: 'a set) \ (UNIV :: nat set)"
using countable_iff_lepoll countable_image_inj_on that(1) uncountable_infinite by blast
then show ?thesis
by (blast intro: lepoll_trans [OF _ lepoll_times2])
next
case False
then have "lists (UNIV :: 'a set) \ (UNIV :: 'a set)"
using \infinite (range V_of)\ eqpoll_imp_lepoll infinite_eqpoll_lists by blast
then show ?thesis
using lepoll_times1 lepoll_trans by fastforce
qed
finally show ?thesis
by (simp add: lepoll_imp_small)
qed
with small [where 'a='a]
show "OFCLASS('a list, small_class)"
apply intro_classes
- apply (clarsimp simp add: small_def)
+ unfolding small_def
+ apply clarify
by (metis inj_V_of_list order_refl small_def small_iff_range)
qed
instance "fun" :: (small,embeddable) embeddable
proof -
have "inj (\f. VLambda A (\x. V_of2 (f (inv V_of1 x))))"
if *: "inj V_of1" "inj V_of2" "range V_of1 \ elts A"
for V_of1 :: "'a \ V" and V_of2 :: "'b \ V" and A
proof -
have "f u = f' u"
if "VLambda A (\u. V_of2 (f (inv V_of1 u))) = VLambda A (\x. V_of2 (f' (inv V_of1 x)))"
for f f' :: "'a \ 'b" and u
by (metis inv_f_f rangeI subsetD VLambda_eq_D2 [OF that, of "V_of1 u"] *)
then show ?thesis
by (auto simp: inj_on_def)
qed
then show "OFCLASS('a \ 'b, embeddable_class)"
by intro_classes (metis embeddable_class.ex_inj small order_refl replacement small_iff)
qed
instance "fun" :: (small,small) small
proof -
have "inj (\f. VLambda A (\x. V_of2 (f (inv V_of1 x))))" (is "inj ?\")
"range (\f. VLambda A (\x. V_of2 (f (inv V_of1 x)))) \ elts (VPi A (\x. B))"
if *: "inj V_of1" "inj V_of2" "range V_of1 \ elts A" and "range V_of2 \ elts B"
for V_of1 :: "'a \ V" and V_of2 :: "'b \ V" and A B
proof -
have "f u = f' u"
if "VLambda A (\u. V_of2 (f (inv V_of1 u))) = VLambda A (\x. V_of2 (f' (inv V_of1 x)))"
for f f' :: "'a \ 'b" and u
by (metis inv_f_f rangeI subsetD VLambda_eq_D2 [OF that, of "V_of1 u"] *)
then show "inj ?\"
by (auto simp: inj_on_def)
show "range ?\ \ elts (VPi A (\x. B))"
using that by (simp add: VPi_I subset_eq)
qed
with small [where 'a='a] small [where 'a='b]
show "OFCLASS('a \ 'b, small_class)"
apply intro_classes
- apply (clarsimp simp add: small_def)
+ unfolding small_def
+ apply clarify
by (metis down_raw dual_order.refl)
qed
-lemma TC_small [iff]:
- fixes A :: "'a::small set"
- shows "small A"
- using small smaller_than_small by blast
+instance set :: (small) small
+proof -
+ have 1: "inj (\x. ZFC_in_HOL.set (V_of ` x))"
+ if "inj V_of" for V_of :: "'a \ V"
+ by (simp add: inj_on_def inj_image_eq_iff [OF that])
+ have 2: "range (\x. ZFC_in_HOL.set (V_of ` x)) \ elts (VPow A)"
+ if "range V_of \ elts A" for V_of :: "'a \ V" and A
+ using that by (auto simp: inj_on_def image_subset_iff)
+ from small [where 'a='a]
+ show "OFCLASS('a set, small_class)"
+ apply intro_classes
+ unfolding small_def
+ apply clarify
+ by (metis 1 2 down_raw subsetI)
+qed
+
+instance real :: small
+proof -
+ have "small (range (Rep_real))"
+ by simp
+ then show "OFCLASS(real, small_class)"
+ by intro_classes (metis Rep_real_inverse image_inv_f_f inj_on_def replacement)
+qed
+
+instance complex :: small
+proof -
+ have "\c. c \ range (\(x,y). Complex x y)"
+ by (metis case_prod_conv complex.exhaust_sel rangeI)
+ then show "OFCLASS(complex, small_class)"
+ by intro_classes (meson TC_small replacement smaller_than_small subset_eq)
+qed
+
end