[STATEMENT]
lemma Rat_induct_pos [case_names Fract, induct type: rat]:
  assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)"
  shows "P q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P q
[PROOF STEP]
proof (cases q)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>q = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> P q
[PROOF STEP]
case (Fract a b)
[PROOF STATE]
proof (state)
this:
q = Fract a b
0 < b
coprime a b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>q = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> P q
[PROOF STEP]
have step': "P (Fract a b)" if b: "b < 0" for a b :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (Fract a b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (Fract a b)
[PROOF STEP]
from b
[PROOF STATE]
proof (chain)
picking this:
b < 0
[PROOF STEP]
have "0 < - b"
[PROOF STATE]
proof (prove)
using this:
b < 0

goal (1 subgoal):
 1. 0 < - b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < - b

goal (1 subgoal):
 1. P (Fract a b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < - b
[PROOF STEP]
have "P (Fract (- a) (- b))"
[PROOF STATE]
proof (prove)
using this:
0 < - b

goal (1 subgoal):
 1. P (Fract (- a) (- b))
[PROOF STEP]
by (rule step)
[PROOF STATE]
proof (state)
this:
P (Fract (- a) (- b))

goal (1 subgoal):
 1. P (Fract a b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P (Fract (- a) (- b))
[PROOF STEP]
show "P (Fract a b)"
[PROOF STATE]
proof (prove)
using this:
P (Fract (- a) (- b))

goal (1 subgoal):
 1. P (Fract a b)
[PROOF STEP]
by (simp add: order_less_imp_not_eq [OF b])
[PROOF STATE]
proof (state)
this:
P (Fract a b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?b < 0 \<Longrightarrow> P (Fract ?a ?b)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>q = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> P q
[PROOF STEP]
from Fract
[PROOF STATE]
proof (chain)
picking this:
q = Fract a b
0 < b
coprime a b
[PROOF STEP]
show "P q"
[PROOF STATE]
proof (prove)
using this:
q = Fract a b
0 < b
coprime a b

goal (1 subgoal):
 1. P q
[PROOF STEP]
by (auto simp add: linorder_neq_iff step step')
[PROOF STATE]
proof (state)
this:
P q

goal:
No subgoals!
[PROOF STEP]
qed