--- a/doc-src/Ref/tctical.tex Fri Jan 28 11:22:02 2000 +0100
+++ b/doc-src/Ref/tctical.tex Fri Jan 28 11:23:41 2000 +0100
@@ -67,11 +67,13 @@
\subsection{Repetition tacticals}
\index{tacticals!repetition}
\begin{ttbox}
-TRY : tactic -> tactic
-REPEAT_DETERM : tactic -> tactic
-REPEAT : tactic -> tactic
-REPEAT1 : tactic -> tactic
-trace_REPEAT : bool ref \hfill{\bf initially false}
+TRY : tactic -> tactic
+REPEAT_DETERM : tactic -> tactic
+REPEAT_DETERM_N : int -> tactic -> tactic
+REPEAT : tactic -> tactic
+REPEAT1 : tactic -> tactic
+DETERM_UNTIL : (thm -> bool) -> tactic -> tactic
+trace_REPEAT : bool ref \hfill{\bf initially false}
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{TRY} {\it tac}]
@@ -84,6 +86,10 @@
resulting sequence. It returns the first state to make {\it tac\/} fail.
It is deterministic, discarding alternative outcomes.
+\item[\ttindexbold{REPEAT_DETERM_N} {\it n} {\it tac}]
+is like \hbox{\tt REPEAT_DETERM {\it tac}} but the number of repititions
+is bound by {\it n} (unless negative).
+
\item[\ttindexbold{REPEAT} {\it tac}]
applies {\it tac\/} to the proof state and, recursively, to each element of
the resulting sequence. The resulting sequence consists of those states
@@ -96,6 +102,12 @@
is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at
least once, failing if this is impossible.
+\item[\ttindexbold{DETERM_UNTIL} {\it p} {\it tac}]
+applies {\it tac\/} to the proof state and, recursively, to the head of the
+resulting sequence, until the predicate {\it p} (applied on the proof state)
+yields {\it true}. It fails if {\it tac\/} fails on any of the intermediate
+states. It is deterministic, discarding alternative outcomes.
+
\item[set \ttindexbold{trace_REPEAT};]
enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM}
and {\tt REPEAT}. To view the tracing options, type {\tt h} at the prompt.
@@ -252,10 +264,11 @@
\index{tacticals!conditional}
\index{tacticals!deterministic}
\begin{ttbox}
-COND : (thm->bool) -> tactic -> tactic -> tactic
-IF_UNSOLVED : tactic -> tactic
-SOLVE : tactic -> tactic
-DETERM : tactic -> tactic
+COND : (thm->bool) -> tactic -> tactic -> tactic
+IF_UNSOLVED : tactic -> tactic
+SOLVE : tactic -> tactic
+DETERM : tactic -> tactic
+DETERM_UNTIL_SOLVED : tactic -> tactic
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$]
@@ -277,6 +290,10 @@
applies {\it tac\/} to the proof state and returns the head of the
resulting sequence. {\tt DETERM} limits the search space by making its
argument deterministic.
+
+\item[\ttindexbold{DETERM_UNTIL_SOLVED} {\it tac}]
+forces repeated deterministic application of {\it tac\/} to the proof state
+until the goal is solved completely.
\end{ttdescription}
--- a/src/HOLCF/domain/theorems.ML Fri Jan 28 11:22:02 2000 +0100
+++ b/src/HOLCF/domain/theorems.ML Fri Jan 28 11:23:41 2000 +0100
@@ -27,14 +27,6 @@
fun pg' thy defs t tacsf=pg'' thy defs t (fn [] => tacsf
| prems=> (cut_facts_tac prems 1)::tacsf);
-fun REPEAT_DETERM_UNTIL p tac =
-let fun drep st = if p st then Seq.single st
- else (case Seq.pull(tac st) of
- None => Seq.empty
- | Some(st',_) => drep st')
-in drep end;
-val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
-
local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in
val kill_neq_tac = dtac trueI2 end;
fun case_UU_tac rews i v = case_tac (v^"=UU") i THEN
@@ -131,7 +123,7 @@
rewrite_goals_tac axs_con_def,
dtac iso_swap 1,
simp_tac HOLCF_ss 1,
- UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
+ DETERM_UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
fun sum_tac [(_,args)] [p] =
prod_tac args THEN sum_rest_tac p
| sum_tac ((_,args)::cons') (p::prems) = DETERM(
@@ -159,7 +151,7 @@
else sum_tac cons (tl prems)])end;
val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[
rtac casedist 1,
- UNTIL_SOLVED(fast_tac HOL_cs 1)];
+ DETERM_UNTIL_SOLVED(fast_tac HOL_cs 1)];
end;
local
@@ -197,7 +189,7 @@
defined(%%(dis_name con)`%x_name)) [
rtac casedist 1,
contr_tac 1,
- UNTIL_SOLVED (CHANGED(asm_simp_tac
+ DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac
(HOLCF_ss addsimps dis_apps) 1))]) cons;
in dis_stricts @ dis_defins @ dis_apps end;
@@ -237,7 +229,7 @@
defined(%%(sel_of arg)`%x_name)) [
rtac casedist 1,
contr_tac 1,
- UNTIL_SOLVED (CHANGED(asm_simp_tac
+ DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac
(HOLCF_ss addsimps sel_apps) 1))])
(filter_out is_lazy (snd(hd cons))) else [];
val sel_rews = sel_stricts @ sel_defins @ sel_apps;
--- a/src/Pure/search.ML Fri Jan 28 11:22:02 2000 +0100
+++ b/src/Pure/search.ML Fri Jan 28 11:23:41 2000 +0100
@@ -24,6 +24,7 @@
val has_fewer_prems : int -> thm -> bool
val IF_UNSOLVED : tactic -> tactic
val SOLVE : tactic -> tactic
+ val DETERM_UNTIL_SOLVED: tactic -> tactic
val trace_BEST_FIRST : bool ref
val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic
val THEN_BEST_FIRST : tactic -> (thm->bool) * (thm->int) -> tactic
@@ -69,6 +70,9 @@
(*Force a tactic to solve its goal completely, otherwise fail *)
fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
+(*Force repeated application of tactic until goal is solved completely *)
+val DETERM_UNTIL_SOLVED = DETERM_UNTIL (has_fewer_prems 1);
+
(*Execute tac1, but only execute tac2 if there are at least as many subgoals
as before. This ensures that tac2 is only applied to an outcome of tac1.*)
fun (tac1 THEN_MAYBE tac2) st =
--- a/src/Pure/tctical.ML Fri Jan 28 11:22:02 2000 +0100
+++ b/src/Pure/tctical.ML Fri Jan 28 11:23:41 2000 +0100
@@ -41,13 +41,14 @@
val print_tac : string -> tactic
val REPEAT : tactic -> tactic
val REPEAT1 : tactic -> tactic
+ val REPEAT_FIRST : (int -> tactic) -> tactic
+ val REPEAT_SOME : (int -> 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 DETERM_UNTIL : (thm -> bool) -> tactic -> tactic
val SELECT_GOAL : tactic -> int -> tactic
val SOMEGOAL : (int -> tactic) -> tactic
val strip_context : term -> (string * typ) list * term list * term
@@ -244,6 +245,16 @@
handle TRACE_EXIT st' => Some(st', Seq.empty)));
+(*Deterministic DO..UNTIL: only retains the first outcome; tail recursive.
+ Forces repitition until predicate on state is fulfilled.*)
+fun DETERM_UNTIL p tac =
+let val tac = tracify trace_REPEAT tac
+ fun drep st = if p st then Some (st, Seq.empty)
+ else (case Seq.pull(tac st) of
+ None => None
+ | Some(st',_) => drep st')
+in traced_tac drep end;
+
(*Deterministic REPEAT: only retains the first outcome;
uses less space than REPEAT; tail recursive.
If non-negative, n bounds the number of repetitions.*)