[STATEMENT]
lemma wf_Ord_ordermap [iff]: assumes "wf r" "trans r" shows "Ord (ordermap A r x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord (ordermap A r x)
[PROOF STEP]
using \<open>wf r\<close>
[PROOF STATE]
proof (prove)
using this:
wf r

goal (1 subgoal):
 1. Ord (ordermap A r x)
[PROOF STEP]
proof (induction x rule: wf_induct_rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> r \<Longrightarrow> Ord (ordermap A r y)) \<Longrightarrow> Ord (ordermap A r x)
[PROOF STEP]
case (less u)
[PROOF STATE]
proof (state)
this:
(?y, u) \<in> r \<Longrightarrow> Ord (ordermap A r ?y)

goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> r \<Longrightarrow> Ord (ordermap A r y)) \<Longrightarrow> Ord (ordermap A r x)
[PROOF STEP]
have "Transset (set (ordermap A r ` {y \<in> A. (y, u) \<in> r}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Transset (set (ordermap A r ` {y \<in> A. (y, u) \<in> r}))
[PROOF STEP]
proof (clarsimp simp add: Transset_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y x. \<lbrakk>small (ordermap A r ` {y \<in> A. (y, u) \<in> r}); x \<in> elts (ordermap A r y); y \<in> A; (y, u) \<in> r\<rbrakk> \<Longrightarrow> x \<in> ordermap A r ` {y \<in> A. (y, u) \<in> r}
[PROOF STEP]
show "x \<in> ordermap A r ` {y \<in> A. (y, u) \<in> r}"
      if "small (ordermap A r ` {y \<in> A. (y, u) \<in> r})"
        and x: "x \<in> elts (ordermap A r y)" and "y \<in> A" "(y, u) \<in> r" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ordermap A r ` {y \<in> A. (y, u) \<in> r}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> ordermap A r ` {y \<in> A. (y, u) \<in> r}
[PROOF STEP]
have "ordermap A r y = ZFC_in_HOL.set (ordermap A r ` {a \<in> A. (a, y) \<in> r})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap A r y = set (ordermap A r ` {a \<in> A. (a, y) \<in> r})
[PROOF STEP]
using ordermap assms(1)
[PROOF STATE]
proof (prove)
using this:
wf ?r \<Longrightarrow> ordermap ?A ?r ?a = set (ordermap ?A ?r ` {y \<in> ?A. (y, ?a) \<in> ?r})
wf r

goal (1 subgoal):
 1. ordermap A r y = set (ordermap A r ` {a \<in> A. (a, y) \<in> r})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ordermap A r y = set (ordermap A r ` {a \<in> A. (a, y) \<in> r})

goal (1 subgoal):
 1. x \<in> ordermap A r ` {y \<in> A. (y, u) \<in> r}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ordermap A r y = set (ordermap A r ` {a \<in> A. (a, y) \<in> r})
[PROOF STEP]
have "x \<in> ordermap A r ` {z \<in> A. (z, y) \<in> r}"
[PROOF STATE]
proof (prove)
using this:
ordermap A r y = set (ordermap A r ` {a \<in> A. (a, y) \<in> r})

goal (1 subgoal):
 1. x \<in> ordermap A r ` {z \<in> A. (z, y) \<in> r}
[PROOF STEP]
by (metis (no_types, lifting) elts_of_set empty_iff x)
[PROOF STATE]
proof (state)
this:
x \<in> ordermap A r ` {z \<in> A. (z, y) \<in> r}

goal (1 subgoal):
 1. x \<in> ordermap A r ` {y \<in> A. (y, u) \<in> r}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> ordermap A r ` {z \<in> A. (z, y) \<in> r}
[PROOF STEP]
have "\<exists>v. v \<in> A \<and> (v, u) \<in> r \<and> x = ordermap A r v"
[PROOF STATE]
proof (prove)
using this:
x \<in> ordermap A r ` {z \<in> A. (z, y) \<in> r}

goal (1 subgoal):
 1. \<exists>v. v \<in> A \<and> (v, u) \<in> r \<and> x = ordermap A r v
[PROOF STEP]
using that transD [OF \<open>trans r\<close>]
[PROOF STATE]
proof (prove)
using this:
x \<in> ordermap A r ` {z \<in> A. (z, y) \<in> r}
small (ordermap A r ` {y \<in> A. (y, u) \<in> r})
x \<in> elts (ordermap A r y)
y \<in> A
(y, u) \<in> r
\<lbrakk>(?x, ?y) \<in> r; (?y, ?z) \<in> r\<rbrakk> \<Longrightarrow> (?x, ?z) \<in> r

goal (1 subgoal):
 1. \<exists>v. v \<in> A \<and> (v, u) \<in> r \<and> x = ordermap A r v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>v. v \<in> A \<and> (v, u) \<in> r \<and> x = ordermap A r v

goal (1 subgoal):
 1. x \<in> ordermap A r ` {y \<in> A. (y, u) \<in> r}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. v \<in> A \<and> (v, u) \<in> r \<and> x = ordermap A r v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>v. v \<in> A \<and> (v, u) \<in> r \<and> x = ordermap A r v

goal (1 subgoal):
 1. x \<in> ordermap A r ` {y \<in> A. (y, u) \<in> r}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> ordermap A r ` {y \<in> A. (y, u) \<in> r}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>small (ordermap A r ` {y \<in> A. (y, u) \<in> r}); ?x \<in> elts (ordermap A r ?y); ?y \<in> A; (?y, u) \<in> r\<rbrakk> \<Longrightarrow> ?x \<in> ordermap A r ` {y \<in> A. (y, u) \<in> r}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Transset (set (ordermap A r ` {y \<in> A. (y, u) \<in> r}))

goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> r \<Longrightarrow> Ord (ordermap A r y)) \<Longrightarrow> Ord (ordermap A r x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Transset (set (ordermap A r ` {y \<in> A. (y, u) \<in> r}))

goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> r \<Longrightarrow> Ord (ordermap A r y)) \<Longrightarrow> Ord (ordermap A r x)
[PROOF STEP]
have "Ord x"
    if "x \<in> elts (set (ordermap A r ` {y \<in> A. (y, u) \<in> r}))" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord x
[PROOF STEP]
using that less
[PROOF STATE]
proof (prove)
using this:
x \<in> elts (set (ordermap A r ` {y \<in> A. (y, u) \<in> r}))
(?y, u) \<in> r \<Longrightarrow> Ord (ordermap A r ?y)

goal (1 subgoal):
 1. Ord x
[PROOF STEP]
by (auto simp: split: if_split_asm)
[PROOF STATE]
proof (state)
this:
?x \<in> elts (set (ordermap A r ` {y \<in> A. (y, u) \<in> r})) \<Longrightarrow> Ord ?x

goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> r \<Longrightarrow> Ord (ordermap A r y)) \<Longrightarrow> Ord (ordermap A r x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Transset (set (ordermap A r ` {y \<in> A. (y, u) \<in> r}))
?x \<in> elts (set (ordermap A r ` {y \<in> A. (y, u) \<in> r})) \<Longrightarrow> Ord ?x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Transset (set (ordermap A r ` {y \<in> A. (y, u) \<in> r}))
?x \<in> elts (set (ordermap A r ` {y \<in> A. (y, u) \<in> r})) \<Longrightarrow> Ord ?x

goal (1 subgoal):
 1. Ord (ordermap A r u)
[PROOF STEP]
by (metis (full_types) Ord_def ordermap assms(1))
[PROOF STATE]
proof (state)
this:
Ord (ordermap A r u)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_Ord_ordertype: assumes "wf r" "trans r" shows "Ord(ordertype A r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord (ordertype A r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ord (ordertype A r)
[PROOF STEP]
have "y \<le> set (ordermap A r ` A)"
    if "y = ordermap A r x" "x \<in> A" "small (ordermap A r ` A)" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> set (ordermap A r ` A)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
y = ordermap A r x
x \<in> A
small (ordermap A r ` A)

goal (1 subgoal):
 1. y \<le> set (ordermap A r ` A)
[PROOF STEP]
by (auto simp: less_eq_V_def ordermap [OF \<open>wf r\<close>, of A x])
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y = ordermap A r ?x; ?x \<in> A; small (ordermap A r ` A)\<rbrakk> \<Longrightarrow> ?y \<le> set (ordermap A r ` A)

goal (1 subgoal):
 1. Ord (ordertype A r)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y = ordermap A r ?x; ?x \<in> A; small (ordermap A r ` A)\<rbrakk> \<Longrightarrow> ?y \<le> set (ordermap A r ` A)

goal (1 subgoal):
 1. Ord (ordertype A r)
[PROOF STEP]
have "z \<le> y" if "y \<in> ordermap A r ` A" "z \<in> elts y" for y z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<le> y
[PROOF STEP]
by (metis wf_Ord_ordermap OrdmemD assms imageE order.strict_implies_order that)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<in> ordermap A r ` A; ?z \<in> elts ?y\<rbrakk> \<Longrightarrow> ?z \<le> ?y

goal (1 subgoal):
 1. Ord (ordertype A r)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?y = ordermap A r ?x; ?x \<in> A; small (ordermap A r ` A)\<rbrakk> \<Longrightarrow> ?y \<le> set (ordermap A r ` A)
\<lbrakk>?y \<in> ordermap A r ` A; ?z \<in> elts ?y\<rbrakk> \<Longrightarrow> ?z \<le> ?y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = ordermap A r ?x; ?x \<in> A; small (ordermap A r ` A)\<rbrakk> \<Longrightarrow> ?y \<le> set (ordermap A r ` A)
\<lbrakk>?y \<in> ordermap A r ` A; ?z \<in> elts ?y\<rbrakk> \<Longrightarrow> ?z \<le> ?y

goal (1 subgoal):
 1. Ord (ordertype A r)
[PROOF STEP]
unfolding ordertype_def Ord_def Transset_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = ordermap A r ?x; ?x \<in> A; small (ordermap A r ` A)\<rbrakk> \<Longrightarrow> ?y \<le> set (ordermap A r ` A)
\<lbrakk>?y \<in> ordermap A r ` A; ?z \<in> elts ?y\<rbrakk> \<Longrightarrow> ?z \<le> ?y

goal (1 subgoal):
 1. (\<forall>y\<in>elts (set (ordermap A r ` A)). y \<le> set (ordermap A r ` A)) \<and> (\<forall>y\<in>elts (set (ordermap A r ` A)). \<forall>ya\<in>elts y. ya \<le> y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Ord (ordertype A r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Ord_ordertype [simp]: "Ord(ordertype A VWF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord (ordertype A VWF)
[PROOF STEP]
using wf_Ord_ordertype
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>wf ?r; trans ?r\<rbrakk> \<Longrightarrow> Ord (ordertype ?A ?r)

goal (1 subgoal):
 1. Ord (ordertype A VWF)
[PROOF STEP]
by blast


[STATEMENT]
lemma Ord_ordermap [simp]: "Ord (ordermap A VWF x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord (ordermap A VWF x)
[PROOF STEP]
by blast


[STATEMENT]
lemma ordertype_singleton [simp]:
  assumes "wf r"
  shows "ordertype {x} r = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype {x} r = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype {x} r = 1
[PROOF STEP]
have \<dagger>: "{y. y = x \<and> (y, x) \<in> r} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. y = x \<and> (y, x) \<in> r} = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf r

goal (1 subgoal):
 1. {y. y = x \<and> (y, x) \<in> r} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{y. y = x \<and> (y, x) \<in> r} = {}

goal (1 subgoal):
 1. ordertype {x} r = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype {x} r = 1
[PROOF STEP]
by (auto simp add: ordertype_def assms \<dagger> ordermap [where a=x])
[PROOF STATE]
proof (state)
this:
ordertype {x} r = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordermap_mono:
  assumes wx: "(w, x) \<in> r" and "wf r" "w \<in> A" "small A"
    shows "ordermap A r w \<in> elts (ordermap A r x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap A r w \<in> elts (ordermap A r x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordermap A r w \<in> elts (ordermap A r x)
[PROOF STEP]
have "small {a \<in> A. (a, x) \<in> r} \<and> w \<in> A \<and> (w, x) \<in> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {a \<in> A. (a, x) \<in> r} \<and> w \<in> A \<and> (w, x) \<in> r
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
small {a \<in> A. (a, x) \<in> r} \<and> w \<in> A \<and> (w, x) \<in> r

goal (1 subgoal):
 1. ordermap A r w \<in> elts (ordermap A r x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
small {a \<in> A. (a, x) \<in> r} \<and> w \<in> A \<and> (w, x) \<in> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
small {a \<in> A. (a, x) \<in> r} \<and> w \<in> A \<and> (w, x) \<in> r

goal (1 subgoal):
 1. ordermap A r w \<in> elts (ordermap A r x)
[PROOF STEP]
using assms ordermap [of r A]
[PROOF STATE]
proof (prove)
using this:
small {a \<in> A. (a, x) \<in> r} \<and> w \<in> A \<and> (w, x) \<in> r
(w, x) \<in> r
wf r
w \<in> A
small A
wf r \<Longrightarrow> ordermap A r ?a = set (ordermap A r ` {y \<in> A. (y, ?a) \<in> r})

goal (1 subgoal):
 1. ordermap A r w \<in> elts (ordermap A r x)
[PROOF STEP]
by (metis (no_types, lifting) elts_of_set image_eqI mem_Collect_eq replacement)
[PROOF STATE]
proof (state)
this:
ordermap A r w \<in> elts (ordermap A r x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma converse_ordermap_mono:
  assumes "ordermap A r y \<in> elts (ordermap A r x)" "wf r" "total_on A r" "x \<in> A" "y \<in> A" "small A"
  shows "(y, x) \<in> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y, x) \<in> r
[PROOF STEP]
proof (cases "x = y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> (y, x) \<in> r
 2. x \<noteq> y \<Longrightarrow> (y, x) \<in> r
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> (y, x) \<in> r
 2. x \<noteq> y \<Longrightarrow> (y, x) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. (y, x) \<in> r
[PROOF STEP]
using assms(1) mem_not_refl
[PROOF STATE]
proof (prove)
using this:
x = y
ordermap A r y \<in> elts (ordermap A r x)
?i \<notin> elts ?i

goal (1 subgoal):
 1. (y, x) \<in> r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(y, x) \<in> r

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> (y, x) \<in> r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> (y, x) \<in> r
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> (y, x) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
[PROOF STEP]
consider "(x,y) \<in> r" | "(y,x) \<in> r"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> r \<Longrightarrow> thesis; (y, x) \<in> r \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using \<open>total_on A r\<close> assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
total_on A r
ordermap A r y \<in> elts (ordermap A r x)
wf r
total_on A r
x \<in> A
y \<in> A
small A

goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> r \<Longrightarrow> thesis; (y, x) \<in> r \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (meson UNIV_I total_on_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(x, y) \<in> r \<Longrightarrow> ?thesis; (y, x) \<in> r \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> (y, x) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(x, y) \<in> r \<Longrightarrow> ?thesis; (y, x) \<in> r \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(x, y) \<in> r \<Longrightarrow> ?thesis; (y, x) \<in> r \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (y, x) \<in> r
[PROOF STEP]
by (meson ordermap_mono assms mem_not_sym)
[PROOF STATE]
proof (state)
this:
(y, x) \<in> r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma converse_ordermap_mono_iff:
  assumes "wf r" "total_on A r" "x \<in> A" "y \<in> A" "small A"
  shows "ordermap A r y \<in> elts (ordermap A r x) \<longleftrightarrow> (y, x) \<in> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ordermap A r y \<in> elts (ordermap A r x)) = ((y, x) \<in> r)
[PROOF STEP]
by (metis assms converse_ordermap_mono ordermap_mono)


[STATEMENT]
lemma ordermap_surj: "elts (ordertype A r) \<subseteq> ordermap A r ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (ordertype A r) \<subseteq> ordermap A r ` A
[PROOF STEP]
unfolding ordertype_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (set (ordermap A r ` A)) \<subseteq> ordermap A r ` A
[PROOF STEP]
by simp


[STATEMENT]
lemma ordermap_bij:
  assumes "wf r" "total_on A r" "small A"
  shows "bij_betw (ordermap A r) A (elts (ordertype A r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (ordermap A r) A (elts (ordertype A r))
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (ordermap A r) A \<and> ordermap A r ` A = elts (ordertype A r)
[PROOF STEP]
proof (intro conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on (ordermap A r) A
 2. ordermap A r ` A = elts (ordertype A r)
[PROOF STEP]
show "inj_on (ordermap A r) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (ordermap A r) A
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. \<forall>y\<in>A. ordermap A r x = ordermap A r y \<longrightarrow> x = y
[PROOF STEP]
by (metis assms mem_not_refl ordermap_mono total_on_def)
[PROOF STATE]
proof (state)
this:
inj_on (ordermap A r) A

goal (1 subgoal):
 1. ordermap A r ` A = elts (ordertype A r)
[PROOF STEP]
show "ordermap A r ` A = elts (ordertype A r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap A r ` A = elts (ordertype A r)
[PROOF STEP]
by (metis ordertype_def \<open>small A\<close> elts_of_set replacement)
[PROOF STATE]
proof (state)
this:
ordermap A r ` A = elts (ordertype A r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordermap_eq_iff [simp]:
  "\<lbrakk>x \<in> A; y \<in> A; wf r; total_on A r; small A\<rbrakk> \<Longrightarrow> ordermap A r x = ordermap A r y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; y \<in> A; wf r; total_on A r; small A\<rbrakk> \<Longrightarrow> (ordermap A r x = ordermap A r y) = (x = y)
[PROOF STEP]
by (metis bij_betw_iff_bijections ordermap_bij)


[STATEMENT]
lemma inv_into_ordermap: "\<alpha> \<in> elts (ordertype A r) \<Longrightarrow> inv_into A (ordermap A r) \<alpha> \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<in> elts (ordertype A r) \<Longrightarrow> inv_into A (ordermap A r) \<alpha> \<in> A
[PROOF STEP]
by (meson in_mono inv_into_into ordermap_surj)


[STATEMENT]
lemma ordertype_nat_imp_finite:
  assumes "ordertype A r = ord_of_nat m" "small A" "wf r" "total_on A r"
  shows "finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite A
[PROOF STEP]
have "A \<approx> elts m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<approx> elts (ord_of_nat m)
[PROOF STEP]
using eqpoll_def assms ordermap_bij
[PROOF STATE]
proof (prove)
using this:
?A \<approx> ?B \<equiv> \<exists>f. bij_betw f ?A ?B
ordertype A r = ord_of_nat m
small A
wf r
total_on A r
\<lbrakk>wf ?r; total_on ?A ?r; small ?A\<rbrakk> \<Longrightarrow> bij_betw (ordermap ?A ?r) ?A (elts (ordertype ?A ?r))

goal (1 subgoal):
 1. A \<approx> elts (ord_of_nat m)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A \<approx> elts (ord_of_nat m)

goal (1 subgoal):
 1. finite A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<approx> elts (ord_of_nat m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<approx> elts (ord_of_nat m)

goal (1 subgoal):
 1. finite A
[PROOF STEP]
using eqpoll_finite_iff finite_Ord_omega
[PROOF STATE]
proof (prove)
using this:
A \<approx> elts (ord_of_nat m)
?A \<approx> ?B \<Longrightarrow> finite ?A = finite ?B
?\<alpha> \<in> elts \<omega> \<Longrightarrow> finite (elts ?\<alpha>)

goal (1 subgoal):
 1. finite A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_ordertype_eqpoll:
  assumes "wf r" "total_on A r" "small A"
  shows "elts (ordertype A r) \<approx> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (ordertype A r) \<approx> A
[PROOF STEP]
using assms eqpoll_def eqpoll_sym ordermap_bij
[PROOF STATE]
proof (prove)
using this:
wf r
total_on A r
small A
?A \<approx> ?B \<equiv> \<exists>f. bij_betw f ?A ?B
?A \<approx> ?B \<Longrightarrow> ?B \<approx> ?A
\<lbrakk>wf ?r; total_on ?A ?r; small ?A\<rbrakk> \<Longrightarrow> bij_betw (ordermap ?A ?r) ?A (elts (ordertype ?A ?r))

goal (1 subgoal):
 1. elts (ordertype A r) \<approx> A
[PROOF STEP]
by blast


[STATEMENT]
lemma ordertype_eqpoll:
  assumes "small A"
  shows "elts (ordertype A VWF) \<approx> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (ordertype A VWF) \<approx> A
[PROOF STEP]
using assms wf_ordertype_eqpoll total_VWF wf_VWF
[PROOF STATE]
proof (prove)
using this:
small A
\<lbrakk>wf ?r; total_on ?A ?r; small ?A\<rbrakk> \<Longrightarrow> elts (ordertype ?A ?r) \<approx> ?A
total VWF
wf VWF

goal (1 subgoal):
 1. elts (ordertype A VWF) \<approx> A
[PROOF STEP]
by (simp add: wf_ordertype_eqpoll total_on_def)


[STATEMENT]
lemma ordermap_VWF_0 [simp]: "ordermap A VWF 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap A VWF 0 = 0
[PROOF STEP]
by (simp add: ordermap wf_VWO VWF_def)


[STATEMENT]
lemma ordertype_empty [simp]: "ordertype {} r = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype {} r = 0
[PROOF STEP]
by (simp add: ordertype_def)


[STATEMENT]
lemma ordertype_eq_0_iff [simp]: "\<lbrakk>small X; wf r\<rbrakk> \<Longrightarrow> ordertype X r = 0 \<longleftrightarrow> X = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>small X; wf r\<rbrakk> \<Longrightarrow> (ordertype X r = 0) = (X = {})
[PROOF STEP]
by (metis ordertype_def elts_of_set replacement image_is_empty zero_V_def)


[STATEMENT]
lemma ordermap_mono_less:
  assumes "(w, x) \<in> r"
      and "wf r" "trans r"
      and "w \<in> A" "x \<in> A"
      and "small A"
    shows "ordermap A r w < ordermap A r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap A r w < ordermap A r x
[PROOF STEP]
by (simp add: OrdmemD assms ordermap_mono)


[STATEMENT]
lemma ordermap_mono_le:
  assumes "(w, x) \<in> r \<or> w=x"
      and "wf r" "trans r"
      and "w \<in> A" "x \<in> A"
      and "small A"
    shows "ordermap A r w \<le> ordermap A r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap A r w \<le> ordermap A r x
[PROOF STEP]
by (metis assms dual_order.strict_implies_order eq_refl ordermap_mono_less)


[STATEMENT]
lemma converse_ordermap_le_mono:
  assumes "ordermap A r y \<le> ordermap A r x" "wf r" "total r"  "x \<in> A" "small A"
  shows "(y, x) \<in> r \<or> y=x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y, x) \<in> r \<or> y = x
[PROOF STEP]
by (meson UNIV_I assms mem_not_refl ordermap_mono total_on_def vsubsetD)


[STATEMENT]
lemma ordertype_mono:
  assumes "X \<subseteq> Y" and r: "wf r" "trans r" and "small Y"
  shows "ordertype X r \<le> ordertype Y r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype X r \<le> ordertype Y r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype X r \<le> ordertype Y r
[PROOF STEP]
have "small X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small X
[PROOF STEP]
using assms smaller_than_small
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Y
wf r
trans r
small Y
\<lbrakk>small ?A; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> small ?B

goal (1 subgoal):
 1. small X
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
small X

goal (1 subgoal):
 1. ordertype X r \<le> ordertype Y r
[PROOF STEP]
have *: "ordermap X r x \<le> ordermap Y r x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap X r x \<le> ordermap Y r x
[PROOF STEP]
using \<open>wf r\<close>
[PROOF STATE]
proof (prove)
using this:
wf r

goal (1 subgoal):
 1. ordermap X r x \<le> ordermap Y r x
[PROOF STEP]
proof (induction x rule: wf_induct_rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> r \<Longrightarrow> ordermap X r y \<le> ordermap Y r y) \<Longrightarrow> ordermap X r x \<le> ordermap Y r x
[PROOF STEP]
case (less x)
[PROOF STATE]
proof (state)
this:
(?y, x) \<in> r \<Longrightarrow> ordermap X r ?y \<le> ordermap Y r ?y

goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> r \<Longrightarrow> ordermap X r y \<le> ordermap Y r y) \<Longrightarrow> ordermap X r x \<le> ordermap Y r x
[PROOF STEP]
have "ordermap X r z < ordermap Y r x" if "z \<in> X" and zx: "(z,x) \<in> r" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap X r z < ordermap Y r x
[PROOF STEP]
using less [OF zx] assms
[PROOF STATE]
proof (prove)
using this:
ordermap X r z \<le> ordermap Y r z
X \<subseteq> Y
wf r
trans r
small Y

goal (1 subgoal):
 1. ordermap X r z < ordermap Y r x
[PROOF STEP]
by (meson Ord_linear2 OrdmemD wf_Ord_ordermap ordermap_mono in_mono leD that(1) vsubsetD zx)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?z \<in> X; (?z, x) \<in> r\<rbrakk> \<Longrightarrow> ordermap X r ?z < ordermap Y r x

goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> r \<Longrightarrow> ordermap X r y \<le> ordermap Y r y) \<Longrightarrow> ordermap X r x \<le> ordermap Y r x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?z \<in> X; (?z, x) \<in> r\<rbrakk> \<Longrightarrow> ordermap X r ?z < ordermap Y r x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?z \<in> X; (?z, x) \<in> r\<rbrakk> \<Longrightarrow> ordermap X r ?z < ordermap Y r x

goal (1 subgoal):
 1. ordermap X r x \<le> ordermap Y r x
[PROOF STEP]
by (auto simp add: ordermap [of _ X x] \<open>small X\<close> Ord_mem_iff_lt set_image_le_iff less_eq_V_def r)
[PROOF STATE]
proof (state)
this:
ordermap X r x \<le> ordermap Y r x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ordermap X r ?x \<le> ordermap Y r ?x

goal (1 subgoal):
 1. ordertype X r \<le> ordertype Y r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype X r \<le> ordertype Y r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype X r \<le> ordertype Y r
[PROOF STEP]
have "ordermap Y r ` Y = elts (ordertype Y r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap Y r ` Y = elts (ordertype Y r)
[PROOF STEP]
by (metis ordertype_def \<open>small Y\<close> elts_of_set replacement)
[PROOF STATE]
proof (state)
this:
ordermap Y r ` Y = elts (ordertype Y r)

goal (1 subgoal):
 1. ordertype X r \<le> ordertype Y r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ordermap Y r ` Y = elts (ordertype Y r)
[PROOF STEP]
have "ordertype Y r \<notin> ordermap X r ` X"
[PROOF STATE]
proof (prove)
using this:
ordermap Y r ` Y = elts (ordertype Y r)

goal (1 subgoal):
 1. ordertype Y r \<notin> ordermap X r ` X
[PROOF STEP]
using "*" \<open>X \<subseteq> Y\<close>
[PROOF STATE]
proof (prove)
using this:
ordermap Y r ` Y = elts (ordertype Y r)
ordermap X r ?x \<le> ordermap Y r ?x
X \<subseteq> Y

goal (1 subgoal):
 1. ordertype Y r \<notin> ordermap X r ` X
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ordertype Y r \<notin> ordermap X r ` X

goal (1 subgoal):
 1. ordertype X r \<le> ordertype Y r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ordertype Y r \<notin> ordermap X r ` X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ordertype Y r \<notin> ordermap X r ` X

goal (1 subgoal):
 1. ordertype X r \<le> ordertype Y r
[PROOF STEP]
by (metis Ord_linear2 Ord_mem_iff_lt ordertype_def wf_Ord_ordertype \<open>small X\<close> elts_of_set replacement r)
[PROOF STATE]
proof (state)
this:
ordertype X r \<le> ordertype Y r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ordertype X r \<le> ordertype Y r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_UNION_ge:
  assumes "A \<in> \<A>" "wf r" "trans r" "\<A> \<subseteq> Collect small" "small \<A>"
  shows "ordertype A r \<le> ordertype (\<Union>\<A>) r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype A r \<le> ordertype (\<Union> \<A>) r
[PROOF STEP]
by (rule ordertype_mono) (use assms in auto)


[STATEMENT]
lemma inv_ordermap_mono_less:
  assumes "(inv_into M (ordermap M r) \<alpha>, inv_into M (ordermap M r) \<beta>) \<in> r"
    and "small M" and \<alpha>: "\<alpha> \<in> elts (ordertype M r)" and \<beta>: "\<beta> \<in> elts (ordertype M r)"
    and "wf r" "trans r"
  shows "\<alpha> < \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> < \<beta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> < \<beta>
[PROOF STEP]
have "\<alpha> = ordermap M r (inv_into M (ordermap M r) \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> = ordermap M r (inv_into M (ordermap M r) \<alpha>)
[PROOF STEP]
by (metis \<alpha> f_inv_into_f ordermap_surj subset_eq)
[PROOF STATE]
proof (state)
this:
\<alpha> = ordermap M r (inv_into M (ordermap M r) \<alpha>)

goal (1 subgoal):
 1. \<alpha> < \<beta>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<alpha> = ordermap M r (inv_into M (ordermap M r) \<alpha>)

goal (1 subgoal):
 1. \<alpha> < \<beta>
[PROOF STEP]
have "\<dots> < ordermap M r (inv_into M (ordermap M r) \<beta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap M r (inv_into M (ordermap M r) \<alpha>) < ordermap M r (inv_into M (ordermap M r) \<beta>)
[PROOF STEP]
by (meson \<alpha> \<beta> assms in_mono inv_into_into ordermap_mono_less ordermap_surj)
[PROOF STATE]
proof (state)
this:
ordermap M r (inv_into M (ordermap M r) \<alpha>) < ordermap M r (inv_into M (ordermap M r) \<beta>)

goal (1 subgoal):
 1. \<alpha> < \<beta>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ordermap M r (inv_into M (ordermap M r) \<alpha>) < ordermap M r (inv_into M (ordermap M r) \<beta>)

goal (1 subgoal):
 1. \<alpha> < \<beta>
[PROOF STEP]
have "\<dots> = \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap M r (inv_into M (ordermap M r) \<beta>) = \<beta>
[PROOF STEP]
by (meson \<beta> f_inv_into_f in_mono ordermap_surj)
[PROOF STATE]
proof (state)
this:
ordermap M r (inv_into M (ordermap M r) \<beta>) = \<beta>

goal (1 subgoal):
 1. \<alpha> < \<beta>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<alpha> < \<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha> < \<beta>

goal (1 subgoal):
 1. \<alpha> < \<beta>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<alpha> < \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_ordermap_mono_eq:
  assumes "inv_into M (ordermap M r) \<alpha> = inv_into M (ordermap M r) \<beta>"
    and "\<alpha> \<in> elts (ordertype M r)" "\<beta> \<in> elts (ordertype M r)"
  shows "\<alpha> = \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
by (metis assms f_inv_into_f ordermap_surj subsetD)


[STATEMENT]
lemma inv_ordermap_VWF_mono_le:
  assumes "inv_into M (ordermap M VWF) \<alpha> \<le> inv_into M (ordermap M VWF) \<beta>"
    and "M \<subseteq> ON" "small M" and \<alpha>: "\<alpha> \<in> elts (ordertype M VWF)" and \<beta>: "\<beta> \<in> elts (ordertype M VWF)"
  shows "\<alpha> \<le> \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<le> \<beta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> \<le> \<beta>
[PROOF STEP]
have "\<alpha> = ordermap M VWF (inv_into M (ordermap M VWF) \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> = ordermap M VWF (inv_into M (ordermap M VWF) \<alpha>)
[PROOF STEP]
by (metis \<alpha> f_inv_into_f ordermap_surj subset_eq)
[PROOF STATE]
proof (state)
this:
\<alpha> = ordermap M VWF (inv_into M (ordermap M VWF) \<alpha>)

goal (1 subgoal):
 1. \<alpha> \<le> \<beta>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<alpha> = ordermap M VWF (inv_into M (ordermap M VWF) \<alpha>)

goal (1 subgoal):
 1. \<alpha> \<le> \<beta>
[PROOF STEP]
have "\<dots> \<le> ordermap M VWF (inv_into M (ordermap M VWF) \<beta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap M VWF (inv_into M (ordermap M VWF) \<alpha>) \<le> ordermap M VWF (inv_into M (ordermap M VWF) \<beta>)
[PROOF STEP]
by (metis ON_imp_Ord VWF_iff_Ord_less assms dual_order.strict_implies_order elts_of_set eq_refl inv_into_into order.not_eq_order_implies_strict ordermap_mono_less ordertype_def replacement trans_VWF wf_VWF)
[PROOF STATE]
proof (state)
this:
ordermap M VWF (inv_into M (ordermap M VWF) \<alpha>) \<le> ordermap M VWF (inv_into M (ordermap M VWF) \<beta>)

goal (1 subgoal):
 1. \<alpha> \<le> \<beta>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ordermap M VWF (inv_into M (ordermap M VWF) \<alpha>) \<le> ordermap M VWF (inv_into M (ordermap M VWF) \<beta>)

goal (1 subgoal):
 1. \<alpha> \<le> \<beta>
[PROOF STEP]
have "\<dots> = \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap M VWF (inv_into M (ordermap M VWF) \<beta>) = \<beta>
[PROOF STEP]
by (meson \<beta> f_inv_into_f in_mono ordermap_surj)
[PROOF STATE]
proof (state)
this:
ordermap M VWF (inv_into M (ordermap M VWF) \<beta>) = \<beta>

goal (1 subgoal):
 1. \<alpha> \<le> \<beta>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<le> \<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<le> \<beta>

goal (1 subgoal):
 1. \<alpha> \<le> \<beta>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<alpha> \<le> \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_ordermap_VWF_mono_iff:
  assumes "M \<subseteq> ON" "small M" and "\<alpha> \<in> elts (ordertype M VWF)" and "\<beta> \<in> elts (ordertype M VWF)"
  shows "inv_into M (ordermap M VWF) \<alpha> \<le> inv_into M (ordermap M VWF) \<beta> \<longleftrightarrow> \<alpha> \<le> \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inv_into M (ordermap M VWF) \<alpha> \<le> inv_into M (ordermap M VWF) \<beta>) = (\<alpha> \<le> \<beta>)
[PROOF STEP]
by (metis ON_imp_Ord Ord_linear_le assms dual_order.eq_iff inv_into_ordermap inv_ordermap_VWF_mono_le)


[STATEMENT]
lemma inv_ordermap_VWF_strict_mono_iff:
  assumes "M \<subseteq> ON" "small M" and "\<alpha> \<in> elts (ordertype M VWF)" and "\<beta> \<in> elts (ordertype M VWF)"
  shows "inv_into M (ordermap M VWF) \<alpha> < inv_into M (ordermap M VWF) \<beta> \<longleftrightarrow> \<alpha> < \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inv_into M (ordermap M VWF) \<alpha> < inv_into M (ordermap M VWF) \<beta>) = (\<alpha> < \<beta>)
[PROOF STEP]
by (simp add: assms inv_ordermap_VWF_mono_iff less_le_not_le)


[STATEMENT]
lemma strict_mono_on_ordertype:
  assumes "M \<subseteq> ON" "small M"
  obtains f where "f \<in> elts (ordertype M VWF) \<rightarrow> M" "strict_mono_on (elts (ordertype M VWF)) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> elts (ordertype M VWF) \<rightarrow> M; strict_mono_on (elts (ordertype M VWF)) f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>f. \<lbrakk>f \<in> elts (ordertype M VWF) \<rightarrow> M; strict_mono_on (elts (ordertype M VWF)) f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?f2 \<in> elts (ordertype M VWF) \<rightarrow> M
 2. (\<And>f. \<lbrakk>f \<in> elts (ordertype M VWF) \<rightarrow> M; strict_mono_on (elts (ordertype M VWF)) f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> strict_mono_on (elts (ordertype M VWF)) ?f2
[PROOF STEP]
show "inv_into M (ordermap M VWF) \<in> elts (ordertype M VWF) \<rightarrow> M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_into M (ordermap M VWF) \<in> elts (ordertype M VWF) \<rightarrow> M
[PROOF STEP]
by (meson Pi_I' in_mono inv_into_into ordermap_surj)
[PROOF STATE]
proof (state)
this:
inv_into M (ordermap M VWF) \<in> elts (ordertype M VWF) \<rightarrow> M

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> elts (ordertype M VWF) \<rightarrow> M; strict_mono_on (elts (ordertype M VWF)) f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> strict_mono_on (elts (ordertype M VWF)) (inv_into M (ordermap M VWF))
[PROOF STEP]
show "strict_mono_on (elts (ordertype M VWF)) (inv_into M (ordermap M VWF))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono_on (elts (ordertype M VWF)) (inv_into M (ordermap M VWF))
[PROOF STEP]
proof (clarsimp simp: strict_mono_on_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>r \<in> elts (ordertype M VWF); s \<in> elts (ordertype M VWF); r < s\<rbrakk> \<Longrightarrow> inv_into M (ordermap M VWF) r < inv_into M (ordermap M VWF) s
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>r \<in> elts (ordertype M VWF); s \<in> elts (ordertype M VWF); r < s\<rbrakk> \<Longrightarrow> inv_into M (ordermap M VWF) r < inv_into M (ordermap M VWF) s
[PROOF STEP]
assume "x \<in> elts (ordertype M VWF)" "y \<in> elts (ordertype M VWF)" "x < y"
[PROOF STATE]
proof (state)
this:
x \<in> elts (ordertype M VWF)
y \<in> elts (ordertype M VWF)
x < y

goal (1 subgoal):
 1. \<And>r s. \<lbrakk>r \<in> elts (ordertype M VWF); s \<in> elts (ordertype M VWF); r < s\<rbrakk> \<Longrightarrow> inv_into M (ordermap M VWF) r < inv_into M (ordermap M VWF) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> elts (ordertype M VWF)
y \<in> elts (ordertype M VWF)
x < y
[PROOF STEP]
show "inv_into M (ordermap M VWF) x < inv_into M (ordermap M VWF) y"
[PROOF STATE]
proof (prove)
using this:
x \<in> elts (ordertype M VWF)
y \<in> elts (ordertype M VWF)
x < y

goal (1 subgoal):
 1. inv_into M (ordermap M VWF) x < inv_into M (ordermap M VWF) y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> elts (ordertype M VWF)
y \<in> elts (ordertype M VWF)
x < y
M \<subseteq> ON
small M

goal (1 subgoal):
 1. inv_into M (ordermap M VWF) x < inv_into M (ordermap M VWF) y
[PROOF STEP]
by (meson ON_imp_Ord Ord_linear2 inv_into_into inv_ordermap_VWF_mono_le leD ordermap_surj subsetD)
[PROOF STATE]
proof (state)
this:
inv_into M (ordermap M VWF) x < inv_into M (ordermap M VWF) y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
strict_mono_on (elts (ordertype M VWF)) (inv_into M (ordermap M VWF))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordermap_inc_eq:
  assumes "x \<in> A" "small A"
    and \<pi>: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (x,y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> x, \<pi> y) \<in> s"
    and r: "wf r" "total_on A r" and "wf s"
  shows "ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
using \<open>wf r\<close> \<open>x \<in> A\<close>
[PROOF STATE]
proof (prove)
using this:
wf r
x \<in> A

goal (1 subgoal):
 1. ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
proof (induction x rule: wf_induct_rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> r; y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> y) = ordermap A r y; x \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
case (less x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?y, x) \<in> r; ?y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> ?y) = ordermap A r ?y
x \<in> A

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> r; y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> y) = ordermap A r y; x \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?y, x) \<in> r; ?y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> ?y) = ordermap A r ?y
x \<in> A
[PROOF STEP]
have 1: "{y \<in> A. (y, x) \<in> r} = A \<inter> {y. (y, x) \<in> r}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?y, x) \<in> r; ?y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> ?y) = ordermap A r ?y
x \<in> A

goal (1 subgoal):
 1. {y \<in> A. (y, x) \<in> r} = A \<inter> {y. (y, x) \<in> r}
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?y, x) \<in> r; ?y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> ?y) = ordermap A r ?y
x \<in> A
wf r
total_on A r

goal (1 subgoal):
 1. {y \<in> A. (y, x) \<in> r} = A \<inter> {y. (y, x) \<in> r}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{y \<in> A. (y, x) \<in> r} = A \<inter> {y. (y, x) \<in> r}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> r; y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> y) = ordermap A r y; x \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
have 2: "{y \<in> \<pi> ` A. (y, \<pi> x) \<in> s} = \<pi> ` A \<inter> {y. (y, \<pi> x) \<in> s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y \<in> \<pi> ` A. (y, \<pi> x) \<in> s} = \<pi> ` A \<inter> {y. (y, \<pi> x) \<in> s}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{y \<in> \<pi> ` A. (y, \<pi> x) \<in> s} = \<pi> ` A \<inter> {y. (y, \<pi> x) \<in> s}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> r; y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> y) = ordermap A r y; x \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
have inv\<pi>: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (\<pi> x, \<pi> y) \<in> s\<rbrakk> \<Longrightarrow> (x, y) \<in> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; (\<pi> x, \<pi> y) \<in> s\<rbrakk> \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
by (metis \<pi> \<open>wf s\<close> \<open>total_on A r\<close> total_on_def wf_not_sym)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> A; ?y \<in> A; (\<pi> ?x, \<pi> ?y) \<in> s\<rbrakk> \<Longrightarrow> (?x, ?y) \<in> r

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> r; y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> y) = ordermap A r y; x \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
have eq: "f ` (\<pi> ` A \<inter> {y. (y, \<pi> x) \<in> s}) = (f \<circ> \<pi>) ` (A \<inter> {y. (y, x) \<in> r})" for f :: "'b \<Rightarrow> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` (\<pi> ` A \<inter> {y. (y, \<pi> x) \<in> s}) = (f \<circ> \<pi>) ` (A \<inter> {y. (y, x) \<in> r})
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?y, x) \<in> r; ?y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> ?y) = ordermap A r ?y
x \<in> A

goal (1 subgoal):
 1. f ` (\<pi> ` A \<inter> {y. (y, \<pi> x) \<in> s}) = (f \<circ> \<pi>) ` (A \<inter> {y. (y, x) \<in> r})
[PROOF STEP]
by (auto simp: image_subset_iff inv\<pi> \<pi>)
[PROOF STATE]
proof (state)
this:
?f ` (\<pi> ` A \<inter> {y. (y, \<pi> x) \<in> s}) = (?f \<circ> \<pi>) ` (A \<inter> {y. (y, x) \<in> r})

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> r; y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> y) = ordermap A r y; x \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?y, x) \<in> r; ?y \<in> A\<rbrakk> \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> ?y) = ordermap A r ?y
x \<in> A

goal (1 subgoal):
 1. ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
by (simp add: ordermap [OF \<open>wf r\<close>, of _ x] ordermap [OF \<open>wf s\<close>, of _ "\<pi> x"] 1 2 eq)
[PROOF STATE]
proof (state)
this:
ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_inc_eq:
  assumes "small A"
    and \<pi>: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (x,y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> x, \<pi> y) \<in> s"
    and r: "wf r" "total_on A r" and "wf s"
  shows "ordertype (\<pi> ` A) s = ordertype A r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (\<pi> ` A) s = ordertype A r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype (\<pi> ` A) s = ordertype A r
[PROOF STEP]
have "ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x" if "x \<in> A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
using assms that
[PROOF STATE]
proof (prove)
using this:
small A
\<lbrakk>?x \<in> A; ?y \<in> A; (?x, ?y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> ?x, \<pi> ?y) \<in> s
wf r
total_on A r
wf s
x \<in> A

goal (1 subgoal):
 1. ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x
[PROOF STEP]
by (auto simp: ordermap_inc_eq)
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> ?x) = ordermap A r ?x

goal (1 subgoal):
 1. ordertype (\<pi> ` A) s = ordertype A r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> A \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> ?x) = ordermap A r ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> ?x) = ordermap A r ?x

goal (1 subgoal):
 1. ordertype (\<pi> ` A) s = ordertype A r
[PROOF STEP]
unfolding ordertype_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> ordermap (\<pi> ` A) s (\<pi> ?x) = ordermap A r ?x

goal (1 subgoal):
 1. set (ordermap (\<pi> ` A) s ` \<pi> ` A) = set (ordermap A r ` A)
[PROOF STEP]
by (metis (no_types, lifting) image_cong image_image)
[PROOF STATE]
proof (state)
this:
ordertype (\<pi> ` A) s = ordertype A r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_inc_le:
  assumes "small A" "small B"
    and \<pi>: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (x,y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> x, \<pi> y) \<in> s"
    and r: "wf r" "total_on A r" and "wf s" "trans s"
    and "\<pi> ` A \<subseteq> B"
  shows "ordertype A r \<le> ordertype B s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype A r \<le> ordertype B s
[PROOF STEP]
by (metis assms ordertype_inc_eq ordertype_mono)


[STATEMENT]
lemma ordertype_image_ordermap:
  assumes "small A" "X \<subseteq> A" "wf r" "trans r" "total_on X r"
  shows "ordertype (ordermap A r ` X) VWF = ordertype X r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (ordermap A r ` X) VWF = ordertype X r
[PROOF STEP]
proof (rule ordertype_inc_eq)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. small X
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X; (x, y) \<in> r\<rbrakk> \<Longrightarrow> (ordermap A r x, ordermap A r y) \<in> VWF
 3. wf r
 4. total_on X r
 5. wf VWF
[PROOF STEP]
show "small X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small X
[PROOF STEP]
by (meson assms smaller_than_small)
[PROOF STATE]
proof (state)
this:
small X

goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X; (x, y) \<in> r\<rbrakk> \<Longrightarrow> (ordermap A r x, ordermap A r y) \<in> VWF
 2. wf r
 3. total_on X r
 4. wf VWF
[PROOF STEP]
show "(ordermap A r x, ordermap A r y) \<in> VWF"
    if "x \<in> X" "y \<in> X" "(x, y) \<in> r" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ordermap A r x, ordermap A r y) \<in> VWF
[PROOF STEP]
by (meson that wf_Ord_ordermap VWF_iff_Ord_less assms ordermap_mono_less subsetD)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> X; ?y \<in> X; (?x, ?y) \<in> r\<rbrakk> \<Longrightarrow> (ordermap A r ?x, ordermap A r ?y) \<in> VWF

goal (3 subgoals):
 1. wf r
 2. total_on X r
 3. wf VWF
[PROOF STEP]
qed (use assms in auto)


[STATEMENT]
lemma ordertype_map_image:
  assumes "B \<subseteq> A" "small A"
  shows "ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF
[PROOF STEP]
have "ordermap A VWF ` A - ordermap A VWF ` B = ordermap A VWF ` (A - B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap A VWF ` A - ordermap A VWF ` B = ordermap A VWF ` (A - B)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A
small A

goal (1 subgoal):
 1. ordermap A VWF ` A - ordermap A VWF ` B = ordermap A VWF ` (A - B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ordermap A VWF ` A - ordermap A VWF ` B = ordermap A VWF ` (A - B)

goal (1 subgoal):
 1. ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ordermap A VWF ` A - ordermap A VWF ` B = ordermap A VWF ` (A - B)
[PROOF STEP]
have "ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (ordermap A VWF ` (A - B)) VWF"
[PROOF STATE]
proof (prove)
using this:
ordermap A VWF ` A - ordermap A VWF ` B = ordermap A VWF ` (A - B)

goal (1 subgoal):
 1. ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (ordermap A VWF ` (A - B)) VWF
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (ordermap A VWF ` (A - B)) VWF

goal (1 subgoal):
 1. ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (ordermap A VWF ` (A - B)) VWF

