author | haftmann |
Tue, 07 Feb 2017 22:15:03 +0100 | |
changeset 64995 | a7af4045f873 |
parent 63343 | fb5d8a50c641 |
child 66453 | cc19f7ca2ed6 |
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 |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
3 |
Author: Andreas Lochbihler, ETH Zurich |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
6 |
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
|
7 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
|
60500 | 9 |
section \<open>Type of (at Most) Countable Sets\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
11 |
theory Countable_Set_Type |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
12 |
imports Countable_Set Cardinal_Notations Conditionally_Complete_Lattices |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
|
55070 | 15 |
|
60500 | 16 |
subsection\<open>Cardinal stuff\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
17 |
|
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
18 |
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
|
19 |
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
|
20 |
|
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
21 |
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
|
22 |
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
|
23 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
lemma countable_or_card_of: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
25 |
assumes "countable A" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
26 |
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
|
27 |
(infinite A \<and> |A| =o |UNIV::nat set| )" |
55070 | 28 |
by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq |
29 |
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
|
30 |
|
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
| (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
|
35 |
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
|
36 |
|
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
37 |
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
|
38 |
"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
|
39 |
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
|
40 |
|
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
49834
diff
changeset
|
41 |
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
|
42 |
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
|
43 |
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
|
44 |
| (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
|
45 |
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
|
46 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
lemma countable_ordLeq: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
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
|
49 |
shows "countable A" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
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
|
51 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
lemma countable_ordLess: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
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
|
54 |
shows "countable A" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
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
|
56 |
|
60500 | 57 |
subsection \<open>The type of countable sets\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
58 |
|
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
59 |
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
|
60 |
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
|
61 |
|
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
62 |
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
|
63 |
|
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
64 |
declare |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
65 |
rcset_inverse[simp] |
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
66 |
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
|
67 |
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
|
68 |
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
|
69 |
|
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
70 |
instantiation cset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
71 |
begin |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
72 |
|
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61952
diff
changeset
|
73 |
lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
74 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
75 |
lift_definition less_eq_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
76 |
is subset_eq parametric subset_transfer . |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
77 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
78 |
definition less_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
79 |
where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a cset)" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
80 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
81 |
lemma less_cset_transfer[transfer_rule]: |
63343 | 82 |
includes lifting_syntax |
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61952
diff
changeset
|
83 |
assumes [transfer_rule]: "bi_unique A" |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
84 |
shows "((pcr_cset A) ===> (pcr_cset A) ===> op =) op \<subset> op <" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
85 |
unfolding less_cset_def[abs_def] psubset_eq[abs_def] by transfer_prover |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
86 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
87 |
lift_definition sup_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
88 |
is union parametric union_transfer by simp |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
89 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
90 |
lift_definition inf_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
91 |
is inter parametric inter_transfer by simp |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
92 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
93 |
lift_definition minus_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
94 |
is minus parametric Diff_transfer by simp |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
95 |
|
60679 | 96 |
instance by standard (transfer; auto)+ |
97 |
||
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
98 |
end |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
99 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
100 |
abbreviation cempty :: "'a cset" where "cempty \<equiv> bot" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
101 |
abbreviation csubset_eq :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool" where "csubset_eq xs ys \<equiv> xs \<le> ys" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
102 |
abbreviation csubset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool" where "csubset xs ys \<equiv> xs < ys" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
103 |
abbreviation cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" where "cUn xs ys \<equiv> sup xs ys" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
104 |
abbreviation cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" where "cInt xs ys \<equiv> inf xs ys" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
105 |
abbreviation cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" where "cDiff xs ys \<equiv> minus xs ys" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
106 |
|
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
107 |
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
|
108 |
. |
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52662
diff
changeset
|
109 |
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
|
110 |
by (rule countable_insert) |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
111 |
abbreviation csingle :: "'a \<Rightarrow> 'a cset" where "csingle x \<equiv> cinsert x cempty" |
52662
c7cae5ce217d
use transfer/lifting for proving countable set and multisets being BNFs
traytel
parents:
52660
diff
changeset
|
112 |
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
|
113 |
by (rule countable_image) |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
114 |
lift_definition cBall :: "'a cset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer . |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
115 |
lift_definition cBex :: "'a cset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer . |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
116 |
lift_definition cUNION :: "'a cset \<Rightarrow> ('a \<Rightarrow> 'b cset) \<Rightarrow> 'b cset" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
117 |
is "UNION" parametric UNION_transfer by simp |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
118 |
definition cUnion :: "'a cset cset \<Rightarrow> 'a cset" where "cUnion A = cUNION A id" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
119 |
|
61952 | 120 |
lemma Union_conv_UNION: "\<Union>A = UNION A id" |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
121 |
by auto |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
122 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
123 |
lemma cUnion_transfer [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
124 |
"rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) Union cUnion" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62324
diff
changeset
|
125 |
proof - |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62324
diff
changeset
|
126 |
have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. UNION A id) (\<lambda>A. cUNION A id)" |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62324
diff
changeset
|
127 |
by transfer_prover |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62324
diff
changeset
|
128 |
then show ?thesis by (simp add: cUnion_def [symmetric]) |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62324
diff
changeset
|
129 |
qed |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
130 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
131 |
lemmas cset_eqI = set_eqI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
132 |
lemmas cset_eq_iff[no_atp] = set_eq_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
133 |
lemmas cBallI[intro!] = ballI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
134 |
lemmas cbspec[dest?] = bspec[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
135 |
lemmas cBallE[elim] = ballE[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
136 |
lemmas cBexI[intro] = bexI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
137 |
lemmas rev_cBexI[intro?] = rev_bexI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
138 |
lemmas cBexCI = bexCI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
139 |
lemmas cBexE[elim!] = bexE[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
140 |
lemmas cBall_triv[simp] = ball_triv[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
141 |
lemmas cBex_triv[simp] = bex_triv[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
142 |
lemmas cBex_triv_one_point1[simp] = bex_triv_one_point1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
143 |
lemmas cBex_triv_one_point2[simp] = bex_triv_one_point2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
144 |
lemmas cBex_one_point1[simp] = bex_one_point1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
145 |
lemmas cBex_one_point2[simp] = bex_one_point2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
146 |
lemmas cBall_one_point1[simp] = ball_one_point1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
147 |
lemmas cBall_one_point2[simp] = ball_one_point2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
148 |
lemmas cBall_conj_distrib = ball_conj_distrib[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
149 |
lemmas cBex_disj_distrib = bex_disj_distrib[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
150 |
lemmas cBall_cong = ball_cong[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
151 |
lemmas cBex_cong = bex_cong[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
152 |
lemmas csubsetI[intro!] = subsetI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
153 |
lemmas csubsetD[elim, intro?] = subsetD[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
154 |
lemmas rev_csubsetD[no_atp,intro?] = rev_subsetD[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
155 |
lemmas csubsetCE[no_atp,elim] = subsetCE[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
156 |
lemmas csubset_eq[no_atp] = subset_eq[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
157 |
lemmas contra_csubsetD[no_atp] = contra_subsetD[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
158 |
lemmas csubset_refl = subset_refl[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
159 |
lemmas csubset_trans = subset_trans[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
160 |
lemmas cset_rev_mp = set_rev_mp[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
161 |
lemmas cset_mp = set_mp[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
162 |
lemmas csubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
163 |
lemmas eq_cmem_trans = eq_mem_trans[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
164 |
lemmas csubset_antisym[intro!] = subset_antisym[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
165 |
lemmas cequalityD1 = equalityD1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
166 |
lemmas cequalityD2 = equalityD2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
167 |
lemmas cequalityE = equalityE[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
168 |
lemmas cequalityCE[elim] = equalityCE[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
169 |
lemmas eqcset_imp_iff = eqset_imp_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
170 |
lemmas eqcelem_imp_iff = eqelem_imp_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
171 |
lemmas cempty_iff[simp] = empty_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
172 |
lemmas cempty_fsubsetI[iff] = empty_subsetI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
173 |
lemmas equals_cemptyI = equals0I[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
174 |
lemmas equals_cemptyD = equals0D[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
175 |
lemmas cBall_cempty[simp] = ball_empty[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
176 |
lemmas cBex_cempty[simp] = bex_empty[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
177 |
lemmas cInt_iff[simp] = Int_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
178 |
lemmas cIntI[intro!] = IntI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
179 |
lemmas cIntD1 = IntD1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
180 |
lemmas cIntD2 = IntD2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
181 |
lemmas cIntE[elim!] = IntE[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
182 |
lemmas cUn_iff[simp] = Un_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
183 |
lemmas cUnI1[elim?] = UnI1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
184 |
lemmas cUnI2[elim?] = UnI2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
185 |
lemmas cUnCI[intro!] = UnCI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
186 |
lemmas cuUnE[elim!] = UnE[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
187 |
lemmas cDiff_iff[simp] = Diff_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
188 |
lemmas cDiffI[intro!] = DiffI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
189 |
lemmas cDiffD1 = DiffD1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
190 |
lemmas cDiffD2 = DiffD2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
191 |
lemmas cDiffE[elim!] = DiffE[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
192 |
lemmas cinsert_iff[simp] = insert_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
193 |
lemmas cinsertI1 = insertI1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
194 |
lemmas cinsertI2 = insertI2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
195 |
lemmas cinsertE[elim!] = insertE[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
196 |
lemmas cinsertCI[intro!] = insertCI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
197 |
lemmas csubset_cinsert_iff = subset_insert_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
198 |
lemmas cinsert_ident = insert_ident[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
199 |
lemmas csingletonI[intro!,no_atp] = singletonI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
200 |
lemmas csingletonD[dest!,no_atp] = singletonD[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
201 |
lemmas fsingletonE = csingletonD [elim_format] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
202 |
lemmas csingleton_iff = singleton_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
203 |
lemmas csingleton_inject[dest!] = singleton_inject[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
204 |
lemmas csingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
205 |
lemmas csingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
206 |
lemmas csubset_csingletonD = subset_singletonD[Transfer.transferred] |
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61952
diff
changeset
|
207 |
lemmas cDiff_single_cinsert = Diff_single_insert[Transfer.transferred] |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
208 |
lemmas cdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
209 |
lemmas cUn_csingleton_iff = Un_singleton_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
210 |
lemmas csingleton_cUn_iff = singleton_Un_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
211 |
lemmas cimage_eqI[simp, intro] = image_eqI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
212 |
lemmas cimageI = imageI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
213 |
lemmas rev_cimage_eqI = rev_image_eqI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
214 |
lemmas cimageE[elim!] = imageE[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
215 |
lemmas Compr_cimage_eq = Compr_image_eq[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
216 |
lemmas cimage_cUn = image_Un[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
217 |
lemmas cimage_iff = image_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
218 |
lemmas cimage_csubset_iff[no_atp] = image_subset_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
219 |
lemmas cimage_csubsetI = image_subsetI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
220 |
lemmas cimage_ident[simp] = image_ident[Transfer.transferred] |
62390 | 221 |
lemmas if_split_cin1 = if_split_mem1[Transfer.transferred] |
222 |
lemmas if_split_cin2 = if_split_mem2[Transfer.transferred] |
|
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
223 |
lemmas cpsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
224 |
lemmas cpsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
225 |
lemmas cpsubset_finsert_iff = psubset_insert_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
226 |
lemmas cpsubset_eq = psubset_eq[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
227 |
lemmas cpsubset_imp_fsubset = psubset_imp_subset[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
228 |
lemmas cpsubset_trans = psubset_trans[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
229 |
lemmas cpsubsetD = psubsetD[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
230 |
lemmas cpsubset_csubset_trans = psubset_subset_trans[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
231 |
lemmas csubset_cpsubset_trans = subset_psubset_trans[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
232 |
lemmas cpsubset_imp_ex_fmem = psubset_imp_ex_mem[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
233 |
lemmas csubset_cinsertI = subset_insertI[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
234 |
lemmas csubset_cinsertI2 = subset_insertI2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
235 |
lemmas csubset_cinsert = subset_insert[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
236 |
lemmas cUn_upper1 = Un_upper1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
237 |
lemmas cUn_upper2 = Un_upper2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
238 |
lemmas cUn_least = Un_least[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
239 |
lemmas cInt_lower1 = Int_lower1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
240 |
lemmas cInt_lower2 = Int_lower2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
241 |
lemmas cInt_greatest = Int_greatest[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
242 |
lemmas cDiff_csubset = Diff_subset[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
243 |
lemmas cDiff_csubset_conv = Diff_subset_conv[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
244 |
lemmas csubset_cempty[simp] = subset_empty[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
245 |
lemmas not_cpsubset_cempty[iff] = not_psubset_empty[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
246 |
lemmas cinsert_is_cUn = insert_is_Un[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
247 |
lemmas cinsert_not_cempty[simp] = insert_not_empty[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
248 |
lemmas cempty_not_cinsert = empty_not_insert[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
249 |
lemmas cinsert_absorb = insert_absorb[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
250 |
lemmas cinsert_absorb2[simp] = insert_absorb2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
251 |
lemmas cinsert_commute = insert_commute[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
252 |
lemmas cinsert_csubset[simp] = insert_subset[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
253 |
lemmas cinsert_cinter_cinsert[simp] = insert_inter_insert[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
254 |
lemmas cinsert_disjoint[simp,no_atp] = insert_disjoint[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
255 |
lemmas disjoint_cinsert[simp,no_atp] = disjoint_insert[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
256 |
lemmas cimage_cempty[simp] = image_empty[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
257 |
lemmas cimage_cinsert[simp] = image_insert[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
258 |
lemmas cimage_constant = image_constant[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
259 |
lemmas cimage_constant_conv = image_constant_conv[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
260 |
lemmas cimage_cimage = image_image[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
261 |
lemmas cinsert_cimage[simp] = insert_image[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
262 |
lemmas cimage_is_cempty[iff] = image_is_empty[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
263 |
lemmas cempty_is_cimage[iff] = empty_is_image[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
264 |
lemmas cimage_cong = image_cong[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
265 |
lemmas cimage_cInt_csubset = image_Int_subset[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
266 |
lemmas cimage_cDiff_csubset = image_diff_subset[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
267 |
lemmas cInt_absorb = Int_absorb[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
268 |
lemmas cInt_left_absorb = Int_left_absorb[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
269 |
lemmas cInt_commute = Int_commute[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
270 |
lemmas cInt_left_commute = Int_left_commute[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
271 |
lemmas cInt_assoc = Int_assoc[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
272 |
lemmas cInt_ac = Int_ac[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
273 |
lemmas cInt_absorb1 = Int_absorb1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
274 |
lemmas cInt_absorb2 = Int_absorb2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
275 |
lemmas cInt_cempty_left = Int_empty_left[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
276 |
lemmas cInt_cempty_right = Int_empty_right[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
277 |
lemmas disjoint_iff_cnot_equal = disjoint_iff_not_equal[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
278 |
lemmas cInt_cUn_distrib = Int_Un_distrib[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
279 |
lemmas cInt_cUn_distrib2 = Int_Un_distrib2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
280 |
lemmas cInt_csubset_iff[no_atp, simp] = Int_subset_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
281 |
lemmas cUn_absorb = Un_absorb[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
282 |
lemmas cUn_left_absorb = Un_left_absorb[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
283 |
lemmas cUn_commute = Un_commute[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
284 |
lemmas cUn_left_commute = Un_left_commute[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
285 |
lemmas cUn_assoc = Un_assoc[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
286 |
lemmas cUn_ac = Un_ac[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
287 |
lemmas cUn_absorb1 = Un_absorb1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
288 |
lemmas cUn_absorb2 = Un_absorb2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
289 |
lemmas cUn_cempty_left = Un_empty_left[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
290 |
lemmas cUn_cempty_right = Un_empty_right[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
291 |
lemmas cUn_cinsert_left[simp] = Un_insert_left[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
292 |
lemmas cUn_cinsert_right[simp] = Un_insert_right[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
293 |
lemmas cInt_cinsert_left = Int_insert_left[Transfer.transferred] |
59956 | 294 |
lemmas cInt_cinsert_left_if0[simp] = Int_insert_left_if0[Transfer.transferred] |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
295 |
lemmas cInt_cinsert_left_if1[simp] = Int_insert_left_if1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
296 |
lemmas cInt_cinsert_right = Int_insert_right[Transfer.transferred] |
59956 | 297 |
lemmas cInt_cinsert_right_if0[simp] = Int_insert_right_if0[Transfer.transferred] |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
298 |
lemmas cInt_cinsert_right_if1[simp] = Int_insert_right_if1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
299 |
lemmas cUn_cInt_distrib = Un_Int_distrib[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
300 |
lemmas cUn_cInt_distrib2 = Un_Int_distrib2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
301 |
lemmas cUn_cInt_crazy = Un_Int_crazy[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
302 |
lemmas csubset_cUn_eq = subset_Un_eq[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
303 |
lemmas cUn_cempty[iff] = Un_empty[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
304 |
lemmas cUn_csubset_iff[no_atp, simp] = Un_subset_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
305 |
lemmas cUn_cDiff_cInt = Un_Diff_Int[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
306 |
lemmas cDiff_cInt2 = Diff_Int2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
307 |
lemmas cUn_cInt_assoc_eq = Un_Int_assoc_eq[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
308 |
lemmas cBall_cUn = ball_Un[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
309 |
lemmas cBex_cUn = bex_Un[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
310 |
lemmas cDiff_eq_cempty_iff[simp,no_atp] = Diff_eq_empty_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
311 |
lemmas cDiff_cancel[simp] = Diff_cancel[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
312 |
lemmas cDiff_idemp[simp] = Diff_idemp[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
313 |
lemmas cDiff_triv = Diff_triv[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
314 |
lemmas cempty_cDiff[simp] = empty_Diff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
315 |
lemmas cDiff_cempty[simp] = Diff_empty[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
316 |
lemmas cDiff_cinsert0[simp,no_atp] = Diff_insert0[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
317 |
lemmas cDiff_cinsert = Diff_insert[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
318 |
lemmas cDiff_cinsert2 = Diff_insert2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
319 |
lemmas cinsert_cDiff_if = insert_Diff_if[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
320 |
lemmas cinsert_cDiff1[simp] = insert_Diff1[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
321 |
lemmas cinsert_cDiff_single[simp] = insert_Diff_single[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
322 |
lemmas cinsert_cDiff = insert_Diff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
323 |
lemmas cDiff_cinsert_absorb = Diff_insert_absorb[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
324 |
lemmas cDiff_disjoint[simp] = Diff_disjoint[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
325 |
lemmas cDiff_partition = Diff_partition[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
326 |
lemmas double_cDiff = double_diff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
327 |
lemmas cUn_cDiff_cancel[simp] = Un_Diff_cancel[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
328 |
lemmas cUn_cDiff_cancel2[simp] = Un_Diff_cancel2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
329 |
lemmas cDiff_cUn = Diff_Un[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
330 |
lemmas cDiff_cInt = Diff_Int[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
331 |
lemmas cUn_cDiff = Un_Diff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
332 |
lemmas cInt_cDiff = Int_Diff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
333 |
lemmas cDiff_cInt_distrib = Diff_Int_distrib[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
334 |
lemmas cDiff_cInt_distrib2 = Diff_Int_distrib2[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
335 |
lemmas cset_eq_csubset = set_eq_subset[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
336 |
lemmas csubset_iff[no_atp] = subset_iff[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
337 |
lemmas csubset_iff_pfsubset_eq = subset_iff_psubset_eq[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
338 |
lemmas all_not_cin_conv[simp] = all_not_in_conv[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
339 |
lemmas ex_cin_conv = ex_in_conv[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
340 |
lemmas cimage_mono = image_mono[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
341 |
lemmas cinsert_mono = insert_mono[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
342 |
lemmas cunion_mono = Un_mono[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
343 |
lemmas cinter_mono = Int_mono[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
344 |
lemmas cminus_mono = Diff_mono[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
345 |
lemmas cin_mono = in_mono[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
346 |
lemmas cLeast_mono = Least_mono[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
347 |
lemmas cequalityI = equalityI[Transfer.transferred] |
60059 | 348 |
lemmas cUN_iff [simp] = UN_iff[Transfer.transferred] |
349 |
lemmas cUN_I [intro] = UN_I[Transfer.transferred] |
|
350 |
lemmas cUN_E [elim!] = UN_E[Transfer.transferred] |
|
351 |
lemmas cUN_upper = UN_upper[Transfer.transferred] |
|
352 |
lemmas cUN_least = UN_least[Transfer.transferred] |
|
353 |
lemmas cUN_cinsert_distrib = UN_insert_distrib[Transfer.transferred] |
|
354 |
lemmas cUN_empty [simp] = UN_empty[Transfer.transferred] |
|
355 |
lemmas cUN_empty2 [simp] = UN_empty2[Transfer.transferred] |
|
356 |
lemmas cUN_absorb = UN_absorb[Transfer.transferred] |
|
357 |
lemmas cUN_cinsert [simp] = UN_insert[Transfer.transferred] |
|
358 |
lemmas cUN_cUn [simp] = UN_Un[Transfer.transferred] |
|
359 |
lemmas cUN_cUN_flatten = UN_UN_flatten[Transfer.transferred] |
|
360 |
lemmas cUN_csubset_iff = UN_subset_iff[Transfer.transferred] |
|
361 |
lemmas cUN_constant [simp] = UN_constant[Transfer.transferred] |
|
362 |
lemmas cimage_cUnion = image_Union[Transfer.transferred] |
|
363 |
lemmas cUNION_cempty_conv [simp] = UNION_empty_conv[Transfer.transferred] |
|
364 |
lemmas cBall_cUN = ball_UN[Transfer.transferred] |
|
365 |
lemmas cBex_cUN = bex_UN[Transfer.transferred] |
|
366 |
lemmas cUn_eq_cUN = Un_eq_UN[Transfer.transferred] |
|
367 |
lemmas cUN_mono = UN_mono[Transfer.transferred] |
|
368 |
lemmas cimage_cUN = image_UN[Transfer.transferred] |
|
369 |
lemmas cUN_csingleton [simp] = UN_singleton[Transfer.transferred] |
|
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
370 |
|
60500 | 371 |
subsection \<open>Additional lemmas\<close> |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
372 |
|
61585 | 373 |
subsubsection \<open>\<open>cempty\<close>\<close> |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
374 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
375 |
lemma cemptyE [elim!]: "cin a cempty \<Longrightarrow> P" by simp |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
376 |
|
61585 | 377 |
subsubsection \<open>\<open>cinsert\<close>\<close> |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
378 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
379 |
lemma countable_insert_iff: "countable (insert x A) \<longleftrightarrow> countable A" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
380 |
by (metis Diff_eq_empty_iff countable_empty countable_insert subset_insertI uncountable_minus_countable) |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
381 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
382 |
lemma set_cinsert: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
383 |
assumes "cin x A" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
384 |
obtains B where "A = cinsert x B" and "\<not> cin x B" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
385 |
using assms by transfer(erule Set.set_insert, simp add: countable_insert_iff) |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
386 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
387 |
lemma mk_disjoint_cinsert: "cin a A \<Longrightarrow> \<exists>B. A = cinsert a B \<and> \<not> cin a B" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
388 |
by (rule exI[where x = "cDiff A (csingle a)"]) blast |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
389 |
|
61585 | 390 |
subsubsection \<open>\<open>cimage\<close>\<close> |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
391 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
392 |
lemma subset_cimage_iff: "csubset_eq B (cimage f A) \<longleftrightarrow> (\<exists>AA. csubset_eq AA A \<and> B = cimage f AA)" |
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61952
diff
changeset
|
393 |
by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE) |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
394 |
|
60500 | 395 |
subsubsection \<open>bounded quantification\<close> |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
396 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
397 |
lemma cBex_simps [simp, no_atp]: |
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61952
diff
changeset
|
398 |
"\<And>A P Q. cBex A (\<lambda>x. P x \<and> Q) = (cBex A P \<and> Q)" |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
399 |
"\<And>A P Q. cBex A (\<lambda>x. P \<and> Q x) = (P \<and> cBex A Q)" |
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61952
diff
changeset
|
400 |
"\<And>P. cBex cempty P = False" |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
401 |
"\<And>a B P. cBex (cinsert a B) P = (P a \<or> cBex B P)" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
402 |
"\<And>A P f. cBex (cimage f A) P = cBex A (\<lambda>x. P (f x))" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
403 |
"\<And>A P. (\<not> cBex A P) = cBall A (\<lambda>x. \<not> P x)" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
404 |
by auto |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
405 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
406 |
lemma cBall_simps [simp, no_atp]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
407 |
"\<And>A P Q. cBall A (\<lambda>x. P x \<or> Q) = (cBall A P \<or> Q)" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
408 |
"\<And>A P Q. cBall A (\<lambda>x. P \<or> Q x) = (P \<or> cBall A Q)" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
409 |
"\<And>A P Q. cBall A (\<lambda>x. P \<longrightarrow> Q x) = (P \<longrightarrow> cBall A Q)" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
410 |
"\<And>A P Q. cBall A (\<lambda>x. P x \<longrightarrow> Q) = (cBex A P \<longrightarrow> Q)" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
411 |
"\<And>P. cBall cempty P = True" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
412 |
"\<And>a B P. cBall (cinsert a B) P = (P a \<and> cBall B P)" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
413 |
"\<And>A P f. cBall (cimage f A) P = cBall A (\<lambda>x. P (f x))" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
414 |
"\<And>A P. (\<not> cBall A P) = cBex A (\<lambda>x. \<not> P x)" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
415 |
by auto |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
416 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
417 |
lemma atomize_cBall: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
418 |
"(\<And>x. cin x A ==> P x) == Trueprop (cBall A (\<lambda>x. P x))" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
419 |
apply (simp only: atomize_all atomize_imp) |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
420 |
apply (rule equal_intr_rule) |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
421 |
by (transfer, simp)+ |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
422 |
|
60500 | 423 |
subsubsection \<open>@{const cUnion}\<close> |
60059 | 424 |
|
425 |
lemma cUNION_cimage: "cUNION (cimage f A) g = cUNION A (g \<circ> f)" |
|
426 |
including cset.lifting by transfer auto |
|
427 |
||
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
428 |
|
60500 | 429 |
subsection \<open>Setup for Lifting/Transfer\<close> |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
430 |
|
60500 | 431 |
subsubsection \<open>Relator and predicator properties\<close> |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
432 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
433 |
lift_definition rel_cset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
434 |
is rel_set parametric rel_set_transfer . |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
435 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
436 |
lemma rel_cset_alt_def: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
437 |
"rel_cset R a b \<longleftrightarrow> |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
438 |
(\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and> |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
439 |
(\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t)" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
440 |
by(simp add: rel_cset_def rel_set_def) |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
441 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
442 |
lemma rel_cset_iff: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
443 |
"rel_cset R a b \<longleftrightarrow> |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
444 |
(\<forall>t. cin t a \<longrightarrow> (\<exists>u. cin u b \<and> R t u)) \<and> |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
445 |
(\<forall>t. cin t b \<longrightarrow> (\<exists>u. cin u a \<and> R u t))" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
446 |
by transfer(auto simp add: rel_set_def) |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
447 |
|
60059 | 448 |
lemma rel_cset_cUNION: |
449 |
"\<lbrakk> rel_cset Q A B; rel_fun Q (rel_cset R) f g \<rbrakk> |
|
450 |
\<Longrightarrow> rel_cset R (cUNION A f) (cUNION B g)" |
|
451 |
unfolding rel_fun_def by transfer(erule rel_set_UNION, simp add: rel_fun_def) |
|
452 |
||
453 |
lemma rel_cset_csingle_iff [simp]: "rel_cset R (csingle x) (csingle y) \<longleftrightarrow> R x y" |
|
454 |
by transfer(auto simp add: rel_set_def) |
|
455 |
||
60500 | 456 |
subsubsection \<open>Transfer rules for the Transfer package\<close> |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
457 |
|
60500 | 458 |
text \<open>Unconditional transfer rules\<close> |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
459 |
|
63343 | 460 |
context includes lifting_syntax |
461 |
begin |
|
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
462 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
463 |
lemmas cempty_parametric [transfer_rule] = empty_transfer[Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
464 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
465 |
lemma cinsert_parametric [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
466 |
"(A ===> rel_cset A ===> rel_cset A) cinsert cinsert" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
467 |
unfolding rel_fun_def rel_cset_iff by blast |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
468 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
469 |
lemma cUn_parametric [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
470 |
"(rel_cset A ===> rel_cset A ===> rel_cset A) cUn cUn" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
471 |
unfolding rel_fun_def rel_cset_iff by blast |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
472 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
473 |
lemma cUnion_parametric [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
474 |
"(rel_cset (rel_cset A) ===> rel_cset A) cUnion cUnion" |
62372 | 475 |
unfolding rel_fun_def |
476 |
by transfer (auto simp: rel_set_def, metis+) |
|
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
477 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
478 |
lemma cimage_parametric [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
479 |
"((A ===> B) ===> rel_cset A ===> rel_cset B) cimage cimage" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
480 |
unfolding rel_fun_def rel_cset_iff by blast |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
481 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
482 |
lemma cBall_parametric [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
483 |
"(rel_cset A ===> (A ===> op =) ===> op =) cBall cBall" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
484 |
unfolding rel_cset_iff rel_fun_def by blast |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
485 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
486 |
lemma cBex_parametric [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
487 |
"(rel_cset A ===> (A ===> op =) ===> op =) cBex cBex" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
488 |
unfolding rel_cset_iff rel_fun_def by blast |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
489 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
490 |
lemma rel_cset_parametric [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
491 |
"((A ===> B ===> op =) ===> rel_cset A ===> rel_cset B ===> op =) rel_cset rel_cset" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
492 |
unfolding rel_fun_def |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
493 |
using rel_set_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred, where A = A and B = B] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
494 |
by simp |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
495 |
|
60500 | 496 |
text \<open>Rules requiring bi-unique, bi-total or right-total relations\<close> |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
497 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
498 |
lemma cin_parametric [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
499 |
"bi_unique A \<Longrightarrow> (A ===> rel_cset A ===> op =) cin cin" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
500 |
unfolding rel_fun_def rel_cset_iff bi_unique_def by metis |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
501 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
502 |
lemma cInt_parametric [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
503 |
"bi_unique A \<Longrightarrow> (rel_cset A ===> rel_cset A ===> rel_cset A) cInt cInt" |
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61952
diff
changeset
|
504 |
unfolding rel_fun_def |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
505 |
using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
506 |
by blast |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
507 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
508 |
lemma cDiff_parametric [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
509 |
"bi_unique A \<Longrightarrow> (rel_cset A ===> rel_cset A ===> rel_cset A) cDiff cDiff" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
510 |
unfolding rel_fun_def |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
511 |
using Diff_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
512 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
513 |
lemma csubset_parametric [transfer_rule]: |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
514 |
"bi_unique A \<Longrightarrow> (rel_cset A ===> rel_cset A ===> op =) csubset_eq csubset_eq" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
515 |
unfolding rel_fun_def |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
516 |
using subset_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
517 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
518 |
end |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
519 |
|
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
520 |
lifting_update cset.lifting |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
521 |
lifting_forget cset.lifting |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
522 |
|
60500 | 523 |
subsection \<open>Registration as BNF\<close> |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
524 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
525 |
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
|
526 |
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
|
527 |
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
|
528 |
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
|
529 |
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
|
530 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
531 |
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
|
532 |
"|{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
|
533 |
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
|
534 |
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
|
535 |
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
|
536 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
537 |
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
|
538 |
"|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
|
539 |
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
|
540 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
541 |
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
|
542 |
"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A" |
60679 | 543 |
apply (rule iffI) |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
544 |
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
|
545 |
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
|
546 |
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
|
547 |
apply assumption |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
548 |
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
|
549 |
apply (rule disjI1) |
60679 | 550 |
apply (erule finite_Collect_subsets) |
551 |
done |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
552 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
553 |
lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A" |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
554 |
including cset.lifting |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
555 |
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
|
556 |
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
|
557 |
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
|
558 |
done |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
559 |
|
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
560 |
lemma Collect_Int_Times: "{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}" |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
561 |
by auto |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
562 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
563 |
|
55934 | 564 |
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
|
565 |
"(\<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> |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
566 |
((BNF_Def.Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage fst))\<inverse>\<inverse> OO |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
567 |
BNF_Def.Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R") |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
568 |
proof |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
569 |
assume ?L |
63040 | 570 |
define R' where "R' = the_inv rcset (Collect (case_prod R) \<inter> (rcset a \<times> rcset b))" |
571 |
(is "_ = the_inv rcset ?L'") |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
572 |
have L: "countable ?L'" by auto |
55070 | 573 |
hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset) |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
574 |
thus ?R unfolding Grp_def relcompp.simps conversep.simps including cset.lifting |
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55075
diff
changeset
|
575 |
proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) |
60500 | 576 |
from * \<open>?L\<close> show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times) |
577 |
from * \<open>?L\<close> show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times) |
|
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
578 |
qed simp_all |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
579 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
580 |
assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
581 |
by (simp add: subset_eq Ball_def)(transfer, auto simp add: cimage.rep_eq, metis snd_conv, metis fst_conv) |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
582 |
qed |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
583 |
|
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
584 |
bnf "'a cset" |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
585 |
map: cimage |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
586 |
sets: rcset |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
587 |
bd: natLeq |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
588 |
wits: "cempty" |
55934 | 589 |
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
|
590 |
proof - |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
591 |
show "cimage id = id" by auto |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
592 |
next |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
593 |
fix f g show "cimage (g \<circ> f) = cimage g \<circ> cimage f" by fastforce |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
594 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
595 |
fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a" |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
596 |
thus "cimage f C = cimage g C" including cset.lifting by transfer force |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
597 |
next |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
598 |
fix f show "rcset \<circ> cimage f = op ` f \<circ> rcset" including cset.lifting by transfer' fastforce |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
599 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
600 |
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
|
601 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
602 |
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
|
603 |
next |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
604 |
fix C show "|rcset C| \<le>o natLeq" |
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
605 |
including cset.lifting by transfer (unfold countable_card_le_natLeq) |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
606 |
next |
54841
af71b753c459
express weak pullback property of bnfs only in terms of the relator
traytel
parents:
54539
diff
changeset
|
607 |
fix R S |
55934 | 608 |
show "rel_cset R OO rel_cset S \<le> rel_cset (R OO S)" |
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
609 |
unfolding rel_cset_alt_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
|
610 |
next |
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
611 |
fix R |
62324 | 612 |
show "rel_cset R = (\<lambda>x y. \<exists>z. rcset z \<subseteq> {(x, y). R x y} \<and> |
613 |
cimage fst z = x \<and> cimage snd z = y)" |
|
614 |
unfolding rel_cset_alt_def[abs_def] rel_cset_aux[unfolded OO_Grp_alt] by simp |
|
59954
5ee7e9721eac
more lemmas and operations on cset (adapted from FSet)
Andreas Lochbihler
parents:
58881
diff
changeset
|
615 |
qed(simp add: bot_cset.rep_eq) |
54539
bbab2ebda234
move registration of countable set type as BNF to its own theory file (+ renamed theory)
blanchet
parents:
53013
diff
changeset
|
616 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
617 |
end |