theory More_Numeral_Type

lemma from_top_induct[case_names top step]:
  assumes top: "\<And>x. y \<le> x \<Longrightarrow> P (x::'a)"
  assumes step: "\<And>x. \<lbrakk>P x; 0 < x; x \<le> y\<rbrakk> \<Longrightarrow> P (x - 1)"
  shows "P x" proof - obtain z where x: "x = y - z" by (metis diff_eq_diff_eq diff_right_commute) moreover have "P (y - z)" proof (induct z rule: plus_induct) case 0 then show ?case by (simp add: top) next case (plus x) then have [simp]: "y - (x + 1) = (y - x) - 1" by simp show ?case proof (cases "x < y") case True with plus show ?thesis by simp (metis diff_add_cancel eq_iff_diff_eq_0 le_neq_trans step plus_one_leq not_le
                      top zero_less_eq) next case False with plus show ?thesis by (smt top Rep_Abs_mod Rep_le_n less_def less_eq_def diff_def int_mod_ge' size0) qed qed ultimately show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P x proof (state)
goal (1 subgoal):
 1. P x proof (prove)
goal (1 subgoal):
 1. (\<And>z. x = y - z \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
x = y - z

goal (1 subgoal):
 1. P x proof (state)
this:
x = y - z

goal (1 subgoal):
 1. P x proof (prove)
goal (1 subgoal):
 1. P (y - z) proof (state)
goal (2 subgoals):
 1. P (y - (0::'a))
 2. \<And>x. \<lbrakk>P (y - x); x < x + (1::'a)\<rbrakk> \<Longrightarrow> P (y - (x + (1::'a))) proof (state)
this:


goal (2 subgoals):
 1. P (y - (0::'a))
 2. \<And>x. \<lbrakk>P (y - x); x < x + (1::'a)\<rbrakk> \<Longrightarrow> P (y - (x + (1::'a))) proof (chain)
picking this:
 proof (prove)
goal (1 subgoal):
 1. P (y - (0::'a)) proof (state)
this:
P (y - (0::'a))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>P (y - x); x < x + (1::'a)\<rbrakk> \<Longrightarrow> P (y - (x + (1::'a))) proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>P (y - x); x < x + (1::'a)\<rbrakk> \<Longrightarrow> P (y - (x + (1::'a))) proof (state)
this:
P (y - x)
x < x + (1::'a)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>P (y - x); x < x + (1::'a)\<rbrakk> \<Longrightarrow> P (y - (x + (1::'a))) proof (chain)
picking this:
P (y - x)
x < x + (1::'a) proof (prove)
using this:
P (y - x)
x < x + (1::'a)

goal (1 subgoal):
 1. y - (x + (1::'a)) = y - x - (1::'a) proof (state)
this:
y - (x + (1::'a)) = y - x - (1::'a)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>P (y - x); x < x + (1::'a)\<rbrakk> \<Longrightarrow> P (y - (x + (1::'a))) proof (prove)
goal (1 subgoal):
 1. P (y - (x + (1::'a))) proof (state)
goal (2 subgoals):
 1. x < y \<Longrightarrow> P (y - (x + (1::'a)))
 2. \<not> x < y \<Longrightarrow> P (y - (x + (1::'a))) proof (state)
this:
x < y

goal (2 subgoals):
 1. x < y \<Longrightarrow> P (y - (x + (1::'a)))
 2. \<not> x < y \<Longrightarrow> P (y - (x + (1::'a))) proof (chain)
picking this:
P (y - x)
x < x + (1::'a)
x < y proof (prove)
using this:
P (y - x)
x < x + (1::'a)
x < y

goal (1 subgoal):
 1. P (y - (x + (1::'a))) proof (state)
this:
P (y - (x + (1::'a)))

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> P (y - (x + (1::'a))) proof (state)
goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> P (y - (x + (1::'a))) proof (state)
this:
\<not> x < y

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> P (y - (x + (1::'a))) proof (chain)
picking this:
P (y - x)
x < x + (1::'a)
\<not> x < y proof (prove)
using this:
P (y - x)
x < x + (1::'a)
\<not> x < y

goal (1 subgoal):
 1. P (y - (x + (1::'a))) proof (state)
this:
P (y - (x + (1::'a)))

goal:
No subgoals! proof (state)
this:
P (y - (x + (1::'a)))

goal:
No subgoals! proof (state)
this:
P (y - z)

goal (1 subgoal):
 1. P x proof (chain)
picking this:
x = y - z
P (y - z) proof (prove)
using this:
x = y - z
P (y - z)

goal (1 subgoal):
 1. P x proof (state)
this:
P x

goal:
No subgoals!