renamed Pure/tctical.ML to Pure/tactical.ML;
authorwenzelm
Fri Jul 24 12:00:02 2009 +0200 (2009-07-24 ago)
changeset 32169fbada8ed12e6
parent 32168 116461b8fc01
child 32170 541b35729992
renamed Pure/tctical.ML to Pure/tactical.ML;
src/Pure/General/seq.ML
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/tactical.ML
src/Pure/tctical.ML
     1.1 --- a/src/Pure/General/seq.ML	Fri Jul 24 11:55:34 2009 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Fri Jul 24 12:00:02 2009 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** sequence functions **)      (*cf. Pure/tctical.ML*)
     1.8 +(** sequence functions **)      (*cf. Pure/tactical.ML*)
     1.9  
    1.10  fun succeed x = single x;
    1.11  fun fail _ = empty;
     2.1 --- a/src/Pure/IsaMakefile	Fri Jul 24 11:55:34 2009 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Fri Jul 24 12:00:02 2009 +0200
     2.3 @@ -94,7 +94,7 @@
     2.4    item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML	\
     2.5    morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML	\
     2.6    primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML	\
     2.7 -  sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML	\
     2.8 +  sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tactical.ML	\
     2.9    term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML		\
    2.10    type_infer.ML unify.ML variable.ML
    2.11  	@./mk
     3.1 --- a/src/Pure/ROOT.ML	Fri Jul 24 11:55:34 2009 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Fri Jul 24 12:00:02 2009 +0200
     3.3 @@ -120,7 +120,7 @@
     3.4  use "variable.ML";
     3.5  use "conv.ML";
     3.6  use "display_goal.ML";
     3.7 -use "tctical.ML";
     3.8 +use "tactical.ML";
     3.9  use "search.ML";
    3.10  use "tactic.ML";
    3.11  use "meta_simplifier.ML";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/tactical.ML	Fri Jul 24 12:00:02 2009 +0200
     4.3 @@ -0,0 +1,524 @@
     4.4 +(*  Title:      Pure/tactical.ML
     4.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.6 +
     4.7 +Tacticals.
     4.8 +*)
     4.9 +
    4.10 +infix 1 THEN THEN' THEN_ALL_NEW;
    4.11 +infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
    4.12 +infix 0 THEN_ELSE;
    4.13 +
    4.14 +signature TACTICAL =
    4.15 +sig
    4.16 +  type tactic = thm -> thm Seq.seq
    4.17 +  val THEN: tactic * tactic -> tactic
    4.18 +  val ORELSE: tactic * tactic -> tactic
    4.19 +  val APPEND: tactic * tactic -> tactic
    4.20 +  val INTLEAVE: tactic * tactic -> tactic
    4.21 +  val THEN_ELSE: tactic * (tactic*tactic) -> tactic
    4.22 +  val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    4.23 +  val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    4.24 +  val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    4.25 +  val INTLEAVE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    4.26 +  val all_tac: tactic
    4.27 +  val no_tac: tactic
    4.28 +  val DETERM: tactic -> tactic
    4.29 +  val COND: (thm -> bool) -> tactic -> tactic -> tactic
    4.30 +  val TRY: tactic -> tactic
    4.31 +  val EVERY: tactic list -> tactic
    4.32 +  val EVERY': ('a -> tactic) list -> 'a -> tactic
    4.33 +  val EVERY1: (int -> tactic) list -> tactic
    4.34 +  val FIRST: tactic list -> tactic
    4.35 +  val FIRST': ('a -> tactic) list -> 'a -> tactic
    4.36 +  val FIRST1: (int -> tactic) list -> tactic
    4.37 +  val RANGE: (int -> tactic) list -> int -> tactic
    4.38 +  val print_tac: string -> tactic
    4.39 +  val pause_tac: tactic
    4.40 +  val trace_REPEAT: bool ref
    4.41 +  val suppress_tracing: bool ref
    4.42 +  val tracify: bool ref -> tactic -> tactic
    4.43 +  val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic
    4.44 +  val DETERM_UNTIL: (thm -> bool) -> tactic -> tactic
    4.45 +  val REPEAT_DETERM_N: int -> tactic -> tactic
    4.46 +  val REPEAT_DETERM: tactic -> tactic
    4.47 +  val REPEAT: tactic -> tactic
    4.48 +  val REPEAT_DETERM1: tactic -> tactic
    4.49 +  val REPEAT1: tactic -> tactic
    4.50 +  val FILTER: (thm -> bool) -> tactic -> tactic
    4.51 +  val CHANGED: tactic -> tactic
    4.52 +  val CHANGED_PROP: tactic -> tactic
    4.53 +  val ALLGOALS: (int -> tactic) -> tactic
    4.54 +  val SOMEGOAL: (int -> tactic) -> tactic
    4.55 +  val FIRSTGOAL: (int -> tactic) -> tactic
    4.56 +  val REPEAT_SOME: (int -> tactic) -> tactic
    4.57 +  val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
    4.58 +  val REPEAT_FIRST: (int -> tactic) -> tactic
    4.59 +  val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic
    4.60 +  val TRYALL: (int -> tactic) -> tactic
    4.61 +  val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic
    4.62 +  val SUBGOAL: ((term * int) -> tactic) -> int -> tactic
    4.63 +  val CHANGED_GOAL: (int -> tactic) -> int -> tactic
    4.64 +  val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic
    4.65 +  val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic
    4.66 +  val strip_context: term -> (string * typ) list * term list * term
    4.67 +  val metahyps_thms: int -> thm -> thm list option
    4.68 +  val METAHYPS: (thm list -> tactic) -> int -> tactic
    4.69 +  val PRIMSEQ: (thm -> thm Seq.seq) -> tactic
    4.70 +  val PRIMITIVE: (thm -> thm) -> tactic
    4.71 +  val SINGLE: tactic -> thm -> thm option
    4.72 +  val CONVERSION: conv -> int -> tactic
    4.73 +end;
    4.74 +
    4.75 +structure Tactical : TACTICAL =
    4.76 +struct
    4.77 +
    4.78 +(**** Tactics ****)
    4.79 +
    4.80 +(*A tactic maps a proof tree to a sequence of proof trees:
    4.81 +    if length of sequence = 0 then the tactic does not apply;
    4.82 +    if length > 1 then backtracking on the alternatives can occur.*)
    4.83 +
    4.84 +type tactic = thm -> thm Seq.seq;
    4.85 +
    4.86 +
    4.87 +(*** LCF-style tacticals ***)
    4.88 +
    4.89 +(*the tactical THEN performs one tactic followed by another*)
    4.90 +fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st);
    4.91 +
    4.92 +
    4.93 +(*The tactical ORELSE uses the first tactic that returns a nonempty sequence.
    4.94 +  Like in LCF, ORELSE commits to either tac1 or tac2 immediately.
    4.95 +  Does not backtrack to tac2 if tac1 was initially chosen. *)
    4.96 +fun (tac1 ORELSE tac2) st =
    4.97 +    case Seq.pull(tac1 st) of
    4.98 +        NONE       => tac2 st
    4.99 +      | sequencecell => Seq.make(fn()=> sequencecell);
   4.100 +
   4.101 +
   4.102 +(*The tactical APPEND combines the results of two tactics.
   4.103 +  Like ORELSE, but allows backtracking on both tac1 and tac2.
   4.104 +  The tactic tac2 is not applied until needed.*)
   4.105 +fun (tac1 APPEND tac2) st =
   4.106 +  Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st)));
   4.107 +
   4.108 +(*Like APPEND, but interleaves results of tac1 and tac2.*)
   4.109 +fun (tac1 INTLEAVE tac2) st =
   4.110 +    Seq.interleave(tac1 st,
   4.111 +                        Seq.make(fn()=> Seq.pull (tac2 st)));
   4.112 +
   4.113 +(*Conditional tactic.
   4.114 +        tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
   4.115 +        tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
   4.116 +*)
   4.117 +fun (tac THEN_ELSE (tac1, tac2)) st =
   4.118 +    case Seq.pull(tac st) of
   4.119 +        NONE    => tac2 st                                   (*failed; try tactic 2*)
   4.120 +      | seqcell => Seq.maps tac1 (Seq.make(fn()=> seqcell)); (*succeeded; use tactic 1*)
   4.121 +
   4.122 +
   4.123 +(*Versions for combining tactic-valued functions, as in
   4.124 +     SOMEGOAL (resolve_tac rls THEN' assume_tac) *)
   4.125 +fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x;
   4.126 +fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x;
   4.127 +fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x;
   4.128 +fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x;
   4.129 +
   4.130 +(*passes all proofs through unchanged;  identity of THEN*)
   4.131 +fun all_tac st = Seq.single st;
   4.132 +
   4.133 +(*passes no proofs through;  identity of ORELSE and APPEND*)
   4.134 +fun no_tac st  = Seq.empty;
   4.135 +
   4.136 +
   4.137 +(*Make a tactic deterministic by chopping the tail of the proof sequence*)
   4.138 +fun DETERM tac = Seq.DETERM tac;
   4.139 +
   4.140 +(*Conditional tactical: testfun controls which tactic to use next.
   4.141 +  Beware: due to eager evaluation, both thentac and elsetac are evaluated.*)
   4.142 +fun COND testfun thenf elsef = (fn prf =>
   4.143 +    if testfun prf then  thenf prf   else  elsef prf);
   4.144 +
   4.145 +(*Do the tactic or else do nothing*)
   4.146 +fun TRY tac = tac ORELSE all_tac;
   4.147 +
   4.148 +(*** List-oriented tactics ***)
   4.149 +
   4.150 +local
   4.151 +  (*This version of EVERY avoids backtracking over repeated states*)
   4.152 +
   4.153 +  fun EVY (trail, []) st =
   4.154 +        Seq.make (fn()=> SOME(st,
   4.155 +                        Seq.make (fn()=> Seq.pull (evyBack trail))))
   4.156 +    | EVY (trail, tac::tacs) st =
   4.157 +          case Seq.pull(tac st) of
   4.158 +              NONE    => evyBack trail              (*failed: backtrack*)
   4.159 +            | SOME(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
   4.160 +  and evyBack [] = Seq.empty (*no alternatives*)
   4.161 +    | evyBack ((st',q,tacs)::trail) =
   4.162 +          case Seq.pull q of
   4.163 +              NONE        => evyBack trail
   4.164 +            | SOME(st,q') => if Thm.eq_thm (st',st)
   4.165 +                             then evyBack ((st',q',tacs)::trail)
   4.166 +                             else EVY ((st,q',tacs)::trail, tacs) st
   4.167 +in
   4.168 +
   4.169 +(* EVERY [tac1,...,tacn]   equals    tac1 THEN ... THEN tacn   *)
   4.170 +fun EVERY tacs = EVY ([], tacs);
   4.171 +end;
   4.172 +
   4.173 +
   4.174 +(* EVERY' [tac1,...,tacn] i  equals    tac1 i THEN ... THEN tacn i   *)
   4.175 +fun EVERY' tacs i = EVERY (map (fn f => f i) tacs);
   4.176 +
   4.177 +(*Apply every tactic to 1*)
   4.178 +fun EVERY1 tacs = EVERY' tacs 1;
   4.179 +
   4.180 +(* FIRST [tac1,...,tacn]   equals    tac1 ORELSE ... ORELSE tacn   *)
   4.181 +fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac;
   4.182 +
   4.183 +(* FIRST' [tac1,...,tacn] i  equals    tac1 i ORELSE ... ORELSE tacn i   *)
   4.184 +fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac);
   4.185 +
   4.186 +(*Apply first tactic to 1*)
   4.187 +fun FIRST1 tacs = FIRST' tacs 1;
   4.188 +
   4.189 +(*Apply tactics on consecutive subgoals*)
   4.190 +fun RANGE [] _ = all_tac
   4.191 +  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
   4.192 +
   4.193 +
   4.194 +(*** Tracing tactics ***)
   4.195 +
   4.196 +(*Print the current proof state and pass it on.*)
   4.197 +fun print_tac msg st =
   4.198 + (tracing (msg ^ "\n" ^
   4.199 +    Pretty.string_of (Pretty.chunks
   4.200 +      (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st)));
   4.201 +  Seq.single st);
   4.202 +
   4.203 +(*Pause until a line is typed -- if non-empty then fail. *)
   4.204 +fun pause_tac st =
   4.205 +  (tracing "** Press RETURN to continue:";
   4.206 +   if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st
   4.207 +   else (tracing "Goodbye";  Seq.empty));
   4.208 +
   4.209 +exception TRACE_EXIT of thm
   4.210 +and TRACE_QUIT;
   4.211 +
   4.212 +(*Tracing flags*)
   4.213 +val trace_REPEAT= ref false
   4.214 +and suppress_tracing = ref false;
   4.215 +
   4.216 +(*Handle all tracing commands for current state and tactic *)
   4.217 +fun exec_trace_command flag (tac, st) =
   4.218 +   case TextIO.inputLine TextIO.stdIn of
   4.219 +       SOME "\n" => tac st
   4.220 +     | SOME "f\n" => Seq.empty
   4.221 +     | SOME "o\n" => (flag:=false;  tac st)
   4.222 +     | SOME "s\n" => (suppress_tracing:=true;  tac st)
   4.223 +     | SOME "x\n" => (tracing "Exiting now";  raise (TRACE_EXIT st))
   4.224 +     | SOME "quit\n" => raise TRACE_QUIT
   4.225 +     | _     => (tracing
   4.226 +"Type RETURN to continue or...\n\
   4.227 +\     f    - to fail here\n\
   4.228 +\     o    - to switch tracing off\n\
   4.229 +\     s    - to suppress tracing until next entry to a tactical\n\
   4.230 +\     x    - to exit at this point\n\
   4.231 +\     quit - to abort this tracing run\n\
   4.232 +\** Well? "     ;  exec_trace_command flag (tac, st));
   4.233 +
   4.234 +
   4.235 +(*Extract from a tactic, a thm->thm seq function that handles tracing*)
   4.236 +fun tracify flag tac st =
   4.237 +  if !flag andalso not (!suppress_tracing) then
   4.238 +    (tracing (Pretty.string_of (Pretty.chunks
   4.239 +        (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st @
   4.240 +          [Pretty.str "** Press RETURN to continue:"])));
   4.241 +     exec_trace_command flag (tac, st))
   4.242 +  else tac st;
   4.243 +
   4.244 +(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
   4.245 +fun traced_tac seqf st =
   4.246 +    (suppress_tracing := false;
   4.247 +     Seq.make (fn()=> seqf st
   4.248 +                         handle TRACE_EXIT st' => SOME(st', Seq.empty)));
   4.249 +
   4.250 +
   4.251 +(*Deterministic DO..UNTIL: only retains the first outcome; tail recursive.
   4.252 +  Forces repitition until predicate on state is fulfilled.*)
   4.253 +fun DETERM_UNTIL p tac =
   4.254 +let val tac = tracify trace_REPEAT tac
   4.255 +    fun drep st = if p st then SOME (st, Seq.empty)
   4.256 +                          else (case Seq.pull(tac st) of
   4.257 +                                  NONE        => NONE
   4.258 +                                | SOME(st',_) => drep st')
   4.259 +in  traced_tac drep  end;
   4.260 +
   4.261 +(*Deterministic REPEAT: only retains the first outcome;
   4.262 +  uses less space than REPEAT; tail recursive.
   4.263 +  If non-negative, n bounds the number of repetitions.*)
   4.264 +fun REPEAT_DETERM_N n tac =
   4.265 +  let val tac = tracify trace_REPEAT tac
   4.266 +      fun drep 0 st = SOME(st, Seq.empty)
   4.267 +        | drep n st =
   4.268 +           (case Seq.pull(tac st) of
   4.269 +                NONE       => SOME(st, Seq.empty)
   4.270 +              | SOME(st',_) => drep (n-1) st')
   4.271 +  in  traced_tac (drep n)  end;
   4.272 +
   4.273 +(*Allows any number of repetitions*)
   4.274 +val REPEAT_DETERM = REPEAT_DETERM_N ~1;
   4.275 +
   4.276 +(*General REPEAT: maintains a stack of alternatives; tail recursive*)
   4.277 +fun REPEAT tac =
   4.278 +  let val tac = tracify trace_REPEAT tac
   4.279 +      fun rep qs st =
   4.280 +        case Seq.pull(tac st) of
   4.281 +            NONE       => SOME(st, Seq.make(fn()=> repq qs))
   4.282 +          | SOME(st',q) => rep (q::qs) st'
   4.283 +      and repq [] = NONE
   4.284 +        | repq(q::qs) = case Seq.pull q of
   4.285 +            NONE       => repq qs
   4.286 +          | SOME(st,q) => rep (q::qs) st
   4.287 +  in  traced_tac (rep [])  end;
   4.288 +
   4.289 +(*Repeat 1 or more times*)
   4.290 +fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac;
   4.291 +fun REPEAT1 tac = tac THEN REPEAT tac;
   4.292 +
   4.293 +
   4.294 +(** Filtering tacticals **)
   4.295 +
   4.296 +fun FILTER pred tac st = Seq.filter pred (tac st);
   4.297 +
   4.298 +(*Accept only next states that change the theorem somehow*)
   4.299 +fun CHANGED tac st =
   4.300 +  let fun diff st' = not (Thm.eq_thm (st, st'));
   4.301 +  in Seq.filter diff (tac st) end;
   4.302 +
   4.303 +(*Accept only next states that change the theorem's prop field
   4.304 +  (changes to signature, hyps, etc. don't count)*)
   4.305 +fun CHANGED_PROP tac st =
   4.306 +  let fun diff st' = not (Thm.eq_thm_prop (st, st'));
   4.307 +  in Seq.filter diff (tac st) end;
   4.308 +
   4.309 +
   4.310 +(*** Tacticals based on subgoal numbering ***)
   4.311 +
   4.312 +(*For n subgoals, performs tac(n) THEN ... THEN tac(1)
   4.313 +  Essential to work backwards since tac(i) may add/delete subgoals at i. *)
   4.314 +fun ALLGOALS tac st =
   4.315 +  let fun doall 0 = all_tac
   4.316 +        | doall n = tac(n) THEN doall(n-1)
   4.317 +  in  doall(nprems_of st)st  end;
   4.318 +
   4.319 +(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1)  *)
   4.320 +fun SOMEGOAL tac st =
   4.321 +  let fun find 0 = no_tac
   4.322 +        | find n = tac(n) ORELSE find(n-1)
   4.323 +  in  find(nprems_of st)st  end;
   4.324 +
   4.325 +(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n).
   4.326 +  More appropriate than SOMEGOAL in some cases.*)
   4.327 +fun FIRSTGOAL tac st =
   4.328 +  let fun find (i,n) = if i>n then no_tac else  tac(i) ORELSE find (i+1,n)
   4.329 +  in  find(1, nprems_of st)st  end;
   4.330 +
   4.331 +(*Repeatedly solve some using tac. *)
   4.332 +fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac));
   4.333 +fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac));
   4.334 +
   4.335 +(*Repeatedly solve the first possible subgoal using tac. *)
   4.336 +fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac));
   4.337 +fun REPEAT_DETERM_FIRST tac = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tac));
   4.338 +
   4.339 +(*For n subgoals, tries to apply tac to n,...1  *)
   4.340 +fun TRYALL tac = ALLGOALS (TRY o tac);
   4.341 +
   4.342 +
   4.343 +(*Make a tactic for subgoal i, if there is one.  *)
   4.344 +fun CSUBGOAL goalfun i st =
   4.345 +  (case SOME (Thm.cprem_of st i) handle THM _ => NONE of
   4.346 +    SOME goal => goalfun (goal, i) st
   4.347 +  | NONE => Seq.empty);
   4.348 +
   4.349 +fun SUBGOAL goalfun =
   4.350 +  CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i));
   4.351 +
   4.352 +(*Returns all states that have changed in subgoal i, counted from the LAST
   4.353 +  subgoal.  For stac, for example.*)
   4.354 +fun CHANGED_GOAL tac i st =
   4.355 +    let val np = Thm.nprems_of st
   4.356 +        val d = np-i                 (*distance from END*)
   4.357 +        val t = Thm.term_of (Thm.cprem_of st i)
   4.358 +        fun diff st' =
   4.359 +            Thm.nprems_of st' - d <= 0   (*the subgoal no longer exists*)
   4.360 +            orelse
   4.361 +             not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
   4.362 +    in  Seq.filter diff (tac i st)  end
   4.363 +    handle Subscript => Seq.empty  (*no subgoal i*);
   4.364 +
   4.365 +fun (tac1 THEN_ALL_NEW tac2) i st =
   4.366 +  st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st'));
   4.367 +
   4.368 +(*repeatedly dig into any emerging subgoals*)
   4.369 +fun REPEAT_ALL_NEW tac =
   4.370 +  tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i));
   4.371 +
   4.372 +
   4.373 +(*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
   4.374 +    H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
   4.375 +  Main difference from strip_assums concerns parameters:
   4.376 +    it replaces the bound variables by free variables.  *)
   4.377 +fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) =
   4.378 +        strip_context_aux (params, H::Hs, B)
   4.379 +  | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) =
   4.380 +        let val (b,u) = Syntax.variant_abs(a,T,t)
   4.381 +        in  strip_context_aux ((b,T)::params, Hs, u)  end
   4.382 +  | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
   4.383 +
   4.384 +fun strip_context A = strip_context_aux ([],[],A);
   4.385 +
   4.386 +
   4.387 +(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
   4.388 +       METAHYPS (fn prems => tac prems) i
   4.389 +
   4.390 +converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
   4.391 +proof state A==>A, supplying A1,...,An as meta-level assumptions (in
   4.392 +"prems").  The parameters x1,...,xm become free variables.  If the
   4.393 +resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
   4.394 +then it is lifted back into the original context, yielding k subgoals.
   4.395 +
   4.396 +Replaces unknowns in the context by Frees having the prefix METAHYP_
   4.397 +New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
   4.398 +DOES NOT HANDLE TYPE UNKNOWNS.
   4.399 +****)
   4.400 +
   4.401 +local
   4.402 +
   4.403 +  (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   4.404 +    Instantiates distinct free variables by terms of same type.*)
   4.405 +  fun free_instantiate ctpairs =
   4.406 +    forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
   4.407 +
   4.408 +  fun free_of s ((a, i), T) =
   4.409 +    Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
   4.410 +
   4.411 +  fun mk_inst v = (Var v, free_of "METAHYP1_" v)
   4.412 +in
   4.413 +
   4.414 +(*Common code for METAHYPS and metahyps_thms*)
   4.415 +fun metahyps_split_prem prem =
   4.416 +  let (*find all vars in the hyps -- should find tvars also!*)
   4.417 +      val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
   4.418 +      val insts = map mk_inst hyps_vars
   4.419 +      (*replace the hyps_vars by Frees*)
   4.420 +      val prem' = subst_atomic insts prem
   4.421 +      val (params,hyps,concl) = strip_context prem'
   4.422 +  in (insts,params,hyps,concl)  end;
   4.423 +
   4.424 +fun metahyps_aux_tac tacf (prem,gno) state =
   4.425 +  let val (insts,params,hyps,concl) = metahyps_split_prem prem
   4.426 +      val maxidx = Thm.maxidx_of state
   4.427 +      val cterm = Thm.cterm_of (Thm.theory_of_thm state)
   4.428 +      val chyps = map cterm hyps
   4.429 +      val hypths = map assume chyps
   4.430 +      val subprems = map (Thm.forall_elim_vars 0) hypths
   4.431 +      val fparams = map Free params
   4.432 +      val cparams = map cterm fparams
   4.433 +      fun swap_ctpair (t,u) = (cterm u, cterm t)
   4.434 +      (*Subgoal variables: make Free; lift type over params*)
   4.435 +      fun mk_subgoal_inst concl_vars (v, T) =
   4.436 +          if member (op =) concl_vars (v, T)
   4.437 +          then ((v, T), true, free_of "METAHYP2_" (v, T))
   4.438 +          else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
   4.439 +      (*Instantiate subgoal vars by Free applied to params*)
   4.440 +      fun mk_ctpair (v, in_concl, u) =
   4.441 +          if in_concl then (cterm (Var v), cterm u)
   4.442 +          else (cterm (Var v), cterm (list_comb (u, fparams)))
   4.443 +      (*Restore Vars with higher type and index*)
   4.444 +      fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
   4.445 +          if in_concl then (cterm u, cterm (Var ((a, i), T)))
   4.446 +          else (cterm u, cterm (Var ((a, i + maxidx), U)))
   4.447 +      (*Embed B in the original context of params and hyps*)
   4.448 +      fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
   4.449 +      (*Strip the context using elimination rules*)
   4.450 +      fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
   4.451 +      (*A form of lifting that discharges assumptions.*)
   4.452 +      fun relift st =
   4.453 +        let val prop = Thm.prop_of st
   4.454 +            val subgoal_vars = (*Vars introduced in the subgoals*)
   4.455 +              fold Term.add_vars (Logic.strip_imp_prems prop) []
   4.456 +            and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
   4.457 +            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   4.458 +            val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
   4.459 +            val emBs = map (cterm o embed) (prems_of st')
   4.460 +            val Cth  = implies_elim_list st' (map (elim o assume) emBs)
   4.461 +        in  (*restore the unknowns to the hypotheses*)
   4.462 +            free_instantiate (map swap_ctpair insts @
   4.463 +                              map mk_subgoal_swap_ctpair subgoal_insts)
   4.464 +                (*discharge assumptions from state in same order*)
   4.465 +                (implies_intr_list emBs
   4.466 +                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
   4.467 +        end
   4.468 +      (*function to replace the current subgoal*)
   4.469 +      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
   4.470 +  in Seq.maps next (tacf subprems (trivial (cterm concl))) end;
   4.471 +
   4.472 +end;
   4.473 +
   4.474 +(*Returns the theorem list that METAHYPS would supply to its tactic*)
   4.475 +fun metahyps_thms i state =
   4.476 +  let val prem = Logic.nth_prem (i, Thm.prop_of state)
   4.477 +      and cterm = cterm_of (Thm.theory_of_thm state)
   4.478 +      val (_,_,hyps,_) = metahyps_split_prem prem
   4.479 +  in SOME (map (Thm.forall_elim_vars 0 o Thm.assume o cterm) hyps) end
   4.480 +  handle TERM ("nth_prem", [A]) => NONE;
   4.481 +
   4.482 +local
   4.483 +
   4.484 +fun print_vars_terms thy (n,thm) =
   4.485 +  let
   4.486 +    fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
   4.487 +    fun find_vars thy (Const (c, ty)) =
   4.488 +          if null (Term.add_tvarsT ty []) then I
   4.489 +          else insert (op =) (c ^ typed ty)
   4.490 +      | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
   4.491 +      | find_vars _ (Free _) = I
   4.492 +      | find_vars _ (Bound _) = I
   4.493 +      | find_vars thy (Abs (_, _, t)) = find_vars thy t
   4.494 +      | find_vars thy (t1 $ t2) =
   4.495 +          find_vars thy t1 #> find_vars thy t1;
   4.496 +    val prem = Logic.nth_prem (n, Thm.prop_of thm)
   4.497 +    val tms = find_vars thy prem []
   4.498 +  in
   4.499 +    (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
   4.500 +  end;
   4.501 +
   4.502 +in
   4.503 +
   4.504 +fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
   4.505 +  handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
   4.506 +
   4.507 +end;
   4.508 +
   4.509 +(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
   4.510 +fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
   4.511 +
   4.512 +(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
   4.513 +fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
   4.514 +
   4.515 +(*Inverse (more or less) of PRIMITIVE*)
   4.516 +fun SINGLE tacf = Option.map fst o Seq.pull o tacf
   4.517 +
   4.518 +(*Conversions as tactics*)
   4.519 +fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
   4.520 +  handle THM _ => Seq.empty
   4.521 +    | CTERM _ => Seq.empty
   4.522 +    | TERM _ => Seq.empty
   4.523 +    | TYPE _ => Seq.empty;
   4.524 +
   4.525 +end;
   4.526 +
   4.527 +open Tactical;
     5.1 --- a/src/Pure/tctical.ML	Fri Jul 24 11:55:34 2009 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,524 +0,0 @@
     5.4 -(*  Title:      Pure/tctical.ML
     5.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.6 -
     5.7 -Tacticals.
     5.8 -*)
     5.9 -
    5.10 -infix 1 THEN THEN' THEN_ALL_NEW;
    5.11 -infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
    5.12 -infix 0 THEN_ELSE;
    5.13 -
    5.14 -signature TACTICAL =
    5.15 -sig
    5.16 -  type tactic = thm -> thm Seq.seq
    5.17 -  val THEN: tactic * tactic -> tactic
    5.18 -  val ORELSE: tactic * tactic -> tactic
    5.19 -  val APPEND: tactic * tactic -> tactic
    5.20 -  val INTLEAVE: tactic * tactic -> tactic
    5.21 -  val THEN_ELSE: tactic * (tactic*tactic) -> tactic
    5.22 -  val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    5.23 -  val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    5.24 -  val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    5.25 -  val INTLEAVE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    5.26 -  val all_tac: tactic
    5.27 -  val no_tac: tactic
    5.28 -  val DETERM: tactic -> tactic
    5.29 -  val COND: (thm -> bool) -> tactic -> tactic -> tactic
    5.30 -  val TRY: tactic -> tactic
    5.31 -  val EVERY: tactic list -> tactic
    5.32 -  val EVERY': ('a -> tactic) list -> 'a -> tactic
    5.33 -  val EVERY1: (int -> tactic) list -> tactic
    5.34 -  val FIRST: tactic list -> tactic
    5.35 -  val FIRST': ('a -> tactic) list -> 'a -> tactic
    5.36 -  val FIRST1: (int -> tactic) list -> tactic
    5.37 -  val RANGE: (int -> tactic) list -> int -> tactic
    5.38 -  val print_tac: string -> tactic
    5.39 -  val pause_tac: tactic
    5.40 -  val trace_REPEAT: bool ref
    5.41 -  val suppress_tracing: bool ref
    5.42 -  val tracify: bool ref -> tactic -> tactic
    5.43 -  val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic
    5.44 -  val DETERM_UNTIL: (thm -> bool) -> tactic -> tactic
    5.45 -  val REPEAT_DETERM_N: int -> tactic -> tactic
    5.46 -  val REPEAT_DETERM: tactic -> tactic
    5.47 -  val REPEAT: tactic -> tactic
    5.48 -  val REPEAT_DETERM1: tactic -> tactic
    5.49 -  val REPEAT1: tactic -> tactic
    5.50 -  val FILTER: (thm -> bool) -> tactic -> tactic
    5.51 -  val CHANGED: tactic -> tactic
    5.52 -  val CHANGED_PROP: tactic -> tactic
    5.53 -  val ALLGOALS: (int -> tactic) -> tactic
    5.54 -  val SOMEGOAL: (int -> tactic) -> tactic
    5.55 -  val FIRSTGOAL: (int -> tactic) -> tactic
    5.56 -  val REPEAT_SOME: (int -> tactic) -> tactic
    5.57 -  val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
    5.58 -  val REPEAT_FIRST: (int -> tactic) -> tactic
    5.59 -  val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic
    5.60 -  val TRYALL: (int -> tactic) -> tactic
    5.61 -  val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic
    5.62 -  val SUBGOAL: ((term * int) -> tactic) -> int -> tactic
    5.63 -  val CHANGED_GOAL: (int -> tactic) -> int -> tactic
    5.64 -  val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic
    5.65 -  val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic
    5.66 -  val strip_context: term -> (string * typ) list * term list * term
    5.67 -  val metahyps_thms: int -> thm -> thm list option
    5.68 -  val METAHYPS: (thm list -> tactic) -> int -> tactic
    5.69 -  val PRIMSEQ: (thm -> thm Seq.seq) -> tactic
    5.70 -  val PRIMITIVE: (thm -> thm) -> tactic
    5.71 -  val SINGLE: tactic -> thm -> thm option
    5.72 -  val CONVERSION: conv -> int -> tactic
    5.73 -end;
    5.74 -
    5.75 -structure Tactical : TACTICAL =
    5.76 -struct
    5.77 -
    5.78 -(**** Tactics ****)
    5.79 -
    5.80 -(*A tactic maps a proof tree to a sequence of proof trees:
    5.81 -    if length of sequence = 0 then the tactic does not apply;
    5.82 -    if length > 1 then backtracking on the alternatives can occur.*)
    5.83 -
    5.84 -type tactic = thm -> thm Seq.seq;
    5.85 -
    5.86 -
    5.87 -(*** LCF-style tacticals ***)
    5.88 -
    5.89 -(*the tactical THEN performs one tactic followed by another*)
    5.90 -fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st);
    5.91 -
    5.92 -
    5.93 -(*The tactical ORELSE uses the first tactic that returns a nonempty sequence.
    5.94 -  Like in LCF, ORELSE commits to either tac1 or tac2 immediately.
    5.95 -  Does not backtrack to tac2 if tac1 was initially chosen. *)
    5.96 -fun (tac1 ORELSE tac2) st =
    5.97 -    case Seq.pull(tac1 st) of
    5.98 -        NONE       => tac2 st
    5.99 -      | sequencecell => Seq.make(fn()=> sequencecell);
   5.100 -
   5.101 -
   5.102 -(*The tactical APPEND combines the results of two tactics.
   5.103 -  Like ORELSE, but allows backtracking on both tac1 and tac2.
   5.104 -  The tactic tac2 is not applied until needed.*)
   5.105 -fun (tac1 APPEND tac2) st =
   5.106 -  Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st)));
   5.107 -
   5.108 -(*Like APPEND, but interleaves results of tac1 and tac2.*)
   5.109 -fun (tac1 INTLEAVE tac2) st =
   5.110 -    Seq.interleave(tac1 st,
   5.111 -                        Seq.make(fn()=> Seq.pull (tac2 st)));
   5.112 -
   5.113 -(*Conditional tactic.
   5.114 -        tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
   5.115 -        tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
   5.116 -*)
   5.117 -fun (tac THEN_ELSE (tac1, tac2)) st =
   5.118 -    case Seq.pull(tac st) of
   5.119 -        NONE    => tac2 st                                   (*failed; try tactic 2*)
   5.120 -      | seqcell => Seq.maps tac1 (Seq.make(fn()=> seqcell)); (*succeeded; use tactic 1*)
   5.121 -
   5.122 -
   5.123 -(*Versions for combining tactic-valued functions, as in
   5.124 -     SOMEGOAL (resolve_tac rls THEN' assume_tac) *)
   5.125 -fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x;
   5.126 -fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x;
   5.127 -fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x;
   5.128 -fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x;
   5.129 -
   5.130 -(*passes all proofs through unchanged;  identity of THEN*)
   5.131 -fun all_tac st = Seq.single st;
   5.132 -
   5.133 -(*passes no proofs through;  identity of ORELSE and APPEND*)
   5.134 -fun no_tac st  = Seq.empty;
   5.135 -
   5.136 -
   5.137 -(*Make a tactic deterministic by chopping the tail of the proof sequence*)
   5.138 -fun DETERM tac = Seq.DETERM tac;
   5.139 -
   5.140 -(*Conditional tactical: testfun controls which tactic to use next.
   5.141 -  Beware: due to eager evaluation, both thentac and elsetac are evaluated.*)
   5.142 -fun COND testfun thenf elsef = (fn prf =>
   5.143 -    if testfun prf then  thenf prf   else  elsef prf);
   5.144 -
   5.145 -(*Do the tactic or else do nothing*)
   5.146 -fun TRY tac = tac ORELSE all_tac;
   5.147 -
   5.148 -(*** List-oriented tactics ***)
   5.149 -
   5.150 -local
   5.151 -  (*This version of EVERY avoids backtracking over repeated states*)
   5.152 -
   5.153 -  fun EVY (trail, []) st =
   5.154 -        Seq.make (fn()=> SOME(st,
   5.155 -                        Seq.make (fn()=> Seq.pull (evyBack trail))))
   5.156 -    | EVY (trail, tac::tacs) st =
   5.157 -          case Seq.pull(tac st) of
   5.158 -              NONE    => evyBack trail              (*failed: backtrack*)
   5.159 -            | SOME(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
   5.160 -  and evyBack [] = Seq.empty (*no alternatives*)
   5.161 -    | evyBack ((st',q,tacs)::trail) =
   5.162 -          case Seq.pull q of
   5.163 -              NONE        => evyBack trail
   5.164 -            | SOME(st,q') => if Thm.eq_thm (st',st)
   5.165 -                             then evyBack ((st',q',tacs)::trail)
   5.166 -                             else EVY ((st,q',tacs)::trail, tacs) st
   5.167 -in
   5.168 -
   5.169 -(* EVERY [tac1,...,tacn]   equals    tac1 THEN ... THEN tacn   *)
   5.170 -fun EVERY tacs = EVY ([], tacs);
   5.171 -end;
   5.172 -
   5.173 -
   5.174 -(* EVERY' [tac1,...,tacn] i  equals    tac1 i THEN ... THEN tacn i   *)
   5.175 -fun EVERY' tacs i = EVERY (map (fn f => f i) tacs);
   5.176 -
   5.177 -(*Apply every tactic to 1*)
   5.178 -fun EVERY1 tacs = EVERY' tacs 1;
   5.179 -
   5.180 -(* FIRST [tac1,...,tacn]   equals    tac1 ORELSE ... ORELSE tacn   *)
   5.181 -fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac;
   5.182 -
   5.183 -(* FIRST' [tac1,...,tacn] i  equals    tac1 i ORELSE ... ORELSE tacn i   *)
   5.184 -fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac);
   5.185 -
   5.186 -(*Apply first tactic to 1*)
   5.187 -fun FIRST1 tacs = FIRST' tacs 1;
   5.188 -
   5.189 -(*Apply tactics on consecutive subgoals*)
   5.190 -fun RANGE [] _ = all_tac
   5.191 -  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
   5.192 -
   5.193 -
   5.194 -(*** Tracing tactics ***)
   5.195 -
   5.196 -(*Print the current proof state and pass it on.*)
   5.197 -fun print_tac msg st =
   5.198 - (tracing (msg ^ "\n" ^
   5.199 -    Pretty.string_of (Pretty.chunks
   5.200 -      (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st)));
   5.201 -  Seq.single st);
   5.202 -
   5.203 -(*Pause until a line is typed -- if non-empty then fail. *)
   5.204 -fun pause_tac st =
   5.205 -  (tracing "** Press RETURN to continue:";
   5.206 -   if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st
   5.207 -   else (tracing "Goodbye";  Seq.empty));
   5.208 -
   5.209 -exception TRACE_EXIT of thm
   5.210 -and TRACE_QUIT;
   5.211 -
   5.212 -(*Tracing flags*)
   5.213 -val trace_REPEAT= ref false
   5.214 -and suppress_tracing = ref false;
   5.215 -
   5.216 -(*Handle all tracing commands for current state and tactic *)
   5.217 -fun exec_trace_command flag (tac, st) =
   5.218 -   case TextIO.inputLine TextIO.stdIn of
   5.219 -       SOME "\n" => tac st
   5.220 -     | SOME "f\n" => Seq.empty
   5.221 -     | SOME "o\n" => (flag:=false;  tac st)
   5.222 -     | SOME "s\n" => (suppress_tracing:=true;  tac st)
   5.223 -     | SOME "x\n" => (tracing "Exiting now";  raise (TRACE_EXIT st))
   5.224 -     | SOME "quit\n" => raise TRACE_QUIT
   5.225 -     | _     => (tracing
   5.226 -"Type RETURN to continue or...\n\
   5.227 -\     f    - to fail here\n\
   5.228 -\     o    - to switch tracing off\n\
   5.229 -\     s    - to suppress tracing until next entry to a tactical\n\
   5.230 -\     x    - to exit at this point\n\
   5.231 -\     quit - to abort this tracing run\n\
   5.232 -\** Well? "     ;  exec_trace_command flag (tac, st));
   5.233 -
   5.234 -
   5.235 -(*Extract from a tactic, a thm->thm seq function that handles tracing*)
   5.236 -fun tracify flag tac st =
   5.237 -  if !flag andalso not (!suppress_tracing) then
   5.238 -    (tracing (Pretty.string_of (Pretty.chunks
   5.239 -        (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st @
   5.240 -          [Pretty.str "** Press RETURN to continue:"])));
   5.241 -     exec_trace_command flag (tac, st))
   5.242 -  else tac st;
   5.243 -
   5.244 -(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
   5.245 -fun traced_tac seqf st =
   5.246 -    (suppress_tracing := false;
   5.247 -     Seq.make (fn()=> seqf st
   5.248 -                         handle TRACE_EXIT st' => SOME(st', Seq.empty)));
   5.249 -
   5.250 -
   5.251 -(*Deterministic DO..UNTIL: only retains the first outcome; tail recursive.
   5.252 -  Forces repitition until predicate on state is fulfilled.*)
   5.253 -fun DETERM_UNTIL p tac =
   5.254 -let val tac = tracify trace_REPEAT tac
   5.255 -    fun drep st = if p st then SOME (st, Seq.empty)
   5.256 -                          else (case Seq.pull(tac st) of
   5.257 -                                  NONE        => NONE
   5.258 -                                | SOME(st',_) => drep st')
   5.259 -in  traced_tac drep  end;
   5.260 -
   5.261 -(*Deterministic REPEAT: only retains the first outcome;
   5.262 -  uses less space than REPEAT; tail recursive.
   5.263 -  If non-negative, n bounds the number of repetitions.*)
   5.264 -fun REPEAT_DETERM_N n tac =
   5.265 -  let val tac = tracify trace_REPEAT tac
   5.266 -      fun drep 0 st = SOME(st, Seq.empty)
   5.267 -        | drep n st =
   5.268 -           (case Seq.pull(tac st) of
   5.269 -                NONE       => SOME(st, Seq.empty)
   5.270 -              | SOME(st',_) => drep (n-1) st')
   5.271 -  in  traced_tac (drep n)  end;
   5.272 -
   5.273 -(*Allows any number of repetitions*)
   5.274 -val REPEAT_DETERM = REPEAT_DETERM_N ~1;
   5.275 -
   5.276 -(*General REPEAT: maintains a stack of alternatives; tail recursive*)
   5.277 -fun REPEAT tac =
   5.278 -  let val tac = tracify trace_REPEAT tac
   5.279 -      fun rep qs st =
   5.280 -        case Seq.pull(tac st) of
   5.281 -            NONE       => SOME(st, Seq.make(fn()=> repq qs))
   5.282 -          | SOME(st',q) => rep (q::qs) st'
   5.283 -      and repq [] = NONE
   5.284 -        | repq(q::qs) = case Seq.pull q of
   5.285 -            NONE       => repq qs
   5.286 -          | SOME(st,q) => rep (q::qs) st
   5.287 -  in  traced_tac (rep [])  end;
   5.288 -
   5.289 -(*Repeat 1 or more times*)
   5.290 -fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac;
   5.291 -fun REPEAT1 tac = tac THEN REPEAT tac;
   5.292 -
   5.293 -
   5.294 -(** Filtering tacticals **)
   5.295 -
   5.296 -fun FILTER pred tac st = Seq.filter pred (tac st);
   5.297 -
   5.298 -(*Accept only next states that change the theorem somehow*)
   5.299 -fun CHANGED tac st =
   5.300 -  let fun diff st' = not (Thm.eq_thm (st, st'));
   5.301 -  in Seq.filter diff (tac st) end;
   5.302 -
   5.303 -(*Accept only next states that change the theorem's prop field
   5.304 -  (changes to signature, hyps, etc. don't count)*)
   5.305 -fun CHANGED_PROP tac st =
   5.306 -  let fun diff st' = not (Thm.eq_thm_prop (st, st'));
   5.307 -  in Seq.filter diff (tac st) end;
   5.308 -
   5.309 -
   5.310 -(*** Tacticals based on subgoal numbering ***)
   5.311 -
   5.312 -(*For n subgoals, performs tac(n) THEN ... THEN tac(1)
   5.313 -  Essential to work backwards since tac(i) may add/delete subgoals at i. *)
   5.314 -fun ALLGOALS tac st =
   5.315 -  let fun doall 0 = all_tac
   5.316 -        | doall n = tac(n) THEN doall(n-1)
   5.317 -  in  doall(nprems_of st)st  end;
   5.318 -
   5.319 -(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1)  *)
   5.320 -fun SOMEGOAL tac st =
   5.321 -  let fun find 0 = no_tac
   5.322 -        | find n = tac(n) ORELSE find(n-1)
   5.323 -  in  find(nprems_of st)st  end;
   5.324 -
   5.325 -(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n).
   5.326 -  More appropriate than SOMEGOAL in some cases.*)
   5.327 -fun FIRSTGOAL tac st =
   5.328 -  let fun find (i,n) = if i>n then no_tac else  tac(i) ORELSE find (i+1,n)
   5.329 -  in  find(1, nprems_of st)st  end;
   5.330 -
   5.331 -(*Repeatedly solve some using tac. *)
   5.332 -fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac));
   5.333 -fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac));
   5.334 -
   5.335 -(*Repeatedly solve the first possible subgoal using tac. *)
   5.336 -fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac));
   5.337 -fun REPEAT_DETERM_FIRST tac = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tac));
   5.338 -
   5.339 -(*For n subgoals, tries to apply tac to n,...1  *)
   5.340 -fun TRYALL tac = ALLGOALS (TRY o tac);
   5.341 -
   5.342 -
   5.343 -(*Make a tactic for subgoal i, if there is one.  *)
   5.344 -fun CSUBGOAL goalfun i st =
   5.345 -  (case SOME (Thm.cprem_of st i) handle THM _ => NONE of
   5.346 -    SOME goal => goalfun (goal, i) st
   5.347 -  | NONE => Seq.empty);
   5.348 -
   5.349 -fun SUBGOAL goalfun =
   5.350 -  CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i));
   5.351 -
   5.352 -(*Returns all states that have changed in subgoal i, counted from the LAST
   5.353 -  subgoal.  For stac, for example.*)
   5.354 -fun CHANGED_GOAL tac i st =
   5.355 -    let val np = Thm.nprems_of st
   5.356 -        val d = np-i                 (*distance from END*)
   5.357 -        val t = Thm.term_of (Thm.cprem_of st i)
   5.358 -        fun diff st' =
   5.359 -            Thm.nprems_of st' - d <= 0   (*the subgoal no longer exists*)
   5.360 -            orelse
   5.361 -             not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
   5.362 -    in  Seq.filter diff (tac i st)  end
   5.363 -    handle Subscript => Seq.empty  (*no subgoal i*);
   5.364 -
   5.365 -fun (tac1 THEN_ALL_NEW tac2) i st =
   5.366 -  st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st'));
   5.367 -
   5.368 -(*repeatedly dig into any emerging subgoals*)
   5.369 -fun REPEAT_ALL_NEW tac =
   5.370 -  tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i));
   5.371 -
   5.372 -
   5.373 -(*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
   5.374 -    H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
   5.375 -  Main difference from strip_assums concerns parameters:
   5.376 -    it replaces the bound variables by free variables.  *)
   5.377 -fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) =
   5.378 -        strip_context_aux (params, H::Hs, B)
   5.379 -  | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) =
   5.380 -        let val (b,u) = Syntax.variant_abs(a,T,t)
   5.381 -        in  strip_context_aux ((b,T)::params, Hs, u)  end
   5.382 -  | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
   5.383 -
   5.384 -fun strip_context A = strip_context_aux ([],[],A);
   5.385 -
   5.386 -
   5.387 -(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
   5.388 -       METAHYPS (fn prems => tac prems) i
   5.389 -
   5.390 -converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
   5.391 -proof state A==>A, supplying A1,...,An as meta-level assumptions (in
   5.392 -"prems").  The parameters x1,...,xm become free variables.  If the
   5.393 -resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
   5.394 -then it is lifted back into the original context, yielding k subgoals.
   5.395 -
   5.396 -Replaces unknowns in the context by Frees having the prefix METAHYP_
   5.397 -New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
   5.398 -DOES NOT HANDLE TYPE UNKNOWNS.
   5.399 -****)
   5.400 -
   5.401 -local
   5.402 -
   5.403 -  (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   5.404 -    Instantiates distinct free variables by terms of same type.*)
   5.405 -  fun free_instantiate ctpairs =
   5.406 -    forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
   5.407 -
   5.408 -  fun free_of s ((a, i), T) =
   5.409 -    Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
   5.410 -
   5.411 -  fun mk_inst v = (Var v, free_of "METAHYP1_" v)
   5.412 -in
   5.413 -
   5.414 -(*Common code for METAHYPS and metahyps_thms*)
   5.415 -fun metahyps_split_prem prem =
   5.416 -  let (*find all vars in the hyps -- should find tvars also!*)
   5.417 -      val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
   5.418 -      val insts = map mk_inst hyps_vars
   5.419 -      (*replace the hyps_vars by Frees*)
   5.420 -      val prem' = subst_atomic insts prem
   5.421 -      val (params,hyps,concl) = strip_context prem'
   5.422 -  in (insts,params,hyps,concl)  end;
   5.423 -
   5.424 -fun metahyps_aux_tac tacf (prem,gno) state =
   5.425 -  let val (insts,params,hyps,concl) = metahyps_split_prem prem
   5.426 -      val maxidx = Thm.maxidx_of state
   5.427 -      val cterm = Thm.cterm_of (Thm.theory_of_thm state)
   5.428 -      val chyps = map cterm hyps
   5.429 -      val hypths = map assume chyps
   5.430 -      val subprems = map (Thm.forall_elim_vars 0) hypths
   5.431 -      val fparams = map Free params
   5.432 -      val cparams = map cterm fparams
   5.433 -      fun swap_ctpair (t,u) = (cterm u, cterm t)
   5.434 -      (*Subgoal variables: make Free; lift type over params*)
   5.435 -      fun mk_subgoal_inst concl_vars (v, T) =
   5.436 -          if member (op =) concl_vars (v, T)
   5.437 -          then ((v, T), true, free_of "METAHYP2_" (v, T))
   5.438 -          else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
   5.439 -      (*Instantiate subgoal vars by Free applied to params*)
   5.440 -      fun mk_ctpair (v, in_concl, u) =
   5.441 -          if in_concl then (cterm (Var v), cterm u)
   5.442 -          else (cterm (Var v), cterm (list_comb (u, fparams)))
   5.443 -      (*Restore Vars with higher type and index*)
   5.444 -      fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
   5.445 -          if in_concl then (cterm u, cterm (Var ((a, i), T)))
   5.446 -          else (cterm u, cterm (Var ((a, i + maxidx), U)))
   5.447 -      (*Embed B in the original context of params and hyps*)
   5.448 -      fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
   5.449 -      (*Strip the context using elimination rules*)
   5.450 -      fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
   5.451 -      (*A form of lifting that discharges assumptions.*)
   5.452 -      fun relift st =
   5.453 -        let val prop = Thm.prop_of st
   5.454 -            val subgoal_vars = (*Vars introduced in the subgoals*)
   5.455 -              fold Term.add_vars (Logic.strip_imp_prems prop) []
   5.456 -            and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
   5.457 -            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   5.458 -            val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
   5.459 -            val emBs = map (cterm o embed) (prems_of st')
   5.460 -            val Cth  = implies_elim_list st' (map (elim o assume) emBs)
   5.461 -        in  (*restore the unknowns to the hypotheses*)
   5.462 -            free_instantiate (map swap_ctpair insts @
   5.463 -                              map mk_subgoal_swap_ctpair subgoal_insts)
   5.464 -                (*discharge assumptions from state in same order*)
   5.465 -                (implies_intr_list emBs
   5.466 -                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
   5.467 -        end
   5.468 -      (*function to replace the current subgoal*)
   5.469 -      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
   5.470 -  in Seq.maps next (tacf subprems (trivial (cterm concl))) end;
   5.471 -
   5.472 -end;
   5.473 -
   5.474 -(*Returns the theorem list that METAHYPS would supply to its tactic*)
   5.475 -fun metahyps_thms i state =
   5.476 -  let val prem = Logic.nth_prem (i, Thm.prop_of state)
   5.477 -      and cterm = cterm_of (Thm.theory_of_thm state)
   5.478 -      val (_,_,hyps,_) = metahyps_split_prem prem
   5.479 -  in SOME (map (Thm.forall_elim_vars 0 o Thm.assume o cterm) hyps) end
   5.480 -  handle TERM ("nth_prem", [A]) => NONE;
   5.481 -
   5.482 -local
   5.483 -
   5.484 -fun print_vars_terms thy (n,thm) =
   5.485 -  let
   5.486 -    fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
   5.487 -    fun find_vars thy (Const (c, ty)) =
   5.488 -          if null (Term.add_tvarsT ty []) then I
   5.489 -          else insert (op =) (c ^ typed ty)
   5.490 -      | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
   5.491 -      | find_vars _ (Free _) = I
   5.492 -      | find_vars _ (Bound _) = I
   5.493 -      | find_vars thy (Abs (_, _, t)) = find_vars thy t
   5.494 -      | find_vars thy (t1 $ t2) =
   5.495 -          find_vars thy t1 #> find_vars thy t1;
   5.496 -    val prem = Logic.nth_prem (n, Thm.prop_of thm)
   5.497 -    val tms = find_vars thy prem []
   5.498 -  in
   5.499 -    (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
   5.500 -  end;
   5.501 -
   5.502 -in
   5.503 -
   5.504 -fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
   5.505 -  handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
   5.506 -
   5.507 -end;
   5.508 -
   5.509 -(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
   5.510 -fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
   5.511 -
   5.512 -(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
   5.513 -fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
   5.514 -
   5.515 -(*Inverse (more or less) of PRIMITIVE*)
   5.516 -fun SINGLE tacf = Option.map fst o Seq.pull o tacf
   5.517 -
   5.518 -(*Conversions as tactics*)
   5.519 -fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
   5.520 -  handle THM _ => Seq.empty
   5.521 -    | CTERM _ => Seq.empty
   5.522 -    | TERM _ => Seq.empty
   5.523 -    | TYPE _ => Seq.empty;
   5.524 -
   5.525 -end;
   5.526 -
   5.527 -open Tactical;