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