[STATEMENT]
lemma partition_on_the_part_eq:
  assumes "partition_on A P"
  assumes "x \<in> X" "X \<in> P"
  shows "(THE X. x \<in> X \<and> X \<in> P) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = X
[PROOF STEP]
from \<open>x \<in> X\<close> \<open>X \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
X \<in> P
[PROOF STEP]
have "x \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
X \<in> P

goal (1 subgoal):
 1. x \<in> A
[PROOF STEP]
using \<open>partition_on A P\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> X
X \<in> P
partition_on A P

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

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = X
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
[PROOF STEP]
have "\<exists>!X. x \<in> X \<and> X \<in> P"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
using \<open>partition_on A P\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> A
partition_on A P

goal (1 subgoal):
 1. \<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
by (simp add: partition_on_partition_on_unique)
[PROOF STATE]
proof (state)
this:
\<exists>!X. x \<in> X \<and> X \<in> P

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = X
[PROOF STEP]
from \<open>x \<in> X\<close> \<open>X \<in> P\<close> this
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
X \<in> P
\<exists>!X. x \<in> X \<and> X \<in> P
[PROOF STEP]
show "(THE X. x \<in> X \<and> X \<in> P) = X"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
X \<in> P
\<exists>!X. x \<in> X \<and> X \<in> P

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = X
[PROOF STEP]
by (auto intro!: the1_equality)
[PROOF STATE]
proof (state)
this:
(THE X. x \<in> X \<and> X \<in> P) = X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma the_unique_part_alternative_def:
  assumes "partition_on A P"
  assumes "x \<in> A"
  shows "(THE X. x \<in> X \<and> X \<in> P) = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (THE X. x \<in> X \<and> X \<in> P) \<subseteq> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
 2. {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} \<subseteq> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
show "(THE X. x \<in> X \<and> X \<in> P) \<subseteq> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) \<subseteq> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> (THE X. x \<in> X \<and> X \<in> P) \<Longrightarrow> xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> (THE X. x \<in> X \<and> X \<in> P) \<Longrightarrow> xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
assume "y \<in> (THE X. x \<in> X \<and> X \<in> P)"
[PROOF STATE]
proof (state)
this:
y \<in> (THE X. x \<in> X \<and> X \<in> P)

goal (1 subgoal):
 1. \<And>xa. xa \<in> (THE X. x \<in> X \<and> X \<in> P) \<Longrightarrow> xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> (THE X. x \<in> X \<and> X \<in> P)

goal (1 subgoal):
 1. \<And>xa. xa \<in> (THE X. x \<in> X \<and> X \<in> P) \<Longrightarrow> xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
from \<open>x \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
[PROOF STEP]
have "x \<in> (THE X. x \<in> X \<and> X \<in> P)"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. x \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
using \<open>partition_on A P\<close> partition_on_in_the_unique_part
[PROOF STATE]
proof (prove)
using this:
x \<in> A
partition_on A P
\<lbrakk>partition_on ?A ?P; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?x \<in> (THE X. ?x \<in> X \<and> X \<in> ?P)

goal (1 subgoal):
 1. x \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x \<in> (THE X. x \<in> X \<and> X \<in> P)

goal (1 subgoal):
 1. \<And>xa. xa \<in> (THE X. x \<in> X \<and> X \<in> P) \<Longrightarrow> xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> (THE X. x \<in> X \<and> X \<in> P)

goal (1 subgoal):
 1. \<And>xa. xa \<in> (THE X. x \<in> X \<and> X \<in> P) \<Longrightarrow> xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
from \<open>x \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
[PROOF STEP]
have "(THE X. x \<in> X \<and> X \<in> P) \<in> P"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) \<in> P
[PROOF STEP]
using \<open>partition_on A P\<close> partition_on_the_part_mem
[PROOF STATE]
proof (prove)
using this:
x \<in> A
partition_on A P
\<lbrakk>partition_on ?A ?P; ?x \<in> ?A\<rbrakk> \<Longrightarrow> (THE X. ?x \<in> X \<and> X \<in> ?P) \<in> ?P

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) \<in> P
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(THE X. x \<in> X \<and> X \<in> P) \<in> P

goal (1 subgoal):
 1. \<And>xa. xa \<in> (THE X. x \<in> X \<and> X \<in> P) \<Longrightarrow> xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<in> (THE X. x \<in> X \<and> X \<in> P)
x \<in> (THE X. x \<in> X \<and> X \<in> P)
(THE X. x \<in> X \<and> X \<in> P) \<in> P
[PROOF STEP]
show "y \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}"
[PROOF STATE]
proof (prove)
using this:
y \<in> (THE X. x \<in> X \<and> X \<in> P)
x \<in> (THE X. x \<in> X \<and> X \<in> P)
(THE X. x \<in> X \<and> X \<in> P) \<in> P

goal (1 subgoal):
 1. y \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(THE X. x \<in> X \<and> X \<in> P) \<subseteq> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}

goal (1 subgoal):
 1. {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} \<subseteq> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} \<subseteq> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
show "{y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} \<subseteq> (THE X. x \<in> X \<and> X \<in> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} \<subseteq> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} \<Longrightarrow> xa \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} \<Longrightarrow> xa \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
assume "y \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}"
[PROOF STATE]
proof (state)
this:
y \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} \<Longrightarrow> xa \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
y \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
obtain X where "x \<in> X" and "y \<in> X" and "X \<in> P"
[PROOF STATE]
proof (prove)
using this:
y \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}

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

goal (1 subgoal):
 1. \<And>xa. xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} \<Longrightarrow> xa \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
from \<open>x \<in> X\<close> \<open>X \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
X \<in> P
[PROOF STEP]
have "(THE X. x \<in> X \<and> X \<in> P) = X"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
X \<in> P

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = X
[PROOF STEP]
using \<open>partition_on A P\<close> partition_on_the_part_eq
[PROOF STATE]
proof (prove)
using this:
x \<in> X
X \<in> P
partition_on A P
\<lbrakk>partition_on ?A ?P; ?x \<in> ?X; ?X \<in> ?P\<rbrakk> \<Longrightarrow> (THE X. ?x \<in> X \<and> X \<in> ?P) = ?X

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = X
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(THE X. x \<in> X \<and> X \<in> P) = X

goal (1 subgoal):
 1. \<And>xa. xa \<in> {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} \<Longrightarrow> xa \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
from this \<open>y \<in> X\<close>
[PROOF STATE]
proof (chain)
picking this:
(THE X. x \<in> X \<and> X \<in> P) = X
y \<in> X
[PROOF STEP]
show "y \<in> (THE X. x \<in> X \<and> X \<in> P)"
[PROOF STATE]
proof (prove)
using this:
(THE X. x \<in> X \<and> X \<in> P) = X
y \<in> X

goal (1 subgoal):
 1. y \<in> (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<in> (THE X. x \<in> X \<and> X \<in> P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} \<subseteq> (THE X. x \<in> X \<and> X \<in> P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_all_in_part_eq_part:
  assumes "partition_on A P"
  assumes "X' \<in> P"
  shows "{x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'} = X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'} = X'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'} \<subseteq> X'
 2. X' \<subseteq> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}
[PROOF STEP]
show "{x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'} \<subseteq> X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'} \<subseteq> X'
[PROOF STEP]
using assms(1) partition_on_in_the_unique_part
[PROOF STATE]
proof (prove)
using this:
partition_on A P
\<lbrakk>partition_on ?A ?P; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?x \<in> (THE X. ?x \<in> X \<and> X \<in> ?P)

goal (1 subgoal):
 1. {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'} \<subseteq> X'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'} \<subseteq> X'

goal (1 subgoal):
 1. X' \<subseteq> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X' \<subseteq> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}
[PROOF STEP]
show "X' \<subseteq> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' \<subseteq> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X' \<Longrightarrow> x \<in> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X' \<Longrightarrow> x \<in> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}
[PROOF STEP]
assume "x \<in> X'"
[PROOF STATE]
proof (state)
this:
x \<in> X'

goal (1 subgoal):
 1. \<And>x. x \<in> X' \<Longrightarrow> x \<in> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}
[PROOF STEP]
from \<open>x \<in> X'\<close> \<open>X' \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> X'
X' \<in> P
[PROOF STEP]
have "x \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> X'
X' \<in> P

goal (1 subgoal):
 1. x \<in> A
[PROOF STEP]
using \<open>partition_on A P\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> X'
X' \<in> P
partition_on A P

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

goal (1 subgoal):
 1. \<And>x. x \<in> X' \<Longrightarrow> x \<in> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> X' \<Longrightarrow> x \<in> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}
[PROOF STEP]
from \<open>x \<in> X'\<close> \<open>X' \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> X'
X' \<in> P
[PROOF STEP]
have "(THE X. x \<in> X \<and> X \<in> P) = X'"
[PROOF STATE]
proof (prove)
using this:
x \<in> X'
X' \<in> P

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = X'
[PROOF STEP]
using \<open>partition_on A P\<close> partition_on_the_part_eq
[PROOF STATE]
proof (prove)
using this:
x \<in> X'
X' \<in> P
partition_on A P
\<lbrakk>partition_on ?A ?P; ?x \<in> ?X; ?X \<in> ?P\<rbrakk> \<Longrightarrow> (THE X. ?x \<in> X \<and> X \<in> ?P) = ?X

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = X'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(THE X. x \<in> X \<and> X \<in> P) = X'

goal (1 subgoal):
 1. \<And>x. x \<in> X' \<Longrightarrow> x \<in> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
(THE X. x \<in> X \<and> X \<in> P) = X'
[PROOF STEP]
show "x \<in> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
(THE X. x \<in> X \<and> X \<in> P) = X'

goal (1 subgoal):
 1. x \<in> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
X' \<subseteq> {x \<in> A. (THE X. x \<in> X \<and> X \<in> P) = X'}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_part_characteristic:
  assumes "partition_on A P"
  assumes "X \<in> P" "x \<in> X"
  shows "X = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
