added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
authoroheimb
Fri Jan 28 11:23:41 2000 +0100 (2000-01-28)
changeset 8149941afb897532
parent 8148 5ef0b624aadb
child 8150 7021549ef32d
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
doc-src/Ref/tctical.tex
src/HOLCF/domain/theorems.ML
src/Pure/search.ML
src/Pure/tctical.ML
     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.51                                               (HOLCF_ss addsimps sel_apps) 1))]) 
    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.*)