Theory EnumeratorProps

Up to index of Isabelle/HOL/Tame

theory EnumeratorProps
imports Enumerator GraphProps
begin

```(*  ID:         \$Id: EnumeratorProps.thy,v 1.3 2006/01/13 19:18:50 nipkow Exp \$
Author:     Gertrud Bauer, Tobias Nipkow
*)

theory EnumeratorProps
imports Enumerator GraphProps
begin

lemma length_hideDupsRec[simp]: "!!x. length(hideDupsRec x xs) = length xs"
by(induct xs) auto

lemma length_hideDups[simp]: "length(hideDups xs) = length xs"
by(cases xs) simp_all

lemma length_indexToVertexList[simp]:
"length(indexToVertexList x y xs) = length xs"

(***************************** List not decreasing ***************************)
constdefs increasing:: "('a::linorder) list => bool"
"increasing ls ≡ ∀ x y as bs. ls = as @ x # y # bs --> x ≤ y"

lemma increasing1: "!! as x. increasing ls ==> ls = as @ x # cs @ y # bs ==> x ≤ y"
proof (induct cs)
case Nil then show ?case
by (auto simp: increasing_def)
next
case (Cons c cs) then show ?case
apply (subgoal_tac "c ≤ y")
apply (force simp: increasing_def)
apply (rule_tac Cons) by simp_all
qed

lemma increasing2: "increasing (as@bs) ==> x ∈ set as ==> y ∈ set bs ==> x ≤ y"
proof-
assume n:"increasing (as@bs)" and x:"x ∈ set as" and y: "y ∈ set bs"
from x obtain as' as'' where as: "as = as' @ x # as''" by (auto simp: in_set_conv_decomp)
from y obtain bs' bs'' where bs: "bs = bs' @ y # bs''" by (auto simp: in_set_conv_decomp)
from n as bs show ?thesis
apply (auto intro!: increasing1)
apply (subgoal_tac "as' @ x # as'' @ bs' @ y # bs'' = as' @ x # (as'' @ bs') @ y # bs''")
by (assumption) auto
qed

lemma increasing3: "∀ as bs. (ls = as @ bs --> (∀ x ∈ set as. ∀ y ∈ set bs. x ≤ y)) ==> increasing (ls)"
apply (simp add: increasing_def) apply safe
proof -
fix as bs x y
assume p: "∀asa bsa. as @ x # y # bs = asa @ bsa --> (∀x∈set asa. ∀y∈set bsa. x ≤ y)"
then have p': "!! asa bsa. as @ x # y # bs = asa @ bsa ==> (∀x∈set asa. ∀y∈set bsa. x ≤ y)" by auto
then have "(∀x∈set (as @ [x]). ∀y∈set (y # bs). x ≤ y)" by (rule_tac p') auto
then show "x ≤ y" by (auto simp: increasing_def)
qed

lemma increasing4: "increasing (as@bs) ==> increasing as"
apply (simp add: increasing_def) apply safe by auto

lemma increasing5: "increasing (as@bs) ==> increasing bs"
proof -
assume nd: "increasing (as@bs)"
then have r: "!! x y asa bsa. (∃asa bsa. as @ bs = asa @ x # y # bsa) ==> x ≤ y" by (auto simp: increasing_def)
show ?thesis apply (simp add: increasing_def) apply (intro allI impI) apply (rule_tac r)
apply auto apply (intro exI) apply (subgoal_tac "as @ asa @ x # y # bs = (as @ asa) @ x # y # bs")
by assumption  auto
qed

(*********************************** EnumeratorProps *************************************)

(********** enumBase ***********)

lemma enumBase_length: "ls ∈ set (enumBase nmax) ==> length ls = 1"
by (auto simp: enumBase_def)

lemma enumBase_lenght2: "∀ ls ∈ set (enumBase nmax). length ls = 1"
by (auto simp: enumBase_def)

lemma enumBase_bound: "∀ y ∈ set (enumBase nmax). ∀ z ∈ set y. z ≤  nmax"
by (auto simp: enumBase_def)

lemmas enumBase_simps = enumBase_length enumBase_lenght2 enumBase_bound

(********** enumAppend ************)

lemma enumAppend_length1: "(∀ ls ∈ set lss. length ls = k) ==> ls2 ∈ set (enumAppend nmax lss) ==> length ls2 = k + 1"
by (auto simp: enumAppend_def)

lemma enumAppend_length: "(∀ ls ∈ set lss. length ls = k) ==> (∀ ls2 ∈ set (enumAppend nmax lss). length ls2 = Suc k)"
by (auto simp: enumAppend_def)

lemma enumAppend_length_rec: "(∀ ls ∈ set lss. length ls = k) ==>
(∀ ls2 ∈ set (((enumAppend nmax)^n) lss).  length ls2 = k + n)"
apply (induct n) by (auto intro!: enumAppend_length)

lemma enumAppend_length_rec2: "(∀ ls ∈ set lss. length ls = k)
==> ls2 ∈ set (((enumAppend nmax)^n) lss) ==>  length ls2 = k + n"
by (auto dest: enumAppend_length_rec)

lemma enumAppend_length_rec3: "(∀ ls ∈ set lss. length ls = 1)
==> ls2 ∈ set (((enumAppend nmax)^n) lss) ==>  length ls2 = Suc n"
by (auto dest: enumAppend_length_rec2)

lemma enumAppend_bound: "ls ∈ set ((enumAppend nmax) lss) ==>
∀ y ∈ set lss. ∀ z ∈ set y. z ≤ nmax ==> x ∈ set ls ==> x ≤  nmax"
by (auto simp add: enumAppend_def split: split_if_asm)

lemma enumAppend_bound_rec: "ls ∈ set (((enumAppend nmax)^n) lss) ==>
∀ y ∈ set lss. ∀ z ∈ set y. z ≤ nmax ==> x ∈ set ls ==> x ≤  nmax"
proof -
assume ls: "ls ∈ set ((enumAppend nmax ^ n) lss)" and lss: "∀y∈set lss. ∀z∈set y. z ≤ nmax" and x: "x ∈ set ls"
have ind:"!! lss. ∀y∈set lss. ∀z∈set y. z ≤ nmax ==> ∀ y ∈ set (((enumAppend nmax)^n) lss). ∀ z ∈ set y. z ≤ nmax"
proof (induct n)
case 0 then show ?case by auto
next
case (Suc n) show ?case apply (intro ballI) apply (rule enumAppend_bound) by (auto intro!: Suc)
qed
with lss have "∀ y ∈ set (((enumAppend nmax)^n) lss). ∀ z ∈ set y. z ≤ nmax" apply (rule_tac ind) .
with ls x show ?thesis by auto
qed

lemma enumAppend_increase_rec:
"!! m as bs. ls ∈ set (((enumAppend nmax) ^ m) (enumBase nmax)) ==>
as @ bs = ls ==>  ∀ x ∈ set as. ∀ y ∈ set bs. x ≤ y"
apply (induct ls rule: rev_induct) apply force apply auto apply (case_tac "m") apply simp  apply (drule_tac enumBase_length)
apply (case_tac as) apply simp_all
proof -
fix x xs m as bs xa xb n
assume ih: "!!m as bs.
[|xs ∈ set ((enumAppend nmax ^ m) (enumBase nmax)); as @ bs = xs|]
==> ∀x∈set as. ∀xa∈set bs. x ≤ xa"
and xs:"xs @ [x] ∈ set (enumAppend nmax ((enumAppend nmax ^ n) (enumBase nmax)))"
and asbs: "as @ bs = xs @ [x]" and xa:"xa ∈ set as" and xb: "xb ∈ set bs" and m: "m = Suc n"
from ih have ih2: "!! as bs x y. [|xs ∈ set ((enumAppend nmax ^ n) (enumBase nmax)); as @ bs = xs; x ∈ set as; y ∈ set bs|]
==> x ≤ y" by auto

from xb have "bs ≠ []"  by auto
then obtain bs' b where bs': "bs = bs' @ [b]" apply (cases rule: rev_exhaust) by auto
with asbs have beq:"b = x" by auto
from bs' asbs have xs': "as @ bs' = xs" by auto
with xs have "xa ≤ x"
proof (cases "xs" rule: rev_exhaust)
case Nil with xa xs' show ?thesis by auto
next
case (snoc ys y)
have "xa ≤ y"
proof (cases "xa = y")
case True then show ?thesis by auto
next
case False
from xa xs' have "xa ∈ set xs" by auto
with False snoc have "xa ∈ set ys" by auto
with xs snoc  show ?thesis
apply (rule_tac ih2)
by (auto simp: enumAppend_def)
qed
with xs snoc show "xa ≤ x" by (auto simp: enumAppend_def split:split_if_asm)
qed
then show "xa ≤ xb" apply (cases "xb = b") apply (simp add: beq)
proof (rule_tac ih2)
from xs
show "xs ∈ set ((enumAppend nmax ^ n) (enumBase nmax))"
by (auto simp: enumAppend_def)
next
from xs' show "as @ bs' = xs" by auto
next
from xa show "xa ∈ set as" by auto
next
assume "xb ≠ b"
with xb bs' show "xb ∈ set bs'" by auto
qed
qed

lemma enumAppend_length1: "!!ls. ls ∈ set (((enumAppend nmax)^n) lss) ==>
(∀l ∈ set lss. |l| = k) ==> |ls| = k + n"
apply (induct n)
apply simp
by (auto simp add:enumAppend_def split: split_if_asm)

lemma enumAppend_length2: "!!ls. ls ∈ set (((enumAppend nmax)^n) lss) ==>
(!!l. l ∈ set lss ==> |l| = k) ==> K = k + n ==> |ls| = K"

(*********** enum *********)

lemma enum_enumerator:
"enum i j = enumerator i j"
by(simp add: enum_def enumTab_def tabulate2_def tabulate_def tabulate'_def sub_def sub1_def)

(*********** enumerator *********)

lemma enumerator_hd: "ls ∈ set (enumerator m n) ==> hd ls = 0"
by (auto simp: enumerator_def split: split_if_asm)

lemma enumerator_last: "ls ∈ set (enumerator m n) ==> last ls = (n - 1)"
by (auto simp: enumerator_def split: split_if_asm)

lemma enumerator_length: "ls ∈ set (enumerator m n) ==> 2 ≤ length ls"
by (auto simp: enumerator_def split: split_if_asm)

lemmas set_enumerator_simps = enumerator_hd enumerator_last enumerator_length

lemma enumerator_not_empty[dest]: "ls ∈ set (enumerator m n) ==> ls ≠  []"
apply (subgoal_tac "2 ≤ length ls") apply force  by (rule enumerator_length)

lemma enumerator_length2: "ls ∈ set (enumerator m n) ==> 2 < m ==> length ls = m"
proof -
assume ls:"ls ∈ set (enumerator m n)" and m: "2 < m"
def k ≡ "m - 3"
with m have k: "m = k + 3" by arith
with ls have "ls ∈ set (enumerator (k+3) n)" by auto
then have "length ls = k + 3"
apply (auto simp: enumerator_def enumBase_def)
apply (erule enumAppend_length2) by auto
with k show ?thesis by simp
qed

lemma enumerator_bound: "ls ∈ set (enumerator m nmax) ==>
0 < nmax ==> x ∈ set ls ==> x < nmax"
apply (auto simp: enumerator_def split: split_if_asm)
apply (subgoal_tac "x ≤ nmax - 2") apply arith
apply (rule_tac enumAppend_bound_rec) by(auto simp:enumBase_simps)

lemma enumerator_bound2: "ls ∈ set (enumerator m nmax) ==> 1 < nmax ==> x ∈ set (butlast ls) ==> x < nmax - Suc 0"
apply (auto simp: enumerator_def split: split_if_asm)
apply (subgoal_tac "x ≤  (nmax - 2)") apply arith
apply (rule_tac enumAppend_bound_rec) by(auto simp:enumBase_simps)

lemma enumerator_bound3: "ls ∈ set (enumerator m nmax) ==> 1 < nmax ==> last (butlast ls) < nmax - Suc 0"
apply (case_tac "ls" rule: rev_exhaust) apply force
apply (rule_tac enumerator_bound2) apply assumption
apply auto
apply (case_tac "ys" rule: rev_exhaust) apply simp
apply (subgoal_tac "2 ≤ length (ys @ [y])") apply simp
apply (rule_tac enumerator_length) by auto

lemma enumerator_increase: "!! as bs. ls ∈ set (enumerator m nmax) ==>  as @ bs = ls ==> ∀ x ∈ set as. ∀ y ∈ set bs. x ≤ y"
apply (auto simp: enumerator_def del: Nat.diff_is_0_eq' split: split_if_asm intro: enumAppend_increase_rec)
apply (case_tac as) apply simp apply simp
apply (case_tac bs rule: rev_exhaust)  apply simp apply simp apply auto
apply (drule_tac enumAppend_bound_rec) apply (auto simp:enumBase_simps) apply arith
by (auto dest!: enumAppend_increase_rec)

lemma enumerator_increasing: "ls ∈ set (enumerator m nmax) ==> increasing ls"
apply (rule increasing3)
by (auto dest: enumerator_increase)

constdefs incrIndexList:: "nat list => nat => nat => bool"
"incrIndexList ls m nmax ≡
1 < m ∧ 1 < nmax ∧
hd ls = 0 ∧ last ls = (nmax - 1) ∧ length ls = m
∧ last (butlast ls) < last ls ∧ increasing ls"

lemma incrIndexList_1lem[simp]: "incrIndexList ls m nmax ==> Suc 0 < m"
by (unfold incrIndexList_def) simp

lemma incrIndexList_1len[simp]: "incrIndexList ls m nmax ==> Suc 0 < nmax"
by (unfold incrIndexList_def) simp

lemma incrIndexList_help2[simp]: "incrIndexList ls m nmax ==> hd ls = 0"
by (unfold incrIndexList_def) simp

lemma incrIndexList_help21[simp]: "incrIndexList (l # ls) m nmax ==> l = 0"
by (auto dest: incrIndexList_help2)

lemma incrIndexList_help3[simp]: "incrIndexList ls m nmax ==> last ls = (nmax - (Suc 0))"
by (unfold incrIndexList_def)  simp

lemma incrIndexList_help4[simp]: "incrIndexList ls m nmax ==> length ls = m "
by (unfold incrIndexList_def)  simp

lemma incrIndexList_help5[intro]: "incrIndexList ls m nmax ==>  last (butlast ls) < nmax - Suc 0"
by (unfold incrIndexList_def) auto

lemma incrIndexList_help6[simp]: "incrIndexList ls m nmax ==> increasing ls"
by (unfold incrIndexList_def) simp

lemma incrIndexList_help7[simp]: "incrIndexList ls m nmax ==> ls ≠ []"
apply (subgoal_tac "length ls ≠  0") apply force
apply simp
apply (subgoal_tac "1 < m")  apply arith apply force done

lemma incrIndexList_help71[simp]: "¬ incrIndexList [] m nmax"
by (auto dest: incrIndexList_help7)

lemma incrIndexList_help8[simp]: "incrIndexList ls m nmax ==> butlast ls ≠ []"
proof (rule ccontr)
assume props: "incrIndexList ls m nmax" and butl: "¬ butlast ls ≠ []"
then have "ls ≠ []" by auto
then have ls': "ls = (butlast ls) @ [last ls]" by auto
def l ≡ "last ls"
with butl ls' have "ls = [l]" by auto
then have "length ls = 1" by auto
with props have "m = 1" by auto
with props show "False" by (auto dest: incrIndexList_1lem)
qed

lemma incrIndexList_help81[simp]: "¬ incrIndexList [l] m nmax"
by (auto dest: incrIndexList_help8)

lemma incrIndexList_help9[intro]: "(incrIndexList ls m nmax)  ==>
x ∈ set (butlast ls) ==> x ≤ nmax - 2"
proof -
assume props: "(incrIndexList ls m nmax)"  and x: "x ∈ set (butlast ls)"
then have "last (butlast ls) < last ls" by auto
with props have "last (butlast ls) < nmax - 1" by auto
then have leq: "last (butlast ls) ≤  nmax - 2" by arith
from props  have "ls ≠ []" by auto
then have ls1: "ls = butlast ls @ [last ls]" by auto
def ls' ≡ "(butlast (butlast ls))"
def last2 ≡ "last (butlast ls)"
def last1 ≡ "last ls"
from props  have "butlast ls ≠ []" by auto
with ls'_def last2_def have bls: "butlast ls = ls' @ [last2]" by auto
with last1_def ls1 props have ls3: "ls = ls' @ [last2] @ [last1]" by auto
from props  have "increasing ls" by auto
with ls3 have increasing: "increasing (ls' @ ([last2] @ [last1]))" by auto
then have "x ∈ set ls' ==> x ≤ last2" by (auto intro: increasing2)
then have "x ∈ set (ls' @ [last2]) ==> x ≤ last2" by auto
with bls x have "x ≤ last2" by auto
with leq last2_def show ?thesis by auto
qed

lemma incrIndexList_help10[intro]: "(incrIndexList ls m nmax)  ==>
x ∈ set ls ==> x < nmax" apply (cases ls rule: rev_exhaust) apply auto
apply (frule incrIndexList_help3) apply (auto dest: incrIndexList_1len)
apply (frule incrIndexList_help9) apply auto apply (drule incrIndexList_1len)
by arith

lemma enumerator_correctness: "2 < m ==> 1 < nmax ==>
ls ∈ set (enumerator m nmax) ==>
incrIndexList ls m nmax"
proof -
assume m: "2 < m" and nmax: "1 < nmax" and enum: "ls ∈ set (enumerator m nmax)"
then have "(hd ls = 0 ∧ last ls = (nmax - 1) ∧ length ls = m ∧ last (butlast ls) < last ls ∧  increasing ls)"
by (auto intro: enumerator_increasing enumerator_hd enumerator_last enumerator_length2 enumerator_bound3 simp: set_enumerator_simps)
with m nmax show ?thesis by (unfold incrIndexList_def) auto
qed

lemma enumerator_completeness_help: "!! ls. increasing ls ==> ls ≠ [] ==> length ls = Suc ks ==> list_all (λx. x < Suc nmax) ls ==> ls ∈ set ((enumAppend nmax ^ ks) (enumBase nmax))"
proof (induct ks)
case 0
assume "increasing ls" "ls ≠ []" "length ls = Suc 0" "list_all (λx. x < Suc nmax) ls"
then have "∃ x. ls = [x]"
apply (case_tac "ls::nat list") by auto
then obtain x where ls1: "ls = [x]" by auto
with 0 have "x < Suc nmax" by auto
with ls1 show ?case apply (simp add: enumBase_def) by auto
next
case (Suc n)
def ls' ≡ "butlast ls"
def l ≡ "last ls"
def ll ≡ "last ls'"
def bl ≡ "butlast ls'"
def ls'list ≡ "(enumAppend nmax ^ n) (enumBase nmax)"
then have short: "(enumAppend nmax ^ n) (enumBase nmax) = ls'list" by simp
from Suc have "ls ≠ []" by auto
then have "ls = butlast ls @ [last ls]" by auto
with ls'_def l_def have ls1: "ls = ls' @ [l]" by auto
with Suc have "length ls' = Suc n" by auto
then have ls'ne: "ls' ≠ []" by auto
with ll_def bl_def have ls'1: "ls' = bl @ [ll]" by auto
then have ll_in_ls': "ll ∈ set ls'" by simp
from Suc ls1 have "list_all (λx. x < Suc nmax) ls'" by auto
with ll_in_ls' have "ll < Suc nmax" by (induct ls') auto
with ll_def have llsmall: "last ls' ≤ nmax"  by auto

from ls1 have l_in_ls: "l ∈ set ls" by auto
from Suc have "list_all (λx. x < Suc nmax) ls" by auto
with l_in_ls have "l < Suc nmax" by (induct ls) auto
then have lo: "l ≤ nmax" by auto

from Suc ls1 ls'1 have "increasing ((bl @ [ll]) @ [l])" by auto
then have "ll ≤  l" by (rule increasing2) auto
with ll_def have lu: "last ls' ≤ l" by simp

from Suc ls1 have vors: "ls' ∈ set ((enumAppend nmax ^ n) (enumBase nmax))"
by (rule_tac Suc) (auto intro: increasing4)
with short have "ls' ∈ set ls'list"  by  auto
with short llsmall ls1 lo lu show ?case  apply simp  apply (simp add: enumAppend_def)
apply (intro bexI) by auto
qed

lemma enumerator_completeness: "2 < m ==> incrIndexList ls m nmax ==>
ls ∈ set (enumerator m nmax)"
proof -
assume m: "2 < m" and props: "incrIndexList ls m nmax"
then have props': "(hd ls = 0 ∧ last ls = (nmax - 1)
∧ length ls = m ∧ last (butlast ls) < last ls ∧  increasing ls)"
by (unfold incrIndexList_def) auto
show ?thesis
proof -
have props'': "hd ls = 0 ∧ last ls = (nmax - 1) ∧ length ls = m ∧
increasing ls"
by (auto simp: props')
show "ls ∈ set (enumerator m nmax)"
proof -
from m props'' have l_ls: "2 < length ls"  by auto
then have "∃ x y ks. ls = x # ks @ [y]"
apply (case_tac "ls::(nat list)") apply auto
apply (case_tac "list" rule: rev_exhaust) by auto
then obtain x y ks where "ls = x # ks @ [y]" by auto
with props'' have ls': "ls = 0 # ks @ [nmax - 1]" by auto
with l_ls have l_ms: "0 < length ks" by auto
then have ms_ne: "ks ≠ []" by auto
from ls' have lks: "length ks = length ls - 2" by auto
from props'' have nd: "increasing ls" by auto
from props'' have "!! z. z ∈ set ks ==> 0 ≤ z" by auto
from props'' ls' have "increasing ((0 # ks) @ [nmax - 1])" by auto
then have z: "!! z. z ∈ set ks ==> z ≤ (nmax - 1)"
by (drule_tac increasing2) auto
from props  ls' have z': "!! z. z ∈ set ks ==> z ≤ (nmax - 2)" by auto

have "ks ∈ set ((enumAppend (nmax - 2)
^ (length ks - Suc 0)) (enumBase (nmax - 2)))"
proof (cases "ks = []")
case True with ms_ne show ?thesis by simp
next
case False
from props'' have "increasing ls" by auto
with ls' have "increasing (0 # ks)" by (auto intro: increasing4)
then have "increasing ([0] @ ks)" by auto
then have ndks: "increasing ks" by (rule_tac increasing5)
have listall: "list_all (λx. x < Suc (nmax - 2)) ks"
by (auto dest: z')
with False ndks show ?thesis
apply (rule_tac enumerator_completeness_help) by auto
qed
with lks props' have
"ks ∈ set ((enumAppend (nmax - 2) ^ (m - 3)) (enumBase (nmax - 2)))" by auto
with m ls' show ?thesis by (simp add: enumerator_def)
qed
qed
qed

lemma enumerator_equiv[simp]:
"2 < n ==> 1 < m ==> is ∈ set(enumerator n m) = incrIndexList is n m"
by (auto intro: enumerator_correctness enumerator_completeness)

end```

