[STATEMENT]
lemma ce_set_lm_5: "\<lbrakk> A \<in> ce_sets; p \<in> PrimRec1 \<rbrakk> \<Longrightarrow> { x . p x \<in> A } \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
assume A1: "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
assume A2: "p \<in> PrimRec1"
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec1

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
have "\<exists> pA \<in> PrimRec2. A = fn_to_set pA"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<exists>pA\<in>PrimRec2. A = fn_to_set pA
[PROOF STEP]
by (rule ce_set_lm_3)
[PROOF STATE]
proof (state)
this:
\<exists>pA\<in>PrimRec2. A = fn_to_set pA

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>pA\<in>PrimRec2. A = fn_to_set pA
[PROOF STEP]
obtain pA where pA_is_pr: "pA \<in> PrimRec2" and S1: "A = fn_to_set pA"
[PROOF STATE]
proof (prove)
using this:
\<exists>pA\<in>PrimRec2. A = fn_to_set pA

goal (1 subgoal):
 1. (\<And>pA. \<lbrakk>pA \<in> PrimRec2; A = fn_to_set pA\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
pA \<in> PrimRec2
A = fn_to_set pA

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
from S1
[PROOF STATE]
proof (chain)
picking this:
A = fn_to_set pA
[PROOF STEP]
have S2: "A = { x . \<exists> y. pA x y = 0 }"
[PROOF STATE]
proof (prove)
using this:
A = fn_to_set pA

goal (1 subgoal):
 1. A = {x. \<exists>y. pA x y = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
A = {x. \<exists>y. pA x y = 0}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
define q where "q x y = pA (p x) y" for x y
[PROOF STATE]
proof (state)
this:
q ?x ?y = pA (p ?x) ?y

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
from pA_is_pr A2
[PROOF STATE]
proof (chain)
picking this:
pA \<in> PrimRec2
p \<in> PrimRec1
[PROOF STEP]
have q_is_pr: "q \<in> PrimRec2"
[PROOF STATE]
proof (prove)
using this:
pA \<in> PrimRec2
p \<in> PrimRec1

goal (1 subgoal):
 1. q \<in> PrimRec2
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
using this:
pA \<in> PrimRec2
p \<in> PrimRec1

goal (1 subgoal):
 1. (\<lambda>x. pA (p x)) \<in> PrimRec2
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
q \<in> PrimRec2

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
have "\<And> x. (p x \<in> A) = (\<exists> y. q x y = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (p x \<in> A) = (\<exists>y. q x y = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (p x \<in> A) = (\<exists>y. q x y = 0)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (p x \<in> A) = (\<exists>y. q x y = 0)
[PROOF STEP]
show "(p x \<in> A) = (\<exists> y. q x y = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p x \<in> A) = (\<exists>y. q x y = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p x \<in> A \<Longrightarrow> \<exists>y. q x y = 0
 2. \<exists>y. q x y = 0 \<Longrightarrow> p x \<in> A
[PROOF STEP]
assume A: "p x \<in> A"
[PROOF STATE]
proof (state)
this:
p x \<in> A

goal (2 subgoals):
 1. p x \<in> A \<Longrightarrow> \<exists>y. q x y = 0
 2. \<exists>y. q x y = 0 \<Longrightarrow> p x \<in> A
[PROOF STEP]
with S2
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. pA x y = 0}
p x \<in> A
[PROOF STEP]
obtain y where L1: "pA (p x) y = 0"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. pA x y = 0}
p x \<in> A

goal (1 subgoal):
 1. (\<And>y. pA (p x) y = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pA (p x) y = 0

goal (2 subgoals):
 1. p x \<in> A \<Longrightarrow> \<exists>y. q x y = 0
 2. \<exists>y. q x y = 0 \<Longrightarrow> p x \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pA (p x) y = 0
[PROOF STEP]
have "q x y = 0"
[PROOF STATE]
proof (prove)
using this:
pA (p x) y = 0

goal (1 subgoal):
 1. q x y = 0
[PROOF STEP]
by (simp add: q_def)
[PROOF STATE]
proof (state)
this:
q x y = 0

goal (2 subgoals):
 1. p x \<in> A \<Longrightarrow> \<exists>y. q x y = 0
 2. \<exists>y. q x y = 0 \<Longrightarrow> p x \<in> A
[PROOF STEP]
thus "\<exists> y. q x y = 0"
[PROOF STATE]
proof (prove)
using this:
q x y = 0

goal (1 subgoal):
 1. \<exists>y. q x y = 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>y. q x y = 0

goal (1 subgoal):
 1. \<exists>y. q x y = 0 \<Longrightarrow> p x \<in> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. q x y = 0 \<Longrightarrow> p x \<in> A
[PROOF STEP]
assume A: "\<exists>y. q x y = 0"
[PROOF STATE]
proof (state)
this:
\<exists>y. q x y = 0

goal (1 subgoal):
 1. \<exists>y. q x y = 0 \<Longrightarrow> p x \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. q x y = 0
[PROOF STEP]
obtain y where L1: "q x y = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. q x y = 0

goal (1 subgoal):
 1. (\<And>y. q x y = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
q x y = 0

goal (1 subgoal):
 1. \<exists>y. q x y = 0 \<Longrightarrow> p x \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q x y = 0
[PROOF STEP]
have "pA (p x) y = 0"
[PROOF STATE]
proof (prove)
using this:
q x y = 0

goal (1 subgoal):
 1. pA (p x) y = 0
[PROOF STEP]
by (simp add: q_def)
[PROOF STATE]
proof (state)
this:
pA (p x) y = 0

goal (1 subgoal):
 1. \<exists>y. q x y = 0 \<Longrightarrow> p x \<in> A
[PROOF STEP]
with S2
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. pA x y = 0}
pA (p x) y = 0
[PROOF STEP]
show "p x \<in> A"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. pA x y = 0}
pA (p x) y = 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(p x \<in> A) = (\<exists>y. q x y = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(p ?x \<in> A) = (\<exists>y. q ?x y = 0)

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p ?x \<in> A) = (\<exists>y. q ?x y = 0)
[PROOF STEP]
have "{ x . p x \<in> A } = { x. \<exists> y. q x y = 0 }"
[PROOF STATE]
proof (prove)
using this:
(p ?x \<in> A) = (\<exists>y. q ?x y = 0)

goal (1 subgoal):
 1. {x. p x \<in> A} = {x. \<exists>y. q x y = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. p x \<in> A} = {x. \<exists>y. q x y = 0}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{x. p x \<in> A} = {x. \<exists>y. q x y = 0}
[PROOF STEP]
have "{ x . p x \<in> A } = fn_to_set q"
[PROOF STATE]
proof (prove)
using this:
{x. p x \<in> A} = {x. \<exists>y. q x y = 0}

goal (1 subgoal):
 1. {x. p x \<in> A} = fn_to_set q
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
{x. p x \<in> A} = fn_to_set q

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{x. p x \<in> A} = fn_to_set q

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
from q_is_pr
[PROOF STATE]
proof (chain)
picking this:
q \<in> PrimRec2
[PROOF STEP]
have "fn_to_set q \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
q \<in> PrimRec2

goal (1 subgoal):
 1. fn_to_set q \<in> ce_sets
[PROOF STEP]
by (rule ce_set_lm_1)
[PROOF STATE]
proof (state)
this:
fn_to_set q \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{x. p x \<in> A} = fn_to_set q
fn_to_set q \<in> ce_sets
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{x. p x \<in> A} = fn_to_set q
fn_to_set q \<in> ce_sets

goal (1 subgoal):
 1. {x. p x \<in> A} \<in> ce_sets
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. p x \<in> A} \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_set_lm_6: "\<lbrakk> A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> q \<in> PrimRec1. A = { q x | x. x \<in> UNIV }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
assume A1: "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
assume A2: "A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
have "\<exists> pA \<in> PrimRec2. A = fn_to_set pA"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<exists>pA\<in>PrimRec2. A = fn_to_set pA
[PROOF STEP]
by (rule ce_set_lm_3)
[PROOF STATE]
proof (state)
this:
\<exists>pA\<in>PrimRec2. A = fn_to_set pA

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>pA\<in>PrimRec2. A = fn_to_set pA
[PROOF STEP]
obtain pA where pA_is_pr: "pA \<in> PrimRec2" and S1: "A = fn_to_set pA"
[PROOF STATE]
proof (prove)
using this:
\<exists>pA\<in>PrimRec2. A = fn_to_set pA

