[STATEMENT]
lemma incrIndexList_help3[simp]: "incrIndexList ls m nmax \<Longrightarrow> last ls = (nmax - (Suc 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> last ls = nmax - Suc 0
[PROOF STEP]
by (unfold incrIndexList_def)  simp


[STATEMENT]
lemma incrIndexList_help4[simp]: "incrIndexList ls m nmax \<Longrightarrow> length ls = m "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> |ls| = m
[PROOF STEP]
by (unfold incrIndexList_def)  simp


[STATEMENT]
lemma incrIndexList_help5[intro]: "incrIndexList ls m nmax \<Longrightarrow>  last (butlast ls) < nmax - Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> last (butlast ls) < nmax - Suc 0
[PROOF STEP]
by (unfold incrIndexList_def) auto


[STATEMENT]
lemma incrIndexList_help6[simp]: "incrIndexList ls m nmax \<Longrightarrow> increasing ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> increasing ls
[PROOF STEP]
by (unfold incrIndexList_def) simp


[STATEMENT]
lemma incrIndexList_help7[simp]: "incrIndexList ls m nmax \<Longrightarrow> ls \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> ls \<noteq> []
[PROOF STEP]
apply (subgoal_tac "length ls \<noteq>  0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>incrIndexList ls m nmax; |ls| \<noteq> 0\<rbrakk> \<Longrightarrow> ls \<noteq> []
 2. incrIndexList ls m nmax \<Longrightarrow> |ls| \<noteq> 0
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> |ls| \<noteq> 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> 0 < m
[PROOF STEP]
apply (subgoal_tac "1 < m")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>incrIndexList ls m nmax; 1 < m\<rbrakk> \<Longrightarrow> 0 < m
 2. incrIndexList ls m nmax \<Longrightarrow> 1 < m
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> 1 < m
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma incrIndexList_help71[simp]: "\<not> incrIndexList [] m nmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> incrIndexList [] m nmax
[PROOF STEP]
by (auto dest: incrIndexList_help7)


[STATEMENT]
lemma incrIndexList_help8[simp]: "incrIndexList ls m nmax \<Longrightarrow> butlast ls \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> butlast ls \<noteq> []
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; \<not> butlast ls \<noteq> []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume props: "incrIndexList ls m nmax" and butl: "\<not> butlast ls \<noteq> []"
[PROOF STATE]
proof (state)
this:
incrIndexList ls m nmax
\<not> butlast ls \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; \<not> butlast ls \<noteq> []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
incrIndexList ls m nmax
\<not> butlast ls \<noteq> []
[PROOF STEP]
have "ls \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
incrIndexList ls m nmax
\<not> butlast ls \<noteq> []

goal (1 subgoal):
 1. ls \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; \<not> butlast ls \<noteq> []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ls \<noteq> []
[PROOF STEP]
have ls': "ls = (butlast ls) @ [last ls]"
[PROOF STATE]
proof (prove)
using this:
ls \<noteq> []

goal (1 subgoal):
 1. ls = butlast ls @ [last ls]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = butlast ls @ [last ls]

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; \<not> butlast ls \<noteq> []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
define l where "l = last ls"
[PROOF STATE]
proof (state)
this:
l = last ls

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; \<not> butlast ls \<noteq> []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with butl ls'
[PROOF STATE]
proof (chain)
picking this:
\<not> butlast ls \<noteq> []
ls = butlast ls @ [last ls]
l = last ls
[PROOF STEP]
have "ls = [l]"
[PROOF STATE]
proof (prove)
using this:
\<not> butlast ls \<noteq> []
ls = butlast ls @ [last ls]
l = last ls

goal (1 subgoal):
 1. ls = [l]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = [l]

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; \<not> butlast ls \<noteq> []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ls = [l]
[PROOF STEP]
have "length ls = 1"
[PROOF STATE]
proof (prove)
using this:
ls = [l]

goal (1 subgoal):
 1. |ls| = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|ls| = 1

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; \<not> butlast ls \<noteq> []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with props
[PROOF STATE]
proof (chain)
picking this:
incrIndexList ls m nmax
|ls| = 1
[PROOF STEP]
have "m = 1"
[PROOF STATE]
proof (prove)
using this:
incrIndexList ls m nmax
|ls| = 1

goal (1 subgoal):
 1. m = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m = 1

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; \<not> butlast ls \<noteq> []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with props
[PROOF STATE]
proof (chain)
picking this:
incrIndexList ls m nmax
m = 1
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
incrIndexList ls m nmax
m = 1

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto dest: incrIndexList_1lem)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma incrIndexList_help81[simp]: "\<not> incrIndexList [l] m nmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> incrIndexList [l] m nmax
[PROOF STEP]
by (auto dest: incrIndexList_help8)


[STATEMENT]
lemma incrIndexList_help9[intro]: "(incrIndexList ls m nmax)  \<Longrightarrow>
  x \<in> set (butlast ls) \<Longrightarrow> x \<le> nmax - 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
assume props: "(incrIndexList ls m nmax)"  and x: "x \<in> set (butlast ls)"
[PROOF STATE]
proof (state)
this:
incrIndexList ls m nmax
x \<in> set (butlast ls)

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
incrIndexList ls m nmax
x \<in> set (butlast ls)
[PROOF STEP]
have "last (butlast ls) < last ls"
[PROOF STATE]
proof (prove)
using this:
incrIndexList ls m nmax
x \<in> set (butlast ls)

goal (1 subgoal):
 1. last (butlast ls) < last ls
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
last (butlast ls) < last ls

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
with props
[PROOF STATE]
proof (chain)
picking this:
incrIndexList ls m nmax
last (butlast ls) < last ls
[PROOF STEP]
have "last (butlast ls) < nmax - 1"
[PROOF STATE]
proof (prove)
using this:
incrIndexList ls m nmax
last (butlast ls) < last ls

goal (1 subgoal):
 1. last (butlast ls) < nmax - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
last (butlast ls) < nmax - 1

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
last (butlast ls) < nmax - 1
[PROOF STEP]
have leq: "last (butlast ls) \<le>  nmax - 2"
[PROOF STATE]
proof (prove)
using this:
last (butlast ls) < nmax - 1

goal (1 subgoal):
 1. last (butlast ls) \<le> nmax - 2
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
last (butlast ls) \<le> nmax - 2

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
from props
[PROOF STATE]
proof (chain)
picking this:
incrIndexList ls m nmax
[PROOF STEP]
have "ls \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
incrIndexList ls m nmax

goal (1 subgoal):
 1. ls \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ls \<noteq> []
[PROOF STEP]
have ls1: "ls = butlast ls @ [last ls]"
[PROOF STATE]
proof (prove)
using this:
ls \<noteq> []

goal (1 subgoal):
 1. ls = butlast ls @ [last ls]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = butlast ls @ [last ls]

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
define ls' where "ls' = butlast (butlast ls)"
[PROOF STATE]
proof (state)
this:
ls' = butlast (butlast ls)

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
define last2 where "last2 = last (butlast ls)"
[PROOF STATE]
proof (state)
this:
last2 = last (butlast ls)

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
define last1 where "last1 = last ls"
[PROOF STATE]
proof (state)
this:
last1 = last ls

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
from props
[PROOF STATE]
proof (chain)
picking this:
incrIndexList ls m nmax
[PROOF STEP]
have "butlast ls \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
incrIndexList ls m nmax

goal (1 subgoal):
 1. butlast ls \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
butlast ls \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
with ls'_def last2_def
[PROOF STATE]
proof (chain)
picking this:
ls' = butlast (butlast ls)
last2 = last (butlast ls)
butlast ls \<noteq> []
[PROOF STEP]
have bls: "butlast ls = ls' @ [last2]"
[PROOF STATE]
proof (prove)
using this:
ls' = butlast (butlast ls)
last2 = last (butlast ls)
butlast ls \<noteq> []

goal (1 subgoal):
 1. butlast ls = ls' @ [last2]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
butlast ls = ls' @ [last2]

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
with last1_def ls1 props
[PROOF STATE]
proof (chain)
picking this:
last1 = last ls
ls = butlast ls @ [last ls]
incrIndexList ls m nmax
butlast ls = ls' @ [last2]
[PROOF STEP]
have ls3: "ls = ls' @ [last2] @ [last1]"
[PROOF STATE]
proof (prove)
using this:
last1 = last ls
ls = butlast ls @ [last ls]
incrIndexList ls m nmax
butlast ls = ls' @ [last2]

goal (1 subgoal):
 1. ls = ls' @ [last2] @ [last1]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = ls' @ [last2] @ [last1]

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
from props
[PROOF STATE]
proof (chain)
picking this:
incrIndexList ls m nmax
[PROOF STEP]
have "increasing ls"
[PROOF STATE]
proof (prove)
using this:
incrIndexList ls m nmax

goal (1 subgoal):
 1. increasing ls
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
increasing ls

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
with ls3
[PROOF STATE]
proof (chain)
picking this:
ls = ls' @ [last2] @ [last1]
increasing ls
[PROOF STEP]
have increasing: "increasing (ls' @ ([last2] @ [last1]))"
[PROOF STATE]
proof (prove)
using this:
ls = ls' @ [last2] @ [last1]
increasing ls