from \<open>x \<in> X\<close> \<open>X \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
X \<in> P
[PROOF STEP]
have "x \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
X \<in> P

goal (1 subgoal):
 1. x \<in> A
[PROOF STEP]
using \<open>partition_on A P\<close> partition_onE
[PROOF STATE]
proof (prove)
using this:
x \<in> X
X \<in> P
partition_on A P
\<lbrakk>partition_on ?A ?P; \<lbrakk>\<And>p. p \<in> ?P \<Longrightarrow> p \<noteq> {}; \<Union> ?P = ?A; \<And>p p'. \<lbrakk>p \<in> ?P; p' \<in> ?P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. X = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
from  \<open>x \<in> X\<close> \<open>X \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
X \<in> P
[PROOF STEP]
have "X = (THE X. x \<in> X \<and> X \<in> P)"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
X \<in> P

goal (1 subgoal):
 1. X = (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
using \<open>partition_on A P\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> X
X \<in> P
partition_on A P

goal (1 subgoal):
 1. X = (THE X. x \<in> X \<and> X \<in> P)
[PROOF STEP]
by (simp add: partition_on_the_part_eq)
[PROOF STATE]
proof (state)
this:
X = (THE X. x \<in> X \<and> X \<in> P)

goal (1 subgoal):
 1. X = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
X = (THE X. x \<in> X \<and> X \<in> P)

goal (1 subgoal):
 1. X = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
from \<open>x \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
[PROOF STEP]
have "(THE X. x \<in> X \<and> X \<in> P) = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
using \<open>partition_on A P\<close> the_unique_part_alternative_def
[PROOF STATE]
proof (prove)
using this:
x \<in> A
partition_on A P
\<lbrakk>partition_on ?A ?P; ?x \<in> ?A\<rbrakk> \<Longrightarrow> (THE X. ?x \<in> X \<and> X \<in> ?P) = {y. \<exists>X\<in>?P. ?x \<in> X \<and> y \<in> X}

goal (1 subgoal):
 1. (THE X. x \<in> X \<and> X \<in> P) = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(THE X. x \<in> X \<and> X \<in> P) = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}

goal (1 subgoal):
 1. X = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
X = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}

goal (1 subgoal):
 1. X = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
X = {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_no_partition_outside_carrier:
  assumes "partition_on A P"
  assumes "x \<notin> A"
  shows "{y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
partition_on A P
x \<notin> A

goal (1 subgoal):
 1. {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} = {}
[PROOF STEP]
unfolding partition_on_def
[PROOF STATE]
proof (prove)
using this:
\<Union> P = A \<and> disjoint P \<and> {} \<notin> P
x \<notin> A

goal (1 subgoal):
 1. {y. \<exists>X\<in>P. x \<in> X \<and> y \<in> X} = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma partition_on_le_set_elements:
  assumes "finite A"
  assumes "partition_on A P"
  shows "card P \<le> card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card P \<le> card A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
partition_on A P

goal (1 subgoal):
 1. card P \<le> card A
[PROOF STEP]
proof (induct A arbitrary: P)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. partition_on {} P \<Longrightarrow> card P \<le> card {}
 2. \<And>x F P. \<lbrakk>finite F; x \<notin> F; \<And>P. partition_on F P \<Longrightarrow> card P \<le> card F; partition_on (insert x F) P\<rbrakk> \<Longrightarrow> card P \<le> card (insert x F)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
partition_on {} P

goal (2 subgoals):
 1. \<And>P. partition_on {} P \<Longrightarrow> card P \<le> card {}
 2. \<And>x F P. \<lbrakk>finite F; x \<notin> F; \<And>P. partition_on F P \<Longrightarrow> card P \<le> card F; partition_on (insert x F) P\<rbrakk> \<Longrightarrow> card P \<le> card (insert x F)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
partition_on {} P
[PROOF STEP]
show "card P \<le> card {}"
[PROOF STATE]
proof (prove)
using this:
partition_on {} P

goal (1 subgoal):
 1. card P \<le> card {}
[PROOF STEP]
by (simp add: partition_on_empty)
[PROOF STATE]
proof (state)
this:
card P \<le> card {}

goal (1 subgoal):
 1. \<And>x F P. \<lbrakk>finite F; x \<notin> F; \<And>P. partition_on F P \<Longrightarrow> card P \<le> card F; partition_on (insert x F) P\<rbrakk> \<Longrightarrow> card P \<le> card (insert x F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F P. \<lbrakk>finite F; x \<notin> F; \<And>P. partition_on F P \<Longrightarrow> card P \<le> card F; partition_on (insert x F) P\<rbrakk> \<Longrightarrow> card P \<le> card (insert x F)
[PROOF STEP]
case (insert a A)
[PROOF STATE]
proof (state)
this:
finite A
a \<notin> A
partition_on A ?P \<Longrightarrow> card ?P \<le> card A
partition_on (insert a A) P

goal (1 subgoal):
 1. \<And>x F P. \<lbrakk>finite F; x \<notin> F; \<And>P. partition_on F P \<Longrightarrow> card P \<le> card F; partition_on (insert x F) P\<rbrakk> \<Longrightarrow> card P \<le> card (insert x F)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card P \<le> card (insert a A)
[PROOF STEP]
proof (cases "{a} \<in> P")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {a} \<in> P \<Longrightarrow> card P \<le> card (insert a A)
 2. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
{a} \<in> P

goal (2 subgoals):
 1. {a} \<in> P \<Longrightarrow> card P \<le> card (insert a A)
 2. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
have prop_partition_on: "\<forall>p\<in>P. p \<noteq> {}" "\<Union>P = insert a A"
      "\<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>P. p \<noteq> {} &&& \<Union> P = insert a A &&& \<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}
[PROOF STEP]
using \<open>partition_on (insert a A) P\<close>
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P

goal (1 subgoal):
 1. \<forall>p\<in>P. p \<noteq> {} &&& \<Union> P = insert a A &&& \<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}
[PROOF STEP]
by (fastforce elim: partition_onE)+
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>P. p \<noteq> {}
\<Union> P = insert a A
\<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}

goal (2 subgoals):
 1. {a} \<in> P \<Longrightarrow> card P \<le> card (insert a A)
 2. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
from this(2, 3) \<open>a \<notin> A\<close> \<open>{a} \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Union> P = insert a A
\<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}
a \<notin> A
{a} \<in> P
[PROOF STEP]
have A_eq: "A = \<Union>(P - {{a}})"
[PROOF STATE]
proof (prove)
using this:
\<Union> P = insert a A
\<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}
a \<notin> A
{a} \<in> P

goal (1 subgoal):
 1. A = \<Union> (P - {{a}})
[PROOF STEP]
by auto (metis Int_iff UnionI empty_iff insert_iff)
[PROOF STATE]
proof (state)
this:
A = \<Union> (P - {{a}})

goal (2 subgoals):
 1. {a} \<in> P \<Longrightarrow> card P \<le> card (insert a A)
 2. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
from prop_partition_on A_eq
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>P. p \<noteq> {}
\<Union> P = insert a A
\<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}
A = \<Union> (P - {{a}})
[PROOF STEP]
have partition_on: "partition_on A (P - {{a}})"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>P. p \<noteq> {}
\<Union> P = insert a A
\<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}
A = \<Union> (P - {{a}})

goal (1 subgoal):
 1. partition_on A (P - {{a}})
[PROOF STEP]
by (intro partition_onI) auto
[PROOF STATE]
proof (state)
this:
partition_on A (P - {{a}})

goal (2 subgoals):
 1. {a} \<in> P \<Longrightarrow> card P \<le> card (insert a A)
 2. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
from insert.hyps(3) this
[PROOF STATE]
proof (chain)
picking this:
partition_on A ?P \<Longrightarrow> card ?P \<le> card A
partition_on A (P - {{a}})
[PROOF STEP]
have "card (P - {{a}}) \<le> card A"
[PROOF STATE]
proof (prove)
using this:
partition_on A ?P \<Longrightarrow> card ?P \<le> card A
partition_on A (P - {{a}})

goal (1 subgoal):
 1. card (P - {{a}}) \<le> card A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (P - {{a}}) \<le> card A

goal (2 subgoals):
 1. {a} \<in> P \<Longrightarrow> card P \<le> card (insert a A)
 2. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
from this insert(1, 2, 4) \<open>{a} \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
card (P - {{a}}) \<le> card A
finite A
a \<notin> A
partition_on (insert a A) P
{a} \<in> P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (P - {{a}}) \<le> card A
finite A
a \<notin> A
partition_on (insert a A) P
{a} \<in> P

goal (1 subgoal):
 1. card P \<le> card (insert a A)
