# HG changeset patch # User oheimb # Date 949055021 -3600 # Node ID 941afb897532e51c73f51f4c9db514e91f89ca5a # Parent 5ef0b624aadb972337916f8c22e266fa647beb74 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED diff -r 5ef0b624aadb -r 941afb897532 doc-src/Ref/tctical.tex --- 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} diff -r 5ef0b624aadb -r 941afb897532 src/HOLCF/domain/theorems.ML --- 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; diff -r 5ef0b624aadb -r 941afb897532 src/Pure/search.ML --- 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 = diff -r 5ef0b624aadb -r 941afb897532 src/Pure/tctical.ML --- 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.*)