[STATEMENT]
lemma R31_c_ge_one_half: "pmf (sds R31) c \<ge> 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
from R25.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R25) b = 0 \<or> pmf (sds R25) c = 0
[PROOF STEP]
have "pmf (sds R25) a \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R25) b = 0 \<or> pmf (sds R25) c = 0

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R25) a
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pmf (sds R25) b = 0 \<Longrightarrow> 1 / 2 \<le> pmf (sds R25) a
 2. pmf (sds R25) c = 0 \<Longrightarrow> 1 / 2 \<le> pmf (sds R25) a
[PROOF STEP]
assume "pmf (sds R25) c = 0"
[PROOF STATE]
proof (state)
this:
pmf (sds R25) c = 0

goal (2 subgoals):
 1. pmf (sds R25) b = 0 \<Longrightarrow> 1 / 2 \<le> pmf (sds R25) a
 2. pmf (sds R25) c = 0 \<Longrightarrow> 1 / 2 \<le> pmf (sds R25) a
[PROOF STEP]
with R25_R36.strategyproofness(1) lottery_conditions[OF R36.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R36) a < pmf (sds R25) a \<or> pmf (sds R36) a + pmf (sds R36) c < pmf (sds R25) a + pmf (sds R25) c) \<or> pmf (sds R36) a = pmf (sds R25) a \<and> pmf (sds R36) a + pmf (sds R36) c = pmf (sds R25) a + pmf (sds R25) c
0 \<le> pmf (sds R36) a
0 \<le> pmf (sds R36) b
0 \<le> pmf (sds R36) c
0 \<le> pmf (sds R36) d
pmf (sds R36) a + pmf (sds R36) b + pmf (sds R36) c + pmf (sds R36) d = 1
pmf (sds R25) c = 0
[PROOF STEP]
show "pmf (sds R25) a \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R36) a < pmf (sds R25) a \<or> pmf (sds R36) a + pmf (sds R36) c < pmf (sds R25) a + pmf (sds R25) c) \<or> pmf (sds R36) a = pmf (sds R25) a \<and> pmf (sds R36) a + pmf (sds R36) c = pmf (sds R25) a + pmf (sds R25) c
0 \<le> pmf (sds R36) a
0 \<le> pmf (sds R36) b
0 \<le> pmf (sds R36) c
0 \<le> pmf (sds R36) d
pmf (sds R36) a + pmf (sds R36) b + pmf (sds R36) c + pmf (sds R36) d = 1
pmf (sds R25) c = 0

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R25) a
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R25) a

goal (1 subgoal):
 1. pmf (sds R25) b = 0 \<Longrightarrow> 1 / 2 \<le> pmf (sds R25) a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (sds R25) b = 0 \<Longrightarrow> 1 / 2 \<le> pmf (sds R25) a
[PROOF STEP]
assume [simp]: "pmf (sds R25) b = 0"
[PROOF STATE]
proof (state)
this:
pmf (sds R25) b = 0

goal (1 subgoal):
 1. pmf (sds R25) b = 0 \<Longrightarrow> 1 / 2 \<le> pmf (sds R25) a
[PROOF STEP]
from R36_R25.strategyproofness(1) lottery_conditions[OF R25.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R25) c + pmf (sds R25) a < pmf (sds R36) c + pmf (sds R36) a \<or> pmf (sds R25) c + (pmf (sds R25) a + pmf (sds R25) d) < pmf (sds R36) c + (pmf (sds R36) a + pmf (sds R36) d)) \<or> pmf (sds R25) c + pmf (sds R25) a = pmf (sds R36) c + pmf (sds R36) a \<and> pmf (sds R25) c + (pmf (sds R25) a + pmf (sds R25) d) = pmf (sds R36) c + (pmf (sds R36) a + pmf (sds R36) d)
0 \<le> pmf (sds R25) a
0 \<le> pmf (sds R25) b
0 \<le> pmf (sds R25) c
0 \<le> pmf (sds R25) d
pmf (sds R25) a + pmf (sds R25) b + pmf (sds R25) c + pmf (sds R25) d = 1
[PROOF STEP]
have "pmf (sds R25) c + pmf (sds R25) a \<le> pmf (sds R36) c + 1 / 2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R25) c + pmf (sds R25) a < pmf (sds R36) c + pmf (sds R36) a \<or> pmf (sds R25) c + (pmf (sds R25) a + pmf (sds R25) d) < pmf (sds R36) c + (pmf (sds R36) a + pmf (sds R36) d)) \<or> pmf (sds R25) c + pmf (sds R25) a = pmf (sds R36) c + pmf (sds R36) a \<and> pmf (sds R25) c + (pmf (sds R25) a + pmf (sds R25) d) = pmf (sds R36) c + (pmf (sds R36) a + pmf (sds R36) d)
0 \<le> pmf (sds R25) a
0 \<le> pmf (sds R25) b
0 \<le> pmf (sds R25) c
0 \<le> pmf (sds R25) d
pmf (sds R25) a + pmf (sds R25) b + pmf (sds R25) c + pmf (sds R25) d = 1

goal (1 subgoal):
 1. pmf (sds R25) c + pmf (sds R25) a \<le> pmf (sds R36) c + 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R25) c + pmf (sds R25) a \<le> pmf (sds R36) c + 1 / 2

goal (1 subgoal):
 1. pmf (sds R25) b = 0 \<Longrightarrow> 1 / 2 \<le> pmf (sds R25) a
[PROOF STEP]
with R25_R36.strategyproofness(1)
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R36) a < pmf (sds R25) a \<or> pmf (sds R36) a + pmf (sds R36) c < pmf (sds R25) a + pmf (sds R25) c) \<or> pmf (sds R36) a = pmf (sds R25) a \<and> pmf (sds R36) a + pmf (sds R36) c = pmf (sds R25) a + pmf (sds R25) c
pmf (sds R25) c + pmf (sds R25) a \<le> pmf (sds R36) c + 1 / 2
[PROOF STEP]
show "pmf (sds R25) a \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R36) a < pmf (sds R25) a \<or> pmf (sds R36) a + pmf (sds R36) c < pmf (sds R25) a + pmf (sds R25) c) \<or> pmf (sds R36) a = pmf (sds R25) a \<and> pmf (sds R36) a + pmf (sds R36) c = pmf (sds R25) a + pmf (sds R25) c
pmf (sds R25) c + pmf (sds R25) a \<le> pmf (sds R36) c + 1 / 2

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R25) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R25) a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R25) a

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
hence "pmf (sds R26) a \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> pmf (sds R25) a

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R26) a
[PROOF STEP]
using R25_R26.strategyproofness(1) lottery_conditions[OF R25.wf]
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> pmf (sds R25) a
(pmf (sds R26) d + pmf (sds R26) c < pmf (sds R25) d + pmf (sds R25) b \<or> pmf (sds R26) d + (pmf (sds R26) c + pmf (sds R26) a) < pmf (sds R25) d + (pmf (sds R25) b + pmf (sds R25) a)) \<or> pmf (sds R26) d + pmf (sds R26) c = pmf (sds R25) d + pmf (sds R25) b \<and> pmf (sds R26) d + (pmf (sds R26) c + pmf (sds R26) a) = pmf (sds R25) d + (pmf (sds R25) b + pmf (sds R25) a)
0 \<le> pmf (sds R25) a
0 \<le> pmf (sds R25) b
0 \<le> pmf (sds R25) c
0 \<le> pmf (sds R25) d
pmf (sds R25) a + pmf (sds R25) b + pmf (sds R25) c + pmf (sds R25) d = 1

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R26) a
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R26) a

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
with lottery_conditions[OF R47.wf]
[PROOF STATE]
proof (chain)
picking this:
0 \<le> pmf (sds R47) a
0 \<le> pmf (sds R47) b
0 \<le> pmf (sds R47) c
0 \<le> pmf (sds R47) d
pmf (sds R47) a + pmf (sds R47) b + pmf (sds R47) c + pmf (sds R47) d = 1
1 / 2 \<le> pmf (sds R26) a
[PROOF STEP]
have "1/2 \<le> pmf (sds R26) a + pmf (sds R47) d"
[PROOF STATE]
proof (prove)
using this:
0 \<le> pmf (sds R47) a
0 \<le> pmf (sds R47) b
0 \<le> pmf (sds R47) c
0 \<le> pmf (sds R47) d
pmf (sds R47) a + pmf (sds R47) b + pmf (sds R47) c + pmf (sds R47) d = 1
1 / 2 \<le> pmf (sds R26) a

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R26) a + pmf (sds R47) d
[PROOF STEP]
by (simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R26) a + pmf (sds R47) d

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R26) a + pmf (sds R47) d

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
have "\<dots> = 1 - pmf (sds R8) a + pmf (sds R47) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R26) a + pmf (sds R47) d = 1 - pmf (sds R8) a + pmf (sds R47) d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (sds R26) a + pmf (sds R47) d = 1 - pmf (sds R8) a + pmf (sds R47) d

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (sds R26) a + pmf (sds R47) d = 1 - pmf (sds R8) a + pmf (sds R47) d

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
from R4_R8.strategyproofness(1)
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R8) c < pmf (sds R4) d \<or> pmf (sds R8) c + pmf (sds R8) d < pmf (sds R4) d + pmf (sds R4) c) \<or> pmf (sds R8) c = pmf (sds R4) d \<and> pmf (sds R8) c + pmf (sds R8) d = pmf (sds R4) d + pmf (sds R4) c
[PROOF STEP]
have "1 - pmf (sds R8) a \<le> pmf (sds R21) d"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R8) c < pmf (sds R4) d \<or> pmf (sds R8) c + pmf (sds R8) d < pmf (sds R4) d + pmf (sds R4) c) \<or> pmf (sds R8) c = pmf (sds R4) d \<and> pmf (sds R8) c + pmf (sds R8) d = pmf (sds R4) d + pmf (sds R4) c