lemma length_hideDupsRec:

`  |hideDupsRec x xs| = |xs|`

lemma length_hideDups:

`  |hideDups xs| = |xs|`

lemma length_indexToVertexList:

`  |indexToVertexList x y xs| = |xs|`

lemma increasing1:

`  [| increasing ls; ls = as @ x # cs @ y # bs |] ==> x ≤ y`

lemma increasing2:

`  [| increasing (as @ bs); x ∈ set as; y ∈ set bs |] ==> x ≤ y`

lemma increasing3:

`  ∀as bs. ls = as @ bs --> (∀x∈set as. ∀y∈set bs. x ≤ y) ==> increasing ls`

lemma increasing4:

`  increasing (as @ bs) ==> increasing as`

lemma increasing5:

`  increasing (as @ bs) ==> increasing bs`

lemma enumBase_length:

`  ls ∈ set (enumBase nmax) ==> |ls| = 1`

lemma enumBase_lenght2:

`  ∀ls∈set (enumBase nmax). |ls| = 1`

lemma enumBase_bound:

`  ∀y∈set (enumBase nmax). ∀z∈set y. z ≤ nmax`

lemmas enumBase_simps:

`  ls ∈ set (enumBase nmax) ==> |ls| = 1`
`  ∀ls∈set (enumBase nmax). |ls| = 1`
`  ∀y∈set (enumBase nmax). ∀z∈set y. z ≤ nmax`

