[STATEMENT]
lemma ltake_lfilter:
  shows "\<exists> n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
proof(induct x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n. ltake (enat 0) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat 0) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. \<And>x. \<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<exists>n. ltake (enat 0) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat 0) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. \<And>x. \<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. ltake (enat 0) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat 0) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
by (metis LNil_eq_ltake_iff ldrop_enat ldropn_0 lfilter_code(1) zero_enat_def)
[PROOF STATE]
proof (state)
this:
\<exists>n. ltake (enat 0) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat 0) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (1 subgoal):
 1. \<And>x. \<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
let ?fP = "lfilter P"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
case (Suc x)
[PROOF STATE]
proof (state)
this:
\<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (1 subgoal):
 1. \<And>x. \<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
obtain n where n:"ltake (enat x) (?fP lst) = ?fP (ltake (enat n) lst)"
    "ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst); ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst)
ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (1 subgoal):
 1. \<And>x. \<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
consider "lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> x < llength (?fP lst)" |
    "lfilter P (ldrop (enat n) lst) = LNil" | "x \<ge> llength (?fP lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> thesis; lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> thesis; llength (lfilter P lst) \<le> enat x \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> ?thesis; lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> ?thesis; llength (lfilter P lst) \<le> enat x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x. \<exists>n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> ?thesis; lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> ?thesis; llength (lfilter P lst) \<le> enat x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> ?thesis; lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> ?thesis; llength (lfilter P lst) \<le> enat x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
hence *:"lfilter P (ldrop (enat n) lst) \<noteq> LNil" "enat x < llength (lfilter P lst)"
[PROOF STATE]
proof (prove)
using this:
lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst)

goal (1 subgoal):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil &&& enat x < llength (lfilter P lst)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lfilter P (ldrop (enat n) lst) \<noteq> LNil
enat x < llength (lfilter P lst)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
from lappend_ltake_ldrop
[PROOF STATE]
proof (chain)
picking this:
lappend (ltake ?n ?xs) (ldrop ?n ?xs) = ?xs
[PROOF STEP]
have "lst = lappend (ltake (enat n) lst) (ldrop (enat n) lst)"
[PROOF STATE]
proof (prove)
using this:
lappend (ltake ?n ?xs) (ldrop ?n ?xs) = ?xs

goal (1 subgoal):
 1. lst = lappend (ltake (enat n) lst) (ldrop (enat n) lst)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lst = lappend (ltake (enat n) lst) (ldrop (enat n) lst)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
from lfilter_hdtl[OF *(1)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>na. LCons (lhd (lfilter P (ldrop (enat n) lst))) LNil = lfilter P (ltake (enat na) (ldrop (enat n) lst)) \<and> ltl (lfilter P (ldrop (enat n) lst)) = lfilter P (ldrop (enat na) (ldrop (enat n) lst))
[PROOF STEP]
obtain delta where
      delta:"LCons (lhd (?fP (ldrop (enat n) lst))) LNil = ?fP (ltake (enat delta) (ldrop (enat n) lst))"
      "ltl (lfilter P (ldrop (enat n) lst)) = lfilter P (ldrop (enat delta) (ldrop (enat n) lst))"
[PROOF STATE]
proof (prove)
using this:
\<exists>na. LCons (lhd (lfilter P (ldrop (enat n) lst))) LNil = lfilter P (ltake (enat na) (ldrop (enat n) lst)) \<and> ltl (lfilter P (ldrop (enat n) lst)) = lfilter P (ldrop (enat na) (ldrop (enat n) lst))

goal (1 subgoal):
 1. (\<And>delta. \<lbrakk>LCons (lhd (lfilter P (ldrop (enat n) lst))) LNil = lfilter P (ltake (enat delta) (ldrop (enat n) lst)); ltl (lfilter P (ldrop (enat n) lst)) = lfilter P (ldrop (enat delta) (ldrop (enat n) lst))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
LCons (lhd (lfilter P (ldrop (enat n) lst))) LNil = lfilter P (ltake (enat delta) (ldrop (enat n) lst))
ltl (lfilter P (ldrop (enat n) lst)) = lfilter P (ldrop (enat delta) (ldrop (enat n) lst))

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
have "ltake (enat (Suc x)) (?fP lst) = lappend (?fP (ltake (enat n) lst)) (LCons (?fP lst $ x) LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltake (enat (Suc x)) (lfilter P lst) = lappend (lfilter P (ltake (enat n) lst)) (LCons (lfilter P lst $ x) LNil)
[PROOF STEP]
using n ltake_Suc_conv_snoc_lnth *
[PROOF STATE]
proof (prove)
using this:
ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst)
ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
enat ?m < llength ?xs \<Longrightarrow> ltake (enat (Suc ?m)) ?xs = lappend (ltake (enat ?m) ?xs) (LCons (?xs $ ?m) LNil)
lfilter P (ldrop (enat n) lst) \<noteq> LNil
enat x < llength (lfilter P lst)

goal (1 subgoal):
 1. ltake (enat (Suc x)) (lfilter P lst) = lappend (lfilter P (ltake (enat n) lst)) (LCons (lfilter P lst $ x) LNil)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
ltake (enat (Suc x)) (lfilter P lst) = lappend (lfilter P (ltake (enat n) lst)) (LCons (lfilter P lst $ x) LNil)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ltake (enat (Suc x)) (lfilter P lst) = lappend (lfilter P (ltake (enat n) lst)) (LCons (lfilter P lst $ x) LNil)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
have "?fP lst $ x = ?fP lst $ (the_enat x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfilter P lst $ x = lfilter P lst $ the_enat (enat x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lfilter P lst $ x = lfilter P lst $ the_enat (enat x)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lfilter P lst $ x = lfilter P lst $ the_enat (enat x)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
have "\<dots> = lhd (ldrop x (?fP lst))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfilter P lst $ the_enat (enat x) = lhd (ldrop (enat x) (lfilter P lst))
[PROOF STEP]
using lhd_ldrop[symmetric] *(2)
[PROOF STATE]
proof (prove)
using this:
?n < llength ?xs \<Longrightarrow> ?xs $ the_enat ?n = lhd (ldrop ?n ?xs)
enat x < llength (lfilter P lst)

goal (1 subgoal):
 1. lfilter P lst $ the_enat (enat x) = lhd (ldrop (enat x) (lfilter P lst))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lfilter P lst $ the_enat (enat x) = lhd (ldrop (enat x) (lfilter P lst))

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lfilter P lst $ the_enat (enat x) = lhd (ldrop (enat x) (lfilter P lst))

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
have "\<dots> = lhd (?fP (ldrop (enat n) lst))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lhd (ldrop (enat x) (lfilter P lst)) = lhd (lfilter P (ldrop (enat n) lst))
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst)
ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (1 subgoal):
 1. lhd (ldrop (enat x) (lfilter P lst)) = lhd (lfilter P (ldrop (enat n) lst))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lhd (ldrop (enat x) (lfilter P lst)) = lhd (lfilter P (ldrop (enat n) lst))

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lhd (ldrop (enat x) (lfilter P lst)) = lhd (lfilter P (ldrop (enat n) lst))

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
note delta(1)
[PROOF STATE]
proof (state)
this:
LCons (lhd (lfilter P (ldrop (enat n) lst))) LNil = lfilter P (ltake (enat delta) (ldrop (enat n) lst))

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ltake (enat (Suc x)) (lfilter P lst) = lappend (lfilter P (ltake (enat n) lst)) (lfilter P (ltake (enat delta) (ldrop (enat n) lst)))
[PROOF STEP]
have take_part:"ltake (enat (Suc x)) (?fP lst) = ?fP (ltake (enat (n + delta)) lst)"
[PROOF STATE]
proof (prove)
using this:
ltake (enat (Suc x)) (lfilter P lst) = lappend (lfilter P (ltake (enat n) lst)) (lfilter P (ltake (enat delta) (ldrop (enat n) lst)))

