src/Pure/tactic.ML
changeset 27243 d549b5b0f344
parent 27209 388fd72e9f26
child 29276 94b1ffec9201
     1.1 --- a/src/Pure/tactic.ML	Mon Jun 16 22:13:49 2008 +0200
     1.2 +++ b/src/Pure/tactic.ML	Mon Jun 16 22:13:50 2008 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1991  University of Cambridge
     1.6  
     1.7 -Tactics.
     1.8 +Basic tactics.
     1.9  *)
    1.10  
    1.11  signature BASIC_TACTIC =
    1.12 @@ -36,9 +36,6 @@
    1.13    val flexflex_tac: tactic
    1.14    val distinct_subgoal_tac: int -> tactic
    1.15    val distinct_subgoals_tac: tactic
    1.16 -  val lift_inst_rule: thm * int * (string*string)list * thm -> thm
    1.17 -  val term_lift_inst_rule:
    1.18 -    thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
    1.19    val metacut_tac: thm -> int -> tactic
    1.20    val cut_rules_tac: thm list -> int -> tactic
    1.21    val cut_facts_tac: thm list -> int -> tactic
    1.22 @@ -59,9 +56,7 @@
    1.23    val net_match_tac: thm list -> int -> tactic
    1.24    val subgoals_of_brl: bool * thm -> int
    1.25    val lessb: (bool * thm) * (bool * thm) -> bool
    1.26 -  val rename_params_tac: string list -> int -> tactic
    1.27 -  val rename_tac: string -> int -> tactic
    1.28 -  val rename_last_tac: string -> string list -> int -> tactic
    1.29 +  val rename_tac: string list -> int -> tactic
    1.30    val rotate_tac: int -> int -> tactic
    1.31    val defer_tac: int -> tactic
    1.32    val filter_prems_tac: (term -> bool) -> int -> tactic
    1.33 @@ -71,22 +66,8 @@
    1.34  sig
    1.35    include BASIC_TACTIC
    1.36    val innermost_params: int -> thm -> (string * typ) list
    1.37 -  val lift_inst_rule': thm * int * (indexname * string) list * thm -> thm
    1.38 -  val compose_inst_tac: (string * string) list -> (bool * thm * int) -> int -> tactic
    1.39 -  val res_inst_tac: (string * string) list -> thm -> int -> tactic
    1.40 -  val eres_inst_tac: (string * string) list -> thm -> int -> tactic
    1.41 -  val cut_inst_tac: (string * string) list -> thm -> int -> tactic
    1.42 -  val forw_inst_tac: (string * string) list -> thm -> int -> tactic
    1.43 -  val dres_inst_tac: (string * string) list -> thm -> int -> tactic
    1.44 -  val instantiate_tac: (string * string) list -> tactic
    1.45 -  val compose_inst_tac': (indexname * string) list -> (bool * thm * int) -> int -> tactic
    1.46 -  val res_inst_tac': (indexname * string) list -> thm -> int -> tactic
    1.47 -  val eres_inst_tac': (indexname * string) list -> thm -> int -> tactic
    1.48 -  val make_elim_preserve: thm -> thm
    1.49 -  val instantiate_tac': (indexname * string) list -> tactic
    1.50 -  val thin_tac: string -> int -> tactic
    1.51 -  val subgoal_tac: string -> int -> tactic
    1.52 -  val subgoals_tac: string list -> int -> tactic
    1.53 +  val term_lift_inst_rule:
    1.54 +    thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
    1.55    val untaglist: (int * 'a) list -> 'a list
    1.56    val orderlist: (int * 'a) list -> 'a list
    1.57    val insert_tagged_brl: 'a * (bool * thm) ->
    1.58 @@ -216,37 +197,6 @@
    1.59  (*params of subgoal i as they are printed*)
    1.60  fun params_of_state i st = rev (innermost_params i st);
    1.61  
    1.62 -(*read instantiations with respect to subgoal i of proof state st*)
    1.63 -fun read_insts_in_state (st, i, sinsts, rule) =
    1.64 -  let val thy = Thm.theory_of_thm st
    1.65 -      and params = params_of_state i st
    1.66 -      and rts = Drule.types_sorts rule and (types,sorts) = Drule.types_sorts st
    1.67 -      fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm)
    1.68 -        | types' ixn = types ixn;
    1.69 -      val used = Drule.add_used rule (Drule.add_used st []);
    1.70 -  in Drule.read_insts thy rts (types',sorts) used sinsts end;
    1.71 -
    1.72 -(*Lift and instantiate a rule wrt the given state and subgoal number *)
    1.73 -fun lift_inst_rule' (st, i, sinsts, rule) =
    1.74 -let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule)
    1.75 -    and {maxidx,...} = rep_thm st
    1.76 -    and params = params_of_state i st
    1.77 -    val paramTs = map #2 params
    1.78 -    and inc = maxidx+1
    1.79 -    fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
    1.80 -      | liftvar t = raise TERM("Variable expected", [t]);
    1.81 -    fun liftterm t = list_abs_free (params,
    1.82 -                                    Logic.incr_indexes(paramTs,inc) t)
    1.83 -    (*Lifts instantiation pair over params*)
    1.84 -    fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
    1.85 -    val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
    1.86 -in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
    1.87 -                     (Thm.lift_rule (Thm.cprem_of st i) rule)
    1.88 -end;
    1.89 -
    1.90 -fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
    1.91 -  (st, i, map (apfst Lexicon.read_indexname) sinsts, rule);
    1.92 -
    1.93  (*
    1.94  Like lift_inst_rule but takes terms, not strings, where the terms may contain
    1.95  Bounds referring to parameters of the subgoal.
    1.96 @@ -280,82 +230,13 @@
    1.97                       (Thm.lift_rule (Thm.cprem_of st i) rule)
    1.98  end;
    1.99  
   1.100 -(*** Resolve after lifting and instantation; may refer to parameters of the
   1.101 -     subgoal.  Fails if "i" is out of range.  ***)
   1.102  
   1.103 -(*compose version: arguments are as for bicompose.*)
   1.104 -fun gen_compose_inst_tac instf sinsts (bires_flg, rule, nsubgoal) i st =
   1.105 -  if i > nprems_of st then no_tac st
   1.106 -  else st |>
   1.107 -    (compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i
   1.108 -     handle TERM (msg,_)   => (warning msg;  no_tac)
   1.109 -          | THM  (msg,_,_) => (warning msg;  no_tac));
   1.110 -
   1.111 -val compose_inst_tac = gen_compose_inst_tac lift_inst_rule;
   1.112 -val compose_inst_tac' = gen_compose_inst_tac lift_inst_rule';
   1.113 -
   1.114 -(*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   1.115 -  terms that are substituted contain (term or type) unknowns from the
   1.116 -  goal, because it is unable to instantiate goal unknowns at the same time.
   1.117 -
   1.118 -  The type checker is instructed not to freeze flexible type vars that
   1.119 -  were introduced during type inference and still remain in the term at the
   1.120 -  end.  This increases flexibility but can introduce schematic type vars in
   1.121 -  goals.
   1.122 -*)
   1.123 -fun res_inst_tac sinsts rule i =
   1.124 -    compose_inst_tac sinsts (false, rule, nprems_of rule) i;
   1.125 -
   1.126 -fun res_inst_tac' sinsts rule i =
   1.127 -    compose_inst_tac' sinsts (false, rule, nprems_of rule) i;
   1.128 -
   1.129 -(*eresolve elimination version*)
   1.130 -fun eres_inst_tac sinsts rule i =
   1.131 -    compose_inst_tac sinsts (true, rule, nprems_of rule) i;
   1.132 -
   1.133 -fun eres_inst_tac' sinsts rule i =
   1.134 -    compose_inst_tac' sinsts (true, rule, nprems_of rule) i;
   1.135 -
   1.136 -(*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
   1.137 -  increment revcut_rl instead.*)
   1.138 -fun make_elim_preserve rl =
   1.139 -  let val maxidx = Thm.maxidx_of rl
   1.140 -      val thy = Thm.theory_of_thm rl
   1.141 -      fun cvar ixn = cterm_of thy (Var(ixn,propT));
   1.142 -      val revcut_rl' =
   1.143 -          instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   1.144 -                             (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
   1.145 -      val arg = (false, rl, nprems_of rl)
   1.146 -      val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
   1.147 -  in  th  end
   1.148 -  handle Bind => raise THM("make_elim_preserve", 1, [rl]);
   1.149 -
   1.150 -(*instantiate and cut -- for a FACT, anyway...*)
   1.151 -fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
   1.152 -
   1.153 -(*forward tactic applies a RULE to an assumption without deleting it*)
   1.154 -fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac;
   1.155 -
   1.156 -(*dresolve tactic applies a RULE to replace an assumption*)
   1.157 -fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
   1.158 -
   1.159 -(*instantiate variables in the whole state*)
   1.160 -val instantiate_tac = PRIMITIVE o Drule.read_instantiate;
   1.161 -
   1.162 -val instantiate_tac' = PRIMITIVE o Drule.read_instantiate';
   1.163 -
   1.164 -(*Deletion of an assumption*)
   1.165 -fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
   1.166  
   1.167  (*** Applications of cut_rl ***)
   1.168  
   1.169 -(*Used by metacut_tac*)
   1.170 -fun bires_cut_tac arg i =
   1.171 -    resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
   1.172 -
   1.173  (*The conclusion of the rule gets assumed in subgoal i,
   1.174    while subgoal i+1,... are the premises of the rule.*)
   1.175 -fun metacut_tac rule = bires_cut_tac [(false,rule)];
   1.176 +fun metacut_tac rule i = resolve_tac [cut_rl] i  THEN  biresolve_tac [(false, rule)] (i+1);
   1.177  
   1.178  (*"Cut" a list of rules into the goal.  Their premises will become new
   1.179    subgoals.*)
   1.180 @@ -365,18 +246,6 @@
   1.181    generates no additional subgoals. *)
   1.182  fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths);
   1.183  
   1.184 -(*Introduce the given proposition as a lemma and subgoal*)
   1.185 -fun subgoal_tac sprop =
   1.186 -  DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) =>
   1.187 -    let val concl' = Logic.strip_assums_concl prop in
   1.188 -      if null (term_tvars concl') then ()
   1.189 -      else warning"Type variables in new subgoal: add a type constraint?";
   1.190 -      all_tac
   1.191 -  end);
   1.192 -
   1.193 -(*Introduce a list of lemmas and subgoals*)
   1.194 -fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
   1.195 -
   1.196  
   1.197  (**** Indexing and filtering of theorems ****)
   1.198  
   1.199 @@ -504,40 +373,12 @@
   1.200  fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   1.201  
   1.202  
   1.203 -(*** Renaming of parameters in a subgoal
   1.204 -     Names may contain letters, digits or primes and must be
   1.205 -     separated by blanks ***)
   1.206 -
   1.207 -fun rename_params_tac xs i =
   1.208 +(*Renaming of parameters in a subgoal*)
   1.209 +fun rename_tac xs i =
   1.210    case Library.find_first (not o Syntax.is_identifier) xs of
   1.211        SOME x => error ("Not an identifier: " ^ x)
   1.212      | NONE => PRIMITIVE (rename_params_rule (xs, i));
   1.213  
   1.214 -(*scan a list of characters into "words" composed of "letters" (recognized by
   1.215 -  is_let) and separated by any number of non-"letters"*)
   1.216 -fun scanwords is_let cs =
   1.217 -  let fun scan1 [] = []
   1.218 -        | scan1 cs =
   1.219 -            let val (lets, rest) = take_prefix is_let cs
   1.220 -            in implode lets :: scanwords is_let rest end;
   1.221 -  in scan1 (#2 (take_prefix (not o is_let) cs)) end;
   1.222 -
   1.223 -fun rename_tac str i =
   1.224 -  let val cs = Symbol.explode str in
   1.225 -  case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of
   1.226 -      [] => rename_params_tac (scanwords Symbol.is_letdig cs) i
   1.227 -    | c::_ => error ("Illegal character: " ^ c)
   1.228 -  end;
   1.229 -
   1.230 -(*Rename recent parameters using names generated from a and the suffixes,
   1.231 -  provided the string a, which represents a term, is an identifier. *)
   1.232 -fun rename_last_tac a sufs i =
   1.233 -  let val names = map (curry op^ a) sufs
   1.234 -  in  if Syntax.is_identifier a
   1.235 -      then PRIMITIVE (rename_params_rule (names,i))
   1.236 -      else all_tac
   1.237 -  end;
   1.238 -
   1.239  (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   1.240    right to left if n is positive, and from left to right if n is negative.*)
   1.241  fun rotate_tac 0 i = all_tac