goal (1 subgoal):
 1. ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF
[PROOF STEP]
have "\<dots> = ordertype (A - B) VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (ordermap A VWF ` (A - B)) VWF = ordertype (A - B) VWF
[PROOF STEP]
using \<open>small A\<close> ordertype_image_ordermap
[PROOF STATE]
proof (prove)
using this:
small A
\<lbrakk>small ?A; ?X \<subseteq> ?A; wf ?r; trans ?r; total_on ?X ?r\<rbrakk> \<Longrightarrow> ordertype (ordermap ?A ?r ` ?X) VWF = ordertype ?X ?r

goal (1 subgoal):
 1. ordertype (ordermap A VWF ` (A - B)) VWF = ordertype (A - B) VWF
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ordertype (ordermap A VWF ` (A - B)) VWF = ordertype (A - B) VWF

goal (1 subgoal):
 1. ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF

goal (1 subgoal):
 1. ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iso_imp_ordertype_eq_ordertype:
  assumes iso: "iso r r' f"
    and "wf r"
    and "Total r"
    and sm: "small (Field r)"
  shows "ordertype (Field r) r = ordertype (Field r') r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (Field r) r = ordertype (Field r') r'
[PROOF STEP]
by (metis (no_types, lifting) iso_forward iso_wf assms iso_Field ordertype_inc_eq sm)


[STATEMENT]
lemma ordertype_infinite_ge_\<omega>:
  assumes "infinite A" "small A"
  shows "ordertype A VWF \<ge> \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> \<le> ordertype A VWF
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<omega> \<le> ordertype A VWF
[PROOF STEP]
have "inj_on (ordermap A VWF) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (ordermap A VWF) A
[PROOF STEP]
by (meson ordermap_bij \<open>small A\<close> bij_betw_def total_on_VWF wf_VWF)
[PROOF STATE]
proof (state)
this:
inj_on (ordermap A VWF) A

goal (1 subgoal):
 1. \<omega> \<le> ordertype A VWF
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj_on (ordermap A VWF) A
[PROOF STEP]
have "infinite (ordermap A VWF ` A)"
[PROOF STATE]
proof (prove)
using this:
inj_on (ordermap A VWF) A

