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
*)

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 |] ==> xy

lemma increasing2:

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

lemma increasing3:

as bs. ls = as @ bs --> (∀x∈set as. ∀y∈set bs. xy) ==> 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. znmax

lemmas enumBase_simps:

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

lemmas enumBase_simps:

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

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. znmax; x ∈ set ls |]
  ==> xnmax

lemma enumAppend_bound_rec:

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

lemma enumAppend_increase_rec:

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

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. xy

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) |] ==> xnmax - 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