[STATEMENT]
lemma square_dvd_squarefree_part_iff:
  "x^2 dvd \<Prod>(squarefree_part n) \<longleftrightarrow> x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>2 dvd \<Prod>(squarefree_part n)) = (x = 1)
[PROOF STEP]
proof (rule iffI, rule multiplicity_eq_nat)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < x
 2. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 3. \<And>p. \<lbrakk>x\<^sup>2 dvd \<Prod>(squarefree_part n); prime p\<rbrakk> \<Longrightarrow> multiplicity p x = multiplicity p 1
 4. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
assume dvd: "x^2 dvd \<Prod>(squarefree_part n)"
[PROOF STATE]
proof (state)
this:
x\<^sup>2 dvd \<Prod>(squarefree_part n)

goal (4 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < x
 2. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 3. \<And>p. \<lbrakk>x\<^sup>2 dvd \<Prod>(squarefree_part n); prime p\<rbrakk> \<Longrightarrow> multiplicity p x = multiplicity p 1
 4. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
hence "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 dvd \<Prod>(squarefree_part n)

goal (1 subgoal):
 1. x \<noteq> 0
[PROOF STEP]
using squarefree_part_subset[of n] prime_gt_0_nat
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 dvd \<Prod>(squarefree_part n)
squarefree_part n \<subseteq> prime_factors n
prime ?p \<Longrightarrow> 0 < ?p

goal (1 subgoal):
 1. x \<noteq> 0
[PROOF STEP]
by (intro notI) auto
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (4 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < x
 2. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 3. \<And>p. \<lbrakk>x\<^sup>2 dvd \<Prod>(squarefree_part n); prime p\<rbrakk> \<Longrightarrow> multiplicity p x = multiplicity p 1
 4. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
thus x: "x > 0"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

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

goal (3 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 2. \<And>p. \<lbrakk>x\<^sup>2 dvd \<Prod>(squarefree_part n); prime p\<rbrakk> \<Longrightarrow> multiplicity p x = multiplicity p 1
 3. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
fix p :: nat
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 2. \<And>p. \<lbrakk>x\<^sup>2 dvd \<Prod>(squarefree_part n); prime p\<rbrakk> \<Longrightarrow> multiplicity p x = multiplicity p 1
 3. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
assume p: "prime p"
[PROOF STATE]
proof (state)
this:
prime p

goal (3 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 2. \<And>p. \<lbrakk>x\<^sup>2 dvd \<Prod>(squarefree_part n); prime p\<rbrakk> \<Longrightarrow> multiplicity p x = multiplicity p 1
 3. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
from p x
[PROOF STATE]
proof (chain)
picking this:
prime p
0 < x
[PROOF STEP]
have "2 * multiplicity p x = multiplicity p (x^2)"
[PROOF STATE]
proof (prove)
using this:
prime p
0 < x

goal (1 subgoal):
 1. 2 * multiplicity p x = multiplicity p (x\<^sup>2)
[PROOF STEP]
by (simp add: multiplicity_power_nat)
[PROOF STATE]
proof (state)
this:
2 * multiplicity p x = multiplicity p (x\<^sup>2)

goal (3 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 2. \<And>p. \<lbrakk>x\<^sup>2 dvd \<Prod>(squarefree_part n); prime p\<rbrakk> \<Longrightarrow> multiplicity p x = multiplicity p 1
 3. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * multiplicity p x = multiplicity p (x\<^sup>2)

goal (3 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 2. \<And>p. \<lbrakk>x\<^sup>2 dvd \<Prod>(squarefree_part n); prime p\<rbrakk> \<Longrightarrow> multiplicity p x = multiplicity p 1
 3. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
from dvd
[PROOF STATE]
proof (chain)
picking this:
x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
have "\<dots> \<le> multiplicity p (\<Prod>(squarefree_part n))"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 dvd \<Prod>(squarefree_part n)

goal (1 subgoal):
 1. multiplicity p (x\<^sup>2) \<le> multiplicity p (\<Prod>(squarefree_part n))
[PROOF STEP]
by (intro dvd_imp_multiplicity_le) simp_all
[PROOF STATE]
proof (state)
this:
multiplicity p (x\<^sup>2) \<le> multiplicity p (\<Prod>(squarefree_part n))

goal (3 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 2. \<And>p. \<lbrakk>x\<^sup>2 dvd \<Prod>(squarefree_part n); prime p\<rbrakk> \<Longrightarrow> multiplicity p x = multiplicity p 1
 3. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity p (x\<^sup>2) \<le> multiplicity p (\<Prod>(squarefree_part n))

goal (3 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 2. \<And>p. \<lbrakk>x\<^sup>2 dvd \<Prod>(squarefree_part n); prime p\<rbrakk> \<Longrightarrow> multiplicity p x = multiplicity p 1
 3. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
have "\<dots> \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (\<Prod>(squarefree_part n)) \<le> 1
[PROOF STEP]
using multiplicity_squarefree_part[of p n] p
[PROOF STATE]
proof (prove)
using this:
prime p \<Longrightarrow> multiplicity p (\<Prod>(squarefree_part n)) = (if p \<in> squarefree_part n then 1 else 0)
prime p

goal (1 subgoal):
 1. multiplicity p (\<Prod>(squarefree_part n)) \<le> 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multiplicity p (\<Prod>(squarefree_part n)) \<le> 1

goal (3 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 2. \<And>p. \<lbrakk>x\<^sup>2 dvd \<Prod>(squarefree_part n); prime p\<rbrakk> \<Longrightarrow> multiplicity p x = multiplicity p 1
 3. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * multiplicity p x \<le> 1
[PROOF STEP]
show "multiplicity p x = multiplicity p 1"
[PROOF STATE]
proof (prove)
using this:
2 * multiplicity p x \<le> 1

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

goal (2 subgoals):
 1. x\<^sup>2 dvd \<Prod>(squarefree_part n) \<Longrightarrow> 0 < 1
 2. x = 1 \<Longrightarrow> x\<^sup>2 dvd \<Prod>(squarefree_part n)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma squarefree_decomposition_unique1:
  assumes "squarefree_part m = squarefree_part n"
  assumes "square_part m = square_part n"
  shows   "m = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m = n
[PROOF STEP]
by (subst (1 2) squarefree_decompose [symmetric]) (simp add: assms)


[STATEMENT]
lemma squarefree_decomposition_unique2:
  assumes n: "n > 0"
  assumes decomp: "n = (\<Prod>A2 * s2^2)"
  assumes prime: "\<And>x. x \<in> A2 \<Longrightarrow> prime x"
  assumes fin: "finite A2"
  assumes s2_nonneg: "s2 \<ge> 0"
  shows "A2 = squarefree_part n" and "s2 = square_part n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A2 = squarefree_part n &&& s2 = square_part n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
define A1 s1 where "A1 = squarefree_part n" and "s1 = square_part n"
[PROOF STATE]
proof (state)
this:
A1 = squarefree_part n
s1 = square_part n

goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
have "finite A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A1
[PROOF STEP]
unfolding A1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (squarefree_part n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite A1

goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
note fin = \<open>finite A1\<close> \<open>finite A2\<close>
[PROOF STATE]
proof (state)
this:
finite A1
finite A2

goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
have "A1 \<subseteq> prime_factors n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1 \<subseteq> prime_factors n
[PROOF STEP]
unfolding A1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. squarefree_part n \<subseteq> prime_factors n
[PROOF STEP]
using squarefree_part_subset
[PROOF STATE]
proof (prove)
using this:
squarefree_part ?n \<subseteq> prime_factors ?n

goal (1 subgoal):
 1. squarefree_part n \<subseteq> prime_factors n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A1 \<subseteq> prime_factors n

goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
note subset = this prime
[PROOF STATE]
proof (state)
this:
A1 \<subseteq> prime_factors n
?x \<in> A2 \<Longrightarrow> prime ?x

goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
have "\<Prod>A1 > 0" "\<Prod>A2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<Prod>A1 &&& 0 < \<Prod>A2
[PROOF STEP]
using subset(1)  prime_gt_0_nat
[PROOF STATE]
proof (prove)
using this:
A1 \<subseteq> prime_factors n
prime ?p \<Longrightarrow> 0 < ?p

goal (1 subgoal):
 1. 0 < \<Prod>A1 &&& 0 < \<Prod>A2
[PROOF STEP]
by (auto intro!: prod_pos dest: prime)
[PROOF STATE]
proof (state)
this:
0 < \<Prod>A1
0 < \<Prod>A2

goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have "s1 > 0"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. 0 < s1
[PROOF STEP]
unfolding s1_def
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. 0 < square_part n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < s1

goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
n = \<Prod>A2 * s2\<^sup>2
?x \<in> A2 \<Longrightarrow> prime ?x
finite A2
0 \<le> s2
[PROOF STEP]
have "s2 \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
0 < n
n = \<Prod>A2 * s2\<^sup>2
?x \<in> A2 \<Longrightarrow> prime ?x
finite A2
0 \<le> s2

goal (1 subgoal):
 1. s2 \<noteq> 0
[PROOF STEP]
by (intro notI) simp
[PROOF STATE]
proof (state)
this:
s2 \<noteq> 0

goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
hence "s2 > 0"
[PROOF STATE]
proof (prove)
using this:
s2 \<noteq> 0

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

goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
note pos = \<open>\<Prod>A1 > 0\<close> \<open>\<Prod>A2 > 0\<close> \<open>s1 > 0\<close> \<open>s2 > 0\<close>
[PROOF STATE]
proof (state)
this:
0 < \<Prod>A1
0 < \<Prod>A2
0 < s1
0 < s2

goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
have eq': "multiplicity p s1 = multiplicity p s2"
            "multiplicity p (\<Prod>A1) = multiplicity p (\<Prod>A2)"
    if   p: "prime p" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p s1 = multiplicity p s2 &&& multiplicity p (\<Prod>A1) = multiplicity p (\<Prod>A2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. multiplicity p s1 = multiplicity p s2
 2. multiplicity p (\<Prod>A1) = multiplicity p (\<Prod>A2)
[PROOF STEP]
define m where "m = multiplicity p"
[PROOF STATE]
proof (state)
this:
m = multiplicity p

goal (2 subgoals):
 1. multiplicity p s1 = multiplicity p s2
 2. multiplicity p (\<Prod>A1) = multiplicity p (\<Prod>A2)
[PROOF STEP]
from decomp
[PROOF STATE]
proof (chain)
picking this:
n = \<Prod>A2 * s2\<^sup>2
[PROOF STEP]
have "m (\<Prod>A1 * s1^2) = m (\<Prod>A2 * s2^2)"
[PROOF STATE]
proof (prove)
using this:
n = \<Prod>A2 * s2\<^sup>2

goal (1 subgoal):
 1. m (\<Prod>A1 * s1\<^sup>2) = m (\<Prod>A2 * s2\<^sup>2)
[PROOF STEP]
unfolding A1_def s1_def
[PROOF STATE]
proof (prove)
using this:
n = \<Prod>A2 * s2\<^sup>2

goal (1 subgoal):
 1. m (\<Prod>(squarefree_part n) * (square_part n)\<^sup>2) = m (\<Prod>A2 * s2\<^sup>2)
[PROOF STEP]
by (simp add: A1_def s1_def squarefree_decompose)
[PROOF STATE]
proof (state)
this:
m (\<Prod>A1 * s1\<^sup>2) = m (\<Prod>A2 * s2\<^sup>2)

goal (2 subgoals):
 1. multiplicity p s1 = multiplicity p s2
 2. multiplicity p (\<Prod>A1) = multiplicity p (\<Prod>A2)
[PROOF STEP]
with p pos
[PROOF STATE]
proof (chain)
picking this:
prime p
0 < \<Prod>A1
0 < \<Prod>A2
0 < s1
0 < s2
m (\<Prod>A1 * s1\<^sup>2) = m (\<Prod>A2 * s2\<^sup>2)
[PROOF STEP]
have eq: "m (\<Prod>A1) + 2 * m s1 = m (\<Prod>A2) + 2 * m s2"
[PROOF STATE]
proof (prove)
using this:
prime p
0 < \<Prod>A1
0 < \<Prod>A2
0 < s1
0 < s2
m (\<Prod>A1 * s1\<^sup>2) = m (\<Prod>A2 * s2\<^sup>2)

goal (1 subgoal):
 1. m (\<Prod>A1) + 2 * m s1 = m (\<Prod>A2) + 2 * m s2
[PROOF STEP]
by (simp add: m_def prime_elem_multiplicity_mult_distrib multiplicity_power_nat)
[PROOF STATE]
proof (state)
this:
m (\<Prod>A1) + 2 * m s1 = m (\<Prod>A2) + 2 * m s2

goal (2 subgoals):
 1. multiplicity p s1 = multiplicity p s2
 2. multiplicity p (\<Prod>A1) = multiplicity p (\<Prod>A2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m (\<Prod>A1) + 2 * m s1 = m (\<Prod>A2) + 2 * m s2

goal (2 subgoals):
 1. multiplicity p s1 = multiplicity p s2
 2. multiplicity p (\<Prod>A1) = multiplicity p (\<Prod>A2)
[PROOF STEP]
from fin subset p
[PROOF STATE]
proof (chain)
picking this:
finite A1
finite A2
A1 \<subseteq> prime_factors n
?x \<in> A2 \<Longrightarrow> prime ?x
prime p
[PROOF STEP]
have "m (\<Prod>A1) \<le> 1" "m (\<Prod>A2) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
finite A1
finite A2
A1 \<subseteq> prime_factors n
?x \<in> A2 \<Longrightarrow> prime ?x
prime p

goal (1 subgoal):
 1. m (\<Prod>A1) \<le> 1 &&& m (\<Prod>A2) \<le> 1
[PROOF STEP]
unfolding m_def
[PROOF STATE]
proof (prove)
using this:
finite A1
finite A2
A1 \<subseteq> prime_factors n
?x \<in> A2 \<Longrightarrow> prime ?x
prime p

goal (1 subgoal):
 1. multiplicity p (\<Prod>A1) \<le> 1 &&& multiplicity p (\<Prod>A2) \<le> 1
[PROOF STEP]
by ((subst multiplicity_prod_prime_powers_nat', auto)[])+
[PROOF STATE]
proof (state)
this:
m (\<Prod>A1) \<le> 1
m (\<Prod>A2) \<le> 1

goal (2 subgoals):
 1. multiplicity p s1 = multiplicity p s2
 2. multiplicity p (\<Prod>A1) = multiplicity p (\<Prod>A2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m (\<Prod>A1) + 2 * m s1 = m (\<Prod>A2) + 2 * m s2
m (\<Prod>A1) \<le> 1
m (\<Prod>A2) \<le> 1
[PROOF STEP]
show "m s1 = m s2"
[PROOF STATE]
proof (prove)
using this:
m (\<Prod>A1) + 2 * m s1 = m (\<Prod>A2) + 2 * m s2
m (\<Prod>A1) \<le> 1
m (\<Prod>A2) \<le> 1

goal (1 subgoal):
 1. m s1 = m s2
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
m s1 = m s2

goal (1 subgoal):
 1. multiplicity p (\<Prod>A1) = multiplicity p (\<Prod>A2)
[PROOF STEP]
with eq
[PROOF STATE]
proof (chain)
picking this:
m (\<Prod>A1) + 2 * m s1 = m (\<Prod>A2) + 2 * m s2
m s1 = m s2
[PROOF STEP]
show "m (\<Prod>A1) = m (\<Prod>A2)"
[PROOF STATE]
proof (prove)
using this:
m (\<Prod>A1) + 2 * m s1 = m (\<Prod>A2) + 2 * m s2
m s1 = m s2

goal (1 subgoal):
 1. m (\<Prod>A1) = m (\<Prod>A2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m (\<Prod>A1) = m (\<Prod>A2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime ?p \<Longrightarrow> multiplicity ?p s1 = multiplicity ?p s2
prime ?p \<Longrightarrow> multiplicity ?p (\<Prod>A1) = multiplicity ?p (\<Prod>A2)

goal (2 subgoals):
 1. A2 = squarefree_part n
 2. s2 = square_part n
[PROOF STEP]
show "s2 = square_part n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2 = square_part n
[PROOF STEP]
by (rule multiplicity_eq_nat) (insert pos eq'(1), auto simp: s1_def)
[PROOF STATE]
proof (state)
this:
s2 = square_part n

goal (1 subgoal):
 1. A2 = squarefree_part n
[PROOF STEP]
have "\<Prod>A2 = \<Prod>(squarefree_part n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Prod>A2 = \<Prod>(squarefree_part n)
[PROOF STEP]
by (rule multiplicity_eq_nat) (insert pos eq'(2), auto simp: A1_def)
[PROOF STATE]
proof (state)
this:
\<Prod>A2 = \<Prod>(squarefree_part n)

goal (1 subgoal):
 1. A2 = squarefree_part n
[PROOF STEP]
with fin subset
[PROOF STATE]
proof (chain)
picking this:
finite A1
finite A2
A1 \<subseteq> prime_factors n
?x \<in> A2 \<Longrightarrow> prime ?x
\<Prod>A2 = \<Prod>(squarefree_part n)
[PROOF STEP]
show "A2 = squarefree_part n"
[PROOF STATE]
proof (prove)
using this:
finite A1
finite A2
A1 \<subseteq> prime_factors n
?x \<in> A2 \<Longrightarrow> prime ?x
\<Prod>A2 = \<Prod>(squarefree_part n)

goal (1 subgoal):
 1. A2 = squarefree_part n
[PROOF STEP]
unfolding A1_def
[PROOF STATE]
proof (prove)
using this:
finite (squarefree_part n)
finite A2
squarefree_part n \<subseteq> prime_factors n
?x \<in> A2 \<Longrightarrow> prime ?x
\<Prod>A2 = \<Prod>(squarefree_part n)

goal (1 subgoal):
 1. A2 = squarefree_part n
[PROOF STEP]
by (intro prod_prime_eq) auto
[PROOF STATE]
proof (state)
this:
A2 = squarefree_part n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma squarefree_decomposition_unique2':
  assumes decomp: "(\<Prod>A1 * s1^2) = (\<Prod>A2 * s2^2 :: nat)"
  assumes fin: "finite A1" "finite A2"
  assumes subset: "\<And>x. x \<in> A1 \<Longrightarrow> prime x" "\<And>x. x \<in> A2 \<Longrightarrow> prime x"
  assumes pos: "s1 > 0" "s2 > 0"
  defines "n \<equiv> \<Prod>A1 * s1^2"
  shows "A1 = A2" "s1 = s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1 = A2 &&& s1 = s2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A1 = A2
 2. s1 = s2
[PROOF STEP]
from pos
[PROOF STATE]
proof (chain)
picking this:
0 < s1
0 < s2
[PROOF STEP]
have n: "n > 0"
[PROOF STATE]
proof (prove)
using this:
0 < s1
0 < s2

goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
using prime_gt_0_nat
[PROOF STATE]
proof (prove)
using this:
0 < s1
0 < s2
prime ?p \<Longrightarrow> 0 < ?p

goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
by (auto simp: n_def intro!: prod_pos dest: subset)
[PROOF STATE]
proof (state)
this:
0 < n

goal (2 subgoals):
 1. A1 = A2
 2. s1 = s2
[PROOF STEP]
have "A1 = squarefree_part n" "s1 = square_part n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1 = squarefree_part n &&& s1 = square_part n
[PROOF STEP]
by ((rule squarefree_decomposition_unique2[of n A1 s1], insert assms n, simp_all)[])+
[PROOF STATE]
proof (state)
this:
A1 = squarefree_part n
s1 = square_part n

goal (2 subgoals):
 1. A1 = A2
 2. s1 = s2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A1 = squarefree_part n
s1 = square_part n

goal (2 subgoals):
 1. A1 = A2
 2. s1 = s2
[PROOF STEP]
have "A2 = squarefree_part n" "s2 = square_part n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A2 = squarefree_part n &&& s2 = square_part n
[PROOF STEP]
by ((rule squarefree_decomposition_unique2[of n A2 s2], insert assms n, simp_all)[])+
[PROOF STATE]
proof (state)
this:
A2 = squarefree_part n
s2 = square_part n

goal (2 subgoals):
 1. A1 = A2
 2. s1 = s2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A1 = squarefree_part n
s1 = square_part n
A2 = squarefree_part n
s2 = square_part n
[PROOF STEP]
show "A1 = A2" "s1 = s2"
[PROOF STATE]
proof (prove)
using this:
A1 = squarefree_part n
s1 = square_part n
A2 = squarefree_part n
s2 = square_part n

goal (1 subgoal):
 1. A1 = A2 &&& s1 = s2
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
A1 = A2
s1 = s2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma primes_lower_bound:
  fixes n :: nat
  assumes "n > 0"
  defines "\<pi> \<equiv> \<lambda>n. card {p. prime p \<and> p \<le> n}"
  shows   "real (\<pi> n) \<ge> ln (real n) / ln 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
have "real n = real (card {1..n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real n = real (card {1..n})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real n = real (card {1..n})

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real n = real (card {1..n})

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
have "{1..n} = (\<lambda>(A, b). \<Prod>A * b^2) ` (\<lambda>n. (squarefree_part n, square_part n)) ` {1..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {1..n} = (\<lambda>(A, b). \<Prod>A * b\<^sup>2) ` (\<lambda>n. (squarefree_part n, square_part n)) ` {1..n}
[PROOF STEP]
unfolding image_comp o_def squarefree_decompose case_prod_unfold fst_conv snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {1..n} = (\<lambda>x. x) ` {1..n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{1..n} = (\<lambda>(A, b). \<Prod>A * b\<^sup>2) ` (\<lambda>n. (squarefree_part n, square_part n)) ` {1..n}

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{1..n} = (\<lambda>(A, b). \<Prod>A * b\<^sup>2) ` (\<lambda>n. (squarefree_part n, square_part n)) ` {1..n}

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
have "card \<dots> \<le> card ((\<lambda>n. (squarefree_part n, square_part n)) ` {1..n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>(A, b). \<Prod>A * b\<^sup>2) ` (\<lambda>n. (squarefree_part n, square_part n)) ` {1..n}) \<le> card ((\<lambda>n. (squarefree_part n, square_part n)) ` {1..n})
[PROOF STEP]
by (rule card_image_le) simp_all
[PROOF STATE]
proof (state)
this:
card ((\<lambda>(A, b). \<Prod>A * b\<^sup>2) ` (\<lambda>n. (squarefree_part n, square_part n)) ` {1..n}) \<le> card ((\<lambda>n. (squarefree_part n, square_part n)) ` {1..n})

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ((\<lambda>(A, b). \<Prod>A * b\<^sup>2) ` (\<lambda>n. (squarefree_part n, square_part n)) ` {1..n}) \<le> card ((\<lambda>n. (squarefree_part n, square_part n)) ` {1..n})

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
have "\<dots> \<le> card (squarefree_part ` {1..n} \<times> square_part ` {1..n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>n. (squarefree_part n, square_part n)) ` {1..n}) \<le> card (squarefree_part ` {1..n} \<times> square_part ` {1..n})
[PROOF STEP]
by (rule card_mono) auto
[PROOF STATE]
proof (state)
this:
card ((\<lambda>n. (squarefree_part n, square_part n)) ` {1..n}) \<le> card (squarefree_part ` {1..n} \<times> square_part ` {1..n})

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ((\<lambda>n. (squarefree_part n, square_part n)) ` {1..n}) \<le> card (squarefree_part ` {1..n} \<times> square_part ` {1..n})

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
have "real \<dots> = real (card (squarefree_part ` {1..n})) * real (card (square_part ` {1..n}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (card (squarefree_part ` {1..n} \<times> square_part ` {1..n})) = real (card (squarefree_part ` {1..n})) * real (card (square_part ` {1..n}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (card (squarefree_part ` {1..n} \<times> square_part ` {1..n})) = real (card (squarefree_part ` {1..n})) * real (card (square_part ` {1..n}))

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (card (squarefree_part ` {1..n} \<times> square_part ` {1..n})) = real (card (squarefree_part ` {1..n})) * real (card (square_part ` {1..n}))

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
have "\<dots> \<le> 2 ^ \<pi> n * sqrt (real n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (card (squarefree_part ` {1..n})) * real (card (square_part ` {1..n})) \<le> 2 ^ \<pi> n * sqrt (real n)
[PROOF STEP]
proof (rule mult_mono)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. real (card (squarefree_part ` {1..n})) \<le> 2 ^ \<pi> n
 2. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 3. 0 \<le> 2 ^ \<pi> n
 4. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
have "card (squarefree_part ` {1..n}) \<le> card (Pow {p. prime p \<and> p \<le> n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (squarefree_part ` {1..n}) \<le> card (Pow {p. prime p \<and> p \<le> n})
[PROOF STEP]
using squarefree_part_subset squarefree_part_le
[PROOF STATE]
proof (prove)
using this:
squarefree_part ?n \<subseteq> prime_factors ?n
?p \<in> squarefree_part ?n \<Longrightarrow> ?p \<le> ?n

goal (1 subgoal):
 1. card (squarefree_part ` {1..n}) \<le> card (Pow {p. prime p \<and> p \<le> n})
[PROOF STEP]
by (intro card_mono) force+
[PROOF STATE]
proof (state)
this:
card (squarefree_part ` {1..n}) \<le> card (Pow {p. prime p \<and> p \<le> n})

goal (4 subgoals):
 1. real (card (squarefree_part ` {1..n})) \<le> 2 ^ \<pi> n
 2. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 3. 0 \<le> 2 ^ \<pi> n
 4. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (squarefree_part ` {1..n}) \<le> card (Pow {p. prime p \<and> p \<le> n})

goal (4 subgoals):
 1. real (card (squarefree_part ` {1..n})) \<le> 2 ^ \<pi> n
 2. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 3. 0 \<le> 2 ^ \<pi> n
 4. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
have "real \<dots> = 2 ^ \<pi> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (card (Pow {p. prime p \<and> p \<le> n})) = 2 ^ \<pi> n
[PROOF STEP]
by (simp add: \<pi>_def card_Pow)
[PROOF STATE]
proof (state)
this:
real (card (Pow {p. prime p \<and> p \<le> n})) = 2 ^ \<pi> n

goal (4 subgoals):
 1. real (card (squarefree_part ` {1..n})) \<le> 2 ^ \<pi> n
 2. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 3. 0 \<le> 2 ^ \<pi> n
 4. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y) \<Longrightarrow> real (card (squarefree_part ` {1..n})) \<le> 2 ^ \<pi> n
[PROOF STEP]
show "real (card (squarefree_part ` {1..n})) \<le> 2 ^ \<pi> n"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y) \<Longrightarrow> real (card (squarefree_part ` {1..n})) \<le> 2 ^ \<pi> n

goal (1 subgoal):
 1. real (card (squarefree_part ` {1..n})) \<le> 2 ^ \<pi> n
[PROOF STEP]
by - simp_all
[PROOF STATE]
proof (state)
this:
real (card (squarefree_part ` {1..n})) \<le> 2 ^ \<pi> n

goal (3 subgoals):
 1. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 2. 0 \<le> 2 ^ \<pi> n
 3. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 2. 0 \<le> 2 ^ \<pi> n
 3. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
have "square_part k \<le> nat \<lfloor>sqrt n\<rfloor>" if "k \<le> n" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_part k \<le> nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
by (rule order.trans[OF square_part_le_sqrt])
         (insert that, auto intro!: nat_mono floor_mono)
[PROOF STATE]
proof (state)
this:
?k \<le> n \<Longrightarrow> square_part ?k \<le> nat \<lfloor>sqrt (real n)\<rfloor>

goal (3 subgoals):
 1. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 2. 0 \<le> 2 ^ \<pi> n
 3. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
hence "card (square_part ` {1..n}) \<le> card {1..nat \<lfloor>sqrt n\<rfloor>}"
[PROOF STATE]
proof (prove)
using this:
?k \<le> n \<Longrightarrow> square_part ?k \<le> nat \<lfloor>sqrt (real n)\<rfloor>

goal (1 subgoal):
 1. card (square_part ` {1..n}) \<le> card {1..nat \<lfloor>sqrt (real n)\<rfloor>}
[PROOF STEP]
by (intro card_mono) (auto intro: order.trans[OF square_part_le_sqrt])
[PROOF STATE]
proof (state)
this:
card (square_part ` {1..n}) \<le> card {1..nat \<lfloor>sqrt (real n)\<rfloor>}

goal (3 subgoals):
 1. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 2. 0 \<le> 2 ^ \<pi> n
 3. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (square_part ` {1..n}) \<le> card {1..nat \<lfloor>sqrt (real n)\<rfloor>}

goal (3 subgoals):
 1. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 2. 0 \<le> 2 ^ \<pi> n
 3. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
have "\<dots> = nat \<lfloor>sqrt n\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {1..nat \<lfloor>sqrt (real n)\<rfloor>} = nat \<lfloor>sqrt (real n)\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {1..nat \<lfloor>sqrt (real n)\<rfloor>} = nat \<lfloor>sqrt (real n)\<rfloor>

goal (3 subgoals):
 1. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 2. 0 \<le> 2 ^ \<pi> n
 3. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {1..nat \<lfloor>sqrt (real n)\<rfloor>} = nat \<lfloor>sqrt (real n)\<rfloor>

goal (3 subgoals):
 1. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 2. 0 \<le> 2 ^ \<pi> n
 3. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
have "real \<dots> \<le> sqrt n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (nat \<lfloor>sqrt (real n)\<rfloor>) \<le> sqrt (real n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (nat \<lfloor>sqrt (real n)\<rfloor>) \<le> sqrt (real n)

goal (3 subgoals):
 1. real (card (square_part ` {1..n})) \<le> sqrt (real n)
 2. 0 \<le> 2 ^ \<pi> n
 3. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y) \<Longrightarrow> real (card (square_part ` {1..n})) \<le> sqrt (real n)
[PROOF STEP]
show "real (card (square_part ` {1..n})) \<le> sqrt (real n)"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y) \<Longrightarrow> real (card (square_part ` {1..n})) \<le> sqrt (real n)

goal (1 subgoal):
 1. real (card (square_part ` {1..n})) \<le> sqrt (real n)
[PROOF STEP]
by - simp_all
[PROOF STATE]
proof (state)
this:
real (card (square_part ` {1..n})) \<le> sqrt (real n)

goal (2 subgoals):
 1. 0 \<le> 2 ^ \<pi> n
 2. 0 \<le> real (card (square_part ` {1..n}))
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
real (card (squarefree_part ` {1..n})) * real (card (square_part ` {1..n})) \<le> 2 ^ \<pi> n * sqrt (real n)

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y; \<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y\<rbrakk> \<Longrightarrow> real n \<le> 2 ^ \<pi> n * sqrt (real n)
[PROOF STEP]
have "real n \<le> 2 ^ \<pi> n * sqrt (real n)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y; \<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y\<rbrakk> \<Longrightarrow> real n \<le> 2 ^ \<pi> n * sqrt (real n)

goal (1 subgoal):
 1. real n \<le> 2 ^ \<pi> n * sqrt (real n)
[PROOF STEP]
by - simp_all
[PROOF STATE]
proof (state)
this:
real n \<le> 2 ^ \<pi> n * sqrt (real n)

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
with \<open>n > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < n
real n \<le> 2 ^ \<pi> n * sqrt (real n)
[PROOF STEP]
have "ln (real n) \<le> ln (2 ^ \<pi> n * sqrt (real n))"
[PROOF STATE]
proof (prove)
using this:
0 < n
real n \<le> 2 ^ \<pi> n * sqrt (real n)

goal (1 subgoal):
 1. ln (real n) \<le> ln (2 ^ \<pi> n * sqrt (real n))
[PROOF STEP]
by (subst ln_le_cancel_iff) simp_all
[PROOF STATE]
proof (state)
this:
ln (real n) \<le> ln (2 ^ \<pi> n * sqrt (real n))

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ln (real n) \<le> ln (2 ^ \<pi> n * sqrt (real n))

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
have "ln (4 :: real) = real 2 * ln 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln 4 = real 2 * ln 2
[PROOF STEP]
by (subst ln_realpow [symmetric]) simp_all
[PROOF STATE]
proof (state)
this:
ln 4 = real 2 * ln 2

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ln (real n) \<le> ln (2 ^ \<pi> n * sqrt (real n))
ln 4 = real 2 * ln 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ln (real n) \<le> ln (2 ^ \<pi> n * sqrt (real n))
ln 4 = real 2 * ln 2

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
using \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
ln (real n) \<le> ln (2 ^ \<pi> n * sqrt (real n))
ln 4 = real 2 * ln 2
0 < n

goal (1 subgoal):
 1. ln (real n) / ln 4 \<le> real (\<pi> n)
[PROOF STEP]
by (simp add: ln_mult ln_realpow[of _ "\<pi> n"] ln_sqrt field_simps)
[PROOF STATE]
proof (state)
this:
ln (real n) / ln 4 \<le> real (\<pi> n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nub_strict[simp]: "nub\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nub\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma nub_nub_body_eq: "nub = fix\<cdot>nub_body"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nub = fix\<cdot>nub_body
[PROOF STEP]
by (rule cfun_eqI, subst nub_def, subst nub_body.unfold, simp)


[STATEMENT]
lemma SetMem_strict[simp]: "SetMem\<cdot>x\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SetMem\<cdot>x\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (simp add: SetMem_def)


[STATEMENT]
lemma SetMem_SetEmpty[simp]: "SetMem\<cdot>x\<cdot>SetEmpty = FF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SetMem\<cdot>x\<cdot>SetEmpty = FF
[PROOF STEP]
by (simp add: SetMem_def SetEmpty_def)


[STATEMENT]
lemma SetMem_SetInsert: "SetMem\<cdot>v\<cdot>(SetInsert\<cdot>x\<cdot>s) = (SetMem\<cdot>v\<cdot>s orelse x =\<^sub>B v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SetMem\<cdot>v\<cdot>(SetInsert\<cdot>x\<cdot>s) = (SetMem\<cdot>v\<cdot>s orelse x =\<^sub>B v)
[PROOF STEP]
by (simp add: SetMem_def SetInsert_def)


[STATEMENT]
lemma nextR_strict1[simp]: "nextR\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nextR\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (simp add: nextR_def)


[STATEMENT]
lemma nextR_strict2[simp]: "nextR\<cdot>(R\<cdot>\<bottom>\<cdot>S) = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nextR\<cdot>(R\<cdot>\<bottom>\<cdot>S) = \<bottom>
[PROOF STEP]
by (simp add: nextR_def)


[STATEMENT]
lemma nextR_lnil[simp]: "nextR\<cdot>(R\<cdot>lnil\<cdot>S) = Nothing"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nextR\<cdot>(R\<cdot>lnil\<cdot>S) = Nothing
[PROOF STEP]
by (simp add: nextR_def)


[STATEMENT]
lemma a2c_strict[simp]: "a2c\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a2c\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
unfolding a2c_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> r. lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>r)))\<cdot>(resultR\<cdot>r))\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by simp


[STATEMENT]
lemma a2c_c2a_id: "a2c oo c2a = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a2c oo c2a = ID
[PROOF STEP]
by (rule cfun_eqI, simp add: a2c_def c2a_def lfilter_const_true)


[STATEMENT]
lemma unwrap_strict[simp]: "unwrap\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unwrap\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
unfolding unwrap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> f r. f\<cdot>(a2c\<cdot>r))\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (rule cfun_eqI, simp)


[STATEMENT]
lemma wrap_unwrap_id: "wrap oo unwrap = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrap oo unwrap = ID
[PROOF STEP]
using cfun_fun_cong[OF a2c_c2a_id]
[PROOF STATE]
proof (prove)
using this:
(a2c oo c2a)\<cdot>?x = ID\<cdot>?x

goal (1 subgoal):
 1. wrap oo unwrap = ID
[PROOF STEP]
by - ((rule cfun_eqI)+, simp add: wrap_def unwrap_def)


[STATEMENT]
lemma TR_deMorgan: "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 (rule trE[where p=x], simp_all)


[STATEMENT]
lemma case_maybe_case:
  "(case (case L of lnil \<Rightarrow> Nothing | x :@ xs \<Rightarrow> Just\<cdot>(h\<cdot>x\<cdot>xs)) of
     Nothing \<Rightarrow> f | Just\<cdot>(a, b) \<Rightarrow> g\<cdot>a\<cdot>b)
   =
   (case L of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>(fst (h\<cdot>x\<cdot>xs))\<cdot>(snd (h\<cdot>x\<cdot>xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case case L of lnil \<Rightarrow> Nothing | x :@ xs \<Rightarrow> Just\<cdot>(h\<cdot>x\<cdot>xs) of Nothing \<Rightarrow> f | Just\<cdot>(a, b) \<Rightarrow> g\<cdot>a\<cdot>b) = (case L of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>(fst (h\<cdot>x\<cdot>xs))\<cdot>(snd (h\<cdot>x\<cdot>xs)))
[PROOF STEP]
apply (cases L, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a llist. L = a :@ llist \<Longrightarrow> csplit\<cdot>(\<Lambda> a. Abs_cfun (Rep_cfun (g\<cdot>a)))\<cdot>(h\<cdot>a\<cdot>llist) = g\<cdot>(fst (h\<cdot>a\<cdot>llist))\<cdot>(snd (h\<cdot>a\<cdot>llist))
[PROOF STEP]
apply (case_tac "h\<cdot>a\<cdot>llist")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a llist aa b. \<lbrakk>L = a :@ llist; h\<cdot>a\<cdot>llist = (aa, b)\<rbrakk> \<Longrightarrow> csplit\<cdot>(\<Lambda> a. Abs_cfun (Rep_cfun (g\<cdot>a)))\<cdot>(h\<cdot>a\<cdot>llist) = g\<cdot>(fst (h\<cdot>a\<cdot>llist))\<cdot>(snd (h\<cdot>a\<cdot>llist))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma case_a2c_case_caseR:
    "(case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
   = (case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs) = (case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs) = (case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))
[PROOF STEP]
have "?rhs = (case (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of
                     lnil \<Rightarrow> Nothing
                   | x :@ xs \<Rightarrow> Just\<cdot>(x, R\<cdot>xs\<cdot>(exceptR\<cdot>w))) of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r)) = (case case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> Nothing | x :@ xs \<Rightarrow> Just\<cdot>(x, R\<cdot>xs\<cdot>(exceptR\<cdot>w)) of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))
[PROOF STEP]
by (simp add: nextR_def)
[PROOF STATE]
proof (state)
this:
(case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r)) = (case case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> Nothing | x :@ xs \<Rightarrow> Just\<cdot>(x, R\<cdot>xs\<cdot>(exceptR\<cdot>w)) of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))

goal (1 subgoal):
 1. (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs) = (case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r)) = (case case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> Nothing | x :@ xs \<Rightarrow> Just\<cdot>(x, R\<cdot>xs\<cdot>(exceptR\<cdot>w)) of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))

goal (1 subgoal):
 1. (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs) = (case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))
[PROOF STEP]
have "\<dots> = (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of
                     lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>(R\<cdot>xs\<cdot>(exceptR\<cdot>w))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> Nothing | x :@ xs \<Rightarrow> Just\<cdot>(x, R\<cdot>xs\<cdot>(exceptR\<cdot>w)) of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r)) = (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>(R\<cdot>xs\<cdot>(exceptR\<cdot>w))))
[PROOF STEP]
using case_maybe_case[where L="ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w)"
                            and f=f and g="\<Lambda> x r. g\<cdot>x\<cdot>(a2c\<cdot>r)" and h="\<Lambda> x xs. (x, R\<cdot>xs\<cdot>(exceptR\<cdot>w))"]
[PROOF STATE]
proof (prove)
using this:
(case case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> Nothing | x :@ xs \<Rightarrow> Just\<cdot>((\<Lambda> x xs. (x, R\<cdot>xs\<cdot>(exceptR\<cdot>w)))\<cdot>x\<cdot>xs) of Nothing \<Rightarrow> f | Just\<cdot>(a, b) \<Rightarrow> (\<Lambda> x r. g\<cdot>x\<cdot>(a2c\<cdot>r))\<cdot>a\<cdot>b) = (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> (\<Lambda> x r. g\<cdot>x\<cdot>(a2c\<cdot>r))\<cdot>(fst ((\<Lambda> x xs. (x, R\<cdot>xs\<cdot>(exceptR\<cdot>w)))\<cdot>x\<cdot>xs))\<cdot>(snd ((\<Lambda> x xs. (x, R\<cdot>xs\<cdot>(exceptR\<cdot>w)))\<cdot>x\<cdot>xs)))

goal (1 subgoal):
 1. (case case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> Nothing | x :@ xs \<Rightarrow> Just\<cdot>(x, R\<cdot>xs\<cdot>(exceptR\<cdot>w)) of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r)) = (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>(R\<cdot>xs\<cdot>(exceptR\<cdot>w))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(case case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> Nothing | x :@ xs \<Rightarrow> Just\<cdot>(x, R\<cdot>xs\<cdot>(exceptR\<cdot>w)) of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r)) = (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>(R\<cdot>xs\<cdot>(exceptR\<cdot>w))))

goal (1 subgoal):
 1. (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs) = (case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(case case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> Nothing | x :@ xs \<Rightarrow> Just\<cdot>(x, R\<cdot>xs\<cdot>(exceptR\<cdot>w)) of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r)) = (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>(R\<cdot>xs\<cdot>(exceptR\<cdot>w))))

goal (1 subgoal):
 1. (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs) = (case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))
[PROOF STEP]
have "\<dots> = ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>(R\<cdot>xs\<cdot>(exceptR\<cdot>w)))) = (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
[PROOF STEP]
apply (simp add: a2c_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
[PROOF STEP]
apply (cases "resultR\<cdot>w")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. resultR\<cdot>w = \<bottom> \<Longrightarrow> (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
 2. resultR\<cdot>w = lnil \<Longrightarrow> (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
 3. \<And>a llist. resultR\<cdot>w = a :@ llist \<Longrightarrow> (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a llist. resultR\<cdot>w = a :@ llist \<Longrightarrow> (case If SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) then ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llist else a :@ llist of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case If neg\<cdot>(SetMem\<cdot>a\<cdot>(exceptR\<cdot>w)) then a :@ lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llist else lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llist of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
[PROOF STEP]
apply (rule_tac p="SetMem\<cdot>a\<cdot>(exceptR\<cdot>w)" in trE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a llist. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = \<bottom>\<rbrakk> \<Longrightarrow> (case If SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) then ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llist else a :@ llist of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case If neg\<cdot>(SetMem\<cdot>a\<cdot>(exceptR\<cdot>w)) then a :@ lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llist else lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llist of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
 2. \<And>a llist. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = TT\<rbrakk> \<Longrightarrow> (case If SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) then ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llist else a :@ llist of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case If neg\<cdot>(SetMem\<cdot>a\<cdot>(exceptR\<cdot>w)) then a :@ lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llist else lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llist of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
 3. \<And>a llist. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = FF\<rbrakk> \<Longrightarrow> (case If SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) then ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llist else a :@ llist of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case If neg\<cdot>(SetMem\<cdot>a\<cdot>(exceptR\<cdot>w)) then a :@ lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llist else lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llist of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a llist. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = TT\<rbrakk> \<Longrightarrow> (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llist of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llist of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
[PROOF STEP]
apply (induct_tac llist)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a llist. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = TT\<rbrakk> \<Longrightarrow> adm (\<lambda>a. (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>a of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>a of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs))
 2. \<And>a llist. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = TT\<rbrakk> \<Longrightarrow> (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>\<bottom> of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>\<bottom> of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
 3. \<And>a llist. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = TT\<rbrakk> \<Longrightarrow> (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>lnil of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>lnil of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
 4. \<And>a llist aa llista. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = TT; (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)\<rbrakk> \<Longrightarrow> (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(aa :@ llista) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>(aa :@ llista) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a llist aa llista. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = TT; (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)\<rbrakk> \<Longrightarrow> (case If SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w) then ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llista else aa :@ llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case If neg\<cdot>(SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w)) then aa :@ lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista else lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
[PROOF STEP]
apply (rule_tac p="SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w)" in trE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a llist aa llista. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = TT; (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs); SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w) = \<bottom>\<rbrakk> \<Longrightarrow> (case If SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w) then ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llista else aa :@ llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case If neg\<cdot>(SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w)) then aa :@ lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista else lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
 2. \<And>a llist aa llista. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = TT; (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs); SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w) = TT\<rbrakk> \<Longrightarrow> (case If SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w) then ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llista else aa :@ llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case If neg\<cdot>(SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w)) then aa :@ lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista else lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
 3. \<And>a llist aa llista. \<lbrakk>resultR\<cdot>w = a :@ llist; SetMem\<cdot>a\<cdot>(exceptR\<cdot>w) = TT; (case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs); SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w) = FF\<rbrakk> \<Longrightarrow> (case If SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w) then ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>llista else aa :@ llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>xs)) = (case If neg\<cdot>(SetMem\<cdot>aa\<cdot>(exceptR\<cdot>w)) then aa :@ lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista else lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>w)))\<cdot>llista of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(case ldropWhile\<cdot>(\<Lambda> x. SetMem\<cdot>x\<cdot>(exceptR\<cdot>w))\<cdot>(resultR\<cdot>w) of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>(R\<cdot>xs\<cdot>(exceptR\<cdot>w)))) = (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)

goal (1 subgoal):
 1. (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs) = (case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r)) = (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)
[PROOF STEP]
show "?lhs = ?rhs"
[PROOF STATE]
proof (prove)
using this:
(case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r)) = (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs)

goal (1 subgoal):
 1. (case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs) = (case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(case a2c\<cdot>w of lnil \<Rightarrow> f | x :@ xs \<Rightarrow> g\<cdot>x\<cdot>xs) = (case nextR\<cdot>w of Nothing \<Rightarrow> f | Just\<cdot>(x, r) \<Rightarrow> g\<cdot>x\<cdot>(a2c\<cdot>r))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma filter_filterR: "lfilter\<cdot>(neg oo (\<Lambda> y. x =\<^sub>B y))\<cdot>(a2c\<cdot>r) = a2c\<cdot>(filterR\<cdot>x\<cdot>r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>(a2c\<cdot>r) = a2c\<cdot>(filterR\<cdot>x\<cdot>r)
[PROOF STEP]
using filter_filter[where p="Tr.neg oo (\<Lambda> y. x =\<^sub>B y)" and q="\<Lambda> v. Tr.neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>r))"]
[PROOF STATE]
proof (prove)
using this:
lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>r)))\<cdot>?xs) = lfilter\<cdot>(\<Lambda> xa. (\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>r)))\<cdot>xa andalso (neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>xa)\<cdot>?xs

goal (1 subgoal):
 1. lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>(a2c\<cdot>r) = a2c\<cdot>(filterR\<cdot>x\<cdot>r)
[PROOF STEP]
unfolding a2c_def filterR_def
[PROOF STATE]
proof (prove)
using this:
lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>(lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>r)))\<cdot>?xs) = lfilter\<cdot>(\<Lambda> xa. (\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>r)))\<cdot>xa andalso (neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>xa)\<cdot>?xs

goal (1 subgoal):
 1. lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>((\<Lambda> r. lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>r)))\<cdot>(resultR\<cdot>r))\<cdot>r) = (\<Lambda> r. lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>r)))\<cdot>(resultR\<cdot>r))\<cdot>((\<Lambda> v r. R\<cdot>(resultR\<cdot>r)\<cdot>(SetInsert\<cdot>v\<cdot>(exceptR\<cdot>r)))\<cdot>x\<cdot>r)
[PROOF STEP]
by (cases r, simp_all add: SetMem_SetInsert TR_deMorgan)


[STATEMENT]
lemma nub_body_nub_body'_eq: "unwrap oo nub_body oo wrap = nub_body'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unwrap oo nub_body oo wrap = nub_body'
[PROOF STEP]
unfolding nub_body_def nub_body'_def unwrap_def wrap_def a2c_def c2a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> f r. f\<cdot>((\<Lambda> r. lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>r)))\<cdot>(resultR\<cdot>r))\<cdot>r)) oo (\<mu> nub_body. \<Lambda> f v. Fixrec.run\<cdot>(match_lnil\<cdot>v\<cdot>(Fixrec.succeed\<cdot>lnil) +++ match_lcons\<cdot>v\<cdot>(\<Lambda> x xs. Fixrec.succeed\<cdot>(x :@ f\<cdot>(lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>xs))))) oo (\<Lambda> f xs. f\<cdot>((\<Lambda> xs. R\<cdot>xs\<cdot>SetEmpty)\<cdot>xs)) = (\<Lambda> f r. case (\<Lambda> r. lfilter\<cdot>(\<Lambda> v. neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>r)))\<cdot>(resultR\<cdot>r))\<cdot>r of lnil \<Rightarrow> lnil | x :@ xs \<Rightarrow> x :@ f\<cdot>((\<Lambda> xs. R\<cdot>xs\<cdot>SetEmpty)\<cdot>(lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>xs)))
[PROOF STEP]
by ((rule cfun_eqI)+
     , case_tac "lfilter\<cdot>(\<Lambda> v. Tr.neg\<cdot>(SetMem\<cdot>v\<cdot>(exceptR\<cdot>xa)))\<cdot>(resultR\<cdot>xa)"
     , simp_all add: fix_const)


[STATEMENT]
lemma nub_body'_nub_body''_eq: "nub_body' = nub_body''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nub_body' = nub_body''
[PROOF STEP]
proof(rule cfun_eqI)+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. nub_body'\<cdot>x\<cdot>xa = nub_body''\<cdot>x\<cdot>xa
[PROOF STEP]
fix f r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. nub_body'\<cdot>x\<cdot>xa = nub_body''\<cdot>x\<cdot>xa
[PROOF STEP]
show "nub_body'\<cdot>f\<cdot>r = nub_body''\<cdot>f\<cdot>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nub_body'\<cdot>f\<cdot>r = nub_body''\<cdot>f\<cdot>r
[PROOF STEP]
unfolding nub_body'_def nub_body''_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> f r. case a2c\<cdot>r of lnil \<Rightarrow> lnil | x :@ xs \<Rightarrow> x :@ f\<cdot>(c2a\<cdot>(lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>xs)))\<cdot>f\<cdot>r = (\<Lambda> f r. case nextR\<cdot>r of Nothing \<Rightarrow> lnil | Just\<cdot>(x, xs) \<Rightarrow> x :@ f\<cdot>(c2a\<cdot>(lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>(a2c\<cdot>xs))))\<cdot>f\<cdot>r
[PROOF STEP]
using case_a2c_case_caseR[where f="lnil" and g="\<Lambda> x xs. x :@ f\<cdot>(c2a\<cdot>(lfilter\<cdot>(Tr.neg oo (\<Lambda> y. x =\<^sub>B y))\<cdot>xs))" and w="r"]
[PROOF STATE]
proof (prove)
using this:
(case a2c\<cdot>r of lnil \<Rightarrow> lnil | x :@ xs \<Rightarrow> (\<Lambda> x xs. x :@ f\<cdot>(c2a\<cdot>(lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>xs)))\<cdot>x\<cdot>xs) = (case nextR\<cdot>r of Nothing \<Rightarrow> lnil | Just\<cdot>(x, r) \<Rightarrow> (\<Lambda> x xs. x :@ f\<cdot>(c2a\<cdot>(lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>xs)))\<cdot>x\<cdot>(a2c\<cdot>r))

goal (1 subgoal):
 1. (\<Lambda> f r. case a2c\<cdot>r of lnil \<Rightarrow> lnil | x :@ xs \<Rightarrow> x :@ f\<cdot>(c2a\<cdot>(lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>xs)))\<cdot>f\<cdot>r = (\<Lambda> f r. case nextR\<cdot>r of Nothing \<Rightarrow> lnil | Just\<cdot>(x, xs) \<Rightarrow> x :@ f\<cdot>(c2a\<cdot>(lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>(a2c\<cdot>xs))))\<cdot>f\<cdot>r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nub_body'\<cdot>f\<cdot>r = nub_body''\<cdot>f\<cdot>r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nub_body''_nub_body'''_eq: "nub_body'' = nub_body''' oo (unwrap oo wrap)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nub_body'' = nub_body''' oo unwrap oo wrap
[PROOF STEP]
unfolding nub_body''_def nub_body'''_def wrap_def unwrap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> f r. case nextR\<cdot>r of Nothing \<Rightarrow> lnil | Just\<cdot>(x, xs) \<Rightarrow> x :@ f\<cdot>(c2a\<cdot>(lfilter\<cdot>(neg oo Abs_cfun ((=\<^sub>B) x))\<cdot>(a2c\<cdot>xs)))) = (\<Lambda> f r. case nextR\<cdot>r of Nothing \<Rightarrow> lnil | Just\<cdot>(x, xs) \<Rightarrow> x :@ f\<cdot>(filterR\<cdot>x\<cdot>xs)) oo (\<Lambda> f r. f\<cdot>(a2c\<cdot>r)) oo (\<Lambda> f xs. f\<cdot>(c2a\<cdot>xs))
[PROOF STEP]
by ((rule cfun_eqI)+, simp add: filter_filterR)


[STATEMENT]
lemma nub_wrap_nub_body''': "nub = wrap\<cdot>(fix\<cdot>nub_body''')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nub = wrap\<cdot>(fix\<cdot>nub_body''')
[PROOF STEP]
using worker_wrapper_fusion_new[OF wrap_unwrap_id unwrap_strict, where body=nub_body]
        nub_nub_body_eq
        nub_body_nub_body'_eq
        nub_body'_nub_body''_eq
        nub_body''_nub_body'''_eq
[PROOF STATE]
proof (prove)
using this:
unwrap oo nub_body oo wrap = ?body' oo unwrap oo wrap \<Longrightarrow> fix\<cdot>nub_body = wrap\<cdot>(fix\<cdot>?body')
nub = fix\<cdot>nub_body
unwrap oo nub_body oo wrap = nub_body'
nub_body' = nub_body''
nub_body'' = nub_body''' oo unwrap oo wrap

goal (1 subgoal):
 1. nub = wrap\<cdot>(fix\<cdot>nub_body''')
[PROOF STEP]
by simp


[STATEMENT]
lemma alllsts_UNIV [iff]:
  "s \<in> UNIV\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<infinity>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<infinity>
[PROOF STEP]
have "s \<in> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> UNIV
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s \<in> UNIV

goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<infinity>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> UNIV

goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<infinity>
[PROOF STEP]
proof coinduct
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> x = LNil \<or> (\<exists>l a. x = a ## l \<and> (l \<in> UNIV \<or> l \<in> UNIV\<^sup>\<infinity>) \<and> a \<in> UNIV)
[PROOF STEP]
case (alllsts z)
[PROOF STATE]
proof (state)
this:
z \<in> UNIV

goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> x = LNil \<or> (\<exists>l a. x = a ## l \<and> (l \<in> UNIV \<or> l \<in> UNIV\<^sup>\<infinity>) \<and> a \<in> UNIV)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
z \<in> UNIV

goal (1 subgoal):
 1. z = LNil \<or> (\<exists>l a. z = a ## l \<and> (l \<in> UNIV \<or> l \<in> UNIV\<^sup>\<infinity>) \<and> a \<in> UNIV)
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = LNil \<or> (\<exists>l a. z = a ## l \<and> (l \<in> UNIV \<or> l \<in> UNIV\<^sup>\<infinity>) \<and> a \<in> UNIV)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s \<in> UNIV\<^sup>\<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alllsts_empty [simp]: "{}\<^sup>\<infinity> = {LNil}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {}\<^sup>\<infinity> = {LNil}
[PROOF STEP]
by (auto elim: alllsts.cases)


[STATEMENT]
lemma alllsts_mono:
  assumes asubb: "A \<subseteq> B"
  shows "A\<^sup>\<infinity> \<subseteq> B\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sup>\<infinity> \<subseteq> B\<^sup>\<infinity>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A\<^sup>\<infinity> \<Longrightarrow> x \<in> B\<^sup>\<infinity>
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A\<^sup>\<infinity> \<Longrightarrow> x \<in> B\<^sup>\<infinity>
[PROOF STEP]
assume "x \<in> A\<^sup>\<infinity>"
[PROOF STATE]
proof (state)
this:
x \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. \<And>x. x \<in> A\<^sup>\<infinity> \<Longrightarrow> x \<in> B\<^sup>\<infinity>
[PROOF STEP]
thus "x \<in> B\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
using this:
x \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. x \<in> B\<^sup>\<infinity>
[PROOF STEP]
proof coinduct
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A\<^sup>\<infinity> \<Longrightarrow> x = LNil \<or> (\<exists>l a. x = a ## l \<and> (l \<in> A\<^sup>\<infinity> \<or> l \<in> B\<^sup>\<infinity>) \<and> a \<in> B)
[PROOF STEP]
case (alllsts z)
[PROOF STATE]
proof (state)
this:
z \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. \<And>x. x \<in> A\<^sup>\<infinity> \<Longrightarrow> x = LNil \<or> (\<exists>l a. x = a ## l \<and> (l \<in> A\<^sup>\<infinity> \<or> l \<in> B\<^sup>\<infinity>) \<and> a \<in> B)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
z \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. z = LNil \<or> (\<exists>l a. z = a ## l \<and> (l \<in> A\<^sup>\<infinity> \<or> l \<in> B\<^sup>\<infinity>) \<and> a \<in> B)
[PROOF STEP]
using asubb
[PROOF STATE]
proof (prove)
using this:
z \<in> A\<^sup>\<infinity>
A \<subseteq> B

goal (1 subgoal):
 1. z = LNil \<or> (\<exists>l a. z = a ## l \<and> (l \<in> A\<^sup>\<infinity> \<or> l \<in> B\<^sup>\<infinity>) \<and> a \<in> B)
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = LNil \<or> (\<exists>l a. z = a ## l \<and> (l \<in> A\<^sup>\<infinity> \<or> l \<in> B\<^sup>\<infinity>) \<and> a \<in> B)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> B\<^sup>\<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma LConsE [iff]: "x##xs \<in> A\<^sup>\<infinity> = (x\<in>A \<and> xs \<in> A\<^sup>\<infinity>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ## xs \<in> A\<^sup>\<infinity>) = (x \<in> A \<and> xs \<in> A\<^sup>\<infinity>)
[PROOF STEP]
by (auto elim: alllsts.cases)


[STATEMENT]
lemma poslsts_iff [iff]:
  "(s \<in> A\<^sup>\<spadesuit>) = (s \<in> A\<^sup>\<infinity> \<and> s \<noteq> LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<in> A\<^sup>\<spadesuit>) = (s \<in> A\<^sup>\<infinity> \<and> s \<noteq> LNil)
[PROOF STEP]
by (simp add: poslsts_def)


[STATEMENT]
lemma poslsts_UNIV [iff]:
  "s \<in> UNIV\<^sup>\<spadesuit> = (s \<noteq> LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<in> UNIV\<^sup>\<spadesuit>) = (s \<noteq> LNil)
[PROOF STEP]
by auto


[STATEMENT]
lemma poslsts_empty [simp]: "{}\<^sup>\<spadesuit> = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {}\<^sup>\<spadesuit> = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma poslsts_mono:
  "A \<subseteq> B \<Longrightarrow> A\<^sup>\<spadesuit> \<subseteq> B\<^sup>\<spadesuit>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> A\<^sup>\<spadesuit> \<subseteq> B\<^sup>\<spadesuit>
[PROOF STEP]
by (auto dest: alllsts_mono)


[STATEMENT]
lemma finlsts_empty [simp]: "{}\<^sup>\<star> = {LNil}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {}\<^sup>\<star> = {LNil}
[PROOF STEP]
by (auto elim: finlsts.cases)


[STATEMENT]
lemma finsubsetall: "x \<in> A\<^sup>\<star> \<Longrightarrow> x \<in> A\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A\<^sup>\<star> \<Longrightarrow> x \<in> A\<^sup>\<infinity>
[PROOF STEP]
by (induct rule: finlsts.induct) auto


[STATEMENT]
lemma finlsts_mono:
"A\<subseteq>B \<Longrightarrow> A\<^sup>\<star> \<subseteq> B\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> A\<^sup>\<star> \<subseteq> B\<^sup>\<star>
[PROOF STEP]
by (auto, erule finlsts.induct) auto


[STATEMENT]
lemma finlsts_induct
  [case_names LNil_fin LCons_fin, induct set: finlsts, consumes 1]:
  assumes xA: "x \<in> A\<^sup>\<star>"
  and lnil: "\<And>l. l = LNil \<Longrightarrow> P l"
  and lcons: "\<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; P l; a \<in> A\<rbrakk> \<Longrightarrow> P (a ## l)"
  shows "P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x
[PROOF STEP]
using xA
[PROOF STATE]
proof (prove)
using this:
x \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. P x
[PROOF STEP]
by (induct "x") (auto intro: lnil lcons)


[STATEMENT]
lemma finite_lemma:
  assumes "x \<in> A\<^sup>\<star>"
  shows "x \<in> B\<^sup>\<infinity> \<Longrightarrow> x \<in> B\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> B\<^sup>\<infinity> \<Longrightarrow> x \<in> B\<^sup>\<star>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. x \<in> B\<^sup>\<infinity> \<Longrightarrow> x \<in> B\<^sup>\<star>
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>l = LNil; l \<in> B\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> l \<in> B\<^sup>\<star>
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; l \<in> B\<^sup>\<infinity> \<Longrightarrow> l \<in> B\<^sup>\<star>; a \<in> A; a ## l \<in> B\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> a ## l \<in> B\<^sup>\<star>
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
l_ = LNil
l_ \<in> B\<^sup>\<infinity>

goal (2 subgoals):
 1. \<And>l. \<lbrakk>l = LNil; l \<in> B\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> l \<in> B\<^sup>\<star>
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; l \<in> B\<^sup>\<infinity> \<Longrightarrow> l \<in> B\<^sup>\<star>; a \<in> A; a ## l \<in> B\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> a ## l \<in> B\<^sup>\<star>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l_ = LNil
l_ \<in> B\<^sup>\<infinity>

goal (1 subgoal):
 1. l_ \<in> B\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l_ \<in> B\<^sup>\<star>

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; l \<in> B\<^sup>\<infinity> \<Longrightarrow> l \<in> B\<^sup>\<star>; a \<in> A; a ## l \<in> B\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> a ## l \<in> B\<^sup>\<star>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; l \<in> B\<^sup>\<infinity> \<Longrightarrow> l \<in> B\<^sup>\<star>; a \<in> A; a ## l \<in> B\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> a ## l \<in> B\<^sup>\<star>
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> A\<^sup>\<star>
l \<in> B\<^sup>\<infinity> \<Longrightarrow> l \<in> B\<^sup>\<star>
a \<in> A
a ## l \<in> B\<^sup>\<infinity>

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; l \<in> B\<^sup>\<infinity> \<Longrightarrow> l \<in> B\<^sup>\<star>; a \<in> A; a ## l \<in> B\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> a ## l \<in> B\<^sup>\<star>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<star>
l \<in> B\<^sup>\<infinity> \<Longrightarrow> l \<in> B\<^sup>\<star>
a \<in> A
a ## l \<in> B\<^sup>\<infinity>

goal (1 subgoal):
 1. a ## l \<in> B\<^sup>\<star>
[PROOF STEP]
using LCons_fin
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<star>
l \<in> B\<^sup>\<infinity> \<Longrightarrow> l \<in> B\<^sup>\<star>
a \<in> A
a ## l \<in> B\<^sup>\<infinity>
l \<in> A\<^sup>\<star>
l \<in> B\<^sup>\<infinity> \<Longrightarrow> l \<in> B\<^sup>\<star>
a \<in> A
a ## l \<in> B\<^sup>\<infinity>

goal (1 subgoal):
 1. a ## l \<in> B\<^sup>\<star>
[PROOF STEP]
by (cases "a##l") auto
[PROOF STATE]
proof (state)
this:
a ## l \<in> B\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fin_finite [dest]:
assumes "r \<in> A\<^sup>\<star>" "r \<notin> UNIV\<^sup>\<star>"
  shows "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
have "A \<subseteq> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<subseteq> UNIV

goal (1 subgoal):
 1. False
[PROOF STEP]
hence "A\<^sup>\<star> \<subseteq> UNIV\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> UNIV

goal (1 subgoal):
 1. A\<^sup>\<star> \<subseteq> UNIV\<^sup>\<star>
[PROOF STEP]
by (rule finlsts_mono)
[PROOF STATE]
proof (state)
this:
A\<^sup>\<star> \<subseteq> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A\<^sup>\<star> \<subseteq> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A\<^sup>\<star> \<subseteq> UNIV\<^sup>\<star>
r \<in> A\<^sup>\<star>
r \<notin> UNIV\<^sup>\<star>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finT_simp [simp]:
  "r \<in> A\<^sup>\<star> \<Longrightarrow> r\<in>UNIV\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<Longrightarrow> r \<in> UNIV\<^sup>\<star>
[PROOF STEP]
by auto


[STATEMENT]
lemma finlsts_predI: "r \<in> A\<^sup>\<star> \<Longrightarrow> (r, a##r) \<in> finlsts_pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<Longrightarrow> (r, a ## r) \<in> finlsts_pred
[PROOF STEP]
by (auto simp: finlsts_pred_def)


[STATEMENT]
lemma wf_finlsts_pred: "wf finlsts_pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf finlsts_pred
[PROOF STEP]
proof (rule wfI [of _ "UNIV\<^sup>\<star>"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finlsts_pred \<subseteq> UNIV\<^sup>\<star> \<times> ?B
 2. \<And>x P. \<lbrakk>\<forall>x. (\<forall>y. (y, x) \<in> finlsts_pred \<longrightarrow> P y) \<longrightarrow> P x; x \<in> UNIV\<^sup>\<star>; x \<in> ?B\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
show "finlsts_pred \<subseteq> UNIV\<^sup>\<star> \<times> UNIV\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finlsts_pred \<subseteq> UNIV\<^sup>\<star> \<times> UNIV\<^sup>\<star>
[PROOF STEP]
by (auto simp: finlsts_pred_def elim: finlsts.cases)
[PROOF STATE]
proof (state)
this:
finlsts_pred \<subseteq> UNIV\<^sup>\<star> \<times> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<forall>x. (\<forall>y. (y, x) \<in> finlsts_pred \<longrightarrow> P y) \<longrightarrow> P x; x \<in> UNIV\<^sup>\<star>; x \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<forall>x. (\<forall>y. (y, x) \<in> finlsts_pred \<longrightarrow> P y) \<longrightarrow> P x; x \<in> UNIV\<^sup>\<star>; x \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
fix x::"'a llist" and P::"'a llist \<Rightarrow> bool"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<forall>x. (\<forall>y. (y, x) \<in> finlsts_pred \<longrightarrow> P y) \<longrightarrow> P x; x \<in> UNIV\<^sup>\<star>; x \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
assume xfin: "x \<in> UNIV\<^sup>\<star>" and H [unfolded finlsts_pred_def]:
    "(\<forall>x. (\<forall>y. (y, x) \<in> finlsts_pred \<longrightarrow> P y) \<longrightarrow> P x)"
[PROOF STATE]
proof (state)
this:
x \<in> UNIV\<^sup>\<star>
\<forall>x. (\<forall>y. (y, x) \<in> {(r, s). r \<in> UNIV\<^sup>\<star> \<and> (\<exists>a. a ## r = s)} \<longrightarrow> P y) \<longrightarrow> P x

goal (1 subgoal):
 1. \<And>x P. \<lbrakk>\<forall>x. (\<forall>y. (y, x) \<in> finlsts_pred \<longrightarrow> P y) \<longrightarrow> P x; x \<in> UNIV\<^sup>\<star>; x \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
from  xfin
[PROOF STATE]
proof (chain)
picking this:
x \<in> UNIV\<^sup>\<star>
[PROOF STEP]
show "P x"
[PROOF STATE]
proof (prove)
using this:
x \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. P x
[PROOF STEP]
proof(induct x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> P l
 2. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; P l; a \<in> UNIV\<rbrakk> \<Longrightarrow> P (a ## l)
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
l_ = LNil

goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> P l
 2. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; P l; a \<in> UNIV\<rbrakk> \<Longrightarrow> P (a ## l)
[PROOF STEP]
with H
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. (\<forall>y. (y, x) \<in> {(r, s). r \<in> UNIV\<^sup>\<star> \<and> (\<exists>a. a ## r = s)} \<longrightarrow> P y) \<longrightarrow> P x
l_ = LNil
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<forall>y. (y, x) \<in> {(r, s). r \<in> UNIV\<^sup>\<star> \<and> (\<exists>a. a ## r = s)} \<longrightarrow> P y) \<longrightarrow> P x
l_ = LNil

goal (1 subgoal):
 1. P l_
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P l_

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; P l; a \<in> UNIV\<rbrakk> \<Longrightarrow> P (a ## l)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; P l; a \<in> UNIV\<rbrakk> \<Longrightarrow> P (a ## l)
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> UNIV\<^sup>\<star>
P l
a \<in> UNIV

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; P l; a \<in> UNIV\<rbrakk> \<Longrightarrow> P (a ## l)
[PROOF STEP]
with H
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. (\<forall>y. (y, x) \<in> {(r, s). r \<in> UNIV\<^sup>\<star> \<and> (\<exists>a. a ## r = s)} \<longrightarrow> P y) \<longrightarrow> P x
l \<in> UNIV\<^sup>\<star>
P l
a \<in> UNIV
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<forall>y. (y, x) \<in> {(r, s). r \<in> UNIV\<^sup>\<star> \<and> (\<exists>a. a ## r = s)} \<longrightarrow> P y) \<longrightarrow> P x
l \<in> UNIV\<^sup>\<star>
P l
a \<in> UNIV

goal (1 subgoal):
 1. P (a ## l)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P (a ## l)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finlsts_rec_LNil: "finlsts_rec c d LNil = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finlsts_rec c d LNil = c
[PROOF STEP]
by (auto simp: wf_finlsts_pred finlsts_rec_def wfrec)


[STATEMENT]
lemma finlsts_rec_LCons:
 "r \<in> A\<^sup>\<star> \<Longrightarrow> finlsts_rec c d (a ## r) = d a r (finlsts_rec c d r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<Longrightarrow> finlsts_rec c d (a ## r) = d a r (finlsts_rec c d r)
[PROOF STEP]
by (auto simp: wf_finlsts_pred finlsts_rec_def wfrec cut_def intro: finlsts_predI)


[STATEMENT]
lemma finlsts_rec_LCons_def:
  "\<lbrakk> f \<equiv> finlsts_rec c d; r \<in> A\<^sup>\<star> \<rbrakk> \<Longrightarrow> f (a ## r) = d a r (f r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<equiv> finlsts_rec c d; r \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> f (a ## r) = d a r (f r)
[PROOF STEP]
by (auto simp: finlsts_rec_LCons)


[STATEMENT]
lemma fpslsts_iff [iff]:
  "(s \<in> A\<^sup>\<clubsuit>) = (s \<in> A\<^sup>\<star> \<and> s \<noteq> LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<in> A\<^sup>\<clubsuit>) = (s \<in> A\<^sup>\<star> \<and> s \<noteq> LNil)
[PROOF STEP]
by (auto simp: fpslsts_def)


[STATEMENT]
lemma fpslsts_empty [simp]: "{}\<^sup>\<clubsuit> = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {}\<^sup>\<clubsuit> = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma fpslsts_mono:
  "A \<subseteq> B \<Longrightarrow> A\<^sup>\<clubsuit> \<subseteq> B\<^sup>\<clubsuit>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> A\<^sup>\<clubsuit> \<subseteq> B\<^sup>\<clubsuit>
[PROOF STEP]
by (auto dest: finlsts_mono)


[STATEMENT]
lemma fpslsts_cases [case_names LCons, cases set: fpslsts]:
assumes rfps: "r \<in> A\<^sup>\<clubsuit>"
  and H: "\<And> a rs. \<lbrakk> r = a ## rs; a\<in>A; rs \<in> A\<^sup>\<star> \<rbrakk> \<Longrightarrow> R"
  shows "R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R
[PROOF STEP]
from rfps
[PROOF STATE]
proof (chain)
picking this:
r \<in> A\<^sup>\<clubsuit>
[PROOF STEP]
have "r \<in> A\<^sup>\<star>" and "r \<noteq> LNil"
[PROOF STATE]
proof (prove)
using this:
r \<in> A\<^sup>\<clubsuit>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> &&& r \<noteq> LNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star>
r \<noteq> LNil

goal (1 subgoal):
 1. R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<in> A\<^sup>\<star>
r \<noteq> LNil

goal (1 subgoal):
 1. R
[PROOF STEP]
by (cases r, simp) (blast intro!: H)
[PROOF STATE]
proof (state)
this:
R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inflstsI [intro]:
  "\<lbrakk> x \<in> A\<^sup>\<infinity>; x \<in> UNIV\<^sup>\<star> \<Longrightarrow> False \<rbrakk> \<Longrightarrow> x \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A\<^sup>\<infinity>; x \<in> UNIV\<^sup>\<star> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> x \<in> A\<^sup>\<omega>
[PROOF STEP]
unfolding inflsts_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A\<^sup>\<infinity>; x \<in> UNIV\<^sup>\<star> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> x \<in> A\<^sup>\<infinity> - UNIV\<^sup>\<star>
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma inflstsE [elim]:
  "\<lbrakk> x \<in> A\<^sup>\<omega>; \<lbrakk> x \<in> A\<^sup>\<infinity>; x \<notin> UNIV\<^sup>\<star> \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A\<^sup>\<omega>; \<lbrakk>x \<in> A\<^sup>\<infinity>; x \<notin> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by (unfold inflsts_def) auto


[STATEMENT]
lemma inflsts_empty [simp]: "{}\<^sup>\<omega> = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {}\<^sup>\<omega> = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma inflsts_mono:
  "A \<subseteq> B \<Longrightarrow> A\<^sup>\<omega> \<subseteq> B\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> A\<^sup>\<omega> \<subseteq> B\<^sup>\<omega>
[PROOF STEP]
by (blast dest: alllsts_mono infsubsetall)


[STATEMENT]
lemma inflsts_cases [case_names LCons, cases set: inflsts, consumes 1]:
  assumes sinf: "s \<in> A\<^sup>\<omega>"
  and R: "\<And>a l. \<lbrakk> l \<in> A\<^sup>\<omega>; a \<in> A; s = a ## l \<rbrakk> \<Longrightarrow> R"
  shows "R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R
[PROOF STEP]
from sinf
[PROOF STATE]
proof (chain)
picking this:
s \<in> A\<^sup>\<omega>
[PROOF STEP]
have "s \<in> A\<^sup>\<infinity>" "s \<notin> UNIV\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. s \<in> A\<^sup>\<infinity> &&& s \<notin> UNIV\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> A\<^sup>\<infinity>
s \<notin> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> A\<^sup>\<infinity>
s \<notin> UNIV\<^sup>\<star>
[PROOF STEP]
obtain a l where "l \<in> A\<^sup>\<omega>" and "a\<in>A" and "s = a ## l"
[PROOF STATE]
proof (prove)
using this:
s \<in> A\<^sup>\<infinity>
s \<notin> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. (\<And>l a. \<lbrakk>l \<in> A\<^sup>\<omega>; a \<in> A; s = a ## l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "s") auto
[PROOF STATE]
proof (state)
this:
l \<in> A\<^sup>\<omega>
a \<in> A
s = a ## l

goal (1 subgoal):
 1. R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<omega>
a \<in> A
s = a ## l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inflstsI2: "\<lbrakk>a \<in> A; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> a ## t \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> A; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> a ## t \<in> A\<^sup>\<omega>
[PROOF STEP]
by  (auto elim: finlsts.cases)


[STATEMENT]
lemma infT_simp [simp]:
  "r \<in> A\<^sup>\<omega> \<Longrightarrow> r\<in>UNIV\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<omega> \<Longrightarrow> r \<in> UNIV\<^sup>\<omega>
[PROOF STEP]
by auto


[STATEMENT]
lemma  alllstsE [consumes 1, case_names finite infinite]:
  "\<lbrakk> x\<in>A\<^sup>\<infinity>; x \<in> A\<^sup>\<star> \<Longrightarrow> P; x \<in> A\<^sup>\<omega> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A\<^sup>\<infinity>; x \<in> A\<^sup>\<star> \<Longrightarrow> P; x \<in> A\<^sup>\<omega> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (auto intro: finite_lemma simp: inflsts_def)


[STATEMENT]
lemma fin_inf_cases [case_names finite infinite]:
  "\<lbrakk> r\<in>UNIV\<^sup>\<star> \<Longrightarrow> P; r \<in> UNIV\<^sup>\<omega> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> UNIV\<^sup>\<star> \<Longrightarrow> P; r \<in> UNIV\<^sup>\<omega> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by auto


[STATEMENT]
lemma  fin_Int_inf: "A\<^sup>\<star> \<inter> A\<^sup>\<omega> = {}"
  and   fin_Un_inf: "A\<^sup>\<star> \<union> A\<^sup>\<omega> = A\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sup>\<star> \<inter> A\<^sup>\<omega> = {} &&& A\<^sup>\<star> \<union> A\<^sup>\<omega> = A\<^sup>\<infinity>
[PROOF STEP]
by (auto intro: finite_lemma finsubsetall)


[STATEMENT]
lemma notfin_inf [iff]: "(x \<notin> UNIV\<^sup>\<star>) = (x \<in> UNIV\<^sup>\<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<notin> UNIV\<^sup>\<star>) = (x \<in> UNIV\<^sup>\<omega>)
[PROOF STEP]
by auto


[STATEMENT]
lemma notinf_fin [iff]: "(x \<notin> UNIV\<^sup>\<omega>) = (x \<in> UNIV\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<notin> UNIV\<^sup>\<omega>) = (x \<in> UNIV\<^sup>\<star>)
[PROOF STEP]
by auto


[STATEMENT]
lemma lapp_inf [simp]:
  assumes "s \<in> A\<^sup>\<omega>"
  shows "s @@ t = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s @@ t = s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. s @@ t = s
[PROOF STEP]
by(coinduction arbitrary: s)(auto elim: inflsts_cases)


[STATEMENT]
lemma LNil_is_lappend_conv [iff]:
"(LNil = s @@ t) = (s = LNil \<and> t = LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LNil = s @@ t) = (s = LNil \<and> t = LNil)
[PROOF STEP]
by (cases "s") auto


[STATEMENT]
lemma lappend_is_LNil_conv [iff]:
  "(s @@ t = LNil) = (s = LNil \<and> t = LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s @@ t = LNil) = (s = LNil \<and> t = LNil)
[PROOF STEP]
by (cases "s") auto


[STATEMENT]
lemma same_lappend_eq [iff]:
 "r \<in> A\<^sup>\<star> \<Longrightarrow> (r @@ s = r @@ t) = (s = t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<Longrightarrow> (r @@ s = r @@ t) = (s = t)
[PROOF STEP]
by (erule finlsts.induct) simp+


[STATEMENT]
lemma lappT:
  assumes sllist: "s \<in> A\<^sup>\<infinity>"
  and tllist: "t \<in> A\<^sup>\<infinity>"
  shows "s@@t \<in> A\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s @@ t \<in> A\<^sup>\<infinity>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s @@ t \<in> A\<^sup>\<infinity>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
s \<in> A\<^sup>\<infinity>
t \<in> A\<^sup>\<infinity>
[PROOF STEP]
have "lappend s t \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {lappend u v})"
[PROOF STATE]
proof (prove)
using this:
s \<in> A\<^sup>\<infinity>
t \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. s @@ t \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v})
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
s @@ t \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v})

goal (1 subgoal):
 1. s @@ t \<in> A\<^sup>\<infinity>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s @@ t \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v})

goal (1 subgoal):
 1. s @@ t \<in> A\<^sup>\<infinity>
[PROOF STEP]
proof coinduct
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v}) \<Longrightarrow> x = LNil \<or> (\<exists>l a. x = a ## l \<and> (l \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v}) \<or> l \<in> A\<^sup>\<infinity>) \<and> a \<in> A)
[PROOF STEP]
case (alllsts z)
[PROOF STATE]
proof (state)
this:
z \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v})

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v}) \<Longrightarrow> x = LNil \<or> (\<exists>l a. x = a ## l \<and> (l \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v}) \<or> l \<in> A\<^sup>\<infinity>) \<and> a \<in> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v})
[PROOF STEP]
obtain u v where ullist: "u\<in>A\<^sup>\<infinity>" and vllist: "v\<in>A\<^sup>\<infinity>"
      and zapp: "z=u @@ v"
[PROOF STATE]
proof (prove)
using this:
z \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v})

goal (1 subgoal):
 1. (\<And>u v. \<lbrakk>u \<in> A\<^sup>\<infinity>; v \<in> A\<^sup>\<infinity>; z = u @@ v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> A\<^sup>\<infinity>
v \<in> A\<^sup>\<infinity>
z = u @@ v

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v}) \<Longrightarrow> x = LNil \<or> (\<exists>l a. x = a ## l \<and> (l \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v}) \<or> l \<in> A\<^sup>\<infinity>) \<and> a \<in> A)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
u \<in> A\<^sup>\<infinity>
v \<in> A\<^sup>\<infinity>
z = u @@ v

goal (1 subgoal):
 1. z = LNil \<or> (\<exists>l a. z = a ## l \<and> (l \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v}) \<or> l \<in> A\<^sup>\<infinity>) \<and> a \<in> A)
[PROOF STEP]
by (cases "u") (auto elim: alllsts.cases)
[PROOF STATE]
proof (state)
this:
z = LNil \<or> (\<exists>l a. z = a ## l \<and> (l \<in> (\<Union>u\<in>A\<^sup>\<infinity>. \<Union>v\<in>A\<^sup>\<infinity>. {u @@ v}) \<or> l \<in> A\<^sup>\<infinity>) \<and> a \<in> A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s @@ t \<in> A\<^sup>\<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lappfin_finT: "\<lbrakk> s \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<star> \<rbrakk> \<Longrightarrow> s@@t \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> s @@ t \<in> A\<^sup>\<star>
[PROOF STEP]
by (induct rule: finlsts.induct) auto