goal (1 subgoal):
 1. (\<And>pA. \<lbrakk>pA \<in> PrimRec2; A = fn_to_set pA\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
pA \<in> PrimRec2
A = fn_to_set pA

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
from S1
[PROOF STATE]
proof (chain)
picking this:
A = fn_to_set pA
[PROOF STEP]
have S2: "A = { x. \<exists> y. pA x y = 0 }"
[PROOF STATE]
proof (prove)
using this:
A = fn_to_set pA

goal (1 subgoal):
 1. A = {x. \<exists>y. pA x y = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
A = {x. \<exists>y. pA x y = 0}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
from A2
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> {}
[PROOF STEP]
obtain a where a_in: "a \<in> A"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. (\<And>a. a \<in> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
define q where "q z = (if pA (c_fst z) (c_snd z) = 0 then c_fst z else a)" for z
[PROOF STATE]
proof (state)
this:
q ?z = (if pA (c_fst ?z) (c_snd ?z) = 0 then c_fst ?z else a)

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
from pA_is_pr
[PROOF STATE]
proof (chain)
picking this:
pA \<in> PrimRec2
[PROOF STEP]
have q_is_pr: "q \<in> PrimRec1"
[PROOF STATE]
proof (prove)
using this:
pA \<in> PrimRec2

goal (1 subgoal):
 1. q \<in> PrimRec1
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
using this:
pA \<in> PrimRec2

goal (1 subgoal):
 1. (\<lambda>z. if pA (c_fst z) (c_snd z) = 0 then c_fst z else a) \<in> PrimRec1
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
q \<in> PrimRec1

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
have S3: "\<forall> z. q z \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. q z \<in> A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. q z \<in> A
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. q z \<in> A
[PROOF STEP]
show "q z \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q z \<in> A
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> q z \<in> A
 2. \<not> ?P \<Longrightarrow> q z \<in> A
[PROOF STEP]
assume A: "pA (c_fst z) (c_snd z) = 0"
[PROOF STATE]
proof (state)
this:
pA (c_fst z) (c_snd z) = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> q z \<in> A
 2. \<not> ?P \<Longrightarrow> q z \<in> A
[PROOF STEP]
with S2
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. pA x y = 0}
pA (c_fst z) (c_snd z) = 0
[PROOF STEP]
have "c_fst z \<in> A"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. pA x y = 0}
pA (c_fst z) (c_snd z) = 0

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> q z \<in> A
 2. \<not> ?P \<Longrightarrow> q z \<in> A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c_fst z \<in> A

goal (2 subgoals):
 1. ?P \<Longrightarrow> q z \<in> A
 2. \<not> ?P \<Longrightarrow> q z \<in> A
[PROOF STEP]
from A q_def
[PROOF STATE]
proof (chain)
picking this:
pA (c_fst z) (c_snd z) = 0
q ?z = (if pA (c_fst ?z) (c_snd ?z) = 0 then c_fst ?z else a)
[PROOF STEP]
have "q z = c_fst z"
[PROOF STATE]
proof (prove)
using this:
pA (c_fst z) (c_snd z) = 0
q ?z = (if pA (c_fst ?z) (c_snd ?z) = 0 then c_fst ?z else a)

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> q z \<in> A
 2. \<not> ?P \<Longrightarrow> q z \<in> A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c_fst z \<in> A
q z = c_fst z
[PROOF STEP]
show "q z \<in> A"
[PROOF STATE]
proof (prove)
using this:
c_fst z \<in> A
q z = c_fst z

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

goal (1 subgoal):
 1. pA (c_fst z) (c_snd z) \<noteq> 0 \<Longrightarrow> q z \<in> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pA (c_fst z) (c_snd z) \<noteq> 0 \<Longrightarrow> q z \<in> A
[PROOF STEP]
assume A: "pA (c_fst z) (c_snd z) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
pA (c_fst z) (c_snd z) \<noteq> 0

goal (1 subgoal):
 1. pA (c_fst z) (c_snd z) \<noteq> 0 \<Longrightarrow> q z \<in> A
[PROOF STEP]
with q_def
[PROOF STATE]
proof (chain)
picking this:
q ?z = (if pA (c_fst ?z) (c_snd ?z) = 0 then c_fst ?z else a)
pA (c_fst z) (c_snd z) \<noteq> 0
[PROOF STEP]
have "q z = a"
[PROOF STATE]
proof (prove)
using this:
q ?z = (if pA (c_fst ?z) (c_snd ?z) = 0 then c_fst ?z else a)
pA (c_fst z) (c_snd z) \<noteq> 0

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

goal (1 subgoal):
 1. pA (c_fst z) (c_snd z) \<noteq> 0 \<Longrightarrow> q z \<in> A
[PROOF STEP]
with a_in
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
q z = a
[PROOF STEP]
show "q z \<in> A"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
q z = a

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
q z \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>z. q z \<in> A

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>z. q z \<in> A
[PROOF STEP]
have S4: "{ q x | x. x \<in> UNIV } \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
\<forall>z. q z \<in> A

goal (1 subgoal):
 1. {q x |x. x \<in> UNIV} \<subseteq> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{q x |x. x \<in> UNIV} \<subseteq> A

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
have S5: "A \<subseteq> { q x | x. x \<in> UNIV }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> {q x |x. x \<in> UNIV}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> {q x |x. x \<in> UNIV}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> {q x |x. x \<in> UNIV}
[PROOF STEP]
assume A: "x \<in> A"
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> {q x |x. x \<in> UNIV}
[PROOF STEP]
show "x \<in> {q x |x. x \<in> UNIV}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {q x |x. x \<in> UNIV}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>xa. x = q xa \<and> xa \<in> UNIV
[PROOF STEP]
from A S2
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
A = {x. \<exists>y. pA x y = 0}
[PROOF STEP]
obtain y where L1: "pA x y = 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
A = {x. \<exists>y. pA x y = 0}

goal (1 subgoal):
 1. (\<And>y. pA x y = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pA x y = 0

goal (1 subgoal):
 1. \<exists>xa. x = q xa \<and> xa \<in> UNIV
[PROOF STEP]
let ?z = "c_pair x y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>xa. x = q xa \<and> xa \<in> UNIV
[PROOF STEP]
from L1
[PROOF STATE]
proof (chain)
picking this:
pA x y = 0
[PROOF STEP]
have "q ?z = x"
[PROOF STATE]
proof (prove)
using this:
pA x y = 0

goal (1 subgoal):
 1. q (c_pair x y) = x
[PROOF STEP]
by (simp add: q_def)
[PROOF STATE]
proof (state)
this:
q (c_pair x y) = x

goal (1 subgoal):
 1. \<exists>xa. x = q xa \<and> xa \<in> UNIV
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q (c_pair x y) = x
[PROOF STEP]
have "\<exists> u. q u = x"
[PROOF STATE]
proof (prove)
using this:
q (c_pair x y) = x

goal (1 subgoal):
 1. \<exists>u. q u = x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>u. q u = x

goal (1 subgoal):
 1. \<exists>xa. x = q xa \<and> xa \<in> UNIV
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. q u = x
[PROOF STEP]
show "\<exists>u. x = q u \<and> u \<in> UNIV"
[PROOF STATE]
proof (prove)
using this:
\<exists>u. q u = x

goal (1 subgoal):
 1. \<exists>u. x = q u \<and> u \<in> UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u. x = q u \<and> u \<in> UNIV

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> {q x |x. x \<in> UNIV}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<subseteq> {q x |x. x \<in> UNIV}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
from S4 S5
[PROOF STATE]
proof (chain)
picking this:
{q x |x. x \<in> UNIV} \<subseteq> A
A \<subseteq> {q x |x. x \<in> UNIV}
[PROOF STEP]
have S6: "A = { q x | x. x \<in> UNIV }"
[PROOF STATE]
proof (prove)
using this:
{q x |x. x \<in> UNIV} \<subseteq> A
A \<subseteq> {q x |x. x \<in> UNIV}

goal (1 subgoal):
 1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = {q x |x. x \<in> UNIV}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
with q_is_pr
[PROOF STATE]
proof (chain)
picking this:
q \<in> PrimRec1
A = {q x |x. x \<in> UNIV}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<in> PrimRec1
A = {q x |x. x \<in> UNIV}

goal (1 subgoal):
 1. \<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>q\<in>PrimRec1. A = {q x |x. x \<in> UNIV}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_set_lm_7: "\<lbrakk> A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> { p x | x. x \<in> A } \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
assume A1: "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
assume A2: "p \<in> PrimRec1"
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec1

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
let ?B = "{ p x | x. x \<in> A }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
have S1: "(y \<in> ?B) = (\<exists> x. x \<in> A \<and> (y = p x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> {p x |x. x \<in> A}) = (\<exists>x. x \<in> A \<and> y = p x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y \<in> {p x |x. x \<in> A}) = (\<exists>x. x \<in> A \<and> y = p x)

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
have "\<exists> pA \<in> PrimRec2. A = fn_to_set pA"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<exists>pA\<in>PrimRec2. A = fn_to_set pA
[PROOF STEP]
by (rule ce_set_lm_3)
[PROOF STATE]
proof (state)
this:
\<exists>pA\<in>PrimRec2. A = fn_to_set pA

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>pA\<in>PrimRec2. A = fn_to_set pA
[PROOF STEP]
obtain pA where pA_is_pr: "pA \<in> PrimRec2" and S2: "A = fn_to_set pA"
[PROOF STATE]
proof (prove)
using this:
\<exists>pA\<in>PrimRec2. A = fn_to_set pA

goal (1 subgoal):
 1. (\<And>pA. \<lbrakk>pA \<in> PrimRec2; A = fn_to_set pA\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
pA \<in> PrimRec2
A = fn_to_set pA

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
from S2
[PROOF STATE]
proof (chain)
picking this:
A = fn_to_set pA
[PROOF STEP]
have S3: "A = { x. \<exists> y. pA x y = 0 }"
[PROOF STATE]
proof (prove)
using this:
A = fn_to_set pA

goal (1 subgoal):
 1. A = {x. \<exists>y. pA x y = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
A = {x. \<exists>y. pA x y = 0}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
define q where "q y t = (if y = p (c_snd t) then pA (c_snd t) (c_fst t) else 1)" for y t
[PROOF STATE]
proof (state)
this:
q ?y ?t = (if ?y = p (c_snd ?t) then pA (c_snd ?t) (c_fst ?t) else 1)

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
from pA_is_pr A2
[PROOF STATE]
proof (chain)
picking this:
pA \<in> PrimRec2
p \<in> PrimRec1
[PROOF STEP]
have q_is_pr: "q \<in> PrimRec2"
[PROOF STATE]
proof (prove)
using this:
pA \<in> PrimRec2
p \<in> PrimRec1

goal (1 subgoal):
 1. q \<in> PrimRec2
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
using this:
pA \<in> PrimRec2
p \<in> PrimRec1

goal (1 subgoal):
 1. (\<lambda>y t. if y = p (c_snd t) then pA (c_snd t) (c_fst t) else 1) \<in> PrimRec2
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
q \<in> PrimRec2

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
have L1: "\<And> y. (y \<in> ?B) = (\<exists> z. q y z = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. (y \<in> {p x |x. x \<in> A}) = (\<exists>z. q y z = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. (y \<in> {p x |x. x \<in> A}) = (\<exists>z. q y z = 0)
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. (y \<in> {p x |x. x \<in> A}) = (\<exists>z. q y z = 0)
[PROOF STEP]
show "(y \<in> ?B) = (\<exists> z. q y z = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> {p x |x. x \<in> A}) = (\<exists>z. q y z = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> {p x |x. x \<in> A} \<Longrightarrow> \<exists>z. q y z = 0
 2. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
assume AA1: "y \<in> ?B"
[PROOF STATE]
proof (state)
this:
y \<in> {p x |x. x \<in> A}

goal (2 subgoals):
 1. y \<in> {p x |x. x \<in> A} \<Longrightarrow> \<exists>z. q y z = 0
 2. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> {p x |x. x \<in> A}
[PROOF STEP]
obtain x0 where LL_2: "x0 \<in> A" and LL_3: "y = p x0"
[PROOF STATE]
proof (prove)
using this:
y \<in> {p x |x. x \<in> A}

goal (1 subgoal):
 1. (\<And>x0. \<lbrakk>x0 \<in> A; y = p x0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x0 \<in> A
y = p x0

goal (2 subgoals):
 1. y \<in> {p x |x. x \<in> A} \<Longrightarrow> \<exists>z. q y z = 0
 2. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
from S3
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. pA x y = 0}
[PROOF STEP]
have LL_4: "(x0 \<in> A) = (\<exists> z. pA x0 z = 0)"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. pA x y = 0}

goal (1 subgoal):
 1. (x0 \<in> A) = (\<exists>z. pA x0 z = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x0 \<in> A) = (\<exists>z. pA x0 z = 0)

goal (2 subgoals):
 1. y \<in> {p x |x. x \<in> A} \<Longrightarrow> \<exists>z. q y z = 0
 2. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
from LL_2 LL_4
[PROOF STATE]
proof (chain)
picking this:
x0 \<in> A
(x0 \<in> A) = (\<exists>z. pA x0 z = 0)
[PROOF STEP]
obtain z0 where LL_5: "pA x0 z0 = 0"
[PROOF STATE]
proof (prove)
using this:
x0 \<in> A
(x0 \<in> A) = (\<exists>z. pA x0 z = 0)

goal (1 subgoal):
 1. (\<And>z0. pA x0 z0 = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pA x0 z0 = 0

goal (2 subgoals):
 1. y \<in> {p x |x. x \<in> A} \<Longrightarrow> \<exists>z. q y z = 0
 2. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
define t where "t = c_pair z0 x0"
[PROOF STATE]
proof (state)
this:
t = c_pair z0 x0

goal (2 subgoals):
 1. y \<in> {p x |x. x \<in> A} \<Longrightarrow> \<exists>z. q y z = 0
 2. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
from t_def q_def LL_3 LL_5
[PROOF STATE]
proof (chain)
picking this:
t = c_pair z0 x0
q ?y ?t = (if ?y = p (c_snd ?t) then pA (c_snd ?t) (c_fst ?t) else 1)
y = p x0
pA x0 z0 = 0
[PROOF STEP]
have "q y t = 0"
[PROOF STATE]
proof (prove)
using this:
t = c_pair z0 x0
q ?y ?t = (if ?y = p (c_snd ?t) then pA (c_snd ?t) (c_fst ?t) else 1)
y = p x0
pA x0 z0 = 0

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

goal (2 subgoals):
 1. y \<in> {p x |x. x \<in> A} \<Longrightarrow> \<exists>z. q y z = 0
 2. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q y t = 0
[PROOF STEP]
show "\<exists> z. q y z = 0"
[PROOF STATE]
proof (prove)
using this:
q y t = 0

goal (1 subgoal):
 1. \<exists>z. q y z = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>z. q y z = 0

goal (1 subgoal):
 1. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
assume A1: "\<exists> z. q y z = 0"
[PROOF STATE]
proof (state)
this:
\<exists>z. q y z = 0

goal (1 subgoal):
 1. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>z. q y z = 0
[PROOF STEP]
obtain z0 where LL_1: "q y z0 = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>z. q y z = 0

goal (1 subgoal):
 1. (\<And>z0. q y z0 = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
q y z0 = 0

goal (1 subgoal):
 1. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
have LL2: "y = p (c_snd z0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = p (c_snd z0)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> p (c_snd z0) \<Longrightarrow> False
[PROOF STEP]
assume "y \<noteq> p (c_snd z0)"
[PROOF STATE]
proof (state)
this:
y \<noteq> p (c_snd z0)

goal (1 subgoal):
 1. y \<noteq> p (c_snd z0) \<Longrightarrow> False
[PROOF STEP]
with q_def LL_1
[PROOF STATE]
proof (chain)
picking this:
q ?y ?t = (if ?y = p (c_snd ?t) then pA (c_snd ?t) (c_fst ?t) else 1)
q y z0 = 0
y \<noteq> p (c_snd z0)
[PROOF STEP]
have "q y z0 = 1"
[PROOF STATE]
proof (prove)
using this:
q ?y ?t = (if ?y = p (c_snd ?t) then pA (c_snd ?t) (c_fst ?t) else 1)
q y z0 = 0
y \<noteq> p (c_snd z0)

goal (1 subgoal):
 1. q y z0 = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q y z0 = 1

goal (1 subgoal):
 1. y \<noteq> p (c_snd z0) \<Longrightarrow> False
[PROOF STEP]
with LL_1
[PROOF STATE]
proof (chain)
picking this:
q y z0 = 0
q y z0 = 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
q y z0 = 0
q y z0 = 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y = p (c_snd z0)

goal (1 subgoal):
 1. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
from LL2 LL_1 q_def
[PROOF STATE]
proof (chain)
picking this:
y = p (c_snd z0)
q y z0 = 0
q ?y ?t = (if ?y = p (c_snd ?t) then pA (c_snd ?t) (c_fst ?t) else 1)
[PROOF STEP]
have LL3: "pA (c_snd z0) (c_fst z0) = 0"
[PROOF STATE]
proof (prove)
using this:
y = p (c_snd z0)
q y z0 = 0
q ?y ?t = (if ?y = p (c_snd ?t) then pA (c_snd ?t) (c_fst ?t) else 1)

goal (1 subgoal):
 1. pA (c_snd z0) (c_fst z0) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pA (c_snd z0) (c_fst z0) = 0

goal (1 subgoal):
 1. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
with S3
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. pA x y = 0}
pA (c_snd z0) (c_fst z0) = 0
[PROOF STEP]
have LL4: "c_snd z0 \<in> A"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. pA x y = 0}
pA (c_snd z0) (c_fst z0) = 0

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

goal (1 subgoal):
 1. \<exists>z. q y z = 0 \<Longrightarrow> y \<in> {p x |x. x \<in> A}
[PROOF STEP]
with LL2
[PROOF STATE]
proof (chain)
picking this:
y = p (c_snd z0)
c_snd z0 \<in> A
[PROOF STEP]
show "y \<in> {p x | x. x \<in> A}"
[PROOF STATE]
proof (prove)
using this:
y = p (c_snd z0)
c_snd z0 \<in> A

goal (1 subgoal):
 1. y \<in> {p x |x. x \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> {p x |x. x \<in> A}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(y \<in> {p x |x. x \<in> A}) = (\<exists>z. q y z = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?y \<in> {p x |x. x \<in> A}) = (\<exists>z. q ?y z = 0)

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?y \<in> {p x |x. x \<in> A}) = (\<exists>z. q ?y z = 0)
[PROOF STEP]
have L2: "?B = { y | y. \<exists> z. q y z = 0}"
[PROOF STATE]
proof (prove)
using this:
(?y \<in> {p x |x. x \<in> A}) = (\<exists>z. q ?y z = 0)

goal (1 subgoal):
 1. {p x |x. x \<in> A} = {y |y. \<exists>z. q y z = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{p x |x. x \<in> A} = {y |y. \<exists>z. q y z = 0}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
with fn_to_set_def
[PROOF STATE]
proof (chain)
picking this:
fn_to_set ?f = {x. \<exists>y. ?f x y = 0}
{p x |x. x \<in> A} = {y |y. \<exists>z. q y z = 0}
[PROOF STEP]
have "?B = fn_to_set q"
[PROOF STATE]
proof (prove)
using this:
fn_to_set ?f = {x. \<exists>y. ?f x y = 0}
{p x |x. x \<in> A} = {y |y. \<exists>z. q y z = 0}

goal (1 subgoal):
 1. {p x |x. x \<in> A} = fn_to_set q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{p x |x. x \<in> A} = fn_to_set q

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; p \<in> PrimRec1\<rbrakk> \<Longrightarrow> {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
with q_is_pr ce_set_lm_1
[PROOF STATE]
proof (chain)
picking this:
q \<in> PrimRec2
?p \<in> PrimRec2 \<Longrightarrow> fn_to_set ?p \<in> ce_sets
{p x |x. x \<in> A} = fn_to_set q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<in> PrimRec2
?p \<in> PrimRec2 \<Longrightarrow> fn_to_set ?p \<in> ce_sets
{p x |x. x \<in> A} = fn_to_set q

goal (1 subgoal):
 1. {p x |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{p x |x. x \<in> A} \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ce_univ: "UNIV \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
let ?f = "(\<lambda> x a. (0::nat))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
have S1: "?f \<in> PrimRec2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x a. 0) \<in> PrimRec2
[PROOF STEP]
by (rule const_is_pr_2)
[PROOF STATE]
proof (state)
this:
(\<lambda>x a. 0) \<in> PrimRec2

goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x a. 0) \<in> PrimRec2
[PROOF STEP]
have "\<forall> x a. ?f x a = 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x a. 0) \<in> PrimRec2

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

goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x a. 0 = 0
[PROOF STEP]
have "{x. \<exists> a. ?f x a = 0 }=UNIV"
[PROOF STATE]
proof (prove)
using this:
\<forall>x a. 0 = 0

goal (1 subgoal):
 1. {x. \<exists>a. 0 = 0} = UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. \<exists>a. 0 = 0} = UNIV

goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{x. \<exists>a. 0 = 0} = UNIV

goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
have "fn_to_set ?f = \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fn_to_set (\<lambda>x a. 0) = UNIV
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
fn_to_set (\<lambda>x a. 0) = UNIV

goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
with S1
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x a. 0) \<in> PrimRec2
fn_to_set (\<lambda>x a. 0) = UNIV
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x a. 0) \<in> PrimRec2
fn_to_set (\<lambda>x a. 0) = UNIV

goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
by (auto simp add: ce_sets_def)
[PROOF STATE]
proof (state)
this:
UNIV \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ce_singleton: "{a} \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a} \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a} \<in> ce_sets
[PROOF STEP]
let ?f = "\<lambda> x y. (abs_of_diff x a) + y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a} \<in> ce_sets
[PROOF STEP]
have S1: "?f \<in> PrimRec2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. (+) (abs_of_diff x a)) \<in> PrimRec2
[PROOF STEP]
using const_is_pr_2 [where ?n="a"]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x y. a) \<in> PrimRec2

goal (1 subgoal):
 1. (\<lambda>x. (+) (abs_of_diff x a)) \<in> PrimRec2
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (+) (abs_of_diff x a)) \<in> PrimRec2

