theory More_Numeral_Type

lemma minus_induct[case_names 0 minus]:
  assumes "P (0::'a)"
  assumes suc: "\<And>x. \<lbrakk> P (x - 1); 0 < x \<rbrakk> \<Longrightarrow> P x"
  shows "P x" proof (cases x rule: of_nat_cases) case (of_nat m) have "P (of_nat m)" proof (induct m) case 0 then show ?case using `P 0` by simp next case (Suc m) show ?case proof (cases "1 + of_nat m = (0::'a)") case True then show ?thesis using `P 0` by simp next case False with Suc suc show ?thesis by (metis add_diff_cancel_left' less_eq_0 not_less of_nat_Suc) qed qed with of_nat show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P x proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>x = of_nat m; m < nat n\<rbrakk> \<Longrightarrow> P x proof (state)
this:
x = of_nat m
m < nat n

goal (1 subgoal):
 1. \<And>m. \<lbrakk>x = of_nat m; m < nat n\<rbrakk> \<Longrightarrow> P x proof (prove)
goal (1 subgoal):
 1. P (of_nat m) proof (state)
goal (2 subgoals):
 1. P (of_nat 0)
 2. \<And>m. P (of_nat m) \<Longrightarrow> P (of_nat (Suc m)) proof (state)
this:


goal (2 subgoals):
 1. P (of_nat 0)
 2. \<And>m. P (of_nat m) \<Longrightarrow> P (of_nat (Suc m)) proof (chain)
picking this:
 proof (prove)
goal (1 subgoal):
 1. P (of_nat 0) proof (prove)
using this:
P (0::'a)

goal (1 subgoal):
 1. P (of_nat 0) proof (state)
this:
P (of_nat 0)

goal (1 subgoal):
 1. \<And>m. P (of_nat m) \<Longrightarrow> P (of_nat (Suc m)) proof (state)
goal (1 subgoal):
 1. \<And>m. P (of_nat m) \<Longrightarrow> P (of_nat (Suc m)) proof (state)
this:
P (of_nat m)

goal (1 subgoal):
 1. \<And>m. P (of_nat m) \<Longrightarrow> P (of_nat (Suc m)) proof (prove)
goal (1 subgoal):
 1. P (of_nat (Suc m)) proof (state)
goal (2 subgoals):
 1. (1::'a) + of_nat m = (0::'a) \<Longrightarrow> P (of_nat (Suc m))
 2. (1::'a) + of_nat m \<noteq> (0::'a) \<Longrightarrow> P (of_nat (Suc m)) proof (state)
this:
(1::'a) + of_nat m = (0::'a)

goal (2 subgoals):
 1. (1::'a) + of_nat m = (0::'a) \<Longrightarrow> P (of_nat (Suc m))
 2. (1::'a) + of_nat m \<noteq> (0::'a) \<Longrightarrow> P (of_nat (Suc m)) proof (chain)
picking this:
(1::'a) + of_nat m = (0::'a) proof (prove)
using this:
(1::'a) + of_nat m = (0::'a)

goal (1 subgoal):
 1. P (of_nat (Suc m)) proof (prove)
using this:
(1::'a) + of_nat m = (0::'a)
P (0::'a)

goal (1 subgoal):
 1. P (of_nat (Suc m)) proof (state)
this:
P (of_nat (Suc m))

goal (1 subgoal):
 1. (1::'a) + of_nat m \<noteq> (0::'a) \<Longrightarrow> P (of_nat (Suc m)) proof (state)
goal (1 subgoal):
 1. (1::'a) + of_nat m \<noteq> (0::'a) \<Longrightarrow> P (of_nat (Suc m)) proof (state)
this:
(1::'a) + of_nat m \<noteq> (0::'a)

goal (1 subgoal):
 1. (1::'a) + of_nat m \<noteq> (0::'a) \<Longrightarrow> P (of_nat (Suc m)) proof (chain)
picking this:
P (of_nat m)
\<lbrakk>P (?x - (1::'a)); (0::'a) < ?x\<rbrakk> \<Longrightarrow> P ?x
(1::'a) + of_nat m \<noteq> (0::'a) proof (prove)
using this:
P (of_nat m)
\<lbrakk>P (?x - (1::'a)); (0::'a) < ?x\<rbrakk> \<Longrightarrow> P ?x
(1::'a) + of_nat m \<noteq> (0::'a)

goal (1 subgoal):
 1. P (of_nat (Suc m)) proof (state)
this:
P (of_nat (Suc m))

goal:
No subgoals! proof (state)
this:
P (of_nat (Suc m))

goal:
No subgoals! proof (state)
this:
P (of_nat m)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>x = of_nat m; m < nat n\<rbrakk> \<Longrightarrow> P x proof (chain)
picking this:
x = of_nat m
m < nat n
P (of_nat m) proof (prove)
using this:
x = of_nat m
m < nat n
P (of_nat m)

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

goal:
No subgoals!