66563
|
1 |
(* Title: HOL/Library/Uprod.thy
|
|
2 |
Author: Andreas Lochbihler, ETH Zurich *)
|
|
3 |
|
|
4 |
section \<open>Unordered pairs\<close>
|
|
5 |
|
|
6 |
theory Uprod imports Main begin
|
|
7 |
|
|
8 |
typedef ('a, 'b) commute = "{f :: 'a \<Rightarrow> 'a \<Rightarrow> 'b. \<forall>x y. f x y = f y x}"
|
|
9 |
morphisms apply_commute Abs_commute
|
|
10 |
by auto
|
|
11 |
|
|
12 |
setup_lifting type_definition_commute
|
|
13 |
|
|
14 |
lemma apply_commute_commute: "apply_commute f x y = apply_commute f y x"
|
|
15 |
by(transfer) simp
|
|
16 |
|
|
17 |
context includes lifting_syntax begin
|
|
18 |
|
|
19 |
lift_definition rel_commute :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a, 'c) commute \<Rightarrow> ('b, 'd) commute \<Rightarrow> bool"
|
|
20 |
is "\<lambda>A B. A ===> A ===> B" .
|
|
21 |
|
|
22 |
end
|
|
23 |
|
|
24 |
definition eq_upair :: "('a \<times> 'a) \<Rightarrow> ('a \<times> 'a) \<Rightarrow> bool"
|
|
25 |
where "eq_upair = (\<lambda>(a, b) (c, d). a = c \<and> b = d \<or> a = d \<and> b = c)"
|
|
26 |
|
|
27 |
lemma eq_upair_simps [simp]:
|
|
28 |
"eq_upair (a, b) (c, d) \<longleftrightarrow> a = c \<and> b = d \<or> a = d \<and> b = c"
|
|
29 |
by(simp add: eq_upair_def)
|
|
30 |
|
|
31 |
lemma equivp_eq_upair: "equivp eq_upair"
|
|
32 |
by(auto simp add: equivp_def fun_eq_iff)
|
|
33 |
|
|
34 |
quotient_type 'a uprod = "'a \<times> 'a" / eq_upair by(rule equivp_eq_upair)
|
|
35 |
|
|
36 |
lift_definition Upair :: "'a \<Rightarrow> 'a \<Rightarrow> 'a uprod" is Pair parametric Pair_transfer[of "A" "A" for A] .
|
|
37 |
|
|
38 |
lemma uprod_exhaust [case_names Upair, cases type: uprod]:
|
|
39 |
obtains a b where "x = Upair a b"
|
|
40 |
by transfer fastforce
|
|
41 |
|
|
42 |
lemma Upair_inject [simp]: "Upair a b = Upair c d \<longleftrightarrow> a = c \<and> b = d \<or> a = d \<and> b = c"
|
|
43 |
by transfer auto
|
|
44 |
|
|
45 |
code_datatype Upair
|
|
46 |
|
|
47 |
lift_definition case_uprod :: "('a, 'b) commute \<Rightarrow> 'a uprod \<Rightarrow> 'b" is case_prod
|
|
48 |
parametric case_prod_transfer[of A A for A] by auto
|
|
49 |
|
|
50 |
lemma case_uprod_simps [simp, code]: "case_uprod f (Upair x y) = apply_commute f x y"
|
|
51 |
by transfer auto
|
|
52 |
|
|
53 |
lemma uprod_split: "P (case_uprod f x) \<longleftrightarrow> (\<forall>a b. x = Upair a b \<longrightarrow> P (apply_commute f a b))"
|
|
54 |
by transfer auto
|
|
55 |
|
|
56 |
lemma uprod_split_asm: "P (case_uprod f x) \<longleftrightarrow> \<not> (\<exists>a b. x = Upair a b \<and> \<not> P (apply_commute f a b))"
|
|
57 |
by transfer auto
|
|
58 |
|
67399
|
59 |
lift_definition not_equal :: "('a, bool) commute" is "(\<noteq>)" by auto
|
66563
|
60 |
|
|
61 |
lemma apply_not_equal [simp]: "apply_commute not_equal x y \<longleftrightarrow> x \<noteq> y"
|
|
62 |
by transfer simp
|
|
63 |
|
|
64 |
definition proper_uprod :: "'a uprod \<Rightarrow> bool"
|
|
65 |
where "proper_uprod = case_uprod not_equal"
|
|
66 |
|
|
67 |
lemma proper_uprod_simps [simp, code]: "proper_uprod (Upair x y) \<longleftrightarrow> x \<noteq> y"
|
|
68 |
by(simp add: proper_uprod_def)
|
|
69 |
|
|
70 |
context includes lifting_syntax begin
|
|
71 |
|
|
72 |
private lemma set_uprod_parametric':
|
|
73 |
"(rel_prod A A ===> rel_set A) (\<lambda>(a, b). {a, b}) (\<lambda>(a, b). {a, b})"
|
|
74 |
by transfer_prover
|
|
75 |
|
|
76 |
lift_definition set_uprod :: "'a uprod \<Rightarrow> 'a set" is "\<lambda>(a, b). {a, b}"
|
|
77 |
parametric set_uprod_parametric' by auto
|
|
78 |
|
|
79 |
lemma set_uprod_simps [simp, code]: "set_uprod (Upair x y) = {x, y}"
|
|
80 |
by transfer simp
|
|
81 |
|
|
82 |
lemma finite_set_uprod [simp]: "finite (set_uprod x)"
|
|
83 |
by(cases x) simp
|
|
84 |
|
|
85 |
private lemma map_uprod_parametric':
|
|
86 |
"((A ===> B) ===> rel_prod A A ===> rel_prod B B) (\<lambda>f. map_prod f f) (\<lambda>f. map_prod f f)"
|
|
87 |
by transfer_prover
|
|
88 |
|
|
89 |
lift_definition map_uprod :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a uprod \<Rightarrow> 'b uprod" is "\<lambda>f. map_prod f f"
|
|
90 |
parametric map_uprod_parametric' by auto
|
|
91 |
|
|
92 |
lemma map_uprod_simps [simp, code]: "map_uprod f (Upair x y) = Upair (f x) (f y)"
|
|
93 |
by transfer simp
|
|
94 |
|
|
95 |
private lemma rel_uprod_transfer':
|
67399
|
96 |
"((A ===> B ===> (=)) ===> rel_prod A A ===> rel_prod B B ===> (=))
|
66563
|
97 |
(\<lambda>R (a, b) (c, d). R a c \<and> R b d \<or> R a d \<and> R b c) (\<lambda>R (a, b) (c, d). R a c \<and> R b d \<or> R a d \<and> R b c)"
|
|
98 |
by transfer_prover
|
|
99 |
|
|
100 |
lift_definition rel_uprod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a uprod \<Rightarrow> 'b uprod \<Rightarrow> bool"
|
|
101 |
is "\<lambda>R (a, b) (c, d). R a c \<and> R b d \<or> R a d \<and> R b c" parametric rel_uprod_transfer'
|
|
102 |
by auto
|
|
103 |
|
|
104 |
lemma rel_uprod_simps [simp, code]:
|
|
105 |
"rel_uprod R (Upair a b) (Upair c d) \<longleftrightarrow> R a c \<and> R b d \<or> R a d \<and> R b c"
|
|
106 |
by transfer auto
|
|
107 |
|
|
108 |
lemma Upair_parametric [transfer_rule]: "(A ===> A ===> rel_uprod A) Upair Upair"
|
|
109 |
unfolding rel_fun_def by transfer auto
|
|
110 |
|
|
111 |
lemma case_uprod_parametric [transfer_rule]:
|
|
112 |
"(rel_commute A B ===> rel_uprod A ===> B) case_uprod case_uprod"
|
|
113 |
unfolding rel_fun_def by transfer(force dest: rel_funD)
|
|
114 |
|
|
115 |
end
|
|
116 |
|
|
117 |
bnf uprod: "'a uprod"
|
|
118 |
map: map_uprod
|
|
119 |
sets: set_uprod
|
|
120 |
bd: natLeq
|
|
121 |
rel: rel_uprod
|
|
122 |
proof -
|
|
123 |
show "map_uprod id = id" unfolding fun_eq_iff by transfer auto
|
|
124 |
show "map_uprod (g \<circ> f) = map_uprod g \<circ> map_uprod f" for f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
|
|
125 |
unfolding fun_eq_iff by transfer auto
|
|
126 |
show "map_uprod f x = map_uprod g x" if "\<And>z. z \<in> set_uprod x \<Longrightarrow> f z = g z"
|
|
127 |
for f :: "'a \<Rightarrow> 'b" and g x using that by transfer auto
|
67399
|
128 |
show "set_uprod \<circ> map_uprod f = (`) f \<circ> set_uprod" for f :: "'a \<Rightarrow> 'b" by transfer auto
|
66563
|
129 |
show "card_order natLeq" by(rule natLeq_card_order)
|
|
130 |
show "BNF_Cardinal_Arithmetic.cinfinite natLeq" by(rule natLeq_cinfinite)
|
|
131 |
show "ordLeq3 (card_of (set_uprod x)) natLeq" for x :: "'a uprod"
|
|
132 |
by (auto simp: finite_iff_ordLess_natLeq[symmetric] intro: ordLess_imp_ordLeq)
|
|
133 |
show "rel_uprod R OO rel_uprod S \<le> rel_uprod (R OO S)"
|
|
134 |
for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" by(rule predicate2I)(transfer; auto)
|
|
135 |
show "rel_uprod R = (\<lambda>x y. \<exists>z. set_uprod z \<subseteq> {(x, y). R x y} \<and> map_uprod fst z = x \<and> map_uprod snd z = y)"
|
|
136 |
for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" by transfer(auto simp add: fun_eq_iff)
|
|
137 |
qed
|
|
138 |
|
|
139 |
lemma pred_uprod_code [simp, code]: "pred_uprod P (Upair x y) \<longleftrightarrow> P x \<and> P y"
|
|
140 |
by(simp add: pred_uprod_def)
|
|
141 |
|
|
142 |
instantiation uprod :: (equal) equal begin
|
|
143 |
|
|
144 |
definition equal_uprod :: "'a uprod \<Rightarrow> 'a uprod \<Rightarrow> bool"
|
67399
|
145 |
where "equal_uprod = (=)"
|
66563
|
146 |
|
|
147 |
lemma equal_uprod_code [code]:
|
|
148 |
"HOL.equal (Upair x y) (Upair z u) \<longleftrightarrow> x = z \<and> y = u \<or> x = u \<and> y = z"
|
|
149 |
unfolding equal_uprod_def by simp
|
|
150 |
|
|
151 |
instance by standard(simp add: equal_uprod_def)
|
|
152 |
end
|
|
153 |
|
|
154 |
quickcheck_generator uprod constructors: Upair
|
|
155 |
|
|
156 |
lemma UNIV_uprod: "UNIV = (\<lambda>x. Upair x x) ` UNIV \<union> (\<lambda>(x, y). Upair x y) ` Sigma UNIV (\<lambda>x. UNIV - {x})"
|
|
157 |
apply(rule set_eqI)
|
|
158 |
subgoal for x by(cases x) auto
|
|
159 |
done
|
|
160 |
|
|
161 |
context begin
|
|
162 |
private lift_definition upair_inv :: "'a uprod \<Rightarrow> 'a"
|
|
163 |
is "\<lambda>(x, y). if x = y then x else undefined" by auto
|
|
164 |
|
|
165 |
lemma finite_UNIV_prod [simp]:
|
|
166 |
"finite (UNIV :: 'a uprod set) \<longleftrightarrow> finite (UNIV :: 'a set)" (is "?lhs = ?rhs")
|
|
167 |
proof
|
|
168 |
assume ?lhs
|
|
169 |
hence "finite (range (\<lambda>x :: 'a. Upair x x))" by(rule finite_subset[rotated]) simp
|
|
170 |
hence "finite (upair_inv ` range (\<lambda>x :: 'a. Upair x x))" by(rule finite_imageI)
|
|
171 |
also have "upair_inv (Upair x x) = x" for x :: 'a by transfer simp
|
|
172 |
then have "upair_inv ` range (\<lambda>x :: 'a. Upair x x) = UNIV" by(auto simp add: image_image)
|
|
173 |
finally show ?rhs .
|
|
174 |
qed(simp add: UNIV_uprod)
|
|
175 |
|
|
176 |
end
|
|
177 |
|
|
178 |
lemma card_UNIV_uprod:
|
|
179 |
"card (UNIV :: 'a uprod set) = card (UNIV :: 'a set) * (card (UNIV :: 'a set) + 1) div 2"
|
|
180 |
(is "?UPROD = ?A * _ div _")
|
|
181 |
proof(cases "finite (UNIV :: 'a set)")
|
|
182 |
case True
|
|
183 |
from True obtain f :: "nat \<Rightarrow> 'a" where bij: "bij_betw f {0..<?A} UNIV"
|
|
184 |
by (blast dest: ex_bij_betw_nat_finite)
|
|
185 |
hence [simp]: "f ` {0..<?A} = UNIV" by(rule bij_betw_imp_surj_on)
|
|
186 |
have "UNIV = (\<lambda>(x, y). Upair (f x) (f y)) ` (SIGMA x:{0..<?A}. {..x})"
|
|
187 |
apply(rule set_eqI)
|
|
188 |
subgoal for x
|
|
189 |
apply(cases x)
|
|
190 |
apply(clarsimp)
|
|
191 |
subgoal for a b
|
|
192 |
apply(cases "inv_into {0..<?A} f a \<le> inv_into {0..<?A} f b")
|
|
193 |
subgoal by(rule rev_image_eqI[where x="(inv_into {0..<?A} f _, inv_into {0..<?A} f _)"])
|
|
194 |
(auto simp add: inv_into_into[where A="{0..<?A}" and f=f, simplified] intro: f_inv_into_f[where f=f, symmetric])
|
|
195 |
subgoal
|
|
196 |
apply(simp only: not_le)
|
|
197 |
apply(drule less_imp_le)
|
|
198 |
apply(rule rev_image_eqI[where x="(inv_into {0..<?A} f _, inv_into {0..<?A} f _)"])
|
|
199 |
apply(auto simp add: inv_into_into[where A="{0..<?A}" and f=f, simplified] intro: f_inv_into_f[where f=f, symmetric])
|
|
200 |
done
|
|
201 |
done
|
|
202 |
done
|
|
203 |
done
|
|
204 |
hence "?UPROD = card \<dots>" by simp
|
|
205 |
also have "\<dots> = card (SIGMA x:{0..<?A}. {..x})"
|
|
206 |
apply(rule card_image)
|
|
207 |
using bij[THEN bij_betw_imp_inj_on]
|
|
208 |
by(simp add: inj_on_def Ball_def)(metis leD le_eq_less_or_eq le_less_trans)
|
66936
|
209 |
also have "\<dots> = sum Suc {0..<?A}"
|
|
210 |
by (subst card_SigmaI) simp_all
|
|
211 |
also have "\<dots> = sum of_nat {Suc 0..?A}"
|
|
212 |
using sum.atLeast_lessThan_reindex [symmetric, of Suc 0 ?A id]
|
|
213 |
by (simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
|
66563
|
214 |
also have "\<dots> = ?A * (?A + 1) div 2"
|
66936
|
215 |
using gauss_sum_from_Suc_0 [of ?A, where ?'a = nat] by simp
|
66563
|
216 |
finally show ?thesis .
|
|
217 |
qed simp
|
|
218 |
|
|
219 |
end
|