goal (1 subgoal):
 1. {a} \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. (+) (abs_of_diff x a)) \<in> PrimRec2
[PROOF STEP]
have "\<forall> x y. (?f x y = 0) = (x=a \<and> y=0)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (+) (abs_of_diff x a)) \<in> PrimRec2

goal (1 subgoal):
 1. \<forall>x y. (abs_of_diff x a + y = 0) = (x = a \<and> y = 0)
[PROOF STEP]
by (simp add: abs_of_diff_eq)
[PROOF STATE]
proof (state)
this:
\<forall>x y. (abs_of_diff x a + y = 0) = (x = a \<and> y = 0)

goal (1 subgoal):
 1. {a} \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. (abs_of_diff x a + y = 0) = (x = a \<and> y = 0)
[PROOF STEP]
have S2: "{x. \<exists> y. ?f x y = 0 }={a}"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. (abs_of_diff x a + y = 0) = (x = a \<and> y = 0)

goal (1 subgoal):
 1. {x. \<exists>y. abs_of_diff x a + y = 0} = {a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. \<exists>y. abs_of_diff x a + y = 0} = {a}

goal (1 subgoal):
 1. {a} \<in> ce_sets
[PROOF STEP]
have "fn_to_set ?f = {x. \<exists> y. ?f x y = 0 }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fn_to_set (\<lambda>x. (+) (abs_of_diff x a)) = {x. \<exists>y. abs_of_diff x a + y = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
fn_to_set (\<lambda>x. (+) (abs_of_diff x a)) = {x. \<exists>y. abs_of_diff x a + y = 0}