goal (1 subgoal):
 1. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat (n + delta)) lst)
[PROOF STEP]
using ltake_plus_conv_lappend
[PROOF STATE]
proof (prove)
using this:
ltake (enat (Suc x)) (lfilter P lst) = lappend (lfilter P (ltake (enat n) lst)) (lfilter P (ltake (enat delta) (ldrop (enat n) lst)))
ltake (?n + ?m) ?xs = lappend (ltake ?n ?xs) (ltake ?m (ldrop ?n ?xs))

goal (1 subgoal):
 1. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat (n + delta)) lst)
[PROOF STEP]
by (metis infinite_small_llength lfilter_lappend_lfinite llength_ltake' ltake_all min.strict_order_iff not_less plus_enat_simps(1))
[PROOF STATE]
proof (state)
this:
ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat (n + delta)) lst)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
have "ldrop (enat (Suc x)) (?fP lst) = ltl (ldrop x (?fP lst))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ldrop (enat (Suc x)) (lfilter P lst) = ltl (ldrop (enat x) (lfilter P lst))
[PROOF STEP]
by (simp add: ltl_ldropn ldrop_eSuc_ltl ldrop_enat)
[PROOF STATE]
proof (state)
this:
ldrop (enat (Suc x)) (lfilter P lst) = ltl (ldrop (enat x) (lfilter P lst))

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ldrop (enat (Suc x)) (lfilter P lst) = ltl (ldrop (enat x) (lfilter P lst))

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
have "ldrop x (?fP lst) = ?fP (ldrop (enat n) lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst)
ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (1 subgoal):
 1. ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
note delta(2)
[PROOF STATE]
proof (state)
this:
ltl (lfilter P (ldrop (enat n) lst)) = lfilter P (ldrop (enat delta) (ldrop (enat n) lst))

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ltl (lfilter P (ldrop (enat n) lst)) = lfilter P (ldrop (enat delta) (ldrop (enat n) lst))

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
have "lfilter P (ldrop (enat delta) (ldrop (enat n) lst)) = lfilter P (ldrop (enat delta + enat n) lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfilter P (ldrop (enat delta) (ldrop (enat n) lst)) = lfilter P (ldrop (enat delta + enat n) lst)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lfilter P (ldrop (enat delta) (ldrop (enat n) lst)) = lfilter P (ldrop (enat delta + enat n) lst)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lfilter P (ldrop (enat delta) (ldrop (enat n) lst)) = lfilter P (ldrop (enat delta + enat n) lst)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
have "(enat delta + enat n) = enat (n + delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat delta + enat n = enat (n + delta)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat delta + enat n = enat (n + delta)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat (n + delta)) lst)
[PROOF STEP]
have drop_part:"ldrop (enat (Suc x)) (?fP lst) = ?fP (ldrop (enat (n + delta)) lst)"
[PROOF STATE]
proof (prove)
using this:
ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat (n + delta)) lst)

goal (1 subgoal):
 1. ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat (n + delta)) lst)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat (n + delta)) lst)

goal (3 subgoals):
 1. lfilter P (ldrop (enat n) lst) \<noteq> LNil \<and> enat x < llength (lfilter P lst) \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 3. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
from take_part drop_part
[PROOF STATE]
proof (chain)
picking this:
ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat (n + delta)) lst)
ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat (n + delta)) lst)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat (n + delta)) lst)
ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat (n + delta)) lst)

goal (1 subgoal):
 1. \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (2 subgoals):
 1. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
lfilter P (ldrop (enat n) lst) = LNil

goal (2 subgoals):
 1. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
note * = 2 lappend_ltake_ldrop[of "enat n" lst] Suc_llength infinite_small_llength
             lappend_LNil2 leI lfilter_lappend_lfinite llength_ltake' min.strict_order_iff n
[PROOF STATE]
proof (state)
this:
lfilter P (ldrop (enat n) lst) = LNil
lappend (ltake (enat n) lst) (ldrop (enat n) lst) = lst
enat (Suc ?n) < llength ?xs \<Longrightarrow> enat ?n < llength ?xs
\<not> lfinite ?xs \<Longrightarrow> enat ?n < llength ?xs
lappend ?xs LNil = ?xs
\<not> ?x < ?y \<Longrightarrow> ?y \<le> ?x
lfinite ?xs \<Longrightarrow> lfilter ?P (lappend ?xs ?ys) = lappend (lfilter ?P ?xs) (lfilter ?P ?ys)
enat ?n < llength ?xs \<Longrightarrow> llength (ltake (enat ?n) ?xs) = enat ?n
(?a < ?b) = (?a = min ?a ?b \<and> ?a \<noteq> ?b)
ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst)
ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (2 subgoals):
 1. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
have take_part:"ltake (enat (Suc x)) (?fP lst) = ?fP (ltake (enat n) lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
lfilter P (ldrop (enat n) lst) = LNil
lappend (ltake (enat n) lst) (ldrop (enat n) lst) = lst
enat (Suc ?n) < llength ?xs \<Longrightarrow> enat ?n < llength ?xs
\<not> lfinite ?xs \<Longrightarrow> enat ?n < llength ?xs
lappend ?xs LNil = ?xs
\<not> ?x < ?y \<Longrightarrow> ?y \<le> ?x
lfinite ?xs \<Longrightarrow> lfilter ?P (lappend ?xs ?ys) = lappend (lfilter ?P ?xs) (lfilter ?P ?ys)
enat ?n < llength ?xs \<Longrightarrow> llength (ltake (enat ?n) ?xs) = enat ?n
(?a < ?b) = (?a = min ?a ?b \<and> ?a \<noteq> ?b)
ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst)
ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (1 subgoal):
 1. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst)
[PROOF STEP]
by (smt (z3) ltake_all)
[PROOF STATE]
proof (state)
this:
ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst)

goal (2 subgoals):
 1. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
lfilter P (ldrop (enat n) lst) = LNil
[PROOF STEP]
have drop_part:"ldrop (enat (Suc x)) (?fP lst) = ?fP (ldrop (enat n) lst)"
[PROOF STATE]
proof (prove)
using this:
lfilter P (ldrop (enat n) lst) = LNil

goal (1 subgoal):
 1. ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
lfilter P (ldrop (enat n) lst) = LNil
lfilter P (ldrop (enat n) lst) = LNil
lappend (ltake (enat n) lst) (ldrop (enat n) lst) = lst
enat (Suc ?n) < llength ?xs \<Longrightarrow> enat ?n < llength ?xs
\<not> lfinite ?xs \<Longrightarrow> enat ?n < llength ?xs
lappend ?xs LNil = ?xs
\<not> ?x < ?y \<Longrightarrow> ?y \<le> ?x
lfinite ?xs \<Longrightarrow> lfilter ?P (lappend ?xs ?ys) = lappend (lfilter ?P ?xs) (lfilter ?P ?ys)
enat ?n < llength ?xs \<Longrightarrow> llength (ltake (enat ?n) ?xs) = enat ?n
(?a < ?b) = (?a = min ?a ?b \<and> ?a \<noteq> ?b)
ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst)
ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (1 subgoal):
 1. ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
by (smt (z3) ldrop_all)
[PROOF STATE]
proof (state)
this:
ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (2 subgoals):
 1. lfilter P (ldrop (enat n) lst) = LNil \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
 2. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
from take_part drop_part
[PROOF STATE]
proof (chain)
picking this:
ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst)
ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst)
ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (1 subgoal):
 1. \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal (1 subgoal):
 1. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
llength (lfilter P lst) \<le> enat x

goal (1 subgoal):
 1. llength (lfilter P lst) \<le> enat x \<Longrightarrow> \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
llength (lfilter P lst) \<le> enat x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
llength (lfilter P lst) \<le> enat x

goal (1 subgoal):
 1. \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