goal (1 subgoal):
 1. increasing (ls' @ [last2] @ [last1])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
increasing (ls' @ [last2] @ [last1])

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
increasing (ls' @ [last2] @ [last1])
[PROOF STEP]
have "x \<in> set ls' \<Longrightarrow> x \<le> last2"
[PROOF STATE]
proof (prove)
using this:
increasing (ls' @ [last2] @ [last1])

goal (1 subgoal):
 1. x \<in> set ls' \<Longrightarrow> x \<le> last2
[PROOF STEP]
by (auto intro: increasing2)
[PROOF STATE]
proof (state)
this:
x \<in> set ls' \<Longrightarrow> x \<le> last2

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set ls' \<Longrightarrow> x \<le> last2
[PROOF STEP]
have "x \<in> set (ls' @ [last2]) \<Longrightarrow> x \<le> last2"
[PROOF STATE]
proof (prove)
using this:
x \<in> set ls' \<Longrightarrow> x \<le> last2

goal (1 subgoal):
 1. x \<in> set (ls' @ [last2]) \<Longrightarrow> x \<le> last2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set (ls' @ [last2]) \<Longrightarrow> x \<le> last2

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
with bls x
[PROOF STATE]
proof (chain)
picking this:
butlast ls = ls' @ [last2]
x \<in> set (butlast ls)
x \<in> set (ls' @ [last2]) \<Longrightarrow> x \<le> last2
[PROOF STEP]
have "x \<le> last2"
[PROOF STATE]
proof (prove)
using this:
butlast ls = ls' @ [last2]
x \<in> set (butlast ls)
x \<in> set (ls' @ [last2]) \<Longrightarrow> x \<le> last2

goal (1 subgoal):
 1. x \<le> last2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<le> last2

goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
with leq last2_def
[PROOF STATE]
proof (chain)
picking this:
last (butlast ls) \<le> nmax - 2
last2 = last (butlast ls)
x \<le> last2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
last (butlast ls) \<le> nmax - 2
last2 = last (butlast ls)
x \<le> last2

goal (1 subgoal):
 1. x \<le> nmax - 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<le> nmax - 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma incrIndexList_help10[intro]: "(incrIndexList ls m nmax)  \<Longrightarrow>
  x \<in> set ls \<Longrightarrow> x < nmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set ls\<rbrakk> \<Longrightarrow> x < nmax
[PROOF STEP]
apply (cases ls rule: rev_exhaust)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>incrIndexList ls m nmax; x \<in> set ls; ls = []\<rbrakk> \<Longrightarrow> x < nmax
 2. \<And>ys y. \<lbrakk>incrIndexList ls m nmax; x \<in> set ls; ls = ys @ [y]\<rbrakk> \<Longrightarrow> x < nmax
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ys. \<lbrakk>incrIndexList (ys @ [x]) m nmax; ls = ys @ [x]\<rbrakk> \<Longrightarrow> x < nmax
 2. \<And>ys y. \<lbrakk>incrIndexList (ys @ [y]) m nmax; ls = ys @ [y]; x \<in> set ys\<rbrakk> \<Longrightarrow> x < nmax
[PROOF STEP]
apply (frule incrIndexList_help3)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ys. \<lbrakk>incrIndexList (ys @ [x]) m nmax; ls = ys @ [x]; last (ys @ [x]) = nmax - Suc 0\<rbrakk> \<Longrightarrow> x < nmax
 2. \<And>ys y. \<lbrakk>incrIndexList (ys @ [y]) m nmax; ls = ys @ [y]; x \<in> set ys\<rbrakk> \<Longrightarrow> x < nmax
[PROOF STEP]
apply (auto dest: incrIndexList_1len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>incrIndexList (ys @ [y]) m nmax; ls = ys @ [y]; x \<in> set ys\<rbrakk> \<Longrightarrow> x < nmax
[PROOF STEP]
apply (frule incrIndexList_help9)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ys y. \<lbrakk>incrIndexList (ys @ [y]) m nmax; ls = ys @ [y]; x \<in> set ys\<rbrakk> \<Longrightarrow> ?x9 ys y \<in> set (butlast (ys @ [y]))
 2. \<And>ys y. \<lbrakk>incrIndexList (ys @ [y]) m nmax; ls = ys @ [y]; x \<in> set ys; ?x9 ys y \<le> nmax - 2\<rbrakk> \<Longrightarrow> x < nmax
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>incrIndexList (ys @ [y]) m nmax; ls = ys @ [y]; x \<in> set ys; x \<le> nmax - 2\<rbrakk> \<Longrightarrow> x < nmax
[PROOF STEP]
apply (drule incrIndexList_1len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>ls = ys @ [y]; x \<in> set ys; x \<le> nmax - 2; Suc 0 < nmax\<rbrakk> \<Longrightarrow> x < nmax
[PROOF STEP]
by arith


[STATEMENT]
lemma enumerator_correctness: "2 < m \<Longrightarrow> 1 < nmax \<Longrightarrow>
  ls \<in> set (enumerator m nmax) \<Longrightarrow>
  incrIndexList ls m nmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 < m; 1 < nmax; ls \<in> set (enumerator m nmax)\<rbrakk> \<Longrightarrow> incrIndexList ls m nmax
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>2 < m; 1 < nmax; ls \<in> set (enumerator m nmax)\<rbrakk> \<Longrightarrow> incrIndexList ls m nmax
[PROOF STEP]
assume m: "2 < m" and nmax: "1 < nmax" and enum: "ls \<in> set (enumerator m nmax)"
[PROOF STATE]
proof (state)
this:
2 < m
1 < nmax
ls \<in> set (enumerator m nmax)

goal (1 subgoal):
 1. \<lbrakk>2 < m; 1 < nmax; ls \<in> set (enumerator m nmax)\<rbrakk> \<Longrightarrow> incrIndexList ls m nmax
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 < m
1 < nmax
ls \<in> set (enumerator m nmax)
[PROOF STEP]
have "(hd ls = 0 \<and> last ls = (nmax - 1) \<and> length ls = m \<and> last (butlast ls) < last ls \<and>  increasing ls)"
[PROOF STATE]
proof (prove)
using this:
2 < m
1 < nmax
ls \<in> set (enumerator m nmax)

goal (1 subgoal):
 1. hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> last (butlast ls) < last ls \<and> increasing ls
[PROOF STEP]
by (auto intro: enumerator_increasing enumerator_hd enumerator_last enumerator_length2 enumerator_bound3 simp: set_enumerator_simps)
[PROOF STATE]
proof (state)
this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> last (butlast ls) < last ls \<and> increasing ls

goal (1 subgoal):
 1. \<lbrakk>2 < m; 1 < nmax; ls \<in> set (enumerator m nmax)\<rbrakk> \<Longrightarrow> incrIndexList ls m nmax
[PROOF STEP]
with m nmax
[PROOF STATE]
proof (chain)
picking this:
2 < m
1 < nmax
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> last (butlast ls) < last ls \<and> increasing ls
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 < m
1 < nmax
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> last (butlast ls) < last ls \<and> increasing ls

goal (1 subgoal):
 1. incrIndexList ls m nmax
[PROOF STEP]
by (unfold incrIndexList_def) auto
[PROOF STATE]
proof (state)
this:
incrIndexList ls m nmax

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enumerator_completeness_help: "\<And> ls. increasing ls \<Longrightarrow> ls \<noteq> [] \<Longrightarrow> length ls = Suc ks \<Longrightarrow> list_all (\<lambda>x. x < Suc nmax) ls \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax))
[PROOF STEP]
proof (induct ks)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc 0; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ 0) (enumBase nmax))
 2. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
increasing ls
ls \<noteq> []
|ls| = Suc 0
list_all (\<lambda>x. x < Suc nmax) ls

goal (2 subgoals):
 1. \<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc 0; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ 0) (enumBase nmax))
 2. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
assume "increasing ls" "ls \<noteq> []" "length ls = Suc 0" "list_all (\<lambda>x. x < Suc nmax) ls"
[PROOF STATE]
proof (state)
this:
increasing ls
ls \<noteq> []
|ls| = Suc 0
list_all (\<lambda>x. x < Suc nmax) ls

goal (2 subgoals):
 1. \<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc 0; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ 0) (enumBase nmax))
 2. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
increasing ls
ls \<noteq> []
|ls| = Suc 0
list_all (\<lambda>x. x < Suc nmax) ls
[PROOF STEP]
have "\<exists> x. ls = [x]"
[PROOF STATE]
proof (prove)
using this:
increasing ls
ls \<noteq> []
|ls| = Suc 0
list_all (\<lambda>x. x < Suc nmax) ls

goal (1 subgoal):
 1. \<exists>x. ls = [x]
[PROOF STEP]
apply (case_tac "ls::nat list")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc 0; list_all (\<lambda>x. x < Suc nmax) ls; ls = []\<rbrakk> \<Longrightarrow> \<exists>x. ls = [x]
 2. \<And>a list. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc 0; list_all (\<lambda>x. x < Suc nmax) ls; ls = a # list\<rbrakk> \<Longrightarrow> \<exists>x. ls = [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. ls = [x]

goal (2 subgoals):
 1. \<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc 0; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ 0) (enumBase nmax))
 2. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. ls = [x]
