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