goal (1 subgoal):
 1. 1 - pmf (sds R8) a \<le> pmf (sds R21) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 - pmf (sds R8) a \<le> pmf (sds R21) d

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 - pmf (sds R8) a \<le> pmf (sds R21) d

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
note R21_R47
[PROOF STATE]
proof (state)
this:
pmf (sds R21) d \<le> pmf (sds R47) c

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (sds R21) d \<le> pmf (sds R47) c

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
from R30_R41.strategyproofness(1) R41.support
            lottery_conditions[OF R41.wf] lottery_conditions[OF R47.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R41) c < pmf (sds R30) c \<or> pmf (sds R41) c + (pmf (sds R41) b + pmf (sds R41) a) < pmf (sds R30) c + (pmf (sds R30) b + pmf (sds R30) a)) \<or> pmf (sds R41) c = pmf (sds R30) c \<and> pmf (sds R41) c + (pmf (sds R41) b + pmf (sds R41) a) = pmf (sds R30) c + (pmf (sds R30) b + pmf (sds R30) a)
pmf (sds R41) b = 0
0 \<le> pmf (sds R41) a
0 \<le> pmf (sds R41) b
0 \<le> pmf (sds R41) c
0 \<le> pmf (sds R41) d
pmf (sds R41) a + pmf (sds R41) b + pmf (sds R41) c + pmf (sds R41) d = 1
0 \<le> pmf (sds R47) a
0 \<le> pmf (sds R47) b
0 \<le> pmf (sds R47) c
0 \<le> pmf (sds R47) d
pmf (sds R47) a + pmf (sds R47) b + pmf (sds R47) c + pmf (sds R47) d = 1
[PROOF STEP]
have "pmf (sds R47) c + pmf (sds R47) d \<le> pmf (sds R41) d"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R41) c < pmf (sds R30) c \<or> pmf (sds R41) c + (pmf (sds R41) b + pmf (sds R41) a) < pmf (sds R30) c + (pmf (sds R30) b + pmf (sds R30) a)) \<or> pmf (sds R41) c = pmf (sds R30) c \<and> pmf (sds R41) c + (pmf (sds R41) b + pmf (sds R41) a) = pmf (sds R30) c + (pmf (sds R30) b + pmf (sds R30) a)
pmf (sds R41) b = 0
0 \<le> pmf (sds R41) a
0 \<le> pmf (sds R41) b
0 \<le> pmf (sds R41) c
0 \<le> pmf (sds R41) d
pmf (sds R41) a + pmf (sds R41) b + pmf (sds R41) c + pmf (sds R41) d = 1
0 \<le> pmf (sds R47) a
0 \<le> pmf (sds R47) b
0 \<le> pmf (sds R47) c
0 \<le> pmf (sds R47) d
pmf (sds R47) a + pmf (sds R47) b + pmf (sds R47) c + pmf (sds R47) d = 1

goal (1 subgoal):
 1. pmf (sds R47) c + pmf (sds R47) d \<le> pmf (sds R41) d
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
pmf (sds R47) c + pmf (sds R47) d \<le> pmf (sds R41) d

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (sds R47) c + pmf (sds R47) d \<le> pmf (sds R41) d

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
from R41_R31.strategyproofness(1) R41.support lottery_conditions[OF R31.wf]
       lottery_conditions[OF R41.wf]
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R31) d + (pmf (sds R31) b + pmf (sds R31) a) \<le> pmf (sds R41) c + (pmf (sds R41) b + pmf (sds R41) a)
pmf (sds R41) b = 0
0 \<le> pmf (sds R31) a
0 \<le> pmf (sds R31) b
0 \<le> pmf (sds R31) c
0 \<le> pmf (sds R31) d
pmf (sds R31) a + pmf (sds R31) b + pmf (sds R31) c + pmf (sds R31) d = 1
0 \<le> pmf (sds R41) a
0 \<le> pmf (sds R41) b
0 \<le> pmf (sds R41) c
0 \<le> pmf (sds R41) d
pmf (sds R41) a + pmf (sds R41) b + pmf (sds R41) c + pmf (sds R41) d = 1
[PROOF STEP]
have "pmf (sds R41) d \<le> pmf (sds R31) c"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R31) d + (pmf (sds R31) b + pmf (sds R31) a) \<le> pmf (sds R41) c + (pmf (sds R41) b + pmf (sds R41) a)
pmf (sds R41) b = 0
0 \<le> pmf (sds R31) a
0 \<le> pmf (sds R31) b
0 \<le> pmf (sds R31) c
0 \<le> pmf (sds R31) d
pmf (sds R31) a + pmf (sds R31) b + pmf (sds R31) c + pmf (sds R31) d = 1
0 \<le> pmf (sds R41) a
0 \<le> pmf (sds R41) b
0 \<le> pmf (sds R41) c
0 \<le> pmf (sds R41) d
pmf (sds R41) a + pmf (sds R41) b + pmf (sds R41) c + pmf (sds R41) d = 1

goal (1 subgoal):
 1. pmf (sds R41) d \<le> pmf (sds R31) c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R41) d \<le> pmf (sds R31) c

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + pmf (sds R47) d \<le> y + pmf (sds R47) d; \<And>x y. x \<le> y \<Longrightarrow> x + pmf (sds R47) d \<le> y + pmf (sds R47) d\<rbrakk> \<Longrightarrow> 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
show "pmf (sds R31) c \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + pmf (sds R47) d \<le> y + pmf (sds R47) d; \<And>x y. x \<le> y \<Longrightarrow> x + pmf (sds R47) d \<le> y + pmf (sds R47) d\<rbrakk> \<Longrightarrow> 1 / 2 \<le> pmf (sds R31) c

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R31) c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R31) c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R31: "pmf (sds R31) a = 0" "pmf (sds R31) c = 1/2" "pmf (sds R31) b + pmf (sds R31) d = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R31) a = 0 &&& pmf (sds R31) c = 1 / 2 &&& pmf (sds R31) b + pmf (sds R31) d = 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. pmf (sds R31) a = 0
 2. pmf (sds R31) c = 1 / 2
 3. pmf (sds R31) b + pmf (sds R31) d = 1 / 2
[PROOF STEP]
from R2_R38.strategyproofness(1) lottery_conditions[OF R38.wf]
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R38) c + pmf (sds R38) a \<le> pmf (sds R2) c + pmf (sds R2) a
0 \<le> pmf (sds R38) a
0 \<le> pmf (sds R38) b
0 \<le> pmf (sds R38) c
0 \<le> pmf (sds R38) d
pmf (sds R38) a + pmf (sds R38) b + pmf (sds R38) c + pmf (sds R38) d = 1
[PROOF STEP]
have A: "pmf (sds R38) b + pmf (sds R38) d \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R38) c + pmf (sds R38) a \<le> pmf (sds R2) c + pmf (sds R2) a
0 \<le> pmf (sds R38) a
0 \<le> pmf (sds R38) b
0 \<le> pmf (sds R38) c
0 \<le> pmf (sds R38) d
pmf (sds R38) a + pmf (sds R38) b + pmf (sds R38) c + pmf (sds R38) d = 1

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R38) b + pmf (sds R38) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R38) b + pmf (sds R38) d

goal (3 subgoals):
 1. pmf (sds R31) a = 0
 2. pmf (sds R31) c = 1 / 2
 3. pmf (sds R31) b + pmf (sds R31) d = 1 / 2
[PROOF STEP]
with R31_c_ge_one_half R31_R38.strategyproofness(1)
        lottery_conditions[OF R31.wf] lottery_conditions[OF R38.wf]
