--- a/src/Pure/Thy/thy_read.ML Wed Nov 27 10:52:31 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML Wed Nov 27 10:54:16 1996 +0100
@@ -160,12 +160,13 @@
structures inherit this value.)
*)
val gif_path = ref (tack_on ("/" ^
- space_implode "/" (rev (tl (tl (rev (space_explode "/" (pwd ())))))))
+ space_implode "/" (rev (tl (tl (rev (space_explode "/"
+ (OS.FileSys.getDir ())))))))
"Tools");
(*Path of Isabelle's main directory*)
val base_path = ref (
- "/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (pwd ())))))));
+ "/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (OS.FileSys.getDir ())))))));
(** HTML variables **)
@@ -181,7 +182,7 @@
(*HTML file of theory currently being read
(Initialized by thyfile2html; used by use_thy and store_thm)*)
-val cur_htmlfile = ref None : outstream option ref;
+val cur_htmlfile = ref None : TextIO.outstream option ref;
(*Boolean variable which indicates if the title "Theorems proved in foo.ML"
has already been inserted into the current HTML file*)
@@ -192,18 +193,18 @@
-(*Make name of the output ML file for a theory *)
+(*Make name of the TextIO.output ML file for a theory *)
fun out_name tname = "." ^ tname ^ ".thy.ML";
(*Read a file specified by thy_file containing theory thy *)
fun read_thy tname thy_file =
let
- val instream = open_in thy_file;
- val outstream = open_out (out_name tname);
+ val instream = TextIO.openIn thy_file;
+ val outstream = TextIO.openOut (out_name tname);
in
- output (outstream, ThySyn.parse tname (input (instream, 999999)));
- close_out outstream;
- close_in instream
+ TextIO.output (outstream, ThySyn.parse tname (TextIO.inputAll instream));
+ TextIO.closeOut outstream;
+ TextIO.closeIn instream
end;
fun file_exists file = (file_info file <> "");
@@ -286,7 +287,7 @@
fun get_filenames path name =
let fun new_filename () =
let val found = find_file path (name ^ ".thy");
- val absolute_path = absolute_path (pwd ());
+ val absolute_path = absolute_path (OS.FileSys.getDir ());
val thy_file = absolute_path found;
val (thy_path, _) = split_filename thy_file;
val found = find_file path (name ^ ".ML");
@@ -389,7 +390,7 @@
index_path: relative path to directory containing main theory chart
*)
fun mk_charthead file tname title repeats gif_path index_path package =
- output (file,
+ TextIO.output (file,
"<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^
"</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^
"</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^
@@ -499,8 +500,8 @@
(** Make chart of super-theories **)
- val sup_out = open_out (tack_on tpath ("." ^ tname ^ "_sup.html"));
- val sub_out = open_out (tack_on tpath ("." ^ tname ^ "_sub.html"));
+ val sup_out = TextIO.openOut (tack_on tpath ("." ^ tname ^ "_sup.html"));
+ val sub_out = TextIO.openOut (tack_on tpath ("." ^ tname ^ "_sub.html"));
(*Theories that already have been listed in this chart*)
val listed = ref [];
@@ -528,7 +529,7 @@
| mk_offset (l::ls) cur =
implode (replicate (l - cur) " ") ^ "| " ^
mk_offset ls (l+1);
- in output (sup_out,
+ in TextIO.output (sup_out,
" " ^ mk_offset continued 0 ^
"\\__" ^ (if is_pure then t else
"<A HREF=\"" ^ tack_on rel_path ("." ^ t) ^
@@ -554,31 +555,31 @@
filter (fn s => s mem wanted_theories) (parents_of_name tname);
in mk_entry relatives end;
in if is_some (!cur_htmlfile) then
- (close_out (the (!cur_htmlfile));
+ (TextIO.closeOut (the (!cur_htmlfile));
warning "Last theory's HTML file has not been closed.")
else ();
- cur_htmlfile := Some (open_out (tack_on tpath ("." ^ tname ^ ".html")));
+ cur_htmlfile := Some (TextIO.openOut (tack_on tpath ("." ^ tname ^ ".html")));
cur_has_title := false;
- output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy"));
+ TextIO.output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy"));
mk_charthead sup_out tname "Ancestors" true gif_path rel_index_path
package;
- output(sup_out,
+ TextIO.output(sup_out,
"<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \
\<A HREF = \"." ^ tname ^
"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\n");
list_ancestors tname 0 [];
- output (sup_out, "</PRE><HR></BODY></HTML>");
- close_out sup_out;
+ TextIO.output (sup_out, "</PRE><HR></BODY></HTML>");
+ TextIO.closeOut sup_out;
mk_charthead sub_out tname "Children" false gif_path rel_index_path
package;
- output(sub_out,
+ TextIO.output(sub_out,
"<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \
\<A HREF = \"." ^ tname ^ "_sup.html\"><IMG SRC = \"" ^
tack_on gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n");
- close_out sub_out
+ TextIO.closeOut sub_out
end;
(*Invoke every put method stored in a theory's methods table to initialize
@@ -694,11 +695,11 @@
val fname = tack_on path ("." ^ t ^ "_sub.html");
val out = if file_exists fname then
- open_append fname handle e =>
+ TextIO.openAppend fname handle e =>
(warning ("Unable to write to file " ^
fname); raise e)
else raise MK_HTML;
- in output (out,
+ in TextIO.output (out,
" |\n \\__<A HREF=\"" ^
tack_on rel_path ("." ^ tname) ^ ".html\">" ^ tname ^
"</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\
@@ -707,11 +708,11 @@
\<A HREF = \"" ^ tpath ^ "_sup.html\">\
\<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n");
- close_out out
+ TextIO.closeOut out
end;
val theory_list =
- open_append (tack_on (!index_path) ".theory_list.txt")
+ TextIO.openAppend (tack_on (!index_path) ".theory_list.txt")
handle _ => (make_html := false;
writeln ("Warning: Cannot write to " ^
(!index_path) ^ " while making HTML files.\n\
@@ -719,8 +720,8 @@
\Call init_html() from within a \
\writeable directory to reactivate it.");
raise MK_HTML)
- in output (theory_list, tname ^ " " ^ abs_path ^ "\n");
- close_out theory_list;
+ in TextIO.output (theory_list, tname ^ " " ^ abs_path ^ "\n");
+ TextIO.closeOut theory_list;
robust_seq add_to_parents new_parents
end
@@ -761,7 +762,7 @@
in map store_thm_db axioms end;
if not (!delete_tmpfiles) then ()
- else delete_file (out_name tname);
+ else OS.FileSys.remove (out_name tname);
if not (!make_html) then ()
else thyfile2html abs_path tname
@@ -798,8 +799,8 @@
(*Close HTML file*)
case !cur_htmlfile of
- Some out => (output (out, "<HR></BODY></HTML>\n");
- close_out out;
+ Some out => (TextIO.output (out, "<HR></BODY></HTML>\n");
+ TextIO.closeOut out;
cur_htmlfile := None)
| None => ()
)
@@ -1064,7 +1065,7 @@
fun mk_theorems_title out =
if not (!cur_has_title) then
(cur_has_title := true;
- output (out, "<HR><H2>Theorems proved in <A HREF = \"" ^
+ TextIO.output (out, "<HR><H2>Theorems proved in <A HREF = \"" ^
(!cur_thyname) ^ ".ML\">" ^ (!cur_thyname) ^
".ML</A>:</H2>\n"))
else ();
@@ -1095,10 +1096,10 @@
in case !cur_htmlfile of
Some out =>
(mk_theorems_title out;
- output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^
+ TextIO.output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^
escape
- (explode
- (string_of_thm (#1 (freeze_thaw thm)))) ^
+ (explode
+ (string_of_thm (#1 (freeze_thaw thm)))) ^
"</PRE><P>\n")
)
| None => ()
@@ -1173,16 +1174,16 @@
(*Init HTML generator by setting paths and creating new files*)
fun init_html () =
- let val cwd = pwd();
+ let val cwd = OS.FileSys.getDir();
- val theory_list = close_out (open_out ".theory_list.txt");
+ val theory_list = TextIO.closeOut (TextIO.openOut ".theory_list.txt");
val rel_gif_path = relative_path cwd (!gif_path);
(*Make new HTML files for Pure and CPure*)
fun init_pure_html () =
- let val pure_out = open_out ".Pure_sub.html";
- val cpure_out = open_out ".CPure_sub.html";
+ let val pure_out = TextIO.openOut ".Pure_sub.html";
+ val cpure_out = TextIO.openOut ".CPure_sub.html";
val package =
if cwd subdir_of (!base_path) then
relative_path (!base_path) cwd
@@ -1191,10 +1192,10 @@
package;
mk_charthead cpure_out "CPure" "Children" false rel_gif_path ""
package;
- output (pure_out, "Pure\n");
- output (cpure_out, "CPure\n");
- close_out pure_out;
- close_out cpure_out;
+ TextIO.output (pure_out, "Pure\n");
+ TextIO.output (cpure_out, "CPure\n");
+ TextIO.closeOut pure_out;
+ TextIO.closeOut cpure_out;
pure_subchart := Some cwd
end;
in make_html := true;
@@ -1202,9 +1203,9 @@
(*Make sure that base_path contains the physical path and no
symbolic links*)
- cd (!base_path);
- base_path := pwd();
- cd cwd;
+ OS.FileSys.chDir (!base_path);
+ base_path := OS.FileSys.getDir();
+ OS.FileSys.chDir cwd;
if cwd subdir_of (!base_path) then ()
else warning "The current working directory seems to be no \
@@ -1221,9 +1222,9 @@
(*Generate index.html*)
fun finish_html () = if not (!make_html) then () else
let val tlist_path = tack_on (!index_path) ".theory_list.txt";
- val theory_list = open_in tlist_path;
- val theories = space_explode "\n" (input (theory_list, 999999));
- val dummy = (close_in theory_list; delete_file tlist_path);
+ val theory_list = TextIO.openIn tlist_path;
+ val theories = space_explode "\n" (TextIO.inputAll theory_list);
+ val dummy = (TextIO.closeIn theory_list; OS.FileSys.remove tlist_path);
val gif_path = relative_path (!index_path) (!gif_path);
@@ -1243,7 +1244,7 @@
".html\">" ^ tname ^ "</A><BR>\n"
end;
- val out = open_out (tack_on (!index_path) "index.html");
+ val out = TextIO.openOut (tack_on (!index_path) "index.html");
(*Find out in which subdirectory of Isabelle's main directory the
index.html is placed; if index_path is no subdirectory of base_path
@@ -1269,25 +1270,25 @@
(*Add link to current directory to 'super' index.html*)
fun link_directory () =
- let val old_index = open_in (super_index ^ "/index.html");
- val content = rev (explode (input (old_index, 999999)));
- val dummy = close_in old_index;
+ let val old_index = TextIO.openIn (super_index ^ "/index.html");
+ val content = rev (explode (TextIO.inputAll old_index));
+ val dummy = TextIO.closeIn old_index;
- val out = open_append (super_index ^ "/index.html");
+ val out = TextIO.openAppend (super_index ^ "/index.html");
val rel_path = space_implode "/" (drop (level, subdirs));
in
- output (out,
+ TextIO.output (out,
(if nth_elem (3, content) <> "!" then ""
else "\n<HR><H3>Subdirectories:</H3>\n") ^
"<H3><A HREF = \"" ^ rel_path ^ "/index.html\">" ^ rel_path ^
"</A></H3>\n");
- close_out out
+ TextIO.closeOut out
end;
(*If index_path is no subdirectory of base_path then the title should
not contain the string "Isabelle/"*)
val title = (if inside_isabelle then "Isabelle/" else "") ^ subdir;
- in output (out,
+ in TextIO.output (out,
"<HTML><HEAD><TITLE>" ^ title ^ "</TITLE></HEAD>\n\
\<BODY><H2>" ^ title ^ "</H2>\n\
\The name of every theory is linked to its theory file<BR>\n\
@@ -1309,7 +1310,7 @@
"<BR>View the <A HREF = \"README\">ReadMe</A> file.\n"
else "") ^
"<HR>" ^ implode (map main_entry theories) ^ "<!-->");
- close_out out;
+ TextIO.closeOut out;
if super_index = "" orelse (inside_isabelle andalso level = 0) then ()
else link_directory ()
end;
@@ -1318,7 +1319,7 @@
fun section s =
case !cur_htmlfile of
Some out => (mk_theorems_title out;
- output (out, "<H3>" ^ s ^ "</H3>\n"))
+ TextIO.output (out, "<H3>" ^ s ^ "</H3>\n"))
| None => ();
@@ -1354,7 +1355,7 @@
(*Add file to thy_reader_files list*)
fun set_thy_reader_file file =
- let val file' = absolute_path (pwd ()) file;
+ let val file' = absolute_path (OS.FileSys.getDir ()) file;
in thy_reader_files := file' :: (!thy_reader_files) end;
(*Add file and also 'use' it*)
@@ -1377,12 +1378,12 @@
local
fun gen_use_dir use_cmd dirname =
- let val old_dir = pwd ();
- in cd dirname;
+ let val old_dir = OS.FileSys.getDir ();
+ in OS.FileSys.chDir dirname;
if !make_html then init_html() else ();
use_cmd "ROOT.ML";
finish_html();
- cd old_dir
+ OS.FileSys.chDir old_dir
end;
in
--- a/src/Pure/tctical.ML Wed Nov 27 10:52:31 1996 +0100
+++ b/src/Pure/tctical.ML Wed Nov 27 10:54:16 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: tctical
+(* Title: tctical
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Tacticals
@@ -15,53 +15,53 @@
signature TACTICAL =
sig
type tactic (* = thm -> thm Sequence.seq*)
- val all_tac : tactic
- val ALLGOALS : (int -> tactic) -> tactic
- val APPEND : tactic * tactic -> tactic
- val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
- val CHANGED : tactic -> tactic
- val COND : (thm -> bool) -> tactic -> tactic -> tactic
- val DETERM : tactic -> tactic
- val EVERY : tactic list -> tactic
- val EVERY' : ('a -> tactic) list -> 'a -> tactic
- val EVERY1 : (int -> tactic) list -> tactic
- val FILTER : (thm -> bool) -> tactic -> tactic
- val FIRST : tactic list -> tactic
- val FIRST' : ('a -> tactic) list -> 'a -> tactic
- val FIRST1 : (int -> tactic) list -> tactic
- val FIRSTGOAL : (int -> tactic) -> tactic
- val goals_limit : int ref
- val INTLEAVE : tactic * tactic -> tactic
- val INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
- val METAHYPS : (thm list -> tactic) -> int -> tactic
- val no_tac : tactic
- val ORELSE : tactic * tactic -> tactic
- val ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
- val pause_tac : tactic
- val print_tac : tactic
- val REPEAT : tactic -> tactic
- val REPEAT1 : tactic -> tactic
- val REPEAT_DETERM_N : int -> tactic -> tactic
- val REPEAT_DETERM : tactic -> tactic
- val REPEAT_DETERM1 : tactic -> tactic
+ val all_tac : tactic
+ val ALLGOALS : (int -> tactic) -> tactic
+ val APPEND : tactic * tactic -> tactic
+ val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+ val CHANGED : tactic -> tactic
+ val COND : (thm -> bool) -> tactic -> tactic -> tactic
+ val DETERM : tactic -> tactic
+ val EVERY : tactic list -> tactic
+ val EVERY' : ('a -> tactic) list -> 'a -> tactic
+ val EVERY1 : (int -> tactic) list -> tactic
+ val FILTER : (thm -> bool) -> tactic -> tactic
+ val FIRST : tactic list -> tactic
+ val FIRST' : ('a -> tactic) list -> 'a -> tactic
+ val FIRST1 : (int -> tactic) list -> tactic
+ val FIRSTGOAL : (int -> tactic) -> tactic
+ val goals_limit : int ref
+ val INTLEAVE : tactic * tactic -> tactic
+ val INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+ val METAHYPS : (thm list -> tactic) -> int -> tactic
+ val no_tac : tactic
+ val ORELSE : tactic * tactic -> tactic
+ val ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+ val pause_tac : tactic
+ val print_tac : tactic
+ val REPEAT : tactic -> tactic
+ val REPEAT1 : tactic -> tactic
+ val REPEAT_DETERM_N : int -> tactic -> tactic
+ val REPEAT_DETERM : tactic -> tactic
+ val REPEAT_DETERM1 : tactic -> tactic
val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic
val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
- val REPEAT_FIRST : (int -> tactic) -> tactic
- val REPEAT_SOME : (int -> tactic) -> tactic
- val SELECT_GOAL : tactic -> int -> tactic
- val SOMEGOAL : (int -> tactic) -> tactic
- val STATE : (thm -> tactic) -> tactic
- val strip_context : term -> (string * typ) list * term list * term
- val SUBGOAL : ((term*int) -> tactic) -> int -> tactic
- val suppress_tracing : bool ref
- val THEN : tactic * tactic -> tactic
- val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
- val THEN_ELSE : tactic * (tactic*tactic) -> tactic
- val traced_tac : (thm -> (thm * thm Sequence.seq) option) -> tactic
- val tracify : bool ref -> tactic -> thm -> thm Sequence.seq
- val trace_REPEAT : bool ref
- val TRY : tactic -> tactic
- val TRYALL : (int -> tactic) -> tactic
+ val REPEAT_FIRST : (int -> tactic) -> tactic
+ val REPEAT_SOME : (int -> tactic) -> tactic
+ val SELECT_GOAL : tactic -> int -> tactic
+ val SOMEGOAL : (int -> tactic) -> tactic
+ val STATE : (thm -> tactic) -> tactic
+ val strip_context : term -> (string * typ) list * term list * term
+ val SUBGOAL : ((term*int) -> tactic) -> int -> tactic
+ val suppress_tracing : bool ref
+ val THEN : tactic * tactic -> tactic
+ val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+ val THEN_ELSE : tactic * (tactic*tactic) -> tactic
+ val traced_tac : (thm -> (thm * thm Sequence.seq) option) -> tactic
+ val tracify : bool ref -> tactic -> thm -> thm Sequence.seq
+ val trace_REPEAT : bool ref
+ val TRY : tactic -> tactic
+ val TRYALL : (int -> tactic) -> tactic
end;
@@ -91,7 +91,7 @@
Does not backtrack to tac2 if tac1 was initially chosen. *)
fun (tac1 ORELSE tac2) st =
case Sequence.pull(tac1 st) of
- None => tac2 st
+ None => tac2 st
| sequencecell => Sequence.seqof(fn()=> sequencecell);
@@ -100,22 +100,22 @@
The tactic tac2 is not applied until needed.*)
fun (tac1 APPEND tac2) st =
Sequence.append(tac1 st,
- Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
+ Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
(*Like APPEND, but interleaves results of tac1 and tac2.*)
fun (tac1 INTLEAVE tac2) st =
Sequence.interleave(tac1 st,
- Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
+ Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
(*Conditional tactic.
- tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
- tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac)
+ tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
+ tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac)
*)
fun (tac THEN_ELSE (tac1, tac2)) st =
case Sequence.pull(tac st) of
- None => tac2 st (*failed; try tactic 2*)
- | seqcell => Sequence.flats (*succeeded; use tactic 1*)
- (Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell)));
+ None => tac2 st (*failed; try tactic 2*)
+ | seqcell => Sequence.flats (*succeeded; use tactic 1*)
+ (Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell)));
(*Versions for combining tactic-valued functions, as in
@@ -135,7 +135,7 @@
(*Make a tactic deterministic by chopping the tail of the proof sequence*)
fun DETERM tac st =
case Sequence.pull (tac st) of
- None => Sequence.null
+ None => Sequence.null
| Some(x,_) => Sequence.cons(x, Sequence.null);
@@ -182,7 +182,7 @@
(*Pause until a line is typed -- if non-empty then fail. *)
fun pause_tac st =
(prs"** Press RETURN to continue: ";
- if input(std_in,1) = "\n" then Sequence.single st
+ if TextIO.inputLine TextIO.stdIn = "\n" then Sequence.single st
else (prs"Goodbye\n"; Sequence.null));
exception TRACE_EXIT of thm
@@ -194,7 +194,7 @@
(*Handle all tracing commands for current state and tactic *)
fun exec_trace_command flag (tac, st) =
- case input_line(std_in) of
+ case TextIO.inputLine(TextIO.stdIn) of
"\n" => tac st
| "f\n" => Sequence.null
| "o\n" => (flag:=false; tac st)
@@ -215,15 +215,15 @@
fun tracify flag tac st =
if !flag andalso not (!suppress_tracing)
then (!print_goals_ref (!goals_limit) st;
- prs"** Press RETURN to continue: ";
- exec_trace_command flag (tac,st))
+ prs"** Press RETURN to continue: ";
+ exec_trace_command flag (tac,st))
else tac st;
(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
fun traced_tac seqf st =
(suppress_tracing := false;
Sequence.seqof (fn()=> seqf st
- handle TRACE_EXIT st' => Some(st', Sequence.null)));
+ handle TRACE_EXIT st' => Some(st', Sequence.null)));
(*Deterministic REPEAT: only retains the first outcome;
@@ -232,10 +232,10 @@
fun REPEAT_DETERM_N n tac =
let val tac = tracify trace_REPEAT tac
fun drep 0 st = Some(st, Sequence.null)
- | drep n st =
- (case Sequence.pull(tac st) of
- None => Some(st, Sequence.null)
- | Some(st',_) => drep (n-1) st')
+ | drep n st =
+ (case Sequence.pull(tac st) of
+ None => Some(st, Sequence.null)
+ | Some(st',_) => drep (n-1) st')
in traced_tac (drep n) end;
(*Allows any number of repetitions*)
@@ -245,12 +245,12 @@
fun REPEAT tac =
let val tac = tracify trace_REPEAT tac
fun rep qs st =
- case Sequence.pull(tac st) of
- None => Some(st, Sequence.seqof(fn()=> repq qs))
+ case Sequence.pull(tac st) of
+ None => Some(st, Sequence.seqof(fn()=> repq qs))
| Some(st',q) => rep (q::qs) st'
and repq [] = None
| repq(q::qs) = case Sequence.pull q of
- None => repq qs
+ None => repq qs
| Some(st,q) => rep (q::qs) st
in traced_tac (rep []) end;
@@ -276,13 +276,13 @@
Essential to work backwards since tac(i) may add/delete subgoals at i. *)
fun ALLGOALS tac st =
let fun doall 0 = all_tac
- | doall n = tac(n) THEN doall(n-1)
+ | doall n = tac(n) THEN doall(n-1)
in doall(nprems_of st)st end;
(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *)
fun SOMEGOAL tac st =
let fun find 0 = no_tac
- | find n = tac(n) ORELSE find(n-1)
+ | find n = tac(n) ORELSE find(n-1)
in find(nprems_of st)st end;
(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n).
@@ -334,9 +334,9 @@
val ct_eq_x = mk_prop_equals (ct, xfree)
and refl_ct = reflexive ct
fun restore th =
- implies_elim
- (forall_elim ct (forall_intr xfree (implies_intr ct_eq_x th)))
- refl_ct
+ implies_elim
+ (forall_elim ct (forall_intr xfree (implies_intr ct_eq_x th)))
+ refl_ct
in (equal_elim
(combination (combination refl_implies refl_ct) (assume ct_eq_x))
(trivial ct),
@@ -348,7 +348,7 @@
fun select tac st0 i =
let val cprem::_ = drop(i-1, cprems_of st0)
val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
- eq_trivial (adjust_maxidx cprem)
+ eq_trivial (adjust_maxidx cprem)
fun next st = bicompose false (false, restore st, nprems_of st) i st0
in Sequence.flats (Sequence.maps next (tac eq_cprem))
end;
@@ -361,13 +361,13 @@
(* Prevent the subgoal's assumptions from becoming additional subgoals in the
new proof state by enclosing them by a universal quantification *)
fun protect_subgoal st i =
- Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st)
- handle _ => error"SELECT_GOAL -- impossible error???";
+ Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st)
+ handle _ => error"SELECT_GOAL -- impossible error???";
fun SELECT_GOAL tac i st =
case (i, drop(i-1, prems_of st)) of
(_,[]) => Sequence.null
- | (1,[_]) => tac st (*If i=1 and only one subgoal do nothing!*)
+ | (1,[_]) => tac st (*If i=1 and only one subgoal do nothing!*)
| (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i
| (_, _::_) => select tac st i;
@@ -377,10 +377,10 @@
Main difference from strip_assums concerns parameters:
it replaces the bound variables by free variables. *)
fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) =
- strip_context_aux (params, H::Hs, B)
+ strip_context_aux (params, H::Hs, B)
| strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) =
let val (b,u) = variant_abs(a,T,t)
- in strip_context_aux ((b,T)::params, Hs, u) end
+ in strip_context_aux ((b,T)::params, Hs, u) end
| strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
fun strip_context A = strip_context_aux ([],[],A);
@@ -409,7 +409,7 @@
fun free_of s ((a,i), T) =
Free(s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i),
- T)
+ T)
fun mk_inst (var as Var(v,T)) = (var, free_of "METAHYP1_" (v,T))
in
@@ -431,17 +431,17 @@
(*Subgoal variables: make Free; lift type over params*)
fun mk_subgoal_inst concl_vars (var as Var(v,T)) =
if var mem concl_vars
- then (var, true, free_of "METAHYP2_" (v,T))
- else (var, false,
- free_of "METAHYP2_" (v, map #2 params --->T))
+ then (var, true, free_of "METAHYP2_" (v,T))
+ else (var, false,
+ free_of "METAHYP2_" (v, map #2 params --->T))
(*Instantiate subgoal vars by Free applied to params*)
fun mk_ctpair (t,in_concl,u) =
- if in_concl then (cterm t, cterm u)
+ if in_concl then (cterm t, cterm u)
else (cterm t, cterm (list_comb (u,fparams)))
(*Restore Vars with higher type and index*)
fun mk_subgoal_swap_ctpair
- (t as Var((a,i),_), in_concl, u as Free(_,U)) =
- if in_concl then (cterm u, cterm t)
+ (t as Var((a,i),_), in_concl, u as Free(_,U)) =
+ if in_concl then (cterm u, cterm t)
else (cterm u, cterm(Var((a, i+maxidx), U)))
(*Embed B in the original context of params and hyps*)
fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
@@ -449,34 +449,34 @@
fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
(*Embed an ff pair in the original params*)
fun embed_ff(t,u) = Logic.mk_flexpair (list_abs_free (params, t),
- list_abs_free (params, u))
+ list_abs_free (params, u))
(*Remove parameter abstractions from the ff pairs*)
fun elim_ff ff = flexpair_abs_elim_list cparams ff
(*A form of lifting that discharges assumptions.*)
fun relift st =
- let val prop = #prop(rep_thm st)
- val subgoal_vars = (*Vars introduced in the subgoals*)
- foldr add_term_vars (Logic.strip_imp_prems prop, [])
- and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
- val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
- val st' = instantiate ([], map mk_ctpair subgoal_insts) st
- val emBs = map (cterm o embed) (prems_of st')
+ let val prop = #prop(rep_thm st)
+ val subgoal_vars = (*Vars introduced in the subgoals*)
+ foldr add_term_vars (Logic.strip_imp_prems prop, [])
+ and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
+ val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
+ val st' = instantiate ([], map mk_ctpair subgoal_insts) st
+ val emBs = map (cterm o embed) (prems_of st')
and ffs = map (cterm o embed_ff) (tpairs_of st')
- val Cth = implies_elim_list st'
- (map (elim_ff o assume) ffs @
- map (elim o assume) emBs)
- in (*restore the unknowns to the hypotheses*)
- free_instantiate (map swap_ctpair insts @
- map mk_subgoal_swap_ctpair subgoal_insts)
- (*discharge assumptions from state in same order*)
- (implies_intr_list (ffs@emBs)
- (forall_intr_list cparams (implies_intr_list chyps Cth)))
- end
+ val Cth = implies_elim_list st'
+ (map (elim_ff o assume) ffs @
+ map (elim o assume) emBs)
+ in (*restore the unknowns to the hypotheses*)
+ free_instantiate (map swap_ctpair insts @
+ map mk_subgoal_swap_ctpair subgoal_insts)
+ (*discharge assumptions from state in same order*)
+ (implies_intr_list (ffs@emBs)
+ (forall_intr_list cparams (implies_intr_list chyps Cth)))
+ end
val subprems = map (forall_elim_vars 0) hypths
and st0 = trivial (cterm concl)
(*function to replace the current subgoal*)
fun next st = bicompose false (false, relift st, nprems_of st)
- i state
+ i state
in Sequence.flats (Sequence.maps next (tacf subprems st0))
end;
end;