using n dual_order.order_iff_strict eSuc_enat iless_Suc_eq le_less_trans ltake_all ldrop_all
[PROOF STATE]
proof (prove)
using this:
llength (lfilter P lst) \<le> enat x
ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst)
ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
(?b \<le> ?a) = (?b < ?a \<or> ?a = ?b)
eSuc (enat ?n) = enat (Suc ?n)
(enat ?m < eSuc ?n) = (enat ?m \<le> ?n)
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z
llength ?xs \<le> ?m \<Longrightarrow> ltake ?m ?xs = ?xs
llength ?xs \<le> ?m \<Longrightarrow> ldrop ?m ?xs = LNil

goal (1 subgoal):
 1. \<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>n. ltake (enat (Suc x)) (lfilter P lst) = lfilter P (ltake (enat n) lst) \<and> ldrop (enat (Suc x)) (lfilter P lst) = lfilter P (ldrop (enat n) lst)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma filter_obtain_two:
  assumes "i < j" "j < length (filter P lst)"
  shows "\<exists> i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! i \<and> lst ! j2 = filter P lst ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! i \<and> lst ! j2 = filter P lst ! j
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < j
j < length (filter P lst)

goal (1 subgoal):
 1. \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! i \<and> lst ! j2 = filter P lst ! j
[PROOF STEP]
proof(induct lst arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < j; j < length (filter P [])\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length [] \<and> [] ! i2 = filter P [] ! i \<and> [] ! j2 = filter P [] ! j
 2. \<And>a lst i j. \<lbrakk>\<And>i j. \<lbrakk>i < j; j < length (filter P lst)\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! i \<and> lst ! j2 = filter P lst ! j; i < j; j < length (filter P (a # lst))\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
case (Cons a lst)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < ?j; ?j < length (filter P lst)\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! ?i \<and> lst ! j2 = filter P lst ! ?j
i < j
j < length (filter P (a # lst))

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < j; j < length (filter P [])\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length [] \<and> [] ! i2 = filter P [] ! i \<and> [] ! j2 = filter P [] ! j
 2. \<And>a lst i j. \<lbrakk>\<And>i j. \<lbrakk>i < j; j < length (filter P lst)\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! i \<and> lst ! j2 = filter P lst ! j; i < j; j < length (filter P (a # lst))\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i < ?j; ?j < length (filter P lst)\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! ?i \<and> lst ! j2 = filter P lst ! ?j
i < j
j < length (filter P (a # lst))
[PROOF STEP]
obtain jprev where jprev:"j = Suc jprev"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i < ?j; ?j < length (filter P lst)\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! ?i \<and> lst ! j2 = filter P lst ! ?j
i < j
j < length (filter P (a # lst))

goal (1 subgoal):
 1. (\<And>jprev. j = Suc jprev \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lessE
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i < ?j; ?j < length (filter P lst)\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! ?i \<and> lst ! j2 = filter P lst ! ?j
i < j
j < length (filter P (a # lst))
\<lbrakk>?i < ?k; ?k = Suc ?i \<Longrightarrow> ?P; \<And>j. \<lbrakk>?i < j; ?k = Suc j\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>jprev. j = Suc jprev \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
j = Suc jprev

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < j; j < length (filter P [])\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length [] \<and> [] ! i2 = filter P [] ! i \<and> [] ! j2 = filter P [] ! j
 2. \<And>a lst i j. \<lbrakk>\<And>i j. \<lbrakk>i < j; j < length (filter P lst)\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! i \<and> lst ! j2 = filter P lst ! j; i < j; j < length (filter P (a # lst))\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
proof(cases "P a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
 2. \<not> P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
P a

goal (2 subgoals):
 1. P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
 2. \<not> P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
hence lnth[simp]:"length (filter P (a # lst)) = Suc (length (filter P lst))"
[PROOF STATE]
proof (prove)
using this:
P a

goal (1 subgoal):
 1. length (filter P (a # lst)) = Suc (length (filter P lst))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (filter P (a # lst)) = Suc (length (filter P lst))

goal (2 subgoals):
 1. P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
 2. \<not> P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
proof(cases i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
i = 0

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
from jprev True Cons(3)
[PROOF STATE]
proof (chain)
picking this:
j = Suc jprev
P a
j < length (filter P (a # lst))
[PROOF STEP]
have "jprev < length (filter P lst) "
[PROOF STATE]
proof (prove)
using this:
j = Suc jprev
P a
j < length (filter P (a # lst))

goal (1 subgoal):
 1. jprev < length (filter P lst)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
jprev < length (filter P lst)

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
from nth_mem[OF this]
[PROOF STATE]
proof (chain)
picking this:
filter P lst ! jprev \<in> set (filter P lst)
[PROOF STEP]
have "filter P lst ! jprev \<in> set lst"
[PROOF STATE]
proof (prove)
using this:
filter P lst ! jprev \<in> set (filter P lst)

goal (1 subgoal):
 1. filter P lst ! jprev \<in> set lst
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
filter P lst ! jprev \<in> set lst

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
from this[unfolded in_set_conv_nth]
[PROOF STATE]
proof (chain)
picking this:
\<exists>i<length lst. lst ! i = filter P lst ! jprev
[PROOF STEP]
obtain j2 where
        "j2<length lst" "lst ! j2 = filter P lst ! jprev"
[PROOF STATE]
proof (prove)
using this:
\<exists>i<length lst. lst ! i = filter P lst ! jprev

goal (1 subgoal):
 1. (\<And>j2. \<lbrakk>j2 < length lst; lst ! j2 = filter P lst ! jprev\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j2 < length lst
lst ! j2 = filter P lst ! jprev

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
hence "0 < Suc j2" "Suc j2 < length (a # lst)"
        "(a # lst) ! 0 = filter P (a # lst) ! i"
        "(a # lst) ! Suc j2 = filter P (a # lst) ! j"
[PROOF STATE]
proof (prove)
using this:
j2 < length lst
lst ! j2 = filter P lst ! jprev

goal (1 subgoal):
 1. (0 < Suc j2 &&& Suc j2 < length (a # lst)) &&& (a # lst) ! 0 = filter P (a # lst) ! i &&& (a # lst) ! Suc j2 = filter P (a # lst) ! j
[PROOF STEP]
using 0 True jprev
[PROOF STATE]
proof (prove)
using this:
j2 < length lst
lst ! j2 = filter P lst ! jprev
i = 0
P a
j = Suc jprev

goal (1 subgoal):
 1. (0 < Suc j2 &&& Suc j2 < length (a # lst)) &&& (a # lst) ! 0 = filter P (a # lst) ! i &&& (a # lst) ! Suc j2 = filter P (a # lst) ! j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < Suc j2
Suc j2 < length (a # lst)
(a # lst) ! 0 = filter P (a # lst) ! i
(a # lst) ! Suc j2 = filter P (a # lst) ! j

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < Suc j2
Suc j2 < length (a # lst)
(a # lst) ! 0 = filter P (a # lst) ! i
(a # lst) ! Suc j2 = filter P (a # lst) ! j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < Suc j2
Suc j2 < length (a # lst)
(a # lst) ! 0 = filter P (a # lst) ! i
(a # lst) ! Suc j2 = filter P (a # lst) ! j

goal (1 subgoal):
 1. \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
case (Suc nat)
[PROOF STATE]
proof (state)
this:
i = Suc nat

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = Suc nat
[PROOF STEP]
obtain jprev where jprev:"j = Suc jprev"
[PROOF STATE]
proof (prove)
using this:
i = Suc nat

goal (1 subgoal):
 1. (\<And>jprev. j = Suc jprev \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Cons lessE
[PROOF STATE]
proof (prove)
using this:
i = Suc nat
\<lbrakk>?i < ?j; ?j < length (filter P lst)\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! ?i \<and> lst ! j2 = filter P lst ! ?j
i < j
j < length (filter P (a # lst))
\<lbrakk>?i < ?k; ?k = Suc ?i \<Longrightarrow> ?P; \<And>j. \<lbrakk>?i < j; ?k = Suc j\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>jprev. j = Suc jprev \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
j = Suc jprev

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
hence "nat < jprev" "jprev < length (filter P lst)"
[PROOF STATE]
proof (prove)
using this:
j = Suc jprev

goal (1 subgoal):
 1. nat < jprev &&& jprev < length (filter P lst)
[PROOF STEP]
using Cons Suc lnth
[PROOF STATE]
proof (prove)
using this:
j = Suc jprev
\<lbrakk>?i < ?j; ?j < length (filter P lst)\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! ?i \<and> lst ! j2 = filter P lst ! ?j
i < j
j < length (filter P (a # lst))
i = Suc nat
length (filter P (a # lst)) = Suc (length (filter P lst))

goal (1 subgoal):
 1. nat < jprev &&& jprev < length (filter P lst)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat < jprev
jprev < length (filter P lst)

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
from Cons(1)[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! nat \<and> lst ! j2 = filter P lst ! jprev
[PROOF STEP]
obtain i2 j2 where "i2 < j2" "j2 < length lst"
        "lst ! i2 = filter P lst ! nat" "lst ! j2 = filter P lst ! jprev"
[PROOF STATE]
proof (prove)
using this:
\<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! nat \<and> lst ! j2 = filter P lst ! jprev

goal (1 subgoal):
 1. (\<And>i2 j2. \<lbrakk>i2 < j2; j2 < length lst; lst ! i2 = filter P lst ! nat; lst ! j2 = filter P lst ! jprev\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i2 < j2
j2 < length lst
lst ! i2 = filter P lst ! nat
lst ! j2 = filter P lst ! jprev

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
hence "Suc i2 < Suc j2" "Suc j2 < length (a # lst)"
        "(a # lst) ! Suc i2 = filter P (a # lst) ! Suc nat"
        "(a # lst) ! Suc j2 = filter P (a # lst) ! Suc jprev"
[PROOF STATE]
proof (prove)
using this:
i2 < j2
j2 < length lst
lst ! i2 = filter P lst ! nat
lst ! j2 = filter P lst ! jprev

goal (1 subgoal):
 1. (Suc i2 < Suc j2 &&& Suc j2 < length (a # lst)) &&& (a # lst) ! Suc i2 = filter P (a # lst) ! Suc nat &&& (a # lst) ! Suc j2 = filter P (a # lst) ! Suc jprev
[PROOF STEP]
using lnth
[PROOF STATE]
proof (prove)
using this:
i2 < j2
j2 < length lst
lst ! i2 = filter P lst ! nat
lst ! j2 = filter P lst ! jprev
length (filter P (a # lst)) = Suc (length (filter P lst))

goal (1 subgoal):
 1. (Suc i2 < Suc j2 &&& Suc j2 < length (a # lst)) &&& (a # lst) ! Suc i2 = filter P (a # lst) ! Suc nat &&& (a # lst) ! Suc j2 = filter P (a # lst) ! Suc jprev
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i2 < Suc j2
Suc j2 < length (a # lst)
(a # lst) ! Suc i2 = filter P (a # lst) ! Suc nat
(a # lst) ! Suc j2 = filter P (a # lst) ! Suc jprev

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc i2 < Suc j2
Suc j2 < length (a # lst)
(a # lst) ! Suc i2 = filter P (a # lst) ! Suc nat
(a # lst) ! Suc j2 = filter P (a # lst) ! Suc jprev
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc i2 < Suc j2
Suc j2 < length (a # lst)
(a # lst) ! Suc i2 = filter P (a # lst) ! Suc nat
(a # lst) ! Suc j2 = filter P (a # lst) ! Suc jprev

goal (1 subgoal):
 1. \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
unfolding jprev[symmetric] Suc[symmetric]
[PROOF STATE]
proof (prove)
using this:
Suc i2 < Suc j2
Suc j2 < length (a # lst)
(a # lst) ! Suc i2 = filter P (a # lst) ! i
(a # lst) ! Suc j2 = filter P (a # lst) ! j

goal (1 subgoal):
 1. \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j

goal (1 subgoal):
 1. \<not> P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> P a

goal (1 subgoal):
 1. \<not> P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
hence [simp]: "filter P (a # lst) = filter P lst"
[PROOF STATE]
proof (prove)
using this:
\<not> P a

goal (1 subgoal):
 1. filter P (a # lst) = filter P lst
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
filter P (a # lst) = filter P lst

goal (1 subgoal):
 1. \<not> P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
from Cons(1)[OF Cons(2)] Cons(3)[unfolded this]
[PROOF STATE]
proof (chain)
picking this:
j < length (filter P lst) \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! i \<and> lst ! j2 = filter P lst ! j
j < length (filter P lst)
[PROOF STEP]
obtain i2 j2 where "i2 < j2" "j2 < length lst"
      "lst ! i2 = filter P lst ! i" "lst ! j2 = filter P lst ! j"
[PROOF STATE]
proof (prove)
using this:
j < length (filter P lst) \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length lst \<and> lst ! i2 = filter P lst ! i \<and> lst ! j2 = filter P lst ! j
j < length (filter P lst)

goal (1 subgoal):
 1. (\<And>i2 j2. \<lbrakk>i2 < j2; j2 < length lst; lst ! i2 = filter P lst ! i; lst ! j2 = filter P lst ! j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i2 < j2
j2 < length lst
lst ! i2 = filter P lst ! i
lst ! j2 = filter P lst ! j

goal (1 subgoal):
 1. \<not> P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
hence "Suc i2 < Suc j2" "Suc j2 < length (a # lst)"
      "(a # lst) ! Suc i2 = filter P (a # lst) ! i"
      "(a # lst) ! Suc j2 = filter P (a # lst) ! j"
[PROOF STATE]
proof (prove)
using this:
i2 < j2
j2 < length lst
lst ! i2 = filter P lst ! i
lst ! j2 = filter P lst ! j

goal (1 subgoal):
 1. (Suc i2 < Suc j2 &&& Suc j2 < length (a # lst)) &&& (a # lst) ! Suc i2 = filter P (a # lst) ! i &&& (a # lst) ! Suc j2 = filter P (a # lst) ! j
[PROOF STEP]
by (auto simp:False)
[PROOF STATE]
proof (state)
this:
Suc i2 < Suc j2
Suc j2 < length (a # lst)
(a # lst) ! Suc i2 = filter P (a # lst) ! i
(a # lst) ! Suc j2 = filter P (a # lst) ! j

goal (1 subgoal):
 1. \<not> P a \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc i2 < Suc j2
Suc j2 < length (a # lst)
(a # lst) ! Suc i2 = filter P (a # lst) ! i
(a # lst) ! Suc j2 = filter P (a # lst) ! j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc i2 < Suc j2
Suc j2 < length (a # lst)
(a # lst) ! Suc i2 = filter P (a # lst) ! i
(a # lst) ! Suc j2 = filter P (a # lst) ! j

goal (1 subgoal):
 1. \<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i2 j2. i2 < j2 \<and> j2 < length (a # lst) \<and> (a # lst) ! i2 = filter P (a # lst) ! i \<and> (a # lst) ! j2 = filter P (a # lst) ! j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < j; j < length (filter P [])\<rbrakk> \<Longrightarrow> \<exists>i2 j2. i2 < j2 \<and> j2 < length [] \<and> [] ! i2 = filter P [] ! i \<and> [] ! j2 = filter P [] ! j
[PROOF STEP]
qed auto


[STATEMENT]
lemma ldistinct_lfilterI:
  assumes "\<And> i j. i < llength lst \<Longrightarrow> j < llength lst \<Longrightarrow> lst $ i = lst $ j \<Longrightarrow> P (lst $ i) \<Longrightarrow> i = j"
  shows "ldistinct (lfilter P lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
assume *: "enat i < llength (lfilter P lst)"
            "enat j < llength (lfilter P lst)"
            "lfilter P lst $ i = lfilter P lst $ j"
            "i < j"
[PROOF STATE]
proof (state)
this:
enat i < llength (lfilter P lst)
enat j < llength (lfilter P lst)
lfilter P lst $ i = lfilter P lst $ j
i < j

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
hence "lfilter P lst $ i \<in> lset (lfilter P lst)"
[PROOF STATE]
proof (prove)
using this:
enat i < llength (lfilter P lst)
enat j < llength (lfilter P lst)
lfilter P lst $ i = lfilter P lst $ j
i < j

goal (1 subgoal):
 1. lfilter P lst $ i \<in> lset (lfilter P lst)
[PROOF STEP]
unfolding in_lset_conv_lnth
[PROOF STATE]
proof (prove)
using this:
enat i < llength (lfilter P lst)
enat j < llength (lfilter P lst)
lfilter P lst $ i = lfilter P lst $ j
i < j

goal (1 subgoal):
 1. \<exists>n. enat n < llength (lfilter P lst) \<and> lfilter P lst $ n = lfilter P lst $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lfilter P lst $ i \<in> lset (lfilter P lst)

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
with lset_lfilter
[PROOF STATE]
proof (chain)
picking this:
lset (lfilter ?P ?xs) = {x \<in> lset ?xs. ?P x}
lfilter P lst $ i \<in> lset (lfilter P lst)
[PROOF STEP]
have P:"P (lfilter P lst $ i)"
[PROOF STATE]
proof (prove)
using this:
lset (lfilter ?P ?xs) = {x \<in> lset ?xs. ?P x}
lfilter P lst $ i \<in> lset (lfilter P lst)

goal (1 subgoal):
 1. P (lfilter P lst $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P (lfilter P lst $ i)

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
let ?maxij = "Suc (max i j)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
from ltake_lfilter
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. ltake (enat ?x) (lfilter ?P ?lst) = lfilter ?P (ltake (enat n) ?lst) \<and> ldrop (enat ?x) (lfilter ?P ?lst) = lfilter ?P (ldrop (enat n) ?lst)
[PROOF STEP]
obtain maxij where
    maxij:"ltake ?maxij (lfilter P lst) = lfilter P (ltake (enat maxij) lst)"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. ltake (enat ?x) (lfilter ?P ?lst) = lfilter ?P (ltake (enat n) ?lst) \<and> ldrop (enat ?x) (lfilter ?P ?lst) = lfilter ?P (ldrop (enat n) ?lst)

goal (1 subgoal):
 1. (\<And>maxij. ltake (enat (Suc (max i j))) (lfilter P lst) = lfilter P (ltake (enat maxij) lst) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ltake (enat (Suc (max i j))) (lfilter P lst) = lfilter P (ltake (enat maxij) lst)

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
let ?lst = "ltake (enat maxij) lst"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
have "lfinite ?lst"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite (ltake (enat maxij) lst)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lfinite (ltake (enat maxij) lst)

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
define flst where "flst = list_of ?lst"
[PROOF STATE]
proof (state)
this:
flst = list_of (ltake (enat maxij) lst)

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
hence flst:"llist_of flst = ?lst"
[PROOF STATE]
proof (prove)
using this:
flst = list_of (ltake (enat maxij) lst)

goal (1 subgoal):
 1. llist_of flst = ltake (enat maxij) lst
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
llist_of flst = ltake (enat maxij) lst

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
let ?flst = "llist_of flst"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
from * P
[PROOF STATE]
proof (chain)
picking this:
enat i < llength (lfilter P lst)
enat j < llength (lfilter P lst)
lfilter P lst $ i = lfilter P lst $ j
i < j
P (lfilter P lst $ i)
[PROOF STEP]
have "enat i < llength (lfilter P ?flst)"
         "enat j < llength (lfilter P ?flst)"
         "lfilter P ?flst $ i = lfilter P ?flst $ j"
    and P2:"P (lfilter P ?lst $ i)"
[PROOF STATE]
proof (prove)
using this:
enat i < llength (lfilter P lst)
enat j < llength (lfilter P lst)
lfilter P lst $ i = lfilter P lst $ j
i < j
P (lfilter P lst $ i)

goal (1 subgoal):
 1. (enat i < llength (lfilter P (llist_of flst)) &&& enat j < llength (lfilter P (llist_of flst)) &&& lfilter P (llist_of flst) $ i = lfilter P (llist_of flst) $ j) &&& P (lfilter P (ltake (enat maxij) lst) $ i)
[PROOF STEP]
unfolding maxij[symmetric] flst
[PROOF STATE]
proof (prove)
using this:
enat i < llength (lfilter P lst)
enat j < llength (lfilter P lst)
lfilter P lst $ i = lfilter P lst $ j
i < j
P (lfilter P lst $ i)

goal (1 subgoal):
 1. (enat i < llength (ltake (enat (Suc (max i j))) (lfilter P lst)) &&& enat j < llength (ltake (enat (Suc (max i j))) (lfilter P lst)) &&& ltake (enat (Suc (max i j))) (lfilter P lst) $ i = ltake (enat (Suc (max i j))) (lfilter P lst) $ j) &&& P (ltake (enat (Suc (max i j))) (lfilter P lst) $ i)
[PROOF STEP]
by (auto simp add: lnth_ltake)
[PROOF STATE]
proof (state)
this:
enat i < llength (lfilter P (llist_of flst))
enat j < llength (lfilter P (llist_of flst))
lfilter P (llist_of flst) $ i = lfilter P (llist_of flst) $ j
P (lfilter P (ltake (enat maxij) lst) $ i)

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
hence "i < length (filter P flst)"
        "j < length (filter P flst)"
    and eq_ij: "filter P flst ! i = filter P flst ! j"
[PROOF STATE]
proof (prove)
using this:
enat i < llength (lfilter P (llist_of flst))
enat j < llength (lfilter P (llist_of flst))
lfilter P (llist_of flst) $ i = lfilter P (llist_of flst) $ j
P (lfilter P (ltake (enat maxij) lst) $ i)

goal (1 subgoal):
 1. (i < length (filter P flst) &&& j < length (filter P flst)) &&& filter P flst ! i = filter P flst ! j
[PROOF STEP]
unfolding llength_llist_of lfilter_llist_of lnth_llist_of
[PROOF STATE]
proof (prove)
using this:
enat i < enat (length (filter P flst))
enat j < enat (length (filter P flst))
filter P flst ! i = filter P flst ! j
P (lfilter P (ltake (enat maxij) lst) $ i)

goal (1 subgoal):
 1. (i < length (filter P flst) &&& j < length (filter P flst)) &&& filter P flst ! i = filter P flst ! j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (filter P flst)
j < length (filter P flst)
filter P flst ! i = filter P flst ! j

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
with filter_obtain_two[OF *(4) this(2)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>i2 j2. i2 < j2 \<and> j2 < length flst \<and> flst ! i2 = filter P flst ! i \<and> flst ! j2 = filter P flst ! j
i < length (filter P flst)
j < length (filter P flst)
filter P flst ! i = filter P flst ! j
[PROOF STEP]
obtain i2 j2
    where "i2 < length flst" "j2 < length flst"
          "flst ! i2 = filter P flst ! i"
          "flst ! j2 = filter P flst ! j"
          and ineq:"i2<j2"
[PROOF STATE]
proof (prove)
using this:
\<exists>i2 j2. i2 < j2 \<and> j2 < length flst \<and> flst ! i2 = filter P flst ! i \<and> flst ! j2 = filter P flst ! j
i < length (filter P flst)
j < length (filter P flst)
filter P flst ! i = filter P flst ! j

goal (1 subgoal):
 1. (\<And>i2 j2. \<lbrakk>i2 < length flst; j2 < length flst; flst ! i2 = filter P flst ! i; flst ! j2 = filter P flst ! j; i2 < j2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i2 < length flst
j2 < length flst
flst ! i2 = filter P flst ! i
flst ! j2 = filter P flst ! j
i2 < j2

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
hence "i2 < llength ?flst" "j2 < llength ?flst" "?flst $ i2 = ?flst $ j2" "?flst $ i2 = lfilter P ?flst $ i" "i2<j2"
[PROOF STATE]
proof (prove)
using this:
i2 < length flst
j2 < length flst
flst ! i2 = filter P flst ! i
flst ! j2 = filter P flst ! j
i2 < j2

goal (1 subgoal):
 1. (enat i2 < llength (llist_of flst) &&& enat j2 < llength (llist_of flst)) &&& llist_of flst $ i2 = llist_of flst $ j2 &&& llist_of flst $ i2 = lfilter P (llist_of flst) $ i &&& i2 < j2
[PROOF STEP]
unfolding llength_llist_of lfilter_llist_of lnth_llist_of eq_ij
[PROOF STATE]
proof (prove)
using this:
i2 < length flst
j2 < length flst
flst ! i2 = filter P flst ! j
flst ! j2 = filter P flst ! j
i2 < j2

goal (1 subgoal):
 1. (enat i2 < enat (length flst) &&& enat j2 < enat (length flst)) &&& flst ! i2 = flst ! j2 &&& flst ! i2 = filter P flst ! j &&& i2 < j2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enat i2 < llength (llist_of flst)
enat j2 < llength (llist_of flst)
llist_of flst $ i2 = llist_of flst $ j2
llist_of flst $ i2 = lfilter P (llist_of flst) $ i
i2 < j2

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
hence "enat i2 < llength lst" "enat j2 < llength lst" "lst $ i2 = lst $ j2" "P (lst $ i2)"
[PROOF STATE]
proof (prove)
using this:
enat i2 < llength (llist_of flst)
enat j2 < llength (llist_of flst)
llist_of flst $ i2 = llist_of flst $ j2
llist_of flst $ i2 = lfilter P (llist_of flst) $ i
i2 < j2

goal (1 subgoal):
 1. (enat i2 < llength lst &&& enat j2 < llength lst) &&& lst $ i2 = lst $ j2 &&& P (lst $ i2)
[PROOF STEP]
using P2
[PROOF STATE]
proof (prove)
using this:
enat i2 < llength (llist_of flst)
enat j2 < llength (llist_of flst)
llist_of flst $ i2 = llist_of flst $ j2
llist_of flst $ i2 = lfilter P (llist_of flst) $ i
i2 < j2
P (lfilter P (ltake (enat maxij) lst) $ i)

goal (1 subgoal):
 1. (enat i2 < llength lst &&& enat j2 < llength lst) &&& lst $ i2 = lst $ j2 &&& P (lst $ i2)
[PROOF STEP]
unfolding flst
[PROOF STATE]
proof (prove)
using this:
enat i2 < llength (ltake (enat maxij) lst)
enat j2 < llength (ltake (enat maxij) lst)
ltake (enat maxij) lst $ i2 = ltake (enat maxij) lst $ j2
ltake (enat maxij) lst $ i2 = lfilter P (ltake (enat maxij) lst) $ i
i2 < j2
P (lfilter P (ltake (enat maxij) lst) $ i)

goal (1 subgoal):
 1. (enat i2 < llength lst &&& enat j2 < llength lst) &&& lst $ i2 = lst $ j2 &&& P (lst $ i2)
[PROOF STEP]
by (auto simp add: lnth_ltake)
[PROOF STATE]
proof (state)
this:
enat i2 < llength lst
enat j2 < llength lst
lst $ i2 = lst $ j2
P (lst $ i2)

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
from assms[OF this]
[PROOF STATE]
proof (chain)
picking this:
i2 = j2
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
i2 = j2

goal (1 subgoal):
 1. False
[PROOF STEP]
using ineq
[PROOF STATE]
proof (prove)
using this:
i2 = j2
i2 < j2

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

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>enat ?i2 < llength (lfilter P lst); enat ?j2 < llength (lfilter P lst); lfilter P lst $ ?i2 = lfilter P lst $ ?j2; ?i2 < ?j2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>enat ?i2 < llength (lfilter P lst); enat ?j2 < llength (lfilter P lst); lfilter P lst $ ?i2 = lfilter P lst $ ?j2; ?i2 < ?j2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. ldistinct (lfilter P lst)
[PROOF STEP]
unfolding ldistinct_conv_lnth
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>enat ?i2 < llength (lfilter P lst); enat ?j2 < llength (lfilter P lst); lfilter P lst $ ?i2 = lfilter P lst $ ?j2; ?i2 < ?j2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>i j. enat i < llength (lfilter P lst) \<longrightarrow> enat j < llength (lfilter P lst) \<longrightarrow> i \<noteq> j \<longrightarrow> lfilter P lst $ i \<noteq> lfilter P lst $ j
[PROOF STEP]
by (smt (z3) le_cases3 less_le)
[PROOF STATE]
proof (state)
this:
ldistinct (lfilter P lst)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ldistinct_lfilterE:
  assumes "ldistinct (lfilter P lst)" "e = lst $ i" "e = lst $ j"
          "i < llength lst" "j < llength lst" "P e"
  shows "i = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
let ?maxij = "Suc (max i j)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
let ?lst = "ltake (enat ?maxij) lst"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
have jle:"j < length (list_of (ltake (enat (Suc (max i j))) lst))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length (list_of (ltake (enat (Suc (max i j))) lst))
[PROOF STEP]
using assms(4,5)
[PROOF STATE]
proof (prove)
using this:
enat i < llength lst
enat j < llength lst

goal (1 subgoal):
 1. j < length (list_of (ltake (enat (Suc (max i j))) lst))
[PROOF STEP]
apply(subst length_list_of_conv_the_enat,force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>enat i < llength lst; enat j < llength lst\<rbrakk> \<Longrightarrow> j < the_enat (llength (ltake (enat (Suc (max i j))) lst))
[PROOF STEP]
by(cases "llength lst", auto simp:min_enat2_conv_enat min_enat1_conv_enat)
[PROOF STATE]
proof (state)
this:
j < length (list_of (ltake (enat (Suc (max i j))) lst))

goal (1 subgoal):
 1. i = j
[PROOF STEP]
have ile:"i < length (list_of (ltake (enat (Suc (max i j))) lst))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (list_of (ltake (enat (Suc (max i j))) lst))
[PROOF STEP]
using assms(4,5)
[PROOF STATE]
proof (prove)
using this:
enat i < llength lst
enat j < llength lst

goal (1 subgoal):
 1. i < length (list_of (ltake (enat (Suc (max i j))) lst))
[PROOF STEP]
apply(subst length_list_of_conv_the_enat,force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>enat i < llength lst; enat j < llength lst\<rbrakk> \<Longrightarrow> i < the_enat (llength (ltake (enat (Suc (max i j))) lst))
[PROOF STEP]
by(cases "llength lst", auto simp:min_enat2_conv_enat min_enat1_conv_enat)
[PROOF STATE]
proof (state)
this:
i < length (list_of (ltake (enat (Suc (max i j))) lst))

goal (1 subgoal):
 1. i = j
[PROOF STEP]
have "enat i < ?maxij" "enat j < ?maxij"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat i < enat (Suc (max i j)) &&& enat j < enat (Suc (max i j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enat i < enat (Suc (max i j))
enat j < enat (Suc (max i j))

goal (1 subgoal):
 1. i = j
[PROOF STEP]
from this[THEN lnth_ltake,of lst] assms
[PROOF STATE]
proof (chain)
picking this:
ltake (enat (Suc (max i j))) lst $ i = lst $ i
ltake (enat (Suc (max i j))) lst $ j = lst $ j
ldistinct (lfilter P lst)
e = lst $ i
e = lst $ j
enat i < llength lst
enat j < llength lst
P e
[PROOF STEP]
have "ldistinct (lfilter P ?lst)" "e = ?lst $ i" "e = ?lst $ j"
[PROOF STATE]
proof (prove)
using this:
ltake (enat (Suc (max i j))) lst $ i = lst $ i
ltake (enat (Suc (max i j))) lst $ j = lst $ j
ldistinct (lfilter P lst)
e = lst $ i
e = lst $ j
enat i < llength lst
enat j < llength lst
P e

goal (1 subgoal):
 1. ldistinct (lfilter P (ltake (enat (Suc (max i j))) lst)) &&& e = ltake (enat (Suc (max i j))) lst $ i &&& e = ltake (enat (Suc (max i j))) lst $ j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ldistinct (lfilter P (ltake (enat (Suc (max i j))) lst))
e = ltake (enat (Suc (max i j))) lst $ i
e = ltake (enat (Suc (max i j))) lst $ j

goal (1 subgoal):
 1. i = j
[PROOF STEP]
hence d:"distinct (filter P (list_of ?lst))"
       "(list_of ?lst) ! j = e" "(list_of ?lst) ! i = e"
[PROOF STATE]
proof (prove)
using this:
ldistinct (lfilter P (ltake (enat (Suc (max i j))) lst))
e = ltake (enat (Suc (max i j))) lst $ i
e = ltake (enat (Suc (max i j))) lst $ j

goal (1 subgoal):
 1. distinct (filter P (list_of (ltake (enat (Suc (max i j))) lst))) &&& list_of (ltake (enat (Suc (max i j))) lst) ! j = e &&& list_of (ltake (enat (Suc (max i j))) lst) ! i = e
[PROOF STEP]
using lfilter_llist_of[of P "list_of ?lst"]
[PROOF STATE]
proof (prove)
using this:
ldistinct (lfilter P (ltake (enat (Suc (max i j))) lst))
e = ltake (enat (Suc (max i j))) lst $ i
e = ltake (enat (Suc (max i j))) lst $ j
lfilter P (llist_of (list_of (ltake (enat (Suc (max i j))) lst))) = llist_of (filter P (list_of (ltake (enat (Suc (max i j))) lst)))

goal (1 subgoal):
 1. distinct (filter P (list_of (ltake (enat (Suc (max i j))) lst))) &&& list_of (ltake (enat (Suc (max i j))) lst) ! j = e &&& list_of (ltake (enat (Suc (max i j))) lst) ! i = e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (filter P (list_of (ltake (enat (Suc (max i j))) lst)))
list_of (ltake (enat (Suc (max i j))) lst) ! j = e
list_of (ltake (enat (Suc (max i j))) lst) ! i = e

goal (1 subgoal):
 1. i = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
by(rule distinct_filterD[OF d(1) jle ile assms(6) d(2,3)])
[PROOF STATE]
proof (state)
this:
i = j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ldistinct_lfilter_conv:
  "ldistinct (lfilter P lst) = (\<forall> i j. i < llength lst \<longrightarrow> j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ldistinct (lfilter P lst) = (\<forall>i j. enat i < llength lst \<longrightarrow> enat j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ldistinct (lfilter P lst) \<Longrightarrow> \<forall>i j. enat i < llength lst \<longrightarrow> enat j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j
 2. \<forall>i j. enat i < llength lst \<longrightarrow> enat j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j \<Longrightarrow> ldistinct (lfilter P lst)
[PROOF STEP]
show "ldistinct (lfilter P lst) \<Longrightarrow> \<forall>i j. enat i < llength lst \<longrightarrow> enat j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ldistinct (lfilter P lst) \<Longrightarrow> \<forall>i j. enat i < llength lst \<longrightarrow> enat j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j
[PROOF STEP]
by (auto simp add: ldistinct_lfilterE)
[PROOF STATE]
proof (state)
this:
ldistinct (lfilter P lst) \<Longrightarrow> \<forall>i j. enat i < llength lst \<longrightarrow> enat j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j

goal (1 subgoal):
 1. \<forall>i j. enat i < llength lst \<longrightarrow> enat j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j \<Longrightarrow> ldistinct (lfilter P lst)
[PROOF STEP]
show "\<forall>i j. enat i < llength lst \<longrightarrow> enat j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j \<Longrightarrow> ldistinct (lfilter P lst) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. enat i < llength lst \<longrightarrow> enat j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j \<Longrightarrow> ldistinct (lfilter P lst)
[PROOF STEP]
using ldistinct_lfilterI
[PROOF STATE]
proof (prove)
using this:
(\<And>i j. \<lbrakk>enat i < llength ?lst; enat j < llength ?lst; ?lst $ i = ?lst $ j; ?P (?lst $ i)\<rbrakk> \<Longrightarrow> i = j) \<Longrightarrow> ldistinct (lfilter ?P ?lst)

goal (1 subgoal):
 1. \<forall>i j. enat i < llength lst \<longrightarrow> enat j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j \<Longrightarrow> ldistinct (lfilter P lst)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i j. enat i < llength lst \<longrightarrow> enat j < llength lst \<longrightarrow> P (lst $ i) \<longrightarrow> lst $ i = lst $ j \<longrightarrow> i = j \<Longrightarrow> ldistinct (lfilter P lst)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eq_eqI[case_names bottomLTR bottomRTL LTR RTL]:
  "(x = \<bottom> \<Longrightarrow> y = \<bottom>) \<Longrightarrow> (y = \<bottom> \<Longrightarrow> x = \<bottom>) \<Longrightarrow> (x = TT \<Longrightarrow> y = TT) \<Longrightarrow> (y = TT \<Longrightarrow> x = TT) \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = \<bottom> \<Longrightarrow> y = \<bottom>; y = \<bottom> \<Longrightarrow> x = \<bottom>; x = TT \<Longrightarrow> y = TT; y = TT \<Longrightarrow> x = TT\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (metis Exh_tr)


[STATEMENT]
lemma eq_tr_simps [simp]:
  shows "eq\<cdot>TT\<cdot>TT = TT" and "eq\<cdot>TT\<cdot>FF = FF"
    and "eq\<cdot>FF\<cdot>TT = FF" and "eq\<cdot>FF\<cdot>FF = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eq\<cdot>TT\<cdot>TT = TT &&& eq\<cdot>TT\<cdot>FF = FF) &&& eq\<cdot>FF\<cdot>TT = FF &&& eq\<cdot>FF\<cdot>FF = TT
[PROOF STEP]
unfolding TT_def FF_def eq_lift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Lambda> (Def x) (Def y). Def (x = y))\<cdot>(Def True)\<cdot>(Def True) = Def True &&& (\<Lambda> (Def x) (Def y). Def (x = y))\<cdot>(Def True)\<cdot>(Def False) = Def False) &&& (\<Lambda> (Def x) (Def y). Def (x = y))\<cdot>(Def False)\<cdot>(Def True) = Def False &&& (\<Lambda> (Def x) (Def y). Def (x = y))\<cdot>(Def False)\<cdot>(Def False) = Def True
[PROOF STEP]
by simp_all


[STATEMENT]
lemma compare_tr_simps [simp]:
  "compare\<cdot>FF\<cdot>FF = EQ"
  "compare\<cdot>FF\<cdot>TT = LT"
  "compare\<cdot>TT\<cdot>FF = GT"
  "compare\<cdot>TT\<cdot>TT = EQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (compare\<cdot>FF\<cdot>FF = EQ &&& compare\<cdot>FF\<cdot>TT = LT) &&& compare\<cdot>TT\<cdot>FF = GT &&& compare\<cdot>TT\<cdot>TT = EQ
[PROOF STEP]
unfolding TT_def FF_def compare_lift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Lambda> (Def x) (Def y). if x < y then LT else if y < x then GT else EQ)\<cdot>(Def False)\<cdot>(Def False) = EQ &&& (\<Lambda> (Def x) (Def y). if x < y then LT else if y < x then GT else EQ)\<cdot>(Def False)\<cdot>(Def True) = LT) &&& (\<Lambda> (Def x) (Def y). if x < y then LT else if y < x then GT else EQ)\<cdot>(Def True)\<cdot>(Def False) = GT &&& (\<Lambda> (Def x) (Def y). if x < y then LT else if y < x then GT else EQ)\<cdot>(Def True)\<cdot>(Def True) = EQ
[PROOF STEP]
by simp_all


[STATEMENT]
lemma andalso_eq_TT_iff [simp]:
  "(x andalso y) = TT \<longleftrightarrow> x = TT \<and> y = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x andalso y) = TT) = (x = TT \<and> y = TT)
[PROOF STEP]
by (cases x, simp_all)


[STATEMENT]
lemma andalso_eq_FF_iff [simp]:
  "(x andalso y) = FF \<longleftrightarrow> x = FF \<or> (x = TT \<and> y = FF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x andalso y) = FF) = (x = FF \<or> x = TT \<and> y = FF)
[PROOF STEP]
by (cases x, simp_all)


[STATEMENT]
lemma andalso_eq_bottom_iff [simp]:
  "(x andalso y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<or> (x = TT \<and> y = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x andalso y) = \<bottom>) = (x = \<bottom> \<or> x = TT \<and> y = \<bottom>)
[PROOF STEP]
by (cases x, simp_all)


[STATEMENT]
lemma orelse_eq_FF_iff [simp]:
  "(x orelse y) = FF \<longleftrightarrow> x = FF \<and> y = FF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x orelse y) = FF) = (x = FF \<and> y = FF)
[PROOF STEP]
by (cases x, simp_all)


[STATEMENT]
lemma orelse_assoc [simp]:
  "((x orelse y) orelse z) = (x orelse y orelse z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x orelse y) orelse z) = (x orelse y orelse z)
[PROOF STEP]
by (cases x) auto


[STATEMENT]
lemma andalso_assoc [simp]:
  "((x andalso y) andalso z) = (x andalso y andalso z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x andalso y) andalso z) = (x andalso y andalso z)
[PROOF STEP]
by (cases x) auto


[STATEMENT]
lemma neg_orelse [simp]:
  "neg\<cdot>(x orelse y) = (neg\<cdot>x andalso neg\<cdot>y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neg\<cdot>(x orelse y) = (neg\<cdot>x andalso neg\<cdot>y)
[PROOF STEP]
by (cases x) auto


[STATEMENT]
lemma neg_andalso [simp]:
  "neg\<cdot>(x andalso y) = (neg\<cdot>x orelse neg\<cdot>y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neg\<cdot>(x andalso y) = (neg\<cdot>x orelse neg\<cdot>y)
[PROOF STEP]
by (cases x) auto


[STATEMENT]
lemma neg_eq_simps:
  "neg\<cdot>x = TT \<Longrightarrow> x = FF"
  "neg\<cdot>x = FF \<Longrightarrow> x = TT"
  "neg\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (neg\<cdot>x = TT \<Longrightarrow> x = FF) &&& (neg\<cdot>x = FF \<Longrightarrow> x = TT) &&& (neg\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>)
[PROOF STEP]
by (cases x, simp_all)+


[STATEMENT]
lemma neg_eq_TT_iff [simp]: "neg\<cdot>x = TT \<longleftrightarrow> x = FF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (neg\<cdot>x = TT) = (x = FF)
[PROOF STEP]
by (cases x, simp_all)+


[STATEMENT]
lemma neg_eq_FF_iff [simp]: "neg\<cdot>x = FF \<longleftrightarrow> x = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (neg\<cdot>x = FF) = (x = TT)
[PROOF STEP]
by (cases x, simp_all)+


[STATEMENT]
lemma neg_eq_bottom_iff [simp]: "neg\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (neg\<cdot>x = \<bottom>) = (x = \<bottom>)
[PROOF STEP]
by (cases x, simp_all)+


[STATEMENT]
lemma neg_eq [simp]:
  "neg\<cdot>x = neg\<cdot>y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (neg\<cdot>x = neg\<cdot>y) = (x = y)
[PROOF STEP]
by (cases y, simp_all)


[STATEMENT]
lemma neg_neg [simp]:
  "neg\<cdot>(neg\<cdot>x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neg\<cdot>(neg\<cdot>x) = x
[PROOF STEP]
by (cases x, auto)


[STATEMENT]
lemma neg_comp_neg [simp]:
  "neg oo neg = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neg oo neg = ID
[PROOF STEP]
by (metis cfun_eqI cfcomp2 neg_neg ID1)


[STATEMENT]
lemma AXc:
assumes
  "c1 \<noteq> c2" and
  "c1 \<in># X" and
  "c2 \<in># X"
shows "(A1 \<union># ((A2 \<union># (X -# c2)) -# c1))
      = (A2 \<union># ((A1 \<union># (X -# c1)) -# c2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1 \<union># A2 \<union># X -# c2 -# c1 = A2 \<union># A1 \<union># X -# c1 -# c2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A1 \<union># A2 \<union># X -# c2 -# c1 = A2 \<union># A1 \<union># X -# c1 -# c2
[PROOF STEP]
have
    "(A2 \<union># ((A1 \<union># (X -# c1)) -# c2))
         = (A2 \<union># (A1 \<union># ((X -# c1) -# c2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A2 \<union># A1 \<union># X -# c1 -# c2 = A2 \<union># A1 \<union># X -# c1 -# c2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c1 \<noteq> c2
c1 \<in># X
c2 \<in># X

goal (1 subgoal):
 1. A2 \<union># A1 \<union># X -# c1 -# c2 = A2 \<union># A1 \<union># X -# c1 -# c2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A2 \<union># A1 \<union># X -# c1 -# c2 = A2 \<union># A1 \<union># X -# c1 -# c2

goal (1 subgoal):
 1. A1 \<union># A2 \<union># X -# c2 -# c1 = A2 \<union># A1 \<union># X -# c1 -# c2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A2 \<union># A1 \<union># X -# c1 -# c2 = A2 \<union># A1 \<union># X -# c1 -# c2

goal (1 subgoal):
 1. A1 \<union># A2 \<union># X -# c2 -# c1 = A2 \<union># A1 \<union># X -# c1 -# c2
[PROOF STEP]
have
    "... = (A1 \<union># ((A2 \<union># (X -# c2)) -# c1)) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A2 \<union># A1 \<union># X -# c1 -# c2 = A1 \<union># A2 \<union># X -# c2 -# c1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c1 \<noteq> c2
c1 \<in># X
c2 \<in># X

goal (1 subgoal):
 1. A2 \<union># A1 \<union># X -# c1 -# c2 = A1 \<union># A2 \<union># X -# c2 -# c1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A2 \<union># A1 \<union># X -# c1 -# c2 = A1 \<union># A2 \<union># X -# c2 -# c1

goal (1 subgoal):
 1. A1 \<union># A2 \<union># X -# c2 -# c1 = A2 \<union># A1 \<union># X -# c1 -# c2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A2 \<union># A1 \<union># X -# c1 -# c2 = A1 \<union># A2 \<union># X -# c2 -# c1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A2 \<union># A1 \<union># X -# c1 -# c2 = A1 \<union># A2 \<union># X -# c2 -# c1

goal (1 subgoal):
 1. A1 \<union># A2 \<union># X -# c2 -# c1 = A2 \<union># A1 \<union># X -# c1 -# c2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A1 \<union># A2 \<union># X -# c2 -# c1 = A2 \<union># A1 \<union># X -# c1 -# c2

goal:
No subgoals!
[PROOF STEP]
qed