goal (1 subgoal):
 1. {a} \<in> ce_sets
[PROOF STEP]
with S2
[PROOF STATE]
proof (chain)
picking this:
{x. \<exists>y. abs_of_diff x a + y = 0} = {a}
fn_to_set (\<lambda>x. (+) (abs_of_diff x a)) = {x. \<exists>y. abs_of_diff x a + y = 0}
[PROOF STEP]
have "fn_to_set ?f = {a}"
[PROOF STATE]
proof (prove)
using this:
{x. \<exists>y. abs_of_diff x a + y = 0} = {a}
fn_to_set (\<lambda>x. (+) (abs_of_diff x a)) = {x. \<exists>y. abs_of_diff x a + y = 0}

goal (1 subgoal):
 1. fn_to_set (\<lambda>x. (+) (abs_of_diff x a)) = {a}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fn_to_set (\<lambda>x. (+) (abs_of_diff x a)) = {a}

goal (1 subgoal):
 1. {a} \<in> ce_sets
[PROOF STEP]
with S1
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. (+) (abs_of_diff x a)) \<in> PrimRec2
fn_to_set (\<lambda>x. (+) (abs_of_diff x a)) = {a}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (+) (abs_of_diff x a)) \<in> PrimRec2
fn_to_set (\<lambda>x. (+) (abs_of_diff x a)) = {a}

goal (1 subgoal):
 1. {a} \<in> ce_sets
[PROOF STEP]
by (auto simp add: ce_sets_def)
[PROOF STATE]
proof (state)
this:
{a} \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ce_union: "\<lbrakk> A \<in> ce_sets; B \<in> ce_sets \<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
assume A1: "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
obtain p_a where S2: "p_a \<in> PrimRec2" and S3: "A = fn_to_set p_a"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

goal (1 subgoal):
 1. (\<And>p_a. \<lbrakk>p_a \<in> PrimRec2; A = fn_to_set p_a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: ce_sets_def)
[PROOF STATE]
proof (state)
this:
p_a \<in> PrimRec2
A = fn_to_set p_a

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
assume A2: "B \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
B \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<in> ce_sets
[PROOF STEP]
obtain p_b where S5: "p_b \<in> PrimRec2" and S6: "B = fn_to_set p_b"
[PROOF STATE]
proof (prove)
using this:
B \<in> ce_sets

goal (1 subgoal):
 1. (\<And>p_b. \<lbrakk>p_b \<in> PrimRec2; B = fn_to_set p_b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: ce_sets_def)
[PROOF STATE]
proof (state)
this:
p_b \<in> PrimRec2
B = fn_to_set p_b

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
let ?p = "(\<lambda> x y. (p_a x y) * (p_b x y))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
from S2 S5
[PROOF STATE]
proof (chain)
picking this:
p_a \<in> PrimRec2
p_b \<in> PrimRec2
[PROOF STEP]
have S7: "?p \<in> PrimRec2"
[PROOF STATE]
proof (prove)
using this:
p_a \<in> PrimRec2
p_b \<in> PrimRec2

goal (1 subgoal):
 1. (\<lambda>x y. p_a x y * p_b x y) \<in> PrimRec2
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
(\<lambda>x y. p_a x y * p_b x y) \<in> PrimRec2

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
have S8: "\<forall> x y. (?p x y = 0) = ((p_a x y = 0) \<or> (p_b x y = 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. (p_a x y * p_b x y = 0) = (p_a x y = 0 \<or> p_b x y = 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x y. (p_a x y * p_b x y = 0) = (p_a x y = 0 \<or> p_b x y = 0)

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
let ?C = "fn_to_set ?p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
have S9: "?C = {x. \<exists> y. ?p x y = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fn_to_set (\<lambda>x y. p_a x y * p_b x y) = {x. \<exists>y. p_a x y * p_b x y = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
fn_to_set (\<lambda>x y. p_a x y * p_b x y) = {x. \<exists>y. p_a x y * p_b x y = 0}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
from S3
[PROOF STATE]
proof (chain)
picking this:
A = fn_to_set p_a
[PROOF STEP]
have S10: "A = {x. \<exists> y. p_a x y = 0}"
[PROOF STATE]
proof (prove)
using this:
A = fn_to_set p_a

