[STATEMENT]
lemma real_of_preal_trichotomy:
  "\<exists>m. (x::real) = real_of_preal m \<or> x = 0 \<or> x = -(real_of_preal m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
proof (cases x)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa y. x = Abs_Real (Dedekind_Real.realrel `` {(xa, y)}) \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
case (Abs_Real u v)
[PROOF STATE]
proof (state)
this:
x = Abs_Real (Dedekind_Real.realrel `` {(u, v)})

goal (1 subgoal):
 1. \<And>xa y. x = Abs_Real (Dedekind_Real.realrel `` {(xa, y)}) \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
proof (cases u v rule: linorder_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. u < v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 2. u = v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 3. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
u < v

goal (3 subgoals):
 1. u < v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 2. u = v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 3. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u < v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u < v

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
using less_add_left
[PROOF STATE]
proof (prove)
using this:
u < v
?r < ?s \<Longrightarrow> ?r + (?s - ?r) = ?s

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
apply (simp add: Abs_Real real_of_preal_def real_minus real_zero_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u < v; \<And>r s. r < s \<Longrightarrow> r + (s - r) = s\<rbrakk> \<Longrightarrow> \<exists>m. u + 1 = m + 1 + v \<or> u + 1 = 1 + v \<or> u + (m + 1) = 1 + v
[PROOF STEP]
by (metis preal_add_assoc preal_add_commute)
[PROOF STATE]
proof (state)
this:
\<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m

goal (2 subgoals):
 1. u = v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 2. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 2. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
case equal
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. u = v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 2. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u = v

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
using Abs_Real real_zero_iff
[PROOF STATE]
proof (prove)
using this:
u = v
x = Abs_Real (Dedekind_Real.realrel `` {(u, v)})
Abs_Real (Dedekind_Real.realrel `` {(?x, ?x)}) = 0

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m

goal (1 subgoal):
 1. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
case greater
[PROOF STATE]
proof (state)
this:
v < u

goal (1 subgoal):
 1. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v < u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v < u

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
using less_add_left
[PROOF STATE]
proof (prove)
using this:
v < u
?r < ?s \<Longrightarrow> ?r + (?s - ?r) = ?s

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
apply (simp add: Abs_Real real_of_preal_def real_minus real_zero_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v < u; \<And>r s. r < s \<Longrightarrow> r + (s - r) = s\<rbrakk> \<Longrightarrow> \<exists>m. u + 1 = m + 1 + v \<or> u + 1 = 1 + v \<or> u + (m + 1) = 1 + v
[PROOF STEP]
by (metis preal_add_assoc preal_add_commute)
[PROOF STATE]
proof (state)
this:
\<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m

goal:
No subgoals!
[PROOF STEP]
qed