Revert theory changes in 45c4596

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

src/list/src/listScript.sml

@@ -126,56 +126,72 @@ 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’);
 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

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