goal (1 subgoal):
 1. A = {x. \<exists>y. p_a x y = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
A = {x. \<exists>y. p_a x y = 0}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
from S6
[PROOF STATE]
proof (chain)
picking this:
B = fn_to_set p_b
[PROOF STEP]
have S11: "B = {x. \<exists> y. p_b x y = 0}"
[PROOF STATE]
proof (prove)
using this:
B = fn_to_set p_b

goal (1 subgoal):
 1. B = {x. \<exists>y. p_b x y = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
B = {x. \<exists>y. p_b x y = 0}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
from S10 S11 S9 S8
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. p_a x y = 0}
B = {x. \<exists>y. p_b x y = 0}
fn_to_set (\<lambda>x y. p_a x y * p_b x y) = {x. \<exists>y. p_a x y * p_b x y = 0}
\<forall>x y. (p_a x y * p_b x y = 0) = (p_a x y = 0 \<or> p_b x y = 0)
[PROOF STEP]
have S12: "?C = A \<union> B"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. p_a x y = 0}
B = {x. \<exists>y. p_b x y = 0}
fn_to_set (\<lambda>x y. p_a x y * p_b x y) = {x. \<exists>y. p_a x y * p_b x y = 0}
\<forall>x y. (p_a x y * p_b x y = 0) = (p_a x y = 0 \<or> p_b x y = 0)

goal (1 subgoal):
 1. fn_to_set (\<lambda>x y. p_a x y * p_b x y) = A \<union> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fn_to_set (\<lambda>x y. p_a x y * p_b x y) = A \<union> B

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
from S7
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x y. p_a x y * p_b x y) \<in> PrimRec2
[PROOF STEP]
have "?C \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x y. p_a x y * p_b x y) \<in> PrimRec2

goal (1 subgoal):
 1. fn_to_set (\<lambda>x y. p_a x y * p_b x y) \<in> ce_sets
[PROOF STEP]
by (auto simp add: ce_sets_def)
[PROOF STATE]
proof (state)
this:
fn_to_set (\<lambda>x y. p_a x y * p_b x y) \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<union> B \<in> ce_sets
[PROOF STEP]
with S12
[PROOF STATE]
proof (chain)
picking this:
fn_to_set (\<lambda>x y. p_a x y * p_b x y) = A \<union> B
fn_to_set (\<lambda>x y. p_a x y * p_b x y) \<in> ce_sets
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fn_to_set (\<lambda>x y. p_a x y * p_b x y) = A \<union> B
fn_to_set (\<lambda>x y. p_a x y * p_b x y) \<in> ce_sets

goal (1 subgoal):
 1. A \<union> B \<in> ce_sets
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A \<union> B \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ce_intersect: "\<lbrakk> A \<in> ce_sets; B \<in> ce_sets \<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
assume A1: "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
obtain p_a where S2: "p_a \<in> PrimRec2" and S3: "A = fn_to_set p_a"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

goal (1 subgoal):
 1. (\<And>p_a. \<lbrakk>p_a \<in> PrimRec2; A = fn_to_set p_a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: ce_sets_def)
[PROOF STATE]
proof (state)
this:
p_a \<in> PrimRec2
A = fn_to_set p_a

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
assume A2: "B \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
B \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<in> ce_sets
[PROOF STEP]
obtain p_b where S5: "p_b \<in> PrimRec2" and S6: "B = fn_to_set p_b"
[PROOF STATE]
proof (prove)
using this:
B \<in> ce_sets

goal (1 subgoal):
 1. (\<And>p_b. \<lbrakk>p_b \<in> PrimRec2; B = fn_to_set p_b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: ce_sets_def)
[PROOF STATE]
proof (state)
this:
p_b \<in> PrimRec2
B = fn_to_set p_b

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
let ?p = "(\<lambda> x y. (p_a x (c_fst y)) + (p_b x (c_snd y)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
from S2 S5
[PROOF STATE]
proof (chain)
picking this:
p_a \<in> PrimRec2
p_b \<in> PrimRec2
[PROOF STEP]
have S7: "?p \<in> PrimRec2"
[PROOF STATE]
proof (prove)
using this:
p_a \<in> PrimRec2
p_b \<in> PrimRec2

goal (1 subgoal):
 1. (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) \<in> PrimRec2
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
(\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) \<in> PrimRec2

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
have S8: "\<forall> x. (\<exists> y. ?p x y = 0) = ((\<exists> z. p_a x z = 0) \<and> (\<exists> z. p_b x z = 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
show "(\<exists> y. ?p x y = 0) = ((\<exists> z. p_a x z = 0) \<and> (\<exists> z. p_b x z = 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
have 1: "(\<exists> y. ?p x y = 0) \<Longrightarrow> ((\<exists> z. p_a x z = 0) \<and> (\<exists> z. p_b x z = 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0 \<Longrightarrow> (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0 \<Longrightarrow> (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0)

goal (1 subgoal):
 1. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
have 2: "((\<exists> z. p_a x z = 0) \<and> (\<exists> z. p_b x z = 0)) \<Longrightarrow> (\<exists> y. ?p x y = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0) \<Longrightarrow> \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0) \<Longrightarrow> \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0
[PROOF STEP]
assume "((\<exists> z. p_a x z = 0) \<and> (\<exists> z. p_b x z = 0))"
[PROOF STATE]
proof (state)
this:
(\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0)

goal (1 subgoal):
 1. (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0) \<Longrightarrow> \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0)
[PROOF STEP]
obtain z1 z2 where s_23: "p_a x z1 = 0" and s_24: "p_b x z2 = 0"
[PROOF STATE]
proof (prove)
using this:
(\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0)

goal (1 subgoal):
 1. (\<And>z1 z2. \<lbrakk>p_a x z1 = 0; p_b x z2 = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_a x z1 = 0
p_b x z2 = 0

goal (1 subgoal):
 1. (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0) \<Longrightarrow> \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0
[PROOF STEP]
let ?y1 = "c_pair z1 z2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0) \<Longrightarrow> \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0
[PROOF STEP]
from s_23
[PROOF STATE]
proof (chain)
picking this:
p_a x z1 = 0
[PROOF STEP]
have s_25: "p_a x (c_fst ?y1) = 0"
[PROOF STATE]
proof (prove)
using this:
p_a x z1 = 0

goal (1 subgoal):
 1. p_a x (c_fst (c_pair z1 z2)) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p_a x (c_fst (c_pair z1 z2)) = 0

goal (1 subgoal):
 1. (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0) \<Longrightarrow> \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0
[PROOF STEP]
from s_24
[PROOF STATE]
proof (chain)
picking this:
p_b x z2 = 0
[PROOF STEP]
have s_26: "p_b x (c_snd ?y1) = 0"
[PROOF STATE]
proof (prove)
using this:
p_b x z2 = 0

goal (1 subgoal):
 1. p_b x (c_snd (c_pair z1 z2)) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p_b x (c_snd (c_pair z1 z2)) = 0

goal (1 subgoal):
 1. (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0) \<Longrightarrow> \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0
[PROOF STEP]
from s_25 s_26
[PROOF STATE]
proof (chain)
picking this:
p_a x (c_fst (c_pair z1 z2)) = 0
p_b x (c_snd (c_pair z1 z2)) = 0
[PROOF STEP]
have s_27: "p_a x (c_fst ?y1) + p_b x (c_snd ?y1) = 0"
[PROOF STATE]
proof (prove)
using this:
p_a x (c_fst (c_pair z1 z2)) = 0
p_b x (c_snd (c_pair z1 z2)) = 0

goal (1 subgoal):
 1. p_a x (c_fst (c_pair z1 z2)) + p_b x (c_snd (c_pair z1 z2)) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p_a x (c_fst (c_pair z1 z2)) + p_b x (c_snd (c_pair z1 z2)) = 0

goal (1 subgoal):
 1. (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0) \<Longrightarrow> \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p_a x (c_fst (c_pair z1 z2)) + p_b x (c_snd (c_pair z1 z2)) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p_a x (c_fst (c_pair z1 z2)) + p_b x (c_snd (c_pair z1 z2)) = 0

goal (1 subgoal):
 1. \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0) \<Longrightarrow> \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0

goal (1 subgoal):
 1. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0 \<Longrightarrow> (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0)
(\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0) \<Longrightarrow> \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0
[PROOF STEP]
have "(\<exists> y. ?p x y = 0) = ((\<exists> z. p_a x z = 0) \<and> (\<exists> z. p_b x z = 0))"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0 \<Longrightarrow> (\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0)
(\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0) \<Longrightarrow> \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0

goal (1 subgoal):
 1. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
by (rule iffI)
[PROOF STATE]
proof (state)
this:
(\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))

goal (1 subgoal):
 1. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))

goal (1 subgoal):
 1. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
let ?C = "fn_to_set ?p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
have S9: "?C = {x. \<exists> y. ?p x y = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) = {x. \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) = {x. \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
from S3
[PROOF STATE]
proof (chain)
picking this:
A = fn_to_set p_a
[PROOF STEP]
have S10: "A = {x. \<exists> y. p_a x y = 0}"
[PROOF STATE]
proof (prove)
using this:
A = fn_to_set p_a

goal (1 subgoal):
 1. A = {x. \<exists>y. p_a x y = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
A = {x. \<exists>y. p_a x y = 0}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
from S6
[PROOF STATE]
proof (chain)
picking this:
B = fn_to_set p_b
[PROOF STEP]
have S11: "B = {x. \<exists> y. p_b x y = 0}"
[PROOF STATE]
proof (prove)
using this:
B = fn_to_set p_b

goal (1 subgoal):
 1. B = {x. \<exists>y. p_b x y = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
B = {x. \<exists>y. p_b x y = 0}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
from S10 S11 S9 S8
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. p_a x y = 0}
B = {x. \<exists>y. p_b x y = 0}
fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) = {x. \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0}
\<forall>x. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))
[PROOF STEP]
have S12: "?C = A \<inter> B"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. p_a x y = 0}
B = {x. \<exists>y. p_b x y = 0}
fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) = {x. \<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0}
\<forall>x. (\<exists>y. p_a x (c_fst y) + p_b x (c_snd y) = 0) = ((\<exists>z. p_a x z = 0) \<and> (\<exists>z. p_b x z = 0))

