Structure listTheory
signature listTheory =
sig
type thm = Thm.thm
(* Definitions *)
val ALL_DISTINCT : thm
val APPEND : thm
val CONS_def : thm
val EL : thm
val EVERY_DEF : thm
val EXISTS_DEF : thm
val FILTER : thm
val FLAT : thm
val FOLDL : thm
val FOLDR : thm
val FRONT_DEF : thm
val HD : thm
val LAST_DEF : thm
val LENGTH : thm
val LEN_DEF : thm
val LIST_TO_SET : thm
val MAP : thm
val MAP2 : thm
val MEM : thm
val NIL : thm
val NULL_DEF : thm
val REVERSE_DEF : thm
val REV_DEF : thm
val SUM : thm
val TL : thm
val UNZIP : thm
val ZIP : thm
val list0_def : thm
val list1_def : thm
val listRel : thm
val list_TY_DEF : thm
val list_case_def : thm
val list_repfns : thm
val list_size_def : thm
(* Theorems *)
val ALL_DISTINCT_FILTER : thm
val APPEND_11 : thm
val APPEND_ASSOC : thm
val APPEND_FRONT_LAST : thm
val APPEND_NIL : thm
val APPEND_eq_NIL : thm
val CONS : thm
val CONS_11 : thm
val CONS_ACYCLIC : thm
val EL_ZIP : thm
val EL_compute : thm
val EL_simp : thm
val EQ_LIST : thm
val EVERY_APPEND : thm
val EVERY_CONG : thm
val EVERY_CONJ : thm
val EVERY_EL : thm
val EVERY_MAP : thm
val EVERY_MEM : thm
val EVERY_MONOTONIC : thm
val EVERY_NOT_EXISTS : thm
val EVERY_SIMP : thm
val EXISTS_APPEND : thm
val EXISTS_CONG : thm
val EXISTS_MAP : thm
val EXISTS_MEM : thm
val EXISTS_NOT_EVERY : thm
val EXISTS_SIMP : thm
val FILTER_APPEND_DISTRIB : thm
val FOLDL_CONG : thm
val FOLDR_CONG : thm
val FORALL_LIST : thm
val FRONT_CONS : thm
val IN_LIST_TO_SET : thm
val LAST_CONS : thm
val LENGTH_APPEND : thm
val LENGTH_CONS : thm
val LENGTH_EQ_CONS : thm
val LENGTH_EQ_NIL : thm
val LENGTH_LEN : thm
val LENGTH_MAP : thm
val LENGTH_NIL : thm
val LENGTH_UNZIP : thm
val LENGTH_ZIP : thm
val LEN_LENGTH_LEM : thm
val LIST_NOT_EQ : thm
val MAP2_ZIP : thm
val MAP_APPEND : thm
val MAP_CONG : thm
val MAP_EQ_NIL : thm
val MEM_APPEND : thm
val MEM_EL : thm
val MEM_FILTER : thm
val MEM_MAP : thm
val MEM_REVERSE : thm
val MEM_ZIP : thm
val MONO_EVERY : thm
val MONO_EXISTS : thm
val MONO_listRel : thm
val NOT_CONS_NIL : thm
val NOT_EQ_LIST : thm
val NOT_EVERY : thm
val NOT_EXISTS : thm
val NOT_NIL_CONS : thm
val NULL : thm
val REVERSE_APPEND : thm
val REVERSE_REV : thm
val REVERSE_REVERSE : thm
val REV_REVERSE_LEM : thm
val UNZIP_THM : thm
val UNZIP_ZIP : thm
val WF_LIST_PRED : thm
val ZIP_MAP : thm
val ZIP_UNZIP : thm
val datatype_list : thm
val listRel_CONS : thm
val listRel_LENGTH : thm
val listRel_NIL : thm
val listRel_cases : thm
val listRel_ind : thm
val listRel_rules : thm
val listRel_strong_ind : thm
val list_11 : thm
val list_Axiom : thm
val list_Axiom_old : thm
val list_CASES : thm
val list_INDUCT : thm
val list_case_compute : thm
val list_case_cong : thm
val list_distinct : thm
val list_induction : thm
val list_nchotomy : thm
val list_size_cong : thm
val list_grammars : type_grammar.grammar * term_grammar.grammar
val list_rwts : simpLib.ssfrag
(*
[ind_type] Parent theory of "list"
[ALL_DISTINCT] Definition
|- (ALL_DISTINCT [] = T) /\
!h t. ALL_DISTINCT (h::t) = ~MEM h t /\ ALL_DISTINCT t
[APPEND] Definition
|- (!l. [] ++ l = l) /\ !l1 l2 h. h::l1 ++ l2 = h::(l1 ++ l2)
[CONS_def] Definition
|- CONS = list1
[EL] Definition
|- (!l. EL 0 l = HD l) /\ !l n. EL (SUC n) l = EL n (TL l)
[EVERY_DEF] Definition
|- (!P. EVERY P [] = T) /\ !P h t. EVERY P (h::t) = P h /\ EVERY P t
[EXISTS_DEF] Definition
|- (!P. EXISTS P [] = F) /\ !P h t. EXISTS P (h::t) = P h \/ EXISTS P t
[FILTER] Definition
|- (!P. FILTER P [] = []) /\
!P h t. FILTER P (h::t) = (if P h then h::FILTER P t else FILTER P t)
[FLAT] Definition
|- (FLAT [] = []) /\ !h t. FLAT (h::t) = h ++ FLAT t
[FOLDL] Definition
|- (!f e. FOLDL f e [] = e) /\ !f e x l. FOLDL f e (x::l) = FOLDL f (f e x) l
[FOLDR] Definition
|- (!f e. FOLDR f e [] = e) /\ !f e x l. FOLDR f e (x::l) = f x (FOLDR f e l)
[FRONT_DEF] Definition
|- !h t. FRONT (h::t) = (if t = [] then [] else h::FRONT t)
[HD] Definition
|- !h t. HD (h::t) = h
[LAST_DEF] Definition
|- !h t. LAST (h::t) = (if t = [] then h else LAST t)
[LENGTH] Definition
|- (LENGTH [] = 0) /\ !h t. LENGTH (h::t) = SUC (LENGTH t)
[LEN_DEF] Definition
|- (!n. LEN [] n = n) /\ !h t n. LEN (h::t) n = LEN t (n + 1)
[LIST_TO_SET] Definition
|- LIST_TO_SET = combin$C MEM
[MAP] Definition
|- (!f. MAP f [] = []) /\ !f h t. MAP f (h::t) = f h::MAP f t
[MAP2] Definition
|- (!f. MAP2 f [] [] = []) /\
!f h1 t1 h2 t2. MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2
[MEM] Definition
|- (!x. MEM x [] = F) /\ !x h t. MEM x (h::t) = (x = h) \/ MEM x t
[NIL] Definition
|- [] = list0
[NULL_DEF] Definition
|- (NULL [] = T) /\ !h t. NULL (h::t) = F
[REVERSE_DEF] Definition
|- (REVERSE [] = []) /\ !h t. REVERSE (h::t) = REVERSE t ++ [h]
[REV_DEF] Definition
|- (!acc. REV [] acc = acc) /\ !h t acc. REV (h::t) acc = REV t (h::acc)
[SUM] Definition
|- (SUM [] = 0) /\ !h t. SUM (h::t) = h + SUM t
[TL] Definition
|- !h t. TL (h::t) = t
[UNZIP] Definition
|- (UNZIP [] = ([],[])) /\
!x l. UNZIP (x::l) = (FST x::FST (UNZIP l),SND x::SND (UNZIP l))
[ZIP] Definition
|- (ZIP ([],[]) = []) /\
!x1 l1 x2 l2. ZIP (x1::l1,x2::l2) = (x1,x2)::ZIP (l1,l2)
[list0_def] Definition
|- list0 = mk_list (ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM))
[list1_def] Definition
|- list1 =
(\a0 a1.
mk_list
((\a0 a1. ind_type$CONSTR (SUC 0) a0 (FCONS a1 (\n. ind_type$BOTTOM)))
a0 (dest_list a1)))
[listRel] Definition
|- listRel =
(\R a0 a1.
!listRel'.
(!a0 a1.
(a0 = []) /\ (a1 = []) \/
(?h1 h2 t1 t2.
(a0 = h1::t1) /\ (a1 = h2::t2) /\ R h1 h2 /\ listRel' t1 t2) ==>
listRel' a0 a1) ==>
listRel' a0 a1)
[list_TY_DEF] Definition
|- ?rep.
TYPE_DEFINITION
(\a0'.
!'list'.
(!a0'.
(a0' = ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM)) \/
(?a0 a1.
(a0' =
(\a0 a1.
ind_type$CONSTR (SUC 0) a0
(FCONS a1 (\n. ind_type$BOTTOM))) a0 a1) /\
'list' a1) ==>
'list' a0') ==>
'list' a0') rep
[list_case_def] Definition
|- (!v f. list_case v f [] = v) /\ !v f a0 a1. list_case v f (a0::a1) = f a0 a1
[list_repfns] Definition
|- (!a. mk_list (dest_list a) = a) /\
!r.
(\a0'.
!'list'.
(!a0'.
(a0' = ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM)) \/
(?a0 a1.
(a0' =
(\a0 a1.
ind_type$CONSTR (SUC 0) a0
(FCONS a1 (\n. ind_type$BOTTOM))) a0 a1) /\
'list' a1) ==>
'list' a0') ==>
'list' a0') r =
(dest_list (mk_list r) = r)
[list_size_def] Definition
|- (!f. list_size f [] = 0) /\
!f a0 a1. list_size f (a0::a1) = 1 + (f a0 + list_size f a1)
[ALL_DISTINCT_FILTER] Theorem
|- !l. ALL_DISTINCT l = !x. MEM x l ==> (FILTER ($= x) l = [x])
[APPEND_11] Theorem
|- (!l1 l2 l3. (l1 ++ l2 = l1 ++ l3) = (l2 = l3)) /\
!l1 l2 l3. (l2 ++ l1 = l3 ++ l1) = (l2 = l3)
[APPEND_ASSOC] Theorem
|- !l1 l2 l3. l1 ++ (l2 ++ l3) = l1 ++ l2 ++ l3
[APPEND_FRONT_LAST] Theorem
|- !l. ~(l = []) ==> (FRONT l ++ [LAST l] = l)
[APPEND_NIL] Theorem
|- !l. l ++ [] = l
[APPEND_eq_NIL] Theorem
|- (!l1 l2. ([] = l1 ++ l2) = (l1 = []) /\ (l2 = [])) /\
!l1 l2. (l1 ++ l2 = []) = (l1 = []) /\ (l2 = [])
[CONS] Theorem
|- !l. ~NULL l ==> (HD l::TL l = l)
[CONS_11] Theorem
|- !a0 a1 a0' a1'. (a0::a1 = a0'::a1') = (a0 = a0') /\ (a1 = a1')
[CONS_ACYCLIC] Theorem
|- !l x. ~(l = x::l) /\ ~(x::l = l)
[EL_ZIP] Theorem
|- !l1 l2 n.
(LENGTH l1 = LENGTH l2) /\ n < LENGTH l1 ==>
(EL n (ZIP (l1,l2)) = (EL n l1,EL n l2))
[EL_compute] Theorem
|- !n. EL n l = (if n = 0 then HD l else EL (PRE n) (TL l))
[EL_simp] Theorem
|- (EL (NUMERAL (BIT1 n)) l = EL (PRE (NUMERAL (BIT1 n))) (TL l)) /\
(EL (NUMERAL (BIT2 n)) l = EL (NUMERAL (BIT1 n)) (TL l))
[EQ_LIST] Theorem
|- !h1 h2. (h1 = h2) ==> !l1 l2. (l1 = l2) ==> (h1::l1 = h2::l2)
[EVERY_APPEND] Theorem
|- !P l1 l2. EVERY P (l1 ++ l2) = EVERY P l1 /\ EVERY P l2
[EVERY_CONG] Theorem
|- !l1 l2 P P'.
(l1 = l2) /\ (!x. MEM x l2 ==> (P x = P' x)) ==>
(EVERY P l1 = EVERY P' l2)
[EVERY_CONJ] Theorem
|- !l. EVERY (\x. P x /\ Q x) l = EVERY P l /\ EVERY Q l
[EVERY_EL] Theorem
|- !l P. EVERY P l = !n. n < LENGTH l ==> P (EL n l)
[EVERY_MAP] Theorem
|- !P f l. EVERY P (MAP f l) = EVERY (\x. P (f x)) l
[EVERY_MEM] Theorem
|- !P l. EVERY P l = !e. MEM e l ==> P e
[EVERY_MONOTONIC] Theorem
|- !P Q. (!x. P x ==> Q x) ==> !l. EVERY P l ==> EVERY Q l
[EVERY_NOT_EXISTS] Theorem
|- !P l. EVERY P l = ~EXISTS (\x. ~P x) l
[EVERY_SIMP] Theorem
|- !c l. EVERY (\x. c) l = (l = []) \/ c
[EXISTS_APPEND] Theorem
|- !P l1 l2. EXISTS P (l1 ++ l2) = EXISTS P l1 \/ EXISTS P l2
[EXISTS_CONG] Theorem
|- !l1 l2 P P'.
(l1 = l2) /\ (!x. MEM x l2 ==> (P x = P' x)) ==>
(EXISTS P l1 = EXISTS P' l2)
[EXISTS_MAP] Theorem
|- !P f l. EXISTS P (MAP f l) = EXISTS (\x. P (f x)) l
[EXISTS_MEM] Theorem
|- !P l. EXISTS P l = ?e. MEM e l /\ P e
[EXISTS_NOT_EVERY] Theorem
|- !P l. EXISTS P l = ~EVERY (\x. ~P x) l
[EXISTS_SIMP] Theorem
|- !c l. EXISTS (\x. c) l = ~(l = []) /\ c
[FILTER_APPEND_DISTRIB] Theorem
|- !P L M. FILTER P (L ++ M) = FILTER P L ++ FILTER P M
[FOLDL_CONG] Theorem
|- !l l' b b' f f'.
(l = l') /\ (b = b') /\ (!x a. MEM x l' ==> (f a x = f' a x)) ==>
(FOLDL f b l = FOLDL f' b' l')
[FOLDR_CONG] Theorem
|- !l l' b b' f f'.
(l = l') /\ (b = b') /\ (!x a. MEM x l' ==> (f x a = f' x a)) ==>
(FOLDR f b l = FOLDR f' b' l')
[FORALL_LIST] Theorem
|- (!l. P l) = P [] /\ !h t. P t ==> P (h::t)
[FRONT_CONS] Theorem
|- (!x. FRONT [x] = []) /\ !x y z. FRONT (x::y::z) = x::FRONT (y::z)
[IN_LIST_TO_SET] Theorem
|- x IN LIST_TO_SET l = MEM x l
[LAST_CONS] Theorem
|- (!x. LAST [x] = x) /\ !x y z. LAST (x::y::z) = LAST (y::z)
[LENGTH_APPEND] Theorem
|- !l1 l2. LENGTH (l1 ++ l2) = LENGTH l1 + LENGTH l2
[LENGTH_CONS] Theorem
|- !l n. (LENGTH l = SUC n) = ?h l'. (LENGTH l' = n) /\ (l = h::l')
[LENGTH_EQ_CONS] Theorem
|- !P n.
(!l. (LENGTH l = SUC n) ==> P l) =
!l. (LENGTH l = n) ==> (\l. !x. P (x::l)) l
[LENGTH_EQ_NIL] Theorem
|- !P. (!l. (LENGTH l = 0) ==> P l) = P []
[LENGTH_LEN] Theorem
|- !L. LENGTH L = LEN L 0
[LENGTH_MAP] Theorem
|- !l f. LENGTH (MAP f l) = LENGTH l
[LENGTH_NIL] Theorem
|- !l. (LENGTH l = 0) = (l = [])
[LENGTH_UNZIP] Theorem
|- !pl.
(LENGTH (FST (UNZIP pl)) = LENGTH pl) /\
(LENGTH (SND (UNZIP pl)) = LENGTH pl)
[LENGTH_ZIP] Theorem
|- !l1 l2.
(LENGTH l1 = LENGTH l2) ==>
(LENGTH (ZIP (l1,l2)) = LENGTH l1) /\ (LENGTH (ZIP (l1,l2)) = LENGTH l2)
[LEN_LENGTH_LEM] Theorem
|- !L n. LEN L n = LENGTH L + n
[LIST_NOT_EQ] Theorem
|- !l1 l2. ~(l1 = l2) ==> !h1 h2. ~(h1::l1 = h2::l2)
[MAP2_ZIP] Theorem
|- !l1 l2.
(LENGTH l1 = LENGTH l2) ==>
!f. MAP2 f l1 l2 = MAP (UNCURRY f) (ZIP (l1,l2))
[MAP_APPEND] Theorem
|- !f l1 l2. MAP f (l1 ++ l2) = MAP f l1 ++ MAP f l2
[MAP_CONG] Theorem
|- !l1 l2 f f'.
(l1 = l2) /\ (!x. MEM x l2 ==> (f x = f' x)) ==> (MAP f l1 = MAP f' l2)
[MAP_EQ_NIL] Theorem
|- !l f. ((MAP f l = []) = (l = [])) /\ (([] = MAP f l) = (l = []))
[MEM_APPEND] Theorem
|- !e l1 l2. MEM e (l1 ++ l2) = MEM e l1 \/ MEM e l2
[MEM_EL] Theorem
|- !l x. MEM x l = ?n. n < LENGTH l /\ (x = EL n l)
[MEM_FILTER] Theorem
|- !P L x. MEM x (FILTER P L) = P x /\ MEM x L
[MEM_MAP] Theorem
|- !l f x. MEM x (MAP f l) = ?y. (x = f y) /\ MEM y l
[MEM_REVERSE] Theorem
|- !l x. MEM x (REVERSE l) = MEM x l
[MEM_ZIP] Theorem
|- !l1 l2 p.
(LENGTH l1 = LENGTH l2) ==>
(MEM p (ZIP (l1,l2)) = ?n. n < LENGTH l1 /\ (p = (EL n l1,EL n l2)))
[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
[MONO_listRel] Theorem
|- (!x y. R x y ==> R' x y) ==> listRel R x y ==> listRel R' x y
[NOT_CONS_NIL] Theorem
|- !a1 a0. ~(a0::a1 = [])
[NOT_EQ_LIST] Theorem
|- !h1 h2. ~(h1 = h2) ==> !l1 l2. ~(h1::l1 = h2::l2)
[NOT_EVERY] Theorem
|- !P l. ~EVERY P l = EXISTS ($~ o P) l
[NOT_EXISTS] Theorem
|- !P l. ~EXISTS P l = EVERY ($~ o P) l
[NOT_NIL_CONS] Theorem
|- !a1 a0. ~([] = a0::a1)
[NULL] Theorem
|- NULL [] /\ !h t. ~NULL (h::t)
[REVERSE_APPEND] Theorem
|- !l1 l2. REVERSE (l1 ++ l2) = REVERSE l2 ++ REVERSE l1
[REVERSE_REV] Theorem
|- !L. REVERSE L = REV L []
[REVERSE_REVERSE] Theorem
|- !l. REVERSE (REVERSE l) = l
[REV_REVERSE_LEM] Theorem
|- !L1 L2. REV L1 L2 = REVERSE L1 ++ L2
[UNZIP_THM] Theorem
|- (UNZIP [] = ([],[])) /\
(UNZIP ((x,y)::t) = (let (L1,L2) = UNZIP t in (x::L1,y::L2)))
[UNZIP_ZIP] Theorem
|- !l1 l2. (LENGTH l1 = LENGTH l2) ==> (UNZIP (ZIP (l1,l2)) = (l1,l2))
[WF_LIST_PRED] Theorem
|- WF (\L1 L2. ?h. L2 = h::L1)
[ZIP_MAP] Theorem
|- !l1 l2 f1 f2.
(LENGTH l1 = LENGTH l2) ==>
(ZIP (MAP f1 l1,l2) = MAP (\p. (f1 (FST p),SND p)) (ZIP (l1,l2))) /\
(ZIP (l1,MAP f2 l2) = MAP (\p. (FST p,f2 (SND p))) (ZIP (l1,l2)))
[ZIP_UNZIP] Theorem
|- !l. ZIP (UNZIP l) = l
[datatype_list] Theorem
|- DATATYPE (list [] CONS)
[listRel_CONS] Theorem
|- (listRel R (h::t) y = ?h' t'. (y = h'::t') /\ R h h' /\ listRel R t t') /\
(listRel R x (h'::t') = ?h t. (x = h::t) /\ R h h' /\ listRel R t t')
[listRel_LENGTH] Theorem
|- !x y. listRel R x y ==> (LENGTH x = LENGTH y)
[listRel_NIL] Theorem
|- (listRel R [] y = (y = [])) /\ (listRel R x [] = (x = []))
[listRel_cases] Theorem
|- !R a0 a1.
listRel R a0 a1 =
(a0 = []) /\ (a1 = []) \/
?h1 h2 t1 t2. (a0 = h1::t1) /\ (a1 = h2::t2) /\ R h1 h2 /\ listRel R t1 t2
[listRel_ind] Theorem
|- !R listRel'.
listRel' [] [] /\
(!h1 h2 t1 t2.
R h1 h2 /\ listRel' t1 t2 ==> listRel' (h1::t1) (h2::t2)) ==>
!a0 a1. listRel R a0 a1 ==> listRel' a0 a1
[listRel_rules] Theorem
|- !R.
listRel R [] [] /\
!h1 h2 t1 t2. R h1 h2 /\ listRel R t1 t2 ==> listRel R (h1::t1) (h2::t2)
[listRel_strong_ind] Theorem
|- !R listRel'.
listRel' [] [] /\
(!h1 h2 t1 t2.
R h1 h2 /\ listRel R t1 t2 /\ listRel' t1 t2 ==>
listRel' (h1::t1) (h2::t2)) ==>
!a0 a1. listRel R a0 a1 ==> listRel' a0 a1
[list_11] Theorem
|- !a0 a1 a0' a1'. (a0::a1 = a0'::a1') = (a0 = a0') /\ (a1 = a1')
[list_Axiom] Theorem
|- !f0 f1. ?fn. (fn [] = f0) /\ !a0 a1. fn (a0::a1) = f1 a0 a1 (fn a1)
[list_Axiom_old] Theorem
|- !x f. ?!fn1. (fn1 [] = x) /\ !h t. fn1 (h::t) = f (fn1 t) h t
[list_CASES] Theorem
|- !l. (l = []) \/ ?t h. l = h::t
[list_INDUCT] Theorem
|- !P. P [] /\ (!t. P t ==> !h. P (h::t)) ==> !l. P l
[list_case_compute] Theorem
|- !l. list_case b f l = (if NULL l then b else f (HD l) (TL l))
[list_case_cong] Theorem
|- !M M' v f.
(M = M') /\ ((M' = []) ==> (v = v')) /\
(!a0 a1. (M' = a0::a1) ==> (f a0 a1 = f' a0 a1)) ==>
(list_case v f M = list_case v' f' M')
[list_distinct] Theorem
|- !a1 a0. ~([] = a0::a1)
[list_induction] Theorem
|- !P. P [] /\ (!t. P t ==> !h. P (h::t)) ==> !l. P l
[list_nchotomy] Theorem
|- !l. (l = []) \/ ?t h. l = h::t
[list_size_cong] Theorem
|- !M N f f'.
(M = N) /\ (!x. MEM x N ==> (f x = f' x)) ==>
(list_size f M = list_size f' N)
*)
end
HOL 4, Kananaskis-3