src/Pure/tactic.ML
author paulson
Fri Feb 16 12:34:18 1996 +0100 (1996-02-16)
changeset 1501 bb7f99a0a6f0
parent 1460 5a6f2aabd538
child 1801 927a31ba4346
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 (*  Title: 	tactic
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Tactics 
     7 *)
     8 
     9 signature TACTIC =
    10   sig
    11   val ares_tac: thm list -> int -> tactic
    12   val asm_rewrite_goal_tac:
    13         bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
    14   val assume_tac: int -> tactic
    15   val atac: int ->tactic
    16   val bimatch_from_nets_tac: 
    17       (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    18   val bimatch_tac: (bool*thm)list -> int -> tactic
    19   val biresolve_from_nets_tac: 
    20       (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    21   val biresolve_tac: (bool*thm)list -> int -> tactic
    22   val build_net: thm list -> (int*thm) Net.net
    23   val build_netpair:    (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
    24       (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
    25   val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic
    26   val compose_tac: (bool * thm * int) -> int -> tactic 
    27   val cut_facts_tac: thm list -> int -> tactic
    28   val cut_inst_tac: (string*string)list -> thm -> int -> tactic   
    29   val dmatch_tac: thm list -> int -> tactic
    30   val dresolve_tac: thm list -> int -> tactic
    31   val dres_inst_tac: (string*string)list -> thm -> int -> tactic   
    32   val dtac: thm -> int ->tactic
    33   val etac: thm -> int ->tactic
    34   val eq_assume_tac: int -> tactic   
    35   val ematch_tac: thm list -> int -> tactic
    36   val eresolve_tac: thm list -> int -> tactic
    37   val eres_inst_tac: (string*string)list -> thm -> int -> tactic   
    38   val filter_thms: (term*term->bool) -> int*term*thm list -> thm list
    39   val filt_resolve_tac: thm list -> int -> int -> tactic
    40   val flexflex_tac: tactic
    41   val fold_goals_tac: thm list -> tactic
    42   val fold_tac: thm list -> tactic
    43   val forward_tac: thm list -> int -> tactic   
    44   val forw_inst_tac: (string*string)list -> thm -> int -> tactic
    45   val freeze: thm -> thm   
    46   val insert_tagged_brl:  ('a*(bool*thm)) * 
    47                     (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
    48                     ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
    49   val is_fact: thm -> bool
    50   val lessb: (bool * thm) * (bool * thm) -> bool
    51   val lift_inst_rule: thm * int * (string*string)list * thm -> thm
    52   val make_elim: thm -> thm
    53   val match_from_net_tac: (int*thm) Net.net -> int -> tactic
    54   val match_tac: thm list -> int -> tactic
    55   val metacut_tac: thm -> int -> tactic   
    56   val net_bimatch_tac: (bool*thm) list -> int -> tactic
    57   val net_biresolve_tac: (bool*thm) list -> int -> tactic
    58   val net_match_tac: thm list -> int -> tactic
    59   val net_resolve_tac: thm list -> int -> tactic
    60   val PRIMITIVE: (thm -> thm) -> tactic  
    61   val PRIMSEQ: (thm -> thm Sequence.seq) -> tactic  
    62   val prune_params_tac: tactic
    63   val rename_tac: string -> int -> tactic
    64   val rename_last_tac: string -> string list -> int -> tactic
    65   val resolve_from_net_tac: (int*thm) Net.net -> int -> tactic
    66   val resolve_tac: thm list -> int -> tactic
    67   val res_inst_tac: (string*string)list -> thm -> int -> tactic   
    68   val rewrite_goals_tac: thm list -> tactic
    69   val rewrite_tac: thm list -> tactic
    70   val rewtac: thm -> tactic
    71   val rotate_tac: int -> int -> tactic
    72   val rtac: thm -> int -> tactic
    73   val rule_by_tactic: tactic -> thm -> thm
    74   val subgoal_tac: string -> int -> tactic
    75   val subgoals_tac: string list -> int -> tactic
    76   val subgoals_of_brl: bool * thm -> int
    77   val trace_goalno_tac: (int -> tactic) -> int -> tactic
    78   end;
    79 
    80 
    81 structure Tactic : TACTIC = 
    82 struct
    83 
    84 (*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
    85 fun trace_goalno_tac tac i st =  
    86     case Sequence.pull(tac i st) of
    87 	None    => Sequence.null
    88       | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
    89     			 Sequence.seqof(fn()=> seqcell));
    90 
    91 fun string_of (a,0) = a
    92   | string_of (a,i) = a ^ "_" ^ string_of_int i;
    93 
    94 (*convert all Vars in a theorem to Frees*)
    95 fun freeze th =
    96   let val fth = freezeT th
    97       val {prop,sign,...} = rep_thm fth
    98       fun mk_inst (Var(v,T)) = 
    99 	  (cterm_of sign (Var(v,T)),
   100 	   cterm_of sign (Free(string_of v, T)))
   101       val insts = map mk_inst (term_vars prop)
   102   in  instantiate ([],insts) fth  end;
   103 
   104 (*Makes a rule by applying a tactic to an existing rule*)
   105 fun rule_by_tactic tac rl =
   106     case Sequence.pull(tac (freeze (standard rl))) of
   107 	None        => raise THM("rule_by_tactic", 0, [rl])
   108       | Some(rl',_) => standard rl';
   109  
   110 (*** Basic tactics ***)
   111 
   112 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
   113 fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Sequence.null;
   114 
   115 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
   116 fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
   117 
   118 (*** The following fail if the goal number is out of range:
   119      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
   120 
   121 (*Solve subgoal i by assumption*)
   122 fun assume_tac i = PRIMSEQ (assumption i);
   123 
   124 (*Solve subgoal i by assumption, using no unification*)
   125 fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
   126 
   127 (** Resolution/matching tactics **)
   128 
   129 (*The composition rule/state: no lifting or var renaming.
   130   The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
   131 fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
   132 
   133 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   134   like [| P&Q; P==>R |] ==> R *)
   135 fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   136 
   137 (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
   138 fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
   139 
   140 (*Resolution: the simple case, works for introduction rules*)
   141 fun resolve_tac rules = biresolve_tac (map (pair false) rules);
   142 
   143 (*Resolution with elimination rules only*)
   144 fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
   145 
   146 (*Forward reasoning using destruction rules.*)
   147 fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
   148 
   149 (*Like forward_tac, but deletes the assumption after use.*)
   150 fun dresolve_tac rls = eresolve_tac (map make_elim rls);
   151 
   152 (*Shorthand versions: for resolution with a single theorem*)
   153 fun rtac rl = resolve_tac [rl];
   154 fun etac rl = eresolve_tac [rl];
   155 fun dtac rl = dresolve_tac [rl];
   156 val atac = assume_tac;
   157 
   158 (*Use an assumption or some rules ... A popular combination!*)
   159 fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
   160 
   161 (*Matching tactics -- as above, but forbid updating of state*)
   162 fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
   163 fun match_tac rules  = bimatch_tac (map (pair false) rules);
   164 fun ematch_tac rules = bimatch_tac (map (pair true) rules);
   165 fun dmatch_tac rls   = ematch_tac (map make_elim rls);
   166 
   167 (*Smash all flex-flex disagreement pairs in the proof state.*)
   168 val flexflex_tac = PRIMSEQ flexflex_rule;
   169 
   170 (*Lift and instantiate a rule wrt the given state and subgoal number *)
   171 fun lift_inst_rule (st, i, sinsts, rule) =
   172 let val {maxidx,sign,...} = rep_thm st
   173     val (_, _, Bi, _) = dest_state(st,i)
   174     val params = Logic.strip_params Bi	        (*params of subgoal i*)
   175     val params = rev(rename_wrt_term Bi params) (*as they are printed*)
   176     val paramTs = map #2 params
   177     and inc = maxidx+1
   178     fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
   179       | liftvar t = raise TERM("Variable expected", [t]);
   180     fun liftterm t = list_abs_free (params, 
   181 				    Logic.incr_indexes(paramTs,inc) t)
   182     (*Lifts instantiation pair over params*)
   183     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
   184     fun lifttvar((a,i),ctyp) =
   185 	let val {T,sign} = rep_ctyp ctyp
   186 	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
   187     val rts = types_sorts rule and (types,sorts) = types_sorts st
   188     fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
   189       | types'(ixn) = types ixn;
   190     val used = add_term_tvarnames
   191                   (#prop(rep_thm st) $ #prop(rep_thm rule),[])
   192     val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
   193 in instantiate (map lifttvar Tinsts, map liftpair insts)
   194                (lift_rule (st,i) rule)
   195 end;
   196 
   197 
   198 (*** Resolve after lifting and instantation; may refer to parameters of the
   199      subgoal.  Fails if "i" is out of range.  ***)
   200 
   201 (*compose version: arguments are as for bicompose.*)
   202 fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i =
   203   STATE ( fn st => 
   204 	   compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule),
   205 			nsubgoal) i
   206 	   handle TERM (msg,_) => (writeln msg;  no_tac)
   207 		| THM  (msg,_,_) => (writeln msg;  no_tac) );
   208 
   209 (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   210   terms that are substituted contain (term or type) unknowns from the
   211   goal, because it is unable to instantiate goal unknowns at the same time.
   212 
   213   The type checker is instructed not to freezes flexible type vars that
   214   were introduced during type inference and still remain in the term at the
   215   end.  This increases flexibility but can introduce schematic type vars in
   216   goals.
   217 *)
   218 fun res_inst_tac sinsts rule i =
   219     compose_inst_tac sinsts (false, rule, nprems_of rule) i;
   220 
   221 (*eresolve elimination version*)
   222 fun eres_inst_tac sinsts rule i =
   223     compose_inst_tac sinsts (true, rule, nprems_of rule) i;
   224 
   225 (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
   226   increment revcut_rl instead.*)
   227 fun make_elim_preserve rl = 
   228   let val {maxidx,...} = rep_thm rl
   229       fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT));
   230       val revcut_rl' = 
   231 	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   232 			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
   233       val arg = (false, rl, nprems_of rl)
   234       val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl')
   235   in  th  end
   236   handle Bind => raise THM("make_elim_preserve", 1, [rl]);
   237 
   238 (*instantiate and cut -- for a FACT, anyway...*)
   239 fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
   240 
   241 (*forward tactic applies a RULE to an assumption without deleting it*)
   242 fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac;
   243 
   244 (*dresolve tactic applies a RULE to replace an assumption*)
   245 fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
   246 
   247 (*** Applications of cut_rl ***)
   248 
   249 (*Used by metacut_tac*)
   250 fun bires_cut_tac arg i =
   251     resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
   252 
   253 (*The conclusion of the rule gets assumed in subgoal i,
   254   while subgoal i+1,... are the premises of the rule.*)
   255 fun metacut_tac rule = bires_cut_tac [(false,rule)];
   256 
   257 (*Recognizes theorems that are not rules, but simple propositions*)
   258 fun is_fact rl =
   259     case prems_of rl of
   260 	[] => true  |  _::_ => false;
   261 
   262 (*"Cut" all facts from theorem list into the goal as assumptions. *)
   263 fun cut_facts_tac ths i =
   264     EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
   265 
   266 (*Introduce the given proposition as a lemma and subgoal*)
   267 fun subgoal_tac sprop = res_inst_tac [("psi", sprop)] cut_rl;
   268 
   269 (*Introduce a list of lemmas and subgoals*)
   270 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
   271 
   272 
   273 (**** Indexing and filtering of theorems ****)
   274 
   275 (*Returns the list of potentially resolvable theorems for the goal "prem",
   276 	using the predicate  could(subgoal,concl).
   277   Resulting list is no longer than "limit"*)
   278 fun filter_thms could (limit, prem, ths) =
   279   let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
   280       fun filtr (limit, []) = []
   281 	| filtr (limit, th::ths) =
   282 	    if limit=0 then  []
   283 	    else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   284 	    else filtr(limit,ths)
   285   in  filtr(limit,ths)  end;
   286 
   287 
   288 (*** biresolution and resolution using nets ***)
   289 
   290 (** To preserve the order of the rules, tag them with increasing integers **)
   291 
   292 (*insert tags*)
   293 fun taglist k [] = []
   294   | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
   295 
   296 (*remove tags and suppress duplicates -- list is assumed sorted!*)
   297 fun untaglist [] = []
   298   | untaglist [(k:int,x)] = [x]
   299   | untaglist ((k,x) :: (rest as (k',x')::_)) =
   300       if k=k' then untaglist rest
   301       else    x :: untaglist rest;
   302 
   303 (*return list elements in original order*)
   304 val orderlist = untaglist o sort (fn(x,y)=> #1 x < #1 y); 
   305 
   306 (*insert one tagged brl into the pair of nets*)
   307 fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
   308     if eres then 
   309 	case prems_of th of
   310 	    prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
   311 	  | [] => error"insert_tagged_brl: elimination rule with no premises"
   312     else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
   313 
   314 (*build a pair of nets for biresolution*)
   315 fun build_netpair netpair brls = 
   316     foldr insert_tagged_brl (taglist 1 brls, netpair);
   317 
   318 (*biresolution using a pair of nets rather than rules*)
   319 fun biresolution_from_nets_tac match (inet,enet) =
   320   SUBGOAL
   321     (fn (prem,i) =>
   322       let val hyps = Logic.strip_assums_hyp prem
   323           and concl = Logic.strip_assums_concl prem 
   324           val kbrls = Net.unify_term inet concl @
   325                       flat (map (Net.unify_term enet) hyps)
   326       in PRIMSEQ (biresolution match (orderlist kbrls) i) end);
   327 
   328 (*versions taking pre-built nets*)
   329 val biresolve_from_nets_tac = biresolution_from_nets_tac false;
   330 val bimatch_from_nets_tac = biresolution_from_nets_tac true;
   331 
   332 (*fast versions using nets internally*)
   333 val net_biresolve_tac =
   334     biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
   335 
   336 val net_bimatch_tac =
   337     bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
   338 
   339 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
   340 
   341 (*insert one tagged rl into the net*)
   342 fun insert_krl (krl as (k,th), net) =
   343     Net.insert_term ((concl_of th, krl), net, K false);
   344 
   345 (*build a net of rules for resolution*)
   346 fun build_net rls = 
   347     foldr insert_krl (taglist 1 rls, Net.empty);
   348 
   349 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   350 fun filt_resolution_from_net_tac match pred net =
   351   SUBGOAL
   352     (fn (prem,i) =>
   353       let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   354       in 
   355 	 if pred krls  
   356          then PRIMSEQ
   357 		(biresolution match (map (pair false) (orderlist krls)) i)
   358          else no_tac
   359       end);
   360 
   361 (*Resolve the subgoal using the rules (making a net) unless too flexible,
   362    which means more than maxr rules are unifiable.      *)
   363 fun filt_resolve_tac rules maxr = 
   364     let fun pred krls = length krls <= maxr
   365     in  filt_resolution_from_net_tac false pred (build_net rules)  end;
   366 
   367 (*versions taking pre-built nets*)
   368 val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
   369 val match_from_net_tac = filt_resolution_from_net_tac true (K true);
   370 
   371 (*fast versions using nets internally*)
   372 val net_resolve_tac = resolve_from_net_tac o build_net;
   373 val net_match_tac = match_from_net_tac o build_net;
   374 
   375 
   376 (*** For Natural Deduction using (bires_flg, rule) pairs ***)
   377 
   378 (*The number of new subgoals produced by the brule*)
   379 fun subgoals_of_brl (true,rule)  = nprems_of rule - 1
   380   | subgoals_of_brl (false,rule) = nprems_of rule;
   381 
   382 (*Less-than test: for sorting to minimize number of new subgoals*)
   383 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   384 
   385 
   386 (*** Meta-Rewriting Tactics ***)
   387 
   388 fun result1 tacf mss thm =
   389   case Sequence.pull(tacf mss thm) of
   390     None => None
   391   | Some(thm,_) => Some(thm);
   392 
   393 (*Rewrite subgoal i only *)
   394 fun asm_rewrite_goal_tac mode prover_tac mss i =
   395       PRIMITIVE(rewrite_goal_rule mode (result1 prover_tac) mss i);
   396 
   397 (*Rewrite throughout proof state. *)
   398 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
   399 
   400 (*Rewrite subgoals only, not main goal. *)
   401 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   402 
   403 fun rewtac def = rewrite_goals_tac [def];
   404 
   405 
   406 (*** for folding definitions, handling critical pairs ***)
   407 
   408 (*The depth of nesting in a term*)
   409 fun term_depth (Abs(a,T,t)) = 1 + term_depth t
   410   | term_depth (f$t) = 1 + max [term_depth f, term_depth t]
   411   | term_depth _ = 0;
   412 
   413 val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm;
   414 
   415 (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
   416   Returns longest lhs first to avoid folding its subexpressions.*)
   417 fun sort_lhs_depths defs =
   418   let val keylist = make_keylist (term_depth o lhs_of_thm) defs
   419       val keys = distinct (sort op> (map #2 keylist))
   420   in  map (keyfilter keylist) keys  end;
   421 
   422 fun fold_tac defs = EVERY 
   423     (map rewrite_tac (sort_lhs_depths (map symmetric defs)));
   424 
   425 fun fold_goals_tac defs = EVERY 
   426     (map rewrite_goals_tac (sort_lhs_depths (map symmetric defs)));
   427 
   428 
   429 (*** Renaming of parameters in a subgoal
   430      Names may contain letters, digits or primes and must be
   431      separated by blanks ***)
   432 
   433 (*Calling this will generate the warning "Same as previous level" since
   434   it affects nothing but the names of bound variables!*)
   435 fun rename_tac str i = 
   436   let val cs = explode str 
   437   in  
   438   if !Logic.auto_rename 
   439   then (writeln"Note: setting Logic.auto_rename := false"; 
   440 	Logic.auto_rename := false)
   441   else ();
   442   case #2 (take_prefix (is_letdig orf is_blank) cs) of
   443       [] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i))
   444     | c::_ => error ("Illegal character: " ^ c)
   445   end;
   446 
   447 (*Rename recent parameters using names generated from a and the suffixes,
   448   provided the string a, which represents a term, is an identifier. *)
   449 fun rename_last_tac a sufs i = 
   450   let val names = map (curry op^ a) sufs
   451   in  if Syntax.is_identifier a
   452       then PRIMITIVE (rename_params_rule (names,i))
   453       else all_tac
   454   end;
   455 
   456 (*Prunes all redundant parameters from the proof state by rewriting*)
   457 val prune_params_tac = rewrite_tac [triv_forall_equality];
   458 
   459 (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   460   right to left if n is positive, and from left to right if n is negative.*)
   461 fun rotate_tac n =
   462   let fun rot(n) = EVERY'(replicate n (dtac asm_rl));
   463   in if n >= 0 then rot n
   464      else SUBGOAL (fn (t,i) => rot(length(Logic.strip_assums_hyp t)+n) i)
   465   end;
   466 
   467 end;
   468 
   469 open Tactic;