[STATEMENT]
lemma sorted_wrt_list_set:
  assumes "linorder_on A R" "set xs \<subseteq> A"
  shows   "sorted_wrt_list_of_set R (set xs) = insort_wrt R (remdups xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt_list_of_set R (set xs) = insort_wrt R (remdups xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sorted_wrt_list_of_set R (set xs) = insort_wrt R (remdups xs)
[PROOF STEP]
have "sorted_wrt_list_of_set R (set xs) =
          (THE xsa. set xsa = set xs \<and> distinct xsa \<and> sorted_wrt R xsa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt_list_of_set R (set xs) = (THE xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa)
[PROOF STEP]
by (simp add: sorted_wrt_list_of_set_def)
[PROOF STATE]
proof (state)
this:
sorted_wrt_list_of_set R (set xs) = (THE xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa)

goal (1 subgoal):
 1. sorted_wrt_list_of_set R (set xs) = insort_wrt R (remdups xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sorted_wrt_list_of_set R (set xs) = (THE xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa)

goal (1 subgoal):
 1. sorted_wrt_list_of_set R (set xs) = insort_wrt R (remdups xs)
[PROOF STEP]
have "\<dots> = insort_wrt R (remdups xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa) = insort_wrt R (remdups xs)
[PROOF STEP]
proof (rule the_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set (insort_wrt R (remdups xs)) = set xs \<and> distinct (insort_wrt R (remdups xs)) \<and> Linorder_Relations.sorted_wrt R (insort_wrt R (remdups xs))
 2. \<And>xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa \<Longrightarrow> xsa = insort_wrt R (remdups xs)
[PROOF STEP]
fix xsa
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set (insort_wrt R (remdups xs)) = set xs \<and> distinct (insort_wrt R (remdups xs)) \<and> Linorder_Relations.sorted_wrt R (insort_wrt R (remdups xs))
 2. \<And>xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa \<Longrightarrow> xsa = insort_wrt R (remdups xs)
[PROOF STEP]
assume xsa: "set xsa = set xs \<and> distinct xsa \<and> sorted_wrt R xsa"
[PROOF STATE]
proof (state)
this:
set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa

goal (2 subgoals):
 1. set (insort_wrt R (remdups xs)) = set xs \<and> distinct (insort_wrt R (remdups xs)) \<and> Linorder_Relations.sorted_wrt R (insort_wrt R (remdups xs))
 2. \<And>xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa \<Longrightarrow> xsa = insort_wrt R (remdups xs)
[PROOF STEP]
from xsa
[PROOF STATE]
proof (chain)
picking this:
set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa
[PROOF STEP]
have "mset xsa = mset_set (set xsa)"
[PROOF STATE]
proof (prove)
using this:
set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa

goal (1 subgoal):
 1. mset xsa = mset_set (set xsa)
[PROOF STEP]
by (subst mset_set_set) simp_all
[PROOF STATE]
proof (state)
this:
mset xsa = mset_set (set xsa)

goal (2 subgoals):
 1. set (insort_wrt R (remdups xs)) = set xs \<and> distinct (insort_wrt R (remdups xs)) \<and> Linorder_Relations.sorted_wrt R (insort_wrt R (remdups xs))
 2. \<And>xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa \<Longrightarrow> xsa = insort_wrt R (remdups xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mset xsa = mset_set (set xsa)

goal (2 subgoals):
 1. set (insort_wrt R (remdups xs)) = set xs \<and> distinct (insort_wrt R (remdups xs)) \<and> Linorder_Relations.sorted_wrt R (insort_wrt R (remdups xs))
 2. \<And>xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa \<Longrightarrow> xsa = insort_wrt R (remdups xs)
[PROOF STEP]
from xsa
[PROOF STATE]
proof (chain)
picking this:
set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa
[PROOF STEP]
have "set xsa = set xs"
[PROOF STATE]
proof (prove)
using this:
set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa

goal (1 subgoal):
 1. set xsa = set xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set xsa = set xs

goal (2 subgoals):
 1. set (insort_wrt R (remdups xs)) = set xs \<and> distinct (insort_wrt R (remdups xs)) \<and> Linorder_Relations.sorted_wrt R (insort_wrt R (remdups xs))
 2. \<And>xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa \<Longrightarrow> xsa = insort_wrt R (remdups xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set xsa = set xs

goal (2 subgoals):
 1. set (insort_wrt R (remdups xs)) = set xs \<and> distinct (insort_wrt R (remdups xs)) \<and> Linorder_Relations.sorted_wrt R (insort_wrt R (remdups xs))
 2. \<And>xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa \<Longrightarrow> xsa = insort_wrt R (remdups xs)
[PROOF STEP]
have "mset_set \<dots> = mset (remdups xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_set (set xs) = mset (remdups xs)
[PROOF STEP]
by (simp add: mset_remdups)
[PROOF STATE]
proof (state)
this:
mset_set (set xs) = mset (remdups xs)

goal (2 subgoals):
 1. set (insort_wrt R (remdups xs)) = set xs \<and> distinct (insort_wrt R (remdups xs)) \<and> Linorder_Relations.sorted_wrt R (insort_wrt R (remdups xs))
 2. \<And>xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa \<Longrightarrow> xsa = insort_wrt R (remdups xs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mset xsa = mset (remdups xs)
[PROOF STEP]
show "xsa = insort_wrt R (remdups xs)"
[PROOF STATE]
proof (prove)
using this:
mset xsa = mset (remdups xs)

goal (1 subgoal):
 1. xsa = insort_wrt R (remdups xs)
[PROOF STEP]
using xsa assms
[PROOF STATE]
proof (prove)
using this:
mset xsa = mset (remdups xs)
set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa
linorder_on A R
set xs \<subseteq> A

goal (1 subgoal):
 1. xsa = insort_wrt R (remdups xs)
[PROOF STEP]
by (intro sorted_wrt_linorder_unique[OF assms(1)])
         (auto intro!: sorted_wrt_insort)
[PROOF STATE]
proof (state)
this:
xsa = insort_wrt R (remdups xs)

goal (1 subgoal):
 1. set (insort_wrt R (remdups xs)) = set xs \<and> distinct (insort_wrt R (remdups xs)) \<and> Linorder_Relations.sorted_wrt R (insort_wrt R (remdups xs))
[PROOF STEP]
qed (insert assms, auto intro!: sorted_wrt_insort)
[PROOF STATE]
proof (state)
this:
(THE xsa. set xsa = set xs \<and> distinct xsa \<and> Linorder_Relations.sorted_wrt R xsa) = insort_wrt R (remdups xs)

goal (1 subgoal):
 1. sorted_wrt_list_of_set R (set xs) = insort_wrt R (remdups xs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sorted_wrt_list_of_set R (set xs) = insort_wrt R (remdups xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sorted_wrt_list_of_set R (set xs) = insort_wrt R (remdups xs)

goal (1 subgoal):
 1. sorted_wrt_list_of_set R (set xs) = insort_wrt R (remdups xs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sorted_wrt_list_of_set R (set xs) = insort_wrt R (remdups xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linorder_sorted_wrt_exists:
  assumes "linorder_on A R" "finite B" "B \<subseteq> A"
  shows   "\<exists>xs. set xs = B \<and> distinct xs \<and> sorted_wrt R xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
from \<open>finite B\<close>
[PROOF STATE]
proof (chain)
picking this:
finite B
[PROOF STEP]
obtain xs where "set xs = B" "distinct xs"
[PROOF STATE]
proof (prove)
using this:
finite B

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>set xs = B; distinct xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_distinct_list
[PROOF STATE]
proof (prove)
using this:
finite B
finite ?A \<Longrightarrow> \<exists>xs. set xs = ?A \<and> distinct xs

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>set xs = B; distinct xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set xs = B
distinct xs

goal (1 subgoal):
 1. \<exists>xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
hence "set (insort_wrt R xs) = B" "distinct (insort_wrt R xs)"
[PROOF STATE]
proof (prove)
using this:
set xs = B
distinct xs

goal (1 subgoal):
 1. set (insort_wrt R xs) = B &&& distinct (insort_wrt R xs)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
set (insort_wrt R xs) = B
distinct (insort_wrt R xs)

goal (1 subgoal):
 1. \<exists>xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (insort_wrt R xs) = B
distinct (insort_wrt R xs)

goal (1 subgoal):
 1. \<exists>xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
have "sorted_wrt R (insort_wrt R xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (insort_wrt R xs)
[PROOF STEP]
using assms \<open>set xs = B\<close>
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
finite B
B \<subseteq> A
set xs = B

goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (insort_wrt R xs)
[PROOF STEP]
by (intro sorted_wrt_insort[OF assms(1)]) auto
[PROOF STATE]
proof (state)
this:
Linorder_Relations.sorted_wrt R (insort_wrt R xs)

goal (1 subgoal):
 1. \<exists>xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (insort_wrt R xs) = B
distinct (insort_wrt R xs)
Linorder_Relations.sorted_wrt R (insort_wrt R xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (insort_wrt R xs) = B
distinct (insort_wrt R xs)
Linorder_Relations.sorted_wrt R (insort_wrt R xs)

goal (1 subgoal):
 1. \<exists>xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linorder_sorted_wrt_list_of_set:
  assumes "linorder_on A R" "finite B" "B \<subseteq> A"
  shows   "set (sorted_wrt_list_of_set R B) = B" "distinct (sorted_wrt_list_of_set R B)"
          "sorted_wrt R (sorted_wrt_list_of_set R B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (sorted_wrt_list_of_set R B) = B &&& distinct (sorted_wrt_list_of_set R B) &&& Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. set (sorted_wrt_list_of_set R B) = B
 2. distinct (sorted_wrt_list_of_set R B)
 3. Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R B)
[PROOF STEP]
have "\<exists>!xs. set xs = B \<and> distinct xs \<and> sorted_wrt R xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
proof (rule ex_ex1I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
 2. \<And>xs y. \<lbrakk>set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs; set y = B \<and> distinct y \<and> Linorder_Relations.sorted_wrt R y\<rbrakk> \<Longrightarrow> xs = y
[PROOF STEP]
show "\<exists>xs. set xs = B \<and> distinct xs \<and> sorted_wrt R xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
by (rule linorder_sorted_wrt_exists assms)+
[PROOF STATE]
proof (state)
this:
\<exists>xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs

goal (1 subgoal):
 1. \<And>xs y. \<lbrakk>set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs; set y = B \<and> distinct y \<and> Linorder_Relations.sorted_wrt R y\<rbrakk> \<Longrightarrow> xs = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs y. \<lbrakk>set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs; set y = B \<and> distinct y \<and> Linorder_Relations.sorted_wrt R y\<rbrakk> \<Longrightarrow> xs = y
[PROOF STEP]
fix xs ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs y. \<lbrakk>set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs; set y = B \<and> distinct y \<and> Linorder_Relations.sorted_wrt R y\<rbrakk> \<Longrightarrow> xs = y
[PROOF STEP]
assume "set xs = B \<and> distinct xs \<and> sorted_wrt R xs"
                     "set ys = B \<and> distinct ys \<and> sorted_wrt R ys"
[PROOF STATE]
proof (state)
this:
set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
set ys = B \<and> distinct ys \<and> Linorder_Relations.sorted_wrt R ys

goal (1 subgoal):
 1. \<And>xs y. \<lbrakk>set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs; set y = B \<and> distinct y \<and> Linorder_Relations.sorted_wrt R y\<rbrakk> \<Longrightarrow> xs = y
[PROOF STEP]
thus "xs = ys"
[PROOF STATE]
proof (prove)
using this:
set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs
set ys = B \<and> distinct ys \<and> Linorder_Relations.sorted_wrt R ys

goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
by (intro sorted_wrt_linorder_unique[OF assms(1)]) (auto simp: set_eq_iff_mset_eq_distinct)
[PROOF STATE]
proof (state)
this:
xs = ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!xs. set xs = B \<and> distinct xs \<and> Linorder_Relations.sorted_wrt R xs

goal (3 subgoals):
 1. set (sorted_wrt_list_of_set R B) = B
 2. distinct (sorted_wrt_list_of_set R B)
 3. Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R B)
[PROOF STEP]
from theI'[OF this]
[PROOF STATE]
proof (chain)
picking this:
set (THE x. set x = B \<and> distinct x \<and> Linorder_Relations.sorted_wrt R x) = B \<and> distinct (THE x. set x = B \<and> distinct x \<and> Linorder_Relations.sorted_wrt R x) \<and> Linorder_Relations.sorted_wrt R (THE x. set x = B \<and> distinct x \<and> Linorder_Relations.sorted_wrt R x)
[PROOF STEP]
show  "set (sorted_wrt_list_of_set R B) = B"
    "distinct (sorted_wrt_list_of_set R B)" "sorted_wrt R (sorted_wrt_list_of_set R B)"
[PROOF STATE]
proof (prove)
using this:
set (THE x. set x = B \<and> distinct x \<and> Linorder_Relations.sorted_wrt R x) = B \<and> distinct (THE x. set x = B \<and> distinct x \<and> Linorder_Relations.sorted_wrt R x) \<and> Linorder_Relations.sorted_wrt R (THE x. set x = B \<and> distinct x \<and> Linorder_Relations.sorted_wrt R x)

goal (1 subgoal):
 1. set (sorted_wrt_list_of_set R B) = B &&& distinct (sorted_wrt_list_of_set R B) &&& Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R B)
[PROOF STEP]
by (simp_all add: sorted_wrt_list_of_set_def \<open>finite B\<close>)
[PROOF STATE]
proof (state)
this:
set (sorted_wrt_list_of_set R B) = B
distinct (sorted_wrt_list_of_set R B)
Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sorted_wrt_list_of_set_eqI:
  assumes "linorder_on B R" "A \<subseteq> B" "set xs = A" "distinct xs" "sorted_wrt R xs"
  shows   "sorted_wrt_list_of_set R A = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt_list_of_set R A = xs
[PROOF STEP]
proof (rule sorted_wrt_linorder_unique)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. linorder_on ?A ?R
 2. mset (sorted_wrt_list_of_set R A) = mset xs
 3. Linorder_Relations.sorted_wrt ?R (sorted_wrt_list_of_set R A)
 4. Linorder_Relations.sorted_wrt ?R xs
[PROOF STEP]
show "linorder_on B R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_on B R
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
linorder_on B R

goal (3 subgoals):
 1. mset (sorted_wrt_list_of_set R A) = mset xs
 2. Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)
 3. Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
let ?ys = "sorted_wrt_list_of_set R A"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mset (sorted_wrt_list_of_set R A) = mset xs
 2. Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)
 3. Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
have fin [simp]: "finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A
[PROOF STEP]
by (simp_all add: assms(3) [symmetric])
[PROOF STATE]
proof (state)
this:
finite A

goal (3 subgoals):
 1. mset (sorted_wrt_list_of_set R A) = mset xs
 2. Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)
 3. Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
have *: "distinct ?ys" "set ?ys = A" "sorted_wrt R ?ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (sorted_wrt_list_of_set R A) &&& set (sorted_wrt_list_of_set R A) = A &&& Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)
[PROOF STEP]
by (rule linorder_sorted_wrt_list_of_set[OF assms(1)] fin assms)+
[PROOF STATE]
proof (state)
this:
distinct (sorted_wrt_list_of_set R A)
set (sorted_wrt_list_of_set R A) = A
Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)

goal (3 subgoals):
 1. mset (sorted_wrt_list_of_set R A) = mset xs
 2. Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)
 3. Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
from assms *
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
A \<subseteq> B
set xs = A
distinct xs
Linorder_Relations.sorted_wrt R xs
distinct (sorted_wrt_list_of_set R A)
set (sorted_wrt_list_of_set R A) = A
Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)
[PROOF STEP]
show "mset ?ys = mset xs"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
A \<subseteq> B
set xs = A
distinct xs
Linorder_Relations.sorted_wrt R xs
distinct (sorted_wrt_list_of_set R A)
set (sorted_wrt_list_of_set R A) = A
Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)

goal (1 subgoal):
 1. mset (sorted_wrt_list_of_set R A) = mset xs
[PROOF STEP]
by (subst set_eq_iff_mset_eq_distinct [symmetric]) simp_all
[PROOF STATE]
proof (state)
this:
mset (sorted_wrt_list_of_set R A) = mset xs

goal (2 subgoals):
 1. Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)
 2. Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
show "sorted_wrt R ?ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)

goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R xs
[PROOF STEP]
qed fact+


[STATEMENT]
lemma linorder_rank_le:
  assumes "finite A"
  shows   "linorder_rank R A x \<le> card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R A x \<le> card A
[PROOF STEP]
unfolding linorder_rank_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {y \<in> A - {x}. (y, x) \<in> R} \<le> card A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. card {y \<in> A - {x}. (y, x) \<in> R} \<le> card A
[PROOF STEP]
by (rule card_mono) auto


[STATEMENT]
lemma linorder_rank_less:
  assumes "finite A" "x \<in> A"
  shows   "linorder_rank R A x < card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R A x < card A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linorder_rank R A x < card A
[PROOF STEP]
have "linorder_rank R A x \<le> card (A - {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R A x \<le> card (A - {x})
[PROOF STEP]
unfolding linorder_rank_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {y \<in> A - {x}. (y, x) \<in> R} \<le> card (A - {x})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
x \<in> A

goal (1 subgoal):
 1. card {y \<in> A - {x}. (y, x) \<in> R} \<le> card (A - {x})
[PROOF STEP]
by (intro card_mono) auto
[PROOF STATE]
proof (state)
this:
linorder_rank R A x \<le> card (A - {x})

goal (1 subgoal):
 1. linorder_rank R A x < card A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
linorder_rank R A x \<le> card (A - {x})

goal (1 subgoal):
 1. linorder_rank R A x < card A
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
x \<in> A
[PROOF STEP]
have "\<dots> < card A"
[PROOF STATE]
proof (prove)
using this:
finite A
x \<in> A

goal (1 subgoal):
 1. card (A - {x}) < card A
[PROOF STEP]
by (intro psubset_card_mono) auto
[PROOF STATE]
proof (state)
this:
card (A - {x}) < card A

goal (1 subgoal):
 1. linorder_rank R A x < card A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
linorder_rank R A x < card A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
linorder_rank R A x < card A

goal (1 subgoal):
 1. linorder_rank R A x < card A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
linorder_rank R A x < card A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linorder_rank_union:
  assumes "finite A" "finite B" "A \<inter> B = {}"
  shows   "linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x
[PROOF STEP]
have "linorder_rank R (A \<union> B) x = card {y\<in>(A\<union>B)-{x}. (y,x) \<in> R}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R (A \<union> B) x = card {y \<in> A \<union> B - {x}. (y, x) \<in> R}
[PROOF STEP]
by (simp add: linorder_rank_def)
[PROOF STATE]
proof (state)
this:
linorder_rank R (A \<union> B) x = card {y \<in> A \<union> B - {x}. (y, x) \<in> R}

goal (1 subgoal):
 1. linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
linorder_rank R (A \<union> B) x = card {y \<in> A \<union> B - {x}. (y, x) \<in> R}

goal (1 subgoal):
 1. linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x
[PROOF STEP]
have "{y\<in>(A\<union>B)-{x}. (y,x) \<in> R} = {y\<in>A-{x}. (y,x) \<in> R} \<union> {y\<in>B-{x}. (y,x) \<in> R}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y \<in> A \<union> B - {x}. (y, x) \<in> R} = {y \<in> A - {x}. (y, x) \<in> R} \<union> {y \<in> B - {x}. (y, x) \<in> R}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{y \<in> A \<union> B - {x}. (y, x) \<in> R} = {y \<in> A - {x}. (y, x) \<in> R} \<union> {y \<in> B - {x}. (y, x) \<in> R}

goal (1 subgoal):
 1. linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{y \<in> A \<union> B - {x}. (y, x) \<in> R} = {y \<in> A - {x}. (y, x) \<in> R} \<union> {y \<in> B - {x}. (y, x) \<in> R}

goal (1 subgoal):
 1. linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x
[PROOF STEP]
have "card \<dots> = linorder_rank R A x + linorder_rank R B x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({y \<in> A - {x}. (y, x) \<in> R} \<union> {y \<in> B - {x}. (y, x) \<in> R}) = linorder_rank R A x + linorder_rank R B x
[PROOF STEP]
unfolding linorder_rank_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({y \<in> A - {x}. (y, x) \<in> R} \<union> {y \<in> B - {x}. (y, x) \<in> R}) = card {y \<in> A - {x}. (y, x) \<in> R} + card {y \<in> B - {x}. (y, x) \<in> R}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
finite B
A \<inter> B = {}

goal (1 subgoal):
 1. card ({y \<in> A - {x}. (y, x) \<in> R} \<union> {y \<in> B - {x}. (y, x) \<in> R}) = card {y \<in> A - {x}. (y, x) \<in> R} + card {y \<in> B - {x}. (y, x) \<in> R}
[PROOF STEP]
by (intro card_Un_disjoint) auto
[PROOF STATE]
proof (state)
this:
card ({y \<in> A - {x}. (y, x) \<in> R} \<union> {y \<in> B - {x}. (y, x) \<in> R}) = linorder_rank R A x + linorder_rank R B x

goal (1 subgoal):
 1. linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x

goal (1 subgoal):
 1. linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
linorder_rank R (A \<union> B) x = linorder_rank R A x + linorder_rank R B x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linorder_rank_empty [simp]: "linorder_rank R {} x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R {} x = 0
[PROOF STEP]
by (simp add: linorder_rank_def)


[STATEMENT]
lemma linorder_rank_singleton:
  "linorder_rank R {y} x = (if x \<noteq> y \<and> (y,x) \<in> R then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R {y} x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linorder_rank R {y} x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)
[PROOF STEP]
have "linorder_rank R {y} x = card {z\<in>{y}-{x}. (z,x) \<in> R}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R {y} x = card {z \<in> {y} - {x}. (z, x) \<in> R}
[PROOF STEP]
by (simp add: linorder_rank_def)
[PROOF STATE]
proof (state)
this:
linorder_rank R {y} x = card {z \<in> {y} - {x}. (z, x) \<in> R}

goal (1 subgoal):
 1. linorder_rank R {y} x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
linorder_rank R {y} x = card {z \<in> {y} - {x}. (z, x) \<in> R}

goal (1 subgoal):
 1. linorder_rank R {y} x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)
