author | blanchet |
Sun, 04 May 2014 18:14:58 +0200 | |
changeset 56846 | 9df717fef2bb |
parent 55934 | 800e155d051a |
child 57398 | 882091eb1e9a |
permissions | -rw-r--r-- |
55075 | 1 |
(* Title: HOL/Library/Countable_Set_Type.thy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Andrei Popescu, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
5 |
Type of (at most) countable sets. |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
8 |
header {* Type of (at Most) Countable Sets *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
10 |
theory Countable_Set_Type |
55075 | 11 |
imports Countable_Set Cardinal_Notations |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
|
55070 | 14 |
abbreviation "Grp \<equiv> BNF_Util.Grp" |
15 |
||
16 |
||
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
17 |
subsection{* Cardinal stuff *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
|
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
19 |
lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|" |
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
20 |
unfolding countable_def card_of_ordLeq[symmetric] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
|
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
22 |
lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq" |
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
23 |
unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
25 |
lemma countable_or_card_of: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
26 |
assumes "countable A" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
(infinite A \<and> |A| =o |UNIV::nat set| )" |
55070 | 29 |
by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq |
30 |
ordLeq_iff_ordLess_or_ordIso) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
|
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
32 |
lemma countable_cases_card_of[elim]: |
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
33 |
assumes "countable A" |
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
34 |
obtains (Fin) "finite A" "|A| <o |UNIV::nat set|" |
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
35 |
| (Inf) "infinite A" "|A| =o |UNIV::nat set|" |
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
36 |
using assms countable_or_card_of by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
37 |
|
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
38 |
lemma countable_or: |
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
39 |
"countable A \<Longrightarrow> (\<exists> f::'a\<Rightarrow>nat. finite A \<and> inj_on f A) \<or> (\<exists> f::'a\<Rightarrow>nat. infinite A \<and> bij_betw f A UNIV)" |
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
40 |
by (elim countable_enum_cases) fastforce+ |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
41 |
|
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
42 |
lemma countable_cases[elim]: |
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
43 |
assumes "countable A" |
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
44 |
obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A" |
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
45 |
| (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV" |
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
46 |
using assms countable_or by metis |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
lemma countable_ordLeq: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
49 |
assumes "|A| \<le>o |B|" and "countable B" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
shows "countable A" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
51 |
using assms unfolding countable_card_of_nat by(rule ordLeq_transitive) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
lemma countable_ordLess: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
54 |
assumes AB: "|A| <o |B|" and B: "countable B" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
shows "countable A" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
58 |
subsection {* The type of countable sets *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
59 |
|
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
60 |
typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
61 |
by (rule exI[of _ "{}"]) simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
62 |
|
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
63 |
setup_lifting type_definition_cset |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
|
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
65 |
declare |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
66 |
rcset_inverse[simp] |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
67 |
acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp] |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
68 |
acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp] |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
69 |
rcset[Transfer.transferred, unfolded mem_Collect_eq, simp] |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
70 |
|
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
71 |
lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer |
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset
|
72 |
. |
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
73 |
lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
74 |
by (rule countable_empty) |
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52662
diff
changeset
|
75 |
lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer |
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
76 |
by (rule countable_insert) |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
77 |
lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}" |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
78 |
by (rule countable_insert[OF countable_empty]) |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
79 |
lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
80 |
by (rule countable_Un) |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
81 |
lift_definition cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<inter>" parametric inter_transfer |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
82 |
by (rule countable_Int1) |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
83 |
lift_definition cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op -" parametric Diff_transfer |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
84 |
by (rule countable_Diff) |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
85 |
lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
86 |
by (rule countable_image) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
88 |
subsection {* Registration as BNF *} |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
89 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
90 |
lemma card_of_countable_sets_range: |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
91 |
fixes A :: "'a set" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
92 |
shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
93 |
apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
94 |
unfolding inj_on_def by auto |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
95 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
96 |
lemma card_of_countable_sets_Func: |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
97 |
"|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
98 |
using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric] |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
99 |
unfolding cexp_def Field_natLeq Field_card_of |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
100 |
by (rule ordLeq_ordIso_trans) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
101 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
102 |
lemma ordLeq_countable_subsets: |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
103 |
"|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
104 |
apply (rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
105 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
106 |
lemma finite_countable_subset: |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
107 |
"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
108 |
apply default |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
109 |
apply (erule contrapos_pp) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
110 |
apply (rule card_of_ordLeq_infinite) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
111 |
apply (rule ordLeq_countable_subsets) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
112 |
apply assumption |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
113 |
apply (rule finite_Collect_conjI) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
114 |
apply (rule disjI1) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
115 |
by (erule finite_Collect_subsets) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
116 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
117 |
lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
118 |
apply (rule f_the_inv_into_f[unfolded inj_on_def image_iff]) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
119 |
apply transfer' apply simp |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
120 |
apply transfer' apply simp |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
121 |
done |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
122 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
123 |
lemma Collect_Int_Times: |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
124 |
"{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
125 |
by auto |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
126 |
|
55934 | 127 |
definition rel_cset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where |
128 |
"rel_cset R a b \<longleftrightarrow> |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
129 |
(\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and> |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
130 |
(\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t)" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
131 |
|
55934 | 132 |
lemma rel_cset_aux: |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
133 |
"(\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and> (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t) \<longleftrightarrow> |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
134 |
((Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage fst))\<inverse>\<inverse> OO |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
135 |
Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R") |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
136 |
proof |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
137 |
assume ?L |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
138 |
def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
139 |
(is "the_inv rcset ?L'") |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
140 |
have L: "countable ?L'" by auto |
55070 | 141 |
hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset) |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
142 |
thus ?R unfolding Grp_def relcompp.simps conversep.simps |
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55075
diff
changeset
|
143 |
proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
144 |
from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
145 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
146 |
from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
147 |
qed simp_all |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
148 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
149 |
assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
150 |
by transfer force |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
151 |
qed |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
152 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
153 |
bnf "'a cset" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
154 |
map: cimage |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
155 |
sets: rcset |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
156 |
bd: natLeq |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
157 |
wits: "cempty" |
55934 | 158 |
rel: rel_cset |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
159 |
proof - |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
160 |
show "cimage id = id" by transfer' simp |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
161 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
162 |
fix f g show "cimage (g \<circ> f) = cimage g \<circ> cimage f" by transfer' fastforce |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
163 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
164 |
fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
165 |
thus "cimage f C = cimage g C" by transfer force |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
166 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
167 |
fix f show "rcset \<circ> cimage f = op ` f \<circ> rcset" by transfer' fastforce |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
168 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
169 |
show "card_order natLeq" by (rule natLeq_card_order) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
170 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
171 |
show "cinfinite natLeq" by (rule natLeq_cinfinite) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
172 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
173 |
fix C show "|rcset C| \<le>o natLeq" by transfer (unfold countable_card_le_natLeq) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
174 |
next |
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54539
diff
changeset
|
175 |
fix R S |
55934 | 176 |
show "rel_cset R OO rel_cset S \<le> rel_cset (R OO S)" |
177 |
unfolding rel_cset_def[abs_def] by fast |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
178 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
179 |
fix R |
55934 | 180 |
show "rel_cset R = |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
181 |
(Grp {x. rcset x \<subseteq> Collect (split R)} (cimage fst))\<inverse>\<inverse> OO |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
182 |
Grp {x. rcset x \<subseteq> Collect (split R)} (cimage snd)" |
55934 | 183 |
unfolding rel_cset_def[abs_def] rel_cset_aux by simp |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
184 |
qed (transfer, simp) |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
185 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
186 |
end |