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