[PROOF STEP]
have "{z\<in>{y}-{x}. (z,x) \<in> R} = (if x \<noteq> y \<and> (y,x) \<in> R then {y} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {z \<in> {y} - {x}. (z, x) \<in> R} = (if x \<noteq> y \<and> (y, x) \<in> R then {y} else {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{z \<in> {y} - {x}. (z, x) \<in> R} = (if x \<noteq> y \<and> (y, x) \<in> R then {y} else {})

goal (1 subgoal):
 1. linorder_rank R {y} x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{z \<in> {y} - {x}. (z, x) \<in> R} = (if x \<noteq> y \<and> (y, x) \<in> R then {y} else {})

goal (1 subgoal):
 1. linorder_rank R {y} x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)
[PROOF STEP]
have "card \<dots> = (if x \<noteq> y \<and> (y,x) \<in> R then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (if x \<noteq> y \<and> (y, x) \<in> R then {y} else {}) = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (if x \<noteq> y \<and> (y, x) \<in> R then {y} else {}) = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)

goal (1 subgoal):
 1. linorder_rank R {y} x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
linorder_rank R {y} x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
linorder_rank R {y} x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)

goal (1 subgoal):
 1. linorder_rank R {y} x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
linorder_rank R {y} x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linorder_rank_insert:
  assumes "finite A" "y \<notin> A"
  shows   "linorder_rank R (insert y A) x =
             (if x \<noteq> y \<and> (y,x) \<in> R then 1 else 0) + linorder_rank R A x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R (insert y A) x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0) + linorder_rank R A x
