equal
deleted
inserted
replaced
9 |
9 |
10 theory Countable_Type |
10 theory Countable_Type |
11 imports |
11 imports |
12 "~~/src/HOL/Cardinals/Cardinals" |
12 "~~/src/HOL/Cardinals/Cardinals" |
13 "~~/src/HOL/Library/Countable_Set" |
13 "~~/src/HOL/Library/Countable_Set" |
14 "~~/src/HOL/Library/Quotient_Set" |
|
15 begin |
14 begin |
16 |
15 |
17 subsection{* Cardinal stuff *} |
16 subsection{* Cardinal stuff *} |
18 |
17 |
19 lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|" |
18 lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|" |
74 |
73 |
75 lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer |
74 lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer |
76 .. |
75 .. |
77 lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer |
76 lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer |
78 by (rule countable_empty) |
77 by (rule countable_empty) |
79 lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric insert_transfer |
78 lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer |
80 by (rule countable_insert) |
79 by (rule countable_insert) |
81 lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}" |
80 lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}" |
82 by (rule countable_insert[OF countable_empty]) |
81 by (rule countable_insert[OF countable_empty]) |
83 lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer |
82 lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer |
84 by (rule countable_Un) |
83 by (rule countable_Un) |