[PROOF STEP]
using finite_elements[OF \<open>finite A\<close> partition_on]
[PROOF STATE]
proof (prove)
using this:
card (P - {{a}}) \<le> card A
finite A
a \<notin> A
partition_on (insert a A) P
{a} \<in> P
finite (P - {{a}})

goal (1 subgoal):
 1. card P \<le> card (insert a A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card P \<le> card (insert a A)

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
{a} \<notin> P

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
from \<open>partition_on (insert a A) P\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on (insert a A) P
[PROOF STEP]
obtain p where p_def: "p \<in> P" "a \<in> p"
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> P; a \<in> p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast elim: partition_onE)
[PROOF STATE]
proof (state)
this:
p \<in> P
a \<in> p

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
from \<open>partition_on (insert a A) P\<close> p_def
[PROOF STATE]
proof (chain)
picking this:
partition_on (insert a A) P
p \<in> P
a \<in> p
[PROOF STEP]
have a_notmem: "\<forall>p'\<in> P - {p}. a \<notin> p'"
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P
p \<in> P
a \<in> p

goal (1 subgoal):
 1. \<forall>p'\<in>P - {p}. a \<notin> p'
[PROOF STEP]
by (blast elim: partition_onE)
[PROOF STATE]
proof (state)
this:
\<forall>p'\<in>P - {p}. a \<notin> p'

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
from \<open>partition_on (insert a A) P\<close> p_def
[PROOF STATE]
proof (chain)
picking this:
partition_on (insert a A) P
p \<in> P
a \<in> p
[PROOF STEP]
have "p - {a} \<notin> P"
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P
p \<in> P
a \<in> p

goal (1 subgoal):
 1. p - {a} \<notin> P
