[STATEMENT]
lemma quality_increases_msg_fresh [elim]:
  assumes qinc: "\<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)"
      and "msg_fresh \<sigma> m"
    shows "msg_fresh \<sigma>' m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msg_fresh \<sigma>' m
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
msg_fresh \<sigma> m

goal (1 subgoal):
 1. msg_fresh \<sigma>' m
[PROOF STEP]
proof (cases m)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 x17 x18 x19. \<lbrakk>msg_fresh \<sigma> m; m = Rreq x11 x12 x13 x14 x15 x16 x17 x18 x19\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>msg_fresh \<sigma> m; m = Rrep x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 4. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 5. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
fix hops rreqid dip dsn dsk oip osn sip handled
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 x17 x18 x19. \<lbrakk>msg_fresh \<sigma> m; m = Rreq x11 x12 x13 x14 x15 x16 x17 x18 x19\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>msg_fresh \<sigma> m; m = Rrep x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 4. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 5. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
assume [simp]: "m = Rreq hops rreqid dip dsn dsk oip osn sip handled"
       and "msg_fresh \<sigma> m"
[PROOF STATE]
proof (state)
this:
m = Rreq hops rreqid dip dsn dsk oip osn sip handled
msg_fresh \<sigma> m

goal (5 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 x17 x18 x19. \<lbrakk>msg_fresh \<sigma> m; m = Rreq x11 x12 x13 x14 x15 x16 x17 x18 x19\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>msg_fresh \<sigma> m; m = Rrep x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 4. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 5. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m = Rreq hops rreqid dip dsn dsk oip osn sip handled
msg_fresh \<sigma> m
[PROOF STEP]
have "osn \<ge> 1" and "sip = oip \<or> (oip\<in>kD(rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip
                                           \<and> (nsqn (rt (\<sigma> sip)) oip = osn
                                                 \<longrightarrow> (the (dhops (rt (\<sigma> sip)) oip) \<le> hops
                                                      \<or> the (flag (rt (\<sigma> sip)) oip) = inv)))"
[PROOF STATE]
proof (prove)
using this:
m = Rreq hops rreqid dip dsn dsk oip osn sip handled
msg_fresh \<sigma> m

goal (1 subgoal):
 1. 1 \<le> osn &&& sip = oip \<or> oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> osn
sip = oip \<or> oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv)

goal (5 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 x17 x18 x19. \<lbrakk>msg_fresh \<sigma> m; m = Rreq x11 x12 x13 x14 x15 x16 x17 x18 x19\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>msg_fresh \<sigma> m; m = Rrep x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 4. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 5. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
sip = oip \<or> oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sip = oip \<or> oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. msg_fresh \<sigma>' m
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sip = oip \<Longrightarrow> msg_fresh \<sigma>' m
 2. oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
assume "sip = oip"
[PROOF STATE]
proof (state)
this:
sip = oip

goal (2 subgoals):
 1. sip = oip \<Longrightarrow> msg_fresh \<sigma>' m
 2. oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
with \<open>osn \<ge> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
1 \<le> osn
sip = oip
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> osn
sip = oip

goal (1 subgoal):
 1. msg_fresh \<sigma>' m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msg_fresh \<sigma>' m

goal (1 subgoal):
 1. oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
assume "oip\<in>kD(rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip
                                  \<and> (nsqn (rt (\<sigma> sip)) oip = osn
                                      \<longrightarrow> (the (dhops (rt (\<sigma> sip)) oip) \<le> hops
                                           \<or> the (flag (rt (\<sigma> sip)) oip) = inv))"
[PROOF STATE]
proof (state)
this:
oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
from qinc
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
have "quality_increases (\<sigma> sip) (\<sigma>' sip)"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)