lemmas enumBase_simps:

`  ls ∈ set (enumBase nmax) ==> |ls| = 1`
`  ∀ls∈set (enumBase nmax). |ls| = 1`
`  ∀y∈set (enumBase nmax). ∀z∈set y. z ≤ nmax`

lemma enumAppend_length1:

```  [| ∀ls∈set lss. |ls| = k; ls2.0 ∈ set (enumAppend nmax lss) |]
==> |ls2.0| = k + 1```

lemma enumAppend_length:

`  ∀ls∈set lss. |ls| = k ==> ∀ls2∈set (enumAppend nmax lss). |ls2| = Suc k`

lemma enumAppend_length_rec:

`  ∀ls∈set lss. |ls| = k ==> ∀ls2∈set ((enumAppend nmax ^ n) lss). |ls2| = k + n`

lemma enumAppend_length_rec2:

```  [| ∀ls∈set lss. |ls| = k; ls2.0 ∈ set ((enumAppend nmax ^ n) lss) |]
==> |ls2.0| = k + n```

lemma enumAppend_length_rec3:

```  [| ∀ls∈set lss. |ls| = 1; ls2.0 ∈ set ((enumAppend nmax ^ n) lss) |]
==> |ls2.0| = Suc n```

lemma enumAppend_bound:

