[STATEMENT]
lemma swap0in2:  assumes "set l = {x,y}" "x\<noteq>y" "length l = 2" "dist_perm l l"
  shows
    "x < y in (swap 0) l = (~ x < y in l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
proof (cases "x < y in l")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < y in l

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < y in l
[PROOF STEP]
have a: "index l x < index l y"
[PROOF STATE]
proof (prove)
using this:
x < y in l

goal (1 subgoal):
 1. index l x < index l y
[PROOF STEP]
unfolding before_in_def
[PROOF STATE]
proof (prove)
using this:
index l x < index l y \<and> y \<in> set l

goal (1 subgoal):
 1. index l x < index l y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l x < index l y

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
[PROOF STEP]
have drin: "x\<in>set l" "y\<in>set l"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}

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

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
length l = 2
[PROOF STEP]
have b: "index l y < 2"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}
length l = 2

goal (1 subgoal):
 1. index l y < 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l y < 2

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from a b
[PROOF STATE]
proof (chain)
picking this:
index l x < index l y
index l y < 2
[PROOF STEP]
have k: "index l x = 0" "index l y = 1"
[PROOF STATE]
proof (prove)
using this:
index l x < index l y
index l y < 2

goal (1 subgoal):
 1. index l x = 0 &&& index l y = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index l x = 0
index l y = 1

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have g: "x = l ! 0" "y = l ! 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = l ! 0 &&& y = l ! 1
[PROOF STEP]
using k nth_index assms(1)
[PROOF STATE]
proof (prove)
using this:
index l x = 0
index l y = 1
?x \<in> set ?xs \<Longrightarrow> ?xs ! index ?xs ?x = ?x
set l = {x, y}

goal (1 subgoal):
 1. x = l ! 0 &&& y = l ! 1
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
x = l ! 0
y = l ! 1

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "x < y in swap 0 l
      = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0)
            \<or>  x = l ! Suc 0 \<and> y = l ! 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
apply(rule before_in_swap)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist_perm l ?ys
 2. Suc 0 < length l
[PROOF STEP]
apply(fact assms(4))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc 0 < length l
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
length l = 2

goal (1 subgoal):
 1. Suc 0 < length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "\<dots> = (\<not> (x = l ! 0 \<and> y = l ! Suc 0)
            \<or>  x = l ! Suc 0 \<and> y = l ! 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
x < y in l

goal (1 subgoal):
 1. (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "\<dots> = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = False
[PROOF STEP]
using g assms(2)
[PROOF STATE]
proof (prove)
using this:
x = l ! 0
y = l ! 1
x \<noteq> y

goal (1 subgoal):
 1. (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = False

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x < y in swap 0 l = False
[PROOF STEP]
have "~ x < y in (swap 0) l"
[PROOF STATE]
proof (prove)
using this:
x < y in swap 0 l = False

goal (1 subgoal):
 1. \<not> x < y in swap 0 l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> x < y in swap 0 l

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

goal (1 subgoal):
 1. x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
\<not> x < y in swap 0 l
x < y in l

goal (1 subgoal):
 1. x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (\<not> x < y in l)

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x < y in l

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
x \<noteq> y
[PROOF STEP]
have "index l y \<noteq> index l x"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}
x \<noteq> y

goal (1 subgoal):
 1. index l y \<noteq> index l x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l y \<noteq> index l x

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
with False assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
\<not> x < y in l
set l = {x, y}
x \<noteq> y
index l y \<noteq> index l x
[PROOF STEP]
have a: "index l y < index l x"
[PROOF STATE]
proof (prove)
using this:
\<not> x < y in l
set l = {x, y}
x \<noteq> y
index l y \<noteq> index l x

goal (1 subgoal):
 1. index l y < index l x
[PROOF STEP]
by (metis before_in_def insert_iff linorder_neqE_nat)
[PROOF STATE]
proof (state)
this:
index l y < index l x

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
[PROOF STEP]
have drin: "x\<in>set l" "y\<in>set l"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}

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

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
length l = 2
[PROOF STEP]
have b: "index l x < 2"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}
length l = 2

goal (1 subgoal):
 1. index l x < 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l x < 2

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from a b
[PROOF STATE]
proof (chain)
picking this:
index l y < index l x
index l x < 2
[PROOF STEP]
have k: "index l x = 1" "index l y = 0"
[PROOF STATE]
proof (prove)
using this:
index l y < index l x
index l x < 2

goal (1 subgoal):
 1. index l x = 1 &&& index l y = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index l x = 1
index l y = 0

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
index l x = 1
index l y = 0
[PROOF STEP]
have g: "x = l ! 1" "y = l ! 0"
[PROOF STATE]
proof (prove)
using this:
index l x = 1
index l y = 0

goal (1 subgoal):
 1. x = l ! 1 &&& y = l ! 0
[PROOF STEP]
using k nth_index assms(1)
[PROOF STATE]
proof (prove)
using this:
index l x = 1
index l y = 0
index l x = 1
index l y = 0
?x \<in> set ?xs \<Longrightarrow> ?xs ! index ?xs ?x = ?x
set l = {x, y}

goal (1 subgoal):
 1. x = l ! 1 &&& y = l ! 0
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
x = l ! 1
y = l ! 0

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "x < y in swap 0 l
      = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0)
            \<or>  x = l ! Suc 0 \<and> y = l ! 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
apply(rule before_in_swap)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist_perm l ?ys
 2. Suc 0 < length l
[PROOF STEP]
apply(fact assms(4))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc 0 < length l
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
length l = 2

goal (1 subgoal):
 1. Suc 0 < length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "\<dots> = (x = l ! Suc 0 \<and> y = l ! 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> x < y in l

goal (1 subgoal):
 1. (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (x = l ! Suc 0 \<and> y = l ! 0)

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (x = l ! Suc 0 \<and> y = l ! 0)

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "\<dots> = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x = l ! Suc 0 \<and> y = l ! 0) = True
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
x = l ! 1
y = l ! 0

goal (1 subgoal):
 1. (x = l ! Suc 0 \<and> y = l ! 0) = True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x = l ! Suc 0 \<and> y = l ! 0) = True

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x < y in swap 0 l = True
[PROOF STEP]
have "x < y in (swap 0) l"
[PROOF STATE]
proof (prove)
using this:
x < y in swap 0 l = True

goal (1 subgoal):
 1. x < y in swap 0 l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < y in swap 0 l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x < y in swap 0 l

goal (1 subgoal):
 1. x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
x < y in swap 0 l
\<not> x < y in l

goal (1 subgoal):
 1. x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (\<not> x < y in l)

goal:
No subgoals!
[PROOF STEP]
qed