[PROOF STEP]
obtain x where ls1: "ls = [x]"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. ls = [x]

goal (1 subgoal):
 1. (\<And>x. ls = [x] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = [x]

goal (2 subgoals):
 1. \<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc 0; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ 0) (enumBase nmax))
 2. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
with 0
[PROOF STATE]
proof (chain)
picking this:
increasing ls
ls \<noteq> []
|ls| = Suc 0
list_all (\<lambda>x. x < Suc nmax) ls
ls = [x]
[PROOF STEP]
have "x < Suc nmax"
[PROOF STATE]
proof (prove)
using this:
increasing ls
ls \<noteq> []
|ls| = Suc 0
list_all (\<lambda>x. x < Suc nmax) ls
ls = [x]

goal (1 subgoal):
 1. x < Suc nmax
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < Suc nmax

goal (2 subgoals):
 1. \<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc 0; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ 0) (enumBase nmax))
 2. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
with ls1
[PROOF STATE]
proof (chain)
picking this:
ls = [x]
x < Suc nmax
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ls = [x]
x < Suc nmax

goal (1 subgoal):
 1. ls \<in> set ((enumAppend nmax ^^ 0) (enumBase nmax))
[PROOF STEP]
apply (simp add: enumBase_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls = [x]; x < Suc nmax\<rbrakk> \<Longrightarrow> x = nmax \<or> [x] \<in> (\<lambda>x. [x]) ` {0..<nmax}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls \<in> set ((enumAppend nmax ^^ 0) (enumBase nmax))

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
define ls' where "ls' = butlast ls"
[PROOF STATE]
proof (state)
this:
ls' = butlast ls

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
define l where "l = last ls"
[PROOF STATE]
proof (state)
this:
l = last ls

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
define ll where "ll = last ls'"
[PROOF STATE]
proof (state)
this:
ll = last ls'

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
define bl where "bl = butlast ls'"
[PROOF STATE]
proof (state)
this:
bl = butlast ls'

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
define ls'list where "ls'list = (enumAppend nmax ^^ n) (enumBase nmax)"
[PROOF STATE]
proof (state)
this:
ls'list = (enumAppend nmax ^^ n) (enumBase nmax)

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ls'list = (enumAppend nmax ^^ n) (enumBase nmax)
[PROOF STEP]
have short: "(enumAppend nmax ^^ n) (enumBase nmax) = ls'list"
[PROOF STATE]
proof (prove)
using this:
ls'list = (enumAppend nmax ^^ n) (enumBase nmax)

goal (1 subgoal):
 1. (enumAppend nmax ^^ n) (enumBase nmax) = ls'list
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(enumAppend nmax ^^ n) (enumBase nmax) = ls'list

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls
[PROOF STEP]
have "ls \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls

goal (1 subgoal):
 1. ls \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls \<noteq> []

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ls \<noteq> []
[PROOF STEP]
have "ls = butlast ls @ [last ls]"
[PROOF STATE]
proof (prove)
using this:
ls \<noteq> []

goal (1 subgoal):
 1. ls = butlast ls @ [last ls]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = butlast ls @ [last ls]

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
with ls'_def l_def
[PROOF STATE]
proof (chain)
picking this:
ls' = butlast ls
l = last ls
ls = butlast ls @ [last ls]
[PROOF STEP]
have ls1: "ls = ls' @ [l]"
[PROOF STATE]
proof (prove)
using this:
ls' = butlast ls
l = last ls
ls = butlast ls @ [last ls]

goal (1 subgoal):
 1. ls = ls' @ [l]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = ls' @ [l]

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls
ls = ls' @ [l]
[PROOF STEP]
have "length ls' = Suc n"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls
ls = ls' @ [l]

goal (1 subgoal):
 1. |ls'| = Suc n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|ls'| = Suc n

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
|ls'| = Suc n
[PROOF STEP]
have ls'ne: "ls' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
|ls'| = Suc n

goal (1 subgoal):
 1. ls' \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls' \<noteq> []

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
with ll_def bl_def
[PROOF STATE]
proof (chain)
picking this:
ll = last ls'
bl = butlast ls'
ls' \<noteq> []
[PROOF STEP]
have ls'1: "ls' = bl @ [ll]"
[PROOF STATE]
proof (prove)
using this:
ll = last ls'
bl = butlast ls'
ls' \<noteq> []

goal (1 subgoal):
 1. ls' = bl @ [ll]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls' = bl @ [ll]

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ls' = bl @ [ll]
[PROOF STEP]
have ll_in_ls': "ll \<in> set ls'"
[PROOF STATE]
proof (prove)
using this:
ls' = bl @ [ll]

goal (1 subgoal):
 1. ll \<in> set ls'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ll \<in> set ls'

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
from Suc ls1
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls
ls = ls' @ [l]
[PROOF STEP]
have "list_all (\<lambda>x. x < Suc nmax) ls'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls
ls = ls' @ [l]

goal (1 subgoal):
 1. list_all (\<lambda>x. x < Suc nmax) ls'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list_all (\<lambda>x. x < Suc nmax) ls'

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
with ll_in_ls'
[PROOF STATE]
proof (chain)
picking this:
ll \<in> set ls'
list_all (\<lambda>x. x < Suc nmax) ls'
[PROOF STEP]
have "ll < Suc nmax"
[PROOF STATE]
proof (prove)
using this:
ll \<in> set ls'
list_all (\<lambda>x. x < Suc nmax) ls'

goal (1 subgoal):
 1. ll < Suc nmax
[PROOF STEP]
by (induct ls') auto
[PROOF STATE]
proof (state)
this:
ll < Suc nmax

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
with ll_def
[PROOF STATE]
proof (chain)
picking this:
ll = last ls'
ll < Suc nmax
[PROOF STEP]
have llsmall: "last ls' \<le> nmax"
[PROOF STATE]
proof (prove)
using this:
ll = last ls'
ll < Suc nmax

goal (1 subgoal):
 1. last ls' \<le> nmax
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
last ls' \<le> nmax

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
from ls1
[PROOF STATE]
proof (chain)
picking this:
ls = ls' @ [l]
[PROOF STEP]
have l_in_ls: "l \<in> set ls"
[PROOF STATE]
proof (prove)
using this:
ls = ls' @ [l]

goal (1 subgoal):
 1. l \<in> set ls
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<in> set ls

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls
[PROOF STEP]
have "list_all (\<lambda>x. x < Suc nmax) ls"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls

goal (1 subgoal):
 1. list_all (\<lambda>x. x < Suc nmax) ls
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list_all (\<lambda>x. x < Suc nmax) ls

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
with l_in_ls
[PROOF STATE]
proof (chain)
picking this:
l \<in> set ls
list_all (\<lambda>x. x < Suc nmax) ls
[PROOF STEP]
have "l < Suc nmax"
[PROOF STATE]
proof (prove)
using this:
l \<in> set ls
list_all (\<lambda>x. x < Suc nmax) ls

goal (1 subgoal):
 1. l < Suc nmax
[PROOF STEP]
by (induct ls) auto
[PROOF STATE]
proof (state)
this:
l < Suc nmax

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l < Suc nmax
[PROOF STEP]
have lo: "l \<le> nmax"
[PROOF STATE]
proof (prove)
using this:
l < Suc nmax

goal (1 subgoal):
 1. l \<le> nmax
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<le> nmax

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
from Suc ls1 ls'1
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls
ls = ls' @ [l]
ls' = bl @ [ll]
[PROOF STEP]
have "increasing ((bl @ [ll]) @ [l])"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls
ls = ls' @ [l]
ls' = bl @ [ll]

goal (1 subgoal):
 1. increasing ((bl @ [ll]) @ [l])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
increasing ((bl @ [ll]) @ [l])

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
increasing ((bl @ [ll]) @ [l])
[PROOF STEP]
have "ll \<le>  l"
[PROOF STATE]
proof (prove)
using this:
increasing ((bl @ [ll]) @ [l])

goal (1 subgoal):
 1. ll \<le> l
[PROOF STEP]
by (rule increasing2) auto
[PROOF STATE]
proof (state)
this:
ll \<le> l

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
with ll_def
[PROOF STATE]
proof (chain)
picking this:
ll = last ls'
ll \<le> l
[PROOF STEP]
have lu: "last ls' \<le> l"
[PROOF STATE]
proof (prove)
using this:
ll = last ls'
ll \<le> l

goal (1 subgoal):
 1. last ls' \<le> l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
last ls' \<le> l

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
from Suc ls1
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls
ls = ls' @ [l]
[PROOF STEP]
have vors: "ls' \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>increasing ?ls; ?ls \<noteq> []; |?ls| = Suc n; list_all (\<lambda>x. x < Suc nmax) ?ls\<rbrakk> \<Longrightarrow> ?ls \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
increasing ls
ls \<noteq> []
|ls| = Suc (Suc n)
list_all (\<lambda>x. x < Suc nmax) ls
ls = ls' @ [l]

goal (1 subgoal):
 1. ls' \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
[PROOF STEP]
by (rule_tac Suc) (auto intro: increasing4)
[PROOF STATE]
proof (state)
this:
ls' \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
with short
[PROOF STATE]
proof (chain)
picking this:
(enumAppend nmax ^^ n) (enumBase nmax) = ls'list
ls' \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
[PROOF STEP]
have "ls' \<in> set ls'list"
[PROOF STATE]
proof (prove)
using this:
(enumAppend nmax ^^ n) (enumBase nmax) = ls'list
ls' \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))

goal (1 subgoal):
 1. ls' \<in> set ls'list
[PROOF STEP]
by  auto
[PROOF STATE]
proof (state)
this:
ls' \<in> set ls'list

goal (1 subgoal):
 1. \<And>ks ls. \<lbrakk>\<And>ls. \<lbrakk>increasing ls; ls \<noteq> []; |ls| = Suc ks; list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ ks) (enumBase nmax)); increasing ls; ls \<noteq> []; |ls| = Suc (Suc ks); list_all (\<lambda>x. x < Suc nmax) ls\<rbrakk> \<Longrightarrow> ls \<in> set ((enumAppend nmax ^^ Suc ks) (enumBase nmax))
[PROOF STEP]
with short llsmall ls1 lo lu
[PROOF STATE]
proof (chain)
picking this:
(enumAppend nmax ^^ n) (enumBase nmax) = ls'list
last ls' \<le> nmax
ls = ls' @ [l]
l \<le> nmax
last ls' \<le> l
ls' \<in> set ls'list
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(enumAppend nmax ^^ n) (enumBase nmax) = ls'list
last ls' \<le> nmax
ls = ls' @ [l]
l \<le> nmax
last ls' \<le> l
ls' \<in> set ls'list

goal (1 subgoal):
 1. ls \<in> set ((enumAppend nmax ^^ Suc n) (enumBase nmax))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(enumAppend nmax ^^ n) (enumBase nmax) = ls'list; ls = ls' @ [l]; l \<le> nmax; last ls' \<le> l; ls' \<in> set ls'list\<rbrakk> \<Longrightarrow> ls' @ [l] \<in> set (enumAppend nmax ls'list)
[PROOF STEP]
apply (simp add: enumAppend_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(enumAppend nmax ^^ n) (enumBase nmax) = ls'list; ls = ls' @ [l]; l \<le> nmax; last ls' \<le> l; ls' \<in> set ls'list\<rbrakk> \<Longrightarrow> \<exists>x\<in>set ls'list. ls' @ [l] \<in> (\<lambda>xa. x @ [xa]) ` {xa. last x \<le> nmax \<and> (xa = nmax \<or> last x \<le> xa \<and> xa < nmax)}
[PROOF STEP]
apply (intro bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(enumAppend nmax ^^ n) (enumBase nmax) = ls'list; ls = ls' @ [l]; l \<le> nmax; last ls' \<le> l; ls' \<in> set ls'list\<rbrakk> \<Longrightarrow> ls' @ [l] \<in> (\<lambda>x. ?x14 @ [x]) ` {x. last ?x14 \<le> nmax \<and> (x = nmax \<or> last ?x14 \<le> x \<and> x < nmax)}
 2. \<lbrakk>(enumAppend nmax ^^ n) (enumBase nmax) = ls'list; ls = ls' @ [l]; l \<le> nmax; last ls' \<le> l; ls' \<in> set ls'list\<rbrakk> \<Longrightarrow> ?x14 \<in> set ls'list
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls \<in> set ((enumAppend nmax ^^ Suc n) (enumBase nmax))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enumerator_completeness: "2 < m \<Longrightarrow> incrIndexList ls m nmax \<Longrightarrow>
  ls \<in> set (enumerator m nmax)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 < m; incrIndexList ls m nmax\<rbrakk> \<Longrightarrow> ls \<in> set (enumerator m nmax)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>2 < m; incrIndexList ls m nmax\<rbrakk> \<Longrightarrow> ls \<in> set (enumerator m nmax)
[PROOF STEP]
assume m: "2 < m" and props: "incrIndexList ls m nmax"
[PROOF STATE]
proof (state)
this:
2 < m
incrIndexList ls m nmax

goal (1 subgoal):
 1. \<lbrakk>2 < m; incrIndexList ls m nmax\<rbrakk> \<Longrightarrow> ls \<in> set (enumerator m nmax)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 < m
incrIndexList ls m nmax
[PROOF STEP]
have props': "(hd ls = 0 \<and> last ls = (nmax - 1)
   \<and> length ls = m \<and> last (butlast ls) < last ls \<and>  increasing ls)"
[PROOF STATE]
proof (prove)
using this:
2 < m
incrIndexList ls m nmax

goal (1 subgoal):
 1. hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> last (butlast ls) < last ls \<and> increasing ls
[PROOF STEP]
by (unfold incrIndexList_def) auto
[PROOF STATE]
proof (state)
this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> last (butlast ls) < last ls \<and> increasing ls

goal (1 subgoal):
 1. \<lbrakk>2 < m; incrIndexList ls m nmax\<rbrakk> \<Longrightarrow> ls \<in> set (enumerator m nmax)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
have props'': "hd ls = 0 \<and> last ls = (nmax - 1) \<and> length ls = m \<and>
       increasing ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls
[PROOF STEP]
by (auto simp: props')
[PROOF STATE]
proof (state)
this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
show "ls \<in> set (enumerator m nmax)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
from m props''
[PROOF STATE]
proof (chain)
picking this:
2 < m
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls
[PROOF STEP]
have l_ls: "2 < length ls"
[PROOF STATE]
proof (prove)
using this:
2 < m
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls

goal (1 subgoal):
 1. 2 < |ls|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 < |ls|

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 < |ls|
[PROOF STEP]
have "\<exists> x y ks. ls = x # ks @ [y]"
[PROOF STATE]
proof (prove)
using this:
2 < |ls|

goal (1 subgoal):
 1. \<exists>x y ks. ls = x # ks @ [y]
[PROOF STEP]
apply (case_tac "ls::(nat list)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 < |ls|; ls = []\<rbrakk> \<Longrightarrow> \<exists>x y ks. ls = x # ks @ [y]
 2. \<And>a list. \<lbrakk>2 < |ls|; ls = a # list\<rbrakk> \<Longrightarrow> \<exists>x y ks. ls = x # ks @ [y]
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>Suc 0 < |list|; ls = a # list\<rbrakk> \<Longrightarrow> \<exists>y ks. list = ks @ [y]
[PROOF STEP]
apply (case_tac "list" rule: rev_exhaust)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>Suc 0 < |list|; ls = a # list; list = []\<rbrakk> \<Longrightarrow> \<exists>y ks. list = ks @ [y]
 2. \<And>a list ys y. \<lbrakk>Suc 0 < |list|; ls = a # list; list = ys @ [y]\<rbrakk> \<Longrightarrow> \<exists>y ks. list = ks @ [y]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x y ks. ls = x # ks @ [y]

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x y ks. ls = x # ks @ [y]
[PROOF STEP]
obtain x y ks where "ls = x # ks @ [y]"
[PROOF STATE]
proof (prove)
using this:
\<exists>x y ks. ls = x # ks @ [y]

goal (1 subgoal):
 1. (\<And>x ks y. ls = x # ks @ [y] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = x # ks @ [y]

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
with props''
[PROOF STATE]
proof (chain)
picking this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls
ls = x # ks @ [y]
[PROOF STEP]
have ls': "ls = 0 # ks @ [nmax - 1]"
[PROOF STATE]
proof (prove)
using this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls
ls = x # ks @ [y]

goal (1 subgoal):
 1. ls = 0 # ks @ [nmax - 1]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = 0 # ks @ [nmax - 1]

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
with l_ls
[PROOF STATE]
proof (chain)
picking this:
2 < |ls|
ls = 0 # ks @ [nmax - 1]
[PROOF STEP]
have l_ms: "0 < length ks"
[PROOF STATE]
proof (prove)
using this:
2 < |ls|
ls = 0 # ks @ [nmax - 1]

goal (1 subgoal):
 1. 0 < |ks|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < |ks|

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < |ks|
[PROOF STEP]
have ms_ne: "ks \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
0 < |ks|

goal (1 subgoal):
 1. ks \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ks \<noteq> []

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
from ls'
[PROOF STATE]
proof (chain)
picking this:
ls = 0 # ks @ [nmax - 1]
[PROOF STEP]
have lks: "length ks = length ls - 2"
[PROOF STATE]
proof (prove)
using this:
ls = 0 # ks @ [nmax - 1]

goal (1 subgoal):
 1. |ks| = |ls| - 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|ks| = |ls| - 2

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
from props''
[PROOF STATE]
proof (chain)
picking this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls
[PROOF STEP]
have nd: "increasing ls"
[PROOF STATE]
proof (prove)
using this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls

goal (1 subgoal):
 1. increasing ls
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
increasing ls

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
from props''
[PROOF STATE]
proof (chain)
picking this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls
[PROOF STEP]
have "\<And> z. z \<in> set ks \<Longrightarrow> 0 \<le> z"
[PROOF STATE]
proof (prove)
using this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls

goal (1 subgoal):
 1. \<And>z. z \<in> set ks \<Longrightarrow> 0 \<le> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?z \<in> set ks \<Longrightarrow> 0 \<le> ?z

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
from props'' ls'
[PROOF STATE]
proof (chain)
picking this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls
ls = 0 # ks @ [nmax - 1]
[PROOF STEP]
have "increasing ((0 # ks) @ [nmax - 1])"
[PROOF STATE]
proof (prove)
using this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls
ls = 0 # ks @ [nmax - 1]

goal (1 subgoal):
 1. increasing ((0 # ks) @ [nmax - 1])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
increasing ((0 # ks) @ [nmax - 1])

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
increasing ((0 # ks) @ [nmax - 1])
[PROOF STEP]
have z: "\<And> z. z \<in> set ks \<Longrightarrow> z \<le> (nmax - 1)"
[PROOF STATE]
proof (prove)
using this:
increasing ((0 # ks) @ [nmax - 1])

goal (1 subgoal):
 1. \<And>z. z \<in> set ks \<Longrightarrow> z \<le> nmax - 1
[PROOF STEP]
by (drule_tac increasing2) auto
[PROOF STATE]
proof (state)
this:
?z \<in> set ks \<Longrightarrow> ?z \<le> nmax - 1

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
from props  ls'
[PROOF STATE]
proof (chain)
picking this:
incrIndexList ls m nmax
ls = 0 # ks @ [nmax - 1]
[PROOF STEP]
have z': "\<And> z. z \<in> set ks \<Longrightarrow> z \<le> (nmax - 2)"
[PROOF STATE]
proof (prove)
using this:
incrIndexList ls m nmax
ls = 0 # ks @ [nmax - 1]

goal (1 subgoal):
 1. \<And>z. z \<in> set ks \<Longrightarrow> z \<le> nmax - 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?z \<in> set ks \<Longrightarrow> ?z \<le> nmax - 2

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
have "ks \<in> set ((enumAppend (nmax - 2)
         ^^ (length ks - Suc 0)) (enumBase (nmax - 2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
proof (cases "ks = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ks = [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
 2. ks \<noteq> [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ks = []

goal (2 subgoals):
 1. ks = [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
 2. ks \<noteq> [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
with ms_ne
[PROOF STATE]
proof (chain)
picking this:
ks \<noteq> []
ks = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ks \<noteq> []
ks = []

goal (1 subgoal):
 1. ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))

goal (1 subgoal):
 1. ks \<noteq> [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ks \<noteq> [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ks \<noteq> []

goal (1 subgoal):
 1. ks \<noteq> [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
from props''
[PROOF STATE]
proof (chain)
picking this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls
[PROOF STEP]
have "increasing ls"
[PROOF STATE]
proof (prove)
using this:
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> increasing ls

goal (1 subgoal):
 1. increasing ls
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
increasing ls

goal (1 subgoal):
 1. ks \<noteq> [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
with ls'
[PROOF STATE]
proof (chain)
picking this:
ls = 0 # ks @ [nmax - 1]
increasing ls
[PROOF STEP]
have "increasing (0 # ks)"
[PROOF STATE]
proof (prove)
using this:
ls = 0 # ks @ [nmax - 1]
increasing ls

goal (1 subgoal):
 1. increasing (0 # ks)
[PROOF STEP]
by (auto intro: increasing4)
[PROOF STATE]
proof (state)
this:
increasing (0 # ks)

goal (1 subgoal):
 1. ks \<noteq> [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
increasing (0 # ks)
[PROOF STEP]
have "increasing ([0] @ ks)"
[PROOF STATE]
proof (prove)
using this:
increasing (0 # ks)

goal (1 subgoal):
 1. increasing ([0] @ ks)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
increasing ([0] @ ks)

goal (1 subgoal):
 1. ks \<noteq> [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
increasing ([0] @ ks)
[PROOF STEP]
have ndks: "increasing ks"
[PROOF STATE]
proof (prove)
using this:
increasing ([0] @ ks)

goal (1 subgoal):
 1. increasing ks
[PROOF STEP]
by (rule_tac increasing5)
[PROOF STATE]
proof (state)
this:
increasing ks

goal (1 subgoal):
 1. ks \<noteq> [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
have listall: "list_all (\<lambda>x. x < Suc (nmax - 2)) ks"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>x. x < Suc (nmax - 2)) ks
[PROOF STEP]
apply (simp add: list_all_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set ks. x < Suc (nmax - 2)
[PROOF STEP]
by (auto dest: z')
[PROOF STATE]
proof (state)
this:
list_all (\<lambda>x. x < Suc (nmax - 2)) ks

goal (1 subgoal):
 1. ks \<noteq> [] \<Longrightarrow> ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
with False ndks
[PROOF STATE]
proof (chain)
picking this:
ks \<noteq> []
increasing ks
list_all (\<lambda>x. x < Suc (nmax - 2)) ks
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ks \<noteq> []
increasing ks
list_all (\<lambda>x. x < Suc (nmax - 2)) ks

goal (1 subgoal):
 1. ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
apply (rule_tac enumerator_completeness_help)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ks \<noteq> []; increasing ks; list_all (\<lambda>x. x < Suc (nmax - 2)) ks\<rbrakk> \<Longrightarrow> increasing ks
 2. \<lbrakk>ks \<noteq> []; increasing ks; list_all (\<lambda>x. x < Suc (nmax - 2)) ks\<rbrakk> \<Longrightarrow> ks \<noteq> []
 3. \<lbrakk>ks \<noteq> []; increasing ks; list_all (\<lambda>x. x < Suc (nmax - 2)) ks\<rbrakk> \<Longrightarrow> |ks| = Suc (|ks| - Suc 0)
 4. \<lbrakk>ks \<noteq> []; increasing ks; list_all (\<lambda>x. x < Suc (nmax - 2)) ks\<rbrakk> \<Longrightarrow> list_all (\<lambda>x. x < Suc (nmax - 2)) ks
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
with lks props'
[PROOF STATE]
proof (chain)
picking this:
|ks| = |ls| - 2
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> last (butlast ls) < last ls \<and> increasing ls
ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))
[PROOF STEP]
have
        "ks \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2)))"
[PROOF STATE]
proof (prove)
using this:
|ks| = |ls| - 2
hd ls = 0 \<and> last ls = nmax - 1 \<and> |ls| = m \<and> last (butlast ls) < last ls \<and> increasing ls
ks \<in> set ((enumAppend (nmax - 2) ^^ (|ks| - Suc 0)) (enumBase (nmax - 2)))

goal (1 subgoal):
 1. ks \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ks \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2)))

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
with m ls'
[PROOF STATE]
proof (chain)
picking this:
2 < m
ls = 0 # ks @ [nmax - 1]
ks \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 < m
ls = 0 # ks @ [nmax - 1]
ks \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2)))

goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax)
[PROOF STEP]
by (simp add: enumerator_def)
[PROOF STATE]
proof (state)
this:
ls \<in> set (enumerator m nmax)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ls \<in> set (enumerator m nmax)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ls \<in> set (enumerator m nmax)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enumerator_equiv[simp]:
 "2 < n \<Longrightarrow> 1 < m \<Longrightarrow> is \<in> set(enumerator n m) = incrIndexList is n m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 < n; 1 < m\<rbrakk> \<Longrightarrow> (is \<in> set (enumerator n m)) = incrIndexList is n m
[PROOF STEP]
by (auto intro: enumerator_correctness enumerator_completeness)


[STATEMENT]
lemma linf_norm_vec: "\<parallel>vec n f\<parallel>\<^sub>\<infinity> = max_list (map (abs \<circ> f) [0..<n] @ [0])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>vec n f\<parallel>\<^sub>\<infinity> = Missing_Lemmas.max_list (map (abs \<circ> f) [0..<n] @ [0::'a])
[PROOF STEP]
by (simp add: linf_norm_vec_def)


[STATEMENT]
lemma linf_norm_vec_vCons[simp]: "\<parallel>vCons a v\<parallel>\<^sub>\<infinity> = max \<bar>a\<bar> \<parallel>v\<parallel>\<^sub>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>vCons a v\<parallel>\<^sub>\<infinity> = max \<bar>a\<bar> \<parallel>v\<parallel>\<^sub>\<infinity>
[PROOF STEP]
by (auto simp: linf_norm_vec_def max_list_Cons)


[STATEMENT]
lemma linf_norm_vec_0 [simp]: "\<parallel>vec 0 f\<parallel>\<^sub>\<infinity> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>vec 0 f\<parallel>\<^sub>\<infinity> = (0::'a)
[PROOF STEP]
by (simp add: linf_norm_vec_def)


[STATEMENT]
lemma linf_norm_zero_vec [simp]: "\<parallel>0\<^sub>v n :: 'a :: ordered_ab_group_add_abs vec\<parallel>\<^sub>\<infinity> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>0\<^sub>v n\<parallel>\<^sub>\<infinity> = (0::'a)
[PROOF STEP]
by (induct n, simp add: zero_vec_def, auto simp: zero_vec_Suc)


[STATEMENT]
lemma linf_norm_vec_ge_0 [intro!]:
  fixes v :: "'a :: ordered_ab_group_add_abs vec"
  shows "\<parallel>v\<parallel>\<^sub>\<infinity> \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> \<parallel>v\<parallel>\<^sub>\<infinity>
[PROOF STEP]
by (induct v, auto simp: max_def)


[STATEMENT]
lemma linf_norm_vec_eq_0 [simp]:
  fixes v :: "'a :: ordered_ab_group_add_abs vec"
  assumes "v \<in> carrier_vec n"
  shows "\<parallel>v\<parallel>\<^sub>\<infinity> = 0 \<longleftrightarrow> v = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<parallel>v\<parallel>\<^sub>\<infinity> = (0::'a)) = (v = 0\<^sub>v n)
[PROOF STEP]
by (insert assms, induct rule: carrier_vec_induct, auto simp: zero_vec_Suc max_def)


[STATEMENT]
lemma linf_norm_vec_greater_0 [simp]:
  fixes v :: "'a :: ordered_ab_group_add_abs vec"
  assumes "v \<in> carrier_vec n"
  shows "\<parallel>v\<parallel>\<^sub>\<infinity> > 0 \<longleftrightarrow> v \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) < \<parallel>v\<parallel>\<^sub>\<infinity>) = (v \<noteq> 0\<^sub>v n)
[PROOF STEP]
by (insert assms, induct rule: carrier_vec_induct, auto simp: zero_vec_Suc max_def)


[STATEMENT]
lemma linf_norm_poly_0 [simp]: "\<parallel>0::_ poly\<parallel>\<^sub>\<infinity> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>0\<parallel>\<^sub>\<infinity> = (0::'a)
[PROOF STEP]
by (simp add: linf_norm_poly_def)


[STATEMENT]
lemma linf_norm_pCons [simp]:
  fixes p :: "'a :: ordered_ab_group_add_abs poly"
  shows "\<parallel>pCons a p\<parallel>\<^sub>\<infinity> = max \<bar>a\<bar> \<parallel>p\<parallel>\<^sub>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>pCons a p\<parallel>\<^sub>\<infinity> = max \<bar>a\<bar> \<parallel>p\<parallel>\<^sub>\<infinity>
[PROOF STEP]
by (cases "p = 0", cases "a = 0", auto simp: linf_norm_poly_def max_list_Cons)


[STATEMENT]
lemma linf_norm_poly_ge_0 [intro!]:
  fixes f :: "'a :: ordered_ab_group_add_abs poly"
  shows "\<parallel>f\<parallel>\<^sub>\<infinity> \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> \<parallel>f\<parallel>\<^sub>\<infinity>
[PROOF STEP]
by (induct f, auto simp: max_def)


[STATEMENT]
lemma linf_norm_poly_eq_0 [simp]:
  fixes f :: "'a :: ordered_ab_group_add_abs poly"
  shows "\<parallel>f\<parallel>\<^sub>\<infinity> = 0 \<longleftrightarrow> f = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<parallel>f\<parallel>\<^sub>\<infinity> = (0::'a)) = (f = 0)
[PROOF STEP]
by (induct f, auto simp: max_def)


[STATEMENT]
lemma linf_norm_poly_greater_0 [simp]:
  fixes f :: "'a :: ordered_ab_group_add_abs poly"
  shows "\<parallel>f\<parallel>\<^sub>\<infinity> > 0 \<longleftrightarrow> f \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) < \<parallel>f\<parallel>\<^sub>\<infinity>) = (f \<noteq> 0)
[PROOF STEP]
by (induct f, auto simp: max_def)


[STATEMENT]
lemma sq_norm_vec_vCons[simp]: "\<parallel>vCons a v\<parallel>\<^sup>2 = \<parallel>a\<parallel>\<^sup>2 + \<parallel>v\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>vCons a v\<parallel>\<^sup>2 = sq_norm_conjugate a + \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
by (simp add: sq_norm_vec_def)


[STATEMENT]
lemma sq_norm_vec_0[simp]: "\<parallel>vec 0 f\<parallel>\<^sup>2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>vec 0 f\<parallel>\<^sup>2 = (0::'a)
[PROOF STEP]
by (simp add: sq_norm_vec_def)


[STATEMENT]
lemma sq_norm_vec_as_cscalar_prod:
  fixes v :: "'a :: conjugatable_ring vec"
  shows "\<parallel>v\<parallel>\<^sup>2 = v \<bullet>c v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>v\<parallel>\<^sup>2 = v \<bullet>c v
[PROOF STEP]
by (induct v, simp_all add: sq_norm_vec_def)


[STATEMENT]
lemma sq_norm_zero_vec[simp]: "\<parallel>0\<^sub>v n :: 'a :: conjugatable_ring vec\<parallel>\<^sup>2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>0\<^sub>v n\<parallel>\<^sup>2 = (0::'a)
[PROOF STEP]
by (simp add: sq_norm_vec_as_cscalar_prod)


[STATEMENT]
lemma sq_norm_poly_0 [simp]: "\<parallel>0::_poly\<parallel>\<^sup>2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>0\<parallel>\<^sup>2 = (0::'a)
[PROOF STEP]
by (auto simp: sq_norm_poly_def)


[STATEMENT]
lemma sq_norm_poly_pCons [simp]:
  fixes a :: "'a :: conjugatable_ring"
  shows "\<parallel>pCons a p\<parallel>\<^sup>2 = \<parallel>a\<parallel>\<^sup>2 + \<parallel>p\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>pCons a p\<parallel>\<^sup>2 = sq_norm_conjugate a + \<parallel>p\<parallel>\<^sup>2
[PROOF STEP]
by (cases "p = 0"; cases "a = 0", auto simp: sq_norm_poly_def)


[STATEMENT]
lemma sq_norm_poly_ge_0 [intro!]:
  fixes p :: "'a :: conjugatable_ordered_ring poly"
  shows "\<parallel>p\<parallel>\<^sup>2 \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> \<parallel>p\<parallel>\<^sup>2
[PROOF STEP]
by (unfold sq_norm_poly_def, rule sum_list_nonneg, auto intro!:conjugate_square_positive)


[STATEMENT]
lemma sq_norm_poly_eq_0 [simp]:
  fixes p :: "'a :: {conjugatable_ordered_ring,ring_no_zero_divisors} poly"
  shows "\<parallel>p\<parallel>\<^sup>2 = 0 \<longleftrightarrow> p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<parallel>p\<parallel>\<^sup>2 = (0::'a)) = (p = 0)
[PROOF STEP]
proof (induct p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<parallel>0\<parallel>\<^sup>2 = (0::'a)) = (0 = 0)
 2. \<And>a p. \<lbrakk>a \<noteq> (0::'a) \<or> p \<noteq> 0; (\<parallel>p\<parallel>\<^sup>2 = (0::'a)) = (p = 0)\<rbrakk> \<Longrightarrow> (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
[PROOF STEP]
case IH: (pCons a p)
[PROOF STATE]
proof (state)
this:
a \<noteq> (0::'a) \<or> p \<noteq> 0
(\<parallel>p\<parallel>\<^sup>2 = (0::'a)) = (p = 0)

goal (2 subgoals):
 1. (\<parallel>0\<parallel>\<^sup>2 = (0::'a)) = (0 = 0)
 2. \<And>a p. \<lbrakk>a \<noteq> (0::'a) \<or> p \<noteq> 0; (\<parallel>p\<parallel>\<^sup>2 = (0::'a)) = (p = 0)\<rbrakk> \<Longrightarrow> (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
[PROOF STEP]
proof (cases "a = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
 2. a \<noteq> (0::'a) \<Longrightarrow> (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = (0::'a)

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
 2. a \<noteq> (0::'a) \<Longrightarrow> (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
[PROOF STEP]
with IH
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> (0::'a) \<or> p \<noteq> 0
(\<parallel>p\<parallel>\<^sup>2 = (0::'a)) = (p = 0)
a = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<noteq> (0::'a) \<or> p \<noteq> 0
(\<parallel>p\<parallel>\<^sup>2 = (0::'a)) = (p = 0)
a = (0::'a)

goal (1 subgoal):
 1. (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)

goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> (0::'a)

goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> (0::'a)
[PROOF STEP]
have "\<parallel>a\<parallel>\<^sup>2 + \<parallel>p\<parallel>\<^sup>2 > 0"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> (0::'a)

goal (1 subgoal):
 1. (0::'a) < sq_norm_conjugate a + \<parallel>p\<parallel>\<^sup>2
[PROOF STEP]
by (intro add_pos_nonneg, auto)
[PROOF STATE]
proof (state)
this:
(0::'a) < sq_norm_conjugate a + \<parallel>p\<parallel>\<^sup>2

goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(0::'a) < sq_norm_conjugate a + \<parallel>p\<parallel>\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(0::'a) < sq_norm_conjugate a + \<parallel>p\<parallel>\<^sup>2

goal (1 subgoal):
 1. (\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<parallel>pCons a p\<parallel>\<^sup>2 = (0::'a)) = (pCons a p = 0)

goal (1 subgoal):
 1. (\<parallel>0\<parallel>\<^sup>2 = (0::'a)) = (0 = 0)
[PROOF STEP]
qed simp


[STATEMENT]
lemma sq_norm_poly_pos [simp]:
  fixes p :: "'a :: {conjugatable_ordered_ring,ring_no_zero_divisors} poly"
  shows "\<parallel>p\<parallel>\<^sup>2 > 0 \<longleftrightarrow> p \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) < \<parallel>p\<parallel>\<^sup>2) = (p \<noteq> 0)
[PROOF STEP]
by (auto simp: less_le)


[STATEMENT]
lemma sq_norm_vec_of_poly [simp]:
  fixes p :: "'a :: conjugatable_ring poly"
  shows "\<parallel>vec_of_poly p\<parallel>\<^sup>2 = \<parallel>p\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>vec_of_poly p\<parallel>\<^sup>2 = \<parallel>p\<parallel>\<^sup>2
[PROOF STEP]
apply (unfold sq_norm_poly_def sq_norm_vec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map sq_norm (list_of_vec (vec_of_poly p))) = sum_list (map sq_norm (coeffs p))
[PROOF STEP]
apply (fold sum_mset_sum_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum>\<^sub># (mset (map sq_norm (list_of_vec (vec_of_poly p)))) = \<Sum>\<^sub># (mset (map sq_norm (coeffs p)))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma sq_norm_poly_of_vec [simp]:
  fixes v :: "'a :: conjugatable_ring vec"
  shows "\<parallel>poly_of_vec v\<parallel>\<^sup>2 = \<parallel>v\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>poly_of_vec v\<parallel>\<^sup>2 = \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
apply (unfold sq_norm_poly_def sq_norm_vec_def coeffs_poly_of_vec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map sq_norm (rev (dropWhile ((=) (0::'a)) (list_of_vec v)))) = sum_list (map sq_norm (list_of_vec v))
[PROOF STEP]
apply (fold rev_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (rev (map sq_norm (dropWhile ((=) (0::'a)) (list_of_vec v)))) = sum_list (map sq_norm (list_of_vec v))
[PROOF STEP]
apply (fold sum_mset_sum_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum>\<^sub># (mset (rev (map sq_norm (dropWhile ((=) (0::'a)) (list_of_vec v))))) = \<Sum>\<^sub># (mset (map sq_norm (list_of_vec v)))
[PROOF STEP]
apply (unfold mset_rev)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum>\<^sub># (mset (map sq_norm (dropWhile ((=) (0::'a)) (list_of_vec v)))) = \<Sum>\<^sub># (mset (map sq_norm (list_of_vec v)))
[PROOF STEP]
apply (unfold sum_mset_sum_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map sq_norm (dropWhile ((=) (0::'a)) (list_of_vec v))) = sum_list (map sq_norm (list_of_vec v))
[PROOF STEP]
by (auto intro: sum_list_map_dropWhile0)


[STATEMENT]
lemma add_neg_pos_is_real: "a < 0 \<Longrightarrow> b > 0 \<Longrightarrow> is_real (a + b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < (0::'a); (0::'a) < b\<rbrakk> \<Longrightarrow> is_real (a + b)
[PROOF STEP]
using add_pos_neg_is_real[of b a]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) < b; a < (0::'a)\<rbrakk> \<Longrightarrow> is_real (b + a)

goal (1 subgoal):
 1. \<lbrakk>a < (0::'a); (0::'a) < b\<rbrakk> \<Longrightarrow> is_real (a + b)
[PROOF STEP]
by (simp add: ac_simps)


[STATEMENT]
lemma nonneg_linorder_cases [consumes 2, case_names less eq greater]:
  assumes "0 \<le> a" and "0 \<le> b"
      and "a < b \<Longrightarrow> thesis" "a = b \<Longrightarrow> thesis" "b < a \<Longrightarrow> thesis"
  shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms pos_pos_linear
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> a
(0::'a) \<le> b
a < b \<Longrightarrow> thesis
a = b \<Longrightarrow> thesis
b < a \<Longrightarrow> thesis
\<lbrakk>(0::'a) < ?a; (0::'a) < ?b\<rbrakk> \<Longrightarrow> ?a < ?b \<or> ?a = ?b \<or> ?b < ?a

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto simp: le_less)


[STATEMENT]
lemma nonpos_linorder_cases [consumes 2, case_names less eq greater]:
  assumes "a \<le> 0" "b \<le> 0"
      and "a < b \<Longrightarrow> thesis" "a = b \<Longrightarrow> thesis" "b < a \<Longrightarrow> thesis"
  shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms neg_neg_linear
[PROOF STATE]
proof (prove)
using this:
a \<le> (0::'a)
b \<le> (0::'a)
a < b \<Longrightarrow> thesis
a = b \<Longrightarrow> thesis
b < a \<Longrightarrow> thesis
\<lbrakk>?a < (0::'a); ?b < (0::'a)\<rbrakk> \<Longrightarrow> ?a < ?b \<or> ?a = ?b \<or> ?b < ?a

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto simp: le_less)


[STATEMENT]
lemma real_linear:
  assumes "is_real a" and "is_real b" shows "a < b \<or> a = b \<or> b < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < b \<or> a = b \<or> b < a
[PROOF STEP]
using pos_pos_linear neg_neg_linear assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) < ?a; (0::'a) < ?b\<rbrakk> \<Longrightarrow> ?a < ?b \<or> ?a = ?b \<or> ?b < ?a
\<lbrakk>?a < (0::'a); ?b < (0::'a)\<rbrakk> \<Longrightarrow> ?a < ?b \<or> ?a = ?b \<or> ?b < ?a
is_real a
is_real b

goal (1 subgoal):
 1. a < b \<or> a = b \<or> b < a
[PROOF STEP]
by (auto dest: less_trans[of _ 0])


[STATEMENT]
lemma real_linorder_cases [consumes 2, case_names less eq greater]:
  assumes real: "is_real a" "is_real b"
      and cases: "a < b \<Longrightarrow> thesis" "a = b \<Longrightarrow> thesis" "b < a \<Longrightarrow> thesis"
  shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using real_linear[OF real] cases
[PROOF STATE]
proof (prove)
using this:
a < b \<or> a = b \<or> b < a
a < b \<Longrightarrow> thesis
a = b \<Longrightarrow> thesis
b < a \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma real_mult_eq_0_iff:
  assumes a: "is_real a" and b: "is_real b"
  shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a * b = (0::'a)) = (a = (0::'a) \<or> b = (0::'a))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a * b = (0::'a)) = (a = (0::'a) \<or> b = (0::'a))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a * b = (0::'a)) = (a = (0::'a) \<or> b = (0::'a))
[PROOF STEP]
assume l: "a * b = 0" and "a \<noteq> 0" and "b \<noteq> 0"
[PROOF STATE]
proof (state)
this:
a * b = (0::'a)
a \<noteq> (0::'a)
b \<noteq> (0::'a)

goal (1 subgoal):
 1. (a * b = (0::'a)) = (a = (0::'a) \<or> b = (0::'a))
[PROOF STEP]
with a b
[PROOF STATE]
proof (chain)
picking this:
is_real a
is_real b
a * b = (0::'a)
a \<noteq> (0::'a)
b \<noteq> (0::'a)
[PROOF STEP]
have "a < 0 \<or> 0 < a" and "b < 0 \<or> 0 < b"
[PROOF STATE]
proof (prove)
using this:
is_real a
is_real b
a * b = (0::'a)
a \<noteq> (0::'a)
b \<noteq> (0::'a)

goal (1 subgoal):
 1. a < (0::'a) \<or> (0::'a) < a &&& b < (0::'a) \<or> (0::'a) < b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a < (0::'a) \<or> (0::'a) < a
b < (0::'a) \<or> (0::'a) < b

goal (1 subgoal):
 1. (a * b = (0::'a)) = (a = (0::'a) \<or> b = (0::'a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a < (0::'a) \<or> (0::'a) < a
b < (0::'a) \<or> (0::'a) < b
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
a < (0::'a) \<or> (0::'a) < a
b < (0::'a) \<or> (0::'a) < b

goal (1 subgoal):
 1. False
[PROOF STEP]
using mult_pos_pos[of a b] mult_pos_neg[of a b] mult_neg_pos[of a b] mult_neg_neg[of a b]
[PROOF STATE]
proof (prove)
using this:
a < (0::'a) \<or> (0::'a) < a
b < (0::'a) \<or> (0::'a) < b
\<lbrakk>(0::'a) < a; (0::'a) < b\<rbrakk> \<Longrightarrow> (0::'a) < a * b
\<lbrakk>(0::'a) < a; b < (0::'a)\<rbrakk> \<Longrightarrow> a * b < (0::'a)
\<lbrakk>a < (0::'a); (0::'a) < b\<rbrakk> \<Longrightarrow> a * b < (0::'a)
\<lbrakk>a < (0::'a); b < (0::'a)\<rbrakk> \<Longrightarrow> (0::'a) < a * b

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp:l)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. (a * b = (0::'a)) = (a = (0::'a) \<or> b = (0::'a))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a * b = (0::'a); a \<noteq> (0::'a); b \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (a * b = (0::'a)) = (a = (0::'a) \<or> b = (0::'a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a * b = (0::'a); a \<noteq> (0::'a); b \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a * b = (0::'a); a \<noteq> (0::'a); b \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (a * b = (0::'a)) = (a = (0::'a) \<or> b = (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a * b = (0::'a)) = (a = (0::'a) \<or> b = (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_pos_mult_max:
  fixes a b c :: "'a :: semiring_real_line"
  assumes c: "c > 0" and a: "is_real a" and b: "is_real b"
  shows "c * max a b = max (c * a) (c * b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * max a b = max (c * a) (c * b)
[PROOF STEP]
by (rule hom_max, simp add: real_mult_le_cancel_left_pos[OF a b c])


[STATEMENT]
lemma power_both_mono: "1 \<le> a \<Longrightarrow> m \<le> n \<Longrightarrow> a \<le> b \<Longrightarrow> a ^ m \<le> b ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(1::'a) \<le> a; m \<le> n; a \<le> b\<rbrakk> \<Longrightarrow> a ^ m \<le> b ^ n
[PROOF STEP]
using power_mono[of a b n] power_increasing[of m n a]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> b; (0::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ n \<le> b ^ n
\<lbrakk>m \<le> n; (1::'a) \<le> a\<rbrakk> \<Longrightarrow> a ^ m \<le> a ^ n

goal (1 subgoal):
 1. \<lbrakk>(1::'a) \<le> a; m \<le> n; a \<le> b\<rbrakk> \<Longrightarrow> a ^ m \<le> b ^ n
[PROOF STEP]
by (auto simp: order.trans[OF zero_le_one])


[STATEMENT]
lemma power_pos:
  assumes a0: "0 < a" shows "0 < a ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < a ^ n
[PROOF STEP]
by (induct n, insert mult_strict_mono[OF a0] a0, auto)


[STATEMENT]
lemma power_neg:
  assumes a0: "a < 0" shows "odd n \<Longrightarrow> a ^ n < 0" and "even n \<Longrightarrow> a ^ n > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (odd n \<Longrightarrow> a ^ n < (0::'a)) &&& (even n \<Longrightarrow> (0::'a) < a ^ n)
[PROOF STEP]
by (atomize(full), induct n, insert a0, auto simp add: mult_pos_neg2 mult_neg_neg)


[STATEMENT]
lemma power_ge_0_iff:
  assumes a: "is_real a"
  shows "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
is_real a

goal (1 subgoal):
 1. ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. a < (0::'a) \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
 2. a = (0::'a) \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
 3. (0::'a) < a \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
assume "a < 0"
[PROOF STATE]
proof (state)
this:
a < (0::'a)

goal (3 subgoals):
 1. a < (0::'a) \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
 2. a = (0::'a) \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
 3. (0::'a) < a \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
with power_neg[OF this, of n]
[PROOF STATE]
proof (chain)
picking this:
odd n \<Longrightarrow> a ^ n < (0::'a)
even n \<Longrightarrow> (0::'a) < a ^ n
a < (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
odd n \<Longrightarrow> a ^ n < (0::'a)
even n \<Longrightarrow> (0::'a) < a ^ n
a < (0::'a)

goal (1 subgoal):
 1. ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
by(cases "even n", auto)
[PROOF STATE]
proof (state)
this:
((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
 2. (0::'a) < a \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
 2. (0::'a) < a \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
assume "0 < a"
[PROOF STATE]
proof (state)
this:
(0::'a) < a

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
 2. (0::'a) < a \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
with power_pos[OF this]
[PROOF STATE]
proof (chain)
picking this:
(0::'a) < a ^ ?n
(0::'a) < a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(0::'a) < a ^ ?n
(0::'a) < a

goal (1 subgoal):
 1. ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)

goal (1 subgoal):
 1. a = (0::'a) \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = (0::'a) \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
assume "a = 0"
[PROOF STATE]
proof (state)
this:
a = (0::'a)

goal (1 subgoal):
 1. a = (0::'a) \<Longrightarrow> ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = (0::'a)

goal (1 subgoal):
 1. ((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)
[PROOF STEP]
by (auto simp:power_0_left)
[PROOF STATE]
proof (state)
this:
((0::'a) \<le> a ^ n) = ((0::'a) \<le> a \<or> even n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nonneg_power_less:
  assumes "0 \<le> a" and "0 \<le> b" shows "a^n < b^n \<longleftrightarrow> n > 0 \<and> a < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a ^ n < b ^ n) = (0 < n \<and> a < b)
[PROOF STEP]
proof (insert assms, induct n arbitrary: a b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ 0 < b ^ 0) = (0 < 0 \<and> a < b)
 2. \<And>n a b. \<lbrakk>\<And>a b. \<lbrakk>(0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ n < b ^ n) = (0 < n \<and> a < b); (0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a
(0::'a) \<le> b

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ 0 < b ^ 0) = (0 < 0 \<and> a < b)
 2. \<And>n a b. \<lbrakk>\<And>a b. \<lbrakk>(0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ n < b ^ n) = (0 < n \<and> a < b); (0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<le> a
(0::'a) \<le> b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> a
(0::'a) \<le> b

goal (1 subgoal):
 1. (a ^ 0 < b ^ 0) = (0 < 0 \<and> a < b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a ^ 0 < b ^ 0) = (0 < 0 \<and> a < b)

goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>\<And>a b. \<lbrakk>(0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ n < b ^ n) = (0 < n \<and> a < b); (0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>\<And>a b. \<lbrakk>(0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ n < b ^ n) = (0 < n \<and> a < b); (0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(0::'a) \<le> ?a1; (0::'a) \<le> ?b1\<rbrakk> \<Longrightarrow> (?a1 ^ n < ?b1 ^ n) = (0 < n \<and> ?a1 < ?b1)
(0::'a) \<le> a
(0::'a) \<le> b

goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>\<And>a b. \<lbrakk>(0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ n < b ^ n) = (0 < n \<and> a < b); (0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
note a = \<open>0 \<le> a\<close>
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a

goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>\<And>a b. \<lbrakk>(0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ n < b ^ n) = (0 < n \<and> a < b); (0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
note b = \<open>0 \<le> b\<close>
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> b

goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>\<And>a b. \<lbrakk>(0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ n < b ^ n) = (0 < n \<and> a < b); (0::'a) \<le> a; (0::'a) \<le> b\<rbrakk> \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
proof (cases "n > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < n \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
 2. \<not> 0 < n \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < n

goal (2 subgoals):
 1. 0 < n \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
 2. \<not> 0 < n \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
from a b
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<le> a
(0::'a) \<le> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> a
(0::'a) \<le> b

goal (1 subgoal):
 1. (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
proof (cases rule: nonneg_linorder_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. a < b \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
 2. a = b \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
 3. b < a \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
a < b

goal (3 subgoals):
 1. a < b \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
 2. a = b \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
 3. b < a \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a < b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a < b

goal (1 subgoal):
 1. (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
by (auto simp: Suc.hyps[OF a b] True intro!:mult_strict_mono' a b zero_le_power)
[PROOF STATE]
proof (state)
this:
(a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)

goal (2 subgoals):
 1. a = b \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
 2. b < a \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = b \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
 2. b < a \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
case eq
[PROOF STATE]
proof (state)
this:
a = b

goal (2 subgoals):
 1. a = b \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
 2. b < a \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = b

goal (1 subgoal):
 1. (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)

goal (1 subgoal):
 1. b < a \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b < a \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
case greater
[PROOF STATE]
proof (state)
this:
b < a

goal (1 subgoal):
 1. b < a \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
with Suc.hyps[OF b a] True
[PROOF STATE]
proof (chain)
picking this:
(b ^ n < a ^ n) = (0 < n \<and> b < a)
0 < n
b < a
[PROOF STEP]
have "b ^ n < a ^ n"
[PROOF STATE]
proof (prove)
using this:
(b ^ n < a ^ n) = (0 < n \<and> b < a)
0 < n
b < a

goal (1 subgoal):
 1. b ^ n < a ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b ^ n < a ^ n

goal (1 subgoal):
 1. b < a \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
with mult_strict_mono'[OF greater this] b greater
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(0::'a) \<le> b; (0::'a) \<le> b ^ n\<rbrakk> \<Longrightarrow> b * b ^ n < a * a ^ n
(0::'a) \<le> b
b < a
b ^ n < a ^ n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) \<le> b; (0::'a) \<le> b ^ n\<rbrakk> \<Longrightarrow> b * b ^ n < a * a ^ n
(0::'a) \<le> b
b < a
b ^ n < a ^ n

goal (1 subgoal):
 1. (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)

goal (1 subgoal):
 1. \<not> 0 < n \<Longrightarrow> (a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(a ^ Suc n < b ^ Suc n) = (0 < Suc n \<and> a < b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma power_strict_mono:
  shows "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a ^ n < b ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < b; (0::'a) \<le> a; 0 < n\<rbrakk> \<Longrightarrow> a ^ n < b ^ n
[PROOF STEP]
by (subst nonneg_power_less, auto)