```  [| ls ∈ set (enumAppend nmax lss); ∀y∈set lss. ∀z∈set y. z ≤ nmax; x ∈ set ls |]
==> x ≤ nmax```

lemma enumAppend_bound_rec:

```  [| ls ∈ set ((enumAppend nmax ^ n) lss); ∀y∈set lss. ∀z∈set y. z ≤ nmax;
x ∈ set ls |]
==> x ≤ nmax```

lemma enumAppend_increase_rec:

```  [| ls ∈ set ((enumAppend nmax ^ m) (enumBase nmax)); as @ bs = ls |]
==> ∀x∈set as. ∀y∈set bs. x ≤ y```

lemma enumAppend_length1:

`  [| ls ∈ set ((enumAppend nmax ^ n) lss); ∀l∈set lss. |l| = k |] ==> |ls| = k + n`

lemma enumAppend_length2:

```  [| ls ∈ set ((enumAppend nmax ^ n) lss); !!l. l ∈ set lss ==> |l| = k;
K = k + n |]
==> |ls| = K```

lemma enum_enumerator:

`  enum i j = enumerator i j`

lemma enumerator_hd:

`  ls ∈ set (enumerator m n) ==> hd ls = 0`

lemma enumerator_last:

`  ls ∈ set (enumerator m n) ==> last ls = n - 1`

