(* Title: HOL/BNF_Wellorder_Embedding.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
Well-order embeddings as needed by bounded natural functors.
*)
section \Well-Order Embeddings as Needed by Bounded Natural Functors\
theory BNF_Wellorder_Embedding
imports Hilbert_Choice BNF_Wellorder_Relation
begin
text\In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and
prove their basic properties. The notion of embedding is considered from the point
of view of the theory of ordinals, and therefore requires the source to be injected
as an {\em initial segment} (i.e., {\em order filter}) of the target. A main result
of this section is the existence of embeddings (in one direction or another) between
any two well-orders, having as a consequence the fact that, given any two sets on
any two types, one is smaller than (i.e., can be injected into) the other.\
subsection \Auxiliaries\
lemma UNION_inj_on_ofilter:
assumes WELL: "Well_order r" and
OF: "\ i. i \ I \ wo_rel.ofilter r (A i)" and
INJ: "\ i. i \ I \ inj_on f (A i)"
shows "inj_on f (\i \ I. A i)"
proof-
have "wo_rel r" using WELL by (simp add: wo_rel_def)
hence "\ i j. \i \ I; j \ I\ \ A i <= A j \ A j <= A i"
using wo_rel.ofilter_linord[of r] OF by blast
with WELL INJ show ?thesis
by (auto simp add: inj_on_UNION_chain)
qed
lemma under_underS_bij_betw:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
IN: "a \ Field r" and IN': "f a \ Field r'" and
BIJ: "bij_betw f (underS r a) (underS r' (f a))"
shows "bij_betw f (under r a) (under r' (f a))"
proof-
have "a \ underS r a \ f a \ underS r' (f a)"
unfolding underS_def by auto
moreover
{have "Refl r \ Refl r'" using WELL WELL'
by (auto simp add: order_on_defs)
hence "under r a = underS r a \ {a} \
under r' (f a) = underS r' (f a) \ {f a}"
using IN IN' by(auto simp add: Refl_under_underS)
}
ultimately show ?thesis
using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto
qed
subsection \(Well-order) embeddings, strict embeddings, isomorphisms and order-compatible
functions\
text\Standardly, a function is an embedding of a well-order in another if it injectively and
order-compatibly maps the former into an order filter of the latter.
Here we opt for a more succinct definition (operator \embed\),
asking that, for any element in the source, the function should be a bijection
between the set of strict lower bounds of that element
and the set of strict lower bounds of its image. (Later we prove equivalence with
the standard definition -- lemma \embed_iff_compat_inj_on_ofilter\.)
A {\em strict embedding} (operator \embedS\) is a non-bijective embedding
and an isomorphism (operator \iso\) is a bijective embedding.\
definition embed :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool"
where
"embed r r' f \ \a \ Field r. bij_betw f (under r a) (under r' (f a))"
lemmas embed_defs = embed_def embed_def[abs_def]
text \Strict embeddings:\
definition embedS :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool"
where
"embedS r r' f \ embed r r' f \ \ bij_betw f (Field r) (Field r')"
lemmas embedS_defs = embedS_def embedS_def[abs_def]
definition iso :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool"
where
"iso r r' f \ embed r r' f \ bij_betw f (Field r) (Field r')"
lemmas iso_defs = iso_def iso_def[abs_def]
definition compat :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool"
where
"compat r r' f \ \a b. (a,b) \ r \ (f a, f b) \ r'"
lemma compat_wf:
assumes CMP: "compat r r' f" and WF: "wf r'"
shows "wf r"
proof-
have "r \ inv_image r' f"
unfolding inv_image_def using CMP
by (auto simp add: compat_def)
with WF show ?thesis
using wf_inv_image[of r' f] wf_subset[of "inv_image r' f"] by auto
qed
lemma id_embed: "embed r r id"
by(auto simp add: id_def embed_def bij_betw_def)
lemma id_iso: "iso r r id"
by(auto simp add: id_def embed_def iso_def bij_betw_def)
lemma embed_in_Field:
assumes WELL: "Well_order r" and
EMB: "embed r r' f" and IN: "a \ Field r"
shows "f a \ Field r'"
proof-
have Well: "wo_rel r"
using WELL by (auto simp add: wo_rel_def)
hence 1: "Refl r"
by (auto simp add: wo_rel.REFL)
hence "a \ under r a" using IN Refl_under_in by fastforce
hence "f a \ under r' (f a)"
using EMB IN by (auto simp add: embed_def bij_betw_def)
thus ?thesis unfolding Field_def
by (auto simp: under_def)
qed
lemma comp_embed:
assumes WELL: "Well_order r" and
EMB: "embed r r' f" and EMB': "embed r' r'' f'"
shows "embed r r'' (f' o f)"
proof(unfold embed_def, auto)
fix a assume *: "a \ Field r"
hence "bij_betw f (under r a) (under r' (f a))"
using embed_def[of r] EMB by auto
moreover
{have "f a \ Field r'"
using EMB WELL * by (auto simp add: embed_in_Field)
hence "bij_betw f' (under r' (f a)) (under r'' (f' (f a)))"
using embed_def[of r'] EMB' by auto
}
ultimately
show "bij_betw (f' \ f) (under r a) (under r'' (f'(f a)))"
by(auto simp add: bij_betw_trans)
qed
lemma comp_iso:
assumes WELL: "Well_order r" and
EMB: "iso r r' f" and EMB': "iso r' r'' f'"
shows "iso r r'' (f' o f)"
using assms unfolding iso_def
by (auto simp add: comp_embed bij_betw_trans)
text\That \embedS\ is also preserved by function composition shall be proved only later.\
lemma embed_Field:
"\Well_order r; embed r r' f\ \ f`(Field r) \ Field r'"
by (auto simp add: embed_in_Field)
lemma embed_preserves_ofilter:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f" and OF: "wo_rel.ofilter r A"
shows "wo_rel.ofilter r' (f`A)"
proof-
(* Preliminary facts *)
from WELL have Well: "wo_rel r" unfolding wo_rel_def .
from WELL' have Well': "wo_rel r'" unfolding wo_rel_def .
from OF have 0: "A \ Field r" by(auto simp add: Well wo_rel.ofilter_def)
(* Main proof *)
show ?thesis using Well' WELL EMB 0 embed_Field[of r r' f]
proof(unfold wo_rel.ofilter_def, auto simp add: image_def)
fix a b'
assume *: "a \ A" and **: "b' \ under r' (f a)"
hence "a \ Field r" using 0 by auto
hence "bij_betw f (under r a) (under r' (f a))"
using * EMB by (auto simp add: embed_def)
hence "f`(under r a) = under r' (f a)"
by (simp add: bij_betw_def)
with ** image_def[of f "under r a"] obtain b where
1: "b \ under r a \ b' = f b" by blast
hence "b \ A" using Well * OF
by (auto simp add: wo_rel.ofilter_def)
with 1 show "\b \ A. b' = f b" by blast
qed
qed
lemma embed_Field_ofilter:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f"
shows "wo_rel.ofilter r' (f`(Field r))"
proof-
have "wo_rel.ofilter r (Field r)"
using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter)
with WELL WELL' EMB
show ?thesis by (auto simp add: embed_preserves_ofilter)
qed
lemma embed_compat:
assumes EMB: "embed r r' f"
shows "compat r r' f"
proof(unfold compat_def, clarify)
fix a b
assume *: "(a,b) \ r"
hence 1: "b \ Field r" using Field_def[of r] by blast
have "a \ under r b"
using * under_def[of r] by simp
hence "f a \ under r' (f b)"
using EMB embed_def[of r r' f]
bij_betw_def[of f "under r b" "under r' (f b)"]
image_def[of f "under r b"] 1 by auto
thus "(f a, f b) \ r'"
by (auto simp add: under_def)
qed
lemma embed_inj_on:
assumes WELL: "Well_order r" and EMB: "embed r r' f"
shows "inj_on f (Field r)"
proof(unfold inj_on_def, clarify)
(* Preliminary facts *)
from WELL have Well: "wo_rel r" unfolding wo_rel_def .
with wo_rel.TOTAL[of r]
have Total: "Total r" by simp
from Well wo_rel.REFL[of r]
have Refl: "Refl r" by simp
(* Main proof *)
fix a b
assume *: "a \ Field r" and **: "b \ Field r" and
***: "f a = f b"
hence 1: "a \ Field r \ b \ Field r"
unfolding Field_def by auto
{assume "(a,b) \ r"
hence "a \ under r b \ b \ under r b"
using Refl by(auto simp add: under_def refl_on_def)
hence "a = b"
using EMB 1 ***
by (auto simp add: embed_def bij_betw_def inj_on_def)
}
moreover
{assume "(b,a) \ r"
hence "a \ under r a \ b \ under r a"
using Refl by(auto simp add: under_def refl_on_def)
hence "a = b"
using EMB 1 ***
by (auto simp add: embed_def bij_betw_def inj_on_def)
}
ultimately
show "a = b" using Total 1
by (auto simp add: total_on_def)
qed
lemma embed_underS:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f" and IN: "a \ Field r"
shows "bij_betw f (underS r a) (underS r' (f a))"
proof-
have "bij_betw f (under r a) (under r' (f a))"
using assms by (auto simp add: embed_def)
moreover
{have "f a \ Field r'" using assms embed_Field[of r r' f] by auto
hence "under r a = underS r a \ {a} \
under r' (f a) = underS r' (f a) \ {f a}"
using assms by (auto simp add: order_on_defs Refl_under_underS)
}
moreover
{have "a \ underS r a \ f a \ underS r' (f a)"
unfolding underS_def by blast
}
ultimately show ?thesis
by (auto simp add: notIn_Un_bij_betw3)
qed
lemma embed_iff_compat_inj_on_ofilter:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "embed r r' f = (compat r r' f \ inj_on f (Field r) \ wo_rel.ofilter r' (f`(Field r)))"
using assms
proof(auto simp add: embed_compat embed_inj_on embed_Field_ofilter,
unfold embed_def, auto) (* get rid of one implication *)
fix a
assume *: "inj_on f (Field r)" and
**: "compat r r' f" and
***: "wo_rel.ofilter r' (f`(Field r))" and
****: "a \ Field r"
(* Preliminary facts *)
have Well: "wo_rel r"
using WELL wo_rel_def[of r] by simp
hence Refl: "Refl r"
using wo_rel.REFL[of r] by simp
have Total: "Total r"
using Well wo_rel.TOTAL[of r] by simp
have Well': "wo_rel r'"
using WELL' wo_rel_def[of r'] by simp
hence Antisym': "antisym r'"
using wo_rel.ANTISYM[of r'] by simp
have "(a,a) \ r"
using **** Well wo_rel.REFL[of r]
refl_on_def[of _ r] by auto
hence "(f a, f a) \ r'"
using ** by(auto simp add: compat_def)
hence 0: "f a \ Field r'"
unfolding Field_def by auto
have "f a \ f`(Field r)"
using **** by auto
hence 2: "under r' (f a) \ f`(Field r)"
using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce
(* Main proof *)
show "bij_betw f (under r a) (under r' (f a))"
proof(unfold bij_betw_def, auto)
show "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field])
next
fix b assume "b \ under r a"
thus "f b \ under r' (f a)"
unfolding under_def using **
by (auto simp add: compat_def)
next
fix b' assume *****: "b' \ under r' (f a)"
hence "b' \ f`(Field r)"
using 2 by auto
with Field_def[of r] obtain b where
3: "b \ Field r" and 4: "b' = f b" by auto
have "(b,a): r"
proof-
{assume "(a,b) \ r"
with ** 4 have "(f a, b'): r'"
by (auto simp add: compat_def)
with ***** Antisym' have "f a = b'"
by(auto simp add: under_def antisym_def)
with 3 **** 4 * have "a = b"
by(auto simp add: inj_on_def)
}
moreover
{assume "a = b"
hence "(b,a) \ r" using Refl **** 3
by (auto simp add: refl_on_def)
}
ultimately
show ?thesis using Total **** 3 by (fastforce simp add: total_on_def)
qed
with 4 show "b' \ f`(under r a)"
unfolding under_def by auto
qed
qed
lemma inv_into_ofilter_embed:
assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and
BIJ: "\b \ A. bij_betw f (under r b) (under r' (f b))" and
IMAGE: "f ` A = Field r'"
shows "embed r' r (inv_into A f)"
proof-
(* Preliminary facts *)
have Well: "wo_rel r"
using WELL wo_rel_def[of r] by simp
have Refl: "Refl r"
using Well wo_rel.REFL[of r] by simp
have Total: "Total r"
using Well wo_rel.TOTAL[of r] by simp
(* Main proof *)
have 1: "bij_betw f A (Field r')"
proof(unfold bij_betw_def inj_on_def, auto simp add: IMAGE)
fix b1 b2
assume *: "b1 \ A" and **: "b2 \ A" and
***: "f b1 = f b2"
have 11: "b1 \ Field r \ b2 \ Field r"
using * ** Well OF by (auto simp add: wo_rel.ofilter_def)
moreover
{assume "(b1,b2) \ r"
hence "b1 \ under r b2 \ b2 \ under r b2"
unfolding under_def using 11 Refl
by (auto simp add: refl_on_def)
hence "b1 = b2" using BIJ * ** ***
by (simp add: bij_betw_def inj_on_def)
}
moreover
{assume "(b2,b1) \ r"
hence "b1 \ under r b1 \ b2 \ under r b1"
unfolding under_def using 11 Refl
by (auto simp add: refl_on_def)
hence "b1 = b2" using BIJ * ** ***
by (simp add: bij_betw_def inj_on_def)
}
ultimately
show "b1 = b2"
using Total by (auto simp add: total_on_def)
qed
(* *)
let ?f' = "(inv_into A f)"
(* *)
have 2: "\b \ A. bij_betw ?f' (under r' (f b)) (under r b)"
proof(clarify)
fix b assume *: "b \ A"
hence "under r b \ A"
using Well OF by(auto simp add: wo_rel.ofilter_def)
moreover
have "f ` (under r b) = under r' (f b)"
using * BIJ by (auto simp add: bij_betw_def)
ultimately
show "bij_betw ?f' (under r' (f b)) (under r b)"
using 1 by (auto simp add: bij_betw_inv_into_subset)
qed
(* *)
have 3: "\b' \ Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))"
proof(clarify)
fix b' assume *: "b' \ Field r'"
have "b' = f (?f' b')" using * 1
by (auto simp add: bij_betw_inv_into_right)
moreover
{obtain b where 31: "b \ A" and "f b = b'" using IMAGE * by force
hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left)
with 31 have "?f' b' \ A" by auto
}
ultimately
show "bij_betw ?f' (under r' b') (under r (?f' b'))"
using 2 by auto
qed
(* *)
thus ?thesis unfolding embed_def .
qed
lemma inv_into_underS_embed:
assumes WELL: "Well_order r" and
BIJ: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" and
IN: "a \ Field r" and
IMAGE: "f ` (underS r a) = Field r'"
shows "embed r' r (inv_into (underS r a) f)"
using assms
by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)
lemma inv_into_Field_embed:
assumes WELL: "Well_order r" and EMB: "embed r r' f" and
IMAGE: "Field r' \ f ` (Field r)"
shows "embed r' r (inv_into (Field r) f)"
proof-
have "(\b \ Field r. bij_betw f (under r b) (under r' (f b)))"
using EMB by (auto simp add: embed_def)
moreover
have "f ` (Field r) \ Field r'"
using EMB WELL by (auto simp add: embed_Field)
ultimately
show ?thesis using assms
by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
qed
lemma inv_into_Field_embed_bij_betw:
assumes WELL: "Well_order r" and
EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')"
shows "embed r' r (inv_into (Field r) f)"
proof-
have "Field r' \ f ` (Field r)"
using BIJ by (auto simp add: bij_betw_def)
thus ?thesis using assms
by(auto simp add: inv_into_Field_embed)
qed
subsection \Given any two well-orders, one can be embedded in the other\
text\Here is an overview of the proof of of this fact, stated in theorem
\wellorders_totally_ordered\:
Fix the well-orders \r::'a rel\ and \r'::'a' rel\.
Attempt to define an embedding \f::'a \ 'a'\ from \r\ to \r'\ in the
natural way by well-order recursion ("hoping" that \Field r\ turns out to be smaller
than \Field r'\), but also record, at the recursive step, in a function
\g::'a \ bool\, the extra information of whether \Field r'\
gets exhausted or not.
If \Field r'\ does not get exhausted, then \Field r\ is indeed smaller
and \f\ is the desired embedding from \r\ to \r'\
(lemma \wellorders_totally_ordered_aux\).
Otherwise, it means that \Field r'\ is the smaller one, and the inverse of
(the "good" segment of) \f\ is the desired embedding from \r'\ to \r\
(lemma \wellorders_totally_ordered_aux2\).
\
lemma wellorders_totally_ordered_aux:
fixes r ::"'a rel" and r'::"'a' rel" and
f :: "'a \ 'a'" and a::'a
assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \ Field r" and
IH: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" and
NOT: "f ` (underS r a) \ Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))"
shows "bij_betw f (under r a) (under r' (f a))"
proof-
(* Preliminary facts *)
have Well: "wo_rel r" using WELL unfolding wo_rel_def .
hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
have OF: "wo_rel.ofilter r (underS r a)"
by (auto simp add: Well wo_rel.underS_ofilter)
hence UN: "underS r a = (\b \ underS r a. under r b)"
using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
(* Gather facts about elements of underS r a *)
{fix b assume *: "b \ underS r a"
hence t0: "(b,a) \ r \ b \ a" unfolding underS_def by auto
have t1: "b \ Field r"
using * underS_Field[of r a] by auto
have t2: "f`(under r b) = under r' (f b)"
using IH * by (auto simp add: bij_betw_def)
hence t3: "wo_rel.ofilter r' (f`(under r b))"
using Well' by (auto simp add: wo_rel.under_ofilter)
have "f`(under r b) \ Field r'"
using t2 by (auto simp add: under_Field)
moreover
have "b \ under r b"
using t1 by(auto simp add: Refl Refl_under_in)
ultimately
have t4: "f b \ Field r'" by auto
have "f`(under r b) = under r' (f b) \
wo_rel.ofilter r' (f`(under r b)) \
f b \ Field r'"
using t2 t3 t4 by auto
}
hence bFact:
"\b \ underS r a. f`(under r b) = under r' (f b) \
wo_rel.ofilter r' (f`(under r b)) \
f b \ Field r'" by blast
(* *)
have subField: "f`(underS r a) \ Field r'"
using bFact by blast
(* *)
have OF': "wo_rel.ofilter r' (f`(underS r a))"
proof-
have "f`(underS r a) = f`(\b \ underS r a. under r b)"
using UN by auto
also have "\ = (\b \ underS r a. f`(under r b))" by blast
also have "\ = (\b \ underS r a. (under r' (f b)))"
using bFact by auto
finally
have "f`(underS r a) = (\b \ underS r a. (under r' (f b)))" .
thus ?thesis
using Well' bFact
wo_rel.ofilter_UNION[of r' "underS r a" "\ b. under r' (f b)"] by fastforce
qed
(* *)
have "f`(underS r a) \