[PROOF STATE]
proof (chain)
picking this:
1 / 2 \<le> pmf (sds R31) c
(pmf (sds R38) b + pmf (sds R38) d < pmf (sds R31) d + pmf (sds R31) b \<or> pmf (sds R38) b + (pmf (sds R38) d + pmf (sds R38) c) < pmf (sds R31) d + (pmf (sds R31) b + pmf (sds R31) a)) \<or> pmf (sds R38) b + pmf (sds R38) d = pmf (sds R31) d + pmf (sds R31) b \<and> pmf (sds R38) b + (pmf (sds R38) d + pmf (sds R38) c) = pmf (sds R31) d + (pmf (sds R31) b + pmf (sds R31) a)
0 \<le> pmf (sds R31) a
0 \<le> pmf (sds R31) b
0 \<le> pmf (sds R31) c
0 \<le> pmf (sds R31) d
pmf (sds R31) a + pmf (sds R31) b + pmf (sds R31) c + pmf (sds R31) d = 1
0 \<le> pmf (sds R38) a
0 \<le> pmf (sds R38) b
0 \<le> pmf (sds R38) c
0 \<le> pmf (sds R38) d
pmf (sds R38) a + pmf (sds R38) b + pmf (sds R38) c + pmf (sds R38) d = 1
1 / 2 \<le> pmf (sds R38) b + pmf (sds R38) d
[PROOF STEP]
have "pmf (sds R38) b + pmf (sds R38) d = pmf (sds R31) d + pmf (sds R31) b"
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> pmf (sds R31) c
(pmf (sds R38) b + pmf (sds R38) d < pmf (sds R31) d + pmf (sds R31) b \<or> pmf (sds R38) b + (pmf (sds R38) d + pmf (sds R38) c) < pmf (sds R31) d + (pmf (sds R31) b + pmf (sds R31) a)) \<or> pmf (sds R38) b + pmf (sds R38) d = pmf (sds R31) d + pmf (sds R31) b \<and> pmf (sds R38) b + (pmf (sds R38) d + pmf (sds R38) c) = pmf (sds R31) d + (pmf (sds R31) b + pmf (sds R31) a)
0 \<le> pmf (sds R31) a
0 \<le> pmf (sds R31) b
0 \<le> pmf (sds R31) c
0 \<le> pmf (sds R31) d
pmf (sds R31) a + pmf (sds R31) b + pmf (sds R31) c + pmf (sds R31) d = 1
0 \<le> pmf (sds R38) a
0 \<le> pmf (sds R38) b
0 \<le> pmf (sds R38) c
0 \<le> pmf (sds R38) d
pmf (sds R38) a + pmf (sds R38) b + pmf (sds R38) c + pmf (sds R38) d = 1
1 / 2 \<le> pmf (sds R38) b + pmf (sds R38) d

goal (1 subgoal):
 1. pmf (sds R38) b + pmf (sds R38) d = pmf (sds R31) d + pmf (sds R31) b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R38) b + pmf (sds R38) d = pmf (sds R31) d + pmf (sds R31) b

goal (3 subgoals):
 1. pmf (sds R31) a = 0
 2. pmf (sds R31) c = 1 / 2
 3. pmf (sds R31) b + pmf (sds R31) d = 1 / 2
[PROOF STEP]
with R31_c_ge_one_half A lottery_conditions[OF R31.wf] lottery_conditions[OF R38.wf]
[PROOF STATE]
proof (chain)
picking this:
1 / 2 \<le> pmf (sds R31) c
1 / 2 \<le> pmf (sds R38) b + pmf (sds R38) d
0 \<le> pmf (sds R31) a
0 \<le> pmf (sds R31) b
0 \<le> pmf (sds R31) c
0 \<le> pmf (sds R31) d
pmf (sds R31) a + pmf (sds R31) b + pmf (sds R31) c + pmf (sds R31) d = 1
0 \<le> pmf (sds R38) a
0 \<le> pmf (sds R38) b
0 \<le> pmf (sds R38) c
0 \<le> pmf (sds R38) d
pmf (sds R38) a + pmf (sds R38) b + pmf (sds R38) c + pmf (sds R38) d = 1
pmf (sds R38) b + pmf (sds R38) d = pmf (sds R31) d + pmf (sds R31) b
[PROOF STEP]
show "pmf (sds R31) a = 0" "pmf (sds R31) c = 1/2" "pmf (sds R31) b + pmf (sds R31) d = 1/2"
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> pmf (sds R31) c
1 / 2 \<le> pmf (sds R38) b + pmf (sds R38) d
0 \<le> pmf (sds R31) a
0 \<le> pmf (sds R31) b
0 \<le> pmf (sds R31) c
0 \<le> pmf (sds R31) d
pmf (sds R31) a + pmf (sds R31) b + pmf (sds R31) c + pmf (sds R31) d = 1
0 \<le> pmf (sds R38) a
0 \<le> pmf (sds R38) b
0 \<le> pmf (sds R38) c
0 \<le> pmf (sds R38) d
pmf (sds R38) a + pmf (sds R38) b + pmf (sds R38) c + pmf (sds R38) d = 1
pmf (sds R38) b + pmf (sds R38) d = pmf (sds R31) d + pmf (sds R31) b

goal (1 subgoal):
 1. pmf (sds R31) a = 0 &&& pmf (sds R31) c = 1 / 2 &&& pmf (sds R31) b + pmf (sds R31) d = 1 / 2
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
pmf (sds R31) a = 0
pmf (sds R31) c = 1 / 2
pmf (sds R31) b + pmf (sds R31) d = 1 / 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma absurd: False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using R31 R45_R31.strategyproofness(2)
[PROOF STATE]
proof (prove)
using this:
pmf (sds R31) a = 0
pmf (sds R31) c = 1 / 2
pmf (sds R31) b + pmf (sds R31) d = 1 / 2
(pmf (sds R31) c + pmf (sds R31) d < pmf (sds R45) b + pmf (sds R45) a \<or> pmf (sds R31) c + (pmf (sds R31) d + pmf (sds R31) b) < pmf (sds R45) b + (pmf (sds R45) a + pmf (sds R45) c)) \<or> pmf (sds R31) c + pmf (sds R31) d = pmf (sds R45) b + pmf (sds R45) a \<and> pmf (sds R31) c + (pmf (sds R31) d + pmf (sds R31) b) = pmf (sds R45) b + (pmf (sds R45) a + pmf (sds R45) c)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp


[STATEMENT]
lemma finite_list':
  assumes "finite A"
  obtains xs where "A = set xs" "distinct xs" "length xs = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>A = set xs; distinct xs; length xs = card A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>A = set xs; distinct xs; length xs = card A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
obtain xs where "set xs = A"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. (\<And>xs. set xs = A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_list
[PROOF STATE]
proof (prove)
using this:
finite A
finite ?A \<Longrightarrow> \<exists>xs. set xs = ?A

goal (1 subgoal):
 1. (\<And>xs. set xs = A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set xs = A

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>A = set xs; distinct xs; length xs = card A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set xs = A

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using distinct_card[of "remdups xs"]
[PROOF STATE]
proof (prove)
using this:
set xs = A
distinct (remdups xs) \<Longrightarrow> card (set (remdups xs)) = length (remdups xs)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro that[of "remdups xs"]) simp_all
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_list_subset:
  assumes "finite A" "card A \<ge> n"
  obtains xs where "set xs \<subseteq> A" "distinct xs" "length xs = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>set xs \<subseteq> A; distinct xs; length xs = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>set xs \<subseteq> A; distinct xs; length xs = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain xs where "A = set xs" "distinct xs" "length xs = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>A = set xs; distinct xs; length xs = card A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_list'[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
(\<And>xs. \<lbrakk>A = set xs; distinct xs; length xs = card A\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>A = set xs; distinct xs; length xs = card A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A = set xs
distinct xs
length xs = card A

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>set xs \<subseteq> A; distinct xs; length xs = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
finite A
n \<le> card A
A = set xs
distinct xs
length xs = card A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite A
n \<le> card A
A = set xs
distinct xs
length xs = card A

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro that[of "take n xs"]) (simp_all add: set_take_subset)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_ge_4E:
  assumes "finite A" "card A \<ge> 4"
  obtains a b c d where "distinct [a,b,c,d]" "{a,b,c,d} \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>distinct [a, b, c, d]; {a, b, c, d} \<subseteq> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>distinct [a, b, c, d]; {a, b, c, d} \<subseteq> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
4 \<le> card A
[PROOF STEP]
obtain xs where xs: "set xs \<subseteq> A" "distinct xs" "length xs = 4"
[PROOF STATE]
proof (prove)
using this:
finite A
4 \<le> card A

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>set xs \<subseteq> A; distinct xs; length xs = 4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule finite_list_subset)
[PROOF STATE]
proof (state)
this:
set xs \<subseteq> A
distinct xs
length xs = 4

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>distinct [a, b, c, d]; {a, b, c, d} \<subseteq> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set xs \<subseteq> A
distinct xs
length xs = 4
[PROOF STEP]
obtain a b c d where "xs = [a, b, c, d]"
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> A
distinct xs
length xs = 4

goal (1 subgoal):
 1. (\<And>a b c d. xs = [a, b, c, d] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: eval_nat_numeral length_Suc_conv)