[PROOF STEP]
unfolding partition_on_def disjoint_def
[PROOF STATE]
proof (prove)
using this:
\<Union> P = insert a A \<and> (\<forall>a\<in>P. \<forall>b\<in>P. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> {} \<notin> P
p \<in> P
a \<in> p

goal (1 subgoal):
 1. p - {a} \<notin> P
[PROOF STEP]
by (metis Diff_insert_absorb Diff_subset inf.orderE mk_disjoint_insert)
[PROOF STATE]
proof (state)
this:
p - {a} \<notin> P

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
let ?P' = "insert (p - {a}) (P - {p})"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
have "partition_on A ?P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on A (insert (p - {a}) (P - {p}))
[PROOF STEP]
proof (rule partition_onI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>pa. pa \<in> insert (p - {a}) (P - {p}) \<Longrightarrow> pa \<noteq> {}
 2. \<Union> (insert (p - {a}) (P - {p})) = A
 3. \<And>pa p'. \<lbrakk>pa \<in> insert (p - {a}) (P - {p}); p' \<in> insert (p - {a}) (P - {p}); pa \<noteq> p'\<rbrakk> \<Longrightarrow> pa \<inter> p' = {}
[PROOF STEP]
from \<open>partition_on (insert a A) P\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on (insert a A) P
[PROOF STEP]
have "\<forall>p\<in>P. p \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P

goal (1 subgoal):
 1. \<forall>p\<in>P. p \<noteq> {}
[PROOF STEP]
by (auto elim: partition_onE)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>P. p \<noteq> {}

goal (3 subgoals):
 1. \<And>pa. pa \<in> insert (p - {a}) (P - {p}) \<Longrightarrow> pa \<noteq> {}
 2. \<Union> (insert (p - {a}) (P - {p})) = A
 3. \<And>pa p'. \<lbrakk>pa \<in> insert (p - {a}) (P - {p}); p' \<in> insert (p - {a}) (P - {p}); pa \<noteq> p'\<rbrakk> \<Longrightarrow> pa \<inter> p' = {}
[PROOF STEP]
from this p_def \<open>{a} \<notin> P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>P. p \<noteq> {}
p \<in> P
a \<in> p
{a} \<notin> P
[PROOF STEP]
show "\<And>p'. p'\<in>insert (p - {a}) (P - {p}) \<Longrightarrow> p' \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>P. p \<noteq> {}
p \<in> P
a \<in> p
{a} \<notin> P

goal (1 subgoal):
 1. \<And>p'. p' \<in> insert (p - {a}) (P - {p}) \<Longrightarrow> p' \<noteq> {}
[PROOF STEP]
by (simp; metis (no_types) Diff_eq_empty_iff subset_singletonD)
[PROOF STATE]
proof (state)
this:
?p' \<in> insert (p - {a}) (P - {p}) \<Longrightarrow> ?p' \<noteq> {}

goal (2 subgoals):
 1. \<Union> (insert (p - {a}) (P - {p})) = A
 2. \<And>pa p'. \<lbrakk>pa \<in> insert (p - {a}) (P - {p}); p' \<in> insert (p - {a}) (P - {p}); pa \<noteq> p'\<rbrakk> \<Longrightarrow> pa \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Union> (insert (p - {a}) (P - {p})) = A
 2. \<And>pa p'. \<lbrakk>pa \<in> insert (p - {a}) (P - {p}); p' \<in> insert (p - {a}) (P - {p}); pa \<noteq> p'\<rbrakk> \<Longrightarrow> pa \<inter> p' = {}
[PROOF STEP]
from \<open>partition_on (insert a A) P\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on (insert a A) P
[PROOF STEP]
have "\<Union>P = insert a A"
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P

goal (1 subgoal):
 1. \<Union> P = insert a A
[PROOF STEP]
by (auto elim: partition_onE)
[PROOF STATE]
proof (state)
this:
\<Union> P = insert a A

goal (2 subgoals):
 1. \<Union> (insert (p - {a}) (P - {p})) = A
 2. \<And>pa p'. \<lbrakk>pa \<in> insert (p - {a}) (P - {p}); p' \<in> insert (p - {a}) (P - {p}); pa \<noteq> p'\<rbrakk> \<Longrightarrow> pa \<inter> p' = {}
[PROOF STEP]
from p_def this \<open>a \<notin> A\<close> a_notmem
[PROOF STATE]
proof (chain)
picking this:
p \<in> P
a \<in> p
\<Union> P = insert a A
a \<notin> A
\<forall>p'\<in>P - {p}. a \<notin> p'
[PROOF STEP]
show "\<Union>(insert (p - {a}) (P - {p})) = A"
[PROOF STATE]
proof (prove)
using this:
p \<in> P
a \<in> p
\<Union> P = insert a A
a \<notin> A
\<forall>p'\<in>P - {p}. a \<notin> p'

goal (1 subgoal):
 1. \<Union> (insert (p - {a}) (P - {p})) = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (insert (p - {a}) (P - {p})) = A

goal (1 subgoal):
 1. \<And>pa p'. \<lbrakk>pa \<in> insert (p - {a}) (P - {p}); p' \<in> insert (p - {a}) (P - {p}); pa \<noteq> p'\<rbrakk> \<Longrightarrow> pa \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pa p'. \<lbrakk>pa \<in> insert (p - {a}) (P - {p}); p' \<in> insert (p - {a}) (P - {p}); pa \<noteq> p'\<rbrakk> \<Longrightarrow> pa \<inter> p' = {}
[PROOF STEP]
show "\<And>pa pa'. pa\<in>insert (p - {a}) (P - {p}) \<Longrightarrow> pa'\<in>insert (p - {a}) (P - {p}) \<Longrightarrow> pa \<noteq> pa' \<Longrightarrow> pa \<inter> pa' = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pa pa'. \<lbrakk>pa \<in> insert (p - {a}) (P - {p}); pa' \<in> insert (p - {a}) (P - {p}); pa \<noteq> pa'\<rbrakk> \<Longrightarrow> pa \<inter> pa' = {}
[PROOF STEP]
using \<open>partition_on (insert a A) P\<close> p_def a_notmem
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P
p \<in> P
a \<in> p
\<forall>p'\<in>P - {p}. a \<notin> p'

goal (1 subgoal):
 1. \<And>pa pa'. \<lbrakk>pa \<in> insert (p - {a}) (P - {p}); pa' \<in> insert (p - {a}) (P - {p}); pa \<noteq> pa'\<rbrakk> \<Longrightarrow> pa \<inter> pa' = {}
[PROOF STEP]
unfolding partition_on_def disjoint_def
[PROOF STATE]
proof (prove)
using this:
\<Union> P = insert a A \<and> (\<forall>a\<in>P. \<forall>b\<in>P. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> {} \<notin> P
p \<in> P
a \<in> p
\<forall>p'\<in>P - {p}. a \<notin> p'

goal (1 subgoal):
 1. \<And>pa pa'. \<lbrakk>pa \<in> insert (p - {a}) (P - {p}); pa' \<in> insert (p - {a}) (P - {p}); pa \<noteq> pa'\<rbrakk> \<Longrightarrow> pa \<inter> pa' = {}
[PROOF STEP]
by (metis disjoint_iff_not_equal insert_Diff insert_iff)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?pa \<in> insert (p - {a}) (P - {p}); ?pa' \<in> insert (p - {a}) (P - {p}); ?pa \<noteq> ?pa'\<rbrakk> \<Longrightarrow> ?pa \<inter> ?pa' = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
partition_on A (insert (p - {a}) (P - {p}))

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
have "finite P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite P
[PROOF STEP]
using \<open>finite A\<close> \<open>partition_on A ?P'\<close> finite_elements
[PROOF STATE]
proof (prove)
using this:
finite A
partition_on A (insert (p - {a}) (P - {p}))
\<lbrakk>finite ?A; partition_on ?A ?P\<rbrakk> \<Longrightarrow> finite ?P

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

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
have "card P = Suc (card (P - {p}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card P = Suc (card (P - {p}))
[PROOF STEP]
using p_def \<open>finite P\<close> card.remove
[PROOF STATE]
proof (prove)
using this:
p \<in> P
a \<in> p
finite P
\<lbrakk>finite ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> card ?A = Suc (card (?A - {?x}))

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

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card P = Suc (card (P - {p}))

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
have "\<dots> = card ?P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (card (P - {p})) = card (insert (p - {a}) (P - {p}))
[PROOF STEP]
using \<open>p - {a} \<notin> P\<close> \<open>finite P\<close>
[PROOF STATE]
proof (prove)
using this:
p - {a} \<notin> P
finite P

goal (1 subgoal):
 1. Suc (card (P - {p})) = card (insert (p - {a}) (P - {p}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (card (P - {p})) = card (insert (p - {a}) (P - {p}))

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (card (P - {p})) = card (insert (p - {a}) (P - {p}))

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
have "\<dots> \<le> card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (insert (p - {a}) (P - {p})) \<le> card A
[PROOF STEP]
using \<open>partition_on A ?P'\<close> insert.hyps(3)
[PROOF STATE]
proof (prove)
using this:
partition_on A (insert (p - {a}) (P - {p}))
partition_on A ?P \<Longrightarrow> card ?P \<le> card A

goal (1 subgoal):
 1. card (insert (p - {a}) (P - {p})) \<le> card A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (insert (p - {a}) (P - {p})) \<le> card A

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (insert (p - {a}) (P - {p})) \<le> card A

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
have "\<dots> \<le> card (insert a A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card A \<le> card (insert a A)
[PROOF STEP]
by (simp add: card_insert_le \<open>finite A\<close> )
[PROOF STATE]
proof (state)
this:
card A \<le> card (insert a A)

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> card P \<le> card (insert a A)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card P \<le> card (insert a A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card P \<le> card (insert a A)

goal (1 subgoal):
 1. card P \<le> card (insert a A)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card P \<le> card (insert a A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card P \<le> card (insert a A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_union:
  assumes "A \<inter> B = {}"
  assumes "partition_on A P"
  assumes "partition_on B Q"
  shows "partition_on (A \<union> B) (P \<union> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on (A \<union> B) (P \<union> Q)
[PROOF STEP]
proof (rule partition_onI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p. p \<in> P \<union> Q \<Longrightarrow> p \<noteq> {}
 2. \<Union> (P \<union> Q) = A \<union> B
 3. \<And>p p'. \<lbrakk>p \<in> P \<union> Q; p' \<in> P \<union> Q; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p. p \<in> P \<union> Q \<Longrightarrow> p \<noteq> {}
 2. \<Union> (P \<union> Q) = A \<union> B
 3. \<And>p p'. \<lbrakk>p \<in> P \<union> Q; p' \<in> P \<union> Q; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
assume "X \<in> P \<union> Q"
[PROOF STATE]
proof (state)
this:
X \<in> P \<union> Q

goal (3 subgoals):
 1. \<And>p. p \<in> P \<union> Q \<Longrightarrow> p \<noteq> {}
 2. \<Union> (P \<union> Q) = A \<union> B
 3. \<And>p p'. \<lbrakk>p \<in> P \<union> Q; p' \<in> P \<union> Q; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from this \<open>partition_on A P\<close> \<open>partition_on B Q\<close>
[PROOF STATE]
proof (chain)
picking this:
X \<in> P \<union> Q
partition_on A P
partition_on B Q
[PROOF STEP]
show "X \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
X \<in> P \<union> Q
partition_on A P
partition_on B Q

goal (1 subgoal):
 1. X \<noteq> {}
[PROOF STEP]
by (auto elim: partition_onE)
[PROOF STATE]
proof (state)
this:
X \<noteq> {}

goal (2 subgoals):
 1. \<Union> (P \<union> Q) = A \<union> B
 2. \<And>p p'. \<lbrakk>p \<in> P \<union> Q; p' \<in> P \<union> Q; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Union> (P \<union> Q) = A \<union> B
 2. \<And>p p'. \<lbrakk>p \<in> P \<union> Q; p' \<in> P \<union> Q; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
show "\<Union>(P \<union> Q) = A \<union> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (P \<union> Q) = A \<union> B
[PROOF STEP]
using \<open>partition_on A P\<close> \<open>partition_on B Q\<close>
[PROOF STATE]
proof (prove)
using this:
partition_on A P
partition_on B Q

goal (1 subgoal):
 1. \<Union> (P \<union> Q) = A \<union> B
[PROOF STEP]
by (auto elim: partition_onE)
[PROOF STATE]
proof (state)
this:
\<Union> (P \<union> Q) = A \<union> B

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> P \<union> Q; p' \<in> P \<union> Q; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> P \<union> Q; p' \<in> P \<union> Q; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
fix X Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> P \<union> Q; p' \<in> P \<union> Q; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
assume "X \<in> P \<union> Q" "Y \<in> P \<union> Q" "X \<noteq> Y"
[PROOF STATE]
proof (state)
this:
X \<in> P \<union> Q
Y \<in> P \<union> Q
X \<noteq> Y

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> P \<union> Q; p' \<in> P \<union> Q; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from this assms
[PROOF STATE]
proof (chain)
picking this:
X \<in> P \<union> Q
Y \<in> P \<union> Q
X \<noteq> Y
A \<inter> B = {}
partition_on A P
partition_on B Q
[PROOF STEP]
show "X \<inter> Y = {}"
[PROOF STATE]
proof (prove)
using this:
X \<in> P \<union> Q
Y \<in> P \<union> Q
X \<noteq> Y
A \<inter> B = {}
partition_on A P
partition_on B Q

goal (1 subgoal):
 1. X \<inter> Y = {}
[PROOF STEP]
by (elim UnE partition_onE) auto
[PROOF STATE]
proof (state)
this:
X \<inter> Y = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_split1:
  assumes "partition_on A (P \<union> Q)"
  shows "partition_on (\<Union>P) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on (\<Union> P) P
[PROOF STEP]
proof (rule partition_onI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p. p \<in> P \<Longrightarrow> p \<noteq> {}
 2. \<Union> P = \<Union> P
 3. \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p. p \<in> P \<Longrightarrow> p \<noteq> {}
 2. \<Union> P = \<Union> P
 3. \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
assume "p \<in> P"
[PROOF STATE]
proof (state)
this:
p \<in> P

goal (3 subgoals):
 1. \<And>p. p \<in> P \<Longrightarrow> p \<noteq> {}
 2. \<Union> P = \<Union> P
 3. \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from this assms
[PROOF STATE]
proof (chain)
picking this:
p \<in> P
partition_on A (P \<union> Q)
[PROOF STEP]
show "p \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
p \<in> P
partition_on A (P \<union> Q)

goal (1 subgoal):
 1. p \<noteq> {}
[PROOF STEP]
using Un_iff partition_onE
[PROOF STATE]
proof (prove)
using this:
p \<in> P
partition_on A (P \<union> Q)
(?c \<in> ?A \<union> ?B) = (?c \<in> ?A \<or> ?c \<in> ?B)
\<lbrakk>partition_on ?A ?P; \<lbrakk>\<And>p. p \<in> ?P \<Longrightarrow> p \<noteq> {}; \<Union> ?P = ?A; \<And>p p'. \<lbrakk>p \<in> ?P; p' \<in> ?P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (2 subgoals):
 1. \<Union> P = \<Union> P
 2. \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Union> P = \<Union> P
 2. \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
show "\<Union>P = \<Union>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> P = \<Union> P
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<Union> P = \<Union> P

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
fix p p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
assume a: "p \<in> P" "p' \<in> P" "p \<noteq> p'"
[PROOF STATE]
proof (state)
this:
p \<in> P
p' \<in> P
p \<noteq> p'

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> P; p' \<in> P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from this assms
[PROOF STATE]
proof (chain)
picking this:
p \<in> P
p' \<in> P
p \<noteq> p'
partition_on A (P \<union> Q)
[PROOF STEP]
show "p \<inter> p' = {}"
[PROOF STATE]
proof (prove)
using this:
p \<in> P
p' \<in> P
p \<noteq> p'
partition_on A (P \<union> Q)

goal (1 subgoal):
 1. p \<inter> p' = {}
[PROOF STEP]
using partition_onE subsetCE sup_ge1
[PROOF STATE]
proof (prove)
using this:
p \<in> P
p' \<in> P
p \<noteq> p'
partition_on A (P \<union> Q)
\<lbrakk>partition_on ?A ?P; \<lbrakk>\<And>p. p \<in> ?P \<Longrightarrow> p \<noteq> {}; \<Union> ?P = ?A; \<And>p p'. \<lbrakk>p \<in> ?P; p' \<in> ?P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>?A \<subseteq> ?B; ?c \<notin> ?A \<Longrightarrow> ?P; ?c \<in> ?B \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
?x \<le> sup ?x ?y

goal (1 subgoal):
 1. p \<inter> p' = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<inter> p' = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_split2:
  assumes "partition_on A (P \<union> Q)"
  shows "partition_on (\<Union>Q) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on (\<Union> Q) Q
[PROOF STEP]
using assms partition_on_split1 sup_commute
[PROOF STATE]
proof (prove)
using this:
partition_on A (P \<union> Q)
partition_on ?A (?P \<union> ?Q) \<Longrightarrow> partition_on (\<Union> ?P) ?P
sup ?x ?y = sup ?y ?x

goal (1 subgoal):
 1. partition_on (\<Union> Q) Q
[PROOF STEP]
by metis


[STATEMENT]
lemma partition_on_intersect_on_elements:
  assumes "partition_on (A \<union> C) P"
  assumes "\<forall>X \<in> P. \<exists>x. x \<in> X \<inter> C"
  shows "partition_on C ((\<lambda>X. X \<inter> C) ` P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on C ((\<lambda>X. X \<inter> C) ` P)
[PROOF STEP]
proof (rule partition_onI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p. p \<in> (\<lambda>X. X \<inter> C) ` P \<Longrightarrow> p \<noteq> {}
 2. (\<Union>X\<in>P. X \<inter> C) = C
 3. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<inter> C) ` P; p' \<in> (\<lambda>X. X \<inter> C) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p. p \<in> (\<lambda>X. X \<inter> C) ` P \<Longrightarrow> p \<noteq> {}
 2. (\<Union>X\<in>P. X \<inter> C) = C
 3. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<inter> C) ` P; p' \<in> (\<lambda>X. X \<inter> C) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
assume "p \<in> (\<lambda>X. X \<inter> C) ` P"
[PROOF STATE]
proof (state)
this:
p \<in> (\<lambda>X. X \<inter> C) ` P

goal (3 subgoals):
 1. \<And>p. p \<in> (\<lambda>X. X \<inter> C) ` P \<Longrightarrow> p \<noteq> {}
 2. (\<Union>X\<in>P. X \<inter> C) = C
 3. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<inter> C) ` P; p' \<in> (\<lambda>X. X \<inter> C) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from this assms
[PROOF STATE]
proof (chain)
picking this:
p \<in> (\<lambda>X. X \<inter> C) ` P
partition_on (A \<union> C) P
\<forall>X\<in>P. \<exists>x. x \<in> X \<inter> C
[PROOF STEP]
show "p \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
p \<in> (\<lambda>X. X \<inter> C) ` P
partition_on (A \<union> C) P
\<forall>X\<in>P. \<exists>x. x \<in> X \<inter> C

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

goal (2 subgoals):
 1. (\<Union>X\<in>P. X \<inter> C) = C
 2. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<inter> C) ` P; p' \<in> (\<lambda>X. X \<inter> C) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Union>X\<in>P. X \<inter> C) = C
 2. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<inter> C) ` P; p' \<in> (\<lambda>X. X \<inter> C) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
have "\<Union>P = A \<union> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> P = A \<union> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
partition_on (A \<union> C) P
\<forall>X\<in>P. \<exists>x. x \<in> X \<inter> C

goal (1 subgoal):
 1. \<Union> P = A \<union> C
[PROOF STEP]
by (auto elim: partition_onE)
[PROOF STATE]
proof (state)
this:
\<Union> P = A \<union> C

goal (2 subgoals):
 1. (\<Union>X\<in>P. X \<inter> C) = C
 2. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<inter> C) ` P; p' \<in> (\<lambda>X. X \<inter> C) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<Union> P = A \<union> C
[PROOF STEP]
show "\<Union>((\<lambda>X. X \<inter> C) ` P) = C"
[PROOF STATE]
proof (prove)
using this:
\<Union> P = A \<union> C

goal (1 subgoal):
 1. (\<Union>X\<in>P. X \<inter> C) = C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>X\<in>P. X \<inter> C) = C

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<inter> C) ` P; p' \<in> (\<lambda>X. X \<inter> C) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<inter> C) ` P; p' \<in> (\<lambda>X. X \<inter> C) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
fix p p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<inter> C) ` P; p' \<in> (\<lambda>X. X \<inter> C) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
assume "p \<in> (\<lambda>X. X \<inter> C) ` P" "p' \<in> (\<lambda>X. X \<inter> C) ` P" "p \<noteq> p'"
[PROOF STATE]
proof (state)
this:
p \<in> (\<lambda>X. X \<inter> C) ` P
p' \<in> (\<lambda>X. X \<inter> C) ` P
p \<noteq> p'

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<inter> C) ` P; p' \<in> (\<lambda>X. X \<inter> C) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from this assms(1)
[PROOF STATE]
proof (chain)
picking this:
p \<in> (\<lambda>X. X \<inter> C) ` P
p' \<in> (\<lambda>X. X \<inter> C) ` P
p \<noteq> p'
partition_on (A \<union> C) P
[PROOF STEP]
show "p \<inter> p' = {}"
[PROOF STATE]
proof (prove)
using this:
p \<in> (\<lambda>X. X \<inter> C) ` P
p' \<in> (\<lambda>X. X \<inter> C) ` P
p \<noteq> p'
partition_on (A \<union> C) P

goal (1 subgoal):
 1. p \<inter> p' = {}
[PROOF STEP]
by (blast elim: partition_onE)
[PROOF STATE]
proof (state)
this:
p \<inter> p' = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_insert_elements:
  assumes "A \<inter> B = {}"
  assumes "partition_on B P"
  assumes "f \<in> A \<rightarrow>\<^sub>E P"
  shows "partition_on (A \<union> B) ((\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P)" (is "partition_on _ ?P")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on (A \<union> B) ((\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P)
[PROOF STEP]
proof (rule partition_onI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p. p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P \<Longrightarrow> p \<noteq> {}
 2. (\<Union>X\<in>P. X \<union> {x \<in> A. f x = X}) = A \<union> B
 3. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p. p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P \<Longrightarrow> p \<noteq> {}
 2. (\<Union>X\<in>P. X \<union> {x \<in> A. f x = X}) = A \<union> B
 3. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
assume "X \<in> ?P"
[PROOF STATE]
proof (state)
this:
X \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P

goal (3 subgoals):
 1. \<And>p. p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P \<Longrightarrow> p \<noteq> {}
 2. (\<Union>X\<in>P. X \<union> {x \<in> A. f x = X}) = A \<union> B
 3. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from this \<open>partition_on B P\<close>
[PROOF STATE]
proof (chain)
picking this:
X \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P
partition_on B P
[PROOF STEP]
show "X \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
X \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P
partition_on B P

goal (1 subgoal):
 1. X \<noteq> {}
[PROOF STEP]
by (auto elim: partition_onE)
[PROOF STATE]
proof (state)
this:
X \<noteq> {}

goal (2 subgoals):
 1. (\<Union>X\<in>P. X \<union> {x \<in> A. f x = X}) = A \<union> B
 2. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Union>X\<in>P. X \<union> {x \<in> A. f x = X}) = A \<union> B
 2. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
show "\<Union>?P = A \<union> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>X\<in>P. X \<union> {x \<in> A. f x = X}) = A \<union> B
[PROOF STEP]
using \<open>partition_on B P\<close> \<open>f \<in> A \<rightarrow>\<^sub>E P\<close>
[PROOF STATE]
proof (prove)
using this:
partition_on B P
f \<in> A \<rightarrow>\<^sub>E P

goal (1 subgoal):
 1. (\<Union>X\<in>P. X \<union> {x \<in> A. f x = X}) = A \<union> B
[PROOF STEP]
by (auto elim: partition_onE)
[PROOF STATE]
proof (state)
this:
(\<Union>X\<in>P. X \<union> {x \<in> A. f x = X}) = A \<union> B

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
fix X Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
assume "X \<in> ?P" "Y \<in> ?P" "X \<noteq> Y"
[PROOF STATE]
proof (state)
this:
X \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P
Y \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P
X \<noteq> Y

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from \<open>X \<in> ?P\<close>
[PROOF STATE]
proof (chain)
picking this:
X \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P
[PROOF STEP]
obtain X' where X': "X = X' \<union> {x \<in> A. f x = X'}" "X' \<in> P"
[PROOF STATE]
proof (prove)
using this:
X \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P

goal (1 subgoal):
 1. (\<And>X'. \<lbrakk>X = X' \<union> {x \<in> A. f x = X'}; X' \<in> P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from \<open>Y \<in> ?P\<close>
[PROOF STATE]
proof (chain)
picking this:
Y \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P
[PROOF STEP]
obtain Y' where Y': "Y = Y' \<union> {x \<in> A. f x = Y'}" "Y' \<in> P"
[PROOF STATE]
proof (prove)
using this:
Y \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P

goal (1 subgoal):
 1. (\<And>Y'. \<lbrakk>Y = Y' \<union> {x \<in> A. f x = Y'}; Y' \<in> P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from \<open>X \<noteq> Y\<close> X' Y'
[PROOF STATE]
proof (chain)
picking this:
X \<noteq> Y
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P
[PROOF STEP]
have "X' \<noteq> Y'"
[PROOF STATE]
proof (prove)
using this:
X \<noteq> Y
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P

goal (1 subgoal):
 1. X' \<noteq> Y'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X' \<noteq> Y'

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from this X' Y'
[PROOF STATE]
proof (chain)
picking this:
X' \<noteq> Y'
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P
[PROOF STEP]
have "X' \<inter> Y' = {}"
[PROOF STATE]
proof (prove)
using this:
X' \<noteq> Y'
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P

goal (1 subgoal):
 1. X' \<inter> Y' = {}
[PROOF STEP]
using \<open>partition_on B P\<close>
[PROOF STATE]
proof (prove)
using this:
X' \<noteq> Y'
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P
partition_on B P

goal (1 subgoal):
 1. X' \<inter> Y' = {}
[PROOF STEP]
by (auto elim!: partition_onE)
[PROOF STATE]
proof (state)
this:
X' \<inter> Y' = {}

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from X' Y'
[PROOF STATE]
proof (chain)
picking this:
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P
[PROOF STEP]
have "X' \<subseteq> B" "Y' \<subseteq> B"
[PROOF STATE]
proof (prove)
using this:
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P

goal (1 subgoal):
 1. X' \<subseteq> B &&& Y' \<subseteq> B
[PROOF STEP]
using \<open>partition_on B P\<close>
[PROOF STATE]
proof (prove)
using this:
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P
partition_on B P

goal (1 subgoal):
 1. X' \<subseteq> B &&& Y' \<subseteq> B
[PROOF STEP]
by (auto elim!: partition_onE)
[PROOF STATE]
proof (state)
this:
X' \<subseteq> B
Y' \<subseteq> B

goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p' \<in> (\<lambda>X. X \<union> {x \<in> A. f x = X}) ` P; p \<noteq> p'\<rbrakk> \<Longrightarrow> p \<inter> p' = {}
[PROOF STEP]
from this \<open>X' \<inter> Y' = {}\<close> X' Y' \<open>X' \<noteq> Y'\<close>
[PROOF STATE]
proof (chain)
picking this:
X' \<subseteq> B
Y' \<subseteq> B
X' \<inter> Y' = {}
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P
X' \<noteq> Y'
[PROOF STEP]
show "X \<inter> Y = {}"
[PROOF STATE]
proof (prove)
using this:
X' \<subseteq> B
Y' \<subseteq> B
X' \<inter> Y' = {}
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P
X' \<noteq> Y'

goal (1 subgoal):
 1. X \<inter> Y = {}
[PROOF STEP]
using \<open>A \<inter> B = {}\<close>
[PROOF STATE]
proof (prove)
using this:
X' \<subseteq> B
Y' \<subseteq> B
X' \<inter> Y' = {}
X = X' \<union> {x \<in> A. f x = X'}
X' \<in> P
Y = Y' \<union> {x \<in> A. f x = Y'}
Y' \<in> P
X' \<noteq> Y'
A \<inter> B = {}

goal (1 subgoal):
 1. X \<inter> Y = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<inter> Y = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_on_map:
  assumes "inj_on f A"
  assumes "partition_on A P"
  shows "partition_on (f ` A) ((`) f ` P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on (f ` A) ((`) f ` P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partition_on (f ` A) ((`) f ` P)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partition_on (f ` A) ((`) f ` P)
[PROOF STEP]
fix X Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partition_on (f ` A) ((`) f ` P)
[PROOF STEP]
assume "X \<in> P" "Y \<in> P" "f ` X \<noteq> f ` Y"
[PROOF STATE]
proof (state)
this:
X \<in> P
Y \<in> P
f ` X \<noteq> f ` Y

goal (1 subgoal):
 1. partition_on (f ` A) ((`) f ` P)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X \<in> P
Y \<in> P
f ` X \<noteq> f ` Y

goal (1 subgoal):
 1. partition_on (f ` A) ((`) f ` P)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
inj_on f A
partition_on A P
[PROOF STEP]
have "\<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}" and "inj_on f (\<Union>P)"
[PROOF STATE]
proof (prove)
using this:
inj_on f A
partition_on A P

goal (1 subgoal):
 1. \<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {} &&& inj_on f (\<Union> P)
[PROOF STEP]
by (auto elim!: partition_onE)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}
inj_on f (\<Union> P)

goal (1 subgoal):
 1. partition_on (f ` A) ((`) f ` P)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X \<in> P
Y \<in> P
f ` X \<noteq> f ` Y
\<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}
inj_on f (\<Union> P)
[PROOF STEP]
have "f ` X \<inter> f ` Y = {}"
[PROOF STATE]
proof (prove)
using this:
X \<in> P
Y \<in> P
f ` X \<noteq> f ` Y
\<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}
inj_on f (\<Union> P)

goal (1 subgoal):
 1. f ` X \<inter> f ` Y = {}
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
X \<in> P
Y \<in> P
f ` X \<noteq> f ` Y
\<forall>p\<in>P. \<forall>p'\<in>P. p \<noteq> p' \<longrightarrow> p \<inter> p' = {}
\<forall>x\<in>\<Union> P. \<forall>y\<in>\<Union> P. f x = f y \<longrightarrow> x = y

goal (1 subgoal):
 1. f ` X \<inter> f ` Y = {}
[PROOF STEP]
by auto (metis IntI empty_iff rev_image_eqI)+
[PROOF STATE]
proof (state)
this:
f ` X \<inter> f ` Y = {}

goal (1 subgoal):
 1. partition_on (f ` A) ((`) f ` P)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?X2 \<in> P; ?Y2 \<in> P; f ` ?X2 \<noteq> f ` ?Y2\<rbrakk> \<Longrightarrow> f ` ?X2 \<inter> f ` ?Y2 = {}

goal (1 subgoal):
 1. partition_on (f ` A) ((`) f ` P)
[PROOF STEP]
from assms this
[PROOF STATE]
proof (chain)
picking this:
inj_on f A
partition_on A P
\<lbrakk>?X2 \<in> P; ?Y2 \<in> P; f ` ?X2 \<noteq> f ` ?Y2\<rbrakk> \<Longrightarrow> f ` ?X2 \<inter> f ` ?Y2 = {}
[PROOF STEP]
show "partition_on (f ` A) ((`) f ` P)"
[PROOF STATE]
proof (prove)
using this:
inj_on f A
partition_on A P
\<lbrakk>?X2 \<in> P; ?Y2 \<in> P; f ` ?X2 \<noteq> f ` ?Y2\<rbrakk> \<Longrightarrow> f ` ?X2 \<inter> f ` ?Y2 = {}

goal (1 subgoal):
 1. partition_on (f ` A) ((`) f ` P)
[PROOF STEP]
by (auto intro!: partition_onI elim!: partition_onE)
[PROOF STATE]
proof (state)
this:
partition_on (f ` A) ((`) f ` P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_of_partition_on_map:
  assumes "inj_on f A"
  shows "(`) ((`) f) ` {P. partition_on A P} = {P. partition_on (f ` A) P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) ((`) f) ` {P. partition_on A P} = {P. partition_on (f ` A) P}
[PROOF STEP]
proof (rule set_eqI')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> (`) ((`) f) ` {P. partition_on A P} \<Longrightarrow> x \<in> {P. partition_on (f ` A) P}
 2. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> (`) ((`) f) ` {P. partition_on A P} \<Longrightarrow> x \<in> {P. partition_on (f ` A) P}
 2. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
assume "x \<in> (`) ((`) f) ` {P. partition_on A P}"
[PROOF STATE]
proof (state)
this:
x \<in> (`) ((`) f) ` {P. partition_on A P}

goal (2 subgoals):
 1. \<And>x. x \<in> (`) ((`) f) ` {P. partition_on A P} \<Longrightarrow> x \<in> {P. partition_on (f ` A) P}
 2. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
from this \<open>inj_on f A\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> (`) ((`) f) ` {P. partition_on A P}
inj_on f A
[PROOF STEP]
show "x \<in> {P. partition_on (f ` A) P}"
[PROOF STATE]
proof (prove)
using this:
x \<in> (`) ((`) f) ` {P. partition_on A P}
inj_on f A

goal (1 subgoal):
 1. x \<in> {P. partition_on (f ` A) P}
[PROOF STEP]
by (auto intro: partition_on_map)
[PROOF STATE]
proof (state)
this:
x \<in> {P. partition_on (f ` A) P}

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
assume "P \<in> {P. partition_on (f ` A) P}"
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on (f ` A) P}

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<in> {P. partition_on (f ` A) P}
[PROOF STEP]
have "partition_on (f ` A) P"
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on (f ` A) P}

goal (1 subgoal):
 1. partition_on (f ` A) P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partition_on (f ` A) P

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
partition_on (f ` A) P
[PROOF STEP]
have mem: "\<And>X x. X \<in> P \<Longrightarrow> x \<in> X \<Longrightarrow> x \<in> f ` A"
[PROOF STATE]
proof (prove)
using this:
partition_on (f ` A) P

goal (1 subgoal):
 1. \<And>X x. \<lbrakk>X \<in> P; x \<in> X\<rbrakk> \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
by (auto elim!: partition_onE)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?X \<in> P; ?x \<in> ?X\<rbrakk> \<Longrightarrow> ?x \<in> f ` A

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
have "(`) (f \<circ> the_inv_into A f) ` P = (`) f ` (`) (the_inv_into A f) ` P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) (f \<circ> the_inv_into A f) ` P = (`) f ` (`) (the_inv_into A f) ` P
[PROOF STEP]
by (simp add: image_image cong: image_cong_simp)
[PROOF STATE]
proof (state)
this:
(`) (f \<circ> the_inv_into A f) ` P = (`) f ` (`) (the_inv_into A f) ` P

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(`) (f \<circ> the_inv_into A f) ` P = (`) f ` (`) (the_inv_into A f) ` P

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
have "P = (`) (f \<circ> the_inv_into A f) ` P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P = (`) (f \<circ> the_inv_into A f) ` P
[PROOF STEP]
proof (rule set_eqI')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (`) (f \<circ> the_inv_into A f) ` P
 2. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (`) (f \<circ> the_inv_into A f) ` P
 2. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
assume X: "X \<in> P"
[PROOF STATE]
proof (state)
this:
X \<in> P

goal (2 subgoals):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (`) (f \<circ> the_inv_into A f) ` P
 2. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X \<in> P

goal (2 subgoals):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (`) (f \<circ> the_inv_into A f) ` P
 2. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
from X mem
[PROOF STATE]
proof (chain)
picking this:
X \<in> P
\<lbrakk>?X \<in> P; ?x \<in> ?X\<rbrakk> \<Longrightarrow> ?x \<in> f ` A
[PROOF STEP]
have in_range: "\<forall>x\<in>X. x \<in> f ` A"
[PROOF STATE]
proof (prove)
using this:
X \<in> P
\<lbrakk>?X \<in> P; ?x \<in> ?X\<rbrakk> \<Longrightarrow> ?x \<in> f ` A

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

goal (2 subgoals):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (`) (f \<circ> the_inv_into A f) ` P
 2. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. x \<in> f ` A

goal (2 subgoals):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (`) (f \<circ> the_inv_into A f) ` P
 2. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
have "X = (f \<circ> the_inv_into A f) ` X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X = (f \<circ> the_inv_into A f) ` X
[PROOF STEP]
proof (rule set_eqI')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> (f \<circ> the_inv_into A f) ` X
 2. \<And>x. x \<in> (f \<circ> the_inv_into A f) ` X \<Longrightarrow> x \<in> X
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> (f \<circ> the_inv_into A f) ` X
 2. \<And>x. x \<in> (f \<circ> the_inv_into A f) ` X \<Longrightarrow> x \<in> X
[PROOF STEP]
assume "x \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (2 subgoals):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> (f \<circ> the_inv_into A f) ` X
 2. \<And>x. x \<in> (f \<circ> the_inv_into A f) ` X \<Longrightarrow> x \<in> X
[PROOF STEP]
show "x \<in> (f \<circ> the_inv_into A f) ` X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (f \<circ> the_inv_into A f) ` X
[PROOF STEP]
proof (rule image_eqI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = (f \<circ> the_inv_into A f) ?x
 2. ?x \<in> X
[PROOF STEP]
from in_range \<open>x \<in> X\<close> assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>X. x \<in> f ` A
x \<in> X
inj_on f A
[PROOF STEP]
show "x = (f \<circ> the_inv_into A f) x"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. x \<in> f ` A
x \<in> X
inj_on f A

goal (1 subgoal):
 1. x = (f \<circ> the_inv_into A f) x
[PROOF STEP]
by (auto simp add: f_the_inv_into_f[of f])
[PROOF STATE]
proof (state)
this:
x = (f \<circ> the_inv_into A f) x

goal (1 subgoal):
 1. x \<in> X
[PROOF STEP]
from \<open>x \<in> X\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
[PROOF STEP]
show "x \<in> X"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> (f \<circ> the_inv_into A f) ` X

goal (1 subgoal):
 1. \<And>x. x \<in> (f \<circ> the_inv_into A f) ` X \<Longrightarrow> x \<in> X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (f \<circ> the_inv_into A f) ` X \<Longrightarrow> x \<in> X
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (f \<circ> the_inv_into A f) ` X \<Longrightarrow> x \<in> X
[PROOF STEP]
assume "x \<in> (f \<circ> the_inv_into A f) ` X"
[PROOF STATE]
proof (state)
this:
x \<in> (f \<circ> the_inv_into A f) ` X

goal (1 subgoal):
 1. \<And>x. x \<in> (f \<circ> the_inv_into A f) ` X \<Longrightarrow> x \<in> X
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> (f \<circ> the_inv_into A f) ` X
[PROOF STEP]
obtain x' where x': "x' \<in> X \<and> x = f (the_inv_into A f x')"
[PROOF STATE]
proof (prove)
using this:
x \<in> (f \<circ> the_inv_into A f) ` X

goal (1 subgoal):
 1. (\<And>x'. x' \<in> X \<and> x = f (the_inv_into A f x') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<in> X \<and> x = f (the_inv_into A f x')

goal (1 subgoal):
 1. \<And>x. x \<in> (f \<circ> the_inv_into A f) ` X \<Longrightarrow> x \<in> X
[PROOF STEP]
from in_range x'
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>X. x \<in> f ` A
x' \<in> X \<and> x = f (the_inv_into A f x')
[PROOF STEP]
have f: "f (the_inv_into A f x') \<in> X"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. x \<in> f ` A
x' \<in> X \<and> x = f (the_inv_into A f x')

goal (1 subgoal):
 1. f (the_inv_into A f x') \<in> X
[PROOF STEP]
by (subst f_the_inv_into_f[of f]) (auto intro: \<open>inj_on f A\<close>)
[PROOF STATE]
proof (state)
this:
f (the_inv_into A f x') \<in> X

goal (1 subgoal):
 1. \<And>x. x \<in> (f \<circ> the_inv_into A f) ` X \<Longrightarrow> x \<in> X
[PROOF STEP]
from x' \<open>X \<in> P\<close> f
[PROOF STATE]
proof (chain)
picking this:
x' \<in> X \<and> x = f (the_inv_into A f x')
X \<in> P
f (the_inv_into A f x') \<in> X
[PROOF STEP]
show "x \<in> X"
[PROOF STATE]
proof (prove)
using this:
x' \<in> X \<and> x = f (the_inv_into A f x')
X \<in> P
f (the_inv_into A f x') \<in> X

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
X = (f \<circ> the_inv_into A f) ` X

goal (2 subgoals):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (`) (f \<circ> the_inv_into A f) ` P
 2. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X \<in> P
\<forall>x\<in>X. x \<in> f ` A
X = (f \<circ> the_inv_into A f) ` X
[PROOF STEP]
show "X \<in> (`) (f \<circ> the_inv_into A f) ` P"
[PROOF STATE]
proof (prove)
using this:
X \<in> P
\<forall>x\<in>X. x \<in> f ` A
X = (f \<circ> the_inv_into A f) ` X

goal (1 subgoal):
 1. X \<in> (`) (f \<circ> the_inv_into A f) ` P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<in> (`) (f \<circ> the_inv_into A f) ` P

goal (1 subgoal):
 1. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
assume "X \<in> (`) (f \<circ> the_inv_into A f) ` P"
[PROOF STATE]
proof (state)
this:
X \<in> (`) (f \<circ> the_inv_into A f) ` P

goal (1 subgoal):
 1. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X \<in> (`) (f \<circ> the_inv_into A f) ` P

goal (1 subgoal):
 1. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
X \<in> (`) (f \<circ> the_inv_into A f) ` P

goal (1 subgoal):
 1. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
fix Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
assume "Y \<in> P"
[PROOF STATE]
proof (state)
this:
Y \<in> P

goal (1 subgoal):
 1. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
from this \<open>inj_on f A\<close> mem
[PROOF STATE]
proof (chain)
picking this:
Y \<in> P
inj_on f A
\<lbrakk>?X \<in> P; ?x \<in> ?X\<rbrakk> \<Longrightarrow> ?x \<in> f ` A
[PROOF STEP]
have "\<forall>x\<in>Y. f (the_inv_into A f x) = x"
[PROOF STATE]
proof (prove)
using this:
Y \<in> P
inj_on f A
\<lbrakk>?X \<in> P; ?x \<in> ?X\<rbrakk> \<Longrightarrow> ?x \<in> f ` A

goal (1 subgoal):
 1. \<forall>x\<in>Y. f (the_inv_into A f x) = x
[PROOF STEP]
by (auto simp add: f_the_inv_into_f)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>Y. f (the_inv_into A f x) = x

goal (1 subgoal):
 1. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>Y. f (the_inv_into A f x) = x
[PROOF STEP]
have "(f \<circ> the_inv_into A f) ` Y = Y"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>Y. f (the_inv_into A f x) = x

goal (1 subgoal):
 1. (f \<circ> the_inv_into A f) ` Y = Y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(f \<circ> the_inv_into A f) ` Y = Y

goal (1 subgoal):
 1. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?Y2 \<in> P \<Longrightarrow> (f \<circ> the_inv_into A f) ` ?Y2 = ?Y2

goal (1 subgoal):
 1. \<And>x. x \<in> (`) (f \<circ> the_inv_into A f) ` P \<Longrightarrow> x \<in> P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X \<in> (`) (f \<circ> the_inv_into A f) ` P
?Y2 \<in> P \<Longrightarrow> (f \<circ> the_inv_into A f) ` ?Y2 = ?Y2
[PROOF STEP]
show "X \<in> P"
[PROOF STATE]
proof (prove)
using this:
X \<in> (`) (f \<circ> the_inv_into A f) ` P
?Y2 \<in> P \<Longrightarrow> (f \<circ> the_inv_into A f) ` ?Y2 = ?Y2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P = (`) (f \<circ> the_inv_into A f) ` P

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(`) (f \<circ> the_inv_into A f) ` P = (`) f ` (`) (the_inv_into A f) ` P
P = (`) (f \<circ> the_inv_into A f) ` P
[PROOF STEP]
have P: "P = (`) f ` (`) (the_inv_into A f) ` P"
[PROOF STATE]
proof (prove)
using this:
(`) (f \<circ> the_inv_into A f) ` P = (`) f ` (`) (the_inv_into A f) ` P
P = (`) (f \<circ> the_inv_into A f) ` P

goal (1 subgoal):
 1. P = (`) f ` (`) (the_inv_into A f) ` P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P = (`) f ` (`) (the_inv_into A f) ` P

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
have A_eq: "A = the_inv_into A f ` f ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = the_inv_into A f ` f ` A
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
A = the_inv_into A f ` f ` A

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
from \<open>inj_on f A\<close>
[PROOF STATE]
proof (chain)
picking this:
inj_on f A
[PROOF STEP]
have "inj_on (the_inv_into A f) (f ` A)"
[PROOF STATE]
proof (prove)
using this:
inj_on f A

