--- a/src/LK/LK.ML Tue Oct 24 14:50:24 1995 +0100
+++ b/src/LK/LK.ML Tue Oct 24 14:58:02 1995 +0100
@@ -11,45 +11,6 @@
(*Higher precedence than := facilitates use of references*)
infix 4 add_safes add_unsafes;
-signature LK_RESOLVE =
- sig
- datatype pack = Pack of thm list * thm list
- val add_safes: pack * thm list -> pack
- val add_unsafes: pack * thm list -> pack
- val allL_thin: thm
- val best_tac: pack -> int -> tactic
- val could_res: term * term -> bool
- val could_resolve_seq: term * term -> bool
- val cutL_tac: string -> int -> tactic
- val cutR_tac: string -> int -> tactic
- val conL: thm
- val conR: thm
- val empty_pack: pack
- val exR_thin: thm
- val fast_tac: pack -> int -> tactic
- val filseq_resolve_tac: thm list -> int -> int -> tactic
- val forms_of_seq: term -> term list
- val has_prems: int -> thm -> bool
- val iffL: thm
- val iffR: thm
- val less: thm * thm -> bool
- val LK_dup_pack: pack
- val LK_pack: pack
- val pc_tac: pack -> int -> tactic
- val prop_pack: pack
- val repeat_goal_tac: pack -> int -> tactic
- val reresolve_tac: thm list -> int -> tactic
- val RESOLVE_THEN: thm list -> (int -> tactic) -> int -> tactic
- val safe_goal_tac: pack -> int -> tactic
- val step_tac: pack -> int -> tactic
- val symL: thm
- val TrueR: thm
- end;
-
-
-structure LK_Resolve : LK_RESOLVE =
-struct
-
(*Cut and thin, replacing the right-side formula*)
fun cutR_tac (sP: string) i =
res_inst_tac [ ("P",sP) ] cut i THEN rtac thinR i;
@@ -60,31 +21,31 @@
(** If-and-only-if rules **)
-val iffR = prove_goalw LK.thy [iff_def]
+qed_goalw "iffR" LK.thy [iff_def]
"[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
(fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
-val iffL = prove_goalw LK.thy [iff_def]
+qed_goalw "iffL" LK.thy [iff_def]
"[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
(fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);
-val TrueR = prove_goalw LK.thy [True_def]
+qed_goalw "TrueR" LK.thy [True_def]
"$H |- $E, True, $F"
(fn _=> [ rtac impR 1, rtac basic 1 ]);
(** Weakened quantifier rules. Incomplete, they let the search terminate.**)
-val allL_thin = prove_goal LK.thy
+qed_goal "allL_thin" LK.thy
"$H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E"
(fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);
-val exR_thin = prove_goal LK.thy
+qed_goal "exR_thin" LK.thy
"$H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F"
(fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);
(* Symmetry of equality in hypotheses *)
-val symL = prove_goal LK.thy
+qed_goal "symL" LK.thy
"$H, $G, B = A |- $E ==> $H, A = B, $G |- $E"
(fn prems=>
[ (rtac cut 1),
@@ -222,16 +183,12 @@
(** Contraction. Useful since some rules are not complete. **)
-val conR = prove_goal LK.thy
+qed_goal "conR" LK.thy
"$H |- $E, P, $F, P ==> $H |- $E, P, $F"
(fn prems=>
[ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
-val conL = prove_goal LK.thy
+qed_goal "conL" LK.thy
"$H, P, $G, P |- $E ==> $H, P, $G |- $E"
(fn prems=>
[ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
-
-end;
-
-open LK_Resolve;
--- a/src/LK/Makefile Tue Oct 24 14:50:24 1995 +0100
+++ b/src/LK/Makefile Tue Oct 24 14:58:02 1995 +0100
@@ -1,3 +1,4 @@
+# $Id$
#########################################################################
# #
# Makefile for Isabelle (LK) #
@@ -5,9 +6,11 @@
#########################################################################
#To make the system, cd to this directory and type
-# make -f Makefile
+# make
#To make the system and test it on standard examples, type
-# make -f Makefile test
+# make test
+#To generate HTML files for every theory, set the environment variable
+#MAKE_HTML or add the parameter "MAKE_HTML=".
#Environment variable ISABELLECOMP specifies the compiler.
#Environment variable ISABELLEBIN specifies the destination directory.
@@ -25,8 +28,16 @@
case "$(COMP)" in \
poly*) echo 'make_database"$(BIN)/LK"; quit();' \
| $(COMP) $(BIN)/Pure;\
- echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LK ;;\
- sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/LK" banner;' | $(BIN)/Pure ;;\
+ if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+ | $(COMP) $(BIN)/LK;\
+ else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LK;\
+ fi;;\
+ sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+ then echo 'init_html (); exit_use"ROOT.ML"; xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
+ else echo 'exit_use"ROOT.ML"; xML"$(BIN)/LK" banner;' \
+ | $(BIN)/Pure;\
+ fi;;\
*) echo Bad value for ISABELLECOMP: \
$(COMP) is not poly or sml;;\
esac
--- a/src/LK/ROOT.ML Tue Oct 24 14:50:24 1995 +0100
+++ b/src/LK/ROOT.ML Tue Oct 24 14:58:02 1995 +0100
@@ -19,4 +19,6 @@
use "../Pure/install_pp.ML";
print_depth 8;
+make_chart (); (*make HTML chart*)
+
val LK_build_completed = (); (*indicate successful build*)