author oheimb Fri Jan 28 11:23:41 2000 +0100 (2000-01-28) changeset 8149 941afb897532 parent 8148 5ef0b624aadb child 8150 7021549ef32d
 doc-src/Ref/tctical.tex file | annotate | diff | revisions src/HOLCF/domain/theorems.ML file | annotate | diff | revisions src/Pure/search.ML file | annotate | diff | revisions src/Pure/tctical.ML file | annotate | diff | revisions
     1.1 --- a/doc-src/Ref/tctical.tex	Fri Jan 28 11:22:02 2000 +0100
1.2 +++ b/doc-src/Ref/tctical.tex	Fri Jan 28 11:23:41 2000 +0100
1.3 @@ -67,11 +67,13 @@
1.4  \subsection{Repetition tacticals}
1.5  \index{tacticals!repetition}
1.6  \begin{ttbox}
1.7 -TRY           : tactic -> tactic
1.8 -REPEAT_DETERM : tactic -> tactic
1.9 -REPEAT        : tactic -> tactic
1.10 -REPEAT1       : tactic -> tactic
1.11 -trace_REPEAT  : bool ref \hfill{\bf initially false}
1.12 +TRY             : tactic -> tactic
1.13 +REPEAT_DETERM   : tactic -> tactic
1.14 +REPEAT_DETERM_N : int -> tactic -> tactic
1.15 +REPEAT          : tactic -> tactic
1.16 +REPEAT1         : tactic -> tactic
1.17 +DETERM_UNTIL    : (thm -> bool) -> tactic -> tactic
1.18 +trace_REPEAT    : bool ref \hfill{\bf initially false}
1.19  \end{ttbox}
1.20  \begin{ttdescription}
1.21  \item[\ttindexbold{TRY} {\it tac}]
1.22 @@ -84,6 +86,10 @@
1.23  resulting sequence.  It returns the first state to make {\it tac\/} fail.
1.24  It is deterministic, discarding alternative outcomes.
1.25
1.26 +\item[\ttindexbold{REPEAT_DETERM_N} {\it n} {\it tac}]
1.27 +is like \hbox{\tt REPEAT_DETERM {\it tac}} but the number of repititions
1.28 +is bound by {\it n} (unless negative).
1.29 +
1.30  \item[\ttindexbold{REPEAT} {\it tac}]
1.31  applies {\it tac\/} to the proof state and, recursively, to each element of
1.32  the resulting sequence.  The resulting sequence consists of those states
1.33 @@ -96,6 +102,12 @@
1.34  is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at
1.35  least once, failing if this is impossible.
1.36
1.37 +\item[\ttindexbold{DETERM_UNTIL} {\it p} {\it tac}]
1.38 +applies {\it tac\/} to the proof state and, recursively, to the head of the
1.39 +resulting sequence, until the predicate {\it p} (applied on the proof state)
1.40 +yields {\it true}. It fails if {\it tac\/} fails on any of the intermediate
1.41 +states. It is deterministic, discarding alternative outcomes.
1.42 +
1.43  \item[set \ttindexbold{trace_REPEAT};]
1.44  enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM}
1.45  and {\tt REPEAT}.  To view the tracing options, type {\tt h} at the prompt.
1.46 @@ -252,10 +264,11 @@
1.47  \index{tacticals!conditional}
1.48  \index{tacticals!deterministic}
1.49  \begin{ttbox}
1.50 -COND        : (thm->bool) -> tactic -> tactic -> tactic
1.51 -IF_UNSOLVED : tactic -> tactic
1.52 -SOLVE       : tactic -> tactic
1.53 -DETERM      : tactic -> tactic
1.54 +COND                : (thm->bool) -> tactic -> tactic -> tactic
1.55 +IF_UNSOLVED         : tactic -> tactic
1.56 +SOLVE               : tactic -> tactic
1.57 +DETERM              : tactic -> tactic
1.58 +DETERM_UNTIL_SOLVED : tactic -> tactic
1.59  \end{ttbox}
1.60  \begin{ttdescription}
1.61  \item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$]
1.62 @@ -277,6 +290,10 @@
1.63  applies {\it tac\/} to the proof state and returns the head of the
1.64  resulting sequence.  {\tt DETERM} limits the search space by making its
1.65  argument deterministic.
1.66 +
1.67 +\item[\ttindexbold{DETERM_UNTIL_SOLVED} {\it tac}]
1.68 +forces repeated deterministic application of {\it tac\/} to the proof state
1.69 +until the goal is solved completely.
1.70  \end{ttdescription}
1.71
1.72

     2.1 --- a/src/HOLCF/domain/theorems.ML	Fri Jan 28 11:22:02 2000 +0100