[PROOF STEP]
using linorder_rank_union[of "{y}" A R x] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {y}; finite A; {y} \<inter> A = {}\<rbrakk> \<Longrightarrow> linorder_rank R ({y} \<union> A) x = linorder_rank R {y} x + linorder_rank R A x
finite A
y \<notin> A

goal (1 subgoal):
 1. linorder_rank R (insert y A) x = (if x \<noteq> y \<and> (y, x) \<in> R then 1 else 0) + linorder_rank R A x
[PROOF STEP]
by (auto simp: linorder_rank_singleton)


[STATEMENT]
lemma linorder_rank_mono:
  assumes "linorder_on B R" "finite A" "A \<subseteq> B" "(x, y) \<in> R"
  shows   "linorder_rank R A x \<le> linorder_rank R A y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R A x \<le> linorder_rank R A y
[PROOF STEP]
unfolding linorder_rank_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {y \<in> A - {x}. (y, x) \<in> R} \<le> card {ya \<in> A - {y}. (ya, y) \<in> R}
[PROOF STEP]
proof (rule card_mono)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite {ya \<in> A - {y}. (ya, y) \<in> R}
 2. {y \<in> A - {x}. (y, x) \<in> R} \<subseteq> {ya \<in> A - {y}. (ya, y) \<in> R}
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
finite A
A \<subseteq> B
(x, y) \<in> R
[PROOF STEP]
have trans: "trans R" and antisym: "antisym R"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
finite A
A \<subseteq> B
(x, y) \<in> R

goal (1 subgoal):
 1. trans R &&& antisym R
[PROOF STEP]
by (simp_all add: linorder_on_def)
[PROOF STATE]
proof (state)
this:
trans R
antisym R

goal (2 subgoals):
 1. finite {ya \<in> A - {y}. (ya, y) \<in> R}
 2. {y \<in> A - {x}. (y, x) \<in> R} \<subseteq> {ya \<in> A - {y}. (ya, y) \<in> R}
[PROOF STEP]
from assms antisym
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
finite A
A \<subseteq> B
(x, y) \<in> R
antisym R
[PROOF STEP]
show "{y \<in> A - {x}. (y, x) \<in> R} \<subseteq> {ya \<in> A - {y}. (ya, y) \<in> R}"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
finite A
A \<subseteq> B
(x, y) \<in> R
antisym R

goal (1 subgoal):
 1. {y \<in> A - {x}. (y, x) \<in> R} \<subseteq> {ya \<in> A - {y}. (ya, y) \<in> R}
[PROOF STEP]
by (auto intro: transD[OF trans] simp: antisym_def)
[PROOF STATE]
proof (state)
this:
{y \<in> A - {x}. (y, x) \<in> R} \<subseteq> {ya \<in> A - {y}. (ya, y) \<in> R}

goal (1 subgoal):
 1. finite {ya \<in> A - {y}. (ya, y) \<in> R}
[PROOF STEP]
qed (insert assms, simp_all)


[STATEMENT]
lemma linorder_rank_strict_mono:
  assumes "linorder_on B R" "finite A" "A \<subseteq> B" "y \<in> A" "(y, x) \<in> R" "x \<noteq> y"
  shows   "linorder_rank R A y < linorder_rank R A x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R A y < linorder_rank R A x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linorder_rank R A y < linorder_rank R A x
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
[PROOF STEP]
have trans: "trans R"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R

goal (1 subgoal):
 1. trans R
[PROOF STEP]
by (simp add: linorder_on_def)
[PROOF STATE]
proof (state)
this:
trans R

goal (1 subgoal):
 1. linorder_rank R A y < linorder_rank R A x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
finite A
A \<subseteq> B
y \<in> A
(y, x) \<in> R
x \<noteq> y
[PROOF STEP]
have *: "(x, y) \<notin> R"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
finite A
A \<subseteq> B
y \<in> A
(y, x) \<in> R
x \<noteq> y

goal (1 subgoal):
 1. (x, y) \<notin> R
[PROOF STEP]
by (auto simp: linorder_on_def antisym_def)
[PROOF STATE]
proof (state)
this:
(x, y) \<notin> R

goal (1 subgoal):
 1. linorder_rank R A y < linorder_rank R A x
[PROOF STEP]
from this and \<open>(y,x) \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<notin> R
(y, x) \<in> R
[PROOF STEP]
have "{z\<in>A-{y}. (z, y) \<in> R} \<subseteq> {z\<in>A-{x}. (z,x) \<in> R}"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<notin> R
(y, x) \<in> R

goal (1 subgoal):
 1. {z \<in> A - {y}. (z, y) \<in> R} \<subseteq> {z \<in> A - {x}. (z, x) \<in> R}
[PROOF STEP]
by (auto intro: transD[OF trans])
[PROOF STATE]
proof (state)
this:
{z \<in> A - {y}. (z, y) \<in> R} \<subseteq> {z \<in> A - {x}. (z, x) \<in> R}

goal (1 subgoal):
 1. linorder_rank R A y < linorder_rank R A x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{z \<in> A - {y}. (z, y) \<in> R} \<subseteq> {z \<in> A - {x}. (z, x) \<in> R}

goal (1 subgoal):
 1. linorder_rank R A y < linorder_rank R A x
[PROOF STEP]
from * and assms
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<notin> R
linorder_on B R
finite A
A \<subseteq> B
y \<in> A
(y, x) \<in> R
x \<noteq> y
[PROOF STEP]
have "y \<notin> {z\<in>A-{y}. (z, y) \<in> R}" "y \<in> {z\<in>A-{x}. (z, x) \<in> R}"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<notin> R
linorder_on B R
finite A
A \<subseteq> B
y \<in> A
(y, x) \<in> R
x \<noteq> y

goal (1 subgoal):
 1. y \<notin> {z \<in> A - {y}. (z, y) \<in> R} &&& y \<in> {z \<in> A - {x}. (z, x) \<in> R}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<notin> {z \<in> A - {y}. (z, y) \<in> R}
y \<in> {z \<in> A - {x}. (z, x) \<in> R}

goal (1 subgoal):
 1. linorder_rank R A y < linorder_rank R A x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{z \<in> A - {y}. (z, y) \<in> R} \<subseteq> {z \<in> A - {x}. (z, x) \<in> R}
y \<notin> {z \<in> A - {y}. (z, y) \<in> R}
y \<in> {z \<in> A - {x}. (z, x) \<in> R}
[PROOF STEP]
have "{z\<in>A-{y}. (z, y) \<in> R} \<subset> {z\<in>A-{x}. (z,x) \<in> R}"
[PROOF STATE]
proof (prove)
using this:
{z \<in> A - {y}. (z, y) \<in> R} \<subseteq> {z \<in> A - {x}. (z, x) \<in> R}
y \<notin> {z \<in> A - {y}. (z, y) \<in> R}
y \<in> {z \<in> A - {x}. (z, x) \<in> R}

goal (1 subgoal):
 1. {z \<in> A - {y}. (z, y) \<in> R} \<subset> {z \<in> A - {x}. (z, x) \<in> R}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{z \<in> A - {y}. (z, y) \<in> R} \<subset> {z \<in> A - {x}. (z, x) \<in> R}

goal (1 subgoal):
 1. linorder_rank R A y < linorder_rank R A x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{z \<in> A - {y}. (z, y) \<in> R} \<subset> {z \<in> A - {x}. (z, x) \<in> R}

goal (1 subgoal):
 1. linorder_rank R A y < linorder_rank R A x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{z \<in> A - {y}. (z, y) \<in> R} \<subset> {z \<in> A - {x}. (z, x) \<in> R}
linorder_on B R
finite A
A \<subseteq> B
y \<in> A
(y, x) \<in> R
x \<noteq> y

goal (1 subgoal):
 1. linorder_rank R A y < linorder_rank R A x
[PROOF STEP]
unfolding linorder_rank_def
[PROOF STATE]
proof (prove)
using this:
{z \<in> A - {y}. (z, y) \<in> R} \<subset> {z \<in> A - {x}. (z, x) \<in> R}
linorder_on B R
finite A
A \<subseteq> B
y \<in> A
(y, x) \<in> R
x \<noteq> y

goal (1 subgoal):
 1. card {ya \<in> A - {y}. (ya, y) \<in> R} < card {y \<in> A - {x}. (y, x) \<in> R}
[PROOF STEP]
by (intro psubset_card_mono) auto
[PROOF STATE]
proof (state)
this:
linorder_rank R A y < linorder_rank R A x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linorder_rank_le_iff:
  assumes "linorder_on B R" "finite A" "A \<subseteq> B" "x \<in> A" "y \<in> A"
  shows   "linorder_rank R A x \<le> linorder_rank R A y \<longleftrightarrow> (x, y) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