goal (1 subgoal):
 1. fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) = A \<inter> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) = A \<inter> B

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
from S7
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) \<in> PrimRec2
[PROOF STEP]
have "?C \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) \<in> PrimRec2

goal (1 subgoal):
 1. fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) \<in> ce_sets
[PROOF STEP]
by (auto simp add: ce_sets_def)
[PROOF STATE]
proof (state)
this:
fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<inter> B \<in> ce_sets
[PROOF STEP]
with S12
[PROOF STATE]
proof (chain)
picking this:
fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) = A \<inter> B
fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) \<in> ce_sets
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) = A \<inter> B
fn_to_set (\<lambda>x y. p_a x (c_fst y) + p_b x (c_snd y)) \<in> ce_sets

goal (1 subgoal):
 1. A \<inter> B \<in> ce_sets
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A \<inter> B \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_to_ce_set_lm_1: "nat_to_ce_set n = { x . \<exists> y. (nat_to_pr n) (c_pair x y) = 0 }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_ce_set n = {x. \<exists>y. nat_to_pr n (c_pair x y) = 0}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nat_to_ce_set n = {x. \<exists>y. nat_to_pr n (c_pair x y) = 0}
[PROOF STEP]
have S1: "nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))
[PROOF STEP]
by (simp add: nat_to_ce_set_def)
[PROOF STATE]
proof (state)
this:
nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))

goal (1 subgoal):
 1. nat_to_ce_set n = {x. \<exists>y. nat_to_pr n (c_pair x y) = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))
[PROOF STEP]
have S2: "nat_to_ce_set n = { x . \<exists> y. (pr_conv_1_to_2 (nat_to_pr n)) x y = 0}"
[PROOF STATE]
proof (prove)
using this:
nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))

goal (1 subgoal):
 1. nat_to_ce_set n = {x. \<exists>y. pr_conv_1_to_2 (nat_to_pr n) x y = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
nat_to_ce_set n = {x. \<exists>y. pr_conv_1_to_2 (nat_to_pr n) x y = 0}

goal (1 subgoal):
 1. nat_to_ce_set n = {x. \<exists>y. nat_to_pr n (c_pair x y) = 0}
[PROOF STEP]
have S3: "\<And> x y. (pr_conv_1_to_2 (nat_to_pr n)) x y = (nat_to_pr n) (c_pair x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. pr_conv_1_to_2 (nat_to_pr n) x y = nat_to_pr n (c_pair x y)
[PROOF STEP]
by (simp add: pr_conv_1_to_2_def)
[PROOF STATE]
proof (state)
this:
pr_conv_1_to_2 (nat_to_pr n) ?x ?y = nat_to_pr n (c_pair ?x ?y)

goal (1 subgoal):
 1. nat_to_ce_set n = {x. \<exists>y. nat_to_pr n (c_pair x y) = 0}
[PROOF STEP]
from S2 S3
[PROOF STATE]
proof (chain)
picking this:
nat_to_ce_set n = {x. \<exists>y. pr_conv_1_to_2 (nat_to_pr n) x y = 0}
pr_conv_1_to_2 (nat_to_pr n) ?x ?y = nat_to_pr n (c_pair ?x ?y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nat_to_ce_set n = {x. \<exists>y. pr_conv_1_to_2 (nat_to_pr n) x y = 0}
pr_conv_1_to_2 (nat_to_pr n) ?x ?y = nat_to_pr n (c_pair ?x ?y)

goal (1 subgoal):
 1. nat_to_ce_set n = {x. \<exists>y. nat_to_pr n (c_pair x y) = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat_to_ce_set n = {x. \<exists>y. nat_to_pr n (c_pair x y) = 0}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_to_ce_set_into_ce: "nat_to_ce_set n \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_ce_set n \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nat_to_ce_set n \<in> ce_sets
[PROOF STEP]
have S1: "nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))
[PROOF STEP]
by (simp add: nat_to_ce_set_def)
[PROOF STATE]
proof (state)
this:
nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))

goal (1 subgoal):
 1. nat_to_ce_set n \<in> ce_sets
[PROOF STEP]
have "(nat_to_pr n) \<in> PrimRec1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_pr n \<in> PrimRec1
[PROOF STEP]
by (rule nat_to_pr_into_pr)
[PROOF STATE]
proof (state)
this:
nat_to_pr n \<in> PrimRec1

goal (1 subgoal):
 1. nat_to_ce_set n \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_to_pr n \<in> PrimRec1
[PROOF STEP]
have S2: "(pr_conv_1_to_2 (nat_to_pr n)) \<in> PrimRec2"
[PROOF STATE]
proof (prove)
using this:
nat_to_pr n \<in> PrimRec1

goal (1 subgoal):
 1. pr_conv_1_to_2 (nat_to_pr n) \<in> PrimRec2
[PROOF STEP]
by (rule pr_conv_1_to_2_lm)
[PROOF STATE]
proof (state)
this:
pr_conv_1_to_2 (nat_to_pr n) \<in> PrimRec2

goal (1 subgoal):
 1. nat_to_ce_set n \<in> ce_sets
[PROOF STEP]
from S2 S1
[PROOF STATE]
proof (chain)
picking this:
pr_conv_1_to_2 (nat_to_pr n) \<in> PrimRec2
nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pr_conv_1_to_2 (nat_to_pr n) \<in> PrimRec2
nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))

goal (1 subgoal):
 1. nat_to_ce_set n \<in> ce_sets
[PROOF STEP]
by (simp add: ce_set_lm_1)
[PROOF STATE]
proof (state)
this:
nat_to_ce_set n \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_to_ce_set_srj: "A \<in> ce_sets \<Longrightarrow> \<exists> n. A = nat_to_ce_set n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
assume A: "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
have "\<exists> p \<in> PrimRec2. A = fn_to_set p"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<exists>p\<in>PrimRec2. A = fn_to_set p
[PROOF STEP]
by (rule ce_set_lm_3)
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>PrimRec2. A = fn_to_set p

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p\<in>PrimRec2. A = fn_to_set p
[PROOF STEP]
obtain p where p_is_pr: "p \<in> PrimRec2" and S1: "A = fn_to_set p"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>PrimRec2. A = fn_to_set p

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> PrimRec2; A = fn_to_set p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec2
A = fn_to_set p

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
define q where "q = pr_conv_2_to_1 p"
[PROOF STATE]
proof (state)
this:
q = pr_conv_2_to_1 p

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
from p_is_pr
[PROOF STATE]
proof (chain)
picking this:
p \<in> PrimRec2
[PROOF STEP]
have q_is_pr: "q \<in> PrimRec1"
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec2

goal (1 subgoal):
 1. q \<in> PrimRec1
[PROOF STEP]
by (unfold q_def, rule pr_conv_2_to_1_lm)
[PROOF STATE]
proof (state)
this:
q \<in> PrimRec1

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
from q_def
[PROOF STATE]
proof (chain)
picking this:
q = pr_conv_2_to_1 p
[PROOF STEP]
have S2: "pr_conv_1_to_2 q = p"
[PROOF STATE]
proof (prove)
using this:
q = pr_conv_2_to_1 p

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

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
let ?n = "index_of_pr q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
from q_is_pr
[PROOF STATE]
proof (chain)
picking this:
q \<in> PrimRec1
[PROOF STEP]
have "nat_to_pr ?n = q"
[PROOF STATE]
proof (prove)
using this:
q \<in> PrimRec1

goal (1 subgoal):
 1. nat_to_pr (index_of_pr q) = q
[PROOF STEP]
by (rule index_of_pr_is_real)
[PROOF STATE]
proof (state)
this:
nat_to_pr (index_of_pr q) = q

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
with S2 S1
[PROOF STATE]
proof (chain)
picking this:
pr_conv_1_to_2 q = p
A = fn_to_set p
nat_to_pr (index_of_pr q) = q
[PROOF STEP]
have "A = fn_to_set (pr_conv_1_to_2 (nat_to_pr ?n))"
[PROOF STATE]
proof (prove)
using this:
pr_conv_1_to_2 q = p
A = fn_to_set p
nat_to_pr (index_of_pr q) = q