goal (1 subgoal):
 1. quality_increases (\<sigma> sip) (\<sigma>' sip)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
quality_increases (\<sigma> sip) (\<sigma>' sip)

goal (1 subgoal):
 1. oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv)
quality_increases (\<sigma> sip) (\<sigma>' sip)
[PROOF STEP]
have "oip\<in>kD(rt (\<sigma>' sip)) \<and> osn \<le> nsqn (rt (\<sigma>' sip)) oip
                                           \<and> (nsqn (rt (\<sigma>' sip)) oip = osn
                                              \<longrightarrow> (the (dhops (rt (\<sigma>' sip)) oip) \<le> hops
                                                    \<or> the (flag (rt (\<sigma>' sip)) oip) = inv))"
[PROOF STATE]
proof (prove)
using this:
oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv)
quality_increases (\<sigma> sip) (\<sigma>' sip)

goal (1 subgoal):
 1. oip \<in> kD (rt (\<sigma>' sip)) \<and> osn \<le> nsqn (rt (\<sigma>' sip)) oip \<and> (nsqn (rt (\<sigma>' sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) oip) = Aodv_Basic.inv)
[PROOF STEP]
using \<open>osn \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv)
quality_increases (\<sigma> sip) (\<sigma>' sip)
1 \<le> osn

goal (1 subgoal):
 1. oip \<in> kD (rt (\<sigma>' sip)) \<and> osn \<le> nsqn (rt (\<sigma>' sip)) oip \<and> (nsqn (rt (\<sigma>' sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) oip) = Aodv_Basic.inv)
[PROOF STEP]
by (rule quality_increases_rreq_rrep_props [rotated 2])
[PROOF STATE]
proof (state)
this:
oip \<in> kD (rt (\<sigma>' sip)) \<and> osn \<le> nsqn (rt (\<sigma>' sip)) oip \<and> (nsqn (rt (\<sigma>' sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) oip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. oip \<in> kD (rt (\<sigma> sip)) \<and> osn \<le> nsqn (rt (\<sigma> sip)) oip \<and> (nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) oip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
with \<open>osn \<ge> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
1 \<le> osn
oip \<in> kD (rt (\<sigma>' sip)) \<and> osn \<le> nsqn (rt (\<sigma>' sip)) oip \<and> (nsqn (rt (\<sigma>' sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) oip) = Aodv_Basic.inv)
[PROOF STEP]
show "msg_fresh \<sigma>' m"
[PROOF STATE]
proof (prove)
using this:
1 \<le> osn
oip \<in> kD (rt (\<sigma>' sip)) \<and> osn \<le> nsqn (rt (\<sigma>' sip)) oip \<and> (nsqn (rt (\<sigma>' sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) oip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) oip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. msg_fresh \<sigma>' m
[PROOF STEP]
by (clarsimp)
[PROOF STATE]
proof (state)
this:
msg_fresh \<sigma>' m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
msg_fresh \<sigma>' m

goal (4 subgoals):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>msg_fresh \<sigma> m; m = Rrep x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 4. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>msg_fresh \<sigma> m; m = Rrep x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 4. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
fix hops dip dsn oip sip
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>msg_fresh \<sigma> m; m = Rrep x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 4. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
assume [simp]: "m = Rrep hops dip dsn oip sip"
       and "msg_fresh \<sigma> m"
[PROOF STATE]
proof (state)
this:
m = Rrep hops dip dsn oip sip
msg_fresh \<sigma> m

goal (4 subgoals):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>msg_fresh \<sigma> m; m = Rrep x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 4. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m = Rrep hops dip dsn oip sip
msg_fresh \<sigma> m
[PROOF STEP]
have "dsn \<ge> 1" and "sip = dip \<or> (dip\<in>kD(rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip
                                           \<and> (nsqn (rt (\<sigma> sip)) dip = dsn
                                                 \<longrightarrow> (the (dhops (rt (\<sigma> sip)) dip) \<le> hops
                                                      \<or> the (flag (rt (\<sigma> sip)) dip) = inv)))"
[PROOF STATE]
proof (prove)
using this:
m = Rrep hops dip dsn oip sip
msg_fresh \<sigma> m

goal (1 subgoal):
 1. 1 \<le> dsn &&& sip = dip \<or> dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> dsn
sip = dip \<or> dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv)

goal (4 subgoals):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>msg_fresh \<sigma> m; m = Rrep x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 4. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
sip = dip \<or> dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv)
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
using this:
sip = dip \<or> dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. msg_fresh \<sigma>' m
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sip = dip \<Longrightarrow> msg_fresh \<sigma>' m
 2. dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
assume "sip = dip"
[PROOF STATE]
proof (state)
this:
sip = dip

goal (2 subgoals):
 1. sip = dip \<Longrightarrow> msg_fresh \<sigma>' m
 2. dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
with \<open>dsn \<ge> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
1 \<le> dsn
sip = dip
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> dsn
sip = dip

goal (1 subgoal):
 1. msg_fresh \<sigma>' m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msg_fresh \<sigma>' m

goal (1 subgoal):
 1. dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
assume "dip\<in>kD(rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip
                                  \<and> (nsqn (rt (\<sigma> sip)) dip = dsn
                                      \<longrightarrow> (the (dhops (rt (\<sigma> sip)) dip) \<le> hops
                                           \<or> the (flag (rt (\<sigma> sip)) dip) = inv))"
[PROOF STATE]
proof (state)
this:
dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
from qinc
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
have "quality_increases (\<sigma> sip) (\<sigma>' sip)"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)

goal (1 subgoal):
 1. quality_increases (\<sigma> sip) (\<sigma>' sip)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
quality_increases (\<sigma> sip) (\<sigma>' sip)

goal (1 subgoal):
 1. dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv)
quality_increases (\<sigma> sip) (\<sigma>' sip)
[PROOF STEP]
have "dip\<in>kD(rt (\<sigma>' sip)) \<and> dsn \<le> nsqn (rt (\<sigma>' sip)) dip
                                           \<and> (nsqn (rt (\<sigma>' sip)) dip = dsn
                                              \<longrightarrow> (the (dhops (rt (\<sigma>' sip)) dip) \<le> hops
                                                    \<or> the (flag (rt (\<sigma>' sip)) dip) = inv))"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv)
quality_increases (\<sigma> sip) (\<sigma>' sip)

goal (1 subgoal):
 1. dip \<in> kD (rt (\<sigma>' sip)) \<and> dsn \<le> nsqn (rt (\<sigma>' sip)) dip \<and> (nsqn (rt (\<sigma>' sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) dip) = Aodv_Basic.inv)
[PROOF STEP]
using \<open>dsn \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv)
quality_increases (\<sigma> sip) (\<sigma>' sip)
1 \<le> dsn

goal (1 subgoal):
 1. dip \<in> kD (rt (\<sigma>' sip)) \<and> dsn \<le> nsqn (rt (\<sigma>' sip)) dip \<and> (nsqn (rt (\<sigma>' sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) dip) = Aodv_Basic.inv)
[PROOF STEP]
by (rule quality_increases_rreq_rrep_props [rotated 2])
[PROOF STATE]
proof (state)
this:
dip \<in> kD (rt (\<sigma>' sip)) \<and> dsn \<le> nsqn (rt (\<sigma>' sip)) dip \<and> (nsqn (rt (\<sigma>' sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) dip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. dip \<in> kD (rt (\<sigma> sip)) \<and> dsn \<le> nsqn (rt (\<sigma> sip)) dip \<and> (nsqn (rt (\<sigma> sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma> sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma> sip)) dip) = Aodv_Basic.inv) \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
with \<open>dsn \<ge> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
1 \<le> dsn
dip \<in> kD (rt (\<sigma>' sip)) \<and> dsn \<le> nsqn (rt (\<sigma>' sip)) dip \<and> (nsqn (rt (\<sigma>' sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) dip) = Aodv_Basic.inv)
[PROOF STEP]
show "msg_fresh \<sigma>' m"
[PROOF STATE]
proof (prove)
using this:
1 \<le> dsn
dip \<in> kD (rt (\<sigma>' sip)) \<and> dsn \<le> nsqn (rt (\<sigma>' sip)) dip \<and> (nsqn (rt (\<sigma>' sip)) dip = dsn \<longrightarrow> the (dhops (rt (\<sigma>' sip)) dip) \<le> hops \<or> the (flag (rt (\<sigma>' sip)) dip) = Aodv_Basic.inv)

goal (1 subgoal):
 1. msg_fresh \<sigma>' m
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
msg_fresh \<sigma>' m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
msg_fresh \<sigma>' m

goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
fix dests sip
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
assume [simp]: "m = Rerr dests sip"
       and "msg_fresh \<sigma> m"
[PROOF STATE]
proof (state)
this:
m = Rerr dests sip
msg_fresh \<sigma> m

goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m = Rerr dests sip
msg_fresh \<sigma> m
[PROOF STEP]
have *: "\<forall>rip\<in>dom(dests). rip\<in>kD(rt (\<sigma> sip))
                              \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip"
[PROOF STATE]
proof (prove)
using this:
m = Rerr dests sip
msg_fresh \<sigma> m

goal (1 subgoal):
 1. \<forall>rip\<in>dom dests. rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>rip\<in>dom dests. rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip

goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
have "\<forall>rip\<in>dom(dests). rip\<in>kD(rt (\<sigma>' sip))
                         \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>rip\<in>dom dests. rip \<in> kD (rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip
[PROOF STEP]
fix rip
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip
[PROOF STEP]
assume "rip\<in>dom(dests)"
[PROOF STATE]
proof (state)
this:
rip \<in> dom dests

goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>rip\<in>dom dests. rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
rip \<in> dom dests
[PROOF STEP]
have "rip\<in>kD(rt (\<sigma> sip))" and "the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip"
[PROOF STATE]
proof (prove)
using this:
\<forall>rip\<in>dom dests. rip \<in> kD (rt (\<sigma> sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
rip \<in> dom dests

goal (1 subgoal):
 1. rip \<in> kD (rt (\<sigma> sip)) &&& the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
[PROOF STEP]
by - (drule(1) bspec, clarsimp)+
[PROOF STATE]
proof (state)
this:
rip \<in> kD (rt (\<sigma> sip))
the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip

goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rip \<in> kD (rt (\<sigma> sip))
the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip

goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip
[PROOF STEP]
from qinc
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
have "quality_increases (\<sigma> sip) (\<sigma>' sip)"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. quality_increases (\<sigma> j) (\<sigma>' j)

goal (1 subgoal):
 1. quality_increases (\<sigma> sip) (\<sigma>' sip)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
quality_increases (\<sigma> sip) (\<sigma>' sip)

goal (1 subgoal):
 1. \<And>rip. rip \<in> dom dests \<Longrightarrow> rip \<in> kD (rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rip \<in> kD (rt (\<sigma> sip))
the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
quality_increases (\<sigma> sip) (\<sigma>' sip)
[PROOF STEP]
show "rip\<in>kD(rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip"
[PROOF STATE]
proof (prove)
using this:
rip \<in> kD (rt (\<sigma> sip))
the (dests rip) - 1 \<le> nsqn (rt (\<sigma> sip)) rip
quality_increases (\<sigma> sip) (\<sigma>' sip)

goal (1 subgoal):
 1. rip \<in> kD (rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rip \<in> kD (rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>rip\<in>dom dests. rip \<in> kD (rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip

goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>msg_fresh \<sigma> m; m = Rerr x31 x32\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 3. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>rip\<in>dom dests. rip \<in> kD (rt (\<sigma>' sip)) \<and> the (dests rip) - 1 \<le> nsqn (rt (\<sigma>' sip)) rip

goal (1 subgoal):
 1. msg_fresh \<sigma>' m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
msg_fresh \<sigma>' m

goal (2 subgoals):
 1. \<And>x41 x42. \<lbrakk>msg_fresh \<sigma> m; m = Newpkt x41 x42\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
 2. \<And>x51 x52 x53. \<lbrakk>msg_fresh \<sigma> m; m = Pkt x51 x52 x53\<rbrakk> \<Longrightarrow> msg_fresh \<sigma>' m
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma distinct_map_filterI: "distinct (map f xs) \<Longrightarrow> distinct (map f (filter P xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map f xs) \<Longrightarrow> distinct (map f (filter P xs))
[PROOF STEP]
by(induct xs) auto


[STATEMENT]
lemma map_of_filter_apply:
  "distinct (map fst xs)
  \<Longrightarrow> map_of (filter P xs) k =
  (case map_of xs k of None \<Rightarrow> None | Some v \<Rightarrow> if P (k, v) then Some v else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst xs) \<Longrightarrow> map_of (filter P xs) k = (case map_of xs k of None \<Rightarrow> None | Some v \<Rightarrow> if P (k, v) then Some v else None)
[PROOF STEP]
by(induct xs)(auto simp add: map_of_eq_None_iff split: option.split)


[STATEMENT]
lemma Mapping_RBT_inverse:
  fixes y :: "('a :: ccompare, 'b) rbt"
  assumes "y \<in> {t. ord.is_rbt cless t \<or> ID CCOMPARE('a) = None}"
  shows "impl_of (Mapping_RBT y) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. impl_of (Mapping_RBT y) = y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<in> {t. ord.is_rbt cless t \<or> ID ccompare = None}

goal (1 subgoal):
 1. impl_of (Mapping_RBT y) = y
[PROOF STEP]
by(auto simp add: Mapping_RBT_def Mapping_RBT'_inverse)


[STATEMENT]
lemma impl_of_inverse: "Mapping_RBT (impl_of t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping_RBT (impl_of t) = t
[PROOF STEP]
by(cases t)(auto simp add: Mapping_RBT'_inverse Mapping_RBT_def)


[STATEMENT]
lemma type_definition_mapping_rbt':
  "type_definition impl_of Mapping_RBT
    {t :: ('a, 'b) rbt. ord.is_rbt cless t \<or> ID CCOMPARE('a :: ccompare) = None}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_definition impl_of Mapping_RBT {t. ord.is_rbt cless t \<or> ID ccompare = None}
[PROOF STEP]
by unfold_locales(rule mapping_rbt.impl_of impl_of_inverse Mapping_RBT_inverse)+


[STATEMENT]
lemma rbt_eq_iff:
  "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t1 = t2) = (impl_of t1 = impl_of t2)
[PROOF STEP]
by (simp add: impl_of_inject)


[STATEMENT]
lemma rbt_eqI:
  "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2
[PROOF STEP]
by (simp add: rbt_eq_iff)


[STATEMENT]
lemma Mapping_RBT_impl_of [simp]:
  "Mapping_RBT (impl_of t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping_RBT (impl_of t) = t
[PROOF STEP]
by (simp add: impl_of_inverse)


[STATEMENT]
lemma unfoldr_rbt_entries_generator:
  "list.unfoldr rbt_entries_generator (init t) = entries t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.unfoldr rbt_entries_generator (init t) = entries t
[PROOF STEP]
by transfer(simp add: unfoldr_rbt_entries_generator)


[STATEMENT]
lemma lookup_RBT:
  "ord.is_rbt cless t \<Longrightarrow>
  lookup (Mapping_RBT t) = rbt_comp_lookup ccomp t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord.is_rbt cless t \<Longrightarrow> lookup (Mapping_RBT t) = rbt_comp_lookup ccomp t
[PROOF STEP]
by(simp add: lookup_def Mapping_RBT_inverse)


[STATEMENT]
lemma lookup_impl_of:
  "rbt_comp_lookup ccomp (impl_of t) = lookup t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_comp_lookup ccomp (impl_of t) = lookup t
[PROOF STEP]
by(transfer) simp


[STATEMENT]
lemma entries_impl_of:
  "RBT_Impl.entries (impl_of t) = entries t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RBT_Impl.entries (impl_of t) = entries t
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma keys_impl_of:
  "set (RBT_Impl.keys (impl_of t)) = keys t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (RBT_Impl.keys (impl_of t)) = keys t
[PROOF STEP]
by (simp add: keys_def)


[STATEMENT]
lemma lookup_empty [simp]:
  "lookup empty = Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup RBT_Mapping2.empty = Map.empty
[PROOF STEP]
by transfer (simp add: fun_eq_iff ord.rbt_lookup.simps)


[STATEMENT]
lemma fold_conv_fold:
  "fold f t = List.fold (case_prod f) (entries t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RBT_Mapping2.fold f t = List.fold (\<lambda>(x, y). f x y) (entries t)
[PROOF STEP]
by transfer(simp add: RBT_Impl.fold_def)


[STATEMENT]
lemma is_empty_empty [simp]:
  "is_empty t \<longleftrightarrow> t = empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_empty t = (t = RBT_Mapping2.empty)
[PROOF STEP]
by transfer (simp split: rbt.split)


[STATEMENT]
lemma mapping_linorder: "class.linorder (cless_eq :: 'a \<Rightarrow> 'a \<Rightarrow> bool) cless"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
using ID_ccompare_neq_None
[PROOF STATE]
proof (prove)
using this:
ID ccompare \<noteq> None

goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
by(clarsimp)(rule ID_ccompare)


[STATEMENT]
lemma mapping_comparator: "comparator (ccomp :: 'a comparator)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comparator ccomp
[PROOF STEP]
using ID_ccompare_neq_None
[PROOF STATE]
proof (prove)
using this:
ID ccompare \<noteq> None

goal (1 subgoal):
 1. comparator ccomp
[PROOF STEP]
by(clarsimp)(rule ID_ccompare')


[STATEMENT]
lemma is_rbt_impl_of [simp, intro]:
  fixes t :: "('a, 'b) mapping_rbt"
  shows "ord.is_rbt cless (impl_of t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord.is_rbt cless (impl_of t)
[PROOF STEP]
using ID_ccompare_neq_None impl_of [of t]
[PROOF STATE]
proof (prove)
using this:
ID ccompare \<noteq> None
impl_of t \<in> {t. ord.is_rbt cless t \<or> ID ccompare = None}

goal (1 subgoal):
 1. ord.is_rbt cless (impl_of t)
[PROOF STEP]
by auto


[STATEMENT]
lemma lookup_delete [simp]:
  "lookup (delete (k :: 'a) t) = (lookup t)(k := None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (delete k t) = (lookup t)(k := None)
[PROOF STEP]
by transfer(simp add: ID_ccompare_neq_None linorder.rbt_lookup_rbt_delete[OF mapping_linorder] restrict_complement_singleton_eq)


[STATEMENT]
lemma map_of_entries [simp]:
  "map_of (entries (t :: ('a, 'b) mapping_rbt)) = lookup t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (entries t) = lookup t
[PROOF STEP]
by transfer(simp add: ID_ccompare_neq_None linorder.map_of_entries[OF mapping_linorder] ord.is_rbt_rbt_sorted)


[STATEMENT]
lemma entries_lookup:
  "entries (t1 :: ('a, 'b) mapping_rbt) = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (entries t1 = entries t2) = (lookup t1 = lookup t2)
[PROOF STEP]
by transfer(simp add: ID_ccompare_neq_None linorder.entries_rbt_lookup[OF mapping_linorder] ord.is_rbt_rbt_sorted)


[STATEMENT]
lemma lookup_bulkload [simp]:
  "lookup (bulkload xs) = map_of (xs :: ('a \<times> 'b) list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (bulkload xs) = map_of xs
[PROOF STEP]
by transfer(simp add: linorder.rbt_lookup_rbt_bulkload[OF mapping_linorder])


[STATEMENT]
lemma lookup_map_entry [simp]:
  "lookup (map_entry (k :: 'a) f t) = (lookup t)(k := map_option f (lookup t k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (map_entry k f t) = (lookup t)(k := map_option f (lookup t k))
[PROOF STEP]
by transfer(simp add: ID_ccompare_neq_None linorder.rbt_lookup_rbt_map_entry[OF mapping_linorder])


[STATEMENT]
lemma lookup_map [simp]:
  "lookup (map f t) (k :: 'a) = map_option (f k) (lookup t k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (RBT_Mapping2.map f t) k = map_option (f k) (lookup t k)
[PROOF STEP]
by transfer(simp add: linorder.rbt_lookup_map[OF mapping_linorder])


[STATEMENT]
lemma RBT_lookup_empty [simp]:
  "ord.rbt_lookup cless (t :: ('a, 'b) RBT_Impl.rbt) = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ord.rbt_lookup cless t = Map.empty) = (t = rbt.Empty)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ord.rbt_lookup cless t = Map.empty) = (t = rbt.Empty)
[PROOF STEP]
interpret linorder "cless_eq :: 'a \<Rightarrow> 'a \<Rightarrow> bool" cless
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
by(rule mapping_linorder)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (local.rbt_lookup t = Map.empty) = (t = rbt.Empty)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.rbt_lookup t = Map.empty) = (t = rbt.Empty)
[PROOF STEP]
by(cases t)(auto simp add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
(local.rbt_lookup t = Map.empty) = (t = rbt.Empty)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lookup_empty_empty [simp]:
  "lookup t = Map.empty \<longleftrightarrow> (t :: ('a, 'b) mapping_rbt) = empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lookup t = Map.empty) = (t = RBT_Mapping2.empty)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma finite_dom_lookup [simp]: "finite (dom (lookup (t :: ('a, 'b) mapping_rbt)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (dom (lookup t))
[PROOF STEP]
by transfer(auto simp add: linorder.finite_dom_rbt_lookup[OF mapping_linorder])


[STATEMENT]
lemma card_com_lookup [unfolded length_map, simp]:
  "card (dom (lookup (t :: ('a, 'b) mapping_rbt))) = length (List.map fst (entries t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (dom (lookup t)) = length (list.map fst (entries t))
[PROOF STEP]
by transfer(auto simp add: linorder.rbt_lookup_keys[OF mapping_linorder] linorder.distinct_entries[OF mapping_linorder] RBT_Impl.keys_def ord.is_rbt_rbt_sorted ID_ccompare_neq_None List.card_set simp del: set_map length_map)


[STATEMENT]
lemma lookup_join:
  "lookup (join f (t1 :: ('a, 'b) mapping_rbt) t2) =
  (\<lambda>k. case lookup t1 k of None \<Rightarrow> lookup t2 k | Some v1 \<Rightarrow> Some (case lookup t2 k of None \<Rightarrow> v1 | Some v2 \<Rightarrow> f k v1 v2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (join f t1 t2) = (\<lambda>k. case lookup t1 k of None \<Rightarrow> lookup t2 k | Some v1 \<Rightarrow> Some (case lookup t2 k of None \<Rightarrow> v1 | Some v2 \<Rightarrow> f k v1 v2))
[PROOF STEP]
by transfer(auto simp add: fun_eq_iff linorder.rbt_lookup_rbt_unionwk[OF mapping_linorder] ord.is_rbt_rbt_sorted ID_ccompare_neq_None split: option.splits)


[STATEMENT]
lemma lookup_meet:
  "lookup (meet f (t1 :: ('a, 'b) mapping_rbt) t2) =
  (\<lambda>k. case lookup t1 k of None \<Rightarrow> None | Some v1 \<Rightarrow> case lookup t2 k of None \<Rightarrow> None | Some v2 \<Rightarrow> Some (f k v1 v2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (meet f t1 t2) = (\<lambda>k. case lookup t1 k of None \<Rightarrow> None | Some v1 \<Rightarrow> case lookup t2 k of None \<Rightarrow> None | Some v2 \<Rightarrow> Some (f k v1 v2))
[PROOF STEP]
by transfer(auto simp add: fun_eq_iff linorder.rbt_lookup_rbt_interwk[OF mapping_linorder] ord.is_rbt_rbt_sorted ID_ccompare_neq_None split: option.splits)


[STATEMENT]
lemma lookup_filter [simp]:
  "lookup (filter P (t :: ('a, 'b) mapping_rbt)) k =
  (case lookup t k of None \<Rightarrow> None | Some v \<Rightarrow> if P (k, v) then Some v else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (RBT_Mapping2.filter P t) k = (case lookup t k of None \<Rightarrow> None | Some v \<Rightarrow> if P (k, v) then Some v else None)
[PROOF STEP]
by transfer(simp split: option.split add: ID_ccompare_neq_None linorder.rbt_lookup_rbtreeify[OF mapping_linorder] linorder.sorted_filter[OF mapping_linorder] ord.is_rbt_rbt_sorted linorder.rbt_sorted_entries[OF mapping_linorder] distinct_map_filterI linorder.distinct_entries[OF mapping_linorder] map_of_filter_apply linorder.map_of_entries[OF mapping_linorder])


[STATEMENT]
lemma all_conv_all_lookup:
  "all P t \<longleftrightarrow> (\<forall>(k :: 'a) v. lookup t k = Some v \<longrightarrow> P k v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all P t = (\<forall>k v. lookup t k = Some v \<longrightarrow> P k v)
[PROOF STEP]
by transfer(auto simp add: ID_ccompare_neq_None linorder.rbt_lookup_keys[OF mapping_linorder] ord.is_rbt_rbt_sorted RBT_Impl.keys_def RBT_Impl_rbt_all_def linorder.map_of_entries[OF mapping_linorder, symmetric] linorder.distinct_entries[OF mapping_linorder] dest: map_of_SomeD intro: map_of_is_SomeI)


[STATEMENT]
lemma ex_conv_ex_lookup:
  "ex P t \<longleftrightarrow> (\<exists>(k :: 'a) v. lookup t k = Some v \<and> P k v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ex P t = (\<exists>k v. lookup t k = Some v \<and> P k v)
[PROOF STEP]
by transfer(auto simp add: ID_ccompare_neq_None linorder.rbt_lookup_keys[OF mapping_linorder] ord.is_rbt_rbt_sorted RBT_Impl.keys_def RBT_Impl_rbt_ex_def linorder.map_of_entries[OF mapping_linorder, symmetric] linorder.distinct_entries[OF mapping_linorder] intro: map_of_is_SomeI)


[STATEMENT]
lemma diag_lookup:
  "lookup (diag t) = (\<lambda>(k :: 'a, k'). if k = k' then lookup t k else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (diag t) = (\<lambda>(k, k'). if k = k' then lookup t k else None)
[PROOF STEP]
using linorder.rbt_lookup_RBT_Impl_diag[where ?'b='b, OF mapping_linorder]
[PROOF STATE]
proof (prove)
using this:
ord.rbt_lookup (less_prod cless_eq cless cless) (RBT_Impl_diag ?t) = (\<lambda>(k, k'). if k = k' then ord.rbt_lookup cless ?t k else None)

goal (1 subgoal):
 1. lookup (diag t) = (\<lambda>(k, k'). if k = k' then lookup t k else None)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<And>t. ord.rbt_lookup (less_prod cless_eq cless cless) (RBT_Impl_diag t) = (\<lambda>(k, k'). if k = k' then ord.rbt_lookup cless t k else None); ord.is_rbt cless t \<or> ID ccompare = None\<rbrakk> \<Longrightarrow> rbt_comp_lookup ccomp (RBT_Impl_diag t) = (\<lambda>(k, k'). if k = k' then rbt_comp_lookup ccomp t k else None)
[PROOF STEP]
apply (clarsimp simp add: ID_ccompare_neq_None ccompare_prod_def lt_of_comp_less_prod[symmetric]
  rbt_comp_lookup[OF comparator_prod[OF mapping_comparator mapping_comparator], symmetric]
  ID_Some split: option.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t x2. \<lbrakk>\<And>t. rbt_comp_lookup (comparator_prod x2 x2) (RBT_Impl_diag t) = (\<lambda>(k, k'). if k = k' then ord.rbt_lookup cless t k else None); ord.is_rbt (lt_of_comp x2) t; ID ccompare = Some x2\<rbrakk> \<Longrightarrow> (\<lambda>(k, k'). if k = k' then ord.rbt_lookup cless t k else None) = (\<lambda>(k, k'). if k = k' then rbt_comp_lookup ccomp t k else None)
[PROOF STEP]
apply (unfold rbt_comp_lookup[OF mapping_comparator], simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mapping_linorder': "class.linorder (cless_eq :: 'b \<Rightarrow> 'b \<Rightarrow> bool) cless"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
using ID_ccompare_neq_None'
[PROOF STATE]
proof (prove)
using this:
ID ccompare \<noteq> None

goal (1 subgoal):
 1. class.linorder cless_eq cless
[PROOF STEP]
by(clarsimp)(rule ID_ccompare)


[STATEMENT]
lemma mapping_comparator': "comparator (ccomp :: 'b comparator)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comparator ccomp
[PROOF STEP]
using ID_ccompare_neq_None'
[PROOF STATE]
proof (prove)
using this:
ID ccompare \<noteq> None

goal (1 subgoal):
 1. comparator ccomp
[PROOF STEP]
by(clarsimp)(rule ID_ccompare')


[STATEMENT]
lemma ccomp_comparator_prod:
  "ccomp = (comparator_prod ccomp ccomp :: ('a \<times> 'b)comparator)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccomp = comparator_prod ccomp ccomp
[PROOF STEP]
by(simp add: ccompare_prod_def lt_of_comp_less_prod ID_ccompare_neq_None ID_ccompare_neq_None' ID_Some split: option.splits)


[STATEMENT]
lemma lookup_product:
  "lookup (product f rbt1 rbt2) (a :: 'a, b :: 'b) =
  (case lookup rbt1 a of None \<Rightarrow> None
   | Some c \<Rightarrow> map_option (f a c b) (lookup rbt2 b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (product f rbt1 rbt2) (a, b) = (case lookup rbt1 a of None \<Rightarrow> None | Some c \<Rightarrow> map_option (f a c b) (lookup rbt2 b))
[PROOF STEP]
using mapping_linorder mapping_linorder'
[PROOF STATE]
proof (prove)
using this:
class.linorder cless_eq cless
class.linorder cless_eq cless

goal (1 subgoal):
 1. lookup (product f rbt1 rbt2) (a, b) = (case lookup rbt1 a of None \<Rightarrow> None | Some c \<Rightarrow> map_option (f a c b) (lookup rbt2 b))
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f rbt1 rbt2 a b. \<lbrakk>class.linorder cless_eq cless; class.linorder cless_eq cless; ord.is_rbt cless rbt1 \<or> ID ccompare = None; ord.is_rbt cless rbt2 \<or> ID ccompare = None\<rbrakk> \<Longrightarrow> rbt_comp_lookup ccomp (rbt_product f rbt1 rbt2) (a, b) = (case rbt_comp_lookup ccomp rbt1 a of None \<Rightarrow> None | Some c \<Rightarrow> map_option (f a c b) (rbt_comp_lookup ccomp rbt2 b))
[PROOF STEP]
apply (unfold ccomp_comparator_prod rbt_comp_lookup[OF comparator_prod[OF mapping_comparator mapping_comparator']]
  rbt_comp rbt_comp' lt_of_comp_less_prod)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f rbt1 rbt2 a b. \<lbrakk>class.linorder cless_eq cless; class.linorder cless_eq cless; ord.is_rbt cless rbt1 \<or> ID ccompare = None; ord.is_rbt cless rbt2 \<or> ID ccompare = None\<rbrakk> \<Longrightarrow> ord.rbt_lookup (less_prod cless_eq cless cless) (rbt_product f rbt1 rbt2) (a, b) = (case ord.rbt_lookup cless rbt1 a of None \<Rightarrow> None | Some c \<Rightarrow> map_option (f a c b) (ord.rbt_lookup cless rbt2 b))
[PROOF STEP]
apply (simp add: ID_ccompare_neq_None ID_ccompare_neq_None' rbt_lookup_rbt_product)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "filter_bool_list bs xs = map snd (filter fst (zip bs xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_bool_list bs xs = map snd (filter fst (zip bs xs))
[PROOF STEP]
by(induct bs xs rule: filter_bool_list.induct) auto


[STATEMENT]
lemma filter_bool_list_in:
  "n < length xs \<Longrightarrow> n < length bs \<Longrightarrow> bs!n \<Longrightarrow> xs!n \<in> set (filter_bool_list bs xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; n < length bs; bs ! n\<rbrakk> \<Longrightarrow> xs ! n \<in> set (filter_bool_list bs xs)
[PROOF STEP]
proof (induct bs xs arbitrary: n rule: filter_bool_list.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>uu_ n. \<lbrakk>n < length uu_; n < length []; [] ! n\<rbrakk> \<Longrightarrow> uu_ ! n \<in> set (filter_bool_list [] uu_)
 2. \<And>v va n. \<lbrakk>n < length []; n < length (v # va); (v # va) ! n\<rbrakk> \<Longrightarrow> [] ! n \<in> set (filter_bool_list (v # va) [])
 3. \<And>b bs x xs n. \<lbrakk>\<And>n. \<lbrakk>b; n < length xs; n < length bs; bs ! n\<rbrakk> \<Longrightarrow> xs ! n \<in> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; n < length xs; n < length bs; bs ! n\<rbrakk> \<Longrightarrow> xs ! n \<in> set (filter_bool_list bs xs); n < length (x # xs); n < length (b # bs); (b # bs) ! n\<rbrakk> \<Longrightarrow> (x # xs) ! n \<in> set (filter_bool_list (b # bs) (x # xs))
[PROOF STEP]
case (3 b bs x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>b; ?n < length xs; ?n < length bs; bs ! ?n\<rbrakk> \<Longrightarrow> xs ! ?n \<in> set (filter_bool_list bs xs)
\<lbrakk>\<not> b; ?n < length xs; ?n < length bs; bs ! ?n\<rbrakk> \<Longrightarrow> xs ! ?n \<in> set (filter_bool_list bs xs)
n < length (x # xs)
n < length (b # bs)
(b # bs) ! n

goal (3 subgoals):
 1. \<And>uu_ n. \<lbrakk>n < length uu_; n < length []; [] ! n\<rbrakk> \<Longrightarrow> uu_ ! n \<in> set (filter_bool_list [] uu_)
 2. \<And>v va n. \<lbrakk>n < length []; n < length (v # va); (v # va) ! n\<rbrakk> \<Longrightarrow> [] ! n \<in> set (filter_bool_list (v # va) [])
 3. \<And>b bs x xs n. \<lbrakk>\<And>n. \<lbrakk>b; n < length xs; n < length bs; bs ! n\<rbrakk> \<Longrightarrow> xs ! n \<in> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; n < length xs; n < length bs; bs ! n\<rbrakk> \<Longrightarrow> xs ! n \<in> set (filter_bool_list bs xs); n < length (x # xs); n < length (b # bs); (b # bs) ! n\<rbrakk> \<Longrightarrow> (x # xs) ! n \<in> set (filter_bool_list (b # bs) (x # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>b; ?n < length xs; ?n < length bs; bs ! ?n\<rbrakk> \<Longrightarrow> xs ! ?n \<in> set (filter_bool_list bs xs)
\<lbrakk>\<not> b; ?n < length xs; ?n < length bs; bs ! ?n\<rbrakk> \<Longrightarrow> xs ! ?n \<in> set (filter_bool_list bs xs)
n < length (x # xs)
n < length (b # bs)
(b # bs) ! n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b; ?n < length xs; ?n < length bs; bs ! ?n\<rbrakk> \<Longrightarrow> xs ! ?n \<in> set (filter_bool_list bs xs)
\<lbrakk>\<not> b; ?n < length xs; ?n < length bs; bs ! ?n\<rbrakk> \<Longrightarrow> xs ! ?n \<in> set (filter_bool_list bs xs)
n < length (x # xs)
n < length (b # bs)
(b # bs) ! n

goal (1 subgoal):
 1. (x # xs) ! n \<in> set (filter_bool_list (b # bs) (x # xs))
[PROOF STEP]
by(cases n) auto
[PROOF STATE]
proof (state)
this:
(x # xs) ! n \<in> set (filter_bool_list (b # bs) (x # xs))

goal (2 subgoals):
 1. \<And>uu_ n. \<lbrakk>n < length uu_; n < length []; [] ! n\<rbrakk> \<Longrightarrow> uu_ ! n \<in> set (filter_bool_list [] uu_)
 2. \<And>v va n. \<lbrakk>n < length []; n < length (v # va); (v # va) ! n\<rbrakk> \<Longrightarrow> [] ! n \<in> set (filter_bool_list (v # va) [])
[PROOF STEP]
qed auto


[STATEMENT]
lemma filter_bool_list_not_elem: "x \<notin> set xs \<Longrightarrow> x \<notin> set (filter_bool_list bs xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> x \<notin> set (filter_bool_list bs xs)
[PROOF STEP]
by(induct bs xs rule: filter_bool_list.induct) auto


[STATEMENT]
lemma filter_bool_list_elem: "x \<in> set (filter_bool_list bs xs) \<Longrightarrow> x \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (filter_bool_list bs xs) \<Longrightarrow> x \<in> set xs
[PROOF STEP]
using filter_bool_list_not_elem
[PROOF STATE]
proof (prove)
using this:
?x \<notin> set ?xs \<Longrightarrow> ?x \<notin> set (filter_bool_list ?bs ?xs)

goal (1 subgoal):
 1. x \<in> set (filter_bool_list bs xs) \<Longrightarrow> x \<in> set xs
[PROOF STEP]
by fast


[STATEMENT]
lemma filter_bool_list_not_in:
  "distinct xs \<Longrightarrow> n < length xs\<Longrightarrow> n < length bs \<Longrightarrow> bs!n = False
    \<Longrightarrow> xs!n \<notin> set (filter_bool_list bs xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs)
[PROOF STEP]
proof (induct bs xs arbitrary: n rule: filter_bool_list.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>uu_ n. \<lbrakk>distinct uu_; n < length uu_; n < length []; [] ! n = False\<rbrakk> \<Longrightarrow> uu_ ! n \<notin> set (filter_bool_list [] uu_)
 2. \<And>v va n. \<lbrakk>distinct []; n < length []; n < length (v # va); (v # va) ! n = False\<rbrakk> \<Longrightarrow> [] ! n \<notin> set (filter_bool_list (v # va) [])
 3. \<And>b bs x xs n. \<lbrakk>\<And>n. \<lbrakk>b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); distinct (x # xs); n < length (x # xs); n < length (b # bs); (b # bs) ! n = False\<rbrakk> \<Longrightarrow> (x # xs) ! n \<notin> set (filter_bool_list (b # bs) (x # xs))
[PROOF STEP]
case (3 b bs x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
\<lbrakk>\<not> b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
distinct (x # xs)
n < length (x # xs)
n < length (b # bs)
(b # bs) ! n = False

goal (3 subgoals):
 1. \<And>uu_ n. \<lbrakk>distinct uu_; n < length uu_; n < length []; [] ! n = False\<rbrakk> \<Longrightarrow> uu_ ! n \<notin> set (filter_bool_list [] uu_)
 2. \<And>v va n. \<lbrakk>distinct []; n < length []; n < length (v # va); (v # va) ! n = False\<rbrakk> \<Longrightarrow> [] ! n \<notin> set (filter_bool_list (v # va) [])
 3. \<And>b bs x xs n. \<lbrakk>\<And>n. \<lbrakk>b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); distinct (x # xs); n < length (x # xs); n < length (b # bs); (b # bs) ! n = False\<rbrakk> \<Longrightarrow> (x # xs) ! n \<notin> set (filter_bool_list (b # bs) (x # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
\<lbrakk>\<not> b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
distinct (x # xs)
n < length (x # xs)
n < length (b # bs)
(b # bs) ! n = False
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
\<lbrakk>\<not> b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
distinct (x # xs)
n < length (x # xs)
n < length (b # bs)
(b # bs) ! n = False

goal (1 subgoal):
 1. (x # xs) ! n \<notin> set (filter_bool_list (b # bs) (x # xs))
[PROOF STEP]
proof(induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); distinct (x # xs); 0 < length (x # xs); 0 < length (b # bs); (b # bs) ! 0 = False\<rbrakk> \<Longrightarrow> (x # xs) ! 0 \<notin> set (filter_bool_list (b # bs) (x # xs))
 2. \<And>n. \<lbrakk>\<lbrakk>\<And>n. \<lbrakk>b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); distinct (x # xs); n < length (x # xs); n < length (b # bs); (b # bs) ! n = False\<rbrakk> \<Longrightarrow> (x # xs) ! n \<notin> set (filter_bool_list (b # bs) (x # xs)); \<And>n. \<lbrakk>b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); distinct (x # xs); Suc n < length (x # xs); Suc n < length (b # bs); (b # bs) ! Suc n = False\<rbrakk> \<Longrightarrow> (x # xs) ! Suc n \<notin> set (filter_bool_list (b # bs) (x # xs))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<lbrakk>b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
\<lbrakk>\<not> b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
distinct (x # xs)
0 < length (x # xs)
0 < length (b # bs)
(b # bs) ! 0 = False

goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); distinct (x # xs); 0 < length (x # xs); 0 < length (b # bs); (b # bs) ! 0 = False\<rbrakk> \<Longrightarrow> (x # xs) ! 0 \<notin> set (filter_bool_list (b # bs) (x # xs))
 2. \<And>n. \<lbrakk>\<lbrakk>\<And>n. \<lbrakk>b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); distinct (x # xs); n < length (x # xs); n < length (b # bs); (b # bs) ! n = False\<rbrakk> \<Longrightarrow> (x # xs) ! n \<notin> set (filter_bool_list (b # bs) (x # xs)); \<And>n. \<lbrakk>b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); distinct (x # xs); Suc n < length (x # xs); Suc n < length (b # bs); (b # bs) ! Suc n = False\<rbrakk> \<Longrightarrow> (x # xs) ! Suc n \<notin> set (filter_bool_list (b # bs) (x # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
\<lbrakk>\<not> b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
distinct (x # xs)
0 < length (x # xs)
0 < length (b # bs)
(b # bs) ! 0 = False
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
\<lbrakk>\<not> b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
distinct (x # xs)
0 < length (x # xs)
0 < length (b # bs)
(b # bs) ! 0 = False

goal (1 subgoal):
 1. (x # xs) ! 0 \<notin> set (filter_bool_list (b # bs) (x # xs))
[PROOF STEP]
using filter_bool_list_not_elem
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
\<lbrakk>\<not> b; distinct xs; ?n < length xs; ?n < length bs; bs ! ?n = False\<rbrakk> \<Longrightarrow> xs ! ?n \<notin> set (filter_bool_list bs xs)
distinct (x # xs)
0 < length (x # xs)
0 < length (b # bs)
(b # bs) ! 0 = False
?x \<notin> set ?xs \<Longrightarrow> ?x \<notin> set (filter_bool_list ?bs ?xs)

goal (1 subgoal):
 1. (x # xs) ! 0 \<notin> set (filter_bool_list (b # bs) (x # xs))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(x # xs) ! 0 \<notin> set (filter_bool_list (b # bs) (x # xs))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>\<And>n. \<lbrakk>b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); distinct (x # xs); n < length (x # xs); n < length (b # bs); (b # bs) ! n = False\<rbrakk> \<Longrightarrow> (x # xs) ! n \<notin> set (filter_bool_list (b # bs) (x # xs)); \<And>n. \<lbrakk>b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); \<And>n. \<lbrakk>\<not> b; distinct xs; n < length xs; n < length bs; bs ! n = False\<rbrakk> \<Longrightarrow> xs ! n \<notin> set (filter_bool_list bs xs); distinct (x # xs); Suc n < length (x # xs); Suc n < length (b # bs); (b # bs) ! Suc n = False\<rbrakk> \<Longrightarrow> (x # xs) ! Suc n \<notin> set (filter_bool_list (b # bs) (x # xs))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(x # xs) ! n \<notin> set (filter_bool_list (b # bs) (x # xs))

goal (2 subgoals):
 1. \<And>uu_ n. \<lbrakk>distinct uu_; n < length uu_; n < length []; [] ! n = False\<rbrakk> \<Longrightarrow> uu_ ! n \<notin> set (filter_bool_list [] uu_)
 2. \<And>v va n. \<lbrakk>distinct []; n < length []; n < length (v # va); (v # va) ! n = False\<rbrakk> \<Longrightarrow> [] ! n \<notin> set (filter_bool_list (v # va) [])
[PROOF STEP]
qed auto


[STATEMENT]
lemma filter_bool_list_elem_nth:  "ys \<in> set (filter_bool_list bs xs)
  \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys \<in> set (filter_bool_list bs xs) \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs
[PROOF STEP]
proof(induct bs xs arbitrary: ys rule: filter_bool_list.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>uu_ ys. ys \<in> set (filter_bool_list [] uu_) \<Longrightarrow> \<exists>n. ys = uu_ ! n \<and> [] ! n \<and> n < length [] \<and> n < length uu_
 2. \<And>v va ys. ys \<in> set (filter_bool_list (v # va) []) \<Longrightarrow> \<exists>n. ys = [] ! n \<and> (v # va) ! n \<and> n < length (v # va) \<and> n < length []
 3. \<And>b bs x xs ys. \<lbrakk>\<And>ys. \<lbrakk>b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; \<And>ys. \<lbrakk>\<not> b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; ys \<in> set (filter_bool_list (b # bs) (x # xs))\<rbrakk> \<Longrightarrow> \<exists>n. ys = (x # xs) ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length (x # xs)
[PROOF STEP]
case (1 xs)
[PROOF STATE]
proof (state)
this:
ys \<in> set (filter_bool_list [] xs)

goal (3 subgoals):
 1. \<And>uu_ ys. ys \<in> set (filter_bool_list [] uu_) \<Longrightarrow> \<exists>n. ys = uu_ ! n \<and> [] ! n \<and> n < length [] \<and> n < length uu_
 2. \<And>v va ys. ys \<in> set (filter_bool_list (v # va) []) \<Longrightarrow> \<exists>n. ys = [] ! n \<and> (v # va) ! n \<and> n < length (v # va) \<and> n < length []
 3. \<And>b bs x xs ys. \<lbrakk>\<And>ys. \<lbrakk>b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; \<And>ys. \<lbrakk>\<not> b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; ys \<in> set (filter_bool_list (b # bs) (x # xs))\<rbrakk> \<Longrightarrow> \<exists>n. ys = (x # xs) ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys \<in> set (filter_bool_list [] xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ys \<in> set (filter_bool_list [] xs)

goal (1 subgoal):
 1. \<exists>n. ys = xs ! n \<and> [] ! n \<and> n < length [] \<and> n < length xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>n. ys = xs ! n \<and> [] ! n \<and> n < length [] \<and> n < length xs

goal (2 subgoals):
 1. \<And>v va ys. ys \<in> set (filter_bool_list (v # va) []) \<Longrightarrow> \<exists>n. ys = [] ! n \<and> (v # va) ! n \<and> n < length (v # va) \<and> n < length []
 2. \<And>b bs x xs ys. \<lbrakk>\<And>ys. \<lbrakk>b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; \<And>ys. \<lbrakk>\<not> b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; ys \<in> set (filter_bool_list (b # bs) (x # xs))\<rbrakk> \<Longrightarrow> \<exists>n. ys = (x # xs) ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length (x # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v va ys. ys \<in> set (filter_bool_list (v # va) []) \<Longrightarrow> \<exists>n. ys = [] ! n \<and> (v # va) ! n \<and> n < length (v # va) \<and> n < length []
 2. \<And>b bs x xs ys. \<lbrakk>\<And>ys. \<lbrakk>b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; \<And>ys. \<lbrakk>\<not> b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; ys \<in> set (filter_bool_list (b # bs) (x # xs))\<rbrakk> \<Longrightarrow> \<exists>n. ys = (x # xs) ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length (x # xs)
[PROOF STEP]
case (2 b bs)
[PROOF STATE]
proof (state)
this:
ys \<in> set (filter_bool_list (b # bs) [])

goal (2 subgoals):
 1. \<And>v va ys. ys \<in> set (filter_bool_list (v # va) []) \<Longrightarrow> \<exists>n. ys = [] ! n \<and> (v # va) ! n \<and> n < length (v # va) \<and> n < length []
 2. \<And>b bs x xs ys. \<lbrakk>\<And>ys. \<lbrakk>b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; \<And>ys. \<lbrakk>\<not> b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; ys \<in> set (filter_bool_list (b # bs) (x # xs))\<rbrakk> \<Longrightarrow> \<exists>n. ys = (x # xs) ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys \<in> set (filter_bool_list (b # bs) [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ys \<in> set (filter_bool_list (b # bs) [])

goal (1 subgoal):
 1. \<exists>n. ys = [] ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>n. ys = [] ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length []

goal (1 subgoal):
 1. \<And>b bs x xs ys. \<lbrakk>\<And>ys. \<lbrakk>b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; \<And>ys. \<lbrakk>\<not> b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; ys \<in> set (filter_bool_list (b # bs) (x # xs))\<rbrakk> \<Longrightarrow> \<exists>n. ys = (x # xs) ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length (x # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b bs x xs ys. \<lbrakk>\<And>ys. \<lbrakk>b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; \<And>ys. \<lbrakk>\<not> b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; ys \<in> set (filter_bool_list (b # bs) (x # xs))\<rbrakk> \<Longrightarrow> \<exists>n. ys = (x # xs) ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length (x # xs)
[PROOF STEP]
case (3 b bs y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>b; ?ys \<in> set (filter_bool_list bs ysa__)\<rbrakk> \<Longrightarrow> \<exists>n. ?ys = ysa__ ! n \<and> bs ! n \<and> n < length bs \<and> n < length ysa__
\<lbrakk>\<not> b; ?ys \<in> set (filter_bool_list bs ysa__)\<rbrakk> \<Longrightarrow> \<exists>n. ?ys = ysa__ ! n \<and> bs ! n \<and> n < length bs \<and> n < length ysa__
ys \<in> set (filter_bool_list (b # bs) (y # ysa__))

goal (1 subgoal):
 1. \<And>b bs x xs ys. \<lbrakk>\<And>ys. \<lbrakk>b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; \<And>ys. \<lbrakk>\<not> b; ys \<in> set (filter_bool_list bs xs)\<rbrakk> \<Longrightarrow> \<exists>n. ys = xs ! n \<and> bs ! n \<and> n < length bs \<and> n < length xs; ys \<in> set (filter_bool_list (b # bs) (x # xs))\<rbrakk> \<Longrightarrow> \<exists>n. ys = (x # xs) ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>b; ?ys \<in> set (filter_bool_list bs ysa__)\<rbrakk> \<Longrightarrow> \<exists>n. ?ys = ysa__ ! n \<and> bs ! n \<and> n < length bs \<and> n < length ysa__
\<lbrakk>\<not> b; ?ys \<in> set (filter_bool_list bs ysa__)\<rbrakk> \<Longrightarrow> \<exists>n. ?ys = ysa__ ! n \<and> bs ! n \<and> n < length bs \<and> n < length ysa__
ys \<in> set (filter_bool_list (b # bs) (y # ysa__))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b; ?ys \<in> set (filter_bool_list bs ysa__)\<rbrakk> \<Longrightarrow> \<exists>n. ?ys = ysa__ ! n \<and> bs ! n \<and> n < length bs \<and> n < length ysa__
\<lbrakk>\<not> b; ?ys \<in> set (filter_bool_list bs ysa__)\<rbrakk> \<Longrightarrow> \<exists>n. ?ys = ysa__ ! n \<and> bs ! n \<and> n < length bs \<and> n < length ysa__
ys \<in> set (filter_bool_list (b # bs) (y # ysa__))

goal (1 subgoal):
 1. \<exists>n. ys = (y # ysa__) ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length (y # ysa__)
[PROOF STEP]
by(cases b) (force)+
[PROOF STATE]
proof (state)
this:
\<exists>n. ys = (y # ysa__) ! n \<and> (b # bs) ! n \<and> n < length (b # bs) \<and> n < length (y # ysa__)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma filter_bool_list_set_nth:
  "set (filter_bool_list bs xs) = {xs ! n |n. bs ! n \<and> n < length bs \<and> n < length xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (filter_bool_list bs xs) = {xs ! n |n. bs ! n \<and> n < length bs \<and> n < length xs}
[PROOF STEP]
by (auto simp: filter_bool_list_in filter_bool_list_elem_nth)


[STATEMENT]
lemma filter_bool_list_exist_length: "A \<subseteq> set xs
  \<Longrightarrow> \<exists>bs. length bs = length xs \<and> A = set (filter_bool_list bs xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> A = set (filter_bool_list bs xs)
[PROOF STEP]
proof(induct xs arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. A \<subseteq> set [] \<Longrightarrow> \<exists>bs. length bs = length [] \<and> A = set (filter_bool_list bs [])
 2. \<And>a xs A. \<lbrakk>\<And>A. A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> A = set (filter_bool_list bs xs); A \<subseteq> set (a # xs)\<rbrakk> \<Longrightarrow> \<exists>bs. length bs = length (a # xs) \<and> A = set (filter_bool_list bs (a # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
A \<subseteq> set []

goal (2 subgoals):
 1. \<And>A. A \<subseteq> set [] \<Longrightarrow> \<exists>bs. length bs = length [] \<and> A = set (filter_bool_list bs [])
 2. \<And>a xs A. \<lbrakk>\<And>A. A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> A = set (filter_bool_list bs xs); A \<subseteq> set (a # xs)\<rbrakk> \<Longrightarrow> \<exists>bs. length bs = length (a # xs) \<and> A = set (filter_bool_list bs (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<subseteq> set []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> set []

goal (1 subgoal):
 1. \<exists>bs. length bs = length [] \<and> A = set (filter_bool_list bs [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>bs. length bs = length [] \<and> A = set (filter_bool_list bs [])

goal (1 subgoal):
 1. \<And>a xs A. \<lbrakk>\<And>A. A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> A = set (filter_bool_list bs xs); A \<subseteq> set (a # xs)\<rbrakk> \<Longrightarrow> \<exists>bs. length bs = length (a # xs) \<and> A = set (filter_bool_list bs (a # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs A. \<lbrakk>\<And>A. A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> A = set (filter_bool_list bs xs); A \<subseteq> set (a # xs)\<rbrakk> \<Longrightarrow> \<exists>bs. length bs = length (a # xs) \<and> A = set (filter_bool_list bs (a # xs))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
?A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> ?A = set (filter_bool_list bs xs)
A \<subseteq> set (x # xs)

goal (1 subgoal):
 1. \<And>a xs A. \<lbrakk>\<And>A. A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> A = set (filter_bool_list bs xs); A \<subseteq> set (a # xs)\<rbrakk> \<Longrightarrow> \<exists>bs. length bs = length (a # xs) \<and> A = set (filter_bool_list bs (a # xs))
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
?A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> ?A = set (filter_bool_list bs xs)
A \<subseteq> set (x # xs)
[PROOF STEP]
have "A - {x} \<subseteq> set xs"
[PROOF STATE]
proof (prove)
using this:
?A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> ?A = set (filter_bool_list bs xs)
A \<subseteq> set (x # xs)

goal (1 subgoal):
 1. A - {x} \<subseteq> set xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A - {x} \<subseteq> set xs

goal (1 subgoal):
 1. \<And>a xs A. \<lbrakk>\<And>A. A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> A = set (filter_bool_list bs xs); A \<subseteq> set (a # xs)\<rbrakk> \<Longrightarrow> \<exists>bs. length bs = length (a # xs) \<and> A = set (filter_bool_list bs (a # xs))
[PROOF STEP]
from this Cons
[PROOF STATE]
proof (chain)
picking this:
A - {x} \<subseteq> set xs
?A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> ?A = set (filter_bool_list bs xs)
A \<subseteq> set (x # xs)
[PROOF STEP]
have 1: "\<exists>bs. length bs = length xs \<and> A - {x} = set (filter_bool_list bs xs)"
[PROOF STATE]
proof (prove)
using this:
A - {x} \<subseteq> set xs
?A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> ?A = set (filter_bool_list bs xs)
A \<subseteq> set (x # xs)

goal (1 subgoal):
 1. \<exists>bs. length bs = length xs \<and> A - {x} = set (filter_bool_list bs xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>bs. length bs = length xs \<and> A - {x} = set (filter_bool_list bs xs)

goal (1 subgoal):
 1. \<And>a xs A. \<lbrakk>\<And>A. A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> A = set (filter_bool_list bs xs); A \<subseteq> set (a # xs)\<rbrakk> \<Longrightarrow> \<exists>bs. length bs = length (a # xs) \<and> A = set (filter_bool_list bs (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>bs. length bs = length xs \<and> A - {x} = set (filter_bool_list bs xs)
[PROOF STEP]
have "\<exists>bs. length bs = length (x # xs) \<and> A = set (filter_bool_list bs (x # xs))"
[PROOF STATE]
proof (prove)
using this:
\<exists>bs. length bs = length xs \<and> A - {x} = set (filter_bool_list bs xs)

goal (1 subgoal):
 1. \<exists>bs. length bs = length (x # xs) \<and> A = set (filter_bool_list bs (x # xs))
[PROOF STEP]
by (metis Diff_empty Diff_insert0 insert_Diff_single insert_absorb list.simps(15) list.size(4) filter_bool_list.simps(3))
[PROOF STATE]
proof (state)
this:
\<exists>bs. length bs = length (x # xs) \<and> A = set (filter_bool_list bs (x # xs))

goal (1 subgoal):
 1. \<And>a xs A. \<lbrakk>\<And>A. A \<subseteq> set xs \<Longrightarrow> \<exists>bs. length bs = length xs \<and> A = set (filter_bool_list bs xs); A \<subseteq> set (a # xs)\<rbrakk> \<Longrightarrow> \<exists>bs. length bs = length (a # xs) \<and> A = set (filter_bool_list bs (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>bs. length bs = length (x # xs) \<and> A = set (filter_bool_list bs (x # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>bs. length bs = length (x # xs) \<and> A = set (filter_bool_list bs (x # xs))

goal (1 subgoal):
 1. \<exists>bs. length bs = length (x # xs) \<and> A = set (filter_bool_list bs (x # xs))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>bs. length bs = length (x # xs) \<and> A = set (filter_bool_list bs (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma filter_bool_list_card:
  "\<lbrakk>distinct xs; length xs = length bs\<rbrakk> \<Longrightarrow> card (set (filter_bool_list bs xs)) = count_list bs True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; length xs = length bs\<rbrakk> \<Longrightarrow> card (set (filter_bool_list bs xs)) = count_list bs True
[PROOF STEP]
by(induct bs xs rule: filter_bool_list.induct) (auto simp: filter_bool_list_not_elem)


[STATEMENT]
lemma filter_bool_list_exist_length_card_True: "\<lbrakk>distinct xs; A \<subseteq> set xs; n = card A\<rbrakk>
   \<Longrightarrow> \<exists>bs. length bs = length xs \<and> count_list bs True = card A \<and> A = set (filter_bool_list bs xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; A \<subseteq> set xs; n = card A\<rbrakk> \<Longrightarrow> \<exists>bs. length bs = length xs \<and> count_list bs True = card A \<and> A = set (filter_bool_list bs xs)
[PROOF STEP]
by (metis filter_bool_list_card filter_bool_list_exist_length)


[STATEMENT]
lemma filter_bool_list_distinct: "distinct xs \<Longrightarrow> distinct (filter_bool_list bs xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> distinct (filter_bool_list bs xs)
[PROOF STEP]
by(induct bs xs rule: filter_bool_list.induct) (auto simp: filter_bool_list_not_elem)


[STATEMENT]
lemma filter_bool_list_inj_aux:
  assumes "length bs1 = length xs"
  and "length xs = length bs2"
  and "distinct xs"
shows "filter_bool_list bs1 xs = filter_bool_list bs2 xs \<Longrightarrow> bs1 = bs2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_bool_list bs1 xs = filter_bool_list bs2 xs \<Longrightarrow> bs1 = bs2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length bs1 = length xs
length xs = length bs2
distinct xs

goal (1 subgoal):
 1. filter_bool_list bs1 xs = filter_bool_list bs2 xs \<Longrightarrow> bs1 = bs2
[PROOF STEP]
proof(induct rule: list_induct3)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>filter_bool_list [] [] = filter_bool_list [] []; distinct []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys z zs. \<lbrakk>length xs = length ys; length ys = length zs; \<lbrakk>filter_bool_list xs ys = filter_bool_list zs ys; distinct ys\<rbrakk> \<Longrightarrow> xs = zs; filter_bool_list (x # xs) (y # ys) = filter_bool_list (z # zs) (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> x # xs = z # zs
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
filter_bool_list [] [] = filter_bool_list [] []
distinct []

goal (2 subgoals):
 1. \<lbrakk>filter_bool_list [] [] = filter_bool_list [] []; distinct []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys z zs. \<lbrakk>length xs = length ys; length ys = length zs; \<lbrakk>filter_bool_list xs ys = filter_bool_list zs ys; distinct ys\<rbrakk> \<Longrightarrow> xs = zs; filter_bool_list (x # xs) (y # ys) = filter_bool_list (z # zs) (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> x # xs = z # zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
filter_bool_list [] [] = filter_bool_list [] []
distinct []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
filter_bool_list [] [] = filter_bool_list [] []
distinct []

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

goal (1 subgoal):
 1. \<And>x xs y ys z zs. \<lbrakk>length xs = length ys; length ys = length zs; \<lbrakk>filter_bool_list xs ys = filter_bool_list zs ys; distinct ys\<rbrakk> \<Longrightarrow> xs = zs; filter_bool_list (x # xs) (y # ys) = filter_bool_list (z # zs) (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> x # xs = z # zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys z zs. \<lbrakk>length xs = length ys; length ys = length zs; \<lbrakk>filter_bool_list xs ys = filter_bool_list zs ys; distinct ys\<rbrakk> \<Longrightarrow> xs = zs; filter_bool_list (x # xs) (y # ys) = filter_bool_list (z # zs) (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> x # xs = z # zs
[PROOF STEP]
case (Cons b1 bs1 x xs b2 bs2)
[PROOF STATE]
proof (state)
this:
length bs1 = length xs
length xs = length bs2
\<lbrakk>filter_bool_list bs1 xs = filter_bool_list bs2 xs; distinct xs\<rbrakk> \<Longrightarrow> bs1 = bs2
filter_bool_list (b1 # bs1) (x # xs) = filter_bool_list (b2 # bs2) (x # xs)
distinct (x # xs)

goal (1 subgoal):
 1. \<And>x xs y ys z zs. \<lbrakk>length xs = length ys; length ys = length zs; \<lbrakk>filter_bool_list xs ys = filter_bool_list zs ys; distinct ys\<rbrakk> \<Longrightarrow> xs = zs; filter_bool_list (x # xs) (y # ys) = filter_bool_list (z # zs) (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> x # xs = z # zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length bs1 = length xs
length xs = length bs2
\<lbrakk>filter_bool_list bs1 xs = filter_bool_list bs2 xs; distinct xs\<rbrakk> \<Longrightarrow> bs1 = bs2
filter_bool_list (b1 # bs1) (x # xs) = filter_bool_list (b2 # bs2) (x # xs)
distinct (x # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length bs1 = length xs
length xs = length bs2
\<lbrakk>filter_bool_list bs1 xs = filter_bool_list bs2 xs; distinct xs\<rbrakk> \<Longrightarrow> bs1 = bs2
filter_bool_list (b1 # bs1) (x # xs) = filter_bool_list (b2 # bs2) (x # xs)
distinct (x # xs)

goal (1 subgoal):
 1. b1 # bs1 = b2 # bs2
[PROOF STEP]
by(cases b1; cases b2, auto) (metis list.set_intros(1) filter_bool_list_not_elem)+
[PROOF STATE]
proof (state)
this:
b1 # bs1 = b2 # bs2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma filter_bool_list_inj:
  "distinct xs \<Longrightarrow> inj_on (\<lambda>bs. filter_bool_list bs xs) {bs. length bs = length xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> inj_on (\<lambda>bs. filter_bool_list bs xs) {bs. length bs = length xs}
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> \<forall>x\<in>{bs. length bs = length xs}. \<forall>y\<in>{bs. length bs = length xs}. filter_bool_list x xs = filter_bool_list y xs \<longrightarrow> x = y
[PROOF STEP]
using filter_bool_list_inj_aux
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?bs1.0 = length ?xs; length ?xs = length ?bs2.0; distinct ?xs; filter_bool_list ?bs1.0 ?xs = filter_bool_list ?bs2.0 ?xs\<rbrakk> \<Longrightarrow> ?bs1.0 = ?bs2.0

goal (1 subgoal):
 1. distinct xs \<Longrightarrow> \<forall>x\<in>{bs. length bs = length xs}. \<forall>y\<in>{bs. length bs = length xs}. filter_bool_list x xs = filter_bool_list y xs \<longrightarrow> x = y
[PROOF STEP]
by fastforce