2.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Jan 28 11:23:41 2000 +0100
2.3 @@ -27,14 +27,6 @@
2.4  fun pg'  thy defs t tacsf=pg'' thy defs t (fn []   => tacsf
2.5                                  | prems=> (cut_facts_tac prems 1)::tacsf);
2.6
2.7 -fun REPEAT_DETERM_UNTIL p tac =
2.8 -let fun drep st = if p st then Seq.single st
2.9 -                          else (case Seq.pull(tac st) of
2.10 -                                  None        => Seq.empty
2.11 -                                | Some(st',_) => drep st')
2.12 -in drep end;
2.13 -val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
2.14 -
2.15  local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in
2.16  val kill_neq_tac = dtac trueI2 end;
2.17  fun case_UU_tac rews i v =      case_tac (v^"=UU") i THEN
2.18 @@ -131,7 +123,7 @@
2.19                                  rewrite_goals_tac axs_con_def,
2.20                                  dtac iso_swap 1,
2.21                                  simp_tac HOLCF_ss 1,
2.22 -                                UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
2.23 +                                DETERM_UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
2.24              fun sum_tac [(_,args)]       [p]        =
2.25                                  prod_tac args THEN sum_rest_tac p
2.26              |   sum_tac ((_,args)::cons') (p::prems) = DETERM(
2.27 @@ -159,7 +151,7 @@
2.28                                  else sum_tac cons (tl prems)])end;
2.29  val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[
2.30                                  rtac casedist 1,
2.31 -                                UNTIL_SOLVED(fast_tac HOL_cs 1)];
2.32 +                                DETERM_UNTIL_SOLVED(fast_tac HOL_cs 1)];
2.33  end;
2.34
2.35  local
2.36 @@ -197,7 +189,7 @@
2.37                        defined(%%(dis_name con)%x_name)) [
2.38                                  rtac casedist 1,
2.39                                  contr_tac 1,
2.40 -                                UNTIL_SOLVED (CHANGED(asm_simp_tac
2.41 +                                DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac
2.42                                          (HOLCF_ss addsimps dis_apps) 1))]) cons;
2.43  in dis_stricts @ dis_defins @ dis_apps end;
2.44
2.45 @@ -237,7 +229,7 @@
2.46                          defined(%%(sel_of arg)%x_name)) [
2.47                                  rtac casedist 1,
2.48                                  contr_tac 1,
2.49 -                                UNTIL_SOLVED (CHANGED(asm_simp_tac
2.50 +                                DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac
2.52                   (filter_out is_lazy (snd(hd cons))) else [];
2.53  val sel_rews = sel_stricts @ sel_defins @ sel_apps;

     3.1 --- a/src/Pure/search.ML	Fri Jan 28 11:22:02 2000 +0100
3.2 +++ b/src/Pure/search.ML	Fri Jan 28 11:23:41 2000 +0100
3.3 @@ -24,6 +24,7 @@
3.4    val has_fewer_prems	: int -> thm -> bool
3.5    val IF_UNSOLVED	: tactic -> tactic
3.6    val SOLVE		: tactic -> tactic
3.7 +  val DETERM_UNTIL_SOLVED: tactic -> tactic
3.8    val trace_BEST_FIRST	: bool ref
3.9    val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
3.10    val THEN_BEST_FIRST	: tactic -> (thm->bool) * (thm->int) -> tactic
3.11 @@ -69,6 +70,9 @@
3.12  (*Force a tactic to solve its goal completely, otherwise fail *)
3.13  fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
3.14
3.15 +(*Force repeated application of tactic until goal is solved completely *)
3.16 +val DETERM_UNTIL_SOLVED = DETERM_UNTIL (has_fewer_prems 1);
3.17 +
3.18  (*Execute tac1, but only execute tac2 if there are at least as many subgoals
3.19    as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
3.20  fun (tac1 THEN_MAYBE tac2) st =

     4.1 --- a/src/Pure/tctical.ML	Fri Jan 28 11:22:02 2000 +0100
4.2 +++ b/src/Pure/tctical.ML	Fri Jan 28 11:23:41 2000 +0100
4.3 @@ -41,13 +41,14 @@
4.4    val print_tac         : string -> tactic
4.5    val REPEAT            : tactic -> tactic
4.6    val REPEAT1           : tactic -> tactic
4.7 +  val REPEAT_FIRST      : (int -> tactic) -> tactic
4.8 +  val REPEAT_SOME       : (int -> tactic) -> tactic
4.9    val REPEAT_DETERM_N   : int -> tactic -> tactic
4.10    val REPEAT_DETERM     : tactic -> tactic
4.11    val REPEAT_DETERM1    : tactic -> tactic
4.12    val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic
4.13    val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
4.14 -  val REPEAT_FIRST      : (int -> tactic) -> tactic
4.15 -  val REPEAT_SOME       : (int -> tactic) -> tactic
4.16 +  val DETERM_UNTIL      : (thm -> bool) -> tactic -> tactic
4.17    val SELECT_GOAL       : tactic -> int -> tactic
4.18    val SOMEGOAL          : (int -> tactic) -> tactic
4.19    val strip_context     : term -> (string * typ) list * term list * term
4.20 @@ -244,6 +245,16 @@
4.21                           handle TRACE_EXIT st' => Some(st', Seq.empty)));
4.22
4.23
4.24 +(*Deterministic DO..UNTIL: only retains the first outcome; tail recursive.
4.25 +  Forces repitition until predicate on state is fulfilled.*)
4.26 +fun DETERM_UNTIL p tac =
4.27 +let val tac = tracify trace_REPEAT tac
4.28 +    fun drep st = if p st then Some (st, Seq.empty)
4.29 +                          else (case Seq.pull(tac st) of
4.30 +                                  None        => None
4.31 +                                | Some(st',_) => drep st')
4.32 +in  traced_tac drep  end;
4.33 +
4.34  (*Deterministic REPEAT: only retains the first outcome;
4.35    uses less space than REPEAT; tail recursive.
4.36    If non-negative, n bounds the number of repetitions.*)