goal (1 subgoal):
 1. infinite (ordermap A VWF ` A)
[PROOF STEP]
using \<open>infinite A\<close> finite_image_iff
[PROOF STATE]
proof (prove)
using this:
inj_on (ordermap A VWF) A
infinite A
inj_on ?f ?A \<Longrightarrow> finite (?f ` ?A) = finite ?A

goal (1 subgoal):
 1. infinite (ordermap A VWF ` A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite (ordermap A VWF ` A)

goal (1 subgoal):
 1. \<omega> \<le> ordertype A VWF
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite (ordermap A VWF ` A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite (ordermap A VWF ` A)

goal (1 subgoal):
 1. \<omega> \<le> ordertype A VWF
[PROOF STEP]
using Ord_ordertype \<open>small A\<close> infinite_Ord_omega
[PROOF STATE]
proof (prove)
using this:
infinite (ordermap A VWF ` A)
Ord (ordertype ?A VWF)
small A
\<lbrakk>Ord ?\<alpha>; infinite (elts ?\<alpha>)\<rbrakk> \<Longrightarrow> \<omega> \<le> ?\<alpha>

goal (1 subgoal):
 1. \<omega> \<le> ordertype A VWF
[PROOF STEP]
by (auto simp: ordertype_def)
[PROOF STATE]
proof (state)
this:
\<omega> \<le> ordertype A VWF

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_eqI:
  assumes "wf r" "total_on A r" "small A" "wf s"
          "bij_betw f A B" "(\<forall>x \<in> A. \<forall>y \<in> A. (f x, f y) \<in> s \<longleftrightarrow> (x,y) \<in> r)"
  shows "ordertype A r = ordertype B s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype A r = ordertype B s
[PROOF STEP]
by (metis assms bij_betw_imp_surj_on ordertype_inc_eq)


[STATEMENT]
lemma ordermap_eq_self:
  assumes "Ord \<alpha>" and x: "x \<in> elts \<alpha>"
  shows "ordermap (elts \<alpha>) VWF x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap (elts \<alpha>) VWF x = x
[PROOF STEP]
using Ord_in_Ord [OF assms] x
[PROOF STATE]
proof (prove)
using this:
Ord x
x \<in> elts \<alpha>

goal (1 subgoal):
 1. ordermap (elts \<alpha>) VWF x = x
[PROOF STEP]
proof (induction x rule: Ord_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ord x; \<And>y. \<lbrakk>y \<in> elts x; y \<in> elts \<alpha>\<rbrakk> \<Longrightarrow> ordermap (elts \<alpha>) VWF y = y; x \<in> elts \<alpha>\<rbrakk> \<Longrightarrow> ordermap (elts \<alpha>) VWF x = x
[PROOF STEP]
case (step x)
[PROOF STATE]
proof (state)
this:
Ord x
\<lbrakk>?y \<in> elts x; ?y \<in> elts \<alpha>\<rbrakk> \<Longrightarrow> ordermap (elts \<alpha>) VWF ?y = ?y
x \<in> elts \<alpha>

goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ord x; \<And>y. \<lbrakk>y \<in> elts x; y \<in> elts \<alpha>\<rbrakk> \<Longrightarrow> ordermap (elts \<alpha>) VWF y = y; x \<in> elts \<alpha>\<rbrakk> \<Longrightarrow> ordermap (elts \<alpha>) VWF x = x
[PROOF STEP]
have 1: "{y \<in> elts \<alpha>. (y, x) \<in> VWF} = elts x" (is "?A = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y \<in> elts \<alpha>. (y, x) \<in> VWF} = elts x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {y \<in> elts \<alpha>. (y, x) \<in> VWF} \<subseteq> elts x
 2. elts x \<subseteq> {y \<in> elts \<alpha>. (y, x) \<in> VWF}
[PROOF STEP]
show "?A \<subseteq> elts x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y \<in> elts \<alpha>. (y, x) \<in> VWF} \<subseteq> elts x
[PROOF STEP]
using \<open>Ord \<alpha>\<close>
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>

goal (1 subgoal):
 1. {y \<in> elts \<alpha>. (y, x) \<in> VWF} \<subseteq> elts x
[PROOF STEP]
by clarify (meson Ord_in_Ord Ord_mem_iff_lt VWF_iff_Ord_less step.hyps)
[PROOF STATE]
proof (state)
this:
{y \<in> elts \<alpha>. (y, x) \<in> VWF} \<subseteq> elts x

goal (1 subgoal):
 1. elts x \<subseteq> {y \<in> elts \<alpha>. (y, x) \<in> VWF}
[PROOF STEP]
show "elts x \<subseteq> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts x \<subseteq> {y \<in> elts \<alpha>. (y, x) \<in> VWF}
[PROOF STEP]
using \<open>Ord \<alpha>\<close>
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>

goal (1 subgoal):
 1. elts x \<subseteq> {y \<in> elts \<alpha>. (y, x) \<in> VWF}
[PROOF STEP]
by clarify (meson Ord_in_Ord Ord_trans OrdmemD VWF_iff_Ord_less step.prems)
[PROOF STATE]
proof (state)
this:
elts x \<subseteq> {y \<in> elts \<alpha>. (y, x) \<in> VWF}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{y \<in> elts \<alpha>. (y, x) \<in> VWF} = elts x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ord x; \<And>y. \<lbrakk>y \<in> elts x; y \<in> elts \<alpha>\<rbrakk> \<Longrightarrow> ordermap (elts \<alpha>) VWF y = y; x \<in> elts \<alpha>\<rbrakk> \<Longrightarrow> ordermap (elts \<alpha>) VWF x = x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap (elts \<alpha>) VWF x = x
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
Ord x
\<lbrakk>?y \<in> elts x; ?y \<in> elts \<alpha>\<rbrakk> \<Longrightarrow> ordermap (elts \<alpha>) VWF ?y = ?y
x \<in> elts \<alpha>

goal (1 subgoal):
 1. ordermap (elts \<alpha>) VWF x = x
[PROOF STEP]
by (simp add: ordermap [OF wf_VWF, of _ x] 1 Ord_trans [of _ _ \<alpha>] step.prems \<open>Ord \<alpha>\<close> cong: image_cong)
[PROOF STATE]
proof (state)
this:
ordermap (elts \<alpha>) VWF x = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_eq_Ord [simp]:
  assumes "Ord \<alpha>"
  shows "ordertype (elts \<alpha>) VWF = \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (elts \<alpha>) VWF = \<alpha>
[PROOF STEP]
using assms ordermap_eq_self [OF assms]
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>
?x \<in> elts \<alpha> \<Longrightarrow> ordermap (elts \<alpha>) VWF ?x = ?x

goal (1 subgoal):
 1. ordertype (elts \<alpha>) VWF = \<alpha>
[PROOF STEP]
by (simp add: ordertype_def)


[STATEMENT]
lemma ordertype_le_Ord:
  assumes "Ord \<alpha>" "X \<subseteq> elts \<alpha>"
  shows "ordertype X VWF \<le> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype X VWF \<le> \<alpha>
[PROOF STEP]
by (metis assms ordertype_VWF_mono ordertype_eq_Ord small_elts)


[STATEMENT]
lemma ordertype_inc_le_Ord:
  assumes "small A" "Ord \<alpha>"
    and \<pi>: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (x,y) \<in> r\<rbrakk> \<Longrightarrow> \<pi> x < \<pi> y"
    and "wf r" "total_on A r"
    and sub: "\<pi> ` A \<subseteq> elts \<alpha>"
  shows "ordertype A r \<le> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype A r \<le> \<alpha>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype A r \<le> \<alpha>
[PROOF STEP]
have "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (x,y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> x, \<pi> y) \<in> VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; (x, y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> x, \<pi> y) \<in> VWF
[PROOF STEP]
by (meson Ord_in_Ord VWF_iff_Ord_less \<pi> \<open>Ord \<alpha>\<close> sub image_subset_iff)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> A; ?y \<in> A; (?x, ?y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> ?x, \<pi> ?y) \<in> VWF

goal (1 subgoal):
 1. ordertype A r \<le> \<alpha>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
small A
Ord \<alpha>
\<lbrakk>?x \<in> A; ?y \<in> A; (?x, ?y) \<in> r\<rbrakk> \<Longrightarrow> \<pi> ?x < \<pi> ?y
wf r
total_on A r
\<pi> ` A \<subseteq> elts \<alpha>
\<lbrakk>?x \<in> A; ?y \<in> A; (?x, ?y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> ?x, \<pi> ?y) \<in> VWF
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
small A
Ord \<alpha>
\<lbrakk>?x \<in> A; ?y \<in> A; (?x, ?y) \<in> r\<rbrakk> \<Longrightarrow> \<pi> ?x < \<pi> ?y
wf r
total_on A r
\<pi> ` A \<subseteq> elts \<alpha>
\<lbrakk>?x \<in> A; ?y \<in> A; (?x, ?y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> ?x, \<pi> ?y) \<in> VWF

goal (1 subgoal):
 1. ordertype A r \<le> \<alpha>
[PROOF STEP]
by (metis ordertype_inc_eq ordertype_le_Ord wf_VWF)
[PROOF STATE]
proof (state)
this:
ordertype A r \<le> \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma le_ordertype_obtains_subset:
  assumes \<alpha>: "\<beta> \<le> \<alpha>" "ordertype H VWF = \<alpha>" and "small H" "Ord \<beta>"
  obtains G where "G \<subseteq> H" "ordertype G VWF = \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>G. \<lbrakk>G \<subseteq> H; ordertype G VWF = \<beta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (intro exI conjI that)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>G. \<lbrakk>G \<subseteq> H; ordertype G VWF = \<beta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?G2 \<subseteq> H
 2. (\<And>G. \<lbrakk>G \<subseteq> H; ordertype G VWF = \<beta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ordertype ?G2 VWF = \<beta>
[PROOF STEP]
let ?f = "ordermap H VWF"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>G. \<lbrakk>G \<subseteq> H; ordertype G VWF = \<beta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?G2 \<subseteq> H
 2. (\<And>G. \<lbrakk>G \<subseteq> H; ordertype G VWF = \<beta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ordertype ?G2 VWF = \<beta>
[PROOF STEP]
show \<ddagger>: "inv_into H ?f ` elts \<beta> \<subseteq> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_into H (ordermap H VWF) ` elts \<beta> \<subseteq> H
[PROOF STEP]
unfolding image_subset_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>elts \<beta>. inv_into H (ordermap H VWF) x \<in> H
[PROOF STEP]
by (metis \<alpha> inv_into_into ordermap_surj subsetD vsubsetD)
[PROOF STATE]
proof (state)
this:
inv_into H (ordermap H VWF) ` elts \<beta> \<subseteq> H

goal (1 subgoal):
 1. (\<And>G. \<lbrakk>G \<subseteq> H; ordertype G VWF = \<beta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ordertype (inv_into H (ordermap H VWF) ` elts \<beta>) VWF = \<beta>
[PROOF STEP]
have "\<exists>f. bij_betw f (inv_into H ?f ` elts \<beta>) (elts \<beta>) \<and> (\<forall>x\<in>inv_into H ?f ` elts \<beta>. \<forall>y\<in>inv_into H ?f ` elts \<beta>. (f x < f y) = ((x, y) \<in> VWF))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. bij_betw f (inv_into H (ordermap H VWF) ` elts \<beta>) (elts \<beta>) \<and> (\<forall>x\<in>inv_into H (ordermap H VWF) ` elts \<beta>. \<forall>y\<in>inv_into H (ordermap H VWF) ` elts \<beta>. (f x < f y) = ((x, y) \<in> VWF))
[PROOF STEP]
proof (intro exI conjI ballI iffI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. bij_betw ?f (inv_into H (ordermap H VWF) ` elts \<beta>) (elts \<beta>)
 2. \<And>x y. \<lbrakk>x \<in> inv_into H (ordermap H VWF) ` elts \<beta>; y \<in> inv_into H (ordermap H VWF) ` elts \<beta>; ?f x < ?f y\<rbrakk> \<Longrightarrow> (x, y) \<in> VWF
 3. \<And>x y. \<lbrakk>x \<in> inv_into H (ordermap H VWF) ` elts \<beta>; y \<in> inv_into H (ordermap H VWF) ` elts \<beta>; (x, y) \<in> VWF\<rbrakk> \<Longrightarrow> ?f x < ?f y
[PROOF STEP]
show "bij_betw ?f (inv_into H ?f ` elts \<beta>) (elts \<beta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (ordermap H VWF) (inv_into H (ordermap H VWF) ` elts \<beta>) (elts \<beta>)
[PROOF STEP]
using ordermap_bij [OF wf_VWF total_on_VWF \<open>small H\<close>] \<alpha>
[PROOF STATE]
proof (prove)
using this:
bij_betw (ordermap H VWF) H (elts (ordertype H VWF))
\<beta> \<le> \<alpha>
ordertype H VWF = \<alpha>

goal (1 subgoal):
 1. bij_betw (ordermap H VWF) (inv_into H (ordermap H VWF) ` elts \<beta>) (elts \<beta>)
[PROOF STEP]
by (metis bij_betw_inv_into_RIGHT bij_betw_subset less_eq_V_def \<ddagger>)
[PROOF STATE]
proof (state)
this:
bij_betw (ordermap H VWF) (inv_into H (ordermap H VWF) ` elts \<beta>) (elts \<beta>)

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> inv_into H (ordermap H VWF) ` elts \<beta>; y \<in> inv_into H (ordermap H VWF) ` elts \<beta>; ordermap H VWF x < ordermap H VWF y\<rbrakk> \<Longrightarrow> (x, y) \<in> VWF
 2. \<And>x y. \<lbrakk>x \<in> inv_into H (ordermap H VWF) ` elts \<beta>; y \<in> inv_into H (ordermap H VWF) ` elts \<beta>; (x, y) \<in> VWF\<rbrakk> \<Longrightarrow> ordermap H VWF x < ordermap H VWF y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> inv_into H (ordermap H VWF) ` elts \<beta>; y \<in> inv_into H (ordermap H VWF) ` elts \<beta>; ordermap H VWF x < ordermap H VWF y\<rbrakk> \<Longrightarrow> (x, y) \<in> VWF
 2. \<And>x y. \<lbrakk>x \<in> inv_into H (ordermap H VWF) ` elts \<beta>; y \<in> inv_into H (ordermap H VWF) ` elts \<beta>; (x, y) \<in> VWF\<rbrakk> \<Longrightarrow> ordermap H VWF x < ordermap H VWF y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> inv_into H (ordermap H VWF) ` elts \<beta>; y \<in> inv_into H (ordermap H VWF) ` elts \<beta>; ordermap H VWF x < ordermap H VWF y\<rbrakk> \<Longrightarrow> (x, y) \<in> VWF
 2. \<And>x y. \<lbrakk>x \<in> inv_into H (ordermap H VWF) ` elts \<beta>; y \<in> inv_into H (ordermap H VWF) ` elts \<beta>; (x, y) \<in> VWF\<rbrakk> \<Longrightarrow> ordermap H VWF x < ordermap H VWF y
[PROOF STEP]
assume x: "x \<in> inv_into H ?f ` elts \<beta>"
        and y: "y \<in> inv_into H ?f ` elts \<beta>"
[PROOF STATE]
proof (state)
this:
x \<in> inv_into H (ordermap H VWF) ` elts \<beta>
y \<in> inv_into H (ordermap H VWF) ` elts \<beta>

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> inv_into H (ordermap H VWF) ` elts \<beta>; y \<in> inv_into H (ordermap H VWF) ` elts \<beta>; ordermap H VWF x < ordermap H VWF y\<rbrakk> \<Longrightarrow> (x, y) \<in> VWF
 2. \<And>x y. \<lbrakk>x \<in> inv_into H (ordermap H VWF) ` elts \<beta>; y \<in> inv_into H (ordermap H VWF) ` elts \<beta>; (x, y) \<in> VWF\<rbrakk> \<Longrightarrow> ordermap H VWF x < ordermap H VWF y
[PROOF STEP]
show "?f x < ?f y" if "(x,y) \<in> VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap H VWF x < ordermap H VWF y
[PROOF STEP]
using that \<ddagger> \<open>small H\<close> in_mono ordermap_mono_less x y
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> VWF
inv_into H (ordermap H VWF) ` elts \<beta> \<subseteq> H
small H
?A \<subseteq> ?B \<Longrightarrow> ?x \<in> ?A \<longrightarrow> ?x \<in> ?B
\<lbrakk>(?w, ?x) \<in> ?r; wf ?r; trans ?r; ?w \<in> ?A; ?x \<in> ?A; small ?A\<rbrakk> \<Longrightarrow> ordermap ?A ?r ?w < ordermap ?A ?r ?x
x \<in> inv_into H (ordermap H VWF) ` elts \<beta>
y \<in> inv_into H (ordermap H VWF) ` elts \<beta>

goal (1 subgoal):
 1. ordermap H VWF x < ordermap H VWF y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(x, y) \<in> VWF \<Longrightarrow> ordermap H VWF x < ordermap H VWF y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> inv_into H (ordermap H VWF) ` elts \<beta>; y \<in> inv_into H (ordermap H VWF) ` elts \<beta>; ordermap H VWF x < ordermap H VWF y\<rbrakk> \<Longrightarrow> (x, y) \<in> VWF
[PROOF STEP]
show "(x,y) \<in> VWF" if "?f x < ?f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> VWF
[PROOF STEP]
using that \<ddagger> \<open>small H\<close> in_mono ordermap_mono_less [OF _ wf_VWF trans_VWF] x y
[PROOF STATE]
proof (prove)
using this:
ordermap H VWF x < ordermap H VWF y
inv_into H (ordermap H VWF) ` elts \<beta> \<subseteq> H
small H
?A \<subseteq> ?B \<Longrightarrow> ?x \<in> ?A \<longrightarrow> ?x \<in> ?B
\<lbrakk>(?w, ?x) \<in> VWF; ?w \<in> ?A; ?x \<in> ?A; small ?A\<rbrakk> \<Longrightarrow> ordermap ?A VWF ?w < ordermap ?A VWF ?x
x \<in> inv_into H (ordermap H VWF) ` elts \<beta>
y \<in> inv_into H (ordermap H VWF) ` elts \<beta>

goal (1 subgoal):
 1. (x, y) \<in> VWF
[PROOF STEP]
by (metis UNIV_I less_imp_not_less total_VWF total_on_def)
[PROOF STATE]
proof (state)
this:
ordermap H VWF x < ordermap H VWF y \<Longrightarrow> (x, y) \<in> VWF

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>f. bij_betw f (inv_into H (ordermap H VWF) ` elts \<beta>) (elts \<beta>) \<and> (\<forall>x\<in>inv_into H (ordermap H VWF) ` elts \<beta>. \<forall>y\<in>inv_into H (ordermap H VWF) ` elts \<beta>. (f x < f y) = ((x, y) \<in> VWF))

goal (1 subgoal):
 1. (\<And>G. \<lbrakk>G \<subseteq> H; ordertype G VWF = \<beta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ordertype (inv_into H (ordermap H VWF) ` elts \<beta>) VWF = \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. bij_betw f (inv_into H (ordermap H VWF) ` elts \<beta>) (elts \<beta>) \<and> (\<forall>x\<in>inv_into H (ordermap H VWF) ` elts \<beta>. \<forall>y\<in>inv_into H (ordermap H VWF) ` elts \<beta>. (f x < f y) = ((x, y) \<in> VWF))
[PROOF STEP]
show "ordertype (inv_into H ?f ` elts \<beta>) VWF = \<beta>"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. bij_betw f (inv_into H (ordermap H VWF) ` elts \<beta>) (elts \<beta>) \<and> (\<forall>x\<in>inv_into H (ordermap H VWF) ` elts \<beta>. \<forall>y\<in>inv_into H (ordermap H VWF) ` elts \<beta>. (f x < f y) = ((x, y) \<in> VWF))

goal (1 subgoal):
 1. ordertype (inv_into H (ordermap H VWF) ` elts \<beta>) VWF = \<beta>
[PROOF STEP]
by (subst ordertype_eq_iff) (use assms in auto)
[PROOF STATE]
proof (state)
this:
ordertype (inv_into H (ordermap H VWF) ` elts \<beta>) VWF = \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_infinite_\<omega>:
  assumes "A \<subseteq> elts \<omega>" "infinite A"
  shows "ordertype A VWF = \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype A VWF = \<omega>
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ordertype A VWF \<le> \<omega>
 2. \<omega> \<le> ordertype A VWF
[PROOF STEP]
show "ordertype A VWF \<le> \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype A VWF \<le> \<omega>
[PROOF STEP]
by (simp add: assms ordertype_le_Ord)
[PROOF STATE]
proof (state)
this:
ordertype A VWF \<le> \<omega>

goal (1 subgoal):
 1. \<omega> \<le> ordertype A VWF
[PROOF STEP]
show "\<omega> \<le> ordertype A VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> \<le> ordertype A VWF
[PROOF STEP]
using assms down ordertype_infinite_ge_\<omega>
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> elts \<omega>
infinite A
?Y \<subseteq> elts ?x \<Longrightarrow> small ?Y
\<lbrakk>infinite ?A; small ?A\<rbrakk> \<Longrightarrow> \<omega> \<le> ordertype ?A VWF

goal (1 subgoal):
 1. \<omega> \<le> ordertype A VWF
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<omega> \<le> ordertype A VWF

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_nat_\<omega>:
  assumes "infinite N" shows "ordertype N less_than = \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype N less_than = \<omega>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype N less_than = \<omega>
[PROOF STEP]
have "small N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small N
[PROOF STEP]
by (meson inj_on_def ord_of_nat_inject small_def small_iff_range small_image_nat_V)
[PROOF STATE]
proof (state)
this:
small N

goal (1 subgoal):
 1. ordertype N less_than = \<omega>
[PROOF STEP]
have "ordertype (ord_of_nat ` N) VWF = \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (ord_of_nat ` N) VWF = \<omega>
[PROOF STEP]
by (force simp: assms finite_image_iff inj_on_def intro: ordertype_infinite_\<omega>)
[PROOF STATE]
proof (state)
this:
ordertype (ord_of_nat ` N) VWF = \<omega>

goal (1 subgoal):
 1. ordertype N less_than = \<omega>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ordertype (ord_of_nat ` N) VWF = \<omega>

goal (1 subgoal):
 1. ordertype N less_than = \<omega>
[PROOF STEP]
have "ordertype (ord_of_nat ` N) VWF = ordertype N less_than"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (ord_of_nat ` N) VWF = ordertype N less_than
[PROOF STEP]
by (auto intro: ordertype_inc_eq \<open>small N\<close>)
[PROOF STATE]
proof (state)
this:
ordertype (ord_of_nat ` N) VWF = ordertype N less_than

goal (1 subgoal):
 1. ordertype N less_than = \<omega>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ordertype (ord_of_nat ` N) VWF = \<omega>
ordertype (ord_of_nat ` N) VWF = ordertype N less_than
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ordertype (ord_of_nat ` N) VWF = \<omega>
ordertype (ord_of_nat ` N) VWF = ordertype N less_than

goal (1 subgoal):
 1. ordertype N less_than = \<omega>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ordertype N less_than = \<omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_ordertype_imp_Field_Restr:
  assumes Lim: "Limit (ordertype A r)" and r: "wf r" "total_on A r" and "small A"
  shows "Field (Restr r A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (Restr r A) = A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Field (Restr r A) = A
[PROOF STEP]
have "\<exists>y\<in>A. (x,y) \<in> r" if "x \<in> A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>A. (x, y) \<in> r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y\<in>A. (x, y) \<in> r
[PROOF STEP]
let ?oy = "succ (ordermap A r x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y\<in>A. (x, y) \<in> r
[PROOF STEP]
have \<section>: "?oy \<in> elts (ordertype A r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.succ (ordermap A r x) \<in> elts (ordertype A r)
[PROOF STEP]
by (simp add: Lim \<open>small A\<close> ordermap_in_ordertype succ_in_Limit_iff that)
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.succ (ordermap A r x) \<in> elts (ordertype A r)

goal (1 subgoal):
 1. \<exists>y\<in>A. (x, y) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ZFC_in_HOL.succ (ordermap A r x) \<in> elts (ordertype A r)
[PROOF STEP]
have A: "inv_into A (ordermap A r) ?oy \<in> A"
[PROOF STATE]
proof (prove)
using this:
ZFC_in_HOL.succ (ordermap A r x) \<in> elts (ordertype A r)

goal (1 subgoal):
 1. inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x)) \<in> A
[PROOF STEP]
by (simp add: inv_into_ordermap)
[PROOF STATE]
proof (state)
this:
inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x)) \<in> A

goal (1 subgoal):
 1. \<exists>y\<in>A. (x, y) \<in> r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x)) \<in> A