goal (1 subgoal):
 1. A = fn_to_set (pr_conv_1_to_2 (nat_to_pr (index_of_pr q)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = fn_to_set (pr_conv_1_to_2 (nat_to_pr (index_of_pr q)))

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = fn_to_set (pr_conv_1_to_2 (nat_to_pr (index_of_pr q)))
[PROOF STEP]
have "A = nat_to_ce_set ?n"
[PROOF STATE]
proof (prove)
using this:
A = fn_to_set (pr_conv_1_to_2 (nat_to_pr (index_of_pr q)))

goal (1 subgoal):
 1. A = nat_to_ce_set (index_of_pr q)
[PROOF STEP]
by (simp add: nat_to_ce_set_def)
[PROOF STATE]
proof (state)
this:
A = nat_to_ce_set (index_of_pr q)

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A = nat_to_ce_set (index_of_pr q)

goal (1 subgoal):
 1. \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>n. A = nat_to_ce_set n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chf_lm_1 [simp]: "zero_set (chf A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_set (chf A) = A
[PROOF STEP]
by (unfold chf_def, unfold zero_set_def, simp)


[STATEMENT]
lemma chf_lm_2: "(x \<in> A) = (chf A x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> A) = (chf A x = 0)
[PROOF STEP]
by (unfold chf_def, simp)


[STATEMENT]
lemma chf_lm_3: "(x \<notin> A) = (chf A x = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<notin> A) = (chf A x = 1)
[PROOF STEP]
by (unfold chf_def, simp)


[STATEMENT]
lemma chf_lm_4: "chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
assume A: "chf A \<in> PrimRec1"
[PROOF STATE]
proof (state)
this:
chf A \<in> PrimRec1

goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
define p where "p = chf A"
[PROOF STATE]
proof (state)
this:
p = chf A

goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
from A p_def
[PROOF STATE]
proof (chain)
picking this:
chf A \<in> PrimRec1
p = chf A
[PROOF STEP]
have p_is_pr: "p \<in> PrimRec1"
[PROOF STATE]
proof (prove)
using this:
chf A \<in> PrimRec1
p = chf A

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

goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
define q where "q x y = p x" for x y :: nat
[PROOF STATE]
proof (state)
this:
q ?x ?y = p ?x

goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
from p_is_pr
[PROOF STATE]
proof (chain)
picking this:
p \<in> PrimRec1
[PROOF STEP]
have q_is_pr: "q \<in> PrimRec2"
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec1

goal (1 subgoal):
 1. q \<in> PrimRec2
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec1

goal (1 subgoal):
 1. (\<lambda>x y. p x) \<in> PrimRec2
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
q \<in> PrimRec2

goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
have S1: "A = {x. p(x) = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = {x. p x = 0}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A = {x. p x = 0}
[PROOF STEP]
have "zero_set p = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_set p = A
[PROOF STEP]
by (unfold p_def, simp)
[PROOF STATE]
proof (state)
this:
zero_set p = A

goal (1 subgoal):
 1. A = {x. p x = 0}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
zero_set p = A

goal (1 subgoal):
 1. A = {x. p x = 0}
[PROOF STEP]
by (simp add: zero_set_def)
[PROOF STATE]
proof (state)
this:
A = {x. p x = 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A = {x. p x = 0}

goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
have S2: "fn_to_set q = {x. \<exists> y. q x y = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fn_to_set q = {x. \<exists>y. q x y = 0}
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
fn_to_set q = {x. \<exists>y. q x y = 0}

goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
have S3: "\<And> x. (p x = 0) = (\<exists> y. q x y = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (p x = 0) = (\<exists>y. q x y = 0)
[PROOF STEP]
by (unfold q_def, auto)
[PROOF STATE]
proof (state)
this:
(p ?x = 0) = (\<exists>y. q ?x y = 0)

goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p ?x = 0) = (\<exists>y. q ?x y = 0)
[PROOF STEP]
have S4: "{x. p x = 0} = {x. \<exists> y. q x y = 0}"
[PROOF STATE]
proof (prove)
using this:
(p ?x = 0) = (\<exists>y. q ?x y = 0)

goal (1 subgoal):
 1. {x. p x = 0} = {x. \<exists>y. q x y = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. p x = 0} = {x. \<exists>y. q x y = 0}

goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
with S1 S2
[PROOF STATE]
proof (chain)
picking this:
A = {x. p x = 0}
fn_to_set q = {x. \<exists>y. q x y = 0}
{x. p x = 0} = {x. \<exists>y. q x y = 0}
[PROOF STEP]
have S5: "fn_to_set q = A"
[PROOF STATE]
proof (prove)
using this:
A = {x. p x = 0}
fn_to_set q = {x. \<exists>y. q x y = 0}
{x. p x = 0} = {x. \<exists>y. q x y = 0}

goal (1 subgoal):
 1. fn_to_set q = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fn_to_set q = A

goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
from q_is_pr
[PROOF STATE]
proof (chain)
picking this:
q \<in> PrimRec2
[PROOF STEP]
have "fn_to_set q \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
q \<in> PrimRec2

goal (1 subgoal):
 1. fn_to_set q \<in> ce_sets
[PROOF STEP]
by (rule ce_set_lm_1)
[PROOF STATE]
proof (state)
this:
fn_to_set q \<in> ce_sets

goal (1 subgoal):
 1. chf A \<in> PrimRec1 \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
with S5
[PROOF STATE]
proof (chain)
picking this:
fn_to_set q = A
fn_to_set q \<in> ce_sets
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fn_to_set q = A
fn_to_set q \<in> ce_sets

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chf_lm_5: "finite A \<Longrightarrow> chf A \<in> PrimRec1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> chf A \<in> PrimRec1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite A \<Longrightarrow> chf A \<in> PrimRec1
[PROOF STEP]
assume A: "finite A"
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. finite A \<Longrightarrow> chf A \<in> PrimRec1
[PROOF STEP]
define u where "u = set_to_nat A"
[PROOF STATE]
proof (state)
this:
u = set_to_nat A

goal (1 subgoal):
 1. finite A \<Longrightarrow> chf A \<in> PrimRec1
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have S1: "nat_to_set u = A"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. nat_to_set u = A
[PROOF STEP]
by (unfold u_def, rule nat_to_set_srj)
[PROOF STATE]
proof (state)
this:
nat_to_set u = A

goal (1 subgoal):
 1. finite A \<Longrightarrow> chf A \<in> PrimRec1
[PROOF STEP]
have "chf A = (\<lambda> x. sgn2 (c_in x u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chf A = (\<lambda>x. sgn2 (c_in x u))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. chf A x = sgn2 (c_in x u)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. chf A x = sgn2 (c_in x u)
[PROOF STEP]
show "chf A x = sgn2 (c_in x u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chf A x = sgn2 (c_in x u)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> chf A x = sgn2 (c_in x u)
 2. \<not> ?P \<Longrightarrow> chf A x = sgn2 (c_in x u)
[PROOF STEP]
assume A: "x \<in> A"
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (2 subgoals):
 1. ?P \<Longrightarrow> chf A x = sgn2 (c_in x u)
 2. \<not> ?P \<Longrightarrow> chf A x = sgn2 (c_in x u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
[PROOF STEP]
have S1_1: "chf A x = 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. chf A x = 0
[PROOF STEP]
by (simp add: chf_lm_2)
[PROOF STATE]
proof (state)
this:
chf A x = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> chf A x = sgn2 (c_in x u)
 2. \<not> ?P \<Longrightarrow> chf A x = sgn2 (c_in x u)
[PROOF STEP]
from A S1
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
nat_to_set u = A
[PROOF STEP]
have "x \<in> nat_to_set u"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
nat_to_set u = A

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> chf A x = sgn2 (c_in x u)
 2. \<not> ?P \<Longrightarrow> chf A x = sgn2 (c_in x u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> nat_to_set u
[PROOF STEP]
have "c_in x u = 1"
[PROOF STATE]
proof (prove)
using this:
x \<in> nat_to_set u

goal (1 subgoal):
 1. c_in x u = 1
[PROOF STEP]
by (simp add: x_in_u_eq)
[PROOF STATE]
proof (state)
this:
c_in x u = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> chf A x = sgn2 (c_in x u)
 2. \<not> ?P \<Longrightarrow> chf A x = sgn2 (c_in x u)
[PROOF STEP]
with S1_1
[PROOF STATE]
proof (chain)
picking this:
chf A x = 0
c_in x u = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
chf A x = 0
c_in x u = 1

goal (1 subgoal):
 1. chf A x = sgn2 (c_in x u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
chf A x = sgn2 (c_in x u)

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = sgn2 (c_in x u)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = sgn2 (c_in x u)
[PROOF STEP]
assume A: "x \<notin> A"
[PROOF STATE]
proof (state)
this:
x \<notin> A

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = sgn2 (c_in x u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> A
[PROOF STEP]
have S1_1: "chf A x = 1"
[PROOF STATE]
proof (prove)
using this:
x \<notin> A

goal (1 subgoal):
 1. chf A x = 1
[PROOF STEP]
by (simp add: chf_def)
[PROOF STATE]
proof (state)
this:
chf A x = 1

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = sgn2 (c_in x u)
[PROOF STEP]
from A S1
[PROOF STATE]
proof (chain)
picking this:
x \<notin> A
nat_to_set u = A
[PROOF STEP]
have "x \<notin> nat_to_set u"
[PROOF STATE]
proof (prove)
using this:
x \<notin> A
nat_to_set u = A

goal (1 subgoal):
 1. x \<notin> nat_to_set u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> nat_to_set u

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = sgn2 (c_in x u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> nat_to_set u
[PROOF STEP]
have "c_in x u = 0"
[PROOF STATE]
proof (prove)
using this:
x \<notin> nat_to_set u

goal (1 subgoal):
 1. c_in x u = 0
[PROOF STEP]
by (simp add: x_in_u_eq c_in_def)
[PROOF STATE]
proof (state)
this:
c_in x u = 0

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = sgn2 (c_in x u)
[PROOF STEP]
with S1_1
[PROOF STATE]
proof (chain)
picking this:
chf A x = 1
c_in x u = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
chf A x = 1
c_in x u = 0

goal (1 subgoal):
 1. chf A x = sgn2 (c_in x u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
chf A x = sgn2 (c_in x u)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
chf A x = sgn2 (c_in x u)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
chf A = (\<lambda>x. sgn2 (c_in x u))

goal (1 subgoal):
 1. finite A \<Longrightarrow> chf A \<in> PrimRec1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
chf A = (\<lambda>x. sgn2 (c_in x u))

goal (1 subgoal):
 1. finite A \<Longrightarrow> chf A \<in> PrimRec1
[PROOF STEP]
from c_in_is_pr
[PROOF STATE]
proof (chain)
picking this:
c_in \<in> PrimRec2
[PROOF STEP]
have "(\<lambda> x. sgn2 (c_in x u)) \<in> PrimRec1"
[PROOF STATE]
proof (prove)
using this:
c_in \<in> PrimRec2

goal (1 subgoal):
 1. (\<lambda>x. sgn2 (c_in x u)) \<in> PrimRec1
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
(\<lambda>x. sgn2 (c_in x u)) \<in> PrimRec1

goal (1 subgoal):
 1. finite A \<Longrightarrow> chf A \<in> PrimRec1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
chf A = (\<lambda>x. sgn2 (c_in x u))
(\<lambda>x. sgn2 (c_in x u)) \<in> PrimRec1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
chf A = (\<lambda>x. sgn2 (c_in x u))
(\<lambda>x. sgn2 (c_in x u)) \<in> PrimRec1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ce_finite: "finite A \<Longrightarrow> A \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite A \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
assume A: "finite A"
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. finite A \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have "chf A \<in> PrimRec1"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. chf A \<in> PrimRec1
[PROOF STEP]
by (rule chf_lm_5)
[PROOF STATE]
proof (state)
this:
chf A \<in> PrimRec1

goal (1 subgoal):
 1. finite A \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
chf A \<in> PrimRec1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
chf A \<in> PrimRec1

goal (1 subgoal):
 1. A \<in> ce_sets
[PROOF STEP]
by (rule chf_lm_4)
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_1 [simp]: "ce_set_to_rel (ce_rel_to_set r) = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_set_to_rel (ce_rel_to_set r) = r
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ce_set_to_rel (ce_rel_to_set r) \<subseteq> r
 2. r \<subseteq> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
show " ce_set_to_rel (ce_rel_to_set r) \<subseteq> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_set_to_rel (ce_rel_to_set r) \<subseteq> r
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ce_set_to_rel (ce_rel_to_set r) \<Longrightarrow> x \<in> r
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ce_set_to_rel (ce_rel_to_set r) \<Longrightarrow> x \<in> r
[PROOF STEP]
assume A: "z \<in> ce_set_to_rel (ce_rel_to_set r)"
[PROOF STATE]
proof (state)
this:
z \<in> ce_set_to_rel (ce_rel_to_set r)

goal (1 subgoal):
 1. \<And>x. x \<in> ce_set_to_rel (ce_rel_to_set r) \<Longrightarrow> x \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
obtain u where L1: "u \<in> (ce_rel_to_set r)" and L2: "z = (c_fst u, c_snd u)"
[PROOF STATE]
proof (prove)
using this:
z \<in> ce_set_to_rel (ce_rel_to_set r)

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u \<in> ce_rel_to_set r; z = (c_fst u, c_snd u)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ce_set_to_rel_def
[PROOF STATE]
proof (prove)
using this:
z \<in> {(c_fst x, c_snd x) |x. x \<in> ce_rel_to_set r}

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u \<in> ce_rel_to_set r; z = (c_fst u, c_snd u)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> ce_rel_to_set r
z = (c_fst u, c_snd u)

goal (1 subgoal):
 1. \<And>x. x \<in> ce_set_to_rel (ce_rel_to_set r) \<Longrightarrow> x \<in> r
[PROOF STEP]
from L1
[PROOF STATE]
proof (chain)
picking this:
u \<in> ce_rel_to_set r
[PROOF STEP]
obtain x y where L3: "(x,y) \<in> r" and L4: "u = c_pair x y"
[PROOF STATE]
proof (prove)
using this:
u \<in> ce_rel_to_set r

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>(x, y) \<in> r; u = c_pair x y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ce_rel_to_set_def
[PROOF STATE]
proof (prove)
using this:
u \<in> {c_pair x y |x y. (x, y) \<in> r}

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>(x, y) \<in> r; u = c_pair x y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r
u = c_pair x y

goal (1 subgoal):
 1. \<And>x. x \<in> ce_set_to_rel (ce_rel_to_set r) \<Longrightarrow> x \<in> r
[PROOF STEP]
from L4
[PROOF STATE]
proof (chain)
picking this:
u = c_pair x y
[PROOF STEP]
have L5: "c_fst u = x"
[PROOF STATE]
proof (prove)
using this:
u = c_pair x y

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

goal (1 subgoal):
 1. \<And>x. x \<in> ce_set_to_rel (ce_rel_to_set r) \<Longrightarrow> x \<in> r
[PROOF STEP]
from L4
[PROOF STATE]
proof (chain)
picking this:
u = c_pair x y
[PROOF STEP]
have L6: "c_snd u = y"
[PROOF STATE]
proof (prove)
using this:
u = c_pair x y

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

goal (1 subgoal):
 1. \<And>x. x \<in> ce_set_to_rel (ce_rel_to_set r) \<Longrightarrow> x \<in> r
[PROOF STEP]
from L5 L6 L2
[PROOF STATE]
proof (chain)
picking this:
c_fst u = x
c_snd u = y
z = (c_fst u, c_snd u)
[PROOF STEP]
have "z = (x,y)"
[PROOF STATE]
proof (prove)
using this:
c_fst u = x
c_snd u = y
z = (c_fst u, c_snd u)

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

goal (1 subgoal):
 1. \<And>x. x \<in> ce_set_to_rel (ce_rel_to_set r) \<Longrightarrow> x \<in> r
[PROOF STEP]
with L3
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> r
z = (x, y)
[PROOF STEP]
show "z \<in> r"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> r
z = (x, y)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ce_set_to_rel (ce_rel_to_set r) \<subseteq> r

goal (1 subgoal):
 1. r \<subseteq> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<subseteq> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
show "r \<subseteq> ce_set_to_rel (ce_rel_to_set r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<subseteq> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> r \<Longrightarrow> x \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> r \<Longrightarrow> x \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
show "z \<in> r \<Longrightarrow> z \<in> ce_set_to_rel (ce_rel_to_set r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> r \<Longrightarrow> z \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<in> r \<Longrightarrow> z \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
assume A: "z \<in> r"
[PROOF STATE]
proof (state)
this:
z \<in> r

goal (1 subgoal):
 1. z \<in> r \<Longrightarrow> z \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
define x where "x = fst z"
[PROOF STATE]
proof (state)
this:
x = fst z

goal (1 subgoal):
 1. z \<in> r \<Longrightarrow> z \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
define y where "y = snd z"
[PROOF STATE]
proof (state)
this:
y = snd z

goal (1 subgoal):
 1. z \<in> r \<Longrightarrow> z \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
from x_def y_def
[PROOF STATE]
proof (chain)
picking this:
x = fst z
y = snd z
[PROOF STEP]
have L1: "z = (x,y)"
[PROOF STATE]
proof (prove)
using this:
x = fst z
y = snd z

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

goal (1 subgoal):
 1. z \<in> r \<Longrightarrow> z \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
define u where "u = c_pair x y"
[PROOF STATE]
proof (state)
this:
u = c_pair x y

goal (1 subgoal):
 1. z \<in> r \<Longrightarrow> z \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
from A L1 u_def
[PROOF STATE]
proof (chain)
picking this:
z \<in> r
z = (x, y)
u = c_pair x y
[PROOF STEP]
have L2: "u \<in> ce_rel_to_set r"
[PROOF STATE]
proof (prove)
using this:
z \<in> r
z = (x, y)
u = c_pair x y

goal (1 subgoal):
 1. u \<in> ce_rel_to_set r
[PROOF STEP]
by (unfold ce_rel_to_set_def, auto)
[PROOF STATE]
proof (state)
this:
u \<in> ce_rel_to_set r

goal (1 subgoal):
 1. z \<in> r \<Longrightarrow> z \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
from L1 u_def
[PROOF STATE]
proof (chain)
picking this:
z = (x, y)
u = c_pair x y
[PROOF STEP]
have L3: "z = (c_fst u, c_snd u)"
[PROOF STATE]
proof (prove)
using this:
z = (x, y)
u = c_pair x y

goal (1 subgoal):
 1. z = (c_fst u, c_snd u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z = (c_fst u, c_snd u)

goal (1 subgoal):
 1. z \<in> r \<Longrightarrow> z \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
from L2 L3
[PROOF STATE]
proof (chain)
picking this:
u \<in> ce_rel_to_set r
z = (c_fst u, c_snd u)
[PROOF STEP]
show "z \<in> ce_set_to_rel (ce_rel_to_set r)"
[PROOF STATE]
proof (prove)
using this:
u \<in> ce_rel_to_set r
z = (c_fst u, c_snd u)

goal (1 subgoal):
 1. z \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
by (unfold ce_set_to_rel_def, auto)
[PROOF STATE]
proof (state)
this:
z \<in> ce_set_to_rel (ce_rel_to_set r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> r \<Longrightarrow> z \<in> ce_set_to_rel (ce_rel_to_set r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<subseteq> ce_set_to_rel (ce_rel_to_set r)

goal:
No subgoals!
[PROOF STEP]
qed