[PROOF STATE]
proof (state)
this:
xs = [a, b, c, d]

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>distinct [a, b, c, d]; {a, b, c, d} \<subseteq> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with xs
[PROOF STATE]
proof (chain)
picking this:
set xs \<subseteq> A
distinct xs
length xs = 4
xs = [a, b, c, d]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> A
distinct xs
length xs = 4
xs = [a, b, c, d]

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro that[of a b c d]) simp_all
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma absurd: False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
from card_ge_4E[OF finite_agents agents_ge_4]
[PROOF STATE]
proof (chain)
picking this:
(\<And>a b c d. \<lbrakk>distinct [a, b, c, d]; {a, b, c, d} \<subseteq> agents\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain A1 A2 A3 A4 where agents: "distinct [A1, A2, A3, A4]" "{A1, A2, A3, A4} \<subseteq> agents"
[PROOF STATE]
proof (prove)
using this:
(\<And>a b c d. \<lbrakk>distinct [a, b, c, d]; {a, b, c, d} \<subseteq> agents\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>A1 A2 A3 A4. \<lbrakk>distinct [A1, A2, A3, A4]; {A1, A2, A3, A4} \<subseteq> agents\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
distinct [A1, A2, A3, A4]
{A1, A2, A3, A4} \<subseteq> agents

goal (1 subgoal):
 1. False
[PROOF STEP]
from card_ge_4E[OF finite_alts alts_ge_4]
[PROOF STATE]
proof (chain)
picking this:
(\<And>a b c d. \<lbrakk>distinct [a, b, c, d]; {a, b, c, d} \<subseteq> alts\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain a b c d where alts: "distinct [a, b, c, d]" "{a, b, c, d} \<subseteq> alts"
[PROOF STATE]
proof (prove)
using this:
(\<And>a b c d. \<lbrakk>distinct [a, b, c, d]; {a, b, c, d} \<subseteq> alts\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>distinct [a, b, c, d]; {a, b, c, d} \<subseteq> alts\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
distinct [a, b, c, d]
{a, b, c, d} \<subseteq> alts

goal (1 subgoal):
 1. False
[PROOF STEP]
define agents' alts' where "agents' = {A1,A2,A3,A4}" and "alts' = {a,b,c,d}"
[PROOF STATE]
proof (state)
this:
agents' = {A1, A2, A3, A4}
alts' = {a, b, c, d}

goal (1 subgoal):
 1. False
[PROOF STEP]
from agents alts
[PROOF STATE]
proof (chain)
picking this:
distinct [A1, A2, A3, A4]
{A1, A2, A3, A4} \<subseteq> agents
distinct [a, b, c, d]
{a, b, c, d} \<subseteq> alts
[PROOF STEP]
interpret sds_lowering_anonymous_neutral_sdeff_stratproof agents alts sds agents' alts'
[PROOF STATE]
proof (prove)
using this:
distinct [A1, A2, A3, A4]
{A1, A2, A3, A4} \<subseteq> agents
distinct [a, b, c, d]
{a, b, c, d} \<subseteq> alts

goal (1 subgoal):
 1. sds_lowering_anonymous_neutral_sdeff_stratproof agents alts sds agents' alts'
[PROOF STEP]
unfolding agents'_def alts'_def
[PROOF STATE]
proof (prove)
using this:
distinct [A1, A2, A3, A4]
{A1, A2, A3, A4} \<subseteq> agents
distinct [a, b, c, d]
{a, b, c, d} \<subseteq> alts

goal (1 subgoal):
 1. sds_lowering_anonymous_neutral_sdeff_stratproof agents alts sds {A1, A2, A3, A4} {a, b, c, d}
[PROOF STEP]
by unfold_locales simp_all
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
from agents alts
[PROOF STATE]
proof (chain)
picking this:
distinct [A1, A2, A3, A4]
{A1, A2, A3, A4} \<subseteq> agents
distinct [a, b, c, d]
{a, b, c, d} \<subseteq> alts
[PROOF STEP]
interpret sds_impossibility_4_4 agents' alts' lowered A1 A2 A3 A4 a b c d
[PROOF STATE]
proof (prove)
using this:
distinct [A1, A2, A3, A4]
{A1, A2, A3, A4} \<subseteq> agents
distinct [a, b, c, d]
{a, b, c, d} \<subseteq> alts

goal (1 subgoal):
 1. sds_impossibility_4_4 agents' alts' lowered A1 A2 A3 A4 a b c d
[PROOF STEP]
by unfold_locales (simp_all add: agents'_def alts'_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
from absurd
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_majorities_intersect:
    assumes crd: "card E < card S + card T"
        and s: "S \<subseteq> E" and t: "T \<subseteq> E" and e: "finite E"
    shows "S \<inter> T \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> T \<noteq> {}
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> False
[PROOF STEP]
assume contra: "S \<inter> T = {}"
[PROOF STATE]
proof (state)
this:
S \<inter> T = {}

goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> False
[PROOF STEP]
from s t e
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> E
T \<subseteq> E
finite E
[PROOF STEP]
have "finite S" and "finite T"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> E
T \<subseteq> E
finite E

goal (1 subgoal):
 1. finite S &&& finite T
[PROOF STEP]
by (auto simp: finite_subset)
[PROOF STATE]
proof (state)
this:
finite S
finite T

goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> False
[PROOF STEP]
with crd contra
[PROOF STATE]
proof (chain)
picking this:
card E < card S + card T
S \<inter> T = {}
finite S
finite T
[PROOF STEP]
have "card E < card (S \<union> T)"
[PROOF STATE]
proof (prove)
using this:
card E < card S + card T
S \<inter> T = {}
finite S
finite T

goal (1 subgoal):
 1. card E < card (S \<union> T)
[PROOF STEP]
by (auto simp add: card_Un_Int)
[PROOF STATE]
proof (state)
this:
card E < card (S \<union> T)

goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card E < card (S \<union> T)

goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> False
[PROOF STEP]
from s t e
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> E
T \<subseteq> E
finite E
[PROOF STEP]
have "card (S \<union> T) \<le> card E"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> E
T \<subseteq> E
finite E

goal (1 subgoal):
 1. card (S \<union> T) \<le> card E
[PROOF STEP]
by (simp add: card_mono)
[PROOF STATE]
proof (state)
this:
card (S \<union> T) \<le> card E

goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card E < card (S \<union> T)
card (S \<union> T) \<le> card E
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
card E < card (S \<union> T)
card (S \<union> T) \<le> card E

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_majoritiesE:
  assumes crd: "card E < card S + card T"
      and s: "S \<subseteq> E" and t: "T \<subseteq> E" and e: "finite E"
  obtains p where "p \<in> S" and "p \<in> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
card E < card S + card T
S \<subseteq> E
T \<subseteq> E
finite E
[PROOF STEP]
have "S \<inter> T \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
card E < card S + card T
S \<subseteq> E
T \<subseteq> E
finite E

goal (1 subgoal):
 1. S \<inter> T \<noteq> {}
[PROOF STEP]
by (rule abs_majorities_intersect)
[PROOF STATE]
proof (state)
this:
S \<inter> T \<noteq> {}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S \<inter> T \<noteq> {}
[PROOF STEP]
obtain p where "p \<in> S \<inter> T"
[PROOF STATE]
proof (prove)
using this:
S \<inter> T \<noteq> {}

goal (1 subgoal):
 1. (\<And>p. p \<in> S \<inter> T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<in> S \<inter> T

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?p \<in> S; ?p \<in> T\<rbrakk> \<Longrightarrow> thesis
p \<in> S \<inter> T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<in> S; ?p \<in> T\<rbrakk> \<Longrightarrow> thesis
p \<in> S \<inter> T

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_majoritiesE':
  assumes Smaj: "card S > (card E) div 2" and Tmaj: "card T > (card E) div 2"
      and s: "S \<subseteq> E" and t: "T \<subseteq> E" and e: "finite E"
  obtains p where "p \<in> S" and "p \<in> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule abs_majoritiesE[OF _ s t e])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>p. \<lbrakk>p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> card E < card S + card T
 2. \<And>p. \<lbrakk>\<And>p. \<lbrakk>p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis; p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from Smaj Tmaj
[PROOF STATE]
proof (chain)
picking this:
card E div 2 < card S
card E div 2 < card T
[PROOF STEP]
show "card E < card S + card T"
[PROOF STATE]
proof (prove)
using this:
card E div 2 < card S
card E div 2 < card T

goal (1 subgoal):
 1. card E < card S + card T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card E < card S + card T

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<And>p. \<lbrakk>p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis; p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
qed


[STATEMENT]
lemma majorities_intersect:
  assumes crd: "card (UNIV::('a::finite) set) < card (S::'a set) + card T"
  shows "S \<inter> T \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> T \<noteq> {}
[PROOF STEP]
by (rule abs_majorities_intersect[OF crd]) auto


[STATEMENT]
lemma majoritiesE:
  assumes crd: "card (UNIV::('a::finite) set) < card (S::'a set) + card (T::'a set)"
  obtains p where "p \<in> S" and "p \<in> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using crd majorities_intersect
[PROOF STATE]
proof (prove)
using this:
card UNIV < card S + card T
card UNIV < card ?S + card ?T \<Longrightarrow> ?S \<inter> ?T \<noteq> {}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma majoritiesE':
  assumes S: "card (S::('a::finite) set) > (card (UNIV::'a set)) div 2"
  and T: "card (T::'a set) > (card (UNIV::'a set)) div 2"
  obtains p where "p \<in> S" and "p \<in> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> S; p \<in> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule abs_majoritiesE'[OF S T]) auto


[STATEMENT]
lemma oPrec_oSuc [simp]: "oPrec (oSuc x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oPrec (oSuc x) = x
[PROOF STEP]
by (unfold oPrec_def, rule the_equality, simp_all)


[STATEMENT]
lemma oPrec_less: "\<exists>p. x = oSuc p \<Longrightarrow> oPrec x < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. x = oSuc p \<Longrightarrow> oPrec x < x
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma ordinal_rec0_0:
"ordinal_rec0 z s l 0 = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_rec0 z s l 0 = z
[PROOF STEP]
apply (rule trans[OF def_wfrec[OF ordinal_rec0_def wf]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 = 0 then z else if \<exists>p. 0 = oSuc p then s (oPrec 0) (cut (ordinal_rec0 z s l) {(x, y). x < y} 0 (oPrec 0)) else THE y. \<forall>f. (\<forall>n. f n < oLimit f) \<and> oLimit f = 0 \<longrightarrow> l (\<lambda>n. cut (ordinal_rec0 z s l) {(x, y). x < y} 0 (f n)) = y) = z
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ordinal_rec0_oSuc:
"ordinal_rec0 z s l (oSuc x) = s x (ordinal_rec0 z s l x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_rec0 z s l (oSuc x) = s x (ordinal_rec0 z s l x)
[PROOF STEP]
apply (rule trans[OF def_wfrec[OF ordinal_rec0_def wf]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if oSuc x = 0 then z else if \<exists>p. oSuc x = oSuc p then s (oPrec (oSuc x)) (cut (ordinal_rec0 z s l) {(x, y). x < y} (oSuc x) (oPrec (oSuc x))) else THE y. \<forall>f. (\<forall>n. f n < oLimit f) \<and> oLimit f = oSuc x \<longrightarrow> l (\<lambda>n. cut (ordinal_rec0 z s l) {(x, y). x < y} (oSuc x) (f n)) = y) = s x (ordinal_rec0 z s l x)
[PROOF STEP]
apply (simp add: cut_apply)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma limit_ordinal_not_0: "limit_ordinal x \<Longrightarrow> x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_ordinal x \<Longrightarrow> x \<noteq> 0
[PROOF STEP]
by (clarsimp)


[STATEMENT]
lemma limit_ordinal_not_oSuc: "limit_ordinal x \<Longrightarrow> x \<noteq> oSuc p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_ordinal x \<Longrightarrow> x \<noteq> oSuc p
[PROOF STEP]
by (clarsimp)


[STATEMENT]
lemma ordinal_rec0_limit_ordinal:
"limit_ordinal x \<Longrightarrow> ordinal_rec0 z s l x =
 (THE y. \<forall>f. (\<forall>n. f n < oLimit f) \<and> oLimit f = x \<longrightarrow>
   l (\<lambda>n. ordinal_rec0 z s l (f n)) = y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_ordinal x \<Longrightarrow> ordinal_rec0 z s l x = (THE y. \<forall>f. (\<forall>n. f n < oLimit f) \<and> oLimit f = x \<longrightarrow> l (\<lambda>n. ordinal_rec0 z s l (f n)) = y)
[PROOF STEP]
apply (rule trans[OF def_wfrec[OF ordinal_rec0_def wf]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_ordinal x \<Longrightarrow> (if x = 0 then z else if \<exists>p. x = oSuc p then s (oPrec x) (cut (ordinal_rec0 z s l) {(x, y). x < y} x (oPrec x)) else THE y. \<forall>f. (\<forall>n. f n < oLimit f) \<and> oLimit f = x \<longrightarrow> l (\<lambda>n. cut (ordinal_rec0 z s l) {(x, y). x < y} x (f n)) = y) = (THE y. \<forall>f. (\<forall>n. f n < oLimit f) \<and> oLimit f = x \<longrightarrow> l (\<lambda>n. ordinal_rec0 z s l (f n)) = y)
[PROOF STEP]
apply (simp add: limit_ordinal_not_oSuc limit_ordinal_not_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_ordinal x \<Longrightarrow> (THE y. \<forall>f. (\<forall>n. f n < oLimit f) \<and> oLimit f = x \<longrightarrow> l (\<lambda>n. cut (ordinal_rec0 z s l) {(x, y). x < y} x (f n)) = y) = (THE y. \<forall>f. (\<forall>n. f n < oLimit f) \<and> oLimit f = x \<longrightarrow> l (\<lambda>n. ordinal_rec0 z s l (f n)) = y)
[PROOF STEP]
apply (rule_tac f=The in arg_cong, rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. limit_ordinal x \<Longrightarrow> (\<forall>f. (\<forall>n. f n < oLimit f) \<and> oLimit f = x \<longrightarrow> l (\<lambda>n. cut (ordinal_rec0 z s l) {(x, y). x < y} x (f n)) = y) = (\<forall>f. (\<forall>n. f n < oLimit f) \<and> oLimit f = x \<longrightarrow> l (\<lambda>n. ordinal_rec0 z s l (f n)) = y)
[PROOF STEP]
apply (rule_tac f=All in arg_cong, rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y f. limit_ordinal x \<Longrightarrow> ((\<forall>n. f n < oLimit f) \<and> oLimit f = x \<longrightarrow> l (\<lambda>n. cut (ordinal_rec0 z s l) {(x, y). x < y} x (f n)) = y) = ((\<forall>n. f n < oLimit f) \<and> oLimit f = x \<longrightarrow> l (\<lambda>n. ordinal_rec0 z s l (f n)) = y)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y f. \<lbrakk>limit_ordinal (oLimit f); \<forall>n. f n < oLimit f; x = oLimit f\<rbrakk> \<Longrightarrow> l (\<lambda>n. ordinal_rec0 z s l (f n)) = l (\<lambda>n. cut (ordinal_rec0 z s l) {(x, y). x < y} (oLimit f) (f n))
 2. \<And>y f. \<lbrakk>limit_ordinal (oLimit f); \<forall>n. f n < oLimit f; x = oLimit f\<rbrakk> \<Longrightarrow> l (\<lambda>n. cut (ordinal_rec0 z s l) {(x, y). x < y} (oLimit f) (f n)) = l (\<lambda>n. ordinal_rec0 z s l (f n))
[PROOF STEP]
apply (simp add: cut_apply)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y f. \<lbrakk>limit_ordinal (oLimit f); \<forall>n. f n < oLimit f; x = oLimit f\<rbrakk> \<Longrightarrow> l (\<lambda>n. cut (ordinal_rec0 z s l) {(x, y). x < y} (oLimit f) (f n)) = l (\<lambda>n. ordinal_rec0 z s l (f n))
[PROOF STEP]
apply (simp add: cut_apply)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma porder_order: "porder ((\<le>) :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. porder (\<le>)
[PROOF STEP]
apply (rule porder.intro)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<le> x
 2. \<And>x y z. \<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z
 3. \<And>x y. \<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (rule order_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z
 2. \<And>x y. \<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (rule order_trans, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (rule order_antisym, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in porder) flip: "porder (\<lambda>x y. y << x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. porder (\<lambda>x y. y << x)
[PROOF STEP]
apply (rule porder.intro)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x << x
 2. \<And>x y z. \<lbrakk>y << x; z << y\<rbrakk> \<Longrightarrow> z << x
 3. \<And>x y. \<lbrakk>y << x; x << y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (rule po_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>y << x; z << y\<rbrakk> \<Longrightarrow> z << x
 2. \<And>x y. \<lbrakk>y << x; x << y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (rule po_trans, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>y << x; x << y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (rule po_antisym, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in omega_complete) lub_cong_lemma:
"\<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g;
 \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk>
 \<Longrightarrow> lub (\<lambda>n. F (f n)) << lub (\<lambda>n. F (g n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> lub (\<lambda>n. F (f n)) << lub (\<lambda>n. F (g n))
[PROOF STEP]
apply (rule is_lub_lub[rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> F (f n) << lub (\<lambda>n. F (g n))
[PROOF STEP]
apply (subgoal_tac "f n < oLimit g")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y; f n < oLimit g\<rbrakk> \<Longrightarrow> F (f n) << lub (\<lambda>n. F (g n))
 2. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> f n < oLimit g
[PROOF STEP]
apply (drule less_oLimitD, clarify, rename_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y; f n < g m\<rbrakk> \<Longrightarrow> F (f n) << lub (\<lambda>n. F (g n))
 2. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> f n < oLimit g
[PROOF STEP]
apply (drule_tac x="g m" in spec, drule mp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n m. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; f n < g m\<rbrakk> \<Longrightarrow> g m < oLimit g
 2. \<And>n m. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; f n < g m; \<forall>x\<le>g m. F x << F (g m)\<rbrakk> \<Longrightarrow> F (f n) << lub (\<lambda>n. F (g n))
 3. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> f n < oLimit g
[PROOF STEP]
apply (erule spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; f n < g m; \<forall>x\<le>g m. F x << F (g m)\<rbrakk> \<Longrightarrow> F (f n) << lub (\<lambda>n. F (g n))
 2. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> f n < oLimit g
[PROOF STEP]
apply (drule_tac x="f n" in spec, drule mp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n m. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; f n < g m\<rbrakk> \<Longrightarrow> f n \<le> g m
 2. \<And>n m. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; f n < g m; F (f n) << F (g m)\<rbrakk> \<Longrightarrow> F (f n) << lub (\<lambda>n. F (g n))
 3. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> f n < oLimit g
[PROOF STEP]
apply (erule order_less_imp_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; f n < g m; F (f n) << F (g m)\<rbrakk> \<Longrightarrow> F (f n) << lub (\<lambda>n. F (g n))
 2. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> f n < oLimit g
[PROOF STEP]
apply (erule po_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; f n < g m\<rbrakk> \<Longrightarrow> F (g m) << lub (\<lambda>n. F (g n))
 2. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> f n < oLimit g
[PROOF STEP]
apply (rule is_ub_lub)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> f n < oLimit g
[PROOF STEP]
apply (rule order_less_le_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> f n < ?y23 n
 2. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> ?y23 n \<le> oLimit g
[PROOF STEP]
apply (erule spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f \<le> oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> oLimit f \<le> oLimit g
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in omega_complete) lub_cong:
"\<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g;
 \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk>
 \<Longrightarrow> lub (\<lambda>n. F (f n)) = lub (\<lambda>n. F (g n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> lub (\<lambda>n. F (f n)) = lub (\<lambda>n. F (g n))
[PROOF STEP]
apply (rule po_antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> lub (\<lambda>n. F (f n)) << lub (\<lambda>n. F (g n))
 2. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> lub (\<lambda>n. F (g n)) << lub (\<lambda>n. F (f n))
[PROOF STEP]
apply (rule lub_cong_lemma, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> oLimit f \<le> oLimit g
 2. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y
 3. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> lub (\<lambda>n. F (g n)) << lub (\<lambda>n. F (f n))
[PROOF STEP]
apply (simp add: po_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y
 2. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> lub (\<lambda>n. F (g n)) << lub (\<lambda>n. F (f n))
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> lub (\<lambda>n. F (g n)) << lub (\<lambda>n. F (f n))
[PROOF STEP]
apply (rule lub_cong_lemma, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> oLimit g \<le> oLimit f
 2. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> \<forall>y<oLimit f. \<forall>x\<le>y. F x << F y
[PROOF STEP]
apply (simp add: po_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>m. g m < oLimit g; oLimit f = oLimit g; \<forall>y<oLimit g. \<forall>x\<le>y. F x << F y\<rbrakk> \<Longrightarrow> \<forall>y<oLimit f. \<forall>x\<le>y. F x << F y
[PROOF STEP]
apply (drule sym, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in omega_complete) ordinal_rec0_mono_lemma:
assumes s: "\<forall>p x. x << s p x"
shows "\<forall>y\<le>w. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<le>w. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply (rule_tac a=w in oLimit_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>y\<le>0. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
 2. \<And>x. \<forall>y\<le>x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y \<Longrightarrow> \<forall>y\<le>oSuc x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y)\<rbrakk> \<Longrightarrow> \<forall>y\<le>oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply (simp add: po_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>y\<le>x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y \<Longrightarrow> \<forall>y\<le>oSuc x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y)\<rbrakk> \<Longrightarrow> \<forall>y\<le>oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y xa. \<lbrakk>\<forall>y\<le>x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y; y \<le> oSuc x; xa \<le> y\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub y
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y)\<rbrakk> \<Longrightarrow> \<forall>y\<le>oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply (erule le_oSucE, simp, clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>y\<le>x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y; xa \<le> oSuc x\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub (oSuc x)
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y)\<rbrakk> \<Longrightarrow> \<forall>y\<le>oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply (erule le_oSucE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>y\<le>x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y; xa \<le> x\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub (oSuc x)
 2. \<And>x xa. \<lbrakk>\<forall>y\<le>x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y; xa = oSuc x\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub (oSuc x)
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y)\<rbrakk> \<Longrightarrow> \<forall>y\<le>oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply (drule spec, drule mp, rule order_refl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>xa \<le> x; \<forall>xa\<le>x. ordinal_rec0 z s lub xa << ordinal_rec0 z s lub x\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub (oSuc x)
 2. \<And>x xa. \<lbrakk>\<forall>y\<le>x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y; xa = oSuc x\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub (oSuc x)
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y)\<rbrakk> \<Longrightarrow> \<forall>y\<le>oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply (drule spec, drule mp, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>xa \<le> x; ordinal_rec0 z s lub xa << ordinal_rec0 z s lub x\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub (oSuc x)
 2. \<And>x xa. \<lbrakk>\<forall>y\<le>x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y; xa = oSuc x\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub (oSuc x)
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y)\<rbrakk> \<Longrightarrow> \<forall>y\<le>oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply (erule po_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. xa \<le> x \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oSuc x)
 2. \<And>x xa. \<lbrakk>\<forall>y\<le>x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y; xa = oSuc x\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub (oSuc x)
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y)\<rbrakk> \<Longrightarrow> \<forall>y\<le>oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply (simp add: ordinal_rec0_oSuc s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>y\<le>x. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y; xa = oSuc x\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub (oSuc x)
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y)\<rbrakk> \<Longrightarrow> \<forall>y\<le>oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply (simp add: po_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y)\<rbrakk> \<Longrightarrow> \<forall>y\<le>oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f y x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); y \<le> oLimit f; x \<le> y\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply (erule le_oLimitE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f y x n. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> y; y \<le> f n\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
 2. \<And>f y x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> y; y = oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f y x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> y; y = oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
[PROOF STEP]
apply (subgoal_tac "ordinal_rec0 z s lub (oLimit f) =
                     lub (\<lambda>n. ordinal_rec0 z s lub (f n))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
 2. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (erule le_oLimitE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f x n. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n)); x \<le> f n\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
 2. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n)); x = oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
 3. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (drule_tac x=n in spec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f x n. \<lbrakk>OrdinalInduct.strict_mono f; ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n)); x \<le> f n; \<forall>y\<le>f n. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
 2. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n)); x = oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
 3. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (drule spec, drule mp, rule order_refl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f x n. \<lbrakk>OrdinalInduct.strict_mono f; ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n)); x \<le> f n; \<forall>x\<le>f n. ordinal_rec0 z s lub x << ordinal_rec0 z s lub (f n)\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
 2. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n)); x = oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
 3. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (drule spec, drule mp, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f x n. \<lbrakk>OrdinalInduct.strict_mono f; ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n)); x \<le> f n; ordinal_rec0 z s lub x << ordinal_rec0 z s lub (f n)\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
 2. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n)); x = oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
 3. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (erule po_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f x n. \<lbrakk>OrdinalInduct.strict_mono f; ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n)); x \<le> f n\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub (f n) << ordinal_rec0 z s lub (oLimit f)
 2. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n)); x = oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
 3. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (simp, rule is_ub_lub)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n)); x = oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub (oLimit f)
 2. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (simp add: po_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (simp only: ordinal_rec0_limit_ordinal strict_mono_limit_ordinal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f\<rbrakk> \<Longrightarrow> (THE y. \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (rule the_equality, clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x fa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f\<rbrakk> \<Longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
 2. \<And>f x y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (rule lub_cong, assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>f x fa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f\<rbrakk> \<Longrightarrow> \<forall>m. f m < oLimit f
 2. \<And>f x fa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f\<rbrakk> \<Longrightarrow> oLimit fa = oLimit f
 3. \<And>f x fa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f\<rbrakk> \<Longrightarrow> \<forall>y<oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
 4. \<And>f x y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (simp add: strict_mono_less_oLimit)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f x fa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f\<rbrakk> \<Longrightarrow> oLimit fa = oLimit f
 2. \<And>f x fa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f\<rbrakk> \<Longrightarrow> \<forall>y<oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
 3. \<And>f x y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x fa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f\<rbrakk> \<Longrightarrow> \<forall>y<oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
 2. \<And>f x y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x fa y xa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f; y < oLimit f; xa \<le> y\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub y
 2. \<And>f x y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (drule less_oLimitD, clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x fa y xa n. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f; xa \<le> y; y < f n\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub y
 2. \<And>f x y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (drule order_less_imp_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x fa y xa n. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f; xa \<le> y; y \<le> f n\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub xa << ordinal_rec0 z s lub y
 2. \<And>f x y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<le> f n \<longrightarrow> (\<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y); x \<le> oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (drule_tac x=f in spec, simp add: strict_mono_less_oLimit)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in omega_complete) ordinal_rec0_mono:
assumes s: "\<forall>p x. x << s p x"
shows "x \<le> y \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
[PROOF STEP]
apply (rule ordinal_rec0_mono_lemma[OF s, rule_format])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> y \<le> ?w
 2. x \<le> y \<Longrightarrow> x \<le> y
[PROOF STEP]
apply (rule order_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x \<le> y
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in omega_complete) ordinal_rec0_oLimit:
assumes s: "\<forall>p x. x << s p x"
shows "ordinal_rec0 z s lub (oLimit f) =
         lub (\<lambda>n. ordinal_rec0 z s lub (f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (case_tac "\<forall>n. f n < oLimit f")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
 2. \<not> (\<forall>n. f n < oLimit f) \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (simp add: ordinal_rec0_limit_ordinal limit_ordinal_oLimitI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>n. f n < oLimit f \<Longrightarrow> (THE y. \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
 2. \<not> (\<forall>n. f n < oLimit f) \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (rule the_equality, clarify)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>fa. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f\<rbrakk> \<Longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
 2. \<And>y. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
 3. \<not> (\<forall>n. f n < oLimit f) \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (rule lub_cong, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>fa. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f\<rbrakk> \<Longrightarrow> \<forall>y<oLimit f. \<forall>x\<le>y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
 2. \<And>y. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
 3. \<not> (\<forall>n. f n < oLimit f) \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>fa y x. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>n. fa n < oLimit fa; oLimit fa = oLimit f; y < oLimit f; x \<le> y\<rbrakk> \<Longrightarrow> ordinal_rec0 z s lub x << ordinal_rec0 z s lub y
 2. \<And>y. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
 3. \<not> (\<forall>n. f n < oLimit f) \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (erule ordinal_rec0_mono[OF s])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>n. f n < oLimit f; \<forall>fa. (\<forall>n. fa n < oLimit fa) \<and> oLimit fa = oLimit f \<longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (fa n)) = y\<rbrakk> \<Longrightarrow> y = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
 2. \<not> (\<forall>n. f n < oLimit f) \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (drule_tac x=f in spec, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>n. f n < oLimit f) \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (simp add: linorder_not_less, clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. oLimit f \<le> f n \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) = lub (\<lambda>n. ordinal_rec0 z s lub (f n))
[PROOF STEP]
apply (rule po_antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. oLimit f \<le> f n \<Longrightarrow> ordinal_rec0 z s lub (oLimit f) << lub (\<lambda>n. ordinal_rec0 z s lub (f n))
 2. \<And>n. oLimit f \<le> f n \<Longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (f n)) << ordinal_rec0 z s lub (oLimit f)
[PROOF STEP]
apply (erule po_trans[OF ordinal_rec0_mono[OF s]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. ordinal_rec0 z s lub (f n) << lub (\<lambda>n. ordinal_rec0 z s lub (f n))
 2. \<And>n. oLimit f \<le> f n \<Longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (f n)) << ordinal_rec0 z s lub (oLimit f)
[PROOF STEP]
apply (rule is_ub_lub)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. oLimit f \<le> f n \<Longrightarrow> lub (\<lambda>n. ordinal_rec0 z s lub (f n)) << ordinal_rec0 z s lub (oLimit f)
[PROOF STEP]
apply (rule is_lub_lub[rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. oLimit f \<le> f n \<Longrightarrow> ordinal_rec0 z s lub (f na) << ordinal_rec0 z s lub (oLimit f)
[PROOF STEP]
apply (rule ordinal_rec0_mono[OF s le_oLimit])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma omega_complete_oLimit: "omega_complete (\<le>) oLimit"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. omega_complete (\<le>) oLimit
[PROOF STEP]
apply (rule omega_complete.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. porder (\<le>)
 2. omega_complete_axioms (\<le>) oLimit
[PROOF STEP]
apply (rule porder_order)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. omega_complete_axioms (\<le>) oLimit
[PROOF STEP]
apply (rule omega_complete_axioms.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f n. f n \<le> oLimit f
 2. \<And>f x. \<forall>n. f n \<le> x \<Longrightarrow> oLimit f \<le> x
[PROOF STEP]
apply (rule le_oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. \<forall>n. f n \<le> x \<Longrightarrow> oLimit f \<le> x
[PROOF STEP]
apply (erule oLimit_leI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ordinal_rec_0 [simp]: "ordinal_rec z s 0 = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_rec z s 0 = z
[PROOF STEP]
by (unfold ordinal_rec_def, rule ordinal_rec0_0)


[STATEMENT]
lemma ordinal_rec_oSuc [simp]:
"ordinal_rec z s (oSuc x) = s x (ordinal_rec z s x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_rec z s (oSuc x) = s x (ordinal_rec z s x)
[PROOF STEP]
by (unfold ordinal_rec_def, rule ordinal_rec0_oSuc)


[STATEMENT]
lemma ordinal_rec_oLimit:
assumes s: "\<forall>p x. x \<le> s p x"
shows "ordinal_rec z s (oLimit f) = oLimit (\<lambda>n. ordinal_rec z s (f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_rec z s (oLimit f) = oLimit (\<lambda>n. ordinal_rec z s (f n))
[PROOF STEP]
apply (unfold ordinal_rec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_rec0 z s oLimit (oLimit f) = oLimit (\<lambda>n. ordinal_rec0 z s oLimit (f n))
[PROOF STEP]
apply (rule omega_complete.ordinal_rec0_oLimit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. omega_complete ?le oLimit
 2. \<forall>p x. ?le x (s p x)
[PROOF STEP]
apply (rule omega_complete_oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p x. x \<le> s p x
[PROOF STEP]
apply (rule s)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma continuous_ordinal_rec:
assumes s: "\<forall>p x. x \<le> s p x"
shows "continuous (ordinal_rec z s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (ordinal_rec z s)
[PROOF STEP]
apply (rule continuousI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. OrdinalInduct.strict_mono f \<Longrightarrow> ordinal_rec z s (oLimit f) = oLimit (\<lambda>n. ordinal_rec z s (f n))
 2. \<And>x. ordinal_rec z s x \<le> ordinal_rec z s (oSuc x)
[PROOF STEP]
apply (rule ordinal_rec_oLimit[OF s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ordinal_rec z s x \<le> ordinal_rec z s (oSuc x)
[PROOF STEP]
apply (simp add: s)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mono_ordinal_rec:
assumes s: "\<forall>p x. x \<le> s p x"
shows "mono (ordinal_rec z s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (ordinal_rec z s)
[PROOF STEP]
apply (rule continuous.mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (ordinal_rec z s)
[PROOF STEP]
apply (rule continuous_ordinal_rec[OF s])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma normal_ordinal_rec:
assumes s: "\<forall>p x. x < s p x"
shows "normal (ordinal_rec z s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal (ordinal_rec z s)
[PROOF STEP]
apply (rule normalI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. OrdinalInduct.strict_mono f \<Longrightarrow> ordinal_rec z s (oLimit f) = oLimit (\<lambda>n. ordinal_rec z s (f n))
 2. \<And>x. ordinal_rec z s x < ordinal_rec z s (oSuc x)
[PROOF STEP]
apply (rule ordinal_rec_oLimit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. OrdinalInduct.strict_mono f \<Longrightarrow> \<forall>p x. x \<le> s p x
 2. \<And>x. ordinal_rec z s x < ordinal_rec z s (oSuc x)
[PROOF STEP]
apply (simp add: s order_less_imp_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ordinal_rec z s x < ordinal_rec z s (oSuc x)
[PROOF STEP]
apply (simp add: s)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma float_of_int[code]:
  "double_of_int i = double_of_integer (integer_of_int i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. double_of_int i = double_of_integer (integer_of_int i)
[PROOF STEP]
by (auto simp: double_of_integer_def)


[STATEMENT]
lemma compute_Float_of_double[code]:
  "Float_of_double x =
    map_option (\<lambda>(m, e). Float (int_of_integer m) (int_of_integer e)) (man_exp_of_double x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Float_of_double x = map_option (\<lambda>(m, e). Float (int_of_integer m) (int_of_integer e)) (man_exp_of_double x)
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_option (\<lambda>(m, e). Float (int_of_integer m) (int_of_integer e)) (man_exp_of_double x) = Float_of_double x
[PROOF STEP]
by transfer (auto simp: man_exp_of_double_def Let_def mantissa_exponent[symmetric]
      Float_mantissa_exponent)


[STATEMENT]
lemma compute_double_of_Float[code]:
  "double_of_Float f = double_of_man_exp (integer_of_int (mantissa f)) (integer_of_int (Float.exponent f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. double_of_Float f = double_of_man_exp (integer_of_int (mantissa f)) (integer_of_int (Float.exponent f))
[PROOF STEP]
unfolding double_of_man_exp_def Let_def Float_mantissa_exponent int_of_integer_integer_of_int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. double_of_Float f = (if is_finite_Float TYPE((11, 52) IEEE.float) f then Some (Double.of_finite_Float f) else None)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. is_finite_Float TYPE((11, 52) IEEE.float) f \<Longrightarrow> double_of_Float f = Some (Double.of_finite_Float f)
 2. \<not> is_finite_Float TYPE((11, 52) IEEE.float) f \<Longrightarrow> double_of_Float f = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_finite_Float TYPE((11, 52) IEEE.float) f \<Longrightarrow> double_of_Float f = Some (Double.of_finite_Float f)
[PROOF STEP]
by transfer auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_finite_Float TYPE((11, 52) IEEE.float) f \<Longrightarrow> double_of_Float f = None
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_finite_Float TYPE((11, 52) IEEE.float) f \<Longrightarrow> double_of_Float f = None
[PROOF STEP]
by transfer auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "check_conversions 100 100"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_conversions 100 100
[PROOF STEP]
by eval


[STATEMENT]
lemma times_scalar_id: "times id v = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.times id v = v
[PROOF STEP]
by(induction v)(auto simp add:left_id)


[STATEMENT]
lemma times_vector_id: "times v [id] = [v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.times v [id] = [v]
[PROOF STEP]
by(simp add:right_id)


[STATEMENT]
lemma preserving_length: "length (times n y) = (length y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (local.times n y) = length y
[PROOF STEP]
by(induction y)(auto)


[STATEMENT]
lemma vec_vec_Tensor_left_id: "vec_vec_Tensor [id] v = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor [id] v = v
[PROOF STEP]
by(induction v)(auto simp add:left_id)


[STATEMENT]
lemma vec_vec_Tensor_right_id: "vec_vec_Tensor v [id] = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor v [id] = v
[PROOF STEP]
by(induction v)(auto simp add:right_id)


[STATEMENT]
theorem vec_vec_Tensor_length :
 "(length(vec_vec_Tensor x y)) = (length x)*(length y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec_vec_Tensor x y) = length x * length y
[PROOF STEP]
by(induction x)(auto simp add: preserving_length)


[STATEMENT]
theorem vec_length: assumes "vec m x" and "vec n y"
shows "vec (m*n) (vec_vec_Tensor x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec (m * n) (vec_vec_Tensor x y)
[PROOF STEP]
apply(simp add:vec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec_vec_Tensor x y) = m * n
[PROOF STEP]
apply(simp add:vec_vec_Tensor_length)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length x * length y = m * n
[PROOF STEP]
apply (metis assms(1) assms(2) vec_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma vec_mat_Tensor_vector_id: "vec_mat_Tensor [id] v = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_mat_Tensor [id] v = v
[PROOF STEP]
by(induction v)(auto simp add: times_scalar_id)


[STATEMENT]
lemma vec_mat_Tensor_matrix_id: "vec_mat_Tensor  v [[id]] = [v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_mat_Tensor v [[id]] = [v]
[PROOF STEP]
by(induction v)(auto simp add: right_id)


[STATEMENT]
theorem vec_mat_Tensor_length:
 "length(vec_mat_Tensor xs ys) = length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec_mat_Tensor xs ys) = length ys
[PROOF STEP]
by(induction ys)(auto)


[STATEMENT]
theorem length_matrix:
 assumes "mat nr nc (y#ys)" and "length v = k"
     and "(vec_mat_Tensor v (y#ys) = x#xs)"
 shows "(vec (nr*k) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
have "vec_mat_Tensor v (y#ys) = (vec_vec_Tensor v y)#(vec_mat_Tensor v ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_mat_Tensor v (y # ys) = vec_vec_Tensor v y # vec_mat_Tensor v ys
[PROOF STEP]
using vec_mat_Tensor_def assms
[PROOF STATE]
proof (prove)
using this:
vec_mat_Tensor \<equiv> \<lambda>uu uua. rec_list (\<lambda>xs. []) (\<lambda>ys yss yssa xs. vec_vec_Tensor xs ys # yssa xs) uua uu
mat nr nc (y # ys)
length v = k
vec_mat_Tensor v (y # ys) = x # xs

goal (1 subgoal):
 1. vec_mat_Tensor v (y # ys) = vec_vec_Tensor v y # vec_mat_Tensor v ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_mat_Tensor v (y # ys) = vec_vec_Tensor v y # vec_mat_Tensor v ys

goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec_mat_Tensor v (y # ys) = vec_vec_Tensor v y # vec_mat_Tensor v ys

goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
have "(vec_vec_Tensor v y) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_vec_Tensor v y = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat nr nc (y # ys)
length v = k
vec_mat_Tensor v (y # ys) = x # xs

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

goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec_vec_Tensor v y = x

goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
have "length y = nr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length y = nr
[PROOF STEP]
using assms mat_def
[PROOF STATE]
proof (prove)
using this:
mat nr nc (y # ys)
length v = k
vec_mat_Tensor v (y # ys) = x # xs
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))

goal (1 subgoal):
 1. length y = nr
[PROOF STEP]
by (metis in_set_member member_rec(1) vec_def)
[PROOF STATE]
proof (state)
this:
length y = nr

goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
length y = nr
[PROOF STEP]
have "length (vec_vec_Tensor v y) = nr*k"
[PROOF STATE]
proof (prove)
using this:
length y = nr

goal (1 subgoal):
 1. length (vec_vec_Tensor v y) = nr * k
[PROOF STEP]
using assms vec_vec_Tensor_length
[PROOF STATE]
proof (prove)
using this:
length y = nr
mat nr nc (y # ys)
length v = k
vec_mat_Tensor v (y # ys) = x # xs
length (vec_vec_Tensor ?x ?y) = length ?x * length ?y

goal (1 subgoal):
 1. length (vec_vec_Tensor v y) = nr * k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (vec_vec_Tensor v y) = nr * k

goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
length (vec_vec_Tensor v y) = nr * k
[PROOF STEP]
have "length x = nr*k"
[PROOF STATE]
proof (prove)
using this:
length (vec_vec_Tensor v y) = nr * k

goal (1 subgoal):
 1. length x = nr * k
[PROOF STEP]
by (simp add: \<open>vec_vec_Tensor v y = x\<close>)
[PROOF STATE]
proof (state)
this:
length x = nr * k

goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
length x = nr * k
[PROOF STEP]
have "vec (nr*k) x"
[PROOF STATE]
proof (prove)
using this:
length x = nr * k

goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
using vec_def
[PROOF STATE]
proof (prove)
using this:
length x = nr * k
vec ?n ?x = (length ?x = ?n)

goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec (nr * k) x

goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vec (nr * k) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vec (nr * k) x

goal (1 subgoal):
 1. vec (nr * k) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec (nr * k) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_set_list:
 assumes "mat nr nc M"
     and "length v = k"
     and " x \<in> set M"
 shows "\<exists>ys.\<exists>zs.(ys@x#zs = M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ys zs. ys @ x # zs = M
[PROOF STEP]
using assms set_def in_set_conv_decomp
[PROOF STATE]
proof (prove)
using this:
mat nr nc M
length v = k
x \<in> set M
set \<equiv> ctor_fold_list (\<lambda>z. set1_pre_list z \<union> \<Union> (set2_pre_list z))
(?x \<in> set ?xs) = (\<exists>ys zs. ?xs = ys @ ?x # zs)

goal (1 subgoal):
 1. \<exists>ys zs. ys @ x # zs = M
[PROOF STEP]
by metis


[STATEMENT]
lemma length_reduct:
 assumes "m \<noteq> []"
 shows "length (reduct m) +1  = (length m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (reduct m) + 1 = length m
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (length (reduct m)) = length m
[PROOF STEP]
by (metis One_nat_def Suc_eq_plus1 assms list.size(4) neq_Nil_conv reduct.simps(2))


[STATEMENT]
lemma mat_empty_column_length: assumes "mat nr nc M" and "M = []"
shows "nc = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nc = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nc = 0
[PROOF STEP]
have "(length M = nc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length M = nc
[PROOF STEP]
using mat_def assms
[PROOF STATE]
proof (prove)
using this:
mat ?nr ?nc ?m = (length ?m = ?nc \<and> Ball (set ?m) (vec ?nr))
mat nr nc M
M = []

goal (1 subgoal):
 1. length M = nc
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length M = nc

goal (1 subgoal):
 1. nc = 0
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
length M = nc
[PROOF STEP]
have "nc = 0"
[PROOF STATE]
proof (prove)
using this:
length M = nc

goal (1 subgoal):
 1. nc = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length M = nc
mat nr nc M
M = []

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

goal (1 subgoal):
 1. nc = 0
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
nc = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nc = 0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_uniqueness:
 assumes "vec m v"
     and "vec n v"
 shows "m = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m = n
[PROOF STEP]
using vec_def assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
vec ?n ?x = (length ?x = ?n)
vec m v
vec n v

goal (1 subgoal):
 1. m = n
[PROOF STEP]
by metis