diff --git a/src/list/src/ListConv1.sml b/src/list/src/ListConv1.sml index bd78023baa..0d0c190f05 100644 --- a/src/list/src/ListConv1.sml +++ b/src/list/src/ListConv1.sml @@ -280,16 +280,11 @@ end; (* ADDED: TFM 91.10.26 *) (*---------------------------------------------------------------------*) -local - open Psyntax - val l1v = mk_var("l1", listSyntax.mk_list_type alpha) - val l2v = mk_var("l2", listSyntax.mk_list_type alpha) - val hv = mk_var("h", alpha) - val (th1,th2) = CONJ_PAIR (listTheory.APPEND) - val th3 = SPECL [hv,l1v,l2v] th2 - val th4 = GENL [l2v,l1v,hv] th3 +local val (th1,th2) = CONJ_PAIR (listTheory.APPEND) + val th3 = SPECL [%`l1: 'a list`, %`l2: 'a list`] th2 + val th4 = GENL [%`l2: 'a list`, %`l1: 'a list`] th3 fun itfn (cns,ath) v th = - let val th1 = AP_TERM (mk_comb(cns,v)) th + let val th1 = AP_TERM (mk_comb{Rator=cns,Rand=v}) th val l = rand(rator(rand(rator(concl th)))) in TRANS (SPEC v (SPEC l ath)) th1 end diff --git a/src/list/src/listScript.sml b/src/list/src/listScript.sml index daefba4424..4266ce8fd0 100644 --- a/src/list/src/listScript.sml +++ b/src/list/src/listScript.sml @@ -126,30 +126,38 @@ val list_Axiom_old = store_thm( Now some definitions. ---------------------------------------------------------------------------*) -Definition NULL_DEF: - (NULL [] = T) /\ - (NULL (h::t) = F) -End - -Definition HD[simp]: - HD (h::t) = h -End - -Definition TL_DEF[simp]: - TL [] = [] /\ - TL (h::t) = t -End -Theorem TL = CONJUNCT2 TL_DEF - -Definition SUM: - SUM [] = 0 /\ - SUM (h::t) = h + SUM t -End - -Definition APPEND[simp]: - APPEND [] l = l /\ - APPEND (h::l1) l2 = h::APPEND l1 l2 -End +val NULL_DEF = new_recursive_definition + {name = "NULL_DEF", + rec_axiom = list_Axiom, + def = “(NULL [] = T) /\ + (NULL (h::t) = F)”}; + +val HD = new_recursive_definition + {name = "HD", + rec_axiom = list_Axiom, + def = “HD (h::t) = h”}; +val _ = export_rewrites ["HD"] + +val TL_DEF = new_recursive_definition + {name = "TL_DEF", + rec_axiom = list_Axiom, + def = “(TL [] = []) /\ + (TL (h::t) = t)”}; +val TL = save_thm("TL",CONJUNCT2 TL_DEF); +val _ = export_rewrites ["TL_DEF"]; + +val SUM = new_recursive_definition + {name = "SUM", + rec_axiom = list_Axiom, + def = “(SUM [] = 0) /\ + (!h t. SUM (h::t) = h + SUM t)”}; + +val APPEND = new_recursive_definition + {name = "APPEND", + rec_axiom = list_Axiom, + def = “(!l:'a list. APPEND [] l = l) /\ + (!l1 l2 h. APPEND (h::l1) l2 = h::APPEND l1 l2)”}; +val _ = export_rewrites ["APPEND"] val _ = set_fixity "++" (Infixl 480); val _ = overload_on ("++", Term‘APPEND’); @@ -157,25 +165,33 @@ val _ = Unicode.unicode_version {u = UnicodeChars.doubleplus, tmnm = "++"} val _ = TeX_notation { hol = UnicodeChars.doubleplus, TeX = ("\\HOLTokenDoublePlus", 1) } -Definition FLAT[simp]: - FLAT [] = [] /\ - FLAT (h::t) = APPEND h (FLAT t) -End - -Definition LENGTH[simp]: - LENGTH [] = 0 /\ - LENGTH (h::t) = SUC (LENGTH t) -End - -Definition MAP[simp]: - MAP f [] = [] /\ - MAP f (h::t) = f h::MAP f t -End - -Definition LIST_TO_SET_DEF[simp]: - (LIST_TO_SET [] x <=> F) /\ - (LIST_TO_SET (h::t) x <=> (x = h) \/ LIST_TO_SET t x) -End +val FLAT = new_recursive_definition + {name = "FLAT", + rec_axiom = list_Axiom, + def = “(FLAT [] = []) /\ + (!h t. FLAT (h::t) = APPEND h (FLAT t))”}; +val _ = export_rewrites ["FLAT"] + +val LENGTH = new_recursive_definition + {name = "LENGTH", + rec_axiom = list_Axiom, + def = “(LENGTH [] = 0) /\ + (!(h:'a) t. LENGTH (h::t) = SUC (LENGTH t))”}; +val _ = export_rewrites ["LENGTH"] + +val MAP = new_recursive_definition + {name = "MAP", + rec_axiom = list_Axiom, + def = “(!f:'a->'b. MAP f [] = []) /\ + (!f h t. MAP f (h::t) = f h::MAP f t)”}; +val _ = export_rewrites ["MAP"] + +val LIST_TO_SET_DEF = new_recursive_definition{ + name = "LIST_TO_SET_DEF", + rec_axiom = list_Axiom, + def = “(!x:'a. LIST_TO_SET [] x <=> F) /\ + (!h:'a t x. LIST_TO_SET (h::t) x <=> (x = h) \/ LIST_TO_SET t x)”} +val _ = export_rewrites ["LIST_TO_SET_DEF"] val _ = overload_on ("set", “LIST_TO_SET”) val _ = overload_on ("MEM", “\h:'a l:'a list. h IN LIST_TO_SET l”) @@ -194,35 +210,48 @@ Proof SRW_TAC [] [FUN_EQ_THM, IN_DEF] QED -Definition FILTER[simp]: - FILTER P [] = [] /\ - FILTER P (h::t) = if P h then (h::FILTER P t) else FILTER P t -End +val FILTER = new_recursive_definition + {name = "FILTER", + rec_axiom = list_Axiom, + def = “(!P. FILTER P [] = []) /\ + (!(P:'a->bool) h t. + FILTER P (h::t) = + if P h then (h::FILTER P t) else FILTER P t)”}; +val _ = export_rewrites ["FILTER"] + +val FOLDR = new_recursive_definition + {name = "FOLDR", + rec_axiom = list_Axiom, + def = “(!f e. FOLDR (f:'a->'b->'b) e [] = e) /\ + (!f e x l. FOLDR f e (x::l) = f x (FOLDR f e l))”}; + +val FOLDL = new_recursive_definition + {name = "FOLDL", + rec_axiom = list_Axiom, + def = “(!f e. FOLDL (f:'b->'a->'b) e [] = e) /\ + (!f e x l. FOLDL f e (x::l) = FOLDL f (f e x) l)”}; + +val EVERY_DEF = new_recursive_definition + {name = "EVERY_DEF", + rec_axiom = list_Axiom, + def = “(!P:'a->bool. EVERY P [] = T) /\ + (!P h t. EVERY P (h::t) <=> P h /\ EVERY P t)”}; +val _ = export_rewrites ["EVERY_DEF"] + +val EXISTS_DEF = new_recursive_definition + {name = "EXISTS_DEF", + rec_axiom = list_Axiom, + def = “(!P:'a->bool. EXISTS P [] = F) + /\ (!P h t. EXISTS P (h::t) <=> P h \/ EXISTS P t)”}; +val _ = export_rewrites ["EXISTS_DEF"] + +val EL = new_recursive_definition + {name = "EL", + rec_axiom = num_Axiom, + def = “(!l. EL 0 l = (HD l:'a)) /\ + (!l:'a list. !n. EL (SUC n) l = EL n (TL l))”}; -Definition FOLDR: - FOLDR (f:'a->'b->'b) e [] = e /\ - FOLDR f e (x::l) = f x (FOLDR f e l) -End -Definition FOLDL: - FOLDL (f:'b->'a->'b) e [] = e /\ - FOLDL f e (x::l) = FOLDL f (f e x) l -End - -Definition EVERY_DEF[simp]: - (EVERY P [] <=> T) /\ - (EVERY P (h::t) <=> P h /\ EVERY P t) -End - -Definition EXISTS_DEF[simp]: - (EXISTS P [] <=> F) /\ - (EXISTS P (h::t) <=> P h \/ EXISTS P t) -End - -Definition EL: - EL 0 l = (HD l:'a) /\ - EL (SUC n) l = EL n (TL l) -End (* ---------------------------------------------------------------------*) (* Definition of a function *) @@ -1226,10 +1255,9 @@ val NOT_NULL_MEM = Q.store_thm Cases_on ‘l’ THEN SIMP_TAC bool_ss [EXISTS_OR_THM, MEM, NOT_CONS_NIL, NULL]); (* Computing EL when n is in numeral representation *) -Theorem EL_compute[allow_rebind]: - !n. EL n l = if n=0 then HD l else EL (PRE n) (TL l) -Proof INDUCT_TAC THEN ASM_REWRITE_TAC [NOT_SUC, EL, PRE] -QED +val EL_compute = store_thm("EL_compute", +Term ‘!n. EL n l = if n=0 then HD l else EL (PRE n) (TL l)’, +INDUCT_TAC THEN ASM_REWRITE_TAC [NOT_SUC, EL, PRE]); (* a version of the above that is safe to use in the simplifier *) (* only bother with BIT1/2 cases because the zero case is already provided diff --git a/src/list/src/selftest.sml b/src/list/src/selftest.sml index f63a490b75..f298474f2c 100644 --- a/src/list/src/selftest.sml +++ b/src/list/src/selftest.sml @@ -64,11 +64,6 @@ val _ = app(test "LASTN_CONV" Term.compare term_to_string LASTN_CONV) val _ = app(test "LIST_EQ_SIMP_CONV" Term.compare term_to_string listSimps.LIST_EQ_SIMP_CONV) [(``(l1:'a list ++ [])::t = p ++ q``, ``(l1:'a list)::t = p ++ q``)] -val _ = app(test "APPEND_CONV" Term.compare term_to_string - ListConv1.APPEND_CONV) - [(“[1;2;3] ++ [4;5;6]”, “[1;2;3;4;5;6]”), - (“[] ++ [1]”, “[1]”), (“[1;2] ++ []”, “[1;2]”), - (“[x;y] ++ [y;x]:'a list”, “[x;y;y;x]:'a list”)] val _ = Lib.appi (fn i => fn t => test0 ("EL_CONV "^Int.toString (i+1))