goal (1 subgoal):
 1. \<exists>y\<in>A. (x, y) \<in> r
[PROOF STEP]
have "(x, inv_into A (ordermap A r) ?oy) \<in> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))) \<in> r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))) \<in> r
[PROOF STEP]
have "ordermap A r x \<in> elts (ordermap A r (inv_into A (ordermap A r) ?oy))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap A r x \<in> elts (ordermap A r (inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))))
[PROOF STEP]
by (metis "\<section>" elts_succ f_inv_into_f insert_iff ordermap_surj subsetD)
[PROOF STATE]
proof (state)
this:
ordermap A r x \<in> elts (ordermap A r (inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))))

goal (1 subgoal):
 1. (x, inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ordermap A r x \<in> elts (ordermap A r (inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ordermap A r x \<in> elts (ordermap A r (inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))))

goal (1 subgoal):
 1. (x, inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))) \<in> r
[PROOF STEP]
by (metis \<open>small A\<close> A converse_ordermap_mono r that)
[PROOF STATE]
proof (state)
this:
(x, inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))) \<in> r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x, inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))) \<in> r

goal (1 subgoal):
 1. \<exists>y\<in>A. (x, y) \<in> r
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x)) \<in> A
(x, inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))) \<in> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x)) \<in> A
(x, inv_into A (ordermap A r) (ZFC_in_HOL.succ (ordermap A r x))) \<in> r

