[STATEMENT]
lemma FINITE_ALL_DISTINCT_LISTS_i:
  fixes P
  assumes "finite P"
  shows "
    {p. distinct p \<and> set p \<subseteq> P}
    = {[]} \<union> (\<Union> ((\<lambda>e. {e # p0 | p0. distinct p0 \<and> set p0 \<subseteq> (P - {e})}) ` P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
let ?A="{p. distinct p \<and> set p \<subseteq> P }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
let ?B="{[]} \<union> (\<Union> ((\<lambda>e. {e # p0 | p0. distinct p0 \<and> set p0 \<subseteq> (P - {e})}) ` P))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
assume P: "a \<in> ?A"
[PROOF STATE]
proof (state)
this:
a \<in> {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
have "a \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
a \<in> {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
text \<open> The empty list is distinct and its corresponding set is the empty set which is a
            trivial subset of `?B`. The `Nil` case can therefore be derived by automation. \<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
case (Cons h list)
[PROOF STATE]
proof (state)
this:
a = h # list

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a = h # list

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
let ?b'="h"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
a \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
have "set a \<subseteq> P"
[PROOF STATE]
proof (prove)
using this:
a \<in> {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. set a \<subseteq> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set a \<subseteq> P

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set a \<subseteq> P
[PROOF STEP]
have "set list \<subseteq> (P - {h})"
[PROOF STATE]
proof (prove)
using this:
set a \<subseteq> P

goal (1 subgoal):
 1. set list \<subseteq> P - {h}
[PROOF STEP]
using P dual_order.trans local.Cons
[PROOF STATE]
proof (prove)
using this:
set a \<subseteq> P
a \<in> {p. distinct p \<and> set p \<subseteq> P}
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a
a = h # list

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

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
set list \<subseteq> P - {h}

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set list \<subseteq> P - {h}

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
from P Cons
[PROOF STATE]
proof (chain)
picking this:
a \<in> {p. distinct p \<and> set p \<subseteq> P}
a = h # list
[PROOF STEP]
have "distinct list"
[PROOF STATE]
proof (prove)
using this:
a \<in> {p. distinct p \<and> set p \<subseteq> P}
a = h # list

goal (1 subgoal):
 1. distinct list
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
distinct list

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set list \<subseteq> P - {h}
distinct list
[PROOF STEP]
have "a \<in> ((\<lambda>e. {e # p0 | p0. distinct p0 \<and> set p0 \<subseteq> (P - {e})}) ?b')"
[PROOF STATE]
proof (prove)
using this:
set list \<subseteq> P - {h}
distinct list

goal (1 subgoal):
 1. a \<in> {h # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {h}}
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
set list \<subseteq> P - {h}
distinct list
a = h # list

goal (1 subgoal):
 1. a \<in> {h # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {h}}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> {h # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {h}}

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<in> {h # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {h}}

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a \<in> {h # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {h}}

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
from P Cons
[PROOF STATE]
proof (chain)
picking this:
a \<in> {p. distinct p \<and> set p \<subseteq> P}
a = h # list
[PROOF STEP]
have "?b' \<in> set a"
[PROOF STATE]
proof (prove)
using this:
a \<in> {p. distinct p \<and> set p \<subseteq> P}
a = h # list

goal (1 subgoal):
 1. h \<in> set a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h \<in> set a

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
h \<in> set a

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
a \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
have "set a \<subseteq> P"
[PROOF STATE]
proof (prove)
using this:
a \<in> {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. set a \<subseteq> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set a \<subseteq> P

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
h \<in> set a
set a \<subseteq> P
[PROOF STEP]
have "?b' \<in> P"
[PROOF STATE]
proof (prove)
using this:
h \<in> set a
set a \<subseteq> P

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

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
h \<in> P

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<in> {h # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {h}}
h \<in> P
[PROOF STEP]
have
            "\<exists>b' \<in> P. a \<in> ((\<lambda>e. {e # p0 | p0. distinct p0 \<and> set p0 \<subseteq> (P - {e})}) b')"
[PROOF STATE]
proof (prove)
using this:
a \<in> {h # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {h}}
h \<in> P

goal (1 subgoal):
 1. \<exists>b'\<in>P. a \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
\<exists>b'\<in>P. a \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>b'\<in>P. a \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>b'\<in>P. a \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}
[PROOF STEP]
obtain b' where
          "b' \<in> P" "a \<in> ((\<lambda>e. {e # p0 | p0. distinct p0 \<and> set p0 \<subseteq> (P - {e})}) b')"
[PROOF STATE]
proof (prove)
using this:
\<exists>b'\<in>P. a \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}

goal (1 subgoal):
 1. (\<And>b'. \<lbrakk>b' \<in> P; a \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b' \<in> P
a \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}

goal (2 subgoals):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
 2. \<And>aa list. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = aa # list\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b' \<in> P
a \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b' \<in> P
a \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}

goal (1 subgoal):
 1. a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. \<lbrakk>a \<in> {p. distinct p \<and> set p \<subseteq> P}; a = []\<rbrakk> \<Longrightarrow> a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
qed blast
[PROOF STATE]
proof (state)
this:
a \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?a2 \<in> {p. distinct p \<and> set p \<subseteq> P} \<Longrightarrow> ?a2 \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?a2 \<in> {p. distinct p \<and> set p \<subseteq> P} \<Longrightarrow> ?a2 \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
have "?A \<subseteq> ?B"
[PROOF STATE]
proof (prove)
using this:
?a2 \<in> {p. distinct p \<and> set p \<subseteq> P} \<Longrightarrow> ?a2 \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} \<subseteq> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{p. distinct p \<and> set p \<subseteq> P} \<subseteq> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
{p. distinct p \<and> set p \<subseteq> P} \<subseteq> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{p. distinct p \<and> set p \<subseteq> P} \<subseteq> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
{p. distinct p \<and> set p \<subseteq> P} \<subseteq> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
{p. distinct p \<and> set p \<subseteq> P} \<subseteq> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
assume P: "b \<in> ?B"
[PROOF STATE]
proof (state)
this:
b \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
have "b \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
text \<open> The empty list is in `?B` by construction. The `Nil` case can therefore be derived
          straightforwardly.\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
proof (cases b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = [] \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
 2. \<And>a list. b = a # list \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
case (Cons a list)
[PROOF STATE]
proof (state)
this:
b = a # list

goal (2 subgoals):
 1. b = [] \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
 2. \<And>a list. b = a # list \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
from P Cons
[PROOF STATE]
proof (chain)
picking this:
b \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
b = a # list
[PROOF STEP]
obtain b' where a:
          "b' \<in> P" "b \<in> {b' # p0 | p0. distinct p0 \<and> set p0 \<subseteq> (P - {b'})}"
[PROOF STATE]
proof (prove)
using this:
b \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
b = a # list

goal (1 subgoal):
 1. (\<And>b'. \<lbrakk>b' \<in> P; b \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
b' \<in> P
b \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}

goal (2 subgoals):
 1. b = [] \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
 2. \<And>a list. b = a # list \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b' \<in> P
b \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}
[PROOF STEP]
obtain p0 where b: "b = b' # p0" "distinct p0" "set p0 \<subseteq> (P - {b'})"
[PROOF STATE]
proof (prove)
using this:
b' \<in> P
b \<in> {b' # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {b'}}

goal (1 subgoal):
 1. (\<And>p0. \<lbrakk>b = b' # p0; distinct p0; set p0 \<subseteq> P - {b'}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = b' # p0
distinct p0
set p0 \<subseteq> P - {b'}

goal (2 subgoals):
 1. b = [] \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
 2. \<And>a list. b = a # list \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = b' # p0
distinct p0
set p0 \<subseteq> P - {b'}
[PROOF STEP]
have "distinct (b' # p0)"
[PROOF STATE]
proof (prove)
using this:
b = b' # p0
distinct p0
set p0 \<subseteq> P - {b'}

goal (1 subgoal):
 1. distinct (b' # p0)
[PROOF STEP]
by (simp add: subset_Diff_insert)
[PROOF STATE]
proof (state)
this:
distinct (b' # p0)

goal (2 subgoals):
 1. b = [] \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
 2. \<And>a list. b = a # list \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (b' # p0)

goal (2 subgoals):
 1. b = [] \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
 2. \<And>a list. b = a # list \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
have "set (b' # p0) \<subseteq> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (b' # p0) \<subseteq> P
[PROOF STEP]
using a(1) b(3)
[PROOF STATE]
proof (prove)
using this:
b' \<in> P
set p0 \<subseteq> P - {b'}

goal (1 subgoal):
 1. set (b' # p0) \<subseteq> P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (b' # p0) \<subseteq> P

goal (2 subgoals):
 1. b = [] \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
 2. \<And>a list. b = a # list \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct (b' # p0)
set (b' # p0) \<subseteq> P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct (b' # p0)
set (b' # p0) \<subseteq> P

goal (1 subgoal):
 1. b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
using b(1)
[PROOF STATE]
proof (prove)
using this:
distinct (b' # p0)
set (b' # p0) \<subseteq> P
b = b' # p0

goal (1 subgoal):
 1. b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
b \<in> {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. b = [] \<Longrightarrow> b \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
b \<in> {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?b2 \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}) \<Longrightarrow> ?b2 \<in> {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?b2 \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}) \<Longrightarrow> ?b2 \<in> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
have "?B \<subseteq> ?A"
[PROOF STATE]
proof (prove)
using this:
?b2 \<in> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}) \<Longrightarrow> ?b2 \<in> {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}) \<subseteq> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}) \<subseteq> {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
{[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}) \<subseteq> {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{p. distinct p \<and> set p \<subseteq> P} \<subseteq> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
{[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}) \<subseteq> {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{p. distinct p \<and> set p \<subseteq> P} \<subseteq> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
{[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}) \<subseteq> {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
using set_eq_subset
[PROOF STATE]
proof (prove)
using this:
{p. distinct p \<and> set p \<subseteq> P} \<subseteq> {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
{[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}) \<subseteq> {p. distinct p \<and> set p \<subseteq> P}
(?A = ?B) = (?A \<subseteq> ?B \<and> ?B \<subseteq> ?A)

goal (1 subgoal):
 1. {p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma FINITE_ALL_DISTINCT_LISTS:
  fixes P
  assumes "finite P"
  shows "finite {p. distinct p \<and> set p \<subseteq> P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite P

goal (1 subgoal):
 1. finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
proof (induction "card P" arbitrary: P)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>0 = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
 2. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = card P
finite P

goal (2 subgoals):
 1. \<And>P. \<lbrakk>0 = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
 2. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 = card P
finite P
[PROOF STEP]
have "P = {}"
[PROOF STATE]
proof (prove)
using this:
0 = card P
finite P

goal (1 subgoal):
 1. P = {}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
P = {}

goal (2 subgoals):
 1. \<And>P. \<lbrakk>0 = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
 2. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P = {}

goal (1 subgoal):
 1. finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
P = {}
0 = card P
finite P

goal (1 subgoal):
 1. finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {p. distinct p \<and> set p \<subseteq> P}

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
case (Suc x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = card ?P; finite ?P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> ?P}
Suc x = card P
finite P

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = card ?P; finite ?P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> ?P}
Suc x = card P
finite P

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
text \<open> Proof the finiteness of the union by proving both sets of the union are finite. The
      singleton set `{[]}` is trivially finite. \<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = card ?P; finite ?P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> ?P}
Suc x = card P
finite P

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = card ?P; finite ?P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> ?P}
Suc x = card P
finite P

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = card ?P; finite ?P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> ?P}
Suc x = card P
finite P

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
fix e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
assume P: "e \<in> P"
[PROOF STATE]
proof (state)
this:
e \<in> P

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
have "
          {e # p0 | p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}
          = (\<lambda>p. e # p) ` { p. distinct p \<and> set p \<subseteq> P - {e}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}} = (#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}} = (#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}}

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}} = (#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}}

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
{e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}} = (#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}}

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
let ?P'="P - {e}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
from Suc.prems
[PROOF STATE]
proof (chain)
picking this:
finite P
[PROOF STEP]
have "finite ?P'"
[PROOF STATE]
proof (prove)
using this:
finite P

goal (1 subgoal):
 1. finite (P - {e})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (P - {e})

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
text \<open> The finiteness can now be shown using the induction hypothesis. However `e` might
            already be contained in `?P`, so we have to split cases first. \<close>
[PROOF STATE]
proof (state)
this:
finite (P - {e})

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
have "finite ((\<lambda>p. e # p) ` {p. distinct p \<and> set p \<subseteq> ?P'})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
proof (cases "e \<in> P")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. e \<in> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
 2. e \<notin> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
e \<in> P

goal (2 subgoals):
 1. e \<in> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
 2. e \<notin> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e \<in> P
[PROOF STEP]
have "x = card ?P'"
[PROOF STATE]
proof (prove)
using this:
e \<in> P

goal (1 subgoal):
 1. x = card (P - {e})
[PROOF STEP]
using Suc.prems Suc(2)
[PROOF STATE]
proof (prove)
using this:
e \<in> P
finite P
Suc x = card P

goal (1 subgoal):
 1. x = card (P - {e})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x = card (P - {e})

goal (2 subgoals):
 1. e \<in> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
 2. e \<notin> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = card (P - {e})

goal (2 subgoals):
 1. e \<in> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
 2. e \<notin> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
from Suc.prems
[PROOF STATE]
proof (chain)
picking this:
finite P
[PROOF STEP]
have "finite ?P'"
[PROOF STATE]
proof (prove)
using this:
finite P

goal (1 subgoal):
 1. finite (P - {e})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (P - {e})

goal (2 subgoals):
 1. e \<in> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
 2. e \<notin> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = card (P - {e})
finite (P - {e})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = card (P - {e})
finite (P - {e})

goal (1 subgoal):
 1. finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
using Suc(1)
[PROOF STATE]
proof (prove)
using this:
x = card (P - {e})
finite (P - {e})
\<lbrakk>x = card ?P; finite ?P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> ?P}

goal (1 subgoal):
 1. finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})

goal (1 subgoal):
 1. e \<notin> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e \<notin> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
e \<notin> P

goal (1 subgoal):
 1. e \<notin> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e \<notin> P
[PROOF STEP]
have "?P' = P"
[PROOF STATE]
proof (prove)
using this:
e \<notin> P

goal (1 subgoal):
 1. P - {e} = P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P - {e} = P

goal (1 subgoal):
 1. e \<notin> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P - {e} = P
[PROOF STEP]
have "finite {p. distinct p \<and> set p \<subseteq> ?P'}"
[PROOF STATE]
proof (prove)
using this:
P - {e} = P

goal (1 subgoal):
 1. finite {p. distinct p \<and> set p \<subseteq> P - {e}}
[PROOF STEP]
using False P
[PROOF STATE]
proof (prove)
using this:
P - {e} = P
e \<notin> P
e \<in> P

goal (1 subgoal):
 1. finite {p. distinct p \<and> set p \<subseteq> P - {e}}
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
finite {p. distinct p \<and> set p \<subseteq> P - {e}}

goal (1 subgoal):
 1. e \<notin> P \<Longrightarrow> finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite {p. distinct p \<and> set p \<subseteq> P - {e}}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {p. distinct p \<and> set p \<subseteq> P - {e}}

goal (1 subgoal):
 1. finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
using finite_imageI
[PROOF STATE]
proof (prove)
using this:
finite {p. distinct p \<and> set p \<subseteq> P - {e}}
finite ?F \<Longrightarrow> finite (?h ` ?F)

goal (1 subgoal):
 1. finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}} = (#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}}
finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})
[PROOF STEP]
have "finite {e # p0 | p0. distinct p0 \<and> set p0 \<subseteq> (P - {e})}"
[PROOF STATE]
proof (prove)
using this:
{e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}} = (#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}}
finite ((#) e ` {p. distinct p \<and> set p \<subseteq> P - {e}})

goal (1 subgoal):
 1. finite {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
finite {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?e2 \<in> P \<Longrightarrow> finite {?e2 # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {?e2}}

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?e2 \<in> P \<Longrightarrow> finite {?e2 # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {?e2}}
[PROOF STEP]
have "finite (\<Union> ((\<lambda>e. {e # p0 | p0. distinct p0 \<and> set p0 \<subseteq> (P - {e})}) ` P))"
[PROOF STATE]
proof (prove)
using this:
?e2 \<in> P \<Longrightarrow> finite {?e2 # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {?e2}}

goal (1 subgoal):
 1. finite (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
?e2 \<in> P \<Longrightarrow> finite {?e2 # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {?e2}}
finite P

goal (1 subgoal):
 1. finite (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
finite (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
[PROOF STEP]
have
      "finite ({[]} \<union> (\<Union> ((\<lambda>e. {e # p0 | p0. distinct p0 \<and> set p0 \<subseteq> (P - {e})}) ` P)))"
[PROOF STATE]
proof (prove)
using this:
finite (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. finite ({[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}))
[PROOF STEP]
using finite_Un
[PROOF STATE]
proof (prove)
using this:
finite (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})
finite (?F \<union> ?G) = (finite ?F \<and> finite ?G)

goal (1 subgoal):
 1. finite ({[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite ({[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}))

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
finite ({[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}))

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<And>P. \<lbrakk>x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}; Suc x = card P; finite P\<rbrakk> \<Longrightarrow> finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite ({[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite ({[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}))

goal (1 subgoal):
 1. finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
using FINITE_ALL_DISTINCT_LISTS_i[OF Suc.prems]
[PROOF STATE]
proof (prove)
using this:
finite ({[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}}))
{p. distinct p \<and> set p \<subseteq> P} = {[]} \<union> (\<Union>e\<in>P. {e # p0 |p0. distinct p0 \<and> set p0 \<subseteq> P - {e}})

goal (1 subgoal):
 1. finite {p. distinct p \<and> set p \<subseteq> P}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite {p. distinct p \<and> set p \<subseteq> P}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subset_inter_diff_empty:
  assumes "s \<subseteq> t"
  shows "(s \<inter> (u - t) = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<inter> (u - t) = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<subseteq> t

goal (1 subgoal):
 1. s \<inter> (u - t) = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma map_of_tabulate:
  "map_of (map (\<lambda>x. (x, f x)) xs) x \<noteq> None \<longleftrightarrow> x \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_of (map (\<lambda>x. (x, f x)) xs) x \<noteq> None) = (x \<in> set xs)
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma map_of_tabulate_simp:
  "map_of (map (\<lambda>x. (x, f x)) xs) x = (if x \<in> set xs then Some (f x) else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>x. (x, f x)) xs) x = (if x \<in> set xs then Some (f x) else None)
[PROOF STEP]
by (metis (mono_tags, lifting) comp_eq_dest_lhs map_of_map_restrict restrict_map_def)


[STATEMENT]
lemma dom_map_update:
  "dom (m (k \<mapsto> v)) = dom m \<union> {k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (m(k \<mapsto> v)) = dom m \<union> {k}
[PROOF STEP]
by simp


[STATEMENT]
lemma map_equal:
  "dom m = dom m' \<Longrightarrow> (\<And>x. x \<in> dom m \<Longrightarrow> m x = m' x) \<Longrightarrow> m = m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom m = dom m'; \<And>x. x \<in> dom m \<Longrightarrow> m x = m' x\<rbrakk> \<Longrightarrow> m = m'
[PROOF STEP]
by fastforce


[STATEMENT]
lemma map_reduce:
  assumes "dom m = {a} \<union> B"
  shows "\<exists>m'. dom m' = B \<and> (\<forall>x \<in> B. m x = m' x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
[PROOF STEP]
proof (cases "a \<in> B")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> B \<Longrightarrow> \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
 2. a \<notin> B \<Longrightarrow> \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> B

goal (2 subgoals):
 1. a \<in> B \<Longrightarrow> \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
 2. a \<notin> B \<Longrightarrow> \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<in> B

goal (1 subgoal):
 1. \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> B
dom m = {a} \<union> B

goal (1 subgoal):
 1. \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
[PROOF STEP]
by (metis insert_absorb insert_is_Un)
[PROOF STATE]
proof (state)
this:
\<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)

goal (1 subgoal):
 1. a \<notin> B \<Longrightarrow> \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin> B \<Longrightarrow> \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> B

goal (1 subgoal):
 1. a \<notin> B \<Longrightarrow> \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
dom m = {a} \<union> B
a \<notin> B
[PROOF STEP]
have "dom (m (a := None)) = B \<and> (\<forall>x\<in>B. m x = (m (a := None)) x)"
[PROOF STATE]
proof (prove)
using this:
dom m = {a} \<union> B
a \<notin> B

goal (1 subgoal):
 1. dom (m(a := None)) = B \<and> (\<forall>x\<in>B. m x = (m(a := None)) x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dom (m(a := None)) = B \<and> (\<forall>x\<in>B. m x = (m(a := None)) x)

goal (1 subgoal):
 1. a \<notin> B \<Longrightarrow> \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
dom (m(a := None)) = B \<and> (\<forall>x\<in>B. m x = (m(a := None)) x)

goal (1 subgoal):
 1. \<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m'. dom m' = B \<and> (\<forall>x\<in>B. m x = m' x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_seq_length_mono:
  fixes seq :: "nat \<Rightarrow> 'a list"
  assumes "\<And>i. (\<exists>x. seq (Suc i) = x # seq i)" and "i < j"
  shows "length (seq i) < length (seq j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (seq i) < length (seq j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (seq i) < length (seq j)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
i < j
[PROOF STEP]
obtain k where "j = Suc (i + k)"
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. (\<And>k. j = Suc (i + k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using less_iff_Suc_add
[PROOF STATE]
proof (prove)
using this:
i < j
(?m < ?n) = (\<exists>k. ?n = Suc (?m + k))

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

goal (1 subgoal):
 1. length (seq i) < length (seq j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (seq i) < length (seq j)
[PROOF STEP]
unfolding \<open>j = Suc (i + k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (seq i) < length (seq (Suc (i + k)))
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (seq i) < length (seq (Suc (i + 0)))
 2. \<And>k. length (seq i) < length (seq (Suc (i + k))) \<Longrightarrow> length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. length (seq i) < length (seq (Suc (i + 0)))
 2. \<And>k. length (seq i) < length (seq (Suc (i + k))) \<Longrightarrow> length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. seq (Suc ?i) = x # seq ?i
[PROOF STEP]
obtain x where eq: "seq (Suc i) = x # seq i"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. seq (Suc ?i) = x # seq ?i

goal (1 subgoal):
 1. (\<And>x. seq (Suc i) = x # seq i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
seq (Suc i) = x # seq i

goal (2 subgoals):
 1. length (seq i) < length (seq (Suc (i + 0)))
 2. \<And>k. length (seq i) < length (seq (Suc (i + k))) \<Longrightarrow> length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (seq i) < length (seq (Suc (i + 0)))
[PROOF STEP]
by (simp add: eq)
[PROOF STATE]
proof (state)
this:
length (seq i) < length (seq (Suc (i + 0)))

goal (1 subgoal):
 1. \<And>k. length (seq i) < length (seq (Suc (i + k))) \<Longrightarrow> length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. length (seq i) < length (seq (Suc (i + k))) \<Longrightarrow> length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
length (seq i) < length (seq (Suc (i + k)))

goal (1 subgoal):
 1. \<And>k. length (seq i) < length (seq (Suc (i + k))) \<Longrightarrow> length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. seq (Suc ?i) = x # seq ?i
[PROOF STEP]
obtain x where "seq (Suc (i + Suc k)) = x # seq (i + Suc k)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. seq (Suc ?i) = x # seq ?i

goal (1 subgoal):
 1. (\<And>x. seq (Suc (i + Suc k)) = x # seq (i + Suc k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
seq (Suc (i + Suc k)) = x # seq (i + Suc k)

goal (1 subgoal):
 1. \<And>k. length (seq i) < length (seq (Suc (i + k))) \<Longrightarrow> length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
hence eq: "seq (Suc (Suc (i + k))) = x # seq (Suc (i + k))"
[PROOF STATE]
proof (prove)
using this:
seq (Suc (i + Suc k)) = x # seq (i + Suc k)

goal (1 subgoal):
 1. seq (Suc (Suc (i + k))) = x # seq (Suc (i + k))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
seq (Suc (Suc (i + k))) = x # seq (Suc (i + k))

goal (1 subgoal):
 1. \<And>k. length (seq i) < length (seq (Suc (i + k))) \<Longrightarrow> length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
note Suc
[PROOF STATE]
proof (state)
this:
length (seq i) < length (seq (Suc (i + k)))

goal (1 subgoal):
 1. \<And>k. length (seq i) < length (seq (Suc (i + k))) \<Longrightarrow> length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (seq i) < length (seq (Suc (i + k)))

goal (1 subgoal):
 1. \<And>k. length (seq i) < length (seq (Suc (i + k))) \<Longrightarrow> length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
have "length (seq (Suc (i + k))) < length (seq (Suc (i + Suc k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (seq (Suc (i + k))) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
by (simp add: eq)
[PROOF STATE]
proof (state)
this:
length (seq (Suc (i + k))) < length (seq (Suc (i + Suc k)))

goal (1 subgoal):
 1. \<And>k. length (seq i) < length (seq (Suc (i + k))) \<Longrightarrow> length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length (seq i) < length (seq (Suc (i + Suc k)))

goal (1 subgoal):
 1. length (seq i) < length (seq (Suc (i + Suc k)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
length (seq i) < length (seq (Suc (i + Suc k)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (seq i) < length (seq j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_seq_indexE_length:
  fixes seq :: "nat \<Rightarrow> 'a list"
  assumes "\<And>i. (\<exists>x. seq (Suc i) = x # seq i)"
  obtains j where "i < length (seq j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (induct i arbitrary: thesis)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>thesis. (\<And>j. 0 < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 < length (seq ?j) \<Longrightarrow> thesis

goal (2 subgoals):
 1. \<And>thesis. (\<And>j. 0 < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "0 \<le> length (seq 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> length (seq 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> length (seq 0)

goal (2 subgoals):
 1. \<And>thesis. (\<And>j. 0 < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<le> length (seq 0)

goal (2 subgoals):
 1. \<And>thesis. (\<And>j. 0 < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from assms lessI
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. seq (Suc ?i) = x # seq ?i
?n < Suc ?n
[PROOF STEP]
have "... < length (seq (Suc 0))"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. seq (Suc ?i) = x # seq ?i
?n < Suc ?n

goal (1 subgoal):
 1. length (seq 0) < length (seq (Suc 0))
[PROOF STEP]
by (rule list_seq_length_mono)
[PROOF STATE]
proof (state)
this:
length (seq 0) < length (seq (Suc 0))

goal (2 subgoals):
 1. \<And>thesis. (\<And>j. 0 < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 < length (seq (Suc 0))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < length (seq (Suc 0))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule 0)
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
(\<And>j. i < length (seq j) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
Suc i < length (seq ?j) \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain j where "i < length (seq j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Suc(1))
[PROOF STATE]
proof (state)
this:
i < length (seq j)

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "Suc i \<le> length (seq j)"
[PROOF STATE]
proof (prove)
using this:
i < length (seq j)

goal (1 subgoal):
 1. Suc i \<le> length (seq j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc i \<le> length (seq j)

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc i \<le> length (seq j)

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from assms lessI
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. seq (Suc ?i) = x # seq ?i
?n < Suc ?n
[PROOF STEP]
have "... < length (seq (Suc j))"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. seq (Suc ?i) = x # seq ?i
?n < Suc ?n

goal (1 subgoal):
 1. length (seq j) < length (seq (Suc j))
[PROOF STEP]
by (rule list_seq_length_mono)
[PROOF STATE]
proof (state)
this:
length (seq j) < length (seq (Suc j))

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>j. i < length (seq j) \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>j. Suc i < length (seq j) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Suc i < length (seq (Suc j))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Suc i < length (seq (Suc j))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule Suc(2))
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_seq_nth:
  fixes seq :: "nat \<Rightarrow> 'a list"
  assumes "\<And>i. (\<exists>x. seq (Suc i) = x # seq i)" and "i < length (seq j)" and "j \<le> k"
  shows "rev (seq k) ! i = rev (seq j) ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (seq k) ! i = rev (seq j) ! i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rev (seq k) ! i = rev (seq j) ! i
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
j \<le> k
[PROOF STEP]
obtain l where "k = j + l"
[PROOF STATE]
proof (prove)
using this:
j \<le> k

goal (1 subgoal):
 1. (\<And>l. k = j + l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nat_le_iff_add
[PROOF STATE]
proof (prove)
using this:
j \<le> k
(?m \<le> ?n) = (\<exists>k. ?n = ?m + k)

goal (1 subgoal):
 1. (\<And>l. k = j + l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k = j + l

goal (1 subgoal):
 1. rev (seq k) ! i = rev (seq j) ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (seq k) ! i = rev (seq j) ! i
[PROOF STEP]
unfolding \<open>k = j + l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (seq (j + l)) ! i = rev (seq j) ! i
[PROOF STEP]
proof (induct l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rev (seq (j + 0)) ! i = rev (seq j) ! i
 2. \<And>l. rev (seq (j + l)) ! i = rev (seq j) ! i \<Longrightarrow> rev (seq (j + Suc l)) ! i = rev (seq j) ! i
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. rev (seq (j + 0)) ! i = rev (seq j) ! i
 2. \<And>l. rev (seq (j + l)) ! i = rev (seq j) ! i \<Longrightarrow> rev (seq (j + Suc l)) ! i = rev (seq j) ! i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (seq (j + 0)) ! i = rev (seq j) ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rev (seq (j + 0)) ! i = rev (seq j) ! i

goal (1 subgoal):
 1. \<And>l. rev (seq (j + l)) ! i = rev (seq j) ! i \<Longrightarrow> rev (seq (j + Suc l)) ! i = rev (seq j) ! i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. rev (seq (j + l)) ! i = rev (seq j) ! i \<Longrightarrow> rev (seq (j + Suc l)) ! i = rev (seq j) ! i
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
rev (seq (j + l)) ! i = rev (seq j) ! i

goal (1 subgoal):
 1. \<And>l. rev (seq (j + l)) ! i = rev (seq j) ! i \<Longrightarrow> rev (seq (j + Suc l)) ! i = rev (seq j) ! i
[PROOF STEP]
note assms(2)
[PROOF STATE]
proof (state)
this:
i < length (seq j)

goal (1 subgoal):
 1. \<And>l. rev (seq (j + l)) ! i = rev (seq j) ! i \<Longrightarrow> rev (seq (j + Suc l)) ! i = rev (seq j) ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
i < length (seq j)

goal (1 subgoal):
 1. \<And>l. rev (seq (j + l)) ! i = rev (seq j) ! i \<Longrightarrow> rev (seq (j + Suc l)) ! i = rev (seq j) ! i
[PROOF STEP]
from assms(1) le_add1
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. seq (Suc ?i) = x # seq ?i
?n \<le> ?n + ?m
[PROOF STEP]
have "length (seq j) \<le> length (seq (j + l))"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. seq (Suc ?i) = x # seq ?i
?n \<le> ?n + ?m

goal (1 subgoal):
 1. length (seq j) \<le> length (seq (j + l))
[PROOF STEP]
by (rule list_seq_length_mono_weak)
[PROOF STATE]
proof (state)
this:
length (seq j) \<le> length (seq (j + l))

goal (1 subgoal):
 1. \<And>l. rev (seq (j + l)) ! i = rev (seq j) ! i \<Longrightarrow> rev (seq (j + Suc l)) ! i = rev (seq j) ! i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
i < length (seq (j + l))
[PROOF STEP]
have i: "i < length (seq (j + l))"
[PROOF STATE]
proof (prove)
using this:
i < length (seq (j + l))

goal (1 subgoal):
 1. i < length (seq (j + l))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i < length (seq (j + l))

goal (1 subgoal):
 1. \<And>l. rev (seq (j + l)) ! i = rev (seq j) ! i \<Longrightarrow> rev (seq (j + Suc l)) ! i = rev (seq j) ! i
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. seq (Suc ?i) = x # seq ?i
[PROOF STEP]
obtain x where "seq (Suc (j + l)) = x # seq (j + l)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. seq (Suc ?i) = x # seq ?i

goal (1 subgoal):
 1. (\<And>x. seq (Suc (j + l)) = x # seq (j + l) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
seq (Suc (j + l)) = x # seq (j + l)

goal (1 subgoal):
 1. \<And>l. rev (seq (j + l)) ! i = rev (seq j) ! i \<Longrightarrow> rev (seq (j + Suc l)) ! i = rev (seq j) ! i
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
seq (Suc (j + l)) = x # seq (j + l)

goal (1 subgoal):
 1. rev (seq (j + Suc l)) ! i = rev (seq j) ! i
[PROOF STEP]
by (simp add: nth_append i Suc)
[PROOF STATE]
proof (state)
this:
rev (seq (j + Suc l)) ! i = rev (seq j) ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rev (seq k) ! i = rev (seq j) ! i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma filter_merge_wrt_1:
  assumes "\<And>y. y \<in> set ys \<Longrightarrow> P y \<Longrightarrow> False"
  shows "filter P (merge_wrt rel xs ys) = filter P xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel xs ys) = filter P xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> set ys; P ?y\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. filter P (merge_wrt rel xs ys) = filter P xs
[PROOF STEP]
proof (induct rel xs ys rule: merge_wrt.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>uu_ xs. (\<And>y. \<lbrakk>y \<in> set []; P y\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt uu_ xs []) = filter P xs
 2. \<And>rel v va. (\<And>y. \<lbrakk>y \<in> set (v # va); P y\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt rel [] (v # va)) = filter P []
 3. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
case (1 rel xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<in> set []; P ?y\<rbrakk> \<Longrightarrow> False

goal (3 subgoals):
 1. \<And>uu_ xs. (\<And>y. \<lbrakk>y \<in> set []; P y\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt uu_ xs []) = filter P xs
 2. \<And>rel v va. (\<And>y. \<lbrakk>y \<in> set (v # va); P y\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt rel [] (v # va)) = filter P []
 3. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel xs []) = filter P xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
filter P (merge_wrt rel xs []) = filter P xs

goal (2 subgoals):
 1. \<And>rel v va. (\<And>y. \<lbrakk>y \<in> set (v # va); P y\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt rel [] (v # va)) = filter P []
 2. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>rel v va. (\<And>y. \<lbrakk>y \<in> set (v # va); P y\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt rel [] (v # va)) = filter P []
 2. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
case (2 rel y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<in> set (y # ys); P ?y\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>rel v va. (\<And>y. \<lbrakk>y \<in> set (v # va); P y\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt rel [] (v # va)) = filter P []
 2. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
hence "P y \<Longrightarrow> False" and "\<And>z. z \<in> set ys \<Longrightarrow> P z \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> set (y # ys); P ?y\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (P y \<Longrightarrow> False) &&& (\<And>z. \<lbrakk>z \<in> set ys; P z\<rbrakk> \<Longrightarrow> False)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P y \<Longrightarrow> False
\<lbrakk>?z \<in> set ys; P ?z\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>rel v va. (\<And>y. \<lbrakk>y \<in> set (v # va); P y\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt rel [] (v # va)) = filter P []
 2. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P y \<Longrightarrow> False
\<lbrakk>?z \<in> set ys; P ?z\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. filter P (merge_wrt rel [] (y # ys)) = filter P []
[PROOF STEP]
by (auto simp: filter_empty_conv)
[PROOF STATE]
proof (state)
this:
filter P (merge_wrt rel [] (y # ys)) = filter P []

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
case (3 rel x xs y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs
\<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs
\<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs)
\<lbrakk>?y \<in> set (y # ys); P ?y\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
hence "\<not> P y" and x: "\<And>z. z \<in> set ys \<Longrightarrow> P z \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs
\<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs
\<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs)
\<lbrakk>?y \<in> set (y # ys); P ?y\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> P y &&& (\<And>z. \<lbrakk>z \<in> set ys; P z\<rbrakk> \<Longrightarrow> False)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> P y
\<lbrakk>?z \<in> set ys; P ?z\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
have a: "filter P (merge_wrt rel xs ys) = filter P xs" if "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel xs ys) = filter P xs
[PROOF STEP]
using that x
[PROOF STATE]
proof (prove)
using this:
x = y
\<lbrakk>?z \<in> set ys; P ?z\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. filter P (merge_wrt rel xs ys) = filter P xs
[PROOF STEP]
by (rule 3(1))
[PROOF STATE]
proof (state)
this:
x = y \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
have b: "filter P (merge_wrt rel xs (y # ys)) = filter P xs" if "x \<noteq> y" and "rel x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel xs (y # ys)) = filter P xs
[PROOF STEP]
using that 3(4)
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
rel x y
\<lbrakk>?y \<in> set (y # ys); P ?y\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. filter P (merge_wrt rel xs (y # ys)) = filter P xs
[PROOF STEP]
by (rule 3(2))
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<noteq> y; rel x y\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
have c: "filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs)" if "x \<noteq> y" and "\<not> rel x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs)
[PROOF STEP]
using that x
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
\<not> rel x y
\<lbrakk>?z \<in> set ys; P ?z\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs)
[PROOF STEP]
by (rule 3(3))
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<noteq> y; \<not> rel x y\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs)

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P xs; \<lbrakk>x \<noteq> y; rel x y; \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P xs; \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>y. \<lbrakk>y \<in> set ys; P y\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P (x # xs); \<And>ya. \<lbrakk>ya \<in> set (y # ys); P ya\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)
[PROOF STEP]
by (simp add: a b c \<open>\<not> P y\<close>)
[PROOF STATE]
proof (state)
this:
filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (x # xs)

goal:
No subgoals!
[PROOF STEP]
qed