[STATEMENT]
lemma ordinal_cases:
assumes zero: "a = 0 \<Longrightarrow> P"
    and suc:  "\<And>x. a = oSuc x \<Longrightarrow> P"
    and lim:  "\<And>f. \<lbrakk>strict_mono f; a = oLimit f\<rbrakk> \<Longrightarrow> P"
shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
apply (subgoal_tac "\<forall>x. a = x \<longrightarrow> P", force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. a = x \<longrightarrow> P
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. a = x \<longrightarrow> P
[PROOF STEP]
apply (rule_tac a=x in oLimit_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. a = 0 \<longrightarrow> P
 2. \<And>x xa. a = xa \<longrightarrow> P \<Longrightarrow> a = oSuc xa \<longrightarrow> P
 3. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. a = f n \<longrightarrow> P\<rbrakk> \<Longrightarrow> a = oLimit f \<longrightarrow> P
[PROOF STEP]
apply (rule impI, erule zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. a = xa \<longrightarrow> P \<Longrightarrow> a = oSuc xa \<longrightarrow> P
 2. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. a = f n \<longrightarrow> P\<rbrakk> \<Longrightarrow> a = oLimit f \<longrightarrow> P
[PROOF STEP]
apply (rule impI, erule suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. a = f n \<longrightarrow> P\<rbrakk> \<Longrightarrow> a = oLimit f \<longrightarrow> P
[PROOF STEP]
apply (rule impI, erule lim, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done