goal (1 subgoal):
 1. \<exists>y\<in>A. (x, y) \<in> r
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>A. (x, y) \<in> r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> \<exists>y\<in>A. (?x, y) \<in> r

goal (1 subgoal):
 1. Field (Restr r A) = A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> A \<Longrightarrow> \<exists>y\<in>A. (?x, y) \<in> r
[PROOF STEP]
have "A \<subseteq> Field (Restr r A)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> \<exists>y\<in>A. (?x, y) \<in> r

goal (1 subgoal):
 1. A \<subseteq> Field (Restr r A)
[PROOF STEP]
by (auto simp: Field_def)
[PROOF STATE]
proof (state)
this:
A \<subseteq> Field (Restr r A)

goal (1 subgoal):
 1. Field (Restr r A) = A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<subseteq> Field (Restr r A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> Field (Restr r A)

goal (1 subgoal):
 1. Field (Restr r A) = A
[PROOF STEP]
by (simp add: Field_Restr_subset subset_antisym)
[PROOF STATE]
proof (state)
this:
Field (Restr r A) = A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_Field_Restr:
  assumes "wf r" "total_on A r" "trans r" "small A" "Field (Restr r A) = A"
  shows "ordertype (Field (Restr r A)) (Restr r A) = ordertype A r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (Field (Restr r A)) (Restr r A) = ordertype A r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf r
total_on A r
trans r
small A
Field (Restr r A) = A

goal (1 subgoal):
 1. ordertype (Field (Restr r A)) (Restr r A) = ordertype A r
[PROOF STEP]
by (force simp: ordertype_eq_ordertype wf_Restr total_on_def trans_Restr)


[STATEMENT]
lemma ordermap_insert:
  assumes "Ord \<alpha>" and y: "Ord y" "y \<le> \<alpha>" and U: "U \<subseteq> elts \<alpha>"
  shows "ordermap (insert \<alpha> U) VWF y = ordermap U VWF y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap (insert \<alpha> U) VWF y = ordermap U VWF y
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
Ord y
y \<le> \<alpha>

goal (1 subgoal):
 1. ordermap (insert \<alpha> U) VWF y = ordermap U VWF y
[PROOF STEP]
proof (induction rule: Ord_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ord x; \<And>y. \<lbrakk>y \<in> elts x; y \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF y = ordermap U VWF y; x \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF x = ordermap U VWF x
[PROOF STEP]
case (step y)
[PROOF STATE]
proof (state)
this:
Ord y
\<lbrakk>?y \<in> elts y; ?y \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF ?y = ordermap U VWF ?y
y \<le> \<alpha>

goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ord x; \<And>y. \<lbrakk>y \<in> elts x; y \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF y = ordermap U VWF y; x \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF x = ordermap U VWF x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ord y
\<lbrakk>?y \<in> elts y; ?y \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF ?y = ordermap U VWF ?y
y \<le> \<alpha>
[PROOF STEP]
have 1: "{u \<in> U. (u, y) \<in> VWF} = elts y \<inter> U"
[PROOF STATE]
proof (prove)
using this:
Ord y
\<lbrakk>?y \<in> elts y; ?y \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF ?y = ordermap U VWF ?y
y \<le> \<alpha>

goal (1 subgoal):
 1. {u \<in> U. (u, y) \<in> VWF} = elts y \<inter> U
[PROOF STEP]
apply (simp add: set_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord y; \<And>y. \<lbrakk>y \<in> elts y; y \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF y = ordermap U VWF y; y \<le> \<alpha>\<rbrakk> \<Longrightarrow> \<forall>x. (x \<in> U \<and> (x, y) \<in> VWF) = (x \<in> elts y \<and> x \<in> U)
[PROOF STEP]
by (meson Ord_in_Ord Ord_mem_iff_lt VWF_iff_Ord_less assms subsetD)
[PROOF STATE]
proof (state)
this:
{u \<in> U. (u, y) \<in> VWF} = elts y \<inter> U

goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ord x; \<And>y. \<lbrakk>y \<in> elts x; y \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF y = ordermap U VWF y; x \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF x = ordermap U VWF x
[PROOF STEP]
have 2: "{u \<in> insert \<alpha> U. (u, y) \<in> VWF} = elts y \<inter> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {u \<in> insert \<alpha> U. (u, y) \<in> VWF} = elts y \<inter> U
[PROOF STEP]
apply (simp add: set_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. ((x = \<alpha> \<or> x \<in> U) \<and> (x, y) \<in> VWF) = (x \<in> elts y \<and> x \<in> U)
[PROOF STEP]
by (meson Ord_in_Ord Ord_mem_iff_lt VWF_iff_Ord_less assms leD step.hyps step.prems subsetD)
[PROOF STATE]
proof (state)
this:
{u \<in> insert \<alpha> U. (u, y) \<in> VWF} = elts y \<inter> U

goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ord x; \<And>y. \<lbrakk>y \<in> elts x; y \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF y = ordermap U VWF y; x \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF x = ordermap U VWF x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap (insert \<alpha> U) VWF y = ordermap U VWF y
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
Ord y
\<lbrakk>?y \<in> elts y; ?y \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF ?y = ordermap U VWF ?y
y \<le> \<alpha>

goal (1 subgoal):
 1. ordermap (insert \<alpha> U) VWF y = ordermap U VWF y
[PROOF STEP]
apply (simp only: ordermap [OF wf_VWF, of _ y] 1 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord y; \<And>y. \<lbrakk>y \<in> elts y; y \<le> \<alpha>\<rbrakk> \<Longrightarrow> ordermap (insert \<alpha> U) VWF y = ordermap U VWF y; y \<le> \<alpha>\<rbrakk> \<Longrightarrow> set (ordermap (insert \<alpha> U) VWF ` (elts y \<inter> U)) = set (ordermap U VWF ` (elts y \<inter> U))
[PROOF STEP]
by (meson Int_lower1 Ord_is_Transset Sup.SUP_cong Transset_def assms(1) in_mono vsubsetD)
[PROOF STATE]
proof (state)
this:
ordermap (insert \<alpha> U) VWF y = ordermap U VWF y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_insert:
  assumes "Ord \<alpha>" and U: "U \<subseteq> elts \<alpha>"
  shows "ordertype (insert \<alpha> U) VWF = succ (ordertype U VWF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
have \<dagger>: "{y \<in> insert \<alpha> U. (y, \<alpha>) \<in> VWF} = U" "{y \<in> U. (y, \<alpha>) \<in> VWF} = U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y \<in> insert \<alpha> U. (y, \<alpha>) \<in> VWF} = U &&& {y \<in> U. (y, \<alpha>) \<in> VWF} = U
[PROOF STEP]
using Ord_in_Ord OrdmemD assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Ord ?k; ?m \<in> elts ?k\<rbrakk> \<Longrightarrow> Ord ?m
\<lbrakk>Ord ?k; ?j \<in> elts ?k\<rbrakk> \<Longrightarrow> ?j < ?k
Ord \<alpha>
U \<subseteq> elts \<alpha>

goal (1 subgoal):
 1. {y \<in> insert \<alpha> U. (y, \<alpha>) \<in> VWF} = U &&& {y \<in> U. (y, \<alpha>) \<in> VWF} = U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{y \<in> insert \<alpha> U. (y, \<alpha>) \<in> VWF} = U
{y \<in> U. (y, \<alpha>) \<in> VWF} = U

goal (1 subgoal):
 1. ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
have eq: "\<And>x. x \<in> U \<Longrightarrow> ordermap (insert \<alpha> U) VWF x = ordermap U VWF x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> ordermap (insert \<alpha> U) VWF x = ordermap U VWF x
[PROOF STEP]
by (meson Ord_in_Ord Ord_is_Transset Transset_def U assms(1) in_mono ordermap_insert)
[PROOF STATE]
proof (state)
this:
?x \<in> U \<Longrightarrow> ordermap (insert \<alpha> U) VWF ?x = ordermap U VWF ?x

goal (1 subgoal):
 1. ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
have "ordertype (insert \<alpha> U) VWF =
        ZFC_in_HOL.set (insert (ordermap U VWF \<alpha>) (ordermap U VWF ` U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (insert \<alpha> U) VWF = set (insert (ordermap U VWF \<alpha>) (ordermap U VWF ` U))
[PROOF STEP]
by (simp add: ordertype_def ordermap_insert assms eq)
[PROOF STATE]
proof (state)
this:
ordertype (insert \<alpha> U) VWF = set (insert (ordermap U VWF \<alpha>) (ordermap U VWF ` U))

goal (1 subgoal):
 1. ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ordertype (insert \<alpha> U) VWF = set (insert (ordermap U VWF \<alpha>) (ordermap U VWF ` U))

goal (1 subgoal):
 1. ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
have "\<dots> = succ (ZFC_in_HOL.set (ordermap U VWF ` U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (insert (ordermap U VWF \<alpha>) (ordermap U VWF ` U)) = ZFC_in_HOL.succ (set (ordermap U VWF ` U))
[PROOF STEP]
using "\<dagger>" U
[PROOF STATE]
proof (prove)
using this:
{y \<in> insert \<alpha> U. (y, \<alpha>) \<in> VWF} = U
{y \<in> U. (y, \<alpha>) \<in> VWF} = U
U \<subseteq> elts \<alpha>

goal (1 subgoal):
 1. set (insert (ordermap U VWF \<alpha>) (ordermap U VWF ` U)) = ZFC_in_HOL.succ (set (ordermap U VWF ` U))
[PROOF STEP]
by (simp add: ordermap [OF wf_VWF, of _ \<alpha>] down succ_def vinsert_def)
[PROOF STATE]
proof (state)
this:
set (insert (ordermap U VWF \<alpha>) (ordermap U VWF ` U)) = ZFC_in_HOL.succ (set (ordermap U VWF ` U))

goal (1 subgoal):
 1. ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (insert (ordermap U VWF \<alpha>) (ordermap U VWF ` U)) = ZFC_in_HOL.succ (set (ordermap U VWF ` U))

goal (1 subgoal):
 1. ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
have "\<dots> = succ (ordertype U VWF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.succ (set (ordermap U VWF ` U)) = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
by (simp add: ordertype_def)
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.succ (set (ordermap U VWF ` U)) = ZFC_in_HOL.succ (ordertype U VWF)

goal (1 subgoal):
 1. ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)

goal (1 subgoal):
 1. ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ordertype (insert \<alpha> U) VWF = ZFC_in_HOL.succ (ordertype U VWF)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_ordertype_le_card:
  assumes "finite A" "wf r" "trans r"
  shows "ordertype A r \<le> ord_of_nat (card A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype A r \<le> ord_of_nat (card A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype A r \<le> ord_of_nat (card A)
[PROOF STEP]
have "Ord (ordertype A r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord (ordertype A r)
[PROOF STEP]
by (simp add: wf_Ord_ordertype assms)
[PROOF STATE]
proof (state)
this:
Ord (ordertype A r)

goal (1 subgoal):
 1. ordertype A r \<le> ord_of_nat (card A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Ord (ordertype A r)

goal (1 subgoal):
 1. ordertype A r \<le> ord_of_nat (card A)
[PROOF STEP]
have "ordermap A r ` A = elts (ordertype A r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordermap A r ` A = elts (ordertype A r)
[PROOF STEP]
by (simp add: ordertype_def finite_imp_small \<open>finite A\<close>)
[PROOF STATE]
proof (state)
this:
ordermap A r ` A = elts (ordertype A r)

goal (1 subgoal):
 1. ordertype A r \<le> ord_of_nat (card A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ordermap A r ` A = elts (ordertype A r)

goal (1 subgoal):
 1. ordertype A r \<le> ord_of_nat (card A)
[PROOF STEP]
have "card (ordermap A r ` A) \<le> card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (ordermap A r ` A) \<le> card A
[PROOF STEP]
using \<open>finite A\<close> card_image_le
[PROOF STATE]
proof (prove)
using this:
finite A
finite ?A \<Longrightarrow> card (?f ` ?A) \<le> card ?A

goal (1 subgoal):
 1. card (ordermap A r ` A) \<le> card A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (ordermap A r ` A) \<le> card A

goal (1 subgoal):
 1. ordertype A r \<le> ord_of_nat (card A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Ord (ordertype A r)
ordermap A r ` A = elts (ordertype A r)
card (ordermap A r ` A) \<le> card A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Ord (ordertype A r)
ordermap A r ` A = elts (ordertype A r)
card (ordermap A r ` A) \<le> card A

goal (1 subgoal):
 1. ordertype A r \<le> ord_of_nat (card A)
[PROOF STEP]
by (metis Ord_linear_le Ord_ord_of_nat \<open>finite A\<close> card_ord_of_nat card_seteq finite_imageI less_eq_V_def)
[PROOF STATE]
proof (state)
this:
ordertype A r \<le> ord_of_nat (card A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_VWF_\<omega>:
  assumes "finite A"
  shows "ordertype A VWF \<in> elts \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype A VWF \<in> elts \<omega>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype A VWF \<in> elts \<omega>
[PROOF STEP]
have "finite (ordermap A VWF ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (ordermap A VWF ` A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. finite (ordermap A VWF ` A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (ordermap A VWF ` A)

goal (1 subgoal):
 1. ordertype A VWF \<in> elts \<omega>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (ordermap A VWF ` A)
[PROOF STEP]
have "ordertype A VWF < \<omega>"
[PROOF STATE]
proof (prove)
using this:
finite (ordermap A VWF ` A)

goal (1 subgoal):
 1. ordertype A VWF < \<omega>
[PROOF STEP]
by (meson Ord_\<omega> OrdmemD trans_VWF wf_VWF assms finite_ordertype_le_card le_less_trans ord_of_nat_\<omega>)
[PROOF STATE]
proof (state)
this:
ordertype A VWF < \<omega>

goal (1 subgoal):
 1. ordertype A VWF \<in> elts \<omega>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ordertype A VWF < \<omega>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ordertype A VWF < \<omega>

goal (1 subgoal):
 1. ordertype A VWF \<in> elts \<omega>
[PROOF STEP]
by (simp add: Ord_mem_iff_lt)
[PROOF STATE]
proof (state)
this:
ordertype A VWF \<in> elts \<omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_VWF_finite_nat:
  assumes "finite A"
  shows "ordertype A VWF = ord_of_nat (card A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype A VWF = ord_of_nat (card A)
[PROOF STEP]
by (metis finite_imp_small ordermap_bij total_on_VWF wf_VWF \<omega>_def assms bij_betw_same_card card_ord_of_nat elts_of_set f_inv_into_f inf ordertype_VWF_\<omega>)


[STATEMENT]
lemma finite_ordertype_eq_card:
  assumes "small A" "wf r" "trans r" "total_on A r"
  shows "ordertype A r = ord_of_nat m \<longleftrightarrow> finite A \<and> card A = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ordertype A r = ord_of_nat m) = (finite A \<and> card A = m)
[PROOF STEP]
using ordermap_bij [OF \<open>wf r\<close>]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>total_on ?A r; small ?A\<rbrakk> \<Longrightarrow> bij_betw (ordermap ?A r) ?A (elts (ordertype ?A r))

goal (1 subgoal):
 1. (ordertype A r = ord_of_nat m) = (finite A \<and> card A = m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>A. \<lbrakk>total_on A r; small A\<rbrakk> \<Longrightarrow> bij_betw (ordermap A r) A (elts (ordertype A r))) \<Longrightarrow> (ordertype A r = ord_of_nat m) = (finite A \<and> card A = m)
[PROOF STEP]
have *: "bij_betw (ordermap A r) A (elts (ordertype A r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (ordermap A r) A (elts (ordertype A r))
[PROOF STEP]
by (simp add: assms ordermap_bij)
[PROOF STATE]
proof (state)
this:
bij_betw (ordermap A r) A (elts (ordertype A r))

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>total_on A r; small A\<rbrakk> \<Longrightarrow> bij_betw (ordermap A r) A (elts (ordertype A r))) \<Longrightarrow> (ordertype A r = ord_of_nat m) = (finite A \<and> card A = m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bij_betw (ordermap A r) A (elts (ordertype A r))

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>total_on A r; small A\<rbrakk> \<Longrightarrow> bij_betw (ordermap A r) A (elts (ordertype A r))) \<Longrightarrow> (ordertype A r = ord_of_nat m) = (finite A \<and> card A = m)
[PROOF STEP]
have "card (ordermap A r ` A) = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (ordermap A r ` A) = card A
[PROOF STEP]
by (meson bij_betw_def * card_image)
[PROOF STATE]
proof (state)
this:
card (ordermap A r ` A) = card A

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>total_on A r; small A\<rbrakk> \<Longrightarrow> bij_betw (ordermap A r) A (elts (ordertype A r))) \<Longrightarrow> (ordertype A r = ord_of_nat m) = (finite A \<and> card A = m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bij_betw (ordermap A r) A (elts (ordertype A r))
card (ordermap A r ` A) = card A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bij_betw (ordermap A r) A (elts (ordertype A r))
card (ordermap A r ` A) = card A

goal (1 subgoal):
 1. (ordertype A r = ord_of_nat m) = (finite A \<and> card A = m)
[PROOF STEP]
using assms bij_betw_finite bij_betw_imp_surj_on finite_Ord_omega ordertype_VWF_finite_nat wf_Ord_ordertype
[PROOF STATE]
proof (prove)
using this:
bij_betw (ordermap A r) A (elts (ordertype A r))
card (ordermap A r ` A) = card A
small A
wf r
trans r
total_on A r
bij_betw ?f ?A ?B \<Longrightarrow> finite ?A = finite ?B
bij_betw ?f ?A ?B \<Longrightarrow> ?f ` ?A = ?B
?\<alpha> \<in> elts \<omega> \<Longrightarrow> finite (elts ?\<alpha>)
finite ?A \<Longrightarrow> ordertype ?A VWF = ord_of_nat (card ?A)
\<lbrakk>wf ?r; trans ?r\<rbrakk> \<Longrightarrow> Ord (ordertype ?A ?r)

goal (1 subgoal):
 1. (ordertype A r = ord_of_nat m) = (finite A \<and> card A = m)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(ordertype A r = ord_of_nat m) = (finite A \<and> card A = m)

goal:
No subgoals!
[PROOF STEP]
qed