[STATEMENT]
lemma ordering_INTER_0:
"\<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk>
 \<Longrightarrow> ordering (\<Inter>n. A n) 0 = oLimit (\<lambda>n. ordering (A n) 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (\<Inter> (range A)) 0 = oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0)
[PROOF STEP]
apply (subst ordering_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> (LEAST z. z \<in> \<Inter> (range A)) = oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0)
[PROOF STEP]
apply (rule Least_equality)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0) \<in> \<Inter> (range A)
 2. \<And>y. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; y \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0) \<le> y
[PROOF STEP]
apply (rule oLimit_mem_INTER, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> \<forall>n. OrdinalVeblen.ordering (A n) 0 \<in> A n
 2. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> mono (\<lambda>n. OrdinalVeblen.ordering (A n) 0)
 3. \<And>y. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; y \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0) \<le> y
[PROOF STEP]
apply (simp add: normal_set.ordering_mem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> mono (\<lambda>n. OrdinalVeblen.ordering (A n) 0)
 2. \<And>y. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; y \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0) \<le> y
[PROOF STEP]
apply (rule mono_natI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (A n) 0 \<le> OrdinalVeblen.ordering (A (Suc n)) 0
 2. \<And>y. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; y \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0) \<le> y
[PROOF STEP]
apply (simp add: ordering_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> (LEAST z. z \<in> A n) \<le> (LEAST z. z \<in> A (Suc n))
 2. \<And>y. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; y \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0) \<le> y
[PROOF STEP]
apply (rule Least_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> (LEAST z. z \<in> A (Suc n)) \<in> A n
 2. \<And>y. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; y \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0) \<le> y
[PROOF STEP]
apply (rule subsetD, erule spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> (LEAST z. z \<in> A (Suc n)) \<in> A (Suc n)
 2. \<And>y. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; y \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0) \<le> y
[PROOF STEP]
apply (drule_tac x="Suc n" in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n. A (Suc n) \<subseteq> A n; normal_set (A (Suc n))\<rbrakk> \<Longrightarrow> (LEAST z. z \<in> A (Suc n)) \<in> A (Suc n)
 2. \<And>y. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; y \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0) \<le> y
[PROOF STEP]
apply (drule normal_set.unbounded, clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n y. \<lbrakk>\<forall>n. A (Suc n) \<subseteq> A n; y \<in> A (Suc n); ?x18 n < y\<rbrakk> \<Longrightarrow> (LEAST z. z \<in> A (Suc n)) \<in> A (Suc n)
 2. \<And>y. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; y \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0) \<le> y
