Up to index of Isabelle/HOL/Tame
theory EnumeratorProps(* ID: $Id: EnumeratorProps.thy,v 1.3 2006/01/13 19:18:50 nipkow Exp $
Author: Gertrud Bauer, Tobias Nipkow
*)
header{* Properties of Patch Enumeration*}
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"
by(simp add:indexToVertexList_def)
(***************************** 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"
by (auto simp add: enumAppend_length1)
(*********** 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"
apply (simp add: list_all_iff)
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