src/Pure/tactic.ML
author lcp
Tue Jul 25 17:03:16 1995 +0200 (1995-07-25 ago)
changeset 1194 563ecd14c1d8
parent 1077 c2df11ae8b55
child 1209 03dc596b3a18
permissions -rw-r--r--
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
     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 rtac: thm -> int -> tactic
    75   val rule_by_tactic: tactic -> thm -> thm
    76   val subgoal_tac: string -> int -> tactic
    77   val subgoals_tac: string list -> int -> tactic
    78   val subgoals_of_brl: bool * thm -> int
    79   val trace_goalno_tac: (int -> tactic) -> int -> tactic
    80   end
    81 end;
    82 
    83 
    84 functor TacticFun (structure Logic: LOGIC and Drule: DRULE and 
    85 		   Tactical: TACTICAL and Net: NET
    86 	  sharing Drule.Thm = Tactical.Thm) : TACTIC = 
    87 struct
    88 structure Tactical = Tactical;
    89 structure Thm = Tactical.Thm;
    90 structure Net = Net;
    91 structure Sequence = Thm.Sequence;
    92 structure Sign = Thm.Sign;
    93 local open Tactical Tactical.Thm Drule
    94 in
    95 
    96 (*Discover what goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
    97 fun trace_goalno_tac tf i = Tactic (fn state => 
    98     case Sequence.pull(tapply(tf i, state)) of
    99 	None    => Sequence.null
   100       | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
   101     			 Sequence.seqof(fn()=> seqcell)));
   102 
   103 fun string_of (a,0) = a
   104   | string_of (a,i) = a ^ "_" ^ string_of_int i;
   105 
   106 (*convert all Vars in a theorem to Frees*)
   107 fun freeze th =
   108   let val fth = freezeT th
   109       val {prop,sign,...} = rep_thm fth
   110       fun mk_inst (Var(v,T)) = 
   111 	  (cterm_of sign (Var(v,T)),
   112 	   cterm_of sign (Free(string_of v, T)))
   113       val insts = map mk_inst (term_vars prop)
   114   in  instantiate ([],insts) fth  end;
   115 
   116 (*Makes a rule by applying a tactic to an existing rule*)
   117 fun rule_by_tactic (Tactic tf) rl =
   118     case Sequence.pull(tf (freeze (standard rl))) of
   119 	None        => raise THM("rule_by_tactic", 0, [rl])
   120       | Some(rl',_) => standard rl';
   121  
   122 (*** Basic tactics ***)
   123 
   124 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
   125 fun PRIMSEQ thmfun = Tactic (fn state => thmfun state
   126 			                 handle THM _ => Sequence.null);
   127 
   128 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
   129 fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
   130 
   131 (*** The following fail if the goal number is out of range:
   132      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
   133 
   134 (*Solve subgoal i by assumption*)
   135 fun assume_tac i = PRIMSEQ (assumption i);
   136 
   137 (*Solve subgoal i by assumption, using no unification*)
   138 fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
   139 
   140 (** Resolution/matching tactics **)
   141 
   142 (*The composition rule/state: no lifting or var renaming.
   143   The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
   144 fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
   145 
   146 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   147   like [| P&Q; P==>R |] ==> R *)
   148 fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   149 
   150 (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
   151 fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
   152 
   153 (*Resolution: the simple case, works for introduction rules*)
   154 fun resolve_tac rules = biresolve_tac (map (pair false) rules);
   155 
   156 (*Resolution with elimination rules only*)
   157 fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
   158 
   159 (*Forward reasoning using destruction rules.*)
   160 fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
   161 
   162 (*Like forward_tac, but deletes the assumption after use.*)
   163 fun dresolve_tac rls = eresolve_tac (map make_elim rls);
   164 
   165 (*Shorthand versions: for resolution with a single theorem*)
   166 fun rtac rl = resolve_tac [rl];
   167 fun etac rl = eresolve_tac [rl];
   168 fun dtac rl = dresolve_tac [rl];
   169 val atac = assume_tac;
   170 
   171 (*Use an assumption or some rules ... A popular combination!*)
   172 fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
   173 
   174 (*Matching tactics -- as above, but forbid updating of state*)
   175 fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
   176 fun match_tac rules  = bimatch_tac (map (pair false) rules);
   177 fun ematch_tac rules = bimatch_tac (map (pair true) rules);
   178 fun dmatch_tac rls   = ematch_tac (map make_elim rls);
   179 
   180 (*Smash all flex-flex disagreement pairs in the proof state.*)
   181 val flexflex_tac = PRIMSEQ flexflex_rule;
   182 
   183 (*Lift and instantiate a rule wrt the given state and subgoal number *)
   184 fun lift_inst_rule (state, i, sinsts, rule) =
   185 let val {maxidx,sign,...} = rep_thm state
   186     val (_, _, Bi, _) = dest_state(state,i)
   187     val params = Logic.strip_params Bi	        (*params of subgoal i*)
   188     val params = rev(rename_wrt_term Bi params) (*as they are printed*)
   189     val paramTs = map #2 params
   190     and inc = maxidx+1
   191     fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
   192       | liftvar t = raise TERM("Variable expected", [t]);
   193     fun liftterm t = list_abs_free (params, 
   194 				    Logic.incr_indexes(paramTs,inc) t)
   195     (*Lifts instantiation pair over params*)
   196     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
   197     fun lifttvar((a,i),ctyp) =
   198 	let val {T,sign} = rep_ctyp ctyp
   199 	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
   200     val rts = types_sorts rule and (types,sorts) = types_sorts state
   201     fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
   202       | types'(ixn) = types ixn;
   203     val used = add_term_tvarnames
   204                   (#prop(rep_thm state) $ #prop(rep_thm rule),[])
   205     val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
   206 in instantiate (map lifttvar Tinsts, map liftpair insts)
   207                (lift_rule (state,i) rule)
   208 end;
   209 
   210 
   211 (*** Resolve after lifting and instantation; may refer to parameters of the
   212      subgoal.  Fails if "i" is out of range.  ***)
   213 
   214 (*compose version: arguments are as for bicompose.*)
   215 fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i =
   216   STATE ( fn state => 
   217 	   compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
   218 			nsubgoal) i
   219 	   handle TERM (msg,_) => (writeln msg;  no_tac)
   220 		| THM  (msg,_,_) => (writeln msg;  no_tac) );
   221 
   222 (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   223   terms that are substituted contain (term or type) unknowns from the
   224   goal, because it is unable to instantiate goal unknowns at the same time.
   225 
   226   The type checker is instructed not to freezes flexible type vars that
   227   were introduced during type inference and still remain in the term at the
   228   end.  This increases flexibility but can introduce schematic type vars in
   229   goals.
   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_tagged_brl (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_tagged_brl: 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_tagged_brl (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)  = nprems_of rule - 1
   393   | subgoals_of_brl (false,rule) = nprems_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;