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