lemma enumerator_length:

`  ls ∈ set (enumerator m n) ==> 2 ≤ |ls|`

lemmas set_enumerator_simps:

`  ls ∈ set (enumerator m n) ==> hd ls = 0`
`  ls ∈ set (enumerator m n) ==> last ls = n - 1`
`  ls ∈ set (enumerator m n) ==> 2 ≤ |ls|`

lemmas set_enumerator_simps:

`  ls ∈ set (enumerator m n) ==> hd ls = 0`
`  ls ∈ set (enumerator m n) ==> last ls = n - 1`
`  ls ∈ set (enumerator m n) ==> 2 ≤ |ls|`

lemma enumerator_not_empty:

`  ls ∈ set (enumerator m n) ==> ls ≠ []`

lemma enumerator_length2:

`  [| ls ∈ set (enumerator m n); 2 < m |] ==> |ls| = m`

lemma enumerator_bound:

`  [| ls ∈ set (enumerator m nmax); 0 < nmax; x ∈ set ls |] ==> x < nmax`

lemma enumerator_bound2:

```  [| ls ∈ set (enumerator m nmax); 1 < nmax; x ∈ set (butlast ls) |]
==> x < nmax - Suc 0```

lemma enumerator_bound3:

```  [| ls ∈ set (enumerator m nmax); 1 < nmax |]
==> last (butlast ls) < nmax - Suc 0```