[PROOF STEP]
apply (erule LeastI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; y \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (A n) 0) \<le> y
[PROOF STEP]
apply (rule oLimit_leI[rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; y \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (A n) 0 \<le> y
[PROOF STEP]
apply (simp add: ordering_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>x. y \<in> A x\<rbrakk> \<Longrightarrow> (LEAST z. z \<in> A n) \<le> y
[PROOF STEP]
apply (rule Least_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>x. y \<in> A x\<rbrakk> \<Longrightarrow> y \<in> A n
[PROOF STEP]
apply (erule spec)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma critical_set_0:
"critical_set A 0 = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. critical_set A 0 = A
[PROOF STEP]
by (unfold critical_set_def, rule ordinal_rec0_0)


[STATEMENT]
lemma critical_set_oSuc_lemma:
"critical_set A (oSuc n) =
  critical_set A n \<inter> range (oDeriv (ordering (critical_set A n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. critical_set A (oSuc n) = critical_set A n \<inter> range (oDeriv (OrdinalVeblen.ordering (critical_set A n)))
[PROOF STEP]
by (unfold critical_set_def, rule ordinal_rec0_oSuc)


[STATEMENT]
lemma omega_complete_INTER:
"omega_complete (\<lambda>x y. y \<subseteq> x) (\<lambda>f. \<Inter> (range f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. omega_complete (\<lambda>x y. y \<subseteq> x) (\<lambda>f. \<Inter> (range f))
[PROOF STEP]
apply (rule omega_complete.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. porder (\<lambda>x y. y \<subseteq> x)
 2. omega_complete_axioms (\<lambda>x y. y \<subseteq> x) (\<lambda>f. \<Inter> (range f))
[PROOF STEP]
apply (rule porder.flip)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. porder (\<subseteq>)
 2. omega_complete_axioms (\<lambda>x y. y \<subseteq> x) (\<lambda>f. \<Inter> (range f))
[PROOF STEP]
apply (rule porder_order)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. omega_complete_axioms (\<lambda>x y. y \<subseteq> x) (\<lambda>f. \<Inter> (range f))
[PROOF STEP]
apply (rule omega_complete_axioms.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f n. \<Inter> (range f) \<subseteq> f n
 2. \<And>f x. \<forall>n. x \<subseteq> f n \<Longrightarrow> x \<subseteq> \<Inter> (range f)
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. \<forall>n. x \<subseteq> f n \<Longrightarrow> x \<subseteq> \<Inter> (range f)
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma critical_set_oLimit:
"critical_set A (oLimit f) = (\<Inter>n. critical_set A (f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. critical_set A (oLimit f) = (\<Inter>n. critical_set A (f n))
[PROOF STEP]
apply (unfold critical_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_rec0 A (\<lambda>p x. x \<inter> range (oDeriv (OrdinalVeblen.ordering x))) (\<lambda>f. \<Inter> (range f)) (oLimit f) = (\<Inter>n. ordinal_rec0 A (\<lambda>p x. x \<inter> range (oDeriv (OrdinalVeblen.ordering x))) (\<lambda>f. \<Inter> (range f)) (f n))
[PROOF STEP]
apply (rule omega_complete.ordinal_rec0_oLimit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. omega_complete ?le (\<lambda>f. \<Inter> (range f))
 2. \<forall>p x. ?le x (x \<inter> range (oDeriv (OrdinalVeblen.ordering x)))
[PROOF STEP]
apply (rule omega_complete_INTER)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p x. x \<inter> range (oDeriv (OrdinalVeblen.ordering x)) \<subseteq> x
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma critical_set_mono:
"x \<le> y \<Longrightarrow> critical_set A y \<subseteq> critical_set A x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> critical_set A y \<subseteq> critical_set A x
[PROOF STEP]
apply (unfold critical_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> ordinal_rec0 A (\<lambda>p x. x \<inter> range (oDeriv (OrdinalVeblen.ordering x))) (\<lambda>f. \<Inter> (range f)) y \<subseteq> ordinal_rec0 A (\<lambda>p x. x \<inter> range (oDeriv (OrdinalVeblen.ordering x))) (\<lambda>f. \<Inter> (range f)) x
[PROOF STEP]
apply (rule omega_complete.ordinal_rec0_mono
          [OF omega_complete_INTER])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> \<forall>p x. x \<inter> range (oDeriv (OrdinalVeblen.ordering x)) \<subseteq> x
 2. x \<le> y \<Longrightarrow> x \<le> y
[PROOF STEP]
apply fast
[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 normal_set) range_oDeriv_subset:
"range (oDeriv (ordering A)) \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (oDeriv (OrdinalVeblen.ordering A)) \<subseteq> A
[PROOF STEP]
apply (clarsimp, rename_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. oDeriv (OrdinalVeblen.ordering A) x \<in> A
[PROOF STEP]
apply (cut_tac n=x in oDeriv_fixed[OF normal_ordering])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. OrdinalVeblen.ordering A (oDeriv (OrdinalVeblen.ordering A) x) = oDeriv (OrdinalVeblen.ordering A) x \<Longrightarrow> oDeriv (OrdinalVeblen.ordering A) x \<in> A
[PROOF STEP]
apply (erule subst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. OrdinalVeblen.ordering A (oDeriv (OrdinalVeblen.ordering A) x) \<in> A
[PROOF STEP]
apply (rule ordering_mem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma normal_set_critical_set:
"normal_set A \<Longrightarrow> normal_set (critical_set A x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_set A \<Longrightarrow> normal_set (critical_set A x)
[PROOF STEP]
apply (rule_tac a=x in oLimit_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. normal_set A \<Longrightarrow> normal_set (critical_set A 0)
 2. \<And>x. \<lbrakk>normal_set A; normal_set (critical_set A x)\<rbrakk> \<Longrightarrow> normal_set (critical_set A (oSuc x))
 3. \<And>f. \<lbrakk>normal_set A; OrdinalInduct.strict_mono f; \<forall>n. normal_set (critical_set A (f n))\<rbrakk> \<Longrightarrow> normal_set (critical_set A (oLimit f))
[PROOF STEP]
apply (simp only: critical_set_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>normal_set A; normal_set (critical_set A x)\<rbrakk> \<Longrightarrow> normal_set (critical_set A (oSuc x))
 2. \<And>f. \<lbrakk>normal_set A; OrdinalInduct.strict_mono f; \<forall>n. normal_set (critical_set A (f n))\<rbrakk> \<Longrightarrow> normal_set (critical_set A (oLimit f))
[PROOF STEP]
apply (simp only: critical_set_oSuc_lemma)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>normal_set A; normal_set (critical_set A x)\<rbrakk> \<Longrightarrow> normal_set (critical_set A x \<inter> range (oDeriv (OrdinalVeblen.ordering (critical_set A x))))
 2. \<And>f. \<lbrakk>normal_set A; OrdinalInduct.strict_mono f; \<forall>n. normal_set (critical_set A (f n))\<rbrakk> \<Longrightarrow> normal_set (critical_set A (oLimit f))
[PROOF STEP]
apply (subst Int_absorb1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>normal_set A; normal_set (critical_set A x)\<rbrakk> \<Longrightarrow> range (oDeriv (OrdinalVeblen.ordering (critical_set A x))) \<subseteq> critical_set A x
 2. \<And>x. \<lbrakk>normal_set A; normal_set (critical_set A x)\<rbrakk> \<Longrightarrow> normal_set (range (oDeriv (OrdinalVeblen.ordering (critical_set A x))))
 3. \<And>f. \<lbrakk>normal_set A; OrdinalInduct.strict_mono f; \<forall>n. normal_set (critical_set A (f n))\<rbrakk> \<Longrightarrow> normal_set (critical_set A (oLimit f))
[PROOF STEP]
apply (erule normal_set.range_oDeriv_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>normal_set A; normal_set (critical_set A x)\<rbrakk> \<Longrightarrow> normal_set (range (oDeriv (OrdinalVeblen.ordering (critical_set A x))))
 2. \<And>f. \<lbrakk>normal_set A; OrdinalInduct.strict_mono f; \<forall>n. normal_set (critical_set A (f n))\<rbrakk> \<Longrightarrow> normal_set (critical_set A (oLimit f))
[PROOF STEP]
apply (rule normal.normal_set_range)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>normal_set A; normal_set (critical_set A x)\<rbrakk> \<Longrightarrow> normal (oDeriv (OrdinalVeblen.ordering (critical_set A x)))
 2. \<And>f. \<lbrakk>normal_set A; OrdinalInduct.strict_mono f; \<forall>n. normal_set (critical_set A (f n))\<rbrakk> \<Longrightarrow> normal_set (critical_set A (oLimit f))
[PROOF STEP]
apply (rule normal_oDeriv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>normal_set A; OrdinalInduct.strict_mono f; \<forall>n. normal_set (critical_set A (f n))\<rbrakk> \<Longrightarrow> normal_set (critical_set A (oLimit f))
[PROOF STEP]
apply (simp only: critical_set_oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>normal_set A; OrdinalInduct.strict_mono f; \<forall>n. normal_set (critical_set A (f n))\<rbrakk> \<Longrightarrow> normal_set (\<Inter>n. critical_set A (f n))
[PROOF STEP]
apply (erule normal_set_INTER)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>normal_set A; OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> \<forall>n. critical_set A (f (Suc n)) \<subseteq> critical_set A (f n)
[PROOF STEP]
apply (rule allI, rule critical_set_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f n. \<lbrakk>normal_set A; OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> f n \<le> f (Suc n)
[PROOF STEP]
apply (simp add: strict_mono_monoD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma critical_set_oSuc:
"normal_set A
 \<Longrightarrow> critical_set A (oSuc x) = range (oDeriv (ordering (critical_set A x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_set A \<Longrightarrow> critical_set A (oSuc x) = range (oDeriv (OrdinalVeblen.ordering (critical_set A x)))
[PROOF STEP]
apply (simp only: critical_set_oSuc_lemma)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_set A \<Longrightarrow> critical_set A x \<inter> range (oDeriv (OrdinalVeblen.ordering (critical_set A x))) = range (oDeriv (OrdinalVeblen.ordering (critical_set A x)))
[PROOF STEP]
apply (rule Int_absorb1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_set A \<Longrightarrow> range (oDeriv (OrdinalVeblen.ordering (critical_set A x))) \<subseteq> critical_set A x
[PROOF STEP]
apply (rule normal_set.range_oDeriv_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_set A \<Longrightarrow> normal_set (critical_set A x)
[PROOF STEP]
apply (erule normal_set_critical_set)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) oVeblen_0: "oVeblen F 0 = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oVeblen F 0 = F
[PROOF STEP]
apply (unfold oVeblen_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalVeblen.ordering (critical_set (range F) 0) = F
[PROOF STEP]
apply (subst critical_set_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalVeblen.ordering (range F) = F
[PROOF STEP]
apply (rule ordering_range)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) oVeblen_oSuc:
"oVeblen F (oSuc x) = oDeriv (oVeblen F x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oVeblen F (oSuc x) = oDeriv (oVeblen F x)
[PROOF STEP]
apply (unfold oVeblen_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalVeblen.ordering (critical_set (range F) (oSuc x)) = oDeriv (OrdinalVeblen.ordering (critical_set (range F) x))
[PROOF STEP]
apply (subst critical_set_oSuc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. normal_set (range F)
 2. OrdinalVeblen.ordering (range (oDeriv (OrdinalVeblen.ordering (critical_set (range F) x)))) = oDeriv (OrdinalVeblen.ordering (critical_set (range F) x))
[PROOF STEP]
apply (rule normal_set_range)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalVeblen.ordering (range (oDeriv (OrdinalVeblen.ordering (critical_set (range F) x)))) = oDeriv (OrdinalVeblen.ordering (critical_set (range F) x))
[PROOF STEP]
apply (rule normal.ordering_range)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal (oDeriv (OrdinalVeblen.ordering (critical_set (range F) x)))
[PROOF STEP]
apply (rule normal_oDeriv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) oVeblen_oLimit:
"oVeblen F (oLimit f) = ordering (\<Inter>n. range (oVeblen F (f n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oVeblen F (oLimit f) = OrdinalVeblen.ordering (\<Inter>n. range (oVeblen F (f n)))
[PROOF STEP]
apply (unfold oVeblen_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalVeblen.ordering (critical_set (range F) (oLimit f)) = OrdinalVeblen.ordering (\<Inter>n. range (OrdinalVeblen.ordering (critical_set (range F) (f n))))
[PROOF STEP]
apply (subst critical_set_oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalVeblen.ordering (\<Inter>n. critical_set (range F) (f n)) = OrdinalVeblen.ordering (\<Inter>n. range (OrdinalVeblen.ordering (critical_set (range F) (f n))))
[PROOF STEP]
apply (cut_tac normal_set_range)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_set (range F) \<Longrightarrow> OrdinalVeblen.ordering (\<Inter>n. critical_set (range F) (f n)) = OrdinalVeblen.ordering (\<Inter>n. range (OrdinalVeblen.ordering (critical_set (range F) (f n))))
[PROOF STEP]
apply (simp add: normal_set.range_ordering[OF normal_set_critical_set])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) normal_oVeblen:
"normal (oVeblen F x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal (oVeblen F x)
[PROOF STEP]
apply (unfold oVeblen_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal (OrdinalVeblen.ordering (critical_set (range F) x))
[PROOF STEP]
apply (rule normal_set.normal_ordering)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_set (critical_set (range F) x)
[PROOF STEP]
apply (rule normal_set_critical_set)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_set (range F)
[PROOF STEP]
apply (rule normal_set_range)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) continuous_oVeblen_0:
"continuous (\<lambda>x. oVeblen F x 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (\<lambda>x. oVeblen F x 0)
[PROOF STEP]
apply (rule continuousI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. OrdinalInduct.strict_mono f \<Longrightarrow> oVeblen F (oLimit f) 0 = oLimit (\<lambda>n. oVeblen F (f n) 0)
 2. \<And>x. oVeblen F x 0 \<le> oVeblen F (oSuc x) 0
[PROOF STEP]
apply (simp add: oVeblen_def critical_set_oLimit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. OrdinalInduct.strict_mono f \<Longrightarrow> OrdinalVeblen.ordering (\<Inter>n. critical_set (range F) (f n)) 0 = oLimit (\<lambda>n. OrdinalVeblen.ordering (critical_set (range F) (f n)) 0)
 2. \<And>x. oVeblen F x 0 \<le> oVeblen F (oSuc x) 0
[PROOF STEP]
apply (rule ordering_INTER_0[rule_format])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f n. OrdinalInduct.strict_mono f \<Longrightarrow> normal_set (critical_set (range F) (f n))
 2. \<And>f n. OrdinalInduct.strict_mono f \<Longrightarrow> critical_set (range F) (f (Suc n)) \<subseteq> critical_set (range F) (f n)
 3. \<And>x. oVeblen F x 0 \<le> oVeblen F (oSuc x) 0
[PROOF STEP]
apply (rule normal_set_critical_set)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f n. OrdinalInduct.strict_mono f \<Longrightarrow> normal_set (range F)
 2. \<And>f n. OrdinalInduct.strict_mono f \<Longrightarrow> critical_set (range F) (f (Suc n)) \<subseteq> critical_set (range F) (f n)
 3. \<And>x. oVeblen F x 0 \<le> oVeblen F (oSuc x) 0
[PROOF STEP]
apply (rule normal_set_range)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f n. OrdinalInduct.strict_mono f \<Longrightarrow> critical_set (range F) (f (Suc n)) \<subseteq> critical_set (range F) (f n)
 2. \<And>x. oVeblen F x 0 \<le> oVeblen F (oSuc x) 0
[PROOF STEP]
apply (rule critical_set_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f n. OrdinalInduct.strict_mono f \<Longrightarrow> f n \<le> f (Suc n)
 2. \<And>x. oVeblen F x 0 \<le> oVeblen F (oSuc x) 0
[PROOF STEP]
apply (simp add: strict_mono_monoD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. oVeblen F x 0 \<le> oVeblen F (oSuc x) 0
[PROOF STEP]
apply (simp only: oVeblen_oSuc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. oVeblen F x 0 \<le> oDeriv (oVeblen F x) 0
[PROOF STEP]
apply (rule oDeriv_increasing)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. continuous (oVeblen F x)
[PROOF STEP]
apply (rule normal.continuous)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. normal (oVeblen F x)
[PROOF STEP]
apply (rule normal_oVeblen)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) oVeblen_oLimit_0:
"oVeblen F (oLimit f) 0 = oLimit (\<lambda>n. oVeblen F (f n) 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oVeblen F (oLimit f) 0 = oLimit (\<lambda>n. oVeblen F (f n) 0)
[PROOF STEP]
by (rule continuousD[OF continuous_oVeblen_0])


[STATEMENT]
lemma (in normal) normal_oVeblen_0:
"0 < F 0 \<Longrightarrow> normal (\<lambda>x. oVeblen F x 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < F 0 \<Longrightarrow> normal (\<lambda>x. oVeblen F x 0)
[PROOF STEP]
apply (rule normalI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>0 < F 0; OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> oVeblen F (oLimit f) 0 = oLimit (\<lambda>n. oVeblen F (f n) 0)
 2. \<And>x. 0 < F 0 \<Longrightarrow> oVeblen F x 0 < oVeblen F (oSuc x) 0
[PROOF STEP]
apply (rule oVeblen_oLimit_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. 0 < F 0 \<Longrightarrow> oVeblen F x 0 < oVeblen F (oSuc x) 0
[PROOF STEP]
apply (simp only: oVeblen_oSuc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. 0 < F 0 \<Longrightarrow> oVeblen F x 0 < oDeriv (oVeblen F x) 0
[PROOF STEP]
apply (subst oDeriv_fixed[OF normal_oVeblen, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. 0 < F 0 \<Longrightarrow> oVeblen F x 0 < oVeblen F x (oDeriv (oVeblen F x) 0)
[PROOF STEP]
apply (rule normal.strict_monoD[OF normal_oVeblen])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. 0 < F 0 \<Longrightarrow> 0 < oDeriv (oVeblen F x) 0
[PROOF STEP]
apply (simp add: zero_less_oFix_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. 0 < F 0 \<Longrightarrow> 0 < oVeblen F x 0
[PROOF STEP]
apply (erule order_less_le_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. F 0 \<le> oVeblen F x 0
[PROOF STEP]
apply (subgoal_tac "oVeblen F 0 0 \<le> oVeblen F x 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. oVeblen F 0 0 \<le> oVeblen F x 0 \<Longrightarrow> F 0 \<le> oVeblen F x 0
 2. \<And>x. oVeblen F 0 0 \<le> oVeblen F x 0
[PROOF STEP]
apply (simp add: oVeblen_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. oVeblen F 0 0 \<le> oVeblen F x 0
[PROOF STEP]
apply (rule continuous.monoD[OF _ ordinal_0_le])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. continuous (\<lambda>a. oVeblen F a 0)
[PROOF STEP]
apply (rule continuous_oVeblen_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) range_oVeblen:
"range (oVeblen F x) = critical_set (range F) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (oVeblen F x) = critical_set (range F) x
[PROOF STEP]
apply (unfold oVeblen_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (OrdinalVeblen.ordering (critical_set (range F) x)) = critical_set (range F) x
[PROOF STEP]
apply (rule normal_set.range_ordering)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_set (critical_set (range F) x)
[PROOF STEP]
apply (rule normal_set_critical_set)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_set (range F)
[PROOF STEP]
apply (rule normal_set_range)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) range_oVeblen_subset:
"x \<le> y \<Longrightarrow> range (oVeblen F y) \<subseteq> range (oVeblen F x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> range (oVeblen F y) \<subseteq> range (oVeblen F x)
[PROOF STEP]
apply (simp only: range_oVeblen)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> critical_set (range F) y \<subseteq> critical_set (range F) x
[PROOF STEP]
apply (erule critical_set_mono)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) oVeblen_fixed:
"\<forall>x<y. \<forall>a. oVeblen F x (oVeblen F y a) = oVeblen F y a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x<y. \<forall>a. oVeblen F x (oVeblen F y a) = oVeblen F y a
[PROOF STEP]
apply (rule_tac a=y in oLimit_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>x<0. \<forall>a. oVeblen F x (oVeblen F 0 a) = oVeblen F 0 a
 2. \<And>x. \<forall>xa<x. \<forall>a. oVeblen F xa (oVeblen F x a) = oVeblen F x a \<Longrightarrow> \<forall>xa<oSuc x. \<forall>a. oVeblen F xa (oVeblen F (oSuc x) a) = oVeblen F (oSuc x) a
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a)\<rbrakk> \<Longrightarrow> \<forall>x<oLimit f. \<forall>a. oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>xa<x. \<forall>a. oVeblen F xa (oVeblen F x a) = oVeblen F x a \<Longrightarrow> \<forall>xa<oSuc x. \<forall>a. oVeblen F xa (oVeblen F (oSuc x) a) = oVeblen F (oSuc x) a
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a)\<rbrakk> \<Longrightarrow> \<forall>x<oLimit f. \<forall>a. oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply (clarsimp simp only: oVeblen_oSuc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa a. \<lbrakk>\<forall>xa<x. \<forall>a. oVeblen F xa (oVeblen F x a) = oVeblen F x a; xa < oSuc x\<rbrakk> \<Longrightarrow> oVeblen F xa (oDeriv (oVeblen F x) a) = oDeriv (oVeblen F x) a
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a)\<rbrakk> \<Longrightarrow> \<forall>x<oLimit f. \<forall>a. oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply (erule less_oSucE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa a. \<lbrakk>\<forall>xa<x. \<forall>a. oVeblen F xa (oVeblen F x a) = oVeblen F x a; xa < x\<rbrakk> \<Longrightarrow> oVeblen F xa (oDeriv (oVeblen F x) a) = oDeriv (oVeblen F x) a
 2. \<And>x xa a. \<lbrakk>\<forall>xa<x. \<forall>a. oVeblen F xa (oVeblen F x a) = oVeblen F x a; xa = x\<rbrakk> \<Longrightarrow> oVeblen F xa (oDeriv (oVeblen F x) a) = oDeriv (oVeblen F x) a
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a)\<rbrakk> \<Longrightarrow> \<forall>x<oLimit f. \<forall>a. oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply (drule spec, drule mp, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa a. \<lbrakk>xa < x; \<forall>a. oVeblen F xa (oVeblen F x a) = oVeblen F x a\<rbrakk> \<Longrightarrow> oVeblen F xa (oDeriv (oVeblen F x) a) = oDeriv (oVeblen F x) a
 2. \<And>x xa a. \<lbrakk>\<forall>xa<x. \<forall>a. oVeblen F xa (oVeblen F x a) = oVeblen F x a; xa = x\<rbrakk> \<Longrightarrow> oVeblen F xa (oDeriv (oVeblen F x) a) = oDeriv (oVeblen F x) a
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a)\<rbrakk> \<Longrightarrow> \<forall>x<oLimit f. \<forall>a. oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply (drule_tac x="oDeriv (oVeblen F x) a" in spec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa a. \<lbrakk>xa < x; oVeblen F xa (oVeblen F x (oDeriv (oVeblen F x) a)) = oVeblen F x (oDeriv (oVeblen F x) a)\<rbrakk> \<Longrightarrow> oVeblen F xa (oDeriv (oVeblen F x) a) = oDeriv (oVeblen F x) a
 2. \<And>x xa a. \<lbrakk>\<forall>xa<x. \<forall>a. oVeblen F xa (oVeblen F x a) = oVeblen F x a; xa = x\<rbrakk> \<Longrightarrow> oVeblen F xa (oDeriv (oVeblen F x) a) = oDeriv (oVeblen F x) a
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a)\<rbrakk> \<Longrightarrow> \<forall>x<oLimit f. \<forall>a. oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply (simp add: oDeriv_fixed normal_oVeblen)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa a. \<lbrakk>\<forall>xa<x. \<forall>a. oVeblen F xa (oVeblen F x a) = oVeblen F x a; xa = x\<rbrakk> \<Longrightarrow> oVeblen F xa (oDeriv (oVeblen F x) a) = oDeriv (oVeblen F x) a
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a)\<rbrakk> \<Longrightarrow> \<forall>x<oLimit f. \<forall>a. oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa a. \<lbrakk>\<forall>xa<x. \<forall>a. oVeblen F xa (oVeblen F x a) = oVeblen F x a; xa = x\<rbrakk> \<Longrightarrow> oVeblen F x (oDeriv (oVeblen F x) a) = oDeriv (oVeblen F x) a
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a)\<rbrakk> \<Longrightarrow> \<forall>x<oLimit f. \<forall>a. oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply (rule oDeriv_fixed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa a. \<lbrakk>\<forall>xa<x. \<forall>a. oVeblen F xa (oVeblen F x a) = oVeblen F x a; xa = x\<rbrakk> \<Longrightarrow> normal (oVeblen F x)
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a)\<rbrakk> \<Longrightarrow> \<forall>x<oLimit f. \<forall>a. oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply (rule normal_oVeblen)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a)\<rbrakk> \<Longrightarrow> \<forall>x<oLimit f. \<forall>a. oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x a. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a); x < oLimit f\<rbrakk> \<Longrightarrow> oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply (erule less_oLimitE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x a n. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n x. x < f n \<longrightarrow> (\<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a); x < f n\<rbrakk> \<Longrightarrow> oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply (drule spec, drule spec, drule mp, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x a n. \<lbrakk>OrdinalInduct.strict_mono f; x < f n; \<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a\<rbrakk> \<Longrightarrow> oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
[PROOF STEP]
apply (subgoal_tac "oVeblen F (oLimit f) a \<in> range (oVeblen F (f n))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x a n. \<lbrakk>OrdinalInduct.strict_mono f; x < f n; \<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a; oVeblen F (oLimit f) a \<in> range (oVeblen F (f n))\<rbrakk> \<Longrightarrow> oVeblen F x (oVeblen F (oLimit f) a) = oVeblen F (oLimit f) a
 2. \<And>f x a n. \<lbrakk>OrdinalInduct.strict_mono f; x < f n; \<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a\<rbrakk> \<Longrightarrow> oVeblen F (oLimit f) a \<in> range (oVeblen F (f n))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x a n. \<lbrakk>OrdinalInduct.strict_mono f; x < f n; \<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a\<rbrakk> \<Longrightarrow> oVeblen F (oLimit f) a \<in> range (oVeblen F (f n))
[PROOF STEP]
apply (rule_tac A="range (oVeblen F (oLimit f))" in subsetD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x a n. \<lbrakk>OrdinalInduct.strict_mono f; x < f n; \<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a\<rbrakk> \<Longrightarrow> range (oVeblen F (oLimit f)) \<subseteq> range (oVeblen F (f n))
 2. \<And>f x a n. \<lbrakk>OrdinalInduct.strict_mono f; x < f n; \<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a\<rbrakk> \<Longrightarrow> oVeblen F (oLimit f) a \<in> range (oVeblen F (oLimit f))
[PROOF STEP]
apply (rule range_oVeblen_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x a n. \<lbrakk>OrdinalInduct.strict_mono f; x < f n; \<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a\<rbrakk> \<Longrightarrow> f n \<le> oLimit f
 2. \<And>f x a n. \<lbrakk>OrdinalInduct.strict_mono f; x < f n; \<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a\<rbrakk> \<Longrightarrow> oVeblen F (oLimit f) a \<in> range (oVeblen F (oLimit f))
[PROOF STEP]
apply (rule le_oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x a n. \<lbrakk>OrdinalInduct.strict_mono f; x < f n; \<forall>a. oVeblen F x (oVeblen F (f n) a) = oVeblen F (f n) a\<rbrakk> \<Longrightarrow> oVeblen F (oLimit f) a \<in> range (oVeblen F (oLimit f))
[PROOF STEP]
apply (rule rangeI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) critical_set_fixed:
"0 < z \<Longrightarrow> range (oVeblen F z) = {x. \<forall>y<z. oVeblen F y x = x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < z \<Longrightarrow> range (oVeblen F z) = {x. \<forall>y<z. oVeblen F y x = x}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < z \<Longrightarrow> range (oVeblen F z) \<subseteq> {x. \<forall>y<z. oVeblen F y x = x}
 2. 0 < z \<Longrightarrow> {x. \<forall>y<z. oVeblen F y x = x} \<subseteq> range (oVeblen F z)
[PROOF STEP]
apply (clarsimp simp add: oVeblen_fixed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < z \<Longrightarrow> {x. \<forall>y<z. oVeblen F y x = x} \<subseteq> range (oVeblen F z)
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < z \<longrightarrow> {x. \<forall>y<z. oVeblen F y x = x} \<subseteq> range (oVeblen F z)
[PROOF STEP]
apply (rule_tac a=z in oLimit_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 0 < 0 \<longrightarrow> {x. \<forall>y<0. oVeblen F y x = x} \<subseteq> range (oVeblen F 0)
 2. \<And>x. 0 < x \<longrightarrow> {xa. \<forall>y<x. oVeblen F y xa = xa} \<subseteq> range (oVeblen F x) \<Longrightarrow> 0 < oSuc x \<longrightarrow> {xa. \<forall>y<oSuc x. oVeblen F y xa = xa} \<subseteq> range (oVeblen F (oSuc x))
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> range (oVeblen F (f n))\<rbrakk> \<Longrightarrow> 0 < oLimit f \<longrightarrow> {x. \<forall>y<oLimit f. oVeblen F y x = x} \<subseteq> range (oVeblen F (oLimit f))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. 0 < x \<longrightarrow> {xa. \<forall>y<x. oVeblen F y xa = xa} \<subseteq> range (oVeblen F x) \<Longrightarrow> 0 < oSuc x \<longrightarrow> {xa. \<forall>y<oSuc x. oVeblen F y xa = xa} \<subseteq> range (oVeblen F (oSuc x))
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> range (oVeblen F (f n))\<rbrakk> \<Longrightarrow> 0 < oLimit f \<longrightarrow> {x. \<forall>y<oLimit f. oVeblen F y x = x} \<subseteq> range (oVeblen F (oLimit f))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>0 < x \<longrightarrow> {xa. \<forall>y<x. oVeblen F y xa = xa} \<subseteq> range (oVeblen F x); \<forall>y<oSuc x. oVeblen F y xa = xa\<rbrakk> \<Longrightarrow> xa \<in> range (oVeblen F (oSuc x))
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> range (oVeblen F (f n))\<rbrakk> \<Longrightarrow> 0 < oLimit f \<longrightarrow> {x. \<forall>y<oLimit f. oVeblen F y x = x} \<subseteq> range (oVeblen F (oLimit f))
[PROOF STEP]
apply (simp add: oVeblen_oSuc range_oDeriv normal_oVeblen)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> range (oVeblen F (f n))\<rbrakk> \<Longrightarrow> 0 < oLimit f \<longrightarrow> {x. \<forall>y<oLimit f. oVeblen F y x = x} \<subseteq> range (oVeblen F (oLimit f))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> range (oVeblen F (f n)); 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x\<rbrakk> \<Longrightarrow> x \<in> range (oVeblen F (oLimit f))
[PROOF STEP]
apply (simp add: range_oVeblen)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> critical_set (range F) (f n); 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x\<rbrakk> \<Longrightarrow> x \<in> critical_set (range F) (oLimit f)
[PROOF STEP]
apply (clarsimp simp add: critical_set_oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x xa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> critical_set (range F) (f n); 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x\<rbrakk> \<Longrightarrow> x \<in> critical_set (range F) (f xa)
[PROOF STEP]
apply (rule_tac A="critical_set (range F) (f (Suc xa))" in subsetD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x xa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> critical_set (range F) (f n); 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x\<rbrakk> \<Longrightarrow> critical_set (range F) (f (Suc xa)) \<subseteq> critical_set (range F) (f xa)
 2. \<And>f x xa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> critical_set (range F) (f n); 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x\<rbrakk> \<Longrightarrow> x \<in> critical_set (range F) (f (Suc xa))
[PROOF STEP]
apply (rule critical_set_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x xa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> critical_set (range F) (f n); 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x\<rbrakk> \<Longrightarrow> f xa \<le> f (Suc xa)
 2. \<And>f x xa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> critical_set (range F) (f n); 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x\<rbrakk> \<Longrightarrow> x \<in> critical_set (range F) (f (Suc xa))
[PROOF STEP]
apply (simp add: strict_mono_monoD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x xa. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. 0 < f n \<longrightarrow> {x. \<forall>y<f n. oVeblen F y x = x} \<subseteq> critical_set (range F) (f n); 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x\<rbrakk> \<Longrightarrow> x \<in> critical_set (range F) (f (Suc xa))
[PROOF STEP]
apply (drule_tac x="Suc xa" in spec, drule mp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x xa. \<lbrakk>OrdinalInduct.strict_mono f; 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x\<rbrakk> \<Longrightarrow> 0 < f (Suc xa)
 2. \<And>f x xa. \<lbrakk>OrdinalInduct.strict_mono f; 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x; {x. \<forall>y<f (Suc xa). oVeblen F y x = x} \<subseteq> critical_set (range F) (f (Suc xa))\<rbrakk> \<Longrightarrow> x \<in> critical_set (range F) (f (Suc xa))
[PROOF STEP]
apply (rule_tac y="f xa" in order_le_less_trans, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x xa. \<lbrakk>OrdinalInduct.strict_mono f; 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x\<rbrakk> \<Longrightarrow> f xa < f (Suc xa)
 2. \<And>f x xa. \<lbrakk>OrdinalInduct.strict_mono f; 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x; {x. \<forall>y<f (Suc xa). oVeblen F y x = x} \<subseteq> critical_set (range F) (f (Suc xa))\<rbrakk> \<Longrightarrow> x \<in> critical_set (range F) (f (Suc xa))
[PROOF STEP]
apply (erule OrdinalInduct.strict_monoD, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x xa. \<lbrakk>OrdinalInduct.strict_mono f; 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x; {x. \<forall>y<f (Suc xa). oVeblen F y x = x} \<subseteq> critical_set (range F) (f (Suc xa))\<rbrakk> \<Longrightarrow> x \<in> critical_set (range F) (f (Suc xa))
[PROOF STEP]
apply (erule subsetD, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x xa y. \<lbrakk>OrdinalInduct.strict_mono f; 0 < oLimit f; \<forall>y<oLimit f. oVeblen F y x = x; y < f (Suc xa)\<rbrakk> \<Longrightarrow> oVeblen F y x = x
[PROOF STEP]
apply (drule spec, erule mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x xa y. \<lbrakk>OrdinalInduct.strict_mono f; 0 < oLimit f; y < f (Suc xa)\<rbrakk> \<Longrightarrow> y < oLimit f
[PROOF STEP]
apply (erule order_less_le_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x xa y. \<lbrakk>OrdinalInduct.strict_mono f; 0 < oLimit f\<rbrakk> \<Longrightarrow> f (Suc xa) \<le> oLimit f
[PROOF STEP]
apply (rule le_oLimit)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oDeriv_id: "oDeriv id = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oDeriv id = id
[PROOF STEP]
apply (rule ext, rule_tac a=x in oLimit_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. oDeriv id 0 = id 0
 2. \<And>x xa. oDeriv id xa = id xa \<Longrightarrow> oDeriv id (oSuc xa) = id (oSuc xa)
 3. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. oDeriv id (f n) = id (f n)\<rbrakk> \<Longrightarrow> oDeriv id (oLimit f) = id (oLimit f)
[PROOF STEP]
apply (simp add: oFix_eq_self)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. oDeriv id xa = id xa \<Longrightarrow> oDeriv id (oSuc xa) = id (oSuc xa)
 2. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. oDeriv id (f n) = id (f n)\<rbrakk> \<Longrightarrow> oDeriv id (oLimit f) = id (oLimit f)
[PROOF STEP]
apply (simp add: oFix_eq_self)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. oDeriv id (f n) = id (f n)\<rbrakk> \<Longrightarrow> oDeriv id (oLimit f) = id (oLimit f)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oFix_plus: "oFix (\<lambda>x. a + x) 0 = a * \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oFix ((+) a) 0 = a * \<omega>
[PROOF STEP]
apply (simp add: oFix_def omega_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oLimit (\<lambda>n. iter n ((+) a) 0) = oLimit (\<lambda>n. a * ordinal_of_nat n)
[PROOF STEP]
apply (rule_tac f=oLimit in arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. iter n ((+) a) 0) = (\<lambda>n. a * ordinal_of_nat n)
[PROOF STEP]
apply (rule ext, induct_tac n, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. iter na ((+) a) 0 = a * ordinal_of_nat na \<Longrightarrow> iter (Suc na) ((+) a) 0 = a * ordinal_of_nat (Suc na)
[PROOF STEP]
apply (simp, rename_tac n)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. iter n ((+) a) 0 = a * ordinal_of_nat n \<Longrightarrow> a + a * ordinal_of_nat n = a * ordinal_of_nat n + a
[PROOF STEP]
apply (induct_tac n, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>iter n ((+) a) 0 = a * ordinal_of_nat n; a + a * ordinal_of_nat na = a * ordinal_of_nat na + a\<rbrakk> \<Longrightarrow> a + a * ordinal_of_nat (Suc na) = a * ordinal_of_nat (Suc na) + a
[PROOF STEP]
apply (simp add: ordinal_plus_assoc[symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oDeriv_plus: "oDeriv ((+) a) = ((+) (a * \<omega>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oDeriv ((+) a) = (+) (a * \<omega>)
[PROOF STEP]
apply (rule ext, rule_tac a=x in oLimit_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. oDeriv ((+) a) 0 = a * \<omega> + 0
 2. \<And>x xa. oDeriv ((+) a) xa = a * \<omega> + xa \<Longrightarrow> oDeriv ((+) a) (oSuc xa) = a * \<omega> + oSuc xa
 3. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. oDeriv ((+) a) (f n) = a * \<omega> + f n\<rbrakk> \<Longrightarrow> oDeriv ((+) a) (oLimit f) = a * \<omega> + oLimit f
[PROOF STEP]
apply (simp add: oFix_plus)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. oDeriv ((+) a) xa = a * \<omega> + xa \<Longrightarrow> oDeriv ((+) a) (oSuc xa) = a * \<omega> + oSuc xa
 2. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. oDeriv ((+) a) (f n) = a * \<omega> + f n\<rbrakk> \<Longrightarrow> oDeriv ((+) a) (oLimit f) = a * \<omega> + oLimit f
[PROOF STEP]
apply (simp add: oFix_eq_self
                   ordinal_plus_assoc[symmetric]
                   ordinal_plus_times_omega)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. oDeriv ((+) a) (f n) = a * \<omega> + f n\<rbrakk> \<Longrightarrow> oDeriv ((+) a) (oLimit f) = a * \<omega> + oLimit f
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oVeblen_1_plus: "oVeblen ((+) 1) x = ((+) (\<omega> ** x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oVeblen ((+) 1) x = (+) (\<omega> ** x)
[PROOF STEP]
apply (rule_tac a=x in wf_induct[OF wf], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>y<x. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y) \<Longrightarrow> oVeblen ((+) (oSuc 0)) x = (+) (\<omega> ** x)
[PROOF STEP]
apply (rule_tac a=x in ordinal_cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>y<x. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); x = 0\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) x = (+) (\<omega> ** x)
 2. \<And>x xa. \<lbrakk>\<forall>y<x. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); x = oSuc xa\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) x = (+) (\<omega> ** x)
 3. \<And>x f. \<lbrakk>\<forall>y<x. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; x = oLimit f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) x = (+) (\<omega> ** x)
[PROOF STEP]
apply (simp add: normal.oVeblen_0[OF normal_plus])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>y<x. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); x = oSuc xa\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) x = (+) (\<omega> ** x)
 2. \<And>x f. \<lbrakk>\<forall>y<x. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; x = oLimit f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) x = (+) (\<omega> ** x)
[PROOF STEP]
apply (simp add: normal.oVeblen_oSuc[OF normal_plus])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>y<oSuc xa. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); x = oSuc xa\<rbrakk> \<Longrightarrow> oDeriv ((+) (\<omega> ** xa)) = (+) (\<omega> ** xa * \<omega>)
 2. \<And>x f. \<lbrakk>\<forall>y<x. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; x = oLimit f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) x = (+) (\<omega> ** x)
[PROOF STEP]
apply (simp add: oDeriv_plus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>\<forall>y<x. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; x = oLimit f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) x = (+) (\<omega> ** x)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) (oLimit f) = (+) (oLimit (\<lambda>n. \<omega> ** f n))
[PROOF STEP]
apply (rule normal_range_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> normal (oVeblen ((+) (oSuc 0)) (oLimit f))
 2. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> normal ((+) (oLimit (\<lambda>n. \<omega> ** f n)))
 3. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> range (oVeblen ((+) (oSuc 0)) (oLimit f)) = range ((+) (oLimit (\<lambda>n. \<omega> ** f n)))
[PROOF STEP]
apply (rule normal.normal_oVeblen[OF normal_plus])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> normal ((+) (oLimit (\<lambda>n. \<omega> ** f n)))
 2. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> range (oVeblen ((+) (oSuc 0)) (oLimit f)) = range ((+) (oLimit (\<lambda>n. \<omega> ** f n)))
[PROOF STEP]
apply (rule normal_plus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> range (oVeblen ((+) (oSuc 0)) (oLimit f)) = range ((+) (oLimit (\<lambda>n. \<omega> ** f n)))
[PROOF STEP]
apply (subst normal.critical_set_fixed[OF normal_plus])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> 0 < oLimit f
 2. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> {x. \<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y x = x} = range ((+) (oLimit (\<lambda>n. \<omega> ** f n)))
[PROOF STEP]
apply (rule_tac y="f 0" in order_le_less_trans, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> f 0 < oLimit f
 2. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> {x. \<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y x = x} = range ((+) (oLimit (\<lambda>n. \<omega> ** f n)))
[PROOF STEP]
apply (simp add: strict_mono_less_oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f\<rbrakk> \<Longrightarrow> {x. \<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y x = x} = range ((+) (oLimit (\<lambda>n. \<omega> ** f n)))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; \<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y x = x\<rbrakk> \<Longrightarrow> x \<in> range ((+) (oLimit (\<lambda>n. \<omega> ** f n)))
 2. \<And>f x xa y. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; xa \<in> UNIV; y < oLimit f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) y (oLimit (\<lambda>n. \<omega> ** f n) + xa) = oLimit (\<lambda>n. \<omega> ** f n) + xa
[PROOF STEP]
apply (simp add: image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; \<forall>y<oLimit f. \<omega> ** y + x = x\<rbrakk> \<Longrightarrow> \<exists>xa. x = oLimit (\<lambda>n. \<omega> ** f n) + xa
 2. \<And>f x xa y. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; xa \<in> UNIV; y < oLimit f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) y (oLimit (\<lambda>n. \<omega> ** f n) + xa) = oLimit (\<lambda>n. \<omega> ** f n) + xa
[PROOF STEP]
apply (rule exI, rule ordinal_plus_minus2[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; \<forall>y<oLimit f. \<omega> ** y + x = x\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. \<omega> ** f n) \<le> x
 2. \<And>f x xa y. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; xa \<in> UNIV; y < oLimit f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) y (oLimit (\<lambda>n. \<omega> ** f n) + xa) = oLimit (\<lambda>n. \<omega> ** f n) + xa
[PROOF STEP]
apply (rule oLimit_leI[rule_format])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x n. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; \<forall>y<oLimit f. \<omega> ** y + x = x\<rbrakk> \<Longrightarrow> \<omega> ** f n \<le> x
 2. \<And>f x xa y. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; xa \<in> UNIV; y < oLimit f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) y (oLimit (\<lambda>n. \<omega> ** f n) + xa) = oLimit (\<lambda>n. \<omega> ** f n) + xa
[PROOF STEP]
apply (subgoal_tac "\<omega> ** f n + x = x", erule subst, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x n. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; \<forall>y<oLimit f. \<omega> ** y + x = x\<rbrakk> \<Longrightarrow> \<omega> ** f n + x = x
 2. \<And>f x xa y. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; xa \<in> UNIV; y < oLimit f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) y (oLimit (\<lambda>n. \<omega> ** f n) + xa) = oLimit (\<lambda>n. \<omega> ** f n) + xa
[PROOF STEP]
apply (drule_tac x="f n" in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f x n. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>y<oLimit f. \<omega> ** y + x = x; f n < oLimit f \<longrightarrow> oVeblen ((+) (oSuc 0)) (f n) = (+) (\<omega> ** f n)\<rbrakk> \<Longrightarrow> \<omega> ** f n + x = x
 2. \<And>f x xa y. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; xa \<in> UNIV; y < oLimit f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) y (oLimit (\<lambda>n. \<omega> ** f n) + xa) = oLimit (\<lambda>n. \<omega> ** f n) + xa
[PROOF STEP]
apply (simp add: strict_mono_less_oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x xa y. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; xa \<in> UNIV; y < oLimit f\<rbrakk> \<Longrightarrow> oVeblen ((+) (oSuc 0)) y (oLimit (\<lambda>n. \<omega> ** f n) + xa) = oLimit (\<lambda>n. \<omega> ** f n) + xa
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f xa y. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; y < oLimit f\<rbrakk> \<Longrightarrow> \<omega> ** y + (oLimit (\<lambda>n. \<omega> ** f n) + xa) = oLimit (\<lambda>n. \<omega> ** f n) + xa
[PROOF STEP]
apply (simp only: ordinal_exp_oLimit[symmetric] zero_less_omega)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f xa y. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; y < oLimit f\<rbrakk> \<Longrightarrow> \<omega> ** y + (\<omega> ** oLimit f + xa) = \<omega> ** oLimit f + xa
[PROOF STEP]
apply (simp only: ordinal_plus_assoc[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f xa y. \<lbrakk>\<forall>y<oLimit f. oVeblen ((+) (oSuc 0)) y = (+) (\<omega> ** y); OrdinalInduct.strict_mono f; y < oLimit f\<rbrakk> \<Longrightarrow> \<omega> ** y + \<omega> ** oLimit f + xa = \<omega> ** oLimit f + xa
[PROOF STEP]
apply (simp only: absorb_omega_exp2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prime_set_non_empty: "prime_set \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_set \<noteq> {}
[PROOF STEP]
using prime_set_gt_2
[PROOF STATE]
proof (prove)
using this:
2 < card prime_set

goal (1 subgoal):
 1. prime_set \<noteq> {}
[PROOF STEP]
by auto


[STATEMENT]
lemma coprime_set_non_empty:
  assumes "N > 2"
  shows "coprime_set N \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime_set N \<noteq> {}
[PROOF STEP]
by(simp add: coprime_set_def; metis assms(1) Suc_lessE coprime_Suc_right_nat lessI numeral_2_eq_2)


[STATEMENT]
lemma sample_coprime_e_gt_1:
  assumes "e \<in> set_spmf (sample_coprime N)"
  shows "e > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
e \<in> set_spmf (sample_coprime N)

goal (1 subgoal):
 1. 1 < e
[PROOF STEP]
by(simp add: sample_coprime_def coprime_set_def)


[STATEMENT]
lemma lossless_sample_coprime:
  assumes "\<not> prime N"
    and "N > 2"
  shows  "lossless_spmf (sample_coprime N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (sample_coprime N)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lossless_spmf (sample_coprime N)
[PROOF STEP]
have "coprime_set N \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime_set N \<noteq> {}
[PROOF STEP]
by(simp add: coprime_set_non_empty assms)
[PROOF STATE]
proof (state)
this:
coprime_set N \<noteq> {}

goal (1 subgoal):
 1. lossless_spmf (sample_coprime N)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coprime_set N \<noteq> {}

goal (1 subgoal):
 1. lossless_spmf (sample_coprime N)
[PROOF STEP]
have "finite (coprime_set N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (coprime_set N)
[PROOF STEP]
by(simp add: coprime_set_def)
[PROOF STATE]
proof (state)
this:
finite (coprime_set N)

goal (1 subgoal):
 1. lossless_spmf (sample_coprime N)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
coprime_set N \<noteq> {}
finite (coprime_set N)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
coprime_set N \<noteq> {}
finite (coprime_set N)

goal (1 subgoal):
 1. lossless_spmf (sample_coprime N)
[PROOF STEP]
by(simp add: sample_coprime_def)
[PROOF STATE]
proof (state)
this:
lossless_spmf (sample_coprime N)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_spmf_sample_coprime:
  shows "set_spmf (sample_coprime N) = {x. coprime x N \<and> x > 1 \<and> x < N}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_spmf (sample_coprime N) = {x. coprime x N \<and> 1 < x \<and> x < N}
[PROOF STEP]
by(simp add: sample_coprime_def coprime_set_def)


[STATEMENT]
lemma lossless_sample_primes:
  shows "lossless_spmf sample_primes"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf sample_primes
[PROOF STEP]
by(simp add: sample_primes_def prime_set_non_empty finite_prime_set)


[STATEMENT]
lemma set_spmf_sample_primes:
  shows "set_spmf sample_primes \<subseteq> {x. prime x \<and> x > 2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_spmf sample_primes \<subseteq> {x. prime x \<and> 2 < x}
[PROOF STEP]
by(auto simp add: sample_primes_def prime_set_ass finite_prime_set)


[STATEMENT]
lemma mem_samp_primes_gt_2:
  shows "x \<in> set_spmf sample_primes \<Longrightarrow> x > 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set_spmf sample_primes \<Longrightarrow> 2 < x
[PROOF STEP]
apply (simp add: finite_prime_set sample_primes_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> prime_set \<Longrightarrow> 2 < x
[PROOF STEP]
using prime_set_ass
[PROOF STATE]
proof (prove)
using this:
prime_set \<subseteq> {x. prime x \<and> 2 < x}

goal (1 subgoal):
 1. x \<in> prime_set \<Longrightarrow> 2 < x
[PROOF STEP]
by blast


[STATEMENT]
lemma mem_samp_primes_prime:
  shows "x \<in> set_spmf sample_primes \<Longrightarrow> prime x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set_spmf sample_primes \<Longrightarrow> prime x
[PROOF STEP]
apply (simp add: finite_prime_set sample_primes_def prime_set_ass)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> prime_set \<Longrightarrow> prime x
[PROOF STEP]
using prime_set_ass
[PROOF STATE]
proof (prove)
using this:
prime_set \<subseteq> {x. prime x \<and> 2 < x}

goal (1 subgoal):
 1. x \<in> prime_set \<Longrightarrow> prime x
[PROOF STEP]
by blast


[STATEMENT]
lemma lossless_sample_primes_excl:
  shows "lossless_spmf (sample_primes_excl {P})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (sample_primes_excl {P})
[PROOF STEP]
apply(simp add: sample_primes_excl_def finite_prime_set)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> prime_set \<subseteq> {P}
[PROOF STEP]
using prime_set_gt_2 subset_singletonD
[PROOF STATE]
proof (prove)
using this:
2 < card prime_set
?A \<subseteq> {?x} \<Longrightarrow> ?A = {} \<or> ?A = {?x}

goal (1 subgoal):
 1. \<not> prime_set \<subseteq> {P}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma set_spmf_sample_set_excl [simp]:
  assumes "finite (Q - P)"
  shows "set_spmf (sample_set_excl Q P) = (Q - P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_spmf (sample_set_excl Q P) = Q - P
[PROOF STEP]
unfolding  sample_set_excl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_spmf (spmf_of_set (Q - P)) = Q - P
[PROOF STEP]
by (metis set_spmf_of_set assms)+


[STATEMENT]
lemma lossless_sample_set_excl:
  assumes "finite Q"
    and "card Q > 2"
  shows "lossless_spmf (sample_set_excl Q {P})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (sample_set_excl Q {P})
[PROOF STEP]
unfolding sample_set_excl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (spmf_of_set (Q - {P}))
[PROOF STEP]
using assms subset_singletonD
[PROOF STATE]
proof (prove)
using this:
finite Q
2 < card Q
?A \<subseteq> {?x} \<Longrightarrow> ?A = {} \<or> ?A = {?x}

goal (1 subgoal):
 1. lossless_spmf (spmf_of_set (Q - {P}))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma mem_samp_primes_excl_gt_2:
  shows "x \<in> set_spmf (sample_set_excl prime_set {y}) \<Longrightarrow> x > 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set_spmf (sample_set_excl prime_set {y}) \<Longrightarrow> 2 < x
[PROOF STEP]
apply(simp add: finite_prime_set sample_set_excl_def  prime_set_ass )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> prime_set \<and> x \<noteq> y \<Longrightarrow> 2 < x
[PROOF STEP]
using prime_set_ass
[PROOF STATE]
proof (prove)
using this:
prime_set \<subseteq> {x. prime x \<and> 2 < x}

goal (1 subgoal):
 1. x \<in> prime_set \<and> x \<noteq> y \<Longrightarrow> 2 < x
[PROOF STEP]
by blast


[STATEMENT]
lemma mem_samp_primes_excl_prime :
  shows "x \<in> set_spmf (sample_set_excl prime_set {y}) \<Longrightarrow> prime x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set_spmf (sample_set_excl prime_set {y}) \<Longrightarrow> prime x
[PROOF STEP]
apply (simp add: finite_prime_set sample_set_excl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> prime_set \<and> x \<noteq> y \<Longrightarrow> prime x
[PROOF STEP]
using prime_set_ass
[PROOF STATE]
proof (prove)
using this:
prime_set \<subseteq> {x. prime x \<and> 2 < x}

goal (1 subgoal):
 1. x \<in> prime_set \<and> x \<noteq> y \<Longrightarrow> prime x
[PROOF STEP]
by blast


[STATEMENT]
lemma sample_coprime_lem:
  assumes "x \<in> set_spmf sample_primes"
    and " y \<in> set_spmf (sample_set_excl prime_set {x}) "
  shows "lossless_spmf (sample_coprime ((x - Suc 0) * (y - Suc 0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (sample_coprime ((x - Suc 0) * (y - Suc 0)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lossless_spmf (sample_coprime ((x - Suc 0) * (y - Suc 0)))
[PROOF STEP]
have gt_2: "x > 2" "y > 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 < x &&& 2 < y
[PROOF STEP]
using mem_samp_primes_gt_2 assms mem_samp_primes_excl_gt_2
[PROOF STATE]
proof (prove)
using this:
?x \<in> set_spmf sample_primes \<Longrightarrow> 2 < ?x
x \<in> set_spmf sample_primes
y \<in> set_spmf (sample_set_excl prime_set {x})
?x \<in> set_spmf (sample_set_excl prime_set {?y}) \<Longrightarrow> 2 < ?x

goal (1 subgoal):
 1. 2 < x &&& 2 < y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 < x
2 < y

goal (1 subgoal):
 1. lossless_spmf (sample_coprime ((x - Suc 0) * (y - Suc 0)))
[PROOF STEP]
have "\<not> prime ((x-1)*(y-1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> prime ((x - 1) * (y - 1))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> prime ((x - 1) * (y - 1))
[PROOF STEP]
have "prime x" "prime y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime x &&& prime y
[PROOF STEP]
using mem_samp_primes_prime mem_samp_primes_excl_prime assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> set_spmf sample_primes \<Longrightarrow> prime ?x
?x \<in> set_spmf (sample_set_excl prime_set {?y}) \<Longrightarrow> prime ?x
x \<in> set_spmf sample_primes
y \<in> set_spmf (sample_set_excl prime_set {x})

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

goal (1 subgoal):
 1. \<not> prime ((x - 1) * (y - 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prime x
prime y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime x
prime y

goal (1 subgoal):
 1. \<not> prime ((x - 1) * (y - 1))
[PROOF STEP]
using prod_not_prime gt_2
[PROOF STATE]
proof (prove)
using this:
prime x
prime y
\<lbrakk>prime ?x; prime ?y; 2 < ?x; 2 < ?y\<rbrakk> \<Longrightarrow> \<not> prime ((?x - 1) * (?y - 1))
2 < x
2 < y

goal (1 subgoal):
 1. \<not> prime ((x - 1) * (y - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> prime ((x - 1) * (y - 1))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> prime ((x - 1) * (y - 1))

goal (1 subgoal):
 1. lossless_spmf (sample_coprime ((x - Suc 0) * (y - Suc 0)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<not> prime ((x - 1) * (y - 1))

goal (1 subgoal):
 1. lossless_spmf (sample_coprime ((x - Suc 0) * (y - Suc 0)))
[PROOF STEP]
have "((x-1)*(y-1)) > 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 < (x - 1) * (y - 1)
[PROOF STEP]
by (metis (no_types, lifting) gt_2 One_nat_def Suc_diff_1 assms(1) assms(2) calculation
          divisors_zero less_2_cases nat_1_eq_mult_iff nat_neq_iff not_numeral_less_one numeral_2_eq_2
              prime_gt_0_nat rsa_base.mem_samp_primes_excl_prime rsa_base.mem_samp_primes_prime rsa_base_axioms two_is_prime_nat)
[PROOF STATE]
proof (state)
this:
2 < (x - 1) * (y - 1)

goal (1 subgoal):
 1. lossless_spmf (sample_coprime ((x - Suc 0) * (y - Suc 0)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> prime ((x - 1) * (y - 1))
2 < (x - 1) * (y - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> prime ((x - 1) * (y - 1))
2 < (x - 1) * (y - 1)

goal (1 subgoal):
 1. lossless_spmf (sample_coprime ((x - Suc 0) * (y - Suc 0)))
[PROOF STEP]
using lossless_sample_coprime
[PROOF STATE]
proof (prove)
using this:
\<not> prime ((x - 1) * (y - 1))
2 < (x - 1) * (y - 1)
\<lbrakk>\<not> prime ?N; 2 < ?N\<rbrakk> \<Longrightarrow> lossless_spmf (sample_coprime ?N)

goal (1 subgoal):
 1. lossless_spmf (sample_coprime ((x - Suc 0) * (y - Suc 0)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lossless_spmf (sample_coprime ((x - Suc 0) * (y - Suc 0)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lossless_I: "lossless_spmf I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf I
[PROOF STEP]
by(auto simp add: I_def lossless_sample_primes lossless_sample_set_excl finite_prime_set prime_set_gt_2 Let_def sample_coprime_lem)


[STATEMENT]
lemma set_spmf_I_N:
  assumes "((N,e),d) \<in> set_spmf I"
  obtains P Q where "N = P * Q"
    and "P \<noteq> Q"
    and "prime P"
    and "prime Q"
    and "coprime e ((P - 1)*(Q - 1))"
    and "d = nat (fst (bezw e ((P-1)*(Q-1))) mod int ((P-1)*(Q-1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>N = P * Q; P \<noteq> Q; prime P; prime Q; coprime e ((P - 1) * (Q - 1)); d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((N, e), d) \<in> set_spmf I

goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>N = P * Q; P \<noteq> Q; prime P; prime Q; coprime e ((P - 1) * (Q - 1)); d = nat (fst (bezw e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(auto simp add: I_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>P Q. \<lbrakk>x * xa = P * Q; P \<noteq> Q; prime P; prime Q; coprime e (P - Suc 0) \<and> coprime e (Q - Suc 0); nat (fst (bezw e ((x - Suc 0) * (xa - Suc 0))) mod (int (x - Suc 0) * int (xa - Suc 0))) = nat (fst (bezw e ((P - Suc 0) * (Q - Suc 0))) mod (int (P - Suc 0) * int (Q - Suc 0)))\<rbrakk> \<Longrightarrow> thesis; x \<in> set_spmf sample_primes; xa \<in> set_spmf (sample_set_excl prime_set {x}); N = x * xa; e \<in> set_spmf (sample_coprime ((x - Suc 0) * (xa - Suc 0))); d = nat (fst (bezw e ((x - Suc 0) * (xa - Suc 0))) mod (int (x - Suc 0) * int (xa - Suc 0)))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using finite_prime_set mem_samp_primes_prime sample_set_excl_def rsa_base_axioms sample_primes_def
[PROOF STATE]
proof (prove)
using this:
finite prime_set
?x \<in> set_spmf sample_primes \<Longrightarrow> prime ?x
sample_set_excl ?Q ?P = spmf_of_set (?Q - ?P)
rsa_base prime_set
sample_primes = spmf_of_set prime_set

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>P Q. \<lbrakk>x * xa = P * Q; P \<noteq> Q; prime P; prime Q; coprime e (P - Suc 0) \<and> coprime e (Q - Suc 0); nat (fst (bezw e ((x - Suc 0) * (xa - Suc 0))) mod (int (x - Suc 0) * int (xa - Suc 0))) = nat (fst (bezw e ((P - Suc 0) * (Q - Suc 0))) mod (int (P - Suc 0) * int (Q - Suc 0)))\<rbrakk> \<Longrightarrow> thesis; x \<in> set_spmf sample_primes; xa \<in> set_spmf (sample_set_excl prime_set {x}); N = x * xa; e \<in> set_spmf (sample_coprime ((x - Suc 0) * (xa - Suc 0))); d = nat (fst (bezw e ((x - Suc 0) * (xa - Suc 0))) mod (int (x - Suc 0) * int (xa - Suc 0)))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (simp add: set_spmf_sample_coprime)


[STATEMENT]
lemma set_spmf_I_e_d:
  assumes "((N,e),d) \<in> set_spmf I"
  shows "e > 1" and "d > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < e &&& 1 < d
[PROOF STEP]
using assms sample_coprime_e_gt_1
[PROOF STATE]
proof (prove)
using this:
((N, e), d) \<in> set_spmf I
?e \<in> set_spmf (sample_coprime ?N) \<Longrightarrow> 1 < ?e

goal (1 subgoal):
 1. 1 < e &&& 1 < d
[PROOF STEP]
apply(auto simp add: I_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>e N. e \<in> set_spmf (sample_coprime N) \<Longrightarrow> Suc 0 < e; x \<in> set_spmf sample_primes; xa \<in> set_spmf (sample_set_excl prime_set {x}); N = x * xa; e \<in> set_spmf (sample_coprime ((x - Suc 0) * (xa - Suc 0))); d = nat (fst (bezw e ((x - Suc 0) * (xa - Suc 0))) mod (int (x - Suc 0) * int (xa - Suc 0)))\<rbrakk> \<Longrightarrow> 1 < fst (bezw e ((x - Suc 0) * (xa - Suc 0))) mod (int (x - Suc 0) * int (xa - Suc 0))
[PROOF STEP]
by (smt Euclidean_Division.pos_mod_sign Num.of_nat_simps(5) Suc_diff_1 bezw_inverse cong_def coprime_imp_gcd_eq_1 gr0I less_1_mult less_numeral_extra(2) mem_Collect_eq mod_by_0 mod_less more_arith_simps(6) nat_0 nat_0_less_mult_iff nat_int nat_neq_iff numerals(2) of_nat_0_le_iff of_nat_1 rsa_base.mem_samp_primes_gt_2 rsa_base_axioms set_spmf_sample_coprime zero_less_diff)


[STATEMENT]
lemma finite_range: "finite (range index)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (local.range index)
[PROOF STEP]
by(simp add: range_def)


[STATEMENT]
lemma dom_eq_ran: "domain index = range index"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.domain index = local.range index
[PROOF STEP]
by(simp add: range_def domain_def)