[STATEMENT]
lemma min_None:
     "\<lbrakk> invar s; min s P = None \<rbrakk> \<Longrightarrow> {x\<in>\<alpha> s. P x} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; min s P = None\<rbrakk> \<Longrightarrow> {x \<in> \<alpha> s. P x} = {}
[PROOF STEP]
apply (cases "{x\<in>\<alpha> s. P x} = {}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; min s P = None; {x \<in> \<alpha> s. P x} = {}\<rbrakk> \<Longrightarrow> {x \<in> \<alpha> s. P x} = {}
 2. \<lbrakk>invar s; min s P = None; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> {x \<in> \<alpha> s. P x} = {}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; min s P = None; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> {x \<in> \<alpha> s. P x} = {}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; min s P = None; \<exists>x. x \<in> \<alpha> s \<and> P x\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> \<alpha> s \<longrightarrow> \<not> P x
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>invar s; min s P = None; x \<in> \<alpha> s \<and> P x\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> \<alpha> s \<longrightarrow> \<not> P x
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>invar s; min s P = None; x \<in> \<alpha> s; P x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule (2) min_correct(1)[where P=P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>min s P = None; x \<in> \<alpha> s; P x; xa \<in> \<alpha> s; P xa; min s P \<in> Some ` {x \<in> \<alpha> s. P x}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma maxE:
     assumes A: "invar s" "x\<in>\<alpha> s" "P x"
     obtains x' where
     "max s P = Some x'" "x'\<in>\<alpha> s" "P x'" "\<forall>x\<in>\<alpha> s. P x \<longrightarrow> x' \<ge> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>max s P = Some x'; x' \<in> \<alpha> s; P x'; \<forall>x\<in>\<alpha> s. P x \<longrightarrow> x \<le> x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>max s P = Some x'; x' \<in> \<alpha> s; P x'; \<forall>x\<in>\<alpha> s. P x \<longrightarrow> x \<le> x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from max_correct(1)[where P=P, OF A]
[PROOF STATE]
proof (chain)
picking this:
max s P \<in> Some ` {x \<in> \<alpha> s. P x}
[PROOF STEP]
have
       MIS: "max s P \<in> Some ` {x\<in>\<alpha> s. P x}"
[PROOF STATE]
proof (prove)
using this:
max s P \<in> Some ` {x \<in> \<alpha> s. P x}

goal (1 subgoal):
 1. max s P \<in> Some ` {x \<in> \<alpha> s. P x}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
max s P \<in> Some ` {x \<in> \<alpha> s. P x}

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>max s P = Some x'; x' \<in> \<alpha> s; P x'; \<forall>x\<in>\<alpha> s. P x \<longrightarrow> x \<le> x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max s P \<in> Some ` {x \<in> \<alpha> s. P x}
[PROOF STEP]
obtain x' where KV: "max s P = Some x'" "x'\<in> \<alpha> s" "P x'"
[PROOF STATE]
proof (prove)
using this:
max s P \<in> Some ` {x \<in> \<alpha> s. P x}

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>max s P = Some x'; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max s P = Some x'
x' \<in> \<alpha> s
P x'

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>max s P = Some x'; x' \<in> \<alpha> s; P x'; \<forall>x\<in>\<alpha> s. P x \<longrightarrow> x \<le> x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply (rule that[OF KV])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>\<alpha> s. P x \<longrightarrow> x \<le> x'
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> \<alpha> s; P x\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply (drule (1) max_correct(2)[OF \<open>invar s\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>P x; x \<le> the (max s P)\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply (simp add: KV(1))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_Some:
     "\<lbrakk> invar s; max s P = Some x \<rbrakk> \<Longrightarrow> x\<in>\<alpha> s"
     "\<lbrakk> invar s; max s P = Some x \<rbrakk> \<Longrightarrow> P x"
     "\<lbrakk> invar s; max s P = Some x; x'\<in>\<alpha> s; P x'\<rbrakk> \<Longrightarrow> x\<ge>x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s) &&& (\<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> P x) &&& (\<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply (cases "{x\<in>\<alpha> s. P x} = {}")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>invar s; max s P = Some x; {x \<in> \<alpha> s. P x} = {}\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; max s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 3. \<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> P x
 4. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply (drule (1) max_correct(3))
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>max s P = Some x; {x \<in> \<alpha> s. P x} = {}; max s P = None\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; max s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 3. \<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> P x
 4. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invar s; max s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invar s; max s P = Some x; \<exists>x. x \<in> \<alpha> s \<and> P x\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>invar s; max s P = Some x; xa \<in> \<alpha> s \<and> P xa\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>invar s; max s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply (drule (2) max_correct(1)[of s _ P])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>max s P = Some x; xa \<in> \<alpha> s; P xa; max s P \<in> Some ` {x \<in> \<alpha> s. P x}\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply auto [1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; max s P = Some x\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply (cases "{x\<in>\<alpha> s. P x} = {}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invar s; max s P = Some x; {x \<in> \<alpha> s. P x} = {}\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; max s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply (drule (1) max_correct(3))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>max s P = Some x; {x \<in> \<alpha> s. P x} = {}; max s P = None\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; max s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; max s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; max s P = Some x; \<exists>x. x \<in> \<alpha> s \<and> P x\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>invar s; max s P = Some x; xa \<in> \<alpha> s \<and> P xa\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>invar s; max s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply (drule (2) max_correct(1)[of s _ P])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>max s P = Some x; xa \<in> \<alpha> s; P xa; max s P \<in> Some ` {x \<in> \<alpha> s. P x}\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply auto [1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply (drule (1) max_correct(2)[where P=P])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>max s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> P x'
 2. \<lbrakk>max s P = Some x; x' \<in> \<alpha> s; P x'; x' \<le> the (max s P)\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma max_None:
     "\<lbrakk> invar s; max s P = None \<rbrakk> \<Longrightarrow> {x\<in>\<alpha> s. P x} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; max s P = None\<rbrakk> \<Longrightarrow> {x \<in> \<alpha> s. P x} = {}
[PROOF STEP]
apply (cases "{x\<in>\<alpha> s. P x} = {}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; max s P = None; {x \<in> \<alpha> s. P x} = {}\<rbrakk> \<Longrightarrow> {x \<in> \<alpha> s. P x} = {}
 2. \<lbrakk>invar s; max s P = None; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> {x \<in> \<alpha> s. P x} = {}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; max s P = None; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> {x \<in> \<alpha> s. P x} = {}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; max s P = None; \<exists>x. x \<in> \<alpha> s \<and> P x\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> \<alpha> s \<longrightarrow> \<not> P x
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>invar s; max s P = None; x \<in> \<alpha> s \<and> P x\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> \<alpha> s \<longrightarrow> \<not> P x
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>invar s; max s P = None; x \<in> \<alpha> s; P x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule (1) max_correct(1)[where P=P])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>max s P = None; x \<in> \<alpha> s; P x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> P x
 2. \<And>x xa. \<lbrakk>max s P = None; x \<in> \<alpha> s; P x; xa \<in> \<alpha> s; P xa; max s P \<in> Some ` {x \<in> \<alpha> s. P x}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_UNIV_nat: "icard (UNIV::nat set) = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard UNIV = \<infinity>
[PROOF STEP]
by (simp add: icard_def)


[STATEMENT]
lemma icard_finite_conv: "(icard A = enat (card A)) = finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (icard A = enat (card A)) = finite A
[PROOF STEP]
by (case_tac "finite A", simp_all add: icard_def)


[STATEMENT]
lemma icard_infinite_conv: "(icard A = \<infinity>) = infinite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (icard A = \<infinity>) = infinite A
[PROOF STEP]
by (case_tac "finite A", simp_all add: icard_def)


[STATEMENT]
lemma icard_eq_enat_imp: "icard A = enat n \<Longrightarrow> finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard A = enat n \<Longrightarrow> finite A
[PROOF STEP]
by (case_tac "finite A", simp_all)


[STATEMENT]
lemma icard_eq_Infty_imp: "icard A = \<infinity> \<Longrightarrow> infinite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard A = \<infinity> \<Longrightarrow> infinite A
[PROOF STEP]
by (rule icard_infinite_conv[THEN iffD1])


[STATEMENT]
lemma icard_the_enat: "finite A \<Longrightarrow> the_enat (icard A) = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> the_enat (icard A) = card A
[PROOF STEP]
by (simp add: icard_def)


[STATEMENT]
lemma icard_eq_enat_imp_card: "icard A = enat n \<Longrightarrow> card A = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard A = enat n \<Longrightarrow> card A = n
[PROOF STEP]
by (frule icard_eq_enat_imp, simp add: icard_finite)


[STATEMENT]
lemma icard_eq_enat_card_conv: "0 < n \<Longrightarrow> (icard A = enat n) = (card A = n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (icard A = enat n) = (card A = n)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; icard A = enat n\<rbrakk> \<Longrightarrow> card A = n
 2. \<lbrakk>0 < n; card A = n\<rbrakk> \<Longrightarrow> icard A = enat n
[PROOF STEP]
apply (simp add: icard_eq_enat_imp_card)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; card A = n\<rbrakk> \<Longrightarrow> icard A = enat n
[PROOF STEP]
apply (drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < card A; n = card A\<rbrakk> \<Longrightarrow> icard A = enat (card A)
[PROOF STEP]
apply (frule card_gr0_imp_finite)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < card A; n = card A; finite A\<rbrakk> \<Longrightarrow> icard A = enat (card A)
[PROOF STEP]
apply (rule icard_finite, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_empty[simp]: "icard {} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard {} = 0
[PROOF STEP]
by (simp add: icard_finite[OF finite.emptyI])


[STATEMENT]
lemma icard_empty_iff: "(icard A = 0) = (A = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (icard A = 0) = (A = {})
[PROOF STEP]
apply (unfold zero_enat_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (icard A = enat 0) = (A = {})
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. icard A = enat 0 \<Longrightarrow> A = {}
 2. A = {} \<Longrightarrow> icard A = enat 0
[PROOF STEP]
apply (frule icard_eq_enat_imp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>icard A = enat 0; finite A\<rbrakk> \<Longrightarrow> A = {}
 2. A = {} \<Longrightarrow> icard A = enat 0
[PROOF STEP]
apply (simp add: icard_finite)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = {} \<Longrightarrow> icard A = enat 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_singleton: "icard {a} = eSuc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard {a} = eSuc 0
[PROOF STEP]
by (simp add: icard_finite eSuc_enat)


[STATEMENT]
lemma icard_1_singleton_conv: "(icard A = eSuc 0) = (\<exists>a. A = {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (icard A = eSuc 0) = (\<exists>a. A = {a})
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. icard A = eSuc 0 \<Longrightarrow> \<exists>a. A = {a}
 2. \<exists>a. A = {a} \<Longrightarrow> icard A = eSuc 0
[PROOF STEP]
apply (simp add: icard_1_imp_singleton)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. A = {a} \<Longrightarrow> icard A = eSuc 0
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_insert_if: "icard (insert x A) = (if x \<in> A then icard A else eSuc (icard A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard (insert x A) = (if x \<in> A then icard A else eSuc (icard A))
[PROOF STEP]
apply (case_tac "x \<in> A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> A \<Longrightarrow> icard (insert x A) = (if x \<in> A then icard A else eSuc (icard A))
 2. x \<notin> A \<Longrightarrow> icard (insert x A) = (if x \<in> A then icard A else eSuc (icard A))
[PROOF STEP]
apply (simp add: insert_absorb)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> icard (insert x A) = (if x \<in> A then icard A else eSuc (icard A))
[PROOF STEP]
apply (simp add: icard_insert_disjoint)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_Suc_Diff1: "x \<in> A \<Longrightarrow> eSuc (icard (A - {x})) = icard A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> eSuc (icard (A - {x})) = icard A
[PROOF STEP]
apply (case_tac "finite A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> A; finite A\<rbrakk> \<Longrightarrow> eSuc (icard (A - {x})) = icard A
 2. \<lbrakk>x \<in> A; infinite A\<rbrakk> \<Longrightarrow> eSuc (icard (A - {x})) = icard A
[PROOF STEP]
apply (simp add: icard_finite eSuc_enat in_imp_not_empty not_empty_card_gr0_conv[THEN iffD1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; infinite A\<rbrakk> \<Longrightarrow> eSuc (icard (A - {x})) = icard A
[PROOF STEP]
apply (simp add: Diff_infinite_finite[OF singleton_finite])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_Diff_singleton: "x \<in> A \<Longrightarrow> icard (A - {x}) = icard A - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> icard (A - {x}) = icard A - 1
[PROOF STEP]
apply (rule eSuc_inject[THEN iffD1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> eSuc (icard (A - {x})) = eSuc (icard A - 1)
[PROOF STEP]
apply (frule in_imp_not_empty, drule icard_not_empty_iff[THEN iffD2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; 0 < icard A\<rbrakk> \<Longrightarrow> eSuc (icard (A - {x})) = eSuc (icard A - 1)
[PROOF STEP]
apply (simp add: icard_Suc_Diff1 eSuc_pred_enat one_eSuc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_Diff_singleton_if: "icard (A - {x}) = (if x \<in> A then icard A - 1 else icard A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard (A - {x}) = (if x \<in> A then icard A - 1 else icard A)
[PROOF STEP]
by (simp add: icard_Diff_singleton)


[STATEMENT]
lemma icard_insert: "icard (insert x A) = eSuc (icard (A - {x}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard (insert x A) = eSuc (icard (A - {x}))
[PROOF STEP]
by (metis icard_Diff_singleton_if icard_Suc_Diff1 icard_insert_disjoint insert_absorb)


[STATEMENT]
lemma icard_insert_le: "icard A \<le> icard (insert x A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard A \<le> icard (insert x A)
[PROOF STEP]
by (simp add: icard_insert_if)


[STATEMENT]
lemma icard_mono: "A \<subseteq> B \<Longrightarrow> icard A \<le> icard B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> icard A \<le> icard B
[PROOF STEP]
apply (case_tac "finite B")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<subseteq> B; finite B\<rbrakk> \<Longrightarrow> icard A \<le> icard B
 2. \<lbrakk>A \<subseteq> B; infinite B\<rbrakk> \<Longrightarrow> icard A \<le> icard B
[PROOF STEP]
apply (frule subset_finite_imp_finite, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<subseteq> B; finite B; finite A\<rbrakk> \<Longrightarrow> icard A \<le> icard B
 2. \<lbrakk>A \<subseteq> B; infinite B\<rbrakk> \<Longrightarrow> icard A \<le> icard B
[PROOF STEP]
apply (simp add: icard_finite card_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; infinite B\<rbrakk> \<Longrightarrow> icard A \<le> icard B
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_icard_seteq: "\<exists>(A::nat set) B. (A \<subseteq> B \<and> icard B \<le> icard A \<and> \<not> A = B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A B. A \<subseteq> B \<and> icard B \<le> icard A \<and> A \<noteq> B
[PROOF STEP]
apply (rule_tac x="{1..}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B. {1..} \<subseteq> B \<and> icard B \<le> icard {1..} \<and> {1..} \<noteq> B
[PROOF STEP]
apply (rule_tac x="{0..}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {1..} \<subseteq> {0..} \<and> icard {0..} \<le> icard {1..} \<and> {1..} \<noteq> {0..}
[PROOF STEP]
apply (fastforce simp add: infinite_atLeast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_psubset_icard_mono: "\<exists>(A::nat set) B. A \<subset> B \<and> \<not> icard A < icard B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A B. A \<subset> B \<and> \<not> icard A < icard B
[PROOF STEP]
apply (rule_tac x="{1..}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B. {1..} \<subset> B \<and> \<not> icard {1..} < icard B
[PROOF STEP]
apply (rule_tac x="{0..}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {1..} \<subset> {0..} \<and> \<not> icard {1..} < icard {0..}
[PROOF STEP]
apply (fastforce simp add: infinite_atLeast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_Un_Int: "icard A + icard B = icard (A \<union> B) + icard (A \<inter> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard A + icard B = icard (A \<union> B) + icard (A \<inter> B)
[PROOF STEP]
apply (case_tac "finite A", case_tac "finite B")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> icard A + icard B = icard (A \<union> B) + icard (A \<inter> B)
 2. \<lbrakk>finite A; infinite B\<rbrakk> \<Longrightarrow> icard A + icard B = icard (A \<union> B) + icard (A \<inter> B)
 3. infinite A \<Longrightarrow> icard A + icard B = icard (A \<union> B) + icard (A \<inter> B)
[PROOF STEP]
apply (simp add: icard_finite card_Un_Int[of A])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite A; infinite B\<rbrakk> \<Longrightarrow> icard A + icard B = icard (A \<union> B) + icard (A \<inter> B)
 2. infinite A \<Longrightarrow> icard A + icard B = icard (A \<union> B) + icard (A \<inter> B)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_Un_disjoint: "A \<inter> B = {} \<Longrightarrow> icard (A \<union> B) = icard A + icard B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> B = {} \<Longrightarrow> icard (A \<union> B) = icard A + icard B
[PROOF STEP]
by (simp add: icard_Un_Int[of A])


[STATEMENT]
lemma not_icard_Diff_subset: "\<exists>(A::nat set) B. B \<subseteq> A \<and> \<not> icard (A - B) = icard A - icard B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A B. B \<subseteq> A \<and> icard (A - B) \<noteq> icard A - icard B
[PROOF STEP]
apply (rule_tac x="{0..}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B\<subseteq>{0..}. icard ({0..} - B) \<noteq> icard {0..} - icard B
[PROOF STEP]
apply (rule_tac x="{1..}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {1..} \<subseteq> {0..} \<and> icard ({0..} - {1..}) \<noteq> icard {0..} - icard {1..}
[PROOF STEP]
apply (simp add: set_diff_eq linorder_not_le icard_UNIV_nat eSuc_enat)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_icard_Diff1_less: "\<exists>(A::nat set)x. x \<in> A \<and> \<not> icard (A - {x}) < icard A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A x. x \<in> A \<and> \<not> icard (A - {x}) < icard A
[PROOF STEP]
by (rule_tac x="{0..}" in exI, simp)


[STATEMENT]
lemma not_icard_Diff2_less: "\<exists>(A::nat set)x y. x \<in> A \<and> y \<in> A \<and> \<not> icard (A - {x} - {y}) < icard A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A x y. x \<in> A \<and> y \<in> A \<and> \<not> icard (A - {x} - {y}) < icard A
[PROOF STEP]
by (rule_tac x="{0..}" in exI, simp)


[STATEMENT]
lemma icard_Diff1_le: "icard (A - {x}) \<le> icard A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard (A - {x}) \<le> icard A
[PROOF STEP]
by (rule icard_mono, rule Diff_subset)


[STATEMENT]
lemma icard_psubset: "\<lbrakk> A \<subseteq> B; icard A < icard B \<rbrakk> \<Longrightarrow> A \<subset> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; icard A < icard B\<rbrakk> \<Longrightarrow> A \<subset> B
[PROOF STEP]
by (metis less_le psubset_eq)


[STATEMENT]
lemma icard_partition: "
  \<lbrakk> \<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {} \<rbrakk> \<Longrightarrow>
  icard (\<Union>C) = k * icard C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (case_tac "C = {}", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (case_tac "k = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = 0\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 2. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k \<noteq> 0\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (simp add: icard_empty_iff_enat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k \<noteq> 0\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (case_tac k, rename_tac k1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 2. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (subgoal_tac "0 < k1")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 2. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1\<rbrakk> \<Longrightarrow> 0 < k1
 3. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1\<rbrakk> \<Longrightarrow> 0 < k1
 2. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 3. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 2. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (case_tac "finite C")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; finite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 2. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 3. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (simp add: icard_finite)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = enat (k1 * card C)
 2. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 3. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (subgoal_tac "\<And>c. c \<in> C \<Longrightarrow> card c = k1")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k1\<rbrakk> \<Longrightarrow> icard (\<Union> C) = enat (k1 * card C)
 2. \<And>k1 c. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; c \<in> C\<rbrakk> \<Longrightarrow> card c = k1
 3. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 4. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>k1 c. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; c \<in> C\<rbrakk> \<Longrightarrow> card c = k1
 2. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k1\<rbrakk> \<Longrightarrow> icard (\<Union> C) = enat (k1 * card C)
 3. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 4. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (rule icard_eq_enat_imp_card, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k1\<rbrakk> \<Longrightarrow> icard (\<Union> C) = enat (k1 * card C)
 2. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 3. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (frule_tac C=C and k=k1 in SetInterval2.card_partition, simp+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k1; card (\<Union> C) = k1 * card C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = enat (k1 * card C)
 2. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 3. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (subgoal_tac "finite (\<Union>C)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k1; card (\<Union> C) = k1 * card C; finite (\<Union> C)\<rbrakk> \<Longrightarrow> icard (\<Union> C) = enat (k1 * card C)
 2. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k1; card (\<Union> C) = k1 * card C\<rbrakk> \<Longrightarrow> finite (\<Union> C)
 3. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 4. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k1; card (\<Union> C) = k1 * card C\<rbrakk> \<Longrightarrow> finite (\<Union> C)
 2. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k1; card (\<Union> C) = k1 * card C; finite (\<Union> C)\<rbrakk> \<Longrightarrow> icard (\<Union> C) = enat (k1 * card C)
 3. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 4. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (rule card_gr0_imp_finite)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k1; card (\<Union> C) = k1 * card C\<rbrakk> \<Longrightarrow> 0 < card (\<Union> C)
 2. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k1; card (\<Union> C) = k1 * card C; finite (\<Union> C)\<rbrakk> \<Longrightarrow> icard (\<Union> C) = enat (k1 * card C)
 3. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 4. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (simp add: not_empty_card_gr0_conv)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; finite C; \<And>c. c \<in> C \<Longrightarrow> card c = k1; card (\<Union> C) = k1 * card C; finite (\<Union> C)\<rbrakk> \<Longrightarrow> icard (\<Union> C) = enat (k1 * card C)
 2. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 3. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (simp add: icard_finite)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
 2. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = \<infinity>
 2. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (rule icard_infinite)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; infinite C\<rbrakk> \<Longrightarrow> infinite (\<Union> C)
 2. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (rule ccontr, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = enat k1; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = enat k1; 0 < k1; infinite C; finite (\<Union> C)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (drule finite_UnionD, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (frule icard_not_empty_iff[THEN iffD2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> icard c = k; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; enat 0 < k; k = \<infinity>; 0 < icard C\<rbrakk> \<Longrightarrow> icard (\<Union> C) = k * icard C
[PROOF STEP]
apply (simp add: icard_infinite_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> infinite c; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = \<infinity>; enat 0 < icard C\<rbrakk> \<Longrightarrow> infinite (\<Union> C)
[PROOF STEP]
apply (frule not_empty_imp_ex, erule exE, rename_tac c)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> infinite c; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = \<infinity>; enat 0 < icard C; c \<in> C\<rbrakk> \<Longrightarrow> infinite (\<Union> C)
[PROOF STEP]
apply (frule Union_upper)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> infinite c; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = \<infinity>; enat 0 < icard C; c \<in> C; c \<subseteq> \<Union> C\<rbrakk> \<Longrightarrow> infinite (\<Union> C)
[PROOF STEP]
apply (rule infinite_super, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>\<And>c. c \<in> C \<Longrightarrow> infinite c; \<And>c1 c2. \<lbrakk>c1 \<in> C; c2 \<in> C; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}; C \<noteq> {}; k = \<infinity>; enat 0 < icard C; c \<in> C; c \<subseteq> \<Union> C\<rbrakk> \<Longrightarrow> infinite c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_image_le: "icard (f ` A) \<le> icard A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard (f ` A) \<le> icard A
[PROOF STEP]
apply (case_tac "finite A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite A \<Longrightarrow> icard (f ` A) \<le> icard A
 2. infinite A \<Longrightarrow> icard (f ` A) \<le> icard A
[PROOF STEP]
apply (simp add: icard_finite card_image_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite A \<Longrightarrow> icard (f ` A) \<le> icard A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_image: "inj_on f A \<Longrightarrow> icard (f ` A) = icard A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f A \<Longrightarrow> icard (f ` A) = icard A
[PROOF STEP]
apply (case_tac "finite A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj_on f A; finite A\<rbrakk> \<Longrightarrow> icard (f ` A) = icard A
 2. \<lbrakk>inj_on f A; infinite A\<rbrakk> \<Longrightarrow> icard (f ` A) = icard A
[PROOF STEP]
apply (simp add: icard_finite card_image)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f A; infinite A\<rbrakk> \<Longrightarrow> icard (f ` A) = icard A
[PROOF STEP]
apply (simp add: icard_infinite_conv inj_on_imp_infinite_image)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_eq_icard_imp_inj_on: "\<exists>(f::nat\<Rightarrow>nat) (A::nat set). icard (f ` A) = icard A \<and> \<not> inj_on f A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f A. icard (f ` A) = icard A \<and> \<not> inj_on f A
[PROOF STEP]
apply (rule_tac x="\<lambda>n. (if n = 0 then Suc 0 else n)" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. icard ((\<lambda>n. if n = 0 then Suc 0 else n) ` A) = icard A \<and> \<not> inj_on (\<lambda>n. if n = 0 then Suc 0 else n) A
[PROOF STEP]
apply (rule_tac x="{0..}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard ((\<lambda>n. if n = 0 then Suc 0 else n) ` {0..}) = icard {0..} \<and> \<not> inj_on (\<lambda>n. if n = 0 then Suc 0 else n) {0..}
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. icard ((\<lambda>n. if n = 0 then Suc 0 else n) ` {0..}) = icard {0..}
 2. \<not> inj_on (\<lambda>n. if n = 0 then Suc 0 else n) {0..}
[PROOF STEP]
apply (rule subst[of "{1..}" "((\<lambda>n. if n = 0 then Suc 0 else n) ` {0..})"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. {1..} = (\<lambda>n. if n = 0 then Suc 0 else n) ` {0..}
 2. icard {1..} = icard {0..}
 3. \<not> inj_on (\<lambda>n. if n = 0 then Suc 0 else n) {0..}
[PROOF STEP]
apply (simp add: set_eq_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>x. (Suc 0 \<le> x) = (x = Suc 0 \<or> 0 < x)
 2. icard {1..} = icard {0..}
 3. \<not> inj_on (\<lambda>n. if n = 0 then Suc 0 else n) {0..}
[PROOF STEP]
apply (rule allI, rename_tac n)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. (Suc 0 \<le> n) = (n = Suc 0 \<or> 0 < n)
 2. icard {1..} = icard {0..}
 3. \<not> inj_on (\<lambda>n. if n = 0 then Suc 0 else n) {0..}
[PROOF STEP]
apply (case_tac "n = 0", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. n \<noteq> 0 \<Longrightarrow> (Suc 0 \<le> n) = (n = Suc 0 \<or> 0 < n)
 2. icard {1..} = icard {0..}
 3. \<not> inj_on (\<lambda>n. if n = 0 then Suc 0 else n) {0..}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. icard {1..} = icard {0..}
 2. \<not> inj_on (\<lambda>n. if n = 0 then Suc 0 else n) {0..}
[PROOF STEP]
apply (simp only: icard_infinite[OF infinite_atLeast])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> inj_on (\<lambda>n. if n = 0 then Suc 0 else n) {0..}
[PROOF STEP]
apply (simp add: inj_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. (x = 0 \<longrightarrow> (\<exists>y>0. 0 < y \<longrightarrow> Suc 0 = y)) \<and> (0 < x \<longrightarrow> x = Suc 0)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_inj_on_iff_eq_icard: "\<exists>(f::nat\<Rightarrow>nat) (A::nat set). \<not> (inj_on f A = (icard (f ` A) = icard A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f A. inj_on f A \<noteq> (icard (f ` A) = icard A)
[PROOF STEP]
by (insert not_eq_icard_imp_inj_on, blast)


[STATEMENT]
lemma icard_inj_on_le: "\<lbrakk> inj_on f A; f ` A \<subseteq> B \<rbrakk> \<Longrightarrow> icard A \<le> icard B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f A; f ` A \<subseteq> B\<rbrakk> \<Longrightarrow> icard A \<le> icard B
[PROOF STEP]
apply (case_tac "finite B")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj_on f A; f ` A \<subseteq> B; finite B\<rbrakk> \<Longrightarrow> icard A \<le> icard B
 2. \<lbrakk>inj_on f A; f ` A \<subseteq> B; infinite B\<rbrakk> \<Longrightarrow> icard A \<le> icard B
[PROOF STEP]
apply (metis icard_image icard_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f A; f ` A \<subseteq> B; infinite B\<rbrakk> \<Longrightarrow> icard A \<le> icard B
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_bij_eq: "
  \<lbrakk> inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A \<rbrakk> \<Longrightarrow>
  icard A = icard B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A\<rbrakk> \<Longrightarrow> icard A = icard B
[PROOF STEP]
by (simp add: order_eq_iff icard_inj_on_le)


[STATEMENT]
lemma icard_cartesian_product: "icard (A \<times> B) = icard A * icard B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard (A \<times> B) = icard A * icard B
[PROOF STEP]
apply (case_tac "A = {} \<or> B = {}", fastforce)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {}) \<Longrightarrow> icard (A \<times> B) = icard A * icard B
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> icard (A \<times> B) = icard A * icard B
[PROOF STEP]
apply (case_tac "finite A \<and> finite B")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}; finite A \<and> finite B\<rbrakk> \<Longrightarrow> icard (A \<times> B) = icard A * icard B
 2. \<lbrakk>A \<noteq> {}; B \<noteq> {}; \<not> (finite A \<and> finite B)\<rbrakk> \<Longrightarrow> icard (A \<times> B) = icard A * icard B
[PROOF STEP]
apply (simp add: icard_finite)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}; \<not> (finite A \<and> finite B)\<rbrakk> \<Longrightarrow> icard (A \<times> B) = icard A * icard B
[PROOF STEP]
apply (simp only: de_Morgan_conj, erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}; infinite A\<rbrakk> \<Longrightarrow> icard (A \<times> B) = icard A * icard B
 2. \<lbrakk>A \<noteq> {}; B \<noteq> {}; infinite B\<rbrakk> \<Longrightarrow> icard (A \<times> B) = icard A * icard B
[PROOF STEP]
apply (simp_all add:
  icard_not_empty_iff[symmetric]
  cartesian_product_infiniteL_imp_infinite cartesian_product_infiniteR_imp_infinite)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma icard_cartesian_product_singleton: "icard ({x} \<times> A) = icard A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard ({x} \<times> A) = icard A
[PROOF STEP]
by (simp add: icard_cartesian_product mult_eSuc)


[STATEMENT]
lemma icard_cartesian_product_singleton_right: "icard (A \<times> {x}) = icard A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard (A \<times> {x}) = icard A
[PROOF STEP]
by (simp add: icard_cartesian_product mult_eSuc_right)


[STATEMENT]
lemma icard_atLeast: "icard {(u::nat)..} = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard {u..} = \<infinity>
[PROOF STEP]
by (simp add: infinite_atLeast)


[STATEMENT]
lemma icard_greaterThan: "icard {(u::nat)<..} = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard {u<..} = \<infinity>
[PROOF STEP]
by (simp add: infinite_greaterThan)


[STATEMENT]
lemma icard_atLeast_int: "icard {(u::int)..} = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard {u..} = \<infinity>
[PROOF STEP]
by (simp add: infinite_atLeast_int)


[STATEMENT]
lemma icard_greaterThan_int: "icard {(u::int)<..} = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard {u<..} = \<infinity>
[PROOF STEP]
by (simp add: infinite_greaterThan_int)


[STATEMENT]
lemma icard_atMost_int: "icard {..(u::int)} = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard {..u} = \<infinity>
[PROOF STEP]
by (simp add: infinite_atMost_int)


[STATEMENT]
lemma icard_lessThan_int: "icard {..<(u::int)} = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. icard {..<u} = \<infinity>
[PROOF STEP]
by (simp add: infinite_lessThan_int)


[STATEMENT]
lemma v_of_empty_sem_env[simp]: "sem_env.v empty_sem_env = nsEmpty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sem_env.v empty_sem_env = nsEmpty
[PROOF STEP]
unfolding empty_sem_env_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sem_env.v (make_sem_env nsEmpty static_cenv) = nsEmpty
[PROOF STEP]
by simp


[STATEMENT]
lemma c_of_empty_sem_env[simp]: "c empty_sem_env = static_cenv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c empty_sem_env = static_cenv
[PROOF STEP]
unfolding empty_sem_env_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c (make_sem_env nsEmpty static_cenv) = static_cenv
[PROOF STEP]
by simp


[STATEMENT]
lemma is_cupcake_all_envE:
  assumes "is_cupcake_all_env env"
  obtains v c where "env = \<lparr> sem_env.v = Bind v [], sem_env.c = c \<rparr>" "c = static_cenv" "list_all (is_cupcake_value \<circ> snd) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v c. \<lbrakk>env = make_sem_env (Bind v []) c; c = static_cenv; list_all (is_cupcake_value \<circ> snd) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_cupcake_all_env env

goal (1 subgoal):
 1. (\<And>v c. \<lbrakk>env = make_sem_env (Bind v []) c; c = static_cenv; list_all (is_cupcake_value \<circ> snd) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim!: is_cupcake_all_env.elims)


[STATEMENT]
lemma is_cupcake_nsE:
  assumes "is_cupcake_ns ns"
  obtains v where "ns = Bind v []" "list_all (is_cupcake_value \<circ> snd) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. \<lbrakk>ns = Bind v []; list_all (is_cupcake_value \<circ> snd) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_cupcake_ns ns

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>ns = Bind v []; list_all (is_cupcake_value \<circ> snd) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule is_cupcake_ns.elims)


[STATEMENT]
lemma is_cupcake_all_envD:
  assumes "is_cupcake_all_env env"
  shows "is_cupcake_ns (sem_env.v env)" "cupcake_c_ns (c env)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cupcake_ns (sem_env.v env) &&& cupcake_c_ns (c env)
[PROOF STEP]
using assms static_cenv
[PROOF STATE]
proof (prove)
using this:
is_cupcake_all_env env
cupcake_c_ns static_cenv

goal (1 subgoal):
 1. is_cupcake_ns (sem_env.v env) &&& cupcake_c_ns (c env)
[PROOF STEP]
by (auto elim!: is_cupcake_all_envE)


[STATEMENT]
lemma is_cupcake_all_envI:
  assumes "is_cupcake_ns (sem_env.v env)" "sem_env.c env = static_cenv"
  shows "is_cupcake_all_env env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cupcake_all_env env
[PROOF STEP]
using assms static_cenv
[PROOF STATE]
proof (prove)
using this:
is_cupcake_ns (sem_env.v env)
c env = static_cenv
cupcake_c_ns static_cenv

goal (1 subgoal):
 1. is_cupcake_all_env env
[PROOF STEP]
apply (cases env)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>is_cupcake_ns (sem_env.v env); c env = static_cenv; cupcake_c_ns static_cenv; env = make_sem_env x1 x2\<rbrakk> \<Longrightarrow> is_cupcake_all_env env
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>is_cupcake_ns x1; x2 = static_cenv; cupcake_c_ns static_cenv; env = make_sem_env x1 static_cenv\<rbrakk> \<Longrightarrow> is_cupcake_all_env (make_sem_env x1 static_cenv)
[PROOF STEP]
subgoal for v c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_cupcake_ns v; c = static_cenv; cupcake_c_ns static_cenv; env = make_sem_env v static_cenv\<rbrakk> \<Longrightarrow> is_cupcake_all_env (make_sem_env v static_cenv)
[PROOF STEP]
apply (cases v)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>is_cupcake_ns v; c = static_cenv; cupcake_c_ns static_cenv; env = make_sem_env v static_cenv; v = Bind x1 x2\<rbrakk> \<Longrightarrow> is_cupcake_all_env (make_sem_env v static_cenv)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>is_cupcake_ns (Bind x1 x2); c = static_cenv; cupcake_c_ns static_cenv; env = make_sem_env (Bind x1 x2) static_cenv; v = Bind x1 x2\<rbrakk> \<Longrightarrow> is_cupcake_all_env (make_sem_env (Bind x1 x2) static_cenv)
[PROOF STEP]
subgoal for x1 x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_cupcake_ns (Bind x1 x2); c = static_cenv; cupcake_c_ns static_cenv; env = make_sem_env (Bind x1 x2) static_cenv; v = Bind x1 x2\<rbrakk> \<Longrightarrow> is_cupcake_all_env (make_sem_env (Bind x1 x2) static_cenv)
[PROOF STEP]
by (cases x2) auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ex1_imp_Collect_singleton: "(\<exists>!x. P x) \<and> P x \<longleftrightarrow> Collect P = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<exists>!x. P x) \<and> P x) = (Collect P = {x})
[PROOF STEP]
proof(intro iffI conjI, unfold conj_imp_eq_imp_imp)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>Ex1 P; P x\<rbrakk> \<Longrightarrow> Collect P = {x}
 2. Collect P = {x} \<Longrightarrow> \<exists>!x. P x
 3. Collect P = {x} \<Longrightarrow> P x
[PROOF STEP]
assume "Ex1 P" "P x"
[PROOF STATE]
proof (state)
this:
Ex1 P
P x

goal (3 subgoals):
 1. \<lbrakk>Ex1 P; P x\<rbrakk> \<Longrightarrow> Collect P = {x}
 2. Collect P = {x} \<Longrightarrow> \<exists>!x. P x
 3. Collect P = {x} \<Longrightarrow> P x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ex1 P
P x
[PROOF STEP]
show "Collect P = {x}"
[PROOF STATE]
proof (prove)
using this:
Ex1 P
P x

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

goal (2 subgoals):
 1. Collect P = {x} \<Longrightarrow> \<exists>!x. P x
 2. Collect P = {x} \<Longrightarrow> P x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Collect P = {x} \<Longrightarrow> \<exists>!x. P x
 2. Collect P = {x} \<Longrightarrow> P x
[PROOF STEP]
assume Px: "Collect P = {x}"
[PROOF STATE]
proof (state)
this:
Collect P = {x}

goal (2 subgoals):
 1. Collect P = {x} \<Longrightarrow> \<exists>!x. P x
 2. Collect P = {x} \<Longrightarrow> P x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Collect P = {x}
[PROOF STEP]
have "P y \<longleftrightarrow> x = y" for y
[PROOF STATE]
proof (prove)
using this:
Collect P = {x}

goal (1 subgoal):
 1. P y = (x = y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P ?y = (x = ?y)

goal (2 subgoals):
 1. Collect P = {x} \<Longrightarrow> \<exists>!x. P x
 2. Collect P = {x} \<Longrightarrow> P x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P ?y = (x = ?y)
[PROOF STEP]
show "Ex1 P"
[PROOF STATE]
proof (prove)
using this:
P ?y = (x = ?y)

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

goal (1 subgoal):
 1. Collect P = {x} \<Longrightarrow> P x
[PROOF STEP]
from Px
[PROOF STATE]
proof (chain)
picking this:
Collect P = {x}
[PROOF STEP]
show "P x"
[PROOF STATE]
proof (prove)
using this:
Collect P = {x}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex1_Collect_singleton[consumes 2]:
  assumes "\<exists>!x. P x" and "P x" and "Collect P = {x} \<Longrightarrow> thesis" shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule assms(3), subst ex1_imp_Collect_singleton[symmetric], insert assms(1,2), auto)


[STATEMENT]
lemma ex1_iff_Collect_singleton: "P x \<Longrightarrow> (\<exists>!x. P x) \<longleftrightarrow> Collect P = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x \<Longrightarrow> (\<exists>!x. P x) = (Collect P = {x})
[PROOF STEP]
by (subst ex1_imp_Collect_singleton[symmetric], auto)


[STATEMENT]
lemma bij_imp_ex1_iff: "(\<exists>!x. P (f x)) \<longleftrightarrow> (\<exists>!y. P y)" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>!x. P (f x)) = (\<exists>!y. P y)
[PROOF STEP]
proof (intro iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>!x. P (f x) \<Longrightarrow> \<exists>!y. P y
 2. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
assume l: ?l
[PROOF STATE]
proof (state)
this:
\<exists>!x. P (f x)

goal (2 subgoals):
 1. \<exists>!x. P (f x) \<Longrightarrow> \<exists>!y. P y
 2. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>!x. P (f x)
[PROOF STEP]
obtain x where "P (f x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. P (f x)

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

goal (2 subgoals):
 1. \<exists>!x. P (f x) \<Longrightarrow> \<exists>!y. P y
 2. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
with l
[PROOF STATE]
proof (chain)
picking this:
\<exists>!x. P (f x)
P (f x)
[PROOF STEP]
have *: "{x} = Collect (P o f)"
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. P (f x)
P (f x)

goal (1 subgoal):
 1. {x} = Collect (P \<circ> f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x} = Collect (P \<circ> f)

goal (2 subgoals):
 1. \<exists>!x. P (f x) \<Longrightarrow> \<exists>!y. P y
 2. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{x} = Collect (P \<circ> f)

goal (2 subgoals):
 1. \<exists>!x. P (f x) \<Longrightarrow> \<exists>!y. P y
 2. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
have "f ` \<dots> = {y. P (f (Hilbert_Choice.inv f y))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` Collect (P \<circ> f) = {y. P (f (inv f y))}
[PROOF STEP]
using bij_image_Collect_eq[OF bij]
[PROOF STATE]
proof (prove)
using this:
f ` Collect ?P = {y. ?P (inv f y)}

goal (1 subgoal):
 1. f ` Collect (P \<circ> f) = {y. P (f (inv f y))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` Collect (P \<circ> f) = {y. P (f (inv f y))}

goal (2 subgoals):
 1. \<exists>!x. P (f x) \<Longrightarrow> \<exists>!y. P y
 2. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f ` Collect (P \<circ> f) = {y. P (f (inv f y))}

goal (2 subgoals):
 1. \<exists>!x. P (f x) \<Longrightarrow> \<exists>!y. P y
 2. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
have "\<dots> = {y. P y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. P (f (inv f y))} = {y. P y}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {y. P (f (inv f y))} = {y. P y}
[PROOF STEP]
have "f (Hilbert_Choice.inv f y) = y" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (inv f y) = y
[PROOF STEP]
by (meson bij bij_inv_eq_iff)
[PROOF STATE]
proof (state)
this:
f (inv f ?y) = ?y

goal (1 subgoal):
 1. {y. P (f (inv f y))} = {y. P y}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (inv f ?y) = ?y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f (inv f ?y) = ?y

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{y. P (f (inv f y))} = {y. P y}

goal (2 subgoals):
 1. \<exists>!x. P (f x) \<Longrightarrow> \<exists>!y. P y
 2. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f ` {x} = {y. P y}
[PROOF STEP]
have "Collect P = {f x}"
[PROOF STATE]
proof (prove)
using this:
f ` {x} = {y. P y}

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

goal (2 subgoals):
 1. \<exists>!x. P (f x) \<Longrightarrow> \<exists>!y. P y
 2. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Collect P = {f x}
[PROOF STEP]
show ?r
[PROOF STATE]
proof (prove)
using this:
Collect P = {f x}

goal (1 subgoal):
 1. \<exists>!y. P y
[PROOF STEP]
by (fold ex1_imp_Collect_singleton, auto)
[PROOF STATE]
proof (state)
this:
\<exists>!y. P y

goal (1 subgoal):
 1. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
assume r: ?r
[PROOF STATE]
proof (state)
this:
\<exists>!y. P y

goal (1 subgoal):
 1. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>!y. P y
[PROOF STEP]
obtain y where "P y"
[PROOF STATE]
proof (prove)
using this:
\<exists>!y. P y

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

goal (1 subgoal):
 1. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
with r
[PROOF STATE]
proof (chain)
picking this:
\<exists>!y. P y
P y
[PROOF STEP]
have "{y} = Collect P"
[PROOF STATE]
proof (prove)
using this:
\<exists>!y. P y
P y

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

goal (1 subgoal):
 1. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{y} = Collect P

goal (1 subgoal):
 1. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
have "Hilbert_Choice.inv f ` \<dots> = Collect (P \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv f ` Collect P = Collect (P \<circ> f)
[PROOF STEP]
using bij_image_Collect_eq[OF bij_imp_bij_inv[OF bij]] bij
[PROOF STATE]
proof (prove)
using this:
inv f ` Collect ?P = {y. ?P (inv (inv f) y)}
bij f

goal (1 subgoal):
 1. inv f ` Collect P = Collect (P \<circ> f)
[PROOF STEP]
by (auto simp: inv_inv_eq)
[PROOF STATE]
proof (state)
this:
inv f ` Collect P = Collect (P \<circ> f)

goal (1 subgoal):
 1. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
inv f ` {y} = {a. (P \<circ> f) a}
[PROOF STEP]
have "Collect (P o f) = {Hilbert_Choice.inv f y}"
[PROOF STATE]
proof (prove)
using this:
inv f ` {y} = {a. (P \<circ> f) a}

goal (1 subgoal):
 1. Collect (P \<circ> f) = {inv f y}
[PROOF STEP]
by (simp add: o_def)
[PROOF STATE]
proof (state)
this:
Collect (P \<circ> f) = {inv f y}

goal (1 subgoal):
 1. \<exists>!y. P y \<Longrightarrow> \<exists>!x. P (f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Collect (P \<circ> f) = {inv f y}
[PROOF STEP]
show ?l
[PROOF STATE]
proof (prove)
using this:
Collect (P \<circ> f) = {inv f y}

goal (1 subgoal):
 1. \<exists>!x. P (f x)
[PROOF STEP]
by (fold ex1_imp_Collect_singleton, auto)
[PROOF STATE]
proof (state)
this:
\<exists>!x. P (f x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_ex1_imp_the_shift:
  assumes ex1: "\<exists>!y. P y" shows "(THE x. P (f x)) = Hilbert_Choice.inv f (THE y. P y)" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE x. P (f x)) = inv f (THE y. P y)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (THE x. P (f x)) = inv f (THE y. P y)
[PROOF STEP]
from ex1
[PROOF STATE]
proof (chain)
picking this:
\<exists>!y. P y
[PROOF STEP]
have "P (THE y. P y)"
[PROOF STATE]
proof (prove)
using this:
\<exists>!y. P y

goal (1 subgoal):
 1. P (THE y. P y)
[PROOF STEP]
by (rule the1I2)
[PROOF STATE]
proof (state)
this:
P (THE y. P y)

goal (1 subgoal):
 1. (THE x. P (f x)) = inv f (THE y. P y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P (THE y. P y)

goal (1 subgoal):
 1. (THE x. P (f x)) = inv f (THE y. P y)
[PROOF STEP]
from ex1[folded bij_imp_ex1_iff]
[PROOF STATE]
proof (chain)
picking this:
\<exists>!x. P (f x)
[PROOF STEP]
have "P (f (THE x. P (f x)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. P (f x)

goal (1 subgoal):
 1. P (f (THE x. P (f x)))
[PROOF STEP]
by (rule the1I2)
[PROOF STATE]
proof (state)
this:
P (f (THE x. P (f x)))

goal (1 subgoal):
 1. (THE x. P (f x)) = inv f (THE y. P y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P (THE y. P y)
P (f (THE x. P (f x)))
[PROOF STEP]
have "(THE y. P y) = f (THE x. P (f x))"
[PROOF STATE]
proof (prove)
using this:
P (THE y. P y)
P (f (THE x. P (f x)))

goal (1 subgoal):
 1. (THE y. P y) = f (THE x. P (f x))
[PROOF STEP]
using ex1
[PROOF STATE]
proof (prove)
using this:
P (THE y. P y)
P (f (THE x. P (f x)))
\<exists>!y. P y

goal (1 subgoal):
 1. (THE y. P y) = f (THE x. P (f x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE y. P y) = f (THE x. P (f x))

goal (1 subgoal):
 1. (THE x. P (f x)) = inv f (THE y. P y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(THE y. P y) = f (THE x. P (f x))

goal (1 subgoal):
 1. (THE x. P (f x)) = inv f (THE y. P y)
[PROOF STEP]
have "Hilbert_Choice.inv f \<dots> = (THE x. P (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv f (f (THE x. P (f x))) = (THE x. P (f x))
[PROOF STEP]
using bij
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. inv f (f (THE x. P (f x))) = (THE x. P (f x))
[PROOF STEP]
by (simp add: bij_is_inj)
[PROOF STATE]
proof (state)
this:
inv f (f (THE x. P (f x))) = (THE x. P (f x))

goal (1 subgoal):
 1. (THE x. P (f x)) = inv f (THE y. P y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
inv f (THE y. P y) = (THE x. P (f x))
[PROOF STEP]
show "?l = ?r"
[PROOF STATE]
proof (prove)
using this:
inv f (THE y. P y) = (THE x. P (f x))

goal (1 subgoal):
 1. (THE x. P (f x)) = inv f (THE y. P y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE x. P (f x)) = inv f (THE y. P y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_imp_Collect_image: "{x. P (f x)} = Hilbert_Choice.inv f ` {y. P y}" (is "?l = ?g ` _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. P (f x)} = inv f ` {y. P y}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {x. P (f x)} = inv f ` {y. P y}
[PROOF STEP]
have "?l = ?g ` f ` ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. P (f x)} = inv f ` f ` {x. P (f x)}
[PROOF STEP]
by (simp add: image_comp inv_o_cancel[OF bij_is_inj[OF bij]])
[PROOF STATE]
proof (state)
this:
{x. P (f x)} = inv f ` f ` {x. P (f x)}

goal (1 subgoal):
 1. {x. P (f x)} = inv f ` {y. P y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{x. P (f x)} = inv f ` f ` {x. P (f x)}

goal (1 subgoal):
 1. {x. P (f x)} = inv f ` {y. P y}
[PROOF STEP]
have "f ` ?l = {f x | x. P (f x)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {x. P (f x)} = {f x |x. P (f x)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` {x. P (f x)} = {f x |x. P (f x)}

goal (1 subgoal):
 1. {x. P (f x)} = inv f ` {y. P y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f ` {x. P (f x)} = {f x |x. P (f x)}

goal (1 subgoal):
 1. {x. P (f x)} = inv f ` {y. P y}
[PROOF STEP]
have "\<dots> = {y. P y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f x |x. P (f x)} = {y. P y}
[PROOF STEP]
by (metis bij bij_iff)
[PROOF STATE]
proof (state)
this:
{f x |x. P (f x)} = {y. P y}

goal (1 subgoal):
 1. {x. P (f x)} = inv f ` {y. P y}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{x. P (f x)} = inv f ` {y. P y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{x. P (f x)} = inv f ` {y. P y}

goal (1 subgoal):
 1. {x. P (f x)} = inv f ` {y. P y}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
{x. P (f x)} = inv f ` {y. P y}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_imp_card_image: "card (f ` X) = card X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (f ` X) = card X
[PROOF STEP]
by (metis bij bij_iff card.infinite finite_imageD inj_onI inj_on_iff_eq_card)


[STATEMENT]
lemma poly_condI[intro]:
  assumes "lead_coeff p > 0" and "irreducible p" shows "poly_cond p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_cond p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < lead_coeff p
irreducible p

goal (1 subgoal):
 1. poly_cond p
[PROOF STEP]
by (auto simp: poly_cond_def)


[STATEMENT]
lemma poly_condD:
  assumes "poly_cond p"
  shows "irreducible p" and "lead_coeff p > 0" and "root_free p" and "square_free p" and "p \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (irreducible p &&& 0 < lead_coeff p) &&& root_free p &&& square_free p &&& p \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
poly_cond p

goal (1 subgoal):
 1. (irreducible p &&& 0 < lead_coeff p) &&& root_free p &&& square_free p &&& p \<noteq> 0
[PROOF STEP]
unfolding poly_cond_def
[PROOF STATE]
proof (prove)
using this:
0 < lead_coeff p \<and> irreducible p

goal (1 subgoal):
 1. (irreducible p &&& 0 < lead_coeff p) &&& root_free p &&& square_free p &&& p \<noteq> 0
[PROOF STEP]
using irreducible_root_free irreducible_imp_square_free cf_pos_def
[PROOF STATE]
proof (prove)
using this:
0 < lead_coeff p \<and> irreducible p
irreducible ?p \<Longrightarrow> root_free ?p
irreducible ?p \<Longrightarrow> square_free ?p
cf_pos ?p = (content ?p = 1 \<and> 0 < lead_coeff ?p)

goal (1 subgoal):
 1. (irreducible p &&& 0 < lead_coeff p) &&& root_free p &&& square_free p &&& p \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma poly_condE[elim]:
  assumes "poly_cond p"
      and "irreducible p \<Longrightarrow> lead_coeff p > 0 \<Longrightarrow> root_free p \<Longrightarrow> square_free p \<Longrightarrow> p \<noteq> 0 \<Longrightarrow> thesis"
  shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
poly_cond p
\<lbrakk>irreducible p; 0 < lead_coeff p; root_free p; square_free p; p \<noteq> 0\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto dest:poly_condD)


[STATEMENT]
lemma poly_cond_abs_int_poly[simp]: "irreducible p \<Longrightarrow> poly_cond (abs_int_poly p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreducible p \<Longrightarrow> poly_cond (abs_int_poly p)
[PROOF STEP]
unfolding poly_cond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreducible p \<Longrightarrow> 0 < lead_coeff (abs_int_poly p) \<and> irreducible (abs_int_poly p)
[PROOF STEP]
by (cases "p = 0", auto)


[STATEMENT]
lemma irreducible_poly_uminus[simp]: "irreducible p \<Longrightarrow> irreducible (poly_uminus (p :: int poly))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreducible p \<Longrightarrow> irreducible (poly_uminus p)
[PROOF STEP]
proof (cases "degree p = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>irreducible p; degree p = 0\<rbrakk> \<Longrightarrow> irreducible (poly_uminus p)
 2. \<lbrakk>irreducible p; degree p \<noteq> 0\<rbrakk> \<Longrightarrow> irreducible (poly_uminus p)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
degree p = 0

goal (2 subgoals):
 1. \<lbrakk>irreducible p; degree p = 0\<rbrakk> \<Longrightarrow> irreducible (poly_uminus p)
 2. \<lbrakk>irreducible p; degree p \<noteq> 0\<rbrakk> \<Longrightarrow> irreducible (poly_uminus p)
[PROOF STEP]
from degree0_coeffs[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. p = [:a:]
[PROOF STEP]
obtain a where p: "p = [:a:]"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. p = [:a:]

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

goal (2 subgoals):
 1. \<lbrakk>irreducible p; degree p = 0\<rbrakk> \<Longrightarrow> irreducible (poly_uminus p)
 2. \<lbrakk>irreducible p; degree p \<noteq> 0\<rbrakk> \<Longrightarrow> irreducible (poly_uminus p)
[PROOF STEP]
have "poly_uminus p = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_uminus p = p
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_uminus [:a:] = [:a:]
[PROOF STEP]
by (cases "a = 0", auto)
[PROOF STATE]
proof (state)
this:
poly_uminus p = p

goal (2 subgoals):
 1. \<lbrakk>irreducible p; degree p = 0\<rbrakk> \<Longrightarrow> irreducible (poly_uminus p)
 2. \<lbrakk>irreducible p; degree p \<noteq> 0\<rbrakk> \<Longrightarrow> irreducible (poly_uminus p)
[PROOF STEP]
thus "irreducible p \<Longrightarrow> irreducible (poly_uminus p)"
[PROOF STATE]
proof (prove)
using this:
poly_uminus p = p

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

goal (1 subgoal):
 1. \<lbrakk>irreducible p; degree p \<noteq> 0\<rbrakk> \<Longrightarrow> irreducible (poly_uminus p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>irreducible p; degree p \<noteq> 0\<rbrakk> \<Longrightarrow> irreducible (poly_uminus p)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
degree p \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>irreducible p; degree p \<noteq> 0\<rbrakk> \<Longrightarrow> irreducible (poly_uminus p)
[PROOF STEP]
from poly_uminus_irreducible[OF _ this]
[PROOF STATE]
proof (chain)
picking this:
irreducible p \<Longrightarrow> irreducible (poly_uminus p)
[PROOF STEP]
show "irreducible p \<Longrightarrow> irreducible (poly_uminus p)"
[PROOF STATE]
proof (prove)
using this:
irreducible p \<Longrightarrow> irreducible (poly_uminus p)

goal (1 subgoal):
 1. irreducible p \<Longrightarrow> irreducible (poly_uminus p)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
irreducible p \<Longrightarrow> irreducible (poly_uminus p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma irreducible_poly_uminus_abs[simp]: "irreducible p \<Longrightarrow> irreducible (poly_uminus_abs p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreducible p \<Longrightarrow> irreducible (poly_uminus_abs p)
[PROOF STEP]
unfolding poly_uminus_abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreducible p \<Longrightarrow> irreducible (abs_int_poly (poly_uminus p))
[PROOF STEP]
using irreducible_poly_uminus[of p]
[PROOF STATE]
proof (prove)
using this:
irreducible p \<Longrightarrow> irreducible (poly_uminus p)

goal (1 subgoal):
 1. irreducible p \<Longrightarrow> irreducible (abs_int_poly (poly_uminus p))
[PROOF STEP]
by auto


[STATEMENT]
lemma poly_cond_poly_uminus_abs[simp]: "poly_cond p \<Longrightarrow> poly_cond (poly_uminus_abs p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_cond p \<Longrightarrow> poly_cond (poly_uminus_abs p)
[PROOF STEP]
by (auto simp: poly_cond_def, unfold poly_uminus_abs_def, subst pos_poly_abs_poly, auto)


[STATEMENT]
lemma ipoly_poly_uminus_abs_zero[simp]: "ipoly (poly_uminus_abs p) (x :: 'a :: idom) = 0 \<longleftrightarrow> ipoly p (-x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ipoly (poly_uminus_abs p) x = (0::'a)) = (ipoly p (- x) = (0::'a))
[PROOF STEP]
unfolding poly_uminus_abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ipoly (abs_int_poly (poly_uminus p)) x = (0::'a)) = (ipoly p (- x) = (0::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma degree_poly_uminus_abs[simp]: "degree (poly_uminus_abs p) = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (poly_uminus_abs p) = degree p
[PROOF STEP]
unfolding poly_uminus_abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (abs_int_poly (poly_uminus p)) = degree p
[PROOF STEP]
by auto


[STATEMENT]
lemma irreducible_poly_inverse[simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> irreducible p \<Longrightarrow> irreducible (poly_inverse p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>coeff p 0 \<noteq> 0; irreducible p\<rbrakk> \<Longrightarrow> irreducible (poly_inverse p)
[PROOF STEP]
unfolding poly_inverse_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>coeff p 0 \<noteq> 0; irreducible p\<rbrakk> \<Longrightarrow> irreducible (abs_int_poly (reflect_poly p))
[PROOF STEP]
by (auto simp: irreducible_reflect_poly)


[STATEMENT]
lemma degree_poly_inverse[simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> degree (poly_inverse p) = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff p 0 \<noteq> 0 \<Longrightarrow> degree (poly_inverse p) = degree p
[PROOF STEP]
unfolding poly_inverse_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff p 0 \<noteq> 0 \<Longrightarrow> degree (abs_int_poly (reflect_poly p)) = degree p
[PROOF STEP]
by auto


[STATEMENT]
lemma ipoly_poly_inverse[simp]: assumes "coeff p 0 \<noteq> 0"
  shows "ipoly (poly_inverse p) (x :: 'a :: field_char_0) = 0 \<longleftrightarrow> ipoly p (inverse x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ipoly (poly_inverse p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))
[PROOF STEP]
unfolding poly_inverse_def ipoly_abs_int_poly_eq_zero_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = (0::'a) \<Longrightarrow> (ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))
 2. x \<noteq> (0::'a) \<Longrightarrow> (ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> (0::'a)

goal (2 subgoals):
 1. x = (0::'a) \<Longrightarrow> (ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))
 2. x \<noteq> (0::'a) \<Longrightarrow> (ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))
[PROOF STEP]
thus "(ipoly (reflect_poly p) x = 0) = (ipoly p (inverse x) = 0)"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'a)

goal (1 subgoal):
 1. (ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))
[PROOF STEP]
by (subst ipoly_reflect_poly, auto)
[PROOF STATE]
proof (state)
this:
(ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))

goal (1 subgoal):
 1. x = (0::'a) \<Longrightarrow> (ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = (0::'a) \<Longrightarrow> (ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = (0::'a)

goal (1 subgoal):
 1. x = (0::'a) \<Longrightarrow> (ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))
[PROOF STEP]
show "(ipoly (reflect_poly p) x = 0) = (ipoly p (inverse x) = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))
[PROOF STEP]
unfolding True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ipoly (reflect_poly p) (0::'a) = (0::'a)) = (ipoly p (inverse (0::'a)) = (0::'a))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
coeff p 0 \<noteq> 0

goal (1 subgoal):
 1. (ipoly (reflect_poly p) (0::'a) = (0::'a)) = (ipoly p (inverse (0::'a)) = (0::'a))
[PROOF STEP]
by (auto simp: poly_0_coeff_0)
[PROOF STATE]
proof (state)
this:
(ipoly (reflect_poly p) x = (0::'a)) = (ipoly p (inverse x) = (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipoly_roots_finite: "p \<noteq> 0 \<Longrightarrow> finite {x :: 'a :: {idom, ring_char_0}. ipoly p x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> finite {x. ipoly p x = (0::'a)}
[PROOF STEP]
by (rule poly_roots_finite, simp)