lemma enumerator_increase:

`  [| ls ∈ set (enumerator m nmax); as @ bs = ls |] ==> ∀x∈set as. ∀y∈set bs. x ≤ y`

lemma enumerator_increasing:

`  ls ∈ set (enumerator m nmax) ==> increasing ls`

lemma incrIndexList_1lem:

`  incrIndexList ls m nmax ==> Suc 0 < m`

lemma incrIndexList_1len:

`  incrIndexList ls m nmax ==> Suc 0 < nmax`

lemma incrIndexList_help2:

`  incrIndexList ls m nmax ==> hd ls = 0`

lemma incrIndexList_help21:

`  incrIndexList (l # ls) m nmax ==> l = 0`

lemma incrIndexList_help3:

`  incrIndexList ls m nmax ==> last ls = nmax - Suc 0`

lemma incrIndexList_help4:

`  incrIndexList ls m nmax ==> |ls| = m`

lemma incrIndexList_help5:

`  incrIndexList ls m nmax ==> last (butlast ls) < nmax - Suc 0`

lemma incrIndexList_help6:

`  incrIndexList ls m nmax ==> increasing ls`

lemma incrIndexList_help7:

`  incrIndexList ls m nmax ==> ls ≠ []`

lemma incrIndexList_help71:

`  ¬ incrIndexList [] m nmax`

lemma incrIndexList_help8:

`  incrIndexList ls m nmax ==> butlast ls ≠ []`

lemma incrIndexList_help81:

`  ¬ incrIndexList [l] m nmax`

lemma incrIndexList_help9:

`  [| incrIndexList ls m nmax; x ∈ set (butlast ls) |] ==> x ≤ nmax - 2`

lemma incrIndexList_help10:

`  [| incrIndexList ls m nmax; x ∈ set ls |] ==> x < nmax`

lemma enumerator_correctness:

`  [| 2 < m; 1 < nmax; ls ∈ set (enumerator m nmax) |] ==> incrIndexList ls m nmax`

lemma enumerator_completeness_help:

```  [| increasing ls; ls ≠ []; |ls| = Suc ks; list_all (λx. x < Suc nmax) ls |]
==> ls ∈ set ((enumAppend nmax ^ ks) (enumBase nmax))```

lemma enumerator_completeness:

`  [| 2 < m; incrIndexList ls m nmax |] ==> ls ∈ set (enumerator m nmax)`

lemma enumerator_equiv:

`  [| 2 < n; 1 < m |] ==> (is ∈ set (enumerator n m)) = incrIndexList is n m`