Structure llistTheory
signature llistTheory =
sig
type thm = Thm.thm
(* Definitions *)
val LAPPEND : thm
val LCONS : thm
val LDROP : thm
val LFILTER : thm
val LFINITE_def : thm
val LFLATTEN : thm
val LGENLIST_def : thm
val LHD : thm
val LLENGTH : thm
val LMAP : thm
val LNIL : thm
val LNTH : thm
val LPREFIX_def : thm
val LREPEAT_def : thm
val LSET_def : thm
val LSUFFIX_def : thm
val LTAKE : thm
val LTL : thm
val LTL_HD_def : thm
val LUNFOLD_def : thm
val LUNZIP_THM : thm
val LZIP_THM : thm
val always_def : thm
val eventually_def : thm
val every_def : thm
val exists_def : thm
val fromList_def : thm
val fromSeq_def : thm
val linear_order_to_list_f_def : thm
val llength_rel_def : thm
val llist_CASE_def : thm
val llist_TY_DEF : thm
val llist_absrep : thm
val llist_rel_def : thm
val llist_upto_def : thm
val lrep_ok_def : thm
val toList : thm
val until_def : thm
(* Theorems *)
val LAPPEND_ASSOC : thm
val LAPPEND_EQ_LNIL : thm
val LAPPEND_NIL_2ND : thm
val LAPPEND_fromList : thm
val LAPPEND_fromSeq : thm
val LCONS_11 : thm
val LCONS_NOT_NIL : thm
val LDROP1_THM : thm
val LDROP_1 : thm
val LDROP_ADD : thm
val LDROP_APPEND1 : thm
val LDROP_EQ_LNIL : thm
val LDROP_FUNPOW : thm
val LDROP_LDROP : thm
val LDROP_NONE_LFINITE : thm
val LDROP_SOME_LLENGTH : thm
val LDROP_SUC : thm
val LDROP_THM : thm
val LDROP_fromList : thm
val LDROP_fromSeq : thm
val LFILTER_APPEND : thm
val LFILTER_EQ_CONS : thm
val LFILTER_EQ_NIL : thm
val LFILTER_NIL : thm
val LFILTER_THM : thm
val LFILTER_fromList : thm
val LFILTER_fromSeq : thm
val LFINITE : thm
val LFINITE_APPEND : thm
val LFINITE_DROP : thm
val LFINITE_HAS_LENGTH : thm
val LFINITE_IMP_fromList : thm
val LFINITE_INDUCTION : thm
val LFINITE_LAPPEND_IMP_NIL : thm
val LFINITE_LFLATTEN : thm
val LFINITE_LGENLIST : thm
val LFINITE_LLENGTH : thm
val LFINITE_LNTH_NONE : thm
val LFINITE_MAP : thm
val LFINITE_STRONG_INDUCTION : thm
val LFINITE_TAKE : thm
val LFINITE_THM : thm
val LFINITE_cases : thm
val LFINITE_fromList : thm
val LFINITE_fromSeq : thm
val LFINITE_ind : thm
val LFINITE_rules : thm
val LFINITE_strongind : thm
val LFINITE_toList : thm
val LFINITE_toList_SOME : thm
val LFLATTEN_APPEND : thm
val LFLATTEN_EQ_NIL : thm
val LFLATTEN_SINGLETON : thm
val LFLATTEN_THM : thm
val LFLATTEN_fromList : thm
val LGENLIST_CHUNK_GENLIST : thm
val LGENLIST_EQ_CONS : thm
val LGENLIST_EQ_LNIL : thm
val LGENLIST_EQ_fromList : thm
val LGENLIST_EQ_fromSeq : thm
val LGENLIST_SOME : thm
val LGENLIST_SOME_compute : thm
val LHDTL_CONS_THM : thm
val LHDTL_EQ_SOME : thm
val LHD_EQ_NONE : thm
val LHD_LAPPEND : thm
val LHD_LCONS : thm
val LHD_LGENLIST : thm
val LHD_LREPEAT : thm
val LHD_LUNFOLD : thm
val LHD_THM : thm
val LHD_fromList : thm
val LHD_fromSeq : thm
val LLENGTH_0 : thm
val LLENGTH_APPEND : thm
val LLENGTH_LGENLIST : thm
val LLENGTH_LREPEAT : thm
val LLENGTH_MAP : thm
val LLENGTH_THM : thm
val LLENGTH_fromList : thm
val LLENGTH_fromSeq : thm
val LLIST_BISIMULATION : thm
val LLIST_BISIMULATION0 : thm
val LLIST_BISIMULATION_I : thm
val LLIST_BISIM_UPTO : thm
val LLIST_CASE_CONG : thm
val LLIST_CASE_EQ : thm
val LLIST_DISTINCT : thm
val LLIST_EQ : thm
val LLIST_STRONG_BISIMULATION : thm
val LL_ALL_THM : thm
val LMAP_APPEND : thm
val LMAP_LGENLIST : thm
val LMAP_LUNFOLD : thm
val LMAP_MAP : thm
val LMAP_fromList : thm
val LMAP_fromSeq : thm
val LNTH_ADD : thm
val LNTH_EQ : thm
val LNTH_HD_LDROP : thm
val LNTH_LAPPEND : thm
val LNTH_LDROP : thm
val LNTH_LGENLIST : thm
val LNTH_LLENGTH_NONE : thm
val LNTH_LMAP : thm
val LNTH_LUNFOLD : thm
val LNTH_LUNFOLD_compute : thm
val LNTH_NONE_MONO : thm
val LNTH_THM : thm
val LNTH_fromList : thm
val LNTH_fromSeq : thm
val LNTH_rep : thm
val LPREFIX_ANTISYM : thm
val LPREFIX_APPEND : thm
val LPREFIX_LCONS : thm
val LPREFIX_LNIL : thm
val LPREFIX_LUNFOLD : thm
val LPREFIX_NTH : thm
val LPREFIX_REFL : thm
val LPREFIX_TRANS : thm
val LPREFIX_fromList : thm
val LREPEAT_EQ_LNIL : thm
val LREPEAT_NIL : thm
val LREPEAT_thm : thm
val LSET : thm
val LSUFFIX : thm
val LSUFFIX_ANTISYM : thm
val LSUFFIX_REFL : thm
val LSUFFIX_TRANS : thm
val LSUFFIX_fromList : thm
val LTAKE_CONS_EQ_NONE : thm
val LTAKE_CONS_EQ_SOME : thm
val LTAKE_DROP : thm
val LTAKE_EQ : thm
val LTAKE_EQ_NONE_LNTH : thm
val LTAKE_EQ_SOME_CONS : thm
val LTAKE_IMP_LDROP : thm
val LTAKE_LAPPEND1 : thm
val LTAKE_LAPPEND2 : thm
val LTAKE_LAPPEND_fromList : thm
val LTAKE_LENGTH : thm
val LTAKE_LLENGTH_NONE : thm
val LTAKE_LLENGTH_SOME : thm
val LTAKE_LMAP : thm
val LTAKE_LNTH_EL : thm
val LTAKE_LPREFIX : thm
val LTAKE_LUNFOLD : thm
val LTAKE_NIL_EQ_NONE : thm
val LTAKE_NIL_EQ_SOME : thm
val LTAKE_SNOC_LNTH : thm
val LTAKE_TAKE_LESS : thm
val LTAKE_THM : thm
val LTAKE_fromList : thm
val LTAKE_fromSeq : thm
val LTL_EQ_NONE : thm
val LTL_HD_11 : thm
val LTL_HD_HD : thm
val LTL_HD_LCONS : thm
val LTL_HD_LNIL : thm
val LTL_HD_LTL_LHD : thm
val LTL_HD_LUNFOLD : thm
val LTL_HD_TL : thm
val LTL_HD_iff : thm
val LTL_LAPPEND : thm
val LTL_LCONS : thm
val LTL_LGENLIST : thm
val LTL_LREPEAT : thm
val LTL_LUNFOLD : thm
val LTL_THM : thm
val LTL_fromList : thm
val LTL_fromSeq : thm
val LUNFOLD : thm
val LUNFOLD_BISIMULATION : thm
val LUNFOLD_EQ : thm
val LUNFOLD_LTL_HD : thm
val LUNFOLD_THM : thm
val LUNFOLD_UNIQUE : thm
val LZIP_LUNZIP : thm
val MONO_every : thm
val MONO_exists : thm
val NOT_LFINITE_APPEND : thm
val NOT_LFINITE_DROP : thm
val NOT_LFINITE_DROP_LFINITE : thm
val NOT_LFINITE_IMP_fromSeq : thm
val NOT_LFINITE_NO_LENGTH : thm
val NOT_LFINITE_TAKE : thm
val always_DROP : thm
val always_cases : thm
val always_coind : thm
val always_conj_l : thm
val always_eventually_ind : thm
val always_rules : thm
val always_thm : thm
val eventually_cases : thm
val eventually_ind : thm
val eventually_rules : thm
val eventually_strongind : thm
val eventually_thm : thm
val eventually_until_EQN : thm
val every_LAPPEND1 : thm
val every_LAPPEND2_LFINITE : thm
val every_LDROP : thm
val every_LFILTER : thm
val every_LFILTER_imp : thm
val every_LNTH : thm
val every_coind : thm
val every_fromList_EVERY : thm
val every_fromSeq : thm
val every_strong_coind : thm
val every_thm : thm
val exists_LDROP : thm
val exists_LNTH : thm
val exists_cases : thm
val exists_fromSeq : thm
val exists_ind : thm
val exists_rules : thm
val exists_strong_ind : thm
val exists_strongind : thm
val exists_thm : thm
val exists_thm_strong : thm
val fromList_11 : thm
val fromList_EQ_LNIL : thm
val fromList_NEQ_fromSeq : thm
val fromList_fromSeq : thm
val fromSeq_11 : thm
val fromSeq_LCONS : thm
val from_toList : thm
val infinite_lnth_some : thm
val linear_order_to_llist : thm
val linear_order_to_llist_eq : thm
val llength_rel_cases : thm
val llength_rel_ind : thm
val llength_rel_rules : thm
val llength_rel_strongind : thm
val llist_Axiom : thm
val llist_Axiom_1 : thm
val llist_Axiom_1ue : thm
val llist_CASES : thm
val llist_CASE_compute : thm
val llist_forall_split : thm
val llist_rep_LCONS : thm
val llist_rep_LNIL : thm
val llist_ue_Axiom : thm
val llist_upto_cases : thm
val llist_upto_context : thm
val llist_upto_eq : thm
val llist_upto_ind : thm
val llist_upto_rel : thm
val llist_upto_rules : thm
val llist_upto_strongind : thm
val llist_upto_trans : thm
val lnth_fromList_some : thm
val lnth_some_down_closed : thm
val lrep_ok_FUNPOW_BIND : thm
val lrep_ok_MAP : thm
val lrep_ok_alt : thm
val lrep_ok_cases : thm
val lrep_ok_coind : thm
val lrep_ok_rules : thm
val numopt_BISIMULATION : thm
val prefixes_lprefix_total : thm
val toList_LAPPEND_APPEND : thm
val toList_THM : thm
val to_fromList : thm
val until_cases : thm
val until_ind : thm
val until_rules : thm
val until_strongind : thm
val llist_grammars : type_grammar.grammar * term_grammar.grammar
(*
[indexedLists] Parent theory of "llist"
[patternMatches] Parent theory of "llist"
[set_relation] Parent theory of "llist"
[LAPPEND] Definition
⊢ (∀x. LAPPEND [||] x = x) ∧
∀h t x. LAPPEND (h:::t) x = h:::LAPPEND t x
[LCONS] Definition
⊢ ∀h t.
h:::t =
llist_abs (λn. if n = 0 then SOME h else llist_rep t (n − 1))
[LDROP] Definition
⊢ (∀ll. LDROP 0 ll = SOME ll) ∧
∀n ll.
LDROP (SUC n) ll = OPTION_JOIN (OPTION_MAP (LDROP n) (LTL ll))
[LFILTER] Definition
⊢ ∀P ll.
LFILTER P ll =
if ¬exists P ll then [||]
else if P (THE (LHD ll)) then
THE (LHD ll):::LFILTER P (THE (LTL ll))
else LFILTER P (THE (LTL ll))
[LFINITE_def] Definition
⊢ LFINITE =
(λa0.
∀LFINITE'.
(∀a0.
a0 = [||] ∨ (∃h t. a0 = h:::t ∧ LFINITE' t) ⇒ LFINITE' a0) ⇒
LFINITE' a0)
[LFLATTEN] Definition
⊢ ∀ll.
LFLATTEN ll =
if every ($= [||]) ll then [||]
else if THE (LHD ll) = [||] then LFLATTEN (THE (LTL ll))
else
THE (LHD (THE (LHD ll))):::
LFLATTEN (THE (LTL (THE (LHD ll))):::THE (LTL ll))
[LGENLIST_def] Definition
⊢ (∀f. LGENLIST f NONE = LUNFOLD (λn. SOME (n + 1,f n)) 0) ∧
∀f lim.
LGENLIST f (SOME lim) =
LUNFOLD (λn. if n < lim then SOME (n + 1,f n) else NONE) 0
[LHD] Definition
⊢ ∀ll. LHD ll = llist_rep ll 0
[LLENGTH] Definition
⊢ ∀ll.
LLENGTH ll =
if LFINITE ll then SOME (@n. llength_rel ll n) else NONE
[LMAP] Definition
⊢ (∀f. LMAP f [||] = [||]) ∧ ∀f h t. LMAP f (h:::t) = f h:::LMAP f t
[LNIL] Definition
⊢ [||] = llist_abs (λn. NONE)
[LNTH] Definition
⊢ (∀ll. LNTH 0 ll = LHD ll) ∧
∀n ll. LNTH (SUC n) ll = OPTION_JOIN (OPTION_MAP (LNTH n) (LTL ll))
[LPREFIX_def] Definition
⊢ ∀l1 l2.
LPREFIX l1 l2 ⇔
case toList l1 of
NONE => l1 = l2
| SOME xs =>
case toList l2 of
NONE => LTAKE (LENGTH xs) l2 = SOME xs
| SOME ys => xs ≼ ys
[LREPEAT_def] Definition
⊢ ∀l. LREPEAT l =
if NULL l then [||]
else LGENLIST (λn. EL (n MOD LENGTH l) l) NONE
[LSET_def] Definition
⊢ ∀l x. LSET l x ⇔ ∃n. LNTH n l = SOME x
[LSUFFIX_def] Definition
⊢ ∀xs zs.
LSUFFIX xs zs ⇔ ∃ys. xs = LAPPEND (fromList ys) zs ∨ zs = [||]
[LTAKE] Definition
⊢ (∀ll. LTAKE 0 ll = SOME []) ∧
∀n ll.
LTAKE (SUC n) ll =
case LHD ll of
NONE => NONE
| SOME hd =>
case LTAKE n (THE (LTL ll)) of
NONE => NONE
| SOME tl => SOME (hd::tl)
[LTL] Definition
⊢ ∀ll.
LTL ll =
case LHD ll of
NONE => NONE
| SOME v => SOME (llist_abs (λn. llist_rep ll (n + 1)))
[LTL_HD_def] Definition
⊢ ∀ll.
LTL_HD ll =
case llist_rep ll 0 of
NONE => NONE
| SOME h => SOME (llist_abs (llist_rep ll ∘ SUC),h)
[LUNFOLD_def] Definition
⊢ ∀f z.
LUNFOLD f z =
llist_abs
(λn.
OPTION_MAP SND
(FUNPOW (λm. OPTION_BIND m (UNCURRY (K ∘ f))) n (f z)))
[LUNZIP_THM] Definition
⊢ LUNZIP [||] = ([||],[||]) ∧
∀x y t.
LUNZIP ((x,y):::t) =
(let (ll1,ll2) = LUNZIP t in (x:::ll1,y:::ll2))
[LZIP_THM] Definition
⊢ (∀l1. LZIP (l1,[||]) = [||]) ∧ (∀l2. LZIP ([||],l2) = [||]) ∧
∀h1 h2 t1 t2. LZIP (h1:::t1,h2:::t2) = (h1,h2):::LZIP (t1,t2)
[always_def] Definition
⊢ always =
(λP a0.
∃always'.
always' a0 ∧
∀a0. always' a0 ⇒ ∃h t. a0 = h:::t ∧ P (h:::t) ∧ always' t)
[eventually_def] Definition
⊢ eventually =
(λP a0.
∀eventually'.
(∀a0.
P a0 ∨ (∃h t. a0 = h:::t ∧ eventually' t) ⇒
eventually' a0) ⇒
eventually' a0)
[every_def] Definition
⊢ ∀P ll. every P ll ⇔ ¬exists ($¬ ∘ P) ll
[exists_def] Definition
⊢ exists =
(λP a0.
∀exists'.
(∀a0.
(∃h t. a0 = h:::t ∧ P h) ∨ (∃h t. a0 = h:::t ∧ exists' t) ⇒
exists' a0) ⇒
exists' a0)
[fromList_def] Definition
⊢ fromList [] = [||] ∧ ∀h t. fromList (h::t) = h:::fromList t
[fromSeq_def] Definition
⊢ ∀f. fromSeq f = LUNFOLD (λx. SOME (SUC x,f x)) 0
[linear_order_to_list_f_def] Definition
⊢ ∀lo.
linear_order_to_list_f lo =
(let
min = minimal_elements (domain lo ∪ range lo) lo
in
if min = ∅ then NONE
else
SOME
(rrestrict lo (domain lo ∪ range lo DIFF min),CHOICE min))
[llength_rel_def] Definition
⊢ llength_rel =
(λa0 a1.
∀llength_rel'.
(∀a0 a1.
a0 = [||] ∧ a1 = 0 ∨
(∃h n t. a0 = h:::t ∧ a1 = SUC n ∧ llength_rel' t n) ⇒
llength_rel' a0 a1) ⇒
llength_rel' a0 a1)
[llist_CASE_def] Definition
⊢ ∀ll b f.
llist_CASE ll b f =
case LTL_HD ll of NONE => b | SOME (ltl,lhd) => f lhd ltl
[llist_TY_DEF] Definition
⊢ ∃rep. TYPE_DEFINITION lrep_ok rep
[llist_absrep] Definition
⊢ (∀a. llist_abs (llist_rep a) = a) ∧
∀r. lrep_ok r ⇔ llist_rep (llist_abs r) = r
[llist_rel_def] Definition
⊢ ∀R l1 l2.
llist_rel R l1 l2 ⇔
LLENGTH l1 = LLENGTH l2 ∧
∀i x y. LNTH i l1 = SOME x ∧ LNTH i l2 = SOME y ⇒ R x y
[llist_upto_def] Definition
⊢ llist_upto =
(λR a0 a1.
∀llist_upto'.
(∀a0 a1.
a1 = a0 ∨ R a0 a1 ∨
(∃y. llist_upto' a0 y ∧ llist_upto' y a1) ∨
(∃x y z.
a0 = LAPPEND z x ∧ a1 = LAPPEND z y ∧ llist_upto' x y) ⇒
llist_upto' a0 a1) ⇒
llist_upto' a0 a1)
[lrep_ok_def] Definition
⊢ lrep_ok =
(λa0.
∃lrep_ok'.
lrep_ok' a0 ∧
∀a0.
lrep_ok' a0 ⇒
a0 = (λn. NONE) ∨
∃h t.
a0 = (λn. if n = 0 then SOME h else t (n − 1)) ∧
lrep_ok' t)
[toList] Definition
⊢ ∀ll.
toList ll =
if LFINITE ll then LTAKE (THE (LLENGTH ll)) ll else NONE
[until_def] Definition
⊢ until =
(λP Q a0.
∀until'.
(∀a0.
Q a0 ∨ (∃h t. a0 = h:::t ∧ P (h:::t) ∧ until' t) ⇒
until' a0) ⇒
until' a0)
[LAPPEND_ASSOC] Theorem
⊢ ∀ll1 ll2 ll3.
LAPPEND (LAPPEND ll1 ll2) ll3 = LAPPEND ll1 (LAPPEND ll2 ll3)
[LAPPEND_EQ_LNIL] Theorem
⊢ LAPPEND l1 l2 = [||] ⇔ l1 = [||] ∧ l2 = [||]
[LAPPEND_NIL_2ND] Theorem
⊢ ∀ll. LAPPEND ll [||] = ll
[LAPPEND_fromList] Theorem
⊢ ∀l1 l2. LAPPEND (fromList l1) (fromList l2) = fromList (l1 ⧺ l2)
[LAPPEND_fromSeq] Theorem
⊢ (∀f ll. LAPPEND (fromSeq f) ll = fromSeq f) ∧
∀l f.
LAPPEND (fromList l) (fromSeq f) =
fromSeq (λn. if n < LENGTH l then EL n l else f (n − LENGTH l))
[LCONS_11] Theorem
⊢ ∀h1 t1 h2 t2. h1:::t1 = h2:::t2 ⇔ h1 = h2 ∧ t1 = t2
[LCONS_NOT_NIL] Theorem
⊢ ∀h t. h:::t ≠ [||] ∧ [||] ≠ h:::t
[LDROP1_THM] Theorem
⊢ LDROP 1 = LTL
[LDROP_1] Theorem
⊢ LDROP 1 (h:::t) = SOME t
[LDROP_ADD] Theorem
⊢ ∀k1 k2 x.
LDROP (k1 + k2) x =
case LDROP k1 x of NONE => NONE | SOME ll => LDROP k2 ll
[LDROP_APPEND1] Theorem
⊢ LDROP n l1 = SOME l ⇒ LDROP n (LAPPEND l1 l2) = SOME (LAPPEND l l2)
[LDROP_EQ_LNIL] Theorem
⊢ LDROP n ll = SOME [||] ⇔ LLENGTH ll = SOME n
[LDROP_FUNPOW] Theorem
⊢ ∀n ll. LDROP n ll = FUNPOW (λm. OPTION_BIND m LTL) n (SOME ll)
[LDROP_LDROP] Theorem
⊢ ∀ll k1 k2.
¬LFINITE ll ⇒
THE (LDROP k2 (THE (LDROP k1 ll))) =
THE (LDROP k1 (THE (LDROP k2 ll)))
[LDROP_NONE_LFINITE] Theorem
⊢ LDROP k l = NONE ⇒ LFINITE l
[LDROP_SOME_LLENGTH] Theorem
⊢ LDROP n ll = SOME l ∧ LLENGTH ll = SOME m ⇒
n ≤ m ∧ LLENGTH l = SOME (m − n)
[LDROP_SUC] Theorem
⊢ LDROP (SUC n) ls = OPTION_BIND (LDROP n ls) LTL
[LDROP_THM] Theorem
⊢ (∀ll. LDROP 0 ll = SOME ll) ∧ (∀n. LDROP (SUC n) [||] = NONE) ∧
∀n h t. LDROP (SUC n) (h:::t) = LDROP n t
[LDROP_fromList] Theorem
⊢ ∀ls n.
LDROP n (fromList ls) =
if n ≤ LENGTH ls then SOME (fromList (DROP n ls)) else NONE
[LDROP_fromSeq] Theorem
⊢ ∀n f. LDROP n (fromSeq f) = SOME (fromSeq (f ∘ $+ n))
[LFILTER_APPEND] Theorem
⊢ ∀P ll1 ll2.
LFINITE ll1 ⇒
LFILTER P (LAPPEND ll1 ll2) =
LAPPEND (LFILTER P ll1) (LFILTER P ll2)
[LFILTER_EQ_CONS] Theorem
⊢ LFILTER P ll = h:::t ⇒
∃l ll'.
ll = LAPPEND (fromList l) (h:::ll') ∧ EVERY ($¬ ∘ P) l ∧ P h ∧
LFILTER P ll' = t
[LFILTER_EQ_NIL] Theorem
⊢ ∀ll. LFILTER P ll = [||] ⇔ every ($¬ ∘ P) ll
[LFILTER_NIL] Theorem
⊢ ∀P ll. every ($¬ ∘ P) ll ⇒ LFILTER P ll = [||]
[LFILTER_THM] Theorem
⊢ (∀P. LFILTER P [||] = [||]) ∧
∀P h t.
LFILTER P (h:::t) = if P h then h:::LFILTER P t else LFILTER P t
[LFILTER_fromList] Theorem
⊢ ∀p l. LFILTER p (fromList l) = fromList (FILTER p l)
[LFILTER_fromSeq] Theorem
⊢ ∀p f.
LFILTER p (fromSeq f) =
if ∀i. ¬p (f i) then [||]
else if p (f 0) then f 0:::LFILTER p (fromSeq (f ∘ SUC))
else LFILTER p (fromSeq (f ∘ SUC))
[LFINITE] Theorem
⊢ LFINITE ll ⇔ ∃n. LTAKE n ll = NONE
[LFINITE_APPEND] Theorem
⊢ ∀ll1 ll2. LFINITE (LAPPEND ll1 ll2) ⇔ LFINITE ll1 ∧ LFINITE ll2
[LFINITE_DROP] Theorem
⊢ ∀n ll. LFINITE ll ∧ n ≤ THE (LLENGTH ll) ⇒ ∃y. LDROP n ll = SOME y
[LFINITE_HAS_LENGTH] Theorem
⊢ ∀ll. LFINITE ll ⇒ ∃n. LLENGTH ll = SOME n
[LFINITE_IMP_fromList] Theorem
⊢ ∀ll. LFINITE ll ⇒ ∃l. ll = fromList l
[LFINITE_INDUCTION] Theorem
⊢ ∀P. P [||] ∧ (∀h t. P t ⇒ P (h:::t)) ⇒ ∀a0. LFINITE a0 ⇒ P a0
[LFINITE_LAPPEND_IMP_NIL] Theorem
⊢ ∀ll. LFINITE ll ⇒ ∀l2. LAPPEND ll l2 = ll ⇒ l2 = [||]
[LFINITE_LFLATTEN] Theorem
⊢ ∀lll.
every (λll. LFINITE ll ∧ ll ≠ [||]) lll ⇒
(LFINITE (LFLATTEN lll) ⇔ LFINITE lll)
[LFINITE_LGENLIST] Theorem
⊢ LFINITE (LGENLIST f n) ⇔ n ≠ NONE
[LFINITE_LLENGTH] Theorem
⊢ LFINITE ll ⇔ ∃n. LLENGTH ll = SOME n
[LFINITE_LNTH_NONE] Theorem
⊢ LFINITE ll ⇔ ∃n. LNTH n ll = NONE
[LFINITE_MAP] Theorem
⊢ ∀f ll. LFINITE (LMAP f ll) ⇔ LFINITE ll
[LFINITE_STRONG_INDUCTION] Theorem
⊢ P [||] ∧ (∀h t. LFINITE t ∧ P t ⇒ P (h:::t)) ⇒
∀a0. LFINITE a0 ⇒ P a0
[LFINITE_TAKE] Theorem
⊢ ∀n ll. LFINITE ll ∧ n ≤ THE (LLENGTH ll) ⇒ ∃y. LTAKE n ll = SOME y
[LFINITE_THM] Theorem
⊢ (LFINITE [||] ⇔ T) ∧ ∀h t. LFINITE (h:::t) ⇔ LFINITE t
[LFINITE_cases] Theorem
⊢ ∀a0. LFINITE a0 ⇔ a0 = [||] ∨ ∃h t. a0 = h:::t ∧ LFINITE t
[LFINITE_fromList] Theorem
⊢ ∀l. LFINITE (fromList l)
[LFINITE_fromSeq] Theorem
⊢ ∀f. ¬LFINITE (fromSeq f)
[LFINITE_ind] Theorem
⊢ ∀LFINITE'.
LFINITE' [||] ∧ (∀h t. LFINITE' t ⇒ LFINITE' (h:::t)) ⇒
∀a0. LFINITE a0 ⇒ LFINITE' a0
[LFINITE_rules] Theorem
⊢ LFINITE [||] ∧ ∀h t. LFINITE t ⇒ LFINITE (h:::t)
[LFINITE_strongind] Theorem
⊢ ∀LFINITE'.
LFINITE' [||] ∧ (∀h t. LFINITE t ∧ LFINITE' t ⇒ LFINITE' (h:::t)) ⇒
∀a0. LFINITE a0 ⇒ LFINITE' a0
[LFINITE_toList] Theorem
⊢ ∀ll. LFINITE ll ⇒ ∃l. toList ll = SOME l
[LFINITE_toList_SOME] Theorem
⊢ LFINITE ll ⇔ IS_SOME (toList ll)
[LFLATTEN_APPEND] Theorem
⊢ ∀h t. LFLATTEN (h:::t) = LAPPEND h (LFLATTEN t)
[LFLATTEN_EQ_NIL] Theorem
⊢ ∀ll. LFLATTEN ll = [||] ⇔ every ($= [||]) ll
[LFLATTEN_SINGLETON] Theorem
⊢ ∀h. LFLATTEN [|h|] = h
[LFLATTEN_THM] Theorem
⊢ LFLATTEN [||] = [||] ∧ (∀tl. LFLATTEN ([||]:::t) = LFLATTEN t) ∧
∀h t tl. LFLATTEN ((h:::t):::tl) = h:::LFLATTEN (t:::tl)
[LFLATTEN_fromList] Theorem
⊢ ∀l. LFLATTEN (fromList (MAP fromList l)) = fromList (FLAT l)
[LGENLIST_CHUNK_GENLIST] Theorem
⊢ LGENLIST f NONE =
LAPPEND (fromList (GENLIST f n)) (LGENLIST (f ∘ $+ n) NONE)
[LGENLIST_EQ_CONS] Theorem
⊢ LGENLIST f NONE = h:::t ⇔ h = f 0 ∧ t = LGENLIST (f ∘ $+ 1) NONE
[LGENLIST_EQ_LNIL] Theorem
⊢ (LGENLIST f n = [||] ⇔ n = SOME 0) ∧
([||] = LGENLIST f n ⇔ n = SOME 0)
[LGENLIST_EQ_fromList] Theorem
⊢ ∀f k. LGENLIST f (SOME k) = fromList (GENLIST f k)
[LGENLIST_EQ_fromSeq] Theorem
⊢ ∀f. LGENLIST f NONE = fromSeq f
[LGENLIST_SOME] Theorem
⊢ LGENLIST f (SOME 0) = [||] ∧
∀n. LGENLIST f (SOME (SUC n)) = f 0:::LGENLIST (f ∘ SUC) (SOME n)
[LGENLIST_SOME_compute] Theorem
⊢ LGENLIST f (SOME 0) = [||] ∧
(∀n. LGENLIST f (SOME (NUMERAL (BIT1 n))) =
f 0:::LGENLIST (f ∘ SUC) (SOME (NUMERAL (BIT1 n) − 1))) ∧
∀n. LGENLIST f (SOME (NUMERAL (BIT2 n))) =
f 0:::LGENLIST (f ∘ SUC) (SOME (NUMERAL (BIT1 n)))
[LHDTL_CONS_THM] Theorem
⊢ ∀h t. LHD (h:::t) = SOME h ∧ LTL (h:::t) = SOME t
[LHDTL_EQ_SOME] Theorem
⊢ ∀h t ll. ll = h:::t ⇔ LHD ll = SOME h ∧ LTL ll = SOME t
[LHD_EQ_NONE] Theorem
⊢ ∀ll. (LHD ll = NONE ⇔ ll = [||]) ∧ (NONE = LHD ll ⇔ ll = [||])
[LHD_LAPPEND] Theorem
⊢ LHD (LAPPEND l1 l2) = if l1 = [||] then LHD l2 else LHD l1
[LHD_LCONS] Theorem
⊢ LHD (h:::t) = SOME h
[LHD_LGENLIST] Theorem
⊢ LHD (LGENLIST f limopt) =
if limopt = SOME 0 then NONE else SOME (f 0)
[LHD_LREPEAT] Theorem
⊢ LHD (LREPEAT l) = LHD (fromList l)
[LHD_LUNFOLD] Theorem
⊢ LHD (LUNFOLD f x) = OPTION_MAP SND (f x)
[LHD_THM] Theorem
⊢ LHD [||] = NONE ∧ ∀h t. LHD (h:::t) = SOME h
[LHD_fromList] Theorem
⊢ LHD (fromList l) = if NULL l then NONE else SOME (HD l)
[LHD_fromSeq] Theorem
⊢ ∀f. LHD (fromSeq f) = SOME (f 0)
[LLENGTH_0] Theorem
⊢ LLENGTH x = SOME 0 ⇔ x = [||]
[LLENGTH_APPEND] Theorem
⊢ ∀ll1 ll2.
LLENGTH (LAPPEND ll1 ll2) =
if LFINITE ll1 ∧ LFINITE ll2 then
SOME (THE (LLENGTH ll1) + THE (LLENGTH ll2))
else NONE
[LLENGTH_LGENLIST] Theorem
⊢ ∀f. LLENGTH (LGENLIST f limopt) = limopt
[LLENGTH_LREPEAT] Theorem
⊢ LLENGTH (LREPEAT l) = if NULL l then SOME 0 else NONE
[LLENGTH_MAP] Theorem
⊢ ∀ll f. LLENGTH (LMAP f ll) = LLENGTH ll
[LLENGTH_THM] Theorem
⊢ LLENGTH [||] = SOME 0 ∧
∀h t. LLENGTH (h:::t) = OPTION_MAP SUC (LLENGTH t)
[LLENGTH_fromList] Theorem
⊢ ∀l. LLENGTH (fromList l) = SOME (LENGTH l)
[LLENGTH_fromSeq] Theorem
⊢ ∀f. LLENGTH (fromSeq f) = NONE
[LLIST_BISIMULATION] Theorem
⊢ ∀ll1 ll2.
ll1 = ll2 ⇔
∃R. R ll1 ll2 ∧
∀ll3 ll4.
R ll3 ll4 ⇒
ll3 = [||] ∧ ll4 = [||] ∨
LHD ll3 = LHD ll4 ∧ R (THE (LTL ll3)) (THE (LTL ll4))
[LLIST_BISIMULATION0] Theorem
⊢ ∀ll1 ll2.
ll1 = ll2 ⇔
∃R. R ll1 ll2 ∧
∀ll3 ll4.
R ll3 ll4 ⇒
ll3 = [||] ∧ ll4 = [||] ∨
∃h t1 t2. ll3 = h:::t1 ∧ ll4 = h:::t2 ∧ R t1 t2
[LLIST_BISIMULATION_I] Theorem
⊢ ∀ll2 ll1.
(∃R. R ll1 ll2 ∧
∀ll3 ll4.
R ll3 ll4 ⇒
ll3 = [||] ∧ ll4 = [||] ∨
LHD ll3 = LHD ll4 ∧ R (THE (LTL ll3)) (THE (LTL ll4))) ⇒
ll1 = ll2
[LLIST_BISIM_UPTO] Theorem
⊢ ∀ll1 ll2 R.
R ll1 ll2 ∧
(∀ll3 ll4.
R ll3 ll4 ⇒
ll3 = [||] ∧ ll4 = [||] ∨
LHD ll3 = LHD ll4 ∧
llist_upto R (THE (LTL ll3)) (THE (LTL ll4))) ⇒
ll1 = ll2
[LLIST_CASE_CONG] Theorem
⊢ ∀M M' v f.
M = M' ∧ (M' = [||] ⇒ v = v') ∧
(∀a0 a1. M' = a0:::a1 ⇒ f a0 a1 = f' a0 a1) ⇒
llist_CASE M v f = llist_CASE M' v' f'
[LLIST_CASE_EQ] Theorem
⊢ llist_CASE x v f = v' ⇔
x = [||] ∧ v = v' ∨ ∃a l. x = a:::l ∧ f a l = v'
[LLIST_DISTINCT] Theorem
⊢ ∀a1 a0. [||] ≠ a0:::a1
[LLIST_EQ] Theorem
⊢ ∀f g.
(∀x. f x = [||] ∧ g x = [||] ∨
∃h y. f x = h:::f y ∧ g x = h:::g y) ⇒
∀x. f x = g x
[LLIST_STRONG_BISIMULATION] Theorem
⊢ ∀ll1 ll2.
ll1 = ll2 ⇔
∃R. R ll1 ll2 ∧
∀ll3 ll4.
R ll3 ll4 ⇒
ll3 = ll4 ∨ ∃h t1 t2. ll3 = h:::t1 ∧ ll4 = h:::t2 ∧ R t1 t2
[LL_ALL_THM] Theorem
⊢ (every P [||] ⇔ T) ∧ (every P (h:::t) ⇔ P h ∧ every P t)
[LMAP_APPEND] Theorem
⊢ ∀f ll1 ll2.
LMAP f (LAPPEND ll1 ll2) = LAPPEND (LMAP f ll1) (LMAP f ll2)
[LMAP_LGENLIST] Theorem
⊢ LMAP f (LGENLIST g limopt) = LGENLIST (f ∘ g) limopt
[LMAP_LUNFOLD] Theorem
⊢ ∀f g s.
LMAP f (LUNFOLD g s) =
LUNFOLD (λs. OPTION_MAP (λ(x,y). (x,f y)) (g s)) s
[LMAP_MAP] Theorem
⊢ ∀f g ll. LMAP f (LMAP g ll) = LMAP (f ∘ g) ll
[LMAP_fromList] Theorem
⊢ LMAP f (fromList l) = fromList (MAP f l)
[LMAP_fromSeq] Theorem
⊢ ∀f g. LMAP f (fromSeq g) = fromSeq (f ∘ g)
[LNTH_ADD] Theorem
⊢ ∀a b ll. LNTH (a + b) ll = OPTION_BIND (LDROP a ll) (LNTH b)
[LNTH_EQ] Theorem
⊢ ∀ll1 ll2. ll1 = ll2 ⇔ ∀n. LNTH n ll1 = LNTH n ll2
[LNTH_HD_LDROP] Theorem
⊢ ∀n ll. LNTH n ll = OPTION_BIND (LDROP n ll) LHD
[LNTH_LAPPEND] Theorem
⊢ LNTH n (LAPPEND l1 l2) =
case LLENGTH l1 of
NONE => LNTH n l1
| SOME m => if n < m then LNTH n l1 else LNTH (n − m) l2
[LNTH_LDROP] Theorem
⊢ ∀n l x. LNTH n l = SOME x ⇒ LHD (THE (LDROP n l)) = SOME x
[LNTH_LGENLIST] Theorem
⊢ ∀n f lim.
LNTH n (LGENLIST f lim) =
case lim of
NONE => SOME (f n)
| SOME lim0 => if n < lim0 then SOME (f n) else NONE
[LNTH_LLENGTH_NONE] Theorem
⊢ LLENGTH l = SOME x ∧ x ≤ n ⇒ LNTH n l = NONE
[LNTH_LMAP] Theorem
⊢ ∀n f l. LNTH n (LMAP f l) = OPTION_MAP f (LNTH n l)
[LNTH_LUNFOLD] Theorem
⊢ LNTH 0 (LUNFOLD f x) = OPTION_MAP SND (f x) ∧
LNTH (SUC n) (LUNFOLD f x) =
case f x of NONE => NONE | SOME (tx,hx) => LNTH n (LUNFOLD f tx)
[LNTH_LUNFOLD_compute] Theorem
⊢ LNTH 0 (LUNFOLD f x) = OPTION_MAP SND (f x) ∧
(∀n. LNTH (NUMERAL (BIT1 n)) (LUNFOLD f x) =
case f x of
NONE => NONE
| SOME (tx,hx) => LNTH (NUMERAL (BIT1 n) − 1) (LUNFOLD f tx)) ∧
∀n. LNTH (NUMERAL (BIT2 n)) (LUNFOLD f x) =
case f x of
NONE => NONE
| SOME (tx,hx) => LNTH (NUMERAL (BIT1 n)) (LUNFOLD f tx)
[LNTH_NONE_MONO] Theorem
⊢ ∀m n l. LNTH m l = NONE ∧ m ≤ n ⇒ LNTH n l = NONE
[LNTH_THM] Theorem
⊢ (∀n. LNTH n [||] = NONE) ∧ (∀h t. LNTH 0 (h:::t) = SOME h) ∧
∀n h t. LNTH (SUC n) (h:::t) = LNTH n t
[LNTH_fromList] Theorem
⊢ ∀n xs.
LNTH n (fromList xs) =
if n < LENGTH xs then SOME (EL n xs) else NONE
[LNTH_fromSeq] Theorem
⊢ ∀n f. LNTH n (fromSeq f) = SOME (f n)
[LNTH_rep] Theorem
⊢ ∀i ll. LNTH i ll = llist_rep ll i
[LPREFIX_ANTISYM] Theorem
⊢ LPREFIX l1 l2 ∧ LPREFIX l2 l1 ⇒ l1 = l2
[LPREFIX_APPEND] Theorem
⊢ LPREFIX l1 l2 ⇔ ∃ll. l2 = LAPPEND l1 ll
[LPREFIX_LCONS] Theorem
⊢ (∀ll h t.
LPREFIX ll (h:::t) ⇔ ll = [||] ∨ ∃l. ll = h:::l ∧ LPREFIX l t) ∧
∀h t ll. LPREFIX (h:::t) ll ⇔ ∃l. ll = h:::l ∧ LPREFIX t l
[LPREFIX_LNIL] Theorem
⊢ LPREFIX [||] ll ∧ (LPREFIX ll [||] ⇔ ll = [||])
[LPREFIX_LUNFOLD] Theorem
⊢ LPREFIX ll (LUNFOLD f n) ⇔
case f n of
NONE => ll = [||]
| SOME (n,x) => ∀h t. ll = h:::t ⇒ h = x ∧ LPREFIX t (LUNFOLD f n)
[LPREFIX_NTH] Theorem
⊢ LPREFIX l1 l2 ⇔ ∀i v. LNTH i l1 = SOME v ⇒ LNTH i l2 = SOME v
[LPREFIX_REFL] Theorem
⊢ LPREFIX ll ll
[LPREFIX_TRANS] Theorem
⊢ LPREFIX l1 l2 ∧ LPREFIX l2 l3 ⇒ LPREFIX l1 l3
[LPREFIX_fromList] Theorem
⊢ ∀l ll.
LPREFIX (fromList l) ll ⇔
case toList ll of
NONE => LTAKE (LENGTH l) ll = SOME l
| SOME ys => l ≼ ys
[LREPEAT_EQ_LNIL] Theorem
⊢ (LREPEAT l = [||] ⇔ l = []) ∧ ([||] = LREPEAT l ⇔ l = [])
[LREPEAT_NIL] Theorem
⊢ LREPEAT [] = [||]
[LREPEAT_thm] Theorem
⊢ LREPEAT l = LAPPEND (fromList l) (LREPEAT l)
[LSET] Theorem
⊢ LSET [||] = ∅ ∧ LSET (x:::xs) = x INSERT LSET xs
[LSUFFIX] Theorem
⊢ (LSUFFIX l [||] ⇔ T) ∧ (LSUFFIX [||] (y:::ys) ⇔ F) ∧
(LSUFFIX (x:::xs) l ⇔ x:::xs = l ∨ LSUFFIX xs l)
[LSUFFIX_ANTISYM] Theorem
⊢ ∀x y. LSUFFIX x y ∧ LSUFFIX y x ∧ LFINITE x ⇒ x = y
[LSUFFIX_REFL] Theorem
⊢ ∀s. LSUFFIX s s
[LSUFFIX_TRANS] Theorem
⊢ ∀x y z. LSUFFIX x y ∧ LSUFFIX y z ⇒ LSUFFIX x z
[LSUFFIX_fromList] Theorem
⊢ ∀xs ys. LSUFFIX (fromList xs) (fromList ys) ⇔ IS_SUFFIX xs ys
[LTAKE_CONS_EQ_NONE] Theorem
⊢ ∀m h t. LTAKE m (h:::t) = NONE ⇔ ∃n. m = SUC n ∧ LTAKE n t = NONE
[LTAKE_CONS_EQ_SOME] Theorem
⊢ ∀m h t l.
LTAKE m (h:::t) = SOME l ⇔
m = 0 ∧ l = [] ∨
∃n l'. m = SUC n ∧ LTAKE n t = SOME l' ∧ l = h::l'
[LTAKE_DROP] Theorem
⊢ (∀n ll.
¬LFINITE ll ⇒
LAPPEND (fromList (THE (LTAKE n ll))) (THE (LDROP n ll)) = ll) ∧
∀n ll.
LFINITE ll ∧ n ≤ THE (LLENGTH ll) ⇒
LAPPEND (fromList (THE (LTAKE n ll))) (THE (LDROP n ll)) = ll
[LTAKE_EQ] Theorem
⊢ ∀ll1 ll2. ll1 = ll2 ⇔ ∀n. LTAKE n ll1 = LTAKE n ll2
[LTAKE_EQ_NONE_LNTH] Theorem
⊢ ∀n ll. LTAKE n ll = NONE ⇒ LNTH n ll = NONE
[LTAKE_EQ_SOME_CONS] Theorem
⊢ ∀n l x. LTAKE n l = SOME x ⇒ ∀h. ∃y. LTAKE n (h:::l) = SOME y
[LTAKE_IMP_LDROP] Theorem
⊢ ∀n ll l1.
LTAKE n ll = SOME l1 ⇒
∃l2. LDROP n ll = SOME l2 ∧ LAPPEND (fromList l1) l2 = ll
[LTAKE_LAPPEND1] Theorem
⊢ ∀n l1 l2.
IS_SOME (LTAKE n l1) ⇒ LTAKE n (LAPPEND l1 l2) = LTAKE n l1
[LTAKE_LAPPEND2] Theorem
⊢ ∀n l1 l2.
LTAKE n l1 = NONE ⇒
LTAKE n (LAPPEND l1 l2) =
OPTION_MAP ($++ (THE (toList l1)))
(LTAKE (n − THE (LLENGTH l1)) l2)
[LTAKE_LAPPEND_fromList] Theorem
⊢ ∀ll l n.
LTAKE (n + LENGTH l) (LAPPEND (fromList l) ll) =
OPTION_MAP ($++ l) (LTAKE n ll)
[LTAKE_LENGTH] Theorem
⊢ ∀n ll l. LTAKE n ll = SOME l ⇒ n = LENGTH l
[LTAKE_LLENGTH_NONE] Theorem
⊢ LLENGTH ll = SOME n ∧ n < m ⇒ LTAKE m ll = NONE
[LTAKE_LLENGTH_SOME] Theorem
⊢ LLENGTH ll = SOME n ⇒ ∃l. LTAKE n ll = SOME l ∧ toList ll = SOME l
[LTAKE_LMAP] Theorem
⊢ ∀n f ll. LTAKE n (LMAP f ll) = OPTION_MAP (MAP f) (LTAKE n ll)
[LTAKE_LNTH_EL] Theorem
⊢ ∀n ll m l. LTAKE n ll = SOME l ∧ m < n ⇒ LNTH m ll = SOME (EL m l)
[LTAKE_LPREFIX] Theorem
⊢ ∀x ll.
¬LFINITE ll ⇒ ∃l. LTAKE x ll = SOME l ∧ LPREFIX (fromList l) ll
[LTAKE_LUNFOLD] Theorem
⊢ LTAKE 0 (LUNFOLD f x) = SOME [] ∧
LTAKE (SUC n) (LUNFOLD f x) =
case f x of
NONE => NONE
| SOME (tx,hx) => OPTION_MAP (CONS hx) (LTAKE n (LUNFOLD f tx))
[LTAKE_NIL_EQ_NONE] Theorem
⊢ ∀m. LTAKE m [||] = NONE ⇔ 0 < m
[LTAKE_NIL_EQ_SOME] Theorem
⊢ ∀l m. LTAKE m [||] = SOME l ⇔ m = 0 ∧ l = []
[LTAKE_SNOC_LNTH] Theorem
⊢ ∀n ll.
LTAKE (SUC n) ll =
case LTAKE n ll of
NONE => NONE
| SOME l =>
case LNTH n ll of NONE => NONE | SOME e => SOME (l ⧺ [e])
[LTAKE_TAKE_LESS] Theorem
⊢ LTAKE n ll = SOME l ∧ m ≤ n ⇒ LTAKE m ll = SOME (TAKE m l)
[LTAKE_THM] Theorem
⊢ (∀l. LTAKE 0 l = SOME []) ∧ (∀n. LTAKE (SUC n) [||] = NONE) ∧
∀n h t. LTAKE (SUC n) (h:::t) = OPTION_MAP (CONS h) (LTAKE n t)
[LTAKE_fromList] Theorem
⊢ ∀l. LTAKE (LENGTH l) (fromList l) = SOME l
[LTAKE_fromSeq] Theorem
⊢ ∀n f. LTAKE n (fromSeq f) = SOME (GENLIST f n)
[LTL_EQ_NONE] Theorem
⊢ ∀ll. (LTL ll = NONE ⇔ ll = [||]) ∧ (NONE = LTL ll ⇔ ll = [||])
[LTL_HD_11] Theorem
⊢ LTL_HD ll1 = LTL_HD ll2 ⇒ ll1 = ll2
[LTL_HD_HD] Theorem
⊢ LHD ll = OPTION_MAP SND (LTL_HD ll)
[LTL_HD_LCONS] Theorem
⊢ LTL_HD (h:::t) = SOME (t,h)
[LTL_HD_LNIL] Theorem
⊢ LTL_HD [||] = NONE
[LTL_HD_LTL_LHD] Theorem
⊢ LTL_HD l =
OPTION_BIND (LHD l) (λh. OPTION_BIND (LTL l) (λt. SOME (t,h)))
[LTL_HD_LUNFOLD] Theorem
⊢ LTL_HD (LUNFOLD f x) = OPTION_MAP (LUNFOLD f ## I) (f x)
[LTL_HD_TL] Theorem
⊢ LTL ll = OPTION_MAP FST (LTL_HD ll)
[LTL_HD_iff] Theorem
⊢ (LTL_HD x = SOME (t,h) ⇔ x = h:::t) ∧ (LTL_HD x = NONE ⇔ x = [||])
[LTL_LAPPEND] Theorem
⊢ LTL (LAPPEND l1 l2) =
if l1 = [||] then LTL l2 else SOME (LAPPEND (THE (LTL l1)) l2)
[LTL_LCONS] Theorem
⊢ LTL (h:::t) = SOME t
[LTL_LGENLIST] Theorem
⊢ LTL (LGENLIST f limopt) =
if limopt = SOME 0 then NONE
else SOME (LGENLIST (f ∘ SUC) (OPTION_MAP PRE limopt))
[LTL_LREPEAT] Theorem
⊢ LTL (LREPEAT l) =
OPTION_MAP (λt. LAPPEND t (LREPEAT l)) (LTL (fromList l))
[LTL_LUNFOLD] Theorem
⊢ LTL (LUNFOLD f x) = OPTION_MAP (LUNFOLD f ∘ FST) (f x)
[LTL_THM] Theorem
⊢ LTL [||] = NONE ∧ ∀h t. LTL (h:::t) = SOME t
[LTL_fromList] Theorem
⊢ LTL (fromList l) = if NULL l then NONE else SOME (fromList (TL l))
[LTL_fromSeq] Theorem
⊢ ∀f. LTL (fromSeq f) = SOME (fromSeq (f ∘ SUC))
[LUNFOLD] Theorem
⊢ ∀f x.
LUNFOLD f x =
case f x of NONE => [||] | SOME (v1,v2) => v2:::LUNFOLD f v1
[LUNFOLD_BISIMULATION] Theorem
⊢ ∀f1 f2 x1 x2.
LUNFOLD f1 x1 = LUNFOLD f2 x2 ⇔
∃R. R x1 x2 ∧
∀y1 y2.
R y1 y2 ⇒
f1 y1 = NONE ∧ f2 y2 = NONE ∨
∃h t1 t2.
f1 y1 = SOME (t1,h) ∧ f2 y2 = SOME (t2,h) ∧ R t1 t2
[LUNFOLD_EQ] Theorem
⊢ ∀R f s ll.
R s ll ∧
(∀s ll.
R s ll ⇒
f s = NONE ∧ ll = [||] ∨
∃s' x ll'.
f s = SOME (s',x) ∧ LHD ll = SOME x ∧ LTL ll = SOME ll' ∧
R s' ll') ⇒
LUNFOLD f s = ll
[LUNFOLD_LTL_HD] Theorem
⊢ LUNFOLD LTL_HD ll = ll
[LUNFOLD_THM] Theorem
⊢ ∀f x v1 v2.
(f x = NONE ⇒ LUNFOLD f x = [||]) ∧
(f x = SOME (v1,v2) ⇒ LUNFOLD f x = v2:::LUNFOLD f v1)
[LUNFOLD_UNIQUE] Theorem
⊢ ∀f g.
(∀x. g x = case f x of NONE => [||] | SOME (v1,v2) => v2:::g v1) ⇒
∀y. g y = LUNFOLD f y
[LZIP_LUNZIP] Theorem
⊢ ∀ll. LZIP (LUNZIP ll) = ll
[MONO_every] Theorem
⊢ (∀x. P x ⇒ Q x) ⇒ every P l ⇒ every Q l
[MONO_exists] Theorem
⊢ (∀x. P x ⇒ Q x) ⇒ exists P l ⇒ exists Q l
[NOT_LFINITE_APPEND] Theorem
⊢ ∀ll1 ll2. ¬LFINITE ll1 ⇒ LAPPEND ll1 ll2 = ll1
[NOT_LFINITE_DROP] Theorem
⊢ ∀ll. ¬LFINITE ll ⇒ ∀n. ∃y. LDROP n ll = SOME y
[NOT_LFINITE_DROP_LFINITE] Theorem
⊢ ∀n l t. ¬LFINITE l ∧ LDROP n l = SOME t ⇒ ¬LFINITE t
[NOT_LFINITE_IMP_fromSeq] Theorem
⊢ ∀ll. ¬LFINITE ll ⇒ ∃f. ll = fromSeq f
[NOT_LFINITE_NO_LENGTH] Theorem
⊢ ∀ll. ¬LFINITE ll ⇒ LLENGTH ll = NONE
[NOT_LFINITE_TAKE] Theorem
⊢ ∀ll. ¬LFINITE ll ⇒ ∀n. ∃y. LTAKE n ll = SOME y
[always_DROP] Theorem
⊢ ∀ll. always P ll ⇒ always P (THE (LDROP k ll))
[always_cases] Theorem
⊢ ∀P a0. always P a0 ⇔ ∃h t. a0 = h:::t ∧ P (h:::t) ∧ always P t
[always_coind] Theorem
⊢ ∀P always'.
(∀a0. always' a0 ⇒ ∃h t. a0 = h:::t ∧ P (h:::t) ∧ always' t) ⇒
∀a0. always' a0 ⇒ always P a0
[always_conj_l] Theorem
⊢ ∀ll. always (λx. P x ∧ Q x) ll ⇒ always P ll
[always_eventually_ind] Theorem
⊢ (∀ll. P ll ∨ ¬P ll ∧ Q (THE (LTL ll)) ⇒ Q ll) ⇒
∀ll. ll ≠ [||] ⇒ always (eventually P) ll ⇒ Q ll
[always_rules] Theorem
⊢ ∀P h t. P (h:::t) ∧ always P t ⇒ always P (h:::t)
[always_thm] Theorem
⊢ (always P [||] ⇔ F) ∧
∀h t. always P (h:::t) ⇔ P (h:::t) ∧ always P t
[eventually_cases] Theorem
⊢ ∀P a0. eventually P a0 ⇔ P a0 ∨ ∃h t. a0 = h:::t ∧ eventually P t
[eventually_ind] Theorem
⊢ ∀P eventually'.
(∀ll. P ll ⇒ eventually' ll) ∧
(∀h t. eventually' t ⇒ eventually' (h:::t)) ⇒
∀a0. eventually P a0 ⇒ eventually' a0
[eventually_rules] Theorem
⊢ ∀P. (∀ll. P ll ⇒ eventually P ll) ∧
∀h t. eventually P t ⇒ eventually P (h:::t)
[eventually_strongind] Theorem
⊢ ∀P eventually'.
(∀ll. P ll ⇒ eventually' ll) ∧
(∀h t. eventually P t ∧ eventually' t ⇒ eventually' (h:::t)) ⇒
∀a0. eventually P a0 ⇒ eventually' a0
[eventually_thm] Theorem
⊢ (eventually P [||] ⇔ P [||]) ∧
(eventually P (h:::t) ⇔ P (h:::t) ∨ eventually P t)
[eventually_until_EQN] Theorem
⊢ eventually P = until (K T) P
[every_LAPPEND1] Theorem
⊢ ∀P ll1 ll2. every P (LAPPEND ll1 ll2) ⇒ every P ll1
[every_LAPPEND2_LFINITE] Theorem
⊢ ∀l P ll. LFINITE l ∧ every P (LAPPEND l ll) ⇒ every P ll
[every_LDROP] Theorem
⊢ ∀f i ll1 ll2. every f ll1 ∧ LDROP i ll1 = SOME ll2 ⇒ every f ll2
[every_LFILTER] Theorem
⊢ ∀ll P. every P (LFILTER P ll)
[every_LFILTER_imp] Theorem
⊢ ∀Q P ll. every Q ll ⇒ every Q (LFILTER P ll)
[every_LNTH] Theorem
⊢ ∀P ll. every P ll ⇔ ∀n e. LNTH n ll = SOME e ⇒ P e
[every_coind] Theorem
⊢ ∀P Q. (∀h t. Q (h:::t) ⇒ P h ∧ Q t) ⇒ ∀ll. Q ll ⇒ every P ll
[every_fromList_EVERY] Theorem
⊢ ∀l P. every P (fromList l) ⇔ EVERY P l
[every_fromSeq] Theorem
⊢ ∀p f. every p (fromSeq f) ⇔ ∀i. p (f i)
[every_strong_coind] Theorem
⊢ ∀P Q.
(∀h t. Q (h:::t) ⇒ P h) ∧ (∀h t. Q (h:::t) ⇒ Q t ∨ every P t) ⇒
∀ll. Q ll ⇒ every P ll
[every_thm] Theorem
⊢ (every P [||] ⇔ T) ∧ (every P (h:::t) ⇔ P h ∧ every P t)
[exists_LDROP] Theorem
⊢ exists P ll ⇔ ∃n a t. LDROP n ll = SOME (a:::t) ∧ P a
[exists_LNTH] Theorem
⊢ ∀l. exists P l ⇔ ∃n e. SOME e = LNTH n l ∧ P e
[exists_cases] Theorem
⊢ ∀P a0.
exists P a0 ⇔
(∃h t. a0 = h:::t ∧ P h) ∨ ∃h t. a0 = h:::t ∧ exists P t
[exists_fromSeq] Theorem
⊢ ∀p f. exists p (fromSeq f) ⇔ ∃i. p (f i)
[exists_ind] Theorem
⊢ ∀P exists'.
(∀h t. P h ⇒ exists' (h:::t)) ∧
(∀h t. exists' t ⇒ exists' (h:::t)) ⇒
∀a0. exists P a0 ⇒ exists' a0
[exists_rules] Theorem
⊢ ∀P. (∀h t. P h ⇒ exists P (h:::t)) ∧
∀h t. exists P t ⇒ exists P (h:::t)
[exists_strong_ind] Theorem
⊢ ∀P Q.
(∀h t. P h ⇒ Q (h:::t)) ∧ (∀h t. Q t ∧ exists P t ⇒ Q (h:::t)) ⇒
∀a0. exists P a0 ⇒ Q a0
[exists_strongind] Theorem
⊢ ∀P exists'.
(∀h t. P h ⇒ exists' (h:::t)) ∧
(∀h t. exists P t ∧ exists' t ⇒ exists' (h:::t)) ⇒
∀a0. exists P a0 ⇒ exists' a0
[exists_thm] Theorem
⊢ (exists P [||] ⇔ F) ∧ (exists P (h:::t) ⇔ P h ∨ exists P t)
[exists_thm_strong] Theorem
⊢ exists P ll ⇔
∃n a t l.
LDROP n ll = SOME (a:::t) ∧ P a ∧ LTAKE n ll = SOME l ∧
EVERY ($¬ ∘ P) l
[fromList_11] Theorem
⊢ ∀xs ys. fromList xs = fromList ys ⇔ xs = ys
[fromList_EQ_LNIL] Theorem
⊢ fromList l = [||] ⇔ l = []
[fromList_NEQ_fromSeq] Theorem
⊢ ∀l f. fromList l ≠ fromSeq f
[fromList_fromSeq] Theorem
⊢ ∀ll. (∃l. ll = fromList l) ∨ ∃f. ll = fromSeq f
[fromSeq_11] Theorem
⊢ ∀f g. fromSeq f = fromSeq g ⇔ f = g
[fromSeq_LCONS] Theorem
⊢ fromSeq f = f 0:::fromSeq (f ∘ SUC)
[from_toList] Theorem
⊢ ∀l. toList (fromList l) = SOME l
[infinite_lnth_some] Theorem
⊢ ∀ll. ¬LFINITE ll ⇔ ∀n. ∃x. LNTH n ll = SOME x
[linear_order_to_llist] Theorem
⊢ ∀lo X.
linear_order lo X ∧ finite_prefixes lo X ⇒
∃ll.
X = {x | ∃i. LNTH i ll = SOME x} ∧
lo ⊆
{(x,y) | ∃i j. i ≤ j ∧ LNTH i ll = SOME x ∧ LNTH j ll = SOME y} ∧
∀i j x. LNTH i ll = SOME x ∧ LNTH j ll = SOME x ⇒ i = j
[linear_order_to_llist_eq] Theorem
⊢ ∀lo X.
linear_order lo X ∧ finite_prefixes lo X ⇒
∃ll.
X = {x | ∃i. LNTH i ll = SOME x} ∧
lo =
{(x,y) | ∃i j. i ≤ j ∧ LNTH i ll = SOME x ∧ LNTH j ll = SOME y} ∧
∀i j x. LNTH i ll = SOME x ∧ LNTH j ll = SOME x ⇒ i = j
[llength_rel_cases] Theorem
⊢ ∀a0 a1.
llength_rel a0 a1 ⇔
a0 = [||] ∧ a1 = 0 ∨
∃h n t. a0 = h:::t ∧ a1 = SUC n ∧ llength_rel t n
[llength_rel_ind] Theorem
⊢ ∀llength_rel'.
llength_rel' [||] 0 ∧
(∀h n t. llength_rel' t n ⇒ llength_rel' (h:::t) (SUC n)) ⇒
∀a0 a1. llength_rel a0 a1 ⇒ llength_rel' a0 a1
[llength_rel_rules] Theorem
⊢ llength_rel [||] 0 ∧
∀h n t. llength_rel t n ⇒ llength_rel (h:::t) (SUC n)
[llength_rel_strongind] Theorem
⊢ ∀llength_rel'.
llength_rel' [||] 0 ∧
(∀h n t.
llength_rel t n ∧ llength_rel' t n ⇒
llength_rel' (h:::t) (SUC n)) ⇒
∀a0 a1. llength_rel a0 a1 ⇒ llength_rel' a0 a1
[llist_Axiom] Theorem
⊢ ∀f. ∃g.
(∀x. LHD (g x) = OPTION_MAP SND (f x)) ∧
∀x. LTL (g x) = OPTION_MAP (g ∘ FST) (f x)
[llist_Axiom_1] Theorem
⊢ ∀f. ∃g. ∀x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a
[llist_Axiom_1ue] Theorem
⊢ ∀f. ∃!g. ∀x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a
[llist_CASES] Theorem
⊢ ∀l. l = [||] ∨ ∃h t. l = h:::t
[llist_CASE_compute] Theorem
⊢ llist_CASE [||] b f = b ∧ llist_CASE (x:::ll) b f = f x ll
[llist_forall_split] Theorem
⊢ ∀P. (∀ll. P ll) ⇔ (∀l. P (fromList l)) ∧ ∀f. P (fromSeq f)
[llist_rep_LCONS] Theorem
⊢ llist_rep (h:::t) =
(λn. if n = 0 then SOME h else llist_rep t (n − 1))
[llist_rep_LNIL] Theorem
⊢ llist_rep [||] = (λn. NONE)
[llist_ue_Axiom] Theorem
⊢ ∀f. ∃!g.
(∀x. LHD (g x) = OPTION_MAP SND (f x)) ∧
∀x. LTL (g x) = OPTION_MAP (g ∘ FST) (f x)
[llist_upto_cases] Theorem
⊢ ∀R a0 a1.
llist_upto R a0 a1 ⇔
a1 = a0 ∨ R a0 a1 ∨ (∃y. llist_upto R a0 y ∧ llist_upto R y a1) ∨
∃x y z. a0 = LAPPEND z x ∧ a1 = LAPPEND z y ∧ llist_upto R x y
[llist_upto_context] Theorem
⊢ ∀R x y z.
llist_upto R x y ⇒ llist_upto R (LAPPEND z x) (LAPPEND z y)
[llist_upto_eq] Theorem
⊢ ∀R x. llist_upto R x x
[llist_upto_ind] Theorem
⊢ ∀R llist_upto'.
(∀x. llist_upto' x x) ∧ (∀x y. R x y ⇒ llist_upto' x y) ∧
(∀x y z. llist_upto' x y ∧ llist_upto' y z ⇒ llist_upto' x z) ∧
(∀x y z.
llist_upto' x y ⇒ llist_upto' (LAPPEND z x) (LAPPEND z y)) ⇒
∀a0 a1. llist_upto R a0 a1 ⇒ llist_upto' a0 a1
[llist_upto_rel] Theorem
⊢ ∀R x y. R x y ⇒ llist_upto R x y
[llist_upto_rules] Theorem
⊢ ∀R. (∀x. llist_upto R x x) ∧ (∀x y. R x y ⇒ llist_upto R x y) ∧
(∀x y z. llist_upto R x y ∧ llist_upto R y z ⇒ llist_upto R x z) ∧
∀x y z.
llist_upto R x y ⇒ llist_upto R (LAPPEND z x) (LAPPEND z y)
[llist_upto_strongind] Theorem
⊢ ∀R llist_upto'.
(∀x. llist_upto' x x) ∧ (∀x y. R x y ⇒ llist_upto' x y) ∧
(∀x y z.
llist_upto R x y ∧ llist_upto' x y ∧ llist_upto R y z ∧
llist_upto' y z ⇒
llist_upto' x z) ∧
(∀x y z.
llist_upto R x y ∧ llist_upto' x y ⇒
llist_upto' (LAPPEND z x) (LAPPEND z y)) ⇒
∀a0 a1. llist_upto R a0 a1 ⇒ llist_upto' a0 a1
[llist_upto_trans] Theorem
⊢ ∀R x y z. llist_upto R x y ∧ llist_upto R y z ⇒ llist_upto R x z
[lnth_fromList_some] Theorem
⊢ ∀n l. n < LENGTH l ⇔ LNTH n (fromList l) = SOME (EL n l)
[lnth_some_down_closed] Theorem
⊢ ∀ll x n1 n2.
LNTH n1 ll = SOME x ∧ n2 ≤ n1 ⇒ ∃y. LNTH n2 ll = SOME y
[lrep_ok_FUNPOW_BIND] Theorem
⊢ lrep_ok (λn. FUNPOW (λm. OPTION_BIND m g) n fz)
[lrep_ok_MAP] Theorem
⊢ lrep_ok (λn. OPTION_MAP f (g n)) ⇔ lrep_ok g
[lrep_ok_alt] Theorem
⊢ lrep_ok f ⇔ ∀n. IS_SOME (f (SUC n)) ⇒ IS_SOME (f n)
[lrep_ok_cases] Theorem
⊢ ∀a0.
lrep_ok a0 ⇔
a0 = (λn. NONE) ∨
∃h t. a0 = (λn. if n = 0 then SOME h else t (n − 1)) ∧ lrep_ok t
[lrep_ok_coind] Theorem
⊢ ∀lrep_ok'.
(∀a0.
lrep_ok' a0 ⇒
a0 = (λn. NONE) ∨
∃h t.
a0 = (λn. if n = 0 then SOME h else t (n − 1)) ∧ lrep_ok' t) ⇒
∀a0. lrep_ok' a0 ⇒ lrep_ok a0
[lrep_ok_rules] Theorem
⊢ lrep_ok (λn. NONE) ∧
∀h t. lrep_ok t ⇒ lrep_ok (λn. if n = 0 then SOME h else t (n − 1))
[numopt_BISIMULATION] Theorem
⊢ ∀mopt nopt.
mopt = nopt ⇔
∃R. R mopt nopt ∧
∀m n.
R m n ⇒
m = SOME 0 ∧ n = SOME 0 ∨
m ≠ SOME 0 ∧ n ≠ SOME 0 ∧
R (OPTION_MAP PRE m) (OPTION_MAP PRE n)
[prefixes_lprefix_total] Theorem
⊢ ∀ll l1 l2.
LPREFIX l1 ll ∧ LPREFIX l2 ll ⇒ LPREFIX l1 l2 ∨ LPREFIX l2 l1
[toList_LAPPEND_APPEND] Theorem
⊢ toList (LAPPEND l1 l2) = SOME x ⇒
x = THE (toList l1) ⧺ THE (toList l2)
[toList_THM] Theorem
⊢ toList [||] = SOME [] ∧
∀h t. toList (h:::t) = OPTION_MAP (CONS h) (toList t)
[to_fromList] Theorem
⊢ ∀ll. LFINITE ll ⇒ fromList (THE (toList ll)) = ll
[until_cases] Theorem
⊢ ∀P Q a0.
until P Q a0 ⇔ Q a0 ∨ ∃h t. a0 = h:::t ∧ P (h:::t) ∧ until P Q t
[until_ind] Theorem
⊢ ∀P Q until'.
(∀ll. Q ll ⇒ until' ll) ∧
(∀h t. P (h:::t) ∧ until' t ⇒ until' (h:::t)) ⇒
∀a0. until P Q a0 ⇒ until' a0
[until_rules] Theorem
⊢ ∀P Q.
(∀ll. Q ll ⇒ until P Q ll) ∧
∀h t. P (h:::t) ∧ until P Q t ⇒ until P Q (h:::t)
[until_strongind] Theorem
⊢ ∀P Q until'.
(∀ll. Q ll ⇒ until' ll) ∧
(∀h t. P (h:::t) ∧ until P Q t ∧ until' t ⇒ until' (h:::t)) ⇒
∀a0. until P Q a0 ⇒ until' a0
*)
end
HOL 4, Kananaskis-14