proof (cases "x = y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
 2. x \<noteq> y \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
 2. x \<noteq> y \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
finite A
A \<subseteq> B
x \<in> A
y \<in> A
x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
finite A
A \<subseteq> B
x \<in> A
y \<in> A
x = y

goal (1 subgoal):
 1. (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
by (auto simp: linorder_on_def refl_on_def)
[PROOF STATE]
proof (state)
this:
(linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)

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

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
[PROOF STEP]
have trans: "trans R"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R

goal (1 subgoal):
 1. trans R
[PROOF STEP]
by (simp_all add: linorder_on_def)
[PROOF STATE]
proof (state)
this:
trans R

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
finite A
A \<subseteq> B
x \<in> A
y \<in> A
[PROOF STEP]
have "x \<in> B" "y \<in> B"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
finite A
A \<subseteq> B
x \<in> A
y \<in> A

goal (1 subgoal):
 1. x \<in> B &&& y \<in> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> B
y \<in> B

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
with \<open>linorder_on B R\<close> and False
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
x \<noteq> y
x \<in> B
y \<in> B
[PROOF STEP]
have "((x,y) \<in> R \<and> (y,x) \<notin> R) \<or> ((y,x) \<in> R \<and> (x,y) \<notin> R)"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
x \<noteq> y
x \<in> B
y \<in> B

goal (1 subgoal):
 1. (x, y) \<in> R \<and> (y, x) \<notin> R \<or> (y, x) \<in> R \<and> (x, y) \<notin> R
[PROOF STEP]
by (fastforce simp: linorder_on_def antisym_def total_on_def)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> R \<and> (y, x) \<notin> R \<or> (y, x) \<in> R \<and> (x, y) \<notin> R

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> R \<and> (y, x) \<notin> R \<or> (y, x) \<in> R \<and> (x, y) \<notin> R

goal (1 subgoal):
 1. (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x, y) \<in> R \<and> (y, x) \<notin> R \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
 2. (y, x) \<in> R \<and> (x, y) \<notin> R \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
assume "(x,y) \<in> R \<and> (y,x) \<notin> R"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> R \<and> (y, x) \<notin> R

goal (2 subgoals):
 1. (x, y) \<in> R \<and> (y, x) \<notin> R \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
 2. (y, x) \<in> R \<and> (x, y) \<notin> R \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
finite A
A \<subseteq> B
x \<in> A
y \<in> A
(x, y) \<in> R \<and> (y, x) \<notin> R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
finite A
A \<subseteq> B
x \<in> A
y \<in> A
(x, y) \<in> R \<and> (y, x) \<notin> R

goal (1 subgoal):
 1. (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
by (auto intro!: linorder_rank_mono)
[PROOF STATE]
proof (state)
this:
(linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)

goal (1 subgoal):
 1. (y, x) \<in> R \<and> (x, y) \<notin> R \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (y, x) \<in> R \<and> (x, y) \<notin> R \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
assume *: "(y,x) \<in> R \<and> (x,y) \<notin> R"
[PROOF STATE]
proof (state)
this:
(y, x) \<in> R \<and> (x, y) \<notin> R

goal (1 subgoal):
 1. (y, x) \<in> R \<and> (x, y) \<notin> R \<Longrightarrow> (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
with linorder_rank_strict_mono[OF assms(1-3), of y x] assms False
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>y \<in> A; (y, x) \<in> R; x \<noteq> y\<rbrakk> \<Longrightarrow> linorder_rank R A y < linorder_rank R A x
linorder_on B R
finite A
A \<subseteq> B
x \<in> A
y \<in> A
x \<noteq> y
(y, x) \<in> R \<and> (x, y) \<notin> R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>y \<in> A; (y, x) \<in> R; x \<noteq> y\<rbrakk> \<Longrightarrow> linorder_rank R A y < linorder_rank R A x
linorder_on B R
finite A
A \<subseteq> B
x \<in> A
y \<in> A
x \<noteq> y
(y, x) \<in> R \<and> (x, y) \<notin> R

goal (1 subgoal):
 1. (linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linorder_rank_eq_iff:
  assumes "linorder_on B R" "finite A" "A \<subseteq> B" "x \<in> A" "y \<in> A"
  shows   "linorder_rank R A x = linorder_rank R A y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (linorder_rank R A x = linorder_rank R A y) = (x = y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. linorder_rank R A x = linorder_rank R A y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> linorder_rank R A x = linorder_rank R A y
[PROOF STEP]
assume "linorder_rank R A x = linorder_rank R A y"
[PROOF STATE]
proof (state)
this:
linorder_rank R A x = linorder_rank R A y

goal (2 subgoals):
 1. linorder_rank R A x = linorder_rank R A y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> linorder_rank R A x = linorder_rank R A y
[PROOF STEP]
with linorder_rank_le_iff[OF assms(1-5)] linorder_rank_le_iff[OF assms(1-3) assms(5,4)]
[PROOF STATE]
proof (chain)
picking this:
(linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
(linorder_rank R A y \<le> linorder_rank R A x) = ((y, x) \<in> R)
linorder_rank R A x = linorder_rank R A y
[PROOF STEP]
have "(x, y) \<in> R" "(y, x) \<in> R"
[PROOF STATE]
proof (prove)
using this:
(linorder_rank R A x \<le> linorder_rank R A y) = ((x, y) \<in> R)
(linorder_rank R A y \<le> linorder_rank R A x) = ((y, x) \<in> R)
linorder_rank R A x = linorder_rank R A y

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

goal (2 subgoals):
 1. linorder_rank R A x = linorder_rank R A y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> linorder_rank R A x = linorder_rank R A y
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
finite A
A \<subseteq> B
x \<in> A
y \<in> A
(x, y) \<in> R
(y, x) \<in> R
[PROOF STEP]
show "x = y"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
finite A
A \<subseteq> B
x \<in> A
y \<in> A
(x, y) \<in> R
(y, x) \<in> R

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (auto simp: linorder_on_def antisym_def)
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. x = y \<Longrightarrow> linorder_rank R A x = linorder_rank R A y
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma linorder_rank_set_sorted_wrt:
  assumes "linorder_on B R" "set xs \<subseteq> B" "sorted_wrt R xs" "x \<in> set xs" "distinct xs"
  shows   "linorder_rank R (set xs) x = index xs x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
define j where "j = index xs x"
[PROOF STATE]
proof (state)
this:
j = index xs x

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
set xs \<subseteq> B
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
distinct xs
[PROOF STEP]
have j: "j < length xs"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
set xs \<subseteq> B
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
distinct xs

goal (1 subgoal):
 1. j < length xs
[PROOF STEP]
by (simp add: j_def)
[PROOF STATE]
proof (state)
this:
j < length xs

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
have *: "x = y \<or> ((x, y) \<in> R \<and> (y, x) \<notin> R) \<or> ((y, x) \<in> R \<and> (x, y) \<notin> R)" if "y \<in> set xs" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y \<or> (x, y) \<in> R \<and> (y, x) \<notin> R \<or> (y, x) \<in> R \<and> (x, y) \<notin> R
[PROOF STEP]
using linorder_on_cases[OF assms(1), of x y] assms that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> B; y \<in> B\<rbrakk> \<Longrightarrow> x = y \<or> (x, y) \<in> R \<and> (y, x) \<notin> R \<or> (y, x) \<in> R \<and> (x, y) \<notin> R
linorder_on B R
set xs \<subseteq> B
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
distinct xs
y \<in> set xs

goal (1 subgoal):
 1. x = y \<or> (x, y) \<in> R \<and> (y, x) \<notin> R \<or> (y, x) \<in> R \<and> (x, y) \<notin> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?y \<in> set xs \<Longrightarrow> x = ?y \<or> (x, ?y) \<in> R \<and> (?y, x) \<notin> R \<or> (?y, x) \<in> R \<and> (x, ?y) \<notin> R

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
set xs \<subseteq> B
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
distinct xs
[PROOF STEP]
have "{y\<in>set xs-{x}. (y, x) \<in> R} = {y\<in>set xs-{x}. index xs y < index xs x}"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
set xs \<subseteq> B
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
distinct xs

goal (1 subgoal):
 1. {y \<in> set xs - {x}. (y, x) \<in> R} = {y \<in> set xs - {x}. index xs y < index xs x}
[PROOF STEP]
by (auto simp: sorted_wrt_linorder_index_less_iff[OF assms(1-3)] dest: *)
[PROOF STATE]
proof (state)
this:
{y \<in> set xs - {x}. (y, x) \<in> R} = {y \<in> set xs - {x}. index xs y < index xs x}

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{y \<in> set xs - {x}. (y, x) \<in> R} = {y \<in> set xs - {x}. index xs y < index xs x}

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
have "\<dots> = {y\<in>set xs. index xs y < j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y \<in> set xs - {x}. index xs y < index xs x} = {y \<in> set xs. index xs y < j}
[PROOF STEP]
by (auto simp: j_def)
[PROOF STATE]
proof (state)
this:
{y \<in> set xs - {x}. index xs y < index xs x} = {y \<in> set xs. index xs y < j}

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{y \<in> set xs - {x}. index xs y < index xs x} = {y \<in> set xs. index xs y < j}

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
have "\<dots> = (\<lambda>i. xs ! i) ` {i. i < j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y \<in> set xs. index xs y < j} = (!) xs ` {i. i < j}
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> set xs; index xs x < j\<rbrakk> \<Longrightarrow> x \<in> (!) xs ` {i. i < j}
 2. \<And>x i. i < j \<Longrightarrow> xs ! i \<in> set xs
 3. \<And>x i. i < j \<Longrightarrow> index xs (xs ! i) < j
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> set xs; index xs x < j\<rbrakk> \<Longrightarrow> x \<in> (!) xs ` {i. i < j}
 2. \<And>x i. i < j \<Longrightarrow> xs ! i \<in> set xs
 3. \<And>x i. i < j \<Longrightarrow> index xs (xs ! i) < j
[PROOF STEP]
assume "y \<in> set xs" "index xs y < j"
[PROOF STATE]
proof (state)
this:
y \<in> set xs
index xs y < j

goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> set xs; index xs x < j\<rbrakk> \<Longrightarrow> x \<in> (!) xs ` {i. i < j}
 2. \<And>x i. i < j \<Longrightarrow> xs ! i \<in> set xs
 3. \<And>x i. i < j \<Longrightarrow> index xs (xs ! i) < j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> set xs
index xs y < j

goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> set xs; index xs x < j\<rbrakk> \<Longrightarrow> x \<in> (!) xs ` {i. i < j}
 2. \<And>x i. i < j \<Longrightarrow> xs ! i \<in> set xs
 3. \<And>x i. i < j \<Longrightarrow> index xs (xs ! i) < j
[PROOF STEP]
from this and j
[PROOF STATE]
proof (chain)
picking this:
y \<in> set xs
index xs y < j
j < length xs
[PROOF STEP]
have "y = xs ! index xs y"
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
index xs y < j
j < length xs

goal (1 subgoal):
 1. y = xs ! index xs y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y = xs ! index xs y

goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> set xs; index xs x < j\<rbrakk> \<Longrightarrow> x \<in> (!) xs ` {i. i < j}
 2. \<And>x i. i < j \<Longrightarrow> xs ! i \<in> set xs
 3. \<And>x i. i < j \<Longrightarrow> index xs (xs ! i) < j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<in> set xs
index xs y < j
y = xs ! index xs y
[PROOF STEP]
show "y \<in> (!) xs ` {i. i < j}"
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
index xs y < j
y = xs ! index xs y

goal (1 subgoal):
 1. y \<in> (!) xs ` {i. i < j}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> (!) xs ` {i. i < j}

goal (2 subgoals):
 1. \<And>x i. i < j \<Longrightarrow> xs ! i \<in> set xs
 2. \<And>x i. i < j \<Longrightarrow> index xs (xs ! i) < j
[PROOF STEP]
qed (insert assms j, auto simp: index_nth_id)
[PROOF STATE]
proof (state)
this:
{y \<in> set xs. index xs y < j} = (!) xs ` {i. i < j}

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{y \<in> set xs. index xs y < j} = (!) xs ` {i. i < j}

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
from assms and j
[PROOF STATE]
proof (chain)
picking this:
linorder_on B R
set xs \<subseteq> B
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
distinct xs
j < length xs
[PROOF STEP]
have "card \<dots> = card {i. i < j}"
[PROOF STATE]
proof (prove)
using this:
linorder_on B R
set xs \<subseteq> B
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
distinct xs
j < length xs

goal (1 subgoal):
 1. card ((!) xs ` {i. i < j}) = card {i. i < j}
[PROOF STEP]
by (intro card_image) (auto simp: inj_on_def nth_eq_iff_index_eq)
[PROOF STATE]
proof (state)
this:
card ((!) xs ` {i. i < j}) = card {i. i < j}

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ((!) xs ` {i. i < j}) = card {i. i < j}

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
have "\<dots> = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. i < j} = j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. i < j} = j

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card {y \<in> set xs - {x}. (y, x) \<in> R} = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card {y \<in> set xs - {x}. (y, x) \<in> R} = j

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
by (simp only: j_def linorder_rank_def)
[PROOF STATE]
proof (state)
this:
linorder_rank R (set xs) x = index xs x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_linorder_rank:
  assumes "linorder_on B R" "finite A" "A \<subseteq> B"
  shows   "bij_betw (linorder_rank R A) A {..<card A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (linorder_rank R A) A {..<card A}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij_betw (linorder_rank R A) A {..<card A}
[PROOF STEP]
define xs where "xs = sorted_wrt_list_of_set R A"
[PROOF STATE]
proof (state)
this:
xs = sorted_wrt_list_of_set R A

goal (1 subgoal):
 1. bij_betw (linorder_rank R A) A {..<card A}
[PROOF STEP]
note xs = linorder_sorted_wrt_list_of_set[OF assms, folded xs_def]
[PROOF STATE]
proof (state)
this:
set xs = A
distinct xs
Linorder_Relations.sorted_wrt R xs

goal (1 subgoal):
 1. bij_betw (linorder_rank R A) A {..<card A}
[PROOF STEP]
from \<open>distinct xs\<close>
[PROOF STATE]
proof (chain)
picking this:
distinct xs
[PROOF STEP]
have len_xs: "length xs = card A"
[PROOF STATE]
proof (prove)
using this:
distinct xs

goal (1 subgoal):
 1. length xs = card A
[PROOF STEP]
by (subst \<open>set xs = A\<close> [symmetric]) (auto simp: distinct_card)
[PROOF STATE]
proof (state)
this:
length xs = card A

goal (1 subgoal):
 1. bij_betw (linorder_rank R A) A {..<card A}
[PROOF STEP]
have rank: "linorder_rank R (set xs) x = index xs x" if "x \<in> A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
using linorder_rank_set_sorted_wrt[OF assms(1), of xs x] assms that xs
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set xs \<subseteq> B; Linorder_Relations.sorted_wrt R xs; x \<in> set xs; distinct xs\<rbrakk> \<Longrightarrow> linorder_rank R (set xs) x = index xs x
linorder_on B R
finite A
A \<subseteq> B
x \<in> A
set xs = A
distinct xs
Linorder_Relations.sorted_wrt R xs

goal (1 subgoal):
 1. linorder_rank R (set xs) x = index xs x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> linorder_rank R (set xs) ?x = index xs ?x

goal (1 subgoal):
 1. bij_betw (linorder_rank R A) A {..<card A}
[PROOF STEP]
from xs len_xs
[PROOF STATE]
proof (chain)
picking this:
set xs = A
distinct xs
Linorder_Relations.sorted_wrt R xs
length xs = card A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set xs = A
distinct xs
Linorder_Relations.sorted_wrt R xs
length xs = card A

goal (1 subgoal):
 1. bij_betw (linorder_rank R A) A {..<card A}
[PROOF STEP]
by (intro bij_betw_byWitness[where f' = "\<lambda>i. xs ! i"])
       (auto simp: rank index_nth_id intro!: nth_mem)
[PROOF STATE]
proof (state)
this:
bij_betw (linorder_rank R A) A {..<card A}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem bij_betw_linorder_of_list:
  assumes "finite A"
  shows   "bij_betw linorder_of_list (permutations_of_set A) {R. linorder_on A R}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw linorder_of_list (permutations_of_set A) {R. linorder_on A R}
[PROOF STEP]
proof (intro bij_betw_byWitness[where f' = "\<lambda>R. sorted_wrt_list_of_set R A"] ballI subsetI,
       goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a. a \<in> permutations_of_set A \<Longrightarrow> sorted_wrt_list_of_set (linorder_of_list a) A = a
 2. \<And>a'. a' \<in> {R. linorder_on A R} \<Longrightarrow> linorder_of_list (sorted_wrt_list_of_set a' A) = a'
 3. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 4. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
case (1 xs)
[PROOF STATE]
proof (state)
this:
xs \<in> permutations_of_set A

goal (4 subgoals):
 1. \<And>a. a \<in> permutations_of_set A \<Longrightarrow> sorted_wrt_list_of_set (linorder_of_list a) A = a
 2. \<And>a'. a' \<in> {R. linorder_on A R} \<Longrightarrow> linorder_of_list (sorted_wrt_list_of_set a' A) = a'
 3. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 4. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
xs \<in> permutations_of_set A

goal (1 subgoal):
 1. sorted_wrt_list_of_set (linorder_of_list xs) A = xs
[PROOF STEP]
by (intro sorted_wrt_list_of_set_eqI) (auto simp: permutations_of_set_def)
[PROOF STATE]
proof (state)
this:
sorted_wrt_list_of_set (linorder_of_list xs) A = xs

goal (3 subgoals):
 1. \<And>a'. a' \<in> {R. linorder_on A R} \<Longrightarrow> linorder_of_list (sorted_wrt_list_of_set a' A) = a'
 2. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 3. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a'. a' \<in> {R. linorder_on A R} \<Longrightarrow> linorder_of_list (sorted_wrt_list_of_set a' A) = a'
 2. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 3. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
case (2 R)
[PROOF STATE]
proof (state)
this:
R \<in> {R. linorder_on A R}

goal (3 subgoals):
 1. \<And>a'. a' \<in> {R. linorder_on A R} \<Longrightarrow> linorder_of_list (sorted_wrt_list_of_set a' A) = a'
 2. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 3. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
hence R: "linorder_on A R"
[PROOF STATE]
proof (prove)
using this:
R \<in> {R. linorder_on A R}

goal (1 subgoal):
 1. linorder_on A R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
linorder_on A R

goal (3 subgoals):
 1. \<And>a'. a' \<in> {R. linorder_on A R} \<Longrightarrow> linorder_of_list (sorted_wrt_list_of_set a' A) = a'
 2. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 3. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
from R
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
[PROOF STEP]
have in_R: "x \<in> A" "y \<in> A" if "(x,y) \<in> R" for x y
[PROOF STATE]
proof (prove)
using this:
linorder_on A R

goal (1 subgoal):
 1. x \<in> A &&& y \<in> A
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
(x, y) \<in> R

goal (1 subgoal):
 1. x \<in> A &&& y \<in> A
[PROOF STEP]
by (auto simp: linorder_on_def refl_on_def)
[PROOF STATE]
proof (state)
this:
(?x, ?y) \<in> R \<Longrightarrow> ?x \<in> A
(?x, ?y) \<in> R \<Longrightarrow> ?y \<in> A

goal (3 subgoals):
 1. \<And>a'. a' \<in> {R. linorder_on A R} \<Longrightarrow> linorder_of_list (sorted_wrt_list_of_set a' A) = a'
 2. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 3. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
let ?xs = "sorted_wrt_list_of_set R A"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a'. a' \<in> {R. linorder_on A R} \<Longrightarrow> linorder_of_list (sorted_wrt_list_of_set a' A) = a'
 2. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 3. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
have xs: "distinct ?xs" "set ?xs = A" "sorted_wrt R ?xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (sorted_wrt_list_of_set R A) &&& set (sorted_wrt_list_of_set R A) = A &&& Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)
[PROOF STEP]
by (rule linorder_sorted_wrt_list_of_set[OF R] assms order.refl)+
[PROOF STATE]
proof (state)
this:
distinct (sorted_wrt_list_of_set R A)
set (sorted_wrt_list_of_set R A) = A
Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)

goal (3 subgoals):
 1. \<And>a'. a' \<in> {R. linorder_on A R} \<Longrightarrow> linorder_of_list (sorted_wrt_list_of_set a' A) = a'
 2. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 3. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
distinct (sorted_wrt_list_of_set R A)
set (sorted_wrt_list_of_set R A) = A
Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)

goal (1 subgoal):
 1. linorder_of_list (sorted_wrt_list_of_set R A) = R
[PROOF STEP]
using sorted_wrt_linorder_index_le_iff[OF R, of ?xs]
[PROOF STATE]
proof (prove)
using this:
distinct (sorted_wrt_list_of_set R A)
set (sorted_wrt_list_of_set R A) = A
Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)
\<lbrakk>set (sorted_wrt_list_of_set R A) \<subseteq> A; Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A); ?x \<in> set (sorted_wrt_list_of_set R A); ?y \<in> set (sorted_wrt_list_of_set R A)\<rbrakk> \<Longrightarrow> (index (sorted_wrt_list_of_set R A) ?x \<le> index (sorted_wrt_list_of_set R A) ?y) = ((?x, ?y) \<in> R)

goal (1 subgoal):
 1. linorder_of_list (sorted_wrt_list_of_set R A) = R
[PROOF STEP]
by (auto simp: linorder_of_list_def dest: in_R)
[PROOF STATE]
proof (state)
this:
linorder_of_list (sorted_wrt_list_of_set R A) = R

goal (2 subgoals):
 1. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 2. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 2. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
case (4 xs)
[PROOF STATE]
proof (state)
this:
xs \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R}

goal (2 subgoals):
 1. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 2. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R}
[PROOF STEP]
obtain R where R: "linorder_on A R" and xs [simp]: "xs = sorted_wrt_list_of_set R A"
[PROOF STATE]
proof (prove)
using this:
xs \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R}

goal (1 subgoal):
 1. (\<And>R. \<lbrakk>linorder_on A R; xs = sorted_wrt_list_of_set R A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
linorder_on A R
xs = sorted_wrt_list_of_set R A

goal (2 subgoals):
 1. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 2. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
let ?xs = "sorted_wrt_list_of_set R A"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 2. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
have xs: "distinct ?xs" "set ?xs = A" "sorted_wrt R ?xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (sorted_wrt_list_of_set R A) &&& set (sorted_wrt_list_of_set R A) = A &&& Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)
[PROOF STEP]
by (rule linorder_sorted_wrt_list_of_set[OF R] assms order.refl)+
[PROOF STATE]
proof (state)
this:
distinct (sorted_wrt_list_of_set R A)
set (sorted_wrt_list_of_set R A) = A
Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)

goal (2 subgoals):
 1. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
 2. \<And>x. x \<in> (\<lambda>R. sorted_wrt_list_of_set R A) ` {R. linorder_on A R} \<Longrightarrow> x \<in> permutations_of_set A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
distinct (sorted_wrt_list_of_set R A)
set (sorted_wrt_list_of_set R A) = A
Linorder_Relations.sorted_wrt R (sorted_wrt_list_of_set R A)

goal (1 subgoal):
 1. xs \<in> permutations_of_set A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs \<in> permutations_of_set A

goal (1 subgoal):
 1. \<And>x. x \<in> linorder_of_list ` permutations_of_set A \<Longrightarrow> x \<in> {R. linorder_on A R}
[PROOF STEP]
qed (auto simp: permutations_of_set_def)


[STATEMENT]
lemma nsqnr_def':
  "nsqn\<^sub>r r = (if \<pi>\<^sub>4(r) = inv then \<pi>\<^sub>2(r) - 1 else \<pi>\<^sub>2(r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn\<^sub>r r = (if \<pi>\<^sub>4 r = Aodv_Basic.inv then \<pi>\<^sub>2 r - 1 else \<pi>\<^sub>2 r)
[PROOF STEP]
unfolding nsqn\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<pi>\<^sub>4 r = val \<or> \<pi>\<^sub>2 r = 0 then \<pi>\<^sub>2 r else \<pi>\<^sub>2 r - 1) = (if \<pi>\<^sub>4 r = Aodv_Basic.inv then \<pi>\<^sub>2 r - 1 else \<pi>\<^sub>2 r)
[PROOF STEP]
by simp


[STATEMENT]
lemma nsqn\<^sub>r_zero [simp]:
  "\<And>dsn dsk flag hops nhip pre. nsqn\<^sub>r (0, dsk, flag, hops, nhip, pre) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dsn dsk flag hops nhip pre. nsqn\<^sub>r (0, dsk, flag, hops, nhip, pre) = 0
[PROOF STEP]
unfolding nsqn\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dsn dsk flag hops nhip pre. (if \<pi>\<^sub>4 (0, dsk, flag, hops, nhip, pre) = val \<or> \<pi>\<^sub>2 (0, dsk, flag, hops, nhip, pre) = 0 then \<pi>\<^sub>2 (0, dsk, flag, hops, nhip, pre) else \<pi>\<^sub>2 (0, dsk, flag, hops, nhip, pre) - 1) = 0
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma nsqn\<^sub>r_val [simp]:
  "\<And>dsn dsk hops nhip pre. nsqn\<^sub>r (dsn, dsk, val, hops, nhip, pre) = dsn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dsn dsk hops nhip pre. nsqn\<^sub>r (dsn, dsk, val, hops, nhip, pre) = dsn
[PROOF STEP]
unfolding nsqn\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dsn dsk hops nhip pre. (if \<pi>\<^sub>4 (dsn, dsk, val, hops, nhip, pre) = val \<or> \<pi>\<^sub>2 (dsn, dsk, val, hops, nhip, pre) = 0 then \<pi>\<^sub>2 (dsn, dsk, val, hops, nhip, pre) else \<pi>\<^sub>2 (dsn, dsk, val, hops, nhip, pre) - 1) = dsn
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma nsqn\<^sub>r_inv [simp]:
  "\<And>dsn dsk hops nhip pre. nsqn\<^sub>r (dsn, dsk, inv, hops, nhip, pre) = dsn - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dsn dsk hops nhip pre. nsqn\<^sub>r (dsn, dsk, Aodv_Basic.inv, hops, nhip, pre) = dsn - 1
[PROOF STEP]
unfolding nsqn\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dsn dsk hops nhip pre. (if \<pi>\<^sub>4 (dsn, dsk, Aodv_Basic.inv, hops, nhip, pre) = val \<or> \<pi>\<^sub>2 (dsn, dsk, Aodv_Basic.inv, hops, nhip, pre) = 0 then \<pi>\<^sub>2 (dsn, dsk, Aodv_Basic.inv, hops, nhip, pre) else \<pi>\<^sub>2 (dsn, dsk, Aodv_Basic.inv, hops, nhip, pre) - 1) = dsn - 1
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma nsqn\<^sub>r_lte_dsn [simp]:
  "\<And>dsn dsk flag hops nhip pre. nsqn\<^sub>r (dsn, dsk, flag, hops, nhip, pre) \<le> dsn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dsn dsk flag hops nhip pre. nsqn\<^sub>r (dsn, dsk, flag, hops, nhip, pre) \<le> dsn
[PROOF STEP]
unfolding nsqn\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dsn dsk flag hops nhip pre. (if \<pi>\<^sub>4 (dsn, dsk, flag, hops, nhip, pre) = val \<or> \<pi>\<^sub>2 (dsn, dsk, flag, hops, nhip, pre) = 0 then \<pi>\<^sub>2 (dsn, dsk, flag, hops, nhip, pre) else \<pi>\<^sub>2 (dsn, dsk, flag, hops, nhip, pre) - 1) \<le> dsn
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma nsqn_sqn_def:
  "\<And>rt dip. nsqn rt dip = (if flag rt dip = Some val \<or> sqn rt dip = 0
                            then sqn rt dip else sqn rt dip - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip. nsqn rt dip = (if flag rt dip = Some val \<or> sqn rt dip = 0 then sqn rt dip else sqn rt dip - 1)
[PROOF STEP]
unfolding nsqn_def sqn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip. (case rt dip of None \<Rightarrow> 0 | Some x \<Rightarrow> nsqn\<^sub>r x) = (if flag rt dip = Some val \<or> (case rt dip of None \<Rightarrow> 0 | Some r \<Rightarrow> \<pi>\<^sub>2 r) = 0 then case rt dip of None \<Rightarrow> 0 | Some r \<Rightarrow> \<pi>\<^sub>2 r else (case rt dip of None \<Rightarrow> 0 | Some r \<Rightarrow> \<pi>\<^sub>2 r) - 1)
[PROOF STEP]
by (clarsimp split: option.split)


[STATEMENT]
lemma not_in_kD_nsqn [simp]:
  assumes "dip \<notin> kD(rt)"
  shows "nsqn rt dip = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn rt dip = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<notin> kD rt

goal (1 subgoal):
 1. nsqn rt dip = 0
[PROOF STEP]
unfolding nsqn_def
[PROOF STATE]
proof (prove)
using this:
dip \<notin> kD rt

goal (1 subgoal):
 1. (case rt dip of None \<Rightarrow> 0 | Some x \<Rightarrow> nsqn\<^sub>r x) = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma kD_nsqn:
  assumes "dip \<in> kD(rt)"
    shows "nsqn rt dip = nsqn\<^sub>r(the (\<sigma>\<^bsub>route\<^esub>(rt, dip)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn rt dip = nsqn\<^sub>r (the (rt dip))
[PROOF STEP]
using assms [THEN kD_Some]
[PROOF STATE]
proof (prove)
using this:
\<exists>dsn dsk flag hops nhip pre. rt dip = Some (dsn, dsk, flag, hops, nhip, pre)

goal (1 subgoal):
 1. nsqn rt dip = nsqn\<^sub>r (the (rt dip))
[PROOF STEP]
unfolding nsqn_def
[PROOF STATE]
proof (prove)
using this:
\<exists>dsn dsk flag hops nhip pre. rt dip = Some (dsn, dsk, flag, hops, nhip, pre)

goal (1 subgoal):
 1. (case rt dip of None \<Rightarrow> 0 | Some x \<Rightarrow> nsqn\<^sub>r x) = nsqn\<^sub>r (the (rt dip))
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma nsqnr_r_flag_pred [simp, intro]:
    fixes dsn dsk flag hops nhip pre
  assumes "P (nsqn\<^sub>r (dsn, dsk, val, hops, nhip, pre))"
      and "P (nsqn\<^sub>r (dsn, dsk, inv, hops, nhip, pre))"
    shows "P (nsqn\<^sub>r (dsn, dsk, flag, hops, nhip, pre))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (nsqn\<^sub>r (dsn, dsk, flag, hops, nhip, pre))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P (nsqn\<^sub>r (dsn, dsk, val, hops, nhip, pre))
P (nsqn\<^sub>r (dsn, dsk, Aodv_Basic.inv, hops, nhip, pre))

goal (1 subgoal):
 1. P (nsqn\<^sub>r (dsn, dsk, flag, hops, nhip, pre))
[PROOF STEP]
by (cases flag) auto


[STATEMENT]
lemma nsqn\<^sub>r_addpreRT_inv [simp]:
  "\<And>rt dip npre dip'. dip \<in> kD(rt) \<Longrightarrow>
   nsqn\<^sub>r (the (the (addpreRT rt dip npre) dip')) = nsqn\<^sub>r (the (rt dip'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip npre dip'. dip \<in> kD rt \<Longrightarrow> nsqn\<^sub>r (the (the (addpreRT rt dip npre) dip')) = nsqn\<^sub>r (the (rt dip'))
[PROOF STEP]
unfolding addpreRT_def nsqn\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip npre dip'. dip \<in> kD rt \<Longrightarrow> (if \<pi>\<^sub>4 (the (the (map_option (\<lambda>s. rt(dip \<mapsto> addpre s npre)) (rt dip)) dip')) = val \<or> \<pi>\<^sub>2 (the (the (map_option (\<lambda>s. rt(dip \<mapsto> addpre s npre)) (rt dip)) dip')) = 0 then \<pi>\<^sub>2 (the (the (map_option (\<lambda>s. rt(dip \<mapsto> addpre s npre)) (rt dip)) dip')) else \<pi>\<^sub>2 (the (the (map_option (\<lambda>s. rt(dip \<mapsto> addpre s npre)) (rt dip)) dip')) - 1) = (if \<pi>\<^sub>4 (the (rt dip')) = val \<or> \<pi>\<^sub>2 (the (rt dip')) = 0 then \<pi>\<^sub>2 (the (rt dip')) else \<pi>\<^sub>2 (the (rt dip')) - 1)
[PROOF STEP]
by (frule kD_Some) (clarsimp split: option.split)


[STATEMENT]
lemma sqn_nsqn:
  "\<And>rt dip. sqn rt dip - 1 \<le> nsqn rt dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip. sqn rt dip - 1 \<le> nsqn rt dip
[PROOF STEP]
unfolding sqn_def nsqn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip. (case rt dip of None \<Rightarrow> 0 | Some r \<Rightarrow> \<pi>\<^sub>2 r) - 1 \<le> (case rt dip of None \<Rightarrow> 0 | Some x \<Rightarrow> nsqn\<^sub>r x)
[PROOF STEP]
by (clarsimp split: option.split)


[STATEMENT]
lemma nsqn_sqn: "nsqn rt dip \<le> sqn rt dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn rt dip \<le> sqn rt dip
[PROOF STEP]
unfolding sqn_def nsqn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case rt dip of None \<Rightarrow> 0 | Some x \<Rightarrow> nsqn\<^sub>r x) \<le> (case rt dip of None \<Rightarrow> 0 | Some r \<Rightarrow> \<pi>\<^sub>2 r)
[PROOF STEP]
by (cases "rt dip") auto


[STATEMENT]
lemma val_nsqn_sqn [elim, simp]:
  assumes "ip\<in>kD(rt)"
      and "the (flag rt ip) = val"
    shows "nsqn rt ip = sqn rt ip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD rt
the (flag rt ip) = val

goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip
[PROOF STEP]
unfolding nsqn_sqn_def
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD rt
the (flag rt ip) = val

goal (1 subgoal):
 1. (if flag rt ip = Some val \<or> sqn rt ip = 0 then sqn rt ip else sqn rt ip - 1) = sqn rt ip
[PROOF STEP]
by auto


[STATEMENT]
lemma vD_nsqn_sqn [elim, simp]:
  assumes "ip\<in>vD(rt)"
    shows "nsqn rt ip = sqn rt ip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip
[PROOF STEP]
from \<open>ip\<in>vD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
ip \<in> vD rt
[PROOF STEP]
have "ip\<in>kD(rt)"
                      and "the (flag rt ip) = val"
[PROOF STATE]
proof (prove)
using this:
ip \<in> vD rt

goal (1 subgoal):
 1. ip \<in> kD rt &&& the (flag rt ip) = val
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ip \<in> kD rt
the (flag rt ip) = val

goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD rt
the (flag rt ip) = val

goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
nsqn rt ip = sqn rt ip

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_nsqn_sqn [elim, simp]:
  assumes "ip\<in>kD(rt)"
      and "the (flag rt ip) = inv"
    shows "nsqn rt ip = sqn rt ip - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip - 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD rt
the (flag rt ip) = Aodv_Basic.inv

goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip - 1
[PROOF STEP]
unfolding nsqn_sqn_def
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD rt
the (flag rt ip) = Aodv_Basic.inv

goal (1 subgoal):
 1. (if flag rt ip = Some val \<or> sqn rt ip = 0 then sqn rt ip else sqn rt ip - 1) = sqn rt ip - 1
[PROOF STEP]
by auto


[STATEMENT]
lemma iD_nsqn_sqn [elim, simp]:
  assumes "ip\<in>iD(rt)"
    shows "nsqn rt ip = sqn rt ip - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip - 1
[PROOF STEP]
from \<open>ip\<in>iD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
ip \<in> iD rt
[PROOF STEP]
have "ip\<in>kD(rt)"
                      and "the (flag rt ip) = inv"
[PROOF STATE]
proof (prove)
using this:
ip \<in> iD rt

goal (1 subgoal):
 1. ip \<in> kD rt &&& the (flag rt ip) = Aodv_Basic.inv
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ip \<in> kD rt
the (flag rt ip) = Aodv_Basic.inv

goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip - 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD rt
the (flag rt ip) = Aodv_Basic.inv

goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip - 1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
nsqn rt ip = sqn rt ip - 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nsqn_update_changed_kno_val [simp]: "\<And>rt ip dsn dsk hops nhip.
  rt \<noteq> update rt ip (dsn, kno, val, hops, nhip, {})
   \<Longrightarrow> nsqn (update rt ip (dsn, kno, val, hops, nhip, {})) ip = dsn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt ip dsn dsk hops nhip. rt \<noteq> update rt ip (dsn, kno, val, hops, nhip, {}) \<Longrightarrow> nsqn (update rt ip (dsn, kno, val, hops, nhip, {})) ip = dsn
[PROOF STEP]
unfolding nsqn\<^sub>r_def update_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt ip dsn dsk hops nhip. rt \<noteq> (case rt ip of None \<Rightarrow> rt(ip \<mapsto> (dsn, kno, val, hops, nhip, {})) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (dsn, kno, val, hops, nhip, {}) then rt(ip \<mapsto> addpre (dsn, kno, val, hops, nhip, {}) (\<pi>\<^sub>7 s)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (dsn, kno, val, hops, nhip, {}) \<and> (\<pi>\<^sub>5 (dsn, kno, val, hops, nhip, {}) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt(ip \<mapsto> addpre (dsn, kno, val, hops, nhip, {}) (\<pi>\<^sub>7 s)) else if \<pi>\<^sub>3 (dsn, kno, val, hops, nhip, {}) = unk then rt(ip \<mapsto> (\<pi>\<^sub>2 s, snd (addpre (dsn, kno, val, hops, nhip, {}) (\<pi>\<^sub>7 s)))) else rt(ip \<mapsto> addpre s (\<pi>\<^sub>7 (dsn, kno, val, hops, nhip, {})))) \<Longrightarrow> nsqn (case rt ip of None \<Rightarrow> rt(ip \<mapsto> (dsn, kno, val, hops, nhip, {})) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (dsn, kno, val, hops, nhip, {}) then rt(ip \<mapsto> addpre (dsn, kno, val, hops, nhip, {}) (\<pi>\<^sub>7 s)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (dsn, kno, val, hops, nhip, {}) \<and> (\<pi>\<^sub>5 (dsn, kno, val, hops, nhip, {}) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt(ip \<mapsto> addpre (dsn, kno, val, hops, nhip, {}) (\<pi>\<^sub>7 s)) else if \<pi>\<^sub>3 (dsn, kno, val, hops, nhip, {}) = unk then rt(ip \<mapsto> (\<pi>\<^sub>2 s, snd (addpre (dsn, kno, val, hops, nhip, {}) (\<pi>\<^sub>7 s)))) else rt(ip \<mapsto> addpre s (\<pi>\<^sub>7 (dsn, kno, val, hops, nhip, {})))) ip = dsn
[PROOF STEP]
by (clarsimp simp: kD_nsqn split: option.split_asm option.split if_split_asm)
     (metis fun_upd_triv)


[STATEMENT]
lemma nsqn_addpreRT_inv [simp]:
  "\<And>rt dip npre dip'. dip \<in> kD(rt) \<Longrightarrow>
   nsqn (the (addpreRT rt dip npre)) dip' = nsqn rt dip'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip npre dip'. dip \<in> kD rt \<Longrightarrow> nsqn (the (addpreRT rt dip npre)) dip' = nsqn rt dip'
[PROOF STEP]
unfolding addpreRT_def nsqn_def nsqn\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip npre dip'. dip \<in> kD rt \<Longrightarrow> (case the (map_option (\<lambda>s. rt(dip \<mapsto> addpre s npre)) (rt dip)) dip' of None \<Rightarrow> 0 | Some r \<Rightarrow> if \<pi>\<^sub>4 r = val \<or> \<pi>\<^sub>2 r = 0 then \<pi>\<^sub>2 r else \<pi>\<^sub>2 r - 1) = (case rt dip' of None \<Rightarrow> 0 | Some r \<Rightarrow> if \<pi>\<^sub>4 r = val \<or> \<pi>\<^sub>2 r = 0 then \<pi>\<^sub>2 r else \<pi>\<^sub>2 r - 1)
[PROOF STEP]
by (frule kD_Some) (clarsimp split: option.split)


[STATEMENT]
lemma nsqn_update_other [simp]:
    fixes dsn dsk flag hops dip nhip pre rt ip
  assumes "dip \<noteq> ip"
    shows "nsqn (update rt ip (dsn, dsk, flag, hops, nhip, pre)) dip = nsqn rt dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn (update rt ip (dsn, dsk, flag, hops, nhip, pre)) dip = nsqn rt dip
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<noteq> ip

goal (1 subgoal):
 1. nsqn (update rt ip (dsn, dsk, flag, hops, nhip, pre)) dip = nsqn rt dip
[PROOF STEP]
unfolding nsqn_def
[PROOF STATE]
proof (prove)
using this:
dip \<noteq> ip

goal (1 subgoal):
 1. (case update rt ip (dsn, dsk, flag, hops, nhip, pre) dip of None \<Rightarrow> 0 | Some x \<Rightarrow> nsqn\<^sub>r x) = (case rt dip of None \<Rightarrow> 0 | Some x \<Rightarrow> nsqn\<^sub>r x)
[PROOF STEP]
by (clarsimp split: option.split)


[STATEMENT]
lemma nsqn_invalidate_eq:
  assumes "dip \<in> kD(rt)"
      and "dests dip = Some rsn"
    shows "nsqn (invalidate rt dests) dip = rsn - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dests dip = Some rsn

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
dests dip = Some rsn
[PROOF STEP]
obtain dsk hops nhip pre
      where "invalidate rt dests dip = Some (rsn, dsk, inv, hops, nhip, pre)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dests dip = Some rsn

goal (1 subgoal):
 1. (\<And>dsk hops nhip pre. invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding invalidate_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dests dip = Some rsn

goal (1 subgoal):
 1. (\<And>dsk hops nhip pre. (case (rt dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba)) = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)

goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)

goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
from \<open>dip \<in> kD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
[PROOF STEP]
have "dip \<in> kD(invalidate rt dests)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt

goal (1 subgoal):
 1. dip \<in> kD (invalidate rt dests)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dip \<in> kD (invalidate rt dests)

goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)
dip \<in> kD (invalidate rt dests)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)
dip \<in> kD (invalidate rt dests)

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
using \<open>dests dip = Some rsn\<close>
[PROOF STATE]
proof (prove)
using this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)
dip \<in> kD (invalidate rt dests)
dests dip = Some rsn

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nsqn (invalidate rt dests) dip = rsn - 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nsqn_invalidate_other [simp]:
  assumes "dip\<in>kD(rt)"
      and "dip\<notin>dom dests"
    shows "nsqn (invalidate rt dests) dip = nsqn rt dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = nsqn rt dip
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<notin> dom dests

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = nsqn rt dip
[PROOF STEP]
by (clarsimp simp add: kD_nsqn)


[STATEMENT]
lemma fresherI1 [intro]:
  assumes "nsqn\<^sub>r r < nsqn\<^sub>r r'"
    shows "r \<sqsubseteq> r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<sqsubseteq> r'
[PROOF STEP]
unfolding fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn\<^sub>r r < nsqn\<^sub>r r' \<or> nsqn\<^sub>r r = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5 r' \<le> \<pi>\<^sub>5 r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nsqn\<^sub>r r < nsqn\<^sub>r r'

goal (1 subgoal):
 1. nsqn\<^sub>r r < nsqn\<^sub>r r' \<or> nsqn\<^sub>r r = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5 r' \<le> \<pi>\<^sub>5 r
[PROOF STEP]
by simp


[STATEMENT]
lemma fresherI2 [intro]:
  assumes "nsqn\<^sub>r r = nsqn\<^sub>r r'"
      and "\<pi>\<^sub>5(r) \<ge> \<pi>\<^sub>5(r')"
    shows "r \<sqsubseteq> r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<sqsubseteq> r'
[PROOF STEP]
unfolding fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn\<^sub>r r < nsqn\<^sub>r r' \<or> nsqn\<^sub>r r = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5 r' \<le> \<pi>\<^sub>5 r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nsqn\<^sub>r r = nsqn\<^sub>r r'
\<pi>\<^sub>5 r' \<le> \<pi>\<^sub>5 r

goal (1 subgoal):
 1. nsqn\<^sub>r r < nsqn\<^sub>r r' \<or> nsqn\<^sub>r r = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5 r' \<le> \<pi>\<^sub>5 r
[PROOF STEP]
by simp


[STATEMENT]
lemma fresherI [intro]:
  assumes "(nsqn\<^sub>r r < nsqn\<^sub>r r') \<or> (nsqn\<^sub>r r  = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5(r) \<ge> \<pi>\<^sub>5(r'))"
    shows "r \<sqsubseteq> r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<sqsubseteq> r'
[PROOF STEP]
unfolding fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn\<^sub>r r < nsqn\<^sub>r r' \<or> nsqn\<^sub>r r = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5 r' \<le> \<pi>\<^sub>5 r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nsqn\<^sub>r r < nsqn\<^sub>r r' \<or> nsqn\<^sub>r r = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5 r' \<le> \<pi>\<^sub>5 r

goal (1 subgoal):
 1. nsqn\<^sub>r r < nsqn\<^sub>r r' \<or> nsqn\<^sub>r r = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5 r' \<le> \<pi>\<^sub>5 r
[PROOF STEP]
.


[STATEMENT]
lemma fresherE [elim]:
  assumes "r \<sqsubseteq> r'"
      and "nsqn\<^sub>r r < nsqn\<^sub>r r' \<Longrightarrow> P r r'"
      and "nsqn\<^sub>r r  = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5(r) \<ge> \<pi>\<^sub>5(r') \<Longrightarrow> P r r'"
    shows "P r r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P r r'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r \<sqsubseteq> r'
nsqn\<^sub>r r < nsqn\<^sub>r r' \<Longrightarrow> P r r'
nsqn\<^sub>r r = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5 r' \<le> \<pi>\<^sub>5 r \<Longrightarrow> P r r'

goal (1 subgoal):
 1. P r r'
[PROOF STEP]
unfolding fresher_def
[PROOF STATE]
proof (prove)
using this:
nsqn\<^sub>r r < nsqn\<^sub>r r' \<or> nsqn\<^sub>r r = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5 r' \<le> \<pi>\<^sub>5 r
nsqn\<^sub>r r < nsqn\<^sub>r r' \<Longrightarrow> P r r'
nsqn\<^sub>r r = nsqn\<^sub>r r' \<and> \<pi>\<^sub>5 r' \<le> \<pi>\<^sub>5 r \<Longrightarrow> P r r'

goal (1 subgoal):
 1. P r r'
[PROOF STEP]
by auto


[STATEMENT]
lemma fresher_trans [elim, trans]:
  "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z
[PROOF STEP]
unfolding fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nsqn\<^sub>r x < nsqn\<^sub>r y \<or> nsqn\<^sub>r x = nsqn\<^sub>r y \<and> \<pi>\<^sub>5 y \<le> \<pi>\<^sub>5 x; nsqn\<^sub>r y < nsqn\<^sub>r z \<or> nsqn\<^sub>r y = nsqn\<^sub>r z \<and> \<pi>\<^sub>5 z \<le> \<pi>\<^sub>5 y\<rbrakk> \<Longrightarrow> nsqn\<^sub>r x < nsqn\<^sub>r z \<or> nsqn\<^sub>r x = nsqn\<^sub>r z \<and> \<pi>\<^sub>5 z \<le> \<pi>\<^sub>5 x
[PROOF STEP]
by auto


[STATEMENT]
lemma not_fresher_trans [elim, trans]:
  "\<lbrakk> \<not>(x \<sqsubseteq> y); \<not>(z \<sqsubseteq> x) \<rbrakk> \<Longrightarrow> \<not>(z \<sqsubseteq> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> x \<sqsubseteq> y; \<not> z \<sqsubseteq> x\<rbrakk> \<Longrightarrow> \<not> z \<sqsubseteq> y
[PROOF STEP]
unfolding fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> (nsqn\<^sub>r x < nsqn\<^sub>r y \<or> nsqn\<^sub>r x = nsqn\<^sub>r y \<and> \<pi>\<^sub>5 y \<le> \<pi>\<^sub>5 x); \<not> (nsqn\<^sub>r z < nsqn\<^sub>r x \<or> nsqn\<^sub>r z = nsqn\<^sub>r x \<and> \<pi>\<^sub>5 x \<le> \<pi>\<^sub>5 z)\<rbrakk> \<Longrightarrow> \<not> (nsqn\<^sub>r z < nsqn\<^sub>r y \<or> nsqn\<^sub>r z = nsqn\<^sub>r y \<and> \<pi>\<^sub>5 y \<le> \<pi>\<^sub>5 z)
[PROOF STEP]
by auto


[STATEMENT]
lemma fresher_dsn_flag_hops_const [simp]:
  fixes dsn dsk dsk' flag hops nhip nhip' pre pre'
  shows "(dsn, dsk, flag, hops, nhip, pre) \<sqsubseteq> (dsn, dsk', flag, hops, nhip', pre')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dsn, dsk, flag, hops, nhip, pre) \<sqsubseteq> (dsn, dsk', flag, hops, nhip', pre')
[PROOF STEP]
unfolding fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn\<^sub>r (dsn, dsk, flag, hops, nhip, pre) < nsqn\<^sub>r (dsn, dsk', flag, hops, nhip', pre') \<or> nsqn\<^sub>r (dsn, dsk, flag, hops, nhip, pre) = nsqn\<^sub>r (dsn, dsk', flag, hops, nhip', pre') \<and> \<pi>\<^sub>5 (dsn, dsk', flag, hops, nhip', pre') \<le> \<pi>\<^sub>5 (dsn, dsk, flag, hops, nhip, pre)
[PROOF STEP]
by (cases flag) simp_all


[STATEMENT]
lemma addpre_fresher [simp]: "\<And>r npre. r \<sqsubseteq> (addpre r npre)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r npre. r \<sqsubseteq> addpre r npre
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma rt_fresher_def':
  "(rt\<^sub>1 \<sqsubseteq>\<^bsub>i\<^esub> rt\<^sub>2) = (nsqn\<^sub>r (the (rt\<^sub>1 i)) < nsqn\<^sub>r (the (rt\<^sub>2 i)) \<or>
                     nsqn\<^sub>r (the (rt\<^sub>1 i)) = nsqn\<^sub>r (the (rt\<^sub>2 i)) \<and> \<pi>\<^sub>5 (the (rt\<^sub>2 i)) \<le> \<pi>\<^sub>5 (the (rt\<^sub>1 i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rt\<^sub>1 \<sqsubseteq>\<^bsub>i\<^esub> rt\<^sub>2) = (nsqn\<^sub>r (the (rt\<^sub>1 i)) < nsqn\<^sub>r (the (rt\<^sub>2 i)) \<or> nsqn\<^sub>r (the (rt\<^sub>1 i)) = nsqn\<^sub>r (the (rt\<^sub>2 i)) \<and> \<pi>\<^sub>5 (the (rt\<^sub>2 i)) \<le> \<pi>\<^sub>5 (the (rt\<^sub>1 i)))
[PROOF STEP]
unfolding rt_fresher_def fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nsqn\<^sub>r (the (rt\<^sub>1 i)) < nsqn\<^sub>r (the (rt\<^sub>2 i)) \<or> nsqn\<^sub>r (the (rt\<^sub>1 i)) = nsqn\<^sub>r (the (rt\<^sub>2 i)) \<and> \<pi>\<^sub>5 (the (rt\<^sub>2 i)) \<le> \<pi>\<^sub>5 (the (rt\<^sub>1 i))) = (nsqn\<^sub>r (the (rt\<^sub>1 i)) < nsqn\<^sub>r (the (rt\<^sub>2 i)) \<or> nsqn\<^sub>r (the (rt\<^sub>1 i)) = nsqn\<^sub>r (the (rt\<^sub>2 i)) \<and> \<pi>\<^sub>5 (the (rt\<^sub>2 i)) \<le> \<pi>\<^sub>5 (the (rt\<^sub>1 i)))
[PROOF STEP]
by (rule refl)


[STATEMENT]
lemma single_rt_fresher [intro]:
  assumes "the (rt1 ip) \<sqsubseteq> the (rt2 ip)"
    shows "rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
the (rt1 ip) \<sqsubseteq> the (rt2 ip)

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2
[PROOF STEP]
unfolding rt_fresher_def
[PROOF STATE]
proof (prove)
using this:
the (rt1 ip) \<sqsubseteq> the (rt2 ip)

goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
.


[STATEMENT]
lemma rt_fresher_single [intro]:
  assumes "rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2"
    shows "the (rt1 ip) \<sqsubseteq> the (rt2 ip)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2

goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
unfolding rt_fresher_def
[PROOF STATE]
proof (prove)
using this:
the (rt1 ip) \<sqsubseteq> the (rt2 ip)

goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
.


[STATEMENT]
lemma rt_fresher_def2:
  assumes "dip \<in> kD(rt1)"
      and "dip \<in> kD(rt2)"
    shows "(rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2) = (nsqn rt1 dip < nsqn rt2 dip
                               \<or> (nsqn rt1 dip = nsqn rt2 dip
                                   \<and> the (dhops rt1 dip) \<ge> the (dhops rt2 dip)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2) = (nsqn rt1 dip < nsqn rt2 dip \<or> nsqn rt1 dip = nsqn rt2 dip \<and> the (dhops rt2 dip) \<le> the (dhops rt1 dip))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt1
dip \<in> kD rt2

goal (1 subgoal):
 1. (rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2) = (nsqn rt1 dip < nsqn rt2 dip \<or> nsqn rt1 dip = nsqn rt2 dip \<and> the (dhops rt2 dip) \<le> the (dhops rt1 dip))
[PROOF STEP]
unfolding rt_fresher_def fresher_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt1
dip \<in> kD rt2

goal (1 subgoal):
 1. (nsqn\<^sub>r (the (rt1 dip)) < nsqn\<^sub>r (the (rt2 dip)) \<or> nsqn\<^sub>r (the (rt1 dip)) = nsqn\<^sub>r (the (rt2 dip)) \<and> \<pi>\<^sub>5 (the (rt2 dip)) \<le> \<pi>\<^sub>5 (the (rt1 dip))) = (nsqn rt1 dip < nsqn rt2 dip \<or> nsqn rt1 dip = nsqn rt2 dip \<and> the (dhops rt2 dip) \<le> the (dhops rt1 dip))
[PROOF STEP]
by (simp add: kD_nsqn proj5_eq_dhops)


[STATEMENT]
lemma rt_fresherI1 [intro]:
  assumes "dip \<in> kD(rt1)"
      and "dip \<in> kD(rt2)"
      and "nsqn rt1 dip < nsqn rt2 dip"
    shows "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
unfolding rt_fresher_def2 [OF assms(1-2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn rt1 dip < nsqn rt2 dip \<or> nsqn rt1 dip = nsqn rt2 dip \<and> the (dhops rt2 dip) \<le> the (dhops rt1 dip)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
nsqn rt1 dip < nsqn rt2 dip

goal (1 subgoal):
 1. nsqn rt1 dip < nsqn rt2 dip \<or> nsqn rt1 dip = nsqn rt2 dip \<and> the (dhops rt2 dip) \<le> the (dhops rt1 dip)
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_fresherI2 [intro]:
  assumes "dip \<in> kD(rt1)"
      and "dip \<in> kD(rt2)"
      and "nsqn rt1 dip = nsqn rt2 dip"
      and "the (dhops rt1 dip) \<ge> the (dhops rt2 dip)"
    shows "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
unfolding rt_fresher_def2 [OF assms(1-2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn rt1 dip < nsqn rt2 dip \<or> nsqn rt1 dip = nsqn rt2 dip \<and> the (dhops rt2 dip) \<le> the (dhops rt1 dip)
[PROOF STEP]
using assms(3-4)
[PROOF STATE]
proof (prove)
using this:
nsqn rt1 dip = nsqn rt2 dip
the (dhops rt2 dip) \<le> the (dhops rt1 dip)

goal (1 subgoal):
 1. nsqn rt1 dip < nsqn rt2 dip \<or> nsqn rt1 dip = nsqn rt2 dip \<and> the (dhops rt2 dip) \<le> the (dhops rt1 dip)
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_fresherE [elim]:
  assumes "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
      and "dip \<in> kD(rt1)"
      and "dip \<in> kD(rt2)"
      and "\<lbrakk> nsqn rt1 dip < nsqn rt2 dip \<rbrakk> \<Longrightarrow> P rt1 rt2 dip"
      and "\<lbrakk> nsqn rt1 dip = nsqn rt2 dip;
             the (dhops rt1 dip) \<ge> the (dhops rt2 dip) \<rbrakk> \<Longrightarrow> P rt1 rt2 dip"
    shows "P rt1 rt2 dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P rt1 rt2 dip
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. P rt1 rt2 dip
[PROOF STEP]
unfolding rt_fresher_def2 [OF assms(2-3)]
[PROOF STATE]
proof (prove)
using this:
nsqn rt1 dip < nsqn rt2 dip \<or> nsqn rt1 dip = nsqn rt2 dip \<and> the (dhops rt2 dip) \<le> the (dhops rt1 dip)

goal (1 subgoal):
 1. P rt1 rt2 dip
[PROOF STEP]
using assms(4-5)
[PROOF STATE]
proof (prove)
using this:
nsqn rt1 dip < nsqn rt2 dip \<or> nsqn rt1 dip = nsqn rt2 dip \<and> the (dhops rt2 dip) \<le> the (dhops rt1 dip)
nsqn rt1 dip < nsqn rt2 dip \<Longrightarrow> P rt1 rt2 dip
\<lbrakk>nsqn rt1 dip = nsqn rt2 dip; the (dhops rt2 dip) \<le> the (dhops rt1 dip)\<rbrakk> \<Longrightarrow> P rt1 rt2 dip

goal (1 subgoal):
 1. P rt1 rt2 dip
[PROOF STEP]
by auto


[STATEMENT]
lemma rt_fresher_refl [simp]: "rt \<sqsubseteq>\<^bsub>dip\<^esub> rt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt \<sqsubseteq>\<^bsub>dip\<^esub> rt
[PROOF STEP]
unfolding rt_fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (rt dip) \<sqsubseteq> the (rt dip)
[PROOF STEP]
by simp


[STATEMENT]
lemma rt_fresher_trans [elim, trans]:
  assumes "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
      and "rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3"
    shows "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
unfolding rt_fresher_def
[PROOF STATE]
proof (prove)
using this:
the (rt1 dip) \<sqsubseteq> the (rt2 dip)
the (rt2 dip) \<sqsubseteq> the (rt3 dip)

goal (1 subgoal):
 1. the (rt1 dip) \<sqsubseteq> the (rt3 dip)
[PROOF STEP]
by auto