Remove some uses of Theory.adjoin*

Could have used the new facilities to make the set_skip call on K
persistent, but with K_THM in the compset, this wasn't doing anything
anyway.

src/combin/combinScript.sml

@@ -10,7 +10,7 @@
 (* AUGMENTED     : (kxs) added C and W combinators                       *)
 (* ===================================================================== *)
 
-open HolKernel Parse boolLib;
+open HolKernel Parse boolLib computeLib;
 
 val _ = new_theory "combin";
 
@@ -20,14 +20,14 @@ val _ = new_theory "combin";
 
 fun def (s,l) p = Q.new_definition_at (DB_dtype.mkloc(s,l,false)) p
 
-val K_DEF = def(#(FILE),#(LINE))("K_DEF",        `K = \x y. x`);
-val S_DEF = def(#(FILE),#(LINE))("S_DEF",        `S = \f g x. f x (g x)`);
-val I_DEF = def(#(FILE),#(LINE))("I_DEF",        `I = S K (K:'a->'a->'a)`);
-val C_DEF = def(#(FILE),#(LINE))("C_DEF",        `C = \f x y. f y x`);
-val W_DEF = def(#(FILE),#(LINE))("W_DEF",        `W = \f x. f x x`);
-val o_DEF = def(#(FILE),#(LINE))("o_DEF", `$o f g = \x. f(g x)`);
+val K_DEF = def(#(FILE),#(LINE))("K_DEF",             ‘K = \x y. x’);
+val S_DEF = def(#(FILE),#(LINE))("S_DEF[compute]",    ‘S = \f g x. f x (g x)’);
+val I_DEF = def(#(FILE),#(LINE))("I_DEF",             ‘I = S K (K:'a->'a->'a)’);
+val C_DEF = def(#(FILE),#(LINE))("C_DEF[compute]",    ‘C = \f x y. f y x’);
+val W_DEF = def(#(FILE),#(LINE))("W_DEF[compute]",    ‘W = \f x. f x x’);
+val o_DEF = def(#(FILE),#(LINE))("o_DEF",             ‘$o f g = \x. f(g x)’);
 val _ = set_fixity "o" (Infixr 800)
-val APP_DEF = def(#(FILE),#(LINE)) ("APP_DEF",   `$:> x f = f x`);
+val APP_DEF = def(#(FILE),#(LINE))("APP_DEF[compute]",‘$:> x f = f x’);
 
 val UPDATE_def = def(#(FILE),#(LINE))("UPDATE_def",
    `UPDATE a b = \f c. if a = c then b else f c`);
@@ -92,12 +92,14 @@ end
  * superset of those on the rhs.                                             *
  *---------------------------------------------------------------------------*)
 
-val o_THM = store_thm("o_THM",
-   “!f g x. (f o g) x = f(g x)”,
+Theorem o_THM[compute]:
+   !f g x. (f o g) x = f(g x)
+Proof
    REPEAT GEN_TAC
    THEN PURE_REWRITE_TAC [ o_DEF ]
    THEN CONV_TAC (DEPTH_CONV BETA_CONV)
-   THEN REFL_TAC);
+   THEN REFL_TAC
+QED
 
 val o_ASSOC = store_thm("o_ASSOC",
    “!f g h. f o (g o h) = (f o g) o h”,
@@ -118,12 +120,14 @@ val o_ABS_R = store_thm(
   ``f o (\x. g x) = (\x. f (g x))``,
   REWRITE_TAC [FUN_EQ_THM, o_THM] THEN BETA_TAC THEN REWRITE_TAC []);
 
-val K_THM = store_thm("K_THM",
-    “!x y. K x y = x”,
+Theorem K_THM[compute]:
+    !x y. K x y = x
+Proof
     REPEAT GEN_TAC
     THEN PURE_REWRITE_TAC [ K_DEF ]
     THEN CONV_TAC (DEPTH_CONV BETA_CONV)
-    THEN REFL_TAC);
+    THEN REFL_TAC
+QED
 
 Theorem K_PARTIAL : (* from seqTheory *)
     !x. K x = \z. x
@@ -168,12 +172,14 @@ val W_THM = store_thm("W_THM",
    THEN CONV_TAC (DEPTH_CONV BETA_CONV)
    THEN REFL_TAC);
 
-val I_THM = store_thm("I_THM",
-   “!x. I x = x”,
+Theorem I_THM[compute]:
+   !x. I x = x
+Proof
    REPEAT GEN_TAC
    THEN PURE_REWRITE_TAC [ I_DEF, S_THM, K_THM ]
    THEN CONV_TAC (DEPTH_CONV BETA_CONV)
-   THEN REFL_TAC);
+   THEN REFL_TAC
+QED
 
 Theorem I_EQ_IDABS:
   I = \x. x
@@ -185,9 +191,11 @@ val I_o_ID = store_thm("I_o_ID",
    “!f. (I o f = f) /\ (f o I = f)”,
    REWRITE_TAC [I_THM, o_THM, FUN_EQ_THM]);
 
-val K_o_THM = store_thm("K_o_THM",
-  “(!f v. K v o f = K v) /\ (!f v. f o K v = K (f v))”,
-  REWRITE_TAC [o_THM, K_THM, FUN_EQ_THM]);
+Theorem K_o_THM[compute]:
+  (!f v. K v o f = K v) /\ (!f v. f o K v = K (f v))
+Proof
+  REWRITE_TAC [o_THM, K_THM, FUN_EQ_THM]
+QED
 
 val UPDATE_APPLY = Q.store_thm("UPDATE_APPLY",
    `(!a x f. (a =+ x) f a = x) /\
@@ -200,10 +208,12 @@ val UPDATE_APPLY = Q.store_thm("UPDATE_APPLY",
 
 Theorem UPDATE_APPLY1 = cj 1 UPDATE_APPLY
 
-val APPLY_UPDATE_THM = Q.store_thm("APPLY_UPDATE_THM",
-  `!f a b c. (a =+ b) f c = (if a = c then b else f c)`,
+Theorem APPLY_UPDATE_THM[compute]:
+  !f a b c. (a =+ b) f c = (if a = c then b else f c)
+Proof
   PURE_REWRITE_TAC [UPDATE_def]
-  THEN BETA_TAC THEN REWRITE_TAC []);
+  THEN BETA_TAC THEN REWRITE_TAC []
+QED
 
 val UPDATE_COMMUTES = Q.store_thm("UPDATE_COMMUTES",
   `!f a b c d. ~(a = b) ==> ((a =+ c) ((b =+ d) f) = (b =+ d) ((a =+ c) f))`,
@@ -553,37 +563,4 @@ Proof
  >> ASM_REWRITE_TAC []
 QED
 
-(*---------------------------------------------------------------------------*)
-
-val _ = adjoin_to_theory
-{sig_ps = NONE,
- struct_ps = SOME (fn _ =>
-  let val S = PP.add_string fun SPC n = PP.add_break(1,n)
-      fun B n = PP.block PP.CONSISTENT n
-      fun I n = PP.block PP.INCONSISTENT n
-      val L = PP.pr_list
-  in
-    B 0 [
-      S "val _ =", SPC 2,
-      B 4 [
-        S "let open computeLib", SPC 0,
-        B 2 [
-          S "val K_tm =", SPC 0,
-          S "Term.prim_mk_const{Name=\"K\",Thy=\"combin\"}"
-        ], SPC ~4,
-        S "in", SPC 0,
-        B 2 [
-          S "add_funs", SPC 0,
-          I 1 (S "[" ::
-               L S [S ",", PP.add_break(0,0)] [
-                 "K_THM", "S_DEF", "I_THM", "C_DEF", "W_DEF", "o_THM",
-                 "K_o_THM", "APP_DEF", "APPLY_UPDATE_THM];"
-              ])
-        ], SPC 0,
-        B 2 (L S [SPC 1] ["set_skip", "the_compset", "K_tm", "(SOME 1)"]),
-        SPC ~4, S "end;"
-      ]
-    ]
-  end)}
-
 val _ = export_theory();