goal (1 subgoal):
 1. inj_on (the_inv_into A f) (f ` A)
[PROOF STEP]
using \<open>partition_on (f ` A) P\<close>
[PROOF STATE]
proof (prove)
using this:
inj_on f A
partition_on (f ` A) P

goal (1 subgoal):
 1. inj_on (the_inv_into A f) (f ` A)
[PROOF STEP]
by (simp add: inj_on_the_inv_into)
[PROOF STATE]
proof (state)
this:
inj_on (the_inv_into A f) (f ` A)

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
inj_on (the_inv_into A f) (f ` A)
[PROOF STEP]
have  "(`) (the_inv_into A f) ` P \<in> {P. partition_on A P}"
[PROOF STATE]
proof (prove)
using this:
inj_on (the_inv_into A f) (f ` A)

goal (1 subgoal):
 1. (`) (the_inv_into A f) ` P \<in> {P. partition_on A P}
[PROOF STEP]
using \<open>partition_on (f ` A) P\<close>
[PROOF STATE]
proof (prove)
using this:
inj_on (the_inv_into A f) (f ` A)
partition_on (f ` A) P

goal (1 subgoal):
 1. (`) (the_inv_into A f) ` P \<in> {P. partition_on A P}
[PROOF STEP]
by (subst A_eq, auto intro!: partition_on_map)
[PROOF STATE]
proof (state)
this:
(`) (the_inv_into A f) ` P \<in> {P. partition_on A P}

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (f ` A) P} \<Longrightarrow> x \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
from P this
[PROOF STATE]
proof (chain)
picking this:
P = (`) f ` (`) (the_inv_into A f) ` P
(`) (the_inv_into A f) ` P \<in> {P. partition_on A P}
[PROOF STEP]
show "P \<in> (`) ((`) f) ` {P. partition_on A P}"
[PROOF STATE]
proof (prove)
using this:
P = (`) f ` (`) (the_inv_into A f) ` P
(`) (the_inv_into A f) ` P \<in> {P. partition_on A P}

goal (1 subgoal):
 1. P \<in> (`) ((`) f) ` {P. partition_on A P}
[PROOF STEP]
by (rule image_eqI)
[PROOF STATE]
proof (state)
this:
P \<in> (`) ((`) f) ` {P. partition_on A P}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_methodI:
  "P \<turnstile> C sees M,b:Ts\<rightarrow>T = m in D \<Longrightarrow> P \<turnstile> C has M,b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> P \<turnstile> C has M, b
[PROOF STEP]
by (unfold has_method_def) blast


[STATEMENT]
lemma typeof_NoneD [simp,dest]: "typeof v = Some x \<Longrightarrow> \<not>is_Addr v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof v = \<lfloor>x\<rfloor> \<Longrightarrow> \<not> is_Addr v
[PROOF STEP]
by (cases v) auto


[STATEMENT]
lemma is_Ref_def2:
  "is_Ref v = (v = Null \<or> (\<exists>a. v = Addr a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Ref v = (v = Null \<or> (\<exists>a. v = Addr a))
[PROOF STEP]
by (cases v) (auto simp add: is_Ref_def)


[STATEMENT]
lemma [iff]: "is_Ref Null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Ref Null
[PROOF STEP]
by (simp add: is_Ref_def2)


[STATEMENT]
lemma is_RefI [intro, simp]: "P,h \<turnstile> v :\<le> T \<Longrightarrow> is_refT T \<Longrightarrow> is_Ref v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> v :\<le> T; is_refT T\<rbrakk> \<Longrightarrow> is_Ref v
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> v :\<le> T; is_refT T\<rbrakk> \<Longrightarrow> is_Ref v
[PROOF STEP]
proof(cases T)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>P,h \<turnstile> v :\<le> T; is_refT T; T = Void\<rbrakk> \<Longrightarrow> is_Ref v
 2. \<lbrakk>P,h \<turnstile> v :\<le> T; is_refT T; T = Boolean\<rbrakk> \<Longrightarrow> is_Ref v
 3. \<lbrakk>P,h \<turnstile> v :\<le> T; is_refT T; T = Integer\<rbrakk> \<Longrightarrow> is_Ref v
 4. \<lbrakk>P,h \<turnstile> v :\<le> T; is_refT T; T = NT\<rbrakk> \<Longrightarrow> is_Ref v
 5. \<And>x5. \<lbrakk>P,h \<turnstile> v :\<le> T; is_refT T; T = Class x5\<rbrakk> \<Longrightarrow> is_Ref v
[PROOF STEP]
qed (auto simp add: is_refT_def is_Ref_def dest: conf_ClassD)


[STATEMENT]
lemma is_BoolI [intro, simp]: "P,h \<turnstile> v :\<le> Boolean \<Longrightarrow> is_Bool v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> v :\<le> Boolean \<Longrightarrow> is_Bool v
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> v :\<le> Boolean \<Longrightarrow> is_Bool v
[PROOF STEP]
by (unfold conf_def) auto


[STATEMENT]
lemma wt_jvm_prog_states_NonStatic:
assumes wf: "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P"
  and mC: "P \<turnstile> C sees M,NonStatic: Ts\<rightarrow>T = (mxs, mxl, ins, et) in C"
  and \<Phi>: "\<Phi> C M ! pc = \<tau>" and pc: "pc < size ins"
shows "OK \<tau> \<in> states P mxs (1+size Ts+mxl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (1 + length Ts + mxl)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (1 + length Ts + mxl)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (1 + length Ts + mxl)
[PROOF STEP]
let ?wf_md = "(\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt).
                       wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (1 + length Ts + mxl)
[PROOF STEP]
have wfmd: "wf_prog ?wf_md P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>\<Phi>\<^esub> P

goal (1 subgoal):
 1. wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P
[PROOF STEP]
by (unfold wf_jvm_prog_phi_def) assumption
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P

goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (1 + length Ts + mxl)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (1 + length Ts + mxl)
[PROOF STEP]
using sees_wf_mdecl[OF wfmd mC] \<Phi> pc
[PROOF STATE]
proof (prove)
using this:
wf_mdecl (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P C (M, NonStatic, Ts, T, mxs, mxl, ins, et)
\<Phi> C M ! pc = \<tau>
pc < length ins

goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (1 + length Ts + mxl)
[PROOF STEP]
by (simp add: wf_mdecl_def wt_method_def check_types_def)
       (blast intro: nth_in)
[PROOF STATE]
proof (state)
this:
OK \<tau> \<in> states P mxs (1 + length Ts + mxl)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wt_jvm_prog_states_Static:
assumes wf: "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P"
  and mC: "P \<turnstile> C sees M,Static: Ts\<rightarrow>T = (mxs, mxl, ins, et) in C"
  and \<Phi>: "\<Phi> C M ! pc = \<tau>" and pc: "pc < size ins"
shows "OK \<tau> \<in> states P mxs (size Ts+mxl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (length Ts + mxl)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (length Ts + mxl)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (length Ts + mxl)
[PROOF STEP]
let ?wf_md = "(\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt).
                       wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (length Ts + mxl)
[PROOF STEP]
have wfmd: "wf_prog ?wf_md P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>\<Phi>\<^esub> P

goal (1 subgoal):
 1. wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P
[PROOF STEP]
by (unfold wf_jvm_prog_phi_def) assumption
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P

goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (length Ts + mxl)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (length Ts + mxl)
[PROOF STEP]
using sees_wf_mdecl[OF wfmd mC] \<Phi> pc
[PROOF STATE]
proof (prove)
using this:
wf_mdecl (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P C (M, Static, Ts, T, mxs, mxl, ins, et)
\<Phi> C M ! pc = \<tau>
pc < length ins

goal (1 subgoal):
 1. OK \<tau> \<in> states P mxs (length Ts + mxl)
[PROOF STEP]
by (simp add: wf_mdecl_def wt_method_def check_types_def)
       (blast intro: nth_in)
[PROOF STATE]
proof (state)
this:
OK \<tau> \<in> states P mxs (length Ts + mxl)

goal